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

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


                 procedure Parser_Utilities.ConvertTimeSpec




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

procedure_converttimespec_1.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H2:    begidx >= rr_type__linelengthindex__first .
H3:    begidx <= rr_type__linelengthindex__last .
H4:    endidx >= rr_type__linelengthindex__first .
H5:    endidx <= rr_type__linelengthindex__last .
        ->
C1:    endidx >= integer__first .
C2:    endidx <= integer__last .
C3:    begidx >= integer__first .
C4:    begidx <= integer__last .
 

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

procedure_converttimespec_2.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H2:    begidx >= rr_type__linelengthindex__first .
H3:    begidx <= rr_type__linelengthindex__last .
H4:    endidx >= rr_type__linelengthindex__first .
H5:    endidx <= rr_type__linelengthindex__last .
H6:    endidx >= integer__first .
H7:    endidx <= integer__last .
H8:    begidx >= integer__first .
H9:    begidx <= integer__last .
        ->
C1:    (begidx <= endidx) -> ((endidx >= integer__first) and (
           endidx <= integer__last)) .
C2:    (begidx <= endidx) -> ((begidx >= integer__first) and (
           begidx <= integer__last)) .
 

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

procedure_converttimespec_3.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H2:    begidx >= rr_type__linelengthindex__first .
H3:    begidx <= rr_type__linelengthindex__last .
H4:    endidx >= rr_type__linelengthindex__first .
H5:    endidx <= rr_type__linelengthindex__last .
H6:    endidx >= integer__first .
H7:    endidx <= integer__last .
H8:    begidx >= integer__first .
H9:    begidx <= integer__last .
H10:   (begidx <= endidx) -> ((endidx >= integer__first) and (
           endidx <= integer__last)) .
H11:   (begidx <= endidx) -> ((begidx >= integer__first) and (
           begidx <= integer__last)) .
H12:   begidx <= endidx .
        ->
C1:    0 >= 0 .
C2:    0 <= rr_type__soa_record_type__max_time_val .
C3:    0 >= 0 .
C4:    0 <= rr_type__soa_record_type__max_time_val .
C5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
C6:    begidx >= rr_type__linelengthindex__first .
C7:    begidx <= rr_type__linelengthindex__last .
C8:    endidx >= rr_type__linelengthindex__first .
C9:    endidx <= rr_type__linelengthindex__last .
C10:   begidx >= integer__first .
C11:   begidx <= integer__last .
C12:   begidx >= begidx .
C13:   begidx <= endidx .
 

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

procedure_converttimespec_4.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   element(s, [loop__1__i]) >= 48 .
H21:   element(s, [loop__1__i]) <= 57 .
H22:   blob >= long_long_integer__first .
H23:   blob <= long_long_integer__last .
H24:   element(s, [loop__1__i]) >= character__first .
H25:   element(s, [loop__1__i]) <= character__last .
H26:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H27:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
H28:   element(s, [loop__1__i]) - 48 >= long_long_integer__base__first .
H29:   element(s, [loop__1__i]) - 48 <= long_long_integer__base__last .
H30:   10 * blob >= long_long_integer__base__first .
H31:   10 * blob <= long_long_integer__base__last .
H32:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H33:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
H34:   10 * blob + (element(s, [loop__1__i]) - 48) > 
           rr_type__soa_record_type__max_time_val .
H35:   not (false = false) .
H36:   not (loop__1__i = endidx) .
        ->
C1:    10 * blob + (element(s, [loop__1__i]) - 48) >= 0 .
C2:    10 * blob + (element(s, [loop__1__i]) - 48) <= 
           rr_type__soa_record_type__max_time_val .
C3:    tmp >= 0 .
C4:    tmp <= rr_type__soa_record_type__max_time_val .
C5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
C6:    begidx >= rr_type__linelengthindex__first .
C7:    begidx <= rr_type__linelengthindex__last .
C8:    endidx >= rr_type__linelengthindex__first .
C9:    endidx <= rr_type__linelengthindex__last .
C10:   loop__1__i + 1 >= integer__first .
C11:   loop__1__i + 1 <= integer__last .
C12:   loop__1__i + 1 >= begidx .
C13:   loop__1__i + 1 <= endidx .
 

procedure_converttimespec_5.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   element(s, [loop__1__i]) >= 48 .
H21:   element(s, [loop__1__i]) <= 57 .
H22:   blob >= long_long_integer__first .
H23:   blob <= long_long_integer__last .
H24:   element(s, [loop__1__i]) >= character__first .
H25:   element(s, [loop__1__i]) <= character__last .
H26:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H27:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
H28:   element(s, [loop__1__i]) - 48 >= long_long_integer__base__first .
H29:   element(s, [loop__1__i]) - 48 <= long_long_integer__base__last .
H30:   10 * blob >= long_long_integer__base__first .
H31:   10 * blob <= long_long_integer__base__last .
H32:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H33:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
H34:   not (10 * blob + (element(s, [loop__1__i]) - 48) > 
           rr_type__soa_record_type__max_time_val) .
H35:   not (success = false) .
H36:   not (loop__1__i = endidx) .
        ->
C1:    10 * blob + (element(s, [loop__1__i]) - 48) >= 0 .
C2:    10 * blob + (element(s, [loop__1__i]) - 48) <= 
           rr_type__soa_record_type__max_time_val .
C3:    tmp >= 0 .
C4:    tmp <= rr_type__soa_record_type__max_time_val .
C5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
C6:    begidx >= rr_type__linelengthindex__first .
C7:    begidx <= rr_type__linelengthindex__last .
C8:    endidx >= rr_type__linelengthindex__first .
C9:    endidx <= rr_type__linelengthindex__last .
C10:   loop__1__i + 1 >= integer__first .
C11:   loop__1__i + 1 <= integer__last .
C12:   loop__1__i + 1 >= begidx .
C13:   loop__1__i + 1 <= endidx .
 

procedure_converttimespec_6.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   not ((element(s, [loop__1__i]) >= 48) and (element(s, [
           loop__1__i]) <= 57)) .
H21:   element(s, [loop__1__i]) >= character__first .
H22:   element(s, [loop__1__i]) <= character__last .
H23:   element(s, [loop__1__i]) >= character__first .
H24:   element(s, [loop__1__i]) <= character__last .
H25:   true .
H26:   ismult(element(s, [loop__1__i])) .
H27:   blob >= long_long_integer__first .
H28:   blob <= long_long_integer__last .
H29:   blob = 0 .
H30:   not (false = false) .
H31:   not (loop__1__i = endidx) .
        ->
C1:    blob >= 0 .
C2:    blob <= rr_type__soa_record_type__max_time_val .
C3:    tmp >= 0 .
C4:    tmp <= rr_type__soa_record_type__max_time_val .
C5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
C6:    begidx >= rr_type__linelengthindex__first .
C7:    begidx <= rr_type__linelengthindex__last .
C8:    endidx >= rr_type__linelengthindex__first .
C9:    endidx <= rr_type__linelengthindex__last .
C10:   loop__1__i + 1 >= integer__first .
C11:   loop__1__i + 1 <= integer__last .
C12:   loop__1__i + 1 >= begidx .
C13:   loop__1__i + 1 <= endidx .
 

procedure_converttimespec_7.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   not ((element(s, [loop__1__i]) >= 48) and (element(s, [
           loop__1__i]) <= 57)) .
H21:   element(s, [loop__1__i]) >= character__first .
H22:   element(s, [loop__1__i]) <= character__last .
H23:   element(s, [loop__1__i]) >= character__first .
H24:   element(s, [loop__1__i]) <= character__last .
H25:   true .
H26:   ismult(element(s, [loop__1__i])) .
H27:   blob >= long_long_integer__first .
H28:   blob <= long_long_integer__last .
H29:   not (blob = 0) .
H30:   blob >= long_long_integer__first .
H31:   blob <= long_long_integer__last .
H32:   element(s, [loop__1__i]) >= character__first .
H33:   element(s, [loop__1__i]) <= character__last .
H34:   ismult(element(s, [loop__1__i])) .
H35:   element(s, [loop__1__i]) >= character__first .
H36:   element(s, [loop__1__i]) <= character__last .
H37:   multvalue(element(s, [loop__1__i])) >= natural__first .
H38:   multvalue(element(s, [loop__1__i])) <= natural__last .
H39:   multvalue(element(s, [loop__1__i])) >= 0 .
H40:   multvalue(element(s, [loop__1__i])) <= 60 * 60 * 24 * 7 .
H41:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H42:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H43:   multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H44:   multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H45:   tmp >= long_long_integer__first .
H46:   tmp <= long_long_integer__last .
H47:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H48:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H49:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H50:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H51:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H52:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H53:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H54:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H55:   (blob * multvalue(element(s, [loop__1__i])) > 
           rr_type__soa_record_type__max_time_val) or (tmp + 
           blob * multvalue(element(s, [loop__1__i])) > 
           rr_type__soa_record_type__max_time_val) .
H56:   0 >= long_long_integer__first .
H57:   0 <= long_long_integer__last .
H58:   not (false = false) .
H59:   not (loop__1__i = endidx) .
        ->
C1:    0 >= 0 .
C2:    0 <= rr_type__soa_record_type__max_time_val .
C3:    tmp + blob * multvalue(element(s, [loop__1__i])) >= 0 .
C4:    tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           rr_type__soa_record_type__max_time_val .
C5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
C6:    begidx >= rr_type__linelengthindex__first .
C7:    begidx <= rr_type__linelengthindex__last .
C8:    endidx >= rr_type__linelengthindex__first .
C9:    endidx <= rr_type__linelengthindex__last .
C10:   loop__1__i + 1 >= integer__first .
C11:   loop__1__i + 1 <= integer__last .
C12:   loop__1__i + 1 >= begidx .
C13:   loop__1__i + 1 <= endidx .
 

procedure_converttimespec_8.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   not ((element(s, [loop__1__i]) >= 48) and (element(s, [
           loop__1__i]) <= 57)) .
H21:   element(s, [loop__1__i]) >= character__first .
H22:   element(s, [loop__1__i]) <= character__last .
H23:   element(s, [loop__1__i]) >= character__first .
H24:   element(s, [loop__1__i]) <= character__last .
H25:   true .
H26:   ismult(element(s, [loop__1__i])) .
H27:   blob >= long_long_integer__first .
H28:   blob <= long_long_integer__last .
H29:   not (blob = 0) .
H30:   blob >= long_long_integer__first .
H31:   blob <= long_long_integer__last .
H32:   element(s, [loop__1__i]) >= character__first .
H33:   element(s, [loop__1__i]) <= character__last .
H34:   ismult(element(s, [loop__1__i])) .
H35:   element(s, [loop__1__i]) >= character__first .
H36:   element(s, [loop__1__i]) <= character__last .
H37:   multvalue(element(s, [loop__1__i])) >= natural__first .
H38:   multvalue(element(s, [loop__1__i])) <= natural__last .
H39:   multvalue(element(s, [loop__1__i])) >= 0 .
H40:   multvalue(element(s, [loop__1__i])) <= 60 * 60 * 24 * 7 .
H41:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H42:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H43:   multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H44:   multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H45:   tmp >= long_long_integer__first .
H46:   tmp <= long_long_integer__last .
H47:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H48:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H49:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H50:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H51:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H52:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H53:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H54:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H55:   not ((blob * multvalue(element(s, [loop__1__i])) > 
           rr_type__soa_record_type__max_time_val) or (tmp + 
           blob * multvalue(element(s, [loop__1__i])) > 
           rr_type__soa_record_type__max_time_val)) .
H56:   0 >= long_long_integer__first .
H57:   0 <= long_long_integer__last .
H58:   not (success = false) .
H59:   not (loop__1__i = endidx) .
        ->
C1:    0 >= 0 .
C2:    0 <= rr_type__soa_record_type__max_time_val .
C3:    tmp + blob * multvalue(element(s, [loop__1__i])) >= 0 .
C4:    tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           rr_type__soa_record_type__max_time_val .
C5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
C6:    begidx >= rr_type__linelengthindex__first .
C7:    begidx <= rr_type__linelengthindex__last .
C8:    endidx >= rr_type__linelengthindex__first .
C9:    endidx <= rr_type__linelengthindex__last .
C10:   loop__1__i + 1 >= integer__first .
C11:   loop__1__i + 1 <= integer__last .
C12:   loop__1__i + 1 >= begidx .
C13:   loop__1__i + 1 <= endidx .
 

procedure_converttimespec_9.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   not ((element(s, [loop__1__i]) >= 48) and (element(s, [
           loop__1__i]) <= 57)) .
H21:   element(s, [loop__1__i]) >= character__first .
H22:   element(s, [loop__1__i]) <= character__last .
H23:   element(s, [loop__1__i]) >= character__first .
H24:   element(s, [loop__1__i]) <= character__last .
H25:   true .
H26:   not (ismult(element(s, [loop__1__i]))) .
H27:   not (false = false) .
H28:   not (loop__1__i = endidx) .
        ->
C1:    blob >= 0 .
C2:    blob <= rr_type__soa_record_type__max_time_val .
C3:    tmp >= 0 .
C4:    tmp <= rr_type__soa_record_type__max_time_val .
C5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
C6:    begidx >= rr_type__linelengthindex__first .
C7:    begidx <= rr_type__linelengthindex__last .
C8:    endidx >= rr_type__linelengthindex__first .
C9:    endidx <= rr_type__linelengthindex__last .
C10:   loop__1__i + 1 >= integer__first .
C11:   loop__1__i + 1 <= integer__last .
C12:   loop__1__i + 1 >= begidx .
C13:   loop__1__i + 1 <= endidx .
 

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

procedure_converttimespec_10.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
        ->
C1:    element(s, [loop__1__i]) >= character__first .
C2:    element(s, [loop__1__i]) <= character__last .
C3:    loop__1__i >= rr_type__linelengthindex__first .
C4:    loop__1__i <= rr_type__linelengthindex__last .
 

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

procedure_converttimespec_11.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   element(s, [loop__1__i]) >= 48 .
H21:   element(s, [loop__1__i]) <= 57 .
H22:   blob >= long_long_integer__first .
H23:   blob <= long_long_integer__last .
H24:   element(s, [loop__1__i]) >= character__first .
H25:   element(s, [loop__1__i]) <= character__last .
        ->
C1:    10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
C2:    10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
C3:    element(s, [loop__1__i]) - 48 >= long_long_integer__base__first .
C4:    element(s, [loop__1__i]) - 48 <= long_long_integer__base__last .
C5:    10 * blob >= long_long_integer__base__first .
C6:    10 * blob <= long_long_integer__base__last .
 

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

procedure_converttimespec_12.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   not ((element(s, [loop__1__i]) >= 48) and (element(s, [
           loop__1__i]) <= 57)) .
H21:   element(s, [loop__1__i]) >= character__first .
H22:   element(s, [loop__1__i]) <= character__last .
        ->
C1:    element(s, [loop__1__i]) >= character__first .
C2:    element(s, [loop__1__i]) <= character__last .
 

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

procedure_converttimespec_13.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   not ((element(s, [loop__1__i]) >= 48) and (element(s, [
           loop__1__i]) <= 57)) .
H21:   element(s, [loop__1__i]) >= character__first .
H22:   element(s, [loop__1__i]) <= character__last .
H23:   element(s, [loop__1__i]) >= character__first .
H24:   element(s, [loop__1__i]) <= character__last .
H25:   true .
H26:   ismult(element(s, [loop__1__i])) .
H27:   blob >= long_long_integer__first .
H28:   blob <= long_long_integer__last .
H29:   not (blob = 0) .
H30:   blob >= long_long_integer__first .
H31:   blob <= long_long_integer__last .
H32:   element(s, [loop__1__i]) >= character__first .
H33:   element(s, [loop__1__i]) <= character__last .
        ->
C1:    ismult(element(s, [loop__1__i])) .
C2:    element(s, [loop__1__i]) >= character__first .
C3:    element(s, [loop__1__i]) <= character__last .
 

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

procedure_converttimespec_14.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   not ((element(s, [loop__1__i]) >= 48) and (element(s, [
           loop__1__i]) <= 57)) .
H21:   element(s, [loop__1__i]) >= character__first .
H22:   element(s, [loop__1__i]) <= character__last .
H23:   element(s, [loop__1__i]) >= character__first .
H24:   element(s, [loop__1__i]) <= character__last .
H25:   true .
H26:   ismult(element(s, [loop__1__i])) .
H27:   blob >= long_long_integer__first .
H28:   blob <= long_long_integer__last .
H29:   not (blob = 0) .
H30:   blob >= long_long_integer__first .
H31:   blob <= long_long_integer__last .
H32:   element(s, [loop__1__i]) >= character__first .
H33:   element(s, [loop__1__i]) <= character__last .
H34:   ismult(element(s, [loop__1__i])) .
H35:   element(s, [loop__1__i]) >= character__first .
H36:   element(s, [loop__1__i]) <= character__last .
H37:   multvalue(element(s, [loop__1__i])) >= natural__first .
H38:   multvalue(element(s, [loop__1__i])) <= natural__last .
H39:   multvalue(element(s, [loop__1__i])) >= 0 .
H40:   multvalue(element(s, [loop__1__i])) <= 60 * 60 * 24 * 7 .
        ->
C1:    blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
C2:    blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
C3:    multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
C4:    multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
 

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

procedure_converttimespec_15.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   not ((element(s, [loop__1__i]) >= 48) and (element(s, [
           loop__1__i]) <= 57)) .
H21:   element(s, [loop__1__i]) >= character__first .
H22:   element(s, [loop__1__i]) <= character__last .
H23:   element(s, [loop__1__i]) >= character__first .
H24:   element(s, [loop__1__i]) <= character__last .
H25:   true .
H26:   ismult(element(s, [loop__1__i])) .
H27:   blob >= long_long_integer__first .
H28:   blob <= long_long_integer__last .
H29:   not (blob = 0) .
H30:   blob >= long_long_integer__first .
H31:   blob <= long_long_integer__last .
H32:   element(s, [loop__1__i]) >= character__first .
H33:   element(s, [loop__1__i]) <= character__last .
H34:   ismult(element(s, [loop__1__i])) .
H35:   element(s, [loop__1__i]) >= character__first .
H36:   element(s, [loop__1__i]) <= character__last .
H37:   multvalue(element(s, [loop__1__i])) >= natural__first .
H38:   multvalue(element(s, [loop__1__i])) <= natural__last .
H39:   multvalue(element(s, [loop__1__i])) >= 0 .
H40:   multvalue(element(s, [loop__1__i])) <= 60 * 60 * 24 * 7 .
H41:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H42:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H43:   multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H44:   multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H45:   tmp >= long_long_integer__first .
H46:   tmp <= long_long_integer__last .
H47:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H48:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
        ->
C1:    tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
C2:    tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
 

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

procedure_converttimespec_16.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   not ((element(s, [loop__1__i]) >= 48) and (element(s, [
           loop__1__i]) <= 57)) .
H21:   element(s, [loop__1__i]) >= character__first .
H22:   element(s, [loop__1__i]) <= character__last .
H23:   element(s, [loop__1__i]) >= character__first .
H24:   element(s, [loop__1__i]) <= character__last .
H25:   true .
H26:   ismult(element(s, [loop__1__i])) .
H27:   blob >= long_long_integer__first .
H28:   blob <= long_long_integer__last .
H29:   not (blob = 0) .
H30:   blob >= long_long_integer__first .
H31:   blob <= long_long_integer__last .
H32:   element(s, [loop__1__i]) >= character__first .
H33:   element(s, [loop__1__i]) <= character__last .
H34:   ismult(element(s, [loop__1__i])) .
H35:   element(s, [loop__1__i]) >= character__first .
H36:   element(s, [loop__1__i]) <= character__last .
H37:   multvalue(element(s, [loop__1__i])) >= natural__first .
H38:   multvalue(element(s, [loop__1__i])) <= natural__last .
H39:   multvalue(element(s, [loop__1__i])) >= 0 .
H40:   multvalue(element(s, [loop__1__i])) <= 60 * 60 * 24 * 7 .
H41:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H42:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H43:   multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H44:   multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H45:   tmp >= long_long_integer__first .
H46:   tmp <= long_long_integer__last .
H47:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H48:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H49:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H50:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H51:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H52:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H53:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H54:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H55:   (blob * multvalue(element(s, [loop__1__i])) > 
           rr_type__soa_record_type__max_time_val) or (tmp + 
           blob * multvalue(element(s, [loop__1__i])) > 
           rr_type__soa_record_type__max_time_val) .
        ->
C1:    0 >= long_long_integer__first .
C2:    0 <= long_long_integer__last .
 

procedure_converttimespec_17.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   not ((element(s, [loop__1__i]) >= 48) and (element(s, [
           loop__1__i]) <= 57)) .
H21:   element(s, [loop__1__i]) >= character__first .
H22:   element(s, [loop__1__i]) <= character__last .
H23:   element(s, [loop__1__i]) >= character__first .
H24:   element(s, [loop__1__i]) <= character__last .
H25:   true .
H26:   ismult(element(s, [loop__1__i])) .
H27:   blob >= long_long_integer__first .
H28:   blob <= long_long_integer__last .
H29:   not (blob = 0) .
H30:   blob >= long_long_integer__first .
H31:   blob <= long_long_integer__last .
H32:   element(s, [loop__1__i]) >= character__first .
H33:   element(s, [loop__1__i]) <= character__last .
H34:   ismult(element(s, [loop__1__i])) .
H35:   element(s, [loop__1__i]) >= character__first .
H36:   element(s, [loop__1__i]) <= character__last .
H37:   multvalue(element(s, [loop__1__i])) >= natural__first .
H38:   multvalue(element(s, [loop__1__i])) <= natural__last .
H39:   multvalue(element(s, [loop__1__i])) >= 0 .
H40:   multvalue(element(s, [loop__1__i])) <= 60 * 60 * 24 * 7 .
H41:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H42:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H43:   multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H44:   multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H45:   tmp >= long_long_integer__first .
H46:   tmp <= long_long_integer__last .
H47:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H48:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H49:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H50:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H51:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H52:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H53:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H54:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H55:   not ((blob * multvalue(element(s, [loop__1__i])) > 
           rr_type__soa_record_type__max_time_val) or (tmp + 
           blob * multvalue(element(s, [loop__1__i])) > 
           rr_type__soa_record_type__max_time_val)) .
        ->
C1:    0 >= long_long_integer__first .
C2:    0 <= long_long_integer__last .
 

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

procedure_converttimespec_18.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H2:    begidx >= rr_type__linelengthindex__first .
H3:    begidx <= rr_type__linelengthindex__last .
H4:    endidx >= rr_type__linelengthindex__first .
H5:    endidx <= rr_type__linelengthindex__last .
H6:    endidx >= integer__first .
H7:    endidx <= integer__last .
H8:    begidx >= integer__first .
H9:    begidx <= integer__last .
H10:   (begidx <= endidx) -> ((endidx >= integer__first) and (
           endidx <= integer__last)) .
H11:   (begidx <= endidx) -> ((begidx >= integer__first) and (
           begidx <= integer__last)) .
H12:   not (begidx <= endidx) .
H13:   not success .
        ->
C1:    0 >= long_long_integer__first .
C2:    0 <= long_long_integer__last .
 

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

procedure_converttimespec_19.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   element(s, [loop__1__i]) >= 48 .
H21:   element(s, [loop__1__i]) <= 57 .
H22:   blob >= long_long_integer__first .
H23:   blob <= long_long_integer__last .
H24:   element(s, [loop__1__i]) >= character__first .
H25:   element(s, [loop__1__i]) <= character__last .
H26:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H27:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
H28:   element(s, [loop__1__i]) - 48 >= long_long_integer__base__first .
H29:   element(s, [loop__1__i]) - 48 <= long_long_integer__base__last .
H30:   10 * blob >= long_long_integer__base__first .
H31:   10 * blob <= long_long_integer__base__last .
H32:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H33:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
H34:   10 * blob + (element(s, [loop__1__i]) - 48) > 
           rr_type__soa_record_type__max_time_val .
H35:   false = false .
H36:   not false .
        ->
C1:    0 >= long_long_integer__first .
C2:    0 <= long_long_integer__last .
 

procedure_converttimespec_20.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   element(s, [loop__1__i]) >= 48 .
H21:   element(s, [loop__1__i]) <= 57 .
H22:   blob >= long_long_integer__first .
H23:   blob <= long_long_integer__last .
H24:   element(s, [loop__1__i]) >= character__first .
H25:   element(s, [loop__1__i]) <= character__last .
H26:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H27:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
H28:   element(s, [loop__1__i]) - 48 >= long_long_integer__base__first .
H29:   element(s, [loop__1__i]) - 48 <= long_long_integer__base__last .
H30:   10 * blob >= long_long_integer__base__first .
H31:   10 * blob <= long_long_integer__base__last .
H32:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H33:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
H34:   not (10 * blob + (element(s, [loop__1__i]) - 48) > 
           rr_type__soa_record_type__max_time_val) .
H35:   success = false .
H36:   not success .
        ->
C1:    0 >= long_long_integer__first .
C2:    0 <= long_long_integer__last .
 

procedure_converttimespec_21.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   not ((element(s, [loop__1__i]) >= 48) and (element(s, [
           loop__1__i]) <= 57)) .
H21:   element(s, [loop__1__i]) >= character__first .
H22:   element(s, [loop__1__i]) <= character__last .
H23:   element(s, [loop__1__i]) >= character__first .
H24:   element(s, [loop__1__i]) <= character__last .
H25:   true .
H26:   ismult(element(s, [loop__1__i])) .
H27:   blob >= long_long_integer__first .
H28:   blob <= long_long_integer__last .
H29:   blob = 0 .
H30:   false = false .
H31:   not false .
        ->
C1:    0 >= long_long_integer__first .
C2:    0 <= long_long_integer__last .
 

procedure_converttimespec_22.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   not ((element(s, [loop__1__i]) >= 48) and (element(s, [
           loop__1__i]) <= 57)) .
H21:   element(s, [loop__1__i]) >= character__first .
H22:   element(s, [loop__1__i]) <= character__last .
H23:   element(s, [loop__1__i]) >= character__first .
H24:   element(s, [loop__1__i]) <= character__last .
H25:   true .
H26:   ismult(element(s, [loop__1__i])) .
H27:   blob >= long_long_integer__first .
H28:   blob <= long_long_integer__last .
H29:   not (blob = 0) .
H30:   blob >= long_long_integer__first .
H31:   blob <= long_long_integer__last .
H32:   element(s, [loop__1__i]) >= character__first .
H33:   element(s, [loop__1__i]) <= character__last .
H34:   ismult(element(s, [loop__1__i])) .
H35:   element(s, [loop__1__i]) >= character__first .
H36:   element(s, [loop__1__i]) <= character__last .
H37:   multvalue(element(s, [loop__1__i])) >= natural__first .
H38:   multvalue(element(s, [loop__1__i])) <= natural__last .
H39:   multvalue(element(s, [loop__1__i])) >= 0 .
H40:   multvalue(element(s, [loop__1__i])) <= 60 * 60 * 24 * 7 .
H41:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H42:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H43:   multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H44:   multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H45:   tmp >= long_long_integer__first .
H46:   tmp <= long_long_integer__last .
H47:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H48:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H49:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H50:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H51:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H52:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H53:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H54:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H55:   (blob * multvalue(element(s, [loop__1__i])) > 
           rr_type__soa_record_type__max_time_val) or (tmp + 
           blob * multvalue(element(s, [loop__1__i])) > 
           rr_type__soa_record_type__max_time_val) .
H56:   0 >= long_long_integer__first .
H57:   0 <= long_long_integer__last .
H58:   false = false .
H59:   not false .
        ->
C1:    0 >= long_long_integer__first .
C2:    0 <= long_long_integer__last .
 

procedure_converttimespec_23.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   not ((element(s, [loop__1__i]) >= 48) and (element(s, [
           loop__1__i]) <= 57)) .
H21:   element(s, [loop__1__i]) >= character__first .
H22:   element(s, [loop__1__i]) <= character__last .
H23:   element(s, [loop__1__i]) >= character__first .
H24:   element(s, [loop__1__i]) <= character__last .
H25:   true .
H26:   ismult(element(s, [loop__1__i])) .
H27:   blob >= long_long_integer__first .
H28:   blob <= long_long_integer__last .
H29:   not (blob = 0) .
H30:   blob >= long_long_integer__first .
H31:   blob <= long_long_integer__last .
H32:   element(s, [loop__1__i]) >= character__first .
H33:   element(s, [loop__1__i]) <= character__last .
H34:   ismult(element(s, [loop__1__i])) .
H35:   element(s, [loop__1__i]) >= character__first .
H36:   element(s, [loop__1__i]) <= character__last .
H37:   multvalue(element(s, [loop__1__i])) >= natural__first .
H38:   multvalue(element(s, [loop__1__i])) <= natural__last .
H39:   multvalue(element(s, [loop__1__i])) >= 0 .
H40:   multvalue(element(s, [loop__1__i])) <= 60 * 60 * 24 * 7 .
H41:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H42:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H43:   multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H44:   multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H45:   tmp >= long_long_integer__first .
H46:   tmp <= long_long_integer__last .
H47:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H48:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H49:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H50:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H51:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H52:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H53:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H54:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H55:   not ((blob * multvalue(element(s, [loop__1__i])) > 
           rr_type__soa_record_type__max_time_val) or (tmp + 
           blob * multvalue(element(s, [loop__1__i])) > 
           rr_type__soa_record_type__max_time_val)) .
H56:   0 >= long_long_integer__first .
H57:   0 <= long_long_integer__last .
H58:   success = false .
H59:   not success .
        ->
C1:    0 >= long_long_integer__first .
C2:    0 <= long_long_integer__last .
 

