QF_IDL (Single Query Track)

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

Results were generated on 2026-07-25

Benchmarks: 641
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	Z3-GEX	QiuQi	Yices2

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout
QiuQi	545	25369.27	25439.96	545	343	202	96	96
Z3-alpha2 ^ne	531 (base -4)	17476.51	17458.43	531	332	199	110	110
Z3-alpha2-debug ⁿ	531	19353.41	18826.56	531	332	199	110	110
z3-BooledASS ^ne	521 (base -16)	20347.21	20412.47	521	335	186	120	104
Z3-GEX ^ne	512 (base -22)	38101.79	10130.76	536	345	191	105	105
Yices2	512	12742.74	12807.32	512	325	187	129	129
cvc5	489	34952.97	35017.17	489	287	202	152	152
OpenSMT	481	26884.55	26946.33	481	307	174	160	160
OpenSMT-SMTS-seq ^ne	480 (base -1)	29291.39	28758.16	480	307	173	161	161
cvc5-cvc5-xyz ^ne	478 (base -1)	51642.27	51706.11	478	281	197	163	163
SMTInterpol	358	23186.99	18581.98	358	225	133	283	252
z3-BooledASS-base ⁿ	537	24979.37	25047.49	537	336	201	104	104
Z3-alpha2-base ⁿ	535	22773.55	22842.56	535	334	201	106	106
Z3-GEX-base ⁿ	534	22314.82	22383.44	534	334	200	107	107
OpenSMT-SMTS-seq-base ⁿ	481	27274.62	27336.49	481	307	174	160	160
cvc5-cvc5-xyz-base ⁿ	479	52744.59	52809.17	479	282	197	162	162

(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	545	25369.27	25439.96	545	343	202	96	96
Z3-GEX ^ne	536 (base +2)	98865.72	25470.01	536	345	191	105	105
Z3-alpha2 ^ne	531 (base -4)	17476.51	17458.43	531	332	199	110	110
Z3-alpha2-debug ⁿ	531	19353.41	18826.56	531	332	199	110	110
z3-BooledASS ^ne	521 (base -16)	20347.21	20412.47	521	335	186	120	104
Yices2	512	12742.74	12807.32	512	325	187	129	129
cvc5	489	34952.97	35017.17	489	287	202	152	152
OpenSMT	481	26884.55	26946.33	481	307	174	160	160
OpenSMT-SMTS-seq ^ne	480 (base -1)	29291.39	28758.16	480	307	173	161	161
cvc5-cvc5-xyz ^ne	478 (base -1)	51642.27	51706.11	478	281	197	163	163
SMTInterpol	358	23186.99	18581.98	358	225	133	283	252
z3-BooledASS-base ⁿ	537	24979.37	25047.49	537	336	201	104	104
Z3-alpha2-base ⁿ	535	22773.55	22842.56	535	334	201	106	106
Z3-GEX-base ⁿ	534	22314.82	22383.44	534	334	200	107	107
OpenSMT-SMTS-seq-base ⁿ	481	27274.62	27336.49	481	307	174	160	160
cvc5-cvc5-xyz-base ⁿ	479	52744.59	52809.17	479	282	197	162	162

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
Z3-GEX	345 (base +11)	61690.06	15867.11	345	345	40	256	40
QiuQi	343	13361.68	13405.90	343	343	42	256	42
z3-BooledASS ^ne	335 (base -1)	14532.62	14574.71	335	335	50	256	49
Z3-alpha2 ^ne	332 (base -2)	9101.15	9096.84	332	332	53	256	53
Z3-alpha2-debug ⁿ	332	10286.20	9963.57	332	332	53	256	53
Yices2	325	8973.22	9014.29	325	325	60	256	60
OpenSMT	307	19080.67	19120.33	307	307	78	256	78
OpenSMT-SMTS-seq ^ne	307 (base +0)	21486.52	21090.11	307	307	78	256	78
cvc5	287	22152.59	22190.56	287	287	98	256	98
cvc5-cvc5-xyz ^ne	281 (base -1)	35276.79	35314.92	281	281	104	256	104
SMTInterpol	225	15571.43	13142.43	225	225	160	256	160
z3-BooledASS-base ⁿ	336	14455.88	14498.34	336	336	49	256	49
Z3-GEX-base ⁿ	334	12010.01	12052.85	334	334	51	256	51
Z3-alpha2-base ⁿ	334	12204.49	12247.50	334	334	51	256	51
OpenSMT-SMTS-seq-base ⁿ	307	19353.33	19392.88	307	307	78	256	78
cvc5-cvc5-xyz-base ⁿ	282	36421.49	36460.12	282	282	103	256	103

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
QiuQi	202	12007.58	12034.07	202	202	23	416	23
cvc5	202	12800.38	12826.61	202	202	23	416	23
Z3-alpha2 ^ne	199 (base -2)	8375.35	8361.59	199	199	26	416	26
Z3-alpha2-debug ⁿ	199	9067.21	8862.99	199	199	26	416	26
cvc5-cvc5-xyz ^ne	197 (base +0)	16365.48	16391.19	197	197	28	416	28
Z3-GEX ^ne	191 (base -9)	37175.66	9602.90	191	191	34	416	34
Yices2	187	3769.52	3793.03	187	187	38	416	38
z3-BooledASS ^ne	186 (base -15)	5814.60	5837.75	186	186	39	416	24
OpenSMT	174	7803.89	7826.00	174	174	51	416	51
OpenSMT-SMTS-seq ^ne	173 (base -1)	7804.88	7668.06	173	173	52	416	52
SMTInterpol	133	7615.57	5439.55	133	133	92	416	61
z3-BooledASS-base ⁿ	201	10523.49	10549.15	201	201	24	416	24
Z3-alpha2-base ⁿ	201	10569.06	10595.06	201	201	24	416	24
Z3-GEX-base ⁿ	200	10304.80	10330.58	200	200	25	416	25
cvc5-cvc5-xyz-base ⁿ	197	16323.10	16349.05	197	197	28	416	28
OpenSMT-SMTS-seq-base ⁿ	174	7921.29	7943.61	174	174	51	416	51

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained
Yices2	456	650.30	706.86	456	292	164	0	185
z3-BooledASS ^ne	433 (base -3)	1129.38	1182.31	433	278	155	3	205
Z3-GEX ^ne	427 (base -8)	4095.98	1238.57	427	284	143	0	214
QiuQi	421	1735.16	1787.87	421	264	157	0	220
Z3-alpha2 ^ne	419 (base -16)	1052.70	1086.83	419	276	143	0	222
Z3-alpha2-debug ⁿ	415	2517.91	2156.35	415	274	141	0	226
OpenSMT	351	1162.67	1206.33	351	207	144	0	290
OpenSMT-SMTS-seq ^ne	347 (base -3)	1253.67	1264.70	347	205	142	0	294
cvc5	344	1222.27	1264.72	344	189	155	0	297
cvc5-cvc5-xyz ^ne	313 (base +1)	1341.15	1379.56	313	167	146	0	328
SMTInterpol	253	2850.12	1320.60	253	153	100	0	388
z3-BooledASS-base ⁿ	436	1142.03	1195.79	436	278	158	0	205
Z3-GEX-base ⁿ	435	1111.10	1165.30	435	278	157	0	206
Z3-alpha2-base ⁿ	435	1119.89	1174.21	435	277	158	0	206
OpenSMT-SMTS-seq-base ⁿ	350	1160.58	1203.98	350	206	144	0	291
cvc5-cvc5-xyz-base ⁿ	312	1313.87	1352.66	312	166	146	0	329

SMT-COMP 2026