NO

Solver Timeout: 4
Global Timeout: 300
No parsing errors!
Init Location: 0
Transitions:
<l0, l20, true>
<l1, l2, (undef1 <= arg1) /\ (undef3 <= arg3) /\ (undef4 <= arg4) /\ (arg1 > 4) /\ (arg3 > 0) /\ (arg4 > 2) /\ (undef1 > 4) /\ (undef3 > 0) /\ (undef4 > 2) /\ ((undef6 + 4) <= arg1) /\ ((arg6 + 4) <= arg1) /\ (arg3 >= (undef8 + 2)) /\ ((arg7 + 2) <= arg4), par{arg1 -> undef1, arg3 -> undef3, arg4 -> undef4, arg6 -> undef6, arg7 -> arg6, arg8 -> undef8, arg9 -> arg7}>
<l3, l4, (undef10 <= arg1) /\ (arg2 > ~(1)) /\ (arg1 > 0) /\ (undef10 > 0) /\ (undef11 > ~(1)), par{arg1 -> undef10, arg2 -> undef11, arg3 -> undef12, arg4 -> undef13, arg5 -> undef14, arg6 -> undef15, arg7 -> undef16, arg8 -> undef17, arg9 -> undef18}>
<l5, l4, (undef19 <= arg1) /\ (undef28 > ~(1)) /\ ((undef20 + 1) <= arg1) /\ (arg1 > 0) /\ (undef19 > 0) /\ (undef20 > ~(1)), par{arg1 -> undef19, arg2 -> undef20, arg3 -> undef21, arg4 -> undef22, arg5 -> undef23, arg6 -> undef24, arg7 -> undef25, arg8 -> undef26, arg9 -> undef27}>
<l4, l6, (undef29 <= arg1) /\ (undef31 >= undef38) /\ ((undef29 - 1) <= arg2) /\ (undef30 <= arg2) /\ (arg1 > 0) /\ (arg2 > ~(1)) /\ (undef29 > 0) /\ (undef30 > ~(1)), par{arg1 -> undef29, arg2 -> undef30, arg3 -> undef31, arg4 -> undef32, arg5 -> undef33, arg6 -> undef34, arg7 -> undef35, arg8 -> undef36, arg9 -> undef37}>
<l4, l6, (undef48 < undef49) /\ (undef48 > ~(1)) /\ (undef39 <= arg1) /\ ((undef39 - 1) <= arg2) /\ (undef40 <= arg2) /\ (arg1 > 0) /\ (arg2 > ~(1)) /\ (undef39 > 0) /\ (undef40 > ~(1)), par{arg1 -> undef39, arg2 -> undef40, arg3 -> (undef48 + 1), arg4 -> undef42, arg5 -> undef43, arg6 -> undef44, arg7 -> undef45, arg8 -> undef46, arg9 -> undef47}>
<l6, l7, (arg3 >= undef59) /\ (undef59 > ~(1)) /\ (undef50 <= arg1) /\ (undef50 <= arg2) /\ (arg1 > 0) /\ (arg2 > 0) /\ (undef50 > 0) /\ (undef51 > 1), par{arg1 -> undef50, arg2 -> undef51, arg3 -> undef52, arg4 -> undef53, arg5 -> undef54, arg6 -> undef55, arg7 -> undef56, arg8 -> undef57, arg9 -> undef58}>
<l4, l8, (undef69 < undef70) /\ (undef69 > ~(1)) /\ (undef70 > 0) /\ (undef62 > ~(1)) /\ ((undef69 + 1) <= undef70) /\ (undef60 <= arg1) /\ (undef60 <= arg2) /\ (arg1 > 0) /\ (arg2 > 0) /\ (undef60 > 0) /\ (undef61 > 1), par{arg1 -> undef60, arg2 -> undef61, arg3 -> undef62, arg4 -> (undef69 + 1), arg5 -> undef64, arg6 -> undef65, arg7 -> undef66, arg8 -> undef67, arg9 -> undef68}>
<l7, l9, (undef71 <= arg2) /\ (undef80 >= undef81) /\ (arg1 > 0) /\ (arg2 > 1) /\ (undef71 > 1) /\ ((arg3 + 2) <= arg2), par{arg1 -> undef71, arg2 -> 0, arg3 -> undef73, arg4 -> undef74, arg5 -> undef75, arg6 -> undef76, arg7 -> undef77, arg8 -> undef78, arg9 -> undef79}>
<l7, l10, (undef91 < undef92) /\ (undef91 > ~(1)) /\ (undef82 <= arg1) /\ ((undef82 + 1) <= arg2) /\ (undef83 <= arg2) /\ (arg1 > 0) /\ (arg2 > 1) /\ (undef82 > 0) /\ (undef83 > 1) /\ ((arg3 + 2) <= arg2), par{arg1 -> undef82, arg2 -> undef83, arg3 -> 0, arg4 -> (undef91 + 1), arg5 -> arg3, arg6 -> undef87, arg7 -> undef88, arg8 -> undef89, arg9 -> undef90}>
<l7, l10, (undef102 < undef103) /\ (undef102 > ~(1)) /\ (undef95 > ~(1)) /\ (undef93 <= arg1) /\ ((undef93 + 1) <= arg2) /\ (undef94 <= arg2) /\ (arg1 > 0) /\ (arg2 > 1) /\ (undef93 > 0) /\ (undef94 > 1) /\ ((arg3 + 2) <= arg2), par{arg1 -> undef93, arg2 -> undef94, arg3 -> undef95, arg4 -> (undef102 + 1), arg5 -> arg3, arg6 -> undef98, arg7 -> undef99, arg8 -> undef100, arg9 -> undef101}>
<l8, l11, (undef104 <= arg1) /\ (undef113 > ~(1)) /\ ((undef104 - 1) <= arg2) /\ (undef105 <= arg2) /\ (arg1 > 0) /\ (arg2 > ~(1)) /\ (undef104 > 0) /\ (undef105 > ~(1)) /\ (0 = arg3), par{arg1 -> undef104, arg2 -> undef105, arg3 -> undef106, arg4 -> undef107, arg5 -> undef108, arg6 -> undef109, arg7 -> undef110, arg8 -> undef111, arg9 -> undef112}>
<l10, l9, (arg4 <= undef123) /\ (undef123 > 0) /\ (arg4 > 0) /\ (undef114 <= arg2) /\ (arg1 > 0) /\ (arg2 > 1) /\ (undef114 > 1) /\ ((arg5 + 2) <= arg2), par{arg1 -> undef114, arg2 -> arg3, arg3 -> undef116, arg4 -> undef117, arg5 -> undef118, arg6 -> undef119, arg7 -> undef120, arg8 -> undef121, arg9 -> undef122}>
<l8, l8, (undef124 <= arg1) /\ (arg3 > 0) /\ (undef124 <= arg2) /\ (arg1 > 0) /\ (arg2 > 0) /\ (undef124 > 0) /\ (undef125 > ~(1)), par{arg1 -> undef124, arg2 -> undef125, arg5 -> undef128, arg6 -> undef129, arg7 -> undef130, arg8 -> undef131, arg9 -> undef132}>
<l11, l12, (undef133 <= arg1) /\ (undef135 >= undef142) /\ ((undef133 - 1) <= arg2) /\ (undef134 <= arg2) /\ (arg1 > 0) /\ (arg2 > ~(1)) /\ (undef133 > 0) /\ (undef134 > ~(1)), par{arg1 -> undef133, arg2 -> undef134, arg3 -> undef135, arg4 -> undef136, arg5 -> undef137, arg6 -> undef138, arg7 -> undef139, arg8 -> undef140, arg9 -> undef141}>
<l8, l11, (undef152 > ~(1)) /\ (arg3 > 0) /\ (arg1 >= undef143) /\ (arg2 >= (undef143 - 1)) /\ (arg1 >= (undef144 + 1)) /\ (arg2 >= undef144) /\ (arg1 > 0) /\ (arg2 > ~(1)) /\ (undef143 > 0) /\ (undef144 > ~(1)), par{arg1 -> undef143, arg2 -> undef144, arg3 -> undef145, arg4 -> undef146, arg5 -> undef147, arg6 -> undef148, arg7 -> undef149, arg8 -> undef150, arg9 -> undef151}>
<l12, l9, (arg3 >= undef162) /\ (undef162 > 0) /\ (arg3 > 0) /\ (undef153 <= arg2) /\ (arg1 > 0) /\ (arg2 > 0) /\ (undef153 > 0), par{arg1 -> undef153, arg2 -> 0, arg3 -> undef155, arg4 -> undef156, arg5 -> undef157, arg6 -> undef158, arg7 -> undef159, arg8 -> undef160, arg9 -> undef161}>
<l11, l12, (undef172 < undef173) /\ (undef172 > 0) /\ (undef163 <= arg1) /\ ((undef163 - 1) <= arg2) /\ (undef164 <= arg2) /\ (arg1 > 0) /\ (arg2 > ~(1)) /\ (undef163 > 0) /\ (undef164 > ~(1)), par{arg1 -> undef163, arg2 -> undef164, arg3 -> (undef172 + 1), arg4 -> undef166, arg5 -> undef167, arg6 -> undef168, arg7 -> undef169, arg8 -> undef170, arg9 -> undef171}>
<l11, l9, (undef183 < undef184) /\ (undef183 > 0) /\ (undef184 > 1) /\ (undef175 > ~(1)) /\ ((undef183 + 1) <= undef184) /\ (undef174 <= arg2) /\ (arg1 > 0) /\ (arg2 > 0) /\ (undef174 > 0), par{arg1 -> undef174, arg2 -> undef175, arg3 -> undef176, arg4 -> undef177, arg5 -> undef178, arg6 -> undef179, arg7 -> undef180, arg8 -> undef181, arg9 -> undef182}>
<l3, l13, ((undef185 + 1) <= arg1) /\ (arg1 > 0) /\ (undef185 > ~(1)) /\ (0 = arg2), par{arg1 -> undef185, arg2 -> 0, arg3 -> 0, arg4 -> 0, arg5 -> 0, arg6 -> undef190, arg7 -> undef191, arg8 -> undef192, arg9 -> undef193}>
<l3, l13, ((undef194 + 1) <= arg1) /\ (arg2 > 0) /\ (arg1 > 0) /\ (undef194 > ~(1)), par{arg1 -> undef194, arg2 -> 0, arg3 -> 0, arg4 -> arg2, arg5 -> 1, arg6 -> undef199, arg7 -> undef200, arg8 -> undef201, arg9 -> undef202}>
<l3, l13, (undef205 > ~(1)) /\ (arg2 > 0) /\ ((undef203 + 1) <= arg1) /\ (arg1 > 0) /\ (undef203 > ~(1)), par{arg1 -> undef203, arg2 -> 0, arg3 -> undef205, arg4 -> arg2, arg5 -> 1, arg6 -> undef208, arg7 -> undef209, arg8 -> undef210, arg9 -> undef211}>
<l13, l13, (arg5 >= arg4) /\ (arg4 > ~(1)) /\ (arg3 > arg2) /\ ((undef212 - 2) <= arg1) /\ (arg1 > ~(1)) /\ (undef212 > 1), par{arg1 -> undef212, arg2 -> (arg2 + 1), arg6 -> undef217, arg7 -> undef218, arg8 -> undef219, arg9 -> undef220}>
<l13, l13, (arg5 >= arg4) /\ (arg4 > ~(1)) /\ (arg3 > arg2) /\ (arg1 > 0) /\ (undef221 > 4), par{arg1 -> undef221, arg2 -> (arg2 + 1), arg6 -> undef226, arg7 -> undef227, arg8 -> undef228, arg9 -> undef229}>
<l13, l14, (arg3 > arg2) /\ (arg4 > ~(1)) /\ (arg5 < arg4) /\ (arg5 > ~(1)) /\ (undef233 <= arg1) /\ (arg1 > ~(1)) /\ (undef231 > 1) /\ (undef233 > ~(1)), par{arg1 -> arg3, arg2 -> undef231, arg3 -> arg2, arg4 -> undef233, arg5 -> arg4, arg6 -> (arg5 + 1), arg7 -> undef236, arg8 -> undef237, arg9 -> undef238}>
<l13, l14, (arg3 > arg2) /\ (arg4 > ~(1)) /\ (arg5 < arg4) /\ (arg5 > ~(1)) /\ (undef248 > ~(1)) /\ (undef242 <= arg1) /\ (arg1 > ~(1)) /\ (undef240 > 1) /\ (undef242 > ~(1)), par{arg1 -> arg3, arg2 -> undef240, arg3 -> arg2, arg4 -> undef242, arg5 -> arg4, arg6 -> (arg5 + 1), arg7 -> undef245, arg8 -> undef246, arg9 -> undef247}>
<l14, l13, (undef249 <= arg2) /\ ((undef249 - 2) <= arg4) /\ (arg2 > 1) /\ (arg4 > ~(1)) /\ (undef249 > 1), par{arg1 -> undef249, arg2 -> (arg3 + 1), arg3 -> arg1, arg4 -> arg5, arg5 -> arg6, arg6 -> undef254, arg7 -> undef255, arg8 -> undef256, arg9 -> undef257}>
<l14, l13, (arg2 > 2) /\ (arg4 > 0) /\ (undef258 > 4), par{arg1 -> undef258, arg2 -> (arg3 + 1), arg3 -> arg1, arg4 -> arg5, arg5 -> arg6, arg6 -> undef263, arg7 -> undef264, arg8 -> undef265, arg9 -> undef266}>
<l6, l15, (undef267 <= arg2) /\ (arg3 >= undef276) /\ (arg1 > 0) /\ (arg2 > 0) /\ (undef267 > 0) /\ (undef268 > ~(1)) /\ ((undef269 + 2) <= arg2), par{arg1 -> undef267, arg2 -> undef268, arg3 -> undef269, arg4 -> undef270, arg5 -> undef271, arg6 -> undef272, arg7 -> undef273, arg8 -> undef274, arg9 -> undef275}>
<l4, l15, (undef286 < undef287) /\ (undef286 > ~(1)) /\ (undef287 > 0) /\ (undef288 > ~(1)) /\ ((undef286 + 1) <= undef287) /\ (undef277 <= arg2) /\ (arg1 > 0) /\ (arg2 > 0) /\ (undef277 > 0) /\ (undef278 > ~(1)) /\ ((undef279 + 2) <= arg2), par{arg1 -> undef277, arg2 -> undef278, arg3 -> undef279, arg4 -> undef280, arg5 -> undef281, arg6 -> undef282, arg7 -> undef283, arg8 -> undef284, arg9 -> undef285}>
<l15, l15, (arg1 > 2) /\ (arg2 > 0) /\ (undef289 > 0) /\ (undef290 > ~(1)) /\ ((arg3 + 2) <= arg1), par{arg1 -> undef289, arg2 -> undef290, arg3 -> undef291, arg4 -> undef292, arg5 -> undef293, arg6 -> undef294, arg7 -> undef295, arg8 -> undef296, arg9 -> undef297}>
<l9, l16, (undef298 <= arg1) /\ (arg2 > 0) /\ (arg1 > 2) /\ (undef298 > 2) /\ (undef300 > 0) /\ ((undef302 + 3) <= arg1), par{arg1 -> undef298, arg3 -> undef300, arg4 -> undef301, arg5 -> undef302, arg6 -> undef303, arg7 -> undef304, arg8 -> undef305, arg9 -> undef306}>
<l9, l17, (undef307 <= arg1) /\ (arg2 > 0) /\ (arg1 > 2) /\ (undef307 > 2) /\ (undef309 > 0), par{arg1 -> undef307, arg3 -> undef309, arg4 -> undef310, arg5 -> undef311, arg6 -> undef312, arg7 -> undef313, arg8 -> undef314, arg9 -> undef315}>
<l16, l1, (arg1 > 2) /\ (arg3 > 0) /\ (undef316 > 4) /\ (undef318 > 0) /\ (undef319 > 2) /\ ((arg5 + 3) <= arg1), par{arg1 -> undef316, arg3 -> undef318, arg4 -> undef319, arg5 -> arg4, arg6 -> undef321, arg7 -> undef322, arg8 -> undef323, arg9 -> undef324}>
<l16, l18, (arg1 > 2) /\ (arg3 > 2) /\ (undef326 > 0) /\ (undef327 > 2) /\ ((arg5 + 3) <= arg1) /\ ((arg5 + 3) <= arg3), par{arg1 -> arg2, arg2 -> undef326, arg3 -> undef327, arg5 -> undef329, arg6 -> undef330, arg7 -> undef331, arg8 -> undef332, arg9 -> undef333}>
<l17, l9, (arg2 > 0) /\ ((arg2 - 1) < arg2) /\ (arg1 > 2) /\ (arg3 > 0) /\ (undef334 > 4), par{arg1 -> undef334, arg2 -> (arg2 - 1), arg3 -> undef336, arg4 -> undef337, arg5 -> undef338, arg6 -> undef339, arg7 -> undef340, arg8 -> undef341, arg9 -> undef342}>
<l17, l19, (arg1 > 2) /\ (arg2 > 0) /\ (arg3 > 2), par{arg1 -> arg2, arg2 -> (arg2 - 1), arg3 -> arg4, arg4 -> undef346, arg5 -> undef347, arg6 -> undef348, arg7 -> undef349, arg8 -> undef350, arg9 -> undef351}>
<l1, l19, (arg1 > 4) /\ (arg2 > 0) /\ (arg3 > 4) /\ (arg4 > 4) /\ ((arg6 + 4) <= arg1) /\ ((arg6 + 4) <= arg3) /\ ((arg7 + 2) <= arg4), par{arg1 -> arg2, arg2 -> (arg2 - 1), arg3 -> arg5, arg4 -> undef355, arg5 -> undef356, arg6 -> undef357, arg7 -> undef358, arg8 -> undef359, arg9 -> undef360}>
<l18, l19, (arg2 > 2) /\ (arg1 > 0) /\ (arg3 > 2), par{arg2 -> (arg1 - 1), arg3 -> arg4, arg4 -> undef364, arg5 -> undef365, arg6 -> undef366, arg7 -> undef367, arg8 -> undef368, arg9 -> undef369}>
<l18, l9, (arg1 > 0) /\ ((arg1 - 1) < arg1) /\ (arg2 > 0) /\ (arg3 > 2) /\ (undef370 > 4), par{arg1 -> undef370, arg2 -> (arg1 - 1), arg3 -> undef372, arg4 -> undef373, arg5 -> undef374, arg6 -> undef375, arg7 -> undef376, arg8 -> undef377, arg9 -> undef378}>
<l2, l9, (arg2 > 0) /\ ((arg2 - 1) < arg2) /\ (undef379 <= arg1) /\ ((undef379 - 2) <= arg3) /\ ((undef379 - 2) <= arg4) /\ (arg1 > 4) /\ (arg3 > 2) /\ (arg4 > 2) /\ (undef379 > 4) /\ ((arg6 + 4) <= arg1) /\ ((arg8 + 2) <= arg3) /\ ((arg8 + 2) <= arg4) /\ (arg6 = arg7) /\ (arg8 = arg9), par{arg1 -> undef379, arg2 -> (arg2 - 1), arg3 -> undef381, arg4 -> undef382, arg5 -> undef383, arg6 -> undef384, arg7 -> undef385, arg8 -> undef386, arg9 -> undef387}>
<l19, l9, (arg2 < arg1) /\ (undef388 > 2) /\ (arg1 > 0), par{arg1 -> undef388, arg3 -> undef390, arg4 -> undef391, arg5 -> undef392, arg6 -> undef393, arg7 -> undef394, arg8 -> undef395, arg9 -> undef396}>
<l2, l9, ((arg2 - 1) < arg2) /\ (arg2 > 0) /\ (arg1 > 4) /\ (arg3 > 0) /\ (arg4 > 2) /\ (undef397 > 4) /\ ((arg6 + 4) <= arg1) /\ ((arg7 + 4) <= arg1) /\ ((arg8 + 2) <= arg3) /\ ((arg9 + 2) <= arg4), par{arg1 -> undef397, arg2 -> (arg2 - 1), arg3 -> undef399, arg4 -> undef400, arg5 -> undef401, arg6 -> undef402, arg7 -> undef403, arg8 -> undef404, arg9 -> undef405}>
<l20, l3, true, par{arg1 -> undef406, arg2 -> undef407, arg3 -> undef408, arg4 -> undef409, arg5 -> undef410, arg6 -> undef411, arg7 -> undef412, arg8 -> undef413, arg9 -> undef414}>

