From: Morgan Deters <mdeters@gmail.com>
Date: Tue, 26 Oct 2010 19:24:09 +0000 (+0000)
Subject: GetValueCommand now gives a TUPLE as output, with the first operand the input express... 
X-Git-Tag: cvc5-1.0.0~8776
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=118b6163f42af017a5ea7f9229df0a9e584c0050;p=cvc5.git

GetValueCommand now gives a TUPLE as output, with the first operand the input expression and the second the value (resolves bug 227)
---

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 38193a75b..60b48542b 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -269,7 +269,8 @@ GetValueCommand::GetValueCommand(Expr term) :
 }
 
 void GetValueCommand::invoke(SmtEngine* smtEngine) {
-  d_result = smtEngine->getValue(d_term);
+  d_result = d_term.getExprManager()->mkExpr(kind::TUPLE, d_term,
+                                             smtEngine->getValue(d_term));
 }
 
 Expr GetValueCommand::getResult() const {