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 Single Query Track.
Page generated on 2023-07-06 16:04:54 +0000
Benchmarks: 10084 Time Limit: 1200 seconds Memory Limit: 60 GB
Logics:| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| STP | STP | STP | STP | STP |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Bitwuzla Fixedn | 0 | 9848 | 161353.128 | 160973.041 | 9848 | 4772 | 5076 | 236 | 0 | 236 | 0 |
| STP | 0 | 9847 | 138024.791 | 137675.49 | 9847 | 4773 | 5074 | 237 | 0 | 236 | 0 |
| 2022-STP-fixedn | 0 | 9846 | 136804.166 | 136545.551 | 9846 | 4773 | 5073 | 238 | 0 | 237 | 0 |
| Bitwuzla | 0 | 9618 | 183578.608 | 182832.756 | 9618 | 4772 | 4846 | 466 | 0 | 466 | 0 |
| Yices2 | 0 | 9384 | 168657.443 | 168411.03 | 9384 | 4715 | 4669 | 700 | 0 | 700 | 0 |
| cvc5 | 0 | 9284 | 406582.764 | 405717.857 | 9284 | 4630 | 4654 | 800 | 0 | 790 | 2 |
| Z3-Owl Fixedn | 0 | 8894 | 578448.56 | 577594.392 | 8894 | 4625 | 4269 | 1190 | 0 | 1190 | 0 |
| Z3-Owl | 0 | 7976 | 459878.565 | 458925.184 | 7976 | 4376 | 3600 | 2108 | 0 | 2108 | 0 |
| UltimateIntBlastingWrapper+SMTInterpol | 0 | 3150 | 754973.118 | 648378.796 | 3150 | 908 | 2242 | 6934 | 0 | 4268 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Bitwuzla Fixedn | 0 | 9848 | 161353.128 | 160973.041 | 9848 | 4772 | 5076 | 236 | 0 | 236 | 0 |
| STP | 0 | 9847 | 138024.791 | 137675.49 | 9847 | 4773 | 5074 | 237 | 0 | 236 | 0 |
| 2022-STP-fixedn | 0 | 9846 | 136804.166 | 136545.551 | 9846 | 4773 | 5073 | 238 | 0 | 237 | 0 |
| Bitwuzla | 0 | 9618 | 183578.608 | 182832.756 | 9618 | 4772 | 4846 | 466 | 0 | 466 | 0 |
| Yices2 | 0 | 9384 | 168657.443 | 168411.03 | 9384 | 4715 | 4669 | 700 | 0 | 700 | 0 |
| cvc5 | 0 | 9284 | 406582.764 | 405717.857 | 9284 | 4630 | 4654 | 800 | 0 | 790 | 2 |
| Z3-Owl Fixedn | 0 | 8894 | 578448.56 | 577594.392 | 8894 | 4625 | 4269 | 1190 | 0 | 1190 | 0 |
| Z3-Owl | 0 | 7976 | 459878.565 | 458925.184 | 7976 | 4376 | 3600 | 2108 | 0 | 2108 | 0 |
| UltimateIntBlastingWrapper+SMTInterpol | 0 | 3221 | 844319.598 | 728071.856 | 3221 | 918 | 2303 | 6863 | 0 | 4196 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2022-STP-fixedn | 0 | 4773 | 58614.057 | 58418.2 | 4773 | 4773 | 0 | 42 | 5269 | 237 | 0 |
| STP | 0 | 4773 | 58730.446 | 58560.425 | 4773 | 4773 | 0 | 42 | 5269 | 236 | 0 |
| Bitwuzla Fixedn | 0 | 4772 | 70283.675 | 70053.855 | 4772 | 4772 | 0 | 43 | 5269 | 236 | 0 |
| Bitwuzla | 0 | 4772 | 73677.282 | 73273.993 | 4772 | 4772 | 0 | 43 | 5269 | 466 | 0 |
| Yices2 | 0 | 4715 | 102940.734 | 102780.634 | 4715 | 4715 | 0 | 100 | 5269 | 700 | 0 |
| cvc5 | 0 | 4630 | 157238.066 | 156705.295 | 4630 | 4630 | 0 | 185 | 5269 | 790 | 2 |
| Z3-Owl Fixedn | 0 | 4625 | 292970.24 | 292462.843 | 4625 | 4625 | 0 | 190 | 5269 | 1190 | 0 |
| Z3-Owl | 0 | 4376 | 241044.259 | 240420.605 | 4376 | 4376 | 0 | 439 | 5269 | 2108 | 0 |
| UltimateIntBlastingWrapper+SMTInterpol | 0 | 918 | 254932.101 | 226939.66 | 918 | 918 | 0 | 3897 | 5269 | 4196 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Bitwuzla Fixedn | 0 | 5076 | 91069.454 | 90919.186 | 5076 | 0 | 5076 | 88 | 4920 | 236 | 0 |
| STP | 0 | 5074 | 79294.344 | 79115.065 | 5074 | 0 | 5074 | 90 | 4920 | 236 | 0 |
| 2022-STP-fixedn | 0 | 5073 | 78190.109 | 78127.35 | 5073 | 0 | 5073 | 91 | 4920 | 237 | 0 |
| Bitwuzla | 0 | 4846 | 109901.326 | 109558.763 | 4846 | 0 | 4846 | 318 | 4920 | 466 | 0 |
| Yices2 | 0 | 4669 | 65716.708 | 65630.396 | 4669 | 0 | 4669 | 495 | 4920 | 700 | 0 |
| cvc5 | 0 | 4654 | 249344.698 | 249012.562 | 4654 | 0 | 4654 | 510 | 4920 | 790 | 2 |
| Z3-Owl Fixedn | 0 | 4269 | 285478.32 | 285131.549 | 4269 | 0 | 4269 | 895 | 4920 | 1190 | 0 |
| Z3-Owl | 0 | 3600 | 218834.306 | 218504.579 | 3600 | 0 | 3600 | 1564 | 4920 | 2108 | 0 |
| UltimateIntBlastingWrapper+SMTInterpol | 0 | 2303 | 589387.496 | 501132.195 | 2303 | 0 | 2303 | 2861 | 4920 | 4196 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| STP | 0 | 9273 | 13680.789 | 13473.301 | 9273 | 4539 | 4734 | 811 | 0 | 810 | 0 |
| 2022-STP-fixedn | 0 | 9272 | 13655.706 | 13467.989 | 9272 | 4537 | 4735 | 812 | 0 | 811 | 0 |
| Bitwuzla Fixedn | 0 | 9139 | 25378.217 | 25022.198 | 9139 | 4452 | 4687 | 945 | 0 | 945 | 0 |
| Bitwuzla | 0 | 8807 | 25639.735 | 25125.553 | 8807 | 4435 | 4372 | 1277 | 0 | 1277 | 0 |
| Yices2 | 0 | 8608 | 7610.387 | 7509.509 | 8608 | 4200 | 4408 | 1476 | 0 | 1476 | 0 |
| cvc5 | 0 | 7406 | 28618.098 | 28197.719 | 7406 | 3603 | 3803 | 2678 | 0 | 2676 | 2 |
| Z3-Owl Fixedn | 0 | 5649 | 28716.16 | 28314.532 | 5649 | 2572 | 3077 | 4435 | 0 | 4435 | 0 |
| Z3-Owl | 0 | 5368 | 26369.253 | 26052.655 | 5368 | 2559 | 2809 | 4716 | 0 | 4716 | 0 |
| UltimateIntBlastingWrapper+SMTInterpol | 0 | 1557 | 38207.063 | 13817.813 | 1557 | 248 | 1309 | 8527 | 0 | 5942 | 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.