procedure_converttimespec_24.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   not ((element(s, [loop__1__i]) >= 48) and (element(s, [
           loop__1__i]) <= 57)) .
H21:   element(s, [loop__1__i]) >= character__first .
H22:   element(s, [loop__1__i]) <= character__last .
H23:   element(s, [loop__1__i]) >= character__first .
H24:   element(s, [loop__1__i]) <= character__last .
H25:   true .
H26:   not (ismult(element(s, [loop__1__i]))) .
H27:   false = false .
H28:   not false .
        ->
C1:    0 >= long_long_integer__first .
C2:    0 <= long_long_integer__last .
 

procedure_converttimespec_25.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   element(s, [loop__1__i]) >= 48 .
H21:   element(s, [loop__1__i]) <= 57 .
H22:   blob >= long_long_integer__first .
H23:   blob <= long_long_integer__last .
H24:   element(s, [loop__1__i]) >= character__first .
H25:   element(s, [loop__1__i]) <= character__last .
H26:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H27:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
H28:   element(s, [loop__1__i]) - 48 >= long_long_integer__base__first .
H29:   element(s, [loop__1__i]) - 48 <= long_long_integer__base__last .
H30:   10 * blob >= long_long_integer__base__first .
H31:   10 * blob <= long_long_integer__base__last .
H32:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H33:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
H34:   10 * blob + (element(s, [loop__1__i]) - 48) > 
           rr_type__soa_record_type__max_time_val .
H35:   not (false = false) .
H36:   loop__1__i = endidx .
H37:   not false .
        ->
C1:    0 >= long_long_integer__first .
C2:    0 <= long_long_integer__last .
 

procedure_converttimespec_26.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   element(s, [loop__1__i]) >= 48 .
H21:   element(s, [loop__1__i]) <= 57 .
H22:   blob >= long_long_integer__first .
H23:   blob <= long_long_integer__last .
H24:   element(s, [loop__1__i]) >= character__first .
H25:   element(s, [loop__1__i]) <= character__last .
H26:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H27:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
H28:   element(s, [loop__1__i]) - 48 >= long_long_integer__base__first .
H29:   element(s, [loop__1__i]) - 48 <= long_long_integer__base__last .
H30:   10 * blob >= long_long_integer__base__first .
H31:   10 * blob <= long_long_integer__base__last .
H32:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H33:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
H34:   not (10 * blob + (element(s, [loop__1__i]) - 48) > 
           rr_type__soa_record_type__max_time_val) .
H35:   not (success = false) .
H36:   loop__1__i = endidx .
H37:   not success .
        ->
C1:    0 >= long_long_integer__first .
C2:    0 <= long_long_integer__last .
 

procedure_converttimespec_27.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   not ((element(s, [loop__1__i]) >= 48) and (element(s, [
           loop__1__i]) <= 57)) .
H21:   element(s, [loop__1__i]) >= character__first .
H22:   element(s, [loop__1__i]) <= character__last .
H23:   element(s, [loop__1__i]) >= character__first .
H24:   element(s, [loop__1__i]) <= character__last .
H25:   true .
H26:   ismult(element(s, [loop__1__i])) .
H27:   blob >= long_long_integer__first .
H28:   blob <= long_long_integer__last .
H29:   blob = 0 .
H30:   not (false = false) .
H31:   loop__1__i = endidx .
H32:   not false .
        ->
C1:    0 >= long_long_integer__first .
C2:    0 <= long_long_integer__last .
 

procedure_converttimespec_28.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   not ((element(s, [loop__1__i]) >= 48) and (element(s, [
           loop__1__i]) <= 57)) .
H21:   element(s, [loop__1__i]) >= character__first .
H22:   element(s, [loop__1__i]) <= character__last .
H23:   element(s, [loop__1__i]) >= character__first .
H24:   element(s, [loop__1__i]) <= character__last .
H25:   true .
H26:   ismult(element(s, [loop__1__i])) .
H27:   blob >= long_long_integer__first .
H28:   blob <= long_long_integer__last .
H29:   not (blob = 0) .
H30:   blob >= long_long_integer__first .
H31:   blob <= long_long_integer__last .
H32:   element(s, [loop__1__i]) >= character__first .
H33:   element(s, [loop__1__i]) <= character__last .
H34:   ismult(element(s, [loop__1__i])) .
H35:   element(s, [loop__1__i]) >= character__first .
H36:   element(s, [loop__1__i]) <= character__last .
H37:   multvalue(element(s, [loop__1__i])) >= natural__first .
H38:   multvalue(element(s, [loop__1__i])) <= natural__last .
H39:   multvalue(element(s, [loop__1__i])) >= 0 .
H40:   multvalue(element(s, [loop__1__i])) <= 60 * 60 * 24 * 7 .
H41:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H42:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H43:   multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H44:   multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H45:   tmp >= long_long_integer__first .
H46:   tmp <= long_long_integer__last .
H47:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H48:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H49:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H50:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H51:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H52:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H53:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H54:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H55:   (blob * multvalue(element(s, [loop__1__i])) > 
           rr_type__soa_record_type__max_time_val) or (tmp + 
           blob * multvalue(element(s, [loop__1__i])) > 
           rr_type__soa_record_type__max_time_val) .
H56:   0 >= long_long_integer__first .
H57:   0 <= long_long_integer__last .
H58:   not (false = false) .
H59:   loop__1__i = endidx .
H60:   not false .
        ->
C1:    0 >= long_long_integer__first .
C2:    0 <= long_long_integer__last .
 

procedure_converttimespec_29.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   not ((element(s, [loop__1__i]) >= 48) and (element(s, [
           loop__1__i]) <= 57)) .
H21:   element(s, [loop__1__i]) >= character__first .
H22:   element(s, [loop__1__i]) <= character__last .
H23:   element(s, [loop__1__i]) >= character__first .
H24:   element(s, [loop__1__i]) <= character__last .
H25:   true .
H26:   ismult(element(s, [loop__1__i])) .
H27:   blob >= long_long_integer__first .
H28:   blob <= long_long_integer__last .
H29:   not (blob = 0) .
H30:   blob >= long_long_integer__first .
H31:   blob <= long_long_integer__last .
H32:   element(s, [loop__1__i]) >= character__first .
H33:   element(s, [loop__1__i]) <= character__last .
H34:   ismult(element(s, [loop__1__i])) .
H35:   element(s, [loop__1__i]) >= character__first .
H36:   element(s, [loop__1__i]) <= character__last .
H37:   multvalue(element(s, [loop__1__i])) >= natural__first .
H38:   multvalue(element(s, [loop__1__i])) <= natural__last .
H39:   multvalue(element(s, [loop__1__i])) >= 0 .
H40:   multvalue(element(s, [loop__1__i])) <= 60 * 60 * 24 * 7 .
H41:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H42:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H43:   multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H44:   multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H45:   tmp >= long_long_integer__first .
H46:   tmp <= long_long_integer__last .
H47:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H48:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H49:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H50:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H51:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H52:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H53:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H54:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H55:   not ((blob * multvalue(element(s, [loop__1__i])) > 
           rr_type__soa_record_type__max_time_val) or (tmp + 
           blob * multvalue(element(s, [loop__1__i])) > 
           rr_type__soa_record_type__max_time_val)) .
H56:   0 >= long_long_integer__first .
H57:   0 <= long_long_integer__last .
H58:   not (success = false) .
H59:   loop__1__i = endidx .
H60:   not success .
        ->
C1:    0 >= long_long_integer__first .
C2:    0 <= long_long_integer__last .
 

procedure_converttimespec_30.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   not ((element(s, [loop__1__i]) >= 48) and (element(s, [
           loop__1__i]) <= 57)) .
H21:   element(s, [loop__1__i]) >= character__first .
H22:   element(s, [loop__1__i]) <= character__last .
H23:   element(s, [loop__1__i]) >= character__first .
H24:   element(s, [loop__1__i]) <= character__last .
H25:   true .
H26:   not (ismult(element(s, [loop__1__i]))) .
H27:   not (false = false) .
H28:   loop__1__i = endidx .
H29:   not false .
        ->
C1:    0 >= long_long_integer__first .
C2:    0 <= long_long_integer__last .
 

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

procedure_converttimespec_31.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H2:    begidx >= rr_type__linelengthindex__first .
H3:    begidx <= rr_type__linelengthindex__last .
H4:    endidx >= rr_type__linelengthindex__first .
H5:    endidx <= rr_type__linelengthindex__last .
H6:    endidx >= integer__first .
H7:    endidx <= integer__last .
H8:    begidx >= integer__first .
H9:    begidx <= integer__last .
H10:   (begidx <= endidx) -> ((endidx >= integer__first) and (
           endidx <= integer__last)) .
H11:   (begidx <= endidx) -> ((begidx >= integer__first) and (
           begidx <= integer__last)) .
H12:   not (begidx <= endidx) .
H13:   not (not success) .
H14:   0 >= long_long_integer__first .
H15:   0 <= long_long_integer__last .
H16:   0 = 0 .
H17:   0 >= long_long_integer__first .
H18:   0 <= long_long_integer__last .
        ->
C1:    0 >= long_long_integer__first .
C2:    0 <= long_long_integer__last .
 

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

procedure_converttimespec_32.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   element(s, [loop__1__i]) >= 48 .
H21:   element(s, [loop__1__i]) <= 57 .
H22:   blob >= long_long_integer__first .
H23:   blob <= long_long_integer__last .
H24:   element(s, [loop__1__i]) >= character__first .
H25:   element(s, [loop__1__i]) <= character__last .
H26:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H27:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
H28:   element(s, [loop__1__i]) - 48 >= long_long_integer__base__first .
H29:   element(s, [loop__1__i]) - 48 <= long_long_integer__base__last .
H30:   10 * blob >= long_long_integer__base__first .
H31:   10 * blob <= long_long_integer__base__last .
H32:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H33:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
H34:   10 * blob + (element(s, [loop__1__i]) - 48) > 
           rr_type__soa_record_type__max_time_val .
H35:   false = false .
H36:   not (not false) .
H37:   tmp >= long_long_integer__first .
H38:   tmp <= long_long_integer__last .
H39:   tmp = 0 .
H40:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H41:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
        ->
C1:    10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
C2:    10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
 

procedure_converttimespec_33.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   element(s, [loop__1__i]) >= 48 .
H21:   element(s, [loop__1__i]) <= 57 .
H22:   blob >= long_long_integer__first .
H23:   blob <= long_long_integer__last .
H24:   element(s, [loop__1__i]) >= character__first .
H25:   element(s, [loop__1__i]) <= character__last .
H26:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H27:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
H28:   element(s, [loop__1__i]) - 48 >= long_long_integer__base__first .
H29:   element(s, [loop__1__i]) - 48 <= long_long_integer__base__last .
H30:   10 * blob >= long_long_integer__base__first .
H31:   10 * blob <= long_long_integer__base__last .
H32:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H33:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
H34:   not (10 * blob + (element(s, [loop__1__i]) - 48) > 
           rr_type__soa_record_type__max_time_val) .
H35:   success = false .
H36:   not (not success) .
H37:   tmp >= long_long_integer__first .
H38:   tmp <= long_long_integer__last .
H39:   tmp = 0 .
H40:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H41:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
        ->
C1:    10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
C2:    10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
 

procedure_converttimespec_34.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   not ((element(s, [loop__1__i]) >= 48) and (element(s, [
           loop__1__i]) <= 57)) .
H21:   element(s, [loop__1__i]) >= character__first .
H22:   element(s, [loop__1__i]) <= character__last .
H23:   element(s, [loop__1__i]) >= character__first .
H24:   element(s, [loop__1__i]) <= character__last .
H25:   true .
H26:   ismult(element(s, [loop__1__i])) .
H27:   blob >= long_long_integer__first .
H28:   blob <= long_long_integer__last .
H29:   blob = 0 .
H30:   false = false .
H31:   not (not false) .
H32:   tmp >= long_long_integer__first .
H33:   tmp <= long_long_integer__last .
H34:   tmp = 0 .
H35:   blob >= long_long_integer__first .
H36:   blob <= long_long_integer__last .
        ->
C1:    blob >= long_long_integer__first .
C2:    blob <= long_long_integer__last .
 

procedure_converttimespec_35.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   not ((element(s, [loop__1__i]) >= 48) and (element(s, [
           loop__1__i]) <= 57)) .
H21:   element(s, [loop__1__i]) >= character__first .
H22:   element(s, [loop__1__i]) <= character__last .
H23:   element(s, [loop__1__i]) >= character__first .
H24:   element(s, [loop__1__i]) <= character__last .
H25:   true .
H26:   ismult(element(s, [loop__1__i])) .
H27:   blob >= long_long_integer__first .
H28:   blob <= long_long_integer__last .
H29:   not (blob = 0) .
H30:   blob >= long_long_integer__first .
H31:   blob <= long_long_integer__last .
H32:   element(s, [loop__1__i]) >= character__first .
H33:   element(s, [loop__1__i]) <= character__last .
H34:   ismult(element(s, [loop__1__i])) .
H35:   element(s, [loop__1__i]) >= character__first .
H36:   element(s, [loop__1__i]) <= character__last .
H37:   multvalue(element(s, [loop__1__i])) >= natural__first .
H38:   multvalue(element(s, [loop__1__i])) <= natural__last .
H39:   multvalue(element(s, [loop__1__i])) >= 0 .
H40:   multvalue(element(s, [loop__1__i])) <= 60 * 60 * 24 * 7 .
H41:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H42:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H43:   multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H44:   multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H45:   tmp >= long_long_integer__first .
H46:   tmp <= long_long_integer__last .
H47:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H48:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H49:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H50:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H51:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H52:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H53:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H54:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H55:   (blob * multvalue(element(s, [loop__1__i])) > 
           rr_type__soa_record_type__max_time_val) or (tmp + 
           blob * multvalue(element(s, [loop__1__i])) > 
           rr_type__soa_record_type__max_time_val) .
H56:   0 >= long_long_integer__first .
H57:   0 <= long_long_integer__last .
H58:   false = false .
H59:   not (not false) .
H60:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H61:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H62:   tmp + blob * multvalue(element(s, [loop__1__i])) = 0 .
H63:   0 >= long_long_integer__first .
H64:   0 <= long_long_integer__last .
        ->
C1:    0 >= long_long_integer__first .
C2:    0 <= long_long_integer__last .
 

procedure_converttimespec_36.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   not ((element(s, [loop__1__i]) >= 48) and (element(s, [
           loop__1__i]) <= 57)) .
H21:   element(s, [loop__1__i]) >= character__first .
H22:   element(s, [loop__1__i]) <= character__last .
H23:   element(s, [loop__1__i]) >= character__first .
H24:   element(s, [loop__1__i]) <= character__last .
H25:   true .
H26:   ismult(element(s, [loop__1__i])) .
H27:   blob >= long_long_integer__first .
H28:   blob <= long_long_integer__last .
H29:   not (blob = 0) .
H30:   blob >= long_long_integer__first .
H31:   blob <= long_long_integer__last .
H32:   element(s, [loop__1__i]) >= character__first .
H33:   element(s, [loop__1__i]) <= character__last .
H34:   ismult(element(s, [loop__1__i])) .
H35:   element(s, [loop__1__i]) >= character__first .
H36:   element(s, [loop__1__i]) <= character__last .
H37:   multvalue(element(s, [loop__1__i])) >= natural__first .
H38:   multvalue(element(s, [loop__1__i])) <= natural__last .
H39:   multvalue(element(s, [loop__1__i])) >= 0 .
H40:   multvalue(element(s, [loop__1__i])) <= 60 * 60 * 24 * 7 .
H41:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H42:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H43:   multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H44:   multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H45:   tmp >= long_long_integer__first .
H46:   tmp <= long_long_integer__last .
H47:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H48:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H49:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H50:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H51:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H52:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H53:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H54:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H55:   not ((blob * multvalue(element(s, [loop__1__i])) > 
           rr_type__soa_record_type__max_time_val) or (tmp + 
           blob * multvalue(element(s, [loop__1__i])) > 
           rr_type__soa_record_type__max_time_val)) .
H56:   0 >= long_long_integer__first .
H57:   0 <= long_long_integer__last .
H58:   success = false .
H59:   not (not success) .
H60:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H61:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H62:   tmp + blob * multvalue(element(s, [loop__1__i])) = 0 .
H63:   0 >= long_long_integer__first .
H64:   0 <= long_long_integer__last .
        ->
C1:    0 >= long_long_integer__first .
C2:    0 <= long_long_integer__last .
 

procedure_converttimespec_37.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   not ((element(s, [loop__1__i]) >= 48) and (element(s, [
           loop__1__i]) <= 57)) .
H21:   element(s, [loop__1__i]) >= character__first .
H22:   element(s, [loop__1__i]) <= character__last .
H23:   element(s, [loop__1__i]) >= character__first .
H24:   element(s, [loop__1__i]) <= character__last .
H25:   true .
H26:   not (ismult(element(s, [loop__1__i]))) .
H27:   false = false .
H28:   not (not false) .
H29:   tmp >= long_long_integer__first .
H30:   tmp <= long_long_integer__last .
H31:   tmp = 0 .
H32:   blob >= long_long_integer__first .
H33:   blob <= long_long_integer__last .
        ->
C1:    blob >= long_long_integer__first .
C2:    blob <= long_long_integer__last .
 

procedure_converttimespec_38.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   element(s, [loop__1__i]) >= 48 .
H21:   element(s, [loop__1__i]) <= 57 .
H22:   blob >= long_long_integer__first .
H23:   blob <= long_long_integer__last .
H24:   element(s, [loop__1__i]) >= character__first .
H25:   element(s, [loop__1__i]) <= character__last .
H26:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H27:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
H28:   element(s, [loop__1__i]) - 48 >= long_long_integer__base__first .
H29:   element(s, [loop__1__i]) - 48 <= long_long_integer__base__last .
H30:   10 * blob >= long_long_integer__base__first .
H31:   10 * blob <= long_long_integer__base__last .
H32:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H33:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
H34:   10 * blob + (element(s, [loop__1__i]) - 48) > 
           rr_type__soa_record_type__max_time_val .
H35:   not (false = false) .
H36:   loop__1__i = endidx .
H37:   not (not false) .
H38:   tmp >= long_long_integer__first .
H39:   tmp <= long_long_integer__last .
H40:   tmp = 0 .
H41:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H42:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
        ->
C1:    10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
C2:    10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
 

procedure_converttimespec_39.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   element(s, [loop__1__i]) >= 48 .
H21:   element(s, [loop__1__i]) <= 57 .
H22:   blob >= long_long_integer__first .
H23:   blob <= long_long_integer__last .
H24:   element(s, [loop__1__i]) >= character__first .
H25:   element(s, [loop__1__i]) <= character__last .
H26:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H27:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
H28:   element(s, [loop__1__i]) - 48 >= long_long_integer__base__first .
H29:   element(s, [loop__1__i]) - 48 <= long_long_integer__base__last .
H30:   10 * blob >= long_long_integer__base__first .
H31:   10 * blob <= long_long_integer__base__last .
H32:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H33:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
H34:   not (10 * blob + (element(s, [loop__1__i]) - 48) > 
           rr_type__soa_record_type__max_time_val) .
H35:   not (success = false) .
H36:   loop__1__i = endidx .
H37:   not (not success) .
H38:   tmp >= long_long_integer__first .
H39:   tmp <= long_long_integer__last .
H40:   tmp = 0 .
H41:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H42:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
        ->
C1:    10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
C2:    10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
 

procedure_converttimespec_40.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   not ((element(s, [loop__1__i]) >= 48) and (element(s, [
           loop__1__i]) <= 57)) .
H21:   element(s, [loop__1__i]) >= character__first .
H22:   element(s, [loop__1__i]) <= character__last .
H23:   element(s, [loop__1__i]) >= character__first .
H24:   element(s, [loop__1__i]) <= character__last .
H25:   true .
H26:   ismult(element(s, [loop__1__i])) .
H27:   blob >= long_long_integer__first .
H28:   blob <= long_long_integer__last .
H29:   blob = 0 .
H30:   not (false = false) .
H31:   loop__1__i = endidx .
H32:   not (not false) .
H33:   tmp >= long_long_integer__first .
H34:   tmp <= long_long_integer__last .
H35:   tmp = 0 .
H36:   blob >= long_long_integer__first .
H37:   blob <= long_long_integer__last .
        ->
C1:    blob >= long_long_integer__first .
C2:    blob <= long_long_integer__last .
 

procedure_converttimespec_41.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   not ((element(s, [loop__1__i]) >= 48) and (element(s, [
           loop__1__i]) <= 57)) .
H21:   element(s, [loop__1__i]) >= character__first .
H22:   element(s, [loop__1__i]) <= character__last .
H23:   element(s, [loop__1__i]) >= character__first .
H24:   element(s, [loop__1__i]) <= character__last .
H25:   true .
H26:   ismult(element(s, [loop__1__i])) .
H27:   blob >= long_long_integer__first .
H28:   blob <= long_long_integer__last .
H29:   not (blob = 0) .
H30:   blob >= long_long_integer__first .
H31:   blob <= long_long_integer__last .
H32:   element(s, [loop__1__i]) >= character__first .
H33:   element(s, [loop__1__i]) <= character__last .
H34:   ismult(element(s, [loop__1__i])) .
H35:   element(s, [loop__1__i]) >= character__first .
H36:   element(s, [loop__1__i]) <= character__last .
H37:   multvalue(element(s, [loop__1__i])) >= natural__first .
H38:   multvalue(element(s, [loop__1__i])) <= natural__last .
H39:   multvalue(element(s, [loop__1__i])) >= 0 .
H40:   multvalue(element(s, [loop__1__i])) <= 60 * 60 * 24 * 7 .
H41:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H42:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H43:   multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H44:   multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H45:   tmp >= long_long_integer__first .
H46:   tmp <= long_long_integer__last .
H47:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H48:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H49:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H50:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H51:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H52:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H53:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H54:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H55:   (blob * multvalue(element(s, [loop__1__i])) > 
           rr_type__soa_record_type__max_time_val) or (tmp + 
           blob * multvalue(element(s, [loop__1__i])) > 
           rr_type__soa_record_type__max_time_val) .
H56:   0 >= long_long_integer__first .
H57:   0 <= long_long_integer__last .
H58:   not (false = false) .
H59:   loop__1__i = endidx .
H60:   not (not false) .
H61:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H62:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H63:   tmp + blob * multvalue(element(s, [loop__1__i])) = 0 .
H64:   0 >= long_long_integer__first .
H65:   0 <= long_long_integer__last .
        ->
C1:    0 >= long_long_integer__first .
C2:    0 <= long_long_integer__last .
 

procedure_converttimespec_42.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   not ((element(s, [loop__1__i]) >= 48) and (element(s, [
           loop__1__i]) <= 57)) .
H21:   element(s, [loop__1__i]) >= character__first .
H22:   element(s, [loop__1__i]) <= character__last .
H23:   element(s, [loop__1__i]) >= character__first .
H24:   element(s, [loop__1__i]) <= character__last .
H25:   true .
H26:   ismult(element(s, [loop__1__i])) .
H27:   blob >= long_long_integer__first .
H28:   blob <= long_long_integer__last .
H29:   not (blob = 0) .
H30:   blob >= long_long_integer__first .
H31:   blob <= long_long_integer__last .
H32:   element(s, [loop__1__i]) >= character__first .
H33:   element(s, [loop__1__i]) <= character__last .
H34:   ismult(element(s, [loop__1__i])) .
H35:   element(s, [loop__1__i]) >= character__first .
H36:   element(s, [loop__1__i]) <= character__last .
H37:   multvalue(element(s, [loop__1__i])) >= natural__first .
H38:   multvalue(element(s, [loop__1__i])) <= natural__last .
H39:   multvalue(element(s, [loop__1__i])) >= 0 .
H40:   multvalue(element(s, [loop__1__i])) <= 60 * 60 * 24 * 7 .
H41:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H42:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H43:   multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H44:   multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H45:   tmp >= long_long_integer__first .
H46:   tmp <= long_long_integer__last .
H47:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H48:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H49:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H50:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H51:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H52:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H53:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H54:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H55:   not ((blob * multvalue(element(s, [loop__1__i])) > 
           rr_type__soa_record_type__max_time_val) or (tmp + 
           blob * multvalue(element(s, [loop__1__i])) > 
           rr_type__soa_record_type__max_time_val)) .
H56:   0 >= long_long_integer__first .
H57:   0 <= long_long_integer__last .
H58:   not (success = false) .
H59:   loop__1__i = endidx .
H60:   not (not success) .
H61:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H62:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H63:   tmp + blob * multvalue(element(s, [loop__1__i])) = 0 .
H64:   0 >= long_long_integer__first .
H65:   0 <= long_long_integer__last .
        ->
C1:    0 >= long_long_integer__first .
C2:    0 <= long_long_integer__last .
 

procedure_converttimespec_43.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   not ((element(s, [loop__1__i]) >= 48) and (element(s, [
           loop__1__i]) <= 57)) .
H21:   element(s, [loop__1__i]) >= character__first .
H22:   element(s, [loop__1__i]) <= character__last .
H23:   element(s, [loop__1__i]) >= character__first .
H24:   element(s, [loop__1__i]) <= character__last .
H25:   true .
H26:   not (ismult(element(s, [loop__1__i]))) .
H27:   not (false = false) .
H28:   loop__1__i = endidx .
H29:   not (not false) .
H30:   tmp >= long_long_integer__first .
H31:   tmp <= long_long_integer__last .
H32:   tmp = 0 .
H33:   blob >= long_long_integer__first .
H34:   blob <= long_long_integer__last .
        ->
C1:    blob >= long_long_integer__first .
C2:    blob <= long_long_integer__last .
 

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

procedure_converttimespec_44.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H2:    begidx >= rr_type__linelengthindex__first .
H3:    begidx <= rr_type__linelengthindex__last .
H4:    endidx >= rr_type__linelengthindex__first .
H5:    endidx <= rr_type__linelengthindex__last .
H6:    endidx >= integer__first .
H7:    endidx <= integer__last .
H8:    begidx >= integer__first .
H9:    begidx <= integer__last .
H10:   (begidx <= endidx) -> ((endidx >= integer__first) and (
           endidx <= integer__last)) .
H11:   (begidx <= endidx) -> ((begidx >= integer__first) and (
           begidx <= integer__last)) .
H12:   not (begidx <= endidx) .
H13:   not success .
H14:   0 >= long_long_integer__first .
H15:   0 <= long_long_integer__last .
H16:   0 >= long_long_integer__first .
H17:   0 <= long_long_integer__last .
        ->
C1:    0 >= unsigned_types__unsigned32__first .
C2:    0 <= unsigned_types__unsigned32__last .
C3:    0 >= unsigned_types__unsigned32__first .
C4:    0 <= unsigned_types__unsigned32__last .
 

procedure_converttimespec_45.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H2:    begidx >= rr_type__linelengthindex__first .
H3:    begidx <= rr_type__linelengthindex__last .
H4:    endidx >= rr_type__linelengthindex__first .
H5:    endidx <= rr_type__linelengthindex__last .
H6:    endidx >= integer__first .
H7:    endidx <= integer__last .
H8:    begidx >= integer__first .
H9:    begidx <= integer__last .
H10:   (begidx <= endidx) -> ((endidx >= integer__first) and (
           endidx <= integer__last)) .
H11:   (begidx <= endidx) -> ((begidx >= integer__first) and (
           begidx <= integer__last)) .
H12:   not (begidx <= endidx) .
H13:   not (not success) .
H14:   0 >= long_long_integer__first .
H15:   0 <= long_long_integer__last .
H16:   0 = 0 .
H17:   0 >= long_long_integer__first .
H18:   0 <= long_long_integer__last .
H19:   0 >= long_long_integer__first .
H20:   0 <= long_long_integer__last .
H21:   0 >= long_long_integer__first .
H22:   0 <= long_long_integer__last .
        ->
C1:    0 >= unsigned_types__unsigned32__first .
C2:    0 <= unsigned_types__unsigned32__last .
C3:    0 >= unsigned_types__unsigned32__first .
C4:    0 <= unsigned_types__unsigned32__last .
 

procedure_converttimespec_46.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H2:    begidx >= rr_type__linelengthindex__first .
H3:    begidx <= rr_type__linelengthindex__last .
H4:    endidx >= rr_type__linelengthindex__first .
H5:    endidx <= rr_type__linelengthindex__last .
H6:    endidx >= integer__first .
H7:    endidx <= integer__last .
H8:    begidx >= integer__first .
H9:    begidx <= integer__last .
H10:   (begidx <= endidx) -> ((endidx >= integer__first) and (
           endidx <= integer__last)) .
H11:   (begidx <= endidx) -> ((begidx >= integer__first) and (
           begidx <= integer__last)) .
H12:   not (begidx <= endidx) .
H13:   not (not success) .
H14:   0 >= long_long_integer__first .
H15:   0 <= long_long_integer__last .
H16:   not (0 = 0) .
H17:   0 >= long_long_integer__first .
H18:   0 <= long_long_integer__last .
        ->
C1:    0 >= unsigned_types__unsigned32__first .
C2:    0 <= unsigned_types__unsigned32__last .
C3:    0 >= unsigned_types__unsigned32__first .
C4:    0 <= unsigned_types__unsigned32__last .
 

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

procedure_converttimespec_47.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   element(s, [loop__1__i]) >= 48 .
H21:   element(s, [loop__1__i]) <= 57 .
H22:   blob >= long_long_integer__first .
H23:   blob <= long_long_integer__last .
H24:   element(s, [loop__1__i]) >= character__first .
H25:   element(s, [loop__1__i]) <= character__last .
H26:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H27:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
H28:   element(s, [loop__1__i]) - 48 >= long_long_integer__base__first .
H29:   element(s, [loop__1__i]) - 48 <= long_long_integer__base__last .
H30:   10 * blob >= long_long_integer__base__first .
H31:   10 * blob <= long_long_integer__base__last .
H32:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H33:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
H34:   10 * blob + (element(s, [loop__1__i]) - 48) > 
           rr_type__soa_record_type__max_time_val .
H35:   false = false .
H36:   not false .
H37:   0 >= long_long_integer__first .
H38:   0 <= long_long_integer__last .
H39:   0 >= long_long_integer__first .
H40:   0 <= long_long_integer__last .
        ->
C1:    0 >= unsigned_types__unsigned32__first .
C2:    0 <= unsigned_types__unsigned32__last .
C3:    0 >= unsigned_types__unsigned32__first .
C4:    0 <= unsigned_types__unsigned32__last .
 

procedure_converttimespec_48.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   element(s, [loop__1__i]) >= 48 .
H21:   element(s, [loop__1__i]) <= 57 .
H22:   blob >= long_long_integer__first .
H23:   blob <= long_long_integer__last .
H24:   element(s, [loop__1__i]) >= character__first .
H25:   element(s, [loop__1__i]) <= character__last .
H26:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H27:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
H28:   element(s, [loop__1__i]) - 48 >= long_long_integer__base__first .
H29:   element(s, [loop__1__i]) - 48 <= long_long_integer__base__last .
H30:   10 * blob >= long_long_integer__base__first .
H31:   10 * blob <= long_long_integer__base__last .
H32:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H33:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
H34:   not (10 * blob + (element(s, [loop__1__i]) - 48) > 
           rr_type__soa_record_type__max_time_val) .
H35:   success = false .
H36:   not success .
H37:   0 >= long_long_integer__first .
H38:   0 <= long_long_integer__last .
H39:   0 >= long_long_integer__first .
H40:   0 <= long_long_integer__last .
        ->
C1:    0 >= unsigned_types__unsigned32__first .
C2:    0 <= unsigned_types__unsigned32__last .
C3:    0 >= unsigned_types__unsigned32__first .
C4:    0 <= unsigned_types__unsigned32__last .
 

procedure_converttimespec_49.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   not ((element(s, [loop__1__i]) >= 48) and (element(s, [
           loop__1__i]) <= 57)) .
H21:   element(s, [loop__1__i]) >= character__first .
H22:   element(s, [loop__1__i]) <= character__last .
H23:   element(s, [loop__1__i]) >= character__first .
H24:   element(s, [loop__1__i]) <= character__last .
H25:   true .
H26:   ismult(element(s, [loop__1__i])) .
H27:   blob >= long_long_integer__first .
H28:   blob <= long_long_integer__last .
H29:   blob = 0 .
H30:   false = false .
H31:   not false .
H32:   0 >= long_long_integer__first .
H33:   0 <= long_long_integer__last .
H34:   0 >= long_long_integer__first .
H35:   0 <= long_long_integer__last .
        ->
C1:    0 >= unsigned_types__unsigned32__first .
C2:    0 <= unsigned_types__unsigned32__last .
C3:    0 >= unsigned_types__unsigned32__first .
C4:    0 <= unsigned_types__unsigned32__last .
 

procedure_converttimespec_50.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   not ((element(s, [loop__1__i]) >= 48) and (element(s, [
           loop__1__i]) <= 57)) .
H21:   element(s, [loop__1__i]) >= character__first .
H22:   element(s, [loop__1__i]) <= character__last .
H23:   element(s, [loop__1__i]) >= character__first .
H24:   element(s, [loop__1__i]) <= character__last .
H25:   true .
H26:   ismult(element(s, [loop__1__i])) .
H27:   blob >= long_long_integer__first .
H28:   blob <= long_long_integer__last .
H29:   not (blob = 0) .
H30:   blob >= long_long_integer__first .
H31:   blob <= long_long_integer__last .
H32:   element(s, [loop__1__i]) >= character__first .
H33:   element(s, [loop__1__i]) <= character__last .
H34:   ismult(element(s, [loop__1__i])) .
H35:   element(s, [loop__1__i]) >= character__first .
H36:   element(s, [loop__1__i]) <= character__last .
H37:   multvalue(element(s, [loop__1__i])) >= natural__first .
H38:   multvalue(element(s, [loop__1__i])) <= natural__last .
H39:   multvalue(element(s, [loop__1__i])) >= 0 .
H40:   multvalue(element(s, [loop__1__i])) <= 60 * 60 * 24 * 7 .
H41:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H42:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H43:   multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H44:   multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H45:   tmp >= long_long_integer__first .
H46:   tmp <= long_long_integer__last .
H47:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H48:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H49:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H50:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H51:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H52:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H53:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H54:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H55:   (blob * multvalue(element(s, [loop__1__i])) > 
           rr_type__soa_record_type__max_time_val) or (tmp + 
           blob * multvalue(element(s, [loop__1__i])) > 
           rr_type__soa_record_type__max_time_val) .
H56:   0 >= long_long_integer__first .
H57:   0 <= long_long_integer__last .
H58:   false = false .
H59:   not false .
H60:   0 >= long_long_integer__first .
H61:   0 <= long_long_integer__last .
H62:   0 >= long_long_integer__first .
H63:   0 <= long_long_integer__last .
        ->
C1:    0 >= unsigned_types__unsigned32__first .
C2:    0 <= unsigned_types__unsigned32__last .
C3:    0 >= unsigned_types__unsigned32__first .
C4:    0 <= unsigned_types__unsigned32__last .
 

procedure_converttimespec_51.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   not ((element(s, [loop__1__i]) >= 48) and (element(s, [
           loop__1__i]) <= 57)) .
H21:   element(s, [loop__1__i]) >= character__first .
H22:   element(s, [loop__1__i]) <= character__last .
H23:   element(s, [loop__1__i]) >= character__first .
H24:   element(s, [loop__1__i]) <= character__last .
H25:   true .
H26:   ismult(element(s, [loop__1__i])) .
H27:   blob >= long_long_integer__first .
H28:   blob <= long_long_integer__last .
H29:   not (blob = 0) .
H30:   blob >= long_long_integer__first .
H31:   blob <= long_long_integer__last .
H32:   element(s, [loop__1__i]) >= character__first .
H33:   element(s, [loop__1__i]) <= character__last .
H34:   ismult(element(s, [loop__1__i])) .
H35:   element(s, [loop__1__i]) >= character__first .
H36:   element(s, [loop__1__i]) <= character__last .
H37:   multvalue(element(s, [loop__1__i])) >= natural__first .
H38:   multvalue(element(s, [loop__1__i])) <= natural__last .
H39:   multvalue(element(s, [loop__1__i])) >= 0 .
H40:   multvalue(element(s, [loop__1__i])) <= 60 * 60 * 24 * 7 .
H41:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H42:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H43:   multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H44:   multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H45:   tmp >= long_long_integer__first .
H46:   tmp <= long_long_integer__last .
H47:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H48:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H49:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H50:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H51:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H52:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H53:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H54:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H55:   not ((blob * multvalue(element(s, [loop__1__i])) > 
           rr_type__soa_record_type__max_time_val) or (tmp + 
           blob * multvalue(element(s, [loop__1__i])) > 
           rr_type__soa_record_type__max_time_val)) .
H56:   0 >= long_long_integer__first .
H57:   0 <= long_long_integer__last .
H58:   success = false .
H59:   not success .
H60:   0 >= long_long_integer__first .
H61:   0 <= long_long_integer__last .
H62:   0 >= long_long_integer__first .
H63:   0 <= long_long_integer__last .
        ->
C1:    0 >= unsigned_types__unsigned32__first .
C2:    0 <= unsigned_types__unsigned32__last .
C3:    0 >= unsigned_types__unsigned32__first .
C4:    0 <= unsigned_types__unsigned32__last .
 

procedure_converttimespec_52.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   not ((element(s, [loop__1__i]) >= 48) and (element(s, [
           loop__1__i]) <= 57)) .
H21:   element(s, [loop__1__i]) >= character__first .
H22:   element(s, [loop__1__i]) <= character__last .
H23:   element(s, [loop__1__i]) >= character__first .
H24:   element(s, [loop__1__i]) <= character__last .
H25:   true .
H26:   not (ismult(element(s, [loop__1__i]))) .
H27:   false = false .
H28:   not false .
H29:   0 >= long_long_integer__first .
H30:   0 <= long_long_integer__last .
H31:   0 >= long_long_integer__first .
H32:   0 <= long_long_integer__last .
        ->
C1:    0 >= unsigned_types__unsigned32__first .
C2:    0 <= unsigned_types__unsigned32__last .
C3:    0 >= unsigned_types__unsigned32__first .
C4:    0 <= unsigned_types__unsigned32__last .
 

procedure_converttimespec_53.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   element(s, [loop__1__i]) >= 48 .
H21:   element(s, [loop__1__i]) <= 57 .
H22:   blob >= long_long_integer__first .
H23:   blob <= long_long_integer__last .
H24:   element(s, [loop__1__i]) >= character__first .
H25:   element(s, [loop__1__i]) <= character__last .
H26:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H27:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
H28:   element(s, [loop__1__i]) - 48 >= long_long_integer__base__first .
H29:   element(s, [loop__1__i]) - 48 <= long_long_integer__base__last .
H30:   10 * blob >= long_long_integer__base__first .
H31:   10 * blob <= long_long_integer__base__last .
H32:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H33:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
H34:   10 * blob + (element(s, [loop__1__i]) - 48) > 
           rr_type__soa_record_type__max_time_val .
H35:   not (false = false) .
H36:   loop__1__i = endidx .
H37:   not false .
H38:   0 >= long_long_integer__first .
H39:   0 <= long_long_integer__last .
H40:   0 >= long_long_integer__first .
H41:   0 <= long_long_integer__last .
        ->
C1:    0 >= unsigned_types__unsigned32__first .
C2:    0 <= unsigned_types__unsigned32__last .
C3:    0 >= unsigned_types__unsigned32__first .
C4:    0 <= unsigned_types__unsigned32__last .
 

procedure_converttimespec_54.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   element(s, [loop__1__i]) >= 48 .
H21:   element(s, [loop__1__i]) <= 57 .
H22:   blob >= long_long_integer__first .
H23:   blob <= long_long_integer__last .
H24:   element(s, [loop__1__i]) >= character__first .
H25:   element(s, [loop__1__i]) <= character__last .
H26:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H27:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
H28:   element(s, [loop__1__i]) - 48 >= long_long_integer__base__first .
H29:   element(s, [loop__1__i]) - 48 <= long_long_integer__base__last .
H30:   10 * blob >= long_long_integer__base__first .
H31:   10 * blob <= long_long_integer__base__last .
H32:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H33:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
H34:   not (10 * blob + (element(s, [loop__1__i]) - 48) > 
           rr_type__soa_record_type__max_time_val) .
H35:   not (success = false) .
H36:   loop__1__i = endidx .
H37:   not success .
H38:   0 >= long_long_integer__first .
H39:   0 <= long_long_integer__last .
H40:   0 >= long_long_integer__first .
H41:   0 <= long_long_integer__last .
        ->
C1:    0 >= unsigned_types__unsigned32__first .
C2:    0 <= unsigned_types__unsigned32__last .
C3:    0 >= unsigned_types__unsigned32__first .
C4:    0 <= unsigned_types__unsigned32__last .
 

procedure_converttimespec_55.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   not ((element(s, [loop__1__i]) >= 48) and (element(s, [
           loop__1__i]) <= 57)) .
H21:   element(s, [loop__1__i]) >= character__first .
H22:   element(s, [loop__1__i]) <= character__last .
H23:   element(s, [loop__1__i]) >= character__first .
H24:   element(s, [loop__1__i]) <= character__last .
H25:   true .
H26:   ismult(element(s, [loop__1__i])) .
H27:   blob >= long_long_integer__first .
H28:   blob <= long_long_integer__last .
H29:   blob = 0 .
H30:   not (false = false) .
H31:   loop__1__i = endidx .
H32:   not false .
H33:   0 >= long_long_integer__first .
H34:   0 <= long_long_integer__last .
H35:   0 >= long_long_integer__first .
H36:   0 <= long_long_integer__last .
        ->
C1:    0 >= unsigned_types__unsigned32__first .
C2:    0 <= unsigned_types__unsigned32__last .
C3:    0 >= unsigned_types__unsigned32__first .
C4:    0 <= unsigned_types__unsigned32__last .
 

procedure_converttimespec_56.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   not ((element(s, [loop__1__i]) >= 48) and (element(s, [
           loop__1__i]) <= 57)) .
H21:   element(s, [loop__1__i]) >= character__first .
H22:   element(s, [loop__1__i]) <= character__last .
H23:   element(s, [loop__1__i]) >= character__first .
H24:   element(s, [loop__1__i]) <= character__last .
H25:   true .
H26:   ismult(element(s, [loop__1__i])) .
H27:   blob >= long_long_integer__first .
H28:   blob <= long_long_integer__last .
H29:   not (blob = 0) .
H30:   blob >= long_long_integer__first .
H31:   blob <= long_long_integer__last .
H32:   element(s, [loop__1__i]) >= character__first .
H33:   element(s, [loop__1__i]) <= character__last .
H34:   ismult(element(s, [loop__1__i])) .
H35:   element(s, [loop__1__i]) >= character__first .
H36:   element(s, [loop__1__i]) <= character__last .
H37:   multvalue(element(s, [loop__1__i])) >= natural__first .
H38:   multvalue(element(s, [loop__1__i])) <= natural__last .
H39:   multvalue(element(s, [loop__1__i])) >= 0 .
H40:   multvalue(element(s, [loop__1__i])) <= 60 * 60 * 24 * 7 .
H41:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H42:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H43:   multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H44:   multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H45:   tmp >= long_long_integer__first .
H46:   tmp <= long_long_integer__last .
H47:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H48:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H49:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H50:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H51:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H52:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H53:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H54:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H55:   (blob * multvalue(element(s, [loop__1__i])) > 
           rr_type__soa_record_type__max_time_val) or (tmp + 
           blob * multvalue(element(s, [loop__1__i])) > 
           rr_type__soa_record_type__max_time_val) .
H56:   0 >= long_long_integer__first .
H57:   0 <= long_long_integer__last .
H58:   not (false = false) .
H59:   loop__1__i = endidx .
H60:   not false .
H61:   0 >= long_long_integer__first .
H62:   0 <= long_long_integer__last .
H63:   0 >= long_long_integer__first .
H64:   0 <= long_long_integer__last .
        ->
C1:    0 >= unsigned_types__unsigned32__first .
C2:    0 <= unsigned_types__unsigned32__last .
C3:    0 >= unsigned_types__unsigned32__first .
C4:    0 <= unsigned_types__unsigned32__last .
 

procedure_converttimespec_57.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   not ((element(s, [loop__1__i]) >= 48) and (element(s, [
           loop__1__i]) <= 57)) .
H21:   element(s, [loop__1__i]) >= character__first .
H22:   element(s, [loop__1__i]) <= character__last .
H23:   element(s, [loop__1__i]) >= character__first .
H24:   element(s, [loop__1__i]) <= character__last .
H25:   true .
H26:   ismult(element(s, [loop__1__i])) .
H27:   blob >= long_long_integer__first .
H28:   blob <= long_long_integer__last .
H29:   not (blob = 0) .
H30:   blob >= long_long_integer__first .
H31:   blob <= long_long_integer__last .
H32:   element(s, [loop__1__i]) >= character__first .
H33:   element(s, [loop__1__i]) <= character__last .
H34:   ismult(element(s, [loop__1__i])) .
H35:   element(s, [loop__1__i]) >= character__first .
H36:   element(s, [loop__1__i]) <= character__last .
H37:   multvalue(element(s, [loop__1__i])) >= natural__first .
H38:   multvalue(element(s, [loop__1__i])) <= natural__last .
H39:   multvalue(element(s, [loop__1__i])) >= 0 .
H40:   multvalue(element(s, [loop__1__i])) <= 60 * 60 * 24 * 7 .
H41:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H42:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H43:   multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H44:   multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H45:   tmp >= long_long_integer__first .
H46:   tmp <= long_long_integer__last .
H47:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H48:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H49:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H50:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H51:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H52:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H53:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H54:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H55:   not ((blob * multvalue(element(s, [loop__1__i])) > 
           rr_type__soa_record_type__max_time_val) or (tmp + 
           blob * multvalue(element(s, [loop__1__i])) > 
           rr_type__soa_record_type__max_time_val)) .
H56:   0 >= long_long_integer__first .
H57:   0 <= long_long_integer__last .
H58:   not (success = false) .
H59:   loop__1__i = endidx .
H60:   not success .
H61:   0 >= long_long_integer__first .
H62:   0 <= long_long_integer__last .
H63:   0 >= long_long_integer__first .
H64:   0 <= long_long_integer__last .
        ->
C1:    0 >= unsigned_types__unsigned32__first .
C2:    0 <= unsigned_types__unsigned32__last .
C3:    0 >= unsigned_types__unsigned32__first .
C4:    0 <= unsigned_types__unsigned32__last .
 

procedure_converttimespec_58.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   not ((element(s, [loop__1__i]) >= 48) and (element(s, [
           loop__1__i]) <= 57)) .
H21:   element(s, [loop__1__i]) >= character__first .
H22:   element(s, [loop__1__i]) <= character__last .
H23:   element(s, [loop__1__i]) >= character__first .
H24:   element(s, [loop__1__i]) <= character__last .
H25:   true .
H26:   not (ismult(element(s, [loop__1__i]))) .
H27:   not (false = false) .
H28:   loop__1__i = endidx .
H29:   not false .
H30:   0 >= long_long_integer__first .
H31:   0 <= long_long_integer__last .
H32:   0 >= long_long_integer__first .
H33:   0 <= long_long_integer__last .
        ->
C1:    0 >= unsigned_types__unsigned32__first .
C2:    0 <= unsigned_types__unsigned32__last .
C3:    0 >= unsigned_types__unsigned32__first .
C4:    0 <= unsigned_types__unsigned32__last .
 

procedure_converttimespec_59.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   element(s, [loop__1__i]) >= 48 .
H21:   element(s, [loop__1__i]) <= 57 .
H22:   blob >= long_long_integer__first .
H23:   blob <= long_long_integer__last .
H24:   element(s, [loop__1__i]) >= character__first .
H25:   element(s, [loop__1__i]) <= character__last .
H26:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H27:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
H28:   element(s, [loop__1__i]) - 48 >= long_long_integer__base__first .
H29:   element(s, [loop__1__i]) - 48 <= long_long_integer__base__last .
H30:   10 * blob >= long_long_integer__base__first .
H31:   10 * blob <= long_long_integer__base__last .
H32:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H33:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
H34:   10 * blob + (element(s, [loop__1__i]) - 48) > 
           rr_type__soa_record_type__max_time_val .
H35:   false = false .
H36:   not (not false) .
H37:   tmp >= long_long_integer__first .
H38:   tmp <= long_long_integer__last .
H39:   tmp = 0 .
H40:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H41:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
H42:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H43:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
H44:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H45:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
        ->
C1:    10 * blob + (element(s, [loop__1__i]) - 48) >= 
           unsigned_types__unsigned32__first .
C2:    10 * blob + (element(s, [loop__1__i]) - 48) <= 
           unsigned_types__unsigned32__last .
C3:    10 * blob + (element(s, [loop__1__i]) - 48) >= 
           unsigned_types__unsigned32__first .
C4:    10 * blob + (element(s, [loop__1__i]) - 48) <= 
           unsigned_types__unsigned32__last .
 

procedure_converttimespec_60.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   element(s, [loop__1__i]) >= 48 .
H21:   element(s, [loop__1__i]) <= 57 .
H22:   blob >= long_long_integer__first .
H23:   blob <= long_long_integer__last .
H24:   element(s, [loop__1__i]) >= character__first .
H25:   element(s, [loop__1__i]) <= character__last .
H26:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H27:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
H28:   element(s, [loop__1__i]) - 48 >= long_long_integer__base__first .
H29:   element(s, [loop__1__i]) - 48 <= long_long_integer__base__last .
H30:   10 * blob >= long_long_integer__base__first .
H31:   10 * blob <= long_long_integer__base__last .
H32:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H33:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
H34:   not (10 * blob + (element(s, [loop__1__i]) - 48) > 
           rr_type__soa_record_type__max_time_val) .
H35:   success = false .
H36:   not (not success) .
H37:   tmp >= long_long_integer__first .
H38:   tmp <= long_long_integer__last .
H39:   tmp = 0 .
H40:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H41:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
H42:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H43:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
H44:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H45:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
        ->
C1:    10 * blob + (element(s, [loop__1__i]) - 48) >= 
           unsigned_types__unsigned32__first .
C2:    10 * blob + (element(s, [loop__1__i]) - 48) <= 
           unsigned_types__unsigned32__last .
C3:    10 * blob + (element(s, [loop__1__i]) - 48) >= 
           unsigned_types__unsigned32__first .
C4:    10 * blob + (element(s, [loop__1__i]) - 48) <= 
           unsigned_types__unsigned32__last .
 

procedure_converttimespec_61.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   not ((element(s, [loop__1__i]) >= 48) and (element(s, [
           loop__1__i]) <= 57)) .
H21:   element(s, [loop__1__i]) >= character__first .
H22:   element(s, [loop__1__i]) <= character__last .
H23:   element(s, [loop__1__i]) >= character__first .
H24:   element(s, [loop__1__i]) <= character__last .
H25:   true .
H26:   ismult(element(s, [loop__1__i])) .
H27:   blob >= long_long_integer__first .
H28:   blob <= long_long_integer__last .
H29:   blob = 0 .
H30:   false = false .
H31:   not (not false) .
H32:   tmp >= long_long_integer__first .
H33:   tmp <= long_long_integer__last .
H34:   tmp = 0 .
H35:   blob >= long_long_integer__first .
H36:   blob <= long_long_integer__last .
H37:   blob >= long_long_integer__first .
H38:   blob <= long_long_integer__last .
H39:   blob >= long_long_integer__first .
H40:   blob <= long_long_integer__last .
        ->
C1:    blob >= unsigned_types__unsigned32__first .
C2:    blob <= unsigned_types__unsigned32__last .
C3:    blob >= unsigned_types__unsigned32__first .
C4:    blob <= unsigned_types__unsigned32__last .
 

procedure_converttimespec_62.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   not ((element(s, [loop__1__i]) >= 48) and (element(s, [
           loop__1__i]) <= 57)) .
H21:   element(s, [loop__1__i]) >= character__first .
H22:   element(s, [loop__1__i]) <= character__last .
H23:   element(s, [loop__1__i]) >= character__first .
H24:   element(s, [loop__1__i]) <= character__last .
H25:   true .
H26:   ismult(element(s, [loop__1__i])) .
H27:   blob >= long_long_integer__first .
H28:   blob <= long_long_integer__last .
H29:   not (blob = 0) .
H30:   blob >= long_long_integer__first .
H31:   blob <= long_long_integer__last .
H32:   element(s, [loop__1__i]) >= character__first .
H33:   element(s, [loop__1__i]) <= character__last .
H34:   ismult(element(s, [loop__1__i])) .
H35:   element(s, [loop__1__i]) >= character__first .
H36:   element(s, [loop__1__i]) <= character__last .
H37:   multvalue(element(s, [loop__1__i])) >= natural__first .
H38:   multvalue(element(s, [loop__1__i])) <= natural__last .
H39:   multvalue(element(s, [loop__1__i])) >= 0 .
H40:   multvalue(element(s, [loop__1__i])) <= 60 * 60 * 24 * 7 .
H41:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H42:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H43:   multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H44:   multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H45:   tmp >= long_long_integer__first .
H46:   tmp <= long_long_integer__last .
H47:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H48:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H49:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H50:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H51:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H52:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H53:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H54:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H55:   (blob * multvalue(element(s, [loop__1__i])) > 
           rr_type__soa_record_type__max_time_val) or (tmp + 
           blob * multvalue(element(s, [loop__1__i])) > 
           rr_type__soa_record_type__max_time_val) .
H56:   0 >= long_long_integer__first .
H57:   0 <= long_long_integer__last .
H58:   false = false .
H59:   not (not false) .
H60:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H61:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H62:   tmp + blob * multvalue(element(s, [loop__1__i])) = 0 .
H63:   0 >= long_long_integer__first .
H64:   0 <= long_long_integer__last .
H65:   0 >= long_long_integer__first .
H66:   0 <= long_long_integer__last .
H67:   0 >= long_long_integer__first .
H68:   0 <= long_long_integer__last .
        ->
C1:    0 >= unsigned_types__unsigned32__first .
C2:    0 <= unsigned_types__unsigned32__last .
C3:    0 >= unsigned_types__unsigned32__first .
C4:    0 <= unsigned_types__unsigned32__last .
 

procedure_converttimespec_63.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   not ((element(s, [loop__1__i]) >= 48) and (element(s, [
           loop__1__i]) <= 57)) .
H21:   element(s, [loop__1__i]) >= character__first .
H22:   element(s, [loop__1__i]) <= character__last .
H23:   element(s, [loop__1__i]) >= character__first .
H24:   element(s, [loop__1__i]) <= character__last .
H25:   true .
H26:   ismult(element(s, [loop__1__i])) .
H27:   blob >= long_long_integer__first .
H28:   blob <= long_long_integer__last .
H29:   not (blob = 0) .
H30:   blob >= long_long_integer__first .
H31:   blob <= long_long_integer__last .
H32:   element(s, [loop__1__i]) >= character__first .
H33:   element(s, [loop__1__i]) <= character__last .
H34:   ismult(element(s, [loop__1__i])) .
H35:   element(s, [loop__1__i]) >= character__first .
H36:   element(s, [loop__1__i]) <= character__last .
H37:   multvalue(element(s, [loop__1__i])) >= natural__first .
H38:   multvalue(element(s, [loop__1__i])) <= natural__last .
H39:   multvalue(element(s, [loop__1__i])) >= 0 .
H40:   multvalue(element(s, [loop__1__i])) <= 60 * 60 * 24 * 7 .
H41:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H42:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H43:   multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H44:   multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H45:   tmp >= long_long_integer__first .
H46:   tmp <= long_long_integer__last .
H47:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H48:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H49:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H50:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H51:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H52:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H53:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H54:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H55:   not ((blob * multvalue(element(s, [loop__1__i])) > 
           rr_type__soa_record_type__max_time_val) or (tmp + 
           blob * multvalue(element(s, [loop__1__i])) > 
           rr_type__soa_record_type__max_time_val)) .
H56:   0 >= long_long_integer__first .
H57:   0 <= long_long_integer__last .
H58:   success = false .
H59:   not (not success) .
H60:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H61:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H62:   tmp + blob * multvalue(element(s, [loop__1__i])) = 0 .
H63:   0 >= long_long_integer__first .
H64:   0 <= long_long_integer__last .
H65:   0 >= long_long_integer__first .
H66:   0 <= long_long_integer__last .
H67:   0 >= long_long_integer__first .
H68:   0 <= long_long_integer__last .
        ->
C1:    0 >= unsigned_types__unsigned32__first .
C2:    0 <= unsigned_types__unsigned32__last .
C3:    0 >= unsigned_types__unsigned32__first .
C4:    0 <= unsigned_types__unsigned32__last .
 

procedure_converttimespec_64.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   not ((element(s, [loop__1__i]) >= 48) and (element(s, [
           loop__1__i]) <= 57)) .
H21:   element(s, [loop__1__i]) >= character__first .
H22:   element(s, [loop__1__i]) <= character__last .
H23:   element(s, [loop__1__i]) >= character__first .
H24:   element(s, [loop__1__i]) <= character__last .
H25:   true .
H26:   not (ismult(element(s, [loop__1__i]))) .
H27:   false = false .
H28:   not (not false) .
H29:   tmp >= long_long_integer__first .
H30:   tmp <= long_long_integer__last .
H31:   tmp = 0 .
H32:   blob >= long_long_integer__first .
H33:   blob <= long_long_integer__last .
H34:   blob >= long_long_integer__first .
H35:   blob <= long_long_integer__last .
H36:   blob >= long_long_integer__first .
H37:   blob <= long_long_integer__last .
        ->
C1:    blob >= unsigned_types__unsigned32__first .
C2:    blob <= unsigned_types__unsigned32__last .
C3:    blob >= unsigned_types__unsigned32__first .
C4:    blob <= unsigned_types__unsigned32__last .
 

procedure_converttimespec_65.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   element(s, [loop__1__i]) >= 48 .
H21:   element(s, [loop__1__i]) <= 57 .
H22:   blob >= long_long_integer__first .
H23:   blob <= long_long_integer__last .
H24:   element(s, [loop__1__i]) >= character__first .
H25:   element(s, [loop__1__i]) <= character__last .
H26:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H27:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
H28:   element(s, [loop__1__i]) - 48 >= long_long_integer__base__first .
H29:   element(s, [loop__1__i]) - 48 <= long_long_integer__base__last .
H30:   10 * blob >= long_long_integer__base__first .
H31:   10 * blob <= long_long_integer__base__last .
H32:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H33:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
H34:   10 * blob + (element(s, [loop__1__i]) - 48) > 
           rr_type__soa_record_type__max_time_val .
H35:   not (false = false) .
H36:   loop__1__i = endidx .
H37:   not (not false) .
H38:   tmp >= long_long_integer__first .
H39:   tmp <= long_long_integer__last .
H40:   tmp = 0 .
H41:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H42:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
H43:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H44:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
H45:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H46:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
        ->
C1:    10 * blob + (element(s, [loop__1__i]) - 48) >= 
           unsigned_types__unsigned32__first .
C2:    10 * blob + (element(s, [loop__1__i]) - 48) <= 
           unsigned_types__unsigned32__last .
C3:    10 * blob + (element(s, [loop__1__i]) - 48) >= 
           unsigned_types__unsigned32__first .
C4:    10 * blob + (element(s, [loop__1__i]) - 48) <= 
           unsigned_types__unsigned32__last .
 

procedure_converttimespec_66.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   element(s, [loop__1__i]) >= 48 .
H21:   element(s, [loop__1__i]) <= 57 .
H22:   blob >= long_long_integer__first .
H23:   blob <= long_long_integer__last .
H24:   element(s, [loop__1__i]) >= character__first .
H25:   element(s, [loop__1__i]) <= character__last .
H26:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H27:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
H28:   element(s, [loop__1__i]) - 48 >= long_long_integer__base__first .
H29:   element(s, [loop__1__i]) - 48 <= long_long_integer__base__last .
H30:   10 * blob >= long_long_integer__base__first .
H31:   10 * blob <= long_long_integer__base__last .
H32:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H33:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
H34:   not (10 * blob + (element(s, [loop__1__i]) - 48) > 
           rr_type__soa_record_type__max_time_val) .
H35:   not (success = false) .
H36:   loop__1__i = endidx .
H37:   not (not success) .
H38:   tmp >= long_long_integer__first .
H39:   tmp <= long_long_integer__last .
H40:   tmp = 0 .
H41:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H42:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
H43:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H44:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
H45:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H46:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
        ->
C1:    10 * blob + (element(s, [loop__1__i]) - 48) >= 
           unsigned_types__unsigned32__first .
C2:    10 * blob + (element(s, [loop__1__i]) - 48) <= 
           unsigned_types__unsigned32__last .
C3:    10 * blob + (element(s, [loop__1__i]) - 48) >= 
           unsigned_types__unsigned32__first .
C4:    10 * blob + (element(s, [loop__1__i]) - 48) <= 
           unsigned_types__unsigned32__last .
 

procedure_converttimespec_67.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   not ((element(s, [loop__1__i]) >= 48) and (element(s, [
           loop__1__i]) <= 57)) .
H21:   element(s, [loop__1__i]) >= character__first .
H22:   element(s, [loop__1__i]) <= character__last .
H23:   element(s, [loop__1__i]) >= character__first .
H24:   element(s, [loop__1__i]) <= character__last .
H25:   true .
H26:   ismult(element(s, [loop__1__i])) .
H27:   blob >= long_long_integer__first .
H28:   blob <= long_long_integer__last .
H29:   blob = 0 .
H30:   not (false = false) .
H31:   loop__1__i = endidx .
H32:   not (not false) .
H33:   tmp >= long_long_integer__first .
H34:   tmp <= long_long_integer__last .
H35:   tmp = 0 .
H36:   blob >= long_long_integer__first .
H37:   blob <= long_long_integer__last .
H38:   blob >= long_long_integer__first .
H39:   blob <= long_long_integer__last .
H40:   blob >= long_long_integer__first .
H41:   blob <= long_long_integer__last .
        ->
C1:    blob >= unsigned_types__unsigned32__first .
C2:    blob <= unsigned_types__unsigned32__last .
C3:    blob >= unsigned_types__unsigned32__first .
C4:    blob <= unsigned_types__unsigned32__last .
 

procedure_converttimespec_68.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   not ((element(s, [loop__1__i]) >= 48) and (element(s, [
           loop__1__i]) <= 57)) .
H21:   element(s, [loop__1__i]) >= character__first .
H22:   element(s, [loop__1__i]) <= character__last .
H23:   element(s, [loop__1__i]) >= character__first .
H24:   element(s, [loop__1__i]) <= character__last .
H25:   true .
H26:   ismult(element(s, [loop__1__i])) .
H27:   blob >= long_long_integer__first .
H28:   blob <= long_long_integer__last .
H29:   not (blob = 0) .
H30:   blob >= long_long_integer__first .
H31:   blob <= long_long_integer__last .
H32:   element(s, [loop__1__i]) >= character__first .
H33:   element(s, [loop__1__i]) <= character__last .
H34:   ismult(element(s, [loop__1__i])) .
H35:   element(s, [loop__1__i]) >= character__first .
H36:   element(s, [loop__1__i]) <= character__last .
H37:   multvalue(element(s, [loop__1__i])) >= natural__first .
H38:   multvalue(element(s, [loop__1__i])) <= natural__last .
H39:   multvalue(element(s, [loop__1__i])) >= 0 .
H40:   multvalue(element(s, [loop__1__i])) <= 60 * 60 * 24 * 7 .
H41:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H42:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H43:   multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H44:   multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H45:   tmp >= long_long_integer__first .
H46:   tmp <= long_long_integer__last .
H47:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H48:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H49:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H50:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H51:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H52:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H53:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H54:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H55:   (blob * multvalue(element(s, [loop__1__i])) > 
           rr_type__soa_record_type__max_time_val) or (tmp + 
           blob * multvalue(element(s, [loop__1__i])) > 
           rr_type__soa_record_type__max_time_val) .
H56:   0 >= long_long_integer__first .
H57:   0 <= long_long_integer__last .
H58:   not (false = false) .
H59:   loop__1__i = endidx .
H60:   not (not false) .
H61:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H62:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H63:   tmp + blob * multvalue(element(s, [loop__1__i])) = 0 .
H64:   0 >= long_long_integer__first .
H65:   0 <= long_long_integer__last .
H66:   0 >= long_long_integer__first .
H67:   0 <= long_long_integer__last .
H68:   0 >= long_long_integer__first .
H69:   0 <= long_long_integer__last .
        ->
C1:    0 >= unsigned_types__unsigned32__first .
C2:    0 <= unsigned_types__unsigned32__last .
C3:    0 >= unsigned_types__unsigned32__first .
C4:    0 <= unsigned_types__unsigned32__last .
 

procedure_converttimespec_69.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   not ((element(s, [loop__1__i]) >= 48) and (element(s, [
           loop__1__i]) <= 57)) .
H21:   element(s, [loop__1__i]) >= character__first .
H22:   element(s, [loop__1__i]) <= character__last .
H23:   element(s, [loop__1__i]) >= character__first .
H24:   element(s, [loop__1__i]) <= character__last .
H25:   true .
H26:   ismult(element(s, [loop__1__i])) .
H27:   blob >= long_long_integer__first .
H28:   blob <= long_long_integer__last .
H29:   not (blob = 0) .
H30:   blob >= long_long_integer__first .
H31:   blob <= long_long_integer__last .
H32:   element(s, [loop__1__i]) >= character__first .
H33:   element(s, [loop__1__i]) <= character__last .
H34:   ismult(element(s, [loop__1__i])) .
H35:   element(s, [loop__1__i]) >= character__first .
H36:   element(s, [loop__1__i]) <= character__last .
H37:   multvalue(element(s, [loop__1__i])) >= natural__first .
H38:   multvalue(element(s, [loop__1__i])) <= natural__last .
H39:   multvalue(element(s, [loop__1__i])) >= 0 .
H40:   multvalue(element(s, [loop__1__i])) <= 60 * 60 * 24 * 7 .
H41:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H42:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H43:   multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H44:   multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H45:   tmp >= long_long_integer__first .
H46:   tmp <= long_long_integer__last .
H47:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H48:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H49:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H50:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H51:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H52:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H53:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H54:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H55:   not ((blob * multvalue(element(s, [loop__1__i])) > 
           rr_type__soa_record_type__max_time_val) or (tmp + 
           blob * multvalue(element(s, [loop__1__i])) > 
           rr_type__soa_record_type__max_time_val)) .
H56:   0 >= long_long_integer__first .
H57:   0 <= long_long_integer__last .
H58:   not (success = false) .
H59:   loop__1__i = endidx .
H60:   not (not success) .
H61:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H62:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H63:   tmp + blob * multvalue(element(s, [loop__1__i])) = 0 .
H64:   0 >= long_long_integer__first .
H65:   0 <= long_long_integer__last .
H66:   0 >= long_long_integer__first .
H67:   0 <= long_long_integer__last .
H68:   0 >= long_long_integer__first .
H69:   0 <= long_long_integer__last .
        ->
C1:    0 >= unsigned_types__unsigned32__first .
C2:    0 <= unsigned_types__unsigned32__last .
C3:    0 >= unsigned_types__unsigned32__first .
C4:    0 <= unsigned_types__unsigned32__last .
 

procedure_converttimespec_70.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   not ((element(s, [loop__1__i]) >= 48) and (element(s, [
           loop__1__i]) <= 57)) .
H21:   element(s, [loop__1__i]) >= character__first .
H22:   element(s, [loop__1__i]) <= character__last .
H23:   element(s, [loop__1__i]) >= character__first .
H24:   element(s, [loop__1__i]) <= character__last .
H25:   true .
H26:   not (ismult(element(s, [loop__1__i]))) .
H27:   not (false = false) .
H28:   loop__1__i = endidx .
H29:   not (not false) .
H30:   tmp >= long_long_integer__first .
H31:   tmp <= long_long_integer__last .
H32:   tmp = 0 .
H33:   blob >= long_long_integer__first .
H34:   blob <= long_long_integer__last .
H35:   blob >= long_long_integer__first .
H36:   blob <= long_long_integer__last .
H37:   blob >= long_long_integer__first .
H38:   blob <= long_long_integer__last .
        ->
C1:    blob >= unsigned_types__unsigned32__first .
C2:    blob <= unsigned_types__unsigned32__last .
C3:    blob >= unsigned_types__unsigned32__first .
C4:    blob <= unsigned_types__unsigned32__last .
 

procedure_converttimespec_71.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   element(s, [loop__1__i]) >= 48 .
H21:   element(s, [loop__1__i]) <= 57 .
H22:   blob >= long_long_integer__first .
H23:   blob <= long_long_integer__last .
H24:   element(s, [loop__1__i]) >= character__first .
H25:   element(s, [loop__1__i]) <= character__last .
H26:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H27:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
H28:   element(s, [loop__1__i]) - 48 >= long_long_integer__base__first .
H29:   element(s, [loop__1__i]) - 48 <= long_long_integer__base__last .
H30:   10 * blob >= long_long_integer__base__first .
H31:   10 * blob <= long_long_integer__base__last .
H32:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H33:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
H34:   10 * blob + (element(s, [loop__1__i]) - 48) > 
           rr_type__soa_record_type__max_time_val .
H35:   false = false .
H36:   not (not false) .
H37:   tmp >= long_long_integer__first .
H38:   tmp <= long_long_integer__last .
H39:   not (tmp = 0) .
H40:   tmp >= long_long_integer__first .
H41:   tmp <= long_long_integer__last .
        ->
C1:    tmp >= unsigned_types__unsigned32__first .
C2:    tmp <= unsigned_types__unsigned32__last .
C3:    tmp >= unsigned_types__unsigned32__first .
C4:    tmp <= unsigned_types__unsigned32__last .
 

procedure_converttimespec_72.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   element(s, [loop__1__i]) >= 48 .
H21:   element(s, [loop__1__i]) <= 57 .
H22:   blob >= long_long_integer__first .
H23:   blob <= long_long_integer__last .
H24:   element(s, [loop__1__i]) >= character__first .
H25:   element(s, [loop__1__i]) <= character__last .
H26:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H27:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
H28:   element(s, [loop__1__i]) - 48 >= long_long_integer__base__first .
H29:   element(s, [loop__1__i]) - 48 <= long_long_integer__base__last .
H30:   10 * blob >= long_long_integer__base__first .
H31:   10 * blob <= long_long_integer__base__last .
H32:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H33:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
H34:   not (10 * blob + (element(s, [loop__1__i]) - 48) > 
           rr_type__soa_record_type__max_time_val) .
H35:   success = false .
H36:   not (not success) .
H37:   tmp >= long_long_integer__first .
H38:   tmp <= long_long_integer__last .
H39:   not (tmp = 0) .
H40:   tmp >= long_long_integer__first .
H41:   tmp <= long_long_integer__last .
        ->
C1:    tmp >= unsigned_types__unsigned32__first .
C2:    tmp <= unsigned_types__unsigned32__last .
C3:    tmp >= unsigned_types__unsigned32__first .
C4:    tmp <= unsigned_types__unsigned32__last .
 

procedure_converttimespec_73.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   not ((element(s, [loop__1__i]) >= 48) and (element(s, [
           loop__1__i]) <= 57)) .
H21:   element(s, [loop__1__i]) >= character__first .
H22:   element(s, [loop__1__i]) <= character__last .
H23:   element(s, [loop__1__i]) >= character__first .
H24:   element(s, [loop__1__i]) <= character__last .
H25:   true .
H26:   ismult(element(s, [loop__1__i])) .
H27:   blob >= long_long_integer__first .
H28:   blob <= long_long_integer__last .
H29:   blob = 0 .
H30:   false = false .
H31:   not (not false) .
H32:   tmp >= long_long_integer__first .
H33:   tmp <= long_long_integer__last .
H34:   not (tmp = 0) .
H35:   tmp >= long_long_integer__first .
H36:   tmp <= long_long_integer__last .
        ->
C1:    tmp >= unsigned_types__unsigned32__first .
C2:    tmp <= unsigned_types__unsigned32__last .
C3:    tmp >= unsigned_types__unsigned32__first .
C4:    tmp <= unsigned_types__unsigned32__last .
 

procedure_converttimespec_74.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   not ((element(s, [loop__1__i]) >= 48) and (element(s, [
           loop__1__i]) <= 57)) .
H21:   element(s, [loop__1__i]) >= character__first .
H22:   element(s, [loop__1__i]) <= character__last .
H23:   element(s, [loop__1__i]) >= character__first .
H24:   element(s, [loop__1__i]) <= character__last .
H25:   true .
H26:   ismult(element(s, [loop__1__i])) .
H27:   blob >= long_long_integer__first .
H28:   blob <= long_long_integer__last .
H29:   not (blob = 0) .
H30:   blob >= long_long_integer__first .
H31:   blob <= long_long_integer__last .
H32:   element(s, [loop__1__i]) >= character__first .
H33:   element(s, [loop__1__i]) <= character__last .
H34:   ismult(element(s, [loop__1__i])) .
H35:   element(s, [loop__1__i]) >= character__first .
H36:   element(s, [loop__1__i]) <= character__last .
H37:   multvalue(element(s, [loop__1__i])) >= natural__first .
H38:   multvalue(element(s, [loop__1__i])) <= natural__last .
H39:   multvalue(element(s, [loop__1__i])) >= 0 .
H40:   multvalue(element(s, [loop__1__i])) <= 60 * 60 * 24 * 7 .
H41:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H42:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H43:   multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H44:   multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H45:   tmp >= long_long_integer__first .
H46:   tmp <= long_long_integer__last .
H47:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H48:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H49:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H50:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H51:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H52:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H53:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H54:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H55:   (blob * multvalue(element(s, [loop__1__i])) > 
           rr_type__soa_record_type__max_time_val) or (tmp + 
           blob * multvalue(element(s, [loop__1__i])) > 
           rr_type__soa_record_type__max_time_val) .
H56:   0 >= long_long_integer__first .
H57:   0 <= long_long_integer__last .
H58:   false = false .
H59:   not (not false) .
H60:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H61:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H62:   not (tmp + blob * multvalue(element(s, [loop__1__i])) = 0) .
H63:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H64:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
        ->
C1:    tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           unsigned_types__unsigned32__first .
C2:    tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           unsigned_types__unsigned32__last .
C3:    tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           unsigned_types__unsigned32__first .
C4:    tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           unsigned_types__unsigned32__last .
 

procedure_converttimespec_75.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   not ((element(s, [loop__1__i]) >= 48) and (element(s, [
           loop__1__i]) <= 57)) .
H21:   element(s, [loop__1__i]) >= character__first .
H22:   element(s, [loop__1__i]) <= character__last .
H23:   element(s, [loop__1__i]) >= character__first .
H24:   element(s, [loop__1__i]) <= character__last .
H25:   true .
H26:   ismult(element(s, [loop__1__i])) .
H27:   blob >= long_long_integer__first .
H28:   blob <= long_long_integer__last .
H29:   not (blob = 0) .
H30:   blob >= long_long_integer__first .
H31:   blob <= long_long_integer__last .
H32:   element(s, [loop__1__i]) >= character__first .
H33:   element(s, [loop__1__i]) <= character__last .
H34:   ismult(element(s, [loop__1__i])) .
H35:   element(s, [loop__1__i]) >= character__first .
H36:   element(s, [loop__1__i]) <= character__last .
H37:   multvalue(element(s, [loop__1__i])) >= natural__first .
H38:   multvalue(element(s, [loop__1__i])) <= natural__last .
H39:   multvalue(element(s, [loop__1__i])) >= 0 .
H40:   multvalue(element(s, [loop__1__i])) <= 60 * 60 * 24 * 7 .
H41:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H42:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H43:   multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H44:   multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H45:   tmp >= long_long_integer__first .
H46:   tmp <= long_long_integer__last .
H47:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H48:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H49:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H50:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H51:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H52:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H53:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H54:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H55:   not ((blob * multvalue(element(s, [loop__1__i])) > 
           rr_type__soa_record_type__max_time_val) or (tmp + 
           blob * multvalue(element(s, [loop__1__i])) > 
           rr_type__soa_record_type__max_time_val)) .
H56:   0 >= long_long_integer__first .
H57:   0 <= long_long_integer__last .
H58:   success = false .
H59:   not (not success) .
H60:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H61:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H62:   not (tmp + blob * multvalue(element(s, [loop__1__i])) = 0) .
H63:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H64:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
        ->
C1:    tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           unsigned_types__unsigned32__first .
C2:    tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           unsigned_types__unsigned32__last .
C3:    tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           unsigned_types__unsigned32__first .
C4:    tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           unsigned_types__unsigned32__last .
 

procedure_converttimespec_76.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   not ((element(s, [loop__1__i]) >= 48) and (element(s, [
           loop__1__i]) <= 57)) .
H21:   element(s, [loop__1__i]) >= character__first .
H22:   element(s, [loop__1__i]) <= character__last .
H23:   element(s, [loop__1__i]) >= character__first .
H24:   element(s, [loop__1__i]) <= character__last .
H25:   true .
H26:   not (ismult(element(s, [loop__1__i]))) .
H27:   false = false .
H28:   not (not false) .
H29:   tmp >= long_long_integer__first .
H30:   tmp <= long_long_integer__last .
H31:   not (tmp = 0) .
H32:   tmp >= long_long_integer__first .
H33:   tmp <= long_long_integer__last .
        ->
C1:    tmp >= unsigned_types__unsigned32__first .
C2:    tmp <= unsigned_types__unsigned32__last .
C3:    tmp >= unsigned_types__unsigned32__first .
C4:    tmp <= unsigned_types__unsigned32__last .
 

procedure_converttimespec_77.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   element(s, [loop__1__i]) >= 48 .
H21:   element(s, [loop__1__i]) <= 57 .
H22:   blob >= long_long_integer__first .
H23:   blob <= long_long_integer__last .
H24:   element(s, [loop__1__i]) >= character__first .
H25:   element(s, [loop__1__i]) <= character__last .
H26:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H27:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
H28:   element(s, [loop__1__i]) - 48 >= long_long_integer__base__first .
H29:   element(s, [loop__1__i]) - 48 <= long_long_integer__base__last .
H30:   10 * blob >= long_long_integer__base__first .
H31:   10 * blob <= long_long_integer__base__last .
H32:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H33:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
H34:   10 * blob + (element(s, [loop__1__i]) - 48) > 
           rr_type__soa_record_type__max_time_val .
H35:   not (false = false) .
H36:   loop__1__i = endidx .
H37:   not (not false) .
H38:   tmp >= long_long_integer__first .
H39:   tmp <= long_long_integer__last .
H40:   not (tmp = 0) .
H41:   tmp >= long_long_integer__first .
H42:   tmp <= long_long_integer__last .
        ->
C1:    tmp >= unsigned_types__unsigned32__first .
C2:    tmp <= unsigned_types__unsigned32__last .
C3:    tmp >= unsigned_types__unsigned32__first .
C4:    tmp <= unsigned_types__unsigned32__last .
 

procedure_converttimespec_78.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   element(s, [loop__1__i]) >= 48 .
H21:   element(s, [loop__1__i]) <= 57 .
H22:   blob >= long_long_integer__first .
H23:   blob <= long_long_integer__last .
H24:   element(s, [loop__1__i]) >= character__first .
H25:   element(s, [loop__1__i]) <= character__last .
H26:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H27:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
H28:   element(s, [loop__1__i]) - 48 >= long_long_integer__base__first .
H29:   element(s, [loop__1__i]) - 48 <= long_long_integer__base__last .
H30:   10 * blob >= long_long_integer__base__first .
H31:   10 * blob <= long_long_integer__base__last .
H32:   10 * blob + (element(s, [loop__1__i]) - 48) >= 
           long_long_integer__first .
H33:   10 * blob + (element(s, [loop__1__i]) - 48) <= 
           long_long_integer__last .
H34:   not (10 * blob + (element(s, [loop__1__i]) - 48) > 
           rr_type__soa_record_type__max_time_val) .
H35:   not (success = false) .
H36:   loop__1__i = endidx .
H37:   not (not success) .
H38:   tmp >= long_long_integer__first .
H39:   tmp <= long_long_integer__last .
H40:   not (tmp = 0) .
H41:   tmp >= long_long_integer__first .
H42:   tmp <= long_long_integer__last .
        ->
C1:    tmp >= unsigned_types__unsigned32__first .
C2:    tmp <= unsigned_types__unsigned32__last .
C3:    tmp >= unsigned_types__unsigned32__first .
C4:    tmp <= unsigned_types__unsigned32__last .
 

procedure_converttimespec_79.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   not ((element(s, [loop__1__i]) >= 48) and (element(s, [
           loop__1__i]) <= 57)) .
H21:   element(s, [loop__1__i]) >= character__first .
H22:   element(s, [loop__1__i]) <= character__last .
H23:   element(s, [loop__1__i]) >= character__first .
H24:   element(s, [loop__1__i]) <= character__last .
H25:   true .
H26:   ismult(element(s, [loop__1__i])) .
H27:   blob >= long_long_integer__first .
H28:   blob <= long_long_integer__last .
H29:   blob = 0 .
H30:   not (false = false) .
H31:   loop__1__i = endidx .
H32:   not (not false) .
H33:   tmp >= long_long_integer__first .
H34:   tmp <= long_long_integer__last .
H35:   not (tmp = 0) .
H36:   tmp >= long_long_integer__first .
H37:   tmp <= long_long_integer__last .
        ->
C1:    tmp >= unsigned_types__unsigned32__first .
C2:    tmp <= unsigned_types__unsigned32__last .
C3:    tmp >= unsigned_types__unsigned32__first .
C4:    tmp <= unsigned_types__unsigned32__last .
 

procedure_converttimespec_80.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   not ((element(s, [loop__1__i]) >= 48) and (element(s, [
           loop__1__i]) <= 57)) .
H21:   element(s, [loop__1__i]) >= character__first .
H22:   element(s, [loop__1__i]) <= character__last .
H23:   element(s, [loop__1__i]) >= character__first .
H24:   element(s, [loop__1__i]) <= character__last .
H25:   true .
H26:   ismult(element(s, [loop__1__i])) .
H27:   blob >= long_long_integer__first .
H28:   blob <= long_long_integer__last .
H29:   not (blob = 0) .
H30:   blob >= long_long_integer__first .
H31:   blob <= long_long_integer__last .
H32:   element(s, [loop__1__i]) >= character__first .
H33:   element(s, [loop__1__i]) <= character__last .
H34:   ismult(element(s, [loop__1__i])) .
H35:   element(s, [loop__1__i]) >= character__first .
H36:   element(s, [loop__1__i]) <= character__last .
H37:   multvalue(element(s, [loop__1__i])) >= natural__first .
H38:   multvalue(element(s, [loop__1__i])) <= natural__last .
H39:   multvalue(element(s, [loop__1__i])) >= 0 .
H40:   multvalue(element(s, [loop__1__i])) <= 60 * 60 * 24 * 7 .
H41:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H42:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H43:   multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H44:   multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H45:   tmp >= long_long_integer__first .
H46:   tmp <= long_long_integer__last .
H47:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H48:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H49:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H50:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H51:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H52:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H53:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H54:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H55:   (blob * multvalue(element(s, [loop__1__i])) > 
           rr_type__soa_record_type__max_time_val) or (tmp + 
           blob * multvalue(element(s, [loop__1__i])) > 
           rr_type__soa_record_type__max_time_val) .
H56:   0 >= long_long_integer__first .
H57:   0 <= long_long_integer__last .
H58:   not (false = false) .
H59:   loop__1__i = endidx .
H60:   not (not false) .
H61:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H62:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H63:   not (tmp + blob * multvalue(element(s, [loop__1__i])) = 0) .
H64:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H65:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
        ->
C1:    tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           unsigned_types__unsigned32__first .
C2:    tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           unsigned_types__unsigned32__last .
C3:    tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           unsigned_types__unsigned32__first .
C4:    tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           unsigned_types__unsigned32__last .
 

procedure_converttimespec_81.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   not ((element(s, [loop__1__i]) >= 48) and (element(s, [
           loop__1__i]) <= 57)) .
H21:   element(s, [loop__1__i]) >= character__first .
H22:   element(s, [loop__1__i]) <= character__last .
H23:   element(s, [loop__1__i]) >= character__first .
H24:   element(s, [loop__1__i]) <= character__last .
H25:   true .
H26:   ismult(element(s, [loop__1__i])) .
H27:   blob >= long_long_integer__first .
H28:   blob <= long_long_integer__last .
H29:   not (blob = 0) .
H30:   blob >= long_long_integer__first .
H31:   blob <= long_long_integer__last .
H32:   element(s, [loop__1__i]) >= character__first .
H33:   element(s, [loop__1__i]) <= character__last .
H34:   ismult(element(s, [loop__1__i])) .
H35:   element(s, [loop__1__i]) >= character__first .
H36:   element(s, [loop__1__i]) <= character__last .
H37:   multvalue(element(s, [loop__1__i])) >= natural__first .
H38:   multvalue(element(s, [loop__1__i])) <= natural__last .
H39:   multvalue(element(s, [loop__1__i])) >= 0 .
H40:   multvalue(element(s, [loop__1__i])) <= 60 * 60 * 24 * 7 .
H41:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H42:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H43:   multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H44:   multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H45:   tmp >= long_long_integer__first .
H46:   tmp <= long_long_integer__last .
H47:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H48:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H49:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H50:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H51:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H52:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H53:   blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H54:   blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H55:   not ((blob * multvalue(element(s, [loop__1__i])) > 
           rr_type__soa_record_type__max_time_val) or (tmp + 
           blob * multvalue(element(s, [loop__1__i])) > 
           rr_type__soa_record_type__max_time_val)) .
H56:   0 >= long_long_integer__first .
H57:   0 <= long_long_integer__last .
H58:   not (success = false) .
H59:   loop__1__i = endidx .
H60:   not (not success) .
H61:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H62:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
H63:   not (tmp + blob * multvalue(element(s, [loop__1__i])) = 0) .
H64:   tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           long_long_integer__first .
H65:   tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           long_long_integer__last .
        ->
C1:    tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           unsigned_types__unsigned32__first .
C2:    tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           unsigned_types__unsigned32__last .
C3:    tmp + blob * multvalue(element(s, [loop__1__i])) >= 
           unsigned_types__unsigned32__first .
C4:    tmp + blob * multvalue(element(s, [loop__1__i])) <= 
           unsigned_types__unsigned32__last .
 

procedure_converttimespec_82.
H1:    blob >= 0 .
H2:    blob <= rr_type__soa_record_type__max_time_val .
H3:    tmp >= 0 .
H4:    tmp <= rr_type__soa_record_type__max_time_val .
H5:    for_all(i___1: integer, ((i___1 >= 
           rr_type__linelengthindex__first) and (i___1 <= 
           rr_type__linelengthindex__last)) -> ((element(s, [
           i___1]) >= character__first) and (element(s, [
           i___1]) <= character__last))) .
H6:    begidx >= rr_type__linelengthindex__first .
H7:    begidx <= rr_type__linelengthindex__last .
H8:    endidx >= rr_type__linelengthindex__first .
H9:    endidx <= rr_type__linelengthindex__last .
H10:   loop__1__i >= integer__first .
H11:   loop__1__i <= integer__last .
H12:   loop__1__i >= begidx .
H13:   loop__1__i <= endidx .
H14:   element(s, [loop__1__i]) >= character__first .
H15:   element(s, [loop__1__i]) <= character__last .
H16:   loop__1__i >= rr_type__linelengthindex__first .
H17:   loop__1__i <= rr_type__linelengthindex__last .
H18:   element(s, [loop__1__i]) >= character__first .
H19:   element(s, [loop__1__i]) <= character__last .
H20:   not ((element(s, [loop__1__i]) >= 48) and (element(s, [
           loop__1__i]) <= 57)) .
H21:   element(s, [loop__1__i]) >= character__first .
H22:   element(s, [loop__1__i]) <= character__last .
H23:   element(s, [loop__1__i]) >= character__first .
H24:   element(s, [loop__1__i]) <= character__last .
H25:   true .
H26:   not (ismult(element(s, [loop__1__i]))) .
H27:   not (false = false) .
H28:   loop__1__i = endidx .
H29:   not (not false) .
H30:   tmp >= long_long_integer__first .
H31:   tmp <= long_long_integer__last .
H32:   not (tmp = 0) .
H33:   tmp >= long_long_integer__first .
H34:   tmp <= long_long_integer__last .
        ->
C1:    tmp >= unsigned_types__unsigned32__first .
C2:    tmp <= unsigned_types__unsigned32__last .
C3:    tmp >= unsigned_types__unsigned32__first .
C4:    tmp <= unsigned_types__unsigned32__last .
 

For path(s) from start to finish:

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


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


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


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

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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


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


