The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the Equality division in the Unsat Core Track.
Page generated on 2022-08-10 11:18:51 +0000
Benchmarks: 2938 Time Limit: 1200 seconds Memory Limit: 60 GB
Logics:| Sequential Performance | Parallel Performance |
|---|---|
| cvc5 | Vampire |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|
| 2020-CVC4-ucn | 0 | 825656 | 400559.654 | 409341.873 | 331 | 0 | |
| cvc5 | 0 | 823606 | 381426.7 | 381458.974 | 310 | 0 | |
| Vampire | 0 | 820883 | 364293.229 | 297670.269 | 229 | 0 | |
| z3-4.8.17n | 0 | 711172 | 604303.48 | 605089.146 | 360 | 23 | |
| smtinterpol | 0 | 495549 | 1672280.22 | 1651612.208 | 1326 | 0 | |
| UltimateEliminator+MathSAT | 0 | 1 | 14549.765 | 8476.615 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|
| Vampire | 0 | 843995 | 499517.049 | 252608.762 | 149 | 0 | |
| 2020-CVC4-ucn | 0 | 825656 | 409253.264 | 409326.163 | 331 | 0 | |
| cvc5 | 0 | 823606 | 381483.44 | 381444.614 | 310 | 0 | |
| z3-4.8.17n | 0 | 711172 | 604377.44 | 605072.576 | 360 | 23 | |
| smtinterpol | 0 | 498006 | 1733255.67 | 1636984.255 | 1283 | 0 | |
| UltimateEliminator+MathSAT | 0 | 1 | 14549.765 | 8476.615 | 0 | 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.