LRA (Single Query Track)

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

Results were generated on 2026-07-25

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

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24 seconds Performance (parallel)
YicesQS	YicesQS	YicesQS	YicesQS	YicesQS

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout
YicesQS	599	173.61	246.78	599	244	355	3	3
z3-BooledASS ^ne	569 (base +0)	28189.24	28261.18	569	238	331	33	33
Z3-alpha2 ^ne	563 (base -6)	19602.96	19350.12	563	235	328	39	39
Z3-alpha2-debug ⁿ	563	20802.54	20006.30	563	235	328	39	39
Z3-GEX ^ne	538 (base -31)	10841.80	2870.20	570	237	333	32	32
UltimateEliminator+MathSAT	518	11187.09	8916.50	518	206	312	84	84
cvc5-cvc5-xyz ^ne	501 (base +0)	11053.05	11116.07	501	206	295	101	101
cvc5	498	9082.58	9145.11	498	206	292	104	104
SMTInterpol	101	3292.79	2794.27	101	0	101	501	18
Z3-alpha2-base ⁿ	569	27699.66	27771.68	569	235	334	33	33
z3-BooledASS-base ⁿ	569	28095.32	28167.35	569	238	331	33	33
Z3-GEX-base ⁿ	569	28287.98	28360.71	569	235	334	33	33
cvc5-cvc5-xyz-base ⁿ	501	11063.13	11126.28	501	206	295	101	101

(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
YicesQS	599	173.61	246.78	599	244	355	3	3
Z3-GEX ^ne	570 (base +1)	86979.06	21924.25	570	237	333	32	32
z3-BooledASS ^ne	569 (base +0)	28189.24	28261.18	569	238	331	33	33
Z3-alpha2 ^ne	563 (base -6)	19602.96	19350.12	563	235	328	39	39
Z3-alpha2-debug ⁿ	563	20802.54	20006.30	563	235	328	39	39
UltimateEliminator+MathSAT	518	11187.09	8916.50	518	206	312	84	84
cvc5-cvc5-xyz ^ne	501 (base +0)	11053.05	11116.07	501	206	295	101	101
cvc5	498	9082.58	9145.11	498	206	292	104	104
SMTInterpol	101	3292.79	2794.27	101	0	101	501	18
Z3-alpha2-base ⁿ	569	27699.66	27771.68	569	235	334	33	33
z3-BooledASS-base ⁿ	569	28095.32	28167.35	569	238	331	33	33
Z3-GEX-base ⁿ	569	28287.98	28360.71	569	235	334	33	33
cvc5-cvc5-xyz-base ⁿ	501	11063.13	11126.28	501	206	295	101	101

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
YicesQS	244	69.31	99.07	244	244	2	356	2
z3-BooledASS ^ne	238 (base +0)	5874.56	5904.15	238	238	8	356	8
Z3-GEX	237 (base +2)	13132.82	3356.10	237	237	9	356	9
Z3-alpha2 ^ne	235 (base +0)	5023.54	4917.84	235	235	11	356	11
Z3-alpha2-debug ⁿ	235	5539.51	5207.38	235	235	11	356	11
UltimateEliminator+MathSAT	206	3843.07	2889.10	206	206	40	356	40
cvc5-cvc5-xyz ^ne	206 (base +0)	3834.02	3859.91	206	206	40	356	40
cvc5	206	4377.23	4403.34	206	206	40	356	40
SMTInterpol	0	0.00	0.00	0	0	246	356	16
z3-BooledASS-base ⁿ	238	5846.49	5876.21	238	238	8	356	8
Z3-alpha2-base ⁿ	235	4151.29	4180.62	235	235	11	356	11
Z3-GEX-base ⁿ	235	4222.00	4251.57	235	235	11	356	11
cvc5-cvc5-xyz-base ⁿ	206	3831.72	3857.73	206	206	40	356	40

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
YicesQS	355	104.31	147.71	355	355	1	246	1
Z3-GEX ^ne	333 (base -1)	73846.24	18568.15	333	333	23	246	23
z3-BooledASS ^ne	331 (base +0)	22314.68	22357.03	331	331	25	246	25
Z3-alpha2 ^ne	328 (base -6)	14579.42	14432.28	328	328	28	246	28
Z3-alpha2-debug ⁿ	328	15263.03	14798.93	328	328	28	246	28
UltimateEliminator+MathSAT	312	7344.02	6027.40	312	312	44	246	44
cvc5-cvc5-xyz ^ne	295 (base +0)	7219.03	7256.16	295	295	61	246	61
cvc5	292	4705.34	4741.77	292	292	64	246	64
SMTInterpol	101	3292.79	2794.27	101	101	255	246	2
Z3-alpha2-base ⁿ	334	23548.37	23591.06	334	334	22	246	22
Z3-GEX-base ⁿ	334	24065.98	24109.14	334	334	22	246	22
z3-BooledASS-base ⁿ	331	22248.83	22291.14	331	331	25	246	25
cvc5-cvc5-xyz-base ⁿ	295	7231.41	7268.55	295	295	61	246	61

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained
YicesQS	599	173.61	246.78	599	244	355	0	3
Z3-GEX ^ne	507 (base +9)	2676.12	818.12	507	225	282	0	95
z3-BooledASS ^ne	500 (base -1)	769.07	830.83	500	222	278	0	102
Z3-alpha2 ^ne	500 (base +2)	2481.03	2255.87	500	222	278	0	102
Z3-alpha2-debug ⁿ	500	3541.00	2833.44	500	222	278	0	102
UltimateEliminator+MathSAT	492	3450.11	1512.03	492	199	293	0	110
cvc5-cvc5-xyz ^ne	437 (base +0)	239.61	293.93	437	173	264	0	165
cvc5	436	224.09	278.21	436	172	264	0	166
SMTInterpol	97	553.97	216.23	97	0	97	468	37
z3-BooledASS-base ⁿ	501	788.64	850.32	501	223	278	0	101
Z3-alpha2-base ⁿ	498	745.67	807.26	498	221	277	0	104
Z3-GEX-base ⁿ	498	761.43	823.51	498	221	277	0	104
cvc5-cvc5-xyz-base ⁿ	437	237.09	291.46	437	173	264	0	165

SMT-COMP 2026