LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
0 73 0: z_389_post + z_389_post ≤ 0z_389_postz_389_post ≤ 0z_389_0 + z_389_0 ≤ 0z_389_0z_389_0 ≤ 0z_28_post + z_28_post ≤ 0z_28_postz_28_post ≤ 0z_28_1 + z_28_1 ≤ 0z_28_1z_28_1 ≤ 0z_28_0 + z_28_0 ≤ 0z_28_0z_28_0 ≤ 0z_279_post + z_279_post ≤ 0z_279_postz_279_post ≤ 0z_279_0 + z_279_0 ≤ 0z_279_0z_279_0 ≤ 0z_265_post + z_265_post ≤ 0z_265_postz_265_post ≤ 0z_265_0 + z_265_0 ≤ 0z_265_0z_265_0 ≤ 0z_252_post + z_252_post ≤ 0z_252_postz_252_post ≤ 0z_252_0 + z_252_0 ≤ 0z_252_0z_252_0 ≤ 0z_238_post + z_238_post ≤ 0z_238_postz_238_post ≤ 0z_238_0 + z_238_0 ≤ 0z_238_0z_238_0 ≤ 0z_229_post + z_229_post ≤ 0z_229_postz_229_post ≤ 0z_229_0 + z_229_0 ≤ 0z_229_0z_229_0 ≤ 0z_188_post + z_188_post ≤ 0z_188_postz_188_post ≤ 0z_188_0 + z_188_0 ≤ 0z_188_0z_188_0 ≤ 0z_160_post + z_160_post ≤ 0z_160_postz_160_post ≤ 0z_160_0 + z_160_0 ≤ 0z_160_0z_160_0 ≤ 0y_22_post + y_22_post ≤ 0y_22_posty_22_post ≤ 0y_22_2 + y_22_2 ≤ 0y_22_2y_22_2 ≤ 0y_22_1 + y_22_1 ≤ 0y_22_1y_22_1 ≤ 0y_22_0 + y_22_0 ≤ 0y_22_0y_22_0 ≤ 0x_SLAM_f_21_post + x_SLAM_f_21_post ≤ 0x_SLAM_f_21_postx_SLAM_f_21_post ≤ 0x_SLAM_f_21_2 + x_SLAM_f_21_2 ≤ 0x_SLAM_f_21_2x_SLAM_f_21_2 ≤ 0x_SLAM_f_21_1 + x_SLAM_f_21_1 ≤ 0x_SLAM_f_21_1x_SLAM_f_21_1 ≤ 0x_SLAM_f_21_0 + x_SLAM_f_21_0 ≤ 0x_SLAM_f_21_0x_SLAM_f_21_0 ≤ 0x_23_post + x_23_post ≤ 0x_23_postx_23_post ≤ 0x_23_2 + x_23_2 ≤ 0x_23_2x_23_2 ≤ 0x_23_1 + x_23_1 ≤ 0x_23_1x_23_1 ≤ 0x_23_0 + x_23_0 ≤ 0x_23_0x_23_0 ≤ 0x_19_post + x_19_post ≤ 0x_19_postx_19_post ≤ 0x_19_1 + x_19_1 ≤ 0x_19_1x_19_1 ≤ 0x_19_0 + x_19_0 ≤ 0x_19_0x_19_0 ≤ 0tmp_37_post + tmp_37_post ≤ 0tmp_37_posttmp_37_post ≤ 0tmp_37_0 + tmp_37_0 ≤ 0tmp_37_0tmp_37_0 ≤ 0temp_38_post + temp_38_post ≤ 0temp_38_posttemp_38_post ≤ 0temp_38_0 + temp_38_0 ≤ 0temp_38_0temp_38_0 ≤ 0temp1_30_post + temp1_30_post ≤ 0temp1_30_posttemp1_30_post ≤ 0temp1_30_0 + temp1_30_0 ≤ 0temp1_30_0temp1_30_0 ≤ 0temp0_34_post + temp0_34_post ≤ 0temp0_34_posttemp0_34_post ≤ 0temp0_34_1 + temp0_34_1 ≤ 0temp0_34_1temp0_34_1 ≤ 0temp0_34_0 + temp0_34_0 ≤ 0temp0_34_0temp0_34_0 ≤ 0temp0_18_0 + temp0_18_0 ≤ 0temp0_18_0temp0_18_0 ≤ 0t_24_post + t_24_post ≤ 0t_24_postt_24_post ≤ 0t_24_1 + t_24_1 ≤ 0t_24_1t_24_1 ≤ 0t_24_0 + t_24_0 ≤ 0t_24_0t_24_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_post + result_dot_nondet_sdv_special_RETURN_VALUE_14_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_postresult_dot_nondet_sdv_special_RETURN_VALUE_14_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_2 + result_dot_nondet_sdv_special_RETURN_VALUE_14_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_2result_dot_nondet_sdv_special_RETURN_VALUE_14_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_1result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_0 + result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_0result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_postresult_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_0 ≤ 0result_11_post + result_11_post ≤ 0result_11_postresult_11_post ≤ 0result_11_2 + result_11_2 ≤ 0result_11_2result_11_2 ≤ 0result_11_1 + result_11_1 ≤ 0result_11_1result_11_1 ≤ 0result_11_0 + result_11_0 ≤ 0result_11_0result_11_0 ≤ 0rcd_70_post + rcd_70_post ≤ 0rcd_70_postrcd_70_post ≤ 0rcd_70_0 + rcd_70_0 ≤ 0rcd_70_0rcd_70_0 ≤ 0rcd_46_post + rcd_46_post ≤ 0rcd_46_postrcd_46_post ≤ 0rcd_46_0 + rcd_46_0 ≤ 0rcd_46_0rcd_46_0 ≤ 0rcd_396_post + rcd_396_post ≤ 0rcd_396_postrcd_396_post ≤ 0rcd_396_0 + rcd_396_0 ≤ 0rcd_396_0rcd_396_0 ≤ 0rcd_376_post + rcd_376_post ≤ 0rcd_376_postrcd_376_post ≤ 0rcd_376_0 + rcd_376_0 ≤ 0rcd_376_0rcd_376_0 ≤ 0rcd_356_post + rcd_356_post ≤ 0rcd_356_postrcd_356_post ≤ 0rcd_356_0 + rcd_356_0 ≤ 0rcd_356_0rcd_356_0 ≤ 0rcd_352_post + rcd_352_post ≤ 0rcd_352_postrcd_352_post ≤ 0rcd_352_0 + rcd_352_0 ≤ 0rcd_352_0rcd_352_0 ≤ 0rcd_264_post + rcd_264_post ≤ 0rcd_264_postrcd_264_post ≤ 0rcd_264_0 + rcd_264_0 ≤ 0rcd_264_0rcd_264_0 ≤ 0rcd_237_post + rcd_237_post ≤ 0rcd_237_postrcd_237_post ≤ 0rcd_237_0 + rcd_237_0 ≤ 0rcd_237_0rcd_237_0 ≤ 0rcd_228_post + rcd_228_post ≤ 0rcd_228_postrcd_228_post ≤ 0rcd_228_0 + rcd_228_0 ≤ 0rcd_228_0rcd_228_0 ≤ 0rcd_226_post + rcd_226_post ≤ 0rcd_226_postrcd_226_post ≤ 0rcd_226_0 + rcd_226_0 ≤ 0rcd_226_0rcd_226_0 ≤ 0rcd_222_post + rcd_222_post ≤ 0rcd_222_postrcd_222_post ≤ 0rcd_222_0 + rcd_222_0 ≤ 0rcd_222_0rcd_222_0 ≤ 0rcd_113_post + rcd_113_post ≤ 0rcd_113_postrcd_113_post ≤ 0rcd_113_0 + rcd_113_0 ≤ 0rcd_113_0rcd_113_0 ≤ 0rcd_105_post + rcd_105_post ≤ 0rcd_105_postrcd_105_post ≤ 0rcd_105_0 + rcd_105_0 ≤ 0rcd_105_0rcd_105_0 ≤ 0r_42_post + r_42_post ≤ 0r_42_postr_42_post ≤ 0r_42_0 + r_42_0 ≤ 0r_42_0r_42_0 ≤ 0r_236_post + r_236_post ≤ 0r_236_postr_236_post ≤ 0r_236_0 + r_236_0 ≤ 0r_236_0r_236_0 ≤ 0r_178_post + r_178_post ≤ 0r_178_postr_178_post ≤ 0r_178_0 + r_178_0 ≤ 0r_178_0r_178_0 ≤ 0nondet_12_post + nondet_12_post ≤ 0nondet_12_postnondet_12_post ≤ 0nondet_12_1 + nondet_12_1 ≤ 0nondet_12_1nondet_12_1 ≤ 0nondet_12_0 + nondet_12_0 ≤ 0nondet_12_0nondet_12_0 ≤ 0lt_483_post + lt_483_post ≤ 0lt_483_postlt_483_post ≤ 0lt_483_0 + lt_483_0 ≤ 0lt_483_0lt_483_0 ≤ 0lt_386_post + lt_386_post ≤ 0lt_386_postlt_386_post ≤ 0lt_386_0 + lt_386_0 ≤ 0lt_386_0lt_386_0 ≤ 0lt_29_post + lt_29_post ≤ 0lt_29_postlt_29_post ≤ 0lt_29_1 + lt_29_1 ≤ 0lt_29_1lt_29_1 ≤ 0lt_29_0 + lt_29_0 ≤ 0lt_29_0lt_29_0 ≤ 0lt_17_post + lt_17_post ≤ 0lt_17_postlt_17_post ≤ 0lt_17_0 + lt_17_0 ≤ 0lt_17_0lt_17_0 ≤ 0length_32_post + length_32_post ≤ 0length_32_postlength_32_post ≤ 0length_32_0 + length_32_0 ≤ 0length_32_0length_32_0 ≤ 0len_286_post + len_286_post ≤ 0len_286_postlen_286_post ≤ 0len_286_0 + len_286_0 ≤ 0len_286_0len_286_0 ≤ 0len_266_post + len_266_post ≤ 0len_266_postlen_266_post ≤ 0len_266_0 + len_266_0 ≤ 0len_266_0len_266_0 ≤ 0len_195_post + len_195_post ≤ 0len_195_postlen_195_post ≤ 0len_195_0 + len_195_0 ≤ 0len_195_0len_195_0 ≤ 0i_33_post + i_33_post ≤ 0i_33_posti_33_post ≤ 0i_33_0 + i_33_0 ≤ 0i_33_0i_33_0 ≤ 0i_227_post + i_227_post ≤ 0i_227_posti_227_post ≤ 0i_227_0 + i_227_0 ≤ 0i_227_0i_227_0 ≤ 0i_120_post + i_120_post ≤ 0i_120_posti_120_post ≤ 0i_120_0 + i_120_0 ≤ 0i_120_0i_120_0 ≤ 0i_111_post + i_111_post ≤ 0i_111_posti_111_post ≤ 0i_111_0 + i_111_0 ≤ 0i_111_0i_111_0 ≤ 0head_35_post + head_35_post ≤ 0head_35_posthead_35_post ≤ 0head_35_0 + head_35_0 ≤ 0head_35_0head_35_0 ≤ 0head_13_post + head_13_post ≤ 0head_13_posthead_13_post ≤ 0head_13_0 + head_13_0 ≤ 0head_13_0head_13_0 ≤ 0ct_20_post + ct_20_post ≤ 0ct_20_postct_20_post ≤ 0ct_20_2 + ct_20_2 ≤ 0ct_20_2ct_20_2 ≤ 0ct_20_1 + ct_20_1 ≤ 0ct_20_1ct_20_1 ≤ 0ct_20_0 + ct_20_0 ≤ 0ct_20_0ct_20_0 ≤ 0a_377_post + a_377_post ≤ 0a_377_posta_377_post ≤ 0a_377_0 + a_377_0 ≤ 0a_377_0a_377_0 ≤ 0a_347_post + a_347_post ≤ 0a_347_posta_347_post ≤ 0a_347_0 + a_347_0 ≤ 0a_347_0a_347_0 ≤ 0a_321_post + a_321_post ≤ 0a_321_posta_321_post ≤ 0a_321_0 + a_321_0 ≤ 0a_321_0a_321_0 ≤ 0a_27_post + a_27_post ≤ 0a_27_posta_27_post ≤ 0a_27_1 + a_27_1 ≤ 0a_27_1a_27_1 ≤ 0a_27_0 + a_27_0 ≤ 0a_27_0a_27_0 ≤ 0a_267_post + a_267_post ≤ 0a_267_posta_267_post ≤ 0a_267_0 + a_267_0 ≤ 0a_267_0a_267_0 ≤ 0a_210_post + a_210_post ≤ 0a_210_posta_210_post ≤ 0a_210_0 + a_210_0 ≤ 0a_210_0a_210_0 ≤ 0a_166_post + a_166_post ≤ 0a_166_posta_166_post ≤ 0a_166_0 + a_166_0 ≤ 0a_166_0a_166_0 ≤ 0
38 80 38: z_389_post + z_389_post ≤ 0z_389_postz_389_post ≤ 0z_389_0 + z_389_0 ≤ 0z_389_0z_389_0 ≤ 0z_28_post + z_28_post ≤ 0z_28_postz_28_post ≤ 0z_28_1 + z_28_1 ≤ 0z_28_1z_28_1 ≤ 0z_28_0 + z_28_0 ≤ 0z_28_0z_28_0 ≤ 0z_279_post + z_279_post ≤ 0z_279_postz_279_post ≤ 0z_279_0 + z_279_0 ≤ 0z_279_0z_279_0 ≤ 0z_265_post + z_265_post ≤ 0z_265_postz_265_post ≤ 0z_265_0 + z_265_0 ≤ 0z_265_0z_265_0 ≤ 0z_252_post + z_252_post ≤ 0z_252_postz_252_post ≤ 0z_252_0 + z_252_0 ≤ 0z_252_0z_252_0 ≤ 0z_238_post + z_238_post ≤ 0z_238_postz_238_post ≤ 0z_238_0 + z_238_0 ≤ 0z_238_0z_238_0 ≤ 0z_229_post + z_229_post ≤ 0z_229_postz_229_post ≤ 0z_229_0 + z_229_0 ≤ 0z_229_0z_229_0 ≤ 0z_188_post + z_188_post ≤ 0z_188_postz_188_post ≤ 0z_188_0 + z_188_0 ≤ 0z_188_0z_188_0 ≤ 0z_160_post + z_160_post ≤ 0z_160_postz_160_post ≤ 0z_160_0 + z_160_0 ≤ 0z_160_0z_160_0 ≤ 0y_22_post + y_22_post ≤ 0y_22_posty_22_post ≤ 0y_22_2 + y_22_2 ≤ 0y_22_2y_22_2 ≤ 0y_22_1 + y_22_1 ≤ 0y_22_1y_22_1 ≤ 0y_22_0 + y_22_0 ≤ 0y_22_0y_22_0 ≤ 0x_SLAM_f_21_post + x_SLAM_f_21_post ≤ 0x_SLAM_f_21_postx_SLAM_f_21_post ≤ 0x_SLAM_f_21_2 + x_SLAM_f_21_2 ≤ 0x_SLAM_f_21_2x_SLAM_f_21_2 ≤ 0x_SLAM_f_21_1 + x_SLAM_f_21_1 ≤ 0x_SLAM_f_21_1x_SLAM_f_21_1 ≤ 0x_SLAM_f_21_0 + x_SLAM_f_21_0 ≤ 0x_SLAM_f_21_0x_SLAM_f_21_0 ≤ 0x_23_post + x_23_post ≤ 0x_23_postx_23_post ≤ 0x_23_2 + x_23_2 ≤ 0x_23_2x_23_2 ≤ 0x_23_1 + x_23_1 ≤ 0x_23_1x_23_1 ≤ 0x_23_0 + x_23_0 ≤ 0x_23_0x_23_0 ≤ 0x_19_post + x_19_post ≤ 0x_19_postx_19_post ≤ 0x_19_1 + x_19_1 ≤ 0x_19_1x_19_1 ≤ 0x_19_0 + x_19_0 ≤ 0x_19_0x_19_0 ≤ 0tmp_37_post + tmp_37_post ≤ 0tmp_37_posttmp_37_post ≤ 0tmp_37_0 + tmp_37_0 ≤ 0tmp_37_0tmp_37_0 ≤ 0temp_38_post + temp_38_post ≤ 0temp_38_posttemp_38_post ≤ 0temp_38_0 + temp_38_0 ≤ 0temp_38_0temp_38_0 ≤ 0temp1_30_post + temp1_30_post ≤ 0temp1_30_posttemp1_30_post ≤ 0temp1_30_0 + temp1_30_0 ≤ 0temp1_30_0temp1_30_0 ≤ 0temp0_34_post + temp0_34_post ≤ 0temp0_34_posttemp0_34_post ≤ 0temp0_34_1 + temp0_34_1 ≤ 0temp0_34_1temp0_34_1 ≤ 0temp0_34_0 + temp0_34_0 ≤ 0temp0_34_0temp0_34_0 ≤ 0temp0_18_0 + temp0_18_0 ≤ 0temp0_18_0temp0_18_0 ≤ 0t_24_post + t_24_post ≤ 0t_24_postt_24_post ≤ 0t_24_1 + t_24_1 ≤ 0t_24_1t_24_1 ≤ 0t_24_0 + t_24_0 ≤ 0t_24_0t_24_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_post + result_dot_nondet_sdv_special_RETURN_VALUE_14_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_postresult_dot_nondet_sdv_special_RETURN_VALUE_14_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_2 + result_dot_nondet_sdv_special_RETURN_VALUE_14_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_2result_dot_nondet_sdv_special_RETURN_VALUE_14_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_1result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_0 + result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_0result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_postresult_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_0 ≤ 0result_11_post + result_11_post ≤ 0result_11_postresult_11_post ≤ 0result_11_2 + result_11_2 ≤ 0result_11_2result_11_2 ≤ 0result_11_1 + result_11_1 ≤ 0result_11_1result_11_1 ≤ 0result_11_0 + result_11_0 ≤ 0result_11_0result_11_0 ≤ 0rcd_70_post + rcd_70_post ≤ 0rcd_70_postrcd_70_post ≤ 0rcd_70_0 + rcd_70_0 ≤ 0rcd_70_0rcd_70_0 ≤ 0rcd_46_post + rcd_46_post ≤ 0rcd_46_postrcd_46_post ≤ 0rcd_46_0 + rcd_46_0 ≤ 0rcd_46_0rcd_46_0 ≤ 0rcd_396_post + rcd_396_post ≤ 0rcd_396_postrcd_396_post ≤ 0rcd_396_0 + rcd_396_0 ≤ 0rcd_396_0rcd_396_0 ≤ 0rcd_376_post + rcd_376_post ≤ 0rcd_376_postrcd_376_post ≤ 0rcd_376_0 + rcd_376_0 ≤ 0rcd_376_0rcd_376_0 ≤ 0rcd_356_post + rcd_356_post ≤ 0rcd_356_postrcd_356_post ≤ 0rcd_356_0 + rcd_356_0 ≤ 0rcd_356_0rcd_356_0 ≤ 0rcd_352_post + rcd_352_post ≤ 0rcd_352_postrcd_352_post ≤ 0rcd_352_0 + rcd_352_0 ≤ 0rcd_352_0rcd_352_0 ≤ 0rcd_264_post + rcd_264_post ≤ 0rcd_264_postrcd_264_post ≤ 0rcd_264_0 + rcd_264_0 ≤ 0rcd_264_0rcd_264_0 ≤ 0rcd_237_post + rcd_237_post ≤ 0rcd_237_postrcd_237_post ≤ 0rcd_237_0 + rcd_237_0 ≤ 0rcd_237_0rcd_237_0 ≤ 0rcd_228_post + rcd_228_post ≤ 0rcd_228_postrcd_228_post ≤ 0rcd_228_0 + rcd_228_0 ≤ 0rcd_228_0rcd_228_0 ≤ 0rcd_226_post + rcd_226_post ≤ 0rcd_226_postrcd_226_post ≤ 0rcd_226_0 + rcd_226_0 ≤ 0rcd_226_0rcd_226_0 ≤ 0rcd_222_post + rcd_222_post ≤ 0rcd_222_postrcd_222_post ≤ 0rcd_222_0 + rcd_222_0 ≤ 0rcd_222_0rcd_222_0 ≤ 0rcd_113_post + rcd_113_post ≤ 0rcd_113_postrcd_113_post ≤ 0rcd_113_0 + rcd_113_0 ≤ 0rcd_113_0rcd_113_0 ≤ 0rcd_105_post + rcd_105_post ≤ 0rcd_105_postrcd_105_post ≤ 0rcd_105_0 + rcd_105_0 ≤ 0rcd_105_0rcd_105_0 ≤ 0r_42_post + r_42_post ≤ 0r_42_postr_42_post ≤ 0r_42_0 + r_42_0 ≤ 0r_42_0r_42_0 ≤ 0r_236_post + r_236_post ≤ 0r_236_postr_236_post ≤ 0r_236_0 + r_236_0 ≤ 0r_236_0r_236_0 ≤ 0r_178_post + r_178_post ≤ 0r_178_postr_178_post ≤ 0r_178_0 + r_178_0 ≤ 0r_178_0r_178_0 ≤ 0nondet_12_post + nondet_12_post ≤ 0nondet_12_postnondet_12_post ≤ 0nondet_12_1 + nondet_12_1 ≤ 0nondet_12_1nondet_12_1 ≤ 0nondet_12_0 + nondet_12_0 ≤ 0nondet_12_0nondet_12_0 ≤ 0lt_483_post + lt_483_post ≤ 0lt_483_postlt_483_post ≤ 0lt_483_0 + lt_483_0 ≤ 0lt_483_0lt_483_0 ≤ 0lt_386_post + lt_386_post ≤ 0lt_386_postlt_386_post ≤ 0lt_386_0 + lt_386_0 ≤ 0lt_386_0lt_386_0 ≤ 0lt_29_post + lt_29_post ≤ 0lt_29_postlt_29_post ≤ 0lt_29_1 + lt_29_1 ≤ 0lt_29_1lt_29_1 ≤ 0lt_29_0 + lt_29_0 ≤ 0lt_29_0lt_29_0 ≤ 0lt_17_post + lt_17_post ≤ 0lt_17_postlt_17_post ≤ 0lt_17_0 + lt_17_0 ≤ 0lt_17_0lt_17_0 ≤ 0length_32_post + length_32_post ≤ 0length_32_postlength_32_post ≤ 0length_32_0 + length_32_0 ≤ 0length_32_0length_32_0 ≤ 0len_286_post + len_286_post ≤ 0len_286_postlen_286_post ≤ 0len_286_0 + len_286_0 ≤ 0len_286_0len_286_0 ≤ 0len_266_post + len_266_post ≤ 0len_266_postlen_266_post ≤ 0len_266_0 + len_266_0 ≤ 0len_266_0len_266_0 ≤ 0len_195_post + len_195_post ≤ 0len_195_postlen_195_post ≤ 0len_195_0 + len_195_0 ≤ 0len_195_0len_195_0 ≤ 0i_33_post + i_33_post ≤ 0i_33_posti_33_post ≤ 0i_33_0 + i_33_0 ≤ 0i_33_0i_33_0 ≤ 0i_227_post + i_227_post ≤ 0i_227_posti_227_post ≤ 0i_227_0 + i_227_0 ≤ 0i_227_0i_227_0 ≤ 0i_120_post + i_120_post ≤ 0i_120_posti_120_post ≤ 0i_120_0 + i_120_0 ≤ 0i_120_0i_120_0 ≤ 0i_111_post + i_111_post ≤ 0i_111_posti_111_post ≤ 0i_111_0 + i_111_0 ≤ 0i_111_0i_111_0 ≤ 0head_35_post + head_35_post ≤ 0head_35_posthead_35_post ≤ 0head_35_0 + head_35_0 ≤ 0head_35_0head_35_0 ≤ 0head_13_post + head_13_post ≤ 0head_13_posthead_13_post ≤ 0head_13_0 + head_13_0 ≤ 0head_13_0head_13_0 ≤ 0ct_20_post + ct_20_post ≤ 0ct_20_postct_20_post ≤ 0ct_20_2 + ct_20_2 ≤ 0ct_20_2ct_20_2 ≤ 0ct_20_1 + ct_20_1 ≤ 0ct_20_1ct_20_1 ≤ 0ct_20_0 + ct_20_0 ≤ 0ct_20_0ct_20_0 ≤ 0a_377_post + a_377_post ≤ 0a_377_posta_377_post ≤ 0a_377_0 + a_377_0 ≤ 0a_377_0a_377_0 ≤ 0a_347_post + a_347_post ≤ 0a_347_posta_347_post ≤ 0a_347_0 + a_347_0 ≤ 0a_347_0a_347_0 ≤ 0a_321_post + a_321_post ≤ 0a_321_posta_321_post ≤ 0a_321_0 + a_321_0 ≤ 0a_321_0a_321_0 ≤ 0a_27_post + a_27_post ≤ 0a_27_posta_27_post ≤ 0a_27_1 + a_27_1 ≤ 0a_27_1a_27_1 ≤ 0a_27_0 + a_27_0 ≤ 0a_27_0a_27_0 ≤ 0a_267_post + a_267_post ≤ 0a_267_posta_267_post ≤ 0a_267_0 + a_267_0 ≤ 0a_267_0a_267_0 ≤ 0a_210_post + a_210_post ≤ 0a_210_posta_210_post ≤ 0a_210_0 + a_210_0 ≤ 0a_210_0a_210_0 ≤ 0a_166_post + a_166_post ≤ 0a_166_posta_166_post ≤ 0a_166_0 + a_166_0 ≤ 0a_166_0a_166_0 ≤ 0
43 87 43: z_389_post + z_389_post ≤ 0z_389_postz_389_post ≤ 0z_389_0 + z_389_0 ≤ 0z_389_0z_389_0 ≤ 0z_28_post + z_28_post ≤ 0z_28_postz_28_post ≤ 0z_28_1 + z_28_1 ≤ 0z_28_1z_28_1 ≤ 0z_28_0 + z_28_0 ≤ 0z_28_0z_28_0 ≤ 0z_279_post + z_279_post ≤ 0z_279_postz_279_post ≤ 0z_279_0 + z_279_0 ≤ 0z_279_0z_279_0 ≤ 0z_265_post + z_265_post ≤ 0z_265_postz_265_post ≤ 0z_265_0 + z_265_0 ≤ 0z_265_0z_265_0 ≤ 0z_252_post + z_252_post ≤ 0z_252_postz_252_post ≤ 0z_252_0 + z_252_0 ≤ 0z_252_0z_252_0 ≤ 0z_238_post + z_238_post ≤ 0z_238_postz_238_post ≤ 0z_238_0 + z_238_0 ≤ 0z_238_0z_238_0 ≤ 0z_229_post + z_229_post ≤ 0z_229_postz_229_post ≤ 0z_229_0 + z_229_0 ≤ 0z_229_0z_229_0 ≤ 0z_188_post + z_188_post ≤ 0z_188_postz_188_post ≤ 0z_188_0 + z_188_0 ≤ 0z_188_0z_188_0 ≤ 0z_160_post + z_160_post ≤ 0z_160_postz_160_post ≤ 0z_160_0 + z_160_0 ≤ 0z_160_0z_160_0 ≤ 0y_22_post + y_22_post ≤ 0y_22_posty_22_post ≤ 0y_22_2 + y_22_2 ≤ 0y_22_2y_22_2 ≤ 0y_22_1 + y_22_1 ≤ 0y_22_1y_22_1 ≤ 0y_22_0 + y_22_0 ≤ 0y_22_0y_22_0 ≤ 0x_SLAM_f_21_post + x_SLAM_f_21_post ≤ 0x_SLAM_f_21_postx_SLAM_f_21_post ≤ 0x_SLAM_f_21_2 + x_SLAM_f_21_2 ≤ 0x_SLAM_f_21_2x_SLAM_f_21_2 ≤ 0x_SLAM_f_21_1 + x_SLAM_f_21_1 ≤ 0x_SLAM_f_21_1x_SLAM_f_21_1 ≤ 0x_SLAM_f_21_0 + x_SLAM_f_21_0 ≤ 0x_SLAM_f_21_0x_SLAM_f_21_0 ≤ 0x_23_post + x_23_post ≤ 0x_23_postx_23_post ≤ 0x_23_2 + x_23_2 ≤ 0x_23_2x_23_2 ≤ 0x_23_1 + x_23_1 ≤ 0x_23_1x_23_1 ≤ 0x_23_0 + x_23_0 ≤ 0x_23_0x_23_0 ≤ 0x_19_post + x_19_post ≤ 0x_19_postx_19_post ≤ 0x_19_1 + x_19_1 ≤ 0x_19_1x_19_1 ≤ 0x_19_0 + x_19_0 ≤ 0x_19_0x_19_0 ≤ 0tmp_37_post + tmp_37_post ≤ 0tmp_37_posttmp_37_post ≤ 0tmp_37_0 + tmp_37_0 ≤ 0tmp_37_0tmp_37_0 ≤ 0temp_38_post + temp_38_post ≤ 0temp_38_posttemp_38_post ≤ 0temp_38_0 + temp_38_0 ≤ 0temp_38_0temp_38_0 ≤ 0temp1_30_post + temp1_30_post ≤ 0temp1_30_posttemp1_30_post ≤ 0temp1_30_0 + temp1_30_0 ≤ 0temp1_30_0temp1_30_0 ≤ 0temp0_34_post + temp0_34_post ≤ 0temp0_34_posttemp0_34_post ≤ 0temp0_34_1 + temp0_34_1 ≤ 0temp0_34_1temp0_34_1 ≤ 0temp0_34_0 + temp0_34_0 ≤ 0temp0_34_0temp0_34_0 ≤ 0temp0_18_0 + temp0_18_0 ≤ 0temp0_18_0temp0_18_0 ≤ 0t_24_post + t_24_post ≤ 0t_24_postt_24_post ≤ 0t_24_1 + t_24_1 ≤ 0t_24_1t_24_1 ≤ 0t_24_0 + t_24_0 ≤ 0t_24_0t_24_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_post + result_dot_nondet_sdv_special_RETURN_VALUE_14_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_postresult_dot_nondet_sdv_special_RETURN_VALUE_14_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_2 + result_dot_nondet_sdv_special_RETURN_VALUE_14_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_2result_dot_nondet_sdv_special_RETURN_VALUE_14_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_1result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_0 + result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_0result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_postresult_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_0 ≤ 0result_11_post + result_11_post ≤ 0result_11_postresult_11_post ≤ 0result_11_2 + result_11_2 ≤ 0result_11_2result_11_2 ≤ 0result_11_1 + result_11_1 ≤ 0result_11_1result_11_1 ≤ 0result_11_0 + result_11_0 ≤ 0result_11_0result_11_0 ≤ 0rcd_70_post + rcd_70_post ≤ 0rcd_70_postrcd_70_post ≤ 0rcd_70_0 + rcd_70_0 ≤ 0rcd_70_0rcd_70_0 ≤ 0rcd_46_post + rcd_46_post ≤ 0rcd_46_postrcd_46_post ≤ 0rcd_46_0 + rcd_46_0 ≤ 0rcd_46_0rcd_46_0 ≤ 0rcd_396_post + rcd_396_post ≤ 0rcd_396_postrcd_396_post ≤ 0rcd_396_0 + rcd_396_0 ≤ 0rcd_396_0rcd_396_0 ≤ 0rcd_376_post + rcd_376_post ≤ 0rcd_376_postrcd_376_post ≤ 0rcd_376_0 + rcd_376_0 ≤ 0rcd_376_0rcd_376_0 ≤ 0rcd_356_post + rcd_356_post ≤ 0rcd_356_postrcd_356_post ≤ 0rcd_356_0 + rcd_356_0 ≤ 0rcd_356_0rcd_356_0 ≤ 0rcd_352_post + rcd_352_post ≤ 0rcd_352_postrcd_352_post ≤ 0rcd_352_0 + rcd_352_0 ≤ 0rcd_352_0rcd_352_0 ≤ 0rcd_264_post + rcd_264_post ≤ 0rcd_264_postrcd_264_post ≤ 0rcd_264_0 + rcd_264_0 ≤ 0rcd_264_0rcd_264_0 ≤ 0rcd_237_post + rcd_237_post ≤ 0rcd_237_postrcd_237_post ≤ 0rcd_237_0 + rcd_237_0 ≤ 0rcd_237_0rcd_237_0 ≤ 0rcd_228_post + rcd_228_post ≤ 0rcd_228_postrcd_228_post ≤ 0rcd_228_0 + rcd_228_0 ≤ 0rcd_228_0rcd_228_0 ≤ 0rcd_226_post + rcd_226_post ≤ 0rcd_226_postrcd_226_post ≤ 0rcd_226_0 + rcd_226_0 ≤ 0rcd_226_0rcd_226_0 ≤ 0rcd_222_post + rcd_222_post ≤ 0rcd_222_postrcd_222_post ≤ 0rcd_222_0 + rcd_222_0 ≤ 0rcd_222_0rcd_222_0 ≤ 0rcd_113_post + rcd_113_post ≤ 0rcd_113_postrcd_113_post ≤ 0rcd_113_0 + rcd_113_0 ≤ 0rcd_113_0rcd_113_0 ≤ 0rcd_105_post + rcd_105_post ≤ 0rcd_105_postrcd_105_post ≤ 0rcd_105_0 + rcd_105_0 ≤ 0rcd_105_0rcd_105_0 ≤ 0r_42_post + r_42_post ≤ 0r_42_postr_42_post ≤ 0r_42_0 + r_42_0 ≤ 0r_42_0r_42_0 ≤ 0r_236_post + r_236_post ≤ 0r_236_postr_236_post ≤ 0r_236_0 + r_236_0 ≤ 0r_236_0r_236_0 ≤ 0r_178_post + r_178_post ≤ 0r_178_postr_178_post ≤ 0r_178_0 + r_178_0 ≤ 0r_178_0r_178_0 ≤ 0nondet_12_post + nondet_12_post ≤ 0nondet_12_postnondet_12_post ≤ 0nondet_12_1 + nondet_12_1 ≤ 0nondet_12_1nondet_12_1 ≤ 0nondet_12_0 + nondet_12_0 ≤ 0nondet_12_0nondet_12_0 ≤ 0lt_483_post + lt_483_post ≤ 0lt_483_postlt_483_post ≤ 0lt_483_0 + lt_483_0 ≤ 0lt_483_0lt_483_0 ≤ 0lt_386_post + lt_386_post ≤ 0lt_386_postlt_386_post ≤ 0lt_386_0 + lt_386_0 ≤ 0lt_386_0lt_386_0 ≤ 0lt_29_post + lt_29_post ≤ 0lt_29_postlt_29_post ≤ 0lt_29_1 + lt_29_1 ≤ 0lt_29_1lt_29_1 ≤ 0lt_29_0 + lt_29_0 ≤ 0lt_29_0lt_29_0 ≤ 0lt_17_post + lt_17_post ≤ 0lt_17_postlt_17_post ≤ 0lt_17_0 + lt_17_0 ≤ 0lt_17_0lt_17_0 ≤ 0length_32_post + length_32_post ≤ 0length_32_postlength_32_post ≤ 0length_32_0 + length_32_0 ≤ 0length_32_0length_32_0 ≤ 0len_286_post + len_286_post ≤ 0len_286_postlen_286_post ≤ 0len_286_0 + len_286_0 ≤ 0len_286_0len_286_0 ≤ 0len_266_post + len_266_post ≤ 0len_266_postlen_266_post ≤ 0len_266_0 + len_266_0 ≤ 0len_266_0len_266_0 ≤ 0len_195_post + len_195_post ≤ 0len_195_postlen_195_post ≤ 0len_195_0 + len_195_0 ≤ 0len_195_0len_195_0 ≤ 0i_33_post + i_33_post ≤ 0i_33_posti_33_post ≤ 0i_33_0 + i_33_0 ≤ 0i_33_0i_33_0 ≤ 0i_227_post + i_227_post ≤ 0i_227_posti_227_post ≤ 0i_227_0 + i_227_0 ≤ 0i_227_0i_227_0 ≤ 0i_120_post + i_120_post ≤ 0i_120_posti_120_post ≤ 0i_120_0 + i_120_0 ≤ 0i_120_0i_120_0 ≤ 0i_111_post + i_111_post ≤ 0i_111_posti_111_post ≤ 0i_111_0 + i_111_0 ≤ 0i_111_0i_111_0 ≤ 0head_35_post + head_35_post ≤ 0head_35_posthead_35_post ≤ 0head_35_0 + head_35_0 ≤ 0head_35_0head_35_0 ≤ 0head_13_post + head_13_post ≤ 0head_13_posthead_13_post ≤ 0head_13_0 + head_13_0 ≤ 0head_13_0head_13_0 ≤ 0ct_20_post + ct_20_post ≤ 0ct_20_postct_20_post ≤ 0ct_20_2 + ct_20_2 ≤ 0ct_20_2ct_20_2 ≤ 0ct_20_1 + ct_20_1 ≤ 0ct_20_1ct_20_1 ≤ 0ct_20_0 + ct_20_0 ≤ 0ct_20_0ct_20_0 ≤ 0a_377_post + a_377_post ≤ 0a_377_posta_377_post ≤ 0a_377_0 + a_377_0 ≤ 0a_377_0a_377_0 ≤ 0a_347_post + a_347_post ≤ 0a_347_posta_347_post ≤ 0a_347_0 + a_347_0 ≤ 0a_347_0a_347_0 ≤ 0a_321_post + a_321_post ≤ 0a_321_posta_321_post ≤ 0a_321_0 + a_321_0 ≤ 0a_321_0a_321_0 ≤ 0a_27_post + a_27_post ≤ 0a_27_posta_27_post ≤ 0a_27_1 + a_27_1 ≤ 0a_27_1a_27_1 ≤ 0a_27_0 + a_27_0 ≤ 0a_27_0a_27_0 ≤ 0a_267_post + a_267_post ≤ 0a_267_posta_267_post ≤ 0a_267_0 + a_267_0 ≤ 0a_267_0a_267_0 ≤ 0a_210_post + a_210_post ≤ 0a_210_posta_210_post ≤ 0a_210_0 + a_210_0 ≤ 0a_210_0a_210_0 ≤ 0a_166_post + a_166_post ≤ 0a_166_posta_166_post ≤ 0a_166_0 + a_166_0 ≤ 0a_166_0a_166_0 ≤ 0
and for every transition t, a duplicate t is considered.

2 Transition Removal

We remove transitions 0, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 47, 48, 49, 50, 51, 71, 72 using the following ranking functions, which are bounded by −75.

66: 0
65: 0
45: 0
25: 0
26: 0
27: 0
28: 0
29: 0
30: 0
31: 0
32: 0
33: 0
34: 0
35: 0
36: 0
37: 0
38: 0
44: 0
39: 0
40: 0
41: 0
42: 0
43: 0
48: 0
49: 0
50: 0
51: 0
52: 0
46: 0
47: 0
18: 0
19: 0
20: 0
21: 0
22: 0
23: 0
24: 0
0: 0
2: 0
3: 0
4: 0
5: 0
6: 0
7: 0
8: 0
1: 0
66: −34
65: −35
45: −36
25: −37
26: −38
27: −39
28: −40
29: −41
30: −42
31: −43
32: −44
33: −45
34: −46
35: −47
36: −48
37: −49
38: −50
44: −50
38_var_snapshot: −50
38*: −50
39: −53
40: −54
41: −55
42: −56
43: −57
48: −57
49: −57
50: −57
51: −57
52: −57
43_var_snapshot: −57
43*: −57
46: −60
47: −61
18: −62
19: −63
20: −64
21: −65
22: −66
23: −67
24: −68
0: −69
2: −69
3: −69
4: −69
5: −69
6: −69
7: −69
8: −69
0_var_snapshot: −69
0*: −69
1: −73

