LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Invariant Updates

The following invariants are asserted.

0: TRUE
1: head_29_post ≤ 0 ∧ − head_29_post ≤ 0 ∧ i_27_post ≤ 0 ∧ − i_27_post ≤ 0 ∧ head_29_0 ≤ 0 ∧ − head_29_0 ≤ 0 ∧ i_27_0 ≤ 0 ∧ − i_27_0 ≤ 0
2: − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ y_19_post ≤ 0 ∧ − y_19_post ≤ 0 ∧ ct_17_1 ≤ 0 ∧ − ct_17_1 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ ct_17_0 ≤ 0 ∧ − ct_17_0 ≤ 0 ∧ y_19_0 ≤ 0 ∧ − y_19_0 ≤ 0
3: TRUE
4: − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ y_19_post ≤ 0 ∧ − y_19_post ≤ 0 ∧ ct_17_1 ≤ 0 ∧ − ct_17_1 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ y_19_0 ≤ 0 ∧ − y_19_0 ≤ 0 ∧ − a_139_0 ≤ 0
5: − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ y_19_post ≤ 0 ∧ − y_19_post ≤ 0 ∧ ct_17_1 ≤ 0 ∧ − ct_17_1 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ y_19_0 ≤ 0 ∧ − y_19_0 ≤ 0 ∧ − a_139_0 ≤ 0
6: − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ y_19_post ≤ 0 ∧ − y_19_post ≤ 0 ∧ ct_17_1 ≤ 0 ∧ − ct_17_1 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ ct_17_0 ≤ 0 ∧ − ct_17_0 ≤ 0 ∧ y_19_0 ≤ 0 ∧ − y_19_0 ≤ 0 ∧ − a_139_0 ≤ 0
7: − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ y_19_post ≤ 0 ∧ − y_19_post ≤ 0 ∧ ct_17_1 ≤ 0 ∧ − ct_17_1 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ ct_17_0 ≤ 0 ∧ − ct_17_0 ≤ 0 ∧ y_19_0 ≤ 0 ∧ − y_19_0 ≤ 0 ∧ − a_139_0 ≤ 0
8: − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ y_19_post ≤ 0 ∧ − y_19_post ≤ 0 ∧ ct_17_1 ≤ 0 ∧ − ct_17_1 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ ct_17_0 ≤ 0 ∧ − ct_17_0 ≤ 0 ∧ y_19_0 ≤ 0 ∧ − y_19_0 ≤ 0 ∧ − a_139_0 ≤ 0
9: − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ y_19_post ≤ 0 ∧ − y_19_post ≤ 0 ∧ ct_17_1 ≤ 0 ∧ − ct_17_1 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ ct_17_0 ≤ 0 ∧ − ct_17_0 ≤ 0 ∧ y_19_0 ≤ 0 ∧ − y_19_0 ≤ 0
18: −1 + i_27_post ≤ 0 ∧ 1 − i_27_post ≤ 0 ∧ −1 + i_27_0 ≤ 0 ∧ 1 − i_27_0 ≤ 0 ∧ 1 − length_26_0 ≤ 0
19: y_19_post ≤ 0 ∧ − y_19_post ≤ 0 ∧ ct_17_1 ≤ 0 ∧ − ct_17_1 ≤ 0 ∧ −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ y_19_0 ≤ 0 ∧ − y_19_0 ≤ 0
20: y_19_post ≤ 0 ∧ − y_19_post ≤ 0 ∧ ct_17_1 ≤ 0 ∧ − ct_17_1 ≤ 0 ∧ −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ y_19_0 ≤ 0 ∧ − y_19_0 ≤ 0
21: −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ y_19_post ≤ 0 ∧ − y_19_post ≤ 0 ∧ ct_17_1 ≤ 0 ∧ − ct_17_1 ≤ 0 ∧ −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ ct_17_0 ≤ 0 ∧ − ct_17_0 ≤ 0 ∧ x_20_0 ≤ 0 ∧ − x_20_0 ≤ 0 ∧ y_19_0 ≤ 0 ∧ − y_19_0 ≤ 0
22: −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ y_19_post ≤ 0 ∧ − y_19_post ≤ 0 ∧ ct_17_1 ≤ 0 ∧ − ct_17_1 ≤ 0 ∧ −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ ct_17_0 ≤ 0 ∧ − ct_17_0 ≤ 0 ∧ x_20_0 ≤ 0 ∧ − x_20_0 ≤ 0 ∧ y_19_0 ≤ 0 ∧ − y_19_0 ≤ 0
23: −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0
24: 2 − length_26_0 ≤ 0
25: − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ y_19_post ≤ 0 ∧ − y_19_post ≤ 0 ∧ ct_17_1 ≤ 0 ∧ − ct_17_1 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ y_19_0 ≤ 0 ∧ − y_19_0 ≤ 0
26: − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ y_19_post ≤ 0 ∧ − y_19_post ≤ 0 ∧ ct_17_1 ≤ 0 ∧ − ct_17_1 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ y_19_0 ≤ 0 ∧ − y_19_0 ≤ 0
27: − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ y_19_post ≤ 0 ∧ − y_19_post ≤ 0 ∧ ct_17_1 ≤ 0 ∧ − ct_17_1 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ ct_17_0 ≤ 0 ∧ − ct_17_0 ≤ 0 ∧ y_19_0 ≤ 0 ∧ − y_19_0 ≤ 0
28: − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ y_19_post ≤ 0 ∧ − y_19_post ≤ 0 ∧ ct_17_1 ≤ 0 ∧ − ct_17_1 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ ct_17_0 ≤ 0 ∧ − ct_17_0 ≤ 0 ∧ y_19_0 ≤ 0 ∧ − y_19_0 ≤ 0
29: − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ y_19_post ≤ 0 ∧ − y_19_post ≤ 0 ∧ ct_17_1 ≤ 0 ∧ − ct_17_1 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ ct_17_0 ≤ 0 ∧ − ct_17_0 ≤ 0 ∧ y_19_0 ≤ 0 ∧ − y_19_0 ≤ 0
30: 2 − length_26_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:
2 36 2: − y_19_post + y_19_post ≤ 0 ∧ y_19_post − y_19_post ≤ 0 ∧ − y_19_2 + y_19_2 ≤ 0 ∧ y_19_2 − y_19_2 ≤ 0 ∧ − y_19_1 + y_19_1 ≤ 0 ∧ y_19_1 − y_19_1 ≤ 0 ∧ − y_19_0 + y_19_0 ≤ 0 ∧ y_19_0 − y_19_0 ≤ 0 ∧ − x_SLAM_f_18_post + x_SLAM_f_18_post ≤ 0 ∧ x_SLAM_f_18_post − x_SLAM_f_18_post ≤ 0 ∧ − x_SLAM_f_18_2 + x_SLAM_f_18_2 ≤ 0 ∧ x_SLAM_f_18_2 − x_SLAM_f_18_2 ≤ 0 ∧ − x_SLAM_f_18_1 + x_SLAM_f_18_1 ≤ 0 ∧ x_SLAM_f_18_1 − x_SLAM_f_18_1 ≤ 0 ∧ − x_SLAM_f_18_0 + x_SLAM_f_18_0 ≤ 0 ∧ x_SLAM_f_18_0 − x_SLAM_f_18_0 ≤ 0 ∧ − x_20_post + x_20_post ≤ 0 ∧ x_20_post − x_20_post ≤ 0 ∧ − x_20_2 + x_20_2 ≤ 0 ∧ x_20_2 − x_20_2 ≤ 0 ∧ − x_20_1 + x_20_1 ≤ 0 ∧ x_20_1 − x_20_1 ≤ 0 ∧ − x_20_0 + x_20_0 ≤ 0 ∧ x_20_0 − x_20_0 ≤ 0 ∧ − x_16_post + x_16_post ≤ 0 ∧ x_16_post − x_16_post ≤ 0 ∧ − x_16_1 + x_16_1 ≤ 0 ∧ x_16_1 − x_16_1 ≤ 0 ∧ − x_16_0 + x_16_0 ≤ 0 ∧ x_16_0 − x_16_0 ≤ 0 ∧ − tmp_31_post + tmp_31_post ≤ 0 ∧ tmp_31_post − tmp_31_post ≤ 0 ∧ − tmp_31_0 + tmp_31_0 ≤ 0 ∧ tmp_31_0 − tmp_31_0 ≤ 0 ∧ − temp_32_post + temp_32_post ≤ 0 ∧ temp_32_post − temp_32_post ≤ 0 ∧ − temp_32_0 + temp_32_0 ≤ 0 ∧ temp_32_0 − temp_32_0 ≤ 0 ∧ − temp0_28_post + temp0_28_post ≤ 0 ∧ temp0_28_post − temp0_28_post ≤ 0 ∧ − temp0_28_1 + temp0_28_1 ≤ 0 ∧ temp0_28_1 − temp0_28_1 ≤ 0 ∧ − temp0_28_0 + temp0_28_0 ≤ 0 ∧ temp0_28_0 − temp0_28_0 ≤ 0 ∧ − temp0_15_0 + temp0_15_0 ≤ 0 ∧ temp0_15_0 − temp0_15_0 ≤ 0 ∧ − t_23_post + t_23_post ≤ 0 ∧ t_23_post − t_23_post ≤ 0 ∧ − t_23_1 + t_23_1 ≤ 0 ∧ t_23_1 − t_23_1 ≤ 0 ∧ − t_23_0 + t_23_0 ≤ 0 ∧ t_23_0 − t_23_0 ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_post + result_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_post − result_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_0 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ − result_dot_SLL_create_sdv_special_RETURN_VALUE_14_post + result_dot_SLL_create_sdv_special_RETURN_VALUE_14_post ≤ 0 ∧ result_dot_SLL_create_sdv_special_RETURN_VALUE_14_post − result_dot_SLL_create_sdv_special_RETURN_VALUE_14_post ≤ 0 ∧ − result_dot_SLL_create_sdv_special_RETURN_VALUE_14_1 + result_dot_SLL_create_sdv_special_RETURN_VALUE_14_1 ≤ 0 ∧ result_dot_SLL_create_sdv_special_RETURN_VALUE_14_1 − result_dot_SLL_create_sdv_special_RETURN_VALUE_14_1 ≤ 0 ∧ − result_dot_SLL_create_sdv_special_RETURN_VALUE_14_0 + result_dot_SLL_create_sdv_special_RETURN_VALUE_14_0 ≤ 0 ∧ result_dot_SLL_create_sdv_special_RETURN_VALUE_14_0 − result_dot_SLL_create_sdv_special_RETURN_VALUE_14_0 ≤ 0 ∧ − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0 ∧ − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 ≤ 0 ∧ − result_11_post + result_11_post ≤ 0 ∧ result_11_post − result_11_post ≤ 0 ∧ − result_11_2 + result_11_2 ≤ 0 ∧ result_11_2 − result_11_2 ≤ 0 ∧ − result_11_1 + result_11_1 ≤ 0 ∧ result_11_1 − result_11_1 ≤ 0 ∧ − result_11_0 + result_11_0 ≤ 0 ∧ result_11_0 − result_11_0 ≤ 0 ∧ − rcd_84_post + rcd_84_post ≤ 0 ∧ rcd_84_post − rcd_84_post ≤ 0 ∧ − rcd_84_0 + rcd_84_0 ≤ 0 ∧ rcd_84_0 − rcd_84_0 ≤ 0 ∧ − rcd_54_post + rcd_54_post ≤ 0 ∧ rcd_54_post − rcd_54_post ≤ 0 ∧ − rcd_54_0 + rcd_54_0 ≤ 0 ∧ rcd_54_0 − rcd_54_0 ≤ 0 ∧ − r_35_post + r_35_post ≤ 0 ∧ r_35_post − r_35_post ≤ 0 ∧ − r_35_0 + r_35_0 ≤ 0 ∧ r_35_0 − r_35_0 ≤ 0 ∧ − nondet_12_post + nondet_12_post ≤ 0 ∧ nondet_12_post − nondet_12_post ≤ 0 ∧ − nondet_12_1 + nondet_12_1 ≤ 0 ∧ nondet_12_1 − nondet_12_1 ≤ 0 ∧ − nondet_12_0 + nondet_12_0 ≤ 0 ∧ nondet_12_0 − nondet_12_0 ≤ 0 ∧ − length_26_post + length_26_post ≤ 0 ∧ length_26_post − length_26_post ≤ 0 ∧ − length_26_0 + length_26_0 ≤ 0 ∧ length_26_0 − length_26_0 ≤ 0 ∧ − i_90_post + i_90_post ≤ 0 ∧ i_90_post − i_90_post ≤ 0 ∧ − i_90_0 + i_90_0 ≤ 0 ∧ i_90_0 − i_90_0 ≤ 0 ∧ − i_27_post + i_27_post ≤ 0 ∧ i_27_post − i_27_post ≤ 0 ∧ − i_27_0 + i_27_0 ≤ 0 ∧ i_27_0 − i_27_0 ≤ 0 ∧ − i_108_post + i_108_post ≤ 0 ∧ i_108_post − i_108_post ≤ 0 ∧ − i_108_0 + i_108_0 ≤ 0 ∧ i_108_0 − i_108_0 ≤ 0 ∧ − head_29_post + head_29_post ≤ 0 ∧ head_29_post − head_29_post ≤ 0 ∧ − head_29_0 + head_29_0 ≤ 0 ∧ head_29_0 − head_29_0 ≤ 0 ∧ − ct_17_post + ct_17_post ≤ 0 ∧ ct_17_post − ct_17_post ≤ 0 ∧ − ct_17_2 + ct_17_2 ≤ 0 ∧ ct_17_2 − ct_17_2 ≤ 0 ∧ − ct_17_1 + ct_17_1 ≤ 0 ∧ ct_17_1 − ct_17_1 ≤ 0 ∧ − ct_17_0 + ct_17_0 ≤ 0 ∧ ct_17_0 − ct_17_0 ≤ 0 ∧ − a_162_post + a_162_post ≤ 0 ∧ a_162_post − a_162_post ≤ 0 ∧ − a_162_0 + a_162_0 ≤ 0 ∧ a_162_0 − a_162_0 ≤ 0 ∧ − a_139_post + a_139_post ≤ 0 ∧ a_139_post − a_139_post ≤ 0 ∧ − a_139_0 + a_139_0 ≤ 0 ∧ a_139_0 − a_139_0 ≤ 0 ∧ − a_117_post + a_117_post ≤ 0 ∧ a_117_post − a_117_post ≤ 0 ∧ − a_117_0 + a_117_0 ≤ 0 ∧ a_117_0 − a_117_0 ≤ 0
24 43 24: − y_19_post + y_19_post ≤ 0 ∧ y_19_post − y_19_post ≤ 0 ∧ − y_19_2 + y_19_2 ≤ 0 ∧ y_19_2 − y_19_2 ≤ 0 ∧ − y_19_1 + y_19_1 ≤ 0 ∧ y_19_1 − y_19_1 ≤ 0 ∧ − y_19_0 + y_19_0 ≤ 0 ∧ y_19_0 − y_19_0 ≤ 0 ∧ − x_SLAM_f_18_post + x_SLAM_f_18_post ≤ 0 ∧ x_SLAM_f_18_post − x_SLAM_f_18_post ≤ 0 ∧ − x_SLAM_f_18_2 + x_SLAM_f_18_2 ≤ 0 ∧ x_SLAM_f_18_2 − x_SLAM_f_18_2 ≤ 0 ∧ − x_SLAM_f_18_1 + x_SLAM_f_18_1 ≤ 0 ∧ x_SLAM_f_18_1 − x_SLAM_f_18_1 ≤ 0 ∧ − x_SLAM_f_18_0 + x_SLAM_f_18_0 ≤ 0 ∧ x_SLAM_f_18_0 − x_SLAM_f_18_0 ≤ 0 ∧ − x_20_post + x_20_post ≤ 0 ∧ x_20_post − x_20_post ≤ 0 ∧ − x_20_2 + x_20_2 ≤ 0 ∧ x_20_2 − x_20_2 ≤ 0 ∧ − x_20_1 + x_20_1 ≤ 0 ∧ x_20_1 − x_20_1 ≤ 0 ∧ − x_20_0 + x_20_0 ≤ 0 ∧ x_20_0 − x_20_0 ≤ 0 ∧ − x_16_post + x_16_post ≤ 0 ∧ x_16_post − x_16_post ≤ 0 ∧ − x_16_1 + x_16_1 ≤ 0 ∧ x_16_1 − x_16_1 ≤ 0 ∧ − x_16_0 + x_16_0 ≤ 0 ∧ x_16_0 − x_16_0 ≤ 0 ∧ − tmp_31_post + tmp_31_post ≤ 0 ∧ tmp_31_post − tmp_31_post ≤ 0 ∧ − tmp_31_0 + tmp_31_0 ≤ 0 ∧ tmp_31_0 − tmp_31_0 ≤ 0 ∧ − temp_32_post + temp_32_post ≤ 0 ∧ temp_32_post − temp_32_post ≤ 0 ∧ − temp_32_0 + temp_32_0 ≤ 0 ∧ temp_32_0 − temp_32_0 ≤ 0 ∧ − temp0_28_post + temp0_28_post ≤ 0 ∧ temp0_28_post − temp0_28_post ≤ 0 ∧ − temp0_28_1 + temp0_28_1 ≤ 0 ∧ temp0_28_1 − temp0_28_1 ≤ 0 ∧ − temp0_28_0 + temp0_28_0 ≤ 0 ∧ temp0_28_0 − temp0_28_0 ≤ 0 ∧ − temp0_15_0 + temp0_15_0 ≤ 0 ∧ temp0_15_0 − temp0_15_0 ≤ 0 ∧ − t_23_post + t_23_post ≤ 0 ∧ t_23_post − t_23_post ≤ 0 ∧ − t_23_1 + t_23_1 ≤ 0 ∧ t_23_1 − t_23_1 ≤ 0 ∧ − t_23_0 + t_23_0 ≤ 0 ∧ t_23_0 − t_23_0 ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_post + result_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_post − result_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_0 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ − result_dot_SLL_create_sdv_special_RETURN_VALUE_14_post + result_dot_SLL_create_sdv_special_RETURN_VALUE_14_post ≤ 0 ∧ result_dot_SLL_create_sdv_special_RETURN_VALUE_14_post − result_dot_SLL_create_sdv_special_RETURN_VALUE_14_post ≤ 0 ∧ − result_dot_SLL_create_sdv_special_RETURN_VALUE_14_1 + result_dot_SLL_create_sdv_special_RETURN_VALUE_14_1 ≤ 0 ∧ result_dot_SLL_create_sdv_special_RETURN_VALUE_14_1 − result_dot_SLL_create_sdv_special_RETURN_VALUE_14_1 ≤ 0 ∧ − result_dot_SLL_create_sdv_special_RETURN_VALUE_14_0 + result_dot_SLL_create_sdv_special_RETURN_VALUE_14_0 ≤ 0 ∧ result_dot_SLL_create_sdv_special_RETURN_VALUE_14_0 − result_dot_SLL_create_sdv_special_RETURN_VALUE_14_0 ≤ 0 ∧ − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0 ∧ − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 ≤ 0 ∧ − result_11_post + result_11_post ≤ 0 ∧ result_11_post − result_11_post ≤ 0 ∧ − result_11_2 + result_11_2 ≤ 0 ∧ result_11_2 − result_11_2 ≤ 0 ∧ − result_11_1 + result_11_1 ≤ 0 ∧ result_11_1 − result_11_1 ≤ 0 ∧ − result_11_0 + result_11_0 ≤ 0 ∧ result_11_0 − result_11_0 ≤ 0 ∧ − rcd_84_post + rcd_84_post ≤ 0 ∧ rcd_84_post − rcd_84_post ≤ 0 ∧ − rcd_84_0 + rcd_84_0 ≤ 0 ∧ rcd_84_0 − rcd_84_0 ≤ 0 ∧ − rcd_54_post + rcd_54_post ≤ 0 ∧ rcd_54_post − rcd_54_post ≤ 0 ∧ − rcd_54_0 + rcd_54_0 ≤ 0 ∧ rcd_54_0 − rcd_54_0 ≤ 0 ∧ − r_35_post + r_35_post ≤ 0 ∧ r_35_post − r_35_post ≤ 0 ∧ − r_35_0 + r_35_0 ≤ 0 ∧ r_35_0 − r_35_0 ≤ 0 ∧ − nondet_12_post + nondet_12_post ≤ 0 ∧ nondet_12_post − nondet_12_post ≤ 0 ∧ − nondet_12_1 + nondet_12_1 ≤ 0 ∧ nondet_12_1 − nondet_12_1 ≤ 0 ∧ − nondet_12_0 + nondet_12_0 ≤ 0 ∧ nondet_12_0 − nondet_12_0 ≤ 0 ∧ − length_26_post + length_26_post ≤ 0 ∧ length_26_post − length_26_post ≤ 0 ∧ − length_26_0 + length_26_0 ≤ 0 ∧ length_26_0 − length_26_0 ≤ 0 ∧ − i_90_post + i_90_post ≤ 0 ∧ i_90_post − i_90_post ≤ 0 ∧ − i_90_0 + i_90_0 ≤ 0 ∧ i_90_0 − i_90_0 ≤ 0 ∧ − i_27_post + i_27_post ≤ 0 ∧ i_27_post − i_27_post ≤ 0 ∧ − i_27_0 + i_27_0 ≤ 0 ∧ i_27_0 − i_27_0 ≤ 0 ∧ − i_108_post + i_108_post ≤ 0 ∧ i_108_post − i_108_post ≤ 0 ∧ − i_108_0 + i_108_0 ≤ 0 ∧ i_108_0 − i_108_0 ≤ 0 ∧ − head_29_post + head_29_post ≤ 0 ∧ head_29_post − head_29_post ≤ 0 ∧ − head_29_0 + head_29_0 ≤ 0 ∧ head_29_0 − head_29_0 ≤ 0 ∧ − ct_17_post + ct_17_post ≤ 0 ∧ ct_17_post − ct_17_post ≤ 0 ∧ − ct_17_2 + ct_17_2 ≤ 0 ∧ ct_17_2 − ct_17_2 ≤ 0 ∧ − ct_17_1 + ct_17_1 ≤ 0 ∧ ct_17_1 − ct_17_1 ≤ 0 ∧ − ct_17_0 + ct_17_0 ≤ 0 ∧ ct_17_0 − ct_17_0 ≤ 0 ∧ − a_162_post + a_162_post ≤ 0 ∧ a_162_post − a_162_post ≤ 0 ∧ − a_162_0 + a_162_0 ≤ 0 ∧ a_162_0 − a_162_0 ≤ 0 ∧ − a_139_post + a_139_post ≤ 0 ∧ a_139_post − a_139_post ≤ 0 ∧ − a_139_0 + a_139_0 ≤ 0 ∧ a_139_0 − a_139_0 ≤ 0 ∧ − a_117_post + a_117_post ≤ 0 ∧ a_117_post − a_117_post ≤ 0 ∧ − a_117_0 + a_117_0 ≤ 0 ∧ a_117_0 − a_117_0 ≤ 0
and for every transition t, a duplicate t is considered.

