NO Solver Timeout: 4 Global Timeout: 300 No parsing errors! Init Location: 0 Transitions: (1 + l^0)}> (1 + i^0)}> (~(1) + i^0)}> undef313, k^0 -> (1 + k^0)}> undef333, g^0 -> undef336, p^0 -> undef343, r^0 -> undef344, s^0 -> undef345}> undef465, f^0 -> undef468, r^0 -> undef477}> undef510, g^0 -> undef513, p^0 -> 0, s^0 -> (0 + undef510)}> undef550, tmp___5^0 -> (0 + (~(1) * undef550))}> undef571, tmp___5^0 -> (0 + undef571)}> undef579, r^0 -> undef587}> (1 + iter^0), tmp___2^0 -> (0 + iter^0)}> (1 + m^0)}> ((0 + undef941) + undef942), tmp^0 -> undef941, tmp___0^0 -> undef942, tmp___1^0 -> undef943}> 0}> Fresh variables: undef313, undef333, undef336, undef343, undef344, undef345, undef353, undef465, undef468, undef477, undef510, undef513, undef550, undef571, undef579, undef587, undef941, undef942, undef943, Undef variables: undef313, undef333, undef336, undef343, undef344, undef345, undef353, undef465, undef468, undef477, undef510, undef513, undef550, undef571, undef579, undef587, undef941, undef942, undef943, Abstraction variables: Exit nodes: Accepting locations: Asserts: Preprocessed LLVMGraph Init Location: 0 Transitions: 0}> (1 + i^0)}> (1 + l^0)}> 0, l^0 -> (1 + l^0)}> (1 + l^0)}> 0, l^0 -> (1 + l^0)}> (1 + l^0)}> 0, l^0 -> (1 + l^0)}> (1 + l^0)}> 0, l^0 -> (1 + l^0)}> (~(1) + i^0)}> (~(1) + i^0), r^0 -> undef344}> (~(1) + i^0), r^0 -> undef344}> (~(1) + i^0), r^0 -> undef477}> (1 + k^0)}> (1 + l^0)}> (1 + iter^0), tmp___2^0 -> (0 + iter^0)}> (1 + iter^0), tmp___2^0 -> (0 + iter^0)}> (1 + m^0)}> (1 + m^0)}> 0, l^0 -> (1 + l^0)}> (1 + iter^0), tmp___2^0 -> (0 + iter^0)}> (1 + iter^0), tmp___2^0 -> (0 + iter^0)}> undef587}> undef344}> undef344}> undef477}> undef587}> undef344}> undef344}> undef477}> undef587}> undef344}> undef344}> undef477}> undef587}> undef344}> undef344}> undef477}> undef587}> undef344}> undef344}> undef477}> undef587}> undef344}> undef344}> undef477}> Fresh variables: undef313, undef333, undef336, undef343, undef344, undef345, undef353, undef465, undef468, undef477, undef510, undef513, undef550, undef571, undef579, undef587, undef941, undef942, undef943, Undef variables: undef313, undef333, undef336, undef343, undef344, undef345, undef353, undef465, undef468, undef477, undef510, undef513, undef550, undef571, undef579, undef587, undef941, undef942, undef943, Abstraction variables: Exit nodes: Accepting locations: Asserts: ************************************************************* ******************************************************************************************* *********************** WORKING TRANSITION SYSTEM (DAG) *********************** ******************************************************************************************* Init Location: 0 Graph 0: Transitions: Variables: Graph 1: Transitions: 1 + i^0, rest remain the same}> Variables: i^0, n^0 Graph 2: Transitions: 0, l^0 -> 1 + l^0, rest remain the same}> 0, l^0 -> 1 + l^0, rest remain the same}> 0, l^0 -> 1 + l^0, rest remain the same}> 0, l^0 -> 1 + l^0, rest remain the same}> -1 + i^0, rest remain the same}> -1 + i^0, r^0 -> undef344, rest remain the same}> -1 + i^0, r^0 -> undef344, rest remain the same}> -1 + i^0, r^0 -> undef477, rest remain the same}> 1 + k^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + m^0, rest remain the same}> 1 + m^0, rest remain the same}> 0, l^0 -> 1 + l^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> undef587, rest remain the same}> undef344, rest remain the same}> undef344, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef344, rest remain the same}> undef344, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef344, rest remain the same}> undef344, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef344, rest remain the same}> undef344, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef344, rest remain the same}> undef344, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef344, rest remain the same}> undef344, rest remain the same}> undef477, rest remain the same}> Variables: l^0, m^0, n^0, r^0, i^0, k^0, iter^0, tmp___2^0, __const_30^0 Graph 3: Transitions: Variables: Precedence: Graph 0 Graph 1 Graph 2 0, rest remain the same}> Graph 3 1 + l^0, rest remain the same}> 1 + l^0, rest remain the same}> 1 + l^0, rest remain the same}> 1 + l^0, rest remain the same}> 1 + l^0, rest remain the same}> Map Locations to Subgraph: ( 0 , 0 ) ( 6 , 1 ) ( 9 , 2 ) ( 13 , 2 ) ( 15 , 2 ) ( 22 , 2 ) ( 28 , 3 ) ******************************************************************************************* ******************************** CHECKING ASSERTIONS ******************************** ******************************************************************************************* Proving termination of subgraph 0 Proving termination of subgraph 1 Checking unfeasibility... Time used: 0.000893 Checking conditional termination of SCC {l6}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000648s Ranking function: -i^0 + n^0 New Graphs: Proving termination of subgraph 2 Checking unfeasibility... Time used: 0.728598 Some transition disabled by a set of invariant(s): Invariant at l9: l^0 <= n^0 Invariant at l13: l^0 <= n^0 Invariant at l15: l^0 <= n^0 Invariant at l22: l^0 <= n^0 Strengthening and disabling transitions... > It's unfeasible. Removing transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, l^0 -> 1 + l^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, l^0 -> 1 + l^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, l^0 -> 1 + l^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, l^0 -> 1 + l^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + i^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + i^0, r^0 -> undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + i^0, r^0 -> undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + i^0, r^0 -> undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + k^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + m^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + m^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, l^0 -> 1 + l^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> Checking unfeasibility... Time used: 0.588002 Checking conditional termination of SCC {l9, l13, l15, l22}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.029324s Ranking function: -8 - 5*l^0 - 3*m^0 + 8*n^0 New Graphs: Transitions: -1 + i^0, rest remain the same}> -1 + i^0, r^0 -> undef344, rest remain the same}> -1 + i^0, r^0 -> undef344, rest remain the same}> -1 + i^0, r^0 -> undef477, rest remain the same}> 1 + k^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + m^0, rest remain the same}> 1 + m^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> undef587, rest remain the same}> undef344, rest remain the same}> undef344, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef344, rest remain the same}> undef344, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef344, rest remain the same}> undef344, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef344, rest remain the same}> undef344, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef344, rest remain the same}> undef344, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef344, rest remain the same}> undef344, rest remain the same}> undef477, rest remain the same}> Variables: __const_30^0, i^0, iter^0, k^0, l^0, m^0, n^0, r^0, tmp___2^0 Checking conditional termination of SCC {l9, l13, l15, l22}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.018157s Ranking function: -5 + 5*i^0 - 5*l^0 New Graphs: Transitions: -1 + i^0, rest remain the same}> 1 + k^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + m^0, rest remain the same}> 1 + m^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> undef587, rest remain the same}> undef344, rest remain the same}> undef344, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef344, rest remain the same}> undef344, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef344, rest remain the same}> undef344, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef344, rest remain the same}> undef344, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef344, rest remain the same}> undef344, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef344, rest remain the same}> undef344, rest remain the same}> undef477, rest remain the same}> Variables: __const_30^0, i^0, iter^0, k^0, l^0, m^0, n^0, r^0, tmp___2^0 Checking conditional termination of SCC {l9, l13, l15, l22}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.018723s Ranking function: 2 - 4*k^0 - 2*l^0 + 6*n^0 New Graphs: Transitions: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + m^0, rest remain the same}> 1 + m^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> undef587, rest remain the same}> -1 + i^0, r^0 -> undef344, rest remain the same}> -1 + i^0, r^0 -> undef344, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> -1 + i^0, r^0 -> undef344, rest remain the same}> -1 + i^0, r^0 -> undef344, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> -1 + i^0, r^0 -> undef344, rest remain the same}> -1 + i^0, r^0 -> undef344, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> -1 + i^0, r^0 -> undef344, rest remain the same}> -1 + i^0, r^0 -> undef344, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> -1 + i^0, r^0 -> undef344, rest remain the same}> -1 + i^0, r^0 -> undef344, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> -1 + i^0, r^0 -> undef344, rest remain the same}> -1 + i^0, r^0 -> undef344, rest remain the same}> undef477, rest remain the same}> Variables: __const_30^0, i^0, iter^0, k^0, l^0, m^0, n^0, r^0, tmp___2^0 Checking conditional termination of SCC {l9, l15, l22}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.017940s Ranking function: -6 - 6*l^0 - 7*m^0 + 13*n^0 It's unfeasible after collapsing. Removing transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> It's unfeasible after collapsing. Removing transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> It's unfeasible after collapsing. Removing transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> It's unfeasible after collapsing. Removing transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> It's unfeasible after collapsing. Removing transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> It's unfeasible after collapsing. Removing transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> It's unfeasible after collapsing. Removing transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> It's unfeasible after collapsing. Removing transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> It's unfeasible after collapsing. Removing transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> It's unfeasible after collapsing. Removing transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> It's unfeasible after collapsing. Removing transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> It's unfeasible after collapsing. Removing transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> New Graphs: Transitions: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> undef587, rest remain the same}> -1 + i^0, r^0 -> undef344, rest remain the same}> -1 + i^0, r^0 -> undef344, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> -1 + i^0, r^0 -> undef344, rest remain the same}> -1 + i^0, r^0 -> undef344, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> -1 + i^0, r^0 -> undef344, rest remain the same}> -1 + i^0, r^0 -> undef344, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> -1 + i^0, r^0 -> undef344, rest remain the same}> -1 + i^0, r^0 -> undef344, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> -1 + i^0, r^0 -> undef344, rest remain the same}> -1 + i^0, r^0 -> undef344, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> -1 + i^0, r^0 -> undef344, rest remain the same}> -1 + i^0, r^0 -> undef344, rest remain the same}> undef477, rest remain the same}> Variables: __const_30^0, i^0, iter^0, k^0, l^0, m^0, n^0, r^0, tmp___2^0 Checking conditional termination of SCC {l9, l22}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.025067s Ranking function: -4 + i^0 + 4*k^0 - 3*l^0 - 2*n^0 New Graphs: Transitions: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> undef587, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef477, rest remain the same}> Variables: __const_30^0, i^0, iter^0, l^0, m^0, n^0, r^0, tmp___2^0 Checking conditional termination of SCC {l9, l22}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.011561s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.133956s Trying to remove transition: undef477, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.043430s Time used: 0.041922 Trying to remove transition: undef587, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.045799s Time used: 0.044263 Trying to remove transition: undef477, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.043550s Time used: 0.041952 Trying to remove transition: undef587, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.045650s Time used: 0.044104 Trying to remove transition: undef477, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.046198s Time used: 0.044643 Trying to remove transition: undef587, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.058315s Time used: 0.056744 Trying to remove transition: undef477, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.046879s Time used: 0.04522 Trying to remove transition: undef587, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.054008s Time used: 0.052438 Trying to remove transition: undef477, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.047623s Time used: 0.045965 Trying to remove transition: undef587, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.051832s Time used: 0.050234 Trying to remove transition: undef477, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.048226s Time used: 0.046588 Trying to remove transition: undef587, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.052824s Time used: 0.051162 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.055763s Time used: 0.054117 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.100363s Time used: 0.098513 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.055760s Time used: 0.053684 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.098091s Time used: 0.096262 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.081626s Time used: 0.0796 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.088406s Time used: 0.086332 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.075627s Time used: 0.073564 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.083739s Time used: 0.081821 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.062322s Time used: 0.060424 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.065454s Time used: 0.063545 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.086584s Time used: 0.084692 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.094174s Time used: 0.092208 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 2.313820s Time used: 2.30901 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.002622s Time used: 1.00261 LOG: SAT solveNonLinear - Elapsed time: 3.316442s Cost: 1; Total time: 3.31162 Failed at location 15: 1 + l^0 <= m^0 Before Improving: Quasi-invariant at l9: 1 + l^0 <= m^0 Quasi-invariant at l13: 1 + l^0 <= m^0 Quasi-invariant at l15: 1 + l^0 <= m^0 Quasi-invariant at l22: 1 + l^0 <= m^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.049711s Remaining time after improvement: 0.969852 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l9: 1 + l^0 <= m^0 Quasi-invariant at l13: 1 + l^0 <= m^0 Quasi-invariant at l15: 1 + l^0 <= m^0 Quasi-invariant at l22: 1 + l^0 <= m^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 0, l^0 -> 1 + l^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 0, l^0 -> 1 + l^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 0, l^0 -> 1 + l^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 0, l^0 -> 1 + l^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + i^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + i^0, r^0 -> undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + i^0, r^0 -> undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + i^0, r^0 -> undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + k^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + m^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + m^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 0, l^0 -> 1 + l^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> [ Termination Graph ] Strengthening and disabling transitions... > It's unfeasible. Removing transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> New Graphs: Transitions: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> undef587, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef477, rest remain the same}> Variables: __const_30^0, i^0, iter^0, l^0, m^0, n^0, r^0, tmp___2^0 Checking conditional termination of SCC {l9, l22}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.010573s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.140339s Trying to remove transition: undef477, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.052917s Time used: 0.050359 Trying to remove transition: undef587, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.061244s Time used: 0.058459 Trying to remove transition: undef477, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.053860s Time used: 0.051324 Trying to remove transition: undef587, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.061509s Time used: 0.059173 Trying to remove transition: undef477, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.059875s Time used: 0.057437 Trying to remove transition: undef587, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.061992s Time used: 0.059657 Trying to remove transition: undef477, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.058116s Time used: 0.055816 Trying to remove transition: undef587, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.063767s Time used: 0.061463 Trying to remove transition: undef477, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.059242s Time used: 0.057072 Trying to remove transition: undef587, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.063214s Time used: 0.061134 Trying to remove transition: undef477, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.058557s Time used: 0.056509 Trying to remove transition: undef587, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.063085s Time used: 0.061098 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.109721s Time used: 0.107782 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.054074s Time used: 0.051991 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.135341s Time used: 0.133532 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.103345s Time used: 0.101351 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.075261s Time used: 0.073259 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.135979s Time used: 0.134176 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.142686s Time used: 0.140914 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.138277s Time used: 0.136474 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.001792s Time used: 4.00001 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.010168s Time used: 4.00006 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.024995s Time used: 1.00021 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 2.140692s Time used: 2.09857 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.003553s Time used: 1.00355 LOG: SAT solveNonLinear - Elapsed time: 3.144245s Cost: 1; Total time: 3.10211 Termination implied by a set of invariant(s): Invariant at l9: 1 + l^0 + tmp___2^0 <= iter^0 + n^0 Invariant at l13: 1 + l^0 + tmp___2^0 <= iter^0 + n^0 Invariant at l15: l^0 <= n^0 Invariant at l22: 1 + l^0 + tmp___2^0 <= iter^0 + n^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + i^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + i^0, r^0 -> undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + i^0, r^0 -> undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + i^0, r^0 -> undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + k^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + m^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + m^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> [ Termination Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> Quasi-ranking function: 50000 - iter^0 - l^0 + m^0 New Graphs: Transitions: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> undef587, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef477, rest remain the same}> Variables: __const_30^0, i^0, iter^0, l^0, m^0, n^0, r^0, tmp___2^0 Checking conditional termination of SCC {l9, l22}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.015866s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 1.031189s Trying to remove transition: undef477, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.070665s Time used: 0.067659 Trying to remove transition: undef587, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.076438s Time used: 0.073421 Trying to remove transition: undef477, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.073280s Time used: 0.070195 Trying to remove transition: undef587, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.077075s Time used: 0.074255 Trying to remove transition: undef477, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.078357s Time used: 0.075336 Trying to remove transition: undef587, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.082113s Time used: 0.079403 Trying to remove transition: undef477, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.080971s Time used: 0.078484 Trying to remove transition: undef587, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.079951s Time used: 0.077517 Trying to remove transition: undef477, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.077197s Time used: 0.074864 Trying to remove transition: undef587, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.081316s Time used: 0.079115 Trying to remove transition: undef477, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.079093s Time used: 0.076909 Trying to remove transition: undef587, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.081782s Time used: 0.079659 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.188032s Time used: 0.186069 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.080764s Time used: 0.078694 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.091248s Time used: 0.089214 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.178257s Time used: 0.1763 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.114864s Time used: 0.112788 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.141144s Time used: 0.139283 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.121958s Time used: 0.120068 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.142780s Time used: 0.140989 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.003870s Time used: 4.00199 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.010218s Time used: 4.00001 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.025195s Time used: 1.0001 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 2.522591s Time used: 2.48004 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.002809s Time used: 1.0028 LOG: SAT solveNonLinear - Elapsed time: 3.525400s Cost: 1; Total time: 3.48285 Termination implied by a set of invariant(s): Invariant at l9: 1 + l^0 <= m^0 Invariant at l13: 1 + l^0 + tmp___2^0 <= iter^0 + n^0 Invariant at l15: l^0 <= n^0 Invariant at l22: iter^0 + l^0 <= 1 + n^0 + tmp___2^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + i^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + i^0, r^0 -> undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + i^0, r^0 -> undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + i^0, r^0 -> undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + k^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + m^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + m^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> [ Termination Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> Quasi-ranking function: 50000 + __const_30^0 - iter^0 - 3*l^0 + 2*m^0 + n^0 New Graphs: Transitions: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> undef587, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef477, rest remain the same}> Variables: __const_30^0, i^0, iter^0, l^0, m^0, n^0, r^0, tmp___2^0 Checking conditional termination of SCC {l9, l22}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.018671s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 1.890413s Trying to remove transition: undef477, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.083417s Time used: 0.080299 Trying to remove transition: undef587, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.090660s Time used: 0.087618 Trying to remove transition: undef477, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.085960s Time used: 0.0828 Trying to remove transition: undef587, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.092830s Time used: 0.089887 Trying to remove transition: undef477, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.091855s Time used: 0.089281 Trying to remove transition: undef587, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.095579s Time used: 0.093049 Trying to remove transition: undef477, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.093424s Time used: 0.091001 Trying to remove transition: undef587, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.094928s Time used: 0.092545 Trying to remove transition: undef477, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.092540s Time used: 0.090324 Trying to remove transition: undef587, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.097613s Time used: 0.095456 Trying to remove transition: undef477, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.091793s Time used: 0.089651 Trying to remove transition: undef587, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.098187s Time used: 0.096134 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.230226s Time used: 0.228178 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.145021s Time used: 0.142801 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.211449s Time used: 0.209308 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.122027s Time used: 0.119796 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.119777s Time used: 0.117682 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.197717s Time used: 0.195556 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.149081s Time used: 0.146975 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.166544s Time used: 0.164509 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.002077s Time used: 4.00001 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.011637s Time used: 4.00135 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.023653s Time used: 1.0002 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 3.381347s Time used: 3.33758 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.665779s Time used: 0.665774 LOG: SAT solveNonLinear - Elapsed time: 4.047126s Cost: 1; Total time: 4.00336 Termination implied by a set of invariant(s): Invariant at l9: l^0 <= 1 + i^0 Invariant at l13: l^0 <= i^0 Invariant at l15: l^0 <= 1 + i^0 Invariant at l22: l^0 <= 1 + i^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + i^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + i^0, r^0 -> undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + i^0, r^0 -> undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + i^0, r^0 -> undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + k^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + m^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + m^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> [ Termination Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> Quasi-ranking function: 50000 + __const_30^0 - i^0 - iter^0 - 3*l^0 + 3*m^0 + n^0 New Graphs: Transitions: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> undef587, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef477, rest remain the same}> Variables: __const_30^0, i^0, iter^0, l^0, m^0, n^0, r^0, tmp___2^0 Checking conditional termination of SCC {l9, l22}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.021557s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 2.010284s Trying to remove transition: undef477, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.096892s Time used: 0.093509 Trying to remove transition: undef587, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.104426s Time used: 0.101311 Trying to remove transition: undef477, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.098825s Time used: 0.095813 Trying to remove transition: undef587, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.104752s Time used: 0.101752 Trying to remove transition: undef477, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.104111s Time used: 0.101515 Trying to remove transition: undef587, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.109118s Time used: 0.106421 Trying to remove transition: undef477, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.105406s Time used: 0.102743 Trying to remove transition: undef587, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.110161s Time used: 0.107648 Trying to remove transition: undef477, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.105620s Time used: 0.103354 Trying to remove transition: undef587, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.113289s Time used: 0.110885 Trying to remove transition: undef477, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.104277s Time used: 0.102106 Trying to remove transition: undef587, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.113123s Time used: 0.111052 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.167014s Time used: 0.164921 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.184951s Time used: 0.182672 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.153376s Time used: 0.151129 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.309572s Time used: 0.307367 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.243633s Time used: 0.241319 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.200267s Time used: 0.19806 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.145760s Time used: 0.143552 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.293816s Time used: 0.291582 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.002324s Time used: 4.00007 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.010287s Time used: 4.00001 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.023062s Time used: 1.00008 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 2.813453s Time used: 2.76999 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.003732s Time used: 1.00372 LOG: SAT solveNonLinear - Elapsed time: 3.817185s Cost: 1; Total time: 3.77371 Termination implied by a set of invariant(s): Invariant at l9: l^0 <= 1 + n^0 Invariant at l13: l^0 + tmp___2^0 <= 1 + iter^0 + n^0 Invariant at l15: l^0 <= n^0 Invariant at l22: tmp___2^0 <= 1 + iter^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + i^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + i^0, r^0 -> undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + i^0, r^0 -> undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + i^0, r^0 -> undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + k^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + m^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + m^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> [ Termination Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> Quasi-ranking function: 50000 + i^0 - iter^0 - 50007*l^0 + 50005*m^0 + n^0 New Graphs: Transitions: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> undef587, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef477, rest remain the same}> Variables: __const_30^0, i^0, iter^0, l^0, m^0, n^0, r^0, tmp___2^0 Checking conditional termination of SCC {l9, l22}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.024519s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 2.042927s Trying to remove transition: undef477, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.113821s Time used: 0.110029 Trying to remove transition: undef587, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.118583s Time used: 0.114924 Trying to remove transition: undef477, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.114877s Time used: 0.111646 Trying to remove transition: undef587, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.128356s Time used: 0.125038 Trying to remove transition: undef477, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.119537s Time used: 0.116383 Trying to remove transition: undef587, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.123848s Time used: 0.120685 Trying to remove transition: undef477, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.121191s Time used: 0.118243 Trying to remove transition: undef587, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.123609s Time used: 0.120984 Trying to remove transition: undef477, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.120196s Time used: 0.117743 Trying to remove transition: undef587, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.122401s Time used: 0.120141 Trying to remove transition: undef477, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.118727s Time used: 0.116505 Trying to remove transition: undef587, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.121947s Time used: 0.119787 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.208748s Time used: 0.206678 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.247894s Time used: 0.245602 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.260543s Time used: 0.258252 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.221603s Time used: 0.219337 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.178905s Time used: 0.176607 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.217168s Time used: 0.214895 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.219713s Time used: 0.217489 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.165889s Time used: 0.163564 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.002628s Time used: 4.00042 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.010606s Time used: 4.00003 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.023678s Time used: 1.00012 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 3.272956s Time used: 3.22853 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.775667s Time used: 0.77566 LOG: SAT solveNonLinear - Elapsed time: 4.048622s Cost: 1; Total time: 4.00419 Termination implied by a set of invariant(s): Invariant at l9: l^0 + tmp___2^0 <= 1 + iter^0 + m^0 Invariant at l13: l^0 + tmp___2^0 <= 1 + iter^0 + m^0 Invariant at l15: l^0 <= 1 + i^0 Invariant at l22: 1 + l^0 + tmp___2^0 <= iter^0 + m^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + i^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + i^0, r^0 -> undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + i^0, r^0 -> undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + i^0, r^0 -> undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + k^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + m^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + m^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef344, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> [ Termination Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> Quasi-ranking function: 50000 + 50004*i^0 - iter^0 - 50010*l^0 + 6*m^0 New Graphs: Transitions: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> undef587, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef477, rest remain the same}> Variables: __const_30^0, i^0, iter^0, l^0, m^0, n^0, r^0, tmp___2^0 Checking conditional termination of SCC {l9, l22}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.028485s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 2.010091s Trying to remove transition: undef477, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.130912s Time used: 0.12689 Trying to remove transition: undef587, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.136285s Time used: 0.132932 Trying to remove transition: undef477, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.130690s Time used: 0.127741 Trying to remove transition: undef587, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.145041s Time used: 0.141983 Trying to remove transition: undef477, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.139368s Time used: 0.13619 Trying to remove transition: undef587, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.145663s Time used: 0.142716 Trying to remove transition: undef477, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.138454s Time used: 0.135811 Trying to remove transition: undef587, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.146589s Time used: 0.144077 Trying to remove transition: undef477, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.139013s Time used: 0.136229 Trying to remove transition: undef587, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.140070s Time used: 0.137802 Trying to remove transition: undef477, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.135562s Time used: 0.133324 Trying to remove transition: undef587, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.139345s Time used: 0.137203 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.205864s Time used: 0.203758 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.282016s Time used: 0.279705 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.229836s Time used: 0.227485 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.220337s Time used: 0.217947 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.279028s Time used: 0.276622 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.200238s Time used: 0.197833 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.383249s Time used: 0.380915 Trying to remove transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.242944s Time used: 0.240478 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.009531s Time used: 4.00706 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.011015s Time used: 4.00002 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.023226s Time used: 1.00008 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.069856s Time used: 4.02772 Termination failed. Trying to show unreachability... Proving unreachability of entry: 0, rest remain the same}> LOG: CALL check - Post:1 <= 0 - Process 1 * Exit transition: 0, rest remain the same}> * Postcondition : 1 <= 0 Postcodition moved up: 1 <= 0 LOG: Try proving POST Postcondition: 1 <= 0 LOG: CALL check - Post:1 <= 0 - Process 2 * Exit transition: * Postcondition : 1 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.011253s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.011299s LOG: NarrowEntry size 1 Narrowing transition: 1 + i^0, rest remain the same}> LOG: Narrow transition size 1 ENTRIES: END ENTRIES: GRAPH: 1 + i^0, rest remain the same}> END GRAPH: EXIT: 0, rest remain the same}> POST: 1 <= 0 LOG: Try proving POST Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.071797s Time used: 0.071635 Improving Solution with cost 51 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.013041s Time used: 1.01303 LOG: SAT solveNonLinear - Elapsed time: 1.084838s Cost: 51; Total time: 1.08467 Failed at location 6: 1 + n^0 <= i^0 Before Improving: Quasi-invariant at l6: 1 + n^0 <= i^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004437s Remaining time after improvement: 0.996824 Some transition disabled by a set of quasi-invariant(s): Quasi-invariant at l6: 1 + n^0 <= i^0 LOG: NEXT CALL check - disable LOG: CALL check - Post:1 + n^0 <= i^0 - Process 3 * Exit transition: * Postcondition : 1 + n^0 <= i^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.011852s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.011904s Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.153138s Time used: 0.152941 Improving Solution with cost 51 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.012703s Time used: 1.0127 LOG: SAT solveNonLinear - Elapsed time: 1.165841s Cost: 51; Total time: 1.16564 Failed at location 6: 1 + n^0 <= i^0 Before Improving: Quasi-invariant at l6: 1 + n^0 <= i^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.005638s Remaining time after improvement: 0.996422 Some transition disabled by a set of quasi-invariant(s): Quasi-invariant at l6: 1 + n^0 <= i^0 LOG: NEXT CALL check - disable LOG: CALL check - Post:1 + n^0 <= i^0 - Process 4 * Exit transition: * Postcondition : 1 + n^0 <= i^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.011615s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.011666s Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.000113s Time used: 1.00001 LOG: Postcondition is not implied - no solution > Postcondition is not implied! LOG: RETURN check - Elapsed time: 3.404095s Cannot prove unreachability Proving non-termination of subgraph 2 Transitions: 0, l^0 -> 1 + l^0, rest remain the same}> 0, l^0 -> 1 + l^0, rest remain the same}> 0, l^0 -> 1 + l^0, rest remain the same}> 0, l^0 -> 1 + l^0, rest remain the same}> -1 + i^0, rest remain the same}> -1 + i^0, r^0 -> undef344, rest remain the same}> -1 + i^0, r^0 -> undef344, rest remain the same}> -1 + i^0, r^0 -> undef477, rest remain the same}> 1 + k^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + m^0, rest remain the same}> 1 + m^0, rest remain the same}> 0, l^0 -> 1 + l^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> undef587, rest remain the same}> undef344, rest remain the same}> undef344, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef344, rest remain the same}> undef344, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef344, rest remain the same}> undef344, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef344, rest remain the same}> undef344, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef344, rest remain the same}> undef344, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef344, rest remain the same}> undef344, rest remain the same}> undef477, rest remain the same}> Variables: l^0, m^0, n^0, r^0, i^0, k^0, iter^0, tmp___2^0, __const_30^0 Checking conditional non-termination of SCC {l9, l13, l15, l22}... EXIT TRANSITIONS: Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 5.000149s Time used: 5.00002 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 5.017213s Time used: 5.00016 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 5.033448s Time used: 5.00017 > Checking if the negation of the conditions of every pending exit is quasi-invariant... NO Proving non-termination of subgraph 2 Transitions: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> undef587, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef477, rest remain the same}> undef587, rest remain the same}> undef477, rest remain the same}> Variables: __const_30^0, i^0, iter^0, l^0, m^0, n^0, r^0, tmp___2^0 Checking conditional non-termination of SCC {l9, l22}... EXIT TRANSITIONS: Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.609907s Time used: 1.6098 LOG: SAT solveNonLinear - Elapsed time: 1.609907s Cost: 0; Total time: 1.6098 Minimizing number of undef constraints... LOG: CALL solveNonLinear LOG: RETURN solveNonLinear - Elapsed time: 0.161985s Number of undef constraints reduced! Non-termination implied by a set of quasi-invariant(s): Quasi-invariant at l9: 1 + l^0 <= m^0 Quasi-invariant at l22: 1 + l^0 <= m^0 Strengthening and disabling EXIT transitions... Closed exits from l9: 4 Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1 + iter^0, tmp___2^0 -> iter^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef587, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef477, rest remain the same}> Calling reachability with... Transition: Conditions: OPEN EXITS: --- Reachability graph --- > Graph without transitions. Calling reachability with... Transition: 0, rest remain the same}> Conditions: OPEN EXITS: 0, rest remain the same}> (condsUp: l^0 <= n^0) --- Reachability graph --- > Graph without transitions. Calling reachability with... Transition: Conditions: 1 + n^0 <= i^0, l^0 <= n^0, OPEN EXITS: > Conditions are reachable! Program does NOT terminate