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

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


                procedure Zone_File_Parser.parseSerialNumber




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

procedure_parseserialnumber_1.
H1:    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))) .
H2:    zlength >= rr_type__linelengthindex__first .
H3:    zlength <= rr_type__linelengthindex__last .
        ->
C1:    0 >= unsigned_types__unsigned32__first .
C2:    0 <= unsigned_types__unsigned32__last .
 

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

procedure_parseserialnumber_2.
H1:    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))) .
H2:    zlength >= rr_type__linelengthindex__first .
H3:    zlength <= rr_type__linelengthindex__last .
H4:    0 >= unsigned_types__unsigned32__first .
H5:    0 <= unsigned_types__unsigned32__last .
H6:    1 >= rr_type__linelengthindex__first .
H7:    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 704:

procedure_parseserialnumber_3.
H1:    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))) .
H2:    zlength >= rr_type__linelengthindex__first .
H3:    zlength <= rr_type__linelengthindex__last .
H4:    0 >= unsigned_types__unsigned32__first .
H5:    0 <= unsigned_types__unsigned32__last .
H6:    1 >= rr_type__linelengthindex__first .
H7:    1 <= rr_type__linelengthindex__last .
H8:    1 >= rr_type__linelengthindex__first .
H9:    1 <= rr_type__linelengthindex__last .
H10:   zlength >= rr_type__linelengthindex__first .
H11:   zlength <= rr_type__linelengthindex__last .
H12:   1 <= zlength .
H13:   begidx__1 <= endidx__1 .
H14:   begidx__1 <= zlength .
H15:   endidx__1 <= zlength .
H16:   (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)))) .
H17:   begidx__1 >= rr_type__linelengthindex__first .
H18:   begidx__1 <= rr_type__linelengthindex__last .
H19:   endidx__1 >= rr_type__linelengthindex__first .
H20:   endidx__1 <= rr_type__linelengthindex__last .
H21:   foundtype__1 >= rr_type__rritemtype__first .
H22:   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 710:

procedure_parseserialnumber_4.
H1:    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))) .
H2:    zlength >= rr_type__linelengthindex__first .
H3:    zlength <= rr_type__linelengthindex__last .
H4:    0 >= unsigned_types__unsigned32__first .
H5:    0 <= unsigned_types__unsigned32__last .
H6:    1 >= rr_type__linelengthindex__first .
H7:    1 <= rr_type__linelengthindex__last .
H8:    1 >= rr_type__linelengthindex__first .
H9:    1 <= rr_type__linelengthindex__last .
H10:   zlength >= rr_type__linelengthindex__first .
H11:   zlength <= rr_type__linelengthindex__last .
H12:   1 <= zlength .
H13:   begidx__1 <= endidx__1 .
H14:   begidx__1 <= zlength .
H15:   endidx__1 <= zlength .
H16:   (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)))) .
H17:   begidx__1 >= rr_type__linelengthindex__first .
H18:   begidx__1 <= rr_type__linelengthindex__last .
H19:   endidx__1 >= rr_type__linelengthindex__first .
H20:   endidx__1 <= rr_type__linelengthindex__last .
H21:   foundtype__1 >= rr_type__rritemtype__first .
H22:   foundtype__1 <= rr_type__rritemtype__last .
H23:   foundtype__1 >= rr_type__rritemtype__first .
H24:   foundtype__1 <= rr_type__rritemtype__last .
H25:   endidx__1 >= rr_type__linelengthindex__first .
H26:   endidx__1 <= rr_type__linelengthindex__last .
H27:   begidx__1 >= rr_type__linelengthindex__first .
H28:   begidx__1 <= rr_type__linelengthindex__last .
H29:   foundtype__1 >= rr_type__rritemtype__first .
H30:   foundtype__1 <= rr_type__rritemtype__last .
H31:   not (foundtype__1 <> rr_type__number) .
        ->
C1:    0 >= long_long_integer__first .
C2:    0 <= long_long_integer__last .
 

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

procedure_parseserialnumber_5.
H1:    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))) .
H2:    zlength >= rr_type__linelengthindex__first .
H3:    zlength <= rr_type__linelengthindex__last .
H4:    0 >= unsigned_types__unsigned32__first .
H5:    0 <= unsigned_types__unsigned32__last .
H6:    1 >= rr_type__linelengthindex__first .
H7:    1 <= rr_type__linelengthindex__last .
H8:    1 >= rr_type__linelengthindex__first .
H9:    1 <= rr_type__linelengthindex__last .
H10:   zlength >= rr_type__linelengthindex__first .
H11:   zlength <= rr_type__linelengthindex__last .
H12:   1 <= zlength .
H13:   begidx__1 <= endidx__1 .
H14:   begidx__1 <= zlength .
H15:   endidx__1 <= zlength .
H16:   (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)))) .
H17:   begidx__1 >= rr_type__linelengthindex__first .
H18:   begidx__1 <= rr_type__linelengthindex__last .
H19:   endidx__1 >= rr_type__linelengthindex__first .
H20:   endidx__1 <= rr_type__linelengthindex__last .
H21:   foundtype__1 >= rr_type__rritemtype__first .
H22:   foundtype__1 <= rr_type__rritemtype__last .
H23:   foundtype__1 >= rr_type__rritemtype__first .
H24:   foundtype__1 <= rr_type__rritemtype__last .
H25:   endidx__1 >= rr_type__linelengthindex__first .
H26:   endidx__1 <= rr_type__linelengthindex__last .
H27:   begidx__1 >= rr_type__linelengthindex__first .
H28:   begidx__1 <= rr_type__linelengthindex__last .
H29:   foundtype__1 >= rr_type__rritemtype__first .
H30:   foundtype__1 <= rr_type__rritemtype__last .
H31:   not (foundtype__1 <> rr_type__number) .
H32:   0 >= long_long_integer__first .
H33:   0 <= long_long_integer__last .
H34:   begidx__1 >= rr_type__linelengthindex__first .
H35:   begidx__1 <= rr_type__linelengthindex__last .
H36:   endidx__1 >= rr_type__linelengthindex__first .
H37:   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 711:

procedure_parseserialnumber_6.
H1:    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))) .
H2:    zlength >= rr_type__linelengthindex__first .
H3:    zlength <= rr_type__linelengthindex__last .
H4:    0 >= unsigned_types__unsigned32__first .
H5:    0 <= unsigned_types__unsigned32__last .
H6:    1 >= rr_type__linelengthindex__first .
H7:    1 <= rr_type__linelengthindex__last .
H8:    1 >= rr_type__linelengthindex__first .
H9:    1 <= rr_type__linelengthindex__last .
H10:   zlength >= rr_type__linelengthindex__first .
H11:   zlength <= rr_type__linelengthindex__last .
H12:   1 <= zlength .
H13:   begidx__1 <= endidx__1 .
H14:   begidx__1 <= zlength .
H15:   endidx__1 <= zlength .
H16:   (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)))) .
H17:   begidx__1 >= rr_type__linelengthindex__first .
H18:   begidx__1 <= rr_type__linelengthindex__last .
H19:   endidx__1 >= rr_type__linelengthindex__first .
H20:   endidx__1 <= rr_type__linelengthindex__last .
H21:   foundtype__1 >= rr_type__rritemtype__first .
H22:   foundtype__1 <= rr_type__rritemtype__last .
H23:   foundtype__1 >= rr_type__rritemtype__first .
H24:   foundtype__1 <= rr_type__rritemtype__last .
H25:   endidx__1 >= rr_type__linelengthindex__first .
H26:   endidx__1 <= rr_type__linelengthindex__last .
H27:   begidx__1 >= rr_type__linelengthindex__first .
H28:   begidx__1 <= rr_type__linelengthindex__last .
H29:   foundtype__1 >= rr_type__rritemtype__first .
H30:   foundtype__1 <= rr_type__rritemtype__last .
H31:   not (foundtype__1 <> rr_type__number) .
H32:   0 >= long_long_integer__first .
H33:   0 <= long_long_integer__last .
H34:   begidx__1 >= rr_type__linelengthindex__first .
H35:   begidx__1 <= rr_type__linelengthindex__last .
H36:   endidx__1 >= rr_type__linelengthindex__first .
H37:   endidx__1 <= rr_type__linelengthindex__last .
H38:   endidx__1 >= integer__first .
H39:   endidx__1 <= integer__last .
H40:   begidx__1 >= integer__first .
H41:   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 712:

procedure_parseserialnumber_7.
H1:    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))) .
H2:    zlength >= rr_type__linelengthindex__first .
H3:    zlength <= rr_type__linelengthindex__last .
H4:    0 >= unsigned_types__unsigned32__first .
H5:    0 <= unsigned_types__unsigned32__last .
H6:    1 >= rr_type__linelengthindex__first .
H7:    1 <= rr_type__linelengthindex__last .
H8:    1 >= rr_type__linelengthindex__first .
H9:    1 <= rr_type__linelengthindex__last .
H10:   zlength >= rr_type__linelengthindex__first .
H11:   zlength <= rr_type__linelengthindex__last .
H12:   1 <= zlength .
H13:   begidx__1 <= endidx__1 .
H14:   begidx__1 <= zlength .
H15:   endidx__1 <= zlength .
H16:   (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)))) .
H17:   begidx__1 >= rr_type__linelengthindex__first .
H18:   begidx__1 <= rr_type__linelengthindex__last .
H19:   endidx__1 >= rr_type__linelengthindex__first .
H20:   endidx__1 <= rr_type__linelengthindex__last .
H21:   foundtype__1 >= rr_type__rritemtype__first .
H22:   foundtype__1 <= rr_type__rritemtype__last .
H23:   foundtype__1 >= rr_type__rritemtype__first .
H24:   foundtype__1 <= rr_type__rritemtype__last .
H25:   endidx__1 >= rr_type__linelengthindex__first .
H26:   endidx__1 <= rr_type__linelengthindex__last .
H27:   begidx__1 >= rr_type__linelengthindex__first .
H28:   begidx__1 <= rr_type__linelengthindex__last .
H29:   foundtype__1 >= rr_type__rritemtype__first .
H30:   foundtype__1 <= rr_type__rritemtype__last .
H31:   not (foundtype__1 <> rr_type__number) .
H32:   0 >= long_long_integer__first .
H33:   0 <= long_long_integer__last .
H34:   begidx__1 >= rr_type__linelengthindex__first .
H35:   begidx__1 <= rr_type__linelengthindex__last .
H36:   endidx__1 >= rr_type__linelengthindex__first .
H37:   endidx__1 <= rr_type__linelengthindex__last .
H38:   endidx__1 >= integer__first .
H39:   endidx__1 <= integer__last .
H40:   begidx__1 >= integer__first .
H41:   begidx__1 <= integer__last .
H42:   (begidx__1 <= endidx__1) -> ((endidx__1 >= integer__first) and (
           endidx__1 <= integer__last)) .
H43:   (begidx__1 <= endidx__1) -> ((begidx__1 >= integer__first) and (
           begidx__1 <= integer__last)) .
H44:   begidx__1 >= rr_type__linelengthindex__first .
H45:   begidx__1 <= rr_type__linelengthindex__last .
H46:   endidx__1 >= rr_type__linelengthindex__first .
H47:   endidx__1 <= rr_type__linelengthindex__last .
H48:   begidx__1 <= endidx__1 .
        ->
C1:    begidx__1 >= 1 .
C2:    0 >= 0 .
C3:    0 <= rr_type__soa_record_type__max_serial_val .
C4:    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))) .
C5:    zlength >= rr_type__linelengthindex__first .
C6:    zlength <= rr_type__linelengthindex__last .
C7:    begidx__1 >= integer__first .
C8:    begidx__1 <= integer__last .
C9:    begidx__1 >= begidx__1 .
C10:   begidx__1 <= endidx__1 .
C11:   endidx__1 >= rr_type__linelengthindex__first .
C12:   endidx__1 <= rr_type__linelengthindex__last .
 

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

