NIA (Single Query Track)

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

Results were generated on 2026-07-25

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

Winners

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

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout
Z3-alpha2	238 (base +15)	3138.10	3047.78	238	77	161	16	16
Z3-alpha2-debug ⁿ	238	3640.51	3319.94	238	77	161	16	16
Z3-GEX	235 (base +12)	670.08	257.36	238	79	159	16	16
cvc5	231	23062.53	23093.31	231	80	151	23	23
cvc5-cvc5-xyz ^ne	230 (base +0)	22276.21	22306.37	230	80	150	24	24
z3-BooledASS ^ne	227 (base +0)	495.84	523.80	227	76	151	27	26
Amaya	208	540.85	570.65	208	53	155	46	5
UltimateEliminator+MathSAT	141	807.36	433.67	141	47	94	113	35
YicesQS	123	1768.95	1783.80	123	77	46	131	131
SMTInterpol	20	42.69	25.87	20	13	7	234	1
cvc5-cvc5-xyz-base ⁿ	230	22276.54	22306.87	230	80	150	24	24
z3-BooledASS-base ⁿ	227	499.31	527.30	227	76	151	27	26
Z3-alpha2-base ⁿ	223	867.53	895.26	223	74	149	31	28
Z3-GEX-base ⁿ	223	1102.79	1130.69	223	73	150	31	27

(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-GEX	238 (base +15)	8961.10	2572.61	238	79	159	16	16
Z3-alpha2	238 (base +15)	3138.10	3047.78	238	77	161	16	16
Z3-alpha2-debug ⁿ	238	3640.51	3319.94	238	77	161	16	16
cvc5	231	23062.53	23093.31	231	80	151	23	23
cvc5-cvc5-xyz ^ne	230 (base +0)	22276.21	22306.37	230	80	150	24	24
z3-BooledASS ^ne	227 (base +0)	495.84	523.80	227	76	151	27	26
Amaya	208	540.85	570.65	208	53	155	46	5
UltimateEliminator+MathSAT	141	807.36	433.67	141	47	94	113	35
YicesQS	123	1768.95	1783.80	123	77	46	131	131
SMTInterpol	20	42.69	25.87	20	13	7	234	1
cvc5-cvc5-xyz-base ⁿ	230	22276.54	22306.87	230	80	150	24	24
z3-BooledASS-base ⁿ	227	499.31	527.30	227	76	151	27	26
Z3-alpha2-base ⁿ	223	867.53	895.26	223	74	149	31	28
Z3-GEX-base ⁿ	223	1102.79	1130.69	223	73	150	31	27

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
cvc5	80	916.20	926.35	80	80	2	172	2
cvc5-cvc5-xyz ^ne	80 (base +0)	917.06	927.02	80	80	2	172	2
Z3-GEX	79 (base +6)	3256.27	1096.84	79	79	3	172	3
YicesQS	77	1223.22	1232.55	77	77	5	172	5
Z3-alpha2	77 (base +3)	1317.22	1287.92	77	77	5	172	5
Z3-alpha2-debug ⁿ	77	1481.21	1377.46	77	77	5	172	5
z3-BooledASS ^ne	76 (base +0)	84.33	93.63	76	76	6	172	6
Amaya	53	274.39	282.29	53	53	29	172	1
UltimateEliminator+MathSAT	47	354.36	229.90	47	47	35	172	14
SMTInterpol	13	23.10	12.49	13	13	69	172	0
cvc5-cvc5-xyz-base ⁿ	80	917.16	927.07	80	80	2	172	2
z3-BooledASS-base ⁿ	76	84.19	93.59	76	76	6	172	6
Z3-alpha2-base ⁿ	74	489.30	498.57	74	74	8	172	8
Z3-GEX-base ⁿ	73	169.68	178.76	73	73	9	172	8

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
Z3-alpha2	161 (base +12)	1820.88	1759.86	161	161	10	83	10
Z3-alpha2-debug ⁿ	161	2159.30	1942.48	161	161	10	83	10
Z3-GEX	159 (base +9)	5704.84	1475.78	159	159	12	83	12
Amaya	155	266.46	288.37	155	155	16	83	4
z3-BooledASS ^ne	151 (base +0)	411.50	430.17	151	151	20	83	19
cvc5	151	22146.33	22166.96	151	151	20	83	20
cvc5-cvc5-xyz ^ne	150 (base +0)	21359.15	21379.35	150	150	21	83	21
UltimateEliminator+MathSAT	94	453.00	203.78	94	94	77	83	21
YicesQS	46	545.73	551.25	46	46	125	83	125
SMTInterpol	7	19.59	13.38	7	7	164	83	1
z3-BooledASS-base ⁿ	151	415.11	433.71	151	151	20	83	19
Z3-GEX-base ⁿ	150	933.11	951.93	150	150	21	83	18
cvc5-cvc5-xyz-base ⁿ	150	21359.37	21379.80	150	150	21	83	21
Z3-alpha2-base ⁿ	149	378.23	396.69	149	149	22	83	19

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained
Z3-GEX	233 (base +18)	246.21	130.19	233	77	156	0	21
Z3-alpha2 ^ne	232 (base +15)	998.09	909.96	232	75	157	0	22
Z3-alpha2-debug ⁿ	232	1491.31	1178.63	232	75	157	0	22
z3-BooledASS ^ne	221 (base +0)	279.79	306.98	221	76	145	1	32
Amaya	207	445.59	475.26	207	52	155	36	11
cvc5	153	37.74	56.82	153	78	75	0	101
cvc5-cvc5-xyz ^ne	153 (base +0)	44.51	63.37	153	78	75	0	101
UltimateEliminator+MathSAT	140	673.29	302.32	140	46	94	75	39
YicesQS	109	57.79	71.23	109	70	39	0	145
SMTInterpol	20	42.69	25.87	20	13	7	229	5
z3-BooledASS-base ⁿ	221	280.90	308.14	221	76	145	1	32
Z3-alpha2-base ⁿ	217	265.44	292.39	217	71	146	3	34
Z3-GEX-base ⁿ	215	219.47	246.28	215	70	145	1	38
cvc5-cvc5-xyz-base ⁿ	153	44.45	63.24	153	78	75	0	101

SMT-COMP 2026