LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Invariant Updates

The following invariants are asserted.

0: 2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0a_147_0 ≤ 0y_19_post ≤ 0y_19_post ≤ 0ct_17_0 ≤ 0ct_17_0 ≤ 0y_19_0 ≤ 0y_19_0 ≤ 0
1: TRUE
2: a_147_0 ≤ 0y_19_post ≤ 0y_19_post ≤ 0y_19_0 ≤ 0y_19_0 ≤ 0a_237_0 ≤ 0
3: a_147_0 ≤ 0y_19_post ≤ 0y_19_post ≤ 0y_19_0 ≤ 0y_19_0 ≤ 0a_237_0 ≤ 0
4: a_147_0 ≤ 0y_19_post ≤ 0y_19_post ≤ 0ct_17_0 ≤ 0ct_17_0 ≤ 0y_19_0 ≤ 0y_19_0 ≤ 0a_237_0 ≤ 0
5: a_147_0 ≤ 0y_19_post ≤ 0y_19_post ≤ 0ct_17_0 ≤ 0ct_17_0 ≤ 0y_19_0 ≤ 0y_19_0 ≤ 0a_237_0 ≤ 0
6: a_147_0 ≤ 0y_19_post ≤ 0y_19_post ≤ 0ct_17_0 ≤ 0ct_17_0 ≤ 0y_19_0 ≤ 0y_19_0 ≤ 0a_237_0 ≤ 0
7: a_147_0 ≤ 0y_19_post ≤ 0y_19_post ≤ 0ct_17_0 ≤ 0ct_17_0 ≤ 0y_19_0 ≤ 0y_19_0 ≤ 0a_237_0 ≤ 0
8: 2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0a_147_0 ≤ 0y_19_post ≤ 0y_19_post ≤ 0ct_17_0 ≤ 0ct_17_0 ≤ 0y_19_0 ≤ 0y_19_0 ≤ 0
18: 2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0len_132_0 ≤ 0a_147_0 ≤ 0ct_17_post ≤ 0ct_17_post ≤ 0y_19_post ≤ 0y_19_post ≤ 0ct_17_0 ≤ 0ct_17_0 ≤ 0y_19_0 ≤ 0y_19_0 ≤ 0
19: len_132_0 ≤ 0a_147_0 ≤ 0y_19_post ≤ 0y_19_post ≤ 0y_19_0 ≤ 0y_19_0 ≤ 0
20: len_132_0 ≤ 0a_147_0 ≤ 0y_19_post ≤ 0y_19_post ≤ 0y_19_0 ≤ 0y_19_0 ≤ 0
21: len_132_0 ≤ 0a_147_0 ≤ 0y_19_post ≤ 0y_19_post ≤ 0ct_17_0 ≤ 0ct_17_0 ≤ 0y_19_0 ≤ 0y_19_0 ≤ 0
22: len_132_0 ≤ 0a_147_0 ≤ 0y_19_post ≤ 0y_19_post ≤ 0ct_17_0 ≤ 0ct_17_0 ≤ 0y_19_0 ≤ 0y_19_0 ≤ 0
23: len_132_0 ≤ 0a_147_0 ≤ 0y_19_post ≤ 0y_19_post ≤ 0ct_17_0 ≤ 0ct_17_0 ≤ 0y_19_0 ≤ 0y_19_0 ≤ 0
24: len_132_0 ≤ 0a_147_0 ≤ 0y_19_post ≤ 0y_19_post ≤ 0ct_17_0 ≤ 0ct_17_0 ≤ 0y_19_0 ≤ 0y_19_0 ≤ 0
25: −1 + i_30_post ≤ 01 − i_30_post ≤ 0−1 + i_30_0 ≤ 01 − i_30_0 ≤ 01 − length_29_0 ≤ 0
26: −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 01 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0
27: −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 01 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0
28: −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 01 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0−1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 01 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0head_27_0 ≤ 0head_27_0 ≤ 0
29: −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 01 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0−1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 01 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0head_27_0 ≤ 0head_27_0 ≤ 0
30: −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 01 − result_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0−1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 01 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0−1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 01 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0ct_17_post ≤ 0ct_17_post ≤ 0y_19_post ≤ 0y_19_post ≤ 0ct_17_0 ≤ 0ct_17_0 ≤ 0y_19_0 ≤ 0y_19_0 ≤ 0
31: −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 01 − result_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0−1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 01 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0−1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 01 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0ct_17_post ≤ 0ct_17_post ≤ 0y_19_post ≤ 0y_19_post ≤ 0ct_17_0 ≤ 0ct_17_0 ≤ 0y_19_0 ≤ 0y_19_0 ≤ 0
32: −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 01 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0y_19_post ≤ 0y_19_post ≤ 0y_19_0 ≤ 0y_19_0 ≤ 0
33: −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 01 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0y_19_post ≤ 0y_19_post ≤ 0y_19_0 ≤ 0y_19_0 ≤ 0
34: −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 01 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0−1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 01 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0y_19_post ≤ 0y_19_post ≤ 0ct_17_0 ≤ 0ct_17_0 ≤ 0x_20_0 ≤ 0x_20_0 ≤ 0y_19_0 ≤ 0y_19_0 ≤ 0
35: −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 01 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0−1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 01 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0y_19_post ≤ 0y_19_post ≤ 0ct_17_0 ≤ 0ct_17_0 ≤ 0x_20_0 ≤ 0x_20_0 ≤ 0y_19_0 ≤ 0y_19_0 ≤ 0
36: −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 01 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0−1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 01 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0y_19_post ≤ 0y_19_post ≤ 0ct_17_0 ≤ 0ct_17_0 ≤ 0x_20_0 ≤ 0x_20_0 ≤ 0y_19_0 ≤ 0y_19_0 ≤ 0
37: −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 01 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0−1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 01 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0
38: 2 − length_29_0 ≤ 0
39: TRUE
40: head_32_post ≤ 0head_32_post ≤ 0i_30_post ≤ 0i_30_post ≤ 0head_32_0 ≤ 0head_32_0 ≤ 0i_30_0 ≤ 0i_30_0 ≤ 0
41: 2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0
42: len_132_0 ≤ 0a_147_0 ≤ 0ct_17_post ≤ 0ct_17_post ≤ 0y_19_post ≤ 0y_19_post ≤ 0ct_17_0 ≤ 0ct_17_0 ≤ 0y_19_0 ≤ 0y_19_0 ≤ 0
43: len_132_0 ≤ 0a_147_0 ≤ 0ct_17_post ≤ 0ct_17_post ≤ 0y_19_post ≤ 0y_19_post ≤ 0ct_17_0 ≤ 0ct_17_0 ≤ 0y_19_0 ≤ 0y_19_0 ≤ 0
44: len_132_0 ≤ 0a_147_0 ≤ 0
45: len_132_0 ≤ 0a_147_0 ≤ 0
46: len_132_0 ≤ 0a_147_0 ≤ 01 − len_183_post ≤ 01 − len_183_0 ≤ 0
47: len_132_0 ≤ 0a_147_0 ≤ 01 − len_183_post ≤ 01 − len_183_0 ≤ 0
48: len_132_0 ≤ 0a_147_0 ≤ 01 − len_183_post ≤ 01 − len_183_0 ≤ 0
49: 2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 01 − len_183_post ≤ 01 − len_183_0 ≤ 0
63: len_132_0 ≤ 0len_132_0 ≤ 0
64: len_132_0 ≤ 0len_132_0 ≤ 0
65: 2 − length_29_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:
0 73 0: y_19_post + y_19_post ≤ 0y_19_posty_19_post ≤ 0y_19_2 + y_19_2 ≤ 0y_19_2y_19_2 ≤ 0y_19_1 + y_19_1 ≤ 0y_19_1y_19_1 ≤ 0y_19_0 + y_19_0 ≤ 0y_19_0y_19_0 ≤ 0x_SLAM_f_18_post + x_SLAM_f_18_post ≤ 0x_SLAM_f_18_postx_SLAM_f_18_post ≤ 0x_SLAM_f_18_2 + x_SLAM_f_18_2 ≤ 0x_SLAM_f_18_2x_SLAM_f_18_2 ≤ 0x_SLAM_f_18_1 + x_SLAM_f_18_1 ≤ 0x_SLAM_f_18_1x_SLAM_f_18_1 ≤ 0x_SLAM_f_18_0 + x_SLAM_f_18_0 ≤ 0x_SLAM_f_18_0x_SLAM_f_18_0 ≤ 0x_20_post + x_20_post ≤ 0x_20_postx_20_post ≤ 0x_20_2 + x_20_2 ≤ 0x_20_2x_20_2 ≤ 0x_20_1 + x_20_1 ≤ 0x_20_1x_20_1 ≤ 0x_20_0 + x_20_0 ≤ 0x_20_0x_20_0 ≤ 0x_16_post + x_16_post ≤ 0x_16_postx_16_post ≤ 0x_16_1 + x_16_1 ≤ 0x_16_1x_16_1 ≤ 0x_16_0 + x_16_0 ≤ 0x_16_0x_16_0 ≤ 0tmp_34_post + tmp_34_post ≤ 0tmp_34_posttmp_34_post ≤ 0tmp_34_0 + tmp_34_0 ≤ 0tmp_34_0tmp_34_0 ≤ 0temp_35_post + temp_35_post ≤ 0temp_35_posttemp_35_post ≤ 0temp_35_0 + temp_35_0 ≤ 0temp_35_0temp_35_0 ≤ 0temp0_31_post + temp0_31_post ≤ 0temp0_31_posttemp0_31_post ≤ 0temp0_31_1 + temp0_31_1 ≤ 0temp0_31_1temp0_31_1 ≤ 0temp0_31_0 + temp0_31_0 ≤ 0temp0_31_0temp0_31_0 ≤ 0temp0_15_0 + temp0_15_0 ≤ 0temp0_15_0temp0_15_0 ≤ 0t_23_post + t_23_post ≤ 0t_23_postt_23_post ≤ 0t_23_1 + t_23_1 ≤ 0t_23_1t_23_1 ≤ 0t_23_0 + t_23_0 ≤ 0t_23_0t_23_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_post + result_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_postresult_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_2 + result_dot_nondet_sdv_special_RETURN_VALUE_13_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_2result_dot_nondet_sdv_special_RETURN_VALUE_13_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_1result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_0 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_0result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_postresult_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_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_88_post + rcd_88_post ≤ 0rcd_88_postrcd_88_post ≤ 0rcd_88_0 + rcd_88_0 ≤ 0rcd_88_0rcd_88_0 ≤ 0rcd_58_post + rcd_58_post ≤ 0rcd_58_postrcd_58_post ≤ 0rcd_58_0 + rcd_58_0 ≤ 0rcd_58_0rcd_58_0 ≤ 0r_39_post + r_39_post ≤ 0r_39_postr_39_post ≤ 0r_39_0 + r_39_0 ≤ 0r_39_0r_39_0 ≤ 0r_163_post + r_163_post ≤ 0r_163_postr_163_post ≤ 0r_163_0 + r_163_0 ≤ 0r_163_0r_163_0 ≤ 0r_124_post + r_124_post ≤ 0r_124_postr_124_post ≤ 0r_124_0 + r_124_0 ≤ 0r_124_0r_124_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_183_post + len_183_post ≤ 0len_183_postlen_183_post ≤ 0len_183_0 + len_183_0 ≤ 0len_183_0len_183_0 ≤ 0len_132_post + len_132_post ≤ 0len_132_postlen_132_post ≤ 0len_132_0 + len_132_0 ≤ 0len_132_0len_132_0 ≤ 0i_94_post + i_94_post ≤ 0i_94_posti_94_post ≤ 0i_94_0 + i_94_0 ≤ 0i_94_0i_94_0 ≤ 0i_30_post + i_30_post ≤ 0i_30_posti_30_post ≤ 0i_30_0 + i_30_0 ≤ 0i_30_0i_30_0 ≤ 0i_167_post + i_167_post ≤ 0i_167_posti_167_post ≤ 0i_167_0 + i_167_0 ≤ 0i_167_0i_167_0 ≤ 0i_108_post + i_108_post ≤ 0i_108_posti_108_post ≤ 0i_108_0 + i_108_0 ≤ 0i_108_0i_108_0 ≤ 0head_SLAM_f_26_post + head_SLAM_f_26_post ≤ 0head_SLAM_f_26_posthead_SLAM_f_26_post ≤ 0head_SLAM_f_26_1 + head_SLAM_f_26_1 ≤ 0head_SLAM_f_26_1head_SLAM_f_26_1 ≤ 0head_SLAM_f_26_0 + head_SLAM_f_26_0 ≤ 0head_SLAM_f_26_0head_SLAM_f_26_0 ≤ 0head_32_post + head_32_post ≤ 0head_32_posthead_32_post ≤ 0head_32_0 + head_32_0 ≤ 0head_32_0head_32_0 ≤ 0head_27_post + head_27_post ≤ 0head_27_posthead_27_post ≤ 0head_27_1 + head_27_1 ≤ 0head_27_1head_27_1 ≤ 0head_27_0 + head_27_0 ≤ 0head_27_0head_27_0 ≤ 0head_175_post + head_175_post ≤ 0head_175_posthead_175_post ≤ 0head_175_0 + head_175_0 ≤ 0head_175_0head_175_0 ≤ 0head_14_post + head_14_post ≤ 0head_14_posthead_14_post ≤ 0head_14_1 + head_14_1 ≤ 0head_14_1head_14_1 ≤ 0head_14_0 + head_14_0 ≤ 0head_14_0head_14_0 ≤ 0head_129_post + head_129_post ≤ 0head_129_posthead_129_post ≤ 0head_129_0 + head_129_0 ≤ 0head_129_0head_129_0 ≤ 0f_170_post + f_170_post ≤ 0f_170_postf_170_post ≤ 0f_170_0 + f_170_0 ≤ 0f_170_0f_170_0 ≤ 0ct_17_post + ct_17_post ≤ 0ct_17_postct_17_post ≤ 0ct_17_2 + ct_17_2 ≤ 0ct_17_2ct_17_2 ≤ 0ct_17_1 + ct_17_1 ≤ 0ct_17_1ct_17_1 ≤ 0ct_17_0 + ct_17_0 ≤ 0ct_17_0ct_17_0 ≤ 0a_260_post + a_260_post ≤ 0a_260_posta_260_post ≤ 0a_260_0 + a_260_0 ≤ 0a_260_0a_260_0 ≤ 0a_237_post + a_237_post ≤ 0a_237_posta_237_post ≤ 0a_237_0 + a_237_0 ≤ 0a_237_0a_237_0 ≤ 0a_215_post + a_215_post ≤ 0a_215_posta_215_post ≤ 0a_215_0 + a_215_0 ≤ 0a_215_0a_215_0 ≤ 0a_184_post + a_184_post ≤ 0a_184_posta_184_post ≤ 0a_184_0 + a_184_0 ≤ 0a_184_0a_184_0 ≤ 0a_147_post + a_147_post ≤ 0a_147_posta_147_post ≤ 0a_147_0 + a_147_0 ≤ 0a_147_0a_147_0 ≤ 0a_116_post + a_116_post ≤ 0a_116_posta_116_post ≤ 0a_116_0 + a_116_0 ≤ 0a_116_0a_116_0 ≤ 0
38 80 38: y_19_post + y_19_post ≤ 0y_19_posty_19_post ≤ 0y_19_2 + y_19_2 ≤ 0y_19_2y_19_2 ≤ 0y_19_1 + y_19_1 ≤ 0y_19_1y_19_1 ≤ 0y_19_0 + y_19_0 ≤ 0y_19_0y_19_0 ≤ 0x_SLAM_f_18_post + x_SLAM_f_18_post ≤ 0x_SLAM_f_18_postx_SLAM_f_18_post ≤ 0x_SLAM_f_18_2 + x_SLAM_f_18_2 ≤ 0x_SLAM_f_18_2x_SLAM_f_18_2 ≤ 0x_SLAM_f_18_1 + x_SLAM_f_18_1 ≤ 0x_SLAM_f_18_1x_SLAM_f_18_1 ≤ 0x_SLAM_f_18_0 + x_SLAM_f_18_0 ≤ 0x_SLAM_f_18_0x_SLAM_f_18_0 ≤ 0x_20_post + x_20_post ≤ 0x_20_postx_20_post ≤ 0x_20_2 + x_20_2 ≤ 0x_20_2x_20_2 ≤ 0x_20_1 + x_20_1 ≤ 0x_20_1x_20_1 ≤ 0x_20_0 + x_20_0 ≤ 0x_20_0x_20_0 ≤ 0x_16_post + x_16_post ≤ 0x_16_postx_16_post ≤ 0x_16_1 + x_16_1 ≤ 0x_16_1x_16_1 ≤ 0x_16_0 + x_16_0 ≤ 0x_16_0x_16_0 ≤ 0tmp_34_post + tmp_34_post ≤ 0tmp_34_posttmp_34_post ≤ 0tmp_34_0 + tmp_34_0 ≤ 0tmp_34_0tmp_34_0 ≤ 0temp_35_post + temp_35_post ≤ 0temp_35_posttemp_35_post ≤ 0temp_35_0 + temp_35_0 ≤ 0temp_35_0temp_35_0 ≤ 0temp0_31_post + temp0_31_post ≤ 0temp0_31_posttemp0_31_post ≤ 0temp0_31_1 + temp0_31_1 ≤ 0temp0_31_1temp0_31_1 ≤ 0temp0_31_0 + temp0_31_0 ≤ 0temp0_31_0temp0_31_0 ≤ 0temp0_15_0 + temp0_15_0 ≤ 0temp0_15_0temp0_15_0 ≤ 0t_23_post + t_23_post ≤ 0t_23_postt_23_post ≤ 0t_23_1 + t_23_1 ≤ 0t_23_1t_23_1 ≤ 0t_23_0 + t_23_0 ≤ 0t_23_0t_23_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_post + result_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_postresult_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_2 + result_dot_nondet_sdv_special_RETURN_VALUE_13_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_2result_dot_nondet_sdv_special_RETURN_VALUE_13_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_1result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_0 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_0result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_postresult_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_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_88_post + rcd_88_post ≤ 0rcd_88_postrcd_88_post ≤ 0rcd_88_0 + rcd_88_0 ≤ 0rcd_88_0rcd_88_0 ≤ 0rcd_58_post + rcd_58_post ≤ 0rcd_58_postrcd_58_post ≤ 0rcd_58_0 + rcd_58_0 ≤ 0rcd_58_0rcd_58_0 ≤ 0r_39_post + r_39_post ≤ 0r_39_postr_39_post ≤ 0r_39_0 + r_39_0 ≤ 0r_39_0r_39_0 ≤ 0r_163_post + r_163_post ≤ 0r_163_postr_163_post ≤ 0r_163_0 + r_163_0 ≤ 0r_163_0r_163_0 ≤ 0r_124_post + r_124_post ≤ 0r_124_postr_124_post ≤ 0r_124_0 + r_124_0 ≤ 0r_124_0r_124_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_183_post + len_183_post ≤ 0len_183_postlen_183_post ≤ 0len_183_0 + len_183_0 ≤ 0len_183_0len_183_0 ≤ 0len_132_post + len_132_post ≤ 0len_132_postlen_132_post ≤ 0len_132_0 + len_132_0 ≤ 0len_132_0len_132_0 ≤ 0i_94_post + i_94_post ≤ 0i_94_posti_94_post ≤ 0i_94_0 + i_94_0 ≤ 0i_94_0i_94_0 ≤ 0i_30_post + i_30_post ≤ 0i_30_posti_30_post ≤ 0i_30_0 + i_30_0 ≤ 0i_30_0i_30_0 ≤ 0i_167_post + i_167_post ≤ 0i_167_posti_167_post ≤ 0i_167_0 + i_167_0 ≤ 0i_167_0i_167_0 ≤ 0i_108_post + i_108_post ≤ 0i_108_posti_108_post ≤ 0i_108_0 + i_108_0 ≤ 0i_108_0i_108_0 ≤ 0head_SLAM_f_26_post + head_SLAM_f_26_post ≤ 0head_SLAM_f_26_posthead_SLAM_f_26_post ≤ 0head_SLAM_f_26_1 + head_SLAM_f_26_1 ≤ 0head_SLAM_f_26_1head_SLAM_f_26_1 ≤ 0head_SLAM_f_26_0 + head_SLAM_f_26_0 ≤ 0head_SLAM_f_26_0head_SLAM_f_26_0 ≤ 0head_32_post + head_32_post ≤ 0head_32_posthead_32_post ≤ 0head_32_0 + head_32_0 ≤ 0head_32_0head_32_0 ≤ 0head_27_post + head_27_post ≤ 0head_27_posthead_27_post ≤ 0head_27_1 + head_27_1 ≤ 0head_27_1head_27_1 ≤ 0head_27_0 + head_27_0 ≤ 0head_27_0head_27_0 ≤ 0head_175_post + head_175_post ≤ 0head_175_posthead_175_post ≤ 0head_175_0 + head_175_0 ≤ 0head_175_0head_175_0 ≤ 0head_14_post + head_14_post ≤ 0head_14_posthead_14_post ≤ 0head_14_1 + head_14_1 ≤ 0head_14_1head_14_1 ≤ 0head_14_0 + head_14_0 ≤ 0head_14_0head_14_0 ≤ 0head_129_post + head_129_post ≤ 0head_129_posthead_129_post ≤ 0head_129_0 + head_129_0 ≤ 0head_129_0head_129_0 ≤ 0f_170_post + f_170_post ≤ 0f_170_postf_170_post ≤ 0f_170_0 + f_170_0 ≤ 0f_170_0f_170_0 ≤ 0ct_17_post + ct_17_post ≤ 0ct_17_postct_17_post ≤ 0ct_17_2 + ct_17_2 ≤ 0ct_17_2ct_17_2 ≤ 0ct_17_1 + ct_17_1 ≤ 0ct_17_1ct_17_1 ≤ 0ct_17_0 + ct_17_0 ≤ 0ct_17_0ct_17_0 ≤ 0a_260_post + a_260_post ≤ 0a_260_posta_260_post ≤ 0a_260_0 + a_260_0 ≤ 0a_260_0a_260_0 ≤ 0a_237_post + a_237_post ≤ 0a_237_posta_237_post ≤ 0a_237_0 + a_237_0 ≤ 0a_237_0a_237_0 ≤ 0a_215_post + a_215_post ≤ 0a_215_posta_215_post ≤ 0a_215_0 + a_215_0 ≤ 0a_215_0a_215_0 ≤ 0a_184_post + a_184_post ≤ 0a_184_posta_184_post ≤ 0a_184_0 + a_184_0 ≤ 0a_184_0a_184_0 ≤ 0a_147_post + a_147_post ≤ 0a_147_posta_147_post ≤ 0a_147_0 + a_147_0 ≤ 0a_147_0a_147_0 ≤ 0a_116_post + a_116_post ≤ 0a_116_posta_116_post ≤ 0a_116_0 + a_116_0 ≤ 0a_116_0a_116_0 ≤ 0
41 87 41: y_19_post + y_19_post ≤ 0y_19_posty_19_post ≤ 0y_19_2 + y_19_2 ≤ 0y_19_2y_19_2 ≤ 0y_19_1 + y_19_1 ≤ 0y_19_1y_19_1 ≤ 0y_19_0 + y_19_0 ≤ 0y_19_0y_19_0 ≤ 0x_SLAM_f_18_post + x_SLAM_f_18_post ≤ 0x_SLAM_f_18_postx_SLAM_f_18_post ≤ 0x_SLAM_f_18_2 + x_SLAM_f_18_2 ≤ 0x_SLAM_f_18_2x_SLAM_f_18_2 ≤ 0x_SLAM_f_18_1 + x_SLAM_f_18_1 ≤ 0x_SLAM_f_18_1x_SLAM_f_18_1 ≤ 0x_SLAM_f_18_0 + x_SLAM_f_18_0 ≤ 0x_SLAM_f_18_0x_SLAM_f_18_0 ≤ 0x_20_post + x_20_post ≤ 0x_20_postx_20_post ≤ 0x_20_2 + x_20_2 ≤ 0x_20_2x_20_2 ≤ 0x_20_1 + x_20_1 ≤ 0x_20_1x_20_1 ≤ 0x_20_0 + x_20_0 ≤ 0x_20_0x_20_0 ≤ 0x_16_post + x_16_post ≤ 0x_16_postx_16_post ≤ 0x_16_1 + x_16_1 ≤ 0x_16_1x_16_1 ≤ 0x_16_0 + x_16_0 ≤ 0x_16_0x_16_0 ≤ 0tmp_34_post + tmp_34_post ≤ 0tmp_34_posttmp_34_post ≤ 0tmp_34_0 + tmp_34_0 ≤ 0tmp_34_0tmp_34_0 ≤ 0temp_35_post + temp_35_post ≤ 0temp_35_posttemp_35_post ≤ 0temp_35_0 + temp_35_0 ≤ 0temp_35_0temp_35_0 ≤ 0temp0_31_post + temp0_31_post ≤ 0temp0_31_posttemp0_31_post ≤ 0temp0_31_1 + temp0_31_1 ≤ 0temp0_31_1temp0_31_1 ≤ 0temp0_31_0 + temp0_31_0 ≤ 0temp0_31_0temp0_31_0 ≤ 0temp0_15_0 + temp0_15_0 ≤ 0temp0_15_0temp0_15_0 ≤ 0t_23_post + t_23_post ≤ 0t_23_postt_23_post ≤ 0t_23_1 + t_23_1 ≤ 0t_23_1t_23_1 ≤ 0t_23_0 + t_23_0 ≤ 0t_23_0t_23_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_post + result_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_postresult_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_2 + result_dot_nondet_sdv_special_RETURN_VALUE_13_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_2result_dot_nondet_sdv_special_RETURN_VALUE_13_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_1result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_0 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_0result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_postresult_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_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_88_post + rcd_88_post ≤ 0rcd_88_postrcd_88_post ≤ 0rcd_88_0 + rcd_88_0 ≤ 0rcd_88_0rcd_88_0 ≤ 0rcd_58_post + rcd_58_post ≤ 0rcd_58_postrcd_58_post ≤ 0rcd_58_0 + rcd_58_0 ≤ 0rcd_58_0rcd_58_0 ≤ 0r_39_post + r_39_post ≤ 0r_39_postr_39_post ≤ 0r_39_0 + r_39_0 ≤ 0r_39_0r_39_0 ≤ 0r_163_post + r_163_post ≤ 0r_163_postr_163_post ≤ 0r_163_0 + r_163_0 ≤ 0r_163_0r_163_0 ≤ 0r_124_post + r_124_post ≤ 0r_124_postr_124_post ≤ 0r_124_0 + r_124_0 ≤ 0r_124_0r_124_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_183_post + len_183_post ≤ 0len_183_postlen_183_post ≤ 0len_183_0 + len_183_0 ≤ 0len_183_0len_183_0 ≤ 0len_132_post + len_132_post ≤ 0len_132_postlen_132_post ≤ 0len_132_0 + len_132_0 ≤ 0len_132_0len_132_0 ≤ 0i_94_post + i_94_post ≤ 0i_94_posti_94_post ≤ 0i_94_0 + i_94_0 ≤ 0i_94_0i_94_0 ≤ 0i_30_post + i_30_post ≤ 0i_30_posti_30_post ≤ 0i_30_0 + i_30_0 ≤ 0i_30_0i_30_0 ≤ 0i_167_post + i_167_post ≤ 0i_167_posti_167_post ≤ 0i_167_0 + i_167_0 ≤ 0i_167_0i_167_0 ≤ 0i_108_post + i_108_post ≤ 0i_108_posti_108_post ≤ 0i_108_0 + i_108_0 ≤ 0i_108_0i_108_0 ≤ 0head_SLAM_f_26_post + head_SLAM_f_26_post ≤ 0head_SLAM_f_26_posthead_SLAM_f_26_post ≤ 0head_SLAM_f_26_1 + head_SLAM_f_26_1 ≤ 0head_SLAM_f_26_1head_SLAM_f_26_1 ≤ 0head_SLAM_f_26_0 + head_SLAM_f_26_0 ≤ 0head_SLAM_f_26_0head_SLAM_f_26_0 ≤ 0head_32_post + head_32_post ≤ 0head_32_posthead_32_post ≤ 0head_32_0 + head_32_0 ≤ 0head_32_0head_32_0 ≤ 0head_27_post + head_27_post ≤ 0head_27_posthead_27_post ≤ 0head_27_1 + head_27_1 ≤ 0head_27_1head_27_1 ≤ 0head_27_0 + head_27_0 ≤ 0head_27_0head_27_0 ≤ 0head_175_post + head_175_post ≤ 0head_175_posthead_175_post ≤ 0head_175_0 + head_175_0 ≤ 0head_175_0head_175_0 ≤ 0head_14_post + head_14_post ≤ 0head_14_posthead_14_post ≤ 0head_14_1 + head_14_1 ≤ 0head_14_1head_14_1 ≤ 0head_14_0 + head_14_0 ≤ 0head_14_0head_14_0 ≤ 0head_129_post + head_129_post ≤ 0head_129_posthead_129_post ≤ 0head_129_0 + head_129_0 ≤ 0head_129_0head_129_0 ≤ 0f_170_post + f_170_post ≤ 0f_170_postf_170_post ≤ 0f_170_0 + f_170_0 ≤ 0f_170_0f_170_0 ≤ 0ct_17_post + ct_17_post ≤ 0ct_17_postct_17_post ≤ 0ct_17_2 + ct_17_2 ≤ 0ct_17_2ct_17_2 ≤ 0ct_17_1 + ct_17_1 ≤ 0ct_17_1ct_17_1 ≤ 0ct_17_0 + ct_17_0 ≤ 0ct_17_0ct_17_0 ≤ 0a_260_post + a_260_post ≤ 0a_260_posta_260_post ≤ 0a_260_0 + a_260_0 ≤ 0a_260_0a_260_0 ≤ 0a_237_post + a_237_post ≤ 0a_237_posta_237_post ≤ 0a_237_0 + a_237_0 ≤ 0a_237_0a_237_0 ≤ 0a_215_post + a_215_post ≤ 0a_215_posta_215_post ≤ 0a_215_0 + a_215_0 ≤ 0a_215_0a_215_0 ≤ 0a_184_post + a_184_post ≤ 0a_184_posta_184_post ≤ 0a_184_0 + a_184_0 ≤ 0a_184_0a_184_0 ≤ 0a_147_post + a_147_post ≤ 0a_147_posta_147_post ≤ 0a_147_0 + a_147_0 ≤ 0a_147_0a_147_0 ≤ 0a_116_post + a_116_post ≤ 0a_116_posta_116_post ≤ 0a_116_0 + a_116_0 ≤ 0a_116_0a_116_0 ≤ 0
and for every transition t, a duplicate t is considered.

3 Transition Removal

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

66: 0
39: 0
40: 0
25: 0
26: 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
65: 0
63: 0
64: 0
41: 0
44: 0
45: 0
46: 0
47: 0
48: 0
49: 0
42: 0
43: 0
18: 0
19: 0
20: 0
21: 0
22: 0
23: 0
24: 0
0: 0
2: 0
3: 0
4: 0
5: 0
6: 0
7: 0
8: 0
1: 0
66: −32
39: −33
40: −34
25: −35
26: −36
27: −37
28: −38
29: −39
30: −40
31: −41
32: −42
33: −43
34: −44
35: −45
36: −46
37: −47
38: −48
65: −48
38_var_snapshot: −48
38*: −48
63: −51
64: −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
18: −58
19: −59
20: −60
21: −61
22: −62
23: −63
24: −64
0: −65
2: −65
3: −65
4: −65
5: −65
6: −65
7: −65
8: −65
0_var_snapshot: −65
0*: −65
1: −69

4 Location Addition

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

0* 76 0: y_19_post + y_19_post ≤ 0y_19_posty_19_post ≤ 0y_19_2 + y_19_2 ≤ 0y_19_2y_19_2 ≤ 0y_19_1 + y_19_1 ≤ 0y_19_1y_19_1 ≤ 0y_19_0 + y_19_0 ≤ 0y_19_0y_19_0 ≤ 0x_SLAM_f_18_post + x_SLAM_f_18_post ≤ 0x_SLAM_f_18_postx_SLAM_f_18_post ≤ 0x_SLAM_f_18_2 + x_SLAM_f_18_2 ≤ 0x_SLAM_f_18_2x_SLAM_f_18_2 ≤ 0x_SLAM_f_18_1 + x_SLAM_f_18_1 ≤ 0x_SLAM_f_18_1x_SLAM_f_18_1 ≤ 0x_SLAM_f_18_0 + x_SLAM_f_18_0 ≤ 0x_SLAM_f_18_0x_SLAM_f_18_0 ≤ 0x_20_post + x_20_post ≤ 0x_20_postx_20_post ≤ 0x_20_2 + x_20_2 ≤ 0x_20_2x_20_2 ≤ 0x_20_1 + x_20_1 ≤ 0x_20_1x_20_1 ≤ 0x_20_0 + x_20_0 ≤ 0x_20_0x_20_0 ≤ 0x_16_post + x_16_post ≤ 0x_16_postx_16_post ≤ 0x_16_1 + x_16_1 ≤ 0x_16_1x_16_1 ≤ 0x_16_0 + x_16_0 ≤ 0x_16_0x_16_0 ≤ 0tmp_34_post + tmp_34_post ≤ 0tmp_34_posttmp_34_post ≤ 0tmp_34_0 + tmp_34_0 ≤ 0tmp_34_0tmp_34_0 ≤ 0temp_35_post + temp_35_post ≤ 0temp_35_posttemp_35_post ≤ 0temp_35_0 + temp_35_0 ≤ 0temp_35_0temp_35_0 ≤ 0temp0_31_post + temp0_31_post ≤ 0temp0_31_posttemp0_31_post ≤ 0temp0_31_1 + temp0_31_1 ≤ 0temp0_31_1temp0_31_1 ≤ 0temp0_31_0 + temp0_31_0 ≤ 0temp0_31_0temp0_31_0 ≤ 0temp0_15_0 + temp0_15_0 ≤ 0temp0_15_0temp0_15_0 ≤ 0t_23_post + t_23_post ≤ 0t_23_postt_23_post ≤ 0t_23_1 + t_23_1 ≤ 0t_23_1t_23_1 ≤ 0t_23_0 + t_23_0 ≤ 0t_23_0t_23_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_post + result_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_postresult_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_2 + result_dot_nondet_sdv_special_RETURN_VALUE_13_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_2result_dot_nondet_sdv_special_RETURN_VALUE_13_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_1result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_0 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_0result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_postresult_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_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_88_post + rcd_88_post ≤ 0rcd_88_postrcd_88_post ≤ 0rcd_88_0 + rcd_88_0 ≤ 0rcd_88_0rcd_88_0 ≤ 0rcd_58_post + rcd_58_post ≤ 0rcd_58_postrcd_58_post ≤ 0rcd_58_0 + rcd_58_0 ≤ 0rcd_58_0rcd_58_0 ≤ 0r_39_post + r_39_post ≤ 0r_39_postr_39_post ≤ 0r_39_0 + r_39_0 ≤ 0r_39_0r_39_0 ≤ 0r_163_post + r_163_post ≤ 0r_163_postr_163_post ≤ 0r_163_0 + r_163_0 ≤ 0r_163_0r_163_0 ≤ 0r_124_post + r_124_post ≤ 0r_124_postr_124_post ≤ 0r_124_0 + r_124_0 ≤ 0r_124_0r_124_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_183_post + len_183_post ≤ 0len_183_postlen_183_post ≤ 0len_183_0 + len_183_0 ≤ 0len_183_0len_183_0 ≤ 0len_132_post + len_132_post ≤ 0len_132_postlen_132_post ≤ 0len_132_0 + len_132_0 ≤ 0len_132_0len_132_0 ≤ 0i_94_post + i_94_post ≤ 0i_94_posti_94_post ≤ 0i_94_0 + i_94_0 ≤ 0i_94_0i_94_0 ≤ 0i_30_post + i_30_post ≤ 0i_30_posti_30_post ≤ 0i_30_0 + i_30_0 ≤ 0i_30_0i_30_0 ≤ 0i_167_post + i_167_post ≤ 0i_167_posti_167_post ≤ 0i_167_0 + i_167_0 ≤ 0i_167_0i_167_0 ≤ 0i_108_post + i_108_post ≤ 0i_108_posti_108_post ≤ 0i_108_0 + i_108_0 ≤ 0i_108_0i_108_0 ≤ 0head_SLAM_f_26_post + head_SLAM_f_26_post ≤ 0head_SLAM_f_26_posthead_SLAM_f_26_post ≤ 0head_SLAM_f_26_1 + head_SLAM_f_26_1 ≤ 0head_SLAM_f_26_1head_SLAM_f_26_1 ≤ 0head_SLAM_f_26_0 + head_SLAM_f_26_0 ≤ 0head_SLAM_f_26_0head_SLAM_f_26_0 ≤ 0head_32_post + head_32_post ≤ 0head_32_posthead_32_post ≤ 0head_32_0 + head_32_0 ≤ 0head_32_0head_32_0 ≤ 0head_27_post + head_27_post ≤ 0head_27_posthead_27_post ≤ 0head_27_1 + head_27_1 ≤ 0head_27_1head_27_1 ≤ 0head_27_0 + head_27_0 ≤ 0head_27_0head_27_0 ≤ 0head_175_post + head_175_post ≤ 0head_175_posthead_175_post ≤ 0head_175_0 + head_175_0 ≤ 0head_175_0head_175_0 ≤ 0head_14_post + head_14_post ≤ 0head_14_posthead_14_post ≤ 0head_14_1 + head_14_1 ≤ 0head_14_1head_14_1 ≤ 0head_14_0 + head_14_0 ≤ 0head_14_0head_14_0 ≤ 0head_129_post + head_129_post ≤ 0head_129_posthead_129_post ≤ 0head_129_0 + head_129_0 ≤ 0head_129_0head_129_0 ≤ 0f_170_post + f_170_post ≤ 0f_170_postf_170_post ≤ 0f_170_0 + f_170_0 ≤ 0f_170_0f_170_0 ≤ 0ct_17_post + ct_17_post ≤ 0ct_17_postct_17_post ≤ 0ct_17_2 + ct_17_2 ≤ 0ct_17_2ct_17_2 ≤ 0ct_17_1 + ct_17_1 ≤ 0ct_17_1ct_17_1 ≤ 0ct_17_0 + ct_17_0 ≤ 0ct_17_0ct_17_0 ≤ 0a_260_post + a_260_post ≤ 0a_260_posta_260_post ≤ 0a_260_0 + a_260_0 ≤ 0a_260_0a_260_0 ≤ 0a_237_post + a_237_post ≤ 0a_237_posta_237_post ≤ 0a_237_0 + a_237_0 ≤ 0a_237_0a_237_0 ≤ 0a_215_post + a_215_post ≤ 0a_215_posta_215_post ≤ 0a_215_0 + a_215_0 ≤ 0a_215_0a_215_0 ≤ 0a_184_post + a_184_post ≤ 0a_184_posta_184_post ≤ 0a_184_0 + a_184_0 ≤ 0a_184_0a_184_0 ≤ 0a_147_post + a_147_post ≤ 0a_147_posta_147_post ≤ 0a_147_0 + a_147_0 ≤ 0a_147_0a_147_0 ≤ 0a_116_post + a_116_post ≤ 0a_116_posta_116_post ≤ 0a_116_0 + a_116_0 ≤ 0a_116_0a_116_0 ≤ 0

5 Location Addition

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

0 74 0_var_snapshot: y_19_post + y_19_post ≤ 0y_19_posty_19_post ≤ 0y_19_2 + y_19_2 ≤ 0y_19_2y_19_2 ≤ 0y_19_1 + y_19_1 ≤ 0y_19_1y_19_1 ≤ 0y_19_0 + y_19_0 ≤ 0y_19_0y_19_0 ≤ 0x_SLAM_f_18_post + x_SLAM_f_18_post ≤ 0x_SLAM_f_18_postx_SLAM_f_18_post ≤ 0x_SLAM_f_18_2 + x_SLAM_f_18_2 ≤ 0x_SLAM_f_18_2x_SLAM_f_18_2 ≤ 0x_SLAM_f_18_1 + x_SLAM_f_18_1 ≤ 0x_SLAM_f_18_1x_SLAM_f_18_1 ≤ 0x_SLAM_f_18_0 + x_SLAM_f_18_0 ≤ 0x_SLAM_f_18_0x_SLAM_f_18_0 ≤ 0x_20_post + x_20_post ≤ 0x_20_postx_20_post ≤ 0x_20_2 + x_20_2 ≤ 0x_20_2x_20_2 ≤ 0x_20_1 + x_20_1 ≤ 0x_20_1x_20_1 ≤ 0x_20_0 + x_20_0 ≤ 0x_20_0x_20_0 ≤ 0x_16_post + x_16_post ≤ 0x_16_postx_16_post ≤ 0x_16_1 + x_16_1 ≤ 0x_16_1x_16_1 ≤ 0x_16_0 + x_16_0 ≤ 0x_16_0x_16_0 ≤ 0tmp_34_post + tmp_34_post ≤ 0tmp_34_posttmp_34_post ≤ 0tmp_34_0 + tmp_34_0 ≤ 0tmp_34_0tmp_34_0 ≤ 0temp_35_post + temp_35_post ≤ 0temp_35_posttemp_35_post ≤ 0temp_35_0 + temp_35_0 ≤ 0temp_35_0temp_35_0 ≤ 0temp0_31_post + temp0_31_post ≤ 0temp0_31_posttemp0_31_post ≤ 0temp0_31_1 + temp0_31_1 ≤ 0temp0_31_1temp0_31_1 ≤ 0temp0_31_0 + temp0_31_0 ≤ 0temp0_31_0temp0_31_0 ≤ 0temp0_15_0 + temp0_15_0 ≤ 0temp0_15_0temp0_15_0 ≤ 0t_23_post + t_23_post ≤ 0t_23_postt_23_post ≤ 0t_23_1 + t_23_1 ≤ 0t_23_1t_23_1 ≤ 0t_23_0 + t_23_0 ≤ 0t_23_0t_23_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_post + result_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_postresult_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_2 + result_dot_nondet_sdv_special_RETURN_VALUE_13_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_2result_dot_nondet_sdv_special_RETURN_VALUE_13_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_1result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_0 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_0result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_postresult_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_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_88_post + rcd_88_post ≤ 0rcd_88_postrcd_88_post ≤ 0rcd_88_0 + rcd_88_0 ≤ 0rcd_88_0rcd_88_0 ≤ 0rcd_58_post + rcd_58_post ≤ 0rcd_58_postrcd_58_post ≤ 0rcd_58_0 + rcd_58_0 ≤ 0rcd_58_0rcd_58_0 ≤ 0r_39_post + r_39_post ≤ 0r_39_postr_39_post ≤ 0r_39_0 + r_39_0 ≤ 0r_39_0r_39_0 ≤ 0r_163_post + r_163_post ≤ 0r_163_postr_163_post ≤ 0r_163_0 + r_163_0 ≤ 0r_163_0r_163_0 ≤ 0r_124_post + r_124_post ≤ 0r_124_postr_124_post ≤ 0r_124_0 + r_124_0 ≤ 0r_124_0r_124_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_183_post + len_183_post ≤ 0len_183_postlen_183_post ≤ 0len_183_0 + len_183_0 ≤ 0len_183_0len_183_0 ≤ 0len_132_post + len_132_post ≤ 0len_132_postlen_132_post ≤ 0len_132_0 + len_132_0 ≤ 0len_132_0len_132_0 ≤ 0i_94_post + i_94_post ≤ 0i_94_posti_94_post ≤ 0i_94_0 + i_94_0 ≤ 0i_94_0i_94_0 ≤ 0i_30_post + i_30_post ≤ 0i_30_posti_30_post ≤ 0i_30_0 + i_30_0 ≤ 0i_30_0i_30_0 ≤ 0i_167_post + i_167_post ≤ 0i_167_posti_167_post ≤ 0i_167_0 + i_167_0 ≤ 0i_167_0i_167_0 ≤ 0i_108_post + i_108_post ≤ 0i_108_posti_108_post ≤ 0i_108_0 + i_108_0 ≤ 0i_108_0i_108_0 ≤ 0head_SLAM_f_26_post + head_SLAM_f_26_post ≤ 0head_SLAM_f_26_posthead_SLAM_f_26_post ≤ 0head_SLAM_f_26_1 + head_SLAM_f_26_1 ≤ 0head_SLAM_f_26_1head_SLAM_f_26_1 ≤ 0head_SLAM_f_26_0 + head_SLAM_f_26_0 ≤ 0head_SLAM_f_26_0head_SLAM_f_26_0 ≤ 0head_32_post + head_32_post ≤ 0head_32_posthead_32_post ≤ 0head_32_0 + head_32_0 ≤ 0head_32_0head_32_0 ≤ 0head_27_post + head_27_post ≤ 0head_27_posthead_27_post ≤ 0head_27_1 + head_27_1 ≤ 0head_27_1head_27_1 ≤ 0head_27_0 + head_27_0 ≤ 0head_27_0head_27_0 ≤ 0head_175_post + head_175_post ≤ 0head_175_posthead_175_post ≤ 0head_175_0 + head_175_0 ≤ 0head_175_0head_175_0 ≤ 0head_14_post + head_14_post ≤ 0head_14_posthead_14_post ≤ 0head_14_1 + head_14_1 ≤ 0head_14_1head_14_1 ≤ 0head_14_0 + head_14_0 ≤ 0head_14_0head_14_0 ≤ 0head_129_post + head_129_post ≤ 0head_129_posthead_129_post ≤ 0head_129_0 + head_129_0 ≤ 0head_129_0head_129_0 ≤ 0f_170_post + f_170_post ≤ 0f_170_postf_170_post ≤ 0f_170_0 + f_170_0 ≤ 0f_170_0f_170_0 ≤ 0ct_17_post + ct_17_post ≤ 0ct_17_postct_17_post ≤ 0ct_17_2 + ct_17_2 ≤ 0ct_17_2ct_17_2 ≤ 0ct_17_1 + ct_17_1 ≤ 0ct_17_1ct_17_1 ≤ 0ct_17_0 + ct_17_0 ≤ 0ct_17_0ct_17_0 ≤ 0a_260_post + a_260_post ≤ 0a_260_posta_260_post ≤ 0a_260_0 + a_260_0 ≤ 0a_260_0a_260_0 ≤ 0a_237_post + a_237_post ≤ 0a_237_posta_237_post ≤ 0a_237_0 + a_237_0 ≤ 0a_237_0a_237_0 ≤ 0a_215_post + a_215_post ≤ 0a_215_posta_215_post ≤ 0a_215_0 + a_215_0 ≤ 0a_215_0a_215_0 ≤ 0a_184_post + a_184_post ≤ 0a_184_posta_184_post ≤ 0a_184_0 + a_184_0 ≤ 0a_184_0a_184_0 ≤ 0a_147_post + a_147_post ≤ 0a_147_posta_147_post ≤ 0a_147_0 + a_147_0 ≤ 0a_147_0a_147_0 ≤ 0a_116_post + a_116_post ≤ 0a_116_posta_116_post ≤ 0a_116_0 + a_116_0 ≤ 0a_116_0a_116_0 ≤ 0

6 Location Addition

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

38* 83 38: y_19_post + y_19_post ≤ 0y_19_posty_19_post ≤ 0y_19_2 + y_19_2 ≤ 0y_19_2y_19_2 ≤ 0y_19_1 + y_19_1 ≤ 0y_19_1y_19_1 ≤ 0y_19_0 + y_19_0 ≤ 0y_19_0y_19_0 ≤ 0x_SLAM_f_18_post + x_SLAM_f_18_post ≤ 0x_SLAM_f_18_postx_SLAM_f_18_post ≤ 0x_SLAM_f_18_2 + x_SLAM_f_18_2 ≤ 0x_SLAM_f_18_2x_SLAM_f_18_2 ≤ 0x_SLAM_f_18_1 + x_SLAM_f_18_1 ≤ 0x_SLAM_f_18_1x_SLAM_f_18_1 ≤ 0x_SLAM_f_18_0 + x_SLAM_f_18_0 ≤ 0x_SLAM_f_18_0x_SLAM_f_18_0 ≤ 0x_20_post + x_20_post ≤ 0x_20_postx_20_post ≤ 0x_20_2 + x_20_2 ≤ 0x_20_2x_20_2 ≤ 0x_20_1 + x_20_1 ≤ 0x_20_1x_20_1 ≤ 0x_20_0 + x_20_0 ≤ 0x_20_0x_20_0 ≤ 0x_16_post + x_16_post ≤ 0x_16_postx_16_post ≤ 0x_16_1 + x_16_1 ≤ 0x_16_1x_16_1 ≤ 0x_16_0 + x_16_0 ≤ 0x_16_0x_16_0 ≤ 0tmp_34_post + tmp_34_post ≤ 0tmp_34_posttmp_34_post ≤ 0tmp_34_0 + tmp_34_0 ≤ 0tmp_34_0tmp_34_0 ≤ 0temp_35_post + temp_35_post ≤ 0temp_35_posttemp_35_post ≤ 0temp_35_0 + temp_35_0 ≤ 0temp_35_0temp_35_0 ≤ 0temp0_31_post + temp0_31_post ≤ 0temp0_31_posttemp0_31_post ≤ 0temp0_31_1 + temp0_31_1 ≤ 0temp0_31_1temp0_31_1 ≤ 0temp0_31_0 + temp0_31_0 ≤ 0temp0_31_0temp0_31_0 ≤ 0temp0_15_0 + temp0_15_0 ≤ 0temp0_15_0temp0_15_0 ≤ 0t_23_post + t_23_post ≤ 0t_23_postt_23_post ≤ 0t_23_1 + t_23_1 ≤ 0t_23_1t_23_1 ≤ 0t_23_0 + t_23_0 ≤ 0t_23_0t_23_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_post + result_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_postresult_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_2 + result_dot_nondet_sdv_special_RETURN_VALUE_13_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_2result_dot_nondet_sdv_special_RETURN_VALUE_13_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_1result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_0 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_0result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_postresult_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_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_88_post + rcd_88_post ≤ 0rcd_88_postrcd_88_post ≤ 0rcd_88_0 + rcd_88_0 ≤ 0rcd_88_0rcd_88_0 ≤ 0rcd_58_post + rcd_58_post ≤ 0rcd_58_postrcd_58_post ≤ 0rcd_58_0 + rcd_58_0 ≤ 0rcd_58_0rcd_58_0 ≤ 0r_39_post + r_39_post ≤ 0r_39_postr_39_post ≤ 0r_39_0 + r_39_0 ≤ 0r_39_0r_39_0 ≤ 0r_163_post + r_163_post ≤ 0r_163_postr_163_post ≤ 0r_163_0 + r_163_0 ≤ 0r_163_0r_163_0 ≤ 0r_124_post + r_124_post ≤ 0r_124_postr_124_post ≤ 0r_124_0 + r_124_0 ≤ 0r_124_0r_124_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_183_post + len_183_post ≤ 0len_183_postlen_183_post ≤ 0len_183_0 + len_183_0 ≤ 0len_183_0len_183_0 ≤ 0len_132_post + len_132_post ≤ 0len_132_postlen_132_post ≤ 0len_132_0 + len_132_0 ≤ 0len_132_0len_132_0 ≤ 0i_94_post + i_94_post ≤ 0i_94_posti_94_post ≤ 0i_94_0 + i_94_0 ≤ 0i_94_0i_94_0 ≤ 0i_30_post + i_30_post ≤ 0i_30_posti_30_post ≤ 0i_30_0 + i_30_0 ≤ 0i_30_0i_30_0 ≤ 0i_167_post + i_167_post ≤ 0i_167_posti_167_post ≤ 0i_167_0 + i_167_0 ≤ 0i_167_0i_167_0 ≤ 0i_108_post + i_108_post ≤ 0i_108_posti_108_post ≤ 0i_108_0 + i_108_0 ≤ 0i_108_0i_108_0 ≤ 0head_SLAM_f_26_post + head_SLAM_f_26_post ≤ 0head_SLAM_f_26_posthead_SLAM_f_26_post ≤ 0head_SLAM_f_26_1 + head_SLAM_f_26_1 ≤ 0head_SLAM_f_26_1head_SLAM_f_26_1 ≤ 0head_SLAM_f_26_0 + head_SLAM_f_26_0 ≤ 0head_SLAM_f_26_0head_SLAM_f_26_0 ≤ 0head_32_post + head_32_post ≤ 0head_32_posthead_32_post ≤ 0head_32_0 + head_32_0 ≤ 0head_32_0head_32_0 ≤ 0head_27_post + head_27_post ≤ 0head_27_posthead_27_post ≤ 0head_27_1 + head_27_1 ≤ 0head_27_1head_27_1 ≤ 0head_27_0 + head_27_0 ≤ 0head_27_0head_27_0 ≤ 0head_175_post + head_175_post ≤ 0head_175_posthead_175_post ≤ 0head_175_0 + head_175_0 ≤ 0head_175_0head_175_0 ≤ 0head_14_post + head_14_post ≤ 0head_14_posthead_14_post ≤ 0head_14_1 + head_14_1 ≤ 0head_14_1head_14_1 ≤ 0head_14_0 + head_14_0 ≤ 0head_14_0head_14_0 ≤ 0head_129_post + head_129_post ≤ 0head_129_posthead_129_post ≤ 0head_129_0 + head_129_0 ≤ 0head_129_0head_129_0 ≤ 0f_170_post + f_170_post ≤ 0f_170_postf_170_post ≤ 0f_170_0 + f_170_0 ≤ 0f_170_0f_170_0 ≤ 0ct_17_post + ct_17_post ≤ 0ct_17_postct_17_post ≤ 0ct_17_2 + ct_17_2 ≤ 0ct_17_2ct_17_2 ≤ 0ct_17_1 + ct_17_1 ≤ 0ct_17_1ct_17_1 ≤ 0ct_17_0 + ct_17_0 ≤ 0ct_17_0ct_17_0 ≤ 0a_260_post + a_260_post ≤ 0a_260_posta_260_post ≤ 0a_260_0 + a_260_0 ≤ 0a_260_0a_260_0 ≤ 0a_237_post + a_237_post ≤ 0a_237_posta_237_post ≤ 0a_237_0 + a_237_0 ≤ 0a_237_0a_237_0 ≤ 0a_215_post + a_215_post ≤ 0a_215_posta_215_post ≤ 0a_215_0 + a_215_0 ≤ 0a_215_0a_215_0 ≤ 0a_184_post + a_184_post ≤ 0a_184_posta_184_post ≤ 0a_184_0 + a_184_0 ≤ 0a_184_0a_184_0 ≤ 0a_147_post + a_147_post ≤ 0a_147_posta_147_post ≤ 0a_147_0 + a_147_0 ≤ 0a_147_0a_147_0 ≤ 0a_116_post + a_116_post ≤ 0a_116_posta_116_post ≤ 0a_116_0 + a_116_0 ≤ 0a_116_0a_116_0 ≤ 0

7 Location Addition

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

38 81 38_var_snapshot: y_19_post + y_19_post ≤ 0y_19_posty_19_post ≤ 0y_19_2 + y_19_2 ≤ 0y_19_2y_19_2 ≤ 0y_19_1 + y_19_1 ≤ 0y_19_1y_19_1 ≤ 0y_19_0 + y_19_0 ≤ 0y_19_0y_19_0 ≤ 0x_SLAM_f_18_post + x_SLAM_f_18_post ≤ 0x_SLAM_f_18_postx_SLAM_f_18_post ≤ 0x_SLAM_f_18_2 + x_SLAM_f_18_2 ≤ 0x_SLAM_f_18_2x_SLAM_f_18_2 ≤ 0x_SLAM_f_18_1 + x_SLAM_f_18_1 ≤ 0x_SLAM_f_18_1x_SLAM_f_18_1 ≤ 0x_SLAM_f_18_0 + x_SLAM_f_18_0 ≤ 0x_SLAM_f_18_0x_SLAM_f_18_0 ≤ 0x_20_post + x_20_post ≤ 0x_20_postx_20_post ≤ 0x_20_2 + x_20_2 ≤ 0x_20_2x_20_2 ≤ 0x_20_1 + x_20_1 ≤ 0x_20_1x_20_1 ≤ 0x_20_0 + x_20_0 ≤ 0x_20_0x_20_0 ≤ 0x_16_post + x_16_post ≤ 0x_16_postx_16_post ≤ 0x_16_1 + x_16_1 ≤ 0x_16_1x_16_1 ≤ 0x_16_0 + x_16_0 ≤ 0x_16_0x_16_0 ≤ 0tmp_34_post + tmp_34_post ≤ 0tmp_34_posttmp_34_post ≤ 0tmp_34_0 + tmp_34_0 ≤ 0tmp_34_0tmp_34_0 ≤ 0temp_35_post + temp_35_post ≤ 0temp_35_posttemp_35_post ≤ 0temp_35_0 + temp_35_0 ≤ 0temp_35_0temp_35_0 ≤ 0temp0_31_post + temp0_31_post ≤ 0temp0_31_posttemp0_31_post ≤ 0temp0_31_1 + temp0_31_1 ≤ 0temp0_31_1temp0_31_1 ≤ 0temp0_31_0 + temp0_31_0 ≤ 0temp0_31_0temp0_31_0 ≤ 0temp0_15_0 + temp0_15_0 ≤ 0temp0_15_0temp0_15_0 ≤ 0t_23_post + t_23_post ≤ 0t_23_postt_23_post ≤ 0t_23_1 + t_23_1 ≤ 0t_23_1t_23_1 ≤ 0t_23_0 + t_23_0 ≤ 0t_23_0t_23_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_post + result_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_postresult_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_2 + result_dot_nondet_sdv_special_RETURN_VALUE_13_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_2result_dot_nondet_sdv_special_RETURN_VALUE_13_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_1result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_0 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_0result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_postresult_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_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_88_post + rcd_88_post ≤ 0rcd_88_postrcd_88_post ≤ 0rcd_88_0 + rcd_88_0 ≤ 0rcd_88_0rcd_88_0 ≤ 0rcd_58_post + rcd_58_post ≤ 0rcd_58_postrcd_58_post ≤ 0rcd_58_0 + rcd_58_0 ≤ 0rcd_58_0rcd_58_0 ≤ 0r_39_post + r_39_post ≤ 0r_39_postr_39_post ≤ 0r_39_0 + r_39_0 ≤ 0r_39_0r_39_0 ≤ 0r_163_post + r_163_post ≤ 0r_163_postr_163_post ≤ 0r_163_0 + r_163_0 ≤ 0r_163_0r_163_0 ≤ 0r_124_post + r_124_post ≤ 0r_124_postr_124_post ≤ 0r_124_0 + r_124_0 ≤ 0r_124_0r_124_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_183_post + len_183_post ≤ 0len_183_postlen_183_post ≤ 0len_183_0 + len_183_0 ≤ 0len_183_0len_183_0 ≤ 0len_132_post + len_132_post ≤ 0len_132_postlen_132_post ≤ 0len_132_0 + len_132_0 ≤ 0len_132_0len_132_0 ≤ 0i_94_post + i_94_post ≤ 0i_94_posti_94_post ≤ 0i_94_0 + i_94_0 ≤ 0i_94_0i_94_0 ≤ 0i_30_post + i_30_post ≤ 0i_30_posti_30_post ≤ 0i_30_0 + i_30_0 ≤ 0i_30_0i_30_0 ≤ 0i_167_post + i_167_post ≤ 0i_167_posti_167_post ≤ 0i_167_0 + i_167_0 ≤ 0i_167_0i_167_0 ≤ 0i_108_post + i_108_post ≤ 0i_108_posti_108_post ≤ 0i_108_0 + i_108_0 ≤ 0i_108_0i_108_0 ≤ 0head_SLAM_f_26_post + head_SLAM_f_26_post ≤ 0head_SLAM_f_26_posthead_SLAM_f_26_post ≤ 0head_SLAM_f_26_1 + head_SLAM_f_26_1 ≤ 0head_SLAM_f_26_1head_SLAM_f_26_1 ≤ 0head_SLAM_f_26_0 + head_SLAM_f_26_0 ≤ 0head_SLAM_f_26_0head_SLAM_f_26_0 ≤ 0head_32_post + head_32_post ≤ 0head_32_posthead_32_post ≤ 0head_32_0 + head_32_0 ≤ 0head_32_0head_32_0 ≤ 0head_27_post + head_27_post ≤ 0head_27_posthead_27_post ≤ 0head_27_1 + head_27_1 ≤ 0head_27_1head_27_1 ≤ 0head_27_0 + head_27_0 ≤ 0head_27_0head_27_0 ≤ 0head_175_post + head_175_post ≤ 0head_175_posthead_175_post ≤ 0head_175_0 + head_175_0 ≤ 0head_175_0head_175_0 ≤ 0head_14_post + head_14_post ≤ 0head_14_posthead_14_post ≤ 0head_14_1 + head_14_1 ≤ 0head_14_1head_14_1 ≤ 0head_14_0 + head_14_0 ≤ 0head_14_0head_14_0 ≤ 0head_129_post + head_129_post ≤ 0head_129_posthead_129_post ≤ 0head_129_0 + head_129_0 ≤ 0head_129_0head_129_0 ≤ 0f_170_post + f_170_post ≤ 0f_170_postf_170_post ≤ 0f_170_0 + f_170_0 ≤ 0f_170_0f_170_0 ≤ 0ct_17_post + ct_17_post ≤ 0ct_17_postct_17_post ≤ 0ct_17_2 + ct_17_2 ≤ 0ct_17_2ct_17_2 ≤ 0ct_17_1 + ct_17_1 ≤ 0ct_17_1ct_17_1 ≤ 0ct_17_0 + ct_17_0 ≤ 0ct_17_0ct_17_0 ≤ 0a_260_post + a_260_post ≤ 0a_260_posta_260_post ≤ 0a_260_0 + a_260_0 ≤ 0a_260_0a_260_0 ≤ 0a_237_post + a_237_post ≤ 0a_237_posta_237_post ≤ 0a_237_0 + a_237_0 ≤ 0a_237_0a_237_0 ≤ 0a_215_post + a_215_post ≤ 0a_215_posta_215_post ≤ 0a_215_0 + a_215_0 ≤ 0a_215_0a_215_0 ≤ 0a_184_post + a_184_post ≤ 0a_184_posta_184_post ≤ 0a_184_0 + a_184_0 ≤ 0a_184_0a_184_0 ≤ 0a_147_post + a_147_post ≤ 0a_147_posta_147_post ≤ 0a_147_0 + a_147_0 ≤ 0a_147_0a_147_0 ≤ 0a_116_post + a_116_post ≤ 0a_116_posta_116_post ≤ 0a_116_0 + a_116_0 ≤ 0a_116_0a_116_0 ≤ 0

