From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Wed, 7 Jan 2015 18:24:14 +0000 (-0600)
Subject: patch to the last commit
X-Git-Tag: cvc5-1.0.0~6451
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=740bfad6ab2c3ac6c1f7eec9c8e6f5338abd8eb5;p=cvc5.git

patch to the last commit
---

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index fb7c9b460..9f6836406 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -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 - start; ++vec_k[i]) {
+            for(vec_k[i] = vec_k[i] + 1; vec_k[i] <= left; ++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;