NO

Initial ITS
Start location: l14
   0: l0 -> l2 : a_11^0'=a_11^post0, lt_34^0'=lt_34^post0, lt_24^0'=lt_24^post0, y_20^0'=y_20^post0, x_13^0'=x_13^post0, ___cil_tmp5_10^0'=___cil_tmp5_10^post0, lt_26^0'=lt_26^post0, k_289^0'=k_289^post0, t_18^0'=t_18^post0, lt_36^0'=lt_36^post0, x_22^0'=x_22^post0, k_187^0'=k_187^post0, ___patmp2^0'=___patmp2^post0, lt_32^0'=lt_32^post0, len_99^0'=len_99^post0, w_17^0'=w_17^post0, lt_38^0'=lt_38^post0, Result_4^0'=Result_4^post0, y_12^0'=y_12^post0, k_243^0'=k_243^post0, k_139^0'=k_139^post0, lt_35^0'=lt_35^post0, lt_25^0'=lt_25^post0, y_23^0'=y_23^post0, x_19^0'=x_19^post0, ___patmp1^0'=___patmp1^post0, lt_27^0'=lt_27^post0, len_263^0'=len_263^post0, tmp_9^0'=tmp_9^post0, lt_37^0'=lt_37^post0, x_8^0'=x_8^post0, k_208^0'=k_208^post0, (0 == 0 /\ lt_27^0-lt_27^post0 == 0 /\ lt_38^0-lt_38^post0 == 0 /\ -tmp_9^post0+tmp_9^0 == 0 /\ -lt_35^post0+lt_35^0 == 0 /\ -y_12^post0+y_12^0 == 0 /\ x_13^0-x_13^post0 == 0 /\ -___patmp1^post0+___patmp1^0 == 0 /\ a_11^0-a_11^post0 == 0 /\ -lt_37^post0+lt_37^0 == 0 /\ y_20^post0-w_17^0 == 0 /\ -len_99^post0+len_99^0 == 0 /\ ___cil_tmp5_10^0-___cil_tmp5_10^post0 == 0 /\ -w_17^post0+w_17^0 == 0 /\ lt_26^0-lt_26^post0 == 0 /\ x_22^0-x_22^post0 == 0 /\ -len_263^0 <= 0 /\ -len_263^post0+len_263^0 == 0 /\ x_19^post0-lt_32^10 == 0 /\ -x_13^0+y_12^0 <= 0 /\ -k_208^post0+k_208^0 == 0 /\ lt_36^0-lt_36^post0 == 0 /\ -k_187^post0+k_187^0 == 0 /\ -x_8^post0+x_8^0 == 0 /\ lt_25^0-lt_25^post0 == 0 /\ k_289^0-k_289^post0 == 0 /\ -t_18^post0+t_18^0 == 0 /\ -k_243^post0+k_243^0 == 0 /\ 1-k_243^0 <= 0 /\ x_13^0-y_12^0 <= 0 /\ ___patmp2^0-___patmp2^post0 == 0 /\ y_23^0-y_23^post0 == 0 /\ -k_139^post0+k_139^0 == 0 /\ lt_24^0-lt_24^post0 == 0), cost: 1
   7: l0 -> l7 : a_11^0'=a_11^post7, lt_34^0'=lt_34^post7, lt_24^0'=lt_24^post7, y_20^0'=y_20^post7, x_13^0'=x_13^post7, ___cil_tmp5_10^0'=___cil_tmp5_10^post7, lt_26^0'=lt_26^post7, k_289^0'=k_289^post7, t_18^0'=t_18^post7, lt_36^0'=lt_36^post7, x_22^0'=x_22^post7, k_187^0'=k_187^post7, ___patmp2^0'=___patmp2^post7, lt_32^0'=lt_32^post7, len_99^0'=len_99^post7, w_17^0'=w_17^post7, lt_38^0'=lt_38^post7, Result_4^0'=Result_4^post7, y_12^0'=y_12^post7, k_243^0'=k_243^post7, k_139^0'=k_139^post7, lt_35^0'=lt_35^post7, lt_25^0'=lt_25^post7, y_23^0'=y_23^post7, x_19^0'=x_19^post7, ___patmp1^0'=___patmp1^post7, lt_27^0'=lt_27^post7, len_263^0'=len_263^post7, tmp_9^0'=tmp_9^post7, lt_37^0'=lt_37^post7, x_8^0'=x_8^post7, k_208^0'=k_208^post7, (-Result_4^post7+Result_4^0 == 0 /\ lt_26^0-lt_26^post7 == 0 /\ lt_34^0-lt_34^post7 == 0 /\ -len_263^post7+len_263^0 == 0 /\ lt_24^0-lt_24^post7 == 0 /\ -lt_38^post7+lt_38^0 == 0 /\ y_12^0-y_12^post7 == 0 /\ -lt_32^post7+lt_32^0 == 0 /\ -len_263^0 <= 0 /\ lt_36^0-lt_36^post7 == 0 /\ -tmp_9^post7+tmp_9^0 == 0 /\ -k_243^post7+k_243^0 == 0 /\ y_20^0-y_20^post7 == 0 /\ ___patmp1^0-___patmp1^post7 == 0 /\ k_139^0-k_139^post7 == 0 /\ -len_99^post7+len_99^0 == 0 /\ -x_13^post7+x_13^0 == 0 /\ -lt_27^post7+lt_27^0 == 0 /\ -lt_35^post7+lt_35^0 == 0 /\ 1+k_289^post7-k_243^0 == 0 /\ t_18^0-t_18^post7 == 0 /\ -k_208^post7+k_208^0 == 0 /\ -lt_37^post7+lt_37^0 == 0 /\ ___patmp2^0-___patmp2^post7 == 0 /\ -x_19^post7+x_19^0 == 0 /\ 1-k_243^0 <= 0 /\ -x_22^post7+x_22^0 == 0 /\ -x_8^post7+x_8^0 == 0 /\ ___cil_tmp5_10^0-___cil_tmp5_10^post7 == 0 /\ -lt_25^post7+lt_25^0 == 0 /\ w_17^0-w_17^post7 == 0 /\ k_187^0-k_187^post7 == 0 /\ -y_23^post7+y_23^0 == 0 /\ a_11^0-a_11^post7 == 0), cost: 1
   1: l2 -> l3 : a_11^0'=a_11^post1, lt_34^0'=lt_34^post1, lt_24^0'=lt_24^post1, y_20^0'=y_20^post1, x_13^0'=x_13^post1, ___cil_tmp5_10^0'=___cil_tmp5_10^post1, lt_26^0'=lt_26^post1, k_289^0'=k_289^post1, t_18^0'=t_18^post1, lt_36^0'=lt_36^post1, x_22^0'=x_22^post1, k_187^0'=k_187^post1, ___patmp2^0'=___patmp2^post1, lt_32^0'=lt_32^post1, len_99^0'=len_99^post1, w_17^0'=w_17^post1, lt_38^0'=lt_38^post1, Result_4^0'=Result_4^post1, y_12^0'=y_12^post1, k_243^0'=k_243^post1, k_139^0'=k_139^post1, lt_35^0'=lt_35^post1, lt_25^0'=lt_25^post1, y_23^0'=y_23^post1, x_19^0'=x_19^post1, ___patmp1^0'=___patmp1^post1, lt_27^0'=lt_27^post1, len_263^0'=len_263^post1, tmp_9^0'=tmp_9^post1, lt_37^0'=lt_37^post1, x_8^0'=x_8^post1, k_208^0'=k_208^post1, (-x_19^post1+x_19^0 == 0 /\ -len_263^post1+len_263^0 == 0 /\ a_11^0-a_11^post1 == 0 /\ -k_208^post1+k_208^0 == 0 /\ k_243^0-k_243^post1 == 0 /\ lt_32^0-lt_32^post1 == 0 /\ -x_8^post1+x_8^0 == 0 /\ -y_23^post1+y_23^0 == 0 /\ lt_24^0-lt_24^post1 == 0 /\ -k_187^post1+k_187^0 == 0 /\ y_20^0-y_20^post1 == 0 /\ lt_36^0-lt_36^post1 == 0 /\ -lt_27^post1+lt_27^0 == 0 /\ -___patmp2^post1+___patmp2^0 == 0 /\ x_13^0-x_13^post1 == 0 /\ -k_139^post1+k_139^0 == 0 /\ lt_26^0-lt_26^post1 == 0 /\ len_99^0-len_99^post1 == 0 /\ lt_34^0-lt_34^post1 == 0 /\ x_22^0-x_22^post1 == 0 /\ lt_25^0-lt_25^post1 == 0 /\ -___patmp1^post1+___patmp1^0 == 0 /\ -tmp_9^post1+tmp_9^0 == 0 /\ -y_12^post1+y_12^0 == 0 /\ -___cil_tmp5_10^post1+___cil_tmp5_10^0 == 0 /\ -t_18^post1+t_18^0 == 0 /\ -Result_4^post1+Result_4^0 == 0 /\ k_289^0-k_289^post1 == 0 /\ lt_38^0-lt_38^post1 == 0 /\ -lt_35^post1+lt_35^0 == 0 /\ 1+w_17^0-x_19^0 <= 0 /\ -w_17^post1+w_17^0 == 0 /\ -lt_37^post1+lt_37^0 == 0), cost: 1
   2: l2 -> l3 : a_11^0'=a_11^post2, lt_34^0'=lt_34^post2, lt_24^0'=lt_24^post2, y_20^0'=y_20^post2, x_13^0'=x_13^post2, ___cil_tmp5_10^0'=___cil_tmp5_10^post2, lt_26^0'=lt_26^post2, k_289^0'=k_289^post2, t_18^0'=t_18^post2, lt_36^0'=lt_36^post2, x_22^0'=x_22^post2, k_187^0'=k_187^post2, ___patmp2^0'=___patmp2^post2, lt_32^0'=lt_32^post2, len_99^0'=len_99^post2, w_17^0'=w_17^post2, lt_38^0'=lt_38^post2, Result_4^0'=Result_4^post2, y_12^0'=y_12^post2, k_243^0'=k_243^post2, k_139^0'=k_139^post2, lt_35^0'=lt_35^post2, lt_25^0'=lt_25^post2, y_23^0'=y_23^post2, x_19^0'=x_19^post2, ___patmp1^0'=___patmp1^post2, lt_27^0'=lt_27^post2, len_263^0'=len_263^post2, tmp_9^0'=tmp_9^post2, lt_37^0'=lt_37^post2, x_8^0'=x_8^post2, k_208^0'=k_208^post2, (k_289^0-k_289^post2 == 0 /\ -y_12^post2+y_12^0 == 0 /\ -___patmp2^post2+___patmp2^0 == 0 /\ lt_36^0-lt_36^post2 == 0 /\ -k_139^post2+k_139^0 == 0 /\ -tmp_9^post2+tmp_9^0 == 0 /\ -lt_35^post2+lt_35^0 == 0 /\ k_243^0-k_243^post2 == 0 /\ -t_18^post2+t_18^0 == 0 /\ lt_24^0-lt_24^post2 == 0 /\ Result_4^0-Result_4^post2 == 0 /\ -lt_37^post2+lt_37^0 == 0 /\ lt_32^0-lt_32^post2 == 0 /\ -len_263^post2+len_263^0 == 0 /\ -w_17^post2+w_17^0 == 0 /\ -x_8^post2+x_8^0 == 0 /\ -k_208^post2+k_208^0 == 0 /\ lt_38^0-lt_38^post2 == 0 /\ y_20^0-y_20^post2 == 0 /\ -lt_27^post2+lt_27^0 == 0 /\ 1-w_17^0+x_19^0 <= 0 /\ x_22^0-x_22^post2 == 0 /\ x_13^0-x_13^post2 == 0 /\ -y_23^post2+y_23^0 == 0 /\ ___cil_tmp5_10^0-___cil_tmp5_10^post2 == 0 /\ lt_26^0-lt_26^post2 == 0 /\ -lt_34^post2+lt_34^0 == 0 /\ lt_25^0-lt_25^post2 == 0 /\ a_11^0-a_11^post2 == 0 /\ len_99^0-len_99^post2 == 0 /\ -___patmp1^post2+___patmp1^0 == 0 /\ k_187^0-k_187^post2 == 0 /\ -x_19^post2+x_19^0 == 0), cost: 1
   3: l3 -> l4 : a_11^0'=a_11^post3, lt_34^0'=lt_34^post3, lt_24^0'=lt_24^post3, y_20^0'=y_20^post3, x_13^0'=x_13^post3, ___cil_tmp5_10^0'=___cil_tmp5_10^post3, lt_26^0'=lt_26^post3, k_289^0'=k_289^post3, t_18^0'=t_18^post3, lt_36^0'=lt_36^post3, x_22^0'=x_22^post3, k_187^0'=k_187^post3, ___patmp2^0'=___patmp2^post3, lt_32^0'=lt_32^post3, len_99^0'=len_99^post3, w_17^0'=w_17^post3, lt_38^0'=lt_38^post3, Result_4^0'=Result_4^post3, y_12^0'=y_12^post3, k_243^0'=k_243^post3, k_139^0'=k_139^post3, lt_35^0'=lt_35^post3, lt_25^0'=lt_25^post3, y_23^0'=y_23^post3, x_19^0'=x_19^post3, ___patmp1^0'=___patmp1^post3, lt_27^0'=lt_27^post3, len_263^0'=len_263^post3, tmp_9^0'=tmp_9^post3, lt_37^0'=lt_37^post3, x_8^0'=x_8^post3, k_208^0'=k_208^post3, (-y_23^post3+y_23^0 == 0 /\ -lt_37^post3+lt_37^0 == 0 /\ Result_4^0-Result_4^post3 == 0 /\ -lt_38^post3+lt_38^0 == 0 /\ len_263^0-len_263^post3 == 0 /\ -lt_25^post3+lt_25^0 == 0 /\ -lt_27^post3+lt_27^0 == 0 /\ -___patmp1^post3+___patmp1^0 == 0 /\ k_289^0-k_289^post3 == 0 /\ lt_24^0-lt_24^post3 == 0 /\ -x_8^post3+x_8^0 == 0 /\ -w_17^post3+w_17^0 == 0 /\ k_243^0-k_243^post3 == 0 /\ -lt_36^post3+lt_36^0 == 0 /\ -k_208^post3+k_208^0 == 0 /\ -___patmp2^post3+___patmp2^0 == 0 /\ -y_12^post3+y_12^0 == 0 /\ x_19^0-x_19^post3 == 0 /\ lt_32^0-lt_32^post3 == 0 /\ -k_139^post3+k_139^0 == 0 /\ x_13^0-x_13^post3 == 0 /\ k_187^0-k_187^post3 == 0 /\ ___cil_tmp5_10^0-___cil_tmp5_10^post3 == 0 /\ -tmp_9^post3+tmp_9^0 == 0 /\ lt_26^0-lt_26^post3 == 0 /\ y_20^post3-t_18^post3 == 0 /\ -lt_34^post3+lt_34^0 == 0 /\ a_11^0-a_11^post3 == 0 /\ len_99^0-len_99^post3 == 0 /\ -x_19^0+t_18^post3 == 0 /\ x_22^0-x_22^post3 == 0 /\ -lt_35^post3+lt_35^0 == 0), cost: 1
   4: l4 -> l5 : a_11^0'=a_11^post4, lt_34^0'=lt_34^post4, lt_24^0'=lt_24^post4, y_20^0'=y_20^post4, x_13^0'=x_13^post4, ___cil_tmp5_10^0'=___cil_tmp5_10^post4, lt_26^0'=lt_26^post4, k_289^0'=k_289^post4, t_18^0'=t_18^post4, lt_36^0'=lt_36^post4, x_22^0'=x_22^post4, k_187^0'=k_187^post4, ___patmp2^0'=___patmp2^post4, lt_32^0'=lt_32^post4, len_99^0'=len_99^post4, w_17^0'=w_17^post4, lt_38^0'=lt_38^post4, Result_4^0'=Result_4^post4, y_12^0'=y_12^post4, k_243^0'=k_243^post4, k_139^0'=k_139^post4, lt_35^0'=lt_35^post4, lt_25^0'=lt_25^post4, y_23^0'=y_23^post4, x_19^0'=x_19^post4, ___patmp1^0'=___patmp1^post4, lt_27^0'=lt_27^post4, len_263^0'=len_263^post4, tmp_9^0'=tmp_9^post4, lt_37^0'=lt_37^post4, x_8^0'=x_8^post4, k_208^0'=k_208^post4, (-y_23^post4+y_23^0 == 0 /\ -lt_37^post4+lt_37^0 == 0 /\ -lt_26^post4+lt_26^0 == 0 /\ -lt_27^post4+lt_27^0 == 0 /\ -lt_38^post4+lt_38^0 == 0 /\ len_263^0-len_263^post4 == 0 /\ lt_34^0-lt_34^post4 == 0 /\ Result_4^0-Result_4^post4 == 0 /\ -lt_25^post4+lt_25^0 == 0 /\ -___patmp1^post4+___patmp1^0 == 0 /\ k_289^0-k_289^post4 == 0 /\ t_18^0-t_18^post4 == 0 /\ -x_8^post4+x_8^0 == 0 /\ -k_208^post4+k_208^0 == 0 /\ -y_12^post4+y_12^0 == 0 /\ -w_17^post4+w_17^0 == 0 /\ k_243^0-k_243^post4 == 0 /\ -lt_36^post4+lt_36^0 == 0 /\ ___cil_tmp5_10^0-___cil_tmp5_10^post4 == 0 /\ -___patmp2^post4+___patmp2^0 == 0 /\ x_19^0-x_19^post4 == 0 /\ lt_24^0-lt_24^post4 == 0 /\ -k_139^post4+k_139^0 == 0 /\ lt_32^0-lt_32^post4 == 0 /\ k_187^0-k_187^post4 == 0 /\ -lt_35^post4+lt_35^0 == 0 /\ -tmp_9^post4+tmp_9^0 == 0 /\ y_20^0-y_20^post4 == 0 /\ x_22^0-x_22^post4 == 0 /\ x_13^0-x_13^post4 == 0 /\ a_11^0-a_11^post4 == 0 /\ len_99^0-len_99^post4 == 0 /\ 1+w_17^0-x_19^0 <= 0), cost: 1
   5: l4 -> l5 : a_11^0'=a_11^post5, lt_34^0'=lt_34^post5, lt_24^0'=lt_24^post5, y_20^0'=y_20^post5, x_13^0'=x_13^post5, ___cil_tmp5_10^0'=___cil_tmp5_10^post5, lt_26^0'=lt_26^post5, k_289^0'=k_289^post5, t_18^0'=t_18^post5, lt_36^0'=lt_36^post5, x_22^0'=x_22^post5, k_187^0'=k_187^post5, ___patmp2^0'=___patmp2^post5, lt_32^0'=lt_32^post5, len_99^0'=len_99^post5, w_17^0'=w_17^post5, lt_38^0'=lt_38^post5, Result_4^0'=Result_4^post5, y_12^0'=y_12^post5, k_243^0'=k_243^post5, k_139^0'=k_139^post5, lt_35^0'=lt_35^post5, lt_25^0'=lt_25^post5, y_23^0'=y_23^post5, x_19^0'=x_19^post5, ___patmp1^0'=___patmp1^post5, lt_27^0'=lt_27^post5, len_263^0'=len_263^post5, tmp_9^0'=tmp_9^post5, lt_37^0'=lt_37^post5, x_8^0'=x_8^post5, k_208^0'=k_208^post5, (t_18^0-t_18^post5 == 0 /\ -___patmp2^post5+___patmp2^0 == 0 /\ x_13^0-x_13^post5 == 0 /\ y_12^0-y_12^post5 == 0 /\ len_99^0-len_99^post5 == 0 /\ x_22^0-x_22^post5 == 0 /\ -lt_36^post5+lt_36^0 == 0 /\ -tmp_9^post5+tmp_9^0 == 0 /\ -lt_38^post5+lt_38^0 == 0 /\ lt_34^0-lt_34^post5 == 0 /\ w_17^0-w_17^post5 == 0 /\ -len_263^post5+len_263^0 == 0 /\ -lt_35^post5+lt_35^0 == 0 /\ k_187^0-k_187^post5 == 0 /\ -lt_32^post5+lt_32^0 == 0 /\ -lt_37^post5+lt_37^0 == 0 /\ -lt_25^post5+lt_25^0 == 0 /\ -k_243^post5+k_243^0 == 0 /\ lt_24^0-lt_24^post5 == 0 /\ -y_23^post5+y_23^0 == 0 /\ k_289^0-k_289^post5 == 0 /\ 1-w_17^0+x_19^0 <= 0 /\ a_11^0-a_11^post5 == 0 /\ ___cil_tmp5_10^0-___cil_tmp5_10^post5 == 0 /\ -lt_27^post5+lt_27^0 == 0 /\ x_19^0-x_19^post5 == 0 /\ k_139^0-k_139^post5 == 0 /\ Result_4^0-Result_4^post5 == 0 /\ -lt_26^post5+lt_26^0 == 0 /\ -k_208^post5+k_208^0 == 0 /\ -___patmp1^post5+___patmp1^0 == 0 /\ -x_8^post5+x_8^0 == 0 /\ -y_20^post5+y_20^0 == 0), cost: 1
   6: l5 -> l1 : a_11^0'=a_11^post6, lt_34^0'=lt_34^post6, lt_24^0'=lt_24^post6, y_20^0'=y_20^post6, x_13^0'=x_13^post6, ___cil_tmp5_10^0'=___cil_tmp5_10^post6, lt_26^0'=lt_26^post6, k_289^0'=k_289^post6, t_18^0'=t_18^post6, lt_36^0'=lt_36^post6, x_22^0'=x_22^post6, k_187^0'=k_187^post6, ___patmp2^0'=___patmp2^post6, lt_32^0'=lt_32^post6, len_99^0'=len_99^post6, w_17^0'=w_17^post6, lt_38^0'=lt_38^post6, Result_4^0'=Result_4^post6, y_12^0'=y_12^post6, k_243^0'=k_243^post6, k_139^0'=k_139^post6, lt_35^0'=lt_35^post6, lt_25^0'=lt_25^post6, y_23^0'=y_23^post6, x_19^0'=x_19^post6, ___patmp1^0'=___patmp1^post6, lt_27^0'=lt_27^post6, len_263^0'=len_263^post6, tmp_9^0'=tmp_9^post6, lt_37^0'=lt_37^post6, x_8^0'=x_8^post6, k_208^0'=k_208^post6, (-lt_27^post6+lt_27^0 == 0 /\ -lt_25^post6+lt_25^0 == 0 /\ y_12^0-y_12^post6 == 0 /\ k_187^0-k_187^post6 == 0 /\ -lt_37^post6+lt_37^0 == 0 /\ w_17^0-w_17^post6 == 0 /\ -x_22^post6+x_22^0 == 0 /\ t_18^post6-x_19^0 == 0 /\ lt_36^0-lt_36^post6 == 0 /\ -x_19^post6+x_19^0 == 0 /\ x_13^0-x_13^post6 == 0 /\ -k_208^post6+k_208^0 == 0 /\ -y_23^post6+y_23^0 == 0 /\ a_11^0-a_11^post6 == 0 /\ -x_8^post6+x_8^0 == 0 /\ len_99^0-len_99^post6 == 0 /\ ___cil_tmp5_10^0-___cil_tmp5_10^post6 == 0 /\ -___patmp1^post6+___patmp1^0 == 0 /\ k_139^0-k_139^post6 == 0 /\ Result_4^0-Result_4^post6 == 0 /\ lt_34^0-lt_34^post6 == 0 /\ -t_18^post6+y_20^post6 == 0 /\ lt_26^0-lt_26^post6 == 0 /\ -lt_32^post6+lt_32^0 == 0 /\ -len_263^post6+len_263^0 == 0 /\ k_289^0-k_289^post6 == 0 /\ -lt_38^post6+lt_38^0 == 0 /\ -lt_35^post6+lt_35^0 == 0 /\ -lt_24^post6+lt_24^0 == 0 /\ ___patmp2^0-___patmp2^post6 == 0 /\ -k_243^post6+k_243^0 == 0 /\ tmp_9^0-tmp_9^post6 == 0), cost: 1
  16: l1 -> l13 : a_11^0'=a_11^post16, lt_34^0'=lt_34^post16, lt_24^0'=lt_24^post16, y_20^0'=y_20^post16, x_13^0'=x_13^post16, ___cil_tmp5_10^0'=___cil_tmp5_10^post16, lt_26^0'=lt_26^post16, k_289^0'=k_289^post16, t_18^0'=t_18^post16, lt_36^0'=lt_36^post16, x_22^0'=x_22^post16, k_187^0'=k_187^post16, ___patmp2^0'=___patmp2^post16, lt_32^0'=lt_32^post16, len_99^0'=len_99^post16, w_17^0'=w_17^post16, lt_38^0'=lt_38^post16, Result_4^0'=Result_4^post16, y_12^0'=y_12^post16, k_243^0'=k_243^post16, k_139^0'=k_139^post16, lt_35^0'=lt_35^post16, lt_25^0'=lt_25^post16, y_23^0'=y_23^post16, x_19^0'=x_19^post16, ___patmp1^0'=___patmp1^post16, lt_27^0'=lt_27^post16, len_263^0'=len_263^post16, tmp_9^0'=tmp_9^post16, lt_37^0'=lt_37^post16, x_8^0'=x_8^post16, k_208^0'=k_208^post16, (-k_139^post16+k_139^0 == 0 /\ k_289^0-k_289^post16 == 0 /\ a_11^0-a_11^post16 == 0 /\ len_263^0-len_263^post16 == 0 /\ -k_208^post16+k_208^0 == 0 /\ -lt_35^post16+lt_35^0 == 0 /\ -___patmp1^post16+___patmp1^0 == 0 /\ -tmp_9^post16+tmp_9^0 == 0 /\ lt_25^0-lt_25^post16 == 0 /\ lt_36^0-lt_36^post16 == 0 /\ -lt_38^post16+lt_38^0 == 0 /\ lt_24^0-lt_24^post16 == 0 /\ Result_4^0-Result_4^post16 == 0 /\ -y_23^post16+y_23^0 == 0 /\ k_243^0-k_243^post16 == 0 /\ lt_32^0-lt_32^post16 == 0 /\ -w_17^post16+w_17^0 == 0 /\ t_18^0-t_18^post16 == 0 /\ -lt_37^post16+lt_37^0 == 0 /\ -x_19^post16+x_19^0 == 0 /\ y_20^0-y_20^post16 == 0 /\ lt_34^0-lt_34^post16 == 0 /\ -x_8^post16+x_8^0 == 0 /\ -y_12^post16+y_12^0 == 0 /\ x_13^0-x_13^post16 == 0 /\ len_99^0-len_99^post16 == 0 /\ x_22^0-x_22^post16 == 0 /\ lt_26^0-lt_26^post16 == 0 /\ ___cil_tmp5_10^0-___cil_tmp5_10^post16 == 0 /\ -lt_27^post16+lt_27^0 == 0 /\ k_187^0-k_187^post16 == 0 /\ -___patmp2^post16+___patmp2^0 == 0 /\ 1+w_17^0-x_19^0 <= 0), cost: 1
  17: l1 -> l13 : a_11^0'=a_11^post17, lt_34^0'=lt_34^post17, lt_24^0'=lt_24^post17, y_20^0'=y_20^post17, x_13^0'=x_13^post17, ___cil_tmp5_10^0'=___cil_tmp5_10^post17, lt_26^0'=lt_26^post17, k_289^0'=k_289^post17, t_18^0'=t_18^post17, lt_36^0'=lt_36^post17, x_22^0'=x_22^post17, k_187^0'=k_187^post17, ___patmp2^0'=___patmp2^post17, lt_32^0'=lt_32^post17, len_99^0'=len_99^post17, w_17^0'=w_17^post17, lt_38^0'=lt_38^post17, Result_4^0'=Result_4^post17, y_12^0'=y_12^post17, k_243^0'=k_243^post17, k_139^0'=k_139^post17, lt_35^0'=lt_35^post17, lt_25^0'=lt_25^post17, y_23^0'=y_23^post17, x_19^0'=x_19^post17, ___patmp1^0'=___patmp1^post17, lt_27^0'=lt_27^post17, len_263^0'=len_263^post17, tmp_9^0'=tmp_9^post17, lt_37^0'=lt_37^post17, x_8^0'=x_8^post17, k_208^0'=k_208^post17, (-x_8^post17+x_8^0 == 0 /\ len_99^0-len_99^post17 == 0 /\ -lt_25^post17+lt_25^0 == 0 /\ y_12^0-y_12^post17 == 0 /\ k_289^0-k_289^post17 == 0 /\ -___patmp1^post17+___patmp1^0 == 0 /\ -lt_27^post17+lt_27^0 == 0 /\ t_18^0-t_18^post17 == 0 /\ len_263^0-len_263^post17 == 0 /\ -___patmp2^post17+___patmp2^0 == 0 /\ lt_24^0-lt_24^post17 == 0 /\ -y_23^post17+y_23^0 == 0 /\ x_19^0-x_19^post17 == 0 /\ -k_208^post17+k_208^0 == 0 /\ -lt_36^post17+lt_36^0 == 0 /\ -k_139^post17+k_139^0 == 0 /\ k_243^0-k_243^post17 == 0 /\ -lt_32^post17+lt_32^0 == 0 /\ k_187^0-k_187^post17 == 0 /\ -lt_38^post17+lt_38^0 == 0 /\ 1-w_17^0+x_19^0 <= 0 /\ x_13^0-x_13^post17 == 0 /\ -tmp_9^post17+tmp_9^0 == 0 /\ -lt_34^post17+lt_34^0 == 0 /\ y_20^0-y_20^post17 == 0 /\ lt_26^0-lt_26^post17 == 0 /\ a_11^0-a_11^post17 == 0 /\ -lt_35^post17+lt_35^0 == 0 /\ ___cil_tmp5_10^0-___cil_tmp5_10^post17 == 0 /\ -lt_37^post17+lt_37^0 == 0 /\ x_22^0-x_22^post17 == 0 /\ Result_4^0-Result_4^post17 == 0 /\ -w_17^post17+w_17^0 == 0), cost: 1
   8: l7 -> l8 : a_11^0'=a_11^post8, lt_34^0'=lt_34^post8, lt_24^0'=lt_24^post8, y_20^0'=y_20^post8, x_13^0'=x_13^post8, ___cil_tmp5_10^0'=___cil_tmp5_10^post8, lt_26^0'=lt_26^post8, k_289^0'=k_289^post8, t_18^0'=t_18^post8, lt_36^0'=lt_36^post8, x_22^0'=x_22^post8, k_187^0'=k_187^post8, ___patmp2^0'=___patmp2^post8, lt_32^0'=lt_32^post8, len_99^0'=len_99^post8, w_17^0'=w_17^post8, lt_38^0'=lt_38^post8, Result_4^0'=Result_4^post8, y_12^0'=y_12^post8, k_243^0'=k_243^post8, k_139^0'=k_139^post8, lt_35^0'=lt_35^post8, lt_25^0'=lt_25^post8, y_23^0'=y_23^post8, x_19^0'=x_19^post8, ___patmp1^0'=___patmp1^post8, lt_27^0'=lt_27^post8, len_263^0'=len_263^post8, tmp_9^0'=tmp_9^post8, lt_37^0'=lt_37^post8, x_8^0'=x_8^post8, k_208^0'=k_208^post8, (lt_34^0-lt_34^post8 == 0 /\ x_22^0-x_22^post8 == 0 /\ ___patmp2^0-___patmp2^post8 == 0 /\ -k_187^post8+k_187^0 == 0 /\ -x_19^post8+x_19^0 == 0 /\ -len_263^post8+len_263^0 == 0 /\ t_18^0-t_18^post8 == 0 /\ -k_208^post8+k_208^0 == 0 /\ -Result_4^post8+Result_4^0 == 0 /\ -x_8^post8+x_8^0 == 0 /\ -k_243^post8+k_243^0 == 0 /\ lt_26^0-lt_26^post8 == 0 /\ -k_139^post8+k_139^0 == 0 /\ -lt_27^post8+lt_27^0 == 0 /\ lt_38^0-lt_38^post8 == 0 /\ 1-x_13^0+y_12^0 <= 0 /\ w_17^0-w_17^post8 == 0 /\ a_11^0-a_11^post8 == 0 /\ lt_32^0-lt_32^post8 == 0 /\ -___patmp1^post8+___patmp1^0 == 0 /\ -tmp_9^post8+tmp_9^0 == 0 /\ -k_289^post8+k_289^0 == 0 /\ lt_35^0-lt_35^post8 == 0 /\ ___cil_tmp5_10^0-___cil_tmp5_10^post8 == 0 /\ lt_24^0-lt_24^post8 == 0 /\ y_20^0-y_20^post8 == 0 /\ lt_37^0-lt_37^post8 == 0 /\ -lt_25^post8+lt_25^0 == 0 /\ -y_12^post8+y_12^0 == 0 /\ lt_36^0-lt_36^post8 == 0 /\ y_23^0-y_23^post8 == 0 /\ -len_99^post8+len_99^0 == 0 /\ -x_13^post8+x_13^0 == 0), cost: 1
   9: l7 -> l8 : a_11^0'=a_11^post9, lt_34^0'=lt_34^post9, lt_24^0'=lt_24^post9, y_20^0'=y_20^post9, x_13^0'=x_13^post9, ___cil_tmp5_10^0'=___cil_tmp5_10^post9, lt_26^0'=lt_26^post9, k_289^0'=k_289^post9, t_18^0'=t_18^post9, lt_36^0'=lt_36^post9, x_22^0'=x_22^post9, k_187^0'=k_187^post9, ___patmp2^0'=___patmp2^post9, lt_32^0'=lt_32^post9, len_99^0'=len_99^post9, w_17^0'=w_17^post9, lt_38^0'=lt_38^post9, Result_4^0'=Result_4^post9, y_12^0'=y_12^post9, k_243^0'=k_243^post9, k_139^0'=k_139^post9, lt_35^0'=lt_35^post9, lt_25^0'=lt_25^post9, y_23^0'=y_23^post9, x_19^0'=x_19^post9, ___patmp1^0'=___patmp1^post9, lt_27^0'=lt_27^post9, len_263^0'=len_263^post9, tmp_9^0'=tmp_9^post9, lt_37^0'=lt_37^post9, x_8^0'=x_8^post9, k_208^0'=k_208^post9, (lt_38^0-lt_38^post9 == 0 /\ lt_27^0-lt_27^post9 == 0 /\ y_20^0-y_20^post9 == 0 /\ -tmp_9^post9+tmp_9^0 == 0 /\ y_23^0-y_23^post9 == 0 /\ -y_12^post9+y_12^0 == 0 /\ -lt_35^post9+lt_35^0 == 0 /\ -___patmp1^post9+___patmp1^0 == 0 /\ x_13^0-x_13^post9 == 0 /\ -lt_37^post9+lt_37^0 == 0 /\ a_11^0-a_11^post9 == 0 /\ lt_34^0-lt_34^post9 == 0 /\ ___cil_tmp5_10^0-___cil_tmp5_10^post9 == 0 /\ lt_26^0-lt_26^post9 == 0 /\ x_22^0-x_22^post9 == 0 /\ -Result_4^post9+Result_4^0 == 0 /\ -w_17^post9+w_17^0 == 0 /\ -len_99^post9+len_99^0 == 0 /\ -x_19^post9+x_19^0 == 0 /\ -len_263^post9+len_263^0 == 0 /\ -x_8^post9+x_8^0 == 0 /\ -k_208^post9+k_208^0 == 0 /\ lt_36^0-lt_36^post9 == 0 /\ -k_187^post9+k_187^0 == 0 /\ lt_25^0-lt_25^post9 == 0 /\ k_289^0-k_289^post9 == 0 /\ -t_18^post9+t_18^0 == 0 /\ 1+x_13^0-y_12^0 <= 0 /\ -k_243^post9+k_243^0 == 0 /\ ___patmp2^0-___patmp2^post9 == 0 /\ lt_32^0-lt_32^post9 == 0 /\ lt_24^0-lt_24^post9 == 0 /\ -k_139^post9+k_139^0 == 0), cost: 1
  10: l8 -> l6 : a_11^0'=a_11^post10, lt_34^0'=lt_34^post10, lt_24^0'=lt_24^post10, y_20^0'=y_20^post10, x_13^0'=x_13^post10, ___cil_tmp5_10^0'=___cil_tmp5_10^post10, lt_26^0'=lt_26^post10, k_289^0'=k_289^post10, t_18^0'=t_18^post10, lt_36^0'=lt_36^post10, x_22^0'=x_22^post10, k_187^0'=k_187^post10, ___patmp2^0'=___patmp2^post10, lt_32^0'=lt_32^post10, len_99^0'=len_99^post10, w_17^0'=w_17^post10, lt_38^0'=lt_38^post10, Result_4^0'=Result_4^post10, y_12^0'=y_12^post10, k_243^0'=k_243^post10, k_139^0'=k_139^post10, lt_35^0'=lt_35^post10, lt_25^0'=lt_25^post10, y_23^0'=y_23^post10, x_19^0'=x_19^post10, ___patmp1^0'=___patmp1^post10, lt_27^0'=lt_27^post10, len_263^0'=len_263^post10, tmp_9^0'=tmp_9^post10, lt_37^0'=lt_37^post10, x_8^0'=x_8^post10, k_208^0'=k_208^post10, (0 == 0 /\ -lt_27^post10+lt_27^0 == 0 /\ x_22^0-x_22^post10 == 0 /\ t_18^0-t_18^post10 == 0 /\ -k_187^post10+k_187^0 == 0 /\ -lt_32^post10+lt_32^0 == 0 /\ -k_289^0+___patmp2^post10 == 0 /\ lt_38^0-lt_38^post10 == 0 /\ k_243^post10-___patmp2^post10 == 0 /\ -x_19^post10+x_19^0 == 0 /\ -k_208^post10+k_208^0 == 0 /\ -len_99^post10+len_99^0 == 0 /\ -tmp_9^post10+tmp_9^0 == 0 /\ y_20^0-y_20^post10 == 0 /\ -len_263^0 <= 0 /\ a_11^0-a_11^post10 == 0 /\ -k_139^post10+k_139^0 == 0 /\ -k_289^post10+k_289^0 == 0 /\ x_13^post10-lt_24^10 == 0 /\ -k_289^0 <= 0 /\ -y_12^post10+y_12^0 == 0 /\ -lt_37^post10+lt_37^0 == 0 /\ w_17^0-w_17^post10 == 0 /\ -1+___patmp1^post10-len_263^0 == 0 /\ ___cil_tmp5_10^0-___cil_tmp5_10^post10 == 0 /\ -x_8^post10+x_8^0 == 0 /\ lt_26^0-lt_26^post10 == 0 /\ -Result_4^post10+Result_4^0 == 0 /\ y_23^0-y_23^post10 == 0 /\ lt_36^0-lt_36^post10 == 0 /\ -lt_34^post10+lt_34^0 == 0 /\ -___patmp1^post10+len_263^post10 == 0 /\ -lt_35^post10+lt_35^0 == 0), cost: 1
  11: l6 -> l0 : a_11^0'=a_11^post11, lt_34^0'=lt_34^post11, lt_24^0'=lt_24^post11, y_20^0'=y_20^post11, x_13^0'=x_13^post11, ___cil_tmp5_10^0'=___cil_tmp5_10^post11, lt_26^0'=lt_26^post11, k_289^0'=k_289^post11, t_18^0'=t_18^post11, lt_36^0'=lt_36^post11, x_22^0'=x_22^post11, k_187^0'=k_187^post11, ___patmp2^0'=___patmp2^post11, lt_32^0'=lt_32^post11, len_99^0'=len_99^post11, w_17^0'=w_17^post11, lt_38^0'=lt_38^post11, Result_4^0'=Result_4^post11, y_12^0'=y_12^post11, k_243^0'=k_243^post11, k_139^0'=k_139^post11, lt_35^0'=lt_35^post11, lt_25^0'=lt_25^post11, y_23^0'=y_23^post11, x_19^0'=x_19^post11, ___patmp1^0'=___patmp1^post11, lt_27^0'=lt_27^post11, len_263^0'=len_263^post11, tmp_9^0'=tmp_9^post11, lt_37^0'=lt_37^post11, x_8^0'=x_8^post11, k_208^0'=k_208^post11, (-len_263^post11+len_263^0 == 0 /\ -lt_38^post11+lt_38^0 == 0 /\ lt_26^0-lt_26^post11 == 0 /\ t_18^0-t_18^post11 == 0 /\ -x_8^post11+x_8^0 == 0 /\ -y_23^post11+y_23^0 == 0 /\ Result_4^0-Result_4^post11 == 0 /\ lt_32^0-lt_32^post11 == 0 /\ -lt_27^post11+lt_27^0 == 0 /\ -w_17^post11+w_17^0 == 0 /\ k_289^0-k_289^post11 == 0 /\ lt_24^0-lt_24^post11 == 0 /\ k_243^0-k_243^post11 == 0 /\ -tmp_9^post11+tmp_9^0 == 0 /\ -lt_35^post11+lt_35^0 == 0 /\ -y_20^post11+y_20^0 == 0 /\ -y_12^post11+y_12^0 == 0 /\ x_19^0-x_19^post11 == 0 /\ -k_208^post11+k_208^0 == 0 /\ x_13^0-x_13^post11 == 0 /\ -___patmp1^post11+___patmp1^0 == 0 /\ a_11^0-a_11^post11 == 0 /\ -___patmp2^post11+___patmp2^0 == 0 /\ -lt_37^post11+lt_37^0 == 0 /\ len_99^0-len_99^post11 == 0 /\ ___cil_tmp5_10^0-___cil_tmp5_10^post11 == 0 /\ k_187^0-k_187^post11 == 0 /\ x_22^0-x_22^post11 == 0 /\ -lt_25^post11+lt_25^0 == 0 /\ k_139^0-k_139^post11 == 0 /\ -lt_36^post11+lt_36^0 == 0 /\ -lt_34^post11+lt_34^0 == 0), cost: 1
  12: l9 -> l10 : a_11^0'=a_11^post12, lt_34^0'=lt_34^post12, lt_24^0'=lt_24^post12, y_20^0'=y_20^post12, x_13^0'=x_13^post12, ___cil_tmp5_10^0'=___cil_tmp5_10^post12, lt_26^0'=lt_26^post12, k_289^0'=k_289^post12, t_18^0'=t_18^post12, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=k_187^post12, ___patmp2^0'=___patmp2^post12, lt_32^0'=lt_32^post12, len_99^0'=len_99^post12, w_17^0'=w_17^post12, lt_38^0'=lt_38^post12, Result_4^0'=Result_4^post12, y_12^0'=y_12^post12, k_243^0'=k_243^post12, k_139^0'=k_139^post12, lt_35^0'=lt_35^post12, lt_25^0'=lt_25^post12, y_23^0'=y_23^post12, x_19^0'=x_19^post12, ___patmp1^0'=___patmp1^post12, lt_27^0'=lt_27^post12, len_263^0'=len_263^post12, tmp_9^0'=tmp_9^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=k_208^post12, (0 == 0 /\ -lt_27^post12+lt_27^0 == 0 /\ x_8^10-tmp_9^10 == 0 /\ t_18^0-t_18^post12 == 0 /\ y_23^post12 == 0 /\ -len_99^post12 <= 0 /\ -tmp_9^post12+x_8^post12 == 0 /\ -1+k_139^post12-len_99^post12 == 0 /\ a_11^0-a_11^post12 == 0 /\ -x_8^30+___cil_tmp5_10^30 == 0 /\ ___patmp2^0-___patmp2^post12 == 0 /\ -lt_25^post12+lt_25^0 == 0 /\ -k_187^post12+k_208^post12 == 0 /\ -x_8^20+___cil_tmp5_10^20 == 0 /\ Result_4^10-___cil_tmp5_10^10 == 0 /\ -1+k_187^post12-k_139^post12 == 0 /\ -lt_32^post12+lt_32^0 == 0 /\ -x_19^post12+x_19^0 == 0 /\ k_289^0-k_289^post12 == 0 /\ Result_4^20-___cil_tmp5_10^20 == 0 /\ -___cil_tmp5_10^post12+Result_4^post12 == 0 /\ -k_139^post12 <= 0 /\ lt_24^0-lt_24^post12 == 0 /\ -len_263^post12+len_263^0 == 0 /\ -x_8^10+___cil_tmp5_10^10 == 0 /\ Result_4^30-___cil_tmp5_10^30 == 0 /\ -___patmp1^post12+___patmp1^0 == 0 /\ -k_243^post12+k_243^0 == 0 /\ y_20^0-y_20^post12 == 0 /\ -tmp_9^20+x_8^20 == 0 /\ -w_17^post12+w_17^0 == 0 /\ lt_26^0-lt_26^post12 == 0 /\ -2+len_99^post12 == 0 /\ -k_187^post12 <= 0 /\ -y_12^post12+y_12^0 == 0 /\ -a_11^0+x_13^post12 == 0 /\ x_8^30-tmp_9^30 == 0 /\ ___cil_tmp5_10^post12-x_8^post12 == 0), cost: 1
  13: l10 -> l11 : a_11^0'=a_11^post13, lt_34^0'=lt_34^post13, lt_24^0'=lt_24^post13, y_20^0'=y_20^post13, x_13^0'=x_13^post13, ___cil_tmp5_10^0'=___cil_tmp5_10^post13, lt_26^0'=lt_26^post13, k_289^0'=k_289^post13, t_18^0'=t_18^post13, lt_36^0'=lt_36^post13, x_22^0'=x_22^post13, k_187^0'=k_187^post13, ___patmp2^0'=___patmp2^post13, lt_32^0'=lt_32^post13, len_99^0'=len_99^post13, w_17^0'=w_17^post13, lt_38^0'=lt_38^post13, Result_4^0'=Result_4^post13, y_12^0'=y_12^post13, k_243^0'=k_243^post13, k_139^0'=k_139^post13, lt_35^0'=lt_35^post13, lt_25^0'=lt_25^post13, y_23^0'=y_23^post13, x_19^0'=x_19^post13, ___patmp1^0'=___patmp1^post13, lt_27^0'=lt_27^post13, len_263^0'=len_263^post13, tmp_9^0'=tmp_9^post13, lt_37^0'=lt_37^post13, x_8^0'=x_8^post13, k_208^0'=k_208^post13, (k_187^0-k_187^post13 == 0 /\ ___patmp1^0-___patmp1^post13 == 0 /\ w_17^0-w_17^post13 == 0 /\ -len_263^post13+len_263^0 == 0 /\ -lt_25^post13+lt_25^0 == 0 /\ x_13^0-x_13^post13 == 0 /\ -k_208^post13+k_208^0 == 0 /\ -lt_36^post13+lt_36^0 == 0 /\ ___cil_tmp5_10^0-___cil_tmp5_10^post13 == 0 /\ -lt_27^post13+lt_27^0 == 0 /\ a_11^0-a_11^post13 == 0 /\ y_20^0-y_20^post13 == 0 /\ 1-x_13^0+y_12^0 <= 0 /\ y_12^0-y_12^post13 == 0 /\ -tmp_9^post13+tmp_9^0 == 0 /\ ___patmp2^0-___patmp2^post13 == 0 /\ -x_19^post13+x_19^0 == 0 /\ -x_22^post13+x_22^0 == 0 /\ y_23^0-y_23^post13 == 0 /\ -Result_4^post13+Result_4^0 == 0 /\ -lt_32^post13+lt_32^0 == 0 /\ lt_26^0-lt_26^post13 == 0 /\ k_289^0-k_289^post13 == 0 /\ lt_34^0-lt_34^post13 == 0 /\ -lt_24^post13+lt_24^0 == 0 /\ -x_8^post13+x_8^0 == 0 /\ -k_243^post13+k_243^0 == 0 /\ -lt_37^post13+lt_37^0 == 0 /\ -k_139^post13+k_139^0 == 0 /\ -lt_38^post13+lt_38^0 == 0 /\ lt_35^0-lt_35^post13 == 0 /\ t_18^0-t_18^post13 == 0 /\ -len_99^post13+len_99^0 == 0), cost: 1
  14: l10 -> l11 : a_11^0'=a_11^post14, lt_34^0'=lt_34^post14, lt_24^0'=lt_24^post14, y_20^0'=y_20^post14, x_13^0'=x_13^post14, ___cil_tmp5_10^0'=___cil_tmp5_10^post14, lt_26^0'=lt_26^post14, k_289^0'=k_289^post14, t_18^0'=t_18^post14, lt_36^0'=lt_36^post14, x_22^0'=x_22^post14, k_187^0'=k_187^post14, ___patmp2^0'=___patmp2^post14, lt_32^0'=lt_32^post14, len_99^0'=len_99^post14, w_17^0'=w_17^post14, lt_38^0'=lt_38^post14, Result_4^0'=Result_4^post14, y_12^0'=y_12^post14, k_243^0'=k_243^post14, k_139^0'=k_139^post14, lt_35^0'=lt_35^post14, lt_25^0'=lt_25^post14, y_23^0'=y_23^post14, x_19^0'=x_19^post14, ___patmp1^0'=___patmp1^post14, lt_27^0'=lt_27^post14, len_263^0'=len_263^post14, tmp_9^0'=tmp_9^post14, lt_37^0'=lt_37^post14, x_8^0'=x_8^post14, k_208^0'=k_208^post14, (-k_139^post14+k_139^0 == 0 /\ lt_38^0-lt_38^post14 == 0 /\ -len_263^post14+len_263^0 == 0 /\ x_22^0-x_22^post14 == 0 /\ ___patmp2^0-___patmp2^post14 == 0 /\ lt_26^0-lt_26^post14 == 0 /\ -___patmp1^post14+___patmp1^0 == 0 /\ -k_187^post14+k_187^0 == 0 /\ -x_8^post14+x_8^0 == 0 /\ -y_12^post14+y_12^0 == 0 /\ -Result_4^post14+Result_4^0 == 0 /\ -lt_27^post14+lt_27^0 == 0 /\ lt_35^0-lt_35^post14 == 0 /\ lt_24^0-lt_24^post14 == 0 /\ lt_36^0-lt_36^post14 == 0 /\ -x_19^post14+x_19^0 == 0 /\ w_17^0-w_17^post14 == 0 /\ lt_32^0-lt_32^post14 == 0 /\ -tmp_9^post14+tmp_9^0 == 0 /\ -k_208^post14+k_208^0 == 0 /\ -lt_25^post14+lt_25^0 == 0 /\ -k_243^post14+k_243^0 == 0 /\ t_18^0-t_18^post14 == 0 /\ x_13^0-x_13^post14 == 0 /\ 1+x_13^0-y_12^0 <= 0 /\ lt_34^0-lt_34^post14 == 0 /\ lt_37^0-lt_37^post14 == 0 /\ a_11^0-a_11^post14 == 0 /\ y_20^0-y_20^post14 == 0 /\ ___cil_tmp5_10^0-___cil_tmp5_10^post14 == 0 /\ y_23^0-y_23^post14 == 0 /\ -len_99^post14+len_99^0 == 0 /\ k_289^0-k_289^post14 == 0), cost: 1
  15: l11 -> l0 : a_11^0'=a_11^post15, lt_34^0'=lt_34^post15, lt_24^0'=lt_24^post15, y_20^0'=y_20^post15, x_13^0'=x_13^post15, ___cil_tmp5_10^0'=___cil_tmp5_10^post15, lt_26^0'=lt_26^post15, k_289^0'=k_289^post15, t_18^0'=t_18^post15, lt_36^0'=lt_36^post15, x_22^0'=x_22^post15, k_187^0'=k_187^post15, ___patmp2^0'=___patmp2^post15, lt_32^0'=lt_32^post15, len_99^0'=len_99^post15, w_17^0'=w_17^post15, lt_38^0'=lt_38^post15, Result_4^0'=Result_4^post15, y_12^0'=y_12^post15, k_243^0'=k_243^post15, k_139^0'=k_139^post15, lt_35^0'=lt_35^post15, lt_25^0'=lt_25^post15, y_23^0'=y_23^post15, x_19^0'=x_19^post15, ___patmp1^0'=___patmp1^post15, lt_27^0'=lt_27^post15, len_263^0'=len_263^post15, tmp_9^0'=tmp_9^post15, lt_37^0'=lt_37^post15, x_8^0'=x_8^post15, k_208^0'=k_208^post15, (0 == 0 /\ -k_289^post15+k_289^0 == 0 /\ y_12^0-y_12^post15 == 0 /\ -k_208^0 <= 0 /\ -x_8^post15+x_8^0 == 0 /\ len_99^0-len_99^post15 == 0 /\ -lt_36^post15+lt_36^0 == 0 /\ x_22^0-x_22^post15 == 0 /\ a_11^0-a_11^post15 == 0 /\ -lt_32^post15+lt_32^0 == 0 /\ lt_34^0-lt_34^post15 == 0 /\ y_20^0-y_20^post15 == 0 /\ ___patmp2^post15-k_208^0 == 0 /\ -tmp_9^post15+tmp_9^0 == 0 /\ -y_23^post15+y_23^0 == 0 /\ t_18^0-t_18^post15 == 0 /\ w_17^0-w_17^post15 == 0 /\ -lt_35^post15+lt_35^0 == 0 /\ k_187^0-k_187^post15 == 0 /\ Result_4^0-Result_4^post15 == 0 /\ -lt_25^post15+lt_25^0 == 0 /\ -1+___patmp1^post15 == 0 /\ -k_208^post15+k_208^0 == 0 /\ -lt_38^post15+lt_38^0 == 0 /\ k_139^0-k_139^post15 == 0 /\ x_19^0-x_19^post15 == 0 /\ -lt_37^post15+lt_37^0 == 0 /\ -___cil_tmp5_10^post15+___cil_tmp5_10^0 == 0 /\ -lt_26^10+x_13^post15 == 0 /\ -___patmp2^post15+k_243^post15 == 0 /\ -___patmp1^post15+len_263^post15 == 0 /\ lt_24^0-lt_24^post15 == 0), cost: 1
  18: l13 -> l12 : a_11^0'=a_11^post18, lt_34^0'=lt_34^post18, lt_24^0'=lt_24^post18, y_20^0'=y_20^post18, x_13^0'=x_13^post18, ___cil_tmp5_10^0'=___cil_tmp5_10^post18, lt_26^0'=lt_26^post18, k_289^0'=k_289^post18, t_18^0'=t_18^post18, lt_36^0'=lt_36^post18, x_22^0'=x_22^post18, k_187^0'=k_187^post18, ___patmp2^0'=___patmp2^post18, lt_32^0'=lt_32^post18, len_99^0'=len_99^post18, w_17^0'=w_17^post18, lt_38^0'=lt_38^post18, Result_4^0'=Result_4^post18, y_12^0'=y_12^post18, k_243^0'=k_243^post18, k_139^0'=k_139^post18, lt_35^0'=lt_35^post18, lt_25^0'=lt_25^post18, y_23^0'=y_23^post18, x_19^0'=x_19^post18, ___patmp1^0'=___patmp1^post18, lt_27^0'=lt_27^post18, len_263^0'=len_263^post18, tmp_9^0'=tmp_9^post18, lt_37^0'=lt_37^post18, x_8^0'=x_8^post18, k_208^0'=k_208^post18, (-x_8^post18+x_8^0 == 0 /\ len_99^0-len_99^post18 == 0 /\ y_20^post18-t_18^post18 == 0 /\ y_12^0-y_12^post18 == 0 /\ -lt_25^post18+lt_25^0 == 0 /\ -lt_26^post18+lt_26^0 == 0 /\ k_289^0-k_289^post18 == 0 /\ -lt_27^post18+lt_27^0 == 0 /\ len_263^0-len_263^post18 == 0 /\ -___patmp2^post18+___patmp2^0 == 0 /\ lt_24^0-lt_24^post18 == 0 /\ ___cil_tmp5_10^0-___cil_tmp5_10^post18 == 0 /\ -k_139^post18+k_139^0 == 0 /\ -y_23^post18+y_23^0 == 0 /\ x_19^0-x_19^post18 == 0 /\ -lt_32^post18+lt_32^0 == 0 /\ k_187^0-k_187^post18 == 0 /\ k_243^0-k_243^post18 == 0 /\ -lt_36^post18+lt_36^0 == 0 /\ -k_208^post18+k_208^0 == 0 /\ -___patmp1^post18+___patmp1^0 == 0 /\ -tmp_9^post18+tmp_9^0 == 0 /\ -lt_38^post18+lt_38^0 == 0 /\ -lt_35^post18+lt_35^0 == 0 /\ a_11^0-a_11^post18 == 0 /\ -lt_37^post18+lt_37^0 == 0 /\ x_13^0-x_13^post18 == 0 /\ x_22^0-x_22^post18 == 0 /\ Result_4^0-Result_4^post18 == 0 /\ -w_17^post18+w_17^0 == 0 /\ -x_19^0+t_18^post18 == 0 /\ -lt_34^post18+lt_34^0 == 0), cost: 1
  19: l12 -> l1 : a_11^0'=a_11^post19, lt_34^0'=lt_34^post19, lt_24^0'=lt_24^post19, y_20^0'=y_20^post19, x_13^0'=x_13^post19, ___cil_tmp5_10^0'=___cil_tmp5_10^post19, lt_26^0'=lt_26^post19, k_289^0'=k_289^post19, t_18^0'=t_18^post19, lt_36^0'=lt_36^post19, x_22^0'=x_22^post19, k_187^0'=k_187^post19, ___patmp2^0'=___patmp2^post19, lt_32^0'=lt_32^post19, len_99^0'=len_99^post19, w_17^0'=w_17^post19, lt_38^0'=lt_38^post19, Result_4^0'=Result_4^post19, y_12^0'=y_12^post19, k_243^0'=k_243^post19, k_139^0'=k_139^post19, lt_35^0'=lt_35^post19, lt_25^0'=lt_25^post19, y_23^0'=y_23^post19, x_19^0'=x_19^post19, ___patmp1^0'=___patmp1^post19, lt_27^0'=lt_27^post19, len_263^0'=len_263^post19, tmp_9^0'=tmp_9^post19, lt_37^0'=lt_37^post19, x_8^0'=x_8^post19, k_208^0'=k_208^post19, (-k_208^post19+k_208^0 == 0 /\ -lt_36^post19+lt_36^0 == 0 /\ lt_34^0-lt_34^post19 == 0 /\ y_20^0-y_20^post19 == 0 /\ -y_23^post19+y_23^0 == 0 /\ -___patmp2^post19+___patmp2^0 == 0 /\ t_18^0-t_18^post19 == 0 /\ x_13^0-x_13^post19 == 0 /\ x_22^0-x_22^post19 == 0 /\ len_99^0-len_99^post19 == 0 /\ -lt_38^post19+lt_38^0 == 0 /\ -tmp_9^post19+tmp_9^0 == 0 /\ ___cil_tmp5_10^0-___cil_tmp5_10^post19 == 0 /\ -lt_35^post19+lt_35^0 == 0 /\ w_17^0-w_17^post19 == 0 /\ k_187^0-k_187^post19 == 0 /\ y_12^0-y_12^post19 == 0 /\ -lt_32^post19+lt_32^0 == 0 /\ -lt_37^post19+lt_37^0 == 0 /\ -len_263^post19+len_263^0 == 0 /\ -lt_26^post19+lt_26^0 == 0 /\ k_289^0-k_289^post19 == 0 /\ -x_8^post19+x_8^0 == 0 /\ a_11^0-a_11^post19 == 0 /\ -k_243^post19+k_243^0 == 0 /\ -lt_27^post19+lt_27^0 == 0 /\ lt_24^0-lt_24^post19 == 0 /\ -lt_25^post19+lt_25^0 == 0 /\ k_139^0-k_139^post19 == 0 /\ x_19^0-x_19^post19 == 0 /\ -___patmp1^post19+___patmp1^0 == 0 /\ -Result_4^post19+Result_4^0 == 0), cost: 1
  20: l14 -> l9 : a_11^0'=a_11^post20, lt_34^0'=lt_34^post20, lt_24^0'=lt_24^post20, y_20^0'=y_20^post20, x_13^0'=x_13^post20, ___cil_tmp5_10^0'=___cil_tmp5_10^post20, lt_26^0'=lt_26^post20, k_289^0'=k_289^post20, t_18^0'=t_18^post20, lt_36^0'=lt_36^post20, x_22^0'=x_22^post20, k_187^0'=k_187^post20, ___patmp2^0'=___patmp2^post20, lt_32^0'=lt_32^post20, len_99^0'=len_99^post20, w_17^0'=w_17^post20, lt_38^0'=lt_38^post20, Result_4^0'=Result_4^post20, y_12^0'=y_12^post20, k_243^0'=k_243^post20, k_139^0'=k_139^post20, lt_35^0'=lt_35^post20, lt_25^0'=lt_25^post20, y_23^0'=y_23^post20, x_19^0'=x_19^post20, ___patmp1^0'=___patmp1^post20, lt_27^0'=lt_27^post20, len_263^0'=len_263^post20, tmp_9^0'=tmp_9^post20, lt_37^0'=lt_37^post20, x_8^0'=x_8^post20, k_208^0'=k_208^post20, (-lt_25^post20+lt_25^0 == 0 /\ ___cil_tmp5_10^0-___cil_tmp5_10^post20 == 0 /\ -k_243^post20+k_243^0 == 0 /\ -lt_37^post20+lt_37^0 == 0 /\ -Result_4^post20+Result_4^0 == 0 /\ y_20^0-y_20^post20 == 0 /\ w_17^0-w_17^post20 == 0 /\ k_187^0-k_187^post20 == 0 /\ -lt_27^post20+lt_27^0 == 0 /\ lt_36^0-lt_36^post20 == 0 /\ -___patmp1^post20+___patmp1^0 == 0 /\ x_13^0-x_13^post20 == 0 /\ lt_34^0-lt_34^post20 == 0 /\ y_12^0-y_12^post20 == 0 /\ a_11^0-a_11^post20 == 0 /\ -lt_38^post20+lt_38^0 == 0 /\ -x_19^post20+x_19^0 == 0 /\ len_99^0-len_99^post20 == 0 /\ -x_22^post20+x_22^0 == 0 /\ -x_8^post20+x_8^0 == 0 /\ lt_26^0-lt_26^post20 == 0 /\ k_139^0-k_139^post20 == 0 /\ -y_23^post20+y_23^0 == 0 /\ t_18^0-t_18^post20 == 0 /\ k_289^0-k_289^post20 == 0 /\ -len_263^post20+len_263^0 == 0 /\ lt_24^0-lt_24^post20 == 0 /\ ___patmp2^0-___patmp2^post20 == 0 /\ tmp_9^0-tmp_9^post20 == 0 /\ -lt_32^post20+lt_32^0 == 0 /\ -k_208^post20+k_208^0 == 0 /\ -lt_35^post20+lt_35^0 == 0), cost: 1


Applied preprocessing
Original rule:
l0 -> l2 : a_11^0'=a_11^post0, lt_34^0'=lt_34^post0, lt_24^0'=lt_24^post0, y_20^0'=y_20^post0, x_13^0'=x_13^post0, ___cil_tmp5_10^0'=___cil_tmp5_10^post0, lt_26^0'=lt_26^post0, k_289^0'=k_289^post0, t_18^0'=t_18^post0, lt_36^0'=lt_36^post0, x_22^0'=x_22^post0, k_187^0'=k_187^post0, ___patmp2^0'=___patmp2^post0, lt_32^0'=lt_32^post0, len_99^0'=len_99^post0, w_17^0'=w_17^post0, lt_38^0'=lt_38^post0, Result_4^0'=Result_4^post0, y_12^0'=y_12^post0, k_243^0'=k_243^post0, k_139^0'=k_139^post0, lt_35^0'=lt_35^post0, lt_25^0'=lt_25^post0, y_23^0'=y_23^post0, x_19^0'=x_19^post0, ___patmp1^0'=___patmp1^post0, lt_27^0'=lt_27^post0, len_263^0'=len_263^post0, tmp_9^0'=tmp_9^post0, lt_37^0'=lt_37^post0, x_8^0'=x_8^post0, k_208^0'=k_208^post0, (0 == 0 /\ lt_27^0-lt_27^post0 == 0 /\ lt_38^0-lt_38^post0 == 0 /\ -tmp_9^post0+tmp_9^0 == 0 /\ -lt_35^post0+lt_35^0 == 0 /\ -y_12^post0+y_12^0 == 0 /\ x_13^0-x_13^post0 == 0 /\ -___patmp1^post0+___patmp1^0 == 0 /\ a_11^0-a_11^post0 == 0 /\ -lt_37^post0+lt_37^0 == 0 /\ y_20^post0-w_17^0 == 0 /\ -len_99^post0+len_99^0 == 0 /\ ___cil_tmp5_10^0-___cil_tmp5_10^post0 == 0 /\ -w_17^post0+w_17^0 == 0 /\ lt_26^0-lt_26^post0 == 0 /\ x_22^0-x_22^post0 == 0 /\ -len_263^0 <= 0 /\ -len_263^post0+len_263^0 == 0 /\ x_19^post0-lt_32^10 == 0 /\ -x_13^0+y_12^0 <= 0 /\ -k_208^post0+k_208^0 == 0 /\ lt_36^0-lt_36^post0 == 0 /\ -k_187^post0+k_187^0 == 0 /\ -x_8^post0+x_8^0 == 0 /\ lt_25^0-lt_25^post0 == 0 /\ k_289^0-k_289^post0 == 0 /\ -t_18^post0+t_18^0 == 0 /\ -k_243^post0+k_243^0 == 0 /\ 1-k_243^0 <= 0 /\ x_13^0-y_12^0 <= 0 /\ ___patmp2^0-___patmp2^post0 == 0 /\ y_23^0-y_23^post0 == 0 /\ -k_139^post0+k_139^0 == 0 /\ lt_24^0-lt_24^post0 == 0), cost: 1
New rule:
l0 -> l2 : lt_34^0'=lt_34^post0, y_20^0'=w_17^0, lt_32^0'=lt_32^post0, Result_4^0'=Result_4^post0, x_19^0'=lt_32^10, (-x_13^0+y_12^0 == 0 /\ -1+k_243^0 >= 0 /\ len_263^0 >= 0), cost: 1

Applied preprocessing
Original rule:
l2 -> l3 : a_11^0'=a_11^post1, lt_34^0'=lt_34^post1, lt_24^0'=lt_24^post1, y_20^0'=y_20^post1, x_13^0'=x_13^post1, ___cil_tmp5_10^0'=___cil_tmp5_10^post1, lt_26^0'=lt_26^post1, k_289^0'=k_289^post1, t_18^0'=t_18^post1, lt_36^0'=lt_36^post1, x_22^0'=x_22^post1, k_187^0'=k_187^post1, ___patmp2^0'=___patmp2^post1, lt_32^0'=lt_32^post1, len_99^0'=len_99^post1, w_17^0'=w_17^post1, lt_38^0'=lt_38^post1, Result_4^0'=Result_4^post1, y_12^0'=y_12^post1, k_243^0'=k_243^post1, k_139^0'=k_139^post1, lt_35^0'=lt_35^post1, lt_25^0'=lt_25^post1, y_23^0'=y_23^post1, x_19^0'=x_19^post1, ___patmp1^0'=___patmp1^post1, lt_27^0'=lt_27^post1, len_263^0'=len_263^post1, tmp_9^0'=tmp_9^post1, lt_37^0'=lt_37^post1, x_8^0'=x_8^post1, k_208^0'=k_208^post1, (-x_19^post1+x_19^0 == 0 /\ -len_263^post1+len_263^0 == 0 /\ a_11^0-a_11^post1 == 0 /\ -k_208^post1+k_208^0 == 0 /\ k_243^0-k_243^post1 == 0 /\ lt_32^0-lt_32^post1 == 0 /\ -x_8^post1+x_8^0 == 0 /\ -y_23^post1+y_23^0 == 0 /\ lt_24^0-lt_24^post1 == 0 /\ -k_187^post1+k_187^0 == 0 /\ y_20^0-y_20^post1 == 0 /\ lt_36^0-lt_36^post1 == 0 /\ -lt_27^post1+lt_27^0 == 0 /\ -___patmp2^post1+___patmp2^0 == 0 /\ x_13^0-x_13^post1 == 0 /\ -k_139^post1+k_139^0 == 0 /\ lt_26^0-lt_26^post1 == 0 /\ len_99^0-len_99^post1 == 0 /\ lt_34^0-lt_34^post1 == 0 /\ x_22^0-x_22^post1 == 0 /\ lt_25^0-lt_25^post1 == 0 /\ -___patmp1^post1+___patmp1^0 == 0 /\ -tmp_9^post1+tmp_9^0 == 0 /\ -y_12^post1+y_12^0 == 0 /\ -___cil_tmp5_10^post1+___cil_tmp5_10^0 == 0 /\ -t_18^post1+t_18^0 == 0 /\ -Result_4^post1+Result_4^0 == 0 /\ k_289^0-k_289^post1 == 0 /\ lt_38^0-lt_38^post1 == 0 /\ -lt_35^post1+lt_35^0 == 0 /\ 1+w_17^0-x_19^0 <= 0 /\ -w_17^post1+w_17^0 == 0 /\ -lt_37^post1+lt_37^0 == 0), cost: 1
New rule:
l2 -> l3 : 1+w_17^0-x_19^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l2 -> l3 : a_11^0'=a_11^post2, lt_34^0'=lt_34^post2, lt_24^0'=lt_24^post2, y_20^0'=y_20^post2, x_13^0'=x_13^post2, ___cil_tmp5_10^0'=___cil_tmp5_10^post2, lt_26^0'=lt_26^post2, k_289^0'=k_289^post2, t_18^0'=t_18^post2, lt_36^0'=lt_36^post2, x_22^0'=x_22^post2, k_187^0'=k_187^post2, ___patmp2^0'=___patmp2^post2, lt_32^0'=lt_32^post2, len_99^0'=len_99^post2, w_17^0'=w_17^post2, lt_38^0'=lt_38^post2, Result_4^0'=Result_4^post2, y_12^0'=y_12^post2, k_243^0'=k_243^post2, k_139^0'=k_139^post2, lt_35^0'=lt_35^post2, lt_25^0'=lt_25^post2, y_23^0'=y_23^post2, x_19^0'=x_19^post2, ___patmp1^0'=___patmp1^post2, lt_27^0'=lt_27^post2, len_263^0'=len_263^post2, tmp_9^0'=tmp_9^post2, lt_37^0'=lt_37^post2, x_8^0'=x_8^post2, k_208^0'=k_208^post2, (k_289^0-k_289^post2 == 0 /\ -y_12^post2+y_12^0 == 0 /\ -___patmp2^post2+___patmp2^0 == 0 /\ lt_36^0-lt_36^post2 == 0 /\ -k_139^post2+k_139^0 == 0 /\ -tmp_9^post2+tmp_9^0 == 0 /\ -lt_35^post2+lt_35^0 == 0 /\ k_243^0-k_243^post2 == 0 /\ -t_18^post2+t_18^0 == 0 /\ lt_24^0-lt_24^post2 == 0 /\ Result_4^0-Result_4^post2 == 0 /\ -lt_37^post2+lt_37^0 == 0 /\ lt_32^0-lt_32^post2 == 0 /\ -len_263^post2+len_263^0 == 0 /\ -w_17^post2+w_17^0 == 0 /\ -x_8^post2+x_8^0 == 0 /\ -k_208^post2+k_208^0 == 0 /\ lt_38^0-lt_38^post2 == 0 /\ y_20^0-y_20^post2 == 0 /\ -lt_27^post2+lt_27^0 == 0 /\ 1-w_17^0+x_19^0 <= 0 /\ x_22^0-x_22^post2 == 0 /\ x_13^0-x_13^post2 == 0 /\ -y_23^post2+y_23^0 == 0 /\ ___cil_tmp5_10^0-___cil_tmp5_10^post2 == 0 /\ lt_26^0-lt_26^post2 == 0 /\ -lt_34^post2+lt_34^0 == 0 /\ lt_25^0-lt_25^post2 == 0 /\ a_11^0-a_11^post2 == 0 /\ len_99^0-len_99^post2 == 0 /\ -___patmp1^post2+___patmp1^0 == 0 /\ k_187^0-k_187^post2 == 0 /\ -x_19^post2+x_19^0 == 0), cost: 1
New rule:
l2 -> l3 : 1-w_17^0+x_19^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l3 -> l4 : a_11^0'=a_11^post3, lt_34^0'=lt_34^post3, lt_24^0'=lt_24^post3, y_20^0'=y_20^post3, x_13^0'=x_13^post3, ___cil_tmp5_10^0'=___cil_tmp5_10^post3, lt_26^0'=lt_26^post3, k_289^0'=k_289^post3, t_18^0'=t_18^post3, lt_36^0'=lt_36^post3, x_22^0'=x_22^post3, k_187^0'=k_187^post3, ___patmp2^0'=___patmp2^post3, lt_32^0'=lt_32^post3, len_99^0'=len_99^post3, w_17^0'=w_17^post3, lt_38^0'=lt_38^post3, Result_4^0'=Result_4^post3, y_12^0'=y_12^post3, k_243^0'=k_243^post3, k_139^0'=k_139^post3, lt_35^0'=lt_35^post3, lt_25^0'=lt_25^post3, y_23^0'=y_23^post3, x_19^0'=x_19^post3, ___patmp1^0'=___patmp1^post3, lt_27^0'=lt_27^post3, len_263^0'=len_263^post3, tmp_9^0'=tmp_9^post3, lt_37^0'=lt_37^post3, x_8^0'=x_8^post3, k_208^0'=k_208^post3, (-y_23^post3+y_23^0 == 0 /\ -lt_37^post3+lt_37^0 == 0 /\ Result_4^0-Result_4^post3 == 0 /\ -lt_38^post3+lt_38^0 == 0 /\ len_263^0-len_263^post3 == 0 /\ -lt_25^post3+lt_25^0 == 0 /\ -lt_27^post3+lt_27^0 == 0 /\ -___patmp1^post3+___patmp1^0 == 0 /\ k_289^0-k_289^post3 == 0 /\ lt_24^0-lt_24^post3 == 0 /\ -x_8^post3+x_8^0 == 0 /\ -w_17^post3+w_17^0 == 0 /\ k_243^0-k_243^post3 == 0 /\ -lt_36^post3+lt_36^0 == 0 /\ -k_208^post3+k_208^0 == 0 /\ -___patmp2^post3+___patmp2^0 == 0 /\ -y_12^post3+y_12^0 == 0 /\ x_19^0-x_19^post3 == 0 /\ lt_32^0-lt_32^post3 == 0 /\ -k_139^post3+k_139^0 == 0 /\ x_13^0-x_13^post3 == 0 /\ k_187^0-k_187^post3 == 0 /\ ___cil_tmp5_10^0-___cil_tmp5_10^post3 == 0 /\ -tmp_9^post3+tmp_9^0 == 0 /\ lt_26^0-lt_26^post3 == 0 /\ y_20^post3-t_18^post3 == 0 /\ -lt_34^post3+lt_34^0 == 0 /\ a_11^0-a_11^post3 == 0 /\ len_99^0-len_99^post3 == 0 /\ -x_19^0+t_18^post3 == 0 /\ x_22^0-x_22^post3 == 0 /\ -lt_35^post3+lt_35^0 == 0), cost: 1
New rule:
l3 -> l4 : y_20^0'=x_19^0, t_18^0'=x_19^0, TRUE, cost: 1

Applied preprocessing
Original rule:
l4 -> l5 : a_11^0'=a_11^post4, lt_34^0'=lt_34^post4, lt_24^0'=lt_24^post4, y_20^0'=y_20^post4, x_13^0'=x_13^post4, ___cil_tmp5_10^0'=___cil_tmp5_10^post4, lt_26^0'=lt_26^post4, k_289^0'=k_289^post4, t_18^0'=t_18^post4, lt_36^0'=lt_36^post4, x_22^0'=x_22^post4, k_187^0'=k_187^post4, ___patmp2^0'=___patmp2^post4, lt_32^0'=lt_32^post4, len_99^0'=len_99^post4, w_17^0'=w_17^post4, lt_38^0'=lt_38^post4, Result_4^0'=Result_4^post4, y_12^0'=y_12^post4, k_243^0'=k_243^post4, k_139^0'=k_139^post4, lt_35^0'=lt_35^post4, lt_25^0'=lt_25^post4, y_23^0'=y_23^post4, x_19^0'=x_19^post4, ___patmp1^0'=___patmp1^post4, lt_27^0'=lt_27^post4, len_263^0'=len_263^post4, tmp_9^0'=tmp_9^post4, lt_37^0'=lt_37^post4, x_8^0'=x_8^post4, k_208^0'=k_208^post4, (-y_23^post4+y_23^0 == 0 /\ -lt_37^post4+lt_37^0 == 0 /\ -lt_26^post4+lt_26^0 == 0 /\ -lt_27^post4+lt_27^0 == 0 /\ -lt_38^post4+lt_38^0 == 0 /\ len_263^0-len_263^post4 == 0 /\ lt_34^0-lt_34^post4 == 0 /\ Result_4^0-Result_4^post4 == 0 /\ -lt_25^post4+lt_25^0 == 0 /\ -___patmp1^post4+___patmp1^0 == 0 /\ k_289^0-k_289^post4 == 0 /\ t_18^0-t_18^post4 == 0 /\ -x_8^post4+x_8^0 == 0 /\ -k_208^post4+k_208^0 == 0 /\ -y_12^post4+y_12^0 == 0 /\ -w_17^post4+w_17^0 == 0 /\ k_243^0-k_243^post4 == 0 /\ -lt_36^post4+lt_36^0 == 0 /\ ___cil_tmp5_10^0-___cil_tmp5_10^post4 == 0 /\ -___patmp2^post4+___patmp2^0 == 0 /\ x_19^0-x_19^post4 == 0 /\ lt_24^0-lt_24^post4 == 0 /\ -k_139^post4+k_139^0 == 0 /\ lt_32^0-lt_32^post4 == 0 /\ k_187^0-k_187^post4 == 0 /\ -lt_35^post4+lt_35^0 == 0 /\ -tmp_9^post4+tmp_9^0 == 0 /\ y_20^0-y_20^post4 == 0 /\ x_22^0-x_22^post4 == 0 /\ x_13^0-x_13^post4 == 0 /\ a_11^0-a_11^post4 == 0 /\ len_99^0-len_99^post4 == 0 /\ 1+w_17^0-x_19^0 <= 0), cost: 1
New rule:
l4 -> l5 : 1+w_17^0-x_19^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l4 -> l5 : a_11^0'=a_11^post5, lt_34^0'=lt_34^post5, lt_24^0'=lt_24^post5, y_20^0'=y_20^post5, x_13^0'=x_13^post5, ___cil_tmp5_10^0'=___cil_tmp5_10^post5, lt_26^0'=lt_26^post5, k_289^0'=k_289^post5, t_18^0'=t_18^post5, lt_36^0'=lt_36^post5, x_22^0'=x_22^post5, k_187^0'=k_187^post5, ___patmp2^0'=___patmp2^post5, lt_32^0'=lt_32^post5, len_99^0'=len_99^post5, w_17^0'=w_17^post5, lt_38^0'=lt_38^post5, Result_4^0'=Result_4^post5, y_12^0'=y_12^post5, k_243^0'=k_243^post5, k_139^0'=k_139^post5, lt_35^0'=lt_35^post5, lt_25^0'=lt_25^post5, y_23^0'=y_23^post5, x_19^0'=x_19^post5, ___patmp1^0'=___patmp1^post5, lt_27^0'=lt_27^post5, len_263^0'=len_263^post5, tmp_9^0'=tmp_9^post5, lt_37^0'=lt_37^post5, x_8^0'=x_8^post5, k_208^0'=k_208^post5, (t_18^0-t_18^post5 == 0 /\ -___patmp2^post5+___patmp2^0 == 0 /\ x_13^0-x_13^post5 == 0 /\ y_12^0-y_12^post5 == 0 /\ len_99^0-len_99^post5 == 0 /\ x_22^0-x_22^post5 == 0 /\ -lt_36^post5+lt_36^0 == 0 /\ -tmp_9^post5+tmp_9^0 == 0 /\ -lt_38^post5+lt_38^0 == 0 /\ lt_34^0-lt_34^post5 == 0 /\ w_17^0-w_17^post5 == 0 /\ -len_263^post5+len_263^0 == 0 /\ -lt_35^post5+lt_35^0 == 0 /\ k_187^0-k_187^post5 == 0 /\ -lt_32^post5+lt_32^0 == 0 /\ -lt_37^post5+lt_37^0 == 0 /\ -lt_25^post5+lt_25^0 == 0 /\ -k_243^post5+k_243^0 == 0 /\ lt_24^0-lt_24^post5 == 0 /\ -y_23^post5+y_23^0 == 0 /\ k_289^0-k_289^post5 == 0 /\ 1-w_17^0+x_19^0 <= 0 /\ a_11^0-a_11^post5 == 0 /\ ___cil_tmp5_10^0-___cil_tmp5_10^post5 == 0 /\ -lt_27^post5+lt_27^0 == 0 /\ x_19^0-x_19^post5 == 0 /\ k_139^0-k_139^post5 == 0 /\ Result_4^0-Result_4^post5 == 0 /\ -lt_26^post5+lt_26^0 == 0 /\ -k_208^post5+k_208^0 == 0 /\ -___patmp1^post5+___patmp1^0 == 0 /\ -x_8^post5+x_8^0 == 0 /\ -y_20^post5+y_20^0 == 0), cost: 1
New rule:
l4 -> l5 : 1-w_17^0+x_19^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l5 -> l1 : a_11^0'=a_11^post6, lt_34^0'=lt_34^post6, lt_24^0'=lt_24^post6, y_20^0'=y_20^post6, x_13^0'=x_13^post6, ___cil_tmp5_10^0'=___cil_tmp5_10^post6, lt_26^0'=lt_26^post6, k_289^0'=k_289^post6, t_18^0'=t_18^post6, lt_36^0'=lt_36^post6, x_22^0'=x_22^post6, k_187^0'=k_187^post6, ___patmp2^0'=___patmp2^post6, lt_32^0'=lt_32^post6, len_99^0'=len_99^post6, w_17^0'=w_17^post6, lt_38^0'=lt_38^post6, Result_4^0'=Result_4^post6, y_12^0'=y_12^post6, k_243^0'=k_243^post6, k_139^0'=k_139^post6, lt_35^0'=lt_35^post6, lt_25^0'=lt_25^post6, y_23^0'=y_23^post6, x_19^0'=x_19^post6, ___patmp1^0'=___patmp1^post6, lt_27^0'=lt_27^post6, len_263^0'=len_263^post6, tmp_9^0'=tmp_9^post6, lt_37^0'=lt_37^post6, x_8^0'=x_8^post6, k_208^0'=k_208^post6, (-lt_27^post6+lt_27^0 == 0 /\ -lt_25^post6+lt_25^0 == 0 /\ y_12^0-y_12^post6 == 0 /\ k_187^0-k_187^post6 == 0 /\ -lt_37^post6+lt_37^0 == 0 /\ w_17^0-w_17^post6 == 0 /\ -x_22^post6+x_22^0 == 0 /\ t_18^post6-x_19^0 == 0 /\ lt_36^0-lt_36^post6 == 0 /\ -x_19^post6+x_19^0 == 0 /\ x_13^0-x_13^post6 == 0 /\ -k_208^post6+k_208^0 == 0 /\ -y_23^post6+y_23^0 == 0 /\ a_11^0-a_11^post6 == 0 /\ -x_8^post6+x_8^0 == 0 /\ len_99^0-len_99^post6 == 0 /\ ___cil_tmp5_10^0-___cil_tmp5_10^post6 == 0 /\ -___patmp1^post6+___patmp1^0 == 0 /\ k_139^0-k_139^post6 == 0 /\ Result_4^0-Result_4^post6 == 0 /\ lt_34^0-lt_34^post6 == 0 /\ -t_18^post6+y_20^post6 == 0 /\ lt_26^0-lt_26^post6 == 0 /\ -lt_32^post6+lt_32^0 == 0 /\ -len_263^post6+len_263^0 == 0 /\ k_289^0-k_289^post6 == 0 /\ -lt_38^post6+lt_38^0 == 0 /\ -lt_35^post6+lt_35^0 == 0 /\ -lt_24^post6+lt_24^0 == 0 /\ ___patmp2^0-___patmp2^post6 == 0 /\ -k_243^post6+k_243^0 == 0 /\ tmp_9^0-tmp_9^post6 == 0), cost: 1
New rule:
l5 -> l1 : y_20^0'=x_19^0, t_18^0'=x_19^0, TRUE, cost: 1

