YES

Solver Timeout: 4
Global Timeout: 300
No parsing errors!
Init Location: 0
Transitions:
<l0, l16, true>
<l1, l2, (undef4 = undef4) /\ (undef5 = undef5) /\ (undef6 = undef6), par{oldX0^0 -> (0 + x0^0), oldX1^0 -> (0 + x1^0), oldX2^0 -> (0 + x2^0), oldX3^0 -> undef4, oldX4^0 -> undef5, oldX5^0 -> undef6, x0^0 -> (0 + undef4), x1^0 -> (0 + undef5), x2^0 -> (0 + undef6)}>
<l3, l4, (undef11 = (0 + x0^0)) /\ (undef12 = (0 + x1^0)) /\ (undef14 = undef14), par{oldX0^0 -> undef11, oldX1^0 -> undef12, oldX2^0 -> (0 + x2^0), oldX3^0 -> undef14, x0^0 -> (0 + undef11), x1^0 -> (0 + undef12), x2^0 -> (0 + undef14)}>
<l5, l2, (undef24 = undef24) /\ (undef25 = undef25) /\ (undef26 = undef26), par{oldX0^0 -> (0 + x0^0), oldX1^0 -> (0 + x1^0), oldX2^0 -> (0 + x2^0), oldX3^0 -> undef24, oldX4^0 -> undef25, oldX5^0 -> undef26, x0^0 -> (0 + undef24), x1^0 -> (0 + undef25), x2^0 -> (0 + undef26)}>
<l6, l3, (undef31 = (0 + x0^0)) /\ (undef32 = (0 + x1^0)) /\ (undef34 = undef34) /\ (2 <= (0 + undef32)), par{oldX0^0 -> undef31, oldX1^0 -> undef32, oldX2^0 -> (0 + x2^0), oldX3^0 -> undef34, x0^0 -> (0 + undef31), x1^0 -> (0 + undef32), x2^0 -> (0 + undef34)}>
<l6, l3, (undef41 = (0 + x0^0)) /\ (undef42 = (0 + x1^0)) /\ (undef44 = undef44) /\ ((1 + undef42) <= 1), par{oldX0^0 -> undef41, oldX1^0 -> undef42, oldX2^0 -> (0 + x2^0), oldX3^0 -> undef44, x0^0 -> (0 + undef41), x1^0 -> (0 + undef42), x2^0 -> (0 + undef44)}>
<l6, l1, (undef51 = (0 + x0^0)) /\ (undef52 = (0 + x1^0)) /\ (undef54 = undef54) /\ ((0 + undef52) <= 1) /\ (1 <= (0 + undef52)), par{oldX0^0 -> undef51, oldX1^0 -> undef52, oldX2^0 -> (0 + x2^0), oldX3^0 -> undef54, x0^0 -> (0 + undef51), x1^0 -> (0 + undef52), x2^0 -> (0 + undef54)}>
<l7, l3, (undef61 = (0 + x0^0)) /\ (undef62 = (0 + x1^0)) /\ (undef64 = undef64) /\ (1 <= (0 + undef62)), par{oldX0^0 -> undef61, oldX1^0 -> undef62, oldX2^0 -> (0 + x2^0), oldX3^0 -> undef64, x0^0 -> (0 + undef61), x1^0 -> (0 + undef62), x2^0 -> (0 + undef64)}>
<l7, l3, (undef71 = (0 + x0^0)) /\ (undef72 = (0 + x1^0)) /\ (undef74 = undef74) /\ ((1 + undef72) <= 0), par{oldX0^0 -> undef71, oldX1^0 -> undef72, oldX2^0 -> (0 + x2^0), oldX3^0 -> undef74, x0^0 -> (0 + undef71), x1^0 -> (0 + undef72), x2^0 -> (0 + undef74)}>
<l7, l5, (undef81 = (0 + x0^0)) /\ (undef82 = (0 + x1^0)) /\ (undef84 = undef84) /\ ((0 + undef82) <= 0) /\ (0 <= (0 + undef82)), par{oldX0^0 -> undef81, oldX1^0 -> undef82, oldX2^0 -> (0 + x2^0), oldX3^0 -> undef84, x0^0 -> (0 + undef81), x1^0 -> (0 + undef82), x2^0 -> (0 + undef84)}>
<l8, l6, (undef91 = (0 + x0^0)) /\ (undef92 = (0 + x1^0)) /\ (undef94 = undef94) /\ (1 <= (0 + undef92)), par{oldX0^0 -> undef91, oldX1^0 -> undef92, oldX2^0 -> (0 + x2^0), oldX3^0 -> undef94, x0^0 -> (0 + undef91), x1^0 -> (0 + undef92), x2^0 -> (0 + undef94)}>
<l8, l7, (undef101 = (0 + x0^0)) /\ (undef102 = (0 + x1^0)) /\ (undef104 = undef104) /\ ((1 + undef102) <= 1), par{oldX0^0 -> undef101, oldX1^0 -> undef102, oldX2^0 -> (0 + x2^0), oldX3^0 -> undef104, x0^0 -> (0 + undef101), x1^0 -> (0 + undef102), x2^0 -> (0 + undef104)}>
<l9, l8, (undef111 = (0 + x0^0)) /\ (undef112 = (0 + x1^0)) /\ (undef114 = undef114), par{oldX0^0 -> undef111, oldX1^0 -> undef112, oldX2^0 -> (0 + x2^0), oldX3^0 -> undef114, x0^0 -> (0 + undef111), x1^0 -> (0 + undef112), x2^0 -> (0 + undef114)}>
<l10, l2, (undef123 = (0 + x2^0)) /\ (undef124 = undef124) /\ (undef125 = undef125) /\ (undef126 = undef126) /\ (undef127 = undef127) /\ (2 <= ((0 + undef123) + (~(2) * undef127))), par{oldX0^0 -> (0 + x0^0), oldX1^0 -> (0 + x1^0), oldX2^0 -> undef123, oldX3^0 -> undef124, oldX4^0 -> undef125, oldX5^0 -> undef126, oldX6^0 -> undef127, x0^0 -> (0 + undef124), x1^0 -> (0 + undef125), x2^0 -> (0 + undef126)}>
<l10, l2, (undef133 = (0 + x2^0)) /\ (undef134 = undef134) /\ (undef135 = undef135) /\ (undef136 = undef136) /\ (undef137 = undef137) /\ (((1 + undef133) + (~(2) * undef137)) <= 0), par{oldX0^0 -> (0 + x0^0), oldX1^0 -> (0 + x1^0), oldX2^0 -> undef133, oldX3^0 -> undef134, oldX4^0 -> undef135, oldX5^0 -> undef136, oldX6^0 -> undef137, x0^0 -> (0 + undef134), x1^0 -> (0 + undef135), x2^0 -> (0 + undef136)}>
<l10, l11, (undef141 = (0 + x0^0)) /\ (undef142 = (0 + x1^0)) /\ (undef143 = (0 + x2^0)) /\ (undef144 = undef144) /\ (0 <= ((0 + undef143) + (~(2) * undef144))) /\ (((1 + undef143) + (~(2) * undef144)) <= 2), par{oldX0^0 -> undef141, oldX1^0 -> undef142, oldX2^0 -> undef143, oldX3^0 -> undef144, x0^0 -> (0 + undef141), x1^0 -> (0 + undef142), x2^0 -> (0 + undef144)}>
<l12, l10, (undef151 = (0 + x0^0)) /\ (undef152 = (0 + x1^0)) /\ (undef153 = (0 + x2^0)), par{oldX0^0 -> undef151, oldX1^0 -> undef152, oldX2^0 -> undef153, x0^0 -> (0 + undef151), x1^0 -> (0 + undef152), x2^0 -> (0 + undef153)}>
<l13, l10, (undef161 = (0 + x0^0)) /\ (undef162 = (0 + x1^0)) /\ (undef163 = (0 + x2^0)) /\ (undef164 = undef164) /\ (2 <= (0 + undef164)), par{oldX0^0 -> undef161, oldX1^0 -> undef162, oldX2^0 -> undef163, oldX3^0 -> undef164, x0^0 -> (0 + undef161), x1^0 -> (0 + undef162), x2^0 -> (0 + undef163)}>
<l13, l10, (undef171 = (0 + x0^0)) /\ (undef172 = (0 + x1^0)) /\ (undef173 = (0 + x2^0)) /\ (undef174 = undef174) /\ ((1 + undef174) <= 1), par{oldX0^0 -> undef171, oldX1^0 -> undef172, oldX2^0 -> undef173, oldX3^0 -> undef174, x0^0 -> (0 + undef171), x1^0 -> (0 + undef172), x2^0 -> (0 + undef173)}>
<l13, l12, (undef181 = (0 + x0^0)) /\ (undef182 = (0 + x1^0)) /\ (undef183 = (0 + x2^0)) /\ (undef184 = undef184) /\ ((0 + undef184) <= 1) /\ (1 <= (0 + undef184)), par{oldX0^0 -> undef181, oldX1^0 -> undef182, oldX2^0 -> undef183, oldX3^0 -> undef184, x0^0 -> (0 + undef181), x1^0 -> (0 + undef182), x2^0 -> (0 + undef183)}>
<l11, l5, (undef191 = (0 + x0^0)) /\ (undef192 = (0 + x1^0)) /\ (undef193 = (0 + x2^0)) /\ (undef194 = undef194) /\ ((0 + undef193) <= 0), par{oldX0^0 -> undef191, oldX1^0 -> undef192, oldX2^0 -> undef193, oldX3^0 -> undef194, x0^0 -> (0 + undef191), x1^0 -> (0 + undef192), x2^0 -> (0 + undef194)}>
<l11, l13, (undef201 = (0 + x0^0)) /\ (undef202 = (0 + x1^0)) /\ (undef203 = (0 + x2^0)) /\ (1 <= (0 + undef203)), par{oldX0^0 -> undef201, oldX1^0 -> undef202, oldX2^0 -> undef203, x0^0 -> (0 + undef201), x1^0 -> (0 + undef202), x2^0 -> (0 + undef203)}>
<l14, l2, (undef214 = undef214) /\ (undef215 = undef215) /\ (undef216 = undef216), par{oldX0^0 -> (0 + x0^0), oldX1^0 -> (0 + x1^0), oldX2^0 -> (0 + x2^0), oldX3^0 -> undef214, oldX4^0 -> undef215, oldX5^0 -> undef216, x0^0 -> (0 + undef214), x1^0 -> (0 + undef215), x2^0 -> (0 + undef216)}>
<l4, l11, (undef221 = (0 + x0^0)) /\ (undef222 = (0 + x1^0)) /\ (3 <= (0 + undef221)), par{oldX0^0 -> undef221, oldX1^0 -> undef222, oldX2^0 -> (0 + x2^0), x0^0 -> (0 + undef221), x1^0 -> (0 + undef222), x2^0 -> (0 + undef222)}>
<l4, l11, (undef231 = (0 + x0^0)) /\ (undef232 = (0 + x1^0)) /\ ((1 + undef231) <= 2), par{oldX0^0 -> undef231, oldX1^0 -> undef232, oldX2^0 -> (0 + x2^0), x0^0 -> (0 + undef231), x1^0 -> (0 + undef232), x2^0 -> (0 + undef232)}>
<l4, l14, (undef241 = (0 + x0^0)) /\ (undef242 = (0 + x1^0)) /\ (undef244 = undef244) /\ ((0 + undef241) <= 2) /\ (2 <= (0 + undef241)), par{oldX0^0 -> undef241, oldX1^0 -> undef242, oldX2^0 -> (0 + x2^0), oldX3^0 -> undef244, x0^0 -> (0 + undef241), x1^0 -> (0 + undef242), x2^0 -> (0 + undef244)}>
<l15, l9, (undef251 = (0 + x0^0)) /\ (undef252 = (0 + x1^0)) /\ (undef254 = undef254), par{oldX0^0 -> undef251, oldX1^0 -> undef252, oldX2^0 -> (0 + x2^0), oldX3^0 -> undef254, x0^0 -> (0 + undef251), x1^0 -> (0 + undef252), x2^0 -> (0 + undef254)}>
<l15, l2, true>
<l15, l1, true>
<l15, l3, true>
<l15, l5, true>
<l15, l6, true>
<l15, l7, true>
<l15, l8, true>
<l15, l9, true>
<l15, l10, true>
<l15, l12, true>
<l15, l13, true>
<l15, l11, true>
<l15, l14, true>
<l15, l4, true>
<l16, l15, true>

