The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_UF division in the Incremental Track.
Page generated on 2020-07-04 11:47:56 +0000
Benchmarks: 306 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 |
|---|---|---|---|---|---|---|---|---|
| 2019-Yices 2.6.2 Incrementaln | 0 | 612 | 73.193 | 61.383 | 0 | 0 | 0 | |
| Yices2-fixed incrementaln | 0 | 612 | 77.415 | 64.338 | 0 | 0 | 0 | |
| Yices2 incremental | 0 | 612 | 78.505 | 65.097 | 0 | 0 | 0 | |
| z3n | 0 | 612 | 186.102 | 173.305 | 0 | 0 | 0 | |
| CVC4-inc | 0 | 612 | 438.578 | 410.3 | 0 | 0 | 0 | |
| SMTInterpol | 0 | 612 | 1297.261 | 469.075 | 0 | 0 | 0 | |
| SMTInterpol-fixedn | 0 | 612 | 1291.405 | 472.126 | 0 | 0 | 0 | |
| OpenSMT | 0 | 611 | 2858.248 | 2840.581 | 1 | 1 | 0 | |
| MathSAT5n | 0 | 574 | 144.304 | 127.049 | 38 | 0 | 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.