The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_UFBV division in the Single Query Track.
Page generated on 2020-07-04 11:46:59 +0000
Benchmarks: 217 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| Yices2 | Yices2 | Yices2 | Yices2 | Bitwuzla |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Yices2 | 0 | 211 | 14843.88 | 14845.61 | 211 | 129 | 82 | 6 | 6 | 0 | |
| Yices2-fixedn | 0 | 211 | 15140.808 | 15143.281 | 211 | 129 | 82 | 6 | 6 | 0 | |
| 2019-Yices 2.6.2n | 0 | 210 | 14972.751 | 14972.424 | 210 | 129 | 81 | 7 | 7 | 0 | |
| Bitwuzla | 0 | 207 | 3263.061 | 3263.74 | 207 | 128 | 79 | 10 | 0 | 0 | |
| Bitwuzla-fixedn | 0 | 207 | 3351.628 | 3327.041 | 207 | 128 | 79 | 10 | 0 | 0 | |
| MathSAT5n | 0 | 198 | 27676.285 | 27679.823 | 198 | 128 | 70 | 19 | 19 | 0 | |
| CVC4 | 0 | 197 | 31531.908 | 31538.491 | 197 | 128 | 69 | 20 | 20 | 0 | |
| z3n | 0 | 186 | 43601.719 | 43528.375 | 186 | 124 | 62 | 31 | 31 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Yices2 | 0 | 211 | 14844.49 | 14845.37 | 211 | 129 | 82 | 6 | 6 | 0 | |
| Yices2-fixedn | 0 | 211 | 15141.398 | 15142.951 | 211 | 129 | 82 | 6 | 6 | 0 | |
| 2019-Yices 2.6.2n | 0 | 210 | 14973.141 | 14972.264 | 210 | 129 | 81 | 7 | 7 | 0 | |
| Bitwuzla | 0 | 207 | 3263.061 | 3263.74 | 207 | 128 | 79 | 10 | 0 | 0 | |
| Bitwuzla-fixedn | 0 | 207 | 3351.628 | 3327.041 | 207 | 128 | 79 | 10 | 0 | 0 | |
| MathSAT5n | 0 | 198 | 27680.795 | 27678.973 | 198 | 128 | 70 | 19 | 19 | 0 | |
| CVC4 | 0 | 197 | 31539.118 | 31537.511 | 197 | 128 | 69 | 20 | 20 | 0 | |
| z3n | 0 | 186 | 43605.689 | 43526.795 | 186 | 124 | 62 | 31 | 31 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Yices2 | 0 | 129 | 209.752 | 209.785 | 129 | 129 | 0 | 88 | 6 | 0 |
| 2019-Yices 2.6.2n | 0 | 129 | 212.658 | 212.687 | 129 | 129 | 0 | 88 | 7 | 0 |
| Yices2-fixedn | 0 | 129 | 216.054 | 216.091 | 129 | 129 | 0 | 88 | 6 | 0 |
| Bitwuzla | 0 | 128 | 129.713 | 129.734 | 128 | 128 | 0 | 89 | 0 | 0 |
| Bitwuzla-fixedn | 0 | 128 | 133.795 | 131.184 | 128 | 128 | 0 | 89 | 0 | 0 |
| MathSAT5n | 0 | 128 | 1590.688 | 1588.122 | 128 | 128 | 0 | 89 | 19 | 0 |
| CVC4 | 0 | 128 | 1646.306 | 1643.071 | 128 | 128 | 0 | 89 | 20 | 0 |
| z3n | 0 | 124 | 7406.0 | 7360.421 | 124 | 124 | 0 | 93 | 31 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Yices2 | 0 | 82 | 14634.738 | 14635.584 | 82 | 0 | 82 | 135 | 6 | 0 |
| Yices2-fixedn | 0 | 82 | 14925.344 | 14926.86 | 82 | 0 | 82 | 135 | 6 | 0 |
| 2019-Yices 2.6.2n | 0 | 81 | 14760.483 | 14759.577 | 81 | 0 | 81 | 136 | 7 | 0 |
| Bitwuzla | 0 | 79 | 3133.348 | 3134.007 | 79 | 0 | 79 | 138 | 0 | 0 |
| Bitwuzla-fixedn | 0 | 79 | 3217.833 | 3195.857 | 79 | 0 | 79 | 138 | 0 | 0 |
| MathSAT5n | 0 | 70 | 26090.107 | 26090.85 | 70 | 0 | 70 | 147 | 19 | 0 |
| CVC4 | 0 | 69 | 29892.811 | 29894.44 | 69 | 0 | 69 | 148 | 20 | 0 |
| z3n | 0 | 62 | 36199.689 | 36166.373 | 62 | 0 | 62 | 155 | 31 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Bitwuzla | 0 | 198 | 612.988 | 613.12 | 198 | 128 | 70 | 19 | 9 | 0 | |
| Bitwuzla-fixedn | 0 | 198 | 642.443 | 617.245 | 198 | 128 | 70 | 19 | 9 | 0 | |
| 2019-Yices 2.6.2n | 0 | 188 | 795.84 | 794.169 | 188 | 128 | 60 | 29 | 29 | 0 | |
| Yices2 | 0 | 188 | 795.276 | 795.301 | 188 | 128 | 60 | 29 | 29 | 0 | |
| Yices2-fixedn | 0 | 188 | 796.132 | 796.159 | 188 | 128 | 60 | 29 | 29 | 0 | |
| CVC4 | 0 | 179 | 1553.473 | 1550.237 | 179 | 128 | 51 | 38 | 38 | 0 | |
| MathSAT5n | 0 | 177 | 1376.339 | 1373.766 | 177 | 125 | 52 | 40 | 40 | 0 | |
| z3n | 0 | 156 | 2043.464 | 2031.145 | 156 | 109 | 47 | 61 | 61 | 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.