           *******************************************************
                       Semantic Analysis of SPARK Text
                             Examiner GPL Edition

           *******************************************************


                procedure Zone_File_Parser.ParseControlLine




For path(s) from start to precondition check associated with statement of line 626:

procedure_parsecontrolline_1.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           neworigin, [i___1]) >= character__first) and (element(
           neworigin, [i___1]) <= character__last))) .
H2:    newttl >= unsigned_types__unsigned32__first .
H3:    newttl <= unsigned_types__unsigned32__last .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H5:    zlength >= rr_type__linelengthindex__first .
H6:    zlength <= rr_type__linelengthindex__last .
H7:    1 >= rr_type__linelengthindex__first .
H8:    1 <= rr_type__linelengthindex__last .
        ->
C1:    1 >= rr_type__linelengthindex__first .
C2:    1 <= rr_type__linelengthindex__last .
C3:    zlength >= rr_type__linelengthindex__first .
C4:    zlength <= rr_type__linelengthindex__last .
C5:    1 <= zlength .
 

For path(s) from start to run-time check associated with statement of line 626:

procedure_parsecontrolline_2.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           neworigin, [i___1]) >= character__first) and (element(
           neworigin, [i___1]) <= character__last))) .
H2:    newttl >= unsigned_types__unsigned32__first .
H3:    newttl <= unsigned_types__unsigned32__last .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H5:    zlength >= rr_type__linelengthindex__first .
H6:    zlength <= rr_type__linelengthindex__last .
H7:    1 >= rr_type__linelengthindex__first .
H8:    1 <= rr_type__linelengthindex__last .
H9:    1 >= rr_type__linelengthindex__first .
H10:   1 <= rr_type__linelengthindex__last .
H11:   zlength >= rr_type__linelengthindex__first .
H12:   zlength <= rr_type__linelengthindex__last .
H13:   1 <= zlength .
H14:   begidx__1 <= endidx__1 .
H15:   begidx__1 <= zlength .
H16:   endidx__1 <= zlength .
H17:   (foundtype__1 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__1) and (i_ <= endidx__1)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H18:   begidx__1 >= rr_type__linelengthindex__first .
H19:   begidx__1 <= rr_type__linelengthindex__last .
H20:   endidx__1 >= rr_type__linelengthindex__first .
H21:   endidx__1 <= rr_type__linelengthindex__last .
H22:   foundtype__1 >= rr_type__rritemtype__first .
H23:   foundtype__1 <= rr_type__rritemtype__last .
        ->
C1:    foundtype__1 >= rr_type__rritemtype__first .
C2:    foundtype__1 <= rr_type__rritemtype__last .
C3:    endidx__1 >= rr_type__linelengthindex__first .
C4:    endidx__1 <= rr_type__linelengthindex__last .
C5:    begidx__1 >= rr_type__linelengthindex__first .
C6:    begidx__1 <= rr_type__linelengthindex__last .
 

For path(s) from start to run-time check associated with statement of line 630:

procedure_parsecontrolline_3.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           neworigin, [i___1]) >= character__first) and (element(
           neworigin, [i___1]) <= character__last))) .
H2:    newttl >= unsigned_types__unsigned32__first .
H3:    newttl <= unsigned_types__unsigned32__last .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H5:    zlength >= rr_type__linelengthindex__first .
H6:    zlength <= rr_type__linelengthindex__last .
H7:    1 >= rr_type__linelengthindex__first .
H8:    1 <= rr_type__linelengthindex__last .
H9:    1 >= rr_type__linelengthindex__first .
H10:   1 <= rr_type__linelengthindex__last .
H11:   zlength >= rr_type__linelengthindex__first .
H12:   zlength <= rr_type__linelengthindex__last .
H13:   1 <= zlength .
H14:   begidx__1 <= endidx__1 .
H15:   begidx__1 <= zlength .
H16:   endidx__1 <= zlength .
H17:   (foundtype__1 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__1) and (i_ <= endidx__1)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H18:   begidx__1 >= rr_type__linelengthindex__first .
H19:   begidx__1 <= rr_type__linelengthindex__last .
H20:   endidx__1 >= rr_type__linelengthindex__first .
H21:   endidx__1 <= rr_type__linelengthindex__last .
H22:   foundtype__1 >= rr_type__rritemtype__first .
H23:   foundtype__1 <= rr_type__rritemtype__last .
H24:   foundtype__1 >= rr_type__rritemtype__first .
H25:   foundtype__1 <= rr_type__rritemtype__last .
H26:   endidx__1 >= rr_type__linelengthindex__first .
H27:   endidx__1 <= rr_type__linelengthindex__last .
H28:   begidx__1 >= rr_type__linelengthindex__first .
H29:   begidx__1 <= rr_type__linelengthindex__last .
H30:   foundtype__1 >= rr_type__rritemtype__first .
H31:   foundtype__1 <= rr_type__rritemtype__last .
H32:   foundtype__1 = rr_type__control .
H33:   begidx__1 >= rr_type__linelengthindex__first .
H34:   begidx__1 <= rr_type__linelengthindex__last .
H35:   endidx__1 >= rr_type__linelengthindex__first .
H36:   endidx__1 <= rr_type__linelengthindex__last .
        ->
C1:    endidx__1 - 6 >= integer__base__first .
C2:    endidx__1 - 6 <= integer__base__last .
 

For path(s) from start to run-time check associated with statement of line 631:

procedure_parsecontrolline_4.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           neworigin, [i___1]) >= character__first) and (element(
           neworigin, [i___1]) <= character__last))) .
H2:    newttl >= unsigned_types__unsigned32__first .
H3:    newttl <= unsigned_types__unsigned32__last .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H5:    zlength >= rr_type__linelengthindex__first .
H6:    zlength <= rr_type__linelengthindex__last .
H7:    1 >= rr_type__linelengthindex__first .
H8:    1 <= rr_type__linelengthindex__last .
H9:    1 >= rr_type__linelengthindex__first .
H10:   1 <= rr_type__linelengthindex__last .
H11:   zlength >= rr_type__linelengthindex__first .
H12:   zlength <= rr_type__linelengthindex__last .
H13:   1 <= zlength .
H14:   begidx__1 <= endidx__1 .
H15:   begidx__1 <= zlength .
H16:   endidx__1 <= zlength .
H17:   (foundtype__1 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__1) and (i_ <= endidx__1)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H18:   begidx__1 >= rr_type__linelengthindex__first .
H19:   begidx__1 <= rr_type__linelengthindex__last .
H20:   endidx__1 >= rr_type__linelengthindex__first .
H21:   endidx__1 <= rr_type__linelengthindex__last .
H22:   foundtype__1 >= rr_type__rritemtype__first .
H23:   foundtype__1 <= rr_type__rritemtype__last .
H24:   foundtype__1 >= rr_type__rritemtype__first .
H25:   foundtype__1 <= rr_type__rritemtype__last .
H26:   endidx__1 >= rr_type__linelengthindex__first .
H27:   endidx__1 <= rr_type__linelengthindex__last .
H28:   begidx__1 >= rr_type__linelengthindex__first .
H29:   begidx__1 <= rr_type__linelengthindex__last .
H30:   foundtype__1 >= rr_type__rritemtype__first .
H31:   foundtype__1 <= rr_type__rritemtype__last .
H32:   foundtype__1 = rr_type__control .
H33:   begidx__1 >= rr_type__linelengthindex__first .
H34:   begidx__1 <= rr_type__linelengthindex__last .
H35:   endidx__1 >= rr_type__linelengthindex__first .
H36:   endidx__1 <= rr_type__linelengthindex__last .
H37:   endidx__1 - 6 >= integer__base__first .
H38:   endidx__1 - 6 <= integer__base__last .
H39:   begidx__1 <= endidx__1 - 6 .
H40:   begidx__1 >= rr_type__linelengthindex__first .
H41:   begidx__1 <= rr_type__linelengthindex__last .
        ->
C1:    begidx__1 + 6 >= rr_type__linelengthindex__first .
C2:    begidx__1 + 6 <= rr_type__linelengthindex__last .
C3:    begidx__1 + 6 >= integer__base__first .
C4:    begidx__1 + 6 <= integer__base__last .
C5:    begidx__1 + 5 >= rr_type__linelengthindex__first .
C6:    begidx__1 + 5 <= rr_type__linelengthindex__last .
C7:    begidx__1 + 5 >= integer__base__first .
C8:    begidx__1 + 5 <= integer__base__last .
C9:    begidx__1 + 4 >= rr_type__linelengthindex__first .
C10:   begidx__1 + 4 <= rr_type__linelengthindex__last .
C11:   begidx__1 + 4 >= integer__base__first .
C12:   begidx__1 + 4 <= integer__base__last .
C13:   begidx__1 + 3 >= rr_type__linelengthindex__first .
C14:   begidx__1 + 3 <= rr_type__linelengthindex__last .
C15:   begidx__1 + 3 >= integer__base__first .
C16:   begidx__1 + 3 <= integer__base__last .
C17:   begidx__1 + 2 >= rr_type__linelengthindex__first .
C18:   begidx__1 + 2 <= rr_type__linelengthindex__last .
C19:   begidx__1 + 2 >= integer__base__first .
C20:   begidx__1 + 2 <= integer__base__last .
C21:   begidx__1 + 1 >= rr_type__linelengthindex__first .
C22:   begidx__1 + 1 <= rr_type__linelengthindex__last .
C23:   begidx__1 + 1 >= integer__base__first .
C24:   begidx__1 + 1 <= integer__base__last .
 

For path(s) from start to run-time check associated with statement of line 638:

procedure_parsecontrolline_5.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           neworigin, [i___1]) >= character__first) and (element(
           neworigin, [i___1]) <= character__last))) .
H2:    newttl >= unsigned_types__unsigned32__first .
H3:    newttl <= unsigned_types__unsigned32__last .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H5:    zlength >= rr_type__linelengthindex__first .
H6:    zlength <= rr_type__linelengthindex__last .
H7:    1 >= rr_type__linelengthindex__first .
H8:    1 <= rr_type__linelengthindex__last .
H9:    1 >= rr_type__linelengthindex__first .
H10:   1 <= rr_type__linelengthindex__last .
H11:   zlength >= rr_type__linelengthindex__first .
H12:   zlength <= rr_type__linelengthindex__last .
H13:   1 <= zlength .
H14:   begidx__1 <= endidx__1 .
H15:   begidx__1 <= zlength .
H16:   endidx__1 <= zlength .
H17:   (foundtype__1 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__1) and (i_ <= endidx__1)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H18:   begidx__1 >= rr_type__linelengthindex__first .
H19:   begidx__1 <= rr_type__linelengthindex__last .
H20:   endidx__1 >= rr_type__linelengthindex__first .
H21:   endidx__1 <= rr_type__linelengthindex__last .
H22:   foundtype__1 >= rr_type__rritemtype__first .
H23:   foundtype__1 <= rr_type__rritemtype__last .
H24:   foundtype__1 >= rr_type__rritemtype__first .
H25:   foundtype__1 <= rr_type__rritemtype__last .
H26:   endidx__1 >= rr_type__linelengthindex__first .
H27:   endidx__1 <= rr_type__linelengthindex__last .
H28:   begidx__1 >= rr_type__linelengthindex__first .
H29:   begidx__1 <= rr_type__linelengthindex__last .
H30:   foundtype__1 >= rr_type__rritemtype__first .
H31:   foundtype__1 <= rr_type__rritemtype__last .
H32:   foundtype__1 = rr_type__control .
H33:   begidx__1 >= rr_type__linelengthindex__first .
H34:   begidx__1 <= rr_type__linelengthindex__last .
H35:   endidx__1 >= rr_type__linelengthindex__first .
H36:   endidx__1 <= rr_type__linelengthindex__last .
H37:   endidx__1 - 6 >= integer__base__first .
H38:   endidx__1 - 6 <= integer__base__last .
H39:   begidx__1 <= endidx__1 - 6 .
H40:   begidx__1 >= rr_type__linelengthindex__first .
H41:   begidx__1 <= rr_type__linelengthindex__last .
H42:   begidx__1 + 6 >= rr_type__linelengthindex__first .
H43:   begidx__1 + 6 <= rr_type__linelengthindex__last .
H44:   begidx__1 + 6 >= integer__base__first .
H45:   begidx__1 + 6 <= integer__base__last .
H46:   begidx__1 + 5 >= rr_type__linelengthindex__first .
H47:   begidx__1 + 5 <= rr_type__linelengthindex__last .
H48:   begidx__1 + 5 >= integer__base__first .
H49:   begidx__1 + 5 <= integer__base__last .
H50:   begidx__1 + 4 >= rr_type__linelengthindex__first .
H51:   begidx__1 + 4 <= rr_type__linelengthindex__last .
H52:   begidx__1 + 4 >= integer__base__first .
H53:   begidx__1 + 4 <= integer__base__last .
H54:   begidx__1 + 3 >= rr_type__linelengthindex__first .
H55:   begidx__1 + 3 <= rr_type__linelengthindex__last .
H56:   begidx__1 + 3 >= integer__base__first .
H57:   begidx__1 + 3 <= integer__base__last .
H58:   begidx__1 + 2 >= rr_type__linelengthindex__first .
H59:   begidx__1 + 2 <= rr_type__linelengthindex__last .
H60:   begidx__1 + 2 >= integer__base__first .
H61:   begidx__1 + 2 <= integer__base__last .
H62:   begidx__1 + 1 >= rr_type__linelengthindex__first .
H63:   begidx__1 + 1 <= rr_type__linelengthindex__last .
H64:   begidx__1 + 1 >= integer__base__first .
H65:   begidx__1 + 1 <= integer__base__last .
H66:   element(zonefileline, [begidx__1 + 1]) = 79 .
H67:   element(zonefileline, [begidx__1 + 2]) = 82 .
H68:   element(zonefileline, [begidx__1 + 3]) = 73 .
H69:   element(zonefileline, [begidx__1 + 4]) = 71 .
H70:   element(zonefileline, [begidx__1 + 5]) = 73 .
H71:   element(zonefileline, [begidx__1 + 6]) = 78 .
H72:   begidx__1 >= rr_type__linelengthindex__first .
H73:   begidx__1 <= rr_type__linelengthindex__last .
H74:   endidx__1 >= rr_type__linelengthindex__first .
H75:   endidx__1 <= rr_type__linelengthindex__last .
H76:   begidx__1 < zlength .
H77:   endidx__1 < zlength .
H78:   endidx__1 >= rr_type__linelengthindex__first .
H79:   endidx__1 <= rr_type__linelengthindex__last .
        ->
C1:    endidx__1 + 1 >= rr_type__linelengthindex__first .
C2:    endidx__1 + 1 <= rr_type__linelengthindex__last .
 

For path(s) from start to precondition check associated with statement of line 639:

procedure_parsecontrolline_6.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           neworigin, [i___1]) >= character__first) and (element(
           neworigin, [i___1]) <= character__last))) .
H2:    newttl >= unsigned_types__unsigned32__first .
H3:    newttl <= unsigned_types__unsigned32__last .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H5:    zlength >= rr_type__linelengthindex__first .
H6:    zlength <= rr_type__linelengthindex__last .
H7:    1 >= rr_type__linelengthindex__first .
H8:    1 <= rr_type__linelengthindex__last .
H9:    1 >= rr_type__linelengthindex__first .
H10:   1 <= rr_type__linelengthindex__last .
H11:   zlength >= rr_type__linelengthindex__first .
H12:   zlength <= rr_type__linelengthindex__last .
H13:   1 <= zlength .
H14:   begidx__1 <= endidx__1 .
H15:   begidx__1 <= zlength .
H16:   endidx__1 <= zlength .
H17:   (foundtype__1 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__1) and (i_ <= endidx__1)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H18:   begidx__1 >= rr_type__linelengthindex__first .
H19:   begidx__1 <= rr_type__linelengthindex__last .
H20:   endidx__1 >= rr_type__linelengthindex__first .
H21:   endidx__1 <= rr_type__linelengthindex__last .
H22:   foundtype__1 >= rr_type__rritemtype__first .
H23:   foundtype__1 <= rr_type__rritemtype__last .
H24:   foundtype__1 >= rr_type__rritemtype__first .
H25:   foundtype__1 <= rr_type__rritemtype__last .
H26:   endidx__1 >= rr_type__linelengthindex__first .
H27:   endidx__1 <= rr_type__linelengthindex__last .
H28:   begidx__1 >= rr_type__linelengthindex__first .
H29:   begidx__1 <= rr_type__linelengthindex__last .
H30:   foundtype__1 >= rr_type__rritemtype__first .
H31:   foundtype__1 <= rr_type__rritemtype__last .
H32:   foundtype__1 = rr_type__control .
H33:   begidx__1 >= rr_type__linelengthindex__first .
H34:   begidx__1 <= rr_type__linelengthindex__last .
H35:   endidx__1 >= rr_type__linelengthindex__first .
H36:   endidx__1 <= rr_type__linelengthindex__last .
H37:   endidx__1 - 6 >= integer__base__first .
H38:   endidx__1 - 6 <= integer__base__last .
H39:   begidx__1 <= endidx__1 - 6 .
H40:   begidx__1 >= rr_type__linelengthindex__first .
H41:   begidx__1 <= rr_type__linelengthindex__last .
H42:   begidx__1 + 6 >= rr_type__linelengthindex__first .
H43:   begidx__1 + 6 <= rr_type__linelengthindex__last .
H44:   begidx__1 + 6 >= integer__base__first .
H45:   begidx__1 + 6 <= integer__base__last .
H46:   begidx__1 + 5 >= rr_type__linelengthindex__first .
H47:   begidx__1 + 5 <= rr_type__linelengthindex__last .
H48:   begidx__1 + 5 >= integer__base__first .
H49:   begidx__1 + 5 <= integer__base__last .
H50:   begidx__1 + 4 >= rr_type__linelengthindex__first .
H51:   begidx__1 + 4 <= rr_type__linelengthindex__last .
H52:   begidx__1 + 4 >= integer__base__first .
H53:   begidx__1 + 4 <= integer__base__last .
H54:   begidx__1 + 3 >= rr_type__linelengthindex__first .
H55:   begidx__1 + 3 <= rr_type__linelengthindex__last .
H56:   begidx__1 + 3 >= integer__base__first .
H57:   begidx__1 + 3 <= integer__base__last .
H58:   begidx__1 + 2 >= rr_type__linelengthindex__first .
H59:   begidx__1 + 2 <= rr_type__linelengthindex__last .
H60:   begidx__1 + 2 >= integer__base__first .
H61:   begidx__1 + 2 <= integer__base__last .
H62:   begidx__1 + 1 >= rr_type__linelengthindex__first .
H63:   begidx__1 + 1 <= rr_type__linelengthindex__last .
H64:   begidx__1 + 1 >= integer__base__first .
H65:   begidx__1 + 1 <= integer__base__last .
H66:   element(zonefileline, [begidx__1 + 1]) = 79 .
H67:   element(zonefileline, [begidx__1 + 2]) = 82 .
H68:   element(zonefileline, [begidx__1 + 3]) = 73 .
H69:   element(zonefileline, [begidx__1 + 4]) = 71 .
H70:   element(zonefileline, [begidx__1 + 5]) = 73 .
H71:   element(zonefileline, [begidx__1 + 6]) = 78 .
H72:   begidx__1 >= rr_type__linelengthindex__first .
H73:   begidx__1 <= rr_type__linelengthindex__last .
H74:   endidx__1 >= rr_type__linelengthindex__first .
H75:   endidx__1 <= rr_type__linelengthindex__last .
H76:   begidx__1 < zlength .
H77:   endidx__1 < zlength .
H78:   endidx__1 >= rr_type__linelengthindex__first .
H79:   endidx__1 <= rr_type__linelengthindex__last .
H80:   endidx__1 + 1 >= rr_type__linelengthindex__first .
H81:   endidx__1 + 1 <= rr_type__linelengthindex__last .
H82:   endidx__1 + 1 >= rr_type__linelengthindex__first .
H83:   endidx__1 + 1 <= rr_type__linelengthindex__last .
        ->
C1:    endidx__1 + 1 >= rr_type__linelengthindex__first .
C2:    endidx__1 + 1 <= rr_type__linelengthindex__last .
C3:    zlength >= rr_type__linelengthindex__first .
C4:    zlength <= rr_type__linelengthindex__last .
C5:    endidx__1 + 1 <= zlength .
 

For path(s) from start to run-time check associated with statement of line 639:

procedure_parsecontrolline_7.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           neworigin, [i___1]) >= character__first) and (element(
           neworigin, [i___1]) <= character__last))) .
H2:    newttl >= unsigned_types__unsigned32__first .
H3:    newttl <= unsigned_types__unsigned32__last .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H5:    zlength >= rr_type__linelengthindex__first .
H6:    zlength <= rr_type__linelengthindex__last .
H7:    1 >= rr_type__linelengthindex__first .
H8:    1 <= rr_type__linelengthindex__last .
H9:    1 >= rr_type__linelengthindex__first .
H10:   1 <= rr_type__linelengthindex__last .
H11:   zlength >= rr_type__linelengthindex__first .
H12:   zlength <= rr_type__linelengthindex__last .
H13:   1 <= zlength .
H14:   begidx__1 <= endidx__1 .
H15:   begidx__1 <= zlength .
H16:   endidx__1 <= zlength .
H17:   (foundtype__1 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__1) and (i_ <= endidx__1)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H18:   begidx__1 >= rr_type__linelengthindex__first .
H19:   begidx__1 <= rr_type__linelengthindex__last .
H20:   endidx__1 >= rr_type__linelengthindex__first .
H21:   endidx__1 <= rr_type__linelengthindex__last .
H22:   foundtype__1 >= rr_type__rritemtype__first .
H23:   foundtype__1 <= rr_type__rritemtype__last .
H24:   foundtype__1 >= rr_type__rritemtype__first .
H25:   foundtype__1 <= rr_type__rritemtype__last .
H26:   endidx__1 >= rr_type__linelengthindex__first .
H27:   endidx__1 <= rr_type__linelengthindex__last .
H28:   begidx__1 >= rr_type__linelengthindex__first .
H29:   begidx__1 <= rr_type__linelengthindex__last .
H30:   foundtype__1 >= rr_type__rritemtype__first .
H31:   foundtype__1 <= rr_type__rritemtype__last .
H32:   foundtype__1 = rr_type__control .
H33:   begidx__1 >= rr_type__linelengthindex__first .
H34:   begidx__1 <= rr_type__linelengthindex__last .
H35:   endidx__1 >= rr_type__linelengthindex__first .
H36:   endidx__1 <= rr_type__linelengthindex__last .
H37:   endidx__1 - 6 >= integer__base__first .
H38:   endidx__1 - 6 <= integer__base__last .
H39:   begidx__1 <= endidx__1 - 6 .
H40:   begidx__1 >= rr_type__linelengthindex__first .
H41:   begidx__1 <= rr_type__linelengthindex__last .
H42:   begidx__1 + 6 >= rr_type__linelengthindex__first .
H43:   begidx__1 + 6 <= rr_type__linelengthindex__last .
H44:   begidx__1 + 6 >= integer__base__first .
H45:   begidx__1 + 6 <= integer__base__last .
H46:   begidx__1 + 5 >= rr_type__linelengthindex__first .
H47:   begidx__1 + 5 <= rr_type__linelengthindex__last .
H48:   begidx__1 + 5 >= integer__base__first .
H49:   begidx__1 + 5 <= integer__base__last .
H50:   begidx__1 + 4 >= rr_type__linelengthindex__first .
H51:   begidx__1 + 4 <= rr_type__linelengthindex__last .
H52:   begidx__1 + 4 >= integer__base__first .
H53:   begidx__1 + 4 <= integer__base__last .
H54:   begidx__1 + 3 >= rr_type__linelengthindex__first .
H55:   begidx__1 + 3 <= rr_type__linelengthindex__last .
H56:   begidx__1 + 3 >= integer__base__first .
H57:   begidx__1 + 3 <= integer__base__last .
H58:   begidx__1 + 2 >= rr_type__linelengthindex__first .
H59:   begidx__1 + 2 <= rr_type__linelengthindex__last .
H60:   begidx__1 + 2 >= integer__base__first .
H61:   begidx__1 + 2 <= integer__base__last .
H62:   begidx__1 + 1 >= rr_type__linelengthindex__first .
H63:   begidx__1 + 1 <= rr_type__linelengthindex__last .
H64:   begidx__1 + 1 >= integer__base__first .
H65:   begidx__1 + 1 <= integer__base__last .
H66:   element(zonefileline, [begidx__1 + 1]) = 79 .
H67:   element(zonefileline, [begidx__1 + 2]) = 82 .
H68:   element(zonefileline, [begidx__1 + 3]) = 73 .
H69:   element(zonefileline, [begidx__1 + 4]) = 71 .
H70:   element(zonefileline, [begidx__1 + 5]) = 73 .
H71:   element(zonefileline, [begidx__1 + 6]) = 78 .
H72:   begidx__1 >= rr_type__linelengthindex__first .
H73:   begidx__1 <= rr_type__linelengthindex__last .
H74:   endidx__1 >= rr_type__linelengthindex__first .
H75:   endidx__1 <= rr_type__linelengthindex__last .
H76:   begidx__1 < zlength .
H77:   endidx__1 < zlength .
H78:   endidx__1 >= rr_type__linelengthindex__first .
H79:   endidx__1 <= rr_type__linelengthindex__last .
H80:   endidx__1 + 1 >= rr_type__linelengthindex__first .
H81:   endidx__1 + 1 <= rr_type__linelengthindex__last .
H82:   endidx__1 + 1 >= rr_type__linelengthindex__first .
H83:   endidx__1 + 1 <= rr_type__linelengthindex__last .
H84:   endidx__1 + 1 >= rr_type__linelengthindex__first .
H85:   endidx__1 + 1 <= rr_type__linelengthindex__last .
H86:   zlength >= rr_type__linelengthindex__first .
H87:   zlength <= rr_type__linelengthindex__last .
H88:   endidx__1 + 1 <= zlength .
H89:   begidx__2 <= endidx__2 .
H90:   begidx__2 <= zlength .
H91:   endidx__2 <= zlength .
H92:   (foundtype__2 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__2) and (i_ <= endidx__2)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H93:   begidx__2 >= rr_type__linelengthindex__first .
H94:   begidx__2 <= rr_type__linelengthindex__last .
H95:   endidx__2 >= rr_type__linelengthindex__first .
H96:   endidx__2 <= rr_type__linelengthindex__last .
H97:   foundtype__2 >= rr_type__rritemtype__first .
H98:   foundtype__2 <= rr_type__rritemtype__last .
        ->
C1:    foundtype__2 >= rr_type__rritemtype__first .
C2:    foundtype__2 <= rr_type__rritemtype__last .
C3:    endidx__2 >= rr_type__linelengthindex__first .
C4:    endidx__2 <= rr_type__linelengthindex__last .
C5:    begidx__2 >= rr_type__linelengthindex__first .
C6:    begidx__2 <= rr_type__linelengthindex__last .
 

For path(s) from start to run-time check associated with statement of line 643:

procedure_parsecontrolline_8.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           neworigin, [i___1]) >= character__first) and (element(
           neworigin, [i___1]) <= character__last))) .