procedure_parseserialnumber_8.
H1:    begidx >= 1 .
H2:    tmpval >= 0 .
H3:    tmpval <= rr_type__soa_record_type__max_serial_val .
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:    loop__1__i >= integer__first .
H8:    loop__1__i <= integer__last .
H9:    loop__1__i >= begidx .
H10:   loop__1__i <= endidx__entry__loop__1 .
H11:   endidx__entry__loop__1 >= rr_type__linelengthindex__first .
H12:   endidx__entry__loop__1 <= rr_type__linelengthindex__last .
H13:   (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus >= 
           unsigned_types__unsigned32__first .
H14:   (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus <= 
           unsigned_types__unsigned32__last .
H15:   loop__1__i >= rr_type__linelengthindex__first .
H16:   loop__1__i <= rr_type__linelengthindex__last .
H17:   (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus >= 
           unsigned_types__unsigned32__first .
H18:   (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus <= 
           unsigned_types__unsigned32__last .
H19:   tmpval >= long_long_integer__first .
H20:   tmpval <= long_long_integer__last .
H21:   10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus >= 
           long_long_integer__first .
H22:   10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus <= 
           long_long_integer__last .
H23:   (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus >= 
           long_long_integer__first .
H24:   (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus <= 
           long_long_integer__last .
H25:   10 * tmpval >= long_long_integer__base__first .
H26:   10 * tmpval <= long_long_integer__base__last .
H27:   10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus >= 
           long_long_integer__first .
H28:   10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus <= 
           long_long_integer__last .
H29:   not (10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus > 
           rr_type__soa_record_type__max_serial_val) .
H30:   not (loop__1__i = endidx__entry__loop__1) .
        ->
C1:    begidx >= 1 .
C2:    10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus >= 0 .
C3:    10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus <= 
           rr_type__soa_record_type__max_serial_val .
C4:    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))) .
C5:    zlength >= rr_type__linelengthindex__first .
C6:    zlength <= rr_type__linelengthindex__last .
C7:    loop__1__i + 1 >= integer__first .
C8:    loop__1__i + 1 <= integer__last .
C9:    loop__1__i + 1 >= begidx .
C10:   loop__1__i + 1 <= endidx__entry__loop__1 .
C11:   endidx__entry__loop__1 >= rr_type__linelengthindex__first .
C12:   endidx__entry__loop__1 <= rr_type__linelengthindex__last .
 

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

procedure_parseserialnumber_9.
H1:    begidx >= 1 .
H2:    tmpval >= 0 .
H3:    tmpval <= rr_type__soa_record_type__max_serial_val .
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:    loop__1__i >= integer__first .
H8:    loop__1__i <= integer__last .
H9:    loop__1__i >= begidx .
H10:   loop__1__i <= endidx__entry__loop__1 .
H11:   endidx__entry__loop__1 >= rr_type__linelengthindex__first .
H12:   endidx__entry__loop__1 <= rr_type__linelengthindex__last .
        ->
C1:    (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus >= 
           unsigned_types__unsigned32__first .
C2:    (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus <= 
           unsigned_types__unsigned32__last .
C3:    loop__1__i >= rr_type__linelengthindex__first .
C4:    loop__1__i <= rr_type__linelengthindex__last .
 

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

procedure_parseserialnumber_10.
H1:    begidx >= 1 .
H2:    tmpval >= 0 .
H3:    tmpval <= rr_type__soa_record_type__max_serial_val .
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:    loop__1__i >= integer__first .
H8:    loop__1__i <= integer__last .
H9:    loop__1__i >= begidx .
H10:   loop__1__i <= endidx__entry__loop__1 .
H11:   endidx__entry__loop__1 >= rr_type__linelengthindex__first .
H12:   endidx__entry__loop__1 <= rr_type__linelengthindex__last .
H13:   (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus >= 
           unsigned_types__unsigned32__first .
H14:   (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus <= 
           unsigned_types__unsigned32__last .
H15:   loop__1__i >= rr_type__linelengthindex__first .
H16:   loop__1__i <= rr_type__linelengthindex__last .
H17:   (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus >= 
           unsigned_types__unsigned32__first .
H18:   (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus <= 
           unsigned_types__unsigned32__last .
H19:   tmpval >= long_long_integer__first .
H20:   tmpval <= long_long_integer__last .
        ->
C1:    10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus >= 
           long_long_integer__first .
C2:    10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus <= 
           long_long_integer__last .
C3:    (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus >= 
           long_long_integer__first .
C4:    (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus <= 
           long_long_integer__last .
C5:    10 * tmpval >= long_long_integer__base__first .
C6:    10 * tmpval <= long_long_integer__base__last .
 

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

procedure_parseserialnumber_11.
H1:    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))) .
H2:    zlength >= rr_type__linelengthindex__first .
H3:    zlength <= rr_type__linelengthindex__last .
H4:    0 >= unsigned_types__unsigned32__first .
H5:    0 <= unsigned_types__unsigned32__last .
H6:    1 >= rr_type__linelengthindex__first .
H7:    1 <= rr_type__linelengthindex__last .
H8:    1 >= rr_type__linelengthindex__first .
H9:    1 <= rr_type__linelengthindex__last .
H10:   zlength >= rr_type__linelengthindex__first .
H11:   zlength <= rr_type__linelengthindex__last .
H12:   1 <= zlength .
H13:   begidx__1 <= endidx__1 .
H14:   begidx__1 <= zlength .
H15:   endidx__1 <= zlength .
H16:   (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)))) .
H17:   begidx__1 >= rr_type__linelengthindex__first .
H18:   begidx__1 <= rr_type__linelengthindex__last .
H19:   endidx__1 >= rr_type__linelengthindex__first .
H20:   endidx__1 <= rr_type__linelengthindex__last .
H21:   foundtype__1 >= rr_type__rritemtype__first .
H22:   foundtype__1 <= rr_type__rritemtype__last .
H23:   foundtype__1 >= rr_type__rritemtype__first .
H24:   foundtype__1 <= rr_type__rritemtype__last .
H25:   endidx__1 >= rr_type__linelengthindex__first .
H26:   endidx__1 <= rr_type__linelengthindex__last .
H27:   begidx__1 >= rr_type__linelengthindex__first .
H28:   begidx__1 <= rr_type__linelengthindex__last .
H29:   foundtype__1 >= rr_type__rritemtype__first .
H30:   foundtype__1 <= rr_type__rritemtype__last .
H31:   not (foundtype__1 <> rr_type__number) .
H32:   0 >= long_long_integer__first .
H33:   0 <= long_long_integer__last .
H34:   begidx__1 >= rr_type__linelengthindex__first .
H35:   begidx__1 <= rr_type__linelengthindex__last .
H36:   endidx__1 >= rr_type__linelengthindex__first .
H37:   endidx__1 <= rr_type__linelengthindex__last .
H38:   endidx__1 >= integer__first .
H39:   endidx__1 <= integer__last .
H40:   begidx__1 >= integer__first .
H41:   begidx__1 <= integer__last .
H42:   (begidx__1 <= endidx__1) -> ((endidx__1 >= integer__first) and (
           endidx__1 <= integer__last)) .
H43:   (begidx__1 <= endidx__1) -> ((begidx__1 >= integer__first) and (
           begidx__1 <= integer__last)) .
H44:   begidx__1 >= rr_type__linelengthindex__first .
H45:   begidx__1 <= rr_type__linelengthindex__last .
H46:   endidx__1 >= rr_type__linelengthindex__first .
H47:   endidx__1 <= rr_type__linelengthindex__last .
H48:   not (begidx__1 <= endidx__1) .
H49:   0 >= long_long_integer__first .
H50:   0 <= long_long_integer__last .
H51:   not (0 > rr_type__soa_record_type__max_serial_val) .
H52:   0 >= long_long_integer__first .
H53:   0 <= long_long_integer__last .
        ->
C1:    0 >= unsigned_types__unsigned32__first .
C2:    0 <= unsigned_types__unsigned32__last .
C3:    0 >= unsigned_types__unsigned32__first .
C4:    0 <= unsigned_types__unsigned32__last .
 

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

procedure_parseserialnumber_12.
H1:    begidx >= 1 .
H2:    tmpval >= 0 .
H3:    tmpval <= rr_type__soa_record_type__max_serial_val .
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:    loop__1__i >= integer__first .
H8:    loop__1__i <= integer__last .
H9:    loop__1__i >= begidx .
H10:   loop__1__i <= endidx__entry__loop__1 .
H11:   endidx__entry__loop__1 >= rr_type__linelengthindex__first .
H12:   endidx__entry__loop__1 <= rr_type__linelengthindex__last .
H13:   (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus >= 
           unsigned_types__unsigned32__first .
H14:   (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus <= 
           unsigned_types__unsigned32__last .
H15:   loop__1__i >= rr_type__linelengthindex__first .
H16:   loop__1__i <= rr_type__linelengthindex__last .
H17:   (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus >= 
           unsigned_types__unsigned32__first .
H18:   (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus <= 
           unsigned_types__unsigned32__last .
H19:   tmpval >= long_long_integer__first .
H20:   tmpval <= long_long_integer__last .
H21:   10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus >= 
           long_long_integer__first .
H22:   10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus <= 
           long_long_integer__last .
H23:   (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus >= 
           long_long_integer__first .
H24:   (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus <= 
           long_long_integer__last .
H25:   10 * tmpval >= long_long_integer__base__first .
H26:   10 * tmpval <= long_long_integer__base__last .
H27:   10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus >= 
           long_long_integer__first .
H28:   10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus <= 
           long_long_integer__last .
H29:   10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus > 
           rr_type__soa_record_type__max_serial_val .
H30:   10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus >= 
           long_long_integer__first .
H31:   10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus <= 
           long_long_integer__last .
H32:   not (10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus > 
           rr_type__soa_record_type__max_serial_val) .
H33:   10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus >= 
           long_long_integer__first .
H34:   10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus <= 
           long_long_integer__last .
        ->
C1:    10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus >= 
           unsigned_types__unsigned32__first .
C2:    10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus <= 
           unsigned_types__unsigned32__last .
C3:    10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus >= 
           unsigned_types__unsigned32__first .
C4:    10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus <= 
           unsigned_types__unsigned32__last .
 

procedure_parseserialnumber_13.
H1:    begidx >= 1 .
H2:    tmpval >= 0 .
H3:    tmpval <= rr_type__soa_record_type__max_serial_val .
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:    loop__1__i >= integer__first .
H8:    loop__1__i <= integer__last .
H9:    loop__1__i >= begidx .
H10:   loop__1__i <= endidx__entry__loop__1 .
H11:   endidx__entry__loop__1 >= rr_type__linelengthindex__first .
H12:   endidx__entry__loop__1 <= rr_type__linelengthindex__last .
H13:   (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus >= 
           unsigned_types__unsigned32__first .
H14:   (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus <= 
           unsigned_types__unsigned32__last .
H15:   loop__1__i >= rr_type__linelengthindex__first .
H16:   loop__1__i <= rr_type__linelengthindex__last .
H17:   (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus >= 
           unsigned_types__unsigned32__first .
H18:   (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus <= 
           unsigned_types__unsigned32__last .
H19:   tmpval >= long_long_integer__first .
H20:   tmpval <= long_long_integer__last .
H21:   10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus >= 
           long_long_integer__first .
H22:   10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus <= 
           long_long_integer__last .
H23:   (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus >= 
           long_long_integer__first .
H24:   (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus <= 
           long_long_integer__last .
H25:   10 * tmpval >= long_long_integer__base__first .
H26:   10 * tmpval <= long_long_integer__base__last .
H27:   10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus >= 
           long_long_integer__first .
H28:   10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus <= 
           long_long_integer__last .
H29:   not (10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus > 
           rr_type__soa_record_type__max_serial_val) .
H30:   loop__1__i = endidx__entry__loop__1 .
H31:   10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus >= 
           long_long_integer__first .
H32:   10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus <= 
           long_long_integer__last .
H33:   not (10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus > 
           rr_type__soa_record_type__max_serial_val) .
H34:   10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus >= 
           long_long_integer__first .
H35:   10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus <= 
           long_long_integer__last .
        ->
C1:    10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus >= 
           unsigned_types__unsigned32__first .
C2:    10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus <= 
           unsigned_types__unsigned32__last .
C3:    10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus >= 
           unsigned_types__unsigned32__first .
C4:    10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
           unsigned_types__unsigned32__modulus <= 
           unsigned_types__unsigned32__last .
 

For path(s) from start to finish:

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


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


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


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

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


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


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


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


