NO NON-Termination: ---------------- SCC: +--transitions: t4 +--nodes: f387_0_lcm_EQ Closed walk: 1 -> t4 Reachability checked! - Recurrent Set Found: { arg1 + arg2 -arg4P == 0, arg3 -arg3P == 0, arg1 + arg2 -arg2P == 0, arg1 -arg1P == 0, arg2 -arg4 == 0, -arg1 >= 0, -1 -arg2 + arg3 >= 0, arg3 >= 0, arg1 -arg2 >= 0 } Connected Subgraphs where we couldn't prove Termination: -------------------------------------------------------- SCC: +--transitions: t10,t9 +--nodes: f454_0_lcm_EQ SCC: +--transitions: t11,t12 +--nodes: f481_0_lcm_EQ SCC: +--transitions: +--nodes: f1_0_main_Load' SCC: +--transitions: +--nodes: f1_0_main_Load SCC: +--transitions: +--nodes: __init method 1