SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

ABV (Unsat Core Track)

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

Results were generated on 2025-08-11

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

Winners

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

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved UNSATUnsolvedAbstainedTimeoutMemout
SMTInterpol07943580.542661.5028228218090
cvc5039427100.1327141.822992991010
Bitwuzla011211.1914.902929271030
UltimateEliminator+MathSAT000.000.0000300000

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved UNSATUnsolvedAbstainedTimeoutMemout
SMTInterpol07943580.542661.5028228218090
cvc5039427100.1327141.822992991010
Bitwuzla011211.1914.902929271030
UltimateEliminator+MathSAT000.000.0000300000

UNSAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved UNSATUnsolvedAbstainedTimeoutMemout
SMTInterpol07943580.542661.5028228218090
cvc5039427100.1327141.822992991010
Bitwuzla011211.1914.902929271030
UltimateEliminator+MathSAT000.000.0000300000

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved UNSATUnsolvedAbstainedTimeoutMemout
SMTInterpol0757398.82250.4627327381900
cvc5022953.2167.63116116018400
Bitwuzla011211.1914.902929268300
UltimateEliminator+MathSAT000.000.0000300000