The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_BV division in the Incremental Track.
Page generated on 2020-07-04 11:47:56 +0000
Benchmarks: 1035 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 | 18669 | 20835.305 | 20741.555 | 395 | 11 | 0 | |
| Yices2 incremental | 0 | 18667 | 20923.314 | 20740.384 | 397 | 11 | 0 | |
| 2019-Yices 2.6.2 Incrementaln | 0 | 18643 | 21069.47 | 21034.235 | 421 | 12 | 0 | |
| STP + CMS | 0 | 18636 | 19265.608 | 16123.708 | 428 | 11 | 0 | |
| Bitwuzla-fixedn | 0 | 18614 | 19550.613 | 19481.889 | 450 | 8 | 0 | |
| Bitwuzla | 0 | 18602 | 19772.61 | 19630.488 | 462 | 8 | 0 | |
| STP + MergeSAT | 0 | 18586 | 16525.963 | 16446.027 | 478 | 11 | 0 | |
| z3n | 0 | 18568 | 43808.158 | 43725.491 | 496 | 15 | 0 | |
| MathSAT5n | 0 | 18551 | 31162.948 | 31095.712 | 513 | 15 | 0 | |
| CVC4-inc | 0 | 18466 | 60912.73 | 60836.537 | 598 | 11 | 0 | |
| LazyBV2Int | 0 | 14781 | 333740.613 | 333648.351 | 4283 | 258 | 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.