QF_LIA (Single Query Track)

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

Results were generated on 2026-07-25

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

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24 seconds Performance (parallel)
QiuQi	QiuQi	QiuQi	QiuQi	Yices2

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout
QiuQi	1262	35058.97	35236.18	1262	795	467	55	45
OpenSMT-SMTS-seq ^ne	1239 (base +6)	84296.33	81103.36	1240	779	461	77	77
OpenSMT	1229	72991.17	73152.11	1229	769	460	88	85
cvc5	1207	67714.63	67869.03	1207	765	442	110	108
Yices2	1183	16934.90	17082.56	1183	737	446	134	132
Z3-GEX	1144 (base +55)	39609.12	11420.64	1157	750	407	160	158
Z3-alpha2	1143 (base +51)	38508.43	38462.97	1143	733	410	174	172
Z3-alpha2-debug ⁿ	1143	42317.90	41177.97	1143	733	410	174	172
SMTInterpol	1132	61606.00	47730.69	1135	692	443	182	164
cvc5-cvc5-xyz ^ne	1111 (base +0)	116950.41	117095.81	1111	725	386	206	204
z3-BooledASS ^ne	1040 (base -52)	34623.75	34753.98	1040	668	372	277	222
NeuroSym	1008	3533.28	3421.70	1008	640	368	309	3
OpenSMT-SMTS-seq-base ⁿ	1233	73901.20	74062.82	1233	773	460	84	81
cvc5-cvc5-xyz-base ⁿ	1111	114563.77	114711.17	1111	725	386	206	204
Z3-alpha2-base ⁿ	1092	36169.77	36309.28	1092	701	391	225	222
z3-BooledASS-base ⁿ	1092	36315.26	36452.23	1092	701	391	225	222
Z3-GEX-base ⁿ	1089	40310.65	40449.90	1089	704	385	228	225

