NO

Solver Timeout: 4
Global Timeout: 300
No parsing errors!
Init Location: 0
Transitions:
<l0, l15, true>
<l1, l2, (undef2 > 6) /\ (undef1 > 9), par{arg1 -> undef1, arg2 -> undef2, arg3 -> undef3, arg4 -> undef4, arg5 -> undef5}>
<l1, l3, (undef7 > 6) /\ (undef6 > 4), par{arg1 -> undef6, arg2 -> undef7, arg3 -> 3, arg4 -> 1, arg5 -> undef10}>
<l1, l4, (undef12 > 6) /\ (undef11 > 6), par{arg1 -> undef11, arg2 -> undef12, arg3 -> undef13, arg4 -> undef14, arg5 -> 5}>
<l5, l4, (arg1 > 6) /\ (undef16 > 6) /\ (undef17 > 6) /\ ((arg2 + 2) <= arg1) /\ (5 = arg3), par{arg1 -> undef16, arg2 -> undef17, arg3 -> undef18, arg4 -> undef19, arg5 -> 5}>
<l4, l6, (arg1 > 6) /\ (arg2 > 6) /\ (undef21 > 6) /\ ((arg3 + 2) <= arg1) /\ ((arg4 + 2) <= arg2) /\ (5 = arg5), par{arg1 -> undef21, arg2 -> undef22, arg3 -> 5, arg4 -> undef24, arg5 -> undef25}>
<l3, l6, (arg1 > 0) /\ (arg2 > 2) /\ (undef26 > 9) /\ ((arg3 + 2) <= arg1) /\ ((arg4 + 2) <= arg2) /\ ((arg3 + 4) <= arg2), par{arg1 -> undef26, arg2 -> 6, arg3 -> 5, arg4 -> undef29, arg5 -> undef30}>
<l4, l6, (arg1 > 6) /\ (arg2 > 6) /\ (undef31 > 6) /\ ((arg3 + 2) <= arg1) /\ ((arg4 + 2) <= arg2) /\ (5 = arg5), par{arg1 -> undef31, arg2 -> undef32, arg3 -> 5, arg4 -> undef34, arg5 -> undef35}>
<l3, l6, ((undef36 - 9) <= arg1) /\ ((undef36 - 7) <= arg2) /\ (arg1 > 0) /\ (arg2 > 2) /\ (undef36 > 9) /\ ((arg3 + 2) <= arg1) /\ ((arg4 + 2) <= arg2) /\ ((arg3 + 4) <= arg2), par{arg1 -> undef36, arg2 -> 6, arg3 -> 5, arg4 -> undef39, arg5 -> undef40}>
<l7, l6, (undef41 <= arg1) /\ (arg1 > 6) /\ (undef41 > 6) /\ ((arg2 + 4) <= arg1) /\ ((arg3 + 4) <= arg1) /\ (5 = arg4), par{arg1 -> undef41, arg2 -> arg3, arg3 -> 5, arg4 -> undef44, arg5 -> undef45}>
<l8, l6, (undef46 <= arg1) /\ (arg1 > 9) /\ (undef46 > 9) /\ ((arg2 + 4) <= arg1) /\ (6 = arg3) /\ (5 = arg4), par{arg1 -> undef46, arg2 -> 6, arg3 -> 5, arg4 -> undef49, arg5 -> undef50}>
<l6, l9, (undef51 <= arg1) /\ (arg1 > 6) /\ (undef51 > 6) /\ ((arg2 + 4) <= arg1) /\ (5 = arg3), par{arg1 -> undef51, arg3 -> 5, arg4 -> undef54, arg5 -> undef55}>
<l6, l9, (undef56 <= arg1) /\ (arg1 > 6) /\ (undef56 > 6) /\ ((arg2 + 4) <= arg1) /\ (5 = arg3), par{arg1 -> undef56, arg3 -> 5, arg4 -> undef59, arg5 -> undef60}>
<l2, l2, (undef61 <= arg1) /\ (undef66 > undef67) /\ ((undef62 + 1) <= arg2) /\ (arg1 > 0) /\ (arg2 > 0) /\ (undef61 > 0) /\ (undef62 > ~(1)), par{arg1 -> undef61, arg2 -> undef62, arg3 -> undef63, arg4 -> undef64, arg5 -> undef65}>
<l2, l2, ((undef68 + 2) <= arg1) /\ (undef73 <= undef74) /\ (undef69 <= arg2) /\ (arg1 > 2) /\ (arg2 > 0) /\ (undef68 > 0) /\ (undef69 > 0), par{arg1 -> undef68, arg2 -> undef69, arg3 -> undef70, arg4 -> undef71, arg5 -> undef72}>
<l4, l10, (undef76 <= arg1) /\ (undef76 <= arg2) /\ (arg1 > 6) /\ (arg2 > 6) /\ (undef75 > 6) /\ (undef76 > 6) /\ (undef77 > ~(1)) /\ ((arg3 + 2) <= arg1) /\ ((arg4 + 2) <= arg2) /\ (5 = arg5), par{arg1 -> undef75, arg2 -> undef76, arg3 -> undef77, arg4 -> 5, arg5 -> 1}>
<l3, l10, ((undef81 - 2) <= arg2) /\ (arg1 > 0) /\ (arg2 > 2) /\ (undef80 > 9) /\ (undef81 > 4) /\ (undef82 > ~(1)) /\ ((arg3 + 2) <= arg1) /\ ((arg4 + 2) <= arg2) /\ ((arg3 + 4) <= arg2), par{arg1 -> undef80, arg2 -> undef81, arg3 -> undef82, arg4 -> 5, arg5 -> arg4}>
<l10, l10, (undef86 <= arg2) /\ (arg1 > 2) /\ (arg2 > 0) /\ (arg3 > 0) /\ (undef85 > 0) /\ (undef86 > 0) /\ (undef87 > ~(1)) /\ ((arg4 + 2) <= arg1) /\ ((arg5 + 2) <= arg2), par{arg1 -> undef85, arg2 -> undef86, arg3 -> undef87, arg4 -> undef88}>
<l4, l11, (undef90 <= arg1) /\ (undef90 <= arg2) /\ (arg1 > 6) /\ (arg2 > 6) /\ (undef90 > 6) /\ (undef91 > ~(1)) /\ ((arg3 + 2) <= arg1) /\ ((arg4 + 2) <= arg2) /\ (5 = arg5), par{arg1 -> undef90, arg2 -> undef91, arg3 -> 5, arg4 -> undef93, arg5 -> undef94}>
<l6, l11, (undef95 <= arg1) /\ (arg1 > 6) /\ (undef95 > 6) /\ (undef96 > ~(1)) /\ ((arg2 + 4) <= arg1) /\ (5 = arg3), par{arg1 -> undef95, arg2 -> undef96, arg3 -> 5, arg4 -> undef98, arg5 -> undef99}>
<l11, l11, (arg1 > 2) /\ (arg2 > 0) /\ (undef100 > 0) /\ (undef101 > ~(1)) /\ ((arg3 + 2) <= arg1), par{arg1 -> undef100, arg2 -> undef101, arg3 -> undef102, arg4 -> undef103, arg5 -> undef104}>
<l4, l12, (undef105 <= arg1) /\ (undef105 <= arg2) /\ (arg1 > 6) /\ (arg2 > 6) /\ (undef105 > 6) /\ (undef106 > ~(1)) /\ ((arg3 + 2) <= arg1) /\ ((arg4 + 2) <= arg2) /\ (5 = arg5), par{arg1 -> undef105, arg2 -> undef106, arg3 -> 5, arg4 -> undef108, arg5 -> undef109}>
<l6, l12, (undef110 <= arg1) /\ (arg1 > 6) /\ (undef110 > 6) /\ (undef111 > ~(1)) /\ ((arg2 + 4) <= arg1) /\ (5 = arg3), par{arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114}>
<l12, l12, (arg1 > 2) /\ (arg2 > 0) /\ (undef115 > 0) /\ (undef116 > ~(1)) /\ ((arg3 + 2) <= arg1), par{arg1 -> undef115, arg2 -> undef116, arg3 -> undef117, arg4 -> undef118, arg5 -> undef119}>
<l4, l13, (undef120 <= arg1) /\ (undef120 <= arg2) /\ (arg1 > 6) /\ (arg2 > 6) /\ (undef120 > 6) /\ (undef121 > ~(1)) /\ ((arg3 + 2) <= arg1) /\ ((arg4 + 2) <= arg2) /\ (5 = arg5), par{arg1 -> undef120, arg2 -> undef121, arg3 -> 5, arg4 -> undef123, arg5 -> undef124}>
<l9, l13, (undef125 <= arg1) /\ (arg1 > 6) /\ (undef125 > 6) /\ (undef126 > ~(1)) /\ ((arg2 + 4) <= arg1) /\ (5 = arg3), par{arg1 -> undef125, arg2 -> undef126, arg3 -> 5, arg4 -> undef128, arg5 -> undef129}>
<l13, l13, (arg1 > 2) /\ (arg2 > 0) /\ (undef130 > 0) /\ (undef131 > ~(1)) /\ ((arg3 + 2) <= arg1), par{arg1 -> undef130, arg2 -> undef131, arg3 -> undef132, arg4 -> undef133, arg5 -> undef134}>
<l13, l10, (undef136 <= arg1) /\ (arg1 > 2) /\ (arg2 > 0) /\ (undef135 > 1) /\ (undef136 > 1) /\ (undef137 > ~(1)) /\ ((arg3 + 2) <= arg1), par{arg1 -> undef135, arg2 -> undef136, arg3 -> undef137, arg4 -> undef138, arg5 -> arg3}>
<l13, l14, (undef141 <= arg1) /\ (arg1 > 2) /\ (arg2 > 0) /\ (undef140 > 2) /\ (undef141 > 1) /\ ((arg3 + 2) <= arg1), par{arg1 -> undef140, arg2 -> undef141, arg3 -> undef142, arg4 -> undef143, arg5 -> arg3}>
<l13, l14, (undef146 <= arg1) /\ (arg1 > 2) /\ (arg2 > 0) /\ (undef145 > 4) /\ (undef146 > 1) /\ ((arg3 + 2) <= arg1), par{arg1 -> undef145, arg2 -> undef146, arg3 -> undef147, arg4 -> undef148, arg5 -> arg3}>
<l14, l10, (undef150 <= arg1) /\ (undef151 <= arg2) /\ (arg1 > 2) /\ (arg2 > 1) /\ (undef150 > 2) /\ (undef151 > 1) /\ (undef152 > ~(1)) /\ ((arg3 + 4) <= arg1) /\ ((arg4 + 2) <= arg1) /\ ((arg5 + 2) <= arg2), par{arg1 -> undef150, arg2 -> undef151, arg3 -> undef152}>
<l15, l1, true, par{arg1 -> undef155, arg2 -> undef156, arg3 -> undef157, arg4 -> undef158, arg5 -> undef159}>

