YES

Solver Timeout: 4
Global Timeout: 300
No parsing errors!
Init Location: 0
Transitions:
<l0, l6, true>
<l1, l2, (undef8 > ~(1)) /\ (arg2 > 1) /\ (undef1 > ~(1)) /\ (undef9 > undef2) /\ (undef9 > ~(1)) /\ (arg1 > 0), par{arg1 -> undef1, arg2 -> undef2, arg3 -> undef3, arg4 -> undef4, arg5 -> undef5, arg6 -> undef6, arg7 -> undef7}>
<l1, l2, (undef17 > ~(1)) /\ (arg2 > 1) /\ (undef11 < 1) /\ (undef10 > ~(1)) /\ (arg1 > 0), par{arg1 -> undef10, arg2 -> undef11, arg3 -> undef12, arg4 -> undef13, arg5 -> undef14, arg6 -> undef15, arg7 -> undef16}>
<l2, l3, (arg2 > 0), par{arg2 -> 0, arg3 -> arg2, arg4 -> arg2, arg5 -> 0, arg6 -> arg2, arg7 -> arg2}>
<l3, l4, (undef32 < arg3) /\ (arg3 > 0) /\ (undef33 < arg6) /\ (arg6 > ~(1)) /\ (undef34 > undef35) /\ (undef33 > ~(1)) /\ (undef33 < undef35) /\ (undef34 > ~(1)) /\ (undef36 > undef33) /\ (undef33 < undef32) /\ (arg1 >= undef37) /\ ((arg1 - (2 * undef38)) = 0) /\ (arg3 = arg4) /\ (arg6 = arg7), par{arg4 -> arg3, arg7 -> arg6}>
<l4, l3, (undef42 < arg3) /\ (arg3 > 0) /\ (undef46 < arg6) /\ (arg6 > ~(1)) /\ (undef47 > undef43) /\ (undef46 > ~(1)) /\ (undef46 < undef43) /\ (undef47 > ~(1)) /\ (undef48 > undef46) /\ (undef46 < undef42) /\ ((arg1 - (2 * undef49)) = 0) /\ (arg1 >= undef39) /\ ((arg1 - (2 * undef49)) >= 0) /\ ((arg1 - (2 * undef49)) < 2) /\ ((arg1 - (2 * undef39)) < 2) /\ ((arg1 - (2 * undef39)) >= 0) /\ (arg3 = arg4) /\ (arg6 = arg7), par{arg1 -> undef39, arg2 -> 1, arg3 -> undef41, arg4 -> undef42, arg5 -> undef43, arg6 -> 0, arg7 -> undef43}>
<l3, l4, (arg4 > 0) /\ (arg5 > 0) /\ (arg7 > ~(1)) /\ (undef57 < arg7) /\ (undef58 < arg4) /\ (undef57 < arg5) /\ (arg2 > 0) /\ ((arg1 - (2 * undef59)) = 1) /\ (undef60 > ~(1)) /\ (undef60 > undef58) /\ (arg1 >= undef61) /\ (undef58 > ~(1)) /\ (undef58 >= undef62) /\ (undef57 > 0)>
<l4, l3, (arg4 > 0) /\ (arg5 > 0) /\ (arg7 > ~(1)) /\ (undef67 < arg7) /\ (undef70 < arg4) /\ (undef67 < arg5) /\ (arg2 > 0) /\ ((arg1 - (2 * undef71)) = 1) /\ (undef72 > ~(1)) /\ (undef72 > undef70) /\ (arg1 >= undef63) /\ (undef70 > ~(1)) /\ (undef67 > 0) /\ (undef70 >= undef66) /\ ((arg1 - (2 * undef71)) >= 0) /\ ((arg1 - (2 * undef71)) < 2) /\ ((arg1 - (2 * undef63)) < 2) /\ ((arg1 - (2 * undef63)) >= 0), par{arg1 -> undef63, arg2 -> 1, arg3 -> undef65, arg4 -> undef66, arg5 -> undef67, arg6 -> 0, arg7 -> undef67}>
<l3, l4, (undef80 < arg3) /\ (arg3 > 0) /\ (undef80 < arg6) /\ (arg6 > ~(1)) /\ (undef81 > undef82) /\ (undef81 > ~(1)) /\ ((arg1 - (2 * undef83)) = 1) /\ (undef80 > 0) /\ (arg1 >= undef84) /\ (arg3 = arg4) /\ (arg6 = arg7), par{arg4 -> arg3, arg7 -> arg6}>
<l4, l3, (undef87 < arg3) /\ (arg3 > 0) /\ (undef87 < arg6) /\ (arg6 > ~(1)) /\ (undef92 > undef93) /\ (undef92 > ~(1)) /\ ((arg1 - (2 * undef94)) = 1) /\ (arg1 >= undef85) /\ (undef87 > 0) /\ ((arg1 - (2 * undef94)) >= 0) /\ ((arg1 - (2 * undef94)) < 2) /\ ((arg1 - (2 * undef85)) < 2) /\ ((arg1 - (2 * undef85)) >= 0) /\ (arg3 = arg4) /\ (arg6 = arg7), par{arg1 -> undef85, arg2 -> 0, arg3 -> undef87, arg4 -> undef87, arg5 -> 0, arg6 -> undef87, arg7 -> undef87}>
<l3, l4, (arg4 > 0) /\ (arg5 > 0) /\ (arg6 > ~(1)) /\ (arg6 < arg2) /\ (undef102 > arg6) /\ (arg6 < arg3) /\ (undef103 > arg6) /\ (arg7 > ~(1)) /\ (undef104 < arg7) /\ (undef104 < undef105) /\ (undef106 < arg4) /\ (undef104 > ~(1)) /\ (undef107 > undef104) /\ (undef108 < arg5) /\ (arg2 > 0) /\ (undef104 < undef106) /\ (undef104 < undef108) /\ (arg1 >= undef109) /\ ((arg1 - (2 * undef110)) = 0)>
<l4, l3, (arg4 > 0) /\ (arg5 > 0) /\ (arg6 > ~(1)) /\ (arg6 < arg2) /\ (undef118 > arg6) /\ (arg6 < arg3) /\ (undef119 > arg6) /\ (arg7 > ~(1)) /\ (undef120 < arg7) /\ (undef120 < undef117) /\ (undef114 < arg4) /\ (undef120 > ~(1)) /\ (undef121 > undef120) /\ (undef115 < arg5) /\ (arg2 > 0) /\ (undef120 < undef114) /\ (undef120 < undef115) /\ ((arg1 - (2 * undef122)) = 0) /\ (arg1 >= undef111) /\ ((arg1 - (2 * undef122)) >= 0) /\ ((arg1 - (2 * undef122)) < 2) /\ ((arg1 - (2 * undef111)) < 2) /\ ((arg1 - (2 * undef111)) >= 0), par{arg1 -> undef111, arg2 -> undef112, arg4 -> undef114, arg5 -> undef115, arg6 -> arg2, arg7 -> undef117}>
<l3, l4, (arg4 > 0) /\ (arg5 > 0) /\ (arg7 > ~(1)) /\ (undef130 < arg7) /\ (undef131 < arg4) /\ (undef132 < arg5) /\ (arg2 > 0) /\ ((arg1 - (2 * undef133)) = 1) /\ (arg3 > ~(1)) /\ (undef134 <= arg3) /\ (undef131 >= undef135) /\ (undef131 > ~(1)) /\ (undef132 >= undef136) /\ (arg6 > 0) /\ (arg1 >= undef137) /\ (undef132 > ~(1)) /\ (undef130 > 0)>
<l4, l3, (arg4 > 0) /\ (arg5 > 0) /\ (arg7 > ~(1)) /\ (undef144 < arg7) /\ (undef145 < arg4) /\ (undef146 < arg5) /\ (arg2 > 0) /\ ((arg1 - (2 * undef147)) = 1) /\ (arg3 > ~(1)) /\ (undef140 <= arg3) /\ (undef145 >= undef141) /\ (undef145 > ~(1)) /\ (undef146 >= undef142) /\ (arg6 > 0) /\ (arg1 >= undef138) /\ (undef144 > 0) /\ (undef146 > ~(1)) /\ ((arg1 - (2 * undef147)) >= 0) /\ ((arg1 - (2 * undef147)) < 2) /\ ((arg1 - (2 * undef138)) < 2) /\ ((arg1 - (2 * undef138)) >= 0), par{arg1 -> undef138, arg2 -> undef139, arg3 -> undef140, arg4 -> undef141, arg5 -> undef142, arg7 -> undef144}>
<l3, l4, (undef155 < arg3) /\ (arg3 > 0) /\ (undef156 < arg6) /\ (arg6 > ~(1)) /\ (undef157 < undef158) /\ (undef158 > ~(1)) /\ ((arg1 - (2 * undef159)) = 1) /\ (arg1 >= undef160) /\ (undef155 > ~(1)) /\ (undef155 >= undef161) /\ (undef156 > 0) /\ (arg3 = arg4) /\ (arg6 = arg7), par{arg4 -> arg3, arg7 -> arg6}>
<l4, l3, (undef169 < arg3) /\ (arg3 > 0) /\ (undef168 < arg6) /\ (arg6 > ~(1)) /\ (undef170 < undef171) /\ (undef171 > ~(1)) /\ ((arg1 - (2 * undef172)) = 1) /\ (arg1 >= undef162) /\ (undef169 > ~(1)) /\ (undef168 > 0) /\ (undef169 >= undef165) /\ ((arg1 - (2 * undef172)) >= 0) /\ ((arg1 - (2 * undef172)) < 2) /\ ((arg1 - (2 * undef162)) < 2) /\ ((arg1 - (2 * undef162)) >= 0) /\ (arg3 = arg4) /\ (arg6 = arg7), par{arg1 -> undef162, arg2 -> undef163, arg3 -> undef164, arg4 -> undef165, arg5 -> undef166, arg6 -> undef167, arg7 -> undef168}>
<l1, l5, (undef180 > ~(1)) /\ (arg2 > 1) /\ (undef181 > ~(1)) /\ (arg1 > 0), par{arg1 -> (undef181 - 1), arg2 -> undef174, arg3 -> undef175, arg4 -> undef176, arg5 -> undef177, arg6 -> undef178, arg7 -> undef179}>
<l5, l5, (arg1 > 0), par{arg1 -> (arg1 - 1), arg2 -> undef183, arg3 -> undef184, arg4 -> undef185, arg5 -> undef186, arg6 -> undef187, arg7 -> undef188}>
<l6, l1, true, par{arg1 -> undef189, arg2 -> undef190, arg3 -> undef191, arg4 -> undef192, arg5 -> undef193, arg6 -> undef194, arg7 -> undef195}>

Fresh variables:
undef1, undef2, undef3, undef4, undef5, undef6, undef7, undef8, undef9, undef10, undef11, undef12, undef13, undef14, undef15, undef16, undef17, undef32, undef33, undef34, undef35, undef36, undef37, undef38, undef39, undef41, undef42, undef43, undef46, undef47, undef48, undef49, undef57, undef58, undef59, undef60, undef61, undef62, undef63, undef65, undef66, undef67, undef70, undef71, undef72, undef80, undef81, undef82, undef83, undef84, undef85, undef87, undef92, undef93, undef94, undef102, undef103, undef104, undef105, undef106, undef107, undef108, undef109, undef110, undef111, undef112, undef114, undef115, undef117, undef118, undef119, undef120, undef121, undef122, undef130, undef131, undef132, undef133, undef134, undef135, undef136, undef137, undef138, undef139, undef140, undef141, undef142, undef144, undef145, undef146, undef147, undef155, undef156, undef157, undef158, undef159, undef160, undef161, undef162, undef163, undef164, undef165, undef166, undef167, undef168, undef169, undef170, undef171, undef172, undef174, undef175, undef176, undef177, undef178, undef179, undef180, undef181, undef183, undef184, undef185, undef186, undef187, undef188, undef189, undef190, undef191, undef192, undef193, undef194, undef195, 

Undef variables:
undef1, undef2, undef3, undef4, undef5, undef6, undef7, undef8, undef9, undef10, undef11, undef12, undef13, undef14, undef15, undef16, undef17, undef32, undef33, undef34, undef35, undef36, undef37, undef38, undef39, undef41, undef42, undef43, undef46, undef47, undef48, undef49, undef57, undef58, undef59, undef60, undef61, undef62, undef63, undef65, undef66, undef67, undef70, undef71, undef72, undef80, undef81, undef82, undef83, undef84, undef85, undef87, undef92, undef93, undef94, undef102, undef103, undef104, undef105, undef106, undef107, undef108, undef109, undef110, undef111, undef112, undef114, undef115, undef117, undef118, undef119, undef120, undef121, undef122, undef130, undef131, undef132, undef133, undef134, undef135, undef136, undef137, undef138, undef139, undef140, undef141, undef142, undef144, undef145, undef146, undef147, undef155, undef156, undef157, undef158, undef159, undef160, undef161, undef162, undef163, undef164, undef165, undef166, undef167, undef168, undef169, undef170, undef171, undef172, undef174, undef175, undef176, undef177, undef178, undef179, undef180, undef181, undef183, undef184, undef185, undef186, undef187, undef188, undef189, undef190, undef191, undef192, undef193, undef194, undef195, 

Abstraction variables:

Exit nodes:

Accepting locations:

Asserts:

Preprocessed LLVMGraph
Init Location: 0
Transitions:
<l0, l3, (undef8 > ~(1)) /\ (undef190 > 1) /\ (undef1 > ~(1)) /\ (undef9 > undef2) /\ (undef9 > ~(1)) /\ (undef189 > 0) /\ (undef2 > 0), par{arg1 -> undef1, arg2 -> 0, arg3 -> undef2, arg4 -> undef2, arg5 -> 0, arg6 -> undef2, arg7 -> undef2}>
<l0, l5, (undef180 > ~(1)) /\ (undef190 > 1) /\ (undef181 > ~(1)) /\ (undef189 > 0), par{arg1 -> (undef181 - 1), arg2 -> undef174, arg3 -> undef175, arg4 -> undef176, arg5 -> undef177, arg6 -> undef178, arg7 -> undef179}>
<l3, l3, (undef32 < arg3) /\ (arg3 > 0) /\ (undef33 < arg6) /\ (arg6 > ~(1)) /\ (undef34 > undef35) /\ (undef33 > ~(1)) /\ (undef33 < undef35) /\ (undef34 > ~(1)) /\ (undef36 > undef33) /\ (undef33 < undef32) /\ (arg1 >= undef37) /\ ((arg1 - (2 * undef38)) = 0) /\ (arg3 = arg4) /\ (arg6 = arg7) /\ (undef42 < arg3) /\ (arg3 > 0) /\ (undef46 < arg6) /\ (arg6 > ~(1)) /\ (undef47 > undef43) /\ (undef46 > ~(1)) /\ (undef46 < undef43) /\ (undef47 > ~(1)) /\ (undef48 > undef46) /\ (undef46 < undef42) /\ ((arg1 - (2 * undef49)) = 0) /\ (arg1 >= undef39) /\ ((arg1 - (2 * undef49)) >= 0) /\ ((arg1 - (2 * undef49)) < 2) /\ ((arg1 - (2 * undef39)) < 2) /\ ((arg1 - (2 * undef39)) >= 0) /\ (arg3 = arg3) /\ (arg6 = arg6), par{arg1 -> undef39, arg2 -> 1, arg3 -> undef41, arg4 -> undef42, arg5 -> undef43, arg6 -> 0, arg7 -> undef43}>
<l3, l3, (undef32 < arg3) /\ (arg3 > 0) /\ (undef33 < arg6) /\ (arg6 > ~(1)) /\ (undef34 > undef35) /\ (undef33 > ~(1)) /\ (undef33 < undef35) /\ (undef34 > ~(1)) /\ (undef36 > undef33) /\ (undef33 < undef32) /\ (arg1 >= undef37) /\ ((arg1 - (2 * undef38)) = 0) /\ (arg3 = arg4) /\ (arg6 = arg7) /\ (arg3 > 0) /\ (arg5 > 0) /\ (arg6 > ~(1)) /\ (arg6 < arg2) /\ (undef118 > arg6) /\ (arg6 < arg3) /\ (undef119 > arg6) /\ (arg6 > ~(1)) /\ (undef120 < arg6) /\ (undef120 < undef117) /\ (undef114 < arg3) /\ (undef120 > ~(1)) /\ (undef121 > undef120) /\ (undef115 < arg5) /\ (arg2 > 0) /\ (undef120 < undef114) /\ (undef120 < undef115) /\ ((arg1 - (2 * undef122)) = 0) /\ (arg1 >= undef111) /\ ((arg1 - (2 * undef122)) >= 0) /\ ((arg1 - (2 * undef122)) < 2) /\ ((arg1 - (2 * undef111)) < 2) /\ ((arg1 - (2 * undef111)) >= 0), par{arg1 -> undef111, arg2 -> undef112, arg4 -> undef114, arg5 -> undef115, arg6 -> arg2, arg7 -> undef117}>
<l3, l3, (arg4 > 0) /\ (arg5 > 0) /\ (arg7 > ~(1)) /\ (undef57 < arg7) /\ (undef58 < arg4) /\ (undef57 < arg5) /\ (arg2 > 0) /\ ((arg1 - (2 * undef59)) = 1) /\ (undef60 > ~(1)) /\ (undef60 > undef58) /\ (arg1 >= undef61) /\ (undef58 > ~(1)) /\ (undef58 >= undef62) /\ (undef57 > 0) /\ (arg4 > 0) /\ (arg5 > 0) /\ (arg7 > ~(1)) /\ (undef67 < arg7) /\ (undef70 < arg4) /\ (undef67 < arg5) /\ (arg2 > 0) /\ ((arg1 - (2 * undef71)) = 1) /\ (undef72 > ~(1)) /\ (undef72 > undef70) /\ (arg1 >= undef63) /\ (undef70 > ~(1)) /\ (undef67 > 0) /\ (undef70 >= undef66) /\ ((arg1 - (2 * undef71)) >= 0) /\ ((arg1 - (2 * undef71)) < 2) /\ ((arg1 - (2 * undef63)) < 2) /\ ((arg1 - (2 * undef63)) >= 0), par{arg1 -> undef63, arg2 -> 1, arg3 -> undef65, arg4 -> undef66, arg5 -> undef67, arg6 -> 0, arg7 -> undef67}>
<l3, l3, (arg4 > 0) /\ (arg5 > 0) /\ (arg7 > ~(1)) /\ (undef57 < arg7) /\ (undef58 < arg4) /\ (undef57 < arg5) /\ (arg2 > 0) /\ ((arg1 - (2 * undef59)) = 1) /\ (undef60 > ~(1)) /\ (undef60 > undef58) /\ (arg1 >= undef61) /\ (undef58 > ~(1)) /\ (undef58 >= undef62) /\ (undef57 > 0) /\ (undef87 < arg3) /\ (arg3 > 0) /\ (undef87 < arg6) /\ (arg6 > ~(1)) /\ (undef92 > undef93) /\ (undef92 > ~(1)) /\ ((arg1 - (2 * undef94)) = 1) /\ (arg1 >= undef85) /\ (undef87 > 0) /\ ((arg1 - (2 * undef94)) >= 0) /\ ((arg1 - (2 * undef94)) < 2) /\ ((arg1 - (2 * undef85)) < 2) /\ ((arg1 - (2 * undef85)) >= 0) /\ (arg3 = arg4) /\ (arg6 = arg7), par{arg1 -> undef85, arg2 -> 0, arg3 -> undef87, arg4 -> undef87, arg5 -> 0, arg6 -> undef87, arg7 -> undef87}>
<l3, l3, (arg4 > 0) /\ (arg5 > 0) /\ (arg7 > ~(1)) /\ (undef57 < arg7) /\ (undef58 < arg4) /\ (undef57 < arg5) /\ (arg2 > 0) /\ ((arg1 - (2 * undef59)) = 1) /\ (undef60 > ~(1)) /\ (undef60 > undef58) /\ (arg1 >= undef61) /\ (undef58 > ~(1)) /\ (undef58 >= undef62) /\ (undef57 > 0) /\ (arg4 > 0) /\ (arg5 > 0) /\ (arg7 > ~(1)) /\ (undef144 < arg7) /\ (undef145 < arg4) /\ (undef146 < arg5) /\ (arg2 > 0) /\ ((arg1 - (2 * undef147)) = 1) /\ (arg3 > ~(1)) /\ (undef140 <= arg3) /\ (undef145 >= undef141) /\ (undef145 > ~(1)) /\ (undef146 >= undef142) /\ (arg6 > 0) /\ (arg1 >= undef138) /\ (undef144 > 0) /\ (undef146 > ~(1)) /\ ((arg1 - (2 * undef147)) >= 0) /\ ((arg1 - (2 * undef147)) < 2) /\ ((arg1 - (2 * undef138)) < 2) /\ ((arg1 - (2 * undef138)) >= 0), par{arg1 -> undef138, arg2 -> undef139, arg3 -> undef140, arg4 -> undef141, arg5 -> undef142, arg7 -> undef144}>
<l3, l3, (arg4 > 0) /\ (arg5 > 0) /\ (arg7 > ~(1)) /\ (undef57 < arg7) /\ (undef58 < arg4) /\ (undef57 < arg5) /\ (arg2 > 0) /\ ((arg1 - (2 * undef59)) = 1) /\ (undef60 > ~(1)) /\ (undef60 > undef58) /\ (arg1 >= undef61) /\ (undef58 > ~(1)) /\ (undef58 >= undef62) /\ (undef57 > 0) /\ (undef169 < arg3) /\ (arg3 > 0) /\ (undef168 < arg6) /\ (arg6 > ~(1)) /\ (undef170 < undef171) /\ (undef171 > ~(1)) /\ ((arg1 - (2 * undef172)) = 1) /\ (arg1 >= undef162) /\ (undef169 > ~(1)) /\ (undef168 > 0) /\ (undef169 >= undef165) /\ ((arg1 - (2 * undef172)) >= 0) /\ ((arg1 - (2 * undef172)) < 2) /\ ((arg1 - (2 * undef162)) < 2) /\ ((arg1 - (2 * undef162)) >= 0) /\ (arg3 = arg4) /\ (arg6 = arg7), par{arg1 -> undef162, arg2 -> undef163, arg3 -> undef164, arg4 -> undef165, arg5 -> undef166, arg6 -> undef167, arg7 -> undef168}>
<l3, l3, (undef80 < arg3) /\ (arg3 > 0) /\ (undef80 < arg6) /\ (arg6 > ~(1)) /\ (undef81 > undef82) /\ (undef81 > ~(1)) /\ ((arg1 - (2 * undef83)) = 1) /\ (undef80 > 0) /\ (arg1 >= undef84) /\ (arg3 = arg4) /\ (arg6 = arg7) /\ (arg3 > 0) /\ (arg5 > 0) /\ (arg6 > ~(1)) /\ (undef67 < arg6) /\ (undef70 < arg3) /\ (undef67 < arg5) /\ (arg2 > 0) /\ ((arg1 - (2 * undef71)) = 1) /\ (undef72 > ~(1)) /\ (undef72 > undef70) /\ (arg1 >= undef63) /\ (undef70 > ~(1)) /\ (undef67 > 0) /\ (undef70 >= undef66) /\ ((arg1 - (2 * undef71)) >= 0) /\ ((arg1 - (2 * undef71)) < 2) /\ ((arg1 - (2 * undef63)) < 2) /\ ((arg1 - (2 * undef63)) >= 0), par{arg1 -> undef63, arg2 -> 1, arg3 -> undef65, arg4 -> undef66, arg5 -> undef67, arg6 -> 0, arg7 -> undef67}>
<l3, l3, (undef80 < arg3) /\ (arg3 > 0) /\ (undef80 < arg6) /\ (arg6 > ~(1)) /\ (undef81 > undef82) /\ (undef81 > ~(1)) /\ ((arg1 - (2 * undef83)) = 1) /\ (undef80 > 0) /\ (arg1 >= undef84) /\ (arg3 = arg4) /\ (arg6 = arg7) /\ (undef87 < arg3) /\ (arg3 > 0) /\ (undef87 < arg6) /\ (arg6 > ~(1)) /\ (undef92 > undef93) /\ (undef92 > ~(1)) /\ ((arg1 - (2 * undef94)) = 1) /\ (arg1 >= undef85) /\ (undef87 > 0) /\ ((arg1 - (2 * undef94)) >= 0) /\ ((arg1 - (2 * undef94)) < 2) /\ ((arg1 - (2 * undef85)) < 2) /\ ((arg1 - (2 * undef85)) >= 0) /\ (arg3 = arg3) /\ (arg6 = arg6), par{arg1 -> undef85, arg2 -> 0, arg3 -> undef87, arg4 -> undef87, arg5 -> 0, arg6 -> undef87, arg7 -> undef87}>
<l3, l3, (undef80 < arg3) /\ (arg3 > 0) /\ (undef80 < arg6) /\ (arg6 > ~(1)) /\ (undef81 > undef82) /\ (undef81 > ~(1)) /\ ((arg1 - (2 * undef83)) = 1) /\ (undef80 > 0) /\ (arg1 >= undef84) /\ (arg3 = arg4) /\ (arg6 = arg7) /\ (arg3 > 0) /\ (arg5 > 0) /\ (arg6 > ~(1)) /\ (undef144 < arg6) /\ (undef145 < arg3) /\ (undef146 < arg5) /\ (arg2 > 0) /\ ((arg1 - (2 * undef147)) = 1) /\ (arg3 > ~(1)) /\ (undef140 <= arg3) /\ (undef145 >= undef141) /\ (undef145 > ~(1)) /\ (undef146 >= undef142) /\ (arg6 > 0) /\ (arg1 >= undef138) /\ (undef144 > 0) /\ (undef146 > ~(1)) /\ ((arg1 - (2 * undef147)) >= 0) /\ ((arg1 - (2 * undef147)) < 2) /\ ((arg1 - (2 * undef138)) < 2) /\ ((arg1 - (2 * undef138)) >= 0), par{arg1 -> undef138, arg2 -> undef139, arg3 -> undef140, arg4 -> undef141, arg5 -> undef142, arg7 -> undef144}>
<l3, l3, (undef80 < arg3) /\ (arg3 > 0) /\ (undef80 < arg6) /\ (arg6 > ~(1)) /\ (undef81 > undef82) /\ (undef81 > ~(1)) /\ ((arg1 - (2 * undef83)) = 1) /\ (undef80 > 0) /\ (arg1 >= undef84) /\ (arg3 = arg4) /\ (arg6 = arg7) /\ (undef169 < arg3) /\ (arg3 > 0) /\ (undef168 < arg6) /\ (arg6 > ~(1)) /\ (undef170 < undef171) /\ (undef171 > ~(1)) /\ ((arg1 - (2 * undef172)) = 1) /\ (arg1 >= undef162) /\ (undef169 > ~(1)) /\ (undef168 > 0) /\ (undef169 >= undef165) /\ ((arg1 - (2 * undef172)) >= 0) /\ ((arg1 - (2 * undef172)) < 2) /\ ((arg1 - (2 * undef162)) < 2) /\ ((arg1 - (2 * undef162)) >= 0) /\ (arg3 = arg3) /\ (arg6 = arg6), par{arg1 -> undef162, arg2 -> undef163, arg3 -> undef164, arg4 -> undef165, arg5 -> undef166, arg6 -> undef167, arg7 -> undef168}>
<l3, l3, (arg4 > 0) /\ (arg5 > 0) /\ (arg6 > ~(1)) /\ (arg6 < arg2) /\ (undef102 > arg6) /\ (arg6 < arg3) /\ (undef103 > arg6) /\ (arg7 > ~(1)) /\ (undef104 < arg7) /\ (undef104 < undef105) /\ (undef106 < arg4) /\ (undef104 > ~(1)) /\ (undef107 > undef104) /\ (undef108 < arg5) /\ (arg2 > 0) /\ (undef104 < undef106) /\ (undef104 < undef108) /\ (arg1 >= undef109) /\ ((arg1 - (2 * undef110)) = 0) /\ (undef42 < arg3) /\ (arg3 > 0) /\ (undef46 < arg6) /\ (arg6 > ~(1)) /\ (undef47 > undef43) /\ (undef46 > ~(1)) /\ (undef46 < undef43) /\ (undef47 > ~(1)) /\ (undef48 > undef46) /\ (undef46 < undef42) /\ ((arg1 - (2 * undef49)) = 0) /\ (arg1 >= undef39) /\ ((arg1 - (2 * undef49)) >= 0) /\ ((arg1 - (2 * undef49)) < 2) /\ ((arg1 - (2 * undef39)) < 2) /\ ((arg1 - (2 * undef39)) >= 0) /\ (arg3 = arg4) /\ (arg6 = arg7), par{arg1 -> undef39, arg2 -> 1, arg3 -> undef41, arg4 -> undef42, arg5 -> undef43, arg6 -> 0, arg7 -> undef43}>
<l3, l3, (arg4 > 0) /\ (arg5 > 0) /\ (arg6 > ~(1)) /\ (arg6 < arg2) /\ (undef102 > arg6) /\ (arg6 < arg3) /\ (undef103 > arg6) /\ (arg7 > ~(1)) /\ (undef104 < arg7) /\ (undef104 < undef105) /\ (undef106 < arg4) /\ (undef104 > ~(1)) /\ (undef107 > undef104) /\ (undef108 < arg5) /\ (arg2 > 0) /\ (undef104 < undef106) /\ (undef104 < undef108) /\ (arg1 >= undef109) /\ ((arg1 - (2 * undef110)) = 0) /\ (arg4 > 0) /\ (arg5 > 0) /\ (arg6 > ~(1)) /\ (arg6 < arg2) /\ (undef118 > arg6) /\ (arg6 < arg3) /\ (undef119 > arg6) /\ (arg7 > ~(1)) /\ (undef120 < arg7) /\ (undef120 < undef117) /\ (undef114 < arg4) /\ (undef120 > ~(1)) /\ (undef121 > undef120) /\ (undef115 < arg5) /\ (arg2 > 0) /\ (undef120 < undef114) /\ (undef120 < undef115) /\ ((arg1 - (2 * undef122)) = 0) /\ (arg1 >= undef111) /\ ((arg1 - (2 * undef122)) >= 0) /\ ((arg1 - (2 * undef122)) < 2) /\ ((arg1 - (2 * undef111)) < 2) /\ ((arg1 - (2 * undef111)) >= 0), par{arg1 -> undef111, arg2 -> undef112, arg4 -> undef114, arg5 -> undef115, arg6 -> arg2, arg7 -> undef117}>
<l3, l3, (arg4 > 0) /\ (arg5 > 0) /\ (arg7 > ~(1)) /\ (undef130 < arg7) /\ (undef131 < arg4) /\ (undef132 < arg5) /\ (arg2 > 0) /\ ((arg1 - (2 * undef133)) = 1) /\ (arg3 > ~(1)) /\ (undef134 <= arg3) /\ (undef131 >= undef135) /\ (undef131 > ~(1)) /\ (undef132 >= undef136) /\ (arg6 > 0) /\ (arg1 >= undef137) /\ (undef132 > ~(1)) /\ (undef130 > 0) /\ (arg4 > 0) /\ (arg5 > 0) /\ (arg7 > ~(1)) /\ (undef67 < arg7) /\ (undef70 < arg4) /\ (undef67 < arg5) /\ (arg2 > 0) /\ ((arg1 - (2 * undef71)) = 1) /\ (undef72 > ~(1)) /\ (undef72 > undef70) /\ (arg1 >= undef63) /\ (undef70 > ~(1)) /\ (undef67 > 0) /\ (undef70 >= undef66) /\ ((arg1 - (2 * undef71)) >= 0) /\ ((arg1 - (2 * undef71)) < 2) /\ ((arg1 - (2 * undef63)) < 2) /\ ((arg1 - (2 * undef63)) >= 0), par{arg1 -> undef63, arg2 -> 1, arg3 -> undef65, arg4 -> undef66, arg5 -> undef67, arg6 -> 0, arg7 -> undef67}>
<l3, l3, (arg4 > 0) /\ (arg5 > 0) /\ (arg7 > ~(1)) /\ (undef130 < arg7) /\ (undef131 < arg4) /\ (undef132 < arg5) /\ (arg2 > 0) /\ ((arg1 - (2 * undef133)) = 1) /\ (arg3 > ~(1)) /\ (undef134 <= arg3) /\ (undef131 >= undef135) /\ (undef131 > ~(1)) /\ (undef132 >= undef136) /\ (arg6 > 0) /\ (arg1 >= undef137) /\ (undef132 > ~(1)) /\ (undef130 > 0) /\ (undef87 < arg3) /\ (arg3 > 0) /\ (undef87 < arg6) /\ (arg6 > ~(1)) /\ (undef92 > undef93) /\ (undef92 > ~(1)) /\ ((arg1 - (2 * undef94)) = 1) /\ (arg1 >= undef85) /\ (undef87 > 0) /\ ((arg1 - (2 * undef94)) >= 0) /\ ((arg1 - (2 * undef94)) < 2) /\ ((arg1 - (2 * undef85)) < 2) /\ ((arg1 - (2 * undef85)) >= 0) /\ (arg3 = arg4) /\ (arg6 = arg7), par{arg1 -> undef85, arg2 -> 0, arg3 -> undef87, arg4 -> undef87, arg5 -> 0, arg6 -> undef87, arg7 -> undef87}>
<l3, l3, (arg4 > 0) /\ (arg5 > 0) /\ (arg7 > ~(1)) /\ (undef130 < arg7) /\ (undef131 < arg4) /\ (undef132 < arg5) /\ (arg2 > 0) /\ ((arg1 - (2 * undef133)) = 1) /\ (arg3 > ~(1)) /\ (undef134 <= arg3) /\ (undef131 >= undef135) /\ (undef131 > ~(1)) /\ (undef132 >= undef136) /\ (arg6 > 0) /\ (arg1 >= undef137) /\ (undef132 > ~(1)) /\ (undef130 > 0) /\ (arg4 > 0) /\ (arg5 > 0) /\ (arg7 > ~(1)) /\ (undef144 < arg7) /\ (undef145 < arg4) /\ (undef146 < arg5) /\ (arg2 > 0) /\ ((arg1 - (2 * undef147)) = 1) /\ (arg3 > ~(1)) /\ (undef140 <= arg3) /\ (undef145 >= undef141) /\ (undef145 > ~(1)) /\ (undef146 >= undef142) /\ (arg6 > 0) /\ (arg1 >= undef138) /\ (undef144 > 0) /\ (undef146 > ~(1)) /\ ((arg1 - (2 * undef147)) >= 0) /\ ((arg1 - (2 * undef147)) < 2) /\ ((arg1 - (2 * undef138)) < 2) /\ ((arg1 - (2 * undef138)) >= 0), par{arg1 -> undef138, arg2 -> undef139, arg3 -> undef140, arg4 -> undef141, arg5 -> undef142, arg7 -> undef144}>
<l3, l3, (arg4 > 0) /\ (arg5 > 0) /\ (arg7 > ~(1)) /\ (undef130 < arg7) /\ (undef131 < arg4) /\ (undef132 < arg5) /\ (arg2 > 0) /\ ((arg1 - (2 * undef133)) = 1) /\ (arg3 > ~(1)) /\ (undef134 <= arg3) /\ (undef131 >= undef135) /\ (undef131 > ~(1)) /\ (undef132 >= undef136) /\ (arg6 > 0) /\ (arg1 >= undef137) /\ (undef132 > ~(1)) /\ (undef130 > 0) /\ (undef169 < arg3) /\ (arg3 > 0) /\ (undef168 < arg6) /\ (arg6 > ~(1)) /\ (undef170 < undef171) /\ (undef171 > ~(1)) /\ ((arg1 - (2 * undef172)) = 1) /\ (arg1 >= undef162) /\ (undef169 > ~(1)) /\ (undef168 > 0) /\ (undef169 >= undef165) /\ ((arg1 - (2 * undef172)) >= 0) /\ ((arg1 - (2 * undef172)) < 2) /\ ((arg1 - (2 * undef162)) < 2) /\ ((arg1 - (2 * undef162)) >= 0) /\ (arg3 = arg4) /\ (arg6 = arg7), par{arg1 -> undef162, arg2 -> undef163, arg3 -> undef164, arg4 -> undef165, arg5 -> undef166, arg6 -> undef167, arg7 -> undef168}>
<l3, l3, (undef155 < arg3) /\ (arg3 > 0) /\ (undef156 < arg6) /\ (arg6 > ~(1)) /\ (undef157 < undef158) /\ (undef158 > ~(1)) /\ ((arg1 - (2 * undef159)) = 1) /\ (arg1 >= undef160) /\ (undef155 > ~(1)) /\ (undef155 >= undef161) /\ (undef156 > 0) /\ (arg3 = arg4) /\ (arg6 = arg7) /\ (arg3 > 0) /\ (arg5 > 0) /\ (arg6 > ~(1)) /\ (undef67 < arg6) /\ (undef70 < arg3) /\ (undef67 < arg5) /\ (arg2 > 0) /\ ((arg1 - (2 * undef71)) = 1) /\ (undef72 > ~(1)) /\ (undef72 > undef70) /\ (arg1 >= undef63) /\ (undef70 > ~(1)) /\ (undef67 > 0) /\ (undef70 >= undef66) /\ ((arg1 - (2 * undef71)) >= 0) /\ ((arg1 - (2 * undef71)) < 2) /\ ((arg1 - (2 * undef63)) < 2) /\ ((arg1 - (2 * undef63)) >= 0), par{arg1 -> undef63, arg2 -> 1, arg3 -> undef65, arg4 -> undef66, arg5 -> undef67, arg6 -> 0, arg7 -> undef67}>
<l3, l3, (undef155 < arg3) /\ (arg3 > 0) /\ (undef156 < arg6) /\ (arg6 > ~(1)) /\ (undef157 < undef158) /\ (undef158 > ~(1)) /\ ((arg1 - (2 * undef159)) = 1) /\ (arg1 >= undef160) /\ (undef155 > ~(1)) /\ (undef155 >= undef161) /\ (undef156 > 0) /\ (arg3 = arg4) /\ (arg6 = arg7) /\ (undef87 < arg3) /\ (arg3 > 0) /\ (undef87 < arg6) /\ (arg6 > ~(1)) /\ (undef92 > undef93) /\ (undef92 > ~(1)) /\ ((arg1 - (2 * undef94)) = 1) /\ (arg1 >= undef85) /\ (undef87 > 0) /\ ((arg1 - (2 * undef94)) >= 0) /\ ((arg1 - (2 * undef94)) < 2) /\ ((arg1 - (2 * undef85)) < 2) /\ ((arg1 - (2 * undef85)) >= 0) /\ (arg3 = arg3) /\ (arg6 = arg6), par{arg1 -> undef85, arg2 -> 0, arg3 -> undef87, arg4 -> undef87, arg5 -> 0, arg6 -> undef87, arg7 -> undef87}>
<l3, l3, (undef155 < arg3) /\ (arg3 > 0) /\ (undef156 < arg6) /\ (arg6 > ~(1)) /\ (undef157 < undef158) /\ (undef158 > ~(1)) /\ ((arg1 - (2 * undef159)) = 1) /\ (arg1 >= undef160) /\ (undef155 > ~(1)) /\ (undef155 >= undef161) /\ (undef156 > 0) /\ (arg3 = arg4) /\ (arg6 = arg7) /\ (arg3 > 0) /\ (arg5 > 0) /\ (arg6 > ~(1)) /\ (undef144 < arg6) /\ (undef145 < arg3) /\ (undef146 < arg5) /\ (arg2 > 0) /\ ((arg1 - (2 * undef147)) = 1) /\ (arg3 > ~(1)) /\ (undef140 <= arg3) /\ (undef145 >= undef141) /\ (undef145 > ~(1)) /\ (undef146 >= undef142) /\ (arg6 > 0) /\ (arg1 >= undef138) /\ (undef144 > 0) /\ (undef146 > ~(1)) /\ ((arg1 - (2 * undef147)) >= 0) /\ ((arg1 - (2 * undef147)) < 2) /\ ((arg1 - (2 * undef138)) < 2) /\ ((arg1 - (2 * undef138)) >= 0), par{arg1 -> undef138, arg2 -> undef139, arg3 -> undef140, arg4 -> undef141, arg5 -> undef142, arg7 -> undef144}>
<l3, l3, (undef155 < arg3) /\ (arg3 > 0) /\ (undef156 < arg6) /\ (arg6 > ~(1)) /\ (undef157 < undef158) /\ (undef158 > ~(1)) /\ ((arg1 - (2 * undef159)) = 1) /\ (arg1 >= undef160) /\ (undef155 > ~(1)) /\ (undef155 >= undef161) /\ (undef156 > 0) /\ (arg3 = arg4) /\ (arg6 = arg7) /\ (undef169 < arg3) /\ (arg3 > 0) /\ (undef168 < arg6) /\ (arg6 > ~(1)) /\ (undef170 < undef171) /\ (undef171 > ~(1)) /\ ((arg1 - (2 * undef172)) = 1) /\ (arg1 >= undef162) /\ (undef169 > ~(1)) /\ (undef168 > 0) /\ (undef169 >= undef165) /\ ((arg1 - (2 * undef172)) >= 0) /\ ((arg1 - (2 * undef172)) < 2) /\ ((arg1 - (2 * undef162)) < 2) /\ ((arg1 - (2 * undef162)) >= 0) /\ (arg3 = arg3) /\ (arg6 = arg6), par{arg1 -> undef162, arg2 -> undef163, arg3 -> undef164, arg4 -> undef165, arg5 -> undef166, arg6 -> undef167, arg7 -> undef168}>
<l5, l5, (arg1 > 0), par{arg1 -> (arg1 - 1), arg2 -> undef183, arg3 -> undef184, arg4 -> undef185, arg5 -> undef186, arg6 -> undef187, arg7 -> undef188}>

Fresh variables:
undef1, undef2, undef3, undef4, undef5, undef6, undef7, undef8, undef9, undef10, undef11, undef12, undef13, undef14, undef15, undef16, undef17, undef32, undef33, undef34, undef35, undef36, undef37, undef38, undef39, undef41, undef42, undef43, undef46, undef47, undef48, undef49, undef57, undef58, undef59, undef60, undef61, undef62, undef63, undef65, undef66, undef67, undef70, undef71, undef72, undef80, undef81, undef82, undef83, undef84, undef85, undef87, undef92, undef93, undef94, undef102, undef103, undef104, undef105, undef106, undef107, undef108, undef109, undef110, undef111, undef112, undef114, undef115, undef117, undef118, undef119, undef120, undef121, undef122, undef130, undef131, undef132, undef133, undef134, undef135, undef136, undef137, undef138, undef139, undef140, undef141, undef142, undef144, undef145, undef146, undef147, undef155, undef156, undef157, undef158, undef159, undef160, undef161, undef162, undef163, undef164, undef165, undef166, undef167, undef168, undef169, undef170, undef171, undef172, undef174, undef175, undef176, undef177, undef178, undef179, undef180, undef181, undef183, undef184, undef185, undef186, undef187, undef188, undef189, undef190, undef191, undef192, undef193, undef194, undef195, 

Undef variables:
undef1, undef2, undef3, undef4, undef5, undef6, undef7, undef8, undef9, undef10, undef11, undef12, undef13, undef14, undef15, undef16, undef17, undef32, undef33, undef34, undef35, undef36, undef37, undef38, undef39, undef41, undef42, undef43, undef46, undef47, undef48, undef49, undef57, undef58, undef59, undef60, undef61, undef62, undef63, undef65, undef66, undef67, undef70, undef71, undef72, undef80, undef81, undef82, undef83, undef84, undef85, undef87, undef92, undef93, undef94, undef102, undef103, undef104, undef105, undef106, undef107, undef108, undef109, undef110, undef111, undef112, undef114, undef115, undef117, undef118, undef119, undef120, undef121, undef122, undef130, undef131, undef132, undef133, undef134, undef135, undef136, undef137, undef138, undef139, undef140, undef141, undef142, undef144, undef145, undef146, undef147, undef155, undef156, undef157, undef158, undef159, undef160, undef161, undef162, undef163, undef164, undef165, undef166, undef167, undef168, undef169, undef170, undef171, undef172, undef174, undef175, undef176, undef177, undef178, undef179, undef180, undef181, undef183, undef184, undef185, undef186, undef187, undef188, undef189, undef190, undef191, undef192, undef193, undef194, undef195, 

Abstraction variables:

Exit nodes:

Accepting locations:

Asserts:

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

Init Location: 0
Graph 0:
Transitions:
Variables:

Graph 1:
Transitions:
<l5, l5, 1 <= arg1, {arg1 -> -1 + arg1, arg2 -> undef183, arg3 -> undef184, arg4 -> undef185, arg5 -> undef186, arg6 -> undef187, arg7 -> undef188, rest remain the same}>
Variables:
arg1, arg2, arg3, arg4, arg5, arg6, arg7

Graph 2:
Transitions:
<l3, l3, 1 <= arg3 /\ 1 + undef32 <= arg3 /\ 1 + undef42 <= arg3 /\ 1 + undef33 <= arg6 /\ 1 + undef46 <= arg6 /\ 1 + undef33 <= undef32 /\ 1 + undef33 <= undef35 /\ 1 + undef33 <= undef36 /\ 1 + undef35 <= undef34 /\ 1 + undef46 <= undef42 /\ 1 + undef43 <= undef47 /\ 1 + undef46 <= undef43 /\ 1 + undef46 <= undef48 /\ arg1 <= 1 + 2*undef39 /\ undef37 <= arg1 /\ undef39 <= arg1 /\ 2*undef39 <= arg1 /\ 0 <= arg6 /\ 0 <= undef33 /\ 0 <= undef34 /\ 0 <= undef46 /\ 0 <= undef47 /\ arg1 = 2*undef38 /\ arg1 = 2*undef49 /\ arg3 = arg4 /\ arg6 = arg7, {arg1 -> undef39, arg2 -> 1, arg3 -> undef41, arg4 -> undef42, arg5 -> undef43, arg6 -> 0, arg7 -> undef43, rest remain the same}>
<l3, l3, 1 <= arg2 /\ 1 + arg6 <= arg2 /\ 1 <= arg3 /\ 1 + arg6 <= arg3 /\ 1 + undef32 <= arg3 /\ 1 + undef114 <= arg3 /\ 1 <= arg5 /\ 1 + undef115 <= arg5 /\ 1 + arg6 <= undef118 /\ 1 + arg6 <= undef119 /\ 1 + undef33 <= arg6 /\ 1 + undef120 <= arg6 /\ 1 + undef33 <= undef32 /\ 1 + undef33 <= undef35 /\ 1 + undef33 <= undef36 /\ 1 + undef35 <= undef34 /\ 1 + undef120 <= undef114 /\ 1 + undef120 <= undef115 /\ 1 + undef120 <= undef117 /\ 1 + undef120 <= undef121 /\ arg1 <= 1 + 2*undef111 /\ undef37 <= arg1 /\ undef111 <= arg1 /\ 2*undef111 <= arg1 /\ 0 <= arg6 /\ 0 <= undef33 /\ 0 <= undef34 /\ 0 <= undef120 /\ arg1 = 2*undef38 /\ arg1 = 2*undef122 /\ arg3 = arg4 /\ arg6 = arg7, {arg1 -> undef111, arg2 -> undef112, arg4 -> undef114, arg5 -> undef115, arg6 -> arg2, arg7 -> undef117, rest remain the same}>
<l3, l3, 1 <= arg2 /\ 1 <= arg4 /\ 1 + undef58 <= arg4 /\ 1 + undef70 <= arg4 /\ 1 <= arg5 /\ 1 + undef57 <= arg5 /\ 1 + undef67 <= arg5 /\ 1 + undef57 <= arg7 /\ 1 + undef67 <= arg7 /\ 1 <= undef57 /\ 1 + undef58 <= undef60 /\ 1 <= undef67 /\ 1 + undef70 <= undef72 /\ arg1 <= 1 + 2*undef63 /\ undef61 <= arg1 /\ undef63 <= arg1 /\ 2*undef63 <= arg1 /\ 0 <= arg7 /\ 0 <= undef58 /\ undef62 <= undef58 /\ 0 <= undef60 /\ undef66 <= undef70 /\ 0 <= undef70 /\ 0 <= undef72 /\ arg1 = 1 + 2*undef59 /\ arg1 = 1 + 2*undef71, {arg1 -> undef63, arg2 -> 1, arg3 -> undef65, arg4 -> undef66, arg5 -> undef67, arg6 -> 0, arg7 -> undef67, rest remain the same}>
<l3, l3, 1 <= arg2 /\ 1 <= arg3 /\ 1 + undef87 <= arg3 /\ 1 <= arg4 /\ 1 + undef58 <= arg4 /\ 1 <= arg5 /\ 1 + undef57 <= arg5 /\ 1 + undef87 <= arg6 /\ 1 + undef57 <= arg7 /\ 1 <= undef57 /\ 1 + undef58 <= undef60 /\ 1 <= undef87 /\ 1 + undef93 <= undef92 /\ arg1 <= 1 + 2*undef85 /\ undef61 <= arg1 /\ undef85 <= arg1 /\ 2*undef85 <= arg1 /\ 0 <= arg6 /\ 0 <= arg7 /\ 0 <= undef58 /\ undef62 <= undef58 /\ 0 <= undef60 /\ 0 <= undef92 /\ arg1 = 1 + 2*undef59 /\ arg1 = 1 + 2*undef94 /\ arg3 = arg4 /\ arg6 = arg7, {arg1 -> undef85, arg2 -> 0, arg3 -> undef87, arg4 -> undef87, arg5 -> 0, arg6 -> undef87, arg7 -> undef87, rest remain the same}>
<l3, l3, 1 <= arg2 /\ 1 <= arg4 /\ 1 + undef58 <= arg4 /\ 1 + undef145 <= arg4 /\ 1 <= arg5 /\ 1 + undef57 <= arg5 /\ 1 + undef146 <= arg5 /\ 1 <= arg6 /\ 1 + undef57 <= arg7 /\ 1 + undef144 <= arg7 /\ 1 <= undef57 /\ 1 + undef58 <= undef60 /\ 1 <= undef144 /\ arg1 <= 1 + 2*undef138 /\ undef61 <= arg1 /\ undef138 <= arg1 /\ 2*undef138 <= arg1 /\ 0 <= arg3 /\ undef140 <= arg3 /\ 0 <= arg7 /\ 0 <= undef58 /\ undef62 <= undef58 /\ 0 <= undef60 /\ undef141 <= undef145 /\ undef142 <= undef146 /\ 0 <= undef145 /\ 0 <= undef146 /\ arg1 = 1 + 2*undef59 /\ arg1 = 1 + 2*undef147, {arg1 -> undef138, arg2 -> undef139, arg3 -> undef140, arg4 -> undef141, arg5 -> undef142, arg7 -> undef144, rest remain the same}>
<l3, l3, 1 <= arg2 /\ 1 <= arg3 /\ 1 + undef169 <= arg3 /\ 1 <= arg4 /\ 1 + undef58 <= arg4 /\ 1 <= arg5 /\ 1 + undef57 <= arg5 /\ 1 + undef168 <= arg6 /\ 1 + undef57 <= arg7 /\ 1 <= undef57 /\ 1 + undef58 <= undef60 /\ 1 <= undef168 /\ 1 + undef170 <= undef171 /\ arg1 <= 1 + 2*undef162 /\ undef61 <= arg1 /\ undef162 <= arg1 /\ 2*undef162 <= arg1 /\ 0 <= arg6 /\ 0 <= arg7 /\ 0 <= undef58 /\ undef62 <= undef58 /\ 0 <= undef60 /\ undef165 <= undef169 /\ 0 <= undef169 /\ 0 <= undef171 /\ arg1 = 1 + 2*undef59 /\ arg1 = 1 + 2*undef172 /\ arg3 = arg4 /\ arg6 = arg7, {arg1 -> undef162, arg2 -> undef163, arg3 -> undef164, arg4 -> undef165, arg5 -> undef166, arg6 -> undef167, arg7 -> undef168, rest remain the same}>
<l3, l3, 1 <= arg2 /\ 1 <= arg3 /\ 1 + undef70 <= arg3 /\ 1 + undef80 <= arg3 /\ 1 <= arg5 /\ 1 + undef67 <= arg5 /\ 1 + undef67 <= arg6 /\ 1 + undef80 <= arg6 /\ 1 <= undef67 /\ 1 + undef70 <= undef72 /\ 1 <= undef80 /\ 1 + undef82 <= undef81 /\ arg1 <= 1 + 2*undef63 /\ undef63 <= arg1 /\ 2*undef63 <= arg1 /\ undef84 <= arg1 /\ 0 <= arg6 /\ undef66 <= undef70 /\ 0 <= undef70 /\ 0 <= undef72 /\ 0 <= undef81 /\ arg1 = 1 + 2*undef71 /\ arg1 = 1 + 2*undef83 /\ arg3 = arg4 /\ arg6 = arg7, {arg1 -> undef63, arg2 -> 1, arg3 -> undef65, arg4 -> undef66, arg5 -> undef67, arg6 -> 0, arg7 -> undef67, rest remain the same}>
<l3, l3, 1 <= arg3 /\ 1 + undef80 <= arg3 /\ 1 + undef87 <= arg3 /\ 1 + undef80 <= arg6 /\ 1 + undef87 <= arg6 /\ 1 <= undef80 /\ 1 + undef82 <= undef81 /\ 1 <= undef87 /\ 1 + undef93 <= undef92 /\ arg1 <= 1 + 2*undef85 /\ undef84 <= arg1 /\ undef85 <= arg1 /\ 2*undef85 <= arg1 /\ 0 <= arg6 /\ 0 <= undef81 /\ 0 <= undef92 /\ arg1 = 1 + 2*undef83 /\ arg1 = 1 + 2*undef94 /\ arg3 = arg4 /\ arg6 = arg7, {arg1 -> undef85, arg2 -> 0, arg3 -> undef87, arg4 -> undef87, arg5 -> 0, arg6 -> undef87, arg7 -> undef87, rest remain the same}>
<l3, l3, 1 <= arg2 /\ 1 <= arg3 /\ 1 + undef80 <= arg3 /\ 1 + undef145 <= arg3 /\ 1 <= arg5 /\ 1 + undef146 <= arg5 /\ 1 <= arg6 /\ 1 + undef80 <= arg6 /\ 1 + undef144 <= arg6 /\ 1 <= undef80 /\ 1 + undef82 <= undef81 /\ 1 <= undef144 /\ arg1 <= 1 + 2*undef138 /\ undef84 <= arg1 /\ undef138 <= arg1 /\ 2*undef138 <= arg1 /\ undef140 <= arg3 /\ 0 <= undef81 /\ undef141 <= undef145 /\ undef142 <= undef146 /\ 0 <= undef145 /\ 0 <= undef146 /\ arg1 = 1 + 2*undef83 /\ arg1 = 1 + 2*undef147 /\ arg3 = arg4 /\ arg6 = arg7, {arg1 -> undef138, arg2 -> undef139, arg3 -> undef140, arg4 -> undef141, arg5 -> undef142, arg7 -> undef144, rest remain the same}>
<l3, l3, 1 <= arg3 /\ 1 + undef80 <= arg3 /\ 1 + undef169 <= arg3 /\ 1 + undef80 <= arg6 /\ 1 + undef168 <= arg6 /\ 1 <= undef80 /\ 1 + undef82 <= undef81 /\ 1 <= undef168 /\ 1 + undef170 <= undef171 /\ arg1 <= 1 + 2*undef162 /\ undef84 <= arg1 /\ undef162 <= arg1 /\ 2*undef162 <= arg1 /\ 0 <= arg6 /\ 0 <= undef81 /\ undef165 <= undef169 /\ 0 <= undef169 /\ 0 <= undef171 /\ arg1 = 1 + 2*undef83 /\ arg1 = 1 + 2*undef172 /\ arg3 = arg4 /\ arg6 = arg7, {arg1 -> undef162, arg2 -> undef163, arg3 -> undef164, arg4 -> undef165, arg5 -> undef166, arg6 -> undef167, arg7 -> undef168, rest remain the same}>
<l3, l3, 1 <= arg2 /\ 1 + arg6 <= arg2 /\ 1 <= arg3 /\ 1 + arg6 <= arg3 /\ 1 + undef42 <= arg3 /\ 1 <= arg4 /\ 1 + undef106 <= arg4 /\ 1 <= arg5 /\ 1 + undef108 <= arg5 /\ 1 + arg6 <= undef102 /\ 1 + arg6 <= undef103 /\ 1 + undef46 <= arg6 /\ 1 + undef104 <= arg7 /\ 1 + undef46 <= undef42 /\ 1 + undef43 <= undef47 /\ 1 + undef46 <= undef43 /\ 1 + undef46 <= undef48 /\ 1 + undef104 <= undef105 /\ 1 + undef104 <= undef106 /\ 1 + undef104 <= undef107 /\ 1 + undef104 <= undef108 /\ arg1 <= 1 + 2*undef39 /\ undef39 <= arg1 /\ 2*undef39 <= arg1 /\ undef109 <= arg1 /\ 0 <= arg6 /\ 0 <= arg7 /\ 0 <= undef46 /\ 0 <= undef47 /\ 0 <= undef104 /\ arg1 = 2*undef49 /\ arg1 = 2*undef110 /\ arg3 = arg4 /\ arg6 = arg7, {arg1 -> undef39, arg2 -> 1, arg3 -> undef41, arg4 -> undef42, arg5 -> undef43, arg6 -> 0, arg7 -> undef43, rest remain the same}>
<l3, l3, 1 <= arg2 /\ 1 + arg6 <= arg2 /\ 1 + arg6 <= arg3 /\ 1 <= arg4 /\ 1 + undef106 <= arg4 /\ 1 + undef114 <= arg4 /\ 1 <= arg5 /\ 1 + undef108 <= arg5 /\ 1 + undef115 <= arg5 /\ 1 + arg6 <= undef102 /\ 1 + arg6 <= undef103 /\ 1 + arg6 <= undef118 /\ 1 + arg6 <= undef119 /\ 1 + undef104 <= arg7 /\ 1 + undef120 <= arg7 /\ 1 + undef104 <= undef105 /\ 1 + undef104 <= undef106 /\ 1 + undef104 <= undef107 /\ 1 + undef104 <= undef108 /\ 1 + undef120 <= undef114 /\ 1 + undef120 <= undef115 /\ 1 + undef120 <= undef117 /\ 1 + undef120 <= undef121 /\ arg1 <= 1 + 2*undef111 /\ undef109 <= arg1 /\ undef111 <= arg1 /\ 2*undef111 <= arg1 /\ 0 <= arg6 /\ 0 <= arg7 /\ 0 <= undef104 /\ 0 <= undef120 /\ arg1 = 2*undef110 /\ arg1 = 2*undef122, {arg1 -> undef111, arg2 -> undef112, arg4 -> undef114, arg5 -> undef115, arg6 -> arg2, arg7 -> undef117, rest remain the same}>
<l3, l3, 1 <= arg2 /\ 1 <= arg4 /\ 1 + undef70 <= arg4 /\ 1 + undef131 <= arg4 /\ 1 <= arg5 /\ 1 + undef67 <= arg5 /\ 1 + undef132 <= arg5 /\ 1 <= arg6 /\ 1 + undef67 <= arg7 /\ 1 + undef130 <= arg7 /\ 1 <= undef67 /\ 1 + undef70 <= undef72 /\ 1 <= undef130 /\ arg1 <= 1 + 2*undef63 /\ undef63 <= arg1 /\ 2*undef63 <= arg1 /\ undef137 <= arg1 /\ 0 <= arg3 /\ undef134 <= arg3 /\ 0 <= arg7 /\ undef66 <= undef70 /\ 0 <= undef70 /\ 0 <= undef72 /\ 0 <= undef131 /\ undef135 <= undef131 /\ 0 <= undef132 /\ undef136 <= undef132 /\ arg1 = 1 + 2*undef71 /\ arg1 = 1 + 2*undef133, {arg1 -> undef63, arg2 -> 1, arg3 -> undef65, arg4 -> undef66, arg5 -> undef67, arg6 -> 0, arg7 -> undef67, rest remain the same}>
<l3, l3, 1 <= arg2 /\ 1 <= arg3 /\ 1 + undef87 <= arg3 /\ 1 <= arg4 /\ 1 + undef131 <= arg4 /\ 1 <= arg5 /\ 1 + undef132 <= arg5 /\ 1 <= arg6 /\ 1 + undef87 <= arg6 /\ 1 + undef130 <= arg7 /\ 1 <= undef87 /\ 1 + undef93 <= undef92 /\ 1 <= undef130 /\ arg1 <= 1 + 2*undef85 /\ undef85 <= arg1 /\ 2*undef85 <= arg1 /\ undef137 <= arg1 /\ undef134 <= arg3 /\ 0 <= arg7 /\ 0 <= undef92 /\ 0 <= undef131 /\ undef135 <= undef131 /\ 0 <= undef132 /\ undef136 <= undef132 /\ arg1 = 1 + 2*undef94 /\ arg1 = 1 + 2*undef133 /\ arg3 = arg4 /\ arg6 = arg7, {arg1 -> undef85, arg2 -> 0, arg3 -> undef87, arg4 -> undef87, arg5 -> 0, arg6 -> undef87, arg7 -> undef87, rest remain the same}>
<l3, l3, 1 <= arg2 /\ 1 <= arg4 /\ 1 + undef131 <= arg4 /\ 1 + undef145 <= arg4 /\ 1 <= arg5 /\ 1 + undef132 <= arg5 /\ 1 + undef146 <= arg5 /\ 1 <= arg6 /\ 1 + undef130 <= arg7 /\ 1 + undef144 <= arg7 /\ 1 <= undef130 /\ 1 <= undef144 /\ arg1 <= 1 + 2*undef138 /\ undef137 <= arg1 /\ undef138 <= arg1 /\ 2*undef138 <= arg1 /\ 0 <= arg3 /\ undef134 <= arg3 /\ undef140 <= arg3 /\ 0 <= arg7 /\ 0 <= undef131 /\ undef135 <= undef131 /\ 0 <= undef132 /\ undef136 <= undef132 /\ undef141 <= undef145 /\ undef142 <= undef146 /\ 0 <= undef145 /\ 0 <= undef146 /\ arg1 = 1 + 2*undef133 /\ arg1 = 1 + 2*undef147, {arg1 -> undef138, arg2 -> undef139, arg3 -> undef140, arg4 -> undef141, arg5 -> undef142, arg7 -> undef144, rest remain the same}>
<l3, l3, 1 <= arg2 /\ 1 <= arg3 /\ 1 + undef169 <= arg3 /\ 1 <= arg4 /\ 1 + undef131 <= arg4 /\ 1 <= arg5 /\ 1 + undef132 <= arg5 /\ 1 <= arg6 /\ 1 + undef168 <= arg6 /\ 1 + undef130 <= arg7 /\ 1 <= undef130 /\ 1 <= undef168 /\ 1 + undef170 <= undef171 /\ arg1 <= 1 + 2*undef162 /\ undef137 <= arg1 /\ undef162 <= arg1 /\ 2*undef162 <= arg1 /\ undef134 <= arg3 /\ 0 <= arg7 /\ 0 <= undef131 /\ undef135 <= undef131 /\ 0 <= undef132 /\ undef136 <= undef132 /\ undef165 <= undef169 /\ 0 <= undef169 /\ 0 <= undef171 /\ arg1 = 1 + 2*undef133 /\ arg1 = 1 + 2*undef172 /\ arg3 = arg4 /\ arg6 = arg7, {arg1 -> undef162, arg2 -> undef163, arg3 -> undef164, arg4 -> undef165, arg5 -> undef166, arg6 -> undef167, arg7 -> undef168, rest remain the same}>
<l3, l3, 1 <= arg2 /\ 1 <= arg3 /\ 1 + undef70 <= arg3 /\ 1 + undef155 <= arg3 /\ 1 <= arg5 /\ 1 + undef67 <= arg5 /\ 1 + undef67 <= arg6 /\ 1 + undef156 <= arg6 /\ 1 <= undef67 /\ 1 + undef70 <= undef72 /\ 1 <= undef156 /\ 1 + undef157 <= undef158 /\ arg1 <= 1 + 2*undef63 /\ undef63 <= arg1 /\ 2*undef63 <= arg1 /\ undef160 <= arg1 /\ 0 <= arg6 /\ undef66 <= undef70 /\ 0 <= undef70 /\ 0 <= undef72 /\ 0 <= undef155 /\ undef161 <= undef155 /\ 0 <= undef158 /\ arg1 = 1 + 2*undef71 /\ arg1 = 1 + 2*undef159 /\ arg3 = arg4 /\ arg6 = arg7, {arg1 -> undef63, arg2 -> 1, arg3 -> undef65, arg4 -> undef66, arg5 -> undef67, arg6 -> 0, arg7 -> undef67, rest remain the same}>
<l3, l3, 1 <= arg3 /\ 1 + undef87 <= arg3 /\ 1 + undef155 <= arg3 /\ 1 + undef87 <= arg6 /\ 1 + undef156 <= arg6 /\ 1 <= undef87 /\ 1 + undef93 <= undef92 /\ 1 <= undef156 /\ 1 + undef157 <= undef158 /\ arg1 <= 1 + 2*undef85 /\ undef85 <= arg1 /\ 2*undef85 <= arg1 /\ undef160 <= arg1 /\ 0 <= arg6 /\ 0 <= undef92 /\ 0 <= undef155 /\ undef161 <= undef155 /\ 0 <= undef158 /\ arg1 = 1 + 2*undef94 /\ arg1 = 1 + 2*undef159 /\ arg3 = arg4 /\ arg6 = arg7, {arg1 -> undef85, arg2 -> 0, arg3 -> undef87, arg4 -> undef87, arg5 -> 0, arg6 -> undef87, arg7 -> undef87, rest remain the same}>
<l3, l3, 1 <= arg2 /\ 1 <= arg3 /\ 1 + undef145 <= arg3 /\ 1 + undef155 <= arg3 /\ 1 <= arg5 /\ 1 + undef146 <= arg5 /\ 1 <= arg6 /\ 1 + undef144 <= arg6 /\ 1 + undef156 <= arg6 /\ 1 <= undef144 /\ 1 <= undef156 /\ 1 + undef157 <= undef158 /\ arg1 <= 1 + 2*undef138 /\ undef138 <= arg1 /\ 2*undef138 <= arg1 /\ undef160 <= arg1 /\ undef140 <= arg3 /\ undef141 <= undef145 /\ undef142 <= undef146 /\ 0 <= undef145 /\ 0 <= undef146 /\ 0 <= undef155 /\ undef161 <= undef155 /\ 0 <= undef158 /\ arg1 = 1 + 2*undef147 /\ arg1 = 1 + 2*undef159 /\ arg3 = arg4 /\ arg6 = arg7, {arg1 -> undef138, arg2 -> undef139, arg3 -> undef140, arg4 -> undef141, arg5 -> undef142, arg7 -> undef144, rest remain the same}>
<l3, l3, 1 <= arg3 /\ 1 + undef155 <= arg3 /\ 1 + undef169 <= arg3 /\ 1 + undef156 <= arg6 /\ 1 + undef168 <= arg6 /\ 1 <= undef156 /\ 1 + undef157 <= undef158 /\ 1 <= undef168 /\ 1 + undef170 <= undef171 /\ arg1 <= 1 + 2*undef162 /\ undef160 <= arg1 /\ undef162 <= arg1 /\ 2*undef162 <= arg1 /\ 0 <= arg6 /\ 0 <= undef155 /\ undef161 <= undef155 /\ 0 <= undef158 /\ undef165 <= undef169 /\ 0 <= undef169 /\ 0 <= undef171 /\ arg1 = 1 + 2*undef159 /\ arg1 = 1 + 2*undef172 /\ arg3 = arg4 /\ arg6 = arg7, {arg1 -> undef162, arg2 -> undef163, arg3 -> undef164, arg4 -> undef165, arg5 -> undef166, arg6 -> undef167, arg7 -> undef168, rest remain the same}>
Variables:
arg1, arg3, arg4, arg5, arg6, arg7, arg2

Precedence: 
Graph 0

Graph 1
<l0, l5, 1 <= undef189 /\ 0 <= undef180 /\ 0 <= undef181 /\ 2 <= undef190, {arg1 -> -1 + undef181, arg2 -> undef174, arg3 -> undef175, arg4 -> undef176, arg5 -> undef177, arg6 -> undef178, arg7 -> undef179, rest remain the same}>

Graph 2
<l0, l3, 1 + undef2 <= undef9 /\ 1 <= undef2 /\ 1 <= undef189 /\ 0 <= undef1 /\ 0 <= undef8 /\ 0 <= undef9 /\ 2 <= undef190, {arg1 -> undef1, arg2 -> 0, arg3 -> undef2, arg4 -> undef2, arg5 -> 0, arg6 -> undef2, arg7 -> undef2, rest remain the same}>

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

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

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

Checking conditional termination of SCC {l5}...

LOG: CALL solveLinear

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

Checking conditional termination of SCC {l3}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.173129s
Ranking function: -8 + 4*arg4
New Graphs: 
Transitions:
<l3, l3, 1 <= arg2 /\ 1 <= arg4 /\ 1 + undef58 <= arg4 /\ 1 + undef70 <= arg4 /\ 1 <= arg5 /\ 1 + undef57 <= arg5 /\ 1 + undef67 <= arg5 /\ 1 + undef57 <= arg7 /\ 1 + undef67 <= arg7 /\ 1 <= undef57 /\ 1 + undef58 <= undef60 /\ 1 <= undef67 /\ 1 + undef70 <= undef72 /\ arg1 <= 1 + 2*undef63 /\ undef61 <= arg1 /\ undef63 <= arg1 /\ 2*undef63 <= arg1 /\ 0 <= arg7 /\ 0 <= undef58 /\ undef62 <= undef58 /\ 0 <= undef60 /\ undef66 <= undef70 /\ 0 <= undef70 /\ 0 <= undef72 /\ arg1 = 1 + 2*undef59 /\ arg1 = 1 + 2*undef71, {arg1 -> undef63, arg2 -> 1, arg3 -> undef65, arg4 -> undef66, arg5 -> undef67, arg6 -> 0, arg7 -> undef67, rest remain the same}>
<l3, l3, 1 <= arg2 /\ 1 <= arg4 /\ 1 + undef58 <= arg4 /\ 1 + undef145 <= arg4 /\ 1 <= arg5 /\ 1 + undef57 <= arg5 /\ 1 + undef146 <= arg5 /\ 1 <= arg6 /\ 1 + undef57 <= arg7 /\ 1 + undef144 <= arg7 /\ 1 <= undef57 /\ 1 + undef58 <= undef60 /\ 1 <= undef144 /\ arg1 <= 1 + 2*undef138 /\ undef61 <= arg1 /\ undef138 <= arg1 /\ 2*undef138 <= arg1 /\ 0 <= arg3 /\ undef140 <= arg3 /\ 0 <= arg7 /\ 0 <= undef58 /\ undef62 <= undef58 /\ 0 <= undef60 /\ undef141 <= undef145 /\ undef142 <= undef146 /\ 0 <= undef145 /\ 0 <= undef146 /\ arg1 = 1 + 2*undef59 /\ arg1 = 1 + 2*undef147, {arg1 -> undef138, arg2 -> undef139, arg3 -> undef140, arg4 -> undef141, arg5 -> undef142, arg7 -> undef144, rest remain the same}>
<l3, l3, 1 <= arg2 /\ 1 <= arg3 /\ 1 + undef169 <= arg3 /\ 1 <= arg4 /\ 1 + undef58 <= arg4 /\ 1 <= arg5 /\ 1 + undef57 <= arg5 /\ 1 + undef168 <= arg6 /\ 1 + undef57 <= arg7 /\ 1 <= undef57 /\ 1 + undef58 <= undef60 /\ 1 <= undef168 /\ 1 + undef170 <= undef171 /\ arg1 <= 1 + 2*undef162 /\ undef61 <= arg1 /\ undef162 <= arg1 /\ 2*undef162 <= arg1 /\ 0 <= arg6 /\ 0 <= arg7 /\ 0 <= undef58 /\ undef62 <= undef58 /\ 0 <= undef60 /\ undef165 <= undef169 /\ 0 <= undef169 /\ 0 <= undef171 /\ arg1 = 1 + 2*undef59 /\ arg1 = 1 + 2*undef172 /\ arg3 = arg4 /\ arg6 = arg7, {arg1 -> undef162, arg2 -> undef163, arg3 -> undef164, arg4 -> undef165, arg5 -> undef166, arg6 -> undef167, arg7 -> undef168, rest remain the same}>
<l3, l3, 1 <= arg2 /\ 1 <= arg4 /\ 1 + undef70 <= arg4 /\ 1 + undef131 <= arg4 /\ 1 <= arg5 /\ 1 + undef67 <= arg5 /\ 1 + undef132 <= arg5 /\ 1 <= arg6 /\ 1 + undef67 <= arg7 /\ 1 + undef130 <= arg7 /\ 1 <= undef67 /\ 1 + undef70 <= undef72 /\ 1 <= undef130 /\ arg1 <= 1 + 2*undef63 /\ undef63 <= arg1 /\ 2*undef63 <= arg1 /\ undef137 <= arg1 /\ 0 <= arg3 /\ undef134 <= arg3 /\ 0 <= arg7 /\ undef66 <= undef70 /\ 0 <= undef70 /\ 0 <= undef72 /\ 0 <= undef131 /\ undef135 <= undef131 /\ 0 <= undef132 /\ undef136 <= undef132 /\ arg1 = 1 + 2*undef71 /\ arg1 = 1 + 2*undef133, {arg1 -> undef63, arg2 -> 1, arg3 -> undef65, arg4 -> undef66, arg5 -> undef67, arg6 -> 0, arg7 -> undef67, rest remain the same}>
<l3, l3, 1 <= arg2 /\ 1 <= arg4 /\ 1 + undef131 <= arg4 /\ 1 + undef145 <= arg4 /\ 1 <= arg5 /\ 1 + undef132 <= arg5 /\ 1 + undef146 <= arg5 /\ 1 <= arg6 /\ 1 + undef130 <= arg7 /\ 1 + undef144 <= arg7 /\ 1 <= undef130 /\ 1 <= undef144 /\ arg1 <= 1 + 2*undef138 /\ undef137 <= arg1 /\ undef138 <= arg1 /\ 2*undef138 <= arg1 /\ 0 <= arg3 /\ undef134 <= arg3 /\ undef140 <= arg3 /\ 0 <= arg7 /\ 0 <= undef131 /\ undef135 <= undef131 /\ 0 <= undef132 /\ undef136 <= undef132 /\ undef141 <= undef145 /\ undef142 <= undef146 /\ 0 <= undef145 /\ 0 <= undef146 /\ arg1 = 1 + 2*undef133 /\ arg1 = 1 + 2*undef147, {arg1 -> undef138, arg2 -> undef139, arg3 -> undef140, arg4 -> undef141, arg5 -> undef142, arg7 -> undef144, rest remain the same}>
<l3, l3, 1 <= arg2 /\ 1 <= arg3 /\ 1 + undef169 <= arg3 /\ 1 <= arg4 /\ 1 + undef131 <= arg4 /\ 1 <= arg5 /\ 1 + undef132 <= arg5 /\ 1 <= arg6 /\ 1 + undef168 <= arg6 /\ 1 + undef130 <= arg7 /\ 1 <= undef130 /\ 1 <= undef168 /\ 1 + undef170 <= undef171 /\ arg1 <= 1 + 2*undef162 /\ undef137 <= arg1 /\ undef162 <= arg1 /\ 2*undef162 <= arg1 /\ undef134 <= arg3 /\ 0 <= arg7 /\ 0 <= undef131 /\ undef135 <= undef131 /\ 0 <= undef132 /\ undef136 <= undef132 /\ undef165 <= undef169 /\ 0 <= undef169 /\ 0 <= undef171 /\ arg1 = 1 + 2*undef133 /\ arg1 = 1 + 2*undef172 /\ arg3 = arg4 /\ arg6 = arg7, {arg1 -> undef162, arg2 -> undef163, arg3 -> undef164, arg4 -> undef165, arg5 -> undef166, arg6 -> undef167, arg7 -> undef168, rest remain the same}>
<l3, l3, 1 <= arg2 /\ 1 <= arg3 /\ 1 + undef70 <= arg3 /\ 1 + undef155 <= arg3 /\ 1 <= arg5 /\ 1 + undef67 <= arg5 /\ 1 + undef67 <= arg6 /\ 1 + undef156 <= arg6 /\ 1 <= undef67 /\ 1 + undef70 <= undef72 /\ 1 <= undef156 /\ 1 + undef157 <= undef158 /\ arg1 <= 1 + 2*undef63 /\ undef63 <= arg1 /\ 2*undef63 <= arg1 /\ undef160 <= arg1 /\ 0 <= arg6 /\ undef66 <= undef70 /\ 0 <= undef70 /\ 0 <= undef72 /\ 0 <= undef155 /\ undef161 <= undef155 /\ 0 <= undef158 /\ arg1 = 1 + 2*undef71 /\ arg1 = 1 + 2*undef159 /\ arg3 = arg4 /\ arg6 = arg7, {arg1 -> undef63, arg2 -> 1, arg3 -> undef65, arg4 -> undef66, arg5 -> undef67, arg6 -> 0, arg7 -> undef67, rest remain the same}>
<l3, l3, 1 <= arg2 /\ 1 <= arg3 /\ 1 + undef145 <= arg3 /\ 1 + undef155 <= arg3 /\ 1 <= arg5 /\ 1 + undef146 <= arg5 /\ 1 <= arg6 /\ 1 + undef144 <= arg6 /\ 1 + undef156 <= arg6 /\ 1 <= undef144 /\ 1 <= undef156 /\ 1 + undef157 <= undef158 /\ arg1 <= 1 + 2*undef138 /\ undef138 <= arg1 /\ 2*undef138 <= arg1 /\ undef160 <= arg1 /\ undef140 <= arg3 /\ undef141 <= undef145 /\ undef142 <= undef146 /\ 0 <= undef145 /\ 0 <= undef146 /\ 0 <= undef155 /\ undef161 <= undef155 /\ 0 <= undef158 /\ arg1 = 1 + 2*undef147 /\ arg1 = 1 + 2*undef159 /\ arg3 = arg4 /\ arg6 = arg7, {arg1 -> undef138, arg2 -> undef139, arg3 -> undef140, arg4 -> undef141, arg5 -> undef142, arg7 -> undef144, rest remain the same}>
<l3, l3, 1 <= arg3 /\ 1 + undef155 <= arg3 /\ 1 + undef169 <= arg3 /\ 1 + undef156 <= arg6 /\ 1 + undef168 <= arg6 /\ 1 <= undef156 /\ 1 + undef157 <= undef158 /\ 1 <= undef168 /\ 1 + undef170 <= undef171 /\ arg1 <= 1 + 2*undef162 /\ undef160 <= arg1 /\ undef162 <= arg1 /\ 2*undef162 <= arg1 /\ 0 <= arg6 /\ 0 <= undef155 /\ undef161 <= undef155 /\ 0 <= undef158 /\ undef165 <= undef169 /\ 0 <= undef169 /\ 0 <= undef171 /\ arg1 = 1 + 2*undef159 /\ arg1 = 1 + 2*undef172 /\ arg3 = arg4 /\ arg6 = arg7, {arg1 -> undef162, arg2 -> undef163, arg3 -> undef164, arg4 -> undef165, arg5 -> undef166, arg6 -> undef167, arg7 -> undef168, rest remain the same}>
Variables:
arg1, arg2, arg3, arg4, arg5, arg6, arg7
Checking conditional termination of SCC {l3}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.028666s
Ranking function: -2 + arg7
New Graphs: 
Program Terminates