NO Solver Timeout: 4 Global Timeout: 300 No parsing errors! Init Location: 0 Transitions: (1 + i^0), j^0 -> (2 + j^0), ret_pair5^0 -> undef3}> 0, j^0 -> 0}> Fresh variables: undef3, Undef variables: undef3, Abstraction variables: Exit nodes: Accepting locations: Asserts: Preprocessed LLVMGraph Init Location: 0 Transitions: (1 + i^0), j^0 -> (2 + j^0)}> Fresh variables: undef3, Undef variables: undef3, Abstraction variables: Exit nodes: Accepting locations: Asserts: ************************************************************* ******************************************************************************************* *********************** WORKING TRANSITION SYSTEM (DAG) *********************** ******************************************************************************************* Init Location: 0 Graph 0: Transitions: Variables: Graph 1: Transitions: 1 + i^0, j^0 -> 2 + j^0, rest remain the same}> Variables: i^0, j^0 Graph 2: Transitions: Variables: Precedence: Graph 0 Graph 1 Graph 2 Map Locations to Subgraph: ( 0 , 0 ) ( 2 , 1 ) ( 3 , 2 ) ******************************************************************************************* ******************************** CHECKING ASSERTIONS ******************************** ******************************************************************************************* Proving termination of subgraph 0 Proving termination of subgraph 1 Checking unfeasibility... Time used: 0.002033 Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000439s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000990s Trying to remove transition: 1 + i^0, j^0 -> 2 + j^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.003976s Time used: 0.003883 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.001049s Time used: 4.00071 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.003241s Time used: 4.00058 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.006570s Time used: 1.00034 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.008654s Time used: 0.004764 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.002164s Time used: 1.00215 LOG: SAT solveNonLinear - Elapsed time: 1.010818s Cost: 1; Total time: 1.00691 Quasi-ranking function: 50000 - i^0 New Graphs: Transitions: 1 + i^0, j^0 -> 2 + j^0, rest remain the same}> Variables: i^0, j^0 Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000252s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000766s Trying to remove transition: 1 + i^0, j^0 -> 2 + j^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.004418s Time used: 0.004351 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.001451s Time used: 4.00109 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.003538s Time used: 4.0006 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.006829s Time used: 1.00108 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.008292s Time used: 0.005229 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.003204s Time used: 1.00318 LOG: SAT solveNonLinear - Elapsed time: 1.011497s Cost: 1; Total time: 1.00841 Termination implied by a set of invariant(s): Invariant at l2: 0 <= 1 + i^0 + j^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + i^0, j^0 -> 2 + j^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): 1 + i^0, j^0 -> 2 + j^0, rest remain the same}> Quasi-ranking function: 50000 - j^0 New Graphs: Transitions: 1 + i^0, j^0 -> 2 + j^0, rest remain the same}> Variables: i^0, j^0 Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000322s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001733s Trying to remove transition: 1 + i^0, j^0 -> 2 + j^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.005331s Time used: 0.005246 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.001253s Time used: 4.00084 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.005061s Time used: 4.00149 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.005953s Time used: 1.00074 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.010380s Time used: 0.006543 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.000705s Time used: 1.00069 LOG: SAT solveNonLinear - Elapsed time: 1.011085s Cost: 1; Total time: 1.00723 Termination implied by a set of invariant(s): Invariant at l2: i^0 <= 1 + j^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + i^0, j^0 -> 2 + j^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): 1 + i^0, j^0 -> 2 + j^0, rest remain the same}> Quasi-ranking function: 50000 + i^0 - j^0 New Graphs: Transitions: 1 + i^0, j^0 -> 2 + j^0, rest remain the same}> Variables: i^0, j^0 Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000398s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002655s Trying to remove transition: 1 + i^0, j^0 -> 2 + j^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.014518s Time used: 0.014424 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.002103s Time used: 4.00175 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.003260s Time used: 4.00091 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.006162s Time used: 1.00081 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.011177s Time used: 0.007163 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.000623s Time used: 1.0006 LOG: SAT solveNonLinear - Elapsed time: 1.011799s Cost: 1; Total time: 1.00777 Termination implied by a set of invariant(s): Invariant at l2: 0 <= i^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1 + i^0, j^0 -> 2 + j^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): 1 + i^0, j^0 -> 2 + j^0, rest remain the same}> Quasi-ranking function: 50000 - 3*i^0 + j^0 New Graphs: Transitions: 1 + i^0, j^0 -> 2 + j^0, rest remain the same}> Variables: i^0, j^0 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.002259s Trying to remove transition: 1 + i^0, j^0 -> 2 + j^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.022586s Time used: 0.022491 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.000935s Time used: 4.00061 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.005242s Time used: 4.00106 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.016431s Time used: 1.01086 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.010685s Time used: 0.006732 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.000745s Time used: 1.00073 LOG: SAT solveNonLinear - Elapsed time: 1.011431s Cost: 1; Total time: 1.00746 Quasi-ranking function: 50000 - i^0 - j^0 New Graphs: Transitions: 1 + i^0, j^0 -> 2 + j^0, rest remain the same}> Variables: i^0, j^0 Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000422s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001818s Trying to remove transition: 1 + i^0, j^0 -> 2 + j^0, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.022968s Time used: 0.022869 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.002009s Time used: 4.00165 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.003803s Time used: 4.00161 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.006575s Time used: 1.00092 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.005434s Time used: 4.00157 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.003439s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.003480s Cannot prove unreachability Proving non-termination of subgraph 1 Transitions: 1 + i^0, j^0 -> 2 + j^0, rest remain the same}> Variables: i^0, j^0 Checking conditional non-termination of SCC {l2}... > No exit transition to close. 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