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

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


              procedure Process_Dns_Request.Create_Response_A




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

procedure_create_response_a_1.
H1:    answer_count <= dns_types__unsigned_short__last - 
           rr_type__maxnumrecords .
H2:    start_byte <= dns_types__packet_size .
H3:    start_byte >= dns_types__packet_bytes_range__first .
H4:    start_byte <= dns_types__packet_bytes_range__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           domainname, [i___1]) >= character__first) and (element(
           domainname, [i___1]) <= character__last))) .
H6:    qname_location >= dns_types__qname_ptr_range__first .
H7:    qname_location <= dns_types__qname_ptr_range__last .
H8:    fld_messageid(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H9:    fld_messageid(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H10:   fld_opcode(fld_header(output_packet)) >= 
           dns_types__opcode_type__first .
H11:   fld_opcode(fld_header(output_packet)) <= 
           dns_types__opcode_type__last .
H12:   fld_rcode(fld_header(output_packet)) >= 
           dns_types__response_code__first .
H13:   fld_rcode(fld_header(output_packet)) <= 
           dns_types__response_code__last .
H14:   fld_qdcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H15:   fld_qdcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H16:   fld_ancount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H17:   fld_ancount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H18:   fld_nscount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H19:   fld_nscount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H20:   fld_arcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H21:   fld_arcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H22:   for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           fld_bytes(output_packet), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           output_packet), [i___1]) <= dns_types__byte__last))) .
H23:   answer_count >= dns_types__unsigned_short__first .
H24:   answer_count <= dns_types__unsigned_short__last .
H25:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_ttlinseconds(fld_inherit(element(returnedarecords__1, [
           i___1]))) >= unsigned_types__unsigned32__first) and (
           fld_ttlinseconds(fld_inherit(element(returnedarecords__1, [
           i___1]))) <= unsigned_types__unsigned32__last))) .
H26:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_class(fld_inherit(element(returnedarecords__1, [
           i___1]))) >= rr_type__classtype__first) and (fld_class(
           fld_inherit(element(returnedarecords__1, [i___1]))) <= 
           rr_type__classtype__last))) .
H27:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_ipv4(element(returnedarecords__1, [i___1])) >= 
           unsigned_types__unsigned32__first) and (fld_ipv4(element(
           returnedarecords__1, [i___1])) <= 
           unsigned_types__unsigned32__last))) .
H28:   numfound__1 >= rr_type__numberofrecordstype__first .
H29:   numfound__1 <= rr_type__numberofrecordstype__last .
        ->
C1:    numfound__1 >= natural__first .
C2:    numfound__1 <= natural__last .
 

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

procedure_create_response_a_2.
H1:    answer_count <= dns_types__unsigned_short__last - 
           rr_type__maxnumrecords .
H2:    start_byte <= dns_types__packet_size .
H3:    start_byte >= dns_types__packet_bytes_range__first .
H4:    start_byte <= dns_types__packet_bytes_range__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           domainname, [i___1]) >= character__first) and (element(
           domainname, [i___1]) <= character__last))) .
H6:    qname_location >= dns_types__qname_ptr_range__first .
H7:    qname_location <= dns_types__qname_ptr_range__last .
H8:    fld_messageid(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H9:    fld_messageid(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H10:   fld_opcode(fld_header(output_packet)) >= 
           dns_types__opcode_type__first .
H11:   fld_opcode(fld_header(output_packet)) <= 
           dns_types__opcode_type__last .
H12:   fld_rcode(fld_header(output_packet)) >= 
           dns_types__response_code__first .
H13:   fld_rcode(fld_header(output_packet)) <= 
           dns_types__response_code__last .
H14:   fld_qdcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H15:   fld_qdcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H16:   fld_ancount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H17:   fld_ancount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H18:   fld_nscount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H19:   fld_nscount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H20:   fld_arcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H21:   fld_arcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H22:   for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           fld_bytes(output_packet), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           output_packet), [i___1]) <= dns_types__byte__last))) .
H23:   answer_count >= dns_types__unsigned_short__first .
H24:   answer_count <= dns_types__unsigned_short__last .
H25:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_ttlinseconds(fld_inherit(element(returnedarecords__1, [
           i___1]))) >= unsigned_types__unsigned32__first) and (
           fld_ttlinseconds(fld_inherit(element(returnedarecords__1, [
           i___1]))) <= unsigned_types__unsigned32__last))) .
H26:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_class(fld_inherit(element(returnedarecords__1, [
           i___1]))) >= rr_type__classtype__first) and (fld_class(
           fld_inherit(element(returnedarecords__1, [i___1]))) <= 
           rr_type__classtype__last))) .
H27:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_ipv4(element(returnedarecords__1, [i___1])) >= 
           unsigned_types__unsigned32__first) and (fld_ipv4(element(
           returnedarecords__1, [i___1])) <= 
           unsigned_types__unsigned32__last))) .
H28:   numfound__1 >= rr_type__numberofrecordstype__first .
H29:   numfound__1 <= rr_type__numberofrecordstype__last .
H30:   numfound__1 >= natural__first .
H31:   numfound__1 <= natural__last .
        ->
C1:    start_byte >= dns_types__packet_bytes_range__first .
C2:    start_byte <= dns_types__packet_bytes_range__last .
 

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

procedure_create_response_a_3.
H1:    answer_count <= dns_types__unsigned_short__last - 
           rr_type__maxnumrecords .
H2:    start_byte <= dns_types__packet_size .
H3:    start_byte >= dns_types__packet_bytes_range__first .
H4:    start_byte <= dns_types__packet_bytes_range__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           domainname, [i___1]) >= character__first) and (element(
           domainname, [i___1]) <= character__last))) .
H6:    qname_location >= dns_types__qname_ptr_range__first .
H7:    qname_location <= dns_types__qname_ptr_range__last .
H8:    fld_messageid(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H9:    fld_messageid(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H10:   fld_opcode(fld_header(output_packet)) >= 
           dns_types__opcode_type__first .
H11:   fld_opcode(fld_header(output_packet)) <= 
           dns_types__opcode_type__last .
H12:   fld_rcode(fld_header(output_packet)) >= 
           dns_types__response_code__first .
H13:   fld_rcode(fld_header(output_packet)) <= 
           dns_types__response_code__last .
H14:   fld_qdcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H15:   fld_qdcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H16:   fld_ancount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H17:   fld_ancount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H18:   fld_nscount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H19:   fld_nscount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H20:   fld_arcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H21:   fld_arcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H22:   for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           fld_bytes(output_packet), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           output_packet), [i___1]) <= dns_types__byte__last))) .
H23:   answer_count >= dns_types__unsigned_short__first .
H24:   answer_count <= dns_types__unsigned_short__last .
H25:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_ttlinseconds(fld_inherit(element(returnedarecords__1, [
           i___1]))) >= unsigned_types__unsigned32__first) and (
           fld_ttlinseconds(fld_inherit(element(returnedarecords__1, [
           i___1]))) <= unsigned_types__unsigned32__last))) .
H26:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_class(fld_inherit(element(returnedarecords__1, [
           i___1]))) >= rr_type__classtype__first) and (fld_class(
           fld_inherit(element(returnedarecords__1, [i___1]))) <= 
           rr_type__classtype__last))) .
H27:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_ipv4(element(returnedarecords__1, [i___1])) >= 
           unsigned_types__unsigned32__first) and (fld_ipv4(element(
           returnedarecords__1, [i___1])) <= 
           unsigned_types__unsigned32__last))) .
H28:   numfound__1 >= rr_type__numberofrecordstype__first .
H29:   numfound__1 <= rr_type__numberofrecordstype__last .
H30:   numfound__1 >= natural__first .
H31:   numfound__1 <= natural__last .
H32:   start_byte >= dns_types__packet_bytes_range__first .
H33:   start_byte <= dns_types__packet_bytes_range__last .
H34:   numfound__1 >= natural__first .
H35:   numfound__1 <= natural__last .
H36:   numfound__1 >= 1 .
        ->
C1:    1 >= natural__first .
C2:    1 <= natural__last .
 

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

procedure_create_response_a_4.
H1:    answer_count <= dns_types__unsigned_short__last - 
           rr_type__maxnumrecords .
H2:    start_byte <= dns_types__packet_size .
H3:    start_byte >= dns_types__packet_bytes_range__first .
H4:    start_byte <= dns_types__packet_bytes_range__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           domainname, [i___1]) >= character__first) and (element(
           domainname, [i___1]) <= character__last))) .
H6:    qname_location >= dns_types__qname_ptr_range__first .
H7:    qname_location <= dns_types__qname_ptr_range__last .
H8:    fld_messageid(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H9:    fld_messageid(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H10:   fld_opcode(fld_header(output_packet)) >= 
           dns_types__opcode_type__first .
H11:   fld_opcode(fld_header(output_packet)) <= 
           dns_types__opcode_type__last .
H12:   fld_rcode(fld_header(output_packet)) >= 
           dns_types__response_code__first .
H13:   fld_rcode(fld_header(output_packet)) <= 
           dns_types__response_code__last .
H14:   fld_qdcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H15:   fld_qdcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H16:   fld_ancount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H17:   fld_ancount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H18:   fld_nscount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H19:   fld_nscount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H20:   fld_arcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H21:   fld_arcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H22:   for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           fld_bytes(output_packet), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           output_packet), [i___1]) <= dns_types__byte__last))) .
H23:   answer_count >= dns_types__unsigned_short__first .
H24:   answer_count <= dns_types__unsigned_short__last .
H25:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_ttlinseconds(fld_inherit(element(returnedarecords__1, [
           i___1]))) >= unsigned_types__unsigned32__first) and (
           fld_ttlinseconds(fld_inherit(element(returnedarecords__1, [
           i___1]))) <= unsigned_types__unsigned32__last))) .
H26:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_class(fld_inherit(element(returnedarecords__1, [
           i___1]))) >= rr_type__classtype__first) and (fld_class(
           fld_inherit(element(returnedarecords__1, [i___1]))) <= 
           rr_type__classtype__last))) .
H27:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_ipv4(element(returnedarecords__1, [i___1])) >= 
           unsigned_types__unsigned32__first) and (fld_ipv4(element(
           returnedarecords__1, [i___1])) <= 
           unsigned_types__unsigned32__last))) .
H28:   numfound__1 >= rr_type__numberofrecordstype__first .
H29:   numfound__1 <= rr_type__numberofrecordstype__last .
H30:   numfound__1 >= natural__first .
H31:   numfound__1 <= natural__last .
H32:   start_byte >= dns_types__packet_bytes_range__first .
H33:   start_byte <= dns_types__packet_bytes_range__last .
H34:   numfound__1 >= natural__first .
H35:   numfound__1 <= natural__last .
H36:   numfound__1 >= 1 .
H37:   1 >= natural__first .
H38:   1 <= natural__last .
H39:   start_byte >= dns_types__packet_bytes_range__first .
H40:   start_byte <= dns_types__packet_bytes_range__last .
H41:   numfound__1 >= natural__first .
H42:   numfound__1 <= natural__last .
H43:   1 >= natural__first .
H44:   1 <= natural__last .
        ->
C1:    dns_types__packet_size - (16 + dns_types__header_bits div 8) >= system__min_int .
C2:    dns_types__packet_size - (16 + dns_types__header_bits div 8) <= system__max_int .
C3:    16 + dns_types__header_bits div 8 >= system__min_int .
C4:    16 + dns_types__header_bits div 8 <= system__max_int .
C5:    dns_types__header_bits div 8 >= system__min_int .
C6:    dns_types__header_bits div 8 <= system__max_int .
C7:    8 <> 0 .
C8:    start_byte >= integer__first .
C9:    start_byte <= integer__last .
 

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

procedure_create_response_a_5.
H1:    response_counter >= 1 .
H2:    response_counter <= numfound .
H3:    start_byte <= dns_types__packet_size .
H4:    answer_count = answer_count~ .
H5:    answer_count <= dns_types__unsigned_short__last - 
           rr_type__maxnumrecords .
H6:    current_byte = start_byte + 16 * (response_counter - 1) .
H7:    current_byte < dns_types__packet_size - (16 + 
           dns_types__header_bits div 8) .
H8:    numfound <= rr_type__maxnumrecords .
H9:    start_byte >= dns_types__packet_bytes_range__first .
H10:   start_byte <= dns_types__packet_bytes_range__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           domainname, [i___1]) >= character__first) and (element(
           domainname, [i___1]) <= character__last))) .
H12:   qname_location >= dns_types__qname_ptr_range__first .
H13:   qname_location <= dns_types__qname_ptr_range__last .
H14:   fld_messageid(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H15:   fld_messageid(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H16:   fld_opcode(fld_header(output_packet)) >= 
           dns_types__opcode_type__first .
H17:   fld_opcode(fld_header(output_packet)) <= 
           dns_types__opcode_type__last .
H18:   fld_rcode(fld_header(output_packet)) >= 
           dns_types__response_code__first .
H19:   fld_rcode(fld_header(output_packet)) <= 
           dns_types__response_code__last .
H20:   fld_qdcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H21:   fld_qdcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H22:   fld_ancount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H23:   fld_ancount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H24:   fld_nscount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H25:   fld_nscount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H26:   fld_arcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H27:   fld_arcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H28:   for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           fld_bytes(output_packet), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           output_packet), [i___1]) <= dns_types__byte__last))) .
H29:   answer_count >= dns_types__unsigned_short__first .
H30:   answer_count <= dns_types__unsigned_short__last .
H31:   answer_count~ <= dns_types__unsigned_short__last - 
           rr_type__maxnumrecords .
H32:   start_byte <= dns_types__packet_size .
H33:   current_byte >= dns_types__packet_bytes_range__first .
H34:   current_byte <= dns_types__packet_bytes_range__last .
H35:   (qname_location + 49152) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H36:   (qname_location + 49152) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H37:   current_byte + 1 >= dns_types__packet_bytes_range__first .
H38:   current_byte + 1 <= dns_types__packet_bytes_range__last .
H39:   current_byte + 1 <= dns_types__packet_bytes_range__last - 1 .
H40:   qname_location >= unsigned_types__unsigned16__first .
H41:   qname_location <= unsigned_types__unsigned16__last .
H42:   current_byte + 1 >= dns_types__packet_bytes_range__base__first .
H43:   current_byte + 1 <= dns_types__packet_bytes_range__base__last .
H44:   for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           fld_bytes(output_packet__2), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           output_packet__2), [i___1]) <= dns_types__byte__last))) .
H45:   fld_header(output_packet__2) = fld_header(
           output_packet) .
H46:   output_packet__2 = upf_bytes(output_packet, fld_bytes(
           output_packet__2)) .
H47:   0 >= dns_types__byte__first .
H48:   0 <= dns_types__byte__last .
H49:   current_byte + 3 >= dns_types__packet_bytes_range__first .
H50:   current_byte + 3 <= dns_types__packet_bytes_range__last .
H51:   current_byte + 3 >= dns_types__packet_bytes_range__base__first .
H52:   current_byte + 3 <= dns_types__packet_bytes_range__base__last .
H53:   1 >= dns_types__byte__first .
H54:   1 <= dns_types__byte__last .
H55:   current_byte + 4 >= dns_types__packet_bytes_range__first .
H56:   current_byte + 4 <= dns_types__packet_bytes_range__last .
H57:   current_byte + 4 >= dns_types__packet_bytes_range__base__first .
H58:   current_byte + 4 <= dns_types__packet_bytes_range__base__last .
H59:   0 >= dns_types__byte__first .
H60:   0 <= dns_types__byte__last .
H61:   current_byte + 5 >= dns_types__packet_bytes_range__first .
H62:   current_byte + 5 <= dns_types__packet_bytes_range__last .
H63:   current_byte + 5 >= dns_types__packet_bytes_range__base__first .
H64:   current_byte + 5 <= dns_types__packet_bytes_range__base__last .
H65:   1 >= dns_types__byte__first .
H66:   1 <= dns_types__byte__last .
H67:   current_byte + 6 >= dns_types__packet_bytes_range__first .
H68:   current_byte + 6 <= dns_types__packet_bytes_range__last .
H69:   current_byte + 6 >= dns_types__packet_bytes_range__base__first .
H70:   current_byte + 6 <= dns_types__packet_bytes_range__base__last .
H71:   current_byte >= dns_types__packet_bytes_range__first .
H72:   current_byte <= dns_types__packet_bytes_range__last .
H73:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_ttlinseconds(fld_inherit(element(
           returnedarecords, [i___1]))) >= 
           unsigned_types__unsigned32__first) and (fld_ttlinseconds(
           fld_inherit(element(returnedarecords, [i___1]))) <= 
           unsigned_types__unsigned32__last))) .
H74:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_class(fld_inherit(element(returnedarecords, [
           i___1]))) >= rr_type__classtype__first) and (fld_class(
           fld_inherit(element(returnedarecords, [i___1]))) <= 
           rr_type__classtype__last))) .
H75:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_ipv4(element(returnedarecords, [i___1])) >= 
           unsigned_types__unsigned32__first) and (fld_ipv4(element(
           returnedarecords, [i___1])) <= 
           unsigned_types__unsigned32__last))) .
H76:   response_counter >= natural__first .
H77:   response_counter <= natural__last .
H78:   current_byte + 7 >= dns_types__packet_bytes_range__first .
H79:   current_byte + 7 <= dns_types__packet_bytes_range__last .
H80:   current_byte + 7 <= dns_types__packet_bytes_range__last - 10 .
H81:   rr_type__returnedrecordsindextype__first + (
           response_counter - 1) >= 
           rr_type__returnedrecordsindextype__first .
H82:   rr_type__returnedrecordsindextype__first + (
           response_counter - 1) <= 
           rr_type__returnedrecordsindextype__last .
H83:   rr_type__returnedrecordsindextype__first + (
           response_counter - 1) >= integer__base__first .
H84:   rr_type__returnedrecordsindextype__first + (
           response_counter - 1) <= integer__base__last .
