SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_ABV (Unsat Core Track)

Competition results for the QF_ABV logic in the Unsat Core Track. Chart

Results were generated on 2025-08-11

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
BitwuzlaBitwuzla-BitwuzlaBitwuzla

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla01893163682.183913.5418551855100100
Yices2018227910856.8511085.6818511851140140
SMTInterpol01720156336.515147.621723172314201400
cvc501525846397.746628.3818521852130130

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla01893163682.183913.5418551855100100
Yices2018227910856.8511085.6818511851140140
SMTInterpol01720156336.515147.621723172314201400
cvc501525846397.746628.3818521852130130

UNSAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla01893163682.183913.5418551855100100
Yices2018227910856.8511085.6818511851140140
SMTInterpol01720156336.515147.621723172314201400
cvc501525846397.746628.3818521852130130

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla01792972109.662338.541837183702800
Yices201716331356.511580.821826182603900
SMTInterpol01540741746.391141.9117021702116200
cvc50141855532.50747.5617341734013100