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 2021-07-18 17:30:28 +0000
Benchmarks: 1294 Time Limit: 1200 seconds Memory Limit: 60 GB
Logics:| Parallel Performance |
|---|
| STP |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|
| STP | 0 | 15786 | 20647.827 | 14260.39 | 485 | 0 | 9 | 0 |
| 2020-Yices2-fixed incrementaln | 0 | 15760 | 23163.028 | 23018.677 | 511 | 0 | 11 | 0 |
| MathSAT5n | 0 | 15759 | 35295.663 | 35098.652 | 512 | 0 | 16 | 0 |
| Yices2 incremental | 0 | 15756 | 23251.649 | 23134.167 | 515 | 0 | 12 | 0 |
| cvc5-inc | 0 | 15720 | 74203.162 | 74025.434 | 551 | 0 | 13 | 0 |
| Bitwuzla | 0 | 15709 | 19959.045 | 19840.335 | 562 | 0 | 7 | 0 |
| z3n | 0 | 15544 | 191060.419 | 190976.399 | 727 | 0 | 89 | 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.