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

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


      procedure process_first_line_of_record.ProcessFirstLineOfRecord




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

procedure_processfirstlineofrecord_1.
H1:    lastpos >= 1 .
H2:    lastpos <= rr_type__linelengthindex__last .
H3:    currentrecordtype >= dns_types__query_type__first .
H4:    currentrecordtype <= dns_types__query_type__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentorigin, [i___1]) >= character__first) and (element(
           currentorigin, [i___1]) <= character__last))) .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentowner, [i___1]) >= character__first) and (element(
           currentowner, [i___1]) <= character__last))) .
H7:    currentttl >= unsigned_types__unsigned32__first .
H8:    currentttl <= unsigned_types__unsigned32__last .
H9:    currentclass >= rr_type__classtype__first .
H10:   currentclass <= rr_type__classtype__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           currentline, [i___1]) >= character__first) and (element(
           currentline, [i___1]) <= character__last))) .
H12:   lastpos >= rr_type__linelengthindex__first .
H13:   lastpos <= rr_type__linelengthindex__last .
H14:   linecount >= unsigned_types__unsigned32__first .
H15:   linecount <= unsigned_types__unsigned32__last .
        ->
C1:    0 >= unsigned_types__unsigned32__first .
C2:    0 <= unsigned_types__unsigned32__last .
 

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

procedure_processfirstlineofrecord_2.
H1:    lastpos >= 1 .
H2:    lastpos <= rr_type__linelengthindex__last .
H3:    currentrecordtype >= dns_types__query_type__first .
H4:    currentrecordtype <= dns_types__query_type__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentorigin, [i___1]) >= character__first) and (element(
           currentorigin, [i___1]) <= character__last))) .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentowner, [i___1]) >= character__first) and (element(
           currentowner, [i___1]) <= character__last))) .
H7:    currentttl >= unsigned_types__unsigned32__first .
H8:    currentttl <= unsigned_types__unsigned32__last .
H9:    currentclass >= rr_type__classtype__first .
H10:   currentclass <= rr_type__classtype__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           currentline, [i___1]) >= character__first) and (element(
           currentline, [i___1]) <= character__last))) .
H12:   lastpos >= rr_type__linelengthindex__first .
H13:   lastpos <= rr_type__linelengthindex__last .
H14:   linecount >= unsigned_types__unsigned32__first .
H15:   linecount <= unsigned_types__unsigned32__last .
H16:   0 >= unsigned_types__unsigned32__first .
H17:   0 <= unsigned_types__unsigned32__last .
H18:   currentrecordtype = dns_types__a .
        ->
C1:    lastpos >= rr_type__linelengthindex__first .
C2:    lastpos <= rr_type__linelengthindex__last .
 

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

procedure_processfirstlineofrecord_3.
H1:    lastpos >= 1 .
H2:    lastpos <= rr_type__linelengthindex__last .
H3:    currentrecordtype >= dns_types__query_type__first .
H4:    currentrecordtype <= dns_types__query_type__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentorigin, [i___1]) >= character__first) and (element(
           currentorigin, [i___1]) <= character__last))) .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentowner, [i___1]) >= character__first) and (element(
           currentowner, [i___1]) <= character__last))) .
H7:    currentttl >= unsigned_types__unsigned32__first .
H8:    currentttl <= unsigned_types__unsigned32__last .
H9:    currentclass >= rr_type__classtype__first .
H10:   currentclass <= rr_type__classtype__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           currentline, [i___1]) >= character__first) and (element(
           currentline, [i___1]) <= character__last))) .
H12:   lastpos >= rr_type__linelengthindex__first .
H13:   lastpos <= rr_type__linelengthindex__last .
H14:   linecount >= unsigned_types__unsigned32__first .
H15:   linecount <= unsigned_types__unsigned32__last .
H16:   0 >= unsigned_types__unsigned32__first .
H17:   0 <= unsigned_types__unsigned32__last .
H18:   currentrecordtype = dns_types__a .
H19:   lastpos >= rr_type__linelengthindex__first .
H20:   lastpos <= rr_type__linelengthindex__last .
H21:   currentipv4__1 >= unsigned_types__unsigned32__first .
H22:   currentipv4__1 <= unsigned_types__unsigned32__last .
        ->
C1:    currentipv4__1 >= unsigned_types__unsigned32__first .
C2:    currentipv4__1 <= unsigned_types__unsigned32__last .
 

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

procedure_processfirstlineofrecord_4.
H1:    lastpos >= 1 .
H2:    lastpos <= rr_type__linelengthindex__last .
H3:    currentrecordtype >= dns_types__query_type__first .
H4:    currentrecordtype <= dns_types__query_type__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentorigin, [i___1]) >= character__first) and (element(
           currentorigin, [i___1]) <= character__last))) .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentowner, [i___1]) >= character__first) and (element(
           currentowner, [i___1]) <= character__last))) .
H7:    currentttl >= unsigned_types__unsigned32__first .
H8:    currentttl <= unsigned_types__unsigned32__last .
H9:    currentclass >= rr_type__classtype__first .
H10:   currentclass <= rr_type__classtype__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           currentline, [i___1]) >= character__first) and (element(
           currentline, [i___1]) <= character__last))) .
H12:   lastpos >= rr_type__linelengthindex__first .
H13:   lastpos <= rr_type__linelengthindex__last .
H14:   linecount >= unsigned_types__unsigned32__first .
H15:   linecount <= unsigned_types__unsigned32__last .
H16:   0 >= unsigned_types__unsigned32__first .
H17:   0 <= unsigned_types__unsigned32__last .
H18:   currentrecordtype = dns_types__a .
H19:   lastpos >= rr_type__linelengthindex__first .
H20:   lastpos <= rr_type__linelengthindex__last .
H21:   currentipv4__1 >= unsigned_types__unsigned32__first .
H22:   currentipv4__1 <= unsigned_types__unsigned32__last .
H23:   currentipv4__1 >= unsigned_types__unsigned32__first .
H24:   currentipv4__1 <= unsigned_types__unsigned32__last .
H25:   success__1 .
H26:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           rr_type__convertdomainnametowire(currentowner), [
           i___1]) >= character__first) and (element(
           rr_type__convertdomainnametowire(currentowner), [
           i___1]) <= character__last))) .
H27:   for_all(i_: integer, ((i_ >= 
           rr_type__domainnamestringtypeindex__first) and (
           i_ <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           rr_type__convertdomainnametowire(currentowner), [
           i_]) >= 0) and (element(
           rr_type__convertdomainnametowire(currentowner), [
           i_]) <= 255))) .
H28:   currentipv4__1 >= unsigned_types__unsigned32__first .
H29:   currentipv4__1 <= unsigned_types__unsigned32__last .
        ->
C1:    currentipv4__1 >= unsigned_types__unsigned32__first .
C2:    currentipv4__1 <= unsigned_types__unsigned32__last .
C3:    currentclass >= rr_type__classtype__first .
C4:    currentclass <= rr_type__classtype__last .
C5:    currentttl >= unsigned_types__unsigned32__first .
C6:    currentttl <= unsigned_types__unsigned32__last .
 

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

procedure_processfirstlineofrecord_5.
H1:    lastpos >= 1 .
H2:    lastpos <= rr_type__linelengthindex__last .
H3:    currentrecordtype >= dns_types__query_type__first .
H4:    currentrecordtype <= dns_types__query_type__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentorigin, [i___1]) >= character__first) and (element(
           currentorigin, [i___1]) <= character__last))) .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentowner, [i___1]) >= character__first) and (element(
           currentowner, [i___1]) <= character__last))) .
H7:    currentttl >= unsigned_types__unsigned32__first .
H8:    currentttl <= unsigned_types__unsigned32__last .
H9:    currentclass >= rr_type__classtype__first .
H10:   currentclass <= rr_type__classtype__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           currentline, [i___1]) >= character__first) and (element(
           currentline, [i___1]) <= character__last))) .
H12:   lastpos >= rr_type__linelengthindex__first .
H13:   lastpos <= rr_type__linelengthindex__last .
H14:   linecount >= unsigned_types__unsigned32__first .
H15:   linecount <= unsigned_types__unsigned32__last .
H16:   0 >= unsigned_types__unsigned32__first .
H17:   0 <= unsigned_types__unsigned32__last .
H18:   currentrecordtype = dns_types__aaaa .
        ->
C1:    lastpos >= rr_type__linelengthindex__first .
C2:    lastpos <= rr_type__linelengthindex__last .
 

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

procedure_processfirstlineofrecord_6.
H1:    lastpos >= 1 .
H2:    lastpos <= rr_type__linelengthindex__last .
H3:    currentrecordtype >= dns_types__query_type__first .
H4:    currentrecordtype <= dns_types__query_type__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentorigin, [i___1]) >= character__first) and (element(
           currentorigin, [i___1]) <= character__last))) .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentowner, [i___1]) >= character__first) and (element(
           currentowner, [i___1]) <= character__last))) .
H7:    currentttl >= unsigned_types__unsigned32__first .
H8:    currentttl <= unsigned_types__unsigned32__last .
H9:    currentclass >= rr_type__classtype__first .
H10:   currentclass <= rr_type__classtype__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           currentline, [i___1]) >= character__first) and (element(
           currentline, [i___1]) <= character__last))) .
H12:   lastpos >= rr_type__linelengthindex__first .
H13:   lastpos <= rr_type__linelengthindex__last .
H14:   linecount >= unsigned_types__unsigned32__first .
H15:   linecount <= unsigned_types__unsigned32__last .
H16:   0 >= unsigned_types__unsigned32__first .
H17:   0 <= unsigned_types__unsigned32__last .
H18:   currentrecordtype = dns_types__aaaa .
H19:   lastpos >= rr_type__linelengthindex__first .
H20:   lastpos <= rr_type__linelengthindex__last .
H21:   for_all(i___1: integer, ((i___1 >= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first) and (
           i___1 <= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__last)) -> ((element(
           currentipv6__3, [i___1]) >= 
           unsigned_types__unsigned16__first) and (element(
           currentipv6__3, [i___1]) <= 
           unsigned_types__unsigned16__last))) .
H22:   success__3 .
H23:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           rr_type__convertdomainnametowire(currentowner), [
           i___1]) >= character__first) and (element(
           rr_type__convertdomainnametowire(currentowner), [
           i___1]) <= character__last))) .
H24:   for_all(i_: integer, ((i_ >= 
           rr_type__domainnamestringtypeindex__first) and (
           i_ <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           rr_type__convertdomainnametowire(currentowner), [
           i_]) >= 0) and (element(
           rr_type__convertdomainnametowire(currentowner), [
           i_]) <= 255))) .
H25:   for_all(i___1: integer, ((i___1 >= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__first) and (
           i___1 <= 
           rr_type__aaaa_record_type__ipv6addrtypeindex__last)) -> ((element(
           currentipv6__3, [i___1]) >= 
           unsigned_types__unsigned16__first) and (element(
           currentipv6__3, [i___1]) <= 
           unsigned_types__unsigned16__last))) .
        ->
C1:    currentclass >= rr_type__classtype__first .
C2:    currentclass <= rr_type__classtype__last .
C3:    currentttl >= unsigned_types__unsigned32__first .
C4:    currentttl <= unsigned_types__unsigned32__last .
 

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

procedure_processfirstlineofrecord_7.
H1:    lastpos >= 1 .
H2:    lastpos <= rr_type__linelengthindex__last .
H3:    currentrecordtype >= dns_types__query_type__first .
H4:    currentrecordtype <= dns_types__query_type__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentorigin, [i___1]) >= character__first) and (element(
           currentorigin, [i___1]) <= character__last))) .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentowner, [i___1]) >= character__first) and (element(
           currentowner, [i___1]) <= character__last))) .
H7:    currentttl >= unsigned_types__unsigned32__first .
H8:    currentttl <= unsigned_types__unsigned32__last .
H9:    currentclass >= rr_type__classtype__first .
H10:   currentclass <= rr_type__classtype__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           currentline, [i___1]) >= character__first) and (element(
           currentline, [i___1]) <= character__last))) .
H12:   lastpos >= rr_type__linelengthindex__first .
H13:   lastpos <= rr_type__linelengthindex__last .
H14:   linecount >= unsigned_types__unsigned32__first .
H15:   linecount <= unsigned_types__unsigned32__last .
H16:   0 >= unsigned_types__unsigned32__first .
H17:   0 <= unsigned_types__unsigned32__last .
H18:   currentrecordtype = dns_types__cname .
        ->
C1:    lastpos >= rr_type__linelengthindex__first .
C2:    lastpos <= rr_type__linelengthindex__last .
 

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

procedure_processfirstlineofrecord_8.
H1:    lastpos >= 1 .
H2:    lastpos <= rr_type__linelengthindex__last .
H3:    currentrecordtype >= dns_types__query_type__first .
H4:    currentrecordtype <= dns_types__query_type__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentorigin, [i___1]) >= character__first) and (element(
           currentorigin, [i___1]) <= character__last))) .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentowner, [i___1]) >= character__first) and (element(
           currentowner, [i___1]) <= character__last))) .
H7:    currentttl >= unsigned_types__unsigned32__first .
H8:    currentttl <= unsigned_types__unsigned32__last .
H9:    currentclass >= rr_type__classtype__first .
H10:   currentclass <= rr_type__classtype__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           currentline, [i___1]) >= character__first) and (element(
           currentline, [i___1]) <= character__last))) .
H12:   lastpos >= rr_type__linelengthindex__first .
H13:   lastpos <= rr_type__linelengthindex__last .
H14:   linecount >= unsigned_types__unsigned32__first .
H15:   linecount <= unsigned_types__unsigned32__last .
H16:   0 >= unsigned_types__unsigned32__first .
H17:   0 <= unsigned_types__unsigned32__last .
H18:   currentrecordtype = dns_types__cname .
H19:   lastpos >= rr_type__linelengthindex__first .
H20:   lastpos <= rr_type__linelengthindex__last .
H21:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__5, [i___1]) >= character__first) and (element(
           currentdomainname__5, [i___1]) <= character__last))) .
H22:   success__5 .
H23:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__5, [i___1]) >= character__first) and (element(
           currentdomainname__5, [i___1]) <= character__last))) .
        ->
C1:    linecount >= unsigned_types__unsigned32__first .
C2:    linecount <= unsigned_types__unsigned32__last .
C3:    lastpos >= rr_type__linelengthindex__first .
C4:    lastpos <= rr_type__linelengthindex__last .
 

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

procedure_processfirstlineofrecord_9.
H1:    lastpos >= 1 .
H2:    lastpos <= rr_type__linelengthindex__last .
H3:    currentrecordtype >= dns_types__query_type__first .
H4:    currentrecordtype <= dns_types__query_type__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentorigin, [i___1]) >= character__first) and (element(
           currentorigin, [i___1]) <= character__last))) .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentowner, [i___1]) >= character__first) and (element(
           currentowner, [i___1]) <= character__last))) .
H7:    currentttl >= unsigned_types__unsigned32__first .
H8:    currentttl <= unsigned_types__unsigned32__last .
H9:    currentclass >= rr_type__classtype__first .
H10:   currentclass <= rr_type__classtype__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           currentline, [i___1]) >= character__first) and (element(
           currentline, [i___1]) <= character__last))) .
H12:   lastpos >= rr_type__linelengthindex__first .
H13:   lastpos <= rr_type__linelengthindex__last .
H14:   linecount >= unsigned_types__unsigned32__first .
H15:   linecount <= unsigned_types__unsigned32__last .
H16:   0 >= unsigned_types__unsigned32__first .
H17:   0 <= unsigned_types__unsigned32__last .
H18:   currentrecordtype = dns_types__cname .
H19:   lastpos >= rr_type__linelengthindex__first .
H20:   lastpos <= rr_type__linelengthindex__last .
H21:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__5, [i___1]) >= character__first) and (element(
           currentdomainname__5, [i___1]) <= character__last))) .
H22:   success__5 .
H23:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__5, [i___1]) >= character__first) and (element(
           currentdomainname__5, [i___1]) <= character__last))) .
H24:   linecount >= unsigned_types__unsigned32__first .
H25:   linecount <= unsigned_types__unsigned32__last .
H26:   lastpos >= rr_type__linelengthindex__first .
H27:   lastpos <= rr_type__linelengthindex__last .
H28:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__6, [i___1]) >= character__first) and (element(
           currentdomainname__6, [i___1]) <= character__last))) .
H29:   success__6 .
H30:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           rr_type__convertdomainnametowire(currentowner), [
           i___1]) >= character__first) and (element(
           rr_type__convertdomainnametowire(currentowner), [
           i___1]) <= character__last))) .
H31:   for_all(i_: integer, ((i_ >= 
           rr_type__domainnamestringtypeindex__first) and (
           i_ <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           rr_type__convertdomainnametowire(currentowner), [
           i_]) >= 0) and (element(
           rr_type__convertdomainnametowire(currentowner), [
           i_]) <= 255))) .
H32:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__6, [i___1]) >= character__first) and (element(
           currentdomainname__6, [i___1]) <= character__last))) .
        ->
C1:    currentclass >= rr_type__classtype__first .
C2:    currentclass <= rr_type__classtype__last .
C3:    currentttl >= unsigned_types__unsigned32__first .
C4:    currentttl <= unsigned_types__unsigned32__last .
 

procedure_processfirstlineofrecord_10.
H1:    lastpos >= 1 .
H2:    lastpos <= rr_type__linelengthindex__last .
H3:    currentrecordtype >= dns_types__query_type__first .
H4:    currentrecordtype <= dns_types__query_type__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentorigin, [i___1]) >= character__first) and (element(
           currentorigin, [i___1]) <= character__last))) .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentowner, [i___1]) >= character__first) and (element(
           currentowner, [i___1]) <= character__last))) .
H7:    currentttl >= unsigned_types__unsigned32__first .
H8:    currentttl <= unsigned_types__unsigned32__last .
H9:    currentclass >= rr_type__classtype__first .
H10:   currentclass <= rr_type__classtype__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           currentline, [i___1]) >= character__first) and (element(
           currentline, [i___1]) <= character__last))) .
H12:   lastpos >= rr_type__linelengthindex__first .
H13:   lastpos <= rr_type__linelengthindex__last .
H14:   linecount >= unsigned_types__unsigned32__first .
H15:   linecount <= unsigned_types__unsigned32__last .
H16:   0 >= unsigned_types__unsigned32__first .
H17:   0 <= unsigned_types__unsigned32__last .
H18:   currentrecordtype = dns_types__cname .
H19:   lastpos >= rr_type__linelengthindex__first .
H20:   lastpos <= rr_type__linelengthindex__last .
H21:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__5, [i___1]) >= character__first) and (element(
           currentdomainname__5, [i___1]) <= character__last))) .
H22:   not success__5 .
H23:   success__5 .
H24:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           rr_type__convertdomainnametowire(currentowner), [
           i___1]) >= character__first) and (element(
           rr_type__convertdomainnametowire(currentowner), [
           i___1]) <= character__last))) .
H25:   for_all(i_: integer, ((i_ >= 
           rr_type__domainnamestringtypeindex__first) and (
           i_ <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           rr_type__convertdomainnametowire(currentowner), [
           i_]) >= 0) and (element(
           rr_type__convertdomainnametowire(currentowner), [
           i_]) <= 255))) .
H26:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__5, [i___1]) >= character__first) and (element(
           currentdomainname__5, [i___1]) <= character__last))) .
        ->
C1:    currentclass >= rr_type__classtype__first .
C2:    currentclass <= rr_type__classtype__last .
C3:    currentttl >= unsigned_types__unsigned32__first .
C4:    currentttl <= unsigned_types__unsigned32__last .
 

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

procedure_processfirstlineofrecord_11.
H1:    lastpos >= 1 .
H2:    lastpos <= rr_type__linelengthindex__last .
H3:    currentrecordtype >= dns_types__query_type__first .
H4:    currentrecordtype <= dns_types__query_type__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentorigin, [i___1]) >= character__first) and (element(
           currentorigin, [i___1]) <= character__last))) .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentowner, [i___1]) >= character__first) and (element(
           currentowner, [i___1]) <= character__last))) .
H7:    currentttl >= unsigned_types__unsigned32__first .
H8:    currentttl <= unsigned_types__unsigned32__last .
H9:    currentclass >= rr_type__classtype__first .
H10:   currentclass <= rr_type__classtype__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           currentline, [i___1]) >= character__first) and (element(
           currentline, [i___1]) <= character__last))) .
H12:   lastpos >= rr_type__linelengthindex__first .
H13:   lastpos <= rr_type__linelengthindex__last .
H14:   linecount >= unsigned_types__unsigned32__first .
H15:   linecount <= unsigned_types__unsigned32__last .
H16:   0 >= unsigned_types__unsigned32__first .
H17:   0 <= unsigned_types__unsigned32__last .
H18:   currentrecordtype = dns_types__mx .
        ->
C1:    lastpos >= rr_type__linelengthindex__first .
C2:    lastpos <= rr_type__linelengthindex__last .
 

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

procedure_processfirstlineofrecord_12.
H1:    lastpos >= 1 .
H2:    lastpos <= rr_type__linelengthindex__last .
H3:    currentrecordtype >= dns_types__query_type__first .
H4:    currentrecordtype <= dns_types__query_type__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentorigin, [i___1]) >= character__first) and (element(
           currentorigin, [i___1]) <= character__last))) .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentowner, [i___1]) >= character__first) and (element(
           currentowner, [i___1]) <= character__last))) .
H7:    currentttl >= unsigned_types__unsigned32__first .
H8:    currentttl <= unsigned_types__unsigned32__last .
H9:    currentclass >= rr_type__classtype__first .
H10:   currentclass <= rr_type__classtype__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           currentline, [i___1]) >= character__first) and (element(
           currentline, [i___1]) <= character__last))) .
H12:   lastpos >= rr_type__linelengthindex__first .
H13:   lastpos <= rr_type__linelengthindex__last .
H14:   linecount >= unsigned_types__unsigned32__first .
H15:   linecount <= unsigned_types__unsigned32__last .
H16:   0 >= unsigned_types__unsigned32__first .
H17:   0 <= unsigned_types__unsigned32__last .
H18:   currentrecordtype = dns_types__mx .
H19:   lastpos >= rr_type__linelengthindex__first .
H20:   lastpos <= rr_type__linelengthindex__last .
H21:   currentpref__8 >= unsigned_types__unsigned16__first .
H22:   currentpref__8 <= unsigned_types__unsigned16__last .
H23:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__8, [i___1]) >= character__first) and (element(
           currentdomainname__8, [i___1]) <= character__last))) .
        ->
C1:    currentpref__8 >= unsigned_types__unsigned16__first .
C2:    currentpref__8 <= unsigned_types__unsigned16__last .
 

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

procedure_processfirstlineofrecord_13.
H1:    lastpos >= 1 .
H2:    lastpos <= rr_type__linelengthindex__last .
H3:    currentrecordtype >= dns_types__query_type__first .
H4:    currentrecordtype <= dns_types__query_type__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentorigin, [i___1]) >= character__first) and (element(
           currentorigin, [i___1]) <= character__last))) .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentowner, [i___1]) >= character__first) and (element(
           currentowner, [i___1]) <= character__last))) .
H7:    currentttl >= unsigned_types__unsigned32__first .
H8:    currentttl <= unsigned_types__unsigned32__last .
H9:    currentclass >= rr_type__classtype__first .
H10:   currentclass <= rr_type__classtype__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           currentline, [i___1]) >= character__first) and (element(
           currentline, [i___1]) <= character__last))) .
H12:   lastpos >= rr_type__linelengthindex__first .
H13:   lastpos <= rr_type__linelengthindex__last .
H14:   linecount >= unsigned_types__unsigned32__first .
H15:   linecount <= unsigned_types__unsigned32__last .
H16:   0 >= unsigned_types__unsigned32__first .
H17:   0 <= unsigned_types__unsigned32__last .
H18:   currentrecordtype = dns_types__mx .
H19:   lastpos >= rr_type__linelengthindex__first .
H20:   lastpos <= rr_type__linelengthindex__last .
H21:   currentpref__8 >= unsigned_types__unsigned16__first .
H22:   currentpref__8 <= unsigned_types__unsigned16__last .
H23:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__8, [i___1]) >= character__first) and (element(
           currentdomainname__8, [i___1]) <= character__last))) .
H24:   currentpref__8 >= unsigned_types__unsigned16__first .
H25:   currentpref__8 <= unsigned_types__unsigned16__last .
H26:   success__8 .
H27:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__8, [i___1]) >= character__first) and (element(
           currentdomainname__8, [i___1]) <= character__last))) .
        ->
C1:    linecount >= unsigned_types__unsigned32__first .
C2:    linecount <= unsigned_types__unsigned32__last .
C3:    lastpos >= rr_type__linelengthindex__first .
C4:    lastpos <= rr_type__linelengthindex__last .
 

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

procedure_processfirstlineofrecord_14.
H1:    lastpos >= 1 .
H2:    lastpos <= rr_type__linelengthindex__last .
H3:    currentrecordtype >= dns_types__query_type__first .
H4:    currentrecordtype <= dns_types__query_type__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentorigin, [i___1]) >= character__first) and (element(
           currentorigin, [i___1]) <= character__last))) .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentowner, [i___1]) >= character__first) and (element(
           currentowner, [i___1]) <= character__last))) .
H7:    currentttl >= unsigned_types__unsigned32__first .
H8:    currentttl <= unsigned_types__unsigned32__last .
H9:    currentclass >= rr_type__classtype__first .
H10:   currentclass <= rr_type__classtype__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           currentline, [i___1]) >= character__first) and (element(
           currentline, [i___1]) <= character__last))) .
H12:   lastpos >= rr_type__linelengthindex__first .
H13:   lastpos <= rr_type__linelengthindex__last .
H14:   linecount >= unsigned_types__unsigned32__first .
H15:   linecount <= unsigned_types__unsigned32__last .
H16:   0 >= unsigned_types__unsigned32__first .
H17:   0 <= unsigned_types__unsigned32__last .
H18:   currentrecordtype = dns_types__mx .
H19:   lastpos >= rr_type__linelengthindex__first .
H20:   lastpos <= rr_type__linelengthindex__last .
H21:   currentpref__8 >= unsigned_types__unsigned16__first .
H22:   currentpref__8 <= unsigned_types__unsigned16__last .
H23:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__8, [i___1]) >= character__first) and (element(
           currentdomainname__8, [i___1]) <= character__last))) .
H24:   currentpref__8 >= unsigned_types__unsigned16__first .
H25:   currentpref__8 <= unsigned_types__unsigned16__last .
H26:   success__8 .
H27:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__8, [i___1]) >= character__first) and (element(
           currentdomainname__8, [i___1]) <= character__last))) .
H28:   linecount >= unsigned_types__unsigned32__first .
H29:   linecount <= unsigned_types__unsigned32__last .
H30:   lastpos >= rr_type__linelengthindex__first .
H31:   lastpos <= rr_type__linelengthindex__last .
H32:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__9, [i___1]) >= character__first) and (element(
           currentdomainname__9, [i___1]) <= character__last))) .
H33:   success__9 .
H34:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           rr_type__convertdomainnametowire(currentowner), [
           i___1]) >= character__first) and (element(
           rr_type__convertdomainnametowire(currentowner), [
           i___1]) <= character__last))) .
H35:   for_all(i_: integer, ((i_ >= 
           rr_type__domainnamestringtypeindex__first) and (
           i_ <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           rr_type__convertdomainnametowire(currentowner), [
           i_]) >= 0) and (element(
           rr_type__convertdomainnametowire(currentowner), [
           i_]) <= 255))) .
H36:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__9, [i___1]) >= character__first) and (element(
           currentdomainname__9, [i___1]) <= character__last))) .
H37:   currentpref__8 >= unsigned_types__unsigned16__first .
H38:   currentpref__8 <= unsigned_types__unsigned16__last .
        ->
C1:    currentpref__8 >= unsigned_types__unsigned16__first .
C2:    currentpref__8 <= unsigned_types__unsigned16__last .
C3:    currentclass >= rr_type__classtype__first .
C4:    currentclass <= rr_type__classtype__last .
C5:    currentttl >= unsigned_types__unsigned32__first .
C6:    currentttl <= unsigned_types__unsigned32__last .
 

procedure_processfirstlineofrecord_15.
H1:    lastpos >= 1 .
H2:    lastpos <= rr_type__linelengthindex__last .
H3:    currentrecordtype >= dns_types__query_type__first .
H4:    currentrecordtype <= dns_types__query_type__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentorigin, [i___1]) >= character__first) and (element(
           currentorigin, [i___1]) <= character__last))) .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentowner, [i___1]) >= character__first) and (element(
           currentowner, [i___1]) <= character__last))) .
H7:    currentttl >= unsigned_types__unsigned32__first .
H8:    currentttl <= unsigned_types__unsigned32__last .
H9:    currentclass >= rr_type__classtype__first .
H10:   currentclass <= rr_type__classtype__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           currentline, [i___1]) >= character__first) and (element(
           currentline, [i___1]) <= character__last))) .
H12:   lastpos >= rr_type__linelengthindex__first .
H13:   lastpos <= rr_type__linelengthindex__last .
H14:   linecount >= unsigned_types__unsigned32__first .
H15:   linecount <= unsigned_types__unsigned32__last .
H16:   0 >= unsigned_types__unsigned32__first .
H17:   0 <= unsigned_types__unsigned32__last .
H18:   currentrecordtype = dns_types__mx .
H19:   lastpos >= rr_type__linelengthindex__first .
H20:   lastpos <= rr_type__linelengthindex__last .
H21:   currentpref__8 >= unsigned_types__unsigned16__first .
H22:   currentpref__8 <= unsigned_types__unsigned16__last .
H23:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__8, [i___1]) >= character__first) and (element(
           currentdomainname__8, [i___1]) <= character__last))) .
H24:   currentpref__8 >= unsigned_types__unsigned16__first .
H25:   currentpref__8 <= unsigned_types__unsigned16__last .
H26:   not success__8 .
H27:   success__8 .
H28:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           rr_type__convertdomainnametowire(currentowner), [
           i___1]) >= character__first) and (element(
           rr_type__convertdomainnametowire(currentowner), [
           i___1]) <= character__last))) .
H29:   for_all(i_: integer, ((i_ >= 
           rr_type__domainnamestringtypeindex__first) and (
           i_ <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           rr_type__convertdomainnametowire(currentowner), [
           i_]) >= 0) and (element(
           rr_type__convertdomainnametowire(currentowner), [
           i_]) <= 255))) .
H30:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__8, [i___1]) >= character__first) and (element(
           currentdomainname__8, [i___1]) <= character__last))) .
H31:   currentpref__8 >= unsigned_types__unsigned16__first .
H32:   currentpref__8 <= unsigned_types__unsigned16__last .
        ->
C1:    currentpref__8 >= unsigned_types__unsigned16__first .
C2:    currentpref__8 <= unsigned_types__unsigned16__last .
C3:    currentclass >= rr_type__classtype__first .
C4:    currentclass <= rr_type__classtype__last .
C5:    currentttl >= unsigned_types__unsigned32__first .
C6:    currentttl <= unsigned_types__unsigned32__last .
 

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

procedure_processfirstlineofrecord_16.
H1:    lastpos >= 1 .
H2:    lastpos <= rr_type__linelengthindex__last .
H3:    currentrecordtype >= dns_types__query_type__first .
H4:    currentrecordtype <= dns_types__query_type__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentorigin, [i___1]) >= character__first) and (element(
           currentorigin, [i___1]) <= character__last))) .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentowner, [i___1]) >= character__first) and (element(
           currentowner, [i___1]) <= character__last))) .
H7:    currentttl >= unsigned_types__unsigned32__first .
H8:    currentttl <= unsigned_types__unsigned32__last .
H9:    currentclass >= rr_type__classtype__first .
H10:   currentclass <= rr_type__classtype__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           currentline, [i___1]) >= character__first) and (element(
           currentline, [i___1]) <= character__last))) .
H12:   lastpos >= rr_type__linelengthindex__first .
H13:   lastpos <= rr_type__linelengthindex__last .
H14:   linecount >= unsigned_types__unsigned32__first .
H15:   linecount <= unsigned_types__unsigned32__last .
H16:   0 >= unsigned_types__unsigned32__first .
H17:   0 <= unsigned_types__unsigned32__last .
H18:   currentrecordtype = dns_types__ns .
        ->
C1:    lastpos >= rr_type__linelengthindex__first .
C2:    lastpos <= rr_type__linelengthindex__last .
 

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

procedure_processfirstlineofrecord_17.
H1:    lastpos >= 1 .
H2:    lastpos <= rr_type__linelengthindex__last .
H3:    currentrecordtype >= dns_types__query_type__first .
H4:    currentrecordtype <= dns_types__query_type__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentorigin, [i___1]) >= character__first) and (element(
           currentorigin, [i___1]) <= character__last))) .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentowner, [i___1]) >= character__first) and (element(
           currentowner, [i___1]) <= character__last))) .
H7:    currentttl >= unsigned_types__unsigned32__first .
H8:    currentttl <= unsigned_types__unsigned32__last .
H9:    currentclass >= rr_type__classtype__first .
H10:   currentclass <= rr_type__classtype__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           currentline, [i___1]) >= character__first) and (element(
           currentline, [i___1]) <= character__last))) .
H12:   lastpos >= rr_type__linelengthindex__first .
H13:   lastpos <= rr_type__linelengthindex__last .
H14:   linecount >= unsigned_types__unsigned32__first .
H15:   linecount <= unsigned_types__unsigned32__last .
H16:   0 >= unsigned_types__unsigned32__first .
H17:   0 <= unsigned_types__unsigned32__last .
H18:   currentrecordtype = dns_types__ns .
H19:   lastpos >= rr_type__linelengthindex__first .
H20:   lastpos <= rr_type__linelengthindex__last .
H21:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__11, [i___1]) >= character__first) and (element(
           currentdomainname__11, [i___1]) <= character__last))) .
H22:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__11, [i___1]) >= character__first) and (element(
           currentdomainname__11, [i___1]) <= character__last))) .
H23:   true .
H24:   success__12 .
H25:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__11, [i___1]) >= character__first) and (element(
           currentdomainname__11, [i___1]) <= character__last))) .
        ->
C1:    linecount >= unsigned_types__unsigned32__first .
C2:    linecount <= unsigned_types__unsigned32__last .
C3:    lastpos >= rr_type__linelengthindex__first .
C4:    lastpos <= rr_type__linelengthindex__last .
 

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

procedure_processfirstlineofrecord_18.
H1:    lastpos >= 1 .
H2:    lastpos <= rr_type__linelengthindex__last .
H3:    currentrecordtype >= dns_types__query_type__first .
H4:    currentrecordtype <= dns_types__query_type__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentorigin, [i___1]) >= character__first) and (element(
           currentorigin, [i___1]) <= character__last))) .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentowner, [i___1]) >= character__first) and (element(
           currentowner, [i___1]) <= character__last))) .
H7:    currentttl >= unsigned_types__unsigned32__first .
H8:    currentttl <= unsigned_types__unsigned32__last .
H9:    currentclass >= rr_type__classtype__first .
H10:   currentclass <= rr_type__classtype__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           currentline, [i___1]) >= character__first) and (element(
           currentline, [i___1]) <= character__last))) .
H12:   lastpos >= rr_type__linelengthindex__first .
H13:   lastpos <= rr_type__linelengthindex__last .
H14:   linecount >= unsigned_types__unsigned32__first .
H15:   linecount <= unsigned_types__unsigned32__last .
H16:   0 >= unsigned_types__unsigned32__first .
H17:   0 <= unsigned_types__unsigned32__last .
H18:   currentrecordtype = dns_types__ns .
H19:   lastpos >= rr_type__linelengthindex__first .
H20:   lastpos <= rr_type__linelengthindex__last .
H21:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__11, [i___1]) >= character__first) and (element(
           currentdomainname__11, [i___1]) <= character__last))) .
H22:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__11, [i___1]) >= character__first) and (element(
           currentdomainname__11, [i___1]) <= character__last))) .
H23:   true .
H24:   success__12 .
H25:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__11, [i___1]) >= character__first) and (element(
           currentdomainname__11, [i___1]) <= character__last))) .
H26:   linecount >= unsigned_types__unsigned32__first .
H27:   linecount <= unsigned_types__unsigned32__last .
H28:   lastpos >= rr_type__linelengthindex__first .
H29:   lastpos <= rr_type__linelengthindex__last .
H30:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__13, [i___1]) >= character__first) and (element(
           currentdomainname__13, [i___1]) <= character__last))) .
H31:   success__13 .
H32:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           rr_type__convertdomainnametowire(currentowner), [
           i___1]) >= character__first) and (element(
           rr_type__convertdomainnametowire(currentowner), [
           i___1]) <= character__last))) .
H33:   for_all(i_: integer, ((i_ >= 
           rr_type__domainnamestringtypeindex__first) and (
           i_ <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           rr_type__convertdomainnametowire(currentowner), [
           i_]) >= 0) and (element(
           rr_type__convertdomainnametowire(currentowner), [
           i_]) <= 255))) .
H34:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__13, [i___1]) >= character__first) and (element(
           currentdomainname__13, [i___1]) <= character__last))) .
        ->
C1:    currentclass >= rr_type__classtype__first .
C2:    currentclass <= rr_type__classtype__last .
C3:    currentttl >= unsigned_types__unsigned32__first .
C4:    currentttl <= unsigned_types__unsigned32__last .
 

procedure_processfirstlineofrecord_19.
H1:    lastpos >= 1 .
H2:    lastpos <= rr_type__linelengthindex__last .
H3:    currentrecordtype >= dns_types__query_type__first .
H4:    currentrecordtype <= dns_types__query_type__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentorigin, [i___1]) >= character__first) and (element(
           currentorigin, [i___1]) <= character__last))) .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentowner, [i___1]) >= character__first) and (element(
           currentowner, [i___1]) <= character__last))) .
H7:    currentttl >= unsigned_types__unsigned32__first .
H8:    currentttl <= unsigned_types__unsigned32__last .
H9:    currentclass >= rr_type__classtype__first .
H10:   currentclass <= rr_type__classtype__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           currentline, [i___1]) >= character__first) and (element(
           currentline, [i___1]) <= character__last))) .
H12:   lastpos >= rr_type__linelengthindex__first .
H13:   lastpos <= rr_type__linelengthindex__last .
H14:   linecount >= unsigned_types__unsigned32__first .
H15:   linecount <= unsigned_types__unsigned32__last .
H16:   0 >= unsigned_types__unsigned32__first .
H17:   0 <= unsigned_types__unsigned32__last .
H18:   currentrecordtype = dns_types__ns .
H19:   lastpos >= rr_type__linelengthindex__first .
H20:   lastpos <= rr_type__linelengthindex__last .
H21:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__11, [i___1]) >= character__first) and (element(
           currentdomainname__11, [i___1]) <= character__last))) .
H22:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__11, [i___1]) >= character__first) and (element(
           currentdomainname__11, [i___1]) <= character__last))) .
H23:   true .
H24:   not success__12 .
H25:   success__12 .
H26:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           rr_type__convertdomainnametowire(currentowner), [
           i___1]) >= character__first) and (element(
           rr_type__convertdomainnametowire(currentowner), [
           i___1]) <= character__last))) .
H27:   for_all(i_: integer, ((i_ >= 
           rr_type__domainnamestringtypeindex__first) and (
           i_ <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           rr_type__convertdomainnametowire(currentowner), [
           i_]) >= 0) and (element(
           rr_type__convertdomainnametowire(currentowner), [
           i_]) <= 255))) .
H28:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__11, [i___1]) >= character__first) and (element(
           currentdomainname__11, [i___1]) <= character__last))) .
        ->
C1:    currentclass >= rr_type__classtype__first .
C2:    currentclass <= rr_type__classtype__last .
C3:    currentttl >= unsigned_types__unsigned32__first .
C4:    currentttl <= unsigned_types__unsigned32__last .
 

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

procedure_processfirstlineofrecord_20.
H1:    lastpos >= 1 .
H2:    lastpos <= rr_type__linelengthindex__last .
H3:    currentrecordtype >= dns_types__query_type__first .
H4:    currentrecordtype <= dns_types__query_type__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentorigin, [i___1]) >= character__first) and (element(
           currentorigin, [i___1]) <= character__last))) .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentowner, [i___1]) >= character__first) and (element(
           currentowner, [i___1]) <= character__last))) .
H7:    currentttl >= unsigned_types__unsigned32__first .
H8:    currentttl <= unsigned_types__unsigned32__last .
H9:    currentclass >= rr_type__classtype__first .
H10:   currentclass <= rr_type__classtype__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           currentline, [i___1]) >= character__first) and (element(
           currentline, [i___1]) <= character__last))) .
H12:   lastpos >= rr_type__linelengthindex__first .
H13:   lastpos <= rr_type__linelengthindex__last .
H14:   linecount >= unsigned_types__unsigned32__first .
H15:   linecount <= unsigned_types__unsigned32__last .
H16:   0 >= unsigned_types__unsigned32__first .
H17:   0 <= unsigned_types__unsigned32__last .
H18:   currentrecordtype = dns_types__ptr .
        ->
C1:    lastpos >= rr_type__linelengthindex__first .
C2:    lastpos <= rr_type__linelengthindex__last .
 

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

procedure_processfirstlineofrecord_21.
H1:    lastpos >= 1 .
H2:    lastpos <= rr_type__linelengthindex__last .
H3:    currentrecordtype >= dns_types__query_type__first .
H4:    currentrecordtype <= dns_types__query_type__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentorigin, [i___1]) >= character__first) and (element(
           currentorigin, [i___1]) <= character__last))) .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentowner, [i___1]) >= character__first) and (element(
           currentowner, [i___1]) <= character__last))) .
H7:    currentttl >= unsigned_types__unsigned32__first .
H8:    currentttl <= unsigned_types__unsigned32__last .
H9:    currentclass >= rr_type__classtype__first .
H10:   currentclass <= rr_type__classtype__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           currentline, [i___1]) >= character__first) and (element(
           currentline, [i___1]) <= character__last))) .
H12:   lastpos >= rr_type__linelengthindex__first .
H13:   lastpos <= rr_type__linelengthindex__last .
H14:   linecount >= unsigned_types__unsigned32__first .
H15:   linecount <= unsigned_types__unsigned32__last .
H16:   0 >= unsigned_types__unsigned32__first .
H17:   0 <= unsigned_types__unsigned32__last .
H18:   currentrecordtype = dns_types__ptr .
H19:   lastpos >= rr_type__linelengthindex__first .
H20:   lastpos <= rr_type__linelengthindex__last .
H21:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__15, [i___1]) >= character__first) and (element(
           currentdomainname__15, [i___1]) <= character__last))) .
H22:   success__15 .
H23:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__15, [i___1]) >= character__first) and (element(
           currentdomainname__15, [i___1]) <= character__last))) .
        ->
C1:    linecount >= unsigned_types__unsigned32__first .
C2:    linecount <= unsigned_types__unsigned32__last .
C3:    lastpos >= rr_type__linelengthindex__first .
C4:    lastpos <= rr_type__linelengthindex__last .
 

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

procedure_processfirstlineofrecord_22.
H1:    lastpos >= 1 .
H2:    lastpos <= rr_type__linelengthindex__last .
H3:    currentrecordtype >= dns_types__query_type__first .
H4:    currentrecordtype <= dns_types__query_type__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentorigin, [i___1]) >= character__first) and (element(
           currentorigin, [i___1]) <= character__last))) .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentowner, [i___1]) >= character__first) and (element(
           currentowner, [i___1]) <= character__last))) .
H7:    currentttl >= unsigned_types__unsigned32__first .
H8:    currentttl <= unsigned_types__unsigned32__last .
H9:    currentclass >= rr_type__classtype__first .
H10:   currentclass <= rr_type__classtype__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           currentline, [i___1]) >= character__first) and (element(
           currentline, [i___1]) <= character__last))) .
H12:   lastpos >= rr_type__linelengthindex__first .
H13:   lastpos <= rr_type__linelengthindex__last .
H14:   linecount >= unsigned_types__unsigned32__first .
H15:   linecount <= unsigned_types__unsigned32__last .
H16:   0 >= unsigned_types__unsigned32__first .
H17:   0 <= unsigned_types__unsigned32__last .
H18:   currentrecordtype = dns_types__ptr .
H19:   lastpos >= rr_type__linelengthindex__first .
H20:   lastpos <= rr_type__linelengthindex__last .
H21:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__15, [i___1]) >= character__first) and (element(
           currentdomainname__15, [i___1]) <= character__last))) .
H22:   success__15 .
H23:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__15, [i___1]) >= character__first) and (element(
           currentdomainname__15, [i___1]) <= character__last))) .
H24:   linecount >= unsigned_types__unsigned32__first .
H25:   linecount <= unsigned_types__unsigned32__last .
H26:   lastpos >= rr_type__linelengthindex__first .
H27:   lastpos <= rr_type__linelengthindex__last .
H28:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__16, [i___1]) >= character__first) and (element(
           currentdomainname__16, [i___1]) <= character__last))) .
H29:   success__16 .
H30:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           rr_type__convertdomainnametowire(currentowner), [
           i___1]) >= character__first) and (element(
           rr_type__convertdomainnametowire(currentowner), [
           i___1]) <= character__last))) .
H31:   for_all(i_: integer, ((i_ >= 
           rr_type__domainnamestringtypeindex__first) and (
           i_ <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           rr_type__convertdomainnametowire(currentowner), [
           i_]) >= 0) and (element(
           rr_type__convertdomainnametowire(currentowner), [
           i_]) <= 255))) .
H32:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__16, [i___1]) >= character__first) and (element(
           currentdomainname__16, [i___1]) <= character__last))) .
        ->
C1:    currentclass >= rr_type__classtype__first .
C2:    currentclass <= rr_type__classtype__last .
C3:    currentttl >= unsigned_types__unsigned32__first .
C4:    currentttl <= unsigned_types__unsigned32__last .
 

procedure_processfirstlineofrecord_23.
H1:    lastpos >= 1 .
H2:    lastpos <= rr_type__linelengthindex__last .
H3:    currentrecordtype >= dns_types__query_type__first .
H4:    currentrecordtype <= dns_types__query_type__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentorigin, [i___1]) >= character__first) and (element(
           currentorigin, [i___1]) <= character__last))) .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentowner, [i___1]) >= character__first) and (element(
           currentowner, [i___1]) <= character__last))) .
H7:    currentttl >= unsigned_types__unsigned32__first .
H8:    currentttl <= unsigned_types__unsigned32__last .
H9:    currentclass >= rr_type__classtype__first .
H10:   currentclass <= rr_type__classtype__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           currentline, [i___1]) >= character__first) and (element(
           currentline, [i___1]) <= character__last))) .
