AUFBVDTLIA (Single Query Track)

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

Results were generated on 2026-07-25

Benchmarks: 556
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-cvc5-xyz ^ne	271 (base +0)	46756.10	46793.64	271	133	138	285	259
cvc5	271	46806.64	46843.92	271	133	138	285	259
z3-BooledASS ^ne	133 (base -3)	1226.91	1243.33	133	37	96	423	388
SMTInterpol	95	318.88	142.57	95	1	94	461	337
cvc5-cvc5-xyz-base ⁿ	271	46810.86	46848.45	271	133	138	285	259
z3-BooledASS-base ⁿ	136	3539.10	3556.10	136	39	97	420	386

(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	271 (base +0)	46756.10	46793.64	271	133	138	285	259
cvc5	271	46806.64	46843.92	271	133	138	285	259
z3-BooledASS ^ne	133 (base -3)	1226.91	1243.33	133	37	96	423	388
SMTInterpol	95	318.88	142.57	95	1	94	461	337
cvc5-cvc5-xyz-base ⁿ	271	46810.86	46848.45	271	133	138	285	259
z3-BooledASS-base ⁿ	136	3539.10	3556.10	136	39	97	420	386

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
cvc5-cvc5-xyz ^ne	133 (base +0)	33092.17	33111.30	133	133	0	423	0
cvc5	133	33142.75	33161.77	133	133	0	423	0
z3-BooledASS ^ne	37 (base -2)	927.06	931.69	37	37	96	423	94
SMTInterpol	1	0.97	0.61	1	1	132	423	80
cvc5-cvc5-xyz-base ⁿ	133	33146.30	33165.56	133	133	0	423	0
z3-BooledASS-base ⁿ	39	1865.41	1870.34	39	39	94	423	91

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
cvc5	138	13663.90	13682.15	138	138	0	418	0
cvc5-cvc5-xyz ^ne	138 (base +0)	13663.93	13682.34	138	138	0	418	0
z3-BooledASS ^ne	96 (base -1)	299.85	311.65	96	96	42	418	39
SMTInterpol	94	317.92	141.97	94	94	44	418	44
cvc5-cvc5-xyz-base ⁿ	138	13664.55	13682.88	138	138	0	418	0
z3-BooledASS-base ⁿ	97	1673.69	1685.76	97	97	41	418	38

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained
z3-BooledASS ^ne	128 (base +0)	61.61	77.33	128	34	94	9	419
cvc5-cvc5-xyz ^ne	106 (base +1)	43.27	56.41	106	6	100	1	449
cvc5	105	42.00	55.02	105	5	100	1	450
SMTInterpol	95	318.88	142.57	95	1	94	109	352
z3-BooledASS-base ⁿ	128	53.05	68.76	128	36	92	9	419
cvc5-cvc5-xyz-base ⁿ	105	42.68	55.78	105	5	100	1	450

SMT-COMP 2026