NO

Initial ITS
Start location: l14
   0: l0 -> l2 : __disjvr_2^0'=__disjvr_2^post0, lt_23^0'=lt_23^post0, k_191^0'=k_191^post0, y_12^0'=y_12^post0, w_15^0'=w_15^post0, __cil_tmp5_10^0'=__cil_tmp5_10^post0, len_87^0'=len_87^post0, a_11^0'=a_11^post0, lt_28^0'=lt_28^post0, lt_25^0'=lt_25^post0, y_20^0'=y_20^post0, x_17^0'=x_17^post0, __disjvr_4^0'=__disjvr_4^post0, __disjvr_1^0'=__disjvr_1^post0, lt_22^0'=lt_22^post0, k_145^0'=k_145^post0, tmp_9^0'=tmp_9^post0, lt_27^0'=lt_27^post0, Result_4^0'=Result_4^post0, x_8^0'=x_8^post0, __patmp2^0'=__patmp2^post0, __disjvr_3^0'=__disjvr_3^post0, lt_24^0'=lt_24^post0, len_165^0'=len_165^post0, y_18^0'=y_18^post0, x_13^0'=x_13^post0, __disjvr_0^0'=__disjvr_0^post0, lt_21^0'=lt_21^post0, k_110^0'=k_110^post0, t_16^0'=t_16^post0, lt_26^0'=lt_26^post0, x_19^0'=x_19^post0, __patmp1^0'=__patmp1^post0, (__disjvr_1^0-__disjvr_1^post0 == 0 /\ lt_27^0-lt_27^post0 == 0 /\ Result_4^0-Result_4^post0 == 0 /\ -__disjvr_4^post0+__disjvr_4^0 == 0 /\ -len_165^post0+len_165^0 == 0 /\ len_87^0-len_87^post0 == 0 /\ -__disjvr_0^post0+__disjvr_0^0 == 0 /\ x_8^0-x_8^post0 == 0 /\ -lt_24^post0+lt_24^0 == 0 /\ -x_19^post0+x_19^0 == 0 /\ -k_110^post0+k_110^0 == 0 /\ lt_23^0-lt_23^post0 == 0 /\ -__patmp1^post0+__patmp1^0 == 0 /\ k_191^0-k_191^post0 == 0 /\ -x_13^post0+x_13^0 == 0 /\ lt_25^0-lt_25^post0 == 0 /\ -y_18^post0+y_18^0 == 0 /\ __disjvr_0^post0-__disjvr_0^0 == 0 /\ tmp_9^0-tmp_9^post0 == 0 /\ lt_22^0-lt_22^post0 == 0 /\ -t_16^post0+t_16^0 == 0 /\ __disjvr_3^0-__disjvr_3^post0 == 0 /\ x_17^0-x_17^post0 == 0 /\ a_11^0-a_11^post0 == 0 /\ -y_12^post0+y_12^0 == 0 /\ y_20^0-y_20^post0 == 0 /\ -__patmp2^post0+__patmp2^0 == 0 /\ w_15^0-w_15^post0 == 0 /\ -lt_28^post0+lt_28^0 == 0 /\ -lt_26^post0+lt_26^0 == 0 /\ __cil_tmp5_10^0-__cil_tmp5_10^post0 == 0 /\ -lt_21^post0+lt_21^0 == 0 /\ -k_145^post0+k_145^0 == 0 /\ __disjvr_2^0-__disjvr_2^post0 == 0), cost: 1
   1: l2 -> l1 : __disjvr_2^0'=__disjvr_2^post1, lt_23^0'=lt_23^post1, k_191^0'=k_191^post1, y_12^0'=y_12^post1, w_15^0'=w_15^post1, __cil_tmp5_10^0'=__cil_tmp5_10^post1, len_87^0'=len_87^post1, a_11^0'=a_11^post1, lt_28^0'=lt_28^post1, lt_25^0'=lt_25^post1, y_20^0'=y_20^post1, x_17^0'=x_17^post1, __disjvr_4^0'=__disjvr_4^post1, __disjvr_1^0'=__disjvr_1^post1, lt_22^0'=lt_22^post1, k_145^0'=k_145^post1, tmp_9^0'=tmp_9^post1, lt_27^0'=lt_27^post1, Result_4^0'=Result_4^post1, x_8^0'=x_8^post1, __patmp2^0'=__patmp2^post1, __disjvr_3^0'=__disjvr_3^post1, lt_24^0'=lt_24^post1, len_165^0'=len_165^post1, y_18^0'=y_18^post1, x_13^0'=x_13^post1, __disjvr_0^0'=__disjvr_0^post1, lt_21^0'=lt_21^post1, k_110^0'=k_110^post1, t_16^0'=t_16^post1, lt_26^0'=lt_26^post1, x_19^0'=x_19^post1, __patmp1^0'=__patmp1^post1, (-x_13^post1+x_13^0 == 0 /\ k_191^0-k_191^post1 == 0 /\ lt_28^0-lt_28^post1 == 0 /\ -x_8^post1+x_8^0 == 0 /\ x_17^0-x_17^post1 == 0 /\ t_16^post1-x_17^0 == 0 /\ -k_110^post1+k_110^0 == 0 /\ w_15^0-w_15^post1 == 0 /\ __disjvr_2^0-__disjvr_2^post1 == 0 /\ y_12^0-y_12^post1 == 0 /\ -t_16^post1+y_18^post1 == 0 /\ -__disjvr_0^post1+__disjvr_0^0 == 0 /\ -lt_22^post1+lt_22^0 == 0 /\ -__patmp1^post1+__patmp1^0 == 0 /\ len_87^0-len_87^post1 == 0 /\ __patmp2^0-__patmp2^post1 == 0 /\ lt_23^0-lt_23^post1 == 0 /\ -a_11^post1+a_11^0 == 0 /\ -lt_26^post1+lt_26^0 == 0 /\ lt_25^0-lt_25^post1 == 0 /\ y_20^0-y_20^post1 == 0 /\ -k_145^post1+k_145^0 == 0 /\ __disjvr_1^0-__disjvr_1^post1 == 0 /\ -lt_21^post1+lt_21^0 == 0 /\ -Result_4^post1+Result_4^0 == 0 /\ -len_165^post1+len_165^0 == 0 /\ __disjvr_3^0-__disjvr_3^post1 == 0 /\ tmp_9^0-tmp_9^post1 == 0 /\ -lt_24^post1+lt_24^0 == 0 /\ -__cil_tmp5_10^post1+__cil_tmp5_10^0 == 0 /\ -lt_27^post1+lt_27^0 == 0 /\ __disjvr_4^0-__disjvr_4^post1 == 0 /\ -x_19^post1+x_19^0 == 0), cost: 1
   2: l1 -> l0 : __disjvr_2^0'=__disjvr_2^post2, lt_23^0'=lt_23^post2, k_191^0'=k_191^post2, y_12^0'=y_12^post2, w_15^0'=w_15^post2, __cil_tmp5_10^0'=__cil_tmp5_10^post2, len_87^0'=len_87^post2, a_11^0'=a_11^post2, lt_28^0'=lt_28^post2, lt_25^0'=lt_25^post2, y_20^0'=y_20^post2, x_17^0'=x_17^post2, __disjvr_4^0'=__disjvr_4^post2, __disjvr_1^0'=__disjvr_1^post2, lt_22^0'=lt_22^post2, k_145^0'=k_145^post2, tmp_9^0'=tmp_9^post2, lt_27^0'=lt_27^post2, Result_4^0'=Result_4^post2, x_8^0'=x_8^post2, __patmp2^0'=__patmp2^post2, __disjvr_3^0'=__disjvr_3^post2, lt_24^0'=lt_24^post2, len_165^0'=len_165^post2, y_18^0'=y_18^post2, x_13^0'=x_13^post2, __disjvr_0^0'=__disjvr_0^post2, lt_21^0'=lt_21^post2, k_110^0'=k_110^post2, t_16^0'=t_16^post2, lt_26^0'=lt_26^post2, x_19^0'=x_19^post2, __patmp1^0'=__patmp1^post2, (lt_23^0-lt_23^post2 == 0 /\ -lt_22^post2+lt_22^0 == 0 /\ -Result_4^post2+Result_4^0 == 0 /\ lt_21^0-lt_21^post2 == 0 /\ y_20^0-y_20^post2 == 0 /\ y_12^0-y_12^post2 == 0 /\ __patmp2^0-__patmp2^post2 == 0 /\ a_11^0-a_11^post2 == 0 /\ -t_16^post2+t_16^0 == 0 /\ -y_18^post2+y_18^0 == 0 /\ -__disjvr_3^post2+__disjvr_3^0 == 0 /\ -__patmp1^post2+__patmp1^0 == 0 /\ -__disjvr_0^post2+__disjvr_0^0 == 0 /\ -x_17^post2+x_17^0 == 0 /\ -lt_26^post2+lt_26^0 == 0 /\ lt_28^0-lt_28^post2 == 0 /\ __disjvr_4^0-__disjvr_4^post2 == 0 /\ k_145^0-k_145^post2 == 0 /\ tmp_9^0-tmp_9^post2 == 0 /\ len_87^0-len_87^post2 == 0 /\ __disjvr_2^0-__disjvr_2^post2 == 0 /\ -k_110^post2+k_110^0 == 0 /\ -x_8^post2+x_8^0 == 0 /\ -x_19^post2+x_19^0 == 0 /\ __cil_tmp5_10^0-__cil_tmp5_10^post2 == 0 /\ -len_165^post2+len_165^0 == 0 /\ k_191^0-k_191^post2 == 0 /\ lt_25^0-lt_25^post2 == 0 /\ x_13^0-x_13^post2 == 0 /\ -lt_27^post2+lt_27^0 == 0 /\ __disjvr_1^0-__disjvr_1^post2 == 0 /\ -lt_24^post2+lt_24^0 == 0 /\ -w_15^post2+w_15^0 == 0), cost: 1
   3: l3 -> l5 : __disjvr_2^0'=__disjvr_2^post3, lt_23^0'=lt_23^post3, k_191^0'=k_191^post3, y_12^0'=y_12^post3, w_15^0'=w_15^post3, __cil_tmp5_10^0'=__cil_tmp5_10^post3, len_87^0'=len_87^post3, a_11^0'=a_11^post3, lt_28^0'=lt_28^post3, lt_25^0'=lt_25^post3, y_20^0'=y_20^post3, x_17^0'=x_17^post3, __disjvr_4^0'=__disjvr_4^post3, __disjvr_1^0'=__disjvr_1^post3, lt_22^0'=lt_22^post3, k_145^0'=k_145^post3, tmp_9^0'=tmp_9^post3, lt_27^0'=lt_27^post3, Result_4^0'=Result_4^post3, x_8^0'=x_8^post3, __patmp2^0'=__patmp2^post3, __disjvr_3^0'=__disjvr_3^post3, lt_24^0'=lt_24^post3, len_165^0'=len_165^post3, y_18^0'=y_18^post3, x_13^0'=x_13^post3, __disjvr_0^0'=__disjvr_0^post3, lt_21^0'=lt_21^post3, k_110^0'=k_110^post3, t_16^0'=t_16^post3, lt_26^0'=lt_26^post3, x_19^0'=x_19^post3, __patmp1^0'=__patmp1^post3, (0 == 0 /\ y_20^post3 == 0 /\ y_12^0-y_12^post3 == 0 /\ __patmp2^0-__patmp2^post3 == 0 /\ -__patmp1^post3+__patmp1^0 == 0 /\ -__disjvr_4^post3+__disjvr_4^0 == 0 /\ -a_11^0+x_13^post3 == 0 /\ -lt_22^post3+lt_22^0 == 0 /\ -t_16^post3+t_16^0 == 0 /\ -lt_25^post3+lt_25^0 == 0 /\ -y_18^post3+y_18^0 == 0 /\ __cil_tmp5_10^post3-x_8^post3 == 0 /\ x_17^0-x_17^post3 == 0 /\ k_145^0-k_145^post3 == 0 /\ -x_8^10+__cil_tmp5_10^10 == 0 /\ -lt_24^post3+lt_24^0 == 0 /\ -len_87^post3 <= 0 /\ __disjvr_2^0-__disjvr_2^post3 == 0 /\ __disjvr_1^0-__disjvr_1^post3 == 0 /\ k_191^0-k_191^post3 == 0 /\ Result_4^10-__cil_tmp5_10^10 == 0 /\ -2+len_87^post3 == 0 /\ a_11^0-a_11^post3 == 0 /\ x_8^post3-tmp_9^post3 == 0 /\ -len_165^post3+len_165^0 == 0 /\ Result_4^post3-__cil_tmp5_10^post3 == 0 /\ -tmp_9^10+x_8^10 == 0 /\ __disjvr_3^0-__disjvr_3^post3 == 0 /\ w_15^0-w_15^post3 == 0 /\ lt_23^0-lt_23^post3 == 0 /\ -__disjvr_0^post3+__disjvr_0^0 == 0 /\ -lt_21^post3+lt_21^0 == 0 /\ k_110^post3-len_87^post3 == 0), cost: 1
   4: l5 -> l6 : __disjvr_2^0'=__disjvr_2^post4, lt_23^0'=lt_23^post4, k_191^0'=k_191^post4, y_12^0'=y_12^post4, w_15^0'=w_15^post4, __cil_tmp5_10^0'=__cil_tmp5_10^post4, len_87^0'=len_87^post4, a_11^0'=a_11^post4, lt_28^0'=lt_28^post4, lt_25^0'=lt_25^post4, y_20^0'=y_20^post4, x_17^0'=x_17^post4, __disjvr_4^0'=__disjvr_4^post4, __disjvr_1^0'=__disjvr_1^post4, lt_22^0'=lt_22^post4, k_145^0'=k_145^post4, tmp_9^0'=tmp_9^post4, lt_27^0'=lt_27^post4, Result_4^0'=Result_4^post4, x_8^0'=x_8^post4, __patmp2^0'=__patmp2^post4, __disjvr_3^0'=__disjvr_3^post4, lt_24^0'=lt_24^post4, len_165^0'=len_165^post4, y_18^0'=y_18^post4, x_13^0'=x_13^post4, __disjvr_0^0'=__disjvr_0^post4, lt_21^0'=lt_21^post4, k_110^0'=k_110^post4, t_16^0'=t_16^post4, lt_26^0'=lt_26^post4, x_19^0'=x_19^post4, __patmp1^0'=__patmp1^post4, (len_87^0-len_87^post4 == 0 /\ w_15^0-w_15^post4 == 0 /\ -lt_24^post4+lt_24^0 == 0 /\ y_20^0-y_20^post4 == 0 /\ y_12^0-y_12^post4 == 0 /\ -lt_26^post4+lt_26^0 == 0 /\ -Result_4^post4+Result_4^0 == 0 /\ -x_19^post4+x_19^0 == 0 /\ -len_165^post4+len_165^0 == 0 /\ lt_25^0-lt_25^post4 == 0 /\ -__disjvr_0^post4+__disjvr_0^0 == 0 /\ lt_23^0-lt_23^post4 == 0 /\ lt_21^0-lt_21^post4 == 0 /\ -__disjvr_3^post4+__disjvr_3^0 == 0 /\ -__patmp2^post4+__patmp2^0 == 0 /\ -lt_27^post4+lt_27^0 == 0 /\ -tmp_9^post4+tmp_9^0 == 0 /\ x_13^0-x_13^post4 == 0 /\ k_191^0-k_191^post4 == 0 /\ -x_17^post4+x_17^0 == 0 /\ lt_22^0-lt_22^post4 == 0 /\ lt_28^0-lt_28^post4 == 0 /\ __disjvr_4^0-__disjvr_4^post4 == 0 /\ -__disjvr_1^post4+__disjvr_1^0 == 0 /\ -k_110^post4+k_110^0 == 0 /\ -__disjvr_2^post4+__disjvr_2^0 == 0 /\ -x_8^post4+x_8^0 == 0 /\ -__patmp1^post4+__patmp1^0 == 0 /\ k_145^0-k_145^post4 == 0 /\ -t_16^post4+t_16^0 == 0 /\ a_11^0-a_11^post4 == 0 /\ __cil_tmp5_10^0-__cil_tmp5_10^post4 == 0 /\ __disjvr_1^post4-__disjvr_1^0 == 0 /\ y_18^0-y_18^post4 == 0), cost: 1
   5: l6 -> l4 : __disjvr_2^0'=__disjvr_2^post5, lt_23^0'=lt_23^post5, k_191^0'=k_191^post5, y_12^0'=y_12^post5, w_15^0'=w_15^post5, __cil_tmp5_10^0'=__cil_tmp5_10^post5, len_87^0'=len_87^post5, a_11^0'=a_11^post5, lt_28^0'=lt_28^post5, lt_25^0'=lt_25^post5, y_20^0'=y_20^post5, x_17^0'=x_17^post5, __disjvr_4^0'=__disjvr_4^post5, __disjvr_1^0'=__disjvr_1^post5, lt_22^0'=lt_22^post5, k_145^0'=k_145^post5, tmp_9^0'=tmp_9^post5, lt_27^0'=lt_27^post5, Result_4^0'=Result_4^post5, x_8^0'=x_8^post5, __patmp2^0'=__patmp2^post5, __disjvr_3^0'=__disjvr_3^post5, lt_24^0'=lt_24^post5, len_165^0'=len_165^post5, y_18^0'=y_18^post5, x_13^0'=x_13^post5, __disjvr_0^0'=__disjvr_0^post5, lt_21^0'=lt_21^post5, k_110^0'=k_110^post5, t_16^0'=t_16^post5, lt_26^0'=lt_26^post5, x_19^0'=x_19^post5, __patmp1^0'=__patmp1^post5, (0 == 0 /\ -lt_21^post5+lt_21^0 == 0 /\ -y_18^post5+y_18^0 == 0 /\ len_87^0-len_87^post5 == 0 /\ -lt_26^post5+lt_26^0 == 0 /\ k_110^0-k_110^post5 == 0 /\ lt_25^0-lt_25^post5 == 0 /\ -y_20^post5+y_20^0 == 0 /\ -x_17^post5+x_17^0 == 0 /\ -x_19^post5+x_19^0 == 0 /\ -__disjvr_0^post5+__disjvr_0^0 == 0 /\ y_12^0-y_12^post5 == 0 /\ w_15^0-w_15^post5 == 0 /\ __disjvr_2^0-__disjvr_2^post5 == 0 /\ -k_110^0 <= 0 /\ -__patmp2^post5+k_145^post5 == 0 /\ -__disjvr_1^post5+__disjvr_1^0 == 0 /\ -Result_4^post5+Result_4^0 == 0 /\ -lt_27^post5+lt_27^0 == 0 /\ -x_8^post5+x_8^0 == 0 /\ -lt_22^post5+lt_22^0 == 0 /\ lt_28^0-lt_28^post5 == 0 /\ -__patmp1^post5+len_165^post5 == 0 /\ __disjvr_4^0-__disjvr_4^post5 == 0 /\ -1+__patmp1^post5 == 0 /\ k_191^0-k_191^post5 == 0 /\ -tmp_9^post5+tmp_9^0 == 0 /\ a_11^0-a_11^post5 == 0 /\ -lt_23^10+x_13^post5 == 0 /\ __disjvr_3^0-__disjvr_3^post5 == 0 /\ -t_16^post5+t_16^0 == 0 /\ __cil_tmp5_10^0-__cil_tmp5_10^post5 == 0 /\ __patmp2^post5-k_110^0 == 0), cost: 1
   6: l4 -> l7 : __disjvr_2^0'=__disjvr_2^post6, lt_23^0'=lt_23^post6, k_191^0'=k_191^post6, y_12^0'=y_12^post6, w_15^0'=w_15^post6, __cil_tmp5_10^0'=__cil_tmp5_10^post6, len_87^0'=len_87^post6, a_11^0'=a_11^post6, lt_28^0'=lt_28^post6, lt_25^0'=lt_25^post6, y_20^0'=y_20^post6, x_17^0'=x_17^post6, __disjvr_4^0'=__disjvr_4^post6, __disjvr_1^0'=__disjvr_1^post6, lt_22^0'=lt_22^post6, k_145^0'=k_145^post6, tmp_9^0'=tmp_9^post6, lt_27^0'=lt_27^post6, Result_4^0'=Result_4^post6, x_8^0'=x_8^post6, __patmp2^0'=__patmp2^post6, __disjvr_3^0'=__disjvr_3^post6, lt_24^0'=lt_24^post6, len_165^0'=len_165^post6, y_18^0'=y_18^post6, x_13^0'=x_13^post6, __disjvr_0^0'=__disjvr_0^post6, lt_21^0'=lt_21^post6, k_110^0'=k_110^post6, t_16^0'=t_16^post6, lt_26^0'=lt_26^post6, x_19^0'=x_19^post6, __patmp1^0'=__patmp1^post6, (0 == 0 /\ 1-k_145^0 <= 0 /\ -len_165^post6+len_165^0 == 0 /\ -a_11^post6+a_11^0 == 0 /\ y_12^0-y_12^post6 == 0 /\ w_15^0-w_15^post6 == 0 /\ -lt_25^10+x_17^post6 == 0 /\ __patmp2^0-__patmp2^post6 == 0 /\ len_87^0-len_87^post6 == 0 /\ __cil_tmp5_10^0-__cil_tmp5_10^post6 == 0 /\ -lt_22^post6+lt_22^0 == 0 /\ -x_8^post6+x_8^0 == 0 /\ lt_28^0-lt_28^post6 == 0 /\ y_20^0-y_20^post6 == 0 /\ lt_23^0-lt_23^post6 == 0 /\ -lt_24^post6+lt_24^0 == 0 /\ -x_19^post6+x_19^0 == 0 /\ -lt_27^post6+lt_27^0 == 0 /\ -lt_21^post6+lt_21^0 == 0 /\ -k_145^post6+k_145^0 == 0 /\ y_12^0-x_13^0 <= 0 /\ -w_15^0+y_18^post6 == 0 /\ -len_165^0 <= 0 /\ __disjvr_1^0-__disjvr_1^post6 == 0 /\ -__disjvr_2^post6+__disjvr_2^0 == 0 /\ -y_12^0+x_13^0 <= 0 /\ -t_16^post6+t_16^0 == 0 /\ k_191^0-k_191^post6 == 0 /\ -__disjvr_0^post6+__disjvr_0^0 == 0 /\ -k_110^post6+k_110^0 == 0 /\ x_13^0-x_13^post6 == 0 /\ -__patmp1^post6+__patmp1^0 == 0 /\ tmp_9^0-tmp_9^post6 == 0 /\ __disjvr_4^0-__disjvr_4^post6 == 0 /\ -__disjvr_3^post6+__disjvr_3^0 == 0), cost: 1
  11: l4 -> l12 : __disjvr_2^0'=__disjvr_2^post11, lt_23^0'=lt_23^post11, k_191^0'=k_191^post11, y_12^0'=y_12^post11, w_15^0'=w_15^post11, __cil_tmp5_10^0'=__cil_tmp5_10^post11, len_87^0'=len_87^post11, a_11^0'=a_11^post11, lt_28^0'=lt_28^post11, lt_25^0'=lt_25^post11, y_20^0'=y_20^post11, x_17^0'=x_17^post11, __disjvr_4^0'=__disjvr_4^post11, __disjvr_1^0'=__disjvr_1^post11, lt_22^0'=lt_22^post11, k_145^0'=k_145^post11, tmp_9^0'=tmp_9^post11, lt_27^0'=lt_27^post11, Result_4^0'=Result_4^post11, x_8^0'=x_8^post11, __patmp2^0'=__patmp2^post11, __disjvr_3^0'=__disjvr_3^post11, lt_24^0'=lt_24^post11, len_165^0'=len_165^post11, y_18^0'=y_18^post11, x_13^0'=x_13^post11, __disjvr_0^0'=__disjvr_0^post11, lt_21^0'=lt_21^post11, k_110^0'=k_110^post11, t_16^0'=t_16^post11, lt_26^0'=lt_26^post11, x_19^0'=x_19^post11, __patmp1^0'=__patmp1^post11, (__disjvr_0^0-__disjvr_0^post11 == 0 /\ -t_16^post11+t_16^0 == 0 /\ 1-k_145^0 <= 0 /\ -Result_4^post11+Result_4^0 == 0 /\ len_87^0-len_87^post11 == 0 /\ __disjvr_2^0-__disjvr_2^post11 == 0 /\ lt_25^0-lt_25^post11 == 0 /\ -y_20^post11+y_20^0 == 0 /\ lt_22^0-lt_22^post11 == 0 /\ -__patmp2^post11+__patmp2^0 == 0 /\ -tmp_9^post11+tmp_9^0 == 0 /\ -x_17^post11+x_17^0 == 0 /\ -lt_26^post11+lt_26^0 == 0 /\ -x_13^post11+x_13^0 == 0 /\ w_15^0-w_15^post11 == 0 /\ lt_27^0-lt_27^post11 == 0 /\ -__disjvr_3^post11+__disjvr_3^0 == 0 /\ -x_19^post11+x_19^0 == 0 /\ -x_8^post11+x_8^0 == 0 /\ -len_165^0 <= 0 /\ -k_110^post11+k_110^0 == 0 /\ y_12^0-y_12^post11 == 0 /\ -__patmp1^post11+__patmp1^0 == 0 /\ lt_28^0-lt_28^post11 == 0 /\ -__disjvr_1^post11+__disjvr_1^0 == 0 /\ k_145^0-k_145^post11 == 0 /\ __disjvr_4^0-__disjvr_4^post11 == 0 /\ len_165^0-len_165^post11 == 0 /\ a_11^0-a_11^post11 == 0 /\ y_18^0-y_18^post11 == 0 /\ 1-k_145^0+k_191^post11 == 0 /\ __cil_tmp5_10^0-__cil_tmp5_10^post11 == 0 /\ lt_24^0-lt_24^post11 == 0 /\ -lt_21^post11+lt_21^0 == 0 /\ lt_23^0-lt_23^post11 == 0), cost: 1
   7: l7 -> l8 : __disjvr_2^0'=__disjvr_2^post7, lt_23^0'=lt_23^post7, k_191^0'=k_191^post7, y_12^0'=y_12^post7, w_15^0'=w_15^post7, __cil_tmp5_10^0'=__cil_tmp5_10^post7, len_87^0'=len_87^post7, a_11^0'=a_11^post7, lt_28^0'=lt_28^post7, lt_25^0'=lt_25^post7, y_20^0'=y_20^post7, x_17^0'=x_17^post7, __disjvr_4^0'=__disjvr_4^post7, __disjvr_1^0'=__disjvr_1^post7, lt_22^0'=lt_22^post7, k_145^0'=k_145^post7, tmp_9^0'=tmp_9^post7, lt_27^0'=lt_27^post7, Result_4^0'=Result_4^post7, x_8^0'=x_8^post7, __patmp2^0'=__patmp2^post7, __disjvr_3^0'=__disjvr_3^post7, lt_24^0'=lt_24^post7, len_165^0'=len_165^post7, y_18^0'=y_18^post7, x_13^0'=x_13^post7, __disjvr_0^0'=__disjvr_0^post7, lt_21^0'=lt_21^post7, k_110^0'=k_110^post7, t_16^0'=t_16^post7, lt_26^0'=lt_26^post7, x_19^0'=x_19^post7, __patmp1^0'=__patmp1^post7, (-__disjvr_4^post7+__disjvr_4^0 == 0 /\ -lt_25^post7+lt_25^0 == 0 /\ lt_28^0-lt_28^post7 == 0 /\ -__disjvr_1^post7+__disjvr_1^0 == 0 /\ -__disjvr_2^0+__disjvr_2^post7 == 0 /\ x_17^0-x_17^post7 == 0 /\ -tmp_9^post7+tmp_9^0 == 0 /\ -k_110^post7+k_110^0 == 0 /\ a_11^0-a_11^post7 == 0 /\ w_15^0-w_15^post7 == 0 /\ -__patmp1^post7+__patmp1^0 == 0 /\ -y_20^post7+y_20^0 == 0 /\ __disjvr_2^0-__disjvr_2^post7 == 0 /\ -x_13^post7+x_13^0 == 0 /\ y_12^0-y_12^post7 == 0 /\ -t_16^post7+t_16^0 == 0 /\ lt_22^0-lt_22^post7 == 0 /\ __disjvr_0^0-__disjvr_0^post7 == 0 /\ __cil_tmp5_10^0-__cil_tmp5_10^post7 == 0 /\ -__disjvr_3^post7+__disjvr_3^0 == 0 /\ lt_27^0-lt_27^post7 == 0 /\ -lt_21^post7+lt_21^0 == 0 /\ lt_23^0-lt_23^post7 == 0 /\ y_18^0-y_18^post7 == 0 /\ x_8^0-x_8^post7 == 0 /\ len_87^0-len_87^post7 == 0 /\ -lt_26^post7+lt_26^0 == 0 /\ k_145^0-k_145^post7 == 0 /\ -x_19^post7+x_19^0 == 0 /\ len_165^0-len_165^post7 == 0 /\ -__patmp2^post7+__patmp2^0 == 0 /\ -Result_4^post7+Result_4^0 == 0 /\ lt_24^0-lt_24^post7 == 0 /\ -k_191^post7+k_191^0 == 0), cost: 1
   8: l8 -> l9 : __disjvr_2^0'=__disjvr_2^post8, lt_23^0'=lt_23^post8, k_191^0'=k_191^post8, y_12^0'=y_12^post8, w_15^0'=w_15^post8, __cil_tmp5_10^0'=__cil_tmp5_10^post8, len_87^0'=len_87^post8, a_11^0'=a_11^post8, lt_28^0'=lt_28^post8, lt_25^0'=lt_25^post8, y_20^0'=y_20^post8, x_17^0'=x_17^post8, __disjvr_4^0'=__disjvr_4^post8, __disjvr_1^0'=__disjvr_1^post8, lt_22^0'=lt_22^post8, k_145^0'=k_145^post8, tmp_9^0'=tmp_9^post8, lt_27^0'=lt_27^post8, Result_4^0'=Result_4^post8, x_8^0'=x_8^post8, __patmp2^0'=__patmp2^post8, __disjvr_3^0'=__disjvr_3^post8, lt_24^0'=lt_24^post8, len_165^0'=len_165^post8, y_18^0'=y_18^post8, x_13^0'=x_13^post8, __disjvr_0^0'=__disjvr_0^post8, lt_21^0'=lt_21^post8, k_110^0'=k_110^post8, t_16^0'=t_16^post8, lt_26^0'=lt_26^post8, x_19^0'=x_19^post8, __patmp1^0'=__patmp1^post8, (t_16^post8-x_17^0 == 0 /\ lt_23^0-lt_23^post8 == 0 /\ -__patmp1^post8+__patmp1^0 == 0 /\ y_12^0-y_12^post8 == 0 /\ -__patmp2^post8+__patmp2^0 == 0 /\ x_8^0-x_8^post8 == 0 /\ -x_13^post8+x_13^0 == 0 /\ a_11^0-a_11^post8 == 0 /\ __disjvr_1^0-__disjvr_1^post8 == 0 /\ lt_27^0-lt_27^post8 == 0 /\ y_20^0-y_20^post8 == 0 /\ -len_87^post8+len_87^0 == 0 /\ -lt_25^post8+lt_25^0 == 0 /\ -lt_26^post8+lt_26^0 == 0 /\ lt_28^0-lt_28^post8 == 0 /\ -tmp_9^post8+tmp_9^0 == 0 /\ -x_19^post8+x_19^0 == 0 /\ -k_110^post8+k_110^0 == 0 /\ __disjvr_2^0-__disjvr_2^post8 == 0 /\ -len_165^post8+len_165^0 == 0 /\ __cil_tmp5_10^0-__cil_tmp5_10^post8 == 0 /\ -t_16^post8+y_18^post8 == 0 /\ k_191^0-k_191^post8 == 0 /\ -lt_21^post8+lt_21^0 == 0 /\ -k_145^post8+k_145^0 == 0 /\ __disjvr_3^0-__disjvr_3^post8 == 0 /\ x_17^0-x_17^post8 == 0 /\ -lt_24^post8+lt_24^0 == 0 /\ Result_4^0-Result_4^post8 == 0 /\ -__disjvr_4^post8+__disjvr_4^0 == 0 /\ -__disjvr_0^post8+__disjvr_0^0 == 0 /\ lt_22^0-lt_22^post8 == 0 /\ w_15^0-w_15^post8 == 0), cost: 1
   9: l9 -> l10 : __disjvr_2^0'=__disjvr_2^post9, lt_23^0'=lt_23^post9, k_191^0'=k_191^post9, y_12^0'=y_12^post9, w_15^0'=w_15^post9, __cil_tmp5_10^0'=__cil_tmp5_10^post9, len_87^0'=len_87^post9, a_11^0'=a_11^post9, lt_28^0'=lt_28^post9, lt_25^0'=lt_25^post9, y_20^0'=y_20^post9, x_17^0'=x_17^post9, __disjvr_4^0'=__disjvr_4^post9, __disjvr_1^0'=__disjvr_1^post9, lt_22^0'=lt_22^post9, k_145^0'=k_145^post9, tmp_9^0'=tmp_9^post9, lt_27^0'=lt_27^post9, Result_4^0'=Result_4^post9, x_8^0'=x_8^post9, __patmp2^0'=__patmp2^post9, __disjvr_3^0'=__disjvr_3^post9, lt_24^0'=lt_24^post9, len_165^0'=len_165^post9, y_18^0'=y_18^post9, x_13^0'=x_13^post9, __disjvr_0^0'=__disjvr_0^post9, lt_21^0'=lt_21^post9, k_110^0'=k_110^post9, t_16^0'=t_16^post9, lt_26^0'=lt_26^post9, x_19^0'=x_19^post9, __patmp1^0'=__patmp1^post9, (-__disjvr_0^post9+__disjvr_0^0 == 0 /\ -t_16^post9+t_16^0 == 0 /\ k_110^0-k_110^post9 == 0 /\ k_191^0-k_191^post9 == 0 /\ -lt_22^post9+lt_22^0 == 0 /\ __disjvr_2^0-__disjvr_2^post9 == 0 /\ lt_25^0-lt_25^post9 == 0 /\ -x_19^post9+x_19^0 == 0 /\ __disjvr_1^0-__disjvr_1^post9 == 0 /\ -lt_26^post9+lt_26^0 == 0 /\ lt_27^0-lt_27^post9 == 0 /\ Result_4^0-Result_4^post9 == 0 /\ x_17^0-x_17^post9 == 0 /\ -x_13^post9+x_13^0 == 0 /\ -k_145^post9+k_145^0 == 0 /\ w_15^0-w_15^post9 == 0 /\ -__disjvr_3^post9+__disjvr_3^0 == 0 /\ __patmp2^0-__patmp2^post9 == 0 /\ -len_165^post9+len_165^0 == 0 /\ -x_8^post9+x_8^0 == 0 /\ -lt_24^post9+lt_24^0 == 0 /\ -__cil_tmp5_10^post9+__cil_tmp5_10^0 == 0 /\ y_12^0-y_12^post9 == 0 /\ tmp_9^0-tmp_9^post9 == 0 /\ y_20^0-y_20^post9 == 0 /\ __disjvr_4^0-__disjvr_4^post9 == 0 /\ -__patmp1^post9+__patmp1^0 == 0 /\ -y_18^post9+y_18^0 == 0 /\ __disjvr_3^post9-__disjvr_3^0 == 0 /\ a_11^0-a_11^post9 == 0 /\ -lt_21^post9+lt_21^0 == 0 /\ -lt_28^post9+lt_28^0 == 0 /\ len_87^0-len_87^post9 == 0 /\ lt_23^0-lt_23^post9 == 0), cost: 1
  10: l10 -> l0 : __disjvr_2^0'=__disjvr_2^post10, lt_23^0'=lt_23^post10, k_191^0'=k_191^post10, y_12^0'=y_12^post10, w_15^0'=w_15^post10, __cil_tmp5_10^0'=__cil_tmp5_10^post10, len_87^0'=len_87^post10, a_11^0'=a_11^post10, lt_28^0'=lt_28^post10, lt_25^0'=lt_25^post10, y_20^0'=y_20^post10, x_17^0'=x_17^post10, __disjvr_4^0'=__disjvr_4^post10, __disjvr_1^0'=__disjvr_1^post10, lt_22^0'=lt_22^post10, k_145^0'=k_145^post10, tmp_9^0'=tmp_9^post10, lt_27^0'=lt_27^post10, Result_4^0'=Result_4^post10, x_8^0'=x_8^post10, __patmp2^0'=__patmp2^post10, __disjvr_3^0'=__disjvr_3^post10, lt_24^0'=lt_24^post10, len_165^0'=len_165^post10, y_18^0'=y_18^post10, x_13^0'=x_13^post10, __disjvr_0^0'=__disjvr_0^post10, lt_21^0'=lt_21^post10, k_110^0'=k_110^post10, t_16^0'=t_16^post10, lt_26^0'=lt_26^post10, x_19^0'=x_19^post10, __patmp1^0'=__patmp1^post10, (-a_11^post10+a_11^0 == 0 /\ -t_16^post10+y_18^post10 == 0 /\ -__disjvr_1^post10+__disjvr_1^0 == 0 /\ -lt_26^post10+lt_26^0 == 0 /\ y_12^0-y_12^post10 == 0 /\ w_15^0-w_15^post10 == 0 /\ -x_17^post10+x_17^0 == 0 /\ k_145^0-k_145^post10 == 0 /\ -Result_4^post10+Result_4^0 == 0 /\ lt_25^0-lt_25^post10 == 0 /\ __cil_tmp5_10^0-__cil_tmp5_10^post10 == 0 /\ len_87^0-len_87^post10 == 0 /\ -__disjvr_0^post10+__disjvr_0^0 == 0 /\ __patmp2^0-__patmp2^post10 == 0 /\ -x_17^0+t_16^post10 == 0 /\ -__disjvr_3^post10+__disjvr_3^0 == 0 /\ __disjvr_2^0-__disjvr_2^post10 == 0 /\ lt_23^0-lt_23^post10 == 0 /\ __disjvr_4^0-__disjvr_4^post10 == 0 /\ -lt_27^post10+lt_27^0 == 0 /\ tmp_9^0-tmp_9^post10 == 0 /\ -lt_22^post10+lt_22^0 == 0 /\ y_20^0-y_20^post10 == 0 /\ -x_8^post10+x_8^0 == 0 /\ lt_28^0-lt_28^post10 == 0 /\ lt_21^0-lt_21^post10 == 0 /\ -x_19^post10+x_19^0 == 0 /\ -len_165^post10+len_165^0 == 0 /\ x_13^0-x_13^post10 == 0 /\ -k_110^post10+k_110^0 == 0 /\ k_191^0-k_191^post10 == 0 /\ -__patmp1^post10+__patmp1^0 == 0 /\ -lt_24^post10+lt_24^0 == 0), cost: 1
  12: l12 -> l13 : __disjvr_2^0'=__disjvr_2^post12, lt_23^0'=lt_23^post12, k_191^0'=k_191^post12, y_12^0'=y_12^post12, w_15^0'=w_15^post12, __cil_tmp5_10^0'=__cil_tmp5_10^post12, len_87^0'=len_87^post12, a_11^0'=a_11^post12, lt_28^0'=lt_28^post12, lt_25^0'=lt_25^post12, y_20^0'=y_20^post12, x_17^0'=x_17^post12, __disjvr_4^0'=__disjvr_4^post12, __disjvr_1^0'=__disjvr_1^post12, lt_22^0'=lt_22^post12, k_145^0'=k_145^post12, tmp_9^0'=tmp_9^post12, lt_27^0'=lt_27^post12, Result_4^0'=Result_4^post12, x_8^0'=x_8^post12, __patmp2^0'=__patmp2^post12, __disjvr_3^0'=__disjvr_3^post12, lt_24^0'=lt_24^post12, len_165^0'=len_165^post12, y_18^0'=y_18^post12, x_13^0'=x_13^post12, __disjvr_0^0'=__disjvr_0^post12, lt_21^0'=lt_21^post12, k_110^0'=k_110^post12, t_16^0'=t_16^post12, lt_26^0'=lt_26^post12, x_19^0'=x_19^post12, __patmp1^0'=__patmp1^post12, (-__patmp2^post12+__patmp2^0 == 0 /\ -x_13^post12+x_13^0 == 0 /\ -lt_26^post12+lt_26^0 == 0 /\ x_17^0-x_17^post12 == 0 /\ lt_22^0-lt_22^post12 == 0 /\ __disjvr_4^post12-__disjvr_4^0 == 0 /\ y_12^0-y_12^post12 == 0 /\ lt_28^0-lt_28^post12 == 0 /\ -k_145^post12+k_145^0 == 0 /\ lt_27^0-lt_27^post12 == 0 /\ -lt_21^post12+lt_21^0 == 0 /\ x_8^0-x_8^post12 == 0 /\ -__disjvr_0^post12+__disjvr_0^0 == 0 /\ lt_23^0-lt_23^post12 == 0 /\ w_15^0-w_15^post12 == 0 /\ -__disjvr_4^post12+__disjvr_4^0 == 0 /\ __disjvr_3^0-__disjvr_3^post12 == 0 /\ a_11^0-a_11^post12 == 0 /\ __cil_tmp5_10^0-__cil_tmp5_10^post12 == 0 /\ -x_19^post12+x_19^0 == 0 /\ len_87^0-len_87^post12 == 0 /\ -y_20^post12+y_20^0 == 0 /\ -tmp_9^post12+tmp_9^0 == 0 /\ __disjvr_2^0-__disjvr_2^post12 == 0 /\ len_165^0-len_165^post12 == 0 /\ -__disjvr_1^post12+__disjvr_1^0 == 0 /\ k_191^0-k_191^post12 == 0 /\ -k_110^post12+k_110^0 == 0 /\ t_16^0-t_16^post12 == 0 /\ -y_18^post12+y_18^0 == 0 /\ -lt_25^post12+lt_25^0 == 0 /\ Result_4^0-Result_4^post12 == 0 /\ -lt_24^post12+lt_24^0 == 0 /\ -__patmp1^post12+__patmp1^0 == 0), cost: 1
  13: l13 -> l11 : __disjvr_2^0'=__disjvr_2^post13, lt_23^0'=lt_23^post13, k_191^0'=k_191^post13, y_12^0'=y_12^post13, w_15^0'=w_15^post13, __cil_tmp5_10^0'=__cil_tmp5_10^post13, len_87^0'=len_87^post13, a_11^0'=a_11^post13, lt_28^0'=lt_28^post13, lt_25^0'=lt_25^post13, y_20^0'=y_20^post13, x_17^0'=x_17^post13, __disjvr_4^0'=__disjvr_4^post13, __disjvr_1^0'=__disjvr_1^post13, lt_22^0'=lt_22^post13, k_145^0'=k_145^post13, tmp_9^0'=tmp_9^post13, lt_27^0'=lt_27^post13, Result_4^0'=Result_4^post13, x_8^0'=x_8^post13, __patmp2^0'=__patmp2^post13, __disjvr_3^0'=__disjvr_3^post13, lt_24^0'=lt_24^post13, len_165^0'=len_165^post13, y_18^0'=y_18^post13, x_13^0'=x_13^post13, __disjvr_0^0'=__disjvr_0^post13, lt_21^0'=lt_21^post13, k_110^0'=k_110^post13, t_16^0'=t_16^post13, lt_26^0'=lt_26^post13, x_19^0'=x_19^post13, __patmp1^0'=__patmp1^post13, (0 == 0 /\ -lt_21^10+x_13^post13 == 0 /\ -tmp_9^post13+tmp_9^0 == 0 /\ len_87^0-len_87^post13 == 0 /\ -__disjvr_3^post13+__disjvr_3^0 == 0 /\ len_165^post13-__patmp1^post13 == 0 /\ -__disjvr_1^post13+__disjvr_1^0 == 0 /\ lt_23^0-lt_23^post13 == 0 /\ -k_110^post13+k_110^0 == 0 /\ y_20^0-y_20^post13 == 0 /\ -Result_4^post13+Result_4^0 == 0 /\ -x_19^post13+x_19^0 == 0 /\ -lt_27^post13+lt_27^0 == 0 /\ -k_191^0+__patmp2^post13 == 0 /\ k_191^0-k_191^post13 == 0 /\ lt_25^0-lt_25^post13 == 0 /\ -1-len_165^0+__patmp1^post13 == 0 /\ -__disjvr_0^post13+__disjvr_0^0 == 0 /\ __cil_tmp5_10^0-__cil_tmp5_10^post13 == 0 /\ -t_16^post13+t_16^0 == 0 /\ -x_17^post13+x_17^0 == 0 /\ lt_28^0-lt_28^post13 == 0 /\ __disjvr_4^0-__disjvr_4^post13 == 0 /\ -len_165^0 <= 0 /\ -lt_24^post13+lt_24^0 == 0 /\ -y_18^post13+y_18^0 == 0 /\ -w_15^post13+w_15^0 == 0 /\ -x_8^post13+x_8^0 == 0 /\ k_145^post13-__patmp2^post13 == 0 /\ -lt_26^post13+lt_26^0 == 0 /\ y_12^0-y_12^post13 == 0 /\ __disjvr_2^0-__disjvr_2^post13 == 0 /\ -k_191^0 <= 0 /\ a_11^0-a_11^post13 == 0), cost: 1
  14: l11 -> l4 : __disjvr_2^0'=__disjvr_2^post14, lt_23^0'=lt_23^post14, k_191^0'=k_191^post14, y_12^0'=y_12^post14, w_15^0'=w_15^post14, __cil_tmp5_10^0'=__cil_tmp5_10^post14, len_87^0'=len_87^post14, a_11^0'=a_11^post14, lt_28^0'=lt_28^post14, lt_25^0'=lt_25^post14, y_20^0'=y_20^post14, x_17^0'=x_17^post14, __disjvr_4^0'=__disjvr_4^post14, __disjvr_1^0'=__disjvr_1^post14, lt_22^0'=lt_22^post14, k_145^0'=k_145^post14, tmp_9^0'=tmp_9^post14, lt_27^0'=lt_27^post14, Result_4^0'=Result_4^post14, x_8^0'=x_8^post14, __patmp2^0'=__patmp2^post14, __disjvr_3^0'=__disjvr_3^post14, lt_24^0'=lt_24^post14, len_165^0'=len_165^post14, y_18^0'=y_18^post14, x_13^0'=x_13^post14, __disjvr_0^0'=__disjvr_0^post14, lt_21^0'=lt_21^post14, k_110^0'=k_110^post14, t_16^0'=t_16^post14, lt_26^0'=lt_26^post14, x_19^0'=x_19^post14, __patmp1^0'=__patmp1^post14, (a_11^0-a_11^post14 == 0 /\ w_15^0-w_15^post14 == 0 /\ -y_18^post14+y_18^0 == 0 /\ y_20^0-y_20^post14 == 0 /\ -x_13^post14+x_13^0 == 0 /\ -k_145^post14+k_145^0 == 0 /\ k_110^0-k_110^post14 == 0 /\ lt_25^0-lt_25^post14 == 0 /\ y_12^0-y_12^post14 == 0 /\ -lt_21^post14+lt_21^0 == 0 /\ -lt_26^post14+lt_26^0 == 0 /\ -lt_28^post14+lt_28^0 == 0 /\ -__disjvr_0^post14+__disjvr_0^0 == 0 /\ -x_19^post14+x_19^0 == 0 /\ -__disjvr_4^post14+__disjvr_4^0 == 0 /\ lt_23^0-lt_23^post14 == 0 /\ __disjvr_1^0-__disjvr_1^post14 == 0 /\ Result_4^0-Result_4^post14 == 0 /\ -len_165^post14+len_165^0 == 0 /\ __patmp2^0-__patmp2^post14 == 0 /\ k_191^0-k_191^post14 == 0 /\ lt_22^0-lt_22^post14 == 0 /\ __disjvr_2^0-__disjvr_2^post14 == 0 /\ tmp_9^0-tmp_9^post14 == 0 /\ __cil_tmp5_10^0-__cil_tmp5_10^post14 == 0 /\ -x_8^post14+x_8^0 == 0 /\ x_17^0-x_17^post14 == 0 /\ -__patmp1^post14+__patmp1^0 == 0 /\ -len_87^post14+len_87^0 == 0 /\ __disjvr_3^0-__disjvr_3^post14 == 0 /\ t_16^0-t_16^post14 == 0 /\ -lt_27^post14+lt_27^0 == 0 /\ -lt_24^post14+lt_24^0 == 0), cost: 1
  15: l14 -> l3 : __disjvr_2^0'=__disjvr_2^post15, lt_23^0'=lt_23^post15, k_191^0'=k_191^post15, y_12^0'=y_12^post15, w_15^0'=w_15^post15, __cil_tmp5_10^0'=__cil_tmp5_10^post15, len_87^0'=len_87^post15, a_11^0'=a_11^post15, lt_28^0'=lt_28^post15, lt_25^0'=lt_25^post15, y_20^0'=y_20^post15, x_17^0'=x_17^post15, __disjvr_4^0'=__disjvr_4^post15, __disjvr_1^0'=__disjvr_1^post15, lt_22^0'=lt_22^post15, k_145^0'=k_145^post15, tmp_9^0'=tmp_9^post15, lt_27^0'=lt_27^post15, Result_4^0'=Result_4^post15, x_8^0'=x_8^post15, __patmp2^0'=__patmp2^post15, __disjvr_3^0'=__disjvr_3^post15, lt_24^0'=lt_24^post15, len_165^0'=len_165^post15, y_18^0'=y_18^post15, x_13^0'=x_13^post15, __disjvr_0^0'=__disjvr_0^post15, lt_21^0'=lt_21^post15, k_110^0'=k_110^post15, t_16^0'=t_16^post15, lt_26^0'=lt_26^post15, x_19^0'=x_19^post15, __patmp1^0'=__patmp1^post15, (-x_19^post15+x_19^0 == 0 /\ x_13^0-x_13^post15 == 0 /\ tmp_9^0-tmp_9^post15 == 0 /\ -x_8^post15+x_8^0 == 0 /\ __disjvr_4^0-__disjvr_4^post15 == 0 /\ -__disjvr_0^post15+__disjvr_0^0 == 0 /\ -len_165^post15+len_165^0 == 0 /\ x_17^0-x_17^post15 == 0 /\ -lt_27^post15+lt_27^0 == 0 /\ __patmp2^0-__patmp2^post15 == 0 /\ -lt_24^post15+lt_24^0 == 0 /\ k_110^0-k_110^post15 == 0 /\ k_191^0-k_191^post15 == 0 /\ -lt_28^post15+lt_28^0 == 0 /\ -Result_4^post15+Result_4^0 == 0 /\ -lt_22^post15+lt_22^0 == 0 /\ __disjvr_1^0-__disjvr_1^post15 == 0 /\ -__patmp1^post15+__patmp1^0 == 0 /\ k_145^0-k_145^post15 == 0 /\ a_11^0-a_11^post15 == 0 /\ -y_18^post15+y_18^0 == 0 /\ -__disjvr_3^post15+__disjvr_3^0 == 0 /\ lt_25^0-lt_25^post15 == 0 /\ w_15^0-w_15^post15 == 0 /\ -t_16^post15+t_16^0 == 0 /\ -lt_23^post15+lt_23^0 == 0 /\ __disjvr_2^0-__disjvr_2^post15 == 0 /\ len_87^0-len_87^post15 == 0 /\ -lt_21^post15+lt_21^0 == 0 /\ y_12^0-y_12^post15 == 0 /\ __cil_tmp5_10^0-__cil_tmp5_10^post15 == 0 /\ -lt_26^post15+lt_26^0 == 0 /\ y_20^0-y_20^post15 == 0), cost: 1


Applied preprocessing
Original rule:
l0 -> l2 : __disjvr_2^0'=__disjvr_2^post0, lt_23^0'=lt_23^post0, k_191^0'=k_191^post0, y_12^0'=y_12^post0, w_15^0'=w_15^post0, __cil_tmp5_10^0'=__cil_tmp5_10^post0, len_87^0'=len_87^post0, a_11^0'=a_11^post0, lt_28^0'=lt_28^post0, lt_25^0'=lt_25^post0, y_20^0'=y_20^post0, x_17^0'=x_17^post0, __disjvr_4^0'=__disjvr_4^post0, __disjvr_1^0'=__disjvr_1^post0, lt_22^0'=lt_22^post0, k_145^0'=k_145^post0, tmp_9^0'=tmp_9^post0, lt_27^0'=lt_27^post0, Result_4^0'=Result_4^post0, x_8^0'=x_8^post0, __patmp2^0'=__patmp2^post0, __disjvr_3^0'=__disjvr_3^post0, lt_24^0'=lt_24^post0, len_165^0'=len_165^post0, y_18^0'=y_18^post0, x_13^0'=x_13^post0, __disjvr_0^0'=__disjvr_0^post0, lt_21^0'=lt_21^post0, k_110^0'=k_110^post0, t_16^0'=t_16^post0, lt_26^0'=lt_26^post0, x_19^0'=x_19^post0, __patmp1^0'=__patmp1^post0, (__disjvr_1^0-__disjvr_1^post0 == 0 /\ lt_27^0-lt_27^post0 == 0 /\ Result_4^0-Result_4^post0 == 0 /\ -__disjvr_4^post0+__disjvr_4^0 == 0 /\ -len_165^post0+len_165^0 == 0 /\ len_87^0-len_87^post0 == 0 /\ -__disjvr_0^post0+__disjvr_0^0 == 0 /\ x_8^0-x_8^post0 == 0 /\ -lt_24^post0+lt_24^0 == 0 /\ -x_19^post0+x_19^0 == 0 /\ -k_110^post0+k_110^0 == 0 /\ lt_23^0-lt_23^post0 == 0 /\ -__patmp1^post0+__patmp1^0 == 0 /\ k_191^0-k_191^post0 == 0 /\ -x_13^post0+x_13^0 == 0 /\ lt_25^0-lt_25^post0 == 0 /\ -y_18^post0+y_18^0 == 0 /\ __disjvr_0^post0-__disjvr_0^0 == 0 /\ tmp_9^0-tmp_9^post0 == 0 /\ lt_22^0-lt_22^post0 == 0 /\ -t_16^post0+t_16^0 == 0 /\ __disjvr_3^0-__disjvr_3^post0 == 0 /\ x_17^0-x_17^post0 == 0 /\ a_11^0-a_11^post0 == 0 /\ -y_12^post0+y_12^0 == 0 /\ y_20^0-y_20^post0 == 0 /\ -__patmp2^post0+__patmp2^0 == 0 /\ w_15^0-w_15^post0 == 0 /\ -lt_28^post0+lt_28^0 == 0 /\ -lt_26^post0+lt_26^0 == 0 /\ __cil_tmp5_10^0-__cil_tmp5_10^post0 == 0 /\ -lt_21^post0+lt_21^0 == 0 /\ -k_145^post0+k_145^0 == 0 /\ __disjvr_2^0-__disjvr_2^post0 == 0), cost: 1
New rule:
l0 -> l2 : 0 == 0, cost: 1

Applied preprocessing
Original rule:
l2 -> l1 : __disjvr_2^0'=__disjvr_2^post1, lt_23^0'=lt_23^post1, k_191^0'=k_191^post1, y_12^0'=y_12^post1, w_15^0'=w_15^post1, __cil_tmp5_10^0'=__cil_tmp5_10^post1, len_87^0'=len_87^post1, a_11^0'=a_11^post1, lt_28^0'=lt_28^post1, lt_25^0'=lt_25^post1, y_20^0'=y_20^post1, x_17^0'=x_17^post1, __disjvr_4^0'=__disjvr_4^post1, __disjvr_1^0'=__disjvr_1^post1, lt_22^0'=lt_22^post1, k_145^0'=k_145^post1, tmp_9^0'=tmp_9^post1, lt_27^0'=lt_27^post1, Result_4^0'=Result_4^post1, x_8^0'=x_8^post1, __patmp2^0'=__patmp2^post1, __disjvr_3^0'=__disjvr_3^post1, lt_24^0'=lt_24^post1, len_165^0'=len_165^post1, y_18^0'=y_18^post1, x_13^0'=x_13^post1, __disjvr_0^0'=__disjvr_0^post1, lt_21^0'=lt_21^post1, k_110^0'=k_110^post1, t_16^0'=t_16^post1, lt_26^0'=lt_26^post1, x_19^0'=x_19^post1, __patmp1^0'=__patmp1^post1, (-x_13^post1+x_13^0 == 0 /\ k_191^0-k_191^post1 == 0 /\ lt_28^0-lt_28^post1 == 0 /\ -x_8^post1+x_8^0 == 0 /\ x_17^0-x_17^post1 == 0 /\ t_16^post1-x_17^0 == 0 /\ -k_110^post1+k_110^0 == 0 /\ w_15^0-w_15^post1 == 0 /\ __disjvr_2^0-__disjvr_2^post1 == 0 /\ y_12^0-y_12^post1 == 0 /\ -t_16^post1+y_18^post1 == 0 /\ -__disjvr_0^post1+__disjvr_0^0 == 0 /\ -lt_22^post1+lt_22^0 == 0 /\ -__patmp1^post1+__patmp1^0 == 0 /\ len_87^0-len_87^post1 == 0 /\ __patmp2^0-__patmp2^post1 == 0 /\ lt_23^0-lt_23^post1 == 0 /\ -a_11^post1+a_11^0 == 0 /\ -lt_26^post1+lt_26^0 == 0 /\ lt_25^0-lt_25^post1 == 0 /\ y_20^0-y_20^post1 == 0 /\ -k_145^post1+k_145^0 == 0 /\ __disjvr_1^0-__disjvr_1^post1 == 0 /\ -lt_21^post1+lt_21^0 == 0 /\ -Result_4^post1+Result_4^0 == 0 /\ -len_165^post1+len_165^0 == 0 /\ __disjvr_3^0-__disjvr_3^post1 == 0 /\ tmp_9^0-tmp_9^post1 == 0 /\ -lt_24^post1+lt_24^0 == 0 /\ -__cil_tmp5_10^post1+__cil_tmp5_10^0 == 0 /\ -lt_27^post1+lt_27^0 == 0 /\ __disjvr_4^0-__disjvr_4^post1 == 0 /\ -x_19^post1+x_19^0 == 0), cost: 1
New rule:
l2 -> l1 : y_18^0'=x_17^0, t_16^0'=x_17^0, TRUE, cost: 1

Applied preprocessing
Original rule:
l1 -> l0 : __disjvr_2^0'=__disjvr_2^post2, lt_23^0'=lt_23^post2, k_191^0'=k_191^post2, y_12^0'=y_12^post2, w_15^0'=w_15^post2, __cil_tmp5_10^0'=__cil_tmp5_10^post2, len_87^0'=len_87^post2, a_11^0'=a_11^post2, lt_28^0'=lt_28^post2, lt_25^0'=lt_25^post2, y_20^0'=y_20^post2, x_17^0'=x_17^post2, __disjvr_4^0'=__disjvr_4^post2, __disjvr_1^0'=__disjvr_1^post2, lt_22^0'=lt_22^post2, k_145^0'=k_145^post2, tmp_9^0'=tmp_9^post2, lt_27^0'=lt_27^post2, Result_4^0'=Result_4^post2, x_8^0'=x_8^post2, __patmp2^0'=__patmp2^post2, __disjvr_3^0'=__disjvr_3^post2, lt_24^0'=lt_24^post2, len_165^0'=len_165^post2, y_18^0'=y_18^post2, x_13^0'=x_13^post2, __disjvr_0^0'=__disjvr_0^post2, lt_21^0'=lt_21^post2, k_110^0'=k_110^post2, t_16^0'=t_16^post2, lt_26^0'=lt_26^post2, x_19^0'=x_19^post2, __patmp1^0'=__patmp1^post2, (lt_23^0-lt_23^post2 == 0 /\ -lt_22^post2+lt_22^0 == 0 /\ -Result_4^post2+Result_4^0 == 0 /\ lt_21^0-lt_21^post2 == 0 /\ y_20^0-y_20^post2 == 0 /\ y_12^0-y_12^post2 == 0 /\ __patmp2^0-__patmp2^post2 == 0 /\ a_11^0-a_11^post2 == 0 /\ -t_16^post2+t_16^0 == 0 /\ -y_18^post2+y_18^0 == 0 /\ -__disjvr_3^post2+__disjvr_3^0 == 0 /\ -__patmp1^post2+__patmp1^0 == 0 /\ -__disjvr_0^post2+__disjvr_0^0 == 0 /\ -x_17^post2+x_17^0 == 0 /\ -lt_26^post2+lt_26^0 == 0 /\ lt_28^0-lt_28^post2 == 0 /\ __disjvr_4^0-__disjvr_4^post2 == 0 /\ k_145^0-k_145^post2 == 0 /\ tmp_9^0-tmp_9^post2 == 0 /\ len_87^0-len_87^post2 == 0 /\ __disjvr_2^0-__disjvr_2^post2 == 0 /\ -k_110^post2+k_110^0 == 0 /\ -x_8^post2+x_8^0 == 0 /\ -x_19^post2+x_19^0 == 0 /\ __cil_tmp5_10^0-__cil_tmp5_10^post2 == 0 /\ -len_165^post2+len_165^0 == 0 /\ k_191^0-k_191^post2 == 0 /\ lt_25^0-lt_25^post2 == 0 /\ x_13^0-x_13^post2 == 0 /\ -lt_27^post2+lt_27^0 == 0 /\ __disjvr_1^0-__disjvr_1^post2 == 0 /\ -lt_24^post2+lt_24^0 == 0 /\ -w_15^post2+w_15^0 == 0), cost: 1
New rule:
l1 -> l0 : TRUE, cost: 1

Applied preprocessing
Original rule:
l3 -> l5 : __disjvr_2^0'=__disjvr_2^post3, lt_23^0'=lt_23^post3, k_191^0'=k_191^post3, y_12^0'=y_12^post3, w_15^0'=w_15^post3, __cil_tmp5_10^0'=__cil_tmp5_10^post3, len_87^0'=len_87^post3, a_11^0'=a_11^post3, lt_28^0'=lt_28^post3, lt_25^0'=lt_25^post3, y_20^0'=y_20^post3, x_17^0'=x_17^post3, __disjvr_4^0'=__disjvr_4^post3, __disjvr_1^0'=__disjvr_1^post3, lt_22^0'=lt_22^post3, k_145^0'=k_145^post3, tmp_9^0'=tmp_9^post3, lt_27^0'=lt_27^post3, Result_4^0'=Result_4^post3, x_8^0'=x_8^post3, __patmp2^0'=__patmp2^post3, __disjvr_3^0'=__disjvr_3^post3, lt_24^0'=lt_24^post3, len_165^0'=len_165^post3, y_18^0'=y_18^post3, x_13^0'=x_13^post3, __disjvr_0^0'=__disjvr_0^post3, lt_21^0'=lt_21^post3, k_110^0'=k_110^post3, t_16^0'=t_16^post3, lt_26^0'=lt_26^post3, x_19^0'=x_19^post3, __patmp1^0'=__patmp1^post3, (0 == 0 /\ y_20^post3 == 0 /\ y_12^0-y_12^post3 == 0 /\ __patmp2^0-__patmp2^post3 == 0 /\ -__patmp1^post3+__patmp1^0 == 0 /\ -__disjvr_4^post3+__disjvr_4^0 == 0 /\ -a_11^0+x_13^post3 == 0 /\ -lt_22^post3+lt_22^0 == 0 /\ -t_16^post3+t_16^0 == 0 /\ -lt_25^post3+lt_25^0 == 0 /\ -y_18^post3+y_18^0 == 0 /\ __cil_tmp5_10^post3-x_8^post3 == 0 /\ x_17^0-x_17^post3 == 0 /\ k_145^0-k_145^post3 == 0 /\ -x_8^10+__cil_tmp5_10^10 == 0 /\ -lt_24^post3+lt_24^0 == 0 /\ -len_87^post3 <= 0 /\ __disjvr_2^0-__disjvr_2^post3 == 0 /\ __disjvr_1^0-__disjvr_1^post3 == 0 /\ k_191^0-k_191^post3 == 0 /\ Result_4^10-__cil_tmp5_10^10 == 0 /\ -2+len_87^post3 == 0 /\ a_11^0-a_11^post3 == 0 /\ x_8^post3-tmp_9^post3 == 0 /\ -len_165^post3+len_165^0 == 0 /\ Result_4^post3-__cil_tmp5_10^post3 == 0 /\ -tmp_9^10+x_8^10 == 0 /\ __disjvr_3^0-__disjvr_3^post3 == 0 /\ w_15^0-w_15^post3 == 0 /\ lt_23^0-lt_23^post3 == 0 /\ -__disjvr_0^post3+__disjvr_0^0 == 0 /\ -lt_21^post3+lt_21^0 == 0 /\ k_110^post3-len_87^post3 == 0), cost: 1
New rule:
l3 -> l5 : __cil_tmp5_10^0'=tmp_9^post3, len_87^0'=2, lt_28^0'=lt_28^post3, y_20^0'=0, tmp_9^0'=tmp_9^post3, lt_27^0'=lt_27^post3, Result_4^0'=tmp_9^post3, x_8^0'=tmp_9^post3, x_13^0'=a_11^0, k_110^0'=2, lt_26^0'=lt_26^post3, x_19^0'=x_19^post3, (0 == 0 /\ -2 <= 0), cost: 1

Applied preprocessing
Original rule:
l5 -> l6 : __disjvr_2^0'=__disjvr_2^post4, lt_23^0'=lt_23^post4, k_191^0'=k_191^post4, y_12^0'=y_12^post4, w_15^0'=w_15^post4, __cil_tmp5_10^0'=__cil_tmp5_10^post4, len_87^0'=len_87^post4, a_11^0'=a_11^post4, lt_28^0'=lt_28^post4, lt_25^0'=lt_25^post4, y_20^0'=y_20^post4, x_17^0'=x_17^post4, __disjvr_4^0'=__disjvr_4^post4, __disjvr_1^0'=__disjvr_1^post4, lt_22^0'=lt_22^post4, k_145^0'=k_145^post4, tmp_9^0'=tmp_9^post4, lt_27^0'=lt_27^post4, Result_4^0'=Result_4^post4, x_8^0'=x_8^post4, __patmp2^0'=__patmp2^post4, __disjvr_3^0'=__disjvr_3^post4, lt_24^0'=lt_24^post4, len_165^0'=len_165^post4, y_18^0'=y_18^post4, x_13^0'=x_13^post4, __disjvr_0^0'=__disjvr_0^post4, lt_21^0'=lt_21^post4, k_110^0'=k_110^post4, t_16^0'=t_16^post4, lt_26^0'=lt_26^post4, x_19^0'=x_19^post4, __patmp1^0'=__patmp1^post4, (len_87^0-len_87^post4 == 0 /\ w_15^0-w_15^post4 == 0 /\ -lt_24^post4+lt_24^0 == 0 /\ y_20^0-y_20^post4 == 0 /\ y_12^0-y_12^post4 == 0 /\ -lt_26^post4+lt_26^0 == 0 /\ -Result_4^post4+Result_4^0 == 0 /\ -x_19^post4+x_19^0 == 0 /\ -len_165^post4+len_165^0 == 0 /\ lt_25^0-lt_25^post4 == 0 /\ -__disjvr_0^post4+__disjvr_0^0 == 0 /\ lt_23^0-lt_23^post4 == 0 /\ lt_21^0-lt_21^post4 == 0 /\ -__disjvr_3^post4+__disjvr_3^0 == 0 /\ -__patmp2^post4+__patmp2^0 == 0 /\ -lt_27^post4+lt_27^0 == 0 /\ -tmp_9^post4+tmp_9^0 == 0 /\ x_13^0-x_13^post4 == 0 /\ k_191^0-k_191^post4 == 0 /\ -x_17^post4+x_17^0 == 0 /\ lt_22^0-lt_22^post4 == 0 /\ lt_28^0-lt_28^post4 == 0 /\ __disjvr_4^0-__disjvr_4^post4 == 0 /\ -__disjvr_1^post4+__disjvr_1^0 == 0 /\ -k_110^post4+k_110^0 == 0 /\ -__disjvr_2^post4+__disjvr_2^0 == 0 /\ -x_8^post4+x_8^0 == 0 /\ -__patmp1^post4+__patmp1^0 == 0 /\ k_145^0-k_145^post4 == 0 /\ -t_16^post4+t_16^0 == 0 /\ a_11^0-a_11^post4 == 0 /\ __cil_tmp5_10^0-__cil_tmp5_10^post4 == 0 /\ __disjvr_1^post4-__disjvr_1^0 == 0 /\ y_18^0-y_18^post4 == 0), cost: 1
New rule:
l5 -> l6 : 0 == 0, cost: 1

