The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the UFDTLIRA logic in the Single Query Track.
Page generated on 2023-07-06 16:04:54 +0000
Benchmarks: 3129 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| cvc5 | cvc5 | cvc5 | cvc5 | cvc5 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 2691 | 1040.707 | 1272.733 | 2691 | 531 | 2160 | 438 | 185 | 0 |
| 2022-cvc5n | 0 | 2691 | 2101.25 | 2159.515 | 2691 | 531 | 2160 | 438 | 185 | 0 |
| SMTInterpol | 0 | 2574 | 11986.638 | 7880.515 | 2574 | 479 | 2095 | 555 | 125 | 0 |
| Vampire | 0 | 2125 | 86542.34 | 21988.023 | 2125 | 12 | 2113 | 1004 | 1004 | 0 |
| iProver Fixedn | 0 | 1969 | 43500.096 | 11816.353 | 1969 | 0 | 1969 | 1160 | 1160 | 0 |
| iProver | 0 | 1966 | 43535.112 | 11774.843 | 1966 | 0 | 1966 | 1163 | 1163 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 2691 | 1040.707 | 1272.733 | 2691 | 531 | 2160 | 438 | 185 | 0 |
| 2022-cvc5n | 0 | 2691 | 2101.25 | 2159.515 | 2691 | 531 | 2160 | 438 | 185 | 0 |
| SMTInterpol | 0 | 2574 | 11986.638 | 7880.515 | 2574 | 479 | 2095 | 555 | 122 | 0 |
| iProver Fixedn | 0 | 2001 | 103253.426 | 26960.276 | 2001 | 0 | 2001 | 1128 | 1128 | 0 |
| iProver | 0 | 2000 | 106576.202 | 27725.355 | 2000 | 0 | 2000 | 1129 | 1129 | 0 |
| Vampire | 17 | 2144 | 145768.57 | 36901.122 | 2144 | 12 | 2132 | 985 | 968 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2022-cvc5n | 0 | 531 | 1043.142 | 1076.65 | 531 | 531 | 0 | 12 | 2586 | 185 | 0 |
| cvc5 | 0 | 531 | 848.728 | 1078.235 | 531 | 531 | 0 | 12 | 2586 | 185 | 0 |
| SMTInterpol | 0 | 479 | 408.205 | 280.68 | 479 | 479 | 0 | 64 | 2586 | 122 | 0 |
| Vampire | 0 | 12 | 2029.855 | 512.418 | 12 | 12 | 0 | 531 | 2586 | 968 | 0 |
| iProver | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 543 | 2586 | 1129 | 0 |
| iProver Fixedn | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 543 | 2586 | 1128 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 2160 | 191.979 | 194.499 | 2160 | 0 | 2160 | 8 | 961 | 185 | 0 |
| 2022-cvc5n | 0 | 2160 | 1058.109 | 1082.866 | 2160 | 0 | 2160 | 8 | 961 | 185 | 0 |
| SMTInterpol | 0 | 2095 | 11578.432 | 7599.836 | 2095 | 0 | 2095 | 73 | 961 | 122 | 0 |
| iProver Fixedn | 0 | 2001 | 103253.426 | 26960.276 | 2001 | 0 | 2001 | 167 | 961 | 1128 | 0 |
| iProver | 0 | 2000 | 106576.202 | 27725.355 | 2000 | 0 | 2000 | 168 | 961 | 1129 | 0 |
| Vampire | 17 | 2132 | 143738.715 | 36388.705 | 2132 | 0 | 2132 | 36 | 961 | 968 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2022-cvc5n | 0 | 2681 | 482.692 | 511.961 | 2681 | 526 | 2155 | 448 | 253 | 0 |
| cvc5 | 0 | 2679 | 302.827 | 309.192 | 2679 | 521 | 2158 | 450 | 253 | 0 |
| SMTInterpol | 0 | 2540 | 5942.165 | 2698.054 | 2540 | 479 | 2061 | 589 | 160 | 0 |
| iProver Fixedn | 0 | 1861 | 6886.519 | 2455.82 | 1861 | 0 | 1861 | 1268 | 1268 | 0 |
| iProver | 0 | 1858 | 7085.613 | 2486.532 | 1858 | 0 | 1858 | 1271 | 1271 | 0 |
| Vampire | 0 | 1809 | 4270.118 | 1238.945 | 1809 | 0 | 1809 | 1320 | 1320 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.