LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
0 74 0: − y_25_post + y_25_post ≤ 0 ∧ y_25_post − y_25_post ≤ 0 ∧ − y_25_1 + y_25_1 ≤ 0 ∧ y_25_1 − y_25_1 ≤ 0 ∧ − y_25_0 + y_25_0 ≤ 0 ∧ y_25_0 − y_25_0 ≤ 0 ∧ − y_18_post + y_18_post ≤ 0 ∧ y_18_post − y_18_post ≤ 0 ∧ − y_18_1 + y_18_1 ≤ 0 ∧ y_18_1 − y_18_1 ≤ 0 ∧ − y_18_0 + y_18_0 ≤ 0 ∧ y_18_0 − y_18_0 ≤ 0 ∧ − x_SLAM_f_24_post + x_SLAM_f_24_post ≤ 0 ∧ x_SLAM_f_24_post − x_SLAM_f_24_post ≤ 0 ∧ − x_SLAM_f_24_1 + x_SLAM_f_24_1 ≤ 0 ∧ x_SLAM_f_24_1 − x_SLAM_f_24_1 ≤ 0 ∧ − x_SLAM_f_24_0 + x_SLAM_f_24_0 ≤ 0 ∧ x_SLAM_f_24_0 − x_SLAM_f_24_0 ≤ 0 ∧ − x_SLAM_f_17_post + x_SLAM_f_17_post ≤ 0 ∧ x_SLAM_f_17_post − x_SLAM_f_17_post ≤ 0 ∧ − x_SLAM_f_17_1 + x_SLAM_f_17_1 ≤ 0 ∧ x_SLAM_f_17_1 − x_SLAM_f_17_1 ≤ 0 ∧ − x_SLAM_f_17_0 + x_SLAM_f_17_0 ≤ 0 ∧ x_SLAM_f_17_0 − x_SLAM_f_17_0 ≤ 0 ∧ − x_26_post + x_26_post ≤ 0 ∧ x_26_post − x_26_post ≤ 0 ∧ − x_26_1 + x_26_1 ≤ 0 ∧ x_26_1 − x_26_1 ≤ 0 ∧ − x_26_0 + x_26_0 ≤ 0 ∧ x_26_0 − x_26_0 ≤ 0 ∧ − x_19_post + x_19_post ≤ 0 ∧ x_19_post − x_19_post ≤ 0 ∧ − x_19_1 + x_19_1 ≤ 0 ∧ x_19_1 − x_19_1 ≤ 0 ∧ − x_19_0 + x_19_0 ≤ 0 ∧ x_19_0 − x_19_0 ≤ 0 ∧ − x_176_post + x_176_post ≤ 0 ∧ x_176_post − x_176_post ≤ 0 ∧ − x_176_0 + x_176_0 ≤ 0 ∧ x_176_0 − x_176_0 ≤ 0 ∧ − x_131_post + x_131_post ≤ 0 ∧ x_131_post − x_131_post ≤ 0 ∧ − x_131_0 + x_131_0 ≤ 0 ∧ x_131_0 − x_131_0 ≤ 0 ∧ − tmp_34_post + tmp_34_post ≤ 0 ∧ tmp_34_post − tmp_34_post ≤ 0 ∧ − tmp_34_0 + tmp_34_0 ≤ 0 ∧ tmp_34_0 − tmp_34_0 ≤ 0 ∧ − temp_35_post + temp_35_post ≤ 0 ∧ temp_35_post − temp_35_post ≤ 0 ∧ − temp_35_0 + temp_35_0 ≤ 0 ∧ temp_35_0 − temp_35_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 ∧ − tail_14_post + tail_14_post ≤ 0 ∧ tail_14_post − tail_14_post ≤ 0 ∧ − tail_14_0 + tail_14_0 ≤ 0 ∧ tail_14_0 − tail_14_0 ≤ 0 ∧ − t_22_post + t_22_post ≤ 0 ∧ t_22_post − t_22_post ≤ 0 ∧ − t_22_0 + t_22_0 ≤ 0 ∧ t_22_0 − t_22_0 ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_post + result_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_post − result_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_2 + result_dot_nondet_sdv_special_RETURN_VALUE_13_2 ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_2 ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_0 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post ≤ 0 ∧ − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0 ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0 − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_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_89_post + rcd_89_post ≤ 0 ∧ rcd_89_post − rcd_89_post ≤ 0 ∧ − rcd_89_0 + rcd_89_0 ≤ 0 ∧ rcd_89_0 − rcd_89_0 ≤ 0 ∧ − rcd_59_post + rcd_59_post ≤ 0 ∧ rcd_59_post − rcd_59_post ≤ 0 ∧ − rcd_59_0 + rcd_59_0 ≤ 0 ∧ rcd_59_0 − rcd_59_0 ≤ 0 ∧ − r_39_post + r_39_post ≤ 0 ∧ r_39_post − r_39_post ≤ 0 ∧ − r_39_0 + r_39_0 ≤ 0 ∧ r_39_0 − r_39_0 ≤ 0 ∧ − r_165_post + r_165_post ≤ 0 ∧ r_165_post − r_165_post ≤ 0 ∧ − r_165_0 + r_165_0 ≤ 0 ∧ r_165_0 − r_165_0 ≤ 0 ∧ − r_126_post + r_126_post ≤ 0 ∧ r_126_post − r_126_post ≤ 0 ∧ − r_126_0 + r_126_0 ≤ 0 ∧ r_126_0 − r_126_0 ≤ 0 ∧ − nondet_12_post + nondet_12_post ≤ 0 ∧ nondet_12_post − nondet_12_post ≤ 0 ∧ − nondet_12_1 + nondet_12_1 ≤ 0 ∧ nondet_12_1 − nondet_12_1 ≤ 0 ∧ − nondet_12_0 + nondet_12_0 ≤ 0 ∧ nondet_12_0 − nondet_12_0 ≤ 0 ∧ − length_28_post + length_28_post ≤ 0 ∧ length_28_post − length_28_post ≤ 0 ∧ − length_28_0 + length_28_0 ≤ 0 ∧ length_28_0 − length_28_0 ≤ 0 ∧ − len_187_post + len_187_post ≤ 0 ∧ len_187_post − len_187_post ≤ 0 ∧ − len_187_0 + len_187_0 ≤ 0 ∧ len_187_0 − len_187_0 ≤ 0 ∧ − len_134_post + len_134_post ≤ 0 ∧ len_134_post − len_134_post ≤ 0 ∧ − len_134_0 + len_134_0 ≤ 0 ∧ len_134_0 − len_134_0 ≤ 0 ∧ − i_95_post + i_95_post ≤ 0 ∧ i_95_post − i_95_post ≤ 0 ∧ − i_95_0 + i_95_0 ≤ 0 ∧ i_95_0 − i_95_0 ≤ 0 ∧ − i_30_post + i_30_post ≤ 0 ∧ i_30_post − i_30_post ≤ 0 ∧ − i_30_0 + i_30_0 ≤ 0 ∧ i_30_0 − i_30_0 ≤ 0 ∧ − i_110_post + i_110_post ≤ 0 ∧ i_110_post − i_110_post ≤ 0 ∧ − i_110_0 + i_110_0 ≤ 0 ∧ i_110_0 − i_110_0 ≤ 0 ∧ − head_SLAM_f_29_post + head_SLAM_f_29_post ≤ 0 ∧ head_SLAM_f_29_post − head_SLAM_f_29_post ≤ 0 ∧ − head_SLAM_f_29_0 + head_SLAM_f_29_0 ≤ 0 ∧ head_SLAM_f_29_0 − head_SLAM_f_29_0 ≤ 0 ∧ − head_32_post + head_32_post ≤ 0 ∧ head_32_post − head_32_post ≤ 0 ∧ − head_32_0 + head_32_0 ≤ 0 ∧ head_32_0 − head_32_0 ≤ 0 ∧ − head_15_post + head_15_post ≤ 0 ∧ head_15_post − head_15_post ≤ 0 ∧ − head_15_0 + head_15_0 ≤ 0 ∧ head_15_0 − head_15_0 ≤ 0 ∧ − f_171_post + f_171_post ≤ 0 ∧ f_171_post − f_171_post ≤ 0 ∧ − f_171_0 + f_171_0 ≤ 0 ∧ f_171_0 − f_171_0 ≤ 0 ∧ − a_343_post + a_343_post ≤ 0 ∧ a_343_post − a_343_post ≤ 0 ∧ − a_343_0 + a_343_0 ≤ 0 ∧ a_343_0 − a_343_0 ≤ 0 ∧ − a_342_post + a_342_post ≤ 0 ∧ a_342_post − a_342_post ≤ 0 ∧ − a_342_0 + a_342_0 ≤ 0 ∧ a_342_0 − a_342_0 ≤ 0 ∧ − a_289_post + a_289_post ≤ 0 ∧ a_289_post − a_289_post ≤ 0 ∧ − a_289_0 + a_289_0 ≤ 0 ∧ a_289_0 − a_289_0 ≤ 0 ∧ − a_281_post + a_281_post ≤ 0 ∧ a_281_post − a_281_post ≤ 0 ∧ − a_281_0 + a_281_0 ≤ 0 ∧ a_281_0 − a_281_0 ≤ 0 ∧ − a_225_post + a_225_post ≤ 0 ∧ a_225_post − a_225_post ≤ 0 ∧ − a_225_0 + a_225_0 ≤ 0 ∧ a_225_0 − a_225_0 ≤ 0 ∧ − a_188_post + a_188_post ≤ 0 ∧ a_188_post − a_188_post ≤ 0 ∧ − a_188_0 + a_188_0 ≤ 0 ∧ a_188_0 − a_188_0 ≤ 0 ∧ − a_149_post + a_149_post ≤ 0 ∧ a_149_post − a_149_post ≤ 0 ∧ − a_149_0 + a_149_0 ≤ 0 ∧ a_149_0 − a_149_0 ≤ 0 ∧ − a_118_post + a_118_post ≤ 0 ∧ a_118_post − a_118_post ≤ 0 ∧ − a_118_0 + a_118_0 ≤ 0 ∧ a_118_0 − a_118_0 ≤ 0
6 81 6: − y_25_post + y_25_post ≤ 0 ∧ y_25_post − y_25_post ≤ 0 ∧ − y_25_1 + y_25_1 ≤ 0 ∧ y_25_1 − y_25_1 ≤ 0 ∧ − y_25_0 + y_25_0 ≤ 0 ∧ y_25_0 − y_25_0 ≤ 0 ∧ − y_18_post + y_18_post ≤ 0 ∧ y_18_post − y_18_post ≤ 0 ∧ − y_18_1 + y_18_1 ≤ 0 ∧ y_18_1 − y_18_1 ≤ 0 ∧ − y_18_0 + y_18_0 ≤ 0 ∧ y_18_0 − y_18_0 ≤ 0 ∧ − x_SLAM_f_24_post + x_SLAM_f_24_post ≤ 0 ∧ x_SLAM_f_24_post − x_SLAM_f_24_post ≤ 0 ∧ − x_SLAM_f_24_1 + x_SLAM_f_24_1 ≤ 0 ∧ x_SLAM_f_24_1 − x_SLAM_f_24_1 ≤ 0 ∧ − x_SLAM_f_24_0 + x_SLAM_f_24_0 ≤ 0 ∧ x_SLAM_f_24_0 − x_SLAM_f_24_0 ≤ 0 ∧ − x_SLAM_f_17_post + x_SLAM_f_17_post ≤ 0 ∧ x_SLAM_f_17_post − x_SLAM_f_17_post ≤ 0 ∧ − x_SLAM_f_17_1 + x_SLAM_f_17_1 ≤ 0 ∧ x_SLAM_f_17_1 − x_SLAM_f_17_1 ≤ 0 ∧ − x_SLAM_f_17_0 + x_SLAM_f_17_0 ≤ 0 ∧ x_SLAM_f_17_0 − x_SLAM_f_17_0 ≤ 0 ∧ − x_26_post + x_26_post ≤ 0 ∧ x_26_post − x_26_post ≤ 0 ∧ − x_26_1 + x_26_1 ≤ 0 ∧ x_26_1 − x_26_1 ≤ 0 ∧ − x_26_0 + x_26_0 ≤ 0 ∧ x_26_0 − x_26_0 ≤ 0 ∧ − x_19_post + x_19_post ≤ 0 ∧ x_19_post − x_19_post ≤ 0 ∧ − x_19_1 + x_19_1 ≤ 0 ∧ x_19_1 − x_19_1 ≤ 0 ∧ − x_19_0 + x_19_0 ≤ 0 ∧ x_19_0 − x_19_0 ≤ 0 ∧ − x_176_post + x_176_post ≤ 0 ∧ x_176_post − x_176_post ≤ 0 ∧ − x_176_0 + x_176_0 ≤ 0 ∧ x_176_0 − x_176_0 ≤ 0 ∧ − x_131_post + x_131_post ≤ 0 ∧ x_131_post − x_131_post ≤ 0 ∧ − x_131_0 + x_131_0 ≤ 0 ∧ x_131_0 − x_131_0 ≤ 0 ∧ − tmp_34_post + tmp_34_post ≤ 0 ∧ tmp_34_post − tmp_34_post ≤ 0 ∧ − tmp_34_0 + tmp_34_0 ≤ 0 ∧ tmp_34_0 − tmp_34_0 ≤ 0 ∧ − temp_35_post + temp_35_post ≤ 0 ∧ temp_35_post − temp_35_post ≤ 0 ∧ − temp_35_0 + temp_35_0 ≤ 0 ∧ temp_35_0 − temp_35_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 ∧ − tail_14_post + tail_14_post ≤ 0 ∧ tail_14_post − tail_14_post ≤ 0 ∧ − tail_14_0 + tail_14_0 ≤ 0 ∧ tail_14_0 − tail_14_0 ≤ 0 ∧ − t_22_post + t_22_post ≤ 0 ∧ t_22_post − t_22_post ≤ 0 ∧ − t_22_0 + t_22_0 ≤ 0 ∧ t_22_0 − t_22_0 ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_post + result_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_post − result_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_2 + result_dot_nondet_sdv_special_RETURN_VALUE_13_2 ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_2 ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_0 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post ≤ 0 ∧ − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0 ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0 − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_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_89_post + rcd_89_post ≤ 0 ∧ rcd_89_post − rcd_89_post ≤ 0 ∧ − rcd_89_0 + rcd_89_0 ≤ 0 ∧ rcd_89_0 − rcd_89_0 ≤ 0 ∧ − rcd_59_post + rcd_59_post ≤ 0 ∧ rcd_59_post − rcd_59_post ≤ 0 ∧ − rcd_59_0 + rcd_59_0 ≤ 0 ∧ rcd_59_0 − rcd_59_0 ≤ 0 ∧ − r_39_post + r_39_post ≤ 0 ∧ r_39_post − r_39_post ≤ 0 ∧ − r_39_0 + r_39_0 ≤ 0 ∧ r_39_0 − r_39_0 ≤ 0 ∧ − r_165_post + r_165_post ≤ 0 ∧ r_165_post − r_165_post ≤ 0 ∧ − r_165_0 + r_165_0 ≤ 0 ∧ r_165_0 − r_165_0 ≤ 0 ∧ − r_126_post + r_126_post ≤ 0 ∧ r_126_post − r_126_post ≤ 0 ∧ − r_126_0 + r_126_0 ≤ 0 ∧ r_126_0 − r_126_0 ≤ 0 ∧ − nondet_12_post + nondet_12_post ≤ 0 ∧ nondet_12_post − nondet_12_post ≤ 0 ∧ − nondet_12_1 + nondet_12_1 ≤ 0 ∧ nondet_12_1 − nondet_12_1 ≤ 0 ∧ − nondet_12_0 + nondet_12_0 ≤ 0 ∧ nondet_12_0 − nondet_12_0 ≤ 0 ∧ − length_28_post + length_28_post ≤ 0 ∧ length_28_post − length_28_post ≤ 0 ∧ − length_28_0 + length_28_0 ≤ 0 ∧ length_28_0 − length_28_0 ≤ 0 ∧ − len_187_post + len_187_post ≤ 0 ∧ len_187_post − len_187_post ≤ 0 ∧ − len_187_0 + len_187_0 ≤ 0 ∧ len_187_0 − len_187_0 ≤ 0 ∧ − len_134_post + len_134_post ≤ 0 ∧ len_134_post − len_134_post ≤ 0 ∧ − len_134_0 + len_134_0 ≤ 0 ∧ len_134_0 − len_134_0 ≤ 0 ∧ − i_95_post + i_95_post ≤ 0 ∧ i_95_post − i_95_post ≤ 0 ∧ − i_95_0 + i_95_0 ≤ 0 ∧ i_95_0 − i_95_0 ≤ 0 ∧ − i_30_post + i_30_post ≤ 0 ∧ i_30_post − i_30_post ≤ 0 ∧ − i_30_0 + i_30_0 ≤ 0 ∧ i_30_0 − i_30_0 ≤ 0 ∧ − i_110_post + i_110_post ≤ 0 ∧ i_110_post − i_110_post ≤ 0 ∧ − i_110_0 + i_110_0 ≤ 0 ∧ i_110_0 − i_110_0 ≤ 0 ∧ − head_SLAM_f_29_post + head_SLAM_f_29_post ≤ 0 ∧ head_SLAM_f_29_post − head_SLAM_f_29_post ≤ 0 ∧ − head_SLAM_f_29_0 + head_SLAM_f_29_0 ≤ 0 ∧ head_SLAM_f_29_0 − head_SLAM_f_29_0 ≤ 0 ∧ − head_32_post + head_32_post ≤ 0 ∧ head_32_post − head_32_post ≤ 0 ∧ − head_32_0 + head_32_0 ≤ 0 ∧ head_32_0 − head_32_0 ≤ 0 ∧ − head_15_post + head_15_post ≤ 0 ∧ head_15_post − head_15_post ≤ 0 ∧ − head_15_0 + head_15_0 ≤ 0 ∧ head_15_0 − head_15_0 ≤ 0 ∧ − f_171_post + f_171_post ≤ 0 ∧ f_171_post − f_171_post ≤ 0 ∧ − f_171_0 + f_171_0 ≤ 0 ∧ f_171_0 − f_171_0 ≤ 0 ∧ − a_343_post + a_343_post ≤ 0 ∧ a_343_post − a_343_post ≤ 0 ∧ − a_343_0 + a_343_0 ≤ 0 ∧ a_343_0 − a_343_0 ≤ 0 ∧ − a_342_post + a_342_post ≤ 0 ∧ a_342_post − a_342_post ≤ 0 ∧ − a_342_0 + a_342_0 ≤ 0 ∧ a_342_0 − a_342_0 ≤ 0 ∧ − a_289_post + a_289_post ≤ 0 ∧ a_289_post − a_289_post ≤ 0 ∧ − a_289_0 + a_289_0 ≤ 0 ∧ a_289_0 − a_289_0 ≤ 0 ∧ − a_281_post + a_281_post ≤ 0 ∧ a_281_post − a_281_post ≤ 0 ∧ − a_281_0 + a_281_0 ≤ 0 ∧ a_281_0 − a_281_0 ≤ 0 ∧ − a_225_post + a_225_post ≤ 0 ∧ a_225_post − a_225_post ≤ 0 ∧ − a_225_0 + a_225_0 ≤ 0 ∧ a_225_0 − a_225_0 ≤ 0 ∧ − a_188_post + a_188_post ≤ 0 ∧ a_188_post − a_188_post ≤ 0 ∧ − a_188_0 + a_188_0 ≤ 0 ∧ a_188_0 − a_188_0 ≤ 0 ∧ − a_149_post + a_149_post ≤ 0 ∧ a_149_post − a_149_post ≤ 0 ∧ − a_149_0 + a_149_0 ≤ 0 ∧ a_149_0 − a_149_0 ≤ 0 ∧ − a_118_post + a_118_post ≤ 0 ∧ a_118_post − a_118_post ≤ 0 ∧ − a_118_0 + a_118_0 ≤ 0 ∧ a_118_0 − a_118_0 ≤ 0
31 88 31: − y_25_post + y_25_post ≤ 0 ∧ y_25_post − y_25_post ≤ 0 ∧ − y_25_1 + y_25_1 ≤ 0 ∧ y_25_1 − y_25_1 ≤ 0 ∧ − y_25_0 + y_25_0 ≤ 0 ∧ y_25_0 − y_25_0 ≤ 0 ∧ − y_18_post + y_18_post ≤ 0 ∧ y_18_post − y_18_post ≤ 0 ∧ − y_18_1 + y_18_1 ≤ 0 ∧ y_18_1 − y_18_1 ≤ 0 ∧ − y_18_0 + y_18_0 ≤ 0 ∧ y_18_0 − y_18_0 ≤ 0 ∧ − x_SLAM_f_24_post + x_SLAM_f_24_post ≤ 0 ∧ x_SLAM_f_24_post − x_SLAM_f_24_post ≤ 0 ∧ − x_SLAM_f_24_1 + x_SLAM_f_24_1 ≤ 0 ∧ x_SLAM_f_24_1 − x_SLAM_f_24_1 ≤ 0 ∧ − x_SLAM_f_24_0 + x_SLAM_f_24_0 ≤ 0 ∧ x_SLAM_f_24_0 − x_SLAM_f_24_0 ≤ 0 ∧ − x_SLAM_f_17_post + x_SLAM_f_17_post ≤ 0 ∧ x_SLAM_f_17_post − x_SLAM_f_17_post ≤ 0 ∧ − x_SLAM_f_17_1 + x_SLAM_f_17_1 ≤ 0 ∧ x_SLAM_f_17_1 − x_SLAM_f_17_1 ≤ 0 ∧ − x_SLAM_f_17_0 + x_SLAM_f_17_0 ≤ 0 ∧ x_SLAM_f_17_0 − x_SLAM_f_17_0 ≤ 0 ∧ − x_26_post + x_26_post ≤ 0 ∧ x_26_post − x_26_post ≤ 0 ∧ − x_26_1 + x_26_1 ≤ 0 ∧ x_26_1 − x_26_1 ≤ 0 ∧ − x_26_0 + x_26_0 ≤ 0 ∧ x_26_0 − x_26_0 ≤ 0 ∧ − x_19_post + x_19_post ≤ 0 ∧ x_19_post − x_19_post ≤ 0 ∧ − x_19_1 + x_19_1 ≤ 0 ∧ x_19_1 − x_19_1 ≤ 0 ∧ − x_19_0 + x_19_0 ≤ 0 ∧ x_19_0 − x_19_0 ≤ 0 ∧ − x_176_post + x_176_post ≤ 0 ∧ x_176_post − x_176_post ≤ 0 ∧ − x_176_0 + x_176_0 ≤ 0 ∧ x_176_0 − x_176_0 ≤ 0 ∧ − x_131_post + x_131_post ≤ 0 ∧ x_131_post − x_131_post ≤ 0 ∧ − x_131_0 + x_131_0 ≤ 0 ∧ x_131_0 − x_131_0 ≤ 0 ∧ − tmp_34_post + tmp_34_post ≤ 0 ∧ tmp_34_post − tmp_34_post ≤ 0 ∧ − tmp_34_0 + tmp_34_0 ≤ 0 ∧ tmp_34_0 − tmp_34_0 ≤ 0 ∧ − temp_35_post + temp_35_post ≤ 0 ∧ temp_35_post − temp_35_post ≤ 0 ∧ − temp_35_0 + temp_35_0 ≤ 0 ∧ temp_35_0 − temp_35_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 ∧ − tail_14_post + tail_14_post ≤ 0 ∧ tail_14_post − tail_14_post ≤ 0 ∧ − tail_14_0 + tail_14_0 ≤ 0 ∧ tail_14_0 − tail_14_0 ≤ 0 ∧ − t_22_post + t_22_post ≤ 0 ∧ t_22_post − t_22_post ≤ 0 ∧ − t_22_0 + t_22_0 ≤ 0 ∧ t_22_0 − t_22_0 ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_post + result_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_post − result_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_2 + result_dot_nondet_sdv_special_RETURN_VALUE_13_2 ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_2 ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_0 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post ≤ 0 ∧ − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0 ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0 − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_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_89_post + rcd_89_post ≤ 0 ∧ rcd_89_post − rcd_89_post ≤ 0 ∧ − rcd_89_0 + rcd_89_0 ≤ 0 ∧ rcd_89_0 − rcd_89_0 ≤ 0 ∧ − rcd_59_post + rcd_59_post ≤ 0 ∧ rcd_59_post − rcd_59_post ≤ 0 ∧ − rcd_59_0 + rcd_59_0 ≤ 0 ∧ rcd_59_0 − rcd_59_0 ≤ 0 ∧ − r_39_post + r_39_post ≤ 0 ∧ r_39_post − r_39_post ≤ 0 ∧ − r_39_0 + r_39_0 ≤ 0 ∧ r_39_0 − r_39_0 ≤ 0 ∧ − r_165_post + r_165_post ≤ 0 ∧ r_165_post − r_165_post ≤ 0 ∧ − r_165_0 + r_165_0 ≤ 0 ∧ r_165_0 − r_165_0 ≤ 0 ∧ − r_126_post + r_126_post ≤ 0 ∧ r_126_post − r_126_post ≤ 0 ∧ − r_126_0 + r_126_0 ≤ 0 ∧ r_126_0 − r_126_0 ≤ 0 ∧ − nondet_12_post + nondet_12_post ≤ 0 ∧ nondet_12_post − nondet_12_post ≤ 0 ∧ − nondet_12_1 + nondet_12_1 ≤ 0 ∧ nondet_12_1 − nondet_12_1 ≤ 0 ∧ − nondet_12_0 + nondet_12_0 ≤ 0 ∧ nondet_12_0 − nondet_12_0 ≤ 0 ∧ − length_28_post + length_28_post ≤ 0 ∧ length_28_post − length_28_post ≤ 0 ∧ − length_28_0 + length_28_0 ≤ 0 ∧ length_28_0 − length_28_0 ≤ 0 ∧ − len_187_post + len_187_post ≤ 0 ∧ len_187_post − len_187_post ≤ 0 ∧ − len_187_0 + len_187_0 ≤ 0 ∧ len_187_0 − len_187_0 ≤ 0 ∧ − len_134_post + len_134_post ≤ 0 ∧ len_134_post − len_134_post ≤ 0 ∧ − len_134_0 + len_134_0 ≤ 0 ∧ len_134_0 − len_134_0 ≤ 0 ∧ − i_95_post + i_95_post ≤ 0 ∧ i_95_post − i_95_post ≤ 0 ∧ − i_95_0 + i_95_0 ≤ 0 ∧ i_95_0 − i_95_0 ≤ 0 ∧ − i_30_post + i_30_post ≤ 0 ∧ i_30_post − i_30_post ≤ 0 ∧ − i_30_0 + i_30_0 ≤ 0 ∧ i_30_0 − i_30_0 ≤ 0 ∧ − i_110_post + i_110_post ≤ 0 ∧ i_110_post − i_110_post ≤ 0 ∧ − i_110_0 + i_110_0 ≤ 0 ∧ i_110_0 − i_110_0 ≤ 0 ∧ − head_SLAM_f_29_post + head_SLAM_f_29_post ≤ 0 ∧ head_SLAM_f_29_post − head_SLAM_f_29_post ≤ 0 ∧ − head_SLAM_f_29_0 + head_SLAM_f_29_0 ≤ 0 ∧ head_SLAM_f_29_0 − head_SLAM_f_29_0 ≤ 0 ∧ − head_32_post + head_32_post ≤ 0 ∧ head_32_post − head_32_post ≤ 0 ∧ − head_32_0 + head_32_0 ≤ 0 ∧ head_32_0 − head_32_0 ≤ 0 ∧ − head_15_post + head_15_post ≤ 0 ∧ head_15_post − head_15_post ≤ 0 ∧ − head_15_0 + head_15_0 ≤ 0 ∧ head_15_0 − head_15_0 ≤ 0 ∧ − f_171_post + f_171_post ≤ 0 ∧ f_171_post − f_171_post ≤ 0 ∧ − f_171_0 + f_171_0 ≤ 0 ∧ f_171_0 − f_171_0 ≤ 0 ∧ − a_343_post + a_343_post ≤ 0 ∧ a_343_post − a_343_post ≤ 0 ∧ − a_343_0 + a_343_0 ≤ 0 ∧ a_343_0 − a_343_0 ≤ 0 ∧ − a_342_post + a_342_post ≤ 0 ∧ a_342_post − a_342_post ≤ 0 ∧ − a_342_0 + a_342_0 ≤ 0 ∧ a_342_0 − a_342_0 ≤ 0 ∧ − a_289_post + a_289_post ≤ 0 ∧ a_289_post − a_289_post ≤ 0 ∧ − a_289_0 + a_289_0 ≤ 0 ∧ a_289_0 − a_289_0 ≤ 0 ∧ − a_281_post + a_281_post ≤ 0 ∧ a_281_post − a_281_post ≤ 0 ∧ − a_281_0 + a_281_0 ≤ 0 ∧ a_281_0 − a_281_0 ≤ 0 ∧ − a_225_post + a_225_post ≤ 0 ∧ a_225_post − a_225_post ≤ 0 ∧ − a_225_0 + a_225_0 ≤ 0 ∧ a_225_0 − a_225_0 ≤ 0 ∧ − a_188_post + a_188_post ≤ 0 ∧ a_188_post − a_188_post ≤ 0 ∧ − a_188_0 + a_188_0 ≤ 0 ∧ a_188_0 − a_188_0 ≤ 0 ∧ − a_149_post + a_149_post ≤ 0 ∧ a_149_post − a_149_post ≤ 0 ∧ − a_149_0 + a_149_0 ≤ 0 ∧ a_149_0 − a_149_0 ≤ 0 ∧ − a_118_post + a_118_post ≤ 0 ∧ a_118_post − a_118_post ≤ 0 ∧ − a_118_0 + a_118_0 ≤ 0 ∧ a_118_0 − a_118_0 ≤ 0
and for every transition t, a duplicate t is considered.

