The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_RDL division in the Model Validation Track.
Page generated on 2020-07-04 11:50:14 +0000
Benchmarks: 109 Time Limit: 1200 seconds Memory Limit: 60 GB
This division is experimental. Solvers are only ranked by performance, but no winner is selected.
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|
| Yices2-fixed Model Validationn | 0 | 109 | 495.298 | 495.402 | 0 | 0 | |
| Yices2 Model Validation | 0 | 109 | 495.323 | 495.404 | 0 | 0 | |
| CVC4-mv | 0 | 106 | 6980.83 | 6981.713 | 3 | 0 | |
| MathSAT5-mvn | 0 | 106 | 7744.608 | 7745.922 | 3 | 0 | |
| z3n | 0 | 103 | 9489.126 | 9485.641 | 6 | 0 | |
| SMTInterpol | 0 | 101 | 15635.556 | 14813.807 | 8 | 0 | |
| SMTInterpol-fixedn | 0 | 101 | 15653.703 | 14841.791 | 8 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|
| Yices2-fixed Model Validationn | 0 | 109 | 495.298 | 495.402 | 0 | 0 | |
| Yices2 Model Validation | 0 | 109 | 495.323 | 495.404 | 0 | 0 | |
| CVC4-mv | 0 | 106 | 6981.04 | 6981.553 | 3 | 0 | |
| MathSAT5-mvn | 0 | 106 | 7744.838 | 7745.842 | 3 | 0 | |
| z3n | 0 | 103 | 9489.456 | 9485.401 | 6 | 0 | |
| SMTInterpol | 0 | 101 | 15635.556 | 14813.807 | 8 | 0 | |
| SMTInterpol-fixedn | 0 | 101 | 15653.703 | 14841.791 | 8 | 0 |
n Non-competing.
Abstained: Total of benchmarks in logics in this division that solver chose to abstain from. For SAT/UNSAT scores, this column also includes benchmarks not known to be SAT/UNSAT.