The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the FPArith division in the Single Query Track.
Page generated on 2022-08-10 11:17:44 +0000
Benchmarks: 1835 Time Limit: 1200 seconds Memory Limit: 60 GB
Logics:| 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 | 0 | 1620 | 286384.484 | 286329.452 | 1620 | 431 | 1189 | 215 | 0 | 213 | 0 |
| z3-4.8.17n | 0 | 1569 | 377537.2 | 377513.632 | 1569 | 489 | 1080 | 266 | 0 | 256 | 0 |
| cvc5 | 0 | 1518 | 383023.408 | 387780.587 | 1518 | 400 | 1118 | 317 | 0 | 280 | 0 |
| 2021-cvc5n | 0 | 1474 | 421673.964 | 436847.304 | 1474 | 351 | 1123 | 361 | 0 | 324 | 0 |
| UltimateEliminator+MathSAT | 0 | 277 | 44345.31 | 41654.593 | 277 | 86 | 191 | 1558 | 0 | 30 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Bitwuzla | 0 | 1620 | 286414.234 | 286321.232 | 1620 | 431 | 1189 | 215 | 0 | 213 | 0 |
| z3-4.8.17n | 0 | 1569 | 377593.85 | 377502.092 | 1569 | 489 | 1080 | 266 | 0 | 256 | 0 |
| cvc5 | 0 | 1518 | 387024.718 | 387768.927 | 1518 | 400 | 1118 | 317 | 0 | 280 | 0 |
| 2021-cvc5n | 0 | 1474 | 436403.597 | 436831.004 | 1474 | 351 | 1123 | 361 | 0 | 324 | 0 |
| UltimateEliminator+MathSAT | 0 | 277 | 44345.31 | 41654.593 | 277 | 86 | 191 | 1558 | 0 | 30 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| z3-4.8.17n | 0 | 489 | 128367.961 | 128342.547 | 489 | 489 | 0 | 84 | 1262 | 256 | 0 |
| Bitwuzla | 0 | 431 | 190574.661 | 190533.252 | 431 | 431 | 0 | 142 | 1262 | 213 | 0 |
| cvc5 | 0 | 400 | 200421.358 | 200328.795 | 400 | 400 | 0 | 173 | 1262 | 280 | 0 |
| 2021-cvc5n | 0 | 351 | 247412.994 | 247465.288 | 351 | 351 | 0 | 222 | 1262 | 324 | 0 |
| UltimateEliminator+MathSAT | 0 | 86 | 3631.94 | 3018.788 | 86 | 86 | 0 | 487 | 1262 | 30 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Bitwuzla | 0 | 1189 | 21439.573 | 21387.98 | 1189 | 0 | 1189 | 7 | 639 | 213 | 0 |
| 2021-cvc5n | 0 | 1123 | 110989.689 | 111364.803 | 1123 | 0 | 1123 | 73 | 639 | 324 | 0 |
| cvc5 | 0 | 1118 | 114602.018 | 115438.79 | 1118 | 0 | 1118 | 78 | 639 | 280 | 0 |
| z3-4.8.17n | 0 | 1080 | 179541.343 | 179474.985 | 1080 | 0 | 1080 | 116 | 639 | 256 | 0 |
| UltimateEliminator+MathSAT | 0 | 191 | 21261.623 | 19268.184 | 191 | 0 | 191 | 1005 | 639 | 30 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Bitwuzla | 0 | 1464 | 9980.517 | 9973.854 | 1464 | 335 | 1129 | 371 | 0 | 369 | 0 |
| cvc5 | 0 | 1342 | 12952.112 | 12907.775 | 1342 | 313 | 1029 | 493 | 0 | 456 | 0 |
| 2021-cvc5n | 0 | 1319 | 13433.92 | 13415.385 | 1319 | 287 | 1032 | 516 | 0 | 479 | 0 |
| z3-4.8.17n | 0 | 1280 | 15474.431 | 15448.226 | 1280 | 368 | 912 | 555 | 0 | 547 | 0 |
| UltimateEliminator+MathSAT | 0 | 268 | 10595.706 | 7658.447 | 268 | 80 | 188 | 1567 | 0 | 46 | 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.