The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the Equality+LinearArith division in the Parallel Track.
Page generated on 2021-07-18 17:32:11 +0000
Benchmarks: 113 Time Limit: 1200 seconds Memory Limit: N/A GB
Logics:
| Solver | Error Score | Correct Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Vampire | 0 | 26 | 108563.404 | 26 | 0 | 26 | 87 | 0 | 87 | 0 |
| Par4n | 0 | 4 | 49379.653 | 4 | 1 | 3 | 39 | 70 | 39 | 0 |
| cvc5-gg | 2 | 38 | 34880.014 | 38 | 0 | 38 | 75 | 0 | 29 | 0 |
| Solver | Error Score | Correct Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Par4n | 0 | 1 | 480.297 | 1 | 1 | 0 | 0 | 112 | 39 | 0 |
| cvc5-gg | 0 | 0 | 1200.0 | 0 | 0 | 0 | 3 | 110 | 29 | 0 |
| Vampire | 0 | 0 | 3600.0 | 0 | 0 | 0 | 3 | 110 | 87 | 0 |
| Solver | Error Score | Correct Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Vampire | 0 | 26 | 42563.404 | 26 | 0 | 26 | 32 | 55 | 87 | 0 |
| Par4n | 0 | 3 | 17699.356 | 3 | 0 | 3 | 13 | 97 | 39 | 0 |
| cvc5-gg | 2 | 38 | 3680.014 | 38 | 0 | 38 | 20 | 55 | 29 | 0 |
| Solver | Error Score | Correct Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Vampire | 0 | 9 | 2521.376 | 9 | 0 | 9 | 104 | 0 | 104 | 0 |
| Par4n | 0 | 0 | 1032.0 | 0 | 0 | 0 | 43 | 70 | 43 | 0 |
| cvc5-gg | 2 | 38 | 776.014 | 38 | 0 | 38 | 75 | 0 | 29 | 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.