The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results as of Fri Oct 30 12:49:29 GMT
| 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 | Z3n; CVC4 (exp); CVC4; veriT; CVC3 |
| Z3n; CVC4 (exp); CVC4; veriT; CVC3 | |||||
| Z3n; CVC4 (exp); CVC4; veriT; CVC3 | |||||
| Z3n; CVC4 (exp); CVC4; veriT; CVC3 | |||||
| AUFLIA | 5 | 4 | 20 | 100 | CVC4 (exp); CVC3; CVC4; Z3n; veriT |
| CVC4 (exp); CVC3; CVC4; Z3n; veriT | |||||
| CVC4; CVC4 (exp); Z3n; CVC3; veriT | |||||
| CVC4; Z3n; CVC4 (exp); CVC3; veriT | |||||
| AUFLIRA | 5 | 19849 | 99245 | 100 | Z3n; CVC4 (exp); CVC4; CVC3; veriT |
| Z3n; CVC4 (exp); CVC4; CVC3; veriT | |||||
| Z3n; CVC4; CVC4 (exp); CVC3; veriT | |||||
| Z3n; CVC4; CVC4 (exp); CVC3; veriT | |||||
| AUFNIRA | 4 | 1050 | 4200 | 100 | CVC4; CVC4 (exp); Z3n; CVC3 |
| CVC4; CVC4 (exp); Z3n; CVC3 | |||||
| CVC4; CVC4 (exp); Z3n; CVC3 | |||||
| CVC4; CVC4 (exp); Z3n; CVC3 | |||||
| BV | 4 | 85 | 340 | 100 | Z3n; CVC4; CVC4 (exp); CVC3 |
| Z3n; CVC4 (exp); CVC4; CVC3 | |||||
| Z3n; CVC4; CVC4 (exp); CVC3 | |||||
| Z3n; CVC4 (exp); CVC4; CVC3 | |||||
| LIA | 5 | 201 | 1005 | 100 | CVC4 (exp); Z3n; CVC4; CVC3; veriT |
| CVC4 (exp); Z3n; CVC4; CVC3; veriT | |||||
| CVC4 (exp); Z3n; CVC4; CVC3; veriT | |||||
| CVC4 (exp); Z3n; CVC4; CVC3; veriT | |||||
| LRA | 5 | 339 | 1695 | 100 | CVC4 (exp); CVC4; Z3n; CVC3; veriT |
| CVC4 (exp); CVC4; Z3n; CVC3; veriT | |||||
| CVC4; CVC4 (exp); Z3n; CVC3; veriT | |||||
| CVC4 (exp); CVC4; Z3n; CVC3; veriT | |||||
| NIA | 4 | 9 | 36 | 100 | Z3n; CVC4; CVC4 (exp); CVC3 |
| Z3n; CVC4; CVC4 (exp); CVC3 | |||||
| Z3n; CVC4; CVC4 (exp); CVC3 | |||||
| Z3n; CVC4; CVC4 (exp); CVC3 | |||||
| NRA | 4 | 3788 | 15152 | 100 | CVC4 (exp); CVC4; CVC3; Z3n |
| CVC4 (exp); CVC4; CVC3; Z3n | |||||
| CVC4 (exp); CVC4; CVC3; Z3n | |||||
| CVC4 (exp); CVC4; CVC3; Z3n | |||||
| QF_ABV | 6 | 14720 | 88320 | 100 | Boolector (QF_AUFBV); Yices; MathSatn; CVC4 (exp); CVC4; Z3n |
| Boolector (QF_AUFBV); Yices; MathSatn; CVC4 (exp); CVC4; Z3n | |||||
| Boolector (QF_AUFBV); Yices; MathSatn; CVC4 (exp); CVC4; Z3n | |||||
| Boolector (QF_AUFBV); Yices; MathSatn; CVC4 (exp); CVC4; Z3n | |||||
| QF_ALIA | 7 | 134 | 938 | 100 | Yices; MathSatn; SMTInterpol; CVC4 (exp); Z3n; CVC4; veriT |
| Yices; MathSatn; SMTInterpol; CVC4 (exp); Z3n; CVC4; veriT | |||||
| Yices; MathSatn; SMTInterpol; CVC4 (exp); Z3n; CVC4; veriT | |||||
| Yices; MathSatn; SMTInterpol; CVC4 (exp); Z3n; CVC4; veriT | |||||
| QF_ANIA | 3 | 6 | 18 | 100 | Z3n; CVC4 (exp); CVC4 |
| Z3n; CVC4 (exp); CVC4 | |||||
| Z3n; CVC4 (exp); CVC4 | |||||
| Z3n; CVC4 (exp); CVC4 | |||||
| QF_AUFBV | 6 | 37 | 222 | 100 | MathSatn; CVC4; CVC4 (exp); Yices; Boolector (QF_AUFBV); Z3n |
| MathSatn; CVC4; CVC4 (exp); Yices; Boolector (QF_AUFBV); Z3n | |||||
| MathSatn; CVC4; CVC4 (exp); Yices; Boolector (QF_AUFBV); Z3n | |||||
| MathSatn; CVC4; CVC4 (exp); Yices; Boolector (QF_AUFBV); Z3n | |||||
| QF_AUFLIA | 7 | 1009 | 7063 | 100 | Yices; Z3n; MathSatn; CVC4 (exp); CVC4; SMTInterpol; veriT |
| Yices; Z3n; MathSatn; CVC4 (exp); SMTInterpol; CVC4; veriT | |||||
| Z3n; Yices; SMTInterpol; CVC4 (exp); MathSatn; CVC4; veriT | |||||
| Z3n; Yices; SMTInterpol; CVC4 (exp); MathSatn; CVC4; veriT | |||||
| QF_AUFNIA | 3 | 21 | 63 | 100 | CVC4; CVC4 (exp); Z3n |
| CVC4; CVC4 (exp); Z3n | |||||
| CVC4; CVC4 (exp); Z3n | |||||
| CVC4; CVC4 (exp); Z3n | |||||
| QF_AX | 7 | 551 | 3857 | 100 | Yices; MathSatn; Z3n; CVC4 (exp); CVC4; SMTInterpol; veriT |
| Yices; MathSatn; Z3n; CVC4 (exp); CVC4; SMTInterpol; veriT | |||||
| - | |||||
| - | |||||
| QF_BV | 11 | 26414 | 290554 | 100 | Boolector (QF_BV); CVC4 (exp); STP-CMSat4; Z3n; CVC4; MathSatn; Yices; STP-CMSat4 (mt-v15); SMT-RAT; STP-CMSat4 (v15); STP-MiniSAT (v15) |
| Boolector (QF_BV); CVC4 (exp); STP-CMSat4; Z3n; CVC4; MathSatn; Yices; STP-CMSat4 (mt-v15); SMT-RAT; STP-CMSat4 (v15); STP-MiniSAT (v15) | |||||
| Boolector (QF_BV); Z3n; STP-CMSat4; Yices; CVC4 (exp); MathSatn; CVC4; STP-CMSat4 (mt-v15); SMT-RAT; STP-CMSat4 (v15); STP-MiniSAT (v15) | |||||
| Boolector (QF_BV); Z3n; CVC4 (exp); STP-CMSat4; Yices; MathSatn; CVC4; STP-CMSat4 (mt-v15); SMT-RAT; STP-CMSat4 (v15); STP-MiniSAT (v15) | |||||
| QF_BVFP | 3 | 7 | 21 | 100 | Z3 (FP); MathSatn; Z3 (ijcar14) |
| Z3 (FP); MathSatn; Z3 (ijcar14) | |||||
| - | |||||
| - | |||||
| QF_FP | 3 | 34413 | 103239 | 100 | Z3 (FP); Z3 (ijcar14); MathSatn |
| Z3 (FP); Z3 (ijcar14); MathSatn | |||||
| - | |||||
| - | |||||
| QF_IDL | 6 | 2094 | 12564 | 100 | Z3n; Yices; CVC4 (exp); CVC4; SMTInterpol; veriT |
| Z3n; Yices; CVC4 (exp); CVC4; SMTInterpol; veriT | |||||
| Z3n; Yices; CVC4 (exp); CVC4; veriT; SMTInterpol | |||||
| Z3n; Yices; CVC4 (exp); CVC4; veriT; SMTInterpol | |||||
| QF_LIA | 8 | 5839 | 46712 | 100 | MathSatn; CVC4 (exp); CVC4; Yices; Z3n; SMTInterpol; SMT-RAT; veriT |
| MathSatn; CVC4 (exp); CVC4; Yices; Z3n; SMTInterpol; SMT-RAT; veriT | |||||
| Z3n; MathSatn; Yices; CVC4 (exp); CVC4; SMTInterpol; veriT; SMT-RAT | |||||
| Z3n; MathSatn; Yices; CVC4 (exp); CVC4; SMTInterpol; veriT; SMT-RAT | |||||
| QF_LIRA | 6 | 6 | 36 | 100 | Yices; CVC4; CVC4 (exp); Z3n; SMT-RAT; SMTInterpol |
| Yices; CVC4; CVC4 (exp); Z3n; SMT-RAT; SMTInterpol | |||||
| Yices; CVC4; CVC4 (exp); Z3n; SMT-RAT; SMTInterpol | |||||
| Yices; CVC4; CVC4 (exp); Z3n; SMT-RAT; SMTInterpol | |||||
| QF_LRA | 8 | 1626 | 13008 | 100 | CVC4; CVC4 (exp); Yices; MathSatn; veriT; Z3n; SMTInterpol; SMT-RAT |
| CVC4; CVC4 (exp); Yices; MathSatn; veriT; Z3n; SMTInterpol; SMT-RAT | |||||
| CVC4; CVC4 (exp); Yices; MathSatn; veriT; Z3n; SMTInterpol; SMT-RAT | |||||
| CVC4; CVC4 (exp); Yices; MathSatn; veriT; Z3n; SMTInterpol; SMT-RAT | |||||
| QF_NIA | 8 | 8475 | 67800 | 100 | Z3n; AProVE; raSAT; SMT-RAT (parallel); SMT-RAT; CVC3; CVC4; CVC4 (exp) |
| Z3n; AProVE; raSAT; SMT-RAT (parallel); SMT-RAT; CVC3; CVC4; CVC4 (exp) | |||||
| Z3n; AProVE; raSAT; SMT-RAT (parallel); SMT-RAT; CVC3; CVC4; CVC4 (exp) | |||||
| Z3n; AProVE; raSAT; SMT-RAT (parallel); SMT-RAT; CVC3; CVC4; CVC4 (exp) | |||||
| QF_NIRA | 4 | 2 | 8 | 100 | CVC4 (exp); CVC4; SMT-RAT; Z3n |
| CVC4 (exp); CVC4; SMT-RAT; Z3n | |||||
| CVC4 (exp); CVC4; SMT-RAT; Z3n | |||||
| CVC4 (exp); CVC4; SMT-RAT; Z3n | |||||
| QF_NRA | 7 | 10184 | 71288 | 100 | Z3n; Yices2-NL; SMT-RAT; raSAT; CVC3; CVC4 (exp); CVC4 |
| Z3n; Yices2-NL; SMT-RAT; raSAT; CVC3; CVC4; CVC4 (exp) | |||||
| Z3n; Yices2-NL; SMT-RAT; raSAT; CVC3; CVC4 (exp); CVC4 | |||||
| Z3n; Yices2-NL; SMT-RAT; raSAT; CVC3; CVC4; CVC4 (exp) | |||||
| QF_RDL | 6 | 220 | 1320 | 100 | Yices; Z3n; veriT; CVC4 (exp); CVC4; SMTInterpol |
| Yices; Z3n; veriT; CVC4 (exp); CVC4; SMTInterpol | |||||
| Yices; Z3n; CVC4; CVC4 (exp); veriT; SMTInterpol | |||||
| Yices; Z3n; CVC4; CVC4 (exp); veriT; SMTInterpol | |||||
| QF_UF | 10 | 6649 | 66490 | 100 | Yices; veriT; CVC4; CVC4 (exp); OpenSMT2; Z3n; MathSatn; SMTInterpol; SMT-RAT; OpenSMT2 (parallel) |
| Yices; veriT; CVC4; CVC4 (exp); OpenSMT2; Z3n; MathSatn; SMTInterpol; SMT-RAT; OpenSMT2 (parallel) | |||||
| Yices; veriT; SMT-RAT; CVC4 (exp); CVC4; OpenSMT2 (parallel); OpenSMT2; MathSatn; Z3n; SMTInterpol | |||||
| Yices; CVC4; SMT-RAT; veriT; CVC4 (exp); OpenSMT2 (parallel); OpenSMT2; MathSatn; Z3n; SMTInterpol | |||||
| QF_UFBV | 6 | 31 | 186 | 100 | Boolector (QF_AUFBV); Yices; CVC4 (exp); Z3n; MathSatn; CVC4 |
| Boolector (QF_AUFBV); Yices; CVC4 (exp); Z3n; MathSatn; CVC4 | |||||
| Boolector (QF_AUFBV); Yices; CVC4 (exp); Z3n; MathSatn; CVC4 | |||||
| Boolector (QF_AUFBV); Yices; CVC4 (exp); Z3n; MathSatn; CVC4 | |||||
| QF_UFIDL | 6 | 441 | 2646 | 100 | Yices; Z3n; SMTInterpol; veriT; CVC4 (exp); CVC4 |
| Yices; Z3n; SMTInterpol; veriT; CVC4 (exp); CVC4 | |||||
| Yices; Z3n; SMTInterpol; CVC4 (exp); CVC4; veriT | |||||
| Yices; Z3n; SMTInterpol; CVC4 (exp); CVC4; veriT | |||||
| QF_UFLIA | 7 | 598 | 4186 | 100 | Z3n; Yices; CVC4; CVC4 (exp); MathSatn; SMTInterpol; veriT |
| Z3n; Yices; CVC4; CVC4 (exp); MathSatn; SMTInterpol; veriT | |||||
| Z3n; Yices; CVC4; CVC4 (exp); MathSatn; SMTInterpol; veriT | |||||
| Z3n; Yices; CVC4; CVC4 (exp); SMTInterpol; MathSatn; veriT | |||||
| QF_UFLRA | 7 | 1627 | 11389 | 100 | Yices; Z3n; MathSatn; CVC4 (exp); CVC4; SMTInterpol; veriT |
| Yices; Z3n; MathSatn; CVC4 (exp); CVC4; SMTInterpol; veriT | |||||
| Yices; Z3n; MathSatn; CVC4 (exp); CVC4; SMTInterpol; veriT | |||||
| Yices; Z3n; MathSatn; CVC4 (exp); CVC4; SMTInterpol; veriT | |||||
| QF_UFNIA | 4 | 7 | 28 | 100 | CVC4 (exp); CVC4; Z3n; CVC3 |
| CVC4 (exp); CVC4; Z3n; CVC3 | |||||
| CVC4 (exp); CVC4; Z3n; CVC3 | |||||
| CVC4 (exp); CVC4; Z3n; CVC3 | |||||
| QF_UFNRA | 4 | 34 | 136 | 100 | Z3n; CVC3; CVC4 (exp); CVC4 |
| Z3n; CVC3; CVC4 (exp); CVC4 | |||||
| Z3n; CVC3; CVC4 (exp); CVC4 | |||||
| Z3n; CVC3; CVC4 (exp); CVC4 | |||||
| UF | 5 | 2839 | 14195 | 100 | CVC4 (exp); CVC4; Z3n; CVC3; veriT |
| CVC4 (exp); CVC4; Z3n; CVC3; veriT | |||||
| CVC4 (exp); CVC4; Z3n; CVC3; veriT | |||||
| CVC4 (exp); CVC4; Z3n; CVC3; veriT | |||||
| UFBV | 4 | 71 | 284 | 100 | Z3n; CVC4; CVC4 (exp); CVC3 |
| Z3n; CVC4; CVC4 (exp); CVC3 | |||||
| Z3n; CVC4; CVC4 (exp); CVC3 | |||||
| Z3n; CVC4; CVC4 (exp); CVC3 | |||||
| UFIDL | 5 | 68 | 340 | 100 | Z3n; CVC4; CVC4 (exp); veriT; CVC3 |
| Z3n; CVC4; CVC4 (exp); veriT; CVC3 | |||||
| Z3n; CVC4; CVC4 (exp); veriT; CVC3 | |||||
| Z3n; CVC4; CVC4 (exp); veriT; CVC3 | |||||
| UFLIA | 5 | 8404 | 42020 | 100 | CVC4; CVC4 (exp); Z3n; veriT; CVC3 |
| CVC4; CVC4 (exp); Z3n; veriT; CVC3 | |||||
| CVC4; CVC4 (exp); Z3n; veriT; CVC3 | |||||
| CVC4; CVC4 (exp); Z3n; veriT; CVC3 | |||||
| UFLRA | 5 | 25 | 125 | 100 | CVC3; veriT; CVC4; CVC4 (exp); Z3n |
| CVC3; veriT; CVC4; CVC4 (exp); Z3n | |||||
| veriT; CVC3; CVC4 (exp); CVC4; Z3n | |||||
| veriT; CVC3; CVC4; CVC4 (exp); Z3n | |||||
| UFNIA | 4 | 2319 | 9276 | 100 | CVC4; CVC4 (exp); Z3n; CVC3 |
| CVC4; CVC4 (exp); Z3n; CVC3 | |||||
| CVC4; CVC4 (exp); Z3n; CVC3 | |||||
| CVC4; CVC4 (exp); Z3n; CVC3 |
n. Non-competitive.