On Fri, 2025-07-25 at 17:21 +0800, Shung-Hsi Yu wrote: [...] > Beside going through the reasoning, I also played with CBMC a bit to > double check that as far as a single run of __reg_deduce_bounds() is > concerned (and that the register state matches certain handwavy > expectations), the change indeed still preserve the original behavior. Interesting, thank you!
