SMT-COMP 2026

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2026

QF_LinearRealArith (Single Query Track)

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

Results were generated on 2026-07-25

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

Logics:

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
Yices2Yices2OpenSMTYices2Yices2

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices2070019785.3719873.30700376324660660
OpenSMT070030975.2331065.21700381319660660
OpenSMT-SMTS-seq ne0696
(base -3)		29486.8428923.76698381317680680
cvc5069128314.7128402.70691367324750750
z3-BooledASS ne0682
(base +0)		33245.3433331.00682364318840840
cvc5-cvc5-xyz ne0677
(base -2)		40265.9040352.36677360317890890
Z3-GEX ne0660
(base -22)		61829.4115864.95687369318790790
SMTInterpol059353442.6545149.1359834625216801630
Samet040017729.7717781.104002531471192471180
OpenSMT-SMTS-seq-base n069929507.6529597.36699381318670670
Z3-GEX-base n068232589.2132678.35682364318840840
z3-BooledASS-base n068233003.9733089.62682364318840840
cvc5-cvc5-xyz-base n067942330.1642418.21679362317870870
(base +/- n): for derived solvers: increment over base solver
ne: not eligible for winning as it does not substantially improve over the base solver (at least 10 % improvement in PAR2 score) n: non-competing solver

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices2070019785.3719873.30700376324660660
OpenSMT070030975.2331065.21700381319660660
OpenSMT-SMTS-seq ne0698
(base -1)		31910.3931298.28698381317680680
cvc5069128314.7128402.70691367324750750
Z3-GEX ne0687
(base +5)		127980.9832448.57687369318790790
z3-BooledASS ne0682
(base +0)		33245.3433331.00682364318840840
cvc5-cvc5-xyz ne0677
(base -2)		40265.9040352.36677360317890890
SMTInterpol059860311.2350252.3359834625216801630
Samet040017729.7717781.104002531471192471180
OpenSMT-SMTS-seq-base n069929507.6529597.36699381318670670
Z3-GEX-base n068232589.2132678.35682364318840840
z3-BooledASS-base n068233003.9733089.62682364318840840
cvc5-cvc5-xyz-base n067942330.1642418.21679362317870870
(base +/- n): for derived solvers: increment over base solver
ne: not eligible for winning as it does not substantially improve over the base solver (at least 10 % improvement in PAR2 score) n: non-competing solver

SAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
OpenSMT038117784.2917833.43381381014371140
OpenSMT-SMTS-seq ne0381
(base +0)		19699.2019305.81381381014371140
Yices203769977.7510024.89376376019371190
Z3-GEX0369
(base +5)		51153.4013057.54369369026371260
cvc5036714367.2814413.85367367028371280
z3-BooledASS ne0364
(base +0)		14818.1114863.40364364031371310
cvc5-cvc5-xyz ne0360
(base -2)		20181.8520227.75360360035371350
SMTInterpol034624588.4321039.59346346049371490
Samet02537807.977840.15253253035478350
OpenSMT-SMTS-seq-base n038118306.3718355.37381381014371140
Z3-GEX-base n036414345.6514393.03364364031371310
z3-BooledASS-base n036414721.4214766.79364364031371310
cvc5-cvc5-xyz-base n036222052.9622099.99362362033371330
(base +/- n): for derived solvers: increment over base solver
ne: not eligible for winning as it does not substantially improve over the base solver (at least 10 % improvement in PAR2 score) n: non-competing solver

UNSAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices203249807.639848.40324032411431110
cvc5032413947.4313988.85324032411431110
OpenSMT031913190.9413231.78319031916431160
z3-BooledASS ne0318
(base +0)		18427.2318467.60318031817431170
Z3-GEX ne0318
(base +0)		76827.5819391.03318031817431170
OpenSMT-SMTS-seq ne0317
(base -1)		12211.1911992.47317031718431180
cvc5-cvc5-xyz ne0317
(base +0)		20084.0620124.62317031718431180
SMTInterpol025235722.8029212.74252025283431780
Samet01479921.799940.95147014779540780
OpenSMT-SMTS-seq-base n031811201.2811241.99318031817431170
Z3-GEX-base n031818243.5618285.32318031817431170
z3-BooledASS-base n031818282.5518322.83318031817431170
cvc5-cvc5-xyz-base n031720277.2120318.22317031718431180
(base +/- n): for derived solvers: increment over base solver
ne: not eligible for winning as it does not substantially improve over the base solver (at least 10 % improvement in PAR2 score) n: non-competing solver

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices206071379.191454.10607331276015900
OpenSMT-SMTS-seq ne0580
(base +1)		1979.491996.66580317263018600
OpenSMT05791815.301887.22579314265018700
cvc505211863.141927.70521284237024500
Z3-GEX ne0514
(base +3)		5939.161686.44514285229025200
z3-BooledASS ne0510
(base +1)		1568.331630.66510276234025600
cvc5-cvc5-xyz ne0450
(base -1)		1674.961730.22450247203031600
SMTInterpol04074120.091895.44407242165035900
Samet0331970.251011.37331220111143400
OpenSMT-SMTS-seq-base n05791828.261900.16579313266018700
Z3-GEX-base n05111548.881613.16511277234025500
z3-BooledASS-base n05091542.581604.89509275234025700
cvc5-cvc5-xyz-base n04511678.411734.27451249202031500
(base +/- n): for derived solvers: increment over base solver
ne: not eligible for winning as it does not substantially improve over the base solver (at least 10 % improvement in PAR2 score) n: non-competing solver