LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Invariant Updates

The following invariants are asserted.

5: 2 − result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0
6: −1 + i_31_post ≤ 01 − i_31_post ≤ 0−1 + i_31_0 ≤ 01 − i_31_0 ≤ 01 − length_29_0 ≤ 0
7: −1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 01 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0
8: −1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 01 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0
9: −1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 01 − result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0−1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 01 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0
10: −1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 01 − result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0−1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 01 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0
11: −1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_post ≤ 01 − result_dot_nondet_sdv_special_RETURN_VALUE_14_post ≤ 0−1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 01 − result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0−1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 01 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0
12: −1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_post ≤ 01 − result_dot_nondet_sdv_special_RETURN_VALUE_14_post ≤ 0−1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 01 − result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0−1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 01 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0
13: −1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 01 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0
14: −1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 01 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0
15: −1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 01 − result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0−1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 01 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0
16: −1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 01 − result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0−1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 01 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0
17: −1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 01 − result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0−1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 01 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0
18: −1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 01 − result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0−1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 01 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0
19: TRUE
20: 2 − length_29_0 ≤ 0
21: len_159_0 ≤ 0len_159_0 ≤ 0
22: len_159_0 ≤ 0len_159_0 ≤ 0
23: 2 − length_29_0 ≤ 0
24: i_31_post ≤ 0i_31_post ≤ 0i_31_0 ≤ 0i_31_0 ≤ 0
25: 2 − result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0a_174_0 ≤ 0
26: a_174_0 ≤ 0a_279_0 ≤ 0
27: a_174_0 ≤ 0a_279_0 ≤ 0
28: a_174_0 ≤ 0a_279_0 ≤ 0
29: a_174_0 ≤ 0a_279_0 ≤ 0
30: a_174_0 ≤ 0a_279_0 ≤ 0
31: a_174_0 ≤ 0a_279_0 ≤ 0
32: 2 − result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0a_174_0 ≤ 0
42: 2 − result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0len_159_0 ≤ 0a_174_0 ≤ 0
43: len_159_0 ≤ 0a_174_0 ≤ 0
44: len_159_0 ≤ 0a_174_0 ≤ 0
45: len_159_0 ≤ 0a_174_0 ≤ 0
46: len_159_0 ≤ 0a_174_0 ≤ 0
47: len_159_0 ≤ 0a_174_0 ≤ 0
48: len_159_0 ≤ 0a_174_0 ≤ 0
49: TRUE
50: len_159_0 ≤ 0a_174_0 ≤ 0
51: len_159_0 ≤ 0a_174_0 ≤ 0
52: len_159_0 ≤ 0a_174_0 ≤ 0
53: len_159_0 ≤ 0a_174_0 ≤ 0
54: len_159_0 ≤ 0a_174_0 ≤ 01 − len_221_post ≤ 01 − len_221_0 ≤ 0
55: len_159_0 ≤ 0a_174_0 ≤ 01 − len_221_post ≤ 01 − len_221_0 ≤ 0
56: len_159_0 ≤ 0a_174_0 ≤ 01 − len_221_post ≤ 01 − len_221_0 ≤ 0
57: 2 − result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 01 − len_221_post ≤ 01 − len_221_0 ≤ 0
66: TRUE

The invariants are proved as follows.

IMPACT Invariant Proof

2 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
5 73 5: y_26_post + y_26_post ≤ 0y_26_posty_26_post ≤ 0y_26_1 + y_26_1 ≤ 0y_26_1y_26_1 ≤ 0y_26_0 + y_26_0 ≤ 0y_26_0y_26_0 ≤ 0y_21_post + y_21_post ≤ 0y_21_posty_21_post ≤ 0y_21_1 + y_21_1 ≤ 0y_21_1y_21_1 ≤ 0y_21_0 + y_21_0 ≤ 0y_21_0y_21_0 ≤ 0x_SLAM_f_25_post + x_SLAM_f_25_post ≤ 0x_SLAM_f_25_postx_SLAM_f_25_post ≤ 0x_SLAM_f_25_1 + x_SLAM_f_25_1 ≤ 0x_SLAM_f_25_1x_SLAM_f_25_1 ≤ 0x_SLAM_f_25_0 + x_SLAM_f_25_0 ≤ 0x_SLAM_f_25_0x_SLAM_f_25_0 ≤ 0x_SLAM_f_20_post + x_SLAM_f_20_post ≤ 0x_SLAM_f_20_postx_SLAM_f_20_post ≤ 0x_SLAM_f_20_1 + x_SLAM_f_20_1 ≤ 0x_SLAM_f_20_1x_SLAM_f_20_1 ≤ 0x_SLAM_f_20_0 + x_SLAM_f_20_0 ≤ 0x_SLAM_f_20_0x_SLAM_f_20_0 ≤ 0x_27_post + x_27_post ≤ 0x_27_postx_27_post ≤ 0x_27_1 + x_27_1 ≤ 0x_27_1x_27_1 ≤ 0x_27_0 + x_27_0 ≤ 0x_27_0x_27_0 ≤ 0x_22_post + x_22_post ≤ 0x_22_postx_22_post ≤ 0x_22_1 + x_22_1 ≤ 0x_22_1x_22_1 ≤ 0x_22_0 + x_22_0 ≤ 0x_22_0x_22_0 ≤ 0x_207_post + x_207_post ≤ 0x_207_postx_207_post ≤ 0x_207_0 + x_207_0 ≤ 0x_207_0x_207_0 ≤ 0x_154_post + x_154_post ≤ 0x_154_postx_154_post ≤ 0x_154_0 + x_154_0 ≤ 0x_154_0x_154_0 ≤ 0tmp_35_post + tmp_35_post ≤ 0tmp_35_posttmp_35_post ≤ 0tmp_35_0 + tmp_35_0 ≤ 0tmp_35_0tmp_35_0 ≤ 0temp_37_post + temp_37_post ≤ 0temp_37_posttemp_37_post ≤ 0temp_37_0 + temp_37_0 ≤ 0temp_37_0temp_37_0 ≤ 0temp_36_post + temp_36_post ≤ 0temp_36_posttemp_36_post ≤ 0temp_36_0 + temp_36_0 ≤ 0temp_36_0temp_36_0 ≤ 0temp0_32_post + temp0_32_post ≤ 0temp0_32_posttemp0_32_post ≤ 0temp0_32_1 + temp0_32_1 ≤ 0temp0_32_1temp0_32_1 ≤ 0temp0_32_0 + temp0_32_0 ≤ 0temp0_32_0temp0_32_0 ≤ 0temp0_19_0 + temp0_19_0 ≤ 0temp0_19_0temp0_19_0 ≤ 0tail_15_post + tail_15_post ≤ 0tail_15_posttail_15_post ≤ 0tail_15_0 + tail_15_0 ≤ 0tail_15_0tail_15_0 ≤ 0t_23_post + t_23_post ≤ 0t_23_postt_23_post ≤ 0t_23_0 + t_23_0 ≤ 0t_23_0t_23_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_post + result_dot_nondet_sdv_special_RETURN_VALUE_14_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_postresult_dot_nondet_sdv_special_RETURN_VALUE_14_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_2 + result_dot_nondet_sdv_special_RETURN_VALUE_14_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_2result_dot_nondet_sdv_special_RETURN_VALUE_14_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_1result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_0 + result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_0result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_postresult_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_postresult_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_1 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_1 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_1result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_1 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_0 ≤ 0result_11_post + result_11_post ≤ 0result_11_postresult_11_post ≤ 0result_11_2 + result_11_2 ≤ 0result_11_2result_11_2 ≤ 0result_11_1 + result_11_1 ≤ 0result_11_1result_11_1 ≤ 0result_11_0 + result_11_0 ≤ 0result_11_0result_11_0 ≤ 0rcd_71_post + rcd_71_post ≤ 0rcd_71_postrcd_71_post ≤ 0rcd_71_0 + rcd_71_0 ≤ 0rcd_71_0rcd_71_0 ≤ 0rcd_45_post + rcd_45_post ≤ 0rcd_45_postrcd_45_post ≤ 0rcd_45_0 + rcd_45_0 ≤ 0rcd_45_0rcd_45_0 ≤ 0rcd_320_post + rcd_320_post ≤ 0rcd_320_postrcd_320_post ≤ 0rcd_320_0 + rcd_320_0 ≤ 0rcd_320_0rcd_320_0 ≤ 0rcd_308_post + rcd_308_post ≤ 0rcd_308_postrcd_308_post ≤ 0rcd_308_0 + rcd_308_0 ≤ 0rcd_308_0rcd_308_0 ≤ 0rcd_288_post + rcd_288_post ≤ 0rcd_288_postrcd_288_post ≤ 0rcd_288_0 + rcd_288_0 ≤ 0rcd_288_0rcd_288_0 ≤ 0rcd_284_post + rcd_284_post ≤ 0rcd_284_postrcd_284_post ≤ 0rcd_284_0 + rcd_284_0 ≤ 0rcd_284_0rcd_284_0 ≤ 0rcd_220_post + rcd_220_post ≤ 0rcd_220_postrcd_220_post ≤ 0rcd_220_0 + rcd_220_0 ≤ 0rcd_220_0rcd_220_0 ≤ 0rcd_199_post + rcd_199_post ≤ 0rcd_199_postrcd_199_post ≤ 0rcd_199_0 + rcd_199_0 ≤ 0rcd_199_0rcd_199_0 ≤ 0rcd_194_post + rcd_194_post ≤ 0rcd_194_postrcd_194_post ≤ 0rcd_194_0 + rcd_194_0 ≤ 0rcd_194_0rcd_194_0 ≤ 0rcd_193_post + rcd_193_post ≤ 0rcd_193_postrcd_193_post ≤ 0rcd_193_0 + rcd_193_0 ≤ 0rcd_193_0rcd_193_0 ≤ 0rcd_185_post + rcd_185_post ≤ 0rcd_185_postrcd_185_post ≤ 0rcd_185_0 + rcd_185_0 ≤ 0rcd_185_0rcd_185_0 ≤ 0rcd_114_post + rcd_114_post ≤ 0rcd_114_postrcd_114_post ≤ 0rcd_114_0 + rcd_114_0 ≤ 0rcd_114_0rcd_114_0 ≤ 0rcd_106_post + rcd_106_post ≤ 0rcd_106_postrcd_106_post ≤ 0rcd_106_0 + rcd_106_0 ≤ 0rcd_106_0rcd_106_0 ≤ 0r_41_post + r_41_post ≤ 0r_41_postr_41_post ≤ 0r_41_0 + r_41_0 ≤ 0r_41_0r_41_0 ≤ 0r_192_post + r_192_post ≤ 0r_192_postr_192_post ≤ 0r_192_0 + r_192_0 ≤ 0r_192_0r_192_0 ≤ 0r_149_post + r_149_post ≤ 0r_149_postr_149_post ≤ 0r_149_0 + r_149_0 ≤ 0r_149_0r_149_0 ≤ 0nondet_12_post + nondet_12_post ≤ 0nondet_12_postnondet_12_post ≤ 0nondet_12_1 + nondet_12_1 ≤ 0nondet_12_1nondet_12_1 ≤ 0nondet_12_0 + nondet_12_0 ≤ 0nondet_12_0nondet_12_0 ≤ 0length_29_post + length_29_post ≤ 0length_29_postlength_29_post ≤ 0length_29_0 + length_29_0 ≤ 0length_29_0length_29_0 ≤ 0len_221_post + len_221_post ≤ 0len_221_postlen_221_post ≤ 0len_221_0 + len_221_0 ≤ 0len_221_0len_221_0 ≤ 0len_159_post + len_159_post ≤ 0len_159_postlen_159_post ≤ 0len_159_0 + len_159_0 ≤ 0len_159_0len_159_0 ≤ 0i_31_post + i_31_post ≤ 0i_31_posti_31_post ≤ 0i_31_0 + i_31_0 ≤ 0i_31_0i_31_0 ≤ 0i_198_post + i_198_post ≤ 0i_198_posti_198_post ≤ 0i_198_0 + i_198_0 ≤ 0i_198_0i_198_0 ≤ 0i_130_post + i_130_post ≤ 0i_130_posti_130_post ≤ 0i_130_0 + i_130_0 ≤ 0i_130_0i_130_0 ≤ 0i_112_post + i_112_post ≤ 0i_112_posti_112_post ≤ 0i_112_0 + i_112_0 ≤ 0i_112_0i_112_0 ≤ 0head_SLAM_f_30_post + head_SLAM_f_30_post ≤ 0head_SLAM_f_30_posthead_SLAM_f_30_post ≤ 0head_SLAM_f_30_0 + head_SLAM_f_30_0 ≤ 0head_SLAM_f_30_0head_SLAM_f_30_0 ≤ 0head_33_post + head_33_post ≤ 0head_33_posthead_33_post ≤ 0head_33_0 + head_33_0 ≤ 0head_33_0head_33_0 ≤ 0head_16_post + head_16_post ≤ 0head_16_posthead_16_post ≤ 0head_16_1 + head_16_1 ≤ 0head_16_1head_16_1 ≤ 0head_16_0 + head_16_0 ≤ 0head_16_0head_16_0 ≤ 0f_202_post + f_202_post ≤ 0f_202_postf_202_post ≤ 0f_202_0 + f_202_0 ≤ 0f_202_0f_202_0 ≤ 0a_309_post + a_309_post ≤ 0a_309_posta_309_post ≤ 0a_309_0 + a_309_0 ≤ 0a_309_0a_309_0 ≤ 0a_279_post + a_279_post ≤ 0a_279_posta_279_post ≤ 0a_279_0 + a_279_0 ≤ 0a_279_0a_279_0 ≤ 0a_253_post + a_253_post ≤ 0a_253_posta_253_post ≤ 0a_253_0 + a_253_0 ≤ 0a_253_0a_253_0 ≤ 0a_222_post + a_222_post ≤ 0a_222_posta_222_post ≤ 0a_222_0 + a_222_0 ≤ 0a_222_0a_222_0 ≤ 0a_174_post + a_174_post ≤ 0a_174_posta_174_post ≤ 0a_174_0 + a_174_0 ≤ 0a_174_0a_174_0 ≤ 0a_139_post + a_139_post ≤ 0a_139_posta_139_post ≤ 0a_139_0 + a_139_0 ≤ 0a_139_0a_139_0 ≤ 0
20 80 20: y_26_post + y_26_post ≤ 0y_26_posty_26_post ≤ 0y_26_1 + y_26_1 ≤ 0y_26_1y_26_1 ≤ 0y_26_0 + y_26_0 ≤ 0y_26_0y_26_0 ≤ 0y_21_post + y_21_post ≤ 0y_21_posty_21_post ≤ 0y_21_1 + y_21_1 ≤ 0y_21_1y_21_1 ≤ 0y_21_0 + y_21_0 ≤ 0y_21_0y_21_0 ≤ 0x_SLAM_f_25_post + x_SLAM_f_25_post ≤ 0x_SLAM_f_25_postx_SLAM_f_25_post ≤ 0x_SLAM_f_25_1 + x_SLAM_f_25_1 ≤ 0x_SLAM_f_25_1x_SLAM_f_25_1 ≤ 0x_SLAM_f_25_0 + x_SLAM_f_25_0 ≤ 0x_SLAM_f_25_0x_SLAM_f_25_0 ≤ 0x_SLAM_f_20_post + x_SLAM_f_20_post ≤ 0x_SLAM_f_20_postx_SLAM_f_20_post ≤ 0x_SLAM_f_20_1 + x_SLAM_f_20_1 ≤ 0x_SLAM_f_20_1x_SLAM_f_20_1 ≤ 0x_SLAM_f_20_0 + x_SLAM_f_20_0 ≤ 0x_SLAM_f_20_0x_SLAM_f_20_0 ≤ 0x_27_post + x_27_post ≤ 0x_27_postx_27_post ≤ 0x_27_1 + x_27_1 ≤ 0x_27_1x_27_1 ≤ 0x_27_0 + x_27_0 ≤ 0x_27_0x_27_0 ≤ 0x_22_post + x_22_post ≤ 0x_22_postx_22_post ≤ 0x_22_1 + x_22_1 ≤ 0x_22_1x_22_1 ≤ 0x_22_0 + x_22_0 ≤ 0x_22_0x_22_0 ≤ 0x_207_post + x_207_post ≤ 0x_207_postx_207_post ≤ 0x_207_0 + x_207_0 ≤ 0x_207_0x_207_0 ≤ 0x_154_post + x_154_post ≤ 0x_154_postx_154_post ≤ 0x_154_0 + x_154_0 ≤ 0x_154_0x_154_0 ≤ 0tmp_35_post + tmp_35_post ≤ 0tmp_35_posttmp_35_post ≤ 0tmp_35_0 + tmp_35_0 ≤ 0tmp_35_0tmp_35_0 ≤ 0temp_37_post + temp_37_post ≤ 0temp_37_posttemp_37_post ≤ 0temp_37_0 + temp_37_0 ≤ 0temp_37_0temp_37_0 ≤ 0temp_36_post + temp_36_post ≤ 0temp_36_posttemp_36_post ≤ 0temp_36_0 + temp_36_0 ≤ 0temp_36_0temp_36_0 ≤ 0temp0_32_post + temp0_32_post ≤ 0temp0_32_posttemp0_32_post ≤ 0temp0_32_1 + temp0_32_1 ≤ 0temp0_32_1temp0_32_1 ≤ 0temp0_32_0 + temp0_32_0 ≤ 0temp0_32_0temp0_32_0 ≤ 0temp0_19_0 + temp0_19_0 ≤ 0temp0_19_0temp0_19_0 ≤ 0tail_15_post + tail_15_post ≤ 0tail_15_posttail_15_post ≤ 0tail_15_0 + tail_15_0 ≤ 0tail_15_0tail_15_0 ≤ 0t_23_post + t_23_post ≤ 0t_23_postt_23_post ≤ 0t_23_0 + t_23_0 ≤ 0t_23_0t_23_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_post + result_dot_nondet_sdv_special_RETURN_VALUE_14_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_postresult_dot_nondet_sdv_special_RETURN_VALUE_14_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_2 + result_dot_nondet_sdv_special_RETURN_VALUE_14_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_2result_dot_nondet_sdv_special_RETURN_VALUE_14_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_1result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_0 + result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_0result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_postresult_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_postresult_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_1 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_1 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_1result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_1 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_0 ≤ 0result_11_post + result_11_post ≤ 0result_11_postresult_11_post ≤ 0result_11_2 + result_11_2 ≤ 0result_11_2result_11_2 ≤ 0result_11_1 + result_11_1 ≤ 0result_11_1result_11_1 ≤ 0result_11_0 + result_11_0 ≤ 0result_11_0result_11_0 ≤ 0rcd_71_post + rcd_71_post ≤ 0rcd_71_postrcd_71_post ≤ 0rcd_71_0 + rcd_71_0 ≤ 0rcd_71_0rcd_71_0 ≤ 0rcd_45_post + rcd_45_post ≤ 0rcd_45_postrcd_45_post ≤ 0rcd_45_0 + rcd_45_0 ≤ 0rcd_45_0rcd_45_0 ≤ 0rcd_320_post + rcd_320_post ≤ 0rcd_320_postrcd_320_post ≤ 0rcd_320_0 + rcd_320_0 ≤ 0rcd_320_0rcd_320_0 ≤ 0rcd_308_post + rcd_308_post ≤ 0rcd_308_postrcd_308_post ≤ 0rcd_308_0 + rcd_308_0 ≤ 0rcd_308_0rcd_308_0 ≤ 0rcd_288_post + rcd_288_post ≤ 0rcd_288_postrcd_288_post ≤ 0rcd_288_0 + rcd_288_0 ≤ 0rcd_288_0rcd_288_0 ≤ 0rcd_284_post + rcd_284_post ≤ 0rcd_284_postrcd_284_post ≤ 0rcd_284_0 + rcd_284_0 ≤ 0rcd_284_0rcd_284_0 ≤ 0rcd_220_post + rcd_220_post ≤ 0rcd_220_postrcd_220_post ≤ 0rcd_220_0 + rcd_220_0 ≤ 0rcd_220_0rcd_220_0 ≤ 0rcd_199_post + rcd_199_post ≤ 0rcd_199_postrcd_199_post ≤ 0rcd_199_0 + rcd_199_0 ≤ 0rcd_199_0rcd_199_0 ≤ 0rcd_194_post + rcd_194_post ≤ 0rcd_194_postrcd_194_post ≤ 0rcd_194_0 + rcd_194_0 ≤ 0rcd_194_0rcd_194_0 ≤ 0rcd_193_post + rcd_193_post ≤ 0rcd_193_postrcd_193_post ≤ 0rcd_193_0 + rcd_193_0 ≤ 0rcd_193_0rcd_193_0 ≤ 0rcd_185_post + rcd_185_post ≤ 0rcd_185_postrcd_185_post ≤ 0rcd_185_0 + rcd_185_0 ≤ 0rcd_185_0rcd_185_0 ≤ 0rcd_114_post + rcd_114_post ≤ 0rcd_114_postrcd_114_post ≤ 0rcd_114_0 + rcd_114_0 ≤ 0rcd_114_0rcd_114_0 ≤ 0rcd_106_post + rcd_106_post ≤ 0rcd_106_postrcd_106_post ≤ 0rcd_106_0 + rcd_106_0 ≤ 0rcd_106_0rcd_106_0 ≤ 0r_41_post + r_41_post ≤ 0r_41_postr_41_post ≤ 0r_41_0 + r_41_0 ≤ 0r_41_0r_41_0 ≤ 0r_192_post + r_192_post ≤ 0r_192_postr_192_post ≤ 0r_192_0 + r_192_0 ≤ 0r_192_0r_192_0 ≤ 0r_149_post + r_149_post ≤ 0r_149_postr_149_post ≤ 0r_149_0 + r_149_0 ≤ 0r_149_0r_149_0 ≤ 0nondet_12_post + nondet_12_post ≤ 0nondet_12_postnondet_12_post ≤ 0nondet_12_1 + nondet_12_1 ≤ 0nondet_12_1nondet_12_1 ≤ 0nondet_12_0 + nondet_12_0 ≤ 0nondet_12_0nondet_12_0 ≤ 0length_29_post + length_29_post ≤ 0length_29_postlength_29_post ≤ 0length_29_0 + length_29_0 ≤ 0length_29_0length_29_0 ≤ 0len_221_post + len_221_post ≤ 0len_221_postlen_221_post ≤ 0len_221_0 + len_221_0 ≤ 0len_221_0len_221_0 ≤ 0len_159_post + len_159_post ≤ 0len_159_postlen_159_post ≤ 0len_159_0 + len_159_0 ≤ 0len_159_0len_159_0 ≤ 0i_31_post + i_31_post ≤ 0i_31_posti_31_post ≤ 0i_31_0 + i_31_0 ≤ 0i_31_0i_31_0 ≤ 0i_198_post + i_198_post ≤ 0i_198_posti_198_post ≤ 0i_198_0 + i_198_0 ≤ 0i_198_0i_198_0 ≤ 0i_130_post + i_130_post ≤ 0i_130_posti_130_post ≤ 0i_130_0 + i_130_0 ≤ 0i_130_0i_130_0 ≤ 0i_112_post + i_112_post ≤ 0i_112_posti_112_post ≤ 0i_112_0 + i_112_0 ≤ 0i_112_0i_112_0 ≤ 0head_SLAM_f_30_post + head_SLAM_f_30_post ≤ 0head_SLAM_f_30_posthead_SLAM_f_30_post ≤ 0head_SLAM_f_30_0 + head_SLAM_f_30_0 ≤ 0head_SLAM_f_30_0head_SLAM_f_30_0 ≤ 0head_33_post + head_33_post ≤ 0head_33_posthead_33_post ≤ 0head_33_0 + head_33_0 ≤ 0head_33_0head_33_0 ≤ 0head_16_post + head_16_post ≤ 0head_16_posthead_16_post ≤ 0head_16_1 + head_16_1 ≤ 0head_16_1head_16_1 ≤ 0head_16_0 + head_16_0 ≤ 0head_16_0head_16_0 ≤ 0f_202_post + f_202_post ≤ 0f_202_postf_202_post ≤ 0f_202_0 + f_202_0 ≤ 0f_202_0f_202_0 ≤ 0a_309_post + a_309_post ≤ 0a_309_posta_309_post ≤ 0a_309_0 + a_309_0 ≤ 0a_309_0a_309_0 ≤ 0a_279_post + a_279_post ≤ 0a_279_posta_279_post ≤ 0a_279_0 + a_279_0 ≤ 0a_279_0a_279_0 ≤ 0a_253_post + a_253_post ≤ 0a_253_posta_253_post ≤ 0a_253_0 + a_253_0 ≤ 0a_253_0a_253_0 ≤ 0a_222_post + a_222_post ≤ 0a_222_posta_222_post ≤ 0a_222_0 + a_222_0 ≤ 0a_222_0a_222_0 ≤ 0a_174_post + a_174_post ≤ 0a_174_posta_174_post ≤ 0a_174_0 + a_174_0 ≤ 0a_174_0a_174_0 ≤ 0a_139_post + a_139_post ≤ 0a_139_posta_139_post ≤ 0a_139_0 + a_139_0 ≤ 0a_139_0a_139_0 ≤ 0
25 87 25: y_26_post + y_26_post ≤ 0y_26_posty_26_post ≤ 0y_26_1 + y_26_1 ≤ 0y_26_1y_26_1 ≤ 0y_26_0 + y_26_0 ≤ 0y_26_0y_26_0 ≤ 0y_21_post + y_21_post ≤ 0y_21_posty_21_post ≤ 0y_21_1 + y_21_1 ≤ 0y_21_1y_21_1 ≤ 0y_21_0 + y_21_0 ≤ 0y_21_0y_21_0 ≤ 0x_SLAM_f_25_post + x_SLAM_f_25_post ≤ 0x_SLAM_f_25_postx_SLAM_f_25_post ≤ 0x_SLAM_f_25_1 + x_SLAM_f_25_1 ≤ 0x_SLAM_f_25_1x_SLAM_f_25_1 ≤ 0x_SLAM_f_25_0 + x_SLAM_f_25_0 ≤ 0x_SLAM_f_25_0x_SLAM_f_25_0 ≤ 0x_SLAM_f_20_post + x_SLAM_f_20_post ≤ 0x_SLAM_f_20_postx_SLAM_f_20_post ≤ 0x_SLAM_f_20_1 + x_SLAM_f_20_1 ≤ 0x_SLAM_f_20_1x_SLAM_f_20_1 ≤ 0x_SLAM_f_20_0 + x_SLAM_f_20_0 ≤ 0x_SLAM_f_20_0x_SLAM_f_20_0 ≤ 0x_27_post + x_27_post ≤ 0x_27_postx_27_post ≤ 0x_27_1 + x_27_1 ≤ 0x_27_1x_27_1 ≤ 0x_27_0 + x_27_0 ≤ 0x_27_0x_27_0 ≤ 0x_22_post + x_22_post ≤ 0x_22_postx_22_post ≤ 0x_22_1 + x_22_1 ≤ 0x_22_1x_22_1 ≤ 0x_22_0 + x_22_0 ≤ 0x_22_0x_22_0 ≤ 0x_207_post + x_207_post ≤ 0x_207_postx_207_post ≤ 0x_207_0 + x_207_0 ≤ 0x_207_0x_207_0 ≤ 0x_154_post + x_154_post ≤ 0x_154_postx_154_post ≤ 0x_154_0 + x_154_0 ≤ 0x_154_0x_154_0 ≤ 0tmp_35_post + tmp_35_post ≤ 0tmp_35_posttmp_35_post ≤ 0tmp_35_0 + tmp_35_0 ≤ 0tmp_35_0tmp_35_0 ≤ 0temp_37_post + temp_37_post ≤ 0temp_37_posttemp_37_post ≤ 0temp_37_0 + temp_37_0 ≤ 0temp_37_0temp_37_0 ≤ 0temp_36_post + temp_36_post ≤ 0temp_36_posttemp_36_post ≤ 0temp_36_0 + temp_36_0 ≤ 0temp_36_0temp_36_0 ≤ 0temp0_32_post + temp0_32_post ≤ 0temp0_32_posttemp0_32_post ≤ 0temp0_32_1 + temp0_32_1 ≤ 0temp0_32_1temp0_32_1 ≤ 0temp0_32_0 + temp0_32_0 ≤ 0temp0_32_0temp0_32_0 ≤ 0temp0_19_0 + temp0_19_0 ≤ 0temp0_19_0temp0_19_0 ≤ 0tail_15_post + tail_15_post ≤ 0tail_15_posttail_15_post ≤ 0tail_15_0 + tail_15_0 ≤ 0tail_15_0tail_15_0 ≤ 0t_23_post + t_23_post ≤ 0t_23_postt_23_post ≤ 0t_23_0 + t_23_0 ≤ 0t_23_0t_23_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_post + result_dot_nondet_sdv_special_RETURN_VALUE_14_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_postresult_dot_nondet_sdv_special_RETURN_VALUE_14_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_2 + result_dot_nondet_sdv_special_RETURN_VALUE_14_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_2result_dot_nondet_sdv_special_RETURN_VALUE_14_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_1result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_0 + result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_0result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_postresult_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_postresult_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_1 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_1 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_1result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_1 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_0 ≤ 0result_11_post + result_11_post ≤ 0result_11_postresult_11_post ≤ 0result_11_2 + result_11_2 ≤ 0result_11_2result_11_2 ≤ 0result_11_1 + result_11_1 ≤ 0result_11_1result_11_1 ≤ 0result_11_0 + result_11_0 ≤ 0result_11_0result_11_0 ≤ 0rcd_71_post + rcd_71_post ≤ 0rcd_71_postrcd_71_post ≤ 0rcd_71_0 + rcd_71_0 ≤ 0rcd_71_0rcd_71_0 ≤ 0rcd_45_post + rcd_45_post ≤ 0rcd_45_postrcd_45_post ≤ 0rcd_45_0 + rcd_45_0 ≤ 0rcd_45_0rcd_45_0 ≤ 0rcd_320_post + rcd_320_post ≤ 0rcd_320_postrcd_320_post ≤ 0rcd_320_0 + rcd_320_0 ≤ 0rcd_320_0rcd_320_0 ≤ 0rcd_308_post + rcd_308_post ≤ 0rcd_308_postrcd_308_post ≤ 0rcd_308_0 + rcd_308_0 ≤ 0rcd_308_0rcd_308_0 ≤ 0rcd_288_post + rcd_288_post ≤ 0rcd_288_postrcd_288_post ≤ 0rcd_288_0 + rcd_288_0 ≤ 0rcd_288_0rcd_288_0 ≤ 0rcd_284_post + rcd_284_post ≤ 0rcd_284_postrcd_284_post ≤ 0rcd_284_0 + rcd_284_0 ≤ 0rcd_284_0rcd_284_0 ≤ 0rcd_220_post + rcd_220_post ≤ 0rcd_220_postrcd_220_post ≤ 0rcd_220_0 + rcd_220_0 ≤ 0rcd_220_0rcd_220_0 ≤ 0rcd_199_post + rcd_199_post ≤ 0rcd_199_postrcd_199_post ≤ 0rcd_199_0 + rcd_199_0 ≤ 0rcd_199_0rcd_199_0 ≤ 0rcd_194_post + rcd_194_post ≤ 0rcd_194_postrcd_194_post ≤ 0rcd_194_0 + rcd_194_0 ≤ 0rcd_194_0rcd_194_0 ≤ 0rcd_193_post + rcd_193_post ≤ 0rcd_193_postrcd_193_post ≤ 0rcd_193_0 + rcd_193_0 ≤ 0rcd_193_0rcd_193_0 ≤ 0rcd_185_post + rcd_185_post ≤ 0rcd_185_postrcd_185_post ≤ 0rcd_185_0 + rcd_185_0 ≤ 0rcd_185_0rcd_185_0 ≤ 0rcd_114_post + rcd_114_post ≤ 0rcd_114_postrcd_114_post ≤ 0rcd_114_0 + rcd_114_0 ≤ 0rcd_114_0rcd_114_0 ≤ 0rcd_106_post + rcd_106_post ≤ 0rcd_106_postrcd_106_post ≤ 0rcd_106_0 + rcd_106_0 ≤ 0rcd_106_0rcd_106_0 ≤ 0r_41_post + r_41_post ≤ 0r_41_postr_41_post ≤ 0r_41_0 + r_41_0 ≤ 0r_41_0r_41_0 ≤ 0r_192_post + r_192_post ≤ 0r_192_postr_192_post ≤ 0r_192_0 + r_192_0 ≤ 0r_192_0r_192_0 ≤ 0r_149_post + r_149_post ≤ 0r_149_postr_149_post ≤ 0r_149_0 + r_149_0 ≤ 0r_149_0r_149_0 ≤ 0nondet_12_post + nondet_12_post ≤ 0nondet_12_postnondet_12_post ≤ 0nondet_12_1 + nondet_12_1 ≤ 0nondet_12_1nondet_12_1 ≤ 0nondet_12_0 + nondet_12_0 ≤ 0nondet_12_0nondet_12_0 ≤ 0length_29_post + length_29_post ≤ 0length_29_postlength_29_post ≤ 0length_29_0 + length_29_0 ≤ 0length_29_0length_29_0 ≤ 0len_221_post + len_221_post ≤ 0len_221_postlen_221_post ≤ 0len_221_0 + len_221_0 ≤ 0len_221_0len_221_0 ≤ 0len_159_post + len_159_post ≤ 0len_159_postlen_159_post ≤ 0len_159_0 + len_159_0 ≤ 0len_159_0len_159_0 ≤ 0i_31_post + i_31_post ≤ 0i_31_posti_31_post ≤ 0i_31_0 + i_31_0 ≤ 0i_31_0i_31_0 ≤ 0i_198_post + i_198_post ≤ 0i_198_posti_198_post ≤ 0i_198_0 + i_198_0 ≤ 0i_198_0i_198_0 ≤ 0i_130_post + i_130_post ≤ 0i_130_posti_130_post ≤ 0i_130_0 + i_130_0 ≤ 0i_130_0i_130_0 ≤ 0i_112_post + i_112_post ≤ 0i_112_posti_112_post ≤ 0i_112_0 + i_112_0 ≤ 0i_112_0i_112_0 ≤ 0head_SLAM_f_30_post + head_SLAM_f_30_post ≤ 0head_SLAM_f_30_posthead_SLAM_f_30_post ≤ 0head_SLAM_f_30_0 + head_SLAM_f_30_0 ≤ 0head_SLAM_f_30_0head_SLAM_f_30_0 ≤ 0head_33_post + head_33_post ≤ 0head_33_posthead_33_post ≤ 0head_33_0 + head_33_0 ≤ 0head_33_0head_33_0 ≤ 0head_16_post + head_16_post ≤ 0head_16_posthead_16_post ≤ 0head_16_1 + head_16_1 ≤ 0head_16_1head_16_1 ≤ 0head_16_0 + head_16_0 ≤ 0head_16_0head_16_0 ≤ 0f_202_post + f_202_post ≤ 0f_202_postf_202_post ≤ 0f_202_0 + f_202_0 ≤ 0f_202_0f_202_0 ≤ 0a_309_post + a_309_post ≤ 0a_309_posta_309_post ≤ 0a_309_0 + a_309_0 ≤ 0a_309_0a_309_0 ≤ 0a_279_post + a_279_post ≤ 0a_279_posta_279_post ≤ 0a_279_0 + a_279_0 ≤ 0a_279_0a_279_0 ≤ 0a_253_post + a_253_post ≤ 0a_253_posta_253_post ≤ 0a_253_0 + a_253_0 ≤ 0a_253_0a_253_0 ≤ 0a_222_post + a_222_post ≤ 0a_222_posta_222_post ≤ 0a_222_0 + a_222_0 ≤ 0a_222_0a_222_0 ≤ 0a_174_post + a_174_post ≤ 0a_174_posta_174_post ≤ 0a_174_0 + a_174_0 ≤ 0a_174_0a_174_0 ≤ 0a_139_post + a_139_post ≤ 0a_139_posta_139_post ≤ 0a_139_0 + a_139_0 ≤ 0a_139_0a_139_0 ≤ 0
and for every transition t, a duplicate t is considered.

3 Transition Removal

We remove transitions 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 24, 25, 26, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 72 using the following ranking functions, which are bounded by −71.

66: 0
49: 0
24: 0
6: 0
7: 0
8: 0
9: 0
10: 0
11: 0
12: 0
13: 0
14: 0
15: 0
16: 0
17: 0
18: 0
20: 0
23: 0
21: 0
22: 0
5: 0
52: 0
53: 0
54: 0
55: 0
56: 0
57: 0
50: 0
51: 0
42: 0
43: 0
44: 0
45: 0
46: 0
47: 0
48: 0
25: 0
26: 0
27: 0
28: 0
29: 0
30: 0
31: 0
32: 0
19: 0
66: −32
49: −33
24: −34
6: −35
7: −36
8: −37
9: −38
10: −39
11: −40
12: −41
13: −42
14: −43
15: −44
16: −45
17: −46
18: −47
20: −48
23: −48
20_var_snapshot: −48
20*: −48
21: −51
22: −52
5: −53
52: −53
53: −53
54: −53
55: −53
56: −53
57: −53
5_var_snapshot: −53
5*: −53
50: −56
51: −57
42: −58
43: −59
44: −60
45: −61
46: −62
47: −63
48: −64
25: −65
26: −65
27: −65
28: −65
29: −65
30: −65
31: −65
32: −65
25_var_snapshot: −65
25*: −65
19: −69

4 Location Addition

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

5* 76 5: y_26_post + y_26_post ≤ 0y_26_posty_26_post ≤ 0y_26_1 + y_26_1 ≤ 0y_26_1y_26_1 ≤ 0y_26_0 + y_26_0 ≤ 0y_26_0y_26_0 ≤ 0y_21_post + y_21_post ≤ 0y_21_posty_21_post ≤ 0y_21_1 + y_21_1 ≤ 0y_21_1y_21_1 ≤ 0y_21_0 + y_21_0 ≤ 0y_21_0y_21_0 ≤ 0x_SLAM_f_25_post + x_SLAM_f_25_post ≤ 0x_SLAM_f_25_postx_SLAM_f_25_post ≤ 0x_SLAM_f_25_1 + x_SLAM_f_25_1 ≤ 0x_SLAM_f_25_1x_SLAM_f_25_1 ≤ 0x_SLAM_f_25_0 + x_SLAM_f_25_0 ≤ 0x_SLAM_f_25_0x_SLAM_f_25_0 ≤ 0x_SLAM_f_20_post + x_SLAM_f_20_post ≤ 0x_SLAM_f_20_postx_SLAM_f_20_post ≤ 0x_SLAM_f_20_1 + x_SLAM_f_20_1 ≤ 0x_SLAM_f_20_1x_SLAM_f_20_1 ≤ 0x_SLAM_f_20_0 + x_SLAM_f_20_0 ≤ 0x_SLAM_f_20_0x_SLAM_f_20_0 ≤ 0x_27_post + x_27_post ≤ 0x_27_postx_27_post ≤ 0x_27_1 + x_27_1 ≤ 0x_27_1x_27_1 ≤ 0x_27_0 + x_27_0 ≤ 0x_27_0x_27_0 ≤ 0x_22_post + x_22_post ≤ 0x_22_postx_22_post ≤ 0x_22_1 + x_22_1 ≤ 0x_22_1x_22_1 ≤ 0x_22_0 + x_22_0 ≤ 0x_22_0x_22_0 ≤ 0x_207_post + x_207_post ≤ 0x_207_postx_207_post ≤ 0x_207_0 + x_207_0 ≤ 0x_207_0x_207_0 ≤ 0x_154_post + x_154_post ≤ 0x_154_postx_154_post ≤ 0x_154_0 + x_154_0 ≤ 0x_154_0x_154_0 ≤ 0tmp_35_post + tmp_35_post ≤ 0tmp_35_posttmp_35_post ≤ 0tmp_35_0 + tmp_35_0 ≤ 0tmp_35_0tmp_35_0 ≤ 0temp_37_post + temp_37_post ≤ 0temp_37_posttemp_37_post ≤ 0temp_37_0 + temp_37_0 ≤ 0temp_37_0temp_37_0 ≤ 0temp_36_post + temp_36_post ≤ 0temp_36_posttemp_36_post ≤ 0temp_36_0 + temp_36_0 ≤ 0temp_36_0temp_36_0 ≤ 0temp0_32_post + temp0_32_post ≤ 0temp0_32_posttemp0_32_post ≤ 0temp0_32_1 + temp0_32_1 ≤ 0temp0_32_1temp0_32_1 ≤ 0temp0_32_0 + temp0_32_0 ≤ 0temp0_32_0temp0_32_0 ≤ 0temp0_19_0 + temp0_19_0 ≤ 0temp0_19_0temp0_19_0 ≤ 0tail_15_post + tail_15_post ≤ 0tail_15_posttail_15_post ≤ 0tail_15_0 + tail_15_0 ≤ 0tail_15_0tail_15_0 ≤ 0t_23_post + t_23_post ≤ 0t_23_postt_23_post ≤ 0t_23_0 + t_23_0 ≤ 0t_23_0t_23_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_post + result_dot_nondet_sdv_special_RETURN_VALUE_14_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_postresult_dot_nondet_sdv_special_RETURN_VALUE_14_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_2 + result_dot_nondet_sdv_special_RETURN_VALUE_14_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_2result_dot_nondet_sdv_special_RETURN_VALUE_14_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_1result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_0 + result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_0result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_postresult_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_postresult_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_1 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_1 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_1result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_1 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_0 ≤ 0result_11_post + result_11_post ≤ 0result_11_postresult_11_post ≤ 0result_11_2 + result_11_2 ≤ 0result_11_2result_11_2 ≤ 0result_11_1 + result_11_1 ≤ 0result_11_1result_11_1 ≤ 0result_11_0 + result_11_0 ≤ 0result_11_0result_11_0 ≤ 0rcd_71_post + rcd_71_post ≤ 0rcd_71_postrcd_71_post ≤ 0rcd_71_0 + rcd_71_0 ≤ 0rcd_71_0rcd_71_0 ≤ 0rcd_45_post + rcd_45_post ≤ 0rcd_45_postrcd_45_post ≤ 0rcd_45_0 + rcd_45_0 ≤ 0rcd_45_0rcd_45_0 ≤ 0rcd_320_post + rcd_320_post ≤ 0rcd_320_postrcd_320_post ≤ 0rcd_320_0 + rcd_320_0 ≤ 0rcd_320_0rcd_320_0 ≤ 0rcd_308_post + rcd_308_post ≤ 0rcd_308_postrcd_308_post ≤ 0rcd_308_0 + rcd_308_0 ≤ 0rcd_308_0rcd_308_0 ≤ 0rcd_288_post + rcd_288_post ≤ 0rcd_288_postrcd_288_post ≤ 0rcd_288_0 + rcd_288_0 ≤ 0rcd_288_0rcd_288_0 ≤ 0rcd_284_post + rcd_284_post ≤ 0rcd_284_postrcd_284_post ≤ 0rcd_284_0 + rcd_284_0 ≤ 0rcd_284_0rcd_284_0 ≤ 0rcd_220_post + rcd_220_post ≤ 0rcd_220_postrcd_220_post ≤ 0rcd_220_0 + rcd_220_0 ≤ 0rcd_220_0rcd_220_0 ≤ 0rcd_199_post + rcd_199_post ≤ 0rcd_199_postrcd_199_post ≤ 0rcd_199_0 + rcd_199_0 ≤ 0rcd_199_0rcd_199_0 ≤ 0rcd_194_post + rcd_194_post ≤ 0rcd_194_postrcd_194_post ≤ 0rcd_194_0 + rcd_194_0 ≤ 0rcd_194_0rcd_194_0 ≤ 0rcd_193_post + rcd_193_post ≤ 0rcd_193_postrcd_193_post ≤ 0rcd_193_0 + rcd_193_0 ≤ 0rcd_193_0rcd_193_0 ≤ 0rcd_185_post + rcd_185_post ≤ 0rcd_185_postrcd_185_post ≤ 0rcd_185_0 + rcd_185_0 ≤ 0rcd_185_0rcd_185_0 ≤ 0rcd_114_post + rcd_114_post ≤ 0rcd_114_postrcd_114_post ≤ 0rcd_114_0 + rcd_114_0 ≤ 0rcd_114_0rcd_114_0 ≤ 0rcd_106_post + rcd_106_post ≤ 0rcd_106_postrcd_106_post ≤ 0rcd_106_0 + rcd_106_0 ≤ 0rcd_106_0rcd_106_0 ≤ 0r_41_post + r_41_post ≤ 0r_41_postr_41_post ≤ 0r_41_0 + r_41_0 ≤ 0r_41_0r_41_0 ≤ 0r_192_post + r_192_post ≤ 0r_192_postr_192_post ≤ 0r_192_0 + r_192_0 ≤ 0r_192_0r_192_0 ≤ 0r_149_post + r_149_post ≤ 0r_149_postr_149_post ≤ 0r_149_0 + r_149_0 ≤ 0r_149_0r_149_0 ≤ 0nondet_12_post + nondet_12_post ≤ 0nondet_12_postnondet_12_post ≤ 0nondet_12_1 + nondet_12_1 ≤ 0nondet_12_1nondet_12_1 ≤ 0nondet_12_0 + nondet_12_0 ≤ 0nondet_12_0nondet_12_0 ≤ 0length_29_post + length_29_post ≤ 0length_29_postlength_29_post ≤ 0length_29_0 + length_29_0 ≤ 0length_29_0length_29_0 ≤ 0len_221_post + len_221_post ≤ 0len_221_postlen_221_post ≤ 0len_221_0 + len_221_0 ≤ 0len_221_0len_221_0 ≤ 0len_159_post + len_159_post ≤ 0len_159_postlen_159_post ≤ 0len_159_0 + len_159_0 ≤ 0len_159_0len_159_0 ≤ 0i_31_post + i_31_post ≤ 0i_31_posti_31_post ≤ 0i_31_0 + i_31_0 ≤ 0i_31_0i_31_0 ≤ 0i_198_post + i_198_post ≤ 0i_198_posti_198_post ≤ 0i_198_0 + i_198_0 ≤ 0i_198_0i_198_0 ≤ 0i_130_post + i_130_post ≤ 0i_130_posti_130_post ≤ 0i_130_0 + i_130_0 ≤ 0i_130_0i_130_0 ≤ 0i_112_post + i_112_post ≤ 0i_112_posti_112_post ≤ 0i_112_0 + i_112_0 ≤ 0i_112_0i_112_0 ≤ 0head_SLAM_f_30_post + head_SLAM_f_30_post ≤ 0head_SLAM_f_30_posthead_SLAM_f_30_post ≤ 0head_SLAM_f_30_0 + head_SLAM_f_30_0 ≤ 0head_SLAM_f_30_0head_SLAM_f_30_0 ≤ 0head_33_post + head_33_post ≤ 0head_33_posthead_33_post ≤ 0head_33_0 + head_33_0 ≤ 0head_33_0head_33_0 ≤ 0head_16_post + head_16_post ≤ 0head_16_posthead_16_post ≤ 0head_16_1 + head_16_1 ≤ 0head_16_1head_16_1 ≤ 0head_16_0 + head_16_0 ≤ 0head_16_0head_16_0 ≤ 0f_202_post + f_202_post ≤ 0f_202_postf_202_post ≤ 0f_202_0 + f_202_0 ≤ 0f_202_0f_202_0 ≤ 0a_309_post + a_309_post ≤ 0a_309_posta_309_post ≤ 0a_309_0 + a_309_0 ≤ 0a_309_0a_309_0 ≤ 0a_279_post + a_279_post ≤ 0a_279_posta_279_post ≤ 0a_279_0 + a_279_0 ≤ 0a_279_0a_279_0 ≤ 0a_253_post + a_253_post ≤ 0a_253_posta_253_post ≤ 0a_253_0 + a_253_0 ≤ 0a_253_0a_253_0 ≤ 0a_222_post + a_222_post ≤ 0a_222_posta_222_post ≤ 0a_222_0 + a_222_0 ≤ 0a_222_0a_222_0 ≤ 0a_174_post + a_174_post ≤ 0a_174_posta_174_post ≤ 0a_174_0 + a_174_0 ≤ 0a_174_0a_174_0 ≤ 0a_139_post + a_139_post ≤ 0a_139_posta_139_post ≤ 0a_139_0 + a_139_0 ≤ 0a_139_0a_139_0 ≤ 0

5 Location Addition

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

5 74 5_var_snapshot: y_26_post + y_26_post ≤ 0y_26_posty_26_post ≤ 0y_26_1 + y_26_1 ≤ 0y_26_1y_26_1 ≤ 0y_26_0 + y_26_0 ≤ 0y_26_0y_26_0 ≤ 0y_21_post + y_21_post ≤ 0y_21_posty_21_post ≤ 0y_21_1 + y_21_1 ≤ 0y_21_1y_21_1 ≤ 0y_21_0 + y_21_0 ≤ 0y_21_0y_21_0 ≤ 0x_SLAM_f_25_post + x_SLAM_f_25_post ≤ 0x_SLAM_f_25_postx_SLAM_f_25_post ≤ 0x_SLAM_f_25_1 + x_SLAM_f_25_1 ≤ 0x_SLAM_f_25_1x_SLAM_f_25_1 ≤ 0x_SLAM_f_25_0 + x_SLAM_f_25_0 ≤ 0x_SLAM_f_25_0x_SLAM_f_25_0 ≤ 0x_SLAM_f_20_post + x_SLAM_f_20_post ≤ 0x_SLAM_f_20_postx_SLAM_f_20_post ≤ 0x_SLAM_f_20_1 + x_SLAM_f_20_1 ≤ 0x_SLAM_f_20_1x_SLAM_f_20_1 ≤ 0x_SLAM_f_20_0 + x_SLAM_f_20_0 ≤ 0x_SLAM_f_20_0x_SLAM_f_20_0 ≤ 0x_27_post + x_27_post ≤ 0x_27_postx_27_post ≤ 0x_27_1 + x_27_1 ≤ 0x_27_1x_27_1 ≤ 0x_27_0 + x_27_0 ≤ 0x_27_0x_27_0 ≤ 0x_22_post + x_22_post ≤ 0x_22_postx_22_post ≤ 0x_22_1 + x_22_1 ≤ 0x_22_1x_22_1 ≤ 0x_22_0 + x_22_0 ≤ 0x_22_0x_22_0 ≤ 0x_207_post + x_207_post ≤ 0x_207_postx_207_post ≤ 0x_207_0 + x_207_0 ≤ 0x_207_0x_207_0 ≤ 0x_154_post + x_154_post ≤ 0x_154_postx_154_post ≤ 0x_154_0 + x_154_0 ≤ 0x_154_0x_154_0 ≤ 0tmp_35_post + tmp_35_post ≤ 0tmp_35_posttmp_35_post ≤ 0tmp_35_0 + tmp_35_0 ≤ 0tmp_35_0tmp_35_0 ≤ 0temp_37_post + temp_37_post ≤ 0temp_37_posttemp_37_post ≤ 0temp_37_0 + temp_37_0 ≤ 0temp_37_0temp_37_0 ≤ 0temp_36_post + temp_36_post ≤ 0temp_36_posttemp_36_post ≤ 0temp_36_0 + temp_36_0 ≤ 0temp_36_0temp_36_0 ≤ 0temp0_32_post + temp0_32_post ≤ 0temp0_32_posttemp0_32_post ≤ 0temp0_32_1 + temp0_32_1 ≤ 0temp0_32_1temp0_32_1 ≤ 0temp0_32_0 + temp0_32_0 ≤ 0temp0_32_0temp0_32_0 ≤ 0temp0_19_0 + temp0_19_0 ≤ 0temp0_19_0temp0_19_0 ≤ 0tail_15_post + tail_15_post ≤ 0tail_15_posttail_15_post ≤ 0tail_15_0 + tail_15_0 ≤ 0tail_15_0tail_15_0 ≤ 0t_23_post + t_23_post ≤ 0t_23_postt_23_post ≤ 0t_23_0 + t_23_0 ≤ 0t_23_0t_23_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_post + result_dot_nondet_sdv_special_RETURN_VALUE_14_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_postresult_dot_nondet_sdv_special_RETURN_VALUE_14_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_2 + result_dot_nondet_sdv_special_RETURN_VALUE_14_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_2result_dot_nondet_sdv_special_RETURN_VALUE_14_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_1result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_0 + result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_0result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_postresult_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_postresult_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_1 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_1 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_1result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_1 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_0 ≤ 0result_11_post + result_11_post ≤ 0result_11_postresult_11_post ≤ 0result_11_2 + result_11_2 ≤ 0result_11_2result_11_2 ≤ 0result_11_1 + result_11_1 ≤ 0result_11_1result_11_1 ≤ 0result_11_0 + result_11_0 ≤ 0result_11_0result_11_0 ≤ 0rcd_71_post + rcd_71_post ≤ 0rcd_71_postrcd_71_post ≤ 0rcd_71_0 + rcd_71_0 ≤ 0rcd_71_0rcd_71_0 ≤ 0rcd_45_post + rcd_45_post ≤ 0rcd_45_postrcd_45_post ≤ 0rcd_45_0 + rcd_45_0 ≤ 0rcd_45_0rcd_45_0 ≤ 0rcd_320_post + rcd_320_post ≤ 0rcd_320_postrcd_320_post ≤ 0rcd_320_0 + rcd_320_0 ≤ 0rcd_320_0rcd_320_0 ≤ 0rcd_308_post + rcd_308_post ≤ 0rcd_308_postrcd_308_post ≤ 0rcd_308_0 + rcd_308_0 ≤ 0rcd_308_0rcd_308_0 ≤ 0rcd_288_post + rcd_288_post ≤ 0rcd_288_postrcd_288_post ≤ 0rcd_288_0 + rcd_288_0 ≤ 0rcd_288_0rcd_288_0 ≤ 0rcd_284_post + rcd_284_post ≤ 0rcd_284_postrcd_284_post ≤ 0rcd_284_0 + rcd_284_0 ≤ 0rcd_284_0rcd_284_0 ≤ 0rcd_220_post + rcd_220_post ≤ 0rcd_220_postrcd_220_post ≤ 0rcd_220_0 + rcd_220_0 ≤ 0rcd_220_0rcd_220_0 ≤ 0rcd_199_post + rcd_199_post ≤ 0rcd_199_postrcd_199_post ≤ 0rcd_199_0 + rcd_199_0 ≤ 0rcd_199_0rcd_199_0 ≤ 0rcd_194_post + rcd_194_post ≤ 0rcd_194_postrcd_194_post ≤ 0rcd_194_0 + rcd_194_0 ≤ 0rcd_194_0rcd_194_0 ≤ 0rcd_193_post + rcd_193_post ≤ 0rcd_193_postrcd_193_post ≤ 0rcd_193_0 + rcd_193_0 ≤ 0rcd_193_0rcd_193_0 ≤ 0rcd_185_post + rcd_185_post ≤ 0rcd_185_postrcd_185_post ≤ 0rcd_185_0 + rcd_185_0 ≤ 0rcd_185_0rcd_185_0 ≤ 0rcd_114_post + rcd_114_post ≤ 0rcd_114_postrcd_114_post ≤ 0rcd_114_0 + rcd_114_0 ≤ 0rcd_114_0rcd_114_0 ≤ 0rcd_106_post + rcd_106_post ≤ 0rcd_106_postrcd_106_post ≤ 0rcd_106_0 + rcd_106_0 ≤ 0rcd_106_0rcd_106_0 ≤ 0r_41_post + r_41_post ≤ 0r_41_postr_41_post ≤ 0r_41_0 + r_41_0 ≤ 0r_41_0r_41_0 ≤ 0r_192_post + r_192_post ≤ 0r_192_postr_192_post ≤ 0r_192_0 + r_192_0 ≤ 0r_192_0r_192_0 ≤ 0r_149_post + r_149_post ≤ 0r_149_postr_149_post ≤ 0r_149_0 + r_149_0 ≤ 0r_149_0r_149_0 ≤ 0nondet_12_post + nondet_12_post ≤ 0nondet_12_postnondet_12_post ≤ 0nondet_12_1 + nondet_12_1 ≤ 0nondet_12_1nondet_12_1 ≤ 0nondet_12_0 + nondet_12_0 ≤ 0nondet_12_0nondet_12_0 ≤ 0length_29_post + length_29_post ≤ 0length_29_postlength_29_post ≤ 0length_29_0 + length_29_0 ≤ 0length_29_0length_29_0 ≤ 0len_221_post + len_221_post ≤ 0len_221_postlen_221_post ≤ 0len_221_0 + len_221_0 ≤ 0len_221_0len_221_0 ≤ 0len_159_post + len_159_post ≤ 0len_159_postlen_159_post ≤ 0len_159_0 + len_159_0 ≤ 0len_159_0len_159_0 ≤ 0i_31_post + i_31_post ≤ 0i_31_posti_31_post ≤ 0i_31_0 + i_31_0 ≤ 0i_31_0i_31_0 ≤ 0i_198_post + i_198_post ≤ 0i_198_posti_198_post ≤ 0i_198_0 + i_198_0 ≤ 0i_198_0i_198_0 ≤ 0i_130_post + i_130_post ≤ 0i_130_posti_130_post ≤ 0i_130_0 + i_130_0 ≤ 0i_130_0i_130_0 ≤ 0i_112_post + i_112_post ≤ 0i_112_posti_112_post ≤ 0i_112_0 + i_112_0 ≤ 0i_112_0i_112_0 ≤ 0head_SLAM_f_30_post + head_SLAM_f_30_post ≤ 0head_SLAM_f_30_posthead_SLAM_f_30_post ≤ 0head_SLAM_f_30_0 + head_SLAM_f_30_0 ≤ 0head_SLAM_f_30_0head_SLAM_f_30_0 ≤ 0head_33_post + head_33_post ≤ 0head_33_posthead_33_post ≤ 0head_33_0 + head_33_0 ≤ 0head_33_0head_33_0 ≤ 0head_16_post + head_16_post ≤ 0head_16_posthead_16_post ≤ 0head_16_1 + head_16_1 ≤ 0head_16_1head_16_1 ≤ 0head_16_0 + head_16_0 ≤ 0head_16_0head_16_0 ≤ 0f_202_post + f_202_post ≤ 0f_202_postf_202_post ≤ 0f_202_0 + f_202_0 ≤ 0f_202_0f_202_0 ≤ 0a_309_post + a_309_post ≤ 0a_309_posta_309_post ≤ 0a_309_0 + a_309_0 ≤ 0a_309_0a_309_0 ≤ 0a_279_post + a_279_post ≤ 0a_279_posta_279_post ≤ 0a_279_0 + a_279_0 ≤ 0a_279_0a_279_0 ≤ 0a_253_post + a_253_post ≤ 0a_253_posta_253_post ≤ 0a_253_0 + a_253_0 ≤ 0a_253_0a_253_0 ≤ 0a_222_post + a_222_post ≤ 0a_222_posta_222_post ≤ 0a_222_0 + a_222_0 ≤ 0a_222_0a_222_0 ≤ 0a_174_post + a_174_post ≤ 0a_174_posta_174_post ≤ 0a_174_0 + a_174_0 ≤ 0a_174_0a_174_0 ≤ 0a_139_post + a_139_post ≤ 0a_139_posta_139_post ≤ 0a_139_0 + a_139_0 ≤ 0a_139_0a_139_0 ≤ 0

6 Location Addition

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

20* 83 20: y_26_post + y_26_post ≤ 0y_26_posty_26_post ≤ 0y_26_1 + y_26_1 ≤ 0y_26_1y_26_1 ≤ 0y_26_0 + y_26_0 ≤ 0y_26_0y_26_0 ≤ 0y_21_post + y_21_post ≤ 0y_21_posty_21_post ≤ 0y_21_1 + y_21_1 ≤ 0y_21_1y_21_1 ≤ 0y_21_0 + y_21_0 ≤ 0y_21_0y_21_0 ≤ 0x_SLAM_f_25_post + x_SLAM_f_25_post ≤ 0x_SLAM_f_25_postx_SLAM_f_25_post ≤ 0x_SLAM_f_25_1 + x_SLAM_f_25_1 ≤ 0x_SLAM_f_25_1x_SLAM_f_25_1 ≤ 0x_SLAM_f_25_0 + x_SLAM_f_25_0 ≤ 0x_SLAM_f_25_0x_SLAM_f_25_0 ≤ 0x_SLAM_f_20_post + x_SLAM_f_20_post ≤ 0x_SLAM_f_20_postx_SLAM_f_20_post ≤ 0x_SLAM_f_20_1 + x_SLAM_f_20_1 ≤ 0x_SLAM_f_20_1x_SLAM_f_20_1 ≤ 0x_SLAM_f_20_0 + x_SLAM_f_20_0 ≤ 0x_SLAM_f_20_0x_SLAM_f_20_0 ≤ 0x_27_post + x_27_post ≤ 0x_27_postx_27_post ≤ 0x_27_1 + x_27_1 ≤ 0x_27_1x_27_1 ≤ 0x_27_0 + x_27_0 ≤ 0x_27_0x_27_0 ≤ 0x_22_post + x_22_post ≤ 0x_22_postx_22_post ≤ 0x_22_1 + x_22_1 ≤ 0x_22_1x_22_1 ≤ 0x_22_0 + x_22_0 ≤ 0x_22_0x_22_0 ≤ 0x_207_post + x_207_post ≤ 0x_207_postx_207_post ≤ 0x_207_0 + x_207_0 ≤ 0x_207_0x_207_0 ≤ 0x_154_post + x_154_post ≤ 0x_154_postx_154_post ≤ 0x_154_0 + x_154_0 ≤ 0x_154_0x_154_0 ≤ 0tmp_35_post + tmp_35_post ≤ 0tmp_35_posttmp_35_post ≤ 0tmp_35_0 + tmp_35_0 ≤ 0tmp_35_0tmp_35_0 ≤ 0temp_37_post + temp_37_post ≤ 0temp_37_posttemp_37_post ≤ 0temp_37_0 + temp_37_0 ≤ 0temp_37_0temp_37_0 ≤ 0temp_36_post + temp_36_post ≤ 0temp_36_posttemp_36_post ≤ 0temp_36_0 + temp_36_0 ≤ 0temp_36_0temp_36_0 ≤ 0temp0_32_post + temp0_32_post ≤ 0temp0_32_posttemp0_32_post ≤ 0temp0_32_1 + temp0_32_1 ≤ 0temp0_32_1temp0_32_1 ≤ 0temp0_32_0 + temp0_32_0 ≤ 0temp0_32_0temp0_32_0 ≤ 0temp0_19_0 + temp0_19_0 ≤ 0temp0_19_0temp0_19_0 ≤ 0tail_15_post + tail_15_post ≤ 0tail_15_posttail_15_post ≤ 0tail_15_0 + tail_15_0 ≤ 0tail_15_0tail_15_0 ≤ 0t_23_post + t_23_post ≤ 0t_23_postt_23_post ≤ 0t_23_0 + t_23_0 ≤ 0t_23_0t_23_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_post + result_dot_nondet_sdv_special_RETURN_VALUE_14_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_postresult_dot_nondet_sdv_special_RETURN_VALUE_14_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_2 + result_dot_nondet_sdv_special_RETURN_VALUE_14_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_2result_dot_nondet_sdv_special_RETURN_VALUE_14_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_1result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_0 + result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_0result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_postresult_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_postresult_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_1 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_1 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_1result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_1 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_0 ≤ 0result_11_post + result_11_post ≤ 0result_11_postresult_11_post ≤ 0result_11_2 + result_11_2 ≤ 0result_11_2result_11_2 ≤ 0result_11_1 + result_11_1 ≤ 0result_11_1result_11_1 ≤ 0result_11_0 + result_11_0 ≤ 0result_11_0result_11_0 ≤ 0rcd_71_post + rcd_71_post ≤ 0rcd_71_postrcd_71_post ≤ 0rcd_71_0 + rcd_71_0 ≤ 0rcd_71_0rcd_71_0 ≤ 0rcd_45_post + rcd_45_post ≤ 0rcd_45_postrcd_45_post ≤ 0rcd_45_0 + rcd_45_0 ≤ 0rcd_45_0rcd_45_0 ≤ 0rcd_320_post + rcd_320_post ≤ 0rcd_320_postrcd_320_post ≤ 0rcd_320_0 + rcd_320_0 ≤ 0rcd_320_0rcd_320_0 ≤ 0rcd_308_post + rcd_308_post ≤ 0rcd_308_postrcd_308_post ≤ 0rcd_308_0 + rcd_308_0 ≤ 0rcd_308_0rcd_308_0 ≤ 0rcd_288_post + rcd_288_post ≤ 0rcd_288_postrcd_288_post ≤ 0rcd_288_0 + rcd_288_0 ≤ 0rcd_288_0rcd_288_0 ≤ 0rcd_284_post + rcd_284_post ≤ 0rcd_284_postrcd_284_post ≤ 0rcd_284_0 + rcd_284_0 ≤ 0rcd_284_0rcd_284_0 ≤ 0rcd_220_post + rcd_220_post ≤ 0rcd_220_postrcd_220_post ≤ 0rcd_220_0 + rcd_220_0 ≤ 0rcd_220_0rcd_220_0 ≤ 0rcd_199_post + rcd_199_post ≤ 0rcd_199_postrcd_199_post ≤ 0rcd_199_0 + rcd_199_0 ≤ 0rcd_199_0rcd_199_0 ≤ 0rcd_194_post + rcd_194_post ≤ 0rcd_194_postrcd_194_post ≤ 0rcd_194_0 + rcd_194_0 ≤ 0rcd_194_0rcd_194_0 ≤ 0rcd_193_post + rcd_193_post ≤ 0rcd_193_postrcd_193_post ≤ 0rcd_193_0 + rcd_193_0 ≤ 0rcd_193_0rcd_193_0 ≤ 0rcd_185_post + rcd_185_post ≤ 0rcd_185_postrcd_185_post ≤ 0rcd_185_0 + rcd_185_0 ≤ 0rcd_185_0rcd_185_0 ≤ 0rcd_114_post + rcd_114_post ≤ 0rcd_114_postrcd_114_post ≤ 0rcd_114_0 + rcd_114_0 ≤ 0rcd_114_0rcd_114_0 ≤ 0rcd_106_post + rcd_106_post ≤ 0rcd_106_postrcd_106_post ≤ 0rcd_106_0 + rcd_106_0 ≤ 0rcd_106_0rcd_106_0 ≤ 0r_41_post + r_41_post ≤ 0r_41_postr_41_post ≤ 0r_41_0 + r_41_0 ≤ 0r_41_0r_41_0 ≤ 0r_192_post + r_192_post ≤ 0r_192_postr_192_post ≤ 0r_192_0 + r_192_0 ≤ 0r_192_0r_192_0 ≤ 0r_149_post + r_149_post ≤ 0r_149_postr_149_post ≤ 0r_149_0 + r_149_0 ≤ 0r_149_0r_149_0 ≤ 0nondet_12_post + nondet_12_post ≤ 0nondet_12_postnondet_12_post ≤ 0nondet_12_1 + nondet_12_1 ≤ 0nondet_12_1nondet_12_1 ≤ 0nondet_12_0 + nondet_12_0 ≤ 0nondet_12_0nondet_12_0 ≤ 0length_29_post + length_29_post ≤ 0length_29_postlength_29_post ≤ 0length_29_0 + length_29_0 ≤ 0length_29_0length_29_0 ≤ 0len_221_post + len_221_post ≤ 0len_221_postlen_221_post ≤ 0len_221_0 + len_221_0 ≤ 0len_221_0len_221_0 ≤ 0len_159_post + len_159_post ≤ 0len_159_postlen_159_post ≤ 0len_159_0 + len_159_0 ≤ 0len_159_0len_159_0 ≤ 0i_31_post + i_31_post ≤ 0i_31_posti_31_post ≤ 0i_31_0 + i_31_0 ≤ 0i_31_0i_31_0 ≤ 0i_198_post + i_198_post ≤ 0i_198_posti_198_post ≤ 0i_198_0 + i_198_0 ≤ 0i_198_0i_198_0 ≤ 0i_130_post + i_130_post ≤ 0i_130_posti_130_post ≤ 0i_130_0 + i_130_0 ≤ 0i_130_0i_130_0 ≤ 0i_112_post + i_112_post ≤ 0i_112_posti_112_post ≤ 0i_112_0 + i_112_0 ≤ 0i_112_0i_112_0 ≤ 0head_SLAM_f_30_post + head_SLAM_f_30_post ≤ 0head_SLAM_f_30_posthead_SLAM_f_30_post ≤ 0head_SLAM_f_30_0 + head_SLAM_f_30_0 ≤ 0head_SLAM_f_30_0head_SLAM_f_30_0 ≤ 0head_33_post + head_33_post ≤ 0head_33_posthead_33_post ≤ 0head_33_0 + head_33_0 ≤ 0head_33_0head_33_0 ≤ 0head_16_post + head_16_post ≤ 0head_16_posthead_16_post ≤ 0head_16_1 + head_16_1 ≤ 0head_16_1head_16_1 ≤ 0head_16_0 + head_16_0 ≤ 0head_16_0head_16_0 ≤ 0f_202_post + f_202_post ≤ 0f_202_postf_202_post ≤ 0f_202_0 + f_202_0 ≤ 0f_202_0f_202_0 ≤ 0a_309_post + a_309_post ≤ 0a_309_posta_309_post ≤ 0a_309_0 + a_309_0 ≤ 0a_309_0a_309_0 ≤ 0a_279_post + a_279_post ≤ 0a_279_posta_279_post ≤ 0a_279_0 + a_279_0 ≤ 0a_279_0a_279_0 ≤ 0a_253_post + a_253_post ≤ 0a_253_posta_253_post ≤ 0a_253_0 + a_253_0 ≤ 0a_253_0a_253_0 ≤ 0a_222_post + a_222_post ≤ 0a_222_posta_222_post ≤ 0a_222_0 + a_222_0 ≤ 0a_222_0a_222_0 ≤ 0a_174_post + a_174_post ≤ 0a_174_posta_174_post ≤ 0a_174_0 + a_174_0 ≤ 0a_174_0a_174_0 ≤ 0a_139_post + a_139_post ≤ 0a_139_posta_139_post ≤ 0a_139_0 + a_139_0 ≤ 0a_139_0a_139_0 ≤ 0

