[Strings] Fix incorrect rewrite (#6837)

Fixes #6834. There were two cases in our extended rewriter for string
equalities that were modifying the node without returning and without
updating information computed from the original node. This mismatch led
to incorrect rewrites. This commit fixes the issue by adding a flag to
returnRewrite() that determines whether node that was an equality
before and after the rewrite should be rewritten again with the extended
rewriter. We generally do not do that (we'd run in danger of rewriting
equality nodes with the extended rewriter even though we shouldn't) but
for the rewrites that were previously continuing to rewrite the node, we
set this flag and return. This ensures that we do not have an issue with
information being out of date. The commit additionally fixes an issue
where we would apply the rewrite STR_EQ_UNIFY even though the node
hadn't changed.

4 files changed, 34 insertions, 11 deletions

diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp
index 6e67352b3..d3360403e 100644
--- a/src/theory/strings/sequences_rewriter.cpp
+++ b/src/theory/strings/sequences_rewriter.cpp
@@ -206,8 +206,15 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node)
     // e.g. x++y = x++z ---> y = z, "AB" ++ x = "A" ++ y --> "B" ++ x = y
     Node s1 = utils::mkConcat(c[0], stype);
     Node s2 = utils::mkConcat(c[1], stype);
-    new_ret = s1.eqNode(s2);
-    node = returnRewrite(node, new_ret, Rewrite::STR_EQ_UNIFY);
+    if (s1 != node[0] || s2 != node[1])
+    {
+      new_ret = s1.eqNode(s2);
+      // We generally don't apply the extended equality rewriter if the
+      // original node was an equality but we may be able to do additional
+      // rewriting here, e.g.,
+      // x++y = "" --> x = "" and y = ""
+      return returnRewrite(node, new_ret, Rewrite::STR_EQ_UNIFY, true);
+    }
   }
 
   // ------- homogeneous constants
@@ -280,8 +287,12 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node)
         // e.g.
         //  "AA" = y ++ x ---> "AA" = x ++ y if x < y
         //  "AAA" = y ++ "A" ++ z ---> "AA" = y ++ z
+        //
+        // We generally don't apply the extended equality rewriter if the
+        // original node was an equality but we may be able to do additional
+        // rewriting here.
         new_ret = lhs.eqNode(ss);
-        node = returnRewrite(node, new_ret, Rewrite::STR_EQ_HOMOG_CONST);
+        return returnRewrite(node, new_ret, Rewrite::STR_EQ_HOMOG_CONST, true);
       }
     }
   }
@@ -3471,7 +3482,10 @@ Node SequencesRewriter::rewriteSeqUnit(Node node)
   return node;
 }
 
-Node SequencesRewriter::returnRewrite(Node node, Node ret, Rewrite r)
+Node SequencesRewriter::returnRewrite(Node node,
+                                      Node ret,
+                                      Rewrite r,
+                                      bool rewriteEqAgain)
 {
   Trace("strings-rewrite") << "Rewrite " << node << " to " << ret << " by " << r
                            << "." << std::endl;
@@ -3515,7 +3529,7 @@ Node SequencesRewriter::returnRewrite(Node node, Node ret, Rewrite r)
   {
     ret = nm->mkNode(NOT, rewriteEqualityExt(ret[0]));
   }
-  else if (retk == EQUAL && node.getKind() != EQUAL)
+  else if (retk == EQUAL && (rewriteEqAgain || node.getKind() != EQUAL))
   {
     Trace("strings-rewrite")
         << "Apply extended equality rewrite on " << ret << std::endl;
diff --git a/src/theory/strings/sequences_rewriter.h b/src/theory/strings/sequences_rewriter.h
index 37ed78786..9127637aa 100644
--- a/src/theory/strings/sequences_rewriter.h
+++ b/src/theory/strings/sequences_rewriter.h
@@ -117,12 +117,15 @@ class SequencesRewriter : public TheoryRewriter
    * The rewrite r indicates the justification for the rewrite, which is printed
    * by this function for debugging.
    *
-   * If node is not an equality and ret is an equality, this method applies
-   * an additional rewrite step (rewriteEqualityExt) that performs
-   * additional rewrites on ret, after which we return the result of this call.
-   * Otherwise, this method simply returns ret.
-   */
-  Node returnRewrite(Node node, Node ret, Rewrite r);
+   * If node is not an equality (or rewriteEq is true) and ret is an equality,
+   * this method applies an additional rewrite step (rewriteEqualityExt) that
+   * performs additional rewrites on ret, after which we return the result of
+   * this call. Otherwise, this method simply returns ret.
+   */
+  Node returnRewrite(Node node,
+                     Node ret,
+                     Rewrite r,
+                     bool rewriteEqAgain = false);
 
  public:
   RewriteResponse postRewrite(TNode node) override;
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 00a50a69c..18e9d9864 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1178,6 +1178,7 @@ set(regress_0_tests
   regress0/strings/issue6604-re-elim.smt2
   regress0/strings/issue6643-ctn-decompose-conflict.smt2
   regress0/strings/issue6681-split-eq-strip-l.smt2
+  regress0/strings/issue6834-str-eq-const-nhomog.smt2
   regress0/strings/itos-entail.smt2
   regress0/strings/large-model.smt2
   regress0/strings/leadingzero001.smt2
diff --git a/test/regress/regress0/strings/issue6834-str-eq-const-nhomog.smt2 b/test/regress/regress0/strings/issue6834-str-eq-const-nhomog.smt2
new file mode 100644
index 000000000..e2579acf5
--- /dev/null
+++ b/test/regress/regress0/strings/issue6834-str-eq-const-nhomog.smt2
@@ -0,0 +1,5 @@
+(set-logic QF_SLIA)
+(declare-fun a () Int)
+(assert (= (str.++ (str.substr "A" 0 a) "B" (str.substr "A" 0 a)) "B"))
+(set-info :status sat)
+(check-sat)