The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the Equality division in the Parallel Track.
Page generated on 2023-07-06 16:06:21 +0000
Benchmarks: 109 Time Limit: 1200 seconds Memory Limit: N/A GB
Logics: This track is experimental. Solvers are only ranked by performance, but no winner is selected.
| Solver | Error Score | Correct Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| iProver | 0 | 6 | 390.658 | 6 | 1 | 5 | 103 | 0 | 0 | 0 |
| Vampire | 3 | 44 | 4458.135 | 44 | 20 | 24 | 65 | 0 | 0 | 0 |
| Solver | Error Score | Correct Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Vampire | 0 | 20 | 1924.343 | 20 | 20 | 0 | 5 | 84 | 0 | 0 |
| iProver | 0 | 1 | 194.444 | 1 | 1 | 0 | 24 | 84 | 0 | 0 |
| Solver | Error Score | Correct Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| iProver | 0 | 5 | 196.214 | 5 | 0 | 5 | 20 | 84 | 0 | 0 |
| Vampire | 3 | 24 | 2533.792 | 24 | 0 | 24 | 1 | 84 | 0 | 0 |
| Solver | Error Score | Correct Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| iProver | 0 | 1 | 11.183 | 1 | 0 | 1 | 108 | 0 | 108 | 0 |
| Vampire | 2 | 14 | 78.763 | 14 | 3 | 11 | 95 | 0 | 93 | 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.