H85:   response_counter - 1 >= integer__base__first .
H86:   response_counter - 1 <= integer__base__last .
H87:   current_byte + 7 >= dns_types__packet_bytes_range__base__first .
H88:   current_byte + 7 <= dns_types__packet_bytes_range__base__last .
H89:   for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           fld_bytes(output_packet__3), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           output_packet__3), [i___1]) <= dns_types__byte__last))) .
H90:   fld_header(output_packet__3) = fld_header(upf_bytes(upf_bytes(
           upf_bytes(upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0)), update(fld_bytes(
           upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0))), [
           current_byte + 4], 1)), update(fld_bytes(upf_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0)), update(fld_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0))), [current_byte + 4], 1))), [
           current_byte + 5], 0)), update(fld_bytes(upf_bytes(upf_bytes(
           upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0)), update(fld_bytes(
           upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0))), [
           current_byte + 4], 1)), update(fld_bytes(upf_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0)), update(fld_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0))), [current_byte + 4], 1))), [
           current_byte + 5], 0))), [current_byte + 6], 1))) .
H91:   output_packet__3 = upf_bytes(upf_bytes(upf_bytes(upf_bytes(
           upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0)), update(fld_bytes(
           upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0))), [
           current_byte + 4], 1)), update(fld_bytes(upf_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0)), update(fld_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0))), [current_byte + 4], 1))), [
           current_byte + 5], 0)), update(fld_bytes(upf_bytes(upf_bytes(
           upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0)), update(fld_bytes(
           upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0))), [
           current_byte + 4], 1)), update(fld_bytes(upf_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0)), update(fld_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0))), [current_byte + 4], 1))), [
           current_byte + 5], 0))), [current_byte + 6], 1)), fld_bytes(
           output_packet__3)) .
H92:   response_counter >= natural__first .
H93:   response_counter <= natural__last .
H94:   response_counter + 1 >= natural__first .
H95:   response_counter + 1 <= natural__last .
H96:   current_byte >= dns_types__packet_bytes_range__first .
H97:   current_byte <= dns_types__packet_bytes_range__last .
H98:   current_byte + 16 >= dns_types__packet_bytes_range__first .
H99:   current_byte + 16 <= dns_types__packet_bytes_range__last .
H100:  current_byte + 16 >= dns_types__packet_bytes_range__first .
H101:  current_byte + 16 <= dns_types__packet_bytes_range__last .
H102:  numfound >= natural__first .
H103:  numfound <= natural__last .
H104:  response_counter + 1 >= natural__first .
H105:  response_counter + 1 <= natural__last .
        ->
C1:    dns_types__packet_size - (16 + dns_types__header_bits div 8) >= system__min_int .
C2:    dns_types__packet_size - (16 + dns_types__header_bits div 8) <= system__max_int .
C3:    16 + dns_types__header_bits div 8 >= system__min_int .
C4:    16 + dns_types__header_bits div 8 <= system__max_int .
C5:    dns_types__header_bits div 8 >= system__min_int .
C6:    dns_types__header_bits div 8 <= system__max_int .
C7:    8 <> 0 .
C8:    current_byte + 16 >= integer__first .
C9:    current_byte + 16 <= integer__last .
 

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

procedure_create_response_a_6.
H1:    answer_count <= dns_types__unsigned_short__last - 
           rr_type__maxnumrecords .
H2:    start_byte <= dns_types__packet_size .
H3:    start_byte >= dns_types__packet_bytes_range__first .
H4:    start_byte <= dns_types__packet_bytes_range__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           domainname, [i___1]) >= character__first) and (element(
           domainname, [i___1]) <= character__last))) .
H6:    qname_location >= dns_types__qname_ptr_range__first .
H7:    qname_location <= dns_types__qname_ptr_range__last .
H8:    fld_messageid(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H9:    fld_messageid(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H10:   fld_opcode(fld_header(output_packet)) >= 
           dns_types__opcode_type__first .
H11:   fld_opcode(fld_header(output_packet)) <= 
           dns_types__opcode_type__last .
H12:   fld_rcode(fld_header(output_packet)) >= 
           dns_types__response_code__first .
H13:   fld_rcode(fld_header(output_packet)) <= 
           dns_types__response_code__last .
H14:   fld_qdcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H15:   fld_qdcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H16:   fld_ancount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H17:   fld_ancount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H18:   fld_nscount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H19:   fld_nscount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H20:   fld_arcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H21:   fld_arcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H22:   for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           fld_bytes(output_packet), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           output_packet), [i___1]) <= dns_types__byte__last))) .
H23:   answer_count >= dns_types__unsigned_short__first .
H24:   answer_count <= dns_types__unsigned_short__last .
H25:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_ttlinseconds(fld_inherit(element(returnedarecords__1, [
           i___1]))) >= unsigned_types__unsigned32__first) and (
           fld_ttlinseconds(fld_inherit(element(returnedarecords__1, [
           i___1]))) <= unsigned_types__unsigned32__last))) .
H26:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_class(fld_inherit(element(returnedarecords__1, [
           i___1]))) >= rr_type__classtype__first) and (fld_class(
           fld_inherit(element(returnedarecords__1, [i___1]))) <= 
           rr_type__classtype__last))) .
H27:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_ipv4(element(returnedarecords__1, [i___1])) >= 
           unsigned_types__unsigned32__first) and (fld_ipv4(element(
           returnedarecords__1, [i___1])) <= 
           unsigned_types__unsigned32__last))) .
H28:   numfound__1 >= rr_type__numberofrecordstype__first .
H29:   numfound__1 <= rr_type__numberofrecordstype__last .
H30:   numfound__1 >= natural__first .
H31:   numfound__1 <= natural__last .
H32:   start_byte >= dns_types__packet_bytes_range__first .
H33:   start_byte <= dns_types__packet_bytes_range__last .
H34:   numfound__1 >= natural__first .
H35:   numfound__1 <= natural__last .
H36:   numfound__1 >= 1 .
H37:   1 >= natural__first .
H38:   1 <= natural__last .
H39:   start_byte >= dns_types__packet_bytes_range__first .
H40:   start_byte <= dns_types__packet_bytes_range__last .
H41:   numfound__1 >= natural__first .
H42:   numfound__1 <= natural__last .
H43:   1 >= natural__first .
H44:   1 <= natural__last .
H45:   dns_types__packet_size - (16 + dns_types__header_bits div 8) >= system__min_int .
H46:   dns_types__packet_size - (16 + dns_types__header_bits div 8) <= system__max_int .
H47:   16 + dns_types__header_bits div 8 >= system__min_int .
H48:   16 + dns_types__header_bits div 8 <= system__max_int .
H49:   dns_types__header_bits div 8 >= system__min_int .
H50:   dns_types__header_bits div 8 <= system__max_int .
H51:   8 <> 0 .
H52:   start_byte >= integer__first .
H53:   start_byte <= integer__last .
H54:   1 <= numfound__1 .
H55:   start_byte < dns_types__packet_size - (16 + 
           dns_types__header_bits div 8) .
        ->
C1:    1 >= 1 .
C2:    1 <= numfound__1 .
C3:    start_byte <= dns_types__packet_size .
C4:    answer_count = answer_count .
C5:    answer_count <= dns_types__unsigned_short__last - 
           rr_type__maxnumrecords .
C6:    start_byte = start_byte + 16 * (1 - 1) .
C7:    start_byte < dns_types__packet_size - (16 + 
           dns_types__header_bits div 8) .
C8:    numfound__1 <= rr_type__maxnumrecords .
C9:    start_byte >= dns_types__packet_bytes_range__first .
C10:   start_byte <= dns_types__packet_bytes_range__last .
C11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           domainname, [i___1]) >= character__first) and (element(
           domainname, [i___1]) <= character__last))) .
C12:   qname_location >= dns_types__qname_ptr_range__first .
C13:   qname_location <= dns_types__qname_ptr_range__last .
C14:   fld_messageid(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
C15:   fld_messageid(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
C16:   fld_opcode(fld_header(output_packet)) >= 
           dns_types__opcode_type__first .
C17:   fld_opcode(fld_header(output_packet)) <= 
           dns_types__opcode_type__last .
C18:   fld_rcode(fld_header(output_packet)) >= 
           dns_types__response_code__first .
C19:   fld_rcode(fld_header(output_packet)) <= 
           dns_types__response_code__last .
C20:   fld_qdcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
C21:   fld_qdcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
C22:   fld_ancount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
C23:   fld_ancount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
C24:   fld_nscount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
C25:   fld_nscount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
C26:   fld_arcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
C27:   fld_arcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
C28:   for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           fld_bytes(output_packet), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           output_packet), [i___1]) <= dns_types__byte__last))) .
C29:   answer_count >= dns_types__unsigned_short__first .
C30:   answer_count <= dns_types__unsigned_short__last .
C31:   answer_count <= dns_types__unsigned_short__last - 
           rr_type__maxnumrecords .
C32:   start_byte <= dns_types__packet_size .
 

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

procedure_create_response_a_7.
H1:    response_counter >= 1 .
H2:    response_counter <= numfound .
H3:    start_byte <= dns_types__packet_size .
H4:    answer_count = answer_count~ .
H5:    answer_count <= dns_types__unsigned_short__last - 
           rr_type__maxnumrecords .
H6:    current_byte = start_byte + 16 * (response_counter - 1) .
H7:    current_byte < dns_types__packet_size - (16 + 
           dns_types__header_bits div 8) .
H8:    numfound <= rr_type__maxnumrecords .
H9:    start_byte >= dns_types__packet_bytes_range__first .
H10:   start_byte <= dns_types__packet_bytes_range__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           domainname, [i___1]) >= character__first) and (element(
           domainname, [i___1]) <= character__last))) .
H12:   qname_location >= dns_types__qname_ptr_range__first .
H13:   qname_location <= dns_types__qname_ptr_range__last .
H14:   fld_messageid(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H15:   fld_messageid(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H16:   fld_opcode(fld_header(output_packet)) >= 
           dns_types__opcode_type__first .
H17:   fld_opcode(fld_header(output_packet)) <= 
           dns_types__opcode_type__last .
H18:   fld_rcode(fld_header(output_packet)) >= 
           dns_types__response_code__first .
H19:   fld_rcode(fld_header(output_packet)) <= 
           dns_types__response_code__last .
H20:   fld_qdcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H21:   fld_qdcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H22:   fld_ancount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H23:   fld_ancount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H24:   fld_nscount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H25:   fld_nscount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H26:   fld_arcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H27:   fld_arcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H28:   for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           fld_bytes(output_packet), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           output_packet), [i___1]) <= dns_types__byte__last))) .
H29:   answer_count >= dns_types__unsigned_short__first .
H30:   answer_count <= dns_types__unsigned_short__last .
H31:   answer_count~ <= dns_types__unsigned_short__last - 
           rr_type__maxnumrecords .
H32:   start_byte <= dns_types__packet_size .
H33:   current_byte >= dns_types__packet_bytes_range__first .
H34:   current_byte <= dns_types__packet_bytes_range__last .
H35:   (qname_location + 49152) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H36:   (qname_location + 49152) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H37:   current_byte + 1 >= dns_types__packet_bytes_range__first .
H38:   current_byte + 1 <= dns_types__packet_bytes_range__last .
H39:   current_byte + 1 <= dns_types__packet_bytes_range__last - 1 .
H40:   qname_location >= unsigned_types__unsigned16__first .
H41:   qname_location <= unsigned_types__unsigned16__last .
H42:   current_byte + 1 >= dns_types__packet_bytes_range__base__first .
H43:   current_byte + 1 <= dns_types__packet_bytes_range__base__last .
H44:   for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           fld_bytes(output_packet__2), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           output_packet__2), [i___1]) <= dns_types__byte__last))) .
H45:   fld_header(output_packet__2) = fld_header(
           output_packet) .
H46:   output_packet__2 = upf_bytes(output_packet, fld_bytes(
           output_packet__2)) .
H47:   0 >= dns_types__byte__first .
H48:   0 <= dns_types__byte__last .
H49:   current_byte + 3 >= dns_types__packet_bytes_range__first .
H50:   current_byte + 3 <= dns_types__packet_bytes_range__last .
H51:   current_byte + 3 >= dns_types__packet_bytes_range__base__first .
H52:   current_byte + 3 <= dns_types__packet_bytes_range__base__last .
H53:   1 >= dns_types__byte__first .
H54:   1 <= dns_types__byte__last .
H55:   current_byte + 4 >= dns_types__packet_bytes_range__first .
H56:   current_byte + 4 <= dns_types__packet_bytes_range__last .
H57:   current_byte + 4 >= dns_types__packet_bytes_range__base__first .
H58:   current_byte + 4 <= dns_types__packet_bytes_range__base__last .
H59:   0 >= dns_types__byte__first .
H60:   0 <= dns_types__byte__last .
H61:   current_byte + 5 >= dns_types__packet_bytes_range__first .
H62:   current_byte + 5 <= dns_types__packet_bytes_range__last .
H63:   current_byte + 5 >= dns_types__packet_bytes_range__base__first .
H64:   current_byte + 5 <= dns_types__packet_bytes_range__base__last .
H65:   1 >= dns_types__byte__first .
H66:   1 <= dns_types__byte__last .
H67:   current_byte + 6 >= dns_types__packet_bytes_range__first .
H68:   current_byte + 6 <= dns_types__packet_bytes_range__last .
H69:   current_byte + 6 >= dns_types__packet_bytes_range__base__first .
H70:   current_byte + 6 <= dns_types__packet_bytes_range__base__last .
H71:   current_byte >= dns_types__packet_bytes_range__first .
H72:   current_byte <= dns_types__packet_bytes_range__last .
H73:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_ttlinseconds(fld_inherit(element(
           returnedarecords, [i___1]))) >= 
           unsigned_types__unsigned32__first) and (fld_ttlinseconds(
           fld_inherit(element(returnedarecords, [i___1]))) <= 
           unsigned_types__unsigned32__last))) .
H74:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_class(fld_inherit(element(returnedarecords, [
           i___1]))) >= rr_type__classtype__first) and (fld_class(
           fld_inherit(element(returnedarecords, [i___1]))) <= 
           rr_type__classtype__last))) .
H75:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_ipv4(element(returnedarecords, [i___1])) >= 
           unsigned_types__unsigned32__first) and (fld_ipv4(element(
           returnedarecords, [i___1])) <= 
           unsigned_types__unsigned32__last))) .
H76:   response_counter >= natural__first .
H77:   response_counter <= natural__last .
H78:   current_byte + 7 >= dns_types__packet_bytes_range__first .
H79:   current_byte + 7 <= dns_types__packet_bytes_range__last .
H80:   current_byte + 7 <= dns_types__packet_bytes_range__last - 10 .
H81:   rr_type__returnedrecordsindextype__first + (
           response_counter - 1) >= 
           rr_type__returnedrecordsindextype__first .
H82:   rr_type__returnedrecordsindextype__first + (
           response_counter - 1) <= 
           rr_type__returnedrecordsindextype__last .
H83:   rr_type__returnedrecordsindextype__first + (
           response_counter - 1) >= integer__base__first .
H84:   rr_type__returnedrecordsindextype__first + (
           response_counter - 1) <= integer__base__last .
H85:   response_counter - 1 >= integer__base__first .
H86:   response_counter - 1 <= integer__base__last .
H87:   current_byte + 7 >= dns_types__packet_bytes_range__base__first .
H88:   current_byte + 7 <= dns_types__packet_bytes_range__base__last .
H89:   for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           fld_bytes(output_packet__3), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           output_packet__3), [i___1]) <= dns_types__byte__last))) .
H90:   fld_header(output_packet__3) = fld_header(upf_bytes(upf_bytes(
           upf_bytes(upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0)), update(fld_bytes(
           upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0))), [
           current_byte + 4], 1)), update(fld_bytes(upf_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0)), update(fld_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0))), [current_byte + 4], 1))), [
           current_byte + 5], 0)), update(fld_bytes(upf_bytes(upf_bytes(
           upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0)), update(fld_bytes(
           upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0))), [
           current_byte + 4], 1)), update(fld_bytes(upf_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0)), update(fld_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0))), [current_byte + 4], 1))), [
           current_byte + 5], 0))), [current_byte + 6], 1))) .
H91:   output_packet__3 = upf_bytes(upf_bytes(upf_bytes(upf_bytes(
           upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0)), update(fld_bytes(
           upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0))), [
           current_byte + 4], 1)), update(fld_bytes(upf_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0)), update(fld_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0))), [current_byte + 4], 1))), [
           current_byte + 5], 0)), update(fld_bytes(upf_bytes(upf_bytes(
           upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0)), update(fld_bytes(
           upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0))), [
           current_byte + 4], 1)), update(fld_bytes(upf_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0)), update(fld_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0))), [current_byte + 4], 1))), [
           current_byte + 5], 0))), [current_byte + 6], 1)), fld_bytes(
           output_packet__3)) .
H92:   response_counter >= natural__first .
H93:   response_counter <= natural__last .
H94:   response_counter + 1 >= natural__first .
H95:   response_counter + 1 <= natural__last .
H96:   current_byte >= dns_types__packet_bytes_range__first .
H97:   current_byte <= dns_types__packet_bytes_range__last .
H98:   current_byte + 16 >= dns_types__packet_bytes_range__first .
H99:   current_byte + 16 <= dns_types__packet_bytes_range__last .
H100:  current_byte + 16 >= dns_types__packet_bytes_range__first .
H101:  current_byte + 16 <= dns_types__packet_bytes_range__last .
H102:  numfound >= natural__first .
H103:  numfound <= natural__last .
H104:  response_counter + 1 >= natural__first .
H105:  response_counter + 1 <= natural__last .
H106:  dns_types__packet_size - (16 + dns_types__header_bits div 8) >= system__min_int .
H107:  dns_types__packet_size - (16 + dns_types__header_bits div 8) <= system__max_int .
H108:  16 + dns_types__header_bits div 8 >= system__min_int .
H109:  16 + dns_types__header_bits div 8 <= system__max_int .
H110:  dns_types__header_bits div 8 >= system__min_int .
H111:  dns_types__header_bits div 8 <= system__max_int .
H112:  8 <> 0 .
H113:  current_byte + 16 >= integer__first .
H114:  current_byte + 16 <= integer__last .
H115:  response_counter + 1 <= numfound .
H116:  current_byte + 16 < dns_types__packet_size - (16 + 
           dns_types__header_bits div 8) .
        ->
