From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Sat, 5 Jun 2021 03:22:57 +0000 (-0700)
Subject: Remove unwanted side effects in `SPLIT_EQ_STRIP_L` (#6689)
X-Git-Tag: cvc5-1.0.0~1638
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f7b60f68bb6a7945eebb7f97a5f63302ad0ddc67;p=cvc5.git

Remove unwanted side effects in `SPLIT_EQ_STRIP_L` (#6689)

Fixes #6681. When checking whether SPLIT_EQ_STRIP_L applies, we were
using sripSymbolicLength, which changes its inputs depending on how
many elements of the concatenation it could strip. However, one of the
arguments, pfxv0, was reused across multiple checks if the strip did
not result in a rewrite. Later invocations were wrong as a result. This
commit changes the call to stripSymbolicLength() to use a new copy of
the vector instead.
---

diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp
index 7ef1242c6..f63b416ff 100644
--- a/src/theory/strings/sequences_rewriter.cpp
+++ b/src/theory/strings/sequences_rewriter.cpp
@@ -437,7 +437,7 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node)
     size_t startRhs = 0;
     for (size_t i = 0, size0 = v0.size(); i <= size0; i++)
     {
-      std::vector<Node> pfxv0(v0.begin(), v0.begin() + i);
+      const std::vector<Node> pfxv0(v0.begin(), v0.begin() + i);
       Node pfx0 = utils::mkConcat(pfxv0, stype);
       for (size_t j = startRhs, size1 = v1.size(); j <= size1; j++)
       {
@@ -502,21 +502,22 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node)
             // Example:
             // (= (str.++ x "AB" z) (str.++ "A" x y)) --->
             //   (and (= (str.++ x "A") (str.++ "A" x)) (= (str.++ "B" z) y))
+            std::vector<Node> sfxv0 = pfxv0;
             std::vector<Node> rpfxv0;
             if (StringsEntail::stripSymbolicLength(
-                    pfxv0, rpfxv0, 1, lenPfx1, true))
+                    sfxv0, rpfxv0, 1, lenPfx1, true))
             {
               // The rewrite requires the full right-hand prefix length to be
               // stripped (otherwise we would have to keep parts of the
               // right-hand prefix).
               if (lenPfx1.isConst() && lenPfx1.getConst<Rational>().isZero())
               {
-                pfxv0.insert(pfxv0.end(), v0.begin() + i, v0.end());
+                sfxv0.insert(sfxv0.end(), v0.begin() + i, v0.end());
                 std::vector<Node> sfxv1(v1.begin() + j, v1.end());
                 Node ret =
                     nm->mkNode(kind::AND,
                                utils::mkConcat(rpfxv0, stype).eqNode(pfx1),
-                               utils::mkConcat(pfxv0, stype)
+                               utils::mkConcat(sfxv0, stype)
                                    .eqNode(utils::mkConcat(sfxv1, stype)));
                 return returnRewrite(node, ret, Rewrite::SPLIT_EQ_STRIP_L);
               }
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 707e5e43d..237ca77dd 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1156,6 +1156,7 @@ set(regress_0_tests
   regress0/strings/issue6560-indexof-reduction.smt2
   regress0/strings/issue6604-re-elim.smt2
   regress0/strings/issue6643-ctn-decompose-conflict.smt2
+  regress0/strings/issue6681-split-eq-strip-l.smt2
   regress0/strings/itos-entail.smt2
   regress0/strings/large-model.smt2
   regress0/strings/leadingzero001.smt2
diff --git a/test/regress/regress0/strings/issue6681-split-eq-strip-l.smt2 b/test/regress/regress0/strings/issue6681-split-eq-strip-l.smt2
new file mode 100644
index 000000000..213d9737b
--- /dev/null
+++ b/test/regress/regress0/strings/issue6681-split-eq-strip-l.smt2
@@ -0,0 +1,8 @@
+(set-logic QF_SLIA)
+(declare-fun a () String)
+(declare-fun b () String)
+(declare-fun c () String)
+(declare-fun d () String)
+(assert (= (str.++ "A" a "CBA" b "BA" d) (str.++ b "BA" d a "CBA" c)))
+(set-info :status sat)
+(check-sat)