Fresh variables:
undef1, undef2, undef3, undef4, undef5, undef6, undef7, undef10, undef11, undef12, undef13, undef14, undef16, undef17, undef18, undef19, undef21, undef22, undef24, undef25, undef26, undef29, undef30, undef31, undef32, undef34, undef35, undef36, undef39, undef40, undef41, undef44, undef45, undef46, undef49, undef50, undef51, undef54, undef55, undef56, undef59, undef60, undef61, undef62, undef63, undef64, undef65, undef66, undef67, undef68, undef69, undef70, undef71, undef72, undef73, undef74, undef75, undef76, undef77, undef80, undef81, undef82, undef85, undef86, undef87, undef88, undef90, undef91, undef93, undef94, undef95, undef96, undef98, undef99, undef100, undef101, undef102, undef103, undef104, undef105, undef106, undef108, undef109, undef110, undef111, undef113, undef114, undef115, undef116, undef117, undef118, undef119, undef120, undef121, undef123, undef124, undef125, undef126, undef128, undef129, undef130, undef131, undef132, undef133, undef134, undef135, undef136, undef137, undef138, undef140, undef141, undef142, undef143, undef145, undef146, undef147, undef148, undef150, undef151, undef152, undef155, undef156, undef157, undef158, undef159, 

Undef variables:
undef1, undef2, undef3, undef4, undef5, undef6, undef7, undef10, undef11, undef12, undef13, undef14, undef16, undef17, undef18, undef19, undef21, undef22, undef24, undef25, undef26, undef29, undef30, undef31, undef32, undef34, undef35, undef36, undef39, undef40, undef41, undef44, undef45, undef46, undef49, undef50, undef51, undef54, undef55, undef56, undef59, undef60, undef61, undef62, undef63, undef64, undef65, undef66, undef67, undef68, undef69, undef70, undef71, undef72, undef73, undef74, undef75, undef76, undef77, undef80, undef81, undef82, undef85, undef86, undef87, undef88, undef90, undef91, undef93, undef94, undef95, undef96, undef98, undef99, undef100, undef101, undef102, undef103, undef104, undef105, undef106, undef108, undef109, undef110, undef111, undef113, undef114, undef115, undef116, undef117, undef118, undef119, undef120, undef121, undef123, undef124, undef125, undef126, undef128, undef129, undef130, undef131, undef132, undef133, undef134, undef135, undef136, undef137, undef138, undef140, undef141, undef142, undef143, undef145, undef146, undef147, undef148, undef150, undef151, undef152, undef155, undef156, undef157, undef158, undef159, 

Abstraction variables:

Exit nodes:

Accepting locations:

Asserts:

Preprocessed LLVMGraph
Init Location: 0
Transitions:
<l0, l2, (undef2 > 6) /\ (undef1 > 9), par{arg1 -> undef1, arg2 -> undef2, arg3 -> undef3, arg4 -> undef4, arg5 -> undef5}>
<l0, l13, (undef7 > 6) /\ (undef6 > 4) /\ (undef6 > 0) /\ (undef7 > 2) /\ (undef26 > 9) /\ ((3 + 2) <= undef6) /\ ((1 + 2) <= undef7) /\ ((3 + 4) <= undef7) /\ (undef51 <= undef26) /\ (undef26 > 6) /\ (undef51 > 6) /\ ((6 + 4) <= undef26) /\ (5 = 5) /\ (undef125 <= undef51) /\ (undef51 > 6) /\ (undef125 > 6) /\ (undef126 > ~(1)) /\ ((6 + 4) <= undef51) /\ (5 = 5), par{arg1 -> undef125, arg2 -> undef126, arg3 -> 5, arg4 -> undef128, arg5 -> undef129}>
<l0, l13, (undef7 > 6) /\ (undef6 > 4) /\ (undef6 > 0) /\ (undef7 > 2) /\ (undef26 > 9) /\ ((3 + 2) <= undef6) /\ ((1 + 2) <= undef7) /\ ((3 + 4) <= undef7) /\ (undef56 <= undef26) /\ (undef26 > 6) /\ (undef56 > 6) /\ ((6 + 4) <= undef26) /\ (5 = 5) /\ (undef125 <= undef56) /\ (undef56 > 6) /\ (undef125 > 6) /\ (undef126 > ~(1)) /\ ((6 + 4) <= undef56) /\ (5 = 5), par{arg1 -> undef125, arg2 -> undef126, arg3 -> 5, arg4 -> undef128, arg5 -> undef129}>
<l0, l11, (undef7 > 6) /\ (undef6 > 4) /\ (undef6 > 0) /\ (undef7 > 2) /\ (undef26 > 9) /\ ((3 + 2) <= undef6) /\ ((1 + 2) <= undef7) /\ ((3 + 4) <= undef7) /\ (undef95 <= undef26) /\ (undef26 > 6) /\ (undef95 > 6) /\ (undef96 > ~(1)) /\ ((6 + 4) <= undef26) /\ (5 = 5), par{arg1 -> undef95, arg2 -> undef96, arg3 -> 5, arg4 -> undef98, arg5 -> undef99}>
<l0, l12, (undef7 > 6) /\ (undef6 > 4) /\ (undef6 > 0) /\ (undef7 > 2) /\ (undef26 > 9) /\ ((3 + 2) <= undef6) /\ ((1 + 2) <= undef7) /\ ((3 + 4) <= undef7) /\ (undef110 <= undef26) /\ (undef26 > 6) /\ (undef110 > 6) /\ (undef111 > ~(1)) /\ ((6 + 4) <= undef26) /\ (5 = 5), par{arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114}>
<l0, l13, (undef7 > 6) /\ (undef6 > 4) /\ ((undef36 - 9) <= undef6) /\ ((undef36 - 7) <= undef7) /\ (undef6 > 0) /\ (undef7 > 2) /\ (undef36 > 9) /\ ((3 + 2) <= undef6) /\ ((1 + 2) <= undef7) /\ ((3 + 4) <= undef7) /\ (undef51 <= undef36) /\ (undef36 > 6) /\ (undef51 > 6) /\ ((6 + 4) <= undef36) /\ (5 = 5) /\ (undef125 <= undef51) /\ (undef51 > 6) /\ (undef125 > 6) /\ (undef126 > ~(1)) /\ ((6 + 4) <= undef51) /\ (5 = 5), par{arg1 -> undef125, arg2 -> undef126, arg3 -> 5, arg4 -> undef128, arg5 -> undef129}>
<l0, l13, (undef7 > 6) /\ (undef6 > 4) /\ ((undef36 - 9) <= undef6) /\ ((undef36 - 7) <= undef7) /\ (undef6 > 0) /\ (undef7 > 2) /\ (undef36 > 9) /\ ((3 + 2) <= undef6) /\ ((1 + 2) <= undef7) /\ ((3 + 4) <= undef7) /\ (undef56 <= undef36) /\ (undef36 > 6) /\ (undef56 > 6) /\ ((6 + 4) <= undef36) /\ (5 = 5) /\ (undef125 <= undef56) /\ (undef56 > 6) /\ (undef125 > 6) /\ (undef126 > ~(1)) /\ ((6 + 4) <= undef56) /\ (5 = 5), par{arg1 -> undef125, arg2 -> undef126, arg3 -> 5, arg4 -> undef128, arg5 -> undef129}>
<l0, l11, (undef7 > 6) /\ (undef6 > 4) /\ ((undef36 - 9) <= undef6) /\ ((undef36 - 7) <= undef7) /\ (undef6 > 0) /\ (undef7 > 2) /\ (undef36 > 9) /\ ((3 + 2) <= undef6) /\ ((1 + 2) <= undef7) /\ ((3 + 4) <= undef7) /\ (undef95 <= undef36) /\ (undef36 > 6) /\ (undef95 > 6) /\ (undef96 > ~(1)) /\ ((6 + 4) <= undef36) /\ (5 = 5), par{arg1 -> undef95, arg2 -> undef96, arg3 -> 5, arg4 -> undef98, arg5 -> undef99}>
<l0, l12, (undef7 > 6) /\ (undef6 > 4) /\ ((undef36 - 9) <= undef6) /\ ((undef36 - 7) <= undef7) /\ (undef6 > 0) /\ (undef7 > 2) /\ (undef36 > 9) /\ ((3 + 2) <= undef6) /\ ((1 + 2) <= undef7) /\ ((3 + 4) <= undef7) /\ (undef110 <= undef36) /\ (undef36 > 6) /\ (undef110 > 6) /\ (undef111 > ~(1)) /\ ((6 + 4) <= undef36) /\ (5 = 5), par{arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114}>
<l0, l10, (undef7 > 6) /\ (undef6 > 4) /\ ((undef81 - 2) <= undef7) /\ (undef6 > 0) /\ (undef7 > 2) /\ (undef80 > 9) /\ (undef81 > 4) /\ (undef82 > ~(1)) /\ ((3 + 2) <= undef6) /\ ((1 + 2) <= undef7) /\ ((3 + 4) <= undef7), par{arg1 -> undef80, arg2 -> undef81, arg3 -> undef82, arg4 -> 5, arg5 -> 1}>
<l0, l13, (undef12 > 6) /\ (undef11 > 6) /\ (undef11 > 6) /\ (undef12 > 6) /\ (undef21 > 6) /\ ((undef13 + 2) <= undef11) /\ ((undef14 + 2) <= undef12) /\ (5 = 5) /\ (undef51 <= undef21) /\ (undef21 > 6) /\ (undef51 > 6) /\ ((undef22 + 4) <= undef21) /\ (5 = 5) /\ (undef125 <= undef51) /\ (undef51 > 6) /\ (undef125 > 6) /\ (undef126 > ~(1)) /\ ((undef22 + 4) <= undef51) /\ (5 = 5), par{arg1 -> undef125, arg2 -> undef126, arg3 -> 5, arg4 -> undef128, arg5 -> undef129}>
<l0, l13, (undef12 > 6) /\ (undef11 > 6) /\ (undef11 > 6) /\ (undef12 > 6) /\ (undef21 > 6) /\ ((undef13 + 2) <= undef11) /\ ((undef14 + 2) <= undef12) /\ (5 = 5) /\ (undef56 <= undef21) /\ (undef21 > 6) /\ (undef56 > 6) /\ ((undef22 + 4) <= undef21) /\ (5 = 5) /\ (undef125 <= undef56) /\ (undef56 > 6) /\ (undef125 > 6) /\ (undef126 > ~(1)) /\ ((undef22 + 4) <= undef56) /\ (5 = 5), par{arg1 -> undef125, arg2 -> undef126, arg3 -> 5, arg4 -> undef128, arg5 -> undef129}>
<l0, l11, (undef12 > 6) /\ (undef11 > 6) /\ (undef11 > 6) /\ (undef12 > 6) /\ (undef21 > 6) /\ ((undef13 + 2) <= undef11) /\ ((undef14 + 2) <= undef12) /\ (5 = 5) /\ (undef95 <= undef21) /\ (undef21 > 6) /\ (undef95 > 6) /\ (undef96 > ~(1)) /\ ((undef22 + 4) <= undef21) /\ (5 = 5), par{arg1 -> undef95, arg2 -> undef96, arg3 -> 5, arg4 -> undef98, arg5 -> undef99}>
<l0, l12, (undef12 > 6) /\ (undef11 > 6) /\ (undef11 > 6) /\ (undef12 > 6) /\ (undef21 > 6) /\ ((undef13 + 2) <= undef11) /\ ((undef14 + 2) <= undef12) /\ (5 = 5) /\ (undef110 <= undef21) /\ (undef21 > 6) /\ (undef110 > 6) /\ (undef111 > ~(1)) /\ ((undef22 + 4) <= undef21) /\ (5 = 5), par{arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114}>
<l0, l13, (undef12 > 6) /\ (undef11 > 6) /\ (undef11 > 6) /\ (undef12 > 6) /\ (undef31 > 6) /\ ((undef13 + 2) <= undef11) /\ ((undef14 + 2) <= undef12) /\ (5 = 5) /\ (undef51 <= undef31) /\ (undef31 > 6) /\ (undef51 > 6) /\ ((undef32 + 4) <= undef31) /\ (5 = 5) /\ (undef125 <= undef51) /\ (undef51 > 6) /\ (undef125 > 6) /\ (undef126 > ~(1)) /\ ((undef32 + 4) <= undef51) /\ (5 = 5), par{arg1 -> undef125, arg2 -> undef126, arg3 -> 5, arg4 -> undef128, arg5 -> undef129}>
<l0, l13, (undef12 > 6) /\ (undef11 > 6) /\ (undef11 > 6) /\ (undef12 > 6) /\ (undef31 > 6) /\ ((undef13 + 2) <= undef11) /\ ((undef14 + 2) <= undef12) /\ (5 = 5) /\ (undef56 <= undef31) /\ (undef31 > 6) /\ (undef56 > 6) /\ ((undef32 + 4) <= undef31) /\ (5 = 5) /\ (undef125 <= undef56) /\ (undef56 > 6) /\ (undef125 > 6) /\ (undef126 > ~(1)) /\ ((undef32 + 4) <= undef56) /\ (5 = 5), par{arg1 -> undef125, arg2 -> undef126, arg3 -> 5, arg4 -> undef128, arg5 -> undef129}>
<l0, l11, (undef12 > 6) /\ (undef11 > 6) /\ (undef11 > 6) /\ (undef12 > 6) /\ (undef31 > 6) /\ ((undef13 + 2) <= undef11) /\ ((undef14 + 2) <= undef12) /\ (5 = 5) /\ (undef95 <= undef31) /\ (undef31 > 6) /\ (undef95 > 6) /\ (undef96 > ~(1)) /\ ((undef32 + 4) <= undef31) /\ (5 = 5), par{arg1 -> undef95, arg2 -> undef96, arg3 -> 5, arg4 -> undef98, arg5 -> undef99}>
<l0, l12, (undef12 > 6) /\ (undef11 > 6) /\ (undef11 > 6) /\ (undef12 > 6) /\ (undef31 > 6) /\ ((undef13 + 2) <= undef11) /\ ((undef14 + 2) <= undef12) /\ (5 = 5) /\ (undef110 <= undef31) /\ (undef31 > 6) /\ (undef110 > 6) /\ (undef111 > ~(1)) /\ ((undef32 + 4) <= undef31) /\ (5 = 5), par{arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114}>
<l0, l10, (undef12 > 6) /\ (undef11 > 6) /\ (undef76 <= undef11) /\ (undef76 <= undef12) /\ (undef11 > 6) /\ (undef12 > 6) /\ (undef75 > 6) /\ (undef76 > 6) /\ (undef77 > ~(1)) /\ ((undef13 + 2) <= undef11) /\ ((undef14 + 2) <= undef12) /\ (5 = 5), par{arg1 -> undef75, arg2 -> undef76, arg3 -> undef77, arg4 -> 5, arg5 -> 1}>
<l0, l11, (undef12 > 6) /\ (undef11 > 6) /\ (undef90 <= undef11) /\ (undef90 <= undef12) /\ (undef11 > 6) /\ (undef12 > 6) /\ (undef90 > 6) /\ (undef91 > ~(1)) /\ ((undef13 + 2) <= undef11) /\ ((undef14 + 2) <= undef12) /\ (5 = 5), par{arg1 -> undef90, arg2 -> undef91, arg3 -> 5, arg4 -> undef93, arg5 -> undef94}>
<l0, l12, (undef12 > 6) /\ (undef11 > 6) /\ (undef105 <= undef11) /\ (undef105 <= undef12) /\ (undef11 > 6) /\ (undef12 > 6) /\ (undef105 > 6) /\ (undef106 > ~(1)) /\ ((undef13 + 2) <= undef11) /\ ((undef14 + 2) <= undef12) /\ (5 = 5), par{arg1 -> undef105, arg2 -> undef106, arg3 -> 5, arg4 -> undef108, arg5 -> undef109}>
<l0, l13, (undef12 > 6) /\ (undef11 > 6) /\ (undef120 <= undef11) /\ (undef120 <= undef12) /\ (undef11 > 6) /\ (undef12 > 6) /\ (undef120 > 6) /\ (undef121 > ~(1)) /\ ((undef13 + 2) <= undef11) /\ ((undef14 + 2) <= undef12) /\ (5 = 5), par{arg1 -> undef120, arg2 -> undef121, arg3 -> 5, arg4 -> undef123, arg5 -> undef124}>
<l2, l2, (undef61 <= arg1) /\ (undef66 > undef67) /\ ((undef62 + 1) <= arg2) /\ (arg1 > 0) /\ (arg2 > 0) /\ (undef61 > 0) /\ (undef62 > ~(1)), par{arg1 -> undef61, arg2 -> undef62, arg3 -> undef63, arg4 -> undef64, arg5 -> undef65}>
<l2, l2, ((undef68 + 2) <= arg1) /\ (undef73 <= undef74) /\ (undef69 <= arg2) /\ (arg1 > 2) /\ (arg2 > 0) /\ (undef68 > 0) /\ (undef69 > 0), par{arg1 -> undef68, arg2 -> undef69, arg3 -> undef70, arg4 -> undef71, arg5 -> undef72}>
<l10, l10, (undef86 <= arg2) /\ (arg1 > 2) /\ (arg2 > 0) /\ (arg3 > 0) /\ (undef85 > 0) /\ (undef86 > 0) /\ (undef87 > ~(1)) /\ ((arg4 + 2) <= arg1) /\ ((arg5 + 2) <= arg2), par{arg1 -> undef85, arg2 -> undef86, arg3 -> undef87, arg4 -> undef88}>
<l11, l11, (arg1 > 2) /\ (arg2 > 0) /\ (undef100 > 0) /\ (undef101 > ~(1)) /\ ((arg3 + 2) <= arg1), par{arg1 -> undef100, arg2 -> undef101, arg3 -> undef102, arg4 -> undef103, arg5 -> undef104}>
<l12, l12, (arg1 > 2) /\ (arg2 > 0) /\ (undef115 > 0) /\ (undef116 > ~(1)) /\ ((arg3 + 2) <= arg1), par{arg1 -> undef115, arg2 -> undef116, arg3 -> undef117, arg4 -> undef118, arg5 -> undef119}>
<l13, l13, (arg1 > 2) /\ (arg2 > 0) /\ (undef130 > 0) /\ (undef131 > ~(1)) /\ ((arg3 + 2) <= arg1), par{arg1 -> undef130, arg2 -> undef131, arg3 -> undef132, arg4 -> undef133, arg5 -> undef134}>
<l13, l10, (undef136 <= arg1) /\ (arg1 > 2) /\ (arg2 > 0) /\ (undef135 > 1) /\ (undef136 > 1) /\ (undef137 > ~(1)) /\ ((arg3 + 2) <= arg1), par{arg1 -> undef135, arg2 -> undef136, arg3 -> undef137, arg4 -> undef138, arg5 -> arg3}>
<l13, l10, (undef141 <= arg1) /\ (arg1 > 2) /\ (arg2 > 0) /\ (undef140 > 2) /\ (undef141 > 1) /\ ((arg3 + 2) <= arg1) /\ (undef150 <= undef140) /\ (undef151 <= undef141) /\ (undef140 > 2) /\ (undef141 > 1) /\ (undef150 > 2) /\ (undef151 > 1) /\ (undef152 > ~(1)) /\ ((undef142 + 4) <= undef140) /\ ((undef143 + 2) <= undef140) /\ ((arg3 + 2) <= undef141), par{arg1 -> undef150, arg2 -> undef151, arg3 -> undef152, arg4 -> undef143, arg5 -> arg3}>
<l13, l10, (undef146 <= arg1) /\ (arg1 > 2) /\ (arg2 > 0) /\ (undef145 > 4) /\ (undef146 > 1) /\ ((arg3 + 2) <= arg1) /\ (undef150 <= undef145) /\ (undef151 <= undef146) /\ (undef145 > 2) /\ (undef146 > 1) /\ (undef150 > 2) /\ (undef151 > 1) /\ (undef152 > ~(1)) /\ ((undef147 + 4) <= undef145) /\ ((undef148 + 2) <= undef145) /\ ((arg3 + 2) <= undef146), par{arg1 -> undef150, arg2 -> undef151, arg3 -> undef152, arg4 -> undef148, arg5 -> arg3}>

