The International Satisfiability Modulo Theories (SMT) Competition.
Competition results for the QF_AUFBV logic in the Incremental Track.
Results were generated on 2024-07-08
Benchmarks: 31
Time Limit: 1200 seconds
Memory Limit: 20480 GB
| Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24 seconds Performance (parallel) |
|---|---|---|---|
| Bitwuzla | - | - | Bitwuzla |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Bitwuzla | 0 | 967 | 3848.676483 | 3852.62804 | 0 | 0 | 0 | 31 | 0 | 0 | 0 |
| Yices2 | 0 | 948 | 9631.237527 | 9639.409557 | 0 | 0 | 0 | 31 | 0 | 6 | 0 |
| cvc5 | 0 | 722 | 21559.712537 | 21574.397877 | 0 | 0 | 0 | 31 | 0 | 16 | 0 |
| SMTInterpol | 0 | 90 | 26555.807239 | 25391.958839 | 0 | 0 | 0 | 31 | 0 | 21 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Bitwuzla | 0 | 216 | 50.267718 | 51.934979 | 0 | 0 | 0 | 18 | 13 | 0 | 0 |
| Yices2 | 0 | 216 | 66.673553 | 68.381237 | 0 | 0 | 0 | 18 | 13 | 0 | 0 |
| cvc5 | 0 | 19 | 20.340147 | 21.187012 | 0 | 0 | 0 | 10 | 21 | 0 | 0 |
| SMTInterpol | 0 | 18 | 134.52426 | 51.67015 | 0 | 0 | 0 | 9 | 22 | 0 | 0 |