SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_NIA (Single Query Track)

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

Results were generated on 2025-08-11

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

Winners

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

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Z3-alpha09964
(base +311)		370765.20108141.00100936735335821850210622
z3siri09692
(base +68)		364271.71365517.539692630233902586023848
Yices20907178210.9579338.429071625928123207031879
cvc5085081735548.851736848.67850859862522377003498262
SMTInterpol0812239.891738.068177412197080
Z3-alpha-base n09653222107.49223333.789653631133422625024311
z3siri-base n09624244751.36245972.789624628933352654024671
(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-alpha010093
(base +440)		646032.41183604.93100936735335821850210622
z3siri09692
(base +68)		364271.71365517.539692630233902586023848
Yices20907178210.9579338.429071625928123207031879
cvc5085081735548.851736848.67850859862522377003498262
SMTInterpol0812239.891738.068177412197080
Z3-alpha-base n09653222107.49223333.789653631133422625024311
z3siri-base n09624244751.36245972.789624628933352654024671
(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-alpha06735
(base +424)		442366.48125752.6467356735041951244056
z3siri06302
(base +13)		255299.99256112.0363026302085251247631
Yices20625948507.3149284.0762596259089551248890
cvc5059861641703.851642679.93598659860116851241046116
SMTInterpol071411.611242.417707147512410
Z3-alpha-base n06311159742.03160544.9663116311084351247730
z3siri-base n06289178877.37179677.3562896289086551247970
(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
z3siri03390
(base +55)		108971.72109405.5033900339026886202500
Z3-alpha03358
(base +16)		203665.9357852.2933580335830086202973
Yices20281229703.6430054.3528120281284686208369
cvc50252293845.0094168.742522025221136862011315
SMTInterpol074828.28495.65740743584862030
Z3-alpha-base n0334262365.4662788.8233420334231686203150
z3siri-base n0333565873.9966295.4333350333532386203220
(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-alpha09078
(base +589)		80823.6224945.5290786019305910319000
Yices20858919652.7320711.5385895943264610367900
z3siri07069
(base -1372)		21946.3622819.5970694524254520518900
cvc50474513431.0914015.1647452595215010752300
SMTInterpol071264.13128.80713681208412300
Z3-alpha-base n0848929778.8830832.2384895502298711377800
z3siri-base n0844130643.3231687.4984415472296911382600
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver