diff options
-rw-r--r-- | src/parser/smt2/smt2.h | 27 |
1 files changed, 11 insertions, 16 deletions
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) |