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

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



SPARK Simplifier GPL 2012
Copyright (C) 2012 Altran Praxis Limited, Bath, U.K.

procedure Process_Dns_Request.Set_TTL_Data_NSEC




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

procedure_set_ttl_data_nsec_1.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_nsec_2.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_nsec_3.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_nsec_4.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_nsec_5.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_nsec_6.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_nsec_7.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_nsec_8.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_nsec_9.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_nsec_10.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_nsec_11.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_nsec_12.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_nsec_13.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_nsec_14.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_nsec_15.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_nsec_16.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_nsec_17.
*** true .          /* all conclusions proved */


For path(s) from assertion of line 153 to assertion of line 164:

procedure_set_ttl_data_nsec_18.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_nsec_19.
*** true .   /* contradiction within hypotheses. */



For path(s) from assertion of line 176 to assertion of line 164:

procedure_set_ttl_data_nsec_20.
H1:    start_byte <= 8174 - current_name_length .
H2:    current_name_length >= 1 .
H3:    current_name_length <= 129 .
H4:    blockoffset >= 1 .
H5:    blockoffset <= start_byte + 6 - 1 + current_name_length + (
          loop__2__block__entry__loop__3 - 1) * 34 .
H6:    dstbytes <= loop__2__block__entry__loop__3 * 32 .
H7:    element(fld_blocklengths(nsec_record), [loop__2__block__entry__loop__3]) 
          >= 1 .
H8:    element(fld_blocklengths(nsec_record), [loop__2__block__entry__loop__3]) 
          <= 32 .
H9:    for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= element(
          bytes, [i___1]) and element(bytes, [i___1]) <= 255) .
H10:   start_byte >= 1 .
H11:   fld_ttlinseconds(fld_inherit(nsec_record)) >= 0 .
H12:   fld_ttlinseconds(fld_inherit(nsec_record)) <= 4294967295 .
H13:   rr_type__internet <= fld_class(fld_inherit(nsec_record)) .
H14:   fld_class(fld_inherit(nsec_record)) <= rr_type__hs .
H15:   for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <= element(
          fld_nextdomainname(nsec_record), [i___1]) and element(
          fld_nextdomainname(nsec_record), [i___1]) <= 255) .
H16:   for_all(i___2 : integer, 1 <= i___2 and i___2 <= 256 -> 0 <= element(
          fld_recordlist(nsec_record), [i___2]) and element(fld_recordlist(
          nsec_record), [i___2]) <= 255) .
H17:   fld_numberofrecordtypes(nsec_record) >= 0 .
H18:   fld_numberofrecordtypes(nsec_record) <= 32 .
H19:   for_all(i___3 : integer, 1 <= i___3 and i___3 <= 32 -> dns_types__a <= 
          element(fld_recordtypes(nsec_record), [i___3]) and element(
          fld_recordtypes(nsec_record), [i___3]) <= dns_types__unimplemented) .
H20:   fld_numberofblocks(nsec_record) >= 0 .
H21:   fld_numberofblocks(nsec_record) <= 32 .
H22:   for_all(i___4 : integer, 1 <= i___4 and i___4 <= 32 -> 0 <= element(
          fld_blocknumbers(nsec_record), [i___4]) and element(fld_blocknumbers(
          nsec_record), [i___4]) <= 255) .
H23:   for_all(i___5 : integer, 1 <= i___5 and i___5 <= 32 -> 1 <= element(
          fld_blocklengths(nsec_record), [i___5]) and element(fld_blocklengths(
          nsec_record), [i___5]) <= 32) .
H24:   for_all(i___6 : integer, 1 <= i___6 and i___6 <= 32 -> for_all(i___7 : 
          integer, 1 <= i___7 and i___7 <= 32 -> 0 <= element(element(
          fld_bitmaps(nsec_record), [i___6]), [i___7]) and element(element(
          fld_bitmaps(nsec_record), [i___6]), [i___7]) <= 255)) .
H25:   start_byte <= 6828 .
H26:   loop__2__block__entry__loop__3 >= 0 .
H27:   loop__2__block__entry__loop__3 <= 32 .
H28:   loop__2__block__entry__loop__3 <= 32 .
H29:   loop__2__block__entry__loop__3 >= 1 .
H30:   element(element(fld_bitmaps(nsec_record), [
          loop__2__block__entry__loop__3]), [element(fld_blocklengths(
          nsec_record), [loop__2__block__entry__loop__3])]) >= 0 .
H31:   element(element(fld_bitmaps(nsec_record), [
          loop__2__block__entry__loop__3]), [element(fld_blocklengths(
          nsec_record), [loop__2__block__entry__loop__3])]) <= 255 .
H32:   blockoffset + 2 + element(fld_blocklengths(nsec_record), [
          loop__2__block__entry__loop__3]) >= 1 .
H33:   blockoffset + 2 + element(fld_blocklengths(nsec_record), [
          loop__2__block__entry__loop__3]) <= 8180 .
H34:   blockoffset + 2 + element(fld_blocklengths(nsec_record), [
          loop__2__block__entry__loop__3]) >= 1 .
H35:   blockoffset + 2 + element(fld_blocklengths(nsec_record), [
          loop__2__block__entry__loop__3]) <= 8180 .
H36:   element(fld_blocklengths(nsec_record), [loop__2__block__entry__loop__3]) 
          >= 1 .
H37:   loop__2__block__entry__loop__3 < fld_numberofblocks(nsec_record) .
H38:   integer__size >= 0 .
H39:   character__size >= 0 .
H40:   positive__size >= 0 .
H41:   dns_types__packet_length_range__size >= 0 .
H42:   dns_types__packet_bytes_range__size >= 0 .
H43:   unsigned_types__unsigned16__size >= 0 .
H44:   unsigned_types__unsigned32__size >= 0 .
H45:   rr_type__classtype__size >= 0 .
H46:   rr_type__linelengthindex__size >= 0 .
H47:   rr_type__linefromfiletype__size >= 0 .
H48:   rr_type__wirestringtypeindex__size >= 0 .
H49:   rr_type__wirestringtype__size >= 0 .
H50:   rr_type__resourcerecordtype__size >= 0 .
H51:   rr_type__nsec_record_type__recordtypeindexvalue__size >= 0 .
H52:   rr_type__nsec_record_type__recordtypearrayindex__size >= 0 .
H53:   rr_type__nsec_record_type__blocknumbervalue__size >= 0 .
H54:   rr_type__nsec_record_type__blocknumberarrayindex__size >= 0 .
H55:   rr_type__nsec_record_type__blocklengthvalue__size >= 0 .
H56:   rr_type__nsec_record_type__bitmapindex__size >= 0 .
H57:   rr_type__nsec_record_type__nsecrecordtype__size >= 0 .
       ->
C1:    blockoffset + 2 + element(fld_blocklengths(nsec_record), [
          loop__2__block__entry__loop__3]) <= start_byte + 6 - 1 + 
          current_name_length + loop__2__block__entry__loop__3 * 34 .


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

procedure_set_ttl_data_nsec_21.
H1:    start_byte <= 8174 - current_name_length .
H2:    current_name_length >= 1 .
H3:    current_name_length <= 129 .
H4:    blockoffset >= 1 .
H5:    blockoffset <= start_byte + 6 - 1 + current_name_length + (
          loop__2__block - 1) * 34 .
H6:    dstbytes <= (loop__2__block - 1) * 32 .
H7:    element(fld_blocklengths(nsec_record), [loop__2__block]) >= 1 .
H8:    element(fld_blocklengths(nsec_record), [loop__2__block]) <= 32 .
H9:    for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= element(
          bytes, [i___1]) and element(bytes, [i___1]) <= 255) .
H10:   start_byte >= 1 .
H11:   fld_ttlinseconds(fld_inherit(nsec_record)) >= 0 .
H12:   fld_ttlinseconds(fld_inherit(nsec_record)) <= 4294967295 .
H13:   rr_type__internet <= fld_class(fld_inherit(nsec_record)) .
H14:   fld_class(fld_inherit(nsec_record)) <= rr_type__hs .
H15:   for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <= element(
          fld_nextdomainname(nsec_record), [i___1]) and element(
          fld_nextdomainname(nsec_record), [i___1]) <= 255) .
H16:   for_all(i___2 : integer, 1 <= i___2 and i___2 <= 256 -> 0 <= element(
          fld_recordlist(nsec_record), [i___2]) and element(fld_recordlist(
          nsec_record), [i___2]) <= 255) .
H17:   fld_numberofrecordtypes(nsec_record) >= 0 .
H18:   fld_numberofrecordtypes(nsec_record) <= 32 .
H19:   for_all(i___3 : integer, 1 <= i___3 and i___3 <= 32 -> dns_types__a <= 
          element(fld_recordtypes(nsec_record), [i___3]) and element(
          fld_recordtypes(nsec_record), [i___3]) <= dns_types__unimplemented) .
H20:   fld_numberofblocks(nsec_record) <= 32 .
H21:   for_all(i___4 : integer, 1 <= i___4 and i___4 <= 32 -> 0 <= element(
          fld_blocknumbers(nsec_record), [i___4]) and element(fld_blocknumbers(
          nsec_record), [i___4]) <= 255) .
H22:   for_all(i___5 : integer, 1 <= i___5 and i___5 <= 32 -> 1 <= element(
          fld_blocklengths(nsec_record), [i___5]) and element(fld_blocklengths(
          nsec_record), [i___5]) <= 32) .
H23:   for_all(i___6 : integer, 1 <= i___6 and i___6 <= 32 -> for_all(i___7 : 
          integer, 1 <= i___7 and i___7 <= 32 -> 0 <= element(element(
          fld_bitmaps(nsec_record), [i___6]), [i___7]) and element(element(
          fld_bitmaps(nsec_record), [i___6]), [i___7]) <= 255)) .
H24:   start_byte <= 6828 .
H25:   loop__2__block <= 32 .
H26:   loop__2__block <= fld_numberofblocks(nsec_record) .
H27:   dstbytes >= 0 .
H28:   integer__size >= 0 .
H29:   character__size >= 0 .
H30:   positive__size >= 0 .
H31:   dns_types__packet_length_range__size >= 0 .
H32:   dns_types__packet_bytes_range__size >= 0 .
H33:   unsigned_types__unsigned16__size >= 0 .
H34:   unsigned_types__unsigned32__size >= 0 .
H35:   rr_type__classtype__size >= 0 .
H36:   rr_type__linelengthindex__size >= 0 .
H37:   rr_type__linefromfiletype__size >= 0 .
H38:   rr_type__wirestringtypeindex__size >= 0 .
H39:   rr_type__wirestringtype__size >= 0 .
H40:   rr_type__resourcerecordtype__size >= 0 .
H41:   rr_type__nsec_record_type__recordtypeindexvalue__size >= 0 .
H42:   rr_type__nsec_record_type__recordtypearrayindex__size >= 0 .
H43:   rr_type__nsec_record_type__blocknumbervalue__size >= 0 .
H44:   rr_type__nsec_record_type__blocknumberarrayindex__size >= 0 .
H45:   rr_type__nsec_record_type__blocklengthvalue__size >= 0 .
H46:   rr_type__nsec_record_type__bitmapindex__size >= 0 .
H47:   rr_type__nsec_record_type__nsecrecordtype__size >= 0 .
       ->
C1:    dstbytes + element(fld_blocklengths(nsec_record), [loop__2__block]) <= 
          8192 .


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

procedure_set_ttl_data_nsec_22.
H1:    start_byte <= 8174 - current_name_length .
H2:    current_name_length >= 1 .
H3:    current_name_length <= 129 .
H4:    blockoffset >= 1 .
H5:    blockoffset <= start_byte + 6 - 1 + current_name_length + (
          loop__2__block - 1) * 34 .
H6:    dstbytes <= (loop__2__block - 1) * 32 .
H7:    element(fld_blocklengths(nsec_record), [loop__2__block]) >= 1 .
H8:    element(fld_blocklengths(nsec_record), [loop__2__block]) <= 32 .
H9:    for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= element(
          bytes, [i___1]) and element(bytes, [i___1]) <= 255) .
H10:   start_byte >= 1 .
H11:   fld_ttlinseconds(fld_inherit(nsec_record)) >= 0 .
H12:   fld_ttlinseconds(fld_inherit(nsec_record)) <= 4294967295 .
H13:   rr_type__internet <= fld_class(fld_inherit(nsec_record)) .
H14:   fld_class(fld_inherit(nsec_record)) <= rr_type__hs .
H15:   for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <= element(
          fld_nextdomainname(nsec_record), [i___1]) and element(
          fld_nextdomainname(nsec_record), [i___1]) <= 255) .
