From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 10 Mar 2021 18:32:19 +0000 (-0600)
Subject: Fix extended equality rewrite involving replace. (#6104)
X-Git-Tag: cvc5-1.0.0~2117
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=132504c9f255fdb2c31b9a43bb3b9513db41afc1;p=cvc5.git

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 c5c60c2d2..b19e98bbd 100644
--- 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 147019108..30cdf43d9 100644
--- 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
index 000000000..f60fe9168
--- /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)