SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

SMT-COMP 2025

QF_S (Single Query Track)

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

Results were generated on 2025-08-11

Benchmarks: 10428
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-Mocha	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	10414 (base +516)	3575.11	4871.77	10414	6227	4187	14	0	4	10
Z3-Noodler	0	9943 (base +981)	4564.08	5800.87	9943	6227	3716	485	0	5	12
OSTRICH	0	9810	50345.10	28279.78	9810	6178	3632	618	0	618	0
cvc5	0	9016	33193.09	34315.66	9016	5952	3064	1412	0	1393	4
Z3-alpha	0	8947 (base -6)	20988.00	11871.38	8950	5949	3001	1478	0	375	67
Z3-Noodler-Mocha-base ⁿ	0	9898	4551.53	5771.52	9898	6227	3671	530	0	5	12
Z3-Noodler-base ⁿ	0	8962	14771.78	15879.14	8962	5963	2999	1466	0	440	3
Z3-alpha-base ⁿ	0	8953	14462.61	15568.10	8953	5960	2993	1475	0	448	4

(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	10414 (base +516)	3575.11	4871.77	10414	6227	4187	14	0	4	10
Z3-Noodler	0	9943 (base +981)	4564.08	5800.87	9943	6227	3716	485	0	5	12
OSTRICH	0	9810	50345.10	28279.78	9810	6178	3632	618	0	618	0
cvc5	0	9016	33193.09	34315.66	9016	5952	3064	1412	0	1393	4
Z3-alpha	0	8950 (base -3)	27165.54	13419.32	8950	5949	3001	1478	0	375	67
Z3-Noodler-Mocha-base ⁿ	0	9898	4551.53	5771.52	9898	6227	3671	530	0	5	12
Z3-Noodler-base ⁿ	0	8962	14771.78	15879.14	8962	5963	2999	1466	0	440	3
Z3-alpha-base ⁿ	0	8953	14462.61	15568.10	8953	5960	2993	1475	0	448	4

(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	6227 (base +0)	2629.61	3405.30	6227	6227	0	0	4201	0	0
Z3-Noodler	0	6227 (base +264)	2664.29	3438.70	6227	6227	0	0	4201	0	0
OSTRICH	0	6178	32463.42	18628.36	6178	6178	0	49	4201	49	0
cvc5	0	5952	8812.30	9551.79	5952	5952	0	275	4201	257	3
Z3-alpha	0	5949 (base -11)	14130.43	8189.85	5949	5949	0	278	4201	7	14
Z3-Noodler-Mocha-base ⁿ	0	6227	2638.53	3405.60	6227	6227	0	0	4201	0	0
Z3-Noodler-base ⁿ	0	5963	6168.93	6904.44	5963	5963	0	264	4201	17	0
Z3-alpha-base ⁿ	0	5960	6908.93	7644.77	5960	5960	0	267	4201	18	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
Z3-Noodler-Mocha	0	4187 (base +516)	945.50	1466.46	4187	0	4187	4	6237	1	3
Z3-Noodler	0	3716 (base +717)	1899.79	2362.17	3716	0	3716	475	6237	2	5
OSTRICH	0	3632	17881.68	9651.42	3632	0	3632	559	6237	559	0
cvc5	0	3064	24380.79	24763.87	3064	0	3064	1127	6237	1126	1
Z3-alpha	0	3001 (base +8)	13035.10	5229.48	3001	0	3001	1190	6237	358	53
Z3-Noodler-Mocha-base ⁿ	0	3671	1913.00	2365.92	3671	0	3671	520	6237	2	5
Z3-Noodler-base ⁿ	0	2999	8602.86	8974.70	2999	0	2999	1192	6237	413	3
Z3-alpha-base ⁿ	0	2993	7553.69	7923.33	2993	0	2993	1198	6237	420	2

(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	10412 (base +536)	2396.72	3692.93	10412	6225	4187	0	16	0	0
Z3-Noodler	0	9921 (base +1014)	2615.19	3848.93	9921	6224	3697	468	39	0	0
OSTRICH	0	9737	36699.09	18346.72	9737	6121	3616	0	691	0	0
cvc5	0	8911	2467.54	3572.83	8911	5923	2988	14	1503	0	0
Z3-alpha	0	8865 (base -39)	10815.95	6842.36	8865	5892	2973	1032	531	0	1
Z3-Noodler-Mocha-base ⁿ	0	9876	2625.00	3842.05	9876	6224	3652	513	39	0	0
Z3-Noodler-base ⁿ	0	8907	3321.46	4420.39	8907	5935	2972	1023	498	0	0
Z3-alpha-base ⁿ	0	8904	3497.63	4595.42	8904	5934	2970	1023	501	0	0

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