Fresh variables:
undef1, undef3, undef4, undef6, undef8, undef10, undef11, undef12, undef13, undef14, undef15, undef16, undef17, undef18, undef19, undef20, undef21, undef22, undef23, undef24, undef25, undef26, undef27, undef28, undef29, undef30, undef31, undef32, undef33, undef34, undef35, undef36, undef37, undef38, undef39, undef40, undef42, undef43, undef44, undef45, undef46, undef47, undef48, undef49, undef50, undef51, undef52, undef53, undef54, undef55, undef56, undef57, undef58, undef59, undef60, undef61, undef62, undef64, undef65, undef66, undef67, undef68, undef69, undef70, undef71, undef73, undef74, undef75, undef76, undef77, undef78, undef79, undef80, undef81, undef82, undef83, undef87, undef88, undef89, undef90, undef91, undef92, undef93, undef94, undef95, undef98, undef99, undef100, undef101, undef102, undef103, undef104, undef105, undef106, undef107, undef108, undef109, undef110, undef111, undef112, undef113, undef114, undef116, undef117, undef118, undef119, undef120, undef121, undef122, undef123, undef124, undef125, undef128, undef129, undef130, undef131, undef132, undef133, undef134, undef135, undef136, undef137, undef138, undef139, undef140, undef141, undef142, undef143, undef144, undef145, undef146, undef147, undef148, undef149, undef150, undef151, undef152, undef153, undef155, undef156, undef157, undef158, undef159, undef160, undef161, undef162, undef163, undef164, undef166, undef167, undef168, undef169, undef170, undef171, undef172, undef173, undef174, undef175, undef176, undef177, undef178, undef179, undef180, undef181, undef182, undef183, undef184, undef185, undef190, undef191, undef192, undef193, undef194, undef199, undef200, undef201, undef202, undef203, undef205, undef208, undef209, undef210, undef211, undef212, undef217, undef218, undef219, undef220, undef221, undef226, undef227, undef228, undef229, undef231, undef233, undef236, undef237, undef238, undef240, undef242, undef245, undef246, undef247, undef248, undef249, undef254, undef255, undef256, undef257, undef258, undef263, undef264, undef265, undef266, undef267, undef268, undef269, undef270, undef271, undef272, undef273, undef274, undef275, undef276, undef277, undef278, undef279, undef280, undef281, undef282, undef283, undef284, undef285, undef286, undef287, undef288, undef289, undef290, undef291, undef292, undef293, undef294, undef295, undef296, undef297, undef298, undef300, undef301, undef302, undef303, undef304, undef305, undef306, undef307, undef309, undef310, undef311, undef312, undef313, undef314, undef315, undef316, undef318, undef319, undef321, undef322, undef323, undef324, undef326, undef327, undef329, undef330, undef331, undef332, undef333, undef334, undef336, undef337, undef338, undef339, undef340, undef341, undef342, undef346, undef347, undef348, undef349, undef350, undef351, undef355, undef356, undef357, undef358, undef359, undef360, undef364, undef365, undef366, undef367, undef368, undef369, undef370, undef372, undef373, undef374, undef375, undef376, undef377, undef378, undef379, undef381, undef382, undef383, undef384, undef385, undef386, undef387, undef388, undef390, undef391, undef392, undef393, undef394, undef395, undef396, undef397, undef399, undef400, undef401, undef402, undef403, undef404, undef405, undef406, undef407, undef408, undef409, undef410, undef411, undef412, undef413, undef414, 

