projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: da73f99) | patch
Allow eager bitblasting with solve bv as int in QF_NIA (#4373)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 22 Apr 2020 13:45:52 +0000 (08:45 -0500)
committerGitHub <noreply@github.com>
Wed, 22 Apr 2020 13:45:52 +0000 (08:45 -0500)
commit286ed8f8a3d6aece0469e983e87626a25107608d
treef710a94efc205c0333ad28d7996a8c1d00d00cc3tree
parentda73f99910a25fca342c0ba1d8ec19de6c3cefdacommit | diff
Allow eager bitblasting with solve bv as int in QF_NIA (#4373)

This also updates the SMT COMP script to revert to our previous behavior.

This is required for SMT COMP. It should be beneficial for satisfiable QF_NIA instances. I will revisit/test this independently.
contrib/competitions/smt-comp/run-script-smtcomp-current diff | blob | history
src/smt/set_defaults.cpp diff | blob | history