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 | cvc5, 2021-z3n, YicesQS, UltimateEliminator+MathSAT, iProver Fixedn, SMTInterpol, iProver, Vampire |
| Parallel Performance | cvc5 | cvc5, 2021-z3n, YicesQS, UltimateEliminator+MathSAT, iProver Fixedn, SMTInterpol, iProver, Vampire |
| SAT Performance | YicesQS | 2021-z3n, YicesQS, cvc5, UltimateEliminator+MathSAT, SMTInterpol, Vampire, iProver, iProver Fixedn |
| UNSAT Performance | cvc5 | cvc5, 2021-z3n, YicesQS, UltimateEliminator+MathSAT, iProver Fixedn, SMTInterpol, iProver, Vampire |
| 24s Performance | YicesQS | YicesQS, cvc5, 2021-z3n, UltimateEliminator+MathSAT, iProver Fixedn, SMTInterpol, iProver, Vampire |
| Scoring Scheme | Winner | Ranking |
|---|---|---|
| Sequential Performance | cvc5 | 2019-Par4n, cvc5, Bitwuzla, Bitwuzla Fixedn, YicesQS, UltimateEliminator+MathSAT, UltimateIntBlastingWrapper+SMTInterpol, Q3B |
| Parallel Performance | cvc5 | 2019-Par4n, cvc5, Bitwuzla Fixedn, Bitwuzla, YicesQS, UltimateEliminator+MathSAT, UltimateIntBlastingWrapper+SMTInterpol, Q3B |
| SAT Performance | Bitwuzla | Bitwuzla, Bitwuzla Fixedn, 2019-Par4n, cvc5, YicesQS, UltimateEliminator+MathSAT, UltimateIntBlastingWrapper+SMTInterpol, Q3B |
| UNSAT Performance | cvc5 | 2019-Par4n, cvc5, Q3B, Bitwuzla Fixedn, Bitwuzla, YicesQS, UltimateEliminator+MathSAT, UltimateIntBlastingWrapper+SMTInterpol |
| 24s Performance | Bitwuzla | 2019-Par4n, Bitwuzla Fixedn, Bitwuzla, cvc5, YicesQS, UltimateEliminator+MathSAT, UltimateIntBlastingWrapper+SMTInterpol, Q3B |
| Scoring Scheme | Winner | Ranking |
|---|---|---|
| Sequential Performance | cvc5 | 2022-cvc5n, cvc5, Vampire, SMTInterpol, iProver, iProver Fixedn, UltimateEliminator+MathSAT |
| Parallel Performance | cvc5 | 2022-cvc5n, cvc5, SMTInterpol, iProver, iProver Fixedn, UltimateEliminator+MathSAT, Vampire |
| SAT Performance | cvc5 | 2022-cvc5n, cvc5, SMTInterpol, Vampire, UltimateEliminator+MathSAT, iProver, iProver Fixedn |
| UNSAT Performance | cvc5 | cvc5, 2022-cvc5n, iProver, iProver Fixedn, SMTInterpol, UltimateEliminator+MathSAT, Vampire |
| 24s Performance | cvc5 | cvc5, 2022-cvc5n, Vampire, SMTInterpol, iProver, iProver Fixedn, UltimateEliminator+MathSAT |
| Scoring Scheme | Winner | Ranking |
|---|---|---|
| Sequential Performance | cvc5 | cvc5, 2022-z3-4.8.17n, Bitwuzla Fixedn, Bitwuzla, UltimateEliminator+MathSAT, UltimateIntBlastingWrapper+SMTInterpol |
| Parallel Performance | cvc5 | cvc5, 2022-z3-4.8.17n, Bitwuzla Fixedn, Bitwuzla, UltimateEliminator+MathSAT, UltimateIntBlastingWrapper+SMTInterpol |
| SAT Performance | cvc5 | cvc5, 2022-z3-4.8.17n, Bitwuzla Fixedn, Bitwuzla, UltimateEliminator+MathSAT, UltimateIntBlastingWrapper+SMTInterpol |
| UNSAT Performance | cvc5 | cvc5, Bitwuzla Fixedn, Bitwuzla, 2022-z3-4.8.17n, UltimateIntBlastingWrapper+SMTInterpol, UltimateEliminator+MathSAT |
| 24s Performance | cvc5 | cvc5, 2022-z3-4.8.17n, Bitwuzla Fixedn, Bitwuzla, UltimateEliminator+MathSAT, UltimateIntBlastingWrapper+SMTInterpol |
| Scoring Scheme | Winner | Ranking |
|---|---|---|
| Sequential Performance | cvc5 | cvc5, 2022-cvc5n, Vampire, iProver, iProver Fixedn, UltimateEliminator+MathSAT |
| Parallel Performance | cvc5 | cvc5, 2022-cvc5n, Vampire, iProver, iProver Fixedn, UltimateEliminator+MathSAT |
| SAT Performance | cvc5 | cvc5, 2022-cvc5n, UltimateEliminator+MathSAT, Vampire, iProver, iProver Fixedn |
| UNSAT Performance | cvc5 | cvc5, 2022-cvc5n, Vampire, iProver, iProver Fixedn, UltimateEliminator+MathSAT |
| 24s Performance | cvc5 | cvc5, 2022-cvc5n, Vampire, iProver Fixedn, iProver, UltimateEliminator+MathSAT |
| Scoring Scheme | Winner | Ranking |
|---|---|---|
| Sequential Performance | cvc5 | cvc5, 2022-cvc5n, iProver Fixedn, iProver, Yices2, SMTInterpol, UltimateEliminator+MathSAT, Vampire |
| Parallel Performance | cvc5 | cvc5, 2022-cvc5n, Yices2, SMTInterpol, UltimateEliminator+MathSAT, iProver Fixedn, iProver, Vampire |
| SAT Performance | cvc5 | cvc5, 2022-cvc5n, Vampire, iProver Fixedn, Yices2, SMTInterpol, UltimateEliminator+MathSAT, iProver |
| UNSAT Performance | cvc5 | cvc5, 2022-cvc5n, Yices2, SMTInterpol, UltimateEliminator+MathSAT, iProver, iProver Fixedn, Vampire |
| 24s Performance | Vampire | Vampire, cvc5, 2022-cvc5n, iProver Fixedn, iProver, Yices2, SMTInterpol, UltimateEliminator+MathSAT |
| Scoring Scheme | Winner | Ranking |
|---|---|---|
| Sequential Performance | Bitwuzla | Bitwuzla, Bitwuzla Fixedn, 2022-Bitwuzlan, cvc5, UltimateEliminator+MathSAT |
| Parallel Performance | Bitwuzla | Bitwuzla, Bitwuzla Fixedn, 2022-Bitwuzlan, cvc5, UltimateEliminator+MathSAT |
| SAT Performance | Bitwuzla | Bitwuzla Fixedn, Bitwuzla, 2022-Bitwuzlan, cvc5, UltimateEliminator+MathSAT |
| UNSAT Performance | Bitwuzla | 2022-Bitwuzlan, Bitwuzla, Bitwuzla Fixedn, cvc5, UltimateEliminator+MathSAT |
| 24s Performance | Bitwuzla | Bitwuzla, Bitwuzla Fixedn, 2022-Bitwuzlan, cvc5, UltimateEliminator+MathSAT |
| Scoring Scheme | Winner | Ranking |
|---|---|---|
| Sequential Performance | STP | Bitwuzla Fixedn, STP, 2022-STP-fixedn, Bitwuzla, Yices2, cvc5, Z3-Owl Fixedn, Z3-Owl, UltimateIntBlastingWrapper+SMTInterpol |
| Parallel Performance | STP | Bitwuzla Fixedn, STP, 2022-STP-fixedn, Bitwuzla, Yices2, cvc5, Z3-Owl Fixedn, Z3-Owl, UltimateIntBlastingWrapper+SMTInterpol |
| SAT Performance | STP | 2022-STP-fixedn, STP, Bitwuzla Fixedn, Bitwuzla, Yices2, cvc5, Z3-Owl Fixedn, Z3-Owl, UltimateIntBlastingWrapper+SMTInterpol |
| UNSAT Performance | STP | Bitwuzla Fixedn, STP, 2022-STP-fixedn, Bitwuzla, Yices2, cvc5, Z3-Owl Fixedn, Z3-Owl, UltimateIntBlastingWrapper+SMTInterpol |
| 24s Performance | STP | STP, 2022-STP-fixedn, Bitwuzla Fixedn, Bitwuzla, Yices2, cvc5, Z3-Owl Fixedn, Z3-Owl, UltimateIntBlastingWrapper+SMTInterpol |
| Scoring Scheme | Winner | Ranking |
|---|---|---|
| Sequential Performance | cvc5 | 2022-z3-4.8.17n, cvc5, SMTInterpol |
| Parallel Performance | cvc5 | 2022-z3-4.8.17n, cvc5, SMTInterpol |
| SAT Performance | cvc5 | cvc5, 2022-z3-4.8.17n, SMTInterpol |
| UNSAT Performance | cvc5 | 2022-z3-4.8.17n, cvc5, SMTInterpol |
| 24s Performance | SMTInterpol | SMTInterpol, 2022-z3-4.8.17n, cvc5 |
| Scoring Scheme | Winner | Ranking |
|---|---|---|
| Sequential Performance | Bitwuzla | Bitwuzla, Bitwuzla Fixedn, 2022-Bitwuzlan, Yices2, cvc5, Z3-Owl Fixedn, UltimateIntBlastingWrapper+SMTInterpol, Z3-Owl |
| Parallel Performance | Bitwuzla | Bitwuzla, Bitwuzla Fixedn, 2022-Bitwuzlan, Yices2, cvc5, Z3-Owl Fixedn, UltimateIntBlastingWrapper+SMTInterpol, Z3-Owl |
| SAT Performance | Bitwuzla | Bitwuzla, Bitwuzla Fixedn, Yices2, 2022-Bitwuzlan, cvc5, Z3-Owl Fixedn, UltimateIntBlastingWrapper+SMTInterpol, Z3-Owl |
| UNSAT Performance | Bitwuzla | Bitwuzla, Bitwuzla Fixedn, 2022-Bitwuzlan, Yices2, cvc5, Z3-Owl Fixedn, Z3-Owl, UltimateIntBlastingWrapper+SMTInterpol |
| 24s Performance | Bitwuzla | Bitwuzla, Bitwuzla Fixedn, Yices2, 2022-Bitwuzlan, cvc5, UltimateIntBlastingWrapper+SMTInterpol, Z3-Owl Fixedn, Z3-Owl |
| Scoring Scheme | Winner | Ranking |
|---|---|---|
| Sequential Performance | SMTInterpol | SMTInterpol, OpenSMT, 2022-z3-4.8.17n, cvc5, Yices2 |
| Parallel Performance | SMTInterpol | SMTInterpol, OpenSMT, 2022-z3-4.8.17n, cvc5, Yices2 |
| SAT Performance | SMTInterpol | SMTInterpol, OpenSMT, 2022-z3-4.8.17n, cvc5, Yices2 |
| UNSAT Performance | OpenSMT | OpenSMT, Yices2, 2022-z3-4.8.17n, cvc5, SMTInterpol |
| 24s Performance | Yices2 | Yices2, 2022-z3-4.8.17n, SMTInterpol, OpenSMT, cvc5 |
| Scoring Scheme | Winner | Ranking |
|---|---|---|
| Sequential Performance | cvc5 | cvc5, Yices2, 2020-CVC4n, SMTInterpol |
| Parallel Performance | cvc5 | cvc5, Yices2, 2020-CVC4n, SMTInterpol |
| SAT Performance | Yices2 | Yices2, cvc5, 2020-CVC4n, SMTInterpol |
| UNSAT Performance | cvc5 | cvc5, 2020-CVC4n, Yices2, SMTInterpol |
| 24s Performance | cvc5 | cvc5, 2020-CVC4n, Yices2, SMTInterpol |
| Scoring Scheme | Winner | Ranking |
|---|---|---|
| Sequential Performance | Yices2 | 2022-Yices2n, Yices2, OpenSMT, cvc5, SMTInterpol |
| Parallel Performance | Yices2 | 2022-Yices2n, Yices2, OpenSMT, cvc5, SMTInterpol |
| SAT Performance | Yices2 | 2022-Yices2n, Yices2, OpenSMT, cvc5, SMTInterpol |
| UNSAT Performance | Yices2 | 2022-Yices2n, Yices2, OpenSMT, cvc5, SMTInterpol |
| 24s Performance | Yices2 | 2022-Yices2n, Yices2, cvc5, OpenSMT, SMTInterpol |
| Scoring Scheme | Winner | Ranking |
|---|---|---|
| Sequential Performance | Bitwuzla | Bitwuzla, Bitwuzla Fixedn, 2022-Bitwuzlan, cvc5, COLIBRI, Z3-Owl Fixedn, Z3-Owl |
| Parallel Performance | Bitwuzla | Bitwuzla, Bitwuzla Fixedn, 2022-Bitwuzlan, cvc5, COLIBRI, Z3-Owl Fixedn, Z3-Owl |
| SAT Performance | Bitwuzla | Bitwuzla, Bitwuzla Fixedn, 2022-Bitwuzlan, cvc5, COLIBRI, Z3-Owl Fixedn, Z3-Owl |
| UNSAT Performance | Bitwuzla | Bitwuzla, Bitwuzla Fixedn, 2022-Bitwuzlan, cvc5, COLIBRI, Z3-Owl Fixedn, Z3-Owl |
| 24s Performance | Bitwuzla | Bitwuzla Fixedn, Bitwuzla, 2022-Bitwuzlan, COLIBRI, cvc5, Z3-Owl Fixedn, Z3-Owl |
| Scoring Scheme | Winner | Ranking |
|---|---|---|
| Sequential Performance | Z3++ | 2019-Par4n, Z3++, OpenSMT, cvc5, Yices2, SMTInterpol |
| Parallel Performance | Z3++ | 2019-Par4n, Z3++, OpenSMT, cvc5, Yices2, SMTInterpol |
| SAT Performance | Z3++ | 2019-Par4n, Z3++, OpenSMT, Yices2, cvc5, SMTInterpol |
| UNSAT Performance | cvc5 | 2019-Par4n, cvc5, OpenSMT, Yices2, SMTInterpol, Z3++ |
| 24s Performance | Yices2 | 2019-Par4n, Yices2, Z3++, OpenSMT, cvc5, SMTInterpol |
| Scoring Scheme | Winner | Ranking |
|---|---|---|
| Sequential Performance | Yices2 | 2021-Yices2n, 2022-Yices2n, Yices2, OpenSMT, cvc5, SMTInterpol, Yaga |
| Parallel Performance | Yices2 | 2021-Yices2n, 2022-Yices2n, Yices2, OpenSMT, cvc5, SMTInterpol, Yaga |
| SAT Performance | OpenSMT | OpenSMT, 2021-Yices2n, 2022-Yices2n, Yices2, cvc5, SMTInterpol, Yaga |
| UNSAT Performance | cvc5 | cvc5, 2022-Yices2n, 2021-Yices2n, Yices2, OpenSMT, SMTInterpol, Yaga |
| 24s Performance | Yices2 | 2022-Yices2n, 2021-Yices2n, Yices2, OpenSMT, cvc5, SMTInterpol, Yaga |
| Scoring Scheme | Winner | Ranking |
|---|---|---|
| Sequential Performance | Z3++ | Z3++, 2022-Z3++-fixedn, yices-ismt, z3-alpha, cvc5, Yices2 |
| Parallel Performance | Z3++ | Z3++, 2022-Z3++-fixedn, yices-ismt, z3-alpha, cvc5, Yices2 |
| SAT Performance | Z3++ | Z3++, yices-ismt, 2022-Z3++-fixedn, z3-alpha, cvc5, Yices2 |
| UNSAT Performance | Z3++ | Z3++, z3-alpha, 2022-Z3++-fixedn, yices-ismt, Yices2, cvc5 |
| 24s Performance | Z3++ | Z3++, Yices2, yices-ismt, z3-alpha, 2022-Z3++-fixedn, cvc5 |
| Scoring Scheme | Winner | Ranking |
|---|---|---|
| Sequential Performance | Z3++ | Z3++, 2019-Par4n, cvc5, cvc5-NRA-LS, Yices2, z3-alpha, SMT-RAT-MCSAT, 2022-Z3++-fixedn |
| Parallel Performance | Z3++ | 2019-Par4n, Z3++, cvc5, cvc5-NRA-LS, Yices2, z3-alpha, SMT-RAT-MCSAT, 2022-Z3++-fixedn |
| SAT Performance | Z3++ | 2022-Z3++-fixedn, Z3++, 2019-Par4n, z3-alpha, cvc5, cvc5-NRA-LS, Yices2, SMT-RAT-MCSAT |
| UNSAT Performance | cvc5 | 2019-Par4n, cvc5, cvc5-NRA-LS, Z3++, Yices2, SMT-RAT-MCSAT, z3-alpha, 2022-Z3++-fixedn |
| 24s Performance | cvc5 | 2019-Par4n, cvc5, 2022-Z3++-fixedn, Z3++, Yices2, z3-alpha, cvc5-NRA-LS, SMT-RAT-MCSAT |
| Scoring Scheme | Winner | Ranking |
|---|---|---|
| Sequential Performance | cvc5 | cvc5, 2022-cvc5n, z3-alpha, OSTRICH Fixedn, Z3-Noodler Fixedn, Z3-Noodler, OSTRICH |
| Parallel Performance | cvc5 | cvc5, 2022-cvc5n, z3-alpha, OSTRICH Fixedn, Z3-Noodler Fixedn, Z3-Noodler, OSTRICH |
| SAT Performance | cvc5 | cvc5, 2022-cvc5n, z3-alpha, OSTRICH Fixedn, Z3-Noodler Fixedn, OSTRICH, Z3-Noodler |
| UNSAT Performance | cvc5 | OSTRICH Fixedn, cvc5, z3-alpha, 2022-cvc5n, Z3-Noodler Fixedn, Z3-Noodler, OSTRICH |
| 24s Performance | z3-alpha | z3-alpha, cvc5, 2022-cvc5n, OSTRICH Fixedn, Z3-Noodler Fixedn, Z3-Noodler, OSTRICH |