We evaluated veriT, CVC3 and Z3 (both using the latest available version in February 2009) against the SMT-LIB benchmarks for QF IDL, QF RDL, QF UF and QF UFIDL (June 2008 version) using an Intel(R) Pentium(R) 4 CPU at 3.00 GHz with 1 GiB of RAM and a timeout of 120 seconds. The following table presents, for each solver, the number of completed benchmarks.
| Solver | QF_UF (6656) | QF_UFIDL (432) | QF_IDL (1673) | QF_RDL (204) | all (8965) |
|---|---|---|---|---|---|
| veriT | 6323 | 332 | 918 | 100 | 7673 |
| CVC3 | 6378 | 278 | 802 | 45 | 7503 |
| Z3 | 6608 | 419 | 1511 | 158 | 8696 |
This clearly shows that, although veriT is not yet as efficient as competition winning tools, its efficiency is decent. The proof production capability of veriT does not come at a cost on efficiency.
