SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Competitions by Year

SMT-COMP 2020

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

BV (Single Query Track)

Competition results for the BV division in the Single Query Track.

Page generated on 2020-07-04 11:46:58 +0000

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
CVC4CVC4CVC4 CVC4 CVC4

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 659 49658.532 45778.8136591964633737 0
CVC4 0 612 135421.639 138922.1616121674458484 0
Bitwuzla-fixedn 0 595 132010.761 126665.336595191404101101 0
z3n 0 576 144196.574 144217.607576173403120116 1
UltimateEliminator+MathSAT 0 227 126646.048 125544.922713214469103 0
Bitwuzla 40 569 108290.851 106379.01356918338612787 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 663 54497.472 43423.9356631984653333 0
CVC4 0 612 137860.739 138917.7116121674458484 0
Bitwuzla-fixedn 0 598 133286.041 125513.7565981934059898 0
z3n 0 576 144211.864 144213.127576173403120116 1
UltimateEliminator+MathSAT 0 227 126646.048 125544.922713214469103 0
Bitwuzla 40 571 108452.381 105260.36357118338812585 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 198 20522.286 14179.19198198049833 0
Bitwuzla-fixedn 0 193 25656.28 21863.603193193050398 0
z3n 0 173 39342.091 39342.391731730523116 1
CVC4 0 167 82986.999 83940.926167167052984 0
UltimateEliminator+MathSAT 0 13 74566.073 73996.17113130683103 0
Bitwuzla 14 183 13745.374 13484.816183183051385 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 465 23175.186 18444.745465046523133 0
CVC4 0 445 44073.741 44176.785445044525184 0
Bitwuzla-fixedn 0 405 96829.762 92850.154405040529198 0
z3n 0 403 94069.773 94070.7374030403293116 1
UltimateEliminator+MathSAT 0 214 49652.688 49132.1282140214482103 0
Bitwuzla 26 388 83907.007 80975.547388038830885 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 644 2652.822 1651.776441864585252 0
Bitwuzla-fixedn 0 565 4088.43 3645.216565181384131131 0
z3n 0 559 3606.942 3607.062559171388137136 1
CVC4 0 529 4660.844 4647.14152999430167167 0
UltimateEliminator+MathSAT 0 226 5009.976 4194.23322613213470109 0
Bitwuzla 40 552 3170.007 2858.553552181371144104 0

n Non-competing.