LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Invariant Updates

The following invariants are asserted.

0: 2 − length_14_0 ≤ 0
1: len_200_0 ≤ 0a_215_0 ≤ 0
2: len_200_0 ≤ 0a_215_0 ≤ 0
3: len_200_0 ≤ 0a_215_0 ≤ 0
4: TRUE
5: len_200_0 ≤ 0a_215_0 ≤ 0
6: len_200_0 ≤ 0a_215_0 ≤ 0
7: len_200_0 ≤ 0a_215_0 ≤ 01 − len_270_post ≤ 01 − len_270_0 ≤ 0
8: len_200_0 ≤ 0a_215_0 ≤ 01 − len_270_post ≤ 01 − len_270_0 ≤ 0
9: len_200_0 ≤ 0a_215_0 ≤ 01 − len_270_post ≤ 01 − len_270_0 ≤ 0
10: len_200_0 ≤ 0a_215_0 ≤ 01 − len_270_post ≤ 01 − len_270_0 ≤ 0
11: len_200_0 ≤ 0a_215_0 ≤ 01 − len_270_post ≤ 01 − len_270_0 ≤ 0
12: 2 − length_14_0 ≤ 01 − len_270_post ≤ 01 − len_270_0 ≤ 0
33: TRUE
34: i_27_post ≤ 0i_27_post ≤ 0i_27_0 ≤ 0i_27_0 ≤ 0
35: −1 + i_27_post ≤ 01 − i_27_post ≤ 0−1 + i_27_0 ≤ 01 − i_27_0 ≤ 01 − length_25_0 ≤ 0
36: −1 + length_14_0 ≤ 01 − length_14_0 ≤ 0−1 + length_14_post ≤ 01 − length_14_post ≤ 0
37: 2 − length_25_0 ≤ 0
38: 2 − length_14_0 ≤ 02 − length_14_post ≤ 0
39: i_114_0 ≤ 0
40: i_114_0 ≤ 0
41: i_114_0 ≤ 0len_200_0 ≤ 0len_200_0 ≤ 0
42: i_114_0 ≤ 0len_200_0 ≤ 0len_200_0 ≤ 0
43: i_114_0 ≤ 0len_200_0 ≤ 0len_200_0 ≤ 0
44: TRUE
45: TRUE
46: −1 + length_14_0 ≤ 01 − length_14_0 ≤ 0
47: −1 + length_14_0 ≤ 01 − length_14_0 ≤ 0
48: −1 + length_14_0 ≤ 01 − length_14_0 ≤ 0
49: 2 − length_25_0 ≤ 0
50: TRUE

The invariants are proved as follows.

IMPACT Invariant Proof

2 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
0 58 0: z_19_post + z_19_post ≤ 0z_19_postz_19_post ≤ 0z_19_1 + z_19_1 ≤ 0z_19_1z_19_1 ≤ 0z_19_0 + z_19_0 ≤ 0z_19_0z_19_0 ≤ 0y_347_post + y_347_post ≤ 0y_347_posty_347_post ≤ 0y_347_0 + y_347_0 ≤ 0y_347_0y_347_0 ≤ 0y_295_post + y_295_post ≤ 0y_295_posty_295_post ≤ 0y_295_0 + y_295_0 ≤ 0y_295_0y_295_0 ≤ 0y_290_post + y_290_post ≤ 0y_290_posty_290_post ≤ 0y_290_0 + y_290_0 ≤ 0y_290_0y_290_0 ≤ 0y_285_post + y_285_post ≤ 0y_285_posty_285_post ≤ 0y_285_0 + y_285_0 ≤ 0y_285_0y_285_0 ≤ 0y_269_post + y_269_post ≤ 0y_269_posty_269_post ≤ 0y_269_0 + y_269_0 ≤ 0y_269_0y_269_0 ≤ 0y_261_post + y_261_post ≤ 0y_261_posty_261_post ≤ 0y_261_0 + y_261_0 ≤ 0y_261_0y_261_0 ≤ 0y_241_post + y_241_post ≤ 0y_241_posty_241_post ≤ 0y_241_0 + y_241_0 ≤ 0y_241_0y_241_0 ≤ 0y_231_post + y_231_post ≤ 0y_231_posty_231_post ≤ 0y_231_0 + y_231_0 ≤ 0y_231_0y_231_0 ≤ 0y_22_post + y_22_post ≤ 0y_22_posty_22_post ≤ 0y_22_1 + y_22_1 ≤ 0y_22_1y_22_1 ≤ 0y_22_0 + y_22_0 ≤ 0y_22_0y_22_0 ≤ 0y_191_post + y_191_post ≤ 0y_191_posty_191_post ≤ 0y_191_0 + y_191_0 ≤ 0y_191_0y_191_0 ≤ 0y_162_post + y_162_post ≤ 0y_162_posty_162_post ≤ 0y_162_0 + y_162_0 ≤ 0y_162_0y_162_0 ≤ 0x_21_post + x_21_post ≤ 0x_21_postx_21_post ≤ 0x_21_1 + x_21_1 ≤ 0x_21_1x_21_1 ≤ 0x_21_0 + x_21_0 ≤ 0x_21_0x_21_0 ≤ 0w_20_post + w_20_post ≤ 0w_20_postw_20_post ≤ 0w_20_1 + w_20_1 ≤ 0w_20_1w_20_1 ≤ 0w_20_0 + w_20_0 ≤ 0w_20_0w_20_0 ≤ 0tmp_31_post + tmp_31_post ≤ 0tmp_31_posttmp_31_post ≤ 0tmp_31_0 + tmp_31_0 ≤ 0tmp_31_0tmp_31_0 ≤ 0temp_32_post + temp_32_post ≤ 0temp_32_posttemp_32_post ≤ 0temp_32_0 + temp_32_0 ≤ 0temp_32_0temp_32_0 ≤ 0temp0_28_post + temp0_28_post ≤ 0temp0_28_posttemp0_28_post ≤ 0temp0_28_1 + temp0_28_1 ≤ 0temp0_28_1temp0_28_1 ≤ 0temp0_28_0 + temp0_28_0 ≤ 0temp0_28_0temp0_28_0 ≤ 0temp0_18_0 + temp0_18_0 ≤ 0temp0_18_0temp0_18_0 ≤ 0tail_15_post + tail_15_post ≤ 0tail_15_posttail_15_post ≤ 0tail_15_0 + tail_15_0 ≤ 0tail_15_0tail_15_0 ≤ 0t_23_post + t_23_post ≤ 0t_23_postt_23_post ≤ 0t_23_0 + t_23_0 ≤ 0t_23_0t_23_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_postresult_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_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_99_post + rcd_99_post ≤ 0rcd_99_postrcd_99_post ≤ 0rcd_99_0 + rcd_99_0 ≤ 0rcd_99_0rcd_99_0 ≤ 0rcd_64_post + rcd_64_post ≤ 0rcd_64_postrcd_64_post ≤ 0rcd_64_0 + rcd_64_0 ≤ 0rcd_64_0rcd_64_0 ≤ 0rcd_40_post + rcd_40_post ≤ 0rcd_40_postrcd_40_post ≤ 0rcd_40_0 + rcd_40_0 ≤ 0rcd_40_0rcd_40_0 ≤ 0rcd_268_post + rcd_268_post ≤ 0rcd_268_postrcd_268_post ≤ 0rcd_268_0 + rcd_268_0 ≤ 0rcd_268_0rcd_268_0 ≤ 0rcd_248_post + rcd_248_post ≤ 0rcd_248_postrcd_248_post ≤ 0rcd_248_0 + rcd_248_0 ≤ 0rcd_248_0rcd_248_0 ≤ 0rcd_243_post + rcd_243_post ≤ 0rcd_243_postrcd_243_post ≤ 0rcd_243_0 + rcd_243_0 ≤ 0rcd_243_0rcd_243_0 ≤ 0rcd_239_post + rcd_239_post ≤ 0rcd_239_postrcd_239_post ≤ 0rcd_239_0 + rcd_239_0 ≤ 0rcd_239_0rcd_239_0 ≤ 0rcd_230_post + rcd_230_post ≤ 0rcd_230_postrcd_230_post ≤ 0rcd_230_0 + rcd_230_0 ≤ 0rcd_230_0rcd_230_0 ≤ 0rcd_107_post + rcd_107_post ≤ 0rcd_107_postrcd_107_post ≤ 0rcd_107_0 + rcd_107_0 ≤ 0rcd_107_0rcd_107_0 ≤ 0r_36_post + r_36_post ≤ 0r_36_postr_36_post ≤ 0r_36_0 + r_36_0 ≤ 0r_36_0r_36_0 ≤ 0r_267_post + r_267_post ≤ 0r_267_postr_267_post ≤ 0r_267_0 + r_267_0 ≤ 0r_267_0r_267_0 ≤ 0r_253_post + r_253_post ≤ 0r_253_postr_253_post ≤ 0r_253_0 + r_253_0 ≤ 0r_253_0r_253_0 ≤ 0r_247_post + r_247_post ≤ 0r_247_postr_247_post ≤ 0r_247_0 + r_247_0 ≤ 0r_247_0r_247_0 ≤ 0r_242_post + r_242_post ≤ 0r_242_postr_242_post ≤ 0r_242_0 + r_242_0 ≤ 0r_242_0r_242_0 ≤ 0r_240_post + r_240_post ≤ 0r_240_postr_240_post ≤ 0r_240_0 + r_240_0 ≤ 0r_240_0r_240_0 ≤ 0r_238_post + r_238_post ≤ 0r_238_postr_238_post ≤ 0r_238_0 + r_238_0 ≤ 0r_238_0r_238_0 ≤ 0r_229_post + r_229_post ≤ 0r_229_postr_229_post ≤ 0r_229_0 + r_229_0 ≤ 0r_229_0r_229_0 ≤ 0r_183_post + r_183_post ≤ 0r_183_postr_183_post ≤ 0r_183_0 + r_183_0 ≤ 0r_183_0r_183_0 ≤ 0r_154_post + r_154_post ≤ 0r_154_postr_154_post ≤ 0r_154_0 + r_154_0 ≤ 0r_154_0r_154_0 ≤ 0length_25_post + length_25_post ≤ 0length_25_postlength_25_post ≤ 0length_25_0 + length_25_0 ≤ 0length_25_0length_25_0 ≤ 0length_14_post + length_14_post ≤ 0length_14_postlength_14_post ≤ 0length_14_1 + length_14_1 ≤ 0length_14_1length_14_1 ≤ 0length_14_0 + length_14_0 ≤ 0length_14_0length_14_0 ≤ 0len_270_post + len_270_post ≤ 0len_270_postlen_270_post ≤ 0len_270_0 + len_270_0 ≤ 0len_270_0len_270_0 ≤ 0len_200_post + len_200_post ≤ 0len_200_postlen_200_post ≤ 0len_200_0 + len_200_0 ≤ 0len_200_0len_200_0 ≤ 0i_27_post + i_27_post ≤ 0i_27_posti_27_post ≤ 0i_27_0 + i_27_0 ≤ 0i_27_0i_27_0 ≤ 0i_114_post + i_114_post ≤ 0i_114_posti_114_post ≤ 0i_114_0 + i_114_0 ≤ 0i_114_0i_114_0 ≤ 0i_105_post + i_105_post ≤ 0i_105_posti_105_post ≤ 0i_105_0 + i_105_0 ≤ 0i_105_0i_105_0 ≤ 0head_SLAM_f_26_post + head_SLAM_f_26_post ≤ 0head_SLAM_f_26_posthead_SLAM_f_26_post ≤ 0head_SLAM_f_26_0 + head_SLAM_f_26_0 ≤ 0head_SLAM_f_26_0head_SLAM_f_26_0 ≤ 0head_29_post + head_29_post ≤ 0head_29_posthead_29_post ≤ 0head_29_0 + head_29_0 ≤ 0head_29_0head_29_0 ≤ 0head_13_post + head_13_post ≤ 0head_13_posthead_13_post ≤ 0head_13_0 + head_13_0 ≤ 0head_13_0head_13_0 ≤ 0a_271_post + a_271_post ≤ 0a_271_posta_271_post ≤ 0a_271_0 + a_271_0 ≤ 0a_271_0a_271_0 ≤ 0a_215_post + a_215_post ≤ 0a_215_posta_215_post ≤ 0a_215_0 + a_215_0 ≤ 0a_215_0a_215_0 ≤ 0a_168_post + a_168_post ≤ 0a_168_posta_168_post ≤ 0a_168_0 + a_168_0 ≤ 0a_168_0a_168_0 ≤ 0a_143_post + a_143_post ≤ 0a_143_posta_143_post ≤ 0a_143_0 + a_143_0 ≤ 0a_143_0a_143_0 ≤ 0
37 65 37: z_19_post + z_19_post ≤ 0z_19_postz_19_post ≤ 0z_19_1 + z_19_1 ≤ 0z_19_1z_19_1 ≤ 0z_19_0 + z_19_0 ≤ 0z_19_0z_19_0 ≤ 0y_347_post + y_347_post ≤ 0y_347_posty_347_post ≤ 0y_347_0 + y_347_0 ≤ 0y_347_0y_347_0 ≤ 0y_295_post + y_295_post ≤ 0y_295_posty_295_post ≤ 0y_295_0 + y_295_0 ≤ 0y_295_0y_295_0 ≤ 0y_290_post + y_290_post ≤ 0y_290_posty_290_post ≤ 0y_290_0 + y_290_0 ≤ 0y_290_0y_290_0 ≤ 0y_285_post + y_285_post ≤ 0y_285_posty_285_post ≤ 0y_285_0 + y_285_0 ≤ 0y_285_0y_285_0 ≤ 0y_269_post + y_269_post ≤ 0y_269_posty_269_post ≤ 0y_269_0 + y_269_0 ≤ 0y_269_0y_269_0 ≤ 0y_261_post + y_261_post ≤ 0y_261_posty_261_post ≤ 0y_261_0 + y_261_0 ≤ 0y_261_0y_261_0 ≤ 0y_241_post + y_241_post ≤ 0y_241_posty_241_post ≤ 0y_241_0 + y_241_0 ≤ 0y_241_0y_241_0 ≤ 0y_231_post + y_231_post ≤ 0y_231_posty_231_post ≤ 0y_231_0 + y_231_0 ≤ 0y_231_0y_231_0 ≤ 0y_22_post + y_22_post ≤ 0y_22_posty_22_post ≤ 0y_22_1 + y_22_1 ≤ 0y_22_1y_22_1 ≤ 0y_22_0 + y_22_0 ≤ 0y_22_0y_22_0 ≤ 0y_191_post + y_191_post ≤ 0y_191_posty_191_post ≤ 0y_191_0 + y_191_0 ≤ 0y_191_0y_191_0 ≤ 0y_162_post + y_162_post ≤ 0y_162_posty_162_post ≤ 0y_162_0 + y_162_0 ≤ 0y_162_0y_162_0 ≤ 0x_21_post + x_21_post ≤ 0x_21_postx_21_post ≤ 0x_21_1 + x_21_1 ≤ 0x_21_1x_21_1 ≤ 0x_21_0 + x_21_0 ≤ 0x_21_0x_21_0 ≤ 0w_20_post + w_20_post ≤ 0w_20_postw_20_post ≤ 0w_20_1 + w_20_1 ≤ 0w_20_1w_20_1 ≤ 0w_20_0 + w_20_0 ≤ 0w_20_0w_20_0 ≤ 0tmp_31_post + tmp_31_post ≤ 0tmp_31_posttmp_31_post ≤ 0tmp_31_0 + tmp_31_0 ≤ 0tmp_31_0tmp_31_0 ≤ 0temp_32_post + temp_32_post ≤ 0temp_32_posttemp_32_post ≤ 0temp_32_0 + temp_32_0 ≤ 0temp_32_0temp_32_0 ≤ 0temp0_28_post + temp0_28_post ≤ 0temp0_28_posttemp0_28_post ≤ 0temp0_28_1 + temp0_28_1 ≤ 0temp0_28_1temp0_28_1 ≤ 0temp0_28_0 + temp0_28_0 ≤ 0temp0_28_0temp0_28_0 ≤ 0temp0_18_0 + temp0_18_0 ≤ 0temp0_18_0temp0_18_0 ≤ 0tail_15_post + tail_15_post ≤ 0tail_15_posttail_15_post ≤ 0tail_15_0 + tail_15_0 ≤ 0tail_15_0tail_15_0 ≤ 0t_23_post + t_23_post ≤ 0t_23_postt_23_post ≤ 0t_23_0 + t_23_0 ≤ 0t_23_0t_23_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_postresult_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_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_99_post + rcd_99_post ≤ 0rcd_99_postrcd_99_post ≤ 0rcd_99_0 + rcd_99_0 ≤ 0rcd_99_0rcd_99_0 ≤ 0rcd_64_post + rcd_64_post ≤ 0rcd_64_postrcd_64_post ≤ 0rcd_64_0 + rcd_64_0 ≤ 0rcd_64_0rcd_64_0 ≤ 0rcd_40_post + rcd_40_post ≤ 0rcd_40_postrcd_40_post ≤ 0rcd_40_0 + rcd_40_0 ≤ 0rcd_40_0rcd_40_0 ≤ 0rcd_268_post + rcd_268_post ≤ 0rcd_268_postrcd_268_post ≤ 0rcd_268_0 + rcd_268_0 ≤ 0rcd_268_0rcd_268_0 ≤ 0rcd_248_post + rcd_248_post ≤ 0rcd_248_postrcd_248_post ≤ 0rcd_248_0 + rcd_248_0 ≤ 0rcd_248_0rcd_248_0 ≤ 0rcd_243_post + rcd_243_post ≤ 0rcd_243_postrcd_243_post ≤ 0rcd_243_0 + rcd_243_0 ≤ 0rcd_243_0rcd_243_0 ≤ 0rcd_239_post + rcd_239_post ≤ 0rcd_239_postrcd_239_post ≤ 0rcd_239_0 + rcd_239_0 ≤ 0rcd_239_0rcd_239_0 ≤ 0rcd_230_post + rcd_230_post ≤ 0rcd_230_postrcd_230_post ≤ 0rcd_230_0 + rcd_230_0 ≤ 0rcd_230_0rcd_230_0 ≤ 0rcd_107_post + rcd_107_post ≤ 0rcd_107_postrcd_107_post ≤ 0rcd_107_0 + rcd_107_0 ≤ 0rcd_107_0rcd_107_0 ≤ 0r_36_post + r_36_post ≤ 0r_36_postr_36_post ≤ 0r_36_0 + r_36_0 ≤ 0r_36_0r_36_0 ≤ 0r_267_post + r_267_post ≤ 0r_267_postr_267_post ≤ 0r_267_0 + r_267_0 ≤ 0r_267_0r_267_0 ≤ 0r_253_post + r_253_post ≤ 0r_253_postr_253_post ≤ 0r_253_0 + r_253_0 ≤ 0r_253_0r_253_0 ≤ 0r_247_post + r_247_post ≤ 0r_247_postr_247_post ≤ 0r_247_0 + r_247_0 ≤ 0r_247_0r_247_0 ≤ 0r_242_post + r_242_post ≤ 0r_242_postr_242_post ≤ 0r_242_0 + r_242_0 ≤ 0r_242_0r_242_0 ≤ 0r_240_post + r_240_post ≤ 0r_240_postr_240_post ≤ 0r_240_0 + r_240_0 ≤ 0r_240_0r_240_0 ≤ 0r_238_post + r_238_post ≤ 0r_238_postr_238_post ≤ 0r_238_0 + r_238_0 ≤ 0r_238_0r_238_0 ≤ 0r_229_post + r_229_post ≤ 0r_229_postr_229_post ≤ 0r_229_0 + r_229_0 ≤ 0r_229_0r_229_0 ≤ 0r_183_post + r_183_post ≤ 0r_183_postr_183_post ≤ 0r_183_0 + r_183_0 ≤ 0r_183_0r_183_0 ≤ 0r_154_post + r_154_post ≤ 0r_154_postr_154_post ≤ 0r_154_0 + r_154_0 ≤ 0r_154_0r_154_0 ≤ 0length_25_post + length_25_post ≤ 0length_25_postlength_25_post ≤ 0length_25_0 + length_25_0 ≤ 0length_25_0length_25_0 ≤ 0length_14_post + length_14_post ≤ 0length_14_postlength_14_post ≤ 0length_14_1 + length_14_1 ≤ 0length_14_1length_14_1 ≤ 0length_14_0 + length_14_0 ≤ 0length_14_0length_14_0 ≤ 0len_270_post + len_270_post ≤ 0len_270_postlen_270_post ≤ 0len_270_0 + len_270_0 ≤ 0len_270_0len_270_0 ≤ 0len_200_post + len_200_post ≤ 0len_200_postlen_200_post ≤ 0len_200_0 + len_200_0 ≤ 0len_200_0len_200_0 ≤ 0i_27_post + i_27_post ≤ 0i_27_posti_27_post ≤ 0i_27_0 + i_27_0 ≤ 0i_27_0i_27_0 ≤ 0i_114_post + i_114_post ≤ 0i_114_posti_114_post ≤ 0i_114_0 + i_114_0 ≤ 0i_114_0i_114_0 ≤ 0i_105_post + i_105_post ≤ 0i_105_posti_105_post ≤ 0i_105_0 + i_105_0 ≤ 0i_105_0i_105_0 ≤ 0head_SLAM_f_26_post + head_SLAM_f_26_post ≤ 0head_SLAM_f_26_posthead_SLAM_f_26_post ≤ 0head_SLAM_f_26_0 + head_SLAM_f_26_0 ≤ 0head_SLAM_f_26_0head_SLAM_f_26_0 ≤ 0head_29_post + head_29_post ≤ 0head_29_posthead_29_post ≤ 0head_29_0 + head_29_0 ≤ 0head_29_0head_29_0 ≤ 0head_13_post + head_13_post ≤ 0head_13_posthead_13_post ≤ 0head_13_0 + head_13_0 ≤ 0head_13_0head_13_0 ≤ 0a_271_post + a_271_post ≤ 0a_271_posta_271_post ≤ 0a_271_0 + a_271_0 ≤ 0a_271_0a_271_0 ≤ 0a_215_post + a_215_post ≤ 0a_215_posta_215_post ≤ 0a_215_0 + a_215_0 ≤ 0a_215_0a_215_0 ≤ 0a_168_post + a_168_post ≤ 0a_168_posta_168_post ≤ 0a_168_0 + a_168_0 ≤ 0a_168_0a_168_0 ≤ 0a_143_post + a_143_post ≤ 0a_143_posta_143_post ≤ 0a_143_0 + a_143_0 ≤ 0a_143_0a_143_0 ≤ 0
and for every transition t, a duplicate t is considered.

