diff options
author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-07-25 15:43:16 -0500 |
---|---|---|
committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-07-25 15:43:16 -0500 |
commit | fc76056f4ac7f049fc62d3c1de91e44fb58ab2e1 (patch) | |
tree | 98600151c2cfd55058b5b9af752d40a337676cfb | |
parent | 215b2b1e8435703f513bcdd02082cd485f2e4bf9 (diff) |
bug fix for pierre 0717
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index ca45cd794..e37cabfb6 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -204,6 +204,7 @@ bool TheoryStringsRewriter::checkConstRegExp( TNode t ) { bool TheoryStringsRewriter::testConstStringInRegExp( CVC4::String &s, unsigned int index_start, TNode r ) { Assert( index_start <= s.size() ); + Trace("regexp-debug") << "Checking " << s << " in " << r << ", starting at " << index_start << std::endl; int k = r.getKind(); switch( k ) { case kind::STRING_TO_REGEXP: { @@ -282,7 +283,7 @@ bool TheoryStringsRewriter::testConstStringInRegExp( CVC4::String &s, unsigned i return false; } case kind::REGEXP_SIGMA: { - if(s.size() == 1) { + if(s.size() == index_start + 1) { return true; } else { return false; |