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

[Antonio Frighetto via llvm-commits]

antoniofrighetto wrote:

> Alive2 struggles (times out) with 32 bit vectors for this particular proof: https://alive2.llvm.org/ce/z/S-78k- In my z3 proof, even 16 bit took quite some times.

Please confirm if I shrink the inputs correctly: https://alive2.llvm.org/ce/z/AABL4v (I guess you missed poison-generating flags in the source, as otherwise your target function is defined for a less pairs of inputs than the source.)

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