Ah I see, thanks for running it! Yeah so it's not this particular loop that's interesting (there's probably always going to be some simple-looking loop a solver can't prove—and I'm sure we could come up with simpler examples), but rather, the interesting question is whether it can figure out
anything that doesn't map directly to bounded for/while/do-while loops. It's interesting because:
1. If the answer is no, then what is the precise reason? Is there a legitimate reason for it? After all, a bounded loop that loops for too long is just as bad as one that never terminates, so clearly they need a way to upper-bound the instruction count for any loop—at which point, why is the bound even relevant? The only reason I can think of is that they do simplistic analysis (e.g. multiplying the bounds on nested loops to naively approximate an overall bound), but your examples suggest they have more sophisticated (SMT/BMC?) solvers, and it's not obvious to me why a modern solver would fail on all unbounded loops.
2. If the answer is yes, then it would seem they actually do allow unbounded loops after all?
The other possibility is they're using the word "bounded" differently (e.g. maybe as a synonym for "terminating"), in which case it would be true that they would need bounded loops by definition.