H16:   for_all(i___2 : integer, 1 <= i___2 and i___2 <= 256 -> 0 <= element(
          fld_recordlist(nsec_record), [i___2]) and element(fld_recordlist(
          nsec_record), [i___2]) <= 255) .
H17:   fld_numberofrecordtypes(nsec_record) >= 0 .
H18:   fld_numberofrecordtypes(nsec_record) <= 32 .
H19:   for_all(i___3 : integer, 1 <= i___3 and i___3 <= 32 -> dns_types__a <= 
          element(fld_recordtypes(nsec_record), [i___3]) and element(
          fld_recordtypes(nsec_record), [i___3]) <= dns_types__unimplemented) .
H20:   fld_numberofblocks(nsec_record) <= 32 .
H21:   for_all(i___4 : integer, 1 <= i___4 and i___4 <= 32 -> 0 <= element(
          fld_blocknumbers(nsec_record), [i___4]) and element(fld_blocknumbers(
          nsec_record), [i___4]) <= 255) .
H22:   for_all(i___5 : integer, 1 <= i___5 and i___5 <= 32 -> 1 <= element(
          fld_blocklengths(nsec_record), [i___5]) and element(fld_blocklengths(
          nsec_record), [i___5]) <= 32) .
H23:   for_all(i___6 : integer, 1 <= i___6 and i___6 <= 32 -> for_all(i___7 : 
          integer, 1 <= i___7 and i___7 <= 32 -> 0 <= element(element(
          fld_bitmaps(nsec_record), [i___6]), [i___7]) and element(element(
          fld_bitmaps(nsec_record), [i___6]), [i___7]) <= 255)) .
H24:   start_byte <= 6828 .
H25:   loop__2__block <= 32 .
H26:   loop__2__block <= fld_numberofblocks(nsec_record) .
H27:   dstbytes >= 0 .
H28:   dstbytes + element(fld_blocklengths(nsec_record), [loop__2__block]) >= 0 
          .
H29:   dstbytes + element(fld_blocklengths(nsec_record), [loop__2__block]) <= 
          8192 .
H30:   integer__size >= 0 .
H31:   character__size >= 0 .
H32:   positive__size >= 0 .
H33:   dns_types__packet_length_range__size >= 0 .
H34:   dns_types__packet_bytes_range__size >= 0 .
H35:   unsigned_types__unsigned16__size >= 0 .
H36:   unsigned_types__unsigned32__size >= 0 .
H37:   rr_type__classtype__size >= 0 .
H38:   rr_type__linelengthindex__size >= 0 .
H39:   rr_type__linefromfiletype__size >= 0 .
H40:   rr_type__wirestringtypeindex__size >= 0 .
H41:   rr_type__wirestringtype__size >= 0 .
H42:   rr_type__resourcerecordtype__size >= 0 .
H43:   rr_type__nsec_record_type__recordtypeindexvalue__size >= 0 .
H44:   rr_type__nsec_record_type__recordtypearrayindex__size >= 0 .
H45:   rr_type__nsec_record_type__blocknumbervalue__size >= 0 .
H46:   rr_type__nsec_record_type__blocknumberarrayindex__size >= 0 .
H47:   rr_type__nsec_record_type__blocklengthvalue__size >= 0 .
H48:   rr_type__nsec_record_type__bitmapindex__size >= 0 .
H49:   rr_type__nsec_record_type__nsecrecordtype__size >= 0 .
       ->
C1:    blockoffset <= 8179 .
C2:    blockoffset <= 2147483646 .


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

procedure_set_ttl_data_nsec_23.
H1:    start_byte <= 8174 - current_name_length .
H2:    current_name_length >= 1 .
H3:    current_name_length <= 129 .
H4:    blockoffset >= 1 .
H5:    blockoffset <= start_byte + 6 - 1 + current_name_length + (
          loop__2__block - 1) * 34 .
H6:    dstbytes <= (loop__2__block - 1) * 32 .
H7:    element(fld_blocklengths(nsec_record), [loop__2__block]) >= 1 .
H8:    element(fld_blocklengths(nsec_record), [loop__2__block]) <= 32 .
H9:    for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= element(
          bytes, [i___1]) and element(bytes, [i___1]) <= 255) .
H10:   start_byte >= 1 .
H11:   fld_ttlinseconds(fld_inherit(nsec_record)) >= 0 .
H12:   fld_ttlinseconds(fld_inherit(nsec_record)) <= 4294967295 .
H13:   rr_type__internet <= fld_class(fld_inherit(nsec_record)) .
H14:   fld_class(fld_inherit(nsec_record)) <= rr_type__hs .
H15:   for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <= element(
          fld_nextdomainname(nsec_record), [i___1]) and element(
          fld_nextdomainname(nsec_record), [i___1]) <= 255) .
H16:   for_all(i___2 : integer, 1 <= i___2 and i___2 <= 256 -> 0 <= element(
          fld_recordlist(nsec_record), [i___2]) and element(fld_recordlist(
          nsec_record), [i___2]) <= 255) .
H17:   fld_numberofrecordtypes(nsec_record) >= 0 .
H18:   fld_numberofrecordtypes(nsec_record) <= 32 .
H19:   for_all(i___3 : integer, 1 <= i___3 and i___3 <= 32 -> dns_types__a <= 
          element(fld_recordtypes(nsec_record), [i___3]) and element(
          fld_recordtypes(nsec_record), [i___3]) <= dns_types__unimplemented) .
H20:   fld_numberofblocks(nsec_record) <= 32 .
H21:   for_all(i___4 : integer, 1 <= i___4 and i___4 <= 32 -> 0 <= element(
          fld_blocknumbers(nsec_record), [i___4]) and element(fld_blocknumbers(
          nsec_record), [i___4]) <= 255) .
H22:   for_all(i___5 : integer, 1 <= i___5 and i___5 <= 32 -> 1 <= element(
          fld_blocklengths(nsec_record), [i___5]) and element(fld_blocklengths(
          nsec_record), [i___5]) <= 32) .
H23:   for_all(i___6 : integer, 1 <= i___6 and i___6 <= 32 -> for_all(i___7 : 
          integer, 1 <= i___7 and i___7 <= 32 -> 0 <= element(element(
          fld_bitmaps(nsec_record), [i___6]), [i___7]) and element(element(
          fld_bitmaps(nsec_record), [i___6]), [i___7]) <= 255)) .