H2:    newttl >= unsigned_types__unsigned32__first .
H3:    newttl <= unsigned_types__unsigned32__last .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H5:    zlength >= rr_type__linelengthindex__first .
H6:    zlength <= rr_type__linelengthindex__last .
H7:    1 >= rr_type__linelengthindex__first .
H8:    1 <= rr_type__linelengthindex__last .
H9:    1 >= rr_type__linelengthindex__first .
H10:   1 <= rr_type__linelengthindex__last .
H11:   zlength >= rr_type__linelengthindex__first .
H12:   zlength <= rr_type__linelengthindex__last .
H13:   1 <= zlength .
H14:   begidx__1 <= endidx__1 .
H15:   begidx__1 <= zlength .
H16:   endidx__1 <= zlength .
H17:   (foundtype__1 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__1) and (i_ <= endidx__1)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H18:   begidx__1 >= rr_type__linelengthindex__first .
H19:   begidx__1 <= rr_type__linelengthindex__last .
H20:   endidx__1 >= rr_type__linelengthindex__first .
H21:   endidx__1 <= rr_type__linelengthindex__last .
H22:   foundtype__1 >= rr_type__rritemtype__first .
H23:   foundtype__1 <= rr_type__rritemtype__last .
H24:   foundtype__1 >= rr_type__rritemtype__first .
H25:   foundtype__1 <= rr_type__rritemtype__last .
H26:   endidx__1 >= rr_type__linelengthindex__first .
H27:   endidx__1 <= rr_type__linelengthindex__last .
H28:   begidx__1 >= rr_type__linelengthindex__first .
H29:   begidx__1 <= rr_type__linelengthindex__last .
H30:   foundtype__1 >= rr_type__rritemtype__first .
H31:   foundtype__1 <= rr_type__rritemtype__last .
H32:   foundtype__1 = rr_type__control .
H33:   begidx__1 >= rr_type__linelengthindex__first .
H34:   begidx__1 <= rr_type__linelengthindex__last .
H35:   endidx__1 >= rr_type__linelengthindex__first .
H36:   endidx__1 <= rr_type__linelengthindex__last .
H37:   endidx__1 - 6 >= integer__base__first .
H38:   endidx__1 - 6 <= integer__base__last .
H39:   begidx__1 <= endidx__1 - 6 .
H40:   begidx__1 >= rr_type__linelengthindex__first .
H41:   begidx__1 <= rr_type__linelengthindex__last .
H42:   begidx__1 + 6 >= rr_type__linelengthindex__first .
H43:   begidx__1 + 6 <= rr_type__linelengthindex__last .
H44:   begidx__1 + 6 >= integer__base__first .
H45:   begidx__1 + 6 <= integer__base__last .
H46:   begidx__1 + 5 >= rr_type__linelengthindex__first .
H47:   begidx__1 + 5 <= rr_type__linelengthindex__last .
H48:   begidx__1 + 5 >= integer__base__first .
H49:   begidx__1 + 5 <= integer__base__last .
H50:   begidx__1 + 4 >= rr_type__linelengthindex__first .
H51:   begidx__1 + 4 <= rr_type__linelengthindex__last .
H52:   begidx__1 + 4 >= integer__base__first .
H53:   begidx__1 + 4 <= integer__base__last .
H54:   begidx__1 + 3 >= rr_type__linelengthindex__first .
H55:   begidx__1 + 3 <= rr_type__linelengthindex__last .
H56:   begidx__1 + 3 >= integer__base__first .
H57:   begidx__1 + 3 <= integer__base__last .
H58:   begidx__1 + 2 >= rr_type__linelengthindex__first .
H59:   begidx__1 + 2 <= rr_type__linelengthindex__last .
H60:   begidx__1 + 2 >= integer__base__first .
H61:   begidx__1 + 2 <= integer__base__last .
H62:   begidx__1 + 1 >= rr_type__linelengthindex__first .
H63:   begidx__1 + 1 <= rr_type__linelengthindex__last .
H64:   begidx__1 + 1 >= integer__base__first .
H65:   begidx__1 + 1 <= integer__base__last .
H66:   element(zonefileline, [begidx__1 + 1]) = 79 .
H67:   element(zonefileline, [begidx__1 + 2]) = 82 .
H68:   element(zonefileline, [begidx__1 + 3]) = 73 .
H69:   element(zonefileline, [begidx__1 + 4]) = 71 .
H70:   element(zonefileline, [begidx__1 + 5]) = 73 .
H71:   element(zonefileline, [begidx__1 + 6]) = 78 .
H72:   begidx__1 >= rr_type__linelengthindex__first .
H73:   begidx__1 <= rr_type__linelengthindex__last .
H74:   endidx__1 >= rr_type__linelengthindex__first .
H75:   endidx__1 <= rr_type__linelengthindex__last .
H76:   begidx__1 < zlength .
H77:   endidx__1 < zlength .
H78:   endidx__1 >= rr_type__linelengthindex__first .
H79:   endidx__1 <= rr_type__linelengthindex__last .
H80:   endidx__1 + 1 >= rr_type__linelengthindex__first .
H81:   endidx__1 + 1 <= rr_type__linelengthindex__last .
H82:   endidx__1 + 1 >= rr_type__linelengthindex__first .
H83:   endidx__1 + 1 <= rr_type__linelengthindex__last .
H84:   endidx__1 + 1 >= rr_type__linelengthindex__first .
H85:   endidx__1 + 1 <= rr_type__linelengthindex__last .
H86:   zlength >= rr_type__linelengthindex__first .
H87:   zlength <= rr_type__linelengthindex__last .
H88:   endidx__1 + 1 <= zlength .
H89:   begidx__2 <= endidx__2 .
H90:   begidx__2 <= zlength .
H91:   endidx__2 <= zlength .
H92:   (foundtype__2 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__2) and (i_ <= endidx__2)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H93:   begidx__2 >= rr_type__linelengthindex__first .
H94:   begidx__2 <= rr_type__linelengthindex__last .
H95:   endidx__2 >= rr_type__linelengthindex__first .
H96:   endidx__2 <= rr_type__linelengthindex__last .
H97:   foundtype__2 >= rr_type__rritemtype__first .
H98:   foundtype__2 <= rr_type__rritemtype__last .
H99:   foundtype__2 >= rr_type__rritemtype__first .
H100:  foundtype__2 <= rr_type__rritemtype__last .
H101:  endidx__2 >= rr_type__linelengthindex__first .
H102:  endidx__2 <= rr_type__linelengthindex__last .
H103:  begidx__2 >= rr_type__linelengthindex__first .
H104:  begidx__2 <= rr_type__linelengthindex__last .
H105:  foundtype__2 >= rr_type__rritemtype__first .
H106:  foundtype__2 <= rr_type__rritemtype__last .
H107:  not (foundtype__2 <> rr_type__domainnameortimespec) .
H108:  endidx__2 >= rr_type__linelengthindex__first .
H109:  endidx__2 <= rr_type__linelengthindex__last .
        ->
C1:    endidx__2 >= rr_type__linelengthindex__first .
C2:    endidx__2 <= rr_type__linelengthindex__last .
 

procedure_parsecontrolline_9.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           neworigin, [i___1]) >= character__first) and (element(
           neworigin, [i___1]) <= character__last))) .
H2:    newttl >= unsigned_types__unsigned32__first .
H3:    newttl <= unsigned_types__unsigned32__last .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H5:    zlength >= rr_type__linelengthindex__first .
H6:    zlength <= rr_type__linelengthindex__last .
H7:    1 >= rr_type__linelengthindex__first .
H8:    1 <= rr_type__linelengthindex__last .
H9:    1 >= rr_type__linelengthindex__first .
H10:   1 <= rr_type__linelengthindex__last .
H11:   zlength >= rr_type__linelengthindex__first .
H12:   zlength <= rr_type__linelengthindex__last .
H13:   1 <= zlength .
H14:   begidx__1 <= endidx__1 .
H15:   begidx__1 <= zlength .
H16:   endidx__1 <= zlength .
H17:   (foundtype__1 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__1) and (i_ <= endidx__1)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H18:   begidx__1 >= rr_type__linelengthindex__first .
H19:   begidx__1 <= rr_type__linelengthindex__last .
H20:   endidx__1 >= rr_type__linelengthindex__first .
H21:   endidx__1 <= rr_type__linelengthindex__last .
H22:   foundtype__1 >= rr_type__rritemtype__first .
H23:   foundtype__1 <= rr_type__rritemtype__last .
H24:   foundtype__1 >= rr_type__rritemtype__first .
H25:   foundtype__1 <= rr_type__rritemtype__last .
H26:   endidx__1 >= rr_type__linelengthindex__first .
H27:   endidx__1 <= rr_type__linelengthindex__last .
H28:   begidx__1 >= rr_type__linelengthindex__first .
H29:   begidx__1 <= rr_type__linelengthindex__last .
H30:   foundtype__1 >= rr_type__rritemtype__first .
H31:   foundtype__1 <= rr_type__rritemtype__last .
H32:   foundtype__1 = rr_type__control .
H33:   begidx__1 >= rr_type__linelengthindex__first .
H34:   begidx__1 <= rr_type__linelengthindex__last .
H35:   endidx__1 >= rr_type__linelengthindex__first .
H36:   endidx__1 <= rr_type__linelengthindex__last .
H37:   endidx__1 - 6 >= integer__base__first .
H38:   endidx__1 - 6 <= integer__base__last .
H39:   begidx__1 <= endidx__1 - 6 .
H40:   begidx__1 >= rr_type__linelengthindex__first .
H41:   begidx__1 <= rr_type__linelengthindex__last .
H42:   begidx__1 + 6 >= rr_type__linelengthindex__first .
H43:   begidx__1 + 6 <= rr_type__linelengthindex__last .
H44:   begidx__1 + 6 >= integer__base__first .
H45:   begidx__1 + 6 <= integer__base__last .
H46:   begidx__1 + 5 >= rr_type__linelengthindex__first .
H47:   begidx__1 + 5 <= rr_type__linelengthindex__last .
H48:   begidx__1 + 5 >= integer__base__first .
H49:   begidx__1 + 5 <= integer__base__last .
H50:   begidx__1 + 4 >= rr_type__linelengthindex__first .
H51:   begidx__1 + 4 <= rr_type__linelengthindex__last .
H52:   begidx__1 + 4 >= integer__base__first .
H53:   begidx__1 + 4 <= integer__base__last .
H54:   begidx__1 + 3 >= rr_type__linelengthindex__first .
H55:   begidx__1 + 3 <= rr_type__linelengthindex__last .
H56:   begidx__1 + 3 >= integer__base__first .
H57:   begidx__1 + 3 <= integer__base__last .
H58:   begidx__1 + 2 >= rr_type__linelengthindex__first .
H59:   begidx__1 + 2 <= rr_type__linelengthindex__last .
H60:   begidx__1 + 2 >= integer__base__first .
H61:   begidx__1 + 2 <= integer__base__last .
H62:   begidx__1 + 1 >= rr_type__linelengthindex__first .
H63:   begidx__1 + 1 <= rr_type__linelengthindex__last .
H64:   begidx__1 + 1 >= integer__base__first .
H65:   begidx__1 + 1 <= integer__base__last .
H66:   element(zonefileline, [begidx__1 + 1]) = 79 .
H67:   element(zonefileline, [begidx__1 + 2]) = 82 .
H68:   element(zonefileline, [begidx__1 + 3]) = 73 .
H69:   element(zonefileline, [begidx__1 + 4]) = 71 .
H70:   element(zonefileline, [begidx__1 + 5]) = 73 .
H71:   element(zonefileline, [begidx__1 + 6]) = 78 .
H72:   begidx__1 >= rr_type__linelengthindex__first .
H73:   begidx__1 <= rr_type__linelengthindex__last .
H74:   endidx__1 >= rr_type__linelengthindex__first .
H75:   endidx__1 <= rr_type__linelengthindex__last .
H76:   not ((begidx__1 < zlength) and (endidx__1 < zlength)) .
H77:   foundtype__1 >= rr_type__rritemtype__first .
H78:   foundtype__1 <= rr_type__rritemtype__last .
H79:   not (foundtype__1 <> rr_type__domainnameortimespec) .
H80:   endidx__1 >= rr_type__linelengthindex__first .
H81:   endidx__1 <= rr_type__linelengthindex__last .
        ->
C1:    endidx__1 >= rr_type__linelengthindex__first .
C2:    endidx__1 <= rr_type__linelengthindex__last .
 

For path(s) from start to run-time check associated with statement of line 648:

procedure_parsecontrolline_10.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           neworigin, [i___1]) >= character__first) and (element(
           neworigin, [i___1]) <= character__last))) .
H2:    newttl >= unsigned_types__unsigned32__first .
H3:    newttl <= unsigned_types__unsigned32__last .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H5:    zlength >= rr_type__linelengthindex__first .
H6:    zlength <= rr_type__linelengthindex__last .
H7:    1 >= rr_type__linelengthindex__first .
H8:    1 <= rr_type__linelengthindex__last .
H9:    1 >= rr_type__linelengthindex__first .
H10:   1 <= rr_type__linelengthindex__last .
H11:   zlength >= rr_type__linelengthindex__first .
H12:   zlength <= rr_type__linelengthindex__last .
H13:   1 <= zlength .
H14:   begidx__1 <= endidx__1 .
H15:   begidx__1 <= zlength .
H16:   endidx__1 <= zlength .
H17:   (foundtype__1 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__1) and (i_ <= endidx__1)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H18:   begidx__1 >= rr_type__linelengthindex__first .
H19:   begidx__1 <= rr_type__linelengthindex__last .
H20:   endidx__1 >= rr_type__linelengthindex__first .
H21:   endidx__1 <= rr_type__linelengthindex__last .
H22:   foundtype__1 >= rr_type__rritemtype__first .
H23:   foundtype__1 <= rr_type__rritemtype__last .
H24:   foundtype__1 >= rr_type__rritemtype__first .
H25:   foundtype__1 <= rr_type__rritemtype__last .
H26:   endidx__1 >= rr_type__linelengthindex__first .
H27:   endidx__1 <= rr_type__linelengthindex__last .
H28:   begidx__1 >= rr_type__linelengthindex__first .
H29:   begidx__1 <= rr_type__linelengthindex__last .
H30:   foundtype__1 >= rr_type__rritemtype__first .
H31:   foundtype__1 <= rr_type__rritemtype__last .
H32:   foundtype__1 = rr_type__control .
H33:   begidx__1 >= rr_type__linelengthindex__first .
H34:   begidx__1 <= rr_type__linelengthindex__last .
H35:   endidx__1 >= rr_type__linelengthindex__first .
H36:   endidx__1 <= rr_type__linelengthindex__last .
H37:   endidx__1 - 6 >= integer__base__first .
H38:   endidx__1 - 6 <= integer__base__last .
H39:   begidx__1 <= endidx__1 - 6 .
H40:   begidx__1 >= rr_type__linelengthindex__first .
H41:   begidx__1 <= rr_type__linelengthindex__last .
H42:   begidx__1 + 6 >= rr_type__linelengthindex__first .
H43:   begidx__1 + 6 <= rr_type__linelengthindex__last .
H44:   begidx__1 + 6 >= integer__base__first .
H45:   begidx__1 + 6 <= integer__base__last .
H46:   begidx__1 + 5 >= rr_type__linelengthindex__first .
H47:   begidx__1 + 5 <= rr_type__linelengthindex__last .
H48:   begidx__1 + 5 >= integer__base__first .
H49:   begidx__1 + 5 <= integer__base__last .
H50:   begidx__1 + 4 >= rr_type__linelengthindex__first .
H51:   begidx__1 + 4 <= rr_type__linelengthindex__last .
H52:   begidx__1 + 4 >= integer__base__first .
H53:   begidx__1 + 4 <= integer__base__last .
H54:   begidx__1 + 3 >= rr_type__linelengthindex__first .
H55:   begidx__1 + 3 <= rr_type__linelengthindex__last .
H56:   begidx__1 + 3 >= integer__base__first .
H57:   begidx__1 + 3 <= integer__base__last .
H58:   begidx__1 + 2 >= rr_type__linelengthindex__first .
H59:   begidx__1 + 2 <= rr_type__linelengthindex__last .
H60:   begidx__1 + 2 >= integer__base__first .
H61:   begidx__1 + 2 <= integer__base__last .
H62:   begidx__1 + 1 >= rr_type__linelengthindex__first .
H63:   begidx__1 + 1 <= rr_type__linelengthindex__last .
H64:   begidx__1 + 1 >= integer__base__first .
H65:   begidx__1 + 1 <= integer__base__last .
H66:   element(zonefileline, [begidx__1 + 1]) = 79 .
H67:   element(zonefileline, [begidx__1 + 2]) = 82 .
H68:   element(zonefileline, [begidx__1 + 3]) = 73 .
H69:   element(zonefileline, [begidx__1 + 4]) = 71 .
H70:   element(zonefileline, [begidx__1 + 5]) = 73 .
H71:   element(zonefileline, [begidx__1 + 6]) = 78 .
H72:   begidx__1 >= rr_type__linelengthindex__first .
H73:   begidx__1 <= rr_type__linelengthindex__last .
H74:   endidx__1 >= rr_type__linelengthindex__first .
H75:   endidx__1 <= rr_type__linelengthindex__last .
H76:   begidx__1 < zlength .
H77:   endidx__1 < zlength .
H78:   endidx__1 >= rr_type__linelengthindex__first .
H79:   endidx__1 <= rr_type__linelengthindex__last .
H80:   endidx__1 + 1 >= rr_type__linelengthindex__first .
H81:   endidx__1 + 1 <= rr_type__linelengthindex__last .
H82:   endidx__1 + 1 >= rr_type__linelengthindex__first .
H83:   endidx__1 + 1 <= rr_type__linelengthindex__last .
H84:   endidx__1 + 1 >= rr_type__linelengthindex__first .
H85:   endidx__1 + 1 <= rr_type__linelengthindex__last .
H86:   zlength >= rr_type__linelengthindex__first .
H87:   zlength <= rr_type__linelengthindex__last .
H88:   endidx__1 + 1 <= zlength .
H89:   begidx__2 <= endidx__2 .
H90:   begidx__2 <= zlength .
H91:   endidx__2 <= zlength .
H92:   (foundtype__2 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__2) and (i_ <= endidx__2)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H93:   begidx__2 >= rr_type__linelengthindex__first .
H94:   begidx__2 <= rr_type__linelengthindex__last .
H95:   endidx__2 >= rr_type__linelengthindex__first .
H96:   endidx__2 <= rr_type__linelengthindex__last .
H97:   foundtype__2 >= rr_type__rritemtype__first .
H98:   foundtype__2 <= rr_type__rritemtype__last .
H99:   foundtype__2 >= rr_type__rritemtype__first .
H100:  foundtype__2 <= rr_type__rritemtype__last .
H101:  endidx__2 >= rr_type__linelengthindex__first .
H102:  endidx__2 <= rr_type__linelengthindex__last .
H103:  begidx__2 >= rr_type__linelengthindex__first .
H104:  begidx__2 <= rr_type__linelengthindex__last .
H105:  foundtype__2 >= rr_type__rritemtype__first .
H106:  foundtype__2 <= rr_type__rritemtype__last .
H107:  not (foundtype__2 <> rr_type__domainnameortimespec) .
H108:  endidx__2 >= rr_type__linelengthindex__first .
H109:  endidx__2 <= rr_type__linelengthindex__last .
H110:  endidx__2 >= rr_type__linelengthindex__first .
H111:  endidx__2 <= rr_type__linelengthindex__last .
H112:  not (element(zonefileline, [endidx__2]) <> 46) .
H113:  begidx__2 >= rr_type__linelengthindex__first .
H114:  begidx__2 <= rr_type__linelengthindex__last .
H115:  endidx__2 >= rr_type__linelengthindex__first .
H116:  endidx__2 <= rr_type__linelengthindex__last .
        ->
C1:    endidx__2 >= integer__first .
C2:    endidx__2 <= integer__last .
C3:    begidx__2 >= integer__first .
C4:    begidx__2 <= integer__last .
 

procedure_parsecontrolline_11.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           neworigin, [i___1]) >= character__first) and (element(
           neworigin, [i___1]) <= character__last))) .
H2:    newttl >= unsigned_types__unsigned32__first .
H3:    newttl <= unsigned_types__unsigned32__last .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H5:    zlength >= rr_type__linelengthindex__first .
H6:    zlength <= rr_type__linelengthindex__last .
H7:    1 >= rr_type__linelengthindex__first .
H8:    1 <= rr_type__linelengthindex__last .
H9:    1 >= rr_type__linelengthindex__first .
H10:   1 <= rr_type__linelengthindex__last .
H11:   zlength >= rr_type__linelengthindex__first .
H12:   zlength <= rr_type__linelengthindex__last .
H13:   1 <= zlength .
H14:   begidx__1 <= endidx__1 .
H15:   begidx__1 <= zlength .
H16:   endidx__1 <= zlength .
H17:   (foundtype__1 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__1) and (i_ <= endidx__1)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H18:   begidx__1 >= rr_type__linelengthindex__first .
H19:   begidx__1 <= rr_type__linelengthindex__last .
H20:   endidx__1 >= rr_type__linelengthindex__first .
H21:   endidx__1 <= rr_type__linelengthindex__last .
H22:   foundtype__1 >= rr_type__rritemtype__first .
H23:   foundtype__1 <= rr_type__rritemtype__last .
H24:   foundtype__1 >= rr_type__rritemtype__first .
H25:   foundtype__1 <= rr_type__rritemtype__last .
H26:   endidx__1 >= rr_type__linelengthindex__first .
H27:   endidx__1 <= rr_type__linelengthindex__last .
H28:   begidx__1 >= rr_type__linelengthindex__first .
H29:   begidx__1 <= rr_type__linelengthindex__last .
H30:   foundtype__1 >= rr_type__rritemtype__first .
H31:   foundtype__1 <= rr_type__rritemtype__last .
H32:   foundtype__1 = rr_type__control .
H33:   begidx__1 >= rr_type__linelengthindex__first .
H34:   begidx__1 <= rr_type__linelengthindex__last .
H35:   endidx__1 >= rr_type__linelengthindex__first .
H36:   endidx__1 <= rr_type__linelengthindex__last .
H37:   endidx__1 - 6 >= integer__base__first .
H38:   endidx__1 - 6 <= integer__base__last .
H39:   begidx__1 <= endidx__1 - 6 .
H40:   begidx__1 >= rr_type__linelengthindex__first .
H41:   begidx__1 <= rr_type__linelengthindex__last .
H42:   begidx__1 + 6 >= rr_type__linelengthindex__first .
H43:   begidx__1 + 6 <= rr_type__linelengthindex__last .
H44:   begidx__1 + 6 >= integer__base__first .
H45:   begidx__1 + 6 <= integer__base__last .
H46:   begidx__1 + 5 >= rr_type__linelengthindex__first .
H47:   begidx__1 + 5 <= rr_type__linelengthindex__last .
H48:   begidx__1 + 5 >= integer__base__first .
H49:   begidx__1 + 5 <= integer__base__last .
H50:   begidx__1 + 4 >= rr_type__linelengthindex__first .
H51:   begidx__1 + 4 <= rr_type__linelengthindex__last .
H52:   begidx__1 + 4 >= integer__base__first .
H53:   begidx__1 + 4 <= integer__base__last .
H54:   begidx__1 + 3 >= rr_type__linelengthindex__first .
H55:   begidx__1 + 3 <= rr_type__linelengthindex__last .
H56:   begidx__1 + 3 >= integer__base__first .
H57:   begidx__1 + 3 <= integer__base__last .
H58:   begidx__1 + 2 >= rr_type__linelengthindex__first .
H59:   begidx__1 + 2 <= rr_type__linelengthindex__last .
H60:   begidx__1 + 2 >= integer__base__first .
H61:   begidx__1 + 2 <= integer__base__last .
H62:   begidx__1 + 1 >= rr_type__linelengthindex__first .
H63:   begidx__1 + 1 <= rr_type__linelengthindex__last .
H64:   begidx__1 + 1 >= integer__base__first .
H65:   begidx__1 + 1 <= integer__base__last .
H66:   element(zonefileline, [begidx__1 + 1]) = 79 .
H67:   element(zonefileline, [begidx__1 + 2]) = 82 .
H68:   element(zonefileline, [begidx__1 + 3]) = 73 .
H69:   element(zonefileline, [begidx__1 + 4]) = 71 .
H70:   element(zonefileline, [begidx__1 + 5]) = 73 .
H71:   element(zonefileline, [begidx__1 + 6]) = 78 .
H72:   begidx__1 >= rr_type__linelengthindex__first .
H73:   begidx__1 <= rr_type__linelengthindex__last .
H74:   endidx__1 >= rr_type__linelengthindex__first .
H75:   endidx__1 <= rr_type__linelengthindex__last .
H76:   not ((begidx__1 < zlength) and (endidx__1 < zlength)) .
H77:   foundtype__1 >= rr_type__rritemtype__first .
H78:   foundtype__1 <= rr_type__rritemtype__last .
H79:   not (foundtype__1 <> rr_type__domainnameortimespec) .
H80:   endidx__1 >= rr_type__linelengthindex__first .
H81:   endidx__1 <= rr_type__linelengthindex__last .
H82:   endidx__1 >= rr_type__linelengthindex__first .
H83:   endidx__1 <= rr_type__linelengthindex__last .
H84:   not (element(zonefileline, [endidx__1]) <> 46) .
H85:   begidx__1 >= rr_type__linelengthindex__first .
H86:   begidx__1 <= rr_type__linelengthindex__last .
H87:   endidx__1 >= rr_type__linelengthindex__first .
H88:   endidx__1 <= rr_type__linelengthindex__last .
        ->
C1:    endidx__1 >= integer__first .
C2:    endidx__1 <= integer__last .
C3:    begidx__1 >= integer__first .
C4:    begidx__1 <= integer__last .
 

For path(s) from start to run-time check associated with statement of line 648:

procedure_parsecontrolline_12.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           neworigin, [i___1]) >= character__first) and (element(
           neworigin, [i___1]) <= character__last))) .
