SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2022

Rules
Benchmarks
Tools
Specs
Proof Exhibition Track
Parallel & Cloud Tracks
Participants
Results
Statistics
Comparisons
Slides

Bitvec (Single Query Track)

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

Page generated on 2022-08-10 11:17:44 +0000

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

Logics:

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
cvc5cvc5cvc5 cvc5 Q3B

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
2019-Par4n 0 884 115396.641 106482.18488424164386086 0
cvc5 0 854 159378.113 165480.2058542316231160116 0
Q3B 0 832 170169.933 166765.1398322286041380135 0
z3-4.8.17n 0 775 232309.365 232323.7937752125631950182 2
Bitwuzla 0 759 251975.775 251990.2837592075522110197 0
Q3B-pBDD 0 753 272789.717 270834.8637531845692170214 0
YicesQS 0 708 318217.125 318269.9857081925162620262 0
UltimateEliminator+MathSAT 0 304 206470.961 204316.516304272776660137 22

Parallel Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
2019-Par4n 0 894126521.801100383.77789424465076076 0
cvc5 0 854164783.792165475.4358542316231160116 0
Q3B 0 835173630.993165779.9238352286071350132 0
z3-4.8.17n 0 775232351.965232315.7437752125631950182 2
Bitwuzla 0 759252001.465251982.5737592075522110197 0
Q3B-pBDD 0 754272853.117270065.627541845702160213 0
YicesQS 0 708318262.215318260.6357081925162620262 0
UltimateEliminator+MathSAT 0 304206554.511204316.276304272776660137 22

SAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
2019-Par4n 0 24433317.72622825.98124424401671076 0
cvc5 0 23152530.48953074.316231231029710116 0
Q3B 0 22840705.42939151.001228228032710132 0
z3-4.8.17n 0 21252689.53752690.324212212048710182 2
Bitwuzla 0 20753987.65153986.379207207053710197 0
YicesQS 0 19283158.83683158.062192192068710262 0
Q3B-pBDD 0 184101080.024100168.464184184076710213 0
UltimateEliminator+MathSAT 0 27121779.362120767.22527270233710137 22

UNSAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
2019-Par4n 0 65062004.07546357.79665006503428676 0
cvc5 0 62381053.30481201.119623062361286116 0
Q3B 0 607101725.56495428.922607060777286132 0
Q3B-pBDD 0 570140573.093138697.1565700570114286213 0
z3-4.8.17n 0 563148462.427148425.4185630563121286182 2
Bitwuzla 0 552166813.815166796.1945520552132286197 0
YicesQS 0 516203903.38203902.5735160516168286262 0
UltimateEliminator+MathSAT 0 27757132.97155918.3652770277407286137 22

24 seconds Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
2019-Par4n 0 8614683.6843203.5438612316301090109 0
Q3B 0 8025510.2744597.9638022105921680167 0
z3-4.8.17n 0 7385971.4495970.7047382075312320230 2
Q3B-pBDD 0 7157170.0956616.717151555602550254 0
cvc5 0 7057313.7257303.07051295762650265 0
Bitwuzla 0 7007040.5457019.8147001835172700256 0
YicesQS 0 6877014.6447012.6876871845032830283 0
UltimateEliminator+MathSAT 0 2909529.9427741.171290202706800182 22

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.