RSilicon wrote: I removed the nuw cases from my proof because they are actually malformed IR and are not covered at all as they are impossible to run into assuming the IR isn't malformed. https://github.com/llvm/llvm-project/pull/100008