YES

Solver Timeout: 4
Global Timeout: 300
No parsing errors!
Init Location: 0
Transitions:
<l0, l67, true>
<l1, l2, (0 <= (0 + a_237^0)) /\ (undef61 = undef61) /\ ((0 + y_19^0) <= (0 + x_20^0)) /\ ((0 + x_20^0) <= (0 + y_19^0)) /\ (undef74 = undef74) /\ (undef75 = undef75) /\ (undef73 = undef73) /\ (undef72 = undef72) /\ (undef71 = undef71) /\ (undef67 = undef67) /\ (undef38 = undef38) /\ (undef69 = undef69) /\ (undef70 = undef70) /\ (undef68 = undef68) /\ (undef62 = undef62) /\ (1 <= (0 + undef61)) /\ (2 <= (0 + undef61)), par{ct_17^0 -> undef38, result_11^0 -> (0 + temp0_15^0), result_dot_nondet_sdv_special_RETURN_VALUE_13^0 -> undef61, t_23^0 -> undef62, x_16^0 -> undef67, x_20^0 -> undef68, x_SLAM_f_18^0 -> undef69, y_19^0 -> undef70}>
<l1, l3, (0 <= (0 + a_237^0)) /\ (undef136 = undef136) /\ (undef116 = undef116) /\ (undef142 = undef142) /\ (undef113 = undef113) /\ (undef144 = undef144) /\ (undef131 = undef131), par{ct_17^0 -> undef113, head_14^0 -> undef116, r_39^0 -> undef131, result_dot_nondet_sdv_special_RETURN_VALUE_13^0 -> undef136, x_16^0 -> undef142, x_SLAM_f_18^0 -> undef144}>
<l3, l4, (undef146 = __disjvr_0^0) /\ (__disjvr_0^0 = undef146), par{__disjvr_0^0 -> undef146}>
<l4, l5, (undef252 = undef252) /\ (0 <= (0 + ct_17^0)) /\ ((0 + ct_17^0) <= 0) /\ (0 <= (0 + y_19^0)) /\ ((0 + y_19^0) <= 0) /\ ((0 + head_14^0) <= (0 + x_16^0)) /\ ((0 + x_16^0) <= (0 + head_14^0)) /\ ((0 + head_14^0) <= (0 + x_SLAM_f_18^0)) /\ ((0 + x_SLAM_f_18^0) <= (0 + head_14^0)) /\ ((0 + x_16^0) <= (0 + x_SLAM_f_18^0)) /\ ((0 + x_SLAM_f_18^0) <= (0 + x_16^0)) /\ ((0 + ct_17^0) <= (0 + y_19^0)) /\ ((0 + y_19^0) <= (0 + ct_17^0)) /\ ((0 + undef252) <= (~(1) + a_237^0)) /\ ((~(1) + a_237^0) <= (0 + undef252)), par{a_260^0 -> undef252, t_23^0 -> (0 + x_20^0)}>
<l5, l6, (undef297 = __disjvr_1^0) /\ (__disjvr_1^0 = undef297), par{__disjvr_1^0 -> undef297}>
<l6, l7, (undef378 = __disjvr_2^0) /\ (__disjvr_2^0 = undef378), par{__disjvr_2^0 -> undef378}>
<l7, l8, (undef450 = __disjvr_3^0) /\ (__disjvr_3^0 = undef450), par{__disjvr_3^0 -> undef450}>
<l8, l9, (1 <= (0 + result_dot_nondet_sdv_special_RETURN_VALUE_13^0)) /\ (2 <= (0 + result_dot_nondet_sdv_special_RETURN_VALUE_13^0)) /\ (undef531 = undef531) /\ ((0 + undef531) <= (0 + a_260^0)) /\ ((0 + a_260^0) <= (0 + undef531)), par{a_237^0 -> undef531}>
<l9, l1, true>
<l10, l11, (0 <= (0 + a_215^0)) /\ (undef696 = undef696) /\ (undef676 = undef676) /\ ((0 + y_19^0) <= (0 + x_20^0)) /\ ((0 + x_20^0) <= (0 + y_19^0)) /\ (undef709 = undef709) /\ (undef710 = undef710) /\ (undef708 = undef708) /\ (undef707 = undef707) /\ (undef706 = undef706) /\ (undef702 = undef702) /\ (undef673 = undef673) /\ (undef704 = undef704) /\ (undef705 = undef705) /\ (undef703 = undef703) /\ (undef697 = undef697), par{ct_17^0 -> undef673, head_14^0 -> undef676, result_11^0 -> (0 + temp0_15^0), result_dot_nondet_sdv_special_RETURN_VALUE_13^0 -> undef696, t_23^0 -> undef697, x_16^0 -> undef702, x_20^0 -> undef703, x_SLAM_f_18^0 -> undef704, y_19^0 -> undef705}>
<l11, l12, (undef736 = __disjvr_4^0) /\ (__disjvr_4^0 = undef736), par{__disjvr_4^0 -> undef736}>
<l12, l2, (1 <= (0 + result_dot_nondet_sdv_special_RETURN_VALUE_13^0)) /\ (2 <= (0 + result_dot_nondet_sdv_special_RETURN_VALUE_13^0))>
<l10, l13, (0 <= (0 + a_215^0)) /\ (undef911 = undef911) /\ (undef891 = undef891) /\ (undef917 = undef917) /\ (undef888 = undef888) /\ (undef919 = undef919), par{ct_17^0 -> undef888, head_14^0 -> undef891, result_dot_nondet_sdv_special_RETURN_VALUE_13^0 -> undef911, x_16^0 -> undef917, x_SLAM_f_18^0 -> undef919}>
<l13, l14, (undef947 = __disjvr_5^0) /\ (__disjvr_5^0 = undef947), par{__disjvr_5^0 -> undef947}>
<l14, l15, (0 <= (0 + ct_17^0)) /\ ((0 + ct_17^0) <= 0) /\ (0 <= (0 + y_19^0)) /\ ((0 + y_19^0) <= 0) /\ ((0 + head_14^0) <= (0 + x_16^0)) /\ ((0 + x_16^0) <= (0 + head_14^0)) /\ ((0 + head_14^0) <= (0 + x_SLAM_f_18^0)) /\ ((0 + x_SLAM_f_18^0) <= (0 + head_14^0)) /\ ((0 + x_16^0) <= (0 + x_SLAM_f_18^0)) /\ ((0 + x_SLAM_f_18^0) <= (0 + x_16^0)) /\ ((0 + ct_17^0) <= (0 + y_19^0)) /\ ((0 + y_19^0) <= (0 + ct_17^0)), par{t_23^0 -> (0 + x_20^0)}>
<l15, l16, (undef1088 = __disjvr_6^0) /\ (__disjvr_6^0 = undef1088), par{__disjvr_6^0 -> undef1088}>
<l16, l17, (undef1159 = __disjvr_7^0) /\ (__disjvr_7^0 = undef1159), par{__disjvr_7^0 -> undef1159}>
<l17, l18, (undef1230 = __disjvr_8^0) /\ (__disjvr_8^0 = undef1230), par{__disjvr_8^0 -> undef1230}>
<l18, l1, (1 <= (0 + result_dot_nondet_sdv_special_RETURN_VALUE_13^0)) /\ (2 <= (0 + result_dot_nondet_sdv_special_RETURN_VALUE_13^0))>
<l19, l20, (0 <= (0 + len_132^0)) /\ (undef1401 = undef1401) /\ (undef1381 = undef1381) /\ (undef1407 = undef1407) /\ (undef1378 = undef1378) /\ (undef1409 = undef1409), par{ct_17^0 -> undef1378, head_14^0 -> undef1381, result_dot_nondet_sdv_special_RETURN_VALUE_13^0 -> undef1401, x_16^0 -> undef1407, x_SLAM_f_18^0 -> undef1409}>
<l20, l21, (undef1441 = __disjvr_9^0) /\ (__disjvr_9^0 = undef1441), par{__disjvr_9^0 -> undef1441}>
<l21, l22, (undef1542 = (0 + x_20^0)) /\ (undef1515 = undef1515) /\ (0 <= (0 + ct_17^0)) /\ ((0 + ct_17^0) <= 0) /\ (0 <= (0 + y_19^0)) /\ ((0 + y_19^0) <= 0) /\ (0 <= ((0 + (~(1) * undef1515)) + a_237^0)) /\ (((0 + (~(1) * undef1515)) + a_237^0) <= 0) /\ ((0 + head_14^0) <= (0 + x_16^0)) /\ ((0 + x_16^0) <= (0 + head_14^0)) /\ ((0 + head_14^0) <= (0 + x_SLAM_f_18^0)) /\ ((0 + x_SLAM_f_18^0) <= (0 + head_14^0)) /\ ((0 + head_14^0) <= (0 + undef1542)) /\ ((0 + undef1542) <= (0 + head_14^0)) /\ ((0 + x_16^0) <= (0 + x_SLAM_f_18^0)) /\ ((0 + x_SLAM_f_18^0) <= (0 + x_16^0)) /\ ((0 + ct_17^0) <= (0 + y_19^0)) /\ ((0 + y_19^0) <= (0 + ct_17^0)) /\ ((0 + undef1515) <= (0 + a_237^0)) /\ ((0 + a_237^0) <= (0 + undef1515)), par{a_215^0 -> undef1515, t_23^0 -> undef1542}>
<l22, l23, (undef1552 = __disjvr_10^0) /\ (__disjvr_10^0 = undef1552), par{__disjvr_10^0 -> undef1552}>
<l23, l24, (undef1623 = __disjvr_11^0) /\ (__disjvr_11^0 = undef1623), par{__disjvr_11^0 -> undef1623}>
<l24, l25, (undef1694 = __disjvr_12^0) /\ (__disjvr_12^0 = undef1694), par{__disjvr_12^0 -> undef1694}>
<l25, l1, (1 <= (0 + result_dot_nondet_sdv_special_RETURN_VALUE_13^0)) /\ (2 <= (0 + result_dot_nondet_sdv_special_RETURN_VALUE_13^0)) /\ (undef1810 = undef1810) /\ ((~(1) + undef1810) <= (0 + a_215^0)) /\ ((0 + a_215^0) <= (~(1) + undef1810)), par{len_132^0 -> undef1810}>
<l26, l27, (undef1904 = undef1904) /\ ((0 + length_29^0) <= (0 + i_30^0)) /\ (undef1905 = (0 + head_32^0)) /\ (undef1903 = (0 + undef1905)) /\ (undef1882 = undef1882) /\ (undef1878 = undef1878) /\ (undef1894 = undef1894) /\ (undef1874 = undef1874) /\ (undef1890 = undef1890) /\ (undef1896 = undef1896) /\ (undef1895 = undef1895) /\ (undef1901 = (0 + undef1903)) /\ (undef1889 = undef1889) /\ (undef1902 = (0 + undef1901)) /\ (undef1873 = (0 + undef1902)) /\ (1 <= (0 + undef1904)) /\ ((0 + undef1904) <= 1) /\ ((0 + undef1901) <= (0 + undef1902)) /\ ((0 + undef1902) <= (0 + undef1901)) /\ ((0 + undef1901) <= (0 + undef1873)) /\ ((0 + undef1873) <= (0 + undef1901)) /\ ((0 + undef1902) <= (0 + undef1873)) /\ ((0 + undef1873) <= (0 + undef1902)) /\ (1 <= (0 + undef1904)) /\ ((0 + undef1904) <= 1) /\ (undef1891 = undef1891) /\ (undef1871 = undef1871) /\ (undef1875 = undef1875), par{head_14^0 -> undef1871, head_27^0 -> undef1873, head_32^0 -> undef1874, head_SLAM_f_26^0 -> undef1875, i_30^0 -> undef1878, length_29^0 -> undef1882, result_11^0 -> undef1889, result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33^0 -> undef1890, result_dot_nondet_sdv_special_RETURN_VALUE_13^0 -> undef1891, temp0_31^0 -> undef1894, temp_35^0 -> undef1895, tmp_34^0 -> undef1896}>
<l27, l28, (undef1910 = __disjvr_13^0) /\ (__disjvr_13^0 = undef1910), par{__disjvr_13^0 -> undef1910}>
<l28, l29, (0 <= (0 + head_27^0)) /\ ((0 + head_27^0) <= 0) /\ (1 <= (0 + result_dot_nondet_sdv_special_RETURN_VALUE_13^0)) /\ ((0 + result_dot_nondet_sdv_special_RETURN_VALUE_13^0) <= 1) /\ ((0 + head_14^0) <= (0 + head_SLAM_f_26^0)) /\ ((0 + head_SLAM_f_26^0) <= (0 + head_14^0))>
<l29, l30, (undef2051 = __disjvr_14^0) /\ (__disjvr_14^0 = undef2051), par{__disjvr_14^0 -> undef2051}>
<l30, l31, (1 <= (0 + result_dot_nondet_sdv_special_RETURN_VALUE_13^0)) /\ ((0 + result_dot_nondet_sdv_special_RETURN_VALUE_13^0) <= 1) /\ (undef2176 = undef2176) /\ (0 <= (0 + head_27^0)) /\ ((0 + head_27^0) <= 0) /\ (undef2160 = undef2160) /\ (undef2158 = undef2158) /\ (undef2182 = (0 + head_14^0)) /\ (undef2153 = 0) /\ (undef2184 = (0 + undef2182)) /\ (undef2185 = (0 + undef2153)) /\ (undef2183 = (0 + undef2184)) /\ (0 <= (0 + undef2153)) /\ ((0 + undef2153) <= 0) /\ (0 <= (0 + undef2185)) /\ ((0 + undef2185) <= 0) /\ (1 <= (0 + undef2176)) /\ ((0 + undef2176) <= 1) /\ ((0 + head_14^0) <= (0 + undef2182)) /\ ((0 + undef2182) <= (0 + head_14^0)) /\ ((0 + head_14^0) <= (0 + undef2184)) /\ ((0 + undef2184) <= (0 + head_14^0)) /\ ((0 + head_14^0) <= (0 + undef2183)) /\ ((0 + undef2183) <= (0 + head_14^0)) /\ ((0 + undef2182) <= (0 + undef2184)) /\ ((0 + undef2184) <= (0 + undef2182)) /\ ((0 + undef2153) <= (0 + undef2185)) /\ ((0 + undef2185) <= (0 + undef2153)) /\ ((0 + undef2184) <= (0 + undef2183)) /\ ((0 + undef2183) <= (0 + undef2184)), par{ct_17^0 -> undef2153, head_27^0 -> undef2158, head_SLAM_f_26^0 -> undef2160, result_dot_nondet_sdv_special_RETURN_VALUE_13^0 -> undef2176, x_16^0 -> undef2182, x_20^0 -> undef2183, x_SLAM_f_18^0 -> undef2184, y_19^0 -> undef2185}>
<l31, l32, (undef2192 = __disjvr_15^0) /\ (__disjvr_15^0 = undef2192), par{__disjvr_15^0 -> undef2192}>
<l32, l33, (1 <= (0 + result_dot_nondet_sdv_special_RETURN_VALUE_13^0)) /\ ((0 + result_dot_nondet_sdv_special_RETURN_VALUE_13^0) <= 1) /\ (undef2316 = undef2316) /\ (undef2296 = undef2296) /\ (undef2322 = undef2322) /\ (undef2293 = undef2293) /\ (undef2324 = undef2324), par{ct_17^0 -> undef2293, head_14^0 -> undef2296, result_dot_nondet_sdv_special_RETURN_VALUE_13^0 -> undef2316, x_16^0 -> undef2322, x_SLAM_f_18^0 -> undef2324}>
<l33, l34, (undef2333 = __disjvr_16^0) /\ (__disjvr_16^0 = undef2333), par{__disjvr_16^0 -> undef2333}>
<l34, l35, (undef2457 = (0 + x_20^0)) /\ (0 <= (0 + ct_17^0)) /\ ((0 + ct_17^0) <= 0) /\ (0 <= (0 + y_19^0)) /\ ((0 + y_19^0) <= 0) /\ (0 <= (0 + x_20^0)) /\ ((0 + x_20^0) <= 0) /\ (1 <= (0 + result_dot_nondet_sdv_special_RETURN_VALUE_13^0)) /\ ((0 + result_dot_nondet_sdv_special_RETURN_VALUE_13^0) <= 1) /\ ((0 + head_14^0) <= (0 + x_16^0)) /\ ((0 + x_16^0) <= (0 + head_14^0)) /\ ((0 + head_14^0) <= (0 + x_SLAM_f_18^0)) /\ ((0 + x_SLAM_f_18^0) <= (0 + head_14^0)) /\ ((0 + head_14^0) <= (0 + undef2457)) /\ ((0 + undef2457) <= (0 + head_14^0)) /\ ((0 + x_16^0) <= (0 + x_SLAM_f_18^0)) /\ ((0 + x_SLAM_f_18^0) <= (0 + x_16^0)) /\ ((0 + ct_17^0) <= (0 + y_19^0)) /\ ((0 + y_19^0) <= (0 + ct_17^0)), par{t_23^0 -> undef2457}>
<l35, l36, (undef2474 = __disjvr_17^0) /\ (__disjvr_17^0 = undef2474), par{__disjvr_17^0 -> undef2474}>
<l36, l37, (undef2545 = __disjvr_18^0) /\ (__disjvr_18^0 = undef2545), par{__disjvr_18^0 -> undef2545}>
<l37, l38, (1 <= (0 + result_dot_nondet_sdv_special_RETURN_VALUE_13^0)) /\ ((0 + result_dot_nondet_sdv_special_RETURN_VALUE_13^0) <= 1) /\ (undef2646 = undef2646) /\ ((0 + y_19^0) <= (0 + x_20^0)) /\ ((0 + x_20^0) <= (0 + y_19^0)) /\ (undef2679 = undef2679) /\ (undef2680 = undef2680) /\ (undef2678 = undef2678) /\ (undef2677 = undef2677) /\ (undef2676 = undef2676) /\ (undef2672 = undef2672) /\ (undef2643 = undef2643) /\ (undef2674 = undef2674) /\ (undef2675 = undef2675) /\ (undef2673 = undef2673) /\ (undef2667 = undef2667), par{ct_17^0 -> undef2643, head_14^0 -> undef2646, result_11^0 -> (0 + temp0_15^0), t_23^0 -> undef2667, x_16^0 -> undef2672, x_20^0 -> undef2673, x_SLAM_f_18^0 -> undef2674, y_19^0 -> undef2675}>
<l38, l2, (undef2691 = __disjvr_19^0) /\ (__disjvr_19^0 = undef2691), par{__disjvr_19^0 -> undef2691}>
<l26, l39, (undef2811 = undef2811) /\ (undef2810 = undef2810) /\ (undef2807 = undef2807) /\ ((1 + i_30^0) <= (0 + length_29^0)) /\ (undef2816 = (0 + temp_35^0)) /\ (undef2815 = undef2815) /\ (undef2794 = (0 + undef2816)) /\ (undef2798 = (1 + i_30^0)) /\ (2 <= (0 + undef2798)) /\ ((0 + undef2798) <= 2) /\ ((0 + undef2811) <= (0 + length_29^0)) /\ ((0 + length_29^0) <= (0 + undef2811)) /\ ((0 + undef2794) <= (0 + undef2810)) /\ ((0 + undef2810) <= (0 + undef2794)) /\ ((0 + undef2794) <= (0 + undef2816)) /\ ((0 + undef2816) <= (0 + undef2794)) /\ ((0 + undef2810) <= (0 + undef2816)) /\ ((0 + undef2816) <= (0 + undef2810)) /\ (1 <= (0 + length_29^0)) /\ (2 <= (0 + length_29^0)), par{head_32^0 -> undef2794, i_30^0 -> undef2798, rcd_58^0 -> undef2807, result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33^0 -> undef2810, result_dot_nondet_sdv_special_RETURN_VALUE_13^0 -> undef2811, temp_35^0 -> undef2815, tmp_34^0 -> undef2816}>
<l40, l41, (undef2891 = undef2891) /\ (undef2881 = (0 + undef2891)) /\ (undef2873 = undef2873) /\ (undef2872 = (0 + undef2881)) /\ (undef2864 = 0) /\ (undef2868 = 0) /\ (0 <= (0 + undef2868)) /\ ((0 + undef2868) <= 0) /\ (0 <= (0 + undef2864)) /\ ((0 + undef2864) <= 0) /\ ((0 + undef2881) <= (0 + undef2872)) /\ ((0 + undef2872) <= (0 + undef2881)), par{head_32^0 -> undef2864, i_30^0 -> undef2868, length_29^0 -> undef2872, nondet_12^0 -> undef2873, result_dot_nondet_sdv_special_RETURN_VALUE_13^0 -> undef2881}>
<l42, l43, (0 <= (0 + len_132^0)) /\ (0 <= (0 + a_147^0)) /\ (undef2952 = undef2952) /\ (0 <= (0 + head_27^0)) /\ ((0 + head_27^0) <= 0) /\ (undef2936 = undef2936) /\ (undef2934 = undef2934) /\ (undef2958 = (0 + head_14^0)) /\ (undef2929 = 0) /\ (undef2960 = (0 + undef2958)) /\ (undef2961 = (0 + undef2929)) /\ (undef2959 = (0 + undef2960)) /\ (0 <= (0 + undef2929)) /\ ((0 + undef2929) <= 0) /\ (0 <= (0 + undef2961)) /\ ((0 + undef2961) <= 0) /\ ((0 + head_14^0) <= (0 + undef2958)) /\ ((0 + undef2958) <= (0 + head_14^0)) /\ ((0 + head_14^0) <= (0 + undef2960)) /\ ((0 + undef2960) <= (0 + head_14^0)) /\ ((0 + head_14^0) <= (0 + undef2959)) /\ ((0 + undef2959) <= (0 + head_14^0)) /\ ((0 + undef2958) <= (0 + undef2960)) /\ ((0 + undef2960) <= (0 + undef2958)) /\ ((0 + undef2929) <= (0 + undef2961)) /\ ((0 + undef2961) <= (0 + undef2929)) /\ ((0 + undef2960) <= (0 + undef2959)) /\ ((0 + undef2959) <= (0 + undef2960)), par{ct_17^0 -> undef2929, head_27^0 -> undef2934, head_SLAM_f_26^0 -> undef2936, result_dot_nondet_sdv_special_RETURN_VALUE_13^0 -> undef2952, x_16^0 -> undef2958, x_20^0 -> undef2959, x_SLAM_f_18^0 -> undef2960, y_19^0 -> undef2961}>
<l43, l44, (undef2974 = __disjvr_20^0) /\ (__disjvr_20^0 = undef2974), par{__disjvr_20^0 -> undef2974}>
<l44, l19, (1 <= (0 + result_dot_nondet_sdv_special_RETURN_VALUE_13^0)) /\ (2 <= (0 + result_dot_nondet_sdv_special_RETURN_VALUE_13^0))>
<l42, l45, (0 <= (0 + len_132^0)) /\ (0 <= (0 + a_147^0)) /\ (undef3162 = undef3162) /\ (undef3142 = undef3142) /\ (undef3146 = undef3146) /\ (undef3157 = undef3157) /\ (undef3140 = undef3140) /\ (undef3143 = undef3143), par{f_170^0 -> undef3140, head_14^0 -> undef3142, head_175^0 -> undef3143, head_SLAM_f_26^0 -> undef3146, r_39^0 -> undef3157, result_dot_nondet_sdv_special_RETURN_VALUE_13^0 -> undef3162}>
<l45, l46, (undef3185 = __disjvr_21^0) /\ (__disjvr_21^0 = undef3185), par{__disjvr_21^0 -> undef3185}>
<l46, l47, (undef3292 = undef3292) /\ (undef3275 = undef3275) /\ (1 <= ((0 + (~(1) * len_132^0)) + undef3292)) /\ (((0 + (~(1) * len_132^0)) + undef3292) <= 1) /\ ((0 + head_14^0) <= (0 + head_SLAM_f_26^0)) /\ ((0 + head_SLAM_f_26^0) <= (0 + head_14^0)) /\ ((0 + head_27^0) <= (0 + f_170^0)) /\ ((0 + f_170^0) <= (0 + head_27^0)) /\ ((0 + undef3275) <= (~(1) + a_147^0)) /\ ((~(1) + a_147^0) <= (0 + undef3275)), par{a_184^0 -> undef3275, len_183^0 -> undef3292}>
<l47, l48, (undef3326 = __disjvr_22^0) /\ (__disjvr_22^0 = undef3326), par{__disjvr_22^0 -> undef3326}>
<l48, l49, (undef3397 = __disjvr_23^0) /\ (__disjvr_23^0 = undef3397), par{__disjvr_23^0 -> undef3397}>
<l49, l50, (1 <= (0 + result_dot_nondet_sdv_special_RETURN_VALUE_13^0)) /\ (2 <= (0 + result_dot_nondet_sdv_special_RETURN_VALUE_13^0)) /\ (undef3484 = undef3484) /\ ((0 + undef3484) <= (0 + a_184^0)) /\ ((0 + a_184^0) <= (0 + undef3484)) /\ (undef3501 = undef3501) /\ ((0 + undef3501) <= (0 + len_183^0)) /\ ((0 + len_183^0) <= (0 + undef3501)), par{a_147^0 -> undef3484, len_132^0 -> undef3501}>
<l50, l42, true>
<l51, l52, (0 <= (0 + a_116^0)) /\ (undef3652 = undef3652) /\ (0 <= (0 + head_27^0)) /\ ((0 + head_27^0) <= 0) /\ (undef3636 = undef3636) /\ (undef3634 = undef3634) /\ (undef3658 = (0 + head_14^0)) /\ (undef3629 = 0) /\ (undef3660 = (0 + undef3658)) /\ (undef3661 = (0 + undef3629)) /\ (undef3659 = (0 + undef3660)) /\ (0 <= (0 + undef3629)) /\ ((0 + undef3629) <= 0) /\ (0 <= (0 + undef3661)) /\ ((0 + undef3661) <= 0) /\ (1 <= (0 + len_132^0)) /\ ((0 + len_132^0) <= 1) /\ ((0 + head_14^0) <= (0 + undef3658)) /\ ((0 + undef3658) <= (0 + head_14^0)) /\ ((0 + head_14^0) <= (0 + undef3660)) /\ ((0 + undef3660) <= (0 + head_14^0)) /\ ((0 + head_14^0) <= (0 + undef3659)) /\ ((0 + undef3659) <= (0 + head_14^0)) /\ ((0 + undef3658) <= (0 + undef3660)) /\ ((0 + undef3660) <= (0 + undef3658)) /\ ((0 + undef3629) <= (0 + undef3661)) /\ ((0 + undef3661) <= (0 + undef3629)) /\ ((0 + undef3660) <= (0 + undef3659)) /\ ((0 + undef3659) <= (0 + undef3660)), par{ct_17^0 -> undef3629, head_27^0 -> undef3634, head_SLAM_f_26^0 -> undef3636, result_dot_nondet_sdv_special_RETURN_VALUE_13^0 -> undef3652, x_16^0 -> undef3658, x_20^0 -> undef3659, x_SLAM_f_18^0 -> undef3660, y_19^0 -> undef3661}>
<l52, l53, (undef3678 = __disjvr_24^0) /\ (__disjvr_24^0 = undef3678), par{__disjvr_24^0 -> undef3678}>
<l53, l19, (1 <= (0 + result_dot_nondet_sdv_special_RETURN_VALUE_13^0)) /\ (2 <= (0 + result_dot_nondet_sdv_special_RETURN_VALUE_13^0))>
<l51, l54, (0 <= (0 + a_116^0)) /\ (undef3862 = undef3862) /\ (undef3842 = undef3842) /\ (undef3846 = undef3846) /\ (undef3855 = undef3855) /\ (undef3841 = undef3841), par{head_129^0 -> undef3841, head_14^0 -> undef3842, head_SLAM_f_26^0 -> undef3846, r_124^0 -> undef3855, result_dot_nondet_sdv_special_RETURN_VALUE_13^0 -> undef3862}>
<l54, l55, (undef3889 = __disjvr_25^0) /\ (__disjvr_25^0 = undef3889), par{__disjvr_25^0 -> undef3889}>
<l55, l56, ((0 + head_14^0) <= (0 + head_SLAM_f_26^0)) /\ ((0 + head_SLAM_f_26^0) <= (0 + head_14^0))>
<l56, l57, (undef4030 = __disjvr_26^0) /\ (__disjvr_26^0 = undef4030), par{__disjvr_26^0 -> undef4030}>
<l57, l58, (undef4101 = __disjvr_27^0) /\ (__disjvr_27^0 = undef4101), par{__disjvr_27^0 -> undef4101}>
<l58, l42, (1 <= (0 + result_dot_nondet_sdv_special_RETURN_VALUE_13^0)) /\ (2 <= (0 + result_dot_nondet_sdv_special_RETURN_VALUE_13^0))>
<l59, l60, (0 <= (0 + i_30^0)) /\ (undef4282 = undef4282) /\ (undef4262 = undef4262) /\ (undef4266 = undef4266) /\ (undef4277 = undef4277) /\ (undef4267 = undef4267) /\ (undef4276 = undef4276), par{head_14^0 -> undef4262, head_SLAM_f_26^0 -> undef4266, i_108^0 -> undef4267, r_163^0 -> undef4276, r_39^0 -> undef4277, result_dot_nondet_sdv_special_RETURN_VALUE_13^0 -> undef4282}>
<l60, l61, (undef4312 = __disjvr_28^0) /\ (__disjvr_28^0 = undef4312), par{__disjvr_28^0 -> undef4312}>
<l61, l62, (undef4393 = undef4393) /\ (0 <= ((0 + (~(1) * undef4393)) + a_147^0)) /\ (((0 + (~(1) * undef4393)) + a_147^0) <= 0) /\ (1 <= (0 + len_132^0)) /\ ((0 + len_132^0) <= 1) /\ ((0 + head_14^0) <= (0 + head_SLAM_f_26^0)) /\ ((0 + head_SLAM_f_26^0) <= (0 + head_14^0)) /\ ((0 + undef4393) <= (0 + a_147^0)) /\ ((0 + a_147^0) <= (0 + undef4393)), par{a_116^0 -> undef4393}>
<l62, l63, (undef4453 = __disjvr_29^0) /\ (__disjvr_29^0 = undef4453), par{__disjvr_29^0 -> undef4453}>
<l63, l42, (1 <= (0 + result_dot_nondet_sdv_special_RETURN_VALUE_13^0)) /\ (2 <= (0 + result_dot_nondet_sdv_special_RETURN_VALUE_13^0)) /\ ((0 + result_dot_nondet_sdv_special_RETURN_VALUE_13^0) <= (0 + i_108^0)) /\ (undef4547 = undef4547) /\ ((~(1) + undef4547) <= (0 + a_116^0)) /\ ((0 + a_116^0) <= (~(1) + undef4547)), par{i_108^0 -> undef4547}>
<l39, l64, (0 <= (0 + i_30^0)) /\ (undef4632 = undef4632) /\ (undef4618 = undef4618) /\ ((0 + length_29^0) <= (0 + i_30^0)) /\ (undef4643 = (0 + head_32^0)) /\ (undef4642 = (0 + undef4643)) /\ (undef4623 = undef4623) /\ (undef4619 = undef4619) /\ (undef4635 = undef4635) /\ (undef4615 = undef4615) /\ (undef4631 = undef4631) /\ (undef4637 = undef4637) /\ (undef4636 = undef4636) /\ (undef4612 = (0 + undef4642)) /\ (undef4630 = undef4630) /\ (undef4616 = (0 + undef4612)) /\ (undef4614 = (0 + undef4616)) /\ (0 <= (0 + len_132^0)) /\ ((0 + len_132^0) <= 0) /\ (0 <= ((0 + a_147^0) + (~(1) * undef4619))) /\ (((0 + a_147^0) + (~(1) * undef4619)) <= 0) /\ ((0 + undef4612) <= (0 + undef4616)) /\ ((0 + undef4616) <= (0 + undef4612)) /\ ((0 + undef4612) <= (0 + undef4614)) /\ ((0 + undef4614) <= (0 + undef4612)) /\ ((0 + undef4616) <= (0 + undef4614)) /\ ((0 + undef4614) <= (0 + undef4616)) /\ ((0 + undef4619) <= (0 + a_147^0)) /\ ((0 + a_147^0) <= (0 + undef4619)), par{head_14^0 -> undef4612, head_27^0 -> undef4614, head_32^0 -> undef4615, head_SLAM_f_26^0 -> undef4616, i_167^0 -> undef4618, i_30^0 -> undef4619, length_29^0 -> undef4623, result_11^0 -> undef4630, result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33^0 -> undef4631, result_dot_nondet_sdv_special_RETURN_VALUE_13^0 -> undef4632, temp0_31^0 -> undef4635, temp_35^0 -> undef4636, tmp_34^0 -> undef4637}>
<l64, l65, (undef4667 = __disjvr_30^0) /\ (__disjvr_30^0 = undef4667), par{__disjvr_30^0 -> undef4667}>
<l65, l42, (1 <= (0 + result_dot_nondet_sdv_special_RETURN_VALUE_13^0)) /\ (2 <= (0 + result_dot_nondet_sdv_special_RETURN_VALUE_13^0)) /\ ((0 + result_dot_nondet_sdv_special_RETURN_VALUE_13^0) <= (0 + i_30^0)) /\ ((0 + result_dot_nondet_sdv_special_RETURN_VALUE_13^0) <= (0 + i_167^0))>
<l39, l66, (0 <= (0 + i_30^0)) /\ (undef4841 = undef4841) /\ (undef4832 = undef4832) /\ ((1 + i_30^0) <= (0 + length_29^0)) /\ (undef4849 = (0 + temp_35^0)) /\ (undef4848 = undef4848) /\ (undef4831 = (1 + i_30^0)) /\ ((0 + undef4831) <= (1 + undef4832)) /\ ((1 + undef4832) <= (0 + undef4831)) /\ ((0 + undef4832) <= (~(1) + undef4831)) /\ ((~(1) + undef4831) <= (0 + undef4832)) /\ ((1 + undef4832) <= (0 + length_29^0)), par{head_32^0 -> (0 + undef4849), i_30^0 -> undef4831, i_94^0 -> undef4832, rcd_88^0 -> undef4841, temp_35^0 -> undef4848, tmp_34^0 -> undef4849}>
<l66, l39, true>
<l41, l2, (undef5000 = undef5000) /\ ((0 + length_29^0) <= (0 + i_30^0)) /\ (undef5003 = (0 + head_32^0)) /\ (undef4998 = (0 + undef5003)) /\ (undef4975 = undef4975) /\ (undef4971 = undef4971) /\ (undef4987 = undef4987) /\ (undef4967 = undef4967) /\ (undef4983 = undef4983) /\ (undef4989 = undef4989) /\ (undef4988 = undef4988) /\ (undef4964 = (0 + undef4998)) /\ (undef4999 = undef4999) /\ (undef4997 = (0 + undef4964)) /\ (undef4996 = (0 + undef4997)) /\ (0 <= (0 + undef4964)) /\ ((0 + undef4964) <= 0) /\ (0 <= (0 + undef4997)) /\ ((0 + undef4997) <= 0) /\ (0 <= (0 + undef4996)) /\ ((0 + undef4996) <= 0) /\ ((0 + undef4964) <= (0 + undef4997)) /\ ((0 + undef4997) <= (0 + undef4964)) /\ ((0 + undef4997) <= (0 + undef4996)) /\ ((0 + undef4996) <= (0 + undef4997)) /\ ((0 + undef5000) <= 0) /\ (undef5001 = undef5001) /\ (0 <= (0 + undef4996)) /\ ((0 + undef4996) <= 0) /\ (undef4968 = undef4968) /\ (undef4966 = undef4966) /\ (undef5004 = (0 + undef4964)) /\ (undef4994 = 0) /\ (undef5007 = (0 + undef5004)) /\ (undef5009 = (0 + undef4994)) /\ (undef5005 = (0 + undef5007)) /\ (0 <= (0 + undef4964)) /\ ((0 + undef4964) <= 0) /\ (0 <= (0 + undef5004)) /\ ((0 + undef5004) <= 0) /\ (0 <= (0 + undef4994)) /\ ((0 + undef4994) <= 0) /\ (0 <= (0 + undef5007)) /\ ((0 + undef5007) <= 0) /\ (0 <= (0 + undef5009)) /\ ((0 + undef5009) <= 0) /\ (0 <= (0 + undef5005)) /\ ((0 + undef5005) <= 0) /\ ((0 + undef4964) <= (0 + undef5004)) /\ ((0 + undef5004) <= (0 + undef4964)) /\ ((0 + undef5004) <= (0 + undef5007)) /\ ((0 + undef5007) <= (0 + undef5004)) /\ ((0 + undef4994) <= (0 + undef5009)) /\ ((0 + undef5009) <= (0 + undef4994)) /\ ((0 + undef5007) <= (0 + undef5005)) /\ ((0 + undef5005) <= (0 + undef5007)) /\ ((0 + undef5001) <= 0) /\ (undef4984 = undef4984) /\ ((0 + undef5009) <= (0 + undef5005)) /\ ((0 + undef5005) <= (0 + undef5009)) /\ (undef5008 = undef5008) /\ (undef5010 = undef5010) /\ (undef5006 = undef5006) /\ (undef5002 = undef5002) /\ (undef4995 = undef4995) /\ (undef4990 = undef4990) /\ (undef4961 = undef4961) /\ (undef4992 = undef4992) /\ (undef4993 = undef4993) /\ (undef4991 = undef4991) /\ (undef4985 = undef4985) /\ ((0 + undef4984) <= 0), par{ct_17^0 -> undef4961, head_14^0 -> undef4964, head_27^0 -> undef4966, head_32^0 -> undef4967, head_SLAM_f_26^0 -> undef4968, i_30^0 -> undef4971, length_29^0 -> undef4975, result_11^0 -> (0 + temp0_15^0), result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33^0 -> undef4983, result_dot_nondet_sdv_special_RETURN_VALUE_13^0 -> undef4984, t_23^0 -> undef4985, temp0_31^0 -> undef4987, temp_35^0 -> undef4988, tmp_34^0 -> undef4989, x_16^0 -> undef4990, x_20^0 -> undef4991, x_SLAM_f_18^0 -> undef4992, y_19^0 -> undef4993}>
<l41, l26, (undef5071 = undef5071) /\ (undef5070 = undef5070) /\ ((1 + i_30^0) <= (0 + length_29^0)) /\ (undef5076 = (0 + temp_35^0)) /\ (undef5075 = undef5075) /\ (undef5054 = (0 + undef5076)) /\ (undef5058 = (1 + i_30^0)) /\ (1 <= (0 + undef5058)) /\ ((0 + undef5058) <= 1) /\ ((0 + undef5071) <= (0 + length_29^0)) /\ ((0 + length_29^0) <= (0 + undef5071)) /\ ((0 + undef5054) <= (0 + undef5070)) /\ ((0 + undef5070) <= (0 + undef5054)) /\ ((0 + undef5054) <= (0 + undef5076)) /\ ((0 + undef5076) <= (0 + undef5054)) /\ ((0 + undef5070) <= (0 + undef5076)) /\ ((0 + undef5076) <= (0 + undef5070)) /\ (1 <= (0 + length_29^0)), par{head_32^0 -> undef5054, i_30^0 -> undef5058, result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_33^0 -> undef5070, result_dot_nondet_sdv_special_RETURN_VALUE_13^0 -> undef5071, temp_35^0 -> undef5075, tmp_34^0 -> undef5076}>
<l67, l40, true>

Fresh variables:
undef38, undef61, undef62, undef67, undef68, undef69, undef70, undef71, undef72, undef73, undef74, undef75, undef113, undef116, undef131, undef136, undef142, undef144, undef146, undef252, undef297, undef378, undef450, undef531, undef673, undef676, undef696, undef697, undef702, undef703, undef704, undef705, undef706, undef707, undef708, undef709, undef710, undef736, undef888, undef891, undef911, undef917, undef919, undef947, undef1088, undef1159, undef1230, undef1378, undef1381, undef1401, undef1407, undef1409, undef1441, undef1515, undef1542, undef1552, undef1623, undef1694, undef1810, undef1871, undef1873, undef1874, undef1875, undef1878, undef1882, undef1889, undef1890, undef1891, undef1894, undef1895, undef1896, undef1901, undef1902, undef1903, undef1904, undef1905, undef1910, undef2051, undef2153, undef2158, undef2160, undef2176, undef2182, undef2183, undef2184, undef2185, undef2192, undef2293, undef2296, undef2316, undef2322, undef2324, undef2333, undef2457, undef2474, undef2545, undef2643, undef2646, undef2667, undef2672, undef2673, undef2674, undef2675, undef2676, undef2677, undef2678, undef2679, undef2680, undef2691, undef2794, undef2798, undef2807, undef2810, undef2811, undef2815, undef2816, undef2864, undef2868, undef2872, undef2873, undef2881, undef2891, undef2929, undef2934, undef2936, undef2952, undef2958, undef2959, undef2960, undef2961, undef2974, undef3140, undef3142, undef3143, undef3146, undef3157, undef3162, undef3185, undef3275, undef3292, undef3326, undef3397, undef3484, undef3501, undef3629, undef3634, undef3636, undef3652, undef3658, undef3659, undef3660, undef3661, undef3678, undef3841, undef3842, undef3846, undef3855, undef3862, undef3889, undef4030, undef4101, undef4262, undef4266, undef4267, undef4276, undef4277, undef4282, undef4312, undef4393, undef4453, undef4547, undef4612, undef4614, undef4615, undef4616, undef4618, undef4619, undef4623, undef4630, undef4631, undef4632, undef4635, undef4636, undef4637, undef4642, undef4643, undef4667, undef4831, undef4832, undef4841, undef4848, undef4849, undef4961, undef4964, undef4966, undef4967, undef4968, undef4971, undef4975, undef4983, undef4984, undef4985, undef4987, undef4988, undef4989, undef4990, undef4991, undef4992, undef4993, undef4994, undef4995, undef4996, undef4997, undef4998, undef4999, undef5000, undef5001, undef5002, undef5003, undef5004, undef5005, undef5006, undef5007, undef5008, undef5009, undef5010, undef5054, undef5058, undef5070, undef5071, undef5075, undef5076, 

Undef variables:
undef38, undef61, undef62, undef67, undef68, undef69, undef70, undef71, undef72, undef73, undef74, undef75, undef113, undef116, undef131, undef136, undef142, undef144, undef146, undef252, undef297, undef378, undef450, undef531, undef673, undef676, undef696, undef697, undef702, undef703, undef704, undef705, undef706, undef707, undef708, undef709, undef710, undef736, undef888, undef891, undef911, undef917, undef919, undef947, undef1088, undef1159, undef1230, undef1378, undef1381, undef1401, undef1407, undef1409, undef1441, undef1515, undef1542, undef1552, undef1623, undef1694, undef1810, undef1871, undef1873, undef1874, undef1875, undef1878, undef1882, undef1889, undef1890, undef1891, undef1894, undef1895, undef1896, undef1901, undef1902, undef1903, undef1904, undef1905, undef1910, undef2051, undef2153, undef2158, undef2160, undef2176, undef2182, undef2183, undef2184, undef2185, undef2192, undef2293, undef2296, undef2316, undef2322, undef2324, undef2333, undef2457, undef2474, undef2545, undef2643, undef2646, undef2667, undef2672, undef2673, undef2674, undef2675, undef2676, undef2677, undef2678, undef2679, undef2680, undef2691, undef2794, undef2798, undef2807, undef2810, undef2811, undef2815, undef2816, undef2864, undef2868, undef2872, undef2873, undef2881, undef2891, undef2929, undef2934, undef2936, undef2952, undef2958, undef2959, undef2960, undef2961, undef2974, undef3140, undef3142, undef3143, undef3146, undef3157, undef3162, undef3185, undef3275, undef3292, undef3326, undef3397, undef3484, undef3501, undef3629, undef3634, undef3636, undef3652, undef3658, undef3659, undef3660, undef3661, undef3678, undef3841, undef3842, undef3846, undef3855, undef3862, undef3889, undef4030, undef4101, undef4262, undef4266, undef4267, undef4276, undef4277, undef4282, undef4312, undef4393, undef4453, undef4547, undef4612, undef4614, undef4615, undef4616, undef4618, undef4619, undef4623, undef4630, undef4631, undef4632, undef4635, undef4636, undef4637, undef4642, undef4643, undef4667, undef4831, undef4832, undef4841, undef4848, undef4849, undef4961, undef4964, undef4966, undef4967, undef4968, undef4971, undef4975, undef4983, undef4984, undef4985, undef4987, undef4988, undef4989, undef4990, undef4991, undef4992, undef4993, undef4994, undef4995, undef4996, undef4997, undef4998, undef4999, undef5000, undef5001, undef5002, undef5003, undef5004, undef5005, undef5006, undef5007, undef5008, undef5009, undef5010, undef5054, undef5058, undef5070, undef5071, undef5075, undef5076, 

