LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Invariant Updates

The following invariants are asserted.

6: i_27_post ≤ 0i_27_0 ≤ 02 − result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 02 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0
9: TRUE
10: TRUE
11: i_27_post ≤ 0i_27_post ≤ 0i_27_0 ≤ 0i_27_0 ≤ 0
12: −1 + i_27_post ≤ 01 − i_27_post ≤ 0−1 + i_27_0 ≤ 01 − i_27_0 ≤ 01 − length_25_0 ≤ 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: 2 − length_25_0 ≤ 0
19: i_27_post ≤ 0i_27_0 ≤ 02 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0a_163_0 ≤ 0
20: i_27_post ≤ 0i_27_0 ≤ 02 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0a_163_0 ≤ 0
21: i_27_post ≤ 0i_27_0 ≤ 02 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0a_163_0 ≤ 0
22: i_27_post ≤ 0i_27_0 ≤ 02 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0a_163_0 ≤ 0
23: i_27_post ≤ 0i_27_0 ≤ 02 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0a_163_0 ≤ 0
24: i_27_post ≤ 0i_27_0 ≤ 02 − result_dot_nondet_sdv_special_RETURN_VALUE_14_0 ≤ 02 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0
25: i_27_post ≤ 0i_27_0 ≤ 02 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0
26: i_27_post ≤ 0i_27_0 ≤ 02 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0
27: i_27_post ≤ 0i_27_0 ≤ 02 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0
28: i_27_post ≤ 0i_27_0 ≤ 02 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0
29: i_27_post ≤ 0i_27_0 ≤ 02 − result_dot_nondet_sdv_special_RETURN_VALUE_14_1 ≤ 0
30: 2 − length_25_0 ≤ 0
31: TRUE

The invariants are proved as follows.

IMPACT Invariant Proof

2 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
6 49 6: y_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_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_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 ≤ 0tmp_31_post + tmp_31_post ≤ 0tmp_31_posttmp_31_post ≤ 0tmp_31_0 + tmp_31_0 ≤ 0tmp_31_0tmp_31_0 ≤ 0temp_33_post + temp_33_post ≤ 0temp_33_posttemp_33_post ≤ 0temp_33_0 + temp_33_0 ≤ 0temp_33_0temp_33_0 ≤ 0temp_32_post + temp_32_post ≤ 0temp_32_posttemp_32_post ≤ 0temp_32_0 + temp_32_0 ≤ 0temp_32_0temp_32_0 ≤ 0temp0_28_post + temp0_28_post ≤ 0temp0_28_posttemp0_28_post ≤ 0temp0_28_1 + temp0_28_1 ≤ 0temp0_28_1temp0_28_1 ≤ 0temp0_28_0 + temp0_28_0 ≤ 0temp0_28_0temp0_28_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_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_30_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_postresult_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_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_67_post + rcd_67_post ≤ 0rcd_67_postrcd_67_post ≤ 0rcd_67_0 + rcd_67_0 ≤ 0rcd_67_0rcd_67_0 ≤ 0rcd_41_post + rcd_41_post ≤ 0rcd_41_postrcd_41_post ≤ 0rcd_41_0 + rcd_41_0 ≤ 0rcd_41_0rcd_41_0 ≤ 0rcd_192_post + rcd_192_post ≤ 0rcd_192_postrcd_192_post ≤ 0rcd_192_0 + rcd_192_0 ≤ 0rcd_192_0rcd_192_0 ≤ 0rcd_172_post + rcd_172_post ≤ 0rcd_172_postrcd_172_post ≤ 0rcd_172_0 + rcd_172_0 ≤ 0rcd_172_0rcd_172_0 ≤ 0rcd_168_post + rcd_168_post ≤ 0rcd_168_postrcd_168_post ≤ 0rcd_168_0 + rcd_168_0 ≤ 0rcd_168_0rcd_168_0 ≤ 0rcd_110_post + rcd_110_post ≤ 0rcd_110_postrcd_110_post ≤ 0rcd_110_0 + rcd_110_0 ≤ 0rcd_110_0rcd_110_0 ≤ 0rcd_102_post + rcd_102_post ≤ 0rcd_102_postrcd_102_post ≤ 0rcd_102_0 + rcd_102_0 ≤ 0rcd_102_0rcd_102_0 ≤ 0r_37_post + r_37_post ≤ 0r_37_postr_37_post ≤ 0r_37_0 + r_37_0 ≤ 0r_37_0r_37_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_25_post + length_25_post ≤ 0length_25_postlength_25_post ≤ 0length_25_0 + length_25_0 ≤ 0length_25_0length_25_0 ≤ 0i_27_post + i_27_post ≤ 0i_27_posti_27_post ≤ 0i_27_0 + i_27_0 ≤ 0i_27_0i_27_0 ≤ 0i_127_post + i_127_post ≤ 0i_127_posti_127_post ≤ 0i_127_0 + i_127_0 ≤ 0i_127_0i_127_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_0 + head_SLAM_f_26_0 ≤ 0head_SLAM_f_26_0head_SLAM_f_26_0 ≤ 0head_29_post + head_29_post ≤ 0head_29_posthead_29_post ≤ 0head_29_0 + head_29_0 ≤ 0head_29_0head_29_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 ≤ 0a_193_post + a_193_post ≤ 0a_193_posta_193_post ≤ 0a_193_0 + a_193_0 ≤ 0a_193_0a_193_0 ≤ 0a_163_post + a_163_post ≤ 0a_163_posta_163_post ≤ 0a_163_0 + a_163_0 ≤ 0a_163_0a_163_0 ≤ 0a_137_post + a_137_post ≤ 0a_137_posta_137_post ≤ 0a_137_0 + a_137_0 ≤ 0a_137_0a_137_0 ≤ 0
18 56 18: y_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_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_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 ≤ 0tmp_31_post + tmp_31_post ≤ 0tmp_31_posttmp_31_post ≤ 0tmp_31_0 + tmp_31_0 ≤ 0tmp_31_0tmp_31_0 ≤ 0temp_33_post + temp_33_post ≤ 0temp_33_posttemp_33_post ≤ 0temp_33_0 + temp_33_0 ≤ 0temp_33_0temp_33_0 ≤ 0temp_32_post + temp_32_post ≤ 0temp_32_posttemp_32_post ≤ 0temp_32_0 + temp_32_0 ≤ 0temp_32_0temp_32_0 ≤ 0temp0_28_post + temp0_28_post ≤ 0temp0_28_posttemp0_28_post ≤ 0temp0_28_1 + temp0_28_1 ≤ 0temp0_28_1temp0_28_1 ≤ 0temp0_28_0 + temp0_28_0 ≤ 0temp0_28_0temp0_28_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_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_30_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_postresult_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_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_67_post + rcd_67_post ≤ 0rcd_67_postrcd_67_post ≤ 0rcd_67_0 + rcd_67_0 ≤ 0rcd_67_0rcd_67_0 ≤ 0rcd_41_post + rcd_41_post ≤ 0rcd_41_postrcd_41_post ≤ 0rcd_41_0 + rcd_41_0 ≤ 0rcd_41_0rcd_41_0 ≤ 0rcd_192_post + rcd_192_post ≤ 0rcd_192_postrcd_192_post ≤ 0rcd_192_0 + rcd_192_0 ≤ 0rcd_192_0rcd_192_0 ≤ 0rcd_172_post + rcd_172_post ≤ 0rcd_172_postrcd_172_post ≤ 0rcd_172_0 + rcd_172_0 ≤ 0rcd_172_0rcd_172_0 ≤ 0rcd_168_post + rcd_168_post ≤ 0rcd_168_postrcd_168_post ≤ 0rcd_168_0 + rcd_168_0 ≤ 0rcd_168_0rcd_168_0 ≤ 0rcd_110_post + rcd_110_post ≤ 0rcd_110_postrcd_110_post ≤ 0rcd_110_0 + rcd_110_0 ≤ 0rcd_110_0rcd_110_0 ≤ 0rcd_102_post + rcd_102_post ≤ 0rcd_102_postrcd_102_post ≤ 0rcd_102_0 + rcd_102_0 ≤ 0rcd_102_0rcd_102_0 ≤ 0r_37_post + r_37_post ≤ 0r_37_postr_37_post ≤ 0r_37_0 + r_37_0 ≤ 0r_37_0r_37_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_25_post + length_25_post ≤ 0length_25_postlength_25_post ≤ 0length_25_0 + length_25_0 ≤ 0length_25_0length_25_0 ≤ 0i_27_post + i_27_post ≤ 0i_27_posti_27_post ≤ 0i_27_0 + i_27_0 ≤ 0i_27_0i_27_0 ≤ 0i_127_post + i_127_post ≤ 0i_127_posti_127_post ≤ 0i_127_0 + i_127_0 ≤ 0i_127_0i_127_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_0 + head_SLAM_f_26_0 ≤ 0head_SLAM_f_26_0head_SLAM_f_26_0 ≤ 0head_29_post + head_29_post ≤ 0head_29_posthead_29_post ≤ 0head_29_0 + head_29_0 ≤ 0head_29_0head_29_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 ≤ 0a_193_post + a_193_post ≤ 0a_193_posta_193_post ≤ 0a_193_0 + a_193_0 ≤ 0a_193_0a_193_0 ≤ 0a_163_post + a_163_post ≤ 0a_163_posta_163_post ≤ 0a_163_0 + a_163_0 ≤ 0a_163_0a_163_0 ≤ 0a_137_post + a_137_post ≤ 0a_137_posta_137_post ≤ 0a_137_0 + a_137_0 ≤ 0a_137_0a_137_0 ≤ 0
and for every transition t, a duplicate t is considered.

3 Transition Removal

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

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

4 Location Addition

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

6* 52 6: y_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_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_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 ≤ 0tmp_31_post + tmp_31_post ≤ 0tmp_31_posttmp_31_post ≤ 0tmp_31_0 + tmp_31_0 ≤ 0tmp_31_0tmp_31_0 ≤ 0temp_33_post + temp_33_post ≤ 0temp_33_posttemp_33_post ≤ 0temp_33_0 + temp_33_0 ≤ 0temp_33_0temp_33_0 ≤ 0temp_32_post + temp_32_post ≤ 0temp_32_posttemp_32_post ≤ 0temp_32_0 + temp_32_0 ≤ 0temp_32_0temp_32_0 ≤ 0temp0_28_post + temp0_28_post ≤ 0temp0_28_posttemp0_28_post ≤ 0temp0_28_1 + temp0_28_1 ≤ 0temp0_28_1temp0_28_1 ≤ 0temp0_28_0 + temp0_28_0 ≤ 0temp0_28_0temp0_28_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_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_30_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_postresult_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_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_67_post + rcd_67_post ≤ 0rcd_67_postrcd_67_post ≤ 0rcd_67_0 + rcd_67_0 ≤ 0rcd_67_0rcd_67_0 ≤ 0rcd_41_post + rcd_41_post ≤ 0rcd_41_postrcd_41_post ≤ 0rcd_41_0 + rcd_41_0 ≤ 0rcd_41_0rcd_41_0 ≤ 0rcd_192_post + rcd_192_post ≤ 0rcd_192_postrcd_192_post ≤ 0rcd_192_0 + rcd_192_0 ≤ 0rcd_192_0rcd_192_0 ≤ 0rcd_172_post + rcd_172_post ≤ 0rcd_172_postrcd_172_post ≤ 0rcd_172_0 + rcd_172_0 ≤ 0rcd_172_0rcd_172_0 ≤ 0rcd_168_post + rcd_168_post ≤ 0rcd_168_postrcd_168_post ≤ 0rcd_168_0 + rcd_168_0 ≤ 0rcd_168_0rcd_168_0 ≤ 0rcd_110_post + rcd_110_post ≤ 0rcd_110_postrcd_110_post ≤ 0rcd_110_0 + rcd_110_0 ≤ 0rcd_110_0rcd_110_0 ≤ 0rcd_102_post + rcd_102_post ≤ 0rcd_102_postrcd_102_post ≤ 0rcd_102_0 + rcd_102_0 ≤ 0rcd_102_0rcd_102_0 ≤ 0r_37_post + r_37_post ≤ 0r_37_postr_37_post ≤ 0r_37_0 + r_37_0 ≤ 0r_37_0r_37_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_25_post + length_25_post ≤ 0length_25_postlength_25_post ≤ 0length_25_0 + length_25_0 ≤ 0length_25_0length_25_0 ≤ 0i_27_post + i_27_post ≤ 0i_27_posti_27_post ≤ 0i_27_0 + i_27_0 ≤ 0i_27_0i_27_0 ≤ 0i_127_post + i_127_post ≤ 0i_127_posti_127_post ≤ 0i_127_0 + i_127_0 ≤ 0i_127_0i_127_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_0 + head_SLAM_f_26_0 ≤ 0head_SLAM_f_26_0head_SLAM_f_26_0 ≤ 0head_29_post + head_29_post ≤ 0head_29_posthead_29_post ≤ 0head_29_0 + head_29_0 ≤ 0head_29_0head_29_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 ≤ 0a_193_post + a_193_post ≤ 0a_193_posta_193_post ≤ 0a_193_0 + a_193_0 ≤ 0a_193_0a_193_0 ≤ 0a_163_post + a_163_post ≤ 0a_163_posta_163_post ≤ 0a_163_0 + a_163_0 ≤ 0a_163_0a_163_0 ≤ 0a_137_post + a_137_post ≤ 0a_137_posta_137_post ≤ 0a_137_0 + a_137_0 ≤ 0a_137_0a_137_0 ≤ 0

5 Location Addition

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

6 50 6_var_snapshot: y_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_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_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 ≤ 0tmp_31_post + tmp_31_post ≤ 0tmp_31_posttmp_31_post ≤ 0tmp_31_0 + tmp_31_0 ≤ 0tmp_31_0tmp_31_0 ≤ 0temp_33_post + temp_33_post ≤ 0temp_33_posttemp_33_post ≤ 0temp_33_0 + temp_33_0 ≤ 0temp_33_0temp_33_0 ≤ 0temp_32_post + temp_32_post ≤ 0temp_32_posttemp_32_post ≤ 0temp_32_0 + temp_32_0 ≤ 0temp_32_0temp_32_0 ≤ 0temp0_28_post + temp0_28_post ≤ 0temp0_28_posttemp0_28_post ≤ 0temp0_28_1 + temp0_28_1 ≤ 0temp0_28_1temp0_28_1 ≤ 0temp0_28_0 + temp0_28_0 ≤ 0temp0_28_0temp0_28_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_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_30_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_postresult_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_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_67_post + rcd_67_post ≤ 0rcd_67_postrcd_67_post ≤ 0rcd_67_0 + rcd_67_0 ≤ 0rcd_67_0rcd_67_0 ≤ 0rcd_41_post + rcd_41_post ≤ 0rcd_41_postrcd_41_post ≤ 0rcd_41_0 + rcd_41_0 ≤ 0rcd_41_0rcd_41_0 ≤ 0rcd_192_post + rcd_192_post ≤ 0rcd_192_postrcd_192_post ≤ 0rcd_192_0 + rcd_192_0 ≤ 0rcd_192_0rcd_192_0 ≤ 0rcd_172_post + rcd_172_post ≤ 0rcd_172_postrcd_172_post ≤ 0rcd_172_0 + rcd_172_0 ≤ 0rcd_172_0rcd_172_0 ≤ 0rcd_168_post + rcd_168_post ≤ 0rcd_168_postrcd_168_post ≤ 0rcd_168_0 + rcd_168_0 ≤ 0rcd_168_0rcd_168_0 ≤ 0rcd_110_post + rcd_110_post ≤ 0rcd_110_postrcd_110_post ≤ 0rcd_110_0 + rcd_110_0 ≤ 0rcd_110_0rcd_110_0 ≤ 0rcd_102_post + rcd_102_post ≤ 0rcd_102_postrcd_102_post ≤ 0rcd_102_0 + rcd_102_0 ≤ 0rcd_102_0rcd_102_0 ≤ 0r_37_post + r_37_post ≤ 0r_37_postr_37_post ≤ 0r_37_0 + r_37_0 ≤ 0r_37_0r_37_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_25_post + length_25_post ≤ 0length_25_postlength_25_post ≤ 0length_25_0 + length_25_0 ≤ 0length_25_0length_25_0 ≤ 0i_27_post + i_27_post ≤ 0i_27_posti_27_post ≤ 0i_27_0 + i_27_0 ≤ 0i_27_0i_27_0 ≤ 0i_127_post + i_127_post ≤ 0i_127_posti_127_post ≤ 0i_127_0 + i_127_0 ≤ 0i_127_0i_127_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_0 + head_SLAM_f_26_0 ≤ 0head_SLAM_f_26_0head_SLAM_f_26_0 ≤ 0head_29_post + head_29_post ≤ 0head_29_posthead_29_post ≤ 0head_29_0 + head_29_0 ≤ 0head_29_0head_29_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 ≤ 0a_193_post + a_193_post ≤ 0a_193_posta_193_post ≤ 0a_193_0 + a_193_0 ≤ 0a_193_0a_193_0 ≤ 0a_163_post + a_163_post ≤ 0a_163_posta_163_post ≤ 0a_163_0 + a_163_0 ≤ 0a_163_0a_163_0 ≤ 0a_137_post + a_137_post ≤ 0a_137_posta_137_post ≤ 0a_137_0 + a_137_0 ≤ 0a_137_0a_137_0 ≤ 0

6 Location Addition

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

18* 59 18: y_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_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_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 ≤ 0tmp_31_post + tmp_31_post ≤ 0tmp_31_posttmp_31_post ≤ 0tmp_31_0 + tmp_31_0 ≤ 0tmp_31_0tmp_31_0 ≤ 0temp_33_post + temp_33_post ≤ 0temp_33_posttemp_33_post ≤ 0temp_33_0 + temp_33_0 ≤ 0temp_33_0temp_33_0 ≤ 0temp_32_post + temp_32_post ≤ 0temp_32_posttemp_32_post ≤ 0temp_32_0 + temp_32_0 ≤ 0temp_32_0temp_32_0 ≤ 0temp0_28_post + temp0_28_post ≤ 0temp0_28_posttemp0_28_post ≤ 0temp0_28_1 + temp0_28_1 ≤ 0temp0_28_1temp0_28_1 ≤ 0temp0_28_0 + temp0_28_0 ≤ 0temp0_28_0temp0_28_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_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_30_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_postresult_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_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_67_post + rcd_67_post ≤ 0rcd_67_postrcd_67_post ≤ 0rcd_67_0 + rcd_67_0 ≤ 0rcd_67_0rcd_67_0 ≤ 0rcd_41_post + rcd_41_post ≤ 0rcd_41_postrcd_41_post ≤ 0rcd_41_0 + rcd_41_0 ≤ 0rcd_41_0rcd_41_0 ≤ 0rcd_192_post + rcd_192_post ≤ 0rcd_192_postrcd_192_post ≤ 0rcd_192_0 + rcd_192_0 ≤ 0rcd_192_0rcd_192_0 ≤ 0rcd_172_post + rcd_172_post ≤ 0rcd_172_postrcd_172_post ≤ 0rcd_172_0 + rcd_172_0 ≤ 0rcd_172_0rcd_172_0 ≤ 0rcd_168_post + rcd_168_post ≤ 0rcd_168_postrcd_168_post ≤ 0rcd_168_0 + rcd_168_0 ≤ 0rcd_168_0rcd_168_0 ≤ 0rcd_110_post + rcd_110_post ≤ 0rcd_110_postrcd_110_post ≤ 0rcd_110_0 + rcd_110_0 ≤ 0rcd_110_0rcd_110_0 ≤ 0rcd_102_post + rcd_102_post ≤ 0rcd_102_postrcd_102_post ≤ 0rcd_102_0 + rcd_102_0 ≤ 0rcd_102_0rcd_102_0 ≤ 0r_37_post + r_37_post ≤ 0r_37_postr_37_post ≤ 0r_37_0 + r_37_0 ≤ 0r_37_0r_37_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_25_post + length_25_post ≤ 0length_25_postlength_25_post ≤ 0length_25_0 + length_25_0 ≤ 0length_25_0length_25_0 ≤ 0i_27_post + i_27_post ≤ 0i_27_posti_27_post ≤ 0i_27_0 + i_27_0 ≤ 0i_27_0i_27_0 ≤ 0i_127_post + i_127_post ≤ 0i_127_posti_127_post ≤ 0i_127_0 + i_127_0 ≤ 0i_127_0i_127_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_0 + head_SLAM_f_26_0 ≤ 0head_SLAM_f_26_0head_SLAM_f_26_0 ≤ 0head_29_post + head_29_post ≤ 0head_29_posthead_29_post ≤ 0head_29_0 + head_29_0 ≤ 0head_29_0head_29_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 ≤ 0a_193_post + a_193_post ≤ 0a_193_posta_193_post ≤ 0a_193_0 + a_193_0 ≤ 0a_193_0a_193_0 ≤ 0a_163_post + a_163_post ≤ 0a_163_posta_163_post ≤ 0a_163_0 + a_163_0 ≤ 0a_163_0a_163_0 ≤ 0a_137_post + a_137_post ≤ 0a_137_posta_137_post ≤ 0a_137_0 + a_137_0 ≤ 0a_137_0a_137_0 ≤ 0

