NO NON-Termination: ---------------- SCC: +--transitions: t0,t2 +--nodes: l0,l1 Closed walk: 2 -> t2, t0 Reachability checked! - Recurrent Set Found: { 2 + 2 * i_0 -j_post == 0, 1 + i_0 -i_post == 0, 2 * i_0 -X1 == 0, i_0 -X0 == 0, 2 * i_0 -j_0 == 0, i_0 >= 0 } method 1