Applied preprocessing
Original rule:
l6 -> l4 : __disjvr_2^0'=__disjvr_2^post5, lt_23^0'=lt_23^post5, k_191^0'=k_191^post5, y_12^0'=y_12^post5, w_15^0'=w_15^post5, __cil_tmp5_10^0'=__cil_tmp5_10^post5, len_87^0'=len_87^post5, a_11^0'=a_11^post5, lt_28^0'=lt_28^post5, lt_25^0'=lt_25^post5, y_20^0'=y_20^post5, x_17^0'=x_17^post5, __disjvr_4^0'=__disjvr_4^post5, __disjvr_1^0'=__disjvr_1^post5, lt_22^0'=lt_22^post5, k_145^0'=k_145^post5, tmp_9^0'=tmp_9^post5, lt_27^0'=lt_27^post5, Result_4^0'=Result_4^post5, x_8^0'=x_8^post5, __patmp2^0'=__patmp2^post5, __disjvr_3^0'=__disjvr_3^post5, lt_24^0'=lt_24^post5, len_165^0'=len_165^post5, y_18^0'=y_18^post5, x_13^0'=x_13^post5, __disjvr_0^0'=__disjvr_0^post5, lt_21^0'=lt_21^post5, k_110^0'=k_110^post5, t_16^0'=t_16^post5, lt_26^0'=lt_26^post5, x_19^0'=x_19^post5, __patmp1^0'=__patmp1^post5, (0 == 0 /\ -lt_21^post5+lt_21^0 == 0 /\ -y_18^post5+y_18^0 == 0 /\ len_87^0-len_87^post5 == 0 /\ -lt_26^post5+lt_26^0 == 0 /\ k_110^0-k_110^post5 == 0 /\ lt_25^0-lt_25^post5 == 0 /\ -y_20^post5+y_20^0 == 0 /\ -x_17^post5+x_17^0 == 0 /\ -x_19^post5+x_19^0 == 0 /\ -__disjvr_0^post5+__disjvr_0^0 == 0 /\ y_12^0-y_12^post5 == 0 /\ w_15^0-w_15^post5 == 0 /\ __disjvr_2^0-__disjvr_2^post5 == 0 /\ -k_110^0 <= 0 /\ -__patmp2^post5+k_145^post5 == 0 /\ -__disjvr_1^post5+__disjvr_1^0 == 0 /\ -Result_4^post5+Result_4^0 == 0 /\ -lt_27^post5+lt_27^0 == 0 /\ -x_8^post5+x_8^0 == 0 /\ -lt_22^post5+lt_22^0 == 0 /\ lt_28^0-lt_28^post5 == 0 /\ -__patmp1^post5+len_165^post5 == 0 /\ __disjvr_4^0-__disjvr_4^post5 == 0 /\ -1+__patmp1^post5 == 0 /\ k_191^0-k_191^post5 == 0 /\ -tmp_9^post5+tmp_9^0 == 0 /\ a_11^0-a_11^post5 == 0 /\ -lt_23^10+x_13^post5 == 0 /\ __disjvr_3^0-__disjvr_3^post5 == 0 /\ -t_16^post5+t_16^0 == 0 /\ __cil_tmp5_10^0-__cil_tmp5_10^post5 == 0 /\ __patmp2^post5-k_110^0 == 0), cost: 1
New rule:
l6 -> l4 : lt_23^0'=lt_23^post5, k_145^0'=k_110^0, __patmp2^0'=k_110^0, lt_24^0'=lt_24^post5, len_165^0'=1, x_13^0'=lt_23^10, __patmp1^0'=1, k_110^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l4 -> l7 : __disjvr_2^0'=__disjvr_2^post6, lt_23^0'=lt_23^post6, k_191^0'=k_191^post6, y_12^0'=y_12^post6, w_15^0'=w_15^post6, __cil_tmp5_10^0'=__cil_tmp5_10^post6, len_87^0'=len_87^post6, a_11^0'=a_11^post6, lt_28^0'=lt_28^post6, lt_25^0'=lt_25^post6, y_20^0'=y_20^post6, x_17^0'=x_17^post6, __disjvr_4^0'=__disjvr_4^post6, __disjvr_1^0'=__disjvr_1^post6, lt_22^0'=lt_22^post6, k_145^0'=k_145^post6, tmp_9^0'=tmp_9^post6, lt_27^0'=lt_27^post6, Result_4^0'=Result_4^post6, x_8^0'=x_8^post6, __patmp2^0'=__patmp2^post6, __disjvr_3^0'=__disjvr_3^post6, lt_24^0'=lt_24^post6, len_165^0'=len_165^post6, y_18^0'=y_18^post6, x_13^0'=x_13^post6, __disjvr_0^0'=__disjvr_0^post6, lt_21^0'=lt_21^post6, k_110^0'=k_110^post6, t_16^0'=t_16^post6, lt_26^0'=lt_26^post6, x_19^0'=x_19^post6, __patmp1^0'=__patmp1^post6, (0 == 0 /\ 1-k_145^0 <= 0 /\ -len_165^post6+len_165^0 == 0 /\ -a_11^post6+a_11^0 == 0 /\ y_12^0-y_12^post6 == 0 /\ w_15^0-w_15^post6 == 0 /\ -lt_25^10+x_17^post6 == 0 /\ __patmp2^0-__patmp2^post6 == 0 /\ len_87^0-len_87^post6 == 0 /\ __cil_tmp5_10^0-__cil_tmp5_10^post6 == 0 /\ -lt_22^post6+lt_22^0 == 0 /\ -x_8^post6+x_8^0 == 0 /\ lt_28^0-lt_28^post6 == 0 /\ y_20^0-y_20^post6 == 0 /\ lt_23^0-lt_23^post6 == 0 /\ -lt_24^post6+lt_24^0 == 0 /\ -x_19^post6+x_19^0 == 0 /\ -lt_27^post6+lt_27^0 == 0 /\ -lt_21^post6+lt_21^0 == 0 /\ -k_145^post6+k_145^0 == 0 /\ y_12^0-x_13^0 <= 0 /\ -w_15^0+y_18^post6 == 0 /\ -len_165^0 <= 0 /\ __disjvr_1^0-__disjvr_1^post6 == 0 /\ -__disjvr_2^post6+__disjvr_2^0 == 0 /\ -y_12^0+x_13^0 <= 0 /\ -t_16^post6+t_16^0 == 0 /\ k_191^0-k_191^post6 == 0 /\ -__disjvr_0^post6+__disjvr_0^0 == 0 /\ -k_110^post6+k_110^0 == 0 /\ x_13^0-x_13^post6 == 0 /\ -__patmp1^post6+__patmp1^0 == 0 /\ tmp_9^0-tmp_9^post6 == 0 /\ __disjvr_4^0-__disjvr_4^post6 == 0 /\ -__disjvr_3^post6+__disjvr_3^0 == 0), cost: 1
New rule:
l4 -> l7 : lt_25^0'=lt_25^post6, x_17^0'=lt_25^10, Result_4^0'=Result_4^post6, y_18^0'=w_15^0, lt_26^0'=lt_26^post6, (-1+k_145^0 >= 0 /\ y_12^0-x_13^0 == 0 /\ len_165^0 >= 0), cost: 1

Applied preprocessing
Original rule:
l7 -> l8 : __disjvr_2^0'=__disjvr_2^post7, lt_23^0'=lt_23^post7, k_191^0'=k_191^post7, y_12^0'=y_12^post7, w_15^0'=w_15^post7, __cil_tmp5_10^0'=__cil_tmp5_10^post7, len_87^0'=len_87^post7, a_11^0'=a_11^post7, lt_28^0'=lt_28^post7, lt_25^0'=lt_25^post7, y_20^0'=y_20^post7, x_17^0'=x_17^post7, __disjvr_4^0'=__disjvr_4^post7, __disjvr_1^0'=__disjvr_1^post7, lt_22^0'=lt_22^post7, k_145^0'=k_145^post7, tmp_9^0'=tmp_9^post7, lt_27^0'=lt_27^post7, Result_4^0'=Result_4^post7, x_8^0'=x_8^post7, __patmp2^0'=__patmp2^post7, __disjvr_3^0'=__disjvr_3^post7, lt_24^0'=lt_24^post7, len_165^0'=len_165^post7, y_18^0'=y_18^post7, x_13^0'=x_13^post7, __disjvr_0^0'=__disjvr_0^post7, lt_21^0'=lt_21^post7, k_110^0'=k_110^post7, t_16^0'=t_16^post7, lt_26^0'=lt_26^post7, x_19^0'=x_19^post7, __patmp1^0'=__patmp1^post7, (-__disjvr_4^post7+__disjvr_4^0 == 0 /\ -lt_25^post7+lt_25^0 == 0 /\ lt_28^0-lt_28^post7 == 0 /\ -__disjvr_1^post7+__disjvr_1^0 == 0 /\ -__disjvr_2^0+__disjvr_2^post7 == 0 /\ x_17^0-x_17^post7 == 0 /\ -tmp_9^post7+tmp_9^0 == 0 /\ -k_110^post7+k_110^0 == 0 /\ a_11^0-a_11^post7 == 0 /\ w_15^0-w_15^post7 == 0 /\ -__patmp1^post7+__patmp1^0 == 0 /\ -y_20^post7+y_20^0 == 0 /\ __disjvr_2^0-__disjvr_2^post7 == 0 /\ -x_13^post7+x_13^0 == 0 /\ y_12^0-y_12^post7 == 0 /\ -t_16^post7+t_16^0 == 0 /\ lt_22^0-lt_22^post7 == 0 /\ __disjvr_0^0-__disjvr_0^post7 == 0 /\ __cil_tmp5_10^0-__cil_tmp5_10^post7 == 0 /\ -__disjvr_3^post7+__disjvr_3^0 == 0 /\ lt_27^0-lt_27^post7 == 0 /\ -lt_21^post7+lt_21^0 == 0 /\ lt_23^0-lt_23^post7 == 0 /\ y_18^0-y_18^post7 == 0 /\ x_8^0-x_8^post7 == 0 /\ len_87^0-len_87^post7 == 0 /\ -lt_26^post7+lt_26^0 == 0 /\ k_145^0-k_145^post7 == 0 /\ -x_19^post7+x_19^0 == 0 /\ len_165^0-len_165^post7 == 0 /\ -__patmp2^post7+__patmp2^0 == 0 /\ -Result_4^post7+Result_4^0 == 0 /\ lt_24^0-lt_24^post7 == 0 /\ -k_191^post7+k_191^0 == 0), cost: 1
New rule:
l7 -> l8 : 0 == 0, cost: 1

Applied preprocessing
Original rule:
l8 -> l9 : __disjvr_2^0'=__disjvr_2^post8, lt_23^0'=lt_23^post8, k_191^0'=k_191^post8, y_12^0'=y_12^post8, w_15^0'=w_15^post8, __cil_tmp5_10^0'=__cil_tmp5_10^post8, len_87^0'=len_87^post8, a_11^0'=a_11^post8, lt_28^0'=lt_28^post8, lt_25^0'=lt_25^post8, y_20^0'=y_20^post8, x_17^0'=x_17^post8, __disjvr_4^0'=__disjvr_4^post8, __disjvr_1^0'=__disjvr_1^post8, lt_22^0'=lt_22^post8, k_145^0'=k_145^post8, tmp_9^0'=tmp_9^post8, lt_27^0'=lt_27^post8, Result_4^0'=Result_4^post8, x_8^0'=x_8^post8, __patmp2^0'=__patmp2^post8, __disjvr_3^0'=__disjvr_3^post8, lt_24^0'=lt_24^post8, len_165^0'=len_165^post8, y_18^0'=y_18^post8, x_13^0'=x_13^post8, __disjvr_0^0'=__disjvr_0^post8, lt_21^0'=lt_21^post8, k_110^0'=k_110^post8, t_16^0'=t_16^post8, lt_26^0'=lt_26^post8, x_19^0'=x_19^post8, __patmp1^0'=__patmp1^post8, (t_16^post8-x_17^0 == 0 /\ lt_23^0-lt_23^post8 == 0 /\ -__patmp1^post8+__patmp1^0 == 0 /\ y_12^0-y_12^post8 == 0 /\ -__patmp2^post8+__patmp2^0 == 0 /\ x_8^0-x_8^post8 == 0 /\ -x_13^post8+x_13^0 == 0 /\ a_11^0-a_11^post8 == 0 /\ __disjvr_1^0-__disjvr_1^post8 == 0 /\ lt_27^0-lt_27^post8 == 0 /\ y_20^0-y_20^post8 == 0 /\ -len_87^post8+len_87^0 == 0 /\ -lt_25^post8+lt_25^0 == 0 /\ -lt_26^post8+lt_26^0 == 0 /\ lt_28^0-lt_28^post8 == 0 /\ -tmp_9^post8+tmp_9^0 == 0 /\ -x_19^post8+x_19^0 == 0 /\ -k_110^post8+k_110^0 == 0 /\ __disjvr_2^0-__disjvr_2^post8 == 0 /\ -len_165^post8+len_165^0 == 0 /\ __cil_tmp5_10^0-__cil_tmp5_10^post8 == 0 /\ -t_16^post8+y_18^post8 == 0 /\ k_191^0-k_191^post8 == 0 /\ -lt_21^post8+lt_21^0 == 0 /\ -k_145^post8+k_145^0 == 0 /\ __disjvr_3^0-__disjvr_3^post8 == 0 /\ x_17^0-x_17^post8 == 0 /\ -lt_24^post8+lt_24^0 == 0 /\ Result_4^0-Result_4^post8 == 0 /\ -__disjvr_4^post8+__disjvr_4^0 == 0 /\ -__disjvr_0^post8+__disjvr_0^0 == 0 /\ lt_22^0-lt_22^post8 == 0 /\ w_15^0-w_15^post8 == 0), cost: 1
New rule:
l8 -> l9 : y_18^0'=x_17^0, t_16^0'=x_17^0, TRUE, cost: 1

Applied preprocessing
Original rule:
l9 -> l10 : __disjvr_2^0'=__disjvr_2^post9, lt_23^0'=lt_23^post9, k_191^0'=k_191^post9, y_12^0'=y_12^post9, w_15^0'=w_15^post9, __cil_tmp5_10^0'=__cil_tmp5_10^post9, len_87^0'=len_87^post9, a_11^0'=a_11^post9, lt_28^0'=lt_28^post9, lt_25^0'=lt_25^post9, y_20^0'=y_20^post9, x_17^0'=x_17^post9, __disjvr_4^0'=__disjvr_4^post9, __disjvr_1^0'=__disjvr_1^post9, lt_22^0'=lt_22^post9, k_145^0'=k_145^post9, tmp_9^0'=tmp_9^post9, lt_27^0'=lt_27^post9, Result_4^0'=Result_4^post9, x_8^0'=x_8^post9, __patmp2^0'=__patmp2^post9, __disjvr_3^0'=__disjvr_3^post9, lt_24^0'=lt_24^post9, len_165^0'=len_165^post9, y_18^0'=y_18^post9, x_13^0'=x_13^post9, __disjvr_0^0'=__disjvr_0^post9, lt_21^0'=lt_21^post9, k_110^0'=k_110^post9, t_16^0'=t_16^post9, lt_26^0'=lt_26^post9, x_19^0'=x_19^post9, __patmp1^0'=__patmp1^post9, (-__disjvr_0^post9+__disjvr_0^0 == 0 /\ -t_16^post9+t_16^0 == 0 /\ k_110^0-k_110^post9 == 0 /\ k_191^0-k_191^post9 == 0 /\ -lt_22^post9+lt_22^0 == 0 /\ __disjvr_2^0-__disjvr_2^post9 == 0 /\ lt_25^0-lt_25^post9 == 0 /\ -x_19^post9+x_19^0 == 0 /\ __disjvr_1^0-__disjvr_1^post9 == 0 /\ -lt_26^post9+lt_26^0 == 0 /\ lt_27^0-lt_27^post9 == 0 /\ Result_4^0-Result_4^post9 == 0 /\ x_17^0-x_17^post9 == 0 /\ -x_13^post9+x_13^0 == 0 /\ -k_145^post9+k_145^0 == 0 /\ w_15^0-w_15^post9 == 0 /\ -__disjvr_3^post9+__disjvr_3^0 == 0 /\ __patmp2^0-__patmp2^post9 == 0 /\ -len_165^post9+len_165^0 == 0 /\ -x_8^post9+x_8^0 == 0 /\ -lt_24^post9+lt_24^0 == 0 /\ -__cil_tmp5_10^post9+__cil_tmp5_10^0 == 0 /\ y_12^0-y_12^post9 == 0 /\ tmp_9^0-tmp_9^post9 == 0 /\ y_20^0-y_20^post9 == 0 /\ __disjvr_4^0-__disjvr_4^post9 == 0 /\ -__patmp1^post9+__patmp1^0 == 0 /\ -y_18^post9+y_18^0 == 0 /\ __disjvr_3^post9-__disjvr_3^0 == 0 /\ a_11^0-a_11^post9 == 0 /\ -lt_21^post9+lt_21^0 == 0 /\ -lt_28^post9+lt_28^0 == 0 /\ len_87^0-len_87^post9 == 0 /\ lt_23^0-lt_23^post9 == 0), cost: 1
New rule:
l9 -> l10 : 0 == 0, cost: 1

