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

[Florian Hahn via llvm-commits]

https://github.com/fhahn commented:

> Since that is true for arbitrary a, b, c and d within our constraints, we can
conclude that:
> 
> max(a * (b - c) + c * d) <= max(max(a), max(d)) * max(b) = U

Would it be possible to add an Alive2 proof for the conclusion?

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