projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 733ab2f) | patch
Do not use extended rewrites on recursive function definitions (#7549)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sat, 6 Nov 2021 01:26:33 +0000 (20:26 -0500)
committerGitHub <noreply@github.com>
Sat, 6 Nov 2021 01:26:33 +0000 (01:26 +0000)
commitd93e02dc254fea6c9d56194f21649cc18f29aafe
treee21dd0bafa7c8f843a224e03361f2119de5d55datree
parent733ab2f6b9430b2ae5824e2614de5811a60033f3commit | diff
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.
src/theory/quantifiers/quantifiers_rewriter.cpp diff | blob | history
src/theory/quantifiers/quantifiers_rewriter.h diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/quantifiers/issue5278-ext-rewrite-rec.smt2 [new file with mode: 0644] blob