H2:    newttl >= unsigned_types__unsigned32__first .
H3:    newttl <= unsigned_types__unsigned32__last .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H5:    zlength >= rr_type__linelengthindex__first .
H6:    zlength <= rr_type__linelengthindex__last .
H7:    1 >= rr_type__linelengthindex__first .
H8:    1 <= rr_type__linelengthindex__last .
H9:    1 >= rr_type__linelengthindex__first .
H10:   1 <= rr_type__linelengthindex__last .
H11:   zlength >= rr_type__linelengthindex__first .
H12:   zlength <= rr_type__linelengthindex__last .
H13:   1 <= zlength .
H14:   begidx__1 <= endidx__1 .
H15:   begidx__1 <= zlength .
H16:   endidx__1 <= zlength .
H17:   (foundtype__1 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__1) and (i_ <= endidx__1)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H18:   begidx__1 >= rr_type__linelengthindex__first .
H19:   begidx__1 <= rr_type__linelengthindex__last .
H20:   endidx__1 >= rr_type__linelengthindex__first .
H21:   endidx__1 <= rr_type__linelengthindex__last .
H22:   foundtype__1 >= rr_type__rritemtype__first .
H23:   foundtype__1 <= rr_type__rritemtype__last .
H24:   foundtype__1 >= rr_type__rritemtype__first .
H25:   foundtype__1 <= rr_type__rritemtype__last .
H26:   endidx__1 >= rr_type__linelengthindex__first .
H27:   endidx__1 <= rr_type__linelengthindex__last .
H28:   begidx__1 >= rr_type__linelengthindex__first .
H29:   begidx__1 <= rr_type__linelengthindex__last .
H30:   foundtype__1 >= rr_type__rritemtype__first .
H31:   foundtype__1 <= rr_type__rritemtype__last .
H32:   foundtype__1 = rr_type__control .
H33:   begidx__1 >= rr_type__linelengthindex__first .
H34:   begidx__1 <= rr_type__linelengthindex__last .
H35:   endidx__1 >= rr_type__linelengthindex__first .
H36:   endidx__1 <= rr_type__linelengthindex__last .
H37:   endidx__1 - 6 >= integer__base__first .
H38:   endidx__1 - 6 <= integer__base__last .
H39:   begidx__1 <= endidx__1 - 6 .
H40:   begidx__1 >= rr_type__linelengthindex__first .
H41:   begidx__1 <= rr_type__linelengthindex__last .
H42:   begidx__1 + 6 >= rr_type__linelengthindex__first .
H43:   begidx__1 + 6 <= rr_type__linelengthindex__last .
H44:   begidx__1 + 6 >= integer__base__first .
H45:   begidx__1 + 6 <= integer__base__last .
H46:   begidx__1 + 5 >= rr_type__linelengthindex__first .
H47:   begidx__1 + 5 <= rr_type__linelengthindex__last .
H48:   begidx__1 + 5 >= integer__base__first .
H49:   begidx__1 + 5 <= integer__base__last .
H50:   begidx__1 + 4 >= rr_type__linelengthindex__first .
H51:   begidx__1 + 4 <= rr_type__linelengthindex__last .
H52:   begidx__1 + 4 >= integer__base__first .
H53:   begidx__1 + 4 <= integer__base__last .
H54:   begidx__1 + 3 >= rr_type__linelengthindex__first .
H55:   begidx__1 + 3 <= rr_type__linelengthindex__last .
H56:   begidx__1 + 3 >= integer__base__first .
H57:   begidx__1 + 3 <= integer__base__last .
H58:   begidx__1 + 2 >= rr_type__linelengthindex__first .
H59:   begidx__1 + 2 <= rr_type__linelengthindex__last .
H60:   begidx__1 + 2 >= integer__base__first .
H61:   begidx__1 + 2 <= integer__base__last .
H62:   begidx__1 + 1 >= rr_type__linelengthindex__first .
H63:   begidx__1 + 1 <= rr_type__linelengthindex__last .
H64:   begidx__1 + 1 >= integer__base__first .
H65:   begidx__1 + 1 <= integer__base__last .
H66:   element(zonefileline, [begidx__1 + 1]) = 79 .
H67:   element(zonefileline, [begidx__1 + 2]) = 82 .
H68:   element(zonefileline, [begidx__1 + 3]) = 73 .
H69:   element(zonefileline, [begidx__1 + 4]) = 71 .
H70:   element(zonefileline, [begidx__1 + 5]) = 73 .
H71:   element(zonefileline, [begidx__1 + 6]) = 78 .
H72:   begidx__1 >= rr_type__linelengthindex__first .
H73:   begidx__1 <= rr_type__linelengthindex__last .
H74:   endidx__1 >= rr_type__linelengthindex__first .
H75:   endidx__1 <= rr_type__linelengthindex__last .
H76:   begidx__1 < zlength .
H77:   endidx__1 < zlength .
H78:   endidx__1 >= rr_type__linelengthindex__first .
H79:   endidx__1 <= rr_type__linelengthindex__last .
H80:   endidx__1 + 1 >= rr_type__linelengthindex__first .
H81:   endidx__1 + 1 <= rr_type__linelengthindex__last .
H82:   endidx__1 + 1 >= rr_type__linelengthindex__first .
H83:   endidx__1 + 1 <= rr_type__linelengthindex__last .
H84:   endidx__1 + 1 >= rr_type__linelengthindex__first .
H85:   endidx__1 + 1 <= rr_type__linelengthindex__last .
H86:   zlength >= rr_type__linelengthindex__first .
H87:   zlength <= rr_type__linelengthindex__last .
H88:   endidx__1 + 1 <= zlength .
H89:   begidx__2 <= endidx__2 .
H90:   begidx__2 <= zlength .
H91:   endidx__2 <= zlength .
H92:   (foundtype__2 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__2) and (i_ <= endidx__2)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H93:   begidx__2 >= rr_type__linelengthindex__first .
H94:   begidx__2 <= rr_type__linelengthindex__last .
H95:   endidx__2 >= rr_type__linelengthindex__first .
H96:   endidx__2 <= rr_type__linelengthindex__last .
H97:   foundtype__2 >= rr_type__rritemtype__first .
H98:   foundtype__2 <= rr_type__rritemtype__last .
H99:   foundtype__2 >= rr_type__rritemtype__first .
H100:  foundtype__2 <= rr_type__rritemtype__last .
H101:  endidx__2 >= rr_type__linelengthindex__first .
H102:  endidx__2 <= rr_type__linelengthindex__last .
H103:  begidx__2 >= rr_type__linelengthindex__first .
H104:  begidx__2 <= rr_type__linelengthindex__last .
H105:  foundtype__2 >= rr_type__rritemtype__first .
H106:  foundtype__2 <= rr_type__rritemtype__last .
H107:  not (foundtype__2 <> rr_type__domainnameortimespec) .
H108:  endidx__2 >= rr_type__linelengthindex__first .
H109:  endidx__2 <= rr_type__linelengthindex__last .
H110:  endidx__2 >= rr_type__linelengthindex__first .
H111:  endidx__2 <= rr_type__linelengthindex__last .
H112:  not (element(zonefileline, [endidx__2]) <> 46) .
H113:  begidx__2 >= rr_type__linelengthindex__first .
H114:  begidx__2 <= rr_type__linelengthindex__last .
H115:  endidx__2 >= rr_type__linelengthindex__first .
H116:  endidx__2 <= rr_type__linelengthindex__last .
H117:  endidx__2 >= integer__first .
H118:  endidx__2 <= integer__last .
H119:  begidx__2 >= integer__first .
H120:  begidx__2 <= integer__last .
        ->
C1:    (begidx__2 <= endidx__2) -> ((endidx__2 >= integer__first) and (
           endidx__2 <= integer__last)) .
C2:    (begidx__2 <= endidx__2) -> ((begidx__2 >= integer__first) and (
           begidx__2 <= integer__last)) .
 

procedure_parsecontrolline_13.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           neworigin, [i___1]) >= character__first) and (element(
           neworigin, [i___1]) <= character__last))) .
H2:    newttl >= unsigned_types__unsigned32__first .
H3:    newttl <= unsigned_types__unsigned32__last .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H5:    zlength >= rr_type__linelengthindex__first .
H6:    zlength <= rr_type__linelengthindex__last .
H7:    1 >= rr_type__linelengthindex__first .
H8:    1 <= rr_type__linelengthindex__last .
H9:    1 >= rr_type__linelengthindex__first .
H10:   1 <= rr_type__linelengthindex__last .
H11:   zlength >= rr_type__linelengthindex__first .
H12:   zlength <= rr_type__linelengthindex__last .
H13:   1 <= zlength .
H14:   begidx__1 <= endidx__1 .
H15:   begidx__1 <= zlength .
H16:   endidx__1 <= zlength .
H17:   (foundtype__1 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__1) and (i_ <= endidx__1)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H18:   begidx__1 >= rr_type__linelengthindex__first .
H19:   begidx__1 <= rr_type__linelengthindex__last .
H20:   endidx__1 >= rr_type__linelengthindex__first .
H21:   endidx__1 <= rr_type__linelengthindex__last .
H22:   foundtype__1 >= rr_type__rritemtype__first .
H23:   foundtype__1 <= rr_type__rritemtype__last .
H24:   foundtype__1 >= rr_type__rritemtype__first .
H25:   foundtype__1 <= rr_type__rritemtype__last .
H26:   endidx__1 >= rr_type__linelengthindex__first .
H27:   endidx__1 <= rr_type__linelengthindex__last .
H28:   begidx__1 >= rr_type__linelengthindex__first .
H29:   begidx__1 <= rr_type__linelengthindex__last .
H30:   foundtype__1 >= rr_type__rritemtype__first .
H31:   foundtype__1 <= rr_type__rritemtype__last .
H32:   foundtype__1 = rr_type__control .
H33:   begidx__1 >= rr_type__linelengthindex__first .
H34:   begidx__1 <= rr_type__linelengthindex__last .
H35:   endidx__1 >= rr_type__linelengthindex__first .
H36:   endidx__1 <= rr_type__linelengthindex__last .
H37:   endidx__1 - 6 >= integer__base__first .
H38:   endidx__1 - 6 <= integer__base__last .
H39:   begidx__1 <= endidx__1 - 6 .
H40:   begidx__1 >= rr_type__linelengthindex__first .
H41:   begidx__1 <= rr_type__linelengthindex__last .
H42:   begidx__1 + 6 >= rr_type__linelengthindex__first .
H43:   begidx__1 + 6 <= rr_type__linelengthindex__last .
H44:   begidx__1 + 6 >= integer__base__first .
H45:   begidx__1 + 6 <= integer__base__last .
H46:   begidx__1 + 5 >= rr_type__linelengthindex__first .
H47:   begidx__1 + 5 <= rr_type__linelengthindex__last .
H48:   begidx__1 + 5 >= integer__base__first .
H49:   begidx__1 + 5 <= integer__base__last .
H50:   begidx__1 + 4 >= rr_type__linelengthindex__first .
H51:   begidx__1 + 4 <= rr_type__linelengthindex__last .
H52:   begidx__1 + 4 >= integer__base__first .
H53:   begidx__1 + 4 <= integer__base__last .
H54:   begidx__1 + 3 >= rr_type__linelengthindex__first .
H55:   begidx__1 + 3 <= rr_type__linelengthindex__last .
H56:   begidx__1 + 3 >= integer__base__first .
H57:   begidx__1 + 3 <= integer__base__last .
H58:   begidx__1 + 2 >= rr_type__linelengthindex__first .
H59:   begidx__1 + 2 <= rr_type__linelengthindex__last .
H60:   begidx__1 + 2 >= integer__base__first .
H61:   begidx__1 + 2 <= integer__base__last .
H62:   begidx__1 + 1 >= rr_type__linelengthindex__first .
H63:   begidx__1 + 1 <= rr_type__linelengthindex__last .
H64:   begidx__1 + 1 >= integer__base__first .
H65:   begidx__1 + 1 <= integer__base__last .
H66:   element(zonefileline, [begidx__1 + 1]) = 79 .
H67:   element(zonefileline, [begidx__1 + 2]) = 82 .
H68:   element(zonefileline, [begidx__1 + 3]) = 73 .
H69:   element(zonefileline, [begidx__1 + 4]) = 71 .
H70:   element(zonefileline, [begidx__1 + 5]) = 73 .
H71:   element(zonefileline, [begidx__1 + 6]) = 78 .
H72:   begidx__1 >= rr_type__linelengthindex__first .
H73:   begidx__1 <= rr_type__linelengthindex__last .
H74:   endidx__1 >= rr_type__linelengthindex__first .
H75:   endidx__1 <= rr_type__linelengthindex__last .
H76:   not ((begidx__1 < zlength) and (endidx__1 < zlength)) .
H77:   foundtype__1 >= rr_type__rritemtype__first .
H78:   foundtype__1 <= rr_type__rritemtype__last .
H79:   not (foundtype__1 <> rr_type__domainnameortimespec) .
H80:   endidx__1 >= rr_type__linelengthindex__first .
H81:   endidx__1 <= rr_type__linelengthindex__last .
H82:   endidx__1 >= rr_type__linelengthindex__first .
H83:   endidx__1 <= rr_type__linelengthindex__last .
H84:   not (element(zonefileline, [endidx__1]) <> 46) .
H85:   begidx__1 >= rr_type__linelengthindex__first .
H86:   begidx__1 <= rr_type__linelengthindex__last .
H87:   endidx__1 >= rr_type__linelengthindex__first .
H88:   endidx__1 <= rr_type__linelengthindex__last .
H89:   endidx__1 >= integer__first .
H90:   endidx__1 <= integer__last .
H91:   begidx__1 >= integer__first .
H92:   begidx__1 <= integer__last .
        ->
C1:    (begidx__1 <= endidx__1) -> ((endidx__1 >= integer__first) and (
           endidx__1 <= integer__last)) .
C2:    (begidx__1 <= endidx__1) -> ((begidx__1 >= integer__first) and (
           begidx__1 <= integer__last)) .
 

For path(s) from start to assertion of line 649:

procedure_parsecontrolline_14.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           neworigin, [i___1]) >= character__first) and (element(
           neworigin, [i___1]) <= character__last))) .
H2:    newttl >= unsigned_types__unsigned32__first .
H3:    newttl <= unsigned_types__unsigned32__last .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H5:    zlength >= rr_type__linelengthindex__first .
H6:    zlength <= rr_type__linelengthindex__last .
H7:    1 >= rr_type__linelengthindex__first .
H8:    1 <= rr_type__linelengthindex__last .
H9:    1 >= rr_type__linelengthindex__first .
H10:   1 <= rr_type__linelengthindex__last .
H11:   zlength >= rr_type__linelengthindex__first .
H12:   zlength <= rr_type__linelengthindex__last .
H13:   1 <= zlength .
H14:   begidx__1 <= endidx__1 .
H15:   begidx__1 <= zlength .
H16:   endidx__1 <= zlength .
H17:   (foundtype__1 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__1) and (i_ <= endidx__1)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H18:   begidx__1 >= rr_type__linelengthindex__first .
H19:   begidx__1 <= rr_type__linelengthindex__last .
H20:   endidx__1 >= rr_type__linelengthindex__first .
H21:   endidx__1 <= rr_type__linelengthindex__last .
H22:   foundtype__1 >= rr_type__rritemtype__first .
H23:   foundtype__1 <= rr_type__rritemtype__last .
H24:   foundtype__1 >= rr_type__rritemtype__first .
H25:   foundtype__1 <= rr_type__rritemtype__last .
H26:   endidx__1 >= rr_type__linelengthindex__first .
H27:   endidx__1 <= rr_type__linelengthindex__last .
H28:   begidx__1 >= rr_type__linelengthindex__first .
H29:   begidx__1 <= rr_type__linelengthindex__last .
H30:   foundtype__1 >= rr_type__rritemtype__first .
H31:   foundtype__1 <= rr_type__rritemtype__last .
H32:   foundtype__1 = rr_type__control .
H33:   begidx__1 >= rr_type__linelengthindex__first .
H34:   begidx__1 <= rr_type__linelengthindex__last .
H35:   endidx__1 >= rr_type__linelengthindex__first .
H36:   endidx__1 <= rr_type__linelengthindex__last .
H37:   endidx__1 - 6 >= integer__base__first .
H38:   endidx__1 - 6 <= integer__base__last .
H39:   begidx__1 <= endidx__1 - 6 .
H40:   begidx__1 >= rr_type__linelengthindex__first .
H41:   begidx__1 <= rr_type__linelengthindex__last .
H42:   begidx__1 + 6 >= rr_type__linelengthindex__first .
H43:   begidx__1 + 6 <= rr_type__linelengthindex__last .
H44:   begidx__1 + 6 >= integer__base__first .
H45:   begidx__1 + 6 <= integer__base__last .
H46:   begidx__1 + 5 >= rr_type__linelengthindex__first .
H47:   begidx__1 + 5 <= rr_type__linelengthindex__last .
H48:   begidx__1 + 5 >= integer__base__first .
H49:   begidx__1 + 5 <= integer__base__last .
H50:   begidx__1 + 4 >= rr_type__linelengthindex__first .
H51:   begidx__1 + 4 <= rr_type__linelengthindex__last .
H52:   begidx__1 + 4 >= integer__base__first .
H53:   begidx__1 + 4 <= integer__base__last .
H54:   begidx__1 + 3 >= rr_type__linelengthindex__first .
H55:   begidx__1 + 3 <= rr_type__linelengthindex__last .
H56:   begidx__1 + 3 >= integer__base__first .
H57:   begidx__1 + 3 <= integer__base__last .
H58:   begidx__1 + 2 >= rr_type__linelengthindex__first .
H59:   begidx__1 + 2 <= rr_type__linelengthindex__last .
H60:   begidx__1 + 2 >= integer__base__first .
H61:   begidx__1 + 2 <= integer__base__last .
H62:   begidx__1 + 1 >= rr_type__linelengthindex__first .
H63:   begidx__1 + 1 <= rr_type__linelengthindex__last .
H64:   begidx__1 + 1 >= integer__base__first .
H65:   begidx__1 + 1 <= integer__base__last .
H66:   element(zonefileline, [begidx__1 + 1]) = 79 .
H67:   element(zonefileline, [begidx__1 + 2]) = 82 .
H68:   element(zonefileline, [begidx__1 + 3]) = 73 .
H69:   element(zonefileline, [begidx__1 + 4]) = 71 .
H70:   element(zonefileline, [begidx__1 + 5]) = 73 .
H71:   element(zonefileline, [begidx__1 + 6]) = 78 .
H72:   begidx__1 >= rr_type__linelengthindex__first .
H73:   begidx__1 <= rr_type__linelengthindex__last .
H74:   endidx__1 >= rr_type__linelengthindex__first .
H75:   endidx__1 <= rr_type__linelengthindex__last .
H76:   begidx__1 < zlength .
H77:   endidx__1 < zlength .
H78:   endidx__1 >= rr_type__linelengthindex__first .
H79:   endidx__1 <= rr_type__linelengthindex__last .
H80:   endidx__1 + 1 >= rr_type__linelengthindex__first .
H81:   endidx__1 + 1 <= rr_type__linelengthindex__last .
H82:   endidx__1 + 1 >= rr_type__linelengthindex__first .
H83:   endidx__1 + 1 <= rr_type__linelengthindex__last .
H84:   endidx__1 + 1 >= rr_type__linelengthindex__first .
H85:   endidx__1 + 1 <= rr_type__linelengthindex__last .
H86:   zlength >= rr_type__linelengthindex__first .
H87:   zlength <= rr_type__linelengthindex__last .
H88:   endidx__1 + 1 <= zlength .
H89:   begidx__2 <= endidx__2 .
H90:   begidx__2 <= zlength .
H91:   endidx__2 <= zlength .
H92:   (foundtype__2 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__2) and (i_ <= endidx__2)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H93:   begidx__2 >= rr_type__linelengthindex__first .
H94:   begidx__2 <= rr_type__linelengthindex__last .
H95:   endidx__2 >= rr_type__linelengthindex__first .
H96:   endidx__2 <= rr_type__linelengthindex__last .
H97:   foundtype__2 >= rr_type__rritemtype__first .
H98:   foundtype__2 <= rr_type__rritemtype__last .
H99:   foundtype__2 >= rr_type__rritemtype__first .
H100:  foundtype__2 <= rr_type__rritemtype__last .
H101:  endidx__2 >= rr_type__linelengthindex__first .
H102:  endidx__2 <= rr_type__linelengthindex__last .
H103:  begidx__2 >= rr_type__linelengthindex__first .
H104:  begidx__2 <= rr_type__linelengthindex__last .
H105:  foundtype__2 >= rr_type__rritemtype__first .
H106:  foundtype__2 <= rr_type__rritemtype__last .
H107:  not (foundtype__2 <> rr_type__domainnameortimespec) .
H108:  endidx__2 >= rr_type__linelengthindex__first .
H109:  endidx__2 <= rr_type__linelengthindex__last .
H110:  endidx__2 >= rr_type__linelengthindex__first .
H111:  endidx__2 <= rr_type__linelengthindex__last .
H112:  not (element(zonefileline, [endidx__2]) <> 46) .
H113:  begidx__2 >= rr_type__linelengthindex__first .
H114:  begidx__2 <= rr_type__linelengthindex__last .
H115:  endidx__2 >= rr_type__linelengthindex__first .
H116:  endidx__2 <= rr_type__linelengthindex__last .
H117:  endidx__2 >= integer__first .
H118:  endidx__2 <= integer__last .
H119:  begidx__2 >= integer__first .
H120:  begidx__2 <= integer__last .
H121:  (begidx__2 <= endidx__2) -> ((endidx__2 >= integer__first) and (
           endidx__2 <= integer__last)) .
H122:  (begidx__2 <= endidx__2) -> ((begidx__2 >= integer__first) and (
           begidx__2 <= integer__last)) .
H123:  begidx__2 >= rr_type__linelengthindex__first .
H124:  begidx__2 <= rr_type__linelengthindex__last .
H125:  endidx__2 >= rr_type__linelengthindex__first .
H126:  endidx__2 <= rr_type__linelengthindex__last .
H127:  begidx__2 <= endidx__2 .
        ->
C1:    begidx__2 >= 1 .
C2:    begidx__2 <= endidx__2 .
C3:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           neworigin, [i___1]) >= character__first) and (element(
           neworigin, [i___1]) <= character__last))) .
C4:    newttl >= unsigned_types__unsigned32__first .
C5:    newttl <= unsigned_types__unsigned32__last .
C6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
C7:    zlength >= rr_type__linelengthindex__first .
C8:    zlength <= rr_type__linelengthindex__last .
C9:    begidx__2 >= integer__first .
C10:   begidx__2 <= integer__last .
C11:   begidx__2 >= begidx__2 .
C12:   begidx__2 <= endidx__2 .
C13:   endidx__2 >= rr_type__linelengthindex__first .
C14:   endidx__2 <= rr_type__linelengthindex__last .
 

procedure_parsecontrolline_15.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           neworigin, [i___1]) >= character__first) and (element(
           neworigin, [i___1]) <= character__last))) .
H2:    newttl >= unsigned_types__unsigned32__first .
H3:    newttl <= unsigned_types__unsigned32__last .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H5:    zlength >= rr_type__linelengthindex__first .
H6:    zlength <= rr_type__linelengthindex__last .
H7:    1 >= rr_type__linelengthindex__first .
H8:    1 <= rr_type__linelengthindex__last .
H9:    1 >= rr_type__linelengthindex__first .
H10:   1 <= rr_type__linelengthindex__last .
H11:   zlength >= rr_type__linelengthindex__first .
H12:   zlength <= rr_type__linelengthindex__last .
H13:   1 <= zlength .
H14:   begidx__1 <= endidx__1 .
H15:   begidx__1 <= zlength .
H16:   endidx__1 <= zlength .
H17:   (foundtype__1 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__1) and (i_ <= endidx__1)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H18:   begidx__1 >= rr_type__linelengthindex__first .
H19:   begidx__1 <= rr_type__linelengthindex__last .
H20:   endidx__1 >= rr_type__linelengthindex__first .
H21:   endidx__1 <= rr_type__linelengthindex__last .
H22:   foundtype__1 >= rr_type__rritemtype__first .
H23:   foundtype__1 <= rr_type__rritemtype__last .
H24:   foundtype__1 >= rr_type__rritemtype__first .
H25:   foundtype__1 <= rr_type__rritemtype__last .
H26:   endidx__1 >= rr_type__linelengthindex__first .
H27:   endidx__1 <= rr_type__linelengthindex__last .
H28:   begidx__1 >= rr_type__linelengthindex__first .
H29:   begidx__1 <= rr_type__linelengthindex__last .
H30:   foundtype__1 >= rr_type__rritemtype__first .
H31:   foundtype__1 <= rr_type__rritemtype__last .
H32:   foundtype__1 = rr_type__control .
H33:   begidx__1 >= rr_type__linelengthindex__first .
H34:   begidx__1 <= rr_type__linelengthindex__last .
H35:   endidx__1 >= rr_type__linelengthindex__first .
H36:   endidx__1 <= rr_type__linelengthindex__last .
H37:   endidx__1 - 6 >= integer__base__first .
H38:   endidx__1 - 6 <= integer__base__last .
H39:   begidx__1 <= endidx__1 - 6 .
H40:   begidx__1 >= rr_type__linelengthindex__first .
H41:   begidx__1 <= rr_type__linelengthindex__last .
H42:   begidx__1 + 6 >= rr_type__linelengthindex__first .
H43:   begidx__1 + 6 <= rr_type__linelengthindex__last .
H44:   begidx__1 + 6 >= integer__base__first .
H45:   begidx__1 + 6 <= integer__base__last .
H46:   begidx__1 + 5 >= rr_type__linelengthindex__first .
H47:   begidx__1 + 5 <= rr_type__linelengthindex__last .
H48:   begidx__1 + 5 >= integer__base__first .
H49:   begidx__1 + 5 <= integer__base__last .
H50:   begidx__1 + 4 >= rr_type__linelengthindex__first .
H51:   begidx__1 + 4 <= rr_type__linelengthindex__last .
H52:   begidx__1 + 4 >= integer__base__first .
H53:   begidx__1 + 4 <= integer__base__last .
H54:   begidx__1 + 3 >= rr_type__linelengthindex__first .
H55:   begidx__1 + 3 <= rr_type__linelengthindex__last .
H56:   begidx__1 + 3 >= integer__base__first .
H57:   begidx__1 + 3 <= integer__base__last .
H58:   begidx__1 + 2 >= rr_type__linelengthindex__first .
H59:   begidx__1 + 2 <= rr_type__linelengthindex__last .
H60:   begidx__1 + 2 >= integer__base__first .
H61:   begidx__1 + 2 <= integer__base__last .
H62:   begidx__1 + 1 >= rr_type__linelengthindex__first .
H63:   begidx__1 + 1 <= rr_type__linelengthindex__last .
H64:   begidx__1 + 1 >= integer__base__first .
H65:   begidx__1 + 1 <= integer__base__last .
H66:   element(zonefileline, [begidx__1 + 1]) = 79 .
H67:   element(zonefileline, [begidx__1 + 2]) = 82 .
H68:   element(zonefileline, [begidx__1 + 3]) = 73 .
H69:   element(zonefileline, [begidx__1 + 4]) = 71 .
H70:   element(zonefileline, [begidx__1 + 5]) = 73 .
H71:   element(zonefileline, [begidx__1 + 6]) = 78 .
H72:   begidx__1 >= rr_type__linelengthindex__first .
H73:   begidx__1 <= rr_type__linelengthindex__last .
H74:   endidx__1 >= rr_type__linelengthindex__first .
H75:   endidx__1 <= rr_type__linelengthindex__last .
H76:   not ((begidx__1 < zlength) and (endidx__1 < zlength)) .
H77:   foundtype__1 >= rr_type__rritemtype__first .
H78:   foundtype__1 <= rr_type__rritemtype__last .
H79:   not (foundtype__1 <> rr_type__domainnameortimespec) .
H80:   endidx__1 >= rr_type__linelengthindex__first .
H81:   endidx__1 <= rr_type__linelengthindex__last .
H82:   endidx__1 >= rr_type__linelengthindex__first .
H83:   endidx__1 <= rr_type__linelengthindex__last .
H84:   not (element(zonefileline, [endidx__1]) <> 46) .
H85:   begidx__1 >= rr_type__linelengthindex__first .
H86:   begidx__1 <= rr_type__linelengthindex__last .
H87:   endidx__1 >= rr_type__linelengthindex__first .
H88:   endidx__1 <= rr_type__linelengthindex__last .
H89:   endidx__1 >= integer__first .
H90:   endidx__1 <= integer__last .
H91:   begidx__1 >= integer__first .
H92:   begidx__1 <= integer__last .
H93:   (begidx__1 <= endidx__1) -> ((endidx__1 >= integer__first) and (
           endidx__1 <= integer__last)) .
H94:   (begidx__1 <= endidx__1) -> ((begidx__1 >= integer__first) and (
           begidx__1 <= integer__last)) .
H95:   begidx__1 >= rr_type__linelengthindex__first .
H96:   begidx__1 <= rr_type__linelengthindex__last .
H97:   endidx__1 >= rr_type__linelengthindex__first .
H98:   endidx__1 <= rr_type__linelengthindex__last .
H99:   begidx__1 <= endidx__1 .
        ->
C1:    begidx__1 >= 1 .
C2:    begidx__1 <= endidx__1 .
C3:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           neworigin, [i___1]) >= character__first) and (element(
           neworigin, [i___1]) <= character__last))) .
C4:    newttl >= unsigned_types__unsigned32__first .
C5:    newttl <= unsigned_types__unsigned32__last .
C6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
C7:    zlength >= rr_type__linelengthindex__first .
C8:    zlength <= rr_type__linelengthindex__last .
C9:    begidx__1 >= integer__first .
C10:   begidx__1 <= integer__last .
C11:   begidx__1 >= begidx__1 .
C12:   begidx__1 <= endidx__1 .
C13:   endidx__1 >= rr_type__linelengthindex__first .
C14:   endidx__1 <= rr_type__linelengthindex__last .
 

For path(s) from assertion of line 649 to assertion of line 649:

procedure_parsecontrolline_16.
H1:    begidx >= 1 .
H2:    begidx <= endidx .
H3:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           neworigin, [i___1]) >= character__first) and (element(
           neworigin, [i___1]) <= character__last))) .
H4:    newttl >= unsigned_types__unsigned32__first .
H5:    newttl <= unsigned_types__unsigned32__last .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H7:    zlength >= rr_type__linelengthindex__first .
H8:    zlength <= rr_type__linelengthindex__last .
H9:    loop__1__i >= integer__first .
H10:   loop__1__i <= integer__last .
H11:   loop__1__i >= begidx .
H12:   loop__1__i <= endidx__entry__loop__1 .
H13:   endidx__entry__loop__1 >= rr_type__linelengthindex__first .
H14:   endidx__entry__loop__1 <= rr_type__linelengthindex__last .
H15:   element(zonefileline, [loop__1__i]) >= character__first .
H16:   element(zonefileline, [loop__1__i]) <= character__last .
H17:   loop__1__i >= rr_type__linelengthindex__first .
H18:   loop__1__i <= rr_type__linelengthindex__last .
H19:   loop__1__i >= rr_type__linelengthindex__first .
H20:   loop__1__i <= rr_type__linelengthindex__last .
H21:   not (loop__1__i = endidx__entry__loop__1) .
        ->
C1:    begidx >= 1 .
C2:    begidx <= endidx .
C3:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           neworigin, [i___1]) >= character__first) and (element(
           neworigin, [i___1]) <= character__last))) .
C4:    newttl >= unsigned_types__unsigned32__first .
C5:    newttl <= unsigned_types__unsigned32__last .
C6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
C7:    zlength >= rr_type__linelengthindex__first .
C8:    zlength <= rr_type__linelengthindex__last .
C9:    loop__1__i + 1 >= integer__first .
C10:   loop__1__i + 1 <= integer__last .
C11:   loop__1__i + 1 >= begidx .
C12:   loop__1__i + 1 <= endidx__entry__loop__1 .
C13:   endidx__entry__loop__1 >= rr_type__linelengthindex__first .
C14:   endidx__entry__loop__1 <= rr_type__linelengthindex__last .
 

For path(s) from assertion of line 649 to run-time check associated with statement of line 650:

procedure_parsecontrolline_17.
H1:    begidx >= 1 .
H2:    begidx <= endidx .
H3:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           neworigin, [i___1]) >= character__first) and (element(
           neworigin, [i___1]) <= character__last))) .
H4:    newttl >= unsigned_types__unsigned32__first .
H5:    newttl <= unsigned_types__unsigned32__last .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H7:    zlength >= rr_type__linelengthindex__first .
H8:    zlength <= rr_type__linelengthindex__last .
H9:    loop__1__i >= integer__first .
H10:   loop__1__i <= integer__last .
H11:   loop__1__i >= begidx .
H12:   loop__1__i <= endidx__entry__loop__1 .
H13:   endidx__entry__loop__1 >= rr_type__linelengthindex__first .
H14:   endidx__entry__loop__1 <= rr_type__linelengthindex__last .
        ->
C1:    element(zonefileline, [loop__1__i]) >= character__first .
C2:    element(zonefileline, [loop__1__i]) <= character__last .
C3:    loop__1__i >= rr_type__linelengthindex__first .
C4:    loop__1__i <= rr_type__linelengthindex__last .
C5:    loop__1__i >= rr_type__linelengthindex__first .
C6:    loop__1__i <= rr_type__linelengthindex__last .
 

For path(s) from start to run-time check associated with statement of line 654:

procedure_parsecontrolline_18.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           neworigin, [i___1]) >= character__first) and (element(
           neworigin, [i___1]) <= character__last))) .
H2:    newttl >= unsigned_types__unsigned32__first .
H3:    newttl <= unsigned_types__unsigned32__last .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H5:    zlength >= rr_type__linelengthindex__first .
H6:    zlength <= rr_type__linelengthindex__last .
H7:    1 >= rr_type__linelengthindex__first .
H8:    1 <= rr_type__linelengthindex__last .
H9:    1 >= rr_type__linelengthindex__first .
H10:   1 <= rr_type__linelengthindex__last .
H11:   zlength >= rr_type__linelengthindex__first .
H12:   zlength <= rr_type__linelengthindex__last .
H13:   1 <= zlength .
H14:   begidx__1 <= endidx__1 .
H15:   begidx__1 <= zlength .
H16:   endidx__1 <= zlength .
H17:   (foundtype__1 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__1) and (i_ <= endidx__1)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H18:   begidx__1 >= rr_type__linelengthindex__first .
H19:   begidx__1 <= rr_type__linelengthindex__last .
H20:   endidx__1 >= rr_type__linelengthindex__first .
H21:   endidx__1 <= rr_type__linelengthindex__last .
H22:   foundtype__1 >= rr_type__rritemtype__first .
H23:   foundtype__1 <= rr_type__rritemtype__last .
H24:   foundtype__1 >= rr_type__rritemtype__first .
H25:   foundtype__1 <= rr_type__rritemtype__last .
H26:   endidx__1 >= rr_type__linelengthindex__first .
H27:   endidx__1 <= rr_type__linelengthindex__last .
H28:   begidx__1 >= rr_type__linelengthindex__first .
H29:   begidx__1 <= rr_type__linelengthindex__last .
H30:   foundtype__1 >= rr_type__rritemtype__first .
H31:   foundtype__1 <= rr_type__rritemtype__last .
H32:   foundtype__1 = rr_type__control .
H33:   begidx__1 >= rr_type__linelengthindex__first .
H34:   begidx__1 <= rr_type__linelengthindex__last .
H35:   endidx__1 >= rr_type__linelengthindex__first .
H36:   endidx__1 <= rr_type__linelengthindex__last .
H37:   endidx__1 - 6 >= integer__base__first .
H38:   endidx__1 - 6 <= integer__base__last .
H39:   begidx__1 <= endidx__1 - 6 .
H40:   begidx__1 >= rr_type__linelengthindex__first .
H41:   begidx__1 <= rr_type__linelengthindex__last .
H42:   begidx__1 + 6 >= rr_type__linelengthindex__first .
H43:   begidx__1 + 6 <= rr_type__linelengthindex__last .
H44:   begidx__1 + 6 >= integer__base__first .
H45:   begidx__1 + 6 <= integer__base__last .
H46:   begidx__1 + 5 >= rr_type__linelengthindex__first .
H47:   begidx__1 + 5 <= rr_type__linelengthindex__last .
H48:   begidx__1 + 5 >= integer__base__first .
H49:   begidx__1 + 5 <= integer__base__last .
H50:   begidx__1 + 4 >= rr_type__linelengthindex__first .
H51:   begidx__1 + 4 <= rr_type__linelengthindex__last .
H52:   begidx__1 + 4 >= integer__base__first .
H53:   begidx__1 + 4 <= integer__base__last .
H54:   begidx__1 + 3 >= rr_type__linelengthindex__first .
H55:   begidx__1 + 3 <= rr_type__linelengthindex__last .
H56:   begidx__1 + 3 >= integer__base__first .
H57:   begidx__1 + 3 <= integer__base__last .
H58:   begidx__1 + 2 >= rr_type__linelengthindex__first .
H59:   begidx__1 + 2 <= rr_type__linelengthindex__last .
H60:   begidx__1 + 2 >= integer__base__first .
H61:   begidx__1 + 2 <= integer__base__last .
H62:   begidx__1 + 1 >= rr_type__linelengthindex__first .
H63:   begidx__1 + 1 <= rr_type__linelengthindex__last .
H64:   begidx__1 + 1 >= integer__base__first .
H65:   begidx__1 + 1 <= integer__base__last .
H66:   element(zonefileline, [begidx__1 + 1]) = 79 .
H67:   element(zonefileline, [begidx__1 + 2]) = 82 .
H68:   element(zonefileline, [begidx__1 + 3]) = 73 .
H69:   element(zonefileline, [begidx__1 + 4]) = 71 .
H70:   element(zonefileline, [begidx__1 + 5]) = 73 .
H71:   element(zonefileline, [begidx__1 + 6]) = 78 .
H72:   begidx__1 >= rr_type__linelengthindex__first .
H73:   begidx__1 <= rr_type__linelengthindex__last .
H74:   endidx__1 >= rr_type__linelengthindex__first .
H75:   endidx__1 <= rr_type__linelengthindex__last .
H76:   begidx__1 < zlength .
H77:   endidx__1 < zlength .
H78:   endidx__1 >= rr_type__linelengthindex__first .
H79:   endidx__1 <= rr_type__linelengthindex__last .
H80:   endidx__1 + 1 >= rr_type__linelengthindex__first .
H81:   endidx__1 + 1 <= rr_type__linelengthindex__last .
H82:   endidx__1 + 1 >= rr_type__linelengthindex__first .
H83:   endidx__1 + 1 <= rr_type__linelengthindex__last .
H84:   endidx__1 + 1 >= rr_type__linelengthindex__first .
H85:   endidx__1 + 1 <= rr_type__linelengthindex__last .
H86:   zlength >= rr_type__linelengthindex__first .
H87:   zlength <= rr_type__linelengthindex__last .
H88:   endidx__1 + 1 <= zlength .
H89:   begidx__2 <= endidx__2 .
H90:   begidx__2 <= zlength .
H91:   endidx__2 <= zlength .
H92:   (foundtype__2 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__2) and (i_ <= endidx__2)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H93:   begidx__2 >= rr_type__linelengthindex__first .
H94:   begidx__2 <= rr_type__linelengthindex__last .
H95:   endidx__2 >= rr_type__linelengthindex__first .
H96:   endidx__2 <= rr_type__linelengthindex__last .
H97:   foundtype__2 >= rr_type__rritemtype__first .
H98:   foundtype__2 <= rr_type__rritemtype__last .
H99:   foundtype__2 >= rr_type__rritemtype__first .
H100:  foundtype__2 <= rr_type__rritemtype__last .
H101:  endidx__2 >= rr_type__linelengthindex__first .
H102:  endidx__2 <= rr_type__linelengthindex__last .
H103:  begidx__2 >= rr_type__linelengthindex__first .
H104:  begidx__2 <= rr_type__linelengthindex__last .
H105:  foundtype__2 >= rr_type__rritemtype__first .
H106:  foundtype__2 <= rr_type__rritemtype__last .
H107:  not (foundtype__2 <> rr_type__domainnameortimespec) .
H108:  endidx__2 >= rr_type__linelengthindex__first .
H109:  endidx__2 <= rr_type__linelengthindex__last .
H110:  endidx__2 >= rr_type__linelengthindex__first .
H111:  endidx__2 <= rr_type__linelengthindex__last .
H112:  not (element(zonefileline, [endidx__2]) <> 46) .
H113:  begidx__2 >= rr_type__linelengthindex__first .
H114:  begidx__2 <= rr_type__linelengthindex__last .
H115:  endidx__2 >= rr_type__linelengthindex__first .
H116:  endidx__2 <= rr_type__linelengthindex__last .
H117:  endidx__2 >= integer__first .
H118:  endidx__2 <= integer__last .
H119:  begidx__2 >= integer__first .
H120:  begidx__2 <= integer__last .
H121:  (begidx__2 <= endidx__2) -> ((endidx__2 >= integer__first) and (
           endidx__2 <= integer__last)) .
H122:  (begidx__2 <= endidx__2) -> ((begidx__2 >= integer__first) and (
           begidx__2 <= integer__last)) .
H123:  begidx__2 >= rr_type__linelengthindex__first .
H124:  begidx__2 <= rr_type__linelengthindex__last .
H125:  endidx__2 >= rr_type__linelengthindex__first .
H126:  endidx__2 <= rr_type__linelengthindex__last .
H127:  not (begidx__2 <= endidx__2) .
        ->
C1:    65 >= character__first .
C2:    65 <= character__last .
C3:    1 >= rr_type__linelengthindex__first .
C4:    1 <= rr_type__linelengthindex__last .
 

procedure_parsecontrolline_19.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           neworigin, [i___1]) >= character__first) and (element(
           neworigin, [i___1]) <= character__last))) .
H2:    newttl >= unsigned_types__unsigned32__first .
H3:    newttl <= unsigned_types__unsigned32__last .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H5:    zlength >= rr_type__linelengthindex__first .
H6:    zlength <= rr_type__linelengthindex__last .
H7:    1 >= rr_type__linelengthindex__first .
H8:    1 <= rr_type__linelengthindex__last .
H9:    1 >= rr_type__linelengthindex__first .
H10:   1 <= rr_type__linelengthindex__last .
H11:   zlength >= rr_type__linelengthindex__first .
H12:   zlength <= rr_type__linelengthindex__last .
H13:   1 <= zlength .
H14:   begidx__1 <= endidx__1 .
H15:   begidx__1 <= zlength .
H16:   endidx__1 <= zlength .
H17:   (foundtype__1 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__1) and (i_ <= endidx__1)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H18:   begidx__1 >= rr_type__linelengthindex__first .
H19:   begidx__1 <= rr_type__linelengthindex__last .
H20:   endidx__1 >= rr_type__linelengthindex__first .
H21:   endidx__1 <= rr_type__linelengthindex__last .
H22:   foundtype__1 >= rr_type__rritemtype__first .
H23:   foundtype__1 <= rr_type__rritemtype__last .
H24:   foundtype__1 >= rr_type__rritemtype__first .
H25:   foundtype__1 <= rr_type__rritemtype__last .
H26:   endidx__1 >= rr_type__linelengthindex__first .
H27:   endidx__1 <= rr_type__linelengthindex__last .
H28:   begidx__1 >= rr_type__linelengthindex__first .
H29:   begidx__1 <= rr_type__linelengthindex__last .
H30:   foundtype__1 >= rr_type__rritemtype__first .
H31:   foundtype__1 <= rr_type__rritemtype__last .
H32:   foundtype__1 = rr_type__control .
H33:   begidx__1 >= rr_type__linelengthindex__first .
H34:   begidx__1 <= rr_type__linelengthindex__last .
H35:   endidx__1 >= rr_type__linelengthindex__first .
H36:   endidx__1 <= rr_type__linelengthindex__last .
H37:   endidx__1 - 6 >= integer__base__first .
H38:   endidx__1 - 6 <= integer__base__last .
H39:   begidx__1 <= endidx__1 - 6 .
H40:   begidx__1 >= rr_type__linelengthindex__first .
H41:   begidx__1 <= rr_type__linelengthindex__last .
H42:   begidx__1 + 6 >= rr_type__linelengthindex__first .
H43:   begidx__1 + 6 <= rr_type__linelengthindex__last .
H44:   begidx__1 + 6 >= integer__base__first .
H45:   begidx__1 + 6 <= integer__base__last .
H46:   begidx__1 + 5 >= rr_type__linelengthindex__first .
H47:   begidx__1 + 5 <= rr_type__linelengthindex__last .
H48:   begidx__1 + 5 >= integer__base__first .
H49:   begidx__1 + 5 <= integer__base__last .
H50:   begidx__1 + 4 >= rr_type__linelengthindex__first .
H51:   begidx__1 + 4 <= rr_type__linelengthindex__last .
H52:   begidx__1 + 4 >= integer__base__first .
H53:   begidx__1 + 4 <= integer__base__last .
H54:   begidx__1 + 3 >= rr_type__linelengthindex__first .
H55:   begidx__1 + 3 <= rr_type__linelengthindex__last .
H56:   begidx__1 + 3 >= integer__base__first .
H57:   begidx__1 + 3 <= integer__base__last .
H58:   begidx__1 + 2 >= rr_type__linelengthindex__first .
H59:   begidx__1 + 2 <= rr_type__linelengthindex__last .
H60:   begidx__1 + 2 >= integer__base__first .
H61:   begidx__1 + 2 <= integer__base__last .
H62:   begidx__1 + 1 >= rr_type__linelengthindex__first .
H63:   begidx__1 + 1 <= rr_type__linelengthindex__last .
H64:   begidx__1 + 1 >= integer__base__first .
H65:   begidx__1 + 1 <= integer__base__last .
H66:   element(zonefileline, [begidx__1 + 1]) = 79 .
H67:   element(zonefileline, [begidx__1 + 2]) = 82 .
H68:   element(zonefileline, [begidx__1 + 3]) = 73 .
H69:   element(zonefileline, [begidx__1 + 4]) = 71 .
H70:   element(zonefileline, [begidx__1 + 5]) = 73 .
H71:   element(zonefileline, [begidx__1 + 6]) = 78 .
H72:   begidx__1 >= rr_type__linelengthindex__first .
H73:   begidx__1 <= rr_type__linelengthindex__last .
H74:   endidx__1 >= rr_type__linelengthindex__first .
H75:   endidx__1 <= rr_type__linelengthindex__last .
H76:   not ((begidx__1 < zlength) and (endidx__1 < zlength)) .
H77:   foundtype__1 >= rr_type__rritemtype__first .
H78:   foundtype__1 <= rr_type__rritemtype__last .
H79:   not (foundtype__1 <> rr_type__domainnameortimespec) .
H80:   endidx__1 >= rr_type__linelengthindex__first .
H81:   endidx__1 <= rr_type__linelengthindex__last .
H82:   endidx__1 >= rr_type__linelengthindex__first .
H83:   endidx__1 <= rr_type__linelengthindex__last .
H84:   not (element(zonefileline, [endidx__1]) <> 46) .
H85:   begidx__1 >= rr_type__linelengthindex__first .
H86:   begidx__1 <= rr_type__linelengthindex__last .
H87:   endidx__1 >= rr_type__linelengthindex__first .
H88:   endidx__1 <= rr_type__linelengthindex__last .
H89:   endidx__1 >= integer__first .
H90:   endidx__1 <= integer__last .
H91:   begidx__1 >= integer__first .
H92:   begidx__1 <= integer__last .
H93:   (begidx__1 <= endidx__1) -> ((endidx__1 >= integer__first) and (
           endidx__1 <= integer__last)) .
H94:   (begidx__1 <= endidx__1) -> ((begidx__1 >= integer__first) and (
           begidx__1 <= integer__last)) .
H95:   begidx__1 >= rr_type__linelengthindex__first .
H96:   begidx__1 <= rr_type__linelengthindex__last .
H97:   endidx__1 >= rr_type__linelengthindex__first .
H98:   endidx__1 <= rr_type__linelengthindex__last .
H99:   not (begidx__1 <= endidx__1) .
        ->
C1:    65 >= character__first .
C2:    65 <= character__last .
C3:    1 >= rr_type__linelengthindex__first .
C4:    1 <= rr_type__linelengthindex__last .
 

For path(s) from assertion of line 649 to run-time check associated with statement of line 654:

procedure_parsecontrolline_20.
H1:    begidx >= 1 .
H2:    begidx <= endidx .
H3:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           neworigin, [i___1]) >= character__first) and (element(
           neworigin, [i___1]) <= character__last))) .
H4:    newttl >= unsigned_types__unsigned32__first .
H5:    newttl <= unsigned_types__unsigned32__last .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H7:    zlength >= rr_type__linelengthindex__first .
H8:    zlength <= rr_type__linelengthindex__last .
H9:    loop__1__i >= integer__first .
H10:   loop__1__i <= integer__last .
H11:   loop__1__i >= begidx .
H12:   loop__1__i <= endidx__entry__loop__1 .
H13:   endidx__entry__loop__1 >= rr_type__linelengthindex__first .
H14:   endidx__entry__loop__1 <= rr_type__linelengthindex__last .
H15:   element(zonefileline, [loop__1__i]) >= character__first .
H16:   element(zonefileline, [loop__1__i]) <= character__last .
H17:   loop__1__i >= rr_type__linelengthindex__first .
H18:   loop__1__i <= rr_type__linelengthindex__last .
H19:   loop__1__i >= rr_type__linelengthindex__first .
H20:   loop__1__i <= rr_type__linelengthindex__last .
H21:   loop__1__i = endidx__entry__loop__1 .
        ->
C1:    65 >= character__first .
C2:    65 <= character__last .
C3:    1 >= rr_type__linelengthindex__first .
C4:    1 <= rr_type__linelengthindex__last .
 

For path(s) from start to run-time check associated with statement of line 655:

procedure_parsecontrolline_21.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           neworigin, [i___1]) >= character__first) and (element(
           neworigin, [i___1]) <= character__last))) .
H2:    newttl >= unsigned_types__unsigned32__first .
H3:    newttl <= unsigned_types__unsigned32__last .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H5:    zlength >= rr_type__linelengthindex__first .
H6:    zlength <= rr_type__linelengthindex__last .
H7:    1 >= rr_type__linelengthindex__first .
H8:    1 <= rr_type__linelengthindex__last .
H9:    1 >= rr_type__linelengthindex__first .
H10:   1 <= rr_type__linelengthindex__last .
H11:   zlength >= rr_type__linelengthindex__first .
H12:   zlength <= rr_type__linelengthindex__last .
H13:   1 <= zlength .
H14:   begidx__1 <= endidx__1 .
H15:   begidx__1 <= zlength .
H16:   endidx__1 <= zlength .
H17:   (foundtype__1 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__1) and (i_ <= endidx__1)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H18:   begidx__1 >= rr_type__linelengthindex__first .
H19:   begidx__1 <= rr_type__linelengthindex__last .
H20:   endidx__1 >= rr_type__linelengthindex__first .
H21:   endidx__1 <= rr_type__linelengthindex__last .
H22:   foundtype__1 >= rr_type__rritemtype__first .
H23:   foundtype__1 <= rr_type__rritemtype__last .
H24:   foundtype__1 >= rr_type__rritemtype__first .
H25:   foundtype__1 <= rr_type__rritemtype__last .
H26:   endidx__1 >= rr_type__linelengthindex__first .
H27:   endidx__1 <= rr_type__linelengthindex__last .
H28:   begidx__1 >= rr_type__linelengthindex__first .
H29:   begidx__1 <= rr_type__linelengthindex__last .
H30:   foundtype__1 >= rr_type__rritemtype__first .
H31:   foundtype__1 <= rr_type__rritemtype__last .
H32:   foundtype__1 = rr_type__control .
H33:   begidx__1 >= rr_type__linelengthindex__first .
H34:   begidx__1 <= rr_type__linelengthindex__last .
H35:   endidx__1 >= rr_type__linelengthindex__first .
H36:   endidx__1 <= rr_type__linelengthindex__last .
H37:   endidx__1 - 6 >= integer__base__first .
H38:   endidx__1 - 6 <= integer__base__last .
H39:   begidx__1 <= endidx__1 - 6 .
H40:   begidx__1 >= rr_type__linelengthindex__first .
H41:   begidx__1 <= rr_type__linelengthindex__last .
H42:   begidx__1 + 6 >= rr_type__linelengthindex__first .
H43:   begidx__1 + 6 <= rr_type__linelengthindex__last .
H44:   begidx__1 + 6 >= integer__base__first .
H45:   begidx__1 + 6 <= integer__base__last .
H46:   begidx__1 + 5 >= rr_type__linelengthindex__first .
H47:   begidx__1 + 5 <= rr_type__linelengthindex__last .
H48:   begidx__1 + 5 >= integer__base__first .
H49:   begidx__1 + 5 <= integer__base__last .
H50:   begidx__1 + 4 >= rr_type__linelengthindex__first .
H51:   begidx__1 + 4 <= rr_type__linelengthindex__last .
H52:   begidx__1 + 4 >= integer__base__first .
H53:   begidx__1 + 4 <= integer__base__last .
H54:   begidx__1 + 3 >= rr_type__linelengthindex__first .
H55:   begidx__1 + 3 <= rr_type__linelengthindex__last .
H56:   begidx__1 + 3 >= integer__base__first .
H57:   begidx__1 + 3 <= integer__base__last .
H58:   begidx__1 + 2 >= rr_type__linelengthindex__first .
H59:   begidx__1 + 2 <= rr_type__linelengthindex__last .
H60:   begidx__1 + 2 >= integer__base__first .
H61:   begidx__1 + 2 <= integer__base__last .
H62:   begidx__1 + 1 >= rr_type__linelengthindex__first .
H63:   begidx__1 + 1 <= rr_type__linelengthindex__last .
H64:   begidx__1 + 1 >= integer__base__first .
H65:   begidx__1 + 1 <= integer__base__last .
H66:   element(zonefileline, [begidx__1 + 1]) = 79 .
H67:   element(zonefileline, [begidx__1 + 2]) = 82 .
H68:   element(zonefileline, [begidx__1 + 3]) = 73 .
H69:   element(zonefileline, [begidx__1 + 4]) = 71 .
H70:   element(zonefileline, [begidx__1 + 5]) = 73 .
H71:   element(zonefileline, [begidx__1 + 6]) = 78 .
H72:   begidx__1 >= rr_type__linelengthindex__first .
H73:   begidx__1 <= rr_type__linelengthindex__last .
H74:   endidx__1 >= rr_type__linelengthindex__first .
H75:   endidx__1 <= rr_type__linelengthindex__last .
H76:   begidx__1 < zlength .
H77:   endidx__1 < zlength .
H78:   endidx__1 >= rr_type__linelengthindex__first .
H79:   endidx__1 <= rr_type__linelengthindex__last .
H80:   endidx__1 + 1 >= rr_type__linelengthindex__first .
H81:   endidx__1 + 1 <= rr_type__linelengthindex__last .
H82:   endidx__1 + 1 >= rr_type__linelengthindex__first .
H83:   endidx__1 + 1 <= rr_type__linelengthindex__last .
H84:   endidx__1 + 1 >= rr_type__linelengthindex__first .
H85:   endidx__1 + 1 <= rr_type__linelengthindex__last .
H86:   zlength >= rr_type__linelengthindex__first .
H87:   zlength <= rr_type__linelengthindex__last .
H88:   endidx__1 + 1 <= zlength .
H89:   begidx__2 <= endidx__2 .
H90:   begidx__2 <= zlength .
H91:   endidx__2 <= zlength .
H92:   (foundtype__2 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__2) and (i_ <= endidx__2)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H93:   begidx__2 >= rr_type__linelengthindex__first .
H94:   begidx__2 <= rr_type__linelengthindex__last .
H95:   endidx__2 >= rr_type__linelengthindex__first .
H96:   endidx__2 <= rr_type__linelengthindex__last .
H97:   foundtype__2 >= rr_type__rritemtype__first .
H98:   foundtype__2 <= rr_type__rritemtype__last .
H99:   foundtype__2 >= rr_type__rritemtype__first .
H100:  foundtype__2 <= rr_type__rritemtype__last .
H101:  endidx__2 >= rr_type__linelengthindex__first .
H102:  endidx__2 <= rr_type__linelengthindex__last .
H103:  begidx__2 >= rr_type__linelengthindex__first .
H104:  begidx__2 <= rr_type__linelengthindex__last .
H105:  foundtype__2 >= rr_type__rritemtype__first .
H106:  foundtype__2 <= rr_type__rritemtype__last .
H107:  not (foundtype__2 <> rr_type__domainnameortimespec) .
H108:  endidx__2 >= rr_type__linelengthindex__first .
H109:  endidx__2 <= rr_type__linelengthindex__last .
H110:  endidx__2 >= rr_type__linelengthindex__first .
H111:  endidx__2 <= rr_type__linelengthindex__last .
H112:  not (element(zonefileline, [endidx__2]) <> 46) .
H113:  begidx__2 >= rr_type__linelengthindex__first .
H114:  begidx__2 <= rr_type__linelengthindex__last .
H115:  endidx__2 >= rr_type__linelengthindex__first .
H116:  endidx__2 <= rr_type__linelengthindex__last .
H117:  endidx__2 >= integer__first .
H118:  endidx__2 <= integer__last .
H119:  begidx__2 >= integer__first .
H120:  begidx__2 <= integer__last .
H121:  (begidx__2 <= endidx__2) -> ((endidx__2 >= integer__first) and (
           endidx__2 <= integer__last)) .
