From: Morgan Deters <mdeters@gmail.com>
Date: Fri, 22 Apr 2011 22:01:36 +0000 (+0000)
Subject: Fixing SmtEngine::getValue() by adding a NodeManagerScope (thanks Tim for finding... 
X-Git-Tag: cvc5-1.0.0~8582
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2a57acc989a917a58dbecb2944c8438140a5627c;p=cvc5.git

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

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) {