LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Invariant Updates

The following invariants are asserted.

3: TRUE
9: 2 − len_14_0 ≤ 0 ∧ y_20_post ≤ 0 ∧ ct_18_1 ≤ 0 ∧ − ct_18_1 ≤ 0 ∧ ct_18_0 ≤ 0 ∧ − ct_18_0 ≤ 0 ∧ y_20_0 ≤ 0 ∧ − y_20_0 ≤ 0
10: TRUE
11: i_13_post ≤ 0 ∧ − i_13_post ≤ 0 ∧ x_15_post ≤ 0 ∧ − x_15_post ≤ 0 ∧ i_13_0 ≤ 0 ∧ − i_13_0 ≤ 0 ∧ x_15_0 ≤ 0 ∧ − x_15_0 ≤ 0
12: −1 + i_13_post ≤ 0 ∧ 1 − i_13_post ≤ 0 ∧ −1 + i_13_0 ≤ 0 ∧ 1 − i_13_0 ≤ 0 ∧ a_28_1 ≤ 0 ∧ d_29_1 ≤ 0 ∧ 1 − len_14_0 ≤ 0
13: a_28_1 ≤ 0 ∧ d_29_1 ≤ 0 ∧ y_20_post ≤ 0 ∧ − y_20_post ≤ 0 ∧ ct_18_1 ≤ 0 ∧ − ct_18_1 ≤ 0 ∧ y_20_0 ≤ 0 ∧ − y_20_0 ≤ 0
14: a_28_1 ≤ 0 ∧ d_29_1 ≤ 0 ∧ y_20_post ≤ 0 ∧ − y_20_post ≤ 0 ∧ ct_18_1 ≤ 0 ∧ − ct_18_1 ≤ 0 ∧ y_20_0 ≤ 0 ∧ − y_20_0 ≤ 0
15: −1 + i_13_0 ≤ 0 ∧ 1 − i_13_0 ≤ 0 ∧ a_28_1 ≤ 0 ∧ d_29_1 ≤ 0 ∧ −1 + len_14_0 ≤ 0 ∧ 1 − len_14_0 ≤ 0 ∧ y_20_post ≤ 0 ∧ − y_20_post ≤ 0 ∧ ct_18_1 ≤ 0 ∧ − ct_18_1 ≤ 0 ∧ ct_18_0 ≤ 0 ∧ − ct_18_0 ≤ 0 ∧ x_21_0 ≤ 0 ∧ − x_21_0 ≤ 0 ∧ y_20_0 ≤ 0 ∧ − y_20_0 ≤ 0
16: −1 + i_13_0 ≤ 0 ∧ 1 − i_13_0 ≤ 0 ∧ a_28_1 ≤ 0 ∧ d_29_1 ≤ 0 ∧ −1 + len_14_0 ≤ 0 ∧ 1 − len_14_0 ≤ 0 ∧ y_20_post ≤ 0 ∧ − y_20_post ≤ 0 ∧ ct_18_1 ≤ 0 ∧ − ct_18_1 ≤ 0 ∧ ct_18_0 ≤ 0 ∧ − ct_18_0 ≤ 0 ∧ x_21_0 ≤ 0 ∧ − x_21_0 ≤ 0 ∧ y_20_0 ≤ 0 ∧ − y_20_0 ≤ 0
17: −1 + i_13_0 ≤ 0 ∧ 1 − i_13_0 ≤ 0 ∧ a_28_1 ≤ 0 ∧ d_29_1 ≤ 0 ∧ −1 + len_14_0 ≤ 0 ∧ 1 − len_14_0 ≤ 0
18: 2 − len_14_0 ≤ 0
19: y_20_post ≤ 0 ∧ ct_18_1 ≤ 0 ∧ − ct_18_1 ≤ 0 ∧ y_20_0 ≤ 0 ∧ − y_20_0 ≤ 0 ∧ − a_152_0 ≤ 0
20: y_20_post ≤ 0 ∧ ct_18_1 ≤ 0 ∧ − ct_18_1 ≤ 0 ∧ y_20_0 ≤ 0 ∧ − y_20_0 ≤ 0 ∧ − a_152_0 ≤ 0
21: y_20_post ≤ 0 ∧ ct_18_1 ≤ 0 ∧ − ct_18_1 ≤ 0 ∧ ct_18_0 ≤ 0 ∧ − ct_18_0 ≤ 0 ∧ y_20_0 ≤ 0 ∧ − y_20_0 ≤ 0 ∧ − a_152_0 ≤ 0
22: y_20_post ≤ 0 ∧ ct_18_1 ≤ 0 ∧ − ct_18_1 ≤ 0 ∧ ct_18_0 ≤ 0 ∧ − ct_18_0 ≤ 0 ∧ y_20_0 ≤ 0 ∧ − y_20_0 ≤ 0 ∧ − a_152_0 ≤ 0
23: y_20_post ≤ 0 ∧ ct_18_1 ≤ 0 ∧ − ct_18_1 ≤ 0 ∧ ct_18_0 ≤ 0 ∧ − ct_18_0 ≤ 0 ∧ y_20_0 ≤ 0 ∧ − y_20_0 ≤ 0 ∧ − a_152_0 ≤ 0
24: 2 − len_14_0 ≤ 0 ∧ y_20_post ≤ 0 ∧ ct_18_1 ≤ 0 ∧ − ct_18_1 ≤ 0 ∧ ct_18_0 ≤ 0 ∧ − ct_18_0 ≤ 0 ∧ y_20_0 ≤ 0 ∧ − y_20_0 ≤ 0
25: y_20_post ≤ 0 ∧ ct_18_1 ≤ 0 ∧ − ct_18_1 ≤ 0 ∧ y_20_0 ≤ 0
26: y_20_post ≤ 0 ∧ ct_18_1 ≤ 0 ∧ − ct_18_1 ≤ 0 ∧ y_20_0 ≤ 0
27: y_20_post ≤ 0 ∧ ct_18_1 ≤ 0 ∧ − ct_18_1 ≤ 0 ∧ ct_18_0 ≤ 0 ∧ − ct_18_0 ≤ 0 ∧ y_20_0 ≤ 0 ∧ − y_20_0 ≤ 0
28: y_20_post ≤ 0 ∧ ct_18_1 ≤ 0 ∧ − ct_18_1 ≤ 0 ∧ ct_18_0 ≤ 0 ∧ − ct_18_0 ≤ 0 ∧ y_20_0 ≤ 0 ∧ − y_20_0 ≤ 0
29: y_20_post ≤ 0 ∧ ct_18_1 ≤ 0 ∧ − ct_18_1 ≤ 0 ∧ ct_18_0 ≤ 0 ∧ − ct_18_0 ≤ 0 ∧ y_20_0 ≤ 0 ∧ − y_20_0 ≤ 0
30: 2 − len_14_0 ≤ 0
31: TRUE

The invariants are proved as follows.