3 Transition Removal

We remove transitions 0, 1, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 33, 34, 35 using the following ranking functions, which are bounded by −41.

31: 0
0: 0
1: 0
18: 0
19: 0
20: 0
21: 0
22: 0
23: 0
24: 0
30: 0
25: 0
26: 0
27: 0
28: 0
29: 0
2: 0
4: 0
5: 0
6: 0
7: 0
8: 0
9: 0
3: 0
31: −18
0: −19
1: −20
18: −21
19: −22
20: −23
21: −24
22: −25
23: −26
24: −27
30: −27
24_var_snapshot: −27
24*: −27
25: −30
26: −31
27: −32
28: −33
29: −34
2: −35
4: −35
5: −35
6: −35
7: −35
8: −35
9: −35
2_var_snapshot: −35
2*: −35
3: −39

4 Location Addition

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

2* 39 2: − y_19_post + y_19_post ≤ 0 ∧ y_19_post − y_19_post ≤ 0 ∧ − y_19_2 + y_19_2 ≤ 0 ∧ y_19_2 − y_19_2 ≤ 0 ∧ − y_19_1 + y_19_1 ≤ 0 ∧ y_19_1 − y_19_1 ≤ 0 ∧ − y_19_0 + y_19_0 ≤ 0 ∧ y_19_0 − y_19_0 ≤ 0 ∧ − x_SLAM_f_18_post + x_SLAM_f_18_post ≤ 0 ∧ x_SLAM_f_18_post − x_SLAM_f_18_post ≤ 0 ∧ − x_SLAM_f_18_2 + x_SLAM_f_18_2 ≤ 0 ∧ x_SLAM_f_18_2 − x_SLAM_f_18_2 ≤ 0 ∧ − x_SLAM_f_18_1 + x_SLAM_f_18_1 ≤ 0 ∧ x_SLAM_f_18_1 − x_SLAM_f_18_1 ≤ 0 ∧ − x_SLAM_f_18_0 + x_SLAM_f_18_0 ≤ 0 ∧ x_SLAM_f_18_0 − x_SLAM_f_18_0 ≤ 0 ∧ − x_20_post + x_20_post ≤ 0 ∧ x_20_post − x_20_post ≤ 0 ∧ − x_20_2 + x_20_2 ≤ 0 ∧ x_20_2 − x_20_2 ≤ 0 ∧ − x_20_1 + x_20_1 ≤ 0 ∧ x_20_1 − x_20_1 ≤ 0 ∧ − x_20_0 + x_20_0 ≤ 0 ∧ x_20_0 − x_20_0 ≤ 0 ∧ − x_16_post + x_16_post ≤ 0 ∧ x_16_post − x_16_post ≤ 0 ∧ − x_16_1 + x_16_1 ≤ 0 ∧ x_16_1 − x_16_1 ≤ 0 ∧ − x_16_0 + x_16_0 ≤ 0 ∧ x_16_0 − x_16_0 ≤ 0 ∧ − tmp_31_post + tmp_31_post ≤ 0 ∧ tmp_31_post − tmp_31_post ≤ 0 ∧ − tmp_31_0 + tmp_31_0 ≤ 0 ∧ tmp_31_0 − tmp_31_0 ≤ 0 ∧ − temp_32_post + temp_32_post ≤ 0 ∧ temp_32_post − temp_32_post ≤ 0 ∧ − temp_32_0 + temp_32_0 ≤ 0 ∧ temp_32_0 − temp_32_0 ≤ 0 ∧ − temp0_28_post + temp0_28_post ≤ 0 ∧ temp0_28_post − temp0_28_post ≤ 0 ∧ − temp0_28_1 + temp0_28_1 ≤ 0 ∧ temp0_28_1 − temp0_28_1 ≤ 0 ∧ − temp0_28_0 + temp0_28_0 ≤ 0 ∧ temp0_28_0 − temp0_28_0 ≤ 0 ∧ − temp0_15_0 + temp0_15_0 ≤ 0 ∧ temp0_15_0 − temp0_15_0 ≤ 0 ∧ − t_23_post + t_23_post ≤ 0 ∧ t_23_post − t_23_post ≤ 0 ∧ − t_23_1 + t_23_1 ≤ 0 ∧ t_23_1 − t_23_1 ≤ 0 ∧ − t_23_0 + t_23_0 ≤ 0 ∧ t_23_0 − t_23_0 ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_post + result_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_post − result_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_0 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ − result_dot_SLL_create_sdv_special_RETURN_VALUE_14_post + result_dot_SLL_create_sdv_special_RETURN_VALUE_14_post ≤ 0 ∧ result_dot_SLL_create_sdv_special_RETURN_VALUE_14_post − result_dot_SLL_create_sdv_special_RETURN_VALUE_14_post ≤ 0 ∧ − result_dot_SLL_create_sdv_special_RETURN_VALUE_14_1 + result_dot_SLL_create_sdv_special_RETURN_VALUE_14_1 ≤ 0 ∧ result_dot_SLL_create_sdv_special_RETURN_VALUE_14_1 − result_dot_SLL_create_sdv_special_RETURN_VALUE_14_1 ≤ 0 ∧ − result_dot_SLL_create_sdv_special_RETURN_VALUE_14_0 + result_dot_SLL_create_sdv_special_RETURN_VALUE_14_0 ≤ 0 ∧ result_dot_SLL_create_sdv_special_RETURN_VALUE_14_0 − result_dot_SLL_create_sdv_special_RETURN_VALUE_14_0 ≤ 0 ∧ − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0 ∧ − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 ≤ 0 ∧ − result_11_post + result_11_post ≤ 0 ∧ result_11_post − result_11_post ≤ 0 ∧ − result_11_2 + result_11_2 ≤ 0 ∧ result_11_2 − result_11_2 ≤ 0 ∧ − result_11_1 + result_11_1 ≤ 0 ∧ result_11_1 − result_11_1 ≤ 0 ∧ − result_11_0 + result_11_0 ≤ 0 ∧ result_11_0 − result_11_0 ≤ 0 ∧ − rcd_84_post + rcd_84_post ≤ 0 ∧ rcd_84_post − rcd_84_post ≤ 0 ∧ − rcd_84_0 + rcd_84_0 ≤ 0 ∧ rcd_84_0 − rcd_84_0 ≤ 0 ∧ − rcd_54_post + rcd_54_post ≤ 0 ∧ rcd_54_post − rcd_54_post ≤ 0 ∧ − rcd_54_0 + rcd_54_0 ≤ 0 ∧ rcd_54_0 − rcd_54_0 ≤ 0 ∧ − r_35_post + r_35_post ≤ 0 ∧ r_35_post − r_35_post ≤ 0 ∧ − r_35_0 + r_35_0 ≤ 0 ∧ r_35_0 − r_35_0 ≤ 0 ∧ − nondet_12_post + nondet_12_post ≤ 0 ∧ nondet_12_post − nondet_12_post ≤ 0 ∧ − nondet_12_1 + nondet_12_1 ≤ 0 ∧ nondet_12_1 − nondet_12_1 ≤ 0 ∧ − nondet_12_0 + nondet_12_0 ≤ 0 ∧ nondet_12_0 − nondet_12_0 ≤ 0 ∧ − length_26_post + length_26_post ≤ 0 ∧ length_26_post − length_26_post ≤ 0 ∧ − length_26_0 + length_26_0 ≤ 0 ∧ length_26_0 − length_26_0 ≤ 0 ∧ − i_90_post + i_90_post ≤ 0 ∧ i_90_post − i_90_post ≤ 0 ∧ − i_90_0 + i_90_0 ≤ 0 ∧ i_90_0 − i_90_0 ≤ 0 ∧ − i_27_post + i_27_post ≤ 0 ∧ i_27_post − i_27_post ≤ 0 ∧ − i_27_0 + i_27_0 ≤ 0 ∧ i_27_0 − i_27_0 ≤ 0 ∧ − i_108_post + i_108_post ≤ 0 ∧ i_108_post − i_108_post ≤ 0 ∧ − i_108_0 + i_108_0 ≤ 0 ∧ i_108_0 − i_108_0 ≤ 0 ∧ − head_29_post + head_29_post ≤ 0 ∧ head_29_post − head_29_post ≤ 0 ∧ − head_29_0 + head_29_0 ≤ 0 ∧ head_29_0 − head_29_0 ≤ 0 ∧ − ct_17_post + ct_17_post ≤ 0 ∧ ct_17_post − ct_17_post ≤ 0 ∧ − ct_17_2 + ct_17_2 ≤ 0 ∧ ct_17_2 − ct_17_2 ≤ 0 ∧ − ct_17_1 + ct_17_1 ≤ 0 ∧ ct_17_1 − ct_17_1 ≤ 0 ∧ − ct_17_0 + ct_17_0 ≤ 0 ∧ ct_17_0 − ct_17_0 ≤ 0 ∧ − a_162_post + a_162_post ≤ 0 ∧ a_162_post − a_162_post ≤ 0 ∧ − a_162_0 + a_162_0 ≤ 0 ∧ a_162_0 − a_162_0 ≤ 0 ∧ − a_139_post + a_139_post ≤ 0 ∧ a_139_post − a_139_post ≤ 0 ∧ − a_139_0 + a_139_0 ≤ 0 ∧ a_139_0 − a_139_0 ≤ 0 ∧ − a_117_post + a_117_post ≤ 0 ∧ a_117_post − a_117_post ≤ 0 ∧ − a_117_0 + a_117_0 ≤ 0 ∧ a_117_0 − a_117_0 ≤ 0

5 Location Addition

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

2 37 2_var_snapshot: − y_19_post + y_19_post ≤ 0 ∧ y_19_post − y_19_post ≤ 0 ∧ − y_19_2 + y_19_2 ≤ 0 ∧ y_19_2 − y_19_2 ≤ 0 ∧ − y_19_1 + y_19_1 ≤ 0 ∧ y_19_1 − y_19_1 ≤ 0 ∧ − y_19_0 + y_19_0 ≤ 0 ∧ y_19_0 − y_19_0 ≤ 0 ∧ − x_SLAM_f_18_post + x_SLAM_f_18_post ≤ 0 ∧ x_SLAM_f_18_post − x_SLAM_f_18_post ≤ 0 ∧ − x_SLAM_f_18_2 + x_SLAM_f_18_2 ≤ 0 ∧ x_SLAM_f_18_2 − x_SLAM_f_18_2 ≤ 0 ∧ − x_SLAM_f_18_1 + x_SLAM_f_18_1 ≤ 0 ∧ x_SLAM_f_18_1 − x_SLAM_f_18_1 ≤ 0 ∧ − x_SLAM_f_18_0 + x_SLAM_f_18_0 ≤ 0 ∧ x_SLAM_f_18_0 − x_SLAM_f_18_0 ≤ 0 ∧ − x_20_post + x_20_post ≤ 0 ∧ x_20_post − x_20_post ≤ 0 ∧ − x_20_2 + x_20_2 ≤ 0 ∧ x_20_2 − x_20_2 ≤ 0 ∧ − x_20_1 + x_20_1 ≤ 0 ∧ x_20_1 − x_20_1 ≤ 0 ∧ − x_20_0 + x_20_0 ≤ 0 ∧ x_20_0 − x_20_0 ≤ 0 ∧ − x_16_post + x_16_post ≤ 0 ∧ x_16_post − x_16_post ≤ 0 ∧ − x_16_1 + x_16_1 ≤ 0 ∧ x_16_1 − x_16_1 ≤ 0 ∧ − x_16_0 + x_16_0 ≤ 0 ∧ x_16_0 − x_16_0 ≤ 0 ∧ − tmp_31_post + tmp_31_post ≤ 0 ∧ tmp_31_post − tmp_31_post ≤ 0 ∧ − tmp_31_0 + tmp_31_0 ≤ 0 ∧ tmp_31_0 − tmp_31_0 ≤ 0 ∧ − temp_32_post + temp_32_post ≤ 0 ∧ temp_32_post − temp_32_post ≤ 0 ∧ − temp_32_0 + temp_32_0 ≤ 0 ∧ temp_32_0 − temp_32_0 ≤ 0 ∧ − temp0_28_post + temp0_28_post ≤ 0 ∧ temp0_28_post − temp0_28_post ≤ 0 ∧ − temp0_28_1 + temp0_28_1 ≤ 0 ∧ temp0_28_1 − temp0_28_1 ≤ 0 ∧ − temp0_28_0 + temp0_28_0 ≤ 0 ∧ temp0_28_0 − temp0_28_0 ≤ 0 ∧ − temp0_15_0 + temp0_15_0 ≤ 0 ∧ temp0_15_0 − temp0_15_0 ≤ 0 ∧ − t_23_post + t_23_post ≤ 0 ∧ t_23_post − t_23_post ≤ 0 ∧ − t_23_1 + t_23_1 ≤ 0 ∧ t_23_1 − t_23_1 ≤ 0 ∧ − t_23_0 + t_23_0 ≤ 0 ∧ t_23_0 − t_23_0 ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_post + result_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_post − result_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_0 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ − result_dot_SLL_create_sdv_special_RETURN_VALUE_14_post + result_dot_SLL_create_sdv_special_RETURN_VALUE_14_post ≤ 0 ∧ result_dot_SLL_create_sdv_special_RETURN_VALUE_14_post − result_dot_SLL_create_sdv_special_RETURN_VALUE_14_post ≤ 0 ∧ − result_dot_SLL_create_sdv_special_RETURN_VALUE_14_1 + result_dot_SLL_create_sdv_special_RETURN_VALUE_14_1 ≤ 0 ∧ result_dot_SLL_create_sdv_special_RETURN_VALUE_14_1 − result_dot_SLL_create_sdv_special_RETURN_VALUE_14_1 ≤ 0 ∧ − result_dot_SLL_create_sdv_special_RETURN_VALUE_14_0 + result_dot_SLL_create_sdv_special_RETURN_VALUE_14_0 ≤ 0 ∧ result_dot_SLL_create_sdv_special_RETURN_VALUE_14_0 − result_dot_SLL_create_sdv_special_RETURN_VALUE_14_0 ≤ 0 ∧ − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0 ∧ − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 ≤ 0 ∧ − result_11_post + result_11_post ≤ 0 ∧ result_11_post − result_11_post ≤ 0 ∧ − result_11_2 + result_11_2 ≤ 0 ∧ result_11_2 − result_11_2 ≤ 0 ∧ − result_11_1 + result_11_1 ≤ 0 ∧ result_11_1 − result_11_1 ≤ 0 ∧ − result_11_0 + result_11_0 ≤ 0 ∧ result_11_0 − result_11_0 ≤ 0 ∧ − rcd_84_post + rcd_84_post ≤ 0 ∧ rcd_84_post − rcd_84_post ≤ 0 ∧ − rcd_84_0 + rcd_84_0 ≤ 0 ∧ rcd_84_0 − rcd_84_0 ≤ 0 ∧ − rcd_54_post + rcd_54_post ≤ 0 ∧ rcd_54_post − rcd_54_post ≤ 0 ∧ − rcd_54_0 + rcd_54_0 ≤ 0 ∧ rcd_54_0 − rcd_54_0 ≤ 0 ∧ − r_35_post + r_35_post ≤ 0 ∧ r_35_post − r_35_post ≤ 0 ∧ − r_35_0 + r_35_0 ≤ 0 ∧ r_35_0 − r_35_0 ≤ 0 ∧ − nondet_12_post + nondet_12_post ≤ 0 ∧ nondet_12_post − nondet_12_post ≤ 0 ∧ − nondet_12_1 + nondet_12_1 ≤ 0 ∧ nondet_12_1 − nondet_12_1 ≤ 0 ∧ − nondet_12_0 + nondet_12_0 ≤ 0 ∧ nondet_12_0 − nondet_12_0 ≤ 0 ∧ − length_26_post + length_26_post ≤ 0 ∧ length_26_post − length_26_post ≤ 0 ∧ − length_26_0 + length_26_0 ≤ 0 ∧ length_26_0 − length_26_0 ≤ 0 ∧ − i_90_post + i_90_post ≤ 0 ∧ i_90_post − i_90_post ≤ 0 ∧ − i_90_0 + i_90_0 ≤ 0 ∧ i_90_0 − i_90_0 ≤ 0 ∧ − i_27_post + i_27_post ≤ 0 ∧ i_27_post − i_27_post ≤ 0 ∧ − i_27_0 + i_27_0 ≤ 0 ∧ i_27_0 − i_27_0 ≤ 0 ∧ − i_108_post + i_108_post ≤ 0 ∧ i_108_post − i_108_post ≤ 0 ∧ − i_108_0 + i_108_0 ≤ 0 ∧ i_108_0 − i_108_0 ≤ 0 ∧ − head_29_post + head_29_post ≤ 0 ∧ head_29_post − head_29_post ≤ 0 ∧ − head_29_0 + head_29_0 ≤ 0 ∧ head_29_0 − head_29_0 ≤ 0 ∧ − ct_17_post + ct_17_post ≤ 0 ∧ ct_17_post − ct_17_post ≤ 0 ∧ − ct_17_2 + ct_17_2 ≤ 0 ∧ ct_17_2 − ct_17_2 ≤ 0 ∧ − ct_17_1 + ct_17_1 ≤ 0 ∧ ct_17_1 − ct_17_1 ≤ 0 ∧ − ct_17_0 + ct_17_0 ≤ 0 ∧ ct_17_0 − ct_17_0 ≤ 0 ∧ − a_162_post + a_162_post ≤ 0 ∧ a_162_post − a_162_post ≤ 0 ∧ − a_162_0 + a_162_0 ≤ 0 ∧ a_162_0 − a_162_0 ≤ 0 ∧ − a_139_post + a_139_post ≤ 0 ∧ a_139_post − a_139_post ≤ 0 ∧ − a_139_0 + a_139_0 ≤ 0 ∧ a_139_0 − a_139_0 ≤ 0 ∧ − a_117_post + a_117_post ≤ 0 ∧ a_117_post − a_117_post ≤ 0 ∧ − a_117_0 + a_117_0 ≤ 0 ∧ a_117_0 − a_117_0 ≤ 0

