NO Solver Timeout: 4 Global Timeout: 300 No parsing errors! Init Location: 0 Transitions: 1, is_aborted^0 -> (0 + undef7), is_aborted_next^0 -> undef7, pc_Drive^0 -> (0 + undef11), pc_Drive_next^0 -> undef11, pc_Loop^0 -> 1, pc_Plan^0 -> undef13, pc_Plan_next^0 -> undef14, x^0 -> (0 + undef16), x_next^0 -> undef16, y^0 -> (0 + undef18), y_next^0 -> undef18}> (0 + undef25), is_aborted_next^0 -> undef25, pc_Drive^0 -> (0 + undef29), pc_Drive_next^0 -> undef29, pc_Loop^0 -> 1, pc_Plan^0 -> undef31, pc_Plan_next^0 -> undef32, x^0 -> (0 + undef34), x_next^0 -> undef34, y^0 -> (0 + undef36), y_next^0 -> undef36}> (0 + undef43), is_aborted_next^0 -> undef43, pc_Drive^0 -> (0 + undef47), pc_Drive_next^0 -> undef47, pc_Loop^0 -> 1, pc_Plan^0 -> undef49, pc_Plan_next^0 -> undef50, x^0 -> (0 + undef52), x_next^0 -> undef52, y^0 -> (0 + undef54), y_next^0 -> undef54}> 1, is_aborted^0 -> (0 + undef61), is_aborted_next^0 -> undef61, pc_Drive^0 -> (0 + undef65), pc_Drive_next^0 -> undef65, pc_Loop^0 -> 1, pc_Plan^0 -> undef67, pc_Plan_next^0 -> undef68, x^0 -> (0 + undef70), x_next^0 -> undef70, y^0 -> (0 + undef72), y_next^0 -> undef72}> (0 + undef79), is_aborted_next^0 -> undef79, pc_Drive^0 -> (0 + undef83), pc_Drive_next^0 -> undef83, pc_Loop^0 -> 1, pc_Plan^0 -> undef85, pc_Plan_next^0 -> undef86, x^0 -> (0 + undef88), x_next^0 -> undef88, y^0 -> (0 + undef90), y_next^0 -> undef90}> (0 + undef97), is_aborted_next^0 -> undef97, pc_Drive^0 -> (0 + undef101), pc_Drive_next^0 -> undef101, pc_Loop^0 -> 1, pc_Plan^0 -> undef103, pc_Plan_next^0 -> undef104, x^0 -> (0 + undef106), x_next^0 -> undef106, y^0 -> (0 + undef108), y_next^0 -> undef108}> undef112, is_aborted^0 -> (0 + undef115), is_aborted_next^0 -> undef115, pc_Drive^0 -> undef118, pc_Drive_next^0 -> undef119, pc_Loop^0 -> 4, pc_Plan^0 -> (0 + undef122), pc_Plan_next^0 -> undef122, x^0 -> (0 + undef124), x_next^0 -> undef124, y^0 -> (0 + undef126), y_next^0 -> undef126}> (0 + undef133), is_aborted_next^0 -> undef133, pc_Drive^0 -> undef136, pc_Drive_next^0 -> undef137, pc_Loop^0 -> 4, pc_Plan^0 -> (0 + undef140), pc_Plan_next^0 -> undef140, x^0 -> (0 + undef142), x_next^0 -> undef142, y^0 -> (0 + undef144), y_next^0 -> undef144}> (0 + undef151), is_aborted_next^0 -> undef151, pc_Drive^0 -> undef154, pc_Drive_next^0 -> undef155, pc_Loop^0 -> 4, pc_Plan^0 -> (0 + undef158), pc_Plan_next^0 -> undef158, x^0 -> (0 + undef160), x_next^0 -> undef160, y^0 -> (0 + undef162), y_next^0 -> undef162}> 1, is_aborted^0 -> (0 + undef169), is_aborted_next^0 -> undef169, pc_Drive^0 -> undef172, pc_Drive_next^0 -> undef173, pc_Loop^0 -> 4, pc_Plan^0 -> (0 + undef176), pc_Plan_next^0 -> undef176, x^0 -> (0 + undef178), x_next^0 -> undef178, y^0 -> (0 + undef180), y_next^0 -> undef180}> 0, is_aborted^0 -> (0 + undef187), is_aborted_next^0 -> undef187, pc_Drive^0 -> undef190, pc_Drive_next^0 -> undef191, pc_Loop^0 -> 4, pc_Plan^0 -> (0 + undef194), pc_Plan_next^0 -> undef194, x^0 -> (0 + undef196), x_next^0 -> undef196, y^0 -> (0 + undef198), y_next^0 -> undef198}> 0, is_aborted^0 -> (0 + undef205), is_aborted_next^0 -> undef205, pc_Drive^0 -> undef208, pc_Drive_next^0 -> undef209, pc_Loop^0 -> 4, pc_Plan^0 -> (0 + undef212), pc_Plan_next^0 -> undef212, x^0 -> (0 + undef214), x_next^0 -> undef214, y^0 -> (0 + undef216), y_next^0 -> undef216}> 1, is_aborted^0 -> undef222, is_aborted_next^0 -> undef223, pc_Drive^0 -> (0 + undef227), pc_Drive_next^0 -> undef227, pc_Loop^0 -> (0 + __const_7^0), pc_Plan^0 -> (0 + undef230), pc_Plan_next^0 -> undef230, x^0 -> (0 + undef232), x_next^0 -> undef232, y^0 -> (0 + undef234), y_next^0 -> undef234}> undef240, is_aborted_next^0 -> undef241, pc_Drive^0 -> (0 + undef245), pc_Drive_next^0 -> undef245, pc_Loop^0 -> (0 + __const_7^0), pc_Plan^0 -> (0 + undef248), pc_Plan_next^0 -> undef248, x^0 -> (0 + undef250), x_next^0 -> undef250, y^0 -> (0 + undef252), y_next^0 -> undef252}> undef258, is_aborted_next^0 -> undef259, pc_Drive^0 -> (0 + undef263), pc_Drive_next^0 -> undef263, pc_Loop^0 -> (0 + __const_7^0), pc_Plan^0 -> (0 + undef266), pc_Plan_next^0 -> undef266, x^0 -> (0 + undef268), x_next^0 -> undef268, y^0 -> (0 + undef270), y_next^0 -> undef270}> 1, is_aborted^0 -> undef276, is_aborted_next^0 -> undef277, pc_Drive^0 -> (0 + undef281), pc_Drive_next^0 -> undef281, pc_Loop^0 -> (0 + __const_7^0), pc_Plan^0 -> (0 + undef284), pc_Plan_next^0 -> undef284, x^0 -> undef285, x_next^0 -> undef286, y^0 -> undef287, y_next^0 -> undef288}> undef294, is_aborted_next^0 -> undef295, pc_Drive^0 -> (0 + undef299), pc_Drive_next^0 -> undef299, pc_Loop^0 -> (0 + __const_7^0), pc_Plan^0 -> (0 + undef302), pc_Plan_next^0 -> undef302, x^0 -> undef303, x_next^0 -> undef304, y^0 -> undef305, y_next^0 -> undef306}> undef312, is_aborted_next^0 -> undef313, pc_Drive^0 -> (0 + undef317), pc_Drive_next^0 -> undef317, pc_Loop^0 -> (0 + __const_7^0), pc_Plan^0 -> (0 + undef320), pc_Plan_next^0 -> undef320, x^0 -> undef321, x_next^0 -> undef322, y^0 -> undef323, y_next^0 -> undef324}> undef328, is_aborted^0 -> undef330, is_aborted_next^0 -> undef331, pc_Drive^0 -> (0 + undef335), pc_Drive_next^0 -> undef335, pc_Loop^0 -> 2, pc_Plan^0 -> (0 + undef338), pc_Plan_next^0 -> undef338, x^0 -> undef339, x_next^0 -> undef340, y^0 -> undef341, y_next^0 -> undef342}> undef348, is_aborted_next^0 -> undef349, pc_Drive^0 -> (0 + undef353), pc_Drive_next^0 -> undef353, pc_Loop^0 -> 2, pc_Plan^0 -> (0 + undef356), pc_Plan_next^0 -> undef356, x^0 -> undef357, x_next^0 -> undef358, y^0 -> undef359, y_next^0 -> undef360}> undef366, is_aborted_next^0 -> undef367, pc_Drive^0 -> (0 + undef371), pc_Drive_next^0 -> undef371, pc_Loop^0 -> 2, pc_Plan^0 -> (0 + undef374), pc_Plan_next^0 -> undef374, x^0 -> undef375, x_next^0 -> undef376, y^0 -> undef377, y_next^0 -> undef378}> 1, is_aborted^0 -> undef384, is_aborted_next^0 -> undef385, pc_Drive^0 -> (0 + undef389), pc_Drive_next^0 -> undef389, pc_Loop^0 -> (0 + __const_6^0), pc_Plan^0 -> (0 + undef392), pc_Plan_next^0 -> undef392, x^0 -> (0 + undef394), x_next^0 -> undef394, y^0 -> (0 + undef396), y_next^0 -> undef396}> undef402, is_aborted_next^0 -> undef403, pc_Drive^0 -> (0 + undef407), pc_Drive_next^0 -> undef407, pc_Loop^0 -> (0 + __const_6^0), pc_Plan^0 -> (0 + undef410), pc_Plan_next^0 -> undef410, x^0 -> (0 + undef412), x_next^0 -> undef412, y^0 -> (0 + undef414), y_next^0 -> undef414}> undef420, is_aborted_next^0 -> undef421, pc_Drive^0 -> (0 + undef425), pc_Drive_next^0 -> undef425, pc_Loop^0 -> (0 + __const_6^0), pc_Plan^0 -> (0 + undef428), pc_Plan_next^0 -> undef428, x^0 -> (0 + undef430), x_next^0 -> undef430, y^0 -> (0 + undef432), y_next^0 -> undef432}> 1, is_aborted^0 -> undef438, is_aborted_next^0 -> undef439, pc_Drive^0 -> (0 + undef443), pc_Drive_next^0 -> undef443, pc_Loop^0 -> 3, pc_Plan^0 -> (0 + undef446), pc_Plan_next^0 -> undef446, x^0 -> (0 + undef448), x_next^0 -> undef448, y^0 -> (0 + undef450), y_next^0 -> undef450}> undef456, is_aborted_next^0 -> undef457, pc_Drive^0 -> (0 + undef461), pc_Drive_next^0 -> undef461, pc_Loop^0 -> 3, pc_Plan^0 -> (0 + undef464), pc_Plan_next^0 -> undef464, x^0 -> (0 + undef466), x_next^0 -> undef466, y^0 -> (0 + undef468), y_next^0 -> undef468}> undef474, is_aborted_next^0 -> undef475, pc_Drive^0 -> (0 + undef479), pc_Drive_next^0 -> undef479, pc_Loop^0 -> 3, pc_Plan^0 -> (0 + undef482), pc_Plan_next^0 -> undef482, x^0 -> (0 + undef484), x_next^0 -> undef484, y^0 -> (0 + undef486), y_next^0 -> undef486}> 1, is_aborted^0 -> undef492, is_aborted_next^0 -> undef493, pc_Drive^0 -> (0 + undef497), pc_Drive_next^0 -> undef497, pc_Loop^0 -> (0 + __const_7^0), pc_Plan^0 -> (0 + undef500), pc_Plan_next^0 -> undef500, x^0 -> (0 + undef502), x_next^0 -> undef502, y^0 -> (0 + undef504), y_next^0 -> undef504}> undef510, is_aborted_next^0 -> undef511, pc_Drive^0 -> (0 + undef515), pc_Drive_next^0 -> undef515, pc_Loop^0 -> (0 + __const_7^0), pc_Plan^0 -> (0 + undef518), pc_Plan_next^0 -> undef518, x^0 -> (0 + undef520), x_next^0 -> undef520, y^0 -> (0 + undef522), y_next^0 -> undef522}> undef528, is_aborted_next^0 -> undef529, pc_Drive^0 -> (0 + undef533), pc_Drive_next^0 -> undef533, pc_Loop^0 -> (0 + __const_7^0), pc_Plan^0 -> (0 + undef536), pc_Plan_next^0 -> undef536, x^0 -> (0 + undef538), x_next^0 -> undef538, y^0 -> (0 + undef540), y_next^0 -> undef540}> 0, fair^0 -> (~(1) + fair^0), is_aborted^0 -> undef546, is_aborted_next^0 -> undef547, pc_Drive^0 -> (0 + undef551), pc_Drive_next^0 -> undef551, pc_Loop^0 -> (0 + __const_7^0), pc_Plan^0 -> (0 + undef554), pc_Plan_next^0 -> undef554, x^0 -> (0 + undef556), x_next^0 -> undef556, y^0 -> (0 + undef558), y_next^0 -> undef558}> 1, is_aborted^0 -> undef564, is_aborted_next^0 -> undef565, pc_Drive^0 -> (0 + undef569), pc_Drive_next^0 -> undef569, pc_Loop^0 -> 2, pc_Plan^0 -> undef571, pc_Plan_next^0 -> undef572, x^0 -> (0 + undef574), x_next^0 -> undef574, y^0 -> (0 + undef576), y_next^0 -> undef576}> 0, is_aborted^0 -> undef582, is_aborted_next^0 -> undef583, pc_Drive^0 -> (0 + undef587), pc_Drive_next^0 -> undef587, pc_Loop^0 -> 2, pc_Plan^0 -> undef589, pc_Plan_next^0 -> undef590, x^0 -> (0 + undef592), x_next^0 -> undef592, y^0 -> (0 + undef594), y_next^0 -> undef594}> 0, is_aborted^0 -> undef600, is_aborted_next^0 -> undef601, pc_Drive^0 -> (0 + undef605), pc_Drive_next^0 -> undef605, pc_Loop^0 -> 2, pc_Plan^0 -> undef607, pc_Plan_next^0 -> undef608, x^0 -> (0 + undef610), x_next^0 -> undef610, y^0 -> (0 + undef612), y_next^0 -> undef612}> 1, is_aborted^0 -> undef618, is_aborted_next^0 -> undef619, pc_Drive^0 -> (0 + undef623), pc_Drive_next^0 -> undef623, pc_Loop^0 -> (0 + __const_7^0), pc_Plan^0 -> (0 + undef626), pc_Plan_next^0 -> undef626, x^0 -> (0 + undef628), x_next^0 -> undef628, y^0 -> (0 + undef630), y_next^0 -> undef630}> 0, is_aborted^0 -> undef636, is_aborted_next^0 -> undef637, pc_Drive^0 -> (0 + undef641), pc_Drive_next^0 -> undef641, pc_Loop^0 -> (0 + __const_7^0), pc_Plan^0 -> (0 + undef644), pc_Plan_next^0 -> undef644, x^0 -> (0 + undef646), x_next^0 -> undef646, y^0 -> (0 + undef648), y_next^0 -> undef648}> Fresh variables: undef7, undef11, undef13, undef14, undef16, undef18, undef25, undef29, undef31, undef32, undef34, undef36, undef43, undef47, undef49, undef50, undef52, undef54, undef61, undef65, undef67, undef68, undef70, undef72, undef79, undef83, undef85, undef86, undef88, undef90, undef97, undef101, undef103, undef104, undef106, undef108, undef112, undef115, undef118, undef119, undef122, undef124, undef126, undef133, undef136, undef137, undef140, undef142, undef144, undef151, undef154, undef155, undef158, undef160, undef162, undef169, undef172, undef173, undef176, undef178, undef180, undef187, undef190, undef191, undef194, undef196, undef198, undef205, undef208, undef209, undef212, undef214, undef216, undef222, undef223, undef227, undef230, undef232, undef234, undef240, undef241, undef245, undef248, undef250, undef252, undef258, undef259, undef263, undef266, undef268, undef270, undef276, undef277, undef281, undef284, undef285, undef286, undef287, undef288, undef294, undef295, undef299, undef302, undef303, undef304, undef305, undef306, undef312, undef313, undef317, undef320, undef321, undef322, undef323, undef324, undef328, undef330, undef331, undef335, undef338, undef339, undef340, undef341, undef342, undef348, undef349, undef353, undef356, undef357, undef358, undef359, undef360, undef366, undef367, undef371, undef374, undef375, undef376, undef377, undef378, undef384, undef385, undef389, undef392, undef394, undef396, undef402, undef403, undef407, undef410, undef412, undef414, undef420, undef421, undef425, undef428, undef430, undef432, undef438, undef439, undef443, undef446, undef448, undef450, undef456, undef457, undef461, undef464, undef466, undef468, undef474, undef475, undef479, undef482, undef484, undef486, undef492, undef493, undef497, undef500, undef502, undef504, undef510, undef511, undef515, undef518, undef520, undef522, undef528, undef529, undef533, undef536, undef538, undef540, undef546, undef547, undef551, undef554, undef556, undef558, undef564, undef565, undef569, undef571, undef572, undef574, undef576, undef582, undef583, undef587, undef589, undef590, undef592, undef594, undef600, undef601, undef605, undef607, undef608, undef610, undef612, undef618, undef619, undef623, undef626, undef628, undef630, undef636, undef637, undef641, undef644, undef646, undef648, Undef variables: undef7, undef11, undef13, undef14, undef16, undef18, undef25, undef29, undef31, undef32, undef34, undef36, undef43, undef47, undef49, undef50, undef52, undef54, undef61, undef65, undef67, undef68, undef70, undef72, undef79, undef83, undef85, undef86, undef88, undef90, undef97, undef101, undef103, undef104, undef106, undef108, undef112, undef115, undef118, undef119, undef122, undef124, undef126, undef133, undef136, undef137, undef140, undef142, undef144, undef151, undef154, undef155, undef158, undef160, undef162, undef169, undef172, undef173, undef176, undef178, undef180, undef187, undef190, undef191, undef194, undef196, undef198, undef205, undef208, undef209, undef212, undef214, undef216, undef222, undef223, undef227, undef230, undef232, undef234, undef240, undef241, undef245, undef248, undef250, undef252, undef258, undef259, undef263, undef266, undef268, undef270, undef276, undef277, undef281, undef284, undef285, undef286, undef287, undef288, undef294, undef295, undef299, undef302, undef303, undef304, undef305, undef306, undef312, undef313, undef317, undef320, undef321, undef322, undef323, undef324, undef328, undef330, undef331, undef335, undef338, undef339, undef340, undef341, undef342, undef348, undef349, undef353, undef356, undef357, undef358, undef359, undef360, undef366, undef367, undef371, undef374, undef375, undef376, undef377, undef378, undef384, undef385, undef389, undef392, undef394, undef396, undef402, undef403, undef407, undef410, undef412, undef414, undef420, undef421, undef425, undef428, undef430, undef432, undef438, undef439, undef443, undef446, undef448, undef450, undef456, undef457, undef461, undef464, undef466, undef468, undef474, undef475, undef479, undef482, undef484, undef486, undef492, undef493, undef497, undef500, undef502, undef504, undef510, undef511, undef515, undef518, undef520, undef522, undef528, undef529, undef533, undef536, undef538, undef540, undef546, undef547, undef551, undef554, undef556, undef558, undef564, undef565, undef569, undef571, undef572, undef574, undef576, undef582, undef583, undef587, undef589, undef590, undef592, undef594, undef600, undef601, undef605, undef607, undef608, undef610, undef612, undef618, undef619, undef623, undef626, undef628, undef630, undef636, undef637, undef641, undef644, undef646, undef648, Abstraction variables: Exit nodes: Accepting locations: Asserts: Preprocessed LLVMGraph Init Location: 0 Transitions: 0, fair^0 -> (~(1) + fair^0), x^0 -> (0 + undef556), y^0 -> (0 + undef558)}> 1, x^0 -> (0 + undef574), y^0 -> (0 + undef576)}> 0, x^0 -> (0 + undef592), y^0 -> (0 + undef594)}> 0, x^0 -> (0 + undef610), y^0 -> (0 + undef612)}> 1, x^0 -> (0 + undef628), y^0 -> (0 + undef630)}> 0, x^0 -> (0 + undef646), y^0 -> (0 + undef648)}> 1, x^0 -> (0 + undef232), y^0 -> (0 + undef234)}> undef112, x^0 -> (0 + undef250), y^0 -> (0 + undef252)}> undef112, x^0 -> (0 + undef268), y^0 -> (0 + undef270)}> 1, x^0 -> undef285, y^0 -> undef287}> undef112, x^0 -> undef303, y^0 -> undef305}> undef112, x^0 -> undef321, y^0 -> undef323}> undef328, x^0 -> undef339, y^0 -> undef341}> undef112, x^0 -> undef357, y^0 -> undef359}> undef112, x^0 -> undef375, y^0 -> undef377}> 1, x^0 -> (0 + undef232), y^0 -> (0 + undef234)}> (0 + undef250), y^0 -> (0 + undef252)}> (0 + undef268), y^0 -> (0 + undef270)}> 1, x^0 -> undef285, y^0 -> undef287}> undef303, y^0 -> undef305}> undef321, y^0 -> undef323}> undef328, x^0 -> undef339, y^0 -> undef341}> undef357, y^0 -> undef359}> undef375, y^0 -> undef377}> 1, x^0 -> (0 + undef232), y^0 -> (0 + undef234)}> (0 + undef250), y^0 -> (0 + undef252)}> (0 + undef268), y^0 -> (0 + undef270)}> 1, x^0 -> undef285, y^0 -> undef287}> undef303, y^0 -> undef305}> undef321, y^0 -> undef323}> undef328, x^0 -> undef339, y^0 -> undef341}> undef357, y^0 -> undef359}> undef375, y^0 -> undef377}> 1, x^0 -> (0 + undef232), y^0 -> (0 + undef234)}> 0, x^0 -> (0 + undef250), y^0 -> (0 + undef252)}> 0, x^0 -> (0 + undef268), y^0 -> (0 + undef270)}> 1, x^0 -> undef285, y^0 -> undef287}> 0, x^0 -> undef303, y^0 -> undef305}> 0, x^0 -> undef321, y^0 -> undef323}> undef328, x^0 -> undef339, y^0 -> undef341}> 1, x^0 -> (0 + undef394), y^0 -> (0 + undef396)}> 1, x^0 -> (0 + undef412), y^0 -> (0 + undef414)}> 1, x^0 -> (0 + undef430), y^0 -> (0 + undef432)}> 1, x^0 -> (0 + undef394), y^0 -> (0 + undef396)}> (0 + undef412), y^0 -> (0 + undef414)}> (0 + undef430), y^0 -> (0 + undef432)}> 1, x^0 -> (0 + undef394), y^0 -> (0 + undef396)}> (0 + undef412), y^0 -> (0 + undef414)}> (0 + undef430), y^0 -> (0 + undef432)}> 1, x^0 -> (0 + undef502), y^0 -> (0 + undef504)}> (0 + undef520), y^0 -> (0 + undef522)}> (0 + undef538), y^0 -> (0 + undef540)}> Fresh variables: undef7, undef11, undef13, undef14, undef16, undef18, undef25, undef29, undef31, undef32, undef34, undef36, undef43, undef47, undef49, undef50, undef52, undef54, undef61, undef65, undef67, undef68, undef70, undef72, undef79, undef83, undef85, undef86, undef88, undef90, undef97, undef101, undef103, undef104, undef106, undef108, undef112, undef115, undef118, undef119, undef122, undef124, undef126, undef133, undef136, undef137, undef140, undef142, undef144, undef151, undef154, undef155, undef158, undef160, undef162, undef169, undef172, undef173, undef176, undef178, undef180, undef187, undef190, undef191, undef194, undef196, undef198, undef205, undef208, undef209, undef212, undef214, undef216, undef222, undef223, undef227, undef230, undef232, undef234, undef240, undef241, undef245, undef248, undef250, undef252, undef258, undef259, undef263, undef266, undef268, undef270, undef276, undef277, undef281, undef284, undef285, undef286, undef287, undef288, undef294, undef295, undef299, undef302, undef303, undef304, undef305, undef306, undef312, undef313, undef317, undef320, undef321, undef322, undef323, undef324, undef328, undef330, undef331, undef335, undef338, undef339, undef340, undef341, undef342, undef348, undef349, undef353, undef356, undef357, undef358, undef359, undef360, undef366, undef367, undef371, undef374, undef375, undef376, undef377, undef378, undef384, undef385, undef389, undef392, undef394, undef396, undef402, undef403, undef407, undef410, undef412, undef414, undef420, undef421, undef425, undef428, undef430, undef432, undef438, undef439, undef443, undef446, undef448, undef450, undef456, undef457, undef461, undef464, undef466, undef468, undef474, undef475, undef479, undef482, undef484, undef486, undef492, undef493, undef497, undef500, undef502, undef504, undef510, undef511, undef515, undef518, undef520, undef522, undef528, undef529, undef533, undef536, undef538, undef540, undef546, undef547, undef551, undef554, undef556, undef558, undef564, undef565, undef569, undef571, undef572, undef574, undef576, undef582, undef583, undef587, undef589, undef590, undef592, undef594, undef600, undef601, undef605, undef607, undef608, undef610, undef612, undef618, undef619, undef623, undef626, undef628, undef630, undef636, undef637, undef641, undef644, undef646, undef648, Undef variables: undef7, undef11, undef13, undef14, undef16, undef18, undef25, undef29, undef31, undef32, undef34, undef36, undef43, undef47, undef49, undef50, undef52, undef54, undef61, undef65, undef67, undef68, undef70, undef72, undef79, undef83, undef85, undef86, undef88, undef90, undef97, undef101, undef103, undef104, undef106, undef108, undef112, undef115, undef118, undef119, undef122, undef124, undef126, undef133, undef136, undef137, undef140, undef142, undef144, undef151, undef154, undef155, undef158, undef160, undef162, undef169, undef172, undef173, undef176, undef178, undef180, undef187, undef190, undef191, undef194, undef196, undef198, undef205, undef208, undef209, undef212, undef214, undef216, undef222, undef223, undef227, undef230, undef232, undef234, undef240, undef241, undef245, undef248, undef250, undef252, undef258, undef259, undef263, undef266, undef268, undef270, undef276, undef277, undef281, undef284, undef285, undef286, undef287, undef288, undef294, undef295, undef299, undef302, undef303, undef304, undef305, undef306, undef312, undef313, undef317, undef320, undef321, undef322, undef323, undef324, undef328, undef330, undef331, undef335, undef338, undef339, undef340, undef341, undef342, undef348, undef349, undef353, undef356, undef357, undef358, undef359, undef360, undef366, undef367, undef371, undef374, undef375, undef376, undef377, undef378, undef384, undef385, undef389, undef392, undef394, undef396, undef402, undef403, undef407, undef410, undef412, undef414, undef420, undef421, undef425, undef428, undef430, undef432, undef438, undef439, undef443, undef446, undef448, undef450, undef456, undef457, undef461, undef464, undef466, undef468, undef474, undef475, undef479, undef482, undef484, undef486, undef492, undef493, undef497, undef500, undef502, undef504, undef510, undef511, undef515, undef518, undef520, undef522, undef528, undef529, undef533, undef536, undef538, undef540, undef546, undef547, undef551, undef554, undef556, undef558, undef564, undef565, undef569, undef571, undef572, undef574, undef576, undef582, undef583, undef587, undef589, undef590, undef592, undef594, undef600, undef601, undef605, undef607, undef608, undef610, undef612, undef618, undef619, undef623, undef626, undef628, undef630, undef636, undef637, undef641, undef644, undef646, undef648, Abstraction variables: Exit nodes: Accepting locations: Asserts: ************************************************************* ******************************************************************************************* *********************** WORKING TRANSITION SYSTEM (DAG) *********************** ******************************************************************************************* Init Location: 0 Graph 0: Transitions: Variables: Graph 1: Transitions: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> undef112, x^0 -> undef357, y^0 -> undef359, rest remain the same}> undef112, x^0 -> undef375, y^0 -> undef377, rest remain the same}> undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> undef357, y^0 -> undef359, rest remain the same}> undef375, y^0 -> undef377, rest remain the same}> undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> undef357, y^0 -> undef359, rest remain the same}> undef375, y^0 -> undef377, rest remain the same}> undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Graph 2: Transitions: Variables: Precedence: Graph 0 Graph 1 1, x^0 -> undef574, y^0 -> undef576, rest remain the same}> 0, x^0 -> undef592, y^0 -> undef594, rest remain the same}> 0, x^0 -> undef610, y^0 -> undef612, rest remain the same}> Graph 2 0, fair^0 -> -1 + fair^0, x^0 -> undef556, y^0 -> undef558, rest remain the same}> 1, x^0 -> undef628, y^0 -> undef630, rest remain the same}> 0, x^0 -> undef646, y^0 -> undef648, rest remain the same}> 1, x^0 -> undef232, y^0 -> undef234, rest remain the same}> undef112, x^0 -> undef250, y^0 -> undef252, rest remain the same}> undef112, x^0 -> undef268, y^0 -> undef270, rest remain the same}> 1, x^0 -> undef285, y^0 -> undef287, rest remain the same}> undef112, x^0 -> undef303, y^0 -> undef305, rest remain the same}> undef112, x^0 -> undef321, y^0 -> undef323, rest remain the same}> 1, x^0 -> undef232, y^0 -> undef234, rest remain the same}> undef250, y^0 -> undef252, rest remain the same}> undef268, y^0 -> undef270, rest remain the same}> 1, x^0 -> undef285, y^0 -> undef287, rest remain the same}> undef303, y^0 -> undef305, rest remain the same}> undef321, y^0 -> undef323, rest remain the same}> 1, x^0 -> undef232, y^0 -> undef234, rest remain the same}> undef250, y^0 -> undef252, rest remain the same}> undef268, y^0 -> undef270, rest remain the same}> 1, x^0 -> undef285, y^0 -> undef287, rest remain the same}> undef303, y^0 -> undef305, rest remain the same}> undef321, y^0 -> undef323, rest remain the same}> 1, x^0 -> undef232, y^0 -> undef234, rest remain the same}> 0, x^0 -> undef250, y^0 -> undef252, rest remain the same}> 0, x^0 -> undef268, y^0 -> undef270, rest remain the same}> 1, x^0 -> undef285, y^0 -> undef287, rest remain the same}> 0, x^0 -> undef303, y^0 -> undef305, rest remain the same}> 0, x^0 -> undef321, y^0 -> undef323, rest remain the same}> 1, x^0 -> undef502, y^0 -> undef504, rest remain the same}> undef520, y^0 -> undef522, rest remain the same}> undef538, y^0 -> undef540, rest remain the same}> Map Locations to Subgraph: ( 0 , 0 ) ( 1 , 2 ) ( 3 , 1 ) ( 5 , 1 ) ******************************************************************************************* ******************************** CHECKING ASSERTIONS ******************************** ******************************************************************************************* Proving termination of subgraph 0 Proving termination of subgraph 1 Checking unfeasibility... Time used: 0.130695 Checking conditional termination of SCC {l3, l5}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.094682s Ranking function: -71 + (~(33) / 2)*__const_7^0 + 3*n0^0 + (131 / 2)*n1^0 - 3*x^0 + (~(131) / 2)*y^0 New Graphs: Transitions: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> undef357, y^0 -> undef359, rest remain the same}> undef375, y^0 -> undef377, rest remain the same}> undef357, y^0 -> undef359, rest remain the same}> undef375, y^0 -> undef377, rest remain the same}> undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l3, l5}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.033820s Ranking function: (~(301) / 4) + (~(5) / 4)*__const_7^0 + (5 / 4)*__const_8^0 + 3*n0^0 + 34*n1^0 - 3*x^0 - 34*y^0 New Graphs: Transitions: 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef328, x^0 -> undef412, y^0 -> undef414, rest remain the same}> undef328, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef328, x^0 -> undef412, y^0 -> undef414, rest remain the same}> undef328, x^0 -> undef430, y^0 -> undef432, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l3}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.503340s Ranking function: -202 - 3*__const_7^0 + 34*__const_8^0 + 8*n0^0 + 5*n1^0 - 8*x^0 - 5*y^0 New Graphs: Transitions: undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef328, x^0 -> undef412, y^0 -> undef414, rest remain the same}> undef328, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef328, x^0 -> undef412, y^0 -> undef414, rest remain the same}> undef328, x^0 -> undef430, y^0 -> undef432, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l3}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.204286s Ranking function: -238 + (~(82) / 3)*__const_7^0 + 63*__const_8^0 + 5*n1^0 - 5*y^0 New Graphs: Transitions: undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef328, x^0 -> undef412, y^0 -> undef414, rest remain the same}> undef328, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef328, x^0 -> undef412, y^0 -> undef414, rest remain the same}> undef328, x^0 -> undef430, y^0 -> undef432, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l3}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.111426s Ranking function: -5 + 5*n1^0 - 5*y^0 New Graphs: Transitions: undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l3}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.036069s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.872805s Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.289618s Time used: 0.277949 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.307712s Time used: 0.303771 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.304449s Time used: 0.300391 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.293902s Time used: 0.289754 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.286152s Time used: 0.281877 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.277781s Time used: 0.273595 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.292013s Time used: 0.287818 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.355904s Time used: 0.351762 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.151758s Time used: 0.147653 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.143754s Time used: 0.139796 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.139206s Time used: 0.135308 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.118954s Time used: 0.115295 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.134955s Time used: 0.131385 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.140611s Time used: 0.137051 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.101362s Time used: 0.097801 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.146739s Time used: 0.143315 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.676665s Time used: 0.66982 Improving Solution with cost 3 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.004007s Time used: 1.00399 LOG: SAT solveNonLinear - Elapsed time: 1.680672s Cost: 3; Total time: 1.67381 Failed at location 5: 1 + n0^0 <= 0 Failed at location 5: 1 + n0^0 <= 0 Failed at location 5: 1 + n0^0 <= 0 Before Improving: Quasi-invariant at l3: 1 + n0^0 <= 0 Quasi-invariant at l5: 1 + n0^0 <= 0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.166277s Remaining time after improvement: 0.862633 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l3: 1 + n0^0 <= 0 Quasi-invariant at l5: 1 + n0^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: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef112, x^0 -> undef357, y^0 -> undef359, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef112, x^0 -> undef375, y^0 -> undef377, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef357, y^0 -> undef359, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef375, y^0 -> undef377, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef357, y^0 -> undef359, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef375, y^0 -> undef377, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef430, y^0 -> undef432, 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: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> New Graphs: Calling Safety with literal 1 + n0^0 <= 0 and entry 1, x^0 -> undef574, y^0 -> undef576, rest remain the same}> LOG: CALL check - Post:1 + n0^0 <= 0 - Process 1 * Exit transition: 1, x^0 -> undef574, y^0 -> undef576, rest remain the same}> * Postcondition : 1 + n0^0 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004166s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.004251s Calling Safety with literal 1 + n0^0 <= 0 and entry 0, x^0 -> undef592, y^0 -> undef594, rest remain the same}> LOG: CALL check - Post:1 + n0^0 <= 0 - Process 2 * Exit transition: 0, x^0 -> undef592, y^0 -> undef594, rest remain the same}> * Postcondition : 1 + n0^0 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004190s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.004271s Calling Safety with literal 1 + n0^0 <= 0 and entry 0, x^0 -> undef610, y^0 -> undef612, rest remain the same}> LOG: CALL check - Post:1 + n0^0 <= 0 - Process 3 * Exit transition: 0, x^0 -> undef610, y^0 -> undef612, rest remain the same}> * Postcondition : 1 + n0^0 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004181s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.004270s INVARIANTS: 3: 5: Quasi-INVARIANTS to narrow Graph: 3: 1 + n0^0 <= 0 , 5: 1 + n0^0 <= 0 , Narrowing transition: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef112, x^0 -> undef357, y^0 -> undef359, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef112, x^0 -> undef375, y^0 -> undef377, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef357, y^0 -> undef359, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef375, y^0 -> undef377, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef357, y^0 -> undef359, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef375, y^0 -> undef377, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> undef112, x^0 -> undef357, y^0 -> undef359, rest remain the same}> undef112, x^0 -> undef375, y^0 -> undef377, rest remain the same}> undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> undef357, y^0 -> undef359, rest remain the same}> undef375, y^0 -> undef377, rest remain the same}> undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> undef357, y^0 -> undef359, rest remain the same}> undef375, y^0 -> undef377, rest remain the same}> undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l3, l5}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.087702s Ranking function: -64 - 11*__const_7^0 + 51*n0^0 + 3*n1^0 - 51*x^0 - 3*y^0 New Graphs: Transitions: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> undef357, y^0 -> undef359, rest remain the same}> undef375, y^0 -> undef377, rest remain the same}> undef357, y^0 -> undef359, rest remain the same}> undef375, y^0 -> undef377, rest remain the same}> undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l3, l5}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.046494s Ranking function: -75 - __const_7^0 + __const_8^0 + 34*n0^0 + 3*n1^0 - 34*x^0 - 3*y^0 New Graphs: Transitions: 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef328, x^0 -> undef412, y^0 -> undef414, rest remain the same}> undef328, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef328, x^0 -> undef412, y^0 -> undef414, rest remain the same}> undef328, x^0 -> undef430, y^0 -> undef432, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l3}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.515178s Ranking function: -202 - 3*__const_7^0 + 34*__const_8^0 + 8*n0^0 + 5*n1^0 - 8*x^0 - 5*y^0 New Graphs: Transitions: undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef328, x^0 -> undef412, y^0 -> undef414, rest remain the same}> undef328, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef328, x^0 -> undef412, y^0 -> undef414, rest remain the same}> undef328, x^0 -> undef430, y^0 -> undef432, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l3}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.213064s Ranking function: -238 + (~(82) / 3)*__const_7^0 + 63*__const_8^0 + 5*n1^0 - 5*y^0 New Graphs: Transitions: undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef328, x^0 -> undef412, y^0 -> undef414, rest remain the same}> undef328, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef328, x^0 -> undef412, y^0 -> undef414, rest remain the same}> undef328, x^0 -> undef430, y^0 -> undef432, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l3}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.115435s Ranking function: -5 + 5*n1^0 - 5*y^0 New Graphs: Transitions: undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l3}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.038284s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.879416s Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.292026s Time used: 0.280446 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.311452s Time used: 0.307401 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.305649s Time used: 0.301604 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.293510s Time used: 0.289311 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.289195s Time used: 0.284997 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.279950s Time used: 0.275743 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.294585s Time used: 0.290353 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.357972s Time used: 0.353769 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.154850s Time used: 0.150635 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.146067s Time used: 0.142001 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.148348s Time used: 0.144488 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.121981s Time used: 0.118241 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.137343s Time used: 0.133661 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.143250s Time used: 0.139622 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.103439s Time used: 0.099809 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.149010s Time used: 0.145533 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.917099s Time used: 0.909168 Improving Solution with cost 3 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.004030s Time used: 1.00401 LOG: SAT solveNonLinear - Elapsed time: 1.921130s Cost: 3; Total time: 1.91318 Failed at location 5: __const_8^0 + n0^0 + n1^0 <= 1 + y^0 Failed at location 5: __const_8^0 + n0^0 + n1^0 <= 1 + y^0 Failed at location 5: __const_8^0 + n0^0 + n1^0 <= 1 + y^0 Before Improving: Quasi-invariant at l3: n1^0 <= y^0 Quasi-invariant at l5: __const_8^0 + n0^0 + n1^0 <= 1 + y^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.171997s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.159062s Remaining time after improvement: 0.719485 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l3: n1^0 <= y^0 Quasi-invariant at l5: __const_8^0 + n0^0 + n1^0 <= 2 + y^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: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef112, x^0 -> undef357, y^0 -> undef359, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef112, x^0 -> undef375, y^0 -> undef377, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef357, y^0 -> undef359, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef375, y^0 -> undef377, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef357, y^0 -> undef359, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef375, y^0 -> undef377, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef430, y^0 -> undef432, 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: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> New Graphs: Calling Safety with literal __const_8^0 + n0^0 + n1^0 <= 2 + y^0 and entry 1, x^0 -> undef574, y^0 -> undef576, rest remain the same}> LOG: CALL check - Post:__const_8^0 + n0^0 + n1^0 <= 2 + y^0 - Process 4 * Exit transition: 1, x^0 -> undef574, y^0 -> undef576, rest remain the same}> * Postcondition : __const_8^0 + n0^0 + n1^0 <= 2 + y^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004674s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.004779s Calling Safety with literal __const_8^0 + n0^0 + n1^0 <= 2 + y^0 and entry 0, x^0 -> undef592, y^0 -> undef594, rest remain the same}> LOG: CALL check - Post:__const_8^0 + n0^0 + n1^0 <= 2 + y^0 - Process 5 * Exit transition: 0, x^0 -> undef592, y^0 -> undef594, rest remain the same}> * Postcondition : __const_8^0 + n0^0 + n1^0 <= 2 + y^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004504s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.004603s Calling Safety with literal __const_8^0 + n0^0 + n1^0 <= 2 + y^0 and entry 0, x^0 -> undef610, y^0 -> undef612, rest remain the same}> LOG: CALL check - Post:__const_8^0 + n0^0 + n1^0 <= 2 + y^0 - Process 6 * Exit transition: 0, x^0 -> undef610, y^0 -> undef612, rest remain the same}> * Postcondition : __const_8^0 + n0^0 + n1^0 <= 2 + y^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004573s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.004674s INVARIANTS: 3: 5: Quasi-INVARIANTS to narrow Graph: 3: n1^0 <= y^0 , 5: __const_8^0 + n0^0 + n1^0 <= 2 + y^0 , Narrowing transition: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef112, x^0 -> undef357, y^0 -> undef359, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef112, x^0 -> undef375, y^0 -> undef377, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef357, y^0 -> undef359, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef375, y^0 -> undef377, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef357, y^0 -> undef359, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef375, y^0 -> undef377, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> undef112, x^0 -> undef357, y^0 -> undef359, rest remain the same}> undef112, x^0 -> undef375, y^0 -> undef377, rest remain the same}> undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> undef357, y^0 -> undef359, rest remain the same}> undef375, y^0 -> undef377, rest remain the same}> undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> undef357, y^0 -> undef359, rest remain the same}> undef375, y^0 -> undef377, rest remain the same}> undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l3, l5}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.119800s Ranking function: -60 - 11*__const_7^0 + 50*n0^0 + 2*n1^0 - 50*x^0 - 2*y^0 New Graphs: Transitions: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> undef357, y^0 -> undef359, rest remain the same}> undef375, y^0 -> undef377, rest remain the same}> undef357, y^0 -> undef359, rest remain the same}> undef375, y^0 -> undef377, rest remain the same}> undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l3, l5}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.069551s Ranking function: -265 - 3*__const_7^0 + 45*__const_8^0 + 3*n0^0 + 2*n1^0 - 3*x^0 - 2*y^0 New Graphs: Transitions: 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef328, x^0 -> undef412, y^0 -> undef414, rest remain the same}> undef328, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef328, x^0 -> undef412, y^0 -> undef414, rest remain the same}> undef328, x^0 -> undef430, y^0 -> undef432, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l3}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 1.230651s Ranking function: -223 - 4*__const_7^0 + (75 / 2)*__const_8^0 + 5*n0^0 + 13*n1^0 - 5*x^0 - 13*y^0 New Graphs: Transitions: undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef328, x^0 -> undef412, y^0 -> undef414, rest remain the same}> undef328, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef328, x^0 -> undef412, y^0 -> undef414, rest remain the same}> undef328, x^0 -> undef430, y^0 -> undef432, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l3}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.402442s Ranking function: -254 - 27*__const_7^0 + 66*__const_8^0 + 5*n0^0 - 5*x^0 New Graphs: Transitions: undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef328, x^0 -> undef412, y^0 -> undef414, rest remain the same}> undef328, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef328, x^0 -> undef412, y^0 -> undef414, rest remain the same}> undef328, x^0 -> undef430, y^0 -> undef432, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l3}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.133945s Ranking function: -1 + (1 / 3)*__const_8^0 + (1 / 3)*n0^0 + (1 / 3)*n1^0 + (~(1) / 3)*y^0 New Graphs: Transitions: undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l3}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.041466s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 1.164193s Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.308987s Time used: 0.297033 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.309303s Time used: 0.305011 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.306049s Time used: 0.301744 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.318805s Time used: 0.314491 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.319667s Time used: 0.315386 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.398020s Time used: 0.393685 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.310337s Time used: 0.305993 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.320594s Time used: 0.316187 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.187350s Time used: 0.183092 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.169727s Time used: 0.165629 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.148867s Time used: 0.144571 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.185110s Time used: 0.181166 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.153492s Time used: 0.149706 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.174541s Time used: 0.170866 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.174233s Time used: 0.170576 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.127852s Time used: 0.124222 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.334921s Time used: 1.32672 Improving Solution with cost 3 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.003339s Time used: 1.00332 LOG: SAT solveNonLinear - Elapsed time: 2.338260s Cost: 3; Total time: 2.33004 Failed at location 5: 1 + __const_8^0 + n0^0 <= __const_7^0 Failed at location 5: 1 + __const_8^0 + n0^0 <= __const_7^0 Failed at location 5: 1 + __const_8^0 + n0^0 <= __const_7^0 Before Improving: Quasi-invariant at l3: 1 + __const_8^0 + n0^0 <= __const_7^0 Quasi-invariant at l5: 1 + __const_8^0 + n0^0 <= __const_7^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.218239s Remaining time after improvement: 0.807461 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l3: 1 + __const_8^0 + n0^0 <= __const_7^0 Quasi-invariant at l5: 1 + __const_8^0 + n0^0 <= __const_7^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: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef112, x^0 -> undef357, y^0 -> undef359, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef112, x^0 -> undef375, y^0 -> undef377, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef357, y^0 -> undef359, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef375, y^0 -> undef377, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef357, y^0 -> undef359, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef375, y^0 -> undef377, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef430, y^0 -> undef432, rest remain the same}> [ Termination Graph ] Strengthening and disabling transitions... > It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> New Graphs: Calling Safety with literal 1 + __const_8^0 + n0^0 <= __const_7^0 and entry 1, x^0 -> undef574, y^0 -> undef576, rest remain the same}> LOG: CALL check - Post:1 + __const_8^0 + n0^0 <= __const_7^0 - Process 7 * Exit transition: 1, x^0 -> undef574, y^0 -> undef576, rest remain the same}> * Postcondition : 1 + __const_8^0 + n0^0 <= __const_7^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.006115s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.006214s Calling Safety with literal 1 + __const_8^0 + n0^0 <= __const_7^0 and entry 0, x^0 -> undef592, y^0 -> undef594, rest remain the same}> LOG: CALL check - Post:1 + __const_8^0 + n0^0 <= __const_7^0 - Process 8 * Exit transition: 0, x^0 -> undef592, y^0 -> undef594, rest remain the same}> * Postcondition : 1 + __const_8^0 + n0^0 <= __const_7^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.006162s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.006263s Calling Safety with literal 1 + __const_8^0 + n0^0 <= __const_7^0 and entry 0, x^0 -> undef610, y^0 -> undef612, rest remain the same}> LOG: CALL check - Post:1 + __const_8^0 + n0^0 <= __const_7^0 - Process 9 * Exit transition: 0, x^0 -> undef610, y^0 -> undef612, rest remain the same}> * Postcondition : 1 + __const_8^0 + n0^0 <= __const_7^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.006166s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.006274s INVARIANTS: 3: 5: Quasi-INVARIANTS to narrow Graph: 3: 1 + __const_8^0 + n0^0 <= __const_7^0 , 5: 1 + __const_8^0 + n0^0 <= __const_7^0 , Narrowing transition: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef112, x^0 -> undef357, y^0 -> undef359, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef112, x^0 -> undef375, y^0 -> undef377, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef357, y^0 -> undef359, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef375, y^0 -> undef377, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef357, y^0 -> undef359, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef375, y^0 -> undef377, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> undef112, x^0 -> undef357, y^0 -> undef359, rest remain the same}> undef112, x^0 -> undef375, y^0 -> undef377, rest remain the same}> undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> undef357, y^0 -> undef359, rest remain the same}> undef375, y^0 -> undef377, rest remain the same}> undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> undef357, y^0 -> undef359, rest remain the same}> undef375, y^0 -> undef377, rest remain the same}> undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l3, l5}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.187320s Ranking function: -19 - 11*__const_7^0 + 4*n0^0 + 17*n1^0 - 4*x^0 - 17*y^0 New Graphs: Transitions: undef112, x^0 -> undef357, y^0 -> undef359, rest remain the same}> undef112, x^0 -> undef375, y^0 -> undef377, rest remain the same}> undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> undef357, y^0 -> undef359, rest remain the same}> undef375, y^0 -> undef377, rest remain the same}> undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> undef357, y^0 -> undef359, rest remain the same}> undef375, y^0 -> undef377, rest remain the same}> undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l3, l5}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.218665s Ranking function: 10 - 24*__const_7^0 + 10*__const_8^0 + 16*n0^0 + 2*n1^0 - 16*x^0 - 2*y^0 New Graphs: Transitions: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> undef357, y^0 -> undef359, rest remain the same}> undef375, y^0 -> undef377, rest remain the same}> undef357, y^0 -> undef359, rest remain the same}> undef375, y^0 -> undef377, rest remain the same}> undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l3, l5}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.094360s Ranking function: -45 + (~(39) / 4)*__const_7^0 + (39 / 4)*__const_8^0 + 3*n0^0 + (117 / 8)*n1^0 - 3*x^0 + (~(117) / 8)*y^0 New Graphs: Transitions: 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef328, x^0 -> undef412, y^0 -> undef414, rest remain the same}> undef328, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef328, x^0 -> undef412, y^0 -> undef414, rest remain the same}> undef328, x^0 -> undef430, y^0 -> undef432, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l3}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 2.022509s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 2.040864s Trying to remove transition: undef328, x^0 -> undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.965892s Time used: 0.924394 LOG: SAT solveNonLinear - Elapsed time: 0.965892s Cost: 0; Total time: 0.924394 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l3: 0 <= __const_8^0 Ranking function: n1^0 - y^0 Ranking function and negation of Quasi-Invariant applied New Graphs: Transitions: undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l3}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.052503s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 1.905263s Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.429782s Time used: 0.414946 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.358842s Time used: 0.353944 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.444386s Time used: 0.439506 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.351864s Time used: 0.346956 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.339396s Time used: 0.334605 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.343983s Time used: 0.339159 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.333270s Time used: 0.328525 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.327168s Time used: 0.32238 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.178806s Time used: 0.174006 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.187517s Time used: 0.182884 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.177187s Time used: 0.17286 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.173047s Time used: 0.168875 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.175358s Time used: 0.171224 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.219152s Time used: 0.215155 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.179542s Time used: 0.175708 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.172888s Time used: 0.169116 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.590081s Time used: 1.58145 Improving Solution with cost 3 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.005601s Time used: 1.00558 LOG: SAT solveNonLinear - Elapsed time: 2.595682s Cost: 3; Total time: 2.58703 Failed at location 5: 1 + __const_7^0 <= 0 Failed at location 5: 1 + __const_7^0 <= 0 Failed at location 5: 1 + __const_7^0 <= 0 Before Improving: Quasi-invariant at l3: 1 + __const_7^0 <= 0 Quasi-invariant at l5: 1 + __const_7^0 <= 0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.202069s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.197023s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.199804s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.213525s Remaining time after improvement: 0.258501 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l3: __const_7^0 <= 4 Quasi-invariant at l5: __const_7^0 <= 4 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef112, x^0 -> undef357, y^0 -> undef359, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef112, x^0 -> undef375, y^0 -> undef377, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef357, y^0 -> undef359, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef375, y^0 -> undef377, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef357, y^0 -> undef359, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef375, y^0 -> undef377, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef430, y^0 -> undef432, 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: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef430, y^0 -> undef432, rest remain the same}> New Graphs: Transitions: undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l3}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.039663s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.465790s Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.187837s Time used: 0.18254 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.175130s Time used: 0.172486 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.190226s Time used: 0.187559 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.182272s Time used: 0.179632 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.174702s Time used: 0.172157 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.181637s Time used: 0.179126 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.171774s Time used: 0.169323 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.182484s Time used: 0.180107 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.742015s Time used: 0.737259 Improving Solution with cost 3 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.008262s Time used: 1.00824 LOG: SAT solveNonLinear - Elapsed time: 1.750277s Cost: 3; Total time: 1.7455 Failed at location 5: __const_7^0 <= 0 Failed at location 5: __const_7^0 <= 0 Failed at location 5: __const_7^0 <= 0 Before Improving: Quasi-invariant at l3: __const_7^0 <= 0 Quasi-invariant at l5: __const_7^0 <= 0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.093711s Remaining time after improvement: 0.915701 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l3: __const_7^0 <= 0 Quasi-invariant at l5: __const_7^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: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef112, x^0 -> undef357, y^0 -> undef359, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef112, x^0 -> undef375, y^0 -> undef377, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef357, y^0 -> undef359, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef375, y^0 -> undef377, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef430, y^0 -> undef432, 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: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> New Graphs: Calling Safety with literal __const_7^0 <= 4 and entry 1, x^0 -> undef574, y^0 -> undef576, rest remain the same}> LOG: CALL check - Post:__const_7^0 <= 4 - Process 10 * Exit transition: 1, x^0 -> undef574, y^0 -> undef576, rest remain the same}> * Postcondition : __const_7^0 <= 4 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.013779s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.013879s Calling Safety with literal __const_7^0 <= 4 and entry 0, x^0 -> undef592, y^0 -> undef594, rest remain the same}> LOG: CALL check - Post:__const_7^0 <= 4 - Process 11 * Exit transition: 0, x^0 -> undef592, y^0 -> undef594, rest remain the same}> * Postcondition : __const_7^0 <= 4 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.013930s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.014030s Calling Safety with literal __const_7^0 <= 4 and entry 0, x^0 -> undef610, y^0 -> undef612, rest remain the same}> LOG: CALL check - Post:__const_7^0 <= 4 - Process 12 * Exit transition: 0, x^0 -> undef610, y^0 -> undef612, rest remain the same}> * Postcondition : __const_7^0 <= 4 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.013974s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.014082s INVARIANTS: 3: 5: Quasi-INVARIANTS to narrow Graph: 3: __const_7^0 <= 4 , 5: __const_7^0 <= 4 , INVARIANTS: 3: 5: Quasi-INVARIANTS to narrow Graph: 3: __const_7^0 <= 0 , 5: __const_7^0 <= 0 , Narrowing transition: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: undef112, x^0 -> undef357, y^0 -> undef359, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: undef112, x^0 -> undef375, y^0 -> undef377, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: undef357, y^0 -> undef359, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: undef375, y^0 -> undef377, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: undef357, y^0 -> undef359, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: undef375, y^0 -> undef377, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: Narrow transition size 2 invGraph after Narrowing: Transitions: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> undef112, x^0 -> undef357, y^0 -> undef359, rest remain the same}> undef112, x^0 -> undef375, y^0 -> undef377, rest remain the same}> undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> undef357, y^0 -> undef359, rest remain the same}> undef375, y^0 -> undef377, rest remain the same}> undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> undef357, y^0 -> undef359, rest remain the same}> undef375, y^0 -> undef377, rest remain the same}> undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l3, l5}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.310126s Ranking function: (~(27) / 2) - 12*__const_7^0 + 5*n0^0 + (31 / 2)*n1^0 - 5*x^0 + (~(31) / 2)*y^0 New Graphs: Transitions: undef112, x^0 -> undef357, y^0 -> undef359, rest remain the same}> undef112, x^0 -> undef375, y^0 -> undef377, rest remain the same}> undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> undef357, y^0 -> undef359, rest remain the same}> undef375, y^0 -> undef377, rest remain the same}> undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> undef357, y^0 -> undef359, rest remain the same}> undef375, y^0 -> undef377, rest remain the same}> undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l3, l5}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.162552s Ranking function: 1 + (~(73) / 3)*__const_7^0 + (37 / 3)*__const_8^0 + (49 / 3)*n0^0 + 2*n1^0 + (~(49) / 3)*x^0 - 2*y^0 New Graphs: Transitions: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> undef357, y^0 -> undef359, rest remain the same}> undef375, y^0 -> undef377, rest remain the same}> undef357, y^0 -> undef359, rest remain the same}> undef375, y^0 -> undef377, rest remain the same}> undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l3, l5}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.073703s Ranking function: (~(17) / 4) + (1 / 4)*__const_7^0 + 3*n0^0 - 3*x^0 New Graphs: Transitions: 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l3}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 2.046168s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 2.040976s Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.107861s Time used: 1.0759 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.219299s Time used: 1.20686 Trying to remove transition: 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.850096s Time used: 0.837406 LOG: SAT solveNonLinear - Elapsed time: 0.850096s Cost: 0; Total time: 0.837406 Ranking function: n1^0 - y^0 Ranking function and negation of Quasi-Invariant applied New Graphs: Transitions: undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l3}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.057337s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 1.363972s Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.379494s Time used: 0.364188 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.418308s Time used: 0.413559 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.430493s Time used: 0.425773 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.425156s Time used: 0.420449 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.371584s Time used: 0.366877 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.346478s Time used: 0.34184 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.353703s Time used: 0.349004 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.384633s Time used: 0.380021 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.221350s Time used: 0.216785 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.224827s Time used: 0.220577 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.234989s Time used: 0.230849 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.197841s Time used: 0.193807 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.210065s Time used: 0.206063 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.216832s Time used: 0.213097 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.194334s Time used: 0.190643 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.207639s Time used: 0.204074 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 2.163395s Time used: 2.15572 Improving Solution with cost 3 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.006753s Time used: 1.00673 LOG: SAT solveNonLinear - Elapsed time: 3.170148s Cost: 3; Total time: 3.16245 Failed at location 5: __const_7^0 + n0^0 <= x^0 Failed at location 5: __const_7^0 + n0^0 <= x^0 Failed at location 5: __const_7^0 + n0^0 <= x^0 Before Improving: Quasi-invariant at l3: __const_7^0 + n0^0 <= x^0 Quasi-invariant at l5: __const_7^0 + n0^0 <= x^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.184033s Remaining time after improvement: 0.851323 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l3: __const_7^0 + n0^0 <= x^0 Quasi-invariant at l5: __const_7^0 + n0^0 <= x^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: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef112, x^0 -> undef357, y^0 -> undef359, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef112, x^0 -> undef375, y^0 -> undef377, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef357, y^0 -> undef359, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef375, y^0 -> undef377, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef357, y^0 -> undef359, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef375, y^0 -> undef377, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef430, y^0 -> undef432, 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: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> New Graphs: Calling Safety with literal __const_7^0 + n0^0 <= x^0 and entry 1, x^0 -> undef574, y^0 -> undef576, rest remain the same}> LOG: CALL check - Post:__const_7^0 + n0^0 <= x^0 - Process 13 * Exit transition: 1, x^0 -> undef574, y^0 -> undef576, rest remain the same}> * Postcondition : __const_7^0 + n0^0 <= x^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.015863s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.015986s Calling Safety with literal __const_7^0 + n0^0 <= x^0 and entry 0, x^0 -> undef592, y^0 -> undef594, rest remain the same}> LOG: CALL check - Post:__const_7^0 + n0^0 <= x^0 - Process 14 * Exit transition: 0, x^0 -> undef592, y^0 -> undef594, rest remain the same}> * Postcondition : __const_7^0 + n0^0 <= x^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.016224s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.016342s Calling Safety with literal __const_7^0 + n0^0 <= x^0 and entry 0, x^0 -> undef610, y^0 -> undef612, rest remain the same}> LOG: CALL check - Post:__const_7^0 + n0^0 <= x^0 - Process 15 * Exit transition: 0, x^0 -> undef610, y^0 -> undef612, rest remain the same}> * Postcondition : __const_7^0 + n0^0 <= x^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.016055s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.016180s INVARIANTS: 3: 5: Quasi-INVARIANTS to narrow Graph: 3: __const_7^0 + n0^0 <= x^0 , 5: __const_7^0 + n0^0 <= x^0 , Narrowing transition: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef112, x^0 -> undef357, y^0 -> undef359, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef112, x^0 -> undef375, y^0 -> undef377, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef357, y^0 -> undef359, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef375, y^0 -> undef377, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef357, y^0 -> undef359, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef375, y^0 -> undef377, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> undef112, x^0 -> undef357, y^0 -> undef359, rest remain the same}> undef112, x^0 -> undef375, y^0 -> undef377, rest remain the same}> undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> undef357, y^0 -> undef359, rest remain the same}> undef375, y^0 -> undef377, rest remain the same}> undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> undef357, y^0 -> undef359, rest remain the same}> undef375, y^0 -> undef377, rest remain the same}> undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l3, l5}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.494540s Ranking function: 11 + (~(79) / 2)*__const_7^0 + 2*n0^0 + 47*n1^0 - 2*x^0 - 47*y^0 New Graphs: Transitions: undef112, x^0 -> undef357, y^0 -> undef359, rest remain the same}> undef112, x^0 -> undef375, y^0 -> undef377, rest remain the same}> undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> undef357, y^0 -> undef359, rest remain the same}> undef375, y^0 -> undef377, rest remain the same}> undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> undef357, y^0 -> undef359, rest remain the same}> undef375, y^0 -> undef377, rest remain the same}> undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l3, l5}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.356837s Ranking function: -40 - 13*__const_7^0 + 4*n0^0 + 42*n1^0 - 4*x^0 - 42*y^0 New Graphs: Transitions: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> undef357, y^0 -> undef359, rest remain the same}> undef375, y^0 -> undef377, rest remain the same}> undef357, y^0 -> undef359, rest remain the same}> undef375, y^0 -> undef377, rest remain the same}> undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l3, l5}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.097043s Ranking function: (~(215) / 26) + (119 / 26)*__const_7^0 + (9 / 13)*__const_8^0 + (61 / 13)*n0^0 + (~(61) / 13)*x^0 New Graphs: Transitions: 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l3}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 2.094430s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 2.109818s Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.193464s Time used: 1.16008 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.153509s Time used: 1.14078 Trying to remove transition: 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.792719s Time used: 0.779668 LOG: SAT solveNonLinear - Elapsed time: 0.792719s Cost: 0; Total time: 0.779668 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l3: __const_7^0 <= executed_Drive^0 + n0^0 + n1^0 Ranking function: n0^0 - x^0 Ranking function and negation of Quasi-Invariant applied New Graphs: Transitions: 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l3}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 1.129405s Ranking function: (~(413) / 4) + (47 / 4)*__const_8^0 - executed_Drive^0 + (87 / 4)*n0^0 + 12*n1^0 - 3*x^0 - 12*y^0 New Graphs: Transitions: undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l3}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.061992s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 1.872925s Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.433726s Time used: 0.41776 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.469449s Time used: 0.464346 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.433937s Time used: 0.428989 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.431409s Time used: 0.4264 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.430594s Time used: 0.425591 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.405952s Time used: 0.400938 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.433069s Time used: 0.428243 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.451025s Time used: 0.446175 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.203858s Time used: 0.199179 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.217363s Time used: 0.212929 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.226881s Time used: 0.222708 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.213345s Time used: 0.209334 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.225738s Time used: 0.221939 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.229655s Time used: 0.226017 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.230368s Time used: 0.226872 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.209607s Time used: 0.206112 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 2.085796s Time used: 2.07787 Improving Solution with cost 3 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.007998s Time used: 1.00798 LOG: SAT solveNonLinear - Elapsed time: 3.093793s Cost: 3; Total time: 3.08585 Failed at location 5: 1 + __const_8^0 + n0^0 + n1^0 <= __const_7^0 Failed at location 5: 1 + __const_8^0 + n0^0 + n1^0 <= __const_7^0 Failed at location 5: 1 + __const_8^0 + n0^0 + n1^0 <= __const_7^0 Before Improving: Quasi-invariant at l3: 1 + __const_8^0 + n0^0 + n1^0 <= __const_7^0 Quasi-invariant at l5: 1 + __const_8^0 + n0^0 + n1^0 <= __const_7^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.191375s Remaining time after improvement: 0.835236 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l3: 1 + __const_8^0 + n0^0 + n1^0 <= __const_7^0 Quasi-invariant at l5: 1 + __const_8^0 + n0^0 + n1^0 <= __const_7^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: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef112, x^0 -> undef357, y^0 -> undef359, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef112, x^0 -> undef375, y^0 -> undef377, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef357, y^0 -> undef359, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef375, y^0 -> undef377, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef357, y^0 -> undef359, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef375, y^0 -> undef377, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef430, y^0 -> undef432, 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: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> New Graphs: Calling Safety with literal 1 + __const_8^0 + n0^0 + n1^0 <= __const_7^0 and entry 1, x^0 -> undef574, y^0 -> undef576, rest remain the same}> LOG: CALL check - Post:1 + __const_8^0 + n0^0 + n1^0 <= __const_7^0 - Process 16 * Exit transition: 1, x^0 -> undef574, y^0 -> undef576, rest remain the same}> * Postcondition : 1 + __const_8^0 + n0^0 + n1^0 <= __const_7^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.018626s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.018749s Calling Safety with literal 1 + __const_8^0 + n0^0 + n1^0 <= __const_7^0 and entry 0, x^0 -> undef592, y^0 -> undef594, rest remain the same}> LOG: CALL check - Post:1 + __const_8^0 + n0^0 + n1^0 <= __const_7^0 - Process 17 * Exit transition: 0, x^0 -> undef592, y^0 -> undef594, rest remain the same}> * Postcondition : 1 + __const_8^0 + n0^0 + n1^0 <= __const_7^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.018783s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.018904s Calling Safety with literal 1 + __const_8^0 + n0^0 + n1^0 <= __const_7^0 and entry 0, x^0 -> undef610, y^0 -> undef612, rest remain the same}> LOG: CALL check - Post:1 + __const_8^0 + n0^0 + n1^0 <= __const_7^0 - Process 18 * Exit transition: 0, x^0 -> undef610, y^0 -> undef612, rest remain the same}> * Postcondition : 1 + __const_8^0 + n0^0 + n1^0 <= __const_7^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.018942s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.019065s INVARIANTS: 3: 5: Quasi-INVARIANTS to narrow Graph: 3: 1 + __const_8^0 + n0^0 + n1^0 <= __const_7^0 , 5: 1 + __const_8^0 + n0^0 + n1^0 <= __const_7^0 , Narrowing transition: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef112, x^0 -> undef357, y^0 -> undef359, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef112, x^0 -> undef375, y^0 -> undef377, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef357, y^0 -> undef359, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef375, y^0 -> undef377, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef357, y^0 -> undef359, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef375, y^0 -> undef377, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> undef112, x^0 -> undef357, y^0 -> undef359, rest remain the same}> undef112, x^0 -> undef375, y^0 -> undef377, rest remain the same}> undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> undef357, y^0 -> undef359, rest remain the same}> undef375, y^0 -> undef377, rest remain the same}> undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> undef357, y^0 -> undef359, rest remain the same}> undef375, y^0 -> undef377, rest remain the same}> undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l3, l5}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.133539s Ranking function: -2 + 2*__const_7^0 + n0^0 - x^0 New Graphs: Transitions: undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l3}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.063769s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 2.021166s Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.478506s Time used: 0.464038 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.462247s Time used: 0.457427 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.468036s Time used: 0.463231 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.424986s Time used: 0.420201 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.484747s Time used: 0.479996 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.478188s Time used: 0.473427 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.426257s Time used: 0.421545 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.463118s Time used: 0.458463 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.216504s Time used: 0.21195 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.217270s Time used: 0.212938 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.234712s Time used: 0.230551 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.236461s Time used: 0.232405 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.234168s Time used: 0.230216 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.219689s Time used: 0.215852 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.238707s Time used: 0.234909 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.226522s Time used: 0.222932 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 2.136964s Time used: 2.12753 Improving Solution with cost 3 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.009408s Time used: 1.00828 LOG: SAT solveNonLinear - Elapsed time: 3.146372s Cost: 3; Total time: 3.13581 Failed at location 5: __const_8^0 + n0^0 <= 1 + __const_7^0 Failed at location 5: __const_8^0 + n0^0 <= 1 + __const_7^0 Failed at location 5: __const_8^0 + n0^0 <= 1 + __const_7^0 Before Improving: Quasi-invariant at l3: __const_8^0 + n0^0 <= 1 + __const_7^0 Quasi-invariant at l5: __const_8^0 + n0^0 <= 1 + __const_7^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.177941s Remaining time after improvement: 0.848189 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l3: __const_8^0 + n0^0 <= 1 + __const_7^0 Quasi-invariant at l5: __const_8^0 + n0^0 <= 1 + __const_7^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: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef112, x^0 -> undef357, y^0 -> undef359, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef112, x^0 -> undef375, y^0 -> undef377, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef357, y^0 -> undef359, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef375, y^0 -> undef377, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef357, y^0 -> undef359, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef375, y^0 -> undef377, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef430, y^0 -> undef432, rest remain the same}> [ Termination Graph ] Strengthening and disabling transitions... > It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> New Graphs: Calling Safety with literal __const_8^0 + n0^0 <= 1 + __const_7^0 and entry 1, x^0 -> undef574, y^0 -> undef576, rest remain the same}> LOG: CALL check - Post:__const_8^0 + n0^0 <= 1 + __const_7^0 - Process 19 * Exit transition: 1, x^0 -> undef574, y^0 -> undef576, rest remain the same}> * Postcondition : __const_8^0 + n0^0 <= 1 + __const_7^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.019724s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.019848s Calling Safety with literal __const_8^0 + n0^0 <= 1 + __const_7^0 and entry 0, x^0 -> undef592, y^0 -> undef594, rest remain the same}> LOG: CALL check - Post:__const_8^0 + n0^0 <= 1 + __const_7^0 - Process 20 * Exit transition: 0, x^0 -> undef592, y^0 -> undef594, rest remain the same}> * Postcondition : __const_8^0 + n0^0 <= 1 + __const_7^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.020015s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.020143s Calling Safety with literal __const_8^0 + n0^0 <= 1 + __const_7^0 and entry 0, x^0 -> undef610, y^0 -> undef612, rest remain the same}> LOG: CALL check - Post:__const_8^0 + n0^0 <= 1 + __const_7^0 - Process 21 * Exit transition: 0, x^0 -> undef610, y^0 -> undef612, rest remain the same}> * Postcondition : __const_8^0 + n0^0 <= 1 + __const_7^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.020014s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.020144s INVARIANTS: 3: 5: Quasi-INVARIANTS to narrow Graph: 3: __const_8^0 + n0^0 <= 1 + __const_7^0 , 5: __const_8^0 + n0^0 <= 1 + __const_7^0 , Narrowing transition: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef112, x^0 -> undef357, y^0 -> undef359, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef112, x^0 -> undef375, y^0 -> undef377, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef357, y^0 -> undef359, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef375, y^0 -> undef377, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef357, y^0 -> undef359, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef375, y^0 -> undef377, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> undef112, x^0 -> undef357, y^0 -> undef359, rest remain the same}> undef112, x^0 -> undef375, y^0 -> undef377, rest remain the same}> undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> undef357, y^0 -> undef359, rest remain the same}> undef375, y^0 -> undef377, rest remain the same}> undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> undef357, y^0 -> undef359, rest remain the same}> undef375, y^0 -> undef377, rest remain the same}> undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l3, l5}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.680969s Ranking function: 9 - 25*__const_7^0 + 11*__const_8^0 + 14*n0^0 + 18*n1^0 - 2*x^0 - 18*y^0 New Graphs: Transitions: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> undef357, y^0 -> undef359, rest remain the same}> undef375, y^0 -> undef377, rest remain the same}> undef357, y^0 -> undef359, rest remain the same}> undef375, y^0 -> undef377, rest remain the same}> undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l3, l5}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.137086s Ranking function: -5 + 2*n0^0 + 5*n1^0 - 2*x^0 - 5*y^0 New Graphs: Transitions: 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l3}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 2.101903s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 2.079106s Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.281697s Time used: 1.2477 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.318296s Time used: 1.30522 Trying to remove transition: 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.865248s Time used: 0.852021 LOG: SAT solveNonLinear - Elapsed time: 0.865248s Cost: 0; Total time: 0.852021 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l3: __const_7^0 + executed_Drive^0 + x^0 <= __const_8^0 + n0^0 + n1^0 Ranking function: n0^0 - x^0 Ranking function and negation of Quasi-Invariant applied New Graphs: Transitions: undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l3}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.065284s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 2.027872s Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.502415s Time used: 0.486337 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.469788s Time used: 0.464606 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.490725s Time used: 0.485635 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.427642s Time used: 0.422569 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.460020s Time used: 0.454961 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.472439s Time used: 0.467263 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.432502s Time used: 0.419313 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.478992s Time used: 0.474197 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.226936s Time used: 0.222257 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.228820s Time used: 0.224404 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.225370s Time used: 0.221222 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.245639s Time used: 0.241596 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.229074s Time used: 0.225241 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.224669s Time used: 0.220965 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.247979s Time used: 0.24438 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.239817s Time used: 0.236275 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 2.499246s Time used: 2.49181 Improving Solution with cost 3 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 1.013658s Time used: 1.01365 LOG: SAT solveNonLinear - Elapsed time: 3.512904s Cost: 3; Total time: 3.50545 Failed at location 5: __const_8^0 + n0^0 <= __const_7^0 + x^0 Failed at location 5: __const_8^0 + n0^0 <= __const_7^0 + x^0 Failed at location 5: __const_8^0 + n0^0 <= __const_7^0 + x^0 Before Improving: Quasi-invariant at l3: __const_8^0 + n0^0 <= __const_7^0 + x^0 Quasi-invariant at l5: __const_8^0 + n0^0 <= __const_7^0 + x^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.232526s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.194465s Remaining time after improvement: 0.619437 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l3: __const_8^0 + n0^0 <= 1 + __const_7^0 + x^0 Quasi-invariant at l5: __const_8^0 + n0^0 <= 1 + __const_7^0 + x^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: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef112, x^0 -> undef357, y^0 -> undef359, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef112, x^0 -> undef375, y^0 -> undef377, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef357, y^0 -> undef359, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef375, y^0 -> undef377, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef357, y^0 -> undef359, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef375, y^0 -> undef377, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef430, y^0 -> undef432, 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: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef430, y^0 -> undef432, rest remain the same}> New Graphs: Calling Safety with literal __const_8^0 + n0^0 <= 1 + __const_7^0 + x^0 and entry 1, x^0 -> undef574, y^0 -> undef576, rest remain the same}> LOG: CALL check - Post:__const_8^0 + n0^0 <= 1 + __const_7^0 + x^0 - Process 22 * Exit transition: 1, x^0 -> undef574, y^0 -> undef576, rest remain the same}> * Postcondition : __const_8^0 + n0^0 <= 1 + __const_7^0 + x^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.022514s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.022644s Calling Safety with literal __const_8^0 + n0^0 <= 1 + __const_7^0 + x^0 and entry 0, x^0 -> undef592, y^0 -> undef594, rest remain the same}> LOG: CALL check - Post:__const_8^0 + n0^0 <= 1 + __const_7^0 + x^0 - Process 23 * Exit transition: 0, x^0 -> undef592, y^0 -> undef594, rest remain the same}> * Postcondition : __const_8^0 + n0^0 <= 1 + __const_7^0 + x^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.023039s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.023176s Calling Safety with literal __const_8^0 + n0^0 <= 1 + __const_7^0 + x^0 and entry 0, x^0 -> undef610, y^0 -> undef612, rest remain the same}> LOG: CALL check - Post:__const_8^0 + n0^0 <= 1 + __const_7^0 + x^0 - Process 24 * Exit transition: 0, x^0 -> undef610, y^0 -> undef612, rest remain the same}> * Postcondition : __const_8^0 + n0^0 <= 1 + __const_7^0 + x^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.022897s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.023036s INVARIANTS: 3: 5: Quasi-INVARIANTS to narrow Graph: 3: __const_8^0 + n0^0 <= 1 + __const_7^0 + x^0 , 5: __const_8^0 + n0^0 <= 1 + __const_7^0 + x^0 , Narrowing transition: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef112, x^0 -> undef357, y^0 -> undef359, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef112, x^0 -> undef375, y^0 -> undef377, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef357, y^0 -> undef359, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef375, y^0 -> undef377, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef357, y^0 -> undef359, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef375, y^0 -> undef377, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef412, y^0 -> undef414, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef430, y^0 -> undef432, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> undef112, x^0 -> undef357, y^0 -> undef359, rest remain the same}> undef112, x^0 -> undef375, y^0 -> undef377, rest remain the same}> undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> undef357, y^0 -> undef359, rest remain the same}> undef375, y^0 -> undef377, rest remain the same}> undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> undef357, y^0 -> undef359, rest remain the same}> undef375, y^0 -> undef377, rest remain the same}> undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l3, l5}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.958557s Ranking function: 13 + (~(257) / 14)*__const_7^0 + (6 / 7)*__const_8^0 + (103 / 14)*n0^0 + (159 / 14)*n1^0 + (~(103) / 14)*x^0 + (~(159) / 14)*y^0 New Graphs: Transitions: undef112, x^0 -> undef357, y^0 -> undef359, rest remain the same}> undef112, x^0 -> undef375, y^0 -> undef377, rest remain the same}> undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> undef357, y^0 -> undef359, rest remain the same}> undef375, y^0 -> undef377, rest remain the same}> undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> undef357, y^0 -> undef359, rest remain the same}> undef375, y^0 -> undef377, rest remain the same}> undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l3, l5}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.691701s Ranking function: 12 + (~(77) / 3)*__const_7^0 + (32 / 3)*__const_8^0 + (44 / 3)*n0^0 + 2*n1^0 - 8*x^0 - 2*y^0 New Graphs: Transitions: undef112, x^0 -> undef375, y^0 -> undef377, rest remain the same}> undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> undef357, y^0 -> undef359, rest remain the same}> undef375, y^0 -> undef377, rest remain the same}> undef357, y^0 -> undef359, rest remain the same}> undef375, y^0 -> undef377, rest remain the same}> undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l3, l5}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.272720s Ranking function: 8 + (~(82) / 3)*__const_7^0 + (40 / 3)*__const_8^0 + (49 / 3)*n0^0 + 2*n1^0 + (~(49) / 3)*x^0 - 2*y^0 New Graphs: Transitions: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> undef357, y^0 -> undef359, rest remain the same}> undef375, y^0 -> undef377, rest remain the same}> undef357, y^0 -> undef359, rest remain the same}> undef375, y^0 -> undef377, rest remain the same}> undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l3, l5}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.171674s Ranking function: -27 + (~(11) / 4)*__const_7^0 + (11 / 4)*__const_8^0 + (11 / 4)*n0^0 + (43 / 4)*n1^0 + (~(11) / 4)*x^0 + (~(43) / 4)*y^0 New Graphs: Transitions: 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l3}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.374082s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.781101s Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.988139s Time used: 0.955047 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.799869s Time used: 0.788097 Trying to remove transition: 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.868078s Time used: 0.855971 LOG: SAT solveNonLinear - Elapsed time: 0.868078s Cost: 0; Total time: 0.855971 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l3: __const_7^0 <= 1 + n0^0 + n1^0 Ranking function: n0^0 - x^0 Ranking function and negation of Quasi-Invariant applied New Graphs: Transitions: 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l3}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.569465s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.863423s Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.880179s Time used: 0.856127 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.935035s Time used: 0.927863 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.908917s Time used: 0.90165 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.820228s Time used: 0.813012 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.271008s Time used: 0.263721 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.675360s Time used: 0.668743 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.844014s Time used: 0.836855 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.893437s Time used: 0.886353 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.282115s Time used: 0.265925 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.410306s Time used: 0.404058 Trying to remove transition: 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.267884s Time used: 0.261355 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.408682s Time used: 0.402876 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.299633s Time used: 0.293605 Trying to remove transition: 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.523225s Time used: 0.517616 LOG: SAT solveNonLinear - Elapsed time: 0.523225s Cost: 0; Total time: 0.517616 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l3: 1 <= __const_8^0 + executed_Drive^0 + n0^0 Ranking function: n1^0 - y^0 Ranking function and negation of Quasi-Invariant applied New Graphs: Transitions: undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l3}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.069473s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.305811s Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.454678s Time used: 0.441472 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.422524s Time used: 0.417831 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.449256s Time used: 0.444661 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.410432s Time used: 0.405796 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.444931s Time used: 0.440422 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.428412s Time used: 0.42396 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.419718s Time used: 0.415389 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.451775s Time used: 0.447401 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.284720s Time used: 0.280316 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.250364s Time used: 0.246217 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.261951s Time used: 0.258009 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.176825s Time used: 0.172925 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.266128s Time used: 0.262717 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.247884s Time used: 0.244232 Trying to remove transition: undef430, y^0 -> undef432, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.176136s Time used: 0.172696 Trying to remove transition: undef412, y^0 -> undef414, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.255575s Time used: 0.243561 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.573767s Time used: 0.570501 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.932032s Time used: 0.922079 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.915145s Time used: 0.899237 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.937427s Time used: 0.914082 Proving non-termination of subgraph 1 Transitions: undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> undef112, x^0 -> undef357, y^0 -> undef359, rest remain the same}> undef112, x^0 -> undef375, y^0 -> undef377, rest remain the same}> undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> undef357, y^0 -> undef359, rest remain the same}> undef375, y^0 -> undef377, rest remain the same}> undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> undef357, y^0 -> undef359, rest remain the same}> undef375, y^0 -> undef377, rest remain the same}> undef328, x^0 -> undef339, y^0 -> undef341, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> 1, x^0 -> undef412, y^0 -> undef414, rest remain the same}> 1, x^0 -> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> 1, x^0 -> undef394, y^0 -> undef396, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking that every undef value has an assignment... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.189297s Checking conditional non-termination of SCC {l3, l5}... > No assignment for some undef value. > Checking if the negation of the conditions of every pending exit is quasi-invariant... NO Proving non-termination of subgraph 1 Transitions: undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> undef412, y^0 -> undef414, rest remain the same}> undef430, y^0 -> undef432, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking that every undef value has an assignment... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.383620s Checking conditional non-termination of SCC {l3}... > No assignment for some undef value. > Checking if the negation of the conditions of every pending exit is quasi-invariant... YES Calling reachability with... Transition: Conditions: 0 <= 1, Transition: Conditions: 0 <= 1, Transition: Conditions: 0 <= 1, OPEN EXITS: (condsUp: 0 <= 1) (condsUp: 0 <= 1) (condsUp: 0 <= 1) --- Reachability graph --- > Graph without transitions. Calling reachability with... Transition: 1, x^0 -> undef574, y^0 -> undef576, rest remain the same}> Conditions: 0 <= 1, Transition: 0, x^0 -> undef592, y^0 -> undef594, rest remain the same}> Conditions: 0 <= 1, Transition: 0, x^0 -> undef610, y^0 -> undef612, rest remain the same}> Conditions: 0 <= 1, Transition: 1, x^0 -> undef574, y^0 -> undef576, rest remain the same}> Conditions: 0 <= 1, Transition: 0, x^0 -> undef592, y^0 -> undef594, rest remain the same}> Conditions: 0 <= 1, Transition: 0, x^0 -> undef610, y^0 -> undef612, rest remain the same}> Conditions: 0 <= 1, Transition: 1, x^0 -> undef574, y^0 -> undef576, rest remain the same}> Conditions: 0 <= 1, Transition: 0, x^0 -> undef592, y^0 -> undef594, rest remain the same}> Conditions: 0 <= 1, Transition: 0, x^0 -> undef610, y^0 -> undef612, rest remain the same}> Conditions: 0 <= 1, OPEN EXITS: 1, x^0 -> undef574, y^0 -> undef576, rest remain the same}> 0, x^0 -> undef592, y^0 -> undef594, rest remain the same}> 0, x^0 -> undef610, y^0 -> undef612, rest remain the same}> 1, x^0 -> undef574, y^0 -> undef576, rest remain the same}> 0, x^0 -> undef592, y^0 -> undef594, rest remain the same}> 0, x^0 -> undef610, y^0 -> undef612, rest remain the same}> 1, x^0 -> undef574, y^0 -> undef576, rest remain the same}> 0, x^0 -> undef592, y^0 -> undef594, rest remain the same}> 0, x^0 -> undef610, y^0 -> undef612, rest remain the same}> > Conditions are reachable! Program does NOT terminate