SMT-COMP 2024

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2024

QF_BV (Single Query Track)

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

Results were generated on 2024-07-08

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
BitwuzlaBitwuzlaSTPBitwuzlaBitwuzla

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla010489136684.154526137761.630559104894907558221402113
STP010488169828.228527170916.15918104884919556921502120
Yices2010388142271.512368143339.280115103884862552631503123
cvc509958365361.544544366433.45916995847735185745071232
Z3-alpha09020391942.581441392924.1734999020442745931683016649
SMTInterpol03339552128.65738442522.5229735488422706715506317134

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla010489136684.154526137761.630559104894907558221402113
STP010488169828.228527170916.15918104884919556921502120
Yices2010388142271.512368143339.280115103884862552631503123
cvc509958365361.544544366433.45916995847735185745071232
Z3-alpha09020391942.581441392924.1734999020442745931683016649
SMTInterpol03548852576.881037651070.95202735488422706715506317134

SAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
STP0491958214.94955158719.496163491949190385746350
Bitwuzla0490764503.77927865008.447599490749070505746482
Yices20486264401.74531264902.948059486248620955746923
cvc504773125866.620821126372.253722477347730184574617013
Z3-alpha04427187187.975681187666.41690144274427053057465273
SMTInterpol0842161463.213932143147.0586818428420411557463454104

UNSAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla0558272180.37524872753.18296558205582755046741
STP05569111613.278976112196.663017556905569885046880
Yices20552677869.76705678436.33205655260552613150461310
cvc505185239494.923723240061.205438518505185472504645715
Z3-alpha04593204754.60576205257.7565984593045931064504610495
SMTInterpol02706691113.667105507923.89334627060270629515046279322

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla0977817874.33506718855.879781977845235255092500
Yices20974311024.84684112001.68132974344825261096000
STP0903523227.66697924136.9002219035458144540166800
cvc50835327196.66542628037.3971598353396643870235000
Z3-alpha0717015231.43419315953.9828527170358035900353300
SMTInterpol0203732731.16615113363.05227520373921645362830400