NO Solver Timeout: 4 Global Timeout: 300 No parsing errors! Init Location: 0 Transitions: ~(1)) /\ ((undef2 - 1) <= arg1) /\ (arg1 > 0) /\ (undef1 > 0) /\ (undef2 > 1), par{arg1 -> undef1, arg2 -> undef2, arg3 -> 0, arg4 -> (arg2 + 1), arg5 -> 0, arg6 -> arg2}> arg3) /\ (arg5 > 0) /\ (arg6 > ~(1)) /\ (arg5 < undef11) /\ (arg1 >= undef7) /\ (arg2 >= undef7) /\ (arg1 > 0) /\ (arg2 > 0) /\ (undef7 > 0) /\ (undef8 > 0), par{arg1 -> undef7, arg2 -> undef8, arg3 -> (arg3 + 1), arg4 -> (arg6 + 1), arg5 -> undef11}> ~(1)) /\ (arg4 > arg3) /\ (undef13 <= arg1) /\ ((undef13 + 1) <= arg2) /\ ((undef14 - 3) <= arg1) /\ ((undef14 - 2) <= arg2) /\ (arg1 > 0) /\ (arg2 > 1) /\ (undef13 > 0) /\ (undef14 > 3), par{arg1 -> undef13, arg2 -> undef14, arg3 -> (arg3 + 1), arg4 -> (arg6 + 1), arg5 -> 1}> 0) /\ (undef19 > 0), par{arg1 -> undef19, arg2 -> (arg2 + 1), arg4 -> undef22, arg5 -> undef23, arg6 -> undef24}> 0) /\ (arg2 > 1) /\ (undef25 > 0), par{arg1 -> undef25, arg2 -> 1, arg3 -> arg6, arg4 -> undef28, arg5 -> undef29, arg6 -> undef30}> 0) /\ (arg4 <= arg3) /\ (arg1 > 0) /\ (arg2 > 0) /\ (undef31 > 0), par{arg1 -> undef31, arg2 -> arg5, arg3 -> 0, arg4 -> 0, arg5 -> 0, arg6 -> arg5}> 0) /\ (arg4 > 0) /\ (undef41 > arg5) /\ (arg5 < arg3) /\ (arg3 > 0) /\ (undef40 < arg4) /\ (arg5 < arg2) /\ (arg1 > 2) /\ (undef37 > 0), par{arg1 -> undef37, arg4 -> undef40, arg5 -> undef41, arg6 -> undef42}> ~(1)) /\ (arg3 > ~(1)) /\ (undef46 < arg3) /\ (arg1 > 2) /\ (undef43 > 0) /\ (arg1 >= (undef49 + 3)) /\ (arg2 = arg6), par{arg1 -> undef43, arg2 -> undef44, arg3 -> 0, arg4 -> undef46, arg5 -> 1, arg6 -> undef48}> undef50, arg2 -> undef51, arg3 -> undef52, arg4 -> undef53, arg5 -> undef54, arg6 -> undef55}> Fresh variables: undef1, undef2, undef7, undef8, undef11, undef13, undef14, undef19, undef22, undef23, undef24, undef25, undef28, undef29, undef30, undef31, undef37, undef40, undef41, undef42, undef43, undef44, undef46, undef48, undef49, undef50, undef51, undef52, undef53, undef54, undef55, Undef variables: undef1, undef2, undef7, undef8, undef11, undef13, undef14, undef19, undef22, undef23, undef24, undef25, undef28, undef29, undef30, undef31, undef37, undef40, undef41, undef42, undef43, undef44, undef46, undef48, undef49, undef50, undef51, undef52, undef53, undef54, undef55, Abstraction variables: Exit nodes: Accepting locations: Asserts: Preprocessed LLVMGraph Init Location: 0 Transitions: ~(1)) /\ ((undef2 - 1) <= undef50) /\ (undef50 > 0) /\ (undef1 > 0) /\ (undef2 > 1)> arg3) /\ (arg5 > 0) /\ (arg6 > ~(1)) /\ (arg5 < undef11) /\ (arg1 >= undef7) /\ (arg2 >= undef7) /\ (arg1 > 0) /\ (arg2 > 0) /\ (undef7 > 0) /\ (undef8 > 0), par{arg1 -> undef7, arg2 -> undef8, arg3 -> (arg3 + 1), arg4 -> (arg6 + 1), arg5 -> undef11}> ~(1)) /\ (arg4 > arg3) /\ (undef13 <= arg1) /\ ((undef13 + 1) <= arg2) /\ ((undef14 - 3) <= arg1) /\ ((undef14 - 2) <= arg2) /\ (arg1 > 0) /\ (arg2 > 1) /\ (undef13 > 0) /\ (undef14 > 3), par{arg1 -> undef13, arg2 -> undef14, arg3 -> (arg3 + 1), arg4 -> (arg6 + 1), arg5 -> 1}> 0) /\ (arg2 > 1) /\ (undef25 > 0), par{arg1 -> undef25, arg2 -> 1, arg3 -> arg6, arg4 -> undef28, arg5 -> undef29, arg6 -> undef30}> 0) /\ (arg4 <= arg3) /\ (arg1 > 0) /\ (arg2 > 0) /\ (undef31 > 0), par{arg1 -> undef31, arg2 -> arg5, arg3 -> 0, arg4 -> 0, arg5 -> 0, arg6 -> arg5}> 0) /\ (undef19 > 0), par{arg1 -> undef19, arg2 -> (arg2 + 1), arg4 -> undef22, arg5 -> undef23, arg6 -> undef24}> 0) /\ (arg4 > 0) /\ (undef41 > arg5) /\ (arg5 < arg3) /\ (arg3 > 0) /\ (undef40 < arg4) /\ (arg5 < arg2) /\ (arg1 > 2) /\ (undef37 > 0), par{arg1 -> undef37, arg4 -> undef40, arg5 -> undef41, arg6 -> undef42}> ~(1)) /\ (arg3 > ~(1)) /\ (undef46 < arg3) /\ (arg1 > 2) /\ (undef43 > 0) /\ (arg1 >= (undef49 + 3)) /\ (arg2 = arg6), par{arg1 -> undef43, arg2 -> undef44, arg3 -> 0, arg4 -> undef46, arg5 -> 1, arg6 -> undef48}> Fresh variables: undef1, undef2, undef7, undef8, undef11, undef13, undef14, undef19, undef22, undef23, undef24, undef25, undef28, undef29, undef30, undef31, undef37, undef40, undef41, undef42, undef43, undef44, undef46, undef48, undef49, undef50, undef51, undef52, undef53, undef54, undef55, Undef variables: undef1, undef2, undef7, undef8, undef11, undef13, undef14, undef19, undef22, undef23, undef24, undef25, undef28, undef29, undef30, undef31, undef37, undef40, undef41, undef42, undef43, undef44, undef46, undef48, undef49, undef50, undef51, undef52, undef53, undef54, undef55, Abstraction variables: Exit nodes: Accepting locations: Asserts: ************************************************************* ******************************************************************************************* *********************** WORKING TRANSITION SYSTEM (DAG) *********************** ******************************************************************************************* Init Location: 0 Graph 0: Transitions: Variables: Graph 1: Transitions: undef7, arg2 -> undef8, arg3 -> 1 + arg3, arg4 -> 1 + arg6, arg5 -> undef11, rest remain the same}> undef13, arg2 -> undef14, arg3 -> 1 + arg3, arg4 -> 1 + arg6, arg5 -> 1, rest remain the same}> Variables: arg1, arg2, arg3, arg4, arg5, arg6 Graph 2: Transitions: undef37, arg4 -> undef40, arg5 -> undef41, arg6 -> undef42, rest remain the same}> undef43, arg2 -> undef44, arg3 -> 0, arg4 -> undef46, arg5 -> 1, arg6 -> undef48, rest remain the same}> Variables: arg1, arg2, arg3, arg4, arg5, arg6 Graph 3: Transitions: undef19, arg2 -> 1 + arg2, arg4 -> undef22, arg5 -> undef23, arg6 -> undef24, rest remain the same}> Variables: arg1, arg2, arg4, arg5, arg6 Precedence: Graph 0 Graph 1 Graph 2 undef31, arg2 -> arg5, arg3 -> 0, arg4 -> 0, arg5 -> 0, arg6 -> arg5, rest remain the same}> Graph 3 undef25, arg2 -> 1, arg3 -> arg6, arg4 -> undef28, arg5 -> undef29, arg6 -> undef30, rest remain the same}> Map Locations to Subgraph: ( 0 , 0 ) ( 2 , 1 ) ( 3 , 3 ) ( 4 , 2 ) ******************************************************************************************* ******************************** CHECKING ASSERTIONS ******************************** ******************************************************************************************* Proving termination of subgraph 0 Proving termination of subgraph 1 Checking unfeasibility... Time used: 0.009778 Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001539s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.008878s Trying to remove transition: undef13, arg2 -> undef14, arg3 -> 1 + arg3, arg4 -> 1 + arg6, arg5 -> 1, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.015927s Time used: 0.015416 Trying to remove transition: undef7, arg2 -> undef8, arg3 -> 1 + arg3, arg4 -> 1 + arg6, arg5 -> undef11, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.013073s Time used: 0.012108 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.022405s Time used: 0.021511 LOG: SAT solveNonLinear - Elapsed time: 0.022405s Cost: 0; Total time: 0.021511 Termination implied by a set of invariant(s): Invariant at l2: arg4 <= 1 + arg6 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef7, arg2 -> undef8, arg3 -> 1 + arg3, arg4 -> 1 + arg6, arg5 -> undef11, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef13, arg2 -> undef14, arg3 -> 1 + arg3, arg4 -> 1 + arg6, arg5 -> 1, rest remain the same}> [ Termination Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef7, arg2 -> undef8, arg3 -> 1 + arg3, arg4 -> 1 + arg6, arg5 -> undef11, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef13, arg2 -> undef14, arg3 -> 1 + arg3, arg4 -> 1 + arg6, arg5 -> 1, rest remain the same}> Ranking function: -arg3 + arg6 New Graphs: INVARIANTS: 2: arg4 <= 1 + arg6 , Quasi-INVARIANTS to narrow Graph: 2: Proving termination of subgraph 2 Checking unfeasibility... Time used: 0.00601 Some transition disabled by a set of invariant(s): Invariant at l4: arg3 <= arg5 Strengthening and disabling transitions... > It's unfeasible. Removing transition: undef37, arg4 -> undef40, arg5 -> undef41, arg6 -> undef42, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef43, arg2 -> undef44, arg3 -> 0, arg4 -> undef46, arg5 -> 1, arg6 -> undef48, rest remain the same}> Checking unfeasibility... Time used: 0.002268 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001008s Ranking function: arg6 New Graphs: Proving termination of subgraph 3 Checking unfeasibility... Time used: 0.001732 Checking conditional termination of SCC {l3}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000465s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001241s Trying to remove transition: undef19, arg2 -> 1 + arg2, arg4 -> undef22, arg5 -> undef23, arg6 -> undef24, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.004957s Time used: 0.00487 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.001616s Time used: 4.00121 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.004298s Time used: 4.00061 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.002865s Time used: 1.00002 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.011490s Time used: 0.00724 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.023113s Time used: 1.0231 LOG: SAT solveNonLinear - Elapsed time: 1.034603s Cost: 1; Total time: 1.03034 Termination implied by a set of invariant(s): Invariant at l3: 0 <= arg2 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef19, arg2 -> 1 + arg2, arg4 -> undef22, arg5 -> undef23, arg6 -> undef24, 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): undef19, arg2 -> 1 + arg2, arg4 -> undef22, arg5 -> undef23, arg6 -> undef24, rest remain the same}> Quasi-ranking function: 50000 - arg2 New Graphs: Transitions: undef19, arg2 -> 1 + arg2, arg4 -> undef22, arg5 -> undef23, arg6 -> undef24, rest remain the same}> Variables: arg1, arg2, arg4, arg5, arg6 Checking conditional termination of SCC {l3}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000455s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001598s Trying to remove transition: undef19, arg2 -> 1 + arg2, arg4 -> undef22, arg5 -> undef23, arg6 -> undef24, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.005726s Time used: 0.005624 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.002435s Time used: 4.00185 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.004107s Time used: 4.00077 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.003502s Time used: 1.00006 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.012857s Time used: 0.008472 Improving Solution with cost 1 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.011800s Time used: 1.01178 LOG: SAT solveNonLinear - Elapsed time: 1.024657s Cost: 1; Total time: 1.02026 Termination implied by a set of invariant(s): Invariant at l3: 1 <= arg1 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef19, arg2 -> 1 + arg2, arg4 -> undef22, arg5 -> undef23, arg6 -> undef24, 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): undef19, arg2 -> 1 + arg2, arg4 -> undef22, arg5 -> undef23, arg6 -> undef24, rest remain the same}> Quasi-ranking function: 50000 + 50000*arg1 - arg2 New Graphs: Transitions: undef19, arg2 -> 1 + arg2, arg4 -> undef22, arg5 -> undef23, arg6 -> undef24, rest remain the same}> Variables: arg1, arg2, arg4, arg5, arg6 Checking conditional termination of SCC {l3}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000505s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002352s Trying to remove transition: undef19, arg2 -> 1 + arg2, arg4 -> undef22, arg5 -> undef23, arg6 -> undef24, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.006767s Time used: 0.006656 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.007299s Time used: 4.00674 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.004404s Time used: 4.00096 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.003052s Time used: 1.00007 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.008153s Time used: 4.00392 Termination failed. Trying to show unreachability... Proving unreachability of entry: undef25, arg2 -> 1, arg3 -> arg6, arg4 -> undef28, arg5 -> undef29, arg6 -> undef30, rest remain the same}> LOG: CALL check - Post:1 <= 0 - Process 1 * Exit transition: undef25, arg2 -> 1, arg3 -> arg6, arg4 -> undef28, arg5 -> undef29, arg6 -> undef30, rest remain the same}> * Postcondition : 1 <= 0 Postcodition moved up: 1 <= 0 LOG: Try proving POST Postcondition: 1 <= 0 LOG: CALL check - Post:1 <= 0 - Process 2 * Exit transition: * Postcondition : 1 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000796s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000889s LOG: NarrowEntry size 1 Narrowing transition: undef7, arg2 -> undef8, arg3 -> 1 + arg3, arg4 -> 1 + arg6, arg5 -> undef11, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef13, arg2 -> undef14, arg3 -> 1 + arg3, arg4 -> 1 + arg6, arg5 -> 1, rest remain the same}> LOG: Narrow transition size 1 ENTRIES: END ENTRIES: GRAPH: undef7, arg2 -> undef8, arg3 -> 1 + arg3, arg4 -> 1 + arg6, arg5 -> undef11, rest remain the same}> undef13, arg2 -> undef14, arg3 -> 1 + arg3, arg4 -> 1 + arg6, arg5 -> 1, rest remain the same}> END GRAPH: EXIT: undef25, arg2 -> 1, arg3 -> arg6, arg4 -> undef28, arg5 -> undef29, arg6 -> undef30, rest remain the same}> POST: 1 <= 0 LOG: Try proving POST Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.052601s Time used: 0.05254 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.412965s Time used: 0.411717 Improving Solution with cost 51 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.000549s Time used: 1.00053 LOG: SAT solveNonLinear - Elapsed time: 1.413514s Cost: 51; Total time: 1.41224 Failed at location 2: arg4 + arg5 + arg6 <= 1 + arg3 Before Improving: Quasi-invariant at l2: 1 + arg6 <= arg4 + arg5 Quasi-invariant at l2: arg4 + arg5 + arg6 <= 1 + arg3 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.008897s Remaining time after improvement: 0.997313 Some transition disabled by a set of quasi-invariant(s): Quasi-invariant at l2: 1 + arg6 <= arg4 + arg5 Quasi-invariant at l2: arg4 + arg5 + arg6 <= 1 + arg3 LOG: NEXT CALL check - disable LOG: CALL check - Post:arg4 + arg5 + arg6 <= 1 + arg3 - Process 3 * Exit transition: * Postcondition : arg4 + arg5 + arg6 <= 1 + arg3 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001579s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001676s Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.000211s Time used: 1.00012 LOG: Postcondition is not implied - no solution > Postcondition is not implied! LOG: RETURN check - Elapsed time: 2.496274s Cannot prove unreachability Proving non-termination of subgraph 3 Transitions: undef19, arg2 -> 1 + arg2, arg4 -> undef22, arg5 -> undef23, arg6 -> undef24, rest remain the same}> Variables: arg1, arg2, arg4, arg5, arg6 Checking that every undef value has an assignment... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000918s Checking conditional non-termination of SCC {l3}... EXIT TRANSITIONS: Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.014663s Time used: 0.01458 LOG: SAT solveNonLinear - Elapsed time: 0.014663s Cost: 0; Total time: 0.01458 Minimizing number of undef constraints... LOG: CALL solveNonLinear LOG: RETURN solveNonLinear - Elapsed time: 0.004425s Number of undef constraints reduced! Non-termination implied by a set of quasi-invariant(s): Quasi-invariant at l3: 1 <= arg1 Strengthening and disabling EXIT transitions... Closed exits from l3: 1 Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef19, arg2 -> 1 + arg2, arg4 -> undef22, arg5 -> undef23, arg6 -> undef24, rest remain the same}> Calling reachability with... Transition: Conditions: 1 <= arg1, OPEN EXITS: --- Reachability graph --- > Graph without transitions. Calling reachability with... Transition: undef25, arg2 -> 1, arg3 -> arg6, arg4 -> undef28, arg5 -> undef29, arg6 -> undef30, rest remain the same}> Conditions: 1 <= arg1, OPEN EXITS: undef25, arg2 -> 1, arg3 -> arg6, arg4 -> undef28, arg5 -> undef29, arg6 -> undef30, rest remain the same}> (condsUp: 1 <= undef25, 1 <= undef25) --- Reachability graph --- > Graph without transitions. Calling reachability with... Transition: Conditions: 1 <= arg1, 1 + undef25 <= arg2, undef25 <= arg1, arg4 <= arg3, 2 <= arg2, 1 <= undef25, 1 <= undef25, OPEN EXITS: > Conditions are not feasible after transitions. --- Reachability graph --- Transitions: undef7, arg2 -> undef8, arg3 -> 1 + arg3, arg4 -> 1 + arg6, arg5 -> undef11, rest remain the same}> Variables: arg1, arg2, arg3, arg4, arg5, arg6, undef25 Checking that every undef value has an assignment... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002057s Checking edge-closing of SCC {l2}... EXIT TRANSITIONS (TO CLOSE): Solving with 1 template(s). WARNING: Applying substitution to an expression with non-program variables. WARNING: Applying substitution to an expression with non-program variables. LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.081688s Time used: 0.081188 Improving Solution with cost 10 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.797129s Time used: 0.797113 Improving Solution with cost 7 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.076351s Time used: 0.076348 LOG: SAT solveNonLinear - Elapsed time: 0.955168s Cost: 7; Total time: 0.954649 Minimizing number of undef constraints... LOG: CALL solveNonLinear LOG: RETURN solveNonLinear - Elapsed time: 0.011905s Edge-closing implied by a set of quasi-invariant(s): Quasi-invariant at l2: 2 <= arg2 Constraint over undef '11 <= undef8' in transition: undef7, arg2 -> undef8, arg3 -> 1 + arg3, arg4 -> 1 + arg6, arg5 -> undef11, rest remain the same}> Strengthening and disabling EXIT transitions... EXIT TRANSITIONS TO BE CLOSED: Closed exits from l2: 3 Strengthening exit transition (result): Strengthening exit transition (result): Strengthening exit transition (result): EXIT TRANSITIONS TO KEEP OPEN: Strengthening exit transition (result): undef25, arg2 -> 1, arg3 -> arg6, arg4 -> undef28, arg5 -> undef29, arg6 -> undef30, rest remain the same}> Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef7, arg2 -> undef8, arg3 -> 1 + arg3, arg4 -> 1 + arg6, arg5 -> undef11, rest remain the same}> Checking edge-closing of SCC {l2}... EXIT TRANSITIONS (TO CLOSE): Solving with 1 template(s). WARNING: Applying substitution to an expression with non-program variables. WARNING: Applying substitution to an expression with non-program variables. LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.053119s Time used: 0.052654 Improving Solution with cost 3 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.072897s Time used: 0.072892 LOG: SAT solveNonLinear - Elapsed time: 0.126016s Cost: 3; Total time: 0.125546 Minimizing number of undef constraints... LOG: CALL solveNonLinear LOG: RETURN solveNonLinear - Elapsed time: 0.009603s Number of undef constraints reduced! Edge-closing implied by a set of quasi-invariant(s): Quasi-invariant at l2: 1 <= arg1 Strengthening and disabling EXIT transitions... EXIT TRANSITIONS TO BE CLOSED: Closed exits from l2: 1 Strengthening exit transition (result): Strengthening exit transition (result): EXIT TRANSITIONS TO KEEP OPEN: Strengthening exit transition (result): undef25, arg2 -> 1, arg3 -> arg6, arg4 -> undef28, arg5 -> undef29, arg6 -> undef30, rest remain the same}> Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef7, arg2 -> undef8, arg3 -> 1 + arg3, arg4 -> 1 + arg6, arg5 -> undef11, rest remain the same}> Checking edge-closing of SCC {l2}... EXIT TRANSITIONS (TO CLOSE): Solving with 1 template(s). WARNING: Applying substitution to an expression with non-program variables. WARNING: Applying substitution to an expression with non-program variables. LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.078677s Time used: 0.078409 Improving Solution with cost 2 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.136381s Time used: 0.136373 LOG: SAT solveNonLinear - Elapsed time: 0.215058s Cost: 2; Total time: 0.214782 Minimizing number of undef constraints... LOG: CALL solveNonLinear LOG: RETURN solveNonLinear - Elapsed time: 0.010358s Number of undef constraints reduced! Edge-closing implied by a set of quasi-invariant(s): Quasi-invariant at l2: arg5 <= 0 Strengthening and disabling EXIT transitions... EXIT TRANSITIONS TO BE CLOSED: Closed exits from l2: 1 Strengthening exit transition (result): EXIT TRANSITIONS TO KEEP OPEN: Strengthening exit transition (result): undef25, arg2 -> 1, arg3 -> arg6, arg4 -> undef28, arg5 -> undef29, arg6 -> undef30, rest remain the same}> Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef7, arg2 -> undef8, arg3 -> 1 + arg3, arg4 -> 1 + arg6, arg5 -> undef11, rest remain the same}> EXIT TRANSITIONS (TO CLOSE): Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.000758s Time used: 0.000533 Solving with 2 template(s). WARNING: Applying substitution to an expression with non-program variables. LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.014380s Time used: 0.014318 Solving with 3 template(s). WARNING: Applying substitution to an expression with non-program variables. WARNING: Applying substitution to an expression with non-program variables. LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 5.001352s Time used: 5.00101 > No quasi-invariants that block all exits have been found. --- Reachability graph --- Transitions: undef7, arg2 -> undef8, arg3 -> 1 + arg3, arg4 -> 1 + arg6, arg5 -> undef11, rest remain the same}> Variables: arg1, arg2, arg3, arg4, arg5, arg6, undef25 Checking that every undef value has an assignment... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001220s Checking edge-closing of SCC {l2}... > No assignment for some undef value. > No quasi-invariants that block all exits have been found. --- Reachability graph --- Transitions: undef7, arg2 -> undef8, arg3 -> 1 + arg3, arg4 -> 1 + arg6, arg5 -> undef11, rest remain the same}> undef7, arg2 -> undef8, arg3 -> 1 + arg3, arg4 -> 1 + arg6, arg5 -> undef11, rest remain the same}> Variables: arg1, arg2, arg3, arg4, arg5, arg6, undef25 Checking that every undef value has an assignment... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002698s Checking edge-closing of SCC {l2}... > No assignment for some undef value. > No quasi-invariants that block all exits have been found. --- Reachability graph --- Transitions: undef7, arg2 -> undef8, arg3 -> 1 + arg3, arg4 -> 1 + arg6, arg5 -> undef11, rest remain the same}> Variables: arg1, arg2, arg3, arg4, arg5, arg6, undef25 Checking that every undef value has an assignment... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001966s Checking edge-closing of SCC {l2}... EXIT TRANSITIONS (TO CLOSE): Solving with 1 template(s). WARNING: Applying substitution to an expression with non-program variables. WARNING: Applying substitution to an expression with non-program variables. LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.064494s Time used: 0.063986 Improving Solution with cost 10 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.313863s Time used: 0.313852 Improving Solution with cost 7 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.134011s Time used: 0.134007 LOG: SAT solveNonLinear - Elapsed time: 0.512368s Cost: 7; Total time: 0.511845 Minimizing number of undef constraints... LOG: CALL solveNonLinear LOG: RETURN solveNonLinear - Elapsed time: 0.012011s Edge-closing implied by a set of quasi-invariant(s): Quasi-invariant at l2: 2 <= arg2 Constraint over undef '2 <= undef8' in transition: undef7, arg2 -> undef8, arg3 -> 1 + arg3, arg4 -> 1 + arg6, arg5 -> undef11, rest remain the same}> Strengthening and disabling EXIT transitions... EXIT TRANSITIONS TO BE CLOSED: Closed exits from l2: 3 Strengthening exit transition (result): Strengthening exit transition (result): Strengthening exit transition (result): EXIT TRANSITIONS TO KEEP OPEN: Strengthening exit transition (result): undef25, arg2 -> 1, arg3 -> arg6, arg4 -> undef28, arg5 -> undef29, arg6 -> undef30, rest remain the same}> Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef7, arg2 -> undef8, arg3 -> 1 + arg3, arg4 -> 1 + arg6, arg5 -> undef11, rest remain the same}> Checking edge-closing of SCC {l2}... EXIT TRANSITIONS (TO CLOSE): Solving with 1 template(s). WARNING: Applying substitution to an expression with non-program variables. WARNING: Applying substitution to an expression with non-program variables. LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.036908s Time used: 0.036497 Improving Solution with cost 3 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.091419s Time used: 0.091416 LOG: SAT solveNonLinear - Elapsed time: 0.128327s Cost: 3; Total time: 0.127913 Minimizing number of undef constraints... LOG: CALL solveNonLinear LOG: RETURN solveNonLinear - Elapsed time: 0.009443s Number of undef constraints reduced! Edge-closing implied by a set of quasi-invariant(s): Quasi-invariant at l2: 1 <= arg1 Strengthening and disabling EXIT transitions... EXIT TRANSITIONS TO BE CLOSED: Closed exits from l2: 1 Strengthening exit transition (result): Strengthening exit transition (result): EXIT TRANSITIONS TO KEEP OPEN: Strengthening exit transition (result): undef25, arg2 -> 1, arg3 -> arg6, arg4 -> undef28, arg5 -> undef29, arg6 -> undef30, rest remain the same}> Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef7, arg2 -> undef8, arg3 -> 1 + arg3, arg4 -> 1 + arg6, arg5 -> undef11, rest remain the same}> Checking edge-closing of SCC {l2}... EXIT TRANSITIONS (TO CLOSE): Solving with 1 template(s). WARNING: Applying substitution to an expression with non-program variables. WARNING: Applying substitution to an expression with non-program variables. LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.063061s Time used: 0.062819 Improving Solution with cost 2 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.074409s Time used: 0.074405 LOG: SAT solveNonLinear - Elapsed time: 0.137470s Cost: 2; Total time: 0.137224 Minimizing number of undef constraints... LOG: CALL solveNonLinear LOG: RETURN solveNonLinear - Elapsed time: 0.008980s Number of undef constraints reduced! Edge-closing implied by a set of quasi-invariant(s): Quasi-invariant at l2: arg5 <= 0 Strengthening and disabling EXIT transitions... EXIT TRANSITIONS TO BE CLOSED: Closed exits from l2: 1 Strengthening exit transition (result): EXIT TRANSITIONS TO KEEP OPEN: Strengthening exit transition (result): undef25, arg2 -> 1, arg3 -> arg6, arg4 -> undef28, arg5 -> undef29, arg6 -> undef30, rest remain the same}> Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef7, arg2 -> undef8, arg3 -> 1 + arg3, arg4 -> 1 + arg6, arg5 -> undef11, rest remain the same}> EXIT TRANSITIONS (TO CLOSE): Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.000797s Time used: 0.000555 Solving with 2 template(s). WARNING: Applying substitution to an expression with non-program variables. LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.014874s Time used: 0.014811 Solving with 3 template(s). WARNING: Applying substitution to an expression with non-program variables. WARNING: Applying substitution to an expression with non-program variables. LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 5.001662s Time used: 5.00126 > No quasi-invariants that block all exits have been found. --- Reachability graph --- Transitions: undef7, arg2 -> undef8, arg3 -> 1 + arg3, arg4 -> 1 + arg6, arg5 -> undef11, rest remain the same}> undef7, arg2 -> undef8, arg3 -> 1 + arg3, arg4 -> 1 + arg6, arg5 -> undef11, rest remain the same}> Variables: arg1, arg2, arg3, arg4, arg5, arg6, undef25 Checking that every undef value has an assignment... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003765s Checking edge-closing of SCC {l2}... EXIT TRANSITIONS (TO CLOSE): Solving with 1 template(s). WARNING: Applying substitution to an expression with non-program variables. WARNING: Applying substitution to an expression with non-program variables. WARNING: Applying substitution to an expression with non-program variables. LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.118971s Time used: 0.117995 Improving Solution with cost 10 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.001048s Time used: 1.00103 LOG: SAT solveNonLinear - Elapsed time: 1.120020s Cost: 10; Total time: 1.11903 Minimizing number of undef constraints... LOG: CALL solveNonLinear LOG: RETURN solveNonLinear - Elapsed time: 0.018864s Number of undef constraints reduced! Edge-closing implied by a set of quasi-invariant(s): Quasi-invariant at l2: 1 <= arg1 Strengthening and disabling EXIT transitions... EXIT TRANSITIONS TO BE CLOSED: Closed exits from l2: 2 Strengthening exit transition (result): Strengthening exit transition (result): Strengthening exit transition (result): Strengthening exit transition (result): EXIT TRANSITIONS TO KEEP OPEN: Strengthening exit transition (result): undef25, arg2 -> 1, arg3 -> arg6, arg4 -> undef28, arg5 -> undef29, arg6 -> undef30, rest remain the same}> Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef7, arg2 -> undef8, arg3 -> 1 + arg3, arg4 -> 1 + arg6, arg5 -> undef11, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef7, arg2 -> undef8, arg3 -> 1 + arg3, arg4 -> 1 + arg6, arg5 -> undef11, rest remain the same}> Checking edge-closing of SCC {l2}... EXIT TRANSITIONS (TO CLOSE): Solving with 1 template(s). WARNING: Applying substitution to an expression with non-program variables. WARNING: Applying substitution to an expression with non-program variables. WARNING: Applying substitution to an expression with non-program variables. LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 5.000856s Time used: 5.00072 Solving with 2 template(s). WARNING: Applying substitution to an expression with non-program variables. WARNING: Applying substitution to an expression with non-program variables. WARNING: Applying substitution to an expression with non-program variables. WARNING: Applying substitution to an expression with non-program variables. WARNING: Applying substitution to an expression with non-program variables. WARNING: Applying substitution to an expression with non-program variables. LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 5.118692s Time used: 5.00158 Solving with 3 template(s). WARNING: Applying substitution to an expression with non-program variables. WARNING: Applying substitution to an expression with non-program variables. WARNING: Applying substitution to an expression with non-program variables. WARNING: Applying substitution to an expression with non-program variables. WARNING: Applying substitution to an expression with non-program variables. WARNING: Applying substitution to an expression with non-program variables. WARNING: Applying substitution to an expression with non-program variables. WARNING: Applying substitution to an expression with non-program variables. WARNING: Applying substitution to an expression with non-program variables. LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.960563s Time used: 0.955837 Improving Solution with cost 2 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.001291s Time used: 1.00127 LOG: SAT solveNonLinear - Elapsed time: 1.961855s Cost: 2; Total time: 1.95711 Minimizing number of undef constraints... LOG: CALL solveNonLinear LOG: RETURN solveNonLinear - Elapsed time: 0.036627s Number of undef constraints reduced! Edge-closing implied by a set of quasi-invariant(s): Quasi-invariant at l2: arg5 <= 0 Quasi-invariant at l2: 1 <= arg2 + arg5 Quasi-invariant at l2: 1 + arg3 + arg5 <= arg4 Strengthening and disabling EXIT transitions... EXIT TRANSITIONS TO BE CLOSED: Closed exits from l2: 3 Strengthening exit transition (result): EXIT TRANSITIONS TO KEEP OPEN: Strengthening exit transition (result): undef25, arg2 -> 1, arg3 -> arg6, arg4 -> undef28, arg5 -> undef29, arg6 -> undef30, rest remain the same}> Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef7, arg2 -> undef8, arg3 -> 1 + arg3, arg4 -> 1 + arg6, arg5 -> undef11, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef7, arg2 -> undef8, arg3 -> 1 + arg3, arg4 -> 1 + arg6, arg5 -> undef11, rest remain the same}> EXIT TRANSITIONS (TO CLOSE): Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.000918s Time used: 0.00063 Solving with 2 template(s). WARNING: Applying substitution to an expression with non-program variables. LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.018064s Time used: 0.017998 Solving with 3 template(s). WARNING: Applying substitution to an expression with non-program variables. WARNING: Applying substitution to an expression with non-program variables. LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 5.002172s Time used: 5.00172 > No quasi-invariants that block all exits have been found. --- Reachability graph --- Transitions: undef7, arg2 -> undef8, arg3 -> 1 + arg3, arg4 -> 1 + arg6, arg5 -> undef11, rest remain the same}> undef7, arg2 -> undef8, arg3 -> 1 + arg3, arg4 -> 1 + arg6, arg5 -> undef11, rest remain the same}> Variables: arg1, arg2, arg3, arg4, arg5, arg6, undef25 Checking that every undef value has an assignment... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002695s Checking edge-closing of SCC {l2}... > No assignment for some undef value. > No quasi-invariants that block all exits have been found. --- Reachability graph --- Transitions: undef7, arg2 -> undef8, arg3 -> 1 + arg3, arg4 -> 1 + arg6, arg5 -> undef11, rest remain the same}> undef7, arg2 -> undef8, arg3 -> 1 + arg3, arg4 -> 1 + arg6, arg5 -> undef11, rest remain the same}> undef7, arg2 -> undef8, arg3 -> 1 + arg3, arg4 -> 1 + arg6, arg5 -> undef11, rest remain the same}> Variables: arg1, arg2, arg3, arg4, arg5, arg6, undef25 Checking that every undef value has an assignment... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004161s Checking edge-closing of SCC {l2}... > No assignment for some undef value. > No quasi-invariants that block all exits have been found. --- Reachability graph --- Transitions: undef13, arg2 -> undef14, arg3 -> 1 + arg3, arg4 -> 1 + arg6, arg5 -> 1, rest remain the same}> Variables: arg1, arg2, arg3, arg4, arg5, arg6 Checking that every undef value has an assignment... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002126s Checking edge-closing of SCC {l2}... EXIT TRANSITIONS (TO CLOSE): Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.031290s Time used: 0.030876 Improving Solution with cost 5 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.108759s Time used: 0.108748 LOG: SAT solveNonLinear - Elapsed time: 0.140049s Cost: 5; Total time: 0.139624 Minimizing number of undef constraints... LOG: CALL solveNonLinear LOG: RETURN solveNonLinear - Elapsed time: 0.027387s Number of undef constraints reduced! Edge-closing implied by a set of quasi-invariant(s): Quasi-invariant at l2: 1 <= arg1 Strengthening and disabling EXIT transitions... EXIT TRANSITIONS TO BE CLOSED: Closed exits from l2: 1 Strengthening exit transition (result): Strengthening exit transition (result): Strengthening exit transition (result): EXIT TRANSITIONS TO KEEP OPEN: Strengthening exit transition (result): undef25, arg2 -> 1, arg3 -> arg6, arg4 -> undef28, arg5 -> undef29, arg6 -> undef30, rest remain the same}> Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef13, arg2 -> undef14, arg3 -> 1 + arg3, arg4 -> 1 + arg6, arg5 -> 1, rest remain the same}> Checking edge-closing of SCC {l2}... EXIT TRANSITIONS (TO CLOSE): Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.056774s Time used: 0.056369 Improving Solution with cost 3 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.123380s Time used: 0.123376 Improving Solution with cost 2 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.123683s Time used: 0.123679 LOG: SAT solveNonLinear - Elapsed time: 0.303838s Cost: 2; Total time: 0.303424 Minimizing number of undef constraints... LOG: CALL solveNonLinear LOG: RETURN solveNonLinear - Elapsed time: 0.012389s Number of undef constraints reduced! Edge-closing implied by a set of quasi-invariant(s): Quasi-invariant at l2: 2 <= arg2 Strengthening and disabling EXIT transitions... EXIT TRANSITIONS TO BE CLOSED: Closed exits from l2: 2 Strengthening exit transition (result): EXIT TRANSITIONS TO KEEP OPEN: Strengthening exit transition (result): undef25, arg2 -> 1, arg3 -> arg6, arg4 -> undef28, arg5 -> undef29, arg6 -> undef30, rest remain the same}> Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef13, arg2 -> undef14, arg3 -> 1 + arg3, arg4 -> 1 + arg6, arg5 -> 1, rest remain the same}> Checking edge-closing of SCC {l2}... EXIT TRANSITIONS (TO CLOSE): Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.027466s Time used: 0.027393 LOG: SAT solveNonLinear - Elapsed time: 0.027466s Cost: 0; Total time: 0.027393 Minimizing number of undef constraints... LOG: CALL solveNonLinear LOG: RETURN solveNonLinear - Elapsed time: 0.010201s Number of undef constraints reduced! Edge-closing implied by a set of quasi-invariant(s): Quasi-invariant at l2: 0 <= arg6 Strengthening and disabling EXIT transitions... EXIT TRANSITIONS TO BE CLOSED: Closed exits from l2: 1 EXIT TRANSITIONS TO KEEP OPEN: Strengthening exit transition (result): undef25, arg2 -> 1, arg3 -> arg6, arg4 -> undef28, arg5 -> undef29, arg6 -> undef30, rest remain the same}> Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef13, arg2 -> undef14, arg3 -> 1 + arg3, arg4 -> 1 + arg6, arg5 -> 1, rest remain the same}> Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000869s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004116s Trying to remove transition: undef13, arg2 -> undef14, arg3 -> 1 + arg3, arg4 -> 1 + arg6, arg5 -> 1, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.013058s Time used: 0.012629 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.016775s Time used: 0.015962 LOG: SAT solveNonLinear - Elapsed time: 0.016775s Cost: 0; Total time: 0.015962 Termination implied by a set of invariant(s): Invariant at l2: 1 + arg6 <= arg4 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef13, arg2 -> undef14, arg3 -> 1 + arg3, arg4 -> 1 + arg6, arg5 -> 1, 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): undef13, arg2 -> undef14, arg3 -> 1 + arg3, arg4 -> 1 + arg6, arg5 -> 1, rest remain the same}> Ranking function: -arg3 + arg4 New Graphs: Calling reachability with... Transition: Conditions: 1 <= arg1, 0 <= arg6, 2 <= arg2, 1 <= undef25, 1 <= undef25, OPEN EXITS: > Conditions are reachable! Program does NOT terminate