[llvm] [ValueTracking] Refine known bits for linear interpolation patterns (PR #166378)

[Valeriy Savchenko via llvm-commits]

SavchenkoValeriy wrote:

> Can you please provide a generalized alive2 proof? See https://llvm.org/docs/InstCombineContributorGuide.html#proofs.

I believe I answered it here:
https://github.com/llvm/llvm-project/pull/166378#issuecomment-3487318866

In short, I'm not improving any particular transformation but an analysis and analysis can't be proven via alive2. I provide a general z3 proof for the exact logic that I encoded. Please tell me if you have any questions about that proof.

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