Applied preprocessing
Original rule:
l0 -> l7 : a_11^0'=a_11^post7, lt_34^0'=lt_34^post7, lt_24^0'=lt_24^post7, y_20^0'=y_20^post7, x_13^0'=x_13^post7, ___cil_tmp5_10^0'=___cil_tmp5_10^post7, lt_26^0'=lt_26^post7, k_289^0'=k_289^post7, t_18^0'=t_18^post7, lt_36^0'=lt_36^post7, x_22^0'=x_22^post7, k_187^0'=k_187^post7, ___patmp2^0'=___patmp2^post7, lt_32^0'=lt_32^post7, len_99^0'=len_99^post7, w_17^0'=w_17^post7, lt_38^0'=lt_38^post7, Result_4^0'=Result_4^post7, y_12^0'=y_12^post7, k_243^0'=k_243^post7, k_139^0'=k_139^post7, lt_35^0'=lt_35^post7, lt_25^0'=lt_25^post7, y_23^0'=y_23^post7, x_19^0'=x_19^post7, ___patmp1^0'=___patmp1^post7, lt_27^0'=lt_27^post7, len_263^0'=len_263^post7, tmp_9^0'=tmp_9^post7, lt_37^0'=lt_37^post7, x_8^0'=x_8^post7, k_208^0'=k_208^post7, (-Result_4^post7+Result_4^0 == 0 /\ lt_26^0-lt_26^post7 == 0 /\ lt_34^0-lt_34^post7 == 0 /\ -len_263^post7+len_263^0 == 0 /\ lt_24^0-lt_24^post7 == 0 /\ -lt_38^post7+lt_38^0 == 0 /\ y_12^0-y_12^post7 == 0 /\ -lt_32^post7+lt_32^0 == 0 /\ -len_263^0 <= 0 /\ lt_36^0-lt_36^post7 == 0 /\ -tmp_9^post7+tmp_9^0 == 0 /\ -k_243^post7+k_243^0 == 0 /\ y_20^0-y_20^post7 == 0 /\ ___patmp1^0-___patmp1^post7 == 0 /\ k_139^0-k_139^post7 == 0 /\ -len_99^post7+len_99^0 == 0 /\ -x_13^post7+x_13^0 == 0 /\ -lt_27^post7+lt_27^0 == 0 /\ -lt_35^post7+lt_35^0 == 0 /\ 1+k_289^post7-k_243^0 == 0 /\ t_18^0-t_18^post7 == 0 /\ -k_208^post7+k_208^0 == 0 /\ -lt_37^post7+lt_37^0 == 0 /\ ___patmp2^0-___patmp2^post7 == 0 /\ -x_19^post7+x_19^0 == 0 /\ 1-k_243^0 <= 0 /\ -x_22^post7+x_22^0 == 0 /\ -x_8^post7+x_8^0 == 0 /\ ___cil_tmp5_10^0-___cil_tmp5_10^post7 == 0 /\ -lt_25^post7+lt_25^0 == 0 /\ w_17^0-w_17^post7 == 0 /\ k_187^0-k_187^post7 == 0 /\ -y_23^post7+y_23^0 == 0 /\ a_11^0-a_11^post7 == 0), cost: 1
New rule:
l0 -> l7 : k_289^0'=-1+k_243^0, (-1+k_243^0 >= 0 /\ len_263^0 >= 0), cost: 1

Applied preprocessing
Original rule:
l7 -> l8 : a_11^0'=a_11^post8, lt_34^0'=lt_34^post8, lt_24^0'=lt_24^post8, y_20^0'=y_20^post8, x_13^0'=x_13^post8, ___cil_tmp5_10^0'=___cil_tmp5_10^post8, lt_26^0'=lt_26^post8, k_289^0'=k_289^post8, t_18^0'=t_18^post8, lt_36^0'=lt_36^post8, x_22^0'=x_22^post8, k_187^0'=k_187^post8, ___patmp2^0'=___patmp2^post8, lt_32^0'=lt_32^post8, len_99^0'=len_99^post8, w_17^0'=w_17^post8, lt_38^0'=lt_38^post8, Result_4^0'=Result_4^post8, y_12^0'=y_12^post8, k_243^0'=k_243^post8, k_139^0'=k_139^post8, lt_35^0'=lt_35^post8, lt_25^0'=lt_25^post8, y_23^0'=y_23^post8, x_19^0'=x_19^post8, ___patmp1^0'=___patmp1^post8, lt_27^0'=lt_27^post8, len_263^0'=len_263^post8, tmp_9^0'=tmp_9^post8, lt_37^0'=lt_37^post8, x_8^0'=x_8^post8, k_208^0'=k_208^post8, (lt_34^0-lt_34^post8 == 0 /\ x_22^0-x_22^post8 == 0 /\ ___patmp2^0-___patmp2^post8 == 0 /\ -k_187^post8+k_187^0 == 0 /\ -x_19^post8+x_19^0 == 0 /\ -len_263^post8+len_263^0 == 0 /\ t_18^0-t_18^post8 == 0 /\ -k_208^post8+k_208^0 == 0 /\ -Result_4^post8+Result_4^0 == 0 /\ -x_8^post8+x_8^0 == 0 /\ -k_243^post8+k_243^0 == 0 /\ lt_26^0-lt_26^post8 == 0 /\ -k_139^post8+k_139^0 == 0 /\ -lt_27^post8+lt_27^0 == 0 /\ lt_38^0-lt_38^post8 == 0 /\ 1-x_13^0+y_12^0 <= 0 /\ w_17^0-w_17^post8 == 0 /\ a_11^0-a_11^post8 == 0 /\ lt_32^0-lt_32^post8 == 0 /\ -___patmp1^post8+___patmp1^0 == 0 /\ -tmp_9^post8+tmp_9^0 == 0 /\ -k_289^post8+k_289^0 == 0 /\ lt_35^0-lt_35^post8 == 0 /\ ___cil_tmp5_10^0-___cil_tmp5_10^post8 == 0 /\ lt_24^0-lt_24^post8 == 0 /\ y_20^0-y_20^post8 == 0 /\ lt_37^0-lt_37^post8 == 0 /\ -lt_25^post8+lt_25^0 == 0 /\ -y_12^post8+y_12^0 == 0 /\ lt_36^0-lt_36^post8 == 0 /\ y_23^0-y_23^post8 == 0 /\ -len_99^post8+len_99^0 == 0 /\ -x_13^post8+x_13^0 == 0), cost: 1
New rule:
l7 -> l8 : 1-x_13^0+y_12^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l7 -> l8 : a_11^0'=a_11^post9, lt_34^0'=lt_34^post9, lt_24^0'=lt_24^post9, y_20^0'=y_20^post9, x_13^0'=x_13^post9, ___cil_tmp5_10^0'=___cil_tmp5_10^post9, lt_26^0'=lt_26^post9, k_289^0'=k_289^post9, t_18^0'=t_18^post9, lt_36^0'=lt_36^post9, x_22^0'=x_22^post9, k_187^0'=k_187^post9, ___patmp2^0'=___patmp2^post9, lt_32^0'=lt_32^post9, len_99^0'=len_99^post9, w_17^0'=w_17^post9, lt_38^0'=lt_38^post9, Result_4^0'=Result_4^post9, y_12^0'=y_12^post9, k_243^0'=k_243^post9, k_139^0'=k_139^post9, lt_35^0'=lt_35^post9, lt_25^0'=lt_25^post9, y_23^0'=y_23^post9, x_19^0'=x_19^post9, ___patmp1^0'=___patmp1^post9, lt_27^0'=lt_27^post9, len_263^0'=len_263^post9, tmp_9^0'=tmp_9^post9, lt_37^0'=lt_37^post9, x_8^0'=x_8^post9, k_208^0'=k_208^post9, (lt_38^0-lt_38^post9 == 0 /\ lt_27^0-lt_27^post9 == 0 /\ y_20^0-y_20^post9 == 0 /\ -tmp_9^post9+tmp_9^0 == 0 /\ y_23^0-y_23^post9 == 0 /\ -y_12^post9+y_12^0 == 0 /\ -lt_35^post9+lt_35^0 == 0 /\ -___patmp1^post9+___patmp1^0 == 0 /\ x_13^0-x_13^post9 == 0 /\ -lt_37^post9+lt_37^0 == 0 /\ a_11^0-a_11^post9 == 0 /\ lt_34^0-lt_34^post9 == 0 /\ ___cil_tmp5_10^0-___cil_tmp5_10^post9 == 0 /\ lt_26^0-lt_26^post9 == 0 /\ x_22^0-x_22^post9 == 0 /\ -Result_4^post9+Result_4^0 == 0 /\ -w_17^post9+w_17^0 == 0 /\ -len_99^post9+len_99^0 == 0 /\ -x_19^post9+x_19^0 == 0 /\ -len_263^post9+len_263^0 == 0 /\ -x_8^post9+x_8^0 == 0 /\ -k_208^post9+k_208^0 == 0 /\ lt_36^0-lt_36^post9 == 0 /\ -k_187^post9+k_187^0 == 0 /\ lt_25^0-lt_25^post9 == 0 /\ k_289^0-k_289^post9 == 0 /\ -t_18^post9+t_18^0 == 0 /\ 1+x_13^0-y_12^0 <= 0 /\ -k_243^post9+k_243^0 == 0 /\ ___patmp2^0-___patmp2^post9 == 0 /\ lt_32^0-lt_32^post9 == 0 /\ lt_24^0-lt_24^post9 == 0 /\ -k_139^post9+k_139^0 == 0), cost: 1
New rule:
l7 -> l8 : 1+x_13^0-y_12^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l8 -> l6 : a_11^0'=a_11^post10, lt_34^0'=lt_34^post10, lt_24^0'=lt_24^post10, y_20^0'=y_20^post10, x_13^0'=x_13^post10, ___cil_tmp5_10^0'=___cil_tmp5_10^post10, lt_26^0'=lt_26^post10, k_289^0'=k_289^post10, t_18^0'=t_18^post10, lt_36^0'=lt_36^post10, x_22^0'=x_22^post10, k_187^0'=k_187^post10, ___patmp2^0'=___patmp2^post10, lt_32^0'=lt_32^post10, len_99^0'=len_99^post10, w_17^0'=w_17^post10, lt_38^0'=lt_38^post10, Result_4^0'=Result_4^post10, y_12^0'=y_12^post10, k_243^0'=k_243^post10, k_139^0'=k_139^post10, lt_35^0'=lt_35^post10, lt_25^0'=lt_25^post10, y_23^0'=y_23^post10, x_19^0'=x_19^post10, ___patmp1^0'=___patmp1^post10, lt_27^0'=lt_27^post10, len_263^0'=len_263^post10, tmp_9^0'=tmp_9^post10, lt_37^0'=lt_37^post10, x_8^0'=x_8^post10, k_208^0'=k_208^post10, (0 == 0 /\ -lt_27^post10+lt_27^0 == 0 /\ x_22^0-x_22^post10 == 0 /\ t_18^0-t_18^post10 == 0 /\ -k_187^post10+k_187^0 == 0 /\ -lt_32^post10+lt_32^0 == 0 /\ -k_289^0+___patmp2^post10 == 0 /\ lt_38^0-lt_38^post10 == 0 /\ k_243^post10-___patmp2^post10 == 0 /\ -x_19^post10+x_19^0 == 0 /\ -k_208^post10+k_208^0 == 0 /\ -len_99^post10+len_99^0 == 0 /\ -tmp_9^post10+tmp_9^0 == 0 /\ y_20^0-y_20^post10 == 0 /\ -len_263^0 <= 0 /\ a_11^0-a_11^post10 == 0 /\ -k_139^post10+k_139^0 == 0 /\ -k_289^post10+k_289^0 == 0 /\ x_13^post10-lt_24^10 == 0 /\ -k_289^0 <= 0 /\ -y_12^post10+y_12^0 == 0 /\ -lt_37^post10+lt_37^0 == 0 /\ w_17^0-w_17^post10 == 0 /\ -1+___patmp1^post10-len_263^0 == 0 /\ ___cil_tmp5_10^0-___cil_tmp5_10^post10 == 0 /\ -x_8^post10+x_8^0 == 0 /\ lt_26^0-lt_26^post10 == 0 /\ -Result_4^post10+Result_4^0 == 0 /\ y_23^0-y_23^post10 == 0 /\ lt_36^0-lt_36^post10 == 0 /\ -lt_34^post10+lt_34^0 == 0 /\ -___patmp1^post10+len_263^post10 == 0 /\ -lt_35^post10+lt_35^0 == 0), cost: 1
New rule:
l8 -> l6 : lt_24^0'=lt_24^post10, x_13^0'=lt_24^10, ___patmp2^0'=k_289^0, k_243^0'=k_289^0, lt_25^0'=lt_25^post10, ___patmp1^0'=1+len_263^0, len_263^0'=1+len_263^0, (k_289^0 >= 0 /\ len_263^0 >= 0), cost: 1

Applied preprocessing
Original rule:
l6 -> l0 : a_11^0'=a_11^post11, lt_34^0'=lt_34^post11, lt_24^0'=lt_24^post11, y_20^0'=y_20^post11, x_13^0'=x_13^post11, ___cil_tmp5_10^0'=___cil_tmp5_10^post11, lt_26^0'=lt_26^post11, k_289^0'=k_289^post11, t_18^0'=t_18^post11, lt_36^0'=lt_36^post11, x_22^0'=x_22^post11, k_187^0'=k_187^post11, ___patmp2^0'=___patmp2^post11, lt_32^0'=lt_32^post11, len_99^0'=len_99^post11, w_17^0'=w_17^post11, lt_38^0'=lt_38^post11, Result_4^0'=Result_4^post11, y_12^0'=y_12^post11, k_243^0'=k_243^post11, k_139^0'=k_139^post11, lt_35^0'=lt_35^post11, lt_25^0'=lt_25^post11, y_23^0'=y_23^post11, x_19^0'=x_19^post11, ___patmp1^0'=___patmp1^post11, lt_27^0'=lt_27^post11, len_263^0'=len_263^post11, tmp_9^0'=tmp_9^post11, lt_37^0'=lt_37^post11, x_8^0'=x_8^post11, k_208^0'=k_208^post11, (-len_263^post11+len_263^0 == 0 /\ -lt_38^post11+lt_38^0 == 0 /\ lt_26^0-lt_26^post11 == 0 /\ t_18^0-t_18^post11 == 0 /\ -x_8^post11+x_8^0 == 0 /\ -y_23^post11+y_23^0 == 0 /\ Result_4^0-Result_4^post11 == 0 /\ lt_32^0-lt_32^post11 == 0 /\ -lt_27^post11+lt_27^0 == 0 /\ -w_17^post11+w_17^0 == 0 /\ k_289^0-k_289^post11 == 0 /\ lt_24^0-lt_24^post11 == 0 /\ k_243^0-k_243^post11 == 0 /\ -tmp_9^post11+tmp_9^0 == 0 /\ -lt_35^post11+lt_35^0 == 0 /\ -y_20^post11+y_20^0 == 0 /\ -y_12^post11+y_12^0 == 0 /\ x_19^0-x_19^post11 == 0 /\ -k_208^post11+k_208^0 == 0 /\ x_13^0-x_13^post11 == 0 /\ -___patmp1^post11+___patmp1^0 == 0 /\ a_11^0-a_11^post11 == 0 /\ -___patmp2^post11+___patmp2^0 == 0 /\ -lt_37^post11+lt_37^0 == 0 /\ len_99^0-len_99^post11 == 0 /\ ___cil_tmp5_10^0-___cil_tmp5_10^post11 == 0 /\ k_187^0-k_187^post11 == 0 /\ x_22^0-x_22^post11 == 0 /\ -lt_25^post11+lt_25^0 == 0 /\ k_139^0-k_139^post11 == 0 /\ -lt_36^post11+lt_36^0 == 0 /\ -lt_34^post11+lt_34^0 == 0), cost: 1
New rule:
l6 -> l0 : TRUE, cost: 1

Applied preprocessing
Original rule:
l9 -> l10 : a_11^0'=a_11^post12, lt_34^0'=lt_34^post12, lt_24^0'=lt_24^post12, y_20^0'=y_20^post12, x_13^0'=x_13^post12, ___cil_tmp5_10^0'=___cil_tmp5_10^post12, lt_26^0'=lt_26^post12, k_289^0'=k_289^post12, t_18^0'=t_18^post12, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=k_187^post12, ___patmp2^0'=___patmp2^post12, lt_32^0'=lt_32^post12, len_99^0'=len_99^post12, w_17^0'=w_17^post12, lt_38^0'=lt_38^post12, Result_4^0'=Result_4^post12, y_12^0'=y_12^post12, k_243^0'=k_243^post12, k_139^0'=k_139^post12, lt_35^0'=lt_35^post12, lt_25^0'=lt_25^post12, y_23^0'=y_23^post12, x_19^0'=x_19^post12, ___patmp1^0'=___patmp1^post12, lt_27^0'=lt_27^post12, len_263^0'=len_263^post12, tmp_9^0'=tmp_9^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=k_208^post12, (0 == 0 /\ -lt_27^post12+lt_27^0 == 0 /\ x_8^10-tmp_9^10 == 0 /\ t_18^0-t_18^post12 == 0 /\ y_23^post12 == 0 /\ -len_99^post12 <= 0 /\ -tmp_9^post12+x_8^post12 == 0 /\ -1+k_139^post12-len_99^post12 == 0 /\ a_11^0-a_11^post12 == 0 /\ -x_8^30+___cil_tmp5_10^30 == 0 /\ ___patmp2^0-___patmp2^post12 == 0 /\ -lt_25^post12+lt_25^0 == 0 /\ -k_187^post12+k_208^post12 == 0 /\ -x_8^20+___cil_tmp5_10^20 == 0 /\ Result_4^10-___cil_tmp5_10^10 == 0 /\ -1+k_187^post12-k_139^post12 == 0 /\ -lt_32^post12+lt_32^0 == 0 /\ -x_19^post12+x_19^0 == 0 /\ k_289^0-k_289^post12 == 0 /\ Result_4^20-___cil_tmp5_10^20 == 0 /\ -___cil_tmp5_10^post12+Result_4^post12 == 0 /\ -k_139^post12 <= 0 /\ lt_24^0-lt_24^post12 == 0 /\ -len_263^post12+len_263^0 == 0 /\ -x_8^10+___cil_tmp5_10^10 == 0 /\ Result_4^30-___cil_tmp5_10^30 == 0 /\ -___patmp1^post12+___patmp1^0 == 0 /\ -k_243^post12+k_243^0 == 0 /\ y_20^0-y_20^post12 == 0 /\ -tmp_9^20+x_8^20 == 0 /\ -w_17^post12+w_17^0 == 0 /\ lt_26^0-lt_26^post12 == 0 /\ -2+len_99^post12 == 0 /\ -k_187^post12 <= 0 /\ -y_12^post12+y_12^0 == 0 /\ -a_11^0+x_13^post12 == 0 /\ x_8^30-tmp_9^30 == 0 /\ ___cil_tmp5_10^post12-x_8^post12 == 0), cost: 1
New rule:
l9 -> l10 : lt_34^0'=lt_34^post12, x_13^0'=a_11^0, ___cil_tmp5_10^0'=x_8^post12, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=x_8^post12, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, (0 == 0 /\ -3 <= 0 /\ -2 <= 0 /\ -4 <= 0), cost: 1

Applied preprocessing
Original rule:
l10 -> l11 : a_11^0'=a_11^post13, lt_34^0'=lt_34^post13, lt_24^0'=lt_24^post13, y_20^0'=y_20^post13, x_13^0'=x_13^post13, ___cil_tmp5_10^0'=___cil_tmp5_10^post13, lt_26^0'=lt_26^post13, k_289^0'=k_289^post13, t_18^0'=t_18^post13, lt_36^0'=lt_36^post13, x_22^0'=x_22^post13, k_187^0'=k_187^post13, ___patmp2^0'=___patmp2^post13, lt_32^0'=lt_32^post13, len_99^0'=len_99^post13, w_17^0'=w_17^post13, lt_38^0'=lt_38^post13, Result_4^0'=Result_4^post13, y_12^0'=y_12^post13, k_243^0'=k_243^post13, k_139^0'=k_139^post13, lt_35^0'=lt_35^post13, lt_25^0'=lt_25^post13, y_23^0'=y_23^post13, x_19^0'=x_19^post13, ___patmp1^0'=___patmp1^post13, lt_27^0'=lt_27^post13, len_263^0'=len_263^post13, tmp_9^0'=tmp_9^post13, lt_37^0'=lt_37^post13, x_8^0'=x_8^post13, k_208^0'=k_208^post13, (k_187^0-k_187^post13 == 0 /\ ___patmp1^0-___patmp1^post13 == 0 /\ w_17^0-w_17^post13 == 0 /\ -len_263^post13+len_263^0 == 0 /\ -lt_25^post13+lt_25^0 == 0 /\ x_13^0-x_13^post13 == 0 /\ -k_208^post13+k_208^0 == 0 /\ -lt_36^post13+lt_36^0 == 0 /\ ___cil_tmp5_10^0-___cil_tmp5_10^post13 == 0 /\ -lt_27^post13+lt_27^0 == 0 /\ a_11^0-a_11^post13 == 0 /\ y_20^0-y_20^post13 == 0 /\ 1-x_13^0+y_12^0 <= 0 /\ y_12^0-y_12^post13 == 0 /\ -tmp_9^post13+tmp_9^0 == 0 /\ ___patmp2^0-___patmp2^post13 == 0 /\ -x_19^post13+x_19^0 == 0 /\ -x_22^post13+x_22^0 == 0 /\ y_23^0-y_23^post13 == 0 /\ -Result_4^post13+Result_4^0 == 0 /\ -lt_32^post13+lt_32^0 == 0 /\ lt_26^0-lt_26^post13 == 0 /\ k_289^0-k_289^post13 == 0 /\ lt_34^0-lt_34^post13 == 0 /\ -lt_24^post13+lt_24^0 == 0 /\ -x_8^post13+x_8^0 == 0 /\ -k_243^post13+k_243^0 == 0 /\ -lt_37^post13+lt_37^0 == 0 /\ -k_139^post13+k_139^0 == 0 /\ -lt_38^post13+lt_38^0 == 0 /\ lt_35^0-lt_35^post13 == 0 /\ t_18^0-t_18^post13 == 0 /\ -len_99^post13+len_99^0 == 0), cost: 1
New rule:
l10 -> l11 : 1-x_13^0+y_12^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l10 -> l11 : a_11^0'=a_11^post14, lt_34^0'=lt_34^post14, lt_24^0'=lt_24^post14, y_20^0'=y_20^post14, x_13^0'=x_13^post14, ___cil_tmp5_10^0'=___cil_tmp5_10^post14, lt_26^0'=lt_26^post14, k_289^0'=k_289^post14, t_18^0'=t_18^post14, lt_36^0'=lt_36^post14, x_22^0'=x_22^post14, k_187^0'=k_187^post14, ___patmp2^0'=___patmp2^post14, lt_32^0'=lt_32^post14, len_99^0'=len_99^post14, w_17^0'=w_17^post14, lt_38^0'=lt_38^post14, Result_4^0'=Result_4^post14, y_12^0'=y_12^post14, k_243^0'=k_243^post14, k_139^0'=k_139^post14, lt_35^0'=lt_35^post14, lt_25^0'=lt_25^post14, y_23^0'=y_23^post14, x_19^0'=x_19^post14, ___patmp1^0'=___patmp1^post14, lt_27^0'=lt_27^post14, len_263^0'=len_263^post14, tmp_9^0'=tmp_9^post14, lt_37^0'=lt_37^post14, x_8^0'=x_8^post14, k_208^0'=k_208^post14, (-k_139^post14+k_139^0 == 0 /\ lt_38^0-lt_38^post14 == 0 /\ -len_263^post14+len_263^0 == 0 /\ x_22^0-x_22^post14 == 0 /\ ___patmp2^0-___patmp2^post14 == 0 /\ lt_26^0-lt_26^post14 == 0 /\ -___patmp1^post14+___patmp1^0 == 0 /\ -k_187^post14+k_187^0 == 0 /\ -x_8^post14+x_8^0 == 0 /\ -y_12^post14+y_12^0 == 0 /\ -Result_4^post14+Result_4^0 == 0 /\ -lt_27^post14+lt_27^0 == 0 /\ lt_35^0-lt_35^post14 == 0 /\ lt_24^0-lt_24^post14 == 0 /\ lt_36^0-lt_36^post14 == 0 /\ -x_19^post14+x_19^0 == 0 /\ w_17^0-w_17^post14 == 0 /\ lt_32^0-lt_32^post14 == 0 /\ -tmp_9^post14+tmp_9^0 == 0 /\ -k_208^post14+k_208^0 == 0 /\ -lt_25^post14+lt_25^0 == 0 /\ -k_243^post14+k_243^0 == 0 /\ t_18^0-t_18^post14 == 0 /\ x_13^0-x_13^post14 == 0 /\ 1+x_13^0-y_12^0 <= 0 /\ lt_34^0-lt_34^post14 == 0 /\ lt_37^0-lt_37^post14 == 0 /\ a_11^0-a_11^post14 == 0 /\ y_20^0-y_20^post14 == 0 /\ ___cil_tmp5_10^0-___cil_tmp5_10^post14 == 0 /\ y_23^0-y_23^post14 == 0 /\ -len_99^post14+len_99^0 == 0 /\ k_289^0-k_289^post14 == 0), cost: 1
New rule:
l10 -> l11 : 1+x_13^0-y_12^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l11 -> l0 : a_11^0'=a_11^post15, lt_34^0'=lt_34^post15, lt_24^0'=lt_24^post15, y_20^0'=y_20^post15, x_13^0'=x_13^post15, ___cil_tmp5_10^0'=___cil_tmp5_10^post15, lt_26^0'=lt_26^post15, k_289^0'=k_289^post15, t_18^0'=t_18^post15, lt_36^0'=lt_36^post15, x_22^0'=x_22^post15, k_187^0'=k_187^post15, ___patmp2^0'=___patmp2^post15, lt_32^0'=lt_32^post15, len_99^0'=len_99^post15, w_17^0'=w_17^post15, lt_38^0'=lt_38^post15, Result_4^0'=Result_4^post15, y_12^0'=y_12^post15, k_243^0'=k_243^post15, k_139^0'=k_139^post15, lt_35^0'=lt_35^post15, lt_25^0'=lt_25^post15, y_23^0'=y_23^post15, x_19^0'=x_19^post15, ___patmp1^0'=___patmp1^post15, lt_27^0'=lt_27^post15, len_263^0'=len_263^post15, tmp_9^0'=tmp_9^post15, lt_37^0'=lt_37^post15, x_8^0'=x_8^post15, k_208^0'=k_208^post15, (0 == 0 /\ -k_289^post15+k_289^0 == 0 /\ y_12^0-y_12^post15 == 0 /\ -k_208^0 <= 0 /\ -x_8^post15+x_8^0 == 0 /\ len_99^0-len_99^post15 == 0 /\ -lt_36^post15+lt_36^0 == 0 /\ x_22^0-x_22^post15 == 0 /\ a_11^0-a_11^post15 == 0 /\ -lt_32^post15+lt_32^0 == 0 /\ lt_34^0-lt_34^post15 == 0 /\ y_20^0-y_20^post15 == 0 /\ ___patmp2^post15-k_208^0 == 0 /\ -tmp_9^post15+tmp_9^0 == 0 /\ -y_23^post15+y_23^0 == 0 /\ t_18^0-t_18^post15 == 0 /\ w_17^0-w_17^post15 == 0 /\ -lt_35^post15+lt_35^0 == 0 /\ k_187^0-k_187^post15 == 0 /\ Result_4^0-Result_4^post15 == 0 /\ -lt_25^post15+lt_25^0 == 0 /\ -1+___patmp1^post15 == 0 /\ -k_208^post15+k_208^0 == 0 /\ -lt_38^post15+lt_38^0 == 0 /\ k_139^0-k_139^post15 == 0 /\ x_19^0-x_19^post15 == 0 /\ -lt_37^post15+lt_37^0 == 0 /\ -___cil_tmp5_10^post15+___cil_tmp5_10^0 == 0 /\ -lt_26^10+x_13^post15 == 0 /\ -___patmp2^post15+k_243^post15 == 0 /\ -___patmp1^post15+len_263^post15 == 0 /\ lt_24^0-lt_24^post15 == 0), cost: 1
New rule:
l11 -> l0 : x_13^0'=lt_26^10, lt_26^0'=lt_26^post15, ___patmp2^0'=k_208^0, k_243^0'=k_208^0, ___patmp1^0'=1, lt_27^0'=lt_27^post15, len_263^0'=1, k_208^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l1 -> l13 : a_11^0'=a_11^post16, lt_34^0'=lt_34^post16, lt_24^0'=lt_24^post16, y_20^0'=y_20^post16, x_13^0'=x_13^post16, ___cil_tmp5_10^0'=___cil_tmp5_10^post16, lt_26^0'=lt_26^post16, k_289^0'=k_289^post16, t_18^0'=t_18^post16, lt_36^0'=lt_36^post16, x_22^0'=x_22^post16, k_187^0'=k_187^post16, ___patmp2^0'=___patmp2^post16, lt_32^0'=lt_32^post16, len_99^0'=len_99^post16, w_17^0'=w_17^post16, lt_38^0'=lt_38^post16, Result_4^0'=Result_4^post16, y_12^0'=y_12^post16, k_243^0'=k_243^post16, k_139^0'=k_139^post16, lt_35^0'=lt_35^post16, lt_25^0'=lt_25^post16, y_23^0'=y_23^post16, x_19^0'=x_19^post16, ___patmp1^0'=___patmp1^post16, lt_27^0'=lt_27^post16, len_263^0'=len_263^post16, tmp_9^0'=tmp_9^post16, lt_37^0'=lt_37^post16, x_8^0'=x_8^post16, k_208^0'=k_208^post16, (-k_139^post16+k_139^0 == 0 /\ k_289^0-k_289^post16 == 0 /\ a_11^0-a_11^post16 == 0 /\ len_263^0-len_263^post16 == 0 /\ -k_208^post16+k_208^0 == 0 /\ -lt_35^post16+lt_35^0 == 0 /\ -___patmp1^post16+___patmp1^0 == 0 /\ -tmp_9^post16+tmp_9^0 == 0 /\ lt_25^0-lt_25^post16 == 0 /\ lt_36^0-lt_36^post16 == 0 /\ -lt_38^post16+lt_38^0 == 0 /\ lt_24^0-lt_24^post16 == 0 /\ Result_4^0-Result_4^post16 == 0 /\ -y_23^post16+y_23^0 == 0 /\ k_243^0-k_243^post16 == 0 /\ lt_32^0-lt_32^post16 == 0 /\ -w_17^post16+w_17^0 == 0 /\ t_18^0-t_18^post16 == 0 /\ -lt_37^post16+lt_37^0 == 0 /\ -x_19^post16+x_19^0 == 0 /\ y_20^0-y_20^post16 == 0 /\ lt_34^0-lt_34^post16 == 0 /\ -x_8^post16+x_8^0 == 0 /\ -y_12^post16+y_12^0 == 0 /\ x_13^0-x_13^post16 == 0 /\ len_99^0-len_99^post16 == 0 /\ x_22^0-x_22^post16 == 0 /\ lt_26^0-lt_26^post16 == 0 /\ ___cil_tmp5_10^0-___cil_tmp5_10^post16 == 0 /\ -lt_27^post16+lt_27^0 == 0 /\ k_187^0-k_187^post16 == 0 /\ -___patmp2^post16+___patmp2^0 == 0 /\ 1+w_17^0-x_19^0 <= 0), cost: 1
New rule:
l1 -> l13 : 1+w_17^0-x_19^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l1 -> l13 : a_11^0'=a_11^post17, lt_34^0'=lt_34^post17, lt_24^0'=lt_24^post17, y_20^0'=y_20^post17, x_13^0'=x_13^post17, ___cil_tmp5_10^0'=___cil_tmp5_10^post17, lt_26^0'=lt_26^post17, k_289^0'=k_289^post17, t_18^0'=t_18^post17, lt_36^0'=lt_36^post17, x_22^0'=x_22^post17, k_187^0'=k_187^post17, ___patmp2^0'=___patmp2^post17, lt_32^0'=lt_32^post17, len_99^0'=len_99^post17, w_17^0'=w_17^post17, lt_38^0'=lt_38^post17, Result_4^0'=Result_4^post17, y_12^0'=y_12^post17, k_243^0'=k_243^post17, k_139^0'=k_139^post17, lt_35^0'=lt_35^post17, lt_25^0'=lt_25^post17, y_23^0'=y_23^post17, x_19^0'=x_19^post17, ___patmp1^0'=___patmp1^post17, lt_27^0'=lt_27^post17, len_263^0'=len_263^post17, tmp_9^0'=tmp_9^post17, lt_37^0'=lt_37^post17, x_8^0'=x_8^post17, k_208^0'=k_208^post17, (-x_8^post17+x_8^0 == 0 /\ len_99^0-len_99^post17 == 0 /\ -lt_25^post17+lt_25^0 == 0 /\ y_12^0-y_12^post17 == 0 /\ k_289^0-k_289^post17 == 0 /\ -___patmp1^post17+___patmp1^0 == 0 /\ -lt_27^post17+lt_27^0 == 0 /\ t_18^0-t_18^post17 == 0 /\ len_263^0-len_263^post17 == 0 /\ -___patmp2^post17+___patmp2^0 == 0 /\ lt_24^0-lt_24^post17 == 0 /\ -y_23^post17+y_23^0 == 0 /\ x_19^0-x_19^post17 == 0 /\ -k_208^post17+k_208^0 == 0 /\ -lt_36^post17+lt_36^0 == 0 /\ -k_139^post17+k_139^0 == 0 /\ k_243^0-k_243^post17 == 0 /\ -lt_32^post17+lt_32^0 == 0 /\ k_187^0-k_187^post17 == 0 /\ -lt_38^post17+lt_38^0 == 0 /\ 1-w_17^0+x_19^0 <= 0 /\ x_13^0-x_13^post17 == 0 /\ -tmp_9^post17+tmp_9^0 == 0 /\ -lt_34^post17+lt_34^0 == 0 /\ y_20^0-y_20^post17 == 0 /\ lt_26^0-lt_26^post17 == 0 /\ a_11^0-a_11^post17 == 0 /\ -lt_35^post17+lt_35^0 == 0 /\ ___cil_tmp5_10^0-___cil_tmp5_10^post17 == 0 /\ -lt_37^post17+lt_37^0 == 0 /\ x_22^0-x_22^post17 == 0 /\ Result_4^0-Result_4^post17 == 0 /\ -w_17^post17+w_17^0 == 0), cost: 1
New rule:
l1 -> l13 : 1-w_17^0+x_19^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l13 -> l12 : a_11^0'=a_11^post18, lt_34^0'=lt_34^post18, lt_24^0'=lt_24^post18, y_20^0'=y_20^post18, x_13^0'=x_13^post18, ___cil_tmp5_10^0'=___cil_tmp5_10^post18, lt_26^0'=lt_26^post18, k_289^0'=k_289^post18, t_18^0'=t_18^post18, lt_36^0'=lt_36^post18, x_22^0'=x_22^post18, k_187^0'=k_187^post18, ___patmp2^0'=___patmp2^post18, lt_32^0'=lt_32^post18, len_99^0'=len_99^post18, w_17^0'=w_17^post18, lt_38^0'=lt_38^post18, Result_4^0'=Result_4^post18, y_12^0'=y_12^post18, k_243^0'=k_243^post18, k_139^0'=k_139^post18, lt_35^0'=lt_35^post18, lt_25^0'=lt_25^post18, y_23^0'=y_23^post18, x_19^0'=x_19^post18, ___patmp1^0'=___patmp1^post18, lt_27^0'=lt_27^post18, len_263^0'=len_263^post18, tmp_9^0'=tmp_9^post18, lt_37^0'=lt_37^post18, x_8^0'=x_8^post18, k_208^0'=k_208^post18, (-x_8^post18+x_8^0 == 0 /\ len_99^0-len_99^post18 == 0 /\ y_20^post18-t_18^post18 == 0 /\ y_12^0-y_12^post18 == 0 /\ -lt_25^post18+lt_25^0 == 0 /\ -lt_26^post18+lt_26^0 == 0 /\ k_289^0-k_289^post18 == 0 /\ -lt_27^post18+lt_27^0 == 0 /\ len_263^0-len_263^post18 == 0 /\ -___patmp2^post18+___patmp2^0 == 0 /\ lt_24^0-lt_24^post18 == 0 /\ ___cil_tmp5_10^0-___cil_tmp5_10^post18 == 0 /\ -k_139^post18+k_139^0 == 0 /\ -y_23^post18+y_23^0 == 0 /\ x_19^0-x_19^post18 == 0 /\ -lt_32^post18+lt_32^0 == 0 /\ k_187^0-k_187^post18 == 0 /\ k_243^0-k_243^post18 == 0 /\ -lt_36^post18+lt_36^0 == 0 /\ -k_208^post18+k_208^0 == 0 /\ -___patmp1^post18+___patmp1^0 == 0 /\ -tmp_9^post18+tmp_9^0 == 0 /\ -lt_38^post18+lt_38^0 == 0 /\ -lt_35^post18+lt_35^0 == 0 /\ a_11^0-a_11^post18 == 0 /\ -lt_37^post18+lt_37^0 == 0 /\ x_13^0-x_13^post18 == 0 /\ x_22^0-x_22^post18 == 0 /\ Result_4^0-Result_4^post18 == 0 /\ -w_17^post18+w_17^0 == 0 /\ -x_19^0+t_18^post18 == 0 /\ -lt_34^post18+lt_34^0 == 0), cost: 1
New rule:
l13 -> l12 : y_20^0'=x_19^0, t_18^0'=x_19^0, TRUE, cost: 1

Applied preprocessing
Original rule:
l12 -> l1 : a_11^0'=a_11^post19, lt_34^0'=lt_34^post19, lt_24^0'=lt_24^post19, y_20^0'=y_20^post19, x_13^0'=x_13^post19, ___cil_tmp5_10^0'=___cil_tmp5_10^post19, lt_26^0'=lt_26^post19, k_289^0'=k_289^post19, t_18^0'=t_18^post19, lt_36^0'=lt_36^post19, x_22^0'=x_22^post19, k_187^0'=k_187^post19, ___patmp2^0'=___patmp2^post19, lt_32^0'=lt_32^post19, len_99^0'=len_99^post19, w_17^0'=w_17^post19, lt_38^0'=lt_38^post19, Result_4^0'=Result_4^post19, y_12^0'=y_12^post19, k_243^0'=k_243^post19, k_139^0'=k_139^post19, lt_35^0'=lt_35^post19, lt_25^0'=lt_25^post19, y_23^0'=y_23^post19, x_19^0'=x_19^post19, ___patmp1^0'=___patmp1^post19, lt_27^0'=lt_27^post19, len_263^0'=len_263^post19, tmp_9^0'=tmp_9^post19, lt_37^0'=lt_37^post19, x_8^0'=x_8^post19, k_208^0'=k_208^post19, (-k_208^post19+k_208^0 == 0 /\ -lt_36^post19+lt_36^0 == 0 /\ lt_34^0-lt_34^post19 == 0 /\ y_20^0-y_20^post19 == 0 /\ -y_23^post19+y_23^0 == 0 /\ -___patmp2^post19+___patmp2^0 == 0 /\ t_18^0-t_18^post19 == 0 /\ x_13^0-x_13^post19 == 0 /\ x_22^0-x_22^post19 == 0 /\ len_99^0-len_99^post19 == 0 /\ -lt_38^post19+lt_38^0 == 0 /\ -tmp_9^post19+tmp_9^0 == 0 /\ ___cil_tmp5_10^0-___cil_tmp5_10^post19 == 0 /\ -lt_35^post19+lt_35^0 == 0 /\ w_17^0-w_17^post19 == 0 /\ k_187^0-k_187^post19 == 0 /\ y_12^0-y_12^post19 == 0 /\ -lt_32^post19+lt_32^0 == 0 /\ -lt_37^post19+lt_37^0 == 0 /\ -len_263^post19+len_263^0 == 0 /\ -lt_26^post19+lt_26^0 == 0 /\ k_289^0-k_289^post19 == 0 /\ -x_8^post19+x_8^0 == 0 /\ a_11^0-a_11^post19 == 0 /\ -k_243^post19+k_243^0 == 0 /\ -lt_27^post19+lt_27^0 == 0 /\ lt_24^0-lt_24^post19 == 0 /\ -lt_25^post19+lt_25^0 == 0 /\ k_139^0-k_139^post19 == 0 /\ x_19^0-x_19^post19 == 0 /\ -___patmp1^post19+___patmp1^0 == 0 /\ -Result_4^post19+Result_4^0 == 0), cost: 1
New rule:
l12 -> l1 : TRUE, cost: 1

Applied preprocessing
Original rule:
l14 -> l9 : a_11^0'=a_11^post20, lt_34^0'=lt_34^post20, lt_24^0'=lt_24^post20, y_20^0'=y_20^post20, x_13^0'=x_13^post20, ___cil_tmp5_10^0'=___cil_tmp5_10^post20, lt_26^0'=lt_26^post20, k_289^0'=k_289^post20, t_18^0'=t_18^post20, lt_36^0'=lt_36^post20, x_22^0'=x_22^post20, k_187^0'=k_187^post20, ___patmp2^0'=___patmp2^post20, lt_32^0'=lt_32^post20, len_99^0'=len_99^post20, w_17^0'=w_17^post20, lt_38^0'=lt_38^post20, Result_4^0'=Result_4^post20, y_12^0'=y_12^post20, k_243^0'=k_243^post20, k_139^0'=k_139^post20, lt_35^0'=lt_35^post20, lt_25^0'=lt_25^post20, y_23^0'=y_23^post20, x_19^0'=x_19^post20, ___patmp1^0'=___patmp1^post20, lt_27^0'=lt_27^post20, len_263^0'=len_263^post20, tmp_9^0'=tmp_9^post20, lt_37^0'=lt_37^post20, x_8^0'=x_8^post20, k_208^0'=k_208^post20, (-lt_25^post20+lt_25^0 == 0 /\ ___cil_tmp5_10^0-___cil_tmp5_10^post20 == 0 /\ -k_243^post20+k_243^0 == 0 /\ -lt_37^post20+lt_37^0 == 0 /\ -Result_4^post20+Result_4^0 == 0 /\ y_20^0-y_20^post20 == 0 /\ w_17^0-w_17^post20 == 0 /\ k_187^0-k_187^post20 == 0 /\ -lt_27^post20+lt_27^0 == 0 /\ lt_36^0-lt_36^post20 == 0 /\ -___patmp1^post20+___patmp1^0 == 0 /\ x_13^0-x_13^post20 == 0 /\ lt_34^0-lt_34^post20 == 0 /\ y_12^0-y_12^post20 == 0 /\ a_11^0-a_11^post20 == 0 /\ -lt_38^post20+lt_38^0 == 0 /\ -x_19^post20+x_19^0 == 0 /\ len_99^0-len_99^post20 == 0 /\ -x_22^post20+x_22^0 == 0 /\ -x_8^post20+x_8^0 == 0 /\ lt_26^0-lt_26^post20 == 0 /\ k_139^0-k_139^post20 == 0 /\ -y_23^post20+y_23^0 == 0 /\ t_18^0-t_18^post20 == 0 /\ k_289^0-k_289^post20 == 0 /\ -len_263^post20+len_263^0 == 0 /\ lt_24^0-lt_24^post20 == 0 /\ ___patmp2^0-___patmp2^post20 == 0 /\ tmp_9^0-tmp_9^post20 == 0 /\ -lt_32^post20+lt_32^0 == 0 /\ -k_208^post20+k_208^0 == 0 /\ -lt_35^post20+lt_35^0 == 0), cost: 1
New rule:
l14 -> l9 : TRUE, cost: 1

Simplified rules
Start location: l14
  21: l0 -> l2 : lt_34^0'=lt_34^post0, y_20^0'=w_17^0, lt_32^0'=lt_32^post0, Result_4^0'=Result_4^post0, x_19^0'=lt_32^10, (-x_13^0+y_12^0 == 0 /\ -1+k_243^0 >= 0 /\ len_263^0 >= 0), cost: 1
  28: l0 -> l7 : k_289^0'=-1+k_243^0, (-1+k_243^0 >= 0 /\ len_263^0 >= 0), cost: 1
  22: l2 -> l3 : 1+w_17^0-x_19^0 <= 0, cost: 1
  23: l2 -> l3 : 1-w_17^0+x_19^0 <= 0, cost: 1
  24: l3 -> l4 : y_20^0'=x_19^0, t_18^0'=x_19^0, TRUE, cost: 1
  25: l4 -> l5 : 1+w_17^0-x_19^0 <= 0, cost: 1
  26: l4 -> l5 : 1-w_17^0+x_19^0 <= 0, cost: 1
  27: l5 -> l1 : y_20^0'=x_19^0, t_18^0'=x_19^0, TRUE, cost: 1
  37: l1 -> l13 : 1+w_17^0-x_19^0 <= 0, cost: 1
  38: l1 -> l13 : 1-w_17^0+x_19^0 <= 0, cost: 1
  29: l7 -> l8 : 1-x_13^0+y_12^0 <= 0, cost: 1
  30: l7 -> l8 : 1+x_13^0-y_12^0 <= 0, cost: 1
  31: l8 -> l6 : lt_24^0'=lt_24^post10, x_13^0'=lt_24^10, ___patmp2^0'=k_289^0, k_243^0'=k_289^0, lt_25^0'=lt_25^post10, ___patmp1^0'=1+len_263^0, len_263^0'=1+len_263^0, (k_289^0 >= 0 /\ len_263^0 >= 0), cost: 1
  32: l6 -> l0 : TRUE, cost: 1
  33: l9 -> l10 : lt_34^0'=lt_34^post12, x_13^0'=a_11^0, ___cil_tmp5_10^0'=x_8^post12, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=x_8^post12, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, (0 == 0 /\ -3 <= 0 /\ -2 <= 0 /\ -4 <= 0), cost: 1
  34: l10 -> l11 : 1-x_13^0+y_12^0 <= 0, cost: 1
  35: l10 -> l11 : 1+x_13^0-y_12^0 <= 0, cost: 1
  36: l11 -> l0 : x_13^0'=lt_26^10, lt_26^0'=lt_26^post15, ___patmp2^0'=k_208^0, k_243^0'=k_208^0, ___patmp1^0'=1, lt_27^0'=lt_27^post15, len_263^0'=1, k_208^0 >= 0, cost: 1
  39: l13 -> l12 : y_20^0'=x_19^0, t_18^0'=x_19^0, TRUE, cost: 1
  40: l12 -> l1 : TRUE, cost: 1
  41: l14 -> l9 : TRUE, cost: 1


Eliminating location l9 by chaining:

Applied chaining
First rule:
l14 -> l9 : TRUE, cost: 1
Second rule:
l9 -> l10 : lt_34^0'=lt_34^post12, x_13^0'=a_11^0, ___cil_tmp5_10^0'=x_8^post12, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=x_8^post12, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, (0 == 0 /\ -3 <= 0 /\ -2 <= 0 /\ -4 <= 0), cost: 1
New rule:
l14 -> l10 : lt_34^0'=lt_34^post12, x_13^0'=a_11^0, ___cil_tmp5_10^0'=x_8^post12, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=x_8^post12, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, (0 == 0 /\ -3 <= 0 /\ -2 <= 0 /\ -4 <= 0), cost: 2

Applied deletion
Removed the following rules: 33 41

Eliminating location l12 by chaining:

Applied chaining
First rule:
l13 -> l12 : y_20^0'=x_19^0, t_18^0'=x_19^0, TRUE, cost: 1
Second rule:
l12 -> l1 : TRUE, cost: 1
New rule:
l13 -> l1 : y_20^0'=x_19^0, t_18^0'=x_19^0, TRUE, cost: 2

Applied deletion
Removed the following rules: 39 40

Eliminating location l6 by chaining:

Applied chaining
First rule:
l8 -> l6 : lt_24^0'=lt_24^post10, x_13^0'=lt_24^10, ___patmp2^0'=k_289^0, k_243^0'=k_289^0, lt_25^0'=lt_25^post10, ___patmp1^0'=1+len_263^0, len_263^0'=1+len_263^0, (k_289^0 >= 0 /\ len_263^0 >= 0), cost: 1
Second rule:
l6 -> l0 : TRUE, cost: 1
New rule:
l8 -> l0 : lt_24^0'=lt_24^post10, x_13^0'=lt_24^10, ___patmp2^0'=k_289^0, k_243^0'=k_289^0, lt_25^0'=lt_25^post10, ___patmp1^0'=1+len_263^0, len_263^0'=1+len_263^0, (k_289^0 >= 0 /\ len_263^0 >= 0), cost: 2

Applied deletion
Removed the following rules: 31 32

