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 Model Validation Track.
Page generated on 2023-07-06 16:06:00 +0000
Benchmarks: 9069 Time Limit: 1200 seconds Memory Limit: 60 GB
Logics:| Sequential Performance | Parallel Performance |
|---|---|
| STP | STP |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|
| Bitwuzla Fixedn | 0 | 9025 | 67902.025 | 67731.773 | 45 | 0 | |
| STP | 0 | 9024 | 57693.477 | 57556.818 | 45 | 0 | |
| Bitwuzla | 0 | 9019 | 71359.346 | 71216.296 | 50 | 0 | |
| 2020-Bitwuzlan | 0 | 9006 | 91083.336 | 90763.568 | 63 | 0 | |
| Yices2 | 0 | 8973 | 99192.946 | 99112.393 | 96 | 0 | |
| cvc5 | 0 | 8650 | 134396.618 | 133952.196 | 411 | 3 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|
| STP | 0 | 9024 | 57693.477 | 57556.818 | 45 | 0 | |
| Bitwuzla Fixedn | 0 | 9024 | 66703.505 | 66531.743 | 45 | 0 | |
| Bitwuzla | 0 | 9019 | 71359.346 | 71216.296 | 50 | 0 | |
| 2020-Bitwuzlan | 0 | 9006 | 91083.336 | 90763.568 | 63 | 0 | |
| Yices2 | 0 | 8973 | 99192.946 | 99112.393 | 96 | 0 | |
| cvc5 | 0 | 8650 | 134396.618 | 133952.196 | 411 | 3 |
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.