7 Location Addition

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

18 57 18_var_snapshot: y_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_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_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 ≤ 0tmp_31_post + tmp_31_post ≤ 0tmp_31_posttmp_31_post ≤ 0tmp_31_0 + tmp_31_0 ≤ 0tmp_31_0tmp_31_0 ≤ 0temp_33_post + temp_33_post ≤ 0temp_33_posttemp_33_post ≤ 0temp_33_0 + temp_33_0 ≤ 0temp_33_0temp_33_0 ≤ 0temp_32_post + temp_32_post ≤ 0temp_32_posttemp_32_post ≤ 0temp_32_0 + temp_32_0 ≤ 0temp_32_0temp_32_0 ≤ 0temp0_28_post + temp0_28_post ≤ 0temp0_28_posttemp0_28_post ≤ 0temp0_28_1 + temp0_28_1 ≤ 0temp0_28_1temp0_28_1 ≤ 0temp0_28_0 + temp0_28_0 ≤ 0temp0_28_0temp0_28_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_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_30_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_postresult_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_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_67_post + rcd_67_post ≤ 0rcd_67_postrcd_67_post ≤ 0rcd_67_0 + rcd_67_0 ≤ 0rcd_67_0rcd_67_0 ≤ 0rcd_41_post + rcd_41_post ≤ 0rcd_41_postrcd_41_post ≤ 0rcd_41_0 + rcd_41_0 ≤ 0rcd_41_0rcd_41_0 ≤ 0rcd_192_post + rcd_192_post ≤ 0rcd_192_postrcd_192_post ≤ 0rcd_192_0 + rcd_192_0 ≤ 0rcd_192_0rcd_192_0 ≤ 0rcd_172_post + rcd_172_post ≤ 0rcd_172_postrcd_172_post ≤ 0rcd_172_0 + rcd_172_0 ≤ 0rcd_172_0rcd_172_0 ≤ 0rcd_168_post + rcd_168_post ≤ 0rcd_168_postrcd_168_post ≤ 0rcd_168_0 + rcd_168_0 ≤ 0rcd_168_0rcd_168_0 ≤ 0rcd_110_post + rcd_110_post ≤ 0rcd_110_postrcd_110_post ≤ 0rcd_110_0 + rcd_110_0 ≤ 0rcd_110_0rcd_110_0 ≤ 0rcd_102_post + rcd_102_post ≤ 0rcd_102_postrcd_102_post ≤ 0rcd_102_0 + rcd_102_0 ≤ 0rcd_102_0rcd_102_0 ≤ 0r_37_post + r_37_post ≤ 0r_37_postr_37_post ≤ 0r_37_0 + r_37_0 ≤ 0r_37_0r_37_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_25_post + length_25_post ≤ 0length_25_postlength_25_post ≤ 0length_25_0 + length_25_0 ≤ 0length_25_0length_25_0 ≤ 0i_27_post + i_27_post ≤ 0i_27_posti_27_post ≤ 0i_27_0 + i_27_0 ≤ 0i_27_0i_27_0 ≤ 0i_127_post + i_127_post ≤ 0i_127_posti_127_post ≤ 0i_127_0 + i_127_0 ≤ 0i_127_0i_127_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_0 + head_SLAM_f_26_0 ≤ 0head_SLAM_f_26_0head_SLAM_f_26_0 ≤ 0head_29_post + head_29_post ≤ 0head_29_posthead_29_post ≤ 0head_29_0 + head_29_0 ≤ 0head_29_0head_29_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 ≤ 0a_193_post + a_193_post ≤ 0a_193_posta_193_post ≤ 0a_193_0 + a_193_0 ≤ 0a_193_0a_193_0 ≤ 0a_163_post + a_163_post ≤ 0a_163_posta_163_post ≤ 0a_163_0 + a_163_0 ≤ 0a_163_0a_163_0 ≤ 0a_137_post + a_137_post ≤ 0a_137_posta_137_post ≤ 0a_137_0 + a_137_0 ≤ 0a_137_0a_137_0 ≤ 0