IMPACT Invariant Proof

2 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
9 49 9: − y_20_post + y_20_post ≤ 0 ∧ y_20_post − y_20_post ≤ 0 ∧ − y_20_2 + y_20_2 ≤ 0 ∧ y_20_2 − y_20_2 ≤ 0 ∧ − y_20_1 + y_20_1 ≤ 0 ∧ y_20_1 − y_20_1 ≤ 0 ∧ − y_20_0 + y_20_0 ≤ 0 ∧ y_20_0 − y_20_0 ≤ 0 ∧ − x_SLAM_f_19_post + x_SLAM_f_19_post ≤ 0 ∧ x_SLAM_f_19_post − x_SLAM_f_19_post ≤ 0 ∧ − x_SLAM_f_19_2 + x_SLAM_f_19_2 ≤ 0 ∧ x_SLAM_f_19_2 − x_SLAM_f_19_2 ≤ 0 ∧ − x_SLAM_f_19_1 + x_SLAM_f_19_1 ≤ 0 ∧ x_SLAM_f_19_1 − x_SLAM_f_19_1 ≤ 0 ∧ − x_SLAM_f_19_0 + x_SLAM_f_19_0 ≤ 0 ∧ x_SLAM_f_19_0 − x_SLAM_f_19_0 ≤ 0 ∧ − x_32_post + x_32_post ≤ 0 ∧ x_32_post − x_32_post ≤ 0 ∧ − x_32_1 + x_32_1 ≤ 0 ∧ x_32_1 − x_32_1 ≤ 0 ∧ − x_32_0 + x_32_0 ≤ 0 ∧ x_32_0 − x_32_0 ≤ 0 ∧ − x_21_post + x_21_post ≤ 0 ∧ x_21_post − x_21_post ≤ 0 ∧ − x_21_2 + x_21_2 ≤ 0 ∧ x_21_2 − x_21_2 ≤ 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 ∧ − x_17_post + x_17_post ≤ 0 ∧ x_17_post − x_17_post ≤ 0 ∧ − x_17_1 + x_17_1 ≤ 0 ∧ x_17_1 − x_17_1 ≤ 0 ∧ − x_17_0 + x_17_0 ≤ 0 ∧ x_17_0 − x_17_0 ≤ 0 ∧ − x_15_post + x_15_post ≤ 0 ∧ x_15_post − x_15_post ≤ 0 ∧ − x_15_0 + x_15_0 ≤ 0 ∧ x_15_0 − x_15_0 ≤ 0 ∧ − tmp_27_post + tmp_27_post ≤ 0 ∧ tmp_27_post − tmp_27_post ≤ 0 ∧ − tmp_27_1 + tmp_27_1 ≤ 0 ∧ tmp_27_1 − tmp_27_1 ≤ 0 ∧ − tmp_27_0 + tmp_27_0 ≤ 0 ∧ tmp_27_0 − tmp_27_0 ≤ 0 ∧ − temp_33_post + temp_33_post ≤ 0 ∧ temp_33_post − temp_33_post ≤ 0 ∧ − temp_33_1 + temp_33_1 ≤ 0 ∧ temp_33_1 − temp_33_1 ≤ 0 ∧ − temp_33_0 + temp_33_0 ≤ 0 ∧ temp_33_0 − temp_33_0 ≤ 0 ∧ − temp0_31_post + temp0_31_post ≤ 0 ∧ temp0_31_post − temp0_31_post ≤ 0 ∧ − temp0_31_1 + temp0_31_1 ≤ 0 ∧ temp0_31_1 − temp0_31_1 ≤ 0 ∧ − temp0_31_0 + temp0_31_0 ≤ 0 ∧ temp0_31_0 − temp0_31_0 ≤ 0 ∧ − temp0_16_0 + temp0_16_0 ≤ 0 ∧ temp0_16_0 − temp0_16_0 ≤ 0 ∧ − t_24_post + t_24_post ≤ 0 ∧ t_24_post − t_24_post ≤ 0 ∧ − t_24_1 + t_24_1 ≤ 0 ∧ t_24_1 − t_24_1 ≤ 0 ∧ − t_24_0 + t_24_0 ≤ 0 ∧ t_24_0 − t_24_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_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_63_post + rcd_63_post ≤ 0 ∧ rcd_63_post − rcd_63_post ≤ 0 ∧ − rcd_63_0 + rcd_63_0 ≤ 0 ∧ rcd_63_0 − rcd_63_0 ≤ 0 ∧ − rcd_100_post + rcd_100_post ≤ 0 ∧ rcd_100_post − rcd_100_post ≤ 0 ∧ − rcd_100_0 + rcd_100_0 ≤ 0 ∧ rcd_100_0 − rcd_100_0 ≤ 0 ∧ − r_37_post + r_37_post ≤ 0 ∧ r_37_post − r_37_post ≤ 0 ∧ − r_37_0 + r_37_0 ≤ 0 ∧ r_37_0 − r_37_0 ≤ 0 ∧ − len_14_post + len_14_post ≤ 0 ∧ len_14_post − len_14_post ≤ 0 ∧ − len_14_0 + len_14_0 ≤ 0 ∧ len_14_0 − len_14_0 ≤ 0 ∧ − i_13_post + i_13_post ≤ 0 ∧ i_13_post − i_13_post ≤ 0 ∧ − i_13_0 + i_13_0 ≤ 0 ∧ i_13_0 − i_13_0 ≤ 0 ∧ − i_111_post + i_111_post ≤ 0 ∧ i_111_post − i_111_post ≤ 0 ∧ − i_111_0 + i_111_0 ≤ 0 ∧ i_111_0 − i_111_0 ≤ 0 ∧ − d_29_post + d_29_post ≤ 0 ∧ d_29_post − d_29_post ≤ 0 ∧ − d_29_1 + d_29_1 ≤ 0 ∧ d_29_1 − d_29_1 ≤ 0 ∧ − d_29_0 + d_29_0 ≤ 0 ∧ d_29_0 − d_29_0 ≤ 0 ∧ − ct_18_post + ct_18_post ≤ 0 ∧ ct_18_post − ct_18_post ≤ 0 ∧ − ct_18_2 + ct_18_2 ≤ 0 ∧ ct_18_2 − ct_18_2 ≤ 0 ∧ − ct_18_1 + ct_18_1 ≤ 0 ∧ ct_18_1 − ct_18_1 ≤ 0 ∧ − ct_18_0 + ct_18_0 ≤ 0 ∧ ct_18_0 − ct_18_0 ≤ 0 ∧ − a_28_post + a_28_post ≤ 0 ∧ a_28_post − a_28_post ≤ 0 ∧ − a_28_1 + a_28_1 ≤ 0 ∧ a_28_1 − a_28_1 ≤ 0 ∧ − a_28_0 + a_28_0 ≤ 0 ∧ a_28_0 − a_28_0 ≤ 0 ∧ − a_175_post + a_175_post ≤ 0 ∧ a_175_post − a_175_post ≤ 0 ∧ − a_175_0 + a_175_0 ≤ 0 ∧ a_175_0 − a_175_0 ≤ 0 ∧ − a_152_post + a_152_post ≤ 0 ∧ a_152_post − a_152_post ≤ 0 ∧ − a_152_0 + a_152_0 ≤ 0 ∧ a_152_0 − a_152_0 ≤ 0 ∧ − a_130_post + a_130_post ≤ 0 ∧ a_130_post − a_130_post ≤ 0 ∧ − a_130_0 + a_130_0 ≤ 0 ∧ a_130_0 − a_130_0 ≤ 0
18 56 18: − y_20_post + y_20_post ≤ 0 ∧ y_20_post − y_20_post ≤ 0 ∧ − y_20_2 + y_20_2 ≤ 0 ∧ y_20_2 − y_20_2 ≤ 0 ∧ − y_20_1 + y_20_1 ≤ 0 ∧ y_20_1 − y_20_1 ≤ 0 ∧ − y_20_0 + y_20_0 ≤ 0 ∧ y_20_0 − y_20_0 ≤ 0 ∧ − x_SLAM_f_19_post + x_SLAM_f_19_post ≤ 0 ∧ x_SLAM_f_19_post − x_SLAM_f_19_post ≤ 0 ∧ − x_SLAM_f_19_2 + x_SLAM_f_19_2 ≤ 0 ∧ x_SLAM_f_19_2 − x_SLAM_f_19_2 ≤ 0 ∧ − x_SLAM_f_19_1 + x_SLAM_f_19_1 ≤ 0 ∧ x_SLAM_f_19_1 − x_SLAM_f_19_1 ≤ 0 ∧ − x_SLAM_f_19_0 + x_SLAM_f_19_0 ≤ 0 ∧ x_SLAM_f_19_0 − x_SLAM_f_19_0 ≤ 0 ∧ − x_32_post + x_32_post ≤ 0 ∧ x_32_post − x_32_post ≤ 0 ∧ − x_32_1 + x_32_1 ≤ 0 ∧ x_32_1 − x_32_1 ≤ 0 ∧ − x_32_0 + x_32_0 ≤ 0 ∧ x_32_0 − x_32_0 ≤ 0 ∧ − x_21_post + x_21_post ≤ 0 ∧ x_21_post − x_21_post ≤ 0 ∧ − x_21_2 + x_21_2 ≤ 0 ∧ x_21_2 − x_21_2 ≤ 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 ∧ − x_17_post + x_17_post ≤ 0 ∧ x_17_post − x_17_post ≤ 0 ∧ − x_17_1 + x_17_1 ≤ 0 ∧ x_17_1 − x_17_1 ≤ 0 ∧ − x_17_0 + x_17_0 ≤ 0 ∧ x_17_0 − x_17_0 ≤ 0 ∧ − x_15_post + x_15_post ≤ 0 ∧ x_15_post − x_15_post ≤ 0 ∧ − x_15_0 + x_15_0 ≤ 0 ∧ x_15_0 − x_15_0 ≤ 0 ∧ − tmp_27_post + tmp_27_post ≤ 0 ∧ tmp_27_post − tmp_27_post ≤ 0 ∧ − tmp_27_1 + tmp_27_1 ≤ 0 ∧ tmp_27_1 − tmp_27_1 ≤ 0 ∧ − tmp_27_0 + tmp_27_0 ≤ 0 ∧ tmp_27_0 − tmp_27_0 ≤ 0 ∧ − temp_33_post + temp_33_post ≤ 0 ∧ temp_33_post − temp_33_post ≤ 0 ∧ − temp_33_1 + temp_33_1 ≤ 0 ∧ temp_33_1 − temp_33_1 ≤ 0 ∧ − temp_33_0 + temp_33_0 ≤ 0 ∧ temp_33_0 − temp_33_0 ≤ 0 ∧ − temp0_31_post + temp0_31_post ≤ 0 ∧ temp0_31_post − temp0_31_post ≤ 0 ∧ − temp0_31_1 + temp0_31_1 ≤ 0 ∧ temp0_31_1 − temp0_31_1 ≤ 0 ∧ − temp0_31_0 + temp0_31_0 ≤ 0 ∧ temp0_31_0 − temp0_31_0 ≤ 0 ∧ − temp0_16_0 + temp0_16_0 ≤ 0 ∧ temp0_16_0 − temp0_16_0 ≤ 0 ∧ − t_24_post + t_24_post ≤ 0 ∧ t_24_post − t_24_post ≤ 0 ∧ − t_24_1 + t_24_1 ≤ 0 ∧ t_24_1 − t_24_1 ≤ 0 ∧ − t_24_0 + t_24_0 ≤ 0 ∧ t_24_0 − t_24_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_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_63_post + rcd_63_post ≤ 0 ∧ rcd_63_post − rcd_63_post ≤ 0 ∧ − rcd_63_0 + rcd_63_0 ≤ 0 ∧ rcd_63_0 − rcd_63_0 ≤ 0 ∧ − rcd_100_post + rcd_100_post ≤ 0 ∧ rcd_100_post − rcd_100_post ≤ 0 ∧ − rcd_100_0 + rcd_100_0 ≤ 0 ∧ rcd_100_0 − rcd_100_0 ≤ 0 ∧ − r_37_post + r_37_post ≤ 0 ∧ r_37_post − r_37_post ≤ 0 ∧ − r_37_0 + r_37_0 ≤ 0 ∧ r_37_0 − r_37_0 ≤ 0 ∧ − len_14_post + len_14_post ≤ 0 ∧ len_14_post − len_14_post ≤ 0 ∧ − len_14_0 + len_14_0 ≤ 0 ∧ len_14_0 − len_14_0 ≤ 0 ∧ − i_13_post + i_13_post ≤ 0 ∧ i_13_post − i_13_post ≤ 0 ∧ − i_13_0 + i_13_0 ≤ 0 ∧ i_13_0 − i_13_0 ≤ 0 ∧ − i_111_post + i_111_post ≤ 0 ∧ i_111_post − i_111_post ≤ 0 ∧ − i_111_0 + i_111_0 ≤ 0 ∧ i_111_0 − i_111_0 ≤ 0 ∧ − d_29_post + d_29_post ≤ 0 ∧ d_29_post − d_29_post ≤ 0 ∧ − d_29_1 + d_29_1 ≤ 0 ∧ d_29_1 − d_29_1 ≤ 0 ∧ − d_29_0 + d_29_0 ≤ 0 ∧ d_29_0 − d_29_0 ≤ 0 ∧ − ct_18_post + ct_18_post ≤ 0 ∧ ct_18_post − ct_18_post ≤ 0 ∧ − ct_18_2 + ct_18_2 ≤ 0 ∧ ct_18_2 − ct_18_2 ≤ 0 ∧ − ct_18_1 + ct_18_1 ≤ 0 ∧ ct_18_1 − ct_18_1 ≤ 0 ∧ − ct_18_0 + ct_18_0 ≤ 0 ∧ ct_18_0 − ct_18_0 ≤ 0 ∧ − a_28_post + a_28_post ≤ 0 ∧ a_28_post − a_28_post ≤ 0 ∧ − a_28_1 + a_28_1 ≤ 0 ∧ a_28_1 − a_28_1 ≤ 0 ∧ − a_28_0 + a_28_0 ≤ 0 ∧ a_28_0 − a_28_0 ≤ 0 ∧ − a_175_post + a_175_post ≤ 0 ∧ a_175_post − a_175_post ≤ 0 ∧ − a_175_0 + a_175_0 ≤ 0 ∧ a_175_0 − a_175_0 ≤ 0 ∧ − a_152_post + a_152_post ≤ 0 ∧ a_152_post − a_152_post ≤ 0 ∧ − a_152_0 + a_152_0 ≤ 0 ∧ a_152_0 − a_152_0 ≤ 0 ∧ − a_130_post + a_130_post ≤ 0 ∧ a_130_post − a_130_post ≤ 0 ∧ − a_130_0 + a_130_0 ≤ 0 ∧ a_130_0 − a_130_0 ≤ 0
and for every transition t, a duplicate t is considered.

