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

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


                   task_type Udp_Dns_Package.Udp_Dns_Task




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

task_type_udp_dns_task_1.
H1:    true .
        ->
C1:    0 >= dns_types__byte__first .
C2:    0 <= dns_types__byte__last .
 

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

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


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

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


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


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


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

task_type_udp_dns_task_6.
H1:    true .
H2:    (not failure__3) -> ((input_bytes__3 >= 1 + 
           dns_types__header_bits div 8) and (input_bytes__3 <= 
           dns_network__max_query_size)) .
H3:    fld_messageid(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H4:    fld_messageid(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H5:    fld_opcode(fld_header(input_packet__3)) >= 
           dns_types__opcode_type__first .
H6:    fld_opcode(fld_header(input_packet__3)) <= 
           dns_types__opcode_type__last .
H7:    fld_rcode(fld_header(input_packet__3)) >= 
           dns_types__response_code__first .
H8:    fld_rcode(fld_header(input_packet__3)) <= 
           dns_types__response_code__last .
H9:    fld_qdcount(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H10:   fld_qdcount(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H11:   fld_ancount(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H12:   fld_ancount(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H13:   fld_nscount(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H14:   fld_nscount(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H15:   fld_arcount(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H16:   fld_arcount(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H17:   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(input_packet__3), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           input_packet__3), [i___1]) <= dns_types__byte__last))) .
H18:   input_bytes__3 >= dns_types__packet_length_range__first .
H19:   input_bytes__3 <= dns_types__packet_length_range__last .
        ->
C1:    input_bytes__3 >= dns_types__packet_length_range__first .
C2:    input_bytes__3 <= dns_types__packet_length_range__last .
 

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

task_type_udp_dns_task_7.
H1:    true .
H2:    (not failure__3) -> ((input_bytes__3 >= 1 + 
           dns_types__header_bits div 8) and (input_bytes__3 <= 
           dns_network__max_query_size)) .
H3:    fld_messageid(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H4:    fld_messageid(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H5:    fld_opcode(fld_header(input_packet__3)) >= 
           dns_types__opcode_type__first .
H6:    fld_opcode(fld_header(input_packet__3)) <= 
           dns_types__opcode_type__last .
H7:    fld_rcode(fld_header(input_packet__3)) >= 
           dns_types__response_code__first .
H8:    fld_rcode(fld_header(input_packet__3)) <= 
           dns_types__response_code__last .
H9:    fld_qdcount(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H10:   fld_qdcount(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H11:   fld_ancount(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H12:   fld_ancount(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H13:   fld_nscount(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H14:   fld_nscount(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H15:   fld_arcount(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H16:   fld_arcount(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H17:   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(input_packet__3), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           input_packet__3), [i___1]) <= dns_types__byte__last))) .
H18:   input_bytes__3 >= dns_types__packet_length_range__first .
H19:   input_bytes__3 <= dns_types__packet_length_range__last .
H20:   input_bytes__3 >= dns_types__packet_length_range__first .
H21:   input_bytes__3 <= dns_types__packet_length_range__last .
H22:   true .
H23:   failure__3 .
H24:   true .
        ->
C1:    0 >= natural__first .
C2:    0 <= natural__last .
 

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

task_type_udp_dns_task_8.
H1:    true .
H2:    (not failure__3) -> ((input_bytes__3 >= 1 + 
           dns_types__header_bits div 8) and (input_bytes__3 <= 
           dns_network__max_query_size)) .
H3:    fld_messageid(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H4:    fld_messageid(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H5:    fld_opcode(fld_header(input_packet__3)) >= 
           dns_types__opcode_type__first .
H6:    fld_opcode(fld_header(input_packet__3)) <= 
           dns_types__opcode_type__last .
H7:    fld_rcode(fld_header(input_packet__3)) >= 
           dns_types__response_code__first .
H8:    fld_rcode(fld_header(input_packet__3)) <= 
           dns_types__response_code__last .
H9:    fld_qdcount(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H10:   fld_qdcount(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H11:   fld_ancount(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H12:   fld_ancount(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H13:   fld_nscount(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H14:   fld_nscount(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H15:   fld_arcount(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H16:   fld_arcount(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H17:   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(input_packet__3), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           input_packet__3), [i___1]) <= dns_types__byte__last))) .
H18:   input_bytes__3 >= dns_types__packet_length_range__first .
H19:   input_bytes__3 <= dns_types__packet_length_range__last .
H20:   input_bytes__3 >= dns_types__packet_length_range__first .
H21:   input_bytes__3 <= dns_types__packet_length_range__last .
H22:   true .
H23:   not failure__3 .
H24:   fld_messageid(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H25:   fld_messageid(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H26:   fld_opcode(fld_header(input_packet__3)) >= 
           dns_types__opcode_type__first .
H27:   fld_opcode(fld_header(input_packet__3)) <= 
           dns_types__opcode_type__last .
H28:   fld_rcode(fld_header(input_packet__3)) >= 
           dns_types__response_code__first .
H29:   fld_rcode(fld_header(input_packet__3)) <= 
           dns_types__response_code__last .
H30:   fld_qdcount(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H31:   fld_qdcount(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H32:   fld_ancount(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H33:   fld_ancount(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H34:   fld_nscount(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H35:   fld_nscount(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H36:   fld_arcount(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H37:   fld_arcount(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H38:   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(input_packet__3), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           input_packet__3), [i___1]) <= dns_types__byte__last))) .
H39:   input_bytes__3 >= dns_types__packet_length_range__first .
H40:   input_bytes__3 <= dns_types__packet_length_range__last .
H41:   fld_messageid(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H42:   fld_messageid(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H43:   fld_opcode(fld_header(output_packet)) >= 
           dns_types__opcode_type__first .
H44:   fld_opcode(fld_header(output_packet)) <= 
           dns_types__opcode_type__last .
H45:   fld_rcode(fld_header(output_packet)) >= 
           dns_types__response_code__first .
H46:   fld_rcode(fld_header(output_packet)) <= 
           dns_types__response_code__last .
H47:   fld_qdcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H48:   fld_qdcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H49:   fld_ancount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H50:   fld_ancount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H51:   fld_nscount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H52:   fld_nscount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H53:   fld_arcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H54:   fld_arcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H55:   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:    input_bytes__3 >= dns_types__packet_length_range__first .
C2:    input_bytes__3 <= dns_types__packet_length_range__last .
C3:    input_bytes__3 >= dns_types__header_bits div 8 + 1 .
C4:    input_bytes__3 < 312 .
 

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

task_type_udp_dns_task_9.
H1:    true .
H2:    (not failure__3) -> ((input_bytes__3 >= 1 + 
           dns_types__header_bits div 8) and (input_bytes__3 <= 
           dns_network__max_query_size)) .
H3:    fld_messageid(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H4:    fld_messageid(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H5:    fld_opcode(fld_header(input_packet__3)) >= 
           dns_types__opcode_type__first .
H6:    fld_opcode(fld_header(input_packet__3)) <= 
           dns_types__opcode_type__last .
H7:    fld_rcode(fld_header(input_packet__3)) >= 
           dns_types__response_code__first .
H8:    fld_rcode(fld_header(input_packet__3)) <= 
           dns_types__response_code__last .
H9:    fld_qdcount(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H10:   fld_qdcount(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H11:   fld_ancount(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H12:   fld_ancount(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H13:   fld_nscount(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H14:   fld_nscount(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H15:   fld_arcount(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H16:   fld_arcount(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H17:   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(input_packet__3), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           input_packet__3), [i___1]) <= dns_types__byte__last))) .
H18:   input_bytes__3 >= dns_types__packet_length_range__first .
H19:   input_bytes__3 <= dns_types__packet_length_range__last .
H20:   input_bytes__3 >= dns_types__packet_length_range__first .
H21:   input_bytes__3 <= dns_types__packet_length_range__last .
H22:   true .
H23:   not failure__3 .
H24:   fld_messageid(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H25:   fld_messageid(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H26:   fld_opcode(fld_header(input_packet__3)) >= 
           dns_types__opcode_type__first .
H27:   fld_opcode(fld_header(input_packet__3)) <= 
           dns_types__opcode_type__last .
H28:   fld_rcode(fld_header(input_packet__3)) >= 
           dns_types__response_code__first .
H29:   fld_rcode(fld_header(input_packet__3)) <= 
           dns_types__response_code__last .
H30:   fld_qdcount(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H31:   fld_qdcount(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H32:   fld_ancount(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H33:   fld_ancount(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H34:   fld_nscount(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H35:   fld_nscount(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H36:   fld_arcount(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H37:   fld_arcount(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H38:   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(input_packet__3), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           input_packet__3), [i___1]) <= dns_types__byte__last))) .
H39:   input_bytes__3 >= dns_types__packet_length_range__first .
H40:   input_bytes__3 <= dns_types__packet_length_range__last .
H41:   fld_messageid(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H42:   fld_messageid(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H43:   fld_opcode(fld_header(output_packet)) >= 
           dns_types__opcode_type__first .
H44:   fld_opcode(fld_header(output_packet)) <= 
           dns_types__opcode_type__last .
H45:   fld_rcode(fld_header(output_packet)) >= 
           dns_types__response_code__first .
H46:   fld_rcode(fld_header(output_packet)) <= 
           dns_types__response_code__last .
H47:   fld_qdcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H48:   fld_qdcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H49:   fld_ancount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H50:   fld_ancount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H51:   fld_nscount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H52:   fld_nscount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H53:   fld_arcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H54:   fld_arcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H55:   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))) .
H56:   input_bytes__3 >= dns_types__packet_length_range__first .
H57:   input_bytes__3 <= dns_types__packet_length_range__last .
H58:   input_bytes__3 >= dns_types__header_bits div 8 + 1 .
H59:   input_bytes__3 < 312 .
H60:   output_bytes__5 >= dns_types__header_bits div 8 + 1 .
H61:   output_bytes__5 <= dns_types__packet_size .
H62:   max_transmit__5 <= dns_types__packet_size .
H63:   max_transmit__5 >= dns_types__udp_max_size .
H64:   fld_messageid(fld_header(output_packet__5)) >= 
           dns_types__unsigned_short__first .
H65:   fld_messageid(fld_header(output_packet__5)) <= 
           dns_types__unsigned_short__last .
H66:   fld_opcode(fld_header(output_packet__5)) >= 
           dns_types__opcode_type__first .
H67:   fld_opcode(fld_header(output_packet__5)) <= 
           dns_types__opcode_type__last .
H68:   fld_rcode(fld_header(output_packet__5)) >= 
           dns_types__response_code__first .
H69:   fld_rcode(fld_header(output_packet__5)) <= 
           dns_types__response_code__last .
H70:   fld_qdcount(fld_header(output_packet__5)) >= 
           dns_types__unsigned_short__first .
H71:   fld_qdcount(fld_header(output_packet__5)) <= 
           dns_types__unsigned_short__last .
H72:   fld_ancount(fld_header(output_packet__5)) >= 
           dns_types__unsigned_short__first .
H73:   fld_ancount(fld_header(output_packet__5)) <= 
           dns_types__unsigned_short__last .
H74:   fld_nscount(fld_header(output_packet__5)) >= 
           dns_types__unsigned_short__first .
H75:   fld_nscount(fld_header(output_packet__5)) <= 
           dns_types__unsigned_short__last .
H76:   fld_arcount(fld_header(output_packet__5)) >= 
           dns_types__unsigned_short__first .
H77:   fld_arcount(fld_header(output_packet__5)) <= 
           dns_types__unsigned_short__last .
H78:   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__5), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           output_packet__5), [i___1]) <= dns_types__byte__last))) .
H79:   output_bytes__5 >= dns_types__packet_length_range__first .
H80:   output_bytes__5 <= dns_types__packet_length_range__last .
H81:   max_transmit__5 >= dns_types__packet_length_range__first .
H82:   max_transmit__5 <= dns_types__packet_length_range__last .
        ->
C1:    max_transmit__5 >= dns_types__packet_length_range__first .
C2:    max_transmit__5 <= dns_types__packet_length_range__last .
C3:    output_bytes__5 >= dns_types__packet_length_range__first .
C4:    output_bytes__5 <= dns_types__packet_length_range__last .
 

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

task_type_udp_dns_task_10.
H1:    true .
H2:    (not failure__3) -> ((input_bytes__3 >= 1 + 
           dns_types__header_bits div 8) and (input_bytes__3 <= 
           dns_network__max_query_size)) .
H3:    fld_messageid(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H4:    fld_messageid(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H5:    fld_opcode(fld_header(input_packet__3)) >= 
           dns_types__opcode_type__first .
H6:    fld_opcode(fld_header(input_packet__3)) <= 
           dns_types__opcode_type__last .
H7:    fld_rcode(fld_header(input_packet__3)) >= 
           dns_types__response_code__first .
H8:    fld_rcode(fld_header(input_packet__3)) <= 
           dns_types__response_code__last .
H9:    fld_qdcount(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H10:   fld_qdcount(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H11:   fld_ancount(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H12:   fld_ancount(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H13:   fld_nscount(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H14:   fld_nscount(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H15:   fld_arcount(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H16:   fld_arcount(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H17:   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(input_packet__3), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           input_packet__3), [i___1]) <= dns_types__byte__last))) .
H18:   input_bytes__3 >= dns_types__packet_length_range__first .
H19:   input_bytes__3 <= dns_types__packet_length_range__last .
H20:   input_bytes__3 >= dns_types__packet_length_range__first .
H21:   input_bytes__3 <= dns_types__packet_length_range__last .
H22:   true .
H23:   not failure__3 .
H24:   fld_messageid(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H25:   fld_messageid(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H26:   fld_opcode(fld_header(input_packet__3)) >= 
           dns_types__opcode_type__first .
H27:   fld_opcode(fld_header(input_packet__3)) <= 
           dns_types__opcode_type__last .
H28:   fld_rcode(fld_header(input_packet__3)) >= 
           dns_types__response_code__first .
H29:   fld_rcode(fld_header(input_packet__3)) <= 
           dns_types__response_code__last .
H30:   fld_qdcount(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H31:   fld_qdcount(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H32:   fld_ancount(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H33:   fld_ancount(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H34:   fld_nscount(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H35:   fld_nscount(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H36:   fld_arcount(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H37:   fld_arcount(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H38:   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(input_packet__3), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           input_packet__3), [i___1]) <= dns_types__byte__last))) .
H39:   input_bytes__3 >= dns_types__packet_length_range__first .
H40:   input_bytes__3 <= dns_types__packet_length_range__last .
H41:   fld_messageid(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H42:   fld_messageid(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H43:   fld_opcode(fld_header(output_packet)) >= 
           dns_types__opcode_type__first .
H44:   fld_opcode(fld_header(output_packet)) <= 
           dns_types__opcode_type__last .
H45:   fld_rcode(fld_header(output_packet)) >= 
           dns_types__response_code__first .
H46:   fld_rcode(fld_header(output_packet)) <= 
           dns_types__response_code__last .
H47:   fld_qdcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H48:   fld_qdcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H49:   fld_ancount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H50:   fld_ancount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H51:   fld_nscount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H52:   fld_nscount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H53:   fld_arcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H54:   fld_arcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H55:   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))) .
H56:   input_bytes__3 >= dns_types__packet_length_range__first .
H57:   input_bytes__3 <= dns_types__packet_length_range__last .
H58:   input_bytes__3 >= dns_types__header_bits div 8 + 1 .
H59:   input_bytes__3 < 312 .
H60:   output_bytes__5 >= dns_types__header_bits div 8 + 1 .
H61:   output_bytes__5 <= dns_types__packet_size .
H62:   max_transmit__5 <= dns_types__packet_size .
H63:   max_transmit__5 >= dns_types__udp_max_size .
H64:   fld_messageid(fld_header(output_packet__5)) >= 
           dns_types__unsigned_short__first .
H65:   fld_messageid(fld_header(output_packet__5)) <= 
           dns_types__unsigned_short__last .
H66:   fld_opcode(fld_header(output_packet__5)) >= 
           dns_types__opcode_type__first .
H67:   fld_opcode(fld_header(output_packet__5)) <= 
           dns_types__opcode_type__last .
H68:   fld_rcode(fld_header(output_packet__5)) >= 
           dns_types__response_code__first .
H69:   fld_rcode(fld_header(output_packet__5)) <= 
           dns_types__response_code__last .
H70:   fld_qdcount(fld_header(output_packet__5)) >= 
           dns_types__unsigned_short__first .
H71:   fld_qdcount(fld_header(output_packet__5)) <= 
           dns_types__unsigned_short__last .
H72:   fld_ancount(fld_header(output_packet__5)) >= 
           dns_types__unsigned_short__first .
H73:   fld_ancount(fld_header(output_packet__5)) <= 
           dns_types__unsigned_short__last .
H74:   fld_nscount(fld_header(output_packet__5)) >= 
           dns_types__unsigned_short__first .
H75:   fld_nscount(fld_header(output_packet__5)) <= 
           dns_types__unsigned_short__last .
H76:   fld_arcount(fld_header(output_packet__5)) >= 
           dns_types__unsigned_short__first .
H77:   fld_arcount(fld_header(output_packet__5)) <= 
           dns_types__unsigned_short__last .
H78:   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__5), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           output_packet__5), [i___1]) <= dns_types__byte__last))) .
H79:   output_bytes__5 >= dns_types__packet_length_range__first .
H80:   output_bytes__5 <= dns_types__packet_length_range__last .
H81:   max_transmit__5 >= dns_types__packet_length_range__first .
H82:   max_transmit__5 <= dns_types__packet_length_range__last .
H83:   max_transmit__5 >= dns_types__packet_length_range__first .
H84:   max_transmit__5 <= dns_types__packet_length_range__last .
H85:   output_bytes__5 >= dns_types__packet_length_range__first .
H86:   output_bytes__5 <= dns_types__packet_length_range__last .
H87:   output_bytes__5 >= dns_types__packet_length_range__first .
H88:   output_bytes__5 <= dns_types__packet_length_range__last .
H89:   max_transmit__5 >= dns_types__packet_length_range__first .
H90:   max_transmit__5 <= dns_types__packet_length_range__last .
        ->
C1:    dns_types__packet_length_range__min(max_transmit__5, 
           output_bytes__5) >= dns_types__packet_length_range__first .
C2:    dns_types__packet_length_range__min(max_transmit__5, 
           output_bytes__5) <= dns_types__packet_length_range__last .
 

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

task_type_udp_dns_task_11.
H1:    true .
H2:    (not failure__3) -> ((input_bytes__3 >= 1 + 
           dns_types__header_bits div 8) and (input_bytes__3 <= 
           dns_network__max_query_size)) .
H3:    fld_messageid(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H4:    fld_messageid(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H5:    fld_opcode(fld_header(input_packet__3)) >= 
           dns_types__opcode_type__first .
H6:    fld_opcode(fld_header(input_packet__3)) <= 
           dns_types__opcode_type__last .
H7:    fld_rcode(fld_header(input_packet__3)) >= 
           dns_types__response_code__first .
H8:    fld_rcode(fld_header(input_packet__3)) <= 
           dns_types__response_code__last .
H9:    fld_qdcount(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H10:   fld_qdcount(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H11:   fld_ancount(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H12:   fld_ancount(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H13:   fld_nscount(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H14:   fld_nscount(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H15:   fld_arcount(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H16:   fld_arcount(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H17:   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(input_packet__3), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           input_packet__3), [i___1]) <= dns_types__byte__last))) .
H18:   input_bytes__3 >= dns_types__packet_length_range__first .
H19:   input_bytes__3 <= dns_types__packet_length_range__last .
H20:   input_bytes__3 >= dns_types__packet_length_range__first .
H21:   input_bytes__3 <= dns_types__packet_length_range__last .
H22:   true .
H23:   not failure__3 .
H24:   fld_messageid(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H25:   fld_messageid(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H26:   fld_opcode(fld_header(input_packet__3)) >= 
           dns_types__opcode_type__first .
H27:   fld_opcode(fld_header(input_packet__3)) <= 
           dns_types__opcode_type__last .
H28:   fld_rcode(fld_header(input_packet__3)) >= 
           dns_types__response_code__first .
H29:   fld_rcode(fld_header(input_packet__3)) <= 
           dns_types__response_code__last .
H30:   fld_qdcount(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H31:   fld_qdcount(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H32:   fld_ancount(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H33:   fld_ancount(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H34:   fld_nscount(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H35:   fld_nscount(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H36:   fld_arcount(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H37:   fld_arcount(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H38:   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(input_packet__3), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           input_packet__3), [i___1]) <= dns_types__byte__last))) .
H39:   input_bytes__3 >= dns_types__packet_length_range__first .
H40:   input_bytes__3 <= dns_types__packet_length_range__last .
H41:   fld_messageid(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H42:   fld_messageid(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H43:   fld_opcode(fld_header(output_packet)) >= 
           dns_types__opcode_type__first .
H44:   fld_opcode(fld_header(output_packet)) <= 
           dns_types__opcode_type__last .
H45:   fld_rcode(fld_header(output_packet)) >= 
           dns_types__response_code__first .
H46:   fld_rcode(fld_header(output_packet)) <= 
           dns_types__response_code__last .
H47:   fld_qdcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H48:   fld_qdcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H49:   fld_ancount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H50:   fld_ancount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H51:   fld_nscount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H52:   fld_nscount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H53:   fld_arcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H54:   fld_arcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H55:   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))) .
H56:   input_bytes__3 >= dns_types__packet_length_range__first .
H57:   input_bytes__3 <= dns_types__packet_length_range__last .
H58:   input_bytes__3 >= dns_types__header_bits div 8 + 1 .
H59:   input_bytes__3 < 312 .
H60:   output_bytes__5 >= dns_types__header_bits div 8 + 1 .
H61:   output_bytes__5 <= dns_types__packet_size .
H62:   max_transmit__5 <= dns_types__packet_size .
H63:   max_transmit__5 >= dns_types__udp_max_size .
H64:   fld_messageid(fld_header(output_packet__5)) >= 
           dns_types__unsigned_short__first .
H65:   fld_messageid(fld_header(output_packet__5)) <= 
           dns_types__unsigned_short__last .
H66:   fld_opcode(fld_header(output_packet__5)) >= 
           dns_types__opcode_type__first .
H67:   fld_opcode(fld_header(output_packet__5)) <= 
           dns_types__opcode_type__last .
H68:   fld_rcode(fld_header(output_packet__5)) >= 
           dns_types__response_code__first .
H69:   fld_rcode(fld_header(output_packet__5)) <= 
           dns_types__response_code__last .
H70:   fld_qdcount(fld_header(output_packet__5)) >= 
           dns_types__unsigned_short__first .
H71:   fld_qdcount(fld_header(output_packet__5)) <= 
           dns_types__unsigned_short__last .
H72:   fld_ancount(fld_header(output_packet__5)) >= 
           dns_types__unsigned_short__first .
H73:   fld_ancount(fld_header(output_packet__5)) <= 
           dns_types__unsigned_short__last .
H74:   fld_nscount(fld_header(output_packet__5)) >= 
           dns_types__unsigned_short__first .
H75:   fld_nscount(fld_header(output_packet__5)) <= 
           dns_types__unsigned_short__last .
H76:   fld_arcount(fld_header(output_packet__5)) >= 
           dns_types__unsigned_short__first .
H77:   fld_arcount(fld_header(output_packet__5)) <= 
           dns_types__unsigned_short__last .
H78:   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__5), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           output_packet__5), [i___1]) <= dns_types__byte__last))) .
H79:   output_bytes__5 >= dns_types__packet_length_range__first .
H80:   output_bytes__5 <= dns_types__packet_length_range__last .
H81:   max_transmit__5 >= dns_types__packet_length_range__first .
H82:   max_transmit__5 <= dns_types__packet_length_range__last .
H83:   max_transmit__5 >= dns_types__packet_length_range__first .
H84:   max_transmit__5 <= dns_types__packet_length_range__last .
H85:   output_bytes__5 >= dns_types__packet_length_range__first .
H86:   output_bytes__5 <= dns_types__packet_length_range__last .
H87:   output_bytes__5 >= dns_types__packet_length_range__first .
H88:   output_bytes__5 <= dns_types__packet_length_range__last .
H89:   max_transmit__5 >= dns_types__packet_length_range__first .
H90:   max_transmit__5 <= dns_types__packet_length_range__last .
H91:   dns_types__packet_length_range__min(max_transmit__5, 
           output_bytes__5) >= dns_types__packet_length_range__first .
H92:   dns_types__packet_length_range__min(max_transmit__5, 
           output_bytes__5) <= dns_types__packet_length_range__last .
H93:   fld_messageid(fld_header(output_packet__5)) >= 
           dns_types__unsigned_short__first .
H94:   fld_messageid(fld_header(output_packet__5)) <= 
           dns_types__unsigned_short__last .
H95:   fld_opcode(fld_header(output_packet__5)) >= 
           dns_types__opcode_type__first .
H96:   fld_opcode(fld_header(output_packet__5)) <= 
           dns_types__opcode_type__last .
H97:   fld_rcode(fld_header(output_packet__5)) >= 
           dns_types__response_code__first .
H98:   fld_rcode(fld_header(output_packet__5)) <= 
           dns_types__response_code__last .
H99:   fld_qdcount(fld_header(output_packet__5)) >= 
           dns_types__unsigned_short__first .
H100:  fld_qdcount(fld_header(output_packet__5)) <= 
           dns_types__unsigned_short__last .
H101:  fld_ancount(fld_header(output_packet__5)) >= 
           dns_types__unsigned_short__first .
H102:  fld_ancount(fld_header(output_packet__5)) <= 
           dns_types__unsigned_short__last .
H103:  fld_nscount(fld_header(output_packet__5)) >= 
           dns_types__unsigned_short__first .
H104:  fld_nscount(fld_header(output_packet__5)) <= 
           dns_types__unsigned_short__last .
H105:  fld_arcount(fld_header(output_packet__5)) >= 
           dns_types__unsigned_short__first .
H106:  fld_arcount(fld_header(output_packet__5)) <= 
           dns_types__unsigned_short__last .
H107:  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__5), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           output_packet__5), [i___1]) <= dns_types__byte__last))) .
H108:  dns_types__packet_length_range__min(max_transmit__5, 
           output_bytes__5) >= dns_types__packet_length_range__first .
H109:  dns_types__packet_length_range__min(max_transmit__5, 
           output_bytes__5) <= dns_types__packet_length_range__last .
H110:  true .
        ->
C1:    dns_types__packet_length_range__min(max_transmit__5, 
           output_bytes__5) >= dns_types__packet_length_range__first .
C2:    dns_types__packet_length_range__min(max_transmit__5, 
           output_bytes__5) <= dns_types__packet_length_range__last .
C3:    dns_types__packet_length_range__min(max_transmit__5, 
           output_bytes__5) > dns_types__header_bits div 8 .
 

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

task_type_udp_dns_task_12.
H1:    true .
H2:    (not failure__3) -> ((input_bytes__3 >= 1 + 
           dns_types__header_bits div 8) and (input_bytes__3 <= 
           dns_network__max_query_size)) .
H3:    fld_messageid(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H4:    fld_messageid(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H5:    fld_opcode(fld_header(input_packet__3)) >= 
           dns_types__opcode_type__first .
H6:    fld_opcode(fld_header(input_packet__3)) <= 
           dns_types__opcode_type__last .
H7:    fld_rcode(fld_header(input_packet__3)) >= 
           dns_types__response_code__first .
H8:    fld_rcode(fld_header(input_packet__3)) <= 
           dns_types__response_code__last .
H9:    fld_qdcount(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H10:   fld_qdcount(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H11:   fld_ancount(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H12:   fld_ancount(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H13:   fld_nscount(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H14:   fld_nscount(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H15:   fld_arcount(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H16:   fld_arcount(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H17:   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(input_packet__3), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           input_packet__3), [i___1]) <= dns_types__byte__last))) .
H18:   input_bytes__3 >= dns_types__packet_length_range__first .
H19:   input_bytes__3 <= dns_types__packet_length_range__last .
H20:   input_bytes__3 >= dns_types__packet_length_range__first .
H21:   input_bytes__3 <= dns_types__packet_length_range__last .
H22:   true .
H23:   not failure__3 .
H24:   fld_messageid(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H25:   fld_messageid(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H26:   fld_opcode(fld_header(input_packet__3)) >= 
           dns_types__opcode_type__first .
H27:   fld_opcode(fld_header(input_packet__3)) <= 
           dns_types__opcode_type__last .
H28:   fld_rcode(fld_header(input_packet__3)) >= 
           dns_types__response_code__first .
H29:   fld_rcode(fld_header(input_packet__3)) <= 
           dns_types__response_code__last .
H30:   fld_qdcount(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H31:   fld_qdcount(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H32:   fld_ancount(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H33:   fld_ancount(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H34:   fld_nscount(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H35:   fld_nscount(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H36:   fld_arcount(fld_header(input_packet__3)) >= 
           dns_types__unsigned_short__first .
H37:   fld_arcount(fld_header(input_packet__3)) <= 
           dns_types__unsigned_short__last .
H38:   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(input_packet__3), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           input_packet__3), [i___1]) <= dns_types__byte__last))) .
H39:   input_bytes__3 >= dns_types__packet_length_range__first .
H40:   input_bytes__3 <= dns_types__packet_length_range__last .
H41:   fld_messageid(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H42:   fld_messageid(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H43:   fld_opcode(fld_header(output_packet)) >= 
           dns_types__opcode_type__first .
H44:   fld_opcode(fld_header(output_packet)) <= 
           dns_types__opcode_type__last .
H45:   fld_rcode(fld_header(output_packet)) >= 
           dns_types__response_code__first .
H46:   fld_rcode(fld_header(output_packet)) <= 
           dns_types__response_code__last .
H47:   fld_qdcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H48:   fld_qdcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H49:   fld_ancount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H50:   fld_ancount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H51:   fld_nscount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H52:   fld_nscount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H53:   fld_arcount(fld_header(output_packet)) >= 
           dns_types__unsigned_short__first .
H54:   fld_arcount(fld_header(output_packet)) <= 
           dns_types__unsigned_short__last .
H55:   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))) .
H56:   input_bytes__3 >= dns_types__packet_length_range__first .
H57:   input_bytes__3 <= dns_types__packet_length_range__last .
H58:   input_bytes__3 >= dns_types__header_bits div 8 + 1 .
H59:   input_bytes__3 < 312 .
H60:   output_bytes__5 >= dns_types__header_bits div 8 + 1 .
H61:   output_bytes__5 <= dns_types__packet_size .
H62:   max_transmit__5 <= dns_types__packet_size .
H63:   max_transmit__5 >= dns_types__udp_max_size .
H64:   fld_messageid(fld_header(output_packet__5)) >= 
           dns_types__unsigned_short__first .
H65:   fld_messageid(fld_header(output_packet__5)) <= 
           dns_types__unsigned_short__last .
H66:   fld_opcode(fld_header(output_packet__5)) >= 
           dns_types__opcode_type__first .
H67:   fld_opcode(fld_header(output_packet__5)) <= 
           dns_types__opcode_type__last .
H68:   fld_rcode(fld_header(output_packet__5)) >= 
           dns_types__response_code__first .
H69:   fld_rcode(fld_header(output_packet__5)) <= 
           dns_types__response_code__last .
H70:   fld_qdcount(fld_header(output_packet__5)) >= 
           dns_types__unsigned_short__first .
H71:   fld_qdcount(fld_header(output_packet__5)) <= 
           dns_types__unsigned_short__last .
H72:   fld_ancount(fld_header(output_packet__5)) >= 
           dns_types__unsigned_short__first .
H73:   fld_ancount(fld_header(output_packet__5)) <= 
           dns_types__unsigned_short__last .
H74:   fld_nscount(fld_header(output_packet__5)) >= 
           dns_types__unsigned_short__first .
H75:   fld_nscount(fld_header(output_packet__5)) <= 
           dns_types__unsigned_short__last .
H76:   fld_arcount(fld_header(output_packet__5)) >= 
           dns_types__unsigned_short__first .
H77:   fld_arcount(fld_header(output_packet__5)) <= 
           dns_types__unsigned_short__last .
H78:   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__5), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           output_packet__5), [i___1]) <= dns_types__byte__last))) .
H79:   output_bytes__5 >= dns_types__packet_length_range__first .
H80:   output_bytes__5 <= dns_types__packet_length_range__last .
H81:   max_transmit__5 >= dns_types__packet_length_range__first .
H82:   max_transmit__5 <= dns_types__packet_length_range__last .
H83:   max_transmit__5 >= dns_types__packet_length_range__first .
H84:   max_transmit__5 <= dns_types__packet_length_range__last .
H85:   output_bytes__5 >= dns_types__packet_length_range__first .
H86:   output_bytes__5 <= dns_types__packet_length_range__last .
H87:   output_bytes__5 >= dns_types__packet_length_range__first .
H88:   output_bytes__5 <= dns_types__packet_length_range__last .
H89:   max_transmit__5 >= dns_types__packet_length_range__first .
H90:   max_transmit__5 <= dns_types__packet_length_range__last .
H91:   dns_types__packet_length_range__min(max_transmit__5, 
           output_bytes__5) >= dns_types__packet_length_range__first .
H92:   dns_types__packet_length_range__min(max_transmit__5, 
           output_bytes__5) <= dns_types__packet_length_range__last .
H93:   fld_messageid(fld_header(output_packet__5)) >= 
           dns_types__unsigned_short__first .
H94:   fld_messageid(fld_header(output_packet__5)) <= 
           dns_types__unsigned_short__last .
H95:   fld_opcode(fld_header(output_packet__5)) >= 
           dns_types__opcode_type__first .
H96:   fld_opcode(fld_header(output_packet__5)) <= 
           dns_types__opcode_type__last .
H97:   fld_rcode(fld_header(output_packet__5)) >= 
           dns_types__response_code__first .
H98:   fld_rcode(fld_header(output_packet__5)) <= 
           dns_types__response_code__last .
H99:   fld_qdcount(fld_header(output_packet__5)) >= 
           dns_types__unsigned_short__first .
H100:  fld_qdcount(fld_header(output_packet__5)) <= 
           dns_types__unsigned_short__last .
H101:  fld_ancount(fld_header(output_packet__5)) >= 
           dns_types__unsigned_short__first .
H102:  fld_ancount(fld_header(output_packet__5)) <= 
           dns_types__unsigned_short__last .
H103:  fld_nscount(fld_header(output_packet__5)) >= 
           dns_types__unsigned_short__first .
H104:  fld_nscount(fld_header(output_packet__5)) <= 
           dns_types__unsigned_short__last .
H105:  fld_arcount(fld_header(output_packet__5)) >= 
           dns_types__unsigned_short__first .
H106:  fld_arcount(fld_header(output_packet__5)) <= 
           dns_types__unsigned_short__last .
H107:  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__5), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           output_packet__5), [i___1]) <= dns_types__byte__last))) .
H108:  dns_types__packet_length_range__min(max_transmit__5, 
           output_bytes__5) >= dns_types__packet_length_range__first .
H109:  dns_types__packet_length_range__min(max_transmit__5, 
           output_bytes__5) <= dns_types__packet_length_range__last .
H110:  true .
H111:  dns_types__packet_length_range__min(max_transmit__5, 
           output_bytes__5) >= dns_types__packet_length_range__first .
H112:  dns_types__packet_length_range__min(max_transmit__5, 
           output_bytes__5) <= dns_types__packet_length_range__last .
H113:  dns_types__packet_length_range__min(max_transmit__5, 
           output_bytes__5) > dns_types__header_bits div 8 .
H114:  (system__default_bit_order = system__high_order_first) -> (
           output_packet__6 = output_packet__5) .
H115:  fld_messageid(fld_header(output_packet__6)) >= 
           dns_types__unsigned_short__first .
H116:  fld_messageid(fld_header(output_packet__6)) <= 
           dns_types__unsigned_short__last .
H117:  fld_opcode(fld_header(output_packet__6)) >= 
           dns_types__opcode_type__first .
H118:  fld_opcode(fld_header(output_packet__6)) <= 
           dns_types__opcode_type__last .
H119:  fld_rcode(fld_header(output_packet__6)) >= 
           dns_types__response_code__first .
H120:  fld_rcode(fld_header(output_packet__6)) <= 
           dns_types__response_code__last .
H121:  fld_qdcount(fld_header(output_packet__6)) >= 
           dns_types__unsigned_short__first .
H122:  fld_qdcount(fld_header(output_packet__6)) <= 
           dns_types__unsigned_short__last .
H123:  fld_ancount(fld_header(output_packet__6)) >= 
           dns_types__unsigned_short__first .
H124:  fld_ancount(fld_header(output_packet__6)) <= 
           dns_types__unsigned_short__last .
H125:  fld_nscount(fld_header(output_packet__6)) >= 
           dns_types__unsigned_short__first .
H126:  fld_nscount(fld_header(output_packet__6)) <= 
           dns_types__unsigned_short__last .
H127:  fld_arcount(fld_header(output_packet__6)) >= 
           dns_types__unsigned_short__first .
H128:  fld_arcount(fld_header(output_packet__6)) <= 
           dns_types__unsigned_short__last .
H129:  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__6), [i___1]) >= 
           dns_types__byte__first) and (element(fld_bytes(
           output_packet__6), [i___1]) <= dns_types__byte__last))) .
H130:  true .
H131:  failure__6 .
H132:  true .
        ->
C1:    0 >= natural__first .
C2:    0 <= natural__last .
 

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

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


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


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


