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