From 9fa66413709fbdb1a02f8986d0c332934523b110 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 19 Jul 2019 09:36:53 -0400
Subject: [PATCH] Fix case of unfolding negative membership in reg exp
 concatenation (#3101)

---
 src/theory/strings/regexp_operation.cpp        | 18 +++++++++++-------
 src/theory/strings/regexp_solver.cpp           |  1 -
 test/regress/CMakeLists.txt                    |  1 +
 .../regress1/strings/re-neg-unfold-rev-a.smt2  | 10 ++++++++++
 4 files changed, 22 insertions(+), 8 deletions(-)
 create mode 100644 test/regress/regress1/strings/re-neg-unfold-rev-a.smt2

diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index 0360228c6..0d422e823 100644
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -850,14 +850,18 @@ void RegExpOpr::simplifyNRegExp( Node s, Node r, std::vector< Node > &new_nodes
         {
           b1 = reLength;
         }
-        Node s1 = nm->mkNode(STRING_SUBSTR, s, d_zero, b1);
-        Node s2 = nm->mkNode(STRING_SUBSTR, s, b1, nm->mkNode(MINUS, lens, b1));
-        if (indexRm != 0)
+        Node s1;
+        Node s2;
+        if (indexRm == 0)
         {
-          // swap if we are removing from the end
-          Node sswap = s1;
-          s1 = s2;
-          s2 = sswap;
+          s1 = nm->mkNode(STRING_SUBSTR, s, d_zero, b1);
+          s2 = nm->mkNode(STRING_SUBSTR, s, b1, nm->mkNode(MINUS, lens, b1));
+        }
+        else
+        {
+          s1 = nm->mkNode(STRING_SUBSTR, s, nm->mkNode(MINUS, lens, b1), b1);
+          s2 =
+              nm->mkNode(STRING_SUBSTR, s, d_zero, nm->mkNode(MINUS, lens, b1));
         }
         Node s1r1 = nm->mkNode(STRING_IN_REGEXP, s1, r[indexRm]).negate();
         std::vector<Node> nvec;
diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp
index 5079806ac..65d616c3c 100644
--- a/src/theory/strings/regexp_solver.cpp
+++ b/src/theory/strings/regexp_solver.cpp
@@ -281,7 +281,6 @@ void RegExpSolver::check()
           std::vector<Node> exp_n;
           exp_n.push_back(assertion);
           Node conc = nvec.size() == 1 ? nvec[0] : nm->mkNode(AND, nvec);
-          conc = Rewriter::rewrite(conc);
           d_im.sendInference(rnfexp, exp_n, conc, "REGEXP_Unfold");
           addedLemma = true;
           if (changed)
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index aae919a2f..af6a9b839 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1580,6 +1580,7 @@ set(regress_1_tests
   regress1/strings/re-agg-total2.smt2
   regress1/strings/re-elim-exact.smt2
   regress1/strings/re-neg-concat-reduct.smt2
+  regress1/strings/re-neg-unfold-rev-a.smt2
   regress1/strings/re-unsound-080718.smt2
   regress1/strings/regexp001.smt2
   regress1/strings/regexp002.smt2
diff --git a/test/regress/regress1/strings/re-neg-unfold-rev-a.smt2 b/test/regress/regress1/strings/re-neg-unfold-rev-a.smt2
new file mode 100644
index 000000000..3f99f8507
--- /dev/null
+++ b/test/regress/regress1/strings/re-neg-unfold-rev-a.smt2
@@ -0,0 +1,10 @@
+(set-info :smt-lib-version 2.5)
+(set-logic QF_S)
+(set-info :status unsat)
+(set-option :strings-exp true)
+
+(declare-const x String)
+(declare-const y String)
+(assert (and (= y "foobar") (str.in.re x (re.++ (str.to.re "ab") (re.* re.allchar) (str.to.re "b") (re.* re.allchar) (str.to.re "b") (re.* re.allchar) (str.to.re "b")))))
+(assert (not (and (= y "foobar") (str.in.re x (re.++ (str.to.re "a") (re.* re.allchar) (str.to.re "b") (re.* re.allchar) (str.to.re "b") (re.* re.allchar) (str.to.re "b"))))))
+(check-sat)
-- 
2.30.2