The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_LinearIntArith division in the Incremental Track.
Page generated on 2022-08-10 11:18:22 +0000
Benchmarks: 69 Time Limit: 1200 seconds Memory Limit: 60 GB
Logics:| Parallel Performance |
|---|
| Yices2 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|
| 2021-Yices2 incrementaln | 0 | 20040331 | 32529.772 | 32010.022 | 883 | 0 | 20 | 0 |
| Yices2 | 0 | 20040331 | 32607.905 | 32086.355 | 883 | 0 | 20 | 0 |
| z3-4.8.17n | 0 | 19637536 | 52201.518 | 51619.056 | 403678 | 0 | 32 | 0 |
| MathSATn | 0 | 17373286 | 41517.382 | 41028.937 | 2667928 | 0 | 26 | 0 |
| smtinterpol | 0 | 10798835 | 65748.625 | 64494.406 | 9242379 | 0 | 48 | 0 |
| cvc5 | 0 | 3733255 | 65635.319 | 65606.888 | 16307959 | 0 | 50 | 0 |
| OpenSMT | 0 | 834416 | 56697.846 | 56693.366 | 19206798 | 0 | 42 | 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.