The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the UFIDL logic in the Single Query Track.
Page generated on 2021-07-18 17:29:07 +0000
Benchmarks: 20 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| cvc5 | cvc5 | cvc5 | cvc5 | cvc5 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 12 | 10663.315 | 10147.1 | 12 | 3 | 9 | 8 | 8 | 0 |
| z3n | 0 | 11 | 7374.316 | 7375.669 | 11 | 2 | 9 | 9 | 5 | 0 |
| 2020-z3n | 0 | 11 | 7462.827 | 7464.105 | 11 | 2 | 9 | 9 | 5 | 0 |
| cvc5 | 0 | 10 | 5005.132 | 10187.143 | 10 | 1 | 9 | 10 | 8 | 0 |
| cvc5 - fixedn | 0 | 10 | 9146.054 | 10170.878 | 10 | 1 | 9 | 10 | 8 | 0 |
| 2020-CVC4n | 0 | 10 | 10050.65 | 10149.306 | 10 | 1 | 9 | 10 | 8 | 0 |
| SMTInterpol | 0 | 8 | 8552.179 | 8465.001 | 8 | 1 | 7 | 12 | 7 | 0 |
| veriT | 0 | 7 | 12297.516 | 12299.384 | 7 | 0 | 7 | 13 | 10 | 0 |
| iProver | 0 | 7 | 13285.502 | 13224.902 | 7 | 0 | 7 | 13 | 11 | 0 |
| Vampire | 0 | 7 | 14430.785 | 15601.585 | 7 | 0 | 7 | 13 | 13 | 0 |
| 2020-Vampiren | 0 | 7 | 15600.836 | 15600.831 | 7 | 0 | 7 | 13 | 13 | 0 |
| Vampire - fixedn | 0 | 6 | 15601.631 | 15601.624 | 6 | 0 | 6 | 14 | 13 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 1248.963 | 948.875 | 0 | 0 | 0 | 20 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 12 | 10663.315 | 10147.1 | 12 | 3 | 9 | 8 | 8 | 0 |
| z3n | 0 | 11 | 7375.116 | 7375.359 | 11 | 2 | 9 | 9 | 5 | 0 |
| 2020-z3n | 0 | 11 | 7463.667 | 7463.835 | 11 | 2 | 9 | 9 | 5 | 0 |
| 2020-CVC4n | 0 | 10 | 10088.9 | 10148.916 | 10 | 1 | 9 | 10 | 8 | 0 |
| cvc5 - fixedn | 0 | 10 | 10119.261 | 10170.518 | 10 | 1 | 9 | 10 | 8 | 0 |
| cvc5 | 0 | 10 | 10119.529 | 10186.783 | 10 | 1 | 9 | 10 | 8 | 0 |
| SMTInterpol | 0 | 8 | 8552.179 | 8465.001 | 8 | 1 | 7 | 12 | 7 | 0 |
| veriT | 0 | 7 | 12299.046 | 12299.064 | 7 | 0 | 7 | 13 | 10 | 0 |
| iProver | 0 | 7 | 13285.502 | 13224.902 | 7 | 0 | 7 | 13 | 11 | 0 |
| 2020-Vampiren | 0 | 7 | 15600.836 | 15600.831 | 7 | 0 | 7 | 13 | 13 | 0 |
| Vampire | 0 | 7 | 15601.545 | 15601.545 | 7 | 0 | 7 | 13 | 13 | 0 |
| Vampire - fixedn | 0 | 6 | 15601.631 | 15601.624 | 6 | 0 | 6 | 14 | 13 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 1248.963 | 948.875 | 0 | 0 | 0 | 20 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 3 | 1063.253 | 546.406 | 3 | 3 | 0 | 0 | 17 | 8 | 0 |
| z3n | 0 | 2 | 1200.069 | 1200.069 | 2 | 2 | 0 | 1 | 17 | 5 | 0 |
| 2020-z3n | 0 | 2 | 1200.103 | 1200.103 | 2 | 2 | 0 | 1 | 17 | 5 | 0 |
| 2020-CVC4n | 0 | 1 | 487.355 | 547.373 | 1 | 1 | 0 | 2 | 17 | 8 | 0 |
| cvc5 - fixedn | 0 | 1 | 517.949 | 569.211 | 1 | 1 | 0 | 2 | 17 | 8 | 0 |
| cvc5 | 0 | 1 | 518.24 | 585.499 | 1 | 1 | 0 | 2 | 17 | 8 | 0 |
| SMTInterpol | 0 | 1 | 1201.469 | 1200.913 | 1 | 1 | 0 | 2 | 17 | 7 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 14.354 | 8.616 | 0 | 0 | 0 | 3 | 17 | 0 | 0 |
| veriT | 0 | 0 | 1200.033 | 1200.038 | 0 | 0 | 0 | 3 | 17 | 10 | 0 |
| iProver | 0 | 0 | 1201.058 | 1201.527 | 0 | 0 | 0 | 3 | 17 | 11 | 0 |
| 2020-Vampiren | 0 | 0 | 3600.0 | 3600.0 | 0 | 0 | 0 | 3 | 17 | 13 | 0 |
| Vampire | 0 | 0 | 3600.0 | 3600.0 | 0 | 0 | 0 | 3 | 17 | 13 | 0 |
| Vampire - fixedn | 0 | 0 | 3600.0 | 3600.0 | 0 | 0 | 0 | 3 | 17 | 13 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 9 | 0.062 | 0.694 | 9 | 0 | 9 | 0 | 11 | 8 | 0 |
| z3n | 0 | 9 | 0.812 | 0.813 | 9 | 0 | 9 | 0 | 11 | 5 | 0 |
| 2020-z3n | 0 | 9 | 0.84 | 0.841 | 9 | 0 | 9 | 0 | 11 | 5 | 0 |
| cvc5 | 0 | 9 | 1.289 | 1.284 | 9 | 0 | 9 | 0 | 11 | 8 | 0 |
| cvc5 - fixedn | 0 | 9 | 1.311 | 1.308 | 9 | 0 | 9 | 0 | 11 | 8 | 0 |
| 2020-CVC4n | 0 | 9 | 1.545 | 1.543 | 9 | 0 | 9 | 0 | 11 | 8 | 0 |
| veriT | 0 | 7 | 1499.013 | 1499.026 | 7 | 0 | 7 | 2 | 11 | 10 | 0 |
| 2020-Vampiren | 0 | 7 | 2400.836 | 2400.831 | 7 | 0 | 7 | 2 | 11 | 13 | 0 |
| Vampire | 0 | 7 | 2401.545 | 2401.545 | 7 | 0 | 7 | 2 | 11 | 13 | 0 |
| iProver | 0 | 7 | 2484.444 | 2423.375 | 7 | 0 | 7 | 2 | 11 | 11 | 0 |
| SMTInterpol | 0 | 7 | 2540.001 | 2459.854 | 7 | 0 | 7 | 2 | 11 | 7 | 0 |
| Vampire - fixedn | 0 | 6 | 2401.631 | 2401.624 | 6 | 0 | 6 | 3 | 11 | 13 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 1189.148 | 915.692 | 0 | 0 | 0 | 9 | 11 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 11 | 216.075 | 216.832 | 11 | 2 | 9 | 9 | 9 | 0 |
| z3n | 0 | 11 | 216.882 | 216.883 | 11 | 2 | 9 | 9 | 9 | 0 |
| 2020-z3n | 0 | 11 | 216.943 | 216.944 | 11 | 2 | 9 | 9 | 9 | 0 |
| cvc5 - fixedn | 0 | 9 | 217.876 | 217.875 | 9 | 0 | 9 | 11 | 9 | 0 |
| cvc5 | 0 | 9 | 218.134 | 218.124 | 9 | 0 | 9 | 11 | 9 | 0 |
| 2020-CVC4n | 0 | 9 | 218.163 | 218.218 | 9 | 0 | 9 | 11 | 9 | 0 |
| SMTInterpol | 0 | 8 | 320.179 | 233.001 | 8 | 1 | 7 | 12 | 7 | 0 |
| veriT | 0 | 7 | 264.185 | 264.188 | 7 | 0 | 7 | 13 | 11 | 0 |
| iProver | 0 | 7 | 349.502 | 288.902 | 7 | 0 | 7 | 13 | 11 | 0 |
| 2020-Vampiren | 0 | 7 | 312.836 | 312.831 | 7 | 0 | 7 | 13 | 13 | 0 |
| Vampire | 0 | 7 | 313.545 | 313.545 | 7 | 0 | 7 | 13 | 13 | 0 |
| Vampire - fixedn | 0 | 6 | 313.631 | 313.624 | 6 | 0 | 6 | 14 | 13 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 235.689 | 176.999 | 0 | 0 | 0 | 20 | 5 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.