The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the Bitvec division in the Unsat Core Track.
Page generated on 2021-07-18 17:31:25 +0000
Benchmarks: 300 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 | 80 | 94429.871 | 94458.077 | 78 | 0 | |
| cvc5-uc | 0 | 77 | 95973.332 | 95985.567 | 78 | 0 | |
| z3n | 0 | 43 | 28336.359 | 28302.139 | 20 | 0 | |
| UltimateEliminator+MathSAT | 0 | 0 | 13102.189 | 12243.819 | 9 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|
| 2020-CVC4-ucn | 0 | 80 | 94453.791 | 94453.927 | 78 | 0 | |
| cvc5-uc | 0 | 77 | 95984.772 | 95982.557 | 78 | 0 | |
| z3n | 0 | 43 | 28340.759 | 28301.289 | 20 | 0 | |
| UltimateEliminator+MathSAT | 0 | 0 | 13102.189 | 12243.819 | 9 | 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.