From b0d216c23bff2163be3f77dfc37f36af5f504686 Mon Sep 17 00:00:00 2001
From: Bruno Dutertre <BrunoDutertre@users.noreply.github.com>
Date: Fri, 28 Jan 2022 12:33:10 -0800
Subject: [PATCH] Try a bit harder on the EQ_NCTN rewrite rule (#7998)

This makes a small change to the sequence rewriter to work a bit harder
on one of the rewrite rule. This fixes some performance issues we've
observed.

Signed-off-by: Bruno Dutertre <dutebrun@amazon.com>
---
 src/theory/strings/sequences_rewriter.cpp | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp
index e4db2f325..bbe25b7a3 100644
--- a/src/theory/strings/sequences_rewriter.cpp
+++ b/src/theory/strings/sequences_rewriter.cpp
@@ -114,8 +114,15 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node)
   {
     // must call rewrite contains directly to avoid infinite loop
     Node ctn = nm->mkNode(STRING_CONTAINS, node[r], node[1 - r]);
+    Node prev = ctn;
     ctn = rewriteContains(ctn);
     Assert(!ctn.isNull());
+    if (ctn != prev && ctn.getKind() == STRING_CONTAINS)
+    {
+      prev = ctn;
+      ctn = rewriteContains(ctn);
+      Assert(!ctn.isNull());
+    }
     if (ctn.isConst())
     {
       if (!ctn.getConst<bool>())
-- 
2.30.2