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

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


           procedure Process_Dns_Request.Create_NXDOMAIN_Response




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

procedure_create_nxdomain_response_1.
H1:    start_byte <= dns_types__packet_size .
H2:    start_byte >= dns_types__packet_bytes_range__first .
H3:    start_byte <= dns_types__packet_bytes_range__last .
H4:    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))) .
H5:    qname_location >= dns_types__qname_ptr_range__first .
H6:    qname_location <= dns_types__qname_ptr_range__last .
H7:    fld_messageid(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H8:    fld_messageid(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H9:    fld_opcode(fld_header(output_packet)) >= 
           dns_types__opcode_type__first .
H10:   fld_opcode(fld_header(output_packet)) <= 
           dns_types__opcode_type__last .
H11:   fld_rcode(fld_header(output_packet)) >= 
           dns_types__response_code__first .
H12:   fld_rcode(fld_header(output_packet)) <= 
           dns_types__response_code__last .
H13:   fld_qdcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H14:   fld_qdcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H15:   fld_ancount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H16:   fld_ancount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H17:   fld_nscount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H18:   fld_nscount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H19:   fld_arcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H20:   fld_arcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H21:   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))) .
        ->
C1:    qname_location >= dns_types__qname_ptr_range__first .
C2:    qname_location <= dns_types__qname_ptr_range__last .
 

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

procedure_create_nxdomain_response_2.
H1:    start_byte <= dns_types__packet_size .
H2:    start_byte >= dns_types__packet_bytes_range__first .
H3:    start_byte <= dns_types__packet_bytes_range__last .
H4:    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))) .
H5:    qname_location >= dns_types__qname_ptr_range__first .
H6:    qname_location <= dns_types__qname_ptr_range__last .
H7:    fld_messageid(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H8:    fld_messageid(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H9:    fld_opcode(fld_header(output_packet)) >= 
           dns_types__opcode_type__first .
H10:   fld_opcode(fld_header(output_packet)) <= 
           dns_types__opcode_type__last .
H11:   fld_rcode(fld_header(output_packet)) >= 
           dns_types__response_code__first .
H12:   fld_rcode(fld_header(output_packet)) <= 
           dns_types__response_code__last .
H13:   fld_qdcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H14:   fld_qdcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H15:   fld_ancount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H16:   fld_ancount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H17:   fld_nscount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H18:   fld_nscount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H19:   fld_arcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H20:   fld_arcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H21:   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))) .
H22:   qname_location >= dns_types__qname_ptr_range__first .
H23:   qname_location <= dns_types__qname_ptr_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 start to run-time check associated with statement of line 1056:

procedure_create_nxdomain_response_3.
H1:    start_byte <= dns_types__packet_size .
H2:    start_byte >= dns_types__packet_bytes_range__first .
H3:    start_byte <= dns_types__packet_bytes_range__last .
H4:    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))) .
H5:    qname_location >= dns_types__qname_ptr_range__first .
H6:    qname_location <= dns_types__qname_ptr_range__last .
H7:    fld_messageid(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H8:    fld_messageid(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H9:    fld_opcode(fld_header(output_packet)) >= 
           dns_types__opcode_type__first .
H10:   fld_opcode(fld_header(output_packet)) <= 
           dns_types__opcode_type__last .
H11:   fld_rcode(fld_header(output_packet)) >= 
           dns_types__response_code__first .
H12:   fld_rcode(fld_header(output_packet)) <= 
           dns_types__response_code__last .
H13:   fld_qdcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H14:   fld_qdcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H15:   fld_ancount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H16:   fld_ancount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H17:   fld_nscount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H18:   fld_nscount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H19:   fld_arcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H20:   fld_arcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H21:   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))) .
H22:   qname_location >= dns_types__qname_ptr_range__first .
H23:   qname_location <= dns_types__qname_ptr_range__last .
H24:   start_byte + dns_types__header_bits div 8 >= 
           dns_types__packet_length_range__first .
H25:   start_byte + dns_types__header_bits div 8 <= 
           dns_types__packet_length_range__last .
H26:   start_byte + dns_types__header_bits div 8 >= 
           dns_types__packet_length_range__first .
H27:   start_byte + dns_types__header_bits div 8 <= 
           dns_types__packet_length_range__last .
H28:   start_byte + dns_types__header_bits div 8 >= 
           dns_types__packet_bytes_range__base__first .
H29:   start_byte + dns_types__header_bits div 8 <= 
           dns_types__packet_bytes_range__base__last .
H30:   dns_types__header_bits div 8 >= 
           dns_types__packet_bytes_range__first .
H31:   dns_types__header_bits div 8 <= 
           dns_types__packet_bytes_range__last .
H32:   dns_types__header_bits div 8 >= system__min_int .
H33:   dns_types__header_bits div 8 <= system__max_int .
H34:   8 <> 0 .
        ->
C1:    dns_types__name_error >= dns_types__response_code__first .
C2:    dns_types__name_error <= dns_types__response_code__last .
 

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

procedure_create_nxdomain_response_4.
H1:    start_byte <= dns_types__packet_size .
H2:    start_byte >= dns_types__packet_bytes_range__first .
H3:    start_byte <= dns_types__packet_bytes_range__last .
H4:    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))) .
H5:    qname_location >= dns_types__qname_ptr_range__first .
H6:    qname_location <= dns_types__qname_ptr_range__last .
H7:    fld_messageid(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H8:    fld_messageid(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H9:    fld_opcode(fld_header(output_packet)) >= 
           dns_types__opcode_type__first .
H10:   fld_opcode(fld_header(output_packet)) <= 
           dns_types__opcode_type__last .
H11:   fld_rcode(fld_header(output_packet)) >= 
           dns_types__response_code__first .
H12:   fld_rcode(fld_header(output_packet)) <= 
           dns_types__response_code__last .
H13:   fld_qdcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H14:   fld_qdcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H15:   fld_ancount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H16:   fld_ancount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H17:   fld_nscount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H18:   fld_nscount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H19:   fld_arcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H20:   fld_arcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H21:   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))) .
H22:   qname_location >= dns_types__qname_ptr_range__first .
H23:   qname_location <= dns_types__qname_ptr_range__last .
H24:   start_byte + dns_types__header_bits div 8 >= 
           dns_types__packet_length_range__first .
H25:   start_byte + dns_types__header_bits div 8 <= 
           dns_types__packet_length_range__last .
H26:   start_byte + dns_types__header_bits div 8 >= 
           dns_types__packet_length_range__first .
H27:   start_byte + dns_types__header_bits div 8 <= 
           dns_types__packet_length_range__last .
H28:   start_byte + dns_types__header_bits div 8 >= 
           dns_types__packet_bytes_range__base__first .
H29:   start_byte + dns_types__header_bits div 8 <= 
           dns_types__packet_bytes_range__base__last .
H30:   dns_types__header_bits div 8 >= 
           dns_types__packet_bytes_range__first .
H31:   dns_types__header_bits div 8 <= 
           dns_types__packet_bytes_range__last .
H32:   dns_types__header_bits div 8 >= system__min_int .
H33:   dns_types__header_bits div 8 <= system__max_int .
H34:   8 <> 0 .
H35:   dns_types__name_error >= dns_types__response_code__first .
H36:   dns_types__name_error <= dns_types__response_code__last .
        ->
C1:    0 >= dns_types__unsigned_short__first .
C2:    0 <= dns_types__unsigned_short__last .
 

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

procedure_create_nxdomain_response_5.
H1:    start_byte <= dns_types__packet_size .
H2:    start_byte >= dns_types__packet_bytes_range__first .
H3:    start_byte <= dns_types__packet_bytes_range__last .
H4:    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))) .
H5:    qname_location >= dns_types__qname_ptr_range__first .
H6:    qname_location <= dns_types__qname_ptr_range__last .
H7:    fld_messageid(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H8:    fld_messageid(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H9:    fld_opcode(fld_header(output_packet)) >= 
           dns_types__opcode_type__first .
H10:   fld_opcode(fld_header(output_packet)) <= 
           dns_types__opcode_type__last .
H11:   fld_rcode(fld_header(output_packet)) >= 
           dns_types__response_code__first .
H12:   fld_rcode(fld_header(output_packet)) <= 
           dns_types__response_code__last .
H13:   fld_qdcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H14:   fld_qdcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H15:   fld_ancount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H16:   fld_ancount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H17:   fld_nscount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H18:   fld_nscount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H19:   fld_arcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H20:   fld_arcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H21:   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))) .
H22:   qname_location >= dns_types__qname_ptr_range__first .
H23:   qname_location <= dns_types__qname_ptr_range__last .
H24:   start_byte + dns_types__header_bits div 8 >= 
           dns_types__packet_length_range__first .
H25:   start_byte + dns_types__header_bits div 8 <= 
           dns_types__packet_length_range__last .
H26:   start_byte + dns_types__header_bits div 8 >= 
           dns_types__packet_length_range__first .
H27:   start_byte + dns_types__header_bits div 8 <= 
           dns_types__packet_length_range__last .
H28:   start_byte + dns_types__header_bits div 8 >= 
           dns_types__packet_bytes_range__base__first .
H29:   start_byte + dns_types__header_bits div 8 <= 
           dns_types__packet_bytes_range__base__last .
H30:   dns_types__header_bits div 8 >= 
           dns_types__packet_bytes_range__first .
H31:   dns_types__header_bits div 8 <= 
           dns_types__packet_bytes_range__last .
H32:   dns_types__header_bits div 8 >= system__min_int .
H33:   dns_types__header_bits div 8 <= system__max_int .
H34:   8 <> 0 .
H35:   dns_types__name_error >= dns_types__response_code__first .
H36:   dns_types__name_error <= dns_types__response_code__last .
H37:   0 >= dns_types__unsigned_short__first .
H38:   0 <= dns_types__unsigned_short__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:   0 >= dns_types__unsigned_short__first .
H42:   0 <= dns_types__unsigned_short__last .
H43:   0 >= natural__first .
H44:   0 <= natural__last .
H45:   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))) .
H46:   qname_location >= dns_types__qname_ptr_range__first .
H47:   qname_location <= dns_types__qname_ptr_range__last .
        ->
C1:    start_byte + dns_types__header_bits div 8 >= 
           dns_types__qname_ptr_range__first .
C2:    start_byte + dns_types__header_bits div 8 <= 
           dns_types__qname_ptr_range__last .
C3:    element(domainname, [rr_type__wirestringtypeindex__first]) >= 
           natural__first .
C4:    element(domainname, [rr_type__wirestringtypeindex__first]) <= 
           natural__last .
C5:    rr_type__wirestringtypeindex__first >= 
           rr_type__wirestringtypeindex__first .
C6:    rr_type__wirestringtypeindex__first <= 
           rr_type__wirestringtypeindex__last .
 

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

procedure_create_nxdomain_response_6.
H1:    answer_count = 0 .
H2:    amount_trimmed >= 0 .
H3:    amount_trimmed < rr_type__wirestringtypeindex__last .
H4:    output_bytes <= dns_types__packet_length_range__last .
H5:    current_qname_location <= output_bytes .
H6:    start_byte >= dns_types__packet_bytes_range__first .
H7:    start_byte <= dns_types__packet_bytes_range__last .
H8:    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))) .
H9:    qname_location >= dns_types__qname_ptr_range__first .
H10:   qname_location <= dns_types__qname_ptr_range__last .
H11:   fld_messageid(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H12:   fld_messageid(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H13:   fld_opcode(fld_header(output_packet)) >= 
           dns_types__opcode_type__first .
H14:   fld_opcode(fld_header(output_packet)) <= 
           dns_types__opcode_type__last .
H15:   fld_rcode(fld_header(output_packet)) >= 
           dns_types__response_code__first .
H16:   fld_rcode(fld_header(output_packet)) <= 
           dns_types__response_code__last .
H17:   fld_qdcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H18:   fld_qdcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H19:   fld_ancount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H20:   fld_ancount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H21:   fld_nscount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H22:   fld_nscount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H23:   fld_arcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H24:   fld_arcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H25:   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))) .
H26:   start_byte <= dns_types__packet_size .
H27:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           current_name, [i___1]) >= character__first) and (element(
           current_name, [i___1]) <= character__last))) .
H28:   current_qname_location >= dns_types__qname_ptr_range__first .
H29:   current_qname_location <= dns_types__qname_ptr_range__last .
H30:   current_qname_location >= dns_types__qname_ptr_range__first .
H31:   current_qname_location <= dns_types__qname_ptr_range__last .
H32:   current_qname_location <= 
           dns_types__packet_length_range__last .
H33:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           trimmed_name__1, [i___1]) >= character__first) and (element(
           trimmed_name__1, [i___1]) <= character__last))) .
H34:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H35:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
H36:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H37:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
H38:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           trimmed_name__1, [i___1]) >= character__first) and (element(
           trimmed_name__1, [i___1]) <= character__last))) .
H39:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H40:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
H41:   answer_count >= dns_types__unsigned_short__first .
H42:   answer_count <= dns_types__unsigned_short__last .
H43:   answer_count >= dns_types__unsigned_short__first .
H44:   answer_count <= dns_types__unsigned_short__last .
H45:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H46:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
H47:   start_byte >= dns_types__packet_bytes_range__first .
H48:   start_byte <= dns_types__packet_bytes_range__last .
H49:   start_byte <= dns_types__packet_size .
H50:   answer_count <= dns_types__unsigned_short__last - 
           rr_type__maxnumrecords .
H51:   output_bytes__2 >= dns_types__header_bits div 8 + 1 .
H52:   output_bytes__2 <= dns_types__packet_size .
H53:   answer_count__2 <= answer_count + 
           rr_type__maxnumrecords .
H54:   fld_messageid(fld_header(output_packet__2)) >= 
           dns_types__unsigned_short__first .
