NO NON-Termination: ---------------- SCC: +--transitions: t1,t2 +--nodes: l1,l2 Closed walk: 2 -> t1, t2 Reachability checked! - Recurrent Set Found: { 1 + x_5_0 -x_5_post == 0, 1 + x_5_0 -X0 == 0, x_5_0 >= 0 } method 1