3 Transition Removal

We remove transitions 0, 1, 2, 3, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 54, 55, 56, 57 using the following ranking functions, which are bounded by −51.

50: 0
33: 0
34: 0
35: 0
36: 0
44: 0
45: 0
46: 0
47: 0
48: 0
37: 0
49: 0
38: 0
39: 0
40: 0
41: 0
42: 0
43: 0
0: 0
5: 0
6: 0
7: 0
8: 0
9: 0
10: 0
11: 0
12: 0
1: 0
2: 0
3: 0
4: 0
50: −23
33: −24
34: −25
35: −26
36: −27
44: −28
45: −29
46: −30
47: −31
48: −32
37: −33
49: −33
37_var_snapshot: −33
37*: −33
38: −36
39: −37
40: −38
41: −39
42: −40
43: −41
0: −42
5: −42
6: −42
7: −42
8: −42
9: −42
10: −42
11: −42
12: −42
0_var_snapshot: −42
0*: −42
1: −46
2: −47
3: −48
4: −49

4 Location Addition

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

0* 61 0: z_19_post + z_19_post ≤ 0z_19_postz_19_post ≤ 0z_19_1 + z_19_1 ≤ 0z_19_1z_19_1 ≤ 0z_19_0 + z_19_0 ≤ 0z_19_0z_19_0 ≤ 0y_347_post + y_347_post ≤ 0y_347_posty_347_post ≤ 0y_347_0 + y_347_0 ≤ 0y_347_0y_347_0 ≤ 0y_295_post + y_295_post ≤ 0y_295_posty_295_post ≤ 0y_295_0 + y_295_0 ≤ 0y_295_0y_295_0 ≤ 0y_290_post + y_290_post ≤ 0y_290_posty_290_post ≤ 0y_290_0 + y_290_0 ≤ 0y_290_0y_290_0 ≤ 0y_285_post + y_285_post ≤ 0y_285_posty_285_post ≤ 0y_285_0 + y_285_0 ≤ 0y_285_0y_285_0 ≤ 0y_269_post + y_269_post ≤ 0y_269_posty_269_post ≤ 0y_269_0 + y_269_0 ≤ 0y_269_0y_269_0 ≤ 0y_261_post + y_261_post ≤ 0y_261_posty_261_post ≤ 0y_261_0 + y_261_0 ≤ 0y_261_0y_261_0 ≤ 0y_241_post + y_241_post ≤ 0y_241_posty_241_post ≤ 0y_241_0 + y_241_0 ≤ 0y_241_0y_241_0 ≤ 0y_231_post + y_231_post ≤ 0y_231_posty_231_post ≤ 0y_231_0 + y_231_0 ≤ 0y_231_0y_231_0 ≤ 0y_22_post + y_22_post ≤ 0y_22_posty_22_post ≤ 0y_22_1 + y_22_1 ≤ 0y_22_1y_22_1 ≤ 0y_22_0 + y_22_0 ≤ 0y_22_0y_22_0 ≤ 0y_191_post + y_191_post ≤ 0y_191_posty_191_post ≤ 0y_191_0 + y_191_0 ≤ 0y_191_0y_191_0 ≤ 0y_162_post + y_162_post ≤ 0y_162_posty_162_post ≤ 0y_162_0 + y_162_0 ≤ 0y_162_0y_162_0 ≤ 0x_21_post + x_21_post ≤ 0x_21_postx_21_post ≤ 0x_21_1 + x_21_1 ≤ 0x_21_1x_21_1 ≤ 0x_21_0 + x_21_0 ≤ 0x_21_0x_21_0 ≤ 0w_20_post + w_20_post ≤ 0w_20_postw_20_post ≤ 0w_20_1 + w_20_1 ≤ 0w_20_1w_20_1 ≤ 0w_20_0 + w_20_0 ≤ 0w_20_0w_20_0 ≤ 0tmp_31_post + tmp_31_post ≤ 0tmp_31_posttmp_31_post ≤ 0tmp_31_0 + tmp_31_0 ≤ 0tmp_31_0tmp_31_0 ≤ 0temp_32_post + temp_32_post ≤ 0temp_32_posttemp_32_post ≤ 0temp_32_0 + temp_32_0 ≤ 0temp_32_0temp_32_0 ≤ 0temp0_28_post + temp0_28_post ≤ 0temp0_28_posttemp0_28_post ≤ 0temp0_28_1 + temp0_28_1 ≤ 0temp0_28_1temp0_28_1 ≤ 0temp0_28_0 + temp0_28_0 ≤ 0temp0_28_0temp0_28_0 ≤ 0temp0_18_0 + temp0_18_0 ≤ 0temp0_18_0temp0_18_0 ≤ 0tail_15_post + tail_15_post ≤ 0tail_15_posttail_15_post ≤ 0tail_15_0 + tail_15_0 ≤ 0tail_15_0tail_15_0 ≤ 0t_23_post + t_23_post ≤ 0t_23_postt_23_post ≤ 0t_23_0 + t_23_0 ≤ 0t_23_0t_23_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_postresult_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_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_99_post + rcd_99_post ≤ 0rcd_99_postrcd_99_post ≤ 0rcd_99_0 + rcd_99_0 ≤ 0rcd_99_0rcd_99_0 ≤ 0rcd_64_post + rcd_64_post ≤ 0rcd_64_postrcd_64_post ≤ 0rcd_64_0 + rcd_64_0 ≤ 0rcd_64_0rcd_64_0 ≤ 0rcd_40_post + rcd_40_post ≤ 0rcd_40_postrcd_40_post ≤ 0rcd_40_0 + rcd_40_0 ≤ 0rcd_40_0rcd_40_0 ≤ 0rcd_268_post + rcd_268_post ≤ 0rcd_268_postrcd_268_post ≤ 0rcd_268_0 + rcd_268_0 ≤ 0rcd_268_0rcd_268_0 ≤ 0rcd_248_post + rcd_248_post ≤ 0rcd_248_postrcd_248_post ≤ 0rcd_248_0 + rcd_248_0 ≤ 0rcd_248_0rcd_248_0 ≤ 0rcd_243_post + rcd_243_post ≤ 0rcd_243_postrcd_243_post ≤ 0rcd_243_0 + rcd_243_0 ≤ 0rcd_243_0rcd_243_0 ≤ 0rcd_239_post + rcd_239_post ≤ 0rcd_239_postrcd_239_post ≤ 0rcd_239_0 + rcd_239_0 ≤ 0rcd_239_0rcd_239_0 ≤ 0rcd_230_post + rcd_230_post ≤ 0rcd_230_postrcd_230_post ≤ 0rcd_230_0 + rcd_230_0 ≤ 0rcd_230_0rcd_230_0 ≤ 0rcd_107_post + rcd_107_post ≤ 0rcd_107_postrcd_107_post ≤ 0rcd_107_0 + rcd_107_0 ≤ 0rcd_107_0rcd_107_0 ≤ 0r_36_post + r_36_post ≤ 0r_36_postr_36_post ≤ 0r_36_0 + r_36_0 ≤ 0r_36_0r_36_0 ≤ 0r_267_post + r_267_post ≤ 0r_267_postr_267_post ≤ 0r_267_0 + r_267_0 ≤ 0r_267_0r_267_0 ≤ 0r_253_post + r_253_post ≤ 0r_253_postr_253_post ≤ 0r_253_0 + r_253_0 ≤ 0r_253_0r_253_0 ≤ 0r_247_post + r_247_post ≤ 0r_247_postr_247_post ≤ 0r_247_0 + r_247_0 ≤ 0r_247_0r_247_0 ≤ 0r_242_post + r_242_post ≤ 0r_242_postr_242_post ≤ 0r_242_0 + r_242_0 ≤ 0r_242_0r_242_0 ≤ 0r_240_post + r_240_post ≤ 0r_240_postr_240_post ≤ 0r_240_0 + r_240_0 ≤ 0r_240_0r_240_0 ≤ 0r_238_post + r_238_post ≤ 0r_238_postr_238_post ≤ 0r_238_0 + r_238_0 ≤ 0r_238_0r_238_0 ≤ 0r_229_post + r_229_post ≤ 0r_229_postr_229_post ≤ 0r_229_0 + r_229_0 ≤ 0r_229_0r_229_0 ≤ 0r_183_post + r_183_post ≤ 0r_183_postr_183_post ≤ 0r_183_0 + r_183_0 ≤ 0r_183_0r_183_0 ≤ 0r_154_post + r_154_post ≤ 0r_154_postr_154_post ≤ 0r_154_0 + r_154_0 ≤ 0r_154_0r_154_0 ≤ 0length_25_post + length_25_post ≤ 0length_25_postlength_25_post ≤ 0length_25_0 + length_25_0 ≤ 0length_25_0length_25_0 ≤ 0length_14_post + length_14_post ≤ 0length_14_postlength_14_post ≤ 0length_14_1 + length_14_1 ≤ 0length_14_1length_14_1 ≤ 0length_14_0 + length_14_0 ≤ 0length_14_0length_14_0 ≤ 0len_270_post + len_270_post ≤ 0len_270_postlen_270_post ≤ 0len_270_0 + len_270_0 ≤ 0len_270_0len_270_0 ≤ 0len_200_post + len_200_post ≤ 0len_200_postlen_200_post ≤ 0len_200_0 + len_200_0 ≤ 0len_200_0len_200_0 ≤ 0i_27_post + i_27_post ≤ 0i_27_posti_27_post ≤ 0i_27_0 + i_27_0 ≤ 0i_27_0i_27_0 ≤ 0i_114_post + i_114_post ≤ 0i_114_posti_114_post ≤ 0i_114_0 + i_114_0 ≤ 0i_114_0i_114_0 ≤ 0i_105_post + i_105_post ≤ 0i_105_posti_105_post ≤ 0i_105_0 + i_105_0 ≤ 0i_105_0i_105_0 ≤ 0head_SLAM_f_26_post + head_SLAM_f_26_post ≤ 0head_SLAM_f_26_posthead_SLAM_f_26_post ≤ 0head_SLAM_f_26_0 + head_SLAM_f_26_0 ≤ 0head_SLAM_f_26_0head_SLAM_f_26_0 ≤ 0head_29_post + head_29_post ≤ 0head_29_posthead_29_post ≤ 0head_29_0 + head_29_0 ≤ 0head_29_0head_29_0 ≤ 0head_13_post + head_13_post ≤ 0head_13_posthead_13_post ≤ 0head_13_0 + head_13_0 ≤ 0head_13_0head_13_0 ≤ 0a_271_post + a_271_post ≤ 0a_271_posta_271_post ≤ 0a_271_0 + a_271_0 ≤ 0a_271_0a_271_0 ≤ 0a_215_post + a_215_post ≤ 0a_215_posta_215_post ≤ 0a_215_0 + a_215_0 ≤ 0a_215_0a_215_0 ≤ 0a_168_post + a_168_post ≤ 0a_168_posta_168_post ≤ 0a_168_0 + a_168_0 ≤ 0a_168_0a_168_0 ≤ 0a_143_post + a_143_post ≤ 0a_143_posta_143_post ≤ 0a_143_0 + a_143_0 ≤ 0a_143_0a_143_0 ≤ 0

