The International Satisfiability Modulo Theories (SMT) Competition.
Competition results for the BV division in the Single Query Track.
Page generated on 2020-01-29 22:04:58 +0000
Benchmarks: 696 Time Limit: 2400 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| CVC4 | CVC4 | CVC4 | CVC4 | CVC4 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 661 | 92766.602 | 86266.714 | 661 | 197 | 464 | 35 | 35 | 0 |
| CVC4 | 0 | 612 | 135421.639 | 138922.161 | 612 | 167 | 445 | 84 | 84 | 0 |
| Bitwuzla-fixedn | 0 | 598 | 250845.351 | 126719.446 | 598 | 193 | 405 | 98 | 98 | 0 |
| z3n | 0 | 576 | 145397.064 | 145418.357 | 576 | 173 | 403 | 120 | 116 | 1 |
| UltimateEliminator+MathSAT | 0 | 227 | 171381.248 | 155549.56 | 227 | 13 | 214 | 469 | 103 | 0 |
| Bitwuzla | 40 | 571 | 210426.481 | 111264.253 | 571 | 183 | 388 | 125 | 85 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 663 | 171030.172 | 43426.815 | 663 | 198 | 465 | 33 | 33 | 0 |
| CVC4 | 0 | 612 | 135421.639 | 138922.161 | 612 | 167 | 445 | 84 | 84 | 0 |
| Bitwuzla-fixedn | 0 | 598 | 250845.371 | 125519.496 | 598 | 193 | 405 | 98 | 98 | 0 |
| z3n | 0 | 576 | 145397.064 | 145418.357 | 576 | 173 | 403 | 120 | 116 | 1 |
| UltimateEliminator+MathSAT | 0 | 227 | 204638.328 | 125551.13 | 227 | 13 | 214 | 469 | 103 | 0 |
| Bitwuzla | 40 | 571 | 210426.881 | 105264.503 | 571 | 183 | 388 | 125 | 85 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 198 | 55841.536 | 14180.11 | 198 | 198 | 0 | 498 | 33 | 0 |
| Bitwuzla-fixedn | 0 | 193 | 43650.58 | 21864.593 | 193 | 193 | 0 | 503 | 98 | 0 |
| z3n | 0 | 173 | 40536.761 | 40543.76 | 173 | 173 | 0 | 523 | 116 | 1 |
| CVC4 | 0 | 167 | 81859.289 | 83942.896 | 167 | 167 | 0 | 529 | 84 | 0 |
| UltimateEliminator+MathSAT | 0 | 13 | 124989.653 | 73999.781 | 13 | 13 | 0 | 683 | 103 | 0 |
| Bitwuzla | 14 | 183 | 26941.564 | 13485.316 | 183 | 183 | 0 | 513 | 85 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 465 | 72571.006 | 18445.915 | 465 | 0 | 465 | 231 | 33 | 0 |
| CVC4 | 0 | 445 | 43037.991 | 44178.365 | 445 | 0 | 445 | 251 | 84 | 0 |
| Bitwuzla-fixedn | 0 | 405 | 185599.402 | 92854.514 | 405 | 0 | 405 | 291 | 98 | 0 |
| z3n | 0 | 403 | 94061.273 | 94074.247 | 403 | 0 | 403 | 293 | 116 | 1 |
| UltimateEliminator+MathSAT | 0 | 214 | 74960.698 | 49134.578 | 214 | 0 | 214 | 482 | 103 | 0 |
| Bitwuzla | 26 | 388 | 161889.627 | 80978.627 | 388 | 0 | 388 | 308 | 85 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 644 | 2652.822 | 1651.77 | 644 | 186 | 458 | 52 | 52 | 0 |
| Bitwuzla-fixedn | 0 | 565 | 4088.43 | 3645.216 | 565 | 181 | 384 | 131 | 131 | 0 |
| z3n | 0 | 559 | 3606.942 | 3607.062 | 559 | 171 | 388 | 137 | 136 | 1 |
| CVC4 | 0 | 529 | 4660.844 | 4647.141 | 529 | 99 | 430 | 167 | 167 | 0 |
| UltimateEliminator+MathSAT | 0 | 226 | 5009.976 | 4194.233 | 226 | 13 | 213 | 470 | 109 | 0 |
| Bitwuzla | 40 | 552 | 3170.007 | 2858.553 | 552 | 181 | 371 | 144 | 104 | 0 |
n Non-competing.