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 -> undef7, arg7 -> undef7, arg8 -> 0, arg9 -> 0, arg10 -> 0, arg11 -> undef11, arg12 -> undef12, arg13 -> undef13, arg14 -> undef14, arg15 -> arg3, arg16 -> arg3, arg17 -> arg4, arg18 -> undef18, arg19 -> arg5, arg20 -> arg6, arg21 -> undef21, arg22 -> undef22, arg23 -> arg7, arg24 -> undef24, arg25 -> undef25}>
<l3, l4, (undef51 > ~(1)) /\ (arg2 > 0) /\ (arg1 > 0) /\ (undef26 > 6), par{arg1 -> undef26, arg2 -> undef27, arg3 -> undef28, arg4 -> arg2, arg5 -> undef30, arg6 -> undef31, arg7 -> undef32, arg8 -> undef33, arg9 -> undef34, arg10 -> undef35, arg11 -> undef36, arg12 -> undef37, arg13 -> undef38, arg14 -> undef39, arg15 -> undef40, arg16 -> undef41, arg17 -> undef42, arg18 -> undef43, arg19 -> undef44, arg20 -> undef45, arg21 -> undef46, arg22 -> undef47, arg23 -> undef48, arg24 -> undef49, arg25 -> undef50}>
<l5, l4, (arg1 > 0) /\ (arg2 > 6) /\ (undef52 > 6) /\ ((arg6 + 5) <= arg2) /\ ((arg7 + 7) <= arg2) /\ ((arg9 + 3) <= arg2) /\ ((arg8 + 7) <= arg2), par{arg1 -> undef52, arg2 -> arg3, arg3 -> arg4, arg4 -> undef55, arg5 -> arg6, arg6 -> undef57, arg7 -> undef58, arg8 -> arg9, arg9 -> undef60, arg10 -> undef61, arg11 -> undef62, arg12 -> undef63, arg13 -> undef64, arg14 -> undef65, arg15 -> undef66, arg16 -> undef67, arg17 -> undef68, arg18 -> undef69, arg19 -> undef70, arg20 -> undef71, arg21 -> undef72, arg22 -> undef73, arg23 -> undef74, arg24 -> undef75, arg25 -> undef76}>
<l4, l6, (undef102 > ~(1)) /\ ((undef102 + 1) < arg4) /\ (undef78 > ~(1)) /\ (undef103 > ~(1)) /\ (undef104 <= undef78) /\ (undef78 < arg5) /\ (arg1 > 6) /\ ((arg5 + 5) <= arg1) /\ ((arg6 + 7) <= arg1) /\ ((arg8 + 3) <= arg1) /\ ((arg7 + 7) <= arg1), par{arg1 -> arg5, arg2 -> undef78, arg4 -> undef80, arg5 -> undef81, arg6 -> undef82, arg7 -> undef83, arg8 -> undef84, arg9 -> undef85, arg10 -> undef86, arg11 -> undef87, arg12 -> undef88, arg13 -> undef89, arg14 -> undef90, arg15 -> undef91, arg16 -> undef92, arg17 -> undef93, arg18 -> undef94, arg19 -> undef95, arg20 -> undef96, arg21 -> undef97, arg22 -> undef98, arg23 -> undef99, arg24 -> undef100, arg25 -> undef101}>
<l6, l6, (arg3 > ~(1)) /\ (undef130 > 0) /\ (undef130 < arg3) /\ (arg2 < arg1) /\ (undef130 < undef107), par{arg1 -> (arg1 - 1), arg3 -> undef107, arg4 -> undef108, arg5 -> undef109, arg6 -> undef110, arg7 -> undef111, arg8 -> undef112, arg9 -> undef113, arg10 -> undef114, arg11 -> undef115, arg12 -> undef116, arg13 -> undef117, arg14 -> undef118, arg15 -> undef119, arg16 -> undef120, arg17 -> undef121, arg18 -> undef122, arg19 -> undef123, arg20 -> undef124, arg21 -> undef125, arg22 -> undef126, arg23 -> undef127, arg24 -> undef128, arg25 -> undef129}>
<l6, l6, (arg2 < arg1) /\ (undef156 < arg3) /\ (arg3 > ~(1)), par{arg1 -> (arg1 - 1), arg3 -> 1, arg4 -> undef134, arg5 -> undef135, arg6 -> undef136, arg7 -> undef137, arg8 -> undef138, arg9 -> undef139, arg10 -> undef140, arg11 -> undef141, arg12 -> undef142, arg13 -> undef143, arg14 -> undef144, arg15 -> undef145, arg16 -> undef146, arg17 -> undef147, arg18 -> undef148, arg19 -> undef149, arg20 -> undef150, arg21 -> undef151, arg22 -> undef152, arg23 -> undef153, arg24 -> undef154, arg25 -> undef155}>
<l4, l7, (undef182 > ~(1)) /\ ((undef182 + 1) < arg4) /\ (undef158 > ~(1)) /\ (undef183 > ~(1)) /\ (undef184 > undef158) /\ (undef158 < arg5) /\ (arg1 > 6) /\ ((arg5 + 5) <= arg1) /\ ((arg6 + 7) <= arg1) /\ ((arg8 + 3) <= arg1) /\ ((arg7 + 7) <= arg1), par{arg1 -> 0, arg2 -> undef158, arg3 -> arg2, arg4 -> undef160, arg5 -> undef161, arg6 -> undef162, arg7 -> undef163, arg8 -> undef164, arg9 -> undef165, arg10 -> undef166, arg11 -> undef167, arg12 -> undef168, arg13 -> undef169, arg14 -> undef170, arg15 -> undef171, arg16 -> undef172, arg17 -> undef173, arg18 -> undef174, arg19 -> undef175, arg20 -> undef176, arg21 -> undef177, arg22 -> undef178, arg23 -> undef179, arg24 -> undef180, arg25 -> undef181}>
<l7, l7, (arg3 > ~(1)) /\ (undef210 > 0) /\ (undef210 < arg3) /\ (arg2 >= arg1) /\ (undef210 < undef187), par{arg1 -> (arg1 + 1), arg3 -> undef187, arg4 -> undef188, arg5 -> undef189, arg6 -> undef190, arg7 -> undef191, arg8 -> undef192, arg9 -> undef193, arg10 -> undef194, arg11 -> undef195, arg12 -> undef196, arg13 -> undef197, arg14 -> undef198, arg15 -> undef199, arg16 -> undef200, arg17 -> undef201, arg18 -> undef202, arg19 -> undef203, arg20 -> undef204, arg21 -> undef205, arg22 -> undef206, arg23 -> undef207, arg24 -> undef208, arg25 -> undef209}>
<l7, l7, (arg2 >= arg1) /\ (undef236 < arg3) /\ (arg3 > ~(1)), par{arg1 -> (arg1 + 1), arg3 -> 1, arg4 -> undef214, arg5 -> undef215, arg6 -> undef216, arg7 -> undef217, arg8 -> undef218, arg9 -> undef219, arg10 -> undef220, arg11 -> undef221, arg12 -> undef222, arg13 -> undef223, arg14 -> undef224, arg15 -> undef225, arg16 -> undef226, arg17 -> undef227, arg18 -> undef228, arg19 -> undef229, arg20 -> undef230, arg21 -> undef231, arg22 -> undef232, arg23 -> undef233, arg24 -> undef234, arg25 -> undef235}>
<l3, l1, (undef237 > ~(1)) /\ (arg2 > 0) /\ ((undef238 - 7) <= arg1) /\ (arg1 > 0) /\ (undef238 > 7), par{arg1 -> undef237, arg2 -> undef238, arg3 -> undef239, arg4 -> undef240, arg5 -> 1, arg6 -> 0, arg7 -> 0, arg8 -> undef244, arg9 -> undef245, arg10 -> undef246, arg11 -> undef247, arg12 -> undef248, arg13 -> undef249, arg14 -> undef250, arg15 -> undef251, arg16 -> undef252, arg17 -> undef253, arg18 -> undef254, arg19 -> undef255, arg20 -> undef256, arg21 -> undef257, arg22 -> undef258, arg23 -> undef259, arg24 -> undef260, arg25 -> undef261}>
<l2, l8, (arg2 > 11) /\ (undef262 > 11) /\ (arg2 >= (arg20 + 5)) /\ (arg2 >= (arg21 + 9)) /\ (arg2 >= (arg22 + 9)) /\ (arg2 >= (arg23 + 3)), par{arg1 -> undef262, arg2 -> arg1, arg3 -> arg13, arg4 -> arg11, arg5 -> arg7, arg6 -> arg12, arg7 -> arg6, arg8 -> undef269, arg9 -> arg3, arg10 -> arg14, arg11 -> arg5, arg12 -> 0, arg13 -> arg4, arg14 -> arg8, arg15 -> arg9, arg16 -> arg10, arg17 -> arg15, arg18 -> arg16, arg19 -> arg17, arg20 -> arg19, arg21 -> arg20, arg22 -> undef283, arg23 -> undef284, arg24 -> undef285, arg25 -> arg23}>
<l8, l8, (arg2 > 0) /\ (undef312 > ~(1)) /\ (arg6 > 0) /\ (arg3 > 0) /\ (arg20 > ~(1)) /\ (arg20 < undef312) /\ (arg10 > 0) /\ (arg4 > 0) /\ (arg13 > 0) /\ (arg11 > 0) /\ (arg12 > 0) /\ (undef313 > ~(1)) /\ (arg9 > 0) /\ (arg5 > 0) /\ (arg18 > 0) /\ (arg14 > 0) /\ (arg19 > 0) /\ (arg17 > 0) /\ (arg15 > 0) /\ (arg16 > 0) /\ (arg25 > ~(1)) /\ (arg21 > ~(1)) /\ (arg1 > 9) /\ (undef287 > 9) /\ ((arg21 + 5) <= arg1) /\ ((arg22 + 9) <= arg1) /\ ((arg23 + 9) <= arg1) /\ ((arg25 + 3) <= arg1) /\ ((arg24 + 9) <= arg1), par{arg1 -> undef287, arg2 -> (arg2 - 1), arg4 -> undef290, arg5 -> undef291, arg9 -> undef295, arg11 -> undef297, arg13 -> undef299, arg14 -> undef300, arg15 -> undef301, arg16 -> undef302, arg17 -> undef303, arg18 -> undef304, arg19 -> undef305, arg20 -> (arg20 + 1), arg21 -> (arg21 + 1), arg22 -> undef308, arg23 -> undef309, arg24 -> undef310, arg25 -> (arg25 + 1)}>
<l8, l8, (arg2 > 0) /\ (undef339 > ~(1)) /\ (arg6 > 0) /\ (arg3 > 0) /\ (arg20 > ~(1)) /\ (arg20 < undef339) /\ (arg10 > 0) /\ (arg12 > 0) /\ (undef340 > ~(1)) /\ (arg18 > 0) /\ (arg19 > 0) /\ (arg17 > 0) /\ (arg8 > 0) /\ (arg25 > ~(1)) /\ (arg21 > ~(1)) /\ (arg1 > 11) /\ (undef314 > 13) /\ ((arg21 + 5) <= arg1) /\ ((arg22 + 9) <= arg1) /\ ((arg23 + 9) <= arg1) /\ ((arg24 + 9) <= arg1) /\ ((arg25 + 3) <= arg1) /\ (arg8 = arg9) /\ (arg10 = arg11) /\ (arg12 = arg13) /\ (arg7 = arg16), par{arg1 -> undef314, arg2 -> (arg2 - 1), arg3 -> 0, arg4 -> 1, arg5 -> 1, arg6 -> undef319, arg7 -> undef320, arg9 -> undef322, arg11 -> undef324, arg13 -> 0, arg14 -> undef327, arg15 -> 2, arg16 -> undef329, arg17 -> undef330, arg18 -> undef331, arg19 -> undef332, arg20 -> (arg20 + 1), arg21 -> (arg21 + 1), arg22 -> undef335, arg23 -> undef336, arg24 -> undef337, arg25 -> (arg25 + 1)}>
<l9, l3, true, par{arg1 -> undef341, arg2 -> undef342, arg3 -> undef343, arg4 -> undef344, arg5 -> undef345, arg6 -> undef346, arg7 -> undef347, arg8 -> undef348, arg9 -> undef349, arg10 -> undef350, arg11 -> undef351, arg12 -> undef352, arg13 -> undef353, arg14 -> undef354, arg15 -> undef355, arg16 -> undef356, arg17 -> undef357, arg18 -> undef358, arg19 -> undef359, arg20 -> undef360, arg21 -> undef361, arg22 -> undef362, arg23 -> undef363, arg24 -> undef364, arg25 -> undef365}>

Fresh variables:
undef2, undef7, undef11, undef12, undef13, undef14, undef18, undef21, undef22, undef24, undef25, undef26, undef27, undef28, undef30, undef31, undef32, undef33, undef34, undef35, undef36, undef37, undef38, undef39, undef40, undef41, undef42, undef43, undef44, undef45, undef46, undef47, undef48, undef49, undef50, undef51, undef52, undef55, undef57, undef58, undef60, undef61, undef62, undef63, undef64, undef65, undef66, undef67, undef68, undef69, undef70, undef71, undef72, undef73, undef74, undef75, undef76, undef78, undef80, undef81, undef82, undef83, undef84, undef85, undef86, undef87, undef88, undef89, undef90, undef91, undef92, undef93, undef94, undef95, undef96, undef97, undef98, undef99, undef100, undef101, undef102, undef103, undef104, undef107, undef108, undef109, undef110, undef111, undef112, undef113, undef114, undef115, undef116, undef117, undef118, undef119, undef120, undef121, undef122, undef123, undef124, undef125, undef126, undef127, undef128, undef129, undef130, undef134, undef135, undef136, undef137, undef138, undef139, undef140, undef141, undef142, undef143, undef144, undef145, undef146, undef147, undef148, undef149, undef150, undef151, undef152, undef153, undef154, undef155, undef156, undef158, undef160, undef161, undef162, undef163, undef164, undef165, undef166, undef167, undef168, undef169, undef170, undef171, undef172, undef173, undef174, undef175, undef176, undef177, undef178, undef179, undef180, undef181, undef182, undef183, undef184, undef187, undef188, undef189, undef190, undef191, undef192, undef193, undef194, undef195, undef196, undef197, undef198, undef199, undef200, undef201, undef202, undef203, undef204, undef205, undef206, undef207, undef208, undef209, undef210, undef214, undef215, undef216, undef217, undef218, undef219, undef220, undef221, undef222, undef223, undef224, undef225, undef226, undef227, undef228, undef229, undef230, undef231, undef232, undef233, undef234, undef235, undef236, undef237, undef238, undef239, undef240, undef244, undef245, undef246, undef247, undef248, undef249, undef250, undef251, undef252, undef253, undef254, undef255, undef256, undef257, undef258, undef259, undef260, undef261, undef262, undef269, undef283, undef284, undef285, undef287, undef290, undef291, undef295, undef297, undef299, undef300, undef301, undef302, undef303, undef304, undef305, undef308, undef309, undef310, undef312, undef313, undef314, undef319, undef320, undef322, undef324, undef327, undef329, undef330, undef331, undef332, undef335, undef336, undef337, undef339, undef340, undef341, undef342, undef343, undef344, undef345, undef346, undef347, undef348, undef349, undef350, undef351, undef352, undef353, undef354, undef355, undef356, undef357, undef358, undef359, undef360, undef361, undef362, undef363, undef364, undef365, 

