The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the LIA division in the Single Query Track.
Page generated on 2019-07-23 17:56:09 +0000
Benchmarks: 300 Time Limit: 2400 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| CVC4 | CVC4 | CVC4 | CVC4 | CVC4 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Z3n | 0 | 300 | 14.903 | 14.905 | 300 | 149 | 151 | 0 | 0 | 0 | |
| 2018-Z3n | 0 | 300 | 15.366 | 15.387 | 300 | 149 | 151 | 0 | 0 | 0 | |
| CVC4 | 0 | 300 | 37.661 | 37.562 | 300 | 149 | 151 | 0 | 0 | 0 | |
| Vampire | 0 | 139 | 388493.95 | 386943.821 | 139 | 3 | 136 | 161 | 161 | 0 | |
| SMTInterpol | 0 | 105 | 212145.383 | 211506.943 | 105 | 8 | 97 | 195 | 81 | 0 | |
| UltimateEliminator+SMTInterpol | 0 | 79 | 369450.547 | 368747.947 | 79 | 29 | 50 | 221 | 152 | 0 | |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 78 | 369012.387 | 368474.22 | 78 | 29 | 49 | 222 | 153 | 0 | |
| veriT | 0 | 69 | 6417.036 | 6407.376 | 69 | 0 | 69 | 231 | 1 | 0 | |
| ProB | 0 | 47 | 409637.564 | 420203.791 | 47 | 17 | 30 | 253 | 161 | 0 | |
| UltimateEliminator+Yices-2.6.1 | 0 | 41 | 203967.219 | 203312.917 | 41 | 10 | 31 | 259 | 82 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Z3n | 0 | 300 | 14.903 | 14.905 | 300 | 149 | 151 | 0 | 0 | 0 | |
| 2018-Z3n | 0 | 300 | 15.366 | 15.387 | 300 | 149 | 151 | 0 | 0 | 0 | |
| CVC4 | 0 | 300 | 37.661 | 37.562 | 300 | 149 | 151 | 0 | 0 | 0 | |
| Vampire | 0 | 140 | 400402.59 | 386287.461 | 140 | 3 | 137 | 160 | 160 | 0 | |
| SMTInterpol | 0 | 105 | 212145.383 | 211506.943 | 105 | 8 | 97 | 195 | 81 | 0 | |
| UltimateEliminator+SMTInterpol | 0 | 79 | 369450.547 | 368747.947 | 79 | 29 | 50 | 221 | 152 | 0 | |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 78 | 369012.387 | 368474.22 | 78 | 29 | 49 | 222 | 153 | 0 | |
| veriT | 0 | 69 | 6417.206 | 6407.286 | 69 | 0 | 69 | 231 | 1 | 0 | |
| ProB | 0 | 47 | 409662.554 | 420197.431 | 47 | 17 | 30 | 253 | 161 | 0 | |
| UltimateEliminator+Yices-2.6.1 | 0 | 41 | 203967.219 | 203312.917 | 41 | 10 | 31 | 259 | 82 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Z3n | 0 | 149 | 8.063 | 8.064 | 149 | 149 | 0 | 151 | 0 | 0 |
| 2018-Z3n | 0 | 149 | 8.368 | 8.377 | 149 | 149 | 0 | 151 | 0 | 0 |
| CVC4 | 0 | 149 | 30.741 | 30.694 | 149 | 149 | 0 | 151 | 0 | 0 |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 29 | 288510.339 | 288296.924 | 29 | 29 | 0 | 271 | 153 | 0 |
| UltimateEliminator+SMTInterpol | 0 | 29 | 289019.58 | 288731.871 | 29 | 29 | 0 | 271 | 152 | 0 |
| ProB | 0 | 17 | 278015.743 | 283350.275 | 17 | 17 | 0 | 283 | 161 | 0 |
| UltimateEliminator+Yices-2.6.1 | 0 | 10 | 176705.516 | 176254.399 | 10 | 10 | 0 | 290 | 82 | 0 |
| SMTInterpol | 0 | 8 | 172052.431 | 171676.009 | 8 | 8 | 0 | 292 | 81 | 0 |
| Vampire | 0 | 3 | 357600.684 | 350354.183 | 3 | 3 | 0 | 297 | 160 | 0 |
| veriT | 0 | 0 | 4716.419 | 4706.489 | 0 | 0 | 0 | 300 | 1 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Z3n | 0 | 151 | 6.841 | 6.841 | 151 | 0 | 151 | 149 | 0 | 0 |
| CVC4 | 0 | 151 | 6.919 | 6.869 | 151 | 0 | 151 | 149 | 0 | 0 |
| 2018-Z3n | 0 | 151 | 6.999 | 7.01 | 151 | 0 | 151 | 149 | 0 | 0 |
| Vampire | 0 | 137 | 42801.907 | 35933.278 | 137 | 0 | 137 | 163 | 160 | 0 |
| SMTInterpol | 0 | 97 | 40092.952 | 39830.934 | 97 | 0 | 97 | 203 | 81 | 0 |
| veriT | 0 | 69 | 1700.786 | 1700.796 | 69 | 0 | 69 | 231 | 1 | 0 |
| UltimateEliminator+SMTInterpol | 0 | 50 | 80430.968 | 80016.076 | 50 | 0 | 50 | 250 | 152 | 0 |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 49 | 80502.047 | 80177.296 | 49 | 0 | 49 | 251 | 153 | 0 |
| UltimateEliminator+Yices-2.6.1 | 0 | 31 | 27261.703 | 27058.517 | 31 | 0 | 31 | 269 | 82 | 0 |
| ProB | 0 | 30 | 131646.811 | 136847.156 | 30 | 0 | 30 | 270 | 161 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Z3n | 0 | 300 | 14.903 | 14.905 | 300 | 149 | 151 | 0 | 0 | 0 | |
| 2018-Z3n | 0 | 300 | 15.366 | 15.387 | 300 | 149 | 151 | 0 | 0 | 0 | |
| CVC4 | 0 | 300 | 37.661 | 37.562 | 300 | 149 | 151 | 0 | 0 | 0 | |
| Vampire | 0 | 137 | 4331.2 | 4034.03 | 137 | 3 | 134 | 163 | 163 | 0 | |
| SMTInterpol | 0 | 105 | 3494.334 | 3245.851 | 105 | 8 | 97 | 195 | 120 | 0 | |
| veriT | 0 | 69 | 1052.108 | 1041.945 | 69 | 0 | 69 | 231 | 7 | 0 | |
| UltimateEliminator+SMTInterpol | 0 | 69 | 4492.431 | 4222.22 | 69 | 24 | 45 | 231 | 162 | 0 | |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 69 | 4504.356 | 4262.009 | 69 | 24 | 45 | 231 | 162 | 0 | |
| ProB | 0 | 46 | 4870.59 | 4874.276 | 46 | 16 | 30 | 254 | 195 | 0 | |
| UltimateEliminator+Yices-2.6.1 | 0 | 41 | 3211.013 | 2807.84 | 41 | 10 | 31 | 259 | 93 | 0 |
n Non-competing.
Abstained: Total of benchmarks in logics in this division that solver chose to abstain from. For SAT/UNSAT scores, this column also includes benchmarks not known to be SAT/UNSAT.