YES Solver Timeout: 4 Global Timeout: 300 No parsing errors! Init Location: 0 Transitions: ~(1)) /\ (arg2 > 0) /\ (undef1 <= arg1) /\ (arg1 > 0) /\ (undef1 > 0) /\ (undef2 > 3), par{arg1 -> undef1, arg2 -> undef2, arg3 -> undef3, arg4 -> undef4, arg5 -> undef5}> 0) /\ (arg2 > 3) /\ (undef7 > 0) /\ (undef8 > 3) /\ ((arg5 + 5) <= arg2) /\ ((arg4 + 5) <= arg2), par{arg1 -> undef7, arg2 -> undef8}> ~(1)) /\ (arg2 > 0) /\ (arg1 > 0), par{arg1 -> undef12, arg3 -> 1, arg4 -> undef15, arg5 -> undef16}> ~(1)) /\ (arg1 > 1) /\ (arg3 > 0) /\ (arg3 < arg2) /\ (undef19 > ~(1)), par{arg2 -> 0, arg3 -> undef19, arg4 -> arg2, arg5 -> (arg3 + 1)}> arg2) /\ (arg1 > 1) /\ (arg3 > 0) /\ (arg5 > 1) /\ ((arg1 - 1) < arg1), par{arg1 -> (arg1 - 1), arg2 -> arg4, arg3 -> arg5, arg4 -> undef25, arg5 -> undef26}> arg2) /\ (arg1 > 1) /\ (arg3 > 0) /\ (arg5 > 1) /\ ((arg1 - 1) < arg1), par{arg2 -> (arg2 + 1), arg5 -> undef31}> 0) /\ (arg3 > 1) /\ ((undef32 - 1) <= arg1) /\ ((undef32 + 2) <= arg2) /\ ((undef33 + 3) <= arg2) /\ (arg1 > 0) /\ (arg2 > 3) /\ (undef32 > 1) /\ (undef33 > 0) /\ ((arg5 + 5) <= arg2) /\ ((arg4 + 5) <= arg2), par{arg1 -> undef32, arg2 -> undef33, arg4 -> undef35, arg5 -> undef36}> 1) /\ ((undef39 + 3) <= arg2) /\ (arg1 > 0) /\ (arg2 > 2) /\ (undef38 > 0) /\ (undef39 > ~(1)), par{arg1 -> undef38, arg2 -> undef39, arg4 -> undef41, arg5 -> undef42}> 1) /\ (arg1 > 0) /\ (arg2 > 2) /\ (undef43 > 0) /\ (undef44 > ~(1)), par{arg1 -> undef43, arg2 -> undef44, arg4 -> undef46, arg5 -> undef47}> 0) /\ (arg2 > 2) /\ (undef48 > 2) /\ (undef49 > ~(1)), par{arg1 -> undef48, arg2 -> undef49, arg4 -> undef51, arg5 -> undef52}> undef53, arg2 -> undef54, arg3 -> undef55, arg4 -> undef56, arg5 -> undef57}> Fresh variables: undef1, undef2, undef3, undef4, undef5, undef6, undef7, undef8, undef12, undef15, undef16, undef19, undef25, undef26, undef31, undef32, undef33, undef35, undef36, undef37, undef38, undef39, undef41, undef42, undef43, undef44, undef46, undef47, undef48, undef49, undef51, undef52, undef53, undef54, undef55, undef56, undef57, Undef variables: undef1, undef2, undef3, undef4, undef5, undef6, undef7, undef8, undef12, undef15, undef16, undef19, undef25, undef26, undef31, undef32, undef33, undef35, undef36, undef37, undef38, undef39, undef41, undef42, undef43, undef44, undef46, undef47, undef48, undef49, undef51, undef52, undef53, undef54, undef55, undef56, undef57, Abstraction variables: Exit nodes: Accepting locations: Asserts: Preprocessed LLVMGraph Init Location: 0 Transitions: ~(1)) /\ (undef54 > 0) /\ (undef1 <= undef53) /\ (undef53 > 0) /\ (undef1 > 0) /\ (undef2 > 3) /\ (undef37 > 0) /\ (undef3 > 1) /\ ((undef32 - 1) <= undef1) /\ ((undef32 + 2) <= undef2) /\ ((undef33 + 3) <= undef2) /\ (undef1 > 0) /\ (undef2 > 3) /\ (undef32 > 1) /\ (undef33 > 0) /\ ((undef5 + 5) <= undef2) /\ ((undef4 + 5) <= undef2), par{arg1 -> undef32, arg2 -> undef33, arg3 -> undef3, arg4 -> undef35, arg5 -> undef36}> ~(1)) /\ (undef54 > 0) /\ (undef53 > 0) /\ (undef54 > ~(1)) /\ (undef12 > 1) /\ (1 > 0) /\ (1 < undef54) /\ (undef19 > ~(1)), par{arg1 -> undef12, arg2 -> 0, arg3 -> undef19, arg4 -> undef54, arg5 -> (1 + 1)}> arg2) /\ (arg1 > 1) /\ (arg3 > 0) /\ (arg5 > 1) /\ ((arg1 - 1) < arg1) /\ (arg4 > ~(1)) /\ ((arg1 - 1) > 1) /\ (arg5 > 0) /\ (arg5 < arg4) /\ (undef19 > ~(1)), par{arg1 -> (arg1 - 1), arg2 -> 0, arg3 -> undef19, arg4 -> arg4, arg5 -> (arg5 + 1)}> arg2) /\ (arg1 > 1) /\ (arg3 > 0) /\ (arg5 > 1) /\ ((arg1 - 1) < arg1), par{arg2 -> (arg2 + 1), arg5 -> undef31}> 1) /\ ((undef39 + 3) <= arg2) /\ (arg1 > 0) /\ (arg2 > 2) /\ (undef38 > 0) /\ (undef39 > ~(1)), par{arg1 -> undef38, arg2 -> undef39, arg4 -> undef41, arg5 -> undef42}> 1) /\ (arg1 > 0) /\ (arg2 > 2) /\ (undef43 > 0) /\ (undef44 > ~(1)), par{arg1 -> undef43, arg2 -> undef44, arg4 -> undef46, arg5 -> undef47}> 0) /\ (arg2 > 2) /\ (undef48 > 2) /\ (undef49 > ~(1)), par{arg1 -> undef48, arg2 -> undef49, arg4 -> undef51, arg5 -> undef52}> Fresh variables: undef1, undef2, undef3, undef4, undef5, undef6, undef7, undef8, undef12, undef15, undef16, undef19, undef25, undef26, undef31, undef32, undef33, undef35, undef36, undef37, undef38, undef39, undef41, undef42, undef43, undef44, undef46, undef47, undef48, undef49, undef51, undef52, undef53, undef54, undef55, undef56, undef57, Undef variables: undef1, undef2, undef3, undef4, undef5, undef6, undef7, undef8, undef12, undef15, undef16, undef19, undef25, undef26, undef31, undef32, undef33, undef35, undef36, undef37, undef38, undef39, undef41, undef42, undef43, undef44, undef46, undef47, undef48, undef49, undef51, undef52, undef53, undef54, undef55, undef56, undef57, Abstraction variables: Exit nodes: Accepting locations: Asserts: ************************************************************* ******************************************************************************************* *********************** WORKING TRANSITION SYSTEM (DAG) *********************** ******************************************************************************************* Init Location: 0 Graph 0: Transitions: Variables: Graph 1: Transitions: -1 + arg1, arg2 -> 0, arg3 -> undef19, arg5 -> 1 + arg5, rest remain the same}> 1 + arg2, arg5 -> undef31, rest remain the same}> Variables: arg1, arg2, arg3, arg4, arg5 Graph 2: Transitions: undef38, arg2 -> undef39, arg4 -> undef41, arg5 -> undef42, rest remain the same}> undef43, arg2 -> undef44, arg4 -> undef46, arg5 -> undef47, rest remain the same}> undef48, arg2 -> undef49, arg4 -> undef51, arg5 -> undef52, rest remain the same}> Variables: arg1, arg2, arg3, arg4, arg5 Precedence: Graph 0 Graph 1 undef12, arg2 -> 0, arg3 -> undef19, arg4 -> undef54, arg5 -> 2, rest remain the same}> Graph 2 undef32, arg2 -> undef33, arg3 -> undef3, arg4 -> undef35, arg5 -> undef36, rest remain the same}> Map Locations to Subgraph: ( 0 , 0 ) ( 5 , 1 ) ( 6 , 2 ) ******************************************************************************************* ******************************** CHECKING ASSERTIONS ******************************** ******************************************************************************************* Proving termination of subgraph 0 Proving termination of subgraph 1 Checking unfeasibility... Time used: 0.006994 Checking conditional termination of SCC {l5}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001215s Ranking function: -12 + 3*arg1 + arg4 New Graphs: Transitions: 1 + arg2, arg5 -> undef31, rest remain the same}> Variables: arg1, arg2, arg3, arg5 Checking conditional termination of SCC {l5}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000482s Ranking function: -1 - arg2 + arg3 New Graphs: Proving termination of subgraph 2 Checking unfeasibility... Time used: 0.007838 Checking conditional termination of SCC {l6}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001833s Ranking function: (~(23) / 2) + (1 / 2)*arg2 + 5*arg3 New Graphs: Transitions: undef48, arg2 -> undef49, arg4 -> undef51, arg5 -> undef52, rest remain the same}> Variables: arg1, arg2, arg4, arg5 Checking conditional termination of SCC {l6}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000595s Ranking function: (~(3) / 2) + (1 / 2)*arg2 New Graphs: Program Terminates