Fix extended equality rewrite involving replace. (#6104)

Fixes #6075.

diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp
index c5c60c2d26119e350fe8b21dfa30269403a1597e..b19e98bbdea787a317672ff8867ab22dd65008a3 100644 (file)
--- a/src/theory/strings/sequences_rewriter.cpp
+++ b/src/theory/strings/sequences_rewriter.cpp
@@ -309,7 +309,7 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node)
         }
 
         // (= "" (str.replace x "A" "")) ---> (str.prefix x "A")
-        if (StringsEntail::checkLengthOne(ne[1]) && ne[2] == empty)
+        if (StringsEntail::checkLengthOne(ne[1], true) && ne[2] == empty)
         {
           Node ret = nm->mkNode(STRING_PREFIX, ne[0], ne[1]);
           return returnRewrite(node, ret, Rewrite::STR_EMP_REPL_EMP);

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 14701910851bafbbe586c2047125dd85331248dd..30cdf43d9c31b54b0473a9adf87f6a27e7d8e717 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2033,6 +2033,7 @@ set(regress_1_tests
   regress1/strings/issue5692-infer-proxy.smt2
   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/kaluza-fl.smt2
   regress1/strings/loop002.smt2
   regress1/strings/loop003.smt2

diff --git a/test/regress/regress1/strings/issue6075-repl-len-one-rr.smt2 b/test/regress/regress1/strings/issue6075-repl-len-one-rr.smt2
new file mode 100644 (file)
index 0000000..f60fe91
--- /dev/null
+++ b/test/regress/regress1/strings/issue6075-repl-len-one-rr.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun x () String)
+(declare-fun y () String)
+(assert (str.< x (str.replace "" (str.++ (str.replace "B" x "")
+(str.replace "B" (str.replace "B" x "") "")) y)))
+(check-sat)