NO Solver Timeout: 4 Global Timeout: 300 No parsing errors! Init Location: 0 Transitions: 1, is_aborted^0 -> (0 + undef4), is_aborted_next^0 -> undef4, pc_Drive^0 -> (0 + undef8), pc_Drive_next^0 -> undef8, pc_Loop^0 -> 1, pc_Plan^0 -> undef10, pc_Plan_next^0 -> undef11, x^0 -> (0 + undef13), x_next^0 -> undef13, y^0 -> (0 + undef15), y_next^0 -> undef15}> (0 + undef19), is_aborted_next^0 -> undef19, pc_Drive^0 -> (0 + undef23), pc_Drive_next^0 -> undef23, pc_Loop^0 -> 1, pc_Plan^0 -> undef25, pc_Plan_next^0 -> undef26, x^0 -> (0 + undef28), x_next^0 -> undef28, y^0 -> (0 + undef30), y_next^0 -> undef30}> (0 + undef34), is_aborted_next^0 -> undef34, pc_Drive^0 -> (0 + undef38), pc_Drive_next^0 -> undef38, pc_Loop^0 -> 1, pc_Plan^0 -> undef40, pc_Plan_next^0 -> undef41, x^0 -> (0 + undef43), x_next^0 -> undef43, y^0 -> (0 + undef45), y_next^0 -> undef45}> 1, is_aborted^0 -> (0 + undef49), is_aborted_next^0 -> undef49, pc_Drive^0 -> (0 + undef53), pc_Drive_next^0 -> undef53, pc_Loop^0 -> 1, pc_Plan^0 -> undef55, pc_Plan_next^0 -> undef56, x^0 -> (0 + undef58), x_next^0 -> undef58, y^0 -> (0 + undef60), y_next^0 -> undef60}> (0 + undef64), is_aborted_next^0 -> undef64, pc_Drive^0 -> (0 + undef68), pc_Drive_next^0 -> undef68, pc_Loop^0 -> 1, pc_Plan^0 -> undef70, pc_Plan_next^0 -> undef71, x^0 -> (0 + undef73), x_next^0 -> undef73, y^0 -> (0 + undef75), y_next^0 -> undef75}> (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}> undef91, is_aborted^0 -> (0 + undef94), is_aborted_next^0 -> undef94, pc_Drive^0 -> undef97, pc_Drive_next^0 -> undef98, pc_Loop^0 -> 4, pc_Plan^0 -> (0 + undef101), pc_Plan_next^0 -> undef101, x^0 -> (0 + undef103), x_next^0 -> undef103, y^0 -> (0 + undef105), y_next^0 -> undef105}> (0 + undef109), is_aborted_next^0 -> undef109, pc_Drive^0 -> undef112, pc_Drive_next^0 -> undef113, pc_Loop^0 -> 4, pc_Plan^0 -> (0 + undef116), pc_Plan_next^0 -> undef116, x^0 -> (0 + undef118), x_next^0 -> undef118, y^0 -> (0 + undef120), y_next^0 -> undef120}> (0 + undef124), is_aborted_next^0 -> undef124, pc_Drive^0 -> undef127, pc_Drive_next^0 -> undef128, pc_Loop^0 -> 4, pc_Plan^0 -> (0 + undef131), pc_Plan_next^0 -> undef131, x^0 -> (0 + undef133), x_next^0 -> undef133, y^0 -> (0 + undef135), y_next^0 -> undef135}> 1, is_aborted^0 -> (0 + undef139), is_aborted_next^0 -> undef139, pc_Drive^0 -> undef142, pc_Drive_next^0 -> undef143, pc_Loop^0 -> 4, pc_Plan^0 -> (0 + undef146), pc_Plan_next^0 -> undef146, x^0 -> (0 + undef148), x_next^0 -> undef148, y^0 -> (0 + undef150), y_next^0 -> undef150}> 0, is_aborted^0 -> (0 + undef154), is_aborted_next^0 -> undef154, pc_Drive^0 -> undef157, pc_Drive_next^0 -> undef158, pc_Loop^0 -> 4, pc_Plan^0 -> (0 + undef161), pc_Plan_next^0 -> undef161, x^0 -> (0 + undef163), x_next^0 -> undef163, y^0 -> (0 + undef165), y_next^0 -> undef165}> 0, 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}> 1, is_aborted^0 -> undef183, is_aborted_next^0 -> undef184, pc_Drive^0 -> (0 + undef188), pc_Drive_next^0 -> undef188, pc_Loop^0 -> 7, pc_Plan^0 -> (0 + undef191), pc_Plan_next^0 -> undef191, x^0 -> (0 + undef193), x_next^0 -> undef193, y^0 -> (0 + undef195), y_next^0 -> undef195}> undef198, is_aborted_next^0 -> undef199, pc_Drive^0 -> (0 + undef203), pc_Drive_next^0 -> undef203, pc_Loop^0 -> 7, pc_Plan^0 -> (0 + undef206), pc_Plan_next^0 -> undef206, x^0 -> (0 + undef208), x_next^0 -> undef208, y^0 -> (0 + undef210), y_next^0 -> undef210}> undef213, is_aborted_next^0 -> undef214, pc_Drive^0 -> (0 + undef218), pc_Drive_next^0 -> undef218, pc_Loop^0 -> 7, pc_Plan^0 -> (0 + undef221), pc_Plan_next^0 -> undef221, x^0 -> (0 + undef223), x_next^0 -> undef223, y^0 -> (0 + undef225), y_next^0 -> undef225}> 1, is_aborted^0 -> undef228, is_aborted_next^0 -> undef229, pc_Drive^0 -> (0 + undef233), pc_Drive_next^0 -> undef233, pc_Loop^0 -> 7, pc_Plan^0 -> (0 + undef236), pc_Plan_next^0 -> undef236, x^0 -> undef237, x_next^0 -> undef238, y^0 -> undef239, y_next^0 -> undef240}> undef243, is_aborted_next^0 -> undef244, pc_Drive^0 -> (0 + undef248), pc_Drive_next^0 -> undef248, pc_Loop^0 -> 7, pc_Plan^0 -> (0 + undef251), pc_Plan_next^0 -> undef251, x^0 -> undef252, x_next^0 -> undef253, y^0 -> undef254, y_next^0 -> undef255}> undef258, is_aborted_next^0 -> undef259, pc_Drive^0 -> (0 + undef263), pc_Drive_next^0 -> undef263, pc_Loop^0 -> 7, pc_Plan^0 -> (0 + undef266), pc_Plan_next^0 -> undef266, x^0 -> undef267, x_next^0 -> undef268, y^0 -> undef269, y_next^0 -> undef270}> undef271, is_aborted^0 -> undef273, is_aborted_next^0 -> undef274, pc_Drive^0 -> (0 + undef278), pc_Drive_next^0 -> undef278, pc_Loop^0 -> 2, pc_Plan^0 -> (0 + undef281), pc_Plan_next^0 -> undef281, x^0 -> undef282, x_next^0 -> undef283, y^0 -> undef284, y_next^0 -> undef285}> undef288, is_aborted_next^0 -> undef289, pc_Drive^0 -> (0 + undef293), pc_Drive_next^0 -> undef293, pc_Loop^0 -> 2, pc_Plan^0 -> (0 + undef296), pc_Plan_next^0 -> undef296, x^0 -> undef297, x_next^0 -> undef298, y^0 -> undef299, y_next^0 -> undef300}> undef303, is_aborted_next^0 -> undef304, pc_Drive^0 -> (0 + undef308), pc_Drive_next^0 -> undef308, pc_Loop^0 -> 2, pc_Plan^0 -> (0 + undef311), pc_Plan_next^0 -> undef311, x^0 -> undef312, x_next^0 -> undef313, y^0 -> undef314, y_next^0 -> undef315}> 1, is_aborted^0 -> undef318, is_aborted_next^0 -> undef319, pc_Drive^0 -> (0 + undef323), pc_Drive_next^0 -> undef323, pc_Loop^0 -> 6, pc_Plan^0 -> (0 + undef326), pc_Plan_next^0 -> undef326, x^0 -> (0 + undef328), x_next^0 -> undef328, y^0 -> (0 + undef330), y_next^0 -> undef330}> undef333, is_aborted_next^0 -> undef334, pc_Drive^0 -> (0 + undef338), pc_Drive_next^0 -> undef338, pc_Loop^0 -> 6, pc_Plan^0 -> (0 + undef341), pc_Plan_next^0 -> undef341, x^0 -> (0 + undef343), x_next^0 -> undef343, y^0 -> (0 + undef345), y_next^0 -> undef345}> undef348, is_aborted_next^0 -> undef349, pc_Drive^0 -> (0 + undef353), pc_Drive_next^0 -> undef353, pc_Loop^0 -> 6, pc_Plan^0 -> (0 + undef356), pc_Plan_next^0 -> undef356, x^0 -> (0 + undef358), x_next^0 -> undef358, y^0 -> (0 + undef360), y_next^0 -> undef360}> 1, is_aborted^0 -> undef363, is_aborted_next^0 -> undef364, pc_Drive^0 -> (0 + undef368), pc_Drive_next^0 -> undef368, pc_Loop^0 -> 3, pc_Plan^0 -> (0 + undef371), pc_Plan_next^0 -> undef371, x^0 -> (0 + undef373), x_next^0 -> undef373, y^0 -> (0 + undef375), y_next^0 -> undef375}> undef378, is_aborted_next^0 -> undef379, pc_Drive^0 -> (0 + undef383), pc_Drive_next^0 -> undef383, pc_Loop^0 -> 3, pc_Plan^0 -> (0 + undef386), pc_Plan_next^0 -> undef386, x^0 -> (0 + undef388), x_next^0 -> undef388, y^0 -> (0 + undef390), y_next^0 -> undef390}> undef393, is_aborted_next^0 -> undef394, pc_Drive^0 -> (0 + undef398), pc_Drive_next^0 -> undef398, pc_Loop^0 -> 3, pc_Plan^0 -> (0 + undef401), pc_Plan_next^0 -> undef401, x^0 -> (0 + undef403), x_next^0 -> undef403, y^0 -> (0 + undef405), y_next^0 -> undef405}> 1, is_aborted^0 -> undef408, is_aborted_next^0 -> undef409, pc_Drive^0 -> (0 + undef413), pc_Drive_next^0 -> undef413, pc_Loop^0 -> 7, pc_Plan^0 -> (0 + undef416), pc_Plan_next^0 -> undef416, x^0 -> (0 + undef418), x_next^0 -> undef418, y^0 -> (0 + undef420), y_next^0 -> undef420}> undef423, is_aborted_next^0 -> undef424, pc_Drive^0 -> (0 + undef428), pc_Drive_next^0 -> undef428, pc_Loop^0 -> 7, pc_Plan^0 -> (0 + undef431), pc_Plan_next^0 -> undef431, x^0 -> (0 + undef433), x_next^0 -> undef433, y^0 -> (0 + undef435), y_next^0 -> undef435}> undef438, is_aborted_next^0 -> undef439, pc_Drive^0 -> (0 + undef443), pc_Drive_next^0 -> undef443, pc_Loop^0 -> 7, 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}> 0, fair^0 -> (~(1) + fair^0), is_aborted^0 -> undef453, is_aborted_next^0 -> undef454, pc_Drive^0 -> (0 + undef458), pc_Drive_next^0 -> undef458, pc_Loop^0 -> 7, pc_Plan^0 -> (0 + undef461), pc_Plan_next^0 -> undef461, x^0 -> (0 + undef463), x_next^0 -> undef463, y^0 -> (0 + undef465), y_next^0 -> undef465}> 1, is_aborted^0 -> undef468, is_aborted_next^0 -> undef469, pc_Drive^0 -> (0 + undef473), pc_Drive_next^0 -> undef473, pc_Loop^0 -> 2, pc_Plan^0 -> undef475, pc_Plan_next^0 -> undef476, x^0 -> (0 + undef478), x_next^0 -> undef478, y^0 -> (0 + undef480), y_next^0 -> undef480}> 0, is_aborted^0 -> undef483, is_aborted_next^0 -> undef484, pc_Drive^0 -> (0 + undef488), pc_Drive_next^0 -> undef488, pc_Loop^0 -> 2, pc_Plan^0 -> undef490, pc_Plan_next^0 -> undef491, x^0 -> (0 + undef493), x_next^0 -> undef493, y^0 -> (0 + undef495), y_next^0 -> undef495}> 0, is_aborted^0 -> undef498, is_aborted_next^0 -> undef499, pc_Drive^0 -> (0 + undef503), pc_Drive_next^0 -> undef503, pc_Loop^0 -> 2, pc_Plan^0 -> undef505, pc_Plan_next^0 -> undef506, x^0 -> (0 + undef508), x_next^0 -> undef508, y^0 -> (0 + undef510), y_next^0 -> undef510}> 1, is_aborted^0 -> undef513, is_aborted_next^0 -> undef514, pc_Drive^0 -> (0 + undef518), pc_Drive_next^0 -> undef518, pc_Loop^0 -> 7, pc_Plan^0 -> (0 + undef521), pc_Plan_next^0 -> undef521, x^0 -> (0 + undef523), x_next^0 -> undef523, y^0 -> (0 + undef525), y_next^0 -> undef525}> 0, is_aborted^0 -> undef528, is_aborted_next^0 -> undef529, pc_Drive^0 -> (0 + undef533), pc_Drive_next^0 -> undef533, pc_Loop^0 -> 7, 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}> Fresh variables: undef4, undef8, undef10, undef11, undef13, undef15, undef19, undef23, undef25, undef26, undef28, undef30, undef34, undef38, undef40, undef41, undef43, undef45, undef49, undef53, undef55, undef56, undef58, undef60, undef64, undef68, undef70, undef71, undef73, undef75, undef79, undef83, undef85, undef86, undef88, undef90, undef91, undef94, undef97, undef98, undef101, undef103, undef105, undef109, undef112, undef113, undef116, undef118, undef120, undef124, undef127, undef128, undef131, undef133, undef135, undef139, undef142, undef143, undef146, undef148, undef150, undef154, undef157, undef158, undef161, undef163, undef165, undef169, undef172, undef173, undef176, undef178, undef180, undef183, undef184, undef188, undef191, undef193, undef195, undef198, undef199, undef203, undef206, undef208, undef210, undef213, undef214, undef218, undef221, undef223, undef225, undef228, undef229, undef233, undef236, undef237, undef238, undef239, undef240, undef243, undef244, undef248, undef251, undef252, undef253, undef254, undef255, undef258, undef259, undef263, undef266, undef267, undef268, undef269, undef270, undef271, undef273, undef274, undef278, undef281, undef282, undef283, undef284, undef285, undef288, undef289, undef293, undef296, undef297, undef298, undef299, undef300, undef303, undef304, undef308, undef311, undef312, undef313, undef314, undef315, undef318, undef319, undef323, undef326, undef328, undef330, undef333, undef334, undef338, undef341, undef343, undef345, undef348, undef349, undef353, undef356, undef358, undef360, undef363, undef364, undef368, undef371, undef373, undef375, undef378, undef379, undef383, undef386, undef388, undef390, undef393, undef394, undef398, undef401, undef403, undef405, undef408, undef409, undef413, undef416, undef418, undef420, undef423, undef424, undef428, undef431, undef433, undef435, undef438, undef439, undef443, undef446, undef448, undef450, undef453, undef454, undef458, undef461, undef463, undef465, undef468, undef469, undef473, undef475, undef476, undef478, undef480, undef483, undef484, undef488, undef490, undef491, undef493, undef495, undef498, undef499, undef503, undef505, undef506, undef508, undef510, undef513, undef514, undef518, undef521, undef523, undef525, undef528, undef529, undef533, undef536, undef538, undef540, Undef variables: undef4, undef8, undef10, undef11, undef13, undef15, undef19, undef23, undef25, undef26, undef28, undef30, undef34, undef38, undef40, undef41, undef43, undef45, undef49, undef53, undef55, undef56, undef58, undef60, undef64, undef68, undef70, undef71, undef73, undef75, undef79, undef83, undef85, undef86, undef88, undef90, undef91, undef94, undef97, undef98, undef101, undef103, undef105, undef109, undef112, undef113, undef116, undef118, undef120, undef124, undef127, undef128, undef131, undef133, undef135, undef139, undef142, undef143, undef146, undef148, undef150, undef154, undef157, undef158, undef161, undef163, undef165, undef169, undef172, undef173, undef176, undef178, undef180, undef183, undef184, undef188, undef191, undef193, undef195, undef198, undef199, undef203, undef206, undef208, undef210, undef213, undef214, undef218, undef221, undef223, undef225, undef228, undef229, undef233, undef236, undef237, undef238, undef239, undef240, undef243, undef244, undef248, undef251, undef252, undef253, undef254, undef255, undef258, undef259, undef263, undef266, undef267, undef268, undef269, undef270, undef271, undef273, undef274, undef278, undef281, undef282, undef283, undef284, undef285, undef288, undef289, undef293, undef296, undef297, undef298, undef299, undef300, undef303, undef304, undef308, undef311, undef312, undef313, undef314, undef315, undef318, undef319, undef323, undef326, undef328, undef330, undef333, undef334, undef338, undef341, undef343, undef345, undef348, undef349, undef353, undef356, undef358, undef360, undef363, undef364, undef368, undef371, undef373, undef375, undef378, undef379, undef383, undef386, undef388, undef390, undef393, undef394, undef398, undef401, undef403, undef405, undef408, undef409, undef413, undef416, undef418, undef420, undef423, undef424, undef428, undef431, undef433, undef435, undef438, undef439, undef443, undef446, undef448, undef450, undef453, undef454, undef458, undef461, undef463, undef465, undef468, undef469, undef473, undef475, undef476, undef478, undef480, undef483, undef484, undef488, undef490, undef491, undef493, undef495, undef498, undef499, undef503, undef505, undef506, undef508, undef510, undef513, undef514, undef518, undef521, undef523, undef525, undef528, undef529, undef533, undef536, undef538, undef540, Abstraction variables: Exit nodes: Accepting locations: Asserts: Preprocessed LLVMGraph Init Location: 0 Transitions: 0, fair^0 -> (~(1) + fair^0), x^0 -> (0 + undef463), y^0 -> (0 + undef465)}> 1, x^0 -> (0 + undef478), y^0 -> (0 + undef480)}> 0, x^0 -> (0 + undef493), y^0 -> (0 + undef495)}> 0, x^0 -> (0 + undef508), y^0 -> (0 + undef510)}> 1, x^0 -> (0 + undef523), y^0 -> (0 + undef525)}> 0, x^0 -> (0 + undef538), y^0 -> (0 + undef540)}> 1, x^0 -> (0 + undef193), y^0 -> (0 + undef195)}> (0 + undef208), y^0 -> (0 + undef210)}> (0 + undef223), y^0 -> (0 + undef225)}> 1, x^0 -> undef237, y^0 -> undef239}> undef252, y^0 -> undef254}> undef267, y^0 -> undef269}> undef271, x^0 -> undef282, y^0 -> undef284}> undef297, y^0 -> undef299}> undef312, y^0 -> undef314}> 1, x^0 -> (0 + undef118), y^0 -> (0 + undef120)}> 0, x^0 -> (0 + undef178), y^0 -> (0 + undef180)}> 1, x^0 -> (0 + undef118), y^0 -> (0 + undef120)}> 0, x^0 -> (0 + undef178), y^0 -> (0 + undef180)}> 1, x^0 -> (0 + undef118), y^0 -> (0 + undef120)}> 0, x^0 -> (0 + undef178), y^0 -> (0 + undef180)}> 1, x^0 -> (0 + undef118), y^0 -> (0 + undef120)}> 0, x^0 -> (0 + undef178), y^0 -> (0 + undef180)}> (0 + undef118), y^0 -> (0 + undef120)}> 0, x^0 -> (0 + undef178), y^0 -> (0 + undef180)}> (0 + undef118), y^0 -> (0 + undef120)}> 0, x^0 -> (0 + undef178), y^0 -> (0 + undef180)}> 1, x^0 -> (0 + undef118), y^0 -> (0 + undef120)}> 0, x^0 -> (0 + undef178), y^0 -> (0 + undef180)}> (0 + undef118), y^0 -> (0 + undef120)}> 0, x^0 -> (0 + undef178), y^0 -> (0 + undef180)}> (0 + undef118), y^0 -> (0 + undef120)}> 0, x^0 -> (0 + undef178), y^0 -> (0 + undef180)}> 1, x^0 -> (0 + undef418), y^0 -> (0 + undef420)}> (0 + undef433), y^0 -> (0 + undef435)}> (0 + undef448), y^0 -> (0 + undef450)}> Fresh variables: undef4, undef8, undef10, undef11, undef13, undef15, undef19, undef23, undef25, undef26, undef28, undef30, undef34, undef38, undef40, undef41, undef43, undef45, undef49, undef53, undef55, undef56, undef58, undef60, undef64, undef68, undef70, undef71, undef73, undef75, undef79, undef83, undef85, undef86, undef88, undef90, undef91, undef94, undef97, undef98, undef101, undef103, undef105, undef109, undef112, undef113, undef116, undef118, undef120, undef124, undef127, undef128, undef131, undef133, undef135, undef139, undef142, undef143, undef146, undef148, undef150, undef154, undef157, undef158, undef161, undef163, undef165, undef169, undef172, undef173, undef176, undef178, undef180, undef183, undef184, undef188, undef191, undef193, undef195, undef198, undef199, undef203, undef206, undef208, undef210, undef213, undef214, undef218, undef221, undef223, undef225, undef228, undef229, undef233, undef236, undef237, undef238, undef239, undef240, undef243, undef244, undef248, undef251, undef252, undef253, undef254, undef255, undef258, undef259, undef263, undef266, undef267, undef268, undef269, undef270, undef271, undef273, undef274, undef278, undef281, undef282, undef283, undef284, undef285, undef288, undef289, undef293, undef296, undef297, undef298, undef299, undef300, undef303, undef304, undef308, undef311, undef312, undef313, undef314, undef315, undef318, undef319, undef323, undef326, undef328, undef330, undef333, undef334, undef338, undef341, undef343, undef345, undef348, undef349, undef353, undef356, undef358, undef360, undef363, undef364, undef368, undef371, undef373, undef375, undef378, undef379, undef383, undef386, undef388, undef390, undef393, undef394, undef398, undef401, undef403, undef405, undef408, undef409, undef413, undef416, undef418, undef420, undef423, undef424, undef428, undef431, undef433, undef435, undef438, undef439, undef443, undef446, undef448, undef450, undef453, undef454, undef458, undef461, undef463, undef465, undef468, undef469, undef473, undef475, undef476, undef478, undef480, undef483, undef484, undef488, undef490, undef491, undef493, undef495, undef498, undef499, undef503, undef505, undef506, undef508, undef510, undef513, undef514, undef518, undef521, undef523, undef525, undef528, undef529, undef533, undef536, undef538, undef540, Undef variables: undef4, undef8, undef10, undef11, undef13, undef15, undef19, undef23, undef25, undef26, undef28, undef30, undef34, undef38, undef40, undef41, undef43, undef45, undef49, undef53, undef55, undef56, undef58, undef60, undef64, undef68, undef70, undef71, undef73, undef75, undef79, undef83, undef85, undef86, undef88, undef90, undef91, undef94, undef97, undef98, undef101, undef103, undef105, undef109, undef112, undef113, undef116, undef118, undef120, undef124, undef127, undef128, undef131, undef133, undef135, undef139, undef142, undef143, undef146, undef148, undef150, undef154, undef157, undef158, undef161, undef163, undef165, undef169, undef172, undef173, undef176, undef178, undef180, undef183, undef184, undef188, undef191, undef193, undef195, undef198, undef199, undef203, undef206, undef208, undef210, undef213, undef214, undef218, undef221, undef223, undef225, undef228, undef229, undef233, undef236, undef237, undef238, undef239, undef240, undef243, undef244, undef248, undef251, undef252, undef253, undef254, undef255, undef258, undef259, undef263, undef266, undef267, undef268, undef269, undef270, undef271, undef273, undef274, undef278, undef281, undef282, undef283, undef284, undef285, undef288, undef289, undef293, undef296, undef297, undef298, undef299, undef300, undef303, undef304, undef308, undef311, undef312, undef313, undef314, undef315, undef318, undef319, undef323, undef326, undef328, undef330, undef333, undef334, undef338, undef341, undef343, undef345, undef348, undef349, undef353, undef356, undef358, undef360, undef363, undef364, undef368, undef371, undef373, undef375, undef378, undef379, undef383, undef386, undef388, undef390, undef393, undef394, undef398, undef401, undef403, undef405, undef408, undef409, undef413, undef416, undef418, undef420, undef423, undef424, undef428, undef431, undef433, undef435, undef438, undef439, undef443, undef446, undef448, undef450, undef453, undef454, undef458, undef461, undef463, undef465, undef468, undef469, undef473, undef475, undef476, undef478, undef480, undef483, undef484, undef488, undef490, undef491, undef493, undef495, undef498, undef499, undef503, undef505, undef506, undef508, undef510, undef513, undef514, undef518, undef521, undef523, undef525, undef528, undef529, undef533, undef536, undef538, undef540, Abstraction variables: Exit nodes: Accepting locations: Asserts: ************************************************************* ******************************************************************************************* *********************** WORKING TRANSITION SYSTEM (DAG) *********************** ******************************************************************************************* Init Location: 0 Graph 0: Transitions: Variables: Graph 1: Transitions: undef271, x^0 -> undef282, y^0 -> undef284, rest remain the same}> undef297, y^0 -> undef299, rest remain the same}> undef312, y^0 -> undef314, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> Variables: executed_Drive^0, n0^0, n1^0, x^0, y^0 Graph 2: Transitions: Variables: Precedence: Graph 0 Graph 1 1, x^0 -> undef478, y^0 -> undef480, rest remain the same}> 0, x^0 -> undef493, y^0 -> undef495, rest remain the same}> 0, x^0 -> undef508, y^0 -> undef510, rest remain the same}> Graph 2 0, fair^0 -> -1 + fair^0, x^0 -> undef463, y^0 -> undef465, rest remain the same}> 1, x^0 -> undef523, y^0 -> undef525, rest remain the same}> 0, x^0 -> undef538, y^0 -> undef540, rest remain the same}> 1, x^0 -> undef193, y^0 -> undef195, rest remain the same}> undef208, y^0 -> undef210, rest remain the same}> undef223, y^0 -> undef225, rest remain the same}> 1, x^0 -> undef237, y^0 -> undef239, rest remain the same}> undef252, y^0 -> undef254, rest remain the same}> undef267, y^0 -> undef269, rest remain the same}> 1, x^0 -> undef418, y^0 -> undef420, rest remain the same}> undef433, y^0 -> undef435, rest remain the same}> undef448, y^0 -> undef450, rest remain the same}> Map Locations to Subgraph: ( 0 , 0 ) ( 1 , 2 ) ( 4 , 1 ) ( 5 , 1 ) ******************************************************************************************* ******************************** CHECKING ASSERTIONS ******************************** ******************************************************************************************* Proving termination of subgraph 0 Proving termination of subgraph 1 Checking unfeasibility... Time used: 0.079762 Checking conditional termination of SCC {l4, l5}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.039868s Ranking function: -81 + 39*n0^0 + 19*n1^0 - 39*x^0 - 19*y^0 New Graphs: Transitions: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> Variables: executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.201183s Ranking function: -10 + 5*n0^0 + 5*n1^0 - 5*x^0 - 5*y^0 New Graphs: Transitions: undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> Variables: executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.057202s Ranking function: -11 + executed_Drive^0 + 5*n0^0 + 5*n1^0 - 5*x^0 - 5*y^0 New Graphs: Transitions: undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> Variables: executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.039725s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.123045s Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.048266s Time used: 0.045181 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.051431s Time used: 0.049353 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.046081s Time used: 0.043967 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.044383s Time used: 0.042125 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.046659s Time used: 0.044335 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.049142s Time used: 0.046713 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.050597s Time used: 0.048113 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.048840s Time used: 0.046201 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.271483s Time used: 0.267336 Improving Solution with cost 3 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.318746s Time used: 0.318741 LOG: SAT solveNonLinear - Elapsed time: 0.590229s Cost: 3; Total time: 0.586077 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 l4: 1 + n0^0 <= 0 Quasi-invariant at l5: 1 + n0^0 <= 0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.063442s Remaining time after improvement: 0.947545 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l4: 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: undef271, x^0 -> undef282, y^0 -> undef284, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef297, y^0 -> undef299, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef312, y^0 -> undef314, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, 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: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> New Graphs: Calling Safety with literal 1 + n0^0 <= 0 and entry 1, x^0 -> undef478, y^0 -> undef480, rest remain the same}> LOG: CALL check - Post:1 + n0^0 <= 0 - Process 1 * Exit transition: 1, x^0 -> undef478, y^0 -> undef480, rest remain the same}> * Postcondition : 1 + n0^0 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002505s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.002583s Calling Safety with literal 1 + n0^0 <= 0 and entry 0, x^0 -> undef493, y^0 -> undef495, rest remain the same}> LOG: CALL check - Post:1 + n0^0 <= 0 - Process 2 * Exit transition: 0, x^0 -> undef493, y^0 -> undef495, rest remain the same}> * Postcondition : 1 + n0^0 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002431s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.002511s Calling Safety with literal 1 + n0^0 <= 0 and entry 0, x^0 -> undef508, y^0 -> undef510, rest remain the same}> LOG: CALL check - Post:1 + n0^0 <= 0 - Process 3 * Exit transition: 0, x^0 -> undef508, y^0 -> undef510, rest remain the same}> * Postcondition : 1 + n0^0 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002436s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.002515s INVARIANTS: 4: 5: Quasi-INVARIANTS to narrow Graph: 4: 1 + n0^0 <= 0 , 5: 1 + n0^0 <= 0 , Narrowing transition: undef271, x^0 -> undef282, y^0 -> undef284, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef297, y^0 -> undef299, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef312, y^0 -> undef314, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: undef271, x^0 -> undef282, y^0 -> undef284, rest remain the same}> undef297, y^0 -> undef299, rest remain the same}> undef312, y^0 -> undef314, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> Variables: executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4, l5}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.044755s Ranking function: -82 + 4*n0^0 + 51*n1^0 - 4*x^0 - 51*y^0 New Graphs: Transitions: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> Variables: executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.199102s Ranking function: -10 + 5*n0^0 + 5*n1^0 - 5*x^0 - 5*y^0 New Graphs: Transitions: undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> Variables: executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.059114s Ranking function: -11 + executed_Drive^0 + 5*n0^0 + 5*n1^0 - 5*x^0 - 5*y^0 New Graphs: Transitions: undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> Variables: executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.041100s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.126541s Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.049816s Time used: 0.046579 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.053243s Time used: 0.050804 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.047521s Time used: 0.045226 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.045919s Time used: 0.043449 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.048244s Time used: 0.045646 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.050597s Time used: 0.047934 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.052195s Time used: 0.049447 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.050380s Time used: 0.047503 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.296245s Time used: 0.292325 Improving Solution with cost 3 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.446529s Time used: 0.446512 LOG: SAT solveNonLinear - Elapsed time: 0.742774s Cost: 3; Total time: 0.738837 Failed at location 5: n0^0 + n1^0 <= 1 + x^0 Failed at location 5: n0^0 + n1^0 <= 1 + x^0 Failed at location 5: n0^0 + n1^0 <= 1 + x^0 Before Improving: Quasi-invariant at l4: n0^0 + n1^0 <= 1 + x^0 Quasi-invariant at l5: n0^0 + n1^0 <= 1 + x^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.072377s Remaining time after improvement: 0.939476 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l4: n0^0 + n1^0 <= 1 + x^0 Quasi-invariant at l5: n0^0 + n1^0 <= 1 + 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: undef271, x^0 -> undef282, y^0 -> undef284, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef297, y^0 -> undef299, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef312, y^0 -> undef314, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, 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: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> New Graphs: Calling Safety with literal n0^0 + n1^0 <= 1 + x^0 and entry 1, x^0 -> undef478, y^0 -> undef480, rest remain the same}> LOG: CALL check - Post:n0^0 + n1^0 <= 1 + x^0 - Process 4 * Exit transition: 1, x^0 -> undef478, y^0 -> undef480, rest remain the same}> * Postcondition : n0^0 + n1^0 <= 1 + x^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002733s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.002822s Calling Safety with literal n0^0 + n1^0 <= 1 + x^0 and entry 0, x^0 -> undef493, y^0 -> undef495, rest remain the same}> LOG: CALL check - Post:n0^0 + n1^0 <= 1 + x^0 - Process 5 * Exit transition: 0, x^0 -> undef493, y^0 -> undef495, rest remain the same}> * Postcondition : n0^0 + n1^0 <= 1 + x^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002854s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.002946s Calling Safety with literal n0^0 + n1^0 <= 1 + x^0 and entry 0, x^0 -> undef508, y^0 -> undef510, rest remain the same}> LOG: CALL check - Post:n0^0 + n1^0 <= 1 + x^0 - Process 6 * Exit transition: 0, x^0 -> undef508, y^0 -> undef510, rest remain the same}> * Postcondition : n0^0 + n1^0 <= 1 + x^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002655s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.002746s INVARIANTS: 4: 5: Quasi-INVARIANTS to narrow Graph: 4: n0^0 + n1^0 <= 1 + x^0 , 5: n0^0 + n1^0 <= 1 + x^0 , Narrowing transition: undef271, x^0 -> undef282, y^0 -> undef284, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef297, y^0 -> undef299, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef312, y^0 -> undef314, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: undef271, x^0 -> undef282, y^0 -> undef284, rest remain the same}> undef297, y^0 -> undef299, rest remain the same}> undef312, y^0 -> undef314, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> Variables: executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4, l5}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.087700s Ranking function: -97 + 67*n0^0 + 7*n1^0 - 16*x^0 - 7*y^0 New Graphs: Transitions: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> Variables: executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.233751s Ranking function: -8 + 3*n0^0 + 5*n1^0 - 3*x^0 - 5*y^0 New Graphs: Transitions: undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> Variables: executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.064332s Ranking function: -9 + executed_Drive^0 + 3*n0^0 + 5*n1^0 - 3*x^0 - 5*y^0 New Graphs: Transitions: undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> Variables: executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.042624s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.137939s Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.057364s Time used: 0.053897 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.049699s Time used: 0.04796 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.048975s Time used: 0.047243 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.050582s Time used: 0.048883 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.050784s Time used: 0.049084 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.052216s Time used: 0.050559 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.049540s Time used: 0.047887 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.046484s Time used: 0.044841 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.282049s Time used: 0.277401 Improving Solution with cost 3 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.418763s Time used: 0.418756 LOG: SAT solveNonLinear - Elapsed time: 0.700812s Cost: 3; Total time: 0.696157 Failed at location 5: n0^0 <= 0 Failed at location 5: n0^0 <= 0 Failed at location 5: n0^0 <= 0 Before Improving: Quasi-invariant at l4: n0^0 <= 0 Quasi-invariant at l5: n0^0 <= 0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.068454s Remaining time after improvement: 0.943183 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l4: n0^0 <= 0 Quasi-invariant at l5: 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: undef271, x^0 -> undef282, y^0 -> undef284, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef297, y^0 -> undef299, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef312, y^0 -> undef314, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> [ Termination Graph ] Strengthening and disabling transitions... > It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> New Graphs: Calling Safety with literal n0^0 <= 0 and entry 1, x^0 -> undef478, y^0 -> undef480, rest remain the same}> LOG: CALL check - Post:n0^0 <= 0 - Process 7 * Exit transition: 1, x^0 -> undef478, y^0 -> undef480, rest remain the same}> * Postcondition : n0^0 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003763s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.003853s Calling Safety with literal n0^0 <= 0 and entry 0, x^0 -> undef493, y^0 -> undef495, rest remain the same}> LOG: CALL check - Post:n0^0 <= 0 - Process 8 * Exit transition: 0, x^0 -> undef493, y^0 -> undef495, rest remain the same}> * Postcondition : n0^0 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003688s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.003779s Calling Safety with literal n0^0 <= 0 and entry 0, x^0 -> undef508, y^0 -> undef510, rest remain the same}> LOG: CALL check - Post:n0^0 <= 0 - Process 9 * Exit transition: 0, x^0 -> undef508, y^0 -> undef510, rest remain the same}> * Postcondition : n0^0 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003606s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.003697s INVARIANTS: 4: 5: Quasi-INVARIANTS to narrow Graph: 4: n0^0 <= 0 , 5: n0^0 <= 0 , Narrowing transition: undef271, x^0 -> undef282, y^0 -> undef284, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef297, y^0 -> undef299, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef312, y^0 -> undef314, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: undef271, x^0 -> undef282, y^0 -> undef284, rest remain the same}> undef297, y^0 -> undef299, rest remain the same}> undef312, y^0 -> undef314, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> Variables: executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4, l5}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.077019s Ranking function: -166 + 46*n0^0 + 37*n1^0 - 46*x^0 - 37*y^0 New Graphs: Transitions: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> Variables: executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.246653s Ranking function: -8 + 3*n0^0 + 5*n1^0 - 3*x^0 - 5*y^0 New Graphs: Transitions: undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> Variables: executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.065801s Ranking function: -9 + executed_Drive^0 + 3*n0^0 + 5*n1^0 - 3*x^0 - 5*y^0 New Graphs: Transitions: undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> Variables: executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.043370s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.141450s Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.059646s Time used: 0.055801 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.051250s Time used: 0.049438 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.050374s Time used: 0.048517 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.051657s Time used: 0.04982 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.052092s Time used: 0.050172 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.053228s Time used: 0.051429 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.050609s Time used: 0.04886 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.047532s Time used: 0.045819 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.388593s Time used: 0.383574 Improving Solution with cost 3 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.604528s Time used: 0.604511 LOG: SAT solveNonLinear - Elapsed time: 0.993121s Cost: 3; Total time: 0.988085 Failed at location 5: n0^0 + n1^0 <= 0 Failed at location 5: n0^0 + n1^0 <= 0 Failed at location 5: n0^0 + n1^0 <= 0 Before Improving: Quasi-invariant at l4: n0^0 + n1^0 <= 0 Quasi-invariant at l5: n0^0 + n1^0 <= 0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.084524s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.069084s Remaining time after improvement: 0.868658 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l4: n0^0 + n1^0 <= 1 Quasi-invariant at l5: n0^0 + n1^0 <= 1 [ 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: undef271, x^0 -> undef282, y^0 -> undef284, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef297, y^0 -> undef299, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef312, y^0 -> undef314, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, 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: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> New Graphs: Calling Safety with literal n0^0 + n1^0 <= 1 and entry 1, x^0 -> undef478, y^0 -> undef480, rest remain the same}> LOG: CALL check - Post:n0^0 + n1^0 <= 1 - Process 10 * Exit transition: 1, x^0 -> undef478, y^0 -> undef480, rest remain the same}> * Postcondition : n0^0 + n1^0 <= 1 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004125s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.004217s Calling Safety with literal n0^0 + n1^0 <= 1 and entry 0, x^0 -> undef493, y^0 -> undef495, rest remain the same}> LOG: CALL check - Post:n0^0 + n1^0 <= 1 - Process 11 * Exit transition: 0, x^0 -> undef493, y^0 -> undef495, rest remain the same}> * Postcondition : n0^0 + n1^0 <= 1 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003942s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.004039s Calling Safety with literal n0^0 + n1^0 <= 1 and entry 0, x^0 -> undef508, y^0 -> undef510, rest remain the same}> LOG: CALL check - Post:n0^0 + n1^0 <= 1 - Process 12 * Exit transition: 0, x^0 -> undef508, y^0 -> undef510, rest remain the same}> * Postcondition : n0^0 + n1^0 <= 1 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003891s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.003988s INVARIANTS: 4: 5: Quasi-INVARIANTS to narrow Graph: 4: n0^0 + n1^0 <= 1 , 5: n0^0 + n1^0 <= 1 , Narrowing transition: undef271, x^0 -> undef282, y^0 -> undef284, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef297, y^0 -> undef299, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef312, y^0 -> undef314, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: undef271, x^0 -> undef282, y^0 -> undef284, rest remain the same}> undef297, y^0 -> undef299, rest remain the same}> undef312, y^0 -> undef314, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> Variables: executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4, l5}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.101379s Ranking function: -258 + 64*n0^0 + 65*n1^0 - 64*x^0 - 65*y^0 New Graphs: Transitions: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> Variables: executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.238432s Ranking function: -8 + 3*n0^0 + 5*n1^0 - 3*x^0 - 5*y^0 New Graphs: Transitions: undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> Variables: executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.064590s Ranking function: -12 + executed_Drive^0 + 3*n0^0 + 8*n1^0 - 3*x^0 - 5*y^0 New Graphs: Transitions: undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> Variables: executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.043982s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.143895s Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.057644s Time used: 0.053911 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.050832s Time used: 0.048967 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.051429s Time used: 0.049598 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.054056s Time used: 0.052214 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.054830s Time used: 0.053006 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.054817s Time used: 0.053014 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.055741s Time used: 0.053958 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.051851s Time used: 0.050076 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.408930s Time used: 0.404138 Improving Solution with cost 3 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.537940s Time used: 0.537933 LOG: SAT solveNonLinear - Elapsed time: 0.946870s Cost: 3; Total time: 0.942071 Failed at location 5: n0^0 + n1^0 <= 1 + y^0 Failed at location 5: n0^0 + n1^0 <= 1 + y^0 Failed at location 5: n0^0 + n1^0 <= 1 + y^0 Before Improving: Quasi-invariant at l4: n0^0 + n1^0 <= 1 + y^0 Quasi-invariant at l5: n0^0 + n1^0 <= 1 + y^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.092052s Remaining time after improvement: 0.920393 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l4: n0^0 + n1^0 <= 1 + y^0 Quasi-invariant at l5: n0^0 + n1^0 <= 1 + 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: undef271, x^0 -> undef282, y^0 -> undef284, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef297, y^0 -> undef299, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef312, y^0 -> undef314, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, 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: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> New Graphs: Calling Safety with literal n0^0 + n1^0 <= 1 + y^0 and entry 1, x^0 -> undef478, y^0 -> undef480, rest remain the same}> LOG: CALL check - Post:n0^0 + n1^0 <= 1 + y^0 - Process 13 * Exit transition: 1, x^0 -> undef478, y^0 -> undef480, rest remain the same}> * Postcondition : n0^0 + n1^0 <= 1 + y^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004831s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.004930s Calling Safety with literal n0^0 + n1^0 <= 1 + y^0 and entry 0, x^0 -> undef493, y^0 -> undef495, rest remain the same}> LOG: CALL check - Post:n0^0 + n1^0 <= 1 + y^0 - Process 14 * Exit transition: 0, x^0 -> undef493, y^0 -> undef495, rest remain the same}> * Postcondition : n0^0 + n1^0 <= 1 + y^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004890s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.005001s Calling Safety with literal n0^0 + n1^0 <= 1 + y^0 and entry 0, x^0 -> undef508, y^0 -> undef510, rest remain the same}> LOG: CALL check - Post:n0^0 + n1^0 <= 1 + y^0 - Process 15 * Exit transition: 0, x^0 -> undef508, y^0 -> undef510, rest remain the same}> * Postcondition : n0^0 + n1^0 <= 1 + y^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004810s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.004914s INVARIANTS: 4: 5: Quasi-INVARIANTS to narrow Graph: 4: n0^0 + n1^0 <= 1 + y^0 , 5: n0^0 + n1^0 <= 1 + y^0 , Narrowing transition: undef271, x^0 -> undef282, y^0 -> undef284, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef297, y^0 -> undef299, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef312, y^0 -> undef314, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: undef271, x^0 -> undef282, y^0 -> undef284, rest remain the same}> undef297, y^0 -> undef299, rest remain the same}> undef312, y^0 -> undef314, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> Variables: executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4, l5}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.112173s Ranking function: -244 + 80*n0^0 + 81*n1^0 - 80*x^0 - 3*y^0 New Graphs: Transitions: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> Variables: executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.264928s Ranking function: -6 + 3*n0^0 + 3*n1^0 - 3*x^0 - 3*y^0 New Graphs: Transitions: undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> Variables: executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.072021s Ranking function: -7 + executed_Drive^0 + 3*n0^0 + 3*n1^0 - 3*x^0 - 3*y^0 New Graphs: Transitions: undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> Variables: executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.045775s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.149893s Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.056830s Time used: 0.053017 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.057092s Time used: 0.05518 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.056001s Time used: 0.054066 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.061369s Time used: 0.059445 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.059919s Time used: 0.058018 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.058520s Time used: 0.056618 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.056688s Time used: 0.054838 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.057300s Time used: 0.055467 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.372849s Time used: 0.36765 Improving Solution with cost 3 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.845524s Time used: 0.845356 LOG: SAT solveNonLinear - Elapsed time: 1.218373s Cost: 3; Total time: 1.21301 Failed at location 5: n0^0 + n1^0 <= x^0 + y^0 Failed at location 5: n0^0 + n1^0 <= x^0 + y^0 Failed at location 5: n0^0 + n1^0 <= x^0 + y^0 Before Improving: Quasi-invariant at l4: n0^0 + n1^0 <= 1 + x^0 + y^0 Quasi-invariant at l5: n0^0 + n1^0 <= x^0 + y^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.089205s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.071451s Remaining time after improvement: 0.856676 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l4: n0^0 + n1^0 <= 1 + x^0 + y^0 Quasi-invariant at l5: n0^0 + n1^0 <= 1 + x^0 + 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: undef271, x^0 -> undef282, y^0 -> undef284, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef297, y^0 -> undef299, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef312, y^0 -> undef314, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, 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: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> New Graphs: Calling Safety with literal n0^0 + n1^0 <= 1 + x^0 + y^0 and entry 1, x^0 -> undef478, y^0 -> undef480, rest remain the same}> LOG: CALL check - Post:n0^0 + n1^0 <= 1 + x^0 + y^0 - Process 16 * Exit transition: 1, x^0 -> undef478, y^0 -> undef480, rest remain the same}> * Postcondition : n0^0 + n1^0 <= 1 + x^0 + y^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.006074s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.006187s Calling Safety with literal n0^0 + n1^0 <= 1 + x^0 + y^0 and entry 0, x^0 -> undef493, y^0 -> undef495, rest remain the same}> LOG: CALL check - Post:n0^0 + n1^0 <= 1 + x^0 + y^0 - Process 17 * Exit transition: 0, x^0 -> undef493, y^0 -> undef495, rest remain the same}> * Postcondition : n0^0 + n1^0 <= 1 + x^0 + y^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.006078s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.006195s Calling Safety with literal n0^0 + n1^0 <= 1 + x^0 + y^0 and entry 0, x^0 -> undef508, y^0 -> undef510, rest remain the same}> LOG: CALL check - Post:n0^0 + n1^0 <= 1 + x^0 + y^0 - Process 18 * Exit transition: 0, x^0 -> undef508, y^0 -> undef510, rest remain the same}> * Postcondition : n0^0 + n1^0 <= 1 + x^0 + y^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.006121s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.006237s INVARIANTS: 4: 5: Quasi-INVARIANTS to narrow Graph: 4: n0^0 + n1^0 <= 1 + x^0 + y^0 , 5: n0^0 + n1^0 <= 1 + x^0 + y^0 , Narrowing transition: undef271, x^0 -> undef282, y^0 -> undef284, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef297, y^0 -> undef299, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef312, y^0 -> undef314, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: undef271, x^0 -> undef282, y^0 -> undef284, rest remain the same}> undef297, y^0 -> undef299, rest remain the same}> undef312, y^0 -> undef314, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> Variables: executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4, l5}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.114304s Ranking function: -166 + 41*n0^0 + 42*n1^0 - 41*x^0 - 42*y^0 New Graphs: Transitions: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> Variables: executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.330707s Ranking function: -2 + n0^0 + n1^0 - x^0 - y^0 New Graphs: Transitions: undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> Variables: executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.076922s Ranking function: -3 + executed_Drive^0 + n0^0 + n1^0 - x^0 - y^0 New Graphs: Transitions: undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> Variables: executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.046931s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.161433s Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.063157s Time used: 0.059139 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.060251s Time used: 0.058253 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.061673s Time used: 0.059653 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.063204s Time used: 0.061211 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.065545s Time used: 0.063517 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.061924s Time used: 0.059959 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.061811s Time used: 0.059902 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.061769s Time used: 0.059903 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.443001s Time used: 0.43851 Improving Solution with cost 3 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.614098s Time used: 0.614085 LOG: SAT solveNonLinear - Elapsed time: 1.057100s Cost: 3; Total time: 1.05259 Failed at location 5: 1 + n1^0 <= 0 Failed at location 5: 1 + n1^0 <= 0 Failed at location 5: 1 + n1^0 <= 0 Before Improving: Quasi-invariant at l4: 1 + n1^0 <= 0 Quasi-invariant at l5: 1 + n1^0 <= 0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.090808s Remaining time after improvement: 0.922734 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l4: 1 + n1^0 <= 0 Quasi-invariant at l5: 1 + n1^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: undef271, x^0 -> undef282, y^0 -> undef284, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef297, y^0 -> undef299, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef312, y^0 -> undef314, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> [ Termination Graph ] Strengthening and disabling transitions... > It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> New Graphs: Calling Safety with literal 1 + n1^0 <= 0 and entry 1, x^0 -> undef478, y^0 -> undef480, rest remain the same}> LOG: CALL check - Post:1 + n1^0 <= 0 - Process 19 * Exit transition: 1, x^0 -> undef478, y^0 -> undef480, rest remain the same}> * Postcondition : 1 + n1^0 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.006888s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.006994s Calling Safety with literal 1 + n1^0 <= 0 and entry 0, x^0 -> undef493, y^0 -> undef495, rest remain the same}> LOG: CALL check - Post:1 + n1^0 <= 0 - Process 20 * Exit transition: 0, x^0 -> undef493, y^0 -> undef495, rest remain the same}> * Postcondition : 1 + n1^0 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.006870s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.006982s Calling Safety with literal 1 + n1^0 <= 0 and entry 0, x^0 -> undef508, y^0 -> undef510, rest remain the same}> LOG: CALL check - Post:1 + n1^0 <= 0 - Process 21 * Exit transition: 0, x^0 -> undef508, y^0 -> undef510, rest remain the same}> * Postcondition : 1 + n1^0 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.006866s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.006976s INVARIANTS: 4: 5: Quasi-INVARIANTS to narrow Graph: 4: 1 + n1^0 <= 0 , 5: 1 + n1^0 <= 0 , Narrowing transition: undef271, x^0 -> undef282, y^0 -> undef284, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef297, y^0 -> undef299, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef312, y^0 -> undef314, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: undef271, x^0 -> undef282, y^0 -> undef284, rest remain the same}> undef297, y^0 -> undef299, rest remain the same}> undef312, y^0 -> undef314, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> Variables: executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4, l5}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.196796s Ranking function: -79 + 2*n0^0 + (77 / 2)*n1^0 - 2*x^0 + (~(73) / 2)*y^0 New Graphs: Transitions: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> Variables: executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.334173s Ranking function: -2 + n0^0 + n1^0 - x^0 - y^0 New Graphs: Transitions: undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> Variables: executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.078965s Ranking function: -3 + executed_Drive^0 + n0^0 + n1^0 - x^0 - y^0 New Graphs: Transitions: undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> Variables: executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.048048s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.165348s Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.064736s Time used: 0.060475 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.061541s Time used: 0.059473 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.062720s Time used: 0.06062 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.064378s Time used: 0.062361 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.066332s Time used: 0.064334 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.062744s Time used: 0.060793 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.062880s Time used: 0.060934 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.062825s Time used: 0.060925 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.455647s Time used: 0.450748 Improving Solution with cost 3 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.627024s Time used: 0.627016 LOG: SAT solveNonLinear - Elapsed time: 1.082671s Cost: 3; Total time: 1.07776 Failed at location 5: n0^0 <= x^0 Failed at location 5: n0^0 <= x^0 Failed at location 5: n0^0 <= x^0 Before Improving: Quasi-invariant at l4: n0^0 <= x^0 Quasi-invariant at l5: n0^0 <= x^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.089156s Remaining time after improvement: 0.926115 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l4: n0^0 <= x^0 Quasi-invariant at l5: 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: undef271, x^0 -> undef282, y^0 -> undef284, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef297, y^0 -> undef299, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef312, y^0 -> undef314, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, 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: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> New Graphs: Calling Safety with literal n0^0 <= x^0 and entry 1, x^0 -> undef478, y^0 -> undef480, rest remain the same}> LOG: CALL check - Post:n0^0 <= x^0 - Process 22 * Exit transition: 1, x^0 -> undef478, y^0 -> undef480, rest remain the same}> * Postcondition : n0^0 <= x^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.006954s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.007076s Calling Safety with literal n0^0 <= x^0 and entry 0, x^0 -> undef493, y^0 -> undef495, rest remain the same}> LOG: CALL check - Post:n0^0 <= x^0 - Process 23 * Exit transition: 0, x^0 -> undef493, y^0 -> undef495, rest remain the same}> * Postcondition : n0^0 <= x^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.007206s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.007344s Calling Safety with literal n0^0 <= x^0 and entry 0, x^0 -> undef508, y^0 -> undef510, rest remain the same}> LOG: CALL check - Post:n0^0 <= x^0 - Process 24 * Exit transition: 0, x^0 -> undef508, y^0 -> undef510, rest remain the same}> * Postcondition : n0^0 <= x^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.007135s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.007267s INVARIANTS: 4: 5: Quasi-INVARIANTS to narrow Graph: 4: n0^0 <= x^0 , 5: n0^0 <= x^0 , Narrowing transition: undef271, x^0 -> undef282, y^0 -> undef284, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef297, y^0 -> undef299, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef312, y^0 -> undef314, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: undef271, x^0 -> undef282, y^0 -> undef284, rest remain the same}> undef297, y^0 -> undef299, rest remain the same}> undef312, y^0 -> undef314, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> Variables: executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4, l5}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.240854s Ranking function: -152 + 74*n0^0 + 51*n1^0 - 25*x^0 - 2*y^0 New Graphs: Transitions: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> Variables: executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.355259s Ranking function: -2 + n0^0 + n1^0 - y^0 New Graphs: Transitions: undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> Variables: executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.079736s Ranking function: -2 + executed_Drive^0 + n1^0 - y^0 New Graphs: Transitions: undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> Variables: executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.047334s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.158188s Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.065063s Time used: 0.06095 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.068618s Time used: 0.066565 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.068814s Time used: 0.066714 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.064602s Time used: 0.062531 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.063048s Time used: 0.061008 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.063208s Time used: 0.061203 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.065337s Time used: 0.063386 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.065363s Time used: 0.063418 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.512046s Time used: 0.506223 Improving Solution with cost 3 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.693249s Time used: 0.693099 LOG: SAT solveNonLinear - Elapsed time: 1.205295s Cost: 3; Total time: 1.19932 Failed at location 5: n1^0 <= 0 Failed at location 5: n1^0 <= 0 Failed at location 5: n1^0 <= 0 Before Improving: Quasi-invariant at l4: n1^0 <= 0 Quasi-invariant at l5: n1^0 <= 0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.075630s Remaining time after improvement: 0.932576 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l4: n1^0 <= 0 Quasi-invariant at l5: n1^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: undef271, x^0 -> undef282, y^0 -> undef284, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef297, y^0 -> undef299, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef312, y^0 -> undef314, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> [ Termination Graph ] Strengthening and disabling transitions... > It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> New Graphs: Calling Safety with literal n1^0 <= 0 and entry 1, x^0 -> undef478, y^0 -> undef480, rest remain the same}> LOG: CALL check - Post:n1^0 <= 0 - Process 25 * Exit transition: 1, x^0 -> undef478, y^0 -> undef480, rest remain the same}> * Postcondition : n1^0 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.008131s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.008242s Calling Safety with literal n1^0 <= 0 and entry 0, x^0 -> undef493, y^0 -> undef495, rest remain the same}> LOG: CALL check - Post:n1^0 <= 0 - Process 26 * Exit transition: 0, x^0 -> undef493, y^0 -> undef495, rest remain the same}> * Postcondition : n1^0 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.008142s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.008260s Calling Safety with literal n1^0 <= 0 and entry 0, x^0 -> undef508, y^0 -> undef510, rest remain the same}> LOG: CALL check - Post:n1^0 <= 0 - Process 27 * Exit transition: 0, x^0 -> undef508, y^0 -> undef510, rest remain the same}> * Postcondition : n1^0 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.008194s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.008317s INVARIANTS: 4: 5: Quasi-INVARIANTS to narrow Graph: 4: n1^0 <= 0 , 5: n1^0 <= 0 , Narrowing transition: undef271, x^0 -> undef282, y^0 -> undef284, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef297, y^0 -> undef299, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef312, y^0 -> undef314, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: undef271, x^0 -> undef282, y^0 -> undef284, rest remain the same}> undef297, y^0 -> undef299, rest remain the same}> undef312, y^0 -> undef314, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> Variables: executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4, l5}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.113630s Ranking function: -166 + 83*n1^0 - 83*y^0 New Graphs: Transitions: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> Variables: executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.358820s Ranking function: -2 + n0^0 + n1^0 - y^0 New Graphs: Transitions: undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> Variables: executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.081738s Ranking function: -2 + executed_Drive^0 + n1^0 - y^0 New Graphs: Transitions: undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> Variables: executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.049687s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.162771s Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.067016s Time used: 0.062596 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.070230s Time used: 0.068123 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.070187s Time used: 0.068053 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.065410s Time used: 0.063282 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.064538s Time used: 0.062459 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.064086s Time used: 0.062028 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.066344s Time used: 0.064382 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.066357s Time used: 0.064435 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.453784s Time used: 0.447938 Improving Solution with cost 3 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.599363s Time used: 0.59935 LOG: SAT solveNonLinear - Elapsed time: 1.053147s Cost: 3; Total time: 1.04729 Failed at location 5: 1 + n1^0 <= y^0 Failed at location 5: 1 + n1^0 <= y^0 Failed at location 5: 1 + n1^0 <= y^0 Before Improving: Quasi-invariant at l4: 1 + n1^0 <= y^0 Quasi-invariant at l5: 1 + n1^0 <= y^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.101674s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.082596s Remaining time after improvement: 0.841894 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l4: n1^0 <= y^0 Quasi-invariant at l5: n1^0 <= 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: undef271, x^0 -> undef282, y^0 -> undef284, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef297, y^0 -> undef299, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef312, y^0 -> undef314, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, 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: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> New Graphs: Calling Safety with literal n1^0 <= y^0 and entry 1, x^0 -> undef478, y^0 -> undef480, rest remain the same}> LOG: CALL check - Post:n1^0 <= y^0 - Process 28 * Exit transition: 1, x^0 -> undef478, y^0 -> undef480, rest remain the same}> * Postcondition : n1^0 <= y^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.008497s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.008617s Calling Safety with literal n1^0 <= y^0 and entry 0, x^0 -> undef493, y^0 -> undef495, rest remain the same}> LOG: CALL check - Post:n1^0 <= y^0 - Process 29 * Exit transition: 0, x^0 -> undef493, y^0 -> undef495, rest remain the same}> * Postcondition : n1^0 <= y^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.008569s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.008711s Calling Safety with literal n1^0 <= y^0 and entry 0, x^0 -> undef508, y^0 -> undef510, rest remain the same}> LOG: CALL check - Post:n1^0 <= y^0 - Process 30 * Exit transition: 0, x^0 -> undef508, y^0 -> undef510, rest remain the same}> * Postcondition : n1^0 <= y^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.008442s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.008577s INVARIANTS: 4: 5: Quasi-INVARIANTS to narrow Graph: 4: n1^0 <= y^0 , 5: n1^0 <= y^0 , Narrowing transition: undef271, x^0 -> undef282, y^0 -> undef284, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef297, y^0 -> undef299, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef312, y^0 -> undef314, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: undef271, x^0 -> undef282, y^0 -> undef284, rest remain the same}> undef297, y^0 -> undef299, rest remain the same}> undef312, y^0 -> undef314, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> Variables: executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4, l5}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.094656s Ranking function: -166 + n0^0 + 82*n1^0 - x^0 - 82*y^0 New Graphs: Transitions: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> Variables: executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.374245s Ranking function: (~(1) / 2) + (1 / 2)*n0^0 + (~(1) / 2)*x^0 New Graphs: Transitions: undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> Variables: executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.080556s Ranking function: -1 + executed_Drive^0 New Graphs: Transitions: undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> Variables: executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.047567s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.169973s Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.068377s Time used: 0.064262 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.067064s Time used: 0.064987 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.066354s Time used: 0.064289 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.067615s Time used: 0.065471 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.069020s Time used: 0.067006 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.068818s Time used: 0.066861 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.066293s Time used: 0.064297 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.067088s Time used: 0.065185 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.730911s Time used: 0.72898 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.031113s Time used: 4.02142 Improving Solution with cost 3 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.201676s Time used: 0.201671 LOG: SAT solveNonLinear - Elapsed time: 4.232789s Cost: 3; Total time: 4.22309 Failed at location 5: executed_Drive^0 + n0^0 <= 1 + x^0 Failed at location 5: executed_Drive^0 + n0^0 <= 1 + x^0 Failed at location 5: executed_Drive^0 + n0^0 <= 1 + x^0 Before Improving: Quasi-invariant at l4: executed_Drive^0 + n0^0 <= 1 + x^0 Quasi-invariant at l4: n0^0 <= 1 + x^0 Quasi-invariant at l5: 0 <= executed_Drive^0 Quasi-invariant at l5: executed_Drive^0 + n0^0 <= 1 + x^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.089394s Remaining time after improvement: 0.930986 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l4: executed_Drive^0 + n0^0 <= 1 + x^0 Quasi-invariant at l4: n0^0 <= 1 + x^0 Quasi-invariant at l5: 0 <= executed_Drive^0 Quasi-invariant at l5: executed_Drive^0 + n0^0 <= 1 + 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: undef271, x^0 -> undef282, y^0 -> undef284, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef297, y^0 -> undef299, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef312, y^0 -> undef314, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): 0, x^0 -> undef178, y^0 -> undef180, 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: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef118, y^0 -> undef120, rest remain the same}> New Graphs: Calling Safety with literal executed_Drive^0 + n0^0 <= 1 + x^0 and entry 1, x^0 -> undef478, y^0 -> undef480, rest remain the same}> LOG: CALL check - Post:executed_Drive^0 + n0^0 <= 1 + x^0 - Process 31 * Exit transition: 1, x^0 -> undef478, y^0 -> undef480, rest remain the same}> * Postcondition : executed_Drive^0 + n0^0 <= 1 + x^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.009276s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.009407s Calling Safety with literal executed_Drive^0 + n0^0 <= 1 + x^0 and entry 0, x^0 -> undef493, y^0 -> undef495, rest remain the same}> LOG: CALL check - Post:executed_Drive^0 + n0^0 <= 1 + x^0 - Process 32 * Exit transition: 0, x^0 -> undef493, y^0 -> undef495, rest remain the same}> * Postcondition : executed_Drive^0 + n0^0 <= 1 + x^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.009382s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.009531s Calling Safety with literal executed_Drive^0 + n0^0 <= 1 + x^0 and entry 0, x^0 -> undef508, y^0 -> undef510, rest remain the same}> LOG: CALL check - Post:executed_Drive^0 + n0^0 <= 1 + x^0 - Process 33 * Exit transition: 0, x^0 -> undef508, y^0 -> undef510, rest remain the same}> * Postcondition : executed_Drive^0 + n0^0 <= 1 + x^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.009460s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.009609s INVARIANTS: 4: 5: Quasi-INVARIANTS to narrow Graph: 4: executed_Drive^0 + n0^0 <= 1 + x^0 , n0^0 <= 1 + x^0 , 5: 0 <= executed_Drive^0 , executed_Drive^0 + n0^0 <= 1 + x^0 , Narrowing transition: undef271, x^0 -> undef282, y^0 -> undef284, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: undef297, y^0 -> undef299, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: undef312, y^0 -> undef314, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: undef118, y^0 -> undef120, rest remain the same}> LOG: Narrow transition size 2 Narrowing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> LOG: Narrow transition size 2 invGraph after Narrowing: Transitions: undef271, x^0 -> undef282, y^0 -> undef284, rest remain the same}> undef271, x^0 -> undef282, y^0 -> undef284, rest remain the same}> undef297, y^0 -> undef299, rest remain the same}> undef312, y^0 -> undef314, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> Variables: executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4, l5}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.390014s Ranking function: -300 + 68*n0^0 + 82*n1^0 - 68*x^0 - 82*y^0 New Graphs: Transitions: undef297, y^0 -> undef299, rest remain the same}> undef312, y^0 -> undef314, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> Variables: executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4, l5}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.353292s Ranking function: (~(1) / 2) + (1 / 4)*n0^0 + (1 / 4)*n1^0 + (~(1) / 4)*x^0 + (~(1) / 4)*y^0 It's unfeasible after collapsing. Removing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> It's unfeasible after collapsing. Removing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> It's unfeasible after collapsing. Removing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> It's unfeasible after collapsing. Removing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> It's unfeasible after collapsing. Removing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> It's unfeasible after collapsing. Removing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> It's unfeasible after collapsing. Removing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> It's unfeasible after collapsing. Removing transition: 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> New Graphs: Transitions: undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> Variables: executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.089833s Ranking function: -1 + executed_Drive^0 New Graphs: Transitions: undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> Variables: executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.046390s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.181534s Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.079829s Time used: 0.074846 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.073319s Time used: 0.071104 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.076730s Time used: 0.074556 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.073158s Time used: 0.070985 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.077232s Time used: 0.075074 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.075235s Time used: 0.073106 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.075620s Time used: 0.07355 Trying to remove transition: undef118, y^0 -> undef120, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.076037s Time used: 0.07395 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.093593s Time used: 1.09141 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.006125s Time used: 4.00019 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.017502s Time used: 1.00077 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.520417s Time used: 0.495148 Proving non-termination of subgraph 1 Transitions: undef271, x^0 -> undef282, y^0 -> undef284, rest remain the same}> undef271, x^0 -> undef282, y^0 -> undef284, rest remain the same}> undef297, y^0 -> undef299, rest remain the same}> undef312, y^0 -> undef314, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 1, x^0 -> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> 0, x^0 -> undef178, y^0 -> undef180, rest remain the same}> Variables: 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.612585s Checking conditional non-termination of SCC {l4, 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: undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> undef118, y^0 -> undef120, rest remain the same}> Variables: 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: 2.009740s Checking conditional non-termination of SCC {l4}... > 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 -> undef478, y^0 -> undef480, rest remain the same}> Conditions: 0 <= 1, Transition: 0, x^0 -> undef493, y^0 -> undef495, rest remain the same}> Conditions: 0 <= 1, Transition: 0, x^0 -> undef508, y^0 -> undef510, rest remain the same}> Conditions: 0 <= 1, Transition: 1, x^0 -> undef478, y^0 -> undef480, rest remain the same}> Conditions: 0 <= 1, Transition: 0, x^0 -> undef493, y^0 -> undef495, rest remain the same}> Conditions: 0 <= 1, Transition: 0, x^0 -> undef508, y^0 -> undef510, rest remain the same}> Conditions: 0 <= 1, Transition: 1, x^0 -> undef478, y^0 -> undef480, rest remain the same}> Conditions: 0 <= 1, Transition: 0, x^0 -> undef493, y^0 -> undef495, rest remain the same}> Conditions: 0 <= 1, Transition: 0, x^0 -> undef508, y^0 -> undef510, rest remain the same}> Conditions: 0 <= 1, OPEN EXITS: 1, x^0 -> undef478, y^0 -> undef480, rest remain the same}> 0, x^0 -> undef493, y^0 -> undef495, rest remain the same}> 0, x^0 -> undef508, y^0 -> undef510, rest remain the same}> 1, x^0 -> undef478, y^0 -> undef480, rest remain the same}> 0, x^0 -> undef493, y^0 -> undef495, rest remain the same}> 0, x^0 -> undef508, y^0 -> undef510, rest remain the same}> 1, x^0 -> undef478, y^0 -> undef480, rest remain the same}> 0, x^0 -> undef493, y^0 -> undef495, rest remain the same}> 0, x^0 -> undef508, y^0 -> undef510, rest remain the same}> > Conditions are reachable! Program does NOT terminate