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 Unsat Core Track.
Page generated on 2021-07-18 17:31:25 +0000
Benchmarks: 2868 Time Limit: 1200 seconds Memory Limit: 60 GB
Logics:| Sequential Performance | Parallel Performance |
|---|---|
| Bitwuzla | Bitwuzla |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|
| 2020-Bitwuzla-fixedn | 0 | 2091261 | 233719.537 | 233582.205 | 122 | 0 | |
| Bitwuzla | 0 | 2083241 | 239535.834 | 239458.841 | 126 | 0 | |
| cvc5-uc | 0 | 1946771 | 865450.459 | 865368.859 | 562 | 0 | |
| Yices2 | 0 | 1813707 | 358232.693 | 358289.327 | 272 | 0 | |
| z3n | 0 | 1475365 | 1449391.728 | 1465270.255 | 1101 | 0 | |
| MathSAT5n | 0 | 0 | 217.866 | 225.142 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|
| 2020-Bitwuzla-fixedn | 0 | 2091261 | 233735.427 | 233577.105 | 122 | 0 | |
| Bitwuzla | 0 | 2083241 | 239551.594 | 239453.571 | 126 | 0 | |
| cvc5-uc | 0 | 1946771 | 865562.749 | 865344.859 | 562 | 0 | |
| Yices2 | 0 | 1813707 | 358281.523 | 358278.747 | 272 | 0 | |
| z3n | 0 | 1475365 | 1463773.093 | 1465229.235 | 1101 | 0 | |
| MathSAT5n | 0 | 0 | 217.866 | 225.142 | 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.