Undef variables:
undef2, undef7, undef11, undef12, undef13, undef14, undef18, undef21, undef22, undef24, undef25, undef26, undef27, undef28, undef30, undef31, undef32, undef33, undef34, undef35, undef36, undef37, undef38, undef39, undef40, undef41, undef42, undef43, undef44, undef45, undef46, undef47, undef48, undef49, undef50, undef51, undef52, undef55, undef57, undef58, undef60, undef61, undef62, undef63, undef64, undef65, undef66, undef67, undef68, undef69, undef70, undef71, undef72, undef73, undef74, undef75, undef76, undef78, undef80, undef81, undef82, undef83, undef84, undef85, undef86, undef87, undef88, undef89, undef90, undef91, undef92, undef93, undef94, undef95, undef96, undef97, undef98, undef99, undef100, undef101, undef102, undef103, undef104, undef107, undef108, undef109, undef110, undef111, undef112, undef113, undef114, undef115, undef116, undef117, undef118, undef119, undef120, undef121, undef122, undef123, undef124, undef125, undef126, undef127, undef128, undef129, undef130, undef134, undef135, undef136, undef137, undef138, undef139, undef140, undef141, undef142, undef143, undef144, undef145, undef146, undef147, undef148, undef149, undef150, undef151, undef152, undef153, undef154, undef155, undef156, undef158, undef160, undef161, undef162, undef163, undef164, undef165, undef166, undef167, undef168, undef169, undef170, undef171, undef172, undef173, undef174, undef175, undef176, undef177, undef178, undef179, undef180, undef181, undef182, undef183, undef184, undef187, undef188, undef189, undef190, undef191, undef192, undef193, undef194, undef195, undef196, undef197, undef198, undef199, undef200, undef201, undef202, undef203, undef204, undef205, undef206, undef207, undef208, undef209, undef210, undef214, undef215, undef216, undef217, undef218, undef219, undef220, undef221, undef222, undef223, undef224, undef225, undef226, undef227, undef228, undef229, undef230, undef231, undef232, undef233, undef234, undef235, undef236, undef237, undef238, undef239, undef240, undef244, undef245, undef246, undef247, undef248, undef249, undef250, undef251, undef252, undef253, undef254, undef255, undef256, undef257, undef258, undef259, undef260, undef261, undef262, undef269, undef283, undef284, undef285, undef287, undef290, undef291, undef295, undef297, undef299, undef300, undef301, undef302, undef303, undef304, undef305, undef308, undef309, undef310, undef312, undef313, undef314, undef319, undef320, undef322, undef324, undef327, undef329, undef330, undef331, undef332, undef335, undef336, undef337, undef339, undef340, undef341, undef342, undef343, undef344, undef345, undef346, undef347, undef348, undef349, undef350, undef351, undef352, undef353, undef354, undef355, undef356, undef357, undef358, undef359, undef360, undef361, undef362, undef363, undef364, undef365, 

