SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_BV (Single Query Track)

Competition results for the QF_BV logic in the Single Query Track. Chart

Results were generated on 2025-08-11

Benchmarks: 10703
Time Limit: 1200 seconds
Memory Limit: 30720 GB

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
Bitwuzla-MachBVBitwuzla-MachBVBitwuzlaBitwuzla-MachBVBitwuzla-MachBV

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla-MachBV010523
(base +38)		97390.1498711.15105234929559418001791
Bitwuzla010498100202.01101517.47104984931556720502032
Yices2010491120555.40121864.36104914924556721202111
cvc509938302092.27303362.99993847905148765072732
z3siri09308
(base +364)		429081.45430296.0393084435487313950120411
Z3-alpha08970
(base +25)		544609.75144055.1393704592477813330125476
bv_decide-nokernel08862426162.80427483.9188624713414918410180237
Z3-Owl08656
(base +115)		345612.16346754.508656450141552047020319
bv_decide08638638058.46639387.5286384627401120650202537
SMTInterpol02917337337.08303061.00292559623297778068070
Bitwuzla-MachBV-base n010485113665.37114969.55104854928555721802135
Z3-alpha-base n08945389801.87390962.9089454467447817580174610
z3siri-base n08944391867.14393027.6189444467447717590174710
Z3-Owl-base n08541587768.50588896.668541428142602162021528
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla-MachBV010523
(base +38)		97390.1498711.15105234929559418001791
Bitwuzla010498100202.01101517.47104984931556720502032
Yices2010491120555.40121864.36104914924556721202111
cvc509938302092.27303362.99993847905148765072732
Z3-alpha09370
(base +425)		1532034.50393050.5293704592477813330125476
z3siri09308
(base +364)		429081.45430296.0393084435487313950120411
bv_decide-nokernel08862426162.80427483.9188624713414918410180237
Z3-Owl08656
(base +115)		345612.16346754.508656450141552047020319
bv_decide08638638058.46639387.5286384627401120650202537
SMTInterpol02925347054.64312426.58292559623297778068070
Bitwuzla-MachBV-base n010485113665.37114969.55104854928555721802135
Z3-alpha-base n08945389801.87390962.9089454467447817580174610
z3siri-base n08944391867.14393027.6189444467447717590174710
Z3-Owl-base n08541587768.50588896.668541428142602162021528
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver

SAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla0493144557.4845173.98493149310315741292
Bitwuzla-MachBV04929
(base +1)		50034.8650653.33492949290335741321
Yices20492450873.5151487.19492449240385741371
cvc504790109431.02110037.61479047900172574115711
bv_decide-nokernel04713210107.19210776.1147134713024957412444
bv_decide04627290823.50291487.4146274627033557413313
Z3-alpha04592
(base +125)		681224.03176140.6345924592037057413619
Z3-Owl04501
(base +220)		161409.09162001.1145014501046157414544
z3siri04435
(base -32)		209098.46209677.2544354435052757414259
SMTInterpol0596127475.21116503.2959659604366574136840
Bitwuzla-MachBV-base n0492853134.8153747.05492849280345741295
Z3-alpha-base n04467199624.27200203.8444674467049557414896
z3siri-base n04467201216.42201797.3844674467049557414896
Z3-Owl-base n04281326455.94327025.0242814281068157416756
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver

UNSAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla-MachBV05594
(base +37)		47355.2848057.82559405594525057520
Bitwuzla0556755644.5356343.49556705567795057790
Yices20556769681.8970377.17556705567795057790
cvc505148192661.24193325.38514805148498505748115
z3siri04873
(base +396)		219982.99220618.7848730487377350576862
Z3-alpha04778
(base +300)		850810.48216909.89477804778868505782936
Z3-Owl04155
(base -105)		184203.06184753.394155041551491505714880
bv_decide-nokernel04149216055.61216707.8041490414914975057146432
bv_decide04011347234.96347900.1140110401116355057159934
SMTInterpol02329219579.43195923.302329023293317505730510
Bitwuzla-MachBV-base n0555760530.5561222.50555705557895057890
Z3-alpha-base n04478190177.61190759.064478044781168505711642
z3siri-base n04477190650.72191230.234477044771169505711652
Z3-Owl-base n04260261312.56261871.644260042601386505713831
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla-MachBV010101
(base +118)		17784.1719040.531010147435358060200
Bitwuzla01001914109.7015349.901001947285291068400
Yices20990911127.2912349.05990945895320079400
cvc50849824252.3425300.078498400544931220400
Z3-alpha07734
(base +383)		70113.7221374.057734379539390296900
z3siri07387
(base +43)		19789.8820708.357387348739008330800
Z3-Owl06983
(base +512)		33022.6833910.416983351934640372000
bv_decide-nokernel0604934413.1535348.336049318128681465300
bv_decide0569437930.6738815.865694301026841500800
SMTInterpol0196521583.019183.1719652871678423831500
Bitwuzla-MachBV-base n0998316027.7717255.32998347165267072000
Z3-alpha-base n0735117648.2918560.457351361537360335200
z3siri-base n0734417741.4118651.467344361237320335900
Z3-Owl-base n0647122159.5022960.326471316933020423200
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver