SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

ABVFP (Single Query Track)

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

Results were generated on 2025-08-11

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

Winners

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

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc5037615.13619.7737352230230
Bitwuzla02413.4716.402424036030
UltimateEliminator+MathSAT015147.18102.371515045000

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc5037615.13619.7737352230230
Bitwuzla02413.4716.402424036030
UltimateEliminator+MathSAT015147.18102.371515045000

SAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc503513.6017.913535012410
Bitwuzla02413.4716.4024240122400
UltimateEliminator+MathSAT015147.18102.3715150212400

UNSAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc502601.53601.8520205800
Bitwuzla000.000.0000025800
UltimateEliminator+MathSAT000.000.0000025800

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc503513.6017.913535002500
Bitwuzla02413.4716.402424033300
UltimateEliminator+MathSAT014119.5077.201414045100