3 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

0* 76 0: z_389_post + z_389_post ≤ 0z_389_postz_389_post ≤ 0z_389_0 + z_389_0 ≤ 0z_389_0z_389_0 ≤ 0z_28_post + z_28_post ≤ 0z_28_postz_28_post ≤ 0z_28_1 + z_28_1 ≤ 0z_28_1z_28_1 ≤ 0z_28_0 + z_28_0 ≤ 0z_28_0z_28_0 ≤ 0z_279_post + z_279_post ≤ 0z_279_postz_279_post ≤ 0z_279_0 + z_279_0 ≤ 0z_279_0z_279_0 ≤ 0z_265_post + z_265_post ≤ 0z_265_postz_265_post ≤ 0z_265_0 + z_265_0 ≤ 0z_265_0z_265_0 ≤ 0z_252_post + z_252_post ≤ 0z_252_postz_252_post ≤ 0z_252_0 + z_252_0 ≤ 0z_252_0z_252_0 ≤ 0z_238_post + z_238_post ≤ 0z_238_postz_238_post ≤ 0z_238_0 + z_238_0 ≤ 0z_238_0z_238_0 ≤ 0z_229_post + z_229_post ≤ 0z_229_postz_229_post ≤ 0z_229_0 + z_229_0 ≤ 0z_229_0z_229_0 ≤ 0z_188_post + z_188_post ≤ 0z_188_postz_188_post ≤ 0z_188_0 + z_188_0 ≤ 0z_188_0z_188_0 ≤ 0z_160_post + z_160_post ≤ 0z_160_postz_160_post ≤ 0z_160_0 + z_160_0 ≤ 0z_160_0z_160_0 ≤ 0y_22_post + y_22_post ≤ 0y_22_posty_22_post ≤ 0y_22_2 + y_22_2 ≤ 0y_22_2y_22_2 ≤ 0y_22_1 + y_22_1 ≤ 0y_22_1y_22_1 ≤ 0y_22_0 + y_22_0 ≤ 0y_22_0y_22_0 ≤ 0x_SLAM_f_21_post + x_SLAM_f_21_post ≤ 0x_SLAM_f_21_postx_SLAM_f_21_post ≤ 0x_SLAM_f_21_2 + x_SLAM_f_21_2 ≤ 0x_SLAM_f_21_2x_SLAM_f_21_2 ≤ 0x_SLAM_f_21_1 + x_SLAM_f_21_1 ≤ 0x_SLAM_f_21_1x_SLAM_f_21_1 ≤ 0x_SLAM_f_21_0 + x_SLAM_f_21_0 ≤ 0x_SLAM_f_21_0x_SLAM_f_21_0 ≤ 0x_23_post + x_23_post ≤ 0x_23_postx_23_post ≤ 0x_23_2 + x_23_2 ≤ 0x_23_2x_23_2 ≤ 0x_23_1 + x_23_1 ≤ 0x_23_1x_23_1 ≤ 0x_23_0 + x_23_0 ≤ 0x_23_0x_23_0 ≤ 0x_19_post + x_19_post ≤ 0x_19_postx_19_post ≤ 0x_19_1 + x_19_1 ≤ 0x_19_1x_19_1 ≤ 0x_19_0 + x_19_0 ≤ 0x_19_0x_19_0 ≤ 0tmp_37_post + tmp_37_post ≤ 0tmp_37_posttmp_37_post ≤ 0tmp_37_0 + tmp_37_0 ≤ 0tmp_37_0tmp_37_0 ≤ 0temp_38_post + temp_38_post ≤ 0temp_38_posttemp_38_post ≤ 0temp_38_0 + temp_38_0 ≤ 0temp_38_0temp_38_0 ≤ 0temp1_30_post + temp1_30_post ≤ 0temp1_30_posttemp1_30_post ≤ 0temp1_30_0 + temp1_30_0 ≤ 0temp1_30_0temp1_30_0 ≤ 0temp0_34_post + temp0_34_post ≤ 0temp0_34_posttemp0_34_post ≤ 0temp0_34_1 + temp0_34_1 ≤ 0temp0_34_1temp0_34_1 ≤ 0temp0_34_0 + temp0_34_0 ≤ 0temp0_34_0temp0_34_0 ≤ 0temp0_18_0 + temp0_18_0 ≤ 0temp0_18_0temp0_18_0 ≤ 0t_24_post + t_24_post ≤ 0t_24_postt_24_post ≤ 0t_24_1 + t_24_1 ≤ 0t_24_1t_24_1 ≤ 0t_24_0 + t_24_0 ≤ 0t_24_0t_24_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_post + result_dot_nondet_sdv_special_RETURN_VALUE_14_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_postresult_dot_nondet_sdv_special_RETURN_VALUE_14_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_2 + result_dot_nondet_sdv_special_RETURN_VALUE_14_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_2result_dot_nondet_sdv_special_RETURN_VALUE_14_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_1result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_0 + result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_0result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_postresult_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_0 ≤ 0result_11_post + result_11_post ≤ 0result_11_postresult_11_post ≤ 0result_11_2 + result_11_2 ≤ 0result_11_2result_11_2 ≤ 0result_11_1 + result_11_1 ≤ 0result_11_1result_11_1 ≤ 0result_11_0 + result_11_0 ≤ 0result_11_0result_11_0 ≤ 0rcd_70_post + rcd_70_post ≤ 0rcd_70_postrcd_70_post ≤ 0rcd_70_0 + rcd_70_0 ≤ 0rcd_70_0rcd_70_0 ≤ 0rcd_46_post + rcd_46_post ≤ 0rcd_46_postrcd_46_post ≤ 0rcd_46_0 + rcd_46_0 ≤ 0rcd_46_0rcd_46_0 ≤ 0rcd_396_post + rcd_396_post ≤ 0rcd_396_postrcd_396_post ≤ 0rcd_396_0 + rcd_396_0 ≤ 0rcd_396_0rcd_396_0 ≤ 0rcd_376_post + rcd_376_post ≤ 0rcd_376_postrcd_376_post ≤ 0rcd_376_0 + rcd_376_0 ≤ 0rcd_376_0rcd_376_0 ≤ 0rcd_356_post + rcd_356_post ≤ 0rcd_356_postrcd_356_post ≤ 0rcd_356_0 + rcd_356_0 ≤ 0rcd_356_0rcd_356_0 ≤ 0rcd_352_post + rcd_352_post ≤ 0rcd_352_postrcd_352_post ≤ 0rcd_352_0 + rcd_352_0 ≤ 0rcd_352_0rcd_352_0 ≤ 0rcd_264_post + rcd_264_post ≤ 0rcd_264_postrcd_264_post ≤ 0rcd_264_0 + rcd_264_0 ≤ 0rcd_264_0rcd_264_0 ≤ 0rcd_237_post + rcd_237_post ≤ 0rcd_237_postrcd_237_post ≤ 0rcd_237_0 + rcd_237_0 ≤ 0rcd_237_0rcd_237_0 ≤ 0rcd_228_post + rcd_228_post ≤ 0rcd_228_postrcd_228_post ≤ 0rcd_228_0 + rcd_228_0 ≤ 0rcd_228_0rcd_228_0 ≤ 0rcd_226_post + rcd_226_post ≤ 0rcd_226_postrcd_226_post ≤ 0rcd_226_0 + rcd_226_0 ≤ 0rcd_226_0rcd_226_0 ≤ 0rcd_222_post + rcd_222_post ≤ 0rcd_222_postrcd_222_post ≤ 0rcd_222_0 + rcd_222_0 ≤ 0rcd_222_0rcd_222_0 ≤ 0rcd_113_post + rcd_113_post ≤ 0rcd_113_postrcd_113_post ≤ 0rcd_113_0 + rcd_113_0 ≤ 0rcd_113_0rcd_113_0 ≤ 0rcd_105_post + rcd_105_post ≤ 0rcd_105_postrcd_105_post ≤ 0rcd_105_0 + rcd_105_0 ≤ 0rcd_105_0rcd_105_0 ≤ 0r_42_post + r_42_post ≤ 0r_42_postr_42_post ≤ 0r_42_0 + r_42_0 ≤ 0r_42_0r_42_0 ≤ 0r_236_post + r_236_post ≤ 0r_236_postr_236_post ≤ 0r_236_0 + r_236_0 ≤ 0r_236_0r_236_0 ≤ 0r_178_post + r_178_post ≤ 0r_178_postr_178_post ≤ 0r_178_0 + r_178_0 ≤ 0r_178_0r_178_0 ≤ 0nondet_12_post + nondet_12_post ≤ 0nondet_12_postnondet_12_post ≤ 0nondet_12_1 + nondet_12_1 ≤ 0nondet_12_1nondet_12_1 ≤ 0nondet_12_0 + nondet_12_0 ≤ 0nondet_12_0nondet_12_0 ≤ 0lt_483_post + lt_483_post ≤ 0lt_483_postlt_483_post ≤ 0lt_483_0 + lt_483_0 ≤ 0lt_483_0lt_483_0 ≤ 0lt_386_post + lt_386_post ≤ 0lt_386_postlt_386_post ≤ 0lt_386_0 + lt_386_0 ≤ 0lt_386_0lt_386_0 ≤ 0lt_29_post + lt_29_post ≤ 0lt_29_postlt_29_post ≤ 0lt_29_1 + lt_29_1 ≤ 0lt_29_1lt_29_1 ≤ 0lt_29_0 + lt_29_0 ≤ 0lt_29_0lt_29_0 ≤ 0lt_17_post + lt_17_post ≤ 0lt_17_postlt_17_post ≤ 0lt_17_0 + lt_17_0 ≤ 0lt_17_0lt_17_0 ≤ 0length_32_post + length_32_post ≤ 0length_32_postlength_32_post ≤ 0length_32_0 + length_32_0 ≤ 0length_32_0length_32_0 ≤ 0len_286_post + len_286_post ≤ 0len_286_postlen_286_post ≤ 0len_286_0 + len_286_0 ≤ 0len_286_0len_286_0 ≤ 0len_266_post + len_266_post ≤ 0len_266_postlen_266_post ≤ 0len_266_0 + len_266_0 ≤ 0len_266_0len_266_0 ≤ 0len_195_post + len_195_post ≤ 0len_195_postlen_195_post ≤ 0len_195_0 + len_195_0 ≤ 0len_195_0len_195_0 ≤ 0i_33_post + i_33_post ≤ 0i_33_posti_33_post ≤ 0i_33_0 + i_33_0 ≤ 0i_33_0i_33_0 ≤ 0i_227_post + i_227_post ≤ 0i_227_posti_227_post ≤ 0i_227_0 + i_227_0 ≤ 0i_227_0i_227_0 ≤ 0i_120_post + i_120_post ≤ 0i_120_posti_120_post ≤ 0i_120_0 + i_120_0 ≤ 0i_120_0i_120_0 ≤ 0i_111_post + i_111_post ≤ 0i_111_posti_111_post ≤ 0i_111_0 + i_111_0 ≤ 0i_111_0i_111_0 ≤ 0head_35_post + head_35_post ≤ 0head_35_posthead_35_post ≤ 0head_35_0 + head_35_0 ≤ 0head_35_0head_35_0 ≤ 0head_13_post + head_13_post ≤ 0head_13_posthead_13_post ≤ 0head_13_0 + head_13_0 ≤ 0head_13_0head_13_0 ≤ 0ct_20_post + ct_20_post ≤ 0ct_20_postct_20_post ≤ 0ct_20_2 + ct_20_2 ≤ 0ct_20_2ct_20_2 ≤ 0ct_20_1 + ct_20_1 ≤ 0ct_20_1ct_20_1 ≤ 0ct_20_0 + ct_20_0 ≤ 0ct_20_0ct_20_0 ≤ 0a_377_post + a_377_post ≤ 0a_377_posta_377_post ≤ 0a_377_0 + a_377_0 ≤ 0a_377_0a_377_0 ≤ 0a_347_post + a_347_post ≤ 0a_347_posta_347_post ≤ 0a_347_0 + a_347_0 ≤ 0a_347_0a_347_0 ≤ 0a_321_post + a_321_post ≤ 0a_321_posta_321_post ≤ 0a_321_0 + a_321_0 ≤ 0a_321_0a_321_0 ≤ 0a_27_post + a_27_post ≤ 0a_27_posta_27_post ≤ 0a_27_1 + a_27_1 ≤ 0a_27_1a_27_1 ≤ 0a_27_0 + a_27_0 ≤ 0a_27_0a_27_0 ≤ 0a_267_post + a_267_post ≤ 0a_267_posta_267_post ≤ 0a_267_0 + a_267_0 ≤ 0a_267_0a_267_0 ≤ 0a_210_post + a_210_post ≤ 0a_210_posta_210_post ≤ 0a_210_0 + a_210_0 ≤ 0a_210_0a_210_0 ≤ 0a_166_post + a_166_post ≤ 0a_166_posta_166_post ≤ 0a_166_0 + a_166_0 ≤ 0a_166_0a_166_0 ≤ 0

