The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_BVFP logic in the Single Query Track.
Page generated on 2021-07-18 17:29:06 +0000
Benchmarks: 484 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 |
|---|---|---|---|---|---|---|---|---|---|---|
| 2020-Bitwuzla-fixedn | 0 | 484 | 2101.451 | 2099.879 | 484 | 221 | 263 | 0 | 0 | 0 |
| 2020-Bitwuzlan | 0 | 484 | 2140.414 | 2115.661 | 484 | 221 | 263 | 0 | 0 | 0 |
| Bitwuzla | 0 | 484 | 2578.135 | 2569.834 | 484 | 221 | 263 | 0 | 0 | 0 |
| cvc5 | 0 | 482 | 4945.124 | 4909.625 | 482 | 221 | 261 | 2 | 2 | 0 |
| 2020-CVC4n | 0 | 482 | 5361.275 | 5311.733 | 482 | 221 | 261 | 2 | 2 | 0 |
| MathSAT5n | 0 | 478 | 10344.199 | 10343.633 | 478 | 221 | 257 | 6 | 6 | 0 |
| 2020-MathSAT5n | 0 | 478 | 10462.524 | 10438.296 | 478 | 221 | 257 | 6 | 6 | 0 |
| z3n | 0 | 477 | 16432.982 | 16378.255 | 477 | 221 | 256 | 7 | 7 | 0 |
| 2020-COLIBRIn | 0 | 451 | 3086.423 | 3087.23 | 451 | 214 | 237 | 33 | 2 | 0 |
| COLIBRI - fixedn | 0 | 451 | 3354.019 | 3354.624 | 451 | 214 | 237 | 33 | 2 | 0 |
| COLIBRI | 4 | 447 | 2813.715 | 2812.891 | 447 | 210 | 237 | 37 | 2 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2020-Bitwuzla-fixedn | 0 | 484 | 2101.451 | 2099.879 | 484 | 221 | 263 | 0 | 0 | 0 |
| 2020-Bitwuzlan | 0 | 484 | 2140.414 | 2115.661 | 484 | 221 | 263 | 0 | 0 | 0 |
| Bitwuzla | 0 | 484 | 2578.135 | 2569.834 | 484 | 221 | 263 | 0 | 0 | 0 |
| cvc5 | 0 | 482 | 4945.704 | 4909.575 | 482 | 221 | 261 | 2 | 2 | 0 |
| 2020-CVC4n | 0 | 482 | 5362.435 | 5311.663 | 482 | 221 | 261 | 2 | 2 | 0 |
| MathSAT5n | 0 | 478 | 10344.659 | 10343.353 | 478 | 221 | 257 | 6 | 6 | 0 |
| 2020-MathSAT5n | 0 | 478 | 10463.534 | 10437.986 | 478 | 221 | 257 | 6 | 6 | 0 |
| z3n | 0 | 477 | 16433.752 | 16377.795 | 477 | 221 | 256 | 7 | 7 | 0 |
| 2020-COLIBRIn | 0 | 451 | 3086.493 | 3087.17 | 451 | 214 | 237 | 33 | 2 | 0 |
| COLIBRI - fixedn | 0 | 451 | 3354.429 | 3354.494 | 451 | 214 | 237 | 33 | 2 | 0 |
| COLIBRI | 4 | 447 | 2813.845 | 2812.831 | 447 | 210 | 237 | 37 | 2 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Bitwuzla | 0 | 221 | 181.982 | 178.279 | 221 | 221 | 0 | 0 | 263 | 0 | 0 |
| 2020-Bitwuzla-fixedn | 0 | 221 | 237.728 | 235.528 | 221 | 221 | 0 | 0 | 263 | 0 | 0 |
| 2020-Bitwuzlan | 0 | 221 | 236.587 | 236.667 | 221 | 221 | 0 | 0 | 263 | 0 | 0 |
| cvc5 | 0 | 221 | 638.875 | 628.195 | 221 | 221 | 0 | 0 | 263 | 2 | 0 |
| 2020-CVC4n | 0 | 221 | 725.248 | 722.4 | 221 | 221 | 0 | 0 | 263 | 2 | 0 |
| MathSAT5n | 0 | 221 | 1172.799 | 1173.152 | 221 | 221 | 0 | 0 | 263 | 6 | 0 |
| 2020-MathSAT5n | 0 | 221 | 1213.141 | 1213.468 | 221 | 221 | 0 | 0 | 263 | 6 | 0 |
| z3n | 0 | 221 | 2089.109 | 2089.739 | 221 | 221 | 0 | 0 | 263 | 7 | 0 |
| COLIBRI - fixedn | 0 | 214 | 1446.718 | 1445.523 | 214 | 214 | 0 | 7 | 263 | 2 | 0 |
| 2020-COLIBRIn | 0 | 214 | 1528.851 | 1529.399 | 214 | 214 | 0 | 7 | 263 | 2 | 0 |
| COLIBRI | 0 | 210 | 1429.983 | 1428.644 | 210 | 210 | 0 | 11 | 263 | 2 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2020-Bitwuzla-fixedn | 0 | 263 | 1863.724 | 1864.351 | 263 | 0 | 263 | 0 | 221 | 0 | 0 |
| 2020-Bitwuzlan | 0 | 263 | 1903.826 | 1878.994 | 263 | 0 | 263 | 0 | 221 | 0 | 0 |
| Bitwuzla | 0 | 263 | 2396.152 | 2391.555 | 263 | 0 | 263 | 0 | 221 | 0 | 0 |
| cvc5 | 0 | 261 | 4306.829 | 4281.381 | 261 | 0 | 261 | 2 | 221 | 2 | 0 |
| 2020-CVC4n | 0 | 261 | 4637.187 | 4589.263 | 261 | 0 | 261 | 2 | 221 | 2 | 0 |
| MathSAT5n | 0 | 257 | 9171.861 | 9170.201 | 257 | 0 | 257 | 6 | 221 | 6 | 0 |
| 2020-MathSAT5n | 0 | 257 | 9250.393 | 9224.518 | 257 | 0 | 257 | 6 | 221 | 6 | 0 |
| z3n | 0 | 256 | 14344.642 | 14288.056 | 256 | 0 | 256 | 7 | 221 | 7 | 0 |
| 2020-COLIBRIn | 0 | 237 | 1557.642 | 1557.771 | 237 | 0 | 237 | 26 | 221 | 2 | 0 |
| COLIBRI - fixedn | 0 | 237 | 1907.711 | 1908.971 | 237 | 0 | 237 | 26 | 221 | 2 | 0 |
| COLIBRI | 4 | 237 | 1383.862 | 1384.187 | 237 | 0 | 237 | 26 | 221 | 2 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Bitwuzla | 0 | 474 | 734.209 | 725.759 | 474 | 220 | 254 | 10 | 10 | 0 |
| 2020-Bitwuzla-fixedn | 0 | 473 | 726.453 | 724.418 | 473 | 219 | 254 | 11 | 11 | 0 |
| 2020-Bitwuzlan | 0 | 473 | 724.72 | 724.939 | 473 | 219 | 254 | 11 | 11 | 0 |
| 2020-CVC4n | 0 | 467 | 1433.367 | 1429.155 | 467 | 214 | 253 | 17 | 17 | 0 |
| cvc5 | 0 | 465 | 1815.068 | 1778.783 | 465 | 216 | 249 | 19 | 19 | 0 |
| MathSAT5n | 0 | 455 | 1340.595 | 1338.613 | 455 | 214 | 241 | 29 | 29 | 0 |
| 2020-MathSAT5n | 0 | 453 | 1400.634 | 1374.471 | 453 | 214 | 239 | 31 | 31 | 0 |
| COLIBRI - fixedn | 0 | 449 | 548.032 | 548.078 | 449 | 214 | 235 | 35 | 4 | 0 |
| 2020-COLIBRIn | 0 | 446 | 666.054 | 666.712 | 446 | 212 | 234 | 38 | 7 | 0 |
| z3n | 0 | 420 | 2682.155 | 2677.962 | 420 | 199 | 221 | 64 | 64 | 0 |
| COLIBRI | 4 | 447 | 461.845 | 460.831 | 447 | 210 | 237 | 37 | 2 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.