diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-01-14 07:28:55 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-01-14 07:28:55 -0600 |
commit | eb6155c5f078a26b7cdddddad6e209fad0f825f8 (patch) | |
tree | be9519b18c6eb61e69af0966c4339c483a534af0 /src/CMakeLists.txt | |
parent | 9fd4e5758df5e1085a3d6c80e3a6162d61b36566 (diff) |
Updates to theory preprocess equality (#5776)
This makes 3 changes related to arithmetic preprocessing of equalities which revert to the original behavior of master before a129c57.
For background, the commit a129c57 unintentionally changed the default behavior slightly in 3 ways (each corrected in this PR), which led a performance regression on QF_LIA in current master.
The 3 fixes are:
(1) Rewrite equalities should be applied as a post-rewrite, not a pre-rewrite in the theory-rewrite-eq preprocessing pass. This is particularly important for equalities between ITE terms that contain other equalities recursively.
(2) theory-rewrite-eq should apply after rewriting and just before the normal theory preprocessing.
(3) The arith-brab test should call ppRewrite on the arithmetic equality it introduces, as it has a choice of whether to eliminate the equality before the lemma is sent out.
Diffstat (limited to 'src/CMakeLists.txt')
0 files changed, 0 insertions, 0 deletions