QF_Datatypes (Single Query Track)

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

Results were generated on 2026-07-25

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

Logics:

QF_DT : 344 benchmarks
QF_UFDT : 200 benchmarks

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24 seconds Performance (parallel)
cvc5-cvc5-xyz	cvc5-cvc5-xyz	cvc5	Z3-Z3++	SMTInterpol

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout
cvc5-cvc5-xyz	398 (base +55)	91890.89	91947.93	398	128	270	146	0	146
Z3-Z3++	336 (base +118)	5871.21	5913.35	336	56	280	8	200	8
cvc5	334	79751.94	79800.97	334	128	206	210	0	210
Z3-alpha2	324 (base +31)	68023.94	67891.72	324	49	275	220	0	220
Z3-alpha2-debug ⁿ	321	65162.10	64728.79	321	48	273	223	0	223
z3-BooledASS ^ne	293 (base +1)	61391.13	61432.25	293	21	272	251	0	251
SMTInterpol	186	18631.32	13103.03	191	43	148	353	0	315
cvc5-cvc5-xyz-base ⁿ	343	84451.22	84501.58	343	128	215	201	0	201
Z3-alpha2-base ⁿ	293	61708.83	61750.62	293	22	271	251	0	251
z3-BooledASS-base ⁿ	292	60780.43	60829.28	292	21	271	252	0	252
Z3-Z3++-base ⁿ	218	54252.40	54284.55	218	27	191	126	200	126

(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
cvc5-cvc5-xyz	398 (base +55)	91890.89	91947.93	398	128	270	146	0	146
Z3-Z3++	336 (base +118)	5871.21	5913.35	336	56	280	8	200	8
cvc5	334	79751.94	79800.97	334	128	206	210	0	210
Z3-alpha2	324 (base +31)	68023.94	67891.72	324	49	275	220	0	220
Z3-alpha2-debug ⁿ	321	65162.10	64728.79	321	48	273	223	0	223
z3-BooledASS ^ne	293 (base +1)	61391.13	61432.25	293	21	272	251	0	251
SMTInterpol	191	25585.73	17435.47	191	43	148	353	0	315
cvc5-cvc5-xyz-base ⁿ	343	84451.22	84501.58	343	128	215	201	0	201
Z3-alpha2-base ⁿ	293	61708.83	61750.62	293	22	271	251	0	251
z3-BooledASS-base ⁿ	292	60780.43	60829.28	292	21	271	252	0	252
Z3-Z3++-base ⁿ	218	54252.40	54284.55	218	27	191	126	200	126

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
cvc5-cvc5-xyz ^ne	128 (base +0)	16088.69	16106.03	128	128	28	388	28
cvc5	128	16528.72	16546.59	128	128	28	388	28
Z3-Z3++	56 (base +29)	285.90	292.86	56	56	0	488	0
Z3-alpha2	49 (base +27)	9445.82	9425.42	49	49	107	388	107
Z3-alpha2-debug ⁿ	48	8359.92	8294.50	48	48	108	388	108
SMTInterpol	43	8562.73	7991.08	43	43	113	388	113
z3-BooledASS ^ne	21 (base +0)	9220.22	9223.68	21	21	135	388	135
cvc5-cvc5-xyz-base ⁿ	128	16485.47	16503.24	128	128	28	388	28
Z3-Z3++-base ⁿ	27	10020.68	10025.17	27	27	29	488	29
Z3-alpha2-base ⁿ	22	10335.32	10338.99	22	22	134	388	134
z3-BooledASS-base ⁿ	21	9248.03	9252.26	21	21	135	388	135

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
Z3-Z3++	280 (base +89)	5585.30	5620.49	280	280	0	264	0
Z3-alpha2 ^ne	275 (base +4)	58578.12	58466.30	275	275	105	164	105
Z3-alpha2-debug ⁿ	273	56802.18	56434.29	273	273	107	164	107
z3-BooledASS ^ne	272 (base +1)	52170.91	52208.58	272	272	108	164	108
cvc5-cvc5-xyz	270 (base +55)	75802.20	75841.90	270	270	110	164	110
cvc5	206	63223.23	63254.38	206	206	174	164	174
SMTInterpol	148	17023.01	9444.39	148	148	232	164	194
Z3-alpha2-base ⁿ	271	51373.50	51411.64	271	271	109	164	109
z3-BooledASS-base ⁿ	271	51532.40	51577.01	271	271	109	164	109
cvc5-cvc5-xyz-base ⁿ	215	67965.75	67998.34	215	215	165	164	165
Z3-Z3++-base ⁿ	191	44231.72	44259.38	191	191	89	264	89

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Abstained
Z3-Z3++ ^ne	306 (base +216)	1291.60	1329.57	306	56	250	238
cvc5-cvc5-xyz ^ne	131 (base +35)	678.98	695.10	131	28	103	413
SMTInterpol	119	1015.78	484.87	119	17	102	425
Z3-alpha2 ^ne	109 (base +15)	875.40	829.65	109	19	90	435
Z3-alpha2-debug ⁿ	109	1109.67	961.21	109	19	90	435
z3-BooledASS ^ne	95 (base +0)	375.33	386.90	95	4	91	449
cvc5	95	444.59	456.37	95	27	68	449
cvc5-cvc5-xyz-base ⁿ	96	463.85	475.79	96	27	69	448
z3-BooledASS-base ⁿ	95	380.23	394.15	95	4	91	449
Z3-alpha2-base ⁿ	94	354.26	365.86	94	4	90	450
Z3-Z3++-base ⁿ	90	213.81	225.03	90	5	85	454

SMT-COMP 2026