6 Location Addition

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

24* 46 24: − y_19_post + y_19_post ≤ 0 ∧ y_19_post − y_19_post ≤ 0 ∧ − y_19_2 + y_19_2 ≤ 0 ∧ y_19_2 − y_19_2 ≤ 0 ∧ − y_19_1 + y_19_1 ≤ 0 ∧ y_19_1 − y_19_1 ≤ 0 ∧ − y_19_0 + y_19_0 ≤ 0 ∧ y_19_0 − y_19_0 ≤ 0 ∧ − x_SLAM_f_18_post + x_SLAM_f_18_post ≤ 0 ∧ x_SLAM_f_18_post − x_SLAM_f_18_post ≤ 0 ∧ − x_SLAM_f_18_2 + x_SLAM_f_18_2 ≤ 0 ∧ x_SLAM_f_18_2 − x_SLAM_f_18_2 ≤ 0 ∧ − x_SLAM_f_18_1 + x_SLAM_f_18_1 ≤ 0 ∧ x_SLAM_f_18_1 − x_SLAM_f_18_1 ≤ 0 ∧ − x_SLAM_f_18_0 + x_SLAM_f_18_0 ≤ 0 ∧ x_SLAM_f_18_0 − x_SLAM_f_18_0 ≤ 0 ∧ − x_20_post + x_20_post ≤ 0 ∧ x_20_post − x_20_post ≤ 0 ∧ − x_20_2 + x_20_2 ≤ 0 ∧ x_20_2 − x_20_2 ≤ 0 ∧ − x_20_1 + x_20_1 ≤ 0 ∧ x_20_1 − x_20_1 ≤ 0 ∧ − x_20_0 + x_20_0 ≤ 0 ∧ x_20_0 − x_20_0 ≤ 0 ∧ − x_16_post + x_16_post ≤ 0 ∧ x_16_post − x_16_post ≤ 0 ∧ − x_16_1 + x_16_1 ≤ 0 ∧ x_16_1 − x_16_1 ≤ 0 ∧ − x_16_0 + x_16_0 ≤ 0 ∧ x_16_0 − x_16_0 ≤ 0 ∧ − tmp_31_post + tmp_31_post ≤ 0 ∧ tmp_31_post − tmp_31_post ≤ 0 ∧ − tmp_31_0 + tmp_31_0 ≤ 0 ∧ tmp_31_0 − tmp_31_0 ≤ 0 ∧ − temp_32_post + temp_32_post ≤ 0 ∧ temp_32_post − temp_32_post ≤ 0 ∧ − temp_32_0 + temp_32_0 ≤ 0 ∧ temp_32_0 − temp_32_0 ≤ 0 ∧ − temp0_28_post + temp0_28_post ≤ 0 ∧ temp0_28_post − temp0_28_post ≤ 0 ∧ − temp0_28_1 + temp0_28_1 ≤ 0 ∧ temp0_28_1 − temp0_28_1 ≤ 0 ∧ − temp0_28_0 + temp0_28_0 ≤ 0 ∧ temp0_28_0 − temp0_28_0 ≤ 0 ∧ − temp0_15_0 + temp0_15_0 ≤ 0 ∧ temp0_15_0 − temp0_15_0 ≤ 0 ∧ − t_23_post + t_23_post ≤ 0 ∧ t_23_post − t_23_post ≤ 0 ∧ − t_23_1 + t_23_1 ≤ 0 ∧ t_23_1 − t_23_1 ≤ 0 ∧ − t_23_0 + t_23_0 ≤ 0 ∧ t_23_0 − t_23_0 ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_post + result_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_post − result_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_0 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ − result_dot_SLL_create_sdv_special_RETURN_VALUE_14_post + result_dot_SLL_create_sdv_special_RETURN_VALUE_14_post ≤ 0 ∧ result_dot_SLL_create_sdv_special_RETURN_VALUE_14_post − result_dot_SLL_create_sdv_special_RETURN_VALUE_14_post ≤ 0 ∧ − result_dot_SLL_create_sdv_special_RETURN_VALUE_14_1 + result_dot_SLL_create_sdv_special_RETURN_VALUE_14_1 ≤ 0 ∧ result_dot_SLL_create_sdv_special_RETURN_VALUE_14_1 − result_dot_SLL_create_sdv_special_RETURN_VALUE_14_1 ≤ 0 ∧ − result_dot_SLL_create_sdv_special_RETURN_VALUE_14_0 + result_dot_SLL_create_sdv_special_RETURN_VALUE_14_0 ≤ 0 ∧ result_dot_SLL_create_sdv_special_RETURN_VALUE_14_0 − result_dot_SLL_create_sdv_special_RETURN_VALUE_14_0 ≤ 0 ∧ − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0 ∧ − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 ≤ 0 ∧ − result_11_post + result_11_post ≤ 0 ∧ result_11_post − result_11_post ≤ 0 ∧ − result_11_2 + result_11_2 ≤ 0 ∧ result_11_2 − result_11_2 ≤ 0 ∧ − result_11_1 + result_11_1 ≤ 0 ∧ result_11_1 − result_11_1 ≤ 0 ∧ − result_11_0 + result_11_0 ≤ 0 ∧ result_11_0 − result_11_0 ≤ 0 ∧ − rcd_84_post + rcd_84_post ≤ 0 ∧ rcd_84_post − rcd_84_post ≤ 0 ∧ − rcd_84_0 + rcd_84_0 ≤ 0 ∧ rcd_84_0 − rcd_84_0 ≤ 0 ∧ − rcd_54_post + rcd_54_post ≤ 0 ∧ rcd_54_post − rcd_54_post ≤ 0 ∧ − rcd_54_0 + rcd_54_0 ≤ 0 ∧ rcd_54_0 − rcd_54_0 ≤ 0 ∧ − r_35_post + r_35_post ≤ 0 ∧ r_35_post − r_35_post ≤ 0 ∧ − r_35_0 + r_35_0 ≤ 0 ∧ r_35_0 − r_35_0 ≤ 0 ∧ − nondet_12_post + nondet_12_post ≤ 0 ∧ nondet_12_post − nondet_12_post ≤ 0 ∧ − nondet_12_1 + nondet_12_1 ≤ 0 ∧ nondet_12_1 − nondet_12_1 ≤ 0 ∧ − nondet_12_0 + nondet_12_0 ≤ 0 ∧ nondet_12_0 − nondet_12_0 ≤ 0 ∧ − length_26_post + length_26_post ≤ 0 ∧ length_26_post − length_26_post ≤ 0 ∧ − length_26_0 + length_26_0 ≤ 0 ∧ length_26_0 − length_26_0 ≤ 0 ∧ − i_90_post + i_90_post ≤ 0 ∧ i_90_post − i_90_post ≤ 0 ∧ − i_90_0 + i_90_0 ≤ 0 ∧ i_90_0 − i_90_0 ≤ 0 ∧ − i_27_post + i_27_post ≤ 0 ∧ i_27_post − i_27_post ≤ 0 ∧ − i_27_0 + i_27_0 ≤ 0 ∧ i_27_0 − i_27_0 ≤ 0 ∧ − i_108_post + i_108_post ≤ 0 ∧ i_108_post − i_108_post ≤ 0 ∧ − i_108_0 + i_108_0 ≤ 0 ∧ i_108_0 − i_108_0 ≤ 0 ∧ − head_29_post + head_29_post ≤ 0 ∧ head_29_post − head_29_post ≤ 0 ∧ − head_29_0 + head_29_0 ≤ 0 ∧ head_29_0 − head_29_0 ≤ 0 ∧ − ct_17_post + ct_17_post ≤ 0 ∧ ct_17_post − ct_17_post ≤ 0 ∧ − ct_17_2 + ct_17_2 ≤ 0 ∧ ct_17_2 − ct_17_2 ≤ 0 ∧ − ct_17_1 + ct_17_1 ≤ 0 ∧ ct_17_1 − ct_17_1 ≤ 0 ∧ − ct_17_0 + ct_17_0 ≤ 0 ∧ ct_17_0 − ct_17_0 ≤ 0 ∧ − a_162_post + a_162_post ≤ 0 ∧ a_162_post − a_162_post ≤ 0 ∧ − a_162_0 + a_162_0 ≤ 0 ∧ a_162_0 − a_162_0 ≤ 0 ∧ − a_139_post + a_139_post ≤ 0 ∧ a_139_post − a_139_post ≤ 0 ∧ − a_139_0 + a_139_0 ≤ 0 ∧ a_139_0 − a_139_0 ≤ 0 ∧ − a_117_post + a_117_post ≤ 0 ∧ a_117_post − a_117_post ≤ 0 ∧ − a_117_0 + a_117_0 ≤ 0 ∧ a_117_0 − a_117_0 ≤ 0

7 Location Addition

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

24 44 24_var_snapshot: − y_19_post + y_19_post ≤ 0 ∧ y_19_post − y_19_post ≤ 0 ∧ − y_19_2 + y_19_2 ≤ 0 ∧ y_19_2 − y_19_2 ≤ 0 ∧ − y_19_1 + y_19_1 ≤ 0 ∧ y_19_1 − y_19_1 ≤ 0 ∧ − y_19_0 + y_19_0 ≤ 0 ∧ y_19_0 − y_19_0 ≤ 0 ∧ − x_SLAM_f_18_post + x_SLAM_f_18_post ≤ 0 ∧ x_SLAM_f_18_post − x_SLAM_f_18_post ≤ 0 ∧ − x_SLAM_f_18_2 + x_SLAM_f_18_2 ≤ 0 ∧ x_SLAM_f_18_2 − x_SLAM_f_18_2 ≤ 0 ∧ − x_SLAM_f_18_1 + x_SLAM_f_18_1 ≤ 0 ∧ x_SLAM_f_18_1 − x_SLAM_f_18_1 ≤ 0 ∧ − x_SLAM_f_18_0 + x_SLAM_f_18_0 ≤ 0 ∧ x_SLAM_f_18_0 − x_SLAM_f_18_0 ≤ 0 ∧ − x_20_post + x_20_post ≤ 0 ∧ x_20_post − x_20_post ≤ 0 ∧ − x_20_2 + x_20_2 ≤ 0 ∧ x_20_2 − x_20_2 ≤ 0 ∧ − x_20_1 + x_20_1 ≤ 0 ∧ x_20_1 − x_20_1 ≤ 0 ∧ − x_20_0 + x_20_0 ≤ 0 ∧ x_20_0 − x_20_0 ≤ 0 ∧ − x_16_post + x_16_post ≤ 0 ∧ x_16_post − x_16_post ≤ 0 ∧ − x_16_1 + x_16_1 ≤ 0 ∧ x_16_1 − x_16_1 ≤ 0 ∧ − x_16_0 + x_16_0 ≤ 0 ∧ x_16_0 − x_16_0 ≤ 0 ∧ − tmp_31_post + tmp_31_post ≤ 0 ∧ tmp_31_post − tmp_31_post ≤ 0 ∧ − tmp_31_0 + tmp_31_0 ≤ 0 ∧ tmp_31_0 − tmp_31_0 ≤ 0 ∧ − temp_32_post + temp_32_post ≤ 0 ∧ temp_32_post − temp_32_post ≤ 0 ∧ − temp_32_0 + temp_32_0 ≤ 0 ∧ temp_32_0 − temp_32_0 ≤ 0 ∧ − temp0_28_post + temp0_28_post ≤ 0 ∧ temp0_28_post − temp0_28_post ≤ 0 ∧ − temp0_28_1 + temp0_28_1 ≤ 0 ∧ temp0_28_1 − temp0_28_1 ≤ 0 ∧ − temp0_28_0 + temp0_28_0 ≤ 0 ∧ temp0_28_0 − temp0_28_0 ≤ 0 ∧ − temp0_15_0 + temp0_15_0 ≤ 0 ∧ temp0_15_0 − temp0_15_0 ≤ 0 ∧ − t_23_post + t_23_post ≤ 0 ∧ t_23_post − t_23_post ≤ 0 ∧ − t_23_1 + t_23_1 ≤ 0 ∧ t_23_1 − t_23_1 ≤ 0 ∧ − t_23_0 + t_23_0 ≤ 0 ∧ t_23_0 − t_23_0 ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_post + result_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_post − result_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ result_dot_nondet_sdv_special_RETURN_VALUE_13_0 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ − result_dot_SLL_create_sdv_special_RETURN_VALUE_14_post + result_dot_SLL_create_sdv_special_RETURN_VALUE_14_post ≤ 0 ∧ result_dot_SLL_create_sdv_special_RETURN_VALUE_14_post − result_dot_SLL_create_sdv_special_RETURN_VALUE_14_post ≤ 0 ∧ − result_dot_SLL_create_sdv_special_RETURN_VALUE_14_1 + result_dot_SLL_create_sdv_special_RETURN_VALUE_14_1 ≤ 0 ∧ result_dot_SLL_create_sdv_special_RETURN_VALUE_14_1 − result_dot_SLL_create_sdv_special_RETURN_VALUE_14_1 ≤ 0 ∧ − result_dot_SLL_create_sdv_special_RETURN_VALUE_14_0 + result_dot_SLL_create_sdv_special_RETURN_VALUE_14_0 ≤ 0 ∧ result_dot_SLL_create_sdv_special_RETURN_VALUE_14_0 − result_dot_SLL_create_sdv_special_RETURN_VALUE_14_0 ≤ 0 ∧ − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0 ∧ − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 ≤ 0 ∧ result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 − result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 ≤ 0 ∧ − result_11_post + result_11_post ≤ 0 ∧ result_11_post − result_11_post ≤ 0 ∧ − result_11_2 + result_11_2 ≤ 0 ∧ result_11_2 − result_11_2 ≤ 0 ∧ − result_11_1 + result_11_1 ≤ 0 ∧ result_11_1 − result_11_1 ≤ 0 ∧ − result_11_0 + result_11_0 ≤ 0 ∧ result_11_0 − result_11_0 ≤ 0 ∧ − rcd_84_post + rcd_84_post ≤ 0 ∧ rcd_84_post − rcd_84_post ≤ 0 ∧ − rcd_84_0 + rcd_84_0 ≤ 0 ∧ rcd_84_0 − rcd_84_0 ≤ 0 ∧ − rcd_54_post + rcd_54_post ≤ 0 ∧ rcd_54_post − rcd_54_post ≤ 0 ∧ − rcd_54_0 + rcd_54_0 ≤ 0 ∧ rcd_54_0 − rcd_54_0 ≤ 0 ∧ − r_35_post + r_35_post ≤ 0 ∧ r_35_post − r_35_post ≤ 0 ∧ − r_35_0 + r_35_0 ≤ 0 ∧ r_35_0 − r_35_0 ≤ 0 ∧ − nondet_12_post + nondet_12_post ≤ 0 ∧ nondet_12_post − nondet_12_post ≤ 0 ∧ − nondet_12_1 + nondet_12_1 ≤ 0 ∧ nondet_12_1 − nondet_12_1 ≤ 0 ∧ − nondet_12_0 + nondet_12_0 ≤ 0 ∧ nondet_12_0 − nondet_12_0 ≤ 0 ∧ − length_26_post + length_26_post ≤ 0 ∧ length_26_post − length_26_post ≤ 0 ∧ − length_26_0 + length_26_0 ≤ 0 ∧ length_26_0 − length_26_0 ≤ 0 ∧ − i_90_post + i_90_post ≤ 0 ∧ i_90_post − i_90_post ≤ 0 ∧ − i_90_0 + i_90_0 ≤ 0 ∧ i_90_0 − i_90_0 ≤ 0 ∧ − i_27_post + i_27_post ≤ 0 ∧ i_27_post − i_27_post ≤ 0 ∧ − i_27_0 + i_27_0 ≤ 0 ∧ i_27_0 − i_27_0 ≤ 0 ∧ − i_108_post + i_108_post ≤ 0 ∧ i_108_post − i_108_post ≤ 0 ∧ − i_108_0 + i_108_0 ≤ 0 ∧ i_108_0 − i_108_0 ≤ 0 ∧ − head_29_post + head_29_post ≤ 0 ∧ head_29_post − head_29_post ≤ 0 ∧ − head_29_0 + head_29_0 ≤ 0 ∧ head_29_0 − head_29_0 ≤ 0 ∧ − ct_17_post + ct_17_post ≤ 0 ∧ ct_17_post − ct_17_post ≤ 0 ∧ − ct_17_2 + ct_17_2 ≤ 0 ∧ ct_17_2 − ct_17_2 ≤ 0 ∧ − ct_17_1 + ct_17_1 ≤ 0 ∧ ct_17_1 − ct_17_1 ≤ 0 ∧ − ct_17_0 + ct_17_0 ≤ 0 ∧ ct_17_0 − ct_17_0 ≤ 0 ∧ − a_162_post + a_162_post ≤ 0 ∧ a_162_post − a_162_post ≤ 0 ∧ − a_162_0 + a_162_0 ≤ 0 ∧ a_162_0 − a_162_0 ≤ 0 ∧ − a_139_post + a_139_post ≤ 0 ∧ a_139_post − a_139_post ≤ 0 ∧ − a_139_0 + a_139_0 ≤ 0 ∧ a_139_0 − a_139_0 ≤ 0 ∧ − a_117_post + a_117_post ≤ 0 ∧ a_117_post − a_117_post ≤ 0 ∧ − a_117_0 + a_117_0 ≤ 0 ∧ a_117_0 − a_117_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 { 2, 4, 5, 6, 7, 8, 9, 2_var_snapshot, 2* }.