7 Location Addition

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

20 81 20_var_snapshot: y_26_post + y_26_post ≤ 0y_26_posty_26_post ≤ 0y_26_1 + y_26_1 ≤ 0y_26_1y_26_1 ≤ 0y_26_0 + y_26_0 ≤ 0y_26_0y_26_0 ≤ 0y_21_post + y_21_post ≤ 0y_21_posty_21_post ≤ 0y_21_1 + y_21_1 ≤ 0y_21_1y_21_1 ≤ 0y_21_0 + y_21_0 ≤ 0y_21_0y_21_0 ≤ 0x_SLAM_f_25_post + x_SLAM_f_25_post ≤ 0x_SLAM_f_25_postx_SLAM_f_25_post ≤ 0x_SLAM_f_25_1 + x_SLAM_f_25_1 ≤ 0x_SLAM_f_25_1x_SLAM_f_25_1 ≤ 0x_SLAM_f_25_0 + x_SLAM_f_25_0 ≤ 0x_SLAM_f_25_0x_SLAM_f_25_0 ≤ 0x_SLAM_f_20_post + x_SLAM_f_20_post ≤ 0x_SLAM_f_20_postx_SLAM_f_20_post ≤ 0x_SLAM_f_20_1 + x_SLAM_f_20_1 ≤ 0x_SLAM_f_20_1x_SLAM_f_20_1 ≤ 0x_SLAM_f_20_0 + x_SLAM_f_20_0 ≤ 0x_SLAM_f_20_0x_SLAM_f_20_0 ≤ 0x_27_post + x_27_post ≤ 0x_27_postx_27_post ≤ 0x_27_1 + x_27_1 ≤ 0x_27_1x_27_1 ≤ 0x_27_0 + x_27_0 ≤ 0x_27_0x_27_0 ≤ 0x_22_post + x_22_post ≤ 0x_22_postx_22_post ≤ 0x_22_1 + x_22_1 ≤ 0x_22_1x_22_1 ≤ 0x_22_0 + x_22_0 ≤ 0x_22_0x_22_0 ≤ 0x_207_post + x_207_post ≤ 0x_207_postx_207_post ≤ 0x_207_0 + x_207_0 ≤ 0x_207_0x_207_0 ≤ 0x_154_post + x_154_post ≤ 0x_154_postx_154_post ≤ 0x_154_0 + x_154_0 ≤ 0x_154_0x_154_0 ≤ 0tmp_35_post + tmp_35_post ≤ 0tmp_35_posttmp_35_post ≤ 0tmp_35_0 + tmp_35_0 ≤ 0tmp_35_0tmp_35_0 ≤ 0temp_37_post + temp_37_post ≤ 0temp_37_posttemp_37_post ≤ 0temp_37_0 + temp_37_0 ≤ 0temp_37_0temp_37_0 ≤ 0temp_36_post + temp_36_post ≤ 0temp_36_posttemp_36_post ≤ 0temp_36_0 + temp_36_0 ≤ 0temp_36_0temp_36_0 ≤ 0temp0_32_post + temp0_32_post ≤ 0temp0_32_posttemp0_32_post ≤ 0temp0_32_1 + temp0_32_1 ≤ 0temp0_32_1temp0_32_1 ≤ 0temp0_32_0 + temp0_32_0 ≤ 0temp0_32_0temp0_32_0 ≤ 0temp0_19_0 + temp0_19_0 ≤ 0temp0_19_0temp0_19_0 ≤ 0tail_15_post + tail_15_post ≤ 0tail_15_posttail_15_post ≤ 0tail_15_0 + tail_15_0 ≤ 0tail_15_0tail_15_0 ≤ 0t_23_post + t_23_post ≤ 0t_23_postt_23_post ≤ 0t_23_0 + t_23_0 ≤ 0t_23_0t_23_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_post + result_dot_nondet_sdv_special_RETURN_VALUE_14_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_postresult_dot_nondet_sdv_special_RETURN_VALUE_14_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_2 + result_dot_nondet_sdv_special_RETURN_VALUE_14_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_2result_dot_nondet_sdv_special_RETURN_VALUE_14_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_1result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_0 + result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_0result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_postresult_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_postresult_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_1 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_1 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_1result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_1 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_0 ≤ 0result_11_post + result_11_post ≤ 0result_11_postresult_11_post ≤ 0result_11_2 + result_11_2 ≤ 0result_11_2result_11_2 ≤ 0result_11_1 + result_11_1 ≤ 0result_11_1result_11_1 ≤ 0result_11_0 + result_11_0 ≤ 0result_11_0result_11_0 ≤ 0rcd_71_post + rcd_71_post ≤ 0rcd_71_postrcd_71_post ≤ 0rcd_71_0 + rcd_71_0 ≤ 0rcd_71_0rcd_71_0 ≤ 0rcd_45_post + rcd_45_post ≤ 0rcd_45_postrcd_45_post ≤ 0rcd_45_0 + rcd_45_0 ≤ 0rcd_45_0rcd_45_0 ≤ 0rcd_320_post + rcd_320_post ≤ 0rcd_320_postrcd_320_post ≤ 0rcd_320_0 + rcd_320_0 ≤ 0rcd_320_0rcd_320_0 ≤ 0rcd_308_post + rcd_308_post ≤ 0rcd_308_postrcd_308_post ≤ 0rcd_308_0 + rcd_308_0 ≤ 0rcd_308_0rcd_308_0 ≤ 0rcd_288_post + rcd_288_post ≤ 0rcd_288_postrcd_288_post ≤ 0rcd_288_0 + rcd_288_0 ≤ 0rcd_288_0rcd_288_0 ≤ 0rcd_284_post + rcd_284_post ≤ 0rcd_284_postrcd_284_post ≤ 0rcd_284_0 + rcd_284_0 ≤ 0rcd_284_0rcd_284_0 ≤ 0rcd_220_post + rcd_220_post ≤ 0rcd_220_postrcd_220_post ≤ 0rcd_220_0 + rcd_220_0 ≤ 0rcd_220_0rcd_220_0 ≤ 0rcd_199_post + rcd_199_post ≤ 0rcd_199_postrcd_199_post ≤ 0rcd_199_0 + rcd_199_0 ≤ 0rcd_199_0rcd_199_0 ≤ 0rcd_194_post + rcd_194_post ≤ 0rcd_194_postrcd_194_post ≤ 0rcd_194_0 + rcd_194_0 ≤ 0rcd_194_0rcd_194_0 ≤ 0rcd_193_post + rcd_193_post ≤ 0rcd_193_postrcd_193_post ≤ 0rcd_193_0 + rcd_193_0 ≤ 0rcd_193_0rcd_193_0 ≤ 0rcd_185_post + rcd_185_post ≤ 0rcd_185_postrcd_185_post ≤ 0rcd_185_0 + rcd_185_0 ≤ 0rcd_185_0rcd_185_0 ≤ 0rcd_114_post + rcd_114_post ≤ 0rcd_114_postrcd_114_post ≤ 0rcd_114_0 + rcd_114_0 ≤ 0rcd_114_0rcd_114_0 ≤ 0rcd_106_post + rcd_106_post ≤ 0rcd_106_postrcd_106_post ≤ 0rcd_106_0 + rcd_106_0 ≤ 0rcd_106_0rcd_106_0 ≤ 0r_41_post + r_41_post ≤ 0r_41_postr_41_post ≤ 0r_41_0 + r_41_0 ≤ 0r_41_0r_41_0 ≤ 0r_192_post + r_192_post ≤ 0r_192_postr_192_post ≤ 0r_192_0 + r_192_0 ≤ 0r_192_0r_192_0 ≤ 0r_149_post + r_149_post ≤ 0r_149_postr_149_post ≤ 0r_149_0 + r_149_0 ≤ 0r_149_0r_149_0 ≤ 0nondet_12_post + nondet_12_post ≤ 0nondet_12_postnondet_12_post ≤ 0nondet_12_1 + nondet_12_1 ≤ 0nondet_12_1nondet_12_1 ≤ 0nondet_12_0 + nondet_12_0 ≤ 0nondet_12_0nondet_12_0 ≤ 0length_29_post + length_29_post ≤ 0length_29_postlength_29_post ≤ 0length_29_0 + length_29_0 ≤ 0length_29_0length_29_0 ≤ 0len_221_post + len_221_post ≤ 0len_221_postlen_221_post ≤ 0len_221_0 + len_221_0 ≤ 0len_221_0len_221_0 ≤ 0len_159_post + len_159_post ≤ 0len_159_postlen_159_post ≤ 0len_159_0 + len_159_0 ≤ 0len_159_0len_159_0 ≤ 0i_31_post + i_31_post ≤ 0i_31_posti_31_post ≤ 0i_31_0 + i_31_0 ≤ 0i_31_0i_31_0 ≤ 0i_198_post + i_198_post ≤ 0i_198_posti_198_post ≤ 0i_198_0 + i_198_0 ≤ 0i_198_0i_198_0 ≤ 0i_130_post + i_130_post ≤ 0i_130_posti_130_post ≤ 0i_130_0 + i_130_0 ≤ 0i_130_0i_130_0 ≤ 0i_112_post + i_112_post ≤ 0i_112_posti_112_post ≤ 0i_112_0 + i_112_0 ≤ 0i_112_0i_112_0 ≤ 0head_SLAM_f_30_post + head_SLAM_f_30_post ≤ 0head_SLAM_f_30_posthead_SLAM_f_30_post ≤ 0head_SLAM_f_30_0 + head_SLAM_f_30_0 ≤ 0head_SLAM_f_30_0head_SLAM_f_30_0 ≤ 0head_33_post + head_33_post ≤ 0head_33_posthead_33_post ≤ 0head_33_0 + head_33_0 ≤ 0head_33_0head_33_0 ≤ 0head_16_post + head_16_post ≤ 0head_16_posthead_16_post ≤ 0head_16_1 + head_16_1 ≤ 0head_16_1head_16_1 ≤ 0head_16_0 + head_16_0 ≤ 0head_16_0head_16_0 ≤ 0f_202_post + f_202_post ≤ 0f_202_postf_202_post ≤ 0f_202_0 + f_202_0 ≤ 0f_202_0f_202_0 ≤ 0a_309_post + a_309_post ≤ 0a_309_posta_309_post ≤ 0a_309_0 + a_309_0 ≤ 0a_309_0a_309_0 ≤ 0a_279_post + a_279_post ≤ 0a_279_posta_279_post ≤ 0a_279_0 + a_279_0 ≤ 0a_279_0a_279_0 ≤ 0a_253_post + a_253_post ≤ 0a_253_posta_253_post ≤ 0a_253_0 + a_253_0 ≤ 0a_253_0a_253_0 ≤ 0a_222_post + a_222_post ≤ 0a_222_posta_222_post ≤ 0a_222_0 + a_222_0 ≤ 0a_222_0a_222_0 ≤ 0a_174_post + a_174_post ≤ 0a_174_posta_174_post ≤ 0a_174_0 + a_174_0 ≤ 0a_174_0a_174_0 ≤ 0a_139_post + a_139_post ≤ 0a_139_posta_139_post ≤ 0a_139_0 + a_139_0 ≤ 0a_139_0a_139_0 ≤ 0

