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 Unsat Core Track.
Page generated on 2021-07-18 17:31:25 +0000
Benchmarks: 1586 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance |
|---|---|
| Bitwuzla | Bitwuzla |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Timeout | Memout |
|---|---|---|---|---|---|---|
| Bitwuzla | 0 | 14216 | 3267.605 | 3268.495 | 1 | 0 |
| 2020-Bitwuzlan | 0 | 14137 | 3180.394 | 3148.9 | 1 | 0 |
| 2020-Bitwuzla-fixedn | 0 | 14134 | 3264.92 | 3265.892 | 1 | 0 |
| z3n | 0 | 14074 | 48151.475 | 48131.454 | 29 | 0 |
| cvc5-uc | 0 | 13947 | 3588.014 | 3585.523 | 0 | 0 |
| MathSAT5n | 0 | 263 | 29.115 | 30.59 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Timeout | Memout |
|---|---|---|---|---|---|---|
| Bitwuzla | 0 | 14216 | 3267.765 | 3268.415 | 1 | 0 |
| 2020-Bitwuzlan | 0 | 14137 | 3180.434 | 3148.88 | 1 | 0 |
| 2020-Bitwuzla-fixedn | 0 | 14134 | 3264.96 | 3265.822 | 1 | 0 |
| z3n | 0 | 14074 | 48159.125 | 48130.264 | 29 | 0 |
| cvc5-uc | 0 | 13947 | 3588.014 | 3585.523 | 0 | 0 |
| MathSAT5n | 0 | 263 | 29.115 | 30.59 | 0 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.