C1:    response_counter + 1 >= 1 .
C2:    response_counter + 1 <= numfound .
C3:    start_byte <= dns_types__packet_size .
C4:    answer_count = answer_count~ .
C5:    answer_count <= dns_types__unsigned_short__last - 
           rr_type__maxnumrecords .
C6:    current_byte + 16 = start_byte + 16 * (
           response_counter + 1 - 1) .
C7:    current_byte + 16 < dns_types__packet_size - (16 + 
           dns_types__header_bits div 8) .
C8:    numfound <= rr_type__maxnumrecords .
C9:    start_byte >= dns_types__packet_bytes_range__first .
C10:   start_byte <= dns_types__packet_bytes_range__last .
C11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           domainname, [i___1]) >= character__first) and (element(
           domainname, [i___1]) <= character__last))) .
C12:   qname_location >= dns_types__qname_ptr_range__first .
C13:   qname_location <= dns_types__qname_ptr_range__last .
C14:   fld_messageid(fld_header(output_packet__3)) >= 
           dns_types__unsigned_short__first .
C15:   fld_messageid(fld_header(output_packet__3)) <= 
           dns_types__unsigned_short__last .
C16:   fld_opcode(fld_header(output_packet__3)) >= 
           dns_types__opcode_type__first .
C17:   fld_opcode(fld_header(output_packet__3)) <= 
           dns_types__opcode_type__last .
C18:   fld_rcode(fld_header(output_packet__3)) >= 
           dns_types__response_code__first .
C19:   fld_rcode(fld_header(output_packet__3)) <= 
           dns_types__response_code__last .
C20:   fld_qdcount(fld_header(output_packet__3)) >= 
           dns_types__unsigned_short__first .
C21:   fld_qdcount(fld_header(output_packet__3)) <= 
           dns_types__unsigned_short__last .
C22:   fld_ancount(fld_header(output_packet__3)) >= 
           dns_types__unsigned_short__first .
C23:   fld_ancount(fld_header(output_packet__3)) <= 
           dns_types__unsigned_short__last .
C24:   fld_nscount(fld_header(output_packet__3)) >= 
           dns_types__unsigned_short__first .
C25:   fld_nscount(fld_header(output_packet__3)) <= 
           dns_types__unsigned_short__last .
C26:   fld_arcount(fld_header(output_packet__3)) >= 
           dns_types__unsigned_short__first .
C27:   fld_arcount(fld_header(output_packet__3)) <= 
           dns_types__unsigned_short__last .
C28:   for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           fld_bytes(output_packet__3), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           output_packet__3), [i___1]) <= dns_types__byte__last))) .
C29:   answer_count >= dns_types__unsigned_short__first .
C30:   answer_count <= dns_types__unsigned_short__last .
C31:   answer_count~ <= dns_types__unsigned_short__last - 
           rr_type__maxnumrecords .
C32:   start_byte <= dns_types__packet_size .
 

For path(s) from assertion of line 546 to precondition check associated with statement of line 555:

procedure_create_response_a_8.
H1:    response_counter >= 1 .
H2:    response_counter <= numfound .
H3:    start_byte <= dns_types__packet_size .
H4:    answer_count = answer_count~ .
H5:    answer_count <= dns_types__unsigned_short__last - 
           rr_type__maxnumrecords .
H6:    current_byte = start_byte + 16 * (response_counter - 1) .
H7:    current_byte < dns_types__packet_size - (16 + 
           dns_types__header_bits div 8) .
H8:    numfound <= rr_type__maxnumrecords .
H9:    start_byte >= dns_types__packet_bytes_range__first .
H10:   start_byte <= dns_types__packet_bytes_range__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           domainname, [i___1]) >= character__first) and (element(
           domainname, [i___1]) <= character__last))) .
H12:   qname_location >= dns_types__qname_ptr_range__first .
H13:   qname_location <= dns_types__qname_ptr_range__last .
H14:   fld_messageid(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H15:   fld_messageid(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H16:   fld_opcode(fld_header(output_packet)) >= 
           dns_types__opcode_type__first .
H17:   fld_opcode(fld_header(output_packet)) <= 
           dns_types__opcode_type__last .
H18:   fld_rcode(fld_header(output_packet)) >= 
           dns_types__response_code__first .
H19:   fld_rcode(fld_header(output_packet)) <= 
           dns_types__response_code__last .
H20:   fld_qdcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H21:   fld_qdcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H22:   fld_ancount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H23:   fld_ancount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H24:   fld_nscount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H25:   fld_nscount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H26:   fld_arcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H27:   fld_arcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H28:   for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           fld_bytes(output_packet), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           output_packet), [i___1]) <= dns_types__byte__last))) .
H29:   answer_count >= dns_types__unsigned_short__first .
H30:   answer_count <= dns_types__unsigned_short__last .
H31:   answer_count~ <= dns_types__unsigned_short__last - 
           rr_type__maxnumrecords .
H32:   start_byte <= dns_types__packet_size .
H33:   current_byte >= dns_types__packet_bytes_range__first .
H34:   current_byte <= dns_types__packet_bytes_range__last .
        ->
C1:    (qname_location + 49152) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
C2:    (qname_location + 49152) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
C3:    current_byte + 1 >= dns_types__packet_bytes_range__first .
C4:    current_byte + 1 <= dns_types__packet_bytes_range__last .
C5:    current_byte + 1 <= dns_types__packet_bytes_range__last - 1 .
C6:    qname_location >= unsigned_types__unsigned16__first .
C7:    qname_location <= unsigned_types__unsigned16__last .
C8:    current_byte + 1 >= dns_types__packet_bytes_range__base__first .
C9:    current_byte + 1 <= dns_types__packet_bytes_range__base__last .
 

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

procedure_create_response_a_9.
H1:    response_counter >= 1 .
H2:    response_counter <= numfound .
H3:    start_byte <= dns_types__packet_size .
H4:    answer_count = answer_count~ .
H5:    answer_count <= dns_types__unsigned_short__last - 
           rr_type__maxnumrecords .
H6:    current_byte = start_byte + 16 * (response_counter - 1) .
H7:    current_byte < dns_types__packet_size - (16 + 
           dns_types__header_bits div 8) .
H8:    numfound <= rr_type__maxnumrecords .
H9:    start_byte >= dns_types__packet_bytes_range__first .
H10:   start_byte <= dns_types__packet_bytes_range__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           domainname, [i___1]) >= character__first) and (element(
           domainname, [i___1]) <= character__last))) .
H12:   qname_location >= dns_types__qname_ptr_range__first .
H13:   qname_location <= dns_types__qname_ptr_range__last .
H14:   fld_messageid(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H15:   fld_messageid(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H16:   fld_opcode(fld_header(output_packet)) >= 
           dns_types__opcode_type__first .
H17:   fld_opcode(fld_header(output_packet)) <= 
           dns_types__opcode_type__last .
H18:   fld_rcode(fld_header(output_packet)) >= 
           dns_types__response_code__first .
H19:   fld_rcode(fld_header(output_packet)) <= 
           dns_types__response_code__last .
H20:   fld_qdcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H21:   fld_qdcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H22:   fld_ancount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H23:   fld_ancount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H24:   fld_nscount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H25:   fld_nscount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H26:   fld_arcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H27:   fld_arcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H28:   for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           fld_bytes(output_packet), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           output_packet), [i___1]) <= dns_types__byte__last))) .
H29:   answer_count >= dns_types__unsigned_short__first .
H30:   answer_count <= dns_types__unsigned_short__last .
H31:   answer_count~ <= dns_types__unsigned_short__last - 
           rr_type__maxnumrecords .
H32:   start_byte <= dns_types__packet_size .
H33:   current_byte >= dns_types__packet_bytes_range__first .
H34:   current_byte <= dns_types__packet_bytes_range__last .
H35:   (qname_location + 49152) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H36:   (qname_location + 49152) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H37:   current_byte + 1 >= dns_types__packet_bytes_range__first .
H38:   current_byte + 1 <= dns_types__packet_bytes_range__last .
H39:   current_byte + 1 <= dns_types__packet_bytes_range__last - 1 .
H40:   qname_location >= unsigned_types__unsigned16__first .
H41:   qname_location <= unsigned_types__unsigned16__last .
H42:   current_byte + 1 >= dns_types__packet_bytes_range__base__first .
H43:   current_byte + 1 <= dns_types__packet_bytes_range__base__last .
H44:   for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           fld_bytes(output_packet__2), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           output_packet__2), [i___1]) <= dns_types__byte__last))) .
H45:   fld_header(output_packet__2) = fld_header(
           output_packet) .
H46:   output_packet__2 = upf_bytes(output_packet, fld_bytes(
           output_packet__2)) .
        ->
C1:    0 >= dns_types__byte__first .
C2:    0 <= dns_types__byte__last .
C3:    current_byte + 3 >= dns_types__packet_bytes_range__first .
C4:    current_byte + 3 <= dns_types__packet_bytes_range__last .
C5:    current_byte + 3 >= dns_types__packet_bytes_range__base__first .
C6:    current_byte + 3 <= dns_types__packet_bytes_range__base__last .
 

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

procedure_create_response_a_10.
H1:    response_counter >= 1 .
H2:    response_counter <= numfound .
H3:    start_byte <= dns_types__packet_size .
H4:    answer_count = answer_count~ .
H5:    answer_count <= dns_types__unsigned_short__last - 
           rr_type__maxnumrecords .
H6:    current_byte = start_byte + 16 * (response_counter - 1) .
H7:    current_byte < dns_types__packet_size - (16 + 
           dns_types__header_bits div 8) .
H8:    numfound <= rr_type__maxnumrecords .
H9:    start_byte >= dns_types__packet_bytes_range__first .
H10:   start_byte <= dns_types__packet_bytes_range__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           domainname, [i___1]) >= character__first) and (element(
           domainname, [i___1]) <= character__last))) .
H12:   qname_location >= dns_types__qname_ptr_range__first .
H13:   qname_location <= dns_types__qname_ptr_range__last .
H14:   fld_messageid(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H15:   fld_messageid(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H16:   fld_opcode(fld_header(output_packet)) >= 
           dns_types__opcode_type__first .
H17:   fld_opcode(fld_header(output_packet)) <= 
           dns_types__opcode_type__last .
H18:   fld_rcode(fld_header(output_packet)) >= 
           dns_types__response_code__first .
H19:   fld_rcode(fld_header(output_packet)) <= 
           dns_types__response_code__last .
H20:   fld_qdcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H21:   fld_qdcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H22:   fld_ancount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H23:   fld_ancount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H24:   fld_nscount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H25:   fld_nscount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H26:   fld_arcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H27:   fld_arcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H28:   for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           fld_bytes(output_packet), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           output_packet), [i___1]) <= dns_types__byte__last))) .
H29:   answer_count >= dns_types__unsigned_short__first .
H30:   answer_count <= dns_types__unsigned_short__last .
H31:   answer_count~ <= dns_types__unsigned_short__last - 
           rr_type__maxnumrecords .
H32:   start_byte <= dns_types__packet_size .
H33:   current_byte >= dns_types__packet_bytes_range__first .
H34:   current_byte <= dns_types__packet_bytes_range__last .
H35:   (qname_location + 49152) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H36:   (qname_location + 49152) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H37:   current_byte + 1 >= dns_types__packet_bytes_range__first .
H38:   current_byte + 1 <= dns_types__packet_bytes_range__last .
H39:   current_byte + 1 <= dns_types__packet_bytes_range__last - 1 .
H40:   qname_location >= unsigned_types__unsigned16__first .
H41:   qname_location <= unsigned_types__unsigned16__last .
H42:   current_byte + 1 >= dns_types__packet_bytes_range__base__first .
H43:   current_byte + 1 <= dns_types__packet_bytes_range__base__last .
H44:   for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           fld_bytes(output_packet__2), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           output_packet__2), [i___1]) <= dns_types__byte__last))) .
H45:   fld_header(output_packet__2) = fld_header(
           output_packet) .
H46:   output_packet__2 = upf_bytes(output_packet, fld_bytes(
           output_packet__2)) .
H47:   0 >= dns_types__byte__first .
H48:   0 <= dns_types__byte__last .
H49:   current_byte + 3 >= dns_types__packet_bytes_range__first .
H50:   current_byte + 3 <= dns_types__packet_bytes_range__last .
H51:   current_byte + 3 >= dns_types__packet_bytes_range__base__first .
H52:   current_byte + 3 <= dns_types__packet_bytes_range__base__last .
        ->
C1:    1 >= dns_types__byte__first .
C2:    1 <= dns_types__byte__last .
C3:    current_byte + 4 >= dns_types__packet_bytes_range__first .
C4:    current_byte + 4 <= dns_types__packet_bytes_range__last .
C5:    current_byte + 4 >= dns_types__packet_bytes_range__base__first .
C6:    current_byte + 4 <= dns_types__packet_bytes_range__base__last .
 

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

procedure_create_response_a_11.
H1:    response_counter >= 1 .
H2:    response_counter <= numfound .
H3:    start_byte <= dns_types__packet_size .
H4:    answer_count = answer_count~ .
H5:    answer_count <= dns_types__unsigned_short__last - 
           rr_type__maxnumrecords .
H6:    current_byte = start_byte + 16 * (response_counter - 1) .
H7:    current_byte < dns_types__packet_size - (16 + 
           dns_types__header_bits div 8) .
H8:    numfound <= rr_type__maxnumrecords .
H9:    start_byte >= dns_types__packet_bytes_range__first .
H10:   start_byte <= dns_types__packet_bytes_range__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           domainname, [i___1]) >= character__first) and (element(
           domainname, [i___1]) <= character__last))) .
H12:   qname_location >= dns_types__qname_ptr_range__first .
H13:   qname_location <= dns_types__qname_ptr_range__last .
H14:   fld_messageid(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H15:   fld_messageid(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H16:   fld_opcode(fld_header(output_packet)) >= 
           dns_types__opcode_type__first .
H17:   fld_opcode(fld_header(output_packet)) <= 
           dns_types__opcode_type__last .
H18:   fld_rcode(fld_header(output_packet)) >= 
           dns_types__response_code__first .
H19:   fld_rcode(fld_header(output_packet)) <= 
           dns_types__response_code__last .
H20:   fld_qdcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H21:   fld_qdcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H22:   fld_ancount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H23:   fld_ancount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H24:   fld_nscount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H25:   fld_nscount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H26:   fld_arcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H27:   fld_arcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H28:   for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           fld_bytes(output_packet), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           output_packet), [i___1]) <= dns_types__byte__last))) .
H29:   answer_count >= dns_types__unsigned_short__first .
H30:   answer_count <= dns_types__unsigned_short__last .
H31:   answer_count~ <= dns_types__unsigned_short__last - 
           rr_type__maxnumrecords .
H32:   start_byte <= dns_types__packet_size .
H33:   current_byte >= dns_types__packet_bytes_range__first .
H34:   current_byte <= dns_types__packet_bytes_range__last .
H35:   (qname_location + 49152) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H36:   (qname_location + 49152) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H37:   current_byte + 1 >= dns_types__packet_bytes_range__first .
H38:   current_byte + 1 <= dns_types__packet_bytes_range__last .
H39:   current_byte + 1 <= dns_types__packet_bytes_range__last - 1 .
H40:   qname_location >= unsigned_types__unsigned16__first .
H41:   qname_location <= unsigned_types__unsigned16__last .
H42:   current_byte + 1 >= dns_types__packet_bytes_range__base__first .
H43:   current_byte + 1 <= dns_types__packet_bytes_range__base__last .
H44:   for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           fld_bytes(output_packet__2), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           output_packet__2), [i___1]) <= dns_types__byte__last))) .
H45:   fld_header(output_packet__2) = fld_header(
           output_packet) .
H46:   output_packet__2 = upf_bytes(output_packet, fld_bytes(
           output_packet__2)) .
H47:   0 >= dns_types__byte__first .
H48:   0 <= dns_types__byte__last .
H49:   current_byte + 3 >= dns_types__packet_bytes_range__first .
H50:   current_byte + 3 <= dns_types__packet_bytes_range__last .
H51:   current_byte + 3 >= dns_types__packet_bytes_range__base__first .
H52:   current_byte + 3 <= dns_types__packet_bytes_range__base__last .
H53:   1 >= dns_types__byte__first .
H54:   1 <= dns_types__byte__last .
H55:   current_byte + 4 >= dns_types__packet_bytes_range__first .
H56:   current_byte + 4 <= dns_types__packet_bytes_range__last .
H57:   current_byte + 4 >= dns_types__packet_bytes_range__base__first .
H58:   current_byte + 4 <= dns_types__packet_bytes_range__base__last .
        ->
C1:    0 >= dns_types__byte__first .
C2:    0 <= dns_types__byte__last .
C3:    current_byte + 5 >= dns_types__packet_bytes_range__first .
C4:    current_byte + 5 <= dns_types__packet_bytes_range__last .
C5:    current_byte + 5 >= dns_types__packet_bytes_range__base__first .
C6:    current_byte + 5 <= dns_types__packet_bytes_range__base__last .
 

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

procedure_create_response_a_12.
H1:    response_counter >= 1 .
H2:    response_counter <= numfound .
H3:    start_byte <= dns_types__packet_size .
H4:    answer_count = answer_count~ .
H5:    answer_count <= dns_types__unsigned_short__last - 
           rr_type__maxnumrecords .
H6:    current_byte = start_byte + 16 * (response_counter - 1) .
H7:    current_byte < dns_types__packet_size - (16 + 
           dns_types__header_bits div 8) .