H12:   lastpos >= rr_type__linelengthindex__first .
H13:   lastpos <= rr_type__linelengthindex__last .
H14:   linecount >= unsigned_types__unsigned32__first .
H15:   linecount <= unsigned_types__unsigned32__last .
H16:   0 >= unsigned_types__unsigned32__first .
H17:   0 <= unsigned_types__unsigned32__last .
H18:   currentrecordtype = dns_types__ptr .
H19:   lastpos >= rr_type__linelengthindex__first .
H20:   lastpos <= rr_type__linelengthindex__last .
H21:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__15, [i___1]) >= character__first) and (element(
           currentdomainname__15, [i___1]) <= character__last))) .
H22:   not success__15 .
H23:   success__15 .
H24:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           rr_type__convertdomainnametowire(currentowner), [
           i___1]) >= character__first) and (element(
           rr_type__convertdomainnametowire(currentowner), [
           i___1]) <= character__last))) .
H25:   for_all(i_: integer, ((i_ >= 
           rr_type__domainnamestringtypeindex__first) and (
           i_ <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           rr_type__convertdomainnametowire(currentowner), [
           i_]) >= 0) and (element(
           rr_type__convertdomainnametowire(currentowner), [
           i_]) <= 255))) .
H26:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__15, [i___1]) >= character__first) and (element(
           currentdomainname__15, [i___1]) <= character__last))) .
        ->
C1:    currentclass >= rr_type__classtype__first .
C2:    currentclass <= rr_type__classtype__last .
C3:    currentttl >= unsigned_types__unsigned32__first .
C4:    currentttl <= unsigned_types__unsigned32__last .
 

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

procedure_processfirstlineofrecord_24.
H1:    lastpos >= 1 .
H2:    lastpos <= rr_type__linelengthindex__last .
H3:    currentrecordtype >= dns_types__query_type__first .
H4:    currentrecordtype <= dns_types__query_type__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentorigin, [i___1]) >= character__first) and (element(
           currentorigin, [i___1]) <= character__last))) .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentowner, [i___1]) >= character__first) and (element(
           currentowner, [i___1]) <= character__last))) .
H7:    currentttl >= unsigned_types__unsigned32__first .
H8:    currentttl <= unsigned_types__unsigned32__last .
H9:    currentclass >= rr_type__classtype__first .
H10:   currentclass <= rr_type__classtype__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           currentline, [i___1]) >= character__first) and (element(
           currentline, [i___1]) <= character__last))) .
H12:   lastpos >= rr_type__linelengthindex__first .
H13:   lastpos <= rr_type__linelengthindex__last .
H14:   linecount >= unsigned_types__unsigned32__first .
H15:   linecount <= unsigned_types__unsigned32__last .
H16:   0 >= unsigned_types__unsigned32__first .
H17:   0 <= unsigned_types__unsigned32__last .
H18:   currentrecordtype = dns_types__soa .
        ->
C1:    0 >= unsigned_types__unsigned32__first .
C2:    0 <= unsigned_types__unsigned32__last .
 

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

procedure_processfirstlineofrecord_25.
H1:    lastpos >= 1 .
H2:    lastpos <= rr_type__linelengthindex__last .
H3:    currentrecordtype >= dns_types__query_type__first .
H4:    currentrecordtype <= dns_types__query_type__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentorigin, [i___1]) >= character__first) and (element(
           currentorigin, [i___1]) <= character__last))) .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentowner, [i___1]) >= character__first) and (element(
           currentowner, [i___1]) <= character__last))) .
H7:    currentttl >= unsigned_types__unsigned32__first .
H8:    currentttl <= unsigned_types__unsigned32__last .
H9:    currentclass >= rr_type__classtype__first .
H10:   currentclass <= rr_type__classtype__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           currentline, [i___1]) >= character__first) and (element(
           currentline, [i___1]) <= character__last))) .
H12:   lastpos >= rr_type__linelengthindex__first .
H13:   lastpos <= rr_type__linelengthindex__last .
H14:   linecount >= unsigned_types__unsigned32__first .
H15:   linecount <= unsigned_types__unsigned32__last .
H16:   0 >= unsigned_types__unsigned32__first .
H17:   0 <= unsigned_types__unsigned32__last .
H18:   currentrecordtype = dns_types__soa .
H19:   0 >= unsigned_types__unsigned32__first .
H20:   0 <= unsigned_types__unsigned32__last .
        ->
C1:    lastpos >= rr_type__linelengthindex__first .
C2:    lastpos <= rr_type__linelengthindex__last .
 

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

procedure_processfirstlineofrecord_26.
H1:    lastpos >= 1 .
H2:    lastpos <= rr_type__linelengthindex__last .
H3:    currentrecordtype >= dns_types__query_type__first .
H4:    currentrecordtype <= dns_types__query_type__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentorigin, [i___1]) >= character__first) and (element(
           currentorigin, [i___1]) <= character__last))) .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentowner, [i___1]) >= character__first) and (element(
           currentowner, [i___1]) <= character__last))) .
H7:    currentttl >= unsigned_types__unsigned32__first .
H8:    currentttl <= unsigned_types__unsigned32__last .
H9:    currentclass >= rr_type__classtype__first .
H10:   currentclass <= rr_type__classtype__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           currentline, [i___1]) >= character__first) and (element(
           currentline, [i___1]) <= character__last))) .
H12:   lastpos >= rr_type__linelengthindex__first .
H13:   lastpos <= rr_type__linelengthindex__last .
H14:   linecount >= unsigned_types__unsigned32__first .
H15:   linecount <= unsigned_types__unsigned32__last .
H16:   0 >= unsigned_types__unsigned32__first .
H17:   0 <= unsigned_types__unsigned32__last .
H18:   currentrecordtype = dns_types__soa .
H19:   0 >= unsigned_types__unsigned32__first .
H20:   0 <= unsigned_types__unsigned32__last .
H21:   lastpos >= rr_type__linelengthindex__first .
H22:   lastpos <= rr_type__linelengthindex__last .
H23:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentnameserver__18, [i___1]) >= character__first) and (element(
           currentnameserver__18, [i___1]) <= character__last))) .
H24:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentemail__18, [i___1]) >= character__first) and (element(
           currentemail__18, [i___1]) <= character__last))) .
H25:   success__18 .
H26:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentnameserver__18, [i___1]) >= character__first) and (element(
           currentnameserver__18, [i___1]) <= character__last))) .
        ->
C1:    linecount >= unsigned_types__unsigned32__first .
C2:    linecount <= unsigned_types__unsigned32__last .
C3:    lastpos >= rr_type__linelengthindex__first .
C4:    lastpos <= rr_type__linelengthindex__last .
 

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

procedure_processfirstlineofrecord_27.
H1:    lastpos >= 1 .
H2:    lastpos <= rr_type__linelengthindex__last .
H3:    currentrecordtype >= dns_types__query_type__first .
H4:    currentrecordtype <= dns_types__query_type__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentorigin, [i___1]) >= character__first) and (element(
           currentorigin, [i___1]) <= character__last))) .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentowner, [i___1]) >= character__first) and (element(
           currentowner, [i___1]) <= character__last))) .
H7:    currentttl >= unsigned_types__unsigned32__first .
H8:    currentttl <= unsigned_types__unsigned32__last .
H9:    currentclass >= rr_type__classtype__first .
H10:   currentclass <= rr_type__classtype__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           currentline, [i___1]) >= character__first) and (element(
           currentline, [i___1]) <= character__last))) .
H12:   lastpos >= rr_type__linelengthindex__first .
H13:   lastpos <= rr_type__linelengthindex__last .
H14:   linecount >= unsigned_types__unsigned32__first .
H15:   linecount <= unsigned_types__unsigned32__last .
H16:   0 >= unsigned_types__unsigned32__first .
H17:   0 <= unsigned_types__unsigned32__last .
H18:   currentrecordtype = dns_types__soa .
H19:   0 >= unsigned_types__unsigned32__first .
H20:   0 <= unsigned_types__unsigned32__last .
H21:   lastpos >= rr_type__linelengthindex__first .
H22:   lastpos <= rr_type__linelengthindex__last .
H23:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentnameserver__18, [i___1]) >= character__first) and (element(
           currentnameserver__18, [i___1]) <= character__last))) .
H24:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentemail__18, [i___1]) >= character__first) and (element(
           currentemail__18, [i___1]) <= character__last))) .
H25:   success__18 .
H26:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentnameserver__18, [i___1]) >= character__first) and (element(
           currentnameserver__18, [i___1]) <= character__last))) .
H27:   linecount >= unsigned_types__unsigned32__first .
H28:   linecount <= unsigned_types__unsigned32__last .
H29:   lastpos >= rr_type__linelengthindex__first .
H30:   lastpos <= rr_type__linelengthindex__last .
H31:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentnameserver__19, [i___1]) >= character__first) and (element(
           currentnameserver__19, [i___1]) <= character__last))) .
H32:   success__19 .
H33:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentemail__18, [i___1]) >= character__first) and (element(
           currentemail__18, [i___1]) <= character__last))) .
        ->
C1:    linecount >= unsigned_types__unsigned32__first .
C2:    linecount <= unsigned_types__unsigned32__last .
C3:    lastpos >= rr_type__linelengthindex__first .
C4:    lastpos <= rr_type__linelengthindex__last .
 

procedure_processfirstlineofrecord_28.
H1:    lastpos >= 1 .
H2:    lastpos <= rr_type__linelengthindex__last .
H3:    currentrecordtype >= dns_types__query_type__first .
H4:    currentrecordtype <= dns_types__query_type__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentorigin, [i___1]) >= character__first) and (element(
           currentorigin, [i___1]) <= character__last))) .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentowner, [i___1]) >= character__first) and (element(
           currentowner, [i___1]) <= character__last))) .
H7:    currentttl >= unsigned_types__unsigned32__first .
H8:    currentttl <= unsigned_types__unsigned32__last .
H9:    currentclass >= rr_type__classtype__first .
H10:   currentclass <= rr_type__classtype__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           currentline, [i___1]) >= character__first) and (element(
           currentline, [i___1]) <= character__last))) .
H12:   lastpos >= rr_type__linelengthindex__first .
H13:   lastpos <= rr_type__linelengthindex__last .
H14:   linecount >= unsigned_types__unsigned32__first .
H15:   linecount <= unsigned_types__unsigned32__last .
H16:   0 >= unsigned_types__unsigned32__first .
H17:   0 <= unsigned_types__unsigned32__last .
H18:   currentrecordtype = dns_types__soa .
H19:   0 >= unsigned_types__unsigned32__first .
H20:   0 <= unsigned_types__unsigned32__last .
H21:   lastpos >= rr_type__linelengthindex__first .
H22:   lastpos <= rr_type__linelengthindex__last .
H23:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentnameserver__18, [i___1]) >= character__first) and (element(
           currentnameserver__18, [i___1]) <= character__last))) .
H24:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentemail__18, [i___1]) >= character__first) and (element(
           currentemail__18, [i___1]) <= character__last))) .
H25:   not success__18 .
H26:   success__18 .
H27:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentemail__18, [i___1]) >= character__first) and (element(
           currentemail__18, [i___1]) <= character__last))) .
        ->
C1:    linecount >= unsigned_types__unsigned32__first .
C2:    linecount <= unsigned_types__unsigned32__last .
C3:    lastpos >= rr_type__linelengthindex__first .
C4:    lastpos <= rr_type__linelengthindex__last .
 

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

procedure_processfirstlineofrecord_29.
H1:    lastpos >= 1 .
H2:    lastpos <= rr_type__linelengthindex__last .
H3:    currentrecordtype >= dns_types__query_type__first .
H4:    currentrecordtype <= dns_types__query_type__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentorigin, [i___1]) >= character__first) and (element(
           currentorigin, [i___1]) <= character__last))) .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentowner, [i___1]) >= character__first) and (element(
           currentowner, [i___1]) <= character__last))) .
H7:    currentttl >= unsigned_types__unsigned32__first .
H8:    currentttl <= unsigned_types__unsigned32__last .
H9:    currentclass >= rr_type__classtype__first .
H10:   currentclass <= rr_type__classtype__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           currentline, [i___1]) >= character__first) and (element(
           currentline, [i___1]) <= character__last))) .
H12:   lastpos >= rr_type__linelengthindex__first .
H13:   lastpos <= rr_type__linelengthindex__last .
H14:   linecount >= unsigned_types__unsigned32__first .
H15:   linecount <= unsigned_types__unsigned32__last .
H16:   0 >= unsigned_types__unsigned32__first .
H17:   0 <= unsigned_types__unsigned32__last .
H18:   currentrecordtype = dns_types__dnskey .
        ->
C1:    0 >= unsigned_types__unsigned32__first .
C2:    0 <= unsigned_types__unsigned32__last .
 

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

procedure_processfirstlineofrecord_30.
H1:    lastpos >= 1 .
H2:    lastpos <= rr_type__linelengthindex__last .
H3:    currentrecordtype >= dns_types__query_type__first .
H4:    currentrecordtype <= dns_types__query_type__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentorigin, [i___1]) >= character__first) and (element(
           currentorigin, [i___1]) <= character__last))) .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentowner, [i___1]) >= character__first) and (element(
           currentowner, [i___1]) <= character__last))) .
H7:    currentttl >= unsigned_types__unsigned32__first .
H8:    currentttl <= unsigned_types__unsigned32__last .
H9:    currentclass >= rr_type__classtype__first .
H10:   currentclass <= rr_type__classtype__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           currentline, [i___1]) >= character__first) and (element(
           currentline, [i___1]) <= character__last))) .
H12:   lastpos >= rr_type__linelengthindex__first .
H13:   lastpos <= rr_type__linelengthindex__last .
H14:   linecount >= unsigned_types__unsigned32__first .
H15:   linecount <= unsigned_types__unsigned32__last .
H16:   0 >= unsigned_types__unsigned32__first .
H17:   0 <= unsigned_types__unsigned32__last .
H18:   currentrecordtype = dns_types__dnskey .
H19:   0 >= unsigned_types__unsigned32__first .
H20:   0 <= unsigned_types__unsigned32__last .
        ->
C1:    lastpos >= rr_type__linelengthindex__first .
C2:    lastpos <= rr_type__linelengthindex__last .
 

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

procedure_processfirstlineofrecord_31.
H1:    lastpos >= 1 .
H2:    lastpos <= rr_type__linelengthindex__last .
H3:    currentrecordtype >= dns_types__query_type__first .
H4:    currentrecordtype <= dns_types__query_type__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentorigin, [i___1]) >= character__first) and (element(
           currentorigin, [i___1]) <= character__last))) .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentowner, [i___1]) >= character__first) and (element(
           currentowner, [i___1]) <= character__last))) .
H7:    currentttl >= unsigned_types__unsigned32__first .
H8:    currentttl <= unsigned_types__unsigned32__last .
H9:    currentclass >= rr_type__classtype__first .
H10:   currentclass <= rr_type__classtype__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           currentline, [i___1]) >= character__first) and (element(
           currentline, [i___1]) <= character__last))) .
H12:   lastpos >= rr_type__linelengthindex__first .
H13:   lastpos <= rr_type__linelengthindex__last .
H14:   linecount >= unsigned_types__unsigned32__first .
H15:   linecount <= unsigned_types__unsigned32__last .
H16:   0 >= unsigned_types__unsigned32__first .
H17:   0 <= unsigned_types__unsigned32__last .
H18:   currentrecordtype = dns_types__nsec .
        ->
C1:    lastpos >= rr_type__linelengthindex__first .
C2:    lastpos <= rr_type__linelengthindex__last .
 

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

procedure_processfirstlineofrecord_32.
H1:    lastpos >= 1 .
H2:    lastpos <= rr_type__linelengthindex__last .
H3:    currentrecordtype >= dns_types__query_type__first .
H4:    currentrecordtype <= dns_types__query_type__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentorigin, [i___1]) >= character__first) and (element(
           currentorigin, [i___1]) <= character__last))) .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentowner, [i___1]) >= character__first) and (element(
           currentowner, [i___1]) <= character__last))) .
H7:    currentttl >= unsigned_types__unsigned32__first .
H8:    currentttl <= unsigned_types__unsigned32__last .
H9:    currentclass >= rr_type__classtype__first .
H10:   currentclass <= rr_type__classtype__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           currentline, [i___1]) >= character__first) and (element(
           currentline, [i___1]) <= character__last))) .
H12:   lastpos >= rr_type__linelengthindex__first .
H13:   lastpos <= rr_type__linelengthindex__last .
H14:   linecount >= unsigned_types__unsigned32__first .
H15:   linecount <= unsigned_types__unsigned32__last .
H16:   0 >= unsigned_types__unsigned32__first .
H17:   0 <= unsigned_types__unsigned32__last .
H18:   currentrecordtype = dns_types__nsec .
H19:   lastpos >= rr_type__linelengthindex__first .
H20:   lastpos <= rr_type__linelengthindex__last .
H21:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__23, [i___1]) >= character__first) and (element(
           currentdomainname__23, [i___1]) <= character__last))) .
H22:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(rrstring__23, [
           i___1]) >= character__first) and (element(rrstring__23, [
           i___1]) <= character__last))) .
H23:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__23, [i___1]) >= character__first) and (element(
           currentdomainname__23, [i___1]) <= character__last))) .
H24:   true .
H25:   success__24 .
H26:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__23, [i___1]) >= character__first) and (element(
           currentdomainname__23, [i___1]) <= character__last))) .
        ->
C1:    linecount >= unsigned_types__unsigned32__first .
C2:    linecount <= unsigned_types__unsigned32__last .
C3:    lastpos >= rr_type__linelengthindex__first .
C4:    lastpos <= rr_type__linelengthindex__last .
 

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

procedure_processfirstlineofrecord_33.
H1:    lastpos >= 1 .
H2:    lastpos <= rr_type__linelengthindex__last .
H3:    currentrecordtype >= dns_types__query_type__first .
H4:    currentrecordtype <= dns_types__query_type__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentorigin, [i___1]) >= character__first) and (element(
           currentorigin, [i___1]) <= character__last))) .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentowner, [i___1]) >= character__first) and (element(
           currentowner, [i___1]) <= character__last))) .
H7:    currentttl >= unsigned_types__unsigned32__first .
H8:    currentttl <= unsigned_types__unsigned32__last .
H9:    currentclass >= rr_type__classtype__first .
H10:   currentclass <= rr_type__classtype__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           currentline, [i___1]) >= character__first) and (element(
           currentline, [i___1]) <= character__last))) .
H12:   lastpos >= rr_type__linelengthindex__first .
H13:   lastpos <= rr_type__linelengthindex__last .
H14:   linecount >= unsigned_types__unsigned32__first .
H15:   linecount <= unsigned_types__unsigned32__last .
H16:   0 >= unsigned_types__unsigned32__first .
H17:   0 <= unsigned_types__unsigned32__last .
H18:   currentrecordtype = dns_types__nsec .
H19:   lastpos >= rr_type__linelengthindex__first .
H20:   lastpos <= rr_type__linelengthindex__last .
H21:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__23, [i___1]) >= character__first) and (element(
           currentdomainname__23, [i___1]) <= character__last))) .
H22:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(rrstring__23, [
           i___1]) >= character__first) and (element(rrstring__23, [
           i___1]) <= character__last))) .
H23:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__23, [i___1]) >= character__first) and (element(
           currentdomainname__23, [i___1]) <= character__last))) .
H24:   true .
H25:   success__24 .
H26:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__23, [i___1]) >= character__first) and (element(
           currentdomainname__23, [i___1]) <= character__last))) .
H27:   linecount >= unsigned_types__unsigned32__first .
H28:   linecount <= unsigned_types__unsigned32__last .
H29:   lastpos >= rr_type__linelengthindex__first .
H30:   lastpos <= rr_type__linelengthindex__last .
H31:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__25, [i___1]) >= character__first) and (element(
           currentdomainname__25, [i___1]) <= character__last))) .
H32:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(rrstring__23, [
           i___1]) >= character__first) and (element(rrstring__23, [
           i___1]) <= character__last))) .
        ->
C1:    linecount >= unsigned_types__unsigned32__first .
C2:    linecount <= unsigned_types__unsigned32__last .
 

procedure_processfirstlineofrecord_34.
H1:    lastpos >= 1 .
H2:    lastpos <= rr_type__linelengthindex__last .
H3:    currentrecordtype >= dns_types__query_type__first .
H4:    currentrecordtype <= dns_types__query_type__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentorigin, [i___1]) >= character__first) and (element(
           currentorigin, [i___1]) <= character__last))) .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentowner, [i___1]) >= character__first) and (element(
           currentowner, [i___1]) <= character__last))) .
H7:    currentttl >= unsigned_types__unsigned32__first .
H8:    currentttl <= unsigned_types__unsigned32__last .
H9:    currentclass >= rr_type__classtype__first .
H10:   currentclass <= rr_type__classtype__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           currentline, [i___1]) >= character__first) and (element(
           currentline, [i___1]) <= character__last))) .
H12:   lastpos >= rr_type__linelengthindex__first .
H13:   lastpos <= rr_type__linelengthindex__last .
H14:   linecount >= unsigned_types__unsigned32__first .
H15:   linecount <= unsigned_types__unsigned32__last .
H16:   0 >= unsigned_types__unsigned32__first .
H17:   0 <= unsigned_types__unsigned32__last .
H18:   currentrecordtype = dns_types__nsec .
H19:   lastpos >= rr_type__linelengthindex__first .
H20:   lastpos <= rr_type__linelengthindex__last .
H21:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__23, [i___1]) >= character__first) and (element(
           currentdomainname__23, [i___1]) <= character__last))) .
H22:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(rrstring__23, [
           i___1]) >= character__first) and (element(rrstring__23, [
           i___1]) <= character__last))) .
H23:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__23, [i___1]) >= character__first) and (element(
           currentdomainname__23, [i___1]) <= character__last))) .
H24:   true .
H25:   not success__24 .
H26:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(rrstring__23, [
           i___1]) >= character__first) and (element(rrstring__23, [
           i___1]) <= character__last))) .
        ->
C1:    linecount >= unsigned_types__unsigned32__first .
C2:    linecount <= unsigned_types__unsigned32__last .
 

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

procedure_processfirstlineofrecord_35.
H1:    lastpos >= 1 .
H2:    lastpos <= rr_type__linelengthindex__last .
H3:    currentrecordtype >= dns_types__query_type__first .
H4:    currentrecordtype <= dns_types__query_type__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentorigin, [i___1]) >= character__first) and (element(
           currentorigin, [i___1]) <= character__last))) .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentowner, [i___1]) >= character__first) and (element(
           currentowner, [i___1]) <= character__last))) .
H7:    currentttl >= unsigned_types__unsigned32__first .
H8:    currentttl <= unsigned_types__unsigned32__last .
H9:    currentclass >= rr_type__classtype__first .
H10:   currentclass <= rr_type__classtype__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           currentline, [i___1]) >= character__first) and (element(
           currentline, [i___1]) <= character__last))) .
H12:   lastpos >= rr_type__linelengthindex__first .
H13:   lastpos <= rr_type__linelengthindex__last .
H14:   linecount >= unsigned_types__unsigned32__first .
H15:   linecount <= unsigned_types__unsigned32__last .
H16:   0 >= unsigned_types__unsigned32__first .
H17:   0 <= unsigned_types__unsigned32__last .
H18:   currentrecordtype = dns_types__nsec .
H19:   lastpos >= rr_type__linelengthindex__first .
H20:   lastpos <= rr_type__linelengthindex__last .
H21:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__23, [i___1]) >= character__first) and (element(
           currentdomainname__23, [i___1]) <= character__last))) .
H22:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(rrstring__23, [
           i___1]) >= character__first) and (element(rrstring__23, [
           i___1]) <= character__last))) .
H23:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__23, [i___1]) >= character__first) and (element(
           currentdomainname__23, [i___1]) <= character__last))) .
H24:   true .
H25:   success__24 .
H26:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__23, [i___1]) >= character__first) and (element(
           currentdomainname__23, [i___1]) <= character__last))) .
H27:   linecount >= unsigned_types__unsigned32__first .
H28:   linecount <= unsigned_types__unsigned32__last .
H29:   lastpos >= rr_type__linelengthindex__first .
H30:   lastpos <= rr_type__linelengthindex__last .
H31:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__25, [i___1]) >= character__first) and (element(
           currentdomainname__25, [i___1]) <= character__last))) .
H32:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(rrstring__23, [
           i___1]) >= character__first) and (element(rrstring__23, [
           i___1]) <= character__last))) .
H33:   linecount >= unsigned_types__unsigned32__first .
H34:   linecount <= unsigned_types__unsigned32__last .
H35:   (success__26 = true) -> (numberofblocks__26 > 0) .
H36:   numberofrecordtypes__26 >= 
           rr_type__nsec_record_type__recordtypeindexvalue__first .
H37:   numberofrecordtypes__26 <= 
           rr_type__nsec_record_type__recordtypeindexvalue__last .
H38:   for_all(i___1: integer, ((i___1 >= 
           rr_type__nsec_record_type__recordtypearrayindex__first) and (
           i___1 <= 
           rr_type__nsec_record_type__recordtypearrayindex__last)) -> ((element(
           recordtypes__26, [i___1]) >= dns_types__query_type__first) and (element(
           recordtypes__26, [i___1]) <= dns_types__query_type__last))) .
H39:   numberofblocks__26 >= 
           rr_type__nsec_record_type__blocknumbervalue__first .
H40:   numberofblocks__26 <= 
           rr_type__nsec_record_type__blocknumbervalue__last .
H41:   for_all(i___1: integer, ((i___1 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___1 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           blocknumbers__26, [i___1]) >= dns_types__byte__first) and (element(
           blocknumbers__26, [i___1]) <= dns_types__byte__last))) .
H42:   for_all(i___1: integer, ((i___1 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___1 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           blocklengths__26, [i___1]) >= 
           rr_type__nsec_record_type__blocklengthvalue__first) and (element(
           blocklengths__26, [i___1]) <= 
           rr_type__nsec_record_type__blocklengthvalue__last))) .
H43:   for_all(i___1: integer, ((i___1 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___1 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__nsec_record_type__bitmapindex__first) and (
           i___2 <= rr_type__nsec_record_type__bitmapindex__last)) -> ((element(element(
           bitmaps__26, [i___1]), [i___2]) >= dns_types__byte__first) and (element(element(
           bitmaps__26, [i___1]), [i___2]) <= dns_types__byte__last))))) .
        ->
C1:    numberofblocks__26 >= 
           rr_type__nsec_record_type__blocknumbervalue__first .
C2:    numberofblocks__26 <= 
           rr_type__nsec_record_type__blocknumbervalue__last .
C3:    numberofrecordtypes__26 >= 
           rr_type__nsec_record_type__recordtypeindexvalue__first .
C4:    numberofrecordtypes__26 <= 
           rr_type__nsec_record_type__recordtypeindexvalue__last .
 

procedure_processfirstlineofrecord_36.
H1:    lastpos >= 1 .
H2:    lastpos <= rr_type__linelengthindex__last .
H3:    currentrecordtype >= dns_types__query_type__first .
H4:    currentrecordtype <= dns_types__query_type__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentorigin, [i___1]) >= character__first) and (element(
           currentorigin, [i___1]) <= character__last))) .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentowner, [i___1]) >= character__first) and (element(
           currentowner, [i___1]) <= character__last))) .
H7:    currentttl >= unsigned_types__unsigned32__first .
H8:    currentttl <= unsigned_types__unsigned32__last .
H9:    currentclass >= rr_type__classtype__first .
H10:   currentclass <= rr_type__classtype__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           currentline, [i___1]) >= character__first) and (element(
           currentline, [i___1]) <= character__last))) .
H12:   lastpos >= rr_type__linelengthindex__first .
H13:   lastpos <= rr_type__linelengthindex__last .
H14:   linecount >= unsigned_types__unsigned32__first .
H15:   linecount <= unsigned_types__unsigned32__last .
H16:   0 >= unsigned_types__unsigned32__first .
H17:   0 <= unsigned_types__unsigned32__last .
H18:   currentrecordtype = dns_types__nsec .
H19:   lastpos >= rr_type__linelengthindex__first .
H20:   lastpos <= rr_type__linelengthindex__last .
H21:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__23, [i___1]) >= character__first) and (element(
           currentdomainname__23, [i___1]) <= character__last))) .
H22:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(rrstring__23, [
           i___1]) >= character__first) and (element(rrstring__23, [
           i___1]) <= character__last))) .
H23:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__23, [i___1]) >= character__first) and (element(
           currentdomainname__23, [i___1]) <= character__last))) .
H24:   true .
H25:   not success__24 .
H26:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(rrstring__23, [
           i___1]) >= character__first) and (element(rrstring__23, [
           i___1]) <= character__last))) .
H27:   linecount >= unsigned_types__unsigned32__first .
H28:   linecount <= unsigned_types__unsigned32__last .
H29:   (success__26 = true) -> (numberofblocks__26 > 0) .
H30:   numberofrecordtypes__26 >= 
           rr_type__nsec_record_type__recordtypeindexvalue__first .
H31:   numberofrecordtypes__26 <= 
           rr_type__nsec_record_type__recordtypeindexvalue__last .
H32:   for_all(i___1: integer, ((i___1 >= 
           rr_type__nsec_record_type__recordtypearrayindex__first) and (
           i___1 <= 
           rr_type__nsec_record_type__recordtypearrayindex__last)) -> ((element(
           recordtypes__26, [i___1]) >= dns_types__query_type__first) and (element(
           recordtypes__26, [i___1]) <= dns_types__query_type__last))) .
H33:   numberofblocks__26 >= 
           rr_type__nsec_record_type__blocknumbervalue__first .
H34:   numberofblocks__26 <= 
           rr_type__nsec_record_type__blocknumbervalue__last .
H35:   for_all(i___1: integer, ((i___1 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___1 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           blocknumbers__26, [i___1]) >= dns_types__byte__first) and (element(
           blocknumbers__26, [i___1]) <= dns_types__byte__last))) .
H36:   for_all(i___1: integer, ((i___1 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___1 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           blocklengths__26, [i___1]) >= 
           rr_type__nsec_record_type__blocklengthvalue__first) and (element(
           blocklengths__26, [i___1]) <= 
           rr_type__nsec_record_type__blocklengthvalue__last))) .
H37:   for_all(i___1: integer, ((i___1 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___1 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__nsec_record_type__bitmapindex__first) and (
           i___2 <= rr_type__nsec_record_type__bitmapindex__last)) -> ((element(element(
           bitmaps__26, [i___1]), [i___2]) >= dns_types__byte__first) and (element(element(
           bitmaps__26, [i___1]), [i___2]) <= dns_types__byte__last))))) .
        ->
C1:    numberofblocks__26 >= 
           rr_type__nsec_record_type__blocknumbervalue__first .
C2:    numberofblocks__26 <= 
           rr_type__nsec_record_type__blocknumbervalue__last .
C3:    numberofrecordtypes__26 >= 
           rr_type__nsec_record_type__recordtypeindexvalue__first .
C4:    numberofrecordtypes__26 <= 
           rr_type__nsec_record_type__recordtypeindexvalue__last .
 

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

procedure_processfirstlineofrecord_37.
H1:    lastpos >= 1 .
H2:    lastpos <= rr_type__linelengthindex__last .
H3:    currentrecordtype >= dns_types__query_type__first .
H4:    currentrecordtype <= dns_types__query_type__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentorigin, [i___1]) >= character__first) and (element(
           currentorigin, [i___1]) <= character__last))) .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentowner, [i___1]) >= character__first) and (element(
           currentowner, [i___1]) <= character__last))) .
