SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

ANIA (Single Query Track)

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

Results were generated on 2025-08-11

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

Winners

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

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
SMTInterpol0924.1311.0394569070
cvc5050.961.5953273050
UltimateEliminator+MathSAT0312.625.9033075000
iProver v3.9.30355.0017.21505730730

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
SMTInterpol0924.1311.0394569070
cvc5050.961.5953273050
iProver v3.9.3054451.861128.64505730730
UltimateEliminator+MathSAT0312.625.9033075000

SAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
SMTInterpol041.801.8144007400
cvc5030.480.8633017400
UltimateEliminator+MathSAT0312.625.9033017400
iProver v3.9.3000.000.0000047440

UNSAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
SMTInterpol0522.329.2150537000
iProver v3.9.3054451.861128.6450537030
cvc5020.480.7320267010
UltimateEliminator+MathSAT000.000.0000087000

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
SMTInterpol0924.1311.0394562700
cvc5050.961.5953268500
UltimateEliminator+MathSAT0312.625.9033075000
iProver v3.9.30355.0017.2130307500