SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_Equality_Bitvec (Model Validation Track)

Competition results for the QF_Equality_Bitvec division in the Model Validation Track. Chart

Results were generated on 2025-08-11

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

Logics:

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
BitwuzlaBitwuzlaBitwuzla-Yices2

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATUnsolvedAbstainedTimeoutMemout
Bitwuzla04739788.519848.534734732020
Yices2047321591.4321652.994734732020
SMTInterpol031324034.2819084.403133131620400
cvc501503950.163969.0915015032503250

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATUnsolvedAbstainedTimeoutMemout
Bitwuzla04739788.519848.534734732020
Yices2047321591.4321652.994734732020
SMTInterpol031324034.2819084.403133131620400
cvc501503950.163969.0915015032503250

SAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATUnsolvedAbstainedTimeoutMemout
Bitwuzla04739788.519848.534734732020
Yices2047321591.4321652.994734732020
SMTInterpol031324034.2819084.403133131620400
cvc501503950.163969.0915015032503250

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATUnsolvedAbstainedTimeoutMemout
Yices203811028.541075.6638138109400
Bitwuzla03651046.241091.23365365011000
SMTInterpol02294377.911810.412292295818800
cvc5013286.33102.39132132034300