The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the NRA logic in the Single Query Track.
Page generated on 2023-07-06 16:04:54 +0000
Benchmarks: 99 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| YicesQS | YicesQS | YicesQS | YicesQS | YicesQS |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| YicesQS | 0 | 92 | 914.146 | 914.223 | 92 | 4 | 88 | 7 | 7 | 0 |
| 2021-z3n | 0 | 91 | 583.03 | 583.033 | 91 | 3 | 88 | 8 | 6 | 0 |
| cvc5 | 0 | 88 | 1826.604 | 1831.985 | 88 | 4 | 84 | 11 | 11 | 0 |
| Vampire | 0 | 83 | 121.625 | 38.885 | 83 | 0 | 83 | 16 | 16 | 0 |
| iProver | 0 | 75 | 4055.705 | 1056.323 | 75 | 0 | 75 | 24 | 24 | 0 |
| iProver Fixedn | 0 | 72 | 1536.044 | 462.629 | 72 | 0 | 72 | 27 | 27 | 0 |
| UltimateEliminator+MathSAT | 0 | 8 | 47.582 | 29.6 | 8 | 1 | 7 | 91 | 35 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| YicesQS | 0 | 92 | 914.146 | 914.223 | 92 | 4 | 88 | 7 | 7 | 0 |
| 2021-z3n | 0 | 91 | 583.03 | 583.033 | 91 | 3 | 88 | 8 | 6 | 0 |
| cvc5 | 0 | 88 | 1826.604 | 1831.985 | 88 | 4 | 84 | 11 | 11 | 0 |
| Vampire | 0 | 83 | 121.625 | 38.885 | 83 | 0 | 83 | 16 | 16 | 0 |
| iProver | 0 | 76 | 7737.925 | 1986.057 | 76 | 0 | 76 | 23 | 23 | 0 |
| iProver Fixedn | 0 | 74 | 6564.794 | 1735.419 | 74 | 0 | 74 | 25 | 25 | 0 |
| UltimateEliminator+MathSAT | 0 | 8 | 47.582 | 29.6 | 8 | 1 | 7 | 91 | 35 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| YicesQS | 0 | 4 | 0.627 | 0.626 | 4 | 4 | 0 | 1 | 94 | 7 | 0 |
| cvc5 | 0 | 4 | 302.604 | 302.648 | 4 | 4 | 0 | 1 | 94 | 11 | 0 |
| 2021-z3n | 0 | 3 | 0.078 | 0.079 | 3 | 3 | 0 | 2 | 94 | 6 | 0 |
| UltimateEliminator+MathSAT | 0 | 1 | 4.721 | 2.745 | 1 | 1 | 0 | 4 | 94 | 35 | 0 |
| Vampire | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 5 | 94 | 16 | 0 |
| iProver | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 5 | 94 | 23 | 0 |
| iProver Fixedn | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 5 | 94 | 25 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2021-z3n | 0 | 88 | 582.951 | 582.954 | 88 | 0 | 88 | 5 | 6 | 6 | 0 |
| YicesQS | 0 | 88 | 913.519 | 913.596 | 88 | 0 | 88 | 5 | 6 | 7 | 0 |
| cvc5 | 0 | 84 | 1523.999 | 1529.337 | 84 | 0 | 84 | 9 | 6 | 11 | 0 |
| Vampire | 0 | 83 | 121.625 | 38.885 | 83 | 0 | 83 | 10 | 6 | 16 | 0 |
| iProver | 0 | 76 | 7737.925 | 1986.057 | 76 | 0 | 76 | 17 | 6 | 23 | 0 |
| iProver Fixedn | 0 | 74 | 6564.794 | 1735.419 | 74 | 0 | 74 | 19 | 6 | 25 | 0 |
| UltimateEliminator+MathSAT | 0 | 7 | 42.861 | 26.855 | 7 | 0 | 7 | 86 | 6 | 35 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| YicesQS | 0 | 90 | 21.367 | 21.37 | 90 | 4 | 86 | 9 | 9 | 0 |
| 2021-z3n | 0 | 89 | 1.932 | 1.94 | 89 | 3 | 86 | 10 | 10 | 0 |
| cvc5 | 0 | 83 | 8.15 | 8.11 | 83 | 3 | 80 | 16 | 16 | 0 |
| Vampire | 0 | 83 | 121.625 | 38.885 | 83 | 0 | 83 | 16 | 16 | 0 |
| iProver | 0 | 69 | 256.904 | 89.034 | 69 | 0 | 69 | 30 | 30 | 0 |
| iProver Fixedn | 0 | 69 | 277.826 | 94.127 | 69 | 0 | 69 | 30 | 30 | 0 |
| UltimateEliminator+MathSAT | 0 | 8 | 47.582 | 29.6 | 8 | 1 | 7 | 91 | 36 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.