The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the AUFDTLIRA logic in the Single Query Track.
Page generated on 2023-07-06 16:04:53 +0000
Benchmarks: 4185 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 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2022-cvc5n | 0 | 3645 | 5680.771 | 5727.328 | 3645 | 0 | 3645 | 540 | 536 | 0 |
| cvc5 | 0 | 3644 | 4844.572 | 4929.386 | 3644 | 0 | 3644 | 541 | 537 | 0 |
| Vampire | 0 | 3342 | 547689.162 | 138202.16 | 3342 | 0 | 3342 | 843 | 843 | 0 |
| SMTInterpol | 0 | 2995 | 25616.737 | 16360.891 | 2995 | 0 | 2995 | 1190 | 1022 | 0 |
| iProver | 0 | 2902 | 158332.391 | 41389.933 | 2902 | 0 | 2902 | 1283 | 1283 | 0 |
| iProver Fixedn | 0 | 2890 | 153317.018 | 40217.262 | 2890 | 0 | 2890 | 1295 | 1295 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2022-cvc5n | 0 | 3645 | 5680.771 | 5727.328 | 3645 | 0 | 3645 | 540 | 536 | 0 |
| cvc5 | 0 | 3644 | 4844.572 | 4929.386 | 3644 | 0 | 3644 | 541 | 537 | 0 |
| Vampire | 0 | 3441 | 772581.222 | 193662.107 | 3441 | 0 | 3441 | 744 | 744 | 0 |
| SMTInterpol | 0 | 2995 | 25616.737 | 16360.891 | 2995 | 0 | 2995 | 1190 | 1020 | 0 |
| iProver | 0 | 2987 | 338649.391 | 86944.403 | 2987 | 0 | 2987 | 1198 | 1198 | 0 |
| iProver Fixedn | 0 | 2985 | 352647.368 | 90872.824 | 2985 | 0 | 2985 | 1200 | 1200 | 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 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 0 | 4185 | 536 | 0 |
| Vampire | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 0 | 4185 | 744 | 0 |
| cvc5 | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 0 | 4185 | 537 | 0 |
| SMTInterpol | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 0 | 4185 | 1020 | 0 |
| iProver | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 0 | 4185 | 1198 | 0 |
| iProver Fixedn | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 0 | 4185 | 1200 | 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 | 3645 | 5680.771 | 5727.328 | 3645 | 0 | 3645 | 17 | 523 | 536 | 0 |
| cvc5 | 0 | 3644 | 4844.572 | 4929.386 | 3644 | 0 | 3644 | 18 | 523 | 537 | 0 |
| Vampire | 0 | 3441 | 772581.222 | 193662.107 | 3441 | 0 | 3441 | 221 | 523 | 744 | 0 |
| SMTInterpol | 0 | 2995 | 25616.737 | 16360.891 | 2995 | 0 | 2995 | 667 | 523 | 1020 | 0 |
| iProver | 0 | 2987 | 338649.391 | 86944.403 | 2987 | 0 | 2987 | 675 | 523 | 1198 | 0 |
| iProver Fixedn | 0 | 2985 | 352647.368 | 90872.824 | 2985 | 0 | 2985 | 677 | 523 | 1200 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 3613 | 386.541 | 384.867 | 3613 | 0 | 3613 | 572 | 570 | 0 |
| 2022-cvc5n | 0 | 3613 | 735.105 | 728.678 | 3613 | 0 | 3613 | 572 | 570 | 0 |
| SMTInterpol | 0 | 2903 | 13730.876 | 6065.939 | 2903 | 0 | 2903 | 1282 | 1135 | 0 |
| iProver Fixedn | 0 | 2513 | 18189.388 | 5634.545 | 2513 | 0 | 2513 | 1672 | 1672 | 0 |
| iProver | 0 | 2511 | 17918.269 | 5529.624 | 2511 | 0 | 2511 | 1674 | 1674 | 0 |
| Vampire | 0 | 2199 | 11145.043 | 3010.477 | 2199 | 0 | 2199 | 1986 | 1986 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.