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 2022-08-10 11:17:45 +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 |
|---|---|---|---|---|---|---|---|---|---|---|
| z3-4.8.17n | 0 | 11 | 7473.103 | 7474.313 | 11 | 2 | 9 | 9 | 5 | 0 |
| 2020-CVC4n | 0 | 10 | 10043.637 | 10135.712 | 10 | 1 | 9 | 10 | 8 | 0 |
| cvc5 | 0 | 10 | 10064.453 | 10192.123 | 10 | 1 | 9 | 10 | 8 | 0 |
| smtinterpol | 0 | 8 | 8842.267 | 8707.326 | 8 | 1 | 7 | 12 | 7 | 0 |
| veriT | 0 | 7 | 11116.982 | 11117.758 | 7 | 0 | 7 | 13 | 9 | 0 |
| Vampire | 0 | 7 | 15600.991 | 15601.416 | 7 | 0 | 7 | 13 | 13 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 153.02 | 74.452 | 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 |
|---|---|---|---|---|---|---|---|---|---|---|
| z3-4.8.17n | 0 | 11 | 7474.083 | 7474.173 | 11 | 2 | 9 | 9 | 5 | 0 |
| 2020-CVC4n | 0 | 10 | 10088.927 | 10135.482 | 10 | 1 | 9 | 10 | 8 | 0 |
| cvc5 | 0 | 10 | 10119.093 | 10191.783 | 10 | 1 | 9 | 10 | 8 | 0 |
| smtinterpol | 0 | 8 | 8842.267 | 8707.326 | 8 | 1 | 7 | 12 | 7 | 0 |
| veriT | 0 | 7 | 11117.502 | 11117.528 | 7 | 0 | 7 | 13 | 9 | 0 |
| Vampire | 0 | 7 | 19201.201 | 15600.826 | 7 | 0 | 7 | 13 | 13 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 153.02 | 74.452 | 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 |
|---|---|---|---|---|---|---|---|---|---|---|---|
| z3-4.8.17n | 0 | 2 | 1200.077 | 1200.073 | 2 | 2 | 0 | 1 | 17 | 5 | 0 |
| 2020-CVC4n | 0 | 1 | 487.413 | 533.971 | 1 | 1 | 0 | 2 | 17 | 8 | 0 |
| cvc5 | 0 | 1 | 517.319 | 590.013 | 1 | 1 | 0 | 2 | 17 | 8 | 0 |
| smtinterpol | 0 | 1 | 1201.51 | 1200.937 | 1 | 1 | 0 | 2 | 17 | 7 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 13.969 | 8.604 | 0 | 0 | 0 | 3 | 17 | 0 | 0 |
| veriT | 0 | 0 | 1200.023 | 1200.026 | 0 | 0 | 0 | 3 | 17 | 9 | 0 |
| Vampire | 0 | 0 | 7200.21 | 3599.41 | 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 |
|---|---|---|---|---|---|---|---|---|---|---|---|
| z3-4.8.17n | 0 | 9 | 0.653 | 0.638 | 9 | 0 | 9 | 0 | 11 | 5 | 0 |
| 2020-CVC4n | 0 | 9 | 1.513 | 1.511 | 9 | 0 | 9 | 0 | 11 | 8 | 0 |
| cvc5 | 0 | 9 | 1.773 | 1.77 | 9 | 0 | 9 | 0 | 11 | 8 | 0 |
| veriT | 0 | 7 | 317.479 | 317.502 | 7 | 0 | 7 | 2 | 11 | 9 | 0 |
| Vampire | 0 | 7 | 2400.991 | 2401.416 | 7 | 0 | 7 | 2 | 11 | 13 | 0 |
| smtinterpol | 0 | 7 | 2828.297 | 2701.361 | 7 | 0 | 7 | 2 | 11 | 7 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 100.306 | 42.618 | 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 |
|---|---|---|---|---|---|---|---|---|---|---|
| z3-4.8.17n | 0 | 11 | 216.731 | 216.711 | 11 | 2 | 9 | 9 | 9 | 0 |
| 2020-CVC4n | 0 | 9 | 218.132 | 218.23 | 9 | 0 | 9 | 11 | 9 | 0 |
| cvc5 | 0 | 9 | 218.459 | 218.507 | 9 | 0 | 9 | 11 | 9 | 0 |
| veriT | 0 | 7 | 264.237 | 264.238 | 7 | 0 | 7 | 13 | 11 | 0 |
| Vampire | 0 | 7 | 312.991 | 313.416 | 7 | 0 | 7 | 13 | 13 | 0 |
| smtinterpol | 0 | 5 | 363.904 | 299.943 | 5 | 1 | 4 | 15 | 10 | 0 |
| UltimateEliminator+MathSAT | 0 | 0 | 153.02 | 74.452 | 0 | 0 | 0 | 20 | 0 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.