[llvm] KnownBits: refine srem for high-bits (PR #109121)

[Ramkumar Ramachandra via llvm-commits]

artagnon wrote:

> Alive2 proof: https://alive2.llvm.org/ce/z/Ugh-Dq

I haven't run tests locally, so relying on CI for latest change. In the meantime, do we have any opinions on whether this Alive2 proof is useful to include with the implementation?

https://github.com/llvm/llvm-project/pull/109121