2 Transition Removal

We remove transitions 0, 3, 4, 5, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 65, 66, 67, 68, 69, 70, 71, 72, 73 using the following ranking functions, which are bounded by −79.

65: 0
30: 0
3: 0
5: 0
40: 0
41: 0
42: 0
43: 0
44: 0
45: 0
46: 0
47: 0
48: 0
49: 0
50: 0
51: 0
52: 0
0: 0
2: 0
1: 0
61: 0
62: 0
63: 0
64: 0
31: 0
34: 0
35: 0
36: 0
37: 0
38: 0
39: 0
32: 0
33: 0
23: 0
24: 0
25: 0
26: 0
27: 0
28: 0
29: 0
6: 0
7: 0
8: 0
9: 0
10: 0
11: 0
12: 0
13: 0
4: 0
65: −36
30: −37
3: −38
5: −39
40: −40
41: −41
42: −42
43: −43
44: −44
45: −45
46: −46
47: −47
48: −48
49: −49
50: −50
51: −51
52: −52
0: −53
2: −53
0_var_snapshot: −53
0*: −53
1: −56
61: −57
62: −58
63: −59
64: −60
31: −61
34: −61
35: −61
36: −61
37: −61
38: −61
39: −61
31_var_snapshot: −61
31*: −61
32: −64
33: −65
23: −66
24: −67
25: −68
26: −69
27: −70
28: −71
29: −72
6: −73
7: −73
8: −73
9: −73
10: −73
11: −73
12: −73
13: −73
6_var_snapshot: −73
6*: −73
4: −77

