NO
Nontermination proof succeeded
Found this recurrent set for cutpoint 71: a_1052_0 == 2 and a_1052_post == 0 and a_1810_0 == 3 and a_1810_post == 0 and a_2035_0 == 2 and a_2035_post == 2 and a_2238_0 == 2 and a_2238_post == 2 and a_244_0 == 1 and a_244_post == 0 and a_511_0 == 1 and a_654_0 == 0 and a_654_post == 0 and ct_19_0 == 0 and ct_19_post == 0 and head_16_0 == -1 and head_16_post == -1 and head_31_0 == -1 and head_31_post == 0 and i_29_0 == 2 and i_29_post == 0 and length_28_0 == 2 and length_28_post == 0 and nondet_13_1 == 2 and r_543_post == 0 and r_662_0 == 0 and rcd_63_post == 0 and rcd_83_0 == 0 and result_12_1 == -1 and sdv_CALLSITE_RETURN_1_14_0 == 2 and sdv_CALLSITE_RETURN_1_14_post == 2 and sdv_CALLSITE_RETURN_1_32_0 == -1 and sdv_CALLSITE_RETURN_1_32_post == 0 and sel_r_543_Flink_24_0 == 0 and t_25_0 == 1 and t_25_post == 1 and temp0_30_1 == -1 and temp_34_1 == -1 and tmp_33_0 == -1 and tmp_33_post == 0 and x_15_0 == 0 and x_15_post == 0 and x_18_0 == -1 and x_18_post == -1 and x_22_0 == 1 and x_22_post == 1 and x_SLAM_f_20_0 == -1 and x_SLAM_f_20_post == -1 and y_21_0 == 0 and y_21_post == 0
Errors: