SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_NonLinearIntArith (Single Query Track)

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

Results were generated on 2025-08-11

Benchmarks: 12280
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-alphaz3siriZ3-alpha

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Z3-alpha09965
(base +311)		370769.84108145.76100946735335921860210722
z3siri09693
(base +68)		364276.43365522.379693630233912587023858
Yices20907178210.9579338.429071625928123209031899
cvc5085091735785.761737085.76850959862523377103499262
SMTInterpol0812239.891738.068177412199090
Z3-alpha-base n09654222112.03223338.459654631133432626024321
z3siri-base n09625244756.16245977.719625628933362655024681
(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-alpha010094
(base +440)		646037.05183609.69100946735335921860210722
z3siri09693
(base +68)		364276.43365522.379693630233912587023858
Yices20907178210.9579338.429071625928123209031899
cvc5085091735785.761737085.76850959862523377103499262
SMTInterpol0812239.891738.068177412199090
Z3-alpha-base n09654222112.03223338.459654631133432626024321
z3siri-base n09625244756.16245977.719625628933362655024681
(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.6467356735041951264056
z3siri06302
(base +13)		255299.99256112.0363026302085251267631
Yices20625948507.3149284.0762596259089551268890
cvc5059861641703.851642679.93598659860116851261046116
SMTInterpol071411.611242.417707147512610
Z3-alpha-base n06311159742.03160544.9663116311084351267730
z3siri-base n06289178877.37179677.3562896289086551267970
(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
z3siri03391
(base +55)		108976.44109410.3533910339126886212500
Z3-alpha03359
(base +16)		203670.5757857.0533590335930086212973
Yices20281229703.6430054.3528120281284786218379
cvc50252394081.9294405.832523025231136862111315
SMTInterpol074828.28495.65740743585862130
Z3-alpha-base n0334362370.0162793.4933430334331686213150
z3siri-base n0333665878.7966300.3633360333632386213220
(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-alpha09079
(base +589)		80828.2624950.2890796019306010319100
Yices20858919652.7320711.5385895943264610368100
z3siri07070
(base -1372)		21951.0922824.4470704524254620519000
cvc50474513431.0914015.1647452595215010752500
SMTInterpol071264.13128.80713681208412500
Z3-alpha-base n0849029783.4230836.9084905502298811377900
z3siri-base n0844230648.1331692.4284425472297011382700
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver