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.

1 files changed, 6 insertions, 3 deletions

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index fa2a1e744..a7834a5aa 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -374,7 +374,8 @@ void Parser::reserveSymbolAtAssertionLevel(const std::string& varName) {
 
 void Parser::checkDeclaration(const std::string& varName,
                               DeclarationCheck check,
-                              SymbolType type)
+                              SymbolType type,
+                              std::string notes)
     throw(ParserException) {
   if(!d_checksEnabled) {
     return;
@@ -384,14 +385,16 @@ void Parser::checkDeclaration(const std::string& varName,
   case CHECK_DECLARED:
     if( !isDeclared(varName, type) ) {
       parseError("Symbol " + varName + " not declared as a " +
-                 (type == SYM_VARIABLE ? "variable" : "type"));
+                 (type == SYM_VARIABLE ? "variable" : "type") +
+                 (notes.size() == 0 ? notes : "\n" + notes));
     }
     break;
 
   case CHECK_UNDECLARED:
     if( isDeclared(varName, type) ) {
       parseError("Symbol " + varName + " previously declared as a " +
-                 (type == SYM_VARIABLE ? "variable" : "type"));
+                 (type == SYM_VARIABLE ? "variable" : "type") +
+                 (notes.size() == 0 ? notes : "\n" + notes));
     }
     break;