SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2020

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 2020-07-04 11:46:59 +0000

Benchmarks: 6861
Time Limit: 1200 seconds
Memory Limit: 60 GB

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
BitwuzlaBitwuzlaBitwuzla Bitwuzla Bitwuzla

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Bitwuzla-fixedn 0 6731 275993.133 275773.208673125294202130130 0
Bitwuzla 0 6730 276329.653 276080.188673025284202131131 0
Yices2-fixedn 0 6719 284359.239 284018.222671925204199142142 0
2019-Boolectorn 0 6710 310011.466 309790.697671025234187151151 0
2019-Poolectorn 0 6632 484753.535 328685.732663224774155229229 0
MinkeyRink-fixedn 0 6610 470014.391 341671.944661024884122251244 0
STP + CMS 0 6580 546415.328 391932.497658024234157281273 0
CVC4 0 6329 911591.33 911144.212632924773852532526 3
MathSAT5n 0 5967 1388776.257 1388624.33596721923775894893 0
z3n 0 5905 1544650.759 1544542.384590523413564956956 0
LazyBV2Int 0 3248 4595944.878 4596409.4333248561268736133612 2
MinkeyRink 0 2120 9364.511 9311.779212011210947410 0
STP + MergeSAT 2 6633 439359.742 439590.458663324594174228224 0
Yices2 32 6578 402038.802 401885.717657823984180283251 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Bitwuzla-fixedn 0 6731 276009.913 275768.178673125294202130130 0
Bitwuzla 0 6730 276345.813 276075.568673025284202131131 0
2019-Poolectorn 0 6721 601905.825 278442.308672125244197140140 0
Yices2-fixedn 0 6719 284373.409 284013.912671925204199142142 0
2019-Boolectorn 0 6710 310030.086 309784.927671025234187151151 0
MinkeyRink-fixedn 0 6690 561747.841 294426.483669025284162171164 0
STP + CMS 0 6689 642484.468 319011.01668925034186172164 0
CVC4 0 6329 911688.83 911121.552632924773852532526 3
MathSAT5n 0 5967 1388964.657 1388584.66596721923775894893 0
z3n 0 5905 1544785.719 1544502.874590523413564956956 0
LazyBV2Int 0 3247 4596373.638 4596276.6133247560268736143612 2
MinkeyRink 0 2120 9364.511 9311.779212011210947410 0
STP + MergeSAT 2 6633 439386.662 439583.558663324594174228224 0
Yices2 32 6578 402053.912 401879.167657823984180283251 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Bitwuzla-fixedn 0 2529 102591.669 102421.8212529252904332130 0
MinkeyRink-fixedn 0 2528 224141.6 88953.4532528252804333164 0
Bitwuzla 0 2528 102851.034 102706.2492528252804333131 0
2019-Poolectorn 0 2524 285094.752 105528.6722524252404337140 0
2019-Boolectorn 0 2523 116830.844 116658.8912523252304338151 0
Yices2-fixedn 0 2520 108990.017 108753.12520252004341142 0
STP + CMS 0 2503 341801.786 141324.1332503250304358164 0
CVC4 0 2477 221216.036 220926.5662477247704384526 3
STP + MergeSAT 0 2459 203940.205 204383.1862459245904402224 0
z3n 0 2341 491381.274 491312.4922341234104520956 0
MathSAT5n 0 2192 604638.661 604392.1192192219204669893 0
LazyBV2Int 0 560 2573664.914 2573681.176560560063013612 2
MinkeyRink 0 11 7036.84 6987.7321111068500 0
Yices2 32 2398 207402.541 207339.8252398239804463251 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Bitwuzla-fixedn 0 4202 127818.244 127746.3574202042022659130 0
Bitwuzla 0 4202 127894.779 127769.3184202042022659131 0
Yices2-fixedn 0 4199 129783.392 129660.8124199041992662142 0
2019-Poolectorn 0 4197 271211.074 127313.6364197041972664140 0
2019-Boolectorn 0 4187 147599.242 147526.0364187041872674151 0
STP + CMS 0 4186 255082.681 132086.8774186041862675164 0
Yices2 0 4180 149051.371 148939.3424180041802681251 0
MinkeyRink-fixedn 0 4162 292006.241 159873.034162041622699164 0
CVC4 0 3852 644872.794 644594.9863852038523009526 3
MathSAT5n 0 3775 738725.996 738592.5413775037753086893 0
z3n 0 3564 1007804.445 1007590.3823564035643297956 0
LazyBV2Int 0 2687 1977108.723 1976995.43626870268741743612 2
MinkeyRink 0 2109 1918.408 1914.52721090210947520 0
STP + MergeSAT 2 4174 189846.457 189600.3734174041742687224 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Poolectorn 0 6211 72668.191 30874.689621122463965650650 0
MinkeyRink-fixedn 0 6201 42927.466 25104.899620122553946660660 0
Bitwuzla 0 6190 32777.904 32530.517619022303960671671 0
Bitwuzla-fixedn 0 6190 32790.103 32597.973619022293961671671 0
Yices2-fixedn 0 6182 24605.956 24517.889618221684014679679 0
2019-Boolectorn 0 6181 31794.444 31669.739618122233958680680 0
STP + CMS 0 6082 45870.656 29734.296608221493933779779 0
STP + MergeSAT 0 5967 38364.565 38117.104596721393828894894 0
CVC4 0 5005 68528.063 68179.95750051727327818561853 3
MathSAT5n 0 4873 60047.395 59892.88648731552332119881988 0
z3n 0 4448 72205.017 71999.2244481487296124132413 0
LazyBV2Int 0 2323 113185.778 113123.0742323164215945384536 2
MinkeyRink 0 2120 5852.929 5799.1392120112109474137 0
Yices2 32 6089 25474.635 25380.35608920844005772740 0

n Non-competing.