The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the NIA logic in the Single Query Track.
Page generated on 2021-07-18 17:29:05 +0000
Benchmarks: 17 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 |
|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 - fixedn | 0 | 17 | 343.004 | 343.56 | 17 | 12 | 5 | 0 | 0 | 0 |
| 2018-Z3n | 0 | 16 | 9.389 | 9.394 | 16 | 12 | 4 | 1 | 0 | 0 |
| cvc5 | 0 | 16 | 325.665 | 1225.768 | 16 | 11 | 5 | 1 | 1 | 0 |
| 2020-z3n | 0 | 15 | 610.065 | 610.216 | 15 | 12 | 3 | 2 | 0 | 0 |
| z3n | 0 | 14 | 685.873 | 686.176 | 14 | 12 | 2 | 3 | 0 | 0 |
| 2020-CVC4n | 0 | 12 | 3761.659 | 3886.432 | 12 | 11 | 1 | 5 | 3 | 0 |
| UltimateEliminator+MathSAT | 0 | 9 | 8470.591 | 8436.51 | 9 | 8 | 1 | 8 | 7 | 0 |
| Vampire | 0 | 4 | 15968.619 | 15694.567 | 4 | 0 | 4 | 13 | 13 | 0 |
| Vampire - fixedn | 0 | 4 | 16180.875 | 15748.014 | 4 | 0 | 4 | 13 | 13 | 0 |
| iProver | 0 | 0 | 20400.0 | 20400.0 | 0 | 0 | 0 | 17 | 17 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 - fixedn | 0 | 17 | 343.004 | 343.56 | 17 | 12 | 5 | 0 | 0 | 0 |
| 2018-Z3n | 0 | 16 | 9.389 | 9.394 | 16 | 12 | 4 | 1 | 0 | 0 |
| cvc5 | 0 | 16 | 1225.683 | 1225.678 | 16 | 11 | 5 | 1 | 1 | 0 |
| 2020-z3n | 0 | 15 | 610.065 | 610.216 | 15 | 12 | 3 | 2 | 0 | 0 |
| z3n | 0 | 14 | 685.873 | 686.176 | 14 | 12 | 2 | 3 | 0 | 0 |
| 2020-CVC4n | 0 | 12 | 3886.109 | 3886.172 | 12 | 11 | 1 | 5 | 3 | 0 |
| UltimateEliminator+MathSAT | 0 | 9 | 8470.591 | 8436.51 | 9 | 8 | 1 | 8 | 7 | 0 |
| Vampire | 0 | 4 | 15968.619 | 15694.567 | 4 | 0 | 4 | 13 | 13 | 0 |
| Vampire - fixedn | 0 | 4 | 16180.875 | 15748.014 | 4 | 0 | 4 | 13 | 13 | 0 |
| iProver | 0 | 0 | 20400.0 | 20400.0 | 0 | 0 | 0 | 17 | 17 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2020-z3n | 0 | 12 | 0.746 | 0.746 | 12 | 12 | 0 | 0 | 5 | 0 | 0 |
| z3n | 0 | 12 | 0.805 | 0.809 | 12 | 12 | 0 | 0 | 5 | 0 | 0 |
| 2018-Z3n | 0 | 12 | 0.826 | 0.83 | 12 | 12 | 0 | 0 | 5 | 0 | 0 |
| cvc5 - fixedn | 0 | 12 | 331.411 | 331.968 | 12 | 12 | 0 | 0 | 5 | 0 | 0 |
| 2020-CVC4n | 0 | 11 | 285.801 | 285.864 | 11 | 11 | 0 | 1 | 5 | 3 | 0 |
| cvc5 | 0 | 11 | 1201.054 | 1201.049 | 11 | 11 | 0 | 1 | 5 | 1 | 0 |
| UltimateEliminator+MathSAT | 0 | 8 | 4849.531 | 4826.567 | 8 | 8 | 0 | 4 | 5 | 7 | 0 |
| iProver | 0 | 0 | 14400.0 | 14400.0 | 0 | 0 | 0 | 12 | 5 | 17 | 0 |
| Vampire | 0 | 0 | 14400.0 | 14400.0 | 0 | 0 | 0 | 12 | 5 | 13 | 0 |
| Vampire - fixedn | 0 | 0 | 14400.0 | 14400.0 | 0 | 0 | 0 | 12 | 5 | 13 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 - fixedn | 0 | 5 | 11.593 | 11.592 | 5 | 0 | 5 | 0 | 12 | 0 | 0 |
| cvc5 | 0 | 5 | 24.628 | 24.629 | 5 | 0 | 5 | 0 | 12 | 1 | 0 |
| 2018-Z3n | 0 | 4 | 8.563 | 8.563 | 4 | 0 | 4 | 1 | 12 | 0 | 0 |
| Vampire | 0 | 4 | 1568.619 | 1294.567 | 4 | 0 | 4 | 1 | 12 | 13 | 0 |
| Vampire - fixedn | 0 | 4 | 1780.875 | 1348.014 | 4 | 0 | 4 | 1 | 12 | 13 | 0 |
| 2020-z3n | 0 | 3 | 609.32 | 609.47 | 3 | 0 | 3 | 2 | 12 | 0 | 0 |
| z3n | 0 | 2 | 685.067 | 685.368 | 2 | 0 | 2 | 3 | 12 | 0 | 0 |
| 2020-CVC4n | 0 | 1 | 3600.308 | 3600.308 | 1 | 0 | 1 | 4 | 12 | 3 | 0 |
| UltimateEliminator+MathSAT | 0 | 1 | 3621.06 | 3609.943 | 1 | 0 | 1 | 4 | 12 | 7 | 0 |
| iProver | 0 | 0 | 6000.0 | 6000.0 | 0 | 0 | 0 | 5 | 12 | 17 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2018-Z3n | 0 | 16 | 9.389 | 9.394 | 16 | 12 | 4 | 1 | 0 | 0 |
| cvc5 - fixedn | 0 | 16 | 36.656 | 36.65 | 16 | 11 | 5 | 1 | 1 | 0 |
| cvc5 | 0 | 16 | 49.683 | 49.678 | 16 | 11 | 5 | 1 | 1 | 0 |
| 2020-z3n | 0 | 15 | 49.876 | 49.877 | 15 | 12 | 3 | 2 | 2 | 0 |
| z3n | 0 | 14 | 72.992 | 72.995 | 14 | 12 | 2 | 3 | 3 | 0 |
| 2020-CVC4n | 0 | 11 | 99.582 | 99.58 | 11 | 10 | 1 | 6 | 4 | 0 |
| UltimateEliminator+MathSAT | 0 | 9 | 238.591 | 204.51 | 9 | 8 | 1 | 8 | 7 | 0 |
| Vampire | 0 | 3 | 337.139 | 337.223 | 3 | 0 | 3 | 14 | 14 | 0 |
| Vampire - fixedn | 0 | 2 | 360.255 | 360.253 | 2 | 0 | 2 | 15 | 15 | 0 |
| iProver | 0 | 0 | 408.0 | 408.0 | 0 | 0 | 0 | 17 | 17 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.