H55:   fld_messageid(fld_header(output_packet__2)) <= 
           dns_types__unsigned_short__last .
H56:   fld_opcode(fld_header(output_packet__2)) >= 
           dns_types__opcode_type__first .
H57:   fld_opcode(fld_header(output_packet__2)) <= 
           dns_types__opcode_type__last .
H58:   fld_rcode(fld_header(output_packet__2)) >= 
           dns_types__response_code__first .
H59:   fld_rcode(fld_header(output_packet__2)) <= 
           dns_types__response_code__last .
H60:   fld_qdcount(fld_header(output_packet__2)) >= 
           dns_types__unsigned_short__first .
H61:   fld_qdcount(fld_header(output_packet__2)) <= 
           dns_types__unsigned_short__last .
H62:   fld_ancount(fld_header(output_packet__2)) >= 
           dns_types__unsigned_short__first .
H63:   fld_ancount(fld_header(output_packet__2)) <= 
           dns_types__unsigned_short__last .
H64:   fld_nscount(fld_header(output_packet__2)) >= 
           dns_types__unsigned_short__first .
H65:   fld_nscount(fld_header(output_packet__2)) <= 
           dns_types__unsigned_short__last .
H66:   fld_arcount(fld_header(output_packet__2)) >= 
           dns_types__unsigned_short__first .
H67:   fld_arcount(fld_header(output_packet__2)) <= 
           dns_types__unsigned_short__last .
H68:   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))) .
H69:   answer_count__2 >= dns_types__unsigned_short__first .
H70:   answer_count__2 <= dns_types__unsigned_short__last .
H71:   output_bytes__2 >= dns_types__packet_length_range__first .
H72:   output_bytes__2 <= dns_types__packet_length_range__last .
H73:   output_bytes__2 >= dns_types__packet_length_range__first .
H74:   output_bytes__2 <= dns_types__packet_length_range__last .
H75:   answer_count__2 >= dns_types__unsigned_short__first .
H76:   answer_count__2 <= dns_types__unsigned_short__last .
H77:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           trimmed_name__1, [i___1]) >= character__first) and (element(
           trimmed_name__1, [i___1]) <= character__last))) .
H78:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H79:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
H80:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H81:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
H82:   amount_trimmed >= natural__first .
H83:   amount_trimmed <= natural__last .
H84:   amount_trimmed + (element(domainname, [
           rr_type__wirestringtypeindex__first]) + 1) >= 
           natural__first .
H85:   amount_trimmed + (element(domainname, [
           rr_type__wirestringtypeindex__first]) + 1) <= 
           natural__last .
H86:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= 
           natural__first .
H87:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= 
           natural__last .
H88:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= system__min_int .
H89:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= system__max_int .
H90:   rr_type__wirestringtypeindex__first >= 
           rr_type__wirestringtypeindex__first .
H91:   rr_type__wirestringtypeindex__first <= 
           rr_type__wirestringtypeindex__last .
H92:   output_bytes__2 >= dns_types__packet_length_range__first .
H93:   output_bytes__2 <= dns_types__packet_length_range__last .
H94:   answer_count__2 >= dns_types__unsigned_short__first .
H95:   answer_count__2 <= dns_types__unsigned_short__last .
H96:   amount_trimmed + (element(domainname, [
           rr_type__wirestringtypeindex__first]) + 1) >= 
           natural__first .
H97:   amount_trimmed + (element(domainname, [
           rr_type__wirestringtypeindex__first]) + 1) <= 
           natural__last .
H98:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           trimmed_name__1, [i___1]) >= character__first) and (element(
           trimmed_name__1, [i___1]) <= character__last))) .
H99:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H100:  new_qname_location__1 <= dns_types__qname_ptr_range__last .
        ->
C1:    output_bytes__2 >= dns_types__qname_ptr_range__first .
C2:    output_bytes__2 <= dns_types__qname_ptr_range__last .
C3:    element(trimmed_name__1, [rr_type__wirestringtypeindex__first]) >= 
           natural__first .
C4:    element(trimmed_name__1, [rr_type__wirestringtypeindex__first]) <= 
           natural__last .
C5:    rr_type__wirestringtypeindex__first >= 
           rr_type__wirestringtypeindex__first .
C6:    rr_type__wirestringtypeindex__first <= 
           rr_type__wirestringtypeindex__last .
 

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

procedure_create_nxdomain_response_7.
H1:    start_byte <= dns_types__packet_size .
H2:    start_byte >= dns_types__packet_bytes_range__first .
H3:    start_byte <= dns_types__packet_bytes_range__last .
H4:    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))) .
H5:    qname_location >= dns_types__qname_ptr_range__first .
H6:    qname_location <= dns_types__qname_ptr_range__last .
H7:    fld_messageid(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H8:    fld_messageid(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H9:    fld_opcode(fld_header(output_packet)) >= 
           dns_types__opcode_type__first .
H10:   fld_opcode(fld_header(output_packet)) <= 
           dns_types__opcode_type__last .
H11:   fld_rcode(fld_header(output_packet)) >= 
           dns_types__response_code__first .
H12:   fld_rcode(fld_header(output_packet)) <= 
           dns_types__response_code__last .
H13:   fld_qdcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H14:   fld_qdcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H15:   fld_ancount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H16:   fld_ancount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H17:   fld_nscount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H18:   fld_nscount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H19:   fld_arcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H20:   fld_arcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H21:   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))) .
H22:   qname_location >= dns_types__qname_ptr_range__first .
H23:   qname_location <= dns_types__qname_ptr_range__last .
H24:   start_byte + dns_types__header_bits div 8 >= 
           dns_types__packet_length_range__first .
H25:   start_byte + dns_types__header_bits div 8 <= 
           dns_types__packet_length_range__last .
H26:   start_byte + dns_types__header_bits div 8 >= 
           dns_types__packet_length_range__first .
H27:   start_byte + dns_types__header_bits div 8 <= 
           dns_types__packet_length_range__last .
H28:   start_byte + dns_types__header_bits div 8 >= 
           dns_types__packet_bytes_range__base__first .
H29:   start_byte + dns_types__header_bits div 8 <= 
           dns_types__packet_bytes_range__base__last .
H30:   dns_types__header_bits div 8 >= 
           dns_types__packet_bytes_range__first .
H31:   dns_types__header_bits div 8 <= 
           dns_types__packet_bytes_range__last .
H32:   dns_types__header_bits div 8 >= system__min_int .
H33:   dns_types__header_bits div 8 <= system__max_int .
H34:   8 <> 0 .
H35:   dns_types__name_error >= dns_types__response_code__first .
H36:   dns_types__name_error <= dns_types__response_code__last .
H37:   0 >= dns_types__unsigned_short__first .
H38:   0 <= dns_types__unsigned_short__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:   0 >= dns_types__unsigned_short__first .
H42:   0 <= dns_types__unsigned_short__last .
H43:   0 >= natural__first .
H44:   0 <= natural__last .
H45:   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))) .
H46:   qname_location >= dns_types__qname_ptr_range__first .
H47:   qname_location <= dns_types__qname_ptr_range__last .
H48:   start_byte + dns_types__header_bits div 8 >= 
           dns_types__qname_ptr_range__first .
H49:   start_byte + dns_types__header_bits div 8 <= 
           dns_types__qname_ptr_range__last .
H50:   element(domainname, [rr_type__wirestringtypeindex__first]) >= 
           natural__first .
H51:   element(domainname, [rr_type__wirestringtypeindex__first]) <= 
           natural__last .
H52:   rr_type__wirestringtypeindex__first >= 
           rr_type__wirestringtypeindex__first .
H53:   rr_type__wirestringtypeindex__first <= 
           rr_type__wirestringtypeindex__last .
H54:   0 = 0 .
H55:   0 < rr_type__wirestringtypeindex__last .
H56:   element(domainname, [rr_type__wirestringtypeindex__first]) <> 0 .
H57:   qname_location <= start_byte + dns_types__header_bits div 8 .
        ->
C1:    0 = 0 .
C2:    0 >= 0 .
C3:    0 < rr_type__wirestringtypeindex__last .
C4:    start_byte + dns_types__header_bits div 8 <= 
           dns_types__packet_length_range__last .
C5:    qname_location <= start_byte + dns_types__header_bits div 8 .
C6:    start_byte >= dns_types__packet_bytes_range__first .
C7:    start_byte <= dns_types__packet_bytes_range__last .
C8:    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))) .
C9:    qname_location >= dns_types__qname_ptr_range__first .
C10:   qname_location <= dns_types__qname_ptr_range__last .
C11:   fld_messageid(fld_header(upf_header(upf_header(
           output_packet, upf_rcode(fld_header(
           output_packet), dns_types__name_error)), upf_ancount(
           fld_header(upf_header(output_packet, upf_rcode(fld_header(
           output_packet), dns_types__name_error))), 0)))) >= 
           dns_types__unsigned_short__first .
C12:   fld_messageid(fld_header(upf_header(upf_header(
           output_packet, upf_rcode(fld_header(
           output_packet), dns_types__name_error)), upf_ancount(
           fld_header(upf_header(output_packet, upf_rcode(fld_header(
           output_packet), dns_types__name_error))), 0)))) <= 
           dns_types__unsigned_short__last .
C13:   fld_opcode(fld_header(upf_header(upf_header(
           output_packet, upf_rcode(fld_header(
           output_packet), dns_types__name_error)), upf_ancount(
           fld_header(upf_header(output_packet, upf_rcode(fld_header(
           output_packet), dns_types__name_error))), 0)))) >= 
           dns_types__opcode_type__first .
C14:   fld_opcode(fld_header(upf_header(upf_header(
           output_packet, upf_rcode(fld_header(
           output_packet), dns_types__name_error)), upf_ancount(
           fld_header(upf_header(output_packet, upf_rcode(fld_header(
           output_packet), dns_types__name_error))), 0)))) <= 
           dns_types__opcode_type__last .
C15:   fld_rcode(fld_header(upf_header(upf_header(
           output_packet, upf_rcode(fld_header(
           output_packet), dns_types__name_error)), upf_ancount(
           fld_header(upf_header(output_packet, upf_rcode(fld_header(
           output_packet), dns_types__name_error))), 0)))) >= 
           dns_types__response_code__first .
C16:   fld_rcode(fld_header(upf_header(upf_header(
           output_packet, upf_rcode(fld_header(
           output_packet), dns_types__name_error)), upf_ancount(
           fld_header(upf_header(output_packet, upf_rcode(fld_header(
           output_packet), dns_types__name_error))), 0)))) <= 
           dns_types__response_code__last .
C17:   fld_qdcount(fld_header(upf_header(upf_header(
           output_packet, upf_rcode(fld_header(
           output_packet), dns_types__name_error)), upf_ancount(
           fld_header(upf_header(output_packet, upf_rcode(fld_header(
           output_packet), dns_types__name_error))), 0)))) >= 
           dns_types__unsigned_short__first .
C18:   fld_qdcount(fld_header(upf_header(upf_header(
           output_packet, upf_rcode(fld_header(
           output_packet), dns_types__name_error)), upf_ancount(
           fld_header(upf_header(output_packet, upf_rcode(fld_header(
           output_packet), dns_types__name_error))), 0)))) <= 
           dns_types__unsigned_short__last .
C19:   fld_ancount(fld_header(upf_header(upf_header(
           output_packet, upf_rcode(fld_header(
           output_packet), dns_types__name_error)), upf_ancount(
           fld_header(upf_header(output_packet, upf_rcode(fld_header(
           output_packet), dns_types__name_error))), 0)))) >= 
           dns_types__unsigned_short__first .
C20:   fld_ancount(fld_header(upf_header(upf_header(
           output_packet, upf_rcode(fld_header(
           output_packet), dns_types__name_error)), upf_ancount(
           fld_header(upf_header(output_packet, upf_rcode(fld_header(
           output_packet), dns_types__name_error))), 0)))) <= 
           dns_types__unsigned_short__last .
C21:   fld_nscount(fld_header(upf_header(upf_header(
           output_packet, upf_rcode(fld_header(
           output_packet), dns_types__name_error)), upf_ancount(
           fld_header(upf_header(output_packet, upf_rcode(fld_header(
           output_packet), dns_types__name_error))), 0)))) >= 
           dns_types__unsigned_short__first .
C22:   fld_nscount(fld_header(upf_header(upf_header(
           output_packet, upf_rcode(fld_header(
           output_packet), dns_types__name_error)), upf_ancount(
           fld_header(upf_header(output_packet, upf_rcode(fld_header(
           output_packet), dns_types__name_error))), 0)))) <= 
           dns_types__unsigned_short__last .
C23:   fld_arcount(fld_header(upf_header(upf_header(
           output_packet, upf_rcode(fld_header(
           output_packet), dns_types__name_error)), upf_ancount(
           fld_header(upf_header(output_packet, upf_rcode(fld_header(
           output_packet), dns_types__name_error))), 0)))) >= 
           dns_types__unsigned_short__first .
C24:   fld_arcount(fld_header(upf_header(upf_header(
           output_packet, upf_rcode(fld_header(
           output_packet), dns_types__name_error)), upf_ancount(
           fld_header(upf_header(output_packet, upf_rcode(fld_header(
           output_packet), dns_types__name_error))), 0)))) <= 
           dns_types__unsigned_short__last .
C25:   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(upf_header(upf_header(output_packet, upf_rcode(
           fld_header(output_packet), dns_types__name_error)), 
           upf_ancount(fld_header(upf_header(output_packet, upf_rcode(
           fld_header(output_packet), dns_types__name_error))), 0))), [
           i___1]) >= dns_types__byte__first) and (element(fld_bytes(
           upf_header(upf_header(output_packet, upf_rcode(fld_header(
           output_packet), dns_types__name_error)), upf_ancount(
           fld_header(upf_header(output_packet, upf_rcode(fld_header(
           output_packet), dns_types__name_error))), 0))), [
           i___1]) <= dns_types__byte__last))) .
