projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 00badd3) | patch
Do not enable unconstrained simplification if arithmetic is present (#4489)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 12 May 2020 16:47:47 +0000 (11:47 -0500)
committerGitHub <noreply@github.com>
Tue, 12 May 2020 16:47:47 +0000 (11:47 -0500)
commit3b50dfe623f44e97d85449fa2a7566e81c639b47
treec4b0ccd1c89435504d83c45408f6188265af351ftree
parent00badd3a63a2fa568373d5c58553944b579d42bbcommit | diff
Do not enable unconstrained simplification if arithmetic is present (#4489)

For now we do not enable unconstrained simplification when arithmetic is present. Post SMT COMP, we should investigate making arithmetic not output lemmas during preprocessing (CVC4/cvc4-wishues#71).
src/smt/set_defaults.cpp diff | blob | history