YES

Solver Timeout: 4
Global Timeout: 300
No parsing errors!
Init Location: 0
Transitions:
<l0, l23, true>
<l1, l2, (undef1 = (0 + x0^0)) /\ (undef9 = (0 + x1^0)) /\ (undef10 = (0 + x2^0)) /\ (undef11 = (0 + x3^0)) /\ (undef12 = (0 + x4^0)) /\ (undef16 = undef16) /\ (undef17 = undef17) /\ (undef2 = undef2) /\ ((0 + undef12) <= 5551), par{oldX0^0 -> undef1, oldX10^0 -> undef2, oldX1^0 -> undef9, oldX2^0 -> undef10, oldX3^0 -> undef11, oldX4^0 -> undef12, oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> (0 + x7^0), oldX8^0 -> undef16, oldX9^0 -> undef17, x0^0 -> (0 + undef1), x1^0 -> (0 + undef9), x2^0 -> (0 + undef10), x3^0 -> (0 + undef11), x4^0 -> (0 + undef12), x5^0 -> (0 + undef16), x6^0 -> (0 + undef17), x7^0 -> (0 + undef2)}>
<l1, l3, (undef26 = (0 + x0^0)) /\ (undef34 = (0 + x1^0)) /\ (undef35 = (0 + x2^0)) /\ (undef36 = (0 + x3^0)) /\ (undef37 = (0 + x4^0)) /\ (undef41 = undef41) /\ (undef42 = undef42) /\ (undef27 = undef27) /\ (5552 <= (0 + undef37)), par{oldX0^0 -> undef26, oldX10^0 -> undef27, oldX1^0 -> undef34, oldX2^0 -> undef35, oldX3^0 -> undef36, oldX4^0 -> undef37, oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> (0 + x7^0), oldX8^0 -> undef41, oldX9^0 -> undef42, x0^0 -> (0 + undef26), x1^0 -> (0 + undef34), x2^0 -> (0 + undef35), x3^0 -> (0 + undef36), x4^0 -> (0 + undef37), x5^0 -> (0 + undef41), x6^0 -> (0 + undef42), x7^0 -> (0 + undef27)}>
<l4, l5, (undef51 = (0 + x0^0)) /\ (undef59 = (0 + x1^0)) /\ (undef60 = (0 + x2^0)) /\ (undef61 = (0 + x3^0)) /\ (undef62 = (0 + x4^0)) /\ (undef63 = (0 + x5^0)) /\ (undef66 = undef66) /\ (1 <= (0 + undef62)), par{oldX0^0 -> undef51, oldX1^0 -> undef59, oldX2^0 -> undef60, oldX3^0 -> undef61, oldX4^0 -> undef62, oldX5^0 -> undef63, oldX6^0 -> (0 + x6^0), oldX7^0 -> (0 + x7^0), oldX8^0 -> undef66, x0^0 -> (0 + undef51), x1^0 -> (0 + undef59), x2^0 -> (0 + undef60), x3^0 -> (0 + undef61), x4^0 -> (0 + undef62), x5^0 -> (0 + undef63), x6^0 -> (~(1) + undef62), x7^0 -> (0 + undef66)}>
<l4, l6, (undef76 = (0 + x0^0)) /\ (undef84 = (0 + x1^0)) /\ (undef85 = (0 + x2^0)) /\ (undef86 = (0 + x3^0)) /\ (undef87 = (0 + x4^0)) /\ (undef88 = (0 + x5^0)) /\ (undef91 = undef91) /\ ((0 + undef87) <= 0), par{oldX0^0 -> undef76, oldX1^0 -> undef84, oldX2^0 -> undef85, oldX3^0 -> undef86, oldX4^0 -> undef87, oldX5^0 -> undef88, oldX6^0 -> (0 + x6^0), oldX7^0 -> (0 + x7^0), oldX8^0 -> undef91, x0^0 -> (0 + undef76), x1^0 -> (0 + undef84), x2^0 -> (0 + undef85), x3^0 -> (0 + undef86), x4^0 -> (0 + undef87), x5^0 -> (0 + undef88), x6^0 -> (~(1) + undef87), x7^0 -> (0 + undef91)}>
<l7, l1, (undef101 = (0 + x0^0)) /\ (undef109 = (0 + x1^0)) /\ (undef110 = (0 + x2^0)) /\ (undef111 = (0 + x3^0)) /\ (undef116 = undef116) /\ (undef117 = undef117) /\ (undef102 = undef102) /\ (16 <= (0 + undef109)), par{oldX0^0 -> undef101, oldX10^0 -> undef102, oldX1^0 -> undef109, oldX2^0 -> undef110, oldX3^0 -> undef111, oldX4^0 -> (0 + x4^0), oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> (0 + x7^0), oldX8^0 -> undef116, oldX9^0 -> undef117, x0^0 -> (0 + undef101), x1^0 -> (0 + undef109), x2^0 -> (0 + undef110), x3^0 -> (0 + undef111), x4^0 -> (0 + undef109), x5^0 -> (0 + undef116), x6^0 -> (0 + undef117), x7^0 -> (0 + undef102)}>
<l7, l4, (undef126 = (0 + x0^0)) /\ (undef134 = (0 + x1^0)) /\ (undef135 = (0 + x2^0)) /\ (undef136 = (0 + x3^0)) /\ (undef141 = undef141) /\ (undef142 = undef142) /\ ((0 + undef134) <= 15), par{oldX0^0 -> undef126, oldX1^0 -> undef134, oldX2^0 -> undef135, oldX3^0 -> undef136, oldX4^0 -> (0 + x4^0), oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> (0 + x7^0), oldX8^0 -> undef141, oldX9^0 -> undef142, x0^0 -> (0 + undef126), x1^0 -> (0 + undef134), x2^0 -> (0 + undef135), x3^0 -> (0 + undef136), x4^0 -> (0 + undef134), x5^0 -> (0 + undef136), x6^0 -> (0 + undef141), x7^0 -> (0 + undef142)}>
<l8, l9, (undef166 = undef166) /\ (undef167 = undef167) /\ (undef152 = undef152) /\ (undef153 = undef153) /\ (undef154 = undef154) /\ (undef155 = undef155) /\ (undef156 = undef156) /\ (undef157 = undef157), par{oldX0^0 -> (0 + x0^0), oldX10^0 -> undef152, oldX11^0 -> undef153, oldX12^0 -> undef154, oldX13^0 -> undef155, oldX14^0 -> undef156, oldX15^0 -> undef157, oldX1^0 -> (0 + x1^0), oldX2^0 -> (0 + x2^0), oldX3^0 -> (0 + x3^0), oldX4^0 -> (0 + x4^0), oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> (0 + x7^0), oldX8^0 -> undef166, oldX9^0 -> undef167, x0^0 -> (0 + undef166), x1^0 -> (0 + undef167), x2^0 -> (0 + undef152), x3^0 -> (0 + undef153), x4^0 -> (0 + undef154), x5^0 -> (0 + undef155), x6^0 -> (0 + undef156), x7^0 -> (0 + undef157)}>
<l10, l7, (undef176 = (0 + x0^0)) /\ (undef184 = (0 + x1^0)) /\ (undef185 = (0 + x2^0)) /\ (undef186 = (0 + x3^0)) /\ (undef191 = undef191) /\ (undef192 = undef192) /\ (undef177 = undef177) /\ (undef178 = undef178), par{oldX0^0 -> undef176, oldX10^0 -> undef177, oldX11^0 -> undef178, oldX1^0 -> undef184, oldX2^0 -> undef185, oldX3^0 -> undef186, oldX4^0 -> (0 + x4^0), oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> (0 + x7^0), oldX8^0 -> undef191, oldX9^0 -> undef192, x0^0 -> (0 + undef176), x1^0 -> (0 + undef184), x2^0 -> (0 + undef185), x3^0 -> (0 + undef186), x4^0 -> (0 + undef191), x5^0 -> (0 + undef192), x6^0 -> (0 + undef177), x7^0 -> (0 + undef178)}>
<l10, l8, (undef201 = (0 + x0^0)) /\ (undef209 = (0 + x1^0)) /\ (undef210 = (0 + x2^0)) /\ (undef211 = (0 + x3^0)) /\ (undef216 = undef216) /\ (undef217 = undef217) /\ (undef202 = undef202) /\ (undef203 = undef203), par{oldX0^0 -> undef201, oldX10^0 -> undef202, oldX11^0 -> undef203, oldX1^0 -> undef209, oldX2^0 -> undef210, oldX3^0 -> undef211, oldX4^0 -> (0 + x4^0), oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> (0 + x7^0), oldX8^0 -> undef216, oldX9^0 -> undef217, x0^0 -> (0 + undef201), x1^0 -> (0 + undef209), x2^0 -> (0 + undef210), x3^0 -> (0 + undef211), x4^0 -> (0 + undef216), x5^0 -> (0 + undef217), x6^0 -> (0 + undef202), x7^0 -> (0 + undef203)}>
<l11, l9, (undef235 = (0 + x2^0)) /\ (undef236 = (0 + x3^0)) /\ (undef241 = undef241) /\ (undef242 = undef242) /\ (undef227 = undef227) /\ (undef228 = undef228) /\ (undef229 = undef229) /\ (undef230 = undef230) /\ (undef231 = undef231) /\ (undef232 = undef232) /\ (undef233 = undef233) /\ (((0 + undef233) + undef236) <= 65520) /\ ((((0 + undef233) + undef235) + undef236) <= 65520), par{oldX0^0 -> (0 + x0^0), oldX10^0 -> undef227, oldX11^0 -> undef228, oldX12^0 -> undef229, oldX13^0 -> undef230, oldX14^0 -> undef231, oldX15^0 -> undef232, oldX16^0 -> undef233, oldX1^0 -> (0 + x1^0), oldX2^0 -> undef235, oldX3^0 -> undef236, oldX4^0 -> (0 + x4^0), oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> (0 + x7^0), oldX8^0 -> undef241, oldX9^0 -> undef242, x0^0 -> (0 + undef241), x1^0 -> (0 + undef242), x2^0 -> (0 + undef227), x3^0 -> (0 + undef228), x4^0 -> (0 + undef229), x5^0 -> (0 + undef230), x6^0 -> (0 + undef231), x7^0 -> (0 + undef232)}>
<l11, l9, (undef260 = (0 + x2^0)) /\ (undef261 = (0 + x3^0)) /\ (undef266 = undef266) /\ (undef267 = undef267) /\ (undef252 = undef252) /\ (undef253 = undef253) /\ (undef254 = undef254) /\ (undef255 = undef255) /\ (undef256 = undef256) /\ (undef257 = undef257) /\ (undef258 = undef258) /\ (((0 + undef258) + undef261) <= 65520) /\ (65521 <= (((0 + undef258) + undef260) + undef261)), par{oldX0^0 -> (0 + x0^0), oldX10^0 -> undef252, oldX11^0 -> undef253, oldX12^0 -> undef254, oldX13^0 -> undef255, oldX14^0 -> undef256, oldX15^0 -> undef257, oldX16^0 -> undef258, oldX1^0 -> (0 + x1^0), oldX2^0 -> undef260, oldX3^0 -> undef261, oldX4^0 -> (0 + x4^0), oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> (0 + x7^0), oldX8^0 -> undef266, oldX9^0 -> undef267, x0^0 -> (0 + undef266), x1^0 -> (0 + undef267), x2^0 -> (0 + undef252), x3^0 -> (0 + undef253), x4^0 -> (0 + undef254), x5^0 -> (0 + undef255), x6^0 -> (0 + undef256), x7^0 -> (0 + undef257)}>
<l11, l9, (undef285 = (0 + x2^0)) /\ (undef286 = (0 + x3^0)) /\ (undef291 = undef291) /\ (undef292 = undef292) /\ (undef277 = undef277) /\ (undef278 = undef278) /\ (undef279 = undef279) /\ (undef280 = undef280) /\ (undef281 = undef281) /\ (undef282 = undef282) /\ (undef283 = undef283) /\ (65521 <= ((0 + undef283) + undef286)) /\ ((((~(65521) + undef283) + undef285) + undef286) <= 65520), par{oldX0^0 -> (0 + x0^0), oldX10^0 -> undef277, oldX11^0 -> undef278, oldX12^0 -> undef279, oldX13^0 -> undef280, oldX14^0 -> undef281, oldX15^0 -> undef282, oldX16^0 -> undef283, oldX1^0 -> (0 + x1^0), oldX2^0 -> undef285, oldX3^0 -> undef286, oldX4^0 -> (0 + x4^0), oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> (0 + x7^0), oldX8^0 -> undef291, oldX9^0 -> undef292, x0^0 -> (0 + undef291), x1^0 -> (0 + undef292), x2^0 -> (0 + undef277), x3^0 -> (0 + undef278), x4^0 -> (0 + undef279), x5^0 -> (0 + undef280), x6^0 -> (0 + undef281), x7^0 -> (0 + undef282)}>
<l11, l9, (undef310 = (0 + x2^0)) /\ (undef311 = (0 + x3^0)) /\ (undef316 = undef316) /\ (undef317 = undef317) /\ (undef302 = undef302) /\ (undef303 = undef303) /\ (undef304 = undef304) /\ (undef305 = undef305) /\ (undef306 = undef306) /\ (undef307 = undef307) /\ (undef308 = undef308) /\ (65521 <= ((0 + undef308) + undef311)) /\ (65521 <= (((~(65521) + undef308) + undef310) + undef311)), par{oldX0^0 -> (0 + x0^0), oldX10^0 -> undef302, oldX11^0 -> undef303, oldX12^0 -> undef304, oldX13^0 -> undef305, oldX14^0 -> undef306, oldX15^0 -> undef307, oldX16^0 -> undef308, oldX1^0 -> (0 + x1^0), oldX2^0 -> undef310, oldX3^0 -> undef311, oldX4^0 -> (0 + x4^0), oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> (0 + x7^0), oldX8^0 -> undef316, oldX9^0 -> undef317, x0^0 -> (0 + undef316), x1^0 -> (0 + undef317), x2^0 -> (0 + undef302), x3^0 -> (0 + undef303), x4^0 -> (0 + undef304), x5^0 -> (0 + undef305), x6^0 -> (0 + undef306), x7^0 -> (0 + undef307)}>
<l12, l13, (undef326 = (0 + x0^0)) /\ (undef334 = (0 + x1^0)) /\ (undef335 = (0 + x2^0)) /\ (undef336 = (0 + x3^0)) /\ (undef337 = (0 + x4^0)) /\ (undef338 = (0 + x5^0)) /\ (undef340 = (0 + x7^0)) /\ (undef341 = undef341), par{oldX0^0 -> undef326, oldX1^0 -> undef334, oldX2^0 -> undef335, oldX3^0 -> undef336, oldX4^0 -> undef337, oldX5^0 -> undef338, oldX6^0 -> (0 + x6^0), oldX7^0 -> undef340, oldX8^0 -> undef341, x0^0 -> (0 + undef326), x1^0 -> (0 + undef334), x2^0 -> (0 + undef335), x3^0 -> (0 + undef336), x4^0 -> (0 + undef337), x5^0 -> (0 + undef338), x6^0 -> (0 + undef340), x7^0 -> (0 + undef341)}>
<l14, l15, (undef351 = (0 + x0^0)) /\ (undef359 = (0 + x1^0)) /\ (undef360 = (0 + x2^0)) /\ (undef361 = (0 + x3^0)) /\ (undef362 = (0 + x4^0)) /\ (undef366 = undef366) /\ (undef367 = undef367) /\ (undef352 = undef352), par{oldX0^0 -> undef351, oldX10^0 -> undef352, oldX1^0 -> undef359, oldX2^0 -> undef360, oldX3^0 -> undef361, oldX4^0 -> undef362, oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> (0 + x7^0), oldX8^0 -> undef366, oldX9^0 -> undef367, x0^0 -> (0 + undef351), x1^0 -> (0 + undef359), x2^0 -> (0 + undef360), x3^0 -> (0 + undef361), x4^0 -> (0 + undef362), x5^0 -> (0 + undef366), x6^0 -> (0 + undef367), x7^0 -> (0 + undef352)}>
<l16, l10, (undef376 = (0 + x0^0)) /\ (undef384 = (0 + x1^0)) /\ (undef391 = undef391) /\ (undef392 = undef392) /\ (undef377 = undef377) /\ (undef378 = undef378) /\ (undef379 = undef379) /\ (undef380 = undef380) /\ (2 <= (0 + undef384)), par{oldX0^0 -> undef376, oldX10^0 -> undef377, oldX11^0 -> undef378, oldX12^0 -> undef379, oldX13^0 -> undef380, oldX1^0 -> undef384, oldX2^0 -> (0 + x2^0), oldX3^0 -> (0 + x3^0), oldX4^0 -> (0 + x4^0), oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> (0 + x7^0), oldX8^0 -> undef391, oldX9^0 -> undef392, x0^0 -> (0 + undef376), x1^0 -> (0 + undef384), x2^0 -> (0 + undef391), x3^0 -> (0 + undef392), x4^0 -> (0 + undef377), x5^0 -> (0 + undef378), x6^0 -> (0 + undef379), x7^0 -> (0 + undef380)}>
<l16, l10, (undef401 = (0 + x0^0)) /\ (undef409 = (0 + x1^0)) /\ (undef416 = undef416) /\ (undef417 = undef417) /\ (undef402 = undef402) /\ (undef403 = undef403) /\ (undef404 = undef404) /\ (undef405 = undef405) /\ ((1 + undef409) <= 1), par{oldX0^0 -> undef401, oldX10^0 -> undef402, oldX11^0 -> undef403, oldX12^0 -> undef404, oldX13^0 -> undef405, oldX1^0 -> undef409, oldX2^0 -> (0 + x2^0), oldX3^0 -> (0 + x3^0), oldX4^0 -> (0 + x4^0), oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> (0 + x7^0), oldX8^0 -> undef416, oldX9^0 -> undef417, x0^0 -> (0 + undef401), x1^0 -> (0 + undef409), x2^0 -> (0 + undef416), x3^0 -> (0 + undef417), x4^0 -> (0 + undef402), x5^0 -> (0 + undef403), x6^0 -> (0 + undef404), x7^0 -> (0 + undef405)}>
<l16, l11, (undef426 = (0 + x0^0)) /\ (undef434 = (0 + x1^0)) /\ (undef441 = undef441) /\ (undef442 = undef442) /\ (undef427 = undef427) /\ (undef428 = undef428) /\ (undef429 = undef429) /\ (undef430 = undef430) /\ ((0 + undef434) <= 1) /\ (1 <= (0 + undef434)), par{oldX0^0 -> undef426, oldX10^0 -> undef427, oldX11^0 -> undef428, oldX12^0 -> undef429, oldX13^0 -> undef430, oldX1^0 -> undef434, oldX2^0 -> (0 + x2^0), oldX3^0 -> (0 + x3^0), oldX4^0 -> (0 + x4^0), oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> (0 + x7^0), oldX8^0 -> undef441, oldX9^0 -> undef442, x0^0 -> (0 + undef426), x1^0 -> (0 + undef434), x2^0 -> (0 + undef441), x3^0 -> (0 + undef442), x4^0 -> (0 + undef427), x5^0 -> (0 + undef428), x6^0 -> (0 + undef429), x7^0 -> (0 + undef430)}>
<l13, l12, (undef451 = (0 + x0^0)) /\ (undef459 = (0 + x1^0)) /\ (undef460 = (0 + x2^0)) /\ (undef461 = (0 + x3^0)) /\ (undef462 = (0 + x4^0)) /\ (undef463 = (0 + x5^0)) /\ (undef464 = (0 + x6^0)) /\ (1 <= (0 + undef464)), par{oldX0^0 -> undef451, oldX1^0 -> undef459, oldX2^0 -> undef460, oldX3^0 -> undef461, oldX4^0 -> undef462, oldX5^0 -> undef463, oldX6^0 -> undef464, oldX7^0 -> (0 + x7^0), x0^0 -> (0 + undef451), x1^0 -> (0 + undef459), x2^0 -> (0 + undef460), x3^0 -> (0 + undef461), x4^0 -> (0 + undef462), x5^0 -> (0 + undef463), x6^0 -> (0 + undef464), x7^0 -> (~(1) + undef464)}>
<l13, l14, (undef476 = (0 + x0^0)) /\ (undef484 = (0 + x1^0)) /\ (undef485 = (0 + x2^0)) /\ (undef486 = (0 + x3^0)) /\ (undef487 = (0 + x4^0)) /\ (undef488 = (0 + x5^0)) /\ (undef489 = (0 + x6^0)) /\ ((0 + undef489) <= 0), par{oldX0^0 -> undef476, oldX1^0 -> undef484, oldX2^0 -> undef485, oldX3^0 -> undef486, oldX4^0 -> undef487, oldX5^0 -> undef488, oldX6^0 -> undef489, oldX7^0 -> (0 + x7^0), x0^0 -> (0 + undef476), x1^0 -> (0 + undef484), x2^0 -> (0 + undef485), x3^0 -> (0 + undef486), x4^0 -> (0 + undef487), x5^0 -> (0 + undef488), x6^0 -> (0 + undef489), x7^0 -> (~(1) + undef489)}>
<l17, l18, (undef501 = (0 + x0^0)) /\ (undef509 = (0 + x1^0)) /\ (undef510 = (0 + x2^0)) /\ (undef511 = (0 + x3^0)) /\ (undef512 = (0 + x4^0)) /\ (undef513 = (0 + x5^0)) /\ (undef516 = undef516) /\ (undef517 = undef517), par{oldX0^0 -> undef501, oldX1^0 -> undef509, oldX2^0 -> undef510, oldX3^0 -> undef511, oldX4^0 -> undef512, oldX5^0 -> undef513, oldX6^0 -> (0 + x6^0), oldX7^0 -> (0 + x7^0), oldX8^0 -> undef516, oldX9^0 -> undef517, x0^0 -> (0 + undef501), x1^0 -> (0 + undef509), x2^0 -> (0 + undef510), x3^0 -> (0 + undef511), x4^0 -> (0 + undef512), x5^0 -> (~(16) + undef513), x6^0 -> (0 + undef516), x7^0 -> (0 + undef517)}>
<l15, l9, (undef541 = undef541) /\ (undef542 = undef542) /\ (undef527 = undef527) /\ (undef528 = undef528) /\ (undef529 = undef529) /\ (undef530 = undef530) /\ (undef531 = undef531) /\ (undef532 = undef532), par{oldX0^0 -> (0 + x0^0), oldX10^0 -> undef527, oldX11^0 -> undef528, oldX12^0 -> undef529, oldX13^0 -> undef530, oldX14^0 -> undef531, oldX15^0 -> undef532, oldX1^0 -> (0 + x1^0), oldX2^0 -> (0 + x2^0), oldX3^0 -> (0 + x3^0), oldX4^0 -> (0 + x4^0), oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> (0 + x7^0), oldX8^0 -> undef541, oldX9^0 -> undef542, x0^0 -> (0 + undef541), x1^0 -> (0 + undef542), x2^0 -> (0 + undef527), x3^0 -> (0 + undef528), x4^0 -> (0 + undef529), x5^0 -> (0 + undef530), x6^0 -> (0 + undef531), x7^0 -> (0 + undef532)}>
<l18, l13, (undef551 = (0 + x0^0)) /\ (undef559 = (0 + x1^0)) /\ (undef560 = (0 + x2^0)) /\ (undef561 = (0 + x3^0)) /\ (undef562 = (0 + x4^0)) /\ (undef563 = (0 + x5^0)) /\ (undef566 = undef566) /\ ((0 + undef563) <= 15), par{oldX0^0 -> undef551, oldX1^0 -> undef559, oldX2^0 -> undef560, oldX3^0 -> undef561, oldX4^0 -> undef562, oldX5^0 -> undef563, oldX6^0 -> (0 + x6^0), oldX7^0 -> (0 + x7^0), oldX8^0 -> undef566, x0^0 -> (0 + undef551), x1^0 -> (0 + undef559), x2^0 -> (0 + undef560), x3^0 -> (0 + undef561), x4^0 -> (0 + undef562), x5^0 -> (0 + undef563), x6^0 -> (0 + undef563), x7^0 -> (0 + undef566)}>
<l18, l17, (undef576 = (0 + x0^0)) /\ (undef584 = (0 + x1^0)) /\ (undef585 = (0 + x2^0)) /\ (undef586 = (0 + x3^0)) /\ (undef587 = (0 + x4^0)) /\ (undef588 = (0 + x5^0)) /\ (undef591 = undef591) /\ (undef592 = undef592) /\ (16 <= (0 + undef588)), par{oldX0^0 -> undef576, oldX1^0 -> undef584, oldX2^0 -> undef585, oldX3^0 -> undef586, oldX4^0 -> undef587, oldX5^0 -> undef588, oldX6^0 -> (0 + x6^0), oldX7^0 -> (0 + x7^0), oldX8^0 -> undef591, oldX9^0 -> undef592, x0^0 -> (0 + undef576), x1^0 -> (0 + undef584), x2^0 -> (0 + undef585), x3^0 -> (0 + undef586), x4^0 -> (0 + undef587), x5^0 -> (0 + undef588), x6^0 -> (0 + undef591), x7^0 -> (0 + undef592)}>
<l19, l1, (undef601 = (0 + x0^0)) /\ (undef609 = (0 + x1^0)) /\ (undef610 = (0 + x2^0)) /\ (undef611 = (0 + x3^0)) /\ (undef613 = (0 + x5^0)) /\ (undef616 = undef616) /\ (undef617 = undef617) /\ (undef602 = undef602), par{oldX0^0 -> undef601, oldX10^0 -> undef602, oldX1^0 -> undef609, oldX2^0 -> undef610, oldX3^0 -> undef611, oldX4^0 -> (0 + x4^0), oldX5^0 -> undef613, oldX6^0 -> (0 + x6^0), oldX7^0 -> (0 + x7^0), oldX8^0 -> undef616, oldX9^0 -> undef617, x0^0 -> (0 + undef601), x1^0 -> (0 + undef609), x2^0 -> (0 + undef610), x3^0 -> (0 + undef611), x4^0 -> (0 + undef613), x5^0 -> (0 + undef616), x6^0 -> (0 + undef617), x7^0 -> (0 + undef602)}>
<l20, l19, (undef626 = (0 + x0^0)) /\ (undef634 = (0 + x1^0)) /\ (undef635 = (0 + x2^0)) /\ (undef636 = (0 + x3^0)) /\ (undef637 = (0 + x4^0)) /\ (undef638 = (0 + x5^0)) /\ (undef639 = (0 + x6^0)) /\ (undef641 = undef641) /\ ((~(1) + undef639) <= 0), par{oldX0^0 -> undef626, oldX1^0 -> undef634, oldX2^0 -> undef635, oldX3^0 -> undef636, oldX4^0 -> undef637, oldX5^0 -> undef638, oldX6^0 -> undef639, oldX7^0 -> (0 + x7^0), oldX8^0 -> undef641, x0^0 -> (0 + undef626), x1^0 -> (0 + undef634), x2^0 -> (0 + undef635), x3^0 -> (0 + undef636), x4^0 -> (0 + undef637), x5^0 -> (0 + undef638), x6^0 -> (0 + undef639), x7^0 -> (0 + undef641)}>
<l20, l21, (undef651 = (0 + x0^0)) /\ (undef659 = (0 + x1^0)) /\ (undef660 = (0 + x2^0)) /\ (undef661 = (0 + x3^0)) /\ (undef662 = (0 + x4^0)) /\ (undef663 = (0 + x5^0)) /\ (undef664 = (0 + x6^0)) /\ (undef666 = undef666) /\ (1 <= (~(1) + undef664)), par{oldX0^0 -> undef651, oldX1^0 -> undef659, oldX2^0 -> undef660, oldX3^0 -> undef661, oldX4^0 -> undef662, oldX5^0 -> undef663, oldX6^0 -> undef664, oldX7^0 -> (0 + x7^0), oldX8^0 -> undef666, x0^0 -> (0 + undef651), x1^0 -> (0 + undef659), x2^0 -> (0 + undef660), x3^0 -> (0 + undef661), x4^0 -> (0 + undef662), x5^0 -> (0 + undef663), x6^0 -> (~(1) + undef664), x7^0 -> (0 + undef666)}>
<l21, l20, true>
<l2, l15, (undef701 = (0 + x0^0)) /\ (undef709 = (0 + x1^0)) /\ (undef710 = (0 + x2^0)) /\ (undef711 = (0 + x3^0)) /\ (undef712 = (0 + x4^0)) /\ (undef716 = undef716) /\ (undef717 = undef717) /\ (undef702 = undef702) /\ ((0 + undef712) <= 0), par{oldX0^0 -> undef701, oldX10^0 -> undef702, oldX1^0 -> undef709, oldX2^0 -> undef710, oldX3^0 -> undef711, oldX4^0 -> undef712, oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> (0 + x7^0), oldX8^0 -> undef716, oldX9^0 -> undef717, x0^0 -> (0 + undef701), x1^0 -> (0 + undef709), x2^0 -> (0 + undef710), x3^0 -> (0 + undef711), x4^0 -> (0 + undef712), x5^0 -> (0 + undef716), x6^0 -> (0 + undef717), x7^0 -> (0 + undef702)}>
<l2, l18, (undef726 = (0 + x0^0)) /\ (undef734 = (0 + x1^0)) /\ (undef735 = (0 + x2^0)) /\ (undef736 = (0 + x3^0)) /\ (undef737 = (0 + x4^0)) /\ (undef741 = undef741) /\ (undef742 = undef742) /\ (1 <= (0 + undef737)), par{oldX0^0 -> undef726, oldX1^0 -> undef734, oldX2^0 -> undef735, oldX3^0 -> undef736, oldX4^0 -> undef737, oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> (0 + x7^0), oldX8^0 -> undef741, oldX9^0 -> undef742, x0^0 -> (0 + undef726), x1^0 -> (0 + undef734), x2^0 -> (0 + undef735), x3^0 -> (0 + undef736), x4^0 -> (0 + undef737), x5^0 -> (0 + undef737), x6^0 -> (0 + undef741), x7^0 -> (0 + undef742)}>
<l3, l20, (undef751 = (0 + x0^0)) /\ (undef759 = (0 + x1^0)) /\ (undef760 = (0 + x2^0)) /\ (undef761 = (0 + x3^0)) /\ (undef762 = (0 + x4^0)) /\ (undef766 = undef766), par{oldX0^0 -> undef751, oldX1^0 -> undef759, oldX2^0 -> undef760, oldX3^0 -> undef761, oldX4^0 -> undef762, oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> (0 + x7^0), oldX8^0 -> undef766, x0^0 -> (0 + undef751), x1^0 -> (0 + undef759), x2^0 -> (0 + undef760), x3^0 -> (0 + undef761), x4^0 -> (0 + undef762), x5^0 -> (~(5552) + undef762), x6^0 -> 347, x7^0 -> (0 + undef766)}>
<l5, l4, (undef776 = (0 + x0^0)) /\ (undef784 = (0 + x1^0)) /\ (undef785 = (0 + x2^0)) /\ (undef786 = (0 + x3^0)) /\ (undef788 = (0 + x5^0)) /\ (undef789 = (0 + x6^0)) /\ (undef791 = undef791) /\ (undef792 = undef792) /\ (undef777 = undef777), par{oldX0^0 -> undef776, oldX10^0 -> undef777, oldX1^0 -> undef784, oldX2^0 -> undef785, oldX3^0 -> undef786, oldX4^0 -> (0 + x4^0), oldX5^0 -> undef788, oldX6^0 -> undef789, oldX7^0 -> (0 + x7^0), oldX8^0 -> undef791, oldX9^0 -> undef792, x0^0 -> (0 + undef776), x1^0 -> (0 + undef784), x2^0 -> (0 + undef785), x3^0 -> (0 + undef786), x4^0 -> (0 + undef789), x5^0 -> ((0 + undef788) + undef791), x6^0 -> (0 + undef792), x7^0 -> (0 + undef777)}>
<l6, l9, (undef813 = (0 + x5^0)) /\ (undef816 = undef816) /\ (undef817 = undef817) /\ (undef802 = undef802) /\ (undef803 = undef803) /\ (undef804 = undef804) /\ (undef805 = undef805) /\ (undef806 = undef806) /\ (undef807 = undef807) /\ ((0 + undef813) <= 65520), par{oldX0^0 -> (0 + x0^0), oldX10^0 -> undef802, oldX11^0 -> undef803, oldX12^0 -> undef804, oldX13^0 -> undef805, oldX14^0 -> undef806, oldX15^0 -> undef807, oldX1^0 -> (0 + x1^0), oldX2^0 -> (0 + x2^0), oldX3^0 -> (0 + x3^0), oldX4^0 -> (0 + x4^0), oldX5^0 -> undef813, oldX6^0 -> (0 + x6^0), oldX7^0 -> (0 + x7^0), oldX8^0 -> undef816, oldX9^0 -> undef817, x0^0 -> (0 + undef816), x1^0 -> (0 + undef817), x2^0 -> (0 + undef802), x3^0 -> (0 + undef803), x4^0 -> (0 + undef804), x5^0 -> (0 + undef805), x6^0 -> (0 + undef806), x7^0 -> (0 + undef807)}>
<l6, l9, (undef838 = (0 + x5^0)) /\ (undef841 = undef841) /\ (undef842 = undef842) /\ (undef827 = undef827) /\ (undef828 = undef828) /\ (undef829 = undef829) /\ (undef830 = undef830) /\ (undef831 = undef831) /\ (undef832 = undef832) /\ (65521 <= (0 + undef838)), par{oldX0^0 -> (0 + x0^0), oldX10^0 -> undef827, oldX11^0 -> undef828, oldX12^0 -> undef829, oldX13^0 -> undef830, oldX14^0 -> undef831, oldX15^0 -> undef832, oldX1^0 -> (0 + x1^0), oldX2^0 -> (0 + x2^0), oldX3^0 -> (0 + x3^0), oldX4^0 -> (0 + x4^0), oldX5^0 -> undef838, oldX6^0 -> (0 + x6^0), oldX7^0 -> (0 + x7^0), oldX8^0 -> undef841, oldX9^0 -> undef842, x0^0 -> (0 + undef841), x1^0 -> (0 + undef842), x2^0 -> (0 + undef827), x3^0 -> (0 + undef828), x4^0 -> (0 + undef829), x5^0 -> (0 + undef830), x6^0 -> (0 + undef831), x7^0 -> (0 + undef832)}>
<l22, l16, (undef851 = (0 + x0^0)) /\ (undef859 = (0 + x1^0)) /\ (undef866 = undef866) /\ (undef867 = undef867) /\ (undef852 = undef852) /\ (undef853 = undef853) /\ (undef854 = undef854) /\ (undef855 = undef855), par{oldX0^0 -> undef851, oldX10^0 -> undef852, oldX11^0 -> undef853, oldX12^0 -> undef854, oldX13^0 -> undef855, oldX1^0 -> undef859, oldX2^0 -> (0 + x2^0), oldX3^0 -> (0 + x3^0), oldX4^0 -> (0 + x4^0), oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> (0 + x7^0), oldX8^0 -> undef866, oldX9^0 -> undef867, x0^0 -> (0 + undef851), x1^0 -> (0 + undef859), x2^0 -> (0 + undef866), x3^0 -> (0 + undef867), x4^0 -> (0 + undef852), x5^0 -> (0 + undef853), x6^0 -> (0 + undef854), x7^0 -> (0 + undef855)}>
<l22, l1, true>
<l22, l4, true>
<l22, l7, true>
<l22, l8, true>
<l22, l9, true>
<l22, l10, true>
<l22, l11, true>
<l22, l12, true>
<l22, l14, true>
<l22, l16, true>
<l22, l13, true>
<l22, l17, true>
<l22, l15, true>
<l22, l18, true>
<l22, l19, true>
<l22, l20, true>
<l22, l2, true>
<l22, l3, true>
<l22, l5, true>
<l22, l6, true>
<l23, l22, true>

Fresh variables:
undef1, undef2, undef9, undef10, undef11, undef12, undef16, undef17, undef26, undef27, undef34, undef35, undef36, undef37, undef41, undef42, undef51, undef59, undef60, undef61, undef62, undef63, undef66, undef76, undef84, undef85, undef86, undef87, undef88, undef91, undef101, undef102, undef109, undef110, undef111, undef116, undef117, undef126, undef134, undef135, undef136, undef141, undef142, undef152, undef153, undef154, undef155, undef156, undef157, undef166, undef167, undef176, undef177, undef178, undef184, undef185, undef186, undef191, undef192, undef201, undef202, undef203, undef209, undef210, undef211, undef216, undef217, undef227, undef228, undef229, undef230, undef231, undef232, undef233, undef235, undef236, undef241, undef242, undef252, undef253, undef254, undef255, undef256, undef257, undef258, undef260, undef261, undef266, undef267, undef277, undef278, undef279, undef280, undef281, undef282, undef283, undef285, undef286, undef291, undef292, undef302, undef303, undef304, undef305, undef306, undef307, undef308, undef310, undef311, undef316, undef317, undef326, undef334, undef335, undef336, undef337, undef338, undef340, undef341, undef351, undef352, undef359, undef360, undef361, undef362, undef366, undef367, undef376, undef377, undef378, undef379, undef380, undef384, undef391, undef392, undef401, undef402, undef403, undef404, undef405, undef409, undef416, undef417, undef426, undef427, undef428, undef429, undef430, undef434, undef441, undef442, undef451, undef459, undef460, undef461, undef462, undef463, undef464, undef476, undef484, undef485, undef486, undef487, undef488, undef489, undef501, undef509, undef510, undef511, undef512, undef513, undef516, undef517, undef527, undef528, undef529, undef530, undef531, undef532, undef541, undef542, undef551, undef559, undef560, undef561, undef562, undef563, undef566, undef576, undef584, undef585, undef586, undef587, undef588, undef591, undef592, undef601, undef602, undef609, undef610, undef611, undef613, undef616, undef617, undef626, undef634, undef635, undef636, undef637, undef638, undef639, undef641, undef651, undef659, undef660, undef661, undef662, undef663, undef664, undef666, undef701, undef702, undef709, undef710, undef711, undef712, undef716, undef717, undef726, undef734, undef735, undef736, undef737, undef741, undef742, undef751, undef759, undef760, undef761, undef762, undef766, undef776, undef777, undef784, undef785, undef786, undef788, undef789, undef791, undef792, undef802, undef803, undef804, undef805, undef806, undef807, undef813, undef816, undef817, undef827, undef828, undef829, undef830, undef831, undef832, undef838, undef841, undef842, undef851, undef852, undef853, undef854, undef855, undef859, undef866, undef867, 

Undef variables:
undef1, undef2, undef9, undef10, undef11, undef12, undef16, undef17, undef26, undef27, undef34, undef35, undef36, undef37, undef41, undef42, undef51, undef59, undef60, undef61, undef62, undef63, undef66, undef76, undef84, undef85, undef86, undef87, undef88, undef91, undef101, undef102, undef109, undef110, undef111, undef116, undef117, undef126, undef134, undef135, undef136, undef141, undef142, undef152, undef153, undef154, undef155, undef156, undef157, undef166, undef167, undef176, undef177, undef178, undef184, undef185, undef186, undef191, undef192, undef201, undef202, undef203, undef209, undef210, undef211, undef216, undef217, undef227, undef228, undef229, undef230, undef231, undef232, undef233, undef235, undef236, undef241, undef242, undef252, undef253, undef254, undef255, undef256, undef257, undef258, undef260, undef261, undef266, undef267, undef277, undef278, undef279, undef280, undef281, undef282, undef283, undef285, undef286, undef291, undef292, undef302, undef303, undef304, undef305, undef306, undef307, undef308, undef310, undef311, undef316, undef317, undef326, undef334, undef335, undef336, undef337, undef338, undef340, undef341, undef351, undef352, undef359, undef360, undef361, undef362, undef366, undef367, undef376, undef377, undef378, undef379, undef380, undef384, undef391, undef392, undef401, undef402, undef403, undef404, undef405, undef409, undef416, undef417, undef426, undef427, undef428, undef429, undef430, undef434, undef441, undef442, undef451, undef459, undef460, undef461, undef462, undef463, undef464, undef476, undef484, undef485, undef486, undef487, undef488, undef489, undef501, undef509, undef510, undef511, undef512, undef513, undef516, undef517, undef527, undef528, undef529, undef530, undef531, undef532, undef541, undef542, undef551, undef559, undef560, undef561, undef562, undef563, undef566, undef576, undef584, undef585, undef586, undef587, undef588, undef591, undef592, undef601, undef602, undef609, undef610, undef611, undef613, undef616, undef617, undef626, undef634, undef635, undef636, undef637, undef638, undef639, undef641, undef651, undef659, undef660, undef661, undef662, undef663, undef664, undef666, undef701, undef702, undef709, undef710, undef711, undef712, undef716, undef717, undef726, undef734, undef735, undef736, undef737, undef741, undef742, undef751, undef759, undef760, undef761, undef762, undef766, undef776, undef777, undef784, undef785, undef786, undef788, undef789, undef791, undef792, undef802, undef803, undef804, undef805, undef806, undef807, undef813, undef816, undef817, undef827, undef828, undef829, undef830, undef831, undef832, undef838, undef841, undef842, undef851, undef852, undef853, undef854, undef855, undef859, undef866, undef867, 

Abstraction variables:

Exit nodes:

Accepting locations:

Asserts:

Preprocessed LLVMGraph
Init Location: 0
Transitions:
<l0, l16, (undef851 = (0 + x0^0)) /\ (undef859 = (0 + x1^0)) /\ (undef866 = undef866) /\ (undef867 = undef867) /\ (undef852 = undef852) /\ (undef853 = undef853) /\ (undef854 = undef854) /\ (undef855 = undef855), par{x0^0 -> (0 + undef851), x1^0 -> (0 + undef859), x2^0 -> (0 + undef866), x3^0 -> (0 + undef867), x4^0 -> (0 + undef852), x5^0 -> (0 + undef853), x6^0 -> (0 + undef854), x7^0 -> (0 + undef855)}>
<l0, l1, true>
<l0, l4, true>
<l0, l7, true>
<l0, l9, (undef166 = undef166) /\ (undef167 = undef167) /\ (undef152 = undef152) /\ (undef153 = undef153) /\ (undef154 = undef154) /\ (undef155 = undef155) /\ (undef156 = undef156) /\ (undef157 = undef157), par{x0^0 -> (0 + undef166), x1^0 -> (0 + undef167), x2^0 -> (0 + undef152), x3^0 -> (0 + undef153), x4^0 -> (0 + undef154), x5^0 -> (0 + undef155), x6^0 -> (0 + undef156), x7^0 -> (0 + undef157)}>
<l0, l9, true>
<l0, l10, true>
<l0, l11, true>
<l0, l13, (undef326 = (0 + x0^0)) /\ (undef334 = (0 + x1^0)) /\ (undef335 = (0 + x2^0)) /\ (undef336 = (0 + x3^0)) /\ (undef337 = (0 + x4^0)) /\ (undef338 = (0 + x5^0)) /\ (undef340 = (0 + x7^0)) /\ (undef341 = undef341), par{x0^0 -> (0 + undef326), x1^0 -> (0 + undef334), x2^0 -> (0 + undef335), x3^0 -> (0 + undef336), x4^0 -> (0 + undef337), x5^0 -> (0 + undef338), x6^0 -> (0 + undef340), x7^0 -> (0 + undef341)}>
<l0, l9, (undef351 = (0 + x0^0)) /\ (undef359 = (0 + x1^0)) /\ (undef360 = (0 + x2^0)) /\ (undef361 = (0 + x3^0)) /\ (undef362 = (0 + x4^0)) /\ (undef366 = undef366) /\ (undef367 = undef367) /\ (undef352 = undef352) /\ (undef541 = undef541) /\ (undef542 = undef542) /\ (undef527 = undef527) /\ (undef528 = undef528) /\ (undef529 = undef529) /\ (undef530 = undef530) /\ (undef531 = undef531) /\ (undef532 = undef532), par{x0^0 -> (0 + undef541), x1^0 -> (0 + undef542), x2^0 -> (0 + undef527), x3^0 -> (0 + undef528), x4^0 -> (0 + undef529), x5^0 -> (0 + undef530), x6^0 -> (0 + undef531), x7^0 -> (0 + undef532)}>
<l0, l16, true>
<l0, l13, true>
<l0, l18, (undef501 = (0 + x0^0)) /\ (undef509 = (0 + x1^0)) /\ (undef510 = (0 + x2^0)) /\ (undef511 = (0 + x3^0)) /\ (undef512 = (0 + x4^0)) /\ (undef513 = (0 + x5^0)) /\ (undef516 = undef516) /\ (undef517 = undef517), par{x0^0 -> (0 + undef501), x1^0 -> (0 + undef509), x2^0 -> (0 + undef510), x3^0 -> (0 + undef511), x4^0 -> (0 + undef512), x5^0 -> (~(16) + undef513), x6^0 -> (0 + undef516), x7^0 -> (0 + undef517)}>
<l0, l9, (undef541 = undef541) /\ (undef542 = undef542) /\ (undef527 = undef527) /\ (undef528 = undef528) /\ (undef529 = undef529) /\ (undef530 = undef530) /\ (undef531 = undef531) /\ (undef532 = undef532), par{x0^0 -> (0 + undef541), x1^0 -> (0 + undef542), x2^0 -> (0 + undef527), x3^0 -> (0 + undef528), x4^0 -> (0 + undef529), x5^0 -> (0 + undef530), x6^0 -> (0 + undef531), x7^0 -> (0 + undef532)}>
<l0, l18, true>
<l0, l1, (undef601 = (0 + x0^0)) /\ (undef609 = (0 + x1^0)) /\ (undef610 = (0 + x2^0)) /\ (undef611 = (0 + x3^0)) /\ (undef613 = (0 + x5^0)) /\ (undef616 = undef616) /\ (undef617 = undef617) /\ (undef602 = undef602), par{x0^0 -> (0 + undef601), x1^0 -> (0 + undef609), x2^0 -> (0 + undef610), x3^0 -> (0 + undef611), x4^0 -> (0 + undef613), x5^0 -> (0 + undef616), x6^0 -> (0 + undef617), x7^0 -> (0 + undef602)}>
<l0, l20, true>
<l0, l2, true>
<l0, l20, (undef751 = (0 + x0^0)) /\ (undef759 = (0 + x1^0)) /\ (undef760 = (0 + x2^0)) /\ (undef761 = (0 + x3^0)) /\ (undef762 = (0 + x4^0)) /\ (undef766 = undef766), par{x0^0 -> (0 + undef751), x1^0 -> (0 + undef759), x2^0 -> (0 + undef760), x3^0 -> (0 + undef761), x4^0 -> (0 + undef762), x5^0 -> (~(5552) + undef762), x6^0 -> 347, x7^0 -> (0 + undef766)}>
<l0, l4, (undef776 = (0 + x0^0)) /\ (undef784 = (0 + x1^0)) /\ (undef785 = (0 + x2^0)) /\ (undef786 = (0 + x3^0)) /\ (undef788 = (0 + x5^0)) /\ (undef789 = (0 + x6^0)) /\ (undef791 = undef791) /\ (undef792 = undef792) /\ (undef777 = undef777), par{x0^0 -> (0 + undef776), x1^0 -> (0 + undef784), x2^0 -> (0 + undef785), x3^0 -> (0 + undef786), x4^0 -> (0 + undef789), x5^0 -> ((0 + undef788) + undef791), x6^0 -> (0 + undef792), x7^0 -> (0 + undef777)}>
<l0, l6, true>
<l1, l2, (undef1 = (0 + x0^0)) /\ (undef9 = (0 + x1^0)) /\ (undef10 = (0 + x2^0)) /\ (undef11 = (0 + x3^0)) /\ (undef12 = (0 + x4^0)) /\ (undef16 = undef16) /\ (undef17 = undef17) /\ (undef2 = undef2) /\ ((0 + undef12) <= 5551), par{x0^0 -> (0 + undef1), x1^0 -> (0 + undef9), x2^0 -> (0 + undef10), x3^0 -> (0 + undef11), x4^0 -> (0 + undef12), x5^0 -> (0 + undef16), x6^0 -> (0 + undef17), x7^0 -> (0 + undef2)}>
<l1, l20, (undef26 = (0 + x0^0)) /\ (undef34 = (0 + x1^0)) /\ (undef35 = (0 + x2^0)) /\ (undef36 = (0 + x3^0)) /\ (undef37 = (0 + x4^0)) /\ (undef41 = undef41) /\ (undef42 = undef42) /\ (undef27 = undef27) /\ (5552 <= (0 + undef37)) /\ (undef751 = (0 + (0 + undef26))) /\ (undef759 = (0 + (0 + undef34))) /\ (undef760 = (0 + (0 + undef35))) /\ (undef761 = (0 + (0 + undef36))) /\ (undef762 = (0 + (0 + undef37))) /\ (undef766 = undef766), par{x0^0 -> (0 + undef751), x1^0 -> (0 + undef759), x2^0 -> (0 + undef760), x3^0 -> (0 + undef761), x4^0 -> (0 + undef762), x5^0 -> (~(5552) + undef762), x6^0 -> 347, x7^0 -> (0 + undef766)}>
<l2, l9, (undef701 = (0 + x0^0)) /\ (undef709 = (0 + x1^0)) /\ (undef710 = (0 + x2^0)) /\ (undef711 = (0 + x3^0)) /\ (undef712 = (0 + x4^0)) /\ (undef716 = undef716) /\ (undef717 = undef717) /\ (undef702 = undef702) /\ ((0 + undef712) <= 0) /\ (undef541 = undef541) /\ (undef542 = undef542) /\ (undef527 = undef527) /\ (undef528 = undef528) /\ (undef529 = undef529) /\ (undef530 = undef530) /\ (undef531 = undef531) /\ (undef532 = undef532), par{x0^0 -> (0 + undef541), x1^0 -> (0 + undef542), x2^0 -> (0 + undef527), x3^0 -> (0 + undef528), x4^0 -> (0 + undef529), x5^0 -> (0 + undef530), x6^0 -> (0 + undef531), x7^0 -> (0 + undef532)}>
<l2, l18, (undef726 = (0 + x0^0)) /\ (undef734 = (0 + x1^0)) /\ (undef735 = (0 + x2^0)) /\ (undef736 = (0 + x3^0)) /\ (undef737 = (0 + x4^0)) /\ (undef741 = undef741) /\ (undef742 = undef742) /\ (1 <= (0 + undef737)), par{x0^0 -> (0 + undef726), x1^0 -> (0 + undef734), x2^0 -> (0 + undef735), x3^0 -> (0 + undef736), x4^0 -> (0 + undef737), x5^0 -> (0 + undef737), x6^0 -> (0 + undef741), x7^0 -> (0 + undef742)}>
<l4, l4, (undef51 = (0 + x0^0)) /\ (undef59 = (0 + x1^0)) /\ (undef60 = (0 + x2^0)) /\ (undef61 = (0 + x3^0)) /\ (undef62 = (0 + x4^0)) /\ (undef63 = (0 + x5^0)) /\ (undef66 = undef66) /\ (1 <= (0 + undef62)) /\ (undef776 = (0 + (0 + undef51))) /\ (undef784 = (0 + (0 + undef59))) /\ (undef785 = (0 + (0 + undef60))) /\ (undef786 = (0 + (0 + undef61))) /\ (undef788 = (0 + (0 + undef63))) /\ (undef789 = (0 + (~(1) + undef62))) /\ (undef791 = undef791) /\ (undef792 = undef792) /\ (undef777 = undef777), par{x0^0 -> (0 + undef776), x1^0 -> (0 + undef784), x2^0 -> (0 + undef785), x3^0 -> (0 + undef786), x4^0 -> (0 + undef789), x5^0 -> ((0 + undef788) + undef791), x6^0 -> (0 + undef792), x7^0 -> (0 + undef777)}>
<l4, l6, (undef76 = (0 + x0^0)) /\ (undef84 = (0 + x1^0)) /\ (undef85 = (0 + x2^0)) /\ (undef86 = (0 + x3^0)) /\ (undef87 = (0 + x4^0)) /\ (undef88 = (0 + x5^0)) /\ (undef91 = undef91) /\ ((0 + undef87) <= 0), par{x0^0 -> (0 + undef76), x1^0 -> (0 + undef84), x2^0 -> (0 + undef85), x3^0 -> (0 + undef86), x4^0 -> (0 + undef87), x5^0 -> (0 + undef88), x6^0 -> (~(1) + undef87), x7^0 -> (0 + undef91)}>
<l6, l9, (undef813 = (0 + x5^0)) /\ (undef816 = undef816) /\ (undef817 = undef817) /\ (undef802 = undef802) /\ (undef803 = undef803) /\ (undef804 = undef804) /\ (undef805 = undef805) /\ (undef806 = undef806) /\ (undef807 = undef807) /\ ((0 + undef813) <= 65520), par{x0^0 -> (0 + undef816), x1^0 -> (0 + undef817), x2^0 -> (0 + undef802), x3^0 -> (0 + undef803), x4^0 -> (0 + undef804), x5^0 -> (0 + undef805), x6^0 -> (0 + undef806), x7^0 -> (0 + undef807)}>
<l6, l9, (undef838 = (0 + x5^0)) /\ (undef841 = undef841) /\ (undef842 = undef842) /\ (undef827 = undef827) /\ (undef828 = undef828) /\ (undef829 = undef829) /\ (undef830 = undef830) /\ (undef831 = undef831) /\ (undef832 = undef832) /\ (65521 <= (0 + undef838)), par{x0^0 -> (0 + undef841), x1^0 -> (0 + undef842), x2^0 -> (0 + undef827), x3^0 -> (0 + undef828), x4^0 -> (0 + undef829), x5^0 -> (0 + undef830), x6^0 -> (0 + undef831), x7^0 -> (0 + undef832)}>
<l7, l1, (undef101 = (0 + x0^0)) /\ (undef109 = (0 + x1^0)) /\ (undef110 = (0 + x2^0)) /\ (undef111 = (0 + x3^0)) /\ (undef116 = undef116) /\ (undef117 = undef117) /\ (undef102 = undef102) /\ (16 <= (0 + undef109)), par{x0^0 -> (0 + undef101), x1^0 -> (0 + undef109), x2^0 -> (0 + undef110), x3^0 -> (0 + undef111), x4^0 -> (0 + undef109), x5^0 -> (0 + undef116), x6^0 -> (0 + undef117), x7^0 -> (0 + undef102)}>
<l7, l4, (undef126 = (0 + x0^0)) /\ (undef134 = (0 + x1^0)) /\ (undef135 = (0 + x2^0)) /\ (undef136 = (0 + x3^0)) /\ (undef141 = undef141) /\ (undef142 = undef142) /\ ((0 + undef134) <= 15), par{x0^0 -> (0 + undef126), x1^0 -> (0 + undef134), x2^0 -> (0 + undef135), x3^0 -> (0 + undef136), x4^0 -> (0 + undef134), x5^0 -> (0 + undef136), x6^0 -> (0 + undef141), x7^0 -> (0 + undef142)}>
<l10, l7, (undef176 = (0 + x0^0)) /\ (undef184 = (0 + x1^0)) /\ (undef185 = (0 + x2^0)) /\ (undef186 = (0 + x3^0)) /\ (undef191 = undef191) /\ (undef192 = undef192) /\ (undef177 = undef177) /\ (undef178 = undef178), par{x0^0 -> (0 + undef176), x1^0 -> (0 + undef184), x2^0 -> (0 + undef185), x3^0 -> (0 + undef186), x4^0 -> (0 + undef191), x5^0 -> (0 + undef192), x6^0 -> (0 + undef177), x7^0 -> (0 + undef178)}>
<l10, l9, (undef201 = (0 + x0^0)) /\ (undef209 = (0 + x1^0)) /\ (undef210 = (0 + x2^0)) /\ (undef211 = (0 + x3^0)) /\ (undef216 = undef216) /\ (undef217 = undef217) /\ (undef202 = undef202) /\ (undef203 = undef203) /\ (undef166 = undef166) /\ (undef167 = undef167) /\ (undef152 = undef152) /\ (undef153 = undef153) /\ (undef154 = undef154) /\ (undef155 = undef155) /\ (undef156 = undef156) /\ (undef157 = undef157), par{x0^0 -> (0 + undef166), x1^0 -> (0 + undef167), x2^0 -> (0 + undef152), x3^0 -> (0 + undef153), x4^0 -> (0 + undef154), x5^0 -> (0 + undef155), x6^0 -> (0 + undef156), x7^0 -> (0 + undef157)}>
<l11, l9, (undef235 = (0 + x2^0)) /\ (undef236 = (0 + x3^0)) /\ (undef241 = undef241) /\ (undef242 = undef242) /\ (undef227 = undef227) /\ (undef228 = undef228) /\ (undef229 = undef229) /\ (undef230 = undef230) /\ (undef231 = undef231) /\ (undef232 = undef232) /\ (undef233 = undef233) /\ (((0 + undef233) + undef236) <= 65520) /\ ((((0 + undef233) + undef235) + undef236) <= 65520), par{x0^0 -> (0 + undef241), x1^0 -> (0 + undef242), x2^0 -> (0 + undef227), x3^0 -> (0 + undef228), x4^0 -> (0 + undef229), x5^0 -> (0 + undef230), x6^0 -> (0 + undef231), x7^0 -> (0 + undef232)}>
<l11, l9, (undef260 = (0 + x2^0)) /\ (undef261 = (0 + x3^0)) /\ (undef266 = undef266) /\ (undef267 = undef267) /\ (undef252 = undef252) /\ (undef253 = undef253) /\ (undef254 = undef254) /\ (undef255 = undef255) /\ (undef256 = undef256) /\ (undef257 = undef257) /\ (undef258 = undef258) /\ (((0 + undef258) + undef261) <= 65520) /\ (65521 <= (((0 + undef258) + undef260) + undef261)), par{x0^0 -> (0 + undef266), x1^0 -> (0 + undef267), x2^0 -> (0 + undef252), x3^0 -> (0 + undef253), x4^0 -> (0 + undef254), x5^0 -> (0 + undef255), x6^0 -> (0 + undef256), x7^0 -> (0 + undef257)}>
<l11, l9, (undef285 = (0 + x2^0)) /\ (undef286 = (0 + x3^0)) /\ (undef291 = undef291) /\ (undef292 = undef292) /\ (undef277 = undef277) /\ (undef278 = undef278) /\ (undef279 = undef279) /\ (undef280 = undef280) /\ (undef281 = undef281) /\ (undef282 = undef282) /\ (undef283 = undef283) /\ (65521 <= ((0 + undef283) + undef286)) /\ ((((~(65521) + undef283) + undef285) + undef286) <= 65520), par{x0^0 -> (0 + undef291), x1^0 -> (0 + undef292), x2^0 -> (0 + undef277), x3^0 -> (0 + undef278), x4^0 -> (0 + undef279), x5^0 -> (0 + undef280), x6^0 -> (0 + undef281), x7^0 -> (0 + undef282)}>
<l11, l9, (undef310 = (0 + x2^0)) /\ (undef311 = (0 + x3^0)) /\ (undef316 = undef316) /\ (undef317 = undef317) /\ (undef302 = undef302) /\ (undef303 = undef303) /\ (undef304 = undef304) /\ (undef305 = undef305) /\ (undef306 = undef306) /\ (undef307 = undef307) /\ (undef308 = undef308) /\ (65521 <= ((0 + undef308) + undef311)) /\ (65521 <= (((~(65521) + undef308) + undef310) + undef311)), par{x0^0 -> (0 + undef316), x1^0 -> (0 + undef317), x2^0 -> (0 + undef302), x3^0 -> (0 + undef303), x4^0 -> (0 + undef304), x5^0 -> (0 + undef305), x6^0 -> (0 + undef306), x7^0 -> (0 + undef307)}>
<l13, l13, (undef451 = (0 + x0^0)) /\ (undef459 = (0 + x1^0)) /\ (undef460 = (0 + x2^0)) /\ (undef461 = (0 + x3^0)) /\ (undef462 = (0 + x4^0)) /\ (undef463 = (0 + x5^0)) /\ (undef464 = (0 + x6^0)) /\ (1 <= (0 + undef464)) /\ (undef326 = (0 + (0 + undef451))) /\ (undef334 = (0 + (0 + undef459))) /\ (undef335 = (0 + (0 + undef460))) /\ (undef336 = (0 + (0 + undef461))) /\ (undef337 = (0 + (0 + undef462))) /\ (undef338 = (0 + (0 + undef463))) /\ (undef340 = (0 + (~(1) + undef464))) /\ (undef341 = undef341), par{x0^0 -> (0 + undef326), x1^0 -> (0 + undef334), x2^0 -> (0 + undef335), x3^0 -> (0 + undef336), x4^0 -> (0 + undef337), x5^0 -> (0 + undef338), x6^0 -> (0 + undef340), x7^0 -> (0 + undef341)}>
<l13, l9, (undef476 = (0 + x0^0)) /\ (undef484 = (0 + x1^0)) /\ (undef485 = (0 + x2^0)) /\ (undef486 = (0 + x3^0)) /\ (undef487 = (0 + x4^0)) /\ (undef488 = (0 + x5^0)) /\ (undef489 = (0 + x6^0)) /\ ((0 + undef489) <= 0) /\ (undef351 = (0 + (0 + undef476))) /\ (undef359 = (0 + (0 + undef484))) /\ (undef360 = (0 + (0 + undef485))) /\ (undef361 = (0 + (0 + undef486))) /\ (undef362 = (0 + (0 + undef487))) /\ (undef366 = undef366) /\ (undef367 = undef367) /\ (undef352 = undef352) /\ (undef541 = undef541) /\ (undef542 = undef542) /\ (undef527 = undef527) /\ (undef528 = undef528) /\ (undef529 = undef529) /\ (undef530 = undef530) /\ (undef531 = undef531) /\ (undef532 = undef532), par{x0^0 -> (0 + undef541), x1^0 -> (0 + undef542), x2^0 -> (0 + undef527), x3^0 -> (0 + undef528), x4^0 -> (0 + undef529), x5^0 -> (0 + undef530), x6^0 -> (0 + undef531), x7^0 -> (0 + undef532)}>
<l16, l10, (undef376 = (0 + x0^0)) /\ (undef384 = (0 + x1^0)) /\ (undef391 = undef391) /\ (undef392 = undef392) /\ (undef377 = undef377) /\ (undef378 = undef378) /\ (undef379 = undef379) /\ (undef380 = undef380) /\ (2 <= (0 + undef384)), par{x0^0 -> (0 + undef376), x1^0 -> (0 + undef384), x2^0 -> (0 + undef391), x3^0 -> (0 + undef392), x4^0 -> (0 + undef377), x5^0 -> (0 + undef378), x6^0 -> (0 + undef379), x7^0 -> (0 + undef380)}>
<l16, l10, (undef401 = (0 + x0^0)) /\ (undef409 = (0 + x1^0)) /\ (undef416 = undef416) /\ (undef417 = undef417) /\ (undef402 = undef402) /\ (undef403 = undef403) /\ (undef404 = undef404) /\ (undef405 = undef405) /\ ((1 + undef409) <= 1), par{x0^0 -> (0 + undef401), x1^0 -> (0 + undef409), x2^0 -> (0 + undef416), x3^0 -> (0 + undef417), x4^0 -> (0 + undef402), x5^0 -> (0 + undef403), x6^0 -> (0 + undef404), x7^0 -> (0 + undef405)}>
<l16, l11, (undef426 = (0 + x0^0)) /\ (undef434 = (0 + x1^0)) /\ (undef441 = undef441) /\ (undef442 = undef442) /\ (undef427 = undef427) /\ (undef428 = undef428) /\ (undef429 = undef429) /\ (undef430 = undef430) /\ ((0 + undef434) <= 1) /\ (1 <= (0 + undef434)), par{x0^0 -> (0 + undef426), x1^0 -> (0 + undef434), x2^0 -> (0 + undef441), x3^0 -> (0 + undef442), x4^0 -> (0 + undef427), x5^0 -> (0 + undef428), x6^0 -> (0 + undef429), x7^0 -> (0 + undef430)}>
<l18, l13, (undef551 = (0 + x0^0)) /\ (undef559 = (0 + x1^0)) /\ (undef560 = (0 + x2^0)) /\ (undef561 = (0 + x3^0)) /\ (undef562 = (0 + x4^0)) /\ (undef563 = (0 + x5^0)) /\ (undef566 = undef566) /\ ((0 + undef563) <= 15), par{x0^0 -> (0 + undef551), x1^0 -> (0 + undef559), x2^0 -> (0 + undef560), x3^0 -> (0 + undef561), x4^0 -> (0 + undef562), x5^0 -> (0 + undef563), x6^0 -> (0 + undef563), x7^0 -> (0 + undef566)}>
<l18, l18, (undef576 = (0 + x0^0)) /\ (undef584 = (0 + x1^0)) /\ (undef585 = (0 + x2^0)) /\ (undef586 = (0 + x3^0)) /\ (undef587 = (0 + x4^0)) /\ (undef588 = (0 + x5^0)) /\ (undef591 = undef591) /\ (undef592 = undef592) /\ (16 <= (0 + undef588)) /\ (undef501 = (0 + (0 + undef576))) /\ (undef509 = (0 + (0 + undef584))) /\ (undef510 = (0 + (0 + undef585))) /\ (undef511 = (0 + (0 + undef586))) /\ (undef512 = (0 + (0 + undef587))) /\ (undef513 = (0 + (0 + undef588))) /\ (undef516 = undef516) /\ (undef517 = undef517), par{x0^0 -> (0 + undef501), x1^0 -> (0 + undef509), x2^0 -> (0 + undef510), x3^0 -> (0 + undef511), x4^0 -> (0 + undef512), x5^0 -> (~(16) + undef513), x6^0 -> (0 + undef516), x7^0 -> (0 + undef517)}>
<l20, l1, (undef626 = (0 + x0^0)) /\ (undef634 = (0 + x1^0)) /\ (undef635 = (0 + x2^0)) /\ (undef636 = (0 + x3^0)) /\ (undef637 = (0 + x4^0)) /\ (undef638 = (0 + x5^0)) /\ (undef639 = (0 + x6^0)) /\ (undef641 = undef641) /\ ((~(1) + undef639) <= 0) /\ (undef601 = (0 + (0 + undef626))) /\ (undef609 = (0 + (0 + undef634))) /\ (undef610 = (0 + (0 + undef635))) /\ (undef611 = (0 + (0 + undef636))) /\ (undef613 = (0 + (0 + undef638))) /\ (undef616 = undef616) /\ (undef617 = undef617) /\ (undef602 = undef602), par{x0^0 -> (0 + undef601), x1^0 -> (0 + undef609), x2^0 -> (0 + undef610), x3^0 -> (0 + undef611), x4^0 -> (0 + undef613), x5^0 -> (0 + undef616), x6^0 -> (0 + undef617), x7^0 -> (0 + undef602)}>
<l20, l20, (undef651 = (0 + x0^0)) /\ (undef659 = (0 + x1^0)) /\ (undef660 = (0 + x2^0)) /\ (undef661 = (0 + x3^0)) /\ (undef662 = (0 + x4^0)) /\ (undef663 = (0 + x5^0)) /\ (undef664 = (0 + x6^0)) /\ (undef666 = undef666) /\ (1 <= (~(1) + undef664)), par{x0^0 -> (0 + undef651), x1^0 -> (0 + undef659), x2^0 -> (0 + undef660), x3^0 -> (0 + undef661), x4^0 -> (0 + undef662), x5^0 -> (0 + undef663), x6^0 -> (~(1) + undef664), x7^0 -> (0 + undef666)}>