H7:    currentttl >= unsigned_types__unsigned32__first .
H8:    currentttl <= unsigned_types__unsigned32__last .
H9:    currentclass >= rr_type__classtype__first .
H10:   currentclass <= rr_type__classtype__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           currentline, [i___1]) >= character__first) and (element(
           currentline, [i___1]) <= character__last))) .
H12:   lastpos >= rr_type__linelengthindex__first .
H13:   lastpos <= rr_type__linelengthindex__last .
H14:   linecount >= unsigned_types__unsigned32__first .
H15:   linecount <= unsigned_types__unsigned32__last .
H16:   0 >= unsigned_types__unsigned32__first .
H17:   0 <= unsigned_types__unsigned32__last .
H18:   currentrecordtype = dns_types__nsec .
H19:   lastpos >= rr_type__linelengthindex__first .
H20:   lastpos <= rr_type__linelengthindex__last .
H21:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__23, [i___1]) >= character__first) and (element(
           currentdomainname__23, [i___1]) <= character__last))) .
H22:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(rrstring__23, [
           i___1]) >= character__first) and (element(rrstring__23, [
           i___1]) <= character__last))) .
H23:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__23, [i___1]) >= character__first) and (element(
           currentdomainname__23, [i___1]) <= character__last))) .
H24:   true .
H25:   success__24 .
H26:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__23, [i___1]) >= character__first) and (element(
           currentdomainname__23, [i___1]) <= character__last))) .
H27:   linecount >= unsigned_types__unsigned32__first .
H28:   linecount <= unsigned_types__unsigned32__last .
H29:   lastpos >= rr_type__linelengthindex__first .
H30:   lastpos <= rr_type__linelengthindex__last .
H31:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__25, [i___1]) >= character__first) and (element(
           currentdomainname__25, [i___1]) <= character__last))) .
H32:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(rrstring__23, [
           i___1]) >= character__first) and (element(rrstring__23, [
           i___1]) <= character__last))) .
H33:   linecount >= unsigned_types__unsigned32__first .
H34:   linecount <= unsigned_types__unsigned32__last .
H35:   (success__26 = true) -> (numberofblocks__26 > 0) .
H36:   numberofrecordtypes__26 >= 
           rr_type__nsec_record_type__recordtypeindexvalue__first .
H37:   numberofrecordtypes__26 <= 
           rr_type__nsec_record_type__recordtypeindexvalue__last .
H38:   for_all(i___1: integer, ((i___1 >= 
           rr_type__nsec_record_type__recordtypearrayindex__first) and (
           i___1 <= 
           rr_type__nsec_record_type__recordtypearrayindex__last)) -> ((element(
           recordtypes__26, [i___1]) >= dns_types__query_type__first) and (element(
           recordtypes__26, [i___1]) <= dns_types__query_type__last))) .
H39:   numberofblocks__26 >= 
           rr_type__nsec_record_type__blocknumbervalue__first .
H40:   numberofblocks__26 <= 
           rr_type__nsec_record_type__blocknumbervalue__last .
H41:   for_all(i___1: integer, ((i___1 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___1 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           blocknumbers__26, [i___1]) >= dns_types__byte__first) and (element(
           blocknumbers__26, [i___1]) <= dns_types__byte__last))) .
H42:   for_all(i___1: integer, ((i___1 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___1 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           blocklengths__26, [i___1]) >= 
           rr_type__nsec_record_type__blocklengthvalue__first) and (element(
           blocklengths__26, [i___1]) <= 
           rr_type__nsec_record_type__blocklengthvalue__last))) .
H43:   for_all(i___1: integer, ((i___1 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___1 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__nsec_record_type__bitmapindex__first) and (
           i___2 <= rr_type__nsec_record_type__bitmapindex__last)) -> ((element(element(
           bitmaps__26, [i___1]), [i___2]) >= dns_types__byte__first) and (element(element(
           bitmaps__26, [i___1]), [i___2]) <= dns_types__byte__last))))) .
H44:   numberofblocks__26 >= 
           rr_type__nsec_record_type__blocknumbervalue__first .
H45:   numberofblocks__26 <= 
           rr_type__nsec_record_type__blocknumbervalue__last .
H46:   numberofrecordtypes__26 >= 
           rr_type__nsec_record_type__recordtypeindexvalue__first .
H47:   numberofrecordtypes__26 <= 
           rr_type__nsec_record_type__recordtypeindexvalue__last .
H48:   success__26 .
H49:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           rr_type__convertdomainnametowire(currentowner), [
           i___1]) >= character__first) and (element(
           rr_type__convertdomainnametowire(currentowner), [
           i___1]) <= character__last))) .
H50:   for_all(i_: integer, ((i_ >= 
           rr_type__domainnamestringtypeindex__first) and (
           i_ <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           rr_type__convertdomainnametowire(currentowner), [
           i_]) >= 0) and (element(
           rr_type__convertdomainnametowire(currentowner), [
           i_]) <= 255))) .
H51:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__25, [i___1]) >= character__first) and (element(
           currentdomainname__25, [i___1]) <= character__last))) .
H52:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(rrstring__23, [
           i___1]) >= character__first) and (element(rrstring__23, [
           i___1]) <= character__last))) .
H53:   numberofblocks__26 >= 
           rr_type__nsec_record_type__blocknumbervalue__first .
H54:   numberofblocks__26 <= 
           rr_type__nsec_record_type__blocknumbervalue__last .
H55:   numberofrecordtypes__26 >= 
           rr_type__nsec_record_type__recordtypeindexvalue__first .
H56:   numberofrecordtypes__26 <= 
           rr_type__nsec_record_type__recordtypeindexvalue__last .
H57:   for_all(i___1: integer, ((i___1 >= 
           rr_type__nsec_record_type__recordtypearrayindex__first) and (
           i___1 <= 
           rr_type__nsec_record_type__recordtypearrayindex__last)) -> ((element(
           recordtypes__26, [i___1]) >= dns_types__query_type__first) and (element(
           recordtypes__26, [i___1]) <= dns_types__query_type__last))) .
H58:   for_all(i___1: integer, ((i___1 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___1 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           blocknumbers__26, [i___1]) >= dns_types__byte__first) and (element(
           blocknumbers__26, [i___1]) <= dns_types__byte__last))) .
H59:   for_all(i___1: integer, ((i___1 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___1 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           blocklengths__26, [i___1]) >= 
           rr_type__nsec_record_type__blocklengthvalue__first) and (element(
           blocklengths__26, [i___1]) <= 
           rr_type__nsec_record_type__blocklengthvalue__last))) .
H60:   for_all(i___1: integer, ((i___1 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___1 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__nsec_record_type__bitmapindex__first) and (
           i___2 <= rr_type__nsec_record_type__bitmapindex__last)) -> ((element(element(
           bitmaps__26, [i___1]), [i___2]) >= dns_types__byte__first) and (element(element(
           bitmaps__26, [i___1]), [i___2]) <= dns_types__byte__last))))) .
        ->
C1:    numberofblocks__26 >= 
           rr_type__nsec_record_type__blocknumbervalue__first .
C2:    numberofblocks__26 <= 
           rr_type__nsec_record_type__blocknumbervalue__last .
C3:    numberofrecordtypes__26 >= 
           rr_type__nsec_record_type__recordtypeindexvalue__first .
C4:    numberofrecordtypes__26 <= 
           rr_type__nsec_record_type__recordtypeindexvalue__last .
C5:    currentclass >= rr_type__classtype__first .
C6:    currentclass <= rr_type__classtype__last .
C7:    currentttl >= unsigned_types__unsigned32__first .
C8:    currentttl <= unsigned_types__unsigned32__last .
 

procedure_processfirstlineofrecord_38.
H1:    lastpos >= 1 .
H2:    lastpos <= rr_type__linelengthindex__last .
H3:    currentrecordtype >= dns_types__query_type__first .
H4:    currentrecordtype <= dns_types__query_type__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentorigin, [i___1]) >= character__first) and (element(
           currentorigin, [i___1]) <= character__last))) .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentowner, [i___1]) >= character__first) and (element(
           currentowner, [i___1]) <= character__last))) .
H7:    currentttl >= unsigned_types__unsigned32__first .
H8:    currentttl <= unsigned_types__unsigned32__last .
H9:    currentclass >= rr_type__classtype__first .
H10:   currentclass <= rr_type__classtype__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           currentline, [i___1]) >= character__first) and (element(
           currentline, [i___1]) <= character__last))) .
H12:   lastpos >= rr_type__linelengthindex__first .
H13:   lastpos <= rr_type__linelengthindex__last .
H14:   linecount >= unsigned_types__unsigned32__first .
H15:   linecount <= unsigned_types__unsigned32__last .
H16:   0 >= unsigned_types__unsigned32__first .
H17:   0 <= unsigned_types__unsigned32__last .
H18:   currentrecordtype = dns_types__nsec .
H19:   lastpos >= rr_type__linelengthindex__first .
H20:   lastpos <= rr_type__linelengthindex__last .
H21:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__23, [i___1]) >= character__first) and (element(
           currentdomainname__23, [i___1]) <= character__last))) .
H22:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(rrstring__23, [
           i___1]) >= character__first) and (element(rrstring__23, [
           i___1]) <= character__last))) .
H23:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__23, [i___1]) >= character__first) and (element(
           currentdomainname__23, [i___1]) <= character__last))) .
H24:   true .
H25:   not success__24 .
H26:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(rrstring__23, [
           i___1]) >= character__first) and (element(rrstring__23, [
           i___1]) <= character__last))) .
H27:   linecount >= unsigned_types__unsigned32__first .
H28:   linecount <= unsigned_types__unsigned32__last .
H29:   (success__26 = true) -> (numberofblocks__26 > 0) .
H30:   numberofrecordtypes__26 >= 
           rr_type__nsec_record_type__recordtypeindexvalue__first .
H31:   numberofrecordtypes__26 <= 
           rr_type__nsec_record_type__recordtypeindexvalue__last .
H32:   for_all(i___1: integer, ((i___1 >= 
           rr_type__nsec_record_type__recordtypearrayindex__first) and (
           i___1 <= 
           rr_type__nsec_record_type__recordtypearrayindex__last)) -> ((element(
           recordtypes__26, [i___1]) >= dns_types__query_type__first) and (element(
           recordtypes__26, [i___1]) <= dns_types__query_type__last))) .
H33:   numberofblocks__26 >= 
           rr_type__nsec_record_type__blocknumbervalue__first .
H34:   numberofblocks__26 <= 
           rr_type__nsec_record_type__blocknumbervalue__last .
H35:   for_all(i___1: integer, ((i___1 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___1 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           blocknumbers__26, [i___1]) >= dns_types__byte__first) and (element(
           blocknumbers__26, [i___1]) <= dns_types__byte__last))) .
H36:   for_all(i___1: integer, ((i___1 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___1 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           blocklengths__26, [i___1]) >= 
           rr_type__nsec_record_type__blocklengthvalue__first) and (element(
           blocklengths__26, [i___1]) <= 
           rr_type__nsec_record_type__blocklengthvalue__last))) .
H37:   for_all(i___1: integer, ((i___1 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___1 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__nsec_record_type__bitmapindex__first) and (
           i___2 <= rr_type__nsec_record_type__bitmapindex__last)) -> ((element(element(
           bitmaps__26, [i___1]), [i___2]) >= dns_types__byte__first) and (element(element(
           bitmaps__26, [i___1]), [i___2]) <= dns_types__byte__last))))) .
H38:   numberofblocks__26 >= 
           rr_type__nsec_record_type__blocknumbervalue__first .
H39:   numberofblocks__26 <= 
           rr_type__nsec_record_type__blocknumbervalue__last .
H40:   numberofrecordtypes__26 >= 
           rr_type__nsec_record_type__recordtypeindexvalue__first .
H41:   numberofrecordtypes__26 <= 
           rr_type__nsec_record_type__recordtypeindexvalue__last .
H42:   success__26 .
H43:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           rr_type__convertdomainnametowire(currentowner), [
           i___1]) >= character__first) and (element(
           rr_type__convertdomainnametowire(currentowner), [
           i___1]) <= character__last))) .
H44:   for_all(i_: integer, ((i_ >= 
           rr_type__domainnamestringtypeindex__first) and (
           i_ <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           rr_type__convertdomainnametowire(currentowner), [
           i_]) >= 0) and (element(
           rr_type__convertdomainnametowire(currentowner), [
           i_]) <= 255))) .
H45:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__23, [i___1]) >= character__first) and (element(
           currentdomainname__23, [i___1]) <= character__last))) .
H46:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(rrstring__23, [
           i___1]) >= character__first) and (element(rrstring__23, [
           i___1]) <= character__last))) .
H47:   numberofblocks__26 >= 
           rr_type__nsec_record_type__blocknumbervalue__first .
H48:   numberofblocks__26 <= 
           rr_type__nsec_record_type__blocknumbervalue__last .
H49:   numberofrecordtypes__26 >= 
           rr_type__nsec_record_type__recordtypeindexvalue__first .
H50:   numberofrecordtypes__26 <= 
           rr_type__nsec_record_type__recordtypeindexvalue__last .
H51:   for_all(i___1: integer, ((i___1 >= 
           rr_type__nsec_record_type__recordtypearrayindex__first) and (
           i___1 <= 
           rr_type__nsec_record_type__recordtypearrayindex__last)) -> ((element(
           recordtypes__26, [i___1]) >= dns_types__query_type__first) and (element(
           recordtypes__26, [i___1]) <= dns_types__query_type__last))) .
H52:   for_all(i___1: integer, ((i___1 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___1 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           blocknumbers__26, [i___1]) >= dns_types__byte__first) and (element(
           blocknumbers__26, [i___1]) <= dns_types__byte__last))) .
H53:   for_all(i___1: integer, ((i___1 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___1 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           blocklengths__26, [i___1]) >= 
           rr_type__nsec_record_type__blocklengthvalue__first) and (element(
           blocklengths__26, [i___1]) <= 
           rr_type__nsec_record_type__blocklengthvalue__last))) .
H54:   for_all(i___1: integer, ((i___1 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___1 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__nsec_record_type__bitmapindex__first) and (
           i___2 <= rr_type__nsec_record_type__bitmapindex__last)) -> ((element(element(
           bitmaps__26, [i___1]), [i___2]) >= dns_types__byte__first) and (element(element(
           bitmaps__26, [i___1]), [i___2]) <= dns_types__byte__last))))) .
        ->
C1:    numberofblocks__26 >= 
           rr_type__nsec_record_type__blocknumbervalue__first .
C2:    numberofblocks__26 <= 
           rr_type__nsec_record_type__blocknumbervalue__last .
C3:    numberofrecordtypes__26 >= 
           rr_type__nsec_record_type__recordtypeindexvalue__first .
C4:    numberofrecordtypes__26 <= 
           rr_type__nsec_record_type__recordtypeindexvalue__last .
C5:    currentclass >= rr_type__classtype__first .
C6:    currentclass <= rr_type__classtype__last .
C7:    currentttl >= unsigned_types__unsigned32__first .
C8:    currentttl <= unsigned_types__unsigned32__last .
 

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

procedure_processfirstlineofrecord_39.
H1:    lastpos >= 1 .
H2:    lastpos <= rr_type__linelengthindex__last .
H3:    currentrecordtype >= dns_types__query_type__first .
H4:    currentrecordtype <= dns_types__query_type__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentorigin, [i___1]) >= character__first) and (element(
           currentorigin, [i___1]) <= character__last))) .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentowner, [i___1]) >= character__first) and (element(
           currentowner, [i___1]) <= character__last))) .
H7:    currentttl >= unsigned_types__unsigned32__first .
H8:    currentttl <= unsigned_types__unsigned32__last .
H9:    currentclass >= rr_type__classtype__first .
H10:   currentclass <= rr_type__classtype__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           currentline, [i___1]) >= character__first) and (element(
           currentline, [i___1]) <= character__last))) .
H12:   lastpos >= rr_type__linelengthindex__first .
H13:   lastpos <= rr_type__linelengthindex__last .
H14:   linecount >= unsigned_types__unsigned32__first .
H15:   linecount <= unsigned_types__unsigned32__last .
H16:   0 >= unsigned_types__unsigned32__first .
H17:   0 <= unsigned_types__unsigned32__last .
H18:   currentrecordtype = dns_types__nsec .
H19:   lastpos >= rr_type__linelengthindex__first .
H20:   lastpos <= rr_type__linelengthindex__last .
H21:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__23, [i___1]) >= character__first) and (element(
           currentdomainname__23, [i___1]) <= character__last))) .
H22:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(rrstring__23, [
           i___1]) >= character__first) and (element(rrstring__23, [
           i___1]) <= character__last))) .
H23:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__23, [i___1]) >= character__first) and (element(
           currentdomainname__23, [i___1]) <= character__last))) .
H24:   true .
H25:   success__24 .
H26:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__23, [i___1]) >= character__first) and (element(
           currentdomainname__23, [i___1]) <= character__last))) .
H27:   linecount >= unsigned_types__unsigned32__first .
H28:   linecount <= unsigned_types__unsigned32__last .
H29:   lastpos >= rr_type__linelengthindex__first .
H30:   lastpos <= rr_type__linelengthindex__last .
H31:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__25, [i___1]) >= character__first) and (element(
           currentdomainname__25, [i___1]) <= character__last))) .
H32:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(rrstring__23, [
           i___1]) >= character__first) and (element(rrstring__23, [
           i___1]) <= character__last))) .
H33:   linecount >= unsigned_types__unsigned32__first .
H34:   linecount <= unsigned_types__unsigned32__last .
H35:   (success__26 = true) -> (numberofblocks__26 > 0) .
H36:   numberofrecordtypes__26 >= 
           rr_type__nsec_record_type__recordtypeindexvalue__first .
H37:   numberofrecordtypes__26 <= 
           rr_type__nsec_record_type__recordtypeindexvalue__last .
H38:   for_all(i___1: integer, ((i___1 >= 
           rr_type__nsec_record_type__recordtypearrayindex__first) and (
           i___1 <= 
           rr_type__nsec_record_type__recordtypearrayindex__last)) -> ((element(
           recordtypes__26, [i___1]) >= dns_types__query_type__first) and (element(
           recordtypes__26, [i___1]) <= dns_types__query_type__last))) .
H39:   numberofblocks__26 >= 
           rr_type__nsec_record_type__blocknumbervalue__first .
H40:   numberofblocks__26 <= 
           rr_type__nsec_record_type__blocknumbervalue__last .
H41:   for_all(i___1: integer, ((i___1 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___1 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           blocknumbers__26, [i___1]) >= dns_types__byte__first) and (element(
           blocknumbers__26, [i___1]) <= dns_types__byte__last))) .
H42:   for_all(i___1: integer, ((i___1 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___1 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           blocklengths__26, [i___1]) >= 
           rr_type__nsec_record_type__blocklengthvalue__first) and (element(
           blocklengths__26, [i___1]) <= 
           rr_type__nsec_record_type__blocklengthvalue__last))) .
H43:   for_all(i___1: integer, ((i___1 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___1 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__nsec_record_type__bitmapindex__first) and (
           i___2 <= rr_type__nsec_record_type__bitmapindex__last)) -> ((element(element(
           bitmaps__26, [i___1]), [i___2]) >= dns_types__byte__first) and (element(element(
           bitmaps__26, [i___1]), [i___2]) <= dns_types__byte__last))))) .
H44:   numberofblocks__26 >= 
           rr_type__nsec_record_type__blocknumbervalue__first .
H45:   numberofblocks__26 <= 
           rr_type__nsec_record_type__blocknumbervalue__last .
H46:   numberofrecordtypes__26 >= 
           rr_type__nsec_record_type__recordtypeindexvalue__first .
H47:   numberofrecordtypes__26 <= 
           rr_type__nsec_record_type__recordtypeindexvalue__last .
H48:   success__26 .
H49:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           rr_type__convertdomainnametowire(currentowner), [
           i___1]) >= character__first) and (element(
           rr_type__convertdomainnametowire(currentowner), [
           i___1]) <= character__last))) .
H50:   for_all(i_: integer, ((i_ >= 
           rr_type__domainnamestringtypeindex__first) and (
           i_ <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           rr_type__convertdomainnametowire(currentowner), [
           i_]) >= 0) and (element(
           rr_type__convertdomainnametowire(currentowner), [
           i_]) <= 255))) .
H51:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__25, [i___1]) >= character__first) and (element(
           currentdomainname__25, [i___1]) <= character__last))) .
H52:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(rrstring__23, [
           i___1]) >= character__first) and (element(rrstring__23, [
           i___1]) <= character__last))) .
H53:   numberofblocks__26 >= 
           rr_type__nsec_record_type__blocknumbervalue__first .
H54:   numberofblocks__26 <= 
           rr_type__nsec_record_type__blocknumbervalue__last .
H55:   numberofrecordtypes__26 >= 
           rr_type__nsec_record_type__recordtypeindexvalue__first .
H56:   numberofrecordtypes__26 <= 
           rr_type__nsec_record_type__recordtypeindexvalue__last .
H57:   for_all(i___1: integer, ((i___1 >= 
           rr_type__nsec_record_type__recordtypearrayindex__first) and (
           i___1 <= 
           rr_type__nsec_record_type__recordtypearrayindex__last)) -> ((element(
           recordtypes__26, [i___1]) >= dns_types__query_type__first) and (element(
           recordtypes__26, [i___1]) <= dns_types__query_type__last))) .
H58:   for_all(i___1: integer, ((i___1 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___1 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           blocknumbers__26, [i___1]) >= dns_types__byte__first) and (element(
           blocknumbers__26, [i___1]) <= dns_types__byte__last))) .
H59:   for_all(i___1: integer, ((i___1 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___1 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           blocklengths__26, [i___1]) >= 
           rr_type__nsec_record_type__blocklengthvalue__first) and (element(
           blocklengths__26, [i___1]) <= 
           rr_type__nsec_record_type__blocklengthvalue__last))) .
H60:   for_all(i___1: integer, ((i___1 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___1 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__nsec_record_type__bitmapindex__first) and (
           i___2 <= rr_type__nsec_record_type__bitmapindex__last)) -> ((element(element(
           bitmaps__26, [i___1]), [i___2]) >= dns_types__byte__first) and (element(element(
           bitmaps__26, [i___1]), [i___2]) <= dns_types__byte__last))))) .
H61:   numberofblocks__26 >= 
           rr_type__nsec_record_type__blocknumbervalue__first .
H62:   numberofblocks__26 <= 
           rr_type__nsec_record_type__blocknumbervalue__last .
H63:   numberofrecordtypes__26 >= 
           rr_type__nsec_record_type__recordtypeindexvalue__first .
H64:   numberofrecordtypes__26 <= 
           rr_type__nsec_record_type__recordtypeindexvalue__last .
H65:   currentclass >= rr_type__classtype__first .
H66:   currentclass <= rr_type__classtype__last .
H67:   currentttl >= unsigned_types__unsigned32__first .
H68:   currentttl <= unsigned_types__unsigned32__last .
H69:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           rr_type__convertdomainnametowire(currentdomainname__25), [
           i___1]) >= character__first) and (element(
           rr_type__convertdomainnametowire(currentdomainname__25), [
           i___1]) <= character__last))) .
H70:   for_all(i_: integer, ((i_ >= 
           rr_type__domainnamestringtypeindex__first) and (
           i_ <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           rr_type__convertdomainnametowire(currentdomainname__25), [
           i_]) >= 0) and (element(
           rr_type__convertdomainnametowire(currentdomainname__25), [
           i_]) <= 255))) .
        ->
C1:    fld_numberofblocks(
           mk__rr_type__nsec_record_type__nsecrecordtype(
           inherit := mk__rr_type__resourcerecordtype(
           ttlinseconds := currentttl, class := 
           currentclass), recordlist := rrstring__23, 
           numberofrecordtypes := numberofrecordtypes__26, 
           recordtypes := recordtypes__26, numberofblocks := 
           numberofblocks__26, blocknumbers := blocknumbers__26, 
           blocklengths := blocklengths__26, bitmaps := bitmaps__26, 
           nextdomainname := rr_type__convertdomainnametowire(
           currentdomainname__25))) > 0 .
 

procedure_processfirstlineofrecord_40.
H1:    lastpos >= 1 .
H2:    lastpos <= rr_type__linelengthindex__last .
H3:    currentrecordtype >= dns_types__query_type__first .
H4:    currentrecordtype <= dns_types__query_type__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentorigin, [i___1]) >= character__first) and (element(
           currentorigin, [i___1]) <= character__last))) .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentowner, [i___1]) >= character__first) and (element(
           currentowner, [i___1]) <= character__last))) .
H7:    currentttl >= unsigned_types__unsigned32__first .
H8:    currentttl <= unsigned_types__unsigned32__last .
H9:    currentclass >= rr_type__classtype__first .
H10:   currentclass <= rr_type__classtype__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           currentline, [i___1]) >= character__first) and (element(
           currentline, [i___1]) <= character__last))) .
H12:   lastpos >= rr_type__linelengthindex__first .
H13:   lastpos <= rr_type__linelengthindex__last .
H14:   linecount >= unsigned_types__unsigned32__first .
H15:   linecount <= unsigned_types__unsigned32__last .
H16:   0 >= unsigned_types__unsigned32__first .
H17:   0 <= unsigned_types__unsigned32__last .
H18:   currentrecordtype = dns_types__nsec .
H19:   lastpos >= rr_type__linelengthindex__first .
H20:   lastpos <= rr_type__linelengthindex__last .
H21:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__23, [i___1]) >= character__first) and (element(
           currentdomainname__23, [i___1]) <= character__last))) .
H22:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(rrstring__23, [
           i___1]) >= character__first) and (element(rrstring__23, [
           i___1]) <= character__last))) .
H23:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__23, [i___1]) >= character__first) and (element(
           currentdomainname__23, [i___1]) <= character__last))) .
H24:   true .
H25:   not success__24 .
H26:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(rrstring__23, [
           i___1]) >= character__first) and (element(rrstring__23, [
           i___1]) <= character__last))) .
H27:   linecount >= unsigned_types__unsigned32__first .
H28:   linecount <= unsigned_types__unsigned32__last .
H29:   (success__26 = true) -> (numberofblocks__26 > 0) .
H30:   numberofrecordtypes__26 >= 
           rr_type__nsec_record_type__recordtypeindexvalue__first .
H31:   numberofrecordtypes__26 <= 
           rr_type__nsec_record_type__recordtypeindexvalue__last .
H32:   for_all(i___1: integer, ((i___1 >= 
           rr_type__nsec_record_type__recordtypearrayindex__first) and (
           i___1 <= 
           rr_type__nsec_record_type__recordtypearrayindex__last)) -> ((element(
           recordtypes__26, [i___1]) >= dns_types__query_type__first) and (element(
           recordtypes__26, [i___1]) <= dns_types__query_type__last))) .
H33:   numberofblocks__26 >= 
           rr_type__nsec_record_type__blocknumbervalue__first .
H34:   numberofblocks__26 <= 
           rr_type__nsec_record_type__blocknumbervalue__last .
H35:   for_all(i___1: integer, ((i___1 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___1 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           blocknumbers__26, [i___1]) >= dns_types__byte__first) and (element(
           blocknumbers__26, [i___1]) <= dns_types__byte__last))) .
H36:   for_all(i___1: integer, ((i___1 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___1 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           blocklengths__26, [i___1]) >= 
           rr_type__nsec_record_type__blocklengthvalue__first) and (element(
           blocklengths__26, [i___1]) <= 
           rr_type__nsec_record_type__blocklengthvalue__last))) .
H37:   for_all(i___1: integer, ((i___1 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___1 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__nsec_record_type__bitmapindex__first) and (
           i___2 <= rr_type__nsec_record_type__bitmapindex__last)) -> ((element(element(
           bitmaps__26, [i___1]), [i___2]) >= dns_types__byte__first) and (element(element(
           bitmaps__26, [i___1]), [i___2]) <= dns_types__byte__last))))) .
H38:   numberofblocks__26 >= 
           rr_type__nsec_record_type__blocknumbervalue__first .
H39:   numberofblocks__26 <= 
           rr_type__nsec_record_type__blocknumbervalue__last .
H40:   numberofrecordtypes__26 >= 
           rr_type__nsec_record_type__recordtypeindexvalue__first .
H41:   numberofrecordtypes__26 <= 
           rr_type__nsec_record_type__recordtypeindexvalue__last .
H42:   success__26 .
H43:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           rr_type__convertdomainnametowire(currentowner), [
           i___1]) >= character__first) and (element(
           rr_type__convertdomainnametowire(currentowner), [
           i___1]) <= character__last))) .
H44:   for_all(i_: integer, ((i_ >= 
           rr_type__domainnamestringtypeindex__first) and (
           i_ <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           rr_type__convertdomainnametowire(currentowner), [
           i_]) >= 0) and (element(
           rr_type__convertdomainnametowire(currentowner), [
           i_]) <= 255))) .
H45:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__23, [i___1]) >= character__first) and (element(
           currentdomainname__23, [i___1]) <= character__last))) .
H46:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(rrstring__23, [
           i___1]) >= character__first) and (element(rrstring__23, [
           i___1]) <= character__last))) .
H47:   numberofblocks__26 >= 
           rr_type__nsec_record_type__blocknumbervalue__first .
H48:   numberofblocks__26 <= 
           rr_type__nsec_record_type__blocknumbervalue__last .
H49:   numberofrecordtypes__26 >= 
           rr_type__nsec_record_type__recordtypeindexvalue__first .
H50:   numberofrecordtypes__26 <= 
           rr_type__nsec_record_type__recordtypeindexvalue__last .
H51:   for_all(i___1: integer, ((i___1 >= 
           rr_type__nsec_record_type__recordtypearrayindex__first) and (
           i___1 <= 
           rr_type__nsec_record_type__recordtypearrayindex__last)) -> ((element(
           recordtypes__26, [i___1]) >= dns_types__query_type__first) and (element(
           recordtypes__26, [i___1]) <= dns_types__query_type__last))) .
H52:   for_all(i___1: integer, ((i___1 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___1 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           blocknumbers__26, [i___1]) >= dns_types__byte__first) and (element(
           blocknumbers__26, [i___1]) <= dns_types__byte__last))) .
H53:   for_all(i___1: integer, ((i___1 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___1 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           blocklengths__26, [i___1]) >= 
           rr_type__nsec_record_type__blocklengthvalue__first) and (element(
           blocklengths__26, [i___1]) <= 
           rr_type__nsec_record_type__blocklengthvalue__last))) .
H54:   for_all(i___1: integer, ((i___1 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___1 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__nsec_record_type__bitmapindex__first) and (
           i___2 <= rr_type__nsec_record_type__bitmapindex__last)) -> ((element(element(
           bitmaps__26, [i___1]), [i___2]) >= dns_types__byte__first) and (element(element(
           bitmaps__26, [i___1]), [i___2]) <= dns_types__byte__last))))) .
H55:   numberofblocks__26 >= 
           rr_type__nsec_record_type__blocknumbervalue__first .
H56:   numberofblocks__26 <= 
           rr_type__nsec_record_type__blocknumbervalue__last .
H57:   numberofrecordtypes__26 >= 
           rr_type__nsec_record_type__recordtypeindexvalue__first .
H58:   numberofrecordtypes__26 <= 
           rr_type__nsec_record_type__recordtypeindexvalue__last .
