AUFLIA (Single Query Track)

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

Results were generated on 2026-07-25

Benchmarks: 731
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-xyz	cvc5

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout
cvc5-cvc5-xyz ^ne	621 (base +2)	16684.49	16762.36	621	91	530	110	104
cvc5	619	15514.57	15591.84	619	91	528	112	106
z3-BooledASS ^ne	571 (base -2)	2583.88	2654.35	571	89	482	160	146
SMTInterpol	479	6949.32	5137.31	480	44	436	251	150
UltimateEliminator+MathSAT	36	163.76	74.46	36	9	27	695	0
cvc5-cvc5-xyz-base ⁿ	619	15530.45	15608.24	619	91	528	112	106
z3-BooledASS-base ⁿ	573	2884.86	2955.48	573	89	484	158	140

(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 ^ne	621 (base +2)	16684.49	16762.36	621	91	530	110	104
cvc5	619	15514.57	15591.84	619	91	528	112	106
z3-BooledASS ^ne	571 (base -2)	2583.88	2654.35	571	89	482	160	146
SMTInterpol	480	8226.05	6003.85	480	44	436	251	150
UltimateEliminator+MathSAT	36	163.76	74.46	36	9	27	695	0
cvc5-cvc5-xyz-base ⁿ	619	15530.45	15608.24	619	91	528	112	106
z3-BooledASS-base ⁿ	573	2884.86	2955.48	573	89	484	158	140

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
cvc5-cvc5-xyz ^ne	91 (base +0)	10048.37	10060.14	91	91	7	633	2
cvc5	91	10331.59	10343.33	91	91	7	633	2
z3-BooledASS ^ne	89 (base +0)	40.44	51.46	89	89	9	633	5
SMTInterpol	44	22.41	21.12	44	44	54	633	12
UltimateEliminator+MathSAT	9	38.71	18.05	9	9	89	633	0
cvc5-cvc5-xyz-base ⁿ	91	10343.49	10355.42	91	91	7	633	2
z3-BooledASS-base ⁿ	89	39.95	50.83	89	89	9	633	5

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
cvc5-cvc5-xyz	530 (base +2)	6636.12	6702.22	530	530	8	193	8
cvc5	528	5182.98	5248.51	528	528	10	193	10
z3-BooledASS ^ne	482 (base -2)	2543.44	2602.89	482	482	56	193	51
SMTInterpol	436	8203.64	5982.73	436	436	102	193	70
UltimateEliminator+MathSAT	27	125.04	56.40	27	27	511	193	0
cvc5-cvc5-xyz-base ⁿ	528	5186.96	5252.82	528	528	10	193	10
z3-BooledASS-base ⁿ	484	2844.91	2904.65	484	484	54	193	49

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained
z3-BooledASS ^ne	558 (base -2)	188.29	256.94	558	89	469	14	159
cvc5	550	189.32	257.00	550	63	487	3	178
cvc5-cvc5-xyz ^ne	550 (base +0)	193.55	261.36	550	63	487	3	178
SMTInterpol	451	1523.14	747.98	451	44	407	57	223
UltimateEliminator+MathSAT	36	163.76	74.46	36	9	27	694	1
z3-BooledASS-base ⁿ	560	222.42	291.18	560	89	471	13	158
cvc5-cvc5-xyz-base ⁿ	550	195.25	263.27	550	63	487	3	178

SMT-COMP 2026