LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Invariant Updates

The following invariants are asserted.

0: TRUE
1: head_30_post ≤ 0 ∧ − head_30_post ≤ 0 ∧ i_28_post ≤ 0 ∧ − i_28_post ≤ 0 ∧ head_30_0 ≤ 0 ∧ − head_30_0 ≤ 0 ∧ i_28_0 ≤ 0 ∧ − i_28_0 ≤ 0
2: 2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ − a_144_0 ≤ 0 ∧ x_14_0 ≤ 0 ∧ − x_14_0 ≤ 0 ∧ y_20_post ≤ 0 ∧ − y_20_post ≤ 0 ∧ ct_18_0 ≤ 0 ∧ − ct_18_0 ≤ 0 ∧ y_20_0 ≤ 0 ∧ − y_20_0 ≤ 0
3: x_14_0 ≤ 0 ∧ − x_14_0 ≤ 0
4: − a_144_0 ≤ 0 ∧ y_20_post ≤ 0 ∧ − y_20_post ≤ 0 ∧ y_20_0 ≤ 0 ∧ − y_20_0 ≤ 0 ∧ − a_234_0 ≤ 0
5: − a_144_0 ≤ 0 ∧ y_20_post ≤ 0 ∧ − y_20_post ≤ 0 ∧ y_20_0 ≤ 0 ∧ − y_20_0 ≤ 0 ∧ − a_234_0 ≤ 0
6: − a_144_0 ≤ 0 ∧ x_14_0 ≤ 0 ∧ − x_14_0 ≤ 0 ∧ y_20_post ≤ 0 ∧ − y_20_post ≤ 0 ∧ ct_18_0 ≤ 0 ∧ − ct_18_0 ≤ 0 ∧ y_20_0 ≤ 0 ∧ − y_20_0 ≤ 0 ∧ − a_234_0 ≤ 0
7: − a_144_0 ≤ 0 ∧ x_14_0 ≤ 0 ∧ − x_14_0 ≤ 0 ∧ y_20_post ≤ 0 ∧ − y_20_post ≤ 0 ∧ ct_18_0 ≤ 0 ∧ − ct_18_0 ≤ 0 ∧ y_20_0 ≤ 0 ∧ − y_20_0 ≤ 0 ∧ − a_234_0 ≤ 0
8: − a_144_0 ≤ 0 ∧ x_14_0 ≤ 0 ∧ − x_14_0 ≤ 0 ∧ y_20_post ≤ 0 ∧ − y_20_post ≤ 0 ∧ ct_18_0 ≤ 0 ∧ − ct_18_0 ≤ 0 ∧ y_20_0 ≤ 0 ∧ − y_20_0 ≤ 0 ∧ − a_234_0 ≤ 0
9: − a_144_0 ≤ 0 ∧ x_14_0 ≤ 0 ∧ − x_14_0 ≤ 0 ∧ y_20_post ≤ 0 ∧ − y_20_post ≤ 0 ∧ ct_18_0 ≤ 0 ∧ − ct_18_0 ≤ 0 ∧ y_20_0 ≤ 0 ∧ − y_20_0 ≤ 0 ∧ − a_234_0 ≤ 0
10: 2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ − a_144_0 ≤ 0 ∧ x_14_0 ≤ 0 ∧ − x_14_0 ≤ 0 ∧ y_20_post ≤ 0 ∧ − y_20_post ≤ 0 ∧ ct_18_0 ≤ 0 ∧ − ct_18_0 ≤ 0 ∧ y_20_0 ≤ 0 ∧ − y_20_0 ≤ 0
20: 2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ − len_129_0 ≤ 0 ∧ − a_144_0 ≤ 0 ∧ x_14_0 ≤ 0 ∧ − x_14_0 ≤ 0 ∧ ct_18_post ≤ 0 ∧ − ct_18_post ≤ 0 ∧ y_20_post ≤ 0 ∧ − y_20_post ≤ 0 ∧ ct_18_0 ≤ 0 ∧ − ct_18_0 ≤ 0 ∧ y_20_0 ≤ 0 ∧ − y_20_0 ≤ 0
21: − len_129_0 ≤ 0 ∧ − a_144_0 ≤ 0 ∧ y_20_post ≤ 0 ∧ − y_20_post ≤ 0 ∧ y_20_0 ≤ 0 ∧ − y_20_0 ≤ 0
22: − len_129_0 ≤ 0 ∧ − a_144_0 ≤ 0 ∧ y_20_post ≤ 0 ∧ − y_20_post ≤ 0 ∧ y_20_0 ≤ 0 ∧ − y_20_0 ≤ 0
23: − len_129_0 ≤ 0 ∧ − a_144_0 ≤ 0 ∧ x_14_0 ≤ 0 ∧ − x_14_0 ≤ 0 ∧ y_20_post ≤ 0 ∧ − y_20_post ≤ 0 ∧ ct_18_0 ≤ 0 ∧ − ct_18_0 ≤ 0 ∧ y_20_0 ≤ 0 ∧ − y_20_0 ≤ 0
24: − len_129_0 ≤ 0 ∧ − a_144_0 ≤ 0 ∧ x_14_0 ≤ 0 ∧ − x_14_0 ≤ 0 ∧ y_20_post ≤ 0 ∧ − y_20_post ≤ 0 ∧ ct_18_0 ≤ 0 ∧ − ct_18_0 ≤ 0 ∧ y_20_0 ≤ 0 ∧ − y_20_0 ≤ 0
25: − len_129_0 ≤ 0 ∧ − a_144_0 ≤ 0 ∧ x_14_0 ≤ 0 ∧ − x_14_0 ≤ 0 ∧ y_20_post ≤ 0 ∧ − y_20_post ≤ 0 ∧ ct_18_0 ≤ 0 ∧ − ct_18_0 ≤ 0 ∧ y_20_0 ≤ 0 ∧ − y_20_0 ≤ 0
26: − len_129_0 ≤ 0 ∧ − a_144_0 ≤ 0 ∧ x_14_0 ≤ 0 ∧ − x_14_0 ≤ 0 ∧ y_20_post ≤ 0 ∧ − y_20_post ≤ 0 ∧ ct_18_0 ≤ 0 ∧ − ct_18_0 ≤ 0 ∧ y_20_0 ≤ 0 ∧ − y_20_0 ≤ 0
27: −1 + i_28_post ≤ 0 ∧ 1 − i_28_post ≤ 0 ∧ −1 + i_28_0 ≤ 0 ∧ 1 − i_28_0 ≤ 0 ∧ 1 − length_27_0 ≤ 0
28: −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0
29: −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0
30: −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ x_14_0 ≤ 0 ∧ − x_14_0 ≤ 0
31: −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ x_14_0 ≤ 0 ∧ − x_14_0 ≤ 0
32: −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0 ∧ −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ x_14_0 ≤ 0 ∧ − x_14_0 ≤ 0 ∧ ct_18_post ≤ 0 ∧ − ct_18_post ≤ 0 ∧ y_20_post ≤ 0 ∧ − y_20_post ≤ 0 ∧ ct_18_0 ≤ 0 ∧ − ct_18_0 ≤ 0 ∧ y_20_0 ≤ 0 ∧ − y_20_0 ≤ 0
33: −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0 ∧ −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ x_14_0 ≤ 0 ∧ − x_14_0 ≤ 0 ∧ ct_18_post ≤ 0 ∧ − ct_18_post ≤ 0 ∧ y_20_post ≤ 0 ∧ − y_20_post ≤ 0 ∧ ct_18_0 ≤ 0 ∧ − ct_18_0 ≤ 0 ∧ y_20_0 ≤ 0 ∧ − y_20_0 ≤ 0
34: −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ y_20_post ≤ 0 ∧ − y_20_post ≤ 0 ∧ y_20_0 ≤ 0 ∧ − y_20_0 ≤ 0
35: −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ y_20_post ≤ 0 ∧ − y_20_post ≤ 0 ∧ y_20_0 ≤ 0 ∧ − y_20_0 ≤ 0
36: −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ x_14_0 ≤ 0 ∧ − x_14_0 ≤ 0 ∧ y_20_post ≤ 0 ∧ − y_20_post ≤ 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
37: −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ x_14_0 ≤ 0 ∧ − x_14_0 ≤ 0 ∧ y_20_post ≤ 0 ∧ − y_20_post ≤ 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
38: −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ x_14_0 ≤ 0 ∧ − x_14_0 ≤ 0 ∧ y_20_post ≤ 0 ∧ − y_20_post ≤ 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
39: −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ x_14_0 ≤ 0 ∧ − x_14_0 ≤ 0
40: 2 − length_27_0 ≤ 0
41: 2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0
42: − len_129_0 ≤ 0 ∧ − a_144_0 ≤ 0 ∧ x_14_0 ≤ 0 ∧ − x_14_0 ≤ 0 ∧ ct_18_post ≤ 0 ∧ − ct_18_post ≤ 0 ∧ y_20_post ≤ 0 ∧ − y_20_post ≤ 0 ∧ ct_18_0 ≤ 0 ∧ − ct_18_0 ≤ 0 ∧ y_20_0 ≤ 0 ∧ − y_20_0 ≤ 0
43: − len_129_0 ≤ 0 ∧ − a_144_0 ≤ 0 ∧ x_14_0 ≤ 0 ∧ − x_14_0 ≤ 0 ∧ ct_18_post ≤ 0 ∧ − ct_18_post ≤ 0 ∧ y_20_post ≤ 0 ∧ − y_20_post ≤ 0 ∧ ct_18_0 ≤ 0 ∧ − ct_18_0 ≤ 0 ∧ y_20_0 ≤ 0 ∧ − y_20_0 ≤ 0
44: − len_129_0 ≤ 0 ∧ − a_144_0 ≤ 0
45: − len_129_0 ≤ 0 ∧ − a_144_0 ≤ 0
46: − len_129_0 ≤ 0 ∧ − a_144_0 ≤ 0 ∧ 1 − len_180_post ≤ 0 ∧ 1 − len_180_0 ≤ 0
47: − len_129_0 ≤ 0 ∧ − a_144_0 ≤ 0 ∧ 1 − len_180_post ≤ 0 ∧ 1 − len_180_0 ≤ 0
48: − len_129_0 ≤ 0 ∧ − a_144_0 ≤ 0 ∧ 1 − len_180_post ≤ 0 ∧ 1 − len_180_0 ≤ 0
49: 2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ 1 − len_180_post ≤ 0 ∧ 1 − len_180_0 ≤ 0
62: len_129_0 ≤ 0 ∧ − len_129_0 ≤ 0
63: len_129_0 ≤ 0 ∧ − len_129_0 ≤ 0
64: 2 − length_27_0 ≤ 0
65: TRUE

