Rule #2 is "Fixed Upper Bound for Loops". Although they define this flexibily as "It should be possible for a verification tool to prove statically that a pres

Rule #2 is "Fixed Upper Bound for Loops". Although they define this flexibily as "It should be possible for a verification tool to prove statically that a preset upper-bound on the number of iteration of a loop can’t be exceeded." So any loops where they can in fact write a verifier is simple enough.