diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 9 | ||||
| -rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.h | 4 |
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 |