YES

Solver Timeout: 4
Global Timeout: 300
No parsing errors!
Init Location: 0
Transitions:
<l0, l8, true>
<l1, l2, (undef2 <= arg2) /\ (arg2 > 9) /\ (undef2 > 9) /\ ((arg7 + 3) <= arg2) /\ ((arg6 + 5) <= 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 -> arg7, arg22 -> undef22, arg23 -> undef23}>
<l3, l4, (undef47 > ~(1)) /\ (arg2 > 0) /\ (undef48 > ~(1)) /\ (undef48 > undef24) /\ (undef49 > ~(1)) /\ (undef49 > undef25) /\ (arg1 > 0), par{arg1 -> undef24, arg2 -> undef25, arg3 -> undef26, arg4 -> undef27, arg5 -> undef28, arg6 -> undef29, arg7 -> undef30, arg8 -> undef31, 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, (undef50 < arg1) /\ (arg1 > ~(1)) /\ (undef51 < arg2) /\ (arg2 > ~(1)), par{arg1 -> undef50, arg2 -> undef51, arg3 -> undef52, arg4 -> undef53, arg5 -> undef54, arg6 -> undef55, arg7 -> undef56, arg8 -> undef57, arg9 -> undef58, arg10 -> undef59, arg11 -> undef60, arg12 -> undef61, arg13 -> undef62, arg14 -> undef63, arg15 -> undef64, arg16 -> undef65, arg17 -> undef66, arg18 -> undef67, arg19 -> undef68, arg20 -> undef69, arg21 -> undef70, arg22 -> undef71, arg23 -> undef72}>
<l4, l6, (arg1 > 0) /\ (arg2 > 0), par{arg1 -> 0, arg2 -> 0, arg3 -> arg1, arg4 -> undef76, arg5 -> undef77, arg6 -> undef78, arg7 -> undef79, arg8 -> undef80, arg9 -> undef81, arg10 -> undef82, arg11 -> undef83, arg12 -> undef84, arg13 -> undef85, arg14 -> undef86, arg15 -> undef87, arg16 -> undef88, arg17 -> undef89, arg18 -> undef90, arg19 -> undef91, arg20 -> undef92, arg21 -> undef93, arg22 -> undef94, arg23 -> undef95}>
<l4, l6, (arg1 > 0), par{arg1 -> 1, arg2 -> undef97, arg3 -> arg1, 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 > 0) /\ (arg3 > 0) /\ (arg1 > 0) /\ (undef121 < arg3), par{arg3 -> undef121, arg4 -> undef122, arg5 -> undef123, arg6 -> undef124, arg7 -> undef125, arg8 -> undef126, arg9 -> undef127, arg10 -> undef128, arg11 -> undef129, arg12 -> undef130, arg13 -> undef131, arg14 -> undef132, arg15 -> undef133, arg16 -> undef134, arg17 -> undef135, arg18 -> undef136, arg19 -> undef137, arg20 -> undef138, arg21 -> undef139, arg22 -> undef140, arg23 -> undef141}>
<l3, l1, (undef142 > ~(1)) /\ (arg2 > 0) /\ ((undef143 - 7) <= arg1) /\ (arg1 > 0) /\ (undef143 > 7), par{arg1 -> undef142, arg2 -> undef143, arg3 -> undef144, arg4 -> undef145, arg5 -> 1, arg6 -> 0, arg7 -> 0, arg8 -> undef149, arg9 -> undef150, arg10 -> undef151, arg11 -> undef152, arg12 -> undef153, arg13 -> undef154, arg14 -> undef155, arg15 -> undef156, arg16 -> undef157, arg17 -> undef158, arg18 -> undef159, arg19 -> undef160, arg20 -> undef161, arg21 -> undef162, arg22 -> undef163, arg23 -> undef164}>
<l2, l7, (arg2 > 11) /\ (undef165 > 11) /\ ((arg21 + 3) <= arg2) /\ ((arg20 + 5) <= arg2), par{arg1 -> undef165, arg2 -> arg1, arg3 -> arg13, arg4 -> arg11, arg5 -> arg7, arg6 -> arg12, arg7 -> arg6, arg8 -> undef172, 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 -> undef185, arg22 -> arg20, arg23 -> arg21}>
<l7, l7, (arg2 > 0) /\ (undef211 > ~(1)) /\ (arg6 > 0) /\ (arg3 > 0) /\ (arg20 > ~(1)) /\ (arg20 < undef211) /\ (arg10 > 0) /\ (arg4 > 0) /\ (arg13 > 0) /\ (arg11 > 0) /\ (arg12 > 0) /\ (undef212 > ~(1)) /\ (arg9 > 0) /\ (arg5 > 0) /\ (arg18 > 0) /\ (arg14 > 0) /\ (arg19 > 0) /\ (arg17 > 0) /\ (arg15 > 0) /\ (arg16 > 0) /\ (arg23 > ~(1)) /\ (arg22 > ~(1)) /\ (arg1 > 9) /\ (undef188 > 9) /\ ((arg21 + 9) <= arg1) /\ ((arg23 + 3) <= arg1) /\ ((arg22 + 5) <= arg1), par{arg1 -> undef188, arg2 -> (arg2 - 1), arg4 -> undef191, arg5 -> undef192, arg9 -> undef196, arg11 -> undef198, arg13 -> undef200, arg14 -> undef201, arg15 -> undef202, arg16 -> undef203, arg17 -> undef204, arg18 -> undef205, arg19 -> undef206, arg20 -> (arg20 + 1), arg21 -> undef208, arg22 -> (arg22 + 1), arg23 -> (arg23 + 1)}>
<l7, l7, (arg2 > 0) /\ (undef236 > ~(1)) /\ (arg6 > 0) /\ (arg3 > 0) /\ (arg20 > ~(1)) /\ (arg20 < undef236) /\ (arg10 > 0) /\ (arg12 > 0) /\ (undef237 > ~(1)) /\ (arg18 > 0) /\ (arg19 > 0) /\ (arg17 > 0) /\ (arg8 > 0) /\ (arg23 > ~(1)) /\ (arg22 > ~(1)) /\ (arg1 > 11) /\ (undef213 > 13) /\ ((arg21 + 9) <= arg1) /\ ((arg23 + 3) <= arg1) /\ ((arg22 + 5) <= arg1) /\ (arg8 = arg9) /\ (arg10 = arg11) /\ (arg12 = arg13) /\ (arg7 = arg16), par{arg1 -> undef213, arg2 -> (arg2 - 1), arg3 -> 0, arg4 -> 1, arg5 -> 1, arg6 -> undef218, arg7 -> undef219, arg9 -> undef221, arg11 -> undef223, arg13 -> 0, arg14 -> 2, arg15 -> undef227, arg16 -> undef228, arg17 -> undef229, arg18 -> undef230, arg19 -> undef231, arg20 -> (arg20 + 1), arg21 -> undef233, arg22 -> (arg22 + 1), arg23 -> (arg23 + 1)}>
<l8, l3, true, par{arg1 -> undef238, arg2 -> undef239, arg3 -> undef240, arg4 -> undef241, arg5 -> undef242, arg6 -> undef243, arg7 -> undef244, arg8 -> undef245, arg9 -> undef246, arg10 -> undef247, arg11 -> undef248, arg12 -> undef249, arg13 -> undef250, arg14 -> undef251, arg15 -> undef252, arg16 -> undef253, arg17 -> undef254, arg18 -> undef255, arg19 -> undef256, arg20 -> undef257, arg21 -> undef258, arg22 -> undef259, arg23 -> undef260}>

Fresh variables:
undef2, undef7, undef11, undef12, undef13, undef14, undef18, undef22, undef23, undef24, undef25, undef26, undef27, undef28, undef29, undef30, undef31, undef32, undef33, undef34, undef35, undef36, undef37, undef38, undef39, undef40, undef41, undef42, undef43, undef44, undef45, undef46, undef47, undef48, undef49, undef50, undef51, undef52, undef53, undef54, undef55, undef56, undef57, undef58, undef59, undef60, undef61, undef62, undef63, undef64, undef65, undef66, undef67, undef68, undef69, undef70, undef71, undef72, undef76, undef77, undef78, undef79, undef80, undef81, undef82, undef83, undef84, undef85, undef86, undef87, undef88, undef89, undef90, undef91, undef92, undef93, undef94, undef95, undef97, undef99, undef100, undef101, undef102, undef103, undef104, undef105, undef106, undef107, undef108, undef109, undef110, undef111, undef112, undef113, undef114, undef115, undef116, undef117, undef118, undef121, undef122, undef123, undef124, undef125, undef126, undef127, undef128, undef129, undef130, undef131, undef132, undef133, undef134, undef135, undef136, undef137, undef138, undef139, undef140, undef141, undef142, undef143, undef144, undef145, undef149, undef150, undef151, undef152, undef153, undef154, undef155, undef156, undef157, undef158, undef159, undef160, undef161, undef162, undef163, undef164, undef165, undef172, undef185, undef188, undef191, undef192, undef196, undef198, undef200, undef201, undef202, undef203, undef204, undef205, undef206, undef208, undef211, undef212, undef213, undef218, undef219, undef221, undef223, undef227, undef228, undef229, undef230, undef231, undef233, undef236, undef237, undef238, undef239, undef240, undef241, undef242, undef243, undef244, undef245, undef246, undef247, undef248, undef249, undef250, undef251, undef252, undef253, undef254, undef255, undef256, undef257, undef258, undef259, undef260, 

Undef variables:
undef2, undef7, undef11, undef12, undef13, undef14, undef18, undef22, undef23, undef24, undef25, undef26, undef27, undef28, undef29, undef30, undef31, undef32, undef33, undef34, undef35, undef36, undef37, undef38, undef39, undef40, undef41, undef42, undef43, undef44, undef45, undef46, undef47, undef48, undef49, undef50, undef51, undef52, undef53, undef54, undef55, undef56, undef57, undef58, undef59, undef60, undef61, undef62, undef63, undef64, undef65, undef66, undef67, undef68, undef69, undef70, undef71, undef72, undef76, undef77, undef78, undef79, undef80, undef81, undef82, undef83, undef84, undef85, undef86, undef87, undef88, undef89, undef90, undef91, undef92, undef93, undef94, undef95, undef97, undef99, undef100, undef101, undef102, undef103, undef104, undef105, undef106, undef107, undef108, undef109, undef110, undef111, undef112, undef113, undef114, undef115, undef116, undef117, undef118, undef121, undef122, undef123, undef124, undef125, undef126, undef127, undef128, undef129, undef130, undef131, undef132, undef133, undef134, undef135, undef136, undef137, undef138, undef139, undef140, undef141, undef142, undef143, undef144, undef145, undef149, undef150, undef151, undef152, undef153, undef154, undef155, undef156, undef157, undef158, undef159, undef160, undef161, undef162, undef163, undef164, undef165, undef172, undef185, undef188, undef191, undef192, undef196, undef198, undef200, undef201, undef202, undef203, undef204, undef205, undef206, undef208, undef211, undef212, undef213, undef218, undef219, undef221, undef223, undef227, undef228, undef229, undef230, undef231, undef233, undef236, undef237, undef238, undef239, undef240, undef241, undef242, undef243, undef244, undef245, undef246, undef247, undef248, undef249, undef250, undef251, undef252, undef253, undef254, undef255, undef256, undef257, undef258, undef259, undef260, 

Abstraction variables:

Exit nodes:

Accepting locations:

Asserts:

Preprocessed LLVMGraph
Init Location: 0
Transitions:
<l0, l6, (undef47 > ~(1)) /\ (undef239 > 0) /\ (undef48 > ~(1)) /\ (undef48 > undef24) /\ (undef49 > ~(1)) /\ (undef49 > undef25) /\ (undef238 > 0) /\ (undef24 > 0) /\ (undef25 > 0), par{arg1 -> 0, arg2 -> 0, arg3 -> undef24, arg4 -> undef76, arg5 -> undef77, arg6 -> undef78, arg7 -> undef79, arg8 -> undef80, arg9 -> undef81, arg10 -> undef82, arg11 -> undef83, arg12 -> undef84, arg13 -> undef85, arg14 -> undef86, arg15 -> undef87, arg16 -> undef88, arg17 -> undef89, arg18 -> undef90, arg19 -> undef91, arg20 -> undef92, arg21 -> undef93, arg22 -> undef94, arg23 -> undef95}>
<l0, l6, (undef47 > ~(1)) /\ (undef239 > 0) /\ (undef48 > ~(1)) /\ (undef48 > undef24) /\ (undef49 > ~(1)) /\ (undef49 > undef25) /\ (undef238 > 0) /\ (undef24 > 0), par{arg1 -> 1, arg2 -> undef97, arg3 -> undef24, 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}>
<l0, l7, (undef142 > ~(1)) /\ (undef239 > 0) /\ ((undef143 - 7) <= undef238) /\ (undef238 > 0) /\ (undef143 > 7) /\ (undef2 <= undef143) /\ (undef143 > 9) /\ (undef2 > 9) /\ ((0 + 3) <= undef143) /\ ((0 + 5) <= undef143) /\ (undef2 > 11) /\ (undef165 > 11) /\ ((0 + 3) <= undef2) /\ ((0 + 5) <= undef2), par{arg1 -> undef165, arg2 -> undef142, arg3 -> undef13, arg4 -> undef11, arg5 -> undef7, arg6 -> undef12, arg7 -> undef7, arg8 -> undef172, arg9 -> 0, arg10 -> undef14, arg11 -> undef145, arg12 -> 0, arg13 -> 0, arg14 -> 0, arg15 -> 0, arg16 -> 0, arg17 -> undef144, arg18 -> undef144, arg19 -> undef145, arg20 -> 1, arg21 -> undef185, arg22 -> 0, arg23 -> 0}>
<l6, l6, (arg2 > 0) /\ (arg3 > 0) /\ (arg1 > 0) /\ (undef121 < arg3), par{arg3 -> undef121, arg4 -> undef122, arg5 -> undef123, arg6 -> undef124, arg7 -> undef125, arg8 -> undef126, arg9 -> undef127, arg10 -> undef128, arg11 -> undef129, arg12 -> undef130, arg13 -> undef131, arg14 -> undef132, arg15 -> undef133, arg16 -> undef134, arg17 -> undef135, arg18 -> undef136, arg19 -> undef137, arg20 -> undef138, arg21 -> undef139, arg22 -> undef140, arg23 -> undef141}>
<l7, l7, (arg2 > 0) /\ (undef211 > ~(1)) /\ (arg6 > 0) /\ (arg3 > 0) /\ (arg20 > ~(1)) /\ (arg20 < undef211) /\ (arg10 > 0) /\ (arg4 > 0) /\ (arg13 > 0) /\ (arg11 > 0) /\ (arg12 > 0) /\ (undef212 > ~(1)) /\ (arg9 > 0) /\ (arg5 > 0) /\ (arg18 > 0) /\ (arg14 > 0) /\ (arg19 > 0) /\ (arg17 > 0) /\ (arg15 > 0) /\ (arg16 > 0) /\ (arg23 > ~(1)) /\ (arg22 > ~(1)) /\ (arg1 > 9) /\ (undef188 > 9) /\ ((arg21 + 9) <= arg1) /\ ((arg23 + 3) <= arg1) /\ ((arg22 + 5) <= arg1), par{arg1 -> undef188, arg2 -> (arg2 - 1), arg4 -> undef191, arg5 -> undef192, arg9 -> undef196, arg11 -> undef198, arg13 -> undef200, arg14 -> undef201, arg15 -> undef202, arg16 -> undef203, arg17 -> undef204, arg18 -> undef205, arg19 -> undef206, arg20 -> (arg20 + 1), arg21 -> undef208, arg22 -> (arg22 + 1), arg23 -> (arg23 + 1)}>
<l7, l7, (arg2 > 0) /\ (undef236 > ~(1)) /\ (arg6 > 0) /\ (arg3 > 0) /\ (arg20 > ~(1)) /\ (arg20 < undef236) /\ (arg10 > 0) /\ (arg12 > 0) /\ (undef237 > ~(1)) /\ (arg18 > 0) /\ (arg19 > 0) /\ (arg17 > 0) /\ (arg8 > 0) /\ (arg23 > ~(1)) /\ (arg22 > ~(1)) /\ (arg1 > 11) /\ (undef213 > 13) /\ ((arg21 + 9) <= arg1) /\ ((arg23 + 3) <= arg1) /\ ((arg22 + 5) <= arg1) /\ (arg8 = arg9) /\ (arg10 = arg11) /\ (arg12 = arg13) /\ (arg7 = arg16), par{arg1 -> undef213, arg2 -> (arg2 - 1), arg3 -> 0, arg4 -> 1, arg5 -> 1, arg6 -> undef218, arg7 -> undef219, arg9 -> undef221, arg11 -> undef223, arg13 -> 0, arg14 -> 2, arg15 -> undef227, arg16 -> undef228, arg17 -> undef229, arg18 -> undef230, arg19 -> undef231, arg20 -> (arg20 + 1), arg21 -> undef233, arg22 -> (arg22 + 1), arg23 -> (arg23 + 1)}>

Fresh variables:
undef2, undef7, undef11, undef12, undef13, undef14, undef18, undef22, undef23, undef24, undef25, undef26, undef27, undef28, undef29, undef30, undef31, undef32, undef33, undef34, undef35, undef36, undef37, undef38, undef39, undef40, undef41, undef42, undef43, undef44, undef45, undef46, undef47, undef48, undef49, undef50, undef51, undef52, undef53, undef54, undef55, undef56, undef57, undef58, undef59, undef60, undef61, undef62, undef63, undef64, undef65, undef66, undef67, undef68, undef69, undef70, undef71, undef72, undef76, undef77, undef78, undef79, undef80, undef81, undef82, undef83, undef84, undef85, undef86, undef87, undef88, undef89, undef90, undef91, undef92, undef93, undef94, undef95, undef97, undef99, undef100, undef101, undef102, undef103, undef104, undef105, undef106, undef107, undef108, undef109, undef110, undef111, undef112, undef113, undef114, undef115, undef116, undef117, undef118, undef121, undef122, undef123, undef124, undef125, undef126, undef127, undef128, undef129, undef130, undef131, undef132, undef133, undef134, undef135, undef136, undef137, undef138, undef139, undef140, undef141, undef142, undef143, undef144, undef145, undef149, undef150, undef151, undef152, undef153, undef154, undef155, undef156, undef157, undef158, undef159, undef160, undef161, undef162, undef163, undef164, undef165, undef172, undef185, undef188, undef191, undef192, undef196, undef198, undef200, undef201, undef202, undef203, undef204, undef205, undef206, undef208, undef211, undef212, undef213, undef218, undef219, undef221, undef223, undef227, undef228, undef229, undef230, undef231, undef233, undef236, undef237, undef238, undef239, undef240, undef241, undef242, undef243, undef244, undef245, undef246, undef247, undef248, undef249, undef250, undef251, undef252, undef253, undef254, undef255, undef256, undef257, undef258, undef259, undef260, 

Undef variables:
undef2, undef7, undef11, undef12, undef13, undef14, undef18, undef22, undef23, undef24, undef25, undef26, undef27, undef28, undef29, undef30, undef31, undef32, undef33, undef34, undef35, undef36, undef37, undef38, undef39, undef40, undef41, undef42, undef43, undef44, undef45, undef46, undef47, undef48, undef49, undef50, undef51, undef52, undef53, undef54, undef55, undef56, undef57, undef58, undef59, undef60, undef61, undef62, undef63, undef64, undef65, undef66, undef67, undef68, undef69, undef70, undef71, undef72, undef76, undef77, undef78, undef79, undef80, undef81, undef82, undef83, undef84, undef85, undef86, undef87, undef88, undef89, undef90, undef91, undef92, undef93, undef94, undef95, undef97, undef99, undef100, undef101, undef102, undef103, undef104, undef105, undef106, undef107, undef108, undef109, undef110, undef111, undef112, undef113, undef114, undef115, undef116, undef117, undef118, undef121, undef122, undef123, undef124, undef125, undef126, undef127, undef128, undef129, undef130, undef131, undef132, undef133, undef134, undef135, undef136, undef137, undef138, undef139, undef140, undef141, undef142, undef143, undef144, undef145, undef149, undef150, undef151, undef152, undef153, undef154, undef155, undef156, undef157, undef158, undef159, undef160, undef161, undef162, undef163, undef164, undef165, undef172, undef185, undef188, undef191, undef192, undef196, undef198, undef200, undef201, undef202, undef203, undef204, undef205, undef206, undef208, undef211, undef212, undef213, undef218, undef219, undef221, undef223, undef227, undef228, undef229, undef230, undef231, undef233, undef236, undef237, undef238, undef239, undef240, undef241, undef242, undef243, undef244, undef245, undef246, undef247, undef248, undef249, undef250, undef251, undef252, undef253, undef254, undef255, undef256, undef257, undef258, undef259, undef260, 

Abstraction variables:

Exit nodes:

Accepting locations:

Asserts:

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

Init Location: 0
Graph 0:
Transitions:
Variables:

Graph 1:
Transitions:
<l7, l7, 9 + arg21 <= arg1 /\ 3 + arg23 <= arg1 /\ 5 + arg22 <= arg1 /\ 0 <= arg20 /\ 0 <= arg22 /\ 0 <= arg23 /\ 0 <= undef211 /\ 0 <= undef212 /\ 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 <= undef211 /\ 10 <= arg1 /\ 10 <= undef188, {arg1 -> undef188, arg2 -> -1 + arg2, arg4 -> undef191, arg5 -> undef192, arg9 -> undef196, arg11 -> undef198, arg13 -> undef200, arg14 -> undef201, arg15 -> undef202, arg16 -> undef203, arg17 -> undef204, arg18 -> undef205, arg19 -> undef206, arg20 -> 1 + arg20, arg21 -> undef208, arg22 -> 1 + arg22, arg23 -> 1 + arg23, rest remain the same}>
<l7, l7, 9 + arg21 <= arg1 /\ 3 + arg23 <= arg1 /\ 5 + arg22 <= arg1 /\ 0 <= arg20 /\ 0 <= arg22 /\ 0 <= arg23 /\ 0 <= undef236 /\ 0 <= undef237 /\ 1 <= arg2 /\ 1 <= arg3 /\ 1 <= arg6 /\ 1 <= arg8 /\ 1 <= arg10 /\ 1 <= arg12 /\ 1 <= arg17 /\ 1 <= arg18 /\ 1 <= arg19 /\ 1 + arg20 <= undef236 /\ 12 <= arg1 /\ 14 <= undef213 /\ arg7 = arg16 /\ arg8 = arg9 /\ arg10 = arg11 /\ arg12 = arg13, {arg1 -> undef213, arg2 -> -1 + arg2, arg3 -> 0, arg4 -> 1, arg5 -> 1, arg6 -> undef218, arg7 -> undef219, arg9 -> undef221, arg11 -> undef223, arg13 -> 0, arg14 -> 2, arg15 -> undef227, arg16 -> undef228, arg17 -> undef229, arg18 -> undef230, arg19 -> undef231, arg20 -> 1 + arg20, arg21 -> undef233, arg22 -> 1 + arg22, arg23 -> 1 + arg23, 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, arg7, arg8

Graph 2:
Transitions:
<l6, l6, 1 <= arg1 /\ 1 <= arg2 /\ 1 <= arg3 /\ 1 + undef121 <= arg3, {arg3 -> undef121, arg4 -> undef122, arg5 -> undef123, arg6 -> undef124, arg7 -> undef125, arg8 -> undef126, arg9 -> undef127, arg10 -> undef128, arg11 -> undef129, arg12 -> undef130, arg13 -> undef131, arg14 -> undef132, arg15 -> undef133, arg16 -> undef134, arg17 -> undef135, arg18 -> undef136, arg19 -> undef137, arg20 -> undef138, arg21 -> undef139, arg22 -> undef140, arg23 -> undef141, 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, l7, undef2 <= undef143 /\ 0 <= undef142 /\ 1 <= undef238 /\ 1 <= undef239 /\ undef143 <= 7 + undef238 /\ 10 <= undef143 /\ 12 <= undef2 /\ 12 <= undef165, {arg1 -> undef165, arg2 -> undef142, arg3 -> undef13, arg4 -> undef11, arg5 -> undef7, arg6 -> undef12, arg7 -> undef7, arg8 -> undef172, arg9 -> 0, arg10 -> undef14, arg11 -> undef145, arg12 -> 0, arg13 -> 0, arg14 -> 0, arg15 -> 0, arg16 -> 0, arg17 -> undef144, arg18 -> undef144, arg19 -> undef145, arg20 -> 1, arg21 -> undef185, arg22 -> 0, arg23 -> 0, rest remain the same}>

Graph 2
<l0, l6, 0 <= undef47 /\ 0 <= undef48 /\ 0 <= undef49 /\ 1 + undef24 <= undef48 /\ 1 <= undef24 /\ 1 + undef25 <= undef49 /\ 1 <= undef25 /\ 1 <= undef238 /\ 1 <= undef239, {arg1 -> 0, arg2 -> 0, arg3 -> undef24, arg4 -> undef76, arg5 -> undef77, arg6 -> undef78, arg7 -> undef79, arg8 -> undef80, arg9 -> undef81, arg10 -> undef82, arg11 -> undef83, arg12 -> undef84, arg13 -> undef85, arg14 -> undef86, arg15 -> undef87, arg16 -> undef88, arg17 -> undef89, arg18 -> undef90, arg19 -> undef91, arg20 -> undef92, arg21 -> undef93, arg22 -> undef94, arg23 -> undef95, rest remain the same}>
<l0, l6, 0 <= undef47 /\ 0 <= undef48 /\ 0 <= undef49 /\ 1 + undef24 <= undef48 /\ 1 <= undef24 /\ 1 + undef25 <= undef49 /\ 1 <= undef238 /\ 1 <= undef239, {arg1 -> 1, arg2 -> undef97, arg3 -> undef24, 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}>

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

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

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

Strengthening and disabling transitions...
> It's unfeasible. Removing transition: 
<l7, l7, 9 + arg21 <= arg1 /\ 3 + arg23 <= arg1 /\ 5 + arg22 <= arg1 /\ 0 <= arg20 /\ 0 <= arg22 /\ 0 <= arg23 /\ 0 <= undef211 /\ 0 <= undef212 /\ 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 <= undef211 /\ 10 <= arg1 /\ 10 <= undef188, {arg1 -> undef188, arg2 -> -1 + arg2, arg4 -> undef191, arg5 -> undef192, arg9 -> undef196, arg11 -> undef198, arg13 -> undef200, arg14 -> undef201, arg15 -> undef202, arg16 -> undef203, arg17 -> undef204, arg18 -> undef205, arg19 -> undef206, arg20 -> 1 + arg20, arg21 -> undef208, arg22 -> 1 + arg22, arg23 -> 1 + arg23, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l7, l7, 9 + arg21 <= arg1 /\ 3 + arg23 <= arg1 /\ 5 + arg22 <= arg1 /\ 0 <= arg20 /\ 0 <= arg22 /\ 0 <= arg23 /\ 0 <= undef236 /\ 0 <= undef237 /\ 1 <= arg2 /\ 1 <= arg3 /\ 1 <= arg6 /\ 1 <= arg8 /\ 1 <= arg10 /\ 1 <= arg12 /\ 1 <= arg17 /\ 1 <= arg18 /\ 1 <= arg19 /\ 1 + arg20 <= undef236 /\ 12 <= arg1 /\ 14 <= undef213 /\ arg7 = arg16 /\ arg8 = arg9 /\ arg10 = arg11 /\ arg12 = arg13, {arg1 -> undef213, arg2 -> -1 + arg2, arg3 -> 0, arg4 -> 1, arg5 -> 1, arg6 -> undef218, arg7 -> undef219, arg9 -> undef221, arg11 -> undef223, arg13 -> 0, arg14 -> 2, arg15 -> undef227, arg16 -> undef228, arg17 -> undef229, arg18 -> undef230, arg19 -> undef231, arg20 -> 1 + arg20, arg21 -> undef233, arg22 -> 1 + arg22, arg23 -> 1 + arg23, rest remain the same}>
Checking unfeasibility...
Time used: 2.3e-05

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

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

Checking conditional termination of SCC {l6}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001483s
Ranking function: -1 + arg3
New Graphs: 
Program Terminates