SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

UFIDL (Single Query Track)

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

Results were generated on 2025-08-11

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

Winners

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

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc5010542.84544.12101910080
SMTInterpol08131.4869.0081712060
iProver v3.9.307247.3370.98707130110
UltimateEliminator+MathSAT000.000.0000020000

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc5010542.84544.12101910080
SMTInterpol08131.4869.0081712060
iProver v3.9.307247.3370.98707130110
UltimateEliminator+MathSAT000.000.0000020000

SAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
SMTInterpol010.740.5811021700
cvc501540.66540.8511021700
UltimateEliminator+MathSAT000.000.0000031700
iProver v3.9.3000.000.0000031710

UNSAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc5092.183.2890901100
SMTInterpol07130.7468.4270721120
iProver v3.9.307247.3370.9870721120
UltimateEliminator+MathSAT000.000.0000091100

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc5092.183.2890901100
SMTInterpol08131.4869.008175700
iProver v3.9.30542.7513.9950521300
UltimateEliminator+MathSAT000.000.0000020000