YES

Solver Timeout: 4
Global Timeout: 300
No parsing errors!
Init Location: 0
Transitions:
<l0, l9, true>
<l1, l2, (arg2 > 9) /\ (undef2 > 9) /\ ((arg6 + 5) <= arg2) /\ ((arg7 + 3) <= arg2), par{arg2 -> undef2, arg3 -> 0, arg4 -> 0, arg5 -> arg4, arg6 -> undef6, arg7 -> 0, arg8 -> 0, arg9 -> 0, arg10 -> undef10, arg11 -> undef11, arg12 -> undef12, arg13 -> arg3, arg14 -> arg3, arg15 -> arg4, arg16 -> undef16, arg17 -> arg5, arg18 -> arg6, arg19 -> undef19, arg20 -> undef20, arg21 -> arg7, arg22 -> undef22, arg23 -> undef23}>
<l3, l4, (arg1 > 0) /\ (arg2 > 6) /\ (undef24 > 6) /\ ((arg6 + 5) <= arg2) /\ ((arg7 + 7) <= arg2) /\ ((arg9 + 3) <= arg2) /\ ((arg8 + 7) <= arg2), par{arg1 -> undef24, arg2 -> arg3, arg3 -> arg4, arg4 -> undef27, arg5 -> arg6, arg6 -> undef29, arg7 -> undef30, arg8 -> arg9, arg9 -> undef32, arg10 -> undef33, arg11 -> undef34, arg12 -> undef35, arg13 -> undef36, arg14 -> undef37, arg15 -> undef38, arg16 -> undef39, arg17 -> undef40, arg18 -> undef41, arg19 -> undef42, arg20 -> undef43, arg21 -> undef44, arg22 -> undef45, arg23 -> undef46}>
<l5, l4, (undef70 > ~(1)) /\ (arg2 > 0) /\ (arg1 > 0) /\ (undef47 > 6), par{arg1 -> undef47, arg2 -> undef48, arg3 -> undef49, arg4 -> arg2, arg5 -> undef51, arg6 -> undef52, arg7 -> undef53, arg8 -> undef54, arg9 -> undef55, arg10 -> undef56, arg11 -> undef57, arg12 -> undef58, arg13 -> undef59, arg14 -> undef60, arg15 -> undef61, arg16 -> undef62, arg17 -> undef63, arg18 -> undef64, arg19 -> undef65, arg20 -> undef66, arg21 -> undef67, arg22 -> undef68, arg23 -> undef69}>
<l4, l6, (undef94 < arg4) /\ (undef94 > 0) /\ (undef72 > ~(1)) /\ (undef95 <= undef72) /\ (undef72 < arg5) /\ (arg1 > 6) /\ ((arg5 + 5) <= arg1) /\ ((arg6 + 7) <= arg1) /\ ((arg8 + 3) <= arg1) /\ ((arg7 + 7) <= arg1), par{arg1 -> arg5, arg2 -> undef72, arg4 -> undef74, arg5 -> undef75, arg6 -> undef76, arg7 -> undef77, arg8 -> undef78, arg9 -> undef79, arg10 -> undef80, arg11 -> undef81, arg12 -> undef82, arg13 -> undef83, arg14 -> undef84, arg15 -> undef85, arg16 -> undef86, arg17 -> undef87, arg18 -> undef88, arg19 -> undef89, arg20 -> undef90, arg21 -> undef91, arg22 -> undef92, arg23 -> undef93}>
<l6, l6, (arg3 > ~(1)) /\ (undef119 > 0) /\ (undef119 < arg3) /\ (arg2 < arg1) /\ (undef119 < undef98), par{arg1 -> (arg1 - 1), arg3 -> undef98, arg4 -> undef99, arg5 -> undef100, arg6 -> undef101, arg7 -> undef102, arg8 -> undef103, arg9 -> undef104, arg10 -> undef105, arg11 -> undef106, arg12 -> undef107, arg13 -> undef108, arg14 -> undef109, arg15 -> undef110, arg16 -> undef111, arg17 -> undef112, arg18 -> undef113, arg19 -> undef114, arg20 -> undef115, arg21 -> undef116, arg22 -> undef117, arg23 -> undef118}>
<l6, l6, (arg2 < arg1) /\ (undef143 < arg3) /\ (arg3 > ~(1)), par{arg1 -> (arg1 - 1), arg3 -> 1, arg4 -> undef123, arg5 -> undef124, arg6 -> undef125, arg7 -> undef126, arg8 -> undef127, arg9 -> undef128, arg10 -> undef129, arg11 -> undef130, arg12 -> undef131, arg13 -> undef132, arg14 -> undef133, arg15 -> undef134, arg16 -> undef135, arg17 -> undef136, arg18 -> undef137, arg19 -> undef138, arg20 -> undef139, arg21 -> undef140, arg22 -> undef141, arg23 -> undef142}>
<l4, l7, (undef167 < arg4) /\ (undef167 > 0) /\ (undef145 > ~(1)) /\ (undef168 > undef145) /\ (undef145 < arg5) /\ (arg1 > 6) /\ ((arg5 + 5) <= arg1) /\ ((arg6 + 7) <= arg1) /\ ((arg8 + 3) <= arg1) /\ ((arg7 + 7) <= arg1), par{arg1 -> 0, arg2 -> undef145, arg3 -> arg2, arg4 -> undef147, arg5 -> undef148, arg6 -> undef149, arg7 -> undef150, arg8 -> undef151, arg9 -> undef152, arg10 -> undef153, arg11 -> undef154, arg12 -> undef155, arg13 -> undef156, arg14 -> undef157, arg15 -> undef158, arg16 -> undef159, arg17 -> undef160, arg18 -> undef161, arg19 -> undef162, arg20 -> undef163, arg21 -> undef164, arg22 -> undef165, arg23 -> undef166}>
<l7, l7, (arg3 > ~(1)) /\ (undef192 > 0) /\ (undef192 < arg3) /\ (arg2 >= arg1) /\ (undef192 < undef171), par{arg1 -> (arg1 + 1), arg3 -> undef171, arg4 -> undef172, arg5 -> undef173, arg6 -> undef174, arg7 -> undef175, arg8 -> undef176, arg9 -> undef177, arg10 -> undef178, arg11 -> undef179, arg12 -> undef180, arg13 -> undef181, arg14 -> undef182, arg15 -> undef183, arg16 -> undef184, arg17 -> undef185, arg18 -> undef186, arg19 -> undef187, arg20 -> undef188, arg21 -> undef189, arg22 -> undef190, arg23 -> undef191}>
<l7, l7, (arg2 >= arg1) /\ (undef216 < arg3) /\ (arg3 > ~(1)), par{arg1 -> (arg1 + 1), arg3 -> 1, arg4 -> undef196, arg5 -> undef197, arg6 -> undef198, arg7 -> undef199, arg8 -> undef200, arg9 -> undef201, arg10 -> undef202, arg11 -> undef203, arg12 -> undef204, arg13 -> undef205, arg14 -> undef206, arg15 -> undef207, arg16 -> undef208, arg17 -> undef209, arg18 -> undef210, arg19 -> undef211, arg20 -> undef212, arg21 -> undef213, arg22 -> undef214, arg23 -> undef215}>
<l5, l1, (undef217 > ~(1)) /\ (arg2 > 0) /\ ((undef218 - 7) <= arg1) /\ (arg1 > 0) /\ (undef218 > 7), par{arg1 -> undef217, arg2 -> undef218, arg3 -> undef219, arg4 -> undef220, arg5 -> 1, arg6 -> 0, arg7 -> 0, arg8 -> undef224, arg9 -> undef225, arg10 -> undef226, arg11 -> undef227, arg12 -> undef228, arg13 -> undef229, arg14 -> undef230, arg15 -> undef231, arg16 -> undef232, arg17 -> undef233, arg18 -> undef234, arg19 -> undef235, arg20 -> undef236, arg21 -> undef237, arg22 -> undef238, arg23 -> undef239}>
<l2, l8, (arg2 > 11) /\ (undef240 > 11) /\ (arg2 >= (arg18 + 5)) /\ (arg2 >= (arg19 + 9)) /\ (arg2 >= (arg20 + 9)) /\ (arg2 >= (arg21 + 3)), par{arg1 -> undef240, arg2 -> arg1, arg3 -> arg4, arg4 -> arg5, arg5 -> arg11, arg6 -> arg10, arg7 -> arg3, arg8 -> arg6, arg9 -> arg7, arg10 -> arg8, arg11 -> arg9, arg16 -> arg17, arg17 -> arg18, arg18 -> undef257, arg19 -> undef258, arg20 -> undef259, arg21 -> undef260, arg22 -> undef261, arg23 -> arg21}>
<l8, l8, (arg2 > 0) /\ (undef286 > ~(1)) /\ (arg16 > 0) /\ (arg16 < undef286) /\ (arg4 > 0) /\ (arg3 > 0) /\ (arg7 > 0) /\ (arg6 > 0) /\ (arg5 > 0) /\ (arg14 > 0) /\ (undef287 > ~(1)) /\ (arg9 > 0) /\ (arg12 > 0) /\ (arg10 > 0) /\ (arg15 > 0) /\ (arg13 > 0) /\ (arg11 > 0) /\ (arg8 > 0) /\ (arg23 > ~(1)) /\ (arg17 > ~(1)) /\ (arg1 > 11) /\ (undef263 > 11) /\ ((arg17 + 5) <= arg1) /\ ((arg18 + 9) <= arg1) /\ ((arg19 + 9) <= arg1) /\ ((arg20 + 9) <= arg1) /\ ((arg21 + 11) <= arg1) /\ ((arg23 + 3) <= arg1) /\ ((arg22 + 11) <= arg1), par{arg1 -> undef263, arg2 -> (arg2 - 1), arg5 -> undef267, arg6 -> undef268, arg7 -> undef269, arg8 -> undef270, arg9 -> undef271, arg10 -> undef272, arg11 -> undef273, arg12 -> undef274, arg13 -> undef275, arg14 -> undef276, arg15 -> undef277, arg16 -> (arg16 + 1), arg17 -> (arg17 + 1), arg18 -> undef280, arg19 -> undef281, arg20 -> undef282, arg21 -> undef283, arg22 -> undef284, arg23 -> (arg23 + 1)}>
<l9, l5, true, par{arg1 -> undef288, arg2 -> undef289, arg3 -> undef290, arg4 -> undef291, arg5 -> undef292, arg6 -> undef293, arg7 -> undef294, arg8 -> undef295, arg9 -> undef296, arg10 -> undef297, arg11 -> undef298, arg12 -> undef299, arg13 -> undef300, arg14 -> undef301, arg15 -> undef302, arg16 -> undef303, arg17 -> undef304, arg18 -> undef305, arg19 -> undef306, arg20 -> undef307, arg21 -> undef308, arg22 -> undef309, arg23 -> undef310}>

Fresh variables:
undef2, undef6, undef10, undef11, undef12, undef16, undef19, undef20, undef22, undef23, undef24, undef27, undef29, undef30, undef32, undef33, undef34, undef35, undef36, undef37, undef38, undef39, undef40, undef41, undef42, undef43, undef44, undef45, undef46, undef47, undef48, undef49, undef51, undef52, undef53, undef54, undef55, undef56, undef57, undef58, undef59, undef60, undef61, undef62, undef63, undef64, undef65, undef66, undef67, undef68, undef69, undef70, undef72, undef74, undef75, undef76, undef77, undef78, undef79, undef80, undef81, undef82, undef83, undef84, undef85, undef86, 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, undef115, undef116, undef117, undef118, undef119, undef123, undef124, undef125, undef126, undef127, undef128, undef129, undef130, undef131, undef132, undef133, undef134, undef135, undef136, undef137, undef138, undef139, undef140, undef141, undef142, undef143, undef145, undef147, undef148, undef149, undef150, undef151, undef152, undef153, undef154, undef155, undef156, undef157, undef158, undef159, undef160, undef161, undef162, undef163, undef164, undef165, undef166, undef167, undef168, undef171, undef172, undef173, undef174, undef175, undef176, undef177, undef178, undef179, undef180, undef181, undef182, undef183, undef184, undef185, undef186, undef187, undef188, undef189, undef190, undef191, undef192, undef196, undef197, undef198, undef199, undef200, undef201, undef202, undef203, undef204, undef205, undef206, undef207, undef208, undef209, undef210, undef211, undef212, undef213, undef214, undef215, undef216, undef217, undef218, undef219, undef220, undef224, undef225, undef226, undef227, undef228, undef229, undef230, undef231, undef232, undef233, undef234, undef235, undef236, undef237, undef238, undef239, undef240, undef257, undef258, undef259, undef260, undef261, undef263, undef267, undef268, undef269, undef270, undef271, undef272, undef273, undef274, undef275, undef276, undef277, undef280, undef281, undef282, undef283, undef284, undef286, undef287, undef288, undef289, undef290, undef291, undef292, undef293, undef294, undef295, undef296, undef297, undef298, undef299, undef300, undef301, undef302, undef303, undef304, undef305, undef306, undef307, undef308, undef309, undef310, 

