YES Solver Timeout: 4 Global Timeout: 300 No parsing errors! Init Location: 0 Transitions: 1, is_aborted^0 -> (0 + undef23), is_aborted_next^0 -> undef23, pc_Drive^0 -> (0 + undef27), pc_Drive_next^0 -> undef27, pc_Loop^0 -> 1, pc_Plan^0 -> undef29, pc_Plan_next^0 -> undef30, x^0 -> (0 + undef32), x_next^0 -> undef32, y^0 -> (0 + undef34), y_next^0 -> undef34}> (0 + undef40), is_aborted_next^0 -> undef40, pc_Drive^0 -> (0 + undef44), pc_Drive_next^0 -> undef44, pc_Loop^0 -> 1, pc_Plan^0 -> undef46, pc_Plan_next^0 -> undef47, x^0 -> (0 + undef49), x_next^0 -> undef49, y^0 -> (0 + undef51), y_next^0 -> undef51}> (0 + undef57), is_aborted_next^0 -> undef57, pc_Drive^0 -> (0 + undef61), pc_Drive_next^0 -> undef61, pc_Loop^0 -> 1, pc_Plan^0 -> undef63, pc_Plan_next^0 -> undef64, x^0 -> (0 + undef66), x_next^0 -> undef66, y^0 -> (0 + undef68), y_next^0 -> undef68}> 1, is_aborted^0 -> (0 + undef74), is_aborted_next^0 -> undef74, pc_Drive^0 -> (0 + undef78), pc_Drive_next^0 -> undef78, pc_Loop^0 -> 1, pc_Plan^0 -> undef80, pc_Plan_next^0 -> undef81, x^0 -> (0 + undef83), x_next^0 -> undef83, y^0 -> (0 + undef85), y_next^0 -> undef85}> (0 + undef91), is_aborted_next^0 -> undef91, pc_Drive^0 -> (0 + undef95), pc_Drive_next^0 -> undef95, pc_Loop^0 -> 1, pc_Plan^0 -> undef97, pc_Plan_next^0 -> undef98, x^0 -> (0 + undef100), x_next^0 -> undef100, y^0 -> (0 + undef102), y_next^0 -> undef102}> (0 + undef108), is_aborted_next^0 -> undef108, pc_Drive^0 -> (0 + undef112), pc_Drive_next^0 -> undef112, pc_Loop^0 -> 1, pc_Plan^0 -> undef114, pc_Plan_next^0 -> undef115, x^0 -> (0 + undef117), x_next^0 -> undef117, y^0 -> (0 + undef119), y_next^0 -> undef119}> undef123, is_aborted^0 -> (0 + undef125), is_aborted_next^0 -> undef125, pc_Drive^0 -> undef128, pc_Drive_next^0 -> undef129, pc_Loop^0 -> 4, pc_Plan^0 -> (0 + undef132), pc_Plan_next^0 -> undef132, x^0 -> (0 + undef134), x_next^0 -> undef134, y^0 -> (0 + undef136), y_next^0 -> undef136}> (0 + undef142), is_aborted_next^0 -> undef142, pc_Drive^0 -> undef145, pc_Drive_next^0 -> undef146, pc_Loop^0 -> 4, pc_Plan^0 -> (0 + undef149), pc_Plan_next^0 -> undef149, x^0 -> (0 + undef151), x_next^0 -> undef151, y^0 -> (0 + undef153), y_next^0 -> undef153}> (0 + undef159), is_aborted_next^0 -> undef159, pc_Drive^0 -> undef162, pc_Drive_next^0 -> undef163, pc_Loop^0 -> 4, pc_Plan^0 -> (0 + undef166), pc_Plan_next^0 -> undef166, x^0 -> (0 + undef168), x_next^0 -> undef168, y^0 -> (0 + undef170), y_next^0 -> undef170}> 1, is_aborted^0 -> (0 + undef176), is_aborted_next^0 -> undef176, pc_Drive^0 -> undef179, pc_Drive_next^0 -> undef180, pc_Loop^0 -> 4, pc_Plan^0 -> (0 + undef183), pc_Plan_next^0 -> undef183, x^0 -> (0 + undef185), x_next^0 -> undef185, y^0 -> (0 + undef187), y_next^0 -> undef187}> 0, is_aborted^0 -> (0 + undef193), is_aborted_next^0 -> undef193, pc_Drive^0 -> undef196, pc_Drive_next^0 -> undef197, pc_Loop^0 -> 4, pc_Plan^0 -> (0 + undef200), pc_Plan_next^0 -> undef200, x^0 -> (0 + undef202), x_next^0 -> undef202, y^0 -> (0 + undef204), y_next^0 -> undef204}> 0, is_aborted^0 -> (0 + undef210), is_aborted_next^0 -> undef210, pc_Drive^0 -> undef213, pc_Drive_next^0 -> undef214, pc_Loop^0 -> 4, pc_Plan^0 -> (0 + undef217), pc_Plan_next^0 -> undef217, x^0 -> (0 + undef219), x_next^0 -> undef219, y^0 -> (0 + undef221), y_next^0 -> undef221}> 1, is_aborted^0 -> undef226, is_aborted_next^0 -> undef227, pc_Drive^0 -> (0 + undef231), pc_Drive_next^0 -> undef231, pc_Loop^0 -> (0 + __const_7^0), pc_Plan^0 -> (0 + undef234), pc_Plan_next^0 -> undef234, x^0 -> (0 + undef236), x_next^0 -> undef236, y^0 -> (0 + undef238), y_next^0 -> undef238}> undef243, is_aborted_next^0 -> undef244, pc_Drive^0 -> (0 + undef248), pc_Drive_next^0 -> undef248, pc_Loop^0 -> (0 + __const_7^0), pc_Plan^0 -> (0 + undef251), pc_Plan_next^0 -> undef251, x^0 -> (0 + undef253), x_next^0 -> undef253, y^0 -> (0 + undef255), y_next^0 -> undef255}> undef260, is_aborted_next^0 -> undef261, pc_Drive^0 -> (0 + undef265), pc_Drive_next^0 -> undef265, pc_Loop^0 -> (0 + __const_7^0), pc_Plan^0 -> (0 + undef268), pc_Plan_next^0 -> undef268, x^0 -> (0 + undef270), x_next^0 -> undef270, y^0 -> (0 + undef272), y_next^0 -> undef272}> 1, is_aborted^0 -> undef277, is_aborted_next^0 -> undef278, pc_Drive^0 -> (0 + undef282), pc_Drive_next^0 -> undef282, pc_Loop^0 -> (0 + __const_7^0), pc_Plan^0 -> (0 + undef285), pc_Plan_next^0 -> undef285, x^0 -> undef286, x_next^0 -> undef287, y^0 -> undef288, y_next^0 -> undef289}> undef294, is_aborted_next^0 -> undef295, pc_Drive^0 -> (0 + undef299), pc_Drive_next^0 -> undef299, pc_Loop^0 -> (0 + __const_7^0), pc_Plan^0 -> (0 + undef302), pc_Plan_next^0 -> undef302, x^0 -> undef303, x_next^0 -> undef304, y^0 -> undef305, y_next^0 -> undef306}> undef311, is_aborted_next^0 -> undef312, pc_Drive^0 -> (0 + undef316), pc_Drive_next^0 -> undef316, pc_Loop^0 -> (0 + __const_7^0), pc_Plan^0 -> (0 + undef319), pc_Plan_next^0 -> undef319, x^0 -> undef320, x_next^0 -> undef321, y^0 -> undef322, y_next^0 -> undef323}> 0, is_aborted^0 -> undef328, is_aborted_next^0 -> undef329, pc_Drive^0 -> (0 + undef333), pc_Drive_next^0 -> undef333, pc_Loop^0 -> 2, pc_Plan^0 -> (0 + undef336), pc_Plan_next^0 -> undef336, x^0 -> undef337, x_next^0 -> undef338, y^0 -> undef339, y_next^0 -> undef340}> 0, is_aborted^0 -> undef346, is_aborted_next^0 -> undef347, pc_Drive^0 -> (0 + undef351), pc_Drive_next^0 -> undef351, pc_Loop^0 -> 2, pc_Plan^0 -> (0 + undef354), pc_Plan_next^0 -> undef354, x^0 -> undef355, x_next^0 -> undef356, y^0 -> undef357, y_next^0 -> undef358}> 0, is_aborted^0 -> undef363, is_aborted_next^0 -> undef364, pc_Drive^0 -> (0 + undef368), pc_Drive_next^0 -> undef368, pc_Loop^0 -> 2, pc_Plan^0 -> (0 + undef371), pc_Plan_next^0 -> undef371, x^0 -> undef372, x_next^0 -> undef373, y^0 -> undef374, y_next^0 -> undef375}> 1, is_aborted^0 -> undef380, is_aborted_next^0 -> undef381, pc_Drive^0 -> (0 + undef385), pc_Drive_next^0 -> undef385, pc_Loop^0 -> (0 + __const_6^0), pc_Plan^0 -> (0 + undef388), pc_Plan_next^0 -> undef388, x^0 -> (0 + undef390), x_next^0 -> undef390, y^0 -> (0 + undef392), y_next^0 -> undef392}> undef397, is_aborted_next^0 -> undef398, pc_Drive^0 -> (0 + undef402), pc_Drive_next^0 -> undef402, pc_Loop^0 -> (0 + __const_6^0), pc_Plan^0 -> (0 + undef405), pc_Plan_next^0 -> undef405, x^0 -> (0 + undef407), x_next^0 -> undef407, y^0 -> (0 + undef409), y_next^0 -> undef409}> undef414, is_aborted_next^0 -> undef415, pc_Drive^0 -> (0 + undef419), pc_Drive_next^0 -> undef419, pc_Loop^0 -> (0 + __const_6^0), pc_Plan^0 -> (0 + undef422), pc_Plan_next^0 -> undef422, x^0 -> (0 + undef424), x_next^0 -> undef424, y^0 -> (0 + undef426), y_next^0 -> undef426}> 1, is_aborted^0 -> undef431, is_aborted_next^0 -> undef432, pc_Drive^0 -> (0 + undef436), pc_Drive_next^0 -> undef436, pc_Loop^0 -> 3, pc_Plan^0 -> (0 + undef439), pc_Plan_next^0 -> undef439, x^0 -> (0 + undef441), x_next^0 -> undef441, y^0 -> (0 + undef443), y_next^0 -> undef443}> undef448, is_aborted_next^0 -> undef449, pc_Drive^0 -> (0 + undef453), pc_Drive_next^0 -> undef453, pc_Loop^0 -> 3, pc_Plan^0 -> (0 + undef456), pc_Plan_next^0 -> undef456, x^0 -> (0 + undef458), x_next^0 -> undef458, y^0 -> (0 + undef460), y_next^0 -> undef460}> undef465, is_aborted_next^0 -> undef466, pc_Drive^0 -> (0 + undef470), pc_Drive_next^0 -> undef470, pc_Loop^0 -> 3, pc_Plan^0 -> (0 + undef473), pc_Plan_next^0 -> undef473, x^0 -> (0 + undef475), x_next^0 -> undef475, y^0 -> (0 + undef477), y_next^0 -> undef477}> 1, is_aborted^0 -> undef482, is_aborted_next^0 -> undef483, pc_Drive^0 -> (0 + undef487), pc_Drive_next^0 -> undef487, pc_Loop^0 -> (0 + __const_7^0), pc_Plan^0 -> (0 + undef490), pc_Plan_next^0 -> undef490, x^0 -> (0 + undef492), x_next^0 -> undef492, y^0 -> (0 + undef494), y_next^0 -> undef494}> undef499, is_aborted_next^0 -> undef500, pc_Drive^0 -> (0 + undef504), pc_Drive_next^0 -> undef504, pc_Loop^0 -> (0 + __const_7^0), pc_Plan^0 -> (0 + undef507), pc_Plan_next^0 -> undef507, x^0 -> (0 + undef509), x_next^0 -> undef509, y^0 -> (0 + undef511), y_next^0 -> undef511}> undef516, is_aborted_next^0 -> undef517, pc_Drive^0 -> (0 + undef521), pc_Drive_next^0 -> undef521, pc_Loop^0 -> (0 + __const_7^0), pc_Plan^0 -> (0 + undef524), pc_Plan_next^0 -> undef524, x^0 -> (0 + undef526), x_next^0 -> undef526, y^0 -> (0 + undef528), y_next^0 -> undef528}> 1, is_aborted^0 -> undef533, is_aborted_next^0 -> undef534, pc_Drive^0 -> (0 + undef538), pc_Drive_next^0 -> undef538, pc_Loop^0 -> 2, pc_Plan^0 -> undef540, pc_Plan_next^0 -> undef541, x^0 -> (0 + undef543), x_next^0 -> undef543, y^0 -> (0 + undef545), y_next^0 -> undef545}> 0, is_aborted^0 -> undef550, is_aborted_next^0 -> undef551, pc_Drive^0 -> (0 + undef555), pc_Drive_next^0 -> undef555, pc_Loop^0 -> 2, pc_Plan^0 -> undef557, pc_Plan_next^0 -> undef558, x^0 -> (0 + undef560), x_next^0 -> undef560, y^0 -> (0 + undef562), y_next^0 -> undef562}> 0, is_aborted^0 -> undef567, is_aborted_next^0 -> undef568, pc_Drive^0 -> (0 + undef572), pc_Drive_next^0 -> undef572, pc_Loop^0 -> 2, pc_Plan^0 -> undef574, pc_Plan_next^0 -> undef575, x^0 -> (0 + undef577), x_next^0 -> undef577, y^0 -> (0 + undef579), y_next^0 -> undef579}> 1, is_aborted^0 -> undef584, is_aborted_next^0 -> undef585, pc_Drive^0 -> (0 + undef589), pc_Drive_next^0 -> undef589, pc_Loop^0 -> (0 + __const_7^0), pc_Plan^0 -> (0 + undef592), pc_Plan_next^0 -> undef592, x^0 -> (0 + undef594), x_next^0 -> undef594, y^0 -> (0 + undef596), y_next^0 -> undef596}> 0, is_aborted^0 -> undef601, is_aborted_next^0 -> undef602, pc_Drive^0 -> (0 + undef606), pc_Drive_next^0 -> undef606, pc_Loop^0 -> (0 + __const_7^0), pc_Plan^0 -> (0 + undef609), pc_Plan_next^0 -> undef609, x^0 -> (0 + undef611), x_next^0 -> undef611, y^0 -> (0 + undef613), y_next^0 -> undef613}> 0, is_aborted^0 -> undef618, is_aborted_next^0 -> undef619, pc_Drive^0 -> (0 + undef623), pc_Drive_next^0 -> undef623, pc_Loop^0 -> (0 + __const_7^0), pc_Plan^0 -> (0 + undef626), pc_Plan_next^0 -> undef626, x^0 -> (0 + undef628), x_next^0 -> undef628, y^0 -> (0 + undef630), y_next^0 -> undef630}> Fresh variables: undef23, undef27, undef29, undef30, undef32, undef34, undef40, undef44, undef46, undef47, undef49, undef51, undef57, undef61, undef63, undef64, undef66, undef68, undef74, undef78, undef80, undef81, undef83, undef85, undef91, undef95, undef97, undef98, undef100, undef102, undef108, undef112, undef114, undef115, undef117, undef119, undef123, undef125, undef128, undef129, undef132, undef134, undef136, undef142, undef145, undef146, undef149, undef151, undef153, undef159, undef162, undef163, undef166, undef168, undef170, undef176, undef179, undef180, undef183, undef185, undef187, undef193, undef196, undef197, undef200, undef202, undef204, undef210, undef213, undef214, undef217, undef219, undef221, undef226, undef227, undef231, undef234, undef236, undef238, undef243, undef244, undef248, undef251, undef253, undef255, undef260, undef261, undef265, undef268, undef270, undef272, undef277, undef278, undef282, undef285, undef286, undef287, undef288, undef289, undef294, undef295, undef299, undef302, undef303, undef304, undef305, undef306, undef311, undef312, undef316, undef319, undef320, undef321, undef322, undef323, undef328, undef329, undef333, undef336, undef337, undef338, undef339, undef340, undef341, undef346, undef347, undef351, undef354, undef355, undef356, undef357, undef358, undef363, undef364, undef368, undef371, undef372, undef373, undef374, undef375, undef380, undef381, undef385, undef388, undef390, undef392, undef397, undef398, undef402, undef405, undef407, undef409, undef414, undef415, undef419, undef422, undef424, undef426, undef431, undef432, undef436, undef439, undef441, undef443, undef448, undef449, undef453, undef456, undef458, undef460, undef465, undef466, undef470, undef473, undef475, undef477, undef482, undef483, undef487, undef490, undef492, undef494, undef499, undef500, undef504, undef507, undef509, undef511, undef516, undef517, undef521, undef524, undef526, undef528, undef533, undef534, undef538, undef540, undef541, undef543, undef545, undef550, undef551, undef555, undef557, undef558, undef560, undef562, undef567, undef568, undef572, undef574, undef575, undef577, undef579, undef584, undef585, undef589, undef592, undef594, undef596, undef601, undef602, undef606, undef609, undef611, undef613, undef618, undef619, undef623, undef626, undef628, undef630, Undef variables: undef23, undef27, undef29, undef30, undef32, undef34, undef40, undef44, undef46, undef47, undef49, undef51, undef57, undef61, undef63, undef64, undef66, undef68, undef74, undef78, undef80, undef81, undef83, undef85, undef91, undef95, undef97, undef98, undef100, undef102, undef108, undef112, undef114, undef115, undef117, undef119, undef123, undef125, undef128, undef129, undef132, undef134, undef136, undef142, undef145, undef146, undef149, undef151, undef153, undef159, undef162, undef163, undef166, undef168, undef170, undef176, undef179, undef180, undef183, undef185, undef187, undef193, undef196, undef197, undef200, undef202, undef204, undef210, undef213, undef214, undef217, undef219, undef221, undef226, undef227, undef231, undef234, undef236, undef238, undef243, undef244, undef248, undef251, undef253, undef255, undef260, undef261, undef265, undef268, undef270, undef272, undef277, undef278, undef282, undef285, undef286, undef287, undef288, undef289, undef294, undef295, undef299, undef302, undef303, undef304, undef305, undef306, undef311, undef312, undef316, undef319, undef320, undef321, undef322, undef323, undef328, undef329, undef333, undef336, undef337, undef338, undef339, undef340, undef341, undef346, undef347, undef351, undef354, undef355, undef356, undef357, undef358, undef363, undef364, undef368, undef371, undef372, undef373, undef374, undef375, undef380, undef381, undef385, undef388, undef390, undef392, undef397, undef398, undef402, undef405, undef407, undef409, undef414, undef415, undef419, undef422, undef424, undef426, undef431, undef432, undef436, undef439, undef441, undef443, undef448, undef449, undef453, undef456, undef458, undef460, undef465, undef466, undef470, undef473, undef475, undef477, undef482, undef483, undef487, undef490, undef492, undef494, undef499, undef500, undef504, undef507, undef509, undef511, undef516, undef517, undef521, undef524, undef526, undef528, undef533, undef534, undef538, undef540, undef541, undef543, undef545, undef550, undef551, undef555, undef557, undef558, undef560, undef562, undef567, undef568, undef572, undef574, undef575, undef577, undef579, undef584, undef585, undef589, undef592, undef594, undef596, undef601, undef602, undef606, undef609, undef611, undef613, undef618, undef619, undef623, undef626, undef628, undef630, Abstraction variables: Exit nodes: Accepting locations: Asserts: Preprocessed LLVMGraph Init Location: 0 Transitions: 1, x^0 -> (0 + undef543), y^0 -> (0 + undef545)}> 0, x^0 -> (0 + undef560), y^0 -> (0 + undef562)}> 0, x^0 -> (0 + undef577), y^0 -> (0 + undef579)}> 1, x^0 -> (0 + undef594), y^0 -> (0 + undef596)}> 0, x^0 -> (0 + undef611), y^0 -> (0 + undef613)}> 0, x^0 -> (0 + undef628), y^0 -> (0 + undef630)}> 1, x^0 -> (0 + undef236), y^0 -> (0 + undef238)}> undef123, x^0 -> (0 + undef253), y^0 -> (0 + undef255)}> undef123, x^0 -> (0 + undef270), y^0 -> (0 + undef272)}> 1, x^0 -> undef286, y^0 -> undef288}> undef123, x^0 -> undef303, y^0 -> undef305}> undef123, x^0 -> undef320, y^0 -> undef322}> 0, x^0 -> undef337, y^0 -> undef339}> 0, x^0 -> undef355, y^0 -> undef357}> 0, x^0 -> undef372, y^0 -> undef374}> 1, x^0 -> (0 + undef236), y^0 -> (0 + undef238)}> (0 + undef253), y^0 -> (0 + undef255)}> (0 + undef270), y^0 -> (0 + undef272)}> 1, x^0 -> undef286, y^0 -> undef288}> undef303, y^0 -> undef305}> undef320, y^0 -> undef322}> 0, x^0 -> undef337, y^0 -> undef339}> 0, x^0 -> undef355, y^0 -> undef357}> 0, x^0 -> undef372, y^0 -> undef374}> 1, x^0 -> (0 + undef236), y^0 -> (0 + undef238)}> (0 + undef253), y^0 -> (0 + undef255)}> (0 + undef270), y^0 -> (0 + undef272)}> 1, x^0 -> undef286, y^0 -> undef288}> undef303, y^0 -> undef305}> undef320, y^0 -> undef322}> 0, x^0 -> undef337, y^0 -> undef339}> 0, x^0 -> undef355, y^0 -> undef357}> 0, x^0 -> undef372, y^0 -> undef374}> 1, x^0 -> (0 + undef236), y^0 -> (0 + undef238)}> 0, x^0 -> (0 + undef253), y^0 -> (0 + undef255)}> 0, x^0 -> (0 + undef270), y^0 -> (0 + undef272)}> 1, x^0 -> undef286, y^0 -> undef288}> 0, x^0 -> undef303, y^0 -> undef305}> 0, x^0 -> undef320, y^0 -> undef322}> 0, x^0 -> undef337, y^0 -> undef339}> 1, x^0 -> (0 + undef390), y^0 -> (0 + undef392)}> 1, x^0 -> (0 + undef407), y^0 -> (0 + undef409)}> 1, x^0 -> (0 + undef424), y^0 -> (0 + undef426)}> 1, x^0 -> (0 + undef390), y^0 -> (0 + undef392)}> (0 + undef407), y^0 -> (0 + undef409)}> (0 + undef424), y^0 -> (0 + undef426)}> 1, x^0 -> (0 + undef390), y^0 -> (0 + undef392)}> (0 + undef407), y^0 -> (0 + undef409)}> (0 + undef424), y^0 -> (0 + undef426)}> 1, x^0 -> (0 + undef492), y^0 -> (0 + undef494)}> (0 + undef509), y^0 -> (0 + undef511)}> (0 + undef526), y^0 -> (0 + undef528)}> Fresh variables: undef23, undef27, undef29, undef30, undef32, undef34, undef40, undef44, undef46, undef47, undef49, undef51, undef57, undef61, undef63, undef64, undef66, undef68, undef74, undef78, undef80, undef81, undef83, undef85, undef91, undef95, undef97, undef98, undef100, undef102, undef108, undef112, undef114, undef115, undef117, undef119, undef123, undef125, undef128, undef129, undef132, undef134, undef136, undef142, undef145, undef146, undef149, undef151, undef153, undef159, undef162, undef163, undef166, undef168, undef170, undef176, undef179, undef180, undef183, undef185, undef187, undef193, undef196, undef197, undef200, undef202, undef204, undef210, undef213, undef214, undef217, undef219, undef221, undef226, undef227, undef231, undef234, undef236, undef238, undef243, undef244, undef248, undef251, undef253, undef255, undef260, undef261, undef265, undef268, undef270, undef272, undef277, undef278, undef282, undef285, undef286, undef287, undef288, undef289, undef294, undef295, undef299, undef302, undef303, undef304, undef305, undef306, undef311, undef312, undef316, undef319, undef320, undef321, undef322, undef323, undef328, undef329, undef333, undef336, undef337, undef338, undef339, undef340, undef341, undef346, undef347, undef351, undef354, undef355, undef356, undef357, undef358, undef363, undef364, undef368, undef371, undef372, undef373, undef374, undef375, undef380, undef381, undef385, undef388, undef390, undef392, undef397, undef398, undef402, undef405, undef407, undef409, undef414, undef415, undef419, undef422, undef424, undef426, undef431, undef432, undef436, undef439, undef441, undef443, undef448, undef449, undef453, undef456, undef458, undef460, undef465, undef466, undef470, undef473, undef475, undef477, undef482, undef483, undef487, undef490, undef492, undef494, undef499, undef500, undef504, undef507, undef509, undef511, undef516, undef517, undef521, undef524, undef526, undef528, undef533, undef534, undef538, undef540, undef541, undef543, undef545, undef550, undef551, undef555, undef557, undef558, undef560, undef562, undef567, undef568, undef572, undef574, undef575, undef577, undef579, undef584, undef585, undef589, undef592, undef594, undef596, undef601, undef602, undef606, undef609, undef611, undef613, undef618, undef619, undef623, undef626, undef628, undef630, Undef variables: undef23, undef27, undef29, undef30, undef32, undef34, undef40, undef44, undef46, undef47, undef49, undef51, undef57, undef61, undef63, undef64, undef66, undef68, undef74, undef78, undef80, undef81, undef83, undef85, undef91, undef95, undef97, undef98, undef100, undef102, undef108, undef112, undef114, undef115, undef117, undef119, undef123, undef125, undef128, undef129, undef132, undef134, undef136, undef142, undef145, undef146, undef149, undef151, undef153, undef159, undef162, undef163, undef166, undef168, undef170, undef176, undef179, undef180, undef183, undef185, undef187, undef193, undef196, undef197, undef200, undef202, undef204, undef210, undef213, undef214, undef217, undef219, undef221, undef226, undef227, undef231, undef234, undef236, undef238, undef243, undef244, undef248, undef251, undef253, undef255, undef260, undef261, undef265, undef268, undef270, undef272, undef277, undef278, undef282, undef285, undef286, undef287, undef288, undef289, undef294, undef295, undef299, undef302, undef303, undef304, undef305, undef306, undef311, undef312, undef316, undef319, undef320, undef321, undef322, undef323, undef328, undef329, undef333, undef336, undef337, undef338, undef339, undef340, undef341, undef346, undef347, undef351, undef354, undef355, undef356, undef357, undef358, undef363, undef364, undef368, undef371, undef372, undef373, undef374, undef375, undef380, undef381, undef385, undef388, undef390, undef392, undef397, undef398, undef402, undef405, undef407, undef409, undef414, undef415, undef419, undef422, undef424, undef426, undef431, undef432, undef436, undef439, undef441, undef443, undef448, undef449, undef453, undef456, undef458, undef460, undef465, undef466, undef470, undef473, undef475, undef477, undef482, undef483, undef487, undef490, undef492, undef494, undef499, undef500, undef504, undef507, undef509, undef511, undef516, undef517, undef521, undef524, undef526, undef528, undef533, undef534, undef538, undef540, undef541, undef543, undef545, undef550, undef551, undef555, undef557, undef558, undef560, undef562, undef567, undef568, undef572, undef574, undef575, undef577, undef579, undef584, undef585, undef589, undef592, undef594, undef596, undef601, undef602, undef606, undef609, undef611, undef613, undef618, undef619, undef623, undef626, undef628, undef630, Abstraction variables: Exit nodes: Accepting locations: Asserts: ************************************************************* ******************************************************************************************* *********************** WORKING TRANSITION SYSTEM (DAG) *********************** ******************************************************************************************* Init Location: 0 Graph 0: Transitions: Variables: Graph 1: Transitions: 0, x^0 -> undef337, y^0 -> undef339, rest remain the same}> 0, x^0 -> undef355, y^0 -> undef357, rest remain the same}> 0, x^0 -> undef372, y^0 -> undef374, rest remain the same}> 0, x^0 -> undef337, y^0 -> undef339, rest remain the same}> 0, x^0 -> undef355, y^0 -> undef357, rest remain the same}> 0, x^0 -> undef372, y^0 -> undef374, rest remain the same}> 0, x^0 -> undef337, y^0 -> undef339, rest remain the same}> 0, x^0 -> undef355, y^0 -> undef357, rest remain the same}> 0, x^0 -> undef372, y^0 -> undef374, rest remain the same}> 0, x^0 -> undef337, y^0 -> undef339, rest remain the same}> 1, x^0 -> undef390, y^0 -> undef392, rest remain the same}> 1, x^0 -> undef407, y^0 -> undef409, rest remain the same}> 1, x^0 -> undef424, y^0 -> undef426, rest remain the same}> 1, x^0 -> undef390, y^0 -> undef392, rest remain the same}> undef407, y^0 -> undef409, rest remain the same}> undef424, y^0 -> undef426, rest remain the same}> 1, x^0 -> undef390, y^0 -> undef392, rest remain the same}> undef407, y^0 -> undef409, rest remain the same}> undef424, y^0 -> undef426, rest remain the same}> Variables: __const_7^0, __const_8^0, n0^0, n1^0, x^0, y^0, executed_Drive^0 Graph 2: Transitions: Variables: Precedence: Graph 0 Graph 1 1, x^0 -> undef543, y^0 -> undef545, rest remain the same}> 0, x^0 -> undef560, y^0 -> undef562, rest remain the same}> 0, x^0 -> undef577, y^0 -> undef579, rest remain the same}> Graph 2 1, x^0 -> undef594, y^0 -> undef596, rest remain the same}> 0, x^0 -> undef611, y^0 -> undef613, rest remain the same}> 0, x^0 -> undef628, y^0 -> undef630, rest remain the same}> 1, x^0 -> undef236, y^0 -> undef238, rest remain the same}> undef123, x^0 -> undef253, y^0 -> undef255, rest remain the same}> undef123, x^0 -> undef270, y^0 -> undef272, rest remain the same}> 1, x^0 -> undef286, y^0 -> undef288, rest remain the same}> undef123, x^0 -> undef303, y^0 -> undef305, rest remain the same}> undef123, x^0 -> undef320, y^0 -> undef322, rest remain the same}> 1, x^0 -> undef236, y^0 -> undef238, rest remain the same}> undef253, y^0 -> undef255, rest remain the same}> undef270, y^0 -> undef272, rest remain the same}> 1, x^0 -> undef286, y^0 -> undef288, rest remain the same}> undef303, y^0 -> undef305, rest remain the same}> undef320, y^0 -> undef322, rest remain the same}> 1, x^0 -> undef236, y^0 -> undef238, rest remain the same}> undef253, y^0 -> undef255, rest remain the same}> undef270, y^0 -> undef272, rest remain the same}> 1, x^0 -> undef286, y^0 -> undef288, rest remain the same}> undef303, y^0 -> undef305, rest remain the same}> undef320, y^0 -> undef322, rest remain the same}> 1, x^0 -> undef236, y^0 -> undef238, rest remain the same}> 0, x^0 -> undef253, y^0 -> undef255, rest remain the same}> 0, x^0 -> undef270, y^0 -> undef272, rest remain the same}> 1, x^0 -> undef286, y^0 -> undef288, rest remain the same}> 0, x^0 -> undef303, y^0 -> undef305, rest remain the same}> 0, x^0 -> undef320, y^0 -> undef322, rest remain the same}> 1, x^0 -> undef492, y^0 -> undef494, rest remain the same}> undef509, y^0 -> undef511, rest remain the same}> undef526, y^0 -> undef528, rest remain the same}> Map Locations to Subgraph: ( 0 , 0 ) ( 3 , 2 ) ( 4 , 1 ) ( 6 , 1 ) ******************************************************************************************* ******************************** CHECKING ASSERTIONS ******************************** ******************************************************************************************* Proving termination of subgraph 0 Proving termination of subgraph 1 Checking unfeasibility... Time used: 0.10302 Checking conditional termination of SCC {l4, l6}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.097465s Ranking function: -38 - 11*__const_7^0 + 27*n0^0 + 3*n1^0 - 23*x^0 - 3*y^0 New Graphs: Transitions: 0, x^0 -> undef355, y^0 -> undef357, rest remain the same}> 0, x^0 -> undef372, y^0 -> undef374, rest remain the same}> 0, x^0 -> undef337, y^0 -> undef339, rest remain the same}> 0, x^0 -> undef355, y^0 -> undef357, rest remain the same}> 0, x^0 -> undef372, y^0 -> undef374, rest remain the same}> 0, x^0 -> undef337, y^0 -> undef339, rest remain the same}> 0, x^0 -> undef355, y^0 -> undef357, rest remain the same}> 0, x^0 -> undef372, y^0 -> undef374, rest remain the same}> 0, x^0 -> undef337, y^0 -> undef339, rest remain the same}> 1, x^0 -> undef390, y^0 -> undef392, rest remain the same}> 1, x^0 -> undef407, y^0 -> undef409, rest remain the same}> 1, x^0 -> undef424, y^0 -> undef426, rest remain the same}> 1, x^0 -> undef390, y^0 -> undef392, rest remain the same}> undef407, y^0 -> undef409, rest remain the same}> undef424, y^0 -> undef426, rest remain the same}> 1, x^0 -> undef390, y^0 -> undef392, rest remain the same}> undef407, y^0 -> undef409, rest remain the same}> undef424, y^0 -> undef426, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4, l6}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.049747s Ranking function: -220 - 49*__const_7^0 + 3*n0^0 + 205*n1^0 - 3*x^0 - 205*y^0 New Graphs: Transitions: 0, x^0 -> undef337, y^0 -> undef339, rest remain the same}> 0, x^0 -> undef355, y^0 -> undef357, rest remain the same}> 0, x^0 -> undef372, y^0 -> undef374, rest remain the same}> 0, x^0 -> undef355, y^0 -> undef357, rest remain the same}> 0, x^0 -> undef372, y^0 -> undef374, rest remain the same}> 0, x^0 -> undef337, y^0 -> undef339, rest remain the same}> 1, x^0 -> undef390, y^0 -> undef392, rest remain the same}> 1, x^0 -> undef407, y^0 -> undef409, rest remain the same}> 1, x^0 -> undef424, y^0 -> undef426, rest remain the same}> 1, x^0 -> undef390, y^0 -> undef392, rest remain the same}> undef407, y^0 -> undef409, rest remain the same}> undef424, y^0 -> undef426, rest remain the same}> 1, x^0 -> undef390, y^0 -> undef392, rest remain the same}> undef407, y^0 -> undef409, rest remain the same}> undef424, y^0 -> undef426, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4, l6}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.035729s Ranking function: -75 - __const_7^0 + __const_8^0 + 3*n0^0 + 34*n1^0 - 3*x^0 - 34*y^0 New Graphs: Transitions: 1, x^0 -> undef390, y^0 -> undef392, rest remain the same}> 1, x^0 -> undef407, y^0 -> undef409, rest remain the same}> 1, x^0 -> undef424, y^0 -> undef426, rest remain the same}> 1, x^0 -> undef390, y^0 -> undef392, rest remain the same}> 0, x^0 -> undef407, y^0 -> undef409, rest remain the same}> 0, x^0 -> undef424, y^0 -> undef426, rest remain the same}> 1, x^0 -> undef390, y^0 -> undef392, rest remain the same}> 0, x^0 -> undef407, y^0 -> undef409, rest remain the same}> 0, x^0 -> undef424, y^0 -> undef426, rest remain the same}> 1, x^0 -> undef390, y^0 -> undef392, rest remain the same}> 1, x^0 -> undef407, y^0 -> undef409, rest remain the same}> 1, x^0 -> undef424, y^0 -> undef426, rest remain the same}> 1, x^0 -> undef390, y^0 -> undef392, rest remain the same}> 0, x^0 -> undef407, y^0 -> undef409, rest remain the same}> 0, x^0 -> undef424, y^0 -> undef426, rest remain the same}> 1, x^0 -> undef390, y^0 -> undef392, rest remain the same}> 0, x^0 -> undef407, y^0 -> undef409, rest remain the same}> 0, x^0 -> undef424, y^0 -> undef426, rest remain the same}> 1, x^0 -> undef390, y^0 -> undef392, rest remain the same}> 1, x^0 -> undef407, y^0 -> undef409, rest remain the same}> 1, x^0 -> undef424, y^0 -> undef426, rest remain the same}> 1, x^0 -> undef390, y^0 -> undef392, rest remain the same}> 0, x^0 -> undef407, y^0 -> undef409, rest remain the same}> 0, x^0 -> undef424, y^0 -> undef426, rest remain the same}> 1, x^0 -> undef390, y^0 -> undef392, rest remain the same}> 0, x^0 -> undef407, y^0 -> undef409, rest remain the same}> 0, x^0 -> undef424, y^0 -> undef426, rest remain the same}> 1, x^0 -> undef390, y^0 -> undef392, rest remain the same}> 1, x^0 -> undef407, y^0 -> undef409, rest remain the same}> 1, x^0 -> undef424, y^0 -> undef426, rest remain the same}> 1, x^0 -> undef390, y^0 -> undef392, rest remain the same}> 0, x^0 -> undef407, y^0 -> undef409, rest remain the same}> 0, x^0 -> undef424, y^0 -> undef426, rest remain the same}> 1, x^0 -> undef390, y^0 -> undef392, rest remain the same}> 0, x^0 -> undef407, y^0 -> undef409, rest remain the same}> 0, x^0 -> undef424, y^0 -> undef426, rest remain the same}> 1, x^0 -> undef390, y^0 -> undef392, rest remain the same}> 1, x^0 -> undef407, y^0 -> undef409, rest remain the same}> 1, x^0 -> undef424, y^0 -> undef426, rest remain the same}> 1, x^0 -> undef390, y^0 -> undef392, rest remain the same}> 0, x^0 -> undef407, y^0 -> undef409, rest remain the same}> 0, x^0 -> undef424, y^0 -> undef426, rest remain the same}> 1, x^0 -> undef390, y^0 -> undef392, rest remain the same}> 0, x^0 -> undef407, y^0 -> undef409, rest remain the same}> 0, x^0 -> undef424, y^0 -> undef426, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.630012s Ranking function: -203 - 4*__const_7^0 + (71 / 2)*__const_8^0 + 5*n0^0 + 5*n1^0 - 5*x^0 - 5*y^0 New Graphs: Transitions: 0, x^0 -> undef407, y^0 -> undef409, rest remain the same}> 0, x^0 -> undef424, y^0 -> undef426, rest remain the same}> 0, x^0 -> undef407, y^0 -> undef409, rest remain the same}> 0, x^0 -> undef424, y^0 -> undef426, rest remain the same}> 0, x^0 -> undef407, y^0 -> undef409, rest remain the same}> 0, x^0 -> undef424, y^0 -> undef426, rest remain the same}> 0, x^0 -> undef407, y^0 -> undef409, rest remain the same}> 0, x^0 -> undef424, y^0 -> undef426, rest remain the same}> 0, x^0 -> undef407, y^0 -> undef409, rest remain the same}> 0, x^0 -> undef424, y^0 -> undef426, rest remain the same}> 0, x^0 -> undef407, y^0 -> undef409, rest remain the same}> 0, x^0 -> undef424, y^0 -> undef426, rest remain the same}> 1, x^0 -> undef390, y^0 -> undef392, rest remain the same}> 1, x^0 -> undef424, y^0 -> undef426, rest remain the same}> 0, x^0 -> undef407, y^0 -> undef409, rest remain the same}> 0, x^0 -> undef424, y^0 -> undef426, rest remain the same}> 1, x^0 -> undef390, y^0 -> undef392, rest remain the same}> 0, x^0 -> undef407, y^0 -> undef409, rest remain the same}> 0, x^0 -> undef424, y^0 -> undef426, rest remain the same}> 1, x^0 -> undef390, y^0 -> undef392, rest remain the same}> 1, x^0 -> undef407, y^0 -> undef409, rest remain the same}> 1, x^0 -> undef424, y^0 -> undef426, rest remain the same}> 1, x^0 -> undef390, y^0 -> undef392, rest remain the same}> 0, x^0 -> undef407, y^0 -> undef409, rest remain the same}> 0, x^0 -> undef424, y^0 -> undef426, rest remain the same}> 1, x^0 -> undef390, y^0 -> undef392, rest remain the same}> 0, x^0 -> undef407, y^0 -> undef409, rest remain the same}> 0, x^0 -> undef424, y^0 -> undef426, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.227766s Ranking function: (~(447) / 2) + (~(61) / 2)*__const_7^0 + 61*__const_8^0 + 5*n0^0 + 5*n1^0 - 5*x^0 - 5*y^0 New Graphs: Transitions: 0, x^0 -> undef407, y^0 -> undef409, rest remain the same}> 0, x^0 -> undef424, y^0 -> undef426, rest remain the same}> 0, x^0 -> undef407, y^0 -> undef409, rest remain the same}> 0, x^0 -> undef424, y^0 -> undef426, rest remain the same}> 0, x^0 -> undef407, y^0 -> undef409, rest remain the same}> 0, x^0 -> undef424, y^0 -> undef426, rest remain the same}> 0, x^0 -> undef407, y^0 -> undef409, rest remain the same}> 0, x^0 -> undef424, y^0 -> undef426, rest remain the same}> 0, x^0 -> undef407, y^0 -> undef409, rest remain the same}> 0, x^0 -> undef424, y^0 -> undef426, rest remain the same}> 0, x^0 -> undef407, y^0 -> undef409, rest remain the same}> 0, x^0 -> undef424, y^0 -> undef426, rest remain the same}> 0, x^0 -> undef407, y^0 -> undef409, rest remain the same}> 0, x^0 -> undef424, y^0 -> undef426, rest remain the same}> 0, x^0 -> undef407, y^0 -> undef409, rest remain the same}> 0, x^0 -> undef424, y^0 -> undef426, rest remain the same}> 1, x^0 -> undef390, y^0 -> undef392, rest remain the same}> 1, x^0 -> undef407, y^0 -> undef409, rest remain the same}> 1, x^0 -> undef424, y^0 -> undef426, rest remain the same}> 1, x^0 -> undef390, y^0 -> undef392, rest remain the same}> 0, x^0 -> undef407, y^0 -> undef409, rest remain the same}> 0, x^0 -> undef424, y^0 -> undef426, rest remain the same}> 1, x^0 -> undef390, y^0 -> undef392, rest remain the same}> 0, x^0 -> undef407, y^0 -> undef409, rest remain the same}> 0, x^0 -> undef424, y^0 -> undef426, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.115302s Ranking function: -10 + 5*n0^0 + 5*n1^0 - 5*x^0 - 5*y^0 New Graphs: Transitions: 0, x^0 -> undef407, y^0 -> undef409, rest remain the same}> 0, x^0 -> undef424, y^0 -> undef426, rest remain the same}> 0, x^0 -> undef407, y^0 -> undef409, rest remain the same}> 0, x^0 -> undef424, y^0 -> undef426, rest remain the same}> 0, x^0 -> undef407, y^0 -> undef409, rest remain the same}> 0, x^0 -> undef424, y^0 -> undef426, rest remain the same}> 0, x^0 -> undef407, y^0 -> undef409, rest remain the same}> 0, x^0 -> undef424, y^0 -> undef426, rest remain the same}> 0, x^0 -> undef407, y^0 -> undef409, rest remain the same}> 0, x^0 -> undef424, y^0 -> undef426, rest remain the same}> 0, x^0 -> undef407, y^0 -> undef409, rest remain the same}> 0, x^0 -> undef424, y^0 -> undef426, rest remain the same}> 0, x^0 -> undef407, y^0 -> undef409, rest remain the same}> 0, x^0 -> undef424, y^0 -> undef426, rest remain the same}> 0, x^0 -> undef407, y^0 -> undef409, rest remain the same}> 0, x^0 -> undef424, y^0 -> undef426, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.063152s Ranking function: -194 + (61 / 2)*__const_8^0 + executed_Drive^0 + 5*n0^0 + 5*n1^0 - 5*x^0 - 5*y^0 New Graphs: Transitions: 0, x^0 -> undef424, y^0 -> undef426, rest remain the same}> Variables: __const_7^0, __const_8^0, executed_Drive^0, n0^0, n1^0, x^0, y^0 Checking conditional termination of SCC {l4}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.005892s Ranking function: -1 + executed_Drive^0 New Graphs: Proving termination of subgraph 2 Analyzing SCC {l3}... No cycles found. Program Terminates