3 Transition Removal

We remove transitions 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 35, 36, 37, 38, 39, 40, 41, 42, 43, 46, 47, 48 using the following ranking functions, which are bounded by −41.

31: 0
10: 0
11: 0
12: 0
13: 0
14: 0
15: 0
16: 0
17: 0
18: 0
30: 0
25: 0
26: 0
27: 0
28: 0
29: 0
9: 0
19: 0
20: 0
21: 0
22: 0
23: 0
24: 0
3: 0
31: −18
10: −19
11: −20
12: −21
13: −22
14: −23
15: −24
16: −25
17: −26
18: −27
30: −27
18_var_snapshot: −27
18*: −27
25: −30
26: −31
27: −32
28: −33
29: −34
9: −35
19: −35
20: −35
21: −35
22: −35
23: −35
24: −35
9_var_snapshot: −35
9*: −35
3: −39

4 Location Addition

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

9* 52 9: − y_20_post + y_20_post ≤ 0 ∧ y_20_post − y_20_post ≤ 0 ∧ − y_20_2 + y_20_2 ≤ 0 ∧ y_20_2 − y_20_2 ≤ 0 ∧ − y_20_1 + y_20_1 ≤ 0 ∧ y_20_1 − y_20_1 ≤ 0 ∧ − y_20_0 + y_20_0 ≤ 0 ∧ y_20_0 − y_20_0 ≤ 0 ∧ − x_SLAM_f_19_post + x_SLAM_f_19_post ≤ 0 ∧ x_SLAM_f_19_post − x_SLAM_f_19_post ≤ 0 ∧ − x_SLAM_f_19_2 + x_SLAM_f_19_2 ≤ 0 ∧ x_SLAM_f_19_2 − x_SLAM_f_19_2 ≤ 0 ∧ − x_SLAM_f_19_1 + x_SLAM_f_19_1 ≤ 0 ∧ x_SLAM_f_19_1 − x_SLAM_f_19_1 ≤ 0 ∧ − x_SLAM_f_19_0 + x_SLAM_f_19_0 ≤ 0 ∧ x_SLAM_f_19_0 − x_SLAM_f_19_0 ≤ 0 ∧ − x_32_post + x_32_post ≤ 0 ∧ x_32_post − x_32_post ≤ 0 ∧ − x_32_1 + x_32_1 ≤ 0 ∧ x_32_1 − x_32_1 ≤ 0 ∧ − x_32_0 + x_32_0 ≤ 0 ∧ x_32_0 − x_32_0 ≤ 0 ∧ − x_21_post + x_21_post ≤ 0 ∧ x_21_post − x_21_post ≤ 0 ∧ − x_21_2 + x_21_2 ≤ 0 ∧ x_21_2 − x_21_2 ≤ 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 ∧ − x_17_post + x_17_post ≤ 0 ∧ x_17_post − x_17_post ≤ 0 ∧ − x_17_1 + x_17_1 ≤ 0 ∧ x_17_1 − x_17_1 ≤ 0 ∧ − x_17_0 + x_17_0 ≤ 0 ∧ x_17_0 − x_17_0 ≤ 0 ∧ − x_15_post + x_15_post ≤ 0 ∧ x_15_post − x_15_post ≤ 0 ∧ − x_15_0 + x_15_0 ≤ 0 ∧ x_15_0 − x_15_0 ≤ 0 ∧ − tmp_27_post + tmp_27_post ≤ 0 ∧ tmp_27_post − tmp_27_post ≤ 0 ∧ − tmp_27_1 + tmp_27_1 ≤ 0 ∧ tmp_27_1 − tmp_27_1 ≤ 0 ∧ − tmp_27_0 + tmp_27_0 ≤ 0 ∧ tmp_27_0 − tmp_27_0 ≤ 0 ∧ − temp_33_post + temp_33_post ≤ 0 ∧ temp_33_post − temp_33_post ≤ 0 ∧ − temp_33_1 + temp_33_1 ≤ 0 ∧ temp_33_1 − temp_33_1 ≤ 0 ∧ − temp_33_0 + temp_33_0 ≤ 0 ∧ temp_33_0 − temp_33_0 ≤ 0 ∧ − temp0_31_post + temp0_31_post ≤ 0 ∧ temp0_31_post − temp0_31_post ≤ 0 ∧ − temp0_31_1 + temp0_31_1 ≤ 0 ∧ temp0_31_1 − temp0_31_1 ≤ 0 ∧ − temp0_31_0 + temp0_31_0 ≤ 0 ∧ temp0_31_0 − temp0_31_0 ≤ 0 ∧ − temp0_16_0 + temp0_16_0 ≤ 0 ∧ temp0_16_0 − temp0_16_0 ≤ 0 ∧ − t_24_post + t_24_post ≤ 0 ∧ t_24_post − t_24_post ≤ 0 ∧ − t_24_1 + t_24_1 ≤ 0 ∧ t_24_1 − t_24_1 ≤ 0 ∧ − t_24_0 + t_24_0 ≤ 0 ∧ t_24_0 − t_24_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_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_63_post + rcd_63_post ≤ 0 ∧ rcd_63_post − rcd_63_post ≤ 0 ∧ − rcd_63_0 + rcd_63_0 ≤ 0 ∧ rcd_63_0 − rcd_63_0 ≤ 0 ∧ − rcd_100_post + rcd_100_post ≤ 0 ∧ rcd_100_post − rcd_100_post ≤ 0 ∧ − rcd_100_0 + rcd_100_0 ≤ 0 ∧ rcd_100_0 − rcd_100_0 ≤ 0 ∧ − r_37_post + r_37_post ≤ 0 ∧ r_37_post − r_37_post ≤ 0 ∧ − r_37_0 + r_37_0 ≤ 0 ∧ r_37_0 − r_37_0 ≤ 0 ∧ − len_14_post + len_14_post ≤ 0 ∧ len_14_post − len_14_post ≤ 0 ∧ − len_14_0 + len_14_0 ≤ 0 ∧ len_14_0 − len_14_0 ≤ 0 ∧ − i_13_post + i_13_post ≤ 0 ∧ i_13_post − i_13_post ≤ 0 ∧ − i_13_0 + i_13_0 ≤ 0 ∧ i_13_0 − i_13_0 ≤ 0 ∧ − i_111_post + i_111_post ≤ 0 ∧ i_111_post − i_111_post ≤ 0 ∧ − i_111_0 + i_111_0 ≤ 0 ∧ i_111_0 − i_111_0 ≤ 0 ∧ − d_29_post + d_29_post ≤ 0 ∧ d_29_post − d_29_post ≤ 0 ∧ − d_29_1 + d_29_1 ≤ 0 ∧ d_29_1 − d_29_1 ≤ 0 ∧ − d_29_0 + d_29_0 ≤ 0 ∧ d_29_0 − d_29_0 ≤ 0 ∧ − ct_18_post + ct_18_post ≤ 0 ∧ ct_18_post − ct_18_post ≤ 0 ∧ − ct_18_2 + ct_18_2 ≤ 0 ∧ ct_18_2 − ct_18_2 ≤ 0 ∧ − ct_18_1 + ct_18_1 ≤ 0 ∧ ct_18_1 − ct_18_1 ≤ 0 ∧ − ct_18_0 + ct_18_0 ≤ 0 ∧ ct_18_0 − ct_18_0 ≤ 0 ∧ − a_28_post + a_28_post ≤ 0 ∧ a_28_post − a_28_post ≤ 0 ∧ − a_28_1 + a_28_1 ≤ 0 ∧ a_28_1 − a_28_1 ≤ 0 ∧ − a_28_0 + a_28_0 ≤ 0 ∧ a_28_0 − a_28_0 ≤ 0 ∧ − a_175_post + a_175_post ≤ 0 ∧ a_175_post − a_175_post ≤ 0 ∧ − a_175_0 + a_175_0 ≤ 0 ∧ a_175_0 − a_175_0 ≤ 0 ∧ − a_152_post + a_152_post ≤ 0 ∧ a_152_post − a_152_post ≤ 0 ∧ − a_152_0 + a_152_0 ≤ 0 ∧ a_152_0 − a_152_0 ≤ 0 ∧ − a_130_post + a_130_post ≤ 0 ∧ a_130_post − a_130_post ≤ 0 ∧ − a_130_0 + a_130_0 ≤ 0 ∧ a_130_0 − a_130_0 ≤ 0

