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 2023-07-06 16:04:54 +0000
Benchmarks: 1849 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 | 1722 | 30652.085 | 30606.759 | 1722 | 571 | 1151 | 127 | 0 | 127 | 0 |
| Bitwuzla Fixedn | 0 | 1722 | 30667.358 | 30615.341 | 1722 | 572 | 1150 | 127 | 0 | 127 | 0 |
| 2022-Bitwuzlan | 0 | 1605 | 33035.414 | 33010.42 | 1605 | 432 | 1173 | 244 | 0 | 240 | 0 |
| cvc5 | 0 | 1499 | 54723.012 | 56850.519 | 1499 | 398 | 1101 | 350 | 0 | 294 | 0 |
| UltimateEliminator+MathSAT | 0 | 291 | 1946.513 | 1474.106 | 291 | 96 | 195 | 1558 | 0 | 25 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Bitwuzla | 0 | 1722 | 30652.085 | 30606.759 | 1722 | 571 | 1151 | 127 | 0 | 127 | 0 |
| Bitwuzla Fixedn | 0 | 1722 | 30667.358 | 30615.341 | 1722 | 572 | 1150 | 127 | 0 | 127 | 0 |
| 2022-Bitwuzlan | 0 | 1605 | 33035.414 | 33010.42 | 1605 | 432 | 1173 | 244 | 0 | 240 | 0 |
| cvc5 | 0 | 1499 | 54723.012 | 56850.519 | 1499 | 398 | 1101 | 350 | 0 | 294 | 0 |
| UltimateEliminator+MathSAT | 0 | 291 | 1946.513 | 1474.106 | 291 | 96 | 195 | 1558 | 0 | 25 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Bitwuzla Fixedn | 0 | 572 | 17412.303 | 17363.157 | 572 | 572 | 0 | 0 | 1277 | 127 | 0 |
| Bitwuzla | 0 | 571 | 16182.41 | 16183.432 | 571 | 571 | 0 | 1 | 1277 | 127 | 0 |
| 2022-Bitwuzlan | 0 | 432 | 18630.522 | 18609.899 | 432 | 432 | 0 | 140 | 1277 | 240 | 0 |
| cvc5 | 0 | 398 | 27382.996 | 27686.339 | 398 | 398 | 0 | 174 | 1277 | 294 | 0 |
| UltimateEliminator+MathSAT | 0 | 96 | 970.494 | 776.556 | 96 | 96 | 0 | 476 | 1277 | 25 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2022-Bitwuzlan | 0 | 1173 | 14404.893 | 14400.521 | 1173 | 0 | 1173 | 13 | 663 | 240 | 0 |
| Bitwuzla | 0 | 1151 | 14469.675 | 14423.327 | 1151 | 0 | 1151 | 35 | 663 | 127 | 0 |
| Bitwuzla Fixedn | 0 | 1150 | 13255.055 | 13252.183 | 1150 | 0 | 1150 | 36 | 663 | 127 | 0 |
| cvc5 | 0 | 1101 | 27340.016 | 29164.18 | 1101 | 0 | 1101 | 85 | 663 | 294 | 0 |
| UltimateEliminator+MathSAT | 0 | 195 | 976.019 | 697.55 | 195 | 0 | 195 | 991 | 663 | 25 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Bitwuzla | 0 | 1577 | 1191.931 | 1186.629 | 1577 | 483 | 1094 | 272 | 0 | 272 | 0 |
| Bitwuzla Fixedn | 0 | 1577 | 1194.603 | 1187.74 | 1577 | 483 | 1094 | 272 | 0 | 272 | 0 |
| 2022-Bitwuzlan | 0 | 1459 | 1148.074 | 1118.537 | 1459 | 347 | 1112 | 390 | 0 | 386 | 0 |
| cvc5 | 0 | 1322 | 2139.587 | 2123.532 | 1322 | 316 | 1006 | 527 | 0 | 494 | 0 |
| UltimateEliminator+MathSAT | 0 | 284 | 1692.062 | 1134.426 | 284 | 90 | 194 | 1565 | 0 | 38 | 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.