NO NON-Termination: ---------------- SCC: +--transitions: t2,t3 +--nodes: f151_0_main_InvokeMethod Closed walk: 1 -> t2 deterministic: Forced for: arg2P, arg1P, arg2P, arg2P, arg1P, arg1P, arg1P, arg2P Reachability checked! - Recurrent Set Found: { arg3 -arg3P == 0, -1 + arg2P == 0, -1 + arg1P == 0, -1 + arg2 == 0, -1 + arg1 == 0, -1 + arg3 >= 0, 2 -arg3 >= 0 } Connected Subgraphs where we couldn't prove Termination: -------------------------------------------------------- SCC: +--transitions: +--nodes: f1_0_main_ConstantStackPush SCC: +--transitions: +--nodes: __init method 1