The invariants are proved as follows.

IMPACT Invariant Proof

2 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
2 72 2: − 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_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_172_post + x_172_post ≤ 0 ∧ x_172_post − x_172_post ≤ 0 ∧ − x_172_0 + x_172_0 ≤ 0 ∧ x_172_0 − x_172_0 ≤ 0 ∧ − x_14_post + x_14_post ≤ 0 ∧ x_14_post − x_14_post ≤ 0 ∧ − x_14_0 + x_14_0 ≤ 0 ∧ x_14_0 − x_14_0 ≤ 0 ∧ − x_126_post + x_126_post ≤ 0 ∧ x_126_post − x_126_post ≤ 0 ∧ − x_126_0 + x_126_0 ≤ 0 ∧ x_126_0 − x_126_0 ≤ 0 ∧ − tmp_32_post + tmp_32_post ≤ 0 ∧ tmp_32_post − tmp_32_post ≤ 0 ∧ − tmp_32_0 + tmp_32_0 ≤ 0 ∧ tmp_32_0 − tmp_32_0 ≤ 0 ∧ − temp_33_post + temp_33_post ≤ 0 ∧ temp_33_post − temp_33_post ≤ 0 ∧ − temp_33_0 + temp_33_0 ≤ 0 ∧ temp_33_0 − temp_33_0 ≤ 0 ∧ − temp0_29_post + temp0_29_post ≤ 0 ∧ temp0_29_post − temp0_29_post ≤ 0 ∧ − temp0_29_1 + temp0_29_1 ≤ 0 ∧ temp0_29_1 − temp0_29_1 ≤ 0 ∧ − temp0_29_0 + temp0_29_0 ≤ 0 ∧ temp0_29_0 − temp0_29_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_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_31_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_post ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_post − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_post ≤ 0 ∧ − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_0 ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_0 − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_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_86_post + rcd_86_post ≤ 0 ∧ rcd_86_post − rcd_86_post ≤ 0 ∧ − rcd_86_0 + rcd_86_0 ≤ 0 ∧ rcd_86_0 − rcd_86_0 ≤ 0 ∧ − rcd_56_post + rcd_56_post ≤ 0 ∧ rcd_56_post − rcd_56_post ≤ 0 ∧ − rcd_56_0 + rcd_56_0 ≤ 0 ∧ rcd_56_0 − rcd_56_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 ∧ − r_160_post + r_160_post ≤ 0 ∧ r_160_post − r_160_post ≤ 0 ∧ − r_160_0 + r_160_0 ≤ 0 ∧ r_160_0 − r_160_0 ≤ 0 ∧ − r_121_post + r_121_post ≤ 0 ∧ r_121_post − r_121_post ≤ 0 ∧ − r_121_0 + r_121_0 ≤ 0 ∧ r_121_0 − r_121_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_27_post + length_27_post ≤ 0 ∧ length_27_post − length_27_post ≤ 0 ∧ − length_27_0 + length_27_0 ≤ 0 ∧ length_27_0 − length_27_0 ≤ 0 ∧ − len_180_post + len_180_post ≤ 0 ∧ len_180_post − len_180_post ≤ 0 ∧ − len_180_0 + len_180_0 ≤ 0 ∧ len_180_0 − len_180_0 ≤ 0 ∧ − len_129_post + len_129_post ≤ 0 ∧ len_129_post − len_129_post ≤ 0 ∧ − len_129_0 + len_129_0 ≤ 0 ∧ len_129_0 − len_129_0 ≤ 0 ∧ − i_92_post + i_92_post ≤ 0 ∧ i_92_post − i_92_post ≤ 0 ∧ − i_92_0 + i_92_0 ≤ 0 ∧ i_92_0 − i_92_0 ≤ 0 ∧ − i_28_post + i_28_post ≤ 0 ∧ i_28_post − i_28_post ≤ 0 ∧ − i_28_0 + i_28_0 ≤ 0 ∧ i_28_0 − i_28_0 ≤ 0 ∧ − i_164_post + i_164_post ≤ 0 ∧ i_164_post − i_164_post ≤ 0 ∧ − i_164_0 + i_164_0 ≤ 0 ∧ i_164_0 − i_164_0 ≤ 0 ∧ − i_105_post + i_105_post ≤ 0 ∧ i_105_post − i_105_post ≤ 0 ∧ − i_105_0 + i_105_0 ≤ 0 ∧ i_105_0 − i_105_0 ≤ 0 ∧ − head_30_post + head_30_post ≤ 0 ∧ head_30_post − head_30_post ≤ 0 ∧ − head_30_0 + head_30_0 ≤ 0 ∧ head_30_0 − head_30_0 ≤ 0 ∧ − head_15_post + head_15_post ≤ 0 ∧ head_15_post − head_15_post ≤ 0 ∧ − head_15_1 + head_15_1 ≤ 0 ∧ head_15_1 − head_15_1 ≤ 0 ∧ − head_15_0 + head_15_0 ≤ 0 ∧ head_15_0 − head_15_0 ≤ 0 ∧ − f_167_post + f_167_post ≤ 0 ∧ f_167_post − f_167_post ≤ 0 ∧ − f_167_0 + f_167_0 ≤ 0 ∧ f_167_0 − f_167_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_257_post + a_257_post ≤ 0 ∧ a_257_post − a_257_post ≤ 0 ∧ − a_257_0 + a_257_0 ≤ 0 ∧ a_257_0 − a_257_0 ≤ 0 ∧ − a_234_post + a_234_post ≤ 0 ∧ a_234_post − a_234_post ≤ 0 ∧ − a_234_0 + a_234_0 ≤ 0 ∧ a_234_0 − a_234_0 ≤ 0 ∧ − a_212_post + a_212_post ≤ 0 ∧ a_212_post − a_212_post ≤ 0 ∧ − a_212_0 + a_212_0 ≤ 0 ∧ a_212_0 − a_212_0 ≤ 0 ∧ − a_181_post + a_181_post ≤ 0 ∧ a_181_post − a_181_post ≤ 0 ∧ − a_181_0 + a_181_0 ≤ 0 ∧ a_181_0 − a_181_0 ≤ 0 ∧ − a_144_post + a_144_post ≤ 0 ∧ a_144_post − a_144_post ≤ 0 ∧ − a_144_0 + a_144_0 ≤ 0 ∧ a_144_0 − a_144_0 ≤ 0 ∧ − a_113_post + a_113_post ≤ 0 ∧ a_113_post − a_113_post ≤ 0 ∧ − a_113_0 + a_113_0 ≤ 0 ∧ a_113_0 − a_113_0 ≤ 0
40 79 40: − 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_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_172_post + x_172_post ≤ 0 ∧ x_172_post − x_172_post ≤ 0 ∧ − x_172_0 + x_172_0 ≤ 0 ∧ x_172_0 − x_172_0 ≤ 0 ∧ − x_14_post + x_14_post ≤ 0 ∧ x_14_post − x_14_post ≤ 0 ∧ − x_14_0 + x_14_0 ≤ 0 ∧ x_14_0 − x_14_0 ≤ 0 ∧ − x_126_post + x_126_post ≤ 0 ∧ x_126_post − x_126_post ≤ 0 ∧ − x_126_0 + x_126_0 ≤ 0 ∧ x_126_0 − x_126_0 ≤ 0 ∧ − tmp_32_post + tmp_32_post ≤ 0 ∧ tmp_32_post − tmp_32_post ≤ 0 ∧ − tmp_32_0 + tmp_32_0 ≤ 0 ∧ tmp_32_0 − tmp_32_0 ≤ 0 ∧ − temp_33_post + temp_33_post ≤ 0 ∧ temp_33_post − temp_33_post ≤ 0 ∧ − temp_33_0 + temp_33_0 ≤ 0 ∧ temp_33_0 − temp_33_0 ≤ 0 ∧ − temp0_29_post + temp0_29_post ≤ 0 ∧ temp0_29_post − temp0_29_post ≤ 0 ∧ − temp0_29_1 + temp0_29_1 ≤ 0 ∧ temp0_29_1 − temp0_29_1 ≤ 0 ∧ − temp0_29_0 + temp0_29_0 ≤ 0 ∧ temp0_29_0 − temp0_29_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_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_31_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_post ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_post − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_post ≤ 0 ∧ − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_0 ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_0 − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_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_86_post + rcd_86_post ≤ 0 ∧ rcd_86_post − rcd_86_post ≤ 0 ∧ − rcd_86_0 + rcd_86_0 ≤ 0 ∧ rcd_86_0 − rcd_86_0 ≤ 0 ∧ − rcd_56_post + rcd_56_post ≤ 0 ∧ rcd_56_post − rcd_56_post ≤ 0 ∧ − rcd_56_0 + rcd_56_0 ≤ 0 ∧ rcd_56_0 − rcd_56_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 ∧ − r_160_post + r_160_post ≤ 0 ∧ r_160_post − r_160_post ≤ 0 ∧ − r_160_0 + r_160_0 ≤ 0 ∧ r_160_0 − r_160_0 ≤ 0 ∧ − r_121_post + r_121_post ≤ 0 ∧ r_121_post − r_121_post ≤ 0 ∧ − r_121_0 + r_121_0 ≤ 0 ∧ r_121_0 − r_121_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_27_post + length_27_post ≤ 0 ∧ length_27_post − length_27_post ≤ 0 ∧ − length_27_0 + length_27_0 ≤ 0 ∧ length_27_0 − length_27_0 ≤ 0 ∧ − len_180_post + len_180_post ≤ 0 ∧ len_180_post − len_180_post ≤ 0 ∧ − len_180_0 + len_180_0 ≤ 0 ∧ len_180_0 − len_180_0 ≤ 0 ∧ − len_129_post + len_129_post ≤ 0 ∧ len_129_post − len_129_post ≤ 0 ∧ − len_129_0 + len_129_0 ≤ 0 ∧ len_129_0 − len_129_0 ≤ 0 ∧ − i_92_post + i_92_post ≤ 0 ∧ i_92_post − i_92_post ≤ 0 ∧ − i_92_0 + i_92_0 ≤ 0 ∧ i_92_0 − i_92_0 ≤ 0 ∧ − i_28_post + i_28_post ≤ 0 ∧ i_28_post − i_28_post ≤ 0 ∧ − i_28_0 + i_28_0 ≤ 0 ∧ i_28_0 − i_28_0 ≤ 0 ∧ − i_164_post + i_164_post ≤ 0 ∧ i_164_post − i_164_post ≤ 0 ∧ − i_164_0 + i_164_0 ≤ 0 ∧ i_164_0 − i_164_0 ≤ 0 ∧ − i_105_post + i_105_post ≤ 0 ∧ i_105_post − i_105_post ≤ 0 ∧ − i_105_0 + i_105_0 ≤ 0 ∧ i_105_0 − i_105_0 ≤ 0 ∧ − head_30_post + head_30_post ≤ 0 ∧ head_30_post − head_30_post ≤ 0 ∧ − head_30_0 + head_30_0 ≤ 0 ∧ head_30_0 − head_30_0 ≤ 0 ∧ − head_15_post + head_15_post ≤ 0 ∧ head_15_post − head_15_post ≤ 0 ∧ − head_15_1 + head_15_1 ≤ 0 ∧ head_15_1 − head_15_1 ≤ 0 ∧ − head_15_0 + head_15_0 ≤ 0 ∧ head_15_0 − head_15_0 ≤ 0 ∧ − f_167_post + f_167_post ≤ 0 ∧ f_167_post − f_167_post ≤ 0 ∧ − f_167_0 + f_167_0 ≤ 0 ∧ f_167_0 − f_167_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_257_post + a_257_post ≤ 0 ∧ a_257_post − a_257_post ≤ 0 ∧ − a_257_0 + a_257_0 ≤ 0 ∧ a_257_0 − a_257_0 ≤ 0 ∧ − a_234_post + a_234_post ≤ 0 ∧ a_234_post − a_234_post ≤ 0 ∧ − a_234_0 + a_234_0 ≤ 0 ∧ a_234_0 − a_234_0 ≤ 0 ∧ − a_212_post + a_212_post ≤ 0 ∧ a_212_post − a_212_post ≤ 0 ∧ − a_212_0 + a_212_0 ≤ 0 ∧ a_212_0 − a_212_0 ≤ 0 ∧ − a_181_post + a_181_post ≤ 0 ∧ a_181_post − a_181_post ≤ 0 ∧ − a_181_0 + a_181_0 ≤ 0 ∧ a_181_0 − a_181_0 ≤ 0 ∧ − a_144_post + a_144_post ≤ 0 ∧ a_144_post − a_144_post ≤ 0 ∧ − a_144_0 + a_144_0 ≤ 0 ∧ a_144_0 − a_144_0 ≤ 0 ∧ − a_113_post + a_113_post ≤ 0 ∧ a_113_post − a_113_post ≤ 0 ∧ − a_113_0 + a_113_0 ≤ 0 ∧ a_113_0 − a_113_0 ≤ 0
41 86 41: − 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_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_172_post + x_172_post ≤ 0 ∧ x_172_post − x_172_post ≤ 0 ∧ − x_172_0 + x_172_0 ≤ 0 ∧ x_172_0 − x_172_0 ≤ 0 ∧ − x_14_post + x_14_post ≤ 0 ∧ x_14_post − x_14_post ≤ 0 ∧ − x_14_0 + x_14_0 ≤ 0 ∧ x_14_0 − x_14_0 ≤ 0 ∧ − x_126_post + x_126_post ≤ 0 ∧ x_126_post − x_126_post ≤ 0 ∧ − x_126_0 + x_126_0 ≤ 0 ∧ x_126_0 − x_126_0 ≤ 0 ∧ − tmp_32_post + tmp_32_post ≤ 0 ∧ tmp_32_post − tmp_32_post ≤ 0 ∧ − tmp_32_0 + tmp_32_0 ≤ 0 ∧ tmp_32_0 − tmp_32_0 ≤ 0 ∧ − temp_33_post + temp_33_post ≤ 0 ∧ temp_33_post − temp_33_post ≤ 0 ∧ − temp_33_0 + temp_33_0 ≤ 0 ∧ temp_33_0 − temp_33_0 ≤ 0 ∧ − temp0_29_post + temp0_29_post ≤ 0 ∧ temp0_29_post − temp0_29_post ≤ 0 ∧ − temp0_29_1 + temp0_29_1 ≤ 0 ∧ temp0_29_1 − temp0_29_1 ≤ 0 ∧ − temp0_29_0 + temp0_29_0 ≤ 0 ∧ temp0_29_0 − temp0_29_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_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_31_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_post ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_post − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_post ≤ 0 ∧ − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_0 ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_0 − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_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_86_post + rcd_86_post ≤ 0 ∧ rcd_86_post − rcd_86_post ≤ 0 ∧ − rcd_86_0 + rcd_86_0 ≤ 0 ∧ rcd_86_0 − rcd_86_0 ≤ 0 ∧ − rcd_56_post + rcd_56_post ≤ 0 ∧ rcd_56_post − rcd_56_post ≤ 0 ∧ − rcd_56_0 + rcd_56_0 ≤ 0 ∧ rcd_56_0 − rcd_56_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 ∧ − r_160_post + r_160_post ≤ 0 ∧ r_160_post − r_160_post ≤ 0 ∧ − r_160_0 + r_160_0 ≤ 0 ∧ r_160_0 − r_160_0 ≤ 0 ∧ − r_121_post + r_121_post ≤ 0 ∧ r_121_post − r_121_post ≤ 0 ∧ − r_121_0 + r_121_0 ≤ 0 ∧ r_121_0 − r_121_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_27_post + length_27_post ≤ 0 ∧ length_27_post − length_27_post ≤ 0 ∧ − length_27_0 + length_27_0 ≤ 0 ∧ length_27_0 − length_27_0 ≤ 0 ∧ − len_180_post + len_180_post ≤ 0 ∧ len_180_post − len_180_post ≤ 0 ∧ − len_180_0 + len_180_0 ≤ 0 ∧ len_180_0 − len_180_0 ≤ 0 ∧ − len_129_post + len_129_post ≤ 0 ∧ len_129_post − len_129_post ≤ 0 ∧ − len_129_0 + len_129_0 ≤ 0 ∧ len_129_0 − len_129_0 ≤ 0 ∧ − i_92_post + i_92_post ≤ 0 ∧ i_92_post − i_92_post ≤ 0 ∧ − i_92_0 + i_92_0 ≤ 0 ∧ i_92_0 − i_92_0 ≤ 0 ∧ − i_28_post + i_28_post ≤ 0 ∧ i_28_post − i_28_post ≤ 0 ∧ − i_28_0 + i_28_0 ≤ 0 ∧ i_28_0 − i_28_0 ≤ 0 ∧ − i_164_post + i_164_post ≤ 0 ∧ i_164_post − i_164_post ≤ 0 ∧ − i_164_0 + i_164_0 ≤ 0 ∧ i_164_0 − i_164_0 ≤ 0 ∧ − i_105_post + i_105_post ≤ 0 ∧ i_105_post − i_105_post ≤ 0 ∧ − i_105_0 + i_105_0 ≤ 0 ∧ i_105_0 − i_105_0 ≤ 0 ∧ − head_30_post + head_30_post ≤ 0 ∧ head_30_post − head_30_post ≤ 0 ∧ − head_30_0 + head_30_0 ≤ 0 ∧ head_30_0 − head_30_0 ≤ 0 ∧ − head_15_post + head_15_post ≤ 0 ∧ head_15_post − head_15_post ≤ 0 ∧ − head_15_1 + head_15_1 ≤ 0 ∧ head_15_1 − head_15_1 ≤ 0 ∧ − head_15_0 + head_15_0 ≤ 0 ∧ head_15_0 − head_15_0 ≤ 0 ∧ − f_167_post + f_167_post ≤ 0 ∧ f_167_post − f_167_post ≤ 0 ∧ − f_167_0 + f_167_0 ≤ 0 ∧ f_167_0 − f_167_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_257_post + a_257_post ≤ 0 ∧ a_257_post − a_257_post ≤ 0 ∧ − a_257_0 + a_257_0 ≤ 0 ∧ a_257_0 − a_257_0 ≤ 0 ∧ − a_234_post + a_234_post ≤ 0 ∧ a_234_post − a_234_post ≤ 0 ∧ − a_234_0 + a_234_0 ≤ 0 ∧ a_234_0 − a_234_0 ≤ 0 ∧ − a_212_post + a_212_post ≤ 0 ∧ a_212_post − a_212_post ≤ 0 ∧ − a_212_0 + a_212_0 ≤ 0 ∧ a_212_0 − a_212_0 ≤ 0 ∧ − a_181_post + a_181_post ≤ 0 ∧ a_181_post − a_181_post ≤ 0 ∧ − a_181_0 + a_181_0 ≤ 0 ∧ a_181_0 − a_181_0 ≤ 0 ∧ − a_144_post + a_144_post ≤ 0 ∧ a_144_post − a_144_post ≤ 0 ∧ − a_144_0 + a_144_0 ≤ 0 ∧ a_144_0 − a_144_0 ≤ 0 ∧ − a_113_post + a_113_post ≤ 0 ∧ a_113_post − a_113_post ≤ 0 ∧ − a_113_0 + a_113_0 ≤ 0 ∧ a_113_0 − a_113_0 ≤ 0
and for every transition t, a duplicate t is considered.