Abstraction variables:

Exit nodes:

Accepting locations:

Asserts:

Preprocessed LLVMGraph
Init Location: 0
Transitions:
<l0, l6, (undef51 > ~(1)) /\ (undef342 > 0) /\ (undef341 > 0) /\ (undef26 > 6) /\ (undef102 > ~(1)) /\ ((undef102 + 1) < undef342) /\ (undef78 > ~(1)) /\ (undef103 > ~(1)) /\ (undef104 <= undef78) /\ (undef78 < undef30) /\ (undef26 > 6) /\ ((undef30 + 5) <= undef26) /\ ((undef31 + 7) <= undef26) /\ ((undef33 + 3) <= undef26) /\ ((undef32 + 7) <= undef26), par{arg1 -> undef30, arg2 -> undef78, arg3 -> undef28, arg4 -> undef80, arg5 -> undef81, arg6 -> undef82, arg7 -> undef83, arg8 -> undef84, arg9 -> undef85, arg10 -> undef86, arg11 -> undef87, arg12 -> undef88, arg13 -> undef89, arg14 -> undef90, arg15 -> undef91, arg16 -> undef92, arg17 -> undef93, arg18 -> undef94, arg19 -> undef95, arg20 -> undef96, arg21 -> undef97, arg22 -> undef98, arg23 -> undef99, arg24 -> undef100, arg25 -> undef101}>
<l0, l7, (undef51 > ~(1)) /\ (undef342 > 0) /\ (undef341 > 0) /\ (undef26 > 6) /\ (undef182 > ~(1)) /\ ((undef182 + 1) < undef342) /\ (undef158 > ~(1)) /\ (undef183 > ~(1)) /\ (undef184 > undef158) /\ (undef158 < undef30) /\ (undef26 > 6) /\ ((undef30 + 5) <= undef26) /\ ((undef31 + 7) <= undef26) /\ ((undef33 + 3) <= undef26) /\ ((undef32 + 7) <= undef26), par{arg1 -> 0, arg2 -> undef158, arg3 -> undef27, arg4 -> undef160, arg5 -> undef161, arg6 -> undef162, arg7 -> undef163, arg8 -> undef164, arg9 -> undef165, arg10 -> undef166, arg11 -> undef167, arg12 -> undef168, arg13 -> undef169, arg14 -> undef170, arg15 -> undef171, arg16 -> undef172, arg17 -> undef173, arg18 -> undef174, arg19 -> undef175, arg20 -> undef176, arg21 -> undef177, arg22 -> undef178, arg23 -> undef179, arg24 -> undef180, arg25 -> undef181}>
<l0, l8, (undef237 > ~(1)) /\ (undef342 > 0) /\ ((undef238 - 7) <= undef341) /\ (undef341 > 0) /\ (undef238 > 7) /\ (undef238 > 9) /\ (undef2 > 9) /\ ((0 + 5) <= undef238) /\ ((0 + 3) <= undef238) /\ (undef2 > 11) /\ (undef262 > 11) /\ (undef2 >= (0 + 5)) /\ (undef2 >= (undef21 + 9)) /\ (undef2 >= (undef22 + 9)) /\ (undef2 >= (0 + 3)), par{arg1 -> undef262, arg2 -> undef237, arg3 -> undef13, arg4 -> undef11, arg5 -> undef7, arg6 -> undef12, arg7 -> undef7, arg8 -> undef269, arg9 -> 0, arg10 -> undef14, arg11 -> undef240, arg12 -> 0, arg13 -> 0, arg14 -> 0, arg15 -> 0, arg16 -> 0, arg17 -> undef239, arg18 -> undef239, arg19 -> undef240, arg20 -> 1, arg21 -> 0, arg22 -> undef283, arg23 -> undef284, arg24 -> undef285, arg25 -> 0}>
<l6, l6, (arg3 > ~(1)) /\ (undef130 > 0) /\ (undef130 < arg3) /\ (arg2 < arg1) /\ (undef130 < undef107), par{arg1 -> (arg1 - 1), arg3 -> undef107, arg4 -> undef108, arg5 -> undef109, arg6 -> undef110, arg7 -> undef111, arg8 -> undef112, arg9 -> undef113, arg10 -> undef114, arg11 -> undef115, arg12 -> undef116, arg13 -> undef117, arg14 -> undef118, arg15 -> undef119, arg16 -> undef120, arg17 -> undef121, arg18 -> undef122, arg19 -> undef123, arg20 -> undef124, arg21 -> undef125, arg22 -> undef126, arg23 -> undef127, arg24 -> undef128, arg25 -> undef129}>
<l6, l6, (arg2 < arg1) /\ (undef156 < arg3) /\ (arg3 > ~(1)), par{arg1 -> (arg1 - 1), arg3 -> 1, arg4 -> undef134, arg5 -> undef135, arg6 -> undef136, arg7 -> undef137, arg8 -> undef138, arg9 -> undef139, arg10 -> undef140, arg11 -> undef141, arg12 -> undef142, arg13 -> undef143, arg14 -> undef144, arg15 -> undef145, arg16 -> undef146, arg17 -> undef147, arg18 -> undef148, arg19 -> undef149, arg20 -> undef150, arg21 -> undef151, arg22 -> undef152, arg23 -> undef153, arg24 -> undef154, arg25 -> undef155}>
<l7, l7, (arg3 > ~(1)) /\ (undef210 > 0) /\ (undef210 < arg3) /\ (arg2 >= arg1) /\ (undef210 < undef187), par{arg1 -> (arg1 + 1), arg3 -> undef187, arg4 -> undef188, arg5 -> undef189, arg6 -> undef190, arg7 -> undef191, arg8 -> undef192, arg9 -> undef193, arg10 -> undef194, arg11 -> undef195, arg12 -> undef196, arg13 -> undef197, arg14 -> undef198, arg15 -> undef199, arg16 -> undef200, arg17 -> undef201, arg18 -> undef202, arg19 -> undef203, arg20 -> undef204, arg21 -> undef205, arg22 -> undef206, arg23 -> undef207, arg24 -> undef208, arg25 -> undef209}>
<l7, l7, (arg2 >= arg1) /\ (undef236 < arg3) /\ (arg3 > ~(1)), par{arg1 -> (arg1 + 1), arg3 -> 1, arg4 -> undef214, arg5 -> undef215, arg6 -> undef216, arg7 -> undef217, arg8 -> undef218, arg9 -> undef219, arg10 -> undef220, arg11 -> undef221, arg12 -> undef222, arg13 -> undef223, arg14 -> undef224, arg15 -> undef225, arg16 -> undef226, arg17 -> undef227, arg18 -> undef228, arg19 -> undef229, arg20 -> undef230, arg21 -> undef231, arg22 -> undef232, arg23 -> undef233, arg24 -> undef234, arg25 -> undef235}>
<l8, l8, (arg2 > 0) /\ (undef312 > ~(1)) /\ (arg6 > 0) /\ (arg3 > 0) /\ (arg20 > ~(1)) /\ (arg20 < undef312) /\ (arg10 > 0) /\ (arg4 > 0) /\ (arg13 > 0) /\ (arg11 > 0) /\ (arg12 > 0) /\ (undef313 > ~(1)) /\ (arg9 > 0) /\ (arg5 > 0) /\ (arg18 > 0) /\ (arg14 > 0) /\ (arg19 > 0) /\ (arg17 > 0) /\ (arg15 > 0) /\ (arg16 > 0) /\ (arg25 > ~(1)) /\ (arg21 > ~(1)) /\ (arg1 > 9) /\ (undef287 > 9) /\ ((arg21 + 5) <= arg1) /\ ((arg22 + 9) <= arg1) /\ ((arg23 + 9) <= arg1) /\ ((arg25 + 3) <= arg1) /\ ((arg24 + 9) <= arg1), par{arg1 -> undef287, arg2 -> (arg2 - 1), arg4 -> undef290, arg5 -> undef291, arg9 -> undef295, arg11 -> undef297, arg13 -> undef299, arg14 -> undef300, arg15 -> undef301, arg16 -> undef302, arg17 -> undef303, arg18 -> undef304, arg19 -> undef305, arg20 -> (arg20 + 1), arg21 -> (arg21 + 1), arg22 -> undef308, arg23 -> undef309, arg24 -> undef310, arg25 -> (arg25 + 1)}>
<l8, l8, (arg2 > 0) /\ (undef339 > ~(1)) /\ (arg6 > 0) /\ (arg3 > 0) /\ (arg20 > ~(1)) /\ (arg20 < undef339) /\ (arg10 > 0) /\ (arg12 > 0) /\ (undef340 > ~(1)) /\ (arg18 > 0) /\ (arg19 > 0) /\ (arg17 > 0) /\ (arg8 > 0) /\ (arg25 > ~(1)) /\ (arg21 > ~(1)) /\ (arg1 > 11) /\ (undef314 > 13) /\ ((arg21 + 5) <= arg1) /\ ((arg22 + 9) <= arg1) /\ ((arg23 + 9) <= arg1) /\ ((arg24 + 9) <= arg1) /\ ((arg25 + 3) <= arg1) /\ (arg8 = arg9) /\ (arg10 = arg11) /\ (arg12 = arg13) /\ (arg7 = arg16), par{arg1 -> undef314, arg2 -> (arg2 - 1), arg3 -> 0, arg4 -> 1, arg5 -> 1, arg6 -> undef319, arg7 -> undef320, arg9 -> undef322, arg11 -> undef324, arg13 -> 0, arg14 -> undef327, arg15 -> 2, arg16 -> undef329, arg17 -> undef330, arg18 -> undef331, arg19 -> undef332, arg20 -> (arg20 + 1), arg21 -> (arg21 + 1), arg22 -> undef335, arg23 -> undef336, arg24 -> undef337, arg25 -> (arg25 + 1)}>

Fresh variables:
undef2, undef7, undef11, undef12, undef13, undef14, undef18, undef21, undef22, undef24, undef25, undef26, undef27, undef28, undef30, undef31, undef32, undef33, undef34, undef35, undef36, undef37, undef38, undef39, undef40, undef41, undef42, undef43, undef44, undef45, undef46, undef47, undef48, undef49, undef50, undef51, undef52, undef55, undef57, undef58, undef60, undef61, undef62, undef63, undef64, undef65, undef66, undef67, undef68, undef69, undef70, undef71, undef72, undef73, undef74, undef75, undef76, undef78, undef80, undef81, undef82, undef83, undef84, undef85, undef86, undef87, undef88, undef89, undef90, undef91, undef92, undef93, undef94, undef95, undef96, undef97, undef98, undef99, undef100, undef101, undef102, undef103, undef104, undef107, undef108, undef109, undef110, undef111, undef112, undef113, undef114, undef115, undef116, undef117, undef118, undef119, undef120, undef121, undef122, undef123, undef124, undef125, undef126, undef127, undef128, undef129, undef130, undef134, undef135, undef136, undef137, undef138, undef139, undef140, undef141, undef142, undef143, undef144, undef145, undef146, undef147, undef148, undef149, undef150, undef151, undef152, undef153, undef154, undef155, undef156, undef158, undef160, undef161, undef162, undef163, undef164, undef165, undef166, undef167, undef168, undef169, undef170, undef171, undef172, undef173, undef174, undef175, undef176, undef177, undef178, undef179, undef180, undef181, undef182, undef183, undef184, undef187, undef188, undef189, undef190, undef191, undef192, undef193, undef194, undef195, undef196, undef197, undef198, undef199, undef200, undef201, undef202, undef203, undef204, undef205, undef206, undef207, undef208, undef209, undef210, undef214, undef215, undef216, undef217, undef218, undef219, undef220, undef221, undef222, undef223, undef224, undef225, undef226, undef227, undef228, undef229, undef230, undef231, undef232, undef233, undef234, undef235, undef236, undef237, undef238, undef239, undef240, undef244, undef245, undef246, undef247, undef248, undef249, undef250, undef251, undef252, undef253, undef254, undef255, undef256, undef257, undef258, undef259, undef260, undef261, undef262, undef269, undef283, undef284, undef285, undef287, undef290, undef291, undef295, undef297, undef299, undef300, undef301, undef302, undef303, undef304, undef305, undef308, undef309, undef310, undef312, undef313, undef314, undef319, undef320, undef322, undef324, undef327, undef329, undef330, undef331, undef332, undef335, undef336, undef337, undef339, undef340, undef341, undef342, undef343, undef344, undef345, undef346, undef347, undef348, undef349, undef350, undef351, undef352, undef353, undef354, undef355, undef356, undef357, undef358, undef359, undef360, undef361, undef362, undef363, undef364, undef365, 

