The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_BVFP division in the Single Query Track.
Page generated on 2020-07-04 11:46:59 +0000
Benchmarks: 394 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 | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Bitwuzla-fixedn | 0 | 394 | 778.029 | 778.417 | 394 | 186 | 208 | 0 | 0 | 0 | |
| Bitwuzla | 0 | 394 | 781.529 | 777.604 | 394 | 186 | 208 | 0 | 0 | 0 | |
| CVC4 | 0 | 394 | 1686.879 | 1663.37 | 394 | 186 | 208 | 0 | 0 | 0 | |
| 2019-Par4n | 0 | 393 | 2699.895 | 1818.448 | 393 | 185 | 208 | 1 | 1 | 0 | |
| MathSAT5n | 0 | 391 | 5739.129 | 5737.693 | 391 | 186 | 205 | 3 | 3 | 0 | |
| z3n | 0 | 386 | 13314.509 | 13313.796 | 386 | 185 | 201 | 8 | 8 | 0 | |
| COLIBRI | 0 | 366 | 3075.447 | 3076.625 | 366 | 181 | 185 | 28 | 2 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Bitwuzla | 0 | 394 | 781.529 | 777.604 | 394 | 186 | 208 | 0 | 0 | 0 | |
| Bitwuzla-fixedn | 0 | 394 | 778.029 | 778.417 | 394 | 186 | 208 | 0 | 0 | 0 | |
| CVC4 | 0 | 394 | 1686.879 | 1663.37 | 394 | 186 | 208 | 0 | 0 | 0 | |
| 2019-Par4n | 0 | 393 | 2699.895 | 1818.448 | 393 | 185 | 208 | 1 | 1 | 0 | |
| MathSAT5n | 0 | 391 | 5739.249 | 5737.533 | 391 | 186 | 205 | 3 | 3 | 0 | |
| z3n | 0 | 386 | 13315.999 | 13313.586 | 386 | 185 | 201 | 8 | 8 | 0 | |
| COLIBRI | 0 | 366 | 3075.557 | 3076.605 | 366 | 181 | 185 | 28 | 2 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Bitwuzla-fixedn | 0 | 186 | 159.292 | 159.347 | 186 | 186 | 0 | 208 | 0 | 0 |
| Bitwuzla | 0 | 186 | 161.223 | 159.73 | 186 | 186 | 0 | 208 | 0 | 0 |
| MathSAT5n | 0 | 186 | 382.88 | 381.882 | 186 | 186 | 0 | 208 | 3 | 0 |
| CVC4 | 0 | 186 | 856.244 | 837.671 | 186 | 186 | 0 | 208 | 0 | 0 |
| 2019-Par4n | 0 | 185 | 1534.342 | 1370.643 | 185 | 185 | 0 | 209 | 1 | 0 |
| z3n | 0 | 185 | 2316.911 | 2315.647 | 185 | 185 | 0 | 209 | 8 | 0 |
| COLIBRI | 0 | 181 | 271.591 | 271.924 | 181 | 181 | 0 | 213 | 2 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 208 | 1165.554 | 447.805 | 208 | 0 | 208 | 186 | 1 | 0 |
| Bitwuzla | 0 | 208 | 620.306 | 617.874 | 208 | 0 | 208 | 186 | 0 | 0 |
| Bitwuzla-fixedn | 0 | 208 | 618.736 | 619.07 | 208 | 0 | 208 | 186 | 0 | 0 |
| CVC4 | 0 | 208 | 830.635 | 825.699 | 208 | 0 | 208 | 186 | 0 | 0 |
| MathSAT5n | 0 | 205 | 5356.369 | 5355.652 | 205 | 0 | 205 | 189 | 3 | 0 |
| z3n | 0 | 201 | 10999.089 | 10997.939 | 201 | 0 | 201 | 193 | 8 | 0 |
| COLIBRI | 0 | 185 | 2803.967 | 2804.681 | 185 | 0 | 185 | 209 | 2 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Bitwuzla-fixedn | 0 | 387 | 540.718 | 541.01 | 387 | 184 | 203 | 7 | 7 | 0 | |
| Bitwuzla | 0 | 387 | 545.18 | 541.226 | 387 | 184 | 203 | 7 | 7 | 0 | |
| 2019-Par4n | 0 | 387 | 940.689 | 543.603 | 387 | 184 | 203 | 7 | 7 | 0 | |
| CVC4 | 0 | 384 | 1080.887 | 1057.253 | 384 | 183 | 201 | 10 | 10 | 0 | |
| MathSAT5n | 0 | 375 | 1013.913 | 1011.852 | 375 | 183 | 192 | 19 | 19 | 0 | |
| z3n | 0 | 358 | 1829.669 | 1826.614 | 358 | 177 | 181 | 36 | 36 | 0 | |
| COLIBRI | 0 | 356 | 611.02 | 611.978 | 356 | 177 | 179 | 38 | 12 | 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.