Abstraction variables:

Exit nodes:

Accepting locations:

Asserts:

Preprocessed LLVMGraph
Init Location: 0
Transitions:
<l0, l2, (undef2891 = undef2891) /\ (undef2881 = (0 + undef2891)) /\ (undef2873 = undef2873) /\ (undef2872 = (0 + undef2881)) /\ (undef2864 = 0) /\ (undef2868 = 0) /\ (0 <= (0 + undef2868)) /\ ((0 + undef2868) <= 0) /\ (0 <= (0 + undef2864)) /\ ((0 + undef2864) <= 0) /\ ((0 + undef2881) <= (0 + undef2872)) /\ ((0 + undef2872) <= (0 + undef2881)) /\ (undef5000 = undef5000) /\ ((0 + undef2872) <= (0 + undef2868)) /\ (undef5003 = (0 + undef2864)) /\ (undef4998 = (0 + undef5003)) /\ (undef4975 = undef4975) /\ (undef4971 = undef4971) /\ (undef4987 = undef4987) /\ (undef4967 = undef4967) /\ (undef4983 = undef4983) /\ (undef4989 = undef4989) /\ (undef4988 = undef4988) /\ (undef4964 = (0 + undef4998)) /\ (undef4999 = undef4999) /\ (undef4997 = (0 + undef4964)) /\ (undef4996 = (0 + undef4997)) /\ (0 <= (0 + undef4964)) /\ ((0 + undef4964) <= 0) /\ (0 <= (0 + undef4997)) /\ ((0 + undef4997) <= 0) /\ (0 <= (0 + undef4996)) /\ ((0 + undef4996) <= 0) /\ ((0 + undef4964) <= (0 + undef4997)) /\ ((0 + undef4997) <= (0 + undef4964)) /\ ((0 + undef4997) <= (0 + undef4996)) /\ ((0 + undef4996) <= (0 + undef4997)) /\ ((0 + undef5000) <= 0) /\ (undef5001 = undef5001) /\ (0 <= (0 + undef4996)) /\ ((0 + undef4996) <= 0) /\ (undef4968 = undef4968) /\ (undef4966 = undef4966) /\ (undef5004 = (0 + undef4964)) /\ (undef4994 = 0) /\ (undef5007 = (0 + undef5004)) /\ (undef5009 = (0 + undef4994)) /\ (undef5005 = (0 + undef5007)) /\ (0 <= (0 + undef4964)) /\ ((0 + undef4964) <= 0) /\ (0 <= (0 + undef5004)) /\ ((0 + undef5004) <= 0) /\ (0 <= (0 + undef4994)) /\ ((0 + undef4994) <= 0) /\ (0 <= (0 + undef5007)) /\ ((0 + undef5007) <= 0) /\ (0 <= (0 + undef5009)) /\ ((0 + undef5009) <= 0) /\ (0 <= (0 + undef5005)) /\ ((0 + undef5005) <= 0) /\ ((0 + undef4964) <= (0 + undef5004)) /\ ((0 + undef5004) <= (0 + undef4964)) /\ ((0 + undef5004) <= (0 + undef5007)) /\ ((0 + undef5007) <= (0 + undef5004)) /\ ((0 + undef4994) <= (0 + undef5009)) /\ ((0 + undef5009) <= (0 + undef4994)) /\ ((0 + undef5007) <= (0 + undef5005)) /\ ((0 + undef5005) <= (0 + undef5007)) /\ ((0 + undef5001) <= 0) /\ (undef4984 = undef4984) /\ ((0 + undef5009) <= (0 + undef5005)) /\ ((0 + undef5005) <= (0 + undef5009)) /\ (undef5008 = undef5008) /\ (undef5010 = undef5010) /\ (undef5006 = undef5006) /\ (undef5002 = undef5002) /\ (undef4995 = undef4995) /\ (undef4990 = undef4990) /\ (undef4961 = undef4961) /\ (undef4992 = undef4992) /\ (undef4993 = undef4993) /\ (undef4991 = undef4991) /\ (undef4985 = undef4985) /\ ((0 + undef4984) <= 0), par{head_14^0 -> undef4964, head_27^0 -> undef4966, head_32^0 -> undef4967, i_30^0 -> undef4971, length_29^0 -> undef4975, temp_35^0 -> undef4988, x_20^0 -> undef4991, y_19^0 -> undef4993}>
<l0, l2, (undef2891 = undef2891) /\ (undef2881 = (0 + undef2891)) /\ (undef2873 = undef2873) /\ (undef2872 = (0 + undef2881)) /\ (undef2864 = 0) /\ (undef2868 = 0) /\ (0 <= (0 + undef2868)) /\ ((0 + undef2868) <= 0) /\ (0 <= (0 + undef2864)) /\ ((0 + undef2864) <= 0) /\ ((0 + undef2881) <= (0 + undef2872)) /\ ((0 + undef2872) <= (0 + undef2881)) /\ (undef5071 = undef5071) /\ (undef5070 = undef5070) /\ ((1 + undef2868) <= (0 + undef2872)) /\ (undef5076 = (0 + temp_35^0)) /\ (undef5075 = undef5075) /\ (undef5054 = (0 + undef5076)) /\ (undef5058 = (1 + undef2868)) /\ (1 <= (0 + undef5058)) /\ ((0 + undef5058) <= 1) /\ ((0 + undef5071) <= (0 + undef2872)) /\ ((0 + undef2872) <= (0 + undef5071)) /\ ((0 + undef5054) <= (0 + undef5070)) /\ ((0 + undef5070) <= (0 + undef5054)) /\ ((0 + undef5054) <= (0 + undef5076)) /\ ((0 + undef5076) <= (0 + undef5054)) /\ ((0 + undef5070) <= (0 + undef5076)) /\ ((0 + undef5076) <= (0 + undef5070)) /\ (1 <= (0 + undef2872)) /\ (undef1904 = undef1904) /\ ((0 + undef2872) <= (0 + undef5058)) /\ (undef1905 = (0 + undef5054)) /\ (undef1903 = (0 + undef1905)) /\ (undef1882 = undef1882) /\ (undef1878 = undef1878) /\ (undef1894 = undef1894) /\ (undef1874 = undef1874) /\ (undef1890 = undef1890) /\ (undef1896 = undef1896) /\ (undef1895 = undef1895) /\ (undef1901 = (0 + undef1903)) /\ (undef1889 = undef1889) /\ (undef1902 = (0 + undef1901)) /\ (undef1873 = (0 + undef1902)) /\ (1 <= (0 + undef1904)) /\ ((0 + undef1904) <= 1) /\ ((0 + undef1901) <= (0 + undef1902)) /\ ((0 + undef1902) <= (0 + undef1901)) /\ ((0 + undef1901) <= (0 + undef1873)) /\ ((0 + undef1873) <= (0 + undef1901)) /\ ((0 + undef1902) <= (0 + undef1873)) /\ ((0 + undef1873) <= (0 + undef1902)) /\ (1 <= (0 + undef1904)) /\ ((0 + undef1904) <= 1) /\ (undef1891 = undef1891) /\ (undef1871 = undef1871) /\ (undef1875 = undef1875) /\ (undef1910 = __disjvr_13^0) /\ (__disjvr_13^0 = undef1910) /\ (0 <= (0 + undef1873)) /\ ((0 + undef1873) <= 0) /\ (1 <= (0 + undef1891)) /\ ((0 + undef1891) <= 1) /\ ((0 + undef1871) <= (0 + undef1875)) /\ ((0 + undef1875) <= (0 + undef1871)) /\ (undef2051 = __disjvr_14^0) /\ (__disjvr_14^0 = undef2051) /\ (1 <= (0 + undef1891)) /\ ((0 + undef1891) <= 1) /\ (undef2176 = undef2176) /\ (0 <= (0 + undef1873)) /\ ((0 + undef1873) <= 0) /\ (undef2160 = undef2160) /\ (undef2158 = undef2158) /\ (undef2182 = (0 + undef1871)) /\ (undef2153 = 0) /\ (undef2184 = (0 + undef2182)) /\ (undef2185 = (0 + undef2153)) /\ (undef2183 = (0 + undef2184)) /\ (0 <= (0 + undef2153)) /\ ((0 + undef2153) <= 0) /\ (0 <= (0 + undef2185)) /\ ((0 + undef2185) <= 0) /\ (1 <= (0 + undef2176)) /\ ((0 + undef2176) <= 1) /\ ((0 + undef1871) <= (0 + undef2182)) /\ ((0 + undef2182) <= (0 + undef1871)) /\ ((0 + undef1871) <= (0 + undef2184)) /\ ((0 + undef2184) <= (0 + undef1871)) /\ ((0 + undef1871) <= (0 + undef2183)) /\ ((0 + undef2183) <= (0 + undef1871)) /\ ((0 + undef2182) <= (0 + undef2184)) /\ ((0 + undef2184) <= (0 + undef2182)) /\ ((0 + undef2153) <= (0 + undef2185)) /\ ((0 + undef2185) <= (0 + undef2153)) /\ ((0 + undef2184) <= (0 + undef2183)) /\ ((0 + undef2183) <= (0 + undef2184)) /\ (undef2192 = __disjvr_15^0) /\ (__disjvr_15^0 = undef2192) /\ (1 <= (0 + undef2176)) /\ ((0 + undef2176) <= 1) /\ (undef2316 = undef2316) /\ (undef2296 = undef2296) /\ (undef2322 = undef2322) /\ (undef2293 = undef2293) /\ (undef2324 = undef2324) /\ (undef2333 = __disjvr_16^0) /\ (__disjvr_16^0 = undef2333) /\ (undef2457 = (0 + undef2183)) /\ (0 <= (0 + undef2293)) /\ ((0 + undef2293) <= 0) /\ (0 <= (0 + undef2185)) /\ ((0 + undef2185) <= 0) /\ (0 <= (0 + undef2183)) /\ ((0 + undef2183) <= 0) /\ (1 <= (0 + undef2316)) /\ ((0 + undef2316) <= 1) /\ ((0 + undef2296) <= (0 + undef2322)) /\ ((0 + undef2322) <= (0 + undef2296)) /\ ((0 + undef2296) <= (0 + undef2324)) /\ ((0 + undef2324) <= (0 + undef2296)) /\ ((0 + undef2296) <= (0 + undef2457)) /\ ((0 + undef2457) <= (0 + undef2296)) /\ ((0 + undef2322) <= (0 + undef2324)) /\ ((0 + undef2324) <= (0 + undef2322)) /\ ((0 + undef2293) <= (0 + undef2185)) /\ ((0 + undef2185) <= (0 + undef2293)) /\ (undef2474 = __disjvr_17^0) /\ (__disjvr_17^0 = undef2474) /\ (undef2545 = __disjvr_18^0) /\ (__disjvr_18^0 = undef2545) /\ (1 <= (0 + undef2316)) /\ ((0 + undef2316) <= 1) /\ (undef2646 = undef2646) /\ ((0 + undef2185) <= (0 + undef2183)) /\ ((0 + undef2183) <= (0 + undef2185)) /\ (undef2679 = undef2679) /\ (undef2680 = undef2680) /\ (undef2678 = undef2678) /\ (undef2677 = undef2677) /\ (undef2676 = undef2676) /\ (undef2672 = undef2672) /\ (undef2643 = undef2643) /\ (undef2674 = undef2674) /\ (undef2675 = undef2675) /\ (undef2673 = undef2673) /\ (undef2667 = undef2667) /\ (undef2691 = __disjvr_19^0) /\ (__disjvr_19^0 = undef2691), par{__disjvr_13^0 -> undef1910, __disjvr_14^0 -> undef2051, __disjvr_15^0 -> undef2192, __disjvr_16^0 -> undef2333, __disjvr_17^0 -> undef2474, __disjvr_18^0 -> undef2545, __disjvr_19^0 -> undef2691, head_14^0 -> undef2646, head_27^0 -> undef2158, head_32^0 -> undef1874, i_30^0 -> undef1878, length_29^0 -> undef1882, temp_35^0 -> undef1895, x_20^0 -> undef2673, y_19^0 -> undef2675}>
<l0, l39, (undef2891 = undef2891) /\ (undef2881 = (0 + undef2891)) /\ (undef2873 = undef2873) /\ (undef2872 = (0 + undef2881)) /\ (undef2864 = 0) /\ (undef2868 = 0) /\ (0 <= (0 + undef2868)) /\ ((0 + undef2868) <= 0) /\ (0 <= (0 + undef2864)) /\ ((0 + undef2864) <= 0) /\ ((0 + undef2881) <= (0 + undef2872)) /\ ((0 + undef2872) <= (0 + undef2881)) /\ (undef5071 = undef5071) /\ (undef5070 = undef5070) /\ ((1 + undef2868) <= (0 + undef2872)) /\ (undef5076 = (0 + temp_35^0)) /\ (undef5075 = undef5075) /\ (undef5054 = (0 + undef5076)) /\ (undef5058 = (1 + undef2868)) /\ (1 <= (0 + undef5058)) /\ ((0 + undef5058) <= 1) /\ ((0 + undef5071) <= (0 + undef2872)) /\ ((0 + undef2872) <= (0 + undef5071)) /\ ((0 + undef5054) <= (0 + undef5070)) /\ ((0 + undef5070) <= (0 + undef5054)) /\ ((0 + undef5054) <= (0 + undef5076)) /\ ((0 + undef5076) <= (0 + undef5054)) /\ ((0 + undef5070) <= (0 + undef5076)) /\ ((0 + undef5076) <= (0 + undef5070)) /\ (1 <= (0 + undef2872)) /\ (undef2811 = undef2811) /\ (undef2810 = undef2810) /\ (undef2807 = undef2807) /\ ((1 + undef5058) <= (0 + undef2872)) /\ (undef2816 = (0 + undef5075)) /\ (undef2815 = undef2815) /\ (undef2794 = (0 + undef2816)) /\ (undef2798 = (1 + undef5058)) /\ (2 <= (0 + undef2798)) /\ ((0 + undef2798) <= 2) /\ ((0 + undef2811) <= (0 + undef2872)) /\ ((0 + undef2872) <= (0 + undef2811)) /\ ((0 + undef2794) <= (0 + undef2810)) /\ ((0 + undef2810) <= (0 + undef2794)) /\ ((0 + undef2794) <= (0 + undef2816)) /\ ((0 + undef2816) <= (0 + undef2794)) /\ ((0 + undef2810) <= (0 + undef2816)) /\ ((0 + undef2816) <= (0 + undef2810)) /\ (1 <= (0 + undef2872)) /\ (2 <= (0 + undef2872)), par{head_32^0 -> undef2794, i_30^0 -> undef2798, length_29^0 -> undef2872, temp_35^0 -> undef2815}>
<l1, l2, (0 <= (0 + a_237^0)) /\ (undef61 = undef61) /\ ((0 + y_19^0) <= (0 + x_20^0)) /\ ((0 + x_20^0) <= (0 + y_19^0)) /\ (undef74 = undef74) /\ (undef75 = undef75) /\ (undef73 = undef73) /\ (undef72 = undef72) /\ (undef71 = undef71) /\ (undef67 = undef67) /\ (undef38 = undef38) /\ (undef69 = undef69) /\ (undef70 = undef70) /\ (undef68 = undef68) /\ (undef62 = undef62) /\ (1 <= (0 + undef61)) /\ (2 <= (0 + undef61)), par{x_20^0 -> undef68, y_19^0 -> undef70}>
<l1, l1, (0 <= (0 + a_237^0)) /\ (undef136 = undef136) /\ (undef116 = undef116) /\ (undef142 = undef142) /\ (undef113 = undef113) /\ (undef144 = undef144) /\ (undef131 = undef131) /\ (undef146 = __disjvr_0^0) /\ (__disjvr_0^0 = undef146) /\ (undef252 = undef252) /\ (0 <= (0 + undef113)) /\ ((0 + undef113) <= 0) /\ (0 <= (0 + y_19^0)) /\ ((0 + y_19^0) <= 0) /\ ((0 + undef116) <= (0 + undef142)) /\ ((0 + undef142) <= (0 + undef116)) /\ ((0 + undef116) <= (0 + undef144)) /\ ((0 + undef144) <= (0 + undef116)) /\ ((0 + undef142) <= (0 + undef144)) /\ ((0 + undef144) <= (0 + undef142)) /\ ((0 + undef113) <= (0 + y_19^0)) /\ ((0 + y_19^0) <= (0 + undef113)) /\ ((0 + undef252) <= (~(1) + a_237^0)) /\ ((~(1) + a_237^0) <= (0 + undef252)) /\ (undef297 = __disjvr_1^0) /\ (__disjvr_1^0 = undef297) /\ (undef378 = __disjvr_2^0) /\ (__disjvr_2^0 = undef378) /\ (undef450 = __disjvr_3^0) /\ (__disjvr_3^0 = undef450) /\ (1 <= (0 + undef136)) /\ (2 <= (0 + undef136)) /\ (undef531 = undef531) /\ ((0 + undef531) <= (0 + undef252)) /\ ((0 + undef252) <= (0 + undef531)), par{__disjvr_0^0 -> undef146, __disjvr_1^0 -> undef297, __disjvr_2^0 -> undef378, __disjvr_3^0 -> undef450, a_237^0 -> undef531, head_14^0 -> undef116}>
<l39, l42, (0 <= (0 + i_30^0)) /\ (undef4632 = undef4632) /\ (undef4618 = undef4618) /\ ((0 + length_29^0) <= (0 + i_30^0)) /\ (undef4643 = (0 + head_32^0)) /\ (undef4642 = (0 + undef4643)) /\ (undef4623 = undef4623) /\ (undef4619 = undef4619) /\ (undef4635 = undef4635) /\ (undef4615 = undef4615) /\ (undef4631 = undef4631) /\ (undef4637 = undef4637) /\ (undef4636 = undef4636) /\ (undef4612 = (0 + undef4642)) /\ (undef4630 = undef4630) /\ (undef4616 = (0 + undef4612)) /\ (undef4614 = (0 + undef4616)) /\ (0 <= (0 + len_132^0)) /\ ((0 + len_132^0) <= 0) /\ (0 <= ((0 + a_147^0) + (~(1) * undef4619))) /\ (((0 + a_147^0) + (~(1) * undef4619)) <= 0) /\ ((0 + undef4612) <= (0 + undef4616)) /\ ((0 + undef4616) <= (0 + undef4612)) /\ ((0 + undef4612) <= (0 + undef4614)) /\ ((0 + undef4614) <= (0 + undef4612)) /\ ((0 + undef4616) <= (0 + undef4614)) /\ ((0 + undef4614) <= (0 + undef4616)) /\ ((0 + undef4619) <= (0 + a_147^0)) /\ ((0 + a_147^0) <= (0 + undef4619)) /\ (undef4667 = __disjvr_30^0) /\ (__disjvr_30^0 = undef4667) /\ (1 <= (0 + undef4632)) /\ (2 <= (0 + undef4632)) /\ ((0 + undef4632) <= (0 + undef4619)) /\ ((0 + undef4632) <= (0 + undef4618)), par{__disjvr_30^0 -> undef4667, head_14^0 -> undef4612, head_27^0 -> undef4614, head_32^0 -> undef4615, i_30^0 -> undef4619, length_29^0 -> undef4623, temp_35^0 -> undef4636}>
<l39, l39, (0 <= (0 + i_30^0)) /\ (undef4841 = undef4841) /\ (undef4832 = undef4832) /\ ((1 + i_30^0) <= (0 + length_29^0)) /\ (undef4849 = (0 + temp_35^0)) /\ (undef4848 = undef4848) /\ (undef4831 = (1 + i_30^0)) /\ ((0 + undef4831) <= (1 + undef4832)) /\ ((1 + undef4832) <= (0 + undef4831)) /\ ((0 + undef4832) <= (~(1) + undef4831)) /\ ((~(1) + undef4831) <= (0 + undef4832)) /\ ((1 + undef4832) <= (0 + length_29^0)), par{head_32^0 -> (0 + undef4849), i_30^0 -> undef4831, temp_35^0 -> undef4848}>
<l42, l1, (0 <= (0 + len_132^0)) /\ (0 <= (0 + a_147^0)) /\ (undef2952 = undef2952) /\ (0 <= (0 + head_27^0)) /\ ((0 + head_27^0) <= 0) /\ (undef2936 = undef2936) /\ (undef2934 = undef2934) /\ (undef2958 = (0 + head_14^0)) /\ (undef2929 = 0) /\ (undef2960 = (0 + undef2958)) /\ (undef2961 = (0 + undef2929)) /\ (undef2959 = (0 + undef2960)) /\ (0 <= (0 + undef2929)) /\ ((0 + undef2929) <= 0) /\ (0 <= (0 + undef2961)) /\ ((0 + undef2961) <= 0) /\ ((0 + head_14^0) <= (0 + undef2958)) /\ ((0 + undef2958) <= (0 + head_14^0)) /\ ((0 + head_14^0) <= (0 + undef2960)) /\ ((0 + undef2960) <= (0 + head_14^0)) /\ ((0 + head_14^0) <= (0 + undef2959)) /\ ((0 + undef2959) <= (0 + head_14^0)) /\ ((0 + undef2958) <= (0 + undef2960)) /\ ((0 + undef2960) <= (0 + undef2958)) /\ ((0 + undef2929) <= (0 + undef2961)) /\ ((0 + undef2961) <= (0 + undef2929)) /\ ((0 + undef2960) <= (0 + undef2959)) /\ ((0 + undef2959) <= (0 + undef2960)) /\ (undef2974 = __disjvr_20^0) /\ (__disjvr_20^0 = undef2974) /\ (1 <= (0 + undef2952)) /\ (2 <= (0 + undef2952)) /\ (0 <= (0 + len_132^0)) /\ (undef1401 = undef1401) /\ (undef1381 = undef1381) /\ (undef1407 = undef1407) /\ (undef1378 = undef1378) /\ (undef1409 = undef1409) /\ (undef1441 = __disjvr_9^0) /\ (__disjvr_9^0 = undef1441) /\ (undef1542 = (0 + undef2959)) /\ (undef1515 = undef1515) /\ (0 <= (0 + undef1378)) /\ ((0 + undef1378) <= 0) /\ (0 <= (0 + undef2961)) /\ ((0 + undef2961) <= 0) /\ (0 <= ((0 + (~(1) * undef1515)) + a_237^0)) /\ (((0 + (~(1) * undef1515)) + a_237^0) <= 0) /\ ((0 + undef1381) <= (0 + undef1407)) /\ ((0 + undef1407) <= (0 + undef1381)) /\ ((0 + undef1381) <= (0 + undef1409)) /\ ((0 + undef1409) <= (0 + undef1381)) /\ ((0 + undef1381) <= (0 + undef1542)) /\ ((0 + undef1542) <= (0 + undef1381)) /\ ((0 + undef1407) <= (0 + undef1409)) /\ ((0 + undef1409) <= (0 + undef1407)) /\ ((0 + undef1378) <= (0 + undef2961)) /\ ((0 + undef2961) <= (0 + undef1378)) /\ ((0 + undef1515) <= (0 + a_237^0)) /\ ((0 + a_237^0) <= (0 + undef1515)) /\ (undef1552 = __disjvr_10^0) /\ (__disjvr_10^0 = undef1552) /\ (undef1623 = __disjvr_11^0) /\ (__disjvr_11^0 = undef1623) /\ (undef1694 = __disjvr_12^0) /\ (__disjvr_12^0 = undef1694) /\ (1 <= (0 + undef1401)) /\ (2 <= (0 + undef1401)) /\ (undef1810 = undef1810) /\ ((~(1) + undef1810) <= (0 + undef1515)) /\ ((0 + undef1515) <= (~(1) + undef1810)), par{__disjvr_10^0 -> undef1552, __disjvr_11^0 -> undef1623, __disjvr_12^0 -> undef1694, __disjvr_20^0 -> undef2974, __disjvr_9^0 -> undef1441, a_215^0 -> undef1515, head_14^0 -> undef1381, head_27^0 -> undef2934, len_132^0 -> undef1810, x_20^0 -> undef2959, y_19^0 -> undef2961}>
<l42, l42, (0 <= (0 + len_132^0)) /\ (0 <= (0 + a_147^0)) /\ (undef3162 = undef3162) /\ (undef3142 = undef3142) /\ (undef3146 = undef3146) /\ (undef3157 = undef3157) /\ (undef3140 = undef3140) /\ (undef3143 = undef3143) /\ (undef3185 = __disjvr_21^0) /\ (__disjvr_21^0 = undef3185) /\ (undef3292 = undef3292) /\ (undef3275 = undef3275) /\ (1 <= ((0 + (~(1) * len_132^0)) + undef3292)) /\ (((0 + (~(1) * len_132^0)) + undef3292) <= 1) /\ ((0 + undef3142) <= (0 + undef3146)) /\ ((0 + undef3146) <= (0 + undef3142)) /\ ((0 + head_27^0) <= (0 + undef3140)) /\ ((0 + undef3140) <= (0 + head_27^0)) /\ ((0 + undef3275) <= (~(1) + a_147^0)) /\ ((~(1) + a_147^0) <= (0 + undef3275)) /\ (undef3326 = __disjvr_22^0) /\ (__disjvr_22^0 = undef3326) /\ (undef3397 = __disjvr_23^0) /\ (__disjvr_23^0 = undef3397) /\ (1 <= (0 + undef3162)) /\ (2 <= (0 + undef3162)) /\ (undef3484 = undef3484) /\ ((0 + undef3484) <= (0 + undef3275)) /\ ((0 + undef3275) <= (0 + undef3484)) /\ (undef3501 = undef3501) /\ ((0 + undef3501) <= (0 + undef3292)) /\ ((0 + undef3292) <= (0 + undef3501)), par{__disjvr_21^0 -> undef3185, __disjvr_22^0 -> undef3326, __disjvr_23^0 -> undef3397, a_147^0 -> undef3484, head_14^0 -> undef3142, len_132^0 -> undef3501}>

Fresh variables:
undef38, undef61, undef62, undef67, undef68, undef69, undef70, undef71, undef72, undef73, undef74, undef75, undef113, undef116, undef131, undef136, undef142, undef144, undef146, undef252, undef297, undef378, undef450, undef531, undef673, undef676, undef696, undef697, undef702, undef703, undef704, undef705, undef706, undef707, undef708, undef709, undef710, undef736, undef888, undef891, undef911, undef917, undef919, undef947, undef1088, undef1159, undef1230, undef1378, undef1381, undef1401, undef1407, undef1409, undef1441, undef1515, undef1542, undef1552, undef1623, undef1694, undef1810, undef1871, undef1873, undef1874, undef1875, undef1878, undef1882, undef1889, undef1890, undef1891, undef1894, undef1895, undef1896, undef1901, undef1902, undef1903, undef1904, undef1905, undef1910, undef2051, undef2153, undef2158, undef2160, undef2176, undef2182, undef2183, undef2184, undef2185, undef2192, undef2293, undef2296, undef2316, undef2322, undef2324, undef2333, undef2457, undef2474, undef2545, undef2643, undef2646, undef2667, undef2672, undef2673, undef2674, undef2675, undef2676, undef2677, undef2678, undef2679, undef2680, undef2691, undef2794, undef2798, undef2807, undef2810, undef2811, undef2815, undef2816, undef2864, undef2868, undef2872, undef2873, undef2881, undef2891, undef2929, undef2934, undef2936, undef2952, undef2958, undef2959, undef2960, undef2961, undef2974, undef3140, undef3142, undef3143, undef3146, undef3157, undef3162, undef3185, undef3275, undef3292, undef3326, undef3397, undef3484, undef3501, undef3629, undef3634, undef3636, undef3652, undef3658, undef3659, undef3660, undef3661, undef3678, undef3841, undef3842, undef3846, undef3855, undef3862, undef3889, undef4030, undef4101, undef4262, undef4266, undef4267, undef4276, undef4277, undef4282, undef4312, undef4393, undef4453, undef4547, undef4612, undef4614, undef4615, undef4616, undef4618, undef4619, undef4623, undef4630, undef4631, undef4632, undef4635, undef4636, undef4637, undef4642, undef4643, undef4667, undef4831, undef4832, undef4841, undef4848, undef4849, undef4961, undef4964, undef4966, undef4967, undef4968, undef4971, undef4975, undef4983, undef4984, undef4985, undef4987, undef4988, undef4989, undef4990, undef4991, undef4992, undef4993, undef4994, undef4995, undef4996, undef4997, undef4998, undef4999, undef5000, undef5001, undef5002, undef5003, undef5004, undef5005, undef5006, undef5007, undef5008, undef5009, undef5010, undef5054, undef5058, undef5070, undef5071, undef5075, undef5076, 