(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
QiuQi	1262	35058.97	35236.18	1262	795	467	55	45
OpenSMT-SMTS-seq ^ne	1240 (base +7)	86007.81	81955.51	1240	779	461	77	77
OpenSMT	1229	72991.17	73152.11	1229	769	460	88	85
cvc5	1207	67714.63	67869.03	1207	765	442	110	108
Yices2	1183	16934.90	17082.56	1183	737	446	134	132
Z3-GEX	1157 (base +68)	62087.94	17059.19	1157	750	407	160	158
Z3-alpha2	1143 (base +51)	38508.43	38462.97	1143	733	410	174	172
Z3-alpha2-debug ⁿ	1143	42317.90	41177.97	1143	733	410	174	172
SMTInterpol	1135	65667.07	50707.52	1135	692	443	182	164
cvc5-cvc5-xyz ^ne	1111 (base +0)	116950.41	117095.81	1111	725	386	206	204
z3-BooledASS ^ne	1040 (base -52)	34623.75	34753.98	1040	668	372	277	222
NeuroSym	1008	3533.28	3421.70	1008	640	368	309	3
OpenSMT-SMTS-seq-base ⁿ	1233	73901.20	74062.82	1233	773	460	84	81
cvc5-cvc5-xyz-base ⁿ	1111	114563.77	114711.17	1111	725	386	206	204
Z3-alpha2-base ⁿ	1092	36169.77	36309.28	1092	701	391	225	222
z3-BooledASS-base ⁿ	1092	36315.26	36452.23	1092	701	391	225	222
Z3-GEX-base ⁿ	1089	40310.65	40449.90	1089	704	385	228	225

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
QiuQi	795	21274.04	21385.21	795	795	34	488	29
OpenSMT-SMTS-seq ^ne	779 (base +6)	68955.31	66175.93	779	779	50	488	50
OpenSMT	769	58669.87	58771.47	769	769	60	488	60
cvc5	765	36071.60	36168.61	765	765	64	488	64
Z3-GEX	750 (base +46)	45843.05	12400.70	750	750	79	488	79
Yices2	737	11915.68	12007.77	737	737	92	488	92
Z3-alpha2	733 (base +32)	28498.36	28488.81	733	733	96	488	96
Z3-alpha2-debug ⁿ	733	30962.91	30251.84	733	733	96	488	96
cvc5-cvc5-xyz ^ne	725 (base +0)	72241.89	72336.38	725	725	104	488	104
SMTInterpol	692	39067.43	31612.56	692	692	137	488	132
z3-BooledASS ^ne	668 (base -33)	25160.95	25244.58	668	668	161	488	128
NeuroSym	640	2275.33	2204.23	640	640	189	488	1
OpenSMT-SMTS-seq-base ⁿ	773	59305.96	59408.29	773	773	56	488	56
cvc5-cvc5-xyz-base ⁿ	725	71247.63	71343.32	725	725	104	488	104
Z3-GEX-base ⁿ	704	29385.33	29475.60	704	704	125	488	125
Z3-alpha2-base ⁿ	701	25993.70	26083.30	701	701	128	488	128
z3-BooledASS-base ⁿ	701	26146.44	26234.38	701	701	128	488	128

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
QiuQi	467	13784.92	13850.96	467	467	15	835	12
OpenSMT-SMTS-seq ^ne	461 (base +1)	17052.50	15779.58	461	461	21	835	21
OpenSMT	460	14321.30	14380.63	460	460	22	835	21
Yices2	446	5019.22	5074.79	446	446	36	835	36
SMTInterpol	443	26599.63	19094.96	443	443	39	835	29
cvc5	442	31643.03	31700.42	442	442	40	835	40
Z3-alpha2	410 (base +19)	10010.07	9974.16	410	410	72	835	72
Z3-alpha2-debug ⁿ	410	11354.99	10926.13	410	410	72	835	72
Z3-GEX	407 (base +22)	16244.89	4658.49	407	407	75	835	75
cvc5-cvc5-xyz ^ne	386 (base +0)	44708.53	44759.43	386	386	96	835	96
z3-BooledASS ^ne	372 (base -19)	9462.79	9509.39	372	372	110	835	90
NeuroSym	368	1257.95	1217.47	368	368	114	835	2
OpenSMT-SMTS-seq-base ⁿ	460	14595.24	14654.53	460	460	22	835	21
z3-BooledASS-base ⁿ	391	10168.82	10217.84	391	391	91	835	90
Z3-alpha2-base ⁿ	391	10176.07	10225.98	391	391	91	835	90
cvc5-cvc5-xyz-base ⁿ	386	43316.14	43367.85	386	386	96	835	96
Z3-GEX-base ⁿ	385	10925.33	10974.30	385	385	97	835	96

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained
Yices2	1123	992.76	1131.70	1123	688	435	2	192
Z3-GEX ^ne	1047 (base +120)	6906.12	2539.29	1047	671	376	2	268
NeuroSym	990	2898.30	2788.58	990	624	366	175	152
QiuQi	974	2720.65	2842.88	974	641	333	10	333
Z3-alpha2 ^ne	947 (base +7)	2493.31	2546.30	947	618	329	2	368
Z3-alpha2-debug ⁿ	937	5734.51	4894.24	937	614	323	2	378
z3-BooledASS ^ne	897 (base -45)	1625.42	1735.19	897	579	318	47	373
OpenSMT	886	2559.59	2669.99	886	527	359	3	428
OpenSMT-SMTS-seq	874 (base -15)	2479.54	2440.40	874	531	343	0	443
cvc5	851	1683.04	1787.79	851	571	280	2	464
SMTInterpol	792	6517.77	2967.39	792	510	282	2	523
cvc5-cvc5-xyz ^ne	764 (base -2)	1407.50	1501.07	764	520	244	2	551
z3-BooledASS-base ⁿ	942	2189.58	2305.09	942	608	334	2	373
Z3-alpha2-base ⁿ	940	2151.25	2268.02	940	607	333	2	375
Z3-GEX-base ⁿ	927	2071.78	2186.97	927	606	321	2	388
OpenSMT-SMTS-seq-base ⁿ	889	2643.67	2754.39	889	529	360	3	425
cvc5-cvc5-xyz-base ⁿ	766	1447.87	1542.39	766	521	245	2	549

SMT-COMP 2026