SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_ABV (Model Validation Track)

Competition results for the QF_ABV logic in the Model Validation Track. Chart

Results were generated on 2025-08-11

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

Winners

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

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATUnsolvedAbstainedTimeoutMemout
Bitwuzla052012609.083240.725201520113031
cvc50474967426.4868017.844749474946504585
SMTInterpol03875304943.37269652.26388738871327012470

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATUnsolvedAbstainedTimeoutMemout
Bitwuzla052012609.083240.725201520113031
cvc50474967426.4868017.844749474946504585
SMTInterpol03887319558.12283788.03388738871327012470

SAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATUnsolvedAbstainedTimeoutMemout
Bitwuzla052012609.083240.725201520113031
cvc50474967426.4868017.844749474946504585
SMTInterpol03887319558.12283788.03388738871327012470

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATUnsolvedAbstainedTimeoutMemout
Bitwuzla051881270.071899.795188518862000
cvc5042025723.206237.62420242022101000
SMTInterpol0284213491.055892.832842284231234100