Fresh variables:
undef1, undef2, undef3, undef4, undef5, undef6, undef7, undef10, undef11, undef12, undef13, undef14, undef16, undef17, undef18, undef19, undef21, undef22, undef24, undef25, undef26, undef29, undef30, undef31, undef32, undef34, undef35, undef36, undef39, undef40, undef41, undef44, undef45, undef46, undef49, undef50, undef51, undef54, undef55, undef56, undef59, undef60, undef61, undef62, undef63, undef64, undef65, undef66, undef67, undef68, undef69, undef70, undef71, undef72, undef73, undef74, undef75, undef76, undef77, undef80, undef81, undef82, undef85, undef86, undef87, undef88, undef90, undef91, undef93, undef94, undef95, undef96, undef98, undef99, undef100, undef101, undef102, undef103, undef104, undef105, undef106, undef108, undef109, undef110, undef111, undef113, undef114, undef115, undef116, undef117, undef118, undef119, undef120, undef121, undef123, undef124, undef125, undef126, undef128, undef129, undef130, undef131, undef132, undef133, undef134, undef135, undef136, undef137, undef138, undef140, undef141, undef142, undef143, undef145, undef146, undef147, undef148, undef150, undef151, undef152, undef155, undef156, undef157, undef158, undef159, 

Undef variables:
undef1, undef2, undef3, undef4, undef5, undef6, undef7, undef10, undef11, undef12, undef13, undef14, undef16, undef17, undef18, undef19, undef21, undef22, undef24, undef25, undef26, undef29, undef30, undef31, undef32, undef34, undef35, undef36, undef39, undef40, undef41, undef44, undef45, undef46, undef49, undef50, undef51, undef54, undef55, undef56, undef59, undef60, undef61, undef62, undef63, undef64, undef65, undef66, undef67, undef68, undef69, undef70, undef71, undef72, undef73, undef74, undef75, undef76, undef77, undef80, undef81, undef82, undef85, undef86, undef87, undef88, undef90, undef91, undef93, undef94, undef95, undef96, undef98, undef99, undef100, undef101, undef102, undef103, undef104, undef105, undef106, undef108, undef109, undef110, undef111, undef113, undef114, undef115, undef116, undef117, undef118, undef119, undef120, undef121, undef123, undef124, undef125, undef126, undef128, undef129, undef130, undef131, undef132, undef133, undef134, undef135, undef136, undef137, undef138, undef140, undef141, undef142, undef143, undef145, undef146, undef147, undef148, undef150, undef151, undef152, undef155, undef156, undef157, undef158, undef159, 

Abstraction variables:

Exit nodes:

Accepting locations:

Asserts:

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

Init Location: 0
Graph 0:
Transitions:
Variables:

Graph 1:
Transitions:
<l12, l12, 3 <= arg1 /\ 1 <= arg2 /\ 1 <= undef115 /\ 2 + arg3 <= arg1 /\ 0 <= undef116, {arg1 -> undef115, arg2 -> undef116, arg3 -> undef117, arg4 -> undef118, arg5 -> undef119, rest remain the same}>
Variables:
arg1, arg2, arg3, arg4, arg5

Graph 2:
Transitions:
<l11, l11, 3 <= arg1 /\ 1 <= arg2 /\ 1 <= undef100 /\ 2 + arg3 <= arg1 /\ 0 <= undef101, {arg1 -> undef100, arg2 -> undef101, arg3 -> undef102, arg4 -> undef103, arg5 -> undef104, rest remain the same}>
Variables:
arg1, arg2, arg3, arg4, arg5

Graph 3:
Transitions:
<l13, l13, 3 <= arg1 /\ 1 <= arg2 /\ 1 <= undef130 /\ 2 + arg3 <= arg1 /\ 0 <= undef131, {arg1 -> undef130, arg2 -> undef131, arg3 -> undef132, arg4 -> undef133, arg5 -> undef134, rest remain the same}>
Variables:
arg1, arg2, arg3, arg4, arg5

Graph 4:
Transitions:
<l10, l10, 3 <= arg1 /\ 1 <= arg2 /\ 1 <= arg3 /\ 1 <= undef85 /\ 1 <= undef86 /\ 2 + arg4 <= arg1 /\ 2 + arg5 <= arg2 /\ undef86 <= arg2 /\ 0 <= undef87, {arg1 -> undef85, arg2 -> undef86, arg3 -> undef87, arg4 -> undef88, rest remain the same}>
Variables:
arg1, arg2, arg3, arg4, arg5

Graph 5:
Transitions:
<l2, l2, 1 <= arg1 /\ 1 <= arg2 /\ 1 + undef62 <= arg2 /\ 1 <= undef61 /\ 1 + undef67 <= undef66 /\ undef61 <= arg1 /\ 0 <= undef62, {arg1 -> undef61, arg2 -> undef62, arg3 -> undef63, arg4 -> undef64, arg5 -> undef65, rest remain the same}>
<l2, l2, 3 <= arg1 /\ 1 <= arg2 /\ 1 <= undef68 /\ 1 <= undef69 /\ 2 + undef68 <= arg1 /\ undef69 <= arg2 /\ undef73 <= undef74, {arg1 -> undef68, arg2 -> undef69, arg3 -> undef70, arg4 -> undef71, arg5 -> undef72, rest remain the same}>
Variables:
arg1, arg2, arg3, arg4, arg5

Precedence: 
Graph 0

Graph 1
<l0, l12, 5 <= undef6 /\ undef110 <= undef26 /\ 0 <= undef111 /\ 7 <= undef7 /\ 7 <= undef110 /\ 10 <= undef26, {arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114, rest remain the same}>
<l0, l12, 5 <= undef6 /\ undef110 <= undef36 /\ 0 <= undef111 /\ 7 <= undef7 /\ 7 <= undef110 /\ undef36 <= 9 + undef6 /\ undef36 <= 7 + undef7 /\ 10 <= undef36, {arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114, rest remain the same}>
<l0, l12, 4 + undef22 <= undef21 /\ 2 + undef13 <= undef11 /\ 2 + undef14 <= undef12 /\ undef110 <= undef21 /\ 0 <= undef111 /\ 7 <= undef11 /\ 7 <= undef12 /\ 7 <= undef21 /\ 7 <= undef110, {arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114, rest remain the same}>
<l0, l12, 4 + undef32 <= undef31 /\ 2 + undef13 <= undef11 /\ 2 + undef14 <= undef12 /\ undef110 <= undef31 /\ 0 <= undef111 /\ 7 <= undef11 /\ 7 <= undef12 /\ 7 <= undef31 /\ 7 <= undef110, {arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114, rest remain the same}>
<l0, l12, 2 + undef13 <= undef11 /\ 2 + undef14 <= undef12 /\ undef105 <= undef11 /\ undef105 <= undef12 /\ 0 <= undef106 /\ 7 <= undef11 /\ 7 <= undef12 /\ 7 <= undef105, {arg1 -> undef105, arg2 -> undef106, arg3 -> 5, arg4 -> undef108, arg5 -> undef109, rest remain the same}>

Graph 2
<l0, l11, 5 <= undef6 /\ undef95 <= undef26 /\ 0 <= undef96 /\ 7 <= undef7 /\ 7 <= undef95 /\ 10 <= undef26, {arg1 -> undef95, arg2 -> undef96, arg3 -> 5, arg4 -> undef98, arg5 -> undef99, rest remain the same}>
<l0, l11, 5 <= undef6 /\ undef95 <= undef36 /\ 0 <= undef96 /\ 7 <= undef7 /\ 7 <= undef95 /\ undef36 <= 9 + undef6 /\ undef36 <= 7 + undef7 /\ 10 <= undef36, {arg1 -> undef95, arg2 -> undef96, arg3 -> 5, arg4 -> undef98, arg5 -> undef99, rest remain the same}>
<l0, l11, 4 + undef22 <= undef21 /\ 2 + undef13 <= undef11 /\ 2 + undef14 <= undef12 /\ undef95 <= undef21 /\ 0 <= undef96 /\ 7 <= undef11 /\ 7 <= undef12 /\ 7 <= undef21 /\ 7 <= undef95, {arg1 -> undef95, arg2 -> undef96, arg3 -> 5, arg4 -> undef98, arg5 -> undef99, rest remain the same}>
<l0, l11, 4 + undef32 <= undef31 /\ 2 + undef13 <= undef11 /\ 2 + undef14 <= undef12 /\ undef95 <= undef31 /\ 0 <= undef96 /\ 7 <= undef11 /\ 7 <= undef12 /\ 7 <= undef31 /\ 7 <= undef95, {arg1 -> undef95, arg2 -> undef96, arg3 -> 5, arg4 -> undef98, arg5 -> undef99, rest remain the same}>
<l0, l11, 2 + undef13 <= undef11 /\ 2 + undef14 <= undef12 /\ undef90 <= undef11 /\ undef90 <= undef12 /\ 0 <= undef91 /\ 7 <= undef11 /\ 7 <= undef12 /\ 7 <= undef90, {arg1 -> undef90, arg2 -> undef91, arg3 -> 5, arg4 -> undef93, arg5 -> undef94, rest remain the same}>

