<div dir="ltr">> It looks like you are correct, it could be TreeSet instead. Please submit the PR?<div><br><div>Filed <a href="https://bugs.openjdk.org/browse/CODETOOLS-7903321">https://bugs.openjdk.org/browse/CODETOOLS-7903321</a> to follow up.<br></div></div><div>I will submit the PR soon.</div></div>