QF_NIA (Single Query Track)

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

Results were generated on 2026-07-25

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

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24 seconds Performance (parallel)
Z3-Z3++	Z3-Z3++	Z3-Z3++	Z3-alpha2	Z3-alpha2

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout
Z3-Z3++	2408 (base +197)	98561.95	98867.97	2408	1630	778	447	429
Z3-alpha2	2407 (base +216)	63966.76	63864.21	2407	1577	830	448	438
Z3-alpha2-debug ⁿ	2403	69528.24	67124.33	2404	1577	827	451	441
Z3-GEX	2326 (base +61)	83033.74	24555.12	2358	1566	792	497	451
Yices2	2145	17196.83	17463.10	2145	1469	676	710	701
cvc5	2001	386705.93	386990.97	2001	1400	601	854	845
cvc5-cvc5-xyz ^ne	1989 (base +9)	395969.61	396252.11	1989	1395	594	866	857
Z3-siri ^ne	1950 (base -319)	18347.43	18591.43	1950	1234	716	905	628
z3-BooledASS ^ne	1407 (base -865)	37612.23	37788.16	1407	968	439	1448	576
Xolver	1333	57236.93	57412.21	1333	1278	55	1522	1496
SMTInterpol	23	73.19	37.25	23	3	20	2832	0
z3-BooledASS-base ⁿ	2272	47236.74	47521.41	2272	1466	806	583	563
Z3-siri-base ⁿ	2269	55002.84	55289.93	2269	1472	797	586	544
Z3-GEX-base ⁿ	2265	56270.59	56558.26	2265	1467	798	590	544
Z3-Z3++-base ⁿ	2211	106184.70	106470.90	2211	1522	689	644	634
Z3-alpha2-base ⁿ	2191	44562.03	44838.07	2191	1414	777	664	549
cvc5-cvc5-xyz-base ⁿ	1980	388267.39	388550.17	1980	1385	595	875	866

