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 Incremental Track.
Page generated on 2019-07-23 17:57:24 +0000
Benchmarks: 1291 Time Limit: 2400 seconds Memory Limit: 60 GB
| Parallel Performance |
|---|
| Yices 2.6.2 Incremental |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|
| Yices 2.6.2 Incremental | 0 | 28864 | 36983.674 | 36919.074 | 531 | 10 | 0 | |
| Minkeyrink Solver MT | 0 | 28857 | 48178.659 | 31397.344 | 538 | 8 | 0 | |
| Minkeyrink Solver | 0 | 28848 | 31497.778 | 31398.148 | 547 | 8 | 0 | |
| 2018-MathSAT (incremental)n | 0 | 28847 | 54562.537 | 54442.89 | 548 | 13 | 0 | |
| STP-incremental | 0 | 28803 | 34147.759 | 34042.746 | 592 | 9 | 0 | |
| Boolector (incremental) | 0 | 28785 | 36369.627 | 36303.009 | 610 | 9 | 0 | |
| CVC4-inc-fixedn | 0 | 28504 | 86002.89 | 85913.522 | 891 | 10 | 0 | |
| Z3n | 0 | 28403 | 188172.007 | 188127.983 | 992 | 35 | 0 | |
| STP-mt | 0 | 2559 | 9137.281 | 5245.373 | 26836 | 0 | 0 | |
| Boolector-ReasonLSn | 0 | 371 | 115.734 | 162.487 | 29024 | 0 | 0 | |
| CVC4-inc | 0 | 0 | 6.573 | 63.471 | 29395 | 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.