Fresh variables:
undef4, undef5, undef6, undef11, undef12, undef14, undef24, undef25, undef26, undef31, undef32, undef34, undef41, undef42, undef44, undef51, undef52, undef54, undef61, undef62, undef64, undef71, undef72, undef74, undef81, undef82, undef84, undef91, undef92, undef94, undef101, undef102, undef104, undef111, undef112, undef114, undef123, undef124, undef125, undef126, undef127, undef133, undef134, undef135, undef136, undef137, undef141, undef142, undef143, undef144, undef151, undef152, undef153, undef161, undef162, undef163, undef164, undef171, undef172, undef173, undef174, undef181, undef182, undef183, undef184, undef191, undef192, undef193, undef194, undef201, undef202, undef203, undef214, undef215, undef216, undef221, undef222, undef231, undef232, undef241, undef242, undef244, undef251, undef252, undef254, 

Undef variables:
undef4, undef5, undef6, undef11, undef12, undef14, undef24, undef25, undef26, undef31, undef32, undef34, undef41, undef42, undef44, undef51, undef52, undef54, undef61, undef62, undef64, undef71, undef72, undef74, undef81, undef82, undef84, undef91, undef92, undef94, undef101, undef102, undef104, undef111, undef112, undef114, undef123, undef124, undef125, undef126, undef127, undef133, undef134, undef135, undef136, undef137, undef141, undef142, undef143, undef144, undef151, undef152, undef153, undef161, undef162, undef163, undef164, undef171, undef172, undef173, undef174, undef181, undef182, undef183, undef184, undef191, undef192, undef193, undef194, undef201, undef202, undef203, undef214, undef215, undef216, undef221, undef222, undef231, undef232, undef241, undef242, undef244, undef251, undef252, undef254, 