C26:   start_byte <= dns_types__packet_size .
 

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

procedure_create_nxdomain_response_8.
H1:    answer_count = 0 .
H2:    amount_trimmed >= 0 .
H3:    amount_trimmed < rr_type__wirestringtypeindex__last .
H4:    output_bytes <= dns_types__packet_length_range__last .
H5:    current_qname_location <= output_bytes .
H6:    start_byte >= dns_types__packet_bytes_range__first .
H7:    start_byte <= dns_types__packet_bytes_range__last .
H8:    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))) .
H9:    qname_location >= dns_types__qname_ptr_range__first .
H10:   qname_location <= dns_types__qname_ptr_range__last .
H11:   fld_messageid(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H12:   fld_messageid(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H13:   fld_opcode(fld_header(output_packet)) >= 
           dns_types__opcode_type__first .
H14:   fld_opcode(fld_header(output_packet)) <= 
           dns_types__opcode_type__last .
H15:   fld_rcode(fld_header(output_packet)) >= 
           dns_types__response_code__first .
H16:   fld_rcode(fld_header(output_packet)) <= 
           dns_types__response_code__last .
H17:   fld_qdcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H18:   fld_qdcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H19:   fld_ancount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H20:   fld_ancount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H21:   fld_nscount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H22:   fld_nscount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H23:   fld_arcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H24:   fld_arcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H25:   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))) .
H26:   start_byte <= dns_types__packet_size .
H27:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           current_name, [i___1]) >= character__first) and (element(
           current_name, [i___1]) <= character__last))) .
H28:   current_qname_location >= dns_types__qname_ptr_range__first .
H29:   current_qname_location <= dns_types__qname_ptr_range__last .
H30:   current_qname_location >= dns_types__qname_ptr_range__first .
H31:   current_qname_location <= dns_types__qname_ptr_range__last .
H32:   current_qname_location <= 
           dns_types__packet_length_range__last .
H33:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           trimmed_name__1, [i___1]) >= character__first) and (element(
           trimmed_name__1, [i___1]) <= character__last))) .
H34:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H35:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
H36:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H37:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
H38:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           trimmed_name__1, [i___1]) >= character__first) and (element(
           trimmed_name__1, [i___1]) <= character__last))) .
H39:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H40:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
H41:   answer_count >= dns_types__unsigned_short__first .
H42:   answer_count <= dns_types__unsigned_short__last .
H43:   answer_count >= dns_types__unsigned_short__first .
H44:   answer_count <= dns_types__unsigned_short__last .
H45:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H46:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
H47:   start_byte >= dns_types__packet_bytes_range__first .
H48:   start_byte <= dns_types__packet_bytes_range__last .
H49:   start_byte <= dns_types__packet_size .
H50:   answer_count <= dns_types__unsigned_short__last - 
           rr_type__maxnumrecords .
H51:   output_bytes__2 >= dns_types__header_bits div 8 + 1 .
H52:   output_bytes__2 <= dns_types__packet_size .
H53:   answer_count__2 <= answer_count + 
           rr_type__maxnumrecords .
H54:   fld_messageid(fld_header(output_packet__2)) >= 
           dns_types__unsigned_short__first .
H55:   fld_messageid(fld_header(output_packet__2)) <= 
           dns_types__unsigned_short__last .
H56:   fld_opcode(fld_header(output_packet__2)) >= 
           dns_types__opcode_type__first .
H57:   fld_opcode(fld_header(output_packet__2)) <= 
           dns_types__opcode_type__last .
H58:   fld_rcode(fld_header(output_packet__2)) >= 
           dns_types__response_code__first .
H59:   fld_rcode(fld_header(output_packet__2)) <= 
           dns_types__response_code__last .
H60:   fld_qdcount(fld_header(output_packet__2)) >= 
           dns_types__unsigned_short__first .
H61:   fld_qdcount(fld_header(output_packet__2)) <= 
           dns_types__unsigned_short__last .
H62:   fld_ancount(fld_header(output_packet__2)) >= 
           dns_types__unsigned_short__first .
H63:   fld_ancount(fld_header(output_packet__2)) <= 
           dns_types__unsigned_short__last .
H64:   fld_nscount(fld_header(output_packet__2)) >= 
           dns_types__unsigned_short__first .
H65:   fld_nscount(fld_header(output_packet__2)) <= 
           dns_types__unsigned_short__last .
H66:   fld_arcount(fld_header(output_packet__2)) >= 
           dns_types__unsigned_short__first .
H67:   fld_arcount(fld_header(output_packet__2)) <= 
           dns_types__unsigned_short__last .
H68:   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))) .
H69:   answer_count__2 >= dns_types__unsigned_short__first .
H70:   answer_count__2 <= dns_types__unsigned_short__last .
H71:   output_bytes__2 >= dns_types__packet_length_range__first .
H72:   output_bytes__2 <= dns_types__packet_length_range__last .
H73:   output_bytes__2 >= dns_types__packet_length_range__first .
H74:   output_bytes__2 <= dns_types__packet_length_range__last .
H75:   answer_count__2 >= dns_types__unsigned_short__first .
H76:   answer_count__2 <= dns_types__unsigned_short__last .
H77:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           trimmed_name__1, [i___1]) >= character__first) and (element(
           trimmed_name__1, [i___1]) <= character__last))) .
H78:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H79:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
H80:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H81:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
H82:   amount_trimmed >= natural__first .
H83:   amount_trimmed <= natural__last .
H84:   amount_trimmed + (element(domainname, [
           rr_type__wirestringtypeindex__first]) + 1) >= 
           natural__first .
H85:   amount_trimmed + (element(domainname, [
           rr_type__wirestringtypeindex__first]) + 1) <= 
           natural__last .
H86:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= 
           natural__first .
H87:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= 
           natural__last .
H88:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= system__min_int .
H89:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= system__max_int .
H90:   rr_type__wirestringtypeindex__first >= 
           rr_type__wirestringtypeindex__first .
H91:   rr_type__wirestringtypeindex__first <= 
           rr_type__wirestringtypeindex__last .
H92:   output_bytes__2 >= dns_types__packet_length_range__first .
H93:   output_bytes__2 <= dns_types__packet_length_range__last .
H94:   answer_count__2 >= dns_types__unsigned_short__first .
H95:   answer_count__2 <= dns_types__unsigned_short__last .
H96:   amount_trimmed + (element(domainname, [
           rr_type__wirestringtypeindex__first]) + 1) >= 
           natural__first .
H97:   amount_trimmed + (element(domainname, [
           rr_type__wirestringtypeindex__first]) + 1) <= 
           natural__last .
H98:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           trimmed_name__1, [i___1]) >= character__first) and (element(
           trimmed_name__1, [i___1]) <= character__last))) .
H99:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H100:  new_qname_location__1 <= dns_types__qname_ptr_range__last .
H101:  output_bytes__2 >= dns_types__qname_ptr_range__first .
H102:  output_bytes__2 <= dns_types__qname_ptr_range__last .
H103:  element(trimmed_name__1, [rr_type__wirestringtypeindex__first]) >= 
           natural__first .
H104:  element(trimmed_name__1, [rr_type__wirestringtypeindex__first]) <= 
           natural__last .
H105:  rr_type__wirestringtypeindex__first >= 
           rr_type__wirestringtypeindex__first .
H106:  rr_type__wirestringtypeindex__first <= 
           rr_type__wirestringtypeindex__last .
H107:  answer_count__2 = 0 .
H108:  amount_trimmed + (element(domainname, [
           rr_type__wirestringtypeindex__first]) + 1) < 
           rr_type__wirestringtypeindex__last .
H109:  element(trimmed_name__1, [rr_type__wirestringtypeindex__first]) <> 
           0 .
H110:  new_qname_location__1 <= output_bytes__2 .
        ->
C1:    answer_count__2 = 0 .
C2:    amount_trimmed + (element(domainname, [
           rr_type__wirestringtypeindex__first]) + 1) >= 0 .
C3:    amount_trimmed + (element(domainname, [
           rr_type__wirestringtypeindex__first]) + 1) < 
           rr_type__wirestringtypeindex__last .
C4:    output_bytes__2 <= dns_types__packet_length_range__last .
C5:    new_qname_location__1 <= output_bytes__2 .
C6:    start_byte >= dns_types__packet_bytes_range__first .
C7:    start_byte <= dns_types__packet_bytes_range__last .
C8:    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))) .
C9:    qname_location >= dns_types__qname_ptr_range__first .
C10:   qname_location <= dns_types__qname_ptr_range__last .
C11:   fld_messageid(fld_header(output_packet__2)) >= 
           dns_types__unsigned_short__first .
C12:   fld_messageid(fld_header(output_packet__2)) <= 
           dns_types__unsigned_short__last .
C13:   fld_opcode(fld_header(output_packet__2)) >= 
           dns_types__opcode_type__first .
C14:   fld_opcode(fld_header(output_packet__2)) <= 
           dns_types__opcode_type__last .
C15:   fld_rcode(fld_header(output_packet__2)) >= 
           dns_types__response_code__first .
C16:   fld_rcode(fld_header(output_packet__2)) <= 
           dns_types__response_code__last .
C17:   fld_qdcount(fld_header(output_packet__2)) >= 
           dns_types__unsigned_short__first .
C18:   fld_qdcount(fld_header(output_packet__2)) <= 
           dns_types__unsigned_short__last .
C19:   fld_ancount(fld_header(output_packet__2)) >= 
           dns_types__unsigned_short__first .
C20:   fld_ancount(fld_header(output_packet__2)) <= 
           dns_types__unsigned_short__last .
C21:   fld_nscount(fld_header(output_packet__2)) >= 
           dns_types__unsigned_short__first .
C22:   fld_nscount(fld_header(output_packet__2)) <= 
           dns_types__unsigned_short__last .
C23:   fld_arcount(fld_header(output_packet__2)) >= 
           dns_types__unsigned_short__first .
C24:   fld_arcount(fld_header(output_packet__2)) <= 
           dns_types__unsigned_short__last .
C25:   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))) .
C26:   start_byte <= dns_types__packet_size .
 

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

procedure_create_nxdomain_response_9.
H1:    answer_count = 0 .
H2:    amount_trimmed >= 0 .
H3:    amount_trimmed < rr_type__wirestringtypeindex__last .
H4:    output_bytes <= dns_types__packet_length_range__last .
H5:    current_qname_location <= output_bytes .
H6:    start_byte >= dns_types__packet_bytes_range__first .
H7:    start_byte <= dns_types__packet_bytes_range__last .
H8:    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))) .
H9:    qname_location >= dns_types__qname_ptr_range__first .
H10:   qname_location <= dns_types__qname_ptr_range__last .
H11:   fld_messageid(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H12:   fld_messageid(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H13:   fld_opcode(fld_header(output_packet)) >= 
           dns_types__opcode_type__first .
H14:   fld_opcode(fld_header(output_packet)) <= 
           dns_types__opcode_type__last .
H15:   fld_rcode(fld_header(output_packet)) >= 
           dns_types__response_code__first .
H16:   fld_rcode(fld_header(output_packet)) <= 
           dns_types__response_code__last .
H17:   fld_qdcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H18:   fld_qdcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H19:   fld_ancount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H20:   fld_ancount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H21:   fld_nscount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H22:   fld_nscount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H23:   fld_arcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H24:   fld_arcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H25:   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))) .
H26:   start_byte <= dns_types__packet_size .
H27:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           current_name, [i___1]) >= character__first) and (element(
           current_name, [i___1]) <= character__last))) .
H28:   current_qname_location >= dns_types__qname_ptr_range__first .
H29:   current_qname_location <= dns_types__qname_ptr_range__last .
        ->
C1:    current_qname_location >= dns_types__qname_ptr_range__first .
C2:    current_qname_location <= dns_types__qname_ptr_range__last .
C3:    current_qname_location <= 
           dns_types__packet_length_range__last .
 

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

procedure_create_nxdomain_response_10.
H1:    answer_count = 0 .
H2:    amount_trimmed >= 0 .
H3:    amount_trimmed < rr_type__wirestringtypeindex__last .
H4:    output_bytes <= dns_types__packet_length_range__last .
H5:    current_qname_location <= output_bytes .
H6:    start_byte >= dns_types__packet_bytes_range__first .
H7:    start_byte <= dns_types__packet_bytes_range__last .
H8:    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))) .
H9:    qname_location >= dns_types__qname_ptr_range__first .
H10:   qname_location <= dns_types__qname_ptr_range__last .
H11:   fld_messageid(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H12:   fld_messageid(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H13:   fld_opcode(fld_header(output_packet)) >= 
           dns_types__opcode_type__first .
H14:   fld_opcode(fld_header(output_packet)) <= 
           dns_types__opcode_type__last .
H15:   fld_rcode(fld_header(output_packet)) >= 
           dns_types__response_code__first .
H16:   fld_rcode(fld_header(output_packet)) <= 
           dns_types__response_code__last .
H17:   fld_qdcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H18:   fld_qdcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H19:   fld_ancount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H20:   fld_ancount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H21:   fld_nscount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H22:   fld_nscount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H23:   fld_arcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H24:   fld_arcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H25:   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))) .
H26:   start_byte <= dns_types__packet_size .
H27:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           current_name, [i___1]) >= character__first) and (element(
           current_name, [i___1]) <= character__last))) .
H28:   current_qname_location >= dns_types__qname_ptr_range__first .
H29:   current_qname_location <= dns_types__qname_ptr_range__last .
H30:   current_qname_location >= dns_types__qname_ptr_range__first .
H31:   current_qname_location <= dns_types__qname_ptr_range__last .
H32:   current_qname_location <= 
           dns_types__packet_length_range__last .
H33:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           trimmed_name__1, [i___1]) >= character__first) and (element(
           trimmed_name__1, [i___1]) <= character__last))) .
H34:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H35:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
        ->
C1:    new_qname_location__1 >= dns_types__qname_ptr_range__first .
C2:    new_qname_location__1 <= dns_types__qname_ptr_range__last .
 

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

procedure_create_nxdomain_response_11.
H1:    answer_count = 0 .
H2:    amount_trimmed >= 0 .
H3:    amount_trimmed < rr_type__wirestringtypeindex__last .
H4:    output_bytes <= dns_types__packet_length_range__last .
H5:    current_qname_location <= output_bytes .
H6:    start_byte >= dns_types__packet_bytes_range__first .
H7:    start_byte <= dns_types__packet_bytes_range__last .
H8:    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))) .
H9:    qname_location >= dns_types__qname_ptr_range__first .
H10:   qname_location <= dns_types__qname_ptr_range__last .
H11:   fld_messageid(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H12:   fld_messageid(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H13:   fld_opcode(fld_header(output_packet)) >= 
           dns_types__opcode_type__first .
H14:   fld_opcode(fld_header(output_packet)) <= 
           dns_types__opcode_type__last .
H15:   fld_rcode(fld_header(output_packet)) >= 
           dns_types__response_code__first .
H16:   fld_rcode(fld_header(output_packet)) <= 
           dns_types__response_code__last .
H17:   fld_qdcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H18:   fld_qdcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H19:   fld_ancount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H20:   fld_ancount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H21:   fld_nscount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H22:   fld_nscount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H23:   fld_arcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H24:   fld_arcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H25:   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))) .
H26:   start_byte <= dns_types__packet_size .
H27:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           current_name, [i___1]) >= character__first) and (element(
           current_name, [i___1]) <= character__last))) .
H28:   current_qname_location >= dns_types__qname_ptr_range__first .
H29:   current_qname_location <= dns_types__qname_ptr_range__last .
H30:   current_qname_location >= dns_types__qname_ptr_range__first .
H31:   current_qname_location <= dns_types__qname_ptr_range__last .
H32:   current_qname_location <= 
           dns_types__packet_length_range__last .
H33:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           trimmed_name__1, [i___1]) >= character__first) and (element(
           trimmed_name__1, [i___1]) <= character__last))) .
H34:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H35:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
H36:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H37:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
H38:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           trimmed_name__1, [i___1]) >= character__first) and (element(
           trimmed_name__1, [i___1]) <= character__last))) .
H39:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H40:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
H41:   answer_count >= dns_types__unsigned_short__first .
H42:   answer_count <= dns_types__unsigned_short__last .
        ->
C1:    answer_count >= dns_types__unsigned_short__first .
C2:    answer_count <= dns_types__unsigned_short__last .
C3:    new_qname_location__1 >= dns_types__qname_ptr_range__first .
C4:    new_qname_location__1 <= dns_types__qname_ptr_range__last .
C5:    start_byte >= dns_types__packet_bytes_range__first .
C6:    start_byte <= dns_types__packet_bytes_range__last .
C7:    start_byte <= dns_types__packet_size .
C8:    answer_count <= dns_types__unsigned_short__last - 
           rr_type__maxnumrecords .
 

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

procedure_create_nxdomain_response_12.
H1:    answer_count = 0 .
H2:    amount_trimmed >= 0 .
H3:    amount_trimmed < rr_type__wirestringtypeindex__last .
H4:    output_bytes <= dns_types__packet_length_range__last .
H5:    current_qname_location <= output_bytes .
H6:    start_byte >= dns_types__packet_bytes_range__first .
H7:    start_byte <= dns_types__packet_bytes_range__last .
H8:    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))) .
H9:    qname_location >= dns_types__qname_ptr_range__first .
H10:   qname_location <= dns_types__qname_ptr_range__last .
H11:   fld_messageid(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H12:   fld_messageid(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H13:   fld_opcode(fld_header(output_packet)) >= 
           dns_types__opcode_type__first .
H14:   fld_opcode(fld_header(output_packet)) <= 
           dns_types__opcode_type__last .
H15:   fld_rcode(fld_header(output_packet)) >= 
           dns_types__response_code__first .
H16:   fld_rcode(fld_header(output_packet)) <= 
           dns_types__response_code__last .
H17:   fld_qdcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H18:   fld_qdcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H19:   fld_ancount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H20:   fld_ancount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H21:   fld_nscount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H22:   fld_nscount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H23:   fld_arcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H24:   fld_arcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H25:   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))) .
H26:   start_byte <= dns_types__packet_size .
H27:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           current_name, [i___1]) >= character__first) and (element(
           current_name, [i___1]) <= character__last))) .
H28:   current_qname_location >= dns_types__qname_ptr_range__first .
H29:   current_qname_location <= dns_types__qname_ptr_range__last .
H30:   current_qname_location >= dns_types__qname_ptr_range__first .
H31:   current_qname_location <= dns_types__qname_ptr_range__last .
H32:   current_qname_location <= 
           dns_types__packet_length_range__last .
H33:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           trimmed_name__1, [i___1]) >= character__first) and (element(
           trimmed_name__1, [i___1]) <= character__last))) .
H34:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H35:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
H36:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H37:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
H38:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           trimmed_name__1, [i___1]) >= character__first) and (element(
           trimmed_name__1, [i___1]) <= character__last))) .
H39:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H40:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
H41:   answer_count >= dns_types__unsigned_short__first .
H42:   answer_count <= dns_types__unsigned_short__last .
H43:   answer_count >= dns_types__unsigned_short__first .
H44:   answer_count <= dns_types__unsigned_short__last .
H45:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H46:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
H47:   start_byte >= dns_types__packet_bytes_range__first .
H48:   start_byte <= dns_types__packet_bytes_range__last .
H49:   start_byte <= dns_types__packet_size .
H50:   answer_count <= dns_types__unsigned_short__last - 
           rr_type__maxnumrecords .
H51:   output_bytes__2 >= dns_types__header_bits div 8 + 1 .
H52:   output_bytes__2 <= dns_types__packet_size .
H53:   answer_count__2 <= answer_count + 
           rr_type__maxnumrecords .
H54:   fld_messageid(fld_header(output_packet__2)) >= 
           dns_types__unsigned_short__first .
H55:   fld_messageid(fld_header(output_packet__2)) <= 
           dns_types__unsigned_short__last .
H56:   fld_opcode(fld_header(output_packet__2)) >= 
           dns_types__opcode_type__first .
H57:   fld_opcode(fld_header(output_packet__2)) <= 
           dns_types__opcode_type__last .
H58:   fld_rcode(fld_header(output_packet__2)) >= 
           dns_types__response_code__first .
H59:   fld_rcode(fld_header(output_packet__2)) <= 
           dns_types__response_code__last .
H60:   fld_qdcount(fld_header(output_packet__2)) >= 
           dns_types__unsigned_short__first .
H61:   fld_qdcount(fld_header(output_packet__2)) <= 
           dns_types__unsigned_short__last .
H62:   fld_ancount(fld_header(output_packet__2)) >= 
           dns_types__unsigned_short__first .
H63:   fld_ancount(fld_header(output_packet__2)) <= 
           dns_types__unsigned_short__last .
H64:   fld_nscount(fld_header(output_packet__2)) >= 
           dns_types__unsigned_short__first .
H65:   fld_nscount(fld_header(output_packet__2)) <= 
           dns_types__unsigned_short__last .
H66:   fld_arcount(fld_header(output_packet__2)) >= 
           dns_types__unsigned_short__first .
H67:   fld_arcount(fld_header(output_packet__2)) <= 
           dns_types__unsigned_short__last .
H68:   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))) .
H69:   answer_count__2 >= dns_types__unsigned_short__first .
H70:   answer_count__2 <= dns_types__unsigned_short__last .
H71:   output_bytes__2 >= dns_types__packet_length_range__first .
H72:   output_bytes__2 <= dns_types__packet_length_range__last .
        ->
C1:    output_bytes__2 >= dns_types__packet_length_range__first .
C2:    output_bytes__2 <= dns_types__packet_length_range__last .
C3:    answer_count__2 >= dns_types__unsigned_short__first .
C4:    answer_count__2 <= dns_types__unsigned_short__last .
 

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

procedure_create_nxdomain_response_13.
H1:    answer_count = 0 .
H2:    amount_trimmed >= 0 .
H3:    amount_trimmed < rr_type__wirestringtypeindex__last .
H4:    output_bytes <= dns_types__packet_length_range__last .
H5:    current_qname_location <= output_bytes .
H6:    start_byte >= dns_types__packet_bytes_range__first .
H7:    start_byte <= dns_types__packet_bytes_range__last .
H8:    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))) .
H9:    qname_location >= dns_types__qname_ptr_range__first .
H10:   qname_location <= dns_types__qname_ptr_range__last .
H11:   fld_messageid(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H12:   fld_messageid(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H13:   fld_opcode(fld_header(output_packet)) >= 
           dns_types__opcode_type__first .
H14:   fld_opcode(fld_header(output_packet)) <= 
           dns_types__opcode_type__last .
H15:   fld_rcode(fld_header(output_packet)) >= 
           dns_types__response_code__first .
H16:   fld_rcode(fld_header(output_packet)) <= 
           dns_types__response_code__last .
H17:   fld_qdcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H18:   fld_qdcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H19:   fld_ancount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H20:   fld_ancount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H21:   fld_nscount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H22:   fld_nscount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H23:   fld_arcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H24:   fld_arcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H25:   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))) .
H26:   start_byte <= dns_types__packet_size .
H27:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           current_name, [i___1]) >= character__first) and (element(
           current_name, [i___1]) <= character__last))) .
H28:   current_qname_location >= dns_types__qname_ptr_range__first .
H29:   current_qname_location <= dns_types__qname_ptr_range__last .
H30:   current_qname_location >= dns_types__qname_ptr_range__first .
H31:   current_qname_location <= dns_types__qname_ptr_range__last .
H32:   current_qname_location <= 
           dns_types__packet_length_range__last .
H33:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           trimmed_name__1, [i___1]) >= character__first) and (element(
           trimmed_name__1, [i___1]) <= character__last))) .
H34:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H35:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
H36:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H37:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
H38:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           trimmed_name__1, [i___1]) >= character__first) and (element(
           trimmed_name__1, [i___1]) <= character__last))) .
H39:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H40:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
H41:   answer_count >= dns_types__unsigned_short__first .
H42:   answer_count <= dns_types__unsigned_short__last .
H43:   answer_count >= dns_types__unsigned_short__first .
H44:   answer_count <= dns_types__unsigned_short__last .
H45:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H46:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
H47:   start_byte >= dns_types__packet_bytes_range__first .
H48:   start_byte <= dns_types__packet_bytes_range__last .
H49:   start_byte <= dns_types__packet_size .
H50:   answer_count <= dns_types__unsigned_short__last - 
           rr_type__maxnumrecords .
H51:   output_bytes__2 >= dns_types__header_bits div 8 + 1 .
H52:   output_bytes__2 <= dns_types__packet_size .
H53:   answer_count__2 <= answer_count + 
           rr_type__maxnumrecords .
H54:   fld_messageid(fld_header(output_packet__2)) >= 
           dns_types__unsigned_short__first .
H55:   fld_messageid(fld_header(output_packet__2)) <= 
           dns_types__unsigned_short__last .
H56:   fld_opcode(fld_header(output_packet__2)) >= 
           dns_types__opcode_type__first .
H57:   fld_opcode(fld_header(output_packet__2)) <= 
           dns_types__opcode_type__last .
H58:   fld_rcode(fld_header(output_packet__2)) >= 
           dns_types__response_code__first .
H59:   fld_rcode(fld_header(output_packet__2)) <= 
           dns_types__response_code__last .
H60:   fld_qdcount(fld_header(output_packet__2)) >= 
           dns_types__unsigned_short__first .
H61:   fld_qdcount(fld_header(output_packet__2)) <= 
           dns_types__unsigned_short__last .
H62:   fld_ancount(fld_header(output_packet__2)) >= 
           dns_types__unsigned_short__first .
H63:   fld_ancount(fld_header(output_packet__2)) <= 
           dns_types__unsigned_short__last .
H64:   fld_nscount(fld_header(output_packet__2)) >= 
           dns_types__unsigned_short__first .
H65:   fld_nscount(fld_header(output_packet__2)) <= 
           dns_types__unsigned_short__last .
H66:   fld_arcount(fld_header(output_packet__2)) >= 
           dns_types__unsigned_short__first .
H67:   fld_arcount(fld_header(output_packet__2)) <= 
           dns_types__unsigned_short__last .
H68:   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))) .
H69:   answer_count__2 >= dns_types__unsigned_short__first .
H70:   answer_count__2 <= dns_types__unsigned_short__last .
H71:   output_bytes__2 >= dns_types__packet_length_range__first .
H72:   output_bytes__2 <= dns_types__packet_length_range__last .
H73:   output_bytes__2 >= dns_types__packet_length_range__first .
H74:   output_bytes__2 <= dns_types__packet_length_range__last .
H75:   answer_count__2 >= dns_types__unsigned_short__first .
H76:   answer_count__2 <= dns_types__unsigned_short__last .
H77:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           trimmed_name__1, [i___1]) >= character__first) and (element(
           trimmed_name__1, [i___1]) <= character__last))) .
H78:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H79:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
        ->
C1:    new_qname_location__1 >= dns_types__qname_ptr_range__first .
C2:    new_qname_location__1 <= dns_types__qname_ptr_range__last .
 

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

procedure_create_nxdomain_response_14.
H1:    answer_count = 0 .
H2:    amount_trimmed >= 0 .
H3:    amount_trimmed < rr_type__wirestringtypeindex__last .
H4:    output_bytes <= dns_types__packet_length_range__last .
H5:    current_qname_location <= output_bytes .
H6:    start_byte >= dns_types__packet_bytes_range__first .
H7:    start_byte <= dns_types__packet_bytes_range__last .
H8:    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))) .
H9:    qname_location >= dns_types__qname_ptr_range__first .
H10:   qname_location <= dns_types__qname_ptr_range__last .
H11:   fld_messageid(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H12:   fld_messageid(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H13:   fld_opcode(fld_header(output_packet)) >= 
           dns_types__opcode_type__first .
H14:   fld_opcode(fld_header(output_packet)) <= 
           dns_types__opcode_type__last .
H15:   fld_rcode(fld_header(output_packet)) >= 
           dns_types__response_code__first .
H16:   fld_rcode(fld_header(output_packet)) <= 
           dns_types__response_code__last .
H17:   fld_qdcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H18:   fld_qdcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H19:   fld_ancount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H20:   fld_ancount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H21:   fld_nscount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H22:   fld_nscount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H23:   fld_arcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H24:   fld_arcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H25:   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))) .
H26:   start_byte <= dns_types__packet_size .
H27:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           current_name, [i___1]) >= character__first) and (element(
           current_name, [i___1]) <= character__last))) .
H28:   current_qname_location >= dns_types__qname_ptr_range__first .
H29:   current_qname_location <= dns_types__qname_ptr_range__last .
H30:   current_qname_location >= dns_types__qname_ptr_range__first .
H31:   current_qname_location <= dns_types__qname_ptr_range__last .
H32:   current_qname_location <= 
           dns_types__packet_length_range__last .
H33:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           trimmed_name__1, [i___1]) >= character__first) and (element(
           trimmed_name__1, [i___1]) <= character__last))) .
H34:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H35:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
H36:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H37:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
H38:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           trimmed_name__1, [i___1]) >= character__first) and (element(
           trimmed_name__1, [i___1]) <= character__last))) .
H39:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H40:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
H41:   answer_count >= dns_types__unsigned_short__first .
H42:   answer_count <= dns_types__unsigned_short__last .
H43:   answer_count >= dns_types__unsigned_short__first .
H44:   answer_count <= dns_types__unsigned_short__last .
H45:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H46:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
H47:   start_byte >= dns_types__packet_bytes_range__first .
H48:   start_byte <= dns_types__packet_bytes_range__last .
H49:   start_byte <= dns_types__packet_size .
H50:   answer_count <= dns_types__unsigned_short__last - 
           rr_type__maxnumrecords .
H51:   output_bytes__2 >= dns_types__header_bits div 8 + 1 .
H52:   output_bytes__2 <= dns_types__packet_size .
H53:   answer_count__2 <= answer_count + 
           rr_type__maxnumrecords .
H54:   fld_messageid(fld_header(output_packet__2)) >= 
           dns_types__unsigned_short__first .
H55:   fld_messageid(fld_header(output_packet__2)) <= 
           dns_types__unsigned_short__last .
H56:   fld_opcode(fld_header(output_packet__2)) >= 
           dns_types__opcode_type__first .
H57:   fld_opcode(fld_header(output_packet__2)) <= 
           dns_types__opcode_type__last .
H58:   fld_rcode(fld_header(output_packet__2)) >= 
           dns_types__response_code__first .
H59:   fld_rcode(fld_header(output_packet__2)) <= 
           dns_types__response_code__last .
H60:   fld_qdcount(fld_header(output_packet__2)) >= 
           dns_types__unsigned_short__first .
H61:   fld_qdcount(fld_header(output_packet__2)) <= 
           dns_types__unsigned_short__last .
H62:   fld_ancount(fld_header(output_packet__2)) >= 
           dns_types__unsigned_short__first .
H63:   fld_ancount(fld_header(output_packet__2)) <= 
           dns_types__unsigned_short__last .
H64:   fld_nscount(fld_header(output_packet__2)) >= 
           dns_types__unsigned_short__first .
H65:   fld_nscount(fld_header(output_packet__2)) <= 
           dns_types__unsigned_short__last .
H66:   fld_arcount(fld_header(output_packet__2)) >= 
           dns_types__unsigned_short__first .
H67:   fld_arcount(fld_header(output_packet__2)) <= 
           dns_types__unsigned_short__last .
H68:   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))) .
H69:   answer_count__2 >= dns_types__unsigned_short__first .
H70:   answer_count__2 <= dns_types__unsigned_short__last .
H71:   output_bytes__2 >= dns_types__packet_length_range__first .
H72:   output_bytes__2 <= dns_types__packet_length_range__last .
H73:   output_bytes__2 >= dns_types__packet_length_range__first .
H74:   output_bytes__2 <= dns_types__packet_length_range__last .
H75:   answer_count__2 >= dns_types__unsigned_short__first .
H76:   answer_count__2 <= dns_types__unsigned_short__last .
H77:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           trimmed_name__1, [i___1]) >= character__first) and (element(
           trimmed_name__1, [i___1]) <= character__last))) .
H78:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H79:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
H80:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H81:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
H82:   amount_trimmed >= natural__first .
H83:   amount_trimmed <= natural__last .
        ->
C1:    amount_trimmed + (element(domainname, [
           rr_type__wirestringtypeindex__first]) + 1) >= 
           natural__first .
C2:    amount_trimmed + (element(domainname, [
           rr_type__wirestringtypeindex__first]) + 1) <= 
           natural__last .
C3:    element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= 
           natural__first .
C4:    element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= 
           natural__last .
C5:    element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= system__min_int .
C6:    element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= system__max_int .
C7:    rr_type__wirestringtypeindex__first >= 
           rr_type__wirestringtypeindex__first .
C8:    rr_type__wirestringtypeindex__first <= 
           rr_type__wirestringtypeindex__last .
 

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

procedure_create_nxdomain_response_15.
H1:    start_byte <= dns_types__packet_size .
H2:    start_byte >= dns_types__packet_bytes_range__first .
H3:    start_byte <= dns_types__packet_bytes_range__last .
H4:    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))) .
H5:    qname_location >= dns_types__qname_ptr_range__first .
H6:    qname_location <= dns_types__qname_ptr_range__last .
H7:    fld_messageid(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H8:    fld_messageid(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H9:    fld_opcode(fld_header(output_packet)) >= 
           dns_types__opcode_type__first .
H10:   fld_opcode(fld_header(output_packet)) <= 
           dns_types__opcode_type__last .
H11:   fld_rcode(fld_header(output_packet)) >= 
           dns_types__response_code__first .
H12:   fld_rcode(fld_header(output_packet)) <= 
           dns_types__response_code__last .
H13:   fld_qdcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H14:   fld_qdcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H15:   fld_ancount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H16:   fld_ancount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H17:   fld_nscount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H18:   fld_nscount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H19:   fld_arcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H20:   fld_arcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H21:   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))) .
H22:   qname_location >= dns_types__qname_ptr_range__first .
H23:   qname_location <= dns_types__qname_ptr_range__last .
H24:   start_byte + dns_types__header_bits div 8 >= 
           dns_types__packet_length_range__first .
H25:   start_byte + dns_types__header_bits div 8 <= 
           dns_types__packet_length_range__last .
H26:   start_byte + dns_types__header_bits div 8 >= 
           dns_types__packet_length_range__first .
H27:   start_byte + dns_types__header_bits div 8 <= 
           dns_types__packet_length_range__last .
H28:   start_byte + dns_types__header_bits div 8 >= 
           dns_types__packet_bytes_range__base__first .
H29:   start_byte + dns_types__header_bits div 8 <= 
           dns_types__packet_bytes_range__base__last .
H30:   dns_types__header_bits div 8 >= 
           dns_types__packet_bytes_range__first .
H31:   dns_types__header_bits div 8 <= 
           dns_types__packet_bytes_range__last .
H32:   dns_types__header_bits div 8 >= system__min_int .
H33:   dns_types__header_bits div 8 <= system__max_int .
H34:   8 <> 0 .
H35:   dns_types__name_error >= dns_types__response_code__first .
H36:   dns_types__name_error <= dns_types__response_code__last .
H37:   0 >= dns_types__unsigned_short__first .
H38:   0 <= dns_types__unsigned_short__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:   0 >= dns_types__unsigned_short__first .
H42:   0 <= dns_types__unsigned_short__last .
H43:   0 >= natural__first .
H44:   0 <= natural__last .
H45:   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))) .
H46:   qname_location >= dns_types__qname_ptr_range__first .
H47:   qname_location <= dns_types__qname_ptr_range__last .
H48:   start_byte + dns_types__header_bits div 8 >= 
           dns_types__qname_ptr_range__first .
H49:   start_byte + dns_types__header_bits div 8 <= 
           dns_types__qname_ptr_range__last .
H50:   element(domainname, [rr_type__wirestringtypeindex__first]) >= 
           natural__first .
H51:   element(domainname, [rr_type__wirestringtypeindex__first]) <= 
           natural__last .
H52:   rr_type__wirestringtypeindex__first >= 
           rr_type__wirestringtypeindex__first .
H53:   rr_type__wirestringtypeindex__first <= 
           rr_type__wirestringtypeindex__last .
H54:   not ((0 = 0) and (((0 < rr_type__wirestringtypeindex__last) and (element(
           domainname, [rr_type__wirestringtypeindex__first]) <> 0)) and (
           qname_location <= start_byte + 
           dns_types__header_bits div 8))) .
H55:   0 >= dns_types__unsigned_short__first .
H56:   0 <= dns_types__unsigned_short__last .
H57:   0 >= 1 .
H58:   0 >= dns_types__unsigned_short__first .
H59:   0 <= dns_types__unsigned_short__last .
        ->
C1:    0 >= dns_types__unsigned_short__first .
C2:    0 <= dns_types__unsigned_short__last .
 

procedure_create_nxdomain_response_16.
H1:    start_byte <= dns_types__packet_size .
H2:    start_byte >= dns_types__packet_bytes_range__first .
H3:    start_byte <= dns_types__packet_bytes_range__last .
H4:    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))) .
H5:    qname_location >= dns_types__qname_ptr_range__first .
H6:    qname_location <= dns_types__qname_ptr_range__last .
H7:    fld_messageid(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H8:    fld_messageid(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H9:    fld_opcode(fld_header(output_packet)) >= 
           dns_types__opcode_type__first .
H10:   fld_opcode(fld_header(output_packet)) <= 
           dns_types__opcode_type__last .
H11:   fld_rcode(fld_header(output_packet)) >= 
           dns_types__response_code__first .
H12:   fld_rcode(fld_header(output_packet)) <= 
           dns_types__response_code__last .
H13:   fld_qdcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H14:   fld_qdcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H15:   fld_ancount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H16:   fld_ancount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H17:   fld_nscount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H18:   fld_nscount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H19:   fld_arcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H20:   fld_arcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H21:   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))) .
H22:   qname_location >= dns_types__qname_ptr_range__first .
H23:   qname_location <= dns_types__qname_ptr_range__last .
H24:   start_byte + dns_types__header_bits div 8 >= 
           dns_types__packet_length_range__first .
H25:   start_byte + dns_types__header_bits div 8 <= 
           dns_types__packet_length_range__last .
H26:   start_byte + dns_types__header_bits div 8 >= 
           dns_types__packet_length_range__first .
H27:   start_byte + dns_types__header_bits div 8 <= 
           dns_types__packet_length_range__last .
H28:   start_byte + dns_types__header_bits div 8 >= 
           dns_types__packet_bytes_range__base__first .
H29:   start_byte + dns_types__header_bits div 8 <= 
           dns_types__packet_bytes_range__base__last .
H30:   dns_types__header_bits div 8 >= 
           dns_types__packet_bytes_range__first .
H31:   dns_types__header_bits div 8 <= 
           dns_types__packet_bytes_range__last .
H32:   dns_types__header_bits div 8 >= system__min_int .
H33:   dns_types__header_bits div 8 <= system__max_int .
H34:   8 <> 0 .
H35:   dns_types__name_error >= dns_types__response_code__first .
H36:   dns_types__name_error <= dns_types__response_code__last .
H37:   0 >= dns_types__unsigned_short__first .
H38:   0 <= dns_types__unsigned_short__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:   0 >= dns_types__unsigned_short__first .
H42:   0 <= dns_types__unsigned_short__last .
H43:   0 >= natural__first .
H44:   0 <= natural__last .
H45:   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))) .
H46:   qname_location >= dns_types__qname_ptr_range__first .
H47:   qname_location <= dns_types__qname_ptr_range__last .
H48:   start_byte + dns_types__header_bits div 8 >= 
           dns_types__qname_ptr_range__first .
H49:   start_byte + dns_types__header_bits div 8 <= 
           dns_types__qname_ptr_range__last .
H50:   element(domainname, [rr_type__wirestringtypeindex__first]) >= 
           natural__first .
H51:   element(domainname, [rr_type__wirestringtypeindex__first]) <= 
           natural__last .
H52:   rr_type__wirestringtypeindex__first >= 
           rr_type__wirestringtypeindex__first .
H53:   rr_type__wirestringtypeindex__first <= 
           rr_type__wirestringtypeindex__last .
H54:   not ((0 = 0) and (((0 < rr_type__wirestringtypeindex__last) and (element(
           domainname, [rr_type__wirestringtypeindex__first]) <> 0)) and (
           qname_location <= start_byte + 
           dns_types__header_bits div 8))) .
