NO Solver Timeout: 4 Global Timeout: 300 No parsing errors! Init Location: 0 Transitions: undef7}> 0, y_6^0 -> (1 + y_6^0)}> undef16}> 0}> 1, x_5^0 -> (1 + x_5^0)}> undef31}> Fresh variables: undef7, undef16, undef31, Undef variables: undef7, undef16, undef31, Abstraction variables: Exit nodes: Accepting locations: Asserts: Preprocessed LLVMGraph Init Location: 0 Transitions: undef7, b_7^0 -> 0, x_5^0 -> (1 + x_5^0), y_6^0 -> (1 + y_6^0)}> 1, x_5^0 -> (1 + x_5^0)}> Fresh variables: undef7, undef16, undef31, Undef variables: undef7, undef16, undef31, Abstraction variables: Exit nodes: Accepting locations: Asserts: ************************************************************* ******************************************************************************************* *********************** WORKING TRANSITION SYSTEM (DAG) *********************** ******************************************************************************************* Init Location: 0 Graph 0: Transitions: Variables: Graph 1: Transitions: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Variables: __disjvr_0^0, b_7^0, x_5^0, y_6^0 Graph 2: Transitions: Variables: Precedence: Graph 0 Graph 1 Graph 2 1, x_5^0 -> 1 + x_5^0, rest remain the same}> Map Locations to Subgraph: ( 0 , 0 ) ( 4 , 1 ) ( 5 , 2 ) ******************************************************************************************* ******************************** CHECKING ASSERTIONS ******************************** ******************************************************************************************* Proving termination of subgraph 0 Proving termination of subgraph 1 Checking unfeasibility... Time used: 0.002508 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000731s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001684s Trying to remove transition: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.005944s Time used: 0.005798 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.005454s Time used: 0.005037 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.007601s Time used: 0.007599 LOG: SAT solveNonLinear - Elapsed time: 0.013054s Cost: 1; Total time: 0.012636 Failed at location 4: 1 + b_7^0 + y_6^0 <= x_5^0 Before Improving: Quasi-invariant at l4: 1 + b_7^0 + y_6^0 <= x_5^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001290s Remaining time after improvement: 0.999437 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l4: 1 + b_7^0 + y_6^0 <= x_5^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: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> [ Termination Graph ] Strengthening and disabling transitions... > It's unfeasible. Removing transition: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> New Graphs: Calling Safety with literal 1 + b_7^0 + y_6^0 <= x_5^0 and entry LOG: CALL check - Post:1 + b_7^0 + y_6^0 <= x_5^0 - Process 1 * Exit transition: * Postcondition : 1 + b_7^0 + y_6^0 <= x_5^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000232s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000267s INVARIANTS: 4: Quasi-INVARIANTS to narrow Graph: 4: 1 + b_7^0 + y_6^0 <= x_5^0 , Narrowing transition: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Variables: __disjvr_0^0, b_7^0, x_5^0, y_6^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000366s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001398s Trying to remove transition: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.004106s Time used: 0.003981 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.007115s Time used: 0.006764 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.005328s Time used: 0.005326 LOG: SAT solveNonLinear - Elapsed time: 0.012443s Cost: 1; Total time: 0.01209 Failed at location 4: y_6^0 <= b_7^0 + x_5^0 Before Improving: Quasi-invariant at l4: y_6^0 <= b_7^0 + x_5^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001669s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000755s Remaining time after improvement: 0.998396 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l4: y_6^0 <= 1 + b_7^0 + x_5^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: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^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: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> New Graphs: Calling Safety with literal y_6^0 <= 1 + b_7^0 + x_5^0 and entry LOG: CALL check - Post:y_6^0 <= 1 + b_7^0 + x_5^0 - Process 2 * Exit transition: * Postcondition : y_6^0 <= 1 + b_7^0 + x_5^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000228s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000269s INVARIANTS: 4: Quasi-INVARIANTS to narrow Graph: 4: y_6^0 <= 1 + b_7^0 + x_5^0 , Narrowing transition: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Variables: __disjvr_0^0, b_7^0, x_5^0, y_6^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000408s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001508s Trying to remove transition: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.004147s Time used: 0.004051 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.001270s Time used: 4.00089 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.003935s Time used: 4.00046 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.002039s Time used: 1.00002 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.009390s Time used: 0.005805 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.007199s Time used: 0.007198 LOG: SAT solveNonLinear - Elapsed time: 0.016589s Cost: 1; Total time: 0.013003 Quasi-ranking function: 50000 - 2*x_5^0 + y_6^0 New Graphs: Transitions: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Variables: __disjvr_0^0, b_7^0, x_5^0, y_6^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000480s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001952s Trying to remove transition: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.006116s Time used: 0.005989 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.001623s Time used: 4.00121 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.004049s Time used: 4.00057 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.002387s Time used: 1.00015 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.010225s Time used: 0.0067 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.008075s Time used: 0.008073 LOG: SAT solveNonLinear - Elapsed time: 0.018300s Cost: 1; Total time: 0.014773 Termination implied by a set of invariant(s): Invariant at l4: b_7^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): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^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): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Quasi-ranking function: 50000 + b_7^0 - 2*x_5^0 + y_6^0 New Graphs: Transitions: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Variables: __disjvr_0^0, b_7^0, x_5^0, y_6^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000542s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002194s Trying to remove transition: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.006052s Time used: 0.005923 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.002025s Time used: 4.00161 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.004110s Time used: 4.00068 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.002339s Time used: 1.00012 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.010532s Time used: 0.006988 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.007833s Time used: 0.00783 LOG: SAT solveNonLinear - Elapsed time: 0.018365s Cost: 1; Total time: 0.014818 Termination implied by a set of invariant(s): Invariant at l4: 0 <= b_7^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^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): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Quasi-ranking function: 50000 - b_7^0 - 3*x_5^0 + 2*y_6^0 New Graphs: Transitions: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Variables: __disjvr_0^0, b_7^0, x_5^0, y_6^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000593s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002357s Trying to remove transition: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.006882s Time used: 0.00675 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.002117s Time used: 4.0017 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.003961s Time used: 4.00063 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.002346s Time used: 1.00006 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.013896s Time used: 0.007931 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.007677s Time used: 0.007675 LOG: SAT solveNonLinear - Elapsed time: 0.021572s Cost: 1; Total time: 0.015606 Quasi-ranking function: 50000 + b_7^0 - x_5^0 New Graphs: Transitions: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Variables: __disjvr_0^0, b_7^0, x_5^0, y_6^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000634s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002894s Trying to remove transition: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.006923s Time used: 0.006783 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.002782s Time used: 4.00227 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.004125s Time used: 4.0007 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.002395s Time used: 1.00018 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.012416s Time used: 0.008879 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.010509s Time used: 0.010507 LOG: SAT solveNonLinear - Elapsed time: 0.022925s Cost: 1; Total time: 0.019386 Quasi-ranking function: 50000 + b_7^0 - y_6^0 New Graphs: Transitions: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Variables: __disjvr_0^0, b_7^0, x_5^0, y_6^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000685s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002796s Trying to remove transition: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.007621s Time used: 0.007478 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.002843s Time used: 4.00232 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.004413s Time used: 4.00068 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.002383s Time used: 1.00017 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.013111s Time used: 0.009458 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.009989s Time used: 0.009988 LOG: SAT solveNonLinear - Elapsed time: 0.023100s Cost: 1; Total time: 0.019446 Termination implied by a set of invariant(s): Invariant at l4: 1 + x_5^0 <= b_7^0 + y_6^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^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): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Quasi-ranking function: 50000 + b_7^0 + x_5^0 - 2*y_6^0 New Graphs: Transitions: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Variables: __disjvr_0^0, b_7^0, x_5^0, y_6^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000758s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003094s Trying to remove transition: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.008252s Time used: 0.008103 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.002295s Time used: 4.00174 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.004393s Time used: 4.00075 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.002325s Time used: 1 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.013327s Time used: 0.009944 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.010415s Time used: 0.010403 LOG: SAT solveNonLinear - Elapsed time: 0.023742s Cost: 1; Total time: 0.020347 Termination implied by a set of invariant(s): Invariant at l4: b_7^0 + x_5^0 <= 1 + y_6^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^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): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Quasi-ranking function: 50000 - b_7^0 + x_5^0 - 2*y_6^0 New Graphs: Transitions: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Variables: __disjvr_0^0, b_7^0, x_5^0, y_6^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000812s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003524s Trying to remove transition: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.008229s Time used: 0.008074 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.002647s Time used: 4.00216 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.004600s Time used: 4.00079 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.002235s Time used: 1.00002 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.013655s Time used: 0.009991 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.010615s Time used: 0.010613 LOG: SAT solveNonLinear - Elapsed time: 0.024270s Cost: 1; Total time: 0.020604 Termination implied by a set of invariant(s): Invariant at l4: 1 + x_5^0 <= b_7^0 + y_6^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^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): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Quasi-ranking function: 50000 + b_7^0 - x_5^0 - y_6^0 New Graphs: Transitions: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Variables: __disjvr_0^0, b_7^0, x_5^0, y_6^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000874s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004111s Trying to remove transition: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.008377s Time used: 0.008021 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.002373s Time used: 4.00188 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.004632s Time used: 4.00088 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.008480s Time used: 1.00009 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.013992s Time used: 0.010413 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.010136s Time used: 0.010134 LOG: SAT solveNonLinear - Elapsed time: 0.024128s Cost: 1; Total time: 0.020547 Termination implied by a set of invariant(s): Invariant at l4: b_7^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): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^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): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Quasi-ranking function: 50000 - b_7^0 - x_5^0 - y_6^0 New Graphs: Transitions: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Variables: __disjvr_0^0, b_7^0, x_5^0, y_6^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000910s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004737s Trying to remove transition: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.009799s Time used: 0.009478 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.003196s Time used: 4.00263 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.004977s Time used: 4.00094 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.002498s Time used: 1.00021 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.014557s Time used: 0.010958 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.011014s Time used: 0.011012 LOG: SAT solveNonLinear - Elapsed time: 0.025572s Cost: 1; Total time: 0.02197 Quasi-ranking function: 50000 + __disjvr_0^0 + b_7^0 - 2*x_5^0 + y_6^0 New Graphs: Transitions: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Variables: __disjvr_0^0, b_7^0, x_5^0, y_6^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000994s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.005604s Trying to remove transition: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.009721s Time used: 0.009373 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.002660s Time used: 4.00208 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.004882s Time used: 4.00091 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.002273s Time used: 1.00007 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.015228s Time used: 0.011625 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.010316s Time used: 0.010315 LOG: SAT solveNonLinear - Elapsed time: 0.025544s Cost: 1; Total time: 0.02194 Termination implied by a set of invariant(s): Invariant at l4: b_7^0 <= 0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^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): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Quasi-ranking function: 50000 + 25004*__disjvr_0^0 + b_7^0 + x_5^0 - 2*y_6^0 New Graphs: Transitions: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Variables: __disjvr_0^0, b_7^0, x_5^0, y_6^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001077s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.006600s Trying to remove transition: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.010900s Time used: 0.010544 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.001491s Time used: 4.00092 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.003782s Time used: 4.00092 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.002383s Time used: 1.00017 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.016905s Time used: 0.013114 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.010526s Time used: 0.010524 LOG: SAT solveNonLinear - Elapsed time: 0.027431s Cost: 1; Total time: 0.023638 Termination implied by a set of invariant(s): Invariant at l4: 0 <= 1 + b_7^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^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): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Quasi-ranking function: 50000 - __disjvr_0^0 + b_7^0 + x_5^0 - 2*y_6^0 New Graphs: Transitions: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Variables: __disjvr_0^0, b_7^0, x_5^0, y_6^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001125s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.006361s Trying to remove transition: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.011166s Time used: 0.010816 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.004026s Time used: 4.00351 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.004547s Time used: 4.00183 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.002355s Time used: 1.0001 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.018046s Time used: 0.013876 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.012274s Time used: 0.012248 LOG: SAT solveNonLinear - Elapsed time: 0.030320s Cost: 1; Total time: 0.026124 Termination implied by a set of invariant(s): Invariant at l4: 1 + x_5^0 <= y_6^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^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): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Quasi-ranking function: 50000 - 16668*__disjvr_0^0 - b_7^0 - x_5^0 - y_6^0 New Graphs: Transitions: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Variables: __disjvr_0^0, b_7^0, x_5^0, y_6^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001229s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.005836s Trying to remove transition: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.011203s Time used: 0.010689 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.003003s Time used: 4.00247 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.004900s Time used: 4.00107 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.002363s Time used: 1.00001 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.020128s Time used: 0.01455 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.009800s Time used: 0.009798 LOG: SAT solveNonLinear - Elapsed time: 0.029928s Cost: 1; Total time: 0.024348 Termination implied by a set of invariant(s): Invariant at l4: 0 <= 1 + b_7^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^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): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Quasi-ranking function: 50000 + __disjvr_0^0 - b_7^0 + x_5^0 - 2*y_6^0 New Graphs: Transitions: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Variables: __disjvr_0^0, b_7^0, x_5^0, y_6^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001267s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.006665s Trying to remove transition: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.012512s Time used: 0.012101 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.003697s Time used: 4.00315 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.005750s Time used: 4.00099 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.002227s Time used: 1.00001 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.018538s Time used: 0.014402 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.013252s Time used: 0.013234 LOG: SAT solveNonLinear - Elapsed time: 0.031790s Cost: 1; Total time: 0.027636 Termination implied by a set of invariant(s): Invariant at l4: 1 + x_5^0 <= b_7^0 + y_6^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^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): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Quasi-ranking function: 50000 - __disjvr_0^0 - b_7^0 + x_5^0 - 2*y_6^0 New Graphs: Transitions: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Variables: __disjvr_0^0, b_7^0, x_5^0, y_6^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001351s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.009124s Trying to remove transition: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.011518s Time used: 0.011093 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.001425s Time used: 4.00087 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.003831s Time used: 4.00096 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.002274s Time used: 1.00002 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.018953s Time used: 0.014905 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.012276s Time used: 0.012274 LOG: SAT solveNonLinear - Elapsed time: 0.031230s Cost: 1; Total time: 0.027179 Termination implied by a set of invariant(s): Invariant at l4: 1 + x_5^0 <= y_6^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^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): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Quasi-ranking function: 50000 + 50006*__disjvr_0^0 - b_7^0 - x_5^0 - y_6^0 New Graphs: Transitions: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Variables: __disjvr_0^0, b_7^0, x_5^0, y_6^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001418s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.029891s Trying to remove transition: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.012860s Time used: 0.012291 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.003447s Time used: 4.00278 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.896176s Time used: 0.891993 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.994305s Time used: 0.992535 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.019574s Time used: 0.016268 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.014380s Time used: 0.014378 LOG: SAT solveNonLinear - Elapsed time: 0.033954s Cost: 1; Total time: 0.030646 Quasi-ranking function: 50000 + __disjvr_0^0 + b_7^0 - x_5^0 - y_6^0 New Graphs: Transitions: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Variables: __disjvr_0^0, b_7^0, x_5^0, y_6^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001496s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.006994s Trying to remove transition: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.012272s Time used: 0.011666 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.931492s Time used: 0.93095 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.007397s Time used: 1.00603 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.989029s Time used: 0.987137 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.021625s Time used: 0.01739 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.014866s Time used: 0.014864 LOG: SAT solveNonLinear - Elapsed time: 0.036491s Cost: 1; Total time: 0.032254 Termination implied by a set of invariant(s): Invariant at l4: 1 + x_5^0 <= b_7^0 + y_6^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^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): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Quasi-ranking function: 50000 - __disjvr_0^0 + b_7^0 - x_5^0 - y_6^0 New Graphs: Transitions: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Variables: __disjvr_0^0, b_7^0, x_5^0, y_6^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001587s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.011693s Trying to remove transition: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.012003s Time used: 0.011504 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.921667s Time used: 0.921112 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.998572s Time used: 0.997168 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.997758s Time used: 0.99586 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.021173s Time used: 0.01678 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.015192s Time used: 0.015189 LOG: SAT solveNonLinear - Elapsed time: 0.036365s Cost: 1; Total time: 0.031969 Termination implied by a set of invariant(s): Invariant at l4: 1 + b_7^0 + x_5^0 <= y_6^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^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): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Quasi-ranking function: 50000 + __disjvr_0^0 - b_7^0 - 2*x_5^0 + y_6^0 New Graphs: Transitions: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Variables: __disjvr_0^0, b_7^0, x_5^0, y_6^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001606s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.029416s Trying to remove transition: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.012896s Time used: 0.01226 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.902295s Time used: 0.901763 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.998890s Time used: 0.997496 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.997960s Time used: 0.996111 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.021889s Time used: 0.017588 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.009906s Time used: 0.009904 LOG: SAT solveNonLinear - Elapsed time: 0.031795s Cost: 1; Total time: 0.027492 Termination implied by a set of invariant(s): Invariant at l4: 0 <= 1 + b_7^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^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): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Quasi-ranking function: 50000 - __disjvr_0^0 + b_7^0 - 2*x_5^0 + y_6^0 New Graphs: Transitions: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Variables: __disjvr_0^0, b_7^0, x_5^0, y_6^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001644s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.018989s Trying to remove transition: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.013416s Time used: 0.012781 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.916837s Time used: 0.916132 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.999104s Time used: 0.997475 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.998492s Time used: 0.996191 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.021801s Time used: 0.017677 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.013737s Time used: 0.013736 LOG: SAT solveNonLinear - Elapsed time: 0.035538s Cost: 1; Total time: 0.031413 Quasi-ranking function: 50000 - __disjvr_0^0 - b_7^0 - 2*x_5^0 + y_6^0 New Graphs: Transitions: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Variables: __disjvr_0^0, b_7^0, x_5^0, y_6^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001692s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.007727s Trying to remove transition: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.014460s Time used: 0.013807 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.923629s Time used: 0.922932 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.998756s Time used: 0.997188 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.998667s Time used: 0.996356 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.022449s Time used: 0.018394 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.010637s Time used: 0.010635 LOG: SAT solveNonLinear - Elapsed time: 0.033086s Cost: 1; Total time: 0.029029 Termination implied by a set of invariant(s): Invariant at l4: 1 + x_5^0 <= b_7^0 + y_6^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^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): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Quasi-ranking function: 50000 - __disjvr_0^0 - 2*x_5^0 + y_6^0 New Graphs: Transitions: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Variables: __disjvr_0^0, b_7^0, x_5^0, y_6^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001758s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.019485s Trying to remove transition: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.014276s Time used: 0.013616 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.912436s Time used: 0.911715 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.999070s Time used: 0.997531 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.997453s Time used: 0.995662 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.029157s Time used: 0.019806 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.011861s Time used: 0.011859 LOG: SAT solveNonLinear - Elapsed time: 0.041018s Cost: 1; Total time: 0.031665 Termination implied by a set of invariant(s): Invariant at l4: x_5^0 <= b_7^0 + y_6^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^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): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Quasi-ranking function: 50000 + x_5^0 - 2*y_6^0 New Graphs: Transitions: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Variables: __disjvr_0^0, b_7^0, x_5^0, y_6^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001796s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.020782s Trying to remove transition: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.019819s Time used: 0.019126 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.898330s Time used: 0.8976 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.998894s Time used: 0.997353 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.997699s Time used: 0.995818 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.022507s Time used: 0.018305 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.010857s Time used: 0.010855 LOG: SAT solveNonLinear - Elapsed time: 0.033364s Cost: 1; Total time: 0.02916 Termination implied by a set of invariant(s): Invariant at l4: 1 + x_5^0 <= b_7^0 + y_6^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^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): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Quasi-ranking function: 50000 - __disjvr_0^0 + x_5^0 - 2*y_6^0 New Graphs: Transitions: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Variables: __disjvr_0^0, b_7^0, x_5^0, y_6^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001862s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.017012s Trying to remove transition: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.014862s Time used: 0.014156 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.914338s Time used: 0.913614 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.998843s Time used: 0.997271 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.998150s Time used: 0.995749 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.025305s Time used: 0.021168 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.011553s Time used: 0.011551 LOG: SAT solveNonLinear - Elapsed time: 0.036858s Cost: 1; Total time: 0.032719 Termination implied by a set of invariant(s): Invariant at l4: 0 <= 1 + b_7^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^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): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Quasi-ranking function: 50000 + __disjvr_0^0 - 2*x_5^0 + y_6^0 New Graphs: Transitions: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Variables: __disjvr_0^0, b_7^0, x_5^0, y_6^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001899s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.019528s Trying to remove transition: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.015649s Time used: 0.014935 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.906481s Time used: 0.905736 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.997613s Time used: 0.996035 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.997418s Time used: 0.995577 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.025859s Time used: 0.021675 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.014894s Time used: 0.014892 LOG: SAT solveNonLinear - Elapsed time: 0.040753s Cost: 1; Total time: 0.036567 Termination implied by a set of invariant(s): Invariant at l4: 1 + b_7^0 + x_5^0 <= y_6^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^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): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Quasi-ranking function: 50000 + __disjvr_0^0 + b_7^0 - x_5^0 New Graphs: Transitions: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Variables: __disjvr_0^0, b_7^0, x_5^0, y_6^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001996s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.033331s Trying to remove transition: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.016675s Time used: 0.015906 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.888013s Time used: 0.887198 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.007944s Time used: 0.997733 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.988154s Time used: 0.986286 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.023512s Time used: 0.019321 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.013591s Time used: 0.013588 LOG: SAT solveNonLinear - Elapsed time: 0.037103s Cost: 1; Total time: 0.032909 Quasi-ranking function: 50000 + __disjvr_0^0 + x_5^0 - 2*y_6^0 New Graphs: Transitions: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Variables: __disjvr_0^0, b_7^0, x_5^0, y_6^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002031s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.045013s Trying to remove transition: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.016355s Time used: 0.015773 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.882826s Time used: 0.882044 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.998167s Time used: 0.996609 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.997613s Time used: 0.995744 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.023609s Time used: 0.019408 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.013382s Time used: 0.01338 LOG: SAT solveNonLinear - Elapsed time: 0.036991s Cost: 1; Total time: 0.032788 Termination implied by a set of invariant(s): Invariant at l4: 0 <= 1 + b_7^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^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): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Quasi-ranking function: 50000 - __disjvr_0^0 - x_5^0 - y_6^0 New Graphs: Transitions: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Variables: __disjvr_0^0, b_7^0, x_5^0, y_6^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002091s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.041074s Trying to remove transition: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.015733s Time used: 0.014937 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.884410s Time used: 0.883612 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.998660s Time used: 0.99709 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.997395s Time used: 0.995457 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.024664s Time used: 0.020438 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.013638s Time used: 0.013636 LOG: SAT solveNonLinear - Elapsed time: 0.038302s Cost: 1; Total time: 0.034074 Termination implied by a set of invariant(s): Invariant at l4: 1 + x_5^0 <= y_6^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^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): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Quasi-ranking function: 50000 + __disjvr_0^0 - x_5^0 - y_6^0 New Graphs: Transitions: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Variables: __disjvr_0^0, b_7^0, x_5^0, y_6^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002129s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.081612s Trying to remove transition: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.017017s Time used: 0.016205 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.840929s Time used: 0.84012 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.998943s Time used: 0.997304 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.005940s Time used: 0.995419 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.024007s Time used: 0.01973 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.012439s Time used: 0.012437 LOG: SAT solveNonLinear - Elapsed time: 0.036446s Cost: 1; Total time: 0.032167 Termination implied by a set of invariant(s): Invariant at l4: 0 <= 1 + b_7^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^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): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Quasi-ranking function: 50000 - x_5^0 - y_6^0 New Graphs: Transitions: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Variables: __disjvr_0^0, b_7^0, x_5^0, y_6^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002209s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.048796s Trying to remove transition: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.016722s Time used: 0.015897 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.867297s Time used: 0.866446 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.998848s Time used: 0.997198 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.997412s Time used: 0.99546 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.024983s Time used: 0.020696 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.015551s Time used: 0.015548 LOG: SAT solveNonLinear - Elapsed time: 0.040534s Cost: 1; Total time: 0.036244 Termination implied by a set of invariant(s): Invariant at l4: x_5^0 <= 1 + b_7^0 + y_6^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^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): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Quasi-ranking function: 50000 - __disjvr_0^0 - x_5^0 New Graphs: Transitions: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Variables: __disjvr_0^0, b_7^0, x_5^0, y_6^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002282s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.065483s Trying to remove transition: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.016907s Time used: 0.016062 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.854659s Time used: 0.853838 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.998722s Time used: 0.997183 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.997877s Time used: 0.995352 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.024871s Time used: 0.020478 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.015730s Time used: 0.015728 LOG: SAT solveNonLinear - Elapsed time: 0.040601s Cost: 1; Total time: 0.036206 Termination implied by a set of invariant(s): Invariant at l4: x_5^0 <= 1 + y_6^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^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): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Quasi-ranking function: 50000 + __disjvr_0^0 - x_5^0 New Graphs: Transitions: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Variables: __disjvr_0^0, b_7^0, x_5^0, y_6^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002287s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.020804s Trying to remove transition: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.017817s Time used: 0.016981 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.897889s Time used: 0.897067 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.998948s Time used: 0.997183 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.997547s Time used: 0.994992 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.024761s Time used: 0.0203 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.017027s Time used: 0.01395 LOG: SAT solveNonLinear - Elapsed time: 0.041788s Cost: 1; Total time: 0.03425 Termination implied by a set of invariant(s): Invariant at l4: 0 <= 1 + b_7^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^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): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Quasi-ranking function: 50000 - x_5^0 New Graphs: Transitions: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Variables: __disjvr_0^0, b_7^0, x_5^0, y_6^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002371s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.034438s Trying to remove transition: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.017825s Time used: 0.016967 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.882766s Time used: 0.88194 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.998466s Time used: 0.996809 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.998067s Time used: 0.995475 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.025340s Time used: 0.02088 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.014595s Time used: 0.014587 LOG: SAT solveNonLinear - Elapsed time: 0.039934s Cost: 1; Total time: 0.035467 Termination implied by a set of invariant(s): Invariant at l4: x_5^0 <= 1 + b_7^0 + y_6^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^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): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Quasi-ranking function: 50000 - __disjvr_0^0 + b_7^0 - x_5^0 New Graphs: Transitions: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Variables: __disjvr_0^0, b_7^0, x_5^0, y_6^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002409s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.025109s Trying to remove transition: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.019070s Time used: 0.018336 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.892616s Time used: 0.8918 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.998568s Time used: 0.996965 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.997436s Time used: 0.994929 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.026673s Time used: 0.022344 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.015146s Time used: 0.015145 LOG: SAT solveNonLinear - Elapsed time: 0.041819s Cost: 1; Total time: 0.037489 Termination implied by a set of invariant(s): Invariant at l4: 0 <= b_7^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^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): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Quasi-ranking function: 50000 - __disjvr_0^0 - b_7^0 - x_5^0 New Graphs: Transitions: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Variables: __disjvr_0^0, b_7^0, x_5^0, y_6^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002444s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.028512s Trying to remove transition: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.017226s Time used: 0.016318 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.890405s Time used: 0.889586 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.997015s Time used: 0.995286 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.996826s Time used: 0.994905 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.026889s Time used: 0.022479 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.014631s Time used: 0.014628 LOG: SAT solveNonLinear - Elapsed time: 0.041520s Cost: 1; Total time: 0.037107 Quasi-ranking function: 50000 - y_6^0 New Graphs: Transitions: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Variables: __disjvr_0^0, b_7^0, x_5^0, y_6^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002519s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.078204s Trying to remove transition: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.018382s Time used: 0.017487 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.840692s Time used: 0.839825 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.998724s Time used: 0.997012 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.997000s Time used: 0.995011 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.024649s Time used: 0.020276 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.016071s Time used: 0.016069 LOG: SAT solveNonLinear - Elapsed time: 0.040720s Cost: 1; Total time: 0.036345 Termination implied by a set of invariant(s): Invariant at l4: 0 <= 1 + b_7^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^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): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Quasi-ranking function: 50000 + __disjvr_0^0 - b_7^0 - x_5^0 New Graphs: Transitions: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Variables: __disjvr_0^0, b_7^0, x_5^0, y_6^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002569s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.092443s Trying to remove transition: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.023302s Time used: 0.022361 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.826507s Time used: 0.825641 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.992382s Time used: 0.990774 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.997698s Time used: 0.995644 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.025349s Time used: 0.020881 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.015976s Time used: 0.015973 LOG: SAT solveNonLinear - Elapsed time: 0.041325s Cost: 1; Total time: 0.036854 Quasi-ranking function: 50000 - b_7^0 - x_5^0 New Graphs: Transitions: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Variables: __disjvr_0^0, b_7^0, x_5^0, y_6^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002654s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.017789s Trying to remove transition: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.019363s Time used: 0.018449 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.899449s Time used: 0.898579 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.998555s Time used: 0.996887 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.996815s Time used: 0.994759 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.025143s Time used: 0.020821 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.015760s Time used: 0.015759 LOG: SAT solveNonLinear - Elapsed time: 0.040904s Cost: 1; Total time: 0.03658 Termination implied by a set of invariant(s): Invariant at l4: 0 <= b_7^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^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): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Quasi-ranking function: 50000 - b_7^0 - y_6^0 New Graphs: Transitions: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Variables: __disjvr_0^0, b_7^0, x_5^0, y_6^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002683s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.068324s Trying to remove transition: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.020005s Time used: 0.019079 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.847729s Time used: 0.846864 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.998170s Time used: 0.996471 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.000125s Time used: 0.995003 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.025483s Time used: 0.021978 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.014732s Time used: 0.01473 LOG: SAT solveNonLinear - Elapsed time: 0.040215s Cost: 1; Total time: 0.036708 Quasi-ranking function: 50000 - __disjvr_0^0 + b_7^0 - y_6^0 New Graphs: Transitions: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Variables: __disjvr_0^0, b_7^0, x_5^0, y_6^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002692s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.083228s Trying to remove transition: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.019551s Time used: 0.018647 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.832588s Time used: 0.831735 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.998551s Time used: 0.996889 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.998283s Time used: 0.996298 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.026186s Time used: 0.021794 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.015038s Time used: 0.015037 LOG: SAT solveNonLinear - Elapsed time: 0.041224s Cost: 1; Total time: 0.036831 Quasi-ranking function: 50000 - __disjvr_0^0 - b_7^0 - y_6^0 New Graphs: Transitions: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Variables: __disjvr_0^0, b_7^0, x_5^0, y_6^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002761s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.058000s Trying to remove transition: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.020824s Time used: 0.019911 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.857467s Time used: 0.856602 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.998549s Time used: 0.996888 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.997016s Time used: 0.995055 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.027025s Time used: 0.022585 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.017239s Time used: 0.017237 LOG: SAT solveNonLinear - Elapsed time: 0.044264s Cost: 1; Total time: 0.039822 Termination implied by a set of invariant(s): Invariant at l4: 1 + x_5^0 <= b_7^0 + y_6^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^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): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Quasi-ranking function: 50000 + __disjvr_0^0 + b_7^0 - y_6^0 New Graphs: Transitions: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Variables: __disjvr_0^0, b_7^0, x_5^0, y_6^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002839s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.012171s Trying to remove transition: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.020304s Time used: 0.019379 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.933684s Time used: 0.932834 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.963993s Time used: 0.96252 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.997338s Time used: 0.995265 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.025497s Time used: 0.021005 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.014935s Time used: 0.014933 LOG: SAT solveNonLinear - Elapsed time: 0.040433s Cost: 1; Total time: 0.035938 Termination implied by a set of invariant(s): Invariant at l4: 0 <= 1 + b_7^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^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): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Quasi-ranking function: 50000 + __disjvr_0^0 - b_7^0 - y_6^0 New Graphs: Transitions: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Variables: __disjvr_0^0, b_7^0, x_5^0, y_6^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.012439s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.092192s Trying to remove transition: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.021008s Time used: 0.02004 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.811780s Time used: 0.810909 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.999278s Time used: 0.997479 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.996419s Time used: 0.994274 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.025474s Time used: 0.021203 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.016134s Time used: 0.016132 LOG: SAT solveNonLinear - Elapsed time: 0.041608s Cost: 1; Total time: 0.037335 Termination implied by a set of invariant(s): Invariant at l4: 1 + b_7^0 + x_5^0 <= y_6^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^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): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Quasi-ranking function: 50000 - __disjvr_0^0 - y_6^0 New Graphs: Transitions: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Variables: __disjvr_0^0, b_7^0, x_5^0, y_6^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002935s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.073260s Trying to remove transition: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.020717s Time used: 0.020021 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.841568s Time used: 0.840713 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.997587s Time used: 0.995878 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.996799s Time used: 0.994889 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.026533s Time used: 0.022346 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.018270s Time used: 0.018268 LOG: SAT solveNonLinear - Elapsed time: 0.044802s Cost: 1; Total time: 0.040614 Termination implied by a set of invariant(s): Invariant at l4: 0 <= b_7^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^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): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Quasi-ranking function: 50000 + __disjvr_0^0 - y_6^0 New Graphs: Transitions: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Variables: __disjvr_0^0, b_7^0, x_5^0, y_6^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002987s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.072016s Trying to remove transition: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.022678s Time used: 0.021748 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.835912s Time used: 0.835289 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.998980s Time used: 0.997216 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.996592s Time used: 0.99467 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.024902s Time used: 0.020948 Proving non-termination of subgraph 1 Transitions: undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Variables: __disjvr_0^0, b_7^0, x_5^0, y_6^0 Checking that every undef value has an assignment... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002017s Checking conditional non-termination of SCC {l4}... EXIT TRANSITIONS: Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.040700s Time used: 0.040413 Improving Solution with cost 5 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.064522s Time used: 0.06452 LOG: SAT solveNonLinear - Elapsed time: 0.105222s Cost: 5; Total time: 0.104933 Failed at location 4: 1 + x_5^0 <= b_7^0 + y_6^0 Before Improving: Quasi-invariant at l4: 1 + x_5^0 <= b_7^0 + y_6^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.010328s Remaining time after improvement: 0.997977 Minimizing number of undef constraints... LOG: CALL solveNonLinear LOG: RETURN solveNonLinear - Elapsed time: 0.005978s Number of undef constraints reduced! Non-termination implied by a set of quasi-invariant(s): Quasi-invariant at l4: 1 + x_5^0 <= b_7^0 + y_6^0 Strengthening and disabling EXIT transitions... Closed exits from l4: 4 Strengthening exit transition (result): Strengthening exit transition (result): Strengthening exit transition (result): Strengthening exit transition (result): Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Checking conditional non-termination of SCC {l4}... EXIT TRANSITIONS: Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.024196s Time used: 0.023972 Improving Solution with cost 2 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.027768s Time used: 0.027759 LOG: SAT solveNonLinear - Elapsed time: 0.051964s Cost: 2; Total time: 0.051731 Minimizing number of undef constraints... LOG: CALL solveNonLinear LOG: RETURN solveNonLinear - Elapsed time: 0.011656s Number of undef constraints reduced! Non-termination implied by a set of quasi-invariant(s): Quasi-invariant at l4: b_7^0 <= 0 Strengthening and disabling EXIT transitions... Closed exits from l4: 2 Strengthening exit transition (result): Strengthening exit transition (result): Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Checking conditional non-termination of SCC {l4}... EXIT TRANSITIONS: Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.021785s Time used: 0.02159 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.018531s Time used: 0.018529 LOG: SAT solveNonLinear - Elapsed time: 0.040316s Cost: 1; Total time: 0.040119 Minimizing number of undef constraints... LOG: CALL solveNonLinear LOG: RETURN solveNonLinear - Elapsed time: 0.010332s Number of undef constraints reduced! Non-termination implied by a set of quasi-invariant(s): Quasi-invariant at l4: 0 <= b_7^0 Strengthening and disabling EXIT transitions... Closed exits from l4: 1 Strengthening exit transition (result): Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Checking conditional non-termination of SCC {l4}... EXIT TRANSITIONS: Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.032556s Time used: 0.032348 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.017852s Time used: 0.01785 LOG: SAT solveNonLinear - Elapsed time: 0.050408s Cost: 1; Total time: 0.050198 Failed at location 4: 2 + x_5^0 <= b_7^0 + y_6^0 Before Improving: Quasi-invariant at l4: 2 + x_5^0 <= b_7^0 + y_6^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.006413s Remaining time after improvement: 0.998634 Minimizing number of undef constraints... LOG: CALL solveNonLinear LOG: RETURN solveNonLinear - Elapsed time: 0.004586s Number of undef constraints reduced! Non-termination implied by a set of quasi-invariant(s): Quasi-invariant at l4: 2 + x_5^0 <= b_7^0 + y_6^0 Strengthening and disabling EXIT transitions... Closed exits from l4: 1 Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef7, b_7^0 -> 0, x_5^0 -> 1 + x_5^0, y_6^0 -> 1 + y_6^0, rest remain the same}> Calling reachability with... Transition: Conditions: 1 + x_5^0 <= b_7^0 + y_6^0, b_7^0 <= 0, 0 <= b_7^0, 2 + x_5^0 <= b_7^0 + y_6^0, OPEN EXITS: --- Reachability graph --- > Graph without transitions. Calling reachability with... Transition: Conditions: 2 + x_5^0 <= b_7^0 + y_6^0, b_7^0 = 0, OPEN EXITS: > Conditions are reachable! Program does NOT terminate