The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_AUFBV division in the Incremental Track.
Page generated on 2020-07-04 11:47:56 +0000
Benchmarks: 31 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 incremental | 0 | 946 | 11073.673 | 11073.482 | 21 | 8 | 0 | |
| Yices2-fixed incrementaln | 0 | 946 | 11087.596 | 11087.459 | 21 | 8 | 0 | |
| 2019-Yices 2.6.2 Incrementaln | 0 | 945 | 11563.07 | 11570.511 | 22 | 9 | 0 | |
| z3n | 0 | 873 | 16615.577 | 16615.351 | 94 | 13 | 0 | |
| MathSAT5n | 0 | 794 | 18877.847 | 18877.811 | 173 | 14 | 0 | |
| CVC4-inc | 0 | 693 | 20743.403 | 20742.93 | 274 | 17 | 0 | |
| Bitwuzla | 0 | 123 | 168.504 | 168.642 | 844 | 0 | 0 | |
| Bitwuzla-fixedn | 0 | 123 | 186.519 | 186.65 | 844 | 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.