Graph 3
<l0, l13, 5 <= undef6 /\ undef51 <= undef26 /\ undef125 <= undef51 /\ 0 <= undef126 /\ 7 <= undef7 /\ 7 <= undef125 /\ 10 <= undef26 /\ 10 <= undef51, {arg1 -> undef125, arg2 -> undef126, arg3 -> 5, arg4 -> undef128, arg5 -> undef129, rest remain the same}>
<l0, l13, 5 <= undef6 /\ undef56 <= undef26 /\ undef125 <= undef56 /\ 0 <= undef126 /\ 7 <= undef7 /\ 7 <= undef125 /\ 10 <= undef26 /\ 10 <= undef56, {arg1 -> undef125, arg2 -> undef126, arg3 -> 5, arg4 -> undef128, arg5 -> undef129, rest remain the same}>
<l0, l13, 5 <= undef6 /\ undef51 <= undef36 /\ undef125 <= undef51 /\ 0 <= undef126 /\ 7 <= undef7 /\ 7 <= undef125 /\ undef36 <= 9 + undef6 /\ undef36 <= 7 + undef7 /\ 10 <= undef36 /\ 10 <= undef51, {arg1 -> undef125, arg2 -> undef126, arg3 -> 5, arg4 -> undef128, arg5 -> undef129, rest remain the same}>
<l0, l13, 5 <= undef6 /\ undef56 <= undef36 /\ undef125 <= undef56 /\ 0 <= undef126 /\ 7 <= undef7 /\ 7 <= undef125 /\ undef36 <= 9 + undef6 /\ undef36 <= 7 + undef7 /\ 10 <= undef36 /\ 10 <= undef56, {arg1 -> undef125, arg2 -> undef126, arg3 -> 5, arg4 -> undef128, arg5 -> undef129, rest remain the same}>
<l0, l13, 4 + undef22 <= undef21 /\ 4 + undef22 <= undef51 /\ 2 + undef13 <= undef11 /\ 2 + undef14 <= undef12 /\ undef51 <= undef21 /\ undef125 <= undef51 /\ 0 <= undef126 /\ 7 <= undef11 /\ 7 <= undef12 /\ 7 <= undef21 /\ 7 <= undef51 /\ 7 <= undef125, {arg1 -> undef125, arg2 -> undef126, arg3 -> 5, arg4 -> undef128, arg5 -> undef129, rest remain the same}>
<l0, l13, 4 + undef22 <= undef21 /\ 4 + undef22 <= undef56 /\ 2 + undef13 <= undef11 /\ 2 + undef14 <= undef12 /\ undef56 <= undef21 /\ undef125 <= undef56 /\ 0 <= undef126 /\ 7 <= undef11 /\ 7 <= undef12 /\ 7 <= undef21 /\ 7 <= undef56 /\ 7 <= undef125, {arg1 -> undef125, arg2 -> undef126, arg3 -> 5, arg4 -> undef128, arg5 -> undef129, rest remain the same}>
<l0, l13, 4 + undef32 <= undef31 /\ 4 + undef32 <= undef51 /\ 2 + undef13 <= undef11 /\ 2 + undef14 <= undef12 /\ undef51 <= undef31 /\ undef125 <= undef51 /\ 0 <= undef126 /\ 7 <= undef11 /\ 7 <= undef12 /\ 7 <= undef31 /\ 7 <= undef51 /\ 7 <= undef125, {arg1 -> undef125, arg2 -> undef126, arg3 -> 5, arg4 -> undef128, arg5 -> undef129, rest remain the same}>
<l0, l13, 4 + undef32 <= undef31 /\ 4 + undef32 <= undef56 /\ 2 + undef13 <= undef11 /\ 2 + undef14 <= undef12 /\ undef56 <= undef31 /\ undef125 <= undef56 /\ 0 <= undef126 /\ 7 <= undef11 /\ 7 <= undef12 /\ 7 <= undef31 /\ 7 <= undef56 /\ 7 <= undef125, {arg1 -> undef125, arg2 -> undef126, arg3 -> 5, arg4 -> undef128, arg5 -> undef129, rest remain the same}>
<l0, l13, 2 + undef13 <= undef11 /\ 2 + undef14 <= undef12 /\ undef120 <= undef11 /\ undef120 <= undef12 /\ 0 <= undef121 /\ 7 <= undef11 /\ 7 <= undef12 /\ 7 <= undef120, {arg1 -> undef120, arg2 -> undef121, arg3 -> 5, arg4 -> undef123, arg5 -> undef124, rest remain the same}>

Graph 4
<l0, l10, 5 <= undef6 /\ 5 <= undef81 /\ 0 <= undef82 /\ 7 <= undef7 /\ undef81 <= 2 + undef7 /\ 10 <= undef80, {arg1 -> undef80, arg2 -> undef81, arg3 -> undef82, arg4 -> 5, arg5 -> 1, rest remain the same}>
<l0, l10, 2 + undef13 <= undef11 /\ 2 + undef14 <= undef12 /\ undef76 <= undef11 /\ undef76 <= undef12 /\ 0 <= undef77 /\ 7 <= undef11 /\ 7 <= undef12 /\ 7 <= undef75 /\ 7 <= undef76, {arg1 -> undef75, arg2 -> undef76, arg3 -> undef77, arg4 -> 5, arg5 -> 1, rest remain the same}>
<l13, l10, 3 <= arg1 /\ 1 <= arg2 /\ 2 + arg3 <= arg1 /\ 2 <= undef135 /\ 2 <= undef136 /\ undef136 <= arg1 /\ 0 <= undef137, {arg1 -> undef135, arg2 -> undef136, arg3 -> undef137, arg4 -> undef138, arg5 -> arg3, rest remain the same}>
<l13, l10, 4 + undef142 <= undef140 /\ 3 <= arg1 /\ 3 <= undef140 /\ 3 <= undef150 /\ 1 <= arg2 /\ 2 + arg3 <= arg1 /\ 2 + arg3 <= undef141 /\ 2 + undef143 <= undef140 /\ 2 <= undef141 /\ 2 <= undef151 /\ undef141 <= arg1 /\ undef150 <= undef140 /\ undef151 <= undef141 /\ 0 <= undef152, {arg1 -> undef150, arg2 -> undef151, arg3 -> undef152, arg4 -> undef143, arg5 -> arg3, rest remain the same}>
<l13, l10, 4 + undef147 <= undef145 /\ 3 <= arg1 /\ 3 <= undef150 /\ 1 <= arg2 /\ 5 <= undef145 /\ 2 + arg3 <= arg1 /\ 2 + arg3 <= undef146 /\ 2 + undef148 <= undef145 /\ 2 <= undef146 /\ 2 <= undef151 /\ undef146 <= arg1 /\ undef150 <= undef145 /\ undef151 <= undef146 /\ 0 <= undef152, {arg1 -> undef150, arg2 -> undef151, arg3 -> undef152, arg4 -> undef148, arg5 -> arg3, rest remain the same}>

Graph 5
<l0, l2, 7 <= undef2 /\ 10 <= undef1, {arg1 -> undef1, arg2 -> undef2, arg3 -> undef3, arg4 -> undef4, arg5 -> undef5, rest remain the same}>

Map Locations to Subgraph:
( 0 , 0 )
( 2 , 5 )
( 10 , 4 )
( 11 , 2 )
( 12 , 1 )
( 13 , 3 )

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

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

