artagnon wrote: Sorry, this is incorrect, and there are subtle problems with it. Is it possible to experiment with an Alive2 proof for this example? (I believe Alive2 doesn't handle loops) https://github.com/llvm/llvm-project/pull/108973