The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_LinearRealArith division in the Model Validation Track.
Page generated on 2022-08-10 11:19:11 +0000
Benchmarks: 625 Time Limit: 1200 seconds Memory Limit: 60 GB
Logics:| Sequential Performance | Parallel Performance |
|---|---|
| OpenSMT | OpenSMT |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|
| OpenSMT | 0 | 606 | 45953.261 | 45966.554 | 19 | 0 | |
| 2021-Yices2 model-validationn | 0 | 601 | 39164.898 | 39129.663 | 24 | 0 | |
| Yices2 | 0 | 601 | 39260.871 | 39269.266 | 24 | 0 | |
| cvc5 | 0 | 596 | 61835.316 | 61841.421 | 29 | 0 | |
| z3-4.8.17n | 0 | 595 | 58503.93 | 58412.58 | 30 | 0 | |
| MathSATn | 0 | 579 | 76601.709 | 76604.393 | 45 | 0 | |
| smtinterpol | 0 | 579 | 95678.469 | 90490.197 | 46 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|
| OpenSMT | 0 | 606 | 45957.641 | 45965.784 | 19 | 0 | |
| 2021-Yices2 model-validationn | 0 | 601 | 39166.538 | 39128.923 | 24 | 0 | |
| Yices2 | 0 | 601 | 39263.471 | 39268.206 | 24 | 0 | |
| cvc5 | 0 | 596 | 61842.836 | 61840.131 | 29 | 0 | |
| z3-4.8.17n | 0 | 595 | 58508.57 | 58411.51 | 30 | 0 | |
| smtinterpol | 0 | 581 | 95706.199 | 90441.617 | 44 | 0 | |
| MathSATn | 0 | 579 | 76609.189 | 76602.353 | 45 | 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.