SMT-COMP 2022 Results - Model Validation Track (Summary)
Summary of all competition results for the Model Validation 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 | Bitwuzla | 2020-Bitwuzlan, Bitwuzla, Yices2, STP, z3-4.8.17n, cvc5, MathSATn, Z3++BV |
| Parallel Performance | Bitwuzla | 2020-Bitwuzlan, Bitwuzla, Yices2, STP, z3-4.8.17n, cvc5, MathSATn, Z3++BV |
| Scoring Scheme | Winner | Ranking |
| Sequential Performance | Bitwuzla | Bitwuzla, 2021-Yices2 model-validationn, Yices2, z3-4.8.17n, cvc5, MathSATn |
| Parallel Performance | Bitwuzla | Bitwuzla, Yices2, 2021-Yices2 model-validationn, z3-4.8.17n, cvc5, MathSATn |
| Scoring Scheme | Winner | Ranking |
| Sequential Performance | smtinterpol | smtinterpol, 2021-SMTInterpoln, cvc5, z3-4.8.17n, Yices2, OpenSMT, MathSATn |
| Parallel Performance | smtinterpol | smtinterpol, 2021-SMTInterpoln, cvc5, z3-4.8.17n, Yices2, OpenSMT, MathSATn |
| Scoring Scheme | Winner | Ranking |
| Sequential Performance | Yices2 | Yices2, 2021-Yices2 model-validationn, z3-4.8.17n, cvc5, smtinterpol, OpenSMT, MathSATn |
| Parallel Performance | Yices2 | 2021-Yices2 model-validationn, Yices2, z3-4.8.17n, cvc5, smtinterpol, OpenSMT, MathSATn |
This division is experimental. Solvers are only ranked by performance, but no
winner is selected.
| Scoring Scheme | Winner | Ranking |
| Sequential Performance | Z3++ | Z3++, 2020-z3n, z3-4.8.17n, OpenSMT, Yices2, cvc5, MathSATn, smtinterpol |
| Parallel Performance | Z3++ | Z3++, 2020-z3n, z3-4.8.17n, OpenSMT, Yices2, cvc5, MathSATn, smtinterpol |
| Scoring Scheme | Winner | Ranking |
| Sequential Performance | OpenSMT | OpenSMT, 2021-Yices2 model-validationn, Yices2, cvc5, z3-4.8.17n, MathSATn, smtinterpol |
| Parallel Performance | OpenSMT | OpenSMT, 2021-Yices2 model-validationn, Yices2, cvc5, z3-4.8.17n, smtinterpol, MathSATn |