H8:    numfound <= rr_type__maxnumrecords .
H9:    start_byte >= dns_types__packet_bytes_range__first .
H10:   start_byte <= dns_types__packet_bytes_range__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           domainname, [i___1]) >= character__first) and (element(
           domainname, [i___1]) <= character__last))) .
H12:   qname_location >= dns_types__qname_ptr_range__first .
H13:   qname_location <= dns_types__qname_ptr_range__last .
H14:   fld_messageid(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H15:   fld_messageid(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H16:   fld_opcode(fld_header(output_packet)) >= 
           dns_types__opcode_type__first .
H17:   fld_opcode(fld_header(output_packet)) <= 
           dns_types__opcode_type__last .
H18:   fld_rcode(fld_header(output_packet)) >= 
           dns_types__response_code__first .
H19:   fld_rcode(fld_header(output_packet)) <= 
           dns_types__response_code__last .
H20:   fld_qdcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H21:   fld_qdcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H22:   fld_ancount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H23:   fld_ancount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H24:   fld_nscount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H25:   fld_nscount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H26:   fld_arcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H27:   fld_arcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H28:   for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           fld_bytes(output_packet), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           output_packet), [i___1]) <= dns_types__byte__last))) .
H29:   answer_count >= dns_types__unsigned_short__first .
H30:   answer_count <= dns_types__unsigned_short__last .
H31:   answer_count~ <= dns_types__unsigned_short__last - 
           rr_type__maxnumrecords .
H32:   start_byte <= dns_types__packet_size .
H33:   current_byte >= dns_types__packet_bytes_range__first .
H34:   current_byte <= dns_types__packet_bytes_range__last .
H35:   (qname_location + 49152) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H36:   (qname_location + 49152) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H37:   current_byte + 1 >= dns_types__packet_bytes_range__first .
H38:   current_byte + 1 <= dns_types__packet_bytes_range__last .
H39:   current_byte + 1 <= dns_types__packet_bytes_range__last - 1 .
H40:   qname_location >= unsigned_types__unsigned16__first .
H41:   qname_location <= unsigned_types__unsigned16__last .
H42:   current_byte + 1 >= dns_types__packet_bytes_range__base__first .
H43:   current_byte + 1 <= dns_types__packet_bytes_range__base__last .
H44:   for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           fld_bytes(output_packet__2), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           output_packet__2), [i___1]) <= dns_types__byte__last))) .
H45:   fld_header(output_packet__2) = fld_header(
           output_packet) .
H46:   output_packet__2 = upf_bytes(output_packet, fld_bytes(
           output_packet__2)) .
H47:   0 >= dns_types__byte__first .
H48:   0 <= dns_types__byte__last .
H49:   current_byte + 3 >= dns_types__packet_bytes_range__first .
H50:   current_byte + 3 <= dns_types__packet_bytes_range__last .
H51:   current_byte + 3 >= dns_types__packet_bytes_range__base__first .
H52:   current_byte + 3 <= dns_types__packet_bytes_range__base__last .
H53:   1 >= dns_types__byte__first .
H54:   1 <= dns_types__byte__last .
H55:   current_byte + 4 >= dns_types__packet_bytes_range__first .
H56:   current_byte + 4 <= dns_types__packet_bytes_range__last .
H57:   current_byte + 4 >= dns_types__packet_bytes_range__base__first .
H58:   current_byte + 4 <= dns_types__packet_bytes_range__base__last .
H59:   0 >= dns_types__byte__first .
H60:   0 <= dns_types__byte__last .
H61:   current_byte + 5 >= dns_types__packet_bytes_range__first .
H62:   current_byte + 5 <= dns_types__packet_bytes_range__last .
H63:   current_byte + 5 >= dns_types__packet_bytes_range__base__first .
H64:   current_byte + 5 <= dns_types__packet_bytes_range__base__last .
        ->
C1:    1 >= dns_types__byte__first .
C2:    1 <= dns_types__byte__last .
C3:    current_byte + 6 >= dns_types__packet_bytes_range__first .
C4:    current_byte + 6 <= dns_types__packet_bytes_range__last .
C5:    current_byte + 6 >= dns_types__packet_bytes_range__base__first .
C6:    current_byte + 6 <= dns_types__packet_bytes_range__base__last .
 

For path(s) from assertion of line 546 to precondition check associated with statement of line 562:

procedure_create_response_a_13.
H1:    response_counter >= 1 .
H2:    response_counter <= numfound .
H3:    start_byte <= dns_types__packet_size .
H4:    answer_count = answer_count~ .
H5:    answer_count <= dns_types__unsigned_short__last - 
           rr_type__maxnumrecords .
H6:    current_byte = start_byte + 16 * (response_counter - 1) .
H7:    current_byte < dns_types__packet_size - (16 + 
           dns_types__header_bits div 8) .
H8:    numfound <= rr_type__maxnumrecords .
H9:    start_byte >= dns_types__packet_bytes_range__first .
H10:   start_byte <= dns_types__packet_bytes_range__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           domainname, [i___1]) >= character__first) and (element(
           domainname, [i___1]) <= character__last))) .
H12:   qname_location >= dns_types__qname_ptr_range__first .
H13:   qname_location <= dns_types__qname_ptr_range__last .
H14:   fld_messageid(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H15:   fld_messageid(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H16:   fld_opcode(fld_header(output_packet)) >= 
           dns_types__opcode_type__first .
H17:   fld_opcode(fld_header(output_packet)) <= 
           dns_types__opcode_type__last .
H18:   fld_rcode(fld_header(output_packet)) >= 
           dns_types__response_code__first .
H19:   fld_rcode(fld_header(output_packet)) <= 
           dns_types__response_code__last .
H20:   fld_qdcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H21:   fld_qdcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H22:   fld_ancount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H23:   fld_ancount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H24:   fld_nscount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H25:   fld_nscount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H26:   fld_arcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H27:   fld_arcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H28:   for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           fld_bytes(output_packet), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           output_packet), [i___1]) <= dns_types__byte__last))) .
H29:   answer_count >= dns_types__unsigned_short__first .
H30:   answer_count <= dns_types__unsigned_short__last .
H31:   answer_count~ <= dns_types__unsigned_short__last - 
           rr_type__maxnumrecords .
H32:   start_byte <= dns_types__packet_size .
H33:   current_byte >= dns_types__packet_bytes_range__first .
H34:   current_byte <= dns_types__packet_bytes_range__last .
H35:   (qname_location + 49152) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H36:   (qname_location + 49152) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H37:   current_byte + 1 >= dns_types__packet_bytes_range__first .
H38:   current_byte + 1 <= dns_types__packet_bytes_range__last .
H39:   current_byte + 1 <= dns_types__packet_bytes_range__last - 1 .
H40:   qname_location >= unsigned_types__unsigned16__first .
H41:   qname_location <= unsigned_types__unsigned16__last .
H42:   current_byte + 1 >= dns_types__packet_bytes_range__base__first .
H43:   current_byte + 1 <= dns_types__packet_bytes_range__base__last .
H44:   for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           fld_bytes(output_packet__2), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           output_packet__2), [i___1]) <= dns_types__byte__last))) .
H45:   fld_header(output_packet__2) = fld_header(
           output_packet) .
H46:   output_packet__2 = upf_bytes(output_packet, fld_bytes(
           output_packet__2)) .
H47:   0 >= dns_types__byte__first .
H48:   0 <= dns_types__byte__last .
H49:   current_byte + 3 >= dns_types__packet_bytes_range__first .
H50:   current_byte + 3 <= dns_types__packet_bytes_range__last .
H51:   current_byte + 3 >= dns_types__packet_bytes_range__base__first .
H52:   current_byte + 3 <= dns_types__packet_bytes_range__base__last .
H53:   1 >= dns_types__byte__first .
H54:   1 <= dns_types__byte__last .
H55:   current_byte + 4 >= dns_types__packet_bytes_range__first .
H56:   current_byte + 4 <= dns_types__packet_bytes_range__last .
H57:   current_byte + 4 >= dns_types__packet_bytes_range__base__first .
H58:   current_byte + 4 <= dns_types__packet_bytes_range__base__last .
H59:   0 >= dns_types__byte__first .
H60:   0 <= dns_types__byte__last .
H61:   current_byte + 5 >= dns_types__packet_bytes_range__first .
H62:   current_byte + 5 <= dns_types__packet_bytes_range__last .
H63:   current_byte + 5 >= dns_types__packet_bytes_range__base__first .
H64:   current_byte + 5 <= dns_types__packet_bytes_range__base__last .
H65:   1 >= dns_types__byte__first .
H66:   1 <= dns_types__byte__last .
H67:   current_byte + 6 >= dns_types__packet_bytes_range__first .
H68:   current_byte + 6 <= dns_types__packet_bytes_range__last .
H69:   current_byte + 6 >= dns_types__packet_bytes_range__base__first .
H70:   current_byte + 6 <= dns_types__packet_bytes_range__base__last .
H71:   current_byte >= dns_types__packet_bytes_range__first .
H72:   current_byte <= dns_types__packet_bytes_range__last .
H73:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_ttlinseconds(fld_inherit(element(
           returnedarecords, [i___1]))) >= 
           unsigned_types__unsigned32__first) and (fld_ttlinseconds(
           fld_inherit(element(returnedarecords, [i___1]))) <= 
           unsigned_types__unsigned32__last))) .
H74:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_class(fld_inherit(element(returnedarecords, [
           i___1]))) >= rr_type__classtype__first) and (fld_class(
           fld_inherit(element(returnedarecords, [i___1]))) <= 
           rr_type__classtype__last))) .
H75:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_ipv4(element(returnedarecords, [i___1])) >= 
           unsigned_types__unsigned32__first) and (fld_ipv4(element(
           returnedarecords, [i___1])) <= 
           unsigned_types__unsigned32__last))) .
H76:   response_counter >= natural__first .
H77:   response_counter <= natural__last .
        ->
C1:    current_byte + 7 >= dns_types__packet_bytes_range__first .
C2:    current_byte + 7 <= dns_types__packet_bytes_range__last .
C3:    current_byte + 7 <= dns_types__packet_bytes_range__last - 10 .
C4:    rr_type__returnedrecordsindextype__first + (
           response_counter - 1) >= 
           rr_type__returnedrecordsindextype__first .
C5:    rr_type__returnedrecordsindextype__first + (
           response_counter - 1) <= 
           rr_type__returnedrecordsindextype__last .
C6:    rr_type__returnedrecordsindextype__first + (
           response_counter - 1) >= integer__base__first .
C7:    rr_type__returnedrecordsindextype__first + (
           response_counter - 1) <= integer__base__last .
C8:    response_counter - 1 >= integer__base__first .
C9:    response_counter - 1 <= integer__base__last .
C10:   current_byte + 7 >= dns_types__packet_bytes_range__base__first .
C11:   current_byte + 7 <= dns_types__packet_bytes_range__base__last .
 

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

procedure_create_response_a_14.
H1:    response_counter >= 1 .
H2:    response_counter <= numfound .
H3:    start_byte <= dns_types__packet_size .
H4:    answer_count = answer_count~ .
H5:    answer_count <= dns_types__unsigned_short__last - 
           rr_type__maxnumrecords .
H6:    current_byte = start_byte + 16 * (response_counter - 1) .
H7:    current_byte < dns_types__packet_size - (16 + 
           dns_types__header_bits div 8) .
H8:    numfound <= rr_type__maxnumrecords .
H9:    start_byte >= dns_types__packet_bytes_range__first .
H10:   start_byte <= dns_types__packet_bytes_range__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           domainname, [i___1]) >= character__first) and (element(
           domainname, [i___1]) <= character__last))) .
H12:   qname_location >= dns_types__qname_ptr_range__first .
H13:   qname_location <= dns_types__qname_ptr_range__last .
H14:   fld_messageid(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H15:   fld_messageid(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H16:   fld_opcode(fld_header(output_packet)) >= 
           dns_types__opcode_type__first .
H17:   fld_opcode(fld_header(output_packet)) <= 
           dns_types__opcode_type__last .
H18:   fld_rcode(fld_header(output_packet)) >= 
           dns_types__response_code__first .
H19:   fld_rcode(fld_header(output_packet)) <= 
           dns_types__response_code__last .
H20:   fld_qdcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H21:   fld_qdcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H22:   fld_ancount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H23:   fld_ancount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H24:   fld_nscount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H25:   fld_nscount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H26:   fld_arcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H27:   fld_arcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H28:   for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           fld_bytes(output_packet), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           output_packet), [i___1]) <= dns_types__byte__last))) .
H29:   answer_count >= dns_types__unsigned_short__first .
H30:   answer_count <= dns_types__unsigned_short__last .
H31:   answer_count~ <= dns_types__unsigned_short__last - 
           rr_type__maxnumrecords .
H32:   start_byte <= dns_types__packet_size .
H33:   current_byte >= dns_types__packet_bytes_range__first .
H34:   current_byte <= dns_types__packet_bytes_range__last .
H35:   (qname_location + 49152) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H36:   (qname_location + 49152) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H37:   current_byte + 1 >= dns_types__packet_bytes_range__first .
H38:   current_byte + 1 <= dns_types__packet_bytes_range__last .
H39:   current_byte + 1 <= dns_types__packet_bytes_range__last - 1 .
H40:   qname_location >= unsigned_types__unsigned16__first .
H41:   qname_location <= unsigned_types__unsigned16__last .
H42:   current_byte + 1 >= dns_types__packet_bytes_range__base__first .
H43:   current_byte + 1 <= dns_types__packet_bytes_range__base__last .
H44:   for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           fld_bytes(output_packet__2), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           output_packet__2), [i___1]) <= dns_types__byte__last))) .
H45:   fld_header(output_packet__2) = fld_header(
           output_packet) .
H46:   output_packet__2 = upf_bytes(output_packet, fld_bytes(
           output_packet__2)) .
H47:   0 >= dns_types__byte__first .
H48:   0 <= dns_types__byte__last .
H49:   current_byte + 3 >= dns_types__packet_bytes_range__first .
H50:   current_byte + 3 <= dns_types__packet_bytes_range__last .
H51:   current_byte + 3 >= dns_types__packet_bytes_range__base__first .
H52:   current_byte + 3 <= dns_types__packet_bytes_range__base__last .
H53:   1 >= dns_types__byte__first .
H54:   1 <= dns_types__byte__last .
H55:   current_byte + 4 >= dns_types__packet_bytes_range__first .
H56:   current_byte + 4 <= dns_types__packet_bytes_range__last .
H57:   current_byte + 4 >= dns_types__packet_bytes_range__base__first .
H58:   current_byte + 4 <= dns_types__packet_bytes_range__base__last .
H59:   0 >= dns_types__byte__first .
H60:   0 <= dns_types__byte__last .
H61:   current_byte + 5 >= dns_types__packet_bytes_range__first .
H62:   current_byte + 5 <= dns_types__packet_bytes_range__last .
H63:   current_byte + 5 >= dns_types__packet_bytes_range__base__first .
H64:   current_byte + 5 <= dns_types__packet_bytes_range__base__last .
H65:   1 >= dns_types__byte__first .
H66:   1 <= dns_types__byte__last .
H67:   current_byte + 6 >= dns_types__packet_bytes_range__first .
H68:   current_byte + 6 <= dns_types__packet_bytes_range__last .
H69:   current_byte + 6 >= dns_types__packet_bytes_range__base__first .
H70:   current_byte + 6 <= dns_types__packet_bytes_range__base__last .
H71:   current_byte >= dns_types__packet_bytes_range__first .
H72:   current_byte <= dns_types__packet_bytes_range__last .
H73:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_ttlinseconds(fld_inherit(element(
           returnedarecords, [i___1]))) >= 
           unsigned_types__unsigned32__first) and (fld_ttlinseconds(
           fld_inherit(element(returnedarecords, [i___1]))) <= 
           unsigned_types__unsigned32__last))) .
H74:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_class(fld_inherit(element(returnedarecords, [
           i___1]))) >= rr_type__classtype__first) and (fld_class(
           fld_inherit(element(returnedarecords, [i___1]))) <= 
           rr_type__classtype__last))) .
H75:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_ipv4(element(returnedarecords, [i___1])) >= 
           unsigned_types__unsigned32__first) and (fld_ipv4(element(
           returnedarecords, [i___1])) <= 
           unsigned_types__unsigned32__last))) .
H76:   response_counter >= natural__first .
H77:   response_counter <= natural__last .
H78:   current_byte + 7 >= dns_types__packet_bytes_range__first .
H79:   current_byte + 7 <= dns_types__packet_bytes_range__last .
H80:   current_byte + 7 <= dns_types__packet_bytes_range__last - 10 .
H81:   rr_type__returnedrecordsindextype__first + (
           response_counter - 1) >= 
           rr_type__returnedrecordsindextype__first .
H82:   rr_type__returnedrecordsindextype__first + (
           response_counter - 1) <= 
           rr_type__returnedrecordsindextype__last .
H83:   rr_type__returnedrecordsindextype__first + (
           response_counter - 1) >= integer__base__first .
H84:   rr_type__returnedrecordsindextype__first + (
           response_counter - 1) <= integer__base__last .
H85:   response_counter - 1 >= integer__base__first .
H86:   response_counter - 1 <= integer__base__last .
H87:   current_byte + 7 >= dns_types__packet_bytes_range__base__first .
H88:   current_byte + 7 <= dns_types__packet_bytes_range__base__last .
H89:   for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           fld_bytes(output_packet__3), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           output_packet__3), [i___1]) <= dns_types__byte__last))) .
H90:   fld_header(output_packet__3) = fld_header(upf_bytes(upf_bytes(
           upf_bytes(upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0)), update(fld_bytes(
           upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0))), [
           current_byte + 4], 1)), update(fld_bytes(upf_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0)), update(fld_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0))), [current_byte + 4], 1))), [
           current_byte + 5], 0)), update(fld_bytes(upf_bytes(upf_bytes(
           upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0)), update(fld_bytes(
           upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0))), [
           current_byte + 4], 1)), update(fld_bytes(upf_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0)), update(fld_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0))), [current_byte + 4], 1))), [
           current_byte + 5], 0))), [current_byte + 6], 1))) .
H91:   output_packet__3 = upf_bytes(upf_bytes(upf_bytes(upf_bytes(
           upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0)), update(fld_bytes(
           upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0))), [
           current_byte + 4], 1)), update(fld_bytes(upf_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0)), update(fld_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0))), [current_byte + 4], 1))), [
           current_byte + 5], 0)), update(fld_bytes(upf_bytes(upf_bytes(
           upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0)), update(fld_bytes(
           upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0))), [
           current_byte + 4], 1)), update(fld_bytes(upf_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0)), update(fld_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0))), [current_byte + 4], 1))), [
           current_byte + 5], 0))), [current_byte + 6], 1)), fld_bytes(
           output_packet__3)) .
H92:   response_counter >= natural__first .
H93:   response_counter <= natural__last .
        ->
C1:    response_counter + 1 >= natural__first .
C2:    response_counter + 1 <= natural__last .
 

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

procedure_create_response_a_15.
H1:    response_counter >= 1 .
H2:    response_counter <= numfound .
H3:    start_byte <= dns_types__packet_size .
H4:    answer_count = answer_count~ .
H5:    answer_count <= dns_types__unsigned_short__last - 
           rr_type__maxnumrecords .
H6:    current_byte = start_byte + 16 * (response_counter - 1) .
H7:    current_byte < dns_types__packet_size - (16 + 
           dns_types__header_bits div 8) .
H8:    numfound <= rr_type__maxnumrecords .
H9:    start_byte >= dns_types__packet_bytes_range__first .
H10:   start_byte <= dns_types__packet_bytes_range__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           domainname, [i___1]) >= character__first) and (element(
           domainname, [i___1]) <= character__last))) .
H12:   qname_location >= dns_types__qname_ptr_range__first .
H13:   qname_location <= dns_types__qname_ptr_range__last .
H14:   fld_messageid(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H15:   fld_messageid(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H16:   fld_opcode(fld_header(output_packet)) >= 
           dns_types__opcode_type__first .
H17:   fld_opcode(fld_header(output_packet)) <= 
           dns_types__opcode_type__last .
H18:   fld_rcode(fld_header(output_packet)) >= 
           dns_types__response_code__first .
H19:   fld_rcode(fld_header(output_packet)) <= 
           dns_types__response_code__last .
H20:   fld_qdcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H21:   fld_qdcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H22:   fld_ancount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H23:   fld_ancount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H24:   fld_nscount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H25:   fld_nscount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H26:   fld_arcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H27:   fld_arcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H28:   for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           fld_bytes(output_packet), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           output_packet), [i___1]) <= dns_types__byte__last))) .
H29:   answer_count >= dns_types__unsigned_short__first .
H30:   answer_count <= dns_types__unsigned_short__last .
H31:   answer_count~ <= dns_types__unsigned_short__last - 
           rr_type__maxnumrecords .
H32:   start_byte <= dns_types__packet_size .
H33:   current_byte >= dns_types__packet_bytes_range__first .
H34:   current_byte <= dns_types__packet_bytes_range__last .
H35:   (qname_location + 49152) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H36:   (qname_location + 49152) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H37:   current_byte + 1 >= dns_types__packet_bytes_range__first .
H38:   current_byte + 1 <= dns_types__packet_bytes_range__last .
H39:   current_byte + 1 <= dns_types__packet_bytes_range__last - 1 .
H40:   qname_location >= unsigned_types__unsigned16__first .
H41:   qname_location <= unsigned_types__unsigned16__last .
H42:   current_byte + 1 >= dns_types__packet_bytes_range__base__first .
H43:   current_byte + 1 <= dns_types__packet_bytes_range__base__last .
H44:   for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           fld_bytes(output_packet__2), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           output_packet__2), [i___1]) <= dns_types__byte__last))) .
H45:   fld_header(output_packet__2) = fld_header(
           output_packet) .
H46:   output_packet__2 = upf_bytes(output_packet, fld_bytes(
           output_packet__2)) .
H47:   0 >= dns_types__byte__first .
H48:   0 <= dns_types__byte__last .
H49:   current_byte + 3 >= dns_types__packet_bytes_range__first .
H50:   current_byte + 3 <= dns_types__packet_bytes_range__last .
H51:   current_byte + 3 >= dns_types__packet_bytes_range__base__first .
H52:   current_byte + 3 <= dns_types__packet_bytes_range__base__last .
H53:   1 >= dns_types__byte__first .
H54:   1 <= dns_types__byte__last .
H55:   current_byte + 4 >= dns_types__packet_bytes_range__first .
H56:   current_byte + 4 <= dns_types__packet_bytes_range__last .
H57:   current_byte + 4 >= dns_types__packet_bytes_range__base__first .
H58:   current_byte + 4 <= dns_types__packet_bytes_range__base__last .
H59:   0 >= dns_types__byte__first .
H60:   0 <= dns_types__byte__last .
H61:   current_byte + 5 >= dns_types__packet_bytes_range__first .
H62:   current_byte + 5 <= dns_types__packet_bytes_range__last .
H63:   current_byte + 5 >= dns_types__packet_bytes_range__base__first .
H64:   current_byte + 5 <= dns_types__packet_bytes_range__base__last .
H65:   1 >= dns_types__byte__first .
H66:   1 <= dns_types__byte__last .
H67:   current_byte + 6 >= dns_types__packet_bytes_range__first .
H68:   current_byte + 6 <= dns_types__packet_bytes_range__last .
H69:   current_byte + 6 >= dns_types__packet_bytes_range__base__first .
H70:   current_byte + 6 <= dns_types__packet_bytes_range__base__last .
H71:   current_byte >= dns_types__packet_bytes_range__first .
H72:   current_byte <= dns_types__packet_bytes_range__last .
H73:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_ttlinseconds(fld_inherit(element(
           returnedarecords, [i___1]))) >= 
           unsigned_types__unsigned32__first) and (fld_ttlinseconds(
           fld_inherit(element(returnedarecords, [i___1]))) <= 
           unsigned_types__unsigned32__last))) .
H74:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_class(fld_inherit(element(returnedarecords, [
           i___1]))) >= rr_type__classtype__first) and (fld_class(
           fld_inherit(element(returnedarecords, [i___1]))) <= 
           rr_type__classtype__last))) .
H75:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_ipv4(element(returnedarecords, [i___1])) >= 
           unsigned_types__unsigned32__first) and (fld_ipv4(element(
           returnedarecords, [i___1])) <= 
           unsigned_types__unsigned32__last))) .
H76:   response_counter >= natural__first .
H77:   response_counter <= natural__last .
H78:   current_byte + 7 >= dns_types__packet_bytes_range__first .
H79:   current_byte + 7 <= dns_types__packet_bytes_range__last .
H80:   current_byte + 7 <= dns_types__packet_bytes_range__last - 10 .
H81:   rr_type__returnedrecordsindextype__first + (
           response_counter - 1) >= 
           rr_type__returnedrecordsindextype__first .
H82:   rr_type__returnedrecordsindextype__first + (
           response_counter - 1) <= 
           rr_type__returnedrecordsindextype__last .
H83:   rr_type__returnedrecordsindextype__first + (
           response_counter - 1) >= integer__base__first .
H84:   rr_type__returnedrecordsindextype__first + (
           response_counter - 1) <= integer__base__last .
H85:   response_counter - 1 >= integer__base__first .
H86:   response_counter - 1 <= integer__base__last .
H87:   current_byte + 7 >= dns_types__packet_bytes_range__base__first .
H88:   current_byte + 7 <= dns_types__packet_bytes_range__base__last .
H89:   for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           fld_bytes(output_packet__3), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           output_packet__3), [i___1]) <= dns_types__byte__last))) .
H90:   fld_header(output_packet__3) = fld_header(upf_bytes(upf_bytes(
           upf_bytes(upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0)), update(fld_bytes(
           upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0))), [
           current_byte + 4], 1)), update(fld_bytes(upf_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0)), update(fld_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0))), [current_byte + 4], 1))), [
           current_byte + 5], 0)), update(fld_bytes(upf_bytes(upf_bytes(
           upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0)), update(fld_bytes(
           upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0))), [
           current_byte + 4], 1)), update(fld_bytes(upf_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0)), update(fld_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0))), [current_byte + 4], 1))), [
           current_byte + 5], 0))), [current_byte + 6], 1))) .
H91:   output_packet__3 = upf_bytes(upf_bytes(upf_bytes(upf_bytes(
           upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0)), update(fld_bytes(
           upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0))), [
           current_byte + 4], 1)), update(fld_bytes(upf_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0)), update(fld_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0))), [current_byte + 4], 1))), [
           current_byte + 5], 0)), update(fld_bytes(upf_bytes(upf_bytes(
           upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0)), update(fld_bytes(
           upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0))), [
           current_byte + 4], 1)), update(fld_bytes(upf_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0)), update(fld_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0))), [current_byte + 4], 1))), [
           current_byte + 5], 0))), [current_byte + 6], 1)), fld_bytes(
           output_packet__3)) .
H92:   response_counter >= natural__first .
H93:   response_counter <= natural__last .
H94:   response_counter + 1 >= natural__first .
H95:   response_counter + 1 <= natural__last .
H96:   current_byte >= dns_types__packet_bytes_range__first .
H97:   current_byte <= dns_types__packet_bytes_range__last .
        ->
C1:    current_byte + 16 >= dns_types__packet_bytes_range__first .
C2:    current_byte + 16 <= dns_types__packet_bytes_range__last .
 

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

procedure_create_response_a_16.
H1:    answer_count <= dns_types__unsigned_short__last - 
           rr_type__maxnumrecords .
H2:    start_byte <= dns_types__packet_size .
H3:    start_byte >= dns_types__packet_bytes_range__first .
H4:    start_byte <= dns_types__packet_bytes_range__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           domainname, [i___1]) >= character__first) and (element(
           domainname, [i___1]) <= character__last))) .
H6:    qname_location >= dns_types__qname_ptr_range__first .
H7:    qname_location <= dns_types__qname_ptr_range__last .
H8:    fld_messageid(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H9:    fld_messageid(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H10:   fld_opcode(fld_header(output_packet)) >= 
           dns_types__opcode_type__first .
H11:   fld_opcode(fld_header(output_packet)) <= 
           dns_types__opcode_type__last .
H12:   fld_rcode(fld_header(output_packet)) >= 
           dns_types__response_code__first .
H13:   fld_rcode(fld_header(output_packet)) <= 
           dns_types__response_code__last .
H14:   fld_qdcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H15:   fld_qdcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H16:   fld_ancount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H17:   fld_ancount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H18:   fld_nscount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H19:   fld_nscount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H20:   fld_arcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H21:   fld_arcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H22:   for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           fld_bytes(output_packet), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           output_packet), [i___1]) <= dns_types__byte__last))) .
H23:   answer_count >= dns_types__unsigned_short__first .
H24:   answer_count <= dns_types__unsigned_short__last .
H25:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_ttlinseconds(fld_inherit(element(returnedarecords__1, [
           i___1]))) >= unsigned_types__unsigned32__first) and (
           fld_ttlinseconds(fld_inherit(element(returnedarecords__1, [
           i___1]))) <= unsigned_types__unsigned32__last))) .
H26:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_class(fld_inherit(element(returnedarecords__1, [
           i___1]))) >= rr_type__classtype__first) and (fld_class(
           fld_inherit(element(returnedarecords__1, [i___1]))) <= 
           rr_type__classtype__last))) .
H27:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_ipv4(element(returnedarecords__1, [i___1])) >= 
           unsigned_types__unsigned32__first) and (fld_ipv4(element(
           returnedarecords__1, [i___1])) <= 
           unsigned_types__unsigned32__last))) .
H28:   numfound__1 >= rr_type__numberofrecordstype__first .
H29:   numfound__1 <= rr_type__numberofrecordstype__last .
H30:   numfound__1 >= natural__first .
H31:   numfound__1 <= natural__last .
H32:   start_byte >= dns_types__packet_bytes_range__first .
H33:   start_byte <= dns_types__packet_bytes_range__last .
H34:   numfound__1 >= natural__first .
H35:   numfound__1 <= natural__last .
H36:   numfound__1 >= 1 .
H37:   1 >= natural__first .
H38:   1 <= natural__last .
H39:   start_byte >= dns_types__packet_bytes_range__first .
H40:   start_byte <= dns_types__packet_bytes_range__last .
H41:   numfound__1 >= natural__first .
H42:   numfound__1 <= natural__last .
H43:   1 >= natural__first .
H44:   1 <= natural__last .
H45:   dns_types__packet_size - (16 + dns_types__header_bits div 8) >= system__min_int .
H46:   dns_types__packet_size - (16 + dns_types__header_bits div 8) <= system__max_int .
H47:   16 + dns_types__header_bits div 8 >= system__min_int .
H48:   16 + dns_types__header_bits div 8 <= system__max_int .
H49:   dns_types__header_bits div 8 >= system__min_int .
H50:   dns_types__header_bits div 8 <= system__max_int .
H51:   8 <> 0 .
H52:   start_byte >= integer__first .
H53:   start_byte <= integer__last .
H54:   not ((1 <= numfound__1) and (start_byte < 
           dns_types__packet_size - (16 + 
           dns_types__header_bits div 8))) .
H55:   start_byte >= dns_types__packet_bytes_range__first .
H56:   start_byte <= dns_types__packet_bytes_range__last .
        ->
C1:    start_byte + dns_types__header_bits div 8 >= 
           dns_types__packet_length_range__first .
C2:    start_byte + dns_types__header_bits div 8 <= 
           dns_types__packet_length_range__last .
C3:    start_byte + dns_types__header_bits div 8 >= 
           dns_types__packet_length_range__first .
C4:    start_byte + dns_types__header_bits div 8 <= 
           dns_types__packet_length_range__last .
C5:    start_byte + dns_types__header_bits div 8 >= 
           dns_types__packet_bytes_range__base__first .
C6:    start_byte + dns_types__header_bits div 8 <= 
           dns_types__packet_bytes_range__base__last .
C7:    dns_types__header_bits div 8 >= 
           dns_types__packet_bytes_range__first .
C8:    dns_types__header_bits div 8 <= 
           dns_types__packet_bytes_range__last .
C9:    dns_types__header_bits div 8 >= system__min_int .
C10:   dns_types__header_bits div 8 <= system__max_int .
C11:   8 <> 0 .
 

procedure_create_response_a_17.
H1:    answer_count <= dns_types__unsigned_short__last - 
           rr_type__maxnumrecords .
H2:    start_byte <= dns_types__packet_size .
H3:    start_byte >= dns_types__packet_bytes_range__first .
H4:    start_byte <= dns_types__packet_bytes_range__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           domainname, [i___1]) >= character__first) and (element(
           domainname, [i___1]) <= character__last))) .
H6:    qname_location >= dns_types__qname_ptr_range__first .
H7:    qname_location <= dns_types__qname_ptr_range__last .
H8:    fld_messageid(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H9:    fld_messageid(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H10:   fld_opcode(fld_header(output_packet)) >= 
           dns_types__opcode_type__first .
H11:   fld_opcode(fld_header(output_packet)) <= 
           dns_types__opcode_type__last .
H12:   fld_rcode(fld_header(output_packet)) >= 
           dns_types__response_code__first .
H13:   fld_rcode(fld_header(output_packet)) <= 
           dns_types__response_code__last .
H14:   fld_qdcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H15:   fld_qdcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H16:   fld_ancount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H17:   fld_ancount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H18:   fld_nscount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H19:   fld_nscount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H20:   fld_arcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H21:   fld_arcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H22:   for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           fld_bytes(output_packet), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           output_packet), [i___1]) <= dns_types__byte__last))) .
H23:   answer_count >= dns_types__unsigned_short__first .
H24:   answer_count <= dns_types__unsigned_short__last .
H25:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_ttlinseconds(fld_inherit(element(returnedarecords__1, [
           i___1]))) >= unsigned_types__unsigned32__first) and (
           fld_ttlinseconds(fld_inherit(element(returnedarecords__1, [
           i___1]))) <= unsigned_types__unsigned32__last))) .
H26:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_class(fld_inherit(element(returnedarecords__1, [
           i___1]))) >= rr_type__classtype__first) and (fld_class(
           fld_inherit(element(returnedarecords__1, [i___1]))) <= 
           rr_type__classtype__last))) .
H27:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_ipv4(element(returnedarecords__1, [i___1])) >= 
           unsigned_types__unsigned32__first) and (fld_ipv4(element(
           returnedarecords__1, [i___1])) <= 
           unsigned_types__unsigned32__last))) .
H28:   numfound__1 >= rr_type__numberofrecordstype__first .
H29:   numfound__1 <= rr_type__numberofrecordstype__last .
H30:   numfound__1 >= natural__first .
H31:   numfound__1 <= natural__last .
H32:   start_byte >= dns_types__packet_bytes_range__first .
H33:   start_byte <= dns_types__packet_bytes_range__last .
H34:   numfound__1 >= natural__first .
H35:   numfound__1 <= natural__last .
H36:   not (numfound__1 >= 1) .
H37:   start_byte >= dns_types__packet_bytes_range__first .
H38:   start_byte <= dns_types__packet_bytes_range__last .
        ->
C1:    start_byte + dns_types__header_bits div 8 >= 
           dns_types__packet_length_range__first .
C2:    start_byte + dns_types__header_bits div 8 <= 
           dns_types__packet_length_range__last .
C3:    start_byte + dns_types__header_bits div 8 >= 
           dns_types__packet_length_range__first .
C4:    start_byte + dns_types__header_bits div 8 <= 
           dns_types__packet_length_range__last .
C5:    start_byte + dns_types__header_bits div 8 >= 
           dns_types__packet_bytes_range__base__first .
C6:    start_byte + dns_types__header_bits div 8 <= 
           dns_types__packet_bytes_range__base__last .
C7:    dns_types__header_bits div 8 >= 
           dns_types__packet_bytes_range__first .
C8:    dns_types__header_bits div 8 <= 
           dns_types__packet_bytes_range__last .
C9:    dns_types__header_bits div 8 >= system__min_int .
C10:   dns_types__header_bits div 8 <= system__max_int .
C11:   8 <> 0 .
 

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

procedure_create_response_a_18.
H1:    response_counter >= 1 .
H2:    response_counter <= numfound .
H3:    start_byte <= dns_types__packet_size .
H4:    answer_count = answer_count~ .
H5:    answer_count <= dns_types__unsigned_short__last - 
           rr_type__maxnumrecords .
H6:    current_byte = start_byte + 16 * (response_counter - 1) .
H7:    current_byte < dns_types__packet_size - (16 + 
           dns_types__header_bits div 8) .
H8:    numfound <= rr_type__maxnumrecords .
H9:    start_byte >= dns_types__packet_bytes_range__first .
H10:   start_byte <= dns_types__packet_bytes_range__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           domainname, [i___1]) >= character__first) and (element(
           domainname, [i___1]) <= character__last))) .
H12:   qname_location >= dns_types__qname_ptr_range__first .
H13:   qname_location <= dns_types__qname_ptr_range__last .
H14:   fld_messageid(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H15:   fld_messageid(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H16:   fld_opcode(fld_header(output_packet)) >= 
           dns_types__opcode_type__first .
H17:   fld_opcode(fld_header(output_packet)) <= 
           dns_types__opcode_type__last .
H18:   fld_rcode(fld_header(output_packet)) >= 
           dns_types__response_code__first .
H19:   fld_rcode(fld_header(output_packet)) <= 
           dns_types__response_code__last .
H20:   fld_qdcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H21:   fld_qdcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H22:   fld_ancount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H23:   fld_ancount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H24:   fld_nscount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H25:   fld_nscount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H26:   fld_arcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H27:   fld_arcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H28:   for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           fld_bytes(output_packet), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           output_packet), [i___1]) <= dns_types__byte__last))) .
H29:   answer_count >= dns_types__unsigned_short__first .
H30:   answer_count <= dns_types__unsigned_short__last .
H31:   answer_count~ <= dns_types__unsigned_short__last - 
           rr_type__maxnumrecords .
H32:   start_byte <= dns_types__packet_size .
H33:   current_byte >= dns_types__packet_bytes_range__first .
H34:   current_byte <= dns_types__packet_bytes_range__last .
H35:   (qname_location + 49152) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H36:   (qname_location + 49152) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H37:   current_byte + 1 >= dns_types__packet_bytes_range__first .
H38:   current_byte + 1 <= dns_types__packet_bytes_range__last .
H39:   current_byte + 1 <= dns_types__packet_bytes_range__last - 1 .
H40:   qname_location >= unsigned_types__unsigned16__first .
H41:   qname_location <= unsigned_types__unsigned16__last .
H42:   current_byte + 1 >= dns_types__packet_bytes_range__base__first .
H43:   current_byte + 1 <= dns_types__packet_bytes_range__base__last .
H44:   for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           fld_bytes(output_packet__2), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           output_packet__2), [i___1]) <= dns_types__byte__last))) .
H45:   fld_header(output_packet__2) = fld_header(
           output_packet) .
H46:   output_packet__2 = upf_bytes(output_packet, fld_bytes(
           output_packet__2)) .
H47:   0 >= dns_types__byte__first .
H48:   0 <= dns_types__byte__last .
H49:   current_byte + 3 >= dns_types__packet_bytes_range__first .
H50:   current_byte + 3 <= dns_types__packet_bytes_range__last .
H51:   current_byte + 3 >= dns_types__packet_bytes_range__base__first .
H52:   current_byte + 3 <= dns_types__packet_bytes_range__base__last .
H53:   1 >= dns_types__byte__first .
H54:   1 <= dns_types__byte__last .
H55:   current_byte + 4 >= dns_types__packet_bytes_range__first .
H56:   current_byte + 4 <= dns_types__packet_bytes_range__last .
H57:   current_byte + 4 >= dns_types__packet_bytes_range__base__first .
H58:   current_byte + 4 <= dns_types__packet_bytes_range__base__last .
H59:   0 >= dns_types__byte__first .
H60:   0 <= dns_types__byte__last .
H61:   current_byte + 5 >= dns_types__packet_bytes_range__first .
H62:   current_byte + 5 <= dns_types__packet_bytes_range__last .
H63:   current_byte + 5 >= dns_types__packet_bytes_range__base__first .
H64:   current_byte + 5 <= dns_types__packet_bytes_range__base__last .
H65:   1 >= dns_types__byte__first .
H66:   1 <= dns_types__byte__last .
H67:   current_byte + 6 >= dns_types__packet_bytes_range__first .
H68:   current_byte + 6 <= dns_types__packet_bytes_range__last .
H69:   current_byte + 6 >= dns_types__packet_bytes_range__base__first .
H70:   current_byte + 6 <= dns_types__packet_bytes_range__base__last .
H71:   current_byte >= dns_types__packet_bytes_range__first .
H72:   current_byte <= dns_types__packet_bytes_range__last .
H73:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_ttlinseconds(fld_inherit(element(
           returnedarecords, [i___1]))) >= 
           unsigned_types__unsigned32__first) and (fld_ttlinseconds(
           fld_inherit(element(returnedarecords, [i___1]))) <= 
           unsigned_types__unsigned32__last))) .
H74:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_class(fld_inherit(element(returnedarecords, [
           i___1]))) >= rr_type__classtype__first) and (fld_class(
           fld_inherit(element(returnedarecords, [i___1]))) <= 
           rr_type__classtype__last))) .
H75:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_ipv4(element(returnedarecords, [i___1])) >= 
           unsigned_types__unsigned32__first) and (fld_ipv4(element(
           returnedarecords, [i___1])) <= 
           unsigned_types__unsigned32__last))) .
H76:   response_counter >= natural__first .
H77:   response_counter <= natural__last .
H78:   current_byte + 7 >= dns_types__packet_bytes_range__first .
H79:   current_byte + 7 <= dns_types__packet_bytes_range__last .
H80:   current_byte + 7 <= dns_types__packet_bytes_range__last - 10 .
H81:   rr_type__returnedrecordsindextype__first + (
           response_counter - 1) >= 
           rr_type__returnedrecordsindextype__first .
H82:   rr_type__returnedrecordsindextype__first + (
           response_counter - 1) <= 
           rr_type__returnedrecordsindextype__last .
H83:   rr_type__returnedrecordsindextype__first + (
           response_counter - 1) >= integer__base__first .
H84:   rr_type__returnedrecordsindextype__first + (
           response_counter - 1) <= integer__base__last .
H85:   response_counter - 1 >= integer__base__first .
H86:   response_counter - 1 <= integer__base__last .
H87:   current_byte + 7 >= dns_types__packet_bytes_range__base__first .
H88:   current_byte + 7 <= dns_types__packet_bytes_range__base__last .
H89:   for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           fld_bytes(output_packet__3), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           output_packet__3), [i___1]) <= dns_types__byte__last))) .
H90:   fld_header(output_packet__3) = fld_header(upf_bytes(upf_bytes(
           upf_bytes(upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0)), update(fld_bytes(
           upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0))), [
           current_byte + 4], 1)), update(fld_bytes(upf_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0)), update(fld_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0))), [current_byte + 4], 1))), [
           current_byte + 5], 0)), update(fld_bytes(upf_bytes(upf_bytes(
           upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0)), update(fld_bytes(
           upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0))), [
           current_byte + 4], 1)), update(fld_bytes(upf_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0)), update(fld_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0))), [current_byte + 4], 1))), [
           current_byte + 5], 0))), [current_byte + 6], 1))) .
H91:   output_packet__3 = upf_bytes(upf_bytes(upf_bytes(upf_bytes(
           upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0)), update(fld_bytes(
           upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0))), [
           current_byte + 4], 1)), update(fld_bytes(upf_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0)), update(fld_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0))), [current_byte + 4], 1))), [
           current_byte + 5], 0)), update(fld_bytes(upf_bytes(upf_bytes(
           upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0)), update(fld_bytes(
           upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0))), [
           current_byte + 4], 1)), update(fld_bytes(upf_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0)), update(fld_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0))), [current_byte + 4], 1))), [
           current_byte + 5], 0))), [current_byte + 6], 1)), fld_bytes(
           output_packet__3)) .
H92:   response_counter >= natural__first .
H93:   response_counter <= natural__last .
H94:   response_counter + 1 >= natural__first .
H95:   response_counter + 1 <= natural__last .
H96:   current_byte >= dns_types__packet_bytes_range__first .
H97:   current_byte <= dns_types__packet_bytes_range__last .
H98:   current_byte + 16 >= dns_types__packet_bytes_range__first .
H99:   current_byte + 16 <= dns_types__packet_bytes_range__last .
H100:  current_byte + 16 >= dns_types__packet_bytes_range__first .
H101:  current_byte + 16 <= dns_types__packet_bytes_range__last .
H102:  numfound >= natural__first .
H103:  numfound <= natural__last .
H104:  response_counter + 1 >= natural__first .
H105:  response_counter + 1 <= natural__last .
H106:  dns_types__packet_size - (16 + dns_types__header_bits div 8) >= system__min_int .
H107:  dns_types__packet_size - (16 + dns_types__header_bits div 8) <= system__max_int .
H108:  16 + dns_types__header_bits div 8 >= system__min_int .
H109:  16 + dns_types__header_bits div 8 <= system__max_int .
H110:  dns_types__header_bits div 8 >= system__min_int .
H111:  dns_types__header_bits div 8 <= system__max_int .
H112:  8 <> 0 .
H113:  current_byte + 16 >= integer__first .
H114:  current_byte + 16 <= integer__last .
H115:  not ((response_counter + 1 <= numfound) and (
           current_byte + 16 < dns_types__packet_size - (16 + 
           dns_types__header_bits div 8))) .
H116:  current_byte + 16 >= dns_types__packet_bytes_range__first .
H117:  current_byte + 16 <= dns_types__packet_bytes_range__last .
        ->
C1:    current_byte + 16 + dns_types__header_bits div 8 >= 
           dns_types__packet_length_range__first .
C2:    current_byte + 16 + dns_types__header_bits div 8 <= 
           dns_types__packet_length_range__last .
C3:    current_byte + 16 + dns_types__header_bits div 8 >= 
           dns_types__packet_length_range__first .
C4:    current_byte + 16 + dns_types__header_bits div 8 <= 
           dns_types__packet_length_range__last .
C5:    current_byte + 16 + dns_types__header_bits div 8 >= 
           dns_types__packet_bytes_range__base__first .
C6:    current_byte + 16 + dns_types__header_bits div 8 <= 
           dns_types__packet_bytes_range__base__last .
C7:    dns_types__header_bits div 8 >= 
           dns_types__packet_bytes_range__first .
C8:    dns_types__header_bits div 8 <= 
           dns_types__packet_bytes_range__last .
C9:    dns_types__header_bits div 8 >= system__min_int .
C10:   dns_types__header_bits div 8 <= system__max_int .
C11:   8 <> 0 .
 

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

procedure_create_response_a_19.
H1:    answer_count <= dns_types__unsigned_short__last - 
           rr_type__maxnumrecords .
H2:    start_byte <= dns_types__packet_size .
H3:    start_byte >= dns_types__packet_bytes_range__first .
H4:    start_byte <= dns_types__packet_bytes_range__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           domainname, [i___1]) >= character__first) and (element(
           domainname, [i___1]) <= character__last))) .
H6:    qname_location >= dns_types__qname_ptr_range__first .
H7:    qname_location <= dns_types__qname_ptr_range__last .
H8:    fld_messageid(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H9:    fld_messageid(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H10:   fld_opcode(fld_header(output_packet)) >= 
           dns_types__opcode_type__first .
H11:   fld_opcode(fld_header(output_packet)) <= 
           dns_types__opcode_type__last .
H12:   fld_rcode(fld_header(output_packet)) >= 
           dns_types__response_code__first .
H13:   fld_rcode(fld_header(output_packet)) <= 
           dns_types__response_code__last .
H14:   fld_qdcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H15:   fld_qdcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H16:   fld_ancount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H17:   fld_ancount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H18:   fld_nscount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H19:   fld_nscount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H20:   fld_arcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H21:   fld_arcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H22:   for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           fld_bytes(output_packet), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           output_packet), [i___1]) <= dns_types__byte__last))) .
H23:   answer_count >= dns_types__unsigned_short__first .
H24:   answer_count <= dns_types__unsigned_short__last .
H25:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_ttlinseconds(fld_inherit(element(returnedarecords__1, [
           i___1]))) >= unsigned_types__unsigned32__first) and (
           fld_ttlinseconds(fld_inherit(element(returnedarecords__1, [
           i___1]))) <= unsigned_types__unsigned32__last))) .
H26:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_class(fld_inherit(element(returnedarecords__1, [
           i___1]))) >= rr_type__classtype__first) and (fld_class(
           fld_inherit(element(returnedarecords__1, [i___1]))) <= 
           rr_type__classtype__last))) .
H27:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_ipv4(element(returnedarecords__1, [i___1])) >= 
           unsigned_types__unsigned32__first) and (fld_ipv4(element(
           returnedarecords__1, [i___1])) <= 
           unsigned_types__unsigned32__last))) .
H28:   numfound__1 >= rr_type__numberofrecordstype__first .
H29:   numfound__1 <= rr_type__numberofrecordstype__last .
H30:   numfound__1 >= natural__first .
H31:   numfound__1 <= natural__last .
H32:   start_byte >= dns_types__packet_bytes_range__first .
H33:   start_byte <= dns_types__packet_bytes_range__last .
H34:   numfound__1 >= natural__first .
H35:   numfound__1 <= natural__last .
H36:   numfound__1 >= 1 .
H37:   1 >= natural__first .
H38:   1 <= natural__last .
H39:   start_byte >= dns_types__packet_bytes_range__first .
H40:   start_byte <= dns_types__packet_bytes_range__last .
H41:   numfound__1 >= natural__first .
H42:   numfound__1 <= natural__last .
H43:   1 >= natural__first .
H44:   1 <= natural__last .
H45:   dns_types__packet_size - (16 + dns_types__header_bits div 8) >= system__min_int .
H46:   dns_types__packet_size - (16 + dns_types__header_bits div 8) <= system__max_int .
H47:   16 + dns_types__header_bits div 8 >= system__min_int .
H48:   16 + dns_types__header_bits div 8 <= system__max_int .
H49:   dns_types__header_bits div 8 >= system__min_int .
H50:   dns_types__header_bits div 8 <= system__max_int .
H51:   8 <> 0 .
H52:   start_byte >= integer__first .
H53:   start_byte <= integer__last .
H54:   not ((1 <= numfound__1) and (start_byte < 
           dns_types__packet_size - (16 + 
           dns_types__header_bits div 8))) .
H55:   start_byte >= dns_types__packet_bytes_range__first .
H56:   start_byte <= dns_types__packet_bytes_range__last .
H57:   start_byte + dns_types__header_bits div 8 >= 
           dns_types__packet_length_range__first .
H58:   start_byte + dns_types__header_bits div 8 <= 
           dns_types__packet_length_range__last .
H59:   start_byte + dns_types__header_bits div 8 >= 
           dns_types__packet_length_range__first .
H60:   start_byte + dns_types__header_bits div 8 <= 
           dns_types__packet_length_range__last .
H61:   start_byte + dns_types__header_bits div 8 >= 
           dns_types__packet_bytes_range__base__first .
H62:   start_byte + dns_types__header_bits div 8 <= 
           dns_types__packet_bytes_range__base__last .
H63:   dns_types__header_bits div 8 >= 
           dns_types__packet_bytes_range__first .
H64:   dns_types__header_bits div 8 <= 
           dns_types__packet_bytes_range__last .
H65:   dns_types__header_bits div 8 >= system__min_int .
H66:   dns_types__header_bits div 8 <= system__max_int .
H67:   8 <> 0 .
H68:   numfound__1 >= natural__first .
H69:   numfound__1 <= natural__last .
        ->
C1:    answer_count + numfound__1 >= 
           dns_types__unsigned_short__first .
C2:    answer_count + numfound__1 <= 
           dns_types__unsigned_short__last .
C3:    numfound__1 >= dns_types__unsigned_short__first .
C4:    numfound__1 <= dns_types__unsigned_short__last .
 

procedure_create_response_a_20.
H1:    answer_count <= dns_types__unsigned_short__last - 
           rr_type__maxnumrecords .
H2:    start_byte <= dns_types__packet_size .
H3:    start_byte >= dns_types__packet_bytes_range__first .
H4:    start_byte <= dns_types__packet_bytes_range__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           domainname, [i___1]) >= character__first) and (element(
           domainname, [i___1]) <= character__last))) .
H6:    qname_location >= dns_types__qname_ptr_range__first .
H7:    qname_location <= dns_types__qname_ptr_range__last .
H8:    fld_messageid(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H9:    fld_messageid(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H10:   fld_opcode(fld_header(output_packet)) >= 
           dns_types__opcode_type__first .
H11:   fld_opcode(fld_header(output_packet)) <= 
           dns_types__opcode_type__last .
H12:   fld_rcode(fld_header(output_packet)) >= 
           dns_types__response_code__first .
H13:   fld_rcode(fld_header(output_packet)) <= 
           dns_types__response_code__last .
H14:   fld_qdcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H15:   fld_qdcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H16:   fld_ancount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H17:   fld_ancount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H18:   fld_nscount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H19:   fld_nscount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H20:   fld_arcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H21:   fld_arcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H22:   for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           fld_bytes(output_packet), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           output_packet), [i___1]) <= dns_types__byte__last))) .
H23:   answer_count >= dns_types__unsigned_short__first .
H24:   answer_count <= dns_types__unsigned_short__last .
H25:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_ttlinseconds(fld_inherit(element(returnedarecords__1, [
           i___1]))) >= unsigned_types__unsigned32__first) and (
           fld_ttlinseconds(fld_inherit(element(returnedarecords__1, [
           i___1]))) <= unsigned_types__unsigned32__last))) .
H26:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_class(fld_inherit(element(returnedarecords__1, [
           i___1]))) >= rr_type__classtype__first) and (fld_class(
           fld_inherit(element(returnedarecords__1, [i___1]))) <= 
           rr_type__classtype__last))) .
H27:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_ipv4(element(returnedarecords__1, [i___1])) >= 
           unsigned_types__unsigned32__first) and (fld_ipv4(element(
           returnedarecords__1, [i___1])) <= 
           unsigned_types__unsigned32__last))) .
H28:   numfound__1 >= rr_type__numberofrecordstype__first .
H29:   numfound__1 <= rr_type__numberofrecordstype__last .
H30:   numfound__1 >= natural__first .
H31:   numfound__1 <= natural__last .
H32:   start_byte >= dns_types__packet_bytes_range__first .
H33:   start_byte <= dns_types__packet_bytes_range__last .
H34:   numfound__1 >= natural__first .
H35:   numfound__1 <= natural__last .
H36:   not (numfound__1 >= 1) .
H37:   start_byte >= dns_types__packet_bytes_range__first .
H38:   start_byte <= dns_types__packet_bytes_range__last .
H39:   start_byte + dns_types__header_bits div 8 >= 
           dns_types__packet_length_range__first .
H40:   start_byte + dns_types__header_bits div 8 <= 
           dns_types__packet_length_range__last .
H41:   start_byte + dns_types__header_bits div 8 >= 
           dns_types__packet_length_range__first .
H42:   start_byte + dns_types__header_bits div 8 <= 
           dns_types__packet_length_range__last .
H43:   start_byte + dns_types__header_bits div 8 >= 
           dns_types__packet_bytes_range__base__first .
H44:   start_byte + dns_types__header_bits div 8 <= 
           dns_types__packet_bytes_range__base__last .
H45:   dns_types__header_bits div 8 >= 
           dns_types__packet_bytes_range__first .
H46:   dns_types__header_bits div 8 <= 
           dns_types__packet_bytes_range__last .
H47:   dns_types__header_bits div 8 >= system__min_int .
H48:   dns_types__header_bits div 8 <= system__max_int .
H49:   8 <> 0 .
H50:   numfound__1 >= natural__first .
H51:   numfound__1 <= natural__last .
        ->
C1:    answer_count + numfound__1 >= 
           dns_types__unsigned_short__first .
C2:    answer_count + numfound__1 <= 
           dns_types__unsigned_short__last .
C3:    numfound__1 >= dns_types__unsigned_short__first .
C4:    numfound__1 <= dns_types__unsigned_short__last .
 

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

procedure_create_response_a_21.
H1:    response_counter >= 1 .
H2:    response_counter <= numfound .
H3:    start_byte <= dns_types__packet_size .
H4:    answer_count = answer_count~ .
H5:    answer_count <= dns_types__unsigned_short__last - 
           rr_type__maxnumrecords .
H6:    current_byte = start_byte + 16 * (response_counter - 1) .
H7:    current_byte < dns_types__packet_size - (16 + 
           dns_types__header_bits div 8) .
H8:    numfound <= rr_type__maxnumrecords .
H9:    start_byte >= dns_types__packet_bytes_range__first .
H10:   start_byte <= dns_types__packet_bytes_range__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           domainname, [i___1]) >= character__first) and (element(
           domainname, [i___1]) <= character__last))) .
H12:   qname_location >= dns_types__qname_ptr_range__first .
H13:   qname_location <= dns_types__qname_ptr_range__last .
H14:   fld_messageid(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H15:   fld_messageid(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H16:   fld_opcode(fld_header(output_packet)) >= 
           dns_types__opcode_type__first .
H17:   fld_opcode(fld_header(output_packet)) <= 
           dns_types__opcode_type__last .
H18:   fld_rcode(fld_header(output_packet)) >= 
           dns_types__response_code__first .
H19:   fld_rcode(fld_header(output_packet)) <= 
           dns_types__response_code__last .
H20:   fld_qdcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H21:   fld_qdcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H22:   fld_ancount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H23:   fld_ancount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H24:   fld_nscount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H25:   fld_nscount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H26:   fld_arcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H27:   fld_arcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H28:   for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           fld_bytes(output_packet), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           output_packet), [i___1]) <= dns_types__byte__last))) .
H29:   answer_count >= dns_types__unsigned_short__first .
H30:   answer_count <= dns_types__unsigned_short__last .
H31:   answer_count~ <= dns_types__unsigned_short__last - 
           rr_type__maxnumrecords .
H32:   start_byte <= dns_types__packet_size .
H33:   current_byte >= dns_types__packet_bytes_range__first .
H34:   current_byte <= dns_types__packet_bytes_range__last .
H35:   (qname_location + 49152) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H36:   (qname_location + 49152) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H37:   current_byte + 1 >= dns_types__packet_bytes_range__first .
H38:   current_byte + 1 <= dns_types__packet_bytes_range__last .
H39:   current_byte + 1 <= dns_types__packet_bytes_range__last - 1 .
H40:   qname_location >= unsigned_types__unsigned16__first .
H41:   qname_location <= unsigned_types__unsigned16__last .
H42:   current_byte + 1 >= dns_types__packet_bytes_range__base__first .
H43:   current_byte + 1 <= dns_types__packet_bytes_range__base__last .
H44:   for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           fld_bytes(output_packet__2), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           output_packet__2), [i___1]) <= dns_types__byte__last))) .
H45:   fld_header(output_packet__2) = fld_header(
           output_packet) .
H46:   output_packet__2 = upf_bytes(output_packet, fld_bytes(
           output_packet__2)) .
H47:   0 >= dns_types__byte__first .
H48:   0 <= dns_types__byte__last .
H49:   current_byte + 3 >= dns_types__packet_bytes_range__first .
H50:   current_byte + 3 <= dns_types__packet_bytes_range__last .
H51:   current_byte + 3 >= dns_types__packet_bytes_range__base__first .
H52:   current_byte + 3 <= dns_types__packet_bytes_range__base__last .
H53:   1 >= dns_types__byte__first .
H54:   1 <= dns_types__byte__last .
H55:   current_byte + 4 >= dns_types__packet_bytes_range__first .
H56:   current_byte + 4 <= dns_types__packet_bytes_range__last .
H57:   current_byte + 4 >= dns_types__packet_bytes_range__base__first .
H58:   current_byte + 4 <= dns_types__packet_bytes_range__base__last .
H59:   0 >= dns_types__byte__first .
H60:   0 <= dns_types__byte__last .
H61:   current_byte + 5 >= dns_types__packet_bytes_range__first .
H62:   current_byte + 5 <= dns_types__packet_bytes_range__last .
H63:   current_byte + 5 >= dns_types__packet_bytes_range__base__first .
H64:   current_byte + 5 <= dns_types__packet_bytes_range__base__last .
H65:   1 >= dns_types__byte__first .
H66:   1 <= dns_types__byte__last .
H67:   current_byte + 6 >= dns_types__packet_bytes_range__first .
H68:   current_byte + 6 <= dns_types__packet_bytes_range__last .
H69:   current_byte + 6 >= dns_types__packet_bytes_range__base__first .
H70:   current_byte + 6 <= dns_types__packet_bytes_range__base__last .
H71:   current_byte >= dns_types__packet_bytes_range__first .
H72:   current_byte <= dns_types__packet_bytes_range__last .
H73:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_ttlinseconds(fld_inherit(element(
           returnedarecords, [i___1]))) >= 
           unsigned_types__unsigned32__first) and (fld_ttlinseconds(
           fld_inherit(element(returnedarecords, [i___1]))) <= 
           unsigned_types__unsigned32__last))) .
H74:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_class(fld_inherit(element(returnedarecords, [
           i___1]))) >= rr_type__classtype__first) and (fld_class(
           fld_inherit(element(returnedarecords, [i___1]))) <= 
           rr_type__classtype__last))) .
H75:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_ipv4(element(returnedarecords, [i___1])) >= 
           unsigned_types__unsigned32__first) and (fld_ipv4(element(
           returnedarecords, [i___1])) <= 
           unsigned_types__unsigned32__last))) .
H76:   response_counter >= natural__first .
H77:   response_counter <= natural__last .
H78:   current_byte + 7 >= dns_types__packet_bytes_range__first .
H79:   current_byte + 7 <= dns_types__packet_bytes_range__last .
H80:   current_byte + 7 <= dns_types__packet_bytes_range__last - 10 .
H81:   rr_type__returnedrecordsindextype__first + (
           response_counter - 1) >= 
           rr_type__returnedrecordsindextype__first .
H82:   rr_type__returnedrecordsindextype__first + (
           response_counter - 1) <= 
           rr_type__returnedrecordsindextype__last .
H83:   rr_type__returnedrecordsindextype__first + (
           response_counter - 1) >= integer__base__first .
H84:   rr_type__returnedrecordsindextype__first + (
           response_counter - 1) <= integer__base__last .
H85:   response_counter - 1 >= integer__base__first .
H86:   response_counter - 1 <= integer__base__last .
H87:   current_byte + 7 >= dns_types__packet_bytes_range__base__first .
H88:   current_byte + 7 <= dns_types__packet_bytes_range__base__last .
H89:   for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           fld_bytes(output_packet__3), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           output_packet__3), [i___1]) <= dns_types__byte__last))) .
H90:   fld_header(output_packet__3) = fld_header(upf_bytes(upf_bytes(
           upf_bytes(upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0)), update(fld_bytes(
           upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0))), [
           current_byte + 4], 1)), update(fld_bytes(upf_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0)), update(fld_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0))), [current_byte + 4], 1))), [
           current_byte + 5], 0)), update(fld_bytes(upf_bytes(upf_bytes(
           upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0)), update(fld_bytes(
           upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0))), [
           current_byte + 4], 1)), update(fld_bytes(upf_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0)), update(fld_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0))), [current_byte + 4], 1))), [
           current_byte + 5], 0))), [current_byte + 6], 1))) .
H91:   output_packet__3 = upf_bytes(upf_bytes(upf_bytes(upf_bytes(
           upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0)), update(fld_bytes(
           upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0))), [
           current_byte + 4], 1)), update(fld_bytes(upf_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0)), update(fld_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0))), [current_byte + 4], 1))), [
           current_byte + 5], 0)), update(fld_bytes(upf_bytes(upf_bytes(
           upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0)), update(fld_bytes(
           upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0))), [
           current_byte + 4], 1)), update(fld_bytes(upf_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0)), update(fld_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0))), [current_byte + 4], 1))), [
           current_byte + 5], 0))), [current_byte + 6], 1)), fld_bytes(
           output_packet__3)) .
H92:   response_counter >= natural__first .
H93:   response_counter <= natural__last .
H94:   response_counter + 1 >= natural__first .
H95:   response_counter + 1 <= natural__last .
H96:   current_byte >= dns_types__packet_bytes_range__first .
H97:   current_byte <= dns_types__packet_bytes_range__last .
H98:   current_byte + 16 >= dns_types__packet_bytes_range__first .
H99:   current_byte + 16 <= dns_types__packet_bytes_range__last .
H100:  current_byte + 16 >= dns_types__packet_bytes_range__first .
H101:  current_byte + 16 <= dns_types__packet_bytes_range__last .
H102:  numfound >= natural__first .
H103:  numfound <= natural__last .
H104:  response_counter + 1 >= natural__first .
H105:  response_counter + 1 <= natural__last .
H106:  dns_types__packet_size - (16 + dns_types__header_bits div 8) >= system__min_int .
H107:  dns_types__packet_size - (16 + dns_types__header_bits div 8) <= system__max_int .
H108:  16 + dns_types__header_bits div 8 >= system__min_int .
H109:  16 + dns_types__header_bits div 8 <= system__max_int .
H110:  dns_types__header_bits div 8 >= system__min_int .
H111:  dns_types__header_bits div 8 <= system__max_int .
H112:  8 <> 0 .
H113:  current_byte + 16 >= integer__first .
H114:  current_byte + 16 <= integer__last .
H115:  not ((response_counter + 1 <= numfound) and (
           current_byte + 16 < dns_types__packet_size - (16 + 
           dns_types__header_bits div 8))) .
H116:  current_byte + 16 >= dns_types__packet_bytes_range__first .
H117:  current_byte + 16 <= dns_types__packet_bytes_range__last .
H118:  current_byte + 16 + dns_types__header_bits div 8 >= 
           dns_types__packet_length_range__first .
H119:  current_byte + 16 + dns_types__header_bits div 8 <= 
           dns_types__packet_length_range__last .
H120:  current_byte + 16 + dns_types__header_bits div 8 >= 
           dns_types__packet_length_range__first .
H121:  current_byte + 16 + dns_types__header_bits div 8 <= 
           dns_types__packet_length_range__last .
H122:  current_byte + 16 + dns_types__header_bits div 8 >= 
           dns_types__packet_bytes_range__base__first .
H123:  current_byte + 16 + dns_types__header_bits div 8 <= 
           dns_types__packet_bytes_range__base__last .
H124:  dns_types__header_bits div 8 >= 
           dns_types__packet_bytes_range__first .
H125:  dns_types__header_bits div 8 <= 
           dns_types__packet_bytes_range__last .
H126:  dns_types__header_bits div 8 >= system__min_int .
H127:  dns_types__header_bits div 8 <= system__max_int .
H128:  8 <> 0 .
H129:  numfound >= natural__first .
H130:  numfound <= natural__last .
        ->
C1:    answer_count + numfound >= dns_types__unsigned_short__first .
C2:    answer_count + numfound <= dns_types__unsigned_short__last .
C3:    numfound >= dns_types__unsigned_short__first .
C4:    numfound <= dns_types__unsigned_short__last .
 

For path(s) from start to finish:

procedure_create_response_a_22.
H1:    answer_count <= dns_types__unsigned_short__last - 
           rr_type__maxnumrecords .
H2:    start_byte <= dns_types__packet_size .
H3:    start_byte >= dns_types__packet_bytes_range__first .
H4:    start_byte <= dns_types__packet_bytes_range__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           domainname, [i___1]) >= character__first) and (element(
           domainname, [i___1]) <= character__last))) .
H6:    qname_location >= dns_types__qname_ptr_range__first .
H7:    qname_location <= dns_types__qname_ptr_range__last .
H8:    fld_messageid(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H9:    fld_messageid(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H10:   fld_opcode(fld_header(output_packet)) >= 
           dns_types__opcode_type__first .
H11:   fld_opcode(fld_header(output_packet)) <= 
           dns_types__opcode_type__last .
H12:   fld_rcode(fld_header(output_packet)) >= 
           dns_types__response_code__first .
H13:   fld_rcode(fld_header(output_packet)) <= 
           dns_types__response_code__last .
H14:   fld_qdcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H15:   fld_qdcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H16:   fld_ancount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H17:   fld_ancount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H18:   fld_nscount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H19:   fld_nscount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H20:   fld_arcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H21:   fld_arcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H22:   for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           fld_bytes(output_packet), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           output_packet), [i___1]) <= dns_types__byte__last))) .
H23:   answer_count >= dns_types__unsigned_short__first .
H24:   answer_count <= dns_types__unsigned_short__last .
H25:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_ttlinseconds(fld_inherit(element(returnedarecords__1, [
           i___1]))) >= unsigned_types__unsigned32__first) and (
           fld_ttlinseconds(fld_inherit(element(returnedarecords__1, [
           i___1]))) <= unsigned_types__unsigned32__last))) .
H26:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_class(fld_inherit(element(returnedarecords__1, [
           i___1]))) >= rr_type__classtype__first) and (fld_class(
           fld_inherit(element(returnedarecords__1, [i___1]))) <= 
           rr_type__classtype__last))) .
H27:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_ipv4(element(returnedarecords__1, [i___1])) >= 
           unsigned_types__unsigned32__first) and (fld_ipv4(element(
           returnedarecords__1, [i___1])) <= 
           unsigned_types__unsigned32__last))) .
H28:   numfound__1 >= rr_type__numberofrecordstype__first .
H29:   numfound__1 <= rr_type__numberofrecordstype__last .
H30:   numfound__1 >= natural__first .
H31:   numfound__1 <= natural__last .
H32:   start_byte >= dns_types__packet_bytes_range__first .
H33:   start_byte <= dns_types__packet_bytes_range__last .
H34:   numfound__1 >= natural__first .
H35:   numfound__1 <= natural__last .
H36:   numfound__1 >= 1 .
H37:   1 >= natural__first .
H38:   1 <= natural__last .
H39:   start_byte >= dns_types__packet_bytes_range__first .
H40:   start_byte <= dns_types__packet_bytes_range__last .
H41:   numfound__1 >= natural__first .
H42:   numfound__1 <= natural__last .
H43:   1 >= natural__first .
H44:   1 <= natural__last .
H45:   dns_types__packet_size - (16 + dns_types__header_bits div 8) >= system__min_int .
H46:   dns_types__packet_size - (16 + dns_types__header_bits div 8) <= system__max_int .
H47:   16 + dns_types__header_bits div 8 >= system__min_int .
H48:   16 + dns_types__header_bits div 8 <= system__max_int .
H49:   dns_types__header_bits div 8 >= system__min_int .
H50:   dns_types__header_bits div 8 <= system__max_int .
H51:   8 <> 0 .
H52:   start_byte >= integer__first .
H53:   start_byte <= integer__last .
H54:   not ((1 <= numfound__1) and (start_byte < 
           dns_types__packet_size - (16 + 
           dns_types__header_bits div 8))) .
H55:   start_byte >= dns_types__packet_bytes_range__first .
H56:   start_byte <= dns_types__packet_bytes_range__last .
H57:   start_byte + dns_types__header_bits div 8 >= 
           dns_types__packet_length_range__first .
H58:   start_byte + dns_types__header_bits div 8 <= 
           dns_types__packet_length_range__last .
H59:   start_byte + dns_types__header_bits div 8 >= 
           dns_types__packet_length_range__first .
H60:   start_byte + dns_types__header_bits div 8 <= 
           dns_types__packet_length_range__last .
H61:   start_byte + dns_types__header_bits div 8 >= 
           dns_types__packet_bytes_range__base__first .
H62:   start_byte + dns_types__header_bits div 8 <= 
           dns_types__packet_bytes_range__base__last .
H63:   dns_types__header_bits div 8 >= 
           dns_types__packet_bytes_range__first .
H64:   dns_types__header_bits div 8 <= 
           dns_types__packet_bytes_range__last .
H65:   dns_types__header_bits div 8 >= system__min_int .
H66:   dns_types__header_bits div 8 <= system__max_int .
H67:   8 <> 0 .
H68:   numfound__1 >= natural__first .
H69:   numfound__1 <= natural__last .
H70:   answer_count + numfound__1 >= 
           dns_types__unsigned_short__first .
H71:   answer_count + numfound__1 <= 
           dns_types__unsigned_short__last .
H72:   numfound__1 >= dns_types__unsigned_short__first .
H73:   numfound__1 <= dns_types__unsigned_short__last .
        ->
C1:    start_byte + dns_types__header_bits div 8 >= 
           dns_types__header_bits div 8 + 1 .
C2:    start_byte + dns_types__header_bits div 8 <= 
           dns_types__packet_size .
C3:    answer_count + numfound__1 <= answer_count + 
           rr_type__maxnumrecords .
 

procedure_create_response_a_23.
H1:    answer_count <= dns_types__unsigned_short__last - 
           rr_type__maxnumrecords .
H2:    start_byte <= dns_types__packet_size .
H3:    start_byte >= dns_types__packet_bytes_range__first .
H4:    start_byte <= dns_types__packet_bytes_range__last .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           domainname, [i___1]) >= character__first) and (element(
           domainname, [i___1]) <= character__last))) .
H6:    qname_location >= dns_types__qname_ptr_range__first .
H7:    qname_location <= dns_types__qname_ptr_range__last .
H8:    fld_messageid(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H9:    fld_messageid(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H10:   fld_opcode(fld_header(output_packet)) >= 
           dns_types__opcode_type__first .
H11:   fld_opcode(fld_header(output_packet)) <= 
           dns_types__opcode_type__last .
H12:   fld_rcode(fld_header(output_packet)) >= 
           dns_types__response_code__first .
H13:   fld_rcode(fld_header(output_packet)) <= 
           dns_types__response_code__last .
H14:   fld_qdcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H15:   fld_qdcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H16:   fld_ancount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H17:   fld_ancount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H18:   fld_nscount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H19:   fld_nscount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H20:   fld_arcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H21:   fld_arcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H22:   for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           fld_bytes(output_packet), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           output_packet), [i___1]) <= dns_types__byte__last))) .
H23:   answer_count >= dns_types__unsigned_short__first .
H24:   answer_count <= dns_types__unsigned_short__last .
H25:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_ttlinseconds(fld_inherit(element(returnedarecords__1, [
           i___1]))) >= unsigned_types__unsigned32__first) and (
           fld_ttlinseconds(fld_inherit(element(returnedarecords__1, [
           i___1]))) <= unsigned_types__unsigned32__last))) .
H26:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_class(fld_inherit(element(returnedarecords__1, [
           i___1]))) >= rr_type__classtype__first) and (fld_class(
           fld_inherit(element(returnedarecords__1, [i___1]))) <= 
           rr_type__classtype__last))) .
H27:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_ipv4(element(returnedarecords__1, [i___1])) >= 
           unsigned_types__unsigned32__first) and (fld_ipv4(element(
           returnedarecords__1, [i___1])) <= 
           unsigned_types__unsigned32__last))) .
H28:   numfound__1 >= rr_type__numberofrecordstype__first .
H29:   numfound__1 <= rr_type__numberofrecordstype__last .
H30:   numfound__1 >= natural__first .
H31:   numfound__1 <= natural__last .
H32:   start_byte >= dns_types__packet_bytes_range__first .
H33:   start_byte <= dns_types__packet_bytes_range__last .
H34:   numfound__1 >= natural__first .
H35:   numfound__1 <= natural__last .
H36:   not (numfound__1 >= 1) .
H37:   start_byte >= dns_types__packet_bytes_range__first .
H38:   start_byte <= dns_types__packet_bytes_range__last .
H39:   start_byte + dns_types__header_bits div 8 >= 
           dns_types__packet_length_range__first .
H40:   start_byte + dns_types__header_bits div 8 <= 
           dns_types__packet_length_range__last .
H41:   start_byte + dns_types__header_bits div 8 >= 
           dns_types__packet_length_range__first .
H42:   start_byte + dns_types__header_bits div 8 <= 
           dns_types__packet_length_range__last .
H43:   start_byte + dns_types__header_bits div 8 >= 
           dns_types__packet_bytes_range__base__first .
H44:   start_byte + dns_types__header_bits div 8 <= 
           dns_types__packet_bytes_range__base__last .
H45:   dns_types__header_bits div 8 >= 
           dns_types__packet_bytes_range__first .
H46:   dns_types__header_bits div 8 <= 
           dns_types__packet_bytes_range__last .
H47:   dns_types__header_bits div 8 >= system__min_int .
H48:   dns_types__header_bits div 8 <= system__max_int .
H49:   8 <> 0 .
H50:   numfound__1 >= natural__first .
H51:   numfound__1 <= natural__last .
H52:   answer_count + numfound__1 >= 
           dns_types__unsigned_short__first .
H53:   answer_count + numfound__1 <= 
           dns_types__unsigned_short__last .
H54:   numfound__1 >= dns_types__unsigned_short__first .
H55:   numfound__1 <= dns_types__unsigned_short__last .
        ->
C1:    start_byte + dns_types__header_bits div 8 >= 
           dns_types__header_bits div 8 + 1 .
C2:    start_byte + dns_types__header_bits div 8 <= 
           dns_types__packet_size .
C3:    answer_count + numfound__1 <= answer_count + 
           rr_type__maxnumrecords .
 

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

procedure_create_response_a_24.
H1:    response_counter >= 1 .
H2:    response_counter <= numfound .
H3:    start_byte <= dns_types__packet_size .
H4:    answer_count = answer_count~ .
H5:    answer_count <= dns_types__unsigned_short__last - 
           rr_type__maxnumrecords .
H6:    current_byte = start_byte + 16 * (response_counter - 1) .
H7:    current_byte < dns_types__packet_size - (16 + 
           dns_types__header_bits div 8) .
H8:    numfound <= rr_type__maxnumrecords .
H9:    start_byte >= dns_types__packet_bytes_range__first .
H10:   start_byte <= dns_types__packet_bytes_range__last .
H11:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           domainname, [i___1]) >= character__first) and (element(
           domainname, [i___1]) <= character__last))) .
H12:   qname_location >= dns_types__qname_ptr_range__first .
H13:   qname_location <= dns_types__qname_ptr_range__last .
H14:   fld_messageid(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H15:   fld_messageid(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H16:   fld_opcode(fld_header(output_packet)) >= 
           dns_types__opcode_type__first .
H17:   fld_opcode(fld_header(output_packet)) <= 
           dns_types__opcode_type__last .
H18:   fld_rcode(fld_header(output_packet)) >= 
           dns_types__response_code__first .
H19:   fld_rcode(fld_header(output_packet)) <= 
           dns_types__response_code__last .
H20:   fld_qdcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H21:   fld_qdcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H22:   fld_ancount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H23:   fld_ancount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H24:   fld_nscount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H25:   fld_nscount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H26:   fld_arcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H27:   fld_arcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H28:   for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           fld_bytes(output_packet), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           output_packet), [i___1]) <= dns_types__byte__last))) .
H29:   answer_count >= dns_types__unsigned_short__first .
H30:   answer_count <= dns_types__unsigned_short__last .
H31:   answer_count~ <= dns_types__unsigned_short__last - 
           rr_type__maxnumrecords .
H32:   start_byte <= dns_types__packet_size .
H33:   current_byte >= dns_types__packet_bytes_range__first .
H34:   current_byte <= dns_types__packet_bytes_range__last .
H35:   (qname_location + 49152) mod 
           unsigned_types__unsigned16__modulus >= 
           unsigned_types__unsigned16__first .
H36:   (qname_location + 49152) mod 
           unsigned_types__unsigned16__modulus <= 
           unsigned_types__unsigned16__last .
H37:   current_byte + 1 >= dns_types__packet_bytes_range__first .
H38:   current_byte + 1 <= dns_types__packet_bytes_range__last .
H39:   current_byte + 1 <= dns_types__packet_bytes_range__last - 1 .
H40:   qname_location >= unsigned_types__unsigned16__first .
H41:   qname_location <= unsigned_types__unsigned16__last .
H42:   current_byte + 1 >= dns_types__packet_bytes_range__base__first .
H43:   current_byte + 1 <= dns_types__packet_bytes_range__base__last .
H44:   for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           fld_bytes(output_packet__2), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           output_packet__2), [i___1]) <= dns_types__byte__last))) .
H45:   fld_header(output_packet__2) = fld_header(
           output_packet) .
H46:   output_packet__2 = upf_bytes(output_packet, fld_bytes(
           output_packet__2)) .
H47:   0 >= dns_types__byte__first .
H48:   0 <= dns_types__byte__last .
H49:   current_byte + 3 >= dns_types__packet_bytes_range__first .
H50:   current_byte + 3 <= dns_types__packet_bytes_range__last .
H51:   current_byte + 3 >= dns_types__packet_bytes_range__base__first .
H52:   current_byte + 3 <= dns_types__packet_bytes_range__base__last .
H53:   1 >= dns_types__byte__first .
H54:   1 <= dns_types__byte__last .
H55:   current_byte + 4 >= dns_types__packet_bytes_range__first .
H56:   current_byte + 4 <= dns_types__packet_bytes_range__last .
H57:   current_byte + 4 >= dns_types__packet_bytes_range__base__first .
H58:   current_byte + 4 <= dns_types__packet_bytes_range__base__last .
H59:   0 >= dns_types__byte__first .
H60:   0 <= dns_types__byte__last .
H61:   current_byte + 5 >= dns_types__packet_bytes_range__first .
H62:   current_byte + 5 <= dns_types__packet_bytes_range__last .
H63:   current_byte + 5 >= dns_types__packet_bytes_range__base__first .
H64:   current_byte + 5 <= dns_types__packet_bytes_range__base__last .
H65:   1 >= dns_types__byte__first .
H66:   1 <= dns_types__byte__last .
H67:   current_byte + 6 >= dns_types__packet_bytes_range__first .
H68:   current_byte + 6 <= dns_types__packet_bytes_range__last .
H69:   current_byte + 6 >= dns_types__packet_bytes_range__base__first .
H70:   current_byte + 6 <= dns_types__packet_bytes_range__base__last .
H71:   current_byte >= dns_types__packet_bytes_range__first .
H72:   current_byte <= dns_types__packet_bytes_range__last .
H73:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_ttlinseconds(fld_inherit(element(
           returnedarecords, [i___1]))) >= 
           unsigned_types__unsigned32__first) and (fld_ttlinseconds(
           fld_inherit(element(returnedarecords, [i___1]))) <= 
           unsigned_types__unsigned32__last))) .
H74:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_class(fld_inherit(element(returnedarecords, [
           i___1]))) >= rr_type__classtype__first) and (fld_class(
           fld_inherit(element(returnedarecords, [i___1]))) <= 
           rr_type__classtype__last))) .
H75:   for_all(i___1: integer, ((i___1 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___1 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_ipv4(element(returnedarecords, [i___1])) >= 
           unsigned_types__unsigned32__first) and (fld_ipv4(element(
           returnedarecords, [i___1])) <= 
           unsigned_types__unsigned32__last))) .
H76:   response_counter >= natural__first .
H77:   response_counter <= natural__last .
H78:   current_byte + 7 >= dns_types__packet_bytes_range__first .
H79:   current_byte + 7 <= dns_types__packet_bytes_range__last .
H80:   current_byte + 7 <= dns_types__packet_bytes_range__last - 10 .
H81:   rr_type__returnedrecordsindextype__first + (
           response_counter - 1) >= 
           rr_type__returnedrecordsindextype__first .
H82:   rr_type__returnedrecordsindextype__first + (
           response_counter - 1) <= 
           rr_type__returnedrecordsindextype__last .
H83:   rr_type__returnedrecordsindextype__first + (
           response_counter - 1) >= integer__base__first .
H84:   rr_type__returnedrecordsindextype__first + (
           response_counter - 1) <= integer__base__last .
H85:   response_counter - 1 >= integer__base__first .
H86:   response_counter - 1 <= integer__base__last .
H87:   current_byte + 7 >= dns_types__packet_bytes_range__base__first .
H88:   current_byte + 7 <= dns_types__packet_bytes_range__base__last .
H89:   for_all(i___1: dns_types__packet_bytes_range, ((
           i___1 >= dns_types__packet_bytes_range__first) and (
           i___1 <= dns_types__packet_bytes_range__last)) -> ((element(
           fld_bytes(output_packet__3), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           output_packet__3), [i___1]) <= dns_types__byte__last))) .
H90:   fld_header(output_packet__3) = fld_header(upf_bytes(upf_bytes(
           upf_bytes(upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0)), update(fld_bytes(
           upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0))), [
           current_byte + 4], 1)), update(fld_bytes(upf_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0)), update(fld_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0))), [current_byte + 4], 1))), [
           current_byte + 5], 0)), update(fld_bytes(upf_bytes(upf_bytes(
           upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0)), update(fld_bytes(
           upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0))), [
           current_byte + 4], 1)), update(fld_bytes(upf_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0)), update(fld_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0))), [current_byte + 4], 1))), [
           current_byte + 5], 0))), [current_byte + 6], 1))) .
H91:   output_packet__3 = upf_bytes(upf_bytes(upf_bytes(upf_bytes(
           upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0)), update(fld_bytes(
           upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0))), [
           current_byte + 4], 1)), update(fld_bytes(upf_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0)), update(fld_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0))), [current_byte + 4], 1))), [
           current_byte + 5], 0)), update(fld_bytes(upf_bytes(upf_bytes(
           upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0)), update(fld_bytes(
           upf_bytes(output_packet__2, update(fld_bytes(
           output_packet__2), [current_byte + 3], 0))), [
           current_byte + 4], 1)), update(fld_bytes(upf_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0)), update(fld_bytes(upf_bytes(
           output_packet__2, update(fld_bytes(output_packet__2), [
           current_byte + 3], 0))), [current_byte + 4], 1))), [
           current_byte + 5], 0))), [current_byte + 6], 1)), fld_bytes(
           output_packet__3)) .
H92:   response_counter >= natural__first .
H93:   response_counter <= natural__last .
H94:   response_counter + 1 >= natural__first .
H95:   response_counter + 1 <= natural__last .
H96:   current_byte >= dns_types__packet_bytes_range__first .
H97:   current_byte <= dns_types__packet_bytes_range__last .
H98:   current_byte + 16 >= dns_types__packet_bytes_range__first .
H99:   current_byte + 16 <= dns_types__packet_bytes_range__last .
H100:  current_byte + 16 >= dns_types__packet_bytes_range__first .
H101:  current_byte + 16 <= dns_types__packet_bytes_range__last .
H102:  numfound >= natural__first .
H103:  numfound <= natural__last .
H104:  response_counter + 1 >= natural__first .
H105:  response_counter + 1 <= natural__last .
H106:  dns_types__packet_size - (16 + dns_types__header_bits div 8) >= system__min_int .
H107:  dns_types__packet_size - (16 + dns_types__header_bits div 8) <= system__max_int .
H108:  16 + dns_types__header_bits div 8 >= system__min_int .
H109:  16 + dns_types__header_bits div 8 <= system__max_int .
H110:  dns_types__header_bits div 8 >= system__min_int .
H111:  dns_types__header_bits div 8 <= system__max_int .
H112:  8 <> 0 .
H113:  current_byte + 16 >= integer__first .
H114:  current_byte + 16 <= integer__last .
H115:  not ((response_counter + 1 <= numfound) and (
           current_byte + 16 < dns_types__packet_size - (16 + 
           dns_types__header_bits div 8))) .
H116:  current_byte + 16 >= dns_types__packet_bytes_range__first .
H117:  current_byte + 16 <= dns_types__packet_bytes_range__last .
H118:  current_byte + 16 + dns_types__header_bits div 8 >= 
           dns_types__packet_length_range__first .
H119:  current_byte + 16 + dns_types__header_bits div 8 <= 
           dns_types__packet_length_range__last .
H120:  current_byte + 16 + dns_types__header_bits div 8 >= 
           dns_types__packet_length_range__first .
H121:  current_byte + 16 + dns_types__header_bits div 8 <= 
           dns_types__packet_length_range__last .
H122:  current_byte + 16 + dns_types__header_bits div 8 >= 
           dns_types__packet_bytes_range__base__first .
H123:  current_byte + 16 + dns_types__header_bits div 8 <= 
           dns_types__packet_bytes_range__base__last .
H124:  dns_types__header_bits div 8 >= 
           dns_types__packet_bytes_range__first .
H125:  dns_types__header_bits div 8 <= 
           dns_types__packet_bytes_range__last .
H126:  dns_types__header_bits div 8 >= system__min_int .
H127:  dns_types__header_bits div 8 <= system__max_int .
H128:  8 <> 0 .
H129:  numfound >= natural__first .
H130:  numfound <= natural__last .
H131:  answer_count + numfound >= dns_types__unsigned_short__first .
H132:  answer_count + numfound <= dns_types__unsigned_short__last .
H133:  numfound >= dns_types__unsigned_short__first .
H134:  numfound <= dns_types__unsigned_short__last .
        ->
C1:    current_byte + 16 + dns_types__header_bits div 8 >= 
           dns_types__header_bits div 8 + 1 .
C2:    current_byte + 16 + dns_types__header_bits div 8 <= 
           dns_types__packet_size .
C3:    answer_count + numfound <= answer_count~ + 
           rr_type__maxnumrecords .
 

