From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Wed, 7 Nov 2018 18:28:25 +0000 (-0800)
Subject: Fix collectEmptyEqs in string rewriter (#2692)
X-Git-Tag: cvc5-1.0.0~4371
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=58ac30a778baf698603af98ff01aa8c17d430b32;p=cvc5.git

Fix collectEmptyEqs in string rewriter (#2692)
---

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 5ba9d6e3f..e94a23c87 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -4948,7 +4948,7 @@ std::pair<bool, std::vector<Node> > TheoryStringsRewriter::collectEmptyEqs(
       allEmptyEqs = false;
     }
   }
-  else
+  else if (x.getKind() == kind::AND)
   {
     for (const Node& c : x)
     {
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 0313f0b13..5304fcab5 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -839,6 +839,7 @@ set(regress_0_tests
   regress0/strings/substr-rewrites.smt2
   regress0/strings/type001.smt2
   regress0/strings/unsound-0908.smt2
+  regress0/strings/unsound-repl-rewrite.smt2
   regress0/sygus/General_plus10.sy
   regress0/sygus/aig-si.sy
   regress0/sygus/c100.sy
diff --git a/test/regress/regress0/strings/unsound-repl-rewrite.smt2 b/test/regress/regress0/strings/unsound-repl-rewrite.smt2
new file mode 100644
index 000000000..02e4cc0b2
--- /dev/null
+++ b/test/regress/regress0/strings/unsound-repl-rewrite.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: sat
+(set-logic QF_S)
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () Int)
+(assert (not (= (str.replace "B" (str.replace "" x "A") "B") (str.replace "B" x "B"))))
+(check-sat)
diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h
index 87aef3704..42ac2cdd9 100644
--- a/test/unit/theory/theory_strings_rewriter_white.h
+++ b/test/unit/theory/theory_strings_rewriter_white.h
@@ -604,6 +604,18 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
                              b);
     repl = d_nm->mkNode(kind::STRING_STRREPL, b, x, b);
     sameNormalForm(repl_repl, repl);
+
+    // Different normal forms for:
+    //
+    // (str.replace "B" (str.replace "" x "A") "B")
+    //
+    // (str.replace "B" x "B")
+    repl_repl = d_nm->mkNode(kind::STRING_STRREPL,
+                             b,
+                             d_nm->mkNode(kind::STRING_STRREPL, empty, x, a),
+                             b);
+    repl = d_nm->mkNode(kind::STRING_STRREPL, b, x, b);
+    differentNormalForms(repl_repl, repl);
   }
 
   void testRewriteContains()