H24:   start_byte <= 6828 .
H25:   loop__2__block <= 32 .
H26:   loop__2__block <= fld_numberofblocks(nsec_record) .
H27:   dstbytes >= 0 .
H28:   dstbytes + element(fld_blocklengths(nsec_record), [loop__2__block]) >= 0 
          .
H29:   dstbytes + element(fld_blocklengths(nsec_record), [loop__2__block]) <= 
          8192 .
H30:   element(fld_blocknumbers(nsec_record), [loop__2__block]) >= 0 .
H31:   element(fld_blocknumbers(nsec_record), [loop__2__block]) <= 255 .
H32:   blockoffset <= 8179 .
H33:   integer__size >= 0 .
H34:   character__size >= 0 .
H35:   positive__size >= 0 .
H36:   dns_types__packet_length_range__size >= 0 .
H37:   dns_types__packet_bytes_range__size >= 0 .
H38:   unsigned_types__unsigned16__size >= 0 .
H39:   unsigned_types__unsigned32__size >= 0 .
H40:   rr_type__classtype__size >= 0 .
H41:   rr_type__linelengthindex__size >= 0 .
H42:   rr_type__linefromfiletype__size >= 0 .
H43:   rr_type__wirestringtypeindex__size >= 0 .
H44:   rr_type__wirestringtype__size >= 0 .
H45:   rr_type__resourcerecordtype__size >= 0 .
H46:   rr_type__nsec_record_type__recordtypeindexvalue__size >= 0 .
H47:   rr_type__nsec_record_type__recordtypearrayindex__size >= 0 .
H48:   rr_type__nsec_record_type__blocknumbervalue__size >= 0 .
H49:   rr_type__nsec_record_type__blocknumberarrayindex__size >= 0 .
H50:   rr_type__nsec_record_type__blocklengthvalue__size >= 0 .
H51:   rr_type__nsec_record_type__bitmapindex__size >= 0 .
H52:   rr_type__nsec_record_type__nsecrecordtype__size >= 0 .
       ->
C1:    blockoffset <= 8178 .


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

procedure_set_ttl_data_nsec_24.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_nsec_25.
*** true .          /* all conclusions proved */


For path(s) from assertion of line 164 to assertion of line 176:

procedure_set_ttl_data_nsec_26.
H1:    start_byte <= 8174 - current_name_length .
H2:    current_name_length >= 1 .
H3:    current_name_length <= 129 .
H4:    blockoffset >= 1 .
H5:    blockoffset <= start_byte + 6 - 1 + current_name_length + (
          loop__2__block - 1) * 34 .
H6:    dstbytes <= (loop__2__block - 1) * 32 .
H7:    element(fld_blocklengths(nsec_record), [loop__2__block]) >= 1 .
H8:    element(fld_blocklengths(nsec_record), [loop__2__block]) <= 32 .
H9:    for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= element(
          bytes, [i___1]) and element(bytes, [i___1]) <= 255) .
H10:   start_byte >= 1 .
H11:   fld_ttlinseconds(fld_inherit(nsec_record)) >= 0 .
H12:   fld_ttlinseconds(fld_inherit(nsec_record)) <= 4294967295 .
H13:   rr_type__internet <= fld_class(fld_inherit(nsec_record)) .
H14:   fld_class(fld_inherit(nsec_record)) <= rr_type__hs .
H15:   for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <= element(
          fld_nextdomainname(nsec_record), [i___1]) and element(
          fld_nextdomainname(nsec_record), [i___1]) <= 255) .
H16:   for_all(i___2 : integer, 1 <= i___2 and i___2 <= 256 -> 0 <= element(
          fld_recordlist(nsec_record), [i___2]) and element(fld_recordlist(
          nsec_record), [i___2]) <= 255) .
H17:   fld_numberofrecordtypes(nsec_record) >= 0 .
H18:   fld_numberofrecordtypes(nsec_record) <= 32 .
H19:   for_all(i___3 : integer, 1 <= i___3 and i___3 <= 32 -> dns_types__a <= 
          element(fld_recordtypes(nsec_record), [i___3]) and element(
          fld_recordtypes(nsec_record), [i___3]) <= dns_types__unimplemented) .
H20:   fld_numberofblocks(nsec_record) >= 0 .
H21:   fld_numberofblocks(nsec_record) <= 32 .
H22:   for_all(i___4 : integer, 1 <= i___4 and i___4 <= 32 -> 0 <= element(
          fld_blocknumbers(nsec_record), [i___4]) and element(fld_blocknumbers(
          nsec_record), [i___4]) <= 255) .
H23:   for_all(i___5 : integer, 1 <= i___5 and i___5 <= 32 -> 1 <= element(
          fld_blocklengths(nsec_record), [i___5]) and element(fld_blocklengths(
          nsec_record), [i___5]) <= 32) .
H24:   for_all(i___6 : integer, 1 <= i___6 and i___6 <= 32 -> for_all(i___7 : 
          integer, 1 <= i___7 and i___7 <= 32 -> 0 <= element(element(
          fld_bitmaps(nsec_record), [i___6]), [i___7]) and element(element(
          fld_bitmaps(nsec_record), [i___6]), [i___7]) <= 255)) .
H25:   start_byte <= 6828 .
H26:   loop__2__block <= 32 .
H27:   loop__2__block <= fld_numberofblocks(nsec_record) .
H28:   dstbytes >= 0 .
H29:   dstbytes + element(fld_blocklengths(nsec_record), [loop__2__block]) >= 0 
          .
H30:   dstbytes + element(fld_blocklengths(nsec_record), [loop__2__block]) <= 
          8192 .
H31:   element(fld_blocknumbers(nsec_record), [loop__2__block]) >= 0 .
H32:   element(fld_blocknumbers(nsec_record), [loop__2__block]) <= 255 .
H33:   blockoffset <= 8178 .
H34:   integer__size >= 0 .
H35:   character__size >= 0 .
H36:   positive__size >= 0 .
H37:   dns_types__packet_length_range__size >= 0 .
H38:   dns_types__packet_bytes_range__size >= 0 .
H39:   unsigned_types__unsigned16__size >= 0 .
H40:   unsigned_types__unsigned32__size >= 0 .
H41:   rr_type__classtype__size >= 0 .
H42:   rr_type__linelengthindex__size >= 0 .
H43:   rr_type__linefromfiletype__size >= 0 .
H44:   rr_type__wirestringtypeindex__size >= 0 .
H45:   rr_type__wirestringtype__size >= 0 .
H46:   rr_type__resourcerecordtype__size >= 0 .
H47:   rr_type__nsec_record_type__recordtypeindexvalue__size >= 0 .
H48:   rr_type__nsec_record_type__recordtypearrayindex__size >= 0 .
H49:   rr_type__nsec_record_type__blocknumbervalue__size >= 0 .
H50:   rr_type__nsec_record_type__blocknumberarrayindex__size >= 0 .
H51:   rr_type__nsec_record_type__blocklengthvalue__size >= 0 .
H52:   rr_type__nsec_record_type__bitmapindex__size >= 0 .
H53:   rr_type__nsec_record_type__nsecrecordtype__size >= 0 .
       ->
C1:    dstbytes + element(fld_blocklengths(nsec_record), [loop__2__block]) <= 
          loop__2__block * 32 .


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

procedure_set_ttl_data_nsec_27.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_nsec_28.
H1:    start_byte <= 8174 - current_name_length .
H2:    current_name_length >= 1 .
H3:    current_name_length <= 129 .
H4:    blockoffset >= 1 .
H5:    blockoffset <= start_byte + 6 - 1 + current_name_length + (
          loop__2__block__entry__loop__3 - 1) * 34 .
H6:    dstbytes <= loop__2__block__entry__loop__3 * 32 .
H7:    loop__3__byte >= 1 .
H8:    loop__3__byte <= 32 .
H9:    for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= element(
          bytes, [i___1]) and element(bytes, [i___1]) <= 255) .
H10:   start_byte >= 1 .
H11:   fld_ttlinseconds(fld_inherit(nsec_record)) >= 0 .
H12:   fld_ttlinseconds(fld_inherit(nsec_record)) <= 4294967295 .
H13:   rr_type__internet <= fld_class(fld_inherit(nsec_record)) .
H14:   fld_class(fld_inherit(nsec_record)) <= rr_type__hs .
H15:   for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <= element(
          fld_nextdomainname(nsec_record), [i___1]) and element(
          fld_nextdomainname(nsec_record), [i___1]) <= 255) .
H16:   for_all(i___2 : integer, 1 <= i___2 and i___2 <= 256 -> 0 <= element(
          fld_recordlist(nsec_record), [i___2]) and element(fld_recordlist(
          nsec_record), [i___2]) <= 255) .
H17:   fld_numberofrecordtypes(nsec_record) >= 0 .
H18:   fld_numberofrecordtypes(nsec_record) <= 32 .
H19:   for_all(i___3 : integer, 1 <= i___3 and i___3 <= 32 -> dns_types__a <= 
          element(fld_recordtypes(nsec_record), [i___3]) and element(
          fld_recordtypes(nsec_record), [i___3]) <= dns_types__unimplemented) .
H20:   fld_numberofblocks(nsec_record) <= 32 .
H21:   for_all(i___4 : integer, 1 <= i___4 and i___4 <= 32 -> 0 <= element(
          fld_blocknumbers(nsec_record), [i___4]) and element(fld_blocknumbers(
          nsec_record), [i___4]) <= 255) .
H22:   for_all(i___5 : integer, 1 <= i___5 and i___5 <= 32 -> 1 <= element(
          fld_blocklengths(nsec_record), [i___5]) and element(fld_blocklengths(
          nsec_record), [i___5]) <= 32) .
H23:   for_all(i___6 : integer, 1 <= i___6 and i___6 <= 32 -> for_all(i___7 : 
          integer, 1 <= i___7 and i___7 <= 32 -> 0 <= element(element(
          fld_bitmaps(nsec_record), [i___6]), [i___7]) and element(element(
          fld_bitmaps(nsec_record), [i___6]), [i___7]) <= 255)) .
H24:   start_byte <= 6828 .
H25:   loop__3__byte <= element(fld_blocklengths(nsec_record), [
          loop__2__block__entry__loop__3]) .
H26:   loop__2__block__entry__loop__3 <= 32 .
H27:   loop__2__block__entry__loop__3 <= 32 .
H28:   loop__2__block__entry__loop__3 >= 1 .
H29:   loop__2__block__entry__loop__3 <= fld_numberofblocks(nsec_record) .
H30:   integer__size >= 0 .
H31:   character__size >= 0 .
H32:   positive__size >= 0 .
H33:   dns_types__packet_length_range__size >= 0 .
H34:   dns_types__packet_bytes_range__size >= 0 .
H35:   unsigned_types__unsigned16__size >= 0 .
H36:   unsigned_types__unsigned32__size >= 0 .
H37:   rr_type__classtype__size >= 0 .
H38:   rr_type__linelengthindex__size >= 0 .
H39:   rr_type__linefromfiletype__size >= 0 .
H40:   rr_type__wirestringtypeindex__size >= 0 .
H41:   rr_type__wirestringtype__size >= 0 .
H42:   rr_type__resourcerecordtype__size >= 0 .
H43:   rr_type__nsec_record_type__recordtypeindexvalue__size >= 0 .
H44:   rr_type__nsec_record_type__recordtypearrayindex__size >= 0 .
H45:   rr_type__nsec_record_type__blocknumbervalue__size >= 0 .
H46:   rr_type__nsec_record_type__blocknumberarrayindex__size >= 0 .
H47:   rr_type__nsec_record_type__blocklengthvalue__size >= 0 .
H48:   rr_type__nsec_record_type__bitmapindex__size >= 0 .
H49:   rr_type__nsec_record_type__nsecrecordtype__size >= 0 .
       ->
C1:    blockoffset + 2 + loop__3__byte <= 8180 .
C2:    blockoffset + 2 + loop__3__byte <= 2147483647 .
C3:    blockoffset <= 2147483645 .


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

procedure_set_ttl_data_nsec_29.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_nsec_30.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_nsec_31.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_nsec_32.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_nsec_33.
*** true .   /* contradiction within hypotheses. */



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

procedure_set_ttl_data_nsec_34.
H1:    start_byte <= 8174 - current_name_length .
H2:    current_name_length >= 1 .
H3:    current_name_length <= 129 .
H4:    blockoffset >= 1 .
H5:    blockoffset <= start_byte + 6 - 1 + current_name_length + (
          fld_numberofblocks(nsec_record) - 1) * 34 .
H6:    dstbytes <= fld_numberofblocks(nsec_record) * 32 .
H7:    element(fld_blocklengths(nsec_record), [fld_numberofblocks(nsec_record)])
           >= 1 .
H8:    element(fld_blocklengths(nsec_record), [fld_numberofblocks(nsec_record)])
           <= 32 .
H9:    for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= element(
          bytes, [i___1]) and element(bytes, [i___1]) <= 255) .
H10:   start_byte >= 1 .
H11:   fld_ttlinseconds(fld_inherit(nsec_record)) >= 0 .
H12:   fld_ttlinseconds(fld_inherit(nsec_record)) <= 4294967295 .
H13:   rr_type__internet <= fld_class(fld_inherit(nsec_record)) .
H14:   fld_class(fld_inherit(nsec_record)) <= rr_type__hs .
H15:   for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <= element(
          fld_nextdomainname(nsec_record), [i___1]) and element(
          fld_nextdomainname(nsec_record), [i___1]) <= 255) .
H16:   for_all(i___2 : integer, 1 <= i___2 and i___2 <= 256 -> 0 <= element(
          fld_recordlist(nsec_record), [i___2]) and element(fld_recordlist(
          nsec_record), [i___2]) <= 255) .
H17:   fld_numberofrecordtypes(nsec_record) >= 0 .
H18:   fld_numberofrecordtypes(nsec_record) <= 32 .
H19:   for_all(i___3 : integer, 1 <= i___3 and i___3 <= 32 -> dns_types__a <= 
          element(fld_recordtypes(nsec_record), [i___3]) and element(
          fld_recordtypes(nsec_record), [i___3]) <= dns_types__unimplemented) .
H20:   fld_numberofblocks(nsec_record) >= 0 .
H21:   fld_numberofblocks(nsec_record) <= 32 .
H22:   for_all(i___4 : integer, 1 <= i___4 and i___4 <= 32 -> 0 <= element(
          fld_blocknumbers(nsec_record), [i___4]) and element(fld_blocknumbers(
          nsec_record), [i___4]) <= 255) .
H23:   for_all(i___5 : integer, 1 <= i___5 and i___5 <= 32 -> 1 <= element(
          fld_blocklengths(nsec_record), [i___5]) and element(fld_blocklengths(
          nsec_record), [i___5]) <= 32) .
H24:   for_all(i___6 : integer, 1 <= i___6 and i___6 <= 32 -> for_all(i___7 : 
          integer, 1 <= i___7 and i___7 <= 32 -> 0 <= element(element(
          fld_bitmaps(nsec_record), [i___6]), [i___7]) and element(element(
          fld_bitmaps(nsec_record), [i___6]), [i___7]) <= 255)) .
H25:   start_byte <= 6828 .
H26:   fld_numberofblocks(nsec_record) >= 0 .
H27:   fld_numberofblocks(nsec_record) <= 32 .
H28:   fld_numberofblocks(nsec_record) <= 32 .
H29:   fld_numberofblocks(nsec_record) >= 1 .
H30:   element(element(fld_bitmaps(nsec_record), [fld_numberofblocks(
          nsec_record)]), [element(fld_blocklengths(nsec_record), [
          fld_numberofblocks(nsec_record)])]) >= 0 .
H31:   element(element(fld_bitmaps(nsec_record), [fld_numberofblocks(
          nsec_record)]), [element(fld_blocklengths(nsec_record), [
          fld_numberofblocks(nsec_record)])]) <= 255 .
H32:   blockoffset + 2 + element(fld_blocklengths(nsec_record), [
          fld_numberofblocks(nsec_record)]) >= 1 .
H33:   blockoffset + 2 + element(fld_blocklengths(nsec_record), [
          fld_numberofblocks(nsec_record)]) <= 8180 .
H34:   blockoffset + 2 + element(fld_blocklengths(nsec_record), [
          fld_numberofblocks(nsec_record)]) >= 1 .
H35:   blockoffset + 2 + element(fld_blocklengths(nsec_record), [
          fld_numberofblocks(nsec_record)]) <= 8180 .
H36:   element(fld_blocklengths(nsec_record), [fld_numberofblocks(nsec_record)])
           >= 1 .
H37:   dstbytes >= 0 .
H38:   integer__size >= 0 .
H39:   character__size >= 0 .
H40:   positive__size >= 0 .
H41:   dns_types__packet_length_range__size >= 0 .
H42:   dns_types__packet_bytes_range__size >= 0 .
H43:   unsigned_types__unsigned16__size >= 0 .
H44:   unsigned_types__unsigned32__size >= 0 .
H45:   rr_type__classtype__size >= 0 .
H46:   rr_type__linelengthindex__size >= 0 .
H47:   rr_type__linefromfiletype__size >= 0 .
H48:   rr_type__wirestringtypeindex__size >= 0 .
H49:   rr_type__wirestringtype__size >= 0 .
H50:   rr_type__resourcerecordtype__size >= 0 .
H51:   rr_type__nsec_record_type__recordtypeindexvalue__size >= 0 .
H52:   rr_type__nsec_record_type__recordtypearrayindex__size >= 0 .
H53:   rr_type__nsec_record_type__blocknumbervalue__size >= 0 .
H54:   rr_type__nsec_record_type__blocknumberarrayindex__size >= 0 .
H55:   rr_type__nsec_record_type__blocklengthvalue__size >= 0 .
H56:   rr_type__nsec_record_type__bitmapindex__size >= 0 .
H57:   rr_type__nsec_record_type__nsecrecordtype__size >= 0 .
       ->
C1:    dstbytes + fld_numberofblocks(nsec_record) * 2 <= 8192 .


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

procedure_set_ttl_data_nsec_35.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_nsec_36.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_nsec_37.
*** true .   /* contradiction within hypotheses. */



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

procedure_set_ttl_data_nsec_38.
H1:    start_byte <= 8174 - current_name_length .
H2:    current_name_length >= 1 .
H3:    current_name_length <= 129 .
H4:    blockoffset >= 1 .
H5:    blockoffset <= start_byte + 6 - 1 + current_name_length + (
          fld_numberofblocks(nsec_record) - 1) * 34 .
