SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

AUFDTLIA (Single Query Track)

Competition results for the AUFDTLIA logic in the Single Query 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)
cvc5cvc5cvc5cvc5cvc5

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc5029322120.5022159.62293852087070
SMTInterpol01851365.83803.6718511841150160
iProver v3.9.3017014058.013804.33179017912101120

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc5029322120.5022159.62293852087070
SMTInterpol01851365.83803.6718511841150160
iProver v3.9.3017931083.988115.91179017912101120

SAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc508522043.8822057.1285850021500
SMTInterpol010.640.5511084215110
iProver v3.9.3000.000.0000085215850

UNSAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc5020876.62102.50208020809200
SMTInterpol01841365.20803.121840184249200
iProver v3.9.3017931083.988115.9117901792992200

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc5025090.08120.932504220805000
SMTInterpol0178782.42323.691781177893300
iProver v3.9.301331410.69484.351330133016700