SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

SMT-COMP 2025

QF_Strings (Single Query Track)

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

Results were generated on 2025-08-11

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

Logics:

QF_S : 10428 benchmarks
QF_SLIA : 23730 benchmarks
QF_SNIA : 70 benchmarks

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	34110 (base +521)	22239.22	26476.54	34110	22093	12017	118	0	75	24
Z3-Noodler	0	33635 (base +4282)	23260.58	27437.40	33635	22088	11547	593	0	77	29
OSTRICH	0	32766	876070.90	572896.46	32781	21440	11341	1447	0	1447	0
cvc5	0	30671	794564.28	798463.70	30671	20275	10396	3557	0	3532	4
Z3-alpha	0	29350 (base -71)	319765.74	110490.43	29524	19113	10411	4704	0	3155	213
Z3-Noodler-Mocha-base ⁿ	0	33589	23586.42	27719.87	33589	22088	11501	639	0	79	28
Z3-alpha-base ⁿ	0	29421	219342.97	223002.50	29421	18963	10458	4807	0	3350	330
Z3-Noodler-base ⁿ	0	29353	188202.78	191856.12	29353	18882	10471	4875	0	3354	325

(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	34110 (base +521)	22239.22	26476.54	34110	22093	12017	118	0	75	24
Z3-Noodler	0	33635 (base +4282)	23260.58	27437.40	33635	22088	11547	593	0	77	29
OSTRICH	0	32781	901069.65	588961.14	32781	21440	11341	1447	0	1447	0
cvc5	0	30671	794564.28	798463.70	30671	20275	10396	3557	0	3532	4
Z3-alpha	0	29524 (base +103)	753806.26	220794.86	29524	19113	10411	4704	0	3155	213
Z3-Noodler-Mocha-base ⁿ	0	33589	23586.42	27719.87	33589	22088	11501	639	0	79	28
Z3-alpha-base ⁿ	0	29421	219342.97	223002.50	29421	18963	10458	4807	0	3350	330
Z3-Noodler-base ⁿ	0	29353	188202.78	191856.12	29353	18882	10471	4875	0	3354	325

(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	22093 (base +5)	15882.66	18623.47	22093	22093	0	51	12084	46	5
Z3-Noodler	0	22088 (base +3206)	15946.83	18685.22	22088	22088	0	56	12084	48	8
OSTRICH	0	21440	788987.02	514244.86	21440	21440	0	704	12084	704	0
cvc5	0	20275	698596.23	701193.20	20275	20275	0	1869	12084	1851	3
Z3-alpha	0	19113 (base +150)	603853.08	178234.40	19113	19113	0	3031	12084	2362	128
Z3-Noodler-Mocha-base ⁿ	0	22088	16244.80	18958.23	22088	22088	0	56	12084	49	7
Z3-alpha-base ⁿ	0	18963	207693.33	210062.17	18963	18963	0	3181	12084	2536	313
Z3-Noodler-base ⁿ	0	18882	175609.63	177963.63	18882	18882	0	3262	12084	2551	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-Mocha	0	12017 (base +516)	6356.56	7853.07	12017	0	12017	46	22165	17	10
Z3-Noodler	0	11547 (base +1076)	7313.76	8752.18	11547	0	11547	516	22165	17	12
OSTRICH	0	11341	112082.64	74716.29	11341	0	11341	722	22165	722	0
Z3-alpha	0	10411 (base -47)	149953.18	42560.47	10411	0	10411	1652	22165	778	85
cvc5	0	10396	95968.05	97270.49	10396	0	10396	1667	22165	1660	1
Z3-Noodler-Mocha-base ⁿ	0	11501	7341.62	8761.64	11501	0	11501	562	22165	18	12
Z3-Noodler-base ⁿ	0	10471	12593.14	13892.50	10471	0	10471	1592	22165	788	13
Z3-alpha-base ⁿ	0	10458	11649.63	12940.33	10458	0	10458	1605	22165	799	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
Z3-Noodler-Mocha	0	34057 (base +541)	9685.94	13914.77	34057	22050	12007	18	153	0	0
Z3-Noodler	0	33559 (base +5385)	9922.05	14087.58	33559	22042	11517	486	183	0	0
Z3-alpha	0	28480 (base +334)	94402.79	44519.30	28480	18253	10227	1117	4631	0	1
cvc5	0	28267	13626.55	17119.73	28267	18205	10062	20	5941	0	0
OSTRICH	0	27956	190516.66	82017.96	27956	16907	11049	0	6272	0	0
Z3-Noodler-Mocha-base ⁿ	0	33516	10023.07	14145.41	33516	22044	11472	531	181	0	0
Z3-Noodler-base ⁿ	0	28174	23832.92	27315.09	28174	17763	10411	1187	4867	0	0
Z3-alpha-base ⁿ	0	28146	23855.72	27327.91	28146	17740	10406	1120	4962	0	0

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