H122:  (begidx__2 <= endidx__2) -> ((begidx__2 >= integer__first) and (
           begidx__2 <= integer__last)) .
H123:  begidx__2 >= rr_type__linelengthindex__first .
H124:  begidx__2 <= rr_type__linelengthindex__last .
H125:  endidx__2 >= rr_type__linelengthindex__first .
H126:  endidx__2 <= rr_type__linelengthindex__last .
H127:  not (begidx__2 <= endidx__2) .
H128:  65 >= character__first .
H129:  65 <= character__last .
H130:  1 >= rr_type__linelengthindex__first .
H131:  1 <= rr_type__linelengthindex__last .
H132:  for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(update(
           mk__string(32), [1], 65), [i___1]) >= character__first) and (element(update(
           mk__string(32), [1], 65), [i___1]) <= character__last))) .
        ->
C1:    rr_type__maxlinelength >= rr_type__linelengthindex__first .
C2:    rr_type__maxlinelength <= rr_type__linelengthindex__last .
 

procedure_parsecontrolline_22.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           neworigin, [i___1]) >= character__first) and (element(
           neworigin, [i___1]) <= character__last))) .
H2:    newttl >= unsigned_types__unsigned32__first .
H3:    newttl <= unsigned_types__unsigned32__last .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H5:    zlength >= rr_type__linelengthindex__first .
H6:    zlength <= rr_type__linelengthindex__last .
H7:    1 >= rr_type__linelengthindex__first .
H8:    1 <= rr_type__linelengthindex__last .
H9:    1 >= rr_type__linelengthindex__first .
H10:   1 <= rr_type__linelengthindex__last .
H11:   zlength >= rr_type__linelengthindex__first .
H12:   zlength <= rr_type__linelengthindex__last .
H13:   1 <= zlength .
H14:   begidx__1 <= endidx__1 .
H15:   begidx__1 <= zlength .
H16:   endidx__1 <= zlength .
H17:   (foundtype__1 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__1) and (i_ <= endidx__1)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H18:   begidx__1 >= rr_type__linelengthindex__first .
H19:   begidx__1 <= rr_type__linelengthindex__last .
H20:   endidx__1 >= rr_type__linelengthindex__first .
H21:   endidx__1 <= rr_type__linelengthindex__last .
H22:   foundtype__1 >= rr_type__rritemtype__first .
H23:   foundtype__1 <= rr_type__rritemtype__last .
H24:   foundtype__1 >= rr_type__rritemtype__first .
H25:   foundtype__1 <= rr_type__rritemtype__last .
H26:   endidx__1 >= rr_type__linelengthindex__first .
H27:   endidx__1 <= rr_type__linelengthindex__last .
H28:   begidx__1 >= rr_type__linelengthindex__first .
H29:   begidx__1 <= rr_type__linelengthindex__last .
H30:   foundtype__1 >= rr_type__rritemtype__first .
H31:   foundtype__1 <= rr_type__rritemtype__last .
H32:   foundtype__1 = rr_type__control .
H33:   begidx__1 >= rr_type__linelengthindex__first .
H34:   begidx__1 <= rr_type__linelengthindex__last .
H35:   endidx__1 >= rr_type__linelengthindex__first .
H36:   endidx__1 <= rr_type__linelengthindex__last .
H37:   endidx__1 - 6 >= integer__base__first .
H38:   endidx__1 - 6 <= integer__base__last .
H39:   begidx__1 <= endidx__1 - 6 .
H40:   begidx__1 >= rr_type__linelengthindex__first .
H41:   begidx__1 <= rr_type__linelengthindex__last .
H42:   begidx__1 + 6 >= rr_type__linelengthindex__first .
H43:   begidx__1 + 6 <= rr_type__linelengthindex__last .
H44:   begidx__1 + 6 >= integer__base__first .
H45:   begidx__1 + 6 <= integer__base__last .
H46:   begidx__1 + 5 >= rr_type__linelengthindex__first .
H47:   begidx__1 + 5 <= rr_type__linelengthindex__last .
H48:   begidx__1 + 5 >= integer__base__first .
H49:   begidx__1 + 5 <= integer__base__last .
H50:   begidx__1 + 4 >= rr_type__linelengthindex__first .
H51:   begidx__1 + 4 <= rr_type__linelengthindex__last .
H52:   begidx__1 + 4 >= integer__base__first .
H53:   begidx__1 + 4 <= integer__base__last .
H54:   begidx__1 + 3 >= rr_type__linelengthindex__first .
H55:   begidx__1 + 3 <= rr_type__linelengthindex__last .
H56:   begidx__1 + 3 >= integer__base__first .
H57:   begidx__1 + 3 <= integer__base__last .
H58:   begidx__1 + 2 >= rr_type__linelengthindex__first .
H59:   begidx__1 + 2 <= rr_type__linelengthindex__last .
H60:   begidx__1 + 2 >= integer__base__first .
H61:   begidx__1 + 2 <= integer__base__last .
H62:   begidx__1 + 1 >= rr_type__linelengthindex__first .
H63:   begidx__1 + 1 <= rr_type__linelengthindex__last .
H64:   begidx__1 + 1 >= integer__base__first .
H65:   begidx__1 + 1 <= integer__base__last .
H66:   element(zonefileline, [begidx__1 + 1]) = 79 .
H67:   element(zonefileline, [begidx__1 + 2]) = 82 .
H68:   element(zonefileline, [begidx__1 + 3]) = 73 .
H69:   element(zonefileline, [begidx__1 + 4]) = 71 .
H70:   element(zonefileline, [begidx__1 + 5]) = 73 .
H71:   element(zonefileline, [begidx__1 + 6]) = 78 .
H72:   begidx__1 >= rr_type__linelengthindex__first .
H73:   begidx__1 <= rr_type__linelengthindex__last .
H74:   endidx__1 >= rr_type__linelengthindex__first .
H75:   endidx__1 <= rr_type__linelengthindex__last .
H76:   not ((begidx__1 < zlength) and (endidx__1 < zlength)) .
H77:   foundtype__1 >= rr_type__rritemtype__first .
H78:   foundtype__1 <= rr_type__rritemtype__last .
H79:   not (foundtype__1 <> rr_type__domainnameortimespec) .
H80:   endidx__1 >= rr_type__linelengthindex__first .
H81:   endidx__1 <= rr_type__linelengthindex__last .
H82:   endidx__1 >= rr_type__linelengthindex__first .
H83:   endidx__1 <= rr_type__linelengthindex__last .
H84:   not (element(zonefileline, [endidx__1]) <> 46) .
H85:   begidx__1 >= rr_type__linelengthindex__first .
H86:   begidx__1 <= rr_type__linelengthindex__last .
H87:   endidx__1 >= rr_type__linelengthindex__first .
H88:   endidx__1 <= rr_type__linelengthindex__last .
H89:   endidx__1 >= integer__first .
H90:   endidx__1 <= integer__last .
H91:   begidx__1 >= integer__first .
H92:   begidx__1 <= integer__last .
H93:   (begidx__1 <= endidx__1) -> ((endidx__1 >= integer__first) and (
           endidx__1 <= integer__last)) .
H94:   (begidx__1 <= endidx__1) -> ((begidx__1 >= integer__first) and (
           begidx__1 <= integer__last)) .
H95:   begidx__1 >= rr_type__linelengthindex__first .
H96:   begidx__1 <= rr_type__linelengthindex__last .
H97:   endidx__1 >= rr_type__linelengthindex__first .
H98:   endidx__1 <= rr_type__linelengthindex__last .
H99:   not (begidx__1 <= endidx__1) .
H100:  65 >= character__first .
H101:  65 <= character__last .
H102:  1 >= rr_type__linelengthindex__first .
H103:  1 <= rr_type__linelengthindex__last .
H104:  for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(update(
           mk__string(32), [1], 65), [i___1]) >= character__first) and (element(update(
           mk__string(32), [1], 65), [i___1]) <= character__last))) .
        ->
C1:    rr_type__maxlinelength >= rr_type__linelengthindex__first .
C2:    rr_type__maxlinelength <= rr_type__linelengthindex__last .
 

For path(s) from assertion of line 649 to run-time check associated with statement of line 655:

procedure_parsecontrolline_23.
H1:    begidx >= 1 .
H2:    begidx <= endidx .
H3:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           neworigin, [i___1]) >= character__first) and (element(
           neworigin, [i___1]) <= character__last))) .
H4:    newttl >= unsigned_types__unsigned32__first .
H5:    newttl <= unsigned_types__unsigned32__last .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H7:    zlength >= rr_type__linelengthindex__first .
H8:    zlength <= rr_type__linelengthindex__last .
H9:    loop__1__i >= integer__first .
H10:   loop__1__i <= integer__last .
H11:   loop__1__i >= begidx .
H12:   loop__1__i <= endidx__entry__loop__1 .
H13:   endidx__entry__loop__1 >= rr_type__linelengthindex__first .
H14:   endidx__entry__loop__1 <= rr_type__linelengthindex__last .
H15:   element(zonefileline, [loop__1__i]) >= character__first .
H16:   element(zonefileline, [loop__1__i]) <= character__last .
H17:   loop__1__i >= rr_type__linelengthindex__first .
H18:   loop__1__i <= rr_type__linelengthindex__last .
H19:   loop__1__i >= rr_type__linelengthindex__first .
H20:   loop__1__i <= rr_type__linelengthindex__last .
H21:   loop__1__i = endidx__entry__loop__1 .
H22:   65 >= character__first .
H23:   65 <= character__last .
H24:   1 >= rr_type__linelengthindex__first .
H25:   1 <= rr_type__linelengthindex__last .
H26:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(update(update(
           tmpline, [loop__1__i], element(zonefileline, [
           loop__1__i])), [1], 65), [i___1]) >= character__first) and (element(update(update(
           tmpline, [loop__1__i], element(zonefileline, [
           loop__1__i])), [1], 65), [i___1]) <= character__last))) .
        ->
C1:    rr_type__maxlinelength >= rr_type__linelengthindex__first .
C2:    rr_type__maxlinelength <= rr_type__linelengthindex__last .
 

For path(s) from start to run-time check associated with statement of line 660:

procedure_parsecontrolline_24.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           neworigin, [i___1]) >= character__first) and (element(
           neworigin, [i___1]) <= character__last))) .
H2:    newttl >= unsigned_types__unsigned32__first .
H3:    newttl <= unsigned_types__unsigned32__last .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H5:    zlength >= rr_type__linelengthindex__first .
H6:    zlength <= rr_type__linelengthindex__last .
H7:    1 >= rr_type__linelengthindex__first .
H8:    1 <= rr_type__linelengthindex__last .
H9:    1 >= rr_type__linelengthindex__first .
H10:   1 <= rr_type__linelengthindex__last .
H11:   zlength >= rr_type__linelengthindex__first .
H12:   zlength <= rr_type__linelengthindex__last .
H13:   1 <= zlength .
H14:   begidx__1 <= endidx__1 .
H15:   begidx__1 <= zlength .
H16:   endidx__1 <= zlength .
H17:   (foundtype__1 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__1) and (i_ <= endidx__1)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H18:   begidx__1 >= rr_type__linelengthindex__first .
H19:   begidx__1 <= rr_type__linelengthindex__last .
H20:   endidx__1 >= rr_type__linelengthindex__first .
H21:   endidx__1 <= rr_type__linelengthindex__last .
H22:   foundtype__1 >= rr_type__rritemtype__first .
H23:   foundtype__1 <= rr_type__rritemtype__last .
H24:   foundtype__1 >= rr_type__rritemtype__first .
H25:   foundtype__1 <= rr_type__rritemtype__last .
H26:   endidx__1 >= rr_type__linelengthindex__first .
H27:   endidx__1 <= rr_type__linelengthindex__last .
H28:   begidx__1 >= rr_type__linelengthindex__first .
H29:   begidx__1 <= rr_type__linelengthindex__last .
H30:   foundtype__1 >= rr_type__rritemtype__first .
H31:   foundtype__1 <= rr_type__rritemtype__last .
H32:   foundtype__1 = rr_type__control .
H33:   begidx__1 >= rr_type__linelengthindex__first .
H34:   begidx__1 <= rr_type__linelengthindex__last .
H35:   endidx__1 >= rr_type__linelengthindex__first .
H36:   endidx__1 <= rr_type__linelengthindex__last .
H37:   endidx__1 - 6 >= integer__base__first .
H38:   endidx__1 - 6 <= integer__base__last .
H39:   not (begidx__1 <= endidx__1 - 6) .
H40:   begidx__1 >= rr_type__linelengthindex__first .
H41:   begidx__1 <= rr_type__linelengthindex__last .
H42:   endidx__1 >= rr_type__linelengthindex__first .
H43:   endidx__1 <= rr_type__linelengthindex__last .
        ->
C1:    endidx__1 - 3 >= integer__base__first .
C2:    endidx__1 - 3 <= integer__base__last .
 

For path(s) from start to run-time check associated with statement of line 661:

procedure_parsecontrolline_25.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           neworigin, [i___1]) >= character__first) and (element(
           neworigin, [i___1]) <= character__last))) .
H2:    newttl >= unsigned_types__unsigned32__first .
H3:    newttl <= unsigned_types__unsigned32__last .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H5:    zlength >= rr_type__linelengthindex__first .
H6:    zlength <= rr_type__linelengthindex__last .
H7:    1 >= rr_type__linelengthindex__first .
H8:    1 <= rr_type__linelengthindex__last .
H9:    1 >= rr_type__linelengthindex__first .
H10:   1 <= rr_type__linelengthindex__last .
H11:   zlength >= rr_type__linelengthindex__first .
H12:   zlength <= rr_type__linelengthindex__last .
H13:   1 <= zlength .
H14:   begidx__1 <= endidx__1 .
H15:   begidx__1 <= zlength .
H16:   endidx__1 <= zlength .
H17:   (foundtype__1 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__1) and (i_ <= endidx__1)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H18:   begidx__1 >= rr_type__linelengthindex__first .
H19:   begidx__1 <= rr_type__linelengthindex__last .
H20:   endidx__1 >= rr_type__linelengthindex__first .
H21:   endidx__1 <= rr_type__linelengthindex__last .
H22:   foundtype__1 >= rr_type__rritemtype__first .
H23:   foundtype__1 <= rr_type__rritemtype__last .
H24:   foundtype__1 >= rr_type__rritemtype__first .
H25:   foundtype__1 <= rr_type__rritemtype__last .
H26:   endidx__1 >= rr_type__linelengthindex__first .
H27:   endidx__1 <= rr_type__linelengthindex__last .
H28:   begidx__1 >= rr_type__linelengthindex__first .
H29:   begidx__1 <= rr_type__linelengthindex__last .
H30:   foundtype__1 >= rr_type__rritemtype__first .
H31:   foundtype__1 <= rr_type__rritemtype__last .
H32:   foundtype__1 = rr_type__control .
H33:   begidx__1 >= rr_type__linelengthindex__first .
H34:   begidx__1 <= rr_type__linelengthindex__last .
H35:   endidx__1 >= rr_type__linelengthindex__first .
H36:   endidx__1 <= rr_type__linelengthindex__last .
H37:   endidx__1 - 6 >= integer__base__first .
H38:   endidx__1 - 6 <= integer__base__last .
H39:   not (begidx__1 <= endidx__1 - 6) .
H40:   begidx__1 >= rr_type__linelengthindex__first .
H41:   begidx__1 <= rr_type__linelengthindex__last .
H42:   endidx__1 >= rr_type__linelengthindex__first .
H43:   endidx__1 <= rr_type__linelengthindex__last .
H44:   endidx__1 - 3 >= integer__base__first .
H45:   endidx__1 - 3 <= integer__base__last .
H46:   begidx__1 <= endidx__1 - 3 .
H47:   begidx__1 >= rr_type__linelengthindex__first .
H48:   begidx__1 <= rr_type__linelengthindex__last .
        ->
C1:    begidx__1 + 3 >= rr_type__linelengthindex__first .
C2:    begidx__1 + 3 <= rr_type__linelengthindex__last .
C3:    begidx__1 + 3 >= integer__base__first .
C4:    begidx__1 + 3 <= integer__base__last .
C5:    begidx__1 + 2 >= rr_type__linelengthindex__first .
C6:    begidx__1 + 2 <= rr_type__linelengthindex__last .
C7:    begidx__1 + 2 >= integer__base__first .
C8:    begidx__1 + 2 <= integer__base__last .
C9:    begidx__1 + 1 >= rr_type__linelengthindex__first .
C10:   begidx__1 + 1 <= rr_type__linelengthindex__last .
C11:   begidx__1 + 1 >= integer__base__first .
C12:   begidx__1 + 1 <= integer__base__last .
 

For path(s) from start to run-time check associated with statement of line 665:

procedure_parsecontrolline_26.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           neworigin, [i___1]) >= character__first) and (element(
           neworigin, [i___1]) <= character__last))) .
H2:    newttl >= unsigned_types__unsigned32__first .
H3:    newttl <= unsigned_types__unsigned32__last .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H5:    zlength >= rr_type__linelengthindex__first .
H6:    zlength <= rr_type__linelengthindex__last .
H7:    1 >= rr_type__linelengthindex__first .
H8:    1 <= rr_type__linelengthindex__last .
H9:    1 >= rr_type__linelengthindex__first .
H10:   1 <= rr_type__linelengthindex__last .
H11:   zlength >= rr_type__linelengthindex__first .
H12:   zlength <= rr_type__linelengthindex__last .
H13:   1 <= zlength .
H14:   begidx__1 <= endidx__1 .
H15:   begidx__1 <= zlength .
H16:   endidx__1 <= zlength .
H17:   (foundtype__1 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__1) and (i_ <= endidx__1)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H18:   begidx__1 >= rr_type__linelengthindex__first .
H19:   begidx__1 <= rr_type__linelengthindex__last .
H20:   endidx__1 >= rr_type__linelengthindex__first .
H21:   endidx__1 <= rr_type__linelengthindex__last .
H22:   foundtype__1 >= rr_type__rritemtype__first .
H23:   foundtype__1 <= rr_type__rritemtype__last .
H24:   foundtype__1 >= rr_type__rritemtype__first .
H25:   foundtype__1 <= rr_type__rritemtype__last .
H26:   endidx__1 >= rr_type__linelengthindex__first .
H27:   endidx__1 <= rr_type__linelengthindex__last .
H28:   begidx__1 >= rr_type__linelengthindex__first .
H29:   begidx__1 <= rr_type__linelengthindex__last .
H30:   foundtype__1 >= rr_type__rritemtype__first .
H31:   foundtype__1 <= rr_type__rritemtype__last .
H32:   foundtype__1 = rr_type__control .
H33:   begidx__1 >= rr_type__linelengthindex__first .
H34:   begidx__1 <= rr_type__linelengthindex__last .
H35:   endidx__1 >= rr_type__linelengthindex__first .
H36:   endidx__1 <= rr_type__linelengthindex__last .
H37:   endidx__1 - 6 >= integer__base__first .
H38:   endidx__1 - 6 <= integer__base__last .
H39:   not (begidx__1 <= endidx__1 - 6) .
H40:   begidx__1 >= rr_type__linelengthindex__first .
H41:   begidx__1 <= rr_type__linelengthindex__last .
H42:   endidx__1 >= rr_type__linelengthindex__first .
H43:   endidx__1 <= rr_type__linelengthindex__last .
H44:   endidx__1 - 3 >= integer__base__first .
H45:   endidx__1 - 3 <= integer__base__last .
H46:   begidx__1 <= endidx__1 - 3 .
H47:   begidx__1 >= rr_type__linelengthindex__first .
H48:   begidx__1 <= rr_type__linelengthindex__last .
H49:   begidx__1 + 3 >= rr_type__linelengthindex__first .
H50:   begidx__1 + 3 <= rr_type__linelengthindex__last .
H51:   begidx__1 + 3 >= integer__base__first .
H52:   begidx__1 + 3 <= integer__base__last .
H53:   begidx__1 + 2 >= rr_type__linelengthindex__first .
H54:   begidx__1 + 2 <= rr_type__linelengthindex__last .
H55:   begidx__1 + 2 >= integer__base__first .
H56:   begidx__1 + 2 <= integer__base__last .
H57:   begidx__1 + 1 >= rr_type__linelengthindex__first .
H58:   begidx__1 + 1 <= rr_type__linelengthindex__last .
H59:   begidx__1 + 1 >= integer__base__first .
H60:   begidx__1 + 1 <= integer__base__last .
H61:   element(zonefileline, [begidx__1 + 1]) = 84 .
H62:   element(zonefileline, [begidx__1 + 2]) = 84 .
H63:   element(zonefileline, [begidx__1 + 3]) = 76 .
H64:   begidx__1 >= rr_type__linelengthindex__first .
H65:   begidx__1 <= rr_type__linelengthindex__last .
H66:   endidx__1 >= rr_type__linelengthindex__first .
H67:   endidx__1 <= rr_type__linelengthindex__last .
H68:   begidx__1 < zlength .
H69:   endidx__1 < zlength .
H70:   endidx__1 >= rr_type__linelengthindex__first .
H71:   endidx__1 <= rr_type__linelengthindex__last .
        ->
C1:    endidx__1 + 1 >= rr_type__linelengthindex__first .
C2:    endidx__1 + 1 <= rr_type__linelengthindex__last .
 

For path(s) from start to precondition check associated with statement of line 666:

procedure_parsecontrolline_27.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           neworigin, [i___1]) >= character__first) and (element(
           neworigin, [i___1]) <= character__last))) .
H2:    newttl >= unsigned_types__unsigned32__first .
H3:    newttl <= unsigned_types__unsigned32__last .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H5:    zlength >= rr_type__linelengthindex__first .
H6:    zlength <= rr_type__linelengthindex__last .
H7:    1 >= rr_type__linelengthindex__first .
H8:    1 <= rr_type__linelengthindex__last .
H9:    1 >= rr_type__linelengthindex__first .
H10:   1 <= rr_type__linelengthindex__last .
H11:   zlength >= rr_type__linelengthindex__first .
H12:   zlength <= rr_type__linelengthindex__last .
H13:   1 <= zlength .
H14:   begidx__1 <= endidx__1 .
H15:   begidx__1 <= zlength .
H16:   endidx__1 <= zlength .
H17:   (foundtype__1 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__1) and (i_ <= endidx__1)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H18:   begidx__1 >= rr_type__linelengthindex__first .
H19:   begidx__1 <= rr_type__linelengthindex__last .
H20:   endidx__1 >= rr_type__linelengthindex__first .
H21:   endidx__1 <= rr_type__linelengthindex__last .
H22:   foundtype__1 >= rr_type__rritemtype__first .
H23:   foundtype__1 <= rr_type__rritemtype__last .
H24:   foundtype__1 >= rr_type__rritemtype__first .
H25:   foundtype__1 <= rr_type__rritemtype__last .
H26:   endidx__1 >= rr_type__linelengthindex__first .
H27:   endidx__1 <= rr_type__linelengthindex__last .
H28:   begidx__1 >= rr_type__linelengthindex__first .
H29:   begidx__1 <= rr_type__linelengthindex__last .
H30:   foundtype__1 >= rr_type__rritemtype__first .
H31:   foundtype__1 <= rr_type__rritemtype__last .
H32:   foundtype__1 = rr_type__control .
H33:   begidx__1 >= rr_type__linelengthindex__first .
H34:   begidx__1 <= rr_type__linelengthindex__last .
H35:   endidx__1 >= rr_type__linelengthindex__first .
H36:   endidx__1 <= rr_type__linelengthindex__last .
H37:   endidx__1 - 6 >= integer__base__first .
H38:   endidx__1 - 6 <= integer__base__last .
H39:   not (begidx__1 <= endidx__1 - 6) .
H40:   begidx__1 >= rr_type__linelengthindex__first .
H41:   begidx__1 <= rr_type__linelengthindex__last .
H42:   endidx__1 >= rr_type__linelengthindex__first .
H43:   endidx__1 <= rr_type__linelengthindex__last .
H44:   endidx__1 - 3 >= integer__base__first .
H45:   endidx__1 - 3 <= integer__base__last .
H46:   begidx__1 <= endidx__1 - 3 .
H47:   begidx__1 >= rr_type__linelengthindex__first .
H48:   begidx__1 <= rr_type__linelengthindex__last .
H49:   begidx__1 + 3 >= rr_type__linelengthindex__first .
H50:   begidx__1 + 3 <= rr_type__linelengthindex__last .
H51:   begidx__1 + 3 >= integer__base__first .
H52:   begidx__1 + 3 <= integer__base__last .
H53:   begidx__1 + 2 >= rr_type__linelengthindex__first .
H54:   begidx__1 + 2 <= rr_type__linelengthindex__last .
H55:   begidx__1 + 2 >= integer__base__first .
H56:   begidx__1 + 2 <= integer__base__last .
H57:   begidx__1 + 1 >= rr_type__linelengthindex__first .
H58:   begidx__1 + 1 <= rr_type__linelengthindex__last .
H59:   begidx__1 + 1 >= integer__base__first .
H60:   begidx__1 + 1 <= integer__base__last .
H61:   element(zonefileline, [begidx__1 + 1]) = 84 .
H62:   element(zonefileline, [begidx__1 + 2]) = 84 .
H63:   element(zonefileline, [begidx__1 + 3]) = 76 .
H64:   begidx__1 >= rr_type__linelengthindex__first .
H65:   begidx__1 <= rr_type__linelengthindex__last .
H66:   endidx__1 >= rr_type__linelengthindex__first .
H67:   endidx__1 <= rr_type__linelengthindex__last .
H68:   begidx__1 < zlength .
H69:   endidx__1 < zlength .
H70:   endidx__1 >= rr_type__linelengthindex__first .
H71:   endidx__1 <= rr_type__linelengthindex__last .
H72:   endidx__1 + 1 >= rr_type__linelengthindex__first .
H73:   endidx__1 + 1 <= rr_type__linelengthindex__last .
H74:   endidx__1 + 1 >= rr_type__linelengthindex__first .
H75:   endidx__1 + 1 <= rr_type__linelengthindex__last .
        ->
