https://github.com/dtcxzyw commented: Can you please provide a generalized alive2 proof? See also https://llvm.org/docs/InstCombineContributorGuide.html#proofs https://github.com/llvm/llvm-project/pull/151044