projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 9ccf3c0) | patch
[SMT-COMP 2019] Use lazy BV as backup for QF_UFBV (#3037)
authorAndres Noetzli <noetzli@stanford.edu>
Mon, 3 Jun 2019 04:23:52 +0000 (21:23 -0700)
committerGitHub <noreply@github.com>
Mon, 3 Jun 2019 04:23:52 +0000 (21:23 -0700)
commit52a910f728f399e782b3ac036e4476f1fb3c27fa
treef71207f20a825d88890f5367979ae56919d246b9tree
parent9ccf3c01a736a9f6d5c6889b51c4589221044c97commit | diff
[SMT-COMP 2019] Use lazy BV as backup for QF_UFBV (#3037)

We cannot Ackermannize all the QF_UFBV benchmarks due to uninterpreted
sorts. This commit adds lazy bit-blasting as a backup strategy.
contrib/run-script-smtcomp2019 diff | blob | history