NO Termination: (Ranking Functions Found) ------------ l0: < < 11 -i_0, 0 > > l1: < < 10 -i_0, 10 -i_0 > > l2: < < 10 -i_0, 0 > > l3: < < 10 -i_0, 0 > > NON-Termination: ---------------- SCC: +--transitions: t1,t2 +--nodes: l2,l3 Closed walk: 2 -> t1, t2 Reachability checked! - Recurrent Set Found: { -1 + j_0 -j_post == 0, i_0 -i_post == 0, j_0 -X1 == 0, i_0 -X0 == 0, i_0 -j_0 >= 0, -2 + i_0 >= 0 } method 1