From: Morgan Deters <mdeters@gmail.com>
Date: Fri, 22 Apr 2011 22:02:46 +0000 (+0000)
Subject: fix to last commit
X-Git-Tag: cvc5-1.0.0~8581
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3558673ff03c3d5fb05ac714e30f35e45aed3af3;p=cvc5.git

fix to last commit
---

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index c28ee7064..f98d60702 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -618,7 +618,6 @@ Expr SmtEngine::getValue(const Expr& e)
     throw ModalException(msg);
   }
 
-  NodeManagerScope nms(d_nodeManager);
   Node eNode = e.getNode();
   Node n = smt::SmtEnginePrivate::preprocess(*this, eNode);
 
@@ -710,6 +709,7 @@ SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) {
 
 vector<Expr> SmtEngine::getAssertions()
   throw(ModalException, AssertionException) {
+  NodeManagerScope nms(d_nodeManager);
   Debug("smt") << "SMT getAssertions()" << endl;
   if(!Options::current()->interactive) {
     const char* msg =