The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_LIA division in the Incremental Track.
Page generated on 2020-07-04 11:47:56 +0000
Benchmarks: 69 Time Limit: 1200 seconds Memory Limit: 60 GB
| Parallel Performance |
|---|
| Yices2 incremental |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|
| Yices2-fixed incrementaln | 0 | 20040344 | 32239.057 | 31776.046 | 870 | 20 | 0 | |
| 2018-Yices (incremental)n | 0 | 20040342 | 32110.053 | 31686.696 | 872 | 20 | 0 | |
| Yices2 incremental | 0 | 20040337 | 32150.689 | 31694.207 | 877 | 20 | 0 | |
| SMTInterpol | 0 | 18116077 | 53008.018 | 51411.234 | 1925137 | 36 | 0 | |
| SMTInterpol-fixedn | 0 | 18092895 | 53028.053 | 51425.701 | 1948319 | 36 | 0 | |
| MathSAT5n | 0 | 16538400 | 41739.865 | 41350.49 | 3502814 | 27 | 0 | |
| CVC4-inc | 0 | 7265722 | 56615.005 | 56558.749 | 12775492 | 41 | 0 | |
| z3n | 0 | 7253153 | 59661.232 | 59606.465 | 12788061 | 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.