Do not use extended rewrites on recursive function definitions (#7549)

Leads to potential non-idempotent behavior in the rewriter.

The issue cannot be replicated on master, but this safe guards this case anyways.

Fixes #5278.

2 files changed, 9 insertions, 4 deletions

diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 52e90e26e..88c6cd96f 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -550,8 +550,13 @@ Node QuantifiersRewriter::computeProcessTerms2(
   return ret;
 }
 
-Node QuantifiersRewriter::computeExtendedRewrite(Node q)
+Node QuantifiersRewriter::computeExtendedRewrite(Node q, const QAttributes& qa)
 {
+  // do not apply to recursive functions
+  if (qa.isFunDef())
+  {
+    return q;
+  }
   Node body = q[1];
   // apply extended rewriter
   Node bodyr = Rewriter::callExtendedRewrite(body);
@@ -1888,7 +1893,7 @@ Node QuantifiersRewriter::computeOperation(Node f,
   }
   else if (computeOption == COMPUTE_EXT_REWRITE)
   {
-    return computeExtendedRewrite(f);
+    return computeExtendedRewrite(f, qa);
   }
   else if (computeOption == COMPUTE_PROCESS_TERMS)
   {
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index 6a7eb5158..8b3cbb522 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -293,9 +293,9 @@ class QuantifiersRewriter : public TheoryRewriter
   /** compute extended rewrite
    *
    * This returns the result of applying the extended rewriter on the body
-   * of quantified formula q.
+   * of quantified formula q with attributes qa.
    */
-  static Node computeExtendedRewrite(Node q);
+  static Node computeExtendedRewrite(Node q, const QAttributes& qa);
   //------------------------------------- end extended rewrite
   /**
    * Return true if we should do operation computeOption on quantified formula