Undef variables:
undef38, undef61, undef62, undef67, undef68, undef69, undef70, undef71, undef72, undef73, undef74, undef75, undef113, undef116, undef131, undef136, undef142, undef144, undef146, undef252, undef297, undef378, undef450, undef531, undef673, undef676, undef696, undef697, undef702, undef703, undef704, undef705, undef706, undef707, undef708, undef709, undef710, undef736, undef888, undef891, undef911, undef917, undef919, undef947, undef1088, undef1159, undef1230, undef1378, undef1381, undef1401, undef1407, undef1409, undef1441, undef1515, undef1542, undef1552, undef1623, undef1694, undef1810, undef1871, undef1873, undef1874, undef1875, undef1878, undef1882, undef1889, undef1890, undef1891, undef1894, undef1895, undef1896, undef1901, undef1902, undef1903, undef1904, undef1905, undef1910, undef2051, undef2153, undef2158, undef2160, undef2176, undef2182, undef2183, undef2184, undef2185, undef2192, undef2293, undef2296, undef2316, undef2322, undef2324, undef2333, undef2457, undef2474, undef2545, undef2643, undef2646, undef2667, undef2672, undef2673, undef2674, undef2675, undef2676, undef2677, undef2678, undef2679, undef2680, undef2691, undef2794, undef2798, undef2807, undef2810, undef2811, undef2815, undef2816, undef2864, undef2868, undef2872, undef2873, undef2881, undef2891, undef2929, undef2934, undef2936, undef2952, undef2958, undef2959, undef2960, undef2961, undef2974, undef3140, undef3142, undef3143, undef3146, undef3157, undef3162, undef3185, undef3275, undef3292, undef3326, undef3397, undef3484, undef3501, undef3629, undef3634, undef3636, undef3652, undef3658, undef3659, undef3660, undef3661, undef3678, undef3841, undef3842, undef3846, undef3855, undef3862, undef3889, undef4030, undef4101, undef4262, undef4266, undef4267, undef4276, undef4277, undef4282, undef4312, undef4393, undef4453, undef4547, undef4612, undef4614, undef4615, undef4616, undef4618, undef4619, undef4623, undef4630, undef4631, undef4632, undef4635, undef4636, undef4637, undef4642, undef4643, undef4667, undef4831, undef4832, undef4841, undef4848, undef4849, undef4961, undef4964, undef4966, undef4967, undef4968, undef4971, undef4975, undef4983, undef4984, undef4985, undef4987, undef4988, undef4989, undef4990, undef4991, undef4992, undef4993, undef4994, undef4995, undef4996, undef4997, undef4998, undef4999, undef5000, undef5001, undef5002, undef5003, undef5004, undef5005, undef5006, undef5007, undef5008, undef5009, undef5010, undef5054, undef5058, undef5070, undef5071, undef5075, undef5076, 

Abstraction variables:

Exit nodes:

Accepting locations:

Asserts:

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

Init Location: 0
Graph 0:
Transitions:
Variables:

Graph 1:
Transitions:
<l39, l39, 0 <= i_30^0 /\ 1 + i_30^0 <= length_29^0 /\ 1 + undef4832 <= length_29^0 /\ temp_35^0 = undef4849 /\ 1 + i_30^0 = undef4831 /\ undef4831 = 1 + undef4832, {head_32^0 -> undef4849, i_30^0 -> undef4831, temp_35^0 -> undef4848, rest remain the same}>
Variables:
head_32^0, i_30^0, length_29^0, temp_35^0

Graph 2:
Transitions:
<l42, l42, 0 <= a_147^0 /\ 0 <= len_132^0 /\ 2 <= undef3162 /\ __disjvr_21^0 = undef3185 /\ __disjvr_22^0 = undef3326 /\ __disjvr_23^0 = undef3397 /\ head_27^0 = undef3140 /\ undef3142 = undef3146 /\ undef3275 = undef3484 /\ undef3292 = undef3501 /\ 1 + len_132^0 = undef3292 /\ a_147^0 = 1 + undef3275, {__disjvr_21^0 -> undef3185, __disjvr_22^0 -> undef3326, __disjvr_23^0 -> undef3397, a_147^0 -> undef3484, head_14^0 -> undef3142, len_132^0 -> undef3501, rest remain the same}>
Variables:
__disjvr_21^0, __disjvr_22^0, __disjvr_23^0, a_147^0, head_14^0, head_27^0, len_132^0

