diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-08-24 00:29:52 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-08-24 00:29:52 +0000 |
commit | 9de66957df6448ba1243cdb7cc84813fe82e69d5 (patch) | |
tree | 9c013455d7f0c0e057f44f51abdead7ff1ebd01c /src/parser | |
parent | 23367b1eac54a17a060697b1cf187ad2cc2ff503 (diff) |
fix get-value output in a couple ways; this fixes bug #378
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/smt2/Smt2.g | 14 |
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; } |