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 2022-08-10 11:17:44 +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 |
|---|---|---|---|---|---|---|---|---|---|---|
| 2021-z3n | 0 | 94 | 5004.068 | 5005.058 | 94 | 3 | 91 | 5 | 3 | 0 |
| YicesQS | 0 | 94 | 6163.958 | 6165.028 | 94 | 4 | 90 | 5 | 5 | 0 |
| z3-4.8.17n | 0 | 90 | 9670.412 | 9671.64 | 90 | 3 | 87 | 9 | 7 | 0 |
| cvc5 | 0 | 86 | 16247.706 | 16272.395 | 86 | 3 | 83 | 13 | 13 | 0 |
| Vampire | 0 | 83 | 19272.672 | 19228.219 | 83 | 0 | 83 | 16 | 16 | 0 |
| UltimateEliminator+MathSAT | 0 | 6 | 39958.845 | 39814.111 | 6 | 1 | 5 | 93 | 33 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2021-z3n | 0 | 94 | 5004.398 | 5004.798 | 94 | 3 | 91 | 5 | 3 | 0 |
| YicesQS | 0 | 94 | 6164.748 | 6164.768 | 94 | 4 | 90 | 5 | 5 | 0 |
| z3-4.8.17n | 0 | 90 | 9671.352 | 9671.34 | 90 | 3 | 87 | 9 | 7 | 0 |
| cvc5 | 0 | 86 | 16271.626 | 16271.875 | 86 | 3 | 83 | 13 | 13 | 0 |
| Vampire | 0 | 83 | 22872.792 | 19224.239 | 83 | 0 | 83 | 16 | 16 | 0 |
| UltimateEliminator+MathSAT | 0 | 6 | 39958.845 | 39814.111 | 6 | 1 | 5 | 93 | 33 | 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 | 1200.939 | 1200.939 | 4 | 4 | 0 | 1 | 94 | 5 | 0 |
| z3-4.8.17n | 0 | 3 | 1646.64 | 1646.67 | 3 | 3 | 0 | 2 | 94 | 7 | 0 |
| 2021-z3n | 0 | 3 | 1745.904 | 1745.972 | 3 | 3 | 0 | 2 | 94 | 3 | 0 |
| cvc5 | 0 | 3 | 2701.413 | 2701.656 | 3 | 3 | 0 | 2 | 94 | 13 | 0 |
| UltimateEliminator+MathSAT | 0 | 1 | 40.239 | 24.324 | 1 | 1 | 0 | 4 | 94 | 33 | 0 |
| Vampire | 0 | 0 | 6000.0 | 6000.0 | 0 | 0 | 0 | 5 | 94 | 16 | 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 | 91 | 2058.493 | 2058.827 | 91 | 0 | 91 | 2 | 6 | 3 | 0 |
| YicesQS | 0 | 90 | 3763.81 | 3763.829 | 90 | 0 | 90 | 3 | 6 | 5 | 0 |
| z3-4.8.17n | 0 | 87 | 6824.712 | 6824.67 | 87 | 0 | 87 | 6 | 6 | 7 | 0 |
| Vampire | 0 | 83 | 15672.792 | 12024.239 | 83 | 0 | 83 | 10 | 6 | 16 | 0 |
| cvc5 | 0 | 83 | 12370.213 | 12370.219 | 83 | 0 | 83 | 10 | 6 | 13 | 0 |
| UltimateEliminator+MathSAT | 0 | 5 | 39913.887 | 39787.0 | 5 | 0 | 5 | 88 | 6 | 33 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2021-z3n | 0 | 93 | 167.55 | 167.585 | 93 | 3 | 90 | 6 | 6 | 0 |
| YicesQS | 0 | 92 | 181.412 | 181.416 | 92 | 4 | 88 | 7 | 7 | 0 |
| z3-4.8.17n | 0 | 89 | 242.316 | 242.155 | 89 | 3 | 86 | 10 | 10 | 0 |
| cvc5 | 0 | 84 | 371.377 | 371.349 | 84 | 2 | 82 | 15 | 15 | 0 |
| Vampire | 0 | 83 | 456.672 | 412.219 | 83 | 0 | 83 | 16 | 16 | 0 |
| UltimateEliminator+MathSAT | 0 | 6 | 1150.845 | 1006.111 | 6 | 1 | 5 | 93 | 33 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.