projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2c7a64f) | patch
[SMT-COMP 2019] Update run script for unsat cores (#3034)
authorAndres Noetzli <noetzli@stanford.edu>
Mon, 3 Jun 2019 02:30:10 +0000 (19:30 -0700)
committerGitHub <noreply@github.com>
Mon, 3 Jun 2019 02:30:10 +0000 (19:30 -0700)
commita211c34d77c432007c3e1ed3c82baaea315a7632
tree66faa195474e692d45a134042bbd3a34e3873103tree
parent2c7a64f5bdafd35e02510db5ec8026cff32e505fcommit | diff
[SMT-COMP 2019] Update run script for unsat cores (#3034)

`--unconstrained-simp` is not compatible with unsat cores, so this
commit removes it for QF_LRA. `--bitblast=eager` is not compatible with
unsat cores for QF_UFBV because the dependencies are not tracked
correctly in the Ackermannization preprocessing pass, so the commit
changes the script to use the lazy BV solver instead. Strings need some
additional options to use the correct theory symbols.
contrib/run-script-smtcomp2019-unsat-cores diff | blob | history