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 Single Query Track.
Page generated on 2020-07-04 11:46:58 +0000
Benchmarks: 3385 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| Bitwuzla | Bitwuzla | Bitwuzla | Bitwuzla | Bitwuzla |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Bitwuzla | 0 | 3370 | 30617.418 | 30633.017 | 3370 | 2311 | 1059 | 15 | 15 | 0 | |
| Bitwuzla-fixedn | 0 | 3370 | 30645.93 | 30643.549 | 3370 | 2311 | 1059 | 15 | 15 | 0 | |
| 2019-Boolectorn | 0 | 3369 | 30976.372 | 30972.057 | 3369 | 2311 | 1058 | 16 | 16 | 0 | |
| 2019-Par4n | 0 | 3360 | 43289.226 | 34638.906 | 3360 | 2305 | 1055 | 25 | 25 | 0 | |
| Yices2 | 0 | 3358 | 54245.844 | 54271.457 | 3358 | 2305 | 1053 | 27 | 27 | 0 | |
| Yices2-fixedn | 0 | 3358 | 54258.657 | 54295.569 | 3358 | 2305 | 1053 | 27 | 27 | 0 | |
| MathSAT5n | 0 | 3311 | 108307.431 | 108303.699 | 3311 | 2278 | 1033 | 74 | 73 | 1 | |
| CVC4 | 0 | 3309 | 104284.532 | 106386.89 | 3309 | 2283 | 1026 | 76 | 76 | 0 | |
| z3n | 0 | 3284 | 141860.837 | 141826.453 | 3284 | 2261 | 1023 | 101 | 101 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Bitwuzla | 0 | 3370 | 30619.818 | 30632.397 | 3370 | 2311 | 1059 | 15 | 15 | 0 | |
| Bitwuzla-fixedn | 0 | 3370 | 30647.86 | 30643.069 | 3370 | 2311 | 1059 | 15 | 15 | 0 | |
| 2019-Boolectorn | 0 | 3369 | 30977.892 | 30971.407 | 3369 | 2311 | 1058 | 16 | 16 | 0 | |
| 2019-Par4n | 0 | 3366 | 46773.206 | 31145.95 | 3366 | 2308 | 1058 | 19 | 19 | 0 | |
| Yices2 | 0 | 3358 | 54249.134 | 54270.317 | 3358 | 2305 | 1053 | 27 | 27 | 0 | |
| Yices2-fixedn | 0 | 3358 | 54262.257 | 54294.469 | 3358 | 2305 | 1053 | 27 | 27 | 0 | |
| MathSAT5n | 0 | 3311 | 108329.961 | 108300.409 | 3311 | 2278 | 1033 | 74 | 73 | 1 | |
| CVC4 | 0 | 3309 | 106021.592 | 106383.01 | 3309 | 2283 | 1026 | 76 | 76 | 0 | |
| z3n | 0 | 3284 | 141873.987 | 141822.753 | 3284 | 2261 | 1023 | 101 | 101 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Boolectorn | 0 | 2311 | 5497.682 | 5487.168 | 2311 | 2311 | 0 | 1074 | 16 | 0 |
| Bitwuzla-fixedn | 0 | 2311 | 6018.941 | 6005.27 | 2311 | 2311 | 0 | 1074 | 15 | 0 |
| Bitwuzla | 0 | 2311 | 6009.253 | 6012.523 | 2311 | 2311 | 0 | 1074 | 15 | 0 |
| 2019-Par4n | 0 | 2308 | 14271.018 | 7450.359 | 2308 | 2308 | 0 | 1077 | 19 | 0 |
| Yices2 | 0 | 2305 | 13990.207 | 13999.721 | 2305 | 2305 | 0 | 1080 | 27 | 0 |
| Yices2-fixedn | 0 | 2305 | 14005.894 | 14026.538 | 2305 | 2305 | 0 | 1080 | 27 | 0 |
| CVC4 | 0 | 2283 | 43169.393 | 43506.049 | 2283 | 2283 | 0 | 1102 | 76 | 0 |
| MathSAT5n | 0 | 2278 | 51014.545 | 50988.625 | 2278 | 2278 | 0 | 1107 | 73 | 1 |
| z3n | 0 | 2261 | 72328.623 | 72290.01 | 2261 | 2261 | 0 | 1124 | 101 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Bitwuzla | 0 | 1059 | 24610.564 | 24619.873 | 1059 | 0 | 1059 | 2326 | 15 | 0 |
| Bitwuzla-fixedn | 0 | 1059 | 24628.918 | 24637.798 | 1059 | 0 | 1059 | 2326 | 15 | 0 |
| 2019-Par4n | 0 | 1058 | 32502.189 | 23695.591 | 1058 | 0 | 1058 | 2327 | 19 | 0 |
| 2019-Boolectorn | 0 | 1058 | 25480.21 | 25484.239 | 1058 | 0 | 1058 | 2327 | 16 | 0 |
| Yices2-fixedn | 0 | 1053 | 40256.362 | 40267.931 | 1053 | 0 | 1053 | 2332 | 27 | 0 |
| Yices2 | 0 | 1053 | 40258.927 | 40270.596 | 1053 | 0 | 1053 | 2332 | 27 | 0 |
| MathSAT5n | 0 | 1033 | 57315.416 | 57311.785 | 1033 | 0 | 1033 | 2352 | 73 | 1 |
| CVC4 | 0 | 1026 | 62852.199 | 62876.961 | 1026 | 0 | 1026 | 2359 | 76 | 0 |
| z3n | 0 | 1023 | 69545.364 | 69532.744 | 1023 | 0 | 1023 | 2362 | 101 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 3328 | 3205.756 | 2104.379 | 3328 | 2293 | 1035 | 57 | 57 | 0 | |
| Bitwuzla | 0 | 3310 | 2913.459 | 2923.184 | 3310 | 2277 | 1033 | 75 | 75 | 0 | |
| Bitwuzla-fixedn | 0 | 3310 | 2936.436 | 2929.131 | 3310 | 2277 | 1033 | 75 | 75 | 0 | |
| 2019-Boolectorn | 0 | 3306 | 2991.139 | 2982.312 | 3306 | 2275 | 1031 | 79 | 79 | 0 | |
| Yices2-fixedn | 0 | 3283 | 3528.368 | 3557.15 | 3283 | 2269 | 1014 | 102 | 102 | 0 | |
| Yices2 | 0 | 3283 | 3539.439 | 3557.732 | 3283 | 2269 | 1014 | 102 | 102 | 0 | |
| CVC4 | 0 | 3231 | 6248.407 | 6218.177 | 3231 | 2232 | 999 | 154 | 154 | 0 | |
| z3n | 0 | 3217 | 5664.53 | 5641.788 | 3217 | 2222 | 995 | 168 | 168 | 0 | |
| MathSAT5n | 0 | 3216 | 5929.565 | 5895.607 | 3216 | 2218 | 998 | 169 | 168 | 1 |
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.