C1:    endidx__1 + 1 >= rr_type__linelengthindex__first .
C2:    endidx__1 + 1 <= rr_type__linelengthindex__last .
C3:    zlength >= rr_type__linelengthindex__first .
C4:    zlength <= rr_type__linelengthindex__last .
C5:    endidx__1 + 1 <= zlength .
 

For path(s) from start to run-time check associated with statement of line 666:

procedure_parsecontrolline_28.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           neworigin, [i___1]) >= character__first) and (element(
           neworigin, [i___1]) <= character__last))) .
H2:    newttl >= unsigned_types__unsigned32__first .
H3:    newttl <= unsigned_types__unsigned32__last .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H5:    zlength >= rr_type__linelengthindex__first .
H6:    zlength <= rr_type__linelengthindex__last .
H7:    1 >= rr_type__linelengthindex__first .
H8:    1 <= rr_type__linelengthindex__last .
H9:    1 >= rr_type__linelengthindex__first .
H10:   1 <= rr_type__linelengthindex__last .
H11:   zlength >= rr_type__linelengthindex__first .
H12:   zlength <= rr_type__linelengthindex__last .
H13:   1 <= zlength .
H14:   begidx__1 <= endidx__1 .
H15:   begidx__1 <= zlength .
H16:   endidx__1 <= zlength .
H17:   (foundtype__1 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__1) and (i_ <= endidx__1)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H18:   begidx__1 >= rr_type__linelengthindex__first .
H19:   begidx__1 <= rr_type__linelengthindex__last .
H20:   endidx__1 >= rr_type__linelengthindex__first .
H21:   endidx__1 <= rr_type__linelengthindex__last .
H22:   foundtype__1 >= rr_type__rritemtype__first .
H23:   foundtype__1 <= rr_type__rritemtype__last .
H24:   foundtype__1 >= rr_type__rritemtype__first .
H25:   foundtype__1 <= rr_type__rritemtype__last .
H26:   endidx__1 >= rr_type__linelengthindex__first .
H27:   endidx__1 <= rr_type__linelengthindex__last .
H28:   begidx__1 >= rr_type__linelengthindex__first .
H29:   begidx__1 <= rr_type__linelengthindex__last .
H30:   foundtype__1 >= rr_type__rritemtype__first .
H31:   foundtype__1 <= rr_type__rritemtype__last .
H32:   foundtype__1 = rr_type__control .
H33:   begidx__1 >= rr_type__linelengthindex__first .
H34:   begidx__1 <= rr_type__linelengthindex__last .
H35:   endidx__1 >= rr_type__linelengthindex__first .
H36:   endidx__1 <= rr_type__linelengthindex__last .
H37:   endidx__1 - 6 >= integer__base__first .
H38:   endidx__1 - 6 <= integer__base__last .
H39:   not (begidx__1 <= endidx__1 - 6) .
H40:   begidx__1 >= rr_type__linelengthindex__first .
H41:   begidx__1 <= rr_type__linelengthindex__last .
H42:   endidx__1 >= rr_type__linelengthindex__first .
H43:   endidx__1 <= rr_type__linelengthindex__last .
H44:   endidx__1 - 3 >= integer__base__first .
H45:   endidx__1 - 3 <= integer__base__last .
H46:   begidx__1 <= endidx__1 - 3 .
H47:   begidx__1 >= rr_type__linelengthindex__first .
H48:   begidx__1 <= rr_type__linelengthindex__last .
H49:   begidx__1 + 3 >= rr_type__linelengthindex__first .
H50:   begidx__1 + 3 <= rr_type__linelengthindex__last .
H51:   begidx__1 + 3 >= integer__base__first .
H52:   begidx__1 + 3 <= integer__base__last .
H53:   begidx__1 + 2 >= rr_type__linelengthindex__first .
H54:   begidx__1 + 2 <= rr_type__linelengthindex__last .
H55:   begidx__1 + 2 >= integer__base__first .
H56:   begidx__1 + 2 <= integer__base__last .
H57:   begidx__1 + 1 >= rr_type__linelengthindex__first .
H58:   begidx__1 + 1 <= rr_type__linelengthindex__last .
H59:   begidx__1 + 1 >= integer__base__first .
H60:   begidx__1 + 1 <= integer__base__last .
H61:   element(zonefileline, [begidx__1 + 1]) = 84 .
H62:   element(zonefileline, [begidx__1 + 2]) = 84 .
H63:   element(zonefileline, [begidx__1 + 3]) = 76 .
H64:   begidx__1 >= rr_type__linelengthindex__first .
H65:   begidx__1 <= rr_type__linelengthindex__last .
H66:   endidx__1 >= rr_type__linelengthindex__first .
H67:   endidx__1 <= rr_type__linelengthindex__last .
H68:   begidx__1 < zlength .
H69:   endidx__1 < zlength .
H70:   endidx__1 >= rr_type__linelengthindex__first .
H71:   endidx__1 <= rr_type__linelengthindex__last .
H72:   endidx__1 + 1 >= rr_type__linelengthindex__first .
H73:   endidx__1 + 1 <= rr_type__linelengthindex__last .
H74:   endidx__1 + 1 >= rr_type__linelengthindex__first .
H75:   endidx__1 + 1 <= rr_type__linelengthindex__last .
H76:   endidx__1 + 1 >= rr_type__linelengthindex__first .
H77:   endidx__1 + 1 <= rr_type__linelengthindex__last .
H78:   zlength >= rr_type__linelengthindex__first .
H79:   zlength <= rr_type__linelengthindex__last .
H80:   endidx__1 + 1 <= zlength .
H81:   begidx__4 <= endidx__4 .
H82:   begidx__4 <= zlength .
H83:   endidx__4 <= zlength .
H84:   (foundtype__4 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__4) and (i_ <= endidx__4)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H85:   begidx__4 >= rr_type__linelengthindex__first .
H86:   begidx__4 <= rr_type__linelengthindex__last .
H87:   endidx__4 >= rr_type__linelengthindex__first .
H88:   endidx__4 <= rr_type__linelengthindex__last .
H89:   foundtype__4 >= rr_type__rritemtype__first .
H90:   foundtype__4 <= rr_type__rritemtype__last .
        ->
C1:    foundtype__4 >= rr_type__rritemtype__first .
C2:    foundtype__4 <= rr_type__rritemtype__last .
C3:    endidx__4 >= rr_type__linelengthindex__first .
C4:    endidx__4 <= rr_type__linelengthindex__last .
C5:    begidx__4 >= rr_type__linelengthindex__first .
C6:    begidx__4 <= rr_type__linelengthindex__last .
 

For path(s) from start to run-time check associated with statement of line 673:

procedure_parsecontrolline_29.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           neworigin, [i___1]) >= character__first) and (element(
           neworigin, [i___1]) <= character__last))) .
H2:    newttl >= unsigned_types__unsigned32__first .
H3:    newttl <= unsigned_types__unsigned32__last .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H5:    zlength >= rr_type__linelengthindex__first .
H6:    zlength <= rr_type__linelengthindex__last .
H7:    1 >= rr_type__linelengthindex__first .
H8:    1 <= rr_type__linelengthindex__last .
H9:    1 >= rr_type__linelengthindex__first .
H10:   1 <= rr_type__linelengthindex__last .
H11:   zlength >= rr_type__linelengthindex__first .
H12:   zlength <= rr_type__linelengthindex__last .
H13:   1 <= zlength .
H14:   begidx__1 <= endidx__1 .
H15:   begidx__1 <= zlength .
H16:   endidx__1 <= zlength .
H17:   (foundtype__1 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__1) and (i_ <= endidx__1)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H18:   begidx__1 >= rr_type__linelengthindex__first .
H19:   begidx__1 <= rr_type__linelengthindex__last .
H20:   endidx__1 >= rr_type__linelengthindex__first .
H21:   endidx__1 <= rr_type__linelengthindex__last .
H22:   foundtype__1 >= rr_type__rritemtype__first .
H23:   foundtype__1 <= rr_type__rritemtype__last .
H24:   foundtype__1 >= rr_type__rritemtype__first .
H25:   foundtype__1 <= rr_type__rritemtype__last .
H26:   endidx__1 >= rr_type__linelengthindex__first .
H27:   endidx__1 <= rr_type__linelengthindex__last .
H28:   begidx__1 >= rr_type__linelengthindex__first .
H29:   begidx__1 <= rr_type__linelengthindex__last .
H30:   foundtype__1 >= rr_type__rritemtype__first .
H31:   foundtype__1 <= rr_type__rritemtype__last .
H32:   foundtype__1 = rr_type__control .
H33:   begidx__1 >= rr_type__linelengthindex__first .
H34:   begidx__1 <= rr_type__linelengthindex__last .
H35:   endidx__1 >= rr_type__linelengthindex__first .
H36:   endidx__1 <= rr_type__linelengthindex__last .
H37:   endidx__1 - 6 >= integer__base__first .
H38:   endidx__1 - 6 <= integer__base__last .
H39:   not (begidx__1 <= endidx__1 - 6) .
H40:   begidx__1 >= rr_type__linelengthindex__first .
H41:   begidx__1 <= rr_type__linelengthindex__last .
H42:   endidx__1 >= rr_type__linelengthindex__first .
H43:   endidx__1 <= rr_type__linelengthindex__last .
H44:   endidx__1 - 3 >= integer__base__first .
H45:   endidx__1 - 3 <= integer__base__last .
H46:   begidx__1 <= endidx__1 - 3 .
H47:   begidx__1 >= rr_type__linelengthindex__first .
H48:   begidx__1 <= rr_type__linelengthindex__last .
H49:   begidx__1 + 3 >= rr_type__linelengthindex__first .
H50:   begidx__1 + 3 <= rr_type__linelengthindex__last .
H51:   begidx__1 + 3 >= integer__base__first .
H52:   begidx__1 + 3 <= integer__base__last .
H53:   begidx__1 + 2 >= rr_type__linelengthindex__first .
H54:   begidx__1 + 2 <= rr_type__linelengthindex__last .
H55:   begidx__1 + 2 >= integer__base__first .
H56:   begidx__1 + 2 <= integer__base__last .
H57:   begidx__1 + 1 >= rr_type__linelengthindex__first .
H58:   begidx__1 + 1 <= rr_type__linelengthindex__last .
H59:   begidx__1 + 1 >= integer__base__first .
H60:   begidx__1 + 1 <= integer__base__last .
H61:   element(zonefileline, [begidx__1 + 1]) = 84 .
H62:   element(zonefileline, [begidx__1 + 2]) = 84 .
H63:   element(zonefileline, [begidx__1 + 3]) = 76 .
H64:   begidx__1 >= rr_type__linelengthindex__first .
H65:   begidx__1 <= rr_type__linelengthindex__last .
H66:   endidx__1 >= rr_type__linelengthindex__first .
H67:   endidx__1 <= rr_type__linelengthindex__last .
H68:   begidx__1 < zlength .
H69:   endidx__1 < zlength .
H70:   endidx__1 >= rr_type__linelengthindex__first .
H71:   endidx__1 <= rr_type__linelengthindex__last .
H72:   endidx__1 + 1 >= rr_type__linelengthindex__first .
H73:   endidx__1 + 1 <= rr_type__linelengthindex__last .
H74:   endidx__1 + 1 >= rr_type__linelengthindex__first .
H75:   endidx__1 + 1 <= rr_type__linelengthindex__last .
H76:   endidx__1 + 1 >= rr_type__linelengthindex__first .
H77:   endidx__1 + 1 <= rr_type__linelengthindex__last .
H78:   zlength >= rr_type__linelengthindex__first .
H79:   zlength <= rr_type__linelengthindex__last .
H80:   endidx__1 + 1 <= zlength .
H81:   begidx__4 <= endidx__4 .
H82:   begidx__4 <= zlength .
H83:   endidx__4 <= zlength .
H84:   (foundtype__4 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__4) and (i_ <= endidx__4)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H85:   begidx__4 >= rr_type__linelengthindex__first .
H86:   begidx__4 <= rr_type__linelengthindex__last .
H87:   endidx__4 >= rr_type__linelengthindex__first .
H88:   endidx__4 <= rr_type__linelengthindex__last .
H89:   foundtype__4 >= rr_type__rritemtype__first .
H90:   foundtype__4 <= rr_type__rritemtype__last .
H91:   foundtype__4 >= rr_type__rritemtype__first .
H92:   foundtype__4 <= rr_type__rritemtype__last .
H93:   endidx__4 >= rr_type__linelengthindex__first .
H94:   endidx__4 <= rr_type__linelengthindex__last .
H95:   begidx__4 >= rr_type__linelengthindex__first .
H96:   begidx__4 <= rr_type__linelengthindex__last .
H97:   foundtype__4 >= rr_type__rritemtype__first .
H98:   foundtype__4 <= rr_type__rritemtype__last .
H99:   not ((foundtype__4 <> rr_type__domainnameortimespec) and (
           foundtype__4 <> rr_type__number)) .
H100:  begidx__4 >= rr_type__linelengthindex__first .
H101:  begidx__4 <= rr_type__linelengthindex__last .
H102:  endidx__4 >= rr_type__linelengthindex__first .
H103:  endidx__4 <= rr_type__linelengthindex__last .
        ->
C1:    endidx__4 >= integer__first .
C2:    endidx__4 <= integer__last .
C3:    begidx__4 >= integer__first .
C4:    begidx__4 <= integer__last .
 

procedure_parsecontrolline_30.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           neworigin, [i___1]) >= character__first) and (element(
           neworigin, [i___1]) <= character__last))) .
H2:    newttl >= unsigned_types__unsigned32__first .
H3:    newttl <= unsigned_types__unsigned32__last .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H5:    zlength >= rr_type__linelengthindex__first .
H6:    zlength <= rr_type__linelengthindex__last .
H7:    1 >= rr_type__linelengthindex__first .
H8:    1 <= rr_type__linelengthindex__last .
H9:    1 >= rr_type__linelengthindex__first .
H10:   1 <= rr_type__linelengthindex__last .
H11:   zlength >= rr_type__linelengthindex__first .
H12:   zlength <= rr_type__linelengthindex__last .
H13:   1 <= zlength .
H14:   begidx__1 <= endidx__1 .
H15:   begidx__1 <= zlength .
H16:   endidx__1 <= zlength .
H17:   (foundtype__1 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__1) and (i_ <= endidx__1)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H18:   begidx__1 >= rr_type__linelengthindex__first .
H19:   begidx__1 <= rr_type__linelengthindex__last .
H20:   endidx__1 >= rr_type__linelengthindex__first .
H21:   endidx__1 <= rr_type__linelengthindex__last .
H22:   foundtype__1 >= rr_type__rritemtype__first .
H23:   foundtype__1 <= rr_type__rritemtype__last .
H24:   foundtype__1 >= rr_type__rritemtype__first .
H25:   foundtype__1 <= rr_type__rritemtype__last .
H26:   endidx__1 >= rr_type__linelengthindex__first .
H27:   endidx__1 <= rr_type__linelengthindex__last .
H28:   begidx__1 >= rr_type__linelengthindex__first .
H29:   begidx__1 <= rr_type__linelengthindex__last .
H30:   foundtype__1 >= rr_type__rritemtype__first .
H31:   foundtype__1 <= rr_type__rritemtype__last .
H32:   foundtype__1 = rr_type__control .
H33:   begidx__1 >= rr_type__linelengthindex__first .
H34:   begidx__1 <= rr_type__linelengthindex__last .
H35:   endidx__1 >= rr_type__linelengthindex__first .
H36:   endidx__1 <= rr_type__linelengthindex__last .
H37:   endidx__1 - 6 >= integer__base__first .
H38:   endidx__1 - 6 <= integer__base__last .
H39:   not (begidx__1 <= endidx__1 - 6) .
H40:   begidx__1 >= rr_type__linelengthindex__first .
H41:   begidx__1 <= rr_type__linelengthindex__last .
H42:   endidx__1 >= rr_type__linelengthindex__first .
H43:   endidx__1 <= rr_type__linelengthindex__last .
H44:   endidx__1 - 3 >= integer__base__first .
H45:   endidx__1 - 3 <= integer__base__last .
H46:   begidx__1 <= endidx__1 - 3 .
H47:   begidx__1 >= rr_type__linelengthindex__first .
H48:   begidx__1 <= rr_type__linelengthindex__last .
H49:   begidx__1 + 3 >= rr_type__linelengthindex__first .
H50:   begidx__1 + 3 <= rr_type__linelengthindex__last .
H51:   begidx__1 + 3 >= integer__base__first .
H52:   begidx__1 + 3 <= integer__base__last .
H53:   begidx__1 + 2 >= rr_type__linelengthindex__first .
H54:   begidx__1 + 2 <= rr_type__linelengthindex__last .
H55:   begidx__1 + 2 >= integer__base__first .
H56:   begidx__1 + 2 <= integer__base__last .
H57:   begidx__1 + 1 >= rr_type__linelengthindex__first .
H58:   begidx__1 + 1 <= rr_type__linelengthindex__last .
H59:   begidx__1 + 1 >= integer__base__first .
H60:   begidx__1 + 1 <= integer__base__last .
H61:   element(zonefileline, [begidx__1 + 1]) = 84 .
H62:   element(zonefileline, [begidx__1 + 2]) = 84 .
H63:   element(zonefileline, [begidx__1 + 3]) = 76 .
H64:   begidx__1 >= rr_type__linelengthindex__first .
H65:   begidx__1 <= rr_type__linelengthindex__last .
H66:   endidx__1 >= rr_type__linelengthindex__first .
H67:   endidx__1 <= rr_type__linelengthindex__last .
H68:   not ((begidx__1 < zlength) and (endidx__1 < zlength)) .
H69:   foundtype__1 >= rr_type__rritemtype__first .
H70:   foundtype__1 <= rr_type__rritemtype__last .
H71:   not ((foundtype__1 <> rr_type__domainnameortimespec) and (
           foundtype__1 <> rr_type__number)) .
H72:   begidx__1 >= rr_type__linelengthindex__first .
H73:   begidx__1 <= rr_type__linelengthindex__last .
H74:   endidx__1 >= rr_type__linelengthindex__first .
H75:   endidx__1 <= rr_type__linelengthindex__last .
        ->
C1:    endidx__1 >= integer__first .
C2:    endidx__1 <= integer__last .
C3:    begidx__1 >= integer__first .
C4:    begidx__1 <= integer__last .
 

For path(s) from start to run-time check associated with statement of line 673:

procedure_parsecontrolline_31.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           neworigin, [i___1]) >= character__first) and (element(
           neworigin, [i___1]) <= character__last))) .
H2:    newttl >= unsigned_types__unsigned32__first .
H3:    newttl <= unsigned_types__unsigned32__last .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H5:    zlength >= rr_type__linelengthindex__first .
H6:    zlength <= rr_type__linelengthindex__last .
H7:    1 >= rr_type__linelengthindex__first .
H8:    1 <= rr_type__linelengthindex__last .
H9:    1 >= rr_type__linelengthindex__first .
H10:   1 <= rr_type__linelengthindex__last .
H11:   zlength >= rr_type__linelengthindex__first .
H12:   zlength <= rr_type__linelengthindex__last .
H13:   1 <= zlength .
H14:   begidx__1 <= endidx__1 .
H15:   begidx__1 <= zlength .
H16:   endidx__1 <= zlength .
H17:   (foundtype__1 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__1) and (i_ <= endidx__1)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H18:   begidx__1 >= rr_type__linelengthindex__first .
H19:   begidx__1 <= rr_type__linelengthindex__last .
H20:   endidx__1 >= rr_type__linelengthindex__first .
H21:   endidx__1 <= rr_type__linelengthindex__last .
H22:   foundtype__1 >= rr_type__rritemtype__first .
H23:   foundtype__1 <= rr_type__rritemtype__last .
H24:   foundtype__1 >= rr_type__rritemtype__first .
H25:   foundtype__1 <= rr_type__rritemtype__last .
H26:   endidx__1 >= rr_type__linelengthindex__first .
H27:   endidx__1 <= rr_type__linelengthindex__last .
H28:   begidx__1 >= rr_type__linelengthindex__first .
H29:   begidx__1 <= rr_type__linelengthindex__last .
H30:   foundtype__1 >= rr_type__rritemtype__first .
H31:   foundtype__1 <= rr_type__rritemtype__last .
H32:   foundtype__1 = rr_type__control .
H33:   begidx__1 >= rr_type__linelengthindex__first .
H34:   begidx__1 <= rr_type__linelengthindex__last .
H35:   endidx__1 >= rr_type__linelengthindex__first .
H36:   endidx__1 <= rr_type__linelengthindex__last .
H37:   endidx__1 - 6 >= integer__base__first .
H38:   endidx__1 - 6 <= integer__base__last .
H39:   not (begidx__1 <= endidx__1 - 6) .
H40:   begidx__1 >= rr_type__linelengthindex__first .
H41:   begidx__1 <= rr_type__linelengthindex__last .
H42:   endidx__1 >= rr_type__linelengthindex__first .
H43:   endidx__1 <= rr_type__linelengthindex__last .
H44:   endidx__1 - 3 >= integer__base__first .
H45:   endidx__1 - 3 <= integer__base__last .
H46:   begidx__1 <= endidx__1 - 3 .
H47:   begidx__1 >= rr_type__linelengthindex__first .
H48:   begidx__1 <= rr_type__linelengthindex__last .
H49:   begidx__1 + 3 >= rr_type__linelengthindex__first .
H50:   begidx__1 + 3 <= rr_type__linelengthindex__last .
H51:   begidx__1 + 3 >= integer__base__first .
H52:   begidx__1 + 3 <= integer__base__last .
H53:   begidx__1 + 2 >= rr_type__linelengthindex__first .
H54:   begidx__1 + 2 <= rr_type__linelengthindex__last .
H55:   begidx__1 + 2 >= integer__base__first .
H56:   begidx__1 + 2 <= integer__base__last .
H57:   begidx__1 + 1 >= rr_type__linelengthindex__first .
H58:   begidx__1 + 1 <= rr_type__linelengthindex__last .
H59:   begidx__1 + 1 >= integer__base__first .
H60:   begidx__1 + 1 <= integer__base__last .
H61:   element(zonefileline, [begidx__1 + 1]) = 84 .
H62:   element(zonefileline, [begidx__1 + 2]) = 84 .
H63:   element(zonefileline, [begidx__1 + 3]) = 76 .
H64:   begidx__1 >= rr_type__linelengthindex__first .
H65:   begidx__1 <= rr_type__linelengthindex__last .
H66:   endidx__1 >= rr_type__linelengthindex__first .
H67:   endidx__1 <= rr_type__linelengthindex__last .
H68:   begidx__1 < zlength .
H69:   endidx__1 < zlength .
H70:   endidx__1 >= rr_type__linelengthindex__first .
H71:   endidx__1 <= rr_type__linelengthindex__last .
H72:   endidx__1 + 1 >= rr_type__linelengthindex__first .
H73:   endidx__1 + 1 <= rr_type__linelengthindex__last .
H74:   endidx__1 + 1 >= rr_type__linelengthindex__first .
H75:   endidx__1 + 1 <= rr_type__linelengthindex__last .
H76:   endidx__1 + 1 >= rr_type__linelengthindex__first .
H77:   endidx__1 + 1 <= rr_type__linelengthindex__last .
H78:   zlength >= rr_type__linelengthindex__first .
H79:   zlength <= rr_type__linelengthindex__last .
H80:   endidx__1 + 1 <= zlength .
H81:   begidx__4 <= endidx__4 .
H82:   begidx__4 <= zlength .
H83:   endidx__4 <= zlength .
H84:   (foundtype__4 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__4) and (i_ <= endidx__4)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H85:   begidx__4 >= rr_type__linelengthindex__first .
H86:   begidx__4 <= rr_type__linelengthindex__last .
H87:   endidx__4 >= rr_type__linelengthindex__first .
H88:   endidx__4 <= rr_type__linelengthindex__last .
H89:   foundtype__4 >= rr_type__rritemtype__first .
H90:   foundtype__4 <= rr_type__rritemtype__last .
H91:   foundtype__4 >= rr_type__rritemtype__first .
H92:   foundtype__4 <= rr_type__rritemtype__last .
H93:   endidx__4 >= rr_type__linelengthindex__first .
H94:   endidx__4 <= rr_type__linelengthindex__last .
H95:   begidx__4 >= rr_type__linelengthindex__first .
H96:   begidx__4 <= rr_type__linelengthindex__last .
H97:   foundtype__4 >= rr_type__rritemtype__first .
H98:   foundtype__4 <= rr_type__rritemtype__last .
H99:   not ((foundtype__4 <> rr_type__domainnameortimespec) and (
           foundtype__4 <> rr_type__number)) .
H100:  begidx__4 >= rr_type__linelengthindex__first .
H101:  begidx__4 <= rr_type__linelengthindex__last .
H102:  endidx__4 >= rr_type__linelengthindex__first .
H103:  endidx__4 <= rr_type__linelengthindex__last .
H104:  endidx__4 >= integer__first .
H105:  endidx__4 <= integer__last .
H106:  begidx__4 >= integer__first .
H107:  begidx__4 <= integer__last .
        ->
C1:    (begidx__4 <= endidx__4) -> ((endidx__4 >= integer__first) and (
           endidx__4 <= integer__last)) .
C2:    (begidx__4 <= endidx__4) -> ((begidx__4 >= integer__first) and (
           begidx__4 <= integer__last)) .
 

procedure_parsecontrolline_32.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           neworigin, [i___1]) >= character__first) and (element(
           neworigin, [i___1]) <= character__last))) .