Applied preprocessing
Original rule:
l10 -> l0 : __disjvr_2^0'=__disjvr_2^post10, lt_23^0'=lt_23^post10, k_191^0'=k_191^post10, y_12^0'=y_12^post10, w_15^0'=w_15^post10, __cil_tmp5_10^0'=__cil_tmp5_10^post10, len_87^0'=len_87^post10, a_11^0'=a_11^post10, lt_28^0'=lt_28^post10, lt_25^0'=lt_25^post10, y_20^0'=y_20^post10, x_17^0'=x_17^post10, __disjvr_4^0'=__disjvr_4^post10, __disjvr_1^0'=__disjvr_1^post10, lt_22^0'=lt_22^post10, k_145^0'=k_145^post10, tmp_9^0'=tmp_9^post10, lt_27^0'=lt_27^post10, Result_4^0'=Result_4^post10, x_8^0'=x_8^post10, __patmp2^0'=__patmp2^post10, __disjvr_3^0'=__disjvr_3^post10, lt_24^0'=lt_24^post10, len_165^0'=len_165^post10, y_18^0'=y_18^post10, x_13^0'=x_13^post10, __disjvr_0^0'=__disjvr_0^post10, lt_21^0'=lt_21^post10, k_110^0'=k_110^post10, t_16^0'=t_16^post10, lt_26^0'=lt_26^post10, x_19^0'=x_19^post10, __patmp1^0'=__patmp1^post10, (-a_11^post10+a_11^0 == 0 /\ -t_16^post10+y_18^post10 == 0 /\ -__disjvr_1^post10+__disjvr_1^0 == 0 /\ -lt_26^post10+lt_26^0 == 0 /\ y_12^0-y_12^post10 == 0 /\ w_15^0-w_15^post10 == 0 /\ -x_17^post10+x_17^0 == 0 /\ k_145^0-k_145^post10 == 0 /\ -Result_4^post10+Result_4^0 == 0 /\ lt_25^0-lt_25^post10 == 0 /\ __cil_tmp5_10^0-__cil_tmp5_10^post10 == 0 /\ len_87^0-len_87^post10 == 0 /\ -__disjvr_0^post10+__disjvr_0^0 == 0 /\ __patmp2^0-__patmp2^post10 == 0 /\ -x_17^0+t_16^post10 == 0 /\ -__disjvr_3^post10+__disjvr_3^0 == 0 /\ __disjvr_2^0-__disjvr_2^post10 == 0 /\ lt_23^0-lt_23^post10 == 0 /\ __disjvr_4^0-__disjvr_4^post10 == 0 /\ -lt_27^post10+lt_27^0 == 0 /\ tmp_9^0-tmp_9^post10 == 0 /\ -lt_22^post10+lt_22^0 == 0 /\ y_20^0-y_20^post10 == 0 /\ -x_8^post10+x_8^0 == 0 /\ lt_28^0-lt_28^post10 == 0 /\ lt_21^0-lt_21^post10 == 0 /\ -x_19^post10+x_19^0 == 0 /\ -len_165^post10+len_165^0 == 0 /\ x_13^0-x_13^post10 == 0 /\ -k_110^post10+k_110^0 == 0 /\ k_191^0-k_191^post10 == 0 /\ -__patmp1^post10+__patmp1^0 == 0 /\ -lt_24^post10+lt_24^0 == 0), cost: 1
New rule:
l10 -> l0 : y_18^0'=x_17^0, t_16^0'=x_17^0, TRUE, cost: 1

Applied preprocessing
Original rule:
l4 -> l12 : __disjvr_2^0'=__disjvr_2^post11, lt_23^0'=lt_23^post11, k_191^0'=k_191^post11, y_12^0'=y_12^post11, w_15^0'=w_15^post11, __cil_tmp5_10^0'=__cil_tmp5_10^post11, len_87^0'=len_87^post11, a_11^0'=a_11^post11, lt_28^0'=lt_28^post11, lt_25^0'=lt_25^post11, y_20^0'=y_20^post11, x_17^0'=x_17^post11, __disjvr_4^0'=__disjvr_4^post11, __disjvr_1^0'=__disjvr_1^post11, lt_22^0'=lt_22^post11, k_145^0'=k_145^post11, tmp_9^0'=tmp_9^post11, lt_27^0'=lt_27^post11, Result_4^0'=Result_4^post11, x_8^0'=x_8^post11, __patmp2^0'=__patmp2^post11, __disjvr_3^0'=__disjvr_3^post11, lt_24^0'=lt_24^post11, len_165^0'=len_165^post11, y_18^0'=y_18^post11, x_13^0'=x_13^post11, __disjvr_0^0'=__disjvr_0^post11, lt_21^0'=lt_21^post11, k_110^0'=k_110^post11, t_16^0'=t_16^post11, lt_26^0'=lt_26^post11, x_19^0'=x_19^post11, __patmp1^0'=__patmp1^post11, (__disjvr_0^0-__disjvr_0^post11 == 0 /\ -t_16^post11+t_16^0 == 0 /\ 1-k_145^0 <= 0 /\ -Result_4^post11+Result_4^0 == 0 /\ len_87^0-len_87^post11 == 0 /\ __disjvr_2^0-__disjvr_2^post11 == 0 /\ lt_25^0-lt_25^post11 == 0 /\ -y_20^post11+y_20^0 == 0 /\ lt_22^0-lt_22^post11 == 0 /\ -__patmp2^post11+__patmp2^0 == 0 /\ -tmp_9^post11+tmp_9^0 == 0 /\ -x_17^post11+x_17^0 == 0 /\ -lt_26^post11+lt_26^0 == 0 /\ -x_13^post11+x_13^0 == 0 /\ w_15^0-w_15^post11 == 0 /\ lt_27^0-lt_27^post11 == 0 /\ -__disjvr_3^post11+__disjvr_3^0 == 0 /\ -x_19^post11+x_19^0 == 0 /\ -x_8^post11+x_8^0 == 0 /\ -len_165^0 <= 0 /\ -k_110^post11+k_110^0 == 0 /\ y_12^0-y_12^post11 == 0 /\ -__patmp1^post11+__patmp1^0 == 0 /\ lt_28^0-lt_28^post11 == 0 /\ -__disjvr_1^post11+__disjvr_1^0 == 0 /\ k_145^0-k_145^post11 == 0 /\ __disjvr_4^0-__disjvr_4^post11 == 0 /\ len_165^0-len_165^post11 == 0 /\ a_11^0-a_11^post11 == 0 /\ y_18^0-y_18^post11 == 0 /\ 1-k_145^0+k_191^post11 == 0 /\ __cil_tmp5_10^0-__cil_tmp5_10^post11 == 0 /\ lt_24^0-lt_24^post11 == 0 /\ -lt_21^post11+lt_21^0 == 0 /\ lt_23^0-lt_23^post11 == 0), cost: 1
New rule:
l4 -> l12 : k_191^0'=-1+k_145^0, (-1+k_145^0 >= 0 /\ len_165^0 >= 0), cost: 1

Applied preprocessing
Original rule:
l12 -> l13 : __disjvr_2^0'=__disjvr_2^post12, lt_23^0'=lt_23^post12, k_191^0'=k_191^post12, y_12^0'=y_12^post12, w_15^0'=w_15^post12, __cil_tmp5_10^0'=__cil_tmp5_10^post12, len_87^0'=len_87^post12, a_11^0'=a_11^post12, lt_28^0'=lt_28^post12, lt_25^0'=lt_25^post12, y_20^0'=y_20^post12, x_17^0'=x_17^post12, __disjvr_4^0'=__disjvr_4^post12, __disjvr_1^0'=__disjvr_1^post12, lt_22^0'=lt_22^post12, k_145^0'=k_145^post12, tmp_9^0'=tmp_9^post12, lt_27^0'=lt_27^post12, Result_4^0'=Result_4^post12, x_8^0'=x_8^post12, __patmp2^0'=__patmp2^post12, __disjvr_3^0'=__disjvr_3^post12, lt_24^0'=lt_24^post12, len_165^0'=len_165^post12, y_18^0'=y_18^post12, x_13^0'=x_13^post12, __disjvr_0^0'=__disjvr_0^post12, lt_21^0'=lt_21^post12, k_110^0'=k_110^post12, t_16^0'=t_16^post12, lt_26^0'=lt_26^post12, x_19^0'=x_19^post12, __patmp1^0'=__patmp1^post12, (-__patmp2^post12+__patmp2^0 == 0 /\ -x_13^post12+x_13^0 == 0 /\ -lt_26^post12+lt_26^0 == 0 /\ x_17^0-x_17^post12 == 0 /\ lt_22^0-lt_22^post12 == 0 /\ __disjvr_4^post12-__disjvr_4^0 == 0 /\ y_12^0-y_12^post12 == 0 /\ lt_28^0-lt_28^post12 == 0 /\ -k_145^post12+k_145^0 == 0 /\ lt_27^0-lt_27^post12 == 0 /\ -lt_21^post12+lt_21^0 == 0 /\ x_8^0-x_8^post12 == 0 /\ -__disjvr_0^post12+__disjvr_0^0 == 0 /\ lt_23^0-lt_23^post12 == 0 /\ w_15^0-w_15^post12 == 0 /\ -__disjvr_4^post12+__disjvr_4^0 == 0 /\ __disjvr_3^0-__disjvr_3^post12 == 0 /\ a_11^0-a_11^post12 == 0 /\ __cil_tmp5_10^0-__cil_tmp5_10^post12 == 0 /\ -x_19^post12+x_19^0 == 0 /\ len_87^0-len_87^post12 == 0 /\ -y_20^post12+y_20^0 == 0 /\ -tmp_9^post12+tmp_9^0 == 0 /\ __disjvr_2^0-__disjvr_2^post12 == 0 /\ len_165^0-len_165^post12 == 0 /\ -__disjvr_1^post12+__disjvr_1^0 == 0 /\ k_191^0-k_191^post12 == 0 /\ -k_110^post12+k_110^0 == 0 /\ t_16^0-t_16^post12 == 0 /\ -y_18^post12+y_18^0 == 0 /\ -lt_25^post12+lt_25^0 == 0 /\ Result_4^0-Result_4^post12 == 0 /\ -lt_24^post12+lt_24^0 == 0 /\ -__patmp1^post12+__patmp1^0 == 0), cost: 1
New rule:
l12 -> l13 : 0 == 0, cost: 1

Applied preprocessing
Original rule:
l13 -> l11 : __disjvr_2^0'=__disjvr_2^post13, lt_23^0'=lt_23^post13, k_191^0'=k_191^post13, y_12^0'=y_12^post13, w_15^0'=w_15^post13, __cil_tmp5_10^0'=__cil_tmp5_10^post13, len_87^0'=len_87^post13, a_11^0'=a_11^post13, lt_28^0'=lt_28^post13, lt_25^0'=lt_25^post13, y_20^0'=y_20^post13, x_17^0'=x_17^post13, __disjvr_4^0'=__disjvr_4^post13, __disjvr_1^0'=__disjvr_1^post13, lt_22^0'=lt_22^post13, k_145^0'=k_145^post13, tmp_9^0'=tmp_9^post13, lt_27^0'=lt_27^post13, Result_4^0'=Result_4^post13, x_8^0'=x_8^post13, __patmp2^0'=__patmp2^post13, __disjvr_3^0'=__disjvr_3^post13, lt_24^0'=lt_24^post13, len_165^0'=len_165^post13, y_18^0'=y_18^post13, x_13^0'=x_13^post13, __disjvr_0^0'=__disjvr_0^post13, lt_21^0'=lt_21^post13, k_110^0'=k_110^post13, t_16^0'=t_16^post13, lt_26^0'=lt_26^post13, x_19^0'=x_19^post13, __patmp1^0'=__patmp1^post13, (0 == 0 /\ -lt_21^10+x_13^post13 == 0 /\ -tmp_9^post13+tmp_9^0 == 0 /\ len_87^0-len_87^post13 == 0 /\ -__disjvr_3^post13+__disjvr_3^0 == 0 /\ len_165^post13-__patmp1^post13 == 0 /\ -__disjvr_1^post13+__disjvr_1^0 == 0 /\ lt_23^0-lt_23^post13 == 0 /\ -k_110^post13+k_110^0 == 0 /\ y_20^0-y_20^post13 == 0 /\ -Result_4^post13+Result_4^0 == 0 /\ -x_19^post13+x_19^0 == 0 /\ -lt_27^post13+lt_27^0 == 0 /\ -k_191^0+__patmp2^post13 == 0 /\ k_191^0-k_191^post13 == 0 /\ lt_25^0-lt_25^post13 == 0 /\ -1-len_165^0+__patmp1^post13 == 0 /\ -__disjvr_0^post13+__disjvr_0^0 == 0 /\ __cil_tmp5_10^0-__cil_tmp5_10^post13 == 0 /\ -t_16^post13+t_16^0 == 0 /\ -x_17^post13+x_17^0 == 0 /\ lt_28^0-lt_28^post13 == 0 /\ __disjvr_4^0-__disjvr_4^post13 == 0 /\ -len_165^0 <= 0 /\ -lt_24^post13+lt_24^0 == 0 /\ -y_18^post13+y_18^0 == 0 /\ -w_15^post13+w_15^0 == 0 /\ -x_8^post13+x_8^0 == 0 /\ k_145^post13-__patmp2^post13 == 0 /\ -lt_26^post13+lt_26^0 == 0 /\ y_12^0-y_12^post13 == 0 /\ __disjvr_2^0-__disjvr_2^post13 == 0 /\ -k_191^0 <= 0 /\ a_11^0-a_11^post13 == 0), cost: 1
New rule:
l13 -> l11 : lt_22^0'=lt_22^post13, k_145^0'=k_191^0, __patmp2^0'=k_191^0, len_165^0'=1+len_165^0, x_13^0'=lt_21^10, lt_21^0'=lt_21^post13, __patmp1^0'=1+len_165^0, (k_191^0 >= 0 /\ len_165^0 >= 0), cost: 1

Applied preprocessing
Original rule:
l11 -> l4 : __disjvr_2^0'=__disjvr_2^post14, lt_23^0'=lt_23^post14, k_191^0'=k_191^post14, y_12^0'=y_12^post14, w_15^0'=w_15^post14, __cil_tmp5_10^0'=__cil_tmp5_10^post14, len_87^0'=len_87^post14, a_11^0'=a_11^post14, lt_28^0'=lt_28^post14, lt_25^0'=lt_25^post14, y_20^0'=y_20^post14, x_17^0'=x_17^post14, __disjvr_4^0'=__disjvr_4^post14, __disjvr_1^0'=__disjvr_1^post14, lt_22^0'=lt_22^post14, k_145^0'=k_145^post14, tmp_9^0'=tmp_9^post14, lt_27^0'=lt_27^post14, Result_4^0'=Result_4^post14, x_8^0'=x_8^post14, __patmp2^0'=__patmp2^post14, __disjvr_3^0'=__disjvr_3^post14, lt_24^0'=lt_24^post14, len_165^0'=len_165^post14, y_18^0'=y_18^post14, x_13^0'=x_13^post14, __disjvr_0^0'=__disjvr_0^post14, lt_21^0'=lt_21^post14, k_110^0'=k_110^post14, t_16^0'=t_16^post14, lt_26^0'=lt_26^post14, x_19^0'=x_19^post14, __patmp1^0'=__patmp1^post14, (a_11^0-a_11^post14 == 0 /\ w_15^0-w_15^post14 == 0 /\ -y_18^post14+y_18^0 == 0 /\ y_20^0-y_20^post14 == 0 /\ -x_13^post14+x_13^0 == 0 /\ -k_145^post14+k_145^0 == 0 /\ k_110^0-k_110^post14 == 0 /\ lt_25^0-lt_25^post14 == 0 /\ y_12^0-y_12^post14 == 0 /\ -lt_21^post14+lt_21^0 == 0 /\ -lt_26^post14+lt_26^0 == 0 /\ -lt_28^post14+lt_28^0 == 0 /\ -__disjvr_0^post14+__disjvr_0^0 == 0 /\ -x_19^post14+x_19^0 == 0 /\ -__disjvr_4^post14+__disjvr_4^0 == 0 /\ lt_23^0-lt_23^post14 == 0 /\ __disjvr_1^0-__disjvr_1^post14 == 0 /\ Result_4^0-Result_4^post14 == 0 /\ -len_165^post14+len_165^0 == 0 /\ __patmp2^0-__patmp2^post14 == 0 /\ k_191^0-k_191^post14 == 0 /\ lt_22^0-lt_22^post14 == 0 /\ __disjvr_2^0-__disjvr_2^post14 == 0 /\ tmp_9^0-tmp_9^post14 == 0 /\ __cil_tmp5_10^0-__cil_tmp5_10^post14 == 0 /\ -x_8^post14+x_8^0 == 0 /\ x_17^0-x_17^post14 == 0 /\ -__patmp1^post14+__patmp1^0 == 0 /\ -len_87^post14+len_87^0 == 0 /\ __disjvr_3^0-__disjvr_3^post14 == 0 /\ t_16^0-t_16^post14 == 0 /\ -lt_27^post14+lt_27^0 == 0 /\ -lt_24^post14+lt_24^0 == 0), cost: 1
New rule:
l11 -> l4 : TRUE, cost: 1

