QF_NonLinearIntArith (Single Query Track)

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

Results were generated on 2026-07-25

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

Logics:

QF_NIA : 2855 benchmarks
QF_NIRA : 2 benchmarks

Winners

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

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout
Z3-alpha2	2408 (base +216)	63970.57	63868.14	2408	1577	831	449	0	439
Z3-Z3++	2408 (base +197)	98561.95	98867.97	2408	1630	778	447	2	429
Z3-alpha2-debug ⁿ	2404	69535.93	67131.18	2405	1577	828	452	0	442
Z3-GEX	2327 (base +61)	83037.53	24559.04	2359	1566	793	498	0	452
Yices2	2145	17196.83	17463.10	2145	1469	676	712	0	703
cvc5	2001	386705.93	386990.97	2001	1400	601	856	0	847
cvc5-cvc5-xyz ^ne	1989 (base +9)	395969.61	396252.11	1989	1395	594	868	0	859
Z3-siri ^ne	1951 (base -319)	18351.19	18595.32	1951	1234	717	906	0	629
z3-BooledASS ^ne	1408 (base -865)	37616.11	37792.15	1408	968	440	1449	0	577
Xolver	1335	57252.30	57427.83	1335	1278	57	1522	0	1496
SMTInterpol	23	73.19	37.25	23	3	20	2834	0	0
z3-BooledASS-base ⁿ	2273	47240.54	47525.35	2273	1466	807	584	0	564
Z3-siri-base ⁿ	2270	55006.58	55293.81	2270	1472	798	587	0	545
Z3-GEX-base ⁿ	2266	56274.34	56562.13	2266	1467	799	591	0	545
Z3-Z3++-base ⁿ	2211	106184.70	106470.90	2211	1522	689	644	2	634
Z3-alpha2-base ⁿ	2192	44565.83	44842.00	2192	1414	778	665	0	550
cvc5-cvc5-xyz-base ⁿ	1980	388267.39	388550.17	1980	1385	595	877	0	868

(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	Abstained	Timeout
Z3-alpha2	2408 (base +216)	63970.57	63868.14	2408	1577	831	449	0	439
Z3-Z3++	2408 (base +197)	98561.95	98867.97	2408	1630	778	447	2	429
Z3-alpha2-debug ⁿ	2405	70737.07	68330.97	2405	1577	828	452	0	442
Z3-GEX	2359 (base +93)	161847.20	45941.75	2359	1566	793	498	0	452
Yices2	2145	17196.83	17463.10	2145	1469	676	712	0	703
cvc5	2001	386705.93	386990.97	2001	1400	601	856	0	847
cvc5-cvc5-xyz ^ne	1989 (base +9)	395969.61	396252.11	1989	1395	594	868	0	859
Z3-siri ^ne	1951 (base -319)	18351.19	18595.32	1951	1234	717	906	0	629
z3-BooledASS ^ne	1408 (base -865)	37616.11	37792.15	1408	968	440	1449	0	577
Xolver	1335	57252.30	57427.83	1335	1278	57	1522	0	1496
SMTInterpol	23	73.19	37.25	23	3	20	2834	0	0
z3-BooledASS-base ⁿ	2273	47240.54	47525.35	2273	1466	807	584	0	564
Z3-siri-base ⁿ	2270	55006.58	55293.81	2270	1472	798	587	0	545
Z3-GEX-base ⁿ	2266	56274.34	56562.13	2266	1467	799	591	0	545
Z3-Z3++-base ⁿ	2211	106184.70	106470.90	2211	1522	689	644	2	634
Z3-alpha2-base ⁿ	2192	44565.83	44842.00	2192	1414	778	665	0	550
cvc5-cvc5-xyz-base ⁿ	1980	388267.39	388550.17	1980	1385	595	877	0	868

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

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
Z3-alpha2	831 (base +53)	16371.74	16340.09	831	831	56	1970	56
Z3-alpha2-debug ⁿ	828	18051.66	17228.55	828	828	59	1970	59
Z3-GEX ^ne	793 (base -6)	77810.58	20477.60	793	793	94	1970	83
Z3-Z3++	778 (base +89)	61854.93	61956.16	778	778	107	1972	107
Z3-siri ^ne	717 (base -81)	10162.13	10252.39	717	717	170	1970	139
Yices2	676	5678.94	5762.60	676	676	211	1970	211
cvc5	601	20269.21	20345.39	601	601	286	1970	286
cvc5-cvc5-xyz ^ne	594 (base -1)	19303.43	19378.05	594	594	293	1970	293
z3-BooledASS ^ne	440 (base -367)	5004.81	5059.20	440	440	447	1970	80
Xolver	57	7472.98	7480.84	57	57	830	1970	823
SMTInterpol	20	64.17	33.62	20	20	867	1970	0
z3-BooledASS-base ⁿ	807	9880.24	9980.69	807	807	80	1970	80
Z3-GEX-base ⁿ	799	21243.42	21345.17	799	799	88	1970	88
Z3-siri-base ⁿ	798	18666.08	18767.17	798	798	89	1970	89
Z3-alpha2-base ⁿ	778	10153.70	10251.20	778	778	109	1970	86
Z3-Z3++-base ⁿ	689	34530.25	34619.05	689	689	196	1972	196
cvc5-cvc5-xyz-base ⁿ	595	19766.70	19842.15	595	595	292	1970	292

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained
Z3-GEX ^ne	2141 (base +139)	19865.71	7041.98	2141	1443	698	13	703
Z3-alpha2	2100 (base +137)	8527.00	8565.91	2100	1365	735	9	748
Z3-alpha2-debug ⁿ	2080	15568.17	13621.21	2080	1349	731	9	768
Yices2	2025	4571.88	4821.93	2025	1391	634	9	823
Z3-Z3++ ^ne	1844 (base +167)	6062.41	6290.89	1844	1408	436	9	1004
Z3-siri ^ne	1828 (base -174)	4372.65	4600.25	1828	1182	646	141	888
z3-BooledASS ^ne	1223 (base -818)	4282.32	4432.40	1223	812	411	818	816
cvc5	1160	2907.57	3050.40	1160	628	532	9	1688
cvc5-cvc5-xyz ^ne	1129 (base -3)	2957.57	3096.40	1129	605	524	9	1719
Xolver	885	4741.99	4853.68	885	870	15	3	1969
SMTInterpol	23	73.19	37.25	23	3	20	2821	13
z3-BooledASS-base ⁿ	2041	5940.96	6193.27	2041	1284	757	18	798
Z3-GEX-base ⁿ	2002	7363.41	7613.03	2002	1299	703	9	846
Z3-siri-base ⁿ	2002	7432.05	7681.40	2002	1307	695	9	846
Z3-alpha2-base ⁿ	1963	5725.25	5969.08	1963	1244	719	109	785
Z3-Z3++-base ⁿ	1677	6771.08	6981.06	1677	1156	521	9	1171
cvc5-cvc5-xyz-base ⁿ	1132	3030.38	3170.29	1132	605	527	9	1716

SMT-COMP 2026