ALIA (Single Query Track)

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

Results were generated on 2026-07-25

Benchmarks: 707
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	UltimateEliminator+MathSAT	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	181 (base +4)	11192.43	11215.62	181	30	151	526	264
cvc5	177	12455.81	12478.73	177	30	147	530	265
SMTInterpol	132	5199.85	3820.23	133	11	122	574	182
z3-BooledASS ^ne	127 (base -96)	33.03	48.77	127	84	43	580	29
UltimateEliminator+MathSAT	67	303.87	145.76	67	56	11	640	0
z3-BooledASS-base ⁿ	223	54.91	82.28	223	163	60	484	108
cvc5-cvc5-xyz-base ⁿ	177	12474.39	12497.19	177	30	147	530	265

(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	181 (base +4)	11192.43	11215.62	181	30	151	526	264
cvc5	177	12455.81	12478.73	177	30	147	530	265
SMTInterpol	133	6989.56	4577.33	133	11	122	574	182
z3-BooledASS ^ne	127 (base -96)	33.03	48.77	127	84	43	580	29
UltimateEliminator+MathSAT	67	303.87	145.76	67	56	11	640	0
z3-BooledASS-base ⁿ	223	54.91	82.28	223	163	60	484	108
cvc5-cvc5-xyz-base ⁿ	177	12474.39	12497.19	177	30	147	530	265

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
z3-BooledASS ^ne	84 (base -79)	25.40	35.78	84	84	159	464	0
UltimateEliminator+MathSAT	56	252.44	122.37	56	56	187	464	0
cvc5-cvc5-xyz ^ne	30 (base +0)	5001.41	5005.47	30	30	213	464	88
cvc5	30	6606.21	6610.43	30	30	213	464	87
SMTInterpol	11	10.12	6.64	11	11	232	464	59
z3-BooledASS-base ⁿ	163	43.64	63.58	163	163	80	464	1
cvc5-cvc5-xyz-base ⁿ	30	6614.91	6619.07	30	30	213	464	87

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
cvc5-cvc5-xyz	151 (base +4)	6191.02	6210.15	151	151	26	530	14
cvc5	147	5849.60	5868.30	147	147	30	530	16
SMTInterpol	122	6979.44	4570.69	122	122	55	530	27
z3-BooledASS ^ne	43 (base -17)	7.64	12.99	43	43	134	530	18
UltimateEliminator+MathSAT	11	51.43	23.38	11	11	166	530	0
cvc5-cvc5-xyz-base ⁿ	147	5859.48	5878.12	147	147	30	530	16
z3-BooledASS-base ⁿ	60	11.27	18.70	60	60	117	530	63

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained
cvc5	135	112.32	129.00	135	12	123	159	413
cvc5-cvc5-xyz ^ne	135 (base +0)	113.61	130.23	135	12	123	159	413
z3-BooledASS ^ne	127 (base -96)	33.03	48.77	127	84	43	544	36
SMTInterpol	110	512.02	371.88	110	11	99	345	252
UltimateEliminator+MathSAT	67	303.87	145.76	67	56	11	640	0
z3-BooledASS-base ⁿ	223	54.91	82.28	223	163	60	362	122
cvc5-cvc5-xyz-base ⁿ	135	114.45	131.07	135	12	123	159	413

SMT-COMP 2026