SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_Equality_NonLinearArith (Unsat Core Track)

Competition results for the QF_Equality_NonLinearArith division in the Unsat Core Track. Chart

Results were generated on 2025-08-11

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

Logics:

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
cvc5cvc5-cvc5Yices2

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc501275673055.053086.36248248180170
SMTInterpol01053442324.661925.28193193730120
Yices2091860624.21651.44221221405382

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc501275673055.053086.36248248180170
SMTInterpol01053442324.661925.28193193730120
Yices2091860624.21651.44221221405382

UNSAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc501275673055.053086.36248248180170
SMTInterpol01053442324.661925.28193193730120
Yices2091860624.21651.44221221405382

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices2089356118.34144.9821721704900
SMTInterpol086537346.84185.56183183592400
cvc5039628187.43216.7023623612900