Abstraction variables:

Exit nodes:

Accepting locations:

Asserts:

Preprocessed LLVMGraph
Init Location: 0
Transitions:
<l0, l6, (undef251 = (0 + x0^0)) /\ (undef252 = (0 + x1^0)) /\ (undef254 = undef254) /\ (undef111 = (0 + (0 + undef251))) /\ (undef112 = (0 + (0 + undef252))) /\ (undef114 = undef114) /\ (undef91 = (0 + (0 + undef111))) /\ (undef92 = (0 + (0 + undef112))) /\ (undef94 = undef94) /\ (1 <= (0 + undef92)), par{x0^0 -> (0 + undef91), x1^0 -> (0 + undef92), x2^0 -> (0 + undef94)}>
<l0, l7, (undef251 = (0 + x0^0)) /\ (undef252 = (0 + x1^0)) /\ (undef254 = undef254) /\ (undef111 = (0 + (0 + undef251))) /\ (undef112 = (0 + (0 + undef252))) /\ (undef114 = undef114) /\ (undef101 = (0 + (0 + undef111))) /\ (undef102 = (0 + (0 + undef112))) /\ (undef104 = undef104) /\ ((1 + undef102) <= 1), par{x0^0 -> (0 + undef101), x1^0 -> (0 + undef102), x2^0 -> (0 + undef104)}>
<l0, l2, true>
<l0, l2, (undef4 = undef4) /\ (undef5 = undef5) /\ (undef6 = undef6), par{x0^0 -> (0 + undef4), x1^0 -> (0 + undef5), x2^0 -> (0 + undef6)}>
<l0, l4, (undef11 = (0 + x0^0)) /\ (undef12 = (0 + x1^0)) /\ (undef14 = undef14), par{x0^0 -> (0 + undef11), x1^0 -> (0 + undef12), x2^0 -> (0 + undef14)}>
<l0, l2, (undef24 = undef24) /\ (undef25 = undef25) /\ (undef26 = undef26), par{x0^0 -> (0 + undef24), x1^0 -> (0 + undef25), x2^0 -> (0 + undef26)}>
<l0, l6, true>
<l0, l7, true>
<l0, l6, (undef91 = (0 + x0^0)) /\ (undef92 = (0 + x1^0)) /\ (undef94 = undef94) /\ (1 <= (0 + undef92)), par{x0^0 -> (0 + undef91), x1^0 -> (0 + undef92), x2^0 -> (0 + undef94)}>
<l0, l7, (undef101 = (0 + x0^0)) /\ (undef102 = (0 + x1^0)) /\ (undef104 = undef104) /\ ((1 + undef102) <= 1), par{x0^0 -> (0 + undef101), x1^0 -> (0 + undef102), x2^0 -> (0 + undef104)}>
<l0, l6, (undef111 = (0 + x0^0)) /\ (undef112 = (0 + x1^0)) /\ (undef114 = undef114) /\ (undef91 = (0 + (0 + undef111))) /\ (undef92 = (0 + (0 + undef112))) /\ (undef94 = undef94) /\ (1 <= (0 + undef92)), par{x0^0 -> (0 + undef91), x1^0 -> (0 + undef92), x2^0 -> (0 + undef94)}>
<l0, l7, (undef111 = (0 + x0^0)) /\ (undef112 = (0 + x1^0)) /\ (undef114 = undef114) /\ (undef101 = (0 + (0 + undef111))) /\ (undef102 = (0 + (0 + undef112))) /\ (undef104 = undef104) /\ ((1 + undef102) <= 1), par{x0^0 -> (0 + undef101), x1^0 -> (0 + undef102), x2^0 -> (0 + undef104)}>
<l0, l10, true>
<l0, l10, (undef151 = (0 + x0^0)) /\ (undef152 = (0 + x1^0)) /\ (undef153 = (0 + x2^0)), par{x0^0 -> (0 + undef151), x1^0 -> (0 + undef152), x2^0 -> (0 + undef153)}>
<l0, l13, true>
<l0, l11, true>
<l0, l2, (undef214 = undef214) /\ (undef215 = undef215) /\ (undef216 = undef216), par{x0^0 -> (0 + undef214), x1^0 -> (0 + undef215), x2^0 -> (0 + undef216)}>
<l0, l4, true>
<l4, l11, (undef221 = (0 + x0^0)) /\ (undef222 = (0 + x1^0)) /\ (3 <= (0 + undef221)), par{x0^0 -> (0 + undef221), x1^0 -> (0 + undef222), x2^0 -> (0 + undef222)}>
<l4, l11, (undef231 = (0 + x0^0)) /\ (undef232 = (0 + x1^0)) /\ ((1 + undef231) <= 2), par{x0^0 -> (0 + undef231), x1^0 -> (0 + undef232), x2^0 -> (0 + undef232)}>
<l4, l2, (undef241 = (0 + x0^0)) /\ (undef242 = (0 + x1^0)) /\ (undef244 = undef244) /\ ((0 + undef241) <= 2) /\ (2 <= (0 + undef241)) /\ (undef214 = undef214) /\ (undef215 = undef215) /\ (undef216 = undef216), par{x0^0 -> (0 + undef214), x1^0 -> (0 + undef215), x2^0 -> (0 + undef216)}>
<l6, l4, (undef31 = (0 + x0^0)) /\ (undef32 = (0 + x1^0)) /\ (undef34 = undef34) /\ (2 <= (0 + undef32)) /\ (undef11 = (0 + (0 + undef31))) /\ (undef12 = (0 + (0 + undef32))) /\ (undef14 = undef14), par{x0^0 -> (0 + undef11), x1^0 -> (0 + undef12), x2^0 -> (0 + undef14)}>
<l6, l4, (undef41 = (0 + x0^0)) /\ (undef42 = (0 + x1^0)) /\ (undef44 = undef44) /\ ((1 + undef42) <= 1) /\ (undef11 = (0 + (0 + undef41))) /\ (undef12 = (0 + (0 + undef42))) /\ (undef14 = undef14), par{x0^0 -> (0 + undef11), x1^0 -> (0 + undef12), x2^0 -> (0 + undef14)}>
<l6, l2, (undef51 = (0 + x0^0)) /\ (undef52 = (0 + x1^0)) /\ (undef54 = undef54) /\ ((0 + undef52) <= 1) /\ (1 <= (0 + undef52)) /\ (undef4 = undef4) /\ (undef5 = undef5) /\ (undef6 = undef6), par{x0^0 -> (0 + undef4), x1^0 -> (0 + undef5), x2^0 -> (0 + undef6)}>
<l7, l4, (undef61 = (0 + x0^0)) /\ (undef62 = (0 + x1^0)) /\ (undef64 = undef64) /\ (1 <= (0 + undef62)) /\ (undef11 = (0 + (0 + undef61))) /\ (undef12 = (0 + (0 + undef62))) /\ (undef14 = undef14), par{x0^0 -> (0 + undef11), x1^0 -> (0 + undef12), x2^0 -> (0 + undef14)}>
<l7, l4, (undef71 = (0 + x0^0)) /\ (undef72 = (0 + x1^0)) /\ (undef74 = undef74) /\ ((1 + undef72) <= 0) /\ (undef11 = (0 + (0 + undef71))) /\ (undef12 = (0 + (0 + undef72))) /\ (undef14 = undef14), par{x0^0 -> (0 + undef11), x1^0 -> (0 + undef12), x2^0 -> (0 + undef14)}>
<l7, l2, (undef81 = (0 + x0^0)) /\ (undef82 = (0 + x1^0)) /\ (undef84 = undef84) /\ ((0 + undef82) <= 0) /\ (0 <= (0 + undef82)) /\ (undef24 = undef24) /\ (undef25 = undef25) /\ (undef26 = undef26), par{x0^0 -> (0 + undef24), x1^0 -> (0 + undef25), x2^0 -> (0 + undef26)}>
<l10, l2, (undef123 = (0 + x2^0)) /\ (undef124 = undef124) /\ (undef125 = undef125) /\ (undef126 = undef126) /\ (undef127 = undef127) /\ (2 <= ((0 + undef123) + (~(2) * undef127))), par{x0^0 -> (0 + undef124), x1^0 -> (0 + undef125), x2^0 -> (0 + undef126)}>
<l10, l2, (undef133 = (0 + x2^0)) /\ (undef134 = undef134) /\ (undef135 = undef135) /\ (undef136 = undef136) /\ (undef137 = undef137) /\ (((1 + undef133) + (~(2) * undef137)) <= 0), par{x0^0 -> (0 + undef134), x1^0 -> (0 + undef135), x2^0 -> (0 + undef136)}>
<l10, l11, (undef141 = (0 + x0^0)) /\ (undef142 = (0 + x1^0)) /\ (undef143 = (0 + x2^0)) /\ (undef144 = undef144) /\ (0 <= ((0 + undef143) + (~(2) * undef144))) /\ (((1 + undef143) + (~(2) * undef144)) <= 2), par{x0^0 -> (0 + undef141), x1^0 -> (0 + undef142), x2^0 -> (0 + undef144)}>
<l11, l2, (undef191 = (0 + x0^0)) /\ (undef192 = (0 + x1^0)) /\ (undef193 = (0 + x2^0)) /\ (undef194 = undef194) /\ ((0 + undef193) <= 0) /\ (undef24 = undef24) /\ (undef25 = undef25) /\ (undef26 = undef26), par{x0^0 -> (0 + undef24), x1^0 -> (0 + undef25), x2^0 -> (0 + undef26)}>
<l11, l13, (undef201 = (0 + x0^0)) /\ (undef202 = (0 + x1^0)) /\ (undef203 = (0 + x2^0)) /\ (1 <= (0 + undef203)), par{x0^0 -> (0 + undef201), x1^0 -> (0 + undef202), x2^0 -> (0 + undef203)}>
<l13, l10, (undef161 = (0 + x0^0)) /\ (undef162 = (0 + x1^0)) /\ (undef163 = (0 + x2^0)) /\ (undef164 = undef164) /\ (2 <= (0 + undef164)), par{x0^0 -> (0 + undef161), x1^0 -> (0 + undef162), x2^0 -> (0 + undef163)}>
<l13, l10, (undef171 = (0 + x0^0)) /\ (undef172 = (0 + x1^0)) /\ (undef173 = (0 + x2^0)) /\ (undef174 = undef174) /\ ((1 + undef174) <= 1), par{x0^0 -> (0 + undef171), x1^0 -> (0 + undef172), x2^0 -> (0 + undef173)}>
<l13, l10, (undef181 = (0 + x0^0)) /\ (undef182 = (0 + x1^0)) /\ (undef183 = (0 + x2^0)) /\ (undef184 = undef184) /\ ((0 + undef184) <= 1) /\ (1 <= (0 + undef184)) /\ (undef151 = (0 + (0 + undef181))) /\ (undef152 = (0 + (0 + undef182))) /\ (undef153 = (0 + (0 + undef183))), par{x0^0 -> (0 + undef151), x1^0 -> (0 + undef152), x2^0 -> (0 + undef153)}>

