QF_LinearIntArith (Single Query Track)

Competition results for the QF_LinearIntArith division in the Single Query Track. Chart

Results were generated on 2026-07-25

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

Logics:

QF_IDL : 641 benchmarks
QF_LIA : 1317 benchmarks
QF_LIRA : 7 benchmarks

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	Abstained	Timeout
QiuQi	1807	60428.23	60676.14	1807	1138	669	151	7	141
OpenSMT-SMTS-seq ^ne	1719 (base +5)	113587.72	109861.52	1720	1086	634	238	7	238
OpenSMT	1710	99875.72	100098.44	1710	1076	634	248	7	245
Yices2	1701	29726.06	29939.03	1701	1063	638	264	0	262
cvc5	1701	102677.96	102897.16	1701	1053	648	264	0	262
Z3-alpha2	1680 (base +47)	56042.67	55979.86	1680	1066	614	285	0	283
Z3-alpha2-debug ⁿ	1680	61750.46	60078.68	1680	1066	614	285	0	283
Z3-GEX	1662 (base +33)	77791.29	21632.54	1699	1096	603	266	0	264
cvc5-cvc5-xyz ^ne	1594 (base -1)	168607.97	168817.82	1594	1007	587	371	0	369
z3-BooledASS ^ne	1567 (base -68)	55029.78	55226.00	1567	1004	563	398	0	327
SMTInterpol	1494	84958.02	66409.16	1497	918	579	468	0	416
NeuroSym	1008	3533.28	3421.70	1008	640	368	309	648	3
OpenSMT-SMTS-seq-base ⁿ	1714	101175.82	101399.31	1714	1080	634	244	7	241
z3-BooledASS-base ⁿ	1635	61352.14	61558.00	1635	1038	597	330	0	327
Z3-alpha2-base ⁿ	1633	58999.82	59209.09	1633	1036	597	332	0	329
Z3-GEX-base ⁿ	1629	62700.71	62909.33	1629	1039	590	336	0	333
cvc5-cvc5-xyz-base ⁿ	1595	167323.57	167536.19	1595	1008	587	370	0	368

