The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the ABVFP logic in the Single Query Track.
Page generated on 2021-07-18 17:29:04 +0000
Benchmarks: 30 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 - fixedn | 0 | 17 | 15562.367 | 15605.13 | 17 | 15 | 2 | 13 | 13 | 0 |
| cvc5 | 0 | 17 | 15570.49 | 15604.857 | 17 | 15 | 2 | 13 | 13 | 0 |
| 2020-CVC4n | 0 | 15 | 12712.834 | 12714.902 | 15 | 13 | 2 | 15 | 10 | 0 |
| UltimateEliminator+MathSAT | 0 | 10 | 290.408 | 226.563 | 10 | 10 | 0 | 20 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 17 | 15604.31 | 15604.307 | 17 | 15 | 2 | 13 | 13 | 0 |
| cvc5 - fixedn | 0 | 17 | 15604.327 | 15604.32 | 17 | 15 | 2 | 13 | 13 | 0 |
| 2020-CVC4n | 0 | 15 | 12714.104 | 12714.442 | 15 | 13 | 2 | 15 | 10 | 0 |
| UltimateEliminator+MathSAT | 0 | 10 | 290.408 | 226.563 | 10 | 10 | 0 | 20 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 15 | 3.973 | 3.971 | 15 | 15 | 0 | 0 | 15 | 13 | 0 |
| cvc5 - fixedn | 0 | 15 | 4.0 | 3.994 | 15 | 15 | 0 | 0 | 15 | 13 | 0 |
| 2020-CVC4n | 0 | 13 | 3.662 | 3.658 | 13 | 13 | 0 | 2 | 15 | 10 | 0 |
| UltimateEliminator+MathSAT | 0 | 10 | 216.596 | 183.258 | 10 | 10 | 0 | 5 | 15 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 - fixedn | 0 | 2 | 0.327 | 0.326 | 2 | 0 | 2 | 0 | 28 | 13 | 0 |
| cvc5 | 0 | 2 | 0.337 | 0.336 | 2 | 0 | 2 | 0 | 28 | 13 | 0 |
| 2020-CVC4n | 0 | 2 | 0.373 | 0.375 | 2 | 0 | 2 | 0 | 28 | 10 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 9.711 | 5.593 | 0 | 0 | 0 | 2 | 28 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 17 | 316.31 | 316.307 | 17 | 15 | 2 | 13 | 13 | 0 |
| cvc5 - fixedn | 0 | 17 | 316.327 | 316.32 | 17 | 15 | 2 | 13 | 13 | 0 |
| 2020-CVC4n | 0 | 15 | 316.036 | 316.033 | 15 | 13 | 2 | 15 | 13 | 0 |
| UltimateEliminator+MathSAT | 0 | 8 | 229.686 | 171.499 | 8 | 8 | 0 | 22 | 2 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.