H6:    dstbytes <= fld_numberofblocks(nsec_record) * 32 .
H7:    element(fld_blocklengths(nsec_record), [fld_numberofblocks(nsec_record)])
           >= 1 .
H8:    element(fld_blocklengths(nsec_record), [fld_numberofblocks(nsec_record)])
           <= 32 .
H9:    for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= element(
          bytes, [i___1]) and element(bytes, [i___1]) <= 255) .
H10:   start_byte >= 1 .
H11:   fld_ttlinseconds(fld_inherit(nsec_record)) >= 0 .
H12:   fld_ttlinseconds(fld_inherit(nsec_record)) <= 4294967295 .
H13:   rr_type__internet <= fld_class(fld_inherit(nsec_record)) .
H14:   fld_class(fld_inherit(nsec_record)) <= rr_type__hs .
H15:   for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <= element(
          fld_nextdomainname(nsec_record), [i___1]) and element(
          fld_nextdomainname(nsec_record), [i___1]) <= 255) .
H16:   for_all(i___2 : integer, 1 <= i___2 and i___2 <= 256 -> 0 <= element(
          fld_recordlist(nsec_record), [i___2]) and element(fld_recordlist(
          nsec_record), [i___2]) <= 255) .
H17:   fld_numberofrecordtypes(nsec_record) >= 0 .
H18:   fld_numberofrecordtypes(nsec_record) <= 32 .
H19:   for_all(i___3 : integer, 1 <= i___3 and i___3 <= 32 -> dns_types__a <= 
          element(fld_recordtypes(nsec_record), [i___3]) and element(
          fld_recordtypes(nsec_record), [i___3]) <= dns_types__unimplemented) .
H20:   fld_numberofblocks(nsec_record) <= 32 .
H21:   for_all(i___4 : integer, 1 <= i___4 and i___4 <= 32 -> 0 <= element(
          fld_blocknumbers(nsec_record), [i___4]) and element(fld_blocknumbers(
          nsec_record), [i___4]) <= 255) .
H22:   for_all(i___5 : integer, 1 <= i___5 and i___5 <= 32 -> 1 <= element(
          fld_blocklengths(nsec_record), [i___5]) and element(fld_blocklengths(
          nsec_record), [i___5]) <= 32) .
H23:   for_all(i___6 : integer, 1 <= i___6 and i___6 <= 32 -> for_all(i___7 : 
          integer, 1 <= i___7 and i___7 <= 32 -> 0 <= element(element(
          fld_bitmaps(nsec_record), [i___6]), [i___7]) and element(element(
          fld_bitmaps(nsec_record), [i___6]), [i___7]) <= 255)) .
H24:   start_byte <= 6828 .
H25:   fld_numberofblocks(nsec_record) >= 0 .
H26:   fld_numberofblocks(nsec_record) <= 32 .
H27:   fld_numberofblocks(nsec_record) <= 32 .
H28:   fld_numberofblocks(nsec_record) >= 1 .
H29:   element(element(fld_bitmaps(nsec_record), [fld_numberofblocks(
          nsec_record)]), [element(fld_blocklengths(nsec_record), [
          fld_numberofblocks(nsec_record)])]) >= 0 .
H30:   element(element(fld_bitmaps(nsec_record), [fld_numberofblocks(
          nsec_record)]), [element(fld_blocklengths(nsec_record), [
          fld_numberofblocks(nsec_record)])]) <= 255 .
H31:   blockoffset + 2 + element(fld_blocklengths(nsec_record), [
          fld_numberofblocks(nsec_record)]) >= 1 .
H32:   blockoffset + 2 + element(fld_blocklengths(nsec_record), [
          fld_numberofblocks(nsec_record)]) <= 8180 .
H33:   blockoffset + 2 + element(fld_blocklengths(nsec_record), [
          fld_numberofblocks(nsec_record)]) >= 1 .
H34:   blockoffset + 2 + element(fld_blocklengths(nsec_record), [
          fld_numberofblocks(nsec_record)]) <= 8180 .
H35:   element(fld_blocklengths(nsec_record), [fld_numberofblocks(nsec_record)])
           >= 1 .
H36:   dstbytes >= 0 .
H37:   dstbytes + fld_numberofblocks(nsec_record) * 2 >= 0 .
H38:   dstbytes + fld_numberofblocks(nsec_record) * 2 <= 8192 .
H39:   fld_numberofblocks(nsec_record) * 2 >= 0 .
H40:   integer__size >= 0 .
H41:   character__size >= 0 .
H42:   positive__size >= 0 .
H43:   dns_types__packet_length_range__size >= 0 .
H44:   dns_types__packet_bytes_range__size >= 0 .
H45:   unsigned_types__unsigned16__size >= 0 .
H46:   unsigned_types__unsigned32__size >= 0 .
H47:   rr_type__classtype__size >= 0 .
H48:   rr_type__linelengthindex__size >= 0 .
H49:   rr_type__linefromfiletype__size >= 0 .
H50:   rr_type__wirestringtypeindex__size >= 0 .
H51:   rr_type__wirestringtype__size >= 0 .
H52:   rr_type__resourcerecordtype__size >= 0 .
H53:   rr_type__nsec_record_type__recordtypeindexvalue__size >= 0 .
H54:   rr_type__nsec_record_type__recordtypearrayindex__size >= 0 .
H55:   rr_type__nsec_record_type__blocknumbervalue__size >= 0 .
H56:   rr_type__nsec_record_type__blocknumberarrayindex__size >= 0 .
H57:   rr_type__nsec_record_type__blocklengthvalue__size >= 0 .
H58:   rr_type__nsec_record_type__bitmapindex__size >= 0 .
H59:   rr_type__nsec_record_type__nsecrecordtype__size >= 0 .
       ->
C1:    dstbytes + fld_numberofblocks(nsec_record) * 2 + current_name_length <= 
          8192 .


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

procedure_set_ttl_data_nsec_39.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_nsec_40.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_nsec_41.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_nsec_42.
*** true .          /* all conclusions proved */


For path(s) from start to finish:

procedure_set_ttl_data_nsec_43.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_nsec_44.
*** true .          /* all conclusions proved */


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

procedure_set_ttl_data_nsec_45.
*** true .   /* contradiction within hypotheses. */



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

procedure_set_ttl_data_nsec_46.
H1:    start_byte <= 8174 - current_name_length .
H2:    current_name_length >= 1 .
H3:    current_name_length <= 129 .
H4:    blockoffset >= 1 .
H5:    blockoffset <= start_byte + 6 - 1 + current_name_length + (
          fld_numberofblocks(nsec_record) - 1) * 34 .
H6:    dstbytes <= fld_numberofblocks(nsec_record) * 32 .
H7:    element(fld_blocklengths(nsec_record), [fld_numberofblocks(nsec_record)])
           >= 1 .
H8:    element(fld_blocklengths(nsec_record), [fld_numberofblocks(nsec_record)])
           <= 32 .
H9:    for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= element(
          bytes, [i___1]) and element(bytes, [i___1]) <= 255) .
H10:   start_byte >= 1 .
H11:   fld_ttlinseconds(fld_inherit(nsec_record)) >= 0 .
H12:   fld_ttlinseconds(fld_inherit(nsec_record)) <= 4294967295 .
H13:   rr_type__internet <= fld_class(fld_inherit(nsec_record)) .
H14:   fld_class(fld_inherit(nsec_record)) <= rr_type__hs .
H15:   for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <= element(
          fld_nextdomainname(nsec_record), [i___1]) and element(
          fld_nextdomainname(nsec_record), [i___1]) <= 255) .
H16:   for_all(i___2 : integer, 1 <= i___2 and i___2 <= 256 -> 0 <= element(
          fld_recordlist(nsec_record), [i___2]) and element(fld_recordlist(
          nsec_record), [i___2]) <= 255) .
H17:   fld_numberofrecordtypes(nsec_record) >= 0 .
H18:   fld_numberofrecordtypes(nsec_record) <= 32 .
H19:   for_all(i___3 : integer, 1 <= i___3 and i___3 <= 32 -> dns_types__a <= 
          element(fld_recordtypes(nsec_record), [i___3]) and element(
          fld_recordtypes(nsec_record), [i___3]) <= dns_types__unimplemented) .
H20:   fld_numberofblocks(nsec_record) <= 32 .
H21:   for_all(i___4 : integer, 1 <= i___4 and i___4 <= 32 -> 0 <= element(
          fld_blocknumbers(nsec_record), [i___4]) and element(fld_blocknumbers(
          nsec_record), [i___4]) <= 255) .
H22:   for_all(i___5 : integer, 1 <= i___5 and i___5 <= 32 -> 1 <= element(
          fld_blocklengths(nsec_record), [i___5]) and element(fld_blocklengths(
          nsec_record), [i___5]) <= 32) .
H23:   for_all(i___6 : integer, 1 <= i___6 and i___6 <= 32 -> for_all(i___7 : 
          integer, 1 <= i___7 and i___7 <= 32 -> 0 <= element(element(
          fld_bitmaps(nsec_record), [i___6]), [i___7]) and element(element(
          fld_bitmaps(nsec_record), [i___6]), [i___7]) <= 255)) .
H24:   start_byte <= 6828 .
H25:   fld_numberofblocks(nsec_record) >= 0 .
H26:   fld_numberofblocks(nsec_record) <= 32 .
H27:   fld_numberofblocks(nsec_record) <= 32 .
H28:   fld_numberofblocks(nsec_record) >= 1 .
H29:   element(element(fld_bitmaps(nsec_record), [fld_numberofblocks(
          nsec_record)]), [element(fld_blocklengths(nsec_record), [
          fld_numberofblocks(nsec_record)])]) >= 0 .
H30:   element(element(fld_bitmaps(nsec_record), [fld_numberofblocks(
          nsec_record)]), [element(fld_blocklengths(nsec_record), [
          fld_numberofblocks(nsec_record)])]) <= 255 .
H31:   blockoffset + 2 + element(fld_blocklengths(nsec_record), [
          fld_numberofblocks(nsec_record)]) >= 1 .
H32:   blockoffset + 2 + element(fld_blocklengths(nsec_record), [
          fld_numberofblocks(nsec_record)]) <= 8180 .
H33:   blockoffset <= 8180 .
H34:   blockoffset + 2 + element(fld_blocklengths(nsec_record), [
          fld_numberofblocks(nsec_record)]) >= 1 .
H35:   blockoffset + 2 + element(fld_blocklengths(nsec_record), [
          fld_numberofblocks(nsec_record)]) <= 8180 .
H36:   element(fld_blocklengths(nsec_record), [fld_numberofblocks(nsec_record)])
           >= 1 .
H37:   dstbytes >= 0 .
H38:   dstbytes <= 8192 .
H39:   dstbytes + fld_numberofblocks(nsec_record) * 2 >= 0 .
H40:   fld_numberofblocks(nsec_record) * 2 >= 0 .
H41:   dstbytes + fld_numberofblocks(nsec_record) * 2 + current_name_length >= 
          0 .
H42:   dstbytes + fld_numberofblocks(nsec_record) * 2 + current_name_length <= 
          8192 .
H43:   for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= element(
          bytes__3, [i___1]) and element(bytes__3, [i___1]) <= 255) .
H44:   integer__size >= 0 .
H45:   character__size >= 0 .
H46:   positive__size >= 0 .
H47:   dns_types__packet_length_range__size >= 0 .
H48:   dns_types__packet_bytes_range__size >= 0 .
H49:   unsigned_types__unsigned16__size >= 0 .
H50:   unsigned_types__unsigned32__size >= 0 .
H51:   rr_type__classtype__size >= 0 .
H52:   rr_type__linelengthindex__size >= 0 .
H53:   rr_type__linefromfiletype__size >= 0 .
H54:   rr_type__wirestringtypeindex__size >= 0 .
H55:   rr_type__wirestringtype__size >= 0 .
H56:   rr_type__resourcerecordtype__size >= 0 .
H57:   rr_type__nsec_record_type__recordtypeindexvalue__size >= 0 .
H58:   rr_type__nsec_record_type__recordtypearrayindex__size >= 0 .
H59:   rr_type__nsec_record_type__blocknumbervalue__size >= 0 .
H60:   rr_type__nsec_record_type__blocknumberarrayindex__size >= 0 .
H61:   rr_type__nsec_record_type__blocklengthvalue__size >= 0 .
H62:   rr_type__nsec_record_type__bitmapindex__size >= 0 .
H63:   rr_type__nsec_record_type__nsecrecordtype__size >= 0 .
       ->
C1:    dstbytes + fld_numberofblocks(nsec_record) * 2 + current_name_length <= 
          1217 .


