summaryrefslogtreecommitdiff
path: root/src/parser/smt2/Smt2.g
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser/smt2/Smt2.g')
-rw-r--r--src/parser/smt2/Smt2.g14
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; }
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback