The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_UFLIA division in the Incremental Track.
Page generated on 2020-07-04 11:47:56 +0000
Benchmarks: 309 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 |
|---|---|---|---|---|---|---|---|---|
| 2018-Z3 (incremental)n | 0 | 12962 | 70666.416 | 70695.49 | 3913 | 51 | 0 | |
| z3n | 0 | 11831 | 73564.672 | 73564.426 | 5044 | 56 | 0 | |
| MathSAT5n | 0 | 10072 | 95643.148 | 95643.503 | 6803 | 76 | 0 | |
| Yices2-fixed incrementaln | 0 | 9316 | 76487.651 | 76487.299 | 7559 | 60 | 0 | |
| Yices2 incremental | 0 | 9310 | 76453.395 | 76452.566 | 7565 | 60 | 0 | |
| SMTInterpol | 0 | 8724 | 92067.626 | 91452.296 | 8151 | 73 | 0 | |
| SMTInterpol-fixedn | 0 | 8724 | 92061.736 | 91456.843 | 8151 | 73 | 0 | |
| CVC4-inc | 0 | 6949 | 92766.16 | 92766.114 | 9926 | 71 | 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.