The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_ABVFP logic in the Single Query Track.
Page generated on 2023-07-06 16:04:54 +0000
Benchmarks: 593 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| Bitwuzla | Bitwuzla | Bitwuzla | Bitwuzla | Bitwuzla |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2022-Bitwuzlan | 0 | 593 | 3105.419 | 3105.898 | 593 | 103 | 490 | 0 | 0 | 0 |
| Bitwuzla Fixedn | 0 | 592 | 1998.245 | 1998.559 | 592 | 103 | 489 | 1 | 1 | 0 |
| Bitwuzla | 0 | 592 | 2036.655 | 2012.415 | 592 | 103 | 489 | 1 | 1 | 0 |
| cvc5 | 0 | 511 | 23600.502 | 23592.094 | 511 | 92 | 419 | 82 | 10 | 0 |
| COLIBRI | 0 | 476 | 1606.495 | 1589.487 | 476 | 89 | 387 | 117 | 31 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2022-Bitwuzlan | 0 | 593 | 3105.419 | 3105.898 | 593 | 103 | 490 | 0 | 0 | 0 |
| Bitwuzla Fixedn | 0 | 592 | 1998.245 | 1998.559 | 592 | 103 | 489 | 1 | 1 | 0 |
| Bitwuzla | 0 | 592 | 2036.655 | 2012.415 | 592 | 103 | 489 | 1 | 1 | 0 |
| cvc5 | 0 | 511 | 23600.502 | 23592.094 | 511 | 92 | 419 | 82 | 10 | 0 |
| COLIBRI | 0 | 476 | 1606.495 | 1589.487 | 476 | 89 | 387 | 117 | 31 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Bitwuzla | 0 | 103 | 214.613 | 207.715 | 103 | 103 | 0 | 0 | 490 | 1 | 0 |
| Bitwuzla Fixedn | 0 | 103 | 208.321 | 208.361 | 103 | 103 | 0 | 0 | 490 | 1 | 0 |
| 2022-Bitwuzlan | 0 | 103 | 251.298 | 251.428 | 103 | 103 | 0 | 0 | 490 | 0 | 0 |
| cvc5 | 0 | 92 | 1578.993 | 1569.621 | 92 | 92 | 0 | 11 | 490 | 10 | 0 |
| COLIBRI | 0 | 89 | 465.108 | 462.922 | 89 | 89 | 0 | 14 | 490 | 31 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2022-Bitwuzlan | 0 | 490 | 2854.121 | 2854.471 | 490 | 0 | 490 | 0 | 103 | 0 | 0 |
| Bitwuzla Fixedn | 0 | 489 | 1789.925 | 1790.198 | 489 | 0 | 489 | 1 | 103 | 1 | 0 |
| Bitwuzla | 0 | 489 | 1822.043 | 1804.7 | 489 | 0 | 489 | 1 | 103 | 1 | 0 |
| cvc5 | 0 | 419 | 22021.509 | 22022.473 | 419 | 0 | 419 | 71 | 103 | 10 | 0 |
| COLIBRI | 0 | 387 | 1141.387 | 1126.565 | 387 | 0 | 387 | 103 | 103 | 31 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Bitwuzla | 0 | 578 | 748.705 | 724.294 | 578 | 101 | 477 | 15 | 15 | 0 |
| Bitwuzla Fixedn | 0 | 578 | 726.7 | 726.837 | 578 | 101 | 477 | 15 | 15 | 0 |
| 2022-Bitwuzlan | 0 | 575 | 688.361 | 688.636 | 575 | 101 | 474 | 18 | 18 | 0 |
| COLIBRI | 0 | 469 | 1223.704 | 1206.612 | 469 | 86 | 383 | 124 | 38 | 0 |
| cvc5 | 0 | 369 | 1874.553 | 1861.509 | 369 | 74 | 295 | 224 | 152 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.