YES Solver Timeout: 4 Global Timeout: 300 No parsing errors! Init Location: 0 Transitions: 0) /\ (undef1 > 0) /\ (undef2 > ~(1)), par{arg1 -> undef1, arg2 -> undef2, arg3 -> undef3, arg4 -> undef4}> 0) /\ (arg2 > ~(1)) /\ (undef5 > 0) /\ (undef6 > ~(1)), par{arg1 -> undef5, arg2 -> undef6, arg3 -> 2, arg4 -> undef8}> 0), par{arg1 -> undef9, arg2 -> undef10, arg3 -> undef11, arg4 -> undef12}> 0) /\ (undef13 > 0), par{arg1 -> undef13, arg2 -> undef14, arg3 -> undef15, arg4 -> undef16}> 0), par{arg1 -> undef17, arg2 -> undef18, arg3 -> undef19, arg4 -> undef20}> 0) /\ (undef21 > 0), par{arg1 -> undef21, arg2 -> undef22, arg3 -> undef23, arg4 -> undef24}> 0) /\ (undef26 > ~(1)) /\ ((undef25 - 3) <= arg1) /\ (arg1 > 0) /\ (undef25 > 3), par{arg1 -> undef25, arg2 -> undef26, arg3 -> undef27, arg4 -> (undef29 + 1)}> 0) /\ (undef31 > ~(1)) /\ ((undef30 - 1) <= arg1) /\ (arg1 > 0) /\ (undef30 > 1), par{arg1 -> undef30, arg2 -> undef31, arg3 -> undef32, arg4 -> (undef34 + 1)}> 0) /\ (arg1 > 1) /\ (undef35 > ~(1)), par{arg1 -> undef35, arg2 -> (arg2 - 1)}> 0) /\ (arg4 > 0) /\ (undef43 > 0) /\ ((undef39 - 2) <= arg1) /\ (arg1 > 2) /\ (undef39 > 3), par{arg1 -> undef39, arg2 -> (arg2 - 1), arg4 -> undef42}> 0) /\ (arg4 > 0) /\ (undef48 > 0) /\ ((undef44 - 2) <= arg1) /\ (arg1 > 2) /\ (undef44 > 3), par{arg1 -> undef44, arg2 -> (arg2 - 1), arg4 -> undef47}> 0) /\ (arg4 > 0) /\ (undef53 > 0) /\ ((undef49 - 3) <= arg1) /\ (arg1 > 2) /\ (undef49 > 5), par{arg1 -> undef49, arg2 -> (arg2 - 1), arg4 -> undef52}> 0) /\ (arg4 > 0) /\ (undef58 > 0) /\ ((undef54 - 3) <= arg1) /\ (arg1 > 2) /\ (undef54 > 5), par{arg1 -> undef54, arg2 -> (arg2 - 1), arg4 -> undef57}> ~(1)) /\ (undef60 <= arg1) /\ (arg1 > 0) /\ (undef59 > 0) /\ (undef60 > 0), par{arg1 -> undef59, arg2 -> undef60, arg3 -> 0, arg4 -> undef62}> 0) /\ (arg4 > 0) /\ (arg3 > ~(1)) /\ ((undef64 + 2) <= arg1) /\ (arg1 > 2) /\ (undef64 > 0), par{arg1 -> undef63, arg2 -> undef64, arg3 -> arg4, arg4 -> undef66}> 0) /\ (arg4 > 0) /\ (undef69 > 0) /\ (arg3 > ~(1)) /\ ((undef68 + 2) <= arg1) /\ (arg1 > 2) /\ (undef68 > 0), par{arg1 -> undef67, arg2 -> undef68, arg3 -> undef69, arg4 -> undef70}> 0) /\ (arg2 > ~(1)) /\ (undef71 > ~(1)), par{arg1 -> undef71, arg2 -> undef72, arg4 -> undef74}> ~(1)) /\ (arg3 > ~(1)) /\ (undef79 < 43) /\ (undef79 > ~(1)) /\ ((undef75 + 1) <= arg1) /\ (arg1 > 0) /\ (undef75 > ~(1)), par{arg1 -> undef75, arg3 -> (arg3 + 1), arg4 -> undef78}> ~(1)) /\ (undef84 > 42) /\ (arg3 > ~(1)) /\ ((undef80 + 1) <= arg1) /\ (arg1 > 0) /\ (undef80 > ~(1)), par{arg1 -> undef80, arg3 -> (arg3 + 1), arg4 -> undef83}> undef85, arg2 -> undef86, arg3 -> undef87, arg4 -> undef88}> Fresh variables: undef1, undef2, undef3, undef4, undef5, undef6, undef8, undef9, undef10, undef11, undef12, undef13, undef14, undef15, undef16, undef17, undef18, undef19, undef20, undef21, undef22, undef23, undef24, undef25, undef26, undef27, undef29, undef30, undef31, undef32, undef34, undef35, undef39, undef42, undef43, undef44, undef47, undef48, undef49, undef52, undef53, undef54, undef57, undef58, undef59, undef60, undef62, undef63, undef64, undef66, undef67, undef68, undef69, undef70, undef71, undef72, undef74, undef75, undef78, undef79, undef80, undef83, undef84, undef85, undef86, undef87, undef88, Undef variables: undef1, undef2, undef3, undef4, undef5, undef6, undef8, undef9, undef10, undef11, undef12, undef13, undef14, undef15, undef16, undef17, undef18, undef19, undef20, undef21, undef22, undef23, undef24, undef25, undef26, undef27, undef29, undef30, undef31, undef32, undef34, undef35, undef39, undef42, undef43, undef44, undef47, undef48, undef49, undef52, undef53, undef54, undef57, undef58, undef59, undef60, undef62, undef63, undef64, undef66, undef67, undef68, undef69, undef70, undef71, undef72, undef74, undef75, undef78, undef79, undef80, undef83, undef84, undef85, undef86, undef87, undef88, Abstraction variables: Exit nodes: Accepting locations: Asserts: Preprocessed LLVMGraph Init Location: 0 Transitions: 0) /\ (undef1 > 0) /\ (undef2 > ~(1)) /\ (undef71 <= undef2) /\ (undef1 > 0) /\ (undef2 > ~(1)) /\ (undef71 > ~(1)), par{arg1 -> undef71, arg2 -> undef72, arg3 -> undef3, arg4 -> undef74}> 0) /\ (undef13 > 0) /\ (undef34 > 0) /\ (undef31 > ~(1)) /\ ((undef30 - 1) <= undef13) /\ (undef13 > 0) /\ (undef30 > 1), par{arg1 -> undef30, arg2 -> undef31, arg3 -> undef32, arg4 -> (undef34 + 1)}> 0) /\ (undef21 > 0) /\ (undef29 > 0) /\ (undef26 > ~(1)) /\ ((undef25 - 3) <= undef21) /\ (undef21 > 0) /\ (undef25 > 3), par{arg1 -> undef25, arg2 -> undef26, arg3 -> undef27, arg4 -> (undef29 + 1)}> ~(1)) /\ (undef60 <= undef85) /\ (undef85 > 0) /\ (undef59 > 0) /\ (undef60 > 0), par{arg1 -> undef59, arg2 -> undef60, arg3 -> 0, arg4 -> undef62}> 0) /\ (arg1 > 1) /\ (undef35 > ~(1)), par{arg1 -> undef35, arg2 -> (arg2 - 1)}> 0) /\ (arg4 > 0) /\ (undef43 > 0) /\ ((undef39 - 2) <= arg1) /\ (arg1 > 2) /\ (undef39 > 3), par{arg1 -> undef39, arg2 -> (arg2 - 1), arg4 -> undef42}> 0) /\ (arg4 > 0) /\ (undef48 > 0) /\ ((undef44 - 2) <= arg1) /\ (arg1 > 2) /\ (undef44 > 3), par{arg1 -> undef44, arg2 -> (arg2 - 1), arg4 -> undef47}> 0) /\ (arg4 > 0) /\ (undef53 > 0) /\ ((undef49 - 3) <= arg1) /\ (arg1 > 2) /\ (undef49 > 5), par{arg1 -> undef49, arg2 -> (arg2 - 1), arg4 -> undef52}> 0) /\ (arg4 > 0) /\ (undef58 > 0) /\ ((undef54 - 3) <= arg1) /\ (arg1 > 2) /\ (undef54 > 5), par{arg1 -> undef54, arg2 -> (arg2 - 1), arg4 -> undef57}> 0) /\ (arg4 > 0) /\ (arg3 > ~(1)) /\ ((undef64 + 2) <= arg1) /\ (arg1 > 2) /\ (undef64 > 0), par{arg1 -> undef63, arg2 -> undef64, arg3 -> arg4, arg4 -> undef66}> 0) /\ (arg4 > 0) /\ (undef69 > 0) /\ (arg3 > ~(1)) /\ ((undef68 + 2) <= arg1) /\ (arg1 > 2) /\ (undef68 > 0), par{arg1 -> undef67, arg2 -> undef68, arg3 -> undef69, arg4 -> undef70}> ~(1)) /\ (arg3 > ~(1)) /\ (undef79 < 43) /\ (undef79 > ~(1)) /\ ((undef75 + 1) <= arg1) /\ (arg1 > 0) /\ (undef75 > ~(1)), par{arg1 -> undef75, arg3 -> (arg3 + 1), arg4 -> undef78}> ~(1)) /\ (undef84 > 42) /\ (arg3 > ~(1)) /\ ((undef80 + 1) <= arg1) /\ (arg1 > 0) /\ (undef80 > ~(1)), par{arg1 -> undef80, arg3 -> (arg3 + 1), arg4 -> undef83}> Fresh variables: undef1, undef2, undef3, undef4, undef5, undef6, undef8, undef9, undef10, undef11, undef12, undef13, undef14, undef15, undef16, undef17, undef18, undef19, undef20, undef21, undef22, undef23, undef24, undef25, undef26, undef27, undef29, undef30, undef31, undef32, undef34, undef35, undef39, undef42, undef43, undef44, undef47, undef48, undef49, undef52, undef53, undef54, undef57, undef58, undef59, undef60, undef62, undef63, undef64, undef66, undef67, undef68, undef69, undef70, undef71, undef72, undef74, undef75, undef78, undef79, undef80, undef83, undef84, undef85, undef86, undef87, undef88, Undef variables: undef1, undef2, undef3, undef4, undef5, undef6, undef8, undef9, undef10, undef11, undef12, undef13, undef14, undef15, undef16, undef17, undef18, undef19, undef20, undef21, undef22, undef23, undef24, undef25, undef26, undef27, undef29, undef30, undef31, undef32, undef34, undef35, undef39, undef42, undef43, undef44, undef47, undef48, undef49, undef52, undef53, undef54, undef57, undef58, undef59, undef60, undef62, undef63, undef64, undef66, undef67, undef68, undef69, undef70, undef71, undef72, undef74, undef75, undef78, undef79, undef80, undef83, undef84, undef85, undef86, undef87, undef88, Abstraction variables: Exit nodes: Accepting locations: Asserts: ************************************************************* ******************************************************************************************* *********************** WORKING TRANSITION SYSTEM (DAG) *********************** ******************************************************************************************* Init Location: 0 Graph 0: Transitions: Variables: Graph 1: Transitions: undef35, arg2 -> -1 + arg2, rest remain the same}> undef39, arg2 -> -1 + arg2, arg4 -> undef42, rest remain the same}> undef44, arg2 -> -1 + arg2, arg4 -> undef47, rest remain the same}> undef49, arg2 -> -1 + arg2, arg4 -> undef52, rest remain the same}> undef54, arg2 -> -1 + arg2, arg4 -> undef57, rest remain the same}> Variables: arg1, arg2, arg4 Graph 2: Transitions: Variables: Graph 3: Transitions: undef75, arg3 -> 1 + arg3, arg4 -> undef78, rest remain the same}> undef80, arg3 -> 1 + arg3, arg4 -> undef83, rest remain the same}> Variables: arg1, arg2, arg3, arg4 Precedence: Graph 0 Graph 1 undef30, arg2 -> undef31, arg3 -> undef32, arg4 -> 1 + undef34, rest remain the same}> undef25, arg2 -> undef26, arg3 -> undef27, arg4 -> 1 + undef29, rest remain the same}> Graph 2 undef59, arg2 -> undef60, arg3 -> 0, arg4 -> undef62, rest remain the same}> undef63, arg2 -> undef64, arg3 -> arg4, arg4 -> undef66, rest remain the same}> undef67, arg2 -> undef68, arg3 -> undef69, arg4 -> undef70, rest remain the same}> Graph 3 undef71, arg2 -> undef72, arg3 -> undef3, arg4 -> undef74, rest remain the same}> Map Locations to Subgraph: ( 0 , 0 ) ( 8 , 1 ) ( 9 , 2 ) ( 10 , 3 ) ******************************************************************************************* ******************************** CHECKING ASSERTIONS ******************************** ******************************************************************************************* Proving termination of subgraph 0 Proving termination of subgraph 1 Checking unfeasibility... Time used: 0.011112 Checking conditional termination of SCC {l8}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002857s Ranking function: -1 + (1 / 5)*arg1 + (3 / 5)*arg2 New Graphs: Transitions: undef49, arg2 -> -1 + arg2, arg4 -> undef52, rest remain the same}> undef54, arg2 -> -1 + arg2, arg4 -> undef57, rest remain the same}> Variables: arg1, arg2, arg4 Checking conditional termination of SCC {l8}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001032s 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.002781 Checking conditional termination of SCC {l10}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001173s Ranking function: -1 + arg1 New Graphs: Program Terminates