5 Location Addition

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

9 50 9_var_snapshot: − y_20_post + y_20_post ≤ 0 ∧ y_20_post − y_20_post ≤ 0 ∧ − y_20_2 + y_20_2 ≤ 0 ∧ y_20_2 − y_20_2 ≤ 0 ∧ − y_20_1 + y_20_1 ≤ 0 ∧ y_20_1 − y_20_1 ≤ 0 ∧ − y_20_0 + y_20_0 ≤ 0 ∧ y_20_0 − y_20_0 ≤ 0 ∧ − x_SLAM_f_19_post + x_SLAM_f_19_post ≤ 0 ∧ x_SLAM_f_19_post − x_SLAM_f_19_post ≤ 0 ∧ − x_SLAM_f_19_2 + x_SLAM_f_19_2 ≤ 0 ∧ x_SLAM_f_19_2 − x_SLAM_f_19_2 ≤ 0 ∧ − x_SLAM_f_19_1 + x_SLAM_f_19_1 ≤ 0 ∧ x_SLAM_f_19_1 − x_SLAM_f_19_1 ≤ 0 ∧ − x_SLAM_f_19_0 + x_SLAM_f_19_0 ≤ 0 ∧ x_SLAM_f_19_0 − x_SLAM_f_19_0 ≤ 0 ∧ − x_32_post + x_32_post ≤ 0 ∧ x_32_post − x_32_post ≤ 0 ∧ − x_32_1 + x_32_1 ≤ 0 ∧ x_32_1 − x_32_1 ≤ 0 ∧ − x_32_0 + x_32_0 ≤ 0 ∧ x_32_0 − x_32_0 ≤ 0 ∧ − x_21_post + x_21_post ≤ 0 ∧ x_21_post − x_21_post ≤ 0 ∧ − x_21_2 + x_21_2 ≤ 0 ∧ x_21_2 − x_21_2 ≤ 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 ∧ − x_17_post + x_17_post ≤ 0 ∧ x_17_post − x_17_post ≤ 0 ∧ − x_17_1 + x_17_1 ≤ 0 ∧ x_17_1 − x_17_1 ≤ 0 ∧ − x_17_0 + x_17_0 ≤ 0 ∧ x_17_0 − x_17_0 ≤ 0 ∧ − x_15_post + x_15_post ≤ 0 ∧ x_15_post − x_15_post ≤ 0 ∧ − x_15_0 + x_15_0 ≤ 0 ∧ x_15_0 − x_15_0 ≤ 0 ∧ − tmp_27_post + tmp_27_post ≤ 0 ∧ tmp_27_post − tmp_27_post ≤ 0 ∧ − tmp_27_1 + tmp_27_1 ≤ 0 ∧ tmp_27_1 − tmp_27_1 ≤ 0 ∧ − tmp_27_0 + tmp_27_0 ≤ 0 ∧ tmp_27_0 − tmp_27_0 ≤ 0 ∧ − temp_33_post + temp_33_post ≤ 0 ∧ temp_33_post − temp_33_post ≤ 0 ∧ − temp_33_1 + temp_33_1 ≤ 0 ∧ temp_33_1 − temp_33_1 ≤ 0 ∧ − temp_33_0 + temp_33_0 ≤ 0 ∧ temp_33_0 − temp_33_0 ≤ 0 ∧ − temp0_31_post + temp0_31_post ≤ 0 ∧ temp0_31_post − temp0_31_post ≤ 0 ∧ − temp0_31_1 + temp0_31_1 ≤ 0 ∧ temp0_31_1 − temp0_31_1 ≤ 0 ∧ − temp0_31_0 + temp0_31_0 ≤ 0 ∧ temp0_31_0 − temp0_31_0 ≤ 0 ∧ − temp0_16_0 + temp0_16_0 ≤ 0 ∧ temp0_16_0 − temp0_16_0 ≤ 0 ∧ − t_24_post + t_24_post ≤ 0 ∧ t_24_post − t_24_post ≤ 0 ∧ − t_24_1 + t_24_1 ≤ 0 ∧ t_24_1 − t_24_1 ≤ 0 ∧ − t_24_0 + t_24_0 ≤ 0 ∧ t_24_0 − t_24_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_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_63_post + rcd_63_post ≤ 0 ∧ rcd_63_post − rcd_63_post ≤ 0 ∧ − rcd_63_0 + rcd_63_0 ≤ 0 ∧ rcd_63_0 − rcd_63_0 ≤ 0 ∧ − rcd_100_post + rcd_100_post ≤ 0 ∧ rcd_100_post − rcd_100_post ≤ 0 ∧ − rcd_100_0 + rcd_100_0 ≤ 0 ∧ rcd_100_0 − rcd_100_0 ≤ 0 ∧ − r_37_post + r_37_post ≤ 0 ∧ r_37_post − r_37_post ≤ 0 ∧ − r_37_0 + r_37_0 ≤ 0 ∧ r_37_0 − r_37_0 ≤ 0 ∧ − len_14_post + len_14_post ≤ 0 ∧ len_14_post − len_14_post ≤ 0 ∧ − len_14_0 + len_14_0 ≤ 0 ∧ len_14_0 − len_14_0 ≤ 0 ∧ − i_13_post + i_13_post ≤ 0 ∧ i_13_post − i_13_post ≤ 0 ∧ − i_13_0 + i_13_0 ≤ 0 ∧ i_13_0 − i_13_0 ≤ 0 ∧ − i_111_post + i_111_post ≤ 0 ∧ i_111_post − i_111_post ≤ 0 ∧ − i_111_0 + i_111_0 ≤ 0 ∧ i_111_0 − i_111_0 ≤ 0 ∧ − d_29_post + d_29_post ≤ 0 ∧ d_29_post − d_29_post ≤ 0 ∧ − d_29_1 + d_29_1 ≤ 0 ∧ d_29_1 − d_29_1 ≤ 0 ∧ − d_29_0 + d_29_0 ≤ 0 ∧ d_29_0 − d_29_0 ≤ 0 ∧ − ct_18_post + ct_18_post ≤ 0 ∧ ct_18_post − ct_18_post ≤ 0 ∧ − ct_18_2 + ct_18_2 ≤ 0 ∧ ct_18_2 − ct_18_2 ≤ 0 ∧ − ct_18_1 + ct_18_1 ≤ 0 ∧ ct_18_1 − ct_18_1 ≤ 0 ∧ − ct_18_0 + ct_18_0 ≤ 0 ∧ ct_18_0 − ct_18_0 ≤ 0 ∧ − a_28_post + a_28_post ≤ 0 ∧ a_28_post − a_28_post ≤ 0 ∧ − a_28_1 + a_28_1 ≤ 0 ∧ a_28_1 − a_28_1 ≤ 0 ∧ − a_28_0 + a_28_0 ≤ 0 ∧ a_28_0 − a_28_0 ≤ 0 ∧ − a_175_post + a_175_post ≤ 0 ∧ a_175_post − a_175_post ≤ 0 ∧ − a_175_0 + a_175_0 ≤ 0 ∧ a_175_0 − a_175_0 ≤ 0 ∧ − a_152_post + a_152_post ≤ 0 ∧ a_152_post − a_152_post ≤ 0 ∧ − a_152_0 + a_152_0 ≤ 0 ∧ a_152_0 − a_152_0 ≤ 0 ∧ − a_130_post + a_130_post ≤ 0 ∧ a_130_post − a_130_post ≤ 0 ∧ − a_130_0 + a_130_0 ≤ 0 ∧ a_130_0 − a_130_0 ≤ 0