Undef variables:
undef1, undef3, undef4, undef6, undef8, undef10, undef11, undef12, undef13, undef14, undef15, undef16, undef17, undef18, undef19, undef20, undef21, undef22, undef23, undef24, undef25, undef26, undef27, undef28, undef29, undef30, undef31, undef32, undef33, undef34, undef35, undef36, undef37, undef38, undef39, undef40, undef42, undef43, undef44, undef45, undef46, undef47, undef48, undef49, undef50, undef51, undef52, undef53, undef54, undef55, undef56, undef57, undef58, undef59, undef60, undef61, undef62, undef64, undef65, undef66, undef67, undef68, undef69, undef70, undef71, undef73, undef74, undef75, undef76, undef77, undef78, undef79, undef80, undef81, undef82, undef83, undef87, undef88, undef89, undef90, undef91, undef92, undef93, undef94, undef95, undef98, undef99, undef100, undef101, undef102, undef103, undef104, undef105, undef106, undef107, undef108, undef109, undef110, undef111, undef112, undef113, undef114, undef116, undef117, undef118, undef119, undef120, undef121, undef122, undef123, undef124, undef125, undef128, undef129, undef130, undef131, undef132, undef133, undef134, undef135, undef136, undef137, undef138, undef139, undef140, undef141, undef142, undef143, undef144, undef145, undef146, undef147, undef148, undef149, undef150, undef151, undef152, undef153, undef155, undef156, undef157, undef158, undef159, undef160, undef161, undef162, undef163, undef164, undef166, undef167, undef168, undef169, undef170, undef171, undef172, undef173, undef174, undef175, undef176, undef177, undef178, undef179, undef180, undef181, undef182, undef183, undef184, undef185, undef190, undef191, undef192, undef193, undef194, undef199, undef200, undef201, undef202, undef203, undef205, undef208, undef209, undef210, undef211, undef212, undef217, undef218, undef219, undef220, undef221, undef226, undef227, undef228, undef229, undef231, undef233, undef236, undef237, undef238, undef240, undef242, undef245, undef246, undef247, undef248, undef249, undef254, undef255, undef256, undef257, undef258, undef263, undef264, undef265, undef266, undef267, undef268, undef269, undef270, undef271, undef272, undef273, undef274, undef275, undef276, undef277, undef278, undef279, undef280, undef281, undef282, undef283, undef284, undef285, undef286, undef287, undef288, undef289, undef290, undef291, undef292, undef293, undef294, undef295, undef296, undef297, undef298, undef300, undef301, undef302, undef303, undef304, undef305, undef306, undef307, undef309, undef310, undef311, undef312, undef313, undef314, undef315, undef316, undef318, undef319, undef321, undef322, undef323, undef324, undef326, undef327, undef329, undef330, undef331, undef332, undef333, undef334, undef336, undef337, undef338, undef339, undef340, undef341, undef342, undef346, undef347, undef348, undef349, undef350, undef351, undef355, undef356, undef357, undef358, undef359, undef360, undef364, undef365, undef366, undef367, undef368, undef369, undef370, undef372, undef373, undef374, undef375, undef376, undef377, undef378, undef379, undef381, undef382, undef383, undef384, undef385, undef386, undef387, undef388, undef390, undef391, undef392, undef393, undef394, undef395, undef396, undef397, undef399, undef400, undef401, undef402, undef403, undef404, undef405, undef406, undef407, undef408, undef409, undef410, undef411, undef412, undef413, undef414, 

Abstraction variables:

Exit nodes:

Accepting locations:

Asserts:

Preprocessed LLVMGraph
Init Location: 0
Transitions:
<l0, l9, (undef10 <= undef406) /\ (undef407 > ~(1)) /\ (undef406 > 0) /\ (undef10 > 0) /\ (undef11 > ~(1)) /\ (undef29 <= undef10) /\ (undef31 >= undef38) /\ ((undef29 - 1) <= undef11) /\ (undef30 <= undef11) /\ (undef10 > 0) /\ (undef11 > ~(1)) /\ (undef29 > 0) /\ (undef30 > ~(1)) /\ (undef31 >= undef59) /\ (undef59 > ~(1)) /\ (undef50 <= undef29) /\ (undef50 <= undef30) /\ (undef29 > 0) /\ (undef30 > 0) /\ (undef50 > 0) /\ (undef51 > 1) /\ (undef71 <= undef51) /\ (undef80 >= undef81) /\ (undef50 > 0) /\ (undef51 > 1) /\ (undef71 > 1) /\ ((undef52 + 2) <= undef51), par{arg1 -> undef71, arg2 -> 0, arg3 -> undef73, arg4 -> undef74, arg5 -> undef75}>
<l0, l9, (undef10 <= undef406) /\ (undef407 > ~(1)) /\ (undef406 > 0) /\ (undef10 > 0) /\ (undef11 > ~(1)) /\ (undef29 <= undef10) /\ (undef31 >= undef38) /\ ((undef29 - 1) <= undef11) /\ (undef30 <= undef11) /\ (undef10 > 0) /\ (undef11 > ~(1)) /\ (undef29 > 0) /\ (undef30 > ~(1)) /\ (undef31 >= undef59) /\ (undef59 > ~(1)) /\ (undef50 <= undef29) /\ (undef50 <= undef30) /\ (undef29 > 0) /\ (undef30 > 0) /\ (undef50 > 0) /\ (undef51 > 1) /\ (undef91 < undef92) /\ (undef91 > ~(1)) /\ (undef82 <= undef50) /\ ((undef82 + 1) <= undef51) /\ (undef83 <= undef51) /\ (undef50 > 0) /\ (undef51 > 1) /\ (undef82 > 0) /\ (undef83 > 1) /\ ((undef52 + 2) <= undef51) /\ ((undef91 + 1) <= undef123) /\ (undef123 > 0) /\ ((undef91 + 1) > 0) /\ (undef114 <= undef83) /\ (undef82 > 0) /\ (undef83 > 1) /\ (undef114 > 1) /\ ((undef52 + 2) <= undef83), par{arg1 -> undef114, arg2 -> 0, arg3 -> undef116, arg4 -> undef117, arg5 -> undef118}>
<l0, l9, (undef10 <= undef406) /\ (undef407 > ~(1)) /\ (undef406 > 0) /\ (undef10 > 0) /\ (undef11 > ~(1)) /\ (undef29 <= undef10) /\ (undef31 >= undef38) /\ ((undef29 - 1) <= undef11) /\ (undef30 <= undef11) /\ (undef10 > 0) /\ (undef11 > ~(1)) /\ (undef29 > 0) /\ (undef30 > ~(1)) /\ (undef31 >= undef59) /\ (undef59 > ~(1)) /\ (undef50 <= undef29) /\ (undef50 <= undef30) /\ (undef29 > 0) /\ (undef30 > 0) /\ (undef50 > 0) /\ (undef51 > 1) /\ (undef102 < undef103) /\ (undef102 > ~(1)) /\ (undef95 > ~(1)) /\ (undef93 <= undef50) /\ ((undef93 + 1) <= undef51) /\ (undef94 <= undef51) /\ (undef50 > 0) /\ (undef51 > 1) /\ (undef93 > 0) /\ (undef94 > 1) /\ ((undef52 + 2) <= undef51) /\ ((undef102 + 1) <= undef123) /\ (undef123 > 0) /\ ((undef102 + 1) > 0) /\ (undef114 <= undef94) /\ (undef93 > 0) /\ (undef94 > 1) /\ (undef114 > 1) /\ ((undef52 + 2) <= undef94), par{arg1 -> undef114, arg2 -> undef95, arg3 -> undef116, arg4 -> undef117, arg5 -> undef118}>
<l0, l15, (undef10 <= undef406) /\ (undef407 > ~(1)) /\ (undef406 > 0) /\ (undef10 > 0) /\ (undef11 > ~(1)) /\ (undef29 <= undef10) /\ (undef31 >= undef38) /\ ((undef29 - 1) <= undef11) /\ (undef30 <= undef11) /\ (undef10 > 0) /\ (undef11 > ~(1)) /\ (undef29 > 0) /\ (undef30 > ~(1)) /\ (undef267 <= undef30) /\ (undef31 >= undef276) /\ (undef29 > 0) /\ (undef30 > 0) /\ (undef267 > 0) /\ (undef268 > ~(1)) /\ ((undef269 + 2) <= undef30), par{arg1 -> undef267, arg2 -> undef268, arg3 -> undef269, arg4 -> undef270, arg5 -> undef271}>
<l0, l9, (undef10 <= undef406) /\ (undef407 > ~(1)) /\ (undef406 > 0) /\ (undef10 > 0) /\ (undef11 > ~(1)) /\ (undef48 < undef49) /\ (undef48 > ~(1)) /\ (undef39 <= undef10) /\ ((undef39 - 1) <= undef11) /\ (undef40 <= undef11) /\ (undef10 > 0) /\ (undef11 > ~(1)) /\ (undef39 > 0) /\ (undef40 > ~(1)) /\ ((undef48 + 1) >= undef59) /\ (undef59 > ~(1)) /\ (undef50 <= undef39) /\ (undef50 <= undef40) /\ (undef39 > 0) /\ (undef40 > 0) /\ (undef50 > 0) /\ (undef51 > 1) /\ (undef71 <= undef51) /\ (undef80 >= undef81) /\ (undef50 > 0) /\ (undef51 > 1) /\ (undef71 > 1) /\ ((undef52 + 2) <= undef51), par{arg1 -> undef71, arg2 -> 0, arg3 -> undef73, arg4 -> undef74, arg5 -> undef75}>
<l0, l9, (undef10 <= undef406) /\ (undef407 > ~(1)) /\ (undef406 > 0) /\ (undef10 > 0) /\ (undef11 > ~(1)) /\ (undef48 < undef49) /\ (undef48 > ~(1)) /\ (undef39 <= undef10) /\ ((undef39 - 1) <= undef11) /\ (undef40 <= undef11) /\ (undef10 > 0) /\ (undef11 > ~(1)) /\ (undef39 > 0) /\ (undef40 > ~(1)) /\ ((undef48 + 1) >= undef59) /\ (undef59 > ~(1)) /\ (undef50 <= undef39) /\ (undef50 <= undef40) /\ (undef39 > 0) /\ (undef40 > 0) /\ (undef50 > 0) /\ (undef51 > 1) /\ (undef91 < undef92) /\ (undef91 > ~(1)) /\ (undef82 <= undef50) /\ ((undef82 + 1) <= undef51) /\ (undef83 <= undef51) /\ (undef50 > 0) /\ (undef51 > 1) /\ (undef82 > 0) /\ (undef83 > 1) /\ ((undef52 + 2) <= undef51) /\ ((undef91 + 1) <= undef123) /\ (undef123 > 0) /\ ((undef91 + 1) > 0) /\ (undef114 <= undef83) /\ (undef82 > 0) /\ (undef83 > 1) /\ (undef114 > 1) /\ ((undef52 + 2) <= undef83), par{arg1 -> undef114, arg2 -> 0, arg3 -> undef116, arg4 -> undef117, arg5 -> undef118}>
<l0, l9, (undef10 <= undef406) /\ (undef407 > ~(1)) /\ (undef406 > 0) /\ (undef10 > 0) /\ (undef11 > ~(1)) /\ (undef48 < undef49) /\ (undef48 > ~(1)) /\ (undef39 <= undef10) /\ ((undef39 - 1) <= undef11) /\ (undef40 <= undef11) /\ (undef10 > 0) /\ (undef11 > ~(1)) /\ (undef39 > 0) /\ (undef40 > ~(1)) /\ ((undef48 + 1) >= undef59) /\ (undef59 > ~(1)) /\ (undef50 <= undef39) /\ (undef50 <= undef40) /\ (undef39 > 0) /\ (undef40 > 0) /\ (undef50 > 0) /\ (undef51 > 1) /\ (undef102 < undef103) /\ (undef102 > ~(1)) /\ (undef95 > ~(1)) /\ (undef93 <= undef50) /\ ((undef93 + 1) <= undef51) /\ (undef94 <= undef51) /\ (undef50 > 0) /\ (undef51 > 1) /\ (undef93 > 0) /\ (undef94 > 1) /\ ((undef52 + 2) <= undef51) /\ ((undef102 + 1) <= undef123) /\ (undef123 > 0) /\ ((undef102 + 1) > 0) /\ (undef114 <= undef94) /\ (undef93 > 0) /\ (undef94 > 1) /\ (undef114 > 1) /\ ((undef52 + 2) <= undef94), par{arg1 -> undef114, arg2 -> undef95, arg3 -> undef116, arg4 -> undef117, arg5 -> undef118}>
<l0, l15, (undef10 <= undef406) /\ (undef407 > ~(1)) /\ (undef406 > 0) /\ (undef10 > 0) /\ (undef11 > ~(1)) /\ (undef48 < undef49) /\ (undef48 > ~(1)) /\ (undef39 <= undef10) /\ ((undef39 - 1) <= undef11) /\ (undef40 <= undef11) /\ (undef10 > 0) /\ (undef11 > ~(1)) /\ (undef39 > 0) /\ (undef40 > ~(1)) /\ (undef267 <= undef40) /\ ((undef48 + 1) >= undef276) /\ (undef39 > 0) /\ (undef40 > 0) /\ (undef267 > 0) /\ (undef268 > ~(1)) /\ ((undef269 + 2) <= undef40), par{arg1 -> undef267, arg2 -> undef268, arg3 -> undef269, arg4 -> undef270, arg5 -> undef271}>
<l0, l8, (undef10 <= undef406) /\ (undef407 > ~(1)) /\ (undef406 > 0) /\ (undef10 > 0) /\ (undef11 > ~(1)) /\ (undef69 < undef70) /\ (undef69 > ~(1)) /\ (undef70 > 0) /\ (undef62 > ~(1)) /\ ((undef69 + 1) <= undef70) /\ (undef60 <= undef10) /\ (undef60 <= undef11) /\ (undef10 > 0) /\ (undef11 > 0) /\ (undef60 > 0) /\ (undef61 > 1), par{arg1 -> undef60, arg2 -> undef61, arg3 -> undef62, arg4 -> (undef69 + 1), arg5 -> undef64}>
<l0, l15, (undef10 <= undef406) /\ (undef407 > ~(1)) /\ (undef406 > 0) /\ (undef10 > 0) /\ (undef11 > ~(1)) /\ (undef286 < undef287) /\ (undef286 > ~(1)) /\ (undef287 > 0) /\ (undef288 > ~(1)) /\ ((undef286 + 1) <= undef287) /\ (undef277 <= undef11) /\ (undef10 > 0) /\ (undef11 > 0) /\ (undef277 > 0) /\ (undef278 > ~(1)) /\ ((undef279 + 2) <= undef11), par{arg1 -> undef277, arg2 -> undef278, arg3 -> undef279, arg4 -> undef280, arg5 -> undef281}>
<l0, l13, ((undef185 + 1) <= undef406) /\ (undef406 > 0) /\ (undef185 > ~(1)) /\ (0 = undef407), par{arg1 -> undef185, arg2 -> 0, arg3 -> 0, arg4 -> 0, arg5 -> 0}>
<l0, l13, ((undef194 + 1) <= undef406) /\ (undef407 > 0) /\ (undef406 > 0) /\ (undef194 > ~(1)), par{arg1 -> undef194, arg2 -> 0, arg3 -> 0, arg4 -> undef407, arg5 -> 1}>
<l0, l13, (undef205 > ~(1)) /\ (undef407 > 0) /\ ((undef203 + 1) <= undef406) /\ (undef406 > 0) /\ (undef203 > ~(1)), par{arg1 -> undef203, arg2 -> 0, arg3 -> undef205, arg4 -> undef407, arg5 -> 1}>
<l8, l9, (undef104 <= arg1) /\ (undef113 > ~(1)) /\ ((undef104 - 1) <= arg2) /\ (undef105 <= arg2) /\ (arg1 > 0) /\ (arg2 > ~(1)) /\ (undef104 > 0) /\ (undef105 > ~(1)) /\ (0 = arg3) /\ (undef133 <= undef104) /\ (undef135 >= undef142) /\ ((undef133 - 1) <= undef105) /\ (undef134 <= undef105) /\ (undef104 > 0) /\ (undef105 > ~(1)) /\ (undef133 > 0) /\ (undef134 > ~(1)) /\ (undef135 >= undef162) /\ (undef162 > 0) /\ (undef135 > 0) /\ (undef153 <= undef134) /\ (undef133 > 0) /\ (undef134 > 0) /\ (undef153 > 0), par{arg1 -> undef153, arg2 -> 0, arg3 -> undef155, arg4 -> undef156, arg5 -> undef157}>
<l8, l9, (undef104 <= arg1) /\ (undef113 > ~(1)) /\ ((undef104 - 1) <= arg2) /\ (undef105 <= arg2) /\ (arg1 > 0) /\ (arg2 > ~(1)) /\ (undef104 > 0) /\ (undef105 > ~(1)) /\ (0 = arg3) /\ (undef172 < undef173) /\ (undef172 > 0) /\ (undef163 <= undef104) /\ ((undef163 - 1) <= undef105) /\ (undef164 <= undef105) /\ (undef104 > 0) /\ (undef105 > ~(1)) /\ (undef163 > 0) /\ (undef164 > ~(1)) /\ ((undef172 + 1) >= undef162) /\ (undef162 > 0) /\ ((undef172 + 1) > 0) /\ (undef153 <= undef164) /\ (undef163 > 0) /\ (undef164 > 0) /\ (undef153 > 0), par{arg1 -> undef153, arg2 -> 0, arg3 -> undef155, arg4 -> undef156, arg5 -> undef157}>
<l8, l9, (undef104 <= arg1) /\ (undef113 > ~(1)) /\ ((undef104 - 1) <= arg2) /\ (undef105 <= arg2) /\ (arg1 > 0) /\ (arg2 > ~(1)) /\ (undef104 > 0) /\ (undef105 > ~(1)) /\ (0 = arg3) /\ (undef183 < undef184) /\ (undef183 > 0) /\ (undef184 > 1) /\ (undef175 > ~(1)) /\ ((undef183 + 1) <= undef184) /\ (undef174 <= undef105) /\ (undef104 > 0) /\ (undef105 > 0) /\ (undef174 > 0), par{arg1 -> undef174, arg2 -> undef175, arg3 -> undef176, arg4 -> undef177, arg5 -> undef178}>
<l8, l8, (undef124 <= arg1) /\ (arg3 > 0) /\ (undef124 <= arg2) /\ (arg1 > 0) /\ (arg2 > 0) /\ (undef124 > 0) /\ (undef125 > ~(1)), par{arg1 -> undef124, arg2 -> undef125, arg5 -> undef128}>
<l8, l9, (undef152 > ~(1)) /\ (arg3 > 0) /\ (arg1 >= undef143) /\ (arg2 >= (undef143 - 1)) /\ (arg1 >= (undef144 + 1)) /\ (arg2 >= undef144) /\ (arg1 > 0) /\ (arg2 > ~(1)) /\ (undef143 > 0) /\ (undef144 > ~(1)) /\ (undef133 <= undef143) /\ (undef135 >= undef142) /\ ((undef133 - 1) <= undef144) /\ (undef134 <= undef144) /\ (undef143 > 0) /\ (undef144 > ~(1)) /\ (undef133 > 0) /\ (undef134 > ~(1)) /\ (undef135 >= undef162) /\ (undef162 > 0) /\ (undef135 > 0) /\ (undef153 <= undef134) /\ (undef133 > 0) /\ (undef134 > 0) /\ (undef153 > 0), par{arg1 -> undef153, arg2 -> 0, arg3 -> undef155, arg4 -> undef156, arg5 -> undef157}>
<l8, l9, (undef152 > ~(1)) /\ (arg3 > 0) /\ (arg1 >= undef143) /\ (arg2 >= (undef143 - 1)) /\ (arg1 >= (undef144 + 1)) /\ (arg2 >= undef144) /\ (arg1 > 0) /\ (arg2 > ~(1)) /\ (undef143 > 0) /\ (undef144 > ~(1)) /\ (undef172 < undef173) /\ (undef172 > 0) /\ (undef163 <= undef143) /\ ((undef163 - 1) <= undef144) /\ (undef164 <= undef144) /\ (undef143 > 0) /\ (undef144 > ~(1)) /\ (undef163 > 0) /\ (undef164 > ~(1)) /\ ((undef172 + 1) >= undef162) /\ (undef162 > 0) /\ ((undef172 + 1) > 0) /\ (undef153 <= undef164) /\ (undef163 > 0) /\ (undef164 > 0) /\ (undef153 > 0), par{arg1 -> undef153, arg2 -> 0, arg3 -> undef155, arg4 -> undef156, arg5 -> undef157}>
<l8, l9, (undef152 > ~(1)) /\ (arg3 > 0) /\ (arg1 >= undef143) /\ (arg2 >= (undef143 - 1)) /\ (arg1 >= (undef144 + 1)) /\ (arg2 >= undef144) /\ (arg1 > 0) /\ (arg2 > ~(1)) /\ (undef143 > 0) /\ (undef144 > ~(1)) /\ (undef183 < undef184) /\ (undef183 > 0) /\ (undef184 > 1) /\ (undef175 > ~(1)) /\ ((undef183 + 1) <= undef184) /\ (undef174 <= undef144) /\ (undef143 > 0) /\ (undef144 > 0) /\ (undef174 > 0), par{arg1 -> undef174, arg2 -> undef175, arg3 -> undef176, arg4 -> undef177, arg5 -> undef178}>
<l9, l9, (undef298 <= arg1) /\ (arg2 > 0) /\ (arg1 > 2) /\ (undef298 > 2) /\ (undef300 > 0) /\ ((undef302 + 3) <= arg1) /\ (undef298 > 2) /\ (undef300 > 0) /\ (undef316 > 4) /\ (undef318 > 0) /\ (undef319 > 2) /\ ((undef302 + 3) <= undef298) /\ (undef1 <= undef316) /\ (undef3 <= undef318) /\ (undef4 <= undef319) /\ (undef316 > 4) /\ (undef318 > 0) /\ (undef319 > 2) /\ (undef1 > 4) /\ (undef3 > 0) /\ (undef4 > 2) /\ ((undef6 + 4) <= undef316) /\ ((undef321 + 4) <= undef316) /\ (undef318 >= (undef8 + 2)) /\ ((undef322 + 2) <= undef319) /\ (arg2 > 0) /\ ((arg2 - 1) < arg2) /\ (undef379 <= undef1) /\ ((undef379 - 2) <= undef3) /\ ((undef379 - 2) <= undef4) /\ (undef1 > 4) /\ (undef3 > 2) /\ (undef4 > 2) /\ (undef379 > 4) /\ ((undef6 + 4) <= undef1) /\ ((undef8 + 2) <= undef3) /\ ((undef8 + 2) <= undef4) /\ (undef6 = undef321) /\ (undef8 = undef322), par{arg1 -> undef379, arg2 -> (arg2 - 1), arg3 -> undef381, arg4 -> undef382, arg5 -> undef383}>
<l9, l9, (undef298 <= arg1) /\ (arg2 > 0) /\ (arg1 > 2) /\ (undef298 > 2) /\ (undef300 > 0) /\ ((undef302 + 3) <= arg1) /\ (undef298 > 2) /\ (undef300 > 0) /\ (undef316 > 4) /\ (undef318 > 0) /\ (undef319 > 2) /\ ((undef302 + 3) <= undef298) /\ (undef1 <= undef316) /\ (undef3 <= undef318) /\ (undef4 <= undef319) /\ (undef316 > 4) /\ (undef318 > 0) /\ (undef319 > 2) /\ (undef1 > 4) /\ (undef3 > 0) /\ (undef4 > 2) /\ ((undef6 + 4) <= undef316) /\ ((undef321 + 4) <= undef316) /\ (undef318 >= (undef8 + 2)) /\ ((undef322 + 2) <= undef319) /\ ((arg2 - 1) < arg2) /\ (arg2 > 0) /\ (undef1 > 4) /\ (undef3 > 0) /\ (undef4 > 2) /\ (undef397 > 4) /\ ((undef6 + 4) <= undef1) /\ ((undef321 + 4) <= undef1) /\ ((undef8 + 2) <= undef3) /\ ((undef322 + 2) <= undef4), par{arg1 -> undef397, arg2 -> (arg2 - 1), arg3 -> undef399, arg4 -> undef400, arg5 -> undef401}>
<l9, l9, (undef298 <= arg1) /\ (arg2 > 0) /\ (arg1 > 2) /\ (undef298 > 2) /\ (undef300 > 0) /\ ((undef302 + 3) <= arg1) /\ (undef298 > 2) /\ (undef300 > 0) /\ (undef316 > 4) /\ (undef318 > 0) /\ (undef319 > 2) /\ ((undef302 + 3) <= undef298) /\ (undef316 > 4) /\ (arg2 > 0) /\ (undef318 > 4) /\ (undef319 > 4) /\ ((undef321 + 4) <= undef316) /\ ((undef321 + 4) <= undef318) /\ ((undef322 + 2) <= undef319) /\ ((arg2 - 1) < arg2) /\ (undef388 > 2) /\ (arg2 > 0), par{arg1 -> undef388, arg2 -> (arg2 - 1), arg3 -> undef390, arg4 -> undef391, arg5 -> undef392}>
<l9, l9, (undef298 <= arg1) /\ (arg2 > 0) /\ (arg1 > 2) /\ (undef298 > 2) /\ (undef300 > 0) /\ ((undef302 + 3) <= arg1) /\ (undef298 > 2) /\ (undef300 > 2) /\ (undef326 > 0) /\ (undef327 > 2) /\ ((undef302 + 3) <= undef298) /\ ((undef302 + 3) <= undef300) /\ (undef326 > 2) /\ (arg2 > 0) /\ (undef327 > 2) /\ ((arg2 - 1) < arg2) /\ (undef388 > 2) /\ (arg2 > 0), par{arg1 -> undef388, arg2 -> (arg2 - 1), arg3 -> undef390, arg4 -> undef391, arg5 -> undef392}>
<l9, l9, (undef298 <= arg1) /\ (arg2 > 0) /\ (arg1 > 2) /\ (undef298 > 2) /\ (undef300 > 0) /\ ((undef302 + 3) <= arg1) /\ (undef298 > 2) /\ (undef300 > 2) /\ (undef326 > 0) /\ (undef327 > 2) /\ ((undef302 + 3) <= undef298) /\ ((undef302 + 3) <= undef300) /\ (arg2 > 0) /\ ((arg2 - 1) < arg2) /\ (undef326 > 0) /\ (undef327 > 2) /\ (undef370 > 4), par{arg1 -> undef370, arg2 -> (arg2 - 1), arg3 -> undef372, arg4 -> undef373, arg5 -> undef374}>
<l9, l9, (undef307 <= arg1) /\ (arg2 > 0) /\ (arg1 > 2) /\ (undef307 > 2) /\ (undef309 > 0) /\ (arg2 > 0) /\ ((arg2 - 1) < arg2) /\ (undef307 > 2) /\ (undef309 > 0) /\ (undef334 > 4), par{arg1 -> undef334, arg2 -> (arg2 - 1), arg3 -> undef336, arg4 -> undef337, arg5 -> undef338}>
<l9, l9, (undef307 <= arg1) /\ (arg2 > 0) /\ (arg1 > 2) /\ (undef307 > 2) /\ (undef309 > 0) /\ (undef307 > 2) /\ (arg2 > 0) /\ (undef309 > 2) /\ ((arg2 - 1) < arg2) /\ (undef388 > 2) /\ (arg2 > 0), par{arg1 -> undef388, arg2 -> (arg2 - 1), arg3 -> undef390, arg4 -> undef391, arg5 -> undef392}>
<l13, l13, (arg5 >= arg4) /\ (arg4 > ~(1)) /\ (arg3 > arg2) /\ ((undef212 - 2) <= arg1) /\ (arg1 > ~(1)) /\ (undef212 > 1), par{arg1 -> undef212, arg2 -> (arg2 + 1)}>
<l13, l13, (arg5 >= arg4) /\ (arg4 > ~(1)) /\ (arg3 > arg2) /\ (arg1 > 0) /\ (undef221 > 4), par{arg1 -> undef221, arg2 -> (arg2 + 1)}>
<l13, l13, (arg3 > arg2) /\ (arg4 > ~(1)) /\ (arg5 < arg4) /\ (arg5 > ~(1)) /\ (undef233 <= arg1) /\ (arg1 > ~(1)) /\ (undef231 > 1) /\ (undef233 > ~(1)) /\ (undef249 <= undef231) /\ ((undef249 - 2) <= undef233) /\ (undef231 > 1) /\ (undef233 > ~(1)) /\ (undef249 > 1), par{arg1 -> undef249, arg2 -> (arg2 + 1), arg3 -> arg3, arg4 -> arg4, arg5 -> (arg5 + 1)}>
<l13, l13, (arg3 > arg2) /\ (arg4 > ~(1)) /\ (arg5 < arg4) /\ (arg5 > ~(1)) /\ (undef233 <= arg1) /\ (arg1 > ~(1)) /\ (undef231 > 1) /\ (undef233 > ~(1)) /\ (undef231 > 2) /\ (undef233 > 0) /\ (undef258 > 4), par{arg1 -> undef258, arg2 -> (arg2 + 1), arg3 -> arg3, arg4 -> arg4, arg5 -> (arg5 + 1)}>
<l13, l13, (arg3 > arg2) /\ (arg4 > ~(1)) /\ (arg5 < arg4) /\ (arg5 > ~(1)) /\ (undef248 > ~(1)) /\ (undef242 <= arg1) /\ (arg1 > ~(1)) /\ (undef240 > 1) /\ (undef242 > ~(1)) /\ (undef249 <= undef240) /\ ((undef249 - 2) <= undef242) /\ (undef240 > 1) /\ (undef242 > ~(1)) /\ (undef249 > 1), par{arg1 -> undef249, arg2 -> (arg2 + 1), arg3 -> arg3, arg4 -> arg4, arg5 -> (arg5 + 1)}>
<l13, l13, (arg3 > arg2) /\ (arg4 > ~(1)) /\ (arg5 < arg4) /\ (arg5 > ~(1)) /\ (undef248 > ~(1)) /\ (undef242 <= arg1) /\ (arg1 > ~(1)) /\ (undef240 > 1) /\ (undef242 > ~(1)) /\ (undef240 > 2) /\ (undef242 > 0) /\ (undef258 > 4), par{arg1 -> undef258, arg2 -> (arg2 + 1), arg3 -> arg3, arg4 -> arg4, arg5 -> (arg5 + 1)}>
<l15, l15, (arg1 > 2) /\ (arg2 > 0) /\ (undef289 > 0) /\ (undef290 > ~(1)) /\ ((arg3 + 2) <= arg1), par{arg1 -> undef289, arg2 -> undef290, arg3 -> undef291, arg4 -> undef292, arg5 -> undef293}>

Fresh variables:
undef1, undef3, undef4, undef6, undef8, undef10, undef11, undef12, undef13, undef14, undef15, undef16, undef17, undef18, undef19, undef20, undef21, undef22, undef23, undef24, undef25, undef26, undef27, undef28, undef29, undef30, undef31, undef32, undef33, undef34, undef35, undef36, undef37, undef38, undef39, undef40, undef42, undef43, undef44, undef45, undef46, undef47, undef48, undef49, undef50, undef51, undef52, undef53, undef54, undef55, undef56, undef57, undef58, undef59, undef60, undef61, undef62, undef64, undef65, undef66, undef67, undef68, undef69, undef70, undef71, undef73, undef74, undef75, undef76, undef77, undef78, undef79, undef80, undef81, undef82, undef83, undef87, undef88, undef89, undef90, undef91, undef92, undef93, undef94, undef95, undef98, undef99, undef100, undef101, undef102, undef103, undef104, undef105, undef106, undef107, undef108, undef109, undef110, undef111, undef112, undef113, undef114, undef116, undef117, undef118, undef119, undef120, undef121, undef122, undef123, undef124, undef125, undef128, undef129, undef130, undef131, undef132, undef133, undef134, undef135, undef136, undef137, undef138, undef139, undef140, undef141, undef142, undef143, undef144, undef145, undef146, undef147, undef148, undef149, undef150, undef151, undef152, undef153, undef155, undef156, undef157, undef158, undef159, undef160, undef161, undef162, undef163, undef164, undef166, undef167, undef168, undef169, undef170, undef171, undef172, undef173, undef174, undef175, undef176, undef177, undef178, undef179, undef180, undef181, undef182, undef183, undef184, undef185, undef190, undef191, undef192, undef193, undef194, undef199, undef200, undef201, undef202, undef203, undef205, undef208, undef209, undef210, undef211, undef212, undef217, undef218, undef219, undef220, undef221, undef226, undef227, undef228, undef229, undef231, undef233, undef236, undef237, undef238, undef240, undef242, undef245, undef246, undef247, undef248, undef249, undef254, undef255, undef256, undef257, undef258, undef263, undef264, undef265, undef266, undef267, undef268, undef269, undef270, undef271, undef272, undef273, undef274, undef275, undef276, undef277, undef278, undef279, undef280, undef281, undef282, undef283, undef284, undef285, undef286, undef287, undef288, undef289, undef290, undef291, undef292, undef293, undef294, undef295, undef296, undef297, undef298, undef300, undef301, undef302, undef303, undef304, undef305, undef306, undef307, undef309, undef310, undef311, undef312, undef313, undef314, undef315, undef316, undef318, undef319, undef321, undef322, undef323, undef324, undef326, undef327, undef329, undef330, undef331, undef332, undef333, undef334, undef336, undef337, undef338, undef339, undef340, undef341, undef342, undef346, undef347, undef348, undef349, undef350, undef351, undef355, undef356, undef357, undef358, undef359, undef360, undef364, undef365, undef366, undef367, undef368, undef369, undef370, undef372, undef373, undef374, undef375, undef376, undef377, undef378, undef379, undef381, undef382, undef383, undef384, undef385, undef386, undef387, undef388, undef390, undef391, undef392, undef393, undef394, undef395, undef396, undef397, undef399, undef400, undef401, undef402, undef403, undef404, undef405, undef406, undef407, undef408, undef409, undef410, undef411, undef412, undef413, undef414, 

Undef variables:
undef1, undef3, undef4, undef6, undef8, undef10, undef11, undef12, undef13, undef14, undef15, undef16, undef17, undef18, undef19, undef20, undef21, undef22, undef23, undef24, undef25, undef26, undef27, undef28, undef29, undef30, undef31, undef32, undef33, undef34, undef35, undef36, undef37, undef38, undef39, undef40, undef42, undef43, undef44, undef45, undef46, undef47, undef48, undef49, undef50, undef51, undef52, undef53, undef54, undef55, undef56, undef57, undef58, undef59, undef60, undef61, undef62, undef64, undef65, undef66, undef67, undef68, undef69, undef70, undef71, undef73, undef74, undef75, undef76, undef77, undef78, undef79, undef80, undef81, undef82, undef83, undef87, undef88, undef89, undef90, undef91, undef92, undef93, undef94, undef95, undef98, undef99, undef100, undef101, undef102, undef103, undef104, undef105, undef106, undef107, undef108, undef109, undef110, undef111, undef112, undef113, undef114, undef116, undef117, undef118, undef119, undef120, undef121, undef122, undef123, undef124, undef125, undef128, undef129, undef130, undef131, undef132, undef133, undef134, undef135, undef136, undef137, undef138, undef139, undef140, undef141, undef142, undef143, undef144, undef145, undef146, undef147, undef148, undef149, undef150, undef151, undef152, undef153, undef155, undef156, undef157, undef158, undef159, undef160, undef161, undef162, undef163, undef164, undef166, undef167, undef168, undef169, undef170, undef171, undef172, undef173, undef174, undef175, undef176, undef177, undef178, undef179, undef180, undef181, undef182, undef183, undef184, undef185, undef190, undef191, undef192, undef193, undef194, undef199, undef200, undef201, undef202, undef203, undef205, undef208, undef209, undef210, undef211, undef212, undef217, undef218, undef219, undef220, undef221, undef226, undef227, undef228, undef229, undef231, undef233, undef236, undef237, undef238, undef240, undef242, undef245, undef246, undef247, undef248, undef249, undef254, undef255, undef256, undef257, undef258, undef263, undef264, undef265, undef266, undef267, undef268, undef269, undef270, undef271, undef272, undef273, undef274, undef275, undef276, undef277, undef278, undef279, undef280, undef281, undef282, undef283, undef284, undef285, undef286, undef287, undef288, undef289, undef290, undef291, undef292, undef293, undef294, undef295, undef296, undef297, undef298, undef300, undef301, undef302, undef303, undef304, undef305, undef306, undef307, undef309, undef310, undef311, undef312, undef313, undef314, undef315, undef316, undef318, undef319, undef321, undef322, undef323, undef324, undef326, undef327, undef329, undef330, undef331, undef332, undef333, undef334, undef336, undef337, undef338, undef339, undef340, undef341, undef342, undef346, undef347, undef348, undef349, undef350, undef351, undef355, undef356, undef357, undef358, undef359, undef360, undef364, undef365, undef366, undef367, undef368, undef369, undef370, undef372, undef373, undef374, undef375, undef376, undef377, undef378, undef379, undef381, undef382, undef383, undef384, undef385, undef386, undef387, undef388, undef390, undef391, undef392, undef393, undef394, undef395, undef396, undef397, undef399, undef400, undef401, undef402, undef403, undef404, undef405, undef406, undef407, undef408, undef409, undef410, undef411, undef412, undef413, undef414, 

