The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_AUFNIA logic in the Single Query Track.
Page generated on 2021-07-18 17:29:06 +0000
Benchmarks: 9 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 |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-MathSAT-defaultn | 0 | 9 | 3.687 | 3.69 | 9 | 2 | 7 | 0 | 0 | 0 |
| MathSAT5n | 0 | 9 | 6.612 | 6.618 | 9 | 2 | 7 | 0 | 0 | 0 |
| 2020-CVC4n | 0 | 9 | 20.623 | 20.624 | 9 | 2 | 7 | 0 | 0 | 0 |
| z3n | 0 | 9 | 37.902 | 37.906 | 9 | 2 | 7 | 0 | 0 | 0 |
| cvc5 | 0 | 9 | 66.342 | 66.352 | 9 | 2 | 7 | 0 | 0 | 0 |
| cvc5 - fixedn | 0 | 9 | 71.887 | 65.797 | 9 | 2 | 7 | 0 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-MathSAT-defaultn | 0 | 9 | 3.687 | 3.69 | 9 | 2 | 7 | 0 | 0 | 0 |
| MathSAT5n | 0 | 9 | 6.612 | 6.618 | 9 | 2 | 7 | 0 | 0 | 0 |
| 2020-CVC4n | 0 | 9 | 20.623 | 20.624 | 9 | 2 | 7 | 0 | 0 | 0 |
| z3n | 0 | 9 | 37.902 | 37.906 | 9 | 2 | 7 | 0 | 0 | 0 |
| cvc5 - fixedn | 0 | 9 | 71.887 | 65.797 | 9 | 2 | 7 | 0 | 0 | 0 |
| cvc5 | 0 | 9 | 66.342 | 66.352 | 9 | 2 | 7 | 0 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-MathSAT-defaultn | 0 | 2 | 0.441 | 0.442 | 2 | 2 | 0 | 0 | 7 | 0 | 0 |
| MathSAT5n | 0 | 2 | 0.528 | 0.531 | 2 | 2 | 0 | 0 | 7 | 0 | 0 |
| 2020-CVC4n | 0 | 2 | 2.513 | 2.512 | 2 | 2 | 0 | 0 | 7 | 0 | 0 |
| cvc5 - fixedn | 0 | 2 | 15.052 | 8.956 | 2 | 2 | 0 | 0 | 7 | 0 | 0 |
| cvc5 | 0 | 2 | 8.963 | 8.967 | 2 | 2 | 0 | 0 | 7 | 0 | 0 |
| z3n | 0 | 2 | 36.84 | 36.844 | 2 | 2 | 0 | 0 | 7 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| z3n | 0 | 7 | 1.062 | 1.063 | 7 | 0 | 7 | 0 | 2 | 0 | 0 |
| 2019-MathSAT-defaultn | 0 | 7 | 3.246 | 3.249 | 7 | 0 | 7 | 0 | 2 | 0 | 0 |
| MathSAT5n | 0 | 7 | 6.084 | 6.087 | 7 | 0 | 7 | 0 | 2 | 0 | 0 |
| 2020-CVC4n | 0 | 7 | 18.11 | 18.112 | 7 | 0 | 7 | 0 | 2 | 0 | 0 |
| cvc5 - fixedn | 0 | 7 | 56.835 | 56.841 | 7 | 0 | 7 | 0 | 2 | 0 | 0 |
| cvc5 | 0 | 7 | 57.379 | 57.385 | 7 | 0 | 7 | 0 | 2 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-MathSAT-defaultn | 0 | 9 | 3.687 | 3.69 | 9 | 2 | 7 | 0 | 0 | 0 |
| MathSAT5n | 0 | 9 | 6.612 | 6.618 | 9 | 2 | 7 | 0 | 0 | 0 |
| 2020-CVC4n | 0 | 9 | 20.623 | 20.624 | 9 | 2 | 7 | 0 | 0 | 0 |
| z3n | 0 | 8 | 26.797 | 26.797 | 8 | 1 | 7 | 1 | 1 | 0 |
| cvc5 - fixedn | 0 | 8 | 71.201 | 65.107 | 8 | 2 | 6 | 1 | 1 | 0 |
| cvc5 | 0 | 8 | 65.44 | 65.449 | 8 | 2 | 6 | 1 | 1 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.