The International Satisfiability Modulo Theories (SMT) Competition.
Competition results for the QF_Equality_Bitvec division in the Incremental Track.
Results were generated on 2024-07-08
Benchmarks: 1832
Time Limit: 1200 seconds
Memory Limit: 20480 GB
| winner_seq | winner_par | winner_sat | winner_unsat | winner_24s |
|---|---|---|---|---|
| Bitwuzla | Bitwuzla | - | - | Yices2 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Bitwuzla | 0 | 5555 | 21701.122916 | 21868.703122 | 0 | 0 | 0 | 1832 | 0 | 12 | 0 |
| Yices2 | 0 | 5247 | 9571.859538 | 9737.848561 | 0 | 0 | 0 | 1832 | 0 | 25 | 0 |
| cvc5 | 0 | 3153 | 18757.896226 | 18892.416697 | 0 | 0 | 0 | 1832 | 0 | 228 | 4 |
| SMTInterpol | 0 | 3076 | 160754.107467 | 117930.835871 | 0 | 0 | 0 | 1832 | 0 | 218 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Bitwuzla | 0 | 5556 | 36117.70645 | 36290.508537 | 0 | 0 | 0 | 1832 | 0 | 12 | 0 |
| Yices2 | 0 | 5507 | 38394.506444 | 38579.275236 | 0 | 0 | 0 | 1832 | 0 | 25 | 0 |
| cvc5 | 0 | 4653 | 292593.028001 | 292891.818349 | 0 | 0 | 0 | 1832 | 0 | 228 | 4 |
| SMTInterpol | 0 | 3337 | 443360.495438 | 387634.138995 | 0 | 0 | 0 | 1832 | 0 | 218 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Yices2 | 0 | 3670 | 1014.802531 | 1174.696744 | 0 | 0 | 0 | 1780 | 52 | 0 | 0 |
| Bitwuzla | 0 | 3645 | 1408.291954 | 1565.040703 | 0 | 0 | 0 | 1754 | 78 | 0 | 0 |
| cvc5 | 0 | 2964 | 2961.379303 | 3096.593474 | 0 | 0 | 0 | 1535 | 297 | 0 | 0 |
| SMTInterpol | 0 | 1709 | 18845.733808 | 6989.337251 | 0 | 0 | 0 | 905 | 927 | 0 | 0 |