fix get-value output in a couple ways; this fixes bug #378

1 files changed, 1 insertions, 13 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index dd0ccb0ad..456e3c656 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -283,19 +283,7 @@ command returns [CVC4::Command* cmd = NULL]
   | /* value query */
     GET_VALUE_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     LPAREN_TOK termList[terms,expr] RPAREN_TOK
-    { if(terms.size() == 1) {
-        $cmd = new GetValueCommand(terms[0]);
-      } else {
-        CommandSequence* seq = new CommandSequence();
-        for(std::vector<Expr>::const_iterator i = terms.begin(),
-              iend = terms.end();
-            i != iend;
-            ++i) {
-          seq->addCommand(new GetValueCommand(*i));
-        }
-        $cmd = seq;
-      }
-    }
+    { $cmd = new GetValueCommand(terms); }
   | /* get-assignment */
     GET_ASSIGNMENT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     { cmd = new GetAssignmentCommand; }