The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results as of Fri Jul 21 10:18:02 GMT
| Logic | Solvers | Benchmarks | # pairs Complete | % Complete | Order (sequential performance) |
|---|---|---|---|---|---|
| Order (parallel performance) | |||||
| ALIA | 4 | 42 | 168 | 100 | z3-4.5.0n; CVC4; vampire 4.2; veriT |
| z3-4.5.0n; CVC4; vampire 4.2; veriT | |||||
| AUFBVDTLIA | 1 | 1709 | 1709 | 100 | CVC4 |
| CVC4 | |||||
| AUFDTLIA | 2 | 728 | 1456 | 100 | CVC4; vampire 4.2 |
| CVC4; vampire 4.2 | |||||
| AUFLIA | 4 | 4 | 16 | 100 | CVC4; veriT; z3-4.5.0n; vampire 4.2 |
| CVC4; vampire 4.2; veriT; z3-4.5.0n | |||||
| AUFLIRA | 4 | 20011 | 80044 | 100 | z3-4.5.0n; vampire 4.2; CVC4; veriT |
| z3-4.5.0n; vampire 4.2; CVC4; veriT | |||||
| AUFNIRA | 3 | 1480 | 4440 | 100 | vampire 4.2; CVC4; z3-4.5.0n |
| vampire 4.2; CVC4; z3-4.5.0n | |||||
| BV | 4 | 5150 | 20600 | 100 | z3-4.5.0n; Q3B; Boolector; CVC4 |
| z3-4.5.0n; Q3B; Boolector; CVC4 | |||||
| LIA | 4 | 388 | 1552 | 100 | z3-4.5.0n; CVC4; vampire 4.2; veriT |
| z3-4.5.0n; CVC4; vampire 4.2; veriT | |||||
| LRA | 5 | 2419 | 12095 | 100 | z3-4.5.0n; CVC4; veriT+Redlog; Redlog; vampire 4.2 |
| z3-4.5.0n; CVC4; veriT+Redlog; Redlog; vampire 4.2 | |||||
| NIA | 3 | 14 | 42 | 100 | z3-4.5.0n; CVC4; vampire 4.2 |
| z3-4.5.0n; CVC4; vampire 4.2 | |||||
| NRA | 5 | 3811 | 19055 | 100 | Redlog; veriT+Redlog; z3-4.5.0n; vampire 4.2; CVC4 |
| Redlog; veriT+Redlog; z3-4.5.0n; vampire 4.2; CVC4 | |||||
| QF_ABV | 5 | 15061 | 75305 | 100 | Boolector; Yices2; CVC4; z3-4.5.0n; mathsat-5.4.1n |
| Boolector; Yices2; CVC4; z3-4.5.0n; mathsat-5.4.1n | |||||
| QF_ALIA | 6 | 139 | 834 | 100 | Yices2; mathsat-5.4.1n; SMTInterpol; CVC4; z3-4.5.0n; veriT |
| Yices2; mathsat-5.4.1n; SMTInterpol; CVC4; z3-4.5.0n; veriT | |||||
| QF_ANIA | 2 | 8 | 16 | 100 | CVC4; z3-4.5.0n |
| CVC4; z3-4.5.0n | |||||
| QF_AUFBV | 5 | 31 | 155 | 100 | mathsat-5.4.1n; Yices2; CVC4; Boolector; z3-4.5.0n |
| mathsat-5.4.1n; Yices2; CVC4; Boolector; z3-4.5.0n | |||||
| QF_AUFLIA | 6 | 1009 | 6054 | 100 | Yices2; z3-4.5.0n; SMTInterpol; mathsat-5.4.1n; CVC4; veriT |
| Yices2; z3-4.5.0n; SMTInterpol; mathsat-5.4.1n; CVC4; veriT | |||||
| QF_AUFNIA | 2 | 17 | 34 | 100 | z3-4.5.0n; CVC4 |
| z3-4.5.0n; CVC4 | |||||
| QF_AX | 5 | 551 | 2755 | 100 | Yices2; mathsat-5.4.1n; z3-4.5.0n; CVC4; SMTInterpol |
| Yices2; mathsat-5.4.1n; z3-4.5.0n; CVC4; SMTInterpol | |||||
| QF_BV | 10 | 40043 | 400430 | 100 | Boolector+CaDiCaL; Boolector; MinkeyRink; stp_st; stp_mt; z3-4.5.0n; CVC4; Yices2; Q3B; mathsat-5.4.1n |
| MinkeyRink; Boolector+CaDiCaL; Boolector; stp_mt; stp_st; CVC4; z3-4.5.0n; Yices2; Q3B; mathsat-5.4.1n | |||||
| QF_BVFP | 2 | 17215 | 34430 | 100 | z3-4.5.0n; COLIBRI |
| z3-4.5.0n; COLIBRI | |||||
| QF_DT | 1 | 8000 | 8000 | 100 | CVC4 |
| CVC4 | |||||
| QF_FP | 3 | 40302 | 120906 | 100 | z3-4.5.0n; COLIBRI; xsat |
| z3-4.5.0n; COLIBRI; xsat | |||||
| QF_IDL | 5 | 2193 | 10965 | 100 | Yices2; z3-4.5.0n; CVC4; veriT; SMTInterpol |
| Yices2; z3-4.5.0n; CVC4; veriT; SMTInterpol | |||||
| QF_LIA | 7 | 6141 | 42987 | 100 | mathsat-5.4.1n; CVC4; Yices2; SMTInterpol; z3-4.5.0n; SMTRAT; veriT |
| mathsat-5.4.1n; CVC4; Yices2; SMTInterpol; z3-4.5.0n; SMTRAT; veriT | |||||
| QF_LIRA | 5 | 7 | 35 | 100 | z3-4.5.0n; Yices2; CVC4; SMTRAT; SMTInterpol |
| z3-4.5.0n; Yices2; CVC4; SMTRAT; SMTInterpol | |||||
| QF_LRA | 8 | 1649 | 13192 | 100 | CVC4; Yices2; SMTInterpol; veriT; mathsat-5.4.1n; z3-4.5.0n; SMTRAT; opensmt2 |
| CVC4; Yices2; SMTInterpol; veriT; mathsat-5.4.1n; z3-4.5.0n; SMTRAT; opensmt2 | |||||
| QF_NIA | 5 | 23876 | 119380 | 100 | CVC4; Yices2; z3-4.5.0n; SMTRAT; AProVE |
| CVC4; Yices2; z3-4.5.0n; SMTRAT; AProVE | |||||
| QF_NIRA | 4 | 3 | 12 | 100 | SMTRAT; z3-4.5.0n; CVC4; Yices2 |
| SMTRAT; z3-4.5.0n; CVC4; Yices2 | |||||
| QF_NRA | 5 | 11354 | 56770 | 100 | Yices2; z3-4.5.0n; veriT+raSAT+Redlog; SMTRAT; CVC4 |
| Yices2; z3-4.5.0n; veriT+raSAT+Redlog; SMTRAT; CVC4 | |||||
| QF_RDL | 5 | 255 | 1275 | 100 | Yices2; CVC4; veriT; z3-4.5.0n; SMTInterpol |
| Yices2; CVC4; veriT; z3-4.5.0n; SMTInterpol | |||||
| QF_UF | 7 | 6650 | 46550 | 100 | Yices2; veriT; CVC4; opensmt2; z3-4.5.0n; mathsat-5.4.1n; SMTInterpol |
| Yices2; veriT; CVC4; opensmt2; z3-4.5.0n; mathsat-5.4.1n; SMTInterpol | |||||
| QF_UFBV | 5 | 31 | 155 | 100 | Boolector; Yices2; CVC4; mathsat-5.4.1n; z3-4.5.0n |
| Boolector; Yices2; CVC4; mathsat-5.4.1n; z3-4.5.0n | |||||
| QF_UFIDL | 5 | 428 | 2140 | 100 | Yices2; z3-4.5.0n; SMTInterpol; veriT; CVC4 |
| Yices2; z3-4.5.0n; SMTInterpol; veriT; CVC4 | |||||
| QF_UFLIA | 6 | 583 | 3498 | 100 | Yices2; z3-4.5.0n; CVC4; SMTInterpol; mathsat-5.4.1n; veriT |
| Yices2; z3-4.5.0n; CVC4; SMTInterpol; mathsat-5.4.1n; veriT | |||||
| QF_UFLRA | 6 | 1284 | 7704 | 100 | Yices2; z3-4.5.0n; mathsat-5.4.1n; veriT; CVC4; SMTInterpol |
| Yices2; z3-4.5.0n; mathsat-5.4.1n; veriT; CVC4; SMTInterpol | |||||
| QF_UFNIA | 3 | 7 | 21 | 100 | Yices2; CVC4; z3-4.5.0n |
| Yices2; CVC4; z3-4.5.0n | |||||
| QF_UFNRA | 4 | 36 | 144 | 100 | z3-4.5.0n; Yices2; CVC4; veriT+raSAT+Redlog |
| z3-4.5.0n; Yices2; CVC4; veriT+raSAT+Redlog | |||||
| UF | 4 | 7562 | 30248 | 100 | vampire 4.2; CVC4; veriT; z3-4.5.0n |
| vampire 4.2; CVC4; veriT; z3-4.5.0n | |||||
| UFBV | 2 | 200 | 400 | 100 | z3-4.5.0n; CVC4 |
| z3-4.5.0n; CVC4 | |||||
| UFDT | 2 | 4535 | 9070 | 100 | CVC4; vampire 4.2 |
| CVC4; vampire 4.2 | |||||
| UFDTLIA | 2 | 303 | 606 | 100 | vampire 4.2; CVC4 |
| vampire 4.2; CVC4 | |||||
| UFIDL | 4 | 68 | 272 | 100 | CVC4; z3-4.5.0n; veriT; vampire 4.2 |
| CVC4; z3-4.5.0n; veriT; vampire 4.2 | |||||
| UFLIA | 4 | 10136 | 40544 | 100 | CVC4; vampire 4.2; veriT; z3-4.5.0n |
| CVC4; vampire 4.2; veriT; z3-4.5.0n | |||||
| UFLRA | 4 | 15 | 60 | 100 | z3-4.5.0n; CVC4; veriT; vampire 4.2 |
| z3-4.5.0n; CVC4; vampire 4.2; veriT | |||||
| UFNIA | 3 | 3308 | 9924 | 100 | vampire 4.2; CVC4; z3-4.5.0n |
| vampire 4.2; CVC4; z3-4.5.0n | |||||
n. Non-competing.