The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the UFLRA division in the Single Query Track.
Page generated on 2019-07-23 17:56:09 +0000
Benchmarks: 7 Time Limit: 2400 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| Alt-Ergo | Alt-Ergo | — | veriT | Alt-Ergo |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2018-Z3n | 0 | 5 | 4901.023 | 4901.347 | 5 | 3 | 2 | 2 | 2 | 0 | |
| Z3n | 0 | 4 | 7207.683 | 7208.314 | 4 | 2 | 2 | 3 | 3 | 0 | |
| Alt-Ergo | 0 | 2 | 5614.731 | 5132.964 | 2 | 0 | 2 | 5 | 2 | 0 | |
| veriT | 0 | 2 | 9613.46 | 9615.16 | 2 | 0 | 2 | 5 | 4 | 0 | |
| Vampire | 0 | 2 | 11098.071 | 10004.205 | 2 | 0 | 2 | 5 | 4 | 0 | |
| CVC4 | 0 | 2 | 11709.135 | 11710.704 | 2 | 0 | 2 | 5 | 4 | 0 | |
| SMTInterpol | 0 | 1 | 12000.773 | 12000.59 | 1 | 0 | 1 | 6 | 5 | 0 | |
| UltimateEliminator+Yices-2.6.1 | 0 | 0 | 22.998 | 15.732 | 0 | 0 | 0 | 7 | 0 | 0 | |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 0 | 23.258 | 16.846 | 0 | 0 | 0 | 7 | 0 | 0 | |
| UltimateEliminator+SMTInterpol | 0 | 0 | 23.294 | 14.932 | 0 | 0 | 0 | 7 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2018-Z3n | 0 | 5 | 4901.213 | 4901.237 | 5 | 3 | 2 | 2 | 2 | 0 | |
| Z3n | 0 | 4 | 7208.243 | 7208.244 | 4 | 2 | 2 | 3 | 3 | 0 | |
| Alt-Ergo | 0 | 2 | 5614.731 | 5132.964 | 2 | 0 | 2 | 5 | 2 | 0 | |
| veriT | 0 | 2 | 9615.08 | 9615.07 | 2 | 0 | 2 | 5 | 4 | 0 | |
| Vampire | 0 | 2 | 11098.071 | 10004.205 | 2 | 0 | 2 | 5 | 4 | 0 | |
| CVC4 | 0 | 2 | 11710.245 | 11710.464 | 2 | 0 | 2 | 5 | 4 | 0 | |
| SMTInterpol | 0 | 1 | 12000.773 | 12000.59 | 1 | 0 | 1 | 6 | 5 | 0 | |
| UltimateEliminator+SMTInterpol | 0 | 0 | 23.294 | 14.932 | 0 | 0 | 0 | 7 | 0 | 0 | |
| UltimateEliminator+Yices-2.6.1 | 0 | 0 | 22.998 | 15.732 | 0 | 0 | 0 | 7 | 0 | 0 | |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 0 | 23.258 | 16.846 | 0 | 0 | 0 | 7 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2018-Z3n | 0 | 3 | 4901.141 | 4901.166 | 3 | 3 | 0 | 4 | 2 | 0 |
| Z3n | 0 | 2 | 7208.171 | 7208.171 | 2 | 2 | 0 | 5 | 3 | 0 |
| UltimateEliminator+SMTInterpol | 0 | 0 | 16.618 | 10.62 | 0 | 0 | 0 | 7 | 0 | 0 |
| UltimateEliminator+Yices-2.6.1 | 0 | 0 | 16.464 | 11.341 | 0 | 0 | 0 | 7 | 0 | 0 |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 0 | 16.541 | 11.521 | 0 | 0 | 0 | 7 | 0 | 0 |
| Alt-Ergo | 0 | 0 | 5614.679 | 5132.913 | 0 | 0 | 0 | 7 | 2 | 0 |
| SMTInterpol | 0 | 0 | 9600.403 | 9600.307 | 0 | 0 | 0 | 7 | 5 | 0 |
| veriT | 0 | 0 | 9615.054 | 9615.045 | 0 | 0 | 0 | 7 | 4 | 0 |
| Vampire | 0 | 0 | 11097.53 | 10003.827 | 0 | 0 | 0 | 7 | 4 | 0 |
| CVC4 | 0 | 0 | 11710.21 | 11710.43 | 0 | 0 | 0 | 7 | 4 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| veriT | 0 | 2 | 0.025 | 0.025 | 2 | 0 | 2 | 5 | 4 | 0 |
| CVC4 | 0 | 2 | 0.035 | 0.034 | 2 | 0 | 2 | 5 | 4 | 0 |
| Alt-Ergo | 0 | 2 | 0.052 | 0.051 | 2 | 0 | 2 | 5 | 2 | 0 |
| 2018-Z3n | 0 | 2 | 0.072 | 0.072 | 2 | 0 | 2 | 5 | 2 | 0 |
| Z3n | 0 | 2 | 0.073 | 0.073 | 2 | 0 | 2 | 5 | 3 | 0 |
| Vampire | 0 | 2 | 0.541 | 0.378 | 2 | 0 | 2 | 5 | 4 | 0 |
| SMTInterpol | 0 | 1 | 2400.37 | 2400.282 | 1 | 0 | 1 | 6 | 5 | 0 |
| UltimateEliminator+SMTInterpol | 0 | 0 | 6.676 | 4.311 | 0 | 0 | 0 | 7 | 0 | 0 |
| UltimateEliminator+Yices-2.6.1 | 0 | 0 | 6.535 | 4.391 | 0 | 0 | 0 | 7 | 0 | 0 |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 0 | 6.717 | 5.326 | 0 | 0 | 0 | 7 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Z3n | 0 | 4 | 80.243 | 80.244 | 4 | 2 | 2 | 3 | 3 | 0 | |
| 2018-Z3n | 0 | 4 | 98.807 | 98.808 | 4 | 2 | 2 | 3 | 3 | 0 | |
| Alt-Ergo | 0 | 2 | 96.207 | 96.107 | 2 | 0 | 2 | 5 | 4 | 0 | |
| veriT | 0 | 2 | 111.08 | 111.07 | 2 | 0 | 2 | 5 | 4 | 0 | |
| CVC4 | 0 | 2 | 120.035 | 120.034 | 2 | 0 | 2 | 5 | 5 | 0 | |
| Vampire | 0 | 2 | 120.541 | 120.378 | 2 | 0 | 2 | 5 | 5 | 0 | |
| SMTInterpol | 0 | 1 | 120.773 | 120.59 | 1 | 0 | 1 | 6 | 5 | 0 | |
| UltimateEliminator+SMTInterpol | 0 | 0 | 23.294 | 14.932 | 0 | 0 | 0 | 7 | 0 | 0 | |
| UltimateEliminator+Yices-2.6.1 | 0 | 0 | 22.998 | 15.732 | 0 | 0 | 0 | 7 | 0 | 0 | |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 0 | 23.258 | 16.846 | 0 | 0 | 0 | 7 | 0 | 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.