4 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

0 74 0_var_snapshot: z_389_post + z_389_post ≤ 0z_389_postz_389_post ≤ 0z_389_0 + z_389_0 ≤ 0z_389_0z_389_0 ≤ 0z_28_post + z_28_post ≤ 0z_28_postz_28_post ≤ 0z_28_1 + z_28_1 ≤ 0z_28_1z_28_1 ≤ 0z_28_0 + z_28_0 ≤ 0z_28_0z_28_0 ≤ 0z_279_post + z_279_post ≤ 0z_279_postz_279_post ≤ 0z_279_0 + z_279_0 ≤ 0z_279_0z_279_0 ≤ 0z_265_post + z_265_post ≤ 0z_265_postz_265_post ≤ 0z_265_0 + z_265_0 ≤ 0z_265_0z_265_0 ≤ 0z_252_post + z_252_post ≤ 0z_252_postz_252_post ≤ 0z_252_0 + z_252_0 ≤ 0z_252_0z_252_0 ≤ 0z_238_post + z_238_post ≤ 0z_238_postz_238_post ≤ 0z_238_0 + z_238_0 ≤ 0z_238_0z_238_0 ≤ 0z_229_post + z_229_post ≤ 0z_229_postz_229_post ≤ 0z_229_0 + z_229_0 ≤ 0z_229_0z_229_0 ≤ 0z_188_post + z_188_post ≤ 0z_188_postz_188_post ≤ 0z_188_0 + z_188_0 ≤ 0z_188_0z_188_0 ≤ 0z_160_post + z_160_post ≤ 0z_160_postz_160_post ≤ 0z_160_0 + z_160_0 ≤ 0z_160_0z_160_0 ≤ 0y_22_post + y_22_post ≤ 0y_22_posty_22_post ≤ 0y_22_2 + y_22_2 ≤ 0y_22_2y_22_2 ≤ 0y_22_1 + y_22_1 ≤ 0y_22_1y_22_1 ≤ 0y_22_0 + y_22_0 ≤ 0y_22_0y_22_0 ≤ 0x_SLAM_f_21_post + x_SLAM_f_21_post ≤ 0x_SLAM_f_21_postx_SLAM_f_21_post ≤ 0x_SLAM_f_21_2 + x_SLAM_f_21_2 ≤ 0x_SLAM_f_21_2x_SLAM_f_21_2 ≤ 0x_SLAM_f_21_1 + x_SLAM_f_21_1 ≤ 0x_SLAM_f_21_1x_SLAM_f_21_1 ≤ 0x_SLAM_f_21_0 + x_SLAM_f_21_0 ≤ 0x_SLAM_f_21_0x_SLAM_f_21_0 ≤ 0x_23_post + x_23_post ≤ 0x_23_postx_23_post ≤ 0x_23_2 + x_23_2 ≤ 0x_23_2x_23_2 ≤ 0x_23_1 + x_23_1 ≤ 0x_23_1x_23_1 ≤ 0x_23_0 + x_23_0 ≤ 0x_23_0x_23_0 ≤ 0x_19_post + x_19_post ≤ 0x_19_postx_19_post ≤ 0x_19_1 + x_19_1 ≤ 0x_19_1x_19_1 ≤ 0x_19_0 + x_19_0 ≤ 0x_19_0x_19_0 ≤ 0tmp_37_post + tmp_37_post ≤ 0tmp_37_posttmp_37_post ≤ 0tmp_37_0 + tmp_37_0 ≤ 0tmp_37_0tmp_37_0 ≤ 0temp_38_post + temp_38_post ≤ 0temp_38_posttemp_38_post ≤ 0temp_38_0 + temp_38_0 ≤ 0temp_38_0temp_38_0 ≤ 0temp1_30_post + temp1_30_post ≤ 0temp1_30_posttemp1_30_post ≤ 0temp1_30_0 + temp1_30_0 ≤ 0temp1_30_0temp1_30_0 ≤ 0temp0_34_post + temp0_34_post ≤ 0temp0_34_posttemp0_34_post ≤ 0temp0_34_1 + temp0_34_1 ≤ 0temp0_34_1temp0_34_1 ≤ 0temp0_34_0 + temp0_34_0 ≤ 0temp0_34_0temp0_34_0 ≤ 0temp0_18_0 + temp0_18_0 ≤ 0temp0_18_0temp0_18_0 ≤ 0t_24_post + t_24_post ≤ 0t_24_postt_24_post ≤ 0t_24_1 + t_24_1 ≤ 0t_24_1t_24_1 ≤ 0t_24_0 + t_24_0 ≤ 0t_24_0t_24_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_post + result_dot_nondet_sdv_special_RETURN_VALUE_14_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_postresult_dot_nondet_sdv_special_RETURN_VALUE_14_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_2 + result_dot_nondet_sdv_special_RETURN_VALUE_14_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_2result_dot_nondet_sdv_special_RETURN_VALUE_14_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_1result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_0 + result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_0result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_postresult_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_0 ≤ 0result_11_post + result_11_post ≤ 0result_11_postresult_11_post ≤ 0result_11_2 + result_11_2 ≤ 0result_11_2result_11_2 ≤ 0result_11_1 + result_11_1 ≤ 0result_11_1result_11_1 ≤ 0result_11_0 + result_11_0 ≤ 0result_11_0result_11_0 ≤ 0rcd_70_post + rcd_70_post ≤ 0rcd_70_postrcd_70_post ≤ 0rcd_70_0 + rcd_70_0 ≤ 0rcd_70_0rcd_70_0 ≤ 0rcd_46_post + rcd_46_post ≤ 0rcd_46_postrcd_46_post ≤ 0rcd_46_0 + rcd_46_0 ≤ 0rcd_46_0rcd_46_0 ≤ 0rcd_396_post + rcd_396_post ≤ 0rcd_396_postrcd_396_post ≤ 0rcd_396_0 + rcd_396_0 ≤ 0rcd_396_0rcd_396_0 ≤ 0rcd_376_post + rcd_376_post ≤ 0rcd_376_postrcd_376_post ≤ 0rcd_376_0 + rcd_376_0 ≤ 0rcd_376_0rcd_376_0 ≤ 0rcd_356_post + rcd_356_post ≤ 0rcd_356_postrcd_356_post ≤ 0rcd_356_0 + rcd_356_0 ≤ 0rcd_356_0rcd_356_0 ≤ 0rcd_352_post + rcd_352_post ≤ 0rcd_352_postrcd_352_post ≤ 0rcd_352_0 + rcd_352_0 ≤ 0rcd_352_0rcd_352_0 ≤ 0rcd_264_post + rcd_264_post ≤ 0rcd_264_postrcd_264_post ≤ 0rcd_264_0 + rcd_264_0 ≤ 0rcd_264_0rcd_264_0 ≤ 0rcd_237_post + rcd_237_post ≤ 0rcd_237_postrcd_237_post ≤ 0rcd_237_0 + rcd_237_0 ≤ 0rcd_237_0rcd_237_0 ≤ 0rcd_228_post + rcd_228_post ≤ 0rcd_228_postrcd_228_post ≤ 0rcd_228_0 + rcd_228_0 ≤ 0rcd_228_0rcd_228_0 ≤ 0rcd_226_post + rcd_226_post ≤ 0rcd_226_postrcd_226_post ≤ 0rcd_226_0 + rcd_226_0 ≤ 0rcd_226_0rcd_226_0 ≤ 0rcd_222_post + rcd_222_post ≤ 0rcd_222_postrcd_222_post ≤ 0rcd_222_0 + rcd_222_0 ≤ 0rcd_222_0rcd_222_0 ≤ 0rcd_113_post + rcd_113_post ≤ 0rcd_113_postrcd_113_post ≤ 0rcd_113_0 + rcd_113_0 ≤ 0rcd_113_0rcd_113_0 ≤ 0rcd_105_post + rcd_105_post ≤ 0rcd_105_postrcd_105_post ≤ 0rcd_105_0 + rcd_105_0 ≤ 0rcd_105_0rcd_105_0 ≤ 0r_42_post + r_42_post ≤ 0r_42_postr_42_post ≤ 0r_42_0 + r_42_0 ≤ 0r_42_0r_42_0 ≤ 0r_236_post + r_236_post ≤ 0r_236_postr_236_post ≤ 0r_236_0 + r_236_0 ≤ 0r_236_0r_236_0 ≤ 0r_178_post + r_178_post ≤ 0r_178_postr_178_post ≤ 0r_178_0 + r_178_0 ≤ 0r_178_0r_178_0 ≤ 0nondet_12_post + nondet_12_post ≤ 0nondet_12_postnondet_12_post ≤ 0nondet_12_1 + nondet_12_1 ≤ 0nondet_12_1nondet_12_1 ≤ 0nondet_12_0 + nondet_12_0 ≤ 0nondet_12_0nondet_12_0 ≤ 0lt_483_post + lt_483_post ≤ 0lt_483_postlt_483_post ≤ 0lt_483_0 + lt_483_0 ≤ 0lt_483_0lt_483_0 ≤ 0lt_386_post + lt_386_post ≤ 0lt_386_postlt_386_post ≤ 0lt_386_0 + lt_386_0 ≤ 0lt_386_0lt_386_0 ≤ 0lt_29_post + lt_29_post ≤ 0lt_29_postlt_29_post ≤ 0lt_29_1 + lt_29_1 ≤ 0lt_29_1lt_29_1 ≤ 0lt_29_0 + lt_29_0 ≤ 0lt_29_0lt_29_0 ≤ 0lt_17_post + lt_17_post ≤ 0lt_17_postlt_17_post ≤ 0lt_17_0 + lt_17_0 ≤ 0lt_17_0lt_17_0 ≤ 0length_32_post + length_32_post ≤ 0length_32_postlength_32_post ≤ 0length_32_0 + length_32_0 ≤ 0length_32_0length_32_0 ≤ 0len_286_post + len_286_post ≤ 0len_286_postlen_286_post ≤ 0len_286_0 + len_286_0 ≤ 0len_286_0len_286_0 ≤ 0len_266_post + len_266_post ≤ 0len_266_postlen_266_post ≤ 0len_266_0 + len_266_0 ≤ 0len_266_0len_266_0 ≤ 0len_195_post + len_195_post ≤ 0len_195_postlen_195_post ≤ 0len_195_0 + len_195_0 ≤ 0len_195_0len_195_0 ≤ 0i_33_post + i_33_post ≤ 0i_33_posti_33_post ≤ 0i_33_0 + i_33_0 ≤ 0i_33_0i_33_0 ≤ 0i_227_post + i_227_post ≤ 0i_227_posti_227_post ≤ 0i_227_0 + i_227_0 ≤ 0i_227_0i_227_0 ≤ 0i_120_post + i_120_post ≤ 0i_120_posti_120_post ≤ 0i_120_0 + i_120_0 ≤ 0i_120_0i_120_0 ≤ 0i_111_post + i_111_post ≤ 0i_111_posti_111_post ≤ 0i_111_0 + i_111_0 ≤ 0i_111_0i_111_0 ≤ 0head_35_post + head_35_post ≤ 0head_35_posthead_35_post ≤ 0head_35_0 + head_35_0 ≤ 0head_35_0head_35_0 ≤ 0head_13_post + head_13_post ≤ 0head_13_posthead_13_post ≤ 0head_13_0 + head_13_0 ≤ 0head_13_0head_13_0 ≤ 0ct_20_post + ct_20_post ≤ 0ct_20_postct_20_post ≤ 0ct_20_2 + ct_20_2 ≤ 0ct_20_2ct_20_2 ≤ 0ct_20_1 + ct_20_1 ≤ 0ct_20_1ct_20_1 ≤ 0ct_20_0 + ct_20_0 ≤ 0ct_20_0ct_20_0 ≤ 0a_377_post + a_377_post ≤ 0a_377_posta_377_post ≤ 0a_377_0 + a_377_0 ≤ 0a_377_0a_377_0 ≤ 0a_347_post + a_347_post ≤ 0a_347_posta_347_post ≤ 0a_347_0 + a_347_0 ≤ 0a_347_0a_347_0 ≤ 0a_321_post + a_321_post ≤ 0a_321_posta_321_post ≤ 0a_321_0 + a_321_0 ≤ 0a_321_0a_321_0 ≤ 0a_27_post + a_27_post ≤ 0a_27_posta_27_post ≤ 0a_27_1 + a_27_1 ≤ 0a_27_1a_27_1 ≤ 0a_27_0 + a_27_0 ≤ 0a_27_0a_27_0 ≤ 0a_267_post + a_267_post ≤ 0a_267_posta_267_post ≤ 0a_267_0 + a_267_0 ≤ 0a_267_0a_267_0 ≤ 0a_210_post + a_210_post ≤ 0a_210_posta_210_post ≤ 0a_210_0 + a_210_0 ≤ 0a_210_0a_210_0 ≤ 0a_166_post + a_166_post ≤ 0a_166_posta_166_post ≤ 0a_166_0 + a_166_0 ≤ 0a_166_0a_166_0 ≤ 0