Fresh variables:
undef1, undef2, undef9, undef10, undef11, undef12, undef16, undef17, undef26, undef27, undef34, undef35, undef36, undef37, undef41, undef42, undef51, undef59, undef60, undef61, undef62, undef63, undef66, undef76, undef84, undef85, undef86, undef87, undef88, undef91, undef101, undef102, undef109, undef110, undef111, undef116, undef117, undef126, undef134, undef135, undef136, undef141, undef142, undef152, undef153, undef154, undef155, undef156, undef157, undef166, undef167, undef176, undef177, undef178, undef184, undef185, undef186, undef191, undef192, undef201, undef202, undef203, undef209, undef210, undef211, undef216, undef217, undef227, undef228, undef229, undef230, undef231, undef232, undef233, undef235, undef236, undef241, undef242, undef252, undef253, undef254, undef255, undef256, undef257, undef258, undef260, undef261, undef266, undef267, undef277, undef278, undef279, undef280, undef281, undef282, undef283, undef285, undef286, undef291, undef292, undef302, undef303, undef304, undef305, undef306, undef307, undef308, undef310, undef311, undef316, undef317, undef326, undef334, undef335, undef336, undef337, undef338, undef340, undef341, undef351, undef352, undef359, undef360, undef361, undef362, undef366, undef367, undef376, undef377, undef378, undef379, undef380, undef384, undef391, undef392, undef401, undef402, undef403, undef404, undef405, undef409, undef416, undef417, undef426, undef427, undef428, undef429, undef430, undef434, undef441, undef442, undef451, undef459, undef460, undef461, undef462, undef463, undef464, undef476, undef484, undef485, undef486, undef487, undef488, undef489, undef501, undef509, undef510, undef511, undef512, undef513, undef516, undef517, undef527, undef528, undef529, undef530, undef531, undef532, undef541, undef542, undef551, undef559, undef560, undef561, undef562, undef563, undef566, undef576, undef584, undef585, undef586, undef587, undef588, undef591, undef592, undef601, undef602, undef609, undef610, undef611, undef613, undef616, undef617, undef626, undef634, undef635, undef636, undef637, undef638, undef639, undef641, undef651, undef659, undef660, undef661, undef662, undef663, undef664, undef666, undef701, undef702, undef709, undef710, undef711, undef712, undef716, undef717, undef726, undef734, undef735, undef736, undef737, undef741, undef742, undef751, undef759, undef760, undef761, undef762, undef766, undef776, undef777, undef784, undef785, undef786, undef788, undef789, undef791, undef792, undef802, undef803, undef804, undef805, undef806, undef807, undef813, undef816, undef817, undef827, undef828, undef829, undef830, undef831, undef832, undef838, undef841, undef842, undef851, undef852, undef853, undef854, undef855, undef859, undef866, undef867, 

Undef variables:
undef1, undef2, undef9, undef10, undef11, undef12, undef16, undef17, undef26, undef27, undef34, undef35, undef36, undef37, undef41, undef42, undef51, undef59, undef60, undef61, undef62, undef63, undef66, undef76, undef84, undef85, undef86, undef87, undef88, undef91, undef101, undef102, undef109, undef110, undef111, undef116, undef117, undef126, undef134, undef135, undef136, undef141, undef142, undef152, undef153, undef154, undef155, undef156, undef157, undef166, undef167, undef176, undef177, undef178, undef184, undef185, undef186, undef191, undef192, undef201, undef202, undef203, undef209, undef210, undef211, undef216, undef217, undef227, undef228, undef229, undef230, undef231, undef232, undef233, undef235, undef236, undef241, undef242, undef252, undef253, undef254, undef255, undef256, undef257, undef258, undef260, undef261, undef266, undef267, undef277, undef278, undef279, undef280, undef281, undef282, undef283, undef285, undef286, undef291, undef292, undef302, undef303, undef304, undef305, undef306, undef307, undef308, undef310, undef311, undef316, undef317, undef326, undef334, undef335, undef336, undef337, undef338, undef340, undef341, undef351, undef352, undef359, undef360, undef361, undef362, undef366, undef367, undef376, undef377, undef378, undef379, undef380, undef384, undef391, undef392, undef401, undef402, undef403, undef404, undef405, undef409, undef416, undef417, undef426, undef427, undef428, undef429, undef430, undef434, undef441, undef442, undef451, undef459, undef460, undef461, undef462, undef463, undef464, undef476, undef484, undef485, undef486, undef487, undef488, undef489, undef501, undef509, undef510, undef511, undef512, undef513, undef516, undef517, undef527, undef528, undef529, undef530, undef531, undef532, undef541, undef542, undef551, undef559, undef560, undef561, undef562, undef563, undef566, undef576, undef584, undef585, undef586, undef587, undef588, undef591, undef592, undef601, undef602, undef609, undef610, undef611, undef613, undef616, undef617, undef626, undef634, undef635, undef636, undef637, undef638, undef639, undef641, undef651, undef659, undef660, undef661, undef662, undef663, undef664, undef666, undef701, undef702, undef709, undef710, undef711, undef712, undef716, undef717, undef726, undef734, undef735, undef736, undef737, undef741, undef742, undef751, undef759, undef760, undef761, undef762, undef766, undef776, undef777, undef784, undef785, undef786, undef788, undef789, undef791, undef792, undef802, undef803, undef804, undef805, undef806, undef807, undef813, undef816, undef817, undef827, undef828, undef829, undef830, undef831, undef832, undef838, undef841, undef842, undef851, undef852, undef853, undef854, undef855, undef859, undef866, undef867, 

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:
Variables:

Graph 5:
Transitions:
<l4, l4, 1 <= undef62 /\ x0^0 = undef51 /\ x1^0 = undef59 /\ x2^0 = undef60 /\ x3^0 = undef61 /\ x4^0 = undef62 /\ x5^0 = undef63 /\ undef51 = undef776 /\ undef59 = undef784 /\ undef60 = undef785 /\ undef61 = undef786 /\ undef63 = undef788 /\ undef62 = 1 + undef789, {x0^0 -> undef776, x1^0 -> undef784, x2^0 -> undef785, x3^0 -> undef786, x4^0 -> undef789, x5^0 -> undef788 + undef791, x6^0 -> undef792, x7^0 -> undef777, rest remain the same}>
Variables:
x0^0, x1^0, x2^0, x3^0, x4^0, x5^0, x6^0, x7^0

Graph 6:
Transitions:
Variables:

Graph 7:
Transitions:
<l1, l20, 5552 <= undef37 /\ x0^0 = undef26 /\ x1^0 = undef34 /\ x2^0 = undef35 /\ x3^0 = undef36 /\ x4^0 = undef37 /\ undef26 = undef751 /\ undef34 = undef759 /\ undef35 = undef760 /\ undef36 = undef761 /\ undef37 = undef762, {x0^0 -> undef751, x1^0 -> undef759, x2^0 -> undef760, x3^0 -> undef761, x4^0 -> undef762, x5^0 -> -5552 + undef762, x6^0 -> 347, x7^0 -> undef766, rest remain the same}>
<l20, l1, undef639 <= 1 /\ x0^0 = undef626 /\ x1^0 = undef634 /\ x2^0 = undef635 /\ x3^0 = undef636 /\ x4^0 = undef637 /\ x5^0 = undef638 /\ x6^0 = undef639 /\ undef601 = undef626 /\ undef609 = undef634 /\ undef610 = undef635 /\ undef611 = undef636 /\ undef613 = undef638, {x0^0 -> undef601, x1^0 -> undef609, x2^0 -> undef610, x3^0 -> undef611, x4^0 -> undef613, x5^0 -> undef616, x6^0 -> undef617, x7^0 -> undef602, rest remain the same}>
<l20, l20, 2 <= undef664 /\ x0^0 = undef651 /\ x1^0 = undef659 /\ x2^0 = undef660 /\ x3^0 = undef661 /\ x4^0 = undef662 /\ x5^0 = undef663 /\ x6^0 = undef664, {x0^0 -> undef651, x1^0 -> undef659, x2^0 -> undef660, x3^0 -> undef661, x4^0 -> undef662, x5^0 -> undef663, x6^0 -> -1 + undef664, x7^0 -> undef666, rest remain the same}>
Variables:
x0^0, x1^0, x2^0, x3^0, x4^0, x5^0, x7^0, x6^0

Graph 8:
Transitions:
Variables:

Graph 9:
Transitions:
<l18, l18, 16 <= undef588 /\ x0^0 = undef576 /\ x1^0 = undef584 /\ x2^0 = undef585 /\ x3^0 = undef586 /\ x4^0 = undef587 /\ x5^0 = undef588 /\ undef501 = undef576 /\ undef509 = undef584 /\ undef510 = undef585 /\ undef511 = undef586 /\ undef512 = undef587 /\ undef513 = undef588, {x0^0 -> undef501, x1^0 -> undef509, x2^0 -> undef510, x3^0 -> undef511, x4^0 -> undef512, x5^0 -> -16 + undef513, x6^0 -> undef516, x7^0 -> undef517, rest remain the same}>
Variables:
x0^0, x1^0, x2^0, x3^0, x4^0, x5^0, x6^0, x7^0

Graph 10:
Transitions:
<l13, l13, 1 <= undef464 /\ x0^0 = undef451 /\ x1^0 = undef459 /\ x2^0 = undef460 /\ x3^0 = undef461 /\ x4^0 = undef462 /\ x5^0 = undef463 /\ x6^0 = undef464 /\ undef326 = undef451 /\ undef334 = undef459 /\ undef335 = undef460 /\ undef336 = undef461 /\ undef337 = undef462 /\ undef338 = undef463 /\ 1 + undef340 = undef464, {x0^0 -> undef326, x1^0 -> undef334, x2^0 -> undef335, x3^0 -> undef336, x4^0 -> undef337, x5^0 -> undef338, x6^0 -> undef340, x7^0 -> undef341, rest remain the same}>
Variables:
x0^0, x1^0, x2^0, x3^0, x4^0, x5^0, x6^0, x7^0

Graph 11:
Transitions:
Variables:

Precedence: 
Graph 0

Graph 1
<l0, l16, x0^0 = undef851 /\ x1^0 = undef859, {x0^0 -> undef851, x1^0 -> undef859, x2^0 -> undef866, x3^0 -> undef867, x4^0 -> undef852, x5^0 -> undef853, x6^0 -> undef854, x7^0 -> undef855, rest remain the same}>
<l0, l16, true, {all remain the same}>

Graph 2
<l0, l11, true, {all remain the same}>
<l16, l11, x0^0 = undef426 /\ x1^0 = undef434 /\ undef434 = 1, {x0^0 -> undef426, x1^0 -> undef434, x2^0 -> undef441, x3^0 -> undef442, x4^0 -> undef427, x5^0 -> undef428, x6^0 -> undef429, x7^0 -> undef430, rest remain the same}>

Graph 3
<l0, l10, true, {all remain the same}>
<l16, l10, 2 <= undef384 /\ x0^0 = undef376 /\ x1^0 = undef384, {x0^0 -> undef376, x1^0 -> undef384, x2^0 -> undef391, x3^0 -> undef392, x4^0 -> undef377, x5^0 -> undef378, x6^0 -> undef379, x7^0 -> undef380, rest remain the same}>
<l16, l10, undef409 <= 0 /\ x0^0 = undef401 /\ x1^0 = undef409, {x0^0 -> undef401, x1^0 -> undef409, x2^0 -> undef416, x3^0 -> undef417, x4^0 -> undef402, x5^0 -> undef403, x6^0 -> undef404, x7^0 -> undef405, rest remain the same}>

Graph 4
<l0, l7, true, {all remain the same}>
<l10, l7, x0^0 = undef176 /\ x1^0 = undef184 /\ x2^0 = undef185 /\ x3^0 = undef186, {x0^0 -> undef176, x1^0 -> undef184, x2^0 -> undef185, x3^0 -> undef186, x4^0 -> undef191, x5^0 -> undef192, x6^0 -> undef177, x7^0 -> undef178, rest remain the same}>

Graph 5
<l0, l4, true, {all remain the same}>
<l0, l4, x0^0 = undef776 /\ x1^0 = undef784 /\ x2^0 = undef785 /\ x3^0 = undef786 /\ x5^0 = undef788 /\ x6^0 = undef789, {x0^0 -> undef776, x1^0 -> undef784, x2^0 -> undef785, x3^0 -> undef786, x4^0 -> undef789, x5^0 -> undef788 + undef791, x6^0 -> undef792, x7^0 -> undef777, rest remain the same}>
<l7, l4, undef134 <= 15 /\ x0^0 = undef126 /\ x1^0 = undef134 /\ x2^0 = undef135 /\ x3^0 = undef136, {x0^0 -> undef126, x1^0 -> undef134, x2^0 -> undef135, x3^0 -> undef136, x4^0 -> undef134, x5^0 -> undef136, x6^0 -> undef141, x7^0 -> undef142, rest remain the same}>

Graph 6
<l0, l6, true, {all remain the same}>
<l4, l6, undef87 <= 0 /\ x0^0 = undef76 /\ x1^0 = undef84 /\ x2^0 = undef85 /\ x3^0 = undef86 /\ x4^0 = undef87 /\ x5^0 = undef88, {x0^0 -> undef76, x1^0 -> undef84, x2^0 -> undef85, x3^0 -> undef86, x4^0 -> undef87, x5^0 -> undef88, x6^0 -> -1 + undef87, x7^0 -> undef91, rest remain the same}>

Graph 7
<l0, l1, true, {all remain the same}>
<l0, l1, x0^0 = undef601 /\ x1^0 = undef609 /\ x2^0 = undef610 /\ x3^0 = undef611 /\ x5^0 = undef613, {x0^0 -> undef601, x1^0 -> undef609, x2^0 -> undef610, x3^0 -> undef611, x4^0 -> undef613, x5^0 -> undef616, x6^0 -> undef617, x7^0 -> undef602, rest remain the same}>
<l0, l20, true, {all remain the same}>
<l0, l20, x0^0 = undef751 /\ x1^0 = undef759 /\ x2^0 = undef760 /\ x3^0 = undef761 /\ x4^0 = undef762, {x0^0 -> undef751, x1^0 -> undef759, x2^0 -> undef760, x3^0 -> undef761, x4^0 -> undef762, x5^0 -> -5552 + undef762, x6^0 -> 347, x7^0 -> undef766, rest remain the same}>
<l7, l1, 16 <= undef109 /\ x0^0 = undef101 /\ x1^0 = undef109 /\ x2^0 = undef110 /\ x3^0 = undef111, {x0^0 -> undef101, x1^0 -> undef109, x2^0 -> undef110, x3^0 -> undef111, x4^0 -> undef109, x5^0 -> undef116, x6^0 -> undef117, x7^0 -> undef102, rest remain the same}>

Graph 8
<l0, l2, true, {all remain the same}>
<l1, l2, undef12 <= 5551 /\ x0^0 = undef1 /\ x1^0 = undef9 /\ x2^0 = undef10 /\ x3^0 = undef11 /\ x4^0 = undef12, {x0^0 -> undef1, x1^0 -> undef9, x2^0 -> undef10, x3^0 -> undef11, x4^0 -> undef12, x5^0 -> undef16, x6^0 -> undef17, x7^0 -> undef2, rest remain the same}>

Graph 9
<l0, l18, x0^0 = undef501 /\ x1^0 = undef509 /\ x2^0 = undef510 /\ x3^0 = undef511 /\ x4^0 = undef512 /\ x5^0 = undef513, {x0^0 -> undef501, x1^0 -> undef509, x2^0 -> undef510, x3^0 -> undef511, x4^0 -> undef512, x5^0 -> -16 + undef513, x6^0 -> undef516, x7^0 -> undef517, rest remain the same}>
<l0, l18, true, {all remain the same}>
<l2, l18, 1 <= undef737 /\ x0^0 = undef726 /\ x1^0 = undef734 /\ x2^0 = undef735 /\ x3^0 = undef736 /\ x4^0 = undef737, {x0^0 -> undef726, x1^0 -> undef734, x2^0 -> undef735, x3^0 -> undef736, x4^0 -> undef737, x5^0 -> undef737, x6^0 -> undef741, x7^0 -> undef742, rest remain the same}>

