From 2a57acc989a917a58dbecb2944c8438140a5627c Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 22 Apr 2011 22:01:36 +0000 Subject: [PATCH] Fixing SmtEngine::getValue() by adding a NodeManagerScope (thanks Tim for finding this) --- src/smt/smt_engine.cpp | 1 + 1 file changed, 1 insertion(+) 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) { -- 2.30.2