The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_Equality division in the Unsat Core Track.
Page generated on 2021-07-18 17:31:25 +0000
Benchmarks: 2463 Time Limit: 1200 seconds Memory Limit: 60 GB
Logics:| Sequential Performance | Parallel Performance |
|---|---|
| cvc5-uc | cvc5-uc |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|
| z3n | 0 | 1143660 | 151976.692 | 152029.63 | 98 | 0 | |
| cvc5-uc | 0 | 447703 | 229933.31 | 229948.434 | 170 | 0 | |
| SMTInterpol | 0 | 386916 | 244711.085 | 232343.671 | 168 | 0 | |
| 2020-Yices2-fixedn | 0 | 276317 | 3731.189 | 3692.838 | 0 | 0 | |
| Yices2 | 0 | 276317 | 3909.914 | 3852.564 | 0 | 0 | |
| 2020-SMTInterpol-fixedn | 0 | 239090 | 14598.44 | 8490.431 | 0 | 0 | |
| MathSAT5n | 0 | 237041 | 1859.149 | 1844.501 | 0 | 0 | |
| SMTInterpol-remus | 0 | 221318 | 1404088.94 | 1348304.352 | 688 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|
| z3n | 0 | 1143660 | 152017.302 | 152024.8 | 98 | 0 | |
| cvc5-uc | 0 | 447703 | 229959.22 | 229942.384 | 170 | 0 | |
| SMTInterpol | 0 | 399875 | 245120.765 | 232160.671 | 163 | 0 | |
| SMTInterpol-remus | 0 | 374174 | 1425716.31 | 1318558.765 | 172 | 0 | |
| 2020-Yices2-fixedn | 0 | 276317 | 3731.189 | 3692.838 | 0 | 0 | |
| Yices2 | 0 | 276317 | 3909.914 | 3852.564 | 0 | 0 | |
| 2020-SMTInterpol-fixedn | 0 | 239090 | 14598.44 | 8490.431 | 0 | 0 | |
| MathSAT5n | 0 | 237041 | 1859.149 | 1844.501 | 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.