acats_c53007a = OK' : return_message' = {| num_of_cks := 14; division_cks := 0; overflow_cks := 14; range_cks := 0 |} : cks_infor_t = {| num_of_cks := 14; division_cks := 0; overflow_cks := 14; range_cks := 0 |} : cks_infor_t = {| num_of_cks := 16; division_cks := 0; overflow_cks := 16; range_cks := 0 |} : cks_infor_t acats_c55c02b = OK' : return_message' = {| num_of_cks := 2; division_cks := 0; overflow_cks := 2; range_cks := 0 |} : cks_infor_t = {| num_of_cks := 2; division_cks := 0; overflow_cks := 2; range_cks := 0 |} : cks_infor_t = {| num_of_cks := 7; division_cks := 0; overflow_cks := 2; range_cks := 5 |} : cks_infor_t array_record_package = OK' : return_message' = {| num_of_cks := 14; division_cks := 1; overflow_cks := 11; range_cks := 2 |} : cks_infor_t = {| num_of_cks := 14; division_cks := 1; overflow_cks := 11; range_cks := 2 |} : cks_infor_t = {| num_of_cks := 14; division_cks := 1; overflow_cks := 11; range_cks := 2 |} : cks_infor_t array_subtype_index = Mismatch' ({| astNumber := 19; sourceLoc := {| line := 10; col := 6; endline := 10; endcol := 6 |}; expectedOptimizedChecks := Do_Range_Check :: nil; gnatproChecks := nil; expectedCompleteChecks := nil; annotation := not_superset_of_opt_cks |} :: nil) : return_message' = {| num_of_cks := 2; division_cks := 0; overflow_cks := 1; range_cks := 1 |} : cks_infor_t = {| num_of_cks := 1; division_cks := 0; overflow_cks := 1; range_cks := 0 |} : cks_infor_t = {| num_of_cks := 2; division_cks := 0; overflow_cks := 1; range_cks := 1 |} : cks_infor_t arrayrecord = OK' : return_message' = {| num_of_cks := 10; division_cks := 1; overflow_cks := 9; range_cks := 0 |} : cks_infor_t = {| num_of_cks := 10; division_cks := 1; overflow_cks := 9; range_cks := 0 |} : cks_infor_t = {| num_of_cks := 12; division_cks := 1; overflow_cks := 9; range_cks := 2 |} : cks_infor_t assign_subtype_var = Mismatch' ({| astNumber := 15; sourceLoc := {| line := 8; col := 13; endline := 8; endcol := 13 |}; expectedOptimizedChecks := Do_Range_Check :: nil; gnatproChecks := nil; expectedCompleteChecks := nil; annotation := not_superset_of_opt_cks |} :: nil) : return_message' = {| num_of_cks := 2; division_cks := 0; overflow_cks := 1; range_cks := 1 |} : cks_infor_t = {| num_of_cks := 1; division_cks := 0; overflow_cks := 1; range_cks := 0 |} : cks_infor_t = {| num_of_cks := 2; division_cks := 0; overflow_cks := 1; range_cks := 1 |} : cks_infor_t binary_search = OK' : return_message' = {| num_of_cks := 4; division_cks := 0; overflow_cks := 0; range_cks := 4 |} : cks_infor_t = {| num_of_cks := 5; division_cks := 1; overflow_cks := 0; range_cks := 4 |} : cks_infor_t = {| num_of_cks := 19; division_cks := 1; overflow_cks := 6; range_cks := 12 |} : cks_infor_t bounded_in_out = Mismatch' ({| astNumber := 26; sourceLoc := {| line := 12; col := 16; endline := 12; endcol := 16 |}; expectedOptimizedChecks := Do_Range_Check :: Do_Range_Check_On_CopyOut :: nil; gnatproChecks := Do_Range_Check :: nil; expectedCompleteChecks := nil; annotation := not_superset_of_opt_cks |} :: nil) : return_message' = {| num_of_cks := 4; division_cks := 0; overflow_cks := 0; range_cks := 4 |} : cks_infor_t = {| num_of_cks := 3; division_cks := 0; overflow_cks := 0; range_cks := 3 |} : cks_infor_t = {| num_of_cks := 5; division_cks := 0; overflow_cks := 1; range_cks := 4 |} : cks_infor_t dependence_test_suite_01 = OK' : return_message' = {| num_of_cks := 2; division_cks := 0; overflow_cks := 2; range_cks := 0 |} : cks_infor_t = {| num_of_cks := 2; division_cks := 0; overflow_cks := 2; range_cks := 0 |} : cks_infor_t = {| num_of_cks := 2; division_cks := 0; overflow_cks := 2; range_cks := 0 |} : cks_infor_t dependence_test_suite_02 = OK' : return_message' = {| num_of_cks := 15; division_cks := 0; overflow_cks := 15; range_cks := 0 |} : cks_infor_t = {| num_of_cks := 15; division_cks := 0; overflow_cks := 15; range_cks := 0 |} : cks_infor_t = {| num_of_cks := 15; division_cks := 0; overflow_cks := 15; range_cks := 0 |} : cks_infor_t division_by_non_zero = OK' : return_message' = {| num_of_cks := 0; division_cks := 0; overflow_cks := 0; range_cks := 0 |} : cks_infor_t = {| num_of_cks := 1; division_cks := 1; overflow_cks := 0; range_cks := 0 |} : cks_infor_t = {| num_of_cks := 4; division_cks := 1; overflow_cks := 2; range_cks := 1 |} : cks_infor_t example = OK' : return_message' = {| num_of_cks := 3; division_cks := 0; overflow_cks := 3; range_cks := 0 |} : cks_infor_t = {| num_of_cks := 3; division_cks := 0; overflow_cks := 3; range_cks := 0 |} : cks_infor_t = {| num_of_cks := 3; division_cks := 0; overflow_cks := 3; range_cks := 0 |} : cks_infor_t factorial = OK' : return_message' = {| num_of_cks := 2; division_cks := 0; overflow_cks := 2; range_cks := 0 |} : cks_infor_t = {| num_of_cks := 2; division_cks := 0; overflow_cks := 2; range_cks := 0 |} : cks_infor_t = {| num_of_cks := 2; division_cks := 0; overflow_cks := 2; range_cks := 0 |} : cks_infor_t faultintegrator = OK' : return_message' = {| num_of_cks := 2; division_cks := 0; overflow_cks := 2; range_cks := 0 |} : cks_infor_t = {| num_of_cks := 2; division_cks := 0; overflow_cks := 2; range_cks := 0 |} : cks_infor_t = {| num_of_cks := 2; division_cks := 0; overflow_cks := 2; range_cks := 0 |} : cks_infor_t gcd = OK' : return_message' = {| num_of_cks := 4; division_cks := 1; overflow_cks := 3; range_cks := 0 |} : cks_infor_t = {| num_of_cks := 4; division_cks := 1; overflow_cks := 3; range_cks := 0 |} : cks_infor_t = {| num_of_cks := 4; division_cks := 1; overflow_cks := 3; range_cks := 0 |} : cks_infor_t gnatprove_test_bool = OK' : return_message' = {| num_of_cks := 0; division_cks := 0; overflow_cks := 0; range_cks := 0 |} : cks_infor_t = {| num_of_cks := 0; division_cks := 0; overflow_cks := 0; range_cks := 0 |} : cks_infor_t = {| num_of_cks := 0; division_cks := 0; overflow_cks := 0; range_cks := 0 |} : cks_infor_t linear_div = OK' : return_message' = {| num_of_cks := 3; division_cks := 0; overflow_cks := 3; range_cks := 0 |} : cks_infor_t = {| num_of_cks := 3; division_cks := 0; overflow_cks := 3; range_cks := 0 |} : cks_infor_t = {| num_of_cks := 3; division_cks := 0; overflow_cks := 3; range_cks := 0 |} : cks_infor_t max = OK' : return_message' = {| num_of_cks := 0; division_cks := 0; overflow_cks := 0; range_cks := 0 |} : cks_infor_t = {| num_of_cks := 0; division_cks := 0; overflow_cks := 0; range_cks := 0 |} : cks_infor_t = {| num_of_cks := 0; division_cks := 0; overflow_cks := 0; range_cks := 0 |} : cks_infor_t min = OK' : return_message' = {| num_of_cks := 0; division_cks := 0; overflow_cks := 0; range_cks := 0 |} : cks_infor_t = {| num_of_cks := 0; division_cks := 0; overflow_cks := 0; range_cks := 0 |} : cks_infor_t = {| num_of_cks := 0; division_cks := 0; overflow_cks := 0; range_cks := 0 |} : cks_infor_t modulus = OK' : return_message' = {| num_of_cks := 1; division_cks := 0; overflow_cks := 1; range_cks := 0 |} : cks_infor_t = {| num_of_cks := 2; division_cks := 1; overflow_cks := 1; range_cks := 0 |} : cks_infor_t = {| num_of_cks := 6; division_cks := 1; overflow_cks := 2; range_cks := 3 |} : cks_infor_t odd = OK' : return_message' = {| num_of_cks := 1; division_cks := 0; overflow_cks := 1; range_cks := 0 |} : cks_infor_t = {| num_of_cks := 2; division_cks := 1; overflow_cks := 1; range_cks := 0 |} : cks_infor_t = {| num_of_cks := 3; division_cks := 1; overflow_cks := 2; range_cks := 0 |} : cks_infor_t p_simple_call = OK' : return_message' = {| num_of_cks := 5; division_cks := 0; overflow_cks := 5; range_cks := 0 |} : cks_infor_t = {| num_of_cks := 5; division_cks := 0; overflow_cks := 5; range_cks := 0 |} : cks_infor_t = {| num_of_cks := 5; division_cks := 0; overflow_cks := 5; range_cks := 0 |} : cks_infor_t p_simple_call_two = OK' : return_message' = {| num_of_cks := 4; division_cks := 0; overflow_cks := 4; range_cks := 0 |} : cks_infor_t = {| num_of_cks := 4; division_cks := 0; overflow_cks := 4; range_cks := 0 |} : cks_infor_t = {| num_of_cks := 4; division_cks := 0; overflow_cks := 4; range_cks := 0 |} : cks_infor_t packagedemo_a = OK' : return_message' = {| num_of_cks := 1; division_cks := 0; overflow_cks := 1; range_cks := 0 |} : cks_infor_t = {| num_of_cks := 1; division_cks := 0; overflow_cks := 1; range_cks := 0 |} : cks_infor_t = {| num_of_cks := 1; division_cks := 0; overflow_cks := 1; range_cks := 0 |} : cks_infor_t prime = OK' : return_message' = {| num_of_cks := 3; division_cks := 1; overflow_cks := 2; range_cks := 0 |} : cks_infor_t = {| num_of_cks := 3; division_cks := 1; overflow_cks := 2; range_cks := 0 |} : cks_infor_t = {| num_of_cks := 3; division_cks := 1; overflow_cks := 2; range_cks := 0 |} : cks_infor_t proceduretest01 = OK' : return_message' = {| num_of_cks := 3; division_cks := 0; overflow_cks := 3; range_cks := 0 |} : cks_infor_t = {| num_of_cks := 3; division_cks := 0; overflow_cks := 3; range_cks := 0 |} : cks_infor_t = {| num_of_cks := 3; division_cks := 0; overflow_cks := 3; range_cks := 0 |} : cks_infor_t quantifiertest = OK' : return_message' = {| num_of_cks := 1; division_cks := 0; overflow_cks := 1; range_cks := 0 |} : cks_infor_t = {| num_of_cks := 1; division_cks := 0; overflow_cks := 1; range_cks := 0 |} : cks_infor_t = {| num_of_cks := 3; division_cks := 0; overflow_cks := 1; range_cks := 2 |} : cks_infor_t recordtest01 = OK' : return_message' = {| num_of_cks := 0; division_cks := 0; overflow_cks := 0; range_cks := 0 |} : cks_infor_t = {| num_of_cks := 0; division_cks := 0; overflow_cks := 0; range_cks := 0 |} : cks_infor_t = {| num_of_cks := 0; division_cks := 0; overflow_cks := 0; range_cks := 0 |} : cks_infor_t recursive_proc_pkg = OK' : return_message' = {| num_of_cks := 3; division_cks := 0; overflow_cks := 3; range_cks := 0 |} : cks_infor_t = {| num_of_cks := 3; division_cks := 0; overflow_cks := 3; range_cks := 0 |} : cks_infor_t = {| num_of_cks := 3; division_cks := 0; overflow_cks := 3; range_cks := 0 |} : cks_infor_t sort = OK' : return_message' = {| num_of_cks := 11; division_cks := 0; overflow_cks := 5; range_cks := 6 |} : cks_infor_t = {| num_of_cks := 11; division_cks := 0; overflow_cks := 5; range_cks := 6 |} : cks_infor_t = {| num_of_cks := 11; division_cks := 0; overflow_cks := 5; range_cks := 6 |} : cks_infor_t test_case_10 = OK' : return_message' = {| num_of_cks := 1; division_cks := 0; overflow_cks := 1; range_cks := 0 |} : cks_infor_t = {| num_of_cks := 1; division_cks := 0; overflow_cks := 1; range_cks := 0 |} : cks_infor_t = {| num_of_cks := 1; division_cks := 0; overflow_cks := 1; range_cks := 0 |} : cks_infor_t the_stack = OK' : return_message' = {| num_of_cks := 6; division_cks := 0; overflow_cks := 0; range_cks := 6 |} : cks_infor_t = {| num_of_cks := 6; division_cks := 0; overflow_cks := 0; range_cks := 6 |} : cks_infor_t = {| num_of_cks := 10; division_cks := 0; overflow_cks := 4; range_cks := 6 |} : cks_infor_t the_stack_praxis = OK' : return_message' = {| num_of_cks := 4; division_cks := 0; overflow_cks := 0; range_cks := 4 |} : cks_infor_t = {| num_of_cks := 4; division_cks := 0; overflow_cks := 0; range_cks := 4 |} : cks_infor_t = {| num_of_cks := 6; division_cks := 0; overflow_cks := 2; range_cks := 4 |} : cks_infor_t two_way_sort = OK' : return_message' = {| num_of_cks := 4; division_cks := 0; overflow_cks := 0; range_cks := 4 |} : cks_infor_t = {| num_of_cks := 4; division_cks := 0; overflow_cks := 0; range_cks := 4 |} : cks_infor_t = {| num_of_cks := 21; division_cks := 0; overflow_cks := 4; range_cks := 17 |} : cks_infor_t tetris = OK' : return_message' = {| num_of_cks := 25; division_cks := 0; overflow_cks := 0; range_cks := 25 |} : cks_infor_t = {| num_of_cks := 25; division_cks := 0; overflow_cks := 0; range_cks := 25 |} : cks_infor_t = {| num_of_cks := 87; division_cks := 0; overflow_cks := 29; range_cks := 58 |} : cks_infor_t skein = OK' : return_message' = {| num_of_cks := 77; division_cks := 0; overflow_cks := 52; range_cks := 25 |} : cks_infor_t = {| num_of_cks := 94; division_cks := 7; overflow_cks := 58; range_cks := 29 |} : cks_infor_t = {| num_of_cks := 347; division_cks := 7; overflow_cks := 94; range_cks := 246 |} : cks_infor_t