diff options
Diffstat (limited to 'src/expr/expr_manager_template.cpp')
| -rw-r--r-- | src/expr/expr_manager_template.cpp | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 43161fe04..5dd7a4dfd 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -695,7 +695,8 @@ Expr ExprManager::mkVar(Type type) return Expr(this, d_nodeManager->mkVarPtr(*type.d_typeNode)); } -Expr ExprManager::mkBoundVar(const std::string& name, Type type) { +Expr ExprManager::mkBoundVar(const std::string& name, Type type) +{ NodeManagerScope nms(d_nodeManager); Node* n = d_nodeManager->mkBoundVarPtr(name, *type.d_typeNode); Debug("nm") << "set " << name << " on " << *n << std::endl; @@ -703,7 +704,8 @@ Expr ExprManager::mkBoundVar(const std::string& name, Type type) { return Expr(this, n); } -Expr ExprManager::mkBoundVar(Type type) { +Expr ExprManager::mkBoundVar(Type type) +{ NodeManagerScope nms(d_nodeManager); INC_STAT_VAR(type, true); return Expr(this, d_nodeManager->mkBoundVarPtr(*type.d_typeNode)); |