dtcxzyw 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) You can try with `-src-unroll/-tgt-unroll`. https://github.com/llvm/llvm-project/pull/108973