The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_UFBV logic in the Unsat Core Track.
Page generated on 2021-07-18 17:31:25 +0000
Benchmarks: 326 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 | Timeout | Memout |
---|---|---|---|---|---|---|
Bitwuzla | 0 | 971861 | 21230.841 | 21235.2 | 6 | 0 |
cvc5-uc | 0 | 920403 | 26097.658 | 26094.324 | 8 | 0 |
z3n | 0 | 607199 | 73837.564 | 73853.747 | 60 | 0 |
2020-Yices2n | 0 | 601295 | 74204.777 | 74225.09 | 61 | 0 |
Yices2 | 0 | 601295 | 74278.135 | 74296.988 | 61 | 0 |
2020-z3n | 0 | 598359 | 74441.89 | 74457.475 | 62 | 0 |
MathSAT5n | 0 | 0 | 28.401 | 28.465 | 0 | 0 |
Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Timeout | Memout |
---|---|---|---|---|---|---|
Bitwuzla | 0 | 971861 | 21232.081 | 21234.82 | 6 | 0 |
cvc5-uc | 0 | 920403 | 26099.558 | 26094.124 | 8 | 0 |
z3n | 0 | 607199 | 73850.654 | 73850.887 | 60 | 0 |
2020-Yices2n | 0 | 601295 | 74221.627 | 74222.21 | 61 | 0 |
Yices2 | 0 | 601295 | 74293.865 | 74294.228 | 61 | 0 |
2020-z3n | 0 | 598359 | 74454.52 | 74454.545 | 62 | 0 |
MathSAT5n | 0 | 0 | 28.401 | 28.465 | 0 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.