LIA (Single Query Track)

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

Results were generated on 2026-07-25

Benchmarks: 300
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-alpha2	Amaya	YicesQS	YicesQS

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout
Z3-alpha2	214 (base +16)	5788.58	5815.90	214	115	99	86	86
Z3-alpha2-debug ⁿ	214	6646.10	6468.19	214	115	99	86	86
YicesQS	202	2438.87	2463.87	202	103	99	98	71
Amaya	200	3642.66	3672.61	200	117	83	100	87
Z3-GEX ^ne	199 (base -2)	3689.44	978.46	201	102	99	99	99
z3-BooledASS ^ne	199 (base +0)	1534.40	1558.90	199	100	99	101	101
cvc5	182	55.99	78.60	182	83	99	118	118
cvc5-cvc5-xyz ^ne	182 (base +0)	57.35	79.96	182	83	99	118	118
UltimateEliminator+MathSAT	139	3764.52	3012.25	139	45	94	161	37
SMTInterpol	65	52.61	41.64	65	6	59	235	51
Z3-GEX-base ⁿ	201	2449.39	2474.67	201	102	99	99	99
z3-BooledASS-base ⁿ	199	1495.58	1520.17	199	100	99	101	101
Z3-alpha2-base ⁿ	198	1217.74	1242.34	198	99	99	102	102
cvc5-cvc5-xyz-base ⁿ	182	57.20	79.89	182	83	99	118	118

(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-alpha2	214 (base +16)	5788.58	5815.90	214	115	99	86	86
Z3-alpha2-debug ⁿ	214	6646.10	6468.19	214	115	99	86	86
YicesQS	202	2438.87	2463.87	202	103	99	98	71
Z3-GEX ^ne	201 (base +0)	8846.53	2269.13	201	102	99	99	99
Amaya	200	3642.66	3672.61	200	117	83	100	87
z3-BooledASS ^ne	199 (base +0)	1534.40	1558.90	199	100	99	101	101
cvc5	182	55.99	78.60	182	83	99	118	118
cvc5-cvc5-xyz ^ne	182 (base +0)	57.35	79.96	182	83	99	118	118
UltimateEliminator+MathSAT	139	3764.52	3012.25	139	45	94	161	37
SMTInterpol	65	52.61	41.64	65	6	59	235	51
Z3-GEX-base ⁿ	201	2449.39	2474.67	201	102	99	99	99
z3-BooledASS-base ⁿ	199	1495.58	1520.17	199	100	99	101	101
Z3-alpha2-base ⁿ	198	1217.74	1242.34	198	99	99	102	102
cvc5-cvc5-xyz-base ⁿ	182	57.20	79.89	182	83	99	118	118

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
Amaya	117	3543.44	3560.83	117	117	84	99	72
Z3-alpha2	115 (base +16)	5760.73	5775.54	115	115	86	99	86
Z3-alpha2-debug ⁿ	115	6235.14	6139.70	115	115	86	99	86
YicesQS	103	2422.38	2435.22	103	103	98	99	71
Z3-GEX ^ne	102 (base +0)	8822.53	2235.47	102	102	99	99	99
z3-BooledASS ^ne	100 (base +0)	1517.02	1529.33	100	100	101	99	101
cvc5	83	34.25	44.50	83	83	118	99	118
cvc5-cvc5-xyz ^ne	83 (base +0)	35.40	45.67	83	83	118	99	118
UltimateEliminator+MathSAT	45	2982.77	2576.28	45	45	156	99	34
SMTInterpol	6	2.53	2.66	6	6	195	99	44
Z3-GEX-base ⁿ	102	2432.37	2445.33	102	102	99	99	99
z3-BooledASS-base ⁿ	100	1478.16	1490.64	100	100	101	99	101
Z3-alpha2-base ⁿ	99	1200.50	1212.81	99	99	102	99	102
cvc5-cvc5-xyz-base ⁿ	83	35.32	45.65	83	83	118	99	118

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
YicesQS	99	16.49	28.65	99	99	0	201	0
z3-BooledASS ^ne	99 (base +0)	17.38	29.58	99	99	0	201	0
Z3-GEX ^ne	99 (base +0)	24.00	33.65	99	99	0	201	0
cvc5	99	21.74	34.10	99	99	0	201	0
cvc5-cvc5-xyz ^ne	99 (base +0)	21.95	34.29	99	99	0	201	0
Z3-alpha2 ^ne	99 (base +0)	27.85	40.37	99	99	0	201	0
Z3-alpha2-debug ⁿ	99	410.95	328.48	99	99	0	201	0
UltimateEliminator+MathSAT	94	781.76	435.97	94	94	5	201	3
Amaya	83	99.21	111.78	83	83	16	201	15
SMTInterpol	59	50.07	38.98	59	59	40	201	7
Z3-GEX-base ⁿ	99	17.02	29.34	99	99	0	201	0
z3-BooledASS-base ⁿ	99	17.42	29.53	99	99	0	201	0
Z3-alpha2-base ⁿ	99	17.25	29.53	99	99	0	201	0
cvc5-cvc5-xyz-base ⁿ	99	21.88	34.24	99	99	0	201	0

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained
Z3-alpha2 ^ne	198 (base +3)	149.34	174.24	198	99	99	0	102
Z3-alpha2-debug ⁿ	198	912.66	747.60	198	99	99	0	102
YicesQS	196	47.47	71.55	196	97	99	0	104
z3-BooledASS ^ne	194 (base +0)	67.39	91.21	194	95	99	0	106
Z3-GEX	193 (base -2)	188.41	100.98	193	94	99	0	107
cvc5	182	55.99	78.60	182	83	99	0	118
cvc5-cvc5-xyz ^ne	182 (base +0)	57.35	79.96	182	83	99	0	118
Amaya	181	424.12	450.87	181	98	83	0	119
UltimateEliminator+MathSAT	129	1007.04	432.14	129	37	92	124	47
SMTInterpol	65	52.61	41.64	65	6	59	164	71
Z3-alpha2-base ⁿ	195	70.84	94.95	195	96	99	0	105
Z3-GEX-base ⁿ	195	92.87	117.18	195	96	99	0	105
z3-BooledASS-base ⁿ	194	67.75	91.62	194	95	99	0	106
cvc5-cvc5-xyz-base ⁿ	182	57.20	79.89	182	83	99	0	118

SMT-COMP 2026