The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_BV division in the Challenge Track (incremental).
Page generated on 2019-07-23 17:57:31 +0000
Benchmarks: 7 Time Limit: 43200 seconds Memory Limit: 60 GB
| Parallel Performance |
|---|
| Boolector (incremental) |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|
| Boolector (incremental) | 0 | 110 | 25502.861 | 25501.216 | 0 | 0 | 0 | |
| 2018-MathSAT (incremental)n | 0 | 109 | 59895.543 | 59899.041 | 1 | 1 | 0 | |
| Yices 2.6.2 Incremental | 0 | 102 | 182741.58 | 182747.14 | 8 | 4 | 0 | |
| STP-incremental | 0 | 99 | 54913.168 | 54913.122 | 11 | 1 | 0 | |
| CVC4-inc-fixedn | 0 | 98 | 92348.09 | 92352.21 | 12 | 1 | 0 | |
| Z3n | 0 | 97 | 248932.47 | 248936.83 | 13 | 5 | 0 | |
| Minkeyrink Solver | 0 | 86 | 5093.107 | 5091.39 | 24 | 0 | 0 | |
| Minkeyrink Solver MT | 0 | 80 | 13418.389 | 4160.732 | 30 | 0 | 0 | |
| STP-mt | 0 | 37 | 43203.91 | 43204.606 | 73 | 1 | 0 | |
| CVC4-inc | 0 | 0 | 0.144 | 1.064 | 110 | 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.