The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_Bitvec division in the Incremental Track.
Page generated on 2023-07-06 16:05:24 +0000
Benchmarks: 1295 Time Limit: 1200 seconds Memory Limit: 60 GB
Logics:| Parallel Performance |
|---|
| Bitwuzla |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|
| Bitwuzla | 0 | 16423 | 27556.4 | 27615.74 | 539 | 0 | 9 | 0 |
| Yices2 Fixedn | 0 | 16374 | 19604.77 | 19632.69 | 588 | 0 | 14 | 0 |
| Yices2 | 0 | 16371 | 19426.92 | 19449.1 | 591 | 0 | 15 | 0 |
| 2022-Yices2n | 0 | 16368 | 19661.38 | 19684.44 | 594 | 0 | 14 | 0 |
| STP | 0 | 16259 | 15362.59 | 15409.37 | 703 | 0 | 10 | 0 |
| cvc5 | 0 | 16122 | 70306.4 | 70354.79 | 840 | 0 | 17 | 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.