SMT-COMP 2019

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Papers
Benchmark Submission
Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

Previous Competitions

SMT-LIB

QF_BV (Single Query Track)

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
BoolectorPoolectorPoolector Poolector Par4

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Boolector 0 8751 593123.182 592976.764875130715680158158 0
Yices 2.6.2 CaDiCal 0 8718 660202.171 660060.442871830535665191191 0
Poolector 0 8685 903990.358 631227.578868530335652224224 0
Par4 0 8684 764037.013 615686.559868430455639225225 0
Yices 2.6.2 New Bvsolver 0 8682 715513.665 715553.17868230345648227227 0
Minkeyrink Solver 0 8665 821185.831 821081.937866530475618244244 0
2018-Boolectorn 0 8643 836115.435 836025.057864329965647266266 0
Yices 2.6.2 Cryptominisat 0 8638 904420.903 904177.225863829965642271270 0
CVC4 0 8586 1089212.311 1088837.964858630605526323312 4
Minkeyrink Solver MT 0 8581 1086025.278 853664.695858130155566328320 0
2018-Minkeyrink MTn 0 8565 1123067.167 894069.472856530025563344337 0
Boolector-ReasonLSn 0 8517 1423084.047 1423178.255851729035614392391 0
Yices 2.6.2 0 8438 1375758.546 1375728.281843830355403471471 0
STP-incremental 0 8344 1871157.156 1872023.692834429155429565562 0
STP 0 8337 1865884.811 1866865.74833729115426572569 0
STP-mergesat-fixedn 0 8254 2206276.164 2207349.558825429085346655652 0
STP-mt 0 8161 2458813.263 1962289.182816128495312748738 0
STP-minisat 0 7780 3177982.896 3179120.18977802826495411291126 0
Z3n 0 7694 3558041.055 3558049.02776942790490412151215 0
STP-portfolio-fixedn 0 7484 3722715.286 3499112.70274842766471814251259 0
Yices 2.6.2 mcsat-bv 0 5181 9404392.697 9405034.83751811641354037283593 134
STP-riss 0 2682 55129.873 57163.521268272675622713 0
STP-mergesat 0 2548 54161.244 55346.539254872541636113 0
STP-portfolio 0 2548 3442094.429 3321325.60325487254163611181 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Poolector 0 8768 1093383.208 530089.056876830785690141141 0
Boolector 0 8751 593150.512 592971.584875130715680158158 0
Par4 0 8730 840952.893 567741.53873030615669179179 0
Yices 2.6.2 CaDiCal 0 8718 660229.751 660053.672871830535665191191 0
Yices 2.6.2 New Bvsolver 0 8682 715556.255 715544.03868230345648227227 0
Minkeyrink Solver MT 0 8667 1321390.108 759870.116866730475620242234 0
Minkeyrink Solver 0 8665 821227.621 821074.187866530475618244244 0
2018-Minkeyrink MTn 0 8646 1327000.077 802191.144864630325614263256 0
2018-Boolectorn 0 8643 836167.075 836015.557864329965647266266 0
Yices 2.6.2 Cryptominisat 0 8638 904474.613 904166.715863829965642271270 0
CVC4 0 8586 1089282.411 1088825.654858630605526323312 4
Boolector-ReasonLSn 0 8517 1423150.187 1423162.935851729035614392391 0
Yices 2.6.2 0 8438 1375826.986 1375712.481843830355403471471 0
STP-mt 0 8365 2981057.933 1729291.895836529345431544534 0
STP-incremental 0 8344 1871251.986 1872005.122834429155429565562 0
STP 0 8337 1866152.051 1866844.69833729115426572569 0
STP-mergesat-fixedn 0 8254 2206568.814 2207327.348825429085346655652 0
STP-minisat 0 7780 3178347.966 3179082.25977802826495411291126 0
Z3n 0 7694 3558315.305 3558001.58776942790490412151215 0
STP-portfolio-fixedn 0 7551 3783376.786 3466055.19275512798475313581191 0
Yices 2.6.2 mcsat-bv 0 5181 9404928.717 9404914.60751811641354037283593 134
STP-riss 0 2682 55309.263 57163.181268272675622713 0
STP-mergesat 0 2548 54344.184 55346.059254872541636113 0
STP-portfolio 0 2548 3467415.509 3306837.44325487254163611146 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Poolector 0 3078 438355.315 145158.463078307805831141 0
Boolector 0 3071 176679.897 176536.663071307105838158 0
Par4 0 3061 276742.106 150188.4213061306105848179 0
CVC4 0 3060 235704.509 235461.1113060306005849312 4
Yices 2.6.2 CaDiCal 0 3053 184986.443 184856.1643053305305856191 0
Minkeyrink Solver MT 0 3047 435207.89 204200.5053047304705862234 0
Minkeyrink Solver 0 3047 229254.087 229205.083047304705862244 0
Yices 2.6.2 0 3035 278569.066 278543.5143035303505874471 0
Yices 2.6.2 New Bvsolver 0 3034 238308.93 238309.5573034303405875227 0
2018-Minkeyrink MTn 0 3032 450610.002 236162.0433032303205877256 0
2018-Boolectorn 0 2996 348134.384 348099.1352996299605913266 0
Yices 2.6.2 Cryptominisat 0 2996 377258.544 376984.8522996299605913270 0
STP-mt 0 2934 1079007.308 572695.3332934293405975534 0
STP-incremental 0 2915 644719.44 645278.1922915291505994562 0
STP 0 2911 635258.955 635924.9682911291105998569 0
STP-mergesat-fixedn 0 2908 644452.097 645070.6532908290806001652 0
Boolector-ReasonLSn 0 2903 836270.517 836467.7872903290306006391 0
STP-minisat 0 2826 811345.848 811874.13828262826060831126 0
STP-portfolio-fixedn 0 2798 1096145.233 945644.34527982798061111191 0
Z3n 0 2790 1089388.13 1089230.12527902790061191215 0
Yices 2.6.2 mcsat-bv 0 1641 3703682.885 3703652.70416411641072683593 134
STP-mergesat 0 7 43068.286 43814.377770890213 0
STP-riss 0 7 43780.171 45101.62770890213 0
STP-portfolio 0 7 973373.55 898952.25977089021146 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Poolector 0 5690 520627.893 250530.5955690056903219141 0
Boolector 0 5680 282070.615 282034.9245680056803229158 0
Par4 0 5669 429810.787 283153.1095669056693240179 0
Yices 2.6.2 CaDiCal 0 5665 340843.307 340797.5085665056653244191 0
Yices 2.6.2 New Bvsolver 0 5648 342847.326 342834.4735648056483261227 0
2018-Boolectorn 0 5647 353632.69 353516.4225647056473262266 0
Yices 2.6.2 Cryptominisat 0 5642 392816.069 392781.8635642056423267270 0
Minkeyrink Solver MT 0 5620 751782.218 421269.6115620056203289234 0
Minkeyrink Solver 0 5618 457573.534 457469.1075618056183291244 0
2018-Minkeyrink MTn 0 5614 741990.075 431629.15614056143295256 0
Boolector-ReasonLSn 0 5614 452479.67 452295.1485614056143295391 0
CVC4 0 5526 719177.902 718964.5445526055263383312 4
STP-mt 0 5431 1767650.625 1022196.5615431054313478534 0
STP-incremental 0 5429 1092132.546 1092326.935429054293480562 0
STP 0 5426 1096493.097 1096519.7215426054263483569 0
Yices 2.6.2 0 5403 962857.921 962768.9665403054033506471 0
STP-mergesat-fixedn 0 5346 1427716.717 1427856.6955346053463563652 0
STP-minisat 0 4954 2232602.118 2232808.12149540495439551126 0
Z3n 0 4904 2334527.175 2334371.46249040490440051215 0
STP-portfolio-fixedn 0 4753 2552831.553 2386010.84747530475341561191 0
Yices 2.6.2 mcsat-bv 0 3540 5566845.832 5566861.90335400354053693593 134
STP-riss 0 2675 10051.381 10365.081267502675623413 0
STP-mergesat 0 2541 9913.661 10169.042254102541636813 0
STP-portfolio 0 2541 2359641.959 2273485.18425410254163681146 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 8194 42231.538 26483.383819427275467715715 0
Poolector 0 8124 88009.535 37429.328812427445380785785 0
Yices 2.6.2 New Bvsolver 0 8100 29071.744 29044.283810026755425809809 0
Boolector 0 8077 38571.647 38428.277807727065371832832 0
Yices 2.6.2 CaDiCal 0 8052 30452.459 30372.569805226845368857857 0
Minkeyrink Solver MT 0 8038 60019.201 33890.259803827275311871871 0
2018-Minkeyrink MTn 0 8018 59960.229 34522.524801827065312891891 0
Minkeyrink Solver 0 7985 36144.083 36022.984798526735312924924 0
2018-Boolectorn 0 7705 41873.386 41768.30577052344536112041204 0
Yices 2.6.2 0 7668 37050.132 37001.14976682542512612411241 0
Yices 2.6.2 Cryptominisat 0 7633 48382.595 48180.95876332279535412761276 0
CVC4 0 7124 71532.451 71195.96471242178494617851779 4
STP-mt 0 6986 97515.748 63991.11269862382460419231923 0
Boolector-ReasonLSn 0 6962 68178.871 68006.80769621697526519471947 0
STP 0 6911 66713.136 66483.66569112318459319981998 0
STP-incremental 0 6910 66356.012 66221.11369102319459119991999 0
STP-minisat 0 6677 68567.199 68435.63666772370430722322232 0
STP-mergesat-fixedn 0 6640 87238.381 86860.866402209443122692269 0
STP-portfolio-fixedn 0 6119 107244.346 93996.03161192050406927902626 0
Z3n 0 5859 89765.661 89636.24858591727413230503050 0
Yices 2.6.2 mcsat-bv 0 4388 113651.8 113615.39243881214317445214387 134
STP-riss 0 2602 14339.451 14457.5492602725956307169 0
STP-mergesat 0 2468 13752.538 13652.8342468724616441154 0
STP-portfolio 0 2468 80514.605 75144.61124687246164412410 0

n Non-competing.