sanjoy added a subscriber: sanjoy. sanjoy added a comment. I don't think you need to check for no-wrap -- a non-zero `B` should be sufficient to prove `A + B != A`. Repository: rL LLVM http://reviews.llvm.org/D12801