YES

Solver Timeout: 4
Global Timeout: 300
No parsing errors!
Init Location: 0
Transitions:
<l0, l5, true>
<l1, l2, ((undef1 - 1) <= arg1) /\ (arg2 > ~(1)) /\ ((undef2 - 201) <= arg1) /\ (arg1 > 0) /\ (undef1 > 1) /\ (undef2 > 201), par{arg1 -> undef1, arg2 -> undef2, arg3 -> arg2, arg4 -> 0, arg5 -> 0, arg6 -> 200, arg7 -> 200, arg8 -> undef8}>
<l2, l3, (arg3 > 0) /\ ((arg3 - 1) < arg3) /\ (arg1 >= undef17) /\ (arg1 > 0) /\ (arg2 > 0) /\ (undef17 > 0) /\ (undef18 > 0) /\ ((arg4 + 2) <= arg1) /\ ((arg5 + 2) <= arg1) /\ (arg2 >= (arg7 + 2)) /\ ((arg6 + 2) <= arg2), par{arg8 -> undef16}>
<l3, l2, (arg3 > 0) /\ ((arg3 - 1) < arg3) /\ (arg1 >= undef19) /\ (arg1 > 0) /\ (arg2 > 0) /\ (undef19 > 0) /\ (undef20 > 0) /\ ((arg4 + 2) <= arg1) /\ ((arg5 + 2) <= arg1) /\ ((arg6 + 2) <= arg2) /\ (arg2 >= (arg7 + 2)) /\ (((((arg4 + arg5) + arg6) - arg7) - (2 * undef24)) >= 0) /\ (((((arg4 + arg5) + arg6) - arg7) - (2 * undef24)) < 2) /\ (((((arg6 + arg7) + arg5) - arg4) - (2 * undef25)) < 2) /\ (((((arg6 + arg7) + arg5) - arg4) - (2 * undef25)) >= 0), par{arg1 -> undef19, arg2 -> undef20, arg3 -> (arg3 - 1), arg6 -> undef24, arg7 -> undef25, arg8 -> undef26}>
<l2, l3, (undef35 <= arg2) /\ (arg1 > 0) /\ (arg2 > 0) /\ (undef36 > 0) /\ (undef35 > 0) /\ ((arg4 + 2) <= arg1) /\ ((arg5 + 2) <= arg1) /\ ((arg7 + 2) <= arg2) /\ ((arg6 + 2) <= arg2) /\ (1 = arg3), par{arg3 -> 1, arg8 -> undef34}>
<l3, l4, (undef40 <= arg2) /\ (arg1 > 0) /\ (arg2 > 0) /\ (undef39 > 0) /\ (undef40 > 0) /\ ((arg4 + 2) <= arg1) /\ ((arg5 + 2) <= arg1) /\ ((arg6 + 2) <= arg2) /\ ((arg7 + 2) <= arg2) /\ (((((arg6 + arg7) + arg5) - arg4) - (2 * undef42)) >= 0) /\ (((((arg6 + arg7) + arg5) - arg4) - (2 * undef42)) < 2) /\ (((((arg4 + arg5) + arg6) - arg7) - (2 * undef41)) < 2) /\ (((((arg4 + arg5) + arg6) - arg7) - (2 * undef41)) >= 0) /\ (1 = arg3), par{arg1 -> 1, arg2 -> 0, arg3 -> undef39, arg4 -> undef40, arg5 -> undef41, arg6 -> undef42, arg7 -> arg6, arg8 -> arg7}>
<l2, l3, (arg3 > 0) /\ ((arg3 - 1) < arg3) /\ (undef53 <= arg2) /\ (arg1 > 0) /\ (arg2 > 0) /\ (undef54 > 0) /\ (undef53 > 0) /\ ((arg4 + 2) <= arg1) /\ ((arg5 + 2) <= arg1) /\ ((arg7 + 2) <= arg2) /\ ((arg6 + 2) <= arg2), par{arg8 -> undef52}>
<l3, l4, (arg3 > 0) /\ ((arg3 - 1) < arg3) /\ (undef58 <= arg2) /\ (arg1 > 0) /\ (arg2 > 0) /\ (undef57 > 0) /\ (undef58 > 0) /\ ((arg4 + 2) <= arg1) /\ ((arg5 + 2) <= arg1) /\ ((arg6 + 2) <= arg2) /\ ((arg7 + 2) <= arg2) /\ (((((arg4 + arg5) + arg6) - arg7) - (2 * undef59)) >= 0) /\ (((((arg4 + arg5) + arg6) - arg7) - (2 * undef59)) < 2) /\ (((((arg6 + arg7) + arg5) - arg4) - (2 * undef60)) < 2) /\ (((((arg6 + arg7) + arg5) - arg4) - (2 * undef60)) >= 0), par{arg1 -> arg3, arg2 -> (arg3 - 1), arg3 -> undef57, arg4 -> undef58, arg5 -> undef59, arg6 -> undef60, arg7 -> arg6, arg8 -> arg7}>
<l4, l2, (arg2 < arg1) /\ (arg1 > 0) /\ (undef63 <= arg3) /\ (undef64 <= arg4) /\ (arg3 > 0) /\ (arg4 > 0) /\ (undef63 > 0) /\ (undef64 > 0) /\ ((arg5 + 2) <= arg3) /\ ((arg6 + 2) <= arg3) /\ ((arg8 + 2) <= arg4) /\ ((arg7 + 2) <= arg4), par{arg1 -> undef63, arg2 -> undef64, arg3 -> arg2, arg4 -> arg5, arg5 -> arg6, arg6 -> arg7, arg7 -> arg8, arg8 -> undef70}>
<l5, l1, true, par{arg1 -> undef71, arg2 -> undef72, arg3 -> undef73, arg4 -> undef74, arg5 -> undef75, arg6 -> undef76, arg7 -> undef77, arg8 -> undef78}>

Fresh variables:
undef1, undef2, undef8, undef16, undef17, undef18, undef19, undef20, undef24, undef25, undef26, undef34, undef35, undef36, undef39, undef40, undef41, undef42, undef52, undef53, undef54, undef57, undef58, undef59, undef60, undef63, undef64, undef70, undef71, undef72, undef73, undef74, undef75, undef76, undef77, undef78, 

Undef variables:
undef1, undef2, undef8, undef16, undef17, undef18, undef19, undef20, undef24, undef25, undef26, undef34, undef35, undef36, undef39, undef40, undef41, undef42, undef52, undef53, undef54, undef57, undef58, undef59, undef60, undef63, undef64, undef70, undef71, undef72, undef73, undef74, undef75, undef76, undef77, undef78, 

Abstraction variables:

Exit nodes:

Accepting locations:

Asserts:

Preprocessed LLVMGraph
Init Location: 0
Transitions:
<l0, l2, (arg1 = undef1) /\ (arg2 = undef2) /\ (arg3 = undef72) /\ (arg4 = 0) /\ (arg5 = 0) /\ (arg6 = 200) /\ (arg7 = 200) /\ ((undef1 - 1) <= undef71) /\ (undef72 > ~(1)) /\ ((undef2 - 201) <= undef71) /\ (undef71 > 0) /\ (undef1 > 1) /\ (undef2 > 201)>
<l2, l2, (arg3 > 0) /\ ((arg3 - 1) < arg3) /\ (arg1 >= undef17) /\ (arg1 > 0) /\ (arg2 > 0) /\ (undef17 > 0) /\ (undef18 > 0) /\ ((arg4 + 2) <= arg1) /\ ((arg5 + 2) <= arg1) /\ (arg2 >= (arg7 + 2)) /\ ((arg6 + 2) <= arg2) /\ (arg3 > 0) /\ ((arg3 - 1) < arg3) /\ (arg1 >= undef19) /\ (arg1 > 0) /\ (arg2 > 0) /\ (undef19 > 0) /\ (undef20 > 0) /\ ((arg4 + 2) <= arg1) /\ ((arg5 + 2) <= arg1) /\ ((arg6 + 2) <= arg2) /\ (arg2 >= (arg7 + 2)) /\ (((((arg4 + arg5) + arg6) - arg7) - (2 * undef24)) >= 0) /\ (((((arg4 + arg5) + arg6) - arg7) - (2 * undef24)) < 2) /\ (((((arg6 + arg7) + arg5) - arg4) - (2 * undef25)) < 2) /\ (((((arg6 + arg7) + arg5) - arg4) - (2 * undef25)) >= 0), par{arg1 -> undef19, arg2 -> undef20, arg3 -> (arg3 - 1), arg6 -> undef24, arg7 -> undef25}>
<l2, l2, (arg3 > 0) /\ ((arg3 - 1) < arg3) /\ (arg1 >= undef17) /\ (arg1 > 0) /\ (arg2 > 0) /\ (undef17 > 0) /\ (undef18 > 0) /\ ((arg4 + 2) <= arg1) /\ ((arg5 + 2) <= arg1) /\ (arg2 >= (arg7 + 2)) /\ ((arg6 + 2) <= arg2) /\ (undef40 <= arg2) /\ (arg1 > 0) /\ (arg2 > 0) /\ (undef39 > 0) /\ (undef40 > 0) /\ ((arg4 + 2) <= arg1) /\ ((arg5 + 2) <= arg1) /\ ((arg6 + 2) <= arg2) /\ ((arg7 + 2) <= arg2) /\ (((((arg6 + arg7) + arg5) - arg4) - (2 * undef42)) >= 0) /\ (((((arg6 + arg7) + arg5) - arg4) - (2 * undef42)) < 2) /\ (((((arg4 + arg5) + arg6) - arg7) - (2 * undef41)) < 2) /\ (((((arg4 + arg5) + arg6) - arg7) - (2 * undef41)) >= 0) /\ (1 = arg3) /\ (0 < 1) /\ (1 > 0) /\ (undef63 <= undef39) /\ (undef64 <= undef40) /\ (undef39 > 0) /\ (undef40 > 0) /\ (undef63 > 0) /\ (undef64 > 0) /\ ((undef41 + 2) <= undef39) /\ ((undef42 + 2) <= undef39) /\ ((arg7 + 2) <= undef40) /\ ((arg6 + 2) <= undef40), par{arg1 -> undef63, arg2 -> undef64, arg3 -> 0, arg4 -> undef41, arg5 -> undef42, arg6 -> arg6, arg7 -> arg7}>
<l2, l2, (arg3 > 0) /\ ((arg3 - 1) < arg3) /\ (arg1 >= undef17) /\ (arg1 > 0) /\ (arg2 > 0) /\ (undef17 > 0) /\ (undef18 > 0) /\ ((arg4 + 2) <= arg1) /\ ((arg5 + 2) <= arg1) /\ (arg2 >= (arg7 + 2)) /\ ((arg6 + 2) <= arg2) /\ (arg3 > 0) /\ ((arg3 - 1) < arg3) /\ (undef58 <= arg2) /\ (arg1 > 0) /\ (arg2 > 0) /\ (undef57 > 0) /\ (undef58 > 0) /\ ((arg4 + 2) <= arg1) /\ ((arg5 + 2) <= arg1) /\ ((arg6 + 2) <= arg2) /\ ((arg7 + 2) <= arg2) /\ (((((arg4 + arg5) + arg6) - arg7) - (2 * undef59)) >= 0) /\ (((((arg4 + arg5) + arg6) - arg7) - (2 * undef59)) < 2) /\ (((((arg6 + arg7) + arg5) - arg4) - (2 * undef60)) < 2) /\ (((((arg6 + arg7) + arg5) - arg4) - (2 * undef60)) >= 0) /\ ((arg3 - 1) < arg3) /\ (arg3 > 0) /\ (undef63 <= undef57) /\ (undef64 <= undef58) /\ (undef57 > 0) /\ (undef58 > 0) /\ (undef63 > 0) /\ (undef64 > 0) /\ ((undef59 + 2) <= undef57) /\ ((undef60 + 2) <= undef57) /\ ((arg7 + 2) <= undef58) /\ ((arg6 + 2) <= undef58), par{arg1 -> undef63, arg2 -> undef64, arg3 -> (arg3 - 1), arg4 -> undef59, arg5 -> undef60, arg6 -> arg6, arg7 -> arg7}>
<l2, l2, (undef35 <= arg2) /\ (arg1 > 0) /\ (arg2 > 0) /\ (undef36 > 0) /\ (undef35 > 0) /\ ((arg4 + 2) <= arg1) /\ ((arg5 + 2) <= arg1) /\ ((arg7 + 2) <= arg2) /\ ((arg6 + 2) <= arg2) /\ (1 = arg3) /\ (1 > 0) /\ ((1 - 1) < 1) /\ (arg1 >= undef19) /\ (arg1 > 0) /\ (arg2 > 0) /\ (undef19 > 0) /\ (undef20 > 0) /\ ((arg4 + 2) <= arg1) /\ ((arg5 + 2) <= arg1) /\ ((arg6 + 2) <= arg2) /\ (arg2 >= (arg7 + 2)) /\ (((((arg4 + arg5) + arg6) - arg7) - (2 * undef24)) >= 0) /\ (((((arg4 + arg5) + arg6) - arg7) - (2 * undef24)) < 2) /\ (((((arg6 + arg7) + arg5) - arg4) - (2 * undef25)) < 2) /\ (((((arg6 + arg7) + arg5) - arg4) - (2 * undef25)) >= 0), par{arg1 -> undef19, arg2 -> undef20, arg3 -> (1 - 1), arg6 -> undef24, arg7 -> undef25}>
<l2, l2, (undef35 <= arg2) /\ (arg1 > 0) /\ (arg2 > 0) /\ (undef36 > 0) /\ (undef35 > 0) /\ ((arg4 + 2) <= arg1) /\ ((arg5 + 2) <= arg1) /\ ((arg7 + 2) <= arg2) /\ ((arg6 + 2) <= arg2) /\ (1 = arg3) /\ (undef40 <= arg2) /\ (arg1 > 0) /\ (arg2 > 0) /\ (undef39 > 0) /\ (undef40 > 0) /\ ((arg4 + 2) <= arg1) /\ ((arg5 + 2) <= arg1) /\ ((arg6 + 2) <= arg2) /\ ((arg7 + 2) <= arg2) /\ (((((arg6 + arg7) + arg5) - arg4) - (2 * undef42)) >= 0) /\ (((((arg6 + arg7) + arg5) - arg4) - (2 * undef42)) < 2) /\ (((((arg4 + arg5) + arg6) - arg7) - (2 * undef41)) < 2) /\ (((((arg4 + arg5) + arg6) - arg7) - (2 * undef41)) >= 0) /\ (1 = 1) /\ (0 < 1) /\ (1 > 0) /\ (undef63 <= undef39) /\ (undef64 <= undef40) /\ (undef39 > 0) /\ (undef40 > 0) /\ (undef63 > 0) /\ (undef64 > 0) /\ ((undef41 + 2) <= undef39) /\ ((undef42 + 2) <= undef39) /\ ((arg7 + 2) <= undef40) /\ ((arg6 + 2) <= undef40), par{arg1 -> undef63, arg2 -> undef64, arg3 -> 0, arg4 -> undef41, arg5 -> undef42, arg6 -> arg6, arg7 -> arg7}>
<l2, l2, (undef35 <= arg2) /\ (arg1 > 0) /\ (arg2 > 0) /\ (undef36 > 0) /\ (undef35 > 0) /\ ((arg4 + 2) <= arg1) /\ ((arg5 + 2) <= arg1) /\ ((arg7 + 2) <= arg2) /\ ((arg6 + 2) <= arg2) /\ (1 = arg3) /\ (1 > 0) /\ ((1 - 1) < 1) /\ (undef58 <= arg2) /\ (arg1 > 0) /\ (arg2 > 0) /\ (undef57 > 0) /\ (undef58 > 0) /\ ((arg4 + 2) <= arg1) /\ ((arg5 + 2) <= arg1) /\ ((arg6 + 2) <= arg2) /\ ((arg7 + 2) <= arg2) /\ (((((arg4 + arg5) + arg6) - arg7) - (2 * undef59)) >= 0) /\ (((((arg4 + arg5) + arg6) - arg7) - (2 * undef59)) < 2) /\ (((((arg6 + arg7) + arg5) - arg4) - (2 * undef60)) < 2) /\ (((((arg6 + arg7) + arg5) - arg4) - (2 * undef60)) >= 0) /\ ((1 - 1) < 1) /\ (1 > 0) /\ (undef63 <= undef57) /\ (undef64 <= undef58) /\ (undef57 > 0) /\ (undef58 > 0) /\ (undef63 > 0) /\ (undef64 > 0) /\ ((undef59 + 2) <= undef57) /\ ((undef60 + 2) <= undef57) /\ ((arg7 + 2) <= undef58) /\ ((arg6 + 2) <= undef58), par{arg1 -> undef63, arg2 -> undef64, arg3 -> (1 - 1), arg4 -> undef59, arg5 -> undef60, arg6 -> arg6, arg7 -> arg7}>
<l2, l2, (arg3 > 0) /\ ((arg3 - 1) < arg3) /\ (undef53 <= arg2) /\ (arg1 > 0) /\ (arg2 > 0) /\ (undef54 > 0) /\ (undef53 > 0) /\ ((arg4 + 2) <= arg1) /\ ((arg5 + 2) <= arg1) /\ ((arg7 + 2) <= arg2) /\ ((arg6 + 2) <= arg2) /\ (arg3 > 0) /\ ((arg3 - 1) < arg3) /\ (arg1 >= undef19) /\ (arg1 > 0) /\ (arg2 > 0) /\ (undef19 > 0) /\ (undef20 > 0) /\ ((arg4 + 2) <= arg1) /\ ((arg5 + 2) <= arg1) /\ ((arg6 + 2) <= arg2) /\ (arg2 >= (arg7 + 2)) /\ (((((arg4 + arg5) + arg6) - arg7) - (2 * undef24)) >= 0) /\ (((((arg4 + arg5) + arg6) - arg7) - (2 * undef24)) < 2) /\ (((((arg6 + arg7) + arg5) - arg4) - (2 * undef25)) < 2) /\ (((((arg6 + arg7) + arg5) - arg4) - (2 * undef25)) >= 0), par{arg1 -> undef19, arg2 -> undef20, arg3 -> (arg3 - 1), arg6 -> undef24, arg7 -> undef25}>
<l2, l2, (arg3 > 0) /\ ((arg3 - 1) < arg3) /\ (undef53 <= arg2) /\ (arg1 > 0) /\ (arg2 > 0) /\ (undef54 > 0) /\ (undef53 > 0) /\ ((arg4 + 2) <= arg1) /\ ((arg5 + 2) <= arg1) /\ ((arg7 + 2) <= arg2) /\ ((arg6 + 2) <= arg2) /\ (undef40 <= arg2) /\ (arg1 > 0) /\ (arg2 > 0) /\ (undef39 > 0) /\ (undef40 > 0) /\ ((arg4 + 2) <= arg1) /\ ((arg5 + 2) <= arg1) /\ ((arg6 + 2) <= arg2) /\ ((arg7 + 2) <= arg2) /\ (((((arg6 + arg7) + arg5) - arg4) - (2 * undef42)) >= 0) /\ (((((arg6 + arg7) + arg5) - arg4) - (2 * undef42)) < 2) /\ (((((arg4 + arg5) + arg6) - arg7) - (2 * undef41)) < 2) /\ (((((arg4 + arg5) + arg6) - arg7) - (2 * undef41)) >= 0) /\ (1 = arg3) /\ (0 < 1) /\ (1 > 0) /\ (undef63 <= undef39) /\ (undef64 <= undef40) /\ (undef39 > 0) /\ (undef40 > 0) /\ (undef63 > 0) /\ (undef64 > 0) /\ ((undef41 + 2) <= undef39) /\ ((undef42 + 2) <= undef39) /\ ((arg7 + 2) <= undef40) /\ ((arg6 + 2) <= undef40), par{arg1 -> undef63, arg2 -> undef64, arg3 -> 0, arg4 -> undef41, arg5 -> undef42, arg6 -> arg6, arg7 -> arg7}>
<l2, l2, (arg3 > 0) /\ ((arg3 - 1) < arg3) /\ (undef53 <= arg2) /\ (arg1 > 0) /\ (arg2 > 0) /\ (undef54 > 0) /\ (undef53 > 0) /\ ((arg4 + 2) <= arg1) /\ ((arg5 + 2) <= arg1) /\ ((arg7 + 2) <= arg2) /\ ((arg6 + 2) <= arg2) /\ (arg3 > 0) /\ ((arg3 - 1) < arg3) /\ (undef58 <= arg2) /\ (arg1 > 0) /\ (arg2 > 0) /\ (undef57 > 0) /\ (undef58 > 0) /\ ((arg4 + 2) <= arg1) /\ ((arg5 + 2) <= arg1) /\ ((arg6 + 2) <= arg2) /\ ((arg7 + 2) <= arg2) /\ (((((arg4 + arg5) + arg6) - arg7) - (2 * undef59)) >= 0) /\ (((((arg4 + arg5) + arg6) - arg7) - (2 * undef59)) < 2) /\ (((((arg6 + arg7) + arg5) - arg4) - (2 * undef60)) < 2) /\ (((((arg6 + arg7) + arg5) - arg4) - (2 * undef60)) >= 0) /\ ((arg3 - 1) < arg3) /\ (arg3 > 0) /\ (undef63 <= undef57) /\ (undef64 <= undef58) /\ (undef57 > 0) /\ (undef58 > 0) /\ (undef63 > 0) /\ (undef64 > 0) /\ ((undef59 + 2) <= undef57) /\ ((undef60 + 2) <= undef57) /\ ((arg7 + 2) <= undef58) /\ ((arg6 + 2) <= undef58), par{arg1 -> undef63, arg2 -> undef64, arg3 -> (arg3 - 1), arg4 -> undef59, arg5 -> undef60, arg6 -> arg6, arg7 -> arg7}>

Fresh variables:
undef1, undef2, undef8, undef16, undef17, undef18, undef19, undef20, undef24, undef25, undef26, undef34, undef35, undef36, undef39, undef40, undef41, undef42, undef52, undef53, undef54, undef57, undef58, undef59, undef60, undef63, undef64, undef70, undef71, undef72, undef73, undef74, undef75, undef76, undef77, undef78, 

Undef variables:
undef1, undef2, undef8, undef16, undef17, undef18, undef19, undef20, undef24, undef25, undef26, undef34, undef35, undef36, undef39, undef40, undef41, undef42, undef52, undef53, undef54, undef57, undef58, undef59, undef60, undef63, undef64, 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:
<l2, l2, 1 <= arg1 /\ 1 <= arg2 /\ 1 <= arg3 /\ 1 <= undef17 /\ 1 <= undef18 /\ 1 <= undef19 /\ 1 <= undef20 /\ arg4 + arg5 + arg6 <= 1 + arg7 + 2*undef24 /\ arg5 + arg6 + arg7 <= 1 + arg4 + 2*undef25 /\ undef17 <= arg1 /\ undef19 <= arg1 /\ arg4 + 2*undef25 <= arg5 + arg6 + arg7 /\ arg7 + 2*undef24 <= arg4 + arg5 + arg6 /\ 2 + arg4 <= arg1 /\ 2 + arg5 <= arg1 /\ 2 + arg6 <= arg2 /\ 2 + arg7 <= arg2, {arg1 -> undef19, arg2 -> undef20, arg3 -> -1 + arg3, arg6 -> undef24, arg7 -> undef25, rest remain the same}>
<l2, l2, 1 <= arg1 /\ 1 <= arg2 /\ 1 <= undef17 /\ 1 <= undef18 /\ 1 <= undef39 /\ 1 <= undef40 /\ 1 <= undef63 /\ 1 <= undef64 /\ arg4 + arg5 + arg6 <= 1 + arg7 + 2*undef41 /\ arg5 + arg6 + arg7 <= 1 + arg4 + 2*undef42 /\ undef17 <= arg1 /\ undef40 <= arg2 /\ arg4 + 2*undef42 <= arg5 + arg6 + arg7 /\ arg7 + 2*undef41 <= arg4 + arg5 + arg6 /\ undef63 <= undef39 /\ undef64 <= undef40 /\ 2 + arg4 <= arg1 /\ 2 + arg5 <= arg1 /\ 2 + arg6 <= arg2 /\ 2 + arg7 <= arg2 /\ 2 + arg6 <= undef40 /\ 2 + arg7 <= undef40 /\ 2 + undef41 <= undef39 /\ 2 + undef42 <= undef39 /\ arg3 = 1, {arg1 -> undef63, arg2 -> undef64, arg3 -> 0, arg4 -> undef41, arg5 -> undef42, rest remain the same}>
<l2, l2, 1 <= arg1 /\ 1 <= arg2 /\ 1 <= arg3 /\ 1 <= undef17 /\ 1 <= undef18 /\ 1 <= undef57 /\ 1 <= undef58 /\ 1 <= undef63 /\ 1 <= undef64 /\ arg4 + arg5 + arg6 <= 1 + arg7 + 2*undef59 /\ arg5 + arg6 + arg7 <= 1 + arg4 + 2*undef60 /\ undef17 <= arg1 /\ undef58 <= arg2 /\ arg4 + 2*undef60 <= arg5 + arg6 + arg7 /\ arg7 + 2*undef59 <= arg4 + arg5 + arg6 /\ undef63 <= undef57 /\ undef64 <= undef58 /\ 2 + arg4 <= arg1 /\ 2 + arg5 <= arg1 /\ 2 + arg6 <= arg2 /\ 2 + arg7 <= arg2 /\ 2 + arg6 <= undef58 /\ 2 + arg7 <= undef58 /\ 2 + undef59 <= undef57 /\ 2 + undef60 <= undef57, {arg1 -> undef63, arg2 -> undef64, arg3 -> -1 + arg3, arg4 -> undef59, arg5 -> undef60, rest remain the same}>
<l2, l2, 1 <= arg1 /\ 1 <= arg2 /\ 1 <= undef19 /\ 1 <= undef20 /\ 1 <= undef35 /\ 1 <= undef36 /\ arg4 + arg5 + arg6 <= 1 + arg7 + 2*undef24 /\ arg5 + arg6 + arg7 <= 1 + arg4 + 2*undef25 /\ undef19 <= arg1 /\ undef35 <= arg2 /\ arg4 + 2*undef25 <= arg5 + arg6 + arg7 /\ arg7 + 2*undef24 <= arg4 + arg5 + arg6 /\ 2 + arg4 <= arg1 /\ 2 + arg5 <= arg1 /\ 2 + arg6 <= arg2 /\ 2 + arg7 <= arg2 /\ arg3 = 1, {arg1 -> undef19, arg2 -> undef20, arg3 -> 0, arg6 -> undef24, arg7 -> undef25, rest remain the same}>
<l2, l2, 1 <= arg1 /\ 1 <= arg2 /\ 1 <= undef35 /\ 1 <= undef36 /\ 1 <= undef39 /\ 1 <= undef40 /\ 1 <= undef63 /\ 1 <= undef64 /\ arg4 + arg5 + arg6 <= 1 + arg7 + 2*undef41 /\ arg5 + arg6 + arg7 <= 1 + arg4 + 2*undef42 /\ undef35 <= arg2 /\ undef40 <= arg2 /\ arg4 + 2*undef42 <= arg5 + arg6 + arg7 /\ arg7 + 2*undef41 <= arg4 + arg5 + arg6 /\ undef63 <= undef39 /\ undef64 <= undef40 /\ 2 + arg4 <= arg1 /\ 2 + arg5 <= arg1 /\ 2 + arg6 <= arg2 /\ 2 + arg7 <= arg2 /\ 2 + arg6 <= undef40 /\ 2 + arg7 <= undef40 /\ 2 + undef41 <= undef39 /\ 2 + undef42 <= undef39 /\ arg3 = 1, {arg1 -> undef63, arg2 -> undef64, arg3 -> 0, arg4 -> undef41, arg5 -> undef42, rest remain the same}>
<l2, l2, 1 <= arg1 /\ 1 <= arg2 /\ 1 <= undef35 /\ 1 <= undef36 /\ 1 <= undef57 /\ 1 <= undef58 /\ 1 <= undef63 /\ 1 <= undef64 /\ arg4 + arg5 + arg6 <= 1 + arg7 + 2*undef59 /\ arg5 + arg6 + arg7 <= 1 + arg4 + 2*undef60 /\ undef35 <= arg2 /\ undef58 <= arg2 /\ arg4 + 2*undef60 <= arg5 + arg6 + arg7 /\ arg7 + 2*undef59 <= arg4 + arg5 + arg6 /\ undef63 <= undef57 /\ undef64 <= undef58 /\ 2 + arg4 <= arg1 /\ 2 + arg5 <= arg1 /\ 2 + arg6 <= arg2 /\ 2 + arg7 <= arg2 /\ 2 + arg6 <= undef58 /\ 2 + arg7 <= undef58 /\ 2 + undef59 <= undef57 /\ 2 + undef60 <= undef57 /\ arg3 = 1, {arg1 -> undef63, arg2 -> undef64, arg3 -> 0, arg4 -> undef59, arg5 -> undef60, rest remain the same}>
<l2, l2, 1 <= arg1 /\ 1 <= arg2 /\ 1 <= arg3 /\ 1 <= undef19 /\ 1 <= undef20 /\ 1 <= undef53 /\ 1 <= undef54 /\ arg4 + arg5 + arg6 <= 1 + arg7 + 2*undef24 /\ arg5 + arg6 + arg7 <= 1 + arg4 + 2*undef25 /\ undef19 <= arg1 /\ undef53 <= arg2 /\ arg4 + 2*undef25 <= arg5 + arg6 + arg7 /\ arg7 + 2*undef24 <= arg4 + arg5 + arg6 /\ 2 + arg4 <= arg1 /\ 2 + arg5 <= arg1 /\ 2 + arg6 <= arg2 /\ 2 + arg7 <= arg2, {arg1 -> undef19, arg2 -> undef20, arg3 -> -1 + arg3, arg6 -> undef24, arg7 -> undef25, rest remain the same}>
<l2, l2, 1 <= arg1 /\ 1 <= arg2 /\ 1 <= undef39 /\ 1 <= undef40 /\ 1 <= undef53 /\ 1 <= undef54 /\ 1 <= undef63 /\ 1 <= undef64 /\ arg4 + arg5 + arg6 <= 1 + arg7 + 2*undef41 /\ arg5 + arg6 + arg7 <= 1 + arg4 + 2*undef42 /\ undef40 <= arg2 /\ undef53 <= arg2 /\ arg4 + 2*undef42 <= arg5 + arg6 + arg7 /\ arg7 + 2*undef41 <= arg4 + arg5 + arg6 /\ undef63 <= undef39 /\ undef64 <= undef40 /\ 2 + arg4 <= arg1 /\ 2 + arg5 <= arg1 /\ 2 + arg6 <= arg2 /\ 2 + arg7 <= arg2 /\ 2 + arg6 <= undef40 /\ 2 + arg7 <= undef40 /\ 2 + undef41 <= undef39 /\ 2 + undef42 <= undef39 /\ arg3 = 1, {arg1 -> undef63, arg2 -> undef64, arg3 -> 0, arg4 -> undef41, arg5 -> undef42, rest remain the same}>
<l2, l2, 1 <= arg1 /\ 1 <= arg2 /\ 1 <= arg3 /\ 1 <= undef53 /\ 1 <= undef54 /\ 1 <= undef57 /\ 1 <= undef58 /\ 1 <= undef63 /\ 1 <= undef64 /\ arg4 + arg5 + arg6 <= 1 + arg7 + 2*undef59 /\ arg5 + arg6 + arg7 <= 1 + arg4 + 2*undef60 /\ undef53 <= arg2 /\ undef58 <= arg2 /\ arg4 + 2*undef60 <= arg5 + arg6 + arg7 /\ arg7 + 2*undef59 <= arg4 + arg5 + arg6 /\ undef63 <= undef57 /\ undef64 <= undef58 /\ 2 + arg4 <= arg1 /\ 2 + arg5 <= arg1 /\ 2 + arg6 <= arg2 /\ 2 + arg7 <= arg2 /\ 2 + arg6 <= undef58 /\ 2 + arg7 <= undef58 /\ 2 + undef59 <= undef57 /\ 2 + undef60 <= undef57, {arg1 -> undef63, arg2 -> undef64, arg3 -> -1 + arg3, arg4 -> undef59, arg5 -> undef60, rest remain the same}>
Variables:
arg1, arg2, arg3, arg4, arg5, arg6, arg7

Precedence: 
Graph 0

Graph 1
<l0, l2, 1 <= undef71 /\ undef1 <= 1 + undef71 /\ 0 <= undef72 /\ 2 <= undef1 /\ undef2 <= 201 + undef71 /\ 202 <= undef2 /\ arg1 = undef1 /\ arg2 = undef2 /\ arg3 = undef72 /\ arg4 = 0 /\ arg5 = 0 /\ arg6 = 200 /\ arg7 = 200, {all remain the same}>

Map Locations to Subgraph:
( 0 , 0 )
( 2 , 1 )

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

Proving termination of subgraph 0
Proving termination of subgraph 1
Checking unfeasibility...
Time used: 0.09749

Checking conditional termination of SCC {l2}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.096161s
Ranking function: -1 + arg3
New Graphs: 
Program Terminates