The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Summary of all competition results for the Single Query Track.
Results are given ranked by performance for each scoring scheme
(best solver is given as left-most solver).
| Scoring Scheme | Winner | Ranking |
|---|---|---|
| Sequential Performance | cvc5 | 2021-z3n, z3-4.8.17n, cvc5, YicesQS, UltimateEliminator+MathSAT, Vampire, smtinterpol, veriT |
| Parallel Performance | cvc5 | 2021-z3n, z3-4.8.17n, cvc5, YicesQS, UltimateEliminator+MathSAT, Vampire, smtinterpol, veriT |
| SAT Performance | YicesQS | 2021-z3n, z3-4.8.17n, YicesQS, cvc5, UltimateEliminator+MathSAT, smtinterpol, Vampire, veriT |
| UNSAT Performance | cvc5 | cvc5, 2021-z3n, z3-4.8.17n, YicesQS, Vampire, UltimateEliminator+MathSAT, smtinterpol, veriT |
| 24s Performance | YicesQS | YicesQS, 2021-z3n, z3-4.8.17n, cvc5, UltimateEliminator+MathSAT, Vampire, smtinterpol, veriT |
| Scoring Scheme | Winner | Ranking |
|---|---|---|
| Sequential Performance | cvc5 | 2019-Par4n, cvc5, Q3B, z3-4.8.17n, Bitwuzla, Q3B-pBDD, YicesQS, UltimateEliminator+MathSAT |
| Parallel Performance | cvc5 | 2019-Par4n, cvc5, Q3B, z3-4.8.17n, Bitwuzla, Q3B-pBDD, YicesQS, UltimateEliminator+MathSAT |
| SAT Performance | cvc5 | 2019-Par4n, cvc5, Q3B, z3-4.8.17n, Bitwuzla, YicesQS, Q3B-pBDD, UltimateEliminator+MathSAT |
| UNSAT Performance | cvc5 | 2019-Par4n, cvc5, Q3B, Q3B-pBDD, z3-4.8.17n, Bitwuzla, YicesQS, UltimateEliminator+MathSAT |
| 24s Performance | Q3B | 2019-Par4n, Q3B, z3-4.8.17n, Q3B-pBDD, cvc5, Bitwuzla, YicesQS, UltimateEliminator+MathSAT |
| Scoring Scheme | Winner | Ranking |
|---|---|---|
| Sequential Performance | cvc5 | cvc5, z3-4.8.17n, 2020-CVC4n, Vampire, veriT, UltimateEliminator+MathSAT, smtinterpol, smtinterpol-fixedn |
| Parallel Performance | cvc5 | cvc5, z3-4.8.17n, 2020-CVC4n, Vampire, veriT, UltimateEliminator+MathSAT, smtinterpol, smtinterpol-fixedn |
| SAT Performance | cvc5 | z3-4.8.17n, cvc5, 2020-CVC4n, Vampire, UltimateEliminator+MathSAT, veriT, smtinterpol, smtinterpol-fixedn |
| UNSAT Performance | cvc5 | cvc5, 2020-CVC4n, Vampire, z3-4.8.17n, smtinterpol, smtinterpol-fixedn, veriT, UltimateEliminator+MathSAT |
| 24s Performance | cvc5 | z3-4.8.17n, cvc5, 2020-CVC4n, Vampire, smtinterpol, smtinterpol-fixedn, veriT, UltimateEliminator+MathSAT |
| Scoring Scheme | Winner | Ranking |
|---|---|---|
| Sequential Performance | cvc5 | z3-4.8.17n, cvc5, 2021-cvc5n, Bitwuzla, UltimateEliminator+MathSAT |
| Parallel Performance | cvc5 | z3-4.8.17n, cvc5, 2021-cvc5n, Bitwuzla, UltimateEliminator+MathSAT |
| SAT Performance | cvc5 | z3-4.8.17n, cvc5, 2021-cvc5n, Bitwuzla, UltimateEliminator+MathSAT |
| UNSAT Performance | cvc5 | z3-4.8.17n, cvc5, 2021-cvc5n, Bitwuzla, UltimateEliminator+MathSAT |
| 24s Performance | cvc5 | z3-4.8.17n, cvc5, 2021-cvc5n, Bitwuzla, UltimateEliminator+MathSAT |
| Scoring Scheme | Winner | Ranking |
|---|---|---|
| Sequential Performance | cvc5 | cvc5, 2020-CVC4n, z3-4.8.17n, Vampire, UltimateEliminator+MathSAT |
| Parallel Performance | cvc5 | cvc5, 2020-CVC4n, z3-4.8.17n, Vampire, UltimateEliminator+MathSAT |
| SAT Performance | cvc5 | cvc5, 2020-CVC4n, z3-4.8.17n, UltimateEliminator+MathSAT, Vampire |
| UNSAT Performance | cvc5 | cvc5, 2020-CVC4n, Vampire, z3-4.8.17n, UltimateEliminator+MathSAT |
| 24s Performance | cvc5 | cvc5, 2020-CVC4n, z3-4.8.17n, Vampire, UltimateEliminator+MathSAT |
| Scoring Scheme | Winner | Ranking |
|---|---|---|
| Sequential Performance | cvc5 | cvc5, 2020-CVC4n, Vampire, z3-4.8.17n, veriT, Yices2, smtinterpol, UltimateEliminator+MathSAT |
| Parallel Performance | cvc5 | cvc5, 2020-CVC4n, Vampire, z3-4.8.17n, veriT, Yices2, smtinterpol, UltimateEliminator+MathSAT |
| SAT Performance | cvc5 | 2020-CVC4n, cvc5, Vampire, z3-4.8.17n, Yices2, smtinterpol, UltimateEliminator+MathSAT, veriT |
| UNSAT Performance | cvc5 | cvc5, 2020-CVC4n, Vampire, veriT, z3-4.8.17n, Yices2, smtinterpol, UltimateEliminator+MathSAT |
| 24s Performance | Vampire | Vampire, cvc5, 2020-CVC4n, z3-4.8.17n, veriT, Yices2, smtinterpol, UltimateEliminator+MathSAT |
| Scoring Scheme | Winner | Ranking |
|---|---|---|
| Sequential Performance | Bitwuzla | Bitwuzla, z3-4.8.17n, cvc5, 2021-cvc5n, UltimateEliminator+MathSAT |
| Parallel Performance | Bitwuzla | Bitwuzla, z3-4.8.17n, cvc5, 2021-cvc5n, UltimateEliminator+MathSAT |
| SAT Performance | Bitwuzla | z3-4.8.17n, Bitwuzla, cvc5, 2021-cvc5n, UltimateEliminator+MathSAT |
| UNSAT Performance | Bitwuzla | Bitwuzla, 2021-cvc5n, cvc5, z3-4.8.17n, UltimateEliminator+MathSAT |
| 24s Performance | Bitwuzla | Bitwuzla, cvc5, 2021-cvc5n, z3-4.8.17n, UltimateEliminator+MathSAT |
| Scoring Scheme | Winner | Ranking |
|---|---|---|
| Sequential Performance | Bitwuzla | STP-fixedn, 2020-Bitwuzla-fixedn, Bitwuzla, Yices2, STP, cvc5, Z3++BV, MathSATn, z3-4.8.17n |
| Parallel Performance | Bitwuzla | STP-fixedn, 2020-Bitwuzla-fixedn, Bitwuzla, Yices2, STP, cvc5, Z3++BV, MathSATn, z3-4.8.17n |
| SAT Performance | Bitwuzla | STP-fixedn, 2020-Bitwuzla-fixedn, Bitwuzla, Yices2, STP, Z3++BV, cvc5, z3-4.8.17n, MathSATn |
| UNSAT Performance | STP | STP, STP-fixedn, 2020-Bitwuzla-fixedn, Bitwuzla, Yices2, cvc5, MathSATn, Z3++BV, z3-4.8.17n |
| 24s Performance | STP | STP-fixedn, STP, Bitwuzla, 2020-Bitwuzla-fixedn, Yices2, Z3++BV, cvc5, MathSATn, z3-4.8.17n |
| Scoring Scheme | Winner | Ranking |
|---|---|---|
| Sequential Performance | cvc5 | z3-4.8.17n, 2021-z3n, cvc5, smtinterpol |
| Parallel Performance | cvc5 | z3-4.8.17n, 2021-z3n, cvc5, smtinterpol |
| SAT Performance | cvc5 | cvc5, z3-4.8.17n, 2021-z3n, smtinterpol |
| UNSAT Performance | cvc5 | z3-4.8.17n, 2021-z3n, cvc5, smtinterpol |
| 24s Performance | smtinterpol | z3-4.8.17n, 2021-z3n, smtinterpol, cvc5 |
| Scoring Scheme | Winner | Ranking |
|---|---|---|
| Sequential Performance | Bitwuzla | Bitwuzla, 2020-Bitwuzlan, Yices2, z3-4.8.17n, cvc5, MathSATn |
| Parallel Performance | Bitwuzla | Bitwuzla, 2020-Bitwuzlan, Yices2, z3-4.8.17n, cvc5, MathSATn |
| SAT Performance | Bitwuzla | 2020-Bitwuzlan, Bitwuzla, Yices2, MathSATn, cvc5, z3-4.8.17n |
| UNSAT Performance | Bitwuzla | Bitwuzla, 2020-Bitwuzlan, Yices2, z3-4.8.17n, cvc5, MathSATn |
| 24s Performance | Bitwuzla | Bitwuzla, 2020-Bitwuzlan, Yices2, MathSATn, z3-4.8.17n, cvc5 |
| Scoring Scheme | Winner | Ranking |
|---|---|---|
| Sequential Performance | smtinterpol | z3-4.8.17n, 2021-SMTInterpoln, smtinterpol, Yices2, cvc5, MathSATn, veriT, OpenSMT |
| Parallel Performance | smtinterpol | z3-4.8.17n, 2021-SMTInterpoln, smtinterpol, Yices2, cvc5, MathSATn, veriT, OpenSMT |
| SAT Performance | smtinterpol | smtinterpol, 2021-SMTInterpoln, z3-4.8.17n, Yices2, cvc5, MathSATn, veriT, OpenSMT |
| UNSAT Performance | Yices2 | z3-4.8.17n, Yices2, MathSATn, 2021-SMTInterpoln, cvc5, smtinterpol, veriT, OpenSMT |
| 24s Performance | Yices2 | z3-4.8.17n, Yices2, 2021-SMTInterpoln, smtinterpol, MathSATn, cvc5, veriT, OpenSMT |
| Scoring Scheme | Winner | Ranking |
|---|---|---|
| Sequential Performance | cvc5 | 2020-CVC4n, cvc5, z3-4.8.17n, MathSATn, Yices2, smtinterpol, veriT+raSAT+Redlog |
| Parallel Performance | cvc5 | 2020-CVC4n, cvc5, z3-4.8.17n, MathSATn, Yices2, smtinterpol, veriT+raSAT+Redlog |
| SAT Performance | cvc5 | 2020-CVC4n, cvc5, z3-4.8.17n, Yices2, MathSATn, smtinterpol, veriT+raSAT+Redlog |
| UNSAT Performance | cvc5 | z3-4.8.17n, 2020-CVC4n, cvc5, MathSATn, Yices2, smtinterpol, veriT+raSAT+Redlog |
| 24s Performance | cvc5 | z3-4.8.17n, 2020-CVC4n, cvc5, MathSATn, Yices2, smtinterpol, veriT+raSAT+Redlog |
| Scoring Scheme | Winner | Ranking |
|---|---|---|
| Sequential Performance | Yices2 | Yices2, OpenSMT, z3-4.8.17n, 2021-z3n, cvc5, smtinterpol, MathSATn, veriT, OpenSMT-fixedn |
| Parallel Performance | Yices2 | Yices2, OpenSMT, z3-4.8.17n, 2021-z3n, cvc5, smtinterpol, MathSATn, veriT, OpenSMT-fixedn |
| SAT Performance | Yices2 | Yices2, z3-4.8.17n, 2021-z3n, OpenSMT, cvc5, smtinterpol, MathSATn, veriT, OpenSMT-fixedn |
| UNSAT Performance | Yices2 | Yices2, OpenSMT, z3-4.8.17n, 2021-z3n, cvc5, MathSATn, smtinterpol, veriT, OpenSMT-fixedn |
| 24s Performance | Yices2 | Yices2, z3-4.8.17n, 2021-z3n, cvc5, OpenSMT, MathSATn, smtinterpol, veriT, OpenSMT-fixedn |
| Scoring Scheme | Winner | Ranking |
|---|---|---|
| Sequential Performance | Bitwuzla | Bitwuzla, cvc5, 2021-cvc5n, MathSATn, z3-4.8.17n, COLIBRI |
| Parallel Performance | Bitwuzla | Bitwuzla, cvc5, 2021-cvc5n, MathSATn, z3-4.8.17n, COLIBRI |
| SAT Performance | Bitwuzla | Bitwuzla, cvc5, 2021-cvc5n, MathSATn, COLIBRI, z3-4.8.17n |
| UNSAT Performance | Bitwuzla | Bitwuzla, 2021-cvc5n, cvc5, MathSATn, z3-4.8.17n, COLIBRI |
| 24s Performance | Bitwuzla | Bitwuzla, COLIBRI, MathSATn, 2021-cvc5n, cvc5, z3-4.8.17n |
| Scoring Scheme | Winner | Ranking |
|---|---|---|
| Sequential Performance | OpenSMT | 2019-Par4n, OpenSMT, Z3++, cvc5, Yices2, MathSATn, z3-4.8.17n, smtinterpol, veriT |
| Parallel Performance | OpenSMT | 2019-Par4n, OpenSMT, Z3++, cvc5, Yices2, MathSATn, z3-4.8.17n, smtinterpol, veriT |
| SAT Performance | Z3++ | 2019-Par4n, Z3++, z3-4.8.17n, OpenSMT, Yices2, cvc5, MathSATn, smtinterpol, veriT |
| UNSAT Performance | cvc5 | 2019-Par4n, cvc5, OpenSMT, Yices2, MathSATn, smtinterpol, Z3++, z3-4.8.17n, veriT |
| 24s Performance | Yices2 | 2019-Par4n, Yices2, z3-4.8.17n, Z3++, MathSATn, OpenSMT, cvc5, smtinterpol, veriT |
| Scoring Scheme | Winner | Ranking |
|---|---|---|
| Sequential Performance | Yices2 | 2021-Yices2n, Yices2, cvc5, OpenSMT, z3-4.8.17n, veriT, MathSATn, smtinterpol, solsmt |
| Parallel Performance | Yices2 | Yices2, 2021-Yices2n, cvc5, OpenSMT, z3-4.8.17n, veriT, MathSATn, smtinterpol, solsmt |
| SAT Performance | Yices2 | Yices2, 2021-Yices2n, OpenSMT, cvc5, z3-4.8.17n, smtinterpol, MathSATn, veriT, solsmt |
| UNSAT Performance | cvc5 | cvc5, Yices2, 2021-Yices2n, OpenSMT, veriT, z3-4.8.17n, MathSATn, smtinterpol, solsmt |
| 24s Performance | Yices2 | Yices2, 2021-Yices2n, OpenSMT, z3-4.8.17n, veriT, MathSATn, cvc5, smtinterpol, solsmt |
| Scoring Scheme | Winner | Ranking |
|---|---|---|
| Sequential Performance | cvc5 | Z3++-fixedn, Yices-ismt-fixedn, 2019-Par4n, z3-4.8.17n, MathSATn, cvc5, Yices2, Z3++, Yices-ismt |
| Parallel Performance | cvc5 | Z3++-fixedn, Yices-ismt-fixedn, 2019-Par4n, z3-4.8.17n, MathSATn, cvc5, Yices2, Z3++, Yices-ismt |
| SAT Performance | cvc5 | Yices-ismt-fixedn, Z3++-fixedn, 2019-Par4n, z3-4.8.17n, cvc5, MathSATn, Yices2, Z3++, Yices-ismt |
| UNSAT Performance | Z3++ | Z3++, Z3++-fixedn, 2019-Par4n, z3-4.8.17n, Yices-ismt-fixedn, Yices-ismt, Yices2, MathSATn, cvc5 |
| 24s Performance | Yices2 | 2019-Par4n, Yices2, Yices-ismt, Yices-ismt-fixedn, Z3++-fixedn, Z3++, z3-4.8.17n, MathSATn, cvc5 |
| Scoring Scheme | Winner | Ranking |
|---|---|---|
| Sequential Performance | cvc5 | Z3++-fixedn, 2019-Par4n, cvc5, NRA-LS, Yices2, z3-4.8.17n, SMT-RAT-MCSAT 22.06, veriT+raSAT+Redlog, MathSATn, Z3++ |
| Parallel Performance | cvc5 | 2019-Par4n, Z3++-fixedn, cvc5, NRA-LS, Yices2, z3-4.8.17n, SMT-RAT-MCSAT 22.06, veriT+raSAT+Redlog, MathSATn, Z3++ |
| SAT Performance | Z3++ | Z3++-fixedn, Z3++, 2019-Par4n, cvc5, z3-4.8.17n, NRA-LS, Yices2, SMT-RAT-MCSAT 22.06, veriT+raSAT+Redlog, MathSATn |
| UNSAT Performance | cvc5 | 2019-Par4n, Z3++-fixedn, cvc5, NRA-LS, Yices2, MathSATn, SMT-RAT-MCSAT 22.06, z3-4.8.17n, veriT+raSAT+Redlog, Z3++ |
| 24s Performance | cvc5 | 2019-Par4n, cvc5, Z3++-fixedn, NRA-LS, Yices2, z3-4.8.17n, SMT-RAT-MCSAT 22.06, veriT+raSAT+Redlog, MathSATn, Z3++ |
| Scoring Scheme | Winner | Ranking |
|---|---|---|
| Sequential Performance | cvc5 | cvc5, 2020-CVC4n, z3-4.8.17n, Z3str4, OSTRICH |
| Parallel Performance | cvc5 | cvc5, 2020-CVC4n, z3-4.8.17n, Z3str4, OSTRICH |
| SAT Performance | cvc5 | cvc5, 2020-CVC4n, z3-4.8.17n, Z3str4, OSTRICH |
| UNSAT Performance | cvc5 | 2020-CVC4n, cvc5, Z3str4, z3-4.8.17n, OSTRICH |
| 24s Performance | cvc5 | cvc5, 2020-CVC4n, Z3str4, z3-4.8.17n, OSTRICH |