5 files changed, 90 insertions, 10 deletions
diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp
index 5a4a25e88..0c8d7c372 100644
--- a/src/theory/strings/theory_strings_utils.cpp
+++ b/src/theory/strings/theory_strings_utils.cpp
@@ -243,19 +243,21 @@ std::pair<bool, std::vector<Node> > collectEmptyEqs(Node x)
   {
     for (const Node& c : x)
     {
-      if (c.getKind() == EQUAL)
+      if (c.getKind() != EQUAL)
       {
-        if (Word::isEmpty(c[0]))
-        {
-          emptyNodes.insert(c[1]);
-        }
-        else if (Word::isEmpty(c[1]))
-        {
-          emptyNodes.insert(c[0]);
-        }
+        allEmptyEqs = false;
+        continue;
       }
-      else
+
+      if (Word::isEmpty(c[0]))
       {
+        emptyNodes.insert(c[1]);
+      }
+      else if (Word::isEmpty(c[1]))
+      {
+        emptyNodes.insert(c[0]);
+      }
+      else {
         allEmptyEqs = false;
       }
     }
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 5e9b38e8d..7358ecca4 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2410,6 +2410,7 @@ set(regress_2_tests
   regress2/strings/cmu-repl-len-nterm.smt2
   regress2/strings/issue3203.smt2
   regress2/strings/issue5381.smt2
+  regress2/strings/issue6483.smt2
   regress2/strings/issue918.smt2
   regress2/strings/non_termination_regular_expression6.smt2
   regress2/strings/range-perf.smt2
diff --git a/test/regress/regress2/strings/issue6483.smt2 b/test/regress/regress2/strings/issue6483.smt2
new file mode 100644
index 000000000..3ee748d27
--- /dev/null
+++ b/test/regress/regress2/strings/issue6483.smt2
@@ -0,0 +1,15 @@
+(set-logic QF_SLIA)
+(declare-fun a () String)
+(assert
+ (xor
+  (= (= (str.replace "B" (str.replace (str.++ (str.replace "B" a "B") a) "B" "") "B")
+      (str.replace "B" (str.replace "B" a (str.++ a "B")) a))
+   (not
+    (= (str.replace "B" (str.replace a "B" "") "B")
+     (str.replace "B" a (str.++ a "B")))))
+  (= (str.replace "B" a "")
+   (str.replace "B" a
+    (ite (not (= (str.replace "" (str.replace a "" a) "") "")) ""
+     (str.replace "" (str.replace a "B" "") "B"))))))
+(set-info :status unsat)
+(check-sat)
diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt
index d0c0e2bd2..9fb0e21f1 100644
--- a/test/unit/theory/CMakeLists.txt
+++ b/test/unit/theory/CMakeLists.txt
@@ -35,6 +35,7 @@ cvc5_add_unit_test_white(theory_quantifiers_bv_inverter_white theory)
 cvc5_add_unit_test_white(theory_sets_type_enumerator_white theory)
 cvc5_add_unit_test_white(theory_sets_type_rules_white theory)
 cvc5_add_unit_test_white(theory_strings_skolem_cache_black theory)
+cvc5_add_unit_test_white(theory_strings_utils_white theory)
 cvc5_add_unit_test_white(theory_strings_word_white theory)
 cvc5_add_unit_test_white(theory_white theory)
 cvc5_add_unit_test_white(type_enumerator_white theory)
diff --git a/test/unit/theory/theory_strings_utils_white.cpp b/test/unit/theory/theory_strings_utils_white.cpp
new file mode 100644
index 000000000..7fb5614cd
--- /dev/null
+++ b/test/unit/theory/theory_strings_utils_white.cpp
@@ -0,0 +1,61 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andres Noetzli
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Unit tests for the string utils 
+ */
+
+#include <vector>
+#include <unordered_set>
+
+#include "expr/node.h"
+#include "test_node.h"
+#include "theory/strings/theory_strings_utils.h"
+
+namespace cvc5 {
+
+using namespace kind;
+using namespace theory;
+using namespace theory::strings;
+
+namespace test {
+
+class TestTheoryWhiteStringsUtils : public TestNode
+{
+};
+
+TEST_F(TestTheoryWhiteStringsUtils, collect_empty_eqs)
+{
+  TypeNode strType = d_nodeManager->stringType();
+
+  Node empty = d_nodeManager->mkConst(String(""));
+  Node a = d_nodeManager->mkConst(::cvc5::String("A"));
+  Node x = d_nodeManager->mkVar("x", strType);
+
+  Node emptyEqX = empty.eqNode(x);
+  Node emptyEqA = a.eqNode(empty);
+  Node xEqA = x.eqNode(a);
+
+  std::vector<Node> emptyNodes;
+  bool allEmptyEqs;
+  std::unordered_set<Node> expected = {a, x};
+
+  std::tie(allEmptyEqs, emptyNodes) = utils::collectEmptyEqs(d_nodeManager->mkNode(AND, emptyEqX, emptyEqA));
+  ASSERT_TRUE(allEmptyEqs);
+  ASSERT_EQ(std::unordered_set<Node>(emptyNodes.begin(), emptyNodes.end()), expected);
+
+  std::tie(allEmptyEqs, emptyNodes) = utils::collectEmptyEqs(d_nodeManager->mkNode(AND, emptyEqX, xEqA, emptyEqA));
+  ASSERT_FALSE(allEmptyEqs);
+  ASSERT_EQ(std::unordered_set<Node>(emptyNodes.begin(), emptyNodes.end()), expected);
+}
+
+}  // namespace test
+}  // namespace cvc5