YES Solver Timeout: 4 Global Timeout: 300 No parsing errors! Init Location: 0 Transitions: 0) /\ (undef1 > ~(1)), par{arg1 -> undef1, arg2 -> undef2, arg3 -> undef3, arg4 -> undef4}> ~(1)) /\ (undef5 > ~(1)), par{arg1 -> undef5, arg2 -> undef6, arg3 -> undef7, arg4 -> undef8}> 0) /\ (undef9 > ~(1)), par{arg1 -> undef9, arg2 -> undef10, arg3 -> undef11, arg4 -> undef12}> 0), par{arg1 -> undef13, arg2 -> undef14, arg3 -> undef15, arg4 -> undef16}> 0) /\ (undef17 > 0), par{arg1 -> undef17, arg2 -> undef18, arg3 -> undef19, arg4 -> undef20}> 0), par{arg1 -> undef21, arg2 -> undef22, arg3 -> undef23, arg4 -> undef24}> 0) /\ (undef25 > 0), par{arg1 -> undef25, arg2 -> undef26, arg3 -> undef27, arg4 -> undef28}> 0) /\ (undef30 > ~(1)) /\ ((undef29 - 3) <= arg1) /\ (arg1 > 0) /\ (undef29 > 3), par{arg1 -> undef29, arg2 -> undef30, arg3 -> undef31, arg4 -> (undef33 + 1)}> 0) /\ (undef35 > ~(1)) /\ ((undef34 - 1) <= arg1) /\ (arg1 > 0) /\ (undef34 > 1), par{arg1 -> undef34, arg2 -> undef35, arg3 -> undef36, arg4 -> (undef38 + 1)}> 0) /\ (arg1 > 1) /\ (undef39 > ~(1)), par{arg1 -> undef39, arg2 -> (arg2 - 1)}> 0) /\ (arg4 > 0) /\ (undef47 > 0) /\ ((undef43 - 2) <= arg1) /\ (arg1 > 2) /\ (undef43 > 3), par{arg1 -> undef43, arg2 -> (arg2 - 1), arg4 -> undef46}> 0) /\ (arg4 > 0) /\ (undef52 > 0) /\ ((undef48 - 2) <= arg1) /\ (arg1 > 2) /\ (undef48 > 3), par{arg1 -> undef48, arg2 -> (arg2 - 1), arg4 -> undef51}> 0) /\ (arg4 > 0) /\ (undef57 > 0) /\ ((undef53 - 3) <= arg1) /\ (arg1 > 2) /\ (undef53 > 5), par{arg1 -> undef53, arg2 -> (arg2 - 1), arg4 -> undef56}> 0) /\ (arg4 > 0) /\ (undef62 > 0) /\ ((undef58 - 3) <= arg1) /\ (arg1 > 2) /\ (undef58 > 5), par{arg1 -> undef58, arg2 -> (arg2 - 1), arg4 -> undef61}> ~(1)) /\ (undef64 <= arg1) /\ (arg1 > 0) /\ (undef63 > 0) /\ (undef64 > 0), par{arg1 -> undef63, arg2 -> undef64, arg3 -> 0, arg4 -> undef66}> 0) /\ (arg4 > 0) /\ (arg3 > ~(1)) /\ ((undef68 + 2) <= arg1) /\ (arg1 > 2) /\ (undef68 > 0), par{arg1 -> undef67, arg2 -> undef68, arg3 -> arg4, arg4 -> undef70}> 0) /\ (arg4 > 0) /\ (undef73 > 0) /\ (arg3 > ~(1)) /\ ((undef72 + 2) <= arg1) /\ (arg1 > 2) /\ (undef72 > 0), par{arg1 -> undef71, arg2 -> undef72, arg3 -> undef73, arg4 -> undef74}> undef75, arg2 -> undef76, arg3 -> undef77, arg4 -> undef78}> Fresh variables: undef1, undef2, undef3, undef4, undef5, undef6, undef7, undef8, undef9, undef10, undef11, undef12, undef13, undef14, undef15, undef16, undef17, undef18, undef19, undef20, undef21, undef22, undef23, undef24, undef25, undef26, undef27, undef28, undef29, undef30, undef31, undef33, undef34, undef35, undef36, undef38, undef39, undef43, undef46, undef47, undef48, undef51, undef52, undef53, undef56, undef57, undef58, undef61, undef62, undef63, undef64, undef66, undef67, undef68, undef70, undef71, undef72, undef73, undef74, undef75, undef76, undef77, undef78, Undef variables: undef1, undef2, undef3, undef4, undef5, undef6, undef7, undef8, undef9, undef10, undef11, undef12, undef13, undef14, undef15, undef16, undef17, undef18, undef19, undef20, undef21, undef22, undef23, undef24, undef25, undef26, undef27, undef28, undef29, undef30, undef31, undef33, undef34, undef35, undef36, undef38, undef39, undef43, undef46, undef47, undef48, undef51, undef52, undef53, undef56, undef57, undef58, undef61, undef62, undef63, undef64, undef66, undef67, undef68, undef70, undef71, undef72, undef73, undef74, undef75, undef76, undef77, undef78, Abstraction variables: Exit nodes: Accepting locations: Asserts: Preprocessed LLVMGraph Init Location: 0 Transitions: 0) /\ (undef1 > ~(1)), par{arg1 -> undef1, arg2 -> undef2, arg3 -> undef3, arg4 -> undef4}> 0) /\ (undef17 > 0) /\ (undef38 > 0) /\ (undef35 > ~(1)) /\ ((undef34 - 1) <= undef17) /\ (undef17 > 0) /\ (undef34 > 1), par{arg1 -> undef34, arg2 -> undef35, arg3 -> undef36, arg4 -> (undef38 + 1)}> 0) /\ (undef25 > 0) /\ (undef33 > 0) /\ (undef30 > ~(1)) /\ ((undef29 - 3) <= undef25) /\ (undef25 > 0) /\ (undef29 > 3), par{arg1 -> undef29, arg2 -> undef30, arg3 -> undef31, arg4 -> (undef33 + 1)}> ~(1)) /\ (undef64 <= undef75) /\ (undef75 > 0) /\ (undef63 > 0) /\ (undef64 > 0), par{arg1 -> undef63, arg2 -> undef64, arg3 -> 0, arg4 -> undef66}> 0) /\ (undef9 > ~(1)), par{arg1 -> undef9, arg2 -> undef10, arg3 -> undef11, arg4 -> undef12}> 0) /\ (arg1 > 1) /\ (undef39 > ~(1)), par{arg1 -> undef39, arg2 -> (arg2 - 1)}> 0) /\ (arg4 > 0) /\ (undef47 > 0) /\ ((undef43 - 2) <= arg1) /\ (arg1 > 2) /\ (undef43 > 3), par{arg1 -> undef43, arg2 -> (arg2 - 1), arg4 -> undef46}> 0) /\ (arg4 > 0) /\ (undef52 > 0) /\ ((undef48 - 2) <= arg1) /\ (arg1 > 2) /\ (undef48 > 3), par{arg1 -> undef48, arg2 -> (arg2 - 1), arg4 -> undef51}> 0) /\ (arg4 > 0) /\ (undef57 > 0) /\ ((undef53 - 3) <= arg1) /\ (arg1 > 2) /\ (undef53 > 5), par{arg1 -> undef53, arg2 -> (arg2 - 1), arg4 -> undef56}> 0) /\ (arg4 > 0) /\ (undef62 > 0) /\ ((undef58 - 3) <= arg1) /\ (arg1 > 2) /\ (undef58 > 5), par{arg1 -> undef58, arg2 -> (arg2 - 1), arg4 -> undef61}> 0) /\ (arg4 > 0) /\ (arg3 > ~(1)) /\ ((undef68 + 2) <= arg1) /\ (arg1 > 2) /\ (undef68 > 0), par{arg1 -> undef67, arg2 -> undef68, arg3 -> arg4, arg4 -> undef70}> 0) /\ (arg4 > 0) /\ (undef73 > 0) /\ (arg3 > ~(1)) /\ ((undef72 + 2) <= arg1) /\ (arg1 > 2) /\ (undef72 > 0), par{arg1 -> undef71, arg2 -> undef72, arg3 -> undef73, arg4 -> undef74}> Fresh variables: undef1, undef2, undef3, undef4, undef5, undef6, undef7, undef8, undef9, undef10, undef11, undef12, undef13, undef14, undef15, undef16, undef17, undef18, undef19, undef20, undef21, undef22, undef23, undef24, undef25, undef26, undef27, undef28, undef29, undef30, undef31, undef33, undef34, undef35, undef36, undef38, undef39, undef43, undef46, undef47, undef48, undef51, undef52, undef53, undef56, undef57, undef58, undef61, undef62, undef63, undef64, undef66, undef67, undef68, undef70, undef71, undef72, undef73, undef74, undef75, undef76, undef77, undef78, Undef variables: undef1, undef2, undef3, undef4, undef5, undef6, undef7, undef8, undef9, undef10, undef11, undef12, undef13, undef14, undef15, undef16, undef17, undef18, undef19, undef20, undef21, undef22, undef23, undef24, undef25, undef26, undef27, undef28, undef29, undef30, undef31, undef33, undef34, undef35, undef36, undef38, undef39, undef43, undef46, undef47, undef48, undef51, undef52, undef53, undef56, undef57, undef58, undef61, undef62, undef63, undef64, undef66, undef67, undef68, undef70, undef71, undef72, undef73, undef74, undef75, undef76, undef77, undef78, Abstraction variables: Exit nodes: Accepting locations: Asserts: ************************************************************* ******************************************************************************************* *********************** WORKING TRANSITION SYSTEM (DAG) *********************** ******************************************************************************************* Init Location: 0 Graph 0: Transitions: Variables: Graph 1: Transitions: undef39, arg2 -> -1 + arg2, rest remain the same}> undef43, arg2 -> -1 + arg2, arg4 -> undef46, rest remain the same}> undef48, arg2 -> -1 + arg2, arg4 -> undef51, rest remain the same}> undef53, arg2 -> -1 + arg2, arg4 -> undef56, rest remain the same}> undef58, arg2 -> -1 + arg2, arg4 -> undef61, rest remain the same}> Variables: arg1, arg2, arg4 Graph 2: Transitions: Variables: Graph 3: Transitions: undef9, arg2 -> undef10, arg3 -> undef11, arg4 -> undef12, rest remain the same}> Variables: arg1, arg2, arg3, arg4 Precedence: Graph 0 Graph 1 undef34, arg2 -> undef35, arg3 -> undef36, arg4 -> 1 + undef38, rest remain the same}> undef29, arg2 -> undef30, arg3 -> undef31, arg4 -> 1 + undef33, rest remain the same}> Graph 2 undef63, arg2 -> undef64, arg3 -> 0, arg4 -> undef66, rest remain the same}> undef67, arg2 -> undef68, arg3 -> arg4, arg4 -> undef70, rest remain the same}> undef71, arg2 -> undef72, arg3 -> undef73, arg4 -> undef74, rest remain the same}> Graph 3 undef1, arg2 -> undef2, arg3 -> undef3, arg4 -> undef4, rest remain the same}> Map Locations to Subgraph: ( 0 , 0 ) ( 2 , 3 ) ( 8 , 1 ) ( 9 , 2 ) ******************************************************************************************* ******************************** CHECKING ASSERTIONS ******************************** ******************************************************************************************* Proving termination of subgraph 0 Proving termination of subgraph 1 Checking unfeasibility... Time used: 0.011303 Checking conditional termination of SCC {l8}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002891s Ranking function: -1 + (1 / 5)*arg1 + (3 / 5)*arg2 New Graphs: Transitions: undef53, arg2 -> -1 + arg2, arg4 -> undef56, rest remain the same}> undef58, arg2 -> -1 + arg2, arg4 -> undef61, rest remain the same}> Variables: arg1, arg2, arg4 Checking conditional termination of SCC {l8}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001029s Ranking function: -1 + arg2 New Graphs: Proving termination of subgraph 2 Analyzing SCC {l9}... No cycles found. Proving termination of subgraph 3 Checking unfeasibility... Time used: 0.001192 Checking conditional termination of SCC {l2}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000530s Ranking function: -1 + arg1 New Graphs: Program Terminates