QF_UFDTLIA (Single Query Track)

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

Results were generated on 2026-07-25

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

Winners

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

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout
cvc5-cvc5-xyz	62 (base +23)	4492.82	4500.75	62	54	8	14	14
SMTInterpol	58	10330.18	9212.03	58	45	13	18	18
z3-BooledASS ^ne	55 (base +0)	662.97	669.78	55	43	12	21	21
cvc5	40	6357.90	6363.55	40	32	8	36	36
z3-BooledASS-base ⁿ	55	662.43	669.42	55	43	12	21	21
cvc5-cvc5-xyz-base ⁿ	39	6002.25	6007.76	39	31	8	37	37

(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
cvc5-cvc5-xyz	62 (base +23)	4492.82	4500.75	62	54	8	14	14
SMTInterpol	58	10330.18	9212.03	58	45	13	18	18
z3-BooledASS ^ne	55 (base +0)	662.97	669.78	55	43	12	21	21
cvc5	40	6357.90	6363.55	40	32	8	36	36
z3-BooledASS-base ⁿ	55	662.43	669.42	55	43	12	21	21
cvc5-cvc5-xyz-base ⁿ	39	6002.25	6007.76	39	31	8	37	37

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
cvc5-cvc5-xyz	54 (base +23)	4446.27	4453.23	54	54	1	21	1
SMTInterpol	45	8057.70	7204.37	45	45	10	21	10
z3-BooledASS ^ne	43 (base +0)	490.79	496.10	43	43	12	21	12
cvc5	32	5728.86	5733.49	32	32	23	21	23
z3-BooledASS-base ⁿ	43	491.17	496.63	43	43	12	21	12
cvc5-cvc5-xyz-base ⁿ	31	5359.01	5363.42	31	31	24	21	24

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
SMTInterpol	13	2272.47	2007.66	13	13	0	63	0
z3-BooledASS ^ne	12 (base +0)	172.18	173.68	12	12	1	63	1
cvc5-cvc5-xyz ^ne	8 (base +0)	46.55	47.52	8	8	5	63	5
cvc5	8	629.05	630.06	8	8	5	63	5
z3-BooledASS-base ⁿ	12	171.26	172.79	12	12	1	63	1
cvc5-cvc5-xyz-base ⁿ	8	643.24	644.34	8	8	5	63	5

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Abstained
z3-BooledASS ^ne	50 (base +0)	243.40	249.53	50	42	8	26
cvc5-cvc5-xyz ^ne	43 (base +20)	278.08	283.36	43	35	8	33
cvc5	24	200.80	203.74	24	18	6	52
SMTInterpol	21	364.68	169.55	21	16	5	55
z3-BooledASS-base ⁿ	50	244.73	251.03	50	42	8	26
cvc5-cvc5-xyz-base ⁿ	23	205.48	208.38	23	17	6	53

SMT-COMP 2026