3 Location Addition

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

0* 77 0: − y_25_post + y_25_post ≤ 0 ∧ y_25_post − y_25_post ≤ 0 ∧ − y_25_1 + y_25_1 ≤ 0 ∧ y_25_1 − y_25_1 ≤ 0 ∧ − y_25_0 + y_25_0 ≤ 0 ∧ y_25_0 − y_25_0 ≤ 0 ∧ − y_18_post + y_18_post ≤ 0 ∧ y_18_post − y_18_post ≤ 0 ∧ − y_18_1 + y_18_1 ≤ 0 ∧ y_18_1 − y_18_1 ≤ 0 ∧ − y_18_0 + y_18_0 ≤ 0 ∧ y_18_0 − y_18_0 ≤ 0 ∧ − x_SLAM_f_24_post + x_SLAM_f_24_post ≤ 0 ∧ x_SLAM_f_24_post − x_SLAM_f_24_post ≤ 0 ∧ − x_SLAM_f_24_1 + x_SLAM_f_24_1 ≤ 0 ∧ x_SLAM_f_24_1 − x_SLAM_f_24_1 ≤ 0 ∧ − x_SLAM_f_24_0 + x_SLAM_f_24_0 ≤ 0 ∧ x_SLAM_f_24_0 − x_SLAM_f_24_0 ≤ 0 ∧ − x_SLAM_f_17_post + x_SLAM_f_17_post ≤ 0 ∧ x_SLAM_f_17_post − x_SLAM_f_17_post ≤ 0 ∧ − x_SLAM_f_17_1 + x_SLAM_f_17_1 ≤ 0 ∧ x_SLAM_f_17_1 − x_SLAM_f_17_1 ≤ 0 ∧ − x_SLAM_f_17_0 + x_SLAM_f_17_0 ≤ 0 ∧ x_SLAM_f_17_0 − x_SLAM_f_17_0 ≤ 0 ∧ − x_26_post + x_26_post ≤ 0 ∧ x_26_post − x_26_post ≤ 0 ∧ − x_26_1 + x_26_1 ≤ 0 ∧ x_26_1 − x_26_1 ≤ 0 ∧ − x_26_0 + x_26_0 ≤ 0 ∧ x_26_0 − x_26_0 ≤ 0 ∧ − x_19_post + x_19_post ≤ 0 ∧ x_19_post − x_19_post ≤ 0 ∧ − x_19_1 + x_19_1 ≤ 0 ∧ x_19_1 − x_19_1 ≤ 0 ∧ − x_19_0 + x_19_0 ≤ 0 ∧ x_19_0 − x_19_0 ≤ 0 ∧ − x_176_post + x_176_post ≤ 0 ∧ x_176_post − x_176_post ≤ 0 ∧ − x_176_0 + x_176_0 ≤ 0 ∧ x_176_0 − x_176_0 ≤ 0 ∧ − x_131_post + x_131_post ≤ 0 ∧ x_131_post − x_131_post ≤ 0 ∧ − x_131_0 + x_131_0 ≤ 0 ∧ x_131_0 − x_131_0 ≤ 0 ∧ − tmp_34_post + tmp_34_post ≤ 0 ∧ tmp_34_post − tmp_34_post ≤ 0 ∧ − tmp_34_0 + tmp_34_0 ≤ 0 ∧ tmp_34_0 − tmp_34_0 ≤ 0 ∧ − temp_35_post + temp_35_post ≤ 0 ∧ temp_35_post − temp_35_post ≤ 0 ∧ − temp_35_0 + temp_35_0 ≤ 0 ∧ temp_35_0 − temp_35_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 ∧ − tail_14_post + tail_14_post ≤ 0 ∧ tail_14_post − tail_14_post ≤ 0 ∧ − tail_14_0 + tail_14_0 ≤ 0 ∧ tail_14_0 − tail_14_0 ≤ 0 ∧ − t_22_post + t_22_post ≤ 0 ∧ t_22_post − t_22_post ≤ 0 ∧ − t_22_0 + t_22_0 ≤ 0 ∧ t_22_0 − t_22_0 ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_post + result_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_post − result_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_2 + result_dot_nondet_sdv_special_RETURN_VALUE_13_2 ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_2 ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_0 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post ≤ 0 ∧ − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0 ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0 − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_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_89_post + rcd_89_post ≤ 0 ∧ rcd_89_post − rcd_89_post ≤ 0 ∧ − rcd_89_0 + rcd_89_0 ≤ 0 ∧ rcd_89_0 − rcd_89_0 ≤ 0 ∧ − rcd_59_post + rcd_59_post ≤ 0 ∧ rcd_59_post − rcd_59_post ≤ 0 ∧ − rcd_59_0 + rcd_59_0 ≤ 0 ∧ rcd_59_0 − rcd_59_0 ≤ 0 ∧ − r_39_post + r_39_post ≤ 0 ∧ r_39_post − r_39_post ≤ 0 ∧ − r_39_0 + r_39_0 ≤ 0 ∧ r_39_0 − r_39_0 ≤ 0 ∧ − r_165_post + r_165_post ≤ 0 ∧ r_165_post − r_165_post ≤ 0 ∧ − r_165_0 + r_165_0 ≤ 0 ∧ r_165_0 − r_165_0 ≤ 0 ∧ − r_126_post + r_126_post ≤ 0 ∧ r_126_post − r_126_post ≤ 0 ∧ − r_126_0 + r_126_0 ≤ 0 ∧ r_126_0 − r_126_0 ≤ 0 ∧ − nondet_12_post + nondet_12_post ≤ 0 ∧ nondet_12_post − nondet_12_post ≤ 0 ∧ − nondet_12_1 + nondet_12_1 ≤ 0 ∧ nondet_12_1 − nondet_12_1 ≤ 0 ∧ − nondet_12_0 + nondet_12_0 ≤ 0 ∧ nondet_12_0 − nondet_12_0 ≤ 0 ∧ − length_28_post + length_28_post ≤ 0 ∧ length_28_post − length_28_post ≤ 0 ∧ − length_28_0 + length_28_0 ≤ 0 ∧ length_28_0 − length_28_0 ≤ 0 ∧ − len_187_post + len_187_post ≤ 0 ∧ len_187_post − len_187_post ≤ 0 ∧ − len_187_0 + len_187_0 ≤ 0 ∧ len_187_0 − len_187_0 ≤ 0 ∧ − len_134_post + len_134_post ≤ 0 ∧ len_134_post − len_134_post ≤ 0 ∧ − len_134_0 + len_134_0 ≤ 0 ∧ len_134_0 − len_134_0 ≤ 0 ∧ − i_95_post + i_95_post ≤ 0 ∧ i_95_post − i_95_post ≤ 0 ∧ − i_95_0 + i_95_0 ≤ 0 ∧ i_95_0 − i_95_0 ≤ 0 ∧ − i_30_post + i_30_post ≤ 0 ∧ i_30_post − i_30_post ≤ 0 ∧ − i_30_0 + i_30_0 ≤ 0 ∧ i_30_0 − i_30_0 ≤ 0 ∧ − i_110_post + i_110_post ≤ 0 ∧ i_110_post − i_110_post ≤ 0 ∧ − i_110_0 + i_110_0 ≤ 0 ∧ i_110_0 − i_110_0 ≤ 0 ∧ − head_SLAM_f_29_post + head_SLAM_f_29_post ≤ 0 ∧ head_SLAM_f_29_post − head_SLAM_f_29_post ≤ 0 ∧ − head_SLAM_f_29_0 + head_SLAM_f_29_0 ≤ 0 ∧ head_SLAM_f_29_0 − head_SLAM_f_29_0 ≤ 0 ∧ − head_32_post + head_32_post ≤ 0 ∧ head_32_post − head_32_post ≤ 0 ∧ − head_32_0 + head_32_0 ≤ 0 ∧ head_32_0 − head_32_0 ≤ 0 ∧ − head_15_post + head_15_post ≤ 0 ∧ head_15_post − head_15_post ≤ 0 ∧ − head_15_0 + head_15_0 ≤ 0 ∧ head_15_0 − head_15_0 ≤ 0 ∧ − f_171_post + f_171_post ≤ 0 ∧ f_171_post − f_171_post ≤ 0 ∧ − f_171_0 + f_171_0 ≤ 0 ∧ f_171_0 − f_171_0 ≤ 0 ∧ − a_343_post + a_343_post ≤ 0 ∧ a_343_post − a_343_post ≤ 0 ∧ − a_343_0 + a_343_0 ≤ 0 ∧ a_343_0 − a_343_0 ≤ 0 ∧ − a_342_post + a_342_post ≤ 0 ∧ a_342_post − a_342_post ≤ 0 ∧ − a_342_0 + a_342_0 ≤ 0 ∧ a_342_0 − a_342_0 ≤ 0 ∧ − a_289_post + a_289_post ≤ 0 ∧ a_289_post − a_289_post ≤ 0 ∧ − a_289_0 + a_289_0 ≤ 0 ∧ a_289_0 − a_289_0 ≤ 0 ∧ − a_281_post + a_281_post ≤ 0 ∧ a_281_post − a_281_post ≤ 0 ∧ − a_281_0 + a_281_0 ≤ 0 ∧ a_281_0 − a_281_0 ≤ 0 ∧ − a_225_post + a_225_post ≤ 0 ∧ a_225_post − a_225_post ≤ 0 ∧ − a_225_0 + a_225_0 ≤ 0 ∧ a_225_0 − a_225_0 ≤ 0 ∧ − a_188_post + a_188_post ≤ 0 ∧ a_188_post − a_188_post ≤ 0 ∧ − a_188_0 + a_188_0 ≤ 0 ∧ a_188_0 − a_188_0 ≤ 0 ∧ − a_149_post + a_149_post ≤ 0 ∧ a_149_post − a_149_post ≤ 0 ∧ − a_149_0 + a_149_0 ≤ 0 ∧ a_149_0 − a_149_0 ≤ 0 ∧ − a_118_post + a_118_post ≤ 0 ∧ a_118_post − a_118_post ≤ 0 ∧ − a_118_0 + a_118_0 ≤ 0 ∧ a_118_0 − a_118_0 ≤ 0

