SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

SMT-COMP 2025

QF_SLIA (Single Query Track)

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

Results were generated on 2025-08-11

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

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24 seconds Performance (parallel)
Z3-Noodler-Mocha	Z3-Noodler-Mocha	Z3-Noodler-Mocha	Z3-Noodler	Z3-Noodler-Mocha

Sequential Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Z3-Noodler-Mocha	0	23626 (base +5)	18652.40	21584.25	23626	15796	7830	104	0	71	14
Z3-Noodler	0	23622 (base +3231)	18684.89	21616.10	23622	15791	7831	108	0	72	17
OSTRICH	0	22886	825579.05	544527.98	22901	15192	7709	829	0	829	0
cvc5	0	21585	761359.99	764128.07	21585	14253	7332	2145	0	2139	0
Z3-alpha	0	20333 (base -65)	298762.46	98595.07	20504	13094	7410	3226	0	2780	146
Z3-Noodler-Mocha-base ⁿ	0	23621	19023.35	21928.09	23621	15791	7830	109	0	74	16
Z3-alpha-base ⁿ	0	20398	204867.86	207413.21	20398	12933	7465	3332	0	2902	326
Z3-Noodler-base ⁿ	0	20391	173430.99	175976.98	20391	12919	7472	3339	0	2914	322

(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
Z3-Noodler-Mocha	0	23626 (base +5)	18652.40	21584.25	23626	15796	7830	104	0	71	14
Z3-Noodler	0	23622 (base +3231)	18684.89	21616.10	23622	15791	7831	108	0	72	17
OSTRICH	0	22901	850577.80	560592.66	22901	15192	7709	829	0	829	0
cvc5	0	21585	761359.99	764128.07	21585	14253	7332	2145	0	2139	0
Z3-alpha	0	20504 (base +106)	726625.45	207351.55	20504	13094	7410	3226	0	2780	146
Z3-Noodler-Mocha-base ⁿ	0	23621	19023.35	21928.09	23621	15791	7830	109	0	74	16
Z3-alpha-base ⁿ	0	20398	204867.86	207413.21	20398	12933	7465	3332	0	2902	326
Z3-Noodler-base ⁿ	0	20391	173430.99	175976.98	20391	12919	7472	3339	0	2914	322

(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-Noodler-Mocha	0	15796 (base +5)	13241.35	15197.64	15796	15796	0	51	7883	46	5
Z3-Noodler	0	15791 (base +2872)	13270.92	15226.09	15791	15791	0	56	7883	48	8
OSTRICH	0	15192	756376.84	495527.79	15192	15192	0	655	7883	655	0
cvc5	0	14253	689772.73	691621.45	14253	14253	0	1594	7883	1594	0
Z3-alpha	0	13094 (base +161)	589707.37	170020.57	13094	13094	0	2753	7883	2355	114
Z3-Noodler-Mocha-base ⁿ	0	15791	13594.73	15532.38	15791	15791	0	56	7883	49	7
Z3-alpha-base ⁿ	0	12933	200771.91	202396.21	12933	12933	0	2914	7883	2518	311
Z3-Noodler-base ⁿ	0	12919	169440.71	171059.18	12919	12919	0	2928	7883	2534	312

(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
Z3-Noodler	0	7831 (base +359)	5413.97	6390.01	7831	0	7831	41	15858	15	7
Z3-Noodler-Mocha	0	7830 (base +0)	5411.06	6386.61	7830	0	7830	42	15858	16	7
OSTRICH	0	7709	94200.96	65064.87	7709	0	7709	163	15858	163	0
Z3-alpha	0	7410 (base -55)	136918.08	37330.99	7410	0	7410	462	15858	420	32
cvc5	0	7332	71587.26	72506.63	7332	0	7332	540	15858	534	0
Z3-Noodler-Mocha-base ⁿ	0	7830	5428.62	6395.71	7830	0	7830	42	15858	16	7
Z3-Noodler-base ⁿ	0	7472	3990.29	4917.80	7472	0	7472	400	15858	375	10
Z3-alpha-base ⁿ	0	7465	4095.95	5017.00	7465	0	7465	407	15858	379	15

(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
Z3-Noodler-Mocha	0	23575 (base +5)	7277.51	10201.32	23575	15755	7820	18	137	0	0
Z3-Noodler	0	23568 (base +4301)	7295.24	10218.22	23568	15748	7820	18	144	0	0
Z3-alpha	0	19545 (base +373)	83571.56	37652.95	19545	12291	7254	85	4100	0	0
cvc5	0	19286	11147.80	13526.93	19286	12212	7074	6	4438	0	0
OSTRICH	0	18149	153670.82	63582.53	18149	10716	7433	0	5581	0	0
Z3-Noodler-Mocha-base ⁿ	0	23570	7386.53	10283.11	23570	15750	7820	18	142	0	0
Z3-Noodler-base ⁿ	0	19267	20511.46	22894.70	19267	11828	7439	94	4369	0	0
Z3-alpha-base ⁿ	0	19172	20345.60	22711.30	19172	11736	7436	97	4461	0	0

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