From 37011fff190bd87adc9d501b6bda48942321aa6d Mon Sep 17 00:00:00 2001
From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Wed, 7 Jan 2015 10:50:58 -0600
Subject: [PATCH] bug fix, thanks to Pierre's report

---
 src/theory/strings/theory_strings_rewriter.cpp |  5 ++---
 test/regress/regress0/strings/Makefile.am      |  1 +
 test/regress/regress0/strings/bug002.smt2      | 10 ++++++++++
 3 files changed, 13 insertions(+), 3 deletions(-)
 create mode 100644 test/regress/regress0/strings/bug002.smt2

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 3e896c559..fb7c9b460 100644
--- 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 8a2674cee..414904919 100644
--- 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
index 000000000..15d1ea5a2
--- /dev/null
+++ b/test/regress/regress0/strings/bug002.smt2
@@ -0,0 +1,10 @@
+(set-logic ASLIA)
+(set-info :smt-lib-version 2.0)
+(set-option :strings-exp true)
+(set-info :status sat)
+
+; regex = [\*-,\t\*-\|](.{6,}()?)+
+(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 "") ) ) ) ) ) ) ) )  ) )
+(assert (not (strinre "6O\1\127\n?")))
+
+(check-sat)
\ No newline at end of file
-- 
2.30.2