Fix simple reg exp consume rewrite (#2281)

3 files changed, 33 insertions, 2 deletions

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index fe92dd8ff..10bce3a29 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -983,12 +983,23 @@ Node TheoryStringsRewriter::rewriteMembership(TNode node) {
         return scn;
       }else{
         if( (children.size() + mchildren.size())!=prevSize ){
+          // Given a membership (str.++ x1 ... xn) in (re.++ r1 ... rm),
+          // above, we strip components to construct an equivalent membership:
+          // (str.++ xi .. xj) in (re.++ rk ... rl).
+          Node xn = mkConcat(kind::STRING_CONCAT, mchildren);
+          Node emptyStr = nm->mkConst(String(""));
           if( children.empty() ){
-            retNode = NodeManager::currentNM()->mkConst( mchildren.empty() );
+            // If we stripped all components on the right, then the left is
+            // equal to the empty string.
+            // e.g. (str.++ "a" x) in (re.++ (str.to.re "a")) ---> (= x "")
+            retNode = xn.eqNode(emptyStr);
           }else{
-            retNode = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, mkConcat( kind::STRING_CONCAT, mchildren ), mkConcat( kind::REGEXP_CONCAT, children ) );
+            // otherwise, construct the updated regular expression
+            retNode = nm->mkNode(
+                STRING_IN_REGEXP, xn, mkConcat(REGEXP_CONCAT, children));
           }
           Trace("regexp-ext-rewrite") << "Regexp : rewrite : " << node << " -> " << retNode << std::endl;
+          return returnRewrite(node, retNode, "re-simple-consume");
         }
       }
     }
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 2be59087b..0724fc163 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -1473,6 +1473,7 @@ REG1_TESTS = \
 	regress1/strings/norn-nel-bug-052116.smt2 \
 	regress1/strings/norn-simp-rew-sat.smt2 \
 	regress1/strings/pierre150331.smt2 \
+	regress1/strings/re-unsound-080718.smt2 \
 	regress1/strings/regexp001.smt2 \
 	regress1/strings/regexp002.smt2 \
 	regress1/strings/regexp003.smt2 \
diff --git a/test/regress/regress1/strings/re-unsound-080718.smt2 b/test/regress/regress1/strings/re-unsound-080718.smt2
new file mode 100644
index 000000000..96353e746
--- /dev/null
+++ b/test/regress/regress1/strings/re-unsound-080718.smt2
@@ -0,0 +1,19 @@
+; COMMAND-LINE: --strings-print-ascii --strings-exp
+; EXPECT: sat
+(set-info :smt-lib-version 2.5)
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun x () String)
+(assert
+(and 
+(not (= 
+  (str.in.re x (re.++ (str.to.re "B") (re.* (str.to.re "B")))) 
+  (str.in.re x (re.++ (str.to.re "B") (str.to.re (str.++ "B" "B"))))
+)) 
+(not (= 
+  (str.in.re x (re.++ (re.union (re.++ (str.to.re "A") re.allchar ) re.allchar ) (str.to.re "B"))) 
+  (str.in.re x (re.++ (str.to.re "A") (str.to.re "B")))
+))
+)
+)
+(check-sat)