[eru]

See https://blog.regehr.org/archives/140 for a longer discussion.

(And to make it closer to our situation, assume that the loop being executed was looking for something that actually has a counterexample that could be found after a long time; instead of Fermat's last theorem.)

[pingyong]

What point is there in deleting side-effect free loops though? Literally the only use for those is to trap the control flow.

[bluGill]

The only intentional use. However when writing generic code you often have code lines that after several levels of code inline reduce to that example.

[pingyong]

So, generic code with a loop, which, depending on parameters, sometimes has side effects and sometimes doesn't, and in the case that it doesn't have side effects it is still not easy to recognize if the loop terminates?

I suppose that is possible, although I'm having a hard time coming up with any reasonable examples.