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 Unsat Core Track.
Page generated on 2022-08-10 11:18:51 +0000
Benchmarks: 204 Time Limit: 1200 seconds Memory Limit: 60 GB
Logics:| Sequential Performance | Parallel Performance |
|---|---|
| Yices2 | Yices2 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|
| 2020-Yices2n | 0 | 149491 | 68959.75 | 69039.985 | 34 | 0 | |
| Yices2 | 0 | 146537 | 77503.152 | 77463.753 | 42 | 0 | |
| cvc5 | 0 | 142733 | 45921.027 | 45899.985 | 14 | 0 | |
| z3-4.8.17n | 0 | 122655 | 75791.029 | 75792.746 | 38 | 0 | |
| MathSATn | 0 | 106426 | 154206.359 | 154236.018 | 110 | 0 | |
| smtinterpol | 0 | 86704 | 116041.785 | 110903.889 | 60 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|
| 2020-Yices2n | 0 | 149491 | 69046.91 | 69038.485 | 34 | 0 | |
| Yices2 | 0 | 146537 | 77508.092 | 77462.153 | 42 | 0 | |
| cvc5 | 0 | 142733 | 45924.207 | 45899.385 | 14 | 0 | |
| z3-4.8.17n | 0 | 122655 | 75795.819 | 75791.006 | 38 | 0 | |
| smtinterpol | 0 | 106531 | 116372.135 | 110599.059 | 56 | 0 | |
| MathSATn | 0 | 106426 | 154226.639 | 154230.858 | 110 | 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.