Fresh variables:
undef4, undef5, undef6, undef11, undef12, undef14, undef24, undef25, undef26, undef31, undef32, undef34, undef41, undef42, undef44, undef51, undef52, undef54, undef61, undef62, undef64, undef71, undef72, undef74, undef81, undef82, undef84, undef91, undef92, undef94, undef101, undef102, undef104, undef111, undef112, undef114, undef123, undef124, undef125, undef126, undef127, undef133, undef134, undef135, undef136, undef137, undef141, undef142, undef143, undef144, undef151, undef152, undef153, undef161, undef162, undef163, undef164, undef171, undef172, undef173, undef174, undef181, undef182, undef183, undef184, undef191, undef192, undef193, undef194, undef201, undef202, undef203, undef214, undef215, undef216, undef221, undef222, undef231, undef232, undef241, undef242, undef244, undef251, undef252, undef254, 

Undef variables:
undef4, undef5, undef6, undef11, undef12, undef14, undef24, undef25, undef26, undef31, undef32, undef34, undef41, undef42, undef44, undef51, undef52, undef54, undef61, undef62, undef64, undef71, undef72, undef74, undef81, undef82, undef84, undef91, undef92, undef94, undef101, undef102, undef104, undef111, undef112, undef114, undef123, undef124, undef125, undef126, undef127, undef133, undef134, undef135, undef136, undef137, undef141, undef142, undef143, undef144, undef151, undef152, undef153, undef161, undef162, undef163, undef164, undef171, undef172, undef173, undef174, undef181, undef182, undef183, undef184, undef191, undef192, undef193, undef194, undef201, undef202, undef203, undef214, undef215, undef216, undef221, undef222, undef231, undef232, undef241, undef242, undef244, undef251, undef252, undef254, 

