NO NON-Termination: ---------------- SCC: +--transitions: t13,t15 +--nodes: eval_main_bb10_in,eval_main_bb9_in Closed walk: 2 -> t13, t15 Reachability checked! - Recurrent Set Found: { v_i.3' == 0, v_i.2 -v_i.2' == 0, v_i.1 -v_i.1' == 0, v_i.0 -v_i.0' == 0, v_8 -v_8' == 0, v_5 -v_5' == 0, v_2 -v_2' == 0, v_10' == 0, X7 == 0, v_i.2 -X6 == 0, v_i.1 -X5 == 0, v_i.0 -X4 == 0, v_8 -X3 == 0, v_5 -X2 == 0, v_2 -X1 == 0, v_10 -X0 == 0, v_i.3 == 0 } method 1