8 Location Addition

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

25* 90 25: y_26_post + y_26_post ≤ 0y_26_posty_26_post ≤ 0y_26_1 + y_26_1 ≤ 0y_26_1y_26_1 ≤ 0y_26_0 + y_26_0 ≤ 0y_26_0y_26_0 ≤ 0y_21_post + y_21_post ≤ 0y_21_posty_21_post ≤ 0y_21_1 + y_21_1 ≤ 0y_21_1y_21_1 ≤ 0y_21_0 + y_21_0 ≤ 0y_21_0y_21_0 ≤ 0x_SLAM_f_25_post + x_SLAM_f_25_post ≤ 0x_SLAM_f_25_postx_SLAM_f_25_post ≤ 0x_SLAM_f_25_1 + x_SLAM_f_25_1 ≤ 0x_SLAM_f_25_1x_SLAM_f_25_1 ≤ 0x_SLAM_f_25_0 + x_SLAM_f_25_0 ≤ 0x_SLAM_f_25_0x_SLAM_f_25_0 ≤ 0x_SLAM_f_20_post + x_SLAM_f_20_post ≤ 0x_SLAM_f_20_postx_SLAM_f_20_post ≤ 0x_SLAM_f_20_1 + x_SLAM_f_20_1 ≤ 0x_SLAM_f_20_1x_SLAM_f_20_1 ≤ 0x_SLAM_f_20_0 + x_SLAM_f_20_0 ≤ 0x_SLAM_f_20_0x_SLAM_f_20_0 ≤ 0x_27_post + x_27_post ≤ 0x_27_postx_27_post ≤ 0x_27_1 + x_27_1 ≤ 0x_27_1x_27_1 ≤ 0x_27_0 + x_27_0 ≤ 0x_27_0x_27_0 ≤ 0x_22_post + x_22_post ≤ 0x_22_postx_22_post ≤ 0x_22_1 + x_22_1 ≤ 0x_22_1x_22_1 ≤ 0x_22_0 + x_22_0 ≤ 0x_22_0x_22_0 ≤ 0x_207_post + x_207_post ≤ 0x_207_postx_207_post ≤ 0x_207_0 + x_207_0 ≤ 0x_207_0x_207_0 ≤ 0x_154_post + x_154_post ≤ 0x_154_postx_154_post ≤ 0x_154_0 + x_154_0 ≤ 0x_154_0x_154_0 ≤ 0tmp_35_post + tmp_35_post ≤ 0tmp_35_posttmp_35_post ≤ 0tmp_35_0 + tmp_35_0 ≤ 0tmp_35_0tmp_35_0 ≤ 0temp_37_post + temp_37_post ≤ 0temp_37_posttemp_37_post ≤ 0temp_37_0 + temp_37_0 ≤ 0temp_37_0temp_37_0 ≤ 0temp_36_post + temp_36_post ≤ 0temp_36_posttemp_36_post ≤ 0temp_36_0 + temp_36_0 ≤ 0temp_36_0temp_36_0 ≤ 0temp0_32_post + temp0_32_post ≤ 0temp0_32_posttemp0_32_post ≤ 0temp0_32_1 + temp0_32_1 ≤ 0temp0_32_1temp0_32_1 ≤ 0temp0_32_0 + temp0_32_0 ≤ 0temp0_32_0temp0_32_0 ≤ 0temp0_19_0 + temp0_19_0 ≤ 0temp0_19_0temp0_19_0 ≤ 0tail_15_post + tail_15_post ≤ 0tail_15_posttail_15_post ≤ 0tail_15_0 + tail_15_0 ≤ 0tail_15_0tail_15_0 ≤ 0t_23_post + t_23_post ≤ 0t_23_postt_23_post ≤ 0t_23_0 + t_23_0 ≤ 0t_23_0t_23_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_post + result_dot_nondet_sdv_special_RETURN_VALUE_14_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_postresult_dot_nondet_sdv_special_RETURN_VALUE_14_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_2 + result_dot_nondet_sdv_special_RETURN_VALUE_14_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_2result_dot_nondet_sdv_special_RETURN_VALUE_14_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_1result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_0 + result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_0result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_postresult_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_postresult_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_1 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_1 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_1result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_1 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_0 ≤ 0result_11_post + result_11_post ≤ 0result_11_postresult_11_post ≤ 0result_11_2 + result_11_2 ≤ 0result_11_2result_11_2 ≤ 0result_11_1 + result_11_1 ≤ 0result_11_1result_11_1 ≤ 0result_11_0 + result_11_0 ≤ 0result_11_0result_11_0 ≤ 0rcd_71_post + rcd_71_post ≤ 0rcd_71_postrcd_71_post ≤ 0rcd_71_0 + rcd_71_0 ≤ 0rcd_71_0rcd_71_0 ≤ 0rcd_45_post + rcd_45_post ≤ 0rcd_45_postrcd_45_post ≤ 0rcd_45_0 + rcd_45_0 ≤ 0rcd_45_0rcd_45_0 ≤ 0rcd_320_post + rcd_320_post ≤ 0rcd_320_postrcd_320_post ≤ 0rcd_320_0 + rcd_320_0 ≤ 0rcd_320_0rcd_320_0 ≤ 0rcd_308_post + rcd_308_post ≤ 0rcd_308_postrcd_308_post ≤ 0rcd_308_0 + rcd_308_0 ≤ 0rcd_308_0rcd_308_0 ≤ 0rcd_288_post + rcd_288_post ≤ 0rcd_288_postrcd_288_post ≤ 0rcd_288_0 + rcd_288_0 ≤ 0rcd_288_0rcd_288_0 ≤ 0rcd_284_post + rcd_284_post ≤ 0rcd_284_postrcd_284_post ≤ 0rcd_284_0 + rcd_284_0 ≤ 0rcd_284_0rcd_284_0 ≤ 0rcd_220_post + rcd_220_post ≤ 0rcd_220_postrcd_220_post ≤ 0rcd_220_0 + rcd_220_0 ≤ 0rcd_220_0rcd_220_0 ≤ 0rcd_199_post + rcd_199_post ≤ 0rcd_199_postrcd_199_post ≤ 0rcd_199_0 + rcd_199_0 ≤ 0rcd_199_0rcd_199_0 ≤ 0rcd_194_post + rcd_194_post ≤ 0rcd_194_postrcd_194_post ≤ 0rcd_194_0 + rcd_194_0 ≤ 0rcd_194_0rcd_194_0 ≤ 0rcd_193_post + rcd_193_post ≤ 0rcd_193_postrcd_193_post ≤ 0rcd_193_0 + rcd_193_0 ≤ 0rcd_193_0rcd_193_0 ≤ 0rcd_185_post + rcd_185_post ≤ 0rcd_185_postrcd_185_post ≤ 0rcd_185_0 + rcd_185_0 ≤ 0rcd_185_0rcd_185_0 ≤ 0rcd_114_post + rcd_114_post ≤ 0rcd_114_postrcd_114_post ≤ 0rcd_114_0 + rcd_114_0 ≤ 0rcd_114_0rcd_114_0 ≤ 0rcd_106_post + rcd_106_post ≤ 0rcd_106_postrcd_106_post ≤ 0rcd_106_0 + rcd_106_0 ≤ 0rcd_106_0rcd_106_0 ≤ 0r_41_post + r_41_post ≤ 0r_41_postr_41_post ≤ 0r_41_0 + r_41_0 ≤ 0r_41_0r_41_0 ≤ 0r_192_post + r_192_post ≤ 0r_192_postr_192_post ≤ 0r_192_0 + r_192_0 ≤ 0r_192_0r_192_0 ≤ 0r_149_post + r_149_post ≤ 0r_149_postr_149_post ≤ 0r_149_0 + r_149_0 ≤ 0r_149_0r_149_0 ≤ 0nondet_12_post + nondet_12_post ≤ 0nondet_12_postnondet_12_post ≤ 0nondet_12_1 + nondet_12_1 ≤ 0nondet_12_1nondet_12_1 ≤ 0nondet_12_0 + nondet_12_0 ≤ 0nondet_12_0nondet_12_0 ≤ 0length_29_post + length_29_post ≤ 0length_29_postlength_29_post ≤ 0length_29_0 + length_29_0 ≤ 0length_29_0length_29_0 ≤ 0len_221_post + len_221_post ≤ 0len_221_postlen_221_post ≤ 0len_221_0 + len_221_0 ≤ 0len_221_0len_221_0 ≤ 0len_159_post + len_159_post ≤ 0len_159_postlen_159_post ≤ 0len_159_0 + len_159_0 ≤ 0len_159_0len_159_0 ≤ 0i_31_post + i_31_post ≤ 0i_31_posti_31_post ≤ 0i_31_0 + i_31_0 ≤ 0i_31_0i_31_0 ≤ 0i_198_post + i_198_post ≤ 0i_198_posti_198_post ≤ 0i_198_0 + i_198_0 ≤ 0i_198_0i_198_0 ≤ 0i_130_post + i_130_post ≤ 0i_130_posti_130_post ≤ 0i_130_0 + i_130_0 ≤ 0i_130_0i_130_0 ≤ 0i_112_post + i_112_post ≤ 0i_112_posti_112_post ≤ 0i_112_0 + i_112_0 ≤ 0i_112_0i_112_0 ≤ 0head_SLAM_f_30_post + head_SLAM_f_30_post ≤ 0head_SLAM_f_30_posthead_SLAM_f_30_post ≤ 0head_SLAM_f_30_0 + head_SLAM_f_30_0 ≤ 0head_SLAM_f_30_0head_SLAM_f_30_0 ≤ 0head_33_post + head_33_post ≤ 0head_33_posthead_33_post ≤ 0head_33_0 + head_33_0 ≤ 0head_33_0head_33_0 ≤ 0head_16_post + head_16_post ≤ 0head_16_posthead_16_post ≤ 0head_16_1 + head_16_1 ≤ 0head_16_1head_16_1 ≤ 0head_16_0 + head_16_0 ≤ 0head_16_0head_16_0 ≤ 0f_202_post + f_202_post ≤ 0f_202_postf_202_post ≤ 0f_202_0 + f_202_0 ≤ 0f_202_0f_202_0 ≤ 0a_309_post + a_309_post ≤ 0a_309_posta_309_post ≤ 0a_309_0 + a_309_0 ≤ 0a_309_0a_309_0 ≤ 0a_279_post + a_279_post ≤ 0a_279_posta_279_post ≤ 0a_279_0 + a_279_0 ≤ 0a_279_0a_279_0 ≤ 0a_253_post + a_253_post ≤ 0a_253_posta_253_post ≤ 0a_253_0 + a_253_0 ≤ 0a_253_0a_253_0 ≤ 0a_222_post + a_222_post ≤ 0a_222_posta_222_post ≤ 0a_222_0 + a_222_0 ≤ 0a_222_0a_222_0 ≤ 0a_174_post + a_174_post ≤ 0a_174_posta_174_post ≤ 0a_174_0 + a_174_0 ≤ 0a_174_0a_174_0 ≤ 0a_139_post + a_139_post ≤ 0a_139_posta_139_post ≤ 0a_139_0 + a_139_0 ≤ 0a_139_0a_139_0 ≤ 0

9 Location Addition

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

