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 Unsat Core Track.
Page generated on 2020-07-04 11:49:33 +0000
Benchmarks: 1492 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance |
|---|---|
| Bitwuzla | Bitwuzla |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|
| z3n | 0 | 174340 | 40200.777 | 40208.972 | 28 | 0 | |
| Bitwuzla | 0 | 171321 | 26899.724 | 26845.316 | 12 | 0 | |
| Yices2-fixedn | 0 | 171147 | 30701.986 | 30687.27 | 19 | 0 | |
| Yices2 | 0 | 171087 | 30972.869 | 30934.232 | 20 | 0 | |
| Bitwuzla-fixedn | 0 | 168993 | 26229.19 | 26207.912 | 13 | 0 | |
| CVC4-uc | 0 | 149406 | 46134.975 | 46146.135 | 34 | 0 | |
| MathSAT5n | 0 | 88 | 43.312 | 43.101 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|
| z3n | 0 | 174340 | 40206.167 | 40207.542 | 28 | 0 | |
| Bitwuzla | 0 | 171321 | 26903.294 | 26844.696 | 12 | 0 | |
| Yices2-fixedn | 0 | 171147 | 30705.296 | 30686.41 | 19 | 0 | |
| Yices2 | 0 | 171087 | 30976.979 | 30933.252 | 20 | 0 | |
| Bitwuzla-fixedn | 0 | 168993 | 26231.89 | 26207.462 | 13 | 0 | |
| CVC4-uc | 0 | 149406 | 46147.075 | 46144.865 | 34 | 0 | |
| MathSAT5n | 0 | 88 | 43.312 | 43.101 | 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.