Fixing SmtEngine::getValue() by adding a NodeManagerScope (thanks Tim for finding...

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 376a8a531647e94f5a32605b67f3801cc6c85794..c28ee7064ce3c6fe4564f89b00ccad5294fadb7f 100644 (file)
--- 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) {