3 Transition Removal

We remove transitions 0, 1, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 64, 65, 66, 69, 70, 71 using the following ranking functions, which are bounded by −71.

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

4 Location Addition

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

2* 75 2: − 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_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_172_post + x_172_post ≤ 0 ∧ x_172_post − x_172_post ≤ 0 ∧ − x_172_0 + x_172_0 ≤ 0 ∧ x_172_0 − x_172_0 ≤ 0 ∧ − x_14_post + x_14_post ≤ 0 ∧ x_14_post − x_14_post ≤ 0 ∧ − x_14_0 + x_14_0 ≤ 0 ∧ x_14_0 − x_14_0 ≤ 0 ∧ − x_126_post + x_126_post ≤ 0 ∧ x_126_post − x_126_post ≤ 0 ∧ − x_126_0 + x_126_0 ≤ 0 ∧ x_126_0 − x_126_0 ≤ 0 ∧ − tmp_32_post + tmp_32_post ≤ 0 ∧ tmp_32_post − tmp_32_post ≤ 0 ∧ − tmp_32_0 + tmp_32_0 ≤ 0 ∧ tmp_32_0 − tmp_32_0 ≤ 0 ∧ − temp_33_post + temp_33_post ≤ 0 ∧ temp_33_post − temp_33_post ≤ 0 ∧ − temp_33_0 + temp_33_0 ≤ 0 ∧ temp_33_0 − temp_33_0 ≤ 0 ∧ − temp0_29_post + temp0_29_post ≤ 0 ∧ temp0_29_post − temp0_29_post ≤ 0 ∧ − temp0_29_1 + temp0_29_1 ≤ 0 ∧ temp0_29_1 − temp0_29_1 ≤ 0 ∧ − temp0_29_0 + temp0_29_0 ≤ 0 ∧ temp0_29_0 − temp0_29_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_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_31_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_post ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_post − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_post ≤ 0 ∧ − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_0 ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_0 − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_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_86_post + rcd_86_post ≤ 0 ∧ rcd_86_post − rcd_86_post ≤ 0 ∧ − rcd_86_0 + rcd_86_0 ≤ 0 ∧ rcd_86_0 − rcd_86_0 ≤ 0 ∧ − rcd_56_post + rcd_56_post ≤ 0 ∧ rcd_56_post − rcd_56_post ≤ 0 ∧ − rcd_56_0 + rcd_56_0 ≤ 0 ∧ rcd_56_0 − rcd_56_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 ∧ − r_160_post + r_160_post ≤ 0 ∧ r_160_post − r_160_post ≤ 0 ∧ − r_160_0 + r_160_0 ≤ 0 ∧ r_160_0 − r_160_0 ≤ 0 ∧ − r_121_post + r_121_post ≤ 0 ∧ r_121_post − r_121_post ≤ 0 ∧ − r_121_0 + r_121_0 ≤ 0 ∧ r_121_0 − r_121_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_27_post + length_27_post ≤ 0 ∧ length_27_post − length_27_post ≤ 0 ∧ − length_27_0 + length_27_0 ≤ 0 ∧ length_27_0 − length_27_0 ≤ 0 ∧ − len_180_post + len_180_post ≤ 0 ∧ len_180_post − len_180_post ≤ 0 ∧ − len_180_0 + len_180_0 ≤ 0 ∧ len_180_0 − len_180_0 ≤ 0 ∧ − len_129_post + len_129_post ≤ 0 ∧ len_129_post − len_129_post ≤ 0 ∧ − len_129_0 + len_129_0 ≤ 0 ∧ len_129_0 − len_129_0 ≤ 0 ∧ − i_92_post + i_92_post ≤ 0 ∧ i_92_post − i_92_post ≤ 0 ∧ − i_92_0 + i_92_0 ≤ 0 ∧ i_92_0 − i_92_0 ≤ 0 ∧ − i_28_post + i_28_post ≤ 0 ∧ i_28_post − i_28_post ≤ 0 ∧ − i_28_0 + i_28_0 ≤ 0 ∧ i_28_0 − i_28_0 ≤ 0 ∧ − i_164_post + i_164_post ≤ 0 ∧ i_164_post − i_164_post ≤ 0 ∧ − i_164_0 + i_164_0 ≤ 0 ∧ i_164_0 − i_164_0 ≤ 0 ∧ − i_105_post + i_105_post ≤ 0 ∧ i_105_post − i_105_post ≤ 0 ∧ − i_105_0 + i_105_0 ≤ 0 ∧ i_105_0 − i_105_0 ≤ 0 ∧ − head_30_post + head_30_post ≤ 0 ∧ head_30_post − head_30_post ≤ 0 ∧ − head_30_0 + head_30_0 ≤ 0 ∧ head_30_0 − head_30_0 ≤ 0 ∧ − head_15_post + head_15_post ≤ 0 ∧ head_15_post − head_15_post ≤ 0 ∧ − head_15_1 + head_15_1 ≤ 0 ∧ head_15_1 − head_15_1 ≤ 0 ∧ − head_15_0 + head_15_0 ≤ 0 ∧ head_15_0 − head_15_0 ≤ 0 ∧ − f_167_post + f_167_post ≤ 0 ∧ f_167_post − f_167_post ≤ 0 ∧ − f_167_0 + f_167_0 ≤ 0 ∧ f_167_0 − f_167_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_257_post + a_257_post ≤ 0 ∧ a_257_post − a_257_post ≤ 0 ∧ − a_257_0 + a_257_0 ≤ 0 ∧ a_257_0 − a_257_0 ≤ 0 ∧ − a_234_post + a_234_post ≤ 0 ∧ a_234_post − a_234_post ≤ 0 ∧ − a_234_0 + a_234_0 ≤ 0 ∧ a_234_0 − a_234_0 ≤ 0 ∧ − a_212_post + a_212_post ≤ 0 ∧ a_212_post − a_212_post ≤ 0 ∧ − a_212_0 + a_212_0 ≤ 0 ∧ a_212_0 − a_212_0 ≤ 0 ∧ − a_181_post + a_181_post ≤ 0 ∧ a_181_post − a_181_post ≤ 0 ∧ − a_181_0 + a_181_0 ≤ 0 ∧ a_181_0 − a_181_0 ≤ 0 ∧ − a_144_post + a_144_post ≤ 0 ∧ a_144_post − a_144_post ≤ 0 ∧ − a_144_0 + a_144_0 ≤ 0 ∧ a_144_0 − a_144_0 ≤ 0 ∧ − a_113_post + a_113_post ≤ 0 ∧ a_113_post − a_113_post ≤ 0 ∧ − a_113_0 + a_113_0 ≤ 0 ∧ a_113_0 − a_113_0 ≤ 0

5 Location Addition

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

2 73 2_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_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_172_post + x_172_post ≤ 0 ∧ x_172_post − x_172_post ≤ 0 ∧ − x_172_0 + x_172_0 ≤ 0 ∧ x_172_0 − x_172_0 ≤ 0 ∧ − x_14_post + x_14_post ≤ 0 ∧ x_14_post − x_14_post ≤ 0 ∧ − x_14_0 + x_14_0 ≤ 0 ∧ x_14_0 − x_14_0 ≤ 0 ∧ − x_126_post + x_126_post ≤ 0 ∧ x_126_post − x_126_post ≤ 0 ∧ − x_126_0 + x_126_0 ≤ 0 ∧ x_126_0 − x_126_0 ≤ 0 ∧ − tmp_32_post + tmp_32_post ≤ 0 ∧ tmp_32_post − tmp_32_post ≤ 0 ∧ − tmp_32_0 + tmp_32_0 ≤ 0 ∧ tmp_32_0 − tmp_32_0 ≤ 0 ∧ − temp_33_post + temp_33_post ≤ 0 ∧ temp_33_post − temp_33_post ≤ 0 ∧ − temp_33_0 + temp_33_0 ≤ 0 ∧ temp_33_0 − temp_33_0 ≤ 0 ∧ − temp0_29_post + temp0_29_post ≤ 0 ∧ temp0_29_post − temp0_29_post ≤ 0 ∧ − temp0_29_1 + temp0_29_1 ≤ 0 ∧ temp0_29_1 − temp0_29_1 ≤ 0 ∧ − temp0_29_0 + temp0_29_0 ≤ 0 ∧ temp0_29_0 − temp0_29_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_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_31_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_post ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_post − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_post ≤ 0 ∧ − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_0 ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_0 − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_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_86_post + rcd_86_post ≤ 0 ∧ rcd_86_post − rcd_86_post ≤ 0 ∧ − rcd_86_0 + rcd_86_0 ≤ 0 ∧ rcd_86_0 − rcd_86_0 ≤ 0 ∧ − rcd_56_post + rcd_56_post ≤ 0 ∧ rcd_56_post − rcd_56_post ≤ 0 ∧ − rcd_56_0 + rcd_56_0 ≤ 0 ∧ rcd_56_0 − rcd_56_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 ∧ − r_160_post + r_160_post ≤ 0 ∧ r_160_post − r_160_post ≤ 0 ∧ − r_160_0 + r_160_0 ≤ 0 ∧ r_160_0 − r_160_0 ≤ 0 ∧ − r_121_post + r_121_post ≤ 0 ∧ r_121_post − r_121_post ≤ 0 ∧ − r_121_0 + r_121_0 ≤ 0 ∧ r_121_0 − r_121_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_27_post + length_27_post ≤ 0 ∧ length_27_post − length_27_post ≤ 0 ∧ − length_27_0 + length_27_0 ≤ 0 ∧ length_27_0 − length_27_0 ≤ 0 ∧ − len_180_post + len_180_post ≤ 0 ∧ len_180_post − len_180_post ≤ 0 ∧ − len_180_0 + len_180_0 ≤ 0 ∧ len_180_0 − len_180_0 ≤ 0 ∧ − len_129_post + len_129_post ≤ 0 ∧ len_129_post − len_129_post ≤ 0 ∧ − len_129_0 + len_129_0 ≤ 0 ∧ len_129_0 − len_129_0 ≤ 0 ∧ − i_92_post + i_92_post ≤ 0 ∧ i_92_post − i_92_post ≤ 0 ∧ − i_92_0 + i_92_0 ≤ 0 ∧ i_92_0 − i_92_0 ≤ 0 ∧ − i_28_post + i_28_post ≤ 0 ∧ i_28_post − i_28_post ≤ 0 ∧ − i_28_0 + i_28_0 ≤ 0 ∧ i_28_0 − i_28_0 ≤ 0 ∧ − i_164_post + i_164_post ≤ 0 ∧ i_164_post − i_164_post ≤ 0 ∧ − i_164_0 + i_164_0 ≤ 0 ∧ i_164_0 − i_164_0 ≤ 0 ∧ − i_105_post + i_105_post ≤ 0 ∧ i_105_post − i_105_post ≤ 0 ∧ − i_105_0 + i_105_0 ≤ 0 ∧ i_105_0 − i_105_0 ≤ 0 ∧ − head_30_post + head_30_post ≤ 0 ∧ head_30_post − head_30_post ≤ 0 ∧ − head_30_0 + head_30_0 ≤ 0 ∧ head_30_0 − head_30_0 ≤ 0 ∧ − head_15_post + head_15_post ≤ 0 ∧ head_15_post − head_15_post ≤ 0 ∧ − head_15_1 + head_15_1 ≤ 0 ∧ head_15_1 − head_15_1 ≤ 0 ∧ − head_15_0 + head_15_0 ≤ 0 ∧ head_15_0 − head_15_0 ≤ 0 ∧ − f_167_post + f_167_post ≤ 0 ∧ f_167_post − f_167_post ≤ 0 ∧ − f_167_0 + f_167_0 ≤ 0 ∧ f_167_0 − f_167_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_257_post + a_257_post ≤ 0 ∧ a_257_post − a_257_post ≤ 0 ∧ − a_257_0 + a_257_0 ≤ 0 ∧ a_257_0 − a_257_0 ≤ 0 ∧ − a_234_post + a_234_post ≤ 0 ∧ a_234_post − a_234_post ≤ 0 ∧ − a_234_0 + a_234_0 ≤ 0 ∧ a_234_0 − a_234_0 ≤ 0 ∧ − a_212_post + a_212_post ≤ 0 ∧ a_212_post − a_212_post ≤ 0 ∧ − a_212_0 + a_212_0 ≤ 0 ∧ a_212_0 − a_212_0 ≤ 0 ∧ − a_181_post + a_181_post ≤ 0 ∧ a_181_post − a_181_post ≤ 0 ∧ − a_181_0 + a_181_0 ≤ 0 ∧ a_181_0 − a_181_0 ≤ 0 ∧ − a_144_post + a_144_post ≤ 0 ∧ a_144_post − a_144_post ≤ 0 ∧ − a_144_0 + a_144_0 ≤ 0 ∧ a_144_0 − a_144_0 ≤ 0 ∧ − a_113_post + a_113_post ≤ 0 ∧ a_113_post − a_113_post ≤ 0 ∧ − a_113_0 + a_113_0 ≤ 0 ∧ a_113_0 − a_113_0 ≤ 0

6 Location Addition

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

40* 82 40: − 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_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_172_post + x_172_post ≤ 0 ∧ x_172_post − x_172_post ≤ 0 ∧ − x_172_0 + x_172_0 ≤ 0 ∧ x_172_0 − x_172_0 ≤ 0 ∧ − x_14_post + x_14_post ≤ 0 ∧ x_14_post − x_14_post ≤ 0 ∧ − x_14_0 + x_14_0 ≤ 0 ∧ x_14_0 − x_14_0 ≤ 0 ∧ − x_126_post + x_126_post ≤ 0 ∧ x_126_post − x_126_post ≤ 0 ∧ − x_126_0 + x_126_0 ≤ 0 ∧ x_126_0 − x_126_0 ≤ 0 ∧ − tmp_32_post + tmp_32_post ≤ 0 ∧ tmp_32_post − tmp_32_post ≤ 0 ∧ − tmp_32_0 + tmp_32_0 ≤ 0 ∧ tmp_32_0 − tmp_32_0 ≤ 0 ∧ − temp_33_post + temp_33_post ≤ 0 ∧ temp_33_post − temp_33_post ≤ 0 ∧ − temp_33_0 + temp_33_0 ≤ 0 ∧ temp_33_0 − temp_33_0 ≤ 0 ∧ − temp0_29_post + temp0_29_post ≤ 0 ∧ temp0_29_post − temp0_29_post ≤ 0 ∧ − temp0_29_1 + temp0_29_1 ≤ 0 ∧ temp0_29_1 − temp0_29_1 ≤ 0 ∧ − temp0_29_0 + temp0_29_0 ≤ 0 ∧ temp0_29_0 − temp0_29_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_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_31_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_post ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_post − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_post ≤ 0 ∧ − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_0 ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_0 − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_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_86_post + rcd_86_post ≤ 0 ∧ rcd_86_post − rcd_86_post ≤ 0 ∧ − rcd_86_0 + rcd_86_0 ≤ 0 ∧ rcd_86_0 − rcd_86_0 ≤ 0 ∧ − rcd_56_post + rcd_56_post ≤ 0 ∧ rcd_56_post − rcd_56_post ≤ 0 ∧ − rcd_56_0 + rcd_56_0 ≤ 0 ∧ rcd_56_0 − rcd_56_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 ∧ − r_160_post + r_160_post ≤ 0 ∧ r_160_post − r_160_post ≤ 0 ∧ − r_160_0 + r_160_0 ≤ 0 ∧ r_160_0 − r_160_0 ≤ 0 ∧ − r_121_post + r_121_post ≤ 0 ∧ r_121_post − r_121_post ≤ 0 ∧ − r_121_0 + r_121_0 ≤ 0 ∧ r_121_0 − r_121_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_27_post + length_27_post ≤ 0 ∧ length_27_post − length_27_post ≤ 0 ∧ − length_27_0 + length_27_0 ≤ 0 ∧ length_27_0 − length_27_0 ≤ 0 ∧ − len_180_post + len_180_post ≤ 0 ∧ len_180_post − len_180_post ≤ 0 ∧ − len_180_0 + len_180_0 ≤ 0 ∧ len_180_0 − len_180_0 ≤ 0 ∧ − len_129_post + len_129_post ≤ 0 ∧ len_129_post − len_129_post ≤ 0 ∧ − len_129_0 + len_129_0 ≤ 0 ∧ len_129_0 − len_129_0 ≤ 0 ∧ − i_92_post + i_92_post ≤ 0 ∧ i_92_post − i_92_post ≤ 0 ∧ − i_92_0 + i_92_0 ≤ 0 ∧ i_92_0 − i_92_0 ≤ 0 ∧ − i_28_post + i_28_post ≤ 0 ∧ i_28_post − i_28_post ≤ 0 ∧ − i_28_0 + i_28_0 ≤ 0 ∧ i_28_0 − i_28_0 ≤ 0 ∧ − i_164_post + i_164_post ≤ 0 ∧ i_164_post − i_164_post ≤ 0 ∧ − i_164_0 + i_164_0 ≤ 0 ∧ i_164_0 − i_164_0 ≤ 0 ∧ − i_105_post + i_105_post ≤ 0 ∧ i_105_post − i_105_post ≤ 0 ∧ − i_105_0 + i_105_0 ≤ 0 ∧ i_105_0 − i_105_0 ≤ 0 ∧ − head_30_post + head_30_post ≤ 0 ∧ head_30_post − head_30_post ≤ 0 ∧ − head_30_0 + head_30_0 ≤ 0 ∧ head_30_0 − head_30_0 ≤ 0 ∧ − head_15_post + head_15_post ≤ 0 ∧ head_15_post − head_15_post ≤ 0 ∧ − head_15_1 + head_15_1 ≤ 0 ∧ head_15_1 − head_15_1 ≤ 0 ∧ − head_15_0 + head_15_0 ≤ 0 ∧ head_15_0 − head_15_0 ≤ 0 ∧ − f_167_post + f_167_post ≤ 0 ∧ f_167_post − f_167_post ≤ 0 ∧ − f_167_0 + f_167_0 ≤ 0 ∧ f_167_0 − f_167_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_257_post + a_257_post ≤ 0 ∧ a_257_post − a_257_post ≤ 0 ∧ − a_257_0 + a_257_0 ≤ 0 ∧ a_257_0 − a_257_0 ≤ 0 ∧ − a_234_post + a_234_post ≤ 0 ∧ a_234_post − a_234_post ≤ 0 ∧ − a_234_0 + a_234_0 ≤ 0 ∧ a_234_0 − a_234_0 ≤ 0 ∧ − a_212_post + a_212_post ≤ 0 ∧ a_212_post − a_212_post ≤ 0 ∧ − a_212_0 + a_212_0 ≤ 0 ∧ a_212_0 − a_212_0 ≤ 0 ∧ − a_181_post + a_181_post ≤ 0 ∧ a_181_post − a_181_post ≤ 0 ∧ − a_181_0 + a_181_0 ≤ 0 ∧ a_181_0 − a_181_0 ≤ 0 ∧ − a_144_post + a_144_post ≤ 0 ∧ a_144_post − a_144_post ≤ 0 ∧ − a_144_0 + a_144_0 ≤ 0 ∧ a_144_0 − a_144_0 ≤ 0 ∧ − a_113_post + a_113_post ≤ 0 ∧ a_113_post − a_113_post ≤ 0 ∧ − a_113_0 + a_113_0 ≤ 0 ∧ a_113_0 − a_113_0 ≤ 0

7 Location Addition

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

40 80 40_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_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_172_post + x_172_post ≤ 0 ∧ x_172_post − x_172_post ≤ 0 ∧ − x_172_0 + x_172_0 ≤ 0 ∧ x_172_0 − x_172_0 ≤ 0 ∧ − x_14_post + x_14_post ≤ 0 ∧ x_14_post − x_14_post ≤ 0 ∧ − x_14_0 + x_14_0 ≤ 0 ∧ x_14_0 − x_14_0 ≤ 0 ∧ − x_126_post + x_126_post ≤ 0 ∧ x_126_post − x_126_post ≤ 0 ∧ − x_126_0 + x_126_0 ≤ 0 ∧ x_126_0 − x_126_0 ≤ 0 ∧ − tmp_32_post + tmp_32_post ≤ 0 ∧ tmp_32_post − tmp_32_post ≤ 0 ∧ − tmp_32_0 + tmp_32_0 ≤ 0 ∧ tmp_32_0 − tmp_32_0 ≤ 0 ∧ − temp_33_post + temp_33_post ≤ 0 ∧ temp_33_post − temp_33_post ≤ 0 ∧ − temp_33_0 + temp_33_0 ≤ 0 ∧ temp_33_0 − temp_33_0 ≤ 0 ∧ − temp0_29_post + temp0_29_post ≤ 0 ∧ temp0_29_post − temp0_29_post ≤ 0 ∧ − temp0_29_1 + temp0_29_1 ≤ 0 ∧ temp0_29_1 − temp0_29_1 ≤ 0 ∧ − temp0_29_0 + temp0_29_0 ≤ 0 ∧ temp0_29_0 − temp0_29_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_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_31_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_post ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_post − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_post ≤ 0 ∧ − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_0 ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_0 − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_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_86_post + rcd_86_post ≤ 0 ∧ rcd_86_post − rcd_86_post ≤ 0 ∧ − rcd_86_0 + rcd_86_0 ≤ 0 ∧ rcd_86_0 − rcd_86_0 ≤ 0 ∧ − rcd_56_post + rcd_56_post ≤ 0 ∧ rcd_56_post − rcd_56_post ≤ 0 ∧ − rcd_56_0 + rcd_56_0 ≤ 0 ∧ rcd_56_0 − rcd_56_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 ∧ − r_160_post + r_160_post ≤ 0 ∧ r_160_post − r_160_post ≤ 0 ∧ − r_160_0 + r_160_0 ≤ 0 ∧ r_160_0 − r_160_0 ≤ 0 ∧ − r_121_post + r_121_post ≤ 0 ∧ r_121_post − r_121_post ≤ 0 ∧ − r_121_0 + r_121_0 ≤ 0 ∧ r_121_0 − r_121_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_27_post + length_27_post ≤ 0 ∧ length_27_post − length_27_post ≤ 0 ∧ − length_27_0 + length_27_0 ≤ 0 ∧ length_27_0 − length_27_0 ≤ 0 ∧ − len_180_post + len_180_post ≤ 0 ∧ len_180_post − len_180_post ≤ 0 ∧ − len_180_0 + len_180_0 ≤ 0 ∧ len_180_0 − len_180_0 ≤ 0 ∧ − len_129_post + len_129_post ≤ 0 ∧ len_129_post − len_129_post ≤ 0 ∧ − len_129_0 + len_129_0 ≤ 0 ∧ len_129_0 − len_129_0 ≤ 0 ∧ − i_92_post + i_92_post ≤ 0 ∧ i_92_post − i_92_post ≤ 0 ∧ − i_92_0 + i_92_0 ≤ 0 ∧ i_92_0 − i_92_0 ≤ 0 ∧ − i_28_post + i_28_post ≤ 0 ∧ i_28_post − i_28_post ≤ 0 ∧ − i_28_0 + i_28_0 ≤ 0 ∧ i_28_0 − i_28_0 ≤ 0 ∧ − i_164_post + i_164_post ≤ 0 ∧ i_164_post − i_164_post ≤ 0 ∧ − i_164_0 + i_164_0 ≤ 0 ∧ i_164_0 − i_164_0 ≤ 0 ∧ − i_105_post + i_105_post ≤ 0 ∧ i_105_post − i_105_post ≤ 0 ∧ − i_105_0 + i_105_0 ≤ 0 ∧ i_105_0 − i_105_0 ≤ 0 ∧ − head_30_post + head_30_post ≤ 0 ∧ head_30_post − head_30_post ≤ 0 ∧ − head_30_0 + head_30_0 ≤ 0 ∧ head_30_0 − head_30_0 ≤ 0 ∧ − head_15_post + head_15_post ≤ 0 ∧ head_15_post − head_15_post ≤ 0 ∧ − head_15_1 + head_15_1 ≤ 0 ∧ head_15_1 − head_15_1 ≤ 0 ∧ − head_15_0 + head_15_0 ≤ 0 ∧ head_15_0 − head_15_0 ≤ 0 ∧ − f_167_post + f_167_post ≤ 0 ∧ f_167_post − f_167_post ≤ 0 ∧ − f_167_0 + f_167_0 ≤ 0 ∧ f_167_0 − f_167_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_257_post + a_257_post ≤ 0 ∧ a_257_post − a_257_post ≤ 0 ∧ − a_257_0 + a_257_0 ≤ 0 ∧ a_257_0 − a_257_0 ≤ 0 ∧ − a_234_post + a_234_post ≤ 0 ∧ a_234_post − a_234_post ≤ 0 ∧ − a_234_0 + a_234_0 ≤ 0 ∧ a_234_0 − a_234_0 ≤ 0 ∧ − a_212_post + a_212_post ≤ 0 ∧ a_212_post − a_212_post ≤ 0 ∧ − a_212_0 + a_212_0 ≤ 0 ∧ a_212_0 − a_212_0 ≤ 0 ∧ − a_181_post + a_181_post ≤ 0 ∧ a_181_post − a_181_post ≤ 0 ∧ − a_181_0 + a_181_0 ≤ 0 ∧ a_181_0 − a_181_0 ≤ 0 ∧ − a_144_post + a_144_post ≤ 0 ∧ a_144_post − a_144_post ≤ 0 ∧ − a_144_0 + a_144_0 ≤ 0 ∧ a_144_0 − a_144_0 ≤ 0 ∧ − a_113_post + a_113_post ≤ 0 ∧ a_113_post − a_113_post ≤ 0 ∧ − a_113_0 + a_113_0 ≤ 0 ∧ a_113_0 − a_113_0 ≤ 0

