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 2021-07-18 17:29:05 +0000
Benchmarks: 300 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| Yices2-QS | Yices2-QS | Yices2-QS | Yices2-QS | Yices2-QS |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Yices2-QS | 0 | 297 | 3875.305 | 3875.717 | 297 | 211 | 86 | 3 | 3 | 0 |
| z3n | 0 | 296 | 6073.724 | 6074.202 | 296 | 210 | 86 | 4 | 4 | 0 |
| 2020-z3n | 0 | 296 | 6074.081 | 6075.032 | 296 | 210 | 86 | 4 | 4 | 0 |
| 2019-Par4n | 0 | 289 | 13440.36 | 13330.679 | 289 | 209 | 80 | 11 | 11 | 0 |
| cvc5 - fixedn | 0 | 153 | 181438.04 | 186983.283 | 153 | 91 | 62 | 147 | 147 | 0 |
| cvc5 | 0 | 151 | 182321.691 | 188752.609 | 151 | 90 | 61 | 149 | 149 | 0 |
| 2020-CVC4n | 0 | 123 | 116193.658 | 116324.925 | 123 | 61 | 62 | 177 | 86 | 0 |
| Vampire | 0 | 81 | 263897.174 | 263188.456 | 81 | 0 | 81 | 219 | 219 | 0 |
| Vampire - fixedn | 0 | 79 | 265876.344 | 265459.278 | 79 | 0 | 79 | 221 | 221 | 0 |
| iProver | 0 | 50 | 300445.789 | 300138.67 | 50 | 0 | 50 | 250 | 250 | 0 |
| UltimateEliminator+MathSAT | 0 | 7 | 295488.95 | 295375.36 | 7 | 0 | 7 | 293 | 246 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Yices2-QS | 0 | 297 | 3875.555 | 3875.657 | 297 | 211 | 86 | 3 | 3 | 0 |
| z3n | 0 | 296 | 6073.904 | 6073.982 | 296 | 210 | 86 | 4 | 4 | 0 |
| 2020-z3n | 0 | 296 | 6074.661 | 6074.842 | 296 | 210 | 86 | 4 | 4 | 0 |
| 2019-Par4n | 0 | 290 | 14541.4 | 13281.279 | 290 | 209 | 81 | 10 | 10 | 0 |
| cvc5 - fixedn | 0 | 153 | 186959.011 | 186977.603 | 153 | 91 | 62 | 147 | 147 | 0 |
| cvc5 | 0 | 151 | 188726.307 | 188746.009 | 151 | 90 | 61 | 149 | 149 | 0 |
| 2020-CVC4n | 0 | 123 | 116356.808 | 116032.213 | 123 | 61 | 62 | 177 | 85 | 0 |
| Vampire | 0 | 85 | 266535.634 | 260341.322 | 85 | 0 | 85 | 215 | 215 | 0 |
| Vampire - fixedn | 0 | 79 | 267555.814 | 265013.999 | 79 | 0 | 79 | 221 | 220 | 0 |
| iProver | 0 | 51 | 303569.279 | 300027.12 | 51 | 0 | 51 | 249 | 249 | 0 |
| UltimateEliminator+MathSAT | 0 | 7 | 295488.95 | 295375.36 | 7 | 0 | 7 | 293 | 246 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Yices2-QS | 0 | 211 | 260.932 | 261.035 | 211 | 211 | 0 | 0 | 89 | 3 | 0 |
| z3n | 0 | 210 | 1209.78 | 1209.793 | 210 | 210 | 0 | 1 | 89 | 4 | 0 |
| 2020-z3n | 0 | 210 | 1212.896 | 1212.898 | 210 | 210 | 0 | 1 | 89 | 4 | 0 |
| 2019-Par4n | 0 | 209 | 2407.235 | 2410.392 | 209 | 209 | 0 | 2 | 89 | 10 | 0 |
| cvc5 - fixedn | 0 | 91 | 154194.361 | 154212.97 | 91 | 91 | 0 | 120 | 89 | 147 | 0 |
| cvc5 | 0 | 90 | 155101.248 | 155120.97 | 90 | 90 | 0 | 121 | 89 | 149 | 0 |
| 2020-CVC4n | 0 | 61 | 84645.354 | 84609.55 | 61 | 61 | 0 | 150 | 89 | 85 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 250809.792 | 250805.935 | 0 | 0 | 0 | 211 | 89 | 246 | 0 |
| iProver | 0 | 0 | 253200.0 | 253200.0 | 0 | 0 | 0 | 211 | 89 | 249 | 0 |
| Vampire | 0 | 0 | 253200.0 | 253200.0 | 0 | 0 | 0 | 211 | 89 | 215 | 0 |
| Vampire - fixedn | 0 | 0 | 253200.0 | 253200.0 | 0 | 0 | 0 | 211 | 89 | 220 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Yices2-QS | 0 | 86 | 2414.623 | 2414.622 | 86 | 0 | 86 | 2 | 212 | 3 | 0 |
| 2020-z3n | 0 | 86 | 3661.765 | 3661.944 | 86 | 0 | 86 | 2 | 212 | 4 | 0 |
| z3n | 0 | 86 | 3664.124 | 3664.189 | 86 | 0 | 86 | 2 | 212 | 4 | 0 |
| Vampire | 0 | 85 | 12135.634 | 5941.322 | 85 | 0 | 85 | 3 | 212 | 215 | 0 |
| 2019-Par4n | 0 | 81 | 10934.165 | 9670.887 | 81 | 0 | 81 | 7 | 212 | 10 | 0 |
| Vampire - fixedn | 0 | 79 | 13155.814 | 10613.999 | 79 | 0 | 79 | 9 | 212 | 220 | 0 |
| 2020-CVC4n | 0 | 62 | 30511.455 | 30222.663 | 62 | 0 | 62 | 26 | 212 | 85 | 0 |
| cvc5 - fixedn | 0 | 62 | 31564.65 | 31564.633 | 62 | 0 | 62 | 26 | 212 | 147 | 0 |
| cvc5 | 0 | 61 | 32425.06 | 32425.039 | 61 | 0 | 61 | 27 | 212 | 149 | 0 |
| iProver | 0 | 51 | 49169.279 | 45627.12 | 51 | 0 | 51 | 37 | 212 | 249 | 0 |
| UltimateEliminator+MathSAT | 0 | 7 | 43479.158 | 43369.425 | 7 | 0 | 7 | 81 | 212 | 246 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Yices2-QS | 0 | 296 | 129.412 | 129.432 | 296 | 210 | 86 | 4 | 4 | 0 |
| z3n | 0 | 294 | 160.492 | 160.561 | 294 | 210 | 84 | 6 | 6 | 0 |
| 2020-z3n | 0 | 294 | 164.557 | 164.563 | 294 | 210 | 84 | 6 | 6 | 0 |
| 2019-Par4n | 0 | 288 | 314.38 | 311.627 | 288 | 209 | 79 | 12 | 12 | 0 |
| cvc5 | 0 | 107 | 4876.66 | 4876.675 | 107 | 46 | 61 | 193 | 193 | 0 |
| cvc5 - fixedn | 0 | 107 | 4877.067 | 4877.082 | 107 | 46 | 61 | 193 | 193 | 0 |
| 2020-CVC4n | 0 | 100 | 5030.154 | 5030.148 | 100 | 41 | 59 | 200 | 200 | 0 |
| Vampire | 0 | 75 | 5408.484 | 5409.907 | 75 | 0 | 75 | 225 | 225 | 0 |
| Vampire - fixedn | 0 | 75 | 5410.821 | 5410.33 | 75 | 0 | 75 | 225 | 225 | 0 |
| iProver | 0 | 50 | 6445.789 | 6138.67 | 50 | 0 | 50 | 250 | 250 | 0 |
| UltimateEliminator+MathSAT | 0 | 7 | 6192.95 | 6079.36 | 7 | 0 | 7 | 293 | 246 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.