Applied preprocessing
Original rule:
l14 -> l3 : __disjvr_2^0'=__disjvr_2^post15, lt_23^0'=lt_23^post15, k_191^0'=k_191^post15, y_12^0'=y_12^post15, w_15^0'=w_15^post15, __cil_tmp5_10^0'=__cil_tmp5_10^post15, len_87^0'=len_87^post15, a_11^0'=a_11^post15, lt_28^0'=lt_28^post15, lt_25^0'=lt_25^post15, y_20^0'=y_20^post15, x_17^0'=x_17^post15, __disjvr_4^0'=__disjvr_4^post15, __disjvr_1^0'=__disjvr_1^post15, lt_22^0'=lt_22^post15, k_145^0'=k_145^post15, tmp_9^0'=tmp_9^post15, lt_27^0'=lt_27^post15, Result_4^0'=Result_4^post15, x_8^0'=x_8^post15, __patmp2^0'=__patmp2^post15, __disjvr_3^0'=__disjvr_3^post15, lt_24^0'=lt_24^post15, len_165^0'=len_165^post15, y_18^0'=y_18^post15, x_13^0'=x_13^post15, __disjvr_0^0'=__disjvr_0^post15, lt_21^0'=lt_21^post15, k_110^0'=k_110^post15, t_16^0'=t_16^post15, lt_26^0'=lt_26^post15, x_19^0'=x_19^post15, __patmp1^0'=__patmp1^post15, (-x_19^post15+x_19^0 == 0 /\ x_13^0-x_13^post15 == 0 /\ tmp_9^0-tmp_9^post15 == 0 /\ -x_8^post15+x_8^0 == 0 /\ __disjvr_4^0-__disjvr_4^post15 == 0 /\ -__disjvr_0^post15+__disjvr_0^0 == 0 /\ -len_165^post15+len_165^0 == 0 /\ x_17^0-x_17^post15 == 0 /\ -lt_27^post15+lt_27^0 == 0 /\ __patmp2^0-__patmp2^post15 == 0 /\ -lt_24^post15+lt_24^0 == 0 /\ k_110^0-k_110^post15 == 0 /\ k_191^0-k_191^post15 == 0 /\ -lt_28^post15+lt_28^0 == 0 /\ -Result_4^post15+Result_4^0 == 0 /\ -lt_22^post15+lt_22^0 == 0 /\ __disjvr_1^0-__disjvr_1^post15 == 0 /\ -__patmp1^post15+__patmp1^0 == 0 /\ k_145^0-k_145^post15 == 0 /\ a_11^0-a_11^post15 == 0 /\ -y_18^post15+y_18^0 == 0 /\ -__disjvr_3^post15+__disjvr_3^0 == 0 /\ lt_25^0-lt_25^post15 == 0 /\ w_15^0-w_15^post15 == 0 /\ -t_16^post15+t_16^0 == 0 /\ -lt_23^post15+lt_23^0 == 0 /\ __disjvr_2^0-__disjvr_2^post15 == 0 /\ len_87^0-len_87^post15 == 0 /\ -lt_21^post15+lt_21^0 == 0 /\ y_12^0-y_12^post15 == 0 /\ __cil_tmp5_10^0-__cil_tmp5_10^post15 == 0 /\ -lt_26^post15+lt_26^0 == 0 /\ y_20^0-y_20^post15 == 0), cost: 1
New rule:
l14 -> l3 : TRUE, cost: 1

Simplified rules
Start location: l14
  16: l0 -> l2 : 0 == 0, cost: 1
  17: l2 -> l1 : y_18^0'=x_17^0, t_16^0'=x_17^0, TRUE, cost: 1
  18: l1 -> l0 : TRUE, cost: 1
  19: l3 -> l5 : __cil_tmp5_10^0'=tmp_9^post3, len_87^0'=2, lt_28^0'=lt_28^post3, y_20^0'=0, tmp_9^0'=tmp_9^post3, lt_27^0'=lt_27^post3, Result_4^0'=tmp_9^post3, x_8^0'=tmp_9^post3, x_13^0'=a_11^0, k_110^0'=2, lt_26^0'=lt_26^post3, x_19^0'=x_19^post3, (0 == 0 /\ -2 <= 0), cost: 1
  20: l5 -> l6 : 0 == 0, cost: 1
  21: l6 -> l4 : lt_23^0'=lt_23^post5, k_145^0'=k_110^0, __patmp2^0'=k_110^0, lt_24^0'=lt_24^post5, len_165^0'=1, x_13^0'=lt_23^10, __patmp1^0'=1, k_110^0 >= 0, cost: 1
  22: l4 -> l7 : lt_25^0'=lt_25^post6, x_17^0'=lt_25^10, Result_4^0'=Result_4^post6, y_18^0'=w_15^0, lt_26^0'=lt_26^post6, (-1+k_145^0 >= 0 /\ y_12^0-x_13^0 == 0 /\ len_165^0 >= 0), cost: 1
  27: l4 -> l12 : k_191^0'=-1+k_145^0, (-1+k_145^0 >= 0 /\ len_165^0 >= 0), cost: 1
  23: l7 -> l8 : 0 == 0, cost: 1
  24: l8 -> l9 : y_18^0'=x_17^0, t_16^0'=x_17^0, TRUE, cost: 1
  25: l9 -> l10 : 0 == 0, cost: 1
  26: l10 -> l0 : y_18^0'=x_17^0, t_16^0'=x_17^0, TRUE, cost: 1
  28: l12 -> l13 : 0 == 0, cost: 1
  29: l13 -> l11 : lt_22^0'=lt_22^post13, k_145^0'=k_191^0, __patmp2^0'=k_191^0, len_165^0'=1+len_165^0, x_13^0'=lt_21^10, lt_21^0'=lt_21^post13, __patmp1^0'=1+len_165^0, (k_191^0 >= 0 /\ len_165^0 >= 0), cost: 1
  30: l11 -> l4 : TRUE, cost: 1
  31: l14 -> l3 : TRUE, cost: 1


Eliminating location l3 by chaining:

Applied chaining
First rule:
l14 -> l3 : TRUE, cost: 1
Second rule:
l3 -> l5 : __cil_tmp5_10^0'=tmp_9^post3, len_87^0'=2, lt_28^0'=lt_28^post3, y_20^0'=0, tmp_9^0'=tmp_9^post3, lt_27^0'=lt_27^post3, Result_4^0'=tmp_9^post3, x_8^0'=tmp_9^post3, x_13^0'=a_11^0, k_110^0'=2, lt_26^0'=lt_26^post3, x_19^0'=x_19^post3, (0 == 0 /\ -2 <= 0), cost: 1
New rule:
l14 -> l5 : __cil_tmp5_10^0'=tmp_9^post3, len_87^0'=2, lt_28^0'=lt_28^post3, y_20^0'=0, tmp_9^0'=tmp_9^post3, lt_27^0'=lt_27^post3, Result_4^0'=tmp_9^post3, x_8^0'=tmp_9^post3, x_13^0'=a_11^0, k_110^0'=2, lt_26^0'=lt_26^post3, x_19^0'=x_19^post3, (0 == 0 /\ -2 <= 0), cost: 2

Applied deletion
Removed the following rules: 19 31

Eliminating location l5 by chaining:

Applied chaining
First rule:
l14 -> l5 : __cil_tmp5_10^0'=tmp_9^post3, len_87^0'=2, lt_28^0'=lt_28^post3, y_20^0'=0, tmp_9^0'=tmp_9^post3, lt_27^0'=lt_27^post3, Result_4^0'=tmp_9^post3, x_8^0'=tmp_9^post3, x_13^0'=a_11^0, k_110^0'=2, lt_26^0'=lt_26^post3, x_19^0'=x_19^post3, (0 == 0 /\ -2 <= 0), cost: 2
Second rule:
l5 -> l6 : 0 == 0, cost: 1
New rule:
l14 -> l6 : __cil_tmp5_10^0'=tmp_9^post3, len_87^0'=2, lt_28^0'=lt_28^post3, y_20^0'=0, tmp_9^0'=tmp_9^post3, lt_27^0'=lt_27^post3, Result_4^0'=tmp_9^post3, x_8^0'=tmp_9^post3, x_13^0'=a_11^0, k_110^0'=2, lt_26^0'=lt_26^post3, x_19^0'=x_19^post3, (0 == 0 /\ -2 <= 0), cost: 3

Applied deletion
Removed the following rules: 20 32

Eliminating location l6 by chaining:

Applied chaining
First rule:
l14 -> l6 : __cil_tmp5_10^0'=tmp_9^post3, len_87^0'=2, lt_28^0'=lt_28^post3, y_20^0'=0, tmp_9^0'=tmp_9^post3, lt_27^0'=lt_27^post3, Result_4^0'=tmp_9^post3, x_8^0'=tmp_9^post3, x_13^0'=a_11^0, k_110^0'=2, lt_26^0'=lt_26^post3, x_19^0'=x_19^post3, (0 == 0 /\ -2 <= 0), cost: 3
Second rule:
l6 -> l4 : lt_23^0'=lt_23^post5, k_145^0'=k_110^0, __patmp2^0'=k_110^0, lt_24^0'=lt_24^post5, len_165^0'=1, x_13^0'=lt_23^10, __patmp1^0'=1, k_110^0 >= 0, cost: 1
New rule:
l14 -> l4 : lt_23^0'=lt_23^post5, __cil_tmp5_10^0'=tmp_9^post3, len_87^0'=2, lt_28^0'=lt_28^post3, y_20^0'=0, k_145^0'=2, tmp_9^0'=tmp_9^post3, lt_27^0'=lt_27^post3, Result_4^0'=tmp_9^post3, x_8^0'=tmp_9^post3, __patmp2^0'=2, lt_24^0'=lt_24^post5, len_165^0'=1, x_13^0'=lt_23^10, k_110^0'=2, lt_26^0'=lt_26^post3, x_19^0'=x_19^post3, __patmp1^0'=1, (0 == 0 /\ -2 <= 0 /\ 2 >= 0), cost: 4

Applied deletion
Removed the following rules: 21 33

Eliminating location l7 by chaining:

Applied chaining
First rule:
l4 -> l7 : lt_25^0'=lt_25^post6, x_17^0'=lt_25^10, Result_4^0'=Result_4^post6, y_18^0'=w_15^0, lt_26^0'=lt_26^post6, (-1+k_145^0 >= 0 /\ y_12^0-x_13^0 == 0 /\ len_165^0 >= 0), cost: 1
Second rule:
l7 -> l8 : 0 == 0, cost: 1
New rule:
l4 -> l8 : lt_25^0'=lt_25^post6, x_17^0'=lt_25^10, Result_4^0'=Result_4^post6, y_18^0'=w_15^0, lt_26^0'=lt_26^post6, (0 == 0 /\ -1+k_145^0 >= 0 /\ y_12^0-x_13^0 == 0 /\ len_165^0 >= 0), cost: 2

Applied simplification
Original rule:
l4 -> l8 : lt_25^0'=lt_25^post6, x_17^0'=lt_25^10, Result_4^0'=Result_4^post6, y_18^0'=w_15^0, lt_26^0'=lt_26^post6, (0 == 0 /\ -1+k_145^0 >= 0 /\ y_12^0-x_13^0 == 0 /\ len_165^0 >= 0), cost: 2
New rule:
l4 -> l8 : lt_25^0'=lt_25^post6, x_17^0'=lt_25^10, Result_4^0'=Result_4^post6, y_18^0'=w_15^0, lt_26^0'=lt_26^post6, (-1+k_145^0 >= 0 /\ y_12^0-x_13^0 == 0 /\ len_165^0 >= 0), cost: 2

Applied deletion
Removed the following rules: 22 23

Eliminating location l12 by chaining:

Applied chaining
First rule:
l4 -> l12 : k_191^0'=-1+k_145^0, (-1+k_145^0 >= 0 /\ len_165^0 >= 0), cost: 1
Second rule:
l12 -> l13 : 0 == 0, cost: 1
New rule:
l4 -> l13 : k_191^0'=-1+k_145^0, (0 == 0 /\ -1+k_145^0 >= 0 /\ len_165^0 >= 0), cost: 2

Applied simplification
Original rule:
l4 -> l13 : k_191^0'=-1+k_145^0, (0 == 0 /\ -1+k_145^0 >= 0 /\ len_165^0 >= 0), cost: 2
New rule:
l4 -> l13 : k_191^0'=-1+k_145^0, (-1+k_145^0 >= 0 /\ len_165^0 >= 0), cost: 2

Applied deletion
Removed the following rules: 27 28

Eliminating location l8 by chaining:

Applied chaining
First rule:
l4 -> l8 : lt_25^0'=lt_25^post6, x_17^0'=lt_25^10, Result_4^0'=Result_4^post6, y_18^0'=w_15^0, lt_26^0'=lt_26^post6, (-1+k_145^0 >= 0 /\ y_12^0-x_13^0 == 0 /\ len_165^0 >= 0), cost: 2
Second rule:
l8 -> l9 : y_18^0'=x_17^0, t_16^0'=x_17^0, TRUE, cost: 1
New rule:
l4 -> l9 : lt_25^0'=lt_25^post6, x_17^0'=lt_25^10, Result_4^0'=Result_4^post6, y_18^0'=lt_25^10, t_16^0'=lt_25^10, lt_26^0'=lt_26^post6, (-1+k_145^0 >= 0 /\ y_12^0-x_13^0 == 0 /\ len_165^0 >= 0), cost: 3

Applied deletion
Removed the following rules: 24 35

Eliminating location l13 by chaining:

Applied chaining
First rule:
l4 -> l13 : k_191^0'=-1+k_145^0, (-1+k_145^0 >= 0 /\ len_165^0 >= 0), cost: 2
Second rule:
l13 -> l11 : lt_22^0'=lt_22^post13, k_145^0'=k_191^0, __patmp2^0'=k_191^0, len_165^0'=1+len_165^0, x_13^0'=lt_21^10, lt_21^0'=lt_21^post13, __patmp1^0'=1+len_165^0, (k_191^0 >= 0 /\ len_165^0 >= 0), cost: 1
New rule:
l4 -> l11 : k_191^0'=-1+k_145^0, lt_22^0'=lt_22^post13, k_145^0'=-1+k_145^0, __patmp2^0'=-1+k_145^0, len_165^0'=1+len_165^0, x_13^0'=lt_21^10, lt_21^0'=lt_21^post13, __patmp1^0'=1+len_165^0, (-1+k_145^0 >= 0 /\ len_165^0 >= 0), cost: 3

Applied deletion
Removed the following rules: 29 36

Eliminating location l9 by chaining:

Applied chaining
First rule:
l4 -> l9 : lt_25^0'=lt_25^post6, x_17^0'=lt_25^10, Result_4^0'=Result_4^post6, y_18^0'=lt_25^10, t_16^0'=lt_25^10, lt_26^0'=lt_26^post6, (-1+k_145^0 >= 0 /\ y_12^0-x_13^0 == 0 /\ len_165^0 >= 0), cost: 3
Second rule:
l9 -> l10 : 0 == 0, cost: 1
New rule:
l4 -> l10 : lt_25^0'=lt_25^post6, x_17^0'=lt_25^10, Result_4^0'=Result_4^post6, y_18^0'=lt_25^10, t_16^0'=lt_25^10, lt_26^0'=lt_26^post6, (0 == 0 /\ -1+k_145^0 >= 0 /\ y_12^0-x_13^0 == 0 /\ len_165^0 >= 0), cost: 4

Applied simplification
Original rule:
l4 -> l10 : lt_25^0'=lt_25^post6, x_17^0'=lt_25^10, Result_4^0'=Result_4^post6, y_18^0'=lt_25^10, t_16^0'=lt_25^10, lt_26^0'=lt_26^post6, (0 == 0 /\ -1+k_145^0 >= 0 /\ y_12^0-x_13^0 == 0 /\ len_165^0 >= 0), cost: 4
New rule:
l4 -> l10 : lt_25^0'=lt_25^post6, x_17^0'=lt_25^10, Result_4^0'=Result_4^post6, y_18^0'=lt_25^10, t_16^0'=lt_25^10, lt_26^0'=lt_26^post6, (-1+k_145^0 >= 0 /\ y_12^0-x_13^0 == 0 /\ len_165^0 >= 0), cost: 4

Applied deletion
Removed the following rules: 25 37

Eliminating location l11 by chaining:

Applied chaining
First rule:
l4 -> l11 : k_191^0'=-1+k_145^0, lt_22^0'=lt_22^post13, k_145^0'=-1+k_145^0, __patmp2^0'=-1+k_145^0, len_165^0'=1+len_165^0, x_13^0'=lt_21^10, lt_21^0'=lt_21^post13, __patmp1^0'=1+len_165^0, (-1+k_145^0 >= 0 /\ len_165^0 >= 0), cost: 3
Second rule:
l11 -> l4 : TRUE, cost: 1
New rule:
l4 -> l4 : k_191^0'=-1+k_145^0, lt_22^0'=lt_22^post13, k_145^0'=-1+k_145^0, __patmp2^0'=-1+k_145^0, len_165^0'=1+len_165^0, x_13^0'=lt_21^10, lt_21^0'=lt_21^post13, __patmp1^0'=1+len_165^0, (-1+k_145^0 >= 0 /\ len_165^0 >= 0), cost: 4

Applied deletion
Removed the following rules: 30 38

Eliminating location l10 by chaining:

Applied chaining
First rule:
l4 -> l10 : lt_25^0'=lt_25^post6, x_17^0'=lt_25^10, Result_4^0'=Result_4^post6, y_18^0'=lt_25^10, t_16^0'=lt_25^10, lt_26^0'=lt_26^post6, (-1+k_145^0 >= 0 /\ y_12^0-x_13^0 == 0 /\ len_165^0 >= 0), cost: 4
Second rule:
l10 -> l0 : y_18^0'=x_17^0, t_16^0'=x_17^0, TRUE, cost: 1
New rule:
l4 -> l0 : lt_25^0'=lt_25^post6, x_17^0'=lt_25^10, Result_4^0'=Result_4^post6, y_18^0'=lt_25^10, t_16^0'=lt_25^10, lt_26^0'=lt_26^post6, (-1+k_145^0 >= 0 /\ y_12^0-x_13^0 == 0 /\ len_165^0 >= 0), cost: 5

Applied deletion
Removed the following rules: 26 39

Eliminating location l2 by chaining:

Applied chaining
First rule:
l0 -> l2 : 0 == 0, cost: 1
Second rule:
l2 -> l1 : y_18^0'=x_17^0, t_16^0'=x_17^0, TRUE, cost: 1
New rule:
l0 -> l1 : y_18^0'=x_17^0, t_16^0'=x_17^0, 0 == 0, cost: 2

Applied deletion
Removed the following rules: 16 17

Eliminating location l1 by chaining:

Applied chaining
First rule:
l0 -> l1 : y_18^0'=x_17^0, t_16^0'=x_17^0, 0 == 0, cost: 2
Second rule:
l1 -> l0 : TRUE, cost: 1
New rule:
l0 -> l0 : y_18^0'=x_17^0, t_16^0'=x_17^0, 0 == 0, cost: 3

Applied deletion
Removed the following rules: 18 42

Eliminated locations on linear paths
Start location: l14
  43: l0 -> l0 : y_18^0'=x_17^0, t_16^0'=x_17^0, 0 == 0, cost: 3
  40: l4 -> l4 : k_191^0'=-1+k_145^0, lt_22^0'=lt_22^post13, k_145^0'=-1+k_145^0, __patmp2^0'=-1+k_145^0, len_165^0'=1+len_165^0, x_13^0'=lt_21^10, lt_21^0'=lt_21^post13, __patmp1^0'=1+len_165^0, (-1+k_145^0 >= 0 /\ len_165^0 >= 0), cost: 4
  41: l4 -> l0 : lt_25^0'=lt_25^post6, x_17^0'=lt_25^10, Result_4^0'=Result_4^post6, y_18^0'=lt_25^10, t_16^0'=lt_25^10, lt_26^0'=lt_26^post6, (-1+k_145^0 >= 0 /\ y_12^0-x_13^0 == 0 /\ len_165^0 >= 0), cost: 5
  34: l14 -> l4 : lt_23^0'=lt_23^post5, __cil_tmp5_10^0'=tmp_9^post3, len_87^0'=2, lt_28^0'=lt_28^post3, y_20^0'=0, k_145^0'=2, tmp_9^0'=tmp_9^post3, lt_27^0'=lt_27^post3, Result_4^0'=tmp_9^post3, x_8^0'=tmp_9^post3, __patmp2^0'=2, lt_24^0'=lt_24^post5, len_165^0'=1, x_13^0'=lt_23^10, k_110^0'=2, lt_26^0'=lt_26^post3, x_19^0'=x_19^post3, __patmp1^0'=1, (0 == 0 /\ -2 <= 0 /\ 2 >= 0), cost: 4


Applied nonterm
Original rule:
l0 -> l0 : y_18^0'=x_17^0, t_16^0'=x_17^0, 0 == 0, cost: 3
New rule:
l0 -> [15] : (0 >= 0 /\ -1+n >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_lhBdIe.txt

Applied simplification
Original rule:
l0 -> [15] : (0 >= 0 /\ -1+n >= 0), cost: NONTERM
New rule:
l0 -> [15] : -1+n >= 0, cost: NONTERM

Applied deletion
Removed the following rules: 43

Applied acceleration
Original rule:
l4 -> l4 : k_191^0'=-1+k_145^0, lt_22^0'=lt_22^post13, k_145^0'=-1+k_145^0, __patmp2^0'=-1+k_145^0, len_165^0'=1+len_165^0, x_13^0'=lt_21^10, lt_21^0'=lt_21^post13, __patmp1^0'=1+len_165^0, (-1+k_145^0 >= 0 /\ len_165^0 >= 0), cost: 4
New rule:
l4 -> l4 : k_191^0'=k_145^0-n0, lt_22^0'=lt_22^post13, k_145^0'=k_145^0-n0, __patmp2^0'=k_145^0-n0, len_165^0'=n0+len_165^0, x_13^0'=lt_21^10, lt_21^0'=lt_21^post13, __patmp1^0'=n0+len_165^0, (k_145^0-n0 >= 0 /\ len_165^0 >= 0 /\ -1+n0 >= 0), cost: 4*n0
Sub-proof via acceration calculus written to file:///tmp/tmpnam_oJmhAN.txt

Applied instantiation
Original rule:
l4 -> l4 : k_191^0'=k_145^0-n0, lt_22^0'=lt_22^post13, k_145^0'=k_145^0-n0, __patmp2^0'=k_145^0-n0, len_165^0'=n0+len_165^0, x_13^0'=lt_21^10, lt_21^0'=lt_21^post13, __patmp1^0'=n0+len_165^0, (k_145^0-n0 >= 0 /\ len_165^0 >= 0 /\ -1+n0 >= 0), cost: 4*n0
New rule:
l4 -> l4 : k_191^0'=0, lt_22^0'=lt_22^post13, k_145^0'=0, __patmp2^0'=0, len_165^0'=k_145^0+len_165^0, x_13^0'=lt_21^10, lt_21^0'=lt_21^post13, __patmp1^0'=k_145^0+len_165^0, (0 >= 0 /\ -1+k_145^0 >= 0 /\ len_165^0 >= 0), cost: 4*k_145^0

Applied simplification
Original rule:
l4 -> l4 : k_191^0'=0, lt_22^0'=lt_22^post13, k_145^0'=0, __patmp2^0'=0, len_165^0'=k_145^0+len_165^0, x_13^0'=lt_21^10, lt_21^0'=lt_21^post13, __patmp1^0'=k_145^0+len_165^0, (0 >= 0 /\ -1+k_145^0 >= 0 /\ len_165^0 >= 0), cost: 4*k_145^0
New rule:
l4 -> l4 : k_191^0'=0, lt_22^0'=lt_22^post13, k_145^0'=0, __patmp2^0'=0, len_165^0'=k_145^0+len_165^0, x_13^0'=lt_21^10, lt_21^0'=lt_21^post13, __patmp1^0'=k_145^0+len_165^0, (-1+k_145^0 >= 0 /\ len_165^0 >= 0), cost: 4*k_145^0

Applied deletion
Removed the following rules: 40

Accelerated simple loops
Start location: l14
  45: l0 -> [15] : -1+n >= 0, cost: NONTERM
  41: l4 -> l0 : lt_25^0'=lt_25^post6, x_17^0'=lt_25^10, Result_4^0'=Result_4^post6, y_18^0'=lt_25^10, t_16^0'=lt_25^10, lt_26^0'=lt_26^post6, (-1+k_145^0 >= 0 /\ y_12^0-x_13^0 == 0 /\ len_165^0 >= 0), cost: 5
  47: l4 -> l4 : k_191^0'=0, lt_22^0'=lt_22^post13, k_145^0'=0, __patmp2^0'=0, len_165^0'=k_145^0+len_165^0, x_13^0'=lt_21^10, lt_21^0'=lt_21^post13, __patmp1^0'=k_145^0+len_165^0, (-1+k_145^0 >= 0 /\ len_165^0 >= 0), cost: 4*k_145^0
  34: l14 -> l4 : lt_23^0'=lt_23^post5, __cil_tmp5_10^0'=tmp_9^post3, len_87^0'=2, lt_28^0'=lt_28^post3, y_20^0'=0, k_145^0'=2, tmp_9^0'=tmp_9^post3, lt_27^0'=lt_27^post3, Result_4^0'=tmp_9^post3, x_8^0'=tmp_9^post3, __patmp2^0'=2, lt_24^0'=lt_24^post5, len_165^0'=1, x_13^0'=lt_23^10, k_110^0'=2, lt_26^0'=lt_26^post3, x_19^0'=x_19^post3, __patmp1^0'=1, (0 == 0 /\ -2 <= 0 /\ 2 >= 0), cost: 4


Applied chaining
First rule:
l4 -> l0 : lt_25^0'=lt_25^post6, x_17^0'=lt_25^10, Result_4^0'=Result_4^post6, y_18^0'=lt_25^10, t_16^0'=lt_25^10, lt_26^0'=lt_26^post6, (-1+k_145^0 >= 0 /\ y_12^0-x_13^0 == 0 /\ len_165^0 >= 0), cost: 5
Second rule:
l0 -> [15] : -1+n >= 0, cost: NONTERM
New rule:
l4 -> [15] : (-1+k_145^0 >= 0 /\ y_12^0-x_13^0 == 0 /\ len_165^0 >= 0), cost: NONTERM

Applied deletion
Removed the following rules: 45

Applied chaining
First rule:
l14 -> l4 : lt_23^0'=lt_23^post5, __cil_tmp5_10^0'=tmp_9^post3, len_87^0'=2, lt_28^0'=lt_28^post3, y_20^0'=0, k_145^0'=2, tmp_9^0'=tmp_9^post3, lt_27^0'=lt_27^post3, Result_4^0'=tmp_9^post3, x_8^0'=tmp_9^post3, __patmp2^0'=2, lt_24^0'=lt_24^post5, len_165^0'=1, x_13^0'=lt_23^10, k_110^0'=2, lt_26^0'=lt_26^post3, x_19^0'=x_19^post3, __patmp1^0'=1, (0 == 0 /\ -2 <= 0 /\ 2 >= 0), cost: 4
Second rule:
l4 -> l4 : k_191^0'=0, lt_22^0'=lt_22^post13, k_145^0'=0, __patmp2^0'=0, len_165^0'=k_145^0+len_165^0, x_13^0'=lt_21^10, lt_21^0'=lt_21^post13, __patmp1^0'=k_145^0+len_165^0, (-1+k_145^0 >= 0 /\ len_165^0 >= 0), cost: 4*k_145^0
New rule:
l14 -> l4 : lt_23^0'=lt_23^post5, k_191^0'=0, __cil_tmp5_10^0'=tmp_9^post3, len_87^0'=2, lt_28^0'=lt_28^post3, y_20^0'=0, lt_22^0'=lt_22^post13, k_145^0'=0, tmp_9^0'=tmp_9^post3, lt_27^0'=lt_27^post3, Result_4^0'=tmp_9^post3, x_8^0'=tmp_9^post3, __patmp2^0'=0, lt_24^0'=lt_24^post5, len_165^0'=3, x_13^0'=lt_21^10, lt_21^0'=lt_21^post13, k_110^0'=2, lt_26^0'=lt_26^post3, x_19^0'=x_19^post3, __patmp1^0'=3, (0 == 0 /\ 1 >= 0 /\ -2 <= 0 /\ 2 >= 0), cost: 12

Applied deletion
Removed the following rules: 47

Chained accelerated rules with incoming rules
Start location: l14
  41: l4 -> l0 : lt_25^0'=lt_25^post6, x_17^0'=lt_25^10, Result_4^0'=Result_4^post6, y_18^0'=lt_25^10, t_16^0'=lt_25^10, lt_26^0'=lt_26^post6, (-1+k_145^0 >= 0 /\ y_12^0-x_13^0 == 0 /\ len_165^0 >= 0), cost: 5
  48: l4 -> [15] : (-1+k_145^0 >= 0 /\ y_12^0-x_13^0 == 0 /\ len_165^0 >= 0), cost: NONTERM
  34: l14 -> l4 : lt_23^0'=lt_23^post5, __cil_tmp5_10^0'=tmp_9^post3, len_87^0'=2, lt_28^0'=lt_28^post3, y_20^0'=0, k_145^0'=2, tmp_9^0'=tmp_9^post3, lt_27^0'=lt_27^post3, Result_4^0'=tmp_9^post3, x_8^0'=tmp_9^post3, __patmp2^0'=2, lt_24^0'=lt_24^post5, len_165^0'=1, x_13^0'=lt_23^10, k_110^0'=2, lt_26^0'=lt_26^post3, x_19^0'=x_19^post3, __patmp1^0'=1, (0 == 0 /\ -2 <= 0 /\ 2 >= 0), cost: 4
  49: l14 -> l4 : lt_23^0'=lt_23^post5, k_191^0'=0, __cil_tmp5_10^0'=tmp_9^post3, len_87^0'=2, lt_28^0'=lt_28^post3, y_20^0'=0, lt_22^0'=lt_22^post13, k_145^0'=0, tmp_9^0'=tmp_9^post3, lt_27^0'=lt_27^post3, Result_4^0'=tmp_9^post3, x_8^0'=tmp_9^post3, __patmp2^0'=0, lt_24^0'=lt_24^post5, len_165^0'=3, x_13^0'=lt_21^10, lt_21^0'=lt_21^post13, k_110^0'=2, lt_26^0'=lt_26^post3, x_19^0'=x_19^post3, __patmp1^0'=3, (0 == 0 /\ 1 >= 0 /\ -2 <= 0 /\ 2 >= 0), cost: 12


Removed unreachable locations and irrelevant leafs
Start location: l14
  48: l4 -> [15] : (-1+k_145^0 >= 0 /\ y_12^0-x_13^0 == 0 /\ len_165^0 >= 0), cost: NONTERM
  34: l14 -> l4 : lt_23^0'=lt_23^post5, __cil_tmp5_10^0'=tmp_9^post3, len_87^0'=2, lt_28^0'=lt_28^post3, y_20^0'=0, k_145^0'=2, tmp_9^0'=tmp_9^post3, lt_27^0'=lt_27^post3, Result_4^0'=tmp_9^post3, x_8^0'=tmp_9^post3, __patmp2^0'=2, lt_24^0'=lt_24^post5, len_165^0'=1, x_13^0'=lt_23^10, k_110^0'=2, lt_26^0'=lt_26^post3, x_19^0'=x_19^post3, __patmp1^0'=1, (0 == 0 /\ -2 <= 0 /\ 2 >= 0), cost: 4
  49: l14 -> l4 : lt_23^0'=lt_23^post5, k_191^0'=0, __cil_tmp5_10^0'=tmp_9^post3, len_87^0'=2, lt_28^0'=lt_28^post3, y_20^0'=0, lt_22^0'=lt_22^post13, k_145^0'=0, tmp_9^0'=tmp_9^post3, lt_27^0'=lt_27^post3, Result_4^0'=tmp_9^post3, x_8^0'=tmp_9^post3, __patmp2^0'=0, lt_24^0'=lt_24^post5, len_165^0'=3, x_13^0'=lt_21^10, lt_21^0'=lt_21^post13, k_110^0'=2, lt_26^0'=lt_26^post3, x_19^0'=x_19^post3, __patmp1^0'=3, (0 == 0 /\ 1 >= 0 /\ -2 <= 0 /\ 2 >= 0), cost: 12


Eliminating location l4 by chaining:

Applied chaining
First rule:
l14 -> l4 : lt_23^0'=lt_23^post5, __cil_tmp5_10^0'=tmp_9^post3, len_87^0'=2, lt_28^0'=lt_28^post3, y_20^0'=0, k_145^0'=2, tmp_9^0'=tmp_9^post3, lt_27^0'=lt_27^post3, Result_4^0'=tmp_9^post3, x_8^0'=tmp_9^post3, __patmp2^0'=2, lt_24^0'=lt_24^post5, len_165^0'=1, x_13^0'=lt_23^10, k_110^0'=2, lt_26^0'=lt_26^post3, x_19^0'=x_19^post3, __patmp1^0'=1, (0 == 0 /\ -2 <= 0 /\ 2 >= 0), cost: 4
Second rule:
l4 -> [15] : (-1+k_145^0 >= 0 /\ y_12^0-x_13^0 == 0 /\ len_165^0 >= 0), cost: NONTERM
New rule:
l14 -> [15] : (0 == 0 /\ 1 >= 0 /\ -2 <= 0 /\ 2 >= 0 /\ y_12^0-lt_23^10 == 0), cost: NONTERM

Applied simplification
Original rule:
l14 -> [15] : (0 == 0 /\ 1 >= 0 /\ -2 <= 0 /\ 2 >= 0 /\ y_12^0-lt_23^10 == 0), cost: NONTERM
New rule:
l14 -> [15] : y_12^0-lt_23^10 == 0, cost: NONTERM

Applied deletion
Removed the following rules: 34 48 49

Eliminated locations on tree-shaped paths
Start location: l14
  50: l14 -> [15] : y_12^0-lt_23^10 == 0, cost: NONTERM


Computing asymptotic complexity
Proved nontermination of rule 50 via SMT.

Proved the following lower bound
Complexity:  Nonterm
Cpx degree: Nonterm

Solved cost: NONTERM
Rule cost:   NONTERM
Rule guard:  y_12^0-lt_23^10 == 0