Abstraction variables:

Exit nodes:

Accepting locations:

Asserts:

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

Init Location: 0
Graph 0:
Transitions:
Variables:

Graph 1:
Transitions:
Variables:

Graph 2:
Transitions:
Variables:

Graph 3:
Transitions:
Variables:

Graph 4:
Transitions:
<l10, l11, 2*undef144 <= undef143 /\ undef143 <= 1 + 2*undef144 /\ x0^0 = undef141 /\ x1^0 = undef142 /\ x2^0 = undef143, {x0^0 -> undef141, x1^0 -> undef142, x2^0 -> undef144, rest remain the same}>
<l11, l13, 1 <= undef203 /\ x0^0 = undef201 /\ x1^0 = undef202 /\ x2^0 = undef203, {x0^0 -> undef201, x1^0 -> undef202, x2^0 -> undef203, rest remain the same}>
<l13, l10, 2 <= undef164 /\ x0^0 = undef161 /\ x1^0 = undef162 /\ x2^0 = undef163, {x0^0 -> undef161, x1^0 -> undef162, x2^0 -> undef163, rest remain the same}>
<l13, l10, undef174 <= 0 /\ x0^0 = undef171 /\ x1^0 = undef172 /\ x2^0 = undef173, {x0^0 -> undef171, x1^0 -> undef172, x2^0 -> undef173, rest remain the same}>
<l13, l10, x0^0 = undef181 /\ x1^0 = undef182 /\ x2^0 = undef183 /\ undef151 = undef181 /\ undef152 = undef182 /\ undef153 = undef183 /\ undef184 = 1, {x0^0 -> undef151, x1^0 -> undef152, x2^0 -> undef153, rest remain the same}>
Variables:
x0^0, x1^0, x2^0

