SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_NonLinearRealArith (Single Query Track)

Competition results for the QF_NonLinearRealArith division in the Single Query Track. Chart

Results were generated on 2025-08-11

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

Logics:

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
Z3-alphaZ3-alphaZ3-alphaZ3-alphaZ3-alpha

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Z3-alpha02856
(base +9)		67264.3622562.8028721452142023202301
z3siri02803
(base -44)		80486.2580842.8728031413139030102951
cvc502766114285.94114640.9327661353141333803380
Yices20274621997.1922341.6927461392135435803571
SMT-RAT0258275051.0175380.3625821296128652205211
SMTInterpol05514555.753400.39551225292553000
Z3-alpha-base n0284750463.5350822.1328471433141425702552
z3siri-base n0284751826.4052185.5528471433141425702552
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Z3-alpha02872
(base +25)		104134.6933978.7328721452142023202301
z3siri02803
(base -44)		80486.2580842.8728031413139030102951
cvc502766114285.94114640.9327661353141333803380
Yices20274621997.1922341.6927461392135435803571
SMT-RAT0258275051.0175380.3625821296128652205211
SMTInterpol05514555.753400.39551225292553000
Z3-alpha-base n0284750463.5350822.1328471433141425702552
z3siri-base n0284751826.4052185.5528471433141425702552
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver

SAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Z3-alpha01452
(base +19)		45895.5415216.23145214520881564861
z3siri01413
(base -20)		27290.7927468.8014131413012715641260
Yices20139213962.4314137.3513921392014815641480
cvc50135353885.7754059.4813531353018715641870
SMT-RAT0129634785.4334950.8512961296024415642440
SMTInterpol0223267.572870.90222201518156400
Z3-alpha-base n0143315586.2515765.4514331433010715641061
z3siri-base n0143316021.2216200.7114331433010715641061
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver

UNSAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Z3-alpha01420
(base +6)		58239.1518762.51142001420371647370
cvc50141360400.1860581.46141301413441647440
z3siri01390
(base -24)		53195.4653374.08139001390671647640
Yices2013548034.778204.3413540135410316471021
SMT-RAT0128640265.5840429.5012860128617116471710
SMTInterpol05291288.17529.495290529928164700
Z3-alpha-base n0141434877.2935056.68141401414431647430
z3siri-base n0141435805.1835984.83141401414431647430
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Z3-alpha02690
(base +293)		7786.823548.56269013901300041400
Yices2026331777.402104.80263313391294047100
cvc5025072628.032937.21250712511256059700
SMT-RAT022993253.103537.32229911951104080500
z3siri02256
(base -141)		1612.731891.29225612401016084800
SMTInterpol05361373.30564.25536752925076100
z3siri-base n023972729.813026.06239713331064070700
Z3-alpha-base n023972744.323040.61239713331064070700
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver