From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 15 Mar 2021 23:09:16 +0000 (-0500)
Subject: Fix rewrite for double replace (#6152)
X-Git-Tag: cvc5-1.0.0~2073
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a6b7bb2502a969811f2e4b226c9ca631858ae42a;p=cvc5.git

Fix rewrite for double replace (#6152)

Fixes #6142.
---

diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp
index 869c40ad8..c54cdfb50 100644
--- a/src/theory/strings/sequences_rewriter.cpp
+++ b/src/theory/strings/sequences_rewriter.cpp
@@ -2862,7 +2862,7 @@ Node SequencesRewriter::rewriteReplace(Node node)
     {
       // str.contains( z, w ) ----> false implies
       // str.replace( x, w, str.replace( z, x, y ) ) ---> str.replace( x, w, z )
-      Node cmp_con2 = d_stringsEntail.checkContains(node[1], node[2][0]);
+      Node cmp_con2 = d_stringsEntail.checkContains(node[2][0], node[1]);
       if (!cmp_con2.isNull() && !cmp_con2.getConst<bool>())
       {
         Node res =
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 5c28a34cc..14752f726 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2036,6 +2036,7 @@ set(regress_1_tests
   regress1/strings/issue5940-skc-len-conc.smt2
   regress1/strings/issue5940-2-skc-len-conc.smt2
   regress1/strings/issue6075-repl-len-one-rr.smt2
+  regress1/strings/issue6142-repl-inv-rew.smt2
   regress1/strings/kaluza-fl.smt2
   regress1/strings/loop002.smt2
   regress1/strings/loop003.smt2
diff --git a/test/regress/regress1/strings/issue6142-repl-inv-rew.smt2 b/test/regress/regress1/strings/issue6142-repl-inv-rew.smt2
new file mode 100644
index 000000000..fdd4f0c78
--- /dev/null
+++ b/test/regress/regress1/strings/issue6142-repl-inv-rew.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun x () String)
+(declare-fun y () String)
+(assert (= (str.++ "A" y) (str.replace x (str.++ "A" y) (str.replace (str.++ "A" (str.replace y "" "A")) x "A"))))
+(check-sat)