The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_ABV division in the Incremental Track.
Page generated on 2020-07-04 11:47:56 +0000
Benchmarks: 508 Time Limit: 1200 seconds Memory Limit: 60 GB
| Parallel Performance |
|---|
| Bitwuzla |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|
| Bitwuzla-fixedn | 0 | 1241 | 33556.365 | 33540.972 | 18 | 18 | 0 | |
| Bitwuzla | 0 | 1241 | 33579.409 | 33564.271 | 18 | 18 | 0 | |
| Yices2 incremental | 0 | 1238 | 13347.304 | 13309.089 | 21 | 7 | 0 | |
| 2018-Boolector (incremental)n | 0 | 1238 | 41815.253 | 41839.697 | 21 | 17 | 0 | |
| Yices2-fixed incrementaln | 0 | 1237 | 13468.034 | 13409.409 | 22 | 8 | 0 | |
| MathSAT5n | 0 | 1231 | 20295.778 | 20258.157 | 28 | 13 | 0 | |
| z3n | 0 | 1136 | 152412.7 | 152401.766 | 123 | 114 | 0 | |
| CVC4-inc | 0 | 1098 | 26609.693 | 26563.877 | 161 | 18 | 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.