diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-06-19 11:09:49 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-06-19 11:09:49 -0400 |
| commit | 010ad47b7b3e1909f31525fc45be2c27c1b72e45 (patch) | |
| tree | b18bf9b0724c6418dc57bf0d15a9db351f6f252e /src/parser/parser.h | |
| parent | c5177b11ad8cc5287fa7a8e65f78d5f6cfe23ead (diff) | |
Give a more useful parse error message for "undeclared variable -1".
Indeed, "-1" is a valid user symbol in SMT-LIB; this commit makes a small
change to the parser to detect when something like "-1" is used but
undeclared, and adds a note to the error message giving the syntax for
unary minus.
Diffstat (limited to 'src/parser/parser.h')
| -rw-r--r-- | src/parser/parser.h | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/parser/parser.h b/src/parser/parser.h index b4e79b427..883f1f12b 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -312,7 +312,8 @@ public: * @throws ParserException if checks are enabled and the check fails */ void checkDeclaration(const std::string& name, DeclarationCheck check, - SymbolType type = SYM_VARIABLE) throw(ParserException); + SymbolType type = SYM_VARIABLE, + std::string notes = "") throw(ParserException); /** * Reserve a symbol at the assertion level. |