The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
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 model-validation, STP, cvc5-mv, z3-mvn, MathSAT5n |
| Parallel Performance | Bitwuzla | 2020-Bitwuzlan, Bitwuzla, Yices2 model-validation, STP, cvc5-mv, z3-mvn, MathSAT5n |
This division is experimental. Solvers are only ranked by performance, but no winner is selected.
| Scoring Scheme | Ranking |
|---|---|
| Sequential Performance | Yices2 model-validation, Bitwuzla, MathSAT5n, cvc5-mv, z3-mvn |
| Parallel Performance | Yices2 model-validation, Bitwuzla, MathSAT5n, cvc5-mv, z3-mvn |
This division is experimental. Solvers are only ranked by performance, but no winner is selected.
| Scoring Scheme | Ranking |
|---|---|
| Sequential Performance | SMTInterpol, cvc5-mv, Yices2 model-validation, z3-mvn, MathSAT5n |
| Parallel Performance | SMTInterpol, cvc5-mv, Yices2 model-validation, z3-mvn, MathSAT5n |
This division is experimental. Solvers are only ranked by performance, but no winner is selected.
| Scoring Scheme | Ranking |
|---|---|
| Sequential Performance | Yices2 model-validation, OpenSMT, cvc5-mv, SMTInterpol, z3-mvn, MathSAT5n |
| Parallel Performance | Yices2 model-validation, OpenSMT, cvc5-mv, SMTInterpol, z3-mvn, MathSAT5n |
| Scoring Scheme | Winner | Ranking |
|---|---|---|
| Sequential Performance | cvc5-mv | 2020-z3n, z3-mvn, cvc5-mv, 2020-Yices2-fixed Model Validationn, 2020-Yices2 Model Validationn, Yices2 model-validation, MathSAT5n, SMTInterpol, OpenSMT, YicesLS |
| Parallel Performance | cvc5-mv | 2020-z3n, z3-mvn, cvc5-mv, 2020-Yices2 Model Validationn, 2020-Yices2-fixed Model Validationn, Yices2 model-validation, MathSAT5n, SMTInterpol, OpenSMT, YicesLS |
| Scoring Scheme | Winner | Ranking |
|---|---|---|
| Sequential Performance | Yices2 model-validation | Yices2 model-validation, OpenSMT, z3-mvn, 2020-Yices2-fixed Model Validationn, cvc5-mv, SMTInterpol, MathSAT5n, 2020-OpenSMTn |
| Parallel Performance | Yices2 model-validation | Yices2 model-validation, OpenSMT, z3-mvn, 2020-Yices2-fixed Model Validationn, cvc5-mv, SMTInterpol, MathSAT5n, 2020-OpenSMTn |