Undef variables:
undef2, undef7, undef11, undef12, undef13, undef14, undef18, undef21, undef22, undef24, undef25, undef26, undef27, undef28, undef30, undef31, undef32, undef33, undef34, undef35, undef36, undef37, undef38, undef39, undef40, undef41, undef42, undef43, undef44, undef45, undef46, undef47, undef48, undef49, undef50, undef51, undef52, undef55, undef57, undef58, undef60, undef61, undef62, undef63, undef64, undef65, undef66, undef67, undef68, undef69, undef70, undef71, undef72, undef73, undef74, undef75, undef76, undef78, undef80, undef81, undef82, undef83, undef84, undef85, undef86, undef87, undef88, undef89, undef90, undef91, undef92, undef93, undef94, undef95, undef96, undef97, undef98, undef99, undef100, undef101, undef102, undef103, undef104, undef107, undef108, undef109, undef110, undef111, undef112, undef113, undef114, undef115, undef116, undef117, undef118, undef119, undef120, undef121, undef122, undef123, undef124, undef125, undef126, undef127, undef128, undef129, undef130, undef134, undef135, undef136, undef137, undef138, undef139, undef140, undef141, undef142, undef143, undef144, undef145, undef146, undef147, undef148, undef149, undef150, undef151, undef152, undef153, undef154, undef155, undef156, undef158, undef160, undef161, undef162, undef163, undef164, undef165, undef166, undef167, undef168, undef169, undef170, undef171, undef172, undef173, undef174, undef175, undef176, undef177, undef178, undef179, undef180, undef181, undef182, undef183, undef184, undef187, undef188, undef189, undef190, undef191, undef192, undef193, undef194, undef195, undef196, undef197, undef198, undef199, undef200, undef201, undef202, undef203, undef204, undef205, undef206, undef207, undef208, undef209, undef210, undef214, undef215, undef216, undef217, undef218, undef219, undef220, undef221, undef222, undef223, undef224, undef225, undef226, undef227, undef228, undef229, undef230, undef231, undef232, undef233, undef234, undef235, undef236, undef237, undef238, undef239, undef240, undef244, undef245, undef246, undef247, undef248, undef249, undef250, undef251, undef252, undef253, undef254, undef255, undef256, undef257, undef258, undef259, undef260, undef261, undef262, undef269, undef283, undef284, undef285, undef287, undef290, undef291, undef295, undef297, undef299, undef300, undef301, undef302, undef303, undef304, undef305, undef308, undef309, undef310, undef312, undef313, undef314, undef319, undef320, undef322, undef324, undef327, undef329, undef330, undef331, undef332, undef335, undef336, undef337, undef339, undef340, undef341, undef342, undef343, undef344, undef345, undef346, undef347, undef348, undef349, undef350, undef351, undef352, undef353, undef354, undef355, undef356, undef357, undef358, undef359, undef360, undef361, undef362, undef363, undef364, undef365, 

Abstraction variables:

Exit nodes:

Accepting locations:

Asserts:

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

Init Location: 0
Graph 0:
Transitions:
Variables:

Graph 1:
Transitions:
<l8, l8, 9 + arg22 <= arg1 /\ 9 + arg23 <= arg1 /\ 9 + arg24 <= arg1 /\ 5 + arg21 <= arg1 /\ 3 + arg25 <= arg1 /\ 0 <= arg20 /\ 0 <= arg21 /\ 0 <= arg25 /\ 0 <= undef312 /\ 0 <= undef313 /\ 1 <= arg2 /\ 1 <= arg3 /\ 1 <= arg4 /\ 1 <= arg5 /\ 1 <= arg6 /\ 1 <= arg9 /\ 1 <= arg10 /\ 1 <= arg11 /\ 1 <= arg12 /\ 1 <= arg13 /\ 1 <= arg14 /\ 1 <= arg15 /\ 1 <= arg16 /\ 1 <= arg17 /\ 1 <= arg18 /\ 1 <= arg19 /\ 1 + arg20 <= undef312 /\ 10 <= arg1 /\ 10 <= undef287, {arg1 -> undef287, arg2 -> -1 + arg2, arg4 -> undef290, arg5 -> undef291, arg9 -> undef295, arg11 -> undef297, arg13 -> undef299, arg14 -> undef300, arg15 -> undef301, arg16 -> undef302, arg17 -> undef303, arg18 -> undef304, arg19 -> undef305, arg20 -> 1 + arg20, arg21 -> 1 + arg21, arg22 -> undef308, arg23 -> undef309, arg24 -> undef310, arg25 -> 1 + arg25, rest remain the same}>
<l8, l8, 9 + arg22 <= arg1 /\ 9 + arg23 <= arg1 /\ 9 + arg24 <= arg1 /\ 5 + arg21 <= arg1 /\ 3 + arg25 <= arg1 /\ 0 <= arg20 /\ 0 <= arg21 /\ 0 <= arg25 /\ 0 <= undef339 /\ 0 <= undef340 /\ 1 <= arg2 /\ 1 <= arg3 /\ 1 <= arg6 /\ 1 <= arg8 /\ 1 <= arg10 /\ 1 <= arg12 /\ 1 <= arg17 /\ 1 <= arg18 /\ 1 <= arg19 /\ 1 + arg20 <= undef339 /\ 12 <= arg1 /\ 14 <= undef314 /\ arg7 = arg16 /\ arg8 = arg9 /\ arg10 = arg11 /\ arg12 = arg13, {arg1 -> undef314, arg2 -> -1 + arg2, arg3 -> 0, arg4 -> 1, arg5 -> 1, arg6 -> undef319, arg7 -> undef320, arg9 -> undef322, arg11 -> undef324, arg13 -> 0, arg14 -> undef327, arg15 -> 2, arg16 -> undef329, arg17 -> undef330, arg18 -> undef331, arg19 -> undef332, arg20 -> 1 + arg20, arg21 -> 1 + arg21, arg22 -> undef335, arg23 -> undef336, arg24 -> undef337, arg25 -> 1 + arg25, rest remain the same}>
Variables:
arg1, arg2, arg3, arg4, arg5, arg6, arg9, arg10, arg11, arg12, arg13, arg14, arg15, arg16, arg17, arg18, arg19, arg20, arg21, arg22, arg23, arg24, arg25, arg7, arg8