6 Location Addition

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

18* 59 18: − y_20_post + y_20_post ≤ 0 ∧ y_20_post − y_20_post ≤ 0 ∧ − y_20_2 + y_20_2 ≤ 0 ∧ y_20_2 − y_20_2 ≤ 0 ∧ − y_20_1 + y_20_1 ≤ 0 ∧ y_20_1 − y_20_1 ≤ 0 ∧ − y_20_0 + y_20_0 ≤ 0 ∧ y_20_0 − y_20_0 ≤ 0 ∧ − x_SLAM_f_19_post + x_SLAM_f_19_post ≤ 0 ∧ x_SLAM_f_19_post − x_SLAM_f_19_post ≤ 0 ∧ − x_SLAM_f_19_2 + x_SLAM_f_19_2 ≤ 0 ∧ x_SLAM_f_19_2 − x_SLAM_f_19_2 ≤ 0 ∧ − x_SLAM_f_19_1 + x_SLAM_f_19_1 ≤ 0 ∧ x_SLAM_f_19_1 − x_SLAM_f_19_1 ≤ 0 ∧ − x_SLAM_f_19_0 + x_SLAM_f_19_0 ≤ 0 ∧ x_SLAM_f_19_0 − x_SLAM_f_19_0 ≤ 0 ∧ − x_32_post + x_32_post ≤ 0 ∧ x_32_post − x_32_post ≤ 0 ∧ − x_32_1 + x_32_1 ≤ 0 ∧ x_32_1 − x_32_1 ≤ 0 ∧ − x_32_0 + x_32_0 ≤ 0 ∧ x_32_0 − x_32_0 ≤ 0 ∧ − x_21_post + x_21_post ≤ 0 ∧ x_21_post − x_21_post ≤ 0 ∧ − x_21_2 + x_21_2 ≤ 0 ∧ x_21_2 − x_21_2 ≤ 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 ∧ − x_17_post + x_17_post ≤ 0 ∧ x_17_post − x_17_post ≤ 0 ∧ − x_17_1 + x_17_1 ≤ 0 ∧ x_17_1 − x_17_1 ≤ 0 ∧ − x_17_0 + x_17_0 ≤ 0 ∧ x_17_0 − x_17_0 ≤ 0 ∧ − x_15_post + x_15_post ≤ 0 ∧ x_15_post − x_15_post ≤ 0 ∧ − x_15_0 + x_15_0 ≤ 0 ∧ x_15_0 − x_15_0 ≤ 0 ∧ − tmp_27_post + tmp_27_post ≤ 0 ∧ tmp_27_post − tmp_27_post ≤ 0 ∧ − tmp_27_1 + tmp_27_1 ≤ 0 ∧ tmp_27_1 − tmp_27_1 ≤ 0 ∧ − tmp_27_0 + tmp_27_0 ≤ 0 ∧ tmp_27_0 − tmp_27_0 ≤ 0 ∧ − temp_33_post + temp_33_post ≤ 0 ∧ temp_33_post − temp_33_post ≤ 0 ∧ − temp_33_1 + temp_33_1 ≤ 0 ∧ temp_33_1 − temp_33_1 ≤ 0 ∧ − temp_33_0 + temp_33_0 ≤ 0 ∧ temp_33_0 − temp_33_0 ≤ 0 ∧ − temp0_31_post + temp0_31_post ≤ 0 ∧ temp0_31_post − temp0_31_post ≤ 0 ∧ − temp0_31_1 + temp0_31_1 ≤ 0 ∧ temp0_31_1 − temp0_31_1 ≤ 0 ∧ − temp0_31_0 + temp0_31_0 ≤ 0 ∧ temp0_31_0 − temp0_31_0 ≤ 0 ∧ − temp0_16_0 + temp0_16_0 ≤ 0 ∧ temp0_16_0 − temp0_16_0 ≤ 0 ∧ − t_24_post + t_24_post ≤ 0 ∧ t_24_post − t_24_post ≤ 0 ∧ − t_24_1 + t_24_1 ≤ 0 ∧ t_24_1 − t_24_1 ≤ 0 ∧ − t_24_0 + t_24_0 ≤ 0 ∧ t_24_0 − t_24_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_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_63_post + rcd_63_post ≤ 0 ∧ rcd_63_post − rcd_63_post ≤ 0 ∧ − rcd_63_0 + rcd_63_0 ≤ 0 ∧ rcd_63_0 − rcd_63_0 ≤ 0 ∧ − rcd_100_post + rcd_100_post ≤ 0 ∧ rcd_100_post − rcd_100_post ≤ 0 ∧ − rcd_100_0 + rcd_100_0 ≤ 0 ∧ rcd_100_0 − rcd_100_0 ≤ 0 ∧ − r_37_post + r_37_post ≤ 0 ∧ r_37_post − r_37_post ≤ 0 ∧ − r_37_0 + r_37_0 ≤ 0 ∧ r_37_0 − r_37_0 ≤ 0 ∧ − len_14_post + len_14_post ≤ 0 ∧ len_14_post − len_14_post ≤ 0 ∧ − len_14_0 + len_14_0 ≤ 0 ∧ len_14_0 − len_14_0 ≤ 0 ∧ − i_13_post + i_13_post ≤ 0 ∧ i_13_post − i_13_post ≤ 0 ∧ − i_13_0 + i_13_0 ≤ 0 ∧ i_13_0 − i_13_0 ≤ 0 ∧ − i_111_post + i_111_post ≤ 0 ∧ i_111_post − i_111_post ≤ 0 ∧ − i_111_0 + i_111_0 ≤ 0 ∧ i_111_0 − i_111_0 ≤ 0 ∧ − d_29_post + d_29_post ≤ 0 ∧ d_29_post − d_29_post ≤ 0 ∧ − d_29_1 + d_29_1 ≤ 0 ∧ d_29_1 − d_29_1 ≤ 0 ∧ − d_29_0 + d_29_0 ≤ 0 ∧ d_29_0 − d_29_0 ≤ 0 ∧ − ct_18_post + ct_18_post ≤ 0 ∧ ct_18_post − ct_18_post ≤ 0 ∧ − ct_18_2 + ct_18_2 ≤ 0 ∧ ct_18_2 − ct_18_2 ≤ 0 ∧ − ct_18_1 + ct_18_1 ≤ 0 ∧ ct_18_1 − ct_18_1 ≤ 0 ∧ − ct_18_0 + ct_18_0 ≤ 0 ∧ ct_18_0 − ct_18_0 ≤ 0 ∧ − a_28_post + a_28_post ≤ 0 ∧ a_28_post − a_28_post ≤ 0 ∧ − a_28_1 + a_28_1 ≤ 0 ∧ a_28_1 − a_28_1 ≤ 0 ∧ − a_28_0 + a_28_0 ≤ 0 ∧ a_28_0 − a_28_0 ≤ 0 ∧ − a_175_post + a_175_post ≤ 0 ∧ a_175_post − a_175_post ≤ 0 ∧ − a_175_0 + a_175_0 ≤ 0 ∧ a_175_0 − a_175_0 ≤ 0 ∧ − a_152_post + a_152_post ≤ 0 ∧ a_152_post − a_152_post ≤ 0 ∧ − a_152_0 + a_152_0 ≤ 0 ∧ a_152_0 − a_152_0 ≤ 0 ∧ − a_130_post + a_130_post ≤ 0 ∧ a_130_post − a_130_post ≤ 0 ∧ − a_130_0 + a_130_0 ≤ 0 ∧ a_130_0 − a_130_0 ≤ 0

7 Location Addition

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

18 57 18_var_snapshot: − y_20_post + y_20_post ≤ 0 ∧ y_20_post − y_20_post ≤ 0 ∧ − y_20_2 + y_20_2 ≤ 0 ∧ y_20_2 − y_20_2 ≤ 0 ∧ − y_20_1 + y_20_1 ≤ 0 ∧ y_20_1 − y_20_1 ≤ 0 ∧ − y_20_0 + y_20_0 ≤ 0 ∧ y_20_0 − y_20_0 ≤ 0 ∧ − x_SLAM_f_19_post + x_SLAM_f_19_post ≤ 0 ∧ x_SLAM_f_19_post − x_SLAM_f_19_post ≤ 0 ∧ − x_SLAM_f_19_2 + x_SLAM_f_19_2 ≤ 0 ∧ x_SLAM_f_19_2 − x_SLAM_f_19_2 ≤ 0 ∧ − x_SLAM_f_19_1 + x_SLAM_f_19_1 ≤ 0 ∧ x_SLAM_f_19_1 − x_SLAM_f_19_1 ≤ 0 ∧ − x_SLAM_f_19_0 + x_SLAM_f_19_0 ≤ 0 ∧ x_SLAM_f_19_0 − x_SLAM_f_19_0 ≤ 0 ∧ − x_32_post + x_32_post ≤ 0 ∧ x_32_post − x_32_post ≤ 0 ∧ − x_32_1 + x_32_1 ≤ 0 ∧ x_32_1 − x_32_1 ≤ 0 ∧ − x_32_0 + x_32_0 ≤ 0 ∧ x_32_0 − x_32_0 ≤ 0 ∧ − x_21_post + x_21_post ≤ 0 ∧ x_21_post − x_21_post ≤ 0 ∧ − x_21_2 + x_21_2 ≤ 0 ∧ x_21_2 − x_21_2 ≤ 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 ∧ − x_17_post + x_17_post ≤ 0 ∧ x_17_post − x_17_post ≤ 0 ∧ − x_17_1 + x_17_1 ≤ 0 ∧ x_17_1 − x_17_1 ≤ 0 ∧ − x_17_0 + x_17_0 ≤ 0 ∧ x_17_0 − x_17_0 ≤ 0 ∧ − x_15_post + x_15_post ≤ 0 ∧ x_15_post − x_15_post ≤ 0 ∧ − x_15_0 + x_15_0 ≤ 0 ∧ x_15_0 − x_15_0 ≤ 0 ∧ − tmp_27_post + tmp_27_post ≤ 0 ∧ tmp_27_post − tmp_27_post ≤ 0 ∧ − tmp_27_1 + tmp_27_1 ≤ 0 ∧ tmp_27_1 − tmp_27_1 ≤ 0 ∧ − tmp_27_0 + tmp_27_0 ≤ 0 ∧ tmp_27_0 − tmp_27_0 ≤ 0 ∧ − temp_33_post + temp_33_post ≤ 0 ∧ temp_33_post − temp_33_post ≤ 0 ∧ − temp_33_1 + temp_33_1 ≤ 0 ∧ temp_33_1 − temp_33_1 ≤ 0 ∧ − temp_33_0 + temp_33_0 ≤ 0 ∧ temp_33_0 − temp_33_0 ≤ 0 ∧ − temp0_31_post + temp0_31_post ≤ 0 ∧ temp0_31_post − temp0_31_post ≤ 0 ∧ − temp0_31_1 + temp0_31_1 ≤ 0 ∧ temp0_31_1 − temp0_31_1 ≤ 0 ∧ − temp0_31_0 + temp0_31_0 ≤ 0 ∧ temp0_31_0 − temp0_31_0 ≤ 0 ∧ − temp0_16_0 + temp0_16_0 ≤ 0 ∧ temp0_16_0 − temp0_16_0 ≤ 0 ∧ − t_24_post + t_24_post ≤ 0 ∧ t_24_post − t_24_post ≤ 0 ∧ − t_24_1 + t_24_1 ≤ 0 ∧ t_24_1 − t_24_1 ≤ 0 ∧ − t_24_0 + t_24_0 ≤ 0 ∧ t_24_0 − t_24_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_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_63_post + rcd_63_post ≤ 0 ∧ rcd_63_post − rcd_63_post ≤ 0 ∧ − rcd_63_0 + rcd_63_0 ≤ 0 ∧ rcd_63_0 − rcd_63_0 ≤ 0 ∧ − rcd_100_post + rcd_100_post ≤ 0 ∧ rcd_100_post − rcd_100_post ≤ 0 ∧ − rcd_100_0 + rcd_100_0 ≤ 0 ∧ rcd_100_0 − rcd_100_0 ≤ 0 ∧ − r_37_post + r_37_post ≤ 0 ∧ r_37_post − r_37_post ≤ 0 ∧ − r_37_0 + r_37_0 ≤ 0 ∧ r_37_0 − r_37_0 ≤ 0 ∧ − len_14_post + len_14_post ≤ 0 ∧ len_14_post − len_14_post ≤ 0 ∧ − len_14_0 + len_14_0 ≤ 0 ∧ len_14_0 − len_14_0 ≤ 0 ∧ − i_13_post + i_13_post ≤ 0 ∧ i_13_post − i_13_post ≤ 0 ∧ − i_13_0 + i_13_0 ≤ 0 ∧ i_13_0 − i_13_0 ≤ 0 ∧ − i_111_post + i_111_post ≤ 0 ∧ i_111_post − i_111_post ≤ 0 ∧ − i_111_0 + i_111_0 ≤ 0 ∧ i_111_0 − i_111_0 ≤ 0 ∧ − d_29_post + d_29_post ≤ 0 ∧ d_29_post − d_29_post ≤ 0 ∧ − d_29_1 + d_29_1 ≤ 0 ∧ d_29_1 − d_29_1 ≤ 0 ∧ − d_29_0 + d_29_0 ≤ 0 ∧ d_29_0 − d_29_0 ≤ 0 ∧ − ct_18_post + ct_18_post ≤ 0 ∧ ct_18_post − ct_18_post ≤ 0 ∧ − ct_18_2 + ct_18_2 ≤ 0 ∧ ct_18_2 − ct_18_2 ≤ 0 ∧ − ct_18_1 + ct_18_1 ≤ 0 ∧ ct_18_1 − ct_18_1 ≤ 0 ∧ − ct_18_0 + ct_18_0 ≤ 0 ∧ ct_18_0 − ct_18_0 ≤ 0 ∧ − a_28_post + a_28_post ≤ 0 ∧ a_28_post − a_28_post ≤ 0 ∧ − a_28_1 + a_28_1 ≤ 0 ∧ a_28_1 − a_28_1 ≤ 0 ∧ − a_28_0 + a_28_0 ≤ 0 ∧ a_28_0 − a_28_0 ≤ 0 ∧ − a_175_post + a_175_post ≤ 0 ∧ a_175_post − a_175_post ≤ 0 ∧ − a_175_0 + a_175_0 ≤ 0 ∧ a_175_0 − a_175_0 ≤ 0 ∧ − a_152_post + a_152_post ≤ 0 ∧ a_152_post − a_152_post ≤ 0 ∧ − a_152_0 + a_152_0 ≤ 0 ∧ a_152_0 − a_152_0 ≤ 0 ∧ − a_130_post + a_130_post ≤ 0 ∧ a_130_post − a_130_post ≤ 0 ∧ − a_130_0 + a_130_0 ≤ 0 ∧ a_130_0 − a_130_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 { 9, 19, 20, 21, 22, 23, 24, 9_var_snapshot, 9* }.

8.1.1 Transition Removal

We remove transitions 25, 26, 27, 28 using the following ranking functions, which are bounded by −5.

9: −1 + 9⋅a_152_0
19: −3 + 9⋅a_152_0
20: −4 + 9⋅a_152_0
21: 4 + 9⋅a_175_0
22: 3 + 9⋅a_175_0
23: 2 + 9⋅a_175_0
24: 1 + 9⋅a_152_0
9_var_snapshot: −2 + 9⋅a_152_0
9*: 9⋅a_152_0

8.1.2 Transition Removal

We remove transitions 50, 52, 29, 31, 32, 33, 34 using the following ranking functions, which are bounded by −4.

9: −3
19: 0
20: 0
21: 2
22: 1
23: 0
24: −1
9_var_snapshot: −4
9*: −2

8.1.3 Transition Removal

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

9: 0
19: 0
20: 0
21: 0
22: −1
23: 0
24: 0
9_var_snapshot: 0
9*: 0

8.1.4 Splitting Cut-Point Transitions

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

8.1.4.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 49.

8.1.4.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 { 18, 30, 18_var_snapshot, 18* }.

8.2.1 Transition Removal

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

18: −2 − 4⋅i_13_0 + 4⋅len_14_0
30: −4⋅i_13_0 + 4⋅len_14_0
18_var_snapshot: −3 − 4⋅i_13_0 + 4⋅len_14_0
18*: −1 − 4⋅i_13_0 + 4⋅len_14_0

8.2.2 Transition Removal

We remove transitions 57, 45 using the following ranking functions, which are bounded by −1.

18: 0
30: 1 + len_14_0
18_var_snapshot: −1
18*: len_14_0

8.2.3 Transition Removal

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

18: −1
30: 0
18_var_snapshot: 0
18*: 0

8.2.4 Splitting Cut-Point Transitions

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

8.2.4.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 56.

8.2.4.1.1 Splitting Cut-Point Transitions

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

Tool configuration

T2Cert