The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_Equality+Bitvec division in the Model Validation Track.
Page generated on 2023-07-06 16:06:00 +0000
Benchmarks: 412 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 |
|---|---|---|---|---|---|---|---|
| Bitwuzla | 0 | 411 | 14080.743 | 14087.182 | 1 | 0 | |
| Bitwuzla Fixedn | 0 | 411 | 14200.806 | 14148.05 | 1 | 0 | |
| 2022-Bitwuzlan | 0 | 406 | 4750.445 | 4701.546 | 4 | 0 | |
| Yices2 | 0 | 401 | 11433.119 | 11404.255 | 11 | 0 | |
| cvc5 | 0 | 388 | 14939.293 | 14941.771 | 24 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|
| Bitwuzla | 0 | 411 | 14080.743 | 14087.182 | 1 | 0 | |
| Bitwuzla Fixedn | 0 | 411 | 14200.806 | 14148.05 | 1 | 0 | |
| 2022-Bitwuzlan | 0 | 406 | 4750.445 | 4701.546 | 4 | 0 | |
| Yices2 | 0 | 401 | 11433.119 | 11404.255 | 11 | 0 | |
| cvc5 | 0 | 388 | 14939.293 | 14941.771 | 24 | 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.