QF_S (Single Query Track)

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

Results were generated on 2026-07-25

Benchmarks: 2417
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	Z3-Noodler	Z3-Noodler	Z3-Noodler	Z3-Noodler

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout
Z3-Noodler	2032 (base +1687)	1801.70	2055.46	2032	587	1445	385	0
OSTRICH	1940	5905.74	6145.94	1940	550	1390	477	477
cvc5-cvc5-xyz ^ne	378 (base +14)	6491.45	6538.79	378	168	210	2039	2013
cvc5	364	9606.06	9652.11	364	168	196	2053	2027
Z3-GEX ^ne	346 (base +0)	7927.70	4656.21	346	196	150	2071	523
z3-BooledASS ^ne	345 (base +0)	3991.27	4034.10	345	195	150	2072	524
cvc5-cvc5-xyz-base ⁿ	364	10059.61	10105.81	364	168	196	2053	2027
Z3-GEX-base ⁿ	346	3267.39	3310.78	346	196	150	2071	523
z3-BooledASS-base ⁿ	345	4006.92	4049.56	345	195	150	2072	524
Z3-Noodler-base ⁿ	345	4092.53	4135.86	345	195	150	2072	524

(base +/- n): for derived solvers: increment over base solver
^ne: not eligible for winning as it does not substantially improve over the base solver (at least 10 % improvement in PAR2 score) ⁿ: non-competing solver

Parallel Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout
Z3-Noodler	2032 (base +1687)	1801.70	2055.46	2032	587	1445	385	0
OSTRICH	1940	5905.74	6145.94	1940	550	1390	477	477
cvc5-cvc5-xyz ^ne	378 (base +14)	6491.45	6538.79	378	168	210	2039	2013
cvc5	364	9606.06	9652.11	364	168	196	2053	2027
Z3-GEX ^ne	346 (base +0)	7927.70	4656.21	346	196	150	2071	523
z3-BooledASS ^ne	345 (base +0)	3991.27	4034.10	345	195	150	2072	524
cvc5-cvc5-xyz-base ⁿ	364	10059.61	10105.81	364	168	196	2053	2027
Z3-GEX-base ⁿ	346	3267.39	3310.78	346	196	150	2071	523
z3-BooledASS-base ⁿ	345	4006.92	4049.56	345	195	150	2072	524
Z3-Noodler-base ⁿ	345	4092.53	4135.86	345	195	150	2072	524

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
Z3-Noodler	587 (base +392)	370.41	443.33	587	587	0	1830	0
OSTRICH	550	2644.44	2712.60	550	550	37	1830	37
Z3-GEX ^ne	196 (base +0)	3879.18	2256.31	196	196	391	1830	0
z3-BooledASS ^ne	195 (base +0)	2570.98	2595.12	195	195	392	1830	1
cvc5-cvc5-xyz ^ne	168 (base +0)	355.30	376.08	168	168	419	1830	393
cvc5	168	646.35	667.28	168	168	419	1830	393
Z3-GEX-base ⁿ	196	1836.78	1861.33	196	196	391	1830	0
z3-BooledASS-base ⁿ	195	2575.99	2600.08	195	195	392	1830	1
Z3-Noodler-base ⁿ	195	2673.63	2698.05	195	195	392	1830	1
cvc5-cvc5-xyz-base ⁿ	168	631.83	652.78	168	168	419	1830	393

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
Z3-Noodler	1445 (base +1295)	1431.29	1612.13	1445	1445	0	972	0
OSTRICH	1390	3261.30	3433.34	1390	1390	55	972	55
cvc5-cvc5-xyz ^ne	210 (base +14)	6136.15	6162.71	210	210	1235	972	1235
cvc5	196	8959.71	8984.83	196	196	1249	972	1249
z3-BooledASS ^ne	150 (base +0)	1420.29	1438.98	150	150	1295	972	523
Z3-GEX ^ne	150 (base +0)	4048.52	2399.91	150	150	1295	972	523
cvc5-cvc5-xyz-base ⁿ	196	9427.78	9453.03	196	196	1249	972	1249
Z3-Noodler-base ⁿ	150	1418.90	1437.81	150	150	1295	972	523
Z3-GEX-base ⁿ	150	1430.61	1449.45	150	150	1295	972	523
z3-BooledASS-base ⁿ	150	1430.93	1449.48	150	150	1295	972	523

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained
Z3-Noodler	2017 (base +1687)	1360.79	1612.50	2017	587	1430	385	15
OSTRICH	1926	1920.91	2158.52	1926	544	1382	0	491
cvc5-cvc5-xyz ^ne	347 (base +9)	756.82	799.74	347	168	179	26	2044
cvc5	338	649.97	692.04	338	164	174	26	2053
z3-BooledASS ^ne	331 (base +0)	588.97	629.72	331	186	145	1548	538
Z3-GEX ^ne	275 (base -59)	450.79	266.86	275	161	114	1547	595
cvc5-cvc5-xyz-base ⁿ	338	609.31	651.29	338	164	174	26	2053
Z3-GEX-base ⁿ	334	611.49	653.15	334	189	145	1548	535
z3-BooledASS-base ⁿ	331	588.73	629.32	331	186	145	1548	538
Z3-Noodler-base ⁿ	330	569.71	610.77	330	185	145	1548	539

SMT-COMP 2026