Right but I guess the point I'm getting at is that termination seems neither necessary nor sufficient to me. A loop (or nested loops...) that goes up to 2^63 may as well be infinite, so on the face of it it's not obvious why boundedness gets you anywhere by itself—you'd need to prove something stronger anyway. Conversely, it's not impossible to have loops that nevertheless (provably) terminate within N instructions. But if you're already bounding the number of instructions, why do you need bounded loops to begin with? Is that a necessary lemma of some sort before the algorithm is capable of proving something stronger? At first glance I don't see why the simulation (BMC?) approach you suggested would require bounded loops, since it would seem it might be capable of proving the termination of some unbounded loops within 1M instructions too.