8 Location Addition

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

41* 89 41: − 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_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_172_post + x_172_post ≤ 0 ∧ x_172_post − x_172_post ≤ 0 ∧ − x_172_0 + x_172_0 ≤ 0 ∧ x_172_0 − x_172_0 ≤ 0 ∧ − x_14_post + x_14_post ≤ 0 ∧ x_14_post − x_14_post ≤ 0 ∧ − x_14_0 + x_14_0 ≤ 0 ∧ x_14_0 − x_14_0 ≤ 0 ∧ − x_126_post + x_126_post ≤ 0 ∧ x_126_post − x_126_post ≤ 0 ∧ − x_126_0 + x_126_0 ≤ 0 ∧ x_126_0 − x_126_0 ≤ 0 ∧ − tmp_32_post + tmp_32_post ≤ 0 ∧ tmp_32_post − tmp_32_post ≤ 0 ∧ − tmp_32_0 + tmp_32_0 ≤ 0 ∧ tmp_32_0 − tmp_32_0 ≤ 0 ∧ − temp_33_post + temp_33_post ≤ 0 ∧ temp_33_post − temp_33_post ≤ 0 ∧ − temp_33_0 + temp_33_0 ≤ 0 ∧ temp_33_0 − temp_33_0 ≤ 0 ∧ − temp0_29_post + temp0_29_post ≤ 0 ∧ temp0_29_post − temp0_29_post ≤ 0 ∧ − temp0_29_1 + temp0_29_1 ≤ 0 ∧ temp0_29_1 − temp0_29_1 ≤ 0 ∧ − temp0_29_0 + temp0_29_0 ≤ 0 ∧ temp0_29_0 − temp0_29_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_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_31_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_post ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_post − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_post ≤ 0 ∧ − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_0 ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_0 − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_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_86_post + rcd_86_post ≤ 0 ∧ rcd_86_post − rcd_86_post ≤ 0 ∧ − rcd_86_0 + rcd_86_0 ≤ 0 ∧ rcd_86_0 − rcd_86_0 ≤ 0 ∧ − rcd_56_post + rcd_56_post ≤ 0 ∧ rcd_56_post − rcd_56_post ≤ 0 ∧ − rcd_56_0 + rcd_56_0 ≤ 0 ∧ rcd_56_0 − rcd_56_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 ∧ − r_160_post + r_160_post ≤ 0 ∧ r_160_post − r_160_post ≤ 0 ∧ − r_160_0 + r_160_0 ≤ 0 ∧ r_160_0 − r_160_0 ≤ 0 ∧ − r_121_post + r_121_post ≤ 0 ∧ r_121_post − r_121_post ≤ 0 ∧ − r_121_0 + r_121_0 ≤ 0 ∧ r_121_0 − r_121_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_27_post + length_27_post ≤ 0 ∧ length_27_post − length_27_post ≤ 0 ∧ − length_27_0 + length_27_0 ≤ 0 ∧ length_27_0 − length_27_0 ≤ 0 ∧ − len_180_post + len_180_post ≤ 0 ∧ len_180_post − len_180_post ≤ 0 ∧ − len_180_0 + len_180_0 ≤ 0 ∧ len_180_0 − len_180_0 ≤ 0 ∧ − len_129_post + len_129_post ≤ 0 ∧ len_129_post − len_129_post ≤ 0 ∧ − len_129_0 + len_129_0 ≤ 0 ∧ len_129_0 − len_129_0 ≤ 0 ∧ − i_92_post + i_92_post ≤ 0 ∧ i_92_post − i_92_post ≤ 0 ∧ − i_92_0 + i_92_0 ≤ 0 ∧ i_92_0 − i_92_0 ≤ 0 ∧ − i_28_post + i_28_post ≤ 0 ∧ i_28_post − i_28_post ≤ 0 ∧ − i_28_0 + i_28_0 ≤ 0 ∧ i_28_0 − i_28_0 ≤ 0 ∧ − i_164_post + i_164_post ≤ 0 ∧ i_164_post − i_164_post ≤ 0 ∧ − i_164_0 + i_164_0 ≤ 0 ∧ i_164_0 − i_164_0 ≤ 0 ∧ − i_105_post + i_105_post ≤ 0 ∧ i_105_post − i_105_post ≤ 0 ∧ − i_105_0 + i_105_0 ≤ 0 ∧ i_105_0 − i_105_0 ≤ 0 ∧ − head_30_post + head_30_post ≤ 0 ∧ head_30_post − head_30_post ≤ 0 ∧ − head_30_0 + head_30_0 ≤ 0 ∧ head_30_0 − head_30_0 ≤ 0 ∧ − head_15_post + head_15_post ≤ 0 ∧ head_15_post − head_15_post ≤ 0 ∧ − head_15_1 + head_15_1 ≤ 0 ∧ head_15_1 − head_15_1 ≤ 0 ∧ − head_15_0 + head_15_0 ≤ 0 ∧ head_15_0 − head_15_0 ≤ 0 ∧ − f_167_post + f_167_post ≤ 0 ∧ f_167_post − f_167_post ≤ 0 ∧ − f_167_0 + f_167_0 ≤ 0 ∧ f_167_0 − f_167_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_257_post + a_257_post ≤ 0 ∧ a_257_post − a_257_post ≤ 0 ∧ − a_257_0 + a_257_0 ≤ 0 ∧ a_257_0 − a_257_0 ≤ 0 ∧ − a_234_post + a_234_post ≤ 0 ∧ a_234_post − a_234_post ≤ 0 ∧ − a_234_0 + a_234_0 ≤ 0 ∧ a_234_0 − a_234_0 ≤ 0 ∧ − a_212_post + a_212_post ≤ 0 ∧ a_212_post − a_212_post ≤ 0 ∧ − a_212_0 + a_212_0 ≤ 0 ∧ a_212_0 − a_212_0 ≤ 0 ∧ − a_181_post + a_181_post ≤ 0 ∧ a_181_post − a_181_post ≤ 0 ∧ − a_181_0 + a_181_0 ≤ 0 ∧ a_181_0 − a_181_0 ≤ 0 ∧ − a_144_post + a_144_post ≤ 0 ∧ a_144_post − a_144_post ≤ 0 ∧ − a_144_0 + a_144_0 ≤ 0 ∧ a_144_0 − a_144_0 ≤ 0 ∧ − a_113_post + a_113_post ≤ 0 ∧ a_113_post − a_113_post ≤ 0 ∧ − a_113_0 + a_113_0 ≤ 0 ∧ a_113_0 − a_113_0 ≤ 0

9 Location Addition

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