25 88 25_var_snapshot: y_26_post + y_26_post ≤ 0y_26_posty_26_post ≤ 0y_26_1 + y_26_1 ≤ 0y_26_1y_26_1 ≤ 0y_26_0 + y_26_0 ≤ 0y_26_0y_26_0 ≤ 0y_21_post + y_21_post ≤ 0y_21_posty_21_post ≤ 0y_21_1 + y_21_1 ≤ 0y_21_1y_21_1 ≤ 0y_21_0 + y_21_0 ≤ 0y_21_0y_21_0 ≤ 0x_SLAM_f_25_post + x_SLAM_f_25_post ≤ 0x_SLAM_f_25_postx_SLAM_f_25_post ≤ 0x_SLAM_f_25_1 + x_SLAM_f_25_1 ≤ 0x_SLAM_f_25_1x_SLAM_f_25_1 ≤ 0x_SLAM_f_25_0 + x_SLAM_f_25_0 ≤ 0x_SLAM_f_25_0x_SLAM_f_25_0 ≤ 0x_SLAM_f_20_post + x_SLAM_f_20_post ≤ 0x_SLAM_f_20_postx_SLAM_f_20_post ≤ 0x_SLAM_f_20_1 + x_SLAM_f_20_1 ≤ 0x_SLAM_f_20_1x_SLAM_f_20_1 ≤ 0x_SLAM_f_20_0 + x_SLAM_f_20_0 ≤ 0x_SLAM_f_20_0x_SLAM_f_20_0 ≤ 0x_27_post + x_27_post ≤ 0x_27_postx_27_post ≤ 0x_27_1 + x_27_1 ≤ 0x_27_1x_27_1 ≤ 0x_27_0 + x_27_0 ≤ 0x_27_0x_27_0 ≤ 0x_22_post + x_22_post ≤ 0x_22_postx_22_post ≤ 0x_22_1 + x_22_1 ≤ 0x_22_1x_22_1 ≤ 0x_22_0 + x_22_0 ≤ 0x_22_0x_22_0 ≤ 0x_207_post + x_207_post ≤ 0x_207_postx_207_post ≤ 0x_207_0 + x_207_0 ≤ 0x_207_0x_207_0 ≤ 0x_154_post + x_154_post ≤ 0x_154_postx_154_post ≤ 0x_154_0 + x_154_0 ≤ 0x_154_0x_154_0 ≤ 0tmp_35_post + tmp_35_post ≤ 0tmp_35_posttmp_35_post ≤ 0tmp_35_0 + tmp_35_0 ≤ 0tmp_35_0tmp_35_0 ≤ 0temp_37_post + temp_37_post ≤ 0temp_37_posttemp_37_post ≤ 0temp_37_0 + temp_37_0 ≤ 0temp_37_0temp_37_0 ≤ 0temp_36_post + temp_36_post ≤ 0temp_36_posttemp_36_post ≤ 0temp_36_0 + temp_36_0 ≤ 0temp_36_0temp_36_0 ≤ 0temp0_32_post + temp0_32_post ≤ 0temp0_32_posttemp0_32_post ≤ 0temp0_32_1 + temp0_32_1 ≤ 0temp0_32_1temp0_32_1 ≤ 0temp0_32_0 + temp0_32_0 ≤ 0temp0_32_0temp0_32_0 ≤ 0temp0_19_0 + temp0_19_0 ≤ 0temp0_19_0temp0_19_0 ≤ 0tail_15_post + tail_15_post ≤ 0tail_15_posttail_15_post ≤ 0tail_15_0 + tail_15_0 ≤ 0tail_15_0tail_15_0 ≤ 0t_23_post + t_23_post ≤ 0t_23_postt_23_post ≤ 0t_23_0 + t_23_0 ≤ 0t_23_0t_23_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_post + result_dot_nondet_sdv_special_RETURN_VALUE_14_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_postresult_dot_nondet_sdv_special_RETURN_VALUE_14_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_2 + result_dot_nondet_sdv_special_RETURN_VALUE_14_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_2result_dot_nondet_sdv_special_RETURN_VALUE_14_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_1 + result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_1result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_0 + result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_14_0result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_postresult_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_34_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_postresult_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_1 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_1 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_1result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_1 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_0 ≤ 0result_11_post + result_11_post ≤ 0result_11_postresult_11_post ≤ 0result_11_2 + result_11_2 ≤ 0result_11_2result_11_2 ≤ 0result_11_1 + result_11_1 ≤ 0result_11_1result_11_1 ≤ 0result_11_0 + result_11_0 ≤ 0result_11_0result_11_0 ≤ 0rcd_71_post + rcd_71_post ≤ 0rcd_71_postrcd_71_post ≤ 0rcd_71_0 + rcd_71_0 ≤ 0rcd_71_0rcd_71_0 ≤ 0rcd_45_post + rcd_45_post ≤ 0rcd_45_postrcd_45_post ≤ 0rcd_45_0 + rcd_45_0 ≤ 0rcd_45_0rcd_45_0 ≤ 0rcd_320_post + rcd_320_post ≤ 0rcd_320_postrcd_320_post ≤ 0rcd_320_0 + rcd_320_0 ≤ 0rcd_320_0rcd_320_0 ≤ 0rcd_308_post + rcd_308_post ≤ 0rcd_308_postrcd_308_post ≤ 0rcd_308_0 + rcd_308_0 ≤ 0rcd_308_0rcd_308_0 ≤ 0rcd_288_post + rcd_288_post ≤ 0rcd_288_postrcd_288_post ≤ 0rcd_288_0 + rcd_288_0 ≤ 0rcd_288_0rcd_288_0 ≤ 0rcd_284_post + rcd_284_post ≤ 0rcd_284_postrcd_284_post ≤ 0rcd_284_0 + rcd_284_0 ≤ 0rcd_284_0rcd_284_0 ≤ 0rcd_220_post + rcd_220_post ≤ 0rcd_220_postrcd_220_post ≤ 0rcd_220_0 + rcd_220_0 ≤ 0rcd_220_0rcd_220_0 ≤ 0rcd_199_post + rcd_199_post ≤ 0rcd_199_postrcd_199_post ≤ 0rcd_199_0 + rcd_199_0 ≤ 0rcd_199_0rcd_199_0 ≤ 0rcd_194_post + rcd_194_post ≤ 0rcd_194_postrcd_194_post ≤ 0rcd_194_0 + rcd_194_0 ≤ 0rcd_194_0rcd_194_0 ≤ 0rcd_193_post + rcd_193_post ≤ 0rcd_193_postrcd_193_post ≤ 0rcd_193_0 + rcd_193_0 ≤ 0rcd_193_0rcd_193_0 ≤ 0rcd_185_post + rcd_185_post ≤ 0rcd_185_postrcd_185_post ≤ 0rcd_185_0 + rcd_185_0 ≤ 0rcd_185_0rcd_185_0 ≤ 0rcd_114_post + rcd_114_post ≤ 0rcd_114_postrcd_114_post ≤ 0rcd_114_0 + rcd_114_0 ≤ 0rcd_114_0rcd_114_0 ≤ 0rcd_106_post + rcd_106_post ≤ 0rcd_106_postrcd_106_post ≤ 0rcd_106_0 + rcd_106_0 ≤ 0rcd_106_0rcd_106_0 ≤ 0r_41_post + r_41_post ≤ 0r_41_postr_41_post ≤ 0r_41_0 + r_41_0 ≤ 0r_41_0r_41_0 ≤ 0r_192_post + r_192_post ≤ 0r_192_postr_192_post ≤ 0r_192_0 + r_192_0 ≤ 0r_192_0r_192_0 ≤ 0r_149_post + r_149_post ≤ 0r_149_postr_149_post ≤ 0r_149_0 + r_149_0 ≤ 0r_149_0r_149_0 ≤ 0nondet_12_post + nondet_12_post ≤ 0nondet_12_postnondet_12_post ≤ 0nondet_12_1 + nondet_12_1 ≤ 0nondet_12_1nondet_12_1 ≤ 0nondet_12_0 + nondet_12_0 ≤ 0nondet_12_0nondet_12_0 ≤ 0length_29_post + length_29_post ≤ 0length_29_postlength_29_post ≤ 0length_29_0 + length_29_0 ≤ 0length_29_0length_29_0 ≤ 0len_221_post + len_221_post ≤ 0len_221_postlen_221_post ≤ 0len_221_0 + len_221_0 ≤ 0len_221_0len_221_0 ≤ 0len_159_post + len_159_post ≤ 0len_159_postlen_159_post ≤ 0len_159_0 + len_159_0 ≤ 0len_159_0len_159_0 ≤ 0i_31_post + i_31_post ≤ 0i_31_posti_31_post ≤ 0i_31_0 + i_31_0 ≤ 0i_31_0i_31_0 ≤ 0i_198_post + i_198_post ≤ 0i_198_posti_198_post ≤ 0i_198_0 + i_198_0 ≤ 0i_198_0i_198_0 ≤ 0i_130_post + i_130_post ≤ 0i_130_posti_130_post ≤ 0i_130_0 + i_130_0 ≤ 0i_130_0i_130_0 ≤ 0i_112_post + i_112_post ≤ 0i_112_posti_112_post ≤ 0i_112_0 + i_112_0 ≤ 0i_112_0i_112_0 ≤ 0head_SLAM_f_30_post + head_SLAM_f_30_post ≤ 0head_SLAM_f_30_posthead_SLAM_f_30_post ≤ 0head_SLAM_f_30_0 + head_SLAM_f_30_0 ≤ 0head_SLAM_f_30_0head_SLAM_f_30_0 ≤ 0head_33_post + head_33_post ≤ 0head_33_posthead_33_post ≤ 0head_33_0 + head_33_0 ≤ 0head_33_0head_33_0 ≤ 0head_16_post + head_16_post ≤ 0head_16_posthead_16_post ≤ 0head_16_1 + head_16_1 ≤ 0head_16_1head_16_1 ≤ 0head_16_0 + head_16_0 ≤ 0head_16_0head_16_0 ≤ 0f_202_post + f_202_post ≤ 0f_202_postf_202_post ≤ 0f_202_0 + f_202_0 ≤ 0f_202_0f_202_0 ≤ 0a_309_post + a_309_post ≤ 0a_309_posta_309_post ≤ 0a_309_0 + a_309_0 ≤ 0a_309_0a_309_0 ≤ 0a_279_post + a_279_post ≤ 0a_279_posta_279_post ≤ 0a_279_0 + a_279_0 ≤ 0a_279_0a_279_0 ≤ 0a_253_post + a_253_post ≤ 0a_253_posta_253_post ≤ 0a_253_0 + a_253_0 ≤ 0a_253_0a_253_0 ≤ 0a_222_post + a_222_post ≤ 0a_222_posta_222_post ≤ 0a_222_0 + a_222_0 ≤ 0a_222_0a_222_0 ≤ 0a_174_post + a_174_post ≤ 0a_174_posta_174_post ≤ 0a_174_0 + a_174_0 ≤ 0a_174_0a_174_0 ≤ 0a_139_post + a_139_post ≤ 0a_139_posta_139_post ≤ 0a_139_0 + a_139_0 ≤ 0a_139_0a_139_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 { 25, 26, 27, 28, 29, 30, 31, 32, 25_var_snapshot, 25* }.

10.1.1 Transition Removal

We remove transitions 27, 28, 29 using the following ranking functions, which are bounded by −6.

25: −2 + 10⋅a_279_0
26: −4 + 10⋅a_279_0
27: −5 + 10⋅a_279_0
28: 4 + 10⋅a_309_0
29: 3 + 10⋅a_309_0
30: 2 + 10⋅a_309_0
31: 1 + 10⋅a_309_0
32: 10⋅a_279_0
25_var_snapshot: −3 + 10⋅a_279_0
25*: −1 + 10⋅a_279_0

10.1.2 Transition Removal

We remove transitions 88, 90, 30, 31, 32, 33, 34 using the following ranking functions, which are bounded by −3.

25: −2
26: 0
27: 0
28: 4
29: 3
30: 2
31: 1
32: 0
25_var_snapshot: −3
25*: −1

10.1.3 Splitting Cut-Point Transitions

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

10.1.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 87.

10.1.3.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 { 5, 52, 53, 54, 55, 56, 57, 5_var_snapshot, 5* }.

10.2.1 Transition Removal

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

5: −2 + 9⋅a_174_0
52: −4 + 9⋅a_174_0
53: −5 + 9⋅a_174_0
54: 3 + 9⋅a_222_0
55: 2 + 9⋅a_222_0
56: 1 + 9⋅a_222_0
57: 9⋅a_174_0
5_var_snapshot: −3 + 9⋅a_174_0
5*: −1 + 9⋅a_174_0

10.2.2 Transition Removal

We remove transitions 74, 76, 56, 57, 59, 60, 61, 62 using the following ranking functions, which are bounded by −2.

5: 1
52: −1
53: −2
54: 1 + 4⋅len_221_0 + len_221_post
55: 4⋅len_221_0 + len_221_post
56: 4⋅len_221_0
57: 3
5_var_snapshot: 0
5*: 2

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

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 { 20, 23, 20_var_snapshot, 20* }.

10.3.1 Transition Removal

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

20: −2 − 4⋅i_31_0 + 4⋅length_29_0
23: −4⋅i_31_0 + 4⋅length_29_0
20_var_snapshot: −3 − 4⋅i_31_0 + 4⋅length_29_0
20*: −1 − 4⋅i_31_0 + 4⋅length_29_0

10.3.2 Transition Removal

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

20: 0
23: 2⋅length_29_0
20_var_snapshot: −1
20*: length_29_0

10.3.3 Transition Removal

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

20: 0
23: 0
20_var_snapshot: 0
20*: −1

10.3.4 Splitting Cut-Point Transitions

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

10.3.4.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 80.

10.3.4.1.1 Splitting Cut-Point Transitions

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

Tool configuration

T2Cert