YES

Solver Timeout: 4
Global Timeout: 300
No parsing errors!
Init Location: 0
Transitions:
<l0, l7, true>
<l1, l2, (undef5 > ~(1)) /\ (arg2 > 0) /\ (undef1 <= arg1) /\ ((undef2 - 7) <= arg1) /\ ((undef3 - 5) <= arg1) /\ (arg1 > 0) /\ (undef1 > 0) /\ (undef2 > 7) /\ (undef3 > 5), par{arg1 -> undef1, arg2 -> undef2, arg3 -> undef3, arg4 -> 0}>
<l1, l2, (undef10 > ~(1)) /\ (arg2 > 0) /\ (undef6 <= arg1) /\ (arg1 > 0) /\ (undef6 > 0) /\ (undef7 > 8) /\ (undef8 > 6), par{arg1 -> undef6, arg2 -> undef7, arg3 -> undef8, arg4 -> undef9}>
<l2, l3, (undef15 > ~(1)) /\ (undef16 > 1) /\ (undef11 <= arg1) /\ ((undef11 + 7) <= arg2) /\ ((undef11 + 5) <= arg3) /\ (arg1 > 0) /\ (arg2 > 7) /\ (arg3 > 5) /\ (undef11 > 0), par{arg1 -> undef11, arg2 -> undef12, arg3 -> undef13, arg4 -> undef14}>
<l2, l3, (undef21 > arg4) /\ (arg4 > 0) /\ (undef22 > arg4) /\ (undef23 > arg4) /\ (undef24 > 1) /\ (undef25 > ~(1)) /\ (undef17 <= arg1) /\ ((undef17 + 6) <= arg2) /\ ((undef17 + 4) <= arg3) /\ (arg1 > 0) /\ (arg2 > 6) /\ (arg3 > 4) /\ (undef17 > 0), par{arg1 -> undef17, arg2 -> undef18, arg3 -> undef19, arg4 -> undef20}>
<l1, l3, (undef30 > ~(1)) /\ (arg2 > 1) /\ (undef31 > ~(1)) /\ (undef26 <= arg1) /\ (arg1 > 0) /\ (undef26 > 0), par{arg1 -> undef26, arg2 -> undef27, arg3 -> undef28, arg4 -> undef29}>
<l2, l4, (undef36 > arg4) /\ (arg4 > 0) /\ (undef37 > arg4) /\ (undef38 > arg4) /\ (undef39 > 1) /\ (undef40 > ~(1)) /\ (undef32 <= arg1) /\ ((undef32 + 6) <= arg2) /\ ((undef32 + 4) <= arg3) /\ (arg1 > 0) /\ (arg2 > 6) /\ (arg3 > 4) /\ (undef32 > 0) /\ (undef33 > 6), par{arg1 -> undef32, arg2 -> undef33, arg3 -> undef34, arg4 -> undef35}>
<l2, l4, (undef45 > ~(1)) /\ (undef46 > 1) /\ (undef41 <= arg1) /\ ((undef41 + 7) <= arg2) /\ ((undef41 + 5) <= arg3) /\ ((undef42 - 5) <= arg1) /\ ((undef42 + 2) <= arg2) /\ (undef42 <= arg3) /\ (arg1 > 0) /\ (arg2 > 7) /\ (arg3 > 5) /\ (undef41 > 0) /\ (undef42 > 5), par{arg1 -> undef41, arg2 -> undef42, arg3 -> undef43, arg4 -> undef44}>
<l2, l4, (undef51 > ~(1)) /\ (undef52 > 1) /\ (undef47 <= arg1) /\ ((undef47 + 7) <= arg2) /\ ((undef47 + 5) <= arg3) /\ (arg1 > 0) /\ (arg2 > 7) /\ (arg3 > 5) /\ (undef47 > 0) /\ (undef48 > 6), par{arg1 -> undef47, arg2 -> undef48, arg3 -> undef49, arg4 -> undef50}>
<l1, l4, (undef57 > ~(1)) /\ (arg2 > 1) /\ (undef58 > ~(1)) /\ (undef53 <= arg1) /\ (arg1 > 0) /\ (undef53 > 0) /\ (undef54 > 6), par{arg1 -> undef53, arg2 -> undef54, arg3 -> undef55, arg4 -> undef56}>
<l2, l4, (undef63 > arg4) /\ (arg4 > 0) /\ (undef64 > arg4) /\ (undef65 > arg4) /\ (undef66 > 1) /\ (undef67 > ~(1)) /\ (undef59 <= arg1) /\ ((undef59 + 6) <= arg2) /\ ((undef59 + 4) <= arg3) /\ ((undef60 - 5) <= arg1) /\ ((undef60 + 1) <= arg2) /\ ((undef60 - 1) <= arg3) /\ (arg1 > 0) /\ (arg2 > 6) /\ (arg3 > 4) /\ (undef59 > 0) /\ (undef60 > 5), par{arg1 -> undef59, arg2 -> undef60, arg3 -> undef61, arg4 -> undef62}>
<l1, l4, (undef72 > ~(1)) /\ (arg2 > 1) /\ (undef73 > ~(1)) /\ (undef68 <= arg1) /\ ((undef69 - 5) <= arg1) /\ (arg1 > 0) /\ (undef68 > 0) /\ (undef69 > 5), par{arg1 -> undef68, arg2 -> undef69, arg3 -> undef70, arg4 -> undef71}>
<l1, l5, (undef74 > ~(1)) /\ (arg2 > 0) /\ (arg1 > 0), par{arg1 -> undef74, arg2 -> 1, arg3 -> undef76, arg4 -> undef77}>
<l2, l5, (undef82 > arg4) /\ (arg4 > 0) /\ (undef83 > arg4) /\ (undef84 > arg4) /\ (undef85 > 1) /\ (undef78 > ~(1)) /\ (arg1 > 0) /\ (arg2 > 6) /\ (arg3 > 4), par{arg1 -> undef78, arg2 -> 2, arg3 -> undef80, arg4 -> undef81}>
<l2, l5, (undef86 > ~(1)) /\ (undef90 > 1) /\ (arg1 > 0) /\ (arg2 > 7) /\ (arg3 > 5), par{arg1 -> undef86, arg2 -> 2, arg3 -> undef88, arg4 -> undef89}>
<l1, l5, (undef95 > ~(1)) /\ (arg2 > 1) /\ (undef91 > ~(1)) /\ (arg1 > 0), par{arg1 -> undef91, arg2 -> 2, arg3 -> undef93, arg4 -> undef94}>
<l5, l5, ((arg1 - 1) < arg1) /\ (arg2 > 0) /\ (arg1 > 1), par{arg1 -> (arg1 - 1), arg3 -> undef98, arg4 -> undef99}>
<l3, l6, ((undef100 - 3) <= arg1) /\ (undef104 > 1) /\ ((undef101 - 1) <= arg1) /\ (arg1 > 0) /\ (undef100 > 3) /\ (undef101 > 1), par{arg1 -> undef100, arg2 -> undef101, arg3 -> undef102, arg4 -> undef103}>
<l4, l6, (undef105 <= arg2) /\ (undef109 > 1) /\ ((undef106 + 2) <= arg2) /\ (arg1 > 0) /\ (arg2 > 4) /\ (undef105 > 4) /\ (undef106 > 2), par{arg1 -> undef105, arg2 -> undef106, arg3 -> undef107, arg4 -> undef108}>
<l6, l6, ((undef110 + 2) <= arg1) /\ (undef110 <= arg2) /\ ((undef111 + 3) <= arg1) /\ ((undef111 + 1) <= arg2) /\ (arg1 > 2) /\ (arg2 > 0) /\ (undef110 > 0) /\ (undef111 > ~(1)), par{arg1 -> undef110, arg2 -> undef111, arg3 -> undef112, arg4 -> undef113}>
<l7, l1, true, par{arg1 -> undef114, arg2 -> undef115, arg3 -> undef116, arg4 -> undef117}>

Fresh variables:
undef1, undef2, undef3, 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, undef32, undef33, undef34, undef35, undef36, undef37, undef38, undef39, undef40, undef41, undef42, undef43, undef44, undef45, undef46, undef47, undef48, undef49, undef50, undef51, undef52, undef53, undef54, undef55, undef56, undef57, undef58, undef59, undef60, undef61, undef62, undef63, undef64, undef65, undef66, undef67, undef68, undef69, undef70, undef71, undef72, undef73, undef74, undef76, undef77, undef78, undef80, undef81, undef82, undef83, undef84, undef85, undef86, undef88, undef89, undef90, undef91, undef93, undef94, undef95, undef98, undef99, undef100, undef101, undef102, undef103, undef104, undef105, undef106, undef107, undef108, undef109, undef110, undef111, undef112, undef113, undef114, undef115, undef116, undef117, 

Undef variables:
undef1, undef2, undef3, 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, undef32, undef33, undef34, undef35, undef36, undef37, undef38, undef39, undef40, undef41, undef42, undef43, undef44, undef45, undef46, undef47, undef48, undef49, undef50, undef51, undef52, undef53, undef54, undef55, undef56, undef57, undef58, undef59, undef60, undef61, undef62, undef63, undef64, undef65, undef66, undef67, undef68, undef69, undef70, undef71, undef72, undef73, undef74, undef76, undef77, undef78, undef80, undef81, undef82, undef83, undef84, undef85, undef86, undef88, undef89, undef90, undef91, undef93, undef94, undef95, undef98, undef99, undef100, undef101, undef102, undef103, undef104, undef105, undef106, undef107, undef108, undef109, undef110, undef111, undef112, undef113, undef114, undef115, undef116, undef117, 

Abstraction variables:

Exit nodes:

Accepting locations:

Asserts:

Preprocessed LLVMGraph
Init Location: 0
Transitions:
<l0, l2, (undef5 > ~(1)) /\ (undef115 > 0) /\ (undef1 <= undef114) /\ ((undef2 - 7) <= undef114) /\ ((undef3 - 5) <= undef114) /\ (undef114 > 0) /\ (undef1 > 0) /\ (undef2 > 7) /\ (undef3 > 5), par{arg1 -> undef1, arg2 -> undef2, arg3 -> undef3, arg4 -> 0}>
<l0, l2, (undef10 > ~(1)) /\ (undef115 > 0) /\ (undef6 <= undef114) /\ (undef114 > 0) /\ (undef6 > 0) /\ (undef7 > 8) /\ (undef8 > 6), par{arg1 -> undef6, arg2 -> undef7, arg3 -> undef8, arg4 -> undef9}>
<l0, l6, (undef30 > ~(1)) /\ (undef115 > 1) /\ (undef31 > ~(1)) /\ (undef26 <= undef114) /\ (undef114 > 0) /\ (undef26 > 0) /\ ((undef100 - 3) <= undef26) /\ (undef104 > 1) /\ ((undef101 - 1) <= undef26) /\ (undef26 > 0) /\ (undef100 > 3) /\ (undef101 > 1), par{arg1 -> undef100, arg2 -> undef101, arg3 -> undef102, arg4 -> undef103}>
<l0, l6, (undef57 > ~(1)) /\ (undef115 > 1) /\ (undef58 > ~(1)) /\ (undef53 <= undef114) /\ (undef114 > 0) /\ (undef53 > 0) /\ (undef54 > 6) /\ (undef105 <= undef54) /\ (undef109 > 1) /\ ((undef106 + 2) <= undef54) /\ (undef53 > 0) /\ (undef54 > 4) /\ (undef105 > 4) /\ (undef106 > 2), par{arg1 -> undef105, arg2 -> undef106, arg3 -> undef107, arg4 -> undef108}>
<l0, l6, (undef72 > ~(1)) /\ (undef115 > 1) /\ (undef73 > ~(1)) /\ (undef68 <= undef114) /\ ((undef69 - 5) <= undef114) /\ (undef114 > 0) /\ (undef68 > 0) /\ (undef69 > 5) /\ (undef105 <= undef69) /\ (undef109 > 1) /\ ((undef106 + 2) <= undef69) /\ (undef68 > 0) /\ (undef69 > 4) /\ (undef105 > 4) /\ (undef106 > 2), par{arg1 -> undef105, arg2 -> undef106, arg3 -> undef107, arg4 -> undef108}>
<l0, l5, (undef74 > ~(1)) /\ (undef115 > 0) /\ (undef114 > 0), par{arg1 -> undef74, arg2 -> 1, arg3 -> undef76, arg4 -> undef77}>
<l0, l5, (undef95 > ~(1)) /\ (undef115 > 1) /\ (undef91 > ~(1)) /\ (undef114 > 0), par{arg1 -> undef91, arg2 -> 2, arg3 -> undef93, arg4 -> undef94}>
<l2, l6, (undef15 > ~(1)) /\ (undef16 > 1) /\ (undef11 <= arg1) /\ ((undef11 + 7) <= arg2) /\ ((undef11 + 5) <= arg3) /\ (arg1 > 0) /\ (arg2 > 7) /\ (arg3 > 5) /\ (undef11 > 0) /\ ((undef100 - 3) <= undef11) /\ (undef104 > 1) /\ ((undef101 - 1) <= undef11) /\ (undef11 > 0) /\ (undef100 > 3) /\ (undef101 > 1), par{arg1 -> undef100, arg2 -> undef101, arg3 -> undef102, arg4 -> undef103}>
<l2, l6, (undef21 > arg4) /\ (arg4 > 0) /\ (undef22 > arg4) /\ (undef23 > arg4) /\ (undef24 > 1) /\ (undef25 > ~(1)) /\ (undef17 <= arg1) /\ ((undef17 + 6) <= arg2) /\ ((undef17 + 4) <= arg3) /\ (arg1 > 0) /\ (arg2 > 6) /\ (arg3 > 4) /\ (undef17 > 0) /\ ((undef100 - 3) <= undef17) /\ (undef104 > 1) /\ ((undef101 - 1) <= undef17) /\ (undef17 > 0) /\ (undef100 > 3) /\ (undef101 > 1), par{arg1 -> undef100, arg2 -> undef101, arg3 -> undef102, arg4 -> undef103}>
<l2, l6, (undef36 > arg4) /\ (arg4 > 0) /\ (undef37 > arg4) /\ (undef38 > arg4) /\ (undef39 > 1) /\ (undef40 > ~(1)) /\ (undef32 <= arg1) /\ ((undef32 + 6) <= arg2) /\ ((undef32 + 4) <= arg3) /\ (arg1 > 0) /\ (arg2 > 6) /\ (arg3 > 4) /\ (undef32 > 0) /\ (undef33 > 6) /\ (undef105 <= undef33) /\ (undef109 > 1) /\ ((undef106 + 2) <= undef33) /\ (undef32 > 0) /\ (undef33 > 4) /\ (undef105 > 4) /\ (undef106 > 2), par{arg1 -> undef105, arg2 -> undef106, arg3 -> undef107, arg4 -> undef108}>
<l2, l6, (undef45 > ~(1)) /\ (undef46 > 1) /\ (undef41 <= arg1) /\ ((undef41 + 7) <= arg2) /\ ((undef41 + 5) <= arg3) /\ ((undef42 - 5) <= arg1) /\ ((undef42 + 2) <= arg2) /\ (undef42 <= arg3) /\ (arg1 > 0) /\ (arg2 > 7) /\ (arg3 > 5) /\ (undef41 > 0) /\ (undef42 > 5) /\ (undef105 <= undef42) /\ (undef109 > 1) /\ ((undef106 + 2) <= undef42) /\ (undef41 > 0) /\ (undef42 > 4) /\ (undef105 > 4) /\ (undef106 > 2), par{arg1 -> undef105, arg2 -> undef106, arg3 -> undef107, arg4 -> undef108}>
<l2, l6, (undef51 > ~(1)) /\ (undef52 > 1) /\ (undef47 <= arg1) /\ ((undef47 + 7) <= arg2) /\ ((undef47 + 5) <= arg3) /\ (arg1 > 0) /\ (arg2 > 7) /\ (arg3 > 5) /\ (undef47 > 0) /\ (undef48 > 6) /\ (undef105 <= undef48) /\ (undef109 > 1) /\ ((undef106 + 2) <= undef48) /\ (undef47 > 0) /\ (undef48 > 4) /\ (undef105 > 4) /\ (undef106 > 2), par{arg1 -> undef105, arg2 -> undef106, arg3 -> undef107, arg4 -> undef108}>
<l2, l6, (undef63 > arg4) /\ (arg4 > 0) /\ (undef64 > arg4) /\ (undef65 > arg4) /\ (undef66 > 1) /\ (undef67 > ~(1)) /\ (undef59 <= arg1) /\ ((undef59 + 6) <= arg2) /\ ((undef59 + 4) <= arg3) /\ ((undef60 - 5) <= arg1) /\ ((undef60 + 1) <= arg2) /\ ((undef60 - 1) <= arg3) /\ (arg1 > 0) /\ (arg2 > 6) /\ (arg3 > 4) /\ (undef59 > 0) /\ (undef60 > 5) /\ (undef105 <= undef60) /\ (undef109 > 1) /\ ((undef106 + 2) <= undef60) /\ (undef59 > 0) /\ (undef60 > 4) /\ (undef105 > 4) /\ (undef106 > 2), par{arg1 -> undef105, arg2 -> undef106, arg3 -> undef107, arg4 -> undef108}>
<l2, l5, (undef82 > arg4) /\ (arg4 > 0) /\ (undef83 > arg4) /\ (undef84 > arg4) /\ (undef85 > 1) /\ (undef78 > ~(1)) /\ (arg1 > 0) /\ (arg2 > 6) /\ (arg3 > 4), par{arg1 -> undef78, arg2 -> 2, arg3 -> undef80, arg4 -> undef81}>
<l2, l5, (undef86 > ~(1)) /\ (undef90 > 1) /\ (arg1 > 0) /\ (arg2 > 7) /\ (arg3 > 5), par{arg1 -> undef86, arg2 -> 2, arg3 -> undef88, arg4 -> undef89}>
<l5, l5, ((arg1 - 1) < arg1) /\ (arg2 > 0) /\ (arg1 > 1), par{arg1 -> (arg1 - 1), arg3 -> undef98, arg4 -> undef99}>
<l6, l6, ((undef110 + 2) <= arg1) /\ (undef110 <= arg2) /\ ((undef111 + 3) <= arg1) /\ ((undef111 + 1) <= arg2) /\ (arg1 > 2) /\ (arg2 > 0) /\ (undef110 > 0) /\ (undef111 > ~(1)), par{arg1 -> undef110, arg2 -> undef111, arg3 -> undef112, arg4 -> undef113}>

Fresh variables:
undef1, undef2, undef3, 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, undef32, undef33, undef34, undef35, undef36, undef37, undef38, undef39, undef40, undef41, undef42, undef43, undef44, undef45, undef46, undef47, undef48, undef49, undef50, undef51, undef52, undef53, undef54, undef55, undef56, undef57, undef58, undef59, undef60, undef61, undef62, undef63, undef64, undef65, undef66, undef67, undef68, undef69, undef70, undef71, undef72, undef73, undef74, undef76, undef77, undef78, undef80, undef81, undef82, undef83, undef84, undef85, undef86, undef88, undef89, undef90, undef91, undef93, undef94, undef95, undef98, undef99, undef100, undef101, undef102, undef103, undef104, undef105, undef106, undef107, undef108, undef109, undef110, undef111, undef112, undef113, undef114, undef115, undef116, undef117, 

Undef variables:
undef1, undef2, undef3, 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, undef32, undef33, undef34, undef35, undef36, undef37, undef38, undef39, undef40, undef41, undef42, undef43, undef44, undef45, undef46, undef47, undef48, undef49, undef50, undef51, undef52, undef53, undef54, undef55, undef56, undef57, undef58, undef59, undef60, undef61, undef62, undef63, undef64, undef65, undef66, undef67, undef68, undef69, undef70, undef71, undef72, undef73, undef74, undef76, undef77, undef78, undef80, undef81, undef82, undef83, undef84, undef85, undef86, undef88, undef89, undef90, undef91, undef93, undef94, undef95, undef98, undef99, undef100, undef101, undef102, undef103, undef104, undef105, undef106, undef107, undef108, undef109, undef110, undef111, undef112, undef113, undef114, undef115, undef116, undef117, 

Abstraction variables:

Exit nodes:

Accepting locations:

Asserts:

*************************************************************
*******************************************************************************************
***********************       WORKING TRANSITION SYSTEM (DAG)       ***********************
*******************************************************************************************

Init Location: 0
Graph 0:
Transitions:
Variables:

Graph 1:
Transitions:
Variables:

Graph 2:
Transitions:
<l5, l5, 1 <= arg2 /\ 2 <= arg1, {arg1 -> -1 + arg1, arg3 -> undef98, arg4 -> undef99, rest remain the same}>
Variables:
arg1, arg2, arg3, arg4

Graph 3:
Transitions:
<l6, l6, 1 <= arg2 /\ 1 + undef111 <= arg2 /\ 1 <= undef110 /\ undef110 <= arg2 /\ 0 <= undef111 /\ 2 + undef110 <= arg1 /\ 3 <= arg1 /\ 3 + undef111 <= arg1, {arg1 -> undef110, arg2 -> undef111, arg3 -> undef112, arg4 -> undef113, rest remain the same}>
Variables:
arg1, arg2, arg3, arg4

Precedence: 
Graph 0

Graph 1
<l0, l2, 1 <= undef1 /\ 1 <= undef114 /\ 1 <= undef115 /\ undef1 <= undef114 /\ 0 <= undef5 /\ 8 <= undef2 /\ 6 <= undef3 /\ undef2 <= 7 + undef114 /\ undef3 <= 5 + undef114, {arg1 -> undef1, arg2 -> undef2, arg3 -> undef3, arg4 -> 0, rest remain the same}>
<l0, l2, 1 <= undef6 /\ 1 <= undef114 /\ 1 <= undef115 /\ undef6 <= undef114 /\ 0 <= undef10 /\ 7 <= undef8 /\ 9 <= undef7, {arg1 -> undef6, arg2 -> undef7, arg3 -> undef8, arg4 -> undef9, rest remain the same}>

Graph 2
<l0, l5, 1 <= undef114 /\ 1 <= undef115 /\ 0 <= undef74, {arg1 -> undef74, arg2 -> 1, arg3 -> undef76, arg4 -> undef77, rest remain the same}>
<l0, l5, 1 <= undef114 /\ 0 <= undef91 /\ 0 <= undef95 /\ 2 <= undef115, {arg1 -> undef91, arg2 -> 2, arg3 -> undef93, arg4 -> undef94, rest remain the same}>
<l2, l5, 1 <= arg1 /\ 1 + arg4 <= undef82 /\ 1 + arg4 <= undef83 /\ 1 + arg4 <= undef84 /\ 1 <= arg4 /\ 0 <= undef78 /\ 7 <= arg2 /\ 5 <= arg3 /\ 2 <= undef85, {arg1 -> undef78, arg2 -> 2, arg3 -> undef80, arg4 -> undef81, rest remain the same}>
<l2, l5, 1 <= arg1 /\ 0 <= undef86 /\ 8 <= arg2 /\ 6 <= arg3 /\ 2 <= undef90, {arg1 -> undef86, arg2 -> 2, arg3 -> undef88, arg4 -> undef89, rest remain the same}>

Graph 3
<l0, l6, 1 <= undef26 /\ 1 <= undef114 /\ undef101 <= 1 + undef26 /\ undef26 <= undef114 /\ 0 <= undef30 /\ 0 <= undef31 /\ 4 <= undef100 /\ 2 <= undef101 /\ 2 <= undef104 /\ 2 <= undef115 /\ undef100 <= 3 + undef26, {arg1 -> undef100, arg2 -> undef101, arg3 -> undef102, arg4 -> undef103, rest remain the same}>
<l0, l6, 1 <= undef53 /\ 1 <= undef114 /\ undef53 <= undef114 /\ undef105 <= undef54 /\ 0 <= undef57 /\ 0 <= undef58 /\ 7 <= undef54 /\ 5 <= undef105 /\ 2 + undef106 <= undef54 /\ 2 <= undef109 /\ 2 <= undef115 /\ 3 <= undef106, {arg1 -> undef105, arg2 -> undef106, arg3 -> undef107, arg4 -> undef108, rest remain the same}>
<l0, l6, 1 <= undef68 /\ 1 <= undef114 /\ undef68 <= undef114 /\ undef105 <= undef69 /\ 0 <= undef72 /\ 0 <= undef73 /\ 5 <= undef105 /\ 6 <= undef69 /\ 2 + undef106 <= undef69 /\ 2 <= undef109 /\ 2 <= undef115 /\ 3 <= undef106 /\ undef69 <= 5 + undef114, {arg1 -> undef105, arg2 -> undef106, arg3 -> undef107, arg4 -> undef108, rest remain the same}>
<l2, l6, 1 <= arg1 /\ 1 <= undef11 /\ undef101 <= 1 + undef11 /\ undef11 <= arg1 /\ 0 <= undef15 /\ 7 + undef11 <= arg2 /\ 5 + undef11 <= arg3 /\ 8 <= arg2 /\ 6 <= arg3 /\ 4 <= undef100 /\ 2 <= undef16 /\ 2 <= undef101 /\ 2 <= undef104 /\ undef100 <= 3 + undef11, {arg1 -> undef100, arg2 -> undef101, arg3 -> undef102, arg4 -> undef103, rest remain the same}>
<l2, l6, 1 <= arg1 /\ 1 + arg4 <= undef21 /\ 1 + arg4 <= undef22 /\ 1 + arg4 <= undef23 /\ 1 <= arg4 /\ 1 <= undef17 /\ undef101 <= 1 + undef17 /\ undef17 <= arg1 /\ 0 <= undef25 /\ 7 <= arg2 /\ 5 <= arg3 /\ 6 + undef17 <= arg2 /\ 4 + undef17 <= arg3 /\ 4 <= undef100 /\ 2 <= undef24 /\ 2 <= undef101 /\ 2 <= undef104 /\ undef100 <= 3 + undef17, {arg1 -> undef100, arg2 -> undef101, arg3 -> undef102, arg4 -> undef103, rest remain the same}>
<l2, l6, 1 <= arg1 /\ 1 + arg4 <= undef36 /\ 1 + arg4 <= undef37 /\ 1 + arg4 <= undef38 /\ 1 <= arg4 /\ 1 <= undef32 /\ undef32 <= arg1 /\ undef105 <= undef33 /\ 0 <= undef40 /\ 7 <= arg2 /\ 7 <= undef33 /\ 5 <= arg3 /\ 5 <= undef105 /\ 6 + undef32 <= arg2 /\ 4 + undef32 <= arg3 /\ 2 + undef106 <= undef33 /\ 2 <= undef39 /\ 2 <= undef109 /\ 3 <= undef106, {arg1 -> undef105, arg2 -> undef106, arg3 -> undef107, arg4 -> undef108, rest remain the same}>
<l2, l6, 1 <= arg1 /\ 1 <= undef41 /\ undef41 <= arg1 /\ undef42 <= arg3 /\ undef105 <= undef42 /\ 0 <= undef45 /\ 7 + undef41 <= arg2 /\ 5 + undef41 <= arg3 /\ 5 <= undef105 /\ 8 <= arg2 /\ 6 <= arg3 /\ 6 <= undef42 /\ 2 + undef42 <= arg2 /\ 2 + undef106 <= undef42 /\ 2 <= undef46 /\ 2 <= undef109 /\ 3 <= undef106 /\ undef42 <= 5 + arg1, {arg1 -> undef105, arg2 -> undef106, arg3 -> undef107, arg4 -> undef108, rest remain the same}>
<l2, l6, 1 <= arg1 /\ 1 <= undef47 /\ undef47 <= arg1 /\ undef105 <= undef48 /\ 0 <= undef51 /\ 7 + undef47 <= arg2 /\ 7 <= undef48 /\ 5 + undef47 <= arg3 /\ 5 <= undef105 /\ 8 <= arg2 /\ 6 <= arg3 /\ 2 + undef106 <= undef48 /\ 2 <= undef52 /\ 2 <= undef109 /\ 3 <= undef106, {arg1 -> undef105, arg2 -> undef106, arg3 -> undef107, arg4 -> undef108, rest remain the same}>
<l2, l6, 1 <= arg1 /\ 1 + undef60 <= arg2 /\ 1 + arg4 <= undef63 /\ 1 + arg4 <= undef64 /\ 1 + arg4 <= undef65 /\ 1 <= arg4 /\ 1 <= undef59 /\ undef60 <= 1 + arg3 /\ undef59 <= arg1 /\ undef105 <= undef60 /\ 0 <= undef67 /\ 7 <= arg2 /\ 5 <= arg3 /\ 5 <= undef105 /\ 6 + undef59 <= arg2 /\ 6 <= undef60 /\ 4 + undef59 <= arg3 /\ 2 + undef106 <= undef60 /\ 2 <= undef66 /\ 2 <= undef109 /\ 3 <= undef106 /\ undef60 <= 5 + arg1, {arg1 -> undef105, arg2 -> undef106, arg3 -> undef107, arg4 -> undef108, rest remain the same}>

Map Locations to Subgraph:
( 0 , 0 )
( 2 , 1 )
( 5 , 2 )
( 6 , 3 )

*******************************************************************************************
********************************    CHECKING ASSERTIONS    ********************************
*******************************************************************************************

Proving termination of subgraph 0
Proving termination of subgraph 1
Analyzing SCC {l2}...
No cycles found.

Proving termination of subgraph 2
Checking unfeasibility...
Time used: 0.002172

Checking conditional termination of SCC {l5}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000498s
Ranking function: -2 + arg1
New Graphs: 
Proving termination of subgraph 3
Checking unfeasibility...
Time used: 0.006212

Checking conditional termination of SCC {l6}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001098s
Ranking function: (~(4) / 3) + (1 / 3)*arg1 + (1 / 3)*arg2
New Graphs: 
Program Terminates