diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-09-10 19:27:05 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-09-10 19:27:05 -0700 |
| commit | 0d997c9351fa1acf0f950c9094fd3e8945d9acf3 (patch) | |
| tree | bbb48d0e1f14596bebb7f045e4af74976cb717bd /src/expr | |
| parent | 1a695dcbe3036ab0f1922c5655c082ec1f14db97 (diff) | |
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.
Diffstat (limited to 'src/expr')
| -rw-r--r-- | src/expr/expr_template.cpp | 7 |
1 files changed, 7 insertions, 0 deletions
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; |