5 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

38* 83 38: z_389_post + z_389_post ≤ 0z_389_postz_389_post ≤ 0z_389_0 + z_389_0 ≤ 0z_389_0z_389_0 ≤ 0z_28_post + z_28_post ≤ 0z_28_postz_28_post ≤ 0z_28_1 + z_28_1 ≤ 0z_28_1z_28_1 ≤ 0z_28_0 + z_28_0 ≤ 0z_28_0z_28_0 ≤ 0z_279_post + z_279_post ≤ 0z_279_postz_279_post ≤ 0z_279_0 + z_279_0 ≤ 0z_279_0z_279_0 ≤ 0z_265_post + z_265_post ≤ 0z_265_postz_265_post ≤ 0z_265_0 + z_265_0 ≤ 0z_265_0z_265_0 ≤ 0z_252_post + z_252_post ≤ 0z_252_postz_252_post ≤ 0z_252_0 + z_252_0 ≤ 0z_252_0z_252_0 ≤ 0z_238_post + z_238_post ≤ 0z_238_postz_238_post ≤ 0z_238_0 + z_238_0 ≤ 0z_238_0z_238_0 ≤ 0z_229_post + z_229_post ≤ 0z_229_postz_229_post ≤ 0z_229_0 + z_229_0 ≤ 0z_229_0z_229_0 ≤ 0z_188_post + z_188_post ≤ 0z_188_postz_188_post ≤ 0z_188_0 + z_188_0 ≤ 0z_188_0z_188_0 ≤ 0z_160_post + z_160_post ≤ 0z_160_postz_160_post ≤ 0z_160_0 + z_160_0 ≤ 0z_160_0z_160_0 ≤ 0y_22_post + y_22_post ≤ 0y_22_posty_22_post ≤ 0y_22_2 + y_22_2 ≤ 0y_22_2y_22_2 ≤ 0y_22_1 + y_22_1 ≤ 0y_22_1y_22_1 ≤ 0y_22_0 + y_22_0 ≤ 0y_22_0y_22_0 ≤ 0x_SLAM_f_21_post + x_SLAM_f_21_post ≤ 0x_SLAM_f_21_postx_SLAM_f_21_post ≤ 0x_SLAM_f_21_2 + x_SLAM_f_21_2 ≤ 0x_SLAM_f_21_2x_SLAM_f_21_2 ≤ 0x_SLAM_f_21_1 + x_SLAM_f_21_1 ≤ 0x_SLAM_f_21_1x_SLAM_f_21_1 ≤ 0x_SLAM_f_21_0 + x_SLAM_f_21_0 ≤ 0x_SLAM_f_21_0x_SLAM_f_21_0 ≤ 0x_23_post + x_23_post ≤ 0x_23_postx_23_post ≤ 0x_23_2 + x_23_2 ≤ 0x_23_2x_23_2 ≤ 0x_23_1 + x_23_1 ≤ 0x_23_1x_23_1 ≤ 0x_23_0 + x_23_0 ≤ 0x_23_0x_23_0 ≤ 0x_19_post + x_19_post ≤ 0x_19_postx_19_post ≤ 0x_19_1 + x_19_1 ≤ 0x_19_1x_19_1 ≤ 0x_19_0 + x_19_0 ≤ 0x_19_0x_19_0 ≤ 0tmp_37_post + tmp_37_post ≤ 0tmp_37_posttmp_37_post ≤ 0tmp_37_0 + tmp_37_0 ≤ 0tmp_37_0tmp_37_0 ≤ 0temp_38_post + temp_38_post ≤ 0temp_38_posttemp_38_post ≤ 0temp_38_0 + temp_38_0 ≤ 0temp_38_0temp_38_0 ≤ 0temp1_30_post + temp1_30_post ≤ 0temp1_30_posttemp1_30_post ≤ 0temp1_30_0 + temp1_30_0 ≤ 0temp1_30_0temp1_30_0 ≤ 0temp0_34_post + temp0_34_post ≤ 0temp0_34_posttemp0_34_post ≤ 0temp0_34_1 + temp0_34_1 ≤ 0temp0_34_1temp0_34_1 ≤ 0temp0_34_0 + temp0_34_0 ≤ 0temp0_34_0temp0_34_0 ≤ 0temp0_18_0 + temp0_18_0 ≤ 0temp0_18_0temp0_18_0 ≤ 0t_24_post + t_24_post ≤ 0t_24_postt_24_post ≤ 0t_24_1 + t_24_1 ≤ 0t_24_1t_24_1 ≤ 0t_24_0 + t_24_0 ≤ 0t_24_0t_24_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_post + result_dot_nondet_sdv_special_RETURN_VALUE_14_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_postresult_dot_nondet_sdv_special_RETURN_VALUE_14_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_2 + result_dot_nondet_sdv_special_RETURN_VALUE_14_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_2result_dot_nondet_sdv_special_RETURN_VALUE_14_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_1result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_0 + result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_0result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_postresult_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_0 ≤ 0result_11_post + result_11_post ≤ 0result_11_postresult_11_post ≤ 0result_11_2 + result_11_2 ≤ 0result_11_2result_11_2 ≤ 0result_11_1 + result_11_1 ≤ 0result_11_1result_11_1 ≤ 0result_11_0 + result_11_0 ≤ 0result_11_0result_11_0 ≤ 0rcd_70_post + rcd_70_post ≤ 0rcd_70_postrcd_70_post ≤ 0rcd_70_0 + rcd_70_0 ≤ 0rcd_70_0rcd_70_0 ≤ 0rcd_46_post + rcd_46_post ≤ 0rcd_46_postrcd_46_post ≤ 0rcd_46_0 + rcd_46_0 ≤ 0rcd_46_0rcd_46_0 ≤ 0rcd_396_post + rcd_396_post ≤ 0rcd_396_postrcd_396_post ≤ 0rcd_396_0 + rcd_396_0 ≤ 0rcd_396_0rcd_396_0 ≤ 0rcd_376_post + rcd_376_post ≤ 0rcd_376_postrcd_376_post ≤ 0rcd_376_0 + rcd_376_0 ≤ 0rcd_376_0rcd_376_0 ≤ 0rcd_356_post + rcd_356_post ≤ 0rcd_356_postrcd_356_post ≤ 0rcd_356_0 + rcd_356_0 ≤ 0rcd_356_0rcd_356_0 ≤ 0rcd_352_post + rcd_352_post ≤ 0rcd_352_postrcd_352_post ≤ 0rcd_352_0 + rcd_352_0 ≤ 0rcd_352_0rcd_352_0 ≤ 0rcd_264_post + rcd_264_post ≤ 0rcd_264_postrcd_264_post ≤ 0rcd_264_0 + rcd_264_0 ≤ 0rcd_264_0rcd_264_0 ≤ 0rcd_237_post + rcd_237_post ≤ 0rcd_237_postrcd_237_post ≤ 0rcd_237_0 + rcd_237_0 ≤ 0rcd_237_0rcd_237_0 ≤ 0rcd_228_post + rcd_228_post ≤ 0rcd_228_postrcd_228_post ≤ 0rcd_228_0 + rcd_228_0 ≤ 0rcd_228_0rcd_228_0 ≤ 0rcd_226_post + rcd_226_post ≤ 0rcd_226_postrcd_226_post ≤ 0rcd_226_0 + rcd_226_0 ≤ 0rcd_226_0rcd_226_0 ≤ 0rcd_222_post + rcd_222_post ≤ 0rcd_222_postrcd_222_post ≤ 0rcd_222_0 + rcd_222_0 ≤ 0rcd_222_0rcd_222_0 ≤ 0rcd_113_post + rcd_113_post ≤ 0rcd_113_postrcd_113_post ≤ 0rcd_113_0 + rcd_113_0 ≤ 0rcd_113_0rcd_113_0 ≤ 0rcd_105_post + rcd_105_post ≤ 0rcd_105_postrcd_105_post ≤ 0rcd_105_0 + rcd_105_0 ≤ 0rcd_105_0rcd_105_0 ≤ 0r_42_post + r_42_post ≤ 0r_42_postr_42_post ≤ 0r_42_0 + r_42_0 ≤ 0r_42_0r_42_0 ≤ 0r_236_post + r_236_post ≤ 0r_236_postr_236_post ≤ 0r_236_0 + r_236_0 ≤ 0r_236_0r_236_0 ≤ 0r_178_post + r_178_post ≤ 0r_178_postr_178_post ≤ 0r_178_0 + r_178_0 ≤ 0r_178_0r_178_0 ≤ 0nondet_12_post + nondet_12_post ≤ 0nondet_12_postnondet_12_post ≤ 0nondet_12_1 + nondet_12_1 ≤ 0nondet_12_1nondet_12_1 ≤ 0nondet_12_0 + nondet_12_0 ≤ 0nondet_12_0nondet_12_0 ≤ 0lt_483_post + lt_483_post ≤ 0lt_483_postlt_483_post ≤ 0lt_483_0 + lt_483_0 ≤ 0lt_483_0lt_483_0 ≤ 0lt_386_post + lt_386_post ≤ 0lt_386_postlt_386_post ≤ 0lt_386_0 + lt_386_0 ≤ 0lt_386_0lt_386_0 ≤ 0lt_29_post + lt_29_post ≤ 0lt_29_postlt_29_post ≤ 0lt_29_1 + lt_29_1 ≤ 0lt_29_1lt_29_1 ≤ 0lt_29_0 + lt_29_0 ≤ 0lt_29_0lt_29_0 ≤ 0lt_17_post + lt_17_post ≤ 0lt_17_postlt_17_post ≤ 0lt_17_0 + lt_17_0 ≤ 0lt_17_0lt_17_0 ≤ 0length_32_post + length_32_post ≤ 0length_32_postlength_32_post ≤ 0length_32_0 + length_32_0 ≤ 0length_32_0length_32_0 ≤ 0len_286_post + len_286_post ≤ 0len_286_postlen_286_post ≤ 0len_286_0 + len_286_0 ≤ 0len_286_0len_286_0 ≤ 0len_266_post + len_266_post ≤ 0len_266_postlen_266_post ≤ 0len_266_0 + len_266_0 ≤ 0len_266_0len_266_0 ≤ 0len_195_post + len_195_post ≤ 0len_195_postlen_195_post ≤ 0len_195_0 + len_195_0 ≤ 0len_195_0len_195_0 ≤ 0i_33_post + i_33_post ≤ 0i_33_posti_33_post ≤ 0i_33_0 + i_33_0 ≤ 0i_33_0i_33_0 ≤ 0i_227_post + i_227_post ≤ 0i_227_posti_227_post ≤ 0i_227_0 + i_227_0 ≤ 0i_227_0i_227_0 ≤ 0i_120_post + i_120_post ≤ 0i_120_posti_120_post ≤ 0i_120_0 + i_120_0 ≤ 0i_120_0i_120_0 ≤ 0i_111_post + i_111_post ≤ 0i_111_posti_111_post ≤ 0i_111_0 + i_111_0 ≤ 0i_111_0i_111_0 ≤ 0head_35_post + head_35_post ≤ 0head_35_posthead_35_post ≤ 0head_35_0 + head_35_0 ≤ 0head_35_0head_35_0 ≤ 0head_13_post + head_13_post ≤ 0head_13_posthead_13_post ≤ 0head_13_0 + head_13_0 ≤ 0head_13_0head_13_0 ≤ 0ct_20_post + ct_20_post ≤ 0ct_20_postct_20_post ≤ 0ct_20_2 + ct_20_2 ≤ 0ct_20_2ct_20_2 ≤ 0ct_20_1 + ct_20_1 ≤ 0ct_20_1ct_20_1 ≤ 0ct_20_0 + ct_20_0 ≤ 0ct_20_0ct_20_0 ≤ 0a_377_post + a_377_post ≤ 0a_377_posta_377_post ≤ 0a_377_0 + a_377_0 ≤ 0a_377_0a_377_0 ≤ 0a_347_post + a_347_post ≤ 0a_347_posta_347_post ≤ 0a_347_0 + a_347_0 ≤ 0a_347_0a_347_0 ≤ 0a_321_post + a_321_post ≤ 0a_321_posta_321_post ≤ 0a_321_0 + a_321_0 ≤ 0a_321_0a_321_0 ≤ 0a_27_post + a_27_post ≤ 0a_27_posta_27_post ≤ 0a_27_1 + a_27_1 ≤ 0a_27_1a_27_1 ≤ 0a_27_0 + a_27_0 ≤ 0a_27_0a_27_0 ≤ 0a_267_post + a_267_post ≤ 0a_267_posta_267_post ≤ 0a_267_0 + a_267_0 ≤ 0a_267_0a_267_0 ≤ 0a_210_post + a_210_post ≤ 0a_210_posta_210_post ≤ 0a_210_0 + a_210_0 ≤ 0a_210_0a_210_0 ≤ 0a_166_post + a_166_post ≤ 0a_166_posta_166_post ≤ 0a_166_0 + a_166_0 ≤ 0a_166_0a_166_0 ≤ 0

6 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

38 81 38_var_snapshot: z_389_post + z_389_post ≤ 0z_389_postz_389_post ≤ 0z_389_0 + z_389_0 ≤ 0z_389_0z_389_0 ≤ 0z_28_post + z_28_post ≤ 0z_28_postz_28_post ≤ 0z_28_1 + z_28_1 ≤ 0z_28_1z_28_1 ≤ 0z_28_0 + z_28_0 ≤ 0z_28_0z_28_0 ≤ 0z_279_post + z_279_post ≤ 0z_279_postz_279_post ≤ 0z_279_0 + z_279_0 ≤ 0z_279_0z_279_0 ≤ 0z_265_post + z_265_post ≤ 0z_265_postz_265_post ≤ 0z_265_0 + z_265_0 ≤ 0z_265_0z_265_0 ≤ 0z_252_post + z_252_post ≤ 0z_252_postz_252_post ≤ 0z_252_0 + z_252_0 ≤ 0z_252_0z_252_0 ≤ 0z_238_post + z_238_post ≤ 0z_238_postz_238_post ≤ 0z_238_0 + z_238_0 ≤ 0z_238_0z_238_0 ≤ 0z_229_post + z_229_post ≤ 0z_229_postz_229_post ≤ 0z_229_0 + z_229_0 ≤ 0z_229_0z_229_0 ≤ 0z_188_post + z_188_post ≤ 0z_188_postz_188_post ≤ 0z_188_0 + z_188_0 ≤ 0z_188_0z_188_0 ≤ 0z_160_post + z_160_post ≤ 0z_160_postz_160_post ≤ 0z_160_0 + z_160_0 ≤ 0z_160_0z_160_0 ≤ 0y_22_post + y_22_post ≤ 0y_22_posty_22_post ≤ 0y_22_2 + y_22_2 ≤ 0y_22_2y_22_2 ≤ 0y_22_1 + y_22_1 ≤ 0y_22_1y_22_1 ≤ 0y_22_0 + y_22_0 ≤ 0y_22_0y_22_0 ≤ 0x_SLAM_f_21_post + x_SLAM_f_21_post ≤ 0x_SLAM_f_21_postx_SLAM_f_21_post ≤ 0x_SLAM_f_21_2 + x_SLAM_f_21_2 ≤ 0x_SLAM_f_21_2x_SLAM_f_21_2 ≤ 0x_SLAM_f_21_1 + x_SLAM_f_21_1 ≤ 0x_SLAM_f_21_1x_SLAM_f_21_1 ≤ 0x_SLAM_f_21_0 + x_SLAM_f_21_0 ≤ 0x_SLAM_f_21_0x_SLAM_f_21_0 ≤ 0x_23_post + x_23_post ≤ 0x_23_postx_23_post ≤ 0x_23_2 + x_23_2 ≤ 0x_23_2x_23_2 ≤ 0x_23_1 + x_23_1 ≤ 0x_23_1x_23_1 ≤ 0x_23_0 + x_23_0 ≤ 0x_23_0x_23_0 ≤ 0x_19_post + x_19_post ≤ 0x_19_postx_19_post ≤ 0x_19_1 + x_19_1 ≤ 0x_19_1x_19_1 ≤ 0x_19_0 + x_19_0 ≤ 0x_19_0x_19_0 ≤ 0tmp_37_post + tmp_37_post ≤ 0tmp_37_posttmp_37_post ≤ 0tmp_37_0 + tmp_37_0 ≤ 0tmp_37_0tmp_37_0 ≤ 0temp_38_post + temp_38_post ≤ 0temp_38_posttemp_38_post ≤ 0temp_38_0 + temp_38_0 ≤ 0temp_38_0temp_38_0 ≤ 0temp1_30_post + temp1_30_post ≤ 0temp1_30_posttemp1_30_post ≤ 0temp1_30_0 + temp1_30_0 ≤ 0temp1_30_0temp1_30_0 ≤ 0temp0_34_post + temp0_34_post ≤ 0temp0_34_posttemp0_34_post ≤ 0temp0_34_1 + temp0_34_1 ≤ 0temp0_34_1temp0_34_1 ≤ 0temp0_34_0 + temp0_34_0 ≤ 0temp0_34_0temp0_34_0 ≤ 0temp0_18_0 + temp0_18_0 ≤ 0temp0_18_0temp0_18_0 ≤ 0t_24_post + t_24_post ≤ 0t_24_postt_24_post ≤ 0t_24_1 + t_24_1 ≤ 0t_24_1t_24_1 ≤ 0t_24_0 + t_24_0 ≤ 0t_24_0t_24_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_post + result_dot_nondet_sdv_special_RETURN_VALUE_14_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_postresult_dot_nondet_sdv_special_RETURN_VALUE_14_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_2 + result_dot_nondet_sdv_special_RETURN_VALUE_14_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_2result_dot_nondet_sdv_special_RETURN_VALUE_14_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_1result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_0 + result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_0result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_postresult_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_0 ≤ 0result_11_post + result_11_post ≤ 0result_11_postresult_11_post ≤ 0result_11_2 + result_11_2 ≤ 0result_11_2result_11_2 ≤ 0result_11_1 + result_11_1 ≤ 0result_11_1result_11_1 ≤ 0result_11_0 + result_11_0 ≤ 0result_11_0result_11_0 ≤ 0rcd_70_post + rcd_70_post ≤ 0rcd_70_postrcd_70_post ≤ 0rcd_70_0 + rcd_70_0 ≤ 0rcd_70_0rcd_70_0 ≤ 0rcd_46_post + rcd_46_post ≤ 0rcd_46_postrcd_46_post ≤ 0rcd_46_0 + rcd_46_0 ≤ 0rcd_46_0rcd_46_0 ≤ 0rcd_396_post + rcd_396_post ≤ 0rcd_396_postrcd_396_post ≤ 0rcd_396_0 + rcd_396_0 ≤ 0rcd_396_0rcd_396_0 ≤ 0rcd_376_post + rcd_376_post ≤ 0rcd_376_postrcd_376_post ≤ 0rcd_376_0 + rcd_376_0 ≤ 0rcd_376_0rcd_376_0 ≤ 0rcd_356_post + rcd_356_post ≤ 0rcd_356_postrcd_356_post ≤ 0rcd_356_0 + rcd_356_0 ≤ 0rcd_356_0rcd_356_0 ≤ 0rcd_352_post + rcd_352_post ≤ 0rcd_352_postrcd_352_post ≤ 0rcd_352_0 + rcd_352_0 ≤ 0rcd_352_0rcd_352_0 ≤ 0rcd_264_post + rcd_264_post ≤ 0rcd_264_postrcd_264_post ≤ 0rcd_264_0 + rcd_264_0 ≤ 0rcd_264_0rcd_264_0 ≤ 0rcd_237_post + rcd_237_post ≤ 0rcd_237_postrcd_237_post ≤ 0rcd_237_0 + rcd_237_0 ≤ 0rcd_237_0rcd_237_0 ≤ 0rcd_228_post + rcd_228_post ≤ 0rcd_228_postrcd_228_post ≤ 0rcd_228_0 + rcd_228_0 ≤ 0rcd_228_0rcd_228_0 ≤ 0rcd_226_post + rcd_226_post ≤ 0rcd_226_postrcd_226_post ≤ 0rcd_226_0 + rcd_226_0 ≤ 0rcd_226_0rcd_226_0 ≤ 0rcd_222_post + rcd_222_post ≤ 0rcd_222_postrcd_222_post ≤ 0rcd_222_0 + rcd_222_0 ≤ 0rcd_222_0rcd_222_0 ≤ 0rcd_113_post + rcd_113_post ≤ 0rcd_113_postrcd_113_post ≤ 0rcd_113_0 + rcd_113_0 ≤ 0rcd_113_0rcd_113_0 ≤ 0rcd_105_post + rcd_105_post ≤ 0rcd_105_postrcd_105_post ≤ 0rcd_105_0 + rcd_105_0 ≤ 0rcd_105_0rcd_105_0 ≤ 0r_42_post + r_42_post ≤ 0r_42_postr_42_post ≤ 0r_42_0 + r_42_0 ≤ 0r_42_0r_42_0 ≤ 0r_236_post + r_236_post ≤ 0r_236_postr_236_post ≤ 0r_236_0 + r_236_0 ≤ 0r_236_0r_236_0 ≤ 0r_178_post + r_178_post ≤ 0r_178_postr_178_post ≤ 0r_178_0 + r_178_0 ≤ 0r_178_0r_178_0 ≤ 0nondet_12_post + nondet_12_post ≤ 0nondet_12_postnondet_12_post ≤ 0nondet_12_1 + nondet_12_1 ≤ 0nondet_12_1nondet_12_1 ≤ 0nondet_12_0 + nondet_12_0 ≤ 0nondet_12_0nondet_12_0 ≤ 0lt_483_post + lt_483_post ≤ 0lt_483_postlt_483_post ≤ 0lt_483_0 + lt_483_0 ≤ 0lt_483_0lt_483_0 ≤ 0lt_386_post + lt_386_post ≤ 0lt_386_postlt_386_post ≤ 0lt_386_0 + lt_386_0 ≤ 0lt_386_0lt_386_0 ≤ 0lt_29_post + lt_29_post ≤ 0lt_29_postlt_29_post ≤ 0lt_29_1 + lt_29_1 ≤ 0lt_29_1lt_29_1 ≤ 0lt_29_0 + lt_29_0 ≤ 0lt_29_0lt_29_0 ≤ 0lt_17_post + lt_17_post ≤ 0lt_17_postlt_17_post ≤ 0lt_17_0 + lt_17_0 ≤ 0lt_17_0lt_17_0 ≤ 0length_32_post + length_32_post ≤ 0length_32_postlength_32_post ≤ 0length_32_0 + length_32_0 ≤ 0length_32_0length_32_0 ≤ 0len_286_post + len_286_post ≤ 0len_286_postlen_286_post ≤ 0len_286_0 + len_286_0 ≤ 0len_286_0len_286_0 ≤ 0len_266_post + len_266_post ≤ 0len_266_postlen_266_post ≤ 0len_266_0 + len_266_0 ≤ 0len_266_0len_266_0 ≤ 0len_195_post + len_195_post ≤ 0len_195_postlen_195_post ≤ 0len_195_0 + len_195_0 ≤ 0len_195_0len_195_0 ≤ 0i_33_post + i_33_post ≤ 0i_33_posti_33_post ≤ 0i_33_0 + i_33_0 ≤ 0i_33_0i_33_0 ≤ 0i_227_post + i_227_post ≤ 0i_227_posti_227_post ≤ 0i_227_0 + i_227_0 ≤ 0i_227_0i_227_0 ≤ 0i_120_post + i_120_post ≤ 0i_120_posti_120_post ≤ 0i_120_0 + i_120_0 ≤ 0i_120_0i_120_0 ≤ 0i_111_post + i_111_post ≤ 0i_111_posti_111_post ≤ 0i_111_0 + i_111_0 ≤ 0i_111_0i_111_0 ≤ 0head_35_post + head_35_post ≤ 0head_35_posthead_35_post ≤ 0head_35_0 + head_35_0 ≤ 0head_35_0head_35_0 ≤ 0head_13_post + head_13_post ≤ 0head_13_posthead_13_post ≤ 0head_13_0 + head_13_0 ≤ 0head_13_0head_13_0 ≤ 0ct_20_post + ct_20_post ≤ 0ct_20_postct_20_post ≤ 0ct_20_2 + ct_20_2 ≤ 0ct_20_2ct_20_2 ≤ 0ct_20_1 + ct_20_1 ≤ 0ct_20_1ct_20_1 ≤ 0ct_20_0 + ct_20_0 ≤ 0ct_20_0ct_20_0 ≤ 0a_377_post + a_377_post ≤ 0a_377_posta_377_post ≤ 0a_377_0 + a_377_0 ≤ 0a_377_0a_377_0 ≤ 0a_347_post + a_347_post ≤ 0a_347_posta_347_post ≤ 0a_347_0 + a_347_0 ≤ 0a_347_0a_347_0 ≤ 0a_321_post + a_321_post ≤ 0a_321_posta_321_post ≤ 0a_321_0 + a_321_0 ≤ 0a_321_0a_321_0 ≤ 0a_27_post + a_27_post ≤ 0a_27_posta_27_post ≤ 0a_27_1 + a_27_1 ≤ 0a_27_1a_27_1 ≤ 0a_27_0 + a_27_0 ≤ 0a_27_0a_27_0 ≤ 0a_267_post + a_267_post ≤ 0a_267_posta_267_post ≤ 0a_267_0 + a_267_0 ≤ 0a_267_0a_267_0 ≤ 0a_210_post + a_210_post ≤ 0a_210_posta_210_post ≤ 0a_210_0 + a_210_0 ≤ 0a_210_0a_210_0 ≤ 0a_166_post + a_166_post ≤ 0a_166_posta_166_post ≤ 0a_166_0 + a_166_0 ≤ 0a_166_0a_166_0 ≤ 0

