YES Solver Timeout: 4 Global Timeout: 300 No parsing errors! Init Location: 0 Transitions: ((0 + x^0) + z^0), z^0 -> (~(1) + z^0)}> ((0 + x^0) + y^0), y^0 -> (~(1) + y^0)}> Fresh variables: Undef variables: Abstraction variables: Exit nodes: Accepting locations: Asserts: Preprocessed LLVMGraph Init Location: 0 Transitions: ((0 + x^0) + z^0), z^0 -> (~(1) + z^0)}> ((0 + x^0) + y^0), y^0 -> (~(1) + y^0)}> Fresh variables: Undef variables: Abstraction variables: Exit nodes: Accepting locations: Asserts: ************************************************************* ******************************************************************************************* *********************** WORKING TRANSITION SYSTEM (DAG) *********************** ******************************************************************************************* Init Location: 0 Graph 0: Transitions: Variables: Graph 1: Transitions: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> Variables: x^0, z^0, y^0 Precedence: Graph 0 Graph 1 Map Locations to Subgraph: ( 0 , 0 ) ( 1 , 1 ) ******************************************************************************************* ******************************** CHECKING ASSERTIONS ******************************** ******************************************************************************************* Proving termination of subgraph 0 Proving termination of subgraph 1 Checking unfeasibility... Time used: 0.003572 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000607s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001887s Trying to remove transition: x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.005450s Time used: 0.005308 Trying to remove transition: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.004214s Time used: 0.003864 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.010007s Time used: 0.009705 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.017455s Time used: 0.017453 LOG: SAT solveNonLinear - Elapsed time: 0.027462s Cost: 1; Total time: 0.027158 Failed at location 1: x^0 <= 0 Before Improving: Quasi-invariant at l1: x^0 <= 0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002406s Remaining time after improvement: 0.99941 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l1: x^0 <= 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: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: x^0 + y^0, y^0 -> -1 + y^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: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> New Graphs: Calling Safety with literal x^0 <= 0 and entry LOG: CALL check - Post:x^0 <= 0 - Process 1 * Exit transition: * Postcondition : x^0 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000196s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000220s INVARIANTS: 1: Quasi-INVARIANTS to narrow Graph: 1: x^0 <= 0 , Narrowing transition: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> Variables: x^0, z^0, y^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000368s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001311s Trying to remove transition: x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.003435s Time used: 0.003355 Trying to remove transition: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.004052s Time used: 0.003767 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.001793s Time used: 4.00147 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.063486s Time used: 0.0585 Improving Solution with cost 2 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.010553s Time used: 1.01054 LOG: SAT solveNonLinear - Elapsed time: 1.074039s Cost: 2; Total time: 1.06904 Failed at location 1: 1 + x^0 + y^0 <= z^0 Failed at location 1: x^0 + z^0 <= 0 Before Improving: Quasi-invariant at l1: 1 + x^0 + y^0 <= z^0 Quasi-invariant at l1: x^0 + z^0 <= 0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.010595s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001320s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000849s Remaining time after improvement: 0.996327 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l1: x^0 + y^0 <= 1 + z^0 Quasi-invariant at l1: x^0 + z^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): x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): x^0 + y^0, y^0 -> -1 + y^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): x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> Ranking function: x^0 New Graphs: Calling Safety with literal x^0 + y^0 <= 1 + z^0 and entry LOG: CALL check - Post:x^0 + y^0 <= 1 + z^0 - Process 2 * Exit transition: * Postcondition : x^0 + y^0 <= 1 + z^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000210s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000244s Calling Safety with literal x^0 + z^0 <= 0 and entry LOG: CALL check - Post:x^0 + z^0 <= 0 - Process 3 * Exit transition: * Postcondition : x^0 + z^0 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000200s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000229s INVARIANTS: 1: Quasi-INVARIANTS to narrow Graph: 1: x^0 + z^0 <= 0 , x^0 + y^0 <= 1 + z^0 , Narrowing transition: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> LOG: Narrow transition size 2 invGraph after Narrowing: Transitions: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> Variables: x^0, z^0, y^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000954s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.006653s Piecewise ranking function: min(0,-3 + 3*x^0) New Graphs: Transitions: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> Variables: x^0, y^0, z^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000728s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.005754s Trying to remove transition: x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.007124s Time used: 0.006764 Trying to remove transition: x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.010864s Time used: 0.010252 Trying to remove transition: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.005375s Time used: 0.004698 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.002018s Time used: 4.00153 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.146031s Time used: 0.140378 Improving Solution with cost 3 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.000452s Time used: 1.00044 LOG: SAT solveNonLinear - Elapsed time: 1.146483s Cost: 3; Total time: 1.14082 Failed at location 1: x^0 + z^0 <= 0 Failed at location 1: x^0 + y^0 <= 1 Failed at location 1: x^0 + y^0 <= 1 Before Improving: Quasi-invariant at l1: x^0 + z^0 <= 0 Quasi-invariant at l1: x^0 + y^0 <= 1 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.024178s Remaining time after improvement: 0.997539 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l1: x^0 + z^0 <= 0 Quasi-invariant at l1: x^0 + y^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): x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> [ Termination Graph ] Strengthening and disabling transitions... > It's unfeasible. Removing transition: x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> New Graphs: Transitions: x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> Variables: x^0, y^0, z^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000676s Ranking function: -2 + y^0 - 2*z^0 New Graphs: Calling Safety with literal x^0 + y^0 <= 1 and entry LOG: CALL check - Post:x^0 + y^0 <= 1 - Process 4 * Exit transition: * Postcondition : x^0 + y^0 <= 1 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000352s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000393s Calling Safety with literal x^0 + z^0 <= 0 and entry LOG: CALL check - Post:x^0 + z^0 <= 0 - Process 5 * Exit transition: * Postcondition : x^0 + z^0 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000322s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000356s Calling Safety with literal x^0 + y^0 <= 1 and entry LOG: CALL check - Post:x^0 + y^0 <= 1 - Process 6 * Exit transition: * Postcondition : x^0 + y^0 <= 1 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000335s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000377s INVARIANTS: 1: Quasi-INVARIANTS to narrow Graph: 1: x^0 + z^0 <= 0 , x^0 + y^0 <= 1 , Narrowing transition: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> LOG: Narrow transition size 2 invGraph after Narrowing: Transitions: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> Variables: x^0, z^0, y^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001144s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.008963s Piecewise ranking function: min(0,-3 + 3*x^0) New Graphs: Transitions: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> Variables: x^0, y^0, z^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000842s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.006970s Trying to remove transition: x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.006544s Time used: 0.006114 Trying to remove transition: x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.012361s Time used: 0.011587 Trying to remove transition: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.005883s Time used: 0.005107 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.002739s Time used: 4.00209 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.185262s Time used: 0.179748 Improving Solution with cost 3 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.000723s Time used: 1.0007 LOG: SAT solveNonLinear - Elapsed time: 1.185985s Cost: 3; Total time: 1.18045 Failed at location 1: z^0 <= 0 Failed at location 1: 1 + x^0 + y^0 <= 0 Failed at location 1: 1 + x^0 + y^0 <= 0 Before Improving: Quasi-invariant at l1: z^0 <= 0 Quasi-invariant at l1: 1 + x^0 + y^0 <= 0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.025199s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003575s Remaining time after improvement: 0.992323 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l1: z^0 <= 0 Quasi-invariant at l1: x^0 + y^0 <= 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: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): x^0 + y^0, y^0 -> -1 + y^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): x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> New Graphs: Transitions: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> Variables: x^0, y^0, z^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001198s Ranking function: -1 + x^0 New Graphs: Transitions: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> Variables: x^0, y^0, z^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000698s Ranking function: -1 - y^0 + z^0 New Graphs: Calling Safety with literal x^0 + y^0 <= 0 and entry LOG: CALL check - Post:x^0 + y^0 <= 0 - Process 7 * Exit transition: * Postcondition : x^0 + y^0 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000430s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000475s Calling Safety with literal z^0 <= 0 and entry LOG: CALL check - Post:z^0 <= 0 - Process 8 * Exit transition: * Postcondition : z^0 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000408s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000439s INVARIANTS: 1: Quasi-INVARIANTS to narrow Graph: 1: x^0 + y^0 <= 0 , z^0 <= 0 , Narrowing transition: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> LOG: Narrow transition size 2 invGraph after Narrowing: Transitions: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> Variables: x^0, z^0, y^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002370s Ranking function: -2 + 2*z^0 New Graphs: Transitions: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> Variables: x^0, y^0, z^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001587s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.024792s Piecewise ranking function: min(1,-2 + 3*x^0) New Graphs: Transitions: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> Variables: x^0, y^0, z^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001024s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.018685s Trying to remove transition: x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.008279s Time used: 0.007841 Trying to remove transition: x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.014480s Time used: 0.013841 Trying to remove transition: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.009288s Time used: 0.008679 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.001896s Time used: 4.00107 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.218180s Time used: 0.20356 Improving Solution with cost 4 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.001244s Time used: 1.00124 LOG: SAT solveNonLinear - Elapsed time: 1.219424s Cost: 4; Total time: 1.2048 Failed at location 1: z^0 <= 1 Failed at location 1: z^0 <= 1 Failed at location 1: 1 + y^0 <= 0 Failed at location 1: 1 + y^0 <= 0 Before Improving: Quasi-invariant at l1: z^0 <= 1 Quasi-invariant at l1: 1 + y^0 <= 0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.009074s Remaining time after improvement: 0.994483 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l1: z^0 <= 1 Quasi-invariant at l1: 1 + y^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): x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): x^0 + y^0, y^0 -> -1 + y^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): x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> Ranking function: 2 + x^0 + z^0 New Graphs: Transitions: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> Variables: x^0, y^0, z^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001030s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.021082s Trying to remove transition: x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.009925s Time used: 0.009605 LOG: SAT solveNonLinear - Elapsed time: 0.009925s Cost: 0; Total time: 0.009605 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l1: x^0 + z^0 <= 0 Ranking function: y^0 - z^0 Ranking function and negation of Quasi-Invariant applied New Graphs: Transitions: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> Variables: x^0, y^0, z^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000479s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002185s Trying to remove transition: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.006376s Time used: 0.006272 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.015946s Time used: 0.015422 Improving Solution with cost 2 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.028275s Time used: 0.028273 LOG: SAT solveNonLinear - Elapsed time: 0.044221s Cost: 2; Total time: 0.043695 Failed at location 1: x^0 + z^0 <= 0 Failed at location 1: x^0 + z^0 <= 0 Before Improving: Quasi-invariant at l1: x^0 + z^0 <= 0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.006433s Remaining time after improvement: 0.997675 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l1: x^0 + z^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): x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> [ Termination Graph ] Strengthening and disabling transitions... > It's unfeasible. Removing transition: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> New Graphs: Calling Safety with literal 1 + y^0 <= 0 and entry LOG: CALL check - Post:1 + y^0 <= 0 - Process 9 * Exit transition: * Postcondition : 1 + y^0 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000640s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000683s Calling Safety with literal z^0 <= 1 and entry LOG: CALL check - Post:z^0 <= 1 - Process 10 * Exit transition: * Postcondition : z^0 <= 1 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000640s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000682s Calling Safety with literal z^0 <= 1 and entry LOG: CALL check - Post:z^0 <= 1 - Process 11 * Exit transition: * Postcondition : z^0 <= 1 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000597s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000634s Calling Safety with literal 1 + y^0 <= 0 and entry LOG: CALL check - Post:1 + y^0 <= 0 - Process 12 * Exit transition: * Postcondition : 1 + y^0 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000626s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000664s INVARIANTS: 1: Quasi-INVARIANTS to narrow Graph: 1: 1 + y^0 <= 0 , z^0 <= 1 , Calling Safety with literal x^0 + z^0 <= 0 and entry LOG: CALL check - Post:x^0 + z^0 <= 0 - Process 13 * Exit transition: * Postcondition : x^0 + z^0 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000606s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000649s Calling Safety with literal x^0 + z^0 <= 0 and entry LOG: CALL check - Post:x^0 + z^0 <= 0 - Process 14 * Exit transition: * Postcondition : x^0 + z^0 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000615s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000654s INVARIANTS: 1: Quasi-INVARIANTS to narrow Graph: 1: x^0 + z^0 <= 0 , Narrowing transition: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: Narrow transition size 3 Narrowing transition: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: Narrow transition size 3 Narrowing transition: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: Narrow transition size 3 Narrowing transition: x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> LOG: Narrow transition size 3 Narrowing transition: x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> LOG: Narrow transition size 3 Narrowing transition: x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> LOG: Narrow transition size 3 invGraph after Narrowing: Transitions: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> Variables: x^0, z^0, y^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004381s Ranking function: -2 + 2*z^0 New Graphs: Transitions: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> Variables: x^0, y^0, z^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003502s Ranking function: 1 + y^0 New Graphs: Transitions: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> Variables: x^0, y^0, z^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001848s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.032740s Piecewise ranking function: min(0,-4 + 4*x^0) New Graphs: Transitions: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> Variables: x^0, y^0, z^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001207s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.022149s Trying to remove transition: x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.011350s Time used: 0.010859 Trying to remove transition: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.009312s Time used: 0.008511 Trying to remove transition: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.010633s Time used: 0.009851 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.029670s Time used: 0.028678 Improving Solution with cost 2 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.047662s Time used: 0.047661 LOG: SAT solveNonLinear - Elapsed time: 0.077332s Cost: 2; Total time: 0.076339 Failed at location 1: 1 + y^0 <= 0 Failed at location 1: 1 + y^0 <= 0 Before Improving: Quasi-invariant at l1: 1 + y^0 <= 0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.012992s Remaining time after improvement: 0.996367 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l1: 1 + y^0 <= 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: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> [ Termination Graph ] Strengthening and disabling transitions... > It's unfeasible. Removing transition: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> New Graphs: Transitions: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> Variables: x^0, y^0, z^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000965s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.009965s Trying to remove transition: x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.009336s Time used: 0.008979 Trying to remove transition: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.009081s Time used: 0.008503 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.025310s Time used: 0.024566 Improving Solution with cost 3 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.000949s Time used: 1.00093 LOG: SAT solveNonLinear - Elapsed time: 1.026259s Cost: 3; Total time: 1.0255 Failed at location 1: x^0 + z^0 <= 1 Failed at location 1: x^0 + z^0 <= 1 Failed at location 1: x^0 + z^0 <= 1 Before Improving: Quasi-invariant at l1: x^0 + z^0 <= 1 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.011706s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002248s Remaining time after improvement: 0.994027 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l1: x^0 + z^0 <= 2 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): x^0 + y^0, y^0 -> -1 + y^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): x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> Ranking function: x^0 + z^0 New Graphs: Calling Safety with literal 1 + y^0 <= 0 and entry LOG: CALL check - Post:1 + y^0 <= 0 - Process 15 * Exit transition: * Postcondition : 1 + y^0 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000758s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000805s Calling Safety with literal 1 + y^0 <= 0 and entry LOG: CALL check - Post:1 + y^0 <= 0 - Process 16 * Exit transition: * Postcondition : 1 + y^0 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000710s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000750s INVARIANTS: 1: Quasi-INVARIANTS to narrow Graph: 1: 1 + y^0 <= 0 , Calling Safety with literal x^0 + z^0 <= 2 and entry LOG: CALL check - Post:x^0 + z^0 <= 2 - Process 17 * Exit transition: * Postcondition : x^0 + z^0 <= 2 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000745s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000788s Calling Safety with literal x^0 + z^0 <= 2 and entry LOG: CALL check - Post:x^0 + z^0 <= 2 - Process 18 * Exit transition: * Postcondition : x^0 + z^0 <= 2 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000730s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000774s Calling Safety with literal x^0 + z^0 <= 2 and entry LOG: CALL check - Post:x^0 + z^0 <= 2 - Process 19 * Exit transition: * Postcondition : x^0 + z^0 <= 2 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000799s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000843s INVARIANTS: 1: Quasi-INVARIANTS to narrow Graph: 1: x^0 + z^0 <= 2 , Narrowing transition: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> LOG: Narrow transition size 2 invGraph after Narrowing: Transitions: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> Variables: x^0, z^0, y^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004484s Ranking function: -2 + 2*z^0 New Graphs: Transitions: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> Variables: x^0, y^0, z^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003769s Ranking function: 1 + y^0 New Graphs: Transitions: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> Variables: x^0, y^0, z^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001832s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.025267s Piecewise ranking function: min(2,-2 + 4*x^0) New Graphs: Transitions: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> Variables: x^0, y^0, z^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001225s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.026637s Trying to remove transition: x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.012590s Time used: 0.011986 Trying to remove transition: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.009774s Time used: 0.008914 Trying to remove transition: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.010913s Time used: 0.010105 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.029819s Time used: 0.028742 Improving Solution with cost 2 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.039766s Time used: 0.039764 LOG: SAT solveNonLinear - Elapsed time: 0.069585s Cost: 2; Total time: 0.068506 Failed at location 1: 1 + y^0 <= 0 Failed at location 1: 1 + y^0 <= 0 Before Improving: Quasi-invariant at l1: 1 + y^0 <= 0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.012920s Remaining time after improvement: 0.996494 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l1: 1 + y^0 <= 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: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: x^0 + y^0, y^0 -> -1 + y^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): x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> New Graphs: Transitions: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> Variables: x^0, y^0, z^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001001s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.009830s Trying to remove transition: x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.008513s Time used: 0.008223 Trying to remove transition: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.009091s Time used: 0.008532 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.023456s Time used: 0.022696 Improving Solution with cost 3 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.000878s Time used: 1.00086 LOG: SAT solveNonLinear - Elapsed time: 1.024334s Cost: 3; Total time: 1.02355 Failed at location 1: z^0 <= 1 Failed at location 1: z^0 <= 1 Failed at location 1: z^0 <= 1 Before Improving: Quasi-invariant at l1: z^0 <= 1 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.010282s Remaining time after improvement: 0.997666 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l1: z^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): x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): x^0 + y^0, y^0 -> -1 + y^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): x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> Ranking function: 2 + x^0 + z^0 New Graphs: Transitions: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> Variables: x^0, y^0, z^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000501s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002079s Trying to remove transition: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.006671s Time used: 0.006568 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.020195s Time used: 0.019727 Improving Solution with cost 3 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.017131s Time used: 0.017129 LOG: SAT solveNonLinear - Elapsed time: 0.037326s Cost: 3; Total time: 0.036856 Failed at location 1: 1 + z^0 <= 0 Failed at location 1: 1 + z^0 <= 0 Failed at location 1: 1 + z^0 <= 0 Before Improving: Quasi-invariant at l1: 1 + z^0 <= 0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.006256s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002088s Remaining time after improvement: 0.994593 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l1: z^0 <= 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: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): x^0 + y^0, y^0 -> -1 + y^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): x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> Ranking function: 2*x^0 + 2*z^0 New Graphs: INVARIANTS: 1: Quasi-INVARIANTS to narrow Graph: 1: 1 + y^0 <= 0 , Calling Safety with literal z^0 <= 1 and entry LOG: CALL check - Post:z^0 <= 1 - Process 20 * Exit transition: * Postcondition : z^0 <= 1 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000887s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000928s Calling Safety with literal z^0 <= 1 and entry LOG: CALL check - Post:z^0 <= 1 - Process 21 * Exit transition: * Postcondition : z^0 <= 1 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000860s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000902s Calling Safety with literal z^0 <= 1 and entry LOG: CALL check - Post:z^0 <= 1 - Process 22 * Exit transition: * Postcondition : z^0 <= 1 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000888s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000929s INVARIANTS: 1: Quasi-INVARIANTS to narrow Graph: 1: z^0 <= 1 , INVARIANTS: 1: Quasi-INVARIANTS to narrow Graph: 1: z^0 <= 0 , Narrowing transition: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: Narrow transition size 3 Narrowing transition: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: Narrow transition size 3 Narrowing transition: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: Narrow transition size 3 Narrowing transition: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: Narrow transition size 3 Narrowing transition: x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> LOG: Narrow transition size 3 Narrowing transition: x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> LOG: Narrow transition size 3 Narrowing transition: x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> LOG: Narrow transition size 3 Narrowing transition: x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> LOG: Narrow transition size 3 invGraph after Narrowing: Transitions: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> Variables: x^0, z^0, y^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004823s Ranking function: -2 + 2*z^0 New Graphs: Transitions: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> Variables: x^0, y^0, z^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003378s Ranking function: 1 + y^0 New Graphs: Transitions: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> Variables: x^0, y^0, z^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001605s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.022592s Piecewise ranking function: min(8 + 8*y^0,4 + 4*x^0 + 8*y^0) New Graphs: Transitions: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> Variables: x^0, y^0, z^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001245s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.010578s Piecewise ranking function: min(-1 + x^0 + z^0,z^0) New Graphs: Transitions: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> Variables: x^0, y^0, z^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000937s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.010296s Trying to remove transition: x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.008341s Time used: 0.008029 LOG: SAT solveNonLinear - Elapsed time: 0.008341s Cost: 0; Total time: 0.008029 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l1: 1 + y^0 <= 0 Ranking function: 2*x^0 - y^0 Ranking function and negation of Quasi-Invariant applied New Graphs: Transitions: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> Variables: x^0, y^0, z^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000446s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001754s Trying to remove transition: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.005403s Time used: 0.005304 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.024257s Time used: 0.02368 Improving Solution with cost 2 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.027469s Time used: 0.027461 LOG: SAT solveNonLinear - Elapsed time: 0.051725s Cost: 2; Total time: 0.051141 Failed at location 1: 1 + y^0 <= 0 Failed at location 1: 1 + y^0 <= 0 Before Improving: Quasi-invariant at l1: 1 + y^0 <= 0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.008195s Remaining time after improvement: 0.997135 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l1: 1 + y^0 <= 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: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: x^0 + y^0, y^0 -> -1 + y^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: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> New Graphs: INVARIANTS: 1: Quasi-INVARIANTS to narrow Graph: 1: 1 + y^0 <= 0 , Narrowing transition: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: Narrow transition size 1 It's unfeasible. Removing transition: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> It's unfeasible. Removing transition: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> Narrowing transition: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> LOG: Narrow transition size 1 It's unfeasible. Removing transition: x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> It's unfeasible. Removing transition: x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> Narrowing transition: x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> Variables: x^0, z^0, y^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002704s Ranking function: y^0 New Graphs: Transitions: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> Variables: x^0, y^0, z^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000963s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.006556s Piecewise ranking function: min(-2 + 2*x^0 + 2*y^0,2*y^0) New Graphs: Transitions: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> Variables: x^0, y^0, z^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000448s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001745s Trying to remove transition: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.005476s Time used: 0.005375 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.012218s Time used: 0.01173 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.013155s Time used: 0.013153 LOG: SAT solveNonLinear - Elapsed time: 0.025372s Cost: 1; Total time: 0.024883 Failed at location 1: z^0 <= 0 Before Improving: Quasi-invariant at l1: z^0 <= 0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004328s Remaining time after improvement: 0.998283 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l1: z^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): x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): x^0 + y^0, y^0 -> -1 + y^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): x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> Ranking function: x^0 + z^0 New Graphs: INVARIANTS: 1: Quasi-INVARIANTS to narrow Graph: 1: z^0 <= 0 , It's unfeasible. Removing transition: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> Narrowing transition: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> LOG: Narrow transition size 1 It's unfeasible. Removing transition: x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> Narrowing transition: x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> x^0 + y^0, y^0 -> -1 + y^0, rest remain the same}> Variables: x^0, z^0, y^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001927s Ranking function: y^0 New Graphs: Transitions: x^0 + z^0, z^0 -> -1 + z^0, rest remain the same}> Variables: x^0, y^0, z^0 Checking conditional termination of SCC {l1}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001285s Ranking function: -1 + z^0 New Graphs: Program Terminates