5 Location Addition

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

0 59 0_var_snapshot: z_19_post + z_19_post ≤ 0z_19_postz_19_post ≤ 0z_19_1 + z_19_1 ≤ 0z_19_1z_19_1 ≤ 0z_19_0 + z_19_0 ≤ 0z_19_0z_19_0 ≤ 0y_347_post + y_347_post ≤ 0y_347_posty_347_post ≤ 0y_347_0 + y_347_0 ≤ 0y_347_0y_347_0 ≤ 0y_295_post + y_295_post ≤ 0y_295_posty_295_post ≤ 0y_295_0 + y_295_0 ≤ 0y_295_0y_295_0 ≤ 0y_290_post + y_290_post ≤ 0y_290_posty_290_post ≤ 0y_290_0 + y_290_0 ≤ 0y_290_0y_290_0 ≤ 0y_285_post + y_285_post ≤ 0y_285_posty_285_post ≤ 0y_285_0 + y_285_0 ≤ 0y_285_0y_285_0 ≤ 0y_269_post + y_269_post ≤ 0y_269_posty_269_post ≤ 0y_269_0 + y_269_0 ≤ 0y_269_0y_269_0 ≤ 0y_261_post + y_261_post ≤ 0y_261_posty_261_post ≤ 0y_261_0 + y_261_0 ≤ 0y_261_0y_261_0 ≤ 0y_241_post + y_241_post ≤ 0y_241_posty_241_post ≤ 0y_241_0 + y_241_0 ≤ 0y_241_0y_241_0 ≤ 0y_231_post + y_231_post ≤ 0y_231_posty_231_post ≤ 0y_231_0 + y_231_0 ≤ 0y_231_0y_231_0 ≤ 0y_22_post + y_22_post ≤ 0y_22_posty_22_post ≤ 0y_22_1 + y_22_1 ≤ 0y_22_1y_22_1 ≤ 0y_22_0 + y_22_0 ≤ 0y_22_0y_22_0 ≤ 0y_191_post + y_191_post ≤ 0y_191_posty_191_post ≤ 0y_191_0 + y_191_0 ≤ 0y_191_0y_191_0 ≤ 0y_162_post + y_162_post ≤ 0y_162_posty_162_post ≤ 0y_162_0 + y_162_0 ≤ 0y_162_0y_162_0 ≤ 0x_21_post + x_21_post ≤ 0x_21_postx_21_post ≤ 0x_21_1 + x_21_1 ≤ 0x_21_1x_21_1 ≤ 0x_21_0 + x_21_0 ≤ 0x_21_0x_21_0 ≤ 0w_20_post + w_20_post ≤ 0w_20_postw_20_post ≤ 0w_20_1 + w_20_1 ≤ 0w_20_1w_20_1 ≤ 0w_20_0 + w_20_0 ≤ 0w_20_0w_20_0 ≤ 0tmp_31_post + tmp_31_post ≤ 0tmp_31_posttmp_31_post ≤ 0tmp_31_0 + tmp_31_0 ≤ 0tmp_31_0tmp_31_0 ≤ 0temp_32_post + temp_32_post ≤ 0temp_32_posttemp_32_post ≤ 0temp_32_0 + temp_32_0 ≤ 0temp_32_0temp_32_0 ≤ 0temp0_28_post + temp0_28_post ≤ 0temp0_28_posttemp0_28_post ≤ 0temp0_28_1 + temp0_28_1 ≤ 0temp0_28_1temp0_28_1 ≤ 0temp0_28_0 + temp0_28_0 ≤ 0temp0_28_0temp0_28_0 ≤ 0temp0_18_0 + temp0_18_0 ≤ 0temp0_18_0temp0_18_0 ≤ 0tail_15_post + tail_15_post ≤ 0tail_15_posttail_15_post ≤ 0tail_15_0 + tail_15_0 ≤ 0tail_15_0tail_15_0 ≤ 0t_23_post + t_23_post ≤ 0t_23_postt_23_post ≤ 0t_23_0 + t_23_0 ≤ 0t_23_0t_23_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_postresult_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_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_99_post + rcd_99_post ≤ 0rcd_99_postrcd_99_post ≤ 0rcd_99_0 + rcd_99_0 ≤ 0rcd_99_0rcd_99_0 ≤ 0rcd_64_post + rcd_64_post ≤ 0rcd_64_postrcd_64_post ≤ 0rcd_64_0 + rcd_64_0 ≤ 0rcd_64_0rcd_64_0 ≤ 0rcd_40_post + rcd_40_post ≤ 0rcd_40_postrcd_40_post ≤ 0rcd_40_0 + rcd_40_0 ≤ 0rcd_40_0rcd_40_0 ≤ 0rcd_268_post + rcd_268_post ≤ 0rcd_268_postrcd_268_post ≤ 0rcd_268_0 + rcd_268_0 ≤ 0rcd_268_0rcd_268_0 ≤ 0rcd_248_post + rcd_248_post ≤ 0rcd_248_postrcd_248_post ≤ 0rcd_248_0 + rcd_248_0 ≤ 0rcd_248_0rcd_248_0 ≤ 0rcd_243_post + rcd_243_post ≤ 0rcd_243_postrcd_243_post ≤ 0rcd_243_0 + rcd_243_0 ≤ 0rcd_243_0rcd_243_0 ≤ 0rcd_239_post + rcd_239_post ≤ 0rcd_239_postrcd_239_post ≤ 0rcd_239_0 + rcd_239_0 ≤ 0rcd_239_0rcd_239_0 ≤ 0rcd_230_post + rcd_230_post ≤ 0rcd_230_postrcd_230_post ≤ 0rcd_230_0 + rcd_230_0 ≤ 0rcd_230_0rcd_230_0 ≤ 0rcd_107_post + rcd_107_post ≤ 0rcd_107_postrcd_107_post ≤ 0rcd_107_0 + rcd_107_0 ≤ 0rcd_107_0rcd_107_0 ≤ 0r_36_post + r_36_post ≤ 0r_36_postr_36_post ≤ 0r_36_0 + r_36_0 ≤ 0r_36_0r_36_0 ≤ 0r_267_post + r_267_post ≤ 0r_267_postr_267_post ≤ 0r_267_0 + r_267_0 ≤ 0r_267_0r_267_0 ≤ 0r_253_post + r_253_post ≤ 0r_253_postr_253_post ≤ 0r_253_0 + r_253_0 ≤ 0r_253_0r_253_0 ≤ 0r_247_post + r_247_post ≤ 0r_247_postr_247_post ≤ 0r_247_0 + r_247_0 ≤ 0r_247_0r_247_0 ≤ 0r_242_post + r_242_post ≤ 0r_242_postr_242_post ≤ 0r_242_0 + r_242_0 ≤ 0r_242_0r_242_0 ≤ 0r_240_post + r_240_post ≤ 0r_240_postr_240_post ≤ 0r_240_0 + r_240_0 ≤ 0r_240_0r_240_0 ≤ 0r_238_post + r_238_post ≤ 0r_238_postr_238_post ≤ 0r_238_0 + r_238_0 ≤ 0r_238_0r_238_0 ≤ 0r_229_post + r_229_post ≤ 0r_229_postr_229_post ≤ 0r_229_0 + r_229_0 ≤ 0r_229_0r_229_0 ≤ 0r_183_post + r_183_post ≤ 0r_183_postr_183_post ≤ 0r_183_0 + r_183_0 ≤ 0r_183_0r_183_0 ≤ 0r_154_post + r_154_post ≤ 0r_154_postr_154_post ≤ 0r_154_0 + r_154_0 ≤ 0r_154_0r_154_0 ≤ 0length_25_post + length_25_post ≤ 0length_25_postlength_25_post ≤ 0length_25_0 + length_25_0 ≤ 0length_25_0length_25_0 ≤ 0length_14_post + length_14_post ≤ 0length_14_postlength_14_post ≤ 0length_14_1 + length_14_1 ≤ 0length_14_1length_14_1 ≤ 0length_14_0 + length_14_0 ≤ 0length_14_0length_14_0 ≤ 0len_270_post + len_270_post ≤ 0len_270_postlen_270_post ≤ 0len_270_0 + len_270_0 ≤ 0len_270_0len_270_0 ≤ 0len_200_post + len_200_post ≤ 0len_200_postlen_200_post ≤ 0len_200_0 + len_200_0 ≤ 0len_200_0len_200_0 ≤ 0i_27_post + i_27_post ≤ 0i_27_posti_27_post ≤ 0i_27_0 + i_27_0 ≤ 0i_27_0i_27_0 ≤ 0i_114_post + i_114_post ≤ 0i_114_posti_114_post ≤ 0i_114_0 + i_114_0 ≤ 0i_114_0i_114_0 ≤ 0i_105_post + i_105_post ≤ 0i_105_posti_105_post ≤ 0i_105_0 + i_105_0 ≤ 0i_105_0i_105_0 ≤ 0head_SLAM_f_26_post + head_SLAM_f_26_post ≤ 0head_SLAM_f_26_posthead_SLAM_f_26_post ≤ 0head_SLAM_f_26_0 + head_SLAM_f_26_0 ≤ 0head_SLAM_f_26_0head_SLAM_f_26_0 ≤ 0head_29_post + head_29_post ≤ 0head_29_posthead_29_post ≤ 0head_29_0 + head_29_0 ≤ 0head_29_0head_29_0 ≤ 0head_13_post + head_13_post ≤ 0head_13_posthead_13_post ≤ 0head_13_0 + head_13_0 ≤ 0head_13_0head_13_0 ≤ 0a_271_post + a_271_post ≤ 0a_271_posta_271_post ≤ 0a_271_0 + a_271_0 ≤ 0a_271_0a_271_0 ≤ 0a_215_post + a_215_post ≤ 0a_215_posta_215_post ≤ 0a_215_0 + a_215_0 ≤ 0a_215_0a_215_0 ≤ 0a_168_post + a_168_post ≤ 0a_168_posta_168_post ≤ 0a_168_0 + a_168_0 ≤ 0a_168_0a_168_0 ≤ 0a_143_post + a_143_post ≤ 0a_143_posta_143_post ≤ 0a_143_0 + a_143_0 ≤ 0a_143_0a_143_0 ≤ 0