Undef variables:
undef2, undef6, undef10, undef11, undef12, undef16, undef19, undef20, undef22, undef23, undef24, undef27, undef29, undef30, undef32, undef33, undef34, undef35, undef36, undef37, undef38, undef39, undef40, undef41, undef42, undef43, undef44, undef45, undef46, undef47, undef48, undef49, undef51, undef52, undef53, undef54, undef55, undef56, undef57, undef58, undef59, undef60, undef61, undef62, undef63, undef64, undef65, undef66, undef67, undef68, undef69, undef70, undef72, undef74, undef75, undef76, undef77, undef78, undef79, undef80, undef81, undef82, undef83, undef84, undef85, undef86, 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, undef115, undef116, undef117, undef118, undef119, undef123, undef124, undef125, undef126, undef127, undef128, undef129, undef130, undef131, undef132, undef133, undef134, undef135, undef136, undef137, undef138, undef139, undef140, undef141, undef142, undef143, undef145, undef147, undef148, undef149, undef150, undef151, undef152, undef153, undef154, undef155, undef156, undef157, undef158, undef159, undef160, undef161, undef162, undef163, undef164, undef165, undef166, undef167, undef168, undef171, undef172, undef173, undef174, undef175, undef176, undef177, undef178, undef179, undef180, undef181, undef182, undef183, undef184, undef185, undef186, undef187, undef188, undef189, undef190, undef191, undef192, undef196, undef197, undef198, undef199, undef200, undef201, undef202, undef203, undef204, undef205, undef206, undef207, undef208, undef209, undef210, undef211, undef212, undef213, undef214, undef215, undef216, undef217, undef218, undef219, undef220, undef224, undef225, undef226, undef227, undef228, undef229, undef230, undef231, undef232, undef233, undef234, undef235, undef236, undef237, undef238, undef239, undef240, undef257, undef258, undef259, undef260, undef261, undef263, undef267, undef268, undef269, undef270, undef271, undef272, undef273, undef274, undef275, undef276, undef277, undef280, undef281, undef282, undef283, undef284, undef286, undef287, undef288, undef289, undef290, undef291, undef292, undef293, undef294, undef295, undef296, undef297, undef298, undef299, undef300, undef301, undef302, undef303, undef304, undef305, undef306, undef307, undef308, undef309, undef310, 

