# CVC4

An efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

28 July 2014

# 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