6 Location Addition

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

37* 68 37: z_19_post + z_19_post ≤ 0z_19_postz_19_post ≤ 0z_19_1 + z_19_1 ≤ 0z_19_1z_19_1 ≤ 0z_19_0 + z_19_0 ≤ 0z_19_0z_19_0 ≤ 0y_347_post + y_347_post ≤ 0y_347_posty_347_post ≤ 0y_347_0 + y_347_0 ≤ 0y_347_0y_347_0 ≤ 0y_295_post + y_295_post ≤ 0y_295_posty_295_post ≤ 0y_295_0 + y_295_0 ≤ 0y_295_0y_295_0 ≤ 0y_290_post + y_290_post ≤ 0y_290_posty_290_post ≤ 0y_290_0 + y_290_0 ≤ 0y_290_0y_290_0 ≤ 0y_285_post + y_285_post ≤ 0y_285_posty_285_post ≤ 0y_285_0 + y_285_0 ≤ 0y_285_0y_285_0 ≤ 0y_269_post + y_269_post ≤ 0y_269_posty_269_post ≤ 0y_269_0 + y_269_0 ≤ 0y_269_0y_269_0 ≤ 0y_261_post + y_261_post ≤ 0y_261_posty_261_post ≤ 0y_261_0 + y_261_0 ≤ 0y_261_0y_261_0 ≤ 0y_241_post + y_241_post ≤ 0y_241_posty_241_post ≤ 0y_241_0 + y_241_0 ≤ 0y_241_0y_241_0 ≤ 0y_231_post + y_231_post ≤ 0y_231_posty_231_post ≤ 0y_231_0 + y_231_0 ≤ 0y_231_0y_231_0 ≤ 0y_22_post + y_22_post ≤ 0y_22_posty_22_post ≤ 0y_22_1 + y_22_1 ≤ 0y_22_1y_22_1 ≤ 0y_22_0 + y_22_0 ≤ 0y_22_0y_22_0 ≤ 0y_191_post + y_191_post ≤ 0y_191_posty_191_post ≤ 0y_191_0 + y_191_0 ≤ 0y_191_0y_191_0 ≤ 0y_162_post + y_162_post ≤ 0y_162_posty_162_post ≤ 0y_162_0 + y_162_0 ≤ 0y_162_0y_162_0 ≤ 0x_21_post + x_21_post ≤ 0x_21_postx_21_post ≤ 0x_21_1 + x_21_1 ≤ 0x_21_1x_21_1 ≤ 0x_21_0 + x_21_0 ≤ 0x_21_0x_21_0 ≤ 0w_20_post + w_20_post ≤ 0w_20_postw_20_post ≤ 0w_20_1 + w_20_1 ≤ 0w_20_1w_20_1 ≤ 0w_20_0 + w_20_0 ≤ 0w_20_0w_20_0 ≤ 0tmp_31_post + tmp_31_post ≤ 0tmp_31_posttmp_31_post ≤ 0tmp_31_0 + tmp_31_0 ≤ 0tmp_31_0tmp_31_0 ≤ 0temp_32_post + temp_32_post ≤ 0temp_32_posttemp_32_post ≤ 0temp_32_0 + temp_32_0 ≤ 0temp_32_0temp_32_0 ≤ 0temp0_28_post + temp0_28_post ≤ 0temp0_28_posttemp0_28_post ≤ 0temp0_28_1 + temp0_28_1 ≤ 0temp0_28_1temp0_28_1 ≤ 0temp0_28_0 + temp0_28_0 ≤ 0temp0_28_0temp0_28_0 ≤ 0temp0_18_0 + temp0_18_0 ≤ 0temp0_18_0temp0_18_0 ≤ 0tail_15_post + tail_15_post ≤ 0tail_15_posttail_15_post ≤ 0tail_15_0 + tail_15_0 ≤ 0tail_15_0tail_15_0 ≤ 0t_23_post + t_23_post ≤ 0t_23_postt_23_post ≤ 0t_23_0 + t_23_0 ≤ 0t_23_0t_23_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_postresult_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_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_99_post + rcd_99_post ≤ 0rcd_99_postrcd_99_post ≤ 0rcd_99_0 + rcd_99_0 ≤ 0rcd_99_0rcd_99_0 ≤ 0rcd_64_post + rcd_64_post ≤ 0rcd_64_postrcd_64_post ≤ 0rcd_64_0 + rcd_64_0 ≤ 0rcd_64_0rcd_64_0 ≤ 0rcd_40_post + rcd_40_post ≤ 0rcd_40_postrcd_40_post ≤ 0rcd_40_0 + rcd_40_0 ≤ 0rcd_40_0rcd_40_0 ≤ 0rcd_268_post + rcd_268_post ≤ 0rcd_268_postrcd_268_post ≤ 0rcd_268_0 + rcd_268_0 ≤ 0rcd_268_0rcd_268_0 ≤ 0rcd_248_post + rcd_248_post ≤ 0rcd_248_postrcd_248_post ≤ 0rcd_248_0 + rcd_248_0 ≤ 0rcd_248_0rcd_248_0 ≤ 0rcd_243_post + rcd_243_post ≤ 0rcd_243_postrcd_243_post ≤ 0rcd_243_0 + rcd_243_0 ≤ 0rcd_243_0rcd_243_0 ≤ 0rcd_239_post + rcd_239_post ≤ 0rcd_239_postrcd_239_post ≤ 0rcd_239_0 + rcd_239_0 ≤ 0rcd_239_0rcd_239_0 ≤ 0rcd_230_post + rcd_230_post ≤ 0rcd_230_postrcd_230_post ≤ 0rcd_230_0 + rcd_230_0 ≤ 0rcd_230_0rcd_230_0 ≤ 0rcd_107_post + rcd_107_post ≤ 0rcd_107_postrcd_107_post ≤ 0rcd_107_0 + rcd_107_0 ≤ 0rcd_107_0rcd_107_0 ≤ 0r_36_post + r_36_post ≤ 0r_36_postr_36_post ≤ 0r_36_0 + r_36_0 ≤ 0r_36_0r_36_0 ≤ 0r_267_post + r_267_post ≤ 0r_267_postr_267_post ≤ 0r_267_0 + r_267_0 ≤ 0r_267_0r_267_0 ≤ 0r_253_post + r_253_post ≤ 0r_253_postr_253_post ≤ 0r_253_0 + r_253_0 ≤ 0r_253_0r_253_0 ≤ 0r_247_post + r_247_post ≤ 0r_247_postr_247_post ≤ 0r_247_0 + r_247_0 ≤ 0r_247_0r_247_0 ≤ 0r_242_post + r_242_post ≤ 0r_242_postr_242_post ≤ 0r_242_0 + r_242_0 ≤ 0r_242_0r_242_0 ≤ 0r_240_post + r_240_post ≤ 0r_240_postr_240_post ≤ 0r_240_0 + r_240_0 ≤ 0r_240_0r_240_0 ≤ 0r_238_post + r_238_post ≤ 0r_238_postr_238_post ≤ 0r_238_0 + r_238_0 ≤ 0r_238_0r_238_0 ≤ 0r_229_post + r_229_post ≤ 0r_229_postr_229_post ≤ 0r_229_0 + r_229_0 ≤ 0r_229_0r_229_0 ≤ 0r_183_post + r_183_post ≤ 0r_183_postr_183_post ≤ 0r_183_0 + r_183_0 ≤ 0r_183_0r_183_0 ≤ 0r_154_post + r_154_post ≤ 0r_154_postr_154_post ≤ 0r_154_0 + r_154_0 ≤ 0r_154_0r_154_0 ≤ 0length_25_post + length_25_post ≤ 0length_25_postlength_25_post ≤ 0length_25_0 + length_25_0 ≤ 0length_25_0length_25_0 ≤ 0length_14_post + length_14_post ≤ 0length_14_postlength_14_post ≤ 0length_14_1 + length_14_1 ≤ 0length_14_1length_14_1 ≤ 0length_14_0 + length_14_0 ≤ 0length_14_0length_14_0 ≤ 0len_270_post + len_270_post ≤ 0len_270_postlen_270_post ≤ 0len_270_0 + len_270_0 ≤ 0len_270_0len_270_0 ≤ 0len_200_post + len_200_post ≤ 0len_200_postlen_200_post ≤ 0len_200_0 + len_200_0 ≤ 0len_200_0len_200_0 ≤ 0i_27_post + i_27_post ≤ 0i_27_posti_27_post ≤ 0i_27_0 + i_27_0 ≤ 0i_27_0i_27_0 ≤ 0i_114_post + i_114_post ≤ 0i_114_posti_114_post ≤ 0i_114_0 + i_114_0 ≤ 0i_114_0i_114_0 ≤ 0i_105_post + i_105_post ≤ 0i_105_posti_105_post ≤ 0i_105_0 + i_105_0 ≤ 0i_105_0i_105_0 ≤ 0head_SLAM_f_26_post + head_SLAM_f_26_post ≤ 0head_SLAM_f_26_posthead_SLAM_f_26_post ≤ 0head_SLAM_f_26_0 + head_SLAM_f_26_0 ≤ 0head_SLAM_f_26_0head_SLAM_f_26_0 ≤ 0head_29_post + head_29_post ≤ 0head_29_posthead_29_post ≤ 0head_29_0 + head_29_0 ≤ 0head_29_0head_29_0 ≤ 0head_13_post + head_13_post ≤ 0head_13_posthead_13_post ≤ 0head_13_0 + head_13_0 ≤ 0head_13_0head_13_0 ≤ 0a_271_post + a_271_post ≤ 0a_271_posta_271_post ≤ 0a_271_0 + a_271_0 ≤ 0a_271_0a_271_0 ≤ 0a_215_post + a_215_post ≤ 0a_215_posta_215_post ≤ 0a_215_0 + a_215_0 ≤ 0a_215_0a_215_0 ≤ 0a_168_post + a_168_post ≤ 0a_168_posta_168_post ≤ 0a_168_0 + a_168_0 ≤ 0a_168_0a_168_0 ≤ 0a_143_post + a_143_post ≤ 0a_143_posta_143_post ≤ 0a_143_0 + a_143_0 ≤ 0a_143_0a_143_0 ≤ 0