7 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

43* 90 43: z_389_post + z_389_post ≤ 0z_389_postz_389_post ≤ 0z_389_0 + z_389_0 ≤ 0z_389_0z_389_0 ≤ 0z_28_post + z_28_post ≤ 0z_28_postz_28_post ≤ 0z_28_1 + z_28_1 ≤ 0z_28_1z_28_1 ≤ 0z_28_0 + z_28_0 ≤ 0z_28_0z_28_0 ≤ 0z_279_post + z_279_post ≤ 0z_279_postz_279_post ≤ 0z_279_0 + z_279_0 ≤ 0z_279_0z_279_0 ≤ 0z_265_post + z_265_post ≤ 0z_265_postz_265_post ≤ 0z_265_0 + z_265_0 ≤ 0z_265_0z_265_0 ≤ 0z_252_post + z_252_post ≤ 0z_252_postz_252_post ≤ 0z_252_0 + z_252_0 ≤ 0z_252_0z_252_0 ≤ 0z_238_post + z_238_post ≤ 0z_238_postz_238_post ≤ 0z_238_0 + z_238_0 ≤ 0z_238_0z_238_0 ≤ 0z_229_post + z_229_post ≤ 0z_229_postz_229_post ≤ 0z_229_0 + z_229_0 ≤ 0z_229_0z_229_0 ≤ 0z_188_post + z_188_post ≤ 0z_188_postz_188_post ≤ 0z_188_0 + z_188_0 ≤ 0z_188_0z_188_0 ≤ 0z_160_post + z_160_post ≤ 0z_160_postz_160_post ≤ 0z_160_0 + z_160_0 ≤ 0z_160_0z_160_0 ≤ 0y_22_post + y_22_post ≤ 0y_22_posty_22_post ≤ 0y_22_2 + y_22_2 ≤ 0y_22_2y_22_2 ≤ 0y_22_1 + y_22_1 ≤ 0y_22_1y_22_1 ≤ 0y_22_0 + y_22_0 ≤ 0y_22_0y_22_0 ≤ 0x_SLAM_f_21_post + x_SLAM_f_21_post ≤ 0x_SLAM_f_21_postx_SLAM_f_21_post ≤ 0x_SLAM_f_21_2 + x_SLAM_f_21_2 ≤ 0x_SLAM_f_21_2x_SLAM_f_21_2 ≤ 0x_SLAM_f_21_1 + x_SLAM_f_21_1 ≤ 0x_SLAM_f_21_1x_SLAM_f_21_1 ≤ 0x_SLAM_f_21_0 + x_SLAM_f_21_0 ≤ 0x_SLAM_f_21_0x_SLAM_f_21_0 ≤ 0x_23_post + x_23_post ≤ 0x_23_postx_23_post ≤ 0x_23_2 + x_23_2 ≤ 0x_23_2x_23_2 ≤ 0x_23_1 + x_23_1 ≤ 0x_23_1x_23_1 ≤ 0x_23_0 + x_23_0 ≤ 0x_23_0x_23_0 ≤ 0x_19_post + x_19_post ≤ 0x_19_postx_19_post ≤ 0x_19_1 + x_19_1 ≤ 0x_19_1x_19_1 ≤ 0x_19_0 + x_19_0 ≤ 0x_19_0x_19_0 ≤ 0tmp_37_post + tmp_37_post ≤ 0tmp_37_posttmp_37_post ≤ 0tmp_37_0 + tmp_37_0 ≤ 0tmp_37_0tmp_37_0 ≤ 0temp_38_post + temp_38_post ≤ 0temp_38_posttemp_38_post ≤ 0temp_38_0 + temp_38_0 ≤ 0temp_38_0temp_38_0 ≤ 0temp1_30_post + temp1_30_post ≤ 0temp1_30_posttemp1_30_post ≤ 0temp1_30_0 + temp1_30_0 ≤ 0temp1_30_0temp1_30_0 ≤ 0temp0_34_post + temp0_34_post ≤ 0temp0_34_posttemp0_34_post ≤ 0temp0_34_1 + temp0_34_1 ≤ 0temp0_34_1temp0_34_1 ≤ 0temp0_34_0 + temp0_34_0 ≤ 0temp0_34_0temp0_34_0 ≤ 0temp0_18_0 + temp0_18_0 ≤ 0temp0_18_0temp0_18_0 ≤ 0t_24_post + t_24_post ≤ 0t_24_postt_24_post ≤ 0t_24_1 + t_24_1 ≤ 0t_24_1t_24_1 ≤ 0t_24_0 + t_24_0 ≤ 0t_24_0t_24_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_post + result_dot_nondet_sdv_special_RETURN_VALUE_14_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_postresult_dot_nondet_sdv_special_RETURN_VALUE_14_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_2 + result_dot_nondet_sdv_special_RETURN_VALUE_14_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_2result_dot_nondet_sdv_special_RETURN_VALUE_14_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_1result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_0 + result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_0result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_postresult_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_0 ≤ 0result_11_post + result_11_post ≤ 0result_11_postresult_11_post ≤ 0result_11_2 + result_11_2 ≤ 0result_11_2result_11_2 ≤ 0result_11_1 + result_11_1 ≤ 0result_11_1result_11_1 ≤ 0result_11_0 + result_11_0 ≤ 0result_11_0result_11_0 ≤ 0rcd_70_post + rcd_70_post ≤ 0rcd_70_postrcd_70_post ≤ 0rcd_70_0 + rcd_70_0 ≤ 0rcd_70_0rcd_70_0 ≤ 0rcd_46_post + rcd_46_post ≤ 0rcd_46_postrcd_46_post ≤ 0rcd_46_0 + rcd_46_0 ≤ 0rcd_46_0rcd_46_0 ≤ 0rcd_396_post + rcd_396_post ≤ 0rcd_396_postrcd_396_post ≤ 0rcd_396_0 + rcd_396_0 ≤ 0rcd_396_0rcd_396_0 ≤ 0rcd_376_post + rcd_376_post ≤ 0rcd_376_postrcd_376_post ≤ 0rcd_376_0 + rcd_376_0 ≤ 0rcd_376_0rcd_376_0 ≤ 0rcd_356_post + rcd_356_post ≤ 0rcd_356_postrcd_356_post ≤ 0rcd_356_0 + rcd_356_0 ≤ 0rcd_356_0rcd_356_0 ≤ 0rcd_352_post + rcd_352_post ≤ 0rcd_352_postrcd_352_post ≤ 0rcd_352_0 + rcd_352_0 ≤ 0rcd_352_0rcd_352_0 ≤ 0rcd_264_post + rcd_264_post ≤ 0rcd_264_postrcd_264_post ≤ 0rcd_264_0 + rcd_264_0 ≤ 0rcd_264_0rcd_264_0 ≤ 0rcd_237_post + rcd_237_post ≤ 0rcd_237_postrcd_237_post ≤ 0rcd_237_0 + rcd_237_0 ≤ 0rcd_237_0rcd_237_0 ≤ 0rcd_228_post + rcd_228_post ≤ 0rcd_228_postrcd_228_post ≤ 0rcd_228_0 + rcd_228_0 ≤ 0rcd_228_0rcd_228_0 ≤ 0rcd_226_post + rcd_226_post ≤ 0rcd_226_postrcd_226_post ≤ 0rcd_226_0 + rcd_226_0 ≤ 0rcd_226_0rcd_226_0 ≤ 0rcd_222_post + rcd_222_post ≤ 0rcd_222_postrcd_222_post ≤ 0rcd_222_0 + rcd_222_0 ≤ 0rcd_222_0rcd_222_0 ≤ 0rcd_113_post + rcd_113_post ≤ 0rcd_113_postrcd_113_post ≤ 0rcd_113_0 + rcd_113_0 ≤ 0rcd_113_0rcd_113_0 ≤ 0rcd_105_post + rcd_105_post ≤ 0rcd_105_postrcd_105_post ≤ 0rcd_105_0 + rcd_105_0 ≤ 0rcd_105_0rcd_105_0 ≤ 0r_42_post + r_42_post ≤ 0r_42_postr_42_post ≤ 0r_42_0 + r_42_0 ≤ 0r_42_0r_42_0 ≤ 0r_236_post + r_236_post ≤ 0r_236_postr_236_post ≤ 0r_236_0 + r_236_0 ≤ 0r_236_0r_236_0 ≤ 0r_178_post + r_178_post ≤ 0r_178_postr_178_post ≤ 0r_178_0 + r_178_0 ≤ 0r_178_0r_178_0 ≤ 0nondet_12_post + nondet_12_post ≤ 0nondet_12_postnondet_12_post ≤ 0nondet_12_1 + nondet_12_1 ≤ 0nondet_12_1nondet_12_1 ≤ 0nondet_12_0 + nondet_12_0 ≤ 0nondet_12_0nondet_12_0 ≤ 0lt_483_post + lt_483_post ≤ 0lt_483_postlt_483_post ≤ 0lt_483_0 + lt_483_0 ≤ 0lt_483_0lt_483_0 ≤ 0lt_386_post + lt_386_post ≤ 0lt_386_postlt_386_post ≤ 0lt_386_0 + lt_386_0 ≤ 0lt_386_0lt_386_0 ≤ 0lt_29_post + lt_29_post ≤ 0lt_29_postlt_29_post ≤ 0lt_29_1 + lt_29_1 ≤ 0lt_29_1lt_29_1 ≤ 0lt_29_0 + lt_29_0 ≤ 0lt_29_0lt_29_0 ≤ 0lt_17_post + lt_17_post ≤ 0lt_17_postlt_17_post ≤ 0lt_17_0 + lt_17_0 ≤ 0lt_17_0lt_17_0 ≤ 0length_32_post + length_32_post ≤ 0length_32_postlength_32_post ≤ 0length_32_0 + length_32_0 ≤ 0length_32_0length_32_0 ≤ 0len_286_post + len_286_post ≤ 0len_286_postlen_286_post ≤ 0len_286_0 + len_286_0 ≤ 0len_286_0len_286_0 ≤ 0len_266_post + len_266_post ≤ 0len_266_postlen_266_post ≤ 0len_266_0 + len_266_0 ≤ 0len_266_0len_266_0 ≤ 0len_195_post + len_195_post ≤ 0len_195_postlen_195_post ≤ 0len_195_0 + len_195_0 ≤ 0len_195_0len_195_0 ≤ 0i_33_post + i_33_post ≤ 0i_33_posti_33_post ≤ 0i_33_0 + i_33_0 ≤ 0i_33_0i_33_0 ≤ 0i_227_post + i_227_post ≤ 0i_227_posti_227_post ≤ 0i_227_0 + i_227_0 ≤ 0i_227_0i_227_0 ≤ 0i_120_post + i_120_post ≤ 0i_120_posti_120_post ≤ 0i_120_0 + i_120_0 ≤ 0i_120_0i_120_0 ≤ 0i_111_post + i_111_post ≤ 0i_111_posti_111_post ≤ 0i_111_0 + i_111_0 ≤ 0i_111_0i_111_0 ≤ 0head_35_post + head_35_post ≤ 0head_35_posthead_35_post ≤ 0head_35_0 + head_35_0 ≤ 0head_35_0head_35_0 ≤ 0head_13_post + head_13_post ≤ 0head_13_posthead_13_post ≤ 0head_13_0 + head_13_0 ≤ 0head_13_0head_13_0 ≤ 0ct_20_post + ct_20_post ≤ 0ct_20_postct_20_post ≤ 0ct_20_2 + ct_20_2 ≤ 0ct_20_2ct_20_2 ≤ 0ct_20_1 + ct_20_1 ≤ 0ct_20_1ct_20_1 ≤ 0ct_20_0 + ct_20_0 ≤ 0ct_20_0ct_20_0 ≤ 0a_377_post + a_377_post ≤ 0a_377_posta_377_post ≤ 0a_377_0 + a_377_0 ≤ 0a_377_0a_377_0 ≤ 0a_347_post + a_347_post ≤ 0a_347_posta_347_post ≤ 0a_347_0 + a_347_0 ≤ 0a_347_0a_347_0 ≤ 0a_321_post + a_321_post ≤ 0a_321_posta_321_post ≤ 0a_321_0 + a_321_0 ≤ 0a_321_0a_321_0 ≤ 0a_27_post + a_27_post ≤ 0a_27_posta_27_post ≤ 0a_27_1 + a_27_1 ≤ 0a_27_1a_27_1 ≤ 0a_27_0 + a_27_0 ≤ 0a_27_0a_27_0 ≤ 0a_267_post + a_267_post ≤ 0a_267_posta_267_post ≤ 0a_267_0 + a_267_0 ≤ 0a_267_0a_267_0 ≤ 0a_210_post + a_210_post ≤ 0a_210_posta_210_post ≤ 0a_210_0 + a_210_0 ≤ 0a_210_0a_210_0 ≤ 0a_166_post + a_166_post ≤ 0a_166_posta_166_post ≤ 0a_166_0 + a_166_0 ≤ 0a_166_0a_166_0 ≤ 0

8 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