Graph 5:
Transitions:
Variables:

Precedence: 
Graph 0

Graph 1
<l0, l7, undef102 <= 0 /\ x0^0 = undef251 /\ x1^0 = undef252 /\ undef101 = undef111 /\ undef102 = undef112 /\ undef111 = undef251 /\ undef112 = undef252, {x0^0 -> undef101, x1^0 -> undef102, x2^0 -> undef104, rest remain the same}>
<l0, l7, true, {all remain the same}>
<l0, l7, undef102 <= 0 /\ x0^0 = undef101 /\ x1^0 = undef102, {x0^0 -> undef101, x1^0 -> undef102, x2^0 -> undef104, rest remain the same}>
<l0, l7, undef102 <= 0 /\ x0^0 = undef111 /\ x1^0 = undef112 /\ undef101 = undef111 /\ undef102 = undef112, {x0^0 -> undef101, x1^0 -> undef102, x2^0 -> undef104, rest remain the same}>

Graph 2
<l0, l6, 1 <= undef92 /\ x0^0 = undef251 /\ x1^0 = undef252 /\ undef91 = undef111 /\ undef92 = undef112 /\ undef111 = undef251 /\ undef112 = undef252, {x0^0 -> undef91, x1^0 -> undef92, x2^0 -> undef94, rest remain the same}>
<l0, l6, true, {all remain the same}>
<l0, l6, 1 <= undef92 /\ x0^0 = undef91 /\ x1^0 = undef92, {x0^0 -> undef91, x1^0 -> undef92, x2^0 -> undef94, rest remain the same}>
<l0, l6, 1 <= undef92 /\ x0^0 = undef111 /\ x1^0 = undef112 /\ undef91 = undef111 /\ undef92 = undef112, {x0^0 -> undef91, x1^0 -> undef92, x2^0 -> undef94, rest remain the same}>

Graph 3
<l0, l4, x0^0 = undef11 /\ x1^0 = undef12, {x0^0 -> undef11, x1^0 -> undef12, x2^0 -> undef14, rest remain the same}>
<l0, l4, true, {all remain the same}>
<l6, l4, 2 <= undef32 /\ x0^0 = undef31 /\ x1^0 = undef32 /\ undef11 = undef31 /\ undef12 = undef32, {x0^0 -> undef11, x1^0 -> undef12, x2^0 -> undef14, rest remain the same}>
<l6, l4, undef42 <= 0 /\ x0^0 = undef41 /\ x1^0 = undef42 /\ undef11 = undef41 /\ undef12 = undef42, {x0^0 -> undef11, x1^0 -> undef12, x2^0 -> undef14, rest remain the same}>
<l7, l4, 1 <= undef62 /\ x0^0 = undef61 /\ x1^0 = undef62 /\ undef11 = undef61 /\ undef12 = undef62, {x0^0 -> undef11, x1^0 -> undef12, x2^0 -> undef14, rest remain the same}>
<l7, l4, 1 + undef72 <= 0 /\ x0^0 = undef71 /\ x1^0 = undef72 /\ undef11 = undef71 /\ undef12 = undef72, {x0^0 -> undef11, x1^0 -> undef12, x2^0 -> undef14, rest remain the same}>

Graph 4
<l0, l10, true, {all remain the same}>
<l0, l10, x0^0 = undef151 /\ x1^0 = undef152 /\ x2^0 = undef153, {x0^0 -> undef151, x1^0 -> undef152, x2^0 -> undef153, rest remain the same}>
<l0, l13, true, {all remain the same}>
<l0, l11, true, {all remain the same}>
<l4, l11, 3 <= undef221 /\ x0^0 = undef221 /\ x1^0 = undef222, {x0^0 -> undef221, x1^0 -> undef222, x2^0 -> undef222, rest remain the same}>
<l4, l11, undef231 <= 1 /\ x0^0 = undef231 /\ x1^0 = undef232, {x0^0 -> undef231, x1^0 -> undef232, x2^0 -> undef232, rest remain the same}>

