| Logic |
Solvers |
Benchmarks |
# pairs Complete |
%
Complete |
Order (sequential performance) |
| Order (parallel performance) |
| Order (sequential performance on industrial benchmarks) |
| Order (parallel performance on industrial benchmarks) |
| ALIA | 5 | 42 | 210 | 100 | [Z3]; CVC4 (exp); CVC4; veriT; CVC3 |
| [Z3]; CVC4 (exp); CVC4; veriT; CVC3 |
| [Z3]; CVC4 (exp); CVC4; veriT; CVC3 |
| [Z3]; CVC4 (exp); CVC4; veriT; CVC3 |
| AUFLIA | 5 | 4 | 20 | 100 | CVC4 (exp); CVC3; CVC4; [Z3]; veriT |
| CVC4 (exp); CVC3; CVC4; [Z3]; veriT |
| CVC4; CVC4 (exp); [Z3]; CVC3; veriT |
| CVC4; [Z3]; CVC4 (exp); CVC3; veriT |
| AUFLIRA | 5 | 19849 | 99245 | 100 | [Z3]; CVC4 (exp); CVC4; CVC3; veriT |
| [Z3]; CVC4 (exp); CVC4; CVC3; veriT |
| [Z3]; CVC4; CVC4 (exp); CVC3; veriT |
| [Z3]; CVC4; CVC4 (exp); CVC3; veriT |
| AUFNIRA | 4 | 1050 | 4200 | 100 | CVC4; CVC4 (exp); [Z3]; CVC3 |
| CVC4; CVC4 (exp); [Z3]; CVC3 |
| CVC4; CVC4 (exp); [Z3]; CVC3 |
| CVC4; CVC4 (exp); [Z3]; CVC3 |
| BV | 4 | 85 | 340 | 100 | [Z3]; CVC4; CVC4 (exp); CVC3 |
| [Z3]; CVC4 (exp); CVC4; CVC3 |
| [Z3]; CVC4; CVC4 (exp); CVC3 |
| [Z3]; CVC4 (exp); CVC4; CVC3 |
| LIA | 5 | 201 | 1005 | 100 | CVC4 (exp); [Z3]; CVC4; CVC3; veriT |
| CVC4 (exp); [Z3]; CVC4; CVC3; veriT |
| CVC4 (exp); [Z3]; CVC4; CVC3; veriT |
| CVC4 (exp); [Z3]; CVC4; CVC3; veriT |
| LRA | 5 | 339 | 1695 | 100 | CVC4 (exp); CVC4; [Z3]; CVC3; veriT |
| CVC4 (exp); CVC4; [Z3]; CVC3; veriT |
| CVC4; CVC4 (exp); [Z3]; CVC3; veriT |
| CVC4 (exp); CVC4; [Z3]; CVC3; veriT |
| NIA | 4 | 9 | 36 | 100 | [Z3]; CVC4; CVC4 (exp); CVC3 |
| [Z3]; CVC4; CVC4 (exp); CVC3 |
| [Z3]; CVC4; CVC4 (exp); CVC3 |
| [Z3]; CVC4; CVC4 (exp); CVC3 |
| NRA | 4 | 3788 | 15152 | 100 | CVC4 (exp); CVC4; CVC3; [Z3] |
| CVC4 (exp); CVC4; CVC3; [Z3] |
| CVC4 (exp); CVC4; CVC3; [Z3] |
| CVC4 (exp); CVC4; CVC3; [Z3] |
| QF_ABV | 6 | 14720 | 88320 | 100 | Boolector (QF_AUFBV); Yices; [MathSat]; CVC4 (exp); CVC4; [Z3] |
| Boolector (QF_AUFBV); Yices; [MathSat]; CVC4 (exp); CVC4; [Z3] |
| Boolector (QF_AUFBV); Yices; [MathSat]; CVC4 (exp); CVC4; [Z3] |
| Boolector (QF_AUFBV); Yices; [MathSat]; CVC4 (exp); CVC4; [Z3] |
| QF_ALIA | 7 | 134 | 938 | 100 | Yices; [MathSat]; SMTInterpol; CVC4 (exp); [Z3]; CVC4; veriT |
| Yices; [MathSat]; SMTInterpol; CVC4 (exp); [Z3]; CVC4; veriT |
| Yices; [MathSat]; SMTInterpol; CVC4 (exp); [Z3]; CVC4; veriT |
| Yices; [MathSat]; SMTInterpol; CVC4 (exp); [Z3]; CVC4; veriT |
| QF_ANIA | 3 | 6 | 18 | 100 | [Z3]; CVC4 (exp); CVC4 |
| [Z3]; CVC4 (exp); CVC4 |
| [Z3]; CVC4 (exp); CVC4 |
| [Z3]; CVC4 (exp); CVC4 |
| QF_AUFBV | 6 | 37 | 222 | 100 | [MathSat]; CVC4; CVC4 (exp); Yices; Boolector (QF_AUFBV); [Z3] |
| [MathSat]; CVC4; CVC4 (exp); Yices; Boolector (QF_AUFBV); [Z3] |
| [MathSat]; CVC4; CVC4 (exp); Yices; Boolector (QF_AUFBV); [Z3] |
| [MathSat]; CVC4; CVC4 (exp); Yices; Boolector (QF_AUFBV); [Z3] |
| QF_AUFLIA | 7 | 1009 | 7063 | 100 | Yices; [Z3]; [MathSat]; CVC4 (exp); CVC4; SMTInterpol; veriT |
| Yices; [Z3]; [MathSat]; CVC4 (exp); SMTInterpol; CVC4; veriT |
| [Z3]; Yices; SMTInterpol; CVC4 (exp); [MathSat]; CVC4; veriT |
| [Z3]; Yices; SMTInterpol; CVC4 (exp); [MathSat]; CVC4; veriT |
| QF_AUFNIA | 3 | 21 | 63 | 100 | CVC4; CVC4 (exp); [Z3] |
| CVC4; CVC4 (exp); [Z3] |
| CVC4; CVC4 (exp); [Z3] |
| CVC4; CVC4 (exp); [Z3] |
| QF_AX | 7 | 551 | 3857 | 100 | Yices; [MathSat]; [Z3]; CVC4 (exp); CVC4; SMTInterpol; veriT |
| Yices; [MathSat]; [Z3]; CVC4 (exp); CVC4; SMTInterpol; veriT |
| - |
| - |
| QF_BV | 11 | 26414 | 290554 | 100 | Boolector (QF_BV); CVC4 (exp); STP-CMSat4; [Z3]; CVC4; [MathSat]; Yices; STP-CMSat4 (mt-v15); SMT-RAT; STP-CMSat4 (v15); STP-MiniSAT (v15) |
| Boolector (QF_BV); CVC4 (exp); STP-CMSat4; [Z3]; CVC4; [MathSat]; Yices; STP-CMSat4 (mt-v15); SMT-RAT; STP-CMSat4 (v15); STP-MiniSAT (v15) |
| Boolector (QF_BV); [Z3]; STP-CMSat4; Yices; CVC4 (exp); [MathSat]; CVC4; STP-CMSat4 (mt-v15); SMT-RAT; STP-CMSat4 (v15); STP-MiniSAT (v15) |
| Boolector (QF_BV); [Z3]; CVC4 (exp); STP-CMSat4; Yices; [MathSat]; CVC4; STP-CMSat4 (mt-v15); SMT-RAT; STP-CMSat4 (v15); STP-MiniSAT (v15) |
| QF_BVFP | 3 | 7 | 21 | 100 | Z3 (FP); [MathSat]; Z3 (ijcar14) |
| Z3 (FP); [MathSat]; Z3 (ijcar14) |
| - |
| - |
| QF_FP | 3 | 34413 | 103239 | 100 | Z3 (FP); Z3 (ijcar14); [MathSat] |
| Z3 (FP); Z3 (ijcar14); [MathSat] |
| - |
| - |
| QF_IDL | 6 | 2094 | 12564 | 100 | [Z3]; Yices; CVC4 (exp); CVC4; SMTInterpol; veriT |
| [Z3]; Yices; CVC4 (exp); CVC4; SMTInterpol; veriT |
| [Z3]; Yices; CVC4 (exp); CVC4; veriT; SMTInterpol |
| [Z3]; Yices; CVC4 (exp); CVC4; veriT; SMTInterpol |
| QF_LIA | 8 | 5839 | 46712 | 100 | [MathSat]; CVC4 (exp); CVC4; Yices; [Z3]; SMTInterpol; SMT-RAT; veriT |
| [MathSat]; CVC4 (exp); CVC4; Yices; [Z3]; SMTInterpol; SMT-RAT; veriT |
| [Z3]; [MathSat]; Yices; CVC4 (exp); CVC4; SMTInterpol; veriT; SMT-RAT |
| [Z3]; [MathSat]; Yices; CVC4 (exp); CVC4; SMTInterpol; veriT; SMT-RAT |
| QF_LIRA | 6 | 6 | 36 | 100 | Yices; CVC4; CVC4 (exp); [Z3]; SMT-RAT; SMTInterpol |
| Yices; CVC4; CVC4 (exp); [Z3]; SMT-RAT; SMTInterpol |
| Yices; CVC4; CVC4 (exp); [Z3]; SMT-RAT; SMTInterpol |
| Yices; CVC4; CVC4 (exp); [Z3]; SMT-RAT; SMTInterpol |
| QF_LRA | 8 | 1626 | 13008 | 100 | CVC4; CVC4 (exp); Yices; [MathSat]; veriT; [Z3]; SMTInterpol; SMT-RAT |
| CVC4; CVC4 (exp); Yices; [MathSat]; veriT; [Z3]; SMTInterpol; SMT-RAT |
| CVC4; CVC4 (exp); Yices; [MathSat]; veriT; [Z3]; SMTInterpol; SMT-RAT |
| CVC4; CVC4 (exp); Yices; [MathSat]; veriT; [Z3]; SMTInterpol; SMT-RAT |
| QF_NIA | 8 | 8475 | 67800 | 100 | [Z3]; AProVE; raSAT; SMT-RAT (parallel); SMT-RAT; CVC3; CVC4; CVC4 (exp) |
| [Z3]; AProVE; raSAT; SMT-RAT (parallel); SMT-RAT; CVC3; CVC4; CVC4 (exp) |
| [Z3]; AProVE; raSAT; SMT-RAT (parallel); SMT-RAT; CVC3; CVC4; CVC4 (exp) |
| [Z3]; AProVE; raSAT; SMT-RAT (parallel); SMT-RAT; CVC3; CVC4; CVC4 (exp) |
| QF_NIRA | 4 | 2 | 8 | 100 | CVC4 (exp); CVC4; SMT-RAT; [Z3] |
| CVC4 (exp); CVC4; SMT-RAT; [Z3] |
| CVC4 (exp); CVC4; SMT-RAT; [Z3] |
| CVC4 (exp); CVC4; SMT-RAT; [Z3] |
| QF_NRA | 7 | 10184 | 71288 | 100 | [Z3]; Yices2-NL; SMT-RAT; raSAT; CVC3; CVC4 (exp); CVC4 |
| [Z3]; Yices2-NL; SMT-RAT; raSAT; CVC3; CVC4; CVC4 (exp) |
| [Z3]; Yices2-NL; SMT-RAT; raSAT; CVC3; CVC4 (exp); CVC4 |
| [Z3]; Yices2-NL; SMT-RAT; raSAT; CVC3; CVC4; CVC4 (exp) |
| QF_RDL | 6 | 220 | 1320 | 100 | Yices; [Z3]; veriT; CVC4 (exp); CVC4; SMTInterpol |
| Yices; [Z3]; veriT; CVC4 (exp); CVC4; SMTInterpol |
| Yices; [Z3]; CVC4; CVC4 (exp); veriT; SMTInterpol |
| Yices; [Z3]; CVC4; CVC4 (exp); veriT; SMTInterpol |
| QF_UF | 10 | 6649 | 66490 | 100 | Yices; veriT; CVC4; CVC4 (exp); OpenSMT2; [Z3]; [MathSat]; SMTInterpol; SMT-RAT; OpenSMT2 (parallel) |
| Yices; veriT; CVC4; CVC4 (exp); OpenSMT2; [Z3]; [MathSat]; SMTInterpol; SMT-RAT; OpenSMT2 (parallel) |
| Yices; veriT; SMT-RAT; CVC4 (exp); CVC4; OpenSMT2 (parallel); OpenSMT2; [MathSat]; [Z3]; SMTInterpol |
| Yices; CVC4; SMT-RAT; veriT; CVC4 (exp); OpenSMT2 (parallel); OpenSMT2; [MathSat]; [Z3]; SMTInterpol |
| QF_UFBV | 6 | 31 | 186 | 100 | Boolector (QF_AUFBV); Yices; CVC4 (exp); [Z3]; [MathSat]; CVC4 |
| Boolector (QF_AUFBV); Yices; CVC4 (exp); [Z3]; [MathSat]; CVC4 |
| Boolector (QF_AUFBV); Yices; CVC4 (exp); [Z3]; [MathSat]; CVC4 |
| Boolector (QF_AUFBV); Yices; CVC4 (exp); [Z3]; [MathSat]; CVC4 |
| QF_UFIDL | 6 | 441 | 2646 | 100 | Yices; [Z3]; SMTInterpol; veriT; CVC4 (exp); CVC4 |
| Yices; [Z3]; SMTInterpol; veriT; CVC4 (exp); CVC4 |
| Yices; [Z3]; SMTInterpol; CVC4 (exp); CVC4; veriT |
| Yices; [Z3]; SMTInterpol; CVC4 (exp); CVC4; veriT |
| QF_UFLIA | 7 | 598 | 4186 | 100 | [Z3]; Yices; CVC4; CVC4 (exp); [MathSat]; SMTInterpol; veriT |
| [Z3]; Yices; CVC4; CVC4 (exp); [MathSat]; SMTInterpol; veriT |
| [Z3]; Yices; CVC4; CVC4 (exp); [MathSat]; SMTInterpol; veriT |
| [Z3]; Yices; CVC4; CVC4 (exp); SMTInterpol; [MathSat]; veriT |
| QF_UFLRA | 7 | 1627 | 11389 | 100 | Yices; [Z3]; [MathSat]; CVC4 (exp); CVC4; SMTInterpol; veriT |
| Yices; [Z3]; [MathSat]; CVC4 (exp); CVC4; SMTInterpol; veriT |
| Yices; [Z3]; [MathSat]; CVC4 (exp); CVC4; SMTInterpol; veriT |
| Yices; [Z3]; [MathSat]; CVC4 (exp); CVC4; SMTInterpol; veriT |
| QF_UFNIA | 4 | 7 | 28 | 100 | CVC4 (exp); CVC4; [Z3]; CVC3 |
| CVC4 (exp); CVC4; [Z3]; CVC3 |
| CVC4 (exp); CVC4; [Z3]; CVC3 |
| CVC4 (exp); CVC4; [Z3]; CVC3 |
| QF_UFNRA | 4 | 34 | 136 | 100 | [Z3]; CVC3; CVC4 (exp); CVC4 |
| [Z3]; CVC3; CVC4 (exp); CVC4 |
| [Z3]; CVC3; CVC4 (exp); CVC4 |
| [Z3]; CVC3; CVC4 (exp); CVC4 |
| UF | 5 | 2839 | 14195 | 100 | CVC4 (exp); CVC4; [Z3]; CVC3; veriT |
| CVC4 (exp); CVC4; [Z3]; CVC3; veriT |
| CVC4 (exp); CVC4; [Z3]; CVC3; veriT |
| CVC4 (exp); CVC4; [Z3]; CVC3; veriT |
| UFBV | 4 | 71 | 284 | 100 | [Z3]; CVC4; CVC4 (exp); CVC3 |
| [Z3]; CVC4; CVC4 (exp); CVC3 |
| [Z3]; CVC4; CVC4 (exp); CVC3 |
| [Z3]; CVC4; CVC4 (exp); CVC3 |
| UFIDL | 5 | 68 | 340 | 100 | [Z3]; CVC4; CVC4 (exp); veriT; CVC3 |
| [Z3]; CVC4; CVC4 (exp); veriT; CVC3 |
| [Z3]; CVC4; CVC4 (exp); veriT; CVC3 |
| [Z3]; CVC4; CVC4 (exp); veriT; CVC3 |
| UFLIA | 5 | 8404 | 42020 | 100 | CVC4; CVC4 (exp); [Z3]; veriT; CVC3 |
| CVC4; CVC4 (exp); [Z3]; veriT; CVC3 |
| CVC4; CVC4 (exp); [Z3]; veriT; CVC3 |
| CVC4; CVC4 (exp); [Z3]; veriT; CVC3 |
| UFLRA | 5 | 25 | 125 | 100 | CVC3; veriT; CVC4; CVC4 (exp); [Z3] |
| CVC3; veriT; CVC4; CVC4 (exp); [Z3] |
| veriT; CVC3; CVC4 (exp); CVC4; [Z3] |
| veriT; CVC3; CVC4; CVC4 (exp); [Z3] |
| UFNIA | 4 | 2319 | 9276 | 100 | CVC4; CVC4 (exp); [Z3]; CVC3 |
| CVC4; CVC4 (exp); [Z3]; CVC3 |
| CVC4; CVC4 (exp); [Z3]; CVC3 |
| CVC4; CVC4 (exp); [Z3]; CVC3 |
Last modified: Fri 30 Oct 2015 12:49 UTC