(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-Z3++	2408 (base +197)	98561.95	98867.97	2408	1630	778	447	429
Z3-alpha2	2407 (base +216)	63966.76	63864.21	2407	1577	830	448	438
Z3-alpha2-debug ⁿ	2404	70729.38	68324.11	2404	1577	827	451	441
Z3-GEX	2358 (base +93)	161843.41	45937.83	2358	1566	792	497	451
Yices2	2145	17196.83	17463.10	2145	1469	676	710	701
cvc5	2001	386705.93	386990.97	2001	1400	601	854	845
cvc5-cvc5-xyz ^ne	1989 (base +9)	395969.61	396252.11	1989	1395	594	866	857
Z3-siri ^ne	1950 (base -319)	18347.43	18591.43	1950	1234	716	905	628
z3-BooledASS ^ne	1407 (base -865)	37612.23	37788.16	1407	968	439	1448	576
Xolver	1333	57236.93	57412.21	1333	1278	55	1522	1496
SMTInterpol	23	73.19	37.25	23	3	20	2832	0
z3-BooledASS-base ⁿ	2272	47236.74	47521.41	2272	1466	806	583	563
Z3-siri-base ⁿ	2269	55002.84	55289.93	2269	1472	797	586	544
Z3-GEX-base ⁿ	2265	56270.59	56558.26	2265	1467	798	590	544
Z3-Z3++-base ⁿ	2211	106184.70	106470.90	2211	1522	689	644	634
Z3-alpha2-base ⁿ	2191	44562.03	44838.07	2191	1414	777	664	549
cvc5-cvc5-xyz-base ⁿ	1980	388267.39	388550.17	1980	1385	595	875	866

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
Z3-Z3++	1630 (base +108)	36707.02	36911.82	1630	1630	34	1191	21
Z3-alpha2	1577 (base +163)	47598.83	47528.05	1577	1577	87	1191	77
Z3-alpha2-debug ⁿ	1577	52685.40	51102.42	1577	1577	87	1191	77
Z3-GEX	1566 (base +99)	84036.62	25464.15	1566	1566	98	1191	76
Yices2	1469	11517.89	11700.50	1469	1469	195	1191	186
cvc5	1400	366436.72	366645.58	1400	1400	264	1191	255
cvc5-cvc5-xyz ^ne	1395 (base +10)	376666.17	376874.06	1395	1395	269	1191	260
Xolver	1278	49779.31	49946.99	1278	1278	386	1191	367
Z3-siri ^ne	1234 (base -238)	8189.07	8342.93	1234	1234	430	1191	208
z3-BooledASS ^ne	968 (base -498)	32611.30	32732.94	968	968	696	1191	191
SMTInterpol	3	9.02	3.63	3	3	1661	1191	0
Z3-Z3++-base ⁿ	1522	71654.45	71851.85	1522	1522	142	1191	133
Z3-siri-base ⁿ	1472	36340.50	36526.64	1472	1472	192	1191	170
Z3-GEX-base ⁿ	1467	35030.92	35216.96	1467	1467	197	1191	174
z3-BooledASS-base ⁿ	1466	37360.30	37544.66	1466	1466	198	1191	178
Z3-alpha2-base ⁿ	1414	34412.13	34590.80	1414	1414	250	1191	184
cvc5-cvc5-xyz-base ⁿ	1385	368500.70	368708.02	1385	1385	279	1191	270

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
Z3-alpha2	830 (base +53)	16367.93	16336.16	830	830	55	1970	55
Z3-alpha2-debug ⁿ	827	18043.98	17221.69	827	827	58	1970	58
Z3-GEX ^ne	792 (base -6)	77806.78	20473.68	792	792	93	1970	82
Z3-Z3++	778 (base +89)	61854.93	61956.16	778	778	107	1970	107
Z3-siri ^ne	716 (base -81)	10158.36	10248.49	716	716	169	1970	138
Yices2	676	5678.94	5762.60	676	676	209	1970	209
cvc5	601	20269.21	20345.39	601	601	284	1970	284
cvc5-cvc5-xyz ^ne	594 (base -1)	19303.43	19378.05	594	594	291	1970	291
z3-BooledASS ^ne	439 (base -367)	5000.94	5055.21	439	439	446	1970	79
Xolver	55	7457.62	7465.22	55	55	830	1970	823
SMTInterpol	20	64.17	33.62	20	20	865	1970	0
z3-BooledASS-base ⁿ	806	9876.44	9976.76	806	806	79	1970	79
Z3-GEX-base ⁿ	798	21239.67	21341.30	798	798	87	1970	87
Z3-siri-base ⁿ	797	18662.34	18763.29	797	797	88	1970	88
Z3-alpha2-base ⁿ	777	10149.90	10247.26	777	777	108	1970	85
Z3-Z3++-base ⁿ	689	34530.25	34619.05	689	689	196	1970	196
cvc5-cvc5-xyz-base ⁿ	595	19766.70	19842.15	595	595	290	1970	290

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained
Z3-GEX ^ne	2140 (base +139)	19861.91	7038.06	2140	1443	697	13	702
Z3-alpha2	2099 (base +137)	8523.19	8561.98	2099	1365	734	9	747
Z3-alpha2-debug ⁿ	2079	15560.48	13614.36	2079	1349	730	9	767
Yices2	2025	4571.88	4821.93	2025	1391	634	9	821
Z3-Z3++ ^ne	1844 (base +167)	6062.41	6290.89	1844	1408	436	9	1002
Z3-siri ^ne	1827 (base -174)	4368.89	4596.36	1827	1182	645	141	887
z3-BooledASS ^ne	1222 (base -818)	4278.45	4428.41	1222	812	410	818	815
cvc5	1160	2907.57	3050.40	1160	628	532	9	1686
cvc5-cvc5-xyz ^ne	1129 (base -3)	2957.57	3096.40	1129	605	524	9	1717
Xolver	883	4726.62	4838.05	883	870	13	3	1969
SMTInterpol	23	73.19	37.25	23	3	20	2821	11
z3-BooledASS-base ⁿ	2040	5937.16	6189.34	2040	1284	756	18	797
Z3-GEX-base ⁿ	2001	7359.66	7609.15	2001	1299	702	9	845
Z3-siri-base ⁿ	2001	7428.31	7677.53	2001	1307	694	9	845
Z3-alpha2-base ⁿ	1962	5721.45	5965.15	1962	1244	718	109	784
Z3-Z3++-base ⁿ	1677	6771.08	6981.06	1677	1156	521	9	1169
cvc5-cvc5-xyz-base ⁿ	1132	3030.38	3170.29	1132	605	527	9	1714

SMT-COMP 2026