diff options
| -rw-r--r-- | src/smt/smt_engine.cpp | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 376a8a531..c28ee7064 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -596,6 +596,7 @@ Expr SmtEngine::simplify(const Expr& e) { Expr SmtEngine::getValue(const Expr& e) throw(ModalException, AssertionException) { Assert(e.getExprManager() == d_exprManager); + NodeManagerScope nms(d_nodeManager); Type type = e.getType(Options::current()->typeChecking);// ensure expr is type-checked at this point Debug("smt") << "SMT getValue(" << e << ")" << endl; if(!Options::current()->produceModels) { |