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 2021-07-18 17:31:25 +0000
Benchmarks: 2628 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 |
|---|---|---|---|---|---|---|---|
| 2020-CVC4-ucn | 0 | 776683 | 187912.416 | 187950.741 | 148 | 0 | |
| cvc5-uc | 0 | 770781 | 195345.142 | 195376.634 | 156 | 0 | |
| z3n | 0 | 392891 | 341085.353 | 341102.384 | 202 | 8 | |
| SMTInterpol | 0 | 287674 | 905312.438 | 891617.8 | 713 | 0 | |
| SMTInterpol-remus | 0 | 177564 | 1553443.855 | 1491460.168 | 978 | 0 | |
| UltimateEliminator+MathSAT | 0 | 0 | 10956.247 | 6970.185 | 1 | 0 | |
| Vampire | 1 | 763559 | 200261.274 | 158804.532 | 120 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|
| 2020-CVC4-ucn | 0 | 776683 | 187942.876 | 187944.051 | 148 | 0 | |
| cvc5-uc | 0 | 770781 | 195370.792 | 195369.484 | 156 | 0 | |
| z3n | 0 | 392891 | 341122.603 | 341093.494 | 202 | 8 | |
| SMTInterpol | 0 | 290423 | 938780.208 | 880134.638 | 684 | 0 | |
| SMTInterpol-remus | 0 | 271770 | 1676096.135 | 1452966.131 | 684 | 0 | |
| UltimateEliminator+MathSAT | 0 | 0 | 10956.247 | 6970.185 | 1 | 0 | |
| Vampire | 1 | 776519 | 272215.154 | 140043.347 | 78 | 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.