QF_ADT_LinArith (Model Validation Track)

Competition results for the QF_ADT_LinArith division in the Model Validation Track. Chart

Results were generated on 2026-07-25

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

Logics:

QF_ALIA : 101 benchmarks
QF_AUFLIA : 300 benchmarks
QF_AX : 272 benchmarks
QF_UFDTLIA : 45 benchmarks
QF_UFDTLIRA : 80 benchmarks

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24 seconds Performance (parallel)
cvc5	cvc5	cvc5	-	SMTInterpol

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
cvc5	765	9067.27	9163.09	765	765	33	0	33
SMTInterpol	764	3006.98	2177.14	764	764	34	0	2
Yices2	661	1143.85	1225.49	661	661	12	125	11
z3-BooledASS ^ne	391 (base +0)	11215.49	11264.36	391	391	407	0	20
z3-BooledASS-base ⁿ	391	11359.50	11408.81	391	391	407	0	20

(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	Unsolved	Abstained	Timeout
cvc5	765	9067.27	9163.09	765	765	33	0	33
SMTInterpol	764	3006.98	2177.14	764	764	34	0	2
Yices2	661	1143.85	1225.49	661	661	12	125	11
z3-BooledASS ^ne	391 (base +0)	11215.49	11264.36	391	391	407	0	20
z3-BooledASS-base ⁿ	391	11359.50	11408.81	391	391	407	0	20

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
cvc5	765	9067.27	9163.09	765	765	33	0	33
SMTInterpol	764	3006.98	2177.14	764	764	34	0	2
Yices2	661	1143.85	1225.49	661	661	12	125	11
z3-BooledASS ^ne	391 (base +0)	11215.49	11264.36	391	391	407	0	20
z3-BooledASS-base ⁿ	391	11359.50	11408.81	391	391	407	0	20

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained
SMTInterpol	753	1208.50	642.00	753	753	10	35
cvc5	736	688.80	780.22	736	736	0	62
Yices2	660	160.11	241.59	660	660	0	138
z3-BooledASS ^ne	368 (base +0)	399.36	444.51	368	368	378	52
z3-BooledASS-base ⁿ	368	397.59	442.96	368	368	378	52

SMT-COMP 2026