AUFDTLIA (Single Query Track)

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

Results were generated on 2026-07-25

Benchmarks: 300
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	cvc5	cvc5	cvc5

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout
cvc5	295	23090.26	23128.30	295	85	210	5	5
cvc5-cvc5-xyz ^ne	295 (base +0)	23162.09	23200.70	295	85	210	5	5
z3-BooledASS ^ne	254 (base +0)	618.59	649.68	254	40	214	46	46
SMTInterpol	192	1669.45	1055.30	192	1	191	108	38
cvc5-cvc5-xyz-base ⁿ	295	23092.48	23130.79	295	85	210	5	5
z3-BooledASS-base ⁿ	254	621.99	653.15	254	40	214	46	46

(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	295	23090.26	23128.30	295	85	210	5	5
cvc5-cvc5-xyz ^ne	295 (base +0)	23162.09	23200.70	295	85	210	5	5
z3-BooledASS ^ne	254 (base +0)	618.59	649.68	254	40	214	46	46
SMTInterpol	192	1669.45	1055.30	192	1	191	108	38
cvc5-cvc5-xyz-base ⁿ	295	23092.48	23130.79	295	85	210	5	5
z3-BooledASS-base ⁿ	254	621.99	653.15	254	40	214	46	46

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
cvc5	85	23011.06	23023.10	85	85	0	215	0
cvc5-cvc5-xyz ^ne	85 (base +0)	23081.37	23093.83	85	85	0	215	0
z3-BooledASS ^ne	40 (base +0)	6.76	11.63	40	40	45	215	45
SMTInterpol	1	0.63	0.54	1	1	84	215	32
cvc5-cvc5-xyz-base ⁿ	85	23012.02	23024.27	85	85	0	215	0
z3-BooledASS-base ⁿ	40	6.77	11.63	40	40	45	215	45

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
z3-BooledASS ^ne	214 (base +0)	611.83	638.05	214	214	1	85	1
cvc5	210	79.21	105.20	210	210	5	85	5
cvc5-cvc5-xyz ^ne	210 (base +0)	80.71	106.87	210	210	5	85	5
SMTInterpol	191	1668.82	1054.77	191	191	24	85	6
z3-BooledASS-base ⁿ	214	615.22	641.52	214	214	1	85	1
cvc5-cvc5-xyz-base ⁿ	210	80.45	106.51	210	210	5	85	5

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained
cvc5	250	92.17	122.87	250	40	210	0	50
cvc5-cvc5-xyz ^ne	250 (base +0)	94.45	125.37	250	40	210	0	50
z3-BooledASS ^ne	249 (base +0)	51.05	81.47	249	40	209	0	51
SMTInterpol	182	735.58	297.10	182	1	181	63	55
cvc5-cvc5-xyz-base ⁿ	250	94.19	125.03	250	40	210	0	50
z3-BooledASS-base ⁿ	249	51.66	82.17	249	40	209	0	51

SMT-COMP 2026