The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the UFIDL division in the Single Query Track.
Page generated on 2020-07-04 11:46:59 +0000
Benchmarks: 20 Time Limit: 1200 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 |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 12 | 10618.295 | 10132.642 | 12 | 3 | 9 | 8 | 8 | 0 | |
| z3n | 0 | 11 | 7791.232 | 7793.177 | 11 | 2 | 9 | 9 | 5 | 0 | |
| CVC4 | 0 | 10 | 10041.945 | 10171.032 | 10 | 1 | 9 | 10 | 8 | 0 | |
| SMTInterpol | 0 | 8 | 8554.856 | 8468.986 | 8 | 1 | 7 | 12 | 7 | 0 | |
| SMTInterpol-fixedn | 0 | 8 | 8559.177 | 8469.646 | 8 | 1 | 7 | 12 | 7 | 0 | |
| veriT+viten | 0 | 7 | 12055.816 | 12057.323 | 7 | 0 | 7 | 13 | 9 | 1 | |
| veriT | 0 | 7 | 15597.39 | 15600.858 | 7 | 0 | 7 | 13 | 12 | 1 | |
| Vampire | 0 | 7 | 15600.743 | 15600.738 | 7 | 0 | 7 | 13 | 13 | 0 | |
| UltimateEliminator+MathSAT | 0 | 0 | 7250.454 | 7233.584 | 0 | 0 | 0 | 20 | 6 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 12 | 10618.295 | 10132.642 | 12 | 3 | 9 | 8 | 8 | 0 | |
| z3n | 0 | 11 | 7792.372 | 7792.837 | 11 | 2 | 9 | 9 | 5 | 0 | |
| CVC4 | 0 | 10 | 10088.555 | 10170.802 | 10 | 1 | 9 | 10 | 8 | 0 | |
| SMTInterpol | 0 | 8 | 8554.856 | 8468.986 | 8 | 1 | 7 | 12 | 7 | 0 | |
| SMTInterpol-fixedn | 0 | 8 | 8559.177 | 8469.646 | 8 | 1 | 7 | 12 | 7 | 0 | |
| veriT+viten | 0 | 7 | 12056.836 | 12056.883 | 7 | 0 | 7 | 13 | 9 | 1 | |
| Vampire | 0 | 7 | 19200.963 | 15599.258 | 7 | 0 | 7 | 13 | 13 | 0 | |
| veriT | 0 | 7 | 15600.31 | 15600.308 | 7 | 0 | 7 | 13 | 12 | 1 | |
| UltimateEliminator+MathSAT | 0 | 0 | 7250.454 | 7233.584 | 0 | 0 | 0 | 20 | 6 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 3 | 1018.234 | 531.949 | 3 | 3 | 0 | 17 | 8 | 0 |
| z3n | 0 | 2 | 1200.099 | 1200.1 | 2 | 2 | 0 | 18 | 5 | 0 |
| CVC4 | 0 | 1 | 487.112 | 569.362 | 1 | 1 | 0 | 19 | 8 | 0 |
| SMTInterpol-fixedn | 0 | 1 | 1201.48 | 1200.874 | 1 | 1 | 0 | 19 | 7 | 0 |
| SMTInterpol | 0 | 1 | 1201.504 | 1200.917 | 1 | 1 | 0 | 19 | 7 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 10.236 | 6.96 | 0 | 0 | 0 | 20 | 6 | 0 |
| veriT+viten | 0 | 0 | 1200.021 | 1200.024 | 0 | 0 | 0 | 20 | 9 | 1 |
| veriT | 0 | 0 | 3600.0 | 3600.0 | 0 | 0 | 0 | 20 | 12 | 1 |
| Vampire | 0 | 0 | 3600.0 | 3600.0 | 0 | 0 | 0 | 20 | 13 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 9 | 0.061 | 0.692 | 9 | 0 | 9 | 11 | 8 | 0 |
| z3n | 0 | 9 | 0.828 | 0.83 | 9 | 0 | 9 | 11 | 5 | 0 |
| CVC4 | 0 | 9 | 1.443 | 1.441 | 9 | 0 | 9 | 11 | 8 | 0 |
| veriT | 0 | 7 | 2400.31 | 2400.308 | 7 | 0 | 7 | 13 | 12 | 1 |
| veriT+viten | 0 | 7 | 2400.307 | 2400.326 | 7 | 0 | 7 | 13 | 9 | 1 |
| Vampire | 0 | 7 | 2400.743 | 2400.738 | 7 | 0 | 7 | 13 | 13 | 0 |
| SMTInterpol | 0 | 7 | 2539.944 | 2463.015 | 7 | 0 | 7 | 13 | 7 | 0 |
| SMTInterpol-fixedn | 0 | 7 | 2544.103 | 2463.659 | 7 | 0 | 7 | 13 | 7 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 7211.383 | 7207.474 | 0 | 0 | 0 | 20 | 6 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 11 | 216.075 | 216.828 | 11 | 2 | 9 | 9 | 9 | 0 | |
| z3n | 0 | 11 | 216.928 | 216.93 | 11 | 2 | 9 | 9 | 9 | 0 | |
| CVC4 | 0 | 9 | 218.016 | 218.098 | 9 | 0 | 9 | 11 | 9 | 0 | |
| SMTInterpol | 0 | 8 | 322.856 | 236.986 | 8 | 1 | 7 | 12 | 7 | 0 | |
| SMTInterpol-fixedn | 0 | 8 | 327.177 | 237.646 | 8 | 1 | 7 | 12 | 7 | 0 | |
| veriT+viten | 0 | 7 | 264.328 | 264.349 | 7 | 0 | 7 | 13 | 10 | 1 | |
| veriT | 0 | 7 | 312.31 | 312.308 | 7 | 0 | 7 | 13 | 12 | 1 | |
| Vampire | 0 | 7 | 312.743 | 312.738 | 7 | 0 | 7 | 13 | 13 | 0 | |
| UltimateEliminator+MathSAT | 0 | 0 | 194.454 | 177.584 | 0 | 0 | 0 | 20 | 6 | 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.