Abstraction variables:

Exit nodes:

Accepting locations:

Asserts:

Preprocessed LLVMGraph
Init Location: 0
Transitions:
<l0, l6, (undef70 > ~(1)) /\ (undef289 > 0) /\ (undef288 > 0) /\ (undef47 > 6) /\ (undef94 < undef289) /\ (undef94 > 0) /\ (undef72 > ~(1)) /\ (undef95 <= undef72) /\ (undef72 < undef51) /\ (undef47 > 6) /\ ((undef51 + 5) <= undef47) /\ ((undef52 + 7) <= undef47) /\ ((undef54 + 3) <= undef47) /\ ((undef53 + 7) <= undef47), par{arg1 -> undef51, arg2 -> undef72, arg3 -> undef49, arg4 -> undef74, arg5 -> undef75, arg6 -> undef76, arg7 -> undef77, arg8 -> undef78, arg9 -> undef79, arg10 -> undef80, arg11 -> undef81, arg12 -> undef82, arg13 -> undef83, arg14 -> undef84, arg15 -> undef85, arg16 -> undef86, arg17 -> undef87, arg18 -> undef88, arg19 -> undef89, arg20 -> undef90, arg21 -> undef91, arg22 -> undef92, arg23 -> undef93}>
<l0, l7, (undef70 > ~(1)) /\ (undef289 > 0) /\ (undef288 > 0) /\ (undef47 > 6) /\ (undef167 < undef289) /\ (undef167 > 0) /\ (undef145 > ~(1)) /\ (undef168 > undef145) /\ (undef145 < undef51) /\ (undef47 > 6) /\ ((undef51 + 5) <= undef47) /\ ((undef52 + 7) <= undef47) /\ ((undef54 + 3) <= undef47) /\ ((undef53 + 7) <= undef47), par{arg1 -> 0, arg2 -> undef145, arg3 -> undef48, arg4 -> undef147, arg5 -> undef148, arg6 -> undef149, arg7 -> undef150, arg8 -> undef151, arg9 -> undef152, arg10 -> undef153, arg11 -> undef154, arg12 -> undef155, arg13 -> undef156, arg14 -> undef157, arg15 -> undef158, arg16 -> undef159, arg17 -> undef160, arg18 -> undef161, arg19 -> undef162, arg20 -> undef163, arg21 -> undef164, arg22 -> undef165, arg23 -> undef166}>
<l0, l8, (undef217 > ~(1)) /\ (undef289 > 0) /\ ((undef218 - 7) <= undef288) /\ (undef288 > 0) /\ (undef218 > 7) /\ (undef218 > 9) /\ (undef2 > 9) /\ ((0 + 5) <= undef218) /\ ((0 + 3) <= undef218) /\ (undef2 > 11) /\ (undef240 > 11) /\ (undef2 >= (0 + 5)) /\ (undef2 >= (undef19 + 9)) /\ (undef2 >= (undef20 + 9)) /\ (undef2 >= (0 + 3)), par{arg1 -> undef240, arg2 -> undef217, arg3 -> 0, arg4 -> undef220, arg5 -> undef11, arg6 -> undef10, arg7 -> 0, arg8 -> undef6, arg9 -> 0, arg10 -> 0, arg11 -> 0, arg12 -> undef12, arg13 -> undef219, arg14 -> undef219, arg15 -> undef220, arg16 -> 1, arg17 -> 0, arg18 -> undef257, arg19 -> undef258, arg20 -> undef259, arg21 -> undef260, arg22 -> undef261, arg23 -> 0}>
<l6, l6, (arg3 > ~(1)) /\ (undef119 > 0) /\ (undef119 < arg3) /\ (arg2 < arg1) /\ (undef119 < undef98), par{arg1 -> (arg1 - 1), arg3 -> undef98, arg4 -> undef99, arg5 -> undef100, arg6 -> undef101, arg7 -> undef102, arg8 -> undef103, arg9 -> undef104, arg10 -> undef105, arg11 -> undef106, arg12 -> undef107, arg13 -> undef108, arg14 -> undef109, arg15 -> undef110, arg16 -> undef111, arg17 -> undef112, arg18 -> undef113, arg19 -> undef114, arg20 -> undef115, arg21 -> undef116, arg22 -> undef117, arg23 -> undef118}>
<l6, l6, (arg2 < arg1) /\ (undef143 < arg3) /\ (arg3 > ~(1)), par{arg1 -> (arg1 - 1), arg3 -> 1, arg4 -> undef123, arg5 -> undef124, arg6 -> undef125, arg7 -> undef126, arg8 -> undef127, arg9 -> undef128, arg10 -> undef129, arg11 -> undef130, arg12 -> undef131, arg13 -> undef132, arg14 -> undef133, arg15 -> undef134, arg16 -> undef135, arg17 -> undef136, arg18 -> undef137, arg19 -> undef138, arg20 -> undef139, arg21 -> undef140, arg22 -> undef141, arg23 -> undef142}>
<l7, l7, (arg3 > ~(1)) /\ (undef192 > 0) /\ (undef192 < arg3) /\ (arg2 >= arg1) /\ (undef192 < undef171), par{arg1 -> (arg1 + 1), arg3 -> undef171, arg4 -> undef172, arg5 -> undef173, arg6 -> undef174, arg7 -> undef175, arg8 -> undef176, arg9 -> undef177, arg10 -> undef178, arg11 -> undef179, arg12 -> undef180, arg13 -> undef181, arg14 -> undef182, arg15 -> undef183, arg16 -> undef184, arg17 -> undef185, arg18 -> undef186, arg19 -> undef187, arg20 -> undef188, arg21 -> undef189, arg22 -> undef190, arg23 -> undef191}>
<l7, l7, (arg2 >= arg1) /\ (undef216 < arg3) /\ (arg3 > ~(1)), par{arg1 -> (arg1 + 1), arg3 -> 1, arg4 -> undef196, arg5 -> undef197, arg6 -> undef198, arg7 -> undef199, arg8 -> undef200, arg9 -> undef201, arg10 -> undef202, arg11 -> undef203, arg12 -> undef204, arg13 -> undef205, arg14 -> undef206, arg15 -> undef207, arg16 -> undef208, arg17 -> undef209, arg18 -> undef210, arg19 -> undef211, arg20 -> undef212, arg21 -> undef213, arg22 -> undef214, arg23 -> undef215}>
<l8, l8, (arg2 > 0) /\ (undef286 > ~(1)) /\ (arg16 > 0) /\ (arg16 < undef286) /\ (arg4 > 0) /\ (arg3 > 0) /\ (arg7 > 0) /\ (arg6 > 0) /\ (arg5 > 0) /\ (arg14 > 0) /\ (undef287 > ~(1)) /\ (arg9 > 0) /\ (arg12 > 0) /\ (arg10 > 0) /\ (arg15 > 0) /\ (arg13 > 0) /\ (arg11 > 0) /\ (arg8 > 0) /\ (arg23 > ~(1)) /\ (arg17 > ~(1)) /\ (arg1 > 11) /\ (undef263 > 11) /\ ((arg17 + 5) <= arg1) /\ ((arg18 + 9) <= arg1) /\ ((arg19 + 9) <= arg1) /\ ((arg20 + 9) <= arg1) /\ ((arg21 + 11) <= arg1) /\ ((arg23 + 3) <= arg1) /\ ((arg22 + 11) <= arg1), par{arg1 -> undef263, arg2 -> (arg2 - 1), arg5 -> undef267, arg6 -> undef268, arg7 -> undef269, arg8 -> undef270, arg9 -> undef271, arg10 -> undef272, arg11 -> undef273, arg12 -> undef274, arg13 -> undef275, arg14 -> undef276, arg15 -> undef277, arg16 -> (arg16 + 1), arg17 -> (arg17 + 1), arg18 -> undef280, arg19 -> undef281, arg20 -> undef282, arg21 -> undef283, arg22 -> undef284, arg23 -> (arg23 + 1)}>

Fresh variables:
undef2, undef6, undef10, undef11, undef12, undef16, undef19, undef20, undef22, undef23, undef24, undef27, undef29, undef30, undef32, undef33, undef34, undef35, undef36, undef37, undef38, undef39, undef40, undef41, undef42, undef43, undef44, undef45, undef46, undef47, undef48, undef49, undef51, undef52, undef53, undef54, undef55, undef56, undef57, undef58, undef59, undef60, undef61, undef62, undef63, undef64, undef65, undef66, undef67, undef68, undef69, undef70, undef72, undef74, undef75, undef76, undef77, undef78, undef79, undef80, undef81, undef82, undef83, undef84, undef85, undef86, 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, undef115, undef116, undef117, undef118, undef119, undef123, undef124, undef125, undef126, undef127, undef128, undef129, undef130, undef131, undef132, undef133, undef134, undef135, undef136, undef137, undef138, undef139, undef140, undef141, undef142, undef143, undef145, undef147, undef148, undef149, undef150, undef151, undef152, undef153, undef154, undef155, undef156, undef157, undef158, undef159, undef160, undef161, undef162, undef163, undef164, undef165, undef166, undef167, undef168, undef171, undef172, undef173, undef174, undef175, undef176, undef177, undef178, undef179, undef180, undef181, undef182, undef183, undef184, undef185, undef186, undef187, undef188, undef189, undef190, undef191, undef192, undef196, undef197, undef198, undef199, undef200, undef201, undef202, undef203, undef204, undef205, undef206, undef207, undef208, undef209, undef210, undef211, undef212, undef213, undef214, undef215, undef216, undef217, undef218, undef219, undef220, undef224, undef225, undef226, undef227, undef228, undef229, undef230, undef231, undef232, undef233, undef234, undef235, undef236, undef237, undef238, undef239, undef240, undef257, undef258, undef259, undef260, undef261, undef263, undef267, undef268, undef269, undef270, undef271, undef272, undef273, undef274, undef275, undef276, undef277, undef280, undef281, undef282, undef283, undef284, undef286, undef287, undef288, undef289, undef290, undef291, undef292, undef293, undef294, undef295, undef296, undef297, undef298, undef299, undef300, undef301, undef302, undef303, undef304, undef305, undef306, undef307, undef308, undef309, undef310, 

Undef variables:
undef2, undef6, undef10, undef11, undef12, undef16, undef19, undef20, undef22, undef23, undef24, undef27, undef29, undef30, undef32, undef33, undef34, undef35, undef36, undef37, undef38, undef39, undef40, undef41, undef42, undef43, undef44, undef45, undef46, undef47, undef48, undef49, undef51, undef52, undef53, undef54, undef55, undef56, undef57, undef58, undef59, undef60, undef61, undef62, undef63, undef64, undef65, undef66, undef67, undef68, undef69, undef70, undef72, undef74, undef75, undef76, undef77, undef78, undef79, undef80, undef81, undef82, undef83, undef84, undef85, undef86, 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, undef115, undef116, undef117, undef118, undef119, undef123, undef124, undef125, undef126, undef127, undef128, undef129, undef130, undef131, undef132, undef133, undef134, undef135, undef136, undef137, undef138, undef139, undef140, undef141, undef142, undef143, undef145, undef147, undef148, undef149, undef150, undef151, undef152, undef153, undef154, undef155, undef156, undef157, undef158, undef159, undef160, undef161, undef162, undef163, undef164, undef165, undef166, undef167, undef168, undef171, undef172, undef173, undef174, undef175, undef176, undef177, undef178, undef179, undef180, undef181, undef182, undef183, undef184, undef185, undef186, undef187, undef188, undef189, undef190, undef191, undef192, undef196, undef197, undef198, undef199, undef200, undef201, undef202, undef203, undef204, undef205, undef206, undef207, undef208, undef209, undef210, undef211, undef212, undef213, undef214, undef215, undef216, undef217, undef218, undef219, undef220, undef224, undef225, undef226, undef227, undef228, undef229, undef230, undef231, undef232, undef233, undef234, undef235, undef236, undef237, undef238, undef239, undef240, undef257, undef258, undef259, undef260, undef261, undef263, undef267, undef268, undef269, undef270, undef271, undef272, undef273, undef274, undef275, undef276, undef277, undef280, undef281, undef282, undef283, undef284, undef286, undef287, undef288, undef289, undef290, undef291, undef292, undef293, undef294, undef295, undef296, undef297, undef298, undef299, undef300, undef301, undef302, undef303, undef304, undef305, undef306, undef307, undef308, undef309, undef310, 

Abstraction variables:

Exit nodes:

Accepting locations:

Asserts:

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

Init Location: 0
Graph 0:
Transitions:
Variables:

Graph 1:
Transitions:
<l8, l8, 9 + arg18 <= arg1 /\ 9 + arg19 <= arg1 /\ 9 + arg20 <= arg1 /\ 5 + arg17 <= arg1 /\ 3 + arg23 <= arg1 /\ 0 <= arg17 /\ 0 <= arg23 /\ 0 <= undef286 /\ 0 <= undef287 /\ 1 <= arg2 /\ 1 <= arg3 /\ 1 <= arg4 /\ 1 <= arg5 /\ 1 <= arg6 /\ 1 <= arg7 /\ 1 <= arg8 /\ 1 <= arg9 /\ 1 <= arg10 /\ 1 <= arg11 /\ 1 <= arg12 /\ 1 <= arg13 /\ 1 <= arg14 /\ 1 <= arg15 /\ 1 + arg16 <= undef286 /\ 1 <= arg16 /\ 11 + arg21 <= arg1 /\ 11 + arg22 <= arg1 /\ 12 <= arg1 /\ 12 <= undef263, {arg1 -> undef263, arg2 -> -1 + arg2, arg5 -> undef267, arg6 -> undef268, arg7 -> undef269, arg8 -> undef270, arg9 -> undef271, arg10 -> undef272, arg11 -> undef273, arg12 -> undef274, arg13 -> undef275, arg14 -> undef276, arg15 -> undef277, arg16 -> 1 + arg16, arg17 -> 1 + arg17, arg18 -> undef280, arg19 -> undef281, arg20 -> undef282, arg21 -> undef283, arg22 -> undef284, arg23 -> 1 + arg23, rest remain the same}>
Variables:
arg1, arg2, arg3, arg4, arg5, arg6, arg7, arg8, arg9, arg10, arg11, arg12, arg13, arg14, arg15, arg16, arg17, arg18, arg19, arg20, arg21, arg22, arg23

Graph 2:
Transitions:
<l7, l7, arg1 <= arg2 /\ 0 <= arg3 /\ 1 + undef192 <= arg3 /\ 1 + undef192 <= undef171 /\ 1 <= undef192, {arg1 -> 1 + arg1, arg3 -> undef171, arg4 -> undef172, arg5 -> undef173, arg6 -> undef174, arg7 -> undef175, arg8 -> undef176, arg9 -> undef177, arg10 -> undef178, arg11 -> undef179, arg12 -> undef180, arg13 -> undef181, arg14 -> undef182, arg15 -> undef183, arg16 -> undef184, arg17 -> undef185, arg18 -> undef186, arg19 -> undef187, arg20 -> undef188, arg21 -> undef189, arg22 -> undef190, arg23 -> undef191, rest remain the same}>
<l7, l7, arg1 <= arg2 /\ 0 <= arg3 /\ 1 + undef216 <= arg3, {arg1 -> 1 + arg1, arg3 -> 1, arg4 -> undef196, arg5 -> undef197, arg6 -> undef198, arg7 -> undef199, arg8 -> undef200, arg9 -> undef201, arg10 -> undef202, arg11 -> undef203, arg12 -> undef204, arg13 -> undef205, arg14 -> undef206, arg15 -> undef207, arg16 -> undef208, arg17 -> undef209, arg18 -> undef210, arg19 -> undef211, arg20 -> undef212, arg21 -> undef213, arg22 -> undef214, arg23 -> undef215, rest remain the same}>
Variables:
arg1, arg2, arg3, arg4, arg5, arg6, arg7, arg8, arg9, arg10, arg11, arg12, arg13, arg14, arg15, arg16, arg17, arg18, arg19, arg20, arg21, arg22, arg23

Graph 3:
Transitions:
<l6, l6, 0 <= arg3 /\ 1 + arg2 <= arg1 /\ 1 + undef119 <= arg3 /\ 1 + undef119 <= undef98 /\ 1 <= undef119, {arg1 -> -1 + arg1, arg3 -> undef98, arg4 -> undef99, arg5 -> undef100, arg6 -> undef101, arg7 -> undef102, arg8 -> undef103, arg9 -> undef104, arg10 -> undef105, arg11 -> undef106, arg12 -> undef107, arg13 -> undef108, arg14 -> undef109, arg15 -> undef110, arg16 -> undef111, arg17 -> undef112, arg18 -> undef113, arg19 -> undef114, arg20 -> undef115, arg21 -> undef116, arg22 -> undef117, arg23 -> undef118, rest remain the same}>
<l6, l6, 0 <= arg3 /\ 1 + arg2 <= arg1 /\ 1 + undef143 <= arg3, {arg1 -> -1 + arg1, arg3 -> 1, arg4 -> undef123, arg5 -> undef124, arg6 -> undef125, arg7 -> undef126, arg8 -> undef127, arg9 -> undef128, arg10 -> undef129, arg11 -> undef130, arg12 -> undef131, arg13 -> undef132, arg14 -> undef133, arg15 -> undef134, arg16 -> undef135, arg17 -> undef136, arg18 -> undef137, arg19 -> undef138, arg20 -> undef139, arg21 -> undef140, arg22 -> undef141, arg23 -> undef142, rest remain the same}>
Variables:
arg1, arg2, arg3, arg4, arg5, arg6, arg7, arg8, arg9, arg10, arg11, arg12, arg13, arg14, arg15, arg16, arg17, arg18, arg19, arg20, arg21, arg22, arg23

Precedence: 
Graph 0