H59:   currentclass >= rr_type__classtype__first .
H60:   currentclass <= rr_type__classtype__last .
H61:   currentttl >= unsigned_types__unsigned32__first .
H62:   currentttl <= unsigned_types__unsigned32__last .
H63:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           rr_type__convertdomainnametowire(currentdomainname__23), [
           i___1]) >= character__first) and (element(
           rr_type__convertdomainnametowire(currentdomainname__23), [
           i___1]) <= character__last))) .
H64:   for_all(i_: integer, ((i_ >= 
           rr_type__domainnamestringtypeindex__first) and (
           i_ <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           rr_type__convertdomainnametowire(currentdomainname__23), [
           i_]) >= 0) and (element(
           rr_type__convertdomainnametowire(currentdomainname__23), [
           i_]) <= 255))) .
        ->
C1:    fld_numberofblocks(
           mk__rr_type__nsec_record_type__nsecrecordtype(
           inherit := mk__rr_type__resourcerecordtype(
           ttlinseconds := currentttl, class := 
           currentclass), recordlist := rrstring__23, 
           numberofrecordtypes := numberofrecordtypes__26, 
           recordtypes := recordtypes__26, numberofblocks := 
           numberofblocks__26, blocknumbers := blocknumbers__26, 
           blocklengths := blocklengths__26, bitmaps := bitmaps__26, 
           nextdomainname := rr_type__convertdomainnametowire(
           currentdomainname__23))) > 0 .
 

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

procedure_processfirstlineofrecord_41.
H1:    lastpos >= 1 .
H2:    lastpos <= rr_type__linelengthindex__last .
H3:    currentrecordtype >= dns_types__query_type__first .
H4:    currentrecordtype <= dns_types__query_type__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentorigin, [i___1]) >= character__first) and (element(
           currentorigin, [i___1]) <= character__last))) .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentowner, [i___1]) >= character__first) and (element(
           currentowner, [i___1]) <= character__last))) .
H7:    currentttl >= unsigned_types__unsigned32__first .
H8:    currentttl <= unsigned_types__unsigned32__last .
H9:    currentclass >= rr_type__classtype__first .
H10:   currentclass <= rr_type__classtype__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           currentline, [i___1]) >= character__first) and (element(
           currentline, [i___1]) <= character__last))) .
H12:   lastpos >= rr_type__linelengthindex__first .
H13:   lastpos <= rr_type__linelengthindex__last .
H14:   linecount >= unsigned_types__unsigned32__first .
H15:   linecount <= unsigned_types__unsigned32__last .
H16:   0 >= unsigned_types__unsigned32__first .
H17:   0 <= unsigned_types__unsigned32__last .
H18:   currentrecordtype = dns_types__nsec .
H19:   lastpos >= rr_type__linelengthindex__first .
H20:   lastpos <= rr_type__linelengthindex__last .
H21:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__23, [i___1]) >= character__first) and (element(
           currentdomainname__23, [i___1]) <= character__last))) .
H22:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(rrstring__23, [
           i___1]) >= character__first) and (element(rrstring__23, [
           i___1]) <= character__last))) .
H23:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__23, [i___1]) >= character__first) and (element(
           currentdomainname__23, [i___1]) <= character__last))) .
H24:   true .
H25:   success__24 .
H26:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__23, [i___1]) >= character__first) and (element(
           currentdomainname__23, [i___1]) <= character__last))) .
H27:   linecount >= unsigned_types__unsigned32__first .
H28:   linecount <= unsigned_types__unsigned32__last .
H29:   lastpos >= rr_type__linelengthindex__first .
H30:   lastpos <= rr_type__linelengthindex__last .
H31:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__25, [i___1]) >= character__first) and (element(
           currentdomainname__25, [i___1]) <= character__last))) .
H32:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(rrstring__23, [
           i___1]) >= character__first) and (element(rrstring__23, [
           i___1]) <= character__last))) .
H33:   linecount >= unsigned_types__unsigned32__first .
H34:   linecount <= unsigned_types__unsigned32__last .
H35:   (success__26 = true) -> (numberofblocks__26 > 0) .
H36:   numberofrecordtypes__26 >= 
           rr_type__nsec_record_type__recordtypeindexvalue__first .
H37:   numberofrecordtypes__26 <= 
           rr_type__nsec_record_type__recordtypeindexvalue__last .
H38:   for_all(i___1: integer, ((i___1 >= 
           rr_type__nsec_record_type__recordtypearrayindex__first) and (
           i___1 <= 
           rr_type__nsec_record_type__recordtypearrayindex__last)) -> ((element(
           recordtypes__26, [i___1]) >= dns_types__query_type__first) and (element(
           recordtypes__26, [i___1]) <= dns_types__query_type__last))) .
H39:   numberofblocks__26 >= 
           rr_type__nsec_record_type__blocknumbervalue__first .
H40:   numberofblocks__26 <= 
           rr_type__nsec_record_type__blocknumbervalue__last .
H41:   for_all(i___1: integer, ((i___1 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___1 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           blocknumbers__26, [i___1]) >= dns_types__byte__first) and (element(
           blocknumbers__26, [i___1]) <= dns_types__byte__last))) .
H42:   for_all(i___1: integer, ((i___1 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___1 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           blocklengths__26, [i___1]) >= 
           rr_type__nsec_record_type__blocklengthvalue__first) and (element(
           blocklengths__26, [i___1]) <= 
           rr_type__nsec_record_type__blocklengthvalue__last))) .
H43:   for_all(i___1: integer, ((i___1 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___1 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__nsec_record_type__bitmapindex__first) and (
           i___2 <= rr_type__nsec_record_type__bitmapindex__last)) -> ((element(element(
           bitmaps__26, [i___1]), [i___2]) >= dns_types__byte__first) and (element(element(
           bitmaps__26, [i___1]), [i___2]) <= dns_types__byte__last))))) .
H44:   numberofblocks__26 >= 
           rr_type__nsec_record_type__blocknumbervalue__first .
H45:   numberofblocks__26 <= 
           rr_type__nsec_record_type__blocknumbervalue__last .
H46:   numberofrecordtypes__26 >= 
           rr_type__nsec_record_type__recordtypeindexvalue__first .
H47:   numberofrecordtypes__26 <= 
           rr_type__nsec_record_type__recordtypeindexvalue__last .
H48:   not success__26 .
        ->
C1:    linecount >= unsigned_types__unsigned32__first .
C2:    linecount <= unsigned_types__unsigned32__last .
C3:    lastpos >= natural__first .
C4:    lastpos <= natural__last .
 

procedure_processfirstlineofrecord_42.
H1:    lastpos >= 1 .
H2:    lastpos <= rr_type__linelengthindex__last .
H3:    currentrecordtype >= dns_types__query_type__first .
H4:    currentrecordtype <= dns_types__query_type__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentorigin, [i___1]) >= character__first) and (element(
           currentorigin, [i___1]) <= character__last))) .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentowner, [i___1]) >= character__first) and (element(
           currentowner, [i___1]) <= character__last))) .
H7:    currentttl >= unsigned_types__unsigned32__first .
H8:    currentttl <= unsigned_types__unsigned32__last .
H9:    currentclass >= rr_type__classtype__first .
H10:   currentclass <= rr_type__classtype__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           currentline, [i___1]) >= character__first) and (element(
           currentline, [i___1]) <= character__last))) .
H12:   lastpos >= rr_type__linelengthindex__first .
H13:   lastpos <= rr_type__linelengthindex__last .
H14:   linecount >= unsigned_types__unsigned32__first .
H15:   linecount <= unsigned_types__unsigned32__last .
H16:   0 >= unsigned_types__unsigned32__first .
H17:   0 <= unsigned_types__unsigned32__last .
H18:   currentrecordtype = dns_types__nsec .
H19:   lastpos >= rr_type__linelengthindex__first .
H20:   lastpos <= rr_type__linelengthindex__last .
H21:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__23, [i___1]) >= character__first) and (element(
           currentdomainname__23, [i___1]) <= character__last))) .
H22:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(rrstring__23, [
           i___1]) >= character__first) and (element(rrstring__23, [
           i___1]) <= character__last))) .
H23:   for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentdomainname__23, [i___1]) >= character__first) and (element(
           currentdomainname__23, [i___1]) <= character__last))) .
H24:   true .
H25:   not success__24 .
H26:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(rrstring__23, [
           i___1]) >= character__first) and (element(rrstring__23, [
           i___1]) <= character__last))) .
H27:   linecount >= unsigned_types__unsigned32__first .
H28:   linecount <= unsigned_types__unsigned32__last .
H29:   (success__26 = true) -> (numberofblocks__26 > 0) .
H30:   numberofrecordtypes__26 >= 
           rr_type__nsec_record_type__recordtypeindexvalue__first .
H31:   numberofrecordtypes__26 <= 
           rr_type__nsec_record_type__recordtypeindexvalue__last .
H32:   for_all(i___1: integer, ((i___1 >= 
           rr_type__nsec_record_type__recordtypearrayindex__first) and (
           i___1 <= 
           rr_type__nsec_record_type__recordtypearrayindex__last)) -> ((element(
           recordtypes__26, [i___1]) >= dns_types__query_type__first) and (element(
           recordtypes__26, [i___1]) <= dns_types__query_type__last))) .
H33:   numberofblocks__26 >= 
           rr_type__nsec_record_type__blocknumbervalue__first .
H34:   numberofblocks__26 <= 
           rr_type__nsec_record_type__blocknumbervalue__last .
H35:   for_all(i___1: integer, ((i___1 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___1 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           blocknumbers__26, [i___1]) >= dns_types__byte__first) and (element(
           blocknumbers__26, [i___1]) <= dns_types__byte__last))) .
H36:   for_all(i___1: integer, ((i___1 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___1 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           blocklengths__26, [i___1]) >= 
           rr_type__nsec_record_type__blocklengthvalue__first) and (element(
           blocklengths__26, [i___1]) <= 
           rr_type__nsec_record_type__blocklengthvalue__last))) .
H37:   for_all(i___1: integer, ((i___1 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___1 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__nsec_record_type__bitmapindex__first) and (
           i___2 <= rr_type__nsec_record_type__bitmapindex__last)) -> ((element(element(
           bitmaps__26, [i___1]), [i___2]) >= dns_types__byte__first) and (element(element(
           bitmaps__26, [i___1]), [i___2]) <= dns_types__byte__last))))) .
H38:   numberofblocks__26 >= 
           rr_type__nsec_record_type__blocknumbervalue__first .
H39:   numberofblocks__26 <= 
           rr_type__nsec_record_type__blocknumbervalue__last .
H40:   numberofrecordtypes__26 >= 
           rr_type__nsec_record_type__recordtypeindexvalue__first .
H41:   numberofrecordtypes__26 <= 
           rr_type__nsec_record_type__recordtypeindexvalue__last .
H42:   not success__26 .
        ->
C1:    linecount >= unsigned_types__unsigned32__first .
C2:    linecount <= unsigned_types__unsigned32__last .
C3:    lastpos >= natural__first .
C4:    lastpos <= natural__last .
 

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

procedure_processfirstlineofrecord_43.
H1:    lastpos >= 1 .
H2:    lastpos <= rr_type__linelengthindex__last .
H3:    currentrecordtype >= dns_types__query_type__first .
H4:    currentrecordtype <= dns_types__query_type__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentorigin, [i___1]) >= character__first) and (element(
           currentorigin, [i___1]) <= character__last))) .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentowner, [i___1]) >= character__first) and (element(
           currentowner, [i___1]) <= character__last))) .
H7:    currentttl >= unsigned_types__unsigned32__first .
H8:    currentttl <= unsigned_types__unsigned32__last .
H9:    currentclass >= rr_type__classtype__first .
H10:   currentclass <= rr_type__classtype__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           currentline, [i___1]) >= character__first) and (element(
           currentline, [i___1]) <= character__last))) .
H12:   lastpos >= rr_type__linelengthindex__first .
H13:   lastpos <= rr_type__linelengthindex__last .
H14:   linecount >= unsigned_types__unsigned32__first .
H15:   linecount <= unsigned_types__unsigned32__last .
H16:   0 >= unsigned_types__unsigned32__first .
H17:   0 <= unsigned_types__unsigned32__last .
H18:   currentrecordtype = dns_types__rrsig .
        ->
C1:    0 >= unsigned_types__unsigned32__first .
C2:    0 <= unsigned_types__unsigned32__last .
 

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

procedure_processfirstlineofrecord_44.
H1:    lastpos >= 1 .
H2:    lastpos <= rr_type__linelengthindex__last .
H3:    currentrecordtype >= dns_types__query_type__first .
H4:    currentrecordtype <= dns_types__query_type__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentorigin, [i___1]) >= character__first) and (element(
           currentorigin, [i___1]) <= character__last))) .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentowner, [i___1]) >= character__first) and (element(
           currentowner, [i___1]) <= character__last))) .
H7:    currentttl >= unsigned_types__unsigned32__first .
H8:    currentttl <= unsigned_types__unsigned32__last .
H9:    currentclass >= rr_type__classtype__first .
H10:   currentclass <= rr_type__classtype__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           currentline, [i___1]) >= character__first) and (element(
           currentline, [i___1]) <= character__last))) .
H12:   lastpos >= rr_type__linelengthindex__first .
H13:   lastpos <= rr_type__linelengthindex__last .
H14:   linecount >= unsigned_types__unsigned32__first .
H15:   linecount <= unsigned_types__unsigned32__last .
H16:   0 >= unsigned_types__unsigned32__first .
H17:   0 <= unsigned_types__unsigned32__last .
H18:   currentrecordtype = dns_types__rrsig .
H19:   0 >= unsigned_types__unsigned32__first .
H20:   0 <= unsigned_types__unsigned32__last .
        ->
C1:    lastpos >= rr_type__linelengthindex__first .
C2:    lastpos <= rr_type__linelengthindex__last .
 

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

procedure_processfirstlineofrecord_45.
H1:    lastpos >= 1 .
H2:    lastpos <= rr_type__linelengthindex__last .
H3:    currentrecordtype >= dns_types__query_type__first .
H4:    currentrecordtype <= dns_types__query_type__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentorigin, [i___1]) >= character__first) and (element(
           currentorigin, [i___1]) <= character__last))) .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__domainnamestringtypeindex__first) and (
           i___1 <= rr_type__domainnamestringtypeindex__last)) -> ((element(
           currentowner, [i___1]) >= character__first) and (element(
           currentowner, [i___1]) <= character__last))) .
H7:    currentttl >= unsigned_types__unsigned32__first .
H8:    currentttl <= unsigned_types__unsigned32__last .
H9:    currentclass >= rr_type__classtype__first .
H10:   currentclass <= rr_type__classtype__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(
           currentline, [i___1]) >= character__first) and (element(
           currentline, [i___1]) <= character__last))) .
H12:   lastpos >= rr_type__linelengthindex__first .
H13:   lastpos <= rr_type__linelengthindex__last .
H14:   linecount >= unsigned_types__unsigned32__first .
H15:   linecount <= unsigned_types__unsigned32__last .
H16:   0 >= unsigned_types__unsigned32__first .
H17:   0 <= unsigned_types__unsigned32__last .
H18:   not (currentrecordtype = dns_types__a) .
H19:   not (currentrecordtype = dns_types__aaaa) .
H20:   not (currentrecordtype = dns_types__cname) .
H21:   not (currentrecordtype = dns_types__mx) .
H22:   not (currentrecordtype = dns_types__ns) .
H23:   not (currentrecordtype = dns_types__ptr) .
H24:   not (currentrecordtype = dns_types__soa) .
H25:   not (currentrecordtype = dns_types__dnskey) .
H26:   not (currentrecordtype = dns_types__nsec) .
H27:   not (currentrecordtype = dns_types__rrsig) .
        ->
C1:    linecount >= unsigned_types__unsigned32__first .
C2:    linecount <= unsigned_types__unsigned32__last .
C3:    lastpos >= natural__first .
C4:    lastpos <= natural__last .
 

For path(s) from start to finish:

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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


