summaryrefslogtreecommitdiff
path: root/src/theory/strings
diff options
context:
space:
mode:
authorTianyi Liang <tianyi-liang@uiowa.edu>2015-01-07 12:24:14 -0600
committerTianyi Liang <tianyi-liang@uiowa.edu>2015-01-07 12:24:14 -0600
commit740bfad6ab2c3ac6c1f7eec9c8e6f5338abd8eb5 (patch)
tree257eda637a6d116fb91ca4ba10968436e1a49387 /src/theory/strings
parent37011fff190bd87adc9d501b6bda48942321aa6d (diff)
patch to the last commit
Diffstat (limited to 'src/theory/strings')
-rw-r--r--src/theory/strings/theory_strings_rewriter.cpp2
1 files changed, 1 insertions, 1 deletions
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback