NO Solver Timeout: 4 Global Timeout: 300 No parsing errors! Init Location: 0 Transitions: undef1}> (0 + deltaext_new^0)}> (0 + deltaext^0)}> (~(1) + deltaext^0)}> (1 + deltaext^0)}> 2}> Fresh variables: undef1, Undef variables: undef1, Abstraction variables: Exit nodes: Accepting locations: Asserts: Preprocessed LLVMGraph Init Location: 0 Transitions: undef1, deltaext^0 -> (0 + (0 + deltaext^0))}> undef1, deltaext^0 -> (0 + (~(1) + deltaext^0))}> undef1, deltaext^0 -> (0 + (1 + deltaext^0))}> Fresh variables: undef1, Undef variables: undef1, Abstraction variables: Exit nodes: Accepting locations: Asserts: ************************************************************* ******************************************************************************************* *********************** WORKING TRANSITION SYSTEM (DAG) *********************** ******************************************************************************************* Init Location: 0 Graph 0: Transitions: Variables: Graph 1: Transitions: undef1, rest remain the same}> undef1, deltaext^0 -> -1 + deltaext^0, rest remain the same}> undef1, deltaext^0 -> 1 + deltaext^0, rest remain the same}> Variables: __disjvr_0^0, deltaext^0, wnt^0 Precedence: Graph 0 Graph 1 Map Locations to Subgraph: ( 0 , 0 ) ( 3 , 1 ) ******************************************************************************************* ******************************** CHECKING ASSERTIONS ******************************** ******************************************************************************************* Proving termination of subgraph 0 Proving termination of subgraph 1 Checking unfeasibility... Time used: 0.004989 Checking conditional termination of SCC {l3}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000835s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.009435s Trying to remove transition: undef1, deltaext^0 -> 1 + deltaext^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.011114s Time used: 0.010834 Trying to remove transition: undef1, deltaext^0 -> -1 + deltaext^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.008209s Time used: 0.00764 Trying to remove transition: undef1, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.005353s Time used: 0.004816 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.022388s Time used: 0.021872 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.001790s Time used: 4.00051 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.300860s Time used: 0.294916 Improving Solution with cost 2 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.705596s Time used: 0.705576 LOG: SAT solveNonLinear - Elapsed time: 1.006457s Cost: 2; Total time: 1.00049 Failed at location 3: wnt^0 <= 0 Failed at location 3: deltaext^0 <= 1 + wnt^0 Before Improving: Quasi-invariant at l3: wnt^0 <= 0 Quasi-invariant at l3: deltaext^0 <= 1 + wnt^0 Quasi-invariant at l3: 0 <= deltaext^0 + wnt^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.006621s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002422s Remaining time after improvement: 0.994871 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l3: wnt^0 <= 1 Quasi-invariant at l3: deltaext^0 <= 1 + wnt^0 Quasi-invariant at l3: 0 <= deltaext^0 + wnt^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef1, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef1, deltaext^0 -> -1 + deltaext^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef1, deltaext^0 -> 1 + deltaext^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): undef1, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef1, deltaext^0 -> -1 + deltaext^0, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef1, deltaext^0 -> 1 + deltaext^0, rest remain the same}> New Graphs: Transitions: undef1, rest remain the same}> undef1, deltaext^0 -> 1 + deltaext^0, rest remain the same}> Variables: __disjvr_0^0, deltaext^0, wnt^0 Checking conditional termination of SCC {l3}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001068s Ranking function: (15 / 2) - 15*deltaext^0 + (15 / 2)*wnt^0 New Graphs: Transitions: undef1, rest remain the same}> Variables: __disjvr_0^0, deltaext^0, wnt^0 Checking conditional termination of SCC {l3}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000423s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001578s Trying to remove transition: undef1, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.003530s Time used: 0.003428 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.024138s Time used: 0.023858 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.001627s Time used: 4.00109 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.005324s Time used: 1.00001 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.009337s Time used: 0.005354 Termination failed. Trying to show unreachability... Proving unreachability of entry: LOG: CALL check - Post:1 <= 0 - Process 1 * Exit transition: * Postcondition : 1 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000958s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001000s Cannot prove unreachability Proving non-termination of subgraph 1 Transitions: undef1, rest remain the same}> undef1, deltaext^0 -> -1 + deltaext^0, rest remain the same}> undef1, deltaext^0 -> 1 + deltaext^0, rest remain the same}> Variables: __disjvr_0^0, deltaext^0, wnt^0 Checking conditional non-termination of SCC {l3}... > No exit transition to close. Checking that every undef value has an assignment... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001105s Calling reachability with... Transition: Conditions: OPEN EXITS: --- Reachability graph --- > Graph without transitions. Calling reachability with... Transition: Conditions: OPEN EXITS: > Conditions are reachable! Program does NOT terminate