SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

UFNIA (Single Query Track)

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

Results were generated on 2025-08-11

Benchmarks: 6313
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
cvc503772204859.93205350.15377270730652541025370
iProver v3.9.301774254272.0066708.552076020764237042370
SMTInterpol010328121.616088.491032769565281022400
UltimateEliminator+MathSAT06149580.358240.20614431183569904670

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc503772204859.93205350.15377270730652541025370
iProver v3.9.3020761134264.25288106.292076020764237042370
SMTInterpol010328121.616088.491032769565281022400
UltimateEliminator+MathSAT06149580.358240.20614431183569904670

SAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc5070730800.8830892.2270770701560510
UltimateEliminator+MathSAT04318587.507640.09431431027756052350
SMTInterpol07654.2843.2376760632560580
iProver v3.9.3000.000.0000070856057080

UNSAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc503065174059.05174457.9330650306511031381100
iProver v3.9.3020761134264.25288106.292076020761099313810990
SMTInterpol09568067.336045.2695609562219313810620
UltimateEliminator+MathSAT0183992.86600.111830183299231381420

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc5031193035.583419.91311963924800319400
iProver v3.9.30124022150.576797.261240012400507300
SMTInterpol010192867.851290.931019769432416287800
UltimateEliminator+MathSAT05853585.522319.57585404181517355500