4 Location Addition

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

0 75 0_var_snapshot: − y_25_post + y_25_post ≤ 0 ∧ y_25_post − y_25_post ≤ 0 ∧ − y_25_1 + y_25_1 ≤ 0 ∧ y_25_1 − y_25_1 ≤ 0 ∧ − y_25_0 + y_25_0 ≤ 0 ∧ y_25_0 − y_25_0 ≤ 0 ∧ − y_18_post + y_18_post ≤ 0 ∧ y_18_post − y_18_post ≤ 0 ∧ − y_18_1 + y_18_1 ≤ 0 ∧ y_18_1 − y_18_1 ≤ 0 ∧ − y_18_0 + y_18_0 ≤ 0 ∧ y_18_0 − y_18_0 ≤ 0 ∧ − x_SLAM_f_24_post + x_SLAM_f_24_post ≤ 0 ∧ x_SLAM_f_24_post − x_SLAM_f_24_post ≤ 0 ∧ − x_SLAM_f_24_1 + x_SLAM_f_24_1 ≤ 0 ∧ x_SLAM_f_24_1 − x_SLAM_f_24_1 ≤ 0 ∧ − x_SLAM_f_24_0 + x_SLAM_f_24_0 ≤ 0 ∧ x_SLAM_f_24_0 − x_SLAM_f_24_0 ≤ 0 ∧ − x_SLAM_f_17_post + x_SLAM_f_17_post ≤ 0 ∧ x_SLAM_f_17_post − x_SLAM_f_17_post ≤ 0 ∧ − x_SLAM_f_17_1 + x_SLAM_f_17_1 ≤ 0 ∧ x_SLAM_f_17_1 − x_SLAM_f_17_1 ≤ 0 ∧ − x_SLAM_f_17_0 + x_SLAM_f_17_0 ≤ 0 ∧ x_SLAM_f_17_0 − x_SLAM_f_17_0 ≤ 0 ∧ − x_26_post + x_26_post ≤ 0 ∧ x_26_post − x_26_post ≤ 0 ∧ − x_26_1 + x_26_1 ≤ 0 ∧ x_26_1 − x_26_1 ≤ 0 ∧ − x_26_0 + x_26_0 ≤ 0 ∧ x_26_0 − x_26_0 ≤ 0 ∧ − x_19_post + x_19_post ≤ 0 ∧ x_19_post − x_19_post ≤ 0 ∧ − x_19_1 + x_19_1 ≤ 0 ∧ x_19_1 − x_19_1 ≤ 0 ∧ − x_19_0 + x_19_0 ≤ 0 ∧ x_19_0 − x_19_0 ≤ 0 ∧ − x_176_post + x_176_post ≤ 0 ∧ x_176_post − x_176_post ≤ 0 ∧ − x_176_0 + x_176_0 ≤ 0 ∧ x_176_0 − x_176_0 ≤ 0 ∧ − x_131_post + x_131_post ≤ 0 ∧ x_131_post − x_131_post ≤ 0 ∧ − x_131_0 + x_131_0 ≤ 0 ∧ x_131_0 − x_131_0 ≤ 0 ∧ − tmp_34_post + tmp_34_post ≤ 0 ∧ tmp_34_post − tmp_34_post ≤ 0 ∧ − tmp_34_0 + tmp_34_0 ≤ 0 ∧ tmp_34_0 − tmp_34_0 ≤ 0 ∧ − temp_35_post + temp_35_post ≤ 0 ∧ temp_35_post − temp_35_post ≤ 0 ∧ − temp_35_0 + temp_35_0 ≤ 0 ∧ temp_35_0 − temp_35_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 ∧ − tail_14_post + tail_14_post ≤ 0 ∧ tail_14_post − tail_14_post ≤ 0 ∧ − tail_14_0 + tail_14_0 ≤ 0 ∧ tail_14_0 − tail_14_0 ≤ 0 ∧ − t_22_post + t_22_post ≤ 0 ∧ t_22_post − t_22_post ≤ 0 ∧ − t_22_0 + t_22_0 ≤ 0 ∧ t_22_0 − t_22_0 ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_post + result_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_post − result_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_2 + result_dot_nondet_sdv_special_RETURN_VALUE_13_2 ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_2 ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_0 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post ≤ 0 ∧ − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0 ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0 − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_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_89_post + rcd_89_post ≤ 0 ∧ rcd_89_post − rcd_89_post ≤ 0 ∧ − rcd_89_0 + rcd_89_0 ≤ 0 ∧ rcd_89_0 − rcd_89_0 ≤ 0 ∧ − rcd_59_post + rcd_59_post ≤ 0 ∧ rcd_59_post − rcd_59_post ≤ 0 ∧ − rcd_59_0 + rcd_59_0 ≤ 0 ∧ rcd_59_0 − rcd_59_0 ≤ 0 ∧ − r_39_post + r_39_post ≤ 0 ∧ r_39_post − r_39_post ≤ 0 ∧ − r_39_0 + r_39_0 ≤ 0 ∧ r_39_0 − r_39_0 ≤ 0 ∧ − r_165_post + r_165_post ≤ 0 ∧ r_165_post − r_165_post ≤ 0 ∧ − r_165_0 + r_165_0 ≤ 0 ∧ r_165_0 − r_165_0 ≤ 0 ∧ − r_126_post + r_126_post ≤ 0 ∧ r_126_post − r_126_post ≤ 0 ∧ − r_126_0 + r_126_0 ≤ 0 ∧ r_126_0 − r_126_0 ≤ 0 ∧ − nondet_12_post + nondet_12_post ≤ 0 ∧ nondet_12_post − nondet_12_post ≤ 0 ∧ − nondet_12_1 + nondet_12_1 ≤ 0 ∧ nondet_12_1 − nondet_12_1 ≤ 0 ∧ − nondet_12_0 + nondet_12_0 ≤ 0 ∧ nondet_12_0 − nondet_12_0 ≤ 0 ∧ − length_28_post + length_28_post ≤ 0 ∧ length_28_post − length_28_post ≤ 0 ∧ − length_28_0 + length_28_0 ≤ 0 ∧ length_28_0 − length_28_0 ≤ 0 ∧ − len_187_post + len_187_post ≤ 0 ∧ len_187_post − len_187_post ≤ 0 ∧ − len_187_0 + len_187_0 ≤ 0 ∧ len_187_0 − len_187_0 ≤ 0 ∧ − len_134_post + len_134_post ≤ 0 ∧ len_134_post − len_134_post ≤ 0 ∧ − len_134_0 + len_134_0 ≤ 0 ∧ len_134_0 − len_134_0 ≤ 0 ∧ − i_95_post + i_95_post ≤ 0 ∧ i_95_post − i_95_post ≤ 0 ∧ − i_95_0 + i_95_0 ≤ 0 ∧ i_95_0 − i_95_0 ≤ 0 ∧ − i_30_post + i_30_post ≤ 0 ∧ i_30_post − i_30_post ≤ 0 ∧ − i_30_0 + i_30_0 ≤ 0 ∧ i_30_0 − i_30_0 ≤ 0 ∧ − i_110_post + i_110_post ≤ 0 ∧ i_110_post − i_110_post ≤ 0 ∧ − i_110_0 + i_110_0 ≤ 0 ∧ i_110_0 − i_110_0 ≤ 0 ∧ − head_SLAM_f_29_post + head_SLAM_f_29_post ≤ 0 ∧ head_SLAM_f_29_post − head_SLAM_f_29_post ≤ 0 ∧ − head_SLAM_f_29_0 + head_SLAM_f_29_0 ≤ 0 ∧ head_SLAM_f_29_0 − head_SLAM_f_29_0 ≤ 0 ∧ − head_32_post + head_32_post ≤ 0 ∧ head_32_post − head_32_post ≤ 0 ∧ − head_32_0 + head_32_0 ≤ 0 ∧ head_32_0 − head_32_0 ≤ 0 ∧ − head_15_post + head_15_post ≤ 0 ∧ head_15_post − head_15_post ≤ 0 ∧ − head_15_0 + head_15_0 ≤ 0 ∧ head_15_0 − head_15_0 ≤ 0 ∧ − f_171_post + f_171_post ≤ 0 ∧ f_171_post − f_171_post ≤ 0 ∧ − f_171_0 + f_171_0 ≤ 0 ∧ f_171_0 − f_171_0 ≤ 0 ∧ − a_343_post + a_343_post ≤ 0 ∧ a_343_post − a_343_post ≤ 0 ∧ − a_343_0 + a_343_0 ≤ 0 ∧ a_343_0 − a_343_0 ≤ 0 ∧ − a_342_post + a_342_post ≤ 0 ∧ a_342_post − a_342_post ≤ 0 ∧ − a_342_0 + a_342_0 ≤ 0 ∧ a_342_0 − a_342_0 ≤ 0 ∧ − a_289_post + a_289_post ≤ 0 ∧ a_289_post − a_289_post ≤ 0 ∧ − a_289_0 + a_289_0 ≤ 0 ∧ a_289_0 − a_289_0 ≤ 0 ∧ − a_281_post + a_281_post ≤ 0 ∧ a_281_post − a_281_post ≤ 0 ∧ − a_281_0 + a_281_0 ≤ 0 ∧ a_281_0 − a_281_0 ≤ 0 ∧ − a_225_post + a_225_post ≤ 0 ∧ a_225_post − a_225_post ≤ 0 ∧ − a_225_0 + a_225_0 ≤ 0 ∧ a_225_0 − a_225_0 ≤ 0 ∧ − a_188_post + a_188_post ≤ 0 ∧ a_188_post − a_188_post ≤ 0 ∧ − a_188_0 + a_188_0 ≤ 0 ∧ a_188_0 − a_188_0 ≤ 0 ∧ − a_149_post + a_149_post ≤ 0 ∧ a_149_post − a_149_post ≤ 0 ∧ − a_149_0 + a_149_0 ≤ 0 ∧ a_149_0 − a_149_0 ≤ 0 ∧ − a_118_post + a_118_post ≤ 0 ∧ a_118_post − a_118_post ≤ 0 ∧ − a_118_0 + a_118_0 ≤ 0 ∧ a_118_0 − a_118_0 ≤ 0

5 Location Addition

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

6* 84 6: − y_25_post + y_25_post ≤ 0 ∧ y_25_post − y_25_post ≤ 0 ∧ − y_25_1 + y_25_1 ≤ 0 ∧ y_25_1 − y_25_1 ≤ 0 ∧ − y_25_0 + y_25_0 ≤ 0 ∧ y_25_0 − y_25_0 ≤ 0 ∧ − y_18_post + y_18_post ≤ 0 ∧ y_18_post − y_18_post ≤ 0 ∧ − y_18_1 + y_18_1 ≤ 0 ∧ y_18_1 − y_18_1 ≤ 0 ∧ − y_18_0 + y_18_0 ≤ 0 ∧ y_18_0 − y_18_0 ≤ 0 ∧ − x_SLAM_f_24_post + x_SLAM_f_24_post ≤ 0 ∧ x_SLAM_f_24_post − x_SLAM_f_24_post ≤ 0 ∧ − x_SLAM_f_24_1 + x_SLAM_f_24_1 ≤ 0 ∧ x_SLAM_f_24_1 − x_SLAM_f_24_1 ≤ 0 ∧ − x_SLAM_f_24_0 + x_SLAM_f_24_0 ≤ 0 ∧ x_SLAM_f_24_0 − x_SLAM_f_24_0 ≤ 0 ∧ − x_SLAM_f_17_post + x_SLAM_f_17_post ≤ 0 ∧ x_SLAM_f_17_post − x_SLAM_f_17_post ≤ 0 ∧ − x_SLAM_f_17_1 + x_SLAM_f_17_1 ≤ 0 ∧ x_SLAM_f_17_1 − x_SLAM_f_17_1 ≤ 0 ∧ − x_SLAM_f_17_0 + x_SLAM_f_17_0 ≤ 0 ∧ x_SLAM_f_17_0 − x_SLAM_f_17_0 ≤ 0 ∧ − x_26_post + x_26_post ≤ 0 ∧ x_26_post − x_26_post ≤ 0 ∧ − x_26_1 + x_26_1 ≤ 0 ∧ x_26_1 − x_26_1 ≤ 0 ∧ − x_26_0 + x_26_0 ≤ 0 ∧ x_26_0 − x_26_0 ≤ 0 ∧ − x_19_post + x_19_post ≤ 0 ∧ x_19_post − x_19_post ≤ 0 ∧ − x_19_1 + x_19_1 ≤ 0 ∧ x_19_1 − x_19_1 ≤ 0 ∧ − x_19_0 + x_19_0 ≤ 0 ∧ x_19_0 − x_19_0 ≤ 0 ∧ − x_176_post + x_176_post ≤ 0 ∧ x_176_post − x_176_post ≤ 0 ∧ − x_176_0 + x_176_0 ≤ 0 ∧ x_176_0 − x_176_0 ≤ 0 ∧ − x_131_post + x_131_post ≤ 0 ∧ x_131_post − x_131_post ≤ 0 ∧ − x_131_0 + x_131_0 ≤ 0 ∧ x_131_0 − x_131_0 ≤ 0 ∧ − tmp_34_post + tmp_34_post ≤ 0 ∧ tmp_34_post − tmp_34_post ≤ 0 ∧ − tmp_34_0 + tmp_34_0 ≤ 0 ∧ tmp_34_0 − tmp_34_0 ≤ 0 ∧ − temp_35_post + temp_35_post ≤ 0 ∧ temp_35_post − temp_35_post ≤ 0 ∧ − temp_35_0 + temp_35_0 ≤ 0 ∧ temp_35_0 − temp_35_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 ∧ − tail_14_post + tail_14_post ≤ 0 ∧ tail_14_post − tail_14_post ≤ 0 ∧ − tail_14_0 + tail_14_0 ≤ 0 ∧ tail_14_0 − tail_14_0 ≤ 0 ∧ − t_22_post + t_22_post ≤ 0 ∧ t_22_post − t_22_post ≤ 0 ∧ − t_22_0 + t_22_0 ≤ 0 ∧ t_22_0 − t_22_0 ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_post + result_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_post − result_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_2 + result_dot_nondet_sdv_special_RETURN_VALUE_13_2 ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_2 ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_0 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post ≤ 0 ∧ − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0 ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0 − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_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_89_post + rcd_89_post ≤ 0 ∧ rcd_89_post − rcd_89_post ≤ 0 ∧ − rcd_89_0 + rcd_89_0 ≤ 0 ∧ rcd_89_0 − rcd_89_0 ≤ 0 ∧ − rcd_59_post + rcd_59_post ≤ 0 ∧ rcd_59_post − rcd_59_post ≤ 0 ∧ − rcd_59_0 + rcd_59_0 ≤ 0 ∧ rcd_59_0 − rcd_59_0 ≤ 0 ∧ − r_39_post + r_39_post ≤ 0 ∧ r_39_post − r_39_post ≤ 0 ∧ − r_39_0 + r_39_0 ≤ 0 ∧ r_39_0 − r_39_0 ≤ 0 ∧ − r_165_post + r_165_post ≤ 0 ∧ r_165_post − r_165_post ≤ 0 ∧ − r_165_0 + r_165_0 ≤ 0 ∧ r_165_0 − r_165_0 ≤ 0 ∧ − r_126_post + r_126_post ≤ 0 ∧ r_126_post − r_126_post ≤ 0 ∧ − r_126_0 + r_126_0 ≤ 0 ∧ r_126_0 − r_126_0 ≤ 0 ∧ − nondet_12_post + nondet_12_post ≤ 0 ∧ nondet_12_post − nondet_12_post ≤ 0 ∧ − nondet_12_1 + nondet_12_1 ≤ 0 ∧ nondet_12_1 − nondet_12_1 ≤ 0 ∧ − nondet_12_0 + nondet_12_0 ≤ 0 ∧ nondet_12_0 − nondet_12_0 ≤ 0 ∧ − length_28_post + length_28_post ≤ 0 ∧ length_28_post − length_28_post ≤ 0 ∧ − length_28_0 + length_28_0 ≤ 0 ∧ length_28_0 − length_28_0 ≤ 0 ∧ − len_187_post + len_187_post ≤ 0 ∧ len_187_post − len_187_post ≤ 0 ∧ − len_187_0 + len_187_0 ≤ 0 ∧ len_187_0 − len_187_0 ≤ 0 ∧ − len_134_post + len_134_post ≤ 0 ∧ len_134_post − len_134_post ≤ 0 ∧ − len_134_0 + len_134_0 ≤ 0 ∧ len_134_0 − len_134_0 ≤ 0 ∧ − i_95_post + i_95_post ≤ 0 ∧ i_95_post − i_95_post ≤ 0 ∧ − i_95_0 + i_95_0 ≤ 0 ∧ i_95_0 − i_95_0 ≤ 0 ∧ − i_30_post + i_30_post ≤ 0 ∧ i_30_post − i_30_post ≤ 0 ∧ − i_30_0 + i_30_0 ≤ 0 ∧ i_30_0 − i_30_0 ≤ 0 ∧ − i_110_post + i_110_post ≤ 0 ∧ i_110_post − i_110_post ≤ 0 ∧ − i_110_0 + i_110_0 ≤ 0 ∧ i_110_0 − i_110_0 ≤ 0 ∧ − head_SLAM_f_29_post + head_SLAM_f_29_post ≤ 0 ∧ head_SLAM_f_29_post − head_SLAM_f_29_post ≤ 0 ∧ − head_SLAM_f_29_0 + head_SLAM_f_29_0 ≤ 0 ∧ head_SLAM_f_29_0 − head_SLAM_f_29_0 ≤ 0 ∧ − head_32_post + head_32_post ≤ 0 ∧ head_32_post − head_32_post ≤ 0 ∧ − head_32_0 + head_32_0 ≤ 0 ∧ head_32_0 − head_32_0 ≤ 0 ∧ − head_15_post + head_15_post ≤ 0 ∧ head_15_post − head_15_post ≤ 0 ∧ − head_15_0 + head_15_0 ≤ 0 ∧ head_15_0 − head_15_0 ≤ 0 ∧ − f_171_post + f_171_post ≤ 0 ∧ f_171_post − f_171_post ≤ 0 ∧ − f_171_0 + f_171_0 ≤ 0 ∧ f_171_0 − f_171_0 ≤ 0 ∧ − a_343_post + a_343_post ≤ 0 ∧ a_343_post − a_343_post ≤ 0 ∧ − a_343_0 + a_343_0 ≤ 0 ∧ a_343_0 − a_343_0 ≤ 0 ∧ − a_342_post + a_342_post ≤ 0 ∧ a_342_post − a_342_post ≤ 0 ∧ − a_342_0 + a_342_0 ≤ 0 ∧ a_342_0 − a_342_0 ≤ 0 ∧ − a_289_post + a_289_post ≤ 0 ∧ a_289_post − a_289_post ≤ 0 ∧ − a_289_0 + a_289_0 ≤ 0 ∧ a_289_0 − a_289_0 ≤ 0 ∧ − a_281_post + a_281_post ≤ 0 ∧ a_281_post − a_281_post ≤ 0 ∧ − a_281_0 + a_281_0 ≤ 0 ∧ a_281_0 − a_281_0 ≤ 0 ∧ − a_225_post + a_225_post ≤ 0 ∧ a_225_post − a_225_post ≤ 0 ∧ − a_225_0 + a_225_0 ≤ 0 ∧ a_225_0 − a_225_0 ≤ 0 ∧ − a_188_post + a_188_post ≤ 0 ∧ a_188_post − a_188_post ≤ 0 ∧ − a_188_0 + a_188_0 ≤ 0 ∧ a_188_0 − a_188_0 ≤ 0 ∧ − a_149_post + a_149_post ≤ 0 ∧ a_149_post − a_149_post ≤ 0 ∧ − a_149_0 + a_149_0 ≤ 0 ∧ a_149_0 − a_149_0 ≤ 0 ∧ − a_118_post + a_118_post ≤ 0 ∧ a_118_post − a_118_post ≤ 0 ∧ − a_118_0 + a_118_0 ≤ 0 ∧ a_118_0 − a_118_0 ≤ 0

