diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-12-16 09:49:05 -0500 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-12-24 12:51:14 -0500 |
| commit | f42dcea977ed9180481cc842531e2c5372acbbe1 (patch) | |
| tree | 5812dccd63af6c73c4543026c3f2692c81de23ef | |
| parent | 4abb82936fbb1a297d0d5eb69f8dbdb4599a67f2 (diff) | |
Better get-value parse error message for common user error.
| -rw-r--r-- | src/parser/smt2/Smt2.g | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index e2e52b158..13850aba6 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -336,8 +336,10 @@ command returns [CVC4::Command* cmd = NULL] } | /* value query */ GET_VALUE_TOK { PARSER_STATE->checkThatLogicIsSet(); } - LPAREN_TOK termList[terms,expr] RPAREN_TOK - { $cmd = new GetValueCommand(terms); } + ( LPAREN_TOK termList[terms,expr] RPAREN_TOK + { $cmd = new GetValueCommand(terms); } + | term[expr, expr2] + { 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(); } { cmd = new GetAssignmentCommand(); } |