From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Fri, 25 Jul 2014 20:43:16 +0000 (-0500)
Subject: bug fix for pierre 0717
X-Git-Tag: cvc5-1.0.0~6685
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fc76056f4ac7f049fc62d3c1de91e44fb58ab2e1;p=cvc5.git

bug fix for pierre 0717
---

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;