NB: for-in-until loop is generated as precondition loop, because the corresponding range is right-exclusive (and thus we have no problems with integer overflows).