projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5e7107f) | patch
Fix non-termination in quantifiers rewriter (#8165)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 25 Feb 2022 19:59:27 +0000 (13:59 -0600)
committerGitHub <noreply@github.com>
Fri, 25 Feb 2022 19:59:27 +0000 (19:59 +0000)
commit0b603261b43424bd0a08db4d9422ff7d005c33cb
treef8a83ffd4a5232e9af92bbd012d0754918ec696ctree
parent5e7107f378f917731acbd017c854829f25ac8bdfcommit | diff
Fix non-termination in quantifiers rewriter (#8165)

Caused by 2 rewrite steps (conditional splitting and extended rewriting) being inverses of each other when miniscoping is disabled.

Fixes the third benchmark on #8159.
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/regress0/quantifiers/issue8159-3-qext-nterm.smt2 [new file with mode: 0644] blob