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 869c40ad8a2f72acb5e4cc0f519cde237ef1b72d..c54cdfb50e202460057589ca514d5326d96b6c57 100644 (file)
--- 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 5c28a34cc9fb2bcf68ba068b4ac2983c0f9a983f..14752f72639feb890e30be8bb267a4cd66e02c43 100644 (file)
--- 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 (file)
index 0000000..fdd4f0c
--- /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)