8 Location Addition

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

41* 90 41: y_19_post + y_19_post ≤ 0y_19_posty_19_post ≤ 0y_19_2 + y_19_2 ≤ 0y_19_2y_19_2 ≤ 0y_19_1 + y_19_1 ≤ 0y_19_1y_19_1 ≤ 0y_19_0 + y_19_0 ≤ 0y_19_0y_19_0 ≤ 0x_SLAM_f_18_post + x_SLAM_f_18_post ≤ 0x_SLAM_f_18_postx_SLAM_f_18_post ≤ 0x_SLAM_f_18_2 + x_SLAM_f_18_2 ≤ 0x_SLAM_f_18_2x_SLAM_f_18_2 ≤ 0x_SLAM_f_18_1 + x_SLAM_f_18_1 ≤ 0x_SLAM_f_18_1x_SLAM_f_18_1 ≤ 0x_SLAM_f_18_0 + x_SLAM_f_18_0 ≤ 0x_SLAM_f_18_0x_SLAM_f_18_0 ≤ 0x_20_post + x_20_post ≤ 0x_20_postx_20_post ≤ 0x_20_2 + x_20_2 ≤ 0x_20_2x_20_2 ≤ 0x_20_1 + x_20_1 ≤ 0x_20_1x_20_1 ≤ 0x_20_0 + x_20_0 ≤ 0x_20_0x_20_0 ≤ 0x_16_post + x_16_post ≤ 0x_16_postx_16_post ≤ 0x_16_1 + x_16_1 ≤ 0x_16_1x_16_1 ≤ 0x_16_0 + x_16_0 ≤ 0x_16_0x_16_0 ≤ 0tmp_34_post + tmp_34_post ≤ 0tmp_34_posttmp_34_post ≤ 0tmp_34_0 + tmp_34_0 ≤ 0tmp_34_0tmp_34_0 ≤ 0temp_35_post + temp_35_post ≤ 0temp_35_posttemp_35_post ≤ 0temp_35_0 + temp_35_0 ≤ 0temp_35_0temp_35_0 ≤ 0temp0_31_post + temp0_31_post ≤ 0temp0_31_posttemp0_31_post ≤ 0temp0_31_1 + temp0_31_1 ≤ 0temp0_31_1temp0_31_1 ≤ 0temp0_31_0 + temp0_31_0 ≤ 0temp0_31_0temp0_31_0 ≤ 0temp0_15_0 + temp0_15_0 ≤ 0temp0_15_0temp0_15_0 ≤ 0t_23_post + t_23_post ≤ 0t_23_postt_23_post ≤ 0t_23_1 + t_23_1 ≤ 0t_23_1t_23_1 ≤ 0t_23_0 + t_23_0 ≤ 0t_23_0t_23_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_post + result_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_postresult_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_2 + result_dot_nondet_sdv_special_RETURN_VALUE_13_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_2result_dot_nondet_sdv_special_RETURN_VALUE_13_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_1result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_0 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_0result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_postresult_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_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_88_post + rcd_88_post ≤ 0rcd_88_postrcd_88_post ≤ 0rcd_88_0 + rcd_88_0 ≤ 0rcd_88_0rcd_88_0 ≤ 0rcd_58_post + rcd_58_post ≤ 0rcd_58_postrcd_58_post ≤ 0rcd_58_0 + rcd_58_0 ≤ 0rcd_58_0rcd_58_0 ≤ 0r_39_post + r_39_post ≤ 0r_39_postr_39_post ≤ 0r_39_0 + r_39_0 ≤ 0r_39_0r_39_0 ≤ 0r_163_post + r_163_post ≤ 0r_163_postr_163_post ≤ 0r_163_0 + r_163_0 ≤ 0r_163_0r_163_0 ≤ 0r_124_post + r_124_post ≤ 0r_124_postr_124_post ≤ 0r_124_0 + r_124_0 ≤ 0r_124_0r_124_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_183_post + len_183_post ≤ 0len_183_postlen_183_post ≤ 0len_183_0 + len_183_0 ≤ 0len_183_0len_183_0 ≤ 0len_132_post + len_132_post ≤ 0len_132_postlen_132_post ≤ 0len_132_0 + len_132_0 ≤ 0len_132_0len_132_0 ≤ 0i_94_post + i_94_post ≤ 0i_94_posti_94_post ≤ 0i_94_0 + i_94_0 ≤ 0i_94_0i_94_0 ≤ 0i_30_post + i_30_post ≤ 0i_30_posti_30_post ≤ 0i_30_0 + i_30_0 ≤ 0i_30_0i_30_0 ≤ 0i_167_post + i_167_post ≤ 0i_167_posti_167_post ≤ 0i_167_0 + i_167_0 ≤ 0i_167_0i_167_0 ≤ 0i_108_post + i_108_post ≤ 0i_108_posti_108_post ≤ 0i_108_0 + i_108_0 ≤ 0i_108_0i_108_0 ≤ 0head_SLAM_f_26_post + head_SLAM_f_26_post ≤ 0head_SLAM_f_26_posthead_SLAM_f_26_post ≤ 0head_SLAM_f_26_1 + head_SLAM_f_26_1 ≤ 0head_SLAM_f_26_1head_SLAM_f_26_1 ≤ 0head_SLAM_f_26_0 + head_SLAM_f_26_0 ≤ 0head_SLAM_f_26_0head_SLAM_f_26_0 ≤ 0head_32_post + head_32_post ≤ 0head_32_posthead_32_post ≤ 0head_32_0 + head_32_0 ≤ 0head_32_0head_32_0 ≤ 0head_27_post + head_27_post ≤ 0head_27_posthead_27_post ≤ 0head_27_1 + head_27_1 ≤ 0head_27_1head_27_1 ≤ 0head_27_0 + head_27_0 ≤ 0head_27_0head_27_0 ≤ 0head_175_post + head_175_post ≤ 0head_175_posthead_175_post ≤ 0head_175_0 + head_175_0 ≤ 0head_175_0head_175_0 ≤ 0head_14_post + head_14_post ≤ 0head_14_posthead_14_post ≤ 0head_14_1 + head_14_1 ≤ 0head_14_1head_14_1 ≤ 0head_14_0 + head_14_0 ≤ 0head_14_0head_14_0 ≤ 0head_129_post + head_129_post ≤ 0head_129_posthead_129_post ≤ 0head_129_0 + head_129_0 ≤ 0head_129_0head_129_0 ≤ 0f_170_post + f_170_post ≤ 0f_170_postf_170_post ≤ 0f_170_0 + f_170_0 ≤ 0f_170_0f_170_0 ≤ 0ct_17_post + ct_17_post ≤ 0ct_17_postct_17_post ≤ 0ct_17_2 + ct_17_2 ≤ 0ct_17_2ct_17_2 ≤ 0ct_17_1 + ct_17_1 ≤ 0ct_17_1ct_17_1 ≤ 0ct_17_0 + ct_17_0 ≤ 0ct_17_0ct_17_0 ≤ 0a_260_post + a_260_post ≤ 0a_260_posta_260_post ≤ 0a_260_0 + a_260_0 ≤ 0a_260_0a_260_0 ≤ 0a_237_post + a_237_post ≤ 0a_237_posta_237_post ≤ 0a_237_0 + a_237_0 ≤ 0a_237_0a_237_0 ≤ 0a_215_post + a_215_post ≤ 0a_215_posta_215_post ≤ 0a_215_0 + a_215_0 ≤ 0a_215_0a_215_0 ≤ 0a_184_post + a_184_post ≤ 0a_184_posta_184_post ≤ 0a_184_0 + a_184_0 ≤ 0a_184_0a_184_0 ≤ 0a_147_post + a_147_post ≤ 0a_147_posta_147_post ≤ 0a_147_0 + a_147_0 ≤ 0a_147_0a_147_0 ≤ 0a_116_post + a_116_post ≤ 0a_116_posta_116_post ≤ 0a_116_0 + a_116_0 ≤ 0a_116_0a_116_0 ≤ 0

9 Location Addition

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

41 88 41_var_snapshot: y_19_post + y_19_post ≤ 0y_19_posty_19_post ≤ 0y_19_2 + y_19_2 ≤ 0y_19_2y_19_2 ≤ 0y_19_1 + y_19_1 ≤ 0y_19_1y_19_1 ≤ 0y_19_0 + y_19_0 ≤ 0y_19_0y_19_0 ≤ 0x_SLAM_f_18_post + x_SLAM_f_18_post ≤ 0x_SLAM_f_18_postx_SLAM_f_18_post ≤ 0x_SLAM_f_18_2 + x_SLAM_f_18_2 ≤ 0x_SLAM_f_18_2x_SLAM_f_18_2 ≤ 0x_SLAM_f_18_1 + x_SLAM_f_18_1 ≤ 0x_SLAM_f_18_1x_SLAM_f_18_1 ≤ 0x_SLAM_f_18_0 + x_SLAM_f_18_0 ≤ 0x_SLAM_f_18_0x_SLAM_f_18_0 ≤ 0x_20_post + x_20_post ≤ 0x_20_postx_20_post ≤ 0x_20_2 + x_20_2 ≤ 0x_20_2x_20_2 ≤ 0x_20_1 + x_20_1 ≤ 0x_20_1x_20_1 ≤ 0x_20_0 + x_20_0 ≤ 0x_20_0x_20_0 ≤ 0x_16_post + x_16_post ≤ 0x_16_postx_16_post ≤ 0x_16_1 + x_16_1 ≤ 0x_16_1x_16_1 ≤ 0x_16_0 + x_16_0 ≤ 0x_16_0x_16_0 ≤ 0tmp_34_post + tmp_34_post ≤ 0tmp_34_posttmp_34_post ≤ 0tmp_34_0 + tmp_34_0 ≤ 0tmp_34_0tmp_34_0 ≤ 0temp_35_post + temp_35_post ≤ 0temp_35_posttemp_35_post ≤ 0temp_35_0 + temp_35_0 ≤ 0temp_35_0temp_35_0 ≤ 0temp0_31_post + temp0_31_post ≤ 0temp0_31_posttemp0_31_post ≤ 0temp0_31_1 + temp0_31_1 ≤ 0temp0_31_1temp0_31_1 ≤ 0temp0_31_0 + temp0_31_0 ≤ 0temp0_31_0temp0_31_0 ≤ 0temp0_15_0 + temp0_15_0 ≤ 0temp0_15_0temp0_15_0 ≤ 0t_23_post + t_23_post ≤ 0t_23_postt_23_post ≤ 0t_23_1 + t_23_1 ≤ 0t_23_1t_23_1 ≤ 0t_23_0 + t_23_0 ≤ 0t_23_0t_23_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_post + result_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_postresult_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_2 + result_dot_nondet_sdv_special_RETURN_VALUE_13_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_2result_dot_nondet_sdv_special_RETURN_VALUE_13_2 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_1result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_0 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_0result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_postresult_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33_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_88_post + rcd_88_post ≤ 0rcd_88_postrcd_88_post ≤ 0rcd_88_0 + rcd_88_0 ≤ 0rcd_88_0rcd_88_0 ≤ 0rcd_58_post + rcd_58_post ≤ 0rcd_58_postrcd_58_post ≤ 0rcd_58_0 + rcd_58_0 ≤ 0rcd_58_0rcd_58_0 ≤ 0r_39_post + r_39_post ≤ 0r_39_postr_39_post ≤ 0r_39_0 + r_39_0 ≤ 0r_39_0r_39_0 ≤ 0r_163_post + r_163_post ≤ 0r_163_postr_163_post ≤ 0r_163_0 + r_163_0 ≤ 0r_163_0r_163_0 ≤ 0r_124_post + r_124_post ≤ 0r_124_postr_124_post ≤ 0r_124_0 + r_124_0 ≤ 0r_124_0r_124_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_183_post + len_183_post ≤ 0len_183_postlen_183_post ≤ 0len_183_0 + len_183_0 ≤ 0len_183_0len_183_0 ≤ 0len_132_post + len_132_post ≤ 0len_132_postlen_132_post ≤ 0len_132_0 + len_132_0 ≤ 0len_132_0len_132_0 ≤ 0i_94_post + i_94_post ≤ 0i_94_posti_94_post ≤ 0i_94_0 + i_94_0 ≤ 0i_94_0i_94_0 ≤ 0i_30_post + i_30_post ≤ 0i_30_posti_30_post ≤ 0i_30_0 + i_30_0 ≤ 0i_30_0i_30_0 ≤ 0i_167_post + i_167_post ≤ 0i_167_posti_167_post ≤ 0i_167_0 + i_167_0 ≤ 0i_167_0i_167_0 ≤ 0i_108_post + i_108_post ≤ 0i_108_posti_108_post ≤ 0i_108_0 + i_108_0 ≤ 0i_108_0i_108_0 ≤ 0head_SLAM_f_26_post + head_SLAM_f_26_post ≤ 0head_SLAM_f_26_posthead_SLAM_f_26_post ≤ 0head_SLAM_f_26_1 + head_SLAM_f_26_1 ≤ 0head_SLAM_f_26_1head_SLAM_f_26_1 ≤ 0head_SLAM_f_26_0 + head_SLAM_f_26_0 ≤ 0head_SLAM_f_26_0head_SLAM_f_26_0 ≤ 0head_32_post + head_32_post ≤ 0head_32_posthead_32_post ≤ 0head_32_0 + head_32_0 ≤ 0head_32_0head_32_0 ≤ 0head_27_post + head_27_post ≤ 0head_27_posthead_27_post ≤ 0head_27_1 + head_27_1 ≤ 0head_27_1head_27_1 ≤ 0head_27_0 + head_27_0 ≤ 0head_27_0head_27_0 ≤ 0head_175_post + head_175_post ≤ 0head_175_posthead_175_post ≤ 0head_175_0 + head_175_0 ≤ 0head_175_0head_175_0 ≤ 0head_14_post + head_14_post ≤ 0head_14_posthead_14_post ≤ 0head_14_1 + head_14_1 ≤ 0head_14_1head_14_1 ≤ 0head_14_0 + head_14_0 ≤ 0head_14_0head_14_0 ≤ 0head_129_post + head_129_post ≤ 0head_129_posthead_129_post ≤ 0head_129_0 + head_129_0 ≤ 0head_129_0head_129_0 ≤ 0f_170_post + f_170_post ≤ 0f_170_postf_170_post ≤ 0f_170_0 + f_170_0 ≤ 0f_170_0f_170_0 ≤ 0ct_17_post + ct_17_post ≤ 0ct_17_postct_17_post ≤ 0ct_17_2 + ct_17_2 ≤ 0ct_17_2ct_17_2 ≤ 0ct_17_1 + ct_17_1 ≤ 0ct_17_1ct_17_1 ≤ 0ct_17_0 + ct_17_0 ≤ 0ct_17_0ct_17_0 ≤ 0a_260_post + a_260_post ≤ 0a_260_posta_260_post ≤ 0a_260_0 + a_260_0 ≤ 0a_260_0a_260_0 ≤ 0a_237_post + a_237_post ≤ 0a_237_posta_237_post ≤ 0a_237_0 + a_237_0 ≤ 0a_237_0a_237_0 ≤ 0a_215_post + a_215_post ≤ 0a_215_posta_215_post ≤ 0a_215_0 + a_215_0 ≤ 0a_215_0a_215_0 ≤ 0a_184_post + a_184_post ≤ 0a_184_posta_184_post ≤ 0a_184_0 + a_184_0 ≤ 0a_184_0a_184_0 ≤ 0a_147_post + a_147_post ≤ 0a_147_posta_147_post ≤ 0a_147_0 + a_147_0 ≤ 0a_147_0a_147_0 ≤ 0a_116_post + a_116_post ≤ 0a_116_posta_116_post ≤ 0a_116_0 + a_116_0 ≤ 0a_116_0a_116_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 { 0, 2, 3, 4, 5, 6, 7, 8, 0_var_snapshot, 0* }.

