From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Tue, 11 Sep 2018 02:27:05 +0000 (-0700)
Subject: Set NodeManager to nullptr when  exporting vars (#2445)
X-Git-Tag: cvc5-1.0.0~4664
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0d997c9351fa1acf0f950c9094fd3e8945d9acf3;p=cvc5.git

Set NodeManager to nullptr when  exporting vars (#2445)

PR #2409 assumed that temporarily setting the NodeManager to nullptr
when creating variables is not needed anymore. However, this made our
portfolio build fail. This commit reintroduces the temporary NodeManager
change while creating variables.
---

diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index c7ef4754f..61568e411 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -204,6 +204,10 @@ public:
           } else if(n.getKind() == kind::VARIABLE) {
             bool isGlobal;
             Node::fromExpr(from_e).getAttribute(GlobalVarAttr(), isGlobal);
+
+            // Temporarily set the node manager to nullptr; this gets around
+            // a check that mkVar isn't called internally
+            NodeManagerScope nullScope(nullptr);
             to_e = to->mkVar(name, type, isGlobal ? ExprManager::VAR_FLAG_GLOBAL : flags);// FIXME thread safety
           } else if(n.getKind() == kind::SKOLEM) {
             // skolems are only available at the Node level (not the Expr level)
@@ -228,6 +232,9 @@ public:
           }
           else
           {
+            // Temporarily set the node manager to nullptr; this gets around
+            // a check that mkVar isn't called internally
+            NodeManagerScope nullScope(nullptr);
             to_e = to->mkVar(type);  // FIXME thread safety
           }
           Debug("export") << "+ exported unnamed var `" << from_e << "' with type `" << from_e.getType() << "' to `" << to_e << "' with type `" << type << "'" << std::endl;