From fc76056f4ac7f049fc62d3c1de91e44fb58ab2e1 Mon Sep 17 00:00:00 2001
From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Fri, 25 Jul 2014 15:43:16 -0500
Subject: [PATCH] bug fix for pierre 0717

---
 src/theory/strings/theory_strings_rewriter.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

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;
-- 
2.30.2