(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	Abstained	Timeout
QiuQi	1807	60428.23	60676.14	1807	1138	669	151	7	141
OpenSMT-SMTS-seq ^ne	1720 (base +6)	115299.21	110713.67	1720	1086	634	238	7	238
OpenSMT	1710	99875.72	100098.44	1710	1076	634	248	7	245
Yices2	1701	29726.06	29939.03	1701	1063	638	264	0	262
cvc5	1701	102677.96	102897.16	1701	1053	648	264	0	262
Z3-GEX	1699 (base +70)	161034.05	42610.35	1699	1096	603	266	0	264
Z3-alpha2	1680 (base +47)	56042.67	55979.86	1680	1066	614	285	0	283
Z3-alpha2-debug ⁿ	1680	61750.46	60078.68	1680	1066	614	285	0	283
cvc5-cvc5-xyz ^ne	1594 (base -1)	168607.97	168817.82	1594	1007	587	371	0	369
z3-BooledASS ^ne	1567 (base -68)	55029.78	55226.00	1567	1004	563	398	0	327
SMTInterpol	1497	89019.09	69385.99	1497	918	579	468	0	416
NeuroSym	1008	3533.28	3421.70	1008	640	368	309	648	3
OpenSMT-SMTS-seq-base ⁿ	1714	101175.82	101399.31	1714	1080	634	244	7	241
z3-BooledASS-base ⁿ	1635	61352.14	61558.00	1635	1038	597	330	0	327
Z3-alpha2-base ⁿ	1633	58999.82	59209.09	1633	1036	597	332	0	329
Z3-GEX-base ⁿ	1629	62700.71	62909.33	1629	1039	590	336	0	333
cvc5-cvc5-xyz-base ⁿ	1595	167323.57	167536.19	1595	1008	587	370	0	368

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
QiuQi	1138	34635.73	34791.11	1138	1138	76	751	71
Z3-GEX	1096 (base +57)	107535.30	28270.12	1096	1096	119	750	119
OpenSMT-SMTS-seq ^ne	1086 (base +6)	90441.83	87266.04	1086	1086	128	751	128
OpenSMT	1076	77750.54	77891.81	1076	1076	138	751	138
Z3-alpha2	1066 (base +30)	37601.06	37587.32	1066	1066	149	750	149
Z3-alpha2-debug ⁿ	1066	41254.43	40219.92	1066	1066	149	750	149
Yices2	1063	20889.10	21022.37	1063	1063	152	750	152
cvc5	1053	58226.61	58361.72	1053	1053	162	750	162
cvc5-cvc5-xyz ^ne	1007 (base -1)	107521.47	107654.22	1007	1007	208	750	208
z3-BooledASS ^ne	1004 (base -34)	39695.17	39821.02	1004	1004	211	750	177
SMTInterpol	918	54657.02	44763.12	918	918	297	750	292
NeuroSym	640	2275.33	2204.23	640	640	189	1136	1
OpenSMT-SMTS-seq-base ⁿ	1080	78659.29	78801.17	1080	1080	134	751	134
Z3-GEX-base ⁿ	1039	41397.57	41530.81	1039	1039	176	750	176
z3-BooledASS-base ⁿ	1038	40603.91	40734.44	1038	1038	177	750	177
Z3-alpha2-base ⁿ	1036	38199.76	38332.49	1036	1036	179	750	179
cvc5-cvc5-xyz-base ⁿ	1008	107671.87	107806.32	1008	1008	207	750	207

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
QiuQi	669	25792.51	25885.03	669	669	38	1258	35
cvc5	648	44451.35	44535.45	648	648	64	1253	64
Yices2	638	8836.95	8916.66	638	638	74	1253	74
OpenSMT	634	22125.19	22206.63	634	634	73	1258	72
OpenSMT-SMTS-seq ^ne	634 (base +0)	24857.38	23447.63	634	634	73	1258	73
Z3-alpha2	614 (base +17)	18441.60	18392.53	614	614	98	1253	98
Z3-alpha2-debug ⁿ	614	20496.03	19858.77	614	614	98	1253	98
Z3-GEX	603 (base +13)	53498.76	14340.22	603	603	109	1253	109
cvc5-cvc5-xyz ^ne	587 (base +0)	61086.51	61163.60	587	587	125	1253	125
SMTInterpol	579	34362.07	24622.86	579	579	133	1253	90
z3-BooledASS ^ne	563 (base -34)	15334.61	15404.98	563	563	149	1253	114
NeuroSym	368	1257.95	1217.47	368	368	114	1483	2
OpenSMT-SMTS-seq-base ⁿ	634	22516.53	22598.14	634	634	73	1258	72
z3-BooledASS-base ⁿ	597	20748.24	20823.56	597	597	115	1253	114
Z3-alpha2-base ⁿ	597	20800.07	20876.60	597	597	115	1253	114
Z3-GEX-base ⁿ	590	21303.14	21378.52	590	590	122	1253	121
cvc5-cvc5-xyz-base ⁿ	587	59651.70	59729.87	587	587	125	1253	125

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained
Yices2	1584	1644.03	1840.14	1584	981	603	2	379
Z3-GEX ^ne	1479 (base +112)	11009.64	3786.02	1479	956	523	2	484
QiuQi	1395	4455.80	4630.75	1395	905	490	10	560
Z3-alpha2 ^ne	1371 (base -9)	3551.23	3638.94	1371	895	476	2	592
Z3-alpha2-debug ⁿ	1357	8276.86	7070.87	1357	889	468	2	606
z3-BooledASS ^ne	1335 (base -48)	2760.24	2923.53	1335	858	477	50	580
OpenSMT	1237	3722.26	3876.32	1237	734	503	3	725
OpenSMT-SMTS-seq ^ne	1221 (base -18)	3733.21	3705.10	1221	736	485	0	744
cvc5	1200	2915.67	3063.48	1200	761	439	2	763
cvc5-cvc5-xyz ^ne	1082 (base -1)	2763.93	2896.54	1082	688	394	2	881
SMTInterpol	1048	9404.63	4303.53	1048	664	384	2	915
NeuroSym	990	2898.30	2788.58	990	624	366	175	800
z3-BooledASS-base ⁿ	1383	3337.02	3506.93	1383	887	496	2	580
Z3-alpha2-base ⁿ	1380	3276.34	3448.06	1380	885	495	2	583
Z3-GEX-base ⁿ	1367	3190.53	3360.55	1367	885	482	2	596
OpenSMT-SMTS-seq-base ⁿ	1239	3804.25	3958.37	1239	735	504	3	723
cvc5-cvc5-xyz-base ⁿ	1083	2776.95	2910.90	1083	688	395	2	880

SMT-COMP 2026