summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
authorTianyi Liang <tianyi-liang@uiowa.edu>2014-07-25 15:43:16 -0500
committerTianyi Liang <tianyi-liang@uiowa.edu>2014-07-25 15:43:16 -0500
commitfc76056f4ac7f049fc62d3c1de91e44fb58ab2e1 (patch)
tree98600151c2cfd55058b5b9af752d40a337676cfb /src/theory
parent215b2b1e8435703f513bcdd02082cd485f2e4bf9 (diff)
bug fix for pierre 0717
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/strings/theory_strings_rewriter.cpp3
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback