SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2019

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

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 UNSATUnsolvedAbstainedTimeout 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 ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
Poolector 0 87681093383.208530089.056876830785690141141 0
Boolector 0 8751593150.512592971.584875130715680158158 0
Par4 0 8730840952.893567741.53873030615669179179 0
Yices 2.6.2 CaDiCal 0 8718660229.751660053.672871830535665191191 0
Yices 2.6.2 New Bvsolver 0 8682715556.255715544.03868230345648227227 0
Minkeyrink Solver MT 0 86671321390.108759870.116866730475620242234 0
Minkeyrink Solver 0 8665821227.621821074.187866530475618244244 0
2018-Minkeyrink MTn 0 86461327000.077802191.144864630325614263256 0
2018-Boolectorn 0 8643836167.075836015.557864329965647266266 0
Yices 2.6.2 Cryptominisat 0 8638904474.613904166.715863829965642271270 0
CVC4 0 85861089282.4111088825.654858630605526323312 4
Boolector-ReasonLSn 0 85171423150.1871423162.935851729035614392391 0
Yices 2.6.2 0 84381375826.9861375712.481843830355403471471 0
STP-mt 0 83652981057.9331729291.895836529345431544534 0
STP-incremental 0 83441871251.9861872005.122834429155429565562 0
STP 0 83371866152.0511866844.69833729115426572569 0
STP-mergesat-fixedn 0 82542206568.8142207327.348825429085346655652 0
STP-minisat 0 77803178347.9663179082.25977802826495411291126 0
Z3n 0 76943558315.3053558001.58776942790490412151215 0
STP-portfolio-fixedn 0 75513783376.7863466055.19275512798475313581191 0
Yices 2.6.2 mcsat-bv 0 51819404928.7179404914.60751811641354037283593 134
STP-riss 0 268255309.26357163.181268272675622713 0
STP-mergesat 0 254854344.18455346.059254872541636113 0
STP-portfolio 0 25483467415.5093306837.44325487254163611146 0

SAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Poolector 0 3078438355.315145158.463078307805831141 0
Boolector 0 3071176679.897176536.663071307105838158 0
Par4 0 3061276742.106150188.4213061306105848179 0
CVC4 0 3060235704.509235461.1113060306005849312 4
Yices 2.6.2 CaDiCal 0 3053184986.443184856.1643053305305856191 0
Minkeyrink Solver MT 0 3047435207.89204200.5053047304705862234 0
Minkeyrink Solver 0 3047229254.087229205.083047304705862244 0
Yices 2.6.2 0 3035278569.066278543.5143035303505874471 0
Yices 2.6.2 New Bvsolver 0 3034238308.93238309.5573034303405875227 0
2018-Minkeyrink MTn 0 3032450610.002236162.0433032303205877256 0
2018-Boolectorn 0 2996348134.384348099.1352996299605913266 0
Yices 2.6.2 Cryptominisat 0 2996377258.544376984.8522996299605913270 0
STP-mt 0 29341079007.308572695.3332934293405975534 0
STP-incremental 0 2915644719.44645278.1922915291505994562 0
STP 0 2911635258.955635924.9682911291105998569 0
STP-mergesat-fixedn 0 2908644452.097645070.6532908290806001652 0
Boolector-ReasonLSn 0 2903836270.517836467.7872903290306006391 0
STP-minisat 0 2826811345.848811874.13828262826060831126 0
STP-portfolio-fixedn 0 27981096145.233945644.34527982798061111191 0
Z3n 0 27901089388.131089230.12527902790061191215 0
Yices 2.6.2 mcsat-bv 0 16413703682.8853703652.70416411641072683593 134
STP-mergesat 0 743068.28643814.377770890213 0
STP-riss 0 743780.17145101.62770890213 0
STP-portfolio 0 7973373.55898952.25977089021146 0

UNSAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Poolector 0 5690520627.893250530.5955690056903219141 0
Boolector 0 5680282070.615282034.9245680056803229158 0
Par4 0 5669429810.787283153.1095669056693240179 0
Yices 2.6.2 CaDiCal 0 5665340843.307340797.5085665056653244191 0
Yices 2.6.2 New Bvsolver 0 5648342847.326342834.4735648056483261227 0
2018-Boolectorn 0 5647353632.69353516.4225647056473262266 0
Yices 2.6.2 Cryptominisat 0 5642392816.069392781.8635642056423267270 0
Minkeyrink Solver MT 0 5620751782.218421269.6115620056203289234 0
Minkeyrink Solver 0 5618457573.534457469.1075618056183291244 0
2018-Minkeyrink MTn 0 5614741990.075431629.15614056143295256 0
Boolector-ReasonLSn 0 5614452479.67452295.1485614056143295391 0
CVC4 0 5526719177.902718964.5445526055263383312 4
STP-mt 0 54311767650.6251022196.5615431054313478534 0
STP-incremental 0 54291092132.5461092326.935429054293480562 0
STP 0 54261096493.0971096519.7215426054263483569 0
Yices 2.6.2 0 5403962857.921962768.9665403054033506471 0
STP-mergesat-fixedn 0 53461427716.7171427856.6955346053463563652 0
STP-minisat 0 49542232602.1182232808.12149540495439551126 0
Z3n 0 49042334527.1752334371.46249040490440051215 0
STP-portfolio-fixedn 0 47532552831.5532386010.84747530475341561191 0
Yices 2.6.2 mcsat-bv 0 35405566845.8325566861.90335400354053693593 134
STP-riss 0 267510051.38110365.081267502675623413 0
STP-mergesat 0 25419913.66110169.042254102541636813 0
STP-portfolio 0 25412359641.9592273485.18425410254163681146 0

24 seconds Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
Par4 0 819442231.53826483.383819427275467715715 0
Poolector 0 812488009.53537429.328812427445380785785 0
Yices 2.6.2 New Bvsolver 0 810029071.74429044.283810026755425809809 0
Boolector 0 807738571.64738428.277807727065371832832 0
Yices 2.6.2 CaDiCal 0 805230452.45930372.569805226845368857857 0
Minkeyrink Solver MT 0 803860019.20133890.259803827275311871871 0
2018-Minkeyrink MTn 0 801859960.22934522.524801827065312891891 0
Minkeyrink Solver 0 798536144.08336022.984798526735312924924 0
2018-Boolectorn 0 770541873.38641768.30577052344536112041204 0
Yices 2.6.2 0 766837050.13237001.14976682542512612411241 0
Yices 2.6.2 Cryptominisat 0 763348382.59548180.95876332279535412761276 0
CVC4 0 712471532.45171195.96471242178494617851779 4
STP-mt 0 698697515.74863991.11269862382460419231923 0
Boolector-ReasonLSn 0 696268178.87168006.80769621697526519471947 0
STP 0 691166713.13666483.66569112318459319981998 0
STP-incremental 0 691066356.01266221.11369102319459119991999 0
STP-minisat 0 667768567.19968435.63666772370430722322232 0
STP-mergesat-fixedn 0 664087238.38186860.866402209443122692269 0
STP-portfolio-fixedn 0 6119107244.34693996.03161192050406927902626 0
Z3n 0 585989765.66189636.24858591727413230503050 0
Yices 2.6.2 mcsat-bv 0 4388113651.8113615.39243881214317445214387 134
STP-riss 0 260214339.45114457.5492602725956307169 0
STP-mergesat 0 246813752.53813652.8342468724616441154 0
STP-portfolio 0 246880514.60575144.61124687246164412410 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.