8 SCC Decomposition

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

8.1 SCC Subproblem 1/2

Here we consider the SCC { 6, 19, 20, 21, 22, 23, 24, 6_var_snapshot, 6* }.

8.1.1 Transition Removal

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

6: −1 + 8⋅a_163_0
19: −2 + 8⋅a_163_0
20: −3 + 8⋅a_163_0
21: 4 + 8⋅a_193_0
22: 3 + 8⋅a_193_0
23: 2 + 8⋅a_193_0
24: 1 + 8⋅a_163_0
6_var_snapshot: −1 + 8⋅a_163_0
6*: 8⋅a_163_0

8.1.2 Transition Removal

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

6: −2
19: 0
20: 4⋅result_dot_nondet_sdv_special_RETURN_VALUE_14_1
21: 4 + result_dot_nondet_sdv_special_RETURN_VALUE_14_1
22: 2 + result_dot_nondet_sdv_special_RETURN_VALUE_14_1
23: result_dot_nondet_sdv_special_RETURN_VALUE_14_1
24: 0
6_var_snapshot: −3
6*: −1

8.1.3 Transition Removal

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

6: 0
19: 0
20: 0
21: 0
22: 0
23: 0
24: 0
6_var_snapshot: 0
6*: result_dot_nondet_sdv_special_RETURN_VALUE_14_0

8.1.4 Splitting Cut-Point Transitions

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

8.1.4.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 49.

8.1.4.1.1 Splitting Cut-Point Transitions

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

8.2 SCC Subproblem 2/2

Here we consider the SCC { 18, 30, 18_var_snapshot, 18* }.

8.2.1 Transition Removal

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

18: −2 − 4⋅i_27_0 + 4⋅length_25_0
30: −4⋅i_27_0 + 4⋅length_25_0
18_var_snapshot: −3 − 4⋅i_27_0 + 4⋅length_25_0
18*: −1 − 4⋅i_27_0 + 4⋅length_25_0

8.2.2 Transition Removal

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

18: 0
30: 2
18_var_snapshot: length_25_0
18*: 1

8.2.3 Transition Removal

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

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

8.2.4 Splitting Cut-Point Transitions

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

8.2.4.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 56.

8.2.4.1.1 Splitting Cut-Point Transitions

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

Tool configuration

T2Cert