diff options
author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2015-01-07 10:50:58 -0600 |
---|---|---|
committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2015-01-07 10:50:58 -0600 |
commit | 37011fff190bd87adc9d501b6bda48942321aa6d (patch) | |
tree | 1d1f0a7b6d729b5ac46b9ad0bdcc808891ca9b41 /src/theory/strings | |
parent | b97e5f0d7a4d6b34d736b403e56188e977574fb2 (diff) |
bug fix, thanks to Pierre's report
Diffstat (limited to 'src/theory/strings')
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 5 |
1 files changed, 2 insertions, 3 deletions
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; } |