Fix destruction issue in GetValueCommand leading to crash.

Thanks to David Cok for reporting this.

1 files changed, 5 insertions, 5 deletions

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 593f84ced..36336a959 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -795,17 +795,17 @@ const std::vector<Expr>& GetValueCommand::getTerms() const throw() {
 
 void GetValueCommand::invoke(SmtEngine* smtEngine) throw() {
   try {
-    vector<Node> result;
-    NodeManager* nm = NodeManager::fromExprManager(smtEngine->getExprManager());
+    vector<Expr> result;
+    ExprManager* em = smtEngine->getExprManager();
+    NodeManager* nm = NodeManager::fromExprManager(em);
     for(std::vector<Expr>::const_iterator i = d_terms.begin(); i != d_terms.end(); ++i) {
       Assert(nm == NodeManager::fromExprManager((*i).getExprManager()));
       smt::SmtScope scope(smtEngine);
       Node request = Node::fromExpr(options::expandDefinitions() ? smtEngine->expandDefinitions(*i) : *i);
       Node value = Node::fromExpr(smtEngine->getValue(*i));
-      result.push_back(nm->mkNode(kind::SEXPR, request, value));
+      result.push_back(nm->mkNode(kind::SEXPR, request, value).toExpr());
     }
-    Node n = nm->mkNode(kind::SEXPR, result);
-    d_result = nm->toExpr(n);
+    d_result = em->mkExpr(kind::SEXPR, result);
     d_commandStatus = CommandSuccess::instance();
   } catch(exception& e) {
     d_commandStatus = new CommandFailure(e.what());