QF_LRA (Single Query Track)

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

Results were generated on 2026-07-25

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

Winners

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

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout
OpenSMT-SMTS-seq ^ne	501 (base +0)	15264.39	14975.42	502	279	223	17	17
OpenSMT	501	16198.05	16261.97	501	278	223	18	18
Yices2	484	15715.58	15776.43	484	269	215	35	35
cvc5	481	22930.12	22991.68	481	265	216	38	38
z3-BooledASS ^ne	474 (base +0)	28059.88	28119.41	474	264	210	45	45
cvc5-cvc5-xyz ^ne	471 (base -1)	32153.67	32214.07	471	260	211	48	48
Z3-GEX ^ne	455 (base -19)	55540.46	14164.94	478	268	210	41	41
SMTInterpol	418	46054.84	39951.70	423	249	174	96	95
Samet	400	17729.77	17781.10	400	253	147	119	118
OpenSMT-SMTS-seq-base ⁿ	501	15404.22	15468.03	501	278	223	18	18
Z3-GEX-base ⁿ	474	27537.92	27600.28	474	264	210	45	45
z3-BooledASS-base ⁿ	474	27757.10	27816.57	474	264	210	45	45
cvc5-cvc5-xyz-base ⁿ	472	33118.46	33179.92	472	261	211	47	47

(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
OpenSMT-SMTS-seq ^ne	502 (base +1)	16477.45	16161.56	502	279	223	17	17
OpenSMT	501	16198.05	16261.97	501	278	223	18	18
Yices2	484	15715.58	15776.43	484	269	215	35	35
cvc5	481	22930.12	22991.68	481	265	216	38	38
Z3-GEX ^ne	478 (base +4)	111367.52	28148.83	478	268	210	41	41
z3-BooledASS ^ne	474 (base +0)	28059.88	28119.41	474	264	210	45	45
cvc5-cvc5-xyz ^ne	471 (base -1)	32153.67	32214.07	471	260	211	48	48
SMTInterpol	423	52923.42	45054.90	423	249	174	96	95
Samet	400	17729.77	17781.10	400	253	147	119	118
OpenSMT-SMTS-seq-base ⁿ	501	15404.22	15468.03	501	278	223	18	18
Z3-GEX-base ⁿ	474	27537.92	27600.28	474	264	210	45	45
z3-BooledASS-base ⁿ	474	27757.10	27816.57	474	264	210	45	45
cvc5-cvc5-xyz-base ⁿ	472	33118.46	33179.92	472	261	211	47	47

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
OpenSMT-SMTS-seq ^ne	279 (base +1)	11782.76	11543.47	279	279	9	231	9
OpenSMT	278	11475.29	11511.07	278	278	10	231	10
Yices2	269	7625.97	7659.75	269	269	19	231	19
Z3-GEX	268 (base +4)	42792.70	10894.41	268	268	20	231	20
cvc5	265	12534.96	12568.78	265	265	23	231	23
z3-BooledASS ^ne	264 (base +0)	11457.79	11490.44	264	264	24	231	24
cvc5-cvc5-xyz ^ne	260 (base -1)	16414.09	16447.35	260	260	28	231	28
Samet	253	7807.97	7840.15	253	253	35	231	35
SMTInterpol	249	21465.30	18668.81	249	249	39	231	39
OpenSMT-SMTS-seq-base ⁿ	278	11739.58	11775.40	278	278	10	231	10
Z3-GEX-base ⁿ	264	11080.99	11115.38	264	264	24	231	24
z3-BooledASS-base ⁿ	264	11310.89	11343.56	264	264	24	231	24
cvc5-cvc5-xyz-base ⁿ	261	17139.53	17173.52	261	261	27	231	27

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
OpenSMT-SMTS-seq ^ne	223 (base +0)	4694.70	4618.09	223	223	3	293	3
OpenSMT	223	4722.76	4750.90	223	223	3	293	3
cvc5	216	10395.16	10422.90	216	216	10	293	10
Yices2	215	8089.61	8116.68	215	215	11	293	11
cvc5-cvc5-xyz ^ne	211 (base +0)	15739.58	15766.72	211	211	15	293	15
z3-BooledASS ^ne	210 (base +0)	16602.09	16628.98	210	210	16	293	16
Z3-GEX ^ne	210 (base +0)	68574.82	17254.43	210	210	16	293	16
SMTInterpol	174	31458.12	26386.09	174	174	52	293	51
Samet	147	9921.79	9940.95	147	147	79	293	78
OpenSMT-SMTS-seq-base ⁿ	223	3664.64	3692.62	223	223	3	293	3
cvc5-cvc5-xyz-base ⁿ	211	15978.93	16006.39	211	211	15	293	15
z3-BooledASS-base ⁿ	210	16446.21	16473.01	210	210	16	293	16
Z3-GEX-base ⁿ	210	16456.94	16484.89	210	210	16	293	16

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained
OpenSMT-SMTS-seq ^ne	431 (base +3)	1590.50	1598.90	431	236	195	0	88
OpenSMT	428	1425.33	1478.61	428	231	197	0	91
Yices2	408	1034.88	1085.17	408	232	176	0	111
cvc5	346	1261.80	1304.75	346	192	154	0	173
Samet	331	970.25	1011.37	331	220	111	1	187
z3-BooledASS ^ne	324 (base +1)	1114.54	1153.99	324	185	139	0	195
Z3-GEX ^ne	323 (base -2)	4198.56	1163.16	323	191	132	0	196
cvc5-cvc5-xyz ^ne	299 (base -2)	1063.34	1100.00	299	171	128	0	220
SMTInterpol	272	2671.01	1228.82	272	167	105	0	247
OpenSMT-SMTS-seq-base ⁿ	428	1424.00	1477.17	428	230	198	0	91
Z3-GEX-base ⁿ	325	1105.91	1146.84	325	186	139	0	194
z3-BooledASS-base ⁿ	323	1085.86	1125.24	323	184	139	0	196
cvc5-cvc5-xyz-base ⁿ	301	1094.32	1131.54	301	173	128	0	218

SMT-COMP 2026