Abstraction variables:

Exit nodes:

Accepting locations:

Asserts:

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

Init Location: 0
Graph 0:
Transitions:
Variables:

Graph 1:
Transitions:
<l13, l13, 0 <= arg1 /\ arg4 <= arg5 /\ 0 <= arg4 /\ 2 <= undef212 /\ 1 + arg2 <= arg3 /\ undef212 <= 2 + arg1, {arg1 -> undef212, arg2 -> 1 + arg2, rest remain the same}>
<l13, l13, arg4 <= arg5 /\ 0 <= arg4 /\ 1 <= arg1 /\ 1 + arg2 <= arg3 /\ 5 <= undef221, {arg1 -> undef221, arg2 -> 1 + arg2, rest remain the same}>
<l13, l13, 0 <= arg1 /\ undef233 <= arg1 /\ 0 <= arg4 /\ 0 <= arg5 /\ undef249 <= undef231 /\ 0 <= undef233 /\ 2 <= undef231 /\ 2 <= undef249 /\ 1 + arg2 <= arg3 /\ 1 + arg5 <= arg4 /\ undef249 <= 2 + undef233, {arg1 -> undef249, arg2 -> 1 + arg2, arg5 -> 1 + arg5, rest remain the same}>
<l13, l13, 0 <= arg1 /\ undef233 <= arg1 /\ 0 <= arg4 /\ 0 <= arg5 /\ 1 + arg2 <= arg3 /\ 1 + arg5 <= arg4 /\ 1 <= undef233 /\ 3 <= undef231 /\ 5 <= undef258, {arg1 -> undef258, arg2 -> 1 + arg2, arg5 -> 1 + arg5, rest remain the same}>
<l13, l13, 0 <= arg1 /\ undef242 <= arg1 /\ 0 <= arg4 /\ 0 <= arg5 /\ undef249 <= undef240 /\ 0 <= undef242 /\ 0 <= undef248 /\ 2 <= undef240 /\ 2 <= undef249 /\ 1 + arg2 <= arg3 /\ 1 + arg5 <= arg4 /\ undef249 <= 2 + undef242, {arg1 -> undef249, arg2 -> 1 + arg2, arg5 -> 1 + arg5, rest remain the same}>
<l13, l13, 0 <= arg1 /\ undef242 <= arg1 /\ 0 <= arg4 /\ 0 <= arg5 /\ 0 <= undef248 /\ 1 + arg2 <= arg3 /\ 1 + arg5 <= arg4 /\ 1 <= undef242 /\ 3 <= undef240 /\ 5 <= undef258, {arg1 -> undef258, arg2 -> 1 + arg2, arg5 -> 1 + arg5, rest remain the same}>
Variables:
arg1, arg2, arg3, arg4, arg5

Graph 2:
Transitions:
<l8, l8, undef124 <= arg1 /\ undef124 <= arg2 /\ 0 <= undef125 /\ 1 <= arg1 /\ 1 <= arg2 /\ 1 <= arg3 /\ 1 <= undef124, {arg1 -> undef124, arg2 -> undef125, arg5 -> undef128, rest remain the same}>
Variables:
arg1, arg2, arg3, arg5

Graph 3:
Transitions:
<l15, l15, 0 <= undef290 /\ 2 + arg3 <= arg1 /\ 1 <= arg2 /\ 1 <= undef289 /\ 3 <= arg1, {arg1 -> undef289, arg2 -> undef290, arg3 -> undef291, arg4 -> undef292, arg5 -> undef293, rest remain the same}>
Variables:
arg1, arg2, arg3, arg4, arg5

Graph 4:
Transitions:
<l9, l9, 4 + undef6 <= undef1 /\ 4 + undef6 <= undef316 /\ 4 + undef321 <= undef316 /\ undef298 <= arg1 /\ undef1 <= undef316 /\ undef379 <= undef1 /\ undef3 <= undef318 /\ undef4 <= undef319 /\ 2 + undef8 <= undef3 /\ 2 + undef8 <= undef4 /\ 2 + undef8 <= undef318 /\ 2 + undef322 <= undef319 /\ 1 <= arg2 /\ 1 <= undef300 /\ 1 <= undef318 /\ 3 <= arg1 /\ 3 + undef302 <= arg1 /\ 3 <= undef3 /\ 3 <= undef4 /\ 3 <= undef298 /\ 3 + undef302 <= undef298 /\ 3 <= undef319 /\ undef379 <= 2 + undef3 /\ undef379 <= 2 + undef4 /\ 5 <= undef1 /\ 5 <= undef316 /\ 5 <= undef379 /\ undef6 = undef321 /\ undef8 = undef322, {arg1 -> undef379, arg2 -> -1 + arg2, arg3 -> undef381, arg4 -> undef382, arg5 -> undef383, rest remain the same}>
<l9, l9, 4 + undef6 <= undef1 /\ 4 + undef321 <= undef1 /\ 4 + undef6 <= undef316 /\ 4 + undef321 <= undef316 /\ undef298 <= arg1 /\ undef1 <= undef316 /\ undef3 <= undef318 /\ undef4 <= undef319 /\ 2 + undef8 <= undef3 /\ 2 + undef322 <= undef4 /\ 2 + undef8 <= undef318 /\ 2 + undef322 <= undef319 /\ 1 <= arg2 /\ 1 <= undef3 /\ 1 <= undef300 /\ 1 <= undef318 /\ 3 <= arg1 /\ 3 + undef302 <= arg1 /\ 3 <= undef4 /\ 3 <= undef298 /\ 3 + undef302 <= undef298 /\ 3 <= undef319 /\ 5 <= undef1 /\ 5 <= undef316 /\ 5 <= undef397, {arg1 -> undef397, arg2 -> -1 + arg2, arg3 -> undef399, arg4 -> undef400, arg5 -> undef401, rest remain the same}>
<l9, l9, 4 + undef321 <= undef316 /\ 4 + undef321 <= undef318 /\ undef298 <= arg1 /\ 2 + undef322 <= undef319 /\ 1 <= arg2 /\ 1 <= undef300 /\ 3 <= arg1 /\ 3 + undef302 <= arg1 /\ 3 <= undef298 /\ 3 + undef302 <= undef298 /\ 3 <= undef388 /\ 5 <= undef316 /\ 5 <= undef318 /\ 5 <= undef319, {arg1 -> undef388, arg2 -> -1 + arg2, arg3 -> undef390, arg4 -> undef391, arg5 -> undef392, rest remain the same}>
<l9, l9, undef298 <= arg1 /\ 1 <= arg2 /\ 3 <= arg1 /\ 3 + undef302 <= arg1 /\ 3 <= undef298 /\ 3 + undef302 <= undef298 /\ 3 <= undef300 /\ 3 + undef302 <= undef300 /\ 3 <= undef326 /\ 3 <= undef327 /\ 3 <= undef388, {arg1 -> undef388, arg2 -> -1 + arg2, arg3 -> undef390, arg4 -> undef391, arg5 -> undef392, rest remain the same}>
<l9, l9, undef298 <= arg1 /\ 1 <= arg2 /\ 1 <= undef326 /\ 3 <= arg1 /\ 3 + undef302 <= arg1 /\ 3 <= undef298 /\ 3 + undef302 <= undef298 /\ 3 <= undef300 /\ 3 + undef302 <= undef300 /\ 3 <= undef327 /\ 5 <= undef370, {arg1 -> undef370, arg2 -> -1 + arg2, arg3 -> undef372, arg4 -> undef373, arg5 -> undef374, rest remain the same}>
<l9, l9, undef307 <= arg1 /\ 1 <= arg2 /\ 1 <= undef309 /\ 3 <= arg1 /\ 3 <= undef307 /\ 5 <= undef334, {arg1 -> undef334, arg2 -> -1 + arg2, arg3 -> undef336, arg4 -> undef337, arg5 -> undef338, rest remain the same}>
<l9, l9, undef307 <= arg1 /\ 1 <= arg2 /\ 3 <= arg1 /\ 3 <= undef307 /\ 3 <= undef309 /\ 3 <= undef388, {arg1 -> undef388, arg2 -> -1 + arg2, arg3 -> undef390, arg4 -> undef391, arg5 -> undef392, rest remain the same}>
Variables:
arg1, arg2, arg3, arg4, arg5

Precedence: 
Graph 0

Graph 1
<l0, l13, 0 <= undef185 /\ 1 + undef185 <= undef406 /\ 1 <= undef406 /\ undef407 = 0, {arg1 -> undef185, arg2 -> 0, arg3 -> 0, arg4 -> 0, arg5 -> 0, rest remain the same}>
<l0, l13, 0 <= undef194 /\ 1 + undef194 <= undef406 /\ 1 <= undef406 /\ 1 <= undef407, {arg1 -> undef194, arg2 -> 0, arg3 -> 0, arg4 -> undef407, arg5 -> 1, rest remain the same}>
<l0, l13, 0 <= undef203 /\ 0 <= undef205 /\ 1 + undef203 <= undef406 /\ 1 <= undef406 /\ 1 <= undef407, {arg1 -> undef203, arg2 -> 0, arg3 -> undef205, arg4 -> undef407, arg5 -> 1, rest remain the same}>

Graph 2
<l0, l8, undef10 <= undef406 /\ undef60 <= undef10 /\ undef60 <= undef11 /\ 0 <= undef62 /\ 0 <= undef69 /\ 0 <= undef407 /\ 2 <= undef61 /\ 1 <= undef10 /\ 1 <= undef11 /\ 1 <= undef60 /\ 1 + undef69 <= undef70 /\ 1 <= undef70 /\ 1 <= undef406, {arg1 -> undef60, arg2 -> undef61, arg3 -> undef62, arg4 -> 1 + undef69, arg5 -> undef64, rest remain the same}>

Graph 3
<l0, l15, undef10 <= undef406 /\ undef29 <= undef10 /\ 0 <= undef11 /\ undef30 <= undef11 /\ undef267 <= undef30 /\ undef38 <= undef31 /\ undef276 <= undef31 /\ 0 <= undef268 /\ 0 <= undef407 /\ 2 + undef269 <= undef30 /\ 1 <= undef10 /\ 1 <= undef29 /\ 1 <= undef30 /\ 1 <= undef267 /\ 1 <= undef406 /\ undef29 <= 1 + undef11, {arg1 -> undef267, arg2 -> undef268, arg3 -> undef269, arg4 -> undef270, arg5 -> undef271, rest remain the same}>
<l0, l15, undef10 <= undef406 /\ undef39 <= undef10 /\ 0 <= undef11 /\ undef40 <= undef11 /\ undef267 <= undef40 /\ 0 <= undef48 /\ 0 <= undef268 /\ 0 <= undef407 /\ 2 + undef269 <= undef40 /\ 1 <= undef10 /\ 1 <= undef39 /\ 1 <= undef40 /\ 1 + undef48 <= undef49 /\ 1 <= undef267 /\ 1 <= undef406 /\ undef39 <= 1 + undef11 /\ undef276 <= 1 + undef48, {arg1 -> undef267, arg2 -> undef268, arg3 -> undef269, arg4 -> undef270, arg5 -> undef271, rest remain the same}>
<l0, l15, undef10 <= undef406 /\ undef277 <= undef11 /\ 0 <= undef278 /\ 0 <= undef286 /\ 0 <= undef288 /\ 0 <= undef407 /\ 2 + undef279 <= undef11 /\ 1 <= undef10 /\ 1 <= undef11 /\ 1 <= undef277 /\ 1 + undef286 <= undef287 /\ 1 <= undef287 /\ 1 <= undef406, {arg1 -> undef277, arg2 -> undef278, arg3 -> undef279, arg4 -> undef280, arg5 -> undef281, rest remain the same}>

Graph 4
<l0, l9, undef10 <= undef406 /\ undef29 <= undef10 /\ 0 <= undef11 /\ undef30 <= undef11 /\ undef50 <= undef29 /\ undef50 <= undef30 /\ undef38 <= undef31 /\ undef59 <= undef31 /\ undef71 <= undef51 /\ 0 <= undef59 /\ undef81 <= undef80 /\ 0 <= undef407 /\ 2 <= undef51 /\ 2 + undef52 <= undef51 /\ 2 <= undef71 /\ 1 <= undef10 /\ 1 <= undef29 /\ 1 <= undef30 /\ 1 <= undef50 /\ 1 <= undef406 /\ undef29 <= 1 + undef11, {arg1 -> undef71, arg2 -> 0, arg3 -> undef73, arg4 -> undef74, arg5 -> undef75, rest remain the same}>
<l0, l9, undef10 <= undef406 /\ undef29 <= undef10 /\ 0 <= undef11 /\ undef30 <= undef11 /\ undef50 <= undef29 /\ undef50 <= undef30 /\ undef38 <= undef31 /\ undef59 <= undef31 /\ undef82 <= undef50 /\ undef83 <= undef51 /\ 0 <= undef59 /\ undef114 <= undef83 /\ 0 <= undef91 /\ 0 <= undef407 /\ 2 <= undef51 /\ 2 + undef52 <= undef51 /\ 2 + undef52 <= undef83 /\ 2 <= undef83 /\ 2 <= undef114 /\ 1 <= undef10 /\ 1 <= undef29 /\ 1 <= undef30 /\ 1 <= undef50 /\ 1 + undef82 <= undef51 /\ 1 <= undef82 /\ 1 + undef91 <= undef92 /\ 1 + undef91 <= undef123 /\ 1 <= undef123 /\ 1 <= undef406 /\ undef29 <= 1 + undef11, {arg1 -> undef114, arg2 -> 0, arg3 -> undef116, arg4 -> undef117, arg5 -> undef118, rest remain the same}>
<l0, l9, undef10 <= undef406 /\ undef29 <= undef10 /\ 0 <= undef11 /\ undef30 <= undef11 /\ undef50 <= undef29 /\ undef50 <= undef30 /\ undef38 <= undef31 /\ undef59 <= undef31 /\ undef93 <= undef50 /\ undef94 <= undef51 /\ 0 <= undef59 /\ undef114 <= undef94 /\ 0 <= undef95 /\ 0 <= undef102 /\ 0 <= undef407 /\ 2 <= undef51 /\ 2 + undef52 <= undef51 /\ 2 + undef52 <= undef94 /\ 2 <= undef94 /\ 2 <= undef114 /\ 1 <= undef10 /\ 1 <= undef29 /\ 1 <= undef30 /\ 1 <= undef50 /\ 1 + undef93 <= undef51 /\ 1 <= undef93 /\ 1 + undef102 <= undef103 /\ 1 + undef102 <= undef123 /\ 1 <= undef123 /\ 1 <= undef406 /\ undef29 <= 1 + undef11, {arg1 -> undef114, arg2 -> undef95, arg3 -> undef116, arg4 -> undef117, arg5 -> undef118, rest remain the same}>
<l0, l9, undef10 <= undef406 /\ undef39 <= undef10 /\ 0 <= undef11 /\ undef40 <= undef11 /\ undef50 <= undef39 /\ undef50 <= undef40 /\ 0 <= undef48 /\ undef71 <= undef51 /\ 0 <= undef59 /\ undef81 <= undef80 /\ 0 <= undef407 /\ 2 <= undef51 /\ 2 + undef52 <= undef51 /\ 2 <= undef71 /\ 1 <= undef10 /\ 1 <= undef39 /\ 1 <= undef40 /\ 1 + undef48 <= undef49 /\ 1 <= undef50 /\ 1 <= undef406 /\ undef39 <= 1 + undef11 /\ undef59 <= 1 + undef48, {arg1 -> undef71, arg2 -> 0, arg3 -> undef73, arg4 -> undef74, arg5 -> undef75, rest remain the same}>
<l0, l9, undef10 <= undef406 /\ undef39 <= undef10 /\ 0 <= undef11 /\ undef40 <= undef11 /\ undef50 <= undef39 /\ undef50 <= undef40 /\ 0 <= undef48 /\ undef82 <= undef50 /\ undef83 <= undef51 /\ 0 <= undef59 /\ undef114 <= undef83 /\ 0 <= undef91 /\ 0 <= undef407 /\ 2 <= undef51 /\ 2 + undef52 <= undef51 /\ 2 + undef52 <= undef83 /\ 2 <= undef83 /\ 2 <= undef114 /\ 1 <= undef10 /\ 1 <= undef39 /\ 1 <= undef40 /\ 1 + undef48 <= undef49 /\ 1 <= undef50 /\ 1 + undef82 <= undef51 /\ 1 <= undef82 /\ 1 + undef91 <= undef92 /\ 1 + undef91 <= undef123 /\ 1 <= undef123 /\ 1 <= undef406 /\ undef39 <= 1 + undef11 /\ undef59 <= 1 + undef48, {arg1 -> undef114, arg2 -> 0, arg3 -> undef116, arg4 -> undef117, arg5 -> undef118, rest remain the same}>
<l0, l9, undef10 <= undef406 /\ undef39 <= undef10 /\ 0 <= undef11 /\ undef40 <= undef11 /\ undef50 <= undef39 /\ undef50 <= undef40 /\ 0 <= undef48 /\ undef93 <= undef50 /\ undef94 <= undef51 /\ 0 <= undef59 /\ undef114 <= undef94 /\ 0 <= undef95 /\ 0 <= undef102 /\ 0 <= undef407 /\ 2 <= undef51 /\ 2 + undef52 <= undef51 /\ 2 + undef52 <= undef94 /\ 2 <= undef94 /\ 2 <= undef114 /\ 1 <= undef10 /\ 1 <= undef39 /\ 1 <= undef40 /\ 1 + undef48 <= undef49 /\ 1 <= undef50 /\ 1 + undef93 <= undef51 /\ 1 <= undef93 /\ 1 + undef102 <= undef103 /\ 1 + undef102 <= undef123 /\ 1 <= undef123 /\ 1 <= undef406 /\ undef39 <= 1 + undef11 /\ undef59 <= 1 + undef48, {arg1 -> undef114, arg2 -> undef95, arg3 -> undef116, arg4 -> undef117, arg5 -> undef118, rest remain the same}>
<l8, l9, undef104 <= arg1 /\ 0 <= arg2 /\ undef105 <= arg2 /\ undef133 <= undef104 /\ 0 <= undef105 /\ undef134 <= undef105 /\ 0 <= undef113 /\ undef153 <= undef134 /\ undef142 <= undef135 /\ undef162 <= undef135 /\ 1 <= arg1 /\ 1 <= undef104 /\ 1 <= undef133 /\ 1 <= undef134 /\ 1 <= undef135 /\ 1 <= undef153 /\ 1 <= undef162 /\ undef104 <= 1 + arg2 /\ undef133 <= 1 + undef105 /\ arg3 = 0, {arg1 -> undef153, arg2 -> 0, arg3 -> undef155, arg4 -> undef156, arg5 -> undef157, rest remain the same}>
<l8, l9, undef104 <= arg1 /\ 0 <= arg2 /\ undef105 <= arg2 /\ undef163 <= undef104 /\ 0 <= undef105 /\ undef164 <= undef105 /\ 0 <= undef113 /\ undef153 <= undef164 /\ 1 <= arg1 /\ 1 <= undef104 /\ 1 <= undef153 /\ 1 <= undef162 /\ 1 <= undef163 /\ 1 <= undef164 /\ 1 + undef172 <= undef173 /\ 1 <= undef172 /\ undef104 <= 1 + arg2 /\ undef163 <= 1 + undef105 /\ undef162 <= 1 + undef172 /\ arg3 = 0, {arg1 -> undef153, arg2 -> 0, arg3 -> undef155, arg4 -> undef156, arg5 -> undef157, rest remain the same}>
<l8, l9, undef104 <= arg1 /\ 0 <= arg2 /\ undef105 <= arg2 /\ undef174 <= undef105 /\ 0 <= undef113 /\ 0 <= undef175 /\ 2 <= undef184 /\ 1 <= arg1 /\ 1 <= undef104 /\ 1 <= undef105 /\ 1 <= undef174 /\ 1 + undef183 <= undef184 /\ 1 <= undef183 /\ undef104 <= 1 + arg2 /\ arg3 = 0, {arg1 -> undef174, arg2 -> undef175, arg3 -> undef176, arg4 -> undef177, arg5 -> undef178, rest remain the same}>
<l8, l9, undef143 <= arg1 /\ 0 <= arg2 /\ undef144 <= arg2 /\ undef133 <= undef143 /\ undef134 <= undef144 /\ undef153 <= undef134 /\ undef142 <= undef135 /\ undef162 <= undef135 /\ 0 <= undef144 /\ 0 <= undef152 /\ 1 <= arg1 /\ 1 + undef144 <= arg1 /\ 1 <= arg3 /\ 1 <= undef133 /\ 1 <= undef134 /\ 1 <= undef135 /\ 1 <= undef143 /\ 1 <= undef153 /\ 1 <= undef162 /\ undef143 <= 1 + arg2 /\ undef133 <= 1 + undef144, {arg1 -> undef153, arg2 -> 0, arg3 -> undef155, arg4 -> undef156, arg5 -> undef157, rest remain the same}>
<l8, l9, undef143 <= arg1 /\ 0 <= arg2 /\ undef144 <= arg2 /\ undef163 <= undef143 /\ 0 <= undef144 /\ undef164 <= undef144 /\ 0 <= undef152 /\ undef153 <= undef164 /\ 1 <= arg1 /\ 1 + undef144 <= arg1 /\ 1 <= arg3 /\ 1 <= undef143 /\ 1 <= undef153 /\ 1 <= undef162 /\ 1 <= undef163 /\ 1 <= undef164 /\ 1 + undef172 <= undef173 /\ 1 <= undef172 /\ undef143 <= 1 + arg2 /\ undef163 <= 1 + undef144 /\ undef162 <= 1 + undef172, {arg1 -> undef153, arg2 -> 0, arg3 -> undef155, arg4 -> undef156, arg5 -> undef157, rest remain the same}>
<l8, l9, undef143 <= arg1 /\ 0 <= arg2 /\ undef144 <= arg2 /\ undef174 <= undef144 /\ 0 <= undef152 /\ 0 <= undef175 /\ 2 <= undef184 /\ 1 <= arg1 /\ 1 + undef144 <= arg1 /\ 1 <= arg3 /\ 1 <= undef143 /\ 1 <= undef144 /\ 1 <= undef174 /\ 1 + undef183 <= undef184 /\ 1 <= undef183 /\ undef143 <= 1 + arg2, {arg1 -> undef174, arg2 -> undef175, arg3 -> undef176, arg4 -> undef177, arg5 -> undef178, rest remain the same}>

Map Locations to Subgraph:
( 0 , 0 )
( 8 , 2 )
( 9 , 4 )
( 13 , 1 )
( 15 , 3 )

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

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

Checking conditional termination of SCC {l13}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.005703s
Ranking function: -1 - arg2 + arg3
New Graphs: 
Proving termination of subgraph 2
Checking unfeasibility...
Time used: 0.002037