H55:   0 >= dns_types__unsigned_short__first .
H56:   0 <= dns_types__unsigned_short__last .
H57:   not (0 >= 1) .
H58:   0 >= dns_types__unsigned_short__first .
H59:   0 <= dns_types__unsigned_short__last .
        ->
C1:    0 >= dns_types__unsigned_short__first .
C2:    0 <= dns_types__unsigned_short__last .
 

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

procedure_create_nxdomain_response_17.
H1:    answer_count = 0 .
H2:    amount_trimmed >= 0 .
H3:    amount_trimmed < rr_type__wirestringtypeindex__last .
H4:    output_bytes <= dns_types__packet_length_range__last .
H5:    current_qname_location <= output_bytes .
H6:    start_byte >= dns_types__packet_bytes_range__first .
H7:    start_byte <= dns_types__packet_bytes_range__last .
H8:    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))) .
H9:    qname_location >= dns_types__qname_ptr_range__first .
H10:   qname_location <= dns_types__qname_ptr_range__last .
H11:   fld_messageid(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H12:   fld_messageid(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H13:   fld_opcode(fld_header(output_packet)) >= 
           dns_types__opcode_type__first .
H14:   fld_opcode(fld_header(output_packet)) <= 
           dns_types__opcode_type__last .
H15:   fld_rcode(fld_header(output_packet)) >= 
           dns_types__response_code__first .
H16:   fld_rcode(fld_header(output_packet)) <= 
           dns_types__response_code__last .
H17:   fld_qdcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H18:   fld_qdcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H19:   fld_ancount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H20:   fld_ancount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H21:   fld_nscount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H22:   fld_nscount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H23:   fld_arcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H24:   fld_arcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H25:   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))) .
H26:   start_byte <= dns_types__packet_size .
H27:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           current_name, [i___1]) >= character__first) and (element(
           current_name, [i___1]) <= character__last))) .
H28:   current_qname_location >= dns_types__qname_ptr_range__first .
H29:   current_qname_location <= dns_types__qname_ptr_range__last .
H30:   current_qname_location >= dns_types__qname_ptr_range__first .
H31:   current_qname_location <= dns_types__qname_ptr_range__last .
H32:   current_qname_location <= 
           dns_types__packet_length_range__last .
H33:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           trimmed_name__1, [i___1]) >= character__first) and (element(
           trimmed_name__1, [i___1]) <= character__last))) .
H34:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H35:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
H36:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H37:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
H38:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           trimmed_name__1, [i___1]) >= character__first) and (element(
           trimmed_name__1, [i___1]) <= character__last))) .
H39:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H40:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
H41:   answer_count >= dns_types__unsigned_short__first .
H42:   answer_count <= dns_types__unsigned_short__last .
H43:   answer_count >= dns_types__unsigned_short__first .
H44:   answer_count <= dns_types__unsigned_short__last .
H45:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H46:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
H47:   start_byte >= dns_types__packet_bytes_range__first .
H48:   start_byte <= dns_types__packet_bytes_range__last .
H49:   start_byte <= dns_types__packet_size .
H50:   answer_count <= dns_types__unsigned_short__last - 
           rr_type__maxnumrecords .
H51:   output_bytes__2 >= dns_types__header_bits div 8 + 1 .
H52:   output_bytes__2 <= dns_types__packet_size .
H53:   answer_count__2 <= answer_count + 
           rr_type__maxnumrecords .
H54:   fld_messageid(fld_header(output_packet__2)) >= 
           dns_types__unsigned_short__first .
H55:   fld_messageid(fld_header(output_packet__2)) <= 
           dns_types__unsigned_short__last .
H56:   fld_opcode(fld_header(output_packet__2)) >= 
           dns_types__opcode_type__first .
H57:   fld_opcode(fld_header(output_packet__2)) <= 
           dns_types__opcode_type__last .
H58:   fld_rcode(fld_header(output_packet__2)) >= 
           dns_types__response_code__first .
H59:   fld_rcode(fld_header(output_packet__2)) <= 
           dns_types__response_code__last .
H60:   fld_qdcount(fld_header(output_packet__2)) >= 
           dns_types__unsigned_short__first .
H61:   fld_qdcount(fld_header(output_packet__2)) <= 
           dns_types__unsigned_short__last .
H62:   fld_ancount(fld_header(output_packet__2)) >= 
           dns_types__unsigned_short__first .
H63:   fld_ancount(fld_header(output_packet__2)) <= 
           dns_types__unsigned_short__last .
H64:   fld_nscount(fld_header(output_packet__2)) >= 
           dns_types__unsigned_short__first .
H65:   fld_nscount(fld_header(output_packet__2)) <= 
           dns_types__unsigned_short__last .
H66:   fld_arcount(fld_header(output_packet__2)) >= 
           dns_types__unsigned_short__first .
H67:   fld_arcount(fld_header(output_packet__2)) <= 
           dns_types__unsigned_short__last .
H68:   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))) .
H69:   answer_count__2 >= dns_types__unsigned_short__first .
H70:   answer_count__2 <= dns_types__unsigned_short__last .
H71:   output_bytes__2 >= dns_types__packet_length_range__first .
H72:   output_bytes__2 <= dns_types__packet_length_range__last .
H73:   output_bytes__2 >= dns_types__packet_length_range__first .
H74:   output_bytes__2 <= dns_types__packet_length_range__last .
H75:   answer_count__2 >= dns_types__unsigned_short__first .
H76:   answer_count__2 <= dns_types__unsigned_short__last .
H77:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           trimmed_name__1, [i___1]) >= character__first) and (element(
           trimmed_name__1, [i___1]) <= character__last))) .
H78:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H79:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
H80:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H81:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
H82:   amount_trimmed >= natural__first .
H83:   amount_trimmed <= natural__last .
H84:   amount_trimmed + (element(domainname, [
           rr_type__wirestringtypeindex__first]) + 1) >= 
           natural__first .
H85:   amount_trimmed + (element(domainname, [
           rr_type__wirestringtypeindex__first]) + 1) <= 
           natural__last .
H86:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= 
           natural__first .
H87:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= 
           natural__last .
H88:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= system__min_int .
H89:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= system__max_int .
H90:   rr_type__wirestringtypeindex__first >= 
           rr_type__wirestringtypeindex__first .
H91:   rr_type__wirestringtypeindex__first <= 
           rr_type__wirestringtypeindex__last .
H92:   output_bytes__2 >= dns_types__packet_length_range__first .
H93:   output_bytes__2 <= dns_types__packet_length_range__last .
H94:   answer_count__2 >= dns_types__unsigned_short__first .
H95:   answer_count__2 <= dns_types__unsigned_short__last .
H96:   amount_trimmed + (element(domainname, [
           rr_type__wirestringtypeindex__first]) + 1) >= 
           natural__first .
H97:   amount_trimmed + (element(domainname, [
           rr_type__wirestringtypeindex__first]) + 1) <= 
           natural__last .
H98:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           trimmed_name__1, [i___1]) >= character__first) and (element(
           trimmed_name__1, [i___1]) <= character__last))) .
H99:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H100:  new_qname_location__1 <= dns_types__qname_ptr_range__last .
H101:  output_bytes__2 >= dns_types__qname_ptr_range__first .
H102:  output_bytes__2 <= dns_types__qname_ptr_range__last .
H103:  element(trimmed_name__1, [rr_type__wirestringtypeindex__first]) >= 
           natural__first .
H104:  element(trimmed_name__1, [rr_type__wirestringtypeindex__first]) <= 
           natural__last .
H105:  rr_type__wirestringtypeindex__first >= 
           rr_type__wirestringtypeindex__first .
H106:  rr_type__wirestringtypeindex__first <= 
           rr_type__wirestringtypeindex__last .
H107:  not ((answer_count__2 = 0) and (((amount_trimmed + (element(
           domainname, [rr_type__wirestringtypeindex__first]) + 1) < 
           rr_type__wirestringtypeindex__last) and (element(
           trimmed_name__1, [rr_type__wirestringtypeindex__first]) <> 0)) and (
           new_qname_location__1 <= output_bytes__2))) .
H108:  answer_count__2 >= dns_types__unsigned_short__first .
H109:  answer_count__2 <= dns_types__unsigned_short__last .
H110:  answer_count__2 >= 1 .
H111:  answer_count__2 >= dns_types__unsigned_short__first .
H112:  answer_count__2 <= dns_types__unsigned_short__last .
        ->
C1:    answer_count__2 >= dns_types__unsigned_short__first .
C2:    answer_count__2 <= dns_types__unsigned_short__last .
 

procedure_create_nxdomain_response_18.
H1:    answer_count = 0 .
H2:    amount_trimmed >= 0 .
H3:    amount_trimmed < rr_type__wirestringtypeindex__last .
H4:    output_bytes <= dns_types__packet_length_range__last .
H5:    current_qname_location <= output_bytes .
H6:    start_byte >= dns_types__packet_bytes_range__first .
H7:    start_byte <= dns_types__packet_bytes_range__last .
H8:    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))) .
H9:    qname_location >= dns_types__qname_ptr_range__first .
H10:   qname_location <= dns_types__qname_ptr_range__last .
H11:   fld_messageid(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H12:   fld_messageid(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H13:   fld_opcode(fld_header(output_packet)) >= 
           dns_types__opcode_type__first .
H14:   fld_opcode(fld_header(output_packet)) <= 
           dns_types__opcode_type__last .
H15:   fld_rcode(fld_header(output_packet)) >= 
           dns_types__response_code__first .
H16:   fld_rcode(fld_header(output_packet)) <= 
           dns_types__response_code__last .
H17:   fld_qdcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H18:   fld_qdcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H19:   fld_ancount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H20:   fld_ancount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H21:   fld_nscount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H22:   fld_nscount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H23:   fld_arcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H24:   fld_arcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H25:   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))) .
H26:   start_byte <= dns_types__packet_size .
H27:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           current_name, [i___1]) >= character__first) and (element(
           current_name, [i___1]) <= character__last))) .
H28:   current_qname_location >= dns_types__qname_ptr_range__first .
H29:   current_qname_location <= dns_types__qname_ptr_range__last .
H30:   current_qname_location >= dns_types__qname_ptr_range__first .
H31:   current_qname_location <= dns_types__qname_ptr_range__last .
H32:   current_qname_location <= 
           dns_types__packet_length_range__last .
H33:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           trimmed_name__1, [i___1]) >= character__first) and (element(
           trimmed_name__1, [i___1]) <= character__last))) .
H34:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H35:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
H36:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H37:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
H38:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           trimmed_name__1, [i___1]) >= character__first) and (element(
           trimmed_name__1, [i___1]) <= character__last))) .
H39:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H40:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
H41:   answer_count >= dns_types__unsigned_short__first .
H42:   answer_count <= dns_types__unsigned_short__last .
H43:   answer_count >= dns_types__unsigned_short__first .
H44:   answer_count <= dns_types__unsigned_short__last .
H45:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H46:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
H47:   start_byte >= dns_types__packet_bytes_range__first .
H48:   start_byte <= dns_types__packet_bytes_range__last .
H49:   start_byte <= dns_types__packet_size .
H50:   answer_count <= dns_types__unsigned_short__last - 
           rr_type__maxnumrecords .
H51:   output_bytes__2 >= dns_types__header_bits div 8 + 1 .
H52:   output_bytes__2 <= dns_types__packet_size .
H53:   answer_count__2 <= answer_count + 
           rr_type__maxnumrecords .
H54:   fld_messageid(fld_header(output_packet__2)) >= 
           dns_types__unsigned_short__first .
H55:   fld_messageid(fld_header(output_packet__2)) <= 
           dns_types__unsigned_short__last .
H56:   fld_opcode(fld_header(output_packet__2)) >= 
           dns_types__opcode_type__first .
H57:   fld_opcode(fld_header(output_packet__2)) <= 
           dns_types__opcode_type__last .
H58:   fld_rcode(fld_header(output_packet__2)) >= 
           dns_types__response_code__first .
H59:   fld_rcode(fld_header(output_packet__2)) <= 
           dns_types__response_code__last .
H60:   fld_qdcount(fld_header(output_packet__2)) >= 
           dns_types__unsigned_short__first .
H61:   fld_qdcount(fld_header(output_packet__2)) <= 
           dns_types__unsigned_short__last .
H62:   fld_ancount(fld_header(output_packet__2)) >= 
           dns_types__unsigned_short__first .
H63:   fld_ancount(fld_header(output_packet__2)) <= 
           dns_types__unsigned_short__last .
H64:   fld_nscount(fld_header(output_packet__2)) >= 
           dns_types__unsigned_short__first .
H65:   fld_nscount(fld_header(output_packet__2)) <= 
           dns_types__unsigned_short__last .
H66:   fld_arcount(fld_header(output_packet__2)) >= 
           dns_types__unsigned_short__first .
H67:   fld_arcount(fld_header(output_packet__2)) <= 
           dns_types__unsigned_short__last .
H68:   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))) .
H69:   answer_count__2 >= dns_types__unsigned_short__first .
H70:   answer_count__2 <= dns_types__unsigned_short__last .
H71:   output_bytes__2 >= dns_types__packet_length_range__first .
H72:   output_bytes__2 <= dns_types__packet_length_range__last .
H73:   output_bytes__2 >= dns_types__packet_length_range__first .
H74:   output_bytes__2 <= dns_types__packet_length_range__last .
H75:   answer_count__2 >= dns_types__unsigned_short__first .
H76:   answer_count__2 <= dns_types__unsigned_short__last .
H77:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           trimmed_name__1, [i___1]) >= character__first) and (element(
           trimmed_name__1, [i___1]) <= character__last))) .
H78:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H79:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
H80:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H81:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
H82:   amount_trimmed >= natural__first .
H83:   amount_trimmed <= natural__last .
H84:   amount_trimmed + (element(domainname, [
           rr_type__wirestringtypeindex__first]) + 1) >= 
           natural__first .
