The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results as of Fri Jun 27 16:49:23 EDT 2014
Completed 347147/347147 = 100.0%
| Logic | Solvers | Benchmarks | # Pairs Complete | % Complete | Order |
|---|---|---|---|---|---|
| ALIA | 4 | 29 | 116 | 100% | Z3n; CVC4; veriT; CVC3; |
| AUFLIA | 4 | 4 | 16 | 100% | CVC4; Z3n; CVC3; veriT; |
| AUFLIRA | 4 | 10791 | 43164 | 100% | Z3n; CVC4; CVC3; veriT; |
| AUFNIRA | 4 | 564 | 2256 | 100% | CVC4-with-bugfixn; Z3n; CVC3; CVC4; |
| BV | 0 | 0 | |||
| LIA | 4 | 46 | 184 | 100% | Z3n; CVC4; CVC3; veriT; |
| LRA | 4 | 171 | 684 | 100% | CVC4; Z3n; CVC3; veriT; |
| NIA | 3 | 9 | 27 | 100% | Z3n; CVC4; CVC3; |
| NRA | 3 | 3747 | 11241 | 100% | Z3n; CVC4; CVC3; |
| QF_ABV | 9 | 6457 | 58113 | 100% | Boolector (justification); Boolector (dual propagation); MathSATn; SONOLAR; CVC4; Z3n; Yices2; Kleaver-STP; Kleaver-portfolio; |
| QF_ALIA | 5 | 97 | 485 | 100% | Yices2; SMTInterpol; Z3n; MathSATn; CVC4; |
| QF_AUFBV | 4 | 37 | 148 | 100% | CVC4; Yices2; Z3n; MathSATn; |
| QF_AUFLIA | 6 | 610 | 3660 | 100% | Yices2; MathSATn; Z3n; SMTInterpol; CVC4; veriT; |
| QF_AX | 5 | 335 | 1675 | 100% | Yices2; MathSATn; Z3n; CVC4; SMTInterpol; |
| QF_BV | 11 | 2488 | 27368 | 100% | Boolector; STP-CryptoMiniSat4; CVC4-with-bugfixn; MathSATn; Z3n; CVC4; 4Simp; SONOLAR; Yices2; abziz_min_features; abziz_all_features; |
| QF_IDL | 4 | 1315 | 5260 | 100% | Z3n; Yices2; CVC4; veriT; |
| QF_LIA | 7 | 4381 | 30667 | 100% | CVC4-with-bugfixn; MathSATn; SMTInterpol; Yices2; Z3n; veriT; CVC4; |
| QF_LRA | 6 | 1343 | 8058 | 100% | CVC4; Yices2; MathSATn; SMTInterpol; veriT; Z3n; |
| QF_NIA | 4 | 8327 | 33308 | 100% | Z3n; AProVE; CVC3; CVC4; |
| QF_NRA | 4 | 10121 | 40484 | 100% | Z3n; CVC3; CVC4; raSAT; |
| QF_RDL | 4 | 132 | 528 | 100% | Yices2; Z3n; veriT; CVC4; |
| QF_UF | 7 | 4124 | 28868 | 100% | Yices2; veriT; CVC4; OpenSMT2; Z3n; MathSATn; SMTInterpol; |
| QF_UFBV | 4 | 31 | 124 | 100% | Yices2; Z3n; MathSATn; CVC4; |
| QF_UFIDL | 4 | 311 | 1244 | 100% | Z3n; Yices2; CVC4; veriT; |
| QF_UFLIA | 6 | 484 | 2904 | 100% | Z3n; Yices2; CVC4; SMTInterpol; MathSATn; veriT; |
| QF_UFLRA | 6 | 1176 | 7056 | 100% | Z3n; Yices2; MathSATn; CVC4; SMTInterpol; veriT; |
| QF_UFNIA | 3 | 7 | 21 | 100% | CVC4; Z3n; CVC3; |
| QF_UFNRA | 3 | 32 | 96 | 100% | Z3n; CVC3; CVC4; |
| UF | 4 | 2830 | 11320 | 100% | CVC4; Z3n; CVC3; veriT; |
| UFBV | 0 | 0 | |||
| UFIDL | 3 | 49 | 147 | 100% | Z3n; CVC4; CVC3; |
| UFLIA | 4 | 5766 | 23064 | 100% | CVC4; Z3n; veriT; CVC3; |
| UFLRA | 4 | 25 | 100 | 100% | Z3n; veriT; CVC3; CVC4; |
| UFNIA | 3 | 1587 | 4761 | 100% | Z3n; CVC4; CVC3; |
n. Non-competitive.