GetValueCommand now gives a TUPLE as output, with the first operand the input express...

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 38193a75bb501c68c5288d250737730c92fe0c64..60b48542bfbb3d895c3b892e4811486a1c75d027 100644 (file)
--- 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 {