The idea (I assume) is to let compilers optimize away loops without determining that they terminate. I.e. the rule is more aimed at loops which would terminate,

The idea (I assume) is to let compilers optimize away loops without determining that they terminate. I.e. the rule is more aimed at loops which would terminate, but this lets compilers avoid proving that they do in fact terminate.