NO

Solver Timeout: 4
Global Timeout: 300
No parsing errors!
Init Location: 0
Transitions:
<l0, l12, true>
<l1, l2, (undef1 <= arg1) /\ (arg2 > ~(1)) /\ (arg1 > 0) /\ (undef1 > 0), par{arg1 -> undef1, arg2 -> 0, arg3 -> undef3, arg4 -> undef4, arg5 -> undef5, arg6 -> undef6}>
<l2, l2, (arg2 < 2) /\ (arg2 < 13) /\ (undef13 > 0) /\ (undef14 > arg2) /\ (undef14 > ~(1)) /\ (undef7 <= arg1) /\ (arg1 > 0) /\ (undef7 > 0), par{arg1 -> undef7, arg2 -> (arg2 + 1), arg3 -> undef9, arg4 -> undef10, arg5 -> undef11, arg6 -> undef12}>
<l2, l2, (arg2 > 1) /\ (arg2 < 13) /\ (undef21 > 0) /\ (undef22 > arg2) /\ (undef22 > ~(1)) /\ (arg1 >= undef15) /\ (arg1 > 0) /\ (undef15 > 0), par{arg1 -> undef15, arg2 -> (arg2 + 1), arg3 -> undef17, arg4 -> undef18, arg5 -> undef19, arg6 -> undef20}>
<l2, l3, (undef23 <= arg1) /\ (arg2 > 12) /\ (arg1 > 0) /\ (undef23 > 0), par{arg1 -> undef23, arg2 -> 1, arg3 -> undef25, arg4 -> undef26, arg5 -> undef27, arg6 -> undef28}>
<l3, l4, (undef29 <= arg1) /\ (arg2 < undef35) /\ (arg1 > 0) /\ (undef29 > 0), par{arg1 -> undef29, arg3 -> 0, arg4 -> undef32, arg5 -> undef33, arg6 -> undef34}>
<l4, l3, (undef36 <= arg1) /\ (arg3 > 12) /\ (arg1 > 0) /\ (undef36 > 0), par{arg1 -> undef36, arg2 -> (arg2 + 1), arg3 -> undef38, arg4 -> undef39, arg5 -> undef40, arg6 -> undef41}>
<l3, l5, (undef42 <= arg1) /\ (arg2 >= undef48) /\ (arg1 > 0) /\ (undef42 > 0), par{arg1 -> undef42, arg2 -> 0, arg3 -> undef44, arg4 -> undef45, arg5 -> undef46, arg6 -> undef47}>
<l4, l6, (arg2 < 8) /\ (arg3 < 13) /\ (arg3 > ~(1)) /\ ((arg3 - undef55) < 0) /\ (arg2 < undef56) /\ (arg2 > 0) /\ ((arg2 - 1) < undef56) /\ (undef57 > arg3) /\ (undef57 > ~(1)) /\ (undef49 <= arg1) /\ (arg1 > 0) /\ (undef49 > 0) /\ (undef51 > ~(1)), par{arg1 -> undef49, arg3 -> undef51, arg4 -> arg3, arg5 -> undef53, arg6 -> undef54}>
<l4, l6, (arg2 < 8) /\ (arg3 < 13) /\ (arg3 > ~(1)) /\ ((arg3 - undef64) < 0) /\ (arg2 < undef65) /\ (arg2 > 0) /\ ((arg2 - 1) < undef65) /\ (undef66 > arg3) /\ (undef66 > ~(1)) /\ (undef58 <= arg1) /\ (undef60 <= arg1) /\ (arg1 > 0) /\ (undef58 > 0) /\ (undef60 > 0), par{arg1 -> undef58, arg3 -> undef60, arg4 -> arg3, arg5 -> undef62, arg6 -> undef63}>
<l4, l7, (arg2 < 8) /\ (arg3 < 13) /\ (arg3 > ~(1)) /\ ((arg3 - undef73) >= 0) /\ (arg2 < undef74) /\ (arg2 > 0) /\ ((arg2 - 1) < undef74) /\ (undef75 > ~(1)) /\ (undef75 > arg3) /\ (arg1 > 0) /\ (undef68 > ~(1)), par{arg1 -> arg2, arg2 -> undef68, arg4 -> undef70, arg5 -> (arg2 - 1), arg6 -> undef72}>
<l4, l7, (arg2 < 8) /\ (arg3 < 13) /\ (arg3 > ~(1)) /\ ((arg3 - undef82) >= 0) /\ (arg2 < undef83) /\ (arg2 > 0) /\ ((arg2 - 1) < undef83) /\ (undef84 > ~(1)) /\ (undef84 > arg3) /\ (undef77 <= arg1) /\ (arg1 > 0) /\ (undef77 > 0), par{arg1 -> arg2, arg2 -> undef77, arg4 -> undef79, arg5 -> (arg2 - 1), arg6 -> undef81}>
<l5, l8, (undef85 <= arg1) /\ (arg2 < undef91) /\ (arg1 > 0) /\ (undef85 > 0), par{arg1 -> undef85, arg3 -> 0, arg4 -> undef88, arg5 -> undef89, arg6 -> undef90}>
<l8, l5, (undef92 <= arg1) /\ (arg3 > 12) /\ (arg1 > 0) /\ (undef92 > 0), par{arg1 -> undef92, arg2 -> (arg2 + 1), arg3 -> undef94, arg4 -> undef95, arg5 -> undef96, arg6 -> undef97}>
<l8, l8, (arg3 < 13) /\ (arg3 < 12) /\ (undef98 <= arg1) /\ (arg1 > 0) /\ (undef98 > 0), par{arg1 -> undef98, arg3 -> (arg3 + 1), arg4 -> undef101, arg5 -> undef102, arg6 -> undef103}>
<l8, l8, (undef104 <= arg1) /\ (arg1 > 0) /\ (undef104 > 0) /\ (12 = arg3), par{arg1 -> undef104, arg3 -> 13, arg4 -> undef107, arg5 -> undef108, arg6 -> undef109}>
<l7, l9, (arg1 < 8) /\ (arg5 < undef116) /\ (arg3 > ~(1)) /\ (undef117 > ~(1)) /\ (undef117 > (arg3 - undef118)) /\ ((undef110 - 1) <= arg2) /\ (undef112 <= arg2) /\ (arg2 > ~(1)) /\ (undef110 > 0) /\ (undef112 > ~(1)), par{arg1 -> undef110, arg2 -> arg1, arg3 -> undef112, arg4 -> arg3, arg5 -> arg4, arg6 -> (undef119 + undef120)}>
<l7, l9, (arg1 < 8) /\ (arg5 < undef127) /\ (arg3 > ~(1)) /\ (undef128 > ~(1)) /\ ((arg3 - undef129) < undef128) /\ (undef121 <= arg2) /\ (undef123 <= arg2) /\ (arg2 > 0) /\ (undef121 > 0) /\ (undef123 > 0), par{arg1 -> undef121, arg2 -> arg1, arg3 -> undef123, arg4 -> arg3, arg5 -> arg4, arg6 -> (undef130 + undef131)}>
<l9, l10, (undef132 <= arg1) /\ (arg6 >= arg5) /\ ((undef132 - 1) <= arg3) /\ (undef134 <= arg3) /\ (arg1 > 0) /\ (arg3 > ~(1)) /\ (undef132 > 0) /\ (undef134 > ~(1)), par{arg1 -> undef132, arg3 -> undef134, arg5 -> undef136, arg6 -> undef137}>
<l9, l10, (undef138 <= arg1) /\ (arg6 < arg5) /\ ((undef138 - 1) <= arg3) /\ (undef140 <= arg3) /\ (arg1 > 0) /\ (arg3 > ~(1)) /\ (undef138 > 0) /\ (undef140 > ~(1)), par{arg1 -> undef138, arg3 -> undef140, arg5 -> undef142, arg6 -> undef143}>
<l5, l11, (arg2 >= undef150) /\ (undef150 > ~(1)) /\ (undef144 <= arg1) /\ (arg1 > 0) /\ (undef144 > 0), par{arg1 -> undef144, arg2 -> 12, arg3 -> (undef150 - 1), arg4 -> undef147, arg5 -> undef148, arg6 -> undef149}>
<l6, l4, (undef157 > ~(1)) /\ (undef157 > arg4) /\ (undef151 <= arg1) /\ (undef151 <= arg3) /\ (arg1 > 0) /\ (arg3 > 0) /\ (undef151 > 0), par{arg1 -> undef151, arg3 -> (arg4 + 1), arg4 -> undef154, arg5 -> undef155, arg6 -> undef156}>
<l10, l4, (undef164 > ~(1)) /\ (undef164 > arg4) /\ (undef158 <= arg1) /\ (undef158 <= arg3) /\ (arg1 > 0) /\ (arg3 > 0) /\ (undef158 > 0), par{arg1 -> undef158, arg3 -> (arg4 + 1), arg4 -> undef161, arg5 -> undef162, arg6 -> undef163}>
<l11, l11, (arg3 < undef171) /\ (arg3 > 0) /\ (undef172 > ~(1)) /\ (undef172 > arg2) /\ ((arg3 - 1) < undef171) /\ (undef173 > arg2) /\ (undef173 > ~(1)) /\ (undef165 <= arg1) /\ (arg1 > 0) /\ (undef165 > 0), par{arg1 -> undef165, arg3 -> (arg3 - 1), arg4 -> undef168, arg5 -> undef169, arg6 -> undef170}>
<l11, l11, (arg3 < undef180) /\ (arg3 > 0) /\ (undef181 > ~(1)) /\ (undef181 > arg2) /\ ((arg3 - 1) < undef180) /\ (undef182 > ~(1)) /\ (undef182 > arg2) /\ (undef183 > undef184) /\ (arg3 < 8) /\ (arg2 > ~(1)) /\ (undef174 <= arg1) /\ (arg1 > 0) /\ (undef174 > 0), par{arg1 -> undef174, arg2 -> (arg2 - undef185), arg3 -> (arg3 - 1), arg4 -> undef177, arg5 -> undef178, arg6 -> undef179}>
<l11, l11, (arg3 < undef192) /\ (arg3 > 0) /\ (undef193 > ~(1)) /\ (undef193 > arg2) /\ ((arg3 - 1) < undef192) /\ (undef194 > ~(1)) /\ (undef194 > arg2) /\ (undef195 < undef196) /\ (arg3 < 8) /\ (arg2 > ~(1)) /\ (undef186 <= arg1) /\ (arg1 > 0) /\ (undef186 > 0), par{arg1 -> undef186, arg2 -> (arg2 - undef197), arg3 -> (arg3 - 1), arg4 -> undef189, arg5 -> undef190, arg6 -> undef191}>
<l12, l1, true, par{arg1 -> undef198, arg2 -> undef199, arg3 -> undef200, arg4 -> undef201, arg5 -> undef202, arg6 -> undef203}>

Fresh variables:
undef1, undef3, undef4, undef5, undef6, undef7, undef9, undef10, undef11, undef12, undef13, undef14, undef15, undef17, undef18, undef19, undef20, undef21, undef22, undef23, undef25, undef26, undef27, undef28, undef29, undef32, undef33, undef34, undef35, undef36, undef38, undef39, undef40, undef41, undef42, undef44, undef45, undef46, undef47, undef48, undef49, undef51, undef53, undef54, undef55, undef56, undef57, undef58, undef60, undef62, undef63, undef64, undef65, undef66, undef68, undef70, undef72, undef73, undef74, undef75, undef77, undef79, undef81, undef82, undef83, undef84, undef85, undef88, undef89, undef90, undef91, undef92, undef94, undef95, undef96, undef97, undef98, undef101, undef102, undef103, undef104, undef107, undef108, undef109, undef110, undef112, undef116, undef117, undef118, undef119, undef120, undef121, undef123, undef127, undef128, undef129, undef130, undef131, undef132, undef134, undef136, undef137, undef138, undef140, undef142, undef143, undef144, undef147, undef148, undef149, undef150, undef151, undef154, undef155, undef156, undef157, undef158, undef161, undef162, undef163, undef164, undef165, undef168, undef169, undef170, undef171, undef172, undef173, undef174, undef177, undef178, undef179, undef180, undef181, undef182, undef183, undef184, undef185, undef186, undef189, undef190, undef191, undef192, undef193, undef194, undef195, undef196, undef197, undef198, undef199, undef200, undef201, undef202, undef203, 

