goldsteinn wrote: The second and third proof seem unrelated? Also the first proof is incorrect w.o the `noundef` i.e: https://alive2.llvm.org/ce/z/22Bers you need to make sure the div will not trigger immediate UB. Please update your code and proofs accordingly. https://github.com/llvm/llvm-project/pull/88422