SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

SMT-COMP 2025

QF_LinearIntArith (Single Query Track)

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

Results were generated on 2025-08-11

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

Logics:

QF_IDL : 1208 benchmarks
QF_LIA : 4825 benchmarks
QF_LIRA : 7 benchmarks

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24 seconds Performance (parallel)
OpenSMT	OpenSMT	Z3-alpha	OpenSMT	Yices2

Sequential Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
OpenSMT	0	5471	317917.99	318645.54	5471	3355	2116	562	7	553	0
Yices2	0	5378	89078.61	89758.64	5378	3296	2082	662	0	649	7
cvc5	0	5370	379623.11	380336.32	5370	3297	2073	670	0	659	5
Z3-alpha	0	5179 (base +139)	222282.46	60479.52	5316	3371	1945	724	0	700	18
SMTInterpol	0	4801	267924.64	205361.47	4805	2823	1982	1235	0	883	0
Z3-alpha-base ⁿ	0	5040	173202.74	173852.15	5040	3186	1854	1000	0	971	22

(base +/- n): for derived solvers: increment over base solver
ⁿ: non-competing solver

Parallel Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
OpenSMT	0	5471	317917.99	318645.54	5471	3355	2116	562	7	553	0
Yices2	0	5378	89078.61	89758.64	5378	3296	2082	662	0	649	7
cvc5	0	5370	379623.11	380336.32	5370	3297	2073	670	0	659	5
Z3-alpha	0	5316 (base +276)	558629.74	145316.44	5316	3371	1945	724	0	700	18
SMTInterpol	0	4805	274831.06	209356.87	4805	2823	1982	1235	0	883	0
Z3-alpha-base ⁿ	0	5040	173202.74	173852.15	5040	3186	1854	1000	0	971	22

(base +/- n): for derived solvers: increment over base solver
ⁿ: non-competing solver

SAT Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Z3-alpha	0	3371 (base +185)	352652.82	91128.81	3371	3371	0	316	2353	306	10
OpenSMT	0	3355	238639.05	239090.37	3355	3355	0	331	2354	331	0
cvc5	0	3297	191610.23	192041.52	3297	3297	0	390	2353	385	5
Yices2	0	3296	72989.67	73408.42	3296	3296	0	391	2353	391	0
SMTInterpol	0	2823	156237.31	129397.05	2823	2823	0	864	2353	703	0
Z3-alpha-base ⁿ	0	3186	117803.80	118215.74	3186	3186	0	501	2353	499	2

(base +/- n): for derived solvers: increment over base solver
ⁿ: non-competing solver

UNSAT Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
OpenSMT	0	2116	79278.94	79555.17	2116	0	2116	152	3772	149	0
Yices2	0	2082	16088.94	16350.21	2082	0	2082	191	3767	191	0
cvc5	0	2073	188012.87	188294.79	2073	0	2073	200	3767	200	0
SMTInterpol	0	1982	118593.75	79959.82	1982	0	1982	291	3767	152	0
Z3-alpha	0	1945 (base +91)	205976.92	54187.64	1945	0	1945	328	3767	327	1
Z3-alpha-base ⁿ	0	1854	55398.93	55636.41	1854	0	1854	419	3767	401	17

(base +/- n): for derived solvers: increment over base solver
ⁿ: non-competing solver

24 seconds Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Yices2	0	5085	4793.62	5426.72	5085	3066	2019	6	949	0	0
Z3-alpha	0	4648 (base +342)	33837.64	11756.41	4648	2934	1714	6	1386	0	0
OpenSMT	0	3973	11065.23	11559.63	3973	2351	1622	9	2058	0	0
cvc5	0	3782	7747.19	8211.92	3782	2402	1380	6	2252	0	0
SMTInterpol	0	3381	26943.96	12293.03	3381	2102	1279	217	2442	0	0
Z3-alpha-base ⁿ	0	4306	10224.64	10757.48	4306	2753	1553	6	1728	0	0

(base +/- n): for derived solvers: increment over base solver
ⁿ: non-competing solver