YES Solver Timeout: 4 Global Timeout: 300 No parsing errors! Init Location: 0 Transitions: ~(1)) /\ (arg1 > 0) /\ (undef1 > 0), par{arg1 -> undef1, arg2 -> (arg2 - 1), arg3 -> arg2, arg4 -> arg2}> 0) /\ (arg1 > 0) /\ (undef5 > 0), par{arg1 -> undef5, arg2 -> (arg2 - 1), arg3 -> arg2}> ~(1)) /\ (arg1 >= undef9) /\ (arg1 > 0) /\ (undef9 > 0), par{arg1 -> undef9, arg2 -> (arg4 - 1), arg3 -> arg4}> 0) /\ (arg1 > 0) /\ (undef13 > 0), par{arg1 -> undef13, arg2 -> (arg2 - 1), arg3 -> arg2}> ~(1)) /\ (arg1 > 0), par{arg1 -> (arg4 - 1), arg2 -> arg4, arg3 -> undef19, arg4 -> undef20}> 2, arg2 -> undef22, arg3 -> undef23, arg4 -> undef24}> 0), par{arg1 -> (arg1 - 1), arg2 -> arg1, arg3 -> undef27, arg4 -> undef28}> ~(1)) /\ (undef29 > ~(1)) /\ (arg1 < 3), par{arg1 -> undef29, arg2 -> undef30, arg3 -> undef31, arg4 -> undef32}> ~(1)) /\ (arg1 < 3), par{arg1 -> (arg1 - 1), arg2 -> undef34, arg3 -> undef35, arg4 -> undef36}> 0) /\ (undef37 > ~(1)), par{arg1 -> undef37, arg2 -> undef38, arg3 -> undef39, arg4 -> undef40}> undef41, arg2 -> undef42, arg3 -> undef43, arg4 -> undef44}> Fresh variables: undef1, undef5, undef9, undef13, undef19, undef20, undef22, undef23, undef24, undef27, undef28, undef29, undef30, undef31, undef32, undef34, undef35, undef36, undef37, undef38, undef39, undef40, undef41, undef42, undef43, undef44, Undef variables: undef1, undef5, undef9, undef13, undef19, undef20, undef22, undef23, undef24, undef27, undef28, undef29, undef30, undef31, undef32, undef34, undef35, undef36, undef37, undef38, undef39, undef40, undef41, undef42, undef43, undef44, Abstraction variables: Exit nodes: Accepting locations: Asserts: Preprocessed LLVMGraph Init Location: 0 Transitions: ~(1)) /\ (undef41 > 0) /\ (undef1 > 0)> 0) /\ (arg1 > 0) /\ (undef5 > 0), par{arg1 -> undef5, arg2 -> (arg2 - 1), arg3 -> arg2}> ~(1)) /\ (arg1 >= undef9) /\ (arg1 > 0) /\ (undef9 > 0), par{arg1 -> undef9, arg2 -> (arg4 - 1), arg3 -> arg4}> 0) /\ (arg1 > 0) /\ (undef13 > 0), par{arg1 -> undef13, arg2 -> (arg2 - 1), arg3 -> arg2}> ~(1)) /\ (arg1 > 0), par{arg1 -> (arg4 - 1), arg2 -> arg4, arg3 -> undef19, arg4 -> undef20}> 2, arg2 -> undef22, arg3 -> undef23, arg4 -> undef24}> 0), par{arg1 -> (arg1 - 1), arg2 -> arg1, arg3 -> undef27, arg4 -> undef28}> ~(1)) /\ (undef29 > ~(1)) /\ (arg1 < 3), par{arg1 -> undef29, arg2 -> undef30, arg3 -> undef31, arg4 -> undef32}> ~(1)) /\ (arg1 < 3), par{arg1 -> (arg1 - 1), arg2 -> undef34, arg3 -> undef35, arg4 -> undef36}> 0) /\ (undef37 > ~(1)), par{arg1 -> undef37, arg2 -> undef38, arg3 -> undef39, arg4 -> undef40}> Fresh variables: undef1, undef5, undef9, undef13, undef19, undef20, undef22, undef23, undef24, undef27, undef28, undef29, undef30, undef31, undef32, undef34, undef35, undef36, undef37, undef38, undef39, undef40, undef41, undef42, undef43, undef44, Undef variables: undef1, undef5, undef9, undef13, undef19, undef20, undef22, undef23, undef24, undef27, undef28, undef29, undef30, undef31, undef32, undef34, undef35, undef36, undef37, undef38, undef39, undef40, undef41, undef42, undef43, undef44, Abstraction variables: Exit nodes: Accepting locations: Asserts: ************************************************************* ******************************************************************************************* *********************** WORKING TRANSITION SYSTEM (DAG) *********************** ******************************************************************************************* Init Location: 0 Graph 0: Transitions: Variables: Graph 1: Transitions: undef5, arg2 -> -1 + arg2, arg3 -> arg2, rest remain the same}> Variables: arg1, arg2, arg3 Graph 2: Transitions: undef13, arg2 -> -1 + arg2, arg3 -> arg2, rest remain the same}> Variables: arg1, arg2, arg3 Graph 3: Transitions: -1 + arg1, arg2 -> arg1, arg3 -> undef27, arg4 -> undef28, rest remain the same}> Variables: arg1, arg2, arg3, arg4 Graph 4: Transitions: -1 + arg1, arg2 -> undef34, arg3 -> undef35, arg4 -> undef36, rest remain the same}> Variables: arg1, arg2, arg3, arg4 Graph 5: Transitions: undef37, arg2 -> undef38, arg3 -> undef39, arg4 -> undef40, rest remain the same}> Variables: arg1, arg2, arg3, arg4 Precedence: Graph 0 Graph 1 Graph 2 undef9, arg2 -> -1 + arg4, arg3 -> arg4, rest remain the same}> Graph 3 -1 + arg4, arg2 -> arg4, arg3 -> undef19, arg4 -> undef20, rest remain the same}> Graph 4 2, arg2 -> undef22, arg3 -> undef23, arg4 -> undef24, rest remain the same}> Graph 5 undef29, arg2 -> undef30, arg3 -> undef31, arg4 -> undef32, rest remain the same}> Map Locations to Subgraph: ( 0 , 0 ) ( 2 , 1 ) ( 3 , 2 ) ( 4 , 3 ) ( 5 , 4 ) ( 6 , 5 ) ******************************************************************************************* ******************************** CHECKING ASSERTIONS ******************************** ******************************************************************************************* Proving termination of subgraph 0 Proving termination of subgraph 1 Checking unfeasibility... Time used: 0.002269 Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000544s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001919s Trying to remove transition: undef5, arg2 -> -1 + arg2, arg3 -> arg2, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.006299s Time used: 0.006157 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.004869s Time used: 0.004615 LOG: SAT solveNonLinear - Elapsed time: 0.004869s Cost: 0; Total time: 0.004615 Termination implied by a set of invariant(s): Invariant at l2: arg3 <= 1 + arg1 + arg2 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef5, arg2 -> -1 + arg2, arg3 -> arg2, 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): undef5, arg2 -> -1 + arg2, arg3 -> arg2, rest remain the same}> Ranking function: arg1 + arg2 New Graphs: INVARIANTS: 2: arg3 <= 1 + arg1 + arg2 , Quasi-INVARIANTS to narrow Graph: 2: Proving termination of subgraph 2 Checking unfeasibility... Time used: 0.001468 Checking conditional termination of SCC {l3}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000428s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001356s Trying to remove transition: undef13, arg2 -> -1 + arg2, arg3 -> arg2, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.004731s Time used: 0.004643 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.005581s Time used: 0.005345 LOG: SAT solveNonLinear - Elapsed time: 0.005581s Cost: 0; Total time: 0.005345 Termination implied by a set of invariant(s): Invariant at l3: arg3 <= 1 + arg1 + arg2 [ 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 -> -1 + arg2, arg3 -> arg2, 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 -> -1 + arg2, arg3 -> arg2, rest remain the same}> Ranking function: arg1 + arg2 New Graphs: INVARIANTS: 3: arg3 <= 1 + arg1 + arg2 , Quasi-INVARIANTS to narrow Graph: 3: Proving termination of subgraph 3 Checking unfeasibility... Time used: 0.001226 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000336s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000906s Trying to remove transition: -1 + arg1, arg2 -> arg1, arg3 -> undef27, arg4 -> undef28, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.004057s Time used: 0.003988 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.004487s Time used: 0.004249 LOG: SAT solveNonLinear - Elapsed time: 0.004487s Cost: 0; Total time: 0.004249 Termination implied by a set of invariant(s): Invariant at l4: arg2 <= 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): -1 + arg1, arg2 -> arg1, arg3 -> undef27, arg4 -> undef28, 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 + arg1, arg2 -> arg1, arg3 -> undef27, arg4 -> undef28, rest remain the same}> Ranking function: arg1 New Graphs: INVARIANTS: 4: arg2 <= 1 + arg1 , Quasi-INVARIANTS to narrow Graph: 4: Proving termination of subgraph 4 Checking unfeasibility... Time used: 0.002202 Checking conditional termination of SCC {l5}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000487s Ranking function: arg1 New Graphs: Proving termination of subgraph 5 Checking unfeasibility... Time used: 0.001251 Checking conditional termination of SCC {l6}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000541s Ranking function: -1 + arg1 New Graphs: Program Terminates