bug fix, thanks to Pierre's report

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 3e896c559af25ed563d9c238666f299db1ba409e..fb7c9b460b3352441137bece3f47c3a236a95629 100644 (file)
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -654,7 +654,7 @@ bool TheoryStringsRewriter::testConstStringInRegExp( CVC4::String &s, unsigned i
       if( s.size() != index_start ) {
         std::vector<int> vec_k( r.getNumChildren(), -1 );
         int start = 0;
-        int left = (int) s.size();
+        int left = (int) s.size() - index_start;
         int i=0;
         while( i<(int) r.getNumChildren() ) {
           bool flag = true;
@@ -665,7 +665,7 @@ bool TheoryStringsRewriter::testConstStringInRegExp( CVC4::String &s, unsigned i
           } else if( i == -1 ) {
             return false;
           } else {
-            for(vec_k[i] = vec_k[i] + 1; vec_k[i] <= left; ++vec_k[i]) {
+            for(vec_k[i] = vec_k[i] + 1; vec_k[i] <= left - start; ++vec_k[i]) {
               CVC4::String t = s.substr(index_start + start, vec_k[i]);
               if( testConstStringInRegExp( t, 0, r[i] ) ) {
                 start += vec_k[i]; left -= vec_k[i]; flag = false;
@@ -739,7 +739,6 @@ bool TheoryStringsRewriter::testConstStringInRegExp( CVC4::String &s, unsigned i
     }
     default: {
       Trace("strings-error") << "Unsupported term: " << r << " in testConstStringInRegExp." << std::endl;
-      //Assert( false, "Unsupported Term" );
       Unreachable();
       return false;
     }

diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am
index 8a2674ceebe960121a6f65d01721c75b2c6bb3a6..4149049194d6359ddba4b96c85ddee7fb311ce6e 100644 (file)
--- a/test/regress/regress0/strings/Makefile.am
+++ b/test/regress/regress0/strings/Makefile.am
@@ -21,6 +21,7 @@ MAKEFLAGS = -k
 TESTS =        \
   at001.smt2 \
   bug001.smt2 \
+  bug002.smt2 \
   cardinality.smt2 \
   escchar.smt2 \
   escchar_25.smt2 \

diff --git a/test/regress/regress0/strings/bug002.smt2 b/test/regress/regress0/strings/bug002.smt2
new file mode 100644 (file)
index 0000000..15d1ea5
--- /dev/null
+++ b/test/regress/regress0/strings/bug002.smt2
@@ -0,0 +1,10 @@
+(set-logic ASLIA)\r
+(set-info :smt-lib-version 2.0)\r
+(set-option :strings-exp true)\r
+(set-info :status sat)\r
+\r
+; regex = [\*-,\t\*-\|](.{6,}()?)+\r
+(define-fun strinre ((?s String)) Bool (str.in.re ?s (re.union re.nostr (re.++ (str.to.re "") (str.to.re "") (re.union re.nostr (re.range "*" ",") (str.to.re "\t") (re.range "*" "|") ) (re.+ (re.union re.nostr (re.++ (str.to.re "") (str.to.re "") (re.loop re.allchar 6 ) (re.opt (re.union re.nostr (re.++ (str.to.re "") (str.to.re "") ) ) ) ) ) ) ) )  ) )\r
+(assert (not (strinre "6O\1\127\n?")))\r
+\r
+(check-sat)
\ No newline at end of file