The International Satisfiability Modulo Theories (SMT) Competition.
Competition results for the QF_Equality+BVArith (QF_ABV, QF_UFBV, QF_AUFBV) division in the Single Query Track.
Page generated on 2020-01-29 22:04:58 +0000
Benchmarks: 3636 Time Limit: 2400 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| Yices2 | Yices2 | Bitwuzla | Yices2 | Bitwuzla |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Yices2 | 0 | 3594 | 84216.893 | 84246.469 | 3594 | 2442 | 1152 | 42 | 42 | 0 |
| Yices2-fixedn | 0 | 3594 | 84416.636 | 84458.331 | 3594 | 2442 | 1152 | 42 | 42 | 0 |
| Bitwuzla | 0 | 3591 | 39279.56 | 39298.666 | 3591 | 2443 | 1148 | 45 | 19 | 0 |
| Bitwuzla-fixedn | 0 | 3591 | 39399.656 | 39374.347 | 3591 | 2443 | 1148 | 45 | 19 | 0 |
| MathSAT5n | 0 | 3526 | 159948.267 | 159953.645 | 3526 | 2409 | 1117 | 110 | 109 | 1 |
| CVC4 | 0 | 3517 | 162592.875 | 165636.447 | 3517 | 2412 | 1105 | 119 | 119 | 0 |
| z3n | 0 | 3489 | 204669.966 | 204567.035 | 3489 | 2389 | 1100 | 147 | 147 | 0 |
| 2019-Boolectorn | 0 | 3369 | 30976.492 | 30972.207 | 3369 | 2311 | 1058 | 16 | 16 | 0 |
| 2019-Par4n | 0 | 3365 | 69306.186 | 52921.14 | 3365 | 2307 | 1058 | 20 | 20 | 0 |
| 2019-Yices 2.6.2n | 0 | 235 | 30011.237 | 30012.745 | 235 | 137 | 98 | 16 | 16 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Yices2 | 0 | 3594 | 84216.893 | 84246.469 | 3594 | 2442 | 1152 | 42 | 42 | 0 |
| Yices2-fixedn | 0 | 3594 | 84416.636 | 84458.331 | 3594 | 2442 | 1152 | 42 | 42 | 0 |
| Bitwuzla | 0 | 3591 | 39279.56 | 39298.666 | 3591 | 2443 | 1148 | 45 | 19 | 0 |
| Bitwuzla-fixedn | 0 | 3591 | 39399.656 | 39374.347 | 3591 | 2443 | 1148 | 45 | 19 | 0 |
| MathSAT5n | 0 | 3526 | 159948.267 | 159953.645 | 3526 | 2409 | 1117 | 110 | 109 | 1 |
| CVC4 | 0 | 3517 | 162592.875 | 165636.447 | 3517 | 2412 | 1105 | 119 | 119 | 0 |
| z3n | 0 | 3489 | 204669.966 | 204567.035 | 3489 | 2389 | 1100 | 147 | 147 | 0 |
| 2019-Boolectorn | 0 | 3369 | 30976.492 | 30972.207 | 3369 | 2311 | 1058 | 16 | 16 | 0 |
| 2019-Par4n | 0 | 3366 | 89838.446 | 31147.69 | 3366 | 2308 | 1058 | 19 | 19 | 0 |
| 2019-Yices 2.6.2n | 0 | 235 | 30011.237 | 30012.745 | 235 | 137 | 98 | 16 | 16 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Bitwuzla-fixedn | 0 | 2443 | 6716.142 | 6700.09 | 2443 | 2443 | 0 | 1193 | 19 | 0 |
| Bitwuzla | 0 | 2443 | 6701.521 | 6705.071 | 2443 | 2443 | 0 | 1193 | 19 | 0 |
| Yices2 | 0 | 2442 | 21327.899 | 21339.293 | 2442 | 2442 | 0 | 1194 | 42 | 0 |
| Yices2-fixedn | 0 | 2442 | 21326.109 | 21348.546 | 2442 | 2442 | 0 | 1194 | 42 | 0 |
| CVC4 | 0 | 2412 | 54991.687 | 57232.09 | 2412 | 2412 | 0 | 1224 | 119 | 0 |
| MathSAT5n | 0 | 2409 | 63560.516 | 63545.443 | 2409 | 2409 | 0 | 1227 | 109 | 1 |
| z3n | 0 | 2389 | 88494.525 | 88420.761 | 2389 | 2389 | 0 | 1247 | 147 | 0 |
| 2019-Boolectorn | 0 | 2311 | 5497.682 | 5487.168 | 2311 | 2311 | 0 | 1074 | 16 | 0 |
| 2019-Par4n | 0 | 2308 | 19045.198 | 7450.659 | 2308 | 2308 | 0 | 1077 | 19 | 0 |
| 2019-Yices 2.6.2n | 0 | 137 | 7338.95 | 7339.895 | 137 | 137 | 0 | 114 | 16 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Yices2 | 0 | 1152 | 58089.523 | 58107.007 | 1152 | 0 | 1152 | 2484 | 42 | 0 |
| Yices2-fixedn | 0 | 1152 | 58290.828 | 58309.605 | 1152 | 0 | 1152 | 2484 | 42 | 0 |
| Bitwuzla | 0 | 1148 | 27780.249 | 27793.325 | 1148 | 0 | 1148 | 2488 | 19 | 0 |
| Bitwuzla-fixedn | 0 | 1148 | 27884.444 | 27873.997 | 1148 | 0 | 1148 | 2488 | 19 | 0 |
| MathSAT5n | 0 | 1117 | 91588.971 | 91607.912 | 1117 | 0 | 1117 | 2519 | 109 | 1 |
| CVC4 | 0 | 1105 | 103029.708 | 103604.127 | 1105 | 0 | 1105 | 2531 | 119 | 0 |
| z3n | 0 | 1100 | 111377.401 | 111346.094 | 1100 | 0 | 1100 | 2536 | 147 | 0 |
| 2019-Par4n | 0 | 1058 | 70793.249 | 23697.031 | 1058 | 0 | 1058 | 2327 | 19 | 0 |
| 2019-Boolectorn | 0 | 1058 | 25478.81 | 25485.039 | 1058 | 0 | 1058 | 2327 | 16 | 0 |
| 2019-Yices 2.6.2n | 0 | 98 | 17872.697 | 17872.669 | 98 | 0 | 98 | 153 | 16 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Bitwuzla | 0 | 3518 | 3722.678 | 3732.695 | 3518 | 2406 | 1112 | 118 | 92 | 0 |
| Bitwuzla-fixedn | 0 | 3518 | 3775.07 | 3742.806 | 3518 | 2406 | 1112 | 118 | 92 | 0 |
| Yices2 | 0 | 3487 | 4803.832 | 4822.163 | 3487 | 2399 | 1088 | 149 | 149 | 0 |
| Yices2-fixedn | 0 | 3487 | 4793.74 | 4822.554 | 3487 | 2399 | 1088 | 149 | 149 | 0 |
| CVC4 | 0 | 3420 | 8406.768 | 8373.301 | 3420 | 2360 | 1060 | 216 | 216 | 0 |
| MathSAT5n | 0 | 3404 | 7873.802 | 7837.288 | 3404 | 2344 | 1060 | 232 | 231 | 1 |
| z3n | 0 | 3386 | 8266.616 | 8231.564 | 3386 | 2333 | 1053 | 250 | 250 | 0 |
| 2019-Par4n | 0 | 3328 | 3205.756 | 2104.379 | 3328 | 2293 | 1035 | 57 | 57 | 0 |
| 2019-Boolectorn | 0 | 3306 | 2991.139 | 2982.312 | 3306 | 2275 | 1031 | 79 | 79 | 0 |
| 2019-Yices 2.6.2n | 0 | 204 | 1264.128 | 1262.459 | 204 | 130 | 74 | 47 | 47 | 0 |
n Non-competing.