H85:   amount_trimmed + (element(domainname, [
           rr_type__wirestringtypeindex__first]) + 1) <= 
           natural__last .
H86:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= 
           natural__first .
H87:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= 
           natural__last .
H88:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= system__min_int .
H89:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= system__max_int .
H90:   rr_type__wirestringtypeindex__first >= 
           rr_type__wirestringtypeindex__first .
H91:   rr_type__wirestringtypeindex__first <= 
           rr_type__wirestringtypeindex__last .
H92:   output_bytes__2 >= dns_types__packet_length_range__first .
H93:   output_bytes__2 <= dns_types__packet_length_range__last .
H94:   answer_count__2 >= dns_types__unsigned_short__first .
H95:   answer_count__2 <= dns_types__unsigned_short__last .
H96:   amount_trimmed + (element(domainname, [
           rr_type__wirestringtypeindex__first]) + 1) >= 
           natural__first .
H97:   amount_trimmed + (element(domainname, [
           rr_type__wirestringtypeindex__first]) + 1) <= 
           natural__last .
H98:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           trimmed_name__1, [i___1]) >= character__first) and (element(
           trimmed_name__1, [i___1]) <= character__last))) .
H99:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H100:  new_qname_location__1 <= dns_types__qname_ptr_range__last .
H101:  output_bytes__2 >= dns_types__qname_ptr_range__first .
H102:  output_bytes__2 <= dns_types__qname_ptr_range__last .
H103:  element(trimmed_name__1, [rr_type__wirestringtypeindex__first]) >= 
           natural__first .
H104:  element(trimmed_name__1, [rr_type__wirestringtypeindex__first]) <= 
           natural__last .
H105:  rr_type__wirestringtypeindex__first >= 
           rr_type__wirestringtypeindex__first .
H106:  rr_type__wirestringtypeindex__first <= 
           rr_type__wirestringtypeindex__last .
H107:  not ((answer_count__2 = 0) and (((amount_trimmed + (element(
           domainname, [rr_type__wirestringtypeindex__first]) + 1) < 
           rr_type__wirestringtypeindex__last) and (element(
           trimmed_name__1, [rr_type__wirestringtypeindex__first]) <> 0)) and (
           new_qname_location__1 <= output_bytes__2))) .
H108:  answer_count__2 >= dns_types__unsigned_short__first .
H109:  answer_count__2 <= dns_types__unsigned_short__last .
H110:  not (answer_count__2 >= 1) .
H111:  answer_count__2 >= dns_types__unsigned_short__first .
H112:  answer_count__2 <= dns_types__unsigned_short__last .
        ->
C1:    answer_count__2 >= dns_types__unsigned_short__first .
C2:    answer_count__2 <= dns_types__unsigned_short__last .
 

For path(s) from start to finish:

procedure_create_nxdomain_response_19.
H1:    start_byte <= dns_types__packet_size .
H2:    start_byte >= dns_types__packet_bytes_range__first .
H3:    start_byte <= dns_types__packet_bytes_range__last .
H4:    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))) .
H5:    qname_location >= dns_types__qname_ptr_range__first .
H6:    qname_location <= dns_types__qname_ptr_range__last .
H7:    fld_messageid(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H8:    fld_messageid(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H9:    fld_opcode(fld_header(output_packet)) >= 
           dns_types__opcode_type__first .
H10:   fld_opcode(fld_header(output_packet)) <= 
           dns_types__opcode_type__last .
H11:   fld_rcode(fld_header(output_packet)) >= 
           dns_types__response_code__first .
H12:   fld_rcode(fld_header(output_packet)) <= 
           dns_types__response_code__last .
H13:   fld_qdcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H14:   fld_qdcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H15:   fld_ancount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H16:   fld_ancount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H17:   fld_nscount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H18:   fld_nscount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H19:   fld_arcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H20:   fld_arcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H21:   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))) .
H22:   qname_location >= dns_types__qname_ptr_range__first .
H23:   qname_location <= dns_types__qname_ptr_range__last .
H24:   start_byte + dns_types__header_bits div 8 >= 
           dns_types__packet_length_range__first .
H25:   start_byte + dns_types__header_bits div 8 <= 
           dns_types__packet_length_range__last .
H26:   start_byte + dns_types__header_bits div 8 >= 
           dns_types__packet_length_range__first .
H27:   start_byte + dns_types__header_bits div 8 <= 
           dns_types__packet_length_range__last .
H28:   start_byte + dns_types__header_bits div 8 >= 
           dns_types__packet_bytes_range__base__first .
H29:   start_byte + dns_types__header_bits div 8 <= 
           dns_types__packet_bytes_range__base__last .
H30:   dns_types__header_bits div 8 >= 
           dns_types__packet_bytes_range__first .
H31:   dns_types__header_bits div 8 <= 
           dns_types__packet_bytes_range__last .
H32:   dns_types__header_bits div 8 >= system__min_int .
H33:   dns_types__header_bits div 8 <= system__max_int .
H34:   8 <> 0 .
H35:   dns_types__name_error >= dns_types__response_code__first .
H36:   dns_types__name_error <= dns_types__response_code__last .
H37:   0 >= dns_types__unsigned_short__first .
H38:   0 <= dns_types__unsigned_short__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:   0 >= dns_types__unsigned_short__first .
H42:   0 <= dns_types__unsigned_short__last .
H43:   0 >= natural__first .
H44:   0 <= natural__last .
H45:   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))) .
H46:   qname_location >= dns_types__qname_ptr_range__first .
H47:   qname_location <= dns_types__qname_ptr_range__last .
H48:   start_byte + dns_types__header_bits div 8 >= 
           dns_types__qname_ptr_range__first .
H49:   start_byte + dns_types__header_bits div 8 <= 
           dns_types__qname_ptr_range__last .
H50:   element(domainname, [rr_type__wirestringtypeindex__first]) >= 
           natural__first .
H51:   element(domainname, [rr_type__wirestringtypeindex__first]) <= 
           natural__last .
H52:   rr_type__wirestringtypeindex__first >= 
           rr_type__wirestringtypeindex__first .
H53:   rr_type__wirestringtypeindex__first <= 
           rr_type__wirestringtypeindex__last .
H54:   not ((0 = 0) and (((0 < rr_type__wirestringtypeindex__last) and (element(
           domainname, [rr_type__wirestringtypeindex__first]) <> 0)) and (
           qname_location <= start_byte + 
           dns_types__header_bits div 8))) .
H55:   0 >= dns_types__unsigned_short__first .
H56:   0 <= dns_types__unsigned_short__last .
H57:   0 >= 1 .
H58:   0 >= dns_types__unsigned_short__first .
H59:   0 <= dns_types__unsigned_short__last .
H60:   0 >= dns_types__unsigned_short__first .
H61:   0 <= 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 .
 

procedure_create_nxdomain_response_20.
H1:    start_byte <= dns_types__packet_size .
H2:    start_byte >= dns_types__packet_bytes_range__first .
H3:    start_byte <= dns_types__packet_bytes_range__last .
H4:    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))) .
H5:    qname_location >= dns_types__qname_ptr_range__first .
H6:    qname_location <= dns_types__qname_ptr_range__last .
H7:    fld_messageid(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H8:    fld_messageid(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H9:    fld_opcode(fld_header(output_packet)) >= 
           dns_types__opcode_type__first .
H10:   fld_opcode(fld_header(output_packet)) <= 
           dns_types__opcode_type__last .
H11:   fld_rcode(fld_header(output_packet)) >= 
           dns_types__response_code__first .
H12:   fld_rcode(fld_header(output_packet)) <= 
           dns_types__response_code__last .
H13:   fld_qdcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H14:   fld_qdcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H15:   fld_ancount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H16:   fld_ancount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H17:   fld_nscount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H18:   fld_nscount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H19:   fld_arcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H20:   fld_arcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H21:   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))) .
H22:   qname_location >= dns_types__qname_ptr_range__first .
H23:   qname_location <= dns_types__qname_ptr_range__last .
H24:   start_byte + dns_types__header_bits div 8 >= 
           dns_types__packet_length_range__first .
H25:   start_byte + dns_types__header_bits div 8 <= 
           dns_types__packet_length_range__last .
H26:   start_byte + dns_types__header_bits div 8 >= 
           dns_types__packet_length_range__first .
H27:   start_byte + dns_types__header_bits div 8 <= 
           dns_types__packet_length_range__last .
H28:   start_byte + dns_types__header_bits div 8 >= 
           dns_types__packet_bytes_range__base__first .
H29:   start_byte + dns_types__header_bits div 8 <= 
           dns_types__packet_bytes_range__base__last .
H30:   dns_types__header_bits div 8 >= 
           dns_types__packet_bytes_range__first .
H31:   dns_types__header_bits div 8 <= 
           dns_types__packet_bytes_range__last .
H32:   dns_types__header_bits div 8 >= system__min_int .
H33:   dns_types__header_bits div 8 <= system__max_int .
H34:   8 <> 0 .
H35:   dns_types__name_error >= dns_types__response_code__first .
H36:   dns_types__name_error <= dns_types__response_code__last .
H37:   0 >= dns_types__unsigned_short__first .
H38:   0 <= dns_types__unsigned_short__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:   0 >= dns_types__unsigned_short__first .
H42:   0 <= dns_types__unsigned_short__last .
H43:   0 >= natural__first .
H44:   0 <= natural__last .
H45:   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))) .
H46:   qname_location >= dns_types__qname_ptr_range__first .
H47:   qname_location <= dns_types__qname_ptr_range__last .
H48:   start_byte + dns_types__header_bits div 8 >= 
           dns_types__qname_ptr_range__first .
H49:   start_byte + dns_types__header_bits div 8 <= 
           dns_types__qname_ptr_range__last .
H50:   element(domainname, [rr_type__wirestringtypeindex__first]) >= 
           natural__first .
H51:   element(domainname, [rr_type__wirestringtypeindex__first]) <= 
           natural__last .
H52:   rr_type__wirestringtypeindex__first >= 
           rr_type__wirestringtypeindex__first .
H53:   rr_type__wirestringtypeindex__first <= 
           rr_type__wirestringtypeindex__last .
H54:   not ((0 = 0) and (((0 < rr_type__wirestringtypeindex__last) and (element(
           domainname, [rr_type__wirestringtypeindex__first]) <> 0)) and (
           qname_location <= start_byte + 
           dns_types__header_bits div 8))) .
H55:   0 >= dns_types__unsigned_short__first .
H56:   0 <= dns_types__unsigned_short__last .
H57:   not (0 >= 1) .
H58:   0 >= dns_types__unsigned_short__first .
H59:   0 <= dns_types__unsigned_short__last .
H60:   0 >= dns_types__unsigned_short__first .
H61:   0 <= 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 .
 

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

procedure_create_nxdomain_response_21.
H1:    answer_count = 0 .
H2:    amount_trimmed >= 0 .
H3:    amount_trimmed < rr_type__wirestringtypeindex__last .
H4:    output_bytes <= dns_types__packet_length_range__last .
H5:    current_qname_location <= output_bytes .
H6:    start_byte >= dns_types__packet_bytes_range__first .
H7:    start_byte <= dns_types__packet_bytes_range__last .
H8:    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))) .
H9:    qname_location >= dns_types__qname_ptr_range__first .
H10:   qname_location <= dns_types__qname_ptr_range__last .
H11:   fld_messageid(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H12:   fld_messageid(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H13:   fld_opcode(fld_header(output_packet)) >= 
           dns_types__opcode_type__first .
H14:   fld_opcode(fld_header(output_packet)) <= 
           dns_types__opcode_type__last .
H15:   fld_rcode(fld_header(output_packet)) >= 
           dns_types__response_code__first .
H16:   fld_rcode(fld_header(output_packet)) <= 
           dns_types__response_code__last .
H17:   fld_qdcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H18:   fld_qdcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H19:   fld_ancount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H20:   fld_ancount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H21:   fld_nscount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H22:   fld_nscount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H23:   fld_arcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H24:   fld_arcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H25:   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))) .
H26:   start_byte <= dns_types__packet_size .
H27:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           current_name, [i___1]) >= character__first) and (element(
           current_name, [i___1]) <= character__last))) .
H28:   current_qname_location >= dns_types__qname_ptr_range__first .
H29:   current_qname_location <= dns_types__qname_ptr_range__last .
H30:   current_qname_location >= dns_types__qname_ptr_range__first .
H31:   current_qname_location <= dns_types__qname_ptr_range__last .
H32:   current_qname_location <= 
           dns_types__packet_length_range__last .
H33:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           trimmed_name__1, [i___1]) >= character__first) and (element(
           trimmed_name__1, [i___1]) <= character__last))) .
H34:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H35:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
H36:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H37:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
H38:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           trimmed_name__1, [i___1]) >= character__first) and (element(
           trimmed_name__1, [i___1]) <= character__last))) .
H39:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H40:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
H41:   answer_count >= dns_types__unsigned_short__first .
H42:   answer_count <= dns_types__unsigned_short__last .
H43:   answer_count >= dns_types__unsigned_short__first .
H44:   answer_count <= dns_types__unsigned_short__last .
H45:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H46:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
H47:   start_byte >= dns_types__packet_bytes_range__first .
H48:   start_byte <= dns_types__packet_bytes_range__last .
H49:   start_byte <= dns_types__packet_size .
H50:   answer_count <= dns_types__unsigned_short__last - 
           rr_type__maxnumrecords .
H51:   output_bytes__2 >= dns_types__header_bits div 8 + 1 .
H52:   output_bytes__2 <= dns_types__packet_size .
H53:   answer_count__2 <= answer_count + 
           rr_type__maxnumrecords .