H2:    newttl >= unsigned_types__unsigned32__first .
H3:    newttl <= unsigned_types__unsigned32__last .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H5:    zlength >= rr_type__linelengthindex__first .
H6:    zlength <= rr_type__linelengthindex__last .
H7:    1 >= rr_type__linelengthindex__first .
H8:    1 <= rr_type__linelengthindex__last .
H9:    1 >= rr_type__linelengthindex__first .
H10:   1 <= rr_type__linelengthindex__last .
H11:   zlength >= rr_type__linelengthindex__first .
H12:   zlength <= rr_type__linelengthindex__last .
H13:   1 <= zlength .
H14:   begidx__1 <= endidx__1 .
H15:   begidx__1 <= zlength .
H16:   endidx__1 <= zlength .
H17:   (foundtype__1 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__1) and (i_ <= endidx__1)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H18:   begidx__1 >= rr_type__linelengthindex__first .
H19:   begidx__1 <= rr_type__linelengthindex__last .
H20:   endidx__1 >= rr_type__linelengthindex__first .
H21:   endidx__1 <= rr_type__linelengthindex__last .
H22:   foundtype__1 >= rr_type__rritemtype__first .
H23:   foundtype__1 <= rr_type__rritemtype__last .
H24:   foundtype__1 >= rr_type__rritemtype__first .
H25:   foundtype__1 <= rr_type__rritemtype__last .
H26:   endidx__1 >= rr_type__linelengthindex__first .
H27:   endidx__1 <= rr_type__linelengthindex__last .
H28:   begidx__1 >= rr_type__linelengthindex__first .
H29:   begidx__1 <= rr_type__linelengthindex__last .
H30:   foundtype__1 >= rr_type__rritemtype__first .
H31:   foundtype__1 <= rr_type__rritemtype__last .
H32:   foundtype__1 = rr_type__control .
H33:   begidx__1 >= rr_type__linelengthindex__first .
H34:   begidx__1 <= rr_type__linelengthindex__last .
H35:   endidx__1 >= rr_type__linelengthindex__first .
H36:   endidx__1 <= rr_type__linelengthindex__last .
H37:   endidx__1 - 6 >= integer__base__first .
H38:   endidx__1 - 6 <= integer__base__last .
H39:   not (begidx__1 <= endidx__1 - 6) .
H40:   begidx__1 >= rr_type__linelengthindex__first .
H41:   begidx__1 <= rr_type__linelengthindex__last .
H42:   endidx__1 >= rr_type__linelengthindex__first .
H43:   endidx__1 <= rr_type__linelengthindex__last .
H44:   endidx__1 - 3 >= integer__base__first .
H45:   endidx__1 - 3 <= integer__base__last .
H46:   begidx__1 <= endidx__1 - 3 .
H47:   begidx__1 >= rr_type__linelengthindex__first .
H48:   begidx__1 <= rr_type__linelengthindex__last .
H49:   begidx__1 + 3 >= rr_type__linelengthindex__first .
H50:   begidx__1 + 3 <= rr_type__linelengthindex__last .
H51:   begidx__1 + 3 >= integer__base__first .
H52:   begidx__1 + 3 <= integer__base__last .
H53:   begidx__1 + 2 >= rr_type__linelengthindex__first .
H54:   begidx__1 + 2 <= rr_type__linelengthindex__last .
H55:   begidx__1 + 2 >= integer__base__first .
H56:   begidx__1 + 2 <= integer__base__last .
H57:   begidx__1 + 1 >= rr_type__linelengthindex__first .
H58:   begidx__1 + 1 <= rr_type__linelengthindex__last .
H59:   begidx__1 + 1 >= integer__base__first .
H60:   begidx__1 + 1 <= integer__base__last .
H61:   element(zonefileline, [begidx__1 + 1]) = 84 .
H62:   element(zonefileline, [begidx__1 + 2]) = 84 .
H63:   element(zonefileline, [begidx__1 + 3]) = 76 .
H64:   begidx__1 >= rr_type__linelengthindex__first .
H65:   begidx__1 <= rr_type__linelengthindex__last .
H66:   endidx__1 >= rr_type__linelengthindex__first .
H67:   endidx__1 <= rr_type__linelengthindex__last .
H68:   not ((begidx__1 < zlength) and (endidx__1 < zlength)) .
H69:   foundtype__1 >= rr_type__rritemtype__first .
H70:   foundtype__1 <= rr_type__rritemtype__last .
H71:   not ((foundtype__1 <> rr_type__domainnameortimespec) and (
           foundtype__1 <> rr_type__number)) .
H72:   begidx__1 >= rr_type__linelengthindex__first .
H73:   begidx__1 <= rr_type__linelengthindex__last .
H74:   endidx__1 >= rr_type__linelengthindex__first .
H75:   endidx__1 <= rr_type__linelengthindex__last .
H76:   endidx__1 >= integer__first .
H77:   endidx__1 <= integer__last .
H78:   begidx__1 >= integer__first .
H79:   begidx__1 <= integer__last .
        ->
C1:    (begidx__1 <= endidx__1) -> ((endidx__1 >= integer__first) and (
           endidx__1 <= integer__last)) .
C2:    (begidx__1 <= endidx__1) -> ((begidx__1 >= integer__first) and (
           begidx__1 <= integer__last)) .
 

For path(s) from start to assertion of line 674:

procedure_parsecontrolline_33.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           neworigin, [i___1]) >= character__first) and (element(
           neworigin, [i___1]) <= character__last))) .
H2:    newttl >= unsigned_types__unsigned32__first .
H3:    newttl <= unsigned_types__unsigned32__last .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H5:    zlength >= rr_type__linelengthindex__first .
H6:    zlength <= rr_type__linelengthindex__last .
H7:    1 >= rr_type__linelengthindex__first .
H8:    1 <= rr_type__linelengthindex__last .
H9:    1 >= rr_type__linelengthindex__first .
H10:   1 <= rr_type__linelengthindex__last .
H11:   zlength >= rr_type__linelengthindex__first .
H12:   zlength <= rr_type__linelengthindex__last .
H13:   1 <= zlength .
H14:   begidx__1 <= endidx__1 .
H15:   begidx__1 <= zlength .
H16:   endidx__1 <= zlength .
H17:   (foundtype__1 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__1) and (i_ <= endidx__1)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H18:   begidx__1 >= rr_type__linelengthindex__first .
H19:   begidx__1 <= rr_type__linelengthindex__last .
H20:   endidx__1 >= rr_type__linelengthindex__first .
H21:   endidx__1 <= rr_type__linelengthindex__last .
H22:   foundtype__1 >= rr_type__rritemtype__first .
H23:   foundtype__1 <= rr_type__rritemtype__last .
H24:   foundtype__1 >= rr_type__rritemtype__first .
H25:   foundtype__1 <= rr_type__rritemtype__last .
H26:   endidx__1 >= rr_type__linelengthindex__first .
H27:   endidx__1 <= rr_type__linelengthindex__last .
H28:   begidx__1 >= rr_type__linelengthindex__first .
H29:   begidx__1 <= rr_type__linelengthindex__last .
H30:   foundtype__1 >= rr_type__rritemtype__first .
H31:   foundtype__1 <= rr_type__rritemtype__last .
H32:   foundtype__1 = rr_type__control .
H33:   begidx__1 >= rr_type__linelengthindex__first .
H34:   begidx__1 <= rr_type__linelengthindex__last .
H35:   endidx__1 >= rr_type__linelengthindex__first .
H36:   endidx__1 <= rr_type__linelengthindex__last .
H37:   endidx__1 - 6 >= integer__base__first .
H38:   endidx__1 - 6 <= integer__base__last .
H39:   not (begidx__1 <= endidx__1 - 6) .
H40:   begidx__1 >= rr_type__linelengthindex__first .
H41:   begidx__1 <= rr_type__linelengthindex__last .
H42:   endidx__1 >= rr_type__linelengthindex__first .
H43:   endidx__1 <= rr_type__linelengthindex__last .
H44:   endidx__1 - 3 >= integer__base__first .
H45:   endidx__1 - 3 <= integer__base__last .
H46:   begidx__1 <= endidx__1 - 3 .
H47:   begidx__1 >= rr_type__linelengthindex__first .
H48:   begidx__1 <= rr_type__linelengthindex__last .
H49:   begidx__1 + 3 >= rr_type__linelengthindex__first .
H50:   begidx__1 + 3 <= rr_type__linelengthindex__last .
H51:   begidx__1 + 3 >= integer__base__first .
H52:   begidx__1 + 3 <= integer__base__last .
H53:   begidx__1 + 2 >= rr_type__linelengthindex__first .
H54:   begidx__1 + 2 <= rr_type__linelengthindex__last .
H55:   begidx__1 + 2 >= integer__base__first .
H56:   begidx__1 + 2 <= integer__base__last .
H57:   begidx__1 + 1 >= rr_type__linelengthindex__first .
H58:   begidx__1 + 1 <= rr_type__linelengthindex__last .
H59:   begidx__1 + 1 >= integer__base__first .
H60:   begidx__1 + 1 <= integer__base__last .
H61:   element(zonefileline, [begidx__1 + 1]) = 84 .
H62:   element(zonefileline, [begidx__1 + 2]) = 84 .
H63:   element(zonefileline, [begidx__1 + 3]) = 76 .
H64:   begidx__1 >= rr_type__linelengthindex__first .
H65:   begidx__1 <= rr_type__linelengthindex__last .
H66:   endidx__1 >= rr_type__linelengthindex__first .
H67:   endidx__1 <= rr_type__linelengthindex__last .
H68:   begidx__1 < zlength .
H69:   endidx__1 < zlength .
H70:   endidx__1 >= rr_type__linelengthindex__first .
H71:   endidx__1 <= rr_type__linelengthindex__last .
H72:   endidx__1 + 1 >= rr_type__linelengthindex__first .
H73:   endidx__1 + 1 <= rr_type__linelengthindex__last .
H74:   endidx__1 + 1 >= rr_type__linelengthindex__first .
H75:   endidx__1 + 1 <= rr_type__linelengthindex__last .
H76:   endidx__1 + 1 >= rr_type__linelengthindex__first .
H77:   endidx__1 + 1 <= rr_type__linelengthindex__last .
H78:   zlength >= rr_type__linelengthindex__first .
H79:   zlength <= rr_type__linelengthindex__last .
H80:   endidx__1 + 1 <= zlength .
H81:   begidx__4 <= endidx__4 .
H82:   begidx__4 <= zlength .
H83:   endidx__4 <= zlength .
H84:   (foundtype__4 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__4) and (i_ <= endidx__4)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H85:   begidx__4 >= rr_type__linelengthindex__first .
H86:   begidx__4 <= rr_type__linelengthindex__last .
H87:   endidx__4 >= rr_type__linelengthindex__first .
H88:   endidx__4 <= rr_type__linelengthindex__last .
H89:   foundtype__4 >= rr_type__rritemtype__first .
H90:   foundtype__4 <= rr_type__rritemtype__last .
H91:   foundtype__4 >= rr_type__rritemtype__first .
H92:   foundtype__4 <= rr_type__rritemtype__last .
H93:   endidx__4 >= rr_type__linelengthindex__first .
H94:   endidx__4 <= rr_type__linelengthindex__last .
H95:   begidx__4 >= rr_type__linelengthindex__first .
H96:   begidx__4 <= rr_type__linelengthindex__last .
H97:   foundtype__4 >= rr_type__rritemtype__first .
H98:   foundtype__4 <= rr_type__rritemtype__last .
H99:   not ((foundtype__4 <> rr_type__domainnameortimespec) and (
           foundtype__4 <> rr_type__number)) .
H100:  begidx__4 >= rr_type__linelengthindex__first .
H101:  begidx__4 <= rr_type__linelengthindex__last .
H102:  endidx__4 >= rr_type__linelengthindex__first .
H103:  endidx__4 <= rr_type__linelengthindex__last .
H104:  endidx__4 >= integer__first .
H105:  endidx__4 <= integer__last .
H106:  begidx__4 >= integer__first .
H107:  begidx__4 <= integer__last .
H108:  (begidx__4 <= endidx__4) -> ((endidx__4 >= integer__first) and (
           endidx__4 <= integer__last)) .
H109:  (begidx__4 <= endidx__4) -> ((begidx__4 >= integer__first) and (
           begidx__4 <= integer__last)) .
H110:  begidx__4 >= rr_type__linelengthindex__first .
H111:  begidx__4 <= rr_type__linelengthindex__last .
H112:  endidx__4 >= rr_type__linelengthindex__first .
H113:  endidx__4 <= rr_type__linelengthindex__last .
H114:  begidx__4 <= endidx__4 .
        ->
C1:    begidx__4 >= 1 .
C2:    begidx__4 <= endidx__4 .
C3:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           neworigin, [i___1]) >= character__first) and (element(
           neworigin, [i___1]) <= character__last))) .
C4:    newttl >= unsigned_types__unsigned32__first .
C5:    newttl <= unsigned_types__unsigned32__last .
C6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
C7:    zlength >= rr_type__linelengthindex__first .
C8:    zlength <= rr_type__linelengthindex__last .
C9:    begidx__4 >= integer__first .
C10:   begidx__4 <= integer__last .
C11:   begidx__4 >= begidx__4 .
C12:   begidx__4 <= endidx__4 .
C13:   endidx__4 >= rr_type__linelengthindex__first .
C14:   endidx__4 <= rr_type__linelengthindex__last .
 

procedure_parsecontrolline_34.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           neworigin, [i___1]) >= character__first) and (element(
           neworigin, [i___1]) <= character__last))) .
H2:    newttl >= unsigned_types__unsigned32__first .
H3:    newttl <= unsigned_types__unsigned32__last .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H5:    zlength >= rr_type__linelengthindex__first .
H6:    zlength <= rr_type__linelengthindex__last .
H7:    1 >= rr_type__linelengthindex__first .
H8:    1 <= rr_type__linelengthindex__last .
H9:    1 >= rr_type__linelengthindex__first .
H10:   1 <= rr_type__linelengthindex__last .
H11:   zlength >= rr_type__linelengthindex__first .
H12:   zlength <= rr_type__linelengthindex__last .
H13:   1 <= zlength .
H14:   begidx__1 <= endidx__1 .
H15:   begidx__1 <= zlength .
H16:   endidx__1 <= zlength .
H17:   (foundtype__1 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__1) and (i_ <= endidx__1)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H18:   begidx__1 >= rr_type__linelengthindex__first .
H19:   begidx__1 <= rr_type__linelengthindex__last .
H20:   endidx__1 >= rr_type__linelengthindex__first .
H21:   endidx__1 <= rr_type__linelengthindex__last .
H22:   foundtype__1 >= rr_type__rritemtype__first .
H23:   foundtype__1 <= rr_type__rritemtype__last .
H24:   foundtype__1 >= rr_type__rritemtype__first .
H25:   foundtype__1 <= rr_type__rritemtype__last .
H26:   endidx__1 >= rr_type__linelengthindex__first .
H27:   endidx__1 <= rr_type__linelengthindex__last .
H28:   begidx__1 >= rr_type__linelengthindex__first .
H29:   begidx__1 <= rr_type__linelengthindex__last .
H30:   foundtype__1 >= rr_type__rritemtype__first .
H31:   foundtype__1 <= rr_type__rritemtype__last .
H32:   foundtype__1 = rr_type__control .
H33:   begidx__1 >= rr_type__linelengthindex__first .
H34:   begidx__1 <= rr_type__linelengthindex__last .
H35:   endidx__1 >= rr_type__linelengthindex__first .
H36:   endidx__1 <= rr_type__linelengthindex__last .
H37:   endidx__1 - 6 >= integer__base__first .
H38:   endidx__1 - 6 <= integer__base__last .
H39:   not (begidx__1 <= endidx__1 - 6) .
H40:   begidx__1 >= rr_type__linelengthindex__first .
H41:   begidx__1 <= rr_type__linelengthindex__last .
H42:   endidx__1 >= rr_type__linelengthindex__first .
H43:   endidx__1 <= rr_type__linelengthindex__last .
H44:   endidx__1 - 3 >= integer__base__first .
H45:   endidx__1 - 3 <= integer__base__last .
H46:   begidx__1 <= endidx__1 - 3 .
H47:   begidx__1 >= rr_type__linelengthindex__first .
H48:   begidx__1 <= rr_type__linelengthindex__last .
H49:   begidx__1 + 3 >= rr_type__linelengthindex__first .
H50:   begidx__1 + 3 <= rr_type__linelengthindex__last .
H51:   begidx__1 + 3 >= integer__base__first .
H52:   begidx__1 + 3 <= integer__base__last .
H53:   begidx__1 + 2 >= rr_type__linelengthindex__first .
H54:   begidx__1 + 2 <= rr_type__linelengthindex__last .
H55:   begidx__1 + 2 >= integer__base__first .
H56:   begidx__1 + 2 <= integer__base__last .
H57:   begidx__1 + 1 >= rr_type__linelengthindex__first .
H58:   begidx__1 + 1 <= rr_type__linelengthindex__last .
H59:   begidx__1 + 1 >= integer__base__first .
H60:   begidx__1 + 1 <= integer__base__last .
H61:   element(zonefileline, [begidx__1 + 1]) = 84 .
H62:   element(zonefileline, [begidx__1 + 2]) = 84 .
H63:   element(zonefileline, [begidx__1 + 3]) = 76 .
H64:   begidx__1 >= rr_type__linelengthindex__first .
H65:   begidx__1 <= rr_type__linelengthindex__last .
H66:   endidx__1 >= rr_type__linelengthindex__first .
H67:   endidx__1 <= rr_type__linelengthindex__last .
H68:   not ((begidx__1 < zlength) and (endidx__1 < zlength)) .
H69:   foundtype__1 >= rr_type__rritemtype__first .
H70:   foundtype__1 <= rr_type__rritemtype__last .
H71:   not ((foundtype__1 <> rr_type__domainnameortimespec) and (
           foundtype__1 <> rr_type__number)) .
H72:   begidx__1 >= rr_type__linelengthindex__first .
H73:   begidx__1 <= rr_type__linelengthindex__last .
H74:   endidx__1 >= rr_type__linelengthindex__first .
H75:   endidx__1 <= rr_type__linelengthindex__last .
H76:   endidx__1 >= integer__first .
H77:   endidx__1 <= integer__last .
H78:   begidx__1 >= integer__first .
H79:   begidx__1 <= integer__last .
H80:   (begidx__1 <= endidx__1) -> ((endidx__1 >= integer__first) and (
           endidx__1 <= integer__last)) .
H81:   (begidx__1 <= endidx__1) -> ((begidx__1 >= integer__first) and (
           begidx__1 <= integer__last)) .
H82:   begidx__1 >= rr_type__linelengthindex__first .
H83:   begidx__1 <= rr_type__linelengthindex__last .
H84:   endidx__1 >= rr_type__linelengthindex__first .
H85:   endidx__1 <= rr_type__linelengthindex__last .
H86:   begidx__1 <= endidx__1 .
        ->
C1:    begidx__1 >= 1 .
C2:    begidx__1 <= endidx__1 .
C3:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           neworigin, [i___1]) >= character__first) and (element(
           neworigin, [i___1]) <= character__last))) .
C4:    newttl >= unsigned_types__unsigned32__first .
C5:    newttl <= unsigned_types__unsigned32__last .
C6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
C7:    zlength >= rr_type__linelengthindex__first .
C8:    zlength <= rr_type__linelengthindex__last .
C9:    begidx__1 >= integer__first .
C10:   begidx__1 <= integer__last .
C11:   begidx__1 >= begidx__1 .
C12:   begidx__1 <= endidx__1 .
C13:   endidx__1 >= rr_type__linelengthindex__first .
C14:   endidx__1 <= rr_type__linelengthindex__last .
 

For path(s) from assertion of line 674 to assertion of line 674:

procedure_parsecontrolline_35.
H1:    begidx >= 1 .
H2:    begidx <= endidx .
H3:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           neworigin, [i___1]) >= character__first) and (element(
           neworigin, [i___1]) <= character__last))) .
H4:    newttl >= unsigned_types__unsigned32__first .
H5:    newttl <= unsigned_types__unsigned32__last .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H7:    zlength >= rr_type__linelengthindex__first .
H8:    zlength <= rr_type__linelengthindex__last .
H9:    loop__2__i >= integer__first .
H10:   loop__2__i <= integer__last .
H11:   loop__2__i >= begidx .
H12:   loop__2__i <= endidx__entry__loop__2 .
H13:   endidx__entry__loop__2 >= rr_type__linelengthindex__first .
H14:   endidx__entry__loop__2 <= rr_type__linelengthindex__last .
H15:   element(zonefileline, [loop__2__i]) >= character__first .
H16:   element(zonefileline, [loop__2__i]) <= character__last .
H17:   loop__2__i >= rr_type__linelengthindex__first .
H18:   loop__2__i <= rr_type__linelengthindex__last .
H19:   loop__2__i >= rr_type__linelengthindex__first .
H20:   loop__2__i <= rr_type__linelengthindex__last .
H21:   not (loop__2__i = endidx__entry__loop__2) .
        ->
C1:    begidx >= 1 .
C2:    begidx <= endidx .
C3:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           neworigin, [i___1]) >= character__first) and (element(
           neworigin, [i___1]) <= character__last))) .
C4:    newttl >= unsigned_types__unsigned32__first .
C5:    newttl <= unsigned_types__unsigned32__last .
C6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
C7:    zlength >= rr_type__linelengthindex__first .
C8:    zlength <= rr_type__linelengthindex__last .
C9:    loop__2__i + 1 >= integer__first .
C10:   loop__2__i + 1 <= integer__last .
C11:   loop__2__i + 1 >= begidx .
C12:   loop__2__i + 1 <= endidx__entry__loop__2 .
C13:   endidx__entry__loop__2 >= rr_type__linelengthindex__first .
C14:   endidx__entry__loop__2 <= rr_type__linelengthindex__last .
 

For path(s) from assertion of line 674 to run-time check associated with statement of line 675:

procedure_parsecontrolline_36.
H1:    begidx >= 1 .
H2:    begidx <= endidx .
H3:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           neworigin, [i___1]) >= character__first) and (element(
           neworigin, [i___1]) <= character__last))) .
H4:    newttl >= unsigned_types__unsigned32__first .
H5:    newttl <= unsigned_types__unsigned32__last .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H7:    zlength >= rr_type__linelengthindex__first .
H8:    zlength <= rr_type__linelengthindex__last .
H9:    loop__2__i >= integer__first .
H10:   loop__2__i <= integer__last .
H11:   loop__2__i >= begidx .
H12:   loop__2__i <= endidx__entry__loop__2 .
H13:   endidx__entry__loop__2 >= rr_type__linelengthindex__first .
H14:   endidx__entry__loop__2 <= rr_type__linelengthindex__last .
        ->
C1:    element(zonefileline, [loop__2__i]) >= character__first .
C2:    element(zonefileline, [loop__2__i]) <= character__last .
C3:    loop__2__i >= rr_type__linelengthindex__first .
C4:    loop__2__i <= rr_type__linelengthindex__last .
C5:    loop__2__i >= rr_type__linelengthindex__first .
C6:    loop__2__i <= rr_type__linelengthindex__last .
 

For path(s) from start to run-time check associated with statement of line 677:

procedure_parsecontrolline_37.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           neworigin, [i___1]) >= character__first) and (element(
           neworigin, [i___1]) <= character__last))) .
H2:    newttl >= unsigned_types__unsigned32__first .
H3:    newttl <= unsigned_types__unsigned32__last .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H5:    zlength >= rr_type__linelengthindex__first .
H6:    zlength <= rr_type__linelengthindex__last .
H7:    1 >= rr_type__linelengthindex__first .
H8:    1 <= rr_type__linelengthindex__last .
H9:    1 >= rr_type__linelengthindex__first .
H10:   1 <= rr_type__linelengthindex__last .
H11:   zlength >= rr_type__linelengthindex__first .
H12:   zlength <= rr_type__linelengthindex__last .
H13:   1 <= zlength .
H14:   begidx__1 <= endidx__1 .
H15:   begidx__1 <= zlength .
H16:   endidx__1 <= zlength .
H17:   (foundtype__1 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__1) and (i_ <= endidx__1)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H18:   begidx__1 >= rr_type__linelengthindex__first .
H19:   begidx__1 <= rr_type__linelengthindex__last .
H20:   endidx__1 >= rr_type__linelengthindex__first .
H21:   endidx__1 <= rr_type__linelengthindex__last .
H22:   foundtype__1 >= rr_type__rritemtype__first .
H23:   foundtype__1 <= rr_type__rritemtype__last .
H24:   foundtype__1 >= rr_type__rritemtype__first .
H25:   foundtype__1 <= rr_type__rritemtype__last .
H26:   endidx__1 >= rr_type__linelengthindex__first .
H27:   endidx__1 <= rr_type__linelengthindex__last .
H28:   begidx__1 >= rr_type__linelengthindex__first .
H29:   begidx__1 <= rr_type__linelengthindex__last .
H30:   foundtype__1 >= rr_type__rritemtype__first .
H31:   foundtype__1 <= rr_type__rritemtype__last .
H32:   foundtype__1 = rr_type__control .
H33:   begidx__1 >= rr_type__linelengthindex__first .
H34:   begidx__1 <= rr_type__linelengthindex__last .
H35:   endidx__1 >= rr_type__linelengthindex__first .
H36:   endidx__1 <= rr_type__linelengthindex__last .
H37:   endidx__1 - 6 >= integer__base__first .
H38:   endidx__1 - 6 <= integer__base__last .
H39:   not (begidx__1 <= endidx__1 - 6) .
H40:   begidx__1 >= rr_type__linelengthindex__first .
H41:   begidx__1 <= rr_type__linelengthindex__last .
H42:   endidx__1 >= rr_type__linelengthindex__first .
H43:   endidx__1 <= rr_type__linelengthindex__last .
H44:   endidx__1 - 3 >= integer__base__first .
H45:   endidx__1 - 3 <= integer__base__last .
H46:   begidx__1 <= endidx__1 - 3 .
H47:   begidx__1 >= rr_type__linelengthindex__first .
H48:   begidx__1 <= rr_type__linelengthindex__last .
H49:   begidx__1 + 3 >= rr_type__linelengthindex__first .
H50:   begidx__1 + 3 <= rr_type__linelengthindex__last .
H51:   begidx__1 + 3 >= integer__base__first .
H52:   begidx__1 + 3 <= integer__base__last .
H53:   begidx__1 + 2 >= rr_type__linelengthindex__first .
H54:   begidx__1 + 2 <= rr_type__linelengthindex__last .
H55:   begidx__1 + 2 >= integer__base__first .
H56:   begidx__1 + 2 <= integer__base__last .
H57:   begidx__1 + 1 >= rr_type__linelengthindex__first .
H58:   begidx__1 + 1 <= rr_type__linelengthindex__last .
H59:   begidx__1 + 1 >= integer__base__first .
H60:   begidx__1 + 1 <= integer__base__last .
H61:   element(zonefileline, [begidx__1 + 1]) = 84 .
H62:   element(zonefileline, [begidx__1 + 2]) = 84 .
H63:   element(zonefileline, [begidx__1 + 3]) = 76 .
H64:   begidx__1 >= rr_type__linelengthindex__first .
H65:   begidx__1 <= rr_type__linelengthindex__last .
H66:   endidx__1 >= rr_type__linelengthindex__first .
H67:   endidx__1 <= rr_type__linelengthindex__last .
H68:   begidx__1 < zlength .
H69:   endidx__1 < zlength .
H70:   endidx__1 >= rr_type__linelengthindex__first .
H71:   endidx__1 <= rr_type__linelengthindex__last .
H72:   endidx__1 + 1 >= rr_type__linelengthindex__first .
H73:   endidx__1 + 1 <= rr_type__linelengthindex__last .
H74:   endidx__1 + 1 >= rr_type__linelengthindex__first .
H75:   endidx__1 + 1 <= rr_type__linelengthindex__last .
H76:   endidx__1 + 1 >= rr_type__linelengthindex__first .
H77:   endidx__1 + 1 <= rr_type__linelengthindex__last .
H78:   zlength >= rr_type__linelengthindex__first .
H79:   zlength <= rr_type__linelengthindex__last .
H80:   endidx__1 + 1 <= zlength .
H81:   begidx__4 <= endidx__4 .
H82:   begidx__4 <= zlength .
H83:   endidx__4 <= zlength .
H84:   (foundtype__4 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__4) and (i_ <= endidx__4)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H85:   begidx__4 >= rr_type__linelengthindex__first .
H86:   begidx__4 <= rr_type__linelengthindex__last .
H87:   endidx__4 >= rr_type__linelengthindex__first .
H88:   endidx__4 <= rr_type__linelengthindex__last .
H89:   foundtype__4 >= rr_type__rritemtype__first .
H90:   foundtype__4 <= rr_type__rritemtype__last .
H91:   foundtype__4 >= rr_type__rritemtype__first .
H92:   foundtype__4 <= rr_type__rritemtype__last .
H93:   endidx__4 >= rr_type__linelengthindex__first .
H94:   endidx__4 <= rr_type__linelengthindex__last .
H95:   begidx__4 >= rr_type__linelengthindex__first .
H96:   begidx__4 <= rr_type__linelengthindex__last .
H97:   foundtype__4 >= rr_type__rritemtype__first .
H98:   foundtype__4 <= rr_type__rritemtype__last .
H99:   not ((foundtype__4 <> rr_type__domainnameortimespec) and (
           foundtype__4 <> rr_type__number)) .
