QF_AUFBVLIA (Incremental Track)

Competition results for the QF_AUFBVLIA logic in the Incremental Track. Chart

Results were generated on 2026-07-25

Benchmarks: 300
Time Limit: 1200 seconds
Memory Limit: 30720 GB

Winners

Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24 seconds Performance (parallel)
Yices2	-	-	Yices2

Parallel Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Unsolved	Timeout	Memout
Yices2	552	6611.27	6610.27	300	4	0
SMTInterpol	522	73302.72	72005.33	300	34	0
cvc5	509	70854.26	70843.36	300	46	1
z3-BooledASS ^ne	0 (base +0)	1.78	2.27	300	0	0
z3-BooledASS-base ⁿ	0	0.00	0.00	300	0	0

(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

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Unsolved	Abstained
Yices2	525	701.17	701.17	284	16
cvc5	308	790.10	790.10	172	128
SMTInterpol	301	1028.15	1028.15	164	136
z3-BooledASS ^ne	0 (base +0)	1.78	2.27	300	0
z3-BooledASS-base ⁿ	0	0.00	0.00	300	0

SMT-COMP 2026

SMT-COMP 2026

QF_AUFBVLIA (Incremental Track)

Winners

Parallel Performance Performance

24 seconds Performance Performance