Graph 5
<l0, l2, true, {all remain the same}>
<l0, l2, true, {x0^0 -> undef4, x1^0 -> undef5, x2^0 -> undef6, rest remain the same}>
<l0, l2, true, {x0^0 -> undef24, x1^0 -> undef25, x2^0 -> undef26, rest remain the same}>
<l0, l2, true, {x0^0 -> undef214, x1^0 -> undef215, x2^0 -> undef216, rest remain the same}>
<l4, l2, x0^0 = undef241 /\ x1^0 = undef242 /\ undef241 = 2, {x0^0 -> undef214, x1^0 -> undef215, x2^0 -> undef216, rest remain the same}>
<l6, l2, x0^0 = undef51 /\ x1^0 = undef52 /\ undef52 = 1, {x0^0 -> undef4, x1^0 -> undef5, x2^0 -> undef6, rest remain the same}>
<l7, l2, x0^0 = undef81 /\ x1^0 = undef82 /\ undef82 = 0, {x0^0 -> undef24, x1^0 -> undef25, x2^0 -> undef26, rest remain the same}>
<l10, l2, 2 + 2*undef127 <= undef123 /\ x2^0 = undef123, {x0^0 -> undef124, x1^0 -> undef125, x2^0 -> undef126, rest remain the same}>
<l10, l2, 1 + undef133 <= 2*undef137 /\ x2^0 = undef133, {x0^0 -> undef134, x1^0 -> undef135, x2^0 -> undef136, rest remain the same}>
<l11, l2, undef193 <= 0 /\ x0^0 = undef191 /\ x1^0 = undef192 /\ x2^0 = undef193, {x0^0 -> undef24, x1^0 -> undef25, x2^0 -> undef26, rest remain the same}>

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

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

Proving termination of subgraph 0
Proving termination of subgraph 1
Analyzing SCC {l7}...
No cycles found.

Proving termination of subgraph 2
Analyzing SCC {l6}...
No cycles found.

Proving termination of subgraph 3
Analyzing SCC {l4}...
No cycles found.

Proving termination of subgraph 4
Checking unfeasibility...
Time used: 0.007391

