diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-12-27 12:21:25 -0500 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-12-27 12:21:25 -0500 |
| commit | 76897e049175f7c42c36ddc6375fc52d8dcdf54d (patch) | |
| tree | f16222f9af14dcd335731aff9e9bfdd571b32df5 | |
| parent | cac85606876d4f0be1c6c54172f7509ce54cdcb5 (diff) | |
| parent | 4b75a8f448288f416dcfeb5672c915c7add877da (diff) | |
Merge branch '1.3.x'
| -rw-r--r-- | src/parser/smt2/Smt2.g | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index b1e37f85e..be8bddcb2 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -338,7 +338,7 @@ command returns [CVC4::Command* cmd = NULL] GET_VALUE_TOK { PARSER_STATE->checkThatLogicIsSet(); } ( LPAREN_TOK termList[terms,expr] RPAREN_TOK { $cmd = new GetValueCommand(terms); } - | term[expr, expr2] + | ~LPAREN_TOK { PARSER_STATE->parseError("The get-value command expects a list of terms. Perhaps you forgot a pair of parentheses?"); } ) | /* get-assignment */ GET_ASSIGNMENT_TOK { PARSER_STATE->checkThatLogicIsSet(); } |