H54:   fld_messageid(fld_header(output_packet__2)) >= 
           dns_types__unsigned_short__first .
H55:   fld_messageid(fld_header(output_packet__2)) <= 
           dns_types__unsigned_short__last .
H56:   fld_opcode(fld_header(output_packet__2)) >= 
           dns_types__opcode_type__first .
H57:   fld_opcode(fld_header(output_packet__2)) <= 
           dns_types__opcode_type__last .
H58:   fld_rcode(fld_header(output_packet__2)) >= 
           dns_types__response_code__first .
H59:   fld_rcode(fld_header(output_packet__2)) <= 
           dns_types__response_code__last .
H60:   fld_qdcount(fld_header(output_packet__2)) >= 
           dns_types__unsigned_short__first .
H61:   fld_qdcount(fld_header(output_packet__2)) <= 
           dns_types__unsigned_short__last .
H62:   fld_ancount(fld_header(output_packet__2)) >= 
           dns_types__unsigned_short__first .
H63:   fld_ancount(fld_header(output_packet__2)) <= 
           dns_types__unsigned_short__last .
H64:   fld_nscount(fld_header(output_packet__2)) >= 
           dns_types__unsigned_short__first .
H65:   fld_nscount(fld_header(output_packet__2)) <= 
           dns_types__unsigned_short__last .
H66:   fld_arcount(fld_header(output_packet__2)) >= 
           dns_types__unsigned_short__first .
H67:   fld_arcount(fld_header(output_packet__2)) <= 
           dns_types__unsigned_short__last .
H68:   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))) .
H69:   answer_count__2 >= dns_types__unsigned_short__first .
H70:   answer_count__2 <= dns_types__unsigned_short__last .
H71:   output_bytes__2 >= dns_types__packet_length_range__first .
H72:   output_bytes__2 <= dns_types__packet_length_range__last .
H73:   output_bytes__2 >= dns_types__packet_length_range__first .
H74:   output_bytes__2 <= dns_types__packet_length_range__last .
H75:   answer_count__2 >= dns_types__unsigned_short__first .
H76:   answer_count__2 <= dns_types__unsigned_short__last .
H77:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           trimmed_name__1, [i___1]) >= character__first) and (element(
           trimmed_name__1, [i___1]) <= character__last))) .
H78:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H79:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
H80:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H81:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
H82:   amount_trimmed >= natural__first .
H83:   amount_trimmed <= natural__last .
H84:   amount_trimmed + (element(domainname, [
           rr_type__wirestringtypeindex__first]) + 1) >= 
           natural__first .
H85:   amount_trimmed + (element(domainname, [
           rr_type__wirestringtypeindex__first]) + 1) <= 
           natural__last .
H86:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= 
           natural__first .
H87:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= 
           natural__last .
H88:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= system__min_int .
H89:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= system__max_int .
H90:   rr_type__wirestringtypeindex__first >= 
           rr_type__wirestringtypeindex__first .
H91:   rr_type__wirestringtypeindex__first <= 
           rr_type__wirestringtypeindex__last .
H92:   output_bytes__2 >= dns_types__packet_length_range__first .
H93:   output_bytes__2 <= dns_types__packet_length_range__last .
H94:   answer_count__2 >= dns_types__unsigned_short__first .
H95:   answer_count__2 <= dns_types__unsigned_short__last .
H96:   amount_trimmed + (element(domainname, [
           rr_type__wirestringtypeindex__first]) + 1) >= 
           natural__first .
H97:   amount_trimmed + (element(domainname, [
           rr_type__wirestringtypeindex__first]) + 1) <= 
           natural__last .
H98:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           trimmed_name__1, [i___1]) >= character__first) and (element(
           trimmed_name__1, [i___1]) <= character__last))) .
H99:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H100:  new_qname_location__1 <= dns_types__qname_ptr_range__last .
H101:  output_bytes__2 >= dns_types__qname_ptr_range__first .
H102:  output_bytes__2 <= dns_types__qname_ptr_range__last .
H103:  element(trimmed_name__1, [rr_type__wirestringtypeindex__first]) >= 
           natural__first .
H104:  element(trimmed_name__1, [rr_type__wirestringtypeindex__first]) <= 
           natural__last .
H105:  rr_type__wirestringtypeindex__first >= 
           rr_type__wirestringtypeindex__first .
H106:  rr_type__wirestringtypeindex__first <= 
           rr_type__wirestringtypeindex__last .
H107:  not ((answer_count__2 = 0) and (((amount_trimmed + (element(
           domainname, [rr_type__wirestringtypeindex__first]) + 1) < 
           rr_type__wirestringtypeindex__last) and (element(
           trimmed_name__1, [rr_type__wirestringtypeindex__first]) <> 0)) and (
           new_qname_location__1 <= output_bytes__2))) .
H108:  answer_count__2 >= dns_types__unsigned_short__first .
H109:  answer_count__2 <= dns_types__unsigned_short__last .
H110:  answer_count__2 >= 1 .
H111:  answer_count__2 >= dns_types__unsigned_short__first .
H112:  answer_count__2 <= dns_types__unsigned_short__last .
H113:  answer_count__2 >= dns_types__unsigned_short__first .
H114:  answer_count__2 <= dns_types__unsigned_short__last .
        ->
C1:    output_bytes__2 >= dns_types__header_bits div 8 + 1 .
C2:    output_bytes__2 <= dns_types__packet_size .
 

procedure_create_nxdomain_response_22.
H1:    answer_count = 0 .
H2:    amount_trimmed >= 0 .
H3:    amount_trimmed < rr_type__wirestringtypeindex__last .
H4:    output_bytes <= dns_types__packet_length_range__last .
H5:    current_qname_location <= output_bytes .
H6:    start_byte >= dns_types__packet_bytes_range__first .
H7:    start_byte <= dns_types__packet_bytes_range__last .
H8:    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))) .
H9:    qname_location >= dns_types__qname_ptr_range__first .
H10:   qname_location <= dns_types__qname_ptr_range__last .
H11:   fld_messageid(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H12:   fld_messageid(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H13:   fld_opcode(fld_header(output_packet)) >= 
           dns_types__opcode_type__first .
H14:   fld_opcode(fld_header(output_packet)) <= 
           dns_types__opcode_type__last .
H15:   fld_rcode(fld_header(output_packet)) >= 
           dns_types__response_code__first .
H16:   fld_rcode(fld_header(output_packet)) <= 
           dns_types__response_code__last .
H17:   fld_qdcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H18:   fld_qdcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H19:   fld_ancount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H20:   fld_ancount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H21:   fld_nscount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H22:   fld_nscount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H23:   fld_arcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H24:   fld_arcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H25:   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))) .
H26:   start_byte <= dns_types__packet_size .
H27:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           current_name, [i___1]) >= character__first) and (element(
           current_name, [i___1]) <= character__last))) .
H28:   current_qname_location >= dns_types__qname_ptr_range__first .
H29:   current_qname_location <= dns_types__qname_ptr_range__last .
H30:   current_qname_location >= dns_types__qname_ptr_range__first .
H31:   current_qname_location <= dns_types__qname_ptr_range__last .
H32:   current_qname_location <= 
           dns_types__packet_length_range__last .
H33:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           trimmed_name__1, [i___1]) >= character__first) and (element(
           trimmed_name__1, [i___1]) <= character__last))) .
H34:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H35:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
H36:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H37:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
H38:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           trimmed_name__1, [i___1]) >= character__first) and (element(
           trimmed_name__1, [i___1]) <= character__last))) .
H39:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H40:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
H41:   answer_count >= dns_types__unsigned_short__first .
H42:   answer_count <= dns_types__unsigned_short__last .
H43:   answer_count >= dns_types__unsigned_short__first .
H44:   answer_count <= dns_types__unsigned_short__last .
H45:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H46:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
H47:   start_byte >= dns_types__packet_bytes_range__first .
H48:   start_byte <= dns_types__packet_bytes_range__last .
H49:   start_byte <= dns_types__packet_size .
H50:   answer_count <= dns_types__unsigned_short__last - 
           rr_type__maxnumrecords .
H51:   output_bytes__2 >= dns_types__header_bits div 8 + 1 .
H52:   output_bytes__2 <= dns_types__packet_size .
H53:   answer_count__2 <= answer_count + 
           rr_type__maxnumrecords .
H54:   fld_messageid(fld_header(output_packet__2)) >= 
           dns_types__unsigned_short__first .
H55:   fld_messageid(fld_header(output_packet__2)) <= 
           dns_types__unsigned_short__last .
H56:   fld_opcode(fld_header(output_packet__2)) >= 
           dns_types__opcode_type__first .
H57:   fld_opcode(fld_header(output_packet__2)) <= 
           dns_types__opcode_type__last .
H58:   fld_rcode(fld_header(output_packet__2)) >= 
           dns_types__response_code__first .
H59:   fld_rcode(fld_header(output_packet__2)) <= 
           dns_types__response_code__last .
H60:   fld_qdcount(fld_header(output_packet__2)) >= 
           dns_types__unsigned_short__first .
H61:   fld_qdcount(fld_header(output_packet__2)) <= 
           dns_types__unsigned_short__last .
H62:   fld_ancount(fld_header(output_packet__2)) >= 
           dns_types__unsigned_short__first .
H63:   fld_ancount(fld_header(output_packet__2)) <= 
           dns_types__unsigned_short__last .
H64:   fld_nscount(fld_header(output_packet__2)) >= 
           dns_types__unsigned_short__first .
H65:   fld_nscount(fld_header(output_packet__2)) <= 
           dns_types__unsigned_short__last .
H66:   fld_arcount(fld_header(output_packet__2)) >= 
           dns_types__unsigned_short__first .
H67:   fld_arcount(fld_header(output_packet__2)) <= 
           dns_types__unsigned_short__last .
H68:   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))) .
H69:   answer_count__2 >= dns_types__unsigned_short__first .
H70:   answer_count__2 <= dns_types__unsigned_short__last .
H71:   output_bytes__2 >= dns_types__packet_length_range__first .
H72:   output_bytes__2 <= dns_types__packet_length_range__last .
H73:   output_bytes__2 >= dns_types__packet_length_range__first .
H74:   output_bytes__2 <= dns_types__packet_length_range__last .
H75:   answer_count__2 >= dns_types__unsigned_short__first .
H76:   answer_count__2 <= dns_types__unsigned_short__last .
H77:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           trimmed_name__1, [i___1]) >= character__first) and (element(
           trimmed_name__1, [i___1]) <= character__last))) .
H78:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H79:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
H80:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H81:   new_qname_location__1 <= dns_types__qname_ptr_range__last .
H82:   amount_trimmed >= natural__first .
H83:   amount_trimmed <= natural__last .
H84:   amount_trimmed + (element(domainname, [
           rr_type__wirestringtypeindex__first]) + 1) >= 
           natural__first .
H85:   amount_trimmed + (element(domainname, [
           rr_type__wirestringtypeindex__first]) + 1) <= 
           natural__last .
H86:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= 
           natural__first .
H87:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= 
           natural__last .
H88:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 >= system__min_int .
H89:   element(domainname, [rr_type__wirestringtypeindex__first]) + 1 <= system__max_int .
H90:   rr_type__wirestringtypeindex__first >= 
           rr_type__wirestringtypeindex__first .
H91:   rr_type__wirestringtypeindex__first <= 
           rr_type__wirestringtypeindex__last .
H92:   output_bytes__2 >= dns_types__packet_length_range__first .
H93:   output_bytes__2 <= dns_types__packet_length_range__last .
H94:   answer_count__2 >= dns_types__unsigned_short__first .
H95:   answer_count__2 <= dns_types__unsigned_short__last .
H96:   amount_trimmed + (element(domainname, [
           rr_type__wirestringtypeindex__first]) + 1) >= 
           natural__first .
H97:   amount_trimmed + (element(domainname, [
           rr_type__wirestringtypeindex__first]) + 1) <= 
           natural__last .
H98:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           trimmed_name__1, [i___1]) >= character__first) and (element(
           trimmed_name__1, [i___1]) <= character__last))) .
H99:   new_qname_location__1 >= dns_types__qname_ptr_range__first .
H100:  new_qname_location__1 <= dns_types__qname_ptr_range__last .
H101:  output_bytes__2 >= dns_types__qname_ptr_range__first .
H102:  output_bytes__2 <= dns_types__qname_ptr_range__last .
H103:  element(trimmed_name__1, [rr_type__wirestringtypeindex__first]) >= 
           natural__first .
H104:  element(trimmed_name__1, [rr_type__wirestringtypeindex__first]) <= 
           natural__last .
H105:  rr_type__wirestringtypeindex__first >= 
           rr_type__wirestringtypeindex__first .
H106:  rr_type__wirestringtypeindex__first <= 
           rr_type__wirestringtypeindex__last .
H107:  not ((answer_count__2 = 0) and (((amount_trimmed + (element(
           domainname, [rr_type__wirestringtypeindex__first]) + 1) < 
           rr_type__wirestringtypeindex__last) and (element(
           trimmed_name__1, [rr_type__wirestringtypeindex__first]) <> 0)) and (
           new_qname_location__1 <= output_bytes__2))) .
H108:  answer_count__2 >= dns_types__unsigned_short__first .
H109:  answer_count__2 <= dns_types__unsigned_short__last .
H110:  not (answer_count__2 >= 1) .
H111:  answer_count__2 >= dns_types__unsigned_short__first .
H112:  answer_count__2 <= dns_types__unsigned_short__last .
H113:  answer_count__2 >= dns_types__unsigned_short__first .
H114:  answer_count__2 <= dns_types__unsigned_short__last .
        ->
C1:    output_bytes__2 >= dns_types__header_bits div 8 + 1 .
C2:    output_bytes__2 <= dns_types__packet_size .
 

