Fix `collectEmptyEqs()` in string utils (#6562)

Fixes #6483. The benchmark in the issue was performing the following
incorrect rewrite:

 Rewrite (str.replace "B" (str.replace (str.++ (str.replace "B" a "B") a) "B" "") "B") to (str.replace "B" a "B") by RPL_X_Y_X_SIMP.
The rewrite RPL_X_Y_X_SIMP rewrites terms of the form (str.replace x y x), where x is of length one and (= y "") rewrites to a
conjunction of equalities of the form (= y_i "") where y_i is some
term. The function responsible for collecting the terms y_i from this
conjunction, collectEmptyEqs(), returns a bool and a vector of
Nodes. The bool indicates whether all equalities in the conjunction
were of the form (= y_i ""). The rewrite RPL_X_Y_X_SIMP only applies
if this is true. However, collectEmptyEqs() had a bug where it would
not return false when all of the conjuncts were equalities but not all
of them were equalities with the empty string. This commit fixes
collectEmptyEqs() and adds tests.

1 files changed, 12 insertions, 9 deletions

diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp
index 5a4a25e88..5df744412 100644
--- a/src/theory/strings/theory_strings_utils.cpp
+++ b/src/theory/strings/theory_strings_utils.cpp
@@ -243,16 +243,19 @@ 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;
+      }
+
+      if (Word::isEmpty(c[0]))
+      {
+        emptyNodes.insert(c[1]);
+      }
+      else if (Word::isEmpty(c[1]))
+      {
+        emptyNodes.insert(c[0]);
       }
       else
       {