SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

UFLRA (Single Query Track)

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

Results were generated on 2025-08-11

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

Winners

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

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc5020.340.592025030
SMTInterpol020.940.942025040
iProver v3.9.30248.9914.822025040
UltimateEliminator+MathSAT000.000.000007000

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc5020.340.592025030
SMTInterpol020.940.942025040
iProver v3.9.30248.9914.822025040
UltimateEliminator+MathSAT000.000.000007000

SAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
SMTInterpol000.000.000005240
UltimateEliminator+MathSAT000.000.000005200
cvc5000.000.000005230
iProver v3.9.3000.000.000005240

UNSAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc5020.340.592020500
SMTInterpol020.940.942020500
iProver v3.9.30248.9914.822020500
UltimateEliminator+MathSAT000.000.000002500

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc5020.340.592020500
SMTInterpol020.940.942021400
iProver v3.9.30248.9914.822021400
UltimateEliminator+MathSAT000.000.000007000