From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 17 May 2013 14:38:03 +0000 (-0400)
Subject: Fix destruction issue in GetValueCommand leading to crash.
X-Git-Tag: cvc5-1.0.0~7287^2~33^2~20
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6f0bdcf8dc8cbe2090c337aedb700571873b9a49;p=cvc5.git

Fix destruction issue in GetValueCommand leading to crash.

Thanks to David Cok for reporting this.
---

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());