Checking conditional termination of SCC {l12}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000584s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001866s
Trying to remove transition: <l12, l12, 3 <= arg1 /\ 1 <= arg2 /\ 1 <= undef115 /\ 2 + arg3 <= arg1 /\ 0 <= undef116, {arg1 -> undef115, arg2 -> undef116, arg3 -> undef117, arg4 -> undef118, arg5 -> undef119, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.019397s
Time used: 0.019395

LOG: SAT solveNonLinear - Elapsed time: 0.033167s
Cost: 5; Total time: 0.032669
Failed at location 12: arg2 <= 0
Failed at location 12: arg2 <= 0
Failed at location 12: arg2 <= 0
Failed at location 12: arg2 <= 0
Failed at location 12: arg2 <= 0
Before Improving: 
Quasi-invariant at l12: arg2 <= 0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002094s
Remaining time after improvement: 0.998954
Termination implied by a set of quasi-invariant(s):
Quasi-invariant at l12: arg2 <= 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: 
<l12, l12, 3 <= arg1 /\ 1 <= arg2 /\ 1 <= undef115 /\ 2 + arg3 <= arg1 /\ 0 <= undef116, {arg1 -> undef115, arg2 -> undef116, arg3 -> undef117, arg4 -> undef118, arg5 -> undef119, 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: 
<l12, l12, 3 <= arg1 /\ 1 <= arg2 /\ 1 <= undef115 /\ 2 + arg3 <= arg1 /\ 0 <= undef116, {arg1 -> undef115, arg2 -> undef116, arg3 -> undef117, arg4 -> undef118, arg5 -> undef119, rest remain the same}>
New Graphs: 
Calling Safety with literal arg2 <= 0 and entry <l0, l12, 5 <= undef6 /\ undef110 <= undef26 /\ 0 <= undef111 /\ 7 <= undef7 /\ 7 <= undef110 /\ 10 <= undef26, {arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114, rest remain the same}>

LOG: CALL check - Post:arg2 <= 0 - Process 1
* Exit transition: <l0, l12, 5 <= undef6 /\ undef110 <= undef26 /\ 0 <= undef111 /\ 7 <= undef7 /\ 7 <= undef110 /\ 10 <= undef26, {arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114, rest remain the same}>
* Postcondition  : arg2 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.000450s
Calling Safety with literal arg2 <= 0 and entry <l0, l12, 5 <= undef6 /\ undef110 <= undef36 /\ 0 <= undef111 /\ 7 <= undef7 /\ 7 <= undef110 /\ undef36 <= 9 + undef6 /\ undef36 <= 7 + undef7 /\ 10 <= undef36, {arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114, rest remain the same}>

LOG: CALL check - Post:arg2 <= 0 - Process 2
* Exit transition: <l0, l12, 5 <= undef6 /\ undef110 <= undef36 /\ 0 <= undef111 /\ 7 <= undef7 /\ 7 <= undef110 /\ undef36 <= 9 + undef6 /\ undef36 <= 7 + undef7 /\ 10 <= undef36, {arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114, rest remain the same}>
* Postcondition  : arg2 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.000491s
Calling Safety with literal arg2 <= 0 and entry <l0, l12, 4 + undef22 <= undef21 /\ 2 + undef13 <= undef11 /\ 2 + undef14 <= undef12 /\ undef110 <= undef21 /\ 0 <= undef111 /\ 7 <= undef11 /\ 7 <= undef12 /\ 7 <= undef21 /\ 7 <= undef110, {arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114, rest remain the same}>

LOG: CALL check - Post:arg2 <= 0 - Process 3
* Exit transition: <l0, l12, 4 + undef22 <= undef21 /\ 2 + undef13 <= undef11 /\ 2 + undef14 <= undef12 /\ undef110 <= undef21 /\ 0 <= undef111 /\ 7 <= undef11 /\ 7 <= undef12 /\ 7 <= undef21 /\ 7 <= undef110, {arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114, rest remain the same}>
* Postcondition  : arg2 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.000465s
Calling Safety with literal arg2 <= 0 and entry <l0, l12, 4 + undef32 <= undef31 /\ 2 + undef13 <= undef11 /\ 2 + undef14 <= undef12 /\ undef110 <= undef31 /\ 0 <= undef111 /\ 7 <= undef11 /\ 7 <= undef12 /\ 7 <= undef31 /\ 7 <= undef110, {arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114, rest remain the same}>

LOG: CALL check - Post:arg2 <= 0 - Process 4
* Exit transition: <l0, l12, 4 + undef32 <= undef31 /\ 2 + undef13 <= undef11 /\ 2 + undef14 <= undef12 /\ undef110 <= undef31 /\ 0 <= undef111 /\ 7 <= undef11 /\ 7 <= undef12 /\ 7 <= undef31 /\ 7 <= undef110, {arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114, rest remain the same}>
* Postcondition  : arg2 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.000465s
Calling Safety with literal arg2 <= 0 and entry <l0, l12, 2 + undef13 <= undef11 /\ 2 + undef14 <= undef12 /\ undef105 <= undef11 /\ undef105 <= undef12 /\ 0 <= undef106 /\ 7 <= undef11 /\ 7 <= undef12 /\ 7 <= undef105, {arg1 -> undef105, arg2 -> undef106, arg3 -> 5, arg4 -> undef108, arg5 -> undef109, rest remain the same}>

LOG: CALL check - Post:arg2 <= 0 - Process 5
* Exit transition: <l0, l12, 2 + undef13 <= undef11 /\ 2 + undef14 <= undef12 /\ undef105 <= undef11 /\ undef105 <= undef12 /\ 0 <= undef106 /\ 7 <= undef11 /\ 7 <= undef12 /\ 7 <= undef105, {arg1 -> undef105, arg2 -> undef106, arg3 -> 5, arg4 -> undef108, arg5 -> undef109, rest remain the same}>
* Postcondition  : arg2 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.000437s
INVARIANTS: 
12: 
Quasi-INVARIANTS to narrow Graph: 
12: arg2 <= 0 , 
Narrowing transition: 
<l12, l12, 3 <= arg1 /\ 1 <= arg2 /\ 1 <= undef115 /\ 2 + arg3 <= arg1 /\ 0 <= undef116, {arg1 -> undef115, arg2 -> undef116, arg3 -> undef117, arg4 -> undef118, arg5 -> undef119, rest remain the same}>

LOG: Narrow transition size 1
invGraph after Narrowing: 
Transitions:
<l12, l12, 3 <= arg1 /\ 1 <= arg2 /\ 1 <= undef115 /\ 2 + arg3 <= arg1 /\ 0 <= undef116, {arg1 -> undef115, arg2 -> undef116, arg3 -> undef117, arg4 -> undef118, arg5 -> undef119, rest remain the same}>
Variables:
arg1, arg2, arg3, arg4, arg5
Checking conditional termination of SCC {l12}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000460s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001865s
Trying to remove transition: <l12, l12, 3 <= arg1 /\ 1 <= arg2 /\ 1 <= undef115 /\ 2 + arg3 <= arg1 /\ 0 <= undef116, {arg1 -> undef115, arg2 -> undef116, arg3 -> undef117, arg4 -> undef118, arg5 -> undef119, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.015679s
Time used: 0.007024

Proving non-termination of subgraph 1
Transitions:
<l12, l12, 3 <= arg1 /\ 1 <= arg2 /\ 1 <= undef115 /\ 2 + arg3 <= arg1 /\ 0 <= undef116, {arg1 -> undef115, arg2 -> undef116, arg3 -> undef117, arg4 -> undef118, arg5 -> undef119, rest remain the same}>
Variables:
arg1, arg2, arg3, arg4, arg5

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

Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.034227s
Time used: 0.034019
Improving Solution with cost 9 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.143840s
Time used: 0.143837
Improving Solution with cost 3 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.046935s
Time used: 0.046932

LOG: SAT solveNonLinear - Elapsed time: 0.225002s
Cost: 3; Total time: 0.224788
Minimizing number of undef constraints...

LOG: CALL solveNonLinear

LOG: RETURN solveNonLinear - Elapsed time: 0.004088s
Non-termination implied by a set of quasi-invariant(s):
Quasi-invariant at l12: 4 <= arg1
Constraint over undef '11 <= undef115' in transition:
<l12, l12, 3 <= arg1 /\ 1 <= arg2 /\ 1 <= undef115 /\ 2 + arg3 <= arg1 /\ 0 <= undef116, {arg1 -> undef115, arg2 -> undef116, arg3 -> undef117, arg4 -> undef118, arg5 -> undef119, rest remain the same}>

Strengthening and disabling EXIT transitions...
Closed exits from l12: 1
Strengthening exit transition (result): 
<l12, end, 4 <= arg1 /\ 1 <= arg2 /\ arg1 <= 1 + arg3, {all remain the same}>
Strengthening exit transition (result): 
<l12, end, 4 <= arg1 /\ arg2 <= 0, {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): 
<l12, l12, 4 <= arg1 /\ 1 <= arg2 /\ 2 + arg3 <= arg1 /\ 0 <= undef116 /\ 11 <= undef115, {arg1 -> undef115, arg2 -> undef116, arg3 -> undef117, arg4 -> undef118, arg5 -> undef119, rest remain the same}>

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

Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.033830s
Time used: 0.033654
Improving Solution with cost 6 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.095715s
Time used: 0.095712
Improving Solution with cost 2 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.039847s
Time used: 0.039845

LOG: SAT solveNonLinear - Elapsed time: 0.169393s
Cost: 2; Total time: 0.169211
Minimizing number of undef constraints...

LOG: CALL solveNonLinear

LOG: RETURN solveNonLinear - Elapsed time: 0.004188s
Non-termination implied by a set of quasi-invariant(s):
Quasi-invariant at l12: 2 + arg3 <= arg1
Constraint over undef '12 + undef117 <= 0' in transition:
<l12, l12, 4 <= arg1 /\ 1 <= arg2 /\ 2 + arg3 <= arg1 /\ 0 <= undef116 /\ 11 <= undef115, {arg1 -> undef115, arg2 -> undef116, arg3 -> undef117, arg4 -> undef118, arg5 -> undef119, rest remain the same}>

Strengthening and disabling EXIT transitions...
Closed exits from l12: 1
Strengthening exit transition (result): 
<l12, end, 4 <= arg1 /\ 2 + arg3 <= arg1 /\ arg2 <= 0, {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): 
<l12, l12, 4 <= arg1 /\ 1 <= arg2 /\ 2 + arg3 <= arg1 /\ 0 <= undef116 /\ 11 <= undef115 /\ 12 + undef117 <= 0, {arg1 -> undef115, arg2 -> undef116, arg3 -> undef117, arg4 -> undef118, arg5 -> undef119, rest remain the same}>

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

Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.055036s
Time used: 0.055033

LOG: SAT solveNonLinear - Elapsed time: 0.074968s
Cost: 5; Total time: 0.074777
Failed at location 12: 1 <= arg2
Failed at location 12: 1 <= arg2
Failed at location 12: 1 <= arg2
Failed at location 12: 1 <= arg2
Failed at location 12: 1 <= arg2
Before Improving: 
Quasi-invariant at l12: 1 <= arg2
Optimizing invariants...

LOG: CALL solveLinear

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

LOG: CALL solveNonLinear

LOG: RETURN solveNonLinear - Elapsed time: 0.002267s
Non-termination implied by a set of quasi-invariant(s):
Quasi-invariant at l12: 1 <= arg2
Constraint over undef '1 <= undef116' in transition:
<l12, l12, 4 <= arg1 /\ 1 <= arg2 /\ 2 + arg3 <= arg1 /\ 0 <= undef116 /\ 11 <= undef115 /\ 12 + undef117 <= 0, {arg1 -> undef115, arg2 -> undef116, arg3 -> undef117, arg4 -> undef118, arg5 -> undef119, rest remain the same}>

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

Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l12, l12, 4 <= arg1 /\ 1 <= arg2 /\ 1 <= undef116 /\ 2 + arg3 <= arg1 /\ 11 <= undef115 /\ 12 + undef117 <= 0, {arg1 -> undef115, arg2 -> undef116, arg3 -> undef117, arg4 -> undef118, arg5 -> undef119, rest remain the same}>

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

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

Calling reachability with...
Transition: <l0, l12, 5 <= undef6 /\ undef110 <= undef26 /\ 0 <= undef111 /\ 7 <= undef7 /\ 7 <= undef110 /\ 10 <= undef26, {arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114, rest remain the same}>
Conditions: 4 <= arg1, 1 <= arg2, 2 + arg3 <= arg1, 
Transition: <l0, l12, 5 <= undef6 /\ undef110 <= undef36 /\ 0 <= undef111 /\ 7 <= undef7 /\ 7 <= undef110 /\ undef36 <= 9 + undef6 /\ undef36 <= 7 + undef7 /\ 10 <= undef36, {arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114, rest remain the same}>
Conditions: 4 <= arg1, 1 <= arg2, 2 + arg3 <= arg1, 
Transition: <l0, l12, 4 + undef22 <= undef21 /\ 2 + undef13 <= undef11 /\ 2 + undef14 <= undef12 /\ undef110 <= undef21 /\ 0 <= undef111 /\ 7 <= undef11 /\ 7 <= undef12 /\ 7 <= undef21 /\ 7 <= undef110, {arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114, rest remain the same}>
Conditions: 4 <= arg1, 1 <= arg2, 2 + arg3 <= arg1, 
Transition: <l0, l12, 4 + undef32 <= undef31 /\ 2 + undef13 <= undef11 /\ 2 + undef14 <= undef12 /\ undef110 <= undef31 /\ 0 <= undef111 /\ 7 <= undef11 /\ 7 <= undef12 /\ 7 <= undef31 /\ 7 <= undef110, {arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114, rest remain the same}>
Conditions: 4 <= arg1, 1 <= arg2, 2 + arg3 <= arg1, 
Transition: <l0, l12, 2 + undef13 <= undef11 /\ 2 + undef14 <= undef12 /\ undef105 <= undef11 /\ undef105 <= undef12 /\ 0 <= undef106 /\ 7 <= undef11 /\ 7 <= undef12 /\ 7 <= undef105, {arg1 -> undef105, arg2 -> undef106, arg3 -> 5, arg4 -> undef108, arg5 -> undef109, rest remain the same}>
Conditions: 4 <= arg1, 1 <= arg2, 2 + arg3 <= arg1, 
Transition: <l0, l12, 5 <= undef6 /\ undef110 <= undef26 /\ 0 <= undef111 /\ 7 <= undef7 /\ 7 <= undef110 /\ 10 <= undef26, {arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114, rest remain the same}>
Conditions: 4 <= arg1, 1 <= arg2, 2 + arg3 <= arg1, 
Transition: <l0, l12, 5 <= undef6 /\ undef110 <= undef36 /\ 0 <= undef111 /\ 7 <= undef7 /\ 7 <= undef110 /\ undef36 <= 9 + undef6 /\ undef36 <= 7 + undef7 /\ 10 <= undef36, {arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114, rest remain the same}>
Conditions: 4 <= arg1, 1 <= arg2, 2 + arg3 <= arg1, 
Transition: <l0, l12, 4 + undef22 <= undef21 /\ 2 + undef13 <= undef11 /\ 2 + undef14 <= undef12 /\ undef110 <= undef21 /\ 0 <= undef111 /\ 7 <= undef11 /\ 7 <= undef12 /\ 7 <= undef21 /\ 7 <= undef110, {arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114, rest remain the same}>
Conditions: 4 <= arg1, 1 <= arg2, 2 + arg3 <= arg1, 
Transition: <l0, l12, 4 + undef32 <= undef31 /\ 2 + undef13 <= undef11 /\ 2 + undef14 <= undef12 /\ undef110 <= undef31 /\ 0 <= undef111 /\ 7 <= undef11 /\ 7 <= undef12 /\ 7 <= undef31 /\ 7 <= undef110, {arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114, rest remain the same}>
Conditions: 4 <= arg1, 1 <= arg2, 2 + arg3 <= arg1, 
Transition: <l0, l12, 2 + undef13 <= undef11 /\ 2 + undef14 <= undef12 /\ undef105 <= undef11 /\ undef105 <= undef12 /\ 0 <= undef106 /\ 7 <= undef11 /\ 7 <= undef12 /\ 7 <= undef105, {arg1 -> undef105, arg2 -> undef106, arg3 -> 5, arg4 -> undef108, arg5 -> undef109, rest remain the same}>
Conditions: 4 <= arg1, 1 <= arg2, 2 + arg3 <= arg1, 
Transition: <l0, l12, 5 <= undef6 /\ undef110 <= undef26 /\ 0 <= undef111 /\ 7 <= undef7 /\ 7 <= undef110 /\ 10 <= undef26, {arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114, rest remain the same}>
Conditions: 4 <= arg1, 1 <= arg2, 2 + arg3 <= arg1, 
Transition: <l0, l12, 5 <= undef6 /\ undef110 <= undef36 /\ 0 <= undef111 /\ 7 <= undef7 /\ 7 <= undef110 /\ undef36 <= 9 + undef6 /\ undef36 <= 7 + undef7 /\ 10 <= undef36, {arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114, rest remain the same}>
Conditions: 4 <= arg1, 1 <= arg2, 2 + arg3 <= arg1, 
Transition: <l0, l12, 4 + undef22 <= undef21 /\ 2 + undef13 <= undef11 /\ 2 + undef14 <= undef12 /\ undef110 <= undef21 /\ 0 <= undef111 /\ 7 <= undef11 /\ 7 <= undef12 /\ 7 <= undef21 /\ 7 <= undef110, {arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114, rest remain the same}>
Conditions: 4 <= arg1, 1 <= arg2, 2 + arg3 <= arg1, 
Transition: <l0, l12, 4 + undef32 <= undef31 /\ 2 + undef13 <= undef11 /\ 2 + undef14 <= undef12 /\ undef110 <= undef31 /\ 0 <= undef111 /\ 7 <= undef11 /\ 7 <= undef12 /\ 7 <= undef31 /\ 7 <= undef110, {arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114, rest remain the same}>
Conditions: 4 <= arg1, 1 <= arg2, 2 + arg3 <= arg1, 
Transition: <l0, l12, 2 + undef13 <= undef11 /\ 2 + undef14 <= undef12 /\ undef105 <= undef11 /\ undef105 <= undef12 /\ 0 <= undef106 /\ 7 <= undef11 /\ 7 <= undef12 /\ 7 <= undef105, {arg1 -> undef105, arg2 -> undef106, arg3 -> 5, arg4 -> undef108, arg5 -> undef109, rest remain the same}>
Conditions: 4 <= arg1, 1 <= arg2, 2 + arg3 <= arg1, 
Transition: <l0, l12, 5 <= undef6 /\ undef110 <= undef26 /\ 0 <= undef111 /\ 7 <= undef7 /\ 7 <= undef110 /\ 10 <= undef26, {arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114, rest remain the same}>
Conditions: 4 <= arg1, 1 <= arg2, 2 + arg3 <= arg1, 
Transition: <l0, l12, 5 <= undef6 /\ undef110 <= undef36 /\ 0 <= undef111 /\ 7 <= undef7 /\ 7 <= undef110 /\ undef36 <= 9 + undef6 /\ undef36 <= 7 + undef7 /\ 10 <= undef36, {arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114, rest remain the same}>
Conditions: 4 <= arg1, 1 <= arg2, 2 + arg3 <= arg1, 
Transition: <l0, l12, 4 + undef22 <= undef21 /\ 2 + undef13 <= undef11 /\ 2 + undef14 <= undef12 /\ undef110 <= undef21 /\ 0 <= undef111 /\ 7 <= undef11 /\ 7 <= undef12 /\ 7 <= undef21 /\ 7 <= undef110, {arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114, rest remain the same}>
Conditions: 4 <= arg1, 1 <= arg2, 2 + arg3 <= arg1, 
Transition: <l0, l12, 4 + undef32 <= undef31 /\ 2 + undef13 <= undef11 /\ 2 + undef14 <= undef12 /\ undef110 <= undef31 /\ 0 <= undef111 /\ 7 <= undef11 /\ 7 <= undef12 /\ 7 <= undef31 /\ 7 <= undef110, {arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114, rest remain the same}>
Conditions: 4 <= arg1, 1 <= arg2, 2 + arg3 <= arg1, 
Transition: <l0, l12, 2 + undef13 <= undef11 /\ 2 + undef14 <= undef12 /\ undef105 <= undef11 /\ undef105 <= undef12 /\ 0 <= undef106 /\ 7 <= undef11 /\ 7 <= undef12 /\ 7 <= undef105, {arg1 -> undef105, arg2 -> undef106, arg3 -> 5, arg4 -> undef108, arg5 -> undef109, rest remain the same}>
Conditions: 4 <= arg1, 1 <= arg2, 2 + arg3 <= arg1, 
Transition: <l0, l12, 5 <= undef6 /\ undef110 <= undef26 /\ 0 <= undef111 /\ 7 <= undef7 /\ 7 <= undef110 /\ 10 <= undef26, {arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114, rest remain the same}>
Conditions: 4 <= arg1, 1 <= arg2, 2 + arg3 <= arg1, 
Transition: <l0, l12, 5 <= undef6 /\ undef110 <= undef36 /\ 0 <= undef111 /\ 7 <= undef7 /\ 7 <= undef110 /\ undef36 <= 9 + undef6 /\ undef36 <= 7 + undef7 /\ 10 <= undef36, {arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114, rest remain the same}>
Conditions: 4 <= arg1, 1 <= arg2, 2 + arg3 <= arg1, 
Transition: <l0, l12, 4 + undef22 <= undef21 /\ 2 + undef13 <= undef11 /\ 2 + undef14 <= undef12 /\ undef110 <= undef21 /\ 0 <= undef111 /\ 7 <= undef11 /\ 7 <= undef12 /\ 7 <= undef21 /\ 7 <= undef110, {arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114, rest remain the same}>
Conditions: 4 <= arg1, 1 <= arg2, 2 + arg3 <= arg1, 
Transition: <l0, l12, 4 + undef32 <= undef31 /\ 2 + undef13 <= undef11 /\ 2 + undef14 <= undef12 /\ undef110 <= undef31 /\ 0 <= undef111 /\ 7 <= undef11 /\ 7 <= undef12 /\ 7 <= undef31 /\ 7 <= undef110, {arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114, rest remain the same}>
Conditions: 4 <= arg1, 1 <= arg2, 2 + arg3 <= arg1, 
Transition: <l0, l12, 2 + undef13 <= undef11 /\ 2 + undef14 <= undef12 /\ undef105 <= undef11 /\ undef105 <= undef12 /\ 0 <= undef106 /\ 7 <= undef11 /\ 7 <= undef12 /\ 7 <= undef105, {arg1 -> undef105, arg2 -> undef106, arg3 -> 5, arg4 -> undef108, arg5 -> undef109, rest remain the same}>
Conditions: 4 <= arg1, 1 <= arg2, 2 + arg3 <= arg1, 
OPEN EXITS: 
<l0, l12, 1 <= undef111 /\ 5 <= undef6 /\ undef110 <= undef26 /\ 7 <= undef7 /\ 7 <= undef110 /\ 10 <= undef26, {arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114, rest remain the same}>
<l0, l12, 1 <= undef111 /\ 5 <= undef6 /\ undef110 <= undef36 /\ 7 <= undef7 /\ 7 <= undef110 /\ undef36 <= 9 + undef6 /\ undef36 <= 7 + undef7 /\ 10 <= undef36, {arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114, rest remain the same}>
<l0, l12, 4 + undef22 <= undef21 /\ 1 <= undef111 /\ 2 + undef13 <= undef11 /\ 2 + undef14 <= undef12 /\ undef110 <= undef21 /\ 7 <= undef11 /\ 7 <= undef12 /\ 7 <= undef21 /\ 7 <= undef110, {arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114, rest remain the same}>
<l0, l12, 4 + undef32 <= undef31 /\ 1 <= undef111 /\ 2 + undef13 <= undef11 /\ 2 + undef14 <= undef12 /\ undef110 <= undef31 /\ 7 <= undef11 /\ 7 <= undef12 /\ 7 <= undef31 /\ 7 <= undef110, {arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114, rest remain the same}>
<l0, l12, 1 <= undef106 /\ 2 + undef13 <= undef11 /\ 2 + undef14 <= undef12 /\ undef105 <= undef11 /\ undef105 <= undef12 /\ 7 <= undef11 /\ 7 <= undef12 /\ 7 <= undef105, {arg1 -> undef105, arg2 -> undef106, arg3 -> 5, arg4 -> undef108, arg5 -> undef109, rest remain the same}>
<l0, l12, 1 <= undef111 /\ 5 <= undef6 /\ undef110 <= undef26 /\ 7 <= undef7 /\ 7 <= undef110 /\ 10 <= undef26, {arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114, rest remain the same}>
<l0, l12, 1 <= undef111 /\ 5 <= undef6 /\ undef110 <= undef36 /\ 7 <= undef7 /\ 7 <= undef110 /\ undef36 <= 9 + undef6 /\ undef36 <= 7 + undef7 /\ 10 <= undef36, {arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114, rest remain the same}>
<l0, l12, 4 + undef22 <= undef21 /\ 1 <= undef111 /\ 2 + undef13 <= undef11 /\ 2 + undef14 <= undef12 /\ undef110 <= undef21 /\ 7 <= undef11 /\ 7 <= undef12 /\ 7 <= undef21 /\ 7 <= undef110, {arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114, rest remain the same}>
<l0, l12, 4 + undef32 <= undef31 /\ 1 <= undef111 /\ 2 + undef13 <= undef11 /\ 2 + undef14 <= undef12 /\ undef110 <= undef31 /\ 7 <= undef11 /\ 7 <= undef12 /\ 7 <= undef31 /\ 7 <= undef110, {arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114, rest remain the same}>
<l0, l12, 1 <= undef106 /\ 2 + undef13 <= undef11 /\ 2 + undef14 <= undef12 /\ undef105 <= undef11 /\ undef105 <= undef12 /\ 7 <= undef11 /\ 7 <= undef12 /\ 7 <= undef105, {arg1 -> undef105, arg2 -> undef106, arg3 -> 5, arg4 -> undef108, arg5 -> undef109, rest remain the same}>
<l0, l12, 1 <= undef111 /\ 5 <= undef6 /\ undef110 <= undef26 /\ 7 <= undef7 /\ 7 <= undef110 /\ 10 <= undef26, {arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114, rest remain the same}>
<l0, l12, 1 <= undef111 /\ 5 <= undef6 /\ undef110 <= undef36 /\ 7 <= undef7 /\ 7 <= undef110 /\ undef36 <= 9 + undef6 /\ undef36 <= 7 + undef7 /\ 10 <= undef36, {arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114, rest remain the same}>
<l0, l12, 4 + undef22 <= undef21 /\ 1 <= undef111 /\ 2 + undef13 <= undef11 /\ 2 + undef14 <= undef12 /\ undef110 <= undef21 /\ 7 <= undef11 /\ 7 <= undef12 /\ 7 <= undef21 /\ 7 <= undef110, {arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114, rest remain the same}>
<l0, l12, 4 + undef32 <= undef31 /\ 1 <= undef111 /\ 2 + undef13 <= undef11 /\ 2 + undef14 <= undef12 /\ undef110 <= undef31 /\ 7 <= undef11 /\ 7 <= undef12 /\ 7 <= undef31 /\ 7 <= undef110, {arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114, rest remain the same}>
<l0, l12, 1 <= undef106 /\ 2 + undef13 <= undef11 /\ 2 + undef14 <= undef12 /\ undef105 <= undef11 /\ undef105 <= undef12 /\ 7 <= undef11 /\ 7 <= undef12 /\ 7 <= undef105, {arg1 -> undef105, arg2 -> undef106, arg3 -> 5, arg4 -> undef108, arg5 -> undef109, rest remain the same}>
<l0, l12, 1 <= undef111 /\ 5 <= undef6 /\ undef110 <= undef26 /\ 7 <= undef7 /\ 7 <= undef110 /\ 10 <= undef26, {arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114, rest remain the same}>
<l0, l12, 1 <= undef111 /\ 5 <= undef6 /\ undef110 <= undef36 /\ 7 <= undef7 /\ 7 <= undef110 /\ undef36 <= 9 + undef6 /\ undef36 <= 7 + undef7 /\ 10 <= undef36, {arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114, rest remain the same}>
<l0, l12, 4 + undef22 <= undef21 /\ 1 <= undef111 /\ 2 + undef13 <= undef11 /\ 2 + undef14 <= undef12 /\ undef110 <= undef21 /\ 7 <= undef11 /\ 7 <= undef12 /\ 7 <= undef21 /\ 7 <= undef110, {arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114, rest remain the same}>
<l0, l12, 4 + undef32 <= undef31 /\ 1 <= undef111 /\ 2 + undef13 <= undef11 /\ 2 + undef14 <= undef12 /\ undef110 <= undef31 /\ 7 <= undef11 /\ 7 <= undef12 /\ 7 <= undef31 /\ 7 <= undef110, {arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114, rest remain the same}>
<l0, l12, 1 <= undef106 /\ 2 + undef13 <= undef11 /\ 2 + undef14 <= undef12 /\ undef105 <= undef11 /\ undef105 <= undef12 /\ 7 <= undef11 /\ 7 <= undef12 /\ 7 <= undef105, {arg1 -> undef105, arg2 -> undef106, arg3 -> 5, arg4 -> undef108, arg5 -> undef109, rest remain the same}>
<l0, l12, 1 <= undef111 /\ 5 <= undef6 /\ undef110 <= undef26 /\ 7 <= undef7 /\ 7 <= undef110 /\ 10 <= undef26, {arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114, rest remain the same}>
<l0, l12, 1 <= undef111 /\ 5 <= undef6 /\ undef110 <= undef36 /\ 7 <= undef7 /\ 7 <= undef110 /\ undef36 <= 9 + undef6 /\ undef36 <= 7 + undef7 /\ 10 <= undef36, {arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114, rest remain the same}>
<l0, l12, 4 + undef22 <= undef21 /\ 1 <= undef111 /\ 2 + undef13 <= undef11 /\ 2 + undef14 <= undef12 /\ undef110 <= undef21 /\ 7 <= undef11 /\ 7 <= undef12 /\ 7 <= undef21 /\ 7 <= undef110, {arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114, rest remain the same}>
<l0, l12, 4 + undef32 <= undef31 /\ 1 <= undef111 /\ 2 + undef13 <= undef11 /\ 2 + undef14 <= undef12 /\ undef110 <= undef31 /\ 7 <= undef11 /\ 7 <= undef12 /\ 7 <= undef31 /\ 7 <= undef110, {arg1 -> undef110, arg2 -> undef111, arg3 -> 5, arg4 -> undef113, arg5 -> undef114, rest remain the same}>
<l0, l12, 1 <= undef106 /\ 2 + undef13 <= undef11 /\ 2 + undef14 <= undef12 /\ undef105 <= undef11 /\ undef105 <= undef12 /\ 7 <= undef11 /\ 7 <= undef12 /\ 7 <= undef105, {arg1 -> undef105, arg2 -> undef106, arg3 -> 5, arg4 -> undef108, arg5 -> undef109, rest remain the same}>

> Conditions are reachable!

Program does NOT terminate