[llvm] [ConstraintElim] Simplify `sadd_with_overflow` if A and B have different signs (PR #135784)

[Florian Hahn via llvm-commits]

https://github.com/fhahn commented:

Could you add an Alive2 proof showing this transform is valid given the precondition for completeness?



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