Eliminated locations on linear paths
Start location: l14
  21: l0 -> l2 : lt_34^0'=lt_34^post0, y_20^0'=w_17^0, lt_32^0'=lt_32^post0, Result_4^0'=Result_4^post0, x_19^0'=lt_32^10, (-x_13^0+y_12^0 == 0 /\ -1+k_243^0 >= 0 /\ len_263^0 >= 0), cost: 1
  28: l0 -> l7 : k_289^0'=-1+k_243^0, (-1+k_243^0 >= 0 /\ len_263^0 >= 0), cost: 1
  22: l2 -> l3 : 1+w_17^0-x_19^0 <= 0, cost: 1
  23: l2 -> l3 : 1-w_17^0+x_19^0 <= 0, cost: 1
  24: l3 -> l4 : y_20^0'=x_19^0, t_18^0'=x_19^0, TRUE, cost: 1
  25: l4 -> l5 : 1+w_17^0-x_19^0 <= 0, cost: 1
  26: l4 -> l5 : 1-w_17^0+x_19^0 <= 0, cost: 1
  27: l5 -> l1 : y_20^0'=x_19^0, t_18^0'=x_19^0, TRUE, cost: 1
  37: l1 -> l13 : 1+w_17^0-x_19^0 <= 0, cost: 1
  38: l1 -> l13 : 1-w_17^0+x_19^0 <= 0, cost: 1
  29: l7 -> l8 : 1-x_13^0+y_12^0 <= 0, cost: 1
  30: l7 -> l8 : 1+x_13^0-y_12^0 <= 0, cost: 1
  44: l8 -> l0 : lt_24^0'=lt_24^post10, x_13^0'=lt_24^10, ___patmp2^0'=k_289^0, k_243^0'=k_289^0, lt_25^0'=lt_25^post10, ___patmp1^0'=1+len_263^0, len_263^0'=1+len_263^0, (k_289^0 >= 0 /\ len_263^0 >= 0), cost: 2
  34: l10 -> l11 : 1-x_13^0+y_12^0 <= 0, cost: 1
  35: l10 -> l11 : 1+x_13^0-y_12^0 <= 0, cost: 1
  36: l11 -> l0 : x_13^0'=lt_26^10, lt_26^0'=lt_26^post15, ___patmp2^0'=k_208^0, k_243^0'=k_208^0, ___patmp1^0'=1, lt_27^0'=lt_27^post15, len_263^0'=1, k_208^0 >= 0, cost: 1
  43: l13 -> l1 : y_20^0'=x_19^0, t_18^0'=x_19^0, TRUE, cost: 2
  42: l14 -> l10 : lt_34^0'=lt_34^post12, x_13^0'=a_11^0, ___cil_tmp5_10^0'=x_8^post12, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=x_8^post12, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, (0 == 0 /\ -3 <= 0 /\ -2 <= 0 /\ -4 <= 0), cost: 2


Eliminating location l10 by chaining:

Applied chaining
First rule:
l14 -> l10 : lt_34^0'=lt_34^post12, x_13^0'=a_11^0, ___cil_tmp5_10^0'=x_8^post12, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=x_8^post12, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, (0 == 0 /\ -3 <= 0 /\ -2 <= 0 /\ -4 <= 0), cost: 2
Second rule:
l10 -> l11 : 1-x_13^0+y_12^0 <= 0, cost: 1
New rule:
l14 -> l11 : lt_34^0'=lt_34^post12, x_13^0'=a_11^0, ___cil_tmp5_10^0'=x_8^post12, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=x_8^post12, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, (0 == 0 /\ -3 <= 0 /\ -2 <= 0 /\ -4 <= 0 /\ 1-a_11^0+y_12^0 <= 0), cost: 3

Applied simplification
Original rule:
l14 -> l11 : lt_34^0'=lt_34^post12, x_13^0'=a_11^0, ___cil_tmp5_10^0'=x_8^post12, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=x_8^post12, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, (0 == 0 /\ -3 <= 0 /\ -2 <= 0 /\ -4 <= 0 /\ 1-a_11^0+y_12^0 <= 0), cost: 3
New rule:
l14 -> l11 : lt_34^0'=lt_34^post12, x_13^0'=a_11^0, ___cil_tmp5_10^0'=x_8^post12, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=x_8^post12, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, 1-a_11^0+y_12^0 <= 0, cost: 3

Applied chaining
First rule:
l14 -> l10 : lt_34^0'=lt_34^post12, x_13^0'=a_11^0, ___cil_tmp5_10^0'=x_8^post12, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=x_8^post12, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, (0 == 0 /\ -3 <= 0 /\ -2 <= 0 /\ -4 <= 0), cost: 2
Second rule:
l10 -> l11 : 1+x_13^0-y_12^0 <= 0, cost: 1
New rule:
l14 -> l11 : lt_34^0'=lt_34^post12, x_13^0'=a_11^0, ___cil_tmp5_10^0'=x_8^post12, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=x_8^post12, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, (0 == 0 /\ -3 <= 0 /\ -2 <= 0 /\ -4 <= 0 /\ 1+a_11^0-y_12^0 <= 0), cost: 3

Applied simplification
Original rule:
l14 -> l11 : lt_34^0'=lt_34^post12, x_13^0'=a_11^0, ___cil_tmp5_10^0'=x_8^post12, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=x_8^post12, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, (0 == 0 /\ -3 <= 0 /\ -2 <= 0 /\ -4 <= 0 /\ 1+a_11^0-y_12^0 <= 0), cost: 3
New rule:
l14 -> l11 : lt_34^0'=lt_34^post12, x_13^0'=a_11^0, ___cil_tmp5_10^0'=x_8^post12, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=x_8^post12, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, 1+a_11^0-y_12^0 <= 0, cost: 3

Applied deletion
Removed the following rules: 34 35 42

Eliminating location l2 by chaining:

Applied chaining
First rule:
l0 -> l2 : lt_34^0'=lt_34^post0, y_20^0'=w_17^0, lt_32^0'=lt_32^post0, Result_4^0'=Result_4^post0, x_19^0'=lt_32^10, (-x_13^0+y_12^0 == 0 /\ -1+k_243^0 >= 0 /\ len_263^0 >= 0), cost: 1
Second rule:
l2 -> l3 : 1+w_17^0-x_19^0 <= 0, cost: 1
New rule:
l0 -> l3 : lt_34^0'=lt_34^post0, y_20^0'=w_17^0, lt_32^0'=lt_32^post0, Result_4^0'=Result_4^post0, x_19^0'=lt_32^10, (-x_13^0+y_12^0 == 0 /\ 1+w_17^0-lt_32^10 <= 0 /\ -1+k_243^0 >= 0 /\ len_263^0 >= 0), cost: 2

Applied chaining
First rule:
l0 -> l2 : lt_34^0'=lt_34^post0, y_20^0'=w_17^0, lt_32^0'=lt_32^post0, Result_4^0'=Result_4^post0, x_19^0'=lt_32^10, (-x_13^0+y_12^0 == 0 /\ -1+k_243^0 >= 0 /\ len_263^0 >= 0), cost: 1
Second rule:
l2 -> l3 : 1-w_17^0+x_19^0 <= 0, cost: 1
New rule:
l0 -> l3 : lt_34^0'=lt_34^post0, y_20^0'=w_17^0, lt_32^0'=lt_32^post0, Result_4^0'=Result_4^post0, x_19^0'=lt_32^10, (-x_13^0+y_12^0 == 0 /\ -1+k_243^0 >= 0 /\ len_263^0 >= 0 /\ 1-w_17^0+lt_32^10 <= 0), cost: 2

Applied deletion
Removed the following rules: 21 22 23

Eliminating location l7 by chaining:

Applied chaining
First rule:
l0 -> l7 : k_289^0'=-1+k_243^0, (-1+k_243^0 >= 0 /\ len_263^0 >= 0), cost: 1
Second rule:
l7 -> l8 : 1-x_13^0+y_12^0 <= 0, cost: 1
New rule:
l0 -> l8 : k_289^0'=-1+k_243^0, (1-x_13^0+y_12^0 <= 0 /\ -1+k_243^0 >= 0 /\ len_263^0 >= 0), cost: 2

Applied chaining
First rule:
l0 -> l7 : k_289^0'=-1+k_243^0, (-1+k_243^0 >= 0 /\ len_263^0 >= 0), cost: 1
Second rule:
l7 -> l8 : 1+x_13^0-y_12^0 <= 0, cost: 1
New rule:
l0 -> l8 : k_289^0'=-1+k_243^0, (1+x_13^0-y_12^0 <= 0 /\ -1+k_243^0 >= 0 /\ len_263^0 >= 0), cost: 2

Applied deletion
Removed the following rules: 28 29 30

Eliminating location l4 by chaining:

Applied chaining
First rule:
l3 -> l4 : y_20^0'=x_19^0, t_18^0'=x_19^0, TRUE, cost: 1
Second rule:
l4 -> l5 : 1+w_17^0-x_19^0 <= 0, cost: 1
New rule:
l3 -> l5 : y_20^0'=x_19^0, t_18^0'=x_19^0, 1+w_17^0-x_19^0 <= 0, cost: 2

Applied chaining
First rule:
l3 -> l4 : y_20^0'=x_19^0, t_18^0'=x_19^0, TRUE, cost: 1
Second rule:
l4 -> l5 : 1-w_17^0+x_19^0 <= 0, cost: 1
New rule:
l3 -> l5 : y_20^0'=x_19^0, t_18^0'=x_19^0, 1-w_17^0+x_19^0 <= 0, cost: 2

Applied deletion
Removed the following rules: 24 25 26

Eliminating location l13 by chaining:

Applied chaining
First rule:
l1 -> l13 : 1+w_17^0-x_19^0 <= 0, cost: 1
Second rule:
l13 -> l1 : y_20^0'=x_19^0, t_18^0'=x_19^0, TRUE, cost: 2
New rule:
l1 -> l1 : y_20^0'=x_19^0, t_18^0'=x_19^0, 1+w_17^0-x_19^0 <= 0, cost: 3

Applied chaining
First rule:
l1 -> l13 : 1-w_17^0+x_19^0 <= 0, cost: 1
Second rule:
l13 -> l1 : y_20^0'=x_19^0, t_18^0'=x_19^0, TRUE, cost: 2
New rule:
l1 -> l1 : y_20^0'=x_19^0, t_18^0'=x_19^0, 1-w_17^0+x_19^0 <= 0, cost: 3

Applied deletion
Removed the following rules: 37 38 43

Eliminated locations on tree-shaped paths
Start location: l14
  47: l0 -> l3 : lt_34^0'=lt_34^post0, y_20^0'=w_17^0, lt_32^0'=lt_32^post0, Result_4^0'=Result_4^post0, x_19^0'=lt_32^10, (-x_13^0+y_12^0 == 0 /\ 1+w_17^0-lt_32^10 <= 0 /\ -1+k_243^0 >= 0 /\ len_263^0 >= 0), cost: 2
  48: l0 -> l3 : lt_34^0'=lt_34^post0, y_20^0'=w_17^0, lt_32^0'=lt_32^post0, Result_4^0'=Result_4^post0, x_19^0'=lt_32^10, (-x_13^0+y_12^0 == 0 /\ -1+k_243^0 >= 0 /\ len_263^0 >= 0 /\ 1-w_17^0+lt_32^10 <= 0), cost: 2
  49: l0 -> l8 : k_289^0'=-1+k_243^0, (1-x_13^0+y_12^0 <= 0 /\ -1+k_243^0 >= 0 /\ len_263^0 >= 0), cost: 2
  50: l0 -> l8 : k_289^0'=-1+k_243^0, (1+x_13^0-y_12^0 <= 0 /\ -1+k_243^0 >= 0 /\ len_263^0 >= 0), cost: 2
  51: l3 -> l5 : y_20^0'=x_19^0, t_18^0'=x_19^0, 1+w_17^0-x_19^0 <= 0, cost: 2
  52: l3 -> l5 : y_20^0'=x_19^0, t_18^0'=x_19^0, 1-w_17^0+x_19^0 <= 0, cost: 2
  27: l5 -> l1 : y_20^0'=x_19^0, t_18^0'=x_19^0, TRUE, cost: 1
  53: l1 -> l1 : y_20^0'=x_19^0, t_18^0'=x_19^0, 1+w_17^0-x_19^0 <= 0, cost: 3
  54: l1 -> l1 : y_20^0'=x_19^0, t_18^0'=x_19^0, 1-w_17^0+x_19^0 <= 0, cost: 3
  44: l8 -> l0 : lt_24^0'=lt_24^post10, x_13^0'=lt_24^10, ___patmp2^0'=k_289^0, k_243^0'=k_289^0, lt_25^0'=lt_25^post10, ___patmp1^0'=1+len_263^0, len_263^0'=1+len_263^0, (k_289^0 >= 0 /\ len_263^0 >= 0), cost: 2
  36: l11 -> l0 : x_13^0'=lt_26^10, lt_26^0'=lt_26^post15, ___patmp2^0'=k_208^0, k_243^0'=k_208^0, ___patmp1^0'=1, lt_27^0'=lt_27^post15, len_263^0'=1, k_208^0 >= 0, cost: 1
  45: l14 -> l11 : lt_34^0'=lt_34^post12, x_13^0'=a_11^0, ___cil_tmp5_10^0'=x_8^post12, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=x_8^post12, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, 1-a_11^0+y_12^0 <= 0, cost: 3
  46: l14 -> l11 : lt_34^0'=lt_34^post12, x_13^0'=a_11^0, ___cil_tmp5_10^0'=x_8^post12, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=x_8^post12, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, 1+a_11^0-y_12^0 <= 0, cost: 3


Applied nonterm
Original rule:
l1 -> l1 : y_20^0'=x_19^0, t_18^0'=x_19^0, 1+w_17^0-x_19^0 <= 0, cost: 3
New rule:
l1 -> [15] : (-1-w_17^0+x_19^0 >= 0 /\ -1+n >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_jABJHb.txt

Applied nonterm
Original rule:
l1 -> l1 : y_20^0'=x_19^0, t_18^0'=x_19^0, 1-w_17^0+x_19^0 <= 0, cost: 3
New rule:
l1 -> [15] : (-1+w_17^0-x_19^0 >= 0 /\ -1+n0 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_LPACdc.txt

Applied deletion
Removed the following rules: 53 54

Accelerated simple loops
Start location: l14
  47: l0 -> l3 : lt_34^0'=lt_34^post0, y_20^0'=w_17^0, lt_32^0'=lt_32^post0, Result_4^0'=Result_4^post0, x_19^0'=lt_32^10, (-x_13^0+y_12^0 == 0 /\ 1+w_17^0-lt_32^10 <= 0 /\ -1+k_243^0 >= 0 /\ len_263^0 >= 0), cost: 2
  48: l0 -> l3 : lt_34^0'=lt_34^post0, y_20^0'=w_17^0, lt_32^0'=lt_32^post0, Result_4^0'=Result_4^post0, x_19^0'=lt_32^10, (-x_13^0+y_12^0 == 0 /\ -1+k_243^0 >= 0 /\ len_263^0 >= 0 /\ 1-w_17^0+lt_32^10 <= 0), cost: 2
  49: l0 -> l8 : k_289^0'=-1+k_243^0, (1-x_13^0+y_12^0 <= 0 /\ -1+k_243^0 >= 0 /\ len_263^0 >= 0), cost: 2
  50: l0 -> l8 : k_289^0'=-1+k_243^0, (1+x_13^0-y_12^0 <= 0 /\ -1+k_243^0 >= 0 /\ len_263^0 >= 0), cost: 2
  51: l3 -> l5 : y_20^0'=x_19^0, t_18^0'=x_19^0, 1+w_17^0-x_19^0 <= 0, cost: 2
  52: l3 -> l5 : y_20^0'=x_19^0, t_18^0'=x_19^0, 1-w_17^0+x_19^0 <= 0, cost: 2
  27: l5 -> l1 : y_20^0'=x_19^0, t_18^0'=x_19^0, TRUE, cost: 1
  55: l1 -> [15] : (-1-w_17^0+x_19^0 >= 0 /\ -1+n >= 0), cost: NONTERM
  56: l1 -> [15] : (-1+w_17^0-x_19^0 >= 0 /\ -1+n0 >= 0), cost: NONTERM
  44: l8 -> l0 : lt_24^0'=lt_24^post10, x_13^0'=lt_24^10, ___patmp2^0'=k_289^0, k_243^0'=k_289^0, lt_25^0'=lt_25^post10, ___patmp1^0'=1+len_263^0, len_263^0'=1+len_263^0, (k_289^0 >= 0 /\ len_263^0 >= 0), cost: 2
  36: l11 -> l0 : x_13^0'=lt_26^10, lt_26^0'=lt_26^post15, ___patmp2^0'=k_208^0, k_243^0'=k_208^0, ___patmp1^0'=1, lt_27^0'=lt_27^post15, len_263^0'=1, k_208^0 >= 0, cost: 1
  45: l14 -> l11 : lt_34^0'=lt_34^post12, x_13^0'=a_11^0, ___cil_tmp5_10^0'=x_8^post12, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=x_8^post12, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, 1-a_11^0+y_12^0 <= 0, cost: 3
  46: l14 -> l11 : lt_34^0'=lt_34^post12, x_13^0'=a_11^0, ___cil_tmp5_10^0'=x_8^post12, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=x_8^post12, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, 1+a_11^0-y_12^0 <= 0, cost: 3


Applied chaining
First rule:
l5 -> l1 : y_20^0'=x_19^0, t_18^0'=x_19^0, TRUE, cost: 1
Second rule:
l1 -> [15] : (-1-w_17^0+x_19^0 >= 0 /\ -1+n >= 0), cost: NONTERM
New rule:
l5 -> [15] : -1-w_17^0+x_19^0 >= 0, cost: NONTERM

Applied chaining
First rule:
l5 -> l1 : y_20^0'=x_19^0, t_18^0'=x_19^0, TRUE, cost: 1
Second rule:
l1 -> [15] : (-1+w_17^0-x_19^0 >= 0 /\ -1+n0 >= 0), cost: NONTERM
New rule:
l5 -> [15] : -1+w_17^0-x_19^0 >= 0, cost: NONTERM

Applied deletion
Removed the following rules: 55 56

Chained accelerated rules with incoming rules
Start location: l14
  47: l0 -> l3 : lt_34^0'=lt_34^post0, y_20^0'=w_17^0, lt_32^0'=lt_32^post0, Result_4^0'=Result_4^post0, x_19^0'=lt_32^10, (-x_13^0+y_12^0 == 0 /\ 1+w_17^0-lt_32^10 <= 0 /\ -1+k_243^0 >= 0 /\ len_263^0 >= 0), cost: 2
  48: l0 -> l3 : lt_34^0'=lt_34^post0, y_20^0'=w_17^0, lt_32^0'=lt_32^post0, Result_4^0'=Result_4^post0, x_19^0'=lt_32^10, (-x_13^0+y_12^0 == 0 /\ -1+k_243^0 >= 0 /\ len_263^0 >= 0 /\ 1-w_17^0+lt_32^10 <= 0), cost: 2
  49: l0 -> l8 : k_289^0'=-1+k_243^0, (1-x_13^0+y_12^0 <= 0 /\ -1+k_243^0 >= 0 /\ len_263^0 >= 0), cost: 2
  50: l0 -> l8 : k_289^0'=-1+k_243^0, (1+x_13^0-y_12^0 <= 0 /\ -1+k_243^0 >= 0 /\ len_263^0 >= 0), cost: 2
  51: l3 -> l5 : y_20^0'=x_19^0, t_18^0'=x_19^0, 1+w_17^0-x_19^0 <= 0, cost: 2
  52: l3 -> l5 : y_20^0'=x_19^0, t_18^0'=x_19^0, 1-w_17^0+x_19^0 <= 0, cost: 2
  27: l5 -> l1 : y_20^0'=x_19^0, t_18^0'=x_19^0, TRUE, cost: 1
  57: l5 -> [15] : -1-w_17^0+x_19^0 >= 0, cost: NONTERM
  58: l5 -> [15] : -1+w_17^0-x_19^0 >= 0, cost: NONTERM
  44: l8 -> l0 : lt_24^0'=lt_24^post10, x_13^0'=lt_24^10, ___patmp2^0'=k_289^0, k_243^0'=k_289^0, lt_25^0'=lt_25^post10, ___patmp1^0'=1+len_263^0, len_263^0'=1+len_263^0, (k_289^0 >= 0 /\ len_263^0 >= 0), cost: 2
  36: l11 -> l0 : x_13^0'=lt_26^10, lt_26^0'=lt_26^post15, ___patmp2^0'=k_208^0, k_243^0'=k_208^0, ___patmp1^0'=1, lt_27^0'=lt_27^post15, len_263^0'=1, k_208^0 >= 0, cost: 1
  45: l14 -> l11 : lt_34^0'=lt_34^post12, x_13^0'=a_11^0, ___cil_tmp5_10^0'=x_8^post12, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=x_8^post12, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, 1-a_11^0+y_12^0 <= 0, cost: 3
  46: l14 -> l11 : lt_34^0'=lt_34^post12, x_13^0'=a_11^0, ___cil_tmp5_10^0'=x_8^post12, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=x_8^post12, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, 1+a_11^0-y_12^0 <= 0, cost: 3


Removed unreachable locations and irrelevant leafs
Start location: l14
  47: l0 -> l3 : lt_34^0'=lt_34^post0, y_20^0'=w_17^0, lt_32^0'=lt_32^post0, Result_4^0'=Result_4^post0, x_19^0'=lt_32^10, (-x_13^0+y_12^0 == 0 /\ 1+w_17^0-lt_32^10 <= 0 /\ -1+k_243^0 >= 0 /\ len_263^0 >= 0), cost: 2
  48: l0 -> l3 : lt_34^0'=lt_34^post0, y_20^0'=w_17^0, lt_32^0'=lt_32^post0, Result_4^0'=Result_4^post0, x_19^0'=lt_32^10, (-x_13^0+y_12^0 == 0 /\ -1+k_243^0 >= 0 /\ len_263^0 >= 0 /\ 1-w_17^0+lt_32^10 <= 0), cost: 2
  49: l0 -> l8 : k_289^0'=-1+k_243^0, (1-x_13^0+y_12^0 <= 0 /\ -1+k_243^0 >= 0 /\ len_263^0 >= 0), cost: 2
  50: l0 -> l8 : k_289^0'=-1+k_243^0, (1+x_13^0-y_12^0 <= 0 /\ -1+k_243^0 >= 0 /\ len_263^0 >= 0), cost: 2
  51: l3 -> l5 : y_20^0'=x_19^0, t_18^0'=x_19^0, 1+w_17^0-x_19^0 <= 0, cost: 2
  52: l3 -> l5 : y_20^0'=x_19^0, t_18^0'=x_19^0, 1-w_17^0+x_19^0 <= 0, cost: 2
  57: l5 -> [15] : -1-w_17^0+x_19^0 >= 0, cost: NONTERM
  58: l5 -> [15] : -1+w_17^0-x_19^0 >= 0, cost: NONTERM
  44: l8 -> l0 : lt_24^0'=lt_24^post10, x_13^0'=lt_24^10, ___patmp2^0'=k_289^0, k_243^0'=k_289^0, lt_25^0'=lt_25^post10, ___patmp1^0'=1+len_263^0, len_263^0'=1+len_263^0, (k_289^0 >= 0 /\ len_263^0 >= 0), cost: 2
  36: l11 -> l0 : x_13^0'=lt_26^10, lt_26^0'=lt_26^post15, ___patmp2^0'=k_208^0, k_243^0'=k_208^0, ___patmp1^0'=1, lt_27^0'=lt_27^post15, len_263^0'=1, k_208^0 >= 0, cost: 1
  45: l14 -> l11 : lt_34^0'=lt_34^post12, x_13^0'=a_11^0, ___cil_tmp5_10^0'=x_8^post12, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=x_8^post12, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, 1-a_11^0+y_12^0 <= 0, cost: 3
  46: l14 -> l11 : lt_34^0'=lt_34^post12, x_13^0'=a_11^0, ___cil_tmp5_10^0'=x_8^post12, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=x_8^post12, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, 1+a_11^0-y_12^0 <= 0, cost: 3


Eliminating location l11 by chaining:

Applied chaining
First rule:
l14 -> l11 : lt_34^0'=lt_34^post12, x_13^0'=a_11^0, ___cil_tmp5_10^0'=x_8^post12, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=x_8^post12, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, 1-a_11^0+y_12^0 <= 0, cost: 3
Second rule:
l11 -> l0 : x_13^0'=lt_26^10, lt_26^0'=lt_26^post15, ___patmp2^0'=k_208^0, k_243^0'=k_208^0, ___patmp1^0'=1, lt_27^0'=lt_27^post15, len_263^0'=1, k_208^0 >= 0, cost: 1
New rule:
l14 -> l0 : lt_34^0'=lt_34^post12, x_13^0'=lt_26^10, ___cil_tmp5_10^0'=x_8^post12, lt_26^0'=lt_26^post15, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, ___patmp2^0'=4, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=x_8^post12, k_243^0'=4, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, ___patmp1^0'=1, lt_27^0'=lt_27^post15, len_263^0'=1, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, (4 >= 0 /\ 1-a_11^0+y_12^0 <= 0), cost: 4

Applied simplification
Original rule:
l14 -> l0 : lt_34^0'=lt_34^post12, x_13^0'=lt_26^10, ___cil_tmp5_10^0'=x_8^post12, lt_26^0'=lt_26^post15, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, ___patmp2^0'=4, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=x_8^post12, k_243^0'=4, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, ___patmp1^0'=1, lt_27^0'=lt_27^post15, len_263^0'=1, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, (4 >= 0 /\ 1-a_11^0+y_12^0 <= 0), cost: 4
New rule:
l14 -> l0 : lt_34^0'=lt_34^post12, x_13^0'=lt_26^10, ___cil_tmp5_10^0'=x_8^post12, lt_26^0'=lt_26^post15, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, ___patmp2^0'=4, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=x_8^post12, k_243^0'=4, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, ___patmp1^0'=1, lt_27^0'=lt_27^post15, len_263^0'=1, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, 1-a_11^0+y_12^0 <= 0, cost: 4

Applied chaining
First rule:
l14 -> l11 : lt_34^0'=lt_34^post12, x_13^0'=a_11^0, ___cil_tmp5_10^0'=x_8^post12, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=x_8^post12, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, 1+a_11^0-y_12^0 <= 0, cost: 3
Second rule:
l11 -> l0 : x_13^0'=lt_26^10, lt_26^0'=lt_26^post15, ___patmp2^0'=k_208^0, k_243^0'=k_208^0, ___patmp1^0'=1, lt_27^0'=lt_27^post15, len_263^0'=1, k_208^0 >= 0, cost: 1
New rule:
l14 -> l0 : lt_34^0'=lt_34^post12, x_13^0'=lt_26^10, ___cil_tmp5_10^0'=x_8^post12, lt_26^0'=lt_26^post15, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, ___patmp2^0'=4, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=x_8^post12, k_243^0'=4, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, ___patmp1^0'=1, lt_27^0'=lt_27^post15, len_263^0'=1, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, (1+a_11^0-y_12^0 <= 0 /\ 4 >= 0), cost: 4

Applied simplification
Original rule:
l14 -> l0 : lt_34^0'=lt_34^post12, x_13^0'=lt_26^10, ___cil_tmp5_10^0'=x_8^post12, lt_26^0'=lt_26^post15, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, ___patmp2^0'=4, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=x_8^post12, k_243^0'=4, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, ___patmp1^0'=1, lt_27^0'=lt_27^post15, len_263^0'=1, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, (1+a_11^0-y_12^0 <= 0 /\ 4 >= 0), cost: 4
New rule:
l14 -> l0 : lt_34^0'=lt_34^post12, x_13^0'=lt_26^10, ___cil_tmp5_10^0'=x_8^post12, lt_26^0'=lt_26^post15, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, ___patmp2^0'=4, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=x_8^post12, k_243^0'=4, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, ___patmp1^0'=1, lt_27^0'=lt_27^post15, len_263^0'=1, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, 1+a_11^0-y_12^0 <= 0, cost: 4

Applied deletion
Removed the following rules: 36 45 46

Eliminating location l3 by chaining:

Applied chaining
First rule:
l0 -> l3 : lt_34^0'=lt_34^post0, y_20^0'=w_17^0, lt_32^0'=lt_32^post0, Result_4^0'=Result_4^post0, x_19^0'=lt_32^10, (-x_13^0+y_12^0 == 0 /\ 1+w_17^0-lt_32^10 <= 0 /\ -1+k_243^0 >= 0 /\ len_263^0 >= 0), cost: 2
Second rule:
l3 -> l5 : y_20^0'=x_19^0, t_18^0'=x_19^0, 1+w_17^0-x_19^0 <= 0, cost: 2
New rule:
l0 -> l5 : lt_34^0'=lt_34^post0, y_20^0'=lt_32^10, t_18^0'=lt_32^10, lt_32^0'=lt_32^post0, Result_4^0'=Result_4^post0, x_19^0'=lt_32^10, (-x_13^0+y_12^0 == 0 /\ 1+w_17^0-lt_32^10 <= 0 /\ -1+k_243^0 >= 0 /\ len_263^0 >= 0), cost: 4

Applied chaining
First rule:
l0 -> l3 : lt_34^0'=lt_34^post0, y_20^0'=w_17^0, lt_32^0'=lt_32^post0, Result_4^0'=Result_4^post0, x_19^0'=lt_32^10, (-x_13^0+y_12^0 == 0 /\ -1+k_243^0 >= 0 /\ len_263^0 >= 0 /\ 1-w_17^0+lt_32^10 <= 0), cost: 2
Second rule:
l3 -> l5 : y_20^0'=x_19^0, t_18^0'=x_19^0, 1-w_17^0+x_19^0 <= 0, cost: 2
New rule:
l0 -> l5 : lt_34^0'=lt_34^post0, y_20^0'=lt_32^10, t_18^0'=lt_32^10, lt_32^0'=lt_32^post0, Result_4^0'=Result_4^post0, x_19^0'=lt_32^10, (-x_13^0+y_12^0 == 0 /\ -1+k_243^0 >= 0 /\ len_263^0 >= 0 /\ 1-w_17^0+lt_32^10 <= 0), cost: 4

Applied deletion
Removed the following rules: 47 48 51 52

Eliminating location l8 by chaining:

Applied chaining
First rule:
l0 -> l8 : k_289^0'=-1+k_243^0, (1-x_13^0+y_12^0 <= 0 /\ -1+k_243^0 >= 0 /\ len_263^0 >= 0), cost: 2
Second rule:
l8 -> l0 : lt_24^0'=lt_24^post10, x_13^0'=lt_24^10, ___patmp2^0'=k_289^0, k_243^0'=k_289^0, lt_25^0'=lt_25^post10, ___patmp1^0'=1+len_263^0, len_263^0'=1+len_263^0, (k_289^0 >= 0 /\ len_263^0 >= 0), cost: 2
New rule:
l0 -> l0 : lt_24^0'=lt_24^post10, x_13^0'=lt_24^10, k_289^0'=-1+k_243^0, ___patmp2^0'=-1+k_243^0, k_243^0'=-1+k_243^0, lt_25^0'=lt_25^post10, ___patmp1^0'=1+len_263^0, len_263^0'=1+len_263^0, (1-x_13^0+y_12^0 <= 0 /\ -1+k_243^0 >= 0 /\ len_263^0 >= 0), cost: 4

Applied chaining
First rule:
l0 -> l8 : k_289^0'=-1+k_243^0, (1+x_13^0-y_12^0 <= 0 /\ -1+k_243^0 >= 0 /\ len_263^0 >= 0), cost: 2
Second rule:
l8 -> l0 : lt_24^0'=lt_24^post10, x_13^0'=lt_24^10, ___patmp2^0'=k_289^0, k_243^0'=k_289^0, lt_25^0'=lt_25^post10, ___patmp1^0'=1+len_263^0, len_263^0'=1+len_263^0, (k_289^0 >= 0 /\ len_263^0 >= 0), cost: 2
New rule:
l0 -> l0 : lt_24^0'=lt_24^post10, x_13^0'=lt_24^10, k_289^0'=-1+k_243^0, ___patmp2^0'=-1+k_243^0, k_243^0'=-1+k_243^0, lt_25^0'=lt_25^post10, ___patmp1^0'=1+len_263^0, len_263^0'=1+len_263^0, (1+x_13^0-y_12^0 <= 0 /\ -1+k_243^0 >= 0 /\ len_263^0 >= 0), cost: 4

Applied deletion
Removed the following rules: 44 49 50

Eliminated locations on tree-shaped paths
Start location: l14
  61: l0 -> l5 : lt_34^0'=lt_34^post0, y_20^0'=lt_32^10, t_18^0'=lt_32^10, lt_32^0'=lt_32^post0, Result_4^0'=Result_4^post0, x_19^0'=lt_32^10, (-x_13^0+y_12^0 == 0 /\ 1+w_17^0-lt_32^10 <= 0 /\ -1+k_243^0 >= 0 /\ len_263^0 >= 0), cost: 4
  62: l0 -> l5 : lt_34^0'=lt_34^post0, y_20^0'=lt_32^10, t_18^0'=lt_32^10, lt_32^0'=lt_32^post0, Result_4^0'=Result_4^post0, x_19^0'=lt_32^10, (-x_13^0+y_12^0 == 0 /\ -1+k_243^0 >= 0 /\ len_263^0 >= 0 /\ 1-w_17^0+lt_32^10 <= 0), cost: 4
  63: l0 -> l0 : lt_24^0'=lt_24^post10, x_13^0'=lt_24^10, k_289^0'=-1+k_243^0, ___patmp2^0'=-1+k_243^0, k_243^0'=-1+k_243^0, lt_25^0'=lt_25^post10, ___patmp1^0'=1+len_263^0, len_263^0'=1+len_263^0, (1-x_13^0+y_12^0 <= 0 /\ -1+k_243^0 >= 0 /\ len_263^0 >= 0), cost: 4
  64: l0 -> l0 : lt_24^0'=lt_24^post10, x_13^0'=lt_24^10, k_289^0'=-1+k_243^0, ___patmp2^0'=-1+k_243^0, k_243^0'=-1+k_243^0, lt_25^0'=lt_25^post10, ___patmp1^0'=1+len_263^0, len_263^0'=1+len_263^0, (1+x_13^0-y_12^0 <= 0 /\ -1+k_243^0 >= 0 /\ len_263^0 >= 0), cost: 4
  57: l5 -> [15] : -1-w_17^0+x_19^0 >= 0, cost: NONTERM
  58: l5 -> [15] : -1+w_17^0-x_19^0 >= 0, cost: NONTERM
  59: l14 -> l0 : lt_34^0'=lt_34^post12, x_13^0'=lt_26^10, ___cil_tmp5_10^0'=x_8^post12, lt_26^0'=lt_26^post15, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, ___patmp2^0'=4, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=x_8^post12, k_243^0'=4, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, ___patmp1^0'=1, lt_27^0'=lt_27^post15, len_263^0'=1, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, 1-a_11^0+y_12^0 <= 0, cost: 4
  60: l14 -> l0 : lt_34^0'=lt_34^post12, x_13^0'=lt_26^10, ___cil_tmp5_10^0'=x_8^post12, lt_26^0'=lt_26^post15, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, ___patmp2^0'=4, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=x_8^post12, k_243^0'=4, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, ___patmp1^0'=1, lt_27^0'=lt_27^post15, len_263^0'=1, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, 1+a_11^0-y_12^0 <= 0, cost: 4


Applied acceleration
Original rule:
l0 -> l0 : lt_24^0'=lt_24^post10, x_13^0'=lt_24^10, k_289^0'=-1+k_243^0, ___patmp2^0'=-1+k_243^0, k_243^0'=-1+k_243^0, lt_25^0'=lt_25^post10, ___patmp1^0'=1+len_263^0, len_263^0'=1+len_263^0, (1-x_13^0+y_12^0 <= 0 /\ -1+k_243^0 >= 0 /\ len_263^0 >= 0), cost: 4
New rule:
l0 -> l0 : lt_24^0'=lt_24^post10, x_13^0'=lt_24^10, k_289^0'=k_243^0-n1, ___patmp2^0'=k_243^0-n1, k_243^0'=k_243^0-n1, lt_25^0'=lt_25^post10, ___patmp1^0'=len_263^0+n1, len_263^0'=len_263^0+n1, (-1+x_13^0-y_12^0 >= 0 /\ k_243^0-n1 >= 0 /\ -1+n1 >= 0 /\ -1-y_12^0+lt_24^10 >= 0 /\ len_263^0 >= 0), cost: 4*n1
Sub-proof via acceration calculus written to file:///tmp/tmpnam_LHKmKG.txt

Applied instantiation
Original rule:
l0 -> l0 : lt_24^0'=lt_24^post10, x_13^0'=lt_24^10, k_289^0'=k_243^0-n1, ___patmp2^0'=k_243^0-n1, k_243^0'=k_243^0-n1, lt_25^0'=lt_25^post10, ___patmp1^0'=len_263^0+n1, len_263^0'=len_263^0+n1, (-1+x_13^0-y_12^0 >= 0 /\ k_243^0-n1 >= 0 /\ -1+n1 >= 0 /\ -1-y_12^0+lt_24^10 >= 0 /\ len_263^0 >= 0), cost: 4*n1
New rule:
l0 -> l0 : lt_24^0'=lt_24^post10, x_13^0'=lt_24^10, k_289^0'=0, ___patmp2^0'=0, k_243^0'=0, lt_25^0'=lt_25^post10, ___patmp1^0'=k_243^0+len_263^0, len_263^0'=k_243^0+len_263^0, (0 >= 0 /\ -1+x_13^0-y_12^0 >= 0 /\ -1+k_243^0 >= 0 /\ -1-y_12^0+lt_24^10 >= 0 /\ len_263^0 >= 0), cost: 4*k_243^0

Applied acceleration
Original rule:
l0 -> l0 : lt_24^0'=lt_24^post10, x_13^0'=lt_24^10, k_289^0'=-1+k_243^0, ___patmp2^0'=-1+k_243^0, k_243^0'=-1+k_243^0, lt_25^0'=lt_25^post10, ___patmp1^0'=1+len_263^0, len_263^0'=1+len_263^0, (1+x_13^0-y_12^0 <= 0 /\ -1+k_243^0 >= 0 /\ len_263^0 >= 0), cost: 4
New rule:
l0 -> l0 : lt_24^0'=lt_24^post10, x_13^0'=lt_24^10, k_289^0'=-n2+k_243^0, ___patmp2^0'=-n2+k_243^0, k_243^0'=-n2+k_243^0, lt_25^0'=lt_25^post10, ___patmp1^0'=n2+len_263^0, len_263^0'=n2+len_263^0, (-1+n2 >= 0 /\ -1-x_13^0+y_12^0 >= 0 /\ -n2+k_243^0 >= 0 /\ -1+y_12^0-lt_24^10 >= 0 /\ len_263^0 >= 0), cost: 4*n2
Sub-proof via acceration calculus written to file:///tmp/tmpnam_LFNffi.txt

Applied instantiation
Original rule:
l0 -> l0 : lt_24^0'=lt_24^post10, x_13^0'=lt_24^10, k_289^0'=-n2+k_243^0, ___patmp2^0'=-n2+k_243^0, k_243^0'=-n2+k_243^0, lt_25^0'=lt_25^post10, ___patmp1^0'=n2+len_263^0, len_263^0'=n2+len_263^0, (-1+n2 >= 0 /\ -1-x_13^0+y_12^0 >= 0 /\ -n2+k_243^0 >= 0 /\ -1+y_12^0-lt_24^10 >= 0 /\ len_263^0 >= 0), cost: 4*n2
New rule:
l0 -> l0 : lt_24^0'=lt_24^post10, x_13^0'=lt_24^10, k_289^0'=0, ___patmp2^0'=0, k_243^0'=0, lt_25^0'=lt_25^post10, ___patmp1^0'=k_243^0+len_263^0, len_263^0'=k_243^0+len_263^0, (0 >= 0 /\ -1-x_13^0+y_12^0 >= 0 /\ -1+y_12^0-lt_24^10 >= 0 /\ -1+k_243^0 >= 0 /\ len_263^0 >= 0), cost: 4*k_243^0

Applied simplification
Original rule:
l0 -> l0 : lt_24^0'=lt_24^post10, x_13^0'=lt_24^10, k_289^0'=0, ___patmp2^0'=0, k_243^0'=0, lt_25^0'=lt_25^post10, ___patmp1^0'=k_243^0+len_263^0, len_263^0'=k_243^0+len_263^0, (0 >= 0 /\ -1+x_13^0-y_12^0 >= 0 /\ -1+k_243^0 >= 0 /\ -1-y_12^0+lt_24^10 >= 0 /\ len_263^0 >= 0), cost: 4*k_243^0
New rule:
l0 -> l0 : lt_24^0'=lt_24^post10, x_13^0'=lt_24^10, k_289^0'=0, ___patmp2^0'=0, k_243^0'=0, lt_25^0'=lt_25^post10, ___patmp1^0'=k_243^0+len_263^0, len_263^0'=k_243^0+len_263^0, (-1+x_13^0-y_12^0 >= 0 /\ -1+k_243^0 >= 0 /\ -1-y_12^0+lt_24^10 >= 0 /\ len_263^0 >= 0), cost: 4*k_243^0

Applied simplification
Original rule:
l0 -> l0 : lt_24^0'=lt_24^post10, x_13^0'=lt_24^10, k_289^0'=0, ___patmp2^0'=0, k_243^0'=0, lt_25^0'=lt_25^post10, ___patmp1^0'=k_243^0+len_263^0, len_263^0'=k_243^0+len_263^0, (0 >= 0 /\ -1-x_13^0+y_12^0 >= 0 /\ -1+y_12^0-lt_24^10 >= 0 /\ -1+k_243^0 >= 0 /\ len_263^0 >= 0), cost: 4*k_243^0
New rule:
l0 -> l0 : lt_24^0'=lt_24^post10, x_13^0'=lt_24^10, k_289^0'=0, ___patmp2^0'=0, k_243^0'=0, lt_25^0'=lt_25^post10, ___patmp1^0'=k_243^0+len_263^0, len_263^0'=k_243^0+len_263^0, (-1-x_13^0+y_12^0 >= 0 /\ -1+y_12^0-lt_24^10 >= 0 /\ -1+k_243^0 >= 0 /\ len_263^0 >= 0), cost: 4*k_243^0

Applied deletion
Removed the following rules: 63 64

Accelerated simple loops
Start location: l14
  61: l0 -> l5 : lt_34^0'=lt_34^post0, y_20^0'=lt_32^10, t_18^0'=lt_32^10, lt_32^0'=lt_32^post0, Result_4^0'=Result_4^post0, x_19^0'=lt_32^10, (-x_13^0+y_12^0 == 0 /\ 1+w_17^0-lt_32^10 <= 0 /\ -1+k_243^0 >= 0 /\ len_263^0 >= 0), cost: 4
  62: l0 -> l5 : lt_34^0'=lt_34^post0, y_20^0'=lt_32^10, t_18^0'=lt_32^10, lt_32^0'=lt_32^post0, Result_4^0'=Result_4^post0, x_19^0'=lt_32^10, (-x_13^0+y_12^0 == 0 /\ -1+k_243^0 >= 0 /\ len_263^0 >= 0 /\ 1-w_17^0+lt_32^10 <= 0), cost: 4
  67: l0 -> l0 : lt_24^0'=lt_24^post10, x_13^0'=lt_24^10, k_289^0'=0, ___patmp2^0'=0, k_243^0'=0, lt_25^0'=lt_25^post10, ___patmp1^0'=k_243^0+len_263^0, len_263^0'=k_243^0+len_263^0, (-1+x_13^0-y_12^0 >= 0 /\ -1+k_243^0 >= 0 /\ -1-y_12^0+lt_24^10 >= 0 /\ len_263^0 >= 0), cost: 4*k_243^0
  68: l0 -> l0 : lt_24^0'=lt_24^post10, x_13^0'=lt_24^10, k_289^0'=0, ___patmp2^0'=0, k_243^0'=0, lt_25^0'=lt_25^post10, ___patmp1^0'=k_243^0+len_263^0, len_263^0'=k_243^0+len_263^0, (-1-x_13^0+y_12^0 >= 0 /\ -1+y_12^0-lt_24^10 >= 0 /\ -1+k_243^0 >= 0 /\ len_263^0 >= 0), cost: 4*k_243^0
  57: l5 -> [15] : -1-w_17^0+x_19^0 >= 0, cost: NONTERM
  58: l5 -> [15] : -1+w_17^0-x_19^0 >= 0, cost: NONTERM
  59: l14 -> l0 : lt_34^0'=lt_34^post12, x_13^0'=lt_26^10, ___cil_tmp5_10^0'=x_8^post12, lt_26^0'=lt_26^post15, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, ___patmp2^0'=4, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=x_8^post12, k_243^0'=4, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, ___patmp1^0'=1, lt_27^0'=lt_27^post15, len_263^0'=1, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, 1-a_11^0+y_12^0 <= 0, cost: 4
  60: l14 -> l0 : lt_34^0'=lt_34^post12, x_13^0'=lt_26^10, ___cil_tmp5_10^0'=x_8^post12, lt_26^0'=lt_26^post15, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, ___patmp2^0'=4, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=x_8^post12, k_243^0'=4, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, ___patmp1^0'=1, lt_27^0'=lt_27^post15, len_263^0'=1, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, 1+a_11^0-y_12^0 <= 0, cost: 4


Applied chaining
First rule:
l14 -> l0 : lt_34^0'=lt_34^post12, x_13^0'=lt_26^10, ___cil_tmp5_10^0'=x_8^post12, lt_26^0'=lt_26^post15, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, ___patmp2^0'=4, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=x_8^post12, k_243^0'=4, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, ___patmp1^0'=1, lt_27^0'=lt_27^post15, len_263^0'=1, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, 1-a_11^0+y_12^0 <= 0, cost: 4
Second rule:
l0 -> l0 : lt_24^0'=lt_24^post10, x_13^0'=lt_24^10, k_289^0'=0, ___patmp2^0'=0, k_243^0'=0, lt_25^0'=lt_25^post10, ___patmp1^0'=k_243^0+len_263^0, len_263^0'=k_243^0+len_263^0, (-1+x_13^0-y_12^0 >= 0 /\ -1+k_243^0 >= 0 /\ -1-y_12^0+lt_24^10 >= 0 /\ len_263^0 >= 0), cost: 4*k_243^0
New rule:
l14 -> l0 : lt_34^0'=lt_34^post12, lt_24^0'=lt_24^post10, x_13^0'=lt_24^10, ___cil_tmp5_10^0'=x_8^post12, lt_26^0'=lt_26^post15, k_289^0'=0, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, ___patmp2^0'=0, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=x_8^post12, k_243^0'=0, k_139^0'=3, lt_35^0'=lt_35^post12, lt_25^0'=lt_25^post10, y_23^0'=0, ___patmp1^0'=5, lt_27^0'=lt_27^post15, len_263^0'=5, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, (-1-y_12^0+lt_24^10 >= 0 /\ 1-a_11^0+y_12^0 <= 0), cost: 20

Applied chaining
First rule:
l14 -> l0 : lt_34^0'=lt_34^post12, x_13^0'=lt_26^10, ___cil_tmp5_10^0'=x_8^post12, lt_26^0'=lt_26^post15, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, ___patmp2^0'=4, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=x_8^post12, k_243^0'=4, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, ___patmp1^0'=1, lt_27^0'=lt_27^post15, len_263^0'=1, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, 1+a_11^0-y_12^0 <= 0, cost: 4
Second rule:
l0 -> l0 : lt_24^0'=lt_24^post10, x_13^0'=lt_24^10, k_289^0'=0, ___patmp2^0'=0, k_243^0'=0, lt_25^0'=lt_25^post10, ___patmp1^0'=k_243^0+len_263^0, len_263^0'=k_243^0+len_263^0, (-1+x_13^0-y_12^0 >= 0 /\ -1+k_243^0 >= 0 /\ -1-y_12^0+lt_24^10 >= 0 /\ len_263^0 >= 0), cost: 4*k_243^0
New rule:
l14 -> l0 : lt_34^0'=lt_34^post12, lt_24^0'=lt_24^post10, x_13^0'=lt_24^10, ___cil_tmp5_10^0'=x_8^post12, lt_26^0'=lt_26^post15, k_289^0'=0, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, ___patmp2^0'=0, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=x_8^post12, k_243^0'=0, k_139^0'=3, lt_35^0'=lt_35^post12, lt_25^0'=lt_25^post10, y_23^0'=0, ___patmp1^0'=5, lt_27^0'=lt_27^post15, len_263^0'=5, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, (1+a_11^0-y_12^0 <= 0 /\ -1-y_12^0+lt_24^10 >= 0), cost: 20

Applied chaining
First rule:
l14 -> l0 : lt_34^0'=lt_34^post12, x_13^0'=lt_26^10, ___cil_tmp5_10^0'=x_8^post12, lt_26^0'=lt_26^post15, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, ___patmp2^0'=4, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=x_8^post12, k_243^0'=4, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, ___patmp1^0'=1, lt_27^0'=lt_27^post15, len_263^0'=1, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, 1-a_11^0+y_12^0 <= 0, cost: 4
Second rule:
l0 -> l0 : lt_24^0'=lt_24^post10, x_13^0'=lt_24^10, k_289^0'=0, ___patmp2^0'=0, k_243^0'=0, lt_25^0'=lt_25^post10, ___patmp1^0'=k_243^0+len_263^0, len_263^0'=k_243^0+len_263^0, (-1-x_13^0+y_12^0 >= 0 /\ -1+y_12^0-lt_24^10 >= 0 /\ -1+k_243^0 >= 0 /\ len_263^0 >= 0), cost: 4*k_243^0
New rule:
l14 -> l0 : lt_34^0'=lt_34^post12, lt_24^0'=lt_24^post10, x_13^0'=lt_24^10, ___cil_tmp5_10^0'=x_8^post12, lt_26^0'=lt_26^post15, k_289^0'=0, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, ___patmp2^0'=0, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=x_8^post12, k_243^0'=0, k_139^0'=3, lt_35^0'=lt_35^post12, lt_25^0'=lt_25^post10, y_23^0'=0, ___patmp1^0'=5, lt_27^0'=lt_27^post15, len_263^0'=5, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, (-1+y_12^0-lt_24^10 >= 0 /\ 1-a_11^0+y_12^0 <= 0), cost: 20

Applied chaining
First rule:
l14 -> l0 : lt_34^0'=lt_34^post12, x_13^0'=lt_26^10, ___cil_tmp5_10^0'=x_8^post12, lt_26^0'=lt_26^post15, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, ___patmp2^0'=4, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=x_8^post12, k_243^0'=4, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, ___patmp1^0'=1, lt_27^0'=lt_27^post15, len_263^0'=1, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, 1+a_11^0-y_12^0 <= 0, cost: 4
Second rule:
l0 -> l0 : lt_24^0'=lt_24^post10, x_13^0'=lt_24^10, k_289^0'=0, ___patmp2^0'=0, k_243^0'=0, lt_25^0'=lt_25^post10, ___patmp1^0'=k_243^0+len_263^0, len_263^0'=k_243^0+len_263^0, (-1-x_13^0+y_12^0 >= 0 /\ -1+y_12^0-lt_24^10 >= 0 /\ -1+k_243^0 >= 0 /\ len_263^0 >= 0), cost: 4*k_243^0
New rule:
l14 -> l0 : lt_34^0'=lt_34^post12, lt_24^0'=lt_24^post10, x_13^0'=lt_24^10, ___cil_tmp5_10^0'=x_8^post12, lt_26^0'=lt_26^post15, k_289^0'=0, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, ___patmp2^0'=0, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=x_8^post12, k_243^0'=0, k_139^0'=3, lt_35^0'=lt_35^post12, lt_25^0'=lt_25^post10, y_23^0'=0, ___patmp1^0'=5, lt_27^0'=lt_27^post15, len_263^0'=5, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, (-1+y_12^0-lt_24^10 >= 0 /\ 1+a_11^0-y_12^0 <= 0), cost: 20

Applied deletion
Removed the following rules: 67 68

Chained accelerated rules with incoming rules
Start location: l14
  61: l0 -> l5 : lt_34^0'=lt_34^post0, y_20^0'=lt_32^10, t_18^0'=lt_32^10, lt_32^0'=lt_32^post0, Result_4^0'=Result_4^post0, x_19^0'=lt_32^10, (-x_13^0+y_12^0 == 0 /\ 1+w_17^0-lt_32^10 <= 0 /\ -1+k_243^0 >= 0 /\ len_263^0 >= 0), cost: 4
  62: l0 -> l5 : lt_34^0'=lt_34^post0, y_20^0'=lt_32^10, t_18^0'=lt_32^10, lt_32^0'=lt_32^post0, Result_4^0'=Result_4^post0, x_19^0'=lt_32^10, (-x_13^0+y_12^0 == 0 /\ -1+k_243^0 >= 0 /\ len_263^0 >= 0 /\ 1-w_17^0+lt_32^10 <= 0), cost: 4
  57: l5 -> [15] : -1-w_17^0+x_19^0 >= 0, cost: NONTERM
  58: l5 -> [15] : -1+w_17^0-x_19^0 >= 0, cost: NONTERM
  59: l14 -> l0 : lt_34^0'=lt_34^post12, x_13^0'=lt_26^10, ___cil_tmp5_10^0'=x_8^post12, lt_26^0'=lt_26^post15, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, ___patmp2^0'=4, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=x_8^post12, k_243^0'=4, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, ___patmp1^0'=1, lt_27^0'=lt_27^post15, len_263^0'=1, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, 1-a_11^0+y_12^0 <= 0, cost: 4
  60: l14 -> l0 : lt_34^0'=lt_34^post12, x_13^0'=lt_26^10, ___cil_tmp5_10^0'=x_8^post12, lt_26^0'=lt_26^post15, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, ___patmp2^0'=4, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=x_8^post12, k_243^0'=4, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, ___patmp1^0'=1, lt_27^0'=lt_27^post15, len_263^0'=1, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, 1+a_11^0-y_12^0 <= 0, cost: 4
  69: l14 -> l0 : lt_34^0'=lt_34^post12, lt_24^0'=lt_24^post10, x_13^0'=lt_24^10, ___cil_tmp5_10^0'=x_8^post12, lt_26^0'=lt_26^post15, k_289^0'=0, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, ___patmp2^0'=0, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=x_8^post12, k_243^0'=0, k_139^0'=3, lt_35^0'=lt_35^post12, lt_25^0'=lt_25^post10, y_23^0'=0, ___patmp1^0'=5, lt_27^0'=lt_27^post15, len_263^0'=5, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, (-1-y_12^0+lt_24^10 >= 0 /\ 1-a_11^0+y_12^0 <= 0), cost: 20
  70: l14 -> l0 : lt_34^0'=lt_34^post12, lt_24^0'=lt_24^post10, x_13^0'=lt_24^10, ___cil_tmp5_10^0'=x_8^post12, lt_26^0'=lt_26^post15, k_289^0'=0, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, ___patmp2^0'=0, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=x_8^post12, k_243^0'=0, k_139^0'=3, lt_35^0'=lt_35^post12, lt_25^0'=lt_25^post10, y_23^0'=0, ___patmp1^0'=5, lt_27^0'=lt_27^post15, len_263^0'=5, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, (1+a_11^0-y_12^0 <= 0 /\ -1-y_12^0+lt_24^10 >= 0), cost: 20
  71: l14 -> l0 : lt_34^0'=lt_34^post12, lt_24^0'=lt_24^post10, x_13^0'=lt_24^10, ___cil_tmp5_10^0'=x_8^post12, lt_26^0'=lt_26^post15, k_289^0'=0, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, ___patmp2^0'=0, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=x_8^post12, k_243^0'=0, k_139^0'=3, lt_35^0'=lt_35^post12, lt_25^0'=lt_25^post10, y_23^0'=0, ___patmp1^0'=5, lt_27^0'=lt_27^post15, len_263^0'=5, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, (-1+y_12^0-lt_24^10 >= 0 /\ 1-a_11^0+y_12^0 <= 0), cost: 20
  72: l14 -> l0 : lt_34^0'=lt_34^post12, lt_24^0'=lt_24^post10, x_13^0'=lt_24^10, ___cil_tmp5_10^0'=x_8^post12, lt_26^0'=lt_26^post15, k_289^0'=0, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, ___patmp2^0'=0, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=x_8^post12, k_243^0'=0, k_139^0'=3, lt_35^0'=lt_35^post12, lt_25^0'=lt_25^post10, y_23^0'=0, ___patmp1^0'=5, lt_27^0'=lt_27^post15, len_263^0'=5, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, (-1+y_12^0-lt_24^10 >= 0 /\ 1+a_11^0-y_12^0 <= 0), cost: 20


Eliminating location l0 by chaining:

Applied chaining
First rule:
l14 -> l0 : lt_34^0'=lt_34^post12, x_13^0'=lt_26^10, ___cil_tmp5_10^0'=x_8^post12, lt_26^0'=lt_26^post15, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, ___patmp2^0'=4, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=x_8^post12, k_243^0'=4, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, ___patmp1^0'=1, lt_27^0'=lt_27^post15, len_263^0'=1, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, 1-a_11^0+y_12^0 <= 0, cost: 4
Second rule:
l0 -> l5 : lt_34^0'=lt_34^post0, y_20^0'=lt_32^10, t_18^0'=lt_32^10, lt_32^0'=lt_32^post0, Result_4^0'=Result_4^post0, x_19^0'=lt_32^10, (-x_13^0+y_12^0 == 0 /\ 1+w_17^0-lt_32^10 <= 0 /\ -1+k_243^0 >= 0 /\ len_263^0 >= 0), cost: 4
New rule:
l14 -> l5 : lt_34^0'=lt_34^post0, y_20^0'=lt_32^10, x_13^0'=lt_26^10, ___cil_tmp5_10^0'=x_8^post12, lt_26^0'=lt_26^post15, t_18^0'=lt_32^10, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, ___patmp2^0'=4, lt_32^0'=lt_32^post0, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=Result_4^post0, k_243^0'=4, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, x_19^0'=lt_32^10, ___patmp1^0'=1, lt_27^0'=lt_27^post15, len_263^0'=1, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, (1 >= 0 /\ 3 >= 0 /\ -lt_26^10+y_12^0 == 0 /\ 1+w_17^0-lt_32^10 <= 0 /\ 1-a_11^0+y_12^0 <= 0), cost: 8

Applied simplification
Original rule:
l14 -> l5 : lt_34^0'=lt_34^post0, y_20^0'=lt_32^10, x_13^0'=lt_26^10, ___cil_tmp5_10^0'=x_8^post12, lt_26^0'=lt_26^post15, t_18^0'=lt_32^10, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, ___patmp2^0'=4, lt_32^0'=lt_32^post0, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=Result_4^post0, k_243^0'=4, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, x_19^0'=lt_32^10, ___patmp1^0'=1, lt_27^0'=lt_27^post15, len_263^0'=1, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, (1 >= 0 /\ 3 >= 0 /\ -lt_26^10+y_12^0 == 0 /\ 1+w_17^0-lt_32^10 <= 0 /\ 1-a_11^0+y_12^0 <= 0), cost: 8
New rule:
l14 -> l5 : lt_34^0'=lt_34^post0, y_20^0'=lt_32^10, x_13^0'=lt_26^10, ___cil_tmp5_10^0'=x_8^post12, lt_26^0'=lt_26^post15, t_18^0'=lt_32^10, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, ___patmp2^0'=4, lt_32^0'=lt_32^post0, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=Result_4^post0, k_243^0'=4, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, x_19^0'=lt_32^10, ___patmp1^0'=1, lt_27^0'=lt_27^post15, len_263^0'=1, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, (-lt_26^10+y_12^0 == 0 /\ 1+w_17^0-lt_32^10 <= 0 /\ 1-a_11^0+y_12^0 <= 0), cost: 8

Applied chaining
First rule:
l14 -> l0 : lt_34^0'=lt_34^post12, x_13^0'=lt_26^10, ___cil_tmp5_10^0'=x_8^post12, lt_26^0'=lt_26^post15, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, ___patmp2^0'=4, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=x_8^post12, k_243^0'=4, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, ___patmp1^0'=1, lt_27^0'=lt_27^post15, len_263^0'=1, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, 1-a_11^0+y_12^0 <= 0, cost: 4
Second rule:
l0 -> l5 : lt_34^0'=lt_34^post0, y_20^0'=lt_32^10, t_18^0'=lt_32^10, lt_32^0'=lt_32^post0, Result_4^0'=Result_4^post0, x_19^0'=lt_32^10, (-x_13^0+y_12^0 == 0 /\ -1+k_243^0 >= 0 /\ len_263^0 >= 0 /\ 1-w_17^0+lt_32^10 <= 0), cost: 4
New rule:
l14 -> l5 : lt_34^0'=lt_34^post0, y_20^0'=lt_32^10, x_13^0'=lt_26^10, ___cil_tmp5_10^0'=x_8^post12, lt_26^0'=lt_26^post15, t_18^0'=lt_32^10, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, ___patmp2^0'=4, lt_32^0'=lt_32^post0, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=Result_4^post0, k_243^0'=4, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, x_19^0'=lt_32^10, ___patmp1^0'=1, lt_27^0'=lt_27^post15, len_263^0'=1, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, (1 >= 0 /\ 3 >= 0 /\ -lt_26^10+y_12^0 == 0 /\ 1-a_11^0+y_12^0 <= 0 /\ 1-w_17^0+lt_32^10 <= 0), cost: 8

Applied simplification
Original rule:
l14 -> l5 : lt_34^0'=lt_34^post0, y_20^0'=lt_32^10, x_13^0'=lt_26^10, ___cil_tmp5_10^0'=x_8^post12, lt_26^0'=lt_26^post15, t_18^0'=lt_32^10, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, ___patmp2^0'=4, lt_32^0'=lt_32^post0, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=Result_4^post0, k_243^0'=4, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, x_19^0'=lt_32^10, ___patmp1^0'=1, lt_27^0'=lt_27^post15, len_263^0'=1, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, (1 >= 0 /\ 3 >= 0 /\ -lt_26^10+y_12^0 == 0 /\ 1-a_11^0+y_12^0 <= 0 /\ 1-w_17^0+lt_32^10 <= 0), cost: 8
New rule:
l14 -> l5 : lt_34^0'=lt_34^post0, y_20^0'=lt_32^10, x_13^0'=lt_26^10, ___cil_tmp5_10^0'=x_8^post12, lt_26^0'=lt_26^post15, t_18^0'=lt_32^10, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, ___patmp2^0'=4, lt_32^0'=lt_32^post0, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=Result_4^post0, k_243^0'=4, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, x_19^0'=lt_32^10, ___patmp1^0'=1, lt_27^0'=lt_27^post15, len_263^0'=1, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, (-lt_26^10+y_12^0 == 0 /\ 1-a_11^0+y_12^0 <= 0 /\ 1-w_17^0+lt_32^10 <= 0), cost: 8

Applied chaining
First rule:
l14 -> l0 : lt_34^0'=lt_34^post12, x_13^0'=lt_26^10, ___cil_tmp5_10^0'=x_8^post12, lt_26^0'=lt_26^post15, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, ___patmp2^0'=4, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=x_8^post12, k_243^0'=4, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, ___patmp1^0'=1, lt_27^0'=lt_27^post15, len_263^0'=1, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, 1+a_11^0-y_12^0 <= 0, cost: 4
Second rule:
l0 -> l5 : lt_34^0'=lt_34^post0, y_20^0'=lt_32^10, t_18^0'=lt_32^10, lt_32^0'=lt_32^post0, Result_4^0'=Result_4^post0, x_19^0'=lt_32^10, (-x_13^0+y_12^0 == 0 /\ 1+w_17^0-lt_32^10 <= 0 /\ -1+k_243^0 >= 0 /\ len_263^0 >= 0), cost: 4
New rule:
l14 -> l5 : lt_34^0'=lt_34^post0, y_20^0'=lt_32^10, x_13^0'=lt_26^10, ___cil_tmp5_10^0'=x_8^post12, lt_26^0'=lt_26^post15, t_18^0'=lt_32^10, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, ___patmp2^0'=4, lt_32^0'=lt_32^post0, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=Result_4^post0, k_243^0'=4, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, x_19^0'=lt_32^10, ___patmp1^0'=1, lt_27^0'=lt_27^post15, len_263^0'=1, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, (1 >= 0 /\ 3 >= 0 /\ -lt_26^10+y_12^0 == 0 /\ 1+a_11^0-y_12^0 <= 0 /\ 1+w_17^0-lt_32^10 <= 0), cost: 8

Applied simplification
Original rule:
l14 -> l5 : lt_34^0'=lt_34^post0, y_20^0'=lt_32^10, x_13^0'=lt_26^10, ___cil_tmp5_10^0'=x_8^post12, lt_26^0'=lt_26^post15, t_18^0'=lt_32^10, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, ___patmp2^0'=4, lt_32^0'=lt_32^post0, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=Result_4^post0, k_243^0'=4, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, x_19^0'=lt_32^10, ___patmp1^0'=1, lt_27^0'=lt_27^post15, len_263^0'=1, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, (1 >= 0 /\ 3 >= 0 /\ -lt_26^10+y_12^0 == 0 /\ 1+a_11^0-y_12^0 <= 0 /\ 1+w_17^0-lt_32^10 <= 0), cost: 8
New rule:
l14 -> l5 : lt_34^0'=lt_34^post0, y_20^0'=lt_32^10, x_13^0'=lt_26^10, ___cil_tmp5_10^0'=x_8^post12, lt_26^0'=lt_26^post15, t_18^0'=lt_32^10, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, ___patmp2^0'=4, lt_32^0'=lt_32^post0, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=Result_4^post0, k_243^0'=4, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, x_19^0'=lt_32^10, ___patmp1^0'=1, lt_27^0'=lt_27^post15, len_263^0'=1, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, (-lt_26^10+y_12^0 == 0 /\ 1+a_11^0-y_12^0 <= 0 /\ 1+w_17^0-lt_32^10 <= 0), cost: 8

Applied chaining
First rule:
l14 -> l0 : lt_34^0'=lt_34^post12, x_13^0'=lt_26^10, ___cil_tmp5_10^0'=x_8^post12, lt_26^0'=lt_26^post15, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, ___patmp2^0'=4, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=x_8^post12, k_243^0'=4, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, ___patmp1^0'=1, lt_27^0'=lt_27^post15, len_263^0'=1, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, 1+a_11^0-y_12^0 <= 0, cost: 4
Second rule:
l0 -> l5 : lt_34^0'=lt_34^post0, y_20^0'=lt_32^10, t_18^0'=lt_32^10, lt_32^0'=lt_32^post0, Result_4^0'=Result_4^post0, x_19^0'=lt_32^10, (-x_13^0+y_12^0 == 0 /\ -1+k_243^0 >= 0 /\ len_263^0 >= 0 /\ 1-w_17^0+lt_32^10 <= 0), cost: 4
New rule:
l14 -> l5 : lt_34^0'=lt_34^post0, y_20^0'=lt_32^10, x_13^0'=lt_26^10, ___cil_tmp5_10^0'=x_8^post12, lt_26^0'=lt_26^post15, t_18^0'=lt_32^10, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, ___patmp2^0'=4, lt_32^0'=lt_32^post0, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=Result_4^post0, k_243^0'=4, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, x_19^0'=lt_32^10, ___patmp1^0'=1, lt_27^0'=lt_27^post15, len_263^0'=1, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, (1 >= 0 /\ 3 >= 0 /\ -lt_26^10+y_12^0 == 0 /\ 1+a_11^0-y_12^0 <= 0 /\ 1-w_17^0+lt_32^10 <= 0), cost: 8

Applied simplification
Original rule:
l14 -> l5 : lt_34^0'=lt_34^post0, y_20^0'=lt_32^10, x_13^0'=lt_26^10, ___cil_tmp5_10^0'=x_8^post12, lt_26^0'=lt_26^post15, t_18^0'=lt_32^10, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, ___patmp2^0'=4, lt_32^0'=lt_32^post0, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=Result_4^post0, k_243^0'=4, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, x_19^0'=lt_32^10, ___patmp1^0'=1, lt_27^0'=lt_27^post15, len_263^0'=1, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, (1 >= 0 /\ 3 >= 0 /\ -lt_26^10+y_12^0 == 0 /\ 1+a_11^0-y_12^0 <= 0 /\ 1-w_17^0+lt_32^10 <= 0), cost: 8
New rule:
l14 -> l5 : lt_34^0'=lt_34^post0, y_20^0'=lt_32^10, x_13^0'=lt_26^10, ___cil_tmp5_10^0'=x_8^post12, lt_26^0'=lt_26^post15, t_18^0'=lt_32^10, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, ___patmp2^0'=4, lt_32^0'=lt_32^post0, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=Result_4^post0, k_243^0'=4, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, x_19^0'=lt_32^10, ___patmp1^0'=1, lt_27^0'=lt_27^post15, len_263^0'=1, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, (-lt_26^10+y_12^0 == 0 /\ 1+a_11^0-y_12^0 <= 0 /\ 1-w_17^0+lt_32^10 <= 0), cost: 8

Applied deletion
Removed the following rules: 59 60 61 62 69 70 71 72

Eliminated locations on tree-shaped paths
Start location: l14
  57: l5 -> [15] : -1-w_17^0+x_19^0 >= 0, cost: NONTERM
  58: l5 -> [15] : -1+w_17^0-x_19^0 >= 0, cost: NONTERM
  73: l14 -> l5 : lt_34^0'=lt_34^post0, y_20^0'=lt_32^10, x_13^0'=lt_26^10, ___cil_tmp5_10^0'=x_8^post12, lt_26^0'=lt_26^post15, t_18^0'=lt_32^10, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, ___patmp2^0'=4, lt_32^0'=lt_32^post0, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=Result_4^post0, k_243^0'=4, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, x_19^0'=lt_32^10, ___patmp1^0'=1, lt_27^0'=lt_27^post15, len_263^0'=1, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, (-lt_26^10+y_12^0 == 0 /\ 1+w_17^0-lt_32^10 <= 0 /\ 1-a_11^0+y_12^0 <= 0), cost: 8
  74: l14 -> l5 : lt_34^0'=lt_34^post0, y_20^0'=lt_32^10, x_13^0'=lt_26^10, ___cil_tmp5_10^0'=x_8^post12, lt_26^0'=lt_26^post15, t_18^0'=lt_32^10, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, ___patmp2^0'=4, lt_32^0'=lt_32^post0, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=Result_4^post0, k_243^0'=4, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, x_19^0'=lt_32^10, ___patmp1^0'=1, lt_27^0'=lt_27^post15, len_263^0'=1, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, (-lt_26^10+y_12^0 == 0 /\ 1-a_11^0+y_12^0 <= 0 /\ 1-w_17^0+lt_32^10 <= 0), cost: 8
  75: l14 -> l5 : lt_34^0'=lt_34^post0, y_20^0'=lt_32^10, x_13^0'=lt_26^10, ___cil_tmp5_10^0'=x_8^post12, lt_26^0'=lt_26^post15, t_18^0'=lt_32^10, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, ___patmp2^0'=4, lt_32^0'=lt_32^post0, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=Result_4^post0, k_243^0'=4, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, x_19^0'=lt_32^10, ___patmp1^0'=1, lt_27^0'=lt_27^post15, len_263^0'=1, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, (-lt_26^10+y_12^0 == 0 /\ 1+a_11^0-y_12^0 <= 0 /\ 1+w_17^0-lt_32^10 <= 0), cost: 8
  76: l14 -> l5 : lt_34^0'=lt_34^post0, y_20^0'=lt_32^10, x_13^0'=lt_26^10, ___cil_tmp5_10^0'=x_8^post12, lt_26^0'=lt_26^post15, t_18^0'=lt_32^10, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, ___patmp2^0'=4, lt_32^0'=lt_32^post0, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=Result_4^post0, k_243^0'=4, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, x_19^0'=lt_32^10, ___patmp1^0'=1, lt_27^0'=lt_27^post15, len_263^0'=1, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, (-lt_26^10+y_12^0 == 0 /\ 1+a_11^0-y_12^0 <= 0 /\ 1-w_17^0+lt_32^10 <= 0), cost: 8


Eliminating location l5 by chaining:

Applied chaining
First rule:
l14 -> l5 : lt_34^0'=lt_34^post0, y_20^0'=lt_32^10, x_13^0'=lt_26^10, ___cil_tmp5_10^0'=x_8^post12, lt_26^0'=lt_26^post15, t_18^0'=lt_32^10, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, ___patmp2^0'=4, lt_32^0'=lt_32^post0, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=Result_4^post0, k_243^0'=4, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, x_19^0'=lt_32^10, ___patmp1^0'=1, lt_27^0'=lt_27^post15, len_263^0'=1, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, (-lt_26^10+y_12^0 == 0 /\ 1+w_17^0-lt_32^10 <= 0 /\ 1-a_11^0+y_12^0 <= 0), cost: 8
Second rule:
l5 -> [15] : -1-w_17^0+x_19^0 >= 0, cost: NONTERM
New rule:
l14 -> [15] : (-1-w_17^0+lt_32^10 >= 0 /\ -lt_26^10+y_12^0 == 0 /\ 1+w_17^0-lt_32^10 <= 0 /\ 1-a_11^0+y_12^0 <= 0), cost: NONTERM

Applied simplification
Original rule:
l14 -> [15] : (-1-w_17^0+lt_32^10 >= 0 /\ -lt_26^10+y_12^0 == 0 /\ 1+w_17^0-lt_32^10 <= 0 /\ 1-a_11^0+y_12^0 <= 0), cost: NONTERM
New rule:
l14 -> [15] : (-lt_26^10+y_12^0 == 0 /\ 1+w_17^0-lt_32^10 <= 0 /\ 1-a_11^0+y_12^0 <= 0), cost: NONTERM

Applied chaining
First rule:
l14 -> l5 : lt_34^0'=lt_34^post0, y_20^0'=lt_32^10, x_13^0'=lt_26^10, ___cil_tmp5_10^0'=x_8^post12, lt_26^0'=lt_26^post15, t_18^0'=lt_32^10, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, ___patmp2^0'=4, lt_32^0'=lt_32^post0, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=Result_4^post0, k_243^0'=4, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, x_19^0'=lt_32^10, ___patmp1^0'=1, lt_27^0'=lt_27^post15, len_263^0'=1, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, (-lt_26^10+y_12^0 == 0 /\ 1-a_11^0+y_12^0 <= 0 /\ 1-w_17^0+lt_32^10 <= 0), cost: 8
Second rule:
l5 -> [15] : -1+w_17^0-x_19^0 >= 0, cost: NONTERM
New rule:
l14 -> [15] : (-1+w_17^0-lt_32^10 >= 0 /\ -lt_26^10+y_12^0 == 0 /\ 1-a_11^0+y_12^0 <= 0 /\ 1-w_17^0+lt_32^10 <= 0), cost: NONTERM

Applied simplification
Original rule:
l14 -> [15] : (-1+w_17^0-lt_32^10 >= 0 /\ -lt_26^10+y_12^0 == 0 /\ 1-a_11^0+y_12^0 <= 0 /\ 1-w_17^0+lt_32^10 <= 0), cost: NONTERM
New rule:
l14 -> [15] : (-lt_26^10+y_12^0 == 0 /\ 1-a_11^0+y_12^0 <= 0 /\ 1-w_17^0+lt_32^10 <= 0), cost: NONTERM

Applied chaining
First rule:
l14 -> l5 : lt_34^0'=lt_34^post0, y_20^0'=lt_32^10, x_13^0'=lt_26^10, ___cil_tmp5_10^0'=x_8^post12, lt_26^0'=lt_26^post15, t_18^0'=lt_32^10, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, ___patmp2^0'=4, lt_32^0'=lt_32^post0, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=Result_4^post0, k_243^0'=4, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, x_19^0'=lt_32^10, ___patmp1^0'=1, lt_27^0'=lt_27^post15, len_263^0'=1, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, (-lt_26^10+y_12^0 == 0 /\ 1+a_11^0-y_12^0 <= 0 /\ 1+w_17^0-lt_32^10 <= 0), cost: 8
Second rule:
l5 -> [15] : -1-w_17^0+x_19^0 >= 0, cost: NONTERM
New rule:
l14 -> [15] : (-1-w_17^0+lt_32^10 >= 0 /\ -lt_26^10+y_12^0 == 0 /\ 1+a_11^0-y_12^0 <= 0 /\ 1+w_17^0-lt_32^10 <= 0), cost: NONTERM

Applied simplification
Original rule:
l14 -> [15] : (-1-w_17^0+lt_32^10 >= 0 /\ -lt_26^10+y_12^0 == 0 /\ 1+a_11^0-y_12^0 <= 0 /\ 1+w_17^0-lt_32^10 <= 0), cost: NONTERM
New rule:
l14 -> [15] : (-lt_26^10+y_12^0 == 0 /\ 1+a_11^0-y_12^0 <= 0 /\ 1+w_17^0-lt_32^10 <= 0), cost: NONTERM

Applied chaining
First rule:
l14 -> l5 : lt_34^0'=lt_34^post0, y_20^0'=lt_32^10, x_13^0'=lt_26^10, ___cil_tmp5_10^0'=x_8^post12, lt_26^0'=lt_26^post15, t_18^0'=lt_32^10, lt_36^0'=lt_36^post12, x_22^0'=x_22^post12, k_187^0'=4, ___patmp2^0'=4, lt_32^0'=lt_32^post0, len_99^0'=2, lt_38^0'=lt_38^post12, Result_4^0'=Result_4^post0, k_243^0'=4, k_139^0'=3, lt_35^0'=lt_35^post12, y_23^0'=0, x_19^0'=lt_32^10, ___patmp1^0'=1, lt_27^0'=lt_27^post15, len_263^0'=1, tmp_9^0'=x_8^post12, lt_37^0'=lt_37^post12, x_8^0'=x_8^post12, k_208^0'=4, (-lt_26^10+y_12^0 == 0 /\ 1+a_11^0-y_12^0 <= 0 /\ 1-w_17^0+lt_32^10 <= 0), cost: 8
Second rule:
l5 -> [15] : -1+w_17^0-x_19^0 >= 0, cost: NONTERM
New rule:
l14 -> [15] : (-1+w_17^0-lt_32^10 >= 0 /\ -lt_26^10+y_12^0 == 0 /\ 1+a_11^0-y_12^0 <= 0 /\ 1-w_17^0+lt_32^10 <= 0), cost: NONTERM

Applied simplification
Original rule:
l14 -> [15] : (-1+w_17^0-lt_32^10 >= 0 /\ -lt_26^10+y_12^0 == 0 /\ 1+a_11^0-y_12^0 <= 0 /\ 1-w_17^0+lt_32^10 <= 0), cost: NONTERM
New rule:
l14 -> [15] : (-lt_26^10+y_12^0 == 0 /\ 1+a_11^0-y_12^0 <= 0 /\ 1-w_17^0+lt_32^10 <= 0), cost: NONTERM

Applied deletion
Removed the following rules: 57 58 73 74 75 76

Eliminated locations on tree-shaped paths
Start location: l14
  77: l14 -> [15] : (-lt_26^10+y_12^0 == 0 /\ 1+w_17^0-lt_32^10 <= 0 /\ 1-a_11^0+y_12^0 <= 0), cost: NONTERM
  78: l14 -> [15] : (-lt_26^10+y_12^0 == 0 /\ 1-a_11^0+y_12^0 <= 0 /\ 1-w_17^0+lt_32^10 <= 0), cost: NONTERM
  79: l14 -> [15] : (-lt_26^10+y_12^0 == 0 /\ 1+a_11^0-y_12^0 <= 0 /\ 1+w_17^0-lt_32^10 <= 0), cost: NONTERM
  80: l14 -> [15] : (-lt_26^10+y_12^0 == 0 /\ 1+a_11^0-y_12^0 <= 0 /\ 1-w_17^0+lt_32^10 <= 0), cost: NONTERM


Computing asymptotic complexity
Proved nontermination of rule 77 via SMT.

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

Solved cost: NONTERM
Rule cost:   NONTERM
Rule guard:  (-lt_26^10+y_12^0 == 0 /\ 1+w_17^0-lt_32^10 <= 0 /\ 1-a_11^0+y_12^0 <= 0)