Graph 1
<l0, l8, 9 + undef19 <= undef2 /\ 9 + undef20 <= undef2 /\ 0 <= undef217 /\ 1 <= undef288 /\ 1 <= undef289 /\ undef218 <= 7 + undef288 /\ 10 <= undef218 /\ 12 <= undef2 /\ 12 <= undef240, {arg1 -> undef240, arg2 -> undef217, arg3 -> 0, arg4 -> undef220, arg5 -> undef11, arg6 -> undef10, arg7 -> 0, arg8 -> undef6, arg9 -> 0, arg10 -> 0, arg11 -> 0, arg12 -> undef12, arg13 -> undef219, arg14 -> undef219, arg15 -> undef220, arg16 -> 1, arg17 -> 0, arg18 -> undef257, arg19 -> undef258, arg20 -> undef259, arg21 -> undef260, arg22 -> undef261, arg23 -> 0, rest remain the same}>

Graph 2
<l0, l7, 5 + undef51 <= undef47 /\ 3 + undef54 <= undef47 /\ 0 <= undef70 /\ 0 <= undef145 /\ 7 <= undef47 /\ 7 + undef52 <= undef47 /\ 7 + undef53 <= undef47 /\ 1 + undef145 <= undef51 /\ 1 + undef145 <= undef168 /\ 1 + undef167 <= undef289 /\ 1 <= undef167 /\ 1 <= undef288 /\ 1 <= undef289, {arg1 -> 0, arg2 -> undef145, arg3 -> undef48, arg4 -> undef147, arg5 -> undef148, arg6 -> undef149, arg7 -> undef150, arg8 -> undef151, arg9 -> undef152, arg10 -> undef153, arg11 -> undef154, arg12 -> undef155, arg13 -> undef156, arg14 -> undef157, arg15 -> undef158, arg16 -> undef159, arg17 -> undef160, arg18 -> undef161, arg19 -> undef162, arg20 -> undef163, arg21 -> undef164, arg22 -> undef165, arg23 -> undef166, rest remain the same}>

Graph 3
<l0, l6, 5 + undef51 <= undef47 /\ 3 + undef54 <= undef47 /\ 0 <= undef70 /\ 0 <= undef72 /\ undef95 <= undef72 /\ 7 <= undef47 /\ 7 + undef52 <= undef47 /\ 7 + undef53 <= undef47 /\ 1 + undef72 <= undef51 /\ 1 + undef94 <= undef289 /\ 1 <= undef94 /\ 1 <= undef288 /\ 1 <= undef289, {arg1 -> undef51, arg2 -> undef72, arg3 -> undef49, arg4 -> undef74, arg5 -> undef75, arg6 -> undef76, arg7 -> undef77, arg8 -> undef78, arg9 -> undef79, arg10 -> undef80, arg11 -> undef81, arg12 -> undef82, arg13 -> undef83, arg14 -> undef84, arg15 -> undef85, arg16 -> undef86, arg17 -> undef87, arg18 -> undef88, arg19 -> undef89, arg20 -> undef90, arg21 -> undef91, arg22 -> undef92, arg23 -> undef93, rest remain the same}>

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

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

Proving termination of subgraph 0
Proving termination of subgraph 1
Checking unfeasibility...
Time used: 0.010426
Some transition disabled by a set of invariant(s):
Invariant at l8: arg3 <= 0

Strengthening and disabling transitions...
> It's unfeasible. Removing transition: 
<l8, l8, 9 + arg18 <= arg1 /\ 9 + arg19 <= arg1 /\ 9 + arg20 <= arg1 /\ 5 + arg17 <= arg1 /\ 3 + arg23 <= arg1 /\ 0 <= arg17 /\ 0 <= arg23 /\ 0 <= undef286 /\ 0 <= undef287 /\ 1 <= arg2 /\ 1 <= arg3 /\ 1 <= arg4 /\ 1 <= arg5 /\ 1 <= arg6 /\ 1 <= arg7 /\ 1 <= arg8 /\ 1 <= arg9 /\ 1 <= arg10 /\ 1 <= arg11 /\ 1 <= arg12 /\ 1 <= arg13 /\ 1 <= arg14 /\ 1 <= arg15 /\ 1 + arg16 <= undef286 /\ 1 <= arg16 /\ 11 + arg21 <= arg1 /\ 11 + arg22 <= arg1 /\ 12 <= arg1 /\ 12 <= undef263, {arg1 -> undef263, arg2 -> -1 + arg2, arg5 -> undef267, arg6 -> undef268, arg7 -> undef269, arg8 -> undef270, arg9 -> undef271, arg10 -> undef272, arg11 -> undef273, arg12 -> undef274, arg13 -> undef275, arg14 -> undef276, arg15 -> undef277, arg16 -> 1 + arg16, arg17 -> 1 + arg17, arg18 -> undef280, arg19 -> undef281, arg20 -> undef282, arg21 -> undef283, arg22 -> undef284, arg23 -> 1 + arg23, rest remain the same}>
Checking unfeasibility...
Time used: 2.3e-05

Analyzing SCC {l8}...
No cycles found.

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

Checking conditional termination of SCC {l7}...

LOG: CALL solveLinear

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

Checking conditional termination of SCC {l6}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002830s
Ranking function: -1 + arg1 - arg2
New Graphs: 
Program Terminates