NO
Nontermination proof succeeded
Found this recurrent set for cutpoint 14: executed_Drive_0 == 1 and executed_Drive_post == 1 and is_aborted_0 == 0 and is_aborted_next_0 == 0 and is_aborted_next_post == 0 and is_aborted_post == 0 and n0_0 == 1 and n1_0 == 1 and pc_Drive_next_0 == 1 and pc_Drive_next_post == 1 and pc_Drive_post == 1 and pc_Loop_0 == 2 and pc_Loop_post == 2 and pc_Plan_next_0 == 1 and pc_Plan_next_post == 1 and pc_Plan_post == 1 and x_0 == 0 and x_next_post == 0 and x_post == 0 and y_0 == 0 and y_next_post == 0 and y_post == 0
Errors: