NO
Nontermination proof succeeded
Found this recurrent set for cutpoint 57: a_153_0 == 0 and a_153_post == 0 and a_178_0 == 0 and a_178_post == 0 and a_208_0 == 0 and a_208_post == 0 and head_16_0 == 1 and head_16_post == 1 and head_31_0 == 1 and head_31_post == 0 and head_SLAM_f_28_post == 0 and i_120_0 == 2 and i_120_post == 1 and i_29_0 == 2 and i_29_post == 0 and length_27_0 == 2 and length_27_post == 0 and lt_17_0 == 2 and lt_20_0 == 0 and lt_20_post == 0 and nondet_12_1 == 2 and rcd_185_0 == 0 and rcd_185_post == 0 and rcd_207_0 == 0 and rcd_207_post == 0 and rcd_43_0 == 0 and rcd_43_post == 0 and result_11_1 == 1 and result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_0 == 0 and result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_13_post == 0 and result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_32_post == 0 and result_dot_nondet_sdv_special_RETURN_VALUE_14_0 == 2 and result_dot_nondet_sdv_special_RETURN_VALUE_14_post == 2 and t_25_0 == 1 and t_25_post == 1 and tail_15_0 == 0 and tail_15_post == 0 and temp0_30_1 == 1 and temp_34_0 == 24 and temp_34_post == 0 and temp_35_0 == 0 and tmp_33_post == 0 and x_24_0 == 1 and x_24_post == 1 and x_SLAM_f_22_0 == 1 and x_SLAM_f_22_1 == 1 and x_SLAM_f_22_post == 1 and y_23_0 == 0 and y_23_post == 0
Errors: