SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_LIA (Single Query Track)

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

Results were generated on 2025-08-11

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

Winners

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

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
OpenSMT04579272280.40272891.4645792784179524602370
cvc504443311878.34312467.2044432752169138203760
Yices20439557937.6758491.7543952653174243004177
Z3-alpha04204
(base +206)		149811.2041325.09427127021569554053513
SMTInterpol04203227287.72173651.5742072491171661805270
Z3-alpha-base n03998122151.77122664.35399825311467827079822
(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
OpenSMT04579272280.40272891.4645792784179524602370
cvc504443311878.34312467.2044432752169138203760
Yices20439557937.6758491.7543952653174243004177
Z3-alpha04271
(base +273)		306454.9281046.39427127021569554053513
SMTInterpol04207234194.14177646.9742072491171661805270
Z3-alpha-base n03998122151.77122664.35399825311467827079822
(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
OpenSMT02784201903.25202278.9927842784017518661750
cvc502752149143.95149501.8027522752020718662070
Z3-alpha02702
(base +171)		207881.3254171.6027022702025718662525
Yices20265351275.1451611.3026532653030618663060
SMTInterpol02491131371.72108236.8524912491046818664610
Z3-alpha-base n0253191157.8891484.4625312531042818664262
(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
OpenSMT0179570377.1570612.48179501795472983440
Yices2017426662.536880.4517420174210029831000
SMTInterpol01716102822.4369410.121716017161262983550
cvc501691162734.40162965.4016910169115129831510
Z3-alpha01569
(base +102)		98573.6126874.7915690156927329832721
Z3-alpha-base n0146730993.8931179.88146701467375298335717
(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
Yices2042163518.544043.76421625011715660300
Z3-alpha03837
(base +356)		26294.179483.85383724021435698200
OpenSMT033298996.709411.053329198013499148700
cvc5031435509.615895.613143205810856167600
SMTInterpol0295522204.9410092.2529551874108144182600
Z3-alpha-base n034818193.268623.783481222412576133800
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver