projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0e2f847) | patch
More robust treatment of flattening in arith rewriter (#8695)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 2 May 2022 22:32:39 +0000 (17:32 -0500)
committerGitHub <noreply@github.com>
Mon, 2 May 2022 22:32:39 +0000 (22:32 +0000)
commitcedb607a0017bff88f6d0be3d7295e87843c1662
tree2359dd92ce482f9dd9f5dd959cdf1c997a77d95ctree
parent0e2f84754dd44baa14206780b93f84dd5002a509commit | diff
More robust treatment of flattening in arith rewriter (#8695)

Currently can allow rewritten forms to be rewritable.

Fixes #8692. Fixes #8693. Fixes #8697.
src/theory/arith/arith_rewriter.cpp diff | blob | history
test/regress/cli/CMakeLists.txt diff | blob | history
test/regress/cli/regress0/nl/issue8692-idem-flatten.smt2 [new file with mode: 0644] blob
test/regress/cli/regress2/nl/issue8693-flatten-to-real.smt2 [new file with mode: 0644] blob