Graph 2:
Transitions:
<l7, l7, arg1 <= arg2 /\ 0 <= arg3 /\ 1 + undef210 <= arg3 /\ 1 + undef210 <= undef187 /\ 1 <= undef210, {arg1 -> 1 + arg1, arg3 -> undef187, arg4 -> undef188, arg5 -> undef189, arg6 -> undef190, arg7 -> undef191, arg8 -> undef192, arg9 -> undef193, arg10 -> undef194, arg11 -> undef195, arg12 -> undef196, arg13 -> undef197, arg14 -> undef198, arg15 -> undef199, arg16 -> undef200, arg17 -> undef201, arg18 -> undef202, arg19 -> undef203, arg20 -> undef204, arg21 -> undef205, arg22 -> undef206, arg23 -> undef207, arg24 -> undef208, arg25 -> undef209, rest remain the same}>
<l7, l7, arg1 <= arg2 /\ 0 <= arg3 /\ 1 + undef236 <= arg3, {arg1 -> 1 + arg1, arg3 -> 1, arg4 -> undef214, arg5 -> undef215, arg6 -> undef216, arg7 -> undef217, arg8 -> undef218, arg9 -> undef219, arg10 -> undef220, arg11 -> undef221, arg12 -> undef222, arg13 -> undef223, arg14 -> undef224, arg15 -> undef225, arg16 -> undef226, arg17 -> undef227, arg18 -> undef228, arg19 -> undef229, arg20 -> undef230, arg21 -> undef231, arg22 -> undef232, arg23 -> undef233, arg24 -> undef234, arg25 -> undef235, 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, arg24, arg25

Graph 3:
Transitions:
<l6, l6, 0 <= arg3 /\ 1 + arg2 <= arg1 /\ 1 + undef130 <= arg3 /\ 1 + undef130 <= undef107 /\ 1 <= undef130, {arg1 -> -1 + arg1, arg3 -> undef107, arg4 -> undef108, arg5 -> undef109, arg6 -> undef110, arg7 -> undef111, arg8 -> undef112, arg9 -> undef113, arg10 -> undef114, arg11 -> undef115, arg12 -> undef116, arg13 -> undef117, arg14 -> undef118, arg15 -> undef119, arg16 -> undef120, arg17 -> undef121, arg18 -> undef122, arg19 -> undef123, arg20 -> undef124, arg21 -> undef125, arg22 -> undef126, arg23 -> undef127, arg24 -> undef128, arg25 -> undef129, rest remain the same}>
<l6, l6, 0 <= arg3 /\ 1 + arg2 <= arg1 /\ 1 + undef156 <= arg3, {arg1 -> -1 + arg1, arg3 -> 1, arg4 -> undef134, arg5 -> undef135, arg6 -> undef136, arg7 -> undef137, arg8 -> undef138, arg9 -> undef139, arg10 -> undef140, arg11 -> undef141, arg12 -> undef142, arg13 -> undef143, arg14 -> undef144, arg15 -> undef145, arg16 -> undef146, arg17 -> undef147, arg18 -> undef148, arg19 -> undef149, arg20 -> undef150, arg21 -> undef151, arg22 -> undef152, arg23 -> undef153, arg24 -> undef154, arg25 -> undef155, 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, arg24, arg25

Precedence: 
Graph 0

Graph 1
<l0, l8, 9 + undef21 <= undef2 /\ 9 + undef22 <= undef2 /\ 0 <= undef237 /\ 1 <= undef341 /\ 1 <= undef342 /\ undef238 <= 7 + undef341 /\ 10 <= undef238 /\ 12 <= undef2 /\ 12 <= undef262, {arg1 -> undef262, arg2 -> undef237, arg3 -> undef13, arg4 -> undef11, arg5 -> undef7, arg6 -> undef12, arg7 -> undef7, arg8 -> undef269, arg9 -> 0, arg10 -> undef14, arg11 -> undef240, arg12 -> 0, arg13 -> 0, arg14 -> 0, arg15 -> 0, arg16 -> 0, arg17 -> undef239, arg18 -> undef239, arg19 -> undef240, arg20 -> 1, arg21 -> 0, arg22 -> undef283, arg23 -> undef284, arg24 -> undef285, arg25 -> 0, rest remain the same}>

Graph 2
<l0, l7, 5 + undef30 <= undef26 /\ 3 + undef33 <= undef26 /\ 0 <= undef51 /\ 0 <= undef158 /\ 0 <= undef182 /\ 0 <= undef183 /\ 1 + undef158 <= undef30 /\ 1 + undef158 <= undef184 /\ 1 <= undef341 /\ 1 <= undef342 /\ 7 <= undef26 /\ 7 + undef31 <= undef26 /\ 7 + undef32 <= undef26 /\ 2 + undef182 <= undef342, {arg1 -> 0, arg2 -> undef158, arg3 -> undef27, arg4 -> undef160, arg5 -> undef161, arg6 -> undef162, arg7 -> undef163, arg8 -> undef164, arg9 -> undef165, arg10 -> undef166, arg11 -> undef167, arg12 -> undef168, arg13 -> undef169, arg14 -> undef170, arg15 -> undef171, arg16 -> undef172, arg17 -> undef173, arg18 -> undef174, arg19 -> undef175, arg20 -> undef176, arg21 -> undef177, arg22 -> undef178, arg23 -> undef179, arg24 -> undef180, arg25 -> undef181, rest remain the same}>

Graph 3
<l0, l6, 5 + undef30 <= undef26 /\ 3 + undef33 <= undef26 /\ 0 <= undef51 /\ 0 <= undef78 /\ undef104 <= undef78 /\ 0 <= undef102 /\ 0 <= undef103 /\ 1 + undef78 <= undef30 /\ 1 <= undef341 /\ 1 <= undef342 /\ 7 <= undef26 /\ 7 + undef31 <= undef26 /\ 7 + undef32 <= undef26 /\ 2 + undef102 <= undef342, {arg1 -> undef30, arg2 -> undef78, arg3 -> undef28, arg4 -> undef80, arg5 -> undef81, arg6 -> undef82, arg7 -> undef83, arg8 -> undef84, arg9 -> undef85, arg10 -> undef86, arg11 -> undef87, arg12 -> undef88, arg13 -> undef89, arg14 -> undef90, arg15 -> undef91, arg16 -> undef92, arg17 -> undef93, arg18 -> undef94, arg19 -> undef95, arg20 -> undef96, arg21 -> undef97, arg22 -> undef98, arg23 -> undef99, arg24 -> undef100, arg25 -> undef101, 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.040462
Some transition disabled by a set of invariant(s):
Invariant at l8: arg13 <= 0

Strengthening and disabling transitions...
> It's unfeasible. Removing transition: 
<l8, l8, 9 + arg22 <= arg1 /\ 9 + arg23 <= arg1 /\ 9 + arg24 <= arg1 /\ 5 + arg21 <= arg1 /\ 3 + arg25 <= arg1 /\ 0 <= arg20 /\ 0 <= arg21 /\ 0 <= arg25 /\ 0 <= undef312 /\ 0 <= undef313 /\ 1 <= arg2 /\ 1 <= arg3 /\ 1 <= arg4 /\ 1 <= arg5 /\ 1 <= arg6 /\ 1 <= arg9 /\ 1 <= arg10 /\ 1 <= arg11 /\ 1 <= arg12 /\ 1 <= arg13 /\ 1 <= arg14 /\ 1 <= arg15 /\ 1 <= arg16 /\ 1 <= arg17 /\ 1 <= arg18 /\ 1 <= arg19 /\ 1 + arg20 <= undef312 /\ 10 <= arg1 /\ 10 <= undef287, {arg1 -> undef287, arg2 -> -1 + arg2, arg4 -> undef290, arg5 -> undef291, arg9 -> undef295, arg11 -> undef297, arg13 -> undef299, arg14 -> undef300, arg15 -> undef301, arg16 -> undef302, arg17 -> undef303, arg18 -> undef304, arg19 -> undef305, arg20 -> 1 + arg20, arg21 -> 1 + arg21, arg22 -> undef308, arg23 -> undef309, arg24 -> undef310, arg25 -> 1 + arg25, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l8, l8, 9 + arg22 <= arg1 /\ 9 + arg23 <= arg1 /\ 9 + arg24 <= arg1 /\ 5 + arg21 <= arg1 /\ 3 + arg25 <= arg1 /\ 0 <= arg20 /\ 0 <= arg21 /\ 0 <= arg25 /\ 0 <= undef339 /\ 0 <= undef340 /\ 1 <= arg2 /\ 1 <= arg3 /\ 1 <= arg6 /\ 1 <= arg8 /\ 1 <= arg10 /\ 1 <= arg12 /\ 1 <= arg17 /\ 1 <= arg18 /\ 1 <= arg19 /\ 1 + arg20 <= undef339 /\ 12 <= arg1 /\ 14 <= undef314 /\ arg7 = arg16 /\ arg8 = arg9 /\ arg10 = arg11 /\ arg12 = arg13, {arg1 -> undef314, arg2 -> -1 + arg2, arg3 -> 0, arg4 -> 1, arg5 -> 1, arg6 -> undef319, arg7 -> undef320, arg9 -> undef322, arg11 -> undef324, arg13 -> 0, arg14 -> undef327, arg15 -> 2, arg16 -> undef329, arg17 -> undef330, arg18 -> undef331, arg19 -> undef332, arg20 -> 1 + arg20, arg21 -> 1 + arg21, arg22 -> undef335, arg23 -> undef336, arg24 -> undef337, arg25 -> 1 + arg25, rest remain the same}>
Checking unfeasibility...
Time used: 2.5e-05

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

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

Checking conditional termination of SCC {l7}...

LOG: CALL solveLinear

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

Checking conditional termination of SCC {l6}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.003166s
Ranking function: -8 + 8*arg1 - 8*arg2
New Graphs: 
Program Terminates