SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

AUFDTLIRA (Single Query Track)

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

Results were generated on 2025-08-11

Benchmarks: 4721
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
cvc5041583033.673548.4741580415856305571
iProver v3.9.303595161081.5244682.6937490374997209720
SMTInterpol0339821257.7413583.583398033981323011480

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc5041583033.673548.4741580415856305571
iProver v3.9.303749560108.14145624.4137490374997209720
SMTInterpol0339821257.7413583.583398033981323011480

UNSAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc5041583033.673548.47415804158156210
iProver v3.9.303749560108.14145624.413749037494105624100
SMTInterpol0339821257.7413583.583398033987615626810

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc504143830.111342.85414304143057800
SMTInterpol0333310840.925312.10333303333113127500
iProver v3.9.30310628310.069863.133106031060161500