Equality_LinearArith (Single Query Track)

Competition results for the Equality_LinearArith division in the Single Query Track. Chart

Results were generated on 2026-07-25

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

Logics:

ALIA : 707 benchmarks
AUFDTLIA : 300 benchmarks
AUFDTLIRA : 1344 benchmarks
AUFLIA : 731 benchmarks
AUFLIRA : 736 benchmarks
UFDTLIA : 554 benchmarks
UFDTLIRA : 1070 benchmarks
UFIDL : 20 benchmarks
UFLIA : 969 benchmarks
UFLRA : 7 benchmarks

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	Abstained	Timeout
cvc5-cvc5-xyz ^ne	4970 (base +4)	86167.78	86789.40	4970	364	4606	1468	0	1094
cvc5	4968	89434.31	90053.38	4968	364	4604	1470	0	1093
z3-BooledASS ^ne	4699 (base -103)	9162.90	9741.16	4699	410	4289	1739	0	1103
SMTInterpol	3440	45601.43	33151.79	3446	192	3254	2992	0	2032
UltimateEliminator+MathSAT	106	483.30	226.97	106	65	41	3064	3268	0
cvc5-cvc5-xyz-base ⁿ	4966	88422.64	89043.93	4966	364	4602	1472	0	1095
z3-BooledASS-base ⁿ	4802	10541.38	11131.31	4802	491	4311	1636	0	1100

(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	Abstained	Timeout
cvc5-cvc5-xyz ^ne	4970 (base +4)	86167.78	86789.40	4970	364	4606	1468	0	1094
cvc5	4968	89434.31	90053.38	4968	364	4604	1470	0	1093
z3-BooledASS ^ne	4699 (base -103)	9162.90	9741.16	4699	410	4289	1739	0	1103
SMTInterpol	3446	54735.88	38702.31	3446	192	3254	2992	0	2032
UltimateEliminator+MathSAT	106	483.30	226.97	106	65	41	3064	3268	0
cvc5-cvc5-xyz-base ⁿ	4966	88422.64	89043.93	4966	364	4602	1472	0	1095
z3-BooledASS-base ⁿ	4802	10541.38	11131.31	4802	491	4311	1636	0	1100

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
z3-BooledASS ^ne	410 (base -81)	2074.73	2125.50	410	410	219	5809	55
cvc5-cvc5-xyz ^ne	364 (base +0)	39626.06	39673.38	364	364	265	5809	117
cvc5	364	41443.55	41490.64	364	364	265	5809	116
SMTInterpol	192	122.72	99.53	192	192	437	5809	128
UltimateEliminator+MathSAT	65	291.15	140.43	65	65	304	6069	0
z3-BooledASS-base ⁿ	491	2496.65	2557.09	491	491	138	5809	54
cvc5-cvc5-xyz-base ⁿ	364	41480.71	41528.03	364	364	265	5809	116

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
cvc5-cvc5-xyz ^ne	4606 (base +4)	46541.71	47116.02	4606	4606	92	1740	80
cvc5	4604	47990.76	48562.75	4604	4604	94	1740	80
z3-BooledASS ^ne	4289 (base -22)	7088.17	7615.66	4289	4289	409	1740	265
SMTInterpol	3254	54613.16	38602.78	3254	3254	1444	1740	1184
UltimateEliminator+MathSAT	41	192.15	86.55	41	41	1947	4450	0
cvc5-cvc5-xyz-base ⁿ	4602	46941.93	47515.90	4602	4602	96	1740	82
z3-BooledASS-base ⁿ	4311	8044.73	8574.22	4311	4311	387	1740	286

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained
cvc5	4664	2096.94	2671.46	4664	268	4396	182	1592
cvc5-cvc5-xyz ^ne	4664 (base +0)	2135.69	2712.12	4664	268	4396	183	1591
z3-BooledASS ^ne	4657 (base -98)	1321.91	1894.13	4657	402	4255	592	1189
SMTInterpol	3292	9658.99	4789.22	3292	192	3100	673	2473
UltimateEliminator+MathSAT	106	483.30	226.97	106	65	41	3060	3272
z3-BooledASS-base ⁿ	4755	1393.94	1977.15	4755	481	4274	406	1277
cvc5-cvc5-xyz-base ⁿ	4664	2138.47	2715.03	4664	268	4396	182	1592

SMT-COMP 2026