Graph 10
<l0, l13, x0^0 = undef326 /\ x1^0 = undef334 /\ x2^0 = undef335 /\ x3^0 = undef336 /\ x4^0 = undef337 /\ x5^0 = undef338 /\ x7^0 = undef340, {x0^0 -> undef326, x1^0 -> undef334, x2^0 -> undef335, x3^0 -> undef336, x4^0 -> undef337, x5^0 -> undef338, x6^0 -> undef340, x7^0 -> undef341, rest remain the same}>
<l0, l13, true, {all remain the same}>
<l18, l13, undef563 <= 15 /\ x0^0 = undef551 /\ x1^0 = undef559 /\ x2^0 = undef560 /\ x3^0 = undef561 /\ x4^0 = undef562 /\ x5^0 = undef563, {x0^0 -> undef551, x1^0 -> undef559, x2^0 -> undef560, x3^0 -> undef561, x4^0 -> undef562, x5^0 -> undef563, x6^0 -> undef563, x7^0 -> undef566, rest remain the same}>

Graph 11
<l0, l9, true, {x0^0 -> undef166, x1^0 -> undef167, x2^0 -> undef152, x3^0 -> undef153, x4^0 -> undef154, x5^0 -> undef155, x6^0 -> undef156, x7^0 -> undef157, rest remain the same}>
<l0, l9, true, {all remain the same}>
<l0, l9, x0^0 = undef351 /\ x1^0 = undef359 /\ x2^0 = undef360 /\ x3^0 = undef361 /\ x4^0 = undef362, {x0^0 -> undef541, x1^0 -> undef542, x2^0 -> undef527, x3^0 -> undef528, x4^0 -> undef529, x5^0 -> undef530, x6^0 -> undef531, x7^0 -> undef532, rest remain the same}>
<l0, l9, true, {x0^0 -> undef541, x1^0 -> undef542, x2^0 -> undef527, x3^0 -> undef528, x4^0 -> undef529, x5^0 -> undef530, x6^0 -> undef531, x7^0 -> undef532, rest remain the same}>
<l2, l9, undef712 <= 0 /\ x0^0 = undef701 /\ x1^0 = undef709 /\ x2^0 = undef710 /\ x3^0 = undef711 /\ x4^0 = undef712, {x0^0 -> undef541, x1^0 -> undef542, x2^0 -> undef527, x3^0 -> undef528, x4^0 -> undef529, x5^0 -> undef530, x6^0 -> undef531, x7^0 -> undef532, rest remain the same}>
<l6, l9, undef813 <= 65520 /\ x5^0 = undef813, {x0^0 -> undef816, x1^0 -> undef817, x2^0 -> undef802, x3^0 -> undef803, x4^0 -> undef804, x5^0 -> undef805, x6^0 -> undef806, x7^0 -> undef807, rest remain the same}>
<l6, l9, 65521 <= undef838 /\ x5^0 = undef838, {x0^0 -> undef841, x1^0 -> undef842, x2^0 -> undef827, x3^0 -> undef828, x4^0 -> undef829, x5^0 -> undef830, x6^0 -> undef831, x7^0 -> undef832, rest remain the same}>
<l10, l9, x0^0 = undef201 /\ x1^0 = undef209 /\ x2^0 = undef210 /\ x3^0 = undef211, {x0^0 -> undef166, x1^0 -> undef167, x2^0 -> undef152, x3^0 -> undef153, x4^0 -> undef154, x5^0 -> undef155, x6^0 -> undef156, x7^0 -> undef157, rest remain the same}>
<l11, l9, undef233 + undef235 + undef236 <= 65520 /\ undef233 + undef236 <= 65520 /\ x2^0 = undef235 /\ x3^0 = undef236, {x0^0 -> undef241, x1^0 -> undef242, x2^0 -> undef227, x3^0 -> undef228, x4^0 -> undef229, x5^0 -> undef230, x6^0 -> undef231, x7^0 -> undef232, rest remain the same}>
<l11, l9, 65521 <= undef258 + undef260 + undef261 /\ undef258 + undef261 <= 65520 /\ x2^0 = undef260 /\ x3^0 = undef261, {x0^0 -> undef266, x1^0 -> undef267, x2^0 -> undef252, x3^0 -> undef253, x4^0 -> undef254, x5^0 -> undef255, x6^0 -> undef256, x7^0 -> undef257, rest remain the same}>
<l11, l9, 65521 <= undef283 + undef286 /\ undef283 + undef285 + undef286 <= 131041 /\ x2^0 = undef285 /\ x3^0 = undef286, {x0^0 -> undef291, x1^0 -> undef292, x2^0 -> undef277, x3^0 -> undef278, x4^0 -> undef279, x5^0 -> undef280, x6^0 -> undef281, x7^0 -> undef282, rest remain the same}>
<l11, l9, 65521 <= undef308 + undef311 /\ 131042 <= undef308 + undef310 + undef311 /\ x2^0 = undef310 /\ x3^0 = undef311, {x0^0 -> undef316, x1^0 -> undef317, x2^0 -> undef302, x3^0 -> undef303, x4^0 -> undef304, x5^0 -> undef305, x6^0 -> undef306, x7^0 -> undef307, rest remain the same}>
<l13, l9, undef489 <= 0 /\ x0^0 = undef476 /\ x1^0 = undef484 /\ x2^0 = undef485 /\ x3^0 = undef486 /\ x4^0 = undef487 /\ x5^0 = undef488 /\ x6^0 = undef489 /\ undef351 = undef476 /\ undef359 = undef484 /\ undef360 = undef485 /\ undef361 = undef486 /\ undef362 = undef487, {x0^0 -> undef541, x1^0 -> undef542, x2^0 -> undef527, x3^0 -> undef528, x4^0 -> undef529, x5^0 -> undef530, x6^0 -> undef531, x7^0 -> undef532, rest remain the same}>

Map Locations to Subgraph:
( 0 , 0 )
( 1 , 7 )
( 2 , 8 )
( 4 , 5 )
( 6 , 6 )
( 7 , 4 )
( 9 , 11 )
( 10 , 3 )
( 11 , 2 )
( 13 , 10 )
( 16 , 1 )
( 18 , 9 )
( 20 , 7 )

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

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

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

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

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

Proving termination of subgraph 5
Checking unfeasibility...
Time used: 0.003564

Checking conditional termination of SCC {l4}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001429s
Ranking function: -1 + x4^0
New Graphs: 
Proving termination of subgraph 6
Analyzing SCC {l6}...
No cycles found.

Proving termination of subgraph 7
Checking unfeasibility...
Time used: 0.0138

