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 Incremental Track.
Page generated on 2023-07-06 16:05:24 +0000
Benchmarks: 10 Time Limit: 1200 seconds Memory Limit: 60 GB
Logics:| Parallel Performance |
|---|
| OpenSMT |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|
| 2018-MathSAT-incrementaln | 0 | 1256 | 7577.73 | 7579.4 | 259 | 0 | 6 | 0 |
| OpenSMT | 0 | 953 | 8467.24 | 8468.08 | 562 | 0 | 6 | 0 |
| Yices2 Fixedn | 0 | 909 | 11353.31 | 11355.11 | 606 | 0 | 10 | 0 |
| Yices2 | 0 | 906 | 11329.04 | 11330.65 | 609 | 0 | 10 | 0 |
| cvc5 | 0 | 695 | 11302.39 | 11303.63 | 820 | 0 | 10 | 0 |
| SMTInterpol | 0 | 513 | 12918.34 | 11099.42 | 1002 | 0 | 10 | 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.