H100:  begidx__4 >= rr_type__linelengthindex__first .
H101:  begidx__4 <= rr_type__linelengthindex__last .
H102:  endidx__4 >= rr_type__linelengthindex__first .
H103:  endidx__4 <= rr_type__linelengthindex__last .
H104:  endidx__4 >= integer__first .
H105:  endidx__4 <= integer__last .
H106:  begidx__4 >= integer__first .
H107:  begidx__4 <= integer__last .
H108:  (begidx__4 <= endidx__4) -> ((endidx__4 >= integer__first) and (
           endidx__4 <= integer__last)) .
H109:  (begidx__4 <= endidx__4) -> ((begidx__4 >= integer__first) and (
           begidx__4 <= integer__last)) .
H110:  begidx__4 >= rr_type__linelengthindex__first .
H111:  begidx__4 <= rr_type__linelengthindex__last .
H112:  endidx__4 >= rr_type__linelengthindex__first .
H113:  endidx__4 <= rr_type__linelengthindex__last .
H114:  not (begidx__4 <= endidx__4) .
H115:  for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           mk__string(32), [i___1]) >= character__first) and (element(
           mk__string(32), [i___1]) <= character__last))) .
        ->
C1:    rr_type__maxlinelength >= rr_type__linelengthindex__first .
C2:    rr_type__maxlinelength <= rr_type__linelengthindex__last .
 

procedure_parsecontrolline_38.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           neworigin, [i___1]) >= character__first) and (element(
           neworigin, [i___1]) <= character__last))) .
H2:    newttl >= unsigned_types__unsigned32__first .
H3:    newttl <= unsigned_types__unsigned32__last .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H5:    zlength >= rr_type__linelengthindex__first .
H6:    zlength <= rr_type__linelengthindex__last .
H7:    1 >= rr_type__linelengthindex__first .
H8:    1 <= rr_type__linelengthindex__last .
H9:    1 >= rr_type__linelengthindex__first .
H10:   1 <= rr_type__linelengthindex__last .
H11:   zlength >= rr_type__linelengthindex__first .
H12:   zlength <= rr_type__linelengthindex__last .
H13:   1 <= zlength .
H14:   begidx__1 <= endidx__1 .
H15:   begidx__1 <= zlength .
H16:   endidx__1 <= zlength .
H17:   (foundtype__1 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__1) and (i_ <= endidx__1)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H18:   begidx__1 >= rr_type__linelengthindex__first .
H19:   begidx__1 <= rr_type__linelengthindex__last .
H20:   endidx__1 >= rr_type__linelengthindex__first .
H21:   endidx__1 <= rr_type__linelengthindex__last .
H22:   foundtype__1 >= rr_type__rritemtype__first .
H23:   foundtype__1 <= rr_type__rritemtype__last .
H24:   foundtype__1 >= rr_type__rritemtype__first .
H25:   foundtype__1 <= rr_type__rritemtype__last .
H26:   endidx__1 >= rr_type__linelengthindex__first .
H27:   endidx__1 <= rr_type__linelengthindex__last .
H28:   begidx__1 >= rr_type__linelengthindex__first .
H29:   begidx__1 <= rr_type__linelengthindex__last .
H30:   foundtype__1 >= rr_type__rritemtype__first .
H31:   foundtype__1 <= rr_type__rritemtype__last .
H32:   foundtype__1 = rr_type__control .
H33:   begidx__1 >= rr_type__linelengthindex__first .
H34:   begidx__1 <= rr_type__linelengthindex__last .
H35:   endidx__1 >= rr_type__linelengthindex__first .
H36:   endidx__1 <= rr_type__linelengthindex__last .
H37:   endidx__1 - 6 >= integer__base__first .
H38:   endidx__1 - 6 <= integer__base__last .
H39:   not (begidx__1 <= endidx__1 - 6) .
H40:   begidx__1 >= rr_type__linelengthindex__first .
H41:   begidx__1 <= rr_type__linelengthindex__last .
H42:   endidx__1 >= rr_type__linelengthindex__first .
H43:   endidx__1 <= rr_type__linelengthindex__last .
H44:   endidx__1 - 3 >= integer__base__first .
H45:   endidx__1 - 3 <= integer__base__last .
H46:   begidx__1 <= endidx__1 - 3 .
H47:   begidx__1 >= rr_type__linelengthindex__first .
H48:   begidx__1 <= rr_type__linelengthindex__last .
H49:   begidx__1 + 3 >= rr_type__linelengthindex__first .
H50:   begidx__1 + 3 <= rr_type__linelengthindex__last .
H51:   begidx__1 + 3 >= integer__base__first .
H52:   begidx__1 + 3 <= integer__base__last .
H53:   begidx__1 + 2 >= rr_type__linelengthindex__first .
H54:   begidx__1 + 2 <= rr_type__linelengthindex__last .
H55:   begidx__1 + 2 >= integer__base__first .
H56:   begidx__1 + 2 <= integer__base__last .
H57:   begidx__1 + 1 >= rr_type__linelengthindex__first .
H58:   begidx__1 + 1 <= rr_type__linelengthindex__last .
H59:   begidx__1 + 1 >= integer__base__first .
H60:   begidx__1 + 1 <= integer__base__last .
H61:   element(zonefileline, [begidx__1 + 1]) = 84 .
H62:   element(zonefileline, [begidx__1 + 2]) = 84 .
H63:   element(zonefileline, [begidx__1 + 3]) = 76 .
H64:   begidx__1 >= rr_type__linelengthindex__first .
H65:   begidx__1 <= rr_type__linelengthindex__last .
H66:   endidx__1 >= rr_type__linelengthindex__first .
H67:   endidx__1 <= rr_type__linelengthindex__last .
H68:   not ((begidx__1 < zlength) and (endidx__1 < zlength)) .
H69:   foundtype__1 >= rr_type__rritemtype__first .
H70:   foundtype__1 <= rr_type__rritemtype__last .
H71:   not ((foundtype__1 <> rr_type__domainnameortimespec) and (
           foundtype__1 <> rr_type__number)) .
H72:   begidx__1 >= rr_type__linelengthindex__first .
H73:   begidx__1 <= rr_type__linelengthindex__last .
H74:   endidx__1 >= rr_type__linelengthindex__first .
H75:   endidx__1 <= rr_type__linelengthindex__last .
H76:   endidx__1 >= integer__first .
H77:   endidx__1 <= integer__last .
H78:   begidx__1 >= integer__first .
H79:   begidx__1 <= integer__last .
H80:   (begidx__1 <= endidx__1) -> ((endidx__1 >= integer__first) and (
           endidx__1 <= integer__last)) .
H81:   (begidx__1 <= endidx__1) -> ((begidx__1 >= integer__first) and (
           begidx__1 <= integer__last)) .
H82:   begidx__1 >= rr_type__linelengthindex__first .
H83:   begidx__1 <= rr_type__linelengthindex__last .
H84:   endidx__1 >= rr_type__linelengthindex__first .
H85:   endidx__1 <= rr_type__linelengthindex__last .
H86:   not (begidx__1 <= endidx__1) .
H87:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           mk__string(32), [i___1]) >= character__first) and (element(
           mk__string(32), [i___1]) <= character__last))) .
        ->
C1:    rr_type__maxlinelength >= rr_type__linelengthindex__first .
C2:    rr_type__maxlinelength <= rr_type__linelengthindex__last .
 

For path(s) from assertion of line 674 to run-time check associated with statement of line 677:

procedure_parsecontrolline_39.
H1:    begidx >= 1 .
H2:    begidx <= endidx .
H3:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           neworigin, [i___1]) >= character__first) and (element(
           neworigin, [i___1]) <= character__last))) .
H4:    newttl >= unsigned_types__unsigned32__first .
H5:    newttl <= unsigned_types__unsigned32__last .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H7:    zlength >= rr_type__linelengthindex__first .
H8:    zlength <= rr_type__linelengthindex__last .
H9:    loop__2__i >= integer__first .
H10:   loop__2__i <= integer__last .
H11:   loop__2__i >= begidx .
H12:   loop__2__i <= endidx__entry__loop__2 .
H13:   endidx__entry__loop__2 >= rr_type__linelengthindex__first .
H14:   endidx__entry__loop__2 <= rr_type__linelengthindex__last .
H15:   element(zonefileline, [loop__2__i]) >= character__first .
H16:   element(zonefileline, [loop__2__i]) <= character__last .
H17:   loop__2__i >= rr_type__linelengthindex__first .
H18:   loop__2__i <= rr_type__linelengthindex__last .
H19:   loop__2__i >= rr_type__linelengthindex__first .
H20:   loop__2__i <= rr_type__linelengthindex__last .
H21:   loop__2__i = endidx__entry__loop__2 .
H22:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(update(
           tmpline, [loop__2__i], element(zonefileline, [
           loop__2__i])), [i___1]) >= character__first) and (element(update(
           tmpline, [loop__2__i], element(zonefileline, [
           loop__2__i])), [i___1]) <= character__last))) .
        ->
C1:    rr_type__maxlinelength >= rr_type__linelengthindex__first .
C2:    rr_type__maxlinelength <= rr_type__linelengthindex__last .
 

For path(s) from start to run-time check associated with statement of line 677:

procedure_parsecontrolline_40.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           neworigin, [i___1]) >= character__first) and (element(
           neworigin, [i___1]) <= character__last))) .
H2:    newttl >= unsigned_types__unsigned32__first .
H3:    newttl <= unsigned_types__unsigned32__last .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H5:    zlength >= rr_type__linelengthindex__first .
H6:    zlength <= rr_type__linelengthindex__last .
H7:    1 >= rr_type__linelengthindex__first .
H8:    1 <= rr_type__linelengthindex__last .
H9:    1 >= rr_type__linelengthindex__first .
H10:   1 <= rr_type__linelengthindex__last .
H11:   zlength >= rr_type__linelengthindex__first .
H12:   zlength <= rr_type__linelengthindex__last .
H13:   1 <= zlength .
H14:   begidx__1 <= endidx__1 .
H15:   begidx__1 <= zlength .
H16:   endidx__1 <= zlength .
H17:   (foundtype__1 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__1) and (i_ <= endidx__1)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H18:   begidx__1 >= rr_type__linelengthindex__first .
H19:   begidx__1 <= rr_type__linelengthindex__last .
H20:   endidx__1 >= rr_type__linelengthindex__first .
H21:   endidx__1 <= rr_type__linelengthindex__last .
H22:   foundtype__1 >= rr_type__rritemtype__first .
H23:   foundtype__1 <= rr_type__rritemtype__last .
H24:   foundtype__1 >= rr_type__rritemtype__first .
H25:   foundtype__1 <= rr_type__rritemtype__last .
H26:   endidx__1 >= rr_type__linelengthindex__first .
H27:   endidx__1 <= rr_type__linelengthindex__last .
H28:   begidx__1 >= rr_type__linelengthindex__first .
H29:   begidx__1 <= rr_type__linelengthindex__last .
H30:   foundtype__1 >= rr_type__rritemtype__first .
H31:   foundtype__1 <= rr_type__rritemtype__last .
H32:   foundtype__1 = rr_type__control .
H33:   begidx__1 >= rr_type__linelengthindex__first .
H34:   begidx__1 <= rr_type__linelengthindex__last .
H35:   endidx__1 >= rr_type__linelengthindex__first .
H36:   endidx__1 <= rr_type__linelengthindex__last .
H37:   endidx__1 - 6 >= integer__base__first .
H38:   endidx__1 - 6 <= integer__base__last .
H39:   not (begidx__1 <= endidx__1 - 6) .
H40:   begidx__1 >= rr_type__linelengthindex__first .
H41:   begidx__1 <= rr_type__linelengthindex__last .
H42:   endidx__1 >= rr_type__linelengthindex__first .
H43:   endidx__1 <= rr_type__linelengthindex__last .
H44:   endidx__1 - 3 >= integer__base__first .
H45:   endidx__1 - 3 <= integer__base__last .
H46:   begidx__1 <= endidx__1 - 3 .
H47:   begidx__1 >= rr_type__linelengthindex__first .
H48:   begidx__1 <= rr_type__linelengthindex__last .
H49:   begidx__1 + 3 >= rr_type__linelengthindex__first .
H50:   begidx__1 + 3 <= rr_type__linelengthindex__last .
H51:   begidx__1 + 3 >= integer__base__first .
H52:   begidx__1 + 3 <= integer__base__last .
H53:   begidx__1 + 2 >= rr_type__linelengthindex__first .
H54:   begidx__1 + 2 <= rr_type__linelengthindex__last .
H55:   begidx__1 + 2 >= integer__base__first .
H56:   begidx__1 + 2 <= integer__base__last .
H57:   begidx__1 + 1 >= rr_type__linelengthindex__first .
H58:   begidx__1 + 1 <= rr_type__linelengthindex__last .
H59:   begidx__1 + 1 >= integer__base__first .
H60:   begidx__1 + 1 <= integer__base__last .
H61:   element(zonefileline, [begidx__1 + 1]) = 84 .
H62:   element(zonefileline, [begidx__1 + 2]) = 84 .
H63:   element(zonefileline, [begidx__1 + 3]) = 76 .
H64:   begidx__1 >= rr_type__linelengthindex__first .
H65:   begidx__1 <= rr_type__linelengthindex__last .
H66:   endidx__1 >= rr_type__linelengthindex__first .
H67:   endidx__1 <= rr_type__linelengthindex__last .
H68:   begidx__1 < zlength .
H69:   endidx__1 < zlength .
H70:   endidx__1 >= rr_type__linelengthindex__first .
H71:   endidx__1 <= rr_type__linelengthindex__last .
H72:   endidx__1 + 1 >= rr_type__linelengthindex__first .
H73:   endidx__1 + 1 <= rr_type__linelengthindex__last .
H74:   endidx__1 + 1 >= rr_type__linelengthindex__first .
H75:   endidx__1 + 1 <= rr_type__linelengthindex__last .
H76:   endidx__1 + 1 >= rr_type__linelengthindex__first .
H77:   endidx__1 + 1 <= rr_type__linelengthindex__last .
H78:   zlength >= rr_type__linelengthindex__first .
H79:   zlength <= rr_type__linelengthindex__last .
H80:   endidx__1 + 1 <= zlength .
H81:   begidx__4 <= endidx__4 .
H82:   begidx__4 <= zlength .
H83:   endidx__4 <= zlength .
H84:   (foundtype__4 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__4) and (i_ <= endidx__4)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H85:   begidx__4 >= rr_type__linelengthindex__first .
H86:   begidx__4 <= rr_type__linelengthindex__last .
H87:   endidx__4 >= rr_type__linelengthindex__first .
H88:   endidx__4 <= rr_type__linelengthindex__last .
H89:   foundtype__4 >= rr_type__rritemtype__first .
H90:   foundtype__4 <= rr_type__rritemtype__last .
H91:   foundtype__4 >= rr_type__rritemtype__first .
H92:   foundtype__4 <= rr_type__rritemtype__last .
H93:   endidx__4 >= rr_type__linelengthindex__first .
H94:   endidx__4 <= rr_type__linelengthindex__last .
H95:   begidx__4 >= rr_type__linelengthindex__first .
H96:   begidx__4 <= rr_type__linelengthindex__last .
H97:   foundtype__4 >= rr_type__rritemtype__first .
H98:   foundtype__4 <= rr_type__rritemtype__last .
H99:   not ((foundtype__4 <> rr_type__domainnameortimespec) and (
           foundtype__4 <> rr_type__number)) .
H100:  begidx__4 >= rr_type__linelengthindex__first .
H101:  begidx__4 <= rr_type__linelengthindex__last .
H102:  endidx__4 >= rr_type__linelengthindex__first .
H103:  endidx__4 <= rr_type__linelengthindex__last .
H104:  endidx__4 >= integer__first .
H105:  endidx__4 <= integer__last .
H106:  begidx__4 >= integer__first .
H107:  begidx__4 <= integer__last .
H108:  (begidx__4 <= endidx__4) -> ((endidx__4 >= integer__first) and (
           endidx__4 <= integer__last)) .
H109:  (begidx__4 <= endidx__4) -> ((begidx__4 >= integer__first) and (
           begidx__4 <= integer__last)) .
H110:  begidx__4 >= rr_type__linelengthindex__first .
H111:  begidx__4 <= rr_type__linelengthindex__last .
H112:  endidx__4 >= rr_type__linelengthindex__first .
H113:  endidx__4 <= rr_type__linelengthindex__last .
H114:  not (begidx__4 <= endidx__4) .
H115:  for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           mk__string(32), [i___1]) >= character__first) and (element(
           mk__string(32), [i___1]) <= character__last))) .
H116:  rr_type__maxlinelength >= rr_type__linelengthindex__first .
H117:  rr_type__maxlinelength <= rr_type__linelengthindex__last .
H118:  newttl__5 >= unsigned_types__unsigned32__first .
H119:  newttl__5 <= unsigned_types__unsigned32__last .
        ->
C1:    newttl__5 >= unsigned_types__unsigned32__first .
C2:    newttl__5 <= unsigned_types__unsigned32__last .
 

procedure_parsecontrolline_41.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           neworigin, [i___1]) >= character__first) and (element(
           neworigin, [i___1]) <= character__last))) .
H2:    newttl >= unsigned_types__unsigned32__first .
H3:    newttl <= unsigned_types__unsigned32__last .
H4:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H5:    zlength >= rr_type__linelengthindex__first .
H6:    zlength <= rr_type__linelengthindex__last .
H7:    1 >= rr_type__linelengthindex__first .
H8:    1 <= rr_type__linelengthindex__last .
H9:    1 >= rr_type__linelengthindex__first .
H10:   1 <= rr_type__linelengthindex__last .
H11:   zlength >= rr_type__linelengthindex__first .
H12:   zlength <= rr_type__linelengthindex__last .
H13:   1 <= zlength .
H14:   begidx__1 <= endidx__1 .
H15:   begidx__1 <= zlength .
H16:   endidx__1 <= zlength .
H17:   (foundtype__1 = rr_type__number) -> (for_all(i_: 
           integer, ((i_ >= begidx__1) and (i_ <= endidx__1)) -> ((element(
           zonefileline, [i_]) >= 48) and (element(
           zonefileline, [i_]) <= 57)))) .
H18:   begidx__1 >= rr_type__linelengthindex__first .
H19:   begidx__1 <= rr_type__linelengthindex__last .
H20:   endidx__1 >= rr_type__linelengthindex__first .
H21:   endidx__1 <= rr_type__linelengthindex__last .
H22:   foundtype__1 >= rr_type__rritemtype__first .
H23:   foundtype__1 <= rr_type__rritemtype__last .
H24:   foundtype__1 >= rr_type__rritemtype__first .
H25:   foundtype__1 <= rr_type__rritemtype__last .
H26:   endidx__1 >= rr_type__linelengthindex__first .
H27:   endidx__1 <= rr_type__linelengthindex__last .
H28:   begidx__1 >= rr_type__linelengthindex__first .
H29:   begidx__1 <= rr_type__linelengthindex__last .
H30:   foundtype__1 >= rr_type__rritemtype__first .
H31:   foundtype__1 <= rr_type__rritemtype__last .
H32:   foundtype__1 = rr_type__control .
H33:   begidx__1 >= rr_type__linelengthindex__first .
H34:   begidx__1 <= rr_type__linelengthindex__last .
H35:   endidx__1 >= rr_type__linelengthindex__first .
H36:   endidx__1 <= rr_type__linelengthindex__last .
H37:   endidx__1 - 6 >= integer__base__first .
H38:   endidx__1 - 6 <= integer__base__last .
H39:   not (begidx__1 <= endidx__1 - 6) .
H40:   begidx__1 >= rr_type__linelengthindex__first .
H41:   begidx__1 <= rr_type__linelengthindex__last .
H42:   endidx__1 >= rr_type__linelengthindex__first .
H43:   endidx__1 <= rr_type__linelengthindex__last .
H44:   endidx__1 - 3 >= integer__base__first .
H45:   endidx__1 - 3 <= integer__base__last .
H46:   begidx__1 <= endidx__1 - 3 .
H47:   begidx__1 >= rr_type__linelengthindex__first .
H48:   begidx__1 <= rr_type__linelengthindex__last .
H49:   begidx__1 + 3 >= rr_type__linelengthindex__first .
H50:   begidx__1 + 3 <= rr_type__linelengthindex__last .
H51:   begidx__1 + 3 >= integer__base__first .
H52:   begidx__1 + 3 <= integer__base__last .
H53:   begidx__1 + 2 >= rr_type__linelengthindex__first .
H54:   begidx__1 + 2 <= rr_type__linelengthindex__last .
H55:   begidx__1 + 2 >= integer__base__first .
H56:   begidx__1 + 2 <= integer__base__last .
H57:   begidx__1 + 1 >= rr_type__linelengthindex__first .
H58:   begidx__1 + 1 <= rr_type__linelengthindex__last .
H59:   begidx__1 + 1 >= integer__base__first .
H60:   begidx__1 + 1 <= integer__base__last .
H61:   element(zonefileline, [begidx__1 + 1]) = 84 .
H62:   element(zonefileline, [begidx__1 + 2]) = 84 .
H63:   element(zonefileline, [begidx__1 + 3]) = 76 .
H64:   begidx__1 >= rr_type__linelengthindex__first .
H65:   begidx__1 <= rr_type__linelengthindex__last .
H66:   endidx__1 >= rr_type__linelengthindex__first .
H67:   endidx__1 <= rr_type__linelengthindex__last .
H68:   not ((begidx__1 < zlength) and (endidx__1 < zlength)) .
H69:   foundtype__1 >= rr_type__rritemtype__first .
H70:   foundtype__1 <= rr_type__rritemtype__last .
H71:   not ((foundtype__1 <> rr_type__domainnameortimespec) and (
           foundtype__1 <> rr_type__number)) .
H72:   begidx__1 >= rr_type__linelengthindex__first .
H73:   begidx__1 <= rr_type__linelengthindex__last .
H74:   endidx__1 >= rr_type__linelengthindex__first .
H75:   endidx__1 <= rr_type__linelengthindex__last .
H76:   endidx__1 >= integer__first .
H77:   endidx__1 <= integer__last .
H78:   begidx__1 >= integer__first .
H79:   begidx__1 <= integer__last .
H80:   (begidx__1 <= endidx__1) -> ((endidx__1 >= integer__first) and (
           endidx__1 <= integer__last)) .
H81:   (begidx__1 <= endidx__1) -> ((begidx__1 >= integer__first) and (
           begidx__1 <= integer__last)) .
H82:   begidx__1 >= rr_type__linelengthindex__first .
H83:   begidx__1 <= rr_type__linelengthindex__last .
H84:   endidx__1 >= rr_type__linelengthindex__first .
H85:   endidx__1 <= rr_type__linelengthindex__last .
H86:   not (begidx__1 <= endidx__1) .
H87:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           mk__string(32), [i___1]) >= character__first) and (element(
           mk__string(32), [i___1]) <= character__last))) .
H88:   rr_type__maxlinelength >= rr_type__linelengthindex__first .
H89:   rr_type__maxlinelength <= rr_type__linelengthindex__last .
H90:   newttl__5 >= unsigned_types__unsigned32__first .
H91:   newttl__5 <= unsigned_types__unsigned32__last .
        ->
C1:    newttl__5 >= unsigned_types__unsigned32__first .
C2:    newttl__5 <= unsigned_types__unsigned32__last .
 

For path(s) from assertion of line 674 to run-time check associated with statement of line 677:

procedure_parsecontrolline_42.
H1:    begidx >= 1 .
H2:    begidx <= endidx .
H3:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           neworigin, [i___1]) >= character__first) and (element(
           neworigin, [i___1]) <= character__last))) .
H4:    newttl >= unsigned_types__unsigned32__first .
H5:    newttl <= unsigned_types__unsigned32__last .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           zonefileline, [i___1]) >= character__first) and (element(
           zonefileline, [i___1]) <= character__last))) .
H7:    zlength >= rr_type__linelengthindex__first .
H8:    zlength <= rr_type__linelengthindex__last .
H9:    loop__2__i >= integer__first .
H10:   loop__2__i <= integer__last .
H11:   loop__2__i >= begidx .
H12:   loop__2__i <= endidx__entry__loop__2 .
H13:   endidx__entry__loop__2 >= rr_type__linelengthindex__first .
H14:   endidx__entry__loop__2 <= rr_type__linelengthindex__last .
H15:   element(zonefileline, [loop__2__i]) >= character__first .
H16:   element(zonefileline, [loop__2__i]) <= character__last .
H17:   loop__2__i >= rr_type__linelengthindex__first .
H18:   loop__2__i <= rr_type__linelengthindex__last .
H19:   loop__2__i >= rr_type__linelengthindex__first .
H20:   loop__2__i <= rr_type__linelengthindex__last .
H21:   loop__2__i = endidx__entry__loop__2 .
H22:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(update(
           tmpline, [loop__2__i], element(zonefileline, [
           loop__2__i])), [i___1]) >= character__first) and (element(update(
           tmpline, [loop__2__i], element(zonefileline, [
           loop__2__i])), [i___1]) <= character__last))) .
H23:   rr_type__maxlinelength >= rr_type__linelengthindex__first .
H24:   rr_type__maxlinelength <= rr_type__linelengthindex__last .
H25:   newttl__5 >= unsigned_types__unsigned32__first .
H26:   newttl__5 <= unsigned_types__unsigned32__last .
        ->
C1:    newttl__5 >= unsigned_types__unsigned32__first .
C2:    newttl__5 <= unsigned_types__unsigned32__last .
 

For path(s) from start to finish:

procedure_parsecontrolline_43.
*** true .          /* trivially true VC removed by Examiner */


procedure_parsecontrolline_44.
*** true .          /* trivially true VC removed by Examiner */


procedure_parsecontrolline_45.
*** true .          /* trivially true VC removed by Examiner */


procedure_parsecontrolline_46.
*** true .          /* trivially true VC removed by Examiner */


procedure_parsecontrolline_47.
*** true .          /* trivially true VC removed by Examiner */


procedure_parsecontrolline_48.
*** true .          /* trivially true VC removed by Examiner */


procedure_parsecontrolline_49.
*** true .          /* trivially true VC removed by Examiner */


procedure_parsecontrolline_50.
*** true .          /* trivially true VC removed by Examiner */


procedure_parsecontrolline_51.
*** true .          /* trivially true VC removed by Examiner */


procedure_parsecontrolline_52.
*** true .          /* trivially true VC removed by Examiner */


procedure_parsecontrolline_53.
*** true .          /* trivially true VC removed by Examiner */


procedure_parsecontrolline_54.
*** true .          /* trivially true VC removed by Examiner */


procedure_parsecontrolline_55.
*** true .          /* trivially true VC removed by Examiner */


procedure_parsecontrolline_56.
*** true .          /* trivially true VC removed by Examiner */


For path(s) from assertion of line 649 to finish:

procedure_parsecontrolline_57.
*** true .          /* trivially true VC removed by Examiner */


For path(s) from assertion of line 674 to finish:

procedure_parsecontrolline_58.
*** true .          /* trivially true VC removed by Examiner */


