NO


Termination: (Ranking Functions Found)
------------
l0: < < -i_29_0 + length_27_0 > >
l10: < < -i_110_0 + length_27_0 > >


NON-Termination:
----------------
SCC:
+--transitions: t26,t27,t28,t29,t30,t31,t32
+--nodes: l2,l25,l26,l27,l28,l29,l30
Closed walk: 7 -> t26, t27, t28, t29, t30, t31, t32
deterministic: Forced for: X3, X11, X18, X20, X22, X28, X62, X75, X151, X151, X166, X166, X151, X166
Reachability checked!
- Recurrent Set Found:
{
	y_23_post == 0,
	x_SLAM_f_22_post == 0,
	t_25_0 -x_24_post == 0,
	tmp_33_0 -tmp_33_post == 0,
	temp_35_0 -temp_35_post == 0,
	temp_34_0 -temp_34_post == 0,
	temp0_21_0 -temp0_21_post == 0,
	tail_15_post == 0,
	t_25_0 -t_25_post == 0,
	-2 + result_dot_nondet_sdv_special_RETURN_VALUE_14_post == 0,
	result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_32_0 -result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_32_post == 0,
	result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_post == 0,
	result_11_0 -result_11_post == 0,
	rcd_43_post == 0,
	rcd_207_post == 0,
	rcd_185_0 -rcd_185_post == 0,
	rcd_179_0 -rcd_179_post == 0,
	rcd_112_0 -rcd_112_post == 0,
	lt_20_post == 0,
	lt_17_0 -lt_17_post == 0,
	length_27_0 -length_27_post == 0,
	i_29_0 -i_29_post == 0,
	1 + a_153_0 -i_120_post == 0,
	i_110_0 -i_110_post == 0,
	head_SLAM_f_28_0 -head_SLAM_f_28_post == 0,
	head_31_0 -head_31_post == 0,
	head_16_post == 0,
	a_208_post == 0,
	a_178_post == 0,
	a_153_0 -a_153_post == 0,
	X179 == 0,
	X178 == 0,
	t_25_0 -X177 == 0,
	tmp_33_0 -X176 == 0,
	temp_35_0 -X175 == 0,
	temp_34_0 -X174 == 0,
	temp0_21_0 -X173 == 0,
	X172 == 0,
	t_25_0 -X171 == 0,
	-2 + X170 == 0,
	result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_32_0 -X169 == 0,
	X168 == 0,
	result_11_0 -X167 == 0,
	X166 == 0,
	X165 == 0,
	rcd_185_0 -X164 == 0,
	rcd_179_0 -X163 == 0,
	rcd_112_0 -X162 == 0,
	X161 == 0,
	lt_17_0 -X160 == 0,
	length_27_0 -X159 == 0,
	i_29_0 -X158 == 0,
	1 + a_153_0 -X157 == 0,
	i_110_0 -X156 == 0,
	head_SLAM_f_28_0 -X155 == 0,
	head_31_0 -X154 == 0,
	X153 == 0,
	X152 == 0,
	X151 == 0,
	a_153_0 -X150 == 0,
	X149 == 0,
	X148 == 0,
	t_25_0 -X147 == 0,
	tmp_33_0 -X146 == 0,
	temp_35_0 -X145 == 0,
	temp_34_0 -X144 == 0,
	temp0_21_0 -X143 == 0,
	X142 == 0,
	t_25_0 -X141 == 0,
	-2 + X140 == 0,
	result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_32_0 -X139 == 0,
	X138 == 0,
	result_11_0 -X137 == 0,
	rcd_43_0 -X136 == 0,
	X135 == 0,
	rcd_185_0 -X134 == 0,
	rcd_179_0 -X133 == 0,
	rcd_112_0 -X132 == 0,
	X131 == 0,
	lt_17_0 -X130 == 0,
	length_27_0 -X129 == 0,
	i_29_0 -X128 == 0,
	1 + a_153_0 -X127 == 0,
	i_110_0 -X126 == 0,
	head_SLAM_f_28_0 -X125 == 0,
	head_31_0 -X124 == 0,
	X123 == 0,
	X122 == 0,
	a_178_0 -X121 == 0,
	a_153_0 -X120 == 0,
	X119 == 0,
	X118 == 0,
	t_25_0 -X117 == 0,
	tmp_33_0 -X116 == 0,
	temp_35_0 -X115 == 0,
	temp_34_0 -X114 == 0,
	temp0_21_0 -X113 == 0,
	X112 == 0,
	t_25_0 -X111 == 0,
	-2 + X110 == 0,
	result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_32_0 -X109 == 0,
	X108 == 0,
	result_11_0 -X107 == 0,
	rcd_43_0 -X106 == 0,
	X105 == 0,
	rcd_185_0 -X104 == 0,
	rcd_179_0 -X103 == 0,
	rcd_112_0 -X102 == 0,
	X101 == 0,
	lt_17_0 -X100 == 0,
	length_27_0 -X99 == 0,
	i_29_0 -X98 == 0,
	1 + a_153_0 -X97 == 0,
	i_110_0 -X96 == 0,
	head_SLAM_f_28_0 -X95 == 0,
	head_31_0 -X94 == 0,
	X93 == 0,
	X92 == 0,
	a_178_0 -X91 == 0,
	a_153_0 -X90 == 0,
	X89 == 0,
	X88 == 0,
	t_25_0 -X87 == 0,
	tmp_33_0 -X86 == 0,
	temp_35_0 -X85 == 0,
	temp_34_0 -X84 == 0,
	temp0_21_0 -X83 == 0,
	X82 == 0,
	t_25_0 -X81 == 0,
	-2 + X80 == 0,
	result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_32_0 -X79 == 0,
	X78 == 0,
	result_11_0 -X77 == 0,
	rcd_43_0 -X76 == 0,
	X75 == 0,
	rcd_185_0 -X74 == 0,
	rcd_179_0 -X73 == 0,
	rcd_112_0 -X72 == 0,
	X71 == 0,
	lt_17_0 -X70 == 0,
	length_27_0 -X69 == 0,
	i_29_0 -X68 == 0,
	1 + a_153_0 -X67 == 0,
	i_110_0 -X66 == 0,
	head_SLAM_f_28_0 -X65 == 0,
	head_31_0 -X64 == 0,
	X63 == 0,
	X62 == 0,
	a_178_0 -X61 == 0,
	a_153_0 -X60 == 0,
	X59 == 0,
	X58 == 0,
	t_25_0 -X57 == 0,
	tmp_33_0 -X56 == 0,
	temp_35_0 -X55 == 0,
	temp_34_0 -X54 == 0,
	temp0_21_0 -X53 == 0,
	X52 == 0,
	t_25_0 -X51 == 0,
	-2 + X50 == 0,
	result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_32_0 -X49 == 0,
	X48 == 0,
	result_11_0 -X47 == 0,
	rcd_43_0 -X46 == 0,
	rcd_207_0 -X45 == 0,
	rcd_185_0 -X44 == 0,
	rcd_179_0 -X43 == 0,
	rcd_112_0 -X42 == 0,
	X41 == 0,
	lt_17_0 -X40 == 0,
	length_27_0 -X39 == 0,
	i_29_0 -X38 == 0,
	1 + a_153_0 -X37 == 0,
	i_110_0 -X36 == 0,
	head_SLAM_f_28_0 -X35 == 0,
	head_31_0 -X34 == 0,
	X33 == 0,
	a_208_0 -X32 == 0,
	a_178_0 -X31 == 0,
	a_153_0 -X30 == 0,
	X29 == 0,
	X28 == 0,
	t_25_0 -X27 == 0,
	tmp_33_0 -X26 == 0,
	temp_35_0 -X25 == 0,
	temp_34_0 -X24 == 0,
	temp0_21_0 -X23 == 0,
	X22 == 0,
	t_25_0 -X21 == 0,
	-2 + X20 == 0,
	result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_32_0 -X19 == 0,
	X18 == 0,
	result_11_0 -X17 == 0,
	rcd_43_0 -X16 == 0,
	rcd_207_0 -X15 == 0,
	rcd_185_0 -X14 == 0,
	rcd_179_0 -X13 == 0,
	rcd_112_0 -X12 == 0,
	X11 == 0,
	lt_17_0 -X10 == 0,
	length_27_0 -X9 == 0,
	i_29_0 -X8 == 0,
	1 + a_153_0 -X7 == 0,
	i_110_0 -X6 == 0,
	head_SLAM_f_28_0 -X5 == 0,
	head_31_0 -X4 == 0,
	X3 == 0,
	a_208_0 -X2 == 0,
	a_178_0 -X1 == 0,
	a_153_0 -X0 == 0,
	y_23_0 == 0,
	head_16_0 -x_SLAM_f_22_0 == 0,
	t_25_0 -x_24_0 == 0,
	result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_0 -tail_15_0 == 0,
	-2 + result_dot_nondet_sdv_special_RETURN_VALUE_14_0 == 0,
	lt_20_0 == 0,
	1 + a_153_0 -i_120_0 == 0
}
Connected Subgraphs where we couldn't prove Termination:
--------------------------------------------------------
SCC:
+--transitions: t9
+--nodes: l0,l10


method 1