SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

BVFP (Single Query Track)

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

Results were generated on 2025-08-11

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

Winners

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

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla0194864.48888.7119418014140140
cvc501761502.841524.641761697320311
UltimateEliminator+MathSAT025295.52221.4025232183010

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla0194864.48888.7119418014140140
cvc501761502.841524.641761697320311
UltimateEliminator+MathSAT025295.52221.4025232183010

SAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla0180700.78723.28180180002800
cvc501691378.201399.1116916901128110
UltimateEliminator+MathSAT023247.10193.50232301572800

UNSAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla014163.69165.4314014019400
cvc507124.64125.53707719470
UltimateEliminator+MathSAT0248.4127.912021219400

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla019160.3384.011911791201700
cvc50172100.08121.20172167503600
UltimateEliminator+MathSAT022203.15136.3722202180600