SMT-COMP 2026

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2026

QF_LRA (Model Validation Track)

Competition results for the QF_LRA logic in the Model Validation Track. Chart

Results were generated on 2026-07-25

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
OpenSMTOpenSMTOpenSMT-Yices2

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATUnsolvedAbstainedTimeoutMemout
OpenSMT04789494.659555.04478478120120
Yices204726564.226623.41472472180180
z3-BooledASS ne0465
(base +0)		13601.7313659.94465465250250
SMTInterpol045826535.5623630.12458458320310
cvc503722729.302775.7137237211801180
z3-BooledASS-base n046513469.5113527.44465465250250
(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 SATUnsolvedAbstainedTimeoutMemout
OpenSMT04789494.659555.04478478120120
Yices204726564.226623.41472472180180
z3-BooledASS ne0465
(base +0)		13601.7313659.94465465250250
SMTInterpol045826535.5623630.12458458320310
cvc503722729.302775.7137237211801180
z3-BooledASS-base n046513469.5113527.44465465250250
(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 SATUnsolvedAbstainedTimeoutMemout
OpenSMT04789494.659555.04478478120120
Yices204726564.226623.41472472180180
z3-BooledASS ne0465
(base +0)		13601.7313659.94465465250250
SMTInterpol045826535.5623630.12458458320310
cvc503722729.302775.7137237211801180
z3-BooledASS-base n046513469.5113527.44465465250250
(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 SATUnsolvedAbstainedTimeoutMemout
Yices20432576.45630.1043243205800
OpenSMT0424718.34771.1042442406600
z3-BooledASS ne0383
(base -2)		713.49760.69383383010700
SMTInterpol03662137.54997.11366366012400
cvc50359378.47423.10359359013100
z3-BooledASS-base n0385755.06802.45385385010500
(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