7 Location Addition

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

37 66 37_var_snapshot: z_19_post + z_19_post ≤ 0z_19_postz_19_post ≤ 0z_19_1 + z_19_1 ≤ 0z_19_1z_19_1 ≤ 0z_19_0 + z_19_0 ≤ 0z_19_0z_19_0 ≤ 0y_347_post + y_347_post ≤ 0y_347_posty_347_post ≤ 0y_347_0 + y_347_0 ≤ 0y_347_0y_347_0 ≤ 0y_295_post + y_295_post ≤ 0y_295_posty_295_post ≤ 0y_295_0 + y_295_0 ≤ 0y_295_0y_295_0 ≤ 0y_290_post + y_290_post ≤ 0y_290_posty_290_post ≤ 0y_290_0 + y_290_0 ≤ 0y_290_0y_290_0 ≤ 0y_285_post + y_285_post ≤ 0y_285_posty_285_post ≤ 0y_285_0 + y_285_0 ≤ 0y_285_0y_285_0 ≤ 0y_269_post + y_269_post ≤ 0y_269_posty_269_post ≤ 0y_269_0 + y_269_0 ≤ 0y_269_0y_269_0 ≤ 0y_261_post + y_261_post ≤ 0y_261_posty_261_post ≤ 0y_261_0 + y_261_0 ≤ 0y_261_0y_261_0 ≤ 0y_241_post + y_241_post ≤ 0y_241_posty_241_post ≤ 0y_241_0 + y_241_0 ≤ 0y_241_0y_241_0 ≤ 0y_231_post + y_231_post ≤ 0y_231_posty_231_post ≤ 0y_231_0 + y_231_0 ≤ 0y_231_0y_231_0 ≤ 0y_22_post + y_22_post ≤ 0y_22_posty_22_post ≤ 0y_22_1 + y_22_1 ≤ 0y_22_1y_22_1 ≤ 0y_22_0 + y_22_0 ≤ 0y_22_0y_22_0 ≤ 0y_191_post + y_191_post ≤ 0y_191_posty_191_post ≤ 0y_191_0 + y_191_0 ≤ 0y_191_0y_191_0 ≤ 0y_162_post + y_162_post ≤ 0y_162_posty_162_post ≤ 0y_162_0 + y_162_0 ≤ 0y_162_0y_162_0 ≤ 0x_21_post + x_21_post ≤ 0x_21_postx_21_post ≤ 0x_21_1 + x_21_1 ≤ 0x_21_1x_21_1 ≤ 0x_21_0 + x_21_0 ≤ 0x_21_0x_21_0 ≤ 0w_20_post + w_20_post ≤ 0w_20_postw_20_post ≤ 0w_20_1 + w_20_1 ≤ 0w_20_1w_20_1 ≤ 0w_20_0 + w_20_0 ≤ 0w_20_0w_20_0 ≤ 0tmp_31_post + tmp_31_post ≤ 0tmp_31_posttmp_31_post ≤ 0tmp_31_0 + tmp_31_0 ≤ 0tmp_31_0tmp_31_0 ≤ 0temp_32_post + temp_32_post ≤ 0temp_32_posttemp_32_post ≤ 0temp_32_0 + temp_32_0 ≤ 0temp_32_0temp_32_0 ≤ 0temp0_28_post + temp0_28_post ≤ 0temp0_28_posttemp0_28_post ≤ 0temp0_28_1 + temp0_28_1 ≤ 0temp0_28_1temp0_28_1 ≤ 0temp0_28_0 + temp0_28_0 ≤ 0temp0_28_0temp0_28_0 ≤ 0temp0_18_0 + temp0_18_0 ≤ 0temp0_18_0temp0_18_0 ≤ 0tail_15_post + tail_15_post ≤ 0tail_15_posttail_15_post ≤ 0tail_15_0 + tail_15_0 ≤ 0tail_15_0tail_15_0 ≤ 0t_23_post + t_23_post ≤ 0t_23_postt_23_post ≤ 0t_23_0 + t_23_0 ≤ 0t_23_0t_23_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_postresult_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_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_99_post + rcd_99_post ≤ 0rcd_99_postrcd_99_post ≤ 0rcd_99_0 + rcd_99_0 ≤ 0rcd_99_0rcd_99_0 ≤ 0rcd_64_post + rcd_64_post ≤ 0rcd_64_postrcd_64_post ≤ 0rcd_64_0 + rcd_64_0 ≤ 0rcd_64_0rcd_64_0 ≤ 0rcd_40_post + rcd_40_post ≤ 0rcd_40_postrcd_40_post ≤ 0rcd_40_0 + rcd_40_0 ≤ 0rcd_40_0rcd_40_0 ≤ 0rcd_268_post + rcd_268_post ≤ 0rcd_268_postrcd_268_post ≤ 0rcd_268_0 + rcd_268_0 ≤ 0rcd_268_0rcd_268_0 ≤ 0rcd_248_post + rcd_248_post ≤ 0rcd_248_postrcd_248_post ≤ 0rcd_248_0 + rcd_248_0 ≤ 0rcd_248_0rcd_248_0 ≤ 0rcd_243_post + rcd_243_post ≤ 0rcd_243_postrcd_243_post ≤ 0rcd_243_0 + rcd_243_0 ≤ 0rcd_243_0rcd_243_0 ≤ 0rcd_239_post + rcd_239_post ≤ 0rcd_239_postrcd_239_post ≤ 0rcd_239_0 + rcd_239_0 ≤ 0rcd_239_0rcd_239_0 ≤ 0rcd_230_post + rcd_230_post ≤ 0rcd_230_postrcd_230_post ≤ 0rcd_230_0 + rcd_230_0 ≤ 0rcd_230_0rcd_230_0 ≤ 0rcd_107_post + rcd_107_post ≤ 0rcd_107_postrcd_107_post ≤ 0rcd_107_0 + rcd_107_0 ≤ 0rcd_107_0rcd_107_0 ≤ 0r_36_post + r_36_post ≤ 0r_36_postr_36_post ≤ 0r_36_0 + r_36_0 ≤ 0r_36_0r_36_0 ≤ 0r_267_post + r_267_post ≤ 0r_267_postr_267_post ≤ 0r_267_0 + r_267_0 ≤ 0r_267_0r_267_0 ≤ 0r_253_post + r_253_post ≤ 0r_253_postr_253_post ≤ 0r_253_0 + r_253_0 ≤ 0r_253_0r_253_0 ≤ 0r_247_post + r_247_post ≤ 0r_247_postr_247_post ≤ 0r_247_0 + r_247_0 ≤ 0r_247_0r_247_0 ≤ 0r_242_post + r_242_post ≤ 0r_242_postr_242_post ≤ 0r_242_0 + r_242_0 ≤ 0r_242_0r_242_0 ≤ 0r_240_post + r_240_post ≤ 0r_240_postr_240_post ≤ 0r_240_0 + r_240_0 ≤ 0r_240_0r_240_0 ≤ 0r_238_post + r_238_post ≤ 0r_238_postr_238_post ≤ 0r_238_0 + r_238_0 ≤ 0r_238_0r_238_0 ≤ 0r_229_post + r_229_post ≤ 0r_229_postr_229_post ≤ 0r_229_0 + r_229_0 ≤ 0r_229_0r_229_0 ≤ 0r_183_post + r_183_post ≤ 0r_183_postr_183_post ≤ 0r_183_0 + r_183_0 ≤ 0r_183_0r_183_0 ≤ 0r_154_post + r_154_post ≤ 0r_154_postr_154_post ≤ 0r_154_0 + r_154_0 ≤ 0r_154_0r_154_0 ≤ 0length_25_post + length_25_post ≤ 0length_25_postlength_25_post ≤ 0length_25_0 + length_25_0 ≤ 0length_25_0length_25_0 ≤ 0length_14_post + length_14_post ≤ 0length_14_postlength_14_post ≤ 0length_14_1 + length_14_1 ≤ 0length_14_1length_14_1 ≤ 0length_14_0 + length_14_0 ≤ 0length_14_0length_14_0 ≤ 0len_270_post + len_270_post ≤ 0len_270_postlen_270_post ≤ 0len_270_0 + len_270_0 ≤ 0len_270_0len_270_0 ≤ 0len_200_post + len_200_post ≤ 0len_200_postlen_200_post ≤ 0len_200_0 + len_200_0 ≤ 0len_200_0len_200_0 ≤ 0i_27_post + i_27_post ≤ 0i_27_posti_27_post ≤ 0i_27_0 + i_27_0 ≤ 0i_27_0i_27_0 ≤ 0i_114_post + i_114_post ≤ 0i_114_posti_114_post ≤ 0i_114_0 + i_114_0 ≤ 0i_114_0i_114_0 ≤ 0i_105_post + i_105_post ≤ 0i_105_posti_105_post ≤ 0i_105_0 + i_105_0 ≤ 0i_105_0i_105_0 ≤ 0head_SLAM_f_26_post + head_SLAM_f_26_post ≤ 0head_SLAM_f_26_posthead_SLAM_f_26_post ≤ 0head_SLAM_f_26_0 + head_SLAM_f_26_0 ≤ 0head_SLAM_f_26_0head_SLAM_f_26_0 ≤ 0head_29_post + head_29_post ≤ 0head_29_posthead_29_post ≤ 0head_29_0 + head_29_0 ≤ 0head_29_0head_29_0 ≤ 0head_13_post + head_13_post ≤ 0head_13_posthead_13_post ≤ 0head_13_0 + head_13_0 ≤ 0head_13_0head_13_0 ≤ 0a_271_post + a_271_post ≤ 0a_271_posta_271_post ≤ 0a_271_0 + a_271_0 ≤ 0a_271_0a_271_0 ≤ 0a_215_post + a_215_post ≤ 0a_215_posta_215_post ≤ 0a_215_0 + a_215_0 ≤ 0a_215_0a_215_0 ≤ 0a_168_post + a_168_post ≤ 0a_168_posta_168_post ≤ 0a_168_0 + a_168_0 ≤ 0a_168_0a_168_0 ≤ 0a_143_post + a_143_post ≤ 0a_143_posta_143_post ≤ 0a_143_0 + a_143_0 ≤ 0a_143_0a_143_0 ≤ 0

