NO Solver Timeout: 4 Global Timeout: 300 No parsing errors! Init Location: 0 Transitions: (1 + m^0)}> (0 + undef28), pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30}> (~(1) + pi^0), wpos^0 -> 0}> (1 + wpos^0)}> (~(1) + m^0)}> (1 + pos^0)}> (~(1) + z^0)}> (0 + undef178), pos^0 -> 0, seq^0 -> undef178, wpos^0 -> 0, z^0 -> undef180}> (~(1) + pi^0), wpos^0 -> 0}> (1 + wpos^0)}> undef272}> (1 + pos^0)}> (~(1) + z^0)}> undef323, max^0 -> undef324, n^0 -> undef325, pi^0 -> (0 + undef328), pos^0 -> 0, seq^0 -> undef328, wpos^0 -> 0, z^0 -> undef330}> undef341}> Fresh variables: undef28, undef30, undef178, undef180, undef272, undef323, undef324, undef325, undef328, undef330, undef341, Undef variables: undef28, undef30, undef178, undef180, undef272, undef323, undef324, undef325, undef328, undef330, undef341, Abstraction variables: Exit nodes: Accepting locations: Asserts: Preprocessed LLVMGraph Init Location: 0 Transitions: undef341, z^0 -> (~(1) + z^0)}> undef341}> undef341, pi^0 -> (0 + undef178), pos^0 -> 0, seq^0 -> undef178, wpos^0 -> 0, z^0 -> undef180}> undef341, pi^0 -> (0 + undef178), pos^0 -> 0, seq^0 -> undef178, wpos^0 -> 0, z^0 -> undef180}> undef341, pi^0 -> (~(1) + pi^0), wpos^0 -> 0}> undef341, wpos^0 -> (1 + wpos^0)}> undef341, pos^0 -> (1 + pos^0)}> undef272, m^0 -> (~(1) + m^0), z^0 -> (~(1) + z^0)}> undef272, z^0 -> (~(1) + z^0)}> undef272, m^0 -> (1 + m^0), z^0 -> (~(1) + z^0)}> undef272, m^0 -> (~(1) + m^0)}> undef272}> undef272, m^0 -> (1 + m^0)}> undef272, m^0 -> (~(1) + m^0), pi^0 -> (0 + undef28), pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30}> undef272, pi^0 -> (0 + undef28), pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30}> undef272, m^0 -> (1 + m^0), pi^0 -> (0 + undef28), pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30}> undef272, m^0 -> (~(1) + m^0), pi^0 -> (0 + undef28), pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30}> undef272, pi^0 -> (0 + undef28), pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30}> undef272, m^0 -> (1 + m^0), pi^0 -> (0 + undef28), pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30}> undef272, m^0 -> (~(1) + m^0), pi^0 -> (~(1) + pi^0), wpos^0 -> 0}> undef272, pi^0 -> (~(1) + pi^0), wpos^0 -> 0}> undef272, m^0 -> (1 + m^0), pi^0 -> (~(1) + pi^0), wpos^0 -> 0}> undef272, m^0 -> (~(1) + m^0), wpos^0 -> (1 + wpos^0)}> undef272, wpos^0 -> (1 + wpos^0)}> undef272, m^0 -> (1 + m^0), wpos^0 -> (1 + wpos^0)}> undef272, m^0 -> (~(1) + m^0), pos^0 -> (1 + pos^0)}> undef272, pos^0 -> (1 + pos^0)}> undef272, m^0 -> (1 + m^0), pos^0 -> (1 + pos^0)}> Fresh variables: undef28, undef30, undef178, undef180, undef272, undef323, undef324, undef325, undef328, undef330, undef341, Undef variables: undef28, undef30, undef178, undef180, undef272, undef323, undef324, undef325, undef328, undef330, undef341, Abstraction variables: Exit nodes: Accepting locations: Asserts: ************************************************************* ******************************************************************************************* *********************** WORKING TRANSITION SYSTEM (DAG) *********************** ******************************************************************************************* Init Location: 0 Graph 0: Transitions: Variables: Graph 1: Transitions: undef341, z^0 -> -1 + z^0, rest remain the same}> undef341, rest remain the same}> undef341, pi^0 -> undef178, pos^0 -> 0, seq^0 -> undef178, wpos^0 -> 0, z^0 -> undef180, rest remain the same}> undef341, pi^0 -> undef178, pos^0 -> 0, seq^0 -> undef178, wpos^0 -> 0, z^0 -> undef180, rest remain the same}> undef341, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> undef341, wpos^0 -> 1 + wpos^0, rest remain the same}> undef341, pos^0 -> 1 + pos^0, rest remain the same}> undef272, m^0 -> -1 + m^0, z^0 -> -1 + z^0, rest remain the same}> undef272, z^0 -> -1 + z^0, rest remain the same}> undef272, m^0 -> 1 + m^0, z^0 -> -1 + z^0, rest remain the same}> undef272, m^0 -> -1 + m^0, rest remain the same}> undef272, rest remain the same}> undef272, m^0 -> 1 + m^0, rest remain the same}> undef272, m^0 -> -1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> undef272, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> undef272, m^0 -> 1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> undef272, m^0 -> -1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> undef272, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> undef272, m^0 -> 1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> undef272, m^0 -> -1 + m^0, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> undef272, wpos^0 -> 1 + wpos^0, rest remain the same}> undef272, m^0 -> 1 + m^0, wpos^0 -> 1 + wpos^0, rest remain the same}> undef272, m^0 -> -1 + m^0, pos^0 -> 1 + pos^0, rest remain the same}> Variables: c1^0, m^0, z^0, pos^0, pi^0, seq^0, wpos^0, c2^0, max^0 Graph 2: Transitions: Variables: Precedence: Graph 0 Graph 1 Graph 2 Map Locations to Subgraph: ( 0 , 0 ) ( 2 , 1 ) ( 12 , 1 ) ( 21 , 2 ) ******************************************************************************************* ******************************** CHECKING ASSERTIONS ******************************** ******************************************************************************************* Proving termination of subgraph 0 Proving termination of subgraph 1 Checking unfeasibility... Time used: 0.193279 Some transition disabled by a set of invariant(s): Invariant at l2: wpos^0 <= pos^0 Invariant at l12: wpos^0 <= pos^0 Strengthening and disabling transitions... > It's unfeasible. Removing transition: undef272, m^0 -> 1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef341, pi^0 -> undef178, pos^0 -> 0, seq^0 -> undef178, wpos^0 -> 0, z^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, pi^0 -> undef178, pos^0 -> 0, seq^0 -> undef178, wpos^0 -> 0, z^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, wpos^0 -> 1 + wpos^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, pos^0 -> 1 + pos^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): undef272, m^0 -> -1 + m^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> 1 + m^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> -1 + m^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> 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: undef272, m^0 -> -1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef272, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> -1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> 1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> -1 + m^0, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, wpos^0 -> 1 + wpos^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> 1 + m^0, wpos^0 -> 1 + wpos^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> -1 + m^0, pos^0 -> 1 + pos^0, rest remain the same}> Checking unfeasibility... Time used: 0.360746 Some transition disabled by a set of invariant(s): Invariant at l2: pos^0 <= 1 Invariant at l12: pos^0 <= 1 Strengthening and disabling transitions... > It's unfeasible. Removing transition: undef272, m^0 -> -1 + m^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef341, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, pi^0 -> undef178, pos^0 -> 0, seq^0 -> undef178, wpos^0 -> 0, z^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, wpos^0 -> 1 + wpos^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, pos^0 -> 1 + pos^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): undef272, m^0 -> -1 + m^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> 1 + m^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef272, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef272, m^0 -> 1 + m^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> -1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> 1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> -1 + m^0, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, wpos^0 -> 1 + wpos^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> 1 + m^0, wpos^0 -> 1 + wpos^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> -1 + m^0, pos^0 -> 1 + pos^0, rest remain the same}> Checking unfeasibility... Time used: 0.956093 Checking conditional termination of SCC {l2, l12}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.022161s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 1.001093s Trying to remove transition: undef272, m^0 -> -1 + m^0, pos^0 -> 1 + pos^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.117345s Time used: 0.097263 Trying to remove transition: undef272, m^0 -> 1 + m^0, wpos^0 -> 1 + wpos^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.168598s Time used: 0.167522 Trying to remove transition: undef272, wpos^0 -> 1 + wpos^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.174071s Time used: 0.172822 Trying to remove transition: undef272, m^0 -> -1 + m^0, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.605072s Time used: 0.60368 Trying to remove transition: undef272, m^0 -> 1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.001903s Time used: 4.00013 Trying to remove transition: undef272, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.607933s Time used: 0.596593 Trying to remove transition: undef272, m^0 -> -1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.402699s Time used: 0.400662 Trying to remove transition: undef272, m^0 -> 1 + m^0, z^0 -> -1 + z^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.204074s Time used: 0.202151 Trying to remove transition: undef272, z^0 -> -1 + z^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.136689s Time used: 0.134946 Trying to remove transition: undef272, m^0 -> -1 + m^0, z^0 -> -1 + z^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.085765s Time used: 0.084105 Trying to remove transition: undef341, pos^0 -> 1 + pos^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.127467s Time used: 0.126049 Trying to remove transition: undef341, wpos^0 -> 1 + wpos^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.154984s Time used: 0.129042 Trying to remove transition: undef341, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.547881s Time used: 0.536318 Trying to remove transition: undef341, pi^0 -> undef178, pos^0 -> 0, seq^0 -> undef178, wpos^0 -> 0, z^0 -> undef180, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.407462s Time used: 0.405706 Trying to remove transition: undef341, z^0 -> -1 + z^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.123061s Time used: 0.121197 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.011931s Time used: 4.0001 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.008644s Time used: 4.00006 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.015103s Time used: 1.00002 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.654442s Time used: 1.63263 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.002040s Time used: 1.00203 LOG: SAT solveNonLinear - Elapsed time: 2.656481s Cost: 1; Total time: 2.63465 Termination implied by a set of invariant(s): Invariant at l2: 0 <= 1 + pos^0 Invariant at l12: 0 <= 1 + pos^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, pi^0 -> undef178, pos^0 -> 0, seq^0 -> undef178, wpos^0 -> 0, z^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, wpos^0 -> 1 + wpos^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, pos^0 -> 1 + pos^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): undef272, m^0 -> -1 + m^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> 1 + m^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> -1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> 1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> -1 + m^0, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, wpos^0 -> 1 + wpos^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> 1 + m^0, wpos^0 -> 1 + wpos^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> -1 + m^0, pos^0 -> 1 + pos^0, 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): undef341, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, pi^0 -> undef178, pos^0 -> 0, seq^0 -> undef178, wpos^0 -> 0, z^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, wpos^0 -> 1 + wpos^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, pos^0 -> 1 + pos^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): undef272, m^0 -> -1 + m^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> 1 + m^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> -1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> 1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> -1 + m^0, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, wpos^0 -> 1 + wpos^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> 1 + m^0, wpos^0 -> 1 + wpos^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> -1 + m^0, pos^0 -> 1 + pos^0, rest remain the same}> Quasi-ranking function: 50000 - pos^0 - 2*seq^0 New Graphs: Transitions: undef341, z^0 -> -1 + z^0, rest remain the same}> undef341, pi^0 -> undef178, pos^0 -> 0, seq^0 -> undef178, wpos^0 -> 0, z^0 -> undef180, rest remain the same}> undef341, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> undef341, wpos^0 -> 1 + wpos^0, rest remain the same}> undef341, pos^0 -> 1 + pos^0, rest remain the same}> undef272, m^0 -> -1 + m^0, z^0 -> -1 + z^0, rest remain the same}> undef272, z^0 -> -1 + z^0, rest remain the same}> undef272, m^0 -> 1 + m^0, z^0 -> -1 + z^0, rest remain the same}> undef272, m^0 -> -1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> undef272, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> undef272, m^0 -> 1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> undef272, m^0 -> -1 + m^0, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> undef272, wpos^0 -> 1 + wpos^0, rest remain the same}> undef272, m^0 -> 1 + m^0, wpos^0 -> 1 + wpos^0, rest remain the same}> undef272, m^0 -> -1 + m^0, pos^0 -> 1 + pos^0, rest remain the same}> Variables: c1^0, c2^0, m^0, max^0, pi^0, pos^0, seq^0, wpos^0, z^0 Checking conditional termination of SCC {l2, l12}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.010728s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 2.004497s Trying to remove transition: undef272, m^0 -> -1 + m^0, pos^0 -> 1 + pos^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.173215s Time used: 0.171231 Trying to remove transition: undef272, m^0 -> 1 + m^0, wpos^0 -> 1 + wpos^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.221387s Time used: 0.219381 Trying to remove transition: undef272, wpos^0 -> 1 + wpos^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.190304s Time used: 0.188139 Trying to remove transition: undef272, m^0 -> -1 + m^0, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.577724s Time used: 0.575552 Trying to remove transition: undef272, m^0 -> 1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.716595s Time used: 0.714389 Trying to remove transition: undef272, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.002904s Time used: 4.00027 Trying to remove transition: undef272, m^0 -> -1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.514218s Time used: 0.501993 Trying to remove transition: undef272, m^0 -> 1 + m^0, z^0 -> -1 + z^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.172094s Time used: 0.169755 Trying to remove transition: undef272, z^0 -> -1 + z^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.168646s Time used: 0.166605 Trying to remove transition: undef272, m^0 -> -1 + m^0, z^0 -> -1 + z^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.117734s Time used: 0.115938 Trying to remove transition: undef341, pos^0 -> 1 + pos^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.198926s Time used: 0.197373 Trying to remove transition: undef341, wpos^0 -> 1 + wpos^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.146048s Time used: 0.144467 Trying to remove transition: undef341, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.512974s Time used: 0.500213 Trying to remove transition: undef341, pi^0 -> undef178, pos^0 -> 0, seq^0 -> undef178, wpos^0 -> 0, z^0 -> undef180, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.001936s Time used: 4.00006 Trying to remove transition: undef341, z^0 -> -1 + z^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.125037s Time used: 0.115612 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 3.240480s Time used: 3.22613 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.776011s Time used: 0.776001 LOG: SAT solveNonLinear - Elapsed time: 4.016491s Cost: 1; Total time: 4.00213 Failed at location 2: m^0 <= 0 Before Improving: Quasi-invariant at l2: m^0 <= 0 Quasi-invariant at l12: 1 <= 0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.033071s Remaining time after improvement: 0.979955 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l2: m^0 <= 0 Quasi-invariant at l12: 1 <= 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: undef341, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef341, pi^0 -> undef178, pos^0 -> 0, seq^0 -> undef178, wpos^0 -> 0, z^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef341, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef341, wpos^0 -> 1 + wpos^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef341, pos^0 -> 1 + pos^0, rest remain the same}> 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: undef272, m^0 -> -1 + m^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef272, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef272, m^0 -> 1 + m^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef272, m^0 -> -1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef272, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef272, m^0 -> 1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef272, m^0 -> -1 + m^0, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef272, wpos^0 -> 1 + wpos^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef272, m^0 -> 1 + m^0, wpos^0 -> 1 + wpos^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef272, m^0 -> -1 + m^0, pos^0 -> 1 + pos^0, rest remain the same}> [ Termination Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef341, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef341, pi^0 -> undef178, pos^0 -> 0, seq^0 -> undef178, wpos^0 -> 0, z^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef341, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef341, wpos^0 -> 1 + wpos^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef341, pos^0 -> 1 + pos^0, rest remain the same}> 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: undef272, m^0 -> -1 + m^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef272, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef272, m^0 -> 1 + m^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef272, m^0 -> -1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef272, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef272, m^0 -> 1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef272, m^0 -> -1 + m^0, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef272, wpos^0 -> 1 + wpos^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef272, m^0 -> 1 + m^0, wpos^0 -> 1 + wpos^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef272, m^0 -> -1 + m^0, pos^0 -> 1 + pos^0, rest remain the same}> New Graphs: INVARIANTS: 2: 0 <= 1 + pos^0 , 12: 0 <= 1 + pos^0 , Quasi-INVARIANTS to narrow Graph: 2: 12: Calling Safety with literal m^0 <= 0 and entry LOG: CALL check - Post:m^0 <= 0 - Process 1 * Exit transition: * Postcondition : m^0 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003275s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.003367s INVARIANTS: 2: 12: Quasi-INVARIANTS to narrow Graph: 2: m^0 <= 0 , 12: 1 <= 0 , Narrowing transition: undef341, z^0 -> -1 + z^0, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef341, pi^0 -> undef178, pos^0 -> 0, seq^0 -> undef178, wpos^0 -> 0, z^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef341, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef341, wpos^0 -> 1 + wpos^0, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef341, pos^0 -> 1 + pos^0, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: LOG: Narrow transition size 1 Narrowing transition: undef272, m^0 -> -1 + m^0, z^0 -> -1 + z^0, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef272, z^0 -> -1 + z^0, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef272, m^0 -> 1 + m^0, z^0 -> -1 + z^0, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef272, m^0 -> -1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef272, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef272, m^0 -> 1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef272, m^0 -> -1 + m^0, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef272, wpos^0 -> 1 + wpos^0, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef272, m^0 -> 1 + m^0, wpos^0 -> 1 + wpos^0, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef272, m^0 -> -1 + m^0, pos^0 -> 1 + pos^0, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: undef341, z^0 -> -1 + z^0, rest remain the same}> undef341, pi^0 -> undef178, pos^0 -> 0, seq^0 -> undef178, wpos^0 -> 0, z^0 -> undef180, rest remain the same}> undef341, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> undef341, wpos^0 -> 1 + wpos^0, rest remain the same}> undef341, pos^0 -> 1 + pos^0, rest remain the same}> undef272, m^0 -> -1 + m^0, z^0 -> -1 + z^0, rest remain the same}> undef272, z^0 -> -1 + z^0, rest remain the same}> undef272, m^0 -> 1 + m^0, z^0 -> -1 + z^0, rest remain the same}> undef272, m^0 -> -1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> undef272, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> undef272, m^0 -> 1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> undef272, m^0 -> -1 + m^0, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> undef272, wpos^0 -> 1 + wpos^0, rest remain the same}> undef272, m^0 -> 1 + m^0, wpos^0 -> 1 + wpos^0, rest remain the same}> undef272, m^0 -> -1 + m^0, pos^0 -> 1 + pos^0, rest remain the same}> Variables: c1^0, m^0, z^0, pos^0, pi^0, seq^0, wpos^0, c2^0, max^0 Checking conditional termination of SCC {l2, l12}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.009889s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 1.321646s Trying to remove transition: undef272, m^0 -> -1 + m^0, pos^0 -> 1 + pos^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.113615s Time used: 0.111764 Trying to remove transition: undef272, m^0 -> 1 + m^0, wpos^0 -> 1 + wpos^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.150638s Time used: 0.148904 Trying to remove transition: undef272, wpos^0 -> 1 + wpos^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.212540s Time used: 0.210659 Trying to remove transition: undef272, m^0 -> -1 + m^0, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.599905s Time used: 0.598097 Trying to remove transition: undef272, m^0 -> 1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.002189s Time used: 4.00006 Trying to remove transition: undef272, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.500005s Time used: 0.489763 Trying to remove transition: undef272, m^0 -> -1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.409359s Time used: 0.406981 Trying to remove transition: undef272, m^0 -> 1 + m^0, z^0 -> -1 + z^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.226706s Time used: 0.224509 Trying to remove transition: undef272, z^0 -> -1 + z^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.104588s Time used: 0.102658 Trying to remove transition: undef272, m^0 -> -1 + m^0, z^0 -> -1 + z^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.119925s Time used: 0.118145 Trying to remove transition: undef341, pos^0 -> 1 + pos^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.137381s Time used: 0.135847 Trying to remove transition: undef341, wpos^0 -> 1 + wpos^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.162611s Time used: 0.150758 Trying to remove transition: undef341, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.531697s Time used: 0.519894 Trying to remove transition: undef341, pi^0 -> undef178, pos^0 -> 0, seq^0 -> undef178, wpos^0 -> 0, z^0 -> undef180, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.351529s Time used: 0.349706 Trying to remove transition: undef341, z^0 -> -1 + z^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.139112s Time used: 0.13719 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.016305s Time used: 4.00433 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.005569s Time used: 4.00052 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.012935s Time used: 1.00001 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.878533s Time used: 1.85634 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.002646s Time used: 1.00263 LOG: SAT solveNonLinear - Elapsed time: 2.881179s Cost: 1; Total time: 2.85897 Termination implied by a set of invariant(s): Invariant at l2: wpos^0 <= pos^0 Invariant at l12: pos^0 <= 1 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, pi^0 -> undef178, pos^0 -> 0, seq^0 -> undef178, wpos^0 -> 0, z^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, wpos^0 -> 1 + wpos^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, pos^0 -> 1 + pos^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): undef272, m^0 -> -1 + m^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> 1 + m^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> -1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> 1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> -1 + m^0, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, wpos^0 -> 1 + wpos^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> 1 + m^0, wpos^0 -> 1 + wpos^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> -1 + m^0, pos^0 -> 1 + pos^0, 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): undef341, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, pi^0 -> undef178, pos^0 -> 0, seq^0 -> undef178, wpos^0 -> 0, z^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, wpos^0 -> 1 + wpos^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, pos^0 -> 1 + pos^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): undef272, m^0 -> -1 + m^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> 1 + m^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> -1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> 1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> -1 + m^0, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, wpos^0 -> 1 + wpos^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> 1 + m^0, wpos^0 -> 1 + wpos^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> -1 + m^0, pos^0 -> 1 + pos^0, rest remain the same}> Quasi-ranking function: 50000 - pos^0 - 2*seq^0 New Graphs: Transitions: undef341, z^0 -> -1 + z^0, rest remain the same}> undef341, pi^0 -> undef178, pos^0 -> 0, seq^0 -> undef178, wpos^0 -> 0, z^0 -> undef180, rest remain the same}> undef341, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> undef341, wpos^0 -> 1 + wpos^0, rest remain the same}> undef341, pos^0 -> 1 + pos^0, rest remain the same}> undef272, m^0 -> -1 + m^0, z^0 -> -1 + z^0, rest remain the same}> undef272, z^0 -> -1 + z^0, rest remain the same}> undef272, m^0 -> 1 + m^0, z^0 -> -1 + z^0, rest remain the same}> undef272, m^0 -> -1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> undef272, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> undef272, m^0 -> 1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> undef272, m^0 -> -1 + m^0, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> undef272, wpos^0 -> 1 + wpos^0, rest remain the same}> undef272, m^0 -> 1 + m^0, wpos^0 -> 1 + wpos^0, rest remain the same}> undef272, m^0 -> -1 + m^0, pos^0 -> 1 + pos^0, rest remain the same}> Variables: c1^0, c2^0, m^0, max^0, pi^0, pos^0, seq^0, wpos^0, z^0 Checking conditional termination of SCC {l2, l12}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.012063s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 2.005100s Trying to remove transition: undef272, m^0 -> -1 + m^0, pos^0 -> 1 + pos^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.162751s Time used: 0.160739 Trying to remove transition: undef272, m^0 -> 1 + m^0, wpos^0 -> 1 + wpos^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.225066s Time used: 0.222811 Trying to remove transition: undef272, wpos^0 -> 1 + wpos^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.165138s Time used: 0.163056 Trying to remove transition: undef272, m^0 -> -1 + m^0, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.594817s Time used: 0.592811 Trying to remove transition: undef272, m^0 -> 1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.749802s Time used: 0.747587 Trying to remove transition: undef272, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.002666s Time used: 4.00001 Trying to remove transition: undef272, m^0 -> -1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.592892s Time used: 0.580597 Trying to remove transition: undef272, m^0 -> 1 + m^0, z^0 -> -1 + z^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.192560s Time used: 0.190259 Trying to remove transition: undef272, z^0 -> -1 + z^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.125004s Time used: 0.123045 Trying to remove transition: undef272, m^0 -> -1 + m^0, z^0 -> -1 + z^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.137023s Time used: 0.135206 Trying to remove transition: undef341, pos^0 -> 1 + pos^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.180416s Time used: 0.178759 Trying to remove transition: undef341, wpos^0 -> 1 + wpos^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.154799s Time used: 0.153199 Trying to remove transition: undef341, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.649140s Time used: 0.63714 Trying to remove transition: undef341, pi^0 -> undef178, pos^0 -> 0, seq^0 -> undef178, wpos^0 -> 0, z^0 -> undef180, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.437714s Time used: 0.435822 Trying to remove transition: undef341, z^0 -> -1 + z^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.095443s Time used: 0.093429 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.015799s Time used: 4.00344 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.004830s Time used: 4.00001 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.012877s Time used: 1.00001 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 2.170818s Time used: 2.1486 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.002959s Time used: 1.00295 LOG: SAT solveNonLinear - Elapsed time: 3.173777s Cost: 1; Total time: 3.15155 Termination implied by a set of invariant(s): Invariant at l2: pi^0 <= seq^0 + wpos^0 Invariant at l12: pi^0 <= seq^0 + wpos^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, pi^0 -> undef178, pos^0 -> 0, seq^0 -> undef178, wpos^0 -> 0, z^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, wpos^0 -> 1 + wpos^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, pos^0 -> 1 + pos^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): undef272, m^0 -> -1 + m^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> 1 + m^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> -1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> 1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> -1 + m^0, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, wpos^0 -> 1 + wpos^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> 1 + m^0, wpos^0 -> 1 + wpos^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> -1 + m^0, pos^0 -> 1 + pos^0, 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): undef341, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, pi^0 -> undef178, pos^0 -> 0, seq^0 -> undef178, wpos^0 -> 0, z^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, wpos^0 -> 1 + wpos^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, pos^0 -> 1 + pos^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): undef272, m^0 -> -1 + m^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> 1 + m^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> -1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> 1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> -1 + m^0, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, wpos^0 -> 1 + wpos^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> 1 + m^0, wpos^0 -> 1 + wpos^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> -1 + m^0, pos^0 -> 1 + pos^0, rest remain the same}> Quasi-ranking function: 50000 - seq^0 New Graphs: Transitions: undef341, z^0 -> -1 + z^0, rest remain the same}> undef341, pi^0 -> undef178, pos^0 -> 0, seq^0 -> undef178, wpos^0 -> 0, z^0 -> undef180, rest remain the same}> undef341, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> undef341, wpos^0 -> 1 + wpos^0, rest remain the same}> undef341, pos^0 -> 1 + pos^0, rest remain the same}> undef272, m^0 -> -1 + m^0, z^0 -> -1 + z^0, rest remain the same}> undef272, z^0 -> -1 + z^0, rest remain the same}> undef272, m^0 -> 1 + m^0, z^0 -> -1 + z^0, rest remain the same}> undef272, m^0 -> -1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> undef272, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> undef272, m^0 -> 1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> undef272, m^0 -> -1 + m^0, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> undef272, wpos^0 -> 1 + wpos^0, rest remain the same}> undef272, m^0 -> 1 + m^0, wpos^0 -> 1 + wpos^0, rest remain the same}> undef272, m^0 -> -1 + m^0, pos^0 -> 1 + pos^0, rest remain the same}> Variables: c1^0, c2^0, m^0, max^0, pi^0, pos^0, seq^0, wpos^0, z^0 Checking conditional termination of SCC {l2, l12}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.014176s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 2.008704s Trying to remove transition: undef272, m^0 -> -1 + m^0, pos^0 -> 1 + pos^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.303783s Time used: 0.3015 Trying to remove transition: undef272, m^0 -> 1 + m^0, wpos^0 -> 1 + wpos^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.393354s Time used: 0.391024 Trying to remove transition: undef272, wpos^0 -> 1 + wpos^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.363639s Time used: 0.361084 Trying to remove transition: undef272, m^0 -> -1 + m^0, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.924549s Time used: 0.922059 Trying to remove transition: undef272, m^0 -> 1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.710590s Time used: 0.708071 Trying to remove transition: undef272, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.977882s Time used: 0.975241 Trying to remove transition: undef272, m^0 -> -1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.574998s Time used: 0.572341 Trying to remove transition: undef272, m^0 -> 1 + m^0, z^0 -> -1 + z^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.293463s Time used: 0.291014 Trying to remove transition: undef272, z^0 -> -1 + z^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.213215s Time used: 0.210727 Trying to remove transition: undef272, m^0 -> -1 + m^0, z^0 -> -1 + z^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.170913s Time used: 0.168606 Trying to remove transition: undef341, pos^0 -> 1 + pos^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.254931s Time used: 0.252922 Trying to remove transition: undef341, wpos^0 -> 1 + wpos^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.201866s Time used: 0.200009 Trying to remove transition: undef341, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.841682s Time used: 0.839828 Trying to remove transition: undef341, pi^0 -> undef178, pos^0 -> 0, seq^0 -> undef178, wpos^0 -> 0, z^0 -> undef180, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.474961s Time used: 0.472792 Trying to remove transition: undef341, z^0 -> -1 + z^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.154262s Time used: 0.1521 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.005307s Time used: 4.00333 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.004790s Time used: 4.00023 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.014004s Time used: 1.00073 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 2.005709s Time used: 1.98281 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.003362s Time used: 1.00335 LOG: SAT solveNonLinear - Elapsed time: 3.009071s Cost: 1; Total time: 2.98616 Termination implied by a set of invariant(s): Invariant at l2: 0 <= 1 + pos^0 Invariant at l12: pos^0 + wpos^0 <= 1 + c1^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): undef341, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, pi^0 -> undef178, pos^0 -> 0, seq^0 -> undef178, wpos^0 -> 0, z^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, wpos^0 -> 1 + wpos^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, pos^0 -> 1 + pos^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): undef272, m^0 -> -1 + m^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> 1 + m^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> -1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> 1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> -1 + m^0, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, wpos^0 -> 1 + wpos^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> 1 + m^0, wpos^0 -> 1 + wpos^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> -1 + m^0, pos^0 -> 1 + pos^0, 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): undef341, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, pi^0 -> undef178, pos^0 -> 0, seq^0 -> undef178, wpos^0 -> 0, z^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, wpos^0 -> 1 + wpos^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, pos^0 -> 1 + pos^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): undef272, m^0 -> -1 + m^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> 1 + m^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> -1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> 1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> -1 + m^0, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, wpos^0 -> 1 + wpos^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> 1 + m^0, wpos^0 -> 1 + wpos^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> -1 + m^0, pos^0 -> 1 + pos^0, rest remain the same}> Quasi-ranking function: 50000 + max^0 - seq^0 New Graphs: Transitions: undef341, z^0 -> -1 + z^0, rest remain the same}> undef341, pi^0 -> undef178, pos^0 -> 0, seq^0 -> undef178, wpos^0 -> 0, z^0 -> undef180, rest remain the same}> undef341, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> undef341, wpos^0 -> 1 + wpos^0, rest remain the same}> undef341, pos^0 -> 1 + pos^0, rest remain the same}> undef272, m^0 -> -1 + m^0, z^0 -> -1 + z^0, rest remain the same}> undef272, z^0 -> -1 + z^0, rest remain the same}> undef272, m^0 -> 1 + m^0, z^0 -> -1 + z^0, rest remain the same}> undef272, m^0 -> -1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> undef272, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> undef272, m^0 -> 1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> undef272, m^0 -> -1 + m^0, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> undef272, wpos^0 -> 1 + wpos^0, rest remain the same}> undef272, m^0 -> 1 + m^0, wpos^0 -> 1 + wpos^0, rest remain the same}> undef272, m^0 -> -1 + m^0, pos^0 -> 1 + pos^0, rest remain the same}> Variables: c1^0, c2^0, m^0, max^0, pi^0, pos^0, seq^0, wpos^0, z^0 Checking conditional termination of SCC {l2, l12}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.016788s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 2.007900s Trying to remove transition: undef272, m^0 -> -1 + m^0, pos^0 -> 1 + pos^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.514047s Time used: 0.511398 Trying to remove transition: undef272, m^0 -> 1 + m^0, wpos^0 -> 1 + wpos^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.538759s Time used: 0.536262 Trying to remove transition: undef272, wpos^0 -> 1 + wpos^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.378120s Time used: 0.375273 Trying to remove transition: undef272, m^0 -> -1 + m^0, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.329448s Time used: 1.3268 Trying to remove transition: undef272, m^0 -> 1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.938354s Time used: 0.935688 Trying to remove transition: undef272, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.877104s Time used: 0.874265 Trying to remove transition: undef272, m^0 -> -1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.014313s Time used: 1.01156 Trying to remove transition: undef272, m^0 -> 1 + m^0, z^0 -> -1 + z^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.296066s Time used: 0.293254 Trying to remove transition: undef272, z^0 -> -1 + z^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.178747s Time used: 0.176172 Trying to remove transition: undef272, m^0 -> -1 + m^0, z^0 -> -1 + z^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.268864s Time used: 0.266504 Trying to remove transition: undef341, pos^0 -> 1 + pos^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.283102s Time used: 0.280925 Trying to remove transition: undef341, wpos^0 -> 1 + wpos^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.243428s Time used: 0.241451 Trying to remove transition: undef341, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.811476s Time used: 0.809583 Trying to remove transition: undef341, pi^0 -> undef178, pos^0 -> 0, seq^0 -> undef178, wpos^0 -> 0, z^0 -> undef180, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.652853s Time used: 0.650601 Trying to remove transition: undef341, z^0 -> -1 + z^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.107227s Time used: 0.104807 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.005856s Time used: 4.00385 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.005593s Time used: 4.00022 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.013331s Time used: 1.00002 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 2.158391s Time used: 2.1356 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.003893s Time used: 1.00388 LOG: SAT solveNonLinear - Elapsed time: 3.162284s Cost: 1; Total time: 3.13948 Termination implied by a set of invariant(s): Invariant at l2: pi^0 <= seq^0 + wpos^0 Invariant at l12: 1 + pi^0 <= m^0 + pos^0 + seq^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, pi^0 -> undef178, pos^0 -> 0, seq^0 -> undef178, wpos^0 -> 0, z^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, wpos^0 -> 1 + wpos^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, pos^0 -> 1 + pos^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): undef272, m^0 -> -1 + m^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> 1 + m^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> -1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> 1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> -1 + m^0, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, wpos^0 -> 1 + wpos^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> 1 + m^0, wpos^0 -> 1 + wpos^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> -1 + m^0, pos^0 -> 1 + pos^0, 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): undef341, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, pi^0 -> undef178, pos^0 -> 0, seq^0 -> undef178, wpos^0 -> 0, z^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, wpos^0 -> 1 + wpos^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, pos^0 -> 1 + pos^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): undef272, m^0 -> -1 + m^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> 1 + m^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> -1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> 1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> -1 + m^0, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, wpos^0 -> 1 + wpos^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> 1 + m^0, wpos^0 -> 1 + wpos^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> -1 + m^0, pos^0 -> 1 + pos^0, rest remain the same}> Quasi-ranking function: 50000 - max^0 - seq^0 New Graphs: Transitions: undef341, z^0 -> -1 + z^0, rest remain the same}> undef341, pi^0 -> undef178, pos^0 -> 0, seq^0 -> undef178, wpos^0 -> 0, z^0 -> undef180, rest remain the same}> undef341, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> undef341, wpos^0 -> 1 + wpos^0, rest remain the same}> undef341, pos^0 -> 1 + pos^0, rest remain the same}> undef272, m^0 -> -1 + m^0, z^0 -> -1 + z^0, rest remain the same}> undef272, z^0 -> -1 + z^0, rest remain the same}> undef272, m^0 -> 1 + m^0, z^0 -> -1 + z^0, rest remain the same}> undef272, m^0 -> -1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> undef272, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> undef272, m^0 -> 1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> undef272, m^0 -> -1 + m^0, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> undef272, wpos^0 -> 1 + wpos^0, rest remain the same}> undef272, m^0 -> 1 + m^0, wpos^0 -> 1 + wpos^0, rest remain the same}> undef272, m^0 -> -1 + m^0, pos^0 -> 1 + pos^0, rest remain the same}> Variables: c1^0, c2^0, m^0, max^0, pi^0, pos^0, seq^0, wpos^0, z^0 Checking conditional termination of SCC {l2, l12}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.019907s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 2.007284s Trying to remove transition: undef272, m^0 -> -1 + m^0, pos^0 -> 1 + pos^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.328843s Time used: 0.326093 Trying to remove transition: undef272, m^0 -> 1 + m^0, wpos^0 -> 1 + wpos^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.445503s Time used: 0.442983 Trying to remove transition: undef272, wpos^0 -> 1 + wpos^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.434983s Time used: 0.432242 Trying to remove transition: undef272, m^0 -> -1 + m^0, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.551759s Time used: 1.54912 Trying to remove transition: undef272, m^0 -> 1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.132064s Time used: 1.12929 Trying to remove transition: undef272, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.007610s Time used: 4.00014 Trying to remove transition: undef272, m^0 -> -1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.150278s Time used: 1.14169 Trying to remove transition: undef272, m^0 -> 1 + m^0, z^0 -> -1 + z^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.453340s Time used: 0.450541 Trying to remove transition: undef272, z^0 -> -1 + z^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.244466s Time used: 0.241955 Trying to remove transition: undef272, m^0 -> -1 + m^0, z^0 -> -1 + z^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.424485s Time used: 0.422156 Trying to remove transition: undef341, pos^0 -> 1 + pos^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.371025s Time used: 0.3688 Trying to remove transition: undef341, wpos^0 -> 1 + wpos^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.227688s Time used: 0.225699 Trying to remove transition: undef341, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.074812s Time used: 1.07287 Trying to remove transition: undef341, pi^0 -> undef178, pos^0 -> 0, seq^0 -> undef178, wpos^0 -> 0, z^0 -> undef180, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.729983s Time used: 0.7276 Trying to remove transition: undef341, z^0 -> -1 + z^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.131777s Time used: 0.129266 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.003485s Time used: 4.00017 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.760996s Time used: 0.756754 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.976311s Time used: 0.964513 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.980384s Time used: 0.959564 Proving non-termination of subgraph 1 Transitions: undef341, z^0 -> -1 + z^0, rest remain the same}> undef341, pi^0 -> undef178, pos^0 -> 0, seq^0 -> undef178, wpos^0 -> 0, z^0 -> undef180, rest remain the same}> undef341, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> undef341, wpos^0 -> 1 + wpos^0, rest remain the same}> undef341, pos^0 -> 1 + pos^0, rest remain the same}> undef272, m^0 -> -1 + m^0, z^0 -> -1 + z^0, rest remain the same}> undef272, z^0 -> -1 + z^0, rest remain the same}> undef272, m^0 -> 1 + m^0, z^0 -> -1 + z^0, rest remain the same}> undef272, m^0 -> -1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> undef272, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> undef272, m^0 -> 1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> undef272, m^0 -> -1 + m^0, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> undef272, wpos^0 -> 1 + wpos^0, rest remain the same}> undef272, m^0 -> 1 + m^0, wpos^0 -> 1 + wpos^0, rest remain the same}> undef272, m^0 -> -1 + m^0, pos^0 -> 1 + pos^0, rest remain the same}> Variables: c1^0, m^0, z^0, pos^0, pi^0, seq^0, wpos^0, c2^0, max^0 Checking that every undef value has an assignment... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.011440s Checking conditional non-termination of SCC {l2, l12}... EXIT TRANSITIONS: Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.813918s Time used: 0.811724 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.538800s Time used: 0.538793 LOG: SAT solveNonLinear - Elapsed time: 1.352718s Cost: 1; Total time: 1.35052 Failed at location 2: 1 <= m^0 Before Improving: Quasi-invariant at l2: 1 <= m^0 Quasi-invariant at l12: 1 <= m^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.042095s Remaining time after improvement: 0.984308 Minimizing number of undef constraints... LOG: CALL solveNonLinear LOG: RETURN solveNonLinear - Elapsed time: 0.070446s Number of undef constraints reduced! Non-termination implied by a set of quasi-invariant(s): Quasi-invariant at l2: 1 <= m^0 Quasi-invariant at l12: 1 <= m^0 Constraint over undef '1 <= undef272' in transition: undef272, m^0 -> -1 + m^0, z^0 -> -1 + z^0, rest remain the same}> Constraint over undef '1 <= undef272' in transition: undef272, m^0 -> -1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> Constraint over undef '1 <= undef272' in transition: undef272, m^0 -> -1 + m^0, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> Constraint over undef '1 <= undef272' in transition: undef272, m^0 -> -1 + m^0, pos^0 -> 1 + pos^0, rest remain the same}> Strengthening and disabling EXIT transitions... Closed exits from l2: 3 Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, pi^0 -> undef178, pos^0 -> 0, seq^0 -> undef178, wpos^0 -> 0, z^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, wpos^0 -> 1 + wpos^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef341, pos^0 -> 1 + pos^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: undef272, m^0 -> -1 + m^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> 1 + m^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef272, m^0 -> -1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> 1 + m^0, pi^0 -> undef28, pos^0 -> 0, seq^0 -> undef28, wpos^0 -> 0, z^0 -> undef30, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef272, m^0 -> -1 + m^0, pi^0 -> -1 + pi^0, wpos^0 -> 0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, wpos^0 -> 1 + wpos^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef272, m^0 -> 1 + m^0, wpos^0 -> 1 + wpos^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef272, m^0 -> -1 + m^0, pos^0 -> 1 + pos^0, rest remain the same}> Calling reachability with... Transition: Conditions: 1 <= m^0, OPEN EXITS: --- Reachability graph --- > Graph without transitions. Calling reachability with... Transition: Conditions: 1 <= m^0, OPEN EXITS: > Conditions are reachable! Program does NOT terminate