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.

diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 52e90e26eeb4301e2790e38407e976ce9d800448..88c6cd96fedac33e2741378ba1a46f991de4ae2a 100644 (file)
--- 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 6a7eb51588bef871038d3ce7cff78e24cd1119bc..8b3cbb5224f499b0892ca69bf7a4d9d440275688 100644 (file)
--- 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

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index f6e52eb344ae2bf9d129cc330ab2507e96052187..b0b19315ecb2dac99cf0efc21588dc36fb1a4b2c 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1966,6 +1966,7 @@ set(regress_1_tests
   regress1/quantifiers/issue4813-qe-quant.smt2
   regress1/quantifiers/issue4849-nqe.smt2
   regress1/quantifiers/issue5019-cegqi-i.smt2
+  regress1/quantifiers/issue5278-ext-rewrite-rec.smt2
   regress1/quantifiers/issue5279-nqe.smt2
   regress1/quantifiers/issue5288-vts-real-int.smt2
   regress1/quantifiers/issue5365-nqe.smt2

diff --git a/test/regress/regress1/quantifiers/issue5278-ext-rewrite-rec.smt2 b/test/regress/regress1/quantifiers/issue5278-ext-rewrite-rec.smt2
new file mode 100644 (file)
index 0000000..9313d9f
--- /dev/null
+++ b/test/regress/regress1/quantifiers/issue5278-ext-rewrite-rec.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --fmf-fun --ext-rewrite-quant -q
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-datatypes ((a 0)) (((b) (c))))
+(define-funs-rec ((d ((x a)) Bool)) ((is-b x)))
+(check-sat)