NO Solver Timeout: 4 Global Timeout: 300 No parsing errors! Init Location: 0 Transitions: 0) /\ (arg2 > ~(1)), par{arg1 -> arg2, arg2 -> undef2}> 10), par{arg1 -> (arg1 - 1), arg2 -> undef4}> 20), par{arg1 -> (arg1 + 1), arg2 -> undef6}> undef8}> 30), par{arg2 -> undef10}> undef11, arg2 -> undef12}> Fresh variables: undef2, undef4, undef6, undef8, undef10, undef11, undef12, Undef variables: undef2, undef4, undef6, undef8, undef10, undef11, undef12, Abstraction variables: Exit nodes: Accepting locations: Asserts: Preprocessed LLVMGraph Init Location: 0 Transitions: 0) /\ (undef12 > ~(1))> 10) /\ ((arg1 - 1) < 30), par{arg1 -> (arg1 - 1)}> 20) /\ ((arg1 + 1) < 30), par{arg1 -> (arg1 + 1)}> 20) /\ ((arg1 + 1) > 30), par{arg1 -> (arg1 + 1)}> Fresh variables: undef2, undef4, undef6, undef8, undef10, undef11, undef12, Undef variables: undef2, undef4, undef6, undef8, undef10, undef11, undef12, Abstraction variables: Exit nodes: Accepting locations: Asserts: ************************************************************* ******************************************************************************************* *********************** WORKING TRANSITION SYSTEM (DAG) *********************** ******************************************************************************************* Init Location: 0 Graph 0: Transitions: Variables: Graph 1: Transitions: -1 + arg1, rest remain the same}> 1 + arg1, rest remain the same}> 1 + arg1, rest remain the same}> Variables: arg1 Precedence: Graph 0 Graph 1 Map Locations to Subgraph: ( 0 , 0 ) ( 2 , 1 ) ******************************************************************************************* ******************************** CHECKING ASSERTIONS ******************************** ******************************************************************************************* Proving termination of subgraph 0 Proving termination of subgraph 1 Checking unfeasibility... Time used: 0.003608 Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001015s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.006052s Piecewise ranking function: min(900 - 30*arg1,270) New Graphs: Transitions: -1 + arg1, rest remain the same}> 1 + arg1, rest remain the same}> Variables: arg1 Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000452s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001728s Piecewise ranking function: min(-341 + 31*arg1,989 - 34*arg1) New Graphs: Transitions: 1 + arg1, rest remain the same}> Variables: arg1 Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000194s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000566s Trying to remove transition: 1 + arg1, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.001615s Time used: 0.001549 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.003982s Time used: 0.00384 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.009855s Time used: 0.009854 LOG: SAT solveNonLinear - Elapsed time: 0.013837s Cost: 1; Total time: 0.013694 Failed at location 2: arg1 <= 1 Before Improving: Quasi-invariant at l2: arg1 <= 1 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001650s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000597s Remaining time after improvement: 0.99874 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l2: arg1 <= 2 [ 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: -1 + arg1, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1 + arg1, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1 + arg1, 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: 1 + arg1, rest remain the same}> New Graphs: Calling Safety with literal arg1 <= 2 and entry LOG: CALL check - Post:arg1 <= 2 - Process 1 * Exit transition: * Postcondition : arg1 <= 2 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000251s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000288s INVARIANTS: 2: Quasi-INVARIANTS to narrow Graph: 2: arg1 <= 2 , Narrowing transition: -1 + arg1, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1 + arg1, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1 + arg1, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: -1 + arg1, rest remain the same}> 1 + arg1, rest remain the same}> 1 + arg1, rest remain the same}> Variables: arg1 Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000477s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004534s Piecewise ranking function: min(900 - 30*arg1,270) New Graphs: Transitions: -1 + arg1, rest remain the same}> 1 + arg1, rest remain the same}> Variables: arg1 Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000357s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001582s Piecewise ranking function: min(-341 + 31*arg1,989 - 34*arg1) New Graphs: Transitions: 1 + arg1, rest remain the same}> Variables: arg1 Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000197s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000576s Trying to remove transition: 1 + arg1, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.001617s Time used: 0.001553 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.013609s Time used: 0.013471 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.016706s Time used: 0.016704 LOG: SAT solveNonLinear - Elapsed time: 0.030316s Cost: 1; Total time: 0.030175 Failed at location 2: arg1 <= 3 Before Improving: Quasi-invariant at l2: arg1 <= 3 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002702s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000879s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000801s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000585s Remaining time after improvement: 0.997128 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l2: arg1 <= 6 [ 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: -1 + arg1, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1 + arg1, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1 + arg1, 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: 1 + arg1, rest remain the same}> New Graphs: Calling Safety with literal arg1 <= 6 and entry LOG: CALL check - Post:arg1 <= 6 - Process 2 * Exit transition: * Postcondition : arg1 <= 6 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000265s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000305s INVARIANTS: 2: Quasi-INVARIANTS to narrow Graph: 2: arg1 <= 6 , Narrowing transition: -1 + arg1, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1 + arg1, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1 + arg1, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: -1 + arg1, rest remain the same}> 1 + arg1, rest remain the same}> 1 + arg1, rest remain the same}> Variables: arg1 Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000495s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004564s Piecewise ranking function: min(900 - 30*arg1,270) New Graphs: Transitions: -1 + arg1, rest remain the same}> 1 + arg1, rest remain the same}> Variables: arg1 Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000375s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001595s Piecewise ranking function: min(-341 + 31*arg1,989 - 34*arg1) New Graphs: Transitions: 1 + arg1, rest remain the same}> Variables: arg1 Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000202s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000579s Trying to remove transition: 1 + arg1, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.001645s Time used: 0.001578 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.014078s Time used: 0.013939 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.016632s Time used: 0.01663 LOG: SAT solveNonLinear - Elapsed time: 0.030710s Cost: 1; Total time: 0.030569 Failed at location 2: arg1 <= 7 Before Improving: Quasi-invariant at l2: arg1 <= 7 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002708s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000704s Remaining time after improvement: 0.998499 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l2: arg1 <= 8 [ 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: -1 + arg1, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1 + arg1, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1 + arg1, 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: 1 + arg1, rest remain the same}> New Graphs: Calling Safety with literal arg1 <= 8 and entry LOG: CALL check - Post:arg1 <= 8 - Process 3 * Exit transition: * Postcondition : arg1 <= 8 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000273s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000314s INVARIANTS: 2: Quasi-INVARIANTS to narrow Graph: 2: arg1 <= 8 , Narrowing transition: -1 + arg1, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1 + arg1, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1 + arg1, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: -1 + arg1, rest remain the same}> 1 + arg1, rest remain the same}> 1 + arg1, rest remain the same}> Variables: arg1 Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000505s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004548s Piecewise ranking function: min(900 - 30*arg1,270) New Graphs: Transitions: -1 + arg1, rest remain the same}> 1 + arg1, rest remain the same}> Variables: arg1 Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000375s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001582s Piecewise ranking function: min(-341 + 31*arg1,989 - 34*arg1) New Graphs: Transitions: 1 + arg1, rest remain the same}> Variables: arg1 Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000199s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000578s Trying to remove transition: 1 + arg1, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.001627s Time used: 0.001561 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.013943s Time used: 0.013798 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.018081s Time used: 0.018079 LOG: SAT solveNonLinear - Elapsed time: 0.032024s Cost: 1; Total time: 0.031877 Failed at location 2: arg1 <= 9 Before Improving: Quasi-invariant at l2: arg1 <= 9 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002464s Remaining time after improvement: 0.999369 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l2: arg1 <= 9 [ 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: -1 + arg1, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1 + arg1, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1 + arg1, 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: 1 + arg1, rest remain the same}> New Graphs: Calling Safety with literal arg1 <= 9 and entry LOG: CALL check - Post:arg1 <= 9 - Process 4 * Exit transition: * Postcondition : arg1 <= 9 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000342s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000384s INVARIANTS: 2: Quasi-INVARIANTS to narrow Graph: 2: arg1 <= 9 , Narrowing transition: -1 + arg1, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1 + arg1, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1 + arg1, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: -1 + arg1, rest remain the same}> 1 + arg1, rest remain the same}> 1 + arg1, rest remain the same}> Variables: arg1 Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000513s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004560s Piecewise ranking function: min(900 - 30*arg1,270) New Graphs: Transitions: -1 + arg1, rest remain the same}> 1 + arg1, rest remain the same}> Variables: arg1 Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000377s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001590s Piecewise ranking function: min(-341 + 31*arg1,989 - 34*arg1) New Graphs: Transitions: 1 + arg1, rest remain the same}> Variables: arg1 Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000208s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000577s Trying to remove transition: 1 + arg1, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.001631s Time used: 0.001567 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.013951s Time used: 0.013813 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.013858s Time used: 0.013856 LOG: SAT solveNonLinear - Elapsed time: 0.027810s Cost: 1; Total time: 0.027669 Failed at location 2: arg1 <= 10 Before Improving: Quasi-invariant at l2: arg1 <= 10 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002482s Remaining time after improvement: 0.999347 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l2: arg1 <= 10 [ 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: -1 + arg1, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1 + arg1, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1 + arg1, 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: 1 + arg1, rest remain the same}> New Graphs: Calling Safety with literal arg1 <= 10 and entry LOG: CALL check - Post:arg1 <= 10 - Process 5 * Exit transition: * Postcondition : arg1 <= 10 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000345s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000385s INVARIANTS: 2: Quasi-INVARIANTS to narrow Graph: 2: arg1 <= 10 , Narrowing transition: -1 + arg1, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1 + arg1, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1 + arg1, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: -1 + arg1, rest remain the same}> 1 + arg1, rest remain the same}> 1 + arg1, rest remain the same}> Variables: arg1 Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000513s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004578s Piecewise ranking function: min(900 - 30*arg1,270) New Graphs: Transitions: -1 + arg1, rest remain the same}> 1 + arg1, rest remain the same}> Variables: arg1 Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000383s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001598s Piecewise ranking function: min(-341 + 31*arg1,989 - 34*arg1) New Graphs: Transitions: 1 + arg1, rest remain the same}> Variables: arg1 Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000198s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000585s Trying to remove transition: 1 + arg1, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.001643s Time used: 0.001579 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.014135s Time used: 0.01399 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.014205s Time used: 0.014203 LOG: SAT solveNonLinear - Elapsed time: 0.028340s Cost: 1; Total time: 0.028193 Failed at location 2: arg1 <= 11 Before Improving: Quasi-invariant at l2: arg1 <= 11 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002778s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000930s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000811s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000785s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000772s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000784s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000763s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000763s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000754s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000581s Remaining time after improvement: 0.992838 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l2: arg1 <= 20 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): -1 + arg1, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1 + arg1, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1 + arg1, 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: 1 + arg1, rest remain the same}> New Graphs: Calling Safety with literal arg1 <= 20 and entry LOG: CALL check - Post:arg1 <= 20 - Process 6 * Exit transition: * Postcondition : arg1 <= 20 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000278s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000319s INVARIANTS: 2: Quasi-INVARIANTS to narrow Graph: 2: arg1 <= 20 , It's unfeasible. Removing transition: -1 + arg1, rest remain the same}> Narrowing transition: 1 + arg1, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1 + arg1, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: 1 + arg1, rest remain the same}> 1 + arg1, rest remain the same}> Variables: arg1 Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000522s Ranking function: 434 + (~(31) / 2)*arg1 New Graphs: Transitions: 1 + arg1, rest remain the same}> Variables: arg1 Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000193s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000584s Trying to remove transition: 1 + arg1, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.001654s Time used: 0.00159 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.019488s Time used: 0.019352 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.013422s Time used: 0.01342 LOG: SAT solveNonLinear - Elapsed time: 0.032910s Cost: 1; Total time: 0.032772 Failed at location 2: arg1 <= 29 Before Improving: Quasi-invariant at l2: arg1 <= 29 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002372s Remaining time after improvement: 0.999413 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l2: arg1 <= 29 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + arg1, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: 1 + arg1, rest remain the same}> [ Termination Graph ] Strengthening and disabling transitions... > It's unfeasible. Removing transition: 1 + arg1, rest remain the same}> New Graphs: Calling Safety with literal arg1 <= 29 and entry LOG: CALL check - Post:arg1 <= 29 - Process 7 * Exit transition: * Postcondition : arg1 <= 29 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000297s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000338s INVARIANTS: 2: Quasi-INVARIANTS to narrow Graph: 2: arg1 <= 29 , It's unfeasible. Removing transition: 1 + arg1, rest remain the same}> Narrowing transition: 1 + arg1, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: 1 + arg1, rest remain the same}> Variables: arg1 Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000200s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000616s Trying to remove transition: 1 + arg1, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.001708s Time used: 0.001643 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.006914s Time used: 4.00678 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.005928s Time used: 4.00129 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.013936s Time used: 1.00693 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.009289s Time used: 0.003036 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.006676s Time used: 0.006674 LOG: SAT solveNonLinear - Elapsed time: 0.015965s Cost: 1; Total time: 0.00971 Quasi-ranking function: 50000 - arg1 New Graphs: Transitions: 1 + arg1, rest remain the same}> Variables: arg1 Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000217s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000678s Trying to remove transition: 1 + arg1, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.001861s Time used: 0.001795 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.003538s Time used: 4.0034 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.005859s Time used: 4.00123 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.008258s Time used: 1.00097 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.009430s Time used: 0.002846 Proving non-termination of subgraph 1 Transitions: 1 + arg1, rest remain the same}> Variables: arg1 Checking conditional non-termination of SCC {l2}... EXIT TRANSITIONS: Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.040685s Time used: 0.040586 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.003156s Time used: 0.003153 LOG: SAT solveNonLinear - Elapsed time: 0.043841s Cost: 1; Total time: 0.043739 Failed at location 2: 30 <= arg1 Before Improving: Quasi-invariant at l2: 30 <= arg1 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000980s Remaining time after improvement: 0.999545 Non-termination implied by a set of quasi-invariant(s): Quasi-invariant at l2: 30 <= arg1 Strengthening and disabling EXIT transitions... Closed exits from l2: 1 Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + arg1, rest remain the same}> Calling reachability with... Transition: Conditions: 30 <= arg1, OPEN EXITS: --- Reachability graph --- > Graph without transitions. Calling reachability with... Transition: Conditions: 30 <= arg1, OPEN EXITS: > Conditions are reachable! Program does NOT terminate