The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the Equality+NonLinearArith division in the Single Query Track.
Page generated on 2023-07-06 16:04:54 +0000
Benchmarks: 9551 Time Limit: 1200 seconds Memory Limit: 60 GB
Logics:| 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 | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 6256 | 127760.327 | 131004.527 | 6256 | 745 | 5511 | 3295 | 0 | 3137 | 0 |
| 2022-cvc5n | 0 | 6219 | 142048.316 | 144583.562 | 6219 | 741 | 5478 | 3276 | 56 | 3166 | 0 |
| Vampire | 0 | 4889 | 490858.535 | 124040.797 | 4889 | 0 | 4889 | 4662 | 0 | 4606 | 0 |
| iProver | 0 | 3620 | 230324.704 | 60301.76 | 3620 | 0 | 3620 | 5931 | 0 | 5931 | 0 |
| iProver Fixedn | 0 | 3591 | 209556.485 | 54960.03 | 3591 | 0 | 3591 | 5960 | 0 | 5960 | 0 |
| UltimateEliminator+MathSAT | 0 | 608 | 11637.288 | 10430.454 | 608 | 426 | 182 | 6030 | 2913 | 531 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 6256 | 127760.327 | 131004.527 | 6256 | 745 | 5511 | 3295 | 0 | 3137 | 0 |
| 2022-cvc5n | 0 | 6219 | 142048.316 | 144583.562 | 6219 | 741 | 5478 | 3276 | 56 | 3166 | 0 |
| Vampire | 0 | 5239 | 1252881.755 | 315641.715 | 5239 | 0 | 5239 | 4312 | 0 | 4254 | 0 |
| iProver | 0 | 3856 | 662175.104 | 170035.179 | 3856 | 0 | 3856 | 5695 | 0 | 5695 | 0 |
| iProver Fixedn | 0 | 3828 | 610036.105 | 156538.001 | 3828 | 0 | 3828 | 5723 | 0 | 5723 | 0 |
| UltimateEliminator+MathSAT | 0 | 608 | 11637.288 | 10430.454 | 608 | 426 | 182 | 6030 | 2913 | 531 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 745 | 23882.181 | 23928.262 | 745 | 745 | 0 | 7 | 8799 | 3137 | 0 |
| 2022-cvc5n | 0 | 741 | 29139.899 | 29266.639 | 741 | 741 | 0 | 8 | 8802 | 3166 | 0 |
| UltimateEliminator+MathSAT | 0 | 426 | 10386.566 | 9536.193 | 426 | 426 | 0 | 326 | 8799 | 531 | 0 |
| Vampire | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 752 | 8799 | 4254 | 0 |
| iProver | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 752 | 8799 | 5695 | 0 |
| iProver Fixedn | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 752 | 8799 | 5723 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 5511 | 103878.146 | 107076.265 | 5511 | 0 | 5511 | 332 | 3708 | 3137 | 0 |
| 2022-cvc5n | 0 | 5478 | 112908.417 | 115316.924 | 5478 | 0 | 5478 | 364 | 3709 | 3166 | 0 |
| Vampire | 0 | 5239 | 1252881.755 | 315641.715 | 5239 | 0 | 5239 | 604 | 3708 | 4254 | 0 |
| iProver | 0 | 3856 | 662175.104 | 170035.179 | 3856 | 0 | 3856 | 1987 | 3708 | 5695 | 0 |
| iProver Fixedn | 0 | 3828 | 610036.105 | 156538.001 | 3828 | 0 | 3828 | 2015 | 3708 | 5723 | 0 |
| UltimateEliminator+MathSAT | 0 | 182 | 1250.723 | 894.261 | 182 | 0 | 182 | 3063 | 6306 | 531 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 5597 | 3046.015 | 3006.588 | 5597 | 691 | 4906 | 3954 | 0 | 3804 | 0 |
| 2022-cvc5n | 0 | 5524 | 3859.53 | 3801.6 | 5524 | 676 | 4848 | 3971 | 56 | 3868 | 0 |
| Vampire | 0 | 3508 | 24421.9 | 6507.436 | 3508 | 0 | 3508 | 6043 | 0 | 5987 | 0 |
| iProver Fixedn | 0 | 3159 | 25007.163 | 7676.112 | 3159 | 0 | 3159 | 6392 | 0 | 6392 | 0 |
| iProver | 0 | 3156 | 25530.051 | 7772.705 | 3156 | 0 | 3156 | 6395 | 0 | 6395 | 0 |
| UltimateEliminator+MathSAT | 0 | 569 | 4118.092 | 3003.98 | 569 | 389 | 180 | 6069 | 2913 | 639 | 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.