NO NON-Termination: ---------------- SCC: +--transitions: t4 +--nodes: n_f192_0_main_NE___2 Closed walk: 1 -> t4 deterministic: Forced for: arg2P, arg1P, arg2P, arg1P, arg2P, arg1P, arg2P Reachability checked! - Recurrent Set Found: { arg3 -arg3P == 0, -4 + arg2P == 0, -1 + arg1P == 0, -4 + arg2 == 0, -1 + arg1 == 0, -1 + arg3 >= 0 } Connected Subgraphs where we couldn't prove Termination: -------------------------------------------------------- SCC: +--transitions: +--nodes: n_f192_0_main_NE___4 SCC: +--transitions: t6 +--nodes: n_f192_0_main_NE___1 SCC: +--transitions: +--nodes: n_f192_0_main_NE___3 method 2