The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results as of Thu Jul 7 07:24:34 GMT
| Logic | Solvers | Benchmarks | # pairs Complete | % Complete | Order (sequential performance) |
|---|---|---|---|---|---|
| Order (parallel performance) | |||||
| ALIA | 5 | 42 | 210 | 100 | z3n; CVC4; vampire_smt_4.1; vampire_smt_4.1_parallel; veriT-dev |
| z3n; CVC4; vampire_smt_4.1_parallel; vampire_smt_4.1; veriT-dev | |||||
| AUFLIA | 5 | 4 | 20 | 100 | CVC4; vampire_smt_4.1; z3n; vampire_smt_4.1_parallel; veriT-dev |
| CVC4; vampire_smt_4.1; vampire_smt_4.1_parallel; z3n; veriT-dev | |||||
| AUFLIRA | 5 | 19849 | 99245 | 100 | z3n; vampire_smt_4.1; vampire_smt_4.1_parallel; CVC4; veriT-dev |
| z3n; vampire_smt_4.1; vampire_smt_4.1_parallel; CVC4; veriT-dev | |||||
| AUFNIRA | 4 | 1050 | 4200 | 100 | vampire_smt_4.1_parallel; vampire_smt_4.1; z3n; CVC4 |
| vampire_smt_4.1_parallel; vampire_smt_4.1; z3n; CVC4 | |||||
| BV | 4 | 85 | 340 | 100 | Q3B; z3n; CVC4; Boolector |
| Q3B; z3n; CVC4; Boolector | |||||
| LIA | 6 | 201 | 1206 | 100 | CVC4; z3n; vampire_smt_4.1_parallel; vampire_smt_4.1; veriT-dev; ProB |
| CVC4; z3n; vampire_smt_4.1_parallel; vampire_smt_4.1; veriT-dev; ProB | |||||
| LRA | 5 | 339 | 1695 | 100 | CVC4; z3n; vampire_smt_4.1; vampire_smt_4.1_parallel; veriT-dev |
| CVC4; z3n; vampire_smt_4.1; vampire_smt_4.1_parallel; veriT-dev | |||||
| NIA | 5 | 9 | 45 | 100 | z3n; ProB; vampire_smt_4.1_parallel; vampire_smt_4.1; CVC4 |
| z3n; ProB; vampire_smt_4.1_parallel; vampire_smt_4.1; CVC4 | |||||
| NRA | 4 | 3788 | 15152 | 100 | vampire_smt_4.1_parallel; vampire_smt_4.1; z3n; CVC4 |
| vampire_smt_4.1_parallel; vampire_smt_4.1; z3n; CVC4 | |||||
| QF_ABV | 5 | 14720 | 73600 | 100 | Boolector; Yices2; MathSat5n; CVC4; z3n |
| Boolector; Yices2; MathSat5n; CVC4; z3n | |||||
| QF_ALIA | 6 | 139 | 834 | 100 | Yices2; MathSat5n; SMTInterpol; CVC4; z3n; veriT-dev |
| Yices2; MathSat5n; SMTInterpol; CVC4; z3n; veriT-dev | |||||
| QF_ANIA | 2 | 8 | 16 | 100 | CVC4; z3n |
| CVC4; z3n | |||||
| QF_AUFBV | 5 | 37 | 185 | 100 | MathSat5n; CVC4; Yices2; Boolector; z3n |
| MathSat5n; CVC4; Yices2; Boolector; z3n | |||||
| QF_AUFLIA | 6 | 1009 | 6054 | 100 | Yices2; z3n; SMTInterpol; MathSat5n; CVC4; veriT-dev |
| Yices2; z3n; SMTInterpol; MathSat5n; CVC4; veriT-dev | |||||
| QF_AUFNIA | 2 | 21 | 42 | 100 | CVC4; z3n |
| CVC4; z3n | |||||
| QF_AX | 5 | 551 | 2755 | 100 | Yices2; MathSat5n; z3n; CVC4; SMTInterpol |
| Yices2; MathSat5n; z3n; CVC4; SMTInterpol | |||||
| QF_BV | 16 | 26414 | 422624 | 100 | Boolector (preprop); Boolector; stp-cms-st; z3n; stp-cms-exp; CVC4; Minkeyrink; stp-cms-mt; ABC_glucose; Yices2; MathSat5n; MapleSTP; MapleSTP-mt; stp-minisat-st; ABC_default; Q3B |
| Boolector (preprop); Boolector; Minkeyrink; stp-cms-mt; stp-cms-st; CVC4; z3n; stp-cms-exp; ABC_glucose; Yices2; MathSat5n; MapleSTP-mt; MapleSTP; stp-minisat-st; ABC_default; Q3B | |||||
| QF_BVFP | 2 | 7 | 14 | 100 | z3n; MathSat5n |
| z3n; MathSat5n | |||||
| QF_FP | 1 | 34413 | 34413 | 100 | MathSat5n |
| MathSat5n | |||||
| QF_IDL | 5 | 2094 | 10470 | 100 | z3n; Yices2; CVC4; veriT-dev; SMTInterpol |
| z3n; Yices2; CVC4; veriT-dev; SMTInterpol | |||||
| QF_LIA | 8 | 5839 | 46712 | 100 | MathSat5n; CVC4; Yices2; SMTInterpol; z3n; SMT-RAT; veriT-dev; ProB |
| MathSat5n; CVC4; Yices2; SMTInterpol; z3n; SMT-RAT; veriT-dev; ProB | |||||
| QF_LIRA | 4 | 6 | 24 | 100 | Yices2; CVC4; z3n; SMTInterpol |
| Yices2; CVC4; z3n; SMTInterpol | |||||
| QF_LRA | 9 | 1626 | 14634 | 100 | CVC4; Yices2; veriT-dev; MathSat5n; SMTInterpol; z3n; OpenSMT2; SMT-RAT; toysmt |
| CVC4; Yices2; veriT-dev; MathSat5n; SMTInterpol; z3n; OpenSMT2; SMT-RAT; toysmt | |||||
| QF_NIA | 8 | 8593 | 68744 | 100 | z3n; Yices2; CVC4; SMT-RAT; AProVE; raSAT 0.4; raSAT 0.3; ProB |
| z3n; Yices2; CVC4; SMT-RAT; AProVE; raSAT 0.4; ProB; raSAT 0.3 | |||||
| QF_NIRA | 5 | 2 | 10 | 100 | CVC4; z3n; Yices2; raSAT 0.3; raSAT 0.4 |
| CVC4; z3n; Yices2; raSAT 0.3; raSAT 0.4 | |||||
| QF_NRA | 6 | 10245 | 61470 | 100 | z3n; Yices2; raSAT 0.4; raSAT 0.3; CVC4; SMT-RAT |
| z3n; Yices2; raSAT 0.4; CVC4; SMT-RAT; raSAT 0.3 | |||||
| QF_RDL | 7 | 220 | 1540 | 100 | Yices2; veriT-dev; z3n; CVC4; SMTInterpol; OpenSMT2; toysmt |
| Yices2; veriT-dev; z3n; CVC4; SMTInterpol; OpenSMT2; toysmt | |||||
| QF_UF | 8 | 6649 | 53192 | 100 | Yices2; veriT-dev; CVC4; OpenSMT2; z3n; MathSat5n; SMTInterpol; toysmt |
| Yices2; veriT-dev; CVC4; OpenSMT2; z3n; MathSat5n; SMTInterpol; toysmt | |||||
| QF_UFBV | 5 | 31 | 155 | 100 | Boolector; Yices2; CVC4; z3n; MathSat5n |
| Boolector; Yices2; CVC4; z3n; MathSat5n | |||||
| QF_UFIDL | 5 | 441 | 2205 | 100 | Yices2; z3n; SMTInterpol; veriT-dev; CVC4 |
| Yices2; z3n; SMTInterpol; veriT-dev; CVC4 | |||||
| QF_UFLIA | 6 | 598 | 3588 | 100 | z3n; Yices2; CVC4; MathSat5n; SMTInterpol; veriT-dev |
| z3n; Yices2; CVC4; MathSat5n; SMTInterpol; veriT-dev | |||||
| QF_UFLRA | 7 | 1627 | 11389 | 100 | Yices2; z3n; veriT-dev; MathSat5n; CVC4; SMTInterpol; toysmt |
| Yices2; z3n; veriT-dev; MathSat5n; CVC4; SMTInterpol; toysmt | |||||
| QF_UFNIA | 3 | 7 | 21 | 100 | Yices2; CVC4; z3n |
| CVC4; Yices2; z3n | |||||
| QF_UFNRA | 3 | 34 | 102 | 100 | Yices2; z3n; CVC4 |
| Yices2; z3n; CVC4 | |||||
| UF | 5 | 2839 | 14195 | 100 | CVC4; vampire_smt_4.1_parallel; vampire_smt_4.1; veriT-dev; z3n |
| CVC4; vampire_smt_4.1_parallel; vampire_smt_4.1; veriT-dev; z3n | |||||
| UFBV | 3 | 71 | 213 | 100 | z3n; CVC4; Boolector |
| z3n; CVC4; Boolector | |||||
| UFIDL | 5 | 68 | 340 | 100 | CVC4; z3n; vampire_smt_4.1; vampire_smt_4.1_parallel; veriT-dev |
| CVC4; z3n; vampire_smt_4.1; vampire_smt_4.1_parallel; veriT-dev | |||||
| UFLIA | 5 | 8404 | 42020 | 100 | CVC4; vampire_smt_4.1; vampire_smt_4.1_parallel; veriT-dev; z3n |
| CVC4; vampire_smt_4.1; vampire_smt_4.1_parallel; veriT-dev; z3n | |||||
| UFLRA | 5 | 25 | 125 | 100 | z3n; vampire_smt_4.1; veriT-dev; vampire_smt_4.1_parallel; CVC4 |
| z3n; vampire_smt_4.1; vampire_smt_4.1_parallel; veriT-dev; CVC4 | |||||
| UFNIA | 4 | 2319 | 9276 | 100 | vampire_smt_4.1_parallel; vampire_smt_4.1; CVC4; z3n |
| vampire_smt_4.1_parallel; vampire_smt_4.1; CVC4; z3n | |||||
n. Non-competitive.