Fix unary minus parse check (#3594)

diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index efdb0c70f6b21aa0f306a8f305902ebc70210d68..4f09359166982201110a23a3645e0d481cf4f30e 100644 (file)
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -450,26 +450,21 @@ class Smt2 : public Parser
   {
     // if the symbol is something like "-1", we'll give the user a helpful
     // syntax hint.  (-1 is a valid identifier in SMT-LIB, NOT unary minus.)
-    if( check != CHECK_DECLARED ||
-        name[0] != '-' ||
-        name.find_first_not_of("0123456789", 1) != std::string::npos ) {
-      this->Parser::checkDeclaration(name, check, type, notes);
-      return;
-    }else{
-      //it is allowable in sygus
-      if (sygus_v1() && name[0] == '-')
+    if (name.length() > 1 && name[0] == '-'
+        && name.find_first_not_of("0123456789", 1) == std::string::npos)
+    {
+      if (sygus_v1())
       {
-        //do not check anything
+        // "-1" is allowed in SyGuS version 1.0
         return;
       }
+      std::stringstream ss;
+      ss << notes << "You may have intended to apply unary minus: `(- "
+         << name.substr(1) << ")'\n";
+      this->Parser::checkDeclaration(name, check, type, ss.str());
+      return;
     }
-
-    std::stringstream ss;
-    ss << notes
-       << "You may have intended to apply unary minus: `(- "
-       << name.substr(1)
-       << ")'\n";
-    this->Parser::checkDeclaration(name, check, type, ss.str());
+    this->Parser::checkDeclaration(name, check, type, notes);
   }
 
   void checkOperator(Kind kind, unsigned numArgs)