6 Location Addition

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

6 82 6_var_snapshot: − y_25_post + y_25_post ≤ 0 ∧ y_25_post − y_25_post ≤ 0 ∧ − y_25_1 + y_25_1 ≤ 0 ∧ y_25_1 − y_25_1 ≤ 0 ∧ − y_25_0 + y_25_0 ≤ 0 ∧ y_25_0 − y_25_0 ≤ 0 ∧ − y_18_post + y_18_post ≤ 0 ∧ y_18_post − y_18_post ≤ 0 ∧ − y_18_1 + y_18_1 ≤ 0 ∧ y_18_1 − y_18_1 ≤ 0 ∧ − y_18_0 + y_18_0 ≤ 0 ∧ y_18_0 − y_18_0 ≤ 0 ∧ − x_SLAM_f_24_post + x_SLAM_f_24_post ≤ 0 ∧ x_SLAM_f_24_post − x_SLAM_f_24_post ≤ 0 ∧ − x_SLAM_f_24_1 + x_SLAM_f_24_1 ≤ 0 ∧ x_SLAM_f_24_1 − x_SLAM_f_24_1 ≤ 0 ∧ − x_SLAM_f_24_0 + x_SLAM_f_24_0 ≤ 0 ∧ x_SLAM_f_24_0 − x_SLAM_f_24_0 ≤ 0 ∧ − x_SLAM_f_17_post + x_SLAM_f_17_post ≤ 0 ∧ x_SLAM_f_17_post − x_SLAM_f_17_post ≤ 0 ∧ − x_SLAM_f_17_1 + x_SLAM_f_17_1 ≤ 0 ∧ x_SLAM_f_17_1 − x_SLAM_f_17_1 ≤ 0 ∧ − x_SLAM_f_17_0 + x_SLAM_f_17_0 ≤ 0 ∧ x_SLAM_f_17_0 − x_SLAM_f_17_0 ≤ 0 ∧ − x_26_post + x_26_post ≤ 0 ∧ x_26_post − x_26_post ≤ 0 ∧ − x_26_1 + x_26_1 ≤ 0 ∧ x_26_1 − x_26_1 ≤ 0 ∧ − x_26_0 + x_26_0 ≤ 0 ∧ x_26_0 − x_26_0 ≤ 0 ∧ − x_19_post + x_19_post ≤ 0 ∧ x_19_post − x_19_post ≤ 0 ∧ − x_19_1 + x_19_1 ≤ 0 ∧ x_19_1 − x_19_1 ≤ 0 ∧ − x_19_0 + x_19_0 ≤ 0 ∧ x_19_0 − x_19_0 ≤ 0 ∧ − x_176_post + x_176_post ≤ 0 ∧ x_176_post − x_176_post ≤ 0 ∧ − x_176_0 + x_176_0 ≤ 0 ∧ x_176_0 − x_176_0 ≤ 0 ∧ − x_131_post + x_131_post ≤ 0 ∧ x_131_post − x_131_post ≤ 0 ∧ − x_131_0 + x_131_0 ≤ 0 ∧ x_131_0 − x_131_0 ≤ 0 ∧ − tmp_34_post + tmp_34_post ≤ 0 ∧ tmp_34_post − tmp_34_post ≤ 0 ∧ − tmp_34_0 + tmp_34_0 ≤ 0 ∧ tmp_34_0 − tmp_34_0 ≤ 0 ∧ − temp_35_post + temp_35_post ≤ 0 ∧ temp_35_post − temp_35_post ≤ 0 ∧ − temp_35_0 + temp_35_0 ≤ 0 ∧ temp_35_0 − temp_35_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 ∧ − tail_14_post + tail_14_post ≤ 0 ∧ tail_14_post − tail_14_post ≤ 0 ∧ − tail_14_0 + tail_14_0 ≤ 0 ∧ tail_14_0 − tail_14_0 ≤ 0 ∧ − t_22_post + t_22_post ≤ 0 ∧ t_22_post − t_22_post ≤ 0 ∧ − t_22_0 + t_22_0 ≤ 0 ∧ t_22_0 − t_22_0 ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_post + result_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_post − result_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_2 + result_dot_nondet_sdv_special_RETURN_VALUE_13_2 ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_2 ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_0 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post ≤ 0 ∧ − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0 ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0 − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_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_89_post + rcd_89_post ≤ 0 ∧ rcd_89_post − rcd_89_post ≤ 0 ∧ − rcd_89_0 + rcd_89_0 ≤ 0 ∧ rcd_89_0 − rcd_89_0 ≤ 0 ∧ − rcd_59_post + rcd_59_post ≤ 0 ∧ rcd_59_post − rcd_59_post ≤ 0 ∧ − rcd_59_0 + rcd_59_0 ≤ 0 ∧ rcd_59_0 − rcd_59_0 ≤ 0 ∧ − r_39_post + r_39_post ≤ 0 ∧ r_39_post − r_39_post ≤ 0 ∧ − r_39_0 + r_39_0 ≤ 0 ∧ r_39_0 − r_39_0 ≤ 0 ∧ − r_165_post + r_165_post ≤ 0 ∧ r_165_post − r_165_post ≤ 0 ∧ − r_165_0 + r_165_0 ≤ 0 ∧ r_165_0 − r_165_0 ≤ 0 ∧ − r_126_post + r_126_post ≤ 0 ∧ r_126_post − r_126_post ≤ 0 ∧ − r_126_0 + r_126_0 ≤ 0 ∧ r_126_0 − r_126_0 ≤ 0 ∧ − nondet_12_post + nondet_12_post ≤ 0 ∧ nondet_12_post − nondet_12_post ≤ 0 ∧ − nondet_12_1 + nondet_12_1 ≤ 0 ∧ nondet_12_1 − nondet_12_1 ≤ 0 ∧ − nondet_12_0 + nondet_12_0 ≤ 0 ∧ nondet_12_0 − nondet_12_0 ≤ 0 ∧ − length_28_post + length_28_post ≤ 0 ∧ length_28_post − length_28_post ≤ 0 ∧ − length_28_0 + length_28_0 ≤ 0 ∧ length_28_0 − length_28_0 ≤ 0 ∧ − len_187_post + len_187_post ≤ 0 ∧ len_187_post − len_187_post ≤ 0 ∧ − len_187_0 + len_187_0 ≤ 0 ∧ len_187_0 − len_187_0 ≤ 0 ∧ − len_134_post + len_134_post ≤ 0 ∧ len_134_post − len_134_post ≤ 0 ∧ − len_134_0 + len_134_0 ≤ 0 ∧ len_134_0 − len_134_0 ≤ 0 ∧ − i_95_post + i_95_post ≤ 0 ∧ i_95_post − i_95_post ≤ 0 ∧ − i_95_0 + i_95_0 ≤ 0 ∧ i_95_0 − i_95_0 ≤ 0 ∧ − i_30_post + i_30_post ≤ 0 ∧ i_30_post − i_30_post ≤ 0 ∧ − i_30_0 + i_30_0 ≤ 0 ∧ i_30_0 − i_30_0 ≤ 0 ∧ − i_110_post + i_110_post ≤ 0 ∧ i_110_post − i_110_post ≤ 0 ∧ − i_110_0 + i_110_0 ≤ 0 ∧ i_110_0 − i_110_0 ≤ 0 ∧ − head_SLAM_f_29_post + head_SLAM_f_29_post ≤ 0 ∧ head_SLAM_f_29_post − head_SLAM_f_29_post ≤ 0 ∧ − head_SLAM_f_29_0 + head_SLAM_f_29_0 ≤ 0 ∧ head_SLAM_f_29_0 − head_SLAM_f_29_0 ≤ 0 ∧ − head_32_post + head_32_post ≤ 0 ∧ head_32_post − head_32_post ≤ 0 ∧ − head_32_0 + head_32_0 ≤ 0 ∧ head_32_0 − head_32_0 ≤ 0 ∧ − head_15_post + head_15_post ≤ 0 ∧ head_15_post − head_15_post ≤ 0 ∧ − head_15_0 + head_15_0 ≤ 0 ∧ head_15_0 − head_15_0 ≤ 0 ∧ − f_171_post + f_171_post ≤ 0 ∧ f_171_post − f_171_post ≤ 0 ∧ − f_171_0 + f_171_0 ≤ 0 ∧ f_171_0 − f_171_0 ≤ 0 ∧ − a_343_post + a_343_post ≤ 0 ∧ a_343_post − a_343_post ≤ 0 ∧ − a_343_0 + a_343_0 ≤ 0 ∧ a_343_0 − a_343_0 ≤ 0 ∧ − a_342_post + a_342_post ≤ 0 ∧ a_342_post − a_342_post ≤ 0 ∧ − a_342_0 + a_342_0 ≤ 0 ∧ a_342_0 − a_342_0 ≤ 0 ∧ − a_289_post + a_289_post ≤ 0 ∧ a_289_post − a_289_post ≤ 0 ∧ − a_289_0 + a_289_0 ≤ 0 ∧ a_289_0 − a_289_0 ≤ 0 ∧ − a_281_post + a_281_post ≤ 0 ∧ a_281_post − a_281_post ≤ 0 ∧ − a_281_0 + a_281_0 ≤ 0 ∧ a_281_0 − a_281_0 ≤ 0 ∧ − a_225_post + a_225_post ≤ 0 ∧ a_225_post − a_225_post ≤ 0 ∧ − a_225_0 + a_225_0 ≤ 0 ∧ a_225_0 − a_225_0 ≤ 0 ∧ − a_188_post + a_188_post ≤ 0 ∧ a_188_post − a_188_post ≤ 0 ∧ − a_188_0 + a_188_0 ≤ 0 ∧ a_188_0 − a_188_0 ≤ 0 ∧ − a_149_post + a_149_post ≤ 0 ∧ a_149_post − a_149_post ≤ 0 ∧ − a_149_0 + a_149_0 ≤ 0 ∧ a_149_0 − a_149_0 ≤ 0 ∧ − a_118_post + a_118_post ≤ 0 ∧ a_118_post − a_118_post ≤ 0 ∧ − a_118_0 + a_118_0 ≤ 0 ∧ a_118_0 − a_118_0 ≤ 0

