The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_BV division in the Single Query Track.
Page generated on 2019-07-23 17:56:09 +0000
Benchmarks: 8909 Time Limit: 2400 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| Boolector | Poolector | Poolector | Poolector | Par4 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Boolector | 0 | 8751 | 593123.182 | 592976.764 | 8751 | 3071 | 5680 | 158 | 158 | 0 | |
| Yices 2.6.2 CaDiCal | 0 | 8718 | 660202.171 | 660060.442 | 8718 | 3053 | 5665 | 191 | 191 | 0 | |
| Poolector | 0 | 8685 | 903990.358 | 631227.578 | 8685 | 3033 | 5652 | 224 | 224 | 0 | |
| Par4 | 0 | 8684 | 764037.013 | 615686.559 | 8684 | 3045 | 5639 | 225 | 225 | 0 | |
| Yices 2.6.2 New Bvsolver | 0 | 8682 | 715513.665 | 715553.17 | 8682 | 3034 | 5648 | 227 | 227 | 0 | |
| Minkeyrink Solver | 0 | 8665 | 821185.831 | 821081.937 | 8665 | 3047 | 5618 | 244 | 244 | 0 | |
| 2018-Boolectorn | 0 | 8643 | 836115.435 | 836025.057 | 8643 | 2996 | 5647 | 266 | 266 | 0 | |
| Yices 2.6.2 Cryptominisat | 0 | 8638 | 904420.903 | 904177.225 | 8638 | 2996 | 5642 | 271 | 270 | 0 | |
| CVC4 | 0 | 8586 | 1089212.311 | 1088837.964 | 8586 | 3060 | 5526 | 323 | 312 | 4 | |
| Minkeyrink Solver MT | 0 | 8581 | 1086025.278 | 853664.695 | 8581 | 3015 | 5566 | 328 | 320 | 0 | |
| 2018-Minkeyrink MTn | 0 | 8565 | 1123067.167 | 894069.472 | 8565 | 3002 | 5563 | 344 | 337 | 0 | |
| Boolector-ReasonLSn | 0 | 8517 | 1423084.047 | 1423178.255 | 8517 | 2903 | 5614 | 392 | 391 | 0 | |
| Yices 2.6.2 | 0 | 8438 | 1375758.546 | 1375728.281 | 8438 | 3035 | 5403 | 471 | 471 | 0 | |
| STP-incremental | 0 | 8344 | 1871157.156 | 1872023.692 | 8344 | 2915 | 5429 | 565 | 562 | 0 | |
| STP | 0 | 8337 | 1865884.811 | 1866865.74 | 8337 | 2911 | 5426 | 572 | 569 | 0 | |
| STP-mergesat-fixedn | 0 | 8254 | 2206276.164 | 2207349.558 | 8254 | 2908 | 5346 | 655 | 652 | 0 | |
| STP-mt | 0 | 8161 | 2458813.263 | 1962289.182 | 8161 | 2849 | 5312 | 748 | 738 | 0 | |
| STP-minisat | 0 | 7780 | 3177982.896 | 3179120.189 | 7780 | 2826 | 4954 | 1129 | 1126 | 0 | |
| Z3n | 0 | 7694 | 3558041.055 | 3558049.027 | 7694 | 2790 | 4904 | 1215 | 1215 | 0 | |
| STP-portfolio-fixedn | 0 | 7484 | 3722715.286 | 3499112.702 | 7484 | 2766 | 4718 | 1425 | 1259 | 0 | |
| Yices 2.6.2 mcsat-bv | 0 | 5181 | 9404392.697 | 9405034.837 | 5181 | 1641 | 3540 | 3728 | 3593 | 134 | |
| STP-riss | 0 | 2682 | 55129.873 | 57163.521 | 2682 | 7 | 2675 | 6227 | 13 | 0 | |
| STP-mergesat | 0 | 2548 | 54161.244 | 55346.539 | 2548 | 7 | 2541 | 6361 | 13 | 0 | |
| STP-portfolio | 0 | 2548 | 3442094.429 | 3321325.603 | 2548 | 7 | 2541 | 6361 | 1181 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Poolector | 0 | 8768 | 1093383.208 | 530089.056 | 8768 | 3078 | 5690 | 141 | 141 | 0 | |
| Boolector | 0 | 8751 | 593150.512 | 592971.584 | 8751 | 3071 | 5680 | 158 | 158 | 0 | |
| Par4 | 0 | 8730 | 840952.893 | 567741.53 | 8730 | 3061 | 5669 | 179 | 179 | 0 | |
| Yices 2.6.2 CaDiCal | 0 | 8718 | 660229.751 | 660053.672 | 8718 | 3053 | 5665 | 191 | 191 | 0 | |
| Yices 2.6.2 New Bvsolver | 0 | 8682 | 715556.255 | 715544.03 | 8682 | 3034 | 5648 | 227 | 227 | 0 | |
| Minkeyrink Solver MT | 0 | 8667 | 1321390.108 | 759870.116 | 8667 | 3047 | 5620 | 242 | 234 | 0 | |
| Minkeyrink Solver | 0 | 8665 | 821227.621 | 821074.187 | 8665 | 3047 | 5618 | 244 | 244 | 0 | |
| 2018-Minkeyrink MTn | 0 | 8646 | 1327000.077 | 802191.144 | 8646 | 3032 | 5614 | 263 | 256 | 0 | |
| 2018-Boolectorn | 0 | 8643 | 836167.075 | 836015.557 | 8643 | 2996 | 5647 | 266 | 266 | 0 | |
| Yices 2.6.2 Cryptominisat | 0 | 8638 | 904474.613 | 904166.715 | 8638 | 2996 | 5642 | 271 | 270 | 0 | |
| CVC4 | 0 | 8586 | 1089282.411 | 1088825.654 | 8586 | 3060 | 5526 | 323 | 312 | 4 | |
| Boolector-ReasonLSn | 0 | 8517 | 1423150.187 | 1423162.935 | 8517 | 2903 | 5614 | 392 | 391 | 0 | |
| Yices 2.6.2 | 0 | 8438 | 1375826.986 | 1375712.481 | 8438 | 3035 | 5403 | 471 | 471 | 0 | |
| STP-mt | 0 | 8365 | 2981057.933 | 1729291.895 | 8365 | 2934 | 5431 | 544 | 534 | 0 | |
| STP-incremental | 0 | 8344 | 1871251.986 | 1872005.122 | 8344 | 2915 | 5429 | 565 | 562 | 0 | |
| STP | 0 | 8337 | 1866152.051 | 1866844.69 | 8337 | 2911 | 5426 | 572 | 569 | 0 | |
| STP-mergesat-fixedn | 0 | 8254 | 2206568.814 | 2207327.348 | 8254 | 2908 | 5346 | 655 | 652 | 0 | |
| STP-minisat | 0 | 7780 | 3178347.966 | 3179082.259 | 7780 | 2826 | 4954 | 1129 | 1126 | 0 | |
| Z3n | 0 | 7694 | 3558315.305 | 3558001.587 | 7694 | 2790 | 4904 | 1215 | 1215 | 0 | |
| STP-portfolio-fixedn | 0 | 7551 | 3783376.786 | 3466055.192 | 7551 | 2798 | 4753 | 1358 | 1191 | 0 | |
| Yices 2.6.2 mcsat-bv | 0 | 5181 | 9404928.717 | 9404914.607 | 5181 | 1641 | 3540 | 3728 | 3593 | 134 | |
| STP-riss | 0 | 2682 | 55309.263 | 57163.181 | 2682 | 7 | 2675 | 6227 | 13 | 0 | |
| STP-mergesat | 0 | 2548 | 54344.184 | 55346.059 | 2548 | 7 | 2541 | 6361 | 13 | 0 | |
| STP-portfolio | 0 | 2548 | 3467415.509 | 3306837.443 | 2548 | 7 | 2541 | 6361 | 1146 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Poolector | 0 | 3078 | 438355.315 | 145158.46 | 3078 | 3078 | 0 | 5831 | 141 | 0 |
| Boolector | 0 | 3071 | 176679.897 | 176536.66 | 3071 | 3071 | 0 | 5838 | 158 | 0 |
| Par4 | 0 | 3061 | 276742.106 | 150188.421 | 3061 | 3061 | 0 | 5848 | 179 | 0 |
| CVC4 | 0 | 3060 | 235704.509 | 235461.111 | 3060 | 3060 | 0 | 5849 | 312 | 4 |
| Yices 2.6.2 CaDiCal | 0 | 3053 | 184986.443 | 184856.164 | 3053 | 3053 | 0 | 5856 | 191 | 0 |
| Minkeyrink Solver MT | 0 | 3047 | 435207.89 | 204200.505 | 3047 | 3047 | 0 | 5862 | 234 | 0 |
| Minkeyrink Solver | 0 | 3047 | 229254.087 | 229205.08 | 3047 | 3047 | 0 | 5862 | 244 | 0 |
| Yices 2.6.2 | 0 | 3035 | 278569.066 | 278543.514 | 3035 | 3035 | 0 | 5874 | 471 | 0 |
| Yices 2.6.2 New Bvsolver | 0 | 3034 | 238308.93 | 238309.557 | 3034 | 3034 | 0 | 5875 | 227 | 0 |
| 2018-Minkeyrink MTn | 0 | 3032 | 450610.002 | 236162.043 | 3032 | 3032 | 0 | 5877 | 256 | 0 |
| 2018-Boolectorn | 0 | 2996 | 348134.384 | 348099.135 | 2996 | 2996 | 0 | 5913 | 266 | 0 |
| Yices 2.6.2 Cryptominisat | 0 | 2996 | 377258.544 | 376984.852 | 2996 | 2996 | 0 | 5913 | 270 | 0 |
| STP-mt | 0 | 2934 | 1079007.308 | 572695.333 | 2934 | 2934 | 0 | 5975 | 534 | 0 |
| STP-incremental | 0 | 2915 | 644719.44 | 645278.192 | 2915 | 2915 | 0 | 5994 | 562 | 0 |
| STP | 0 | 2911 | 635258.955 | 635924.968 | 2911 | 2911 | 0 | 5998 | 569 | 0 |
| STP-mergesat-fixedn | 0 | 2908 | 644452.097 | 645070.653 | 2908 | 2908 | 0 | 6001 | 652 | 0 |
| Boolector-ReasonLSn | 0 | 2903 | 836270.517 | 836467.787 | 2903 | 2903 | 0 | 6006 | 391 | 0 |
| STP-minisat | 0 | 2826 | 811345.848 | 811874.138 | 2826 | 2826 | 0 | 6083 | 1126 | 0 |
| STP-portfolio-fixedn | 0 | 2798 | 1096145.233 | 945644.345 | 2798 | 2798 | 0 | 6111 | 1191 | 0 |
| Z3n | 0 | 2790 | 1089388.13 | 1089230.125 | 2790 | 2790 | 0 | 6119 | 1215 | 0 |
| Yices 2.6.2 mcsat-bv | 0 | 1641 | 3703682.885 | 3703652.704 | 1641 | 1641 | 0 | 7268 | 3593 | 134 |
| STP-mergesat | 0 | 7 | 43068.286 | 43814.377 | 7 | 7 | 0 | 8902 | 13 | 0 |
| STP-riss | 0 | 7 | 43780.171 | 45101.62 | 7 | 7 | 0 | 8902 | 13 | 0 |
| STP-portfolio | 0 | 7 | 973373.55 | 898952.259 | 7 | 7 | 0 | 8902 | 1146 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Poolector | 0 | 5690 | 520627.893 | 250530.595 | 5690 | 0 | 5690 | 3219 | 141 | 0 |
| Boolector | 0 | 5680 | 282070.615 | 282034.924 | 5680 | 0 | 5680 | 3229 | 158 | 0 |
| Par4 | 0 | 5669 | 429810.787 | 283153.109 | 5669 | 0 | 5669 | 3240 | 179 | 0 |
| Yices 2.6.2 CaDiCal | 0 | 5665 | 340843.307 | 340797.508 | 5665 | 0 | 5665 | 3244 | 191 | 0 |
| Yices 2.6.2 New Bvsolver | 0 | 5648 | 342847.326 | 342834.473 | 5648 | 0 | 5648 | 3261 | 227 | 0 |
| 2018-Boolectorn | 0 | 5647 | 353632.69 | 353516.422 | 5647 | 0 | 5647 | 3262 | 266 | 0 |
| Yices 2.6.2 Cryptominisat | 0 | 5642 | 392816.069 | 392781.863 | 5642 | 0 | 5642 | 3267 | 270 | 0 |
| Minkeyrink Solver MT | 0 | 5620 | 751782.218 | 421269.611 | 5620 | 0 | 5620 | 3289 | 234 | 0 |
| Minkeyrink Solver | 0 | 5618 | 457573.534 | 457469.107 | 5618 | 0 | 5618 | 3291 | 244 | 0 |
| 2018-Minkeyrink MTn | 0 | 5614 | 741990.075 | 431629.1 | 5614 | 0 | 5614 | 3295 | 256 | 0 |
| Boolector-ReasonLSn | 0 | 5614 | 452479.67 | 452295.148 | 5614 | 0 | 5614 | 3295 | 391 | 0 |
| CVC4 | 0 | 5526 | 719177.902 | 718964.544 | 5526 | 0 | 5526 | 3383 | 312 | 4 |
| STP-mt | 0 | 5431 | 1767650.625 | 1022196.561 | 5431 | 0 | 5431 | 3478 | 534 | 0 |
| STP-incremental | 0 | 5429 | 1092132.546 | 1092326.93 | 5429 | 0 | 5429 | 3480 | 562 | 0 |
| STP | 0 | 5426 | 1096493.097 | 1096519.721 | 5426 | 0 | 5426 | 3483 | 569 | 0 |
| Yices 2.6.2 | 0 | 5403 | 962857.921 | 962768.966 | 5403 | 0 | 5403 | 3506 | 471 | 0 |
| STP-mergesat-fixedn | 0 | 5346 | 1427716.717 | 1427856.695 | 5346 | 0 | 5346 | 3563 | 652 | 0 |
| STP-minisat | 0 | 4954 | 2232602.118 | 2232808.121 | 4954 | 0 | 4954 | 3955 | 1126 | 0 |
| Z3n | 0 | 4904 | 2334527.175 | 2334371.462 | 4904 | 0 | 4904 | 4005 | 1215 | 0 |
| STP-portfolio-fixedn | 0 | 4753 | 2552831.553 | 2386010.847 | 4753 | 0 | 4753 | 4156 | 1191 | 0 |
| Yices 2.6.2 mcsat-bv | 0 | 3540 | 5566845.832 | 5566861.903 | 3540 | 0 | 3540 | 5369 | 3593 | 134 |
| STP-riss | 0 | 2675 | 10051.381 | 10365.081 | 2675 | 0 | 2675 | 6234 | 13 | 0 |
| STP-mergesat | 0 | 2541 | 9913.661 | 10169.042 | 2541 | 0 | 2541 | 6368 | 13 | 0 |
| STP-portfolio | 0 | 2541 | 2359641.959 | 2273485.184 | 2541 | 0 | 2541 | 6368 | 1146 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 8194 | 42231.538 | 26483.383 | 8194 | 2727 | 5467 | 715 | 715 | 0 | |
| Poolector | 0 | 8124 | 88009.535 | 37429.328 | 8124 | 2744 | 5380 | 785 | 785 | 0 | |
| Yices 2.6.2 New Bvsolver | 0 | 8100 | 29071.744 | 29044.283 | 8100 | 2675 | 5425 | 809 | 809 | 0 | |
| Boolector | 0 | 8077 | 38571.647 | 38428.277 | 8077 | 2706 | 5371 | 832 | 832 | 0 | |
| Yices 2.6.2 CaDiCal | 0 | 8052 | 30452.459 | 30372.569 | 8052 | 2684 | 5368 | 857 | 857 | 0 | |
| Minkeyrink Solver MT | 0 | 8038 | 60019.201 | 33890.259 | 8038 | 2727 | 5311 | 871 | 871 | 0 | |
| 2018-Minkeyrink MTn | 0 | 8018 | 59960.229 | 34522.524 | 8018 | 2706 | 5312 | 891 | 891 | 0 | |
| Minkeyrink Solver | 0 | 7985 | 36144.083 | 36022.984 | 7985 | 2673 | 5312 | 924 | 924 | 0 | |
| 2018-Boolectorn | 0 | 7705 | 41873.386 | 41768.305 | 7705 | 2344 | 5361 | 1204 | 1204 | 0 | |
| Yices 2.6.2 | 0 | 7668 | 37050.132 | 37001.149 | 7668 | 2542 | 5126 | 1241 | 1241 | 0 | |
| Yices 2.6.2 Cryptominisat | 0 | 7633 | 48382.595 | 48180.958 | 7633 | 2279 | 5354 | 1276 | 1276 | 0 | |
| CVC4 | 0 | 7124 | 71532.451 | 71195.964 | 7124 | 2178 | 4946 | 1785 | 1779 | 4 | |
| STP-mt | 0 | 6986 | 97515.748 | 63991.112 | 6986 | 2382 | 4604 | 1923 | 1923 | 0 | |
| Boolector-ReasonLSn | 0 | 6962 | 68178.871 | 68006.807 | 6962 | 1697 | 5265 | 1947 | 1947 | 0 | |
| STP | 0 | 6911 | 66713.136 | 66483.665 | 6911 | 2318 | 4593 | 1998 | 1998 | 0 | |
| STP-incremental | 0 | 6910 | 66356.012 | 66221.113 | 6910 | 2319 | 4591 | 1999 | 1999 | 0 | |
| STP-minisat | 0 | 6677 | 68567.199 | 68435.636 | 6677 | 2370 | 4307 | 2232 | 2232 | 0 | |
| STP-mergesat-fixedn | 0 | 6640 | 87238.381 | 86860.8 | 6640 | 2209 | 4431 | 2269 | 2269 | 0 | |
| STP-portfolio-fixedn | 0 | 6119 | 107244.346 | 93996.031 | 6119 | 2050 | 4069 | 2790 | 2626 | 0 | |
| Z3n | 0 | 5859 | 89765.661 | 89636.248 | 5859 | 1727 | 4132 | 3050 | 3050 | 0 | |
| Yices 2.6.2 mcsat-bv | 0 | 4388 | 113651.8 | 113615.392 | 4388 | 1214 | 3174 | 4521 | 4387 | 134 | |
| STP-riss | 0 | 2602 | 14339.451 | 14457.549 | 2602 | 7 | 2595 | 6307 | 169 | 0 | |
| STP-mergesat | 0 | 2468 | 13752.538 | 13652.834 | 2468 | 7 | 2461 | 6441 | 154 | 0 | |
| STP-portfolio | 0 | 2468 | 80514.605 | 75144.611 | 2468 | 7 | 2461 | 6441 | 2410 | 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.