From 0d997c9351fa1acf0f950c9094fd3e8945d9acf3 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Mon, 10 Sep 2018 19:27:05 -0700 Subject: 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. --- src/expr/expr_template.cpp | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'src') 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; -- cgit v1.2.3