Undef variables:
undef1, undef3, undef4, undef5, undef6, undef7, undef9, undef10, undef11, undef12, undef13, undef14, undef15, undef17, undef18, undef19, undef20, undef21, undef22, undef23, undef25, undef26, undef27, undef28, undef29, undef32, undef33, undef34, undef35, undef36, undef38, undef39, undef40, undef41, undef42, undef44, undef45, undef46, undef47, undef48, undef49, undef51, undef53, undef54, undef55, undef56, undef57, undef58, undef60, undef62, undef63, undef64, undef65, undef66, undef68, undef70, undef72, undef73, undef74, undef75, undef77, undef79, undef81, undef82, undef83, undef84, undef85, undef88, undef89, undef90, undef91, undef92, undef94, undef95, undef96, undef97, undef98, undef101, undef102, undef103, undef104, undef107, undef108, undef109, undef110, undef112, undef116, undef117, undef118, undef119, undef120, undef121, undef123, undef127, undef128, undef129, undef130, undef131, undef132, undef134, undef136, undef137, undef138, undef140, undef142, undef143, undef144, undef147, undef148, undef149, undef150, undef151, undef154, undef155, undef156, undef157, undef158, undef161, undef162, undef163, undef164, undef165, undef168, undef169, undef170, undef171, undef172, undef173, undef174, undef177, undef178, undef179, undef180, undef181, undef182, undef183, undef184, undef185, undef186, undef189, undef190, undef191, undef192, undef193, undef194, undef195, undef196, undef197, undef198, undef199, undef200, undef201, undef202, undef203, 

Abstraction variables:

Exit nodes:

Accepting locations:

Asserts:

Preprocessed LLVMGraph
Init Location: 0
Transitions:
<l0, l2, (arg1 = undef1) /\ (arg2 = 0) /\ (arg3 = undef3) /\ (undef1 <= undef198) /\ (undef199 > ~(1)) /\ (undef198 > 0) /\ (undef1 > 0)>
<l2, l2, (arg2 < 2) /\ (arg2 < 13) /\ (undef13 > 0) /\ (undef14 > arg2) /\ (undef14 > ~(1)) /\ (undef7 <= arg1) /\ (arg1 > 0) /\ (undef7 > 0), par{arg1 -> undef7, arg2 -> (arg2 + 1), arg3 -> undef9}>
<l2, l2, (arg2 > 1) /\ (arg2 < 13) /\ (undef21 > 0) /\ (undef22 > arg2) /\ (undef22 > ~(1)) /\ (arg1 >= undef15) /\ (arg1 > 0) /\ (undef15 > 0), par{arg1 -> undef15, arg2 -> (arg2 + 1), arg3 -> undef17}>
<l2, l4, (undef23 <= arg1) /\ (arg2 > 12) /\ (arg1 > 0) /\ (undef23 > 0) /\ (undef29 <= undef23) /\ (1 < undef35) /\ (undef23 > 0) /\ (undef29 > 0), par{arg1 -> undef29, arg2 -> 1, arg3 -> 0}>
<l2, l8, (undef23 <= arg1) /\ (arg2 > 12) /\ (arg1 > 0) /\ (undef23 > 0) /\ (undef42 <= undef23) /\ (1 >= undef48) /\ (undef23 > 0) /\ (undef42 > 0) /\ (undef85 <= undef42) /\ (0 < undef91) /\ (undef42 > 0) /\ (undef85 > 0), par{arg1 -> undef85, arg2 -> 0, arg3 -> 0}>
<l2, l11, (undef23 <= arg1) /\ (arg2 > 12) /\ (arg1 > 0) /\ (undef23 > 0) /\ (undef42 <= undef23) /\ (1 >= undef48) /\ (undef23 > 0) /\ (undef42 > 0) /\ (0 >= undef150) /\ (undef150 > ~(1)) /\ (undef144 <= undef42) /\ (undef42 > 0) /\ (undef144 > 0), par{arg1 -> undef144, arg2 -> 12, arg3 -> (undef150 - 1)}>
<l4, l4, (undef36 <= arg1) /\ (arg3 > 12) /\ (arg1 > 0) /\ (undef36 > 0) /\ (undef29 <= undef36) /\ ((arg2 + 1) < undef35) /\ (undef36 > 0) /\ (undef29 > 0), par{arg1 -> undef29, arg2 -> (arg2 + 1), arg3 -> 0}>
<l4, l8, (undef36 <= arg1) /\ (arg3 > 12) /\ (arg1 > 0) /\ (undef36 > 0) /\ (undef42 <= undef36) /\ ((arg2 + 1) >= undef48) /\ (undef36 > 0) /\ (undef42 > 0) /\ (undef85 <= undef42) /\ (0 < undef91) /\ (undef42 > 0) /\ (undef85 > 0), par{arg1 -> undef85, arg2 -> 0, arg3 -> 0}>
<l4, l11, (undef36 <= arg1) /\ (arg3 > 12) /\ (arg1 > 0) /\ (undef36 > 0) /\ (undef42 <= undef36) /\ ((arg2 + 1) >= undef48) /\ (undef36 > 0) /\ (undef42 > 0) /\ (0 >= undef150) /\ (undef150 > ~(1)) /\ (undef144 <= undef42) /\ (undef42 > 0) /\ (undef144 > 0), par{arg1 -> undef144, arg2 -> 12, arg3 -> (undef150 - 1)}>
<l4, l4, (arg2 < 8) /\ (arg3 < 13) /\ (arg3 > ~(1)) /\ ((arg3 - undef55) < 0) /\ (arg2 < undef56) /\ (arg2 > 0) /\ ((arg2 - 1) < undef56) /\ (undef57 > arg3) /\ (undef57 > ~(1)) /\ (undef49 <= arg1) /\ (arg1 > 0) /\ (undef49 > 0) /\ (undef51 > ~(1)) /\ (undef157 > ~(1)) /\ (undef157 > arg3) /\ (undef151 <= undef49) /\ (undef151 <= undef51) /\ (undef49 > 0) /\ (undef51 > 0) /\ (undef151 > 0), par{arg1 -> undef151, arg3 -> (arg3 + 1)}>
<l4, l4, (arg2 < 8) /\ (arg3 < 13) /\ (arg3 > ~(1)) /\ ((arg3 - undef64) < 0) /\ (arg2 < undef65) /\ (arg2 > 0) /\ ((arg2 - 1) < undef65) /\ (undef66 > arg3) /\ (undef66 > ~(1)) /\ (undef58 <= arg1) /\ (undef60 <= arg1) /\ (arg1 > 0) /\ (undef58 > 0) /\ (undef60 > 0) /\ (undef157 > ~(1)) /\ (undef157 > arg3) /\ (undef151 <= undef58) /\ (undef151 <= undef60) /\ (undef58 > 0) /\ (undef60 > 0) /\ (undef151 > 0), par{arg1 -> undef151, arg3 -> (arg3 + 1)}>
<l4, l4, (arg2 < 8) /\ (arg3 < 13) /\ (arg3 > ~(1)) /\ ((arg3 - undef73) >= 0) /\ (arg2 < undef74) /\ (arg2 > 0) /\ ((arg2 - 1) < undef74) /\ (undef75 > ~(1)) /\ (undef75 > arg3) /\ (arg1 > 0) /\ (undef68 > ~(1)) /\ (arg2 < 8) /\ ((arg2 - 1) < undef116) /\ (arg3 > ~(1)) /\ (undef117 > ~(1)) /\ (undef117 > (arg3 - undef118)) /\ ((undef110 - 1) <= undef68) /\ (undef112 <= undef68) /\ (undef68 > ~(1)) /\ (undef110 > 0) /\ (undef112 > ~(1)) /\ (undef132 <= undef110) /\ ((undef119 + undef120) >= undef70) /\ ((undef132 - 1) <= undef112) /\ (undef134 <= undef112) /\ (undef110 > 0) /\ (undef112 > ~(1)) /\ (undef132 > 0) /\ (undef134 > ~(1)) /\ (undef164 > ~(1)) /\ (undef164 > arg3) /\ (undef158 <= undef132) /\ (undef158 <= undef134) /\ (undef132 > 0) /\ (undef134 > 0) /\ (undef158 > 0), par{arg1 -> undef158, arg2 -> arg2, arg3 -> (arg3 + 1)}>
<l4, l4, (arg2 < 8) /\ (arg3 < 13) /\ (arg3 > ~(1)) /\ ((arg3 - undef73) >= 0) /\ (arg2 < undef74) /\ (arg2 > 0) /\ ((arg2 - 1) < undef74) /\ (undef75 > ~(1)) /\ (undef75 > arg3) /\ (arg1 > 0) /\ (undef68 > ~(1)) /\ (arg2 < 8) /\ ((arg2 - 1) < undef116) /\ (arg3 > ~(1)) /\ (undef117 > ~(1)) /\ (undef117 > (arg3 - undef118)) /\ ((undef110 - 1) <= undef68) /\ (undef112 <= undef68) /\ (undef68 > ~(1)) /\ (undef110 > 0) /\ (undef112 > ~(1)) /\ (undef138 <= undef110) /\ ((undef119 + undef120) < undef70) /\ ((undef138 - 1) <= undef112) /\ (undef140 <= undef112) /\ (undef110 > 0) /\ (undef112 > ~(1)) /\ (undef138 > 0) /\ (undef140 > ~(1)) /\ (undef164 > ~(1)) /\ (undef164 > arg3) /\ (undef158 <= undef138) /\ (undef158 <= undef140) /\ (undef138 > 0) /\ (undef140 > 0) /\ (undef158 > 0), par{arg1 -> undef158, arg2 -> arg2, arg3 -> (arg3 + 1)}>
<l4, l4, (arg2 < 8) /\ (arg3 < 13) /\ (arg3 > ~(1)) /\ ((arg3 - undef73) >= 0) /\ (arg2 < undef74) /\ (arg2 > 0) /\ ((arg2 - 1) < undef74) /\ (undef75 > ~(1)) /\ (undef75 > arg3) /\ (arg1 > 0) /\ (undef68 > ~(1)) /\ (arg2 < 8) /\ ((arg2 - 1) < undef127) /\ (arg3 > ~(1)) /\ (undef128 > ~(1)) /\ ((arg3 - undef129) < undef128) /\ (undef121 <= undef68) /\ (undef123 <= undef68) /\ (undef68 > 0) /\ (undef121 > 0) /\ (undef123 > 0) /\ (undef132 <= undef121) /\ ((undef130 + undef131) >= undef70) /\ ((undef132 - 1) <= undef123) /\ (undef134 <= undef123) /\ (undef121 > 0) /\ (undef123 > ~(1)) /\ (undef132 > 0) /\ (undef134 > ~(1)) /\ (undef164 > ~(1)) /\ (undef164 > arg3) /\ (undef158 <= undef132) /\ (undef158 <= undef134) /\ (undef132 > 0) /\ (undef134 > 0) /\ (undef158 > 0), par{arg1 -> undef158, arg2 -> arg2, arg3 -> (arg3 + 1)}>
<l4, l4, (arg2 < 8) /\ (arg3 < 13) /\ (arg3 > ~(1)) /\ ((arg3 - undef73) >= 0) /\ (arg2 < undef74) /\ (arg2 > 0) /\ ((arg2 - 1) < undef74) /\ (undef75 > ~(1)) /\ (undef75 > arg3) /\ (arg1 > 0) /\ (undef68 > ~(1)) /\ (arg2 < 8) /\ ((arg2 - 1) < undef127) /\ (arg3 > ~(1)) /\ (undef128 > ~(1)) /\ ((arg3 - undef129) < undef128) /\ (undef121 <= undef68) /\ (undef123 <= undef68) /\ (undef68 > 0) /\ (undef121 > 0) /\ (undef123 > 0) /\ (undef138 <= undef121) /\ ((undef130 + undef131) < undef70) /\ ((undef138 - 1) <= undef123) /\ (undef140 <= undef123) /\ (undef121 > 0) /\ (undef123 > ~(1)) /\ (undef138 > 0) /\ (undef140 > ~(1)) /\ (undef164 > ~(1)) /\ (undef164 > arg3) /\ (undef158 <= undef138) /\ (undef158 <= undef140) /\ (undef138 > 0) /\ (undef140 > 0) /\ (undef158 > 0), par{arg1 -> undef158, arg2 -> arg2, arg3 -> (arg3 + 1)}>
<l4, l4, (arg2 < 8) /\ (arg3 < 13) /\ (arg3 > ~(1)) /\ ((arg3 - undef82) >= 0) /\ (arg2 < undef83) /\ (arg2 > 0) /\ ((arg2 - 1) < undef83) /\ (undef84 > ~(1)) /\ (undef84 > arg3) /\ (undef77 <= arg1) /\ (arg1 > 0) /\ (undef77 > 0) /\ (arg2 < 8) /\ ((arg2 - 1) < undef116) /\ (arg3 > ~(1)) /\ (undef117 > ~(1)) /\ (undef117 > (arg3 - undef118)) /\ ((undef110 - 1) <= undef77) /\ (undef112 <= undef77) /\ (undef77 > ~(1)) /\ (undef110 > 0) /\ (undef112 > ~(1)) /\ (undef132 <= undef110) /\ ((undef119 + undef120) >= undef79) /\ ((undef132 - 1) <= undef112) /\ (undef134 <= undef112) /\ (undef110 > 0) /\ (undef112 > ~(1)) /\ (undef132 > 0) /\ (undef134 > ~(1)) /\ (undef164 > ~(1)) /\ (undef164 > arg3) /\ (undef158 <= undef132) /\ (undef158 <= undef134) /\ (undef132 > 0) /\ (undef134 > 0) /\ (undef158 > 0), par{arg1 -> undef158, arg2 -> arg2, arg3 -> (arg3 + 1)}>
<l4, l4, (arg2 < 8) /\ (arg3 < 13) /\ (arg3 > ~(1)) /\ ((arg3 - undef82) >= 0) /\ (arg2 < undef83) /\ (arg2 > 0) /\ ((arg2 - 1) < undef83) /\ (undef84 > ~(1)) /\ (undef84 > arg3) /\ (undef77 <= arg1) /\ (arg1 > 0) /\ (undef77 > 0) /\ (arg2 < 8) /\ ((arg2 - 1) < undef116) /\ (arg3 > ~(1)) /\ (undef117 > ~(1)) /\ (undef117 > (arg3 - undef118)) /\ ((undef110 - 1) <= undef77) /\ (undef112 <= undef77) /\ (undef77 > ~(1)) /\ (undef110 > 0) /\ (undef112 > ~(1)) /\ (undef138 <= undef110) /\ ((undef119 + undef120) < undef79) /\ ((undef138 - 1) <= undef112) /\ (undef140 <= undef112) /\ (undef110 > 0) /\ (undef112 > ~(1)) /\ (undef138 > 0) /\ (undef140 > ~(1)) /\ (undef164 > ~(1)) /\ (undef164 > arg3) /\ (undef158 <= undef138) /\ (undef158 <= undef140) /\ (undef138 > 0) /\ (undef140 > 0) /\ (undef158 > 0), par{arg1 -> undef158, arg2 -> arg2, arg3 -> (arg3 + 1)}>
<l4, l4, (arg2 < 8) /\ (arg3 < 13) /\ (arg3 > ~(1)) /\ ((arg3 - undef82) >= 0) /\ (arg2 < undef83) /\ (arg2 > 0) /\ ((arg2 - 1) < undef83) /\ (undef84 > ~(1)) /\ (undef84 > arg3) /\ (undef77 <= arg1) /\ (arg1 > 0) /\ (undef77 > 0) /\ (arg2 < 8) /\ ((arg2 - 1) < undef127) /\ (arg3 > ~(1)) /\ (undef128 > ~(1)) /\ ((arg3 - undef129) < undef128) /\ (undef121 <= undef77) /\ (undef123 <= undef77) /\ (undef77 > 0) /\ (undef121 > 0) /\ (undef123 > 0) /\ (undef132 <= undef121) /\ ((undef130 + undef131) >= undef79) /\ ((undef132 - 1) <= undef123) /\ (undef134 <= undef123) /\ (undef121 > 0) /\ (undef123 > ~(1)) /\ (undef132 > 0) /\ (undef134 > ~(1)) /\ (undef164 > ~(1)) /\ (undef164 > arg3) /\ (undef158 <= undef132) /\ (undef158 <= undef134) /\ (undef132 > 0) /\ (undef134 > 0) /\ (undef158 > 0), par{arg1 -> undef158, arg2 -> arg2, arg3 -> (arg3 + 1)}>
<l4, l4, (arg2 < 8) /\ (arg3 < 13) /\ (arg3 > ~(1)) /\ ((arg3 - undef82) >= 0) /\ (arg2 < undef83) /\ (arg2 > 0) /\ ((arg2 - 1) < undef83) /\ (undef84 > ~(1)) /\ (undef84 > arg3) /\ (undef77 <= arg1) /\ (arg1 > 0) /\ (undef77 > 0) /\ (arg2 < 8) /\ ((arg2 - 1) < undef127) /\ (arg3 > ~(1)) /\ (undef128 > ~(1)) /\ ((arg3 - undef129) < undef128) /\ (undef121 <= undef77) /\ (undef123 <= undef77) /\ (undef77 > 0) /\ (undef121 > 0) /\ (undef123 > 0) /\ (undef138 <= undef121) /\ ((undef130 + undef131) < undef79) /\ ((undef138 - 1) <= undef123) /\ (undef140 <= undef123) /\ (undef121 > 0) /\ (undef123 > ~(1)) /\ (undef138 > 0) /\ (undef140 > ~(1)) /\ (undef164 > ~(1)) /\ (undef164 > arg3) /\ (undef158 <= undef138) /\ (undef158 <= undef140) /\ (undef138 > 0) /\ (undef140 > 0) /\ (undef158 > 0), par{arg1 -> undef158, arg2 -> arg2, arg3 -> (arg3 + 1)}>
<l8, l8, (undef92 <= arg1) /\ (arg3 > 12) /\ (arg1 > 0) /\ (undef92 > 0) /\ (undef85 <= undef92) /\ ((arg2 + 1) < undef91) /\ (undef92 > 0) /\ (undef85 > 0), par{arg1 -> undef85, arg2 -> (arg2 + 1), arg3 -> 0}>
<l8, l11, (undef92 <= arg1) /\ (arg3 > 12) /\ (arg1 > 0) /\ (undef92 > 0) /\ ((arg2 + 1) >= undef150) /\ (undef150 > ~(1)) /\ (undef144 <= undef92) /\ (undef92 > 0) /\ (undef144 > 0), par{arg1 -> undef144, arg2 -> 12, arg3 -> (undef150 - 1)}>
<l8, l8, (arg3 < 13) /\ (arg3 < 12) /\ (undef98 <= arg1) /\ (arg1 > 0) /\ (undef98 > 0), par{arg1 -> undef98, arg3 -> (arg3 + 1)}>
<l8, l8, (undef104 <= arg1) /\ (arg1 > 0) /\ (undef104 > 0) /\ (12 = arg3), par{arg1 -> undef104, arg3 -> 13}>
<l11, l11, (arg3 < undef171) /\ (arg3 > 0) /\ (undef172 > ~(1)) /\ (undef172 > arg2) /\ ((arg3 - 1) < undef171) /\ (undef173 > arg2) /\ (undef173 > ~(1)) /\ (undef165 <= arg1) /\ (arg1 > 0) /\ (undef165 > 0), par{arg1 -> undef165, arg3 -> (arg3 - 1)}>
<l11, l11, (arg3 < undef180) /\ (arg3 > 0) /\ (undef181 > ~(1)) /\ (undef181 > arg2) /\ ((arg3 - 1) < undef180) /\ (undef182 > ~(1)) /\ (undef182 > arg2) /\ (undef183 > undef184) /\ (arg3 < 8) /\ (arg2 > ~(1)) /\ (undef174 <= arg1) /\ (arg1 > 0) /\ (undef174 > 0), par{arg1 -> undef174, arg2 -> (arg2 - undef185), arg3 -> (arg3 - 1)}>
<l11, l11, (arg3 < undef192) /\ (arg3 > 0) /\ (undef193 > ~(1)) /\ (undef193 > arg2) /\ ((arg3 - 1) < undef192) /\ (undef194 > ~(1)) /\ (undef194 > arg2) /\ (undef195 < undef196) /\ (arg3 < 8) /\ (arg2 > ~(1)) /\ (undef186 <= arg1) /\ (arg1 > 0) /\ (undef186 > 0), par{arg1 -> undef186, arg2 -> (arg2 - undef197), arg3 -> (arg3 - 1)}>

Fresh variables:
undef1, undef3, undef4, undef5, undef6, undef7, undef9, undef10, undef11, undef12, undef13, undef14, undef15, undef17, undef18, undef19, undef20, undef21, undef22, undef23, undef25, undef26, undef27, undef28, undef29, undef32, undef33, undef34, undef35, undef36, undef38, undef39, undef40, undef41, undef42, undef44, undef45, undef46, undef47, undef48, undef49, undef51, undef53, undef54, undef55, undef56, undef57, undef58, undef60, undef62, undef63, undef64, undef65, undef66, undef68, undef70, undef72, undef73, undef74, undef75, undef77, undef79, undef81, undef82, undef83, undef84, undef85, undef88, undef89, undef90, undef91, undef92, undef94, undef95, undef96, undef97, undef98, undef101, undef102, undef103, undef104, undef107, undef108, undef109, undef110, undef112, undef116, undef117, undef118, undef119, undef120, undef121, undef123, undef127, undef128, undef129, undef130, undef131, undef132, undef134, undef136, undef137, undef138, undef140, undef142, undef143, undef144, undef147, undef148, undef149, undef150, undef151, undef154, undef155, undef156, undef157, undef158, undef161, undef162, undef163, undef164, undef165, undef168, undef169, undef170, undef171, undef172, undef173, undef174, undef177, undef178, undef179, undef180, undef181, undef182, undef183, undef184, undef185, undef186, undef189, undef190, undef191, undef192, undef193, undef194, undef195, undef196, undef197, undef198, undef199, undef200, undef201, undef202, undef203, 

Undef variables:
undef1, undef3, undef4, undef5, undef6, undef7, undef9, undef10, undef11, undef12, undef13, undef14, undef15, undef17, undef18, undef19, undef20, undef21, undef22, undef23, undef25, undef26, undef27, undef28, undef29, undef32, undef33, undef34, undef35, undef36, undef38, undef39, undef40, undef41, undef42, undef44, undef45, undef46, undef47, undef48, undef49, undef51, undef53, undef54, undef55, undef56, undef57, undef58, undef60, undef62, undef63, undef64, undef65, undef66, undef68, undef70, undef72, undef73, undef74, undef75, undef77, undef79, undef81, undef82, undef83, undef84, undef85, undef88, undef89, undef90, undef91, undef92, undef94, undef95, undef96, undef97, undef98, undef101, undef102, undef103, undef104, undef107, undef108, undef109, undef110, undef112, undef116, undef117, undef118, undef119, undef120, undef121, undef123, undef127, undef128, undef129, undef130, undef131, undef132, undef134, undef136, undef137, undef138, undef140, undef142, undef143, undef144, undef147, undef148, undef149, undef150, undef151, undef154, undef155, undef156, undef157, undef158, undef161, undef162, undef163, undef164, undef165, undef168, undef169, undef170, undef171, undef172, undef173, undef174, undef177, undef178, undef179, undef180, undef181, undef182, undef183, undef184, undef185, undef186, undef189, undef190, undef191, undef192, undef193, undef194, undef195, undef196, undef197, undef198, undef199, undef200, undef201, undef202, undef203, 

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 <= undef14 /\ 1 <= undef7 /\ 1 <= undef13 /\ arg2 <= 1 /\ undef7 <= arg1 /\ 0 <= undef14, {arg1 -> undef7, arg2 -> 1 + arg2, arg3 -> undef9, rest remain the same}>
<l2, l2, 1 <= arg1 /\ 1 + arg2 <= undef22 /\ 1 <= undef15 /\ 1 <= undef21 /\ undef15 <= arg1 /\ 0 <= undef22 /\ 2 <= arg2 /\ arg2 <= 12, {arg1 -> undef15, arg2 -> 1 + arg2, arg3 -> undef17, rest remain the same}>
Variables:
arg1, arg2, arg3

Graph 2:
Transitions:
<l4, l4, 1 <= arg1 /\ 1 <= undef29 /\ 1 <= undef36 /\ undef36 <= arg1 /\ undef29 <= undef36 /\ 2 + arg2 <= undef35 /\ 13 <= arg3, {arg1 -> undef29, arg2 -> 1 + arg2, arg3 -> 0, rest remain the same}>
<l4, l4, 1 <= arg1 /\ 1 + arg2 <= undef56 /\ 1 <= arg2 /\ 1 + arg3 <= undef55 /\ 1 + arg3 <= undef57 /\ 1 + arg3 <= undef157 /\ 1 <= undef49 /\ 1 <= undef51 /\ 1 <= undef151 /\ undef49 <= arg1 /\ 0 <= arg3 /\ undef151 <= undef49 /\ undef151 <= undef51 /\ 0 <= undef57 /\ 0 <= undef157 /\ arg3 <= 12 /\ arg2 <= 7, {arg1 -> undef151, arg3 -> 1 + arg3, rest remain the same}>
<l4, l4, 1 <= arg1 /\ 1 + arg2 <= undef65 /\ 1 <= arg2 /\ 1 + arg3 <= undef64 /\ 1 + arg3 <= undef66 /\ 1 + arg3 <= undef157 /\ 1 <= undef58 /\ 1 <= undef60 /\ 1 <= undef151 /\ undef58 <= arg1 /\ undef60 <= arg1 /\ 0 <= arg3 /\ undef151 <= undef58 /\ undef151 <= undef60 /\ 0 <= undef66 /\ 0 <= undef157 /\ arg3 <= 12 /\ arg2 <= 7, {arg1 -> undef151, arg3 -> 1 + arg3, rest remain the same}>
<l4, l4, 1 <= arg1 /\ 1 + arg2 <= undef74 /\ 1 <= arg2 /\ 1 + arg3 <= undef75 /\ 1 + arg3 <= undef117 + undef118 /\ 1 + arg3 <= undef164 /\ 1 <= undef110 /\ 1 <= undef132 /\ 1 <= undef134 /\ 1 <= undef158 /\ undef110 <= 1 + undef68 /\ undef132 <= 1 + undef112 /\ arg2 <= undef116 /\ 0 <= arg3 /\ undef73 <= arg3 /\ 0 <= undef68 /\ undef112 <= undef68 /\ undef70 <= undef119 + undef120 /\ 0 <= undef75 /\ undef132 <= undef110 /\ 0 <= undef112 /\ undef134 <= undef112 /\ 0 <= undef117 /\ undef158 <= undef132 /\ undef158 <= undef134 /\ 0 <= undef164 /\ arg3 <= 12 /\ arg2 <= 7, {arg1 -> undef158, arg3 -> 1 + arg3, rest remain the same}>
<l4, l4, 1 <= arg1 /\ 1 + arg2 <= undef74 /\ 1 <= arg2 /\ 1 + arg3 <= undef75 /\ 1 + arg3 <= undef117 + undef118 /\ 1 + arg3 <= undef164 /\ 1 + undef119 + undef120 <= undef70 /\ 1 <= undef110 /\ 1 <= undef138 /\ 1 <= undef140 /\ 1 <= undef158 /\ undef110 <= 1 + undef68 /\ undef138 <= 1 + undef112 /\ arg2 <= undef116 /\ 0 <= arg3 /\ undef73 <= arg3 /\ 0 <= undef68 /\ undef112 <= undef68 /\ 0 <= undef75 /\ undef138 <= undef110 /\ 0 <= undef112 /\ undef140 <= undef112 /\ 0 <= undef117 /\ undef158 <= undef138 /\ undef158 <= undef140 /\ 0 <= undef164 /\ arg3 <= 12 /\ arg2 <= 7, {arg1 -> undef158, arg3 -> 1 + arg3, rest remain the same}>
<l4, l4, 1 <= arg1 /\ 1 + arg2 <= undef74 /\ 1 <= arg2 /\ 1 + arg3 <= undef75 /\ 1 + arg3 <= undef128 + undef129 /\ 1 + arg3 <= undef164 /\ 1 <= undef68 /\ 1 <= undef121 /\ 1 <= undef123 /\ 1 <= undef132 /\ 1 <= undef134 /\ 1 <= undef158 /\ undef132 <= 1 + undef123 /\ arg2 <= undef127 /\ 0 <= arg3 /\ undef73 <= arg3 /\ undef121 <= undef68 /\ undef123 <= undef68 /\ undef70 <= undef130 + undef131 /\ 0 <= undef75 /\ undef132 <= undef121 /\ undef134 <= undef123 /\ 0 <= undef128 /\ undef158 <= undef132 /\ undef158 <= undef134 /\ 0 <= undef164 /\ arg3 <= 12 /\ arg2 <= 7, {arg1 -> undef158, arg3 -> 1 + arg3, rest remain the same}>
<l4, l4, 1 <= arg1 /\ 1 + arg2 <= undef74 /\ 1 <= arg2 /\ 1 + arg3 <= undef75 /\ 1 + arg3 <= undef128 + undef129 /\ 1 + arg3 <= undef164 /\ 1 <= undef68 /\ 1 + undef130 + undef131 <= undef70 /\ 1 <= undef121 /\ 1 <= undef123 /\ 1 <= undef138 /\ 1 <= undef140 /\ 1 <= undef158 /\ undef138 <= 1 + undef123 /\ arg2 <= undef127 /\ 0 <= arg3 /\ undef73 <= arg3 /\ undef121 <= undef68 /\ undef123 <= undef68 /\ 0 <= undef75 /\ undef138 <= undef121 /\ undef140 <= undef123 /\ 0 <= undef128 /\ undef158 <= undef138 /\ undef158 <= undef140 /\ 0 <= undef164 /\ arg3 <= 12 /\ arg2 <= 7, {arg1 -> undef158, arg3 -> 1 + arg3, rest remain the same}>
<l4, l4, 1 <= arg1 /\ 1 + arg2 <= undef83 /\ 1 <= arg2 /\ 1 + arg3 <= undef84 /\ 1 + arg3 <= undef117 + undef118 /\ 1 + arg3 <= undef164 /\ 1 <= undef77 /\ 1 <= undef110 /\ 1 <= undef132 /\ 1 <= undef134 /\ 1 <= undef158 /\ undef110 <= 1 + undef77 /\ undef132 <= 1 + undef112 /\ undef77 <= arg1 /\ arg2 <= undef116 /\ 0 <= arg3 /\ undef82 <= arg3 /\ undef112 <= undef77 /\ undef79 <= undef119 + undef120 /\ 0 <= undef84 /\ undef132 <= undef110 /\ 0 <= undef112 /\ undef134 <= undef112 /\ 0 <= undef117 /\ undef158 <= undef132 /\ undef158 <= undef134 /\ 0 <= undef164 /\ arg3 <= 12 /\ arg2 <= 7, {arg1 -> undef158, arg3 -> 1 + arg3, rest remain the same}>
<l4, l4, 1 <= arg1 /\ 1 + arg2 <= undef83 /\ 1 <= arg2 /\ 1 + arg3 <= undef84 /\ 1 + arg3 <= undef117 + undef118 /\ 1 + arg3 <= undef164 /\ 1 <= undef77 /\ 1 + undef119 + undef120 <= undef79 /\ 1 <= undef110 /\ 1 <= undef138 /\ 1 <= undef140 /\ 1 <= undef158 /\ undef110 <= 1 + undef77 /\ undef138 <= 1 + undef112 /\ undef77 <= arg1 /\ arg2 <= undef116 /\ 0 <= arg3 /\ undef82 <= arg3 /\ undef112 <= undef77 /\ 0 <= undef84 /\ undef138 <= undef110 /\ 0 <= undef112 /\ undef140 <= undef112 /\ 0 <= undef117 /\ undef158 <= undef138 /\ undef158 <= undef140 /\ 0 <= undef164 /\ arg3 <= 12 /\ arg2 <= 7, {arg1 -> undef158, arg3 -> 1 + arg3, rest remain the same}>
<l4, l4, 1 <= arg1 /\ 1 + arg2 <= undef83 /\ 1 <= arg2 /\ 1 + arg3 <= undef84 /\ 1 + arg3 <= undef128 + undef129 /\ 1 + arg3 <= undef164 /\ 1 <= undef77 /\ 1 <= undef121 /\ 1 <= undef123 /\ 1 <= undef132 /\ 1 <= undef134 /\ 1 <= undef158 /\ undef132 <= 1 + undef123 /\ undef77 <= arg1 /\ arg2 <= undef127 /\ 0 <= arg3 /\ undef82 <= arg3 /\ undef121 <= undef77 /\ undef123 <= undef77 /\ undef79 <= undef130 + undef131 /\ 0 <= undef84 /\ undef132 <= undef121 /\ undef134 <= undef123 /\ 0 <= undef128 /\ undef158 <= undef132 /\ undef158 <= undef134 /\ 0 <= undef164 /\ arg3 <= 12 /\ arg2 <= 7, {arg1 -> undef158, arg3 -> 1 + arg3, rest remain the same}>
<l4, l4, 1 <= arg1 /\ 1 + arg2 <= undef83 /\ 1 <= arg2 /\ 1 + arg3 <= undef84 /\ 1 + arg3 <= undef128 + undef129 /\ 1 + arg3 <= undef164 /\ 1 <= undef77 /\ 1 + undef130 + undef131 <= undef79 /\ 1 <= undef121 /\ 1 <= undef123 /\ 1 <= undef138 /\ 1 <= undef140 /\ 1 <= undef158 /\ undef138 <= 1 + undef123 /\ undef77 <= arg1 /\ arg2 <= undef127 /\ 0 <= arg3 /\ undef82 <= arg3 /\ undef121 <= undef77 /\ undef123 <= undef77 /\ 0 <= undef84 /\ undef138 <= undef121 /\ undef140 <= undef123 /\ 0 <= undef128 /\ undef158 <= undef138 /\ undef158 <= undef140 /\ 0 <= undef164 /\ arg3 <= 12 /\ arg2 <= 7, {arg1 -> undef158, arg3 -> 1 + arg3, rest remain the same}>
Variables:
arg1, arg2, arg3

Graph 3:
Transitions:
<l8, l8, 1 <= arg1 /\ 1 <= undef85 /\ 1 <= undef92 /\ undef92 <= arg1 /\ undef85 <= undef92 /\ 2 + arg2 <= undef91 /\ 13 <= arg3, {arg1 -> undef85, arg2 -> 1 + arg2, arg3 -> 0, rest remain the same}>
<l8, l8, 1 <= arg1 /\ 1 <= undef98 /\ undef98 <= arg1 /\ arg3 <= 11, {arg1 -> undef98, arg3 -> 1 + arg3, rest remain the same}>
<l8, l8, 1 <= arg1 /\ 1 <= undef104 /\ undef104 <= arg1 /\ arg3 = 12, {arg1 -> undef104, arg3 -> 13, rest remain the same}>
Variables:
arg1, arg2, arg3

Graph 4:
Transitions:
<l11, l11, 1 <= arg1 /\ 1 + arg2 <= undef172 /\ 1 + arg2 <= undef173 /\ 1 + arg3 <= undef171 /\ 1 <= arg3 /\ 1 <= undef165 /\ undef165 <= arg1 /\ 0 <= undef172 /\ 0 <= undef173, {arg1 -> undef165, arg3 -> -1 + arg3, rest remain the same}>
<l11, l11, 1 <= arg1 /\ 1 + arg2 <= undef181 /\ 1 + arg2 <= undef182 /\ 1 + arg3 <= undef180 /\ 1 <= arg3 /\ 1 <= undef174 /\ 1 + undef184 <= undef183 /\ undef174 <= arg1 /\ 0 <= arg2 /\ 0 <= undef181 /\ 0 <= undef182 /\ arg3 <= 7, {arg1 -> undef174, arg2 -> arg2 - undef185, arg3 -> -1 + arg3, rest remain the same}>
<l11, l11, 1 <= arg1 /\ 1 + arg2 <= undef193 /\ 1 + arg2 <= undef194 /\ 1 + arg3 <= undef192 /\ 1 <= arg3 /\ 1 <= undef186 /\ 1 + undef195 <= undef196 /\ undef186 <= arg1 /\ 0 <= arg2 /\ 0 <= undef193 /\ 0 <= undef194 /\ arg3 <= 7, {arg1 -> undef186, arg2 -> arg2 - undef197, arg3 -> -1 + arg3, rest remain the same}>
Variables:
arg1, arg2, arg3

Precedence: 
Graph 0

Graph 1
<l0, l2, 1 <= undef1 /\ 1 <= undef198 /\ undef1 <= undef198 /\ 0 <= undef199 /\ arg1 = undef1 /\ arg2 = 0 /\ arg3 = undef3, {all remain the same}>

Graph 2
<l2, l4, 1 <= arg1 /\ 1 <= undef23 /\ 1 <= undef29 /\ undef23 <= arg1 /\ undef29 <= undef23 /\ 2 <= undef35 /\ 13 <= arg2, {arg1 -> undef29, arg2 -> 1, arg3 -> 0, rest remain the same}>

Graph 3
<l2, l8, 1 <= arg1 /\ 1 <= undef23 /\ 1 <= undef42 /\ 1 <= undef85 /\ 1 <= undef91 /\ undef48 <= 1 /\ undef23 <= arg1 /\ undef42 <= undef23 /\ undef85 <= undef42 /\ 13 <= arg2, {arg1 -> undef85, arg2 -> 0, arg3 -> 0, rest remain the same}>
<l4, l8, 1 <= arg1 /\ 1 <= undef36 /\ 1 <= undef42 /\ 1 <= undef85 /\ 1 <= undef91 /\ undef48 <= 1 + arg2 /\ undef36 <= arg1 /\ undef42 <= undef36 /\ undef85 <= undef42 /\ 13 <= arg3, {arg1 -> undef85, arg2 -> 0, arg3 -> 0, rest remain the same}>

Graph 4
<l2, l11, 1 <= arg1 /\ 1 <= undef23 /\ 1 <= undef42 /\ 1 <= undef144 /\ undef48 <= 1 /\ undef23 <= arg1 /\ undef42 <= undef23 /\ undef144 <= undef42 /\ 13 <= arg2 /\ undef150 = 0, {arg1 -> undef144, arg2 -> 12, arg3 -> -1 + undef150, rest remain the same}>
<l4, l11, 1 <= arg1 /\ 1 <= undef36 /\ 1 <= undef42 /\ 1 <= undef144 /\ undef48 <= 1 + arg2 /\ undef36 <= arg1 /\ undef42 <= undef36 /\ undef144 <= undef42 /\ 13 <= arg3 /\ undef150 = 0, {arg1 -> undef144, arg2 -> 12, arg3 -> -1 + undef150, rest remain the same}>
<l8, l11, 1 <= arg1 /\ 1 <= undef92 /\ 1 <= undef144 /\ undef150 <= 1 + arg2 /\ undef92 <= arg1 /\ undef144 <= undef92 /\ 0 <= undef150 /\ 13 <= arg3, {arg1 -> undef144, arg2 -> 12, arg3 -> -1 + undef150, rest remain the same}>

Map Locations to Subgraph:
( 0 , 0 )
( 2 , 1 )
( 4 , 2 )
( 8 , 3 )
( 11 , 4 )

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

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

Checking conditional termination of SCC {l2}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001348s
Ranking function: 12 - arg2
New Graphs: 
Proving termination of subgraph 2
Checking unfeasibility...
Time used: 0.143031

Checking conditional termination of SCC {l4}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.020364s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.684811s
Trying to remove transition: <l4, l4, 1 <= arg1 /\ 1 + arg2 <= undef83 /\ 1 <= arg2 /\ 1 + arg3 <= undef84 /\ 1 + arg3 <= undef128 + undef129 /\ 1 + arg3 <= undef164 /\ 1 <= undef77 /\ 1 + undef130 + undef131 <= undef79 /\ 1 <= undef121 /\ 1 <= undef123 /\ 1 <= undef138 /\ 1 <= undef140 /\ 1 <= undef158 /\ undef138 <= 1 + undef123 /\ undef77 <= arg1 /\ arg2 <= undef127 /\ 0 <= arg3 /\ undef82 <= arg3 /\ undef121 <= undef77 /\ undef123 <= undef77 /\ 0 <= undef84 /\ undef138 <= undef121 /\ undef140 <= undef123 /\ 0 <= undef128 /\ undef158 <= undef138 /\ undef158 <= undef140 /\ 0 <= undef164 /\ arg3 <= 12 /\ arg2 <= 7, {arg1 -> undef158, arg3 -> 1 + arg3, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.131994s
Time used: 0.12843

LOG: SAT solveNonLinear - Elapsed time: 0.131994s
Cost: 0; Total time: 0.12843
Termination implied by a set of quasi-invariant(s):
Quasi-invariant at l4: arg3 <= 13
Ranking function: 103 - 13*arg2 - arg3
Ranking function and negation of Quasi-Invariant applied
New Graphs: 
Transitions:
<l4, l4, 1 <= arg1 /\ 1 <= undef29 /\ 1 <= undef36 /\ undef36 <= arg1 /\ undef29 <= undef36 /\ 2 + arg2 <= undef35 /\ 13 <= arg3, {arg1 -> undef29, arg2 -> 1 + arg2, arg3 -> 0, rest remain the same}>
Variables:
arg1, arg2, arg3
Checking conditional termination of SCC {l4}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001653s
Ranking function: -1 + (1 / 13)*arg3
New Graphs: 
Proving termination of subgraph 3
Checking unfeasibility...
Time used: 4.003

Checking conditional termination of SCC {l8}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.020171s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.015252s
Trying to remove transition: <l8, l8, 1 <= arg1 /\ 1 <= undef104 /\ undef104 <= arg1 /\ arg3 = 12, {arg1 -> undef104, arg3 -> 13, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.002934s
Time used: 4.00225
Trying to remove transition: <l8, l8, 1 <= arg1 /\ 1 <= undef98 /\ undef98 <= arg1 /\ arg3 <= 11, {arg1 -> undef98, arg3 -> 1 + arg3, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.027639s
Time used: 4.00243
Trying to remove transition: <l8, l8, 1 <= arg1 /\ 1 <= undef85 /\ 1 <= undef92 /\ undef92 <= arg1 /\ undef85 <= undef92 /\ 2 + arg2 <= undef91 /\ 13 <= arg3, {arg1 -> undef85, arg2 -> 1 + arg2, arg3 -> 0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.036062s
Time used: 0.017777
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.004468s
Time used: 4.00333
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.004632s
Time used: 4.00189
Solving with 3 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.012672s
Time used: 1.00136
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.032755s
Time used: 0.029407
Improving Solution with cost 1 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.001762s
Time used: 1.00175

LOG: SAT solveNonLinear - Elapsed time: 1.034517s
Cost: 1; Total time: 1.03115
Quasi-ranking function: 50000 - arg2
New Graphs: 
Transitions:
<l8, l8, 1 <= arg1 /\ 1 <= undef85 /\ 1 <= undef92 /\ undef92 <= arg1 /\ undef85 <= undef92 /\ 2 + arg2 <= undef91 /\ 13 <= arg3 /\ 50001 <= arg2, {arg1 -> undef85, arg2 -> 1 + arg2, arg3 -> 0, rest remain the same}>
<l8, l8, 1 <= arg1 /\ 1 <= undef98 /\ undef98 <= arg1 /\ arg3 <= 11, {arg1 -> undef98, arg3 -> 1 + arg3, rest remain the same}>
<l8, l8, 1 <= arg1 /\ 1 <= undef104 /\ undef104 <= arg1 /\ arg3 = 12, {arg1 -> undef104, arg3 -> 13, rest remain the same}>
Variables:
arg1, arg2, arg3
Checking conditional termination of SCC {l8}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001466s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.017954s
Trying to remove transition: <l8, l8, 1 <= arg1 /\ 1 <= undef104 /\ undef104 <= arg1 /\ arg3 = 12, {arg1 -> undef104, arg3 -> 13, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.003489s
Time used: 4.00281
Trying to remove transition: <l8, l8, 1 <= arg1 /\ 1 <= undef98 /\ undef98 <= arg1 /\ arg3 <= 11, {arg1 -> undef98, arg3 -> 1 + arg3, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.028241s
Time used: 4.00274
Trying to remove transition: <l8, l8, 1 <= arg1 /\ 1 <= undef85 /\ 1 <= undef92 /\ undef92 <= arg1 /\ undef85 <= undef92 /\ 2 + arg2 <= undef91 /\ 13 <= arg3 /\ 50001 <= arg2, {arg1 -> undef85, arg2 -> 1 + arg2, arg3 -> 0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.040227s
Time used: 0.024468
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.003654s
Time used: 4.0025
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.019074s
Time used: 4.00183
Solving with 3 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.012391s
Time used: 1.00111
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.035198s
Time used: 0.031501
Improving Solution with cost 1 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.002098s
Time used: 1.00208

LOG: SAT solveNonLinear - Elapsed time: 1.037296s
Cost: 1; Total time: 1.03358
Termination implied by a set of invariant(s):
Invariant at l8: 1 <= arg1
[ Invariant Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l8, l8, 1 <= arg1 /\ 1 <= undef85 /\ 1 <= undef92 /\ undef92 <= arg1 /\ undef85 <= undef92 /\ 2 + arg2 <= undef91 /\ 13 <= arg3, {arg1 -> undef85, arg2 -> 1 + arg2, arg3 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l8, l8, 1 <= arg1 /\ 1 <= undef98 /\ undef98 <= arg1 /\ arg3 <= 11, {arg1 -> undef98, arg3 -> 1 + arg3, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l8, l8, 1 <= arg1 /\ 1 <= undef104 /\ undef104 <= arg1 /\ arg3 = 12, {arg1 -> undef104, arg3 -> 13, rest remain the same}>
[ Termination Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l8, l8, 1 <= arg1 /\ 1 <= undef85 /\ 1 <= undef92 /\ undef92 <= arg1 /\ undef85 <= undef92 /\ 2 + arg2 <= undef91 /\ 13 <= arg3 /\ 50001 <= arg2, {arg1 -> undef85, arg2 -> 1 + arg2, arg3 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l8, l8, 1 <= arg1 /\ 1 <= undef98 /\ undef98 <= arg1 /\ arg3 <= 11, {arg1 -> undef98, arg3 -> 1 + arg3, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l8, l8, 1 <= arg1 /\ 1 <= undef104 /\ undef104 <= arg1 /\ arg3 = 12, {arg1 -> undef104, arg3 -> 13, rest remain the same}>
Quasi-ranking function: 50000 + 50000*arg1 - arg2
New Graphs: 
Transitions:
<l8, l8, 1 <= arg1 /\ 1 <= undef85 /\ 1 <= undef92 /\ undef92 <= arg1 /\ undef85 <= undef92 /\ 2 + arg2 <= undef91 /\ 13 <= arg3 /\ 50001 + 50000*arg1 <= arg2 /\ 50001 <= arg2, {arg1 -> undef85, arg2 -> 1 + arg2, arg3 -> 0, rest remain the same}>
<l8, l8, 1 <= arg1 /\ 1 <= undef98 /\ undef98 <= arg1 /\ arg3 <= 11, {arg1 -> undef98, arg3 -> 1 + arg3, rest remain the same}>
<l8, l8, 1 <= arg1 /\ 1 <= undef104 /\ undef104 <= arg1 /\ arg3 = 12, {arg1 -> undef104, arg3 -> 13, rest remain the same}>
Variables:
arg1, arg2, arg3
Checking conditional termination of SCC {l8}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001568s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.023138s
Trying to remove transition: <l8, l8, 1 <= arg1 /\ 1 <= undef104 /\ undef104 <= arg1 /\ arg3 = 12, {arg1 -> undef104, arg3 -> 13, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.003916s
Time used: 4.00322
Trying to remove transition: <l8, l8, 1 <= arg1 /\ 1 <= undef98 /\ undef98 <= arg1 /\ arg3 <= 11, {arg1 -> undef98, arg3 -> 1 + arg3, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.034211s
Time used: 4.00306
Trying to remove transition: <l8, l8, 1 <= arg1 /\ 1 <= undef85 /\ 1 <= undef92 /\ undef92 <= arg1 /\ undef85 <= undef92 /\ 2 + arg2 <= undef91 /\ 13 <= arg3 /\ 50001 + 50000*arg1 <= arg2 /\ 50001 <= arg2, {arg1 -> undef85, arg2 -> 1 + arg2, arg3 -> 0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.045731s
Time used: 0.030114
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.004688s
Time used: 4.00332
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.011125s
Time used: 4.00186
Solving with 3 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.017392s
Time used: 1.00127
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.461969s
Time used: 0.459644
Improving Solution with cost 1 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.001633s
Time used: 1.00162

LOG: SAT solveNonLinear - Elapsed time: 1.463602s
Cost: 1; Total time: 1.46127
Termination implied by a set of invariant(s):
Invariant at l8: arg3 <= 23
[ Invariant Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l8, l8, 1 <= arg1 /\ 1 <= undef85 /\ 1 <= undef92 /\ undef92 <= arg1 /\ undef85 <= undef92 /\ 2 + arg2 <= undef91 /\ 13 <= arg3 /\ arg3 <= 23, {arg1 -> undef85, arg2 -> 1 + arg2, arg3 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l8, l8, 1 <= arg1 /\ 1 <= undef98 /\ undef98 <= arg1 /\ arg3 <= 11, {arg1 -> undef98, arg3 -> 1 + arg3, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l8, l8, 1 <= arg1 /\ 1 <= undef104 /\ undef104 <= arg1 /\ arg3 = 12, {arg1 -> undef104, arg3 -> 13, rest remain the same}>
[ Termination Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l8, l8, 1 <= arg1 /\ 1 <= undef85 /\ 1 <= undef92 /\ undef92 <= arg1 /\ undef85 <= undef92 /\ 2 + arg2 <= undef91 /\ 13 <= arg3 /\ 50001 + 50000*arg1 <= arg2 /\ 50001 <= arg2 /\ arg3 <= 23, {arg1 -> undef85, arg2 -> 1 + arg2, arg3 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l8, l8, 1 <= arg1 /\ 1 <= undef98 /\ undef98 <= arg1 /\ arg3 <= 11, {arg1 -> undef98, arg3 -> 1 + arg3, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l8, l8, 1 <= arg1 /\ 1 <= undef104 /\ undef104 <= arg1 /\ arg3 = 12, {arg1 -> undef104, arg3 -> 13, rest remain the same}>
Quasi-ranking function: 50000 + 1200000*arg1 - 24*arg2 - arg3
New Graphs: 
Transitions:
<l8, l8, 1 <= arg1 /\ 1 <= undef85 /\ 1 <= undef92 /\ undef92 <= arg1 /\ undef85 <= undef92 /\ 2 + arg2 <= undef91 /\ 13 <= arg3 /\ 50001 + 50000*arg1 <= arg2 /\ 50001 + 1200000*arg1 <= 24*arg2 + arg3 /\ 50001 <= arg2 /\ arg3 <= 23, {arg1 -> undef85, arg2 -> 1 + arg2, arg3 -> 0, rest remain the same}>
<l8, l8, 1 <= arg1 /\ 1 <= undef98 /\ undef98 <= arg1 /\ arg3 <= 11 /\ 50001 + 1200000*arg1 <= 24*arg2 + arg3, {arg1 -> undef98, arg3 -> 1 + arg3, rest remain the same}>
<l8, l8, 1 <= arg1 /\ 1 <= undef104 /\ undef104 <= arg1 /\ 50001 + 1200000*arg1 <= 24*arg2 + arg3 /\ arg3 = 12, {arg1 -> undef104, arg3 -> 13, rest remain the same}>
Variables:
arg1, arg2, arg3
Checking conditional termination of SCC {l8}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001979s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.230399s
Trying to remove transition: <l8, l8, 1 <= arg1 /\ 1 <= undef104 /\ undef104 <= arg1 /\ 50001 + 1200000*arg1 <= 24*arg2 + arg3 /\ arg3 = 12, {arg1 -> undef104, arg3 -> 13, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.004707s
Time used: 4.00364
Trying to remove transition: <l8, l8, 1 <= arg1 /\ 1 <= undef98 /\ undef98 <= arg1 /\ arg3 <= 11 /\ 50001 + 1200000*arg1 <= 24*arg2 + arg3, {arg1 -> undef98, arg3 -> 1 + arg3, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.025803s
Time used: 4.00344
Trying to remove transition: <l8, l8, 1 <= arg1 /\ 1 <= undef85 /\ 1 <= undef92 /\ undef92 <= arg1 /\ undef85 <= undef92 /\ 2 + arg2 <= undef91 /\ 13 <= arg3 /\ 50001 + 50000*arg1 <= arg2 /\ 50001 + 1200000*arg1 <= 24*arg2 + arg3 /\ 50001 <= arg2 /\ arg3 <= 23, {arg1 -> undef85, arg2 -> 1 + arg2, arg3 -> 0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.026949s
Time used: 4.00425
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.007025s
Time used: 4.00397
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.035510s
Time used: 4.00988
Solving with 3 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.007715s
Time used: 1.00002
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.067167s
Time used: 0.063056
Improving Solution with cost 1 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.003077s
Time used: 1.00306

LOG: SAT solveNonLinear - Elapsed time: 1.070244s
Cost: 1; Total time: 1.06611
Termination implied by a set of invariant(s):
Invariant at l8: 0 <= arg2
[ Invariant Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l8, l8, 1 <= arg1 /\ 1 <= undef85 /\ 1 <= undef92 /\ undef92 <= arg1 /\ 0 <= arg2 /\ undef85 <= undef92 /\ 2 + arg2 <= undef91 /\ 13 <= arg3 /\ arg3 <= 23, {arg1 -> undef85, arg2 -> 1 + arg2, arg3 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l8, l8, 1 <= arg1 /\ 1 <= undef98 /\ undef98 <= arg1 /\ 0 <= arg2 /\ arg3 <= 11, {arg1 -> undef98, arg3 -> 1 + arg3, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l8, l8, 1 <= arg1 /\ 1 <= undef104 /\ undef104 <= arg1 /\ 0 <= arg2 /\ arg3 = 12, {arg1 -> undef104, arg3 -> 13, rest remain the same}>
[ Termination Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l8, l8, 1 <= arg1 /\ 1 <= undef85 /\ 1 <= undef92 /\ undef92 <= arg1 /\ undef85 <= undef92 /\ 2 + arg2 <= undef91 /\ 13 <= arg3 /\ 50001 + 50000*arg1 <= arg2 /\ 50001 + 1200000*arg1 <= 24*arg2 + arg3 /\ 50001 <= arg2 /\ arg3 <= 23, {arg1 -> undef85, arg2 -> 1 + arg2, arg3 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l8, l8, 1 <= arg1 /\ 1 <= undef98 /\ undef98 <= arg1 /\ 0 <= arg2 /\ arg3 <= 11 /\ 50001 + 1200000*arg1 <= 24*arg2 + arg3, {arg1 -> undef98, arg3 -> 1 + arg3, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l8, l8, 1 <= arg1 /\ 1 <= undef104 /\ undef104 <= arg1 /\ 0 <= arg2 /\ 50001 + 1200000*arg1 <= 24*arg2 + arg3 /\ arg3 = 12, {arg1 -> undef104, arg3 -> 13, rest remain the same}>
Quasi-ranking function: 50000 - 23*arg2 - arg3
New Graphs: 
Transitions:
<l8, l8, 1 <= arg1 /\ 1 <= undef85 /\ 1 <= undef92 /\ undef92 <= arg1 /\ undef85 <= undef92 /\ 2 + arg2 <= undef91 /\ 13 <= arg3 /\ 50001 + 50000*arg1 <= arg2 /\ 50001 + 1200000*arg1 <= 24*arg2 + arg3 /\ 50001 <= arg2 /\ arg3 <= 23, {arg1 -> undef85, arg2 -> 1 + arg2, arg3 -> 0, rest remain the same}>
<l8, l8, 1 <= arg1 /\ 1 <= undef98 /\ undef98 <= arg1 /\ 0 <= arg2 /\ arg3 <= 11 /\ 50001 + 1200000*arg1 <= 24*arg2 + arg3 /\ 50001 <= 23*arg2 + arg3, {arg1 -> undef98, arg3 -> 1 + arg3, rest remain the same}>
<l8, l8, 1 <= arg1 /\ 1 <= undef104 /\ undef104 <= arg1 /\ 0 <= arg2 /\ 50001 + 1200000*arg1 <= 24*arg2 + arg3 /\ 50001 <= 23*arg2 + arg3 /\ arg3 = 12, {arg1 -> undef104, arg3 -> 13, rest remain the same}>
Variables:
arg1, arg2, arg3
Checking conditional termination of SCC {l8}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002319s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.613621s
Trying to remove transition: <l8, l8, 1 <= arg1 /\ 1 <= undef104 /\ undef104 <= arg1 /\ 0 <= arg2 /\ 50001 + 1200000*arg1 <= 24*arg2 + arg3 /\ 50001 <= 23*arg2 + arg3 /\ arg3 = 12, {arg1 -> undef104, arg3 -> 13, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.006672s
Time used: 4.00535
Trying to remove transition: <l8, l8, 1 <= arg1 /\ 1 <= undef98 /\ undef98 <= arg1 /\ 0 <= arg2 /\ arg3 <= 11 /\ 50001 + 1200000*arg1 <= 24*arg2 + arg3 /\ 50001 <= 23*arg2 + arg3, {arg1 -> undef98, arg3 -> 1 + arg3, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.029534s
Time used: 4.00471
Trying to remove transition: <l8, l8, 1 <= arg1 /\ 1 <= undef85 /\ 1 <= undef92 /\ undef92 <= arg1 /\ undef85 <= undef92 /\ 2 + arg2 <= undef91 /\ 13 <= arg3 /\ 50001 + 50000*arg1 <= arg2 /\ 50001 + 1200000*arg1 <= 24*arg2 + arg3 /\ 50001 <= arg2 /\ arg3 <= 23, {arg1 -> undef85, arg2 -> 1 + arg2, arg3 -> 0, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.019820s
Time used: 4.00511
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.010285s
Time used: 4.00485
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.014266s
Time used: 4.0033
Solving with 3 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.010935s
Time used: 1.00006
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.006690s
Time used: 4.0046
Termination failed. Trying to show unreachability...
Proving unreachability of entry: <l2, l8, 1 <= arg1 /\ 1 <= undef23 /\ 1 <= undef42 /\ 1 <= undef85 /\ 1 <= undef91 /\ undef48 <= 1 /\ undef23 <= arg1 /\ undef42 <= undef23 /\ undef85 <= undef42 /\ 13 <= arg2, {arg1 -> undef85, arg2 -> 0, arg3 -> 0, rest remain the same}>

LOG: CALL check - Post:1 <= 0 - Process 1
* Exit transition: <l2, l8, 1 <= arg1 /\ 1 <= undef23 /\ 1 <= undef42 /\ 1 <= undef85 /\ 1 <= undef91 /\ undef48 <= 1 /\ undef23 <= arg1 /\ undef42 <= undef23 /\ undef85 <= undef42 /\ 13 <= arg2, {arg1 -> undef85, arg2 -> 0, arg3 -> 0, rest remain the same}>
* Postcondition  : 1 <= 0
Postcodition moved up: 1 <= 0

LOG: Try proving POST
Postcondition: 1 <= 0

LOG: CALL check - Post:1 <= 0 - Process 2
* Exit transition: <l0, l2, 1 <= undef1 /\ 1 <= undef23 /\ 1 <= undef42 /\ 1 <= undef85 /\ 1 <= undef91 /\ 1 <= undef198 /\ undef48 <= 1 /\ undef1 <= undef198 /\ undef42 <= undef23 /\ undef85 <= undef42 /\ 0 <= undef199 /\ arg1 = undef1 /\ arg2 = 0 /\ arg3 = undef3, {all remain the same}>
* Postcondition  : 1 <= 0

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002336s
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 0.002432s

LOG: NarrowEntry size 1
Narrowing transition: 
<l2, l2, 1 <= arg1 /\ 1 + arg2 <= undef14 /\ 1 <= undef7 /\ 1 <= undef13 /\ arg2 <= 1 /\ undef7 <= arg1 /\ 0 <= undef14, {arg1 -> undef7, arg2 -> 1 + arg2, arg3 -> undef9, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l2, l2, 1 <= arg1 /\ 1 + arg2 <= undef22 /\ 1 <= undef15 /\ 1 <= undef21 /\ undef15 <= arg1 /\ 0 <= undef22 /\ 2 <= arg2 /\ arg2 <= 12, {arg1 -> undef15, arg2 -> 1 + arg2, arg3 -> undef17, rest remain the same}>

LOG: Narrow transition size 1
ENTRIES:
<l0, l2, 1 <= undef1 /\ 1 <= undef23 /\ 1 <= undef42 /\ 1 <= undef85 /\ 1 <= undef91 /\ 1 <= undef198 /\ undef48 <= 1 /\ 0 <= 0 /\ undef1 <= undef198 /\ undef42 <= undef23 /\ undef85 <= undef42 /\ 0 <= undef199 /\ arg1 = undef1 /\ arg2 = 0 /\ arg3 = undef3, {all remain the same}>
END ENTRIES:
GRAPH:
<l2, l2, 1 <= arg1 /\ 1 + arg2 <= undef14 /\ 1 <= undef7 /\ 1 <= undef13 /\ 1 <= undef23 /\ 1 <= undef42 /\ 1 <= undef85 /\ 1 <= undef91 /\ arg2 <= 1 /\ undef48 <= 1 /\ 0 <= 0 /\ undef7 <= arg1 /\ 0 <= undef14 /\ undef42 <= undef23 /\ undef85 <= undef42, {arg1 -> undef7, arg2 -> 1 + arg2, arg3 -> undef9, rest remain the same}>
<l2, l2, 1 <= arg1 /\ 1 + arg2 <= undef22 /\ 1 <= undef15 /\ 1 <= undef21 /\ 1 <= undef23 /\ 1 <= undef42 /\ 1 <= undef85 /\ 1 <= undef91 /\ undef48 <= 1 /\ 0 <= 0 /\ undef15 <= arg1 /\ 0 <= undef22 /\ undef42 <= undef23 /\ undef85 <= undef42 /\ 2 <= arg2 /\ arg2 <= 12, {arg1 -> undef15, arg2 -> 1 + arg2, arg3 -> undef17, rest remain the same}>
END GRAPH:
EXIT: <l2, l8, 1 <= arg1 /\ 1 <= undef23 /\ 1 <= undef42 /\ 1 <= undef85 /\ 1 <= undef91 /\ undef48 <= 1 /\ undef23 <= arg1 /\ undef42 <= undef23 /\ undef85 <= undef42 /\ 13 <= arg2, {arg1 -> undef85, arg2 -> 0, arg3 -> 0, rest remain the same}>
POST: 1 <= 0


LOG: Try proving POST
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.058448s
Time used: 0.058365
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.011691s
Time used: 4.00413
Solving with 3 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.007524s
Time used: 1.0035

LOG: Postcondition is not implied - no solution
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 5.116295s
Cannot prove unreachability

Proving non-termination of subgraph 3
Transitions:
<l8, l8, 1 <= arg1 /\ 1 <= undef85 /\ 1 <= undef92 /\ undef92 <= arg1 /\ undef85 <= undef92 /\ 2 + arg2 <= undef91 /\ 13 <= arg3, {arg1 -> undef85, arg2 -> 1 + arg2, arg3 -> 0, rest remain the same}>
<l8, l8, 1 <= arg1 /\ 1 <= undef98 /\ undef98 <= arg1 /\ arg3 <= 11, {arg1 -> undef98, arg3 -> 1 + arg3, rest remain the same}>
<l8, l8, 1 <= arg1 /\ 1 <= undef104 /\ undef104 <= arg1 /\ arg3 = 12, {arg1 -> undef104, arg3 -> 13, rest remain the same}>
Variables:
arg1, arg2, arg3

Checking that every undef value has an assignment...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.003696s
Checking conditional non-termination of SCC {l8}...
EXIT TRANSITIONS:
<l8, end, arg1 <= 0 /\ 13 <= arg3, {all remain the same}>
<l8, end, arg1 <= 0 /\ arg3 <= 12, {all remain the same}>

Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.041767s
Time used: 0.04163

LOG: SAT solveNonLinear - Elapsed time: 0.041767s
Cost: 0; Total time: 0.04163
Minimizing number of undef constraints...

LOG: CALL solveNonLinear

LOG: RETURN solveNonLinear - Elapsed time: 0.019469s
Number of undef constraints reduced!

Non-termination implied by a set of quasi-invariant(s):
Quasi-invariant at l8: 1 <= arg1

Strengthening and disabling EXIT transitions...
Closed exits from l8: 2

Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l8, l8, 1 <= arg1 /\ 1 <= undef85 /\ 1 <= undef92 /\ undef92 <= arg1 /\ undef85 <= undef92 /\ 2 + arg2 <= undef91 /\ 13 <= arg3, {arg1 -> undef85, arg2 -> 1 + arg2, arg3 -> 0, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l8, l8, 1 <= arg1 /\ 1 <= undef98 /\ undef98 <= arg1 /\ arg3 <= 11, {arg1 -> undef98, arg3 -> 1 + arg3, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l8, l8, 1 <= arg1 /\ 1 <= undef104 /\ undef104 <= arg1 /\ arg3 = 12, {arg1 -> undef104, arg3 -> 13, rest remain the same}>

Calling reachability with...
Transition: <l8, end, true, {all remain the same}>
Conditions: 1 <= arg1, 
Transition: <l8, end, true, {all remain the same}>
Conditions: 1 <= arg1, 
OPEN EXITS: 
<l8, end, 1 <= arg1, {all remain the same}>
<l8, end, 1 <= arg1, {all remain the same}>

--- Reachability graph ---
> Graph without transitions.

Calling reachability with...
Transition: <l2, l8, 1 <= arg1 /\ 1 <= undef23 /\ 1 <= undef42 /\ 1 <= undef85 /\ 1 <= undef91 /\ undef48 <= 1 /\ undef23 <= arg1 /\ undef42 <= undef23 /\ undef85 <= undef42 /\ 13 <= arg2, {arg1 -> undef85, arg2 -> 0, arg3 -> 0, rest remain the same}>
Conditions: 1 <= arg1, 
Transition: <l2, l8, 1 <= arg1 /\ 1 <= undef23 /\ 1 <= undef42 /\ 1 <= undef85 /\ 1 <= undef91 /\ undef48 <= 1 /\ undef23 <= arg1 /\ undef42 <= undef23 /\ undef85 <= undef42 /\ 13 <= arg2, {arg1 -> undef85, arg2 -> 0, arg3 -> 0, rest remain the same}>
Conditions: 1 <= arg1, 
OPEN EXITS: 
<l2, l8, 1 <= arg1 /\ undef23 <= arg1 /\ 13 <= arg2, {arg1 -> undef85, arg2 -> 0, arg3 -> 0, rest remain the same}> (condsUp: 1 <= undef23, 1 <= undef42, 1 <= undef85, 1 <= undef91, undef48 <= 1, undef42 <= undef23, undef85 <= undef42, 1 <= undef85)
<l2, l8, 1 <= arg1 /\ undef23 <= arg1 /\ 13 <= arg2, {arg1 -> undef85, arg2 -> 0, arg3 -> 0, rest remain the same}> (condsUp: 1 <= undef23, 1 <= undef42, 1 <= undef85, 1 <= undef91, undef48 <= 1, undef42 <= undef23, undef85 <= undef42, 1 <= undef85)

--- Reachability graph ---
> Graph without transitions.

Calling reachability with...
Transition: <l0, l2, 1 <= undef1 /\ 1 <= undef198 /\ undef1 <= undef198 /\ 0 <= undef199 /\ arg1 = undef1 /\ arg2 = 0 /\ arg3 = undef3, {all remain the same}>
Conditions: 1 <= arg1, undef23 <= arg1, 13 <= arg2, 1 <= undef23, 1 <= undef42, 1 <= undef85, 1 <= undef91, undef48 <= 1, undef42 <= undef23, undef85 <= undef42, 1 <= undef85, 
Transition: <l0, l2, 1 <= undef1 /\ 1 <= undef198 /\ undef1 <= undef198 /\ 0 <= undef199 /\ arg1 = undef1 /\ arg2 = 0 /\ arg3 = undef3, {all remain the same}>
Conditions: 1 <= arg1, undef23 <= arg1, 13 <= arg2, 1 <= undef23, 1 <= undef42, 1 <= undef85, 1 <= undef91, undef48 <= 1, undef42 <= undef23, undef85 <= undef42, 1 <= undef85, 
OPEN EXITS: 

> Conditions are not feasible after transitions.
--- Reachability graph ---
Transitions:
<l2, l2, 1 <= arg1 /\ 1 + arg2 <= undef14 /\ 1 <= undef7 /\ 1 <= undef13 /\ arg2 <= 1 /\ undef7 <= arg1 /\ 0 <= undef14, {arg1 -> undef7, arg2 -> 1 + arg2, arg3 -> undef9, rest remain the same}>
Variables:
arg1, arg2, arg3
Checking that every undef value has an assignment...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002676s
Checking edge-closing of SCC {l2}...
EXIT TRANSITIONS (TO CLOSE):
<l2, end, 1 <= arg1 /\ 2 <= arg2 /\ arg2 <= 12, {all remain the same}>
<l2, end, arg1 <= 0 /\ 2 <= arg2, {all remain the same}>
<l2, end, arg2 <= 1 /\ arg1 <= 0, {all remain the same}>

Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.019574s
Time used: 0.019274
Improving Solution with cost 1 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.036010s
Time used: 0.036007

LOG: SAT solveNonLinear - Elapsed time: 0.055584s
Cost: 1; Total time: 0.055281
Minimizing number of undef constraints...

LOG: CALL solveNonLinear

LOG: RETURN solveNonLinear - Elapsed time: 0.019103s
Number of undef constraints reduced!

Edge-closing implied by a set of quasi-invariant(s):
Quasi-invariant at l2: 1 <= arg1

Strengthening and disabling EXIT transitions...
EXIT TRANSITIONS TO BE CLOSED:
Closed exits from l2: 2
Strengthening exit transition (result): 
<l2, end, 1 <= arg1 /\ 2 <= arg2 /\ arg2 <= 12, {all remain the same}>
EXIT TRANSITIONS TO KEEP OPEN:
Strengthening exit transition (result): 
<l2, l8, 1 <= arg1 /\ undef23 <= arg1 /\ 13 <= arg2, {arg1 -> undef85, arg2 -> 0, arg3 -> 0, rest remain the same}>
Strengthening exit transition (result): 
<l2, l8, 1 <= arg1 /\ undef23 <= arg1 /\ 13 <= arg2, {arg1 -> undef85, arg2 -> 0, arg3 -> 0, rest remain the same}>

Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l2, l2, 1 <= arg1 /\ 1 + arg2 <= undef14 /\ 1 <= undef7 /\ 1 <= undef13 /\ arg2 <= 1 /\ undef7 <= arg1 /\ 0 <= undef14, {arg1 -> undef7, arg2 -> 1 + arg2, arg3 -> undef9, rest remain the same}>

Checking edge-closing of SCC {l2}...
EXIT TRANSITIONS (TO CLOSE):
<l2, end, 1 <= arg1 /\ 2 <= arg2 /\ arg2 <= 12, {all remain the same}>

Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.039260s
Time used: 0.039179
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 5.014119s
Time used: 5.00251
Solving with 3 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 5.010756s
Time used: 5.00186
> No quasi-invariants that block all exits have been found.
--- Reachability graph ---
Transitions:
<l2, l2, 1 <= arg1 /\ 1 + arg2 <= undef22 /\ 1 <= undef15 /\ 1 <= undef21 /\ undef15 <= arg1 /\ 0 <= undef22 /\ 2 <= arg2 /\ arg2 <= 12, {arg1 -> undef15, arg2 -> 1 + arg2, arg3 -> undef17, rest remain the same}>
Variables:
arg1, arg2, arg3
Checking that every undef value has an assignment...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.003159s
Checking edge-closing of SCC {l2}...
EXIT TRANSITIONS (TO CLOSE):
<l2, end, 1 <= arg1 /\ arg2 <= 1, {all remain the same}>
<l2, end, arg1 <= 0 /\ 2 <= arg2, {all remain the same}>
<l2, end, arg2 <= 1 /\ arg1 <= 0, {all remain the same}>

Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.020567s
Time used: 0.02025
Improving Solution with cost 1 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.035586s
Time used: 0.035583

LOG: SAT solveNonLinear - Elapsed time: 0.056153s
Cost: 1; Total time: 0.055833
Minimizing number of undef constraints...

LOG: CALL solveNonLinear

LOG: RETURN solveNonLinear - Elapsed time: 0.019877s
Number of undef constraints reduced!

Edge-closing implied by a set of quasi-invariant(s):
Quasi-invariant at l2: 1 <= arg1

Strengthening and disabling EXIT transitions...
EXIT TRANSITIONS TO BE CLOSED:
Closed exits from l2: 2
Strengthening exit transition (result): 
<l2, end, 1 <= arg1 /\ arg2 <= 1, {all remain the same}>
EXIT TRANSITIONS TO KEEP OPEN:
Strengthening exit transition (result): 
<l2, l8, 1 <= arg1 /\ undef23 <= arg1 /\ 13 <= arg2, {arg1 -> undef85, arg2 -> 0, arg3 -> 0, rest remain the same}>
Strengthening exit transition (result): 
<l2, l8, 1 <= arg1 /\ undef23 <= arg1 /\ 13 <= arg2, {arg1 -> undef85, arg2 -> 0, arg3 -> 0, rest remain the same}>

Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l2, l2, 1 <= arg1 /\ 1 + arg2 <= undef22 /\ 1 <= undef15 /\ 1 <= undef21 /\ undef15 <= arg1 /\ 0 <= undef22 /\ 2 <= arg2 /\ arg2 <= 12, {arg1 -> undef15, arg2 -> 1 + arg2, arg3 -> undef17, rest remain the same}>

Checking edge-closing of SCC {l2}...
EXIT TRANSITIONS (TO CLOSE):
<l2, end, 1 <= arg1 /\ arg2 <= 1, {all remain the same}>

Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.013333s
Time used: 0.01325
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 5.010733s
Time used: 5.00447
Solving with 3 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 5.010942s
Time used: 5.00197
> No quasi-invariants that block all exits have been found.
--- Reachability graph ---
Transitions:
<l2, l2, 1 <= arg1 /\ 1 + arg2 <= undef22 /\ 1 <= undef15 /\ 1 <= undef21 /\ undef15 <= arg1 /\ 0 <= undef22 /\ 2 <= arg2 /\ arg2 <= 12, {arg1 -> undef15, arg2 -> 1 + arg2, arg3 -> undef17, rest remain the same}>
<l2, l2, 1 <= arg1 /\ 1 + arg2 <= undef14 /\ 1 <= undef7 /\ 1 <= undef13 /\ arg2 <= 1 /\ undef7 <= arg1 /\ 0 <= undef14, {arg1 -> undef7, arg2 -> 1 + arg2, arg3 -> undef9, rest remain the same}>
Variables:
arg1, arg2, arg3
Checking that every undef value has an assignment...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.004255s
Checking edge-closing of SCC {l2}...
EXIT TRANSITIONS (TO CLOSE):
<l2, end, arg1 <= 0 /\ 2 <= arg2, {all remain the same}>
<l2, end, arg2 <= 1 /\ arg1 <= 0, {all remain the same}>

Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.038690s
Time used: 0.038548

LOG: SAT solveNonLinear - Elapsed time: 0.038690s
Cost: 0; Total time: 0.038548
Minimizing number of undef constraints...

LOG: CALL solveNonLinear

LOG: RETURN solveNonLinear - Elapsed time: 0.017188s
Number of undef constraints reduced!

Edge-closing implied by a set of quasi-invariant(s):
Quasi-invariant at l2: 1 <= arg1

Strengthening and disabling EXIT transitions...
EXIT TRANSITIONS TO BE CLOSED:
Closed exits from l2: 2
EXIT TRANSITIONS TO KEEP OPEN:
Strengthening exit transition (result): 
<l2, l8, 1 <= arg1 /\ undef23 <= arg1 /\ 13 <= arg2, {arg1 -> undef85, arg2 -> 0, arg3 -> 0, rest remain the same}>
Strengthening exit transition (result): 
<l2, l8, 1 <= arg1 /\ undef23 <= arg1 /\ 13 <= arg2, {arg1 -> undef85, arg2 -> 0, arg3 -> 0, rest remain the same}>

Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l2, l2, 1 <= arg1 /\ 1 + arg2 <= undef22 /\ 1 <= undef15 /\ 1 <= undef21 /\ undef15 <= arg1 /\ 0 <= undef22 /\ 2 <= arg2 /\ arg2 <= 12, {arg1 -> undef15, arg2 -> 1 + arg2, arg3 -> undef17, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l2, l2, 1 <= arg1 /\ 1 + arg2 <= undef14 /\ 1 <= undef7 /\ 1 <= undef13 /\ arg2 <= 1 /\ undef7 <= arg1 /\ 0 <= undef14, {arg1 -> undef7, arg2 -> 1 + arg2, arg3 -> undef9, rest remain the same}>

Checking conditional termination of SCC {l2}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.003879s
Ranking function: 22 - 22*arg2
New Graphs: 
Transitions:
<l2, l2, 1 <= arg1 /\ 1 + arg2 <= undef22 /\ 1 <= undef15 /\ 1 <= undef21 /\ undef15 <= arg1 /\ 0 <= undef22 /\ 2 <= arg2 /\ arg2 <= 12, {arg1 -> undef15, arg2 -> 1 + arg2, arg3 -> undef17, rest remain the same}>
Variables:
arg1, arg2, arg3
Checking conditional termination of SCC {l2}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.003085s
Ranking function: 12 - arg2
New Graphs: 
Calling reachability with...
Transition: <l0, l2, 1 <= undef1 /\ 1 <= undef198 /\ undef1 <= undef198 /\ 0 <= undef199 /\ arg1 = undef1 /\ arg2 = 0 /\ arg3 = undef3, {all remain the same}>
Conditions: 1 <= arg1, 1 <= undef23, 1 <= undef42, 1 <= undef85, 1 <= undef91, undef48 <= 1, undef42 <= undef23, undef85 <= undef42, 1 <= undef85, 
Transition: <l0, l2, 1 <= undef1 /\ 1 <= undef198 /\ undef1 <= undef198 /\ 0 <= undef199 /\ arg1 = undef1 /\ arg2 = 0 /\ arg3 = undef3, {all remain the same}>
Conditions: 1 <= arg1, 1 <= undef23, 1 <= undef42, 1 <= undef85, 1 <= undef91, undef48 <= 1, undef42 <= undef23, undef85 <= undef42, 1 <= undef85, 
OPEN EXITS: 
<l0, l2, 1 <= arg1 /\ 1 <= undef1 /\ 1 <= undef23 /\ 1 <= undef42 /\ 1 <= undef85 /\ 1 <= undef91 /\ 1 <= undef198 /\ undef48 <= 1 /\ undef1 <= undef198 /\ undef42 <= undef23 /\ undef85 <= undef42 /\ 0 <= undef199 /\ arg1 = undef1 /\ arg2 = 0 /\ arg3 = undef3, {all remain the same}>
<l0, l2, 1 <= arg1 /\ 1 <= undef1 /\ 1 <= undef23 /\ 1 <= undef42 /\ 1 <= undef85 /\ 1 <= undef91 /\ 1 <= undef198 /\ undef48 <= 1 /\ undef1 <= undef198 /\ undef42 <= undef23 /\ undef85 <= undef42 /\ 0 <= undef199 /\ arg1 = undef1 /\ arg2 = 0 /\ arg3 = undef3, {all remain the same}>

> Conditions are reachable!

Program does NOT terminate