fix was compiler warning in antlr_input, crashing test case with the old fix

diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index 88b43eb0e513d093058fe38690d8e95aa03ea325..ee4e2ff37af09235fa69ee060bdeb7ddce8ce130 100644 (file)
--- 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 f16e18bdfef270f2c5ffe911622198aa533b10cf..521993db3b1c5a5afb471c44ad4716776edfd16e 100644 (file)
--- 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 (file)
index 0000000..59d5b20
--- /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))