7 Location Addition

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

31* 91 31: − y_25_post + y_25_post ≤ 0 ∧ y_25_post − y_25_post ≤ 0 ∧ − y_25_1 + y_25_1 ≤ 0 ∧ y_25_1 − y_25_1 ≤ 0 ∧ − y_25_0 + y_25_0 ≤ 0 ∧ y_25_0 − y_25_0 ≤ 0 ∧ − y_18_post + y_18_post ≤ 0 ∧ y_18_post − y_18_post ≤ 0 ∧ − y_18_1 + y_18_1 ≤ 0 ∧ y_18_1 − y_18_1 ≤ 0 ∧ − y_18_0 + y_18_0 ≤ 0 ∧ y_18_0 − y_18_0 ≤ 0 ∧ − x_SLAM_f_24_post + x_SLAM_f_24_post ≤ 0 ∧ x_SLAM_f_24_post − x_SLAM_f_24_post ≤ 0 ∧ − x_SLAM_f_24_1 + x_SLAM_f_24_1 ≤ 0 ∧ x_SLAM_f_24_1 − x_SLAM_f_24_1 ≤ 0 ∧ − x_SLAM_f_24_0 + x_SLAM_f_24_0 ≤ 0 ∧ x_SLAM_f_24_0 − x_SLAM_f_24_0 ≤ 0 ∧ − x_SLAM_f_17_post + x_SLAM_f_17_post ≤ 0 ∧ x_SLAM_f_17_post − x_SLAM_f_17_post ≤ 0 ∧ − x_SLAM_f_17_1 + x_SLAM_f_17_1 ≤ 0 ∧ x_SLAM_f_17_1 − x_SLAM_f_17_1 ≤ 0 ∧ − x_SLAM_f_17_0 + x_SLAM_f_17_0 ≤ 0 ∧ x_SLAM_f_17_0 − x_SLAM_f_17_0 ≤ 0 ∧ − x_26_post + x_26_post ≤ 0 ∧ x_26_post − x_26_post ≤ 0 ∧ − x_26_1 + x_26_1 ≤ 0 ∧ x_26_1 − x_26_1 ≤ 0 ∧ − x_26_0 + x_26_0 ≤ 0 ∧ x_26_0 − x_26_0 ≤ 0 ∧ − x_19_post + x_19_post ≤ 0 ∧ x_19_post − x_19_post ≤ 0 ∧ − x_19_1 + x_19_1 ≤ 0 ∧ x_19_1 − x_19_1 ≤ 0 ∧ − x_19_0 + x_19_0 ≤ 0 ∧ x_19_0 − x_19_0 ≤ 0 ∧ − x_176_post + x_176_post ≤ 0 ∧ x_176_post − x_176_post ≤ 0 ∧ − x_176_0 + x_176_0 ≤ 0 ∧ x_176_0 − x_176_0 ≤ 0 ∧ − x_131_post + x_131_post ≤ 0 ∧ x_131_post − x_131_post ≤ 0 ∧ − x_131_0 + x_131_0 ≤ 0 ∧ x_131_0 − x_131_0 ≤ 0 ∧ − tmp_34_post + tmp_34_post ≤ 0 ∧ tmp_34_post − tmp_34_post ≤ 0 ∧ − tmp_34_0 + tmp_34_0 ≤ 0 ∧ tmp_34_0 − tmp_34_0 ≤ 0 ∧ − temp_35_post + temp_35_post ≤ 0 ∧ temp_35_post − temp_35_post ≤ 0 ∧ − temp_35_0 + temp_35_0 ≤ 0 ∧ temp_35_0 − temp_35_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 ∧ − tail_14_post + tail_14_post ≤ 0 ∧ tail_14_post − tail_14_post ≤ 0 ∧ − tail_14_0 + tail_14_0 ≤ 0 ∧ tail_14_0 − tail_14_0 ≤ 0 ∧ − t_22_post + t_22_post ≤ 0 ∧ t_22_post − t_22_post ≤ 0 ∧ − t_22_0 + t_22_0 ≤ 0 ∧ t_22_0 − t_22_0 ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_post + result_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_post − result_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_2 + result_dot_nondet_sdv_special_RETURN_VALUE_13_2 ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_2 ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_0 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post ≤ 0 ∧ − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0 ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0 − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_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_89_post + rcd_89_post ≤ 0 ∧ rcd_89_post − rcd_89_post ≤ 0 ∧ − rcd_89_0 + rcd_89_0 ≤ 0 ∧ rcd_89_0 − rcd_89_0 ≤ 0 ∧ − rcd_59_post + rcd_59_post ≤ 0 ∧ rcd_59_post − rcd_59_post ≤ 0 ∧ − rcd_59_0 + rcd_59_0 ≤ 0 ∧ rcd_59_0 − rcd_59_0 ≤ 0 ∧ − r_39_post + r_39_post ≤ 0 ∧ r_39_post − r_39_post ≤ 0 ∧ − r_39_0 + r_39_0 ≤ 0 ∧ r_39_0 − r_39_0 ≤ 0 ∧ − r_165_post + r_165_post ≤ 0 ∧ r_165_post − r_165_post ≤ 0 ∧ − r_165_0 + r_165_0 ≤ 0 ∧ r_165_0 − r_165_0 ≤ 0 ∧ − r_126_post + r_126_post ≤ 0 ∧ r_126_post − r_126_post ≤ 0 ∧ − r_126_0 + r_126_0 ≤ 0 ∧ r_126_0 − r_126_0 ≤ 0 ∧ − nondet_12_post + nondet_12_post ≤ 0 ∧ nondet_12_post − nondet_12_post ≤ 0 ∧ − nondet_12_1 + nondet_12_1 ≤ 0 ∧ nondet_12_1 − nondet_12_1 ≤ 0 ∧ − nondet_12_0 + nondet_12_0 ≤ 0 ∧ nondet_12_0 − nondet_12_0 ≤ 0 ∧ − length_28_post + length_28_post ≤ 0 ∧ length_28_post − length_28_post ≤ 0 ∧ − length_28_0 + length_28_0 ≤ 0 ∧ length_28_0 − length_28_0 ≤ 0 ∧ − len_187_post + len_187_post ≤ 0 ∧ len_187_post − len_187_post ≤ 0 ∧ − len_187_0 + len_187_0 ≤ 0 ∧ len_187_0 − len_187_0 ≤ 0 ∧ − len_134_post + len_134_post ≤ 0 ∧ len_134_post − len_134_post ≤ 0 ∧ − len_134_0 + len_134_0 ≤ 0 ∧ len_134_0 − len_134_0 ≤ 0 ∧ − i_95_post + i_95_post ≤ 0 ∧ i_95_post − i_95_post ≤ 0 ∧ − i_95_0 + i_95_0 ≤ 0 ∧ i_95_0 − i_95_0 ≤ 0 ∧ − i_30_post + i_30_post ≤ 0 ∧ i_30_post − i_30_post ≤ 0 ∧ − i_30_0 + i_30_0 ≤ 0 ∧ i_30_0 − i_30_0 ≤ 0 ∧ − i_110_post + i_110_post ≤ 0 ∧ i_110_post − i_110_post ≤ 0 ∧ − i_110_0 + i_110_0 ≤ 0 ∧ i_110_0 − i_110_0 ≤ 0 ∧ − head_SLAM_f_29_post + head_SLAM_f_29_post ≤ 0 ∧ head_SLAM_f_29_post − head_SLAM_f_29_post ≤ 0 ∧ − head_SLAM_f_29_0 + head_SLAM_f_29_0 ≤ 0 ∧ head_SLAM_f_29_0 − head_SLAM_f_29_0 ≤ 0 ∧ − head_32_post + head_32_post ≤ 0 ∧ head_32_post − head_32_post ≤ 0 ∧ − head_32_0 + head_32_0 ≤ 0 ∧ head_32_0 − head_32_0 ≤ 0 ∧ − head_15_post + head_15_post ≤ 0 ∧ head_15_post − head_15_post ≤ 0 ∧ − head_15_0 + head_15_0 ≤ 0 ∧ head_15_0 − head_15_0 ≤ 0 ∧ − f_171_post + f_171_post ≤ 0 ∧ f_171_post − f_171_post ≤ 0 ∧ − f_171_0 + f_171_0 ≤ 0 ∧ f_171_0 − f_171_0 ≤ 0 ∧ − a_343_post + a_343_post ≤ 0 ∧ a_343_post − a_343_post ≤ 0 ∧ − a_343_0 + a_343_0 ≤ 0 ∧ a_343_0 − a_343_0 ≤ 0 ∧ − a_342_post + a_342_post ≤ 0 ∧ a_342_post − a_342_post ≤ 0 ∧ − a_342_0 + a_342_0 ≤ 0 ∧ a_342_0 − a_342_0 ≤ 0 ∧ − a_289_post + a_289_post ≤ 0 ∧ a_289_post − a_289_post ≤ 0 ∧ − a_289_0 + a_289_0 ≤ 0 ∧ a_289_0 − a_289_0 ≤ 0 ∧ − a_281_post + a_281_post ≤ 0 ∧ a_281_post − a_281_post ≤ 0 ∧ − a_281_0 + a_281_0 ≤ 0 ∧ a_281_0 − a_281_0 ≤ 0 ∧ − a_225_post + a_225_post ≤ 0 ∧ a_225_post − a_225_post ≤ 0 ∧ − a_225_0 + a_225_0 ≤ 0 ∧ a_225_0 − a_225_0 ≤ 0 ∧ − a_188_post + a_188_post ≤ 0 ∧ a_188_post − a_188_post ≤ 0 ∧ − a_188_0 + a_188_0 ≤ 0 ∧ a_188_0 − a_188_0 ≤ 0 ∧ − a_149_post + a_149_post ≤ 0 ∧ a_149_post − a_149_post ≤ 0 ∧ − a_149_0 + a_149_0 ≤ 0 ∧ a_149_0 − a_149_0 ≤ 0 ∧ − a_118_post + a_118_post ≤ 0 ∧ a_118_post − a_118_post ≤ 0 ∧ − a_118_0 + a_118_0 ≤ 0 ∧ a_118_0 − a_118_0 ≤ 0

8 Location Addition

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