Checking conditional termination of SCC {l1, l20}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.003501s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.015482s
Trying to remove transition: <l20, l20, 2 <= undef664 /\ x0^0 = undef651 /\ x1^0 = undef659 /\ x2^0 = undef660 /\ x3^0 = undef661 /\ x4^0 = undef662 /\ x5^0 = undef663 /\ x6^0 = undef664, {x0^0 -> undef651, x1^0 -> undef659, x2^0 -> undef660, x3^0 -> undef661, x4^0 -> undef662, x5^0 -> undef663, x6^0 -> -1 + undef664, x7^0 -> undef666, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.010530s
Time used: 4.00812
Trying to remove transition: <l20, l1, undef639 <= 1 /\ x0^0 = undef626 /\ x1^0 = undef634 /\ x2^0 = undef635 /\ x3^0 = undef636 /\ x4^0 = undef637 /\ x5^0 = undef638 /\ x6^0 = undef639 /\ undef601 = undef626 /\ undef609 = undef634 /\ undef610 = undef635 /\ undef611 = undef636 /\ undef613 = undef638, {x0^0 -> undef601, x1^0 -> undef609, x2^0 -> undef610, x3^0 -> undef611, x4^0 -> undef613, x5^0 -> undef616, x6^0 -> undef617, x7^0 -> undef602, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.105248s
Time used: 0.023233
Trying to remove transition: <l1, l20, 5552 <= undef37 /\ x0^0 = undef26 /\ x1^0 = undef34 /\ x2^0 = undef35 /\ x3^0 = undef36 /\ x4^0 = undef37 /\ undef26 = undef751 /\ undef34 = undef759 /\ undef35 = undef760 /\ undef36 = undef761 /\ undef37 = undef762, {x0^0 -> undef751, x1^0 -> undef759, x2^0 -> undef760, x3^0 -> undef761, x4^0 -> undef762, x5^0 -> -5552 + undef762, x6^0 -> 347, x7^0 -> undef766, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.002942s
Time used: 1.00294

LOG: SAT solveNonLinear - Elapsed time: 1.102952s
Cost: 5; Total time: 1.09845
Failed at location 1: x4^0 <= 1
Failed at location 1: x4^0 <= 1
Failed at location 1: x4^0 <= 1
Failed at location 20: 1 <= 0
Failed at location 20: 1 <= 0
Before Improving: 
Quasi-invariant at l1: x4^0 <= 1
Quasi-invariant at l20: 1 <= 0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.015211s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008694s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008039s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.007855s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008221s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008328s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008438s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.007913s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008142s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008005s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008166s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008329s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008648s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008407s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008303s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008127s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008333s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008187s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008499s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008540s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008682s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008354s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008355s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008261s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008401s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008432s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008781s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008678s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008489s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008302s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008497s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008399s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008608s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008740s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008869s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008481s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008523s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008427s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008588s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008556s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008897s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008800s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008837s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008529s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008658s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008584s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008733s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008840s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009017s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008807s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008730s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008649s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008776s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008705s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008984s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008908s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008978s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008656s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008782s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008718s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008838s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008873s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009041s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008899s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008862s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008761s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008963s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008822s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009134s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009083s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009118s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008849s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008961s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008866s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009048s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009097s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009379s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009141s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009170s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008995s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009034s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008923s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009126s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009209s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009154s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008931s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009023s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.008967s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009063s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009119s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009265s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009111s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009106s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009079s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009210s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009004s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009202s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009242s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009301s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009084s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009192s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009074s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009181s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009177s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009332s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009203s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009140s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009054s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009236s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009166s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009318s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009361s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009327s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009143s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009190s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009158s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009261s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009219s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009394s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009294s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009273s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009152s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009255s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009208s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009320s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009374s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009359s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009163s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009239s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009214s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009300s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009318s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009504s
Quasi-invariant improved
Remaining time after improvement: -0.001616
Termination implied by a set of quasi-invariant(s):
Quasi-invariant at l1: x4^0 <= 147
Quasi-invariant at l20: 1 <= 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: 
<l1, l20, 5552 <= undef37 /\ x0^0 = undef26 /\ x1^0 = undef34 /\ x2^0 = undef35 /\ x3^0 = undef36 /\ x4^0 = undef37 /\ undef26 = undef751 /\ undef34 = undef759 /\ undef35 = undef760 /\ undef36 = undef761 /\ undef37 = undef762, {x0^0 -> undef751, x1^0 -> undef759, x2^0 -> undef760, x3^0 -> undef761, x4^0 -> undef762, x5^0 -> -5552 + undef762, x6^0 -> 347, x7^0 -> undef766, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l20, l1, undef639 <= 1 /\ x0^0 = undef626 /\ x1^0 = undef634 /\ x2^0 = undef635 /\ x3^0 = undef636 /\ x4^0 = undef637 /\ x5^0 = undef638 /\ x6^0 = undef639 /\ undef601 = undef626 /\ undef609 = undef634 /\ undef610 = undef635 /\ undef611 = undef636 /\ undef613 = undef638, {x0^0 -> undef601, x1^0 -> undef609, x2^0 -> undef610, x3^0 -> undef611, x4^0 -> undef613, x5^0 -> undef616, x6^0 -> undef617, x7^0 -> undef602, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l20, l20, 2 <= undef664 /\ x0^0 = undef651 /\ x1^0 = undef659 /\ x2^0 = undef660 /\ x3^0 = undef661 /\ x4^0 = undef662 /\ x5^0 = undef663 /\ x6^0 = undef664, {x0^0 -> undef651, x1^0 -> undef659, x2^0 -> undef660, x3^0 -> undef661, x4^0 -> undef662, x5^0 -> undef663, x6^0 -> -1 + undef664, x7^0 -> undef666, 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: 
<l1, l20, 5552 <= undef37 /\ x0^0 = undef26 /\ x1^0 = undef34 /\ x2^0 = undef35 /\ x3^0 = undef36 /\ x4^0 = undef37 /\ undef26 = undef751 /\ undef34 = undef759 /\ undef35 = undef760 /\ undef36 = undef761 /\ undef37 = undef762, {x0^0 -> undef751, x1^0 -> undef759, x2^0 -> undef760, x3^0 -> undef761, x4^0 -> undef762, x5^0 -> -5552 + undef762, x6^0 -> 347, x7^0 -> undef766, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l20, l1, undef639 <= 1 /\ x0^0 = undef626 /\ x1^0 = undef634 /\ x2^0 = undef635 /\ x3^0 = undef636 /\ x4^0 = undef637 /\ x5^0 = undef638 /\ x6^0 = undef639 /\ undef601 = undef626 /\ undef609 = undef634 /\ undef610 = undef635 /\ undef611 = undef636 /\ undef613 = undef638, {x0^0 -> undef601, x1^0 -> undef609, x2^0 -> undef610, x3^0 -> undef611, x4^0 -> undef613, x5^0 -> undef616, x6^0 -> undef617, x7^0 -> undef602, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l20, l20, 2 <= undef664 /\ x0^0 = undef651 /\ x1^0 = undef659 /\ x2^0 = undef660 /\ x3^0 = undef661 /\ x4^0 = undef662 /\ x5^0 = undef663 /\ x6^0 = undef664, {x0^0 -> undef651, x1^0 -> undef659, x2^0 -> undef660, x3^0 -> undef661, x4^0 -> undef662, x5^0 -> undef663, x6^0 -> -1 + undef664, x7^0 -> undef666, rest remain the same}>
New Graphs: 
Calling Safety with literal x4^0 <= 147 and entry <l0, l1, true, {all remain the same}>

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

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.001497s
Calling Safety with literal x4^0 <= 147 and entry <l0, l1, x0^0 = undef601 /\ x1^0 = undef609 /\ x2^0 = undef610 /\ x3^0 = undef611 /\ x5^0 = undef613, {x0^0 -> undef601, x1^0 -> undef609, x2^0 -> undef610, x3^0 -> undef611, x4^0 -> undef613, x5^0 -> undef616, x6^0 -> undef617, x7^0 -> undef602, rest remain the same}>

LOG: CALL check - Post:x4^0 <= 147 - Process 2
* Exit transition: <l0, l1, x0^0 = undef601 /\ x1^0 = undef609 /\ x2^0 = undef610 /\ x3^0 = undef611 /\ x5^0 = undef613, {x0^0 -> undef601, x1^0 -> undef609, x2^0 -> undef610, x3^0 -> undef611, x4^0 -> undef613, x5^0 -> undef616, x6^0 -> undef617, x7^0 -> undef602, rest remain the same}>
* Postcondition  : x4^0 <= 147

LOG: CALL solveLinear

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

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

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

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.000850s
Calling Safety with literal 1 <= 0 and entry <l0, l20, x0^0 = undef751 /\ x1^0 = undef759 /\ x2^0 = undef760 /\ x3^0 = undef761 /\ x4^0 = undef762, {x0^0 -> undef751, x1^0 -> undef759, x2^0 -> undef760, x3^0 -> undef761, x4^0 -> undef762, x5^0 -> -5552 + undef762, x6^0 -> 347, x7^0 -> undef766, rest remain the same}>

LOG: CALL check - Post:1 <= 0 - Process 4
* Exit transition: <l0, l20, x0^0 = undef751 /\ x1^0 = undef759 /\ x2^0 = undef760 /\ x3^0 = undef761 /\ x4^0 = undef762, {x0^0 -> undef751, x1^0 -> undef759, x2^0 -> undef760, x3^0 -> undef761, x4^0 -> undef762, x5^0 -> -5552 + undef762, x6^0 -> 347, x7^0 -> undef766, rest remain the same}>
* Postcondition  : 1 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.001092s
Calling Safety with literal x4^0 <= 147 and entry <l7, l1, 16 <= undef109 /\ x0^0 = undef101 /\ x1^0 = undef109 /\ x2^0 = undef110 /\ x3^0 = undef111, {x0^0 -> undef101, x1^0 -> undef109, x2^0 -> undef110, x3^0 -> undef111, x4^0 -> undef109, x5^0 -> undef116, x6^0 -> undef117, x7^0 -> undef102, rest remain the same}>

LOG: CALL check - Post:x4^0 <= 147 - Process 5
* Exit transition: <l7, l1, 16 <= undef109 /\ x0^0 = undef101 /\ x1^0 = undef109 /\ x2^0 = undef110 /\ x3^0 = undef111, {x0^0 -> undef101, x1^0 -> undef109, x2^0 -> undef110, x3^0 -> undef111, x4^0 -> undef109, x5^0 -> undef116, x6^0 -> undef117, x7^0 -> undef102, rest remain the same}>
* Postcondition  : x4^0 <= 147
Postcodition moved up: undef109 <= 147

LOG: Try proving POST
Postcondition: undef109 <= 147

LOG: CALL check - Post:undef109 <= 147 - Process 6
* Exit transition: <l0, l7, 16 <= undef109 /\ x0^0 = undef101 /\ x1^0 = undef109 /\ x2^0 = undef110 /\ x3^0 = undef111, {all remain the same}>
* Postcondition  : undef109 <= 147

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.001087s
Postcondition: undef109 <= 147

LOG: CALL check - Post:undef109 <= 147 - Process 7
* Exit transition: <l10, l7, 16 <= undef109 /\ x0^0 = undef176 /\ x1^0 = undef184 /\ x2^0 = undef185 /\ x3^0 = undef186 /\ undef101 = undef176 /\ undef109 = undef184 /\ undef110 = undef185 /\ undef111 = undef186, {x0^0 -> undef176, x1^0 -> undef184, x2^0 -> undef185, x3^0 -> undef186, x4^0 -> undef191, x5^0 -> undef192, x6^0 -> undef177, x7^0 -> undef178, rest remain the same}>
* Postcondition  : undef109 <= 147
Postcodition moved up: undef109 <= 147

LOG: Try proving POST
Postcondition: undef109 <= 147

LOG: CALL check - Post:undef109 <= 147 - Process 8
* Exit transition: <l0, l10, x0^0 = undef176 /\ x1^0 = undef184 /\ x2^0 = undef185 /\ x3^0 = undef186, {all remain the same}>
* Postcondition  : undef109 <= 147

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.001064s
Postcondition: undef109 <= 147

LOG: CALL check - Post:undef109 <= 147 - Process 9
* Exit transition: <l16, l10, 2 <= undef384 /\ x0^0 = undef376 /\ x1^0 = undef384 /\ undef176 = undef376 /\ undef184 = undef384 /\ undef185 = undef391 /\ undef186 = undef392, {x0^0 -> undef376, x1^0 -> undef384, x2^0 -> undef391, x3^0 -> undef392, x4^0 -> undef377, x5^0 -> undef378, x6^0 -> undef379, x7^0 -> undef380, rest remain the same}>
* Postcondition  : undef109 <= 147
Postcodition moved up: undef109 <= 147

LOG: Try proving POST
Postcondition: undef109 <= 147

LOG: CALL check - Post:undef109 <= 147 - Process 10
* Exit transition: <l0, l16, 2 <= undef384 /\ x0^0 = undef851 /\ x1^0 = undef859 /\ undef376 = undef851 /\ undef384 = undef859, {x0^0 -> undef851, x1^0 -> undef859, x2^0 -> undef866, x3^0 -> undef867, x4^0 -> undef852, x5^0 -> undef853, x6^0 -> undef854, x7^0 -> undef855, rest remain the same}>
* Postcondition  : undef109 <= 147

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.001090s
Postcondition: undef109 <= 147

LOG: CALL check - Post:undef109 <= 147 - Process 11
* Exit transition: <l0, l16, 2 <= undef384 /\ x0^0 = undef376 /\ x1^0 = undef384, {all remain the same}>
* Postcondition  : undef109 <= 147

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.000998s

LOG: NarrowEntry size 1

LOG: NarrowEntry size 1
ENTRIES:
<l0, l16, 2 <= undef384 /\ 148 <= undef109 /\ x0^0 = undef851 /\ x1^0 = undef859 /\ undef376 = undef851 /\ undef384 = undef859, {x0^0 -> undef851, x1^0 -> undef859, x2^0 -> undef866, x3^0 -> undef867, x4^0 -> undef852, x5^0 -> undef853, x6^0 -> undef854, x7^0 -> undef855, rest remain the same}>
<l0, l16, 2 <= undef384 /\ 148 <= undef109 /\ x0^0 = undef376 /\ x1^0 = undef384, {all remain the same}>
END ENTRIES:
GRAPH:
END GRAPH:
EXIT: <l16, l10, 2 <= undef384 /\ x0^0 = undef376 /\ x1^0 = undef384 /\ undef176 = undef376 /\ undef184 = undef384 /\ undef185 = undef391 /\ undef186 = undef392, {x0^0 -> undef376, x1^0 -> undef384, x2^0 -> undef391, x3^0 -> undef392, x4^0 -> undef377, x5^0 -> undef378, x6^0 -> undef379, x7^0 -> undef380, rest remain the same}>
POST: undef109 <= 147


LOG: Try proving POST
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.004853s
Time used: 4.00471

LOG: Postcondition is not implied - no solution
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 4.019374s
Postcondition: undef109 <= 147

LOG: CALL check - Post:undef109 <= 147 - Process 12
* Exit transition: <l16, l10, undef409 <= 0 /\ x0^0 = undef401 /\ x1^0 = undef409 /\ undef176 = undef401 /\ undef184 = undef409 /\ undef185 = undef416 /\ undef186 = undef417, {x0^0 -> undef401, x1^0 -> undef409, x2^0 -> undef416, x3^0 -> undef417, x4^0 -> undef402, x5^0 -> undef403, x6^0 -> undef404, x7^0 -> undef405, rest remain the same}>
* Postcondition  : undef109 <= 147
Postcodition moved up: undef109 <= 147

LOG: Try proving POST
Postcondition: undef109 <= 147

LOG: CALL check - Post:undef109 <= 147 - Process 13
* Exit transition: <l0, l16, undef409 <= 0 /\ x0^0 = undef851 /\ x1^0 = undef859 /\ undef401 = undef851 /\ undef409 = undef859, {x0^0 -> undef851, x1^0 -> undef859, x2^0 -> undef866, x3^0 -> undef867, x4^0 -> undef852, x5^0 -> undef853, x6^0 -> undef854, x7^0 -> undef855, rest remain the same}>
* Postcondition  : undef109 <= 147

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.001122s
Postcondition: undef109 <= 147

LOG: CALL check - Post:undef109 <= 147 - Process 14
* Exit transition: <l0, l16, undef409 <= 0 /\ x0^0 = undef401 /\ x1^0 = undef409, {all remain the same}>
* Postcondition  : undef109 <= 147

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.001011s

LOG: NarrowEntry size 1

LOG: NarrowEntry size 1
ENTRIES:
<l0, l16, undef409 <= 0 /\ 148 <= undef109 /\ x0^0 = undef851 /\ x1^0 = undef859 /\ undef401 = undef851 /\ undef409 = undef859, {x0^0 -> undef851, x1^0 -> undef859, x2^0 -> undef866, x3^0 -> undef867, x4^0 -> undef852, x5^0 -> undef853, x6^0 -> undef854, x7^0 -> undef855, rest remain the same}>
<l0, l16, undef409 <= 0 /\ 148 <= undef109 /\ x0^0 = undef401 /\ x1^0 = undef409, {all remain the same}>
END ENTRIES:
GRAPH:
END GRAPH:
EXIT: <l16, l10, undef409 <= 0 /\ x0^0 = undef401 /\ x1^0 = undef409 /\ undef176 = undef401 /\ undef184 = undef409 /\ undef185 = undef416 /\ undef186 = undef417, {x0^0 -> undef401, x1^0 -> undef409, x2^0 -> undef416, x3^0 -> undef417, x4^0 -> undef402, x5^0 -> undef403, x6^0 -> undef404, x7^0 -> undef405, rest remain the same}>
POST: undef109 <= 147


LOG: Try proving POST
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.003061s
Time used: 4.00292

LOG: Postcondition is not implied - no solution
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 4.021019s

LOG: NarrowEntry size 1

LOG: NarrowEntry size 1

LOG: NarrowEntry size 1
ENTRIES:
<l0, l10, 148 <= undef109 /\ x0^0 = undef176 /\ x1^0 = undef184 /\ x2^0 = undef185 /\ x3^0 = undef186, {all remain the same}>
<l16, l10, 2 <= undef384 /\ 148 <= undef109 /\ x0^0 = undef376 /\ x1^0 = undef384 /\ undef176 = undef376 /\ undef184 = undef384 /\ undef185 = undef391 /\ undef186 = undef392, {x0^0 -> undef376, x1^0 -> undef384, x2^0 -> undef391, x3^0 -> undef392, x4^0 -> undef377, x5^0 -> undef378, x6^0 -> undef379, x7^0 -> undef380, rest remain the same}>
<l16, l10, undef409 <= 0 /\ 148 <= undef109 /\ x0^0 = undef401 /\ x1^0 = undef409 /\ undef176 = undef401 /\ undef184 = undef409 /\ undef185 = undef416 /\ undef186 = undef417, {x0^0 -> undef401, x1^0 -> undef409, x2^0 -> undef416, x3^0 -> undef417, x4^0 -> undef402, x5^0 -> undef403, x6^0 -> undef404, x7^0 -> undef405, rest remain the same}>
END ENTRIES:
GRAPH:
END GRAPH:
EXIT: <l10, l7, 16 <= undef109 /\ x0^0 = undef176 /\ x1^0 = undef184 /\ x2^0 = undef185 /\ x3^0 = undef186 /\ undef101 = undef176 /\ undef109 = undef184 /\ undef110 = undef185 /\ undef111 = undef186, {x0^0 -> undef176, x1^0 -> undef184, x2^0 -> undef185, x3^0 -> undef186, x4^0 -> undef191, x5^0 -> undef192, x6^0 -> undef177, x7^0 -> undef178, rest remain the same}>
POST: undef109 <= 147


LOG: Try proving POST
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.006398s
Time used: 0.006257
Improving Solution with cost 2 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.007563s
Time used: 0.007561

LOG: SAT solveNonLinear - Elapsed time: 0.013961s
Cost: 2; Total time: 0.013818
Failed at location 10: x1^0 <= 1
Failed at location 10: x1^0 <= 1
Before Improving: 
Quasi-invariant at l10: x1^0 <= 1
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.004036s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002767s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002408s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002375s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002358s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002319s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002320s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002296s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002302s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002295s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002308s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002319s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002309s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002299s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002316s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002299s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002283s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002297s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002301s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002307s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002298s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002208s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002240s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002256s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002317s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002309s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002302s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002272s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002320s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002321s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002320s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002273s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002278s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002293s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002298s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002299s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002299s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002292s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002301s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002271s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002298s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002286s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002280s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002289s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002289s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002302s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002237s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002275s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002294s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002314s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002286s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002255s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002276s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002314s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002306s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002296s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002290s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002287s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002328s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002291s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002299s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002305s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002291s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002292s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002299s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002286s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002286s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002301s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002317s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002295s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002241s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002256s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002295s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002293s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002304s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002268s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002296s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002310s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002327s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002315s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002292s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002313s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002299s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002311s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002313s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002308s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002306s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002304s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002317s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002302s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002336s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002343s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002310s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002256s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002287s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002316s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002310s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002296s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002288s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002327s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002335s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002317s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002304s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002312s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002336s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002325s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002332s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002326s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002303s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002334s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002326s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002302s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002318s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002315s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002302s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002262s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002292s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002331s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002325s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002303s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002328s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002323s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002348s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002298s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002331s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002330s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002319s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002316s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002318s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002312s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002329s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002329s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002326s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002328s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002321s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002297s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002292s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002312s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002342s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002299s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002321s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002324s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002341s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002327s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002322s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001222s
Remaining time after improvement: 0.689242
Postcondition implied by a set of quasi-invariant(s):
Quasi-invariant at l10: x1^0 <= 147
Postcondition: x1^0 <= 147

LOG: CALL check - Post:x1^0 <= 147 - Process 15
* Exit transition: <l0, l10, 148 <= undef109 /\ x0^0 = undef176 /\ x1^0 = undef184 /\ x2^0 = undef185 /\ x3^0 = undef186, {all remain the same}>
* Postcondition  : x1^0 <= 147

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.001382s
Postcondition: x1^0 <= 147

LOG: CALL check - Post:x1^0 <= 147 - Process 16
* Exit transition: <l16, l10, 2 <= undef384 /\ 148 <= undef109 /\ x0^0 = undef376 /\ x1^0 = undef384 /\ undef176 = undef376 /\ undef184 = undef384 /\ undef185 = undef391 /\ undef186 = undef392, {x0^0 -> undef376, x1^0 -> undef384, x2^0 -> undef391, x3^0 -> undef392, x4^0 -> undef377, x5^0 -> undef378, x6^0 -> undef379, x7^0 -> undef380, rest remain the same}>
* Postcondition  : x1^0 <= 147
Postcodition moved up: undef384 <= 147

LOG: Try proving POST
Postcondition: undef384 <= 147

LOG: CALL check - Post:undef384 <= 147 - Process 17
* Exit transition: <l0, l16, 2 <= undef384 /\ 148 <= undef109 /\ x0^0 = undef851 /\ x1^0 = undef859 /\ undef376 = undef851 /\ undef384 = undef859, {x0^0 -> undef851, x1^0 -> undef859, x2^0 -> undef866, x3^0 -> undef867, x4^0 -> undef852, x5^0 -> undef853, x6^0 -> undef854, x7^0 -> undef855, rest remain the same}>
* Postcondition  : undef384 <= 147

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.001222s
Postcondition: undef384 <= 147

LOG: CALL check - Post:undef384 <= 147 - Process 18
* Exit transition: <l0, l16, 2 <= undef384 /\ 148 <= undef109 /\ x0^0 = undef376 /\ x1^0 = undef384, {all remain the same}>
* Postcondition  : undef384 <= 147

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.001122s

LOG: NarrowEntry size 1

LOG: NarrowEntry size 1
ENTRIES:
<l0, l16, 148 <= undef109 /\ 148 <= undef384 /\ x0^0 = undef851 /\ x1^0 = undef859 /\ undef376 = undef851 /\ undef384 = undef859, {x0^0 -> undef851, x1^0 -> undef859, x2^0 -> undef866, x3^0 -> undef867, x4^0 -> undef852, x5^0 -> undef853, x6^0 -> undef854, x7^0 -> undef855, rest remain the same}>
<l0, l16, 148 <= undef109 /\ 148 <= undef384 /\ x0^0 = undef376 /\ x1^0 = undef384, {all remain the same}>
END ENTRIES:
GRAPH:
END GRAPH:
EXIT: <l16, l10, 2 <= undef384 /\ 148 <= undef109 /\ x0^0 = undef376 /\ x1^0 = undef384 /\ undef176 = undef376 /\ undef184 = undef384 /\ undef185 = undef391 /\ undef186 = undef392, {x0^0 -> undef376, x1^0 -> undef384, x2^0 -> undef391, x3^0 -> undef392, x4^0 -> undef377, x5^0 -> undef378, x6^0 -> undef379, x7^0 -> undef380, rest remain the same}>
POST: x1^0 <= 147


LOG: Try proving POST
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.007607s
Time used: 4.00618

LOG: Postcondition is not implied - no solution
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 4.071802s

LOG: NarrowEntry size 1

LOG: NarrowEntry size 1
INVARIANTS: 
10: 
Quasi-INVARIANTS to narrow Graph: 
10: x1^0 <= 147 , 
ENTRIES:
<l0, l10, 148 <= x1^0 /\ 148 <= undef109 /\ x0^0 = undef176 /\ x1^0 = undef184 /\ x2^0 = undef185 /\ x3^0 = undef186, {all remain the same}>
<l16, l10, 148 <= undef109 /\ 148 <= undef384 /\ x0^0 = undef376 /\ x1^0 = undef384 /\ undef176 = undef376 /\ undef184 = undef384 /\ undef185 = undef391 /\ undef186 = undef392, {x0^0 -> undef376, x1^0 -> undef384, x2^0 -> undef391, x3^0 -> undef392, x4^0 -> undef377, x5^0 -> undef378, x6^0 -> undef379, x7^0 -> undef380, rest remain the same}>
END ENTRIES:
GRAPH:
END GRAPH:
EXIT: <l10, l7, 16 <= undef109 /\ x0^0 = undef176 /\ x1^0 = undef184 /\ x2^0 = undef185 /\ x3^0 = undef186 /\ undef101 = undef176 /\ undef109 = undef184 /\ undef110 = undef185 /\ undef111 = undef186, {x0^0 -> undef176, x1^0 -> undef184, x2^0 -> undef185, x3^0 -> undef186, x4^0 -> undef191, x5^0 -> undef192, x6^0 -> undef177, x7^0 -> undef178, rest remain the same}>
POST: undef109 <= 147


LOG: Try proving POST
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.003692s
Time used: 1.00001

LOG: Postcondition is not implied - no solution
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 17.565906s

LOG: NarrowEntry size 1

LOG: NarrowEntry size 1
ENTRIES:
<l0, l7, 148 <= undef109 /\ x0^0 = undef101 /\ x1^0 = undef109 /\ x2^0 = undef110 /\ x3^0 = undef111, {all remain the same}>
<l10, l7, 148 <= undef109 /\ x0^0 = undef176 /\ x1^0 = undef184 /\ x2^0 = undef185 /\ x3^0 = undef186 /\ undef101 = undef176 /\ undef109 = undef184 /\ undef110 = undef185 /\ undef111 = undef186, {x0^0 -> undef176, x1^0 -> undef184, x2^0 -> undef185, x3^0 -> undef186, x4^0 -> undef191, x5^0 -> undef192, x6^0 -> undef177, x7^0 -> undef178, rest remain the same}>
END ENTRIES:
GRAPH:
END GRAPH:
EXIT: <l7, l1, 16 <= undef109 /\ x0^0 = undef101 /\ x1^0 = undef109 /\ x2^0 = undef110 /\ x3^0 = undef111, {x0^0 -> undef101, x1^0 -> undef109, x2^0 -> undef110, x3^0 -> undef111, x4^0 -> undef109, x5^0 -> undef116, x6^0 -> undef117, x7^0 -> undef102, rest remain the same}>
POST: x4^0 <= 147


LOG: Try proving POST
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.003632s
Time used: 1.00004

LOG: Postcondition is not implied - no solution
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 22.636230s
INVARIANTS: 
1: 
20: 
Quasi-INVARIANTS to narrow Graph: 
1: x4^0 <= 147 , 
20: 1 <= 0 , 
Narrowing transition: 
<l1, l20, 5552 <= undef37 /\ x0^0 = undef26 /\ x1^0 = undef34 /\ x2^0 = undef35 /\ x3^0 = undef36 /\ x4^0 = undef37 /\ undef26 = undef751 /\ undef34 = undef759 /\ undef35 = undef760 /\ undef36 = undef761 /\ undef37 = undef762, {x0^0 -> undef751, x1^0 -> undef759, x2^0 -> undef760, x3^0 -> undef761, x4^0 -> undef762, x5^0 -> -5552 + undef762, x6^0 -> 347, x7^0 -> undef766, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l20, l1, undef639 <= 1 /\ x0^0 = undef626 /\ x1^0 = undef634 /\ x2^0 = undef635 /\ x3^0 = undef636 /\ x4^0 = undef637 /\ x5^0 = undef638 /\ x6^0 = undef639 /\ undef601 = undef626 /\ undef609 = undef634 /\ undef610 = undef635 /\ undef611 = undef636 /\ undef613 = undef638, {x0^0 -> undef601, x1^0 -> undef609, x2^0 -> undef610, x3^0 -> undef611, x4^0 -> undef613, x5^0 -> undef616, x6^0 -> undef617, x7^0 -> undef602, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l20, l20, 2 <= undef664 /\ x0^0 = undef651 /\ x1^0 = undef659 /\ x2^0 = undef660 /\ x3^0 = undef661 /\ x4^0 = undef662 /\ x5^0 = undef663 /\ x6^0 = undef664, {x0^0 -> undef651, x1^0 -> undef659, x2^0 -> undef660, x3^0 -> undef661, x4^0 -> undef662, x5^0 -> undef663, x6^0 -> -1 + undef664, x7^0 -> undef666, rest remain the same}>

LOG: Narrow transition size 1
invGraph after Narrowing: 
Transitions:
<l1, l20, 5552 <= undef37 /\ 148 <= x4^0 /\ x0^0 = undef26 /\ x1^0 = undef34 /\ x2^0 = undef35 /\ x3^0 = undef36 /\ x4^0 = undef37 /\ undef26 = undef751 /\ undef34 = undef759 /\ undef35 = undef760 /\ undef36 = undef761 /\ undef37 = undef762, {x0^0 -> undef751, x1^0 -> undef759, x2^0 -> undef760, x3^0 -> undef761, x4^0 -> undef762, x5^0 -> -5552 + undef762, x6^0 -> 347, x7^0 -> undef766, rest remain the same}>
<l20, l1, 0 <= 0 /\ undef639 <= 1 /\ x0^0 = undef626 /\ x1^0 = undef634 /\ x2^0 = undef635 /\ x3^0 = undef636 /\ x4^0 = undef637 /\ x5^0 = undef638 /\ x6^0 = undef639 /\ undef601 = undef626 /\ undef609 = undef634 /\ undef610 = undef635 /\ undef611 = undef636 /\ undef613 = undef638, {x0^0 -> undef601, x1^0 -> undef609, x2^0 -> undef610, x3^0 -> undef611, x4^0 -> undef613, x5^0 -> undef616, x6^0 -> undef617, x7^0 -> undef602, rest remain the same}>
<l20, l20, 0 <= 0 /\ 2 <= undef664 /\ x0^0 = undef651 /\ x1^0 = undef659 /\ x2^0 = undef660 /\ x3^0 = undef661 /\ x4^0 = undef662 /\ x5^0 = undef663 /\ x6^0 = undef664, {x0^0 -> undef651, x1^0 -> undef659, x2^0 -> undef660, x3^0 -> undef661, x4^0 -> undef662, x5^0 -> undef663, x6^0 -> -1 + undef664, x7^0 -> undef666, rest remain the same}>
Variables:
x0^0, x1^0, x2^0, x3^0, x4^0, x5^0, x7^0, x6^0
Checking conditional termination of SCC {l1, l20}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002968s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.014858s
Trying to remove transition: <l20, l20, 0 <= 0 /\ 2 <= undef664 /\ x0^0 = undef651 /\ x1^0 = undef659 /\ x2^0 = undef660 /\ x3^0 = undef661 /\ x4^0 = undef662 /\ x5^0 = undef663 /\ x6^0 = undef664, {x0^0 -> undef651, x1^0 -> undef659, x2^0 -> undef660, x3^0 -> undef661, x4^0 -> undef662, x5^0 -> undef663, x6^0 -> -1 + undef664, x7^0 -> undef666, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.180909s
Time used: 4.17725
Trying to remove transition: <l20, l1, 0 <= 0 /\ undef639 <= 1 /\ x0^0 = undef626 /\ x1^0 = undef634 /\ x2^0 = undef635 /\ x3^0 = undef636 /\ x4^0 = undef637 /\ x5^0 = undef638 /\ x6^0 = undef639 /\ undef601 = undef626 /\ undef609 = undef634 /\ undef610 = undef635 /\ undef611 = undef636 /\ undef613 = undef638, {x0^0 -> undef601, x1^0 -> undef609, x2^0 -> undef610, x3^0 -> undef611, x4^0 -> undef613, x5^0 -> undef616, x6^0 -> undef617, x7^0 -> undef602, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.100343s
Time used: 0.023044
Trying to remove transition: <l1, l20, 5552 <= undef37 /\ 148 <= x4^0 /\ x0^0 = undef26 /\ x1^0 = undef34 /\ x2^0 = undef35 /\ x3^0 = undef36 /\ x4^0 = undef37 /\ undef26 = undef751 /\ undef34 = undef759 /\ undef35 = undef760 /\ undef36 = undef761 /\ undef37 = undef762, {x0^0 -> undef751, x1^0 -> undef759, x2^0 -> undef760, x3^0 -> undef761, x4^0 -> undef762, x5^0 -> -5552 + undef762, x6^0 -> 347, x7^0 -> undef766, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.004675s
Time used: 1.00467

LOG: SAT solveNonLinear - Elapsed time: 1.124592s
Cost: 5; Total time: 1.11979
Failed at location 1: x4^0 <= 0
Failed at location 1: x4^0 <= 0
Failed at location 1: x4^0 <= 0
Failed at location 20: 1 + x5^0 <= 0
Failed at location 20: 1 + x5^0 <= 0
Before Improving: 
Quasi-invariant at l1: x4^0 <= 0
Quasi-invariant at l20: 1 + x5^0 <= 0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.015381s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011181s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010840s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011151s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010665s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010295s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009967s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010125s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010253s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010227s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009947s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010394s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010954s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011353s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011102s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010714s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010204s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010338s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010411s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010576s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010229s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010383s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010925s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011391s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011318s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010874s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010346s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010407s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010473s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010563s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010286s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010408s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010837s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011443s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011407s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011128s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010580s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010559s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010559s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010750s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010552s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010561s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010774s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011330s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011432s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011368s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010893s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010402s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010618s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010834s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010676s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010639s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010746s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011304s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011495s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011423s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011056s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010728s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010669s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010943s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010810s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010747s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010726s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011333s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011490s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011524s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011117s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010910s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010765s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011005s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010920s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010878s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010814s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011352s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011696s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011653s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011279s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011039s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010866s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011052s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011038s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011034s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010908s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011357s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011555s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011706s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011435s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011196s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010927s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011157s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011128s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011072s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.010994s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011340s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011543s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011689s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011501s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011326s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011026s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011165s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011185s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011164s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011068s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011357s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011643s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011750s
Quasi-invariant improved
Remaining time after improvement: -0.001683
Termination implied by a set of quasi-invariant(s):
Quasi-invariant at l1: x4^0 <= 253
Quasi-invariant at l20: 1 + x5^0 <= 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: 
<l1, l20, 5552 <= undef37 /\ 148 <= x4^0 /\ x0^0 = undef26 /\ x1^0 = undef34 /\ x2^0 = undef35 /\ x3^0 = undef36 /\ x4^0 = undef37 /\ undef26 = undef751 /\ undef34 = undef759 /\ undef35 = undef760 /\ undef36 = undef761 /\ undef37 = undef762, {x0^0 -> undef751, x1^0 -> undef759, x2^0 -> undef760, x3^0 -> undef761, x4^0 -> undef762, x5^0 -> -5552 + undef762, x6^0 -> 347, x7^0 -> undef766, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l20, l1, 0 <= 0 /\ 1 + x5^0 <= 0 /\ undef639 <= 1 /\ x0^0 = undef626 /\ x1^0 = undef634 /\ x2^0 = undef635 /\ x3^0 = undef636 /\ x4^0 = undef637 /\ x5^0 = undef638 /\ x6^0 = undef639 /\ undef601 = undef626 /\ undef609 = undef634 /\ undef610 = undef635 /\ undef611 = undef636 /\ undef613 = undef638, {x0^0 -> undef601, x1^0 -> undef609, x2^0 -> undef610, x3^0 -> undef611, x4^0 -> undef613, x5^0 -> undef616, x6^0 -> undef617, x7^0 -> undef602, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l20, l20, 0 <= 0 /\ 1 + x5^0 <= 0 /\ 2 <= undef664 /\ x0^0 = undef651 /\ x1^0 = undef659 /\ x2^0 = undef660 /\ x3^0 = undef661 /\ x4^0 = undef662 /\ x5^0 = undef663 /\ x6^0 = undef664, {x0^0 -> undef651, x1^0 -> undef659, x2^0 -> undef660, x3^0 -> undef661, x4^0 -> undef662, x5^0 -> undef663, x6^0 -> -1 + undef664, x7^0 -> undef666, 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: 
<l1, l20, 5552 <= undef37 /\ 148 <= x4^0 /\ x0^0 = undef26 /\ x1^0 = undef34 /\ x2^0 = undef35 /\ x3^0 = undef36 /\ x4^0 = undef37 /\ undef26 = undef751 /\ undef34 = undef759 /\ undef35 = undef760 /\ undef36 = undef761 /\ undef37 = undef762, {x0^0 -> undef751, x1^0 -> undef759, x2^0 -> undef760, x3^0 -> undef761, x4^0 -> undef762, x5^0 -> -5552 + undef762, x6^0 -> 347, x7^0 -> undef766, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l20, l1, 0 <= 0 /\ 1 + x5^0 <= 0 /\ undef639 <= 1 /\ x0^0 = undef626 /\ x1^0 = undef634 /\ x2^0 = undef635 /\ x3^0 = undef636 /\ x4^0 = undef637 /\ x5^0 = undef638 /\ x6^0 = undef639 /\ undef601 = undef626 /\ undef609 = undef634 /\ undef610 = undef635 /\ undef611 = undef636 /\ undef613 = undef638, {x0^0 -> undef601, x1^0 -> undef609, x2^0 -> undef610, x3^0 -> undef611, x4^0 -> undef613, x5^0 -> undef616, x6^0 -> undef617, x7^0 -> undef602, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l20, l20, 0 <= 0 /\ 1 + x5^0 <= 0 /\ 2 <= undef664 /\ x0^0 = undef651 /\ x1^0 = undef659 /\ x2^0 = undef660 /\ x3^0 = undef661 /\ x4^0 = undef662 /\ x5^0 = undef663 /\ x6^0 = undef664, {x0^0 -> undef651, x1^0 -> undef659, x2^0 -> undef660, x3^0 -> undef661, x4^0 -> undef662, x5^0 -> undef663, x6^0 -> -1 + undef664, x7^0 -> undef666, rest remain the same}>
New Graphs: 
Transitions:
<l20, l20, 0 <= 0 /\ 1 + x5^0 <= 0 /\ 2 <= undef664 /\ x0^0 = undef651 /\ x1^0 = undef659 /\ x2^0 = undef660 /\ x3^0 = undef661 /\ x4^0 = undef662 /\ x5^0 = undef663 /\ x6^0 = undef664, {x0^0 -> undef651, x1^0 -> undef659, x2^0 -> undef660, x3^0 -> undef661, x4^0 -> undef662, x5^0 -> undef663, x6^0 -> -1 + undef664, x7^0 -> undef666, rest remain the same}>
Variables:
x0^0, x1^0, x2^0, x3^0, x4^0, x5^0, x6^0, x7^0
Checking conditional termination of SCC {l20}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002234s
Ranking function: -2 + x6^0
New Graphs: 
Calling Safety with literal x4^0 <= 253 and entry <l0, l1, 148 <= x4^0, {all remain the same}>

LOG: CALL check - Post:x4^0 <= 253 - Process 19
* Exit transition: <l0, l1, 148 <= x4^0, {all remain the same}>
* Postcondition  : x4^0 <= 253

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.001429s
Calling Safety with literal x4^0 <= 253 and entry <l0, l1, 148 <= undef613 /\ x0^0 = undef601 /\ x1^0 = undef609 /\ x2^0 = undef610 /\ x3^0 = undef611 /\ x5^0 = undef613, {x0^0 -> undef601, x1^0 -> undef609, x2^0 -> undef610, x3^0 -> undef611, x4^0 -> undef613, x5^0 -> undef616, x6^0 -> undef617, x7^0 -> undef602, rest remain the same}>

LOG: CALL check - Post:x4^0 <= 253 - Process 20
* Exit transition: <l0, l1, 148 <= undef613 /\ x0^0 = undef601 /\ x1^0 = undef609 /\ x2^0 = undef610 /\ x3^0 = undef611 /\ x5^0 = undef613, {x0^0 -> undef601, x1^0 -> undef609, x2^0 -> undef610, x3^0 -> undef611, x4^0 -> undef613, x5^0 -> undef616, x6^0 -> undef617, x7^0 -> undef602, rest remain the same}>
* Postcondition  : x4^0 <= 253

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.001653s
Calling Safety with literal 1 + x5^0 <= 0 and entry <l0, l20, 0 <= 0, {all remain the same}>

LOG: CALL check - Post:1 + x5^0 <= 0 - Process 21
* Exit transition: <l0, l20, 0 <= 0, {all remain the same}>
* Postcondition  : 1 + x5^0 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.001369s
Calling Safety with literal 1 + x5^0 <= 0 and entry <l0, l20, 0 <= 0 /\ x0^0 = undef751 /\ x1^0 = undef759 /\ x2^0 = undef760 /\ x3^0 = undef761 /\ x4^0 = undef762, {x0^0 -> undef751, x1^0 -> undef759, x2^0 -> undef760, x3^0 -> undef761, x4^0 -> undef762, x5^0 -> -5552 + undef762, x6^0 -> 347, x7^0 -> undef766, rest remain the same}>

LOG: CALL check - Post:1 + x5^0 <= 0 - Process 22
* Exit transition: <l0, l20, 0 <= 0 /\ x0^0 = undef751 /\ x1^0 = undef759 /\ x2^0 = undef760 /\ x3^0 = undef761 /\ x4^0 = undef762, {x0^0 -> undef751, x1^0 -> undef759, x2^0 -> undef760, x3^0 -> undef761, x4^0 -> undef762, x5^0 -> -5552 + undef762, x6^0 -> 347, x7^0 -> undef766, rest remain the same}>
* Postcondition  : 1 + x5^0 <= 0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.001627s
Calling Safety with literal x4^0 <= 253 and entry <l7, l1, 148 <= undef109 /\ x0^0 = undef101 /\ x1^0 = undef109 /\ x2^0 = undef110 /\ x3^0 = undef111, {x0^0 -> undef101, x1^0 -> undef109, x2^0 -> undef110, x3^0 -> undef111, x4^0 -> undef109, x5^0 -> undef116, x6^0 -> undef117, x7^0 -> undef102, rest remain the same}>

LOG: CALL check - Post:x4^0 <= 253 - Process 23
* Exit transition: <l7, l1, 148 <= undef109 /\ x0^0 = undef101 /\ x1^0 = undef109 /\ x2^0 = undef110 /\ x3^0 = undef111, {x0^0 -> undef101, x1^0 -> undef109, x2^0 -> undef110, x3^0 -> undef111, x4^0 -> undef109, x5^0 -> undef116, x6^0 -> undef117, x7^0 -> undef102, rest remain the same}>
* Postcondition  : x4^0 <= 253
Postcodition moved up: undef109 <= 253

LOG: Try proving POST
Postcondition: undef109 <= 253

LOG: CALL check - Post:undef109 <= 253 - Process 24
* Exit transition: <l0, l7, 148 <= undef109 /\ x0^0 = undef101 /\ x1^0 = undef109 /\ x2^0 = undef110 /\ x3^0 = undef111, {all remain the same}>
* Postcondition  : undef109 <= 253

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.001617s
Postcondition: undef109 <= 253

LOG: CALL check - Post:undef109 <= 253 - Process 25
* Exit transition: <l10, l7, 148 <= undef109 /\ x0^0 = undef176 /\ x1^0 = undef184 /\ x2^0 = undef185 /\ x3^0 = undef186 /\ undef101 = undef176 /\ undef109 = undef184 /\ undef110 = undef185 /\ undef111 = undef186, {x0^0 -> undef176, x1^0 -> undef184, x2^0 -> undef185, x3^0 -> undef186, x4^0 -> undef191, x5^0 -> undef192, x6^0 -> undef177, x7^0 -> undef178, rest remain the same}>
* Postcondition  : undef109 <= 253
Postcodition moved up: undef109 <= 253

LOG: Try proving POST
Postcondition: undef109 <= 253

LOG: CALL check - Post:undef109 <= 253 - Process 26
* Exit transition: <l0, l10, x0^0 = undef176 /\ x1^0 = undef184 /\ x2^0 = undef185 /\ x3^0 = undef186, {all remain the same}>
* Postcondition  : undef109 <= 253

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.001575s
Postcondition: undef109 <= 253

LOG: CALL check - Post:undef109 <= 253 - Process 27
* Exit transition: <l16, l10, 2 <= undef384 /\ x0^0 = undef376 /\ x1^0 = undef384 /\ undef176 = undef376 /\ undef184 = undef384 /\ undef185 = undef391 /\ undef186 = undef392, {x0^0 -> undef376, x1^0 -> undef384, x2^0 -> undef391, x3^0 -> undef392, x4^0 -> undef377, x5^0 -> undef378, x6^0 -> undef379, x7^0 -> undef380, rest remain the same}>
* Postcondition  : undef109 <= 253
Postcodition moved up: undef109 <= 253

LOG: Try proving POST
Postcondition: undef109 <= 253

LOG: CALL check - Post:undef109 <= 253 - Process 28
* Exit transition: <l0, l16, 2 <= undef384 /\ x0^0 = undef851 /\ x1^0 = undef859 /\ undef376 = undef851 /\ undef384 = undef859, {x0^0 -> undef851, x1^0 -> undef859, x2^0 -> undef866, x3^0 -> undef867, x4^0 -> undef852, x5^0 -> undef853, x6^0 -> undef854, x7^0 -> undef855, rest remain the same}>
* Postcondition  : undef109 <= 253

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.001603s
Postcondition: undef109 <= 253

LOG: CALL check - Post:undef109 <= 253 - Process 29
* Exit transition: <l0, l16, 2 <= undef384 /\ x0^0 = undef376 /\ x1^0 = undef384, {all remain the same}>
* Postcondition  : undef109 <= 253

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.001488s

LOG: NarrowEntry size 1

LOG: NarrowEntry size 1
ENTRIES:
<l0, l16, 2 <= undef384 /\ 254 <= undef109 /\ x0^0 = undef851 /\ x1^0 = undef859 /\ undef376 = undef851 /\ undef384 = undef859, {x0^0 -> undef851, x1^0 -> undef859, x2^0 -> undef866, x3^0 -> undef867, x4^0 -> undef852, x5^0 -> undef853, x6^0 -> undef854, x7^0 -> undef855, rest remain the same}>
<l0, l16, 2 <= undef384 /\ 254 <= undef109 /\ x0^0 = undef376 /\ x1^0 = undef384, {all remain the same}>
END ENTRIES:
GRAPH:
END GRAPH:
EXIT: <l16, l10, 2 <= undef384 /\ x0^0 = undef376 /\ x1^0 = undef384 /\ undef176 = undef376 /\ undef184 = undef384 /\ undef185 = undef391 /\ undef186 = undef392, {x0^0 -> undef376, x1^0 -> undef384, x2^0 -> undef391, x3^0 -> undef392, x4^0 -> undef377, x5^0 -> undef378, x6^0 -> undef379, x7^0 -> undef380, rest remain the same}>
POST: undef109 <= 253


LOG: Try proving POST
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.002578s
Time used: 4.00243

LOG: Postcondition is not implied - no solution
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 4.023172s
Postcondition: undef109 <= 253

LOG: CALL check - Post:undef109 <= 253 - Process 30
* Exit transition: <l16, l10, undef409 <= 0 /\ x0^0 = undef401 /\ x1^0 = undef409 /\ undef176 = undef401 /\ undef184 = undef409 /\ undef185 = undef416 /\ undef186 = undef417, {x0^0 -> undef401, x1^0 -> undef409, x2^0 -> undef416, x3^0 -> undef417, x4^0 -> undef402, x5^0 -> undef403, x6^0 -> undef404, x7^0 -> undef405, rest remain the same}>
* Postcondition  : undef109 <= 253
Postcodition moved up: undef109 <= 253

LOG: Try proving POST
Postcondition: undef109 <= 253

LOG: CALL check - Post:undef109 <= 253 - Process 31
* Exit transition: <l0, l16, undef409 <= 0 /\ x0^0 = undef851 /\ x1^0 = undef859 /\ undef401 = undef851 /\ undef409 = undef859, {x0^0 -> undef851, x1^0 -> undef859, x2^0 -> undef866, x3^0 -> undef867, x4^0 -> undef852, x5^0 -> undef853, x6^0 -> undef854, x7^0 -> undef855, rest remain the same}>
* Postcondition  : undef109 <= 253

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.001611s
Postcondition: undef109 <= 253

LOG: CALL check - Post:undef109 <= 253 - Process 32
* Exit transition: <l0, l16, undef409 <= 0 /\ x0^0 = undef401 /\ x1^0 = undef409, {all remain the same}>
* Postcondition  : undef109 <= 253

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.001525s

LOG: NarrowEntry size 1

LOG: NarrowEntry size 1
ENTRIES:
<l0, l16, undef409 <= 0 /\ 254 <= undef109 /\ x0^0 = undef851 /\ x1^0 = undef859 /\ undef401 = undef851 /\ undef409 = undef859, {x0^0 -> undef851, x1^0 -> undef859, x2^0 -> undef866, x3^0 -> undef867, x4^0 -> undef852, x5^0 -> undef853, x6^0 -> undef854, x7^0 -> undef855, rest remain the same}>
<l0, l16, undef409 <= 0 /\ 254 <= undef109 /\ x0^0 = undef401 /\ x1^0 = undef409, {all remain the same}>
END ENTRIES:
GRAPH:
END GRAPH:
EXIT: <l16, l10, undef409 <= 0 /\ x0^0 = undef401 /\ x1^0 = undef409 /\ undef176 = undef401 /\ undef184 = undef409 /\ undef185 = undef416 /\ undef186 = undef417, {x0^0 -> undef401, x1^0 -> undef409, x2^0 -> undef416, x3^0 -> undef417, x4^0 -> undef402, x5^0 -> undef403, x6^0 -> undef404, x7^0 -> undef405, rest remain the same}>
POST: undef109 <= 253


LOG: Try proving POST
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.004236s
Time used: 4.00409

LOG: Postcondition is not implied - no solution
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 4.030100s

LOG: NarrowEntry size 1

LOG: NarrowEntry size 1

LOG: NarrowEntry size 1
ENTRIES:
<l0, l10, 254 <= undef109 /\ x0^0 = undef176 /\ x1^0 = undef184 /\ x2^0 = undef185 /\ x3^0 = undef186, {all remain the same}>
<l16, l10, 2 <= undef384 /\ 254 <= undef109 /\ x0^0 = undef376 /\ x1^0 = undef384 /\ undef176 = undef376 /\ undef184 = undef384 /\ undef185 = undef391 /\ undef186 = undef392, {x0^0 -> undef376, x1^0 -> undef384, x2^0 -> undef391, x3^0 -> undef392, x4^0 -> undef377, x5^0 -> undef378, x6^0 -> undef379, x7^0 -> undef380, rest remain the same}>
<l16, l10, undef409 <= 0 /\ 254 <= undef109 /\ x0^0 = undef401 /\ x1^0 = undef409 /\ undef176 = undef401 /\ undef184 = undef409 /\ undef185 = undef416 /\ undef186 = undef417, {x0^0 -> undef401, x1^0 -> undef409, x2^0 -> undef416, x3^0 -> undef417, x4^0 -> undef402, x5^0 -> undef403, x6^0 -> undef404, x7^0 -> undef405, rest remain the same}>
END ENTRIES:
GRAPH:
END GRAPH:
EXIT: <l10, l7, 148 <= undef109 /\ x0^0 = undef176 /\ x1^0 = undef184 /\ x2^0 = undef185 /\ x3^0 = undef186 /\ undef101 = undef176 /\ undef109 = undef184 /\ undef110 = undef185 /\ undef111 = undef186, {x0^0 -> undef176, x1^0 -> undef184, x2^0 -> undef185, x3^0 -> undef186, x4^0 -> undef191, x5^0 -> undef192, x6^0 -> undef177, x7^0 -> undef178, rest remain the same}>
POST: undef109 <= 253


LOG: Try proving POST
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.007435s
Time used: 0.007282
Improving Solution with cost 2 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.008989s
Time used: 0.008987

LOG: SAT solveNonLinear - Elapsed time: 0.016424s
Cost: 2; Total time: 0.016269
Failed at location 10: x1^0 <= 1
Failed at location 10: x1^0 <= 1
Before Improving: 
Quasi-invariant at l10: x1^0 <= 1
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.005595s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.003751s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.003088s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002984s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002973s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002906s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002897s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002950s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002943s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002962s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002952s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002979s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002947s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002947s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002921s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002944s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002973s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002952s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002992s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002951s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002933s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002939s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002962s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002973s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002951s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.003296s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002925s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002939s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002936s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002916s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002894s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002939s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002878s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002913s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002884s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002895s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002898s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002860s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002835s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002845s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002893s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002902s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002890s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002902s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002917s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002915s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002912s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002957s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002919s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002918s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002858s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002902s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002876s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002901s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002921s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002925s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002920s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002913s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002912s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002898s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002918s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002943s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002906s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002975s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002927s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002992s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002932s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002927s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002924s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002932s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002901s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002918s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002915s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002912s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002900s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002919s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002919s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002879s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002874s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002918s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002884s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002865s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002836s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002857s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002865s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002873s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002878s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002906s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002912s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002902s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002926s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002939s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002904s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002923s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002854s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002891s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002884s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002924s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002928s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002918s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002906s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002906s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002900s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002940s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002910s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002936s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002911s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002930s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002919s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002928s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002920s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002932s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002942s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002950s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002959s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002962s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002914s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002949s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002896s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002922s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002891s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002908s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002897s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002874s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002847s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002846s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002881s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002894s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002894s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002913s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002940s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002933s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002923s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002954s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002914s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002898s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002899s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002916s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002921s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002931s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002918s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002930s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002901s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002925s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002907s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002939s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002919s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002924s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002932s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002924s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002940s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002941s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002936s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002949s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002922s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002930s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002928s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002906s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002928s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002915s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002931s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002908s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002925s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002895s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002876s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002875s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002896s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002904s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002922s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002941s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002927s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002943s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002951s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002952s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002937s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002893s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002929s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002940s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002937s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002958s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002947s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002950s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002927s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002939s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002950s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002950s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002945s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002949s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002947s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002970s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002948s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002984s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002956s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002960s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002955s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002944s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002971s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002946s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002961s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002948s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002922s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002922s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002889s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002877s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002887s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002918s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002906s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002929s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002949s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002959s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002958s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002961s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002921s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002918s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002943s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002959s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002960s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002950s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002958s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002951s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002958s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002977s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002971s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002979s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002961s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002966s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002966s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002969s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002970s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002969s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002956s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002955s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002964s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002943s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002960s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002947s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002948s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002957s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002914s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002921s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002921s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002950s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002930s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002958s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002974s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002967s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002986s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002990s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002960s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002953s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002954s
Quasi-invariant improved

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001351s
Remaining time after improvement: 0.313106
Postcondition implied by a set of quasi-invariant(s):
Quasi-invariant at l10: x1^0 <= 253
Postcondition: x1^0 <= 253

LOG: CALL check - Post:x1^0 <= 253 - Process 33
* Exit transition: <l0, l10, 254 <= undef109 /\ x0^0 = undef176 /\ x1^0 = undef184 /\ x2^0 = undef185 /\ x3^0 = undef186, {all remain the same}>
* Postcondition  : x1^0 <= 253

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.002048s
Postcondition: x1^0 <= 253

LOG: CALL check - Post:x1^0 <= 253 - Process 34
* Exit transition: <l16, l10, 2 <= undef384 /\ 254 <= undef109 /\ x0^0 = undef376 /\ x1^0 = undef384 /\ undef176 = undef376 /\ undef184 = undef384 /\ undef185 = undef391 /\ undef186 = undef392, {x0^0 -> undef376, x1^0 -> undef384, x2^0 -> undef391, x3^0 -> undef392, x4^0 -> undef377, x5^0 -> undef378, x6^0 -> undef379, x7^0 -> undef380, rest remain the same}>
* Postcondition  : x1^0 <= 253
Postcodition moved up: undef384 <= 253

LOG: Try proving POST
Postcondition: undef384 <= 253

LOG: CALL check - Post:undef384 <= 253 - Process 35
* Exit transition: <l0, l16, 2 <= undef384 /\ 254 <= undef109 /\ x0^0 = undef851 /\ x1^0 = undef859 /\ undef376 = undef851 /\ undef384 = undef859, {x0^0 -> undef851, x1^0 -> undef859, x2^0 -> undef866, x3^0 -> undef867, x4^0 -> undef852, x5^0 -> undef853, x6^0 -> undef854, x7^0 -> undef855, rest remain the same}>
* Postcondition  : undef384 <= 253

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.001709s
Postcondition: undef384 <= 253

LOG: CALL check - Post:undef384 <= 253 - Process 36
* Exit transition: <l0, l16, 2 <= undef384 /\ 254 <= undef109 /\ x0^0 = undef376 /\ x1^0 = undef384, {all remain the same}>
* Postcondition  : undef384 <= 253

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.001598s

LOG: NarrowEntry size 1

LOG: NarrowEntry size 1
ENTRIES:
<l0, l16, 254 <= undef109 /\ 254 <= undef384 /\ x0^0 = undef851 /\ x1^0 = undef859 /\ undef376 = undef851 /\ undef384 = undef859, {x0^0 -> undef851, x1^0 -> undef859, x2^0 -> undef866, x3^0 -> undef867, x4^0 -> undef852, x5^0 -> undef853, x6^0 -> undef854, x7^0 -> undef855, rest remain the same}>
<l0, l16, 254 <= undef109 /\ 254 <= undef384 /\ x0^0 = undef376 /\ x1^0 = undef384, {all remain the same}>
END ENTRIES:
GRAPH:
END GRAPH:
EXIT: <l16, l10, 2 <= undef384 /\ 254 <= undef109 /\ x0^0 = undef376 /\ x1^0 = undef384 /\ undef176 = undef376 /\ undef184 = undef384 /\ undef185 = undef391 /\ undef186 = undef392, {x0^0 -> undef376, x1^0 -> undef384, x2^0 -> undef391, x3^0 -> undef392, x4^0 -> undef377, x5^0 -> undef378, x6^0 -> undef379, x7^0 -> undef380, rest remain the same}>
POST: x1^0 <= 253


LOG: Try proving POST
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.007758s
Time used: 4.00467

LOG: Postcondition is not implied - no solution
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 4.169444s

LOG: NarrowEntry size 1

LOG: NarrowEntry size 1
INVARIANTS: 
10: 
Quasi-INVARIANTS to narrow Graph: 
10: x1^0 <= 253 , 
ENTRIES:
<l0, l10, 254 <= x1^0 /\ 254 <= undef109 /\ x0^0 = undef176 /\ x1^0 = undef184 /\ x2^0 = undef185 /\ x3^0 = undef186, {all remain the same}>
<l16, l10, 254 <= undef109 /\ 254 <= undef384 /\ x0^0 = undef376 /\ x1^0 = undef384 /\ undef176 = undef376 /\ undef184 = undef384 /\ undef185 = undef391 /\ undef186 = undef392, {x0^0 -> undef376, x1^0 -> undef384, x2^0 -> undef391, x3^0 -> undef392, x4^0 -> undef377, x5^0 -> undef378, x6^0 -> undef379, x7^0 -> undef380, rest remain the same}>
END ENTRIES:
GRAPH:
END GRAPH:
EXIT: <l10, l7, 148 <= undef109 /\ x0^0 = undef176 /\ x1^0 = undef184 /\ x2^0 = undef185 /\ x3^0 = undef186 /\ undef101 = undef176 /\ undef109 = undef184 /\ undef110 = undef185 /\ undef111 = undef186, {x0^0 -> undef176, x1^0 -> undef184, x2^0 -> undef185, x3^0 -> undef186, x4^0 -> undef191, x5^0 -> undef192, x6^0 -> undef177, x7^0 -> undef178, rest remain the same}>
POST: undef109 <= 253


LOG: Try proving POST
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.005242s
Time used: 1.00003

LOG: Postcondition is not implied - no solution
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 18.133585s

LOG: NarrowEntry size 1

LOG: NarrowEntry size 1
ENTRIES:
<l0, l7, 254 <= undef109 /\ x0^0 = undef101 /\ x1^0 = undef109 /\ x2^0 = undef110 /\ x3^0 = undef111, {all remain the same}>
<l10, l7, 254 <= undef109 /\ x0^0 = undef176 /\ x1^0 = undef184 /\ x2^0 = undef185 /\ x3^0 = undef186 /\ undef101 = undef176 /\ undef109 = undef184 /\ undef110 = undef185 /\ undef111 = undef186, {x0^0 -> undef176, x1^0 -> undef184, x2^0 -> undef185, x3^0 -> undef186, x4^0 -> undef191, x5^0 -> undef192, x6^0 -> undef177, x7^0 -> undef178, rest remain the same}>
END ENTRIES:
GRAPH:
END GRAPH:
EXIT: <l7, l1, 148 <= undef109 /\ x0^0 = undef101 /\ x1^0 = undef109 /\ x2^0 = undef110 /\ x3^0 = undef111, {x0^0 -> undef101, x1^0 -> undef109, x2^0 -> undef110, x3^0 -> undef111, x4^0 -> undef109, x5^0 -> undef116, x6^0 -> undef117, x7^0 -> undef102, rest remain the same}>
POST: x4^0 <= 253


LOG: Try proving POST
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.006000s
Time used: 1.00004

LOG: Postcondition is not implied - no solution
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 23.309322s
INVARIANTS: 
1: 
20: 
Quasi-INVARIANTS to narrow Graph: 
1: x4^0 <= 253 , 
20: 1 + x5^0 <= 0 , 
Narrowing transition: 
<l1, l20, 5552 <= undef37 /\ 148 <= x4^0 /\ x0^0 = undef26 /\ x1^0 = undef34 /\ x2^0 = undef35 /\ x3^0 = undef36 /\ x4^0 = undef37 /\ undef26 = undef751 /\ undef34 = undef759 /\ undef35 = undef760 /\ undef36 = undef761 /\ undef37 = undef762, {x0^0 -> undef751, x1^0 -> undef759, x2^0 -> undef760, x3^0 -> undef761, x4^0 -> undef762, x5^0 -> -5552 + undef762, x6^0 -> 347, x7^0 -> undef766, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l20, l1, 0 <= 0 /\ undef639 <= 1 /\ x0^0 = undef626 /\ x1^0 = undef634 /\ x2^0 = undef635 /\ x3^0 = undef636 /\ x4^0 = undef637 /\ x5^0 = undef638 /\ x6^0 = undef639 /\ undef601 = undef626 /\ undef609 = undef634 /\ undef610 = undef635 /\ undef611 = undef636 /\ undef613 = undef638, {x0^0 -> undef601, x1^0 -> undef609, x2^0 -> undef610, x3^0 -> undef611, x4^0 -> undef613, x5^0 -> undef616, x6^0 -> undef617, x7^0 -> undef602, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l20, l20, 0 <= 0 /\ 2 <= undef664 /\ x0^0 = undef651 /\ x1^0 = undef659 /\ x2^0 = undef660 /\ x3^0 = undef661 /\ x4^0 = undef662 /\ x5^0 = undef663 /\ x6^0 = undef664, {x0^0 -> undef651, x1^0 -> undef659, x2^0 -> undef660, x3^0 -> undef661, x4^0 -> undef662, x5^0 -> undef663, x6^0 -> -1 + undef664, x7^0 -> undef666, rest remain the same}>

LOG: Narrow transition size 1
invGraph after Narrowing: 
Transitions:
<l1, l20, 5552 <= undef37 /\ 254 <= x4^0 /\ x0^0 = undef26 /\ x1^0 = undef34 /\ x2^0 = undef35 /\ x3^0 = undef36 /\ x4^0 = undef37 /\ undef26 = undef751 /\ undef34 = undef759 /\ undef35 = undef760 /\ undef36 = undef761 /\ undef37 = undef762, {x0^0 -> undef751, x1^0 -> undef759, x2^0 -> undef760, x3^0 -> undef761, x4^0 -> undef762, x5^0 -> -5552 + undef762, x6^0 -> 347, x7^0 -> undef766, rest remain the same}>
<l20, l1, 0 <= 0 /\ 0 <= x5^0 /\ undef639 <= 1 /\ x0^0 = undef626 /\ x1^0 = undef634 /\ x2^0 = undef635 /\ x3^0 = undef636 /\ x4^0 = undef637 /\ x5^0 = undef638 /\ x6^0 = undef639 /\ undef601 = undef626 /\ undef609 = undef634 /\ undef610 = undef635 /\ undef611 = undef636 /\ undef613 = undef638, {x0^0 -> undef601, x1^0 -> undef609, x2^0 -> undef610, x3^0 -> undef611, x4^0 -> undef613, x5^0 -> undef616, x6^0 -> undef617, x7^0 -> undef602, rest remain the same}>
<l20, l20, 0 <= 0 /\ 0 <= x5^0 /\ 2 <= undef664 /\ x0^0 = undef651 /\ x1^0 = undef659 /\ x2^0 = undef660 /\ x3^0 = undef661 /\ x4^0 = undef662 /\ x5^0 = undef663 /\ x6^0 = undef664, {x0^0 -> undef651, x1^0 -> undef659, x2^0 -> undef660, x3^0 -> undef661, x4^0 -> undef662, x5^0 -> undef663, x6^0 -> -1 + undef664, x7^0 -> undef666, rest remain the same}>
Variables:
x0^0, x1^0, x2^0, x3^0, x4^0, x5^0, x7^0, x6^0
Checking conditional termination of SCC {l1, l20}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.003248s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.015681s
Trying to remove transition: <l20, l20, 0 <= 0 /\ 0 <= x5^0 /\ 2 <= undef664 /\ x0^0 = undef651 /\ x1^0 = undef659 /\ x2^0 = undef660 /\ x3^0 = undef661 /\ x4^0 = undef662 /\ x5^0 = undef663 /\ x6^0 = undef664, {x0^0 -> undef651, x1^0 -> undef659, x2^0 -> undef660, x3^0 -> undef661, x4^0 -> undef662, x5^0 -> undef663, x6^0 -> -1 + undef664, x7^0 -> undef666, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.015519s
Time used: 4.01143
Trying to remove transition: <l20, l1, 0 <= 0 /\ 0 <= x5^0 /\ undef639 <= 1 /\ x0^0 = undef626 /\ x1^0 = undef634 /\ x2^0 = undef635 /\ x3^0 = undef636 /\ x4^0 = undef637 /\ x5^0 = undef638 /\ x6^0 = undef639 /\ undef601 = undef626 /\ undef609 = undef634 /\ undef610 = undef635 /\ undef611 = undef636 /\ undef613 = undef638, {x0^0 -> undef601, x1^0 -> undef609, x2^0 -> undef610, x3^0 -> undef611, x4^0 -> undef613, x5^0 -> undef616, x6^0 -> undef617, x7^0 -> undef602, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.104300s
Time used: 0.023712
Trying to remove transition: <l1, l20, 5552 <= undef37 /\ 254 <= x4^0 /\ x0^0 = undef26 /\ x1^0 = undef34 /\ x2^0 = undef35 /\ x3^0 = undef36 /\ x4^0 = undef37 /\ undef26 = undef751 /\ undef34 = undef759 /\ undef35 = undef760 /\ undef36 = undef761 /\ undef37 = undef762, {x0^0 -> undef751, x1^0 -> undef759, x2^0 -> undef760, x3^0 -> undef761, x4^0 -> undef762, x5^0 -> -5552 + undef762, x6^0 -> 347, x7^0 -> undef766, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

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

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.080272s
Time used: 0.073751
Improving Solution with cost 1 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.159685s
Time used: 0.159676

LOG: SAT solveNonLinear - Elapsed time: 0.239957s
Cost: 1; Total time: 0.233427
Failed at location 20: 1 + x5^0 <= x4^0
Before Improving: 
Quasi-invariant at l20: 1 + x5^0 <= x4^0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.011103s
Remaining time after improvement: 0.993195
Termination implied by a set of quasi-invariant(s):
Quasi-invariant at l20: 1 + x5^0 <= x4^0
[ Invariant Graph ]
Strengthening and disabling transitions...

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): 
<l20, l1, 0 <= 0 /\ 0 <= x5^0 /\ 1 + x5^0 <= x4^0 /\ undef639 <= 1 /\ x0^0 = undef626 /\ x1^0 = undef634 /\ x2^0 = undef635 /\ x3^0 = undef636 /\ x4^0 = undef637 /\ x5^0 = undef638 /\ x6^0 = undef639 /\ undef601 = undef626 /\ undef609 = undef634 /\ undef610 = undef635 /\ undef611 = undef636 /\ undef613 = undef638, {x0^0 -> undef601, x1^0 -> undef609, x2^0 -> undef610, x3^0 -> undef611, x4^0 -> undef613, x5^0 -> undef616, x6^0 -> undef617, x7^0 -> undef602, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l20, l20, 0 <= 0 /\ 0 <= x5^0 /\ 1 + x5^0 <= x4^0 /\ 2 <= undef664 /\ x0^0 = undef651 /\ x1^0 = undef659 /\ x2^0 = undef660 /\ x3^0 = undef661 /\ x4^0 = undef662 /\ x5^0 = undef663 /\ x6^0 = undef664, {x0^0 -> undef651, x1^0 -> undef659, x2^0 -> undef660, x3^0 -> undef661, x4^0 -> undef662, x5^0 -> undef663, x6^0 -> -1 + undef664, x7^0 -> undef666, rest remain the same}>
[ Termination Graph ]
Strengthening and disabling transitions...

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): 
<l20, l1, 0 <= 0 /\ 0 <= x5^0 /\ 1 + x5^0 <= x4^0 /\ undef639 <= 1 /\ x0^0 = undef626 /\ x1^0 = undef634 /\ x2^0 = undef635 /\ x3^0 = undef636 /\ x4^0 = undef637 /\ x5^0 = undef638 /\ x6^0 = undef639 /\ undef601 = undef626 /\ undef609 = undef634 /\ undef610 = undef635 /\ undef611 = undef636 /\ undef613 = undef638, {x0^0 -> undef601, x1^0 -> undef609, x2^0 -> undef610, x3^0 -> undef611, x4^0 -> undef613, x5^0 -> undef616, x6^0 -> undef617, x7^0 -> undef602, rest remain the same}>

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l20, l20, 0 <= 0 /\ 0 <= x5^0 /\ 1 + x5^0 <= x4^0 /\ 2 <= undef664 /\ x0^0 = undef651 /\ x1^0 = undef659 /\ x2^0 = undef660 /\ x3^0 = undef661 /\ x4^0 = undef662 /\ x5^0 = undef663 /\ x6^0 = undef664, {x0^0 -> undef651, x1^0 -> undef659, x2^0 -> undef660, x3^0 -> undef661, x4^0 -> undef662, x5^0 -> undef663, x6^0 -> -1 + undef664, x7^0 -> undef666, rest remain the same}>
Ranking function: x4^0
New Graphs: 
Transitions:
<l20, l20, 0 <= 0 /\ 0 <= x5^0 /\ 1 + x5^0 <= x4^0 /\ 2 <= undef664 /\ x0^0 = undef651 /\ x1^0 = undef659 /\ x2^0 = undef660 /\ x3^0 = undef661 /\ x4^0 = undef662 /\ x5^0 = undef663 /\ x6^0 = undef664, {x0^0 -> undef651, x1^0 -> undef659, x2^0 -> undef660, x3^0 -> undef661, x4^0 -> undef662, x5^0 -> undef663, x6^0 -> -1 + undef664, x7^0 -> undef666, rest remain the same}>
Variables:
x0^0, x1^0, x2^0, x3^0, x4^0, x5^0, x6^0, x7^0
Checking conditional termination of SCC {l20}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002302s
Ranking function: -2 + x6^0
New Graphs: 
Calling Safety with literal 1 + x5^0 <= x4^0 and entry <l0, l20, 0 <= 0 /\ 0 <= x5^0, {all remain the same}>

LOG: CALL check - Post:1 + x5^0 <= x4^0 - Process 37
* Exit transition: <l0, l20, 0 <= 0 /\ 0 <= x5^0, {all remain the same}>
* Postcondition  : 1 + x5^0 <= x4^0

LOG: CALL solveLinear

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

LOG: RETURN check - Elapsed time: 0.001438s
INVARIANTS: 
20: 
Quasi-INVARIANTS to narrow Graph: 
20: 1 + x5^0 <= x4^0 , 
It's unfeasible. Removing transition: 
<l1, l20, 5552 <= undef37 /\ 254 <= x4^0 /\ x0^0 = undef26 /\ x1^0 = undef34 /\ x2^0 = undef35 /\ x3^0 = undef36 /\ x4^0 = undef37 /\ undef26 = undef751 /\ undef34 = undef759 /\ undef35 = undef760 /\ undef36 = undef761 /\ undef37 = undef762, {x0^0 -> undef751, x1^0 -> undef759, x2^0 -> undef760, x3^0 -> undef761, x4^0 -> undef762, x5^0 -> -5552 + undef762, x6^0 -> 347, x7^0 -> undef766, rest remain the same}>
Narrowing transition: 
<l20, l1, 0 <= 0 /\ 0 <= x5^0 /\ undef639 <= 1 /\ x0^0 = undef626 /\ x1^0 = undef634 /\ x2^0 = undef635 /\ x3^0 = undef636 /\ x4^0 = undef637 /\ x5^0 = undef638 /\ x6^0 = undef639 /\ undef601 = undef626 /\ undef609 = undef634 /\ undef610 = undef635 /\ undef611 = undef636 /\ undef613 = undef638, {x0^0 -> undef601, x1^0 -> undef609, x2^0 -> undef610, x3^0 -> undef611, x4^0 -> undef613, x5^0 -> undef616, x6^0 -> undef617, x7^0 -> undef602, rest remain the same}>

LOG: Narrow transition size 1
Narrowing transition: 
<l20, l20, 0 <= 0 /\ 0 <= x5^0 /\ 2 <= undef664 /\ x0^0 = undef651 /\ x1^0 = undef659 /\ x2^0 = undef660 /\ x3^0 = undef661 /\ x4^0 = undef662 /\ x5^0 = undef663 /\ x6^0 = undef664, {x0^0 -> undef651, x1^0 -> undef659, x2^0 -> undef660, x3^0 -> undef661, x4^0 -> undef662, x5^0 -> undef663, x6^0 -> -1 + undef664, x7^0 -> undef666, rest remain the same}>

LOG: Narrow transition size 1
invGraph after Narrowing: 
Transitions:
<l20, l1, 0 <= 0 /\ x4^0 <= x5^0 /\ 0 <= x5^0 /\ undef639 <= 1 /\ x0^0 = undef626 /\ x1^0 = undef634 /\ x2^0 = undef635 /\ x3^0 = undef636 /\ x4^0 = undef637 /\ x5^0 = undef638 /\ x6^0 = undef639 /\ undef601 = undef626 /\ undef609 = undef634 /\ undef610 = undef635 /\ undef611 = undef636 /\ undef613 = undef638, {x0^0 -> undef601, x1^0 -> undef609, x2^0 -> undef610, x3^0 -> undef611, x4^0 -> undef613, x5^0 -> undef616, x6^0 -> undef617, x7^0 -> undef602, rest remain the same}>
<l20, l20, 0 <= 0 /\ x4^0 <= x5^0 /\ 0 <= x5^0 /\ 2 <= undef664 /\ x0^0 = undef651 /\ x1^0 = undef659 /\ x2^0 = undef660 /\ x3^0 = undef661 /\ x4^0 = undef662 /\ x5^0 = undef663 /\ x6^0 = undef664, {x0^0 -> undef651, x1^0 -> undef659, x2^0 -> undef660, x3^0 -> undef661, x4^0 -> undef662, x5^0 -> undef663, x6^0 -> -1 + undef664, x7^0 -> undef666, rest remain the same}>
Variables:
x0^0, x1^0, x2^0, x3^0, x4^0, x5^0, x7^0, x6^0
Checking conditional termination of SCC {l20}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002198s
Ranking function: -2 + x6^0
New Graphs: 
Proving termination of subgraph 8
Analyzing SCC {l2}...
No cycles found.

Proving termination of subgraph 9
Checking unfeasibility...
Time used: 0.005072

Checking conditional termination of SCC {l18}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.003458s
Ranking function: -1 + (1 / 16)*x5^0
New Graphs: 
Proving termination of subgraph 10
Checking unfeasibility...
Time used: 0.004833

Checking conditional termination of SCC {l13}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.003504s
Ranking function: -1 + x6^0
New Graphs: 
Proving termination of subgraph 11
Analyzing SCC {l9}...
No cycles found.

Program Terminates