SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

Equality_NonLinearArith (Unsat Core Track)

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

Results were generated on 2025-08-11

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

Logics:

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 UNSATUnsolvedAbstainedTimeoutMemout
cvc50458029129829.33130479.155099509958304751
SMTInterpol022057023448.2415960.16337733772305012760
UltimateEliminator+MathSAT06832478.291899.50158158276827561540

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc50458029129829.33130479.155099509958304751
SMTInterpol022057023448.2415960.16337733772305012760
UltimateEliminator+MathSAT06832478.291899.50158158276827561540

UNSAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc50458029129829.33130479.155099509958304751
SMTInterpol022057023448.2415960.16337733772305012760
UltimateEliminator+MathSAT06832478.291899.50158158276827561540

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc503260202530.633103.66463046307997300
SMTInterpol020471610445.434968.3633353335445190200
UltimateEliminator+MathSAT0649932.03516.641401402469307300