8.1.1 Transition Removal

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

2: −1 + 7⋅a_139_0
4: −2 + 7⋅a_139_0
5: −3 + 7⋅a_139_0
6: 4 + 7⋅a_162_0
7: 3 + 7⋅a_162_0
8: 2 + 7⋅a_162_0
9: 1 + 7⋅a_139_0
2_var_snapshot: −1 + 7⋅a_139_0
2*: 7⋅a_139_0

8.1.2 Transition Removal

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

2: −1
4: −3
5: 5⋅result_dot_nondet_sdv_special_RETURN_VALUE_13_1
6: 4 + 2⋅result_dot_nondet_sdv_special_RETURN_VALUE_13_1
7: 2 + 2⋅result_dot_nondet_sdv_special_RETURN_VALUE_13_1
8: 2⋅result_dot_nondet_sdv_special_RETURN_VALUE_13_1
9: 2
2_var_snapshot: −2
2*: 0

8.1.3 Transition Removal

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

2: 0
4: 0
5: result_dot_nondet_sdv_special_RETURN_VALUE_13_1
6: 0
7: 0
8: 0
9: 0
2_var_snapshot: 0
2*: 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 36.

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 { 24, 30, 24_var_snapshot, 24* }.

8.2.1 Transition Removal

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

24: −1 − 4⋅i_27_0 + 4⋅length_26_0
30: 1 − 4⋅i_27_0 + 4⋅length_26_0
24_var_snapshot: −2 − 4⋅i_27_0 + 4⋅length_26_0
24*: −4⋅i_27_0 + 4⋅length_26_0

8.2.2 Transition Removal

We remove transitions 44, 46, 32 using the following ranking functions, which are bounded by −1.

24: 0
30: 2⋅length_26_0
24_var_snapshot: −1
24*: length_26_0

8.2.3 Splitting Cut-Point Transitions

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

8.2.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 43.

8.2.3.1.1 Splitting Cut-Point Transitions

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

Tool configuration

T2Cert