31 89 31_var_snapshot: − y_25_post + y_25_post ≤ 0 ∧ y_25_post − y_25_post ≤ 0 ∧ − y_25_1 + y_25_1 ≤ 0 ∧ y_25_1 − y_25_1 ≤ 0 ∧ − y_25_0 + y_25_0 ≤ 0 ∧ y_25_0 − y_25_0 ≤ 0 ∧ − y_18_post + y_18_post ≤ 0 ∧ y_18_post − y_18_post ≤ 0 ∧ − y_18_1 + y_18_1 ≤ 0 ∧ y_18_1 − y_18_1 ≤ 0 ∧ − y_18_0 + y_18_0 ≤ 0 ∧ y_18_0 − y_18_0 ≤ 0 ∧ − x_SLAM_f_24_post + x_SLAM_f_24_post ≤ 0 ∧ x_SLAM_f_24_post − x_SLAM_f_24_post ≤ 0 ∧ − x_SLAM_f_24_1 + x_SLAM_f_24_1 ≤ 0 ∧ x_SLAM_f_24_1 − x_SLAM_f_24_1 ≤ 0 ∧ − x_SLAM_f_24_0 + x_SLAM_f_24_0 ≤ 0 ∧ x_SLAM_f_24_0 − x_SLAM_f_24_0 ≤ 0 ∧ − x_SLAM_f_17_post + x_SLAM_f_17_post ≤ 0 ∧ x_SLAM_f_17_post − x_SLAM_f_17_post ≤ 0 ∧ − x_SLAM_f_17_1 + x_SLAM_f_17_1 ≤ 0 ∧ x_SLAM_f_17_1 − x_SLAM_f_17_1 ≤ 0 ∧ − x_SLAM_f_17_0 + x_SLAM_f_17_0 ≤ 0 ∧ x_SLAM_f_17_0 − x_SLAM_f_17_0 ≤ 0 ∧ − x_26_post + x_26_post ≤ 0 ∧ x_26_post − x_26_post ≤ 0 ∧ − x_26_1 + x_26_1 ≤ 0 ∧ x_26_1 − x_26_1 ≤ 0 ∧ − x_26_0 + x_26_0 ≤ 0 ∧ x_26_0 − x_26_0 ≤ 0 ∧ − x_19_post + x_19_post ≤ 0 ∧ x_19_post − x_19_post ≤ 0 ∧ − x_19_1 + x_19_1 ≤ 0 ∧ x_19_1 − x_19_1 ≤ 0 ∧ − x_19_0 + x_19_0 ≤ 0 ∧ x_19_0 − x_19_0 ≤ 0 ∧ − x_176_post + x_176_post ≤ 0 ∧ x_176_post − x_176_post ≤ 0 ∧ − x_176_0 + x_176_0 ≤ 0 ∧ x_176_0 − x_176_0 ≤ 0 ∧ − x_131_post + x_131_post ≤ 0 ∧ x_131_post − x_131_post ≤ 0 ∧ − x_131_0 + x_131_0 ≤ 0 ∧ x_131_0 − x_131_0 ≤ 0 ∧ − tmp_34_post + tmp_34_post ≤ 0 ∧ tmp_34_post − tmp_34_post ≤ 0 ∧ − tmp_34_0 + tmp_34_0 ≤ 0 ∧ tmp_34_0 − tmp_34_0 ≤ 0 ∧ − temp_35_post + temp_35_post ≤ 0 ∧ temp_35_post − temp_35_post ≤ 0 ∧ − temp_35_0 + temp_35_0 ≤ 0 ∧ temp_35_0 − temp_35_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 ∧ − tail_14_post + tail_14_post ≤ 0 ∧ tail_14_post − tail_14_post ≤ 0 ∧ − tail_14_0 + tail_14_0 ≤ 0 ∧ tail_14_0 − tail_14_0 ≤ 0 ∧ − t_22_post + t_22_post ≤ 0 ∧ t_22_post − t_22_post ≤ 0 ∧ − t_22_0 + t_22_0 ≤ 0 ∧ t_22_0 − t_22_0 ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_post + result_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_post − result_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_2 + result_dot_nondet_sdv_special_RETURN_VALUE_13_2 ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_2 ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_0 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post ≤ 0 ∧ − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0 ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0 − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_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_89_post + rcd_89_post ≤ 0 ∧ rcd_89_post − rcd_89_post ≤ 0 ∧ − rcd_89_0 + rcd_89_0 ≤ 0 ∧ rcd_89_0 − rcd_89_0 ≤ 0 ∧ − rcd_59_post + rcd_59_post ≤ 0 ∧ rcd_59_post − rcd_59_post ≤ 0 ∧ − rcd_59_0 + rcd_59_0 ≤ 0 ∧ rcd_59_0 − rcd_59_0 ≤ 0 ∧ − r_39_post + r_39_post ≤ 0 ∧ r_39_post − r_39_post ≤ 0 ∧ − r_39_0 + r_39_0 ≤ 0 ∧ r_39_0 − r_39_0 ≤ 0 ∧ − r_165_post + r_165_post ≤ 0 ∧ r_165_post − r_165_post ≤ 0 ∧ − r_165_0 + r_165_0 ≤ 0 ∧ r_165_0 − r_165_0 ≤ 0 ∧ − r_126_post + r_126_post ≤ 0 ∧ r_126_post − r_126_post ≤ 0 ∧ − r_126_0 + r_126_0 ≤ 0 ∧ r_126_0 − r_126_0 ≤ 0 ∧ − nondet_12_post + nondet_12_post ≤ 0 ∧ nondet_12_post − nondet_12_post ≤ 0 ∧ − nondet_12_1 + nondet_12_1 ≤ 0 ∧ nondet_12_1 − nondet_12_1 ≤ 0 ∧ − nondet_12_0 + nondet_12_0 ≤ 0 ∧ nondet_12_0 − nondet_12_0 ≤ 0 ∧ − length_28_post + length_28_post ≤ 0 ∧ length_28_post − length_28_post ≤ 0 ∧ − length_28_0 + length_28_0 ≤ 0 ∧ length_28_0 − length_28_0 ≤ 0 ∧ − len_187_post + len_187_post ≤ 0 ∧ len_187_post − len_187_post ≤ 0 ∧ − len_187_0 + len_187_0 ≤ 0 ∧ len_187_0 − len_187_0 ≤ 0 ∧ − len_134_post + len_134_post ≤ 0 ∧ len_134_post − len_134_post ≤ 0 ∧ − len_134_0 + len_134_0 ≤ 0 ∧ len_134_0 − len_134_0 ≤ 0 ∧ − i_95_post + i_95_post ≤ 0 ∧ i_95_post − i_95_post ≤ 0 ∧ − i_95_0 + i_95_0 ≤ 0 ∧ i_95_0 − i_95_0 ≤ 0 ∧ − i_30_post + i_30_post ≤ 0 ∧ i_30_post − i_30_post ≤ 0 ∧ − i_30_0 + i_30_0 ≤ 0 ∧ i_30_0 − i_30_0 ≤ 0 ∧ − i_110_post + i_110_post ≤ 0 ∧ i_110_post − i_110_post ≤ 0 ∧ − i_110_0 + i_110_0 ≤ 0 ∧ i_110_0 − i_110_0 ≤ 0 ∧ − head_SLAM_f_29_post + head_SLAM_f_29_post ≤ 0 ∧ head_SLAM_f_29_post − head_SLAM_f_29_post ≤ 0 ∧ − head_SLAM_f_29_0 + head_SLAM_f_29_0 ≤ 0 ∧ head_SLAM_f_29_0 − head_SLAM_f_29_0 ≤ 0 ∧ − head_32_post + head_32_post ≤ 0 ∧ head_32_post − head_32_post ≤ 0 ∧ − head_32_0 + head_32_0 ≤ 0 ∧ head_32_0 − head_32_0 ≤ 0 ∧ − head_15_post + head_15_post ≤ 0 ∧ head_15_post − head_15_post ≤ 0 ∧ − head_15_0 + head_15_0 ≤ 0 ∧ head_15_0 − head_15_0 ≤ 0 ∧ − f_171_post + f_171_post ≤ 0 ∧ f_171_post − f_171_post ≤ 0 ∧ − f_171_0 + f_171_0 ≤ 0 ∧ f_171_0 − f_171_0 ≤ 0 ∧ − a_343_post + a_343_post ≤ 0 ∧ a_343_post − a_343_post ≤ 0 ∧ − a_343_0 + a_343_0 ≤ 0 ∧ a_343_0 − a_343_0 ≤ 0 ∧ − a_342_post + a_342_post ≤ 0 ∧ a_342_post − a_342_post ≤ 0 ∧ − a_342_0 + a_342_0 ≤ 0 ∧ a_342_0 − a_342_0 ≤ 0 ∧ − a_289_post + a_289_post ≤ 0 ∧ a_289_post − a_289_post ≤ 0 ∧ − a_289_0 + a_289_0 ≤ 0 ∧ a_289_0 − a_289_0 ≤ 0 ∧ − a_281_post + a_281_post ≤ 0 ∧ a_281_post − a_281_post ≤ 0 ∧ − a_281_0 + a_281_0 ≤ 0 ∧ a_281_0 − a_281_0 ≤ 0 ∧ − a_225_post + a_225_post ≤ 0 ∧ a_225_post − a_225_post ≤ 0 ∧ − a_225_0 + a_225_0 ≤ 0 ∧ a_225_0 − a_225_0 ≤ 0 ∧ − a_188_post + a_188_post ≤ 0 ∧ a_188_post − a_188_post ≤ 0 ∧ − a_188_0 + a_188_0 ≤ 0 ∧ a_188_0 − a_188_0 ≤ 0 ∧ − a_149_post + a_149_post ≤ 0 ∧ a_149_post − a_149_post ≤ 0 ∧ − a_149_0 + a_149_0 ≤ 0 ∧ a_149_0 − a_149_0 ≤ 0 ∧ − a_118_post + a_118_post ≤ 0 ∧ a_118_post − a_118_post ≤ 0 ∧ − a_118_0 + a_118_0 ≤ 0 ∧ a_118_0 − a_118_0 ≤ 0

9 SCC Decomposition

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

9.1 SCC Subproblem 1/3

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

9.1.1 Transition Removal

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

6: −2 + 10⋅a_149_0 + 10⋅a_281_0
7: −4 + 10⋅a_149_0 + 10⋅a_281_0
8: −5 + 10⋅a_149_0 + 10⋅a_281_0
9: 4 + 10⋅a_342_0 + 10⋅a_343_0
10: 3 + 10⋅a_342_0 + 10⋅a_343_0
11: 2 + 10⋅a_342_0 + 10⋅a_343_0
12: 1 + 10⋅a_342_0 + 10⋅a_343_0
13: 10⋅a_149_0 + 10⋅a_281_0
6_var_snapshot: −3 + 10⋅a_149_0 + 10⋅a_281_0
6*: −1 + 10⋅a_149_0 + 10⋅a_281_0

9.1.2 Transition Removal

We remove transitions 84, 7, 8, 9, 10, 11, 12, 13 using the following ranking functions, which are bounded by −3.

6: −2
7: 6
8: 5
9: 4
10: 3
11: 2
12: 1
13: 0
6_var_snapshot: −3
6*: −1

9.1.3 Transition Removal

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

6: 0
7: 0
8: 0
9: 0
10: 0
11: 0
12: 0
13: 0
6_var_snapshot: −1
6*: 0

9.1.4 Splitting Cut-Point Transitions

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

9.1.4.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 81.

9.1.4.1.1 Splitting Cut-Point Transitions

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

9.2 SCC Subproblem 2/3

Here we consider the SCC { 31, 34, 35, 36, 37, 38, 39, 31_var_snapshot, 31* }.

9.2.1 Transition Removal

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

31: −2 + 9⋅a_149_0
34: −4 + 9⋅a_149_0
35: −5 + 9⋅a_149_0
36: 3 + 9⋅a_188_0
37: 2 + 9⋅a_188_0
38: 1 + 9⋅a_188_0
39: 9⋅a_149_0
31_var_snapshot: −3 + 9⋅a_149_0
31*: −1 + 9⋅a_149_0

9.2.2 Transition Removal

We remove transitions 89, 91, 36, 37, 38, 39, 40, 41 using the following ranking functions, which are bounded by −3.

31: −2
34: 5
35: 4
36: 3
37: 2
38: 1
39: 0
31_var_snapshot: −3
31*: −1

9.2.3 Splitting Cut-Point Transitions

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

9.2.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 88.

9.2.3.1.1 Splitting Cut-Point Transitions

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

9.3 SCC Subproblem 3/3

Here we consider the SCC { 0, 2, 0_var_snapshot, 0* }.

9.3.1 Transition Removal

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

0: −1 − 4⋅i_30_0 + 4⋅length_28_0
2: 1 − 4⋅i_30_0 + 4⋅length_28_0
0_var_snapshot: −2 − 4⋅i_30_0 + 4⋅length_28_0
0*: −4⋅i_30_0 + 4⋅length_28_0

9.3.2 Transition Removal

We remove transitions 75, 77, 2 using the following ranking functions, which are bounded by −3.

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

9.3.3 Splitting Cut-Point Transitions

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

9.3.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 74.

9.3.3.1.1 Splitting Cut-Point Transitions

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

Tool configuration

T2Cert