Checking conditional termination of SCC {l8}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000581s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001940s
Trying to remove transition: <l8, l8, undef124 <= arg1 /\ undef124 <= arg2 /\ 0 <= undef125 /\ 1 <= arg1 /\ 1 <= arg2 /\ 1 <= arg3 /\ 1 <= undef124, {arg1 -> undef124, arg2 -> undef125, arg5 -> undef128, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.008714s
Time used: 0.008712

LOG: SAT solveNonLinear - Elapsed time: 0.016069s
Cost: 1; Total time: 0.015648
Failed at location 8: arg1 + arg3 <= 1
Before Improving: 
Quasi-invariant at l8: arg1 + arg3 <= 1
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001792s
Remaining time after improvement: 0.99905
Termination implied by a set of quasi-invariant(s):
Quasi-invariant at l8: arg1 + arg3 <= 1
[ Invariant Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l8, l8, undef124 <= arg1 /\ undef124 <= arg2 /\ 0 <= undef125 /\ 1 <= arg1 /\ 1 <= arg2 /\ 1 <= arg3 /\ 1 <= undef124, {arg1 -> undef124, arg2 -> undef125, arg5 -> undef128, rest remain the same}>
[ Termination Graph ]
Strengthening and disabling transitions...
> It's unfeasible. Removing transition: 
<l8, l8, undef124 <= arg1 /\ undef124 <= arg2 /\ 0 <= undef125 /\ 1 <= arg1 /\ 1 <= arg2 /\ 1 <= arg3 /\ 1 <= undef124, {arg1 -> undef124, arg2 -> undef125, arg5 -> undef128, rest remain the same}>
New Graphs: 
Calling Safety with literal arg1 + arg3 <= 1 and entry <l0, l8, undef10 <= undef406 /\ undef60 <= undef10 /\ undef60 <= undef11 /\ 0 <= undef62 /\ 0 <= undef69 /\ 0 <= undef407 /\ 2 <= undef61 /\ 1 <= undef10 /\ 1 <= undef11 /\ 1 <= undef60 /\ 1 + undef69 <= undef70 /\ 1 <= undef70 /\ 1 <= undef406, {arg1 -> undef60, arg2 -> undef61, arg3 -> undef62, arg4 -> 1 + undef69, arg5 -> undef64, rest remain the same}>

LOG: CALL check - Post:arg1 + arg3 <= 1 - Process 1
* Exit transition: <l0, l8, undef10 <= undef406 /\ undef60 <= undef10 /\ undef60 <= undef11 /\ 0 <= undef62 /\ 0 <= undef69 /\ 0 <= undef407 /\ 2 <= undef61 /\ 1 <= undef10 /\ 1 <= undef11 /\ 1 <= undef60 /\ 1 + undef69 <= undef70 /\ 1 <= undef70 /\ 1 <= undef406, {arg1 -> undef60, arg2 -> undef61, arg3 -> undef62, arg4 -> 1 + undef69, arg5 -> undef64, rest remain the same}>
* Postcondition  : arg1 + arg3 <= 1

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.000706s
INVARIANTS: 
8: 
Quasi-INVARIANTS to narrow Graph: 
8: arg1 + arg3 <= 1 , 
Narrowing transition: 
<l8, l8, undef124 <= arg1 /\ undef124 <= arg2 /\ 0 <= undef125 /\ 1 <= arg1 /\ 1 <= arg2 /\ 1 <= arg3 /\ 1 <= undef124, {arg1 -> undef124, arg2 -> undef125, arg5 -> undef128, rest remain the same}>

LOG: Narrow transition size 1
invGraph after Narrowing: 
Transitions:
<l8, l8, undef124 <= arg1 /\ undef124 <= arg2 /\ 0 <= undef125 /\ 2 <= arg1 + arg3 /\ 1 <= arg1 /\ 1 <= arg2 /\ 1 <= arg3 /\ 1 <= undef124, {arg1 -> undef124, arg2 -> undef125, arg5 -> undef128, rest remain the same}>
Variables:
arg1, arg2, arg3, arg5
Checking conditional termination of SCC {l8}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000540s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002103s
Trying to remove transition: <l8, l8, undef124 <= arg1 /\ undef124 <= arg2 /\ 0 <= undef125 /\ 2 <= arg1 + arg3 /\ 1 <= arg1 /\ 1 <= arg2 /\ 1 <= arg3 /\ 1 <= undef124, {arg1 -> undef124, arg2 -> undef125, arg5 -> undef128, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.012886s
Time used: 0.012885

LOG: SAT solveNonLinear - Elapsed time: 0.020681s
Cost: 1; Total time: 0.020245
Failed at location 8: arg3 <= 0
Before Improving: 
Quasi-invariant at l8: arg3 <= 0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001934s
Remaining time after improvement: 0.998946
Termination implied by a set of quasi-invariant(s):
Quasi-invariant at l8: arg3 <= 0
[ Invariant Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l8, l8, undef124 <= arg1 /\ undef124 <= arg2 /\ 0 <= undef125 /\ 2 <= arg1 + arg3 /\ 1 <= arg1 /\ 1 <= arg2 /\ 1 <= arg3 /\ 1 <= undef124, {arg1 -> undef124, arg2 -> undef125, arg5 -> undef128, rest remain the same}>
[ Termination Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l8, l8, undef124 <= arg1 /\ undef124 <= arg2 /\ 0 <= undef125 /\ 2 <= arg1 + arg3 /\ 1 <= arg1 /\ 1 <= arg2 /\ 1 <= arg3 /\ 1 <= undef124, {arg1 -> undef124, arg2 -> undef125, arg5 -> undef128, rest remain the same}>
New Graphs: 
Calling Safety with literal arg3 <= 0 and entry <l0, l8, undef10 <= undef406 /\ undef60 <= undef10 /\ undef60 <= undef11 /\ 0 <= undef62 /\ 0 <= undef69 /\ 0 <= undef407 /\ 2 <= undef60 + undef62 /\ 2 <= undef61 /\ 1 <= undef10 /\ 1 <= undef11 /\ 1 <= undef60 /\ 1 + undef69 <= undef70 /\ 1 <= undef70 /\ 1 <= undef406, {arg1 -> undef60, arg2 -> undef61, arg3 -> undef62, arg4 -> 1 + undef69, arg5 -> undef64, rest remain the same}>

LOG: CALL check - Post:arg3 <= 0 - Process 2
* Exit transition: <l0, l8, undef10 <= undef406 /\ undef60 <= undef10 /\ undef60 <= undef11 /\ 0 <= undef62 /\ 0 <= undef69 /\ 0 <= undef407 /\ 2 <= undef60 + undef62 /\ 2 <= undef61 /\ 1 <= undef10 /\ 1 <= undef11 /\ 1 <= undef60 /\ 1 + undef69 <= undef70 /\ 1 <= undef70 /\ 1 <= undef406, {arg1 -> undef60, arg2 -> undef61, arg3 -> undef62, arg4 -> 1 + undef69, arg5 -> undef64, rest remain the same}>
* Postcondition  : arg3 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.000641s
INVARIANTS: 
8: 
Quasi-INVARIANTS to narrow Graph: 
8: arg3 <= 0 , 
Narrowing transition: 
<l8, l8, undef124 <= arg1 /\ undef124 <= arg2 /\ 0 <= undef125 /\ 2 <= arg1 + arg3 /\ 1 <= arg1 /\ 1 <= arg2 /\ 1 <= arg3 /\ 1 <= undef124, {arg1 -> undef124, arg2 -> undef125, arg5 -> undef128, rest remain the same}>

LOG: Narrow transition size 1
invGraph after Narrowing: 
Transitions:
<l8, l8, undef124 <= arg1 /\ undef124 <= arg2 /\ 0 <= undef125 /\ 2 <= arg1 + arg3 /\ 1 <= arg1 /\ 1 <= arg2 /\ 1 <= arg3 /\ 1 <= undef124, {arg1 -> undef124, arg2 -> undef125, arg5 -> undef128, rest remain the same}>
Variables:
arg1, arg2, arg3, arg5
Checking conditional termination of SCC {l8}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000552s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002102s
Trying to remove transition: <l8, l8, undef124 <= arg1 /\ undef124 <= arg2 /\ 0 <= undef125 /\ 2 <= arg1 + arg3 /\ 1 <= arg1 /\ 1 <= arg2 /\ 1 <= arg3 /\ 1 <= undef124, {arg1 -> undef124, arg2 -> undef125, arg5 -> undef128, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.012880s
Time used: 0.007506

Proving non-termination of subgraph 2
Transitions:
<l8, l8, undef124 <= arg1 /\ undef124 <= arg2 /\ 0 <= undef125 /\ 2 <= arg1 + arg3 /\ 1 <= arg1 /\ 1 <= arg2 /\ 1 <= arg3 /\ 1 <= undef124, {arg1 -> undef124, arg2 -> undef125, arg5 -> undef128, rest remain the same}>
Variables:
arg1, arg2, arg3, arg5

Checking that every undef value has an assignment...

LOG: CALL solveLinear

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

Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.027904s
Time used: 0.02761
Improving Solution with cost 5 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.077263s
Time used: 0.07726

LOG: SAT solveNonLinear - Elapsed time: 0.105167s
Cost: 5; Total time: 0.10487
Minimizing number of undef constraints...

LOG: CALL solveNonLinear

LOG: RETURN solveNonLinear - Elapsed time: 0.014155s
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 exit transition (result): 
<l8, end, arg3 <= 0 /\ 2 <= arg1 + arg3 /\ 1 <= arg1 /\ 1 <= arg2, {all remain the same}>
Strengthening exit transition (result): 
<l8, end, arg2 <= 0 /\ 2 <= arg1 + arg3 /\ 1 <= arg1, {all remain the same}>
Strengthening exit transition (result): 
<l8, end, arg3 <= 0 /\ 1 <= arg1 /\ arg1 + arg3 <= 1, {all remain the same}>

Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

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

Checking conditional non-termination of SCC {l8}...
EXIT TRANSITIONS:
<l8, end, arg3 <= 0 /\ 2 <= arg1 + arg3 /\ 1 <= arg1 /\ 1 <= arg2, {all remain the same}>
<l8, end, arg2 <= 0 /\ 2 <= arg1 + arg3 /\ 1 <= arg1, {all remain the same}>
<l8, end, arg3 <= 0 /\ 1 <= arg1 /\ arg1 + arg3 <= 1, {all remain the same}>

Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.023778s
Time used: 0.023532
Improving Solution with cost 3 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.037889s
Time used: 0.037886

LOG: SAT solveNonLinear - Elapsed time: 0.061667s
Cost: 3; Total time: 0.061418
Failed at location 8: 1 + arg1 <= arg3
Before Improving: 
Quasi-invariant at l8: 1 + arg1 <= arg3
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011222s
Remaining time after improvement: 0.998322
Minimizing number of undef constraints...

LOG: CALL solveNonLinear

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

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

Strengthening and disabling EXIT transitions...
Closed exits from l8: 2
Strengthening exit transition (result): 
<l8, end, arg2 <= 0 /\ 2 <= arg1 + arg3 /\ 1 + arg1 <= arg3 /\ 1 <= arg1, {all remain the same}>

Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

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

Checking conditional non-termination of SCC {l8}...
EXIT TRANSITIONS:
<l8, end, arg2 <= 0 /\ 2 <= arg1 + arg3 /\ 1 + arg1 <= arg3 /\ 1 <= arg1, {all remain the same}>

Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.022160s
Time used: 0.022102

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

LOG: CALL solveNonLinear

LOG: RETURN solveNonLinear - Elapsed time: 0.004898s
Non-termination implied by a set of quasi-invariant(s):
Quasi-invariant at l8: 1 <= arg2
Constraint over undef '1 <= undef125' in transition:
<l8, l8, undef124 <= arg1 /\ undef124 <= arg2 /\ 0 <= undef125 /\ 2 <= arg1 + arg3 /\ 1 + arg1 <= arg3 /\ 1 <= arg1 /\ 1 <= arg2 /\ 1 <= arg3 /\ 1 <= undef124, {arg1 -> undef124, arg2 -> undef125, arg5 -> undef128, rest remain the same}>

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

Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

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

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

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

Calling reachability with...
Transition: <l0, l8, undef10 <= undef406 /\ undef60 <= undef10 /\ undef60 <= undef11 /\ 0 <= undef62 /\ 0 <= undef69 /\ 0 <= undef407 /\ 2 <= undef61 /\ 1 <= undef10 /\ 1 <= undef11 /\ 1 <= undef60 /\ 1 + undef69 <= undef70 /\ 1 <= undef70 /\ 1 <= undef406, {arg1 -> undef60, arg2 -> undef61, arg3 -> undef62, arg4 -> 1 + undef69, arg5 -> undef64, rest remain the same}>
Conditions: 1 + arg1 <= arg3, 1 <= arg1, 1 <= arg2, 
OPEN EXITS: 
<l0, l8, undef10 <= undef406 /\ undef60 <= undef10 /\ undef60 <= undef11 /\ 0 <= undef62 /\ 0 <= undef69 /\ 0 <= undef407 /\ 2 <= undef61 /\ 1 <= undef10 /\ 1 <= undef11 /\ 1 + undef60 <= undef62 /\ 1 <= undef60 /\ 1 + undef69 <= undef70 /\ 1 <= undef70 /\ 1 <= undef406, {arg1 -> undef60, arg2 -> undef61, arg3 -> undef62, arg4 -> 1 + undef69, arg5 -> undef64, rest remain the same}>

> Conditions are reachable!

Program does NOT terminate