Checking conditional termination of SCC {l10, l11, l13}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001952s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011584s
Trying to remove transition: <l13, l10, x0^0 = undef181 /\ x1^0 = undef182 /\ x2^0 = undef183 /\ undef151 = undef181 /\ undef152 = undef182 /\ undef153 = undef183 /\ undef184 = 1, {x0^0 -> undef151, x1^0 -> undef152, x2^0 -> undef153, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.009723s
Time used: 0.008418
Trying to remove transition: <l13, l10, undef174 <= 0 /\ x0^0 = undef171 /\ x1^0 = undef172 /\ x2^0 = undef173, {x0^0 -> undef171, x1^0 -> undef172, x2^0 -> undef173, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.009230s
Time used: 0.007843
Trying to remove transition: <l13, l10, 2 <= undef164 /\ x0^0 = undef161 /\ x1^0 = undef162 /\ x2^0 = undef163, {x0^0 -> undef161, x1^0 -> undef162, x2^0 -> undef163, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.008989s
Time used: 0.007648
Trying to remove transition: <l11, l13, 1 <= undef203 /\ x0^0 = undef201 /\ x1^0 = undef202 /\ x2^0 = undef203, {x0^0 -> undef201, x1^0 -> undef202, x2^0 -> undef203, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.009242s
Time used: 0.007893
Trying to remove transition: <l10, l11, 2*undef144 <= undef143 /\ undef143 <= 1 + 2*undef144 /\ x0^0 = undef141 /\ x1^0 = undef142 /\ x2^0 = undef143, {x0^0 -> undef141, x1^0 -> undef142, x2^0 -> undef144, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.118178s
Time used: 0.118166

LOG: SAT solveNonLinear - Elapsed time: 0.160741s
Cost: 3; Total time: 0.159076
Failed at location 10: 1 <= x2^0
Failed at location 10: 1 <= x2^0
Failed at location 13: 1 <= x2^0
Before Improving: 
Quasi-invariant at l10: 1 <= x2^0
Quasi-invariant at l13: 1 <= x2^0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.015214s
Remaining time after improvement: 0.995055
Termination implied by a set of quasi-invariant(s):
Quasi-invariant at l10: 1 <= x2^0
Quasi-invariant at l13: 1 <= x2^0
[ Invariant Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l10, l11, 2*undef144 <= undef143 /\ 1 <= x2^0 /\ undef143 <= 1 + 2*undef144 /\ x0^0 = undef141 /\ x1^0 = undef142 /\ x2^0 = undef143, {x0^0 -> undef141, x1^0 -> undef142, x2^0 -> undef144, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l13, l10, 2 <= undef164 /\ 1 <= x2^0 /\ x0^0 = undef161 /\ x1^0 = undef162 /\ x2^0 = undef163, {x0^0 -> undef161, x1^0 -> undef162, x2^0 -> undef163, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l13, l10, undef174 <= 0 /\ 1 <= x2^0 /\ x0^0 = undef171 /\ x1^0 = undef172 /\ x2^0 = undef173, {x0^0 -> undef171, x1^0 -> undef172, x2^0 -> undef173, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l13, l10, 1 <= x2^0 /\ x0^0 = undef181 /\ x1^0 = undef182 /\ x2^0 = undef183 /\ undef151 = undef181 /\ undef152 = undef182 /\ undef153 = undef183 /\ undef184 = 1, {x0^0 -> undef151, x1^0 -> undef152, x2^0 -> undef153, rest remain the same}>
[ Termination Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l10, l11, 2*undef144 <= undef143 /\ 1 <= x2^0 /\ undef143 <= 1 + 2*undef144 /\ x0^0 = undef141 /\ x1^0 = undef142 /\ x2^0 = undef143, {x0^0 -> undef141, x1^0 -> undef142, x2^0 -> undef144, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l13, l10, 2 <= undef164 /\ 1 <= x2^0 /\ x0^0 = undef161 /\ x1^0 = undef162 /\ x2^0 = undef163, {x0^0 -> undef161, x1^0 -> undef162, x2^0 -> undef163, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l13, l10, undef174 <= 0 /\ 1 <= x2^0 /\ x0^0 = undef171 /\ x1^0 = undef172 /\ x2^0 = undef173, {x0^0 -> undef171, x1^0 -> undef172, x2^0 -> undef173, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l13, l10, 1 <= x2^0 /\ x0^0 = undef181 /\ x1^0 = undef182 /\ x2^0 = undef183 /\ undef151 = undef181 /\ undef152 = undef182 /\ undef153 = undef183 /\ undef184 = 1, {x0^0 -> undef151, x1^0 -> undef152, x2^0 -> undef153, rest remain the same}>
Ranking function: x2^0
New Graphs: 
Calling Safety with literal 1 <= x2^0 and entry <l0, l10, true, {all remain the same}>

LOG: CALL check - Post:1 <= x2^0 - Process 1
* Exit transition: <l0, l10, true, {all remain the same}>
* Postcondition  : 1 <= x2^0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.000415s
Calling Safety with literal 1 <= x2^0 and entry <l0, l10, x0^0 = undef151 /\ x1^0 = undef152 /\ x2^0 = undef153, {x0^0 -> undef151, x1^0 -> undef152, x2^0 -> undef153, rest remain the same}>

LOG: CALL check - Post:1 <= x2^0 - Process 2
* Exit transition: <l0, l10, x0^0 = undef151 /\ x1^0 = undef152 /\ x2^0 = undef153, {x0^0 -> undef151, x1^0 -> undef152, x2^0 -> undef153, rest remain the same}>
* Postcondition  : 1 <= x2^0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.000525s
Calling Safety with literal 1 <= x2^0 and entry <l0, l13, true, {all remain the same}>

LOG: CALL check - Post:1 <= x2^0 - Process 3
* Exit transition: <l0, l13, true, {all remain the same}>
* Postcondition  : 1 <= x2^0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.000400s
INVARIANTS: 
10: 
13: 
Quasi-INVARIANTS to narrow Graph: 
10: 1 <= x2^0 , 
13: 1 <= x2^0 , 
Narrowing transition: 
<l10, l11, 2*undef144 <= undef143 /\ undef143 <= 1 + 2*undef144 /\ x0^0 = undef141 /\ x1^0 = undef142 /\ x2^0 = undef143, {x0^0 -> undef141, x1^0 -> undef142, x2^0 -> undef144, rest remain the same}>

LOG: Narrow transition size 1
It's unfeasible. Removing transition: 
<l11, l13, 1 <= undef203 /\ x0^0 = undef201 /\ x1^0 = undef202 /\ x2^0 = undef203, {x0^0 -> undef201, x1^0 -> undef202, x2^0 -> undef203, rest remain the same}>
Narrowing transition: 
<l13, l10, 2 <= undef164 /\ x0^0 = undef161 /\ x1^0 = undef162 /\ x2^0 = undef163, {x0^0 -> undef161, x1^0 -> undef162, x2^0 -> undef163, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l13, l10, undef174 <= 0 /\ x0^0 = undef171 /\ x1^0 = undef172 /\ x2^0 = undef173, {x0^0 -> undef171, x1^0 -> undef172, x2^0 -> undef173, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l13, l10, x0^0 = undef181 /\ x1^0 = undef182 /\ x2^0 = undef183 /\ undef151 = undef181 /\ undef152 = undef182 /\ undef153 = undef183 /\ undef184 = 1, {x0^0 -> undef151, x1^0 -> undef152, x2^0 -> undef153, rest remain the same}>

LOG: Narrow transition size 1
invGraph after Narrowing: 
Transitions:
<l10, l11, x2^0 <= 0 /\ 2*undef144 <= undef143 /\ undef143 <= 1 + 2*undef144 /\ x0^0 = undef141 /\ x1^0 = undef142 /\ x2^0 = undef143, {x0^0 -> undef141, x1^0 -> undef142, x2^0 -> undef144, rest remain the same}>
<l13, l10, x2^0 <= 0 /\ 2 <= undef164 /\ x0^0 = undef161 /\ x1^0 = undef162 /\ x2^0 = undef163, {x0^0 -> undef161, x1^0 -> undef162, x2^0 -> undef163, rest remain the same}>
<l13, l10, x2^0 <= 0 /\ undef174 <= 0 /\ x0^0 = undef171 /\ x1^0 = undef172 /\ x2^0 = undef173, {x0^0 -> undef171, x1^0 -> undef172, x2^0 -> undef173, rest remain the same}>
<l13, l10, x2^0 <= 0 /\ x0^0 = undef181 /\ x1^0 = undef182 /\ x2^0 = undef183 /\ undef151 = undef181 /\ undef152 = undef182 /\ undef153 = undef183 /\ undef184 = 1, {x0^0 -> undef151, x1^0 -> undef152, x2^0 -> undef153, rest remain the same}>
Variables:
x0^0, x1^0, x2^0
Proving termination of subgraph 5
Analyzing SCC {l2}...
No cycles found.

Program Terminates