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 ≤ 0 ∧ − a_215_0 ≤ 0
2: − len_200_0 ≤ 0 ∧ − a_215_0 ≤ 0
3: − len_200_0 ≤ 0 ∧ − a_215_0 ≤ 0
4: TRUE
5: − len_200_0 ≤ 0 ∧ − a_215_0 ≤ 0
6: − len_200_0 ≤ 0 ∧ − a_215_0 ≤ 0
7: − len_200_0 ≤ 0 ∧ − a_215_0 ≤ 0 ∧ 1 − len_270_post ≤ 0 ∧ 1 − len_270_0 ≤ 0
8: − len_200_0 ≤ 0 ∧ − a_215_0 ≤ 0 ∧ 1 − len_270_post ≤ 0 ∧ 1 − len_270_0 ≤ 0
9: − len_200_0 ≤ 0 ∧ − a_215_0 ≤ 0 ∧ 1 − len_270_post ≤ 0 ∧ 1 − len_270_0 ≤ 0
10: − len_200_0 ≤ 0 ∧ − a_215_0 ≤ 0 ∧ 1 − len_270_post ≤ 0 ∧ 1 − len_270_0 ≤ 0
11: − len_200_0 ≤ 0 ∧ − a_215_0 ≤ 0 ∧ 1 − len_270_post ≤ 0 ∧ 1 − len_270_0 ≤ 0
12: 2 − length_14_0 ≤ 0 ∧ 1 − len_270_post ≤ 0 ∧ 1 − len_270_0 ≤ 0
33: TRUE
34: i_27_post ≤ 0 ∧ − i_27_post ≤ 0 ∧ i_27_0 ≤ 0 ∧ − i_27_0 ≤ 0
35: −1 + i_27_post ≤ 0 ∧ 1 − i_27_post ≤ 0 ∧ −1 + i_27_0 ≤ 0 ∧ 1 − i_27_0 ≤ 0 ∧ 1 − length_25_0 ≤ 0
36: −1 + length_14_0 ≤ 0 ∧ 1 − length_14_0 ≤ 0 ∧ −1 + length_14_post ≤ 0 ∧ 1 − length_14_post ≤ 0
37: 2 − length_25_0 ≤ 0
38: 2 − length_14_0 ≤ 0 ∧ 2 − length_14_post ≤ 0
39: − i_114_0 ≤ 0
40: − i_114_0 ≤ 0
41: − i_114_0 ≤ 0 ∧ len_200_0 ≤ 0 ∧ − len_200_0 ≤ 0
42: − i_114_0 ≤ 0 ∧ len_200_0 ≤ 0 ∧ − len_200_0 ≤ 0
43: − i_114_0 ≤ 0 ∧ len_200_0 ≤ 0 ∧ − len_200_0 ≤ 0
44: TRUE
45: TRUE
46: −1 + length_14_0 ≤ 0 ∧ 1 − length_14_0 ≤ 0
47: −1 + length_14_0 ≤ 0 ∧ 1 − length_14_0 ≤ 0
48: −1 + length_14_0 ≤ 0 ∧ 1 − 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 ≤ 0 ∧ z_19_post − z_19_post ≤ 0 ∧ − z_19_1 + z_19_1 ≤ 0 ∧ z_19_1 − z_19_1 ≤ 0 ∧ − z_19_0 + z_19_0 ≤ 0 ∧ z_19_0 − z_19_0 ≤ 0 ∧ − y_347_post + y_347_post ≤ 0 ∧ y_347_post − y_347_post ≤ 0 ∧ − y_347_0 + y_347_0 ≤ 0 ∧ y_347_0 − y_347_0 ≤ 0 ∧ − y_295_post + y_295_post ≤ 0 ∧ y_295_post − y_295_post ≤ 0 ∧ − y_295_0 + y_295_0 ≤ 0 ∧ y_295_0 − y_295_0 ≤ 0 ∧ − y_290_post + y_290_post ≤ 0 ∧ y_290_post − y_290_post ≤ 0 ∧ − y_290_0 + y_290_0 ≤ 0 ∧ y_290_0 − y_290_0 ≤ 0 ∧ − y_285_post + y_285_post ≤ 0 ∧ y_285_post − y_285_post ≤ 0 ∧ − y_285_0 + y_285_0 ≤ 0 ∧ y_285_0 − y_285_0 ≤ 0 ∧ − y_269_post + y_269_post ≤ 0 ∧ y_269_post − y_269_post ≤ 0 ∧ − y_269_0 + y_269_0 ≤ 0 ∧ y_269_0 − y_269_0 ≤ 0 ∧ − y_261_post + y_261_post ≤ 0 ∧ y_261_post − y_261_post ≤ 0 ∧ − y_261_0 + y_261_0 ≤ 0 ∧ y_261_0 − y_261_0 ≤ 0 ∧ − y_241_post + y_241_post ≤ 0 ∧ y_241_post − y_241_post ≤ 0 ∧ − y_241_0 + y_241_0 ≤ 0 ∧ y_241_0 − y_241_0 ≤ 0 ∧ − y_231_post + y_231_post ≤ 0 ∧ y_231_post − y_231_post ≤ 0 ∧ − y_231_0 + y_231_0 ≤ 0 ∧ y_231_0 − y_231_0 ≤ 0 ∧ − y_22_post + y_22_post ≤ 0 ∧ y_22_post − y_22_post ≤ 0 ∧ − y_22_1 + y_22_1 ≤ 0 ∧ y_22_1 − y_22_1 ≤ 0 ∧ − y_22_0 + y_22_0 ≤ 0 ∧ y_22_0 − y_22_0 ≤ 0 ∧ − y_191_post + y_191_post ≤ 0 ∧ y_191_post − y_191_post ≤ 0 ∧ − y_191_0 + y_191_0 ≤ 0 ∧ y_191_0 − y_191_0 ≤ 0 ∧ − y_162_post + y_162_post ≤ 0 ∧ y_162_post − y_162_post ≤ 0 ∧ − y_162_0 + y_162_0 ≤ 0 ∧ y_162_0 − y_162_0 ≤ 0 ∧ − x_21_post + x_21_post ≤ 0 ∧ x_21_post − x_21_post ≤ 0 ∧ − x_21_1 + x_21_1 ≤ 0 ∧ x_21_1 − x_21_1 ≤ 0 ∧ − x_21_0 + x_21_0 ≤ 0 ∧ x_21_0 − x_21_0 ≤ 0 ∧ − w_20_post + w_20_post ≤ 0 ∧ w_20_post − w_20_post ≤ 0 ∧ − w_20_1 + w_20_1 ≤ 0 ∧ w_20_1 − w_20_1 ≤ 0 ∧ − w_20_0 + w_20_0 ≤ 0 ∧ w_20_0 − w_20_0 ≤ 0 ∧ − tmp_31_post + tmp_31_post ≤ 0 ∧ tmp_31_post − tmp_31_post ≤ 0 ∧ − tmp_31_0 + tmp_31_0 ≤ 0 ∧ tmp_31_0 − tmp_31_0 ≤ 0 ∧ − temp_32_post + temp_32_post ≤ 0 ∧ temp_32_post − temp_32_post ≤ 0 ∧ − temp_32_0 + temp_32_0 ≤ 0 ∧ temp_32_0 − temp_32_0 ≤ 0 ∧ − temp0_28_post + temp0_28_post ≤ 0 ∧ temp0_28_post − temp0_28_post ≤ 0 ∧ − temp0_28_1 + temp0_28_1 ≤ 0 ∧ temp0_28_1 − temp0_28_1 ≤ 0 ∧ − temp0_28_0 + temp0_28_0 ≤ 0 ∧ temp0_28_0 − temp0_28_0 ≤ 0 ∧ − temp0_18_0 + temp0_18_0 ≤ 0 ∧ temp0_18_0 − temp0_18_0 ≤ 0 ∧ − tail_15_post + tail_15_post ≤ 0 ∧ tail_15_post − tail_15_post ≤ 0 ∧ − tail_15_0 + tail_15_0 ≤ 0 ∧ tail_15_0 − tail_15_0 ≤ 0 ∧ − t_23_post + t_23_post ≤ 0 ∧ t_23_post − t_23_post ≤ 0 ∧ − t_23_0 + t_23_0 ≤ 0 ∧ t_23_0 − t_23_0 ≤ 0 ∧ − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0 ∧ − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 ≤ 0 ∧ − result_11_post + result_11_post ≤ 0 ∧ result_11_post − result_11_post ≤ 0 ∧ − result_11_2 + result_11_2 ≤ 0 ∧ result_11_2 − result_11_2 ≤ 0 ∧ − result_11_1 + result_11_1 ≤ 0 ∧ result_11_1 − result_11_1 ≤ 0 ∧ − result_11_0 + result_11_0 ≤ 0 ∧ result_11_0 − result_11_0 ≤ 0 ∧ − rcd_99_post + rcd_99_post ≤ 0 ∧ rcd_99_post − rcd_99_post ≤ 0 ∧ − rcd_99_0 + rcd_99_0 ≤ 0 ∧ rcd_99_0 − rcd_99_0 ≤ 0 ∧ − rcd_64_post + rcd_64_post ≤ 0 ∧ rcd_64_post − rcd_64_post ≤ 0 ∧ − rcd_64_0 + rcd_64_0 ≤ 0 ∧ rcd_64_0 − rcd_64_0 ≤ 0 ∧ − rcd_40_post + rcd_40_post ≤ 0 ∧ rcd_40_post − rcd_40_post ≤ 0 ∧ − rcd_40_0 + rcd_40_0 ≤ 0 ∧ rcd_40_0 − rcd_40_0 ≤ 0 ∧ − rcd_268_post + rcd_268_post ≤ 0 ∧ rcd_268_post − rcd_268_post ≤ 0 ∧ − rcd_268_0 + rcd_268_0 ≤ 0 ∧ rcd_268_0 − rcd_268_0 ≤ 0 ∧ − rcd_248_post + rcd_248_post ≤ 0 ∧ rcd_248_post − rcd_248_post ≤ 0 ∧ − rcd_248_0 + rcd_248_0 ≤ 0 ∧ rcd_248_0 − rcd_248_0 ≤ 0 ∧ − rcd_243_post + rcd_243_post ≤ 0 ∧ rcd_243_post − rcd_243_post ≤ 0 ∧ − rcd_243_0 + rcd_243_0 ≤ 0 ∧ rcd_243_0 − rcd_243_0 ≤ 0 ∧ − rcd_239_post + rcd_239_post ≤ 0 ∧ rcd_239_post − rcd_239_post ≤ 0 ∧ − rcd_239_0 + rcd_239_0 ≤ 0 ∧ rcd_239_0 − rcd_239_0 ≤ 0 ∧ − rcd_230_post + rcd_230_post ≤ 0 ∧ rcd_230_post − rcd_230_post ≤ 0 ∧ − rcd_230_0 + rcd_230_0 ≤ 0 ∧ rcd_230_0 − rcd_230_0 ≤ 0 ∧ − rcd_107_post + rcd_107_post ≤ 0 ∧ rcd_107_post − rcd_107_post ≤ 0 ∧ − rcd_107_0 + rcd_107_0 ≤ 0 ∧ rcd_107_0 − rcd_107_0 ≤ 0 ∧ − r_36_post + r_36_post ≤ 0 ∧ r_36_post − r_36_post ≤ 0 ∧ − r_36_0 + r_36_0 ≤ 0 ∧ r_36_0 − r_36_0 ≤ 0 ∧ − r_267_post + r_267_post ≤ 0 ∧ r_267_post − r_267_post ≤ 0 ∧ − r_267_0 + r_267_0 ≤ 0 ∧ r_267_0 − r_267_0 ≤ 0 ∧ − r_253_post + r_253_post ≤ 0 ∧ r_253_post − r_253_post ≤ 0 ∧ − r_253_0 + r_253_0 ≤ 0 ∧ r_253_0 − r_253_0 ≤ 0 ∧ − r_247_post + r_247_post ≤ 0 ∧ r_247_post − r_247_post ≤ 0 ∧ − r_247_0 + r_247_0 ≤ 0 ∧ r_247_0 − r_247_0 ≤ 0 ∧ − r_242_post + r_242_post ≤ 0 ∧ r_242_post − r_242_post ≤ 0 ∧ − r_242_0 + r_242_0 ≤ 0 ∧ r_242_0 − r_242_0 ≤ 0 ∧ − r_240_post + r_240_post ≤ 0 ∧ r_240_post − r_240_post ≤ 0 ∧ − r_240_0 + r_240_0 ≤ 0 ∧ r_240_0 − r_240_0 ≤ 0 ∧ − r_238_post + r_238_post ≤ 0 ∧ r_238_post − r_238_post ≤ 0 ∧ − r_238_0 + r_238_0 ≤ 0 ∧ r_238_0 − r_238_0 ≤ 0 ∧ − r_229_post + r_229_post ≤ 0 ∧ r_229_post − r_229_post ≤ 0 ∧ − r_229_0 + r_229_0 ≤ 0 ∧ r_229_0 − r_229_0 ≤ 0 ∧ − r_183_post + r_183_post ≤ 0 ∧ r_183_post − r_183_post ≤ 0 ∧ − r_183_0 + r_183_0 ≤ 0 ∧ r_183_0 − r_183_0 ≤ 0 ∧ − r_154_post + r_154_post ≤ 0 ∧ r_154_post − r_154_post ≤ 0 ∧ − r_154_0 + r_154_0 ≤ 0 ∧ r_154_0 − r_154_0 ≤ 0 ∧ − length_25_post + length_25_post ≤ 0 ∧ length_25_post − length_25_post ≤ 0 ∧ − length_25_0 + length_25_0 ≤ 0 ∧ length_25_0 − length_25_0 ≤ 0 ∧ − length_14_post + length_14_post ≤ 0 ∧ length_14_post − length_14_post ≤ 0 ∧ − length_14_1 + length_14_1 ≤ 0 ∧ length_14_1 − length_14_1 ≤ 0 ∧ − length_14_0 + length_14_0 ≤ 0 ∧ length_14_0 − length_14_0 ≤ 0 ∧ − len_270_post + len_270_post ≤ 0 ∧ len_270_post − len_270_post ≤ 0 ∧ − len_270_0 + len_270_0 ≤ 0 ∧ len_270_0 − len_270_0 ≤ 0 ∧ − len_200_post + len_200_post ≤ 0 ∧ len_200_post − len_200_post ≤ 0 ∧ − len_200_0 + len_200_0 ≤ 0 ∧ len_200_0 − len_200_0 ≤ 0 ∧ − i_27_post + i_27_post ≤ 0 ∧ i_27_post − i_27_post ≤ 0 ∧ − i_27_0 + i_27_0 ≤ 0 ∧ i_27_0 − i_27_0 ≤ 0 ∧ − i_114_post + i_114_post ≤ 0 ∧ i_114_post − i_114_post ≤ 0 ∧ − i_114_0 + i_114_0 ≤ 0 ∧ i_114_0 − i_114_0 ≤ 0 ∧ − i_105_post + i_105_post ≤ 0 ∧ i_105_post − i_105_post ≤ 0 ∧ − i_105_0 + i_105_0 ≤ 0 ∧ i_105_0 − i_105_0 ≤ 0 ∧ − head_SLAM_f_26_post + head_SLAM_f_26_post ≤ 0 ∧ head_SLAM_f_26_post − head_SLAM_f_26_post ≤ 0 ∧ − head_SLAM_f_26_0 + head_SLAM_f_26_0 ≤ 0 ∧ head_SLAM_f_26_0 − head_SLAM_f_26_0 ≤ 0 ∧ − head_29_post + head_29_post ≤ 0 ∧ head_29_post − head_29_post ≤ 0 ∧ − head_29_0 + head_29_0 ≤ 0 ∧ head_29_0 − head_29_0 ≤ 0 ∧ − head_13_post + head_13_post ≤ 0 ∧ head_13_post − head_13_post ≤ 0 ∧ − head_13_0 + head_13_0 ≤ 0 ∧ head_13_0 − head_13_0 ≤ 0 ∧ − a_271_post + a_271_post ≤ 0 ∧ a_271_post − a_271_post ≤ 0 ∧ − a_271_0 + a_271_0 ≤ 0 ∧ a_271_0 − a_271_0 ≤ 0 ∧ − a_215_post + a_215_post ≤ 0 ∧ a_215_post − a_215_post ≤ 0 ∧ − a_215_0 + a_215_0 ≤ 0 ∧ a_215_0 − a_215_0 ≤ 0 ∧ − a_168_post + a_168_post ≤ 0 ∧ a_168_post − a_168_post ≤ 0 ∧ − a_168_0 + a_168_0 ≤ 0 ∧ a_168_0 − a_168_0 ≤ 0 ∧ − a_143_post + a_143_post ≤ 0 ∧ a_143_post − a_143_post ≤ 0 ∧ − a_143_0 + a_143_0 ≤ 0 ∧ a_143_0 − a_143_0 ≤ 0
37 65 37: − z_19_post + z_19_post ≤ 0 ∧ z_19_post − z_19_post ≤ 0 ∧ − z_19_1 + z_19_1 ≤ 0 ∧ z_19_1 − z_19_1 ≤ 0 ∧ − z_19_0 + z_19_0 ≤ 0 ∧ z_19_0 − z_19_0 ≤ 0 ∧ − y_347_post + y_347_post ≤ 0 ∧ y_347_post − y_347_post ≤ 0 ∧ − y_347_0 + y_347_0 ≤ 0 ∧ y_347_0 − y_347_0 ≤ 0 ∧ − y_295_post + y_295_post ≤ 0 ∧ y_295_post − y_295_post ≤ 0 ∧ − y_295_0 + y_295_0 ≤ 0 ∧ y_295_0 − y_295_0 ≤ 0 ∧ − y_290_post + y_290_post ≤ 0 ∧ y_290_post − y_290_post ≤ 0 ∧ − y_290_0 + y_290_0 ≤ 0 ∧ y_290_0 − y_290_0 ≤ 0 ∧ − y_285_post + y_285_post ≤ 0 ∧ y_285_post − y_285_post ≤ 0 ∧ − y_285_0 + y_285_0 ≤ 0 ∧ y_285_0 − y_285_0 ≤ 0 ∧ − y_269_post + y_269_post ≤ 0 ∧ y_269_post − y_269_post ≤ 0 ∧ − y_269_0 + y_269_0 ≤ 0 ∧ y_269_0 − y_269_0 ≤ 0 ∧ − y_261_post + y_261_post ≤ 0 ∧ y_261_post − y_261_post ≤ 0 ∧ − y_261_0 + y_261_0 ≤ 0 ∧ y_261_0 − y_261_0 ≤ 0 ∧ − y_241_post + y_241_post ≤ 0 ∧ y_241_post − y_241_post ≤ 0 ∧ − y_241_0 + y_241_0 ≤ 0 ∧ y_241_0 − y_241_0 ≤ 0 ∧ − y_231_post + y_231_post ≤ 0 ∧ y_231_post − y_231_post ≤ 0 ∧ − y_231_0 + y_231_0 ≤ 0 ∧ y_231_0 − y_231_0 ≤ 0 ∧ − y_22_post + y_22_post ≤ 0 ∧ y_22_post − y_22_post ≤ 0 ∧ − y_22_1 + y_22_1 ≤ 0 ∧ y_22_1 − y_22_1 ≤ 0 ∧ − y_22_0 + y_22_0 ≤ 0 ∧ y_22_0 − y_22_0 ≤ 0 ∧ − y_191_post + y_191_post ≤ 0 ∧ y_191_post − y_191_post ≤ 0 ∧ − y_191_0 + y_191_0 ≤ 0 ∧ y_191_0 − y_191_0 ≤ 0 ∧ − y_162_post + y_162_post ≤ 0 ∧ y_162_post − y_162_post ≤ 0 ∧ − y_162_0 + y_162_0 ≤ 0 ∧ y_162_0 − y_162_0 ≤ 0 ∧ − x_21_post + x_21_post ≤ 0 ∧ x_21_post − x_21_post ≤ 0 ∧ − x_21_1 + x_21_1 ≤ 0 ∧ x_21_1 − x_21_1 ≤ 0 ∧ − x_21_0 + x_21_0 ≤ 0 ∧ x_21_0 − x_21_0 ≤ 0 ∧ − w_20_post + w_20_post ≤ 0 ∧ w_20_post − w_20_post ≤ 0 ∧ − w_20_1 + w_20_1 ≤ 0 ∧ w_20_1 − w_20_1 ≤ 0 ∧ − w_20_0 + w_20_0 ≤ 0 ∧ w_20_0 − w_20_0 ≤ 0 ∧ − tmp_31_post + tmp_31_post ≤ 0 ∧ tmp_31_post − tmp_31_post ≤ 0 ∧ − tmp_31_0 + tmp_31_0 ≤ 0 ∧ tmp_31_0 − tmp_31_0 ≤ 0 ∧ − temp_32_post + temp_32_post ≤ 0 ∧ temp_32_post − temp_32_post ≤ 0 ∧ − temp_32_0 + temp_32_0 ≤ 0 ∧ temp_32_0 − temp_32_0 ≤ 0 ∧ − temp0_28_post + temp0_28_post ≤ 0 ∧ temp0_28_post − temp0_28_post ≤ 0 ∧ − temp0_28_1 + temp0_28_1 ≤ 0 ∧ temp0_28_1 − temp0_28_1 ≤ 0 ∧ − temp0_28_0 + temp0_28_0 ≤ 0 ∧ temp0_28_0 − temp0_28_0 ≤ 0 ∧ − temp0_18_0 + temp0_18_0 ≤ 0 ∧ temp0_18_0 − temp0_18_0 ≤ 0 ∧ − tail_15_post + tail_15_post ≤ 0 ∧ tail_15_post − tail_15_post ≤ 0 ∧ − tail_15_0 + tail_15_0 ≤ 0 ∧ tail_15_0 − tail_15_0 ≤ 0 ∧ − t_23_post + t_23_post ≤ 0 ∧ t_23_post − t_23_post ≤ 0 ∧ − t_23_0 + t_23_0 ≤ 0 ∧ t_23_0 − t_23_0 ≤ 0 ∧ − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0 ∧ − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 ≤ 0 ∧ − result_11_post + result_11_post ≤ 0 ∧ result_11_post − result_11_post ≤ 0 ∧ − result_11_2 + result_11_2 ≤ 0 ∧ result_11_2 − result_11_2 ≤ 0 ∧ − result_11_1 + result_11_1 ≤ 0 ∧ result_11_1 − result_11_1 ≤ 0 ∧ − result_11_0 + result_11_0 ≤ 0 ∧ result_11_0 − result_11_0 ≤ 0 ∧ − rcd_99_post + rcd_99_post ≤ 0 ∧ rcd_99_post − rcd_99_post ≤ 0 ∧ − rcd_99_0 + rcd_99_0 ≤ 0 ∧ rcd_99_0 − rcd_99_0 ≤ 0 ∧ − rcd_64_post + rcd_64_post ≤ 0 ∧ rcd_64_post − rcd_64_post ≤ 0 ∧ − rcd_64_0 + rcd_64_0 ≤ 0 ∧ rcd_64_0 − rcd_64_0 ≤ 0 ∧ − rcd_40_post + rcd_40_post ≤ 0 ∧ rcd_40_post − rcd_40_post ≤ 0 ∧ − rcd_40_0 + rcd_40_0 ≤ 0 ∧ rcd_40_0 − rcd_40_0 ≤ 0 ∧ − rcd_268_post + rcd_268_post ≤ 0 ∧ rcd_268_post − rcd_268_post ≤ 0 ∧ − rcd_268_0 + rcd_268_0 ≤ 0 ∧ rcd_268_0 − rcd_268_0 ≤ 0 ∧ − rcd_248_post + rcd_248_post ≤ 0 ∧ rcd_248_post − rcd_248_post ≤ 0 ∧ − rcd_248_0 + rcd_248_0 ≤ 0 ∧ rcd_248_0 − rcd_248_0 ≤ 0 ∧ − rcd_243_post + rcd_243_post ≤ 0 ∧ rcd_243_post − rcd_243_post ≤ 0 ∧ − rcd_243_0 + rcd_243_0 ≤ 0 ∧ rcd_243_0 − rcd_243_0 ≤ 0 ∧ − rcd_239_post + rcd_239_post ≤ 0 ∧ rcd_239_post − rcd_239_post ≤ 0 ∧ − rcd_239_0 + rcd_239_0 ≤ 0 ∧ rcd_239_0 − rcd_239_0 ≤ 0 ∧ − rcd_230_post + rcd_230_post ≤ 0 ∧ rcd_230_post − rcd_230_post ≤ 0 ∧ − rcd_230_0 + rcd_230_0 ≤ 0 ∧ rcd_230_0 − rcd_230_0 ≤ 0 ∧ − rcd_107_post + rcd_107_post ≤ 0 ∧ rcd_107_post − rcd_107_post ≤ 0 ∧ − rcd_107_0 + rcd_107_0 ≤ 0 ∧ rcd_107_0 − rcd_107_0 ≤ 0 ∧ − r_36_post + r_36_post ≤ 0 ∧ r_36_post − r_36_post ≤ 0 ∧ − r_36_0 + r_36_0 ≤ 0 ∧ r_36_0 − r_36_0 ≤ 0 ∧ − r_267_post + r_267_post ≤ 0 ∧ r_267_post − r_267_post ≤ 0 ∧ − r_267_0 + r_267_0 ≤ 0 ∧ r_267_0 − r_267_0 ≤ 0 ∧ − r_253_post + r_253_post ≤ 0 ∧ r_253_post − r_253_post ≤ 0 ∧ − r_253_0 + r_253_0 ≤ 0 ∧ r_253_0 − r_253_0 ≤ 0 ∧ − r_247_post + r_247_post ≤ 0 ∧ r_247_post − r_247_post ≤ 0 ∧ − r_247_0 + r_247_0 ≤ 0 ∧ r_247_0 − r_247_0 ≤ 0 ∧ − r_242_post + r_242_post ≤ 0 ∧ r_242_post − r_242_post ≤ 0 ∧ − r_242_0 + r_242_0 ≤ 0 ∧ r_242_0 − r_242_0 ≤ 0 ∧ − r_240_post + r_240_post ≤ 0 ∧ r_240_post − r_240_post ≤ 0 ∧ − r_240_0 + r_240_0 ≤ 0 ∧ r_240_0 − r_240_0 ≤ 0 ∧ − r_238_post + r_238_post ≤ 0 ∧ r_238_post − r_238_post ≤ 0 ∧ − r_238_0 + r_238_0 ≤ 0 ∧ r_238_0 − r_238_0 ≤ 0 ∧ − r_229_post + r_229_post ≤ 0 ∧ r_229_post − r_229_post ≤ 0 ∧ − r_229_0 + r_229_0 ≤ 0 ∧ r_229_0 − r_229_0 ≤ 0 ∧ − r_183_post + r_183_post ≤ 0 ∧ r_183_post − r_183_post ≤ 0 ∧ − r_183_0 + r_183_0 ≤ 0 ∧ r_183_0 − r_183_0 ≤ 0 ∧ − r_154_post + r_154_post ≤ 0 ∧ r_154_post − r_154_post ≤ 0 ∧ − r_154_0 + r_154_0 ≤ 0 ∧ r_154_0 − r_154_0 ≤ 0 ∧ − length_25_post + length_25_post ≤ 0 ∧ length_25_post − length_25_post ≤ 0 ∧ − length_25_0 + length_25_0 ≤ 0 ∧ length_25_0 − length_25_0 ≤ 0 ∧ − length_14_post + length_14_post ≤ 0 ∧ length_14_post − length_14_post ≤ 0 ∧ − length_14_1 + length_14_1 ≤ 0 ∧ length_14_1 − length_14_1 ≤ 0 ∧ − length_14_0 + length_14_0 ≤ 0 ∧ length_14_0 − length_14_0 ≤ 0 ∧ − len_270_post + len_270_post ≤ 0 ∧ len_270_post − len_270_post ≤ 0 ∧ − len_270_0 + len_270_0 ≤ 0 ∧ len_270_0 − len_270_0 ≤ 0 ∧ − len_200_post + len_200_post ≤ 0 ∧ len_200_post − len_200_post ≤ 0 ∧ − len_200_0 + len_200_0 ≤ 0 ∧ len_200_0 − len_200_0 ≤ 0 ∧ − i_27_post + i_27_post ≤ 0 ∧ i_27_post − i_27_post ≤ 0 ∧ − i_27_0 + i_27_0 ≤ 0 ∧ i_27_0 − i_27_0 ≤ 0 ∧ − i_114_post + i_114_post ≤ 0 ∧ i_114_post − i_114_post ≤ 0 ∧ − i_114_0 + i_114_0 ≤ 0 ∧ i_114_0 − i_114_0 ≤ 0 ∧ − i_105_post + i_105_post ≤ 0 ∧ i_105_post − i_105_post ≤ 0 ∧ − i_105_0 + i_105_0 ≤ 0 ∧ i_105_0 − i_105_0 ≤ 0 ∧ − head_SLAM_f_26_post + head_SLAM_f_26_post ≤ 0 ∧ head_SLAM_f_26_post − head_SLAM_f_26_post ≤ 0 ∧ − head_SLAM_f_26_0 + head_SLAM_f_26_0 ≤ 0 ∧ head_SLAM_f_26_0 − head_SLAM_f_26_0 ≤ 0 ∧ − head_29_post + head_29_post ≤ 0 ∧ head_29_post − head_29_post ≤ 0 ∧ − head_29_0 + head_29_0 ≤ 0 ∧ head_29_0 − head_29_0 ≤ 0 ∧ − head_13_post + head_13_post ≤ 0 ∧ head_13_post − head_13_post ≤ 0 ∧ − head_13_0 + head_13_0 ≤ 0 ∧ head_13_0 − head_13_0 ≤ 0 ∧ − a_271_post + a_271_post ≤ 0 ∧ a_271_post − a_271_post ≤ 0 ∧ − a_271_0 + a_271_0 ≤ 0 ∧ a_271_0 − a_271_0 ≤ 0 ∧ − a_215_post + a_215_post ≤ 0 ∧ a_215_post − a_215_post ≤ 0 ∧ − a_215_0 + a_215_0 ≤ 0 ∧ a_215_0 − a_215_0 ≤ 0 ∧ − a_168_post + a_168_post ≤ 0 ∧ a_168_post − a_168_post ≤ 0 ∧ − a_168_0 + a_168_0 ≤ 0 ∧ a_168_0 − a_168_0 ≤ 0 ∧ − a_143_post + a_143_post ≤ 0 ∧ a_143_post − a_143_post ≤ 0 ∧ − a_143_0 + a_143_0 ≤ 0 ∧ a_143_0 − a_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 ≤ 0 ∧ z_19_post − z_19_post ≤ 0 ∧ − z_19_1 + z_19_1 ≤ 0 ∧ z_19_1 − z_19_1 ≤ 0 ∧ − z_19_0 + z_19_0 ≤ 0 ∧ z_19_0 − z_19_0 ≤ 0 ∧ − y_347_post + y_347_post ≤ 0 ∧ y_347_post − y_347_post ≤ 0 ∧ − y_347_0 + y_347_0 ≤ 0 ∧ y_347_0 − y_347_0 ≤ 0 ∧ − y_295_post + y_295_post ≤ 0 ∧ y_295_post − y_295_post ≤ 0 ∧ − y_295_0 + y_295_0 ≤ 0 ∧ y_295_0 − y_295_0 ≤ 0 ∧ − y_290_post + y_290_post ≤ 0 ∧ y_290_post − y_290_post ≤ 0 ∧ − y_290_0 + y_290_0 ≤ 0 ∧ y_290_0 − y_290_0 ≤ 0 ∧ − y_285_post + y_285_post ≤ 0 ∧ y_285_post − y_285_post ≤ 0 ∧ − y_285_0 + y_285_0 ≤ 0 ∧ y_285_0 − y_285_0 ≤ 0 ∧ − y_269_post + y_269_post ≤ 0 ∧ y_269_post − y_269_post ≤ 0 ∧ − y_269_0 + y_269_0 ≤ 0 ∧ y_269_0 − y_269_0 ≤ 0 ∧ − y_261_post + y_261_post ≤ 0 ∧ y_261_post − y_261_post ≤ 0 ∧ − y_261_0 + y_261_0 ≤ 0 ∧ y_261_0 − y_261_0 ≤ 0 ∧ − y_241_post + y_241_post ≤ 0 ∧ y_241_post − y_241_post ≤ 0 ∧ − y_241_0 + y_241_0 ≤ 0 ∧ y_241_0 − y_241_0 ≤ 0 ∧ − y_231_post + y_231_post ≤ 0 ∧ y_231_post − y_231_post ≤ 0 ∧ − y_231_0 + y_231_0 ≤ 0 ∧ y_231_0 − y_231_0 ≤ 0 ∧ − y_22_post + y_22_post ≤ 0 ∧ y_22_post − y_22_post ≤ 0 ∧ − y_22_1 + y_22_1 ≤ 0 ∧ y_22_1 − y_22_1 ≤ 0 ∧ − y_22_0 + y_22_0 ≤ 0 ∧ y_22_0 − y_22_0 ≤ 0 ∧ − y_191_post + y_191_post ≤ 0 ∧ y_191_post − y_191_post ≤ 0 ∧ − y_191_0 + y_191_0 ≤ 0 ∧ y_191_0 − y_191_0 ≤ 0 ∧ − y_162_post + y_162_post ≤ 0 ∧ y_162_post − y_162_post ≤ 0 ∧ − y_162_0 + y_162_0 ≤ 0 ∧ y_162_0 − y_162_0 ≤ 0 ∧ − x_21_post + x_21_post ≤ 0 ∧ x_21_post − x_21_post ≤ 0 ∧ − x_21_1 + x_21_1 ≤ 0 ∧ x_21_1 − x_21_1 ≤ 0 ∧ − x_21_0 + x_21_0 ≤ 0 ∧ x_21_0 − x_21_0 ≤ 0 ∧ − w_20_post + w_20_post ≤ 0 ∧ w_20_post − w_20_post ≤ 0 ∧ − w_20_1 + w_20_1 ≤ 0 ∧ w_20_1 − w_20_1 ≤ 0 ∧ − w_20_0 + w_20_0 ≤ 0 ∧ w_20_0 − w_20_0 ≤ 0 ∧ − tmp_31_post + tmp_31_post ≤ 0 ∧ tmp_31_post − tmp_31_post ≤ 0 ∧ − tmp_31_0 + tmp_31_0 ≤ 0 ∧ tmp_31_0 − tmp_31_0 ≤ 0 ∧ − temp_32_post + temp_32_post ≤ 0 ∧ temp_32_post − temp_32_post ≤ 0 ∧ − temp_32_0 + temp_32_0 ≤ 0 ∧ temp_32_0 − temp_32_0 ≤ 0 ∧ − temp0_28_post + temp0_28_post ≤ 0 ∧ temp0_28_post − temp0_28_post ≤ 0 ∧ − temp0_28_1 + temp0_28_1 ≤ 0 ∧ temp0_28_1 − temp0_28_1 ≤ 0 ∧ − temp0_28_0 + temp0_28_0 ≤ 0 ∧ temp0_28_0 − temp0_28_0 ≤ 0 ∧ − temp0_18_0 + temp0_18_0 ≤ 0 ∧ temp0_18_0 − temp0_18_0 ≤ 0 ∧ − tail_15_post + tail_15_post ≤ 0 ∧ tail_15_post − tail_15_post ≤ 0 ∧ − tail_15_0 + tail_15_0 ≤ 0 ∧ tail_15_0 − tail_15_0 ≤ 0 ∧ − t_23_post + t_23_post ≤ 0 ∧ t_23_post − t_23_post ≤ 0 ∧ − t_23_0 + t_23_0 ≤ 0 ∧ t_23_0 − t_23_0 ≤ 0 ∧ − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0 ∧ − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 ≤ 0 ∧ − result_11_post + result_11_post ≤ 0 ∧ result_11_post − result_11_post ≤ 0 ∧ − result_11_2 + result_11_2 ≤ 0 ∧ result_11_2 − result_11_2 ≤ 0 ∧ − result_11_1 + result_11_1 ≤ 0 ∧ result_11_1 − result_11_1 ≤ 0 ∧ − result_11_0 + result_11_0 ≤ 0 ∧ result_11_0 − result_11_0 ≤ 0 ∧ − rcd_99_post + rcd_99_post ≤ 0 ∧ rcd_99_post − rcd_99_post ≤ 0 ∧ − rcd_99_0 + rcd_99_0 ≤ 0 ∧ rcd_99_0 − rcd_99_0 ≤ 0 ∧ − rcd_64_post + rcd_64_post ≤ 0 ∧ rcd_64_post − rcd_64_post ≤ 0 ∧ − rcd_64_0 + rcd_64_0 ≤ 0 ∧ rcd_64_0 − rcd_64_0 ≤ 0 ∧ − rcd_40_post + rcd_40_post ≤ 0 ∧ rcd_40_post − rcd_40_post ≤ 0 ∧ − rcd_40_0 + rcd_40_0 ≤ 0 ∧ rcd_40_0 − rcd_40_0 ≤ 0 ∧ − rcd_268_post + rcd_268_post ≤ 0 ∧ rcd_268_post − rcd_268_post ≤ 0 ∧ − rcd_268_0 + rcd_268_0 ≤ 0 ∧ rcd_268_0 − rcd_268_0 ≤ 0 ∧ − rcd_248_post + rcd_248_post ≤ 0 ∧ rcd_248_post − rcd_248_post ≤ 0 ∧ − rcd_248_0 + rcd_248_0 ≤ 0 ∧ rcd_248_0 − rcd_248_0 ≤ 0 ∧ − rcd_243_post + rcd_243_post ≤ 0 ∧ rcd_243_post − rcd_243_post ≤ 0 ∧ − rcd_243_0 + rcd_243_0 ≤ 0 ∧ rcd_243_0 − rcd_243_0 ≤ 0 ∧ − rcd_239_post + rcd_239_post ≤ 0 ∧ rcd_239_post − rcd_239_post ≤ 0 ∧ − rcd_239_0 + rcd_239_0 ≤ 0 ∧ rcd_239_0 − rcd_239_0 ≤ 0 ∧ − rcd_230_post + rcd_230_post ≤ 0 ∧ rcd_230_post − rcd_230_post ≤ 0 ∧ − rcd_230_0 + rcd_230_0 ≤ 0 ∧ rcd_230_0 − rcd_230_0 ≤ 0 ∧ − rcd_107_post + rcd_107_post ≤ 0 ∧ rcd_107_post − rcd_107_post ≤ 0 ∧ − rcd_107_0 + rcd_107_0 ≤ 0 ∧ rcd_107_0 − rcd_107_0 ≤ 0 ∧ − r_36_post + r_36_post ≤ 0 ∧ r_36_post − r_36_post ≤ 0 ∧ − r_36_0 + r_36_0 ≤ 0 ∧ r_36_0 − r_36_0 ≤ 0 ∧ − r_267_post + r_267_post ≤ 0 ∧ r_267_post − r_267_post ≤ 0 ∧ − r_267_0 + r_267_0 ≤ 0 ∧ r_267_0 − r_267_0 ≤ 0 ∧ − r_253_post + r_253_post ≤ 0 ∧ r_253_post − r_253_post ≤ 0 ∧ − r_253_0 + r_253_0 ≤ 0 ∧ r_253_0 − r_253_0 ≤ 0 ∧ − r_247_post + r_247_post ≤ 0 ∧ r_247_post − r_247_post ≤ 0 ∧ − r_247_0 + r_247_0 ≤ 0 ∧ r_247_0 − r_247_0 ≤ 0 ∧ − r_242_post + r_242_post ≤ 0 ∧ r_242_post − r_242_post ≤ 0 ∧ − r_242_0 + r_242_0 ≤ 0 ∧ r_242_0 − r_242_0 ≤ 0 ∧ − r_240_post + r_240_post ≤ 0 ∧ r_240_post − r_240_post ≤ 0 ∧ − r_240_0 + r_240_0 ≤ 0 ∧ r_240_0 − r_240_0 ≤ 0 ∧ − r_238_post + r_238_post ≤ 0 ∧ r_238_post − r_238_post ≤ 0 ∧ − r_238_0 + r_238_0 ≤ 0 ∧ r_238_0 − r_238_0 ≤ 0 ∧ − r_229_post + r_229_post ≤ 0 ∧ r_229_post − r_229_post ≤ 0 ∧ − r_229_0 + r_229_0 ≤ 0 ∧ r_229_0 − r_229_0 ≤ 0 ∧ − r_183_post + r_183_post ≤ 0 ∧ r_183_post − r_183_post ≤ 0 ∧ − r_183_0 + r_183_0 ≤ 0 ∧ r_183_0 − r_183_0 ≤ 0 ∧ − r_154_post + r_154_post ≤ 0 ∧ r_154_post − r_154_post ≤ 0 ∧ − r_154_0 + r_154_0 ≤ 0 ∧ r_154_0 − r_154_0 ≤ 0 ∧ − length_25_post + length_25_post ≤ 0 ∧ length_25_post − length_25_post ≤ 0 ∧ − length_25_0 + length_25_0 ≤ 0 ∧ length_25_0 − length_25_0 ≤ 0 ∧ − length_14_post + length_14_post ≤ 0 ∧ length_14_post − length_14_post ≤ 0 ∧ − length_14_1 + length_14_1 ≤ 0 ∧ length_14_1 − length_14_1 ≤ 0 ∧ − length_14_0 + length_14_0 ≤ 0 ∧ length_14_0 − length_14_0 ≤ 0 ∧ − len_270_post + len_270_post ≤ 0 ∧ len_270_post − len_270_post ≤ 0 ∧ − len_270_0 + len_270_0 ≤ 0 ∧ len_270_0 − len_270_0 ≤ 0 ∧ − len_200_post + len_200_post ≤ 0 ∧ len_200_post − len_200_post ≤ 0 ∧ − len_200_0 + len_200_0 ≤ 0 ∧ len_200_0 − len_200_0 ≤ 0 ∧ − i_27_post + i_27_post ≤ 0 ∧ i_27_post − i_27_post ≤ 0 ∧ − i_27_0 + i_27_0 ≤ 0 ∧ i_27_0 − i_27_0 ≤ 0 ∧ − i_114_post + i_114_post ≤ 0 ∧ i_114_post − i_114_post ≤ 0 ∧ − i_114_0 + i_114_0 ≤ 0 ∧ i_114_0 − i_114_0 ≤ 0 ∧ − i_105_post + i_105_post ≤ 0 ∧ i_105_post − i_105_post ≤ 0 ∧ − i_105_0 + i_105_0 ≤ 0 ∧ i_105_0 − i_105_0 ≤ 0 ∧ − head_SLAM_f_26_post + head_SLAM_f_26_post ≤ 0 ∧ head_SLAM_f_26_post − head_SLAM_f_26_post ≤ 0 ∧ − head_SLAM_f_26_0 + head_SLAM_f_26_0 ≤ 0 ∧ head_SLAM_f_26_0 − head_SLAM_f_26_0 ≤ 0 ∧ − head_29_post + head_29_post ≤ 0 ∧ head_29_post − head_29_post ≤ 0 ∧ − head_29_0 + head_29_0 ≤ 0 ∧ head_29_0 − head_29_0 ≤ 0 ∧ − head_13_post + head_13_post ≤ 0 ∧ head_13_post − head_13_post ≤ 0 ∧ − head_13_0 + head_13_0 ≤ 0 ∧ head_13_0 − head_13_0 ≤ 0 ∧ − a_271_post + a_271_post ≤ 0 ∧ a_271_post − a_271_post ≤ 0 ∧ − a_271_0 + a_271_0 ≤ 0 ∧ a_271_0 − a_271_0 ≤ 0 ∧ − a_215_post + a_215_post ≤ 0 ∧ a_215_post − a_215_post ≤ 0 ∧ − a_215_0 + a_215_0 ≤ 0 ∧ a_215_0 − a_215_0 ≤ 0 ∧ − a_168_post + a_168_post ≤ 0 ∧ a_168_post − a_168_post ≤ 0 ∧ − a_168_0 + a_168_0 ≤ 0 ∧ a_168_0 − a_168_0 ≤ 0 ∧ − a_143_post + a_143_post ≤ 0 ∧ a_143_post − a_143_post ≤ 0 ∧ − a_143_0 + a_143_0 ≤ 0 ∧ a_143_0 − a_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 ≤ 0 ∧ z_19_post − z_19_post ≤ 0 ∧ − z_19_1 + z_19_1 ≤ 0 ∧ z_19_1 − z_19_1 ≤ 0 ∧ − z_19_0 + z_19_0 ≤ 0 ∧ z_19_0 − z_19_0 ≤ 0 ∧ − y_347_post + y_347_post ≤ 0 ∧ y_347_post − y_347_post ≤ 0 ∧ − y_347_0 + y_347_0 ≤ 0 ∧ y_347_0 − y_347_0 ≤ 0 ∧ − y_295_post + y_295_post ≤ 0 ∧ y_295_post − y_295_post ≤ 0 ∧ − y_295_0 + y_295_0 ≤ 0 ∧ y_295_0 − y_295_0 ≤ 0 ∧ − y_290_post + y_290_post ≤ 0 ∧ y_290_post − y_290_post ≤ 0 ∧ − y_290_0 + y_290_0 ≤ 0 ∧ y_290_0 − y_290_0 ≤ 0 ∧ − y_285_post + y_285_post ≤ 0 ∧ y_285_post − y_285_post ≤ 0 ∧ − y_285_0 + y_285_0 ≤ 0 ∧ y_285_0 − y_285_0 ≤ 0 ∧ − y_269_post + y_269_post ≤ 0 ∧ y_269_post − y_269_post ≤ 0 ∧ − y_269_0 + y_269_0 ≤ 0 ∧ y_269_0 − y_269_0 ≤ 0 ∧ − y_261_post + y_261_post ≤ 0 ∧ y_261_post − y_261_post ≤ 0 ∧ − y_261_0 + y_261_0 ≤ 0 ∧ y_261_0 − y_261_0 ≤ 0 ∧ − y_241_post + y_241_post ≤ 0 ∧ y_241_post − y_241_post ≤ 0 ∧ − y_241_0 + y_241_0 ≤ 0 ∧ y_241_0 − y_241_0 ≤ 0 ∧ − y_231_post + y_231_post ≤ 0 ∧ y_231_post − y_231_post ≤ 0 ∧ − y_231_0 + y_231_0 ≤ 0 ∧ y_231_0 − y_231_0 ≤ 0 ∧ − y_22_post + y_22_post ≤ 0 ∧ y_22_post − y_22_post ≤ 0 ∧ − y_22_1 + y_22_1 ≤ 0 ∧ y_22_1 − y_22_1 ≤ 0 ∧ − y_22_0 + y_22_0 ≤ 0 ∧ y_22_0 − y_22_0 ≤ 0 ∧ − y_191_post + y_191_post ≤ 0 ∧ y_191_post − y_191_post ≤ 0 ∧ − y_191_0 + y_191_0 ≤ 0 ∧ y_191_0 − y_191_0 ≤ 0 ∧ − y_162_post + y_162_post ≤ 0 ∧ y_162_post − y_162_post ≤ 0 ∧ − y_162_0 + y_162_0 ≤ 0 ∧ y_162_0 − y_162_0 ≤ 0 ∧ − x_21_post + x_21_post ≤ 0 ∧ x_21_post − x_21_post ≤ 0 ∧ − x_21_1 + x_21_1 ≤ 0 ∧ x_21_1 − x_21_1 ≤ 0 ∧ − x_21_0 + x_21_0 ≤ 0 ∧ x_21_0 − x_21_0 ≤ 0 ∧ − w_20_post + w_20_post ≤ 0 ∧ w_20_post − w_20_post ≤ 0 ∧ − w_20_1 + w_20_1 ≤ 0 ∧ w_20_1 − w_20_1 ≤ 0 ∧ − w_20_0 + w_20_0 ≤ 0 ∧ w_20_0 − w_20_0 ≤ 0 ∧ − tmp_31_post + tmp_31_post ≤ 0 ∧ tmp_31_post − tmp_31_post ≤ 0 ∧ − tmp_31_0 + tmp_31_0 ≤ 0 ∧ tmp_31_0 − tmp_31_0 ≤ 0 ∧ − temp_32_post + temp_32_post ≤ 0 ∧ temp_32_post − temp_32_post ≤ 0 ∧ − temp_32_0 + temp_32_0 ≤ 0 ∧ temp_32_0 − temp_32_0 ≤ 0 ∧ − temp0_28_post + temp0_28_post ≤ 0 ∧ temp0_28_post − temp0_28_post ≤ 0 ∧ − temp0_28_1 + temp0_28_1 ≤ 0 ∧ temp0_28_1 − temp0_28_1 ≤ 0 ∧ − temp0_28_0 + temp0_28_0 ≤ 0 ∧ temp0_28_0 − temp0_28_0 ≤ 0 ∧ − temp0_18_0 + temp0_18_0 ≤ 0 ∧ temp0_18_0 − temp0_18_0 ≤ 0 ∧ − tail_15_post + tail_15_post ≤ 0 ∧ tail_15_post − tail_15_post ≤ 0 ∧ − tail_15_0 + tail_15_0 ≤ 0 ∧ tail_15_0 − tail_15_0 ≤ 0 ∧ − t_23_post + t_23_post ≤ 0 ∧ t_23_post − t_23_post ≤ 0 ∧ − t_23_0 + t_23_0 ≤ 0 ∧ t_23_0 − t_23_0 ≤ 0 ∧ − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0 ∧ − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 ≤ 0 ∧ − result_11_post + result_11_post ≤ 0 ∧ result_11_post − result_11_post ≤ 0 ∧ − result_11_2 + result_11_2 ≤ 0 ∧ result_11_2 − result_11_2 ≤ 0 ∧ − result_11_1 + result_11_1 ≤ 0 ∧ result_11_1 − result_11_1 ≤ 0 ∧ − result_11_0 + result_11_0 ≤ 0 ∧ result_11_0 − result_11_0 ≤ 0 ∧ − rcd_99_post + rcd_99_post ≤ 0 ∧ rcd_99_post − rcd_99_post ≤ 0 ∧ − rcd_99_0 + rcd_99_0 ≤ 0 ∧ rcd_99_0 − rcd_99_0 ≤ 0 ∧ − rcd_64_post + rcd_64_post ≤ 0 ∧ rcd_64_post − rcd_64_post ≤ 0 ∧ − rcd_64_0 + rcd_64_0 ≤ 0 ∧ rcd_64_0 − rcd_64_0 ≤ 0 ∧ − rcd_40_post + rcd_40_post ≤ 0 ∧ rcd_40_post − rcd_40_post ≤ 0 ∧ − rcd_40_0 + rcd_40_0 ≤ 0 ∧ rcd_40_0 − rcd_40_0 ≤ 0 ∧ − rcd_268_post + rcd_268_post ≤ 0 ∧ rcd_268_post − rcd_268_post ≤ 0 ∧ − rcd_268_0 + rcd_268_0 ≤ 0 ∧ rcd_268_0 − rcd_268_0 ≤ 0 ∧ − rcd_248_post + rcd_248_post ≤ 0 ∧ rcd_248_post − rcd_248_post ≤ 0 ∧ − rcd_248_0 + rcd_248_0 ≤ 0 ∧ rcd_248_0 − rcd_248_0 ≤ 0 ∧ − rcd_243_post + rcd_243_post ≤ 0 ∧ rcd_243_post − rcd_243_post ≤ 0 ∧ − rcd_243_0 + rcd_243_0 ≤ 0 ∧ rcd_243_0 − rcd_243_0 ≤ 0 ∧ − rcd_239_post + rcd_239_post ≤ 0 ∧ rcd_239_post − rcd_239_post ≤ 0 ∧ − rcd_239_0 + rcd_239_0 ≤ 0 ∧ rcd_239_0 − rcd_239_0 ≤ 0 ∧ − rcd_230_post + rcd_230_post ≤ 0 ∧ rcd_230_post − rcd_230_post ≤ 0 ∧ − rcd_230_0 + rcd_230_0 ≤ 0 ∧ rcd_230_0 − rcd_230_0 ≤ 0 ∧ − rcd_107_post + rcd_107_post ≤ 0 ∧ rcd_107_post − rcd_107_post ≤ 0 ∧ − rcd_107_0 + rcd_107_0 ≤ 0 ∧ rcd_107_0 − rcd_107_0 ≤ 0 ∧ − r_36_post + r_36_post ≤ 0 ∧ r_36_post − r_36_post ≤ 0 ∧ − r_36_0 + r_36_0 ≤ 0 ∧ r_36_0 − r_36_0 ≤ 0 ∧ − r_267_post + r_267_post ≤ 0 ∧ r_267_post − r_267_post ≤ 0 ∧ − r_267_0 + r_267_0 ≤ 0 ∧ r_267_0 − r_267_0 ≤ 0 ∧ − r_253_post + r_253_post ≤ 0 ∧ r_253_post − r_253_post ≤ 0 ∧ − r_253_0 + r_253_0 ≤ 0 ∧ r_253_0 − r_253_0 ≤ 0 ∧ − r_247_post + r_247_post ≤ 0 ∧ r_247_post − r_247_post ≤ 0 ∧ − r_247_0 + r_247_0 ≤ 0 ∧ r_247_0 − r_247_0 ≤ 0 ∧ − r_242_post + r_242_post ≤ 0 ∧ r_242_post − r_242_post ≤ 0 ∧ − r_242_0 + r_242_0 ≤ 0 ∧ r_242_0 − r_242_0 ≤ 0 ∧ − r_240_post + r_240_post ≤ 0 ∧ r_240_post − r_240_post ≤ 0 ∧ − r_240_0 + r_240_0 ≤ 0 ∧ r_240_0 − r_240_0 ≤ 0 ∧ − r_238_post + r_238_post ≤ 0 ∧ r_238_post − r_238_post ≤ 0 ∧ − r_238_0 + r_238_0 ≤ 0 ∧ r_238_0 − r_238_0 ≤ 0 ∧ − r_229_post + r_229_post ≤ 0 ∧ r_229_post − r_229_post ≤ 0 ∧ − r_229_0 + r_229_0 ≤ 0 ∧ r_229_0 − r_229_0 ≤ 0 ∧ − r_183_post + r_183_post ≤ 0 ∧ r_183_post − r_183_post ≤ 0 ∧ − r_183_0 + r_183_0 ≤ 0 ∧ r_183_0 − r_183_0 ≤ 0 ∧ − r_154_post + r_154_post ≤ 0 ∧ r_154_post − r_154_post ≤ 0 ∧ − r_154_0 + r_154_0 ≤ 0 ∧ r_154_0 − r_154_0 ≤ 0 ∧ − length_25_post + length_25_post ≤ 0 ∧ length_25_post − length_25_post ≤ 0 ∧ − length_25_0 + length_25_0 ≤ 0 ∧ length_25_0 − length_25_0 ≤ 0 ∧ − length_14_post + length_14_post ≤ 0 ∧ length_14_post − length_14_post ≤ 0 ∧ − length_14_1 + length_14_1 ≤ 0 ∧ length_14_1 − length_14_1 ≤ 0 ∧ − length_14_0 + length_14_0 ≤ 0 ∧ length_14_0 − length_14_0 ≤ 0 ∧ − len_270_post + len_270_post ≤ 0 ∧ len_270_post − len_270_post ≤ 0 ∧ − len_270_0 + len_270_0 ≤ 0 ∧ len_270_0 − len_270_0 ≤ 0 ∧ − len_200_post + len_200_post ≤ 0 ∧ len_200_post − len_200_post ≤ 0 ∧ − len_200_0 + len_200_0 ≤ 0 ∧ len_200_0 − len_200_0 ≤ 0 ∧ − i_27_post + i_27_post ≤ 0 ∧ i_27_post − i_27_post ≤ 0 ∧ − i_27_0 + i_27_0 ≤ 0 ∧ i_27_0 − i_27_0 ≤ 0 ∧ − i_114_post + i_114_post ≤ 0 ∧ i_114_post − i_114_post ≤ 0 ∧ − i_114_0 + i_114_0 ≤ 0 ∧ i_114_0 − i_114_0 ≤ 0 ∧ − i_105_post + i_105_post ≤ 0 ∧ i_105_post − i_105_post ≤ 0 ∧ − i_105_0 + i_105_0 ≤ 0 ∧ i_105_0 − i_105_0 ≤ 0 ∧ − head_SLAM_f_26_post + head_SLAM_f_26_post ≤ 0 ∧ head_SLAM_f_26_post − head_SLAM_f_26_post ≤ 0 ∧ − head_SLAM_f_26_0 + head_SLAM_f_26_0 ≤ 0 ∧ head_SLAM_f_26_0 − head_SLAM_f_26_0 ≤ 0 ∧ − head_29_post + head_29_post ≤ 0 ∧ head_29_post − head_29_post ≤ 0 ∧ − head_29_0 + head_29_0 ≤ 0 ∧ head_29_0 − head_29_0 ≤ 0 ∧ − head_13_post + head_13_post ≤ 0 ∧ head_13_post − head_13_post ≤ 0 ∧ − head_13_0 + head_13_0 ≤ 0 ∧ head_13_0 − head_13_0 ≤ 0 ∧ − a_271_post + a_271_post ≤ 0 ∧ a_271_post − a_271_post ≤ 0 ∧ − a_271_0 + a_271_0 ≤ 0 ∧ a_271_0 − a_271_0 ≤ 0 ∧ − a_215_post + a_215_post ≤ 0 ∧ a_215_post − a_215_post ≤ 0 ∧ − a_215_0 + a_215_0 ≤ 0 ∧ a_215_0 − a_215_0 ≤ 0 ∧ − a_168_post + a_168_post ≤ 0 ∧ a_168_post − a_168_post ≤ 0 ∧ − a_168_0 + a_168_0 ≤ 0 ∧ a_168_0 − a_168_0 ≤ 0 ∧ − a_143_post + a_143_post ≤ 0 ∧ a_143_post − a_143_post ≤ 0 ∧ − a_143_0 + a_143_0 ≤ 0 ∧ a_143_0 − a_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 ≤ 0 ∧ z_19_post − z_19_post ≤ 0 ∧ − z_19_1 + z_19_1 ≤ 0 ∧ z_19_1 − z_19_1 ≤ 0 ∧ − z_19_0 + z_19_0 ≤ 0 ∧ z_19_0 − z_19_0 ≤ 0 ∧ − y_347_post + y_347_post ≤ 0 ∧ y_347_post − y_347_post ≤ 0 ∧ − y_347_0 + y_347_0 ≤ 0 ∧ y_347_0 − y_347_0 ≤ 0 ∧ − y_295_post + y_295_post ≤ 0 ∧ y_295_post − y_295_post ≤ 0 ∧ − y_295_0 + y_295_0 ≤ 0 ∧ y_295_0 − y_295_0 ≤ 0 ∧ − y_290_post + y_290_post ≤ 0 ∧ y_290_post − y_290_post ≤ 0 ∧ − y_290_0 + y_290_0 ≤ 0 ∧ y_290_0 − y_290_0 ≤ 0 ∧ − y_285_post + y_285_post ≤ 0 ∧ y_285_post − y_285_post ≤ 0 ∧ − y_285_0 + y_285_0 ≤ 0 ∧ y_285_0 − y_285_0 ≤ 0 ∧ − y_269_post + y_269_post ≤ 0 ∧ y_269_post − y_269_post ≤ 0 ∧ − y_269_0 + y_269_0 ≤ 0 ∧ y_269_0 − y_269_0 ≤ 0 ∧ − y_261_post + y_261_post ≤ 0 ∧ y_261_post − y_261_post ≤ 0 ∧ − y_261_0 + y_261_0 ≤ 0 ∧ y_261_0 − y_261_0 ≤ 0 ∧ − y_241_post + y_241_post ≤ 0 ∧ y_241_post − y_241_post ≤ 0 ∧ − y_241_0 + y_241_0 ≤ 0 ∧ y_241_0 − y_241_0 ≤ 0 ∧ − y_231_post + y_231_post ≤ 0 ∧ y_231_post − y_231_post ≤ 0 ∧ − y_231_0 + y_231_0 ≤ 0 ∧ y_231_0 − y_231_0 ≤ 0 ∧ − y_22_post + y_22_post ≤ 0 ∧ y_22_post − y_22_post ≤ 0 ∧ − y_22_1 + y_22_1 ≤ 0 ∧ y_22_1 − y_22_1 ≤ 0 ∧ − y_22_0 + y_22_0 ≤ 0 ∧ y_22_0 − y_22_0 ≤ 0 ∧ − y_191_post + y_191_post ≤ 0 ∧ y_191_post − y_191_post ≤ 0 ∧ − y_191_0 + y_191_0 ≤ 0 ∧ y_191_0 − y_191_0 ≤ 0 ∧ − y_162_post + y_162_post ≤ 0 ∧ y_162_post − y_162_post ≤ 0 ∧ − y_162_0 + y_162_0 ≤ 0 ∧ y_162_0 − y_162_0 ≤ 0 ∧ − x_21_post + x_21_post ≤ 0 ∧ x_21_post − x_21_post ≤ 0 ∧ − x_21_1 + x_21_1 ≤ 0 ∧ x_21_1 − x_21_1 ≤ 0 ∧ − x_21_0 + x_21_0 ≤ 0 ∧ x_21_0 − x_21_0 ≤ 0 ∧ − w_20_post + w_20_post ≤ 0 ∧ w_20_post − w_20_post ≤ 0 ∧ − w_20_1 + w_20_1 ≤ 0 ∧ w_20_1 − w_20_1 ≤ 0 ∧ − w_20_0 + w_20_0 ≤ 0 ∧ w_20_0 − w_20_0 ≤ 0 ∧ − tmp_31_post + tmp_31_post ≤ 0 ∧ tmp_31_post − tmp_31_post ≤ 0 ∧ − tmp_31_0 + tmp_31_0 ≤ 0 ∧ tmp_31_0 − tmp_31_0 ≤ 0 ∧ − temp_32_post + temp_32_post ≤ 0 ∧ temp_32_post − temp_32_post ≤ 0 ∧ − temp_32_0 + temp_32_0 ≤ 0 ∧ temp_32_0 − temp_32_0 ≤ 0 ∧ − temp0_28_post + temp0_28_post ≤ 0 ∧ temp0_28_post − temp0_28_post ≤ 0 ∧ − temp0_28_1 + temp0_28_1 ≤ 0 ∧ temp0_28_1 − temp0_28_1 ≤ 0 ∧ − temp0_28_0 + temp0_28_0 ≤ 0 ∧ temp0_28_0 − temp0_28_0 ≤ 0 ∧ − temp0_18_0 + temp0_18_0 ≤ 0 ∧ temp0_18_0 − temp0_18_0 ≤ 0 ∧ − tail_15_post + tail_15_post ≤ 0 ∧ tail_15_post − tail_15_post ≤ 0 ∧ − tail_15_0 + tail_15_0 ≤ 0 ∧ tail_15_0 − tail_15_0 ≤ 0 ∧ − t_23_post + t_23_post ≤ 0 ∧ t_23_post − t_23_post ≤ 0 ∧ − t_23_0 + t_23_0 ≤ 0 ∧ t_23_0 − t_23_0 ≤ 0 ∧ − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0 ∧ − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 ≤ 0 ∧ − result_11_post + result_11_post ≤ 0 ∧ result_11_post − result_11_post ≤ 0 ∧ − result_11_2 + result_11_2 ≤ 0 ∧ result_11_2 − result_11_2 ≤ 0 ∧ − result_11_1 + result_11_1 ≤ 0 ∧ result_11_1 − result_11_1 ≤ 0 ∧ − result_11_0 + result_11_0 ≤ 0 ∧ result_11_0 − result_11_0 ≤ 0 ∧ − rcd_99_post + rcd_99_post ≤ 0 ∧ rcd_99_post − rcd_99_post ≤ 0 ∧ − rcd_99_0 + rcd_99_0 ≤ 0 ∧ rcd_99_0 − rcd_99_0 ≤ 0 ∧ − rcd_64_post + rcd_64_post ≤ 0 ∧ rcd_64_post − rcd_64_post ≤ 0 ∧ − rcd_64_0 + rcd_64_0 ≤ 0 ∧ rcd_64_0 − rcd_64_0 ≤ 0 ∧ − rcd_40_post + rcd_40_post ≤ 0 ∧ rcd_40_post − rcd_40_post ≤ 0 ∧ − rcd_40_0 + rcd_40_0 ≤ 0 ∧ rcd_40_0 − rcd_40_0 ≤ 0 ∧ − rcd_268_post + rcd_268_post ≤ 0 ∧ rcd_268_post − rcd_268_post ≤ 0 ∧ − rcd_268_0 + rcd_268_0 ≤ 0 ∧ rcd_268_0 − rcd_268_0 ≤ 0 ∧ − rcd_248_post + rcd_248_post ≤ 0 ∧ rcd_248_post − rcd_248_post ≤ 0 ∧ − rcd_248_0 + rcd_248_0 ≤ 0 ∧ rcd_248_0 − rcd_248_0 ≤ 0 ∧ − rcd_243_post + rcd_243_post ≤ 0 ∧ rcd_243_post − rcd_243_post ≤ 0 ∧ − rcd_243_0 + rcd_243_0 ≤ 0 ∧ rcd_243_0 − rcd_243_0 ≤ 0 ∧ − rcd_239_post + rcd_239_post ≤ 0 ∧ rcd_239_post − rcd_239_post ≤ 0 ∧ − rcd_239_0 + rcd_239_0 ≤ 0 ∧ rcd_239_0 − rcd_239_0 ≤ 0 ∧ − rcd_230_post + rcd_230_post ≤ 0 ∧ rcd_230_post − rcd_230_post ≤ 0 ∧ − rcd_230_0 + rcd_230_0 ≤ 0 ∧ rcd_230_0 − rcd_230_0 ≤ 0 ∧ − rcd_107_post + rcd_107_post ≤ 0 ∧ rcd_107_post − rcd_107_post ≤ 0 ∧ − rcd_107_0 + rcd_107_0 ≤ 0 ∧ rcd_107_0 − rcd_107_0 ≤ 0 ∧ − r_36_post + r_36_post ≤ 0 ∧ r_36_post − r_36_post ≤ 0 ∧ − r_36_0 + r_36_0 ≤ 0 ∧ r_36_0 − r_36_0 ≤ 0 ∧ − r_267_post + r_267_post ≤ 0 ∧ r_267_post − r_267_post ≤ 0 ∧ − r_267_0 + r_267_0 ≤ 0 ∧ r_267_0 − r_267_0 ≤ 0 ∧ − r_253_post + r_253_post ≤ 0 ∧ r_253_post − r_253_post ≤ 0 ∧ − r_253_0 + r_253_0 ≤ 0 ∧ r_253_0 − r_253_0 ≤ 0 ∧ − r_247_post + r_247_post ≤ 0 ∧ r_247_post − r_247_post ≤ 0 ∧ − r_247_0 + r_247_0 ≤ 0 ∧ r_247_0 − r_247_0 ≤ 0 ∧ − r_242_post + r_242_post ≤ 0 ∧ r_242_post − r_242_post ≤ 0 ∧ − r_242_0 + r_242_0 ≤ 0 ∧ r_242_0 − r_242_0 ≤ 0 ∧ − r_240_post + r_240_post ≤ 0 ∧ r_240_post − r_240_post ≤ 0 ∧ − r_240_0 + r_240_0 ≤ 0 ∧ r_240_0 − r_240_0 ≤ 0 ∧ − r_238_post + r_238_post ≤ 0 ∧ r_238_post − r_238_post ≤ 0 ∧ − r_238_0 + r_238_0 ≤ 0 ∧ r_238_0 − r_238_0 ≤ 0 ∧ − r_229_post + r_229_post ≤ 0 ∧ r_229_post − r_229_post ≤ 0 ∧ − r_229_0 + r_229_0 ≤ 0 ∧ r_229_0 − r_229_0 ≤ 0 ∧ − r_183_post + r_183_post ≤ 0 ∧ r_183_post − r_183_post ≤ 0 ∧ − r_183_0 + r_183_0 ≤ 0 ∧ r_183_0 − r_183_0 ≤ 0 ∧ − r_154_post + r_154_post ≤ 0 ∧ r_154_post − r_154_post ≤ 0 ∧ − r_154_0 + r_154_0 ≤ 0 ∧ r_154_0 − r_154_0 ≤ 0 ∧ − length_25_post + length_25_post ≤ 0 ∧ length_25_post − length_25_post ≤ 0 ∧ − length_25_0 + length_25_0 ≤ 0 ∧ length_25_0 − length_25_0 ≤ 0 ∧ − length_14_post + length_14_post ≤ 0 ∧ length_14_post − length_14_post ≤ 0 ∧ − length_14_1 + length_14_1 ≤ 0 ∧ length_14_1 − length_14_1 ≤ 0 ∧ − length_14_0 + length_14_0 ≤ 0 ∧ length_14_0 − length_14_0 ≤ 0 ∧ − len_270_post + len_270_post ≤ 0 ∧ len_270_post − len_270_post ≤ 0 ∧ − len_270_0 + len_270_0 ≤ 0 ∧ len_270_0 − len_270_0 ≤ 0 ∧ − len_200_post + len_200_post ≤ 0 ∧ len_200_post − len_200_post ≤ 0 ∧ − len_200_0 + len_200_0 ≤ 0 ∧ len_200_0 − len_200_0 ≤ 0 ∧ − i_27_post + i_27_post ≤ 0 ∧ i_27_post − i_27_post ≤ 0 ∧ − i_27_0 + i_27_0 ≤ 0 ∧ i_27_0 − i_27_0 ≤ 0 ∧ − i_114_post + i_114_post ≤ 0 ∧ i_114_post − i_114_post ≤ 0 ∧ − i_114_0 + i_114_0 ≤ 0 ∧ i_114_0 − i_114_0 ≤ 0 ∧ − i_105_post + i_105_post ≤ 0 ∧ i_105_post − i_105_post ≤ 0 ∧ − i_105_0 + i_105_0 ≤ 0 ∧ i_105_0 − i_105_0 ≤ 0 ∧ − head_SLAM_f_26_post + head_SLAM_f_26_post ≤ 0 ∧ head_SLAM_f_26_post − head_SLAM_f_26_post ≤ 0 ∧ − head_SLAM_f_26_0 + head_SLAM_f_26_0 ≤ 0 ∧ head_SLAM_f_26_0 − head_SLAM_f_26_0 ≤ 0 ∧ − head_29_post + head_29_post ≤ 0 ∧ head_29_post − head_29_post ≤ 0 ∧ − head_29_0 + head_29_0 ≤ 0 ∧ head_29_0 − head_29_0 ≤ 0 ∧ − head_13_post + head_13_post ≤ 0 ∧ head_13_post − head_13_post ≤ 0 ∧ − head_13_0 + head_13_0 ≤ 0 ∧ head_13_0 − head_13_0 ≤ 0 ∧ − a_271_post + a_271_post ≤ 0 ∧ a_271_post − a_271_post ≤ 0 ∧ − a_271_0 + a_271_0 ≤ 0 ∧ a_271_0 − a_271_0 ≤ 0 ∧ − a_215_post + a_215_post ≤ 0 ∧ a_215_post − a_215_post ≤ 0 ∧ − a_215_0 + a_215_0 ≤ 0 ∧ a_215_0 − a_215_0 ≤ 0 ∧ − a_168_post + a_168_post ≤ 0 ∧ a_168_post − a_168_post ≤ 0 ∧ − a_168_0 + a_168_0 ≤ 0 ∧ a_168_0 − a_168_0 ≤ 0 ∧ − a_143_post + a_143_post ≤ 0 ∧ a_143_post − a_143_post ≤ 0 ∧ − a_143_0 + a_143_0 ≤ 0 ∧ a_143_0 − a_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 ≤ 0 ∧ z_19_post − z_19_post ≤ 0 ∧ − z_19_1 + z_19_1 ≤ 0 ∧ z_19_1 − z_19_1 ≤ 0 ∧ − z_19_0 + z_19_0 ≤ 0 ∧ z_19_0 − z_19_0 ≤ 0 ∧ − y_347_post + y_347_post ≤ 0 ∧ y_347_post − y_347_post ≤ 0 ∧ − y_347_0 + y_347_0 ≤ 0 ∧ y_347_0 − y_347_0 ≤ 0 ∧ − y_295_post + y_295_post ≤ 0 ∧ y_295_post − y_295_post ≤ 0 ∧ − y_295_0 + y_295_0 ≤ 0 ∧ y_295_0 − y_295_0 ≤ 0 ∧ − y_290_post + y_290_post ≤ 0 ∧ y_290_post − y_290_post ≤ 0 ∧ − y_290_0 + y_290_0 ≤ 0 ∧ y_290_0 − y_290_0 ≤ 0 ∧ − y_285_post + y_285_post ≤ 0 ∧ y_285_post − y_285_post ≤ 0 ∧ − y_285_0 + y_285_0 ≤ 0 ∧ y_285_0 − y_285_0 ≤ 0 ∧ − y_269_post + y_269_post ≤ 0 ∧ y_269_post − y_269_post ≤ 0 ∧ − y_269_0 + y_269_0 ≤ 0 ∧ y_269_0 − y_269_0 ≤ 0 ∧ − y_261_post + y_261_post ≤ 0 ∧ y_261_post − y_261_post ≤ 0 ∧ − y_261_0 + y_261_0 ≤ 0 ∧ y_261_0 − y_261_0 ≤ 0 ∧ − y_241_post + y_241_post ≤ 0 ∧ y_241_post − y_241_post ≤ 0 ∧ − y_241_0 + y_241_0 ≤ 0 ∧ y_241_0 − y_241_0 ≤ 0 ∧ − y_231_post + y_231_post ≤ 0 ∧ y_231_post − y_231_post ≤ 0 ∧ − y_231_0 + y_231_0 ≤ 0 ∧ y_231_0 − y_231_0 ≤ 0 ∧ − y_22_post + y_22_post ≤ 0 ∧ y_22_post − y_22_post ≤ 0 ∧ − y_22_1 + y_22_1 ≤ 0 ∧ y_22_1 − y_22_1 ≤ 0 ∧ − y_22_0 + y_22_0 ≤ 0 ∧ y_22_0 − y_22_0 ≤ 0 ∧ − y_191_post + y_191_post ≤ 0 ∧ y_191_post − y_191_post ≤ 0 ∧ − y_191_0 + y_191_0 ≤ 0 ∧ y_191_0 − y_191_0 ≤ 0 ∧ − y_162_post + y_162_post ≤ 0 ∧ y_162_post − y_162_post ≤ 0 ∧ − y_162_0 + y_162_0 ≤ 0 ∧ y_162_0 − y_162_0 ≤ 0 ∧ − x_21_post + x_21_post ≤ 0 ∧ x_21_post − x_21_post ≤ 0 ∧ − x_21_1 + x_21_1 ≤ 0 ∧ x_21_1 − x_21_1 ≤ 0 ∧ − x_21_0 + x_21_0 ≤ 0 ∧ x_21_0 − x_21_0 ≤ 0 ∧ − w_20_post + w_20_post ≤ 0 ∧ w_20_post − w_20_post ≤ 0 ∧ − w_20_1 + w_20_1 ≤ 0 ∧ w_20_1 − w_20_1 ≤ 0 ∧ − w_20_0 + w_20_0 ≤ 0 ∧ w_20_0 − w_20_0 ≤ 0 ∧ − tmp_31_post + tmp_31_post ≤ 0 ∧ tmp_31_post − tmp_31_post ≤ 0 ∧ − tmp_31_0 + tmp_31_0 ≤ 0 ∧ tmp_31_0 − tmp_31_0 ≤ 0 ∧ − temp_32_post + temp_32_post ≤ 0 ∧ temp_32_post − temp_32_post ≤ 0 ∧ − temp_32_0 + temp_32_0 ≤ 0 ∧ temp_32_0 − temp_32_0 ≤ 0 ∧ − temp0_28_post + temp0_28_post ≤ 0 ∧ temp0_28_post − temp0_28_post ≤ 0 ∧ − temp0_28_1 + temp0_28_1 ≤ 0 ∧ temp0_28_1 − temp0_28_1 ≤ 0 ∧ − temp0_28_0 + temp0_28_0 ≤ 0 ∧ temp0_28_0 − temp0_28_0 ≤ 0 ∧ − temp0_18_0 + temp0_18_0 ≤ 0 ∧ temp0_18_0 − temp0_18_0 ≤ 0 ∧ − tail_15_post + tail_15_post ≤ 0 ∧ tail_15_post − tail_15_post ≤ 0 ∧ − tail_15_0 + tail_15_0 ≤ 0 ∧ tail_15_0 − tail_15_0 ≤ 0 ∧ − t_23_post + t_23_post ≤ 0 ∧ t_23_post − t_23_post ≤ 0 ∧ − t_23_0 + t_23_0 ≤ 0 ∧ t_23_0 − t_23_0 ≤ 0 ∧ − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0 ∧ − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 ≤ 0 ∧ − result_11_post + result_11_post ≤ 0 ∧ result_11_post − result_11_post ≤ 0 ∧ − result_11_2 + result_11_2 ≤ 0 ∧ result_11_2 − result_11_2 ≤ 0 ∧ − result_11_1 + result_11_1 ≤ 0 ∧ result_11_1 − result_11_1 ≤ 0 ∧ − result_11_0 + result_11_0 ≤ 0 ∧ result_11_0 − result_11_0 ≤ 0 ∧ − rcd_99_post + rcd_99_post ≤ 0 ∧ rcd_99_post − rcd_99_post ≤ 0 ∧ − rcd_99_0 + rcd_99_0 ≤ 0 ∧ rcd_99_0 − rcd_99_0 ≤ 0 ∧ − rcd_64_post + rcd_64_post ≤ 0 ∧ rcd_64_post − rcd_64_post ≤ 0 ∧ − rcd_64_0 + rcd_64_0 ≤ 0 ∧ rcd_64_0 − rcd_64_0 ≤ 0 ∧ − rcd_40_post + rcd_40_post ≤ 0 ∧ rcd_40_post − rcd_40_post ≤ 0 ∧ − rcd_40_0 + rcd_40_0 ≤ 0 ∧ rcd_40_0 − rcd_40_0 ≤ 0 ∧ − rcd_268_post + rcd_268_post ≤ 0 ∧ rcd_268_post − rcd_268_post ≤ 0 ∧ − rcd_268_0 + rcd_268_0 ≤ 0 ∧ rcd_268_0 − rcd_268_0 ≤ 0 ∧ − rcd_248_post + rcd_248_post ≤ 0 ∧ rcd_248_post − rcd_248_post ≤ 0 ∧ − rcd_248_0 + rcd_248_0 ≤ 0 ∧ rcd_248_0 − rcd_248_0 ≤ 0 ∧ − rcd_243_post + rcd_243_post ≤ 0 ∧ rcd_243_post − rcd_243_post ≤ 0 ∧ − rcd_243_0 + rcd_243_0 ≤ 0 ∧ rcd_243_0 − rcd_243_0 ≤ 0 ∧ − rcd_239_post + rcd_239_post ≤ 0 ∧ rcd_239_post − rcd_239_post ≤ 0 ∧ − rcd_239_0 + rcd_239_0 ≤ 0 ∧ rcd_239_0 − rcd_239_0 ≤ 0 ∧ − rcd_230_post + rcd_230_post ≤ 0 ∧ rcd_230_post − rcd_230_post ≤ 0 ∧ − rcd_230_0 + rcd_230_0 ≤ 0 ∧ rcd_230_0 − rcd_230_0 ≤ 0 ∧ − rcd_107_post + rcd_107_post ≤ 0 ∧ rcd_107_post − rcd_107_post ≤ 0 ∧ − rcd_107_0 + rcd_107_0 ≤ 0 ∧ rcd_107_0 − rcd_107_0 ≤ 0 ∧ − r_36_post + r_36_post ≤ 0 ∧ r_36_post − r_36_post ≤ 0 ∧ − r_36_0 + r_36_0 ≤ 0 ∧ r_36_0 − r_36_0 ≤ 0 ∧ − r_267_post + r_267_post ≤ 0 ∧ r_267_post − r_267_post ≤ 0 ∧ − r_267_0 + r_267_0 ≤ 0 ∧ r_267_0 − r_267_0 ≤ 0 ∧ − r_253_post + r_253_post ≤ 0 ∧ r_253_post − r_253_post ≤ 0 ∧ − r_253_0 + r_253_0 ≤ 0 ∧ r_253_0 − r_253_0 ≤ 0 ∧ − r_247_post + r_247_post ≤ 0 ∧ r_247_post − r_247_post ≤ 0 ∧ − r_247_0 + r_247_0 ≤ 0 ∧ r_247_0 − r_247_0 ≤ 0 ∧ − r_242_post + r_242_post ≤ 0 ∧ r_242_post − r_242_post ≤ 0 ∧ − r_242_0 + r_242_0 ≤ 0 ∧ r_242_0 − r_242_0 ≤ 0 ∧ − r_240_post + r_240_post ≤ 0 ∧ r_240_post − r_240_post ≤ 0 ∧ − r_240_0 + r_240_0 ≤ 0 ∧ r_240_0 − r_240_0 ≤ 0 ∧ − r_238_post + r_238_post ≤ 0 ∧ r_238_post − r_238_post ≤ 0 ∧ − r_238_0 + r_238_0 ≤ 0 ∧ r_238_0 − r_238_0 ≤ 0 ∧ − r_229_post + r_229_post ≤ 0 ∧ r_229_post − r_229_post ≤ 0 ∧ − r_229_0 + r_229_0 ≤ 0 ∧ r_229_0 − r_229_0 ≤ 0 ∧ − r_183_post + r_183_post ≤ 0 ∧ r_183_post − r_183_post ≤ 0 ∧ − r_183_0 + r_183_0 ≤ 0 ∧ r_183_0 − r_183_0 ≤ 0 ∧ − r_154_post + r_154_post ≤ 0 ∧ r_154_post − r_154_post ≤ 0 ∧ − r_154_0 + r_154_0 ≤ 0 ∧ r_154_0 − r_154_0 ≤ 0 ∧ − length_25_post + length_25_post ≤ 0 ∧ length_25_post − length_25_post ≤ 0 ∧ − length_25_0 + length_25_0 ≤ 0 ∧ length_25_0 − length_25_0 ≤ 0 ∧ − length_14_post + length_14_post ≤ 0 ∧ length_14_post − length_14_post ≤ 0 ∧ − length_14_1 + length_14_1 ≤ 0 ∧ length_14_1 − length_14_1 ≤ 0 ∧ − length_14_0 + length_14_0 ≤ 0 ∧ length_14_0 − length_14_0 ≤ 0 ∧ − len_270_post + len_270_post ≤ 0 ∧ len_270_post − len_270_post ≤ 0 ∧ − len_270_0 + len_270_0 ≤ 0 ∧ len_270_0 − len_270_0 ≤ 0 ∧ − len_200_post + len_200_post ≤ 0 ∧ len_200_post − len_200_post ≤ 0 ∧ − len_200_0 + len_200_0 ≤ 0 ∧ len_200_0 − len_200_0 ≤ 0 ∧ − i_27_post + i_27_post ≤ 0 ∧ i_27_post − i_27_post ≤ 0 ∧ − i_27_0 + i_27_0 ≤ 0 ∧ i_27_0 − i_27_0 ≤ 0 ∧ − i_114_post + i_114_post ≤ 0 ∧ i_114_post − i_114_post ≤ 0 ∧ − i_114_0 + i_114_0 ≤ 0 ∧ i_114_0 − i_114_0 ≤ 0 ∧ − i_105_post + i_105_post ≤ 0 ∧ i_105_post − i_105_post ≤ 0 ∧ − i_105_0 + i_105_0 ≤ 0 ∧ i_105_0 − i_105_0 ≤ 0 ∧ − head_SLAM_f_26_post + head_SLAM_f_26_post ≤ 0 ∧ head_SLAM_f_26_post − head_SLAM_f_26_post ≤ 0 ∧ − head_SLAM_f_26_0 + head_SLAM_f_26_0 ≤ 0 ∧ head_SLAM_f_26_0 − head_SLAM_f_26_0 ≤ 0 ∧ − head_29_post + head_29_post ≤ 0 ∧ head_29_post − head_29_post ≤ 0 ∧ − head_29_0 + head_29_0 ≤ 0 ∧ head_29_0 − head_29_0 ≤ 0 ∧ − head_13_post + head_13_post ≤ 0 ∧ head_13_post − head_13_post ≤ 0 ∧ − head_13_0 + head_13_0 ≤ 0 ∧ head_13_0 − head_13_0 ≤ 0 ∧ − a_271_post + a_271_post ≤ 0 ∧ a_271_post − a_271_post ≤ 0 ∧ − a_271_0 + a_271_0 ≤ 0 ∧ a_271_0 − a_271_0 ≤ 0 ∧ − a_215_post + a_215_post ≤ 0 ∧ a_215_post − a_215_post ≤ 0 ∧ − a_215_0 + a_215_0 ≤ 0 ∧ a_215_0 − a_215_0 ≤ 0 ∧ − a_168_post + a_168_post ≤ 0 ∧ a_168_post − a_168_post ≤ 0 ∧ − a_168_0 + a_168_0 ≤ 0 ∧ a_168_0 − a_168_0 ≤ 0 ∧ − a_143_post + a_143_post ≤ 0 ∧ a_143_post − a_143_post ≤ 0 ∧ − a_143_0 + a_143_0 ≤ 0 ∧ a_143_0 − a_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