43 88 43_var_snapshot: z_389_post + z_389_post ≤ 0z_389_postz_389_post ≤ 0z_389_0 + z_389_0 ≤ 0z_389_0z_389_0 ≤ 0z_28_post + z_28_post ≤ 0z_28_postz_28_post ≤ 0z_28_1 + z_28_1 ≤ 0z_28_1z_28_1 ≤ 0z_28_0 + z_28_0 ≤ 0z_28_0z_28_0 ≤ 0z_279_post + z_279_post ≤ 0z_279_postz_279_post ≤ 0z_279_0 + z_279_0 ≤ 0z_279_0z_279_0 ≤ 0z_265_post + z_265_post ≤ 0z_265_postz_265_post ≤ 0z_265_0 + z_265_0 ≤ 0z_265_0z_265_0 ≤ 0z_252_post + z_252_post ≤ 0z_252_postz_252_post ≤ 0z_252_0 + z_252_0 ≤ 0z_252_0z_252_0 ≤ 0z_238_post + z_238_post ≤ 0z_238_postz_238_post ≤ 0z_238_0 + z_238_0 ≤ 0z_238_0z_238_0 ≤ 0z_229_post + z_229_post ≤ 0z_229_postz_229_post ≤ 0z_229_0 + z_229_0 ≤ 0z_229_0z_229_0 ≤ 0z_188_post + z_188_post ≤ 0z_188_postz_188_post ≤ 0z_188_0 + z_188_0 ≤ 0z_188_0z_188_0 ≤ 0z_160_post + z_160_post ≤ 0z_160_postz_160_post ≤ 0z_160_0 + z_160_0 ≤ 0z_160_0z_160_0 ≤ 0y_22_post + y_22_post ≤ 0y_22_posty_22_post ≤ 0y_22_2 + y_22_2 ≤ 0y_22_2y_22_2 ≤ 0y_22_1 + y_22_1 ≤ 0y_22_1y_22_1 ≤ 0y_22_0 + y_22_0 ≤ 0y_22_0y_22_0 ≤ 0x_SLAM_f_21_post + x_SLAM_f_21_post ≤ 0x_SLAM_f_21_postx_SLAM_f_21_post ≤ 0x_SLAM_f_21_2 + x_SLAM_f_21_2 ≤ 0x_SLAM_f_21_2x_SLAM_f_21_2 ≤ 0x_SLAM_f_21_1 + x_SLAM_f_21_1 ≤ 0x_SLAM_f_21_1x_SLAM_f_21_1 ≤ 0x_SLAM_f_21_0 + x_SLAM_f_21_0 ≤ 0x_SLAM_f_21_0x_SLAM_f_21_0 ≤ 0x_23_post + x_23_post ≤ 0x_23_postx_23_post ≤ 0x_23_2 + x_23_2 ≤ 0x_23_2x_23_2 ≤ 0x_23_1 + x_23_1 ≤ 0x_23_1x_23_1 ≤ 0x_23_0 + x_23_0 ≤ 0x_23_0x_23_0 ≤ 0x_19_post + x_19_post ≤ 0x_19_postx_19_post ≤ 0x_19_1 + x_19_1 ≤ 0x_19_1x_19_1 ≤ 0x_19_0 + x_19_0 ≤ 0x_19_0x_19_0 ≤ 0tmp_37_post + tmp_37_post ≤ 0tmp_37_posttmp_37_post ≤ 0tmp_37_0 + tmp_37_0 ≤ 0tmp_37_0tmp_37_0 ≤ 0temp_38_post + temp_38_post ≤ 0temp_38_posttemp_38_post ≤ 0temp_38_0 + temp_38_0 ≤ 0temp_38_0temp_38_0 ≤ 0temp1_30_post + temp1_30_post ≤ 0temp1_30_posttemp1_30_post ≤ 0temp1_30_0 + temp1_30_0 ≤ 0temp1_30_0temp1_30_0 ≤ 0temp0_34_post + temp0_34_post ≤ 0temp0_34_posttemp0_34_post ≤ 0temp0_34_1 + temp0_34_1 ≤ 0temp0_34_1temp0_34_1 ≤ 0temp0_34_0 + temp0_34_0 ≤ 0temp0_34_0temp0_34_0 ≤ 0temp0_18_0 + temp0_18_0 ≤ 0temp0_18_0temp0_18_0 ≤ 0t_24_post + t_24_post ≤ 0t_24_postt_24_post ≤ 0t_24_1 + t_24_1 ≤ 0t_24_1t_24_1 ≤ 0t_24_0 + t_24_0 ≤ 0t_24_0t_24_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_post + result_dot_nondet_sdv_special_RETURN_VALUE_14_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_postresult_dot_nondet_sdv_special_RETURN_VALUE_14_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_2 + result_dot_nondet_sdv_special_RETURN_VALUE_14_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_2result_dot_nondet_sdv_special_RETURN_VALUE_14_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_1result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_0 + result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_0result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_postresult_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_36_0 ≤ 0result_11_post + result_11_post ≤ 0result_11_postresult_11_post ≤ 0result_11_2 + result_11_2 ≤ 0result_11_2result_11_2 ≤ 0result_11_1 + result_11_1 ≤ 0result_11_1result_11_1 ≤ 0result_11_0 + result_11_0 ≤ 0result_11_0result_11_0 ≤ 0rcd_70_post + rcd_70_post ≤ 0rcd_70_postrcd_70_post ≤ 0rcd_70_0 + rcd_70_0 ≤ 0rcd_70_0rcd_70_0 ≤ 0rcd_46_post + rcd_46_post ≤ 0rcd_46_postrcd_46_post ≤ 0rcd_46_0 + rcd_46_0 ≤ 0rcd_46_0rcd_46_0 ≤ 0rcd_396_post + rcd_396_post ≤ 0rcd_396_postrcd_396_post ≤ 0rcd_396_0 + rcd_396_0 ≤ 0rcd_396_0rcd_396_0 ≤ 0rcd_376_post + rcd_376_post ≤ 0rcd_376_postrcd_376_post ≤ 0rcd_376_0 + rcd_376_0 ≤ 0rcd_376_0rcd_376_0 ≤ 0rcd_356_post + rcd_356_post ≤ 0rcd_356_postrcd_356_post ≤ 0rcd_356_0 + rcd_356_0 ≤ 0rcd_356_0rcd_356_0 ≤ 0rcd_352_post + rcd_352_post ≤ 0rcd_352_postrcd_352_post ≤ 0rcd_352_0 + rcd_352_0 ≤ 0rcd_352_0rcd_352_0 ≤ 0rcd_264_post + rcd_264_post ≤ 0rcd_264_postrcd_264_post ≤ 0rcd_264_0 + rcd_264_0 ≤ 0rcd_264_0rcd_264_0 ≤ 0rcd_237_post + rcd_237_post ≤ 0rcd_237_postrcd_237_post ≤ 0rcd_237_0 + rcd_237_0 ≤ 0rcd_237_0rcd_237_0 ≤ 0rcd_228_post + rcd_228_post ≤ 0rcd_228_postrcd_228_post ≤ 0rcd_228_0 + rcd_228_0 ≤ 0rcd_228_0rcd_228_0 ≤ 0rcd_226_post + rcd_226_post ≤ 0rcd_226_postrcd_226_post ≤ 0rcd_226_0 + rcd_226_0 ≤ 0rcd_226_0rcd_226_0 ≤ 0rcd_222_post + rcd_222_post ≤ 0rcd_222_postrcd_222_post ≤ 0rcd_222_0 + rcd_222_0 ≤ 0rcd_222_0rcd_222_0 ≤ 0rcd_113_post + rcd_113_post ≤ 0rcd_113_postrcd_113_post ≤ 0rcd_113_0 + rcd_113_0 ≤ 0rcd_113_0rcd_113_0 ≤ 0rcd_105_post + rcd_105_post ≤ 0rcd_105_postrcd_105_post ≤ 0rcd_105_0 + rcd_105_0 ≤ 0rcd_105_0rcd_105_0 ≤ 0r_42_post + r_42_post ≤ 0r_42_postr_42_post ≤ 0r_42_0 + r_42_0 ≤ 0r_42_0r_42_0 ≤ 0r_236_post + r_236_post ≤ 0r_236_postr_236_post ≤ 0r_236_0 + r_236_0 ≤ 0r_236_0r_236_0 ≤ 0r_178_post + r_178_post ≤ 0r_178_postr_178_post ≤ 0r_178_0 + r_178_0 ≤ 0r_178_0r_178_0 ≤ 0nondet_12_post + nondet_12_post ≤ 0nondet_12_postnondet_12_post ≤ 0nondet_12_1 + nondet_12_1 ≤ 0nondet_12_1nondet_12_1 ≤ 0nondet_12_0 + nondet_12_0 ≤ 0nondet_12_0nondet_12_0 ≤ 0lt_483_post + lt_483_post ≤ 0lt_483_postlt_483_post ≤ 0lt_483_0 + lt_483_0 ≤ 0lt_483_0lt_483_0 ≤ 0lt_386_post + lt_386_post ≤ 0lt_386_postlt_386_post ≤ 0lt_386_0 + lt_386_0 ≤ 0lt_386_0lt_386_0 ≤ 0lt_29_post + lt_29_post ≤ 0lt_29_postlt_29_post ≤ 0lt_29_1 + lt_29_1 ≤ 0lt_29_1lt_29_1 ≤ 0lt_29_0 + lt_29_0 ≤ 0lt_29_0lt_29_0 ≤ 0lt_17_post + lt_17_post ≤ 0lt_17_postlt_17_post ≤ 0lt_17_0 + lt_17_0 ≤ 0lt_17_0lt_17_0 ≤ 0length_32_post + length_32_post ≤ 0length_32_postlength_32_post ≤ 0length_32_0 + length_32_0 ≤ 0length_32_0length_32_0 ≤ 0len_286_post + len_286_post ≤ 0len_286_postlen_286_post ≤ 0len_286_0 + len_286_0 ≤ 0len_286_0len_286_0 ≤ 0len_266_post + len_266_post ≤ 0len_266_postlen_266_post ≤ 0len_266_0 + len_266_0 ≤ 0len_266_0len_266_0 ≤ 0len_195_post + len_195_post ≤ 0len_195_postlen_195_post ≤ 0len_195_0 + len_195_0 ≤ 0len_195_0len_195_0 ≤ 0i_33_post + i_33_post ≤ 0i_33_posti_33_post ≤ 0i_33_0 + i_33_0 ≤ 0i_33_0i_33_0 ≤ 0i_227_post + i_227_post ≤ 0i_227_posti_227_post ≤ 0i_227_0 + i_227_0 ≤ 0i_227_0i_227_0 ≤ 0i_120_post + i_120_post ≤ 0i_120_posti_120_post ≤ 0i_120_0 + i_120_0 ≤ 0i_120_0i_120_0 ≤ 0i_111_post + i_111_post ≤ 0i_111_posti_111_post ≤ 0i_111_0 + i_111_0 ≤ 0i_111_0i_111_0 ≤ 0head_35_post + head_35_post ≤ 0head_35_posthead_35_post ≤ 0head_35_0 + head_35_0 ≤ 0head_35_0head_35_0 ≤ 0head_13_post + head_13_post ≤ 0head_13_posthead_13_post ≤ 0head_13_0 + head_13_0 ≤ 0head_13_0head_13_0 ≤ 0ct_20_post + ct_20_post ≤ 0ct_20_postct_20_post ≤ 0ct_20_2 + ct_20_2 ≤ 0ct_20_2ct_20_2 ≤ 0ct_20_1 + ct_20_1 ≤ 0ct_20_1ct_20_1 ≤ 0ct_20_0 + ct_20_0 ≤ 0ct_20_0ct_20_0 ≤ 0a_377_post + a_377_post ≤ 0a_377_posta_377_post ≤ 0a_377_0 + a_377_0 ≤ 0a_377_0a_377_0 ≤ 0a_347_post + a_347_post ≤ 0a_347_posta_347_post ≤ 0a_347_0 + a_347_0 ≤ 0a_347_0a_347_0 ≤ 0a_321_post + a_321_post ≤ 0a_321_posta_321_post ≤ 0a_321_0 + a_321_0 ≤ 0a_321_0a_321_0 ≤ 0a_27_post + a_27_post ≤ 0a_27_posta_27_post ≤ 0a_27_1 + a_27_1 ≤ 0a_27_1a_27_1 ≤ 0a_27_0 + a_27_0 ≤ 0a_27_0a_27_0 ≤ 0a_267_post + a_267_post ≤ 0a_267_posta_267_post ≤ 0a_267_0 + a_267_0 ≤ 0a_267_0a_267_0 ≤ 0a_210_post + a_210_post ≤ 0a_210_posta_210_post ≤ 0a_210_0 + a_210_0 ≤ 0a_210_0a_210_0 ≤ 0a_166_post + a_166_post ≤ 0a_166_posta_166_post ≤ 0a_166_0 + a_166_0 ≤ 0a_166_0a_166_0 ≤ 0

9 SCC Decomposition

We consider subproblems for each of the 3 SCC(s) of the program graph.

9.1 SCC Subproblem 1/3

Here we consider the SCC { 0, 2, 3, 4, 5, 6, 7, 8, 0_var_snapshot, 0* }.

9.1.1 Transition Removal

We remove transition 1 using the following ranking functions, which are bounded by −4.

0: −2 + 10⋅a_347_0
2: −4 + 10⋅a_347_0
3: −5 + 10⋅a_347_0
4: 4 + 10⋅a_377_0
5: 3 + 10⋅a_377_0
6: 2 + 10⋅a_377_0
7: 1 + 10⋅a_377_0
8: 10⋅a_347_0
0_var_snapshot: −3 + 10⋅a_347_0
0*: −1 + 10⋅a_347_0

9.1.2 Transition Removal

We remove transitions 74, 76, 2, 3, 4, 5, 6, 7, 8 using the following ranking functions, which are bounded by −3.

0: −2
2: 6
3: 5
4: 4
5: 3
6: 2
7: 1
8: 0
0_var_snapshot: −3
0*: −1

9.1.3 Splitting Cut-Point Transitions

We consider 1 subproblems corresponding to sets of cut-point transitions as follows.

9.1.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 73.

9.1.3.1.1 Splitting Cut-Point Transitions

There remain no cut-point transition to consider. Hence the cooperation termination is trivial.

9.2 SCC Subproblem 2/3

Here we consider the SCC { 43, 48, 49, 50, 51, 52, 43_var_snapshot, 43* }.

9.2.1 Transition Removal

We remove transition 52 using the following ranking functions, which are bounded by −4.

43: −2 + 8⋅a_210_0
48: −4 + 8⋅a_210_0
49: −5 + 8⋅a_210_0
50: 2 + 8⋅a_267_0
51: 1 + 8⋅a_267_0
52: 8⋅a_210_0
43_var_snapshot: −3 + 8⋅a_210_0
43*: −1 + 8⋅a_210_0

9.2.2 Transition Removal

We remove transitions 88, 90, 53, 54, 55, 56, 57 using the following ranking functions, which are bounded by −3.

43: −2
48: 4
49: 3
50: 2
51: 1
52: 0
43_var_snapshot: −3
43*: −1

9.2.3 Splitting Cut-Point Transitions

We consider 1 subproblems corresponding to sets of cut-point transitions as follows.

9.2.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 87.

9.2.3.1.1 Splitting Cut-Point Transitions

There remain no cut-point transition to consider. Hence the cooperation termination is trivial.

9.3 SCC Subproblem 3/3

Here we consider the SCC { 38, 44, 38_var_snapshot, 38* }.

9.3.1 Transition Removal

We remove transition 45 using the following ranking functions, which are bounded by 1.

38: −1 − 3⋅i_33_0 + 3⋅length_32_0
44: 1 − 3⋅i_33_0 + 3⋅length_32_0
38_var_snapshot: −1 − 3⋅i_33_0 + 3⋅length_32_0
38*: −3⋅i_33_0 + 3⋅length_32_0

9.3.2 Transition Removal

We remove transitions 81, 46 using the following ranking functions, which are bounded by −3.

38: −2
44: 0
38_var_snapshot: −3
38*: −1

9.3.3 Transition Removal

We remove transition 83 using the following ranking functions, which are bounded by 0.

38: 0
44: 0
38_var_snapshot: 0
38*: 1

9.3.4 Splitting Cut-Point Transitions

We consider 1 subproblems corresponding to sets of cut-point transitions as follows.

9.3.4.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 80.

9.3.4.1.1 Splitting Cut-Point Transitions

There remain no cut-point transition to consider. Hence the cooperation termination is trivial.

Tool configuration

T2Cert