CVC4
An efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.
About
News
Downloads
Documentation
Publications
Awards
People
History
Third-Party Applications
Acknowledgements
CVC4 at Vienna Summer of Logic
by Clark Barrett
CVC4 won several honors at the “Olympic Games” at the Vienna Summer of Logic. CVC4 won the most divisions of the SMT-COMP competition (14). Yices won the second most divisions (10). Unfortunately, both CVC4 and Yices got wrong answers due to bugs uncovered by the benchmark scrambling, disqualifying them from receiving an olympic medal. Medals instead went to veriT and SMTInterpol.
Note that Z3 was not an official competitor this year. If it had been, Z3
would have won 16 divisions, CVC4 would have won 7, and Yices would have won 6.
With the CVC4 bug-fix, the numbers would have been 15 for Z3, 9 for CVC4 (and
still 6 for Yices). CVC4 performed especially well in quantified divisions and
arithmetic, due to excellent work by Andrew Reynolds1 2 and Tim
King.3 4 With the bug-fix, performance was also quite good in QF_BV,
coming in behind Boolector and STP, thanks to recent improvements by Liana
Haderean and others (see 5). Z3 did especially well in divisions containing
non-linear arithmetic (AUFNIRA, NIA, NRA, QF_NIA, QF_NRA, QF_UFNIA,
QF_UFNRA, UFNIA), where other solvers generally have very limited
capabilities. Omitting these divisions, the numbers are 9 for Z3, 7 for CVC4
with bug-fix, and 6 for Yices. Finally, it’s worth noting that if you look at
the “overall” score for all divisions, computed according to the SMT-COMP
rules, Z3 wins with 73.97 and CVC4 (with the bug-fix) is second with 65.56, but
if you omit the non-linear divisions, the score becomes 55.57 for CVC4 and
54.82 for Z3. For more details, see the SMT-COMP web site.6
CVC4 also entered CASC, the first-order theorem prover competition, where it was a surprise winner of the TFA division, and placed 3rd in the FNT division. Go to the CASC page for more.7