41 87 41_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_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_172_post + x_172_post ≤ 0 ∧ x_172_post − x_172_post ≤ 0 ∧ − x_172_0 + x_172_0 ≤ 0 ∧ x_172_0 − x_172_0 ≤ 0 ∧ − x_14_post + x_14_post ≤ 0 ∧ x_14_post − x_14_post ≤ 0 ∧ − x_14_0 + x_14_0 ≤ 0 ∧ x_14_0 − x_14_0 ≤ 0 ∧ − x_126_post + x_126_post ≤ 0 ∧ x_126_post − x_126_post ≤ 0 ∧ − x_126_0 + x_126_0 ≤ 0 ∧ x_126_0 − x_126_0 ≤ 0 ∧ − tmp_32_post + tmp_32_post ≤ 0 ∧ tmp_32_post − tmp_32_post ≤ 0 ∧ − tmp_32_0 + tmp_32_0 ≤ 0 ∧ tmp_32_0 − tmp_32_0 ≤ 0 ∧ − temp_33_post + temp_33_post ≤ 0 ∧ temp_33_post − temp_33_post ≤ 0 ∧ − temp_33_0 + temp_33_0 ≤ 0 ∧ temp_33_0 − temp_33_0 ≤ 0 ∧ − temp0_29_post + temp0_29_post ≤ 0 ∧ temp0_29_post − temp0_29_post ≤ 0 ∧ − temp0_29_1 + temp0_29_1 ≤ 0 ∧ temp0_29_1 − temp0_29_1 ≤ 0 ∧ − temp0_29_0 + temp0_29_0 ≤ 0 ∧ temp0_29_0 − temp0_29_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_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_31_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_post ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_post − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_post ≤ 0 ∧ − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_0 ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_0 − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_31_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_86_post + rcd_86_post ≤ 0 ∧ rcd_86_post − rcd_86_post ≤ 0 ∧ − rcd_86_0 + rcd_86_0 ≤ 0 ∧ rcd_86_0 − rcd_86_0 ≤ 0 ∧ − rcd_56_post + rcd_56_post ≤ 0 ∧ rcd_56_post − rcd_56_post ≤ 0 ∧ − rcd_56_0 + rcd_56_0 ≤ 0 ∧ rcd_56_0 − rcd_56_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 ∧ − r_160_post + r_160_post ≤ 0 ∧ r_160_post − r_160_post ≤ 0 ∧ − r_160_0 + r_160_0 ≤ 0 ∧ r_160_0 − r_160_0 ≤ 0 ∧ − r_121_post + r_121_post ≤ 0 ∧ r_121_post − r_121_post ≤ 0 ∧ − r_121_0 + r_121_0 ≤ 0 ∧ r_121_0 − r_121_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_27_post + length_27_post ≤ 0 ∧ length_27_post − length_27_post ≤ 0 ∧ − length_27_0 + length_27_0 ≤ 0 ∧ length_27_0 − length_27_0 ≤ 0 ∧ − len_180_post + len_180_post ≤ 0 ∧ len_180_post − len_180_post ≤ 0 ∧ − len_180_0 + len_180_0 ≤ 0 ∧ len_180_0 − len_180_0 ≤ 0 ∧ − len_129_post + len_129_post ≤ 0 ∧ len_129_post − len_129_post ≤ 0 ∧ − len_129_0 + len_129_0 ≤ 0 ∧ len_129_0 − len_129_0 ≤ 0 ∧ − i_92_post + i_92_post ≤ 0 ∧ i_92_post − i_92_post ≤ 0 ∧ − i_92_0 + i_92_0 ≤ 0 ∧ i_92_0 − i_92_0 ≤ 0 ∧ − i_28_post + i_28_post ≤ 0 ∧ i_28_post − i_28_post ≤ 0 ∧ − i_28_0 + i_28_0 ≤ 0 ∧ i_28_0 − i_28_0 ≤ 0 ∧ − i_164_post + i_164_post ≤ 0 ∧ i_164_post − i_164_post ≤ 0 ∧ − i_164_0 + i_164_0 ≤ 0 ∧ i_164_0 − i_164_0 ≤ 0 ∧ − i_105_post + i_105_post ≤ 0 ∧ i_105_post − i_105_post ≤ 0 ∧ − i_105_0 + i_105_0 ≤ 0 ∧ i_105_0 − i_105_0 ≤ 0 ∧ − head_30_post + head_30_post ≤ 0 ∧ head_30_post − head_30_post ≤ 0 ∧ − head_30_0 + head_30_0 ≤ 0 ∧ head_30_0 − head_30_0 ≤ 0 ∧ − head_15_post + head_15_post ≤ 0 ∧ head_15_post − head_15_post ≤ 0 ∧ − head_15_1 + head_15_1 ≤ 0 ∧ head_15_1 − head_15_1 ≤ 0 ∧ − head_15_0 + head_15_0 ≤ 0 ∧ head_15_0 − head_15_0 ≤ 0 ∧ − f_167_post + f_167_post ≤ 0 ∧ f_167_post − f_167_post ≤ 0 ∧ − f_167_0 + f_167_0 ≤ 0 ∧ f_167_0 − f_167_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_257_post + a_257_post ≤ 0 ∧ a_257_post − a_257_post ≤ 0 ∧ − a_257_0 + a_257_0 ≤ 0 ∧ a_257_0 − a_257_0 ≤ 0 ∧ − a_234_post + a_234_post ≤ 0 ∧ a_234_post − a_234_post ≤ 0 ∧ − a_234_0 + a_234_0 ≤ 0 ∧ a_234_0 − a_234_0 ≤ 0 ∧ − a_212_post + a_212_post ≤ 0 ∧ a_212_post − a_212_post ≤ 0 ∧ − a_212_0 + a_212_0 ≤ 0 ∧ a_212_0 − a_212_0 ≤ 0 ∧ − a_181_post + a_181_post ≤ 0 ∧ a_181_post − a_181_post ≤ 0 ∧ − a_181_0 + a_181_0 ≤ 0 ∧ a_181_0 − a_181_0 ≤ 0 ∧ − a_144_post + a_144_post ≤ 0 ∧ a_144_post − a_144_post ≤ 0 ∧ − a_144_0 + a_144_0 ≤ 0 ∧ a_144_0 − a_144_0 ≤ 0 ∧ − a_113_post + a_113_post ≤ 0 ∧ a_113_post − a_113_post ≤ 0 ∧ − a_113_0 + a_113_0 ≤ 0 ∧ a_113_0 − a_113_0 ≤ 0

10 SCC Decomposition

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

10.1 SCC Subproblem 1/3

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

10.1.1 Transition Removal

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

2: −2 + 10⋅a_234_0
4: −4 + 10⋅a_234_0
5: −5 + 10⋅a_234_0
6: 4 + 10⋅a_257_0
7: 3 + 10⋅a_257_0
8: 2 + 10⋅a_257_0
9: 1 + 10⋅a_257_0
10: 10⋅a_234_0
2_var_snapshot: −3 + 10⋅a_234_0
2*: −1 + 10⋅a_234_0

10.1.2 Transition Removal

We remove transitions 73, 5, 6, 7, 8, 9 using the following ranking functions, which are bounded by −3.

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

10.1.3 Transition Removal

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

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

10.1.4 Splitting Cut-Point Transitions

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

10.1.4.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 72.

10.1.4.1.1 Splitting Cut-Point Transitions

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

10.2 SCC Subproblem 2/3

Here we consider the SCC { 41, 44, 45, 46, 47, 48, 49, 41_var_snapshot, 41* }.

10.2.1 Transition Removal

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

41: −1 + 9⋅a_144_0
44: −3 + 9⋅a_144_0
45: −4 + 9⋅a_144_0
46: 4 + 9⋅a_181_0
47: 3 + 9⋅a_181_0
48: 2 + 9⋅a_181_0
49: 1 + 9⋅a_144_0
41_var_snapshot: −2 + 9⋅a_144_0
41*: 9⋅a_144_0

10.2.2 Transition Removal

We remove transitions 87, 89, 45, 46, 47, 48, 49, 50 using the following ranking functions, which are bounded by −3.

41: −2
44: 5
45: 4
46: 3
47: 2
48: 1
49: 0
41_var_snapshot: −3
41*: −1

10.2.3 Splitting Cut-Point Transitions

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

10.2.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 86.

10.2.3.1.1 Splitting Cut-Point Transitions

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

10.3 SCC Subproblem 3/3

Here we consider the SCC { 40, 64, 40_var_snapshot, 40* }.

10.3.1 Transition Removal

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

40: −2 − 4⋅i_28_0 + 4⋅length_27_0
64: −4⋅i_28_0 + 4⋅length_27_0
40_var_snapshot: −3 − 4⋅i_28_0 + 4⋅length_27_0
40*: −1 − 4⋅i_28_0 + 4⋅length_27_0

10.3.2 Transition Removal

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

40: 0
64: 2⋅length_27_0
40_var_snapshot: − length_27_0
40*: −2 + 2⋅length_27_0

10.3.3 Splitting Cut-Point Transitions

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

10.3.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 79.

10.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