The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the FP logic in the Single Query Track.
Page generated on 2023-07-06 16:04:54 +0000
Benchmarks: 1334 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 |
|---|---|---|---|---|---|---|---|---|---|---|
| 2022-Bitwuzlan | 0 | 1254 | 29722.405 | 29696.886 | 1254 | 119 | 1135 | 80 | 80 | 0 |
| Bitwuzla | 0 | 1235 | 29894.034 | 29848.482 | 1235 | 121 | 1114 | 99 | 99 | 0 |
| Bitwuzla Fixedn | 0 | 1235 | 29895.75 | 29845.092 | 1235 | 122 | 1113 | 99 | 99 | 0 |
| cvc5 | 0 | 1168 | 44192.685 | 46098.542 | 1168 | 98 | 1070 | 166 | 143 | 0 |
| UltimateEliminator+MathSAT | 0 | 175 | 846.697 | 612.483 | 175 | 2 | 173 | 1159 | 25 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2022-Bitwuzlan | 0 | 1254 | 29722.405 | 29696.886 | 1254 | 119 | 1135 | 80 | 80 | 0 |
| Bitwuzla Fixedn | 0 | 1235 | 29895.75 | 29845.092 | 1235 | 122 | 1113 | 99 | 99 | 0 |
| Bitwuzla | 0 | 1235 | 29894.034 | 29848.482 | 1235 | 121 | 1114 | 99 | 99 | 0 |
| cvc5 | 0 | 1168 | 44192.685 | 46098.542 | 1168 | 98 | 1070 | 166 | 143 | 0 |
| UltimateEliminator+MathSAT | 0 | 175 | 846.697 | 612.483 | 175 | 2 | 173 | 1159 | 25 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Bitwuzla Fixedn | 0 | 122 | 16963.362 | 16915.622 | 122 | 122 | 0 | 0 | 1212 | 99 | 0 |
| Bitwuzla | 0 | 121 | 15742.455 | 15743.338 | 121 | 121 | 0 | 1 | 1212 | 99 | 0 |
| 2022-Bitwuzlan | 0 | 119 | 15684.679 | 15663.597 | 119 | 119 | 0 | 3 | 1212 | 80 | 0 |
| cvc5 | 0 | 98 | 18646.655 | 18725.382 | 98 | 98 | 0 | 24 | 1212 | 143 | 0 |
| UltimateEliminator+MathSAT | 0 | 2 | 12.68 | 8.928 | 2 | 2 | 0 | 120 | 1212 | 25 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2022-Bitwuzlan | 0 | 1135 | 14037.726 | 14033.289 | 1135 | 0 | 1135 | 13 | 186 | 80 | 0 |
| Bitwuzla | 0 | 1114 | 14151.579 | 14105.144 | 1114 | 0 | 1114 | 34 | 186 | 99 | 0 |
| Bitwuzla Fixedn | 0 | 1113 | 12932.388 | 12929.469 | 1113 | 0 | 1113 | 35 | 186 | 99 | 0 |
| cvc5 | 0 | 1070 | 25546.03 | 27373.16 | 1070 | 0 | 1070 | 78 | 186 | 143 | 0 |
| UltimateEliminator+MathSAT | 0 | 173 | 834.017 | 603.555 | 173 | 0 | 173 | 975 | 186 | 25 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2022-Bitwuzlan | 0 | 1116 | 976.31 | 946.698 | 1116 | 40 | 1076 | 218 | 218 | 0 |
| Bitwuzla | 0 | 1094 | 1053.029 | 1047.63 | 1094 | 34 | 1060 | 240 | 240 | 0 |
| Bitwuzla Fixedn | 0 | 1094 | 1053.881 | 1048.459 | 1094 | 34 | 1060 | 240 | 240 | 0 |
| cvc5 | 0 | 1029 | 1932.698 | 1922.721 | 1029 | 47 | 982 | 305 | 305 | 0 |
| UltimateEliminator+MathSAT | 0 | 174 | 841.935 | 508.532 | 174 | 2 | 172 | 1160 | 30 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.