The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_ABVFP division in the Single Query Track.
Page generated on 2020-07-04 11:46:58 +0000
Benchmarks: 500 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 | 499 | 4265.161 | 4260.902 | 499 | 93 | 406 | 1 | 1 | 0 | |
| Bitwuzla | 0 | 499 | 4266.55 | 4267.847 | 499 | 93 | 406 | 1 | 1 | 0 | |
| MathSAT5n | 0 | 493 | 12917.083 | 12899.568 | 493 | 93 | 400 | 7 | 7 | 0 | |
| CVC4 | 0 | 489 | 18463.334 | 18439.394 | 489 | 89 | 400 | 11 | 11 | 0 | |
| COLIBRI | 0 | 406 | 26246.007 | 26188.408 | 406 | 83 | 323 | 94 | 20 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Bitwuzla-fixedn | 0 | 499 | 4265.551 | 4260.792 | 499 | 93 | 406 | 1 | 1 | 0 | |
| Bitwuzla | 0 | 499 | 4266.9 | 4267.817 | 499 | 93 | 406 | 1 | 1 | 0 | |
| MathSAT5n | 0 | 493 | 12919.533 | 12899.278 | 493 | 93 | 400 | 7 | 7 | 0 | |
| CVC4 | 0 | 489 | 18466.244 | 18438.744 | 489 | 89 | 400 | 11 | 11 | 0 | |
| COLIBRI | 0 | 406 | 26247.187 | 26187.668 | 406 | 83 | 323 | 94 | 20 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Bitwuzla-fixedn | 0 | 93 | 239.038 | 239.148 | 93 | 93 | 0 | 407 | 1 | 0 |
| Bitwuzla | 0 | 93 | 241.17 | 241.197 | 93 | 93 | 0 | 407 | 1 | 0 |
| MathSAT5n | 0 | 93 | 1237.198 | 1231.695 | 93 | 93 | 0 | 407 | 7 | 0 |
| CVC4 | 0 | 89 | 5613.321 | 5613.481 | 89 | 89 | 0 | 411 | 11 | 0 |
| COLIBRI | 0 | 83 | 3787.881 | 3784.61 | 83 | 83 | 0 | 417 | 20 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Bitwuzla-fixedn | 0 | 406 | 2826.513 | 2821.644 | 406 | 0 | 406 | 94 | 1 | 0 |
| Bitwuzla | 0 | 406 | 2825.73 | 2826.62 | 406 | 0 | 406 | 94 | 1 | 0 |
| MathSAT5n | 0 | 400 | 10482.335 | 10467.584 | 400 | 0 | 400 | 100 | 7 | 0 |
| CVC4 | 0 | 400 | 11652.923 | 11625.264 | 400 | 0 | 400 | 100 | 11 | 0 |
| COLIBRI | 0 | 323 | 21529.53 | 21473.239 | 323 | 0 | 323 | 177 | 20 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Bitwuzla | 0 | 487 | 876.742 | 876.915 | 487 | 91 | 396 | 13 | 13 | 0 | |
| Bitwuzla-fixedn | 0 | 487 | 883.833 | 878.67 | 487 | 91 | 396 | 13 | 13 | 0 | |
| MathSAT5n | 0 | 471 | 2104.035 | 2083.028 | 471 | 85 | 386 | 29 | 29 | 0 | |
| CVC4 | 0 | 460 | 2286.992 | 2258.707 | 460 | 83 | 377 | 40 | 40 | 0 | |
| COLIBRI | 0 | 400 | 1395.61 | 1384.449 | 400 | 82 | 318 | 100 | 27 | 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.