From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 7 Jan 2020 20:22:32 +0000 (-0600)
Subject: Fix unary minus parse check (#3594)
X-Git-Tag: cvc5-1.0.0~3745
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b38ffa21717d220e98581854e2af1ee9d13ce5b7;p=cvc5.git

Fix unary minus parse check (#3594)
---

diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index efdb0c70f..4f0935916 100644
--- 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)