8 SCC Decomposition

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

8.1 SCC Subproblem 1/2

Here we consider the SCC { 0, 5, 6, 7, 8, 9, 10, 11, 12, 0_var_snapshot, 0* }.

8.1.1 Transition Removal

We remove transitions 4, 5 using the following ranking functions, which are bounded by −10.

0: −7 + 11⋅a_215_0
5: −9 + 11⋅a_215_0
6: −10 + 11⋅a_215_0
7: 11⋅a_271_0
8: −1 + 11⋅a_271_0
9: −2 + 11⋅a_271_0
10: −3 + 11⋅a_271_0
11: −4 + 11⋅a_271_0
12: −5 + 11⋅a_215_0
0_var_snapshot: −8 + 11⋅a_215_0
0*: −6 + 11⋅a_215_0

8.1.2 Transition Removal

We remove transitions 59, 61, 6, 7, 8, 9, 10, 11, 12 using the following ranking functions, which are bounded by −2.

0: −1
5: 0
6: 7 + 5⋅len_200_0
7: 1 + 5⋅len_270_post
8: 5⋅len_270_post
9: 3 + len_270_post
10: 2 + len_270_post
11: 1 + len_270_post
12: len_270_post
0_var_snapshot: −2
0*: 0

8.1.3 Splitting Cut-Point Transitions

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

8.1.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 58.

8.1.3.1.1 Splitting Cut-Point Transitions

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

8.2 SCC Subproblem 2/2

Here we consider the SCC { 37, 49, 37_var_snapshot, 37* }.

8.2.1 Transition Removal

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

37: −1 − 4⋅i_27_0 + 4⋅length_25_0
49: 1 − 4⋅i_27_0 + 4⋅length_25_0
37_var_snapshot: −2 − 4⋅i_27_0 + 4⋅length_25_0
37*: −4⋅i_27_0 + 4⋅length_25_0

8.2.2 Transition Removal

We remove transitions 66, 68, 53 using the following ranking functions, which are bounded by −1.

37: 0
49: length_25_0
37_var_snapshot: −1
37*: −1 + length_25_0

8.2.3 Splitting Cut-Point Transitions

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

8.2.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 65.

8.2.3.1.1 Splitting Cut-Point Transitions

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

Tool configuration

T2Cert