QF_DT (Single Query Track)

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

Results were generated on 2026-07-25

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

Winners

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

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout
Z3-Z3++	336 (base +118)	5871.21	5913.35	336	56	280	8	8
cvc5-cvc5-xyz	225 (base +55)	40245.92	40277.08	225	45	180	119	119
Z3-alpha2 ^ne	204 (base +14)	39094.17	39010.26	204	21	183	140	140
Z3-alpha2-debug ⁿ	201	36008.82	35737.05	201	20	181	143	143
z3-BooledASS ^ne	191 (base +1)	34194.59	34220.80	191	12	179	153	153
cvc5	165	29221.13	29244.56	165	45	120	179	179
SMTInterpol	156	11405.79	7355.55	160	19	141	184	166
Z3-Z3++-base ⁿ	218	54252.40	54284.55	218	27	191	126	126
Z3-alpha2-base ⁿ	190	33154.49	33180.92	190	12	178	154	154
z3-BooledASS-base ⁿ	190	33214.62	33245.20	190	12	178	154	154
cvc5-cvc5-xyz-base ⁿ	170	33233.75	33257.88	170	45	125	174	174

(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
Z3-Z3++	336 (base +118)	5871.21	5913.35	336	56	280	8	8
cvc5-cvc5-xyz	225 (base +55)	40245.92	40277.08	225	45	180	119	119
Z3-alpha2 ^ne	204 (base +14)	39094.17	39010.26	204	21	183	140	140
Z3-alpha2-debug ⁿ	201	36008.82	35737.05	201	20	181	143	143
z3-BooledASS ^ne	191 (base +1)	34194.59	34220.80	191	12	179	153	153
cvc5	165	29221.13	29244.56	165	45	120	179	179
SMTInterpol	160	17100.75	11207.03	160	19	141	184	166
Z3-Z3++-base ⁿ	218	54252.40	54284.55	218	27	191	126	126
Z3-alpha2-base ⁿ	190	33154.49	33180.92	190	12	178	154	154
z3-BooledASS-base ⁿ	190	33214.62	33245.20	190	12	178	154	154
cvc5-cvc5-xyz-base ⁿ	170	33233.75	33257.88	170	45	125	174	174

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
Z3-Z3++	56 (base +29)	285.90	292.86	56	56	0	288	0
cvc5-cvc5-xyz ^ne	45 (base +0)	7344.28	7350.52	45	45	11	288	11
cvc5	45	7708.08	7714.65	45	45	11	288	11
Z3-alpha2	21 (base +9)	4547.27	4538.54	21	21	35	288	35
Z3-alpha2-debug ⁿ	20	3412.18	3384.74	20	20	36	288	36
SMTInterpol	19	3698.79	3473.66	19	19	37	288	37
z3-BooledASS ^ne	12 (base +0)	4374.38	4376.27	12	12	44	288	44
cvc5-cvc5-xyz-base ⁿ	45	7649.32	7655.76	45	45	11	288	11
Z3-Z3++-base ⁿ	27	10020.68	10025.17	27	27	29	288	29
Z3-alpha2-base ⁿ	12	4363.72	4365.65	12	12	44	288	44
z3-BooledASS-base ⁿ	12	4367.49	4369.89	12	12	44	288	44

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	64	0
Z3-alpha2 ^ne	183 (base +5)	34546.90	34471.72	183	183	97	64	97
Z3-alpha2-debug ⁿ	181	32596.64	32352.31	181	181	99	64	99
cvc5-cvc5-xyz	180 (base +55)	32901.65	32926.56	180	180	100	64	100
z3-BooledASS ^ne	179 (base +1)	29820.22	29844.53	179	179	101	64	101
SMTInterpol	141	13401.96	7733.37	141	141	139	64	121
cvc5	120	21513.05	21529.91	120	120	160	64	160
Z3-Z3++-base ⁿ	191	44231.72	44259.38	191	191	89	64	89
Z3-alpha2-base ⁿ	178	28790.77	28815.27	178	178	102	64	102
z3-BooledASS-base ⁿ	178	28847.13	28875.31	178	178	102	64	102
cvc5-cvc5-xyz-base ⁿ	125	25584.43	25602.12	125	125	155	64	155

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	38
SMTInterpol	112	877.12	410.51	112	10	102	232
cvc5-cvc5-xyz ^ne	111 (base +35)	402.98	416.59	111	10	101	233
Z3-alpha2 ^ne	95 (base +5)	658.45	618.67	95	10	85	249
Z3-alpha2-debug ⁿ	95	862.75	733.76	95	10	85	249
z3-BooledASS ^ne	90 (base +0)	271.62	282.59	90	4	86	254
cvc5	76	188.76	198.15	76	9	67	268
Z3-Z3++-base ⁿ	90	213.81	225.03	90	5	85	254
Z3-alpha2-base ⁿ	90	273.77	284.87	90	4	86	254
z3-BooledASS-base ⁿ	90	275.61	288.61	90	4	86	254
cvc5-cvc5-xyz-base ⁿ	76	186.18	195.61	76	9	67	268

SMT-COMP 2026