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 5ba9d6e3f39cf63a3e150626625d7d941df39676..e94a23c87a5dea2a5ce53b853beef3fea9f857a8 100644 (file)
--- 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 0313f0b13939dd32e3037a148f29efb2bbbb11d8..5304fcab53d8beff76d14cb4573aeadcaa1bea2d 100644 (file)
--- 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 (file)
index 0000000..02e4cc0
--- /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 87aef3704e1ad9de3b3145ab7166e2d622a951db..42ac2cdd9d080f88a614ce1edc2dc166fd97c1e8 100644 (file)
--- 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()