diff options
| -rw-r--r-- | src/parser/antlr_input.cpp | 8 | ||||
| -rw-r--r-- | test/regress/regress0/Makefile.am | 2 | ||||
| -rw-r--r-- | test/regress/regress0/errorcrash.smt2 | 9 |
3 files changed, 15 insertions, 4 deletions
diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp index 88b43eb0e..ee4e2ff37 100644 --- a/src/parser/antlr_input.cpp +++ b/src/parser/antlr_input.cpp @@ -374,9 +374,9 @@ std::string parseErrorHelper(const char* lineStart, int charPositionInLine, cons string word = slice.substr(caretPos, (caretPosOrig - caretPos + 1)); int messagePosSt = message.find(word); int messagePosEn = messagePosSt + (caretPosOrig - caretPos); - if( messagePosSt < string::npos && + if( (size_t)messagePosSt < string::npos && (messagePosSt == 0 || !isSimpleChar(message[messagePosSt-1]) ) && - (messagePosEn+1 == message.size() || !isSimpleChar(message[messagePosEn+1]) ) ) { + ((size_t)messagePosEn+1 == message.size() || !isSimpleChar(message[messagePosEn+1]) ) ) { // ^the complicated if statement is just 'whole-word' match Debug("friendlyparser") << "[friendlyparser] Feeling good." << std::endl; } @@ -398,9 +398,9 @@ std::string parseErrorHelper(const char* lineStart, int charPositionInLine, cons Debug("friendlyparser") << "[friendlyparser] nearest word = " << word << std::endl; int messagePosSt = message.find(word); int messagePosEn = messagePosSt + (nearestWordEn - nearestWordSt + 1); - if( messagePosSt < string::npos && + if( (size_t)messagePosSt < string::npos && (messagePosSt == 0 || !isSimpleChar(message[messagePosSt-1]) ) && - (messagePosEn+1 == message.size() || !isSimpleChar(message[messagePosEn+1]) ) ) { + ((size_t)messagePosEn+1 == message.size() || !isSimpleChar(message[messagePosEn+1]) ) ) { // ^the complicated if statement is just 'whole-word' match Debug("friendlyparser") << "[friendlyparser] strong evidence that caret should be at " << nearestWordSt << std::endl; diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index f16e18bdf..521993db3 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -170,6 +170,7 @@ if CVC4_BUILD_PROFILE_COMPETITION else TESTS += \ error.cvc \ + errorcrash.smt2 \ arrayinuf_error.smt2 endif @@ -177,6 +178,7 @@ endif EXTRA_DIST += \ subranges.cvc \ arrayinuf_error.smt2 \ + errorcrash.smt2 \ error.cvc # synonyms for "check" in this directory diff --git a/test/regress/regress0/errorcrash.smt2 b/test/regress/regress0/errorcrash.smt2 new file mode 100644 index 000000000..59d5b2014 --- /dev/null +++ b/test/regress/regress0/errorcrash.smt2 @@ -0,0 +1,9 @@ +; EXIT: 1 +; EXPECT-ERROR: (error "Parse Error: errorcrash.smt2:5.29: Symbol 'Array' not declared as a type") +(set-logic QF_UF) +(declare-sort U 0) +(declare-fun x () (Array U U)) +(declare-fun y () (Array U U)) +(assert (= x y)) +(check-sat) +(get-value (x y)) |