SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

UFNIRA (Single Query Track)

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

Results were generated on 2025-08-11

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
cvc5iProver v3.9.3-iProver v3.9.3cvc5

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc5083616.93627.38830831830461
iProver v3.9.30811846.06531.069009017601760
SMTInterpol01810.309.101801824801180
UltimateEliminator+MathSAT000.000.00000266070

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
iProver v3.9.309028316.477209.679009017601760
cvc5083616.93627.38830831830461
SMTInterpol01810.309.101801824801180
UltimateEliminator+MathSAT000.000.00000266070

SAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
SMTInterpol000.000.0000079187510
UltimateEliminator+MathSAT000.000.000007918710
cvc5000.000.000007918740
iProver v3.9.3000.000.0000079187790

UNSAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
iProver v3.9.309028316.477209.67900909779970
cvc5083616.93627.388308310479421
SMTInterpol01810.309.101801816979670
UltimateEliminator+MathSAT000.000.000001877960

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc508152.3162.40810811364900
iProver v3.9.3073181.0192.8673073019300
SMTInterpol01810.309.101801813011800
UltimateEliminator+MathSAT000.000.00000259700