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 Incremental Track.
Page generated on 2022-08-10 11:18:21 +0000
Benchmarks: 1832 Time Limit: 1200 seconds Memory Limit: 60 GB
Logics:| Parallel Performance |
|---|
| Yices2 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|
| Yices2 | 0 | 5002 | 32309.398 | 32237.493 | 57 | 0 | 21 | 0 |
| 2020-Yices2 incrementaln | 0 | 5001 | 31787.425 | 31727.613 | 58 | 0 | 21 | 0 |
| z3-4.8.17n | 0 | 4754 | 202951.875 | 202886.433 | 305 | 0 | 150 | 0 |
| MathSATn | 0 | 4732 | 53111.046 | 53000.544 | 327 | 0 | 38 | 0 |
| cvc5 | 0 | 4199 | 78427.019 | 78247.941 | 860 | 0 | 54 | 0 |
| Bitwuzla | 0 | 4181 | 51837.462 | 51795.353 | 878 | 0 | 31 | 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.