AUFLIRA (Single Query Track)

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

Results were generated on 2026-07-25

Benchmarks: 736
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-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	694 (base +1)	2324.18	2410.69	694	0	694	42	42
cvc5	693	2689.25	2775.30	693	0	693	43	43
z3-BooledASS ^ne	677 (base +0)	2247.16	2330.82	677	16	661	59	57
SMTInterpol	525	5095.10	4185.45	526	0	526	210	160
UltimateEliminator+MathSAT	3	15.68	6.76	3	0	3	733	0
cvc5-cvc5-xyz-base ⁿ	693	2694.50	2780.96	693	0	693	43	43
z3-BooledASS-base ⁿ	677	2255.76	2339.14	677	16	661	59	49

(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	694 (base +1)	2324.18	2410.69	694	0	694	42	42
cvc5	693	2689.25	2775.30	693	0	693	43	43
z3-BooledASS ^ne	677 (base +0)	2247.16	2330.82	677	16	661	59	57
SMTInterpol	526	6672.73	5207.04	526	0	526	210	160
UltimateEliminator+MathSAT	3	15.68	6.76	3	0	3	733	0
cvc5-cvc5-xyz-base ⁿ	693	2694.50	2780.96	693	0	693	43	43
z3-BooledASS-base ⁿ	677	2255.76	2339.14	677	16	661	59	49

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
z3-BooledASS ^ne	16 (base +0)	1393.03	1395.20	16	16	0	720	0
SMTInterpol	0	0.00	0.00	0	0	16	720	16
UltimateEliminator+MathSAT	0	0.00	0.00	0	0	16	720	0
cvc5	0	0.00	0.00	0	0	16	720	16
cvc5-cvc5-xyz ^ne	0 (base +0)	0.00	0.00	0	0	16	720	16
z3-BooledASS-base ⁿ	16	1398.27	1400.41	16	16	0	720	0
cvc5-cvc5-xyz-base ⁿ	0	0.00	0.00	0	0	16	720	16

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
cvc5-cvc5-xyz	694 (base +1)	2324.18	2410.69	694	694	0	42	0
cvc5	693	2689.25	2775.30	693	693	1	42	1
z3-BooledASS ^ne	661 (base +0)	854.13	935.62	661	661	33	42	33
SMTInterpol	526	6672.73	5207.04	526	526	168	42	118
UltimateEliminator+MathSAT	3	15.68	6.76	3	3	691	42	0
cvc5-cvc5-xyz-base ⁿ	693	2694.50	2780.96	693	693	1	42	1
z3-BooledASS-base ⁿ	661	857.49	938.73	661	661	33	42	29

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained
z3-BooledASS ^ne	669 (base +0)	293.42	375.86	669	12	657	0	67
cvc5	666	127.29	209.83	666	0	666	0	70
cvc5-cvc5-xyz ^ne	666 (base +0)	128.54	211.39	666	0	666	0	70
SMTInterpol	509	714.38	414.10	509	0	509	0	227
UltimateEliminator+MathSAT	3	15.68	6.76	3	0	3	733	0
z3-BooledASS-base ⁿ	669	292.16	374.33	669	12	657	0	67
cvc5-cvc5-xyz-base ⁿ	666	129.21	212.00	666	0	666	0	70

SMT-COMP 2026