projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: fcac065) | patch
Remove extended rewrite for arithmetic (#5760)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 11 Jan 2021 14:48:01 +0000 (08:48 -0600)
committerGitHub <noreply@github.com>
Mon, 11 Jan 2021 14:48:01 +0000 (08:48 -0600)
commitae82eb306143ade54a6f99b2aae0b62b8c77cd35
tree1ad4dadb2ada741fbd6d43e7755a81204eadea23tree
parentfcac065b47ea73aecb90f019c07dc6fa09cd914fcommit | diff
Remove extended rewrite for arithmetic (#5760)

This rewrite is no longer needed since our philosophy on rewriting extended arithmetic symbols has changed (we employ aggressive rewriting for extended arithmetic symbols in the normal rewriter). Moreover there was a soundness bug in the extended rewriter for division and mod by 0.

Fixes #5737, fixes #5740.
src/theory/quantifiers/extended_rewrite.cpp diff | blob | history
src/theory/quantifiers/extended_rewrite.h diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/nl/issue5737-div00.smt2 [new file with mode: 0644] blob
test/regress/regress0/nl/issue5740-2-mod00.smt2 [new file with mode: 0644] blob
test/regress/regress0/nl/issue5740-mod00.smt2 [new file with mode: 0644] blob