10.1.1 Transition Removal

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

0: −2 + 10⋅a_237_0
2: −4 + 10⋅a_237_0
3: −5 + 10⋅a_237_0
4: 4 + 10⋅a_260_0
5: 3 + 10⋅a_260_0
6: 2 + 10⋅a_260_0
7: 1 + 10⋅a_260_0
8: 10⋅a_237_0
0_var_snapshot: −3 + 10⋅a_237_0
0*: −1 + 10⋅a_237_0

10.1.2 Transition Removal

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

0: −2
2: 0
3: 0
4: 4
5: 3
6: 2
7: 1
8: 0
0_var_snapshot: −3
0*: −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 73.

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 { 41, 44, 45, 46, 47, 48, 49, 41_var_snapshot, 41* }.

10.2.1 Transition Removal

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

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

10.2.2 Transition Removal

We remove transitions 90, 44, 46, 47, 48, 49, 50 using the following ranking functions, which are bounded by −4.

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

10.2.3 Transition Removal

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

41: result_dot_nondet_sdv_special_RETURN_VALUE_13_0
44: 0
45: 0
46: 0
47: 0
48: 0
49: 0
41_var_snapshot: 0
41*: 0

10.2.4 Splitting Cut-Point Transitions

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

10.2.4.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 87.

10.2.4.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 { 38, 65, 38_var_snapshot, 38* }.

10.3.1 Transition Removal

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

38: 1 − 4⋅i_30_0 + 4⋅length_29_0
65: 3 − 4⋅i_30_0 + 4⋅length_29_0
38_var_snapshot: −4⋅i_30_0 + 4⋅length_29_0
38*: 2 − 4⋅i_30_0 + 4⋅length_29_0

10.3.2 Transition Removal

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

38: 0
65: 2
38_var_snapshot: length_29_0
38*: 1

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

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