Graph 3:
Transitions:
<l1, l1, 0 <= a_237^0 /\ 2 <= undef136 /\ __disjvr_0^0 = undef146 /\ __disjvr_1^0 = undef297 /\ __disjvr_2^0 = undef378 /\ __disjvr_3^0 = undef450 /\ y_19^0 = 0 /\ y_19^0 = undef113 /\ undef113 = 0 /\ undef116 = undef142 /\ undef116 = undef144 /\ undef142 = undef144 /\ undef252 = undef531 /\ a_237^0 = 1 + undef252, {__disjvr_0^0 -> undef146, __disjvr_1^0 -> undef297, __disjvr_2^0 -> undef378, __disjvr_3^0 -> undef450, a_237^0 -> undef531, head_14^0 -> undef116, rest remain the same}>
Variables:
__disjvr_0^0, __disjvr_1^0, __disjvr_2^0, __disjvr_3^0, a_237^0, head_14^0, y_19^0

Graph 4:
Transitions:
Variables:

Precedence: 
Graph 0

Graph 1
<l0, l39, 1 + undef2868 <= undef2872 /\ 1 + undef5058 <= undef2872 /\ 2 <= undef2872 /\ temp_35^0 = undef5076 /\ undef2794 = undef2810 /\ undef2794 = undef2816 /\ undef2810 = undef2816 /\ undef2811 = undef2872 /\ undef2816 = undef5075 /\ undef2864 = 0 /\ undef2868 = 0 /\ undef2872 = undef2881 /\ undef2872 = undef5071 /\ undef2881 = undef2891 /\ undef5054 = undef5070 /\ undef5054 = undef5076 /\ undef5070 = undef5076 /\ 1 + undef2868 = undef5058 /\ undef2798 = 1 + undef5058 /\ undef5058 = 1 /\ undef2798 = 2, {head_32^0 -> undef2794, i_30^0 -> undef2798, length_29^0 -> undef2872, temp_35^0 -> undef2815, rest remain the same}>

Graph 2
<l39, l42, 0 <= i_30^0 /\ length_29^0 <= i_30^0 /\ undef4632 <= undef4618 /\ undef4632 <= undef4619 /\ 2 <= undef4632 /\ __disjvr_30^0 = undef4667 /\ a_147^0 = undef4619 /\ head_32^0 = undef4643 /\ len_132^0 = 0 /\ undef4612 = undef4614 /\ undef4612 = undef4616 /\ undef4612 = undef4642 /\ undef4614 = undef4616 /\ undef4642 = undef4643, {__disjvr_30^0 -> undef4667, head_14^0 -> undef4612, head_27^0 -> undef4614, head_32^0 -> undef4615, i_30^0 -> undef4619, length_29^0 -> undef4623, temp_35^0 -> undef4636, rest remain the same}>

Graph 3
<l42, l1, 0 <= a_147^0 /\ 0 <= len_132^0 /\ 2 <= undef1401 /\ 2 <= undef2952 /\ __disjvr_10^0 = undef1552 /\ __disjvr_11^0 = undef1623 /\ __disjvr_12^0 = undef1694 /\ __disjvr_20^0 = undef2974 /\ __disjvr_9^0 = undef1441 /\ a_237^0 = undef1515 /\ head_14^0 = undef2958 /\ head_14^0 = undef2959 /\ head_14^0 = undef2960 /\ head_27^0 = 0 /\ undef1378 = 0 /\ undef1378 = undef2961 /\ undef1381 = undef1407 /\ undef1381 = undef1409 /\ undef1381 = undef1542 /\ undef1407 = undef1409 /\ undef1542 = undef2959 /\ undef2929 = 0 /\ undef2929 = undef2961 /\ undef2958 = undef2960 /\ undef2959 = undef2960 /\ undef2961 = 0 /\ 1 + undef1515 = undef1810, {__disjvr_10^0 -> undef1552, __disjvr_11^0 -> undef1623, __disjvr_12^0 -> undef1694, __disjvr_20^0 -> undef2974, __disjvr_9^0 -> undef1441, a_215^0 -> undef1515, head_14^0 -> undef1381, head_27^0 -> undef2934, len_132^0 -> undef1810, x_20^0 -> undef2959, y_19^0 -> undef2961, rest remain the same}>

Graph 4
<l0, l2, undef2872 <= undef2868 /\ undef4984 <= 0 /\ undef5000 <= 0 /\ undef5001 <= 0 /\ undef2864 = 0 /\ undef2864 = undef5003 /\ undef2868 = 0 /\ undef2872 = undef2881 /\ undef2881 = undef2891 /\ undef4964 = 0 /\ undef4964 = undef4997 /\ undef4964 = undef4998 /\ undef4964 = undef5004 /\ undef4994 = 0 /\ undef4994 = undef5009 /\ undef4996 = 0 /\ undef4996 = undef4997 /\ undef4997 = 0 /\ undef4998 = undef5003 /\ undef5004 = 0 /\ undef5004 = undef5007 /\ undef5005 = 0 /\ undef5005 = undef5007 /\ undef5005 = undef5009 /\ undef5007 = 0 /\ undef5009 = 0, {head_14^0 -> undef4964, head_27^0 -> undef4966, head_32^0 -> undef4967, i_30^0 -> undef4971, length_29^0 -> undef4975, temp_35^0 -> undef4988, x_20^0 -> undef4991, y_19^0 -> undef4993, rest remain the same}>
<l0, l2, undef2872 <= undef5058 /\ 1 + undef2868 <= undef2872 /\ 1 <= undef2872 /\ __disjvr_13^0 = undef1910 /\ __disjvr_14^0 = undef2051 /\ __disjvr_15^0 = undef2192 /\ __disjvr_16^0 = undef2333 /\ __disjvr_17^0 = undef2474 /\ __disjvr_18^0 = undef2545 /\ __disjvr_19^0 = undef2691 /\ temp_35^0 = undef5076 /\ undef1871 = undef1875 /\ undef1871 = undef2182 /\ undef1871 = undef2183 /\ undef1871 = undef2184 /\ undef1873 = 0 /\ undef1873 = undef1901 /\ undef1873 = undef1902 /\ undef1901 = undef1902 /\ undef1901 = undef1903 /\ undef1903 = undef1905 /\ undef1905 = undef5054 /\ undef2153 = 0 /\ undef2153 = undef2185 /\ undef2182 = undef2184 /\ undef2183 = 0 /\ undef2183 = undef2184 /\ undef2183 = undef2185 /\ undef2183 = undef2457 /\ undef2185 = 0 /\ undef2185 = undef2293 /\ undef2293 = 0 /\ undef2296 = undef2322 /\ undef2296 = undef2324 /\ undef2296 = undef2457 /\ undef2322 = undef2324 /\ undef2864 = 0 /\ undef2868 = 0 /\ undef2872 = undef2881 /\ undef2872 = undef5071 /\ undef2881 = undef2891 /\ undef5054 = undef5070 /\ undef5054 = undef5076 /\ undef5070 = undef5076 /\ 1 + undef2868 = undef5058 /\ undef1891 = 1 /\ undef1904 = 1 /\ undef2176 = 1 /\ undef2316 = 1 /\ undef5058 = 1, {__disjvr_13^0 -> undef1910, __disjvr_14^0 -> undef2051, __disjvr_15^0 -> undef2192, __disjvr_16^0 -> undef2333, __disjvr_17^0 -> undef2474, __disjvr_18^0 -> undef2545, __disjvr_19^0 -> undef2691, head_14^0 -> undef2646, head_27^0 -> undef2158, head_32^0 -> undef1874, i_30^0 -> undef1878, length_29^0 -> undef1882, temp_35^0 -> undef1895, x_20^0 -> undef2673, y_19^0 -> undef2675, rest remain the same}>
<l1, l2, 0 <= a_237^0 /\ 2 <= undef61 /\ x_20^0 = y_19^0, {x_20^0 -> undef68, y_19^0 -> undef70, rest remain the same}>

Map Locations to Subgraph:
( 0 , 0 )
( 1 , 3 )
( 2 , 4 )
( 39 , 1 )
( 42 , 2 )

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

Proving termination of subgraph 0
Proving termination of subgraph 1
Checking unfeasibility...
Time used: 0.002364

Checking conditional termination of SCC {l39}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002194s
Ranking function: -1 - i_30^0 + length_29^0
New Graphs: 
Proving termination of subgraph 2
Checking unfeasibility...
Time used: 0.003126

Checking conditional termination of SCC {l42}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002365s
Ranking function: a_147^0
New Graphs: 
Proving termination of subgraph 3
Checking unfeasibility...
Time used: 0.003275

Checking conditional termination of SCC {l1}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.002406s
Ranking function: a_237^0
New Graphs: 
Proving termination of subgraph 4
Analyzing SCC {l2}...
No cycles found.

Program Terminates