NO

Initial ITS
Start location: l11
   0: l0 -> l1 : a_140^0'=a_140^post0, t_17^0'=t_17^post0, __cil_tmp6_15^0'=__cil_tmp6_15^post0, tmp_20^0'=tmp_20^post0, length_10^0'=length_10^post0, head_12^0'=head_12^post0, __disjvr_1^0'=__disjvr_1^post0, x_18^0'=x_18^post0, lt_21^0'=lt_21^post0, Result_4^0'=Result_4^post0, len_47^0'=len_47^post0, a_16^0'=a_16^post0, tmp_13^0'=tmp_13^post0, __disjvr_0^0'=__disjvr_0^post0, tmp___0_14^0'=tmp___0_14^post0, length_19^0'=length_19^post0, i_11^0'=i_11^post0, (0 == 0 /\ -tmp___0_14^post0+tmp___0_14^0 == 0 /\ -__disjvr_1^post0+__disjvr_1^0 == 0 /\ lt_21^0-lt_21^post0 == 0 /\ t_17^0-t_17^post0 == 0 /\ __disjvr_0^0-__disjvr_0^post0 == 0 /\ -len_47^post0+len_47^0 == 0 /\ -x_18^post0+x_18^0 == 0 /\ -a_16^post0+a_16^0 == 0 /\ tmp_13^0-tmp_13^post0 == 0 /\ Result_4^0-Result_4^post0 == 0 /\ length_10^0-length_10^post0 == 0 /\ head_12^post0 == 0 /\ i_11^post0 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post0 == 0 /\ a_140^0-a_140^post0 == 0 /\ -tmp_20^post0+tmp_20^0 == 0), cost: 1
   1: l1 -> l2 : a_140^0'=a_140^post1, t_17^0'=t_17^post1, __cil_tmp6_15^0'=__cil_tmp6_15^post1, tmp_20^0'=tmp_20^post1, length_10^0'=length_10^post1, head_12^0'=head_12^post1, __disjvr_1^0'=__disjvr_1^post1, x_18^0'=x_18^post1, lt_21^0'=lt_21^post1, Result_4^0'=Result_4^post1, len_47^0'=len_47^post1, a_16^0'=a_16^post1, tmp_13^0'=tmp_13^post1, __disjvr_0^0'=__disjvr_0^post1, tmp___0_14^0'=tmp___0_14^post1, length_19^0'=length_19^post1, i_11^0'=i_11^post1, (0 == 0 /\ tmp_20^0-tmp_20^post1 == 0 /\ a_140^0-a_140^post1 == 0 /\ -1+i_11^post1-i_11^0 == 0 /\ -length_19^post1+length_19^0 == 0 /\ Result_4^0-Result_4^post1 == 0 /\ length_10^0-length_10^post1 == 0 /\ -__disjvr_1^post1+__disjvr_1^0 == 0 /\ tmp_13^post1-tmp___0_14^post1 == 0 /\ -tmp_13^post1+head_12^post1 == 0 /\ x_18^0-x_18^post1 == 0 /\ a_16^0-a_16^post1 == 0 /\ 2-length_10^0+i_11^0 <= 0 /\ -len_47^post1+len_47^0 == 0 /\ -__disjvr_0^post1+__disjvr_0^0 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post1 == 0 /\ t_17^0-t_17^post1 == 0 /\ lt_21^0-lt_21^post1 == 0), cost: 1
   2: l1 -> l3 : a_140^0'=a_140^post2, t_17^0'=t_17^post2, __cil_tmp6_15^0'=__cil_tmp6_15^post2, tmp_20^0'=tmp_20^post2, length_10^0'=length_10^post2, head_12^0'=head_12^post2, __disjvr_1^0'=__disjvr_1^post2, x_18^0'=x_18^post2, lt_21^0'=lt_21^post2, Result_4^0'=Result_4^post2, len_47^0'=len_47^post2, a_16^0'=a_16^post2, tmp_13^0'=tmp_13^post2, __disjvr_0^0'=__disjvr_0^post2, tmp___0_14^0'=tmp___0_14^post2, length_19^0'=length_19^post2, i_11^0'=i_11^post2, (0 == 0 /\ len_47^0-len_47^post2 == 0 /\ lt_21^0-lt_21^post2 == 0 /\ -__disjvr_0^post2+__disjvr_0^0 == 0 /\ -__cil_tmp6_15^post2+Result_4^10 == 0 /\ -tmp_13^post2+tmp_13^0 == 0 /\ -x_18^post2 <= 0 /\ tmp_20^post2-Result_4^10 == 0 /\ length_10^0-length_10^post2 == 0 /\ t_17^0-t_17^post2 == 0 /\ -1+length_10^0-i_11^0 <= 0 /\ x_18^post2-a_16^0 == 0 /\ -__disjvr_1^post2+__disjvr_1^0 == 0 /\ x_18^post2 <= 0 /\ -length_19^post2+length_19^0 == 0 /\ -i_11^post2+i_11^0 == 0 /\ head_12^0-head_12^post2 == 0 /\ -a_16^post2+a_16^0 == 0 /\ -tmp___0_14^post2+tmp___0_14^0 == 0 /\ -head_12^0+__cil_tmp6_15^post2 == 0 /\ a_140^0-a_140^post2 == 0), cost: 1
   3: l2 -> l4 : a_140^0'=a_140^post3, t_17^0'=t_17^post3, __cil_tmp6_15^0'=__cil_tmp6_15^post3, tmp_20^0'=tmp_20^post3, length_10^0'=length_10^post3, head_12^0'=head_12^post3, __disjvr_1^0'=__disjvr_1^post3, x_18^0'=x_18^post3, lt_21^0'=lt_21^post3, Result_4^0'=Result_4^post3, len_47^0'=len_47^post3, a_16^0'=a_16^post3, tmp_13^0'=tmp_13^post3, __disjvr_0^0'=__disjvr_0^post3, tmp___0_14^0'=tmp___0_14^post3, length_19^0'=length_19^post3, i_11^0'=i_11^post3, (0 == 0 /\ -1+i_11^post3-i_11^0 == 0 /\ -lt_21^post3+lt_21^0 == 0 /\ t_17^0-t_17^post3 == 0 /\ a_140^0-a_140^post3 == 0 /\ length_19^0-length_19^post3 == 0 /\ tmp_20^0-tmp_20^post3 == 0 /\ -__disjvr_0^post3+__disjvr_0^0 == 0 /\ head_12^post3-tmp_13^post3 == 0 /\ 2-length_10^0+i_11^0 <= 0 /\ __disjvr_1^0-__disjvr_1^post3 == 0 /\ a_16^0-a_16^post3 == 0 /\ length_10^0-length_10^post3 == 0 /\ x_18^0-x_18^post3 == 0 /\ len_47^0-len_47^post3 == 0 /\ tmp_13^post3-tmp___0_14^post3 == 0 /\ -Result_4^post3+Result_4^0 == 0 /\ -len_47^0 <= 0 /\ -__cil_tmp6_15^post3+__cil_tmp6_15^0 == 0), cost: 1
   5: l2 -> l6 : a_140^0'=a_140^post5, t_17^0'=t_17^post5, __cil_tmp6_15^0'=__cil_tmp6_15^post5, tmp_20^0'=tmp_20^post5, length_10^0'=length_10^post5, head_12^0'=head_12^post5, __disjvr_1^0'=__disjvr_1^post5, x_18^0'=x_18^post5, lt_21^0'=lt_21^post5, Result_4^0'=Result_4^post5, len_47^0'=len_47^post5, a_16^0'=a_16^post5, tmp_13^0'=tmp_13^post5, __disjvr_0^0'=__disjvr_0^post5, tmp___0_14^0'=tmp___0_14^post5, length_19^0'=length_19^post5, i_11^0'=i_11^post5, (0 == 0 /\ -tmp___0_14^post5+tmp___0_14^0 == 0 /\ -__disjvr_1^post5+__disjvr_1^0 == 0 /\ length_10^0-length_10^post5 == 0 /\ a_140^0-a_140^post5 == 0 /\ -1+length_10^0-i_11^0 <= 0 /\ -a_16^post5+a_16^0 == 0 /\ __cil_tmp6_15^post5-head_12^0 == 0 /\ -Result_4^11+tmp_20^post5 == 0 /\ -len_47^post5+len_47^0 == 0 /\ x_18^post5-a_16^0 == 0 /\ lt_21^0-lt_21^post5 == 0 /\ -__disjvr_0^post5+__disjvr_0^0 == 0 /\ t_17^0-t_17^post5 == 0 /\ -length_19^post5+length_19^0 == 0 /\ -__cil_tmp6_15^post5+Result_4^11 == 0 /\ -i_11^post5+i_11^0 == 0 /\ head_12^0-head_12^post5 == 0 /\ -len_47^0 <= 0 /\ tmp_13^0-tmp_13^post5 == 0), cost: 1
   4: l4 -> l2 : a_140^0'=a_140^post4, t_17^0'=t_17^post4, __cil_tmp6_15^0'=__cil_tmp6_15^post4, tmp_20^0'=tmp_20^post4, length_10^0'=length_10^post4, head_12^0'=head_12^post4, __disjvr_1^0'=__disjvr_1^post4, x_18^0'=x_18^post4, lt_21^0'=lt_21^post4, Result_4^0'=Result_4^post4, len_47^0'=len_47^post4, a_16^0'=a_16^post4, tmp_13^0'=tmp_13^post4, __disjvr_0^0'=__disjvr_0^post4, tmp___0_14^0'=tmp___0_14^post4, length_19^0'=length_19^post4, i_11^0'=i_11^post4, (tmp___0_14^0-tmp___0_14^post4 == 0 /\ len_47^0-len_47^post4 == 0 /\ __disjvr_1^0-__disjvr_1^post4 == 0 /\ a_140^0-a_140^post4 == 0 /\ tmp_20^0-tmp_20^post4 == 0 /\ -tmp_13^post4+tmp_13^0 == 0 /\ -i_11^post4+i_11^0 == 0 /\ -head_12^post4+head_12^0 == 0 /\ -__disjvr_0^post4+__disjvr_0^0 == 0 /\ length_10^0-length_10^post4 == 0 /\ x_18^0-x_18^post4 == 0 /\ t_17^0-t_17^post4 == 0 /\ -length_19^post4+length_19^0 == 0 /\ -Result_4^post4+Result_4^0 == 0 /\ -a_16^post4+a_16^0 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post4 == 0 /\ -lt_21^post4+lt_21^0 == 0), cost: 1
   6: l6 -> l7 : a_140^0'=a_140^post6, t_17^0'=t_17^post6, __cil_tmp6_15^0'=__cil_tmp6_15^post6, tmp_20^0'=tmp_20^post6, length_10^0'=length_10^post6, head_12^0'=head_12^post6, __disjvr_1^0'=__disjvr_1^post6, x_18^0'=x_18^post6, lt_21^0'=lt_21^post6, Result_4^0'=Result_4^post6, len_47^0'=len_47^post6, a_16^0'=a_16^post6, tmp_13^0'=tmp_13^post6, __disjvr_0^0'=__disjvr_0^post6, tmp___0_14^0'=tmp___0_14^post6, length_19^0'=length_19^post6, i_11^0'=i_11^post6, (x_18^0-x_18^post6 == 0 /\ -lt_21^post6+lt_21^0 == 0 /\ -__cil_tmp6_15^post6+__cil_tmp6_15^0 == 0 /\ -tmp_13^post6+tmp_13^0 == 0 /\ -head_12^post6+head_12^0 == 0 /\ -i_11^post6+i_11^0 == 0 /\ -length_19^post6+length_19^0 == 0 /\ -Result_4^post6+Result_4^0 == 0 /\ t_17^0-t_17^post6 == 0 /\ len_47^0-len_47^post6 == 0 /\ -tmp___0_14^post6+tmp___0_14^0 == 0 /\ -__disjvr_1^post6+__disjvr_1^0 == 0 /\ tmp_20^0-tmp_20^post6 == 0 /\ a_140^0-a_140^post6 == 0 /\ __disjvr_0^post6-__disjvr_0^0 == 0 /\ length_10^0-length_10^post6 == 0 /\ -a_16^post6+a_16^0 == 0 /\ -__disjvr_0^post6+__disjvr_0^0 == 0), cost: 1
   7: l7 -> l5 : a_140^0'=a_140^post7, t_17^0'=t_17^post7, __cil_tmp6_15^0'=__cil_tmp6_15^post7, tmp_20^0'=tmp_20^post7, length_10^0'=length_10^post7, head_12^0'=head_12^post7, __disjvr_1^0'=__disjvr_1^post7, x_18^0'=x_18^post7, lt_21^0'=lt_21^post7, Result_4^0'=Result_4^post7, len_47^0'=len_47^post7, a_16^0'=a_16^post7, tmp_13^0'=tmp_13^post7, __disjvr_0^0'=__disjvr_0^post7, tmp___0_14^0'=tmp___0_14^post7, length_19^0'=length_19^post7, i_11^0'=i_11^post7, (0 == 0 /\ tmp___0_14^0-tmp___0_14^post7 == 0 /\ a_140^0-a_140^post7 == 0 /\ -i_11^post7+i_11^0 == 0 /\ __disjvr_1^0-__disjvr_1^post7 == 0 /\ Result_4^0-Result_4^post7 == 0 /\ -length_19^post7+length_19^0 == 0 /\ a_16^0-a_16^post7 == 0 /\ -tmp_13^post7+tmp_13^0 == 0 /\ x_18^post7-lt_21^10 == 0 /\ -len_47^post7+len_47^0 == 0 /\ head_12^0-head_12^post7 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post7 == 0 /\ tmp_20^0-tmp_20^post7 == 0 /\ -__disjvr_0^post7+__disjvr_0^0 == 0 /\ t_17^post7-x_18^0 == 0 /\ -length_10^post7+length_10^0 == 0), cost: 1
   8: l5 -> l3 : a_140^0'=a_140^post8, t_17^0'=t_17^post8, __cil_tmp6_15^0'=__cil_tmp6_15^post8, tmp_20^0'=tmp_20^post8, length_10^0'=length_10^post8, head_12^0'=head_12^post8, __disjvr_1^0'=__disjvr_1^post8, x_18^0'=x_18^post8, lt_21^0'=lt_21^post8, Result_4^0'=Result_4^post8, len_47^0'=len_47^post8, a_16^0'=a_16^post8, tmp_13^0'=tmp_13^post8, __disjvr_0^0'=__disjvr_0^post8, tmp___0_14^0'=tmp___0_14^post8, length_19^0'=length_19^post8, i_11^0'=i_11^post8, (0 == 0 /\ -len_47^post8+len_47^0 == 0 /\ -tmp___0_14^post8+tmp___0_14^0 == 0 /\ tmp_20^0-tmp_20^post8 == 0 /\ -a_16^post8+a_16^0 == 0 /\ a_140^0-a_140^post8 == 0 /\ -x_18^0 <= 0 /\ length_10^0-length_10^post8 == 0 /\ x_18^0 <= 0 /\ -__disjvr_1^post8+__disjvr_1^0 == 0 /\ tmp_13^0-tmp_13^post8 == 0 /\ x_18^0-x_18^post8 == 0 /\ -__disjvr_0^post8+__disjvr_0^0 == 0 /\ head_12^0-head_12^post8 == 0 /\ -a_140^0 <= 0 /\ -i_11^post8+i_11^0 == 0 /\ -length_19^post8+length_19^0 == 0 /\ lt_21^0-lt_21^post8 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post8 == 0 /\ t_17^0-t_17^post8 == 0), cost: 1
   9: l5 -> l9 : a_140^0'=a_140^post9, t_17^0'=t_17^post9, __cil_tmp6_15^0'=__cil_tmp6_15^post9, tmp_20^0'=tmp_20^post9, length_10^0'=length_10^post9, head_12^0'=head_12^post9, __disjvr_1^0'=__disjvr_1^post9, x_18^0'=x_18^post9, lt_21^0'=lt_21^post9, Result_4^0'=Result_4^post9, len_47^0'=len_47^post9, a_16^0'=a_16^post9, tmp_13^0'=tmp_13^post9, __disjvr_0^0'=__disjvr_0^post9, tmp___0_14^0'=tmp___0_14^post9, length_19^0'=length_19^post9, i_11^0'=i_11^post9, (__disjvr_1^0-__disjvr_1^post9 == 0 /\ t_17^0-t_17^post9 == 0 /\ -length_19^post9+length_19^0 == 0 /\ -i_11^post9+i_11^0 == 0 /\ -tmp_13^post9+tmp_13^0 == 0 /\ len_47^0-len_47^post9 == 0 /\ tmp_20^0-tmp_20^post9 == 0 /\ -tmp___0_14^post9+tmp___0_14^0 == 0 /\ -Result_4^post9+Result_4^0 == 0 /\ length_10^0-length_10^post9 == 0 /\ -lt_21^post9+lt_21^0 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post9 == 0 /\ -head_12^post9+head_12^0 == 0 /\ -a_140^0 <= 0 /\ -a_16^post9+a_16^0 == 0 /\ a_140^0-a_140^post9 == 0 /\ x_18^0-x_18^post9 == 0 /\ -__disjvr_0^post9+__disjvr_0^0 == 0), cost: 1
  10: l9 -> l10 : a_140^0'=a_140^post10, t_17^0'=t_17^post10, __cil_tmp6_15^0'=__cil_tmp6_15^post10, tmp_20^0'=tmp_20^post10, length_10^0'=length_10^post10, head_12^0'=head_12^post10, __disjvr_1^0'=__disjvr_1^post10, x_18^0'=x_18^post10, lt_21^0'=lt_21^post10, Result_4^0'=Result_4^post10, len_47^0'=len_47^post10, a_16^0'=a_16^post10, tmp_13^0'=tmp_13^post10, __disjvr_0^0'=__disjvr_0^post10, tmp___0_14^0'=tmp___0_14^post10, length_19^0'=length_19^post10, i_11^0'=i_11^post10, (tmp___0_14^0-tmp___0_14^post10 == 0 /\ tmp_13^0-tmp_13^post10 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post10 == 0 /\ -length_10^post10+length_10^0 == 0 /\ -length_19^post10+length_19^0 == 0 /\ -i_11^post10+i_11^0 == 0 /\ -Result_4^post10+Result_4^0 == 0 /\ -x_18^post10+x_18^0 == 0 /\ a_140^0-a_140^post10 == 0 /\ lt_21^0-lt_21^post10 == 0 /\ __disjvr_1^0-__disjvr_1^post10 == 0 /\ t_17^0-t_17^post10 == 0 /\ -len_47^post10+len_47^0 == 0 /\ -__disjvr_1^0+__disjvr_1^post10 == 0 /\ head_12^0-head_12^post10 == 0 /\ -a_16^post10+a_16^0 == 0 /\ tmp_20^0-tmp_20^post10 == 0 /\ -__disjvr_0^post10+__disjvr_0^0 == 0), cost: 1
  11: l10 -> l8 : a_140^0'=a_140^post11, t_17^0'=t_17^post11, __cil_tmp6_15^0'=__cil_tmp6_15^post11, tmp_20^0'=tmp_20^post11, length_10^0'=length_10^post11, head_12^0'=head_12^post11, __disjvr_1^0'=__disjvr_1^post11, x_18^0'=x_18^post11, lt_21^0'=lt_21^post11, Result_4^0'=Result_4^post11, len_47^0'=len_47^post11, a_16^0'=a_16^post11, tmp_13^0'=tmp_13^post11, __disjvr_0^0'=__disjvr_0^post11, tmp___0_14^0'=tmp___0_14^post11, length_19^0'=length_19^post11, i_11^0'=i_11^post11, (0 == 0 /\ length_19^0-length_19^post11 == 0 /\ -i_11^post11+i_11^0 == 0 /\ Result_4^0-Result_4^post11 == 0 /\ -__disjvr_1^post11+__disjvr_1^0 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post11 == 0 /\ -len_47^post11+len_47^0 == 0 /\ tmp_20^0-tmp_20^post11 == 0 /\ a_16^0-a_16^post11 == 0 /\ -__disjvr_0^post11+__disjvr_0^0 == 0 /\ -head_12^post11+head_12^0 == 0 /\ a_140^0-a_140^post11 == 0 /\ -tmp_13^post11+tmp_13^0 == 0 /\ length_10^0-length_10^post11 == 0 /\ -x_18^0+t_17^post11 == 0 /\ -lt_21^11+x_18^post11 == 0 /\ -tmp___0_14^post11+tmp___0_14^0 == 0), cost: 1
  12: l8 -> l5 : a_140^0'=a_140^post12, t_17^0'=t_17^post12, __cil_tmp6_15^0'=__cil_tmp6_15^post12, tmp_20^0'=tmp_20^post12, length_10^0'=length_10^post12, head_12^0'=head_12^post12, __disjvr_1^0'=__disjvr_1^post12, x_18^0'=x_18^post12, lt_21^0'=lt_21^post12, Result_4^0'=Result_4^post12, len_47^0'=len_47^post12, a_16^0'=a_16^post12, tmp_13^0'=tmp_13^post12, __disjvr_0^0'=__disjvr_0^post12, tmp___0_14^0'=tmp___0_14^post12, length_19^0'=length_19^post12, i_11^0'=i_11^post12, (-lt_21^post12+lt_21^0 == 0 /\ -length_19^post12+length_19^0 == 0 /\ tmp_20^0-tmp_20^post12 == 0 /\ -Result_4^post12+Result_4^0 == 0 /\ -a_16^post12+a_16^0 == 0 /\ -tmp___0_14^post12+tmp___0_14^0 == 0 /\ len_47^0-len_47^post12 == 0 /\ __disjvr_1^0-__disjvr_1^post12 == 0 /\ length_10^0-length_10^post12 == 0 /\ -head_12^post12+head_12^0 == 0 /\ -tmp_13^post12+tmp_13^0 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post12 == 0 /\ -i_11^post12+i_11^0 == 0 /\ x_18^0-x_18^post12 == 0 /\ -__disjvr_0^post12+__disjvr_0^0 == 0 /\ a_140^0-a_140^post12 == 0 /\ -t_17^post12+t_17^0 == 0), cost: 1
  13: l11 -> l0 : a_140^0'=a_140^post13, t_17^0'=t_17^post13, __cil_tmp6_15^0'=__cil_tmp6_15^post13, tmp_20^0'=tmp_20^post13, length_10^0'=length_10^post13, head_12^0'=head_12^post13, __disjvr_1^0'=__disjvr_1^post13, x_18^0'=x_18^post13, lt_21^0'=lt_21^post13, Result_4^0'=Result_4^post13, len_47^0'=len_47^post13, a_16^0'=a_16^post13, tmp_13^0'=tmp_13^post13, __disjvr_0^0'=__disjvr_0^post13, tmp___0_14^0'=tmp___0_14^post13, length_19^0'=length_19^post13, i_11^0'=i_11^post13, (head_12^0-head_12^post13 == 0 /\ t_17^0-t_17^post13 == 0 /\ -len_47^post13+len_47^0 == 0 /\ __disjvr_0^0-__disjvr_0^post13 == 0 /\ -i_11^post13+i_11^0 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post13 == 0 /\ -length_10^post13+length_10^0 == 0 /\ Result_4^0-Result_4^post13 == 0 /\ tmp_13^0-tmp_13^post13 == 0 /\ __disjvr_1^0-__disjvr_1^post13 == 0 /\ a_140^0-a_140^post13 == 0 /\ -tmp_20^post13+tmp_20^0 == 0 /\ -length_19^post13+length_19^0 == 0 /\ -x_18^post13+x_18^0 == 0 /\ -a_16^post13+a_16^0 == 0 /\ -tmp___0_14^post13+tmp___0_14^0 == 0 /\ -lt_21^post13+lt_21^0 == 0), cost: 1


Removed unreachable rules and leafs
Start location: l11
   0: l0 -> l1 : a_140^0'=a_140^post0, t_17^0'=t_17^post0, __cil_tmp6_15^0'=__cil_tmp6_15^post0, tmp_20^0'=tmp_20^post0, length_10^0'=length_10^post0, head_12^0'=head_12^post0, __disjvr_1^0'=__disjvr_1^post0, x_18^0'=x_18^post0, lt_21^0'=lt_21^post0, Result_4^0'=Result_4^post0, len_47^0'=len_47^post0, a_16^0'=a_16^post0, tmp_13^0'=tmp_13^post0, __disjvr_0^0'=__disjvr_0^post0, tmp___0_14^0'=tmp___0_14^post0, length_19^0'=length_19^post0, i_11^0'=i_11^post0, (0 == 0 /\ -tmp___0_14^post0+tmp___0_14^0 == 0 /\ -__disjvr_1^post0+__disjvr_1^0 == 0 /\ lt_21^0-lt_21^post0 == 0 /\ t_17^0-t_17^post0 == 0 /\ __disjvr_0^0-__disjvr_0^post0 == 0 /\ -len_47^post0+len_47^0 == 0 /\ -x_18^post0+x_18^0 == 0 /\ -a_16^post0+a_16^0 == 0 /\ tmp_13^0-tmp_13^post0 == 0 /\ Result_4^0-Result_4^post0 == 0 /\ length_10^0-length_10^post0 == 0 /\ head_12^post0 == 0 /\ i_11^post0 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post0 == 0 /\ a_140^0-a_140^post0 == 0 /\ -tmp_20^post0+tmp_20^0 == 0), cost: 1
   1: l1 -> l2 : a_140^0'=a_140^post1, t_17^0'=t_17^post1, __cil_tmp6_15^0'=__cil_tmp6_15^post1, tmp_20^0'=tmp_20^post1, length_10^0'=length_10^post1, head_12^0'=head_12^post1, __disjvr_1^0'=__disjvr_1^post1, x_18^0'=x_18^post1, lt_21^0'=lt_21^post1, Result_4^0'=Result_4^post1, len_47^0'=len_47^post1, a_16^0'=a_16^post1, tmp_13^0'=tmp_13^post1, __disjvr_0^0'=__disjvr_0^post1, tmp___0_14^0'=tmp___0_14^post1, length_19^0'=length_19^post1, i_11^0'=i_11^post1, (0 == 0 /\ tmp_20^0-tmp_20^post1 == 0 /\ a_140^0-a_140^post1 == 0 /\ -1+i_11^post1-i_11^0 == 0 /\ -length_19^post1+length_19^0 == 0 /\ Result_4^0-Result_4^post1 == 0 /\ length_10^0-length_10^post1 == 0 /\ -__disjvr_1^post1+__disjvr_1^0 == 0 /\ tmp_13^post1-tmp___0_14^post1 == 0 /\ -tmp_13^post1+head_12^post1 == 0 /\ x_18^0-x_18^post1 == 0 /\ a_16^0-a_16^post1 == 0 /\ 2-length_10^0+i_11^0 <= 0 /\ -len_47^post1+len_47^0 == 0 /\ -__disjvr_0^post1+__disjvr_0^0 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post1 == 0 /\ t_17^0-t_17^post1 == 0 /\ lt_21^0-lt_21^post1 == 0), cost: 1
   3: l2 -> l4 : a_140^0'=a_140^post3, t_17^0'=t_17^post3, __cil_tmp6_15^0'=__cil_tmp6_15^post3, tmp_20^0'=tmp_20^post3, length_10^0'=length_10^post3, head_12^0'=head_12^post3, __disjvr_1^0'=__disjvr_1^post3, x_18^0'=x_18^post3, lt_21^0'=lt_21^post3, Result_4^0'=Result_4^post3, len_47^0'=len_47^post3, a_16^0'=a_16^post3, tmp_13^0'=tmp_13^post3, __disjvr_0^0'=__disjvr_0^post3, tmp___0_14^0'=tmp___0_14^post3, length_19^0'=length_19^post3, i_11^0'=i_11^post3, (0 == 0 /\ -1+i_11^post3-i_11^0 == 0 /\ -lt_21^post3+lt_21^0 == 0 /\ t_17^0-t_17^post3 == 0 /\ a_140^0-a_140^post3 == 0 /\ length_19^0-length_19^post3 == 0 /\ tmp_20^0-tmp_20^post3 == 0 /\ -__disjvr_0^post3+__disjvr_0^0 == 0 /\ head_12^post3-tmp_13^post3 == 0 /\ 2-length_10^0+i_11^0 <= 0 /\ __disjvr_1^0-__disjvr_1^post3 == 0 /\ a_16^0-a_16^post3 == 0 /\ length_10^0-length_10^post3 == 0 /\ x_18^0-x_18^post3 == 0 /\ len_47^0-len_47^post3 == 0 /\ tmp_13^post3-tmp___0_14^post3 == 0 /\ -Result_4^post3+Result_4^0 == 0 /\ -len_47^0 <= 0 /\ -__cil_tmp6_15^post3+__cil_tmp6_15^0 == 0), cost: 1
   5: l2 -> l6 : a_140^0'=a_140^post5, t_17^0'=t_17^post5, __cil_tmp6_15^0'=__cil_tmp6_15^post5, tmp_20^0'=tmp_20^post5, length_10^0'=length_10^post5, head_12^0'=head_12^post5, __disjvr_1^0'=__disjvr_1^post5, x_18^0'=x_18^post5, lt_21^0'=lt_21^post5, Result_4^0'=Result_4^post5, len_47^0'=len_47^post5, a_16^0'=a_16^post5, tmp_13^0'=tmp_13^post5, __disjvr_0^0'=__disjvr_0^post5, tmp___0_14^0'=tmp___0_14^post5, length_19^0'=length_19^post5, i_11^0'=i_11^post5, (0 == 0 /\ -tmp___0_14^post5+tmp___0_14^0 == 0 /\ -__disjvr_1^post5+__disjvr_1^0 == 0 /\ length_10^0-length_10^post5 == 0 /\ a_140^0-a_140^post5 == 0 /\ -1+length_10^0-i_11^0 <= 0 /\ -a_16^post5+a_16^0 == 0 /\ __cil_tmp6_15^post5-head_12^0 == 0 /\ -Result_4^11+tmp_20^post5 == 0 /\ -len_47^post5+len_47^0 == 0 /\ x_18^post5-a_16^0 == 0 /\ lt_21^0-lt_21^post5 == 0 /\ -__disjvr_0^post5+__disjvr_0^0 == 0 /\ t_17^0-t_17^post5 == 0 /\ -length_19^post5+length_19^0 == 0 /\ -__cil_tmp6_15^post5+Result_4^11 == 0 /\ -i_11^post5+i_11^0 == 0 /\ head_12^0-head_12^post5 == 0 /\ -len_47^0 <= 0 /\ tmp_13^0-tmp_13^post5 == 0), cost: 1
   4: l4 -> l2 : a_140^0'=a_140^post4, t_17^0'=t_17^post4, __cil_tmp6_15^0'=__cil_tmp6_15^post4, tmp_20^0'=tmp_20^post4, length_10^0'=length_10^post4, head_12^0'=head_12^post4, __disjvr_1^0'=__disjvr_1^post4, x_18^0'=x_18^post4, lt_21^0'=lt_21^post4, Result_4^0'=Result_4^post4, len_47^0'=len_47^post4, a_16^0'=a_16^post4, tmp_13^0'=tmp_13^post4, __disjvr_0^0'=__disjvr_0^post4, tmp___0_14^0'=tmp___0_14^post4, length_19^0'=length_19^post4, i_11^0'=i_11^post4, (tmp___0_14^0-tmp___0_14^post4 == 0 /\ len_47^0-len_47^post4 == 0 /\ __disjvr_1^0-__disjvr_1^post4 == 0 /\ a_140^0-a_140^post4 == 0 /\ tmp_20^0-tmp_20^post4 == 0 /\ -tmp_13^post4+tmp_13^0 == 0 /\ -i_11^post4+i_11^0 == 0 /\ -head_12^post4+head_12^0 == 0 /\ -__disjvr_0^post4+__disjvr_0^0 == 0 /\ length_10^0-length_10^post4 == 0 /\ x_18^0-x_18^post4 == 0 /\ t_17^0-t_17^post4 == 0 /\ -length_19^post4+length_19^0 == 0 /\ -Result_4^post4+Result_4^0 == 0 /\ -a_16^post4+a_16^0 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post4 == 0 /\ -lt_21^post4+lt_21^0 == 0), cost: 1
   6: l6 -> l7 : a_140^0'=a_140^post6, t_17^0'=t_17^post6, __cil_tmp6_15^0'=__cil_tmp6_15^post6, tmp_20^0'=tmp_20^post6, length_10^0'=length_10^post6, head_12^0'=head_12^post6, __disjvr_1^0'=__disjvr_1^post6, x_18^0'=x_18^post6, lt_21^0'=lt_21^post6, Result_4^0'=Result_4^post6, len_47^0'=len_47^post6, a_16^0'=a_16^post6, tmp_13^0'=tmp_13^post6, __disjvr_0^0'=__disjvr_0^post6, tmp___0_14^0'=tmp___0_14^post6, length_19^0'=length_19^post6, i_11^0'=i_11^post6, (x_18^0-x_18^post6 == 0 /\ -lt_21^post6+lt_21^0 == 0 /\ -__cil_tmp6_15^post6+__cil_tmp6_15^0 == 0 /\ -tmp_13^post6+tmp_13^0 == 0 /\ -head_12^post6+head_12^0 == 0 /\ -i_11^post6+i_11^0 == 0 /\ -length_19^post6+length_19^0 == 0 /\ -Result_4^post6+Result_4^0 == 0 /\ t_17^0-t_17^post6 == 0 /\ len_47^0-len_47^post6 == 0 /\ -tmp___0_14^post6+tmp___0_14^0 == 0 /\ -__disjvr_1^post6+__disjvr_1^0 == 0 /\ tmp_20^0-tmp_20^post6 == 0 /\ a_140^0-a_140^post6 == 0 /\ __disjvr_0^post6-__disjvr_0^0 == 0 /\ length_10^0-length_10^post6 == 0 /\ -a_16^post6+a_16^0 == 0 /\ -__disjvr_0^post6+__disjvr_0^0 == 0), cost: 1
   7: l7 -> l5 : a_140^0'=a_140^post7, t_17^0'=t_17^post7, __cil_tmp6_15^0'=__cil_tmp6_15^post7, tmp_20^0'=tmp_20^post7, length_10^0'=length_10^post7, head_12^0'=head_12^post7, __disjvr_1^0'=__disjvr_1^post7, x_18^0'=x_18^post7, lt_21^0'=lt_21^post7, Result_4^0'=Result_4^post7, len_47^0'=len_47^post7, a_16^0'=a_16^post7, tmp_13^0'=tmp_13^post7, __disjvr_0^0'=__disjvr_0^post7, tmp___0_14^0'=tmp___0_14^post7, length_19^0'=length_19^post7, i_11^0'=i_11^post7, (0 == 0 /\ tmp___0_14^0-tmp___0_14^post7 == 0 /\ a_140^0-a_140^post7 == 0 /\ -i_11^post7+i_11^0 == 0 /\ __disjvr_1^0-__disjvr_1^post7 == 0 /\ Result_4^0-Result_4^post7 == 0 /\ -length_19^post7+length_19^0 == 0 /\ a_16^0-a_16^post7 == 0 /\ -tmp_13^post7+tmp_13^0 == 0 /\ x_18^post7-lt_21^10 == 0 /\ -len_47^post7+len_47^0 == 0 /\ head_12^0-head_12^post7 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post7 == 0 /\ tmp_20^0-tmp_20^post7 == 0 /\ -__disjvr_0^post7+__disjvr_0^0 == 0 /\ t_17^post7-x_18^0 == 0 /\ -length_10^post7+length_10^0 == 0), cost: 1
   9: l5 -> l9 : a_140^0'=a_140^post9, t_17^0'=t_17^post9, __cil_tmp6_15^0'=__cil_tmp6_15^post9, tmp_20^0'=tmp_20^post9, length_10^0'=length_10^post9, head_12^0'=head_12^post9, __disjvr_1^0'=__disjvr_1^post9, x_18^0'=x_18^post9, lt_21^0'=lt_21^post9, Result_4^0'=Result_4^post9, len_47^0'=len_47^post9, a_16^0'=a_16^post9, tmp_13^0'=tmp_13^post9, __disjvr_0^0'=__disjvr_0^post9, tmp___0_14^0'=tmp___0_14^post9, length_19^0'=length_19^post9, i_11^0'=i_11^post9, (__disjvr_1^0-__disjvr_1^post9 == 0 /\ t_17^0-t_17^post9 == 0 /\ -length_19^post9+length_19^0 == 0 /\ -i_11^post9+i_11^0 == 0 /\ -tmp_13^post9+tmp_13^0 == 0 /\ len_47^0-len_47^post9 == 0 /\ tmp_20^0-tmp_20^post9 == 0 /\ -tmp___0_14^post9+tmp___0_14^0 == 0 /\ -Result_4^post9+Result_4^0 == 0 /\ length_10^0-length_10^post9 == 0 /\ -lt_21^post9+lt_21^0 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post9 == 0 /\ -head_12^post9+head_12^0 == 0 /\ -a_140^0 <= 0 /\ -a_16^post9+a_16^0 == 0 /\ a_140^0-a_140^post9 == 0 /\ x_18^0-x_18^post9 == 0 /\ -__disjvr_0^post9+__disjvr_0^0 == 0), cost: 1
  10: l9 -> l10 : a_140^0'=a_140^post10, t_17^0'=t_17^post10, __cil_tmp6_15^0'=__cil_tmp6_15^post10, tmp_20^0'=tmp_20^post10, length_10^0'=length_10^post10, head_12^0'=head_12^post10, __disjvr_1^0'=__disjvr_1^post10, x_18^0'=x_18^post10, lt_21^0'=lt_21^post10, Result_4^0'=Result_4^post10, len_47^0'=len_47^post10, a_16^0'=a_16^post10, tmp_13^0'=tmp_13^post10, __disjvr_0^0'=__disjvr_0^post10, tmp___0_14^0'=tmp___0_14^post10, length_19^0'=length_19^post10, i_11^0'=i_11^post10, (tmp___0_14^0-tmp___0_14^post10 == 0 /\ tmp_13^0-tmp_13^post10 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post10 == 0 /\ -length_10^post10+length_10^0 == 0 /\ -length_19^post10+length_19^0 == 0 /\ -i_11^post10+i_11^0 == 0 /\ -Result_4^post10+Result_4^0 == 0 /\ -x_18^post10+x_18^0 == 0 /\ a_140^0-a_140^post10 == 0 /\ lt_21^0-lt_21^post10 == 0 /\ __disjvr_1^0-__disjvr_1^post10 == 0 /\ t_17^0-t_17^post10 == 0 /\ -len_47^post10+len_47^0 == 0 /\ -__disjvr_1^0+__disjvr_1^post10 == 0 /\ head_12^0-head_12^post10 == 0 /\ -a_16^post10+a_16^0 == 0 /\ tmp_20^0-tmp_20^post10 == 0 /\ -__disjvr_0^post10+__disjvr_0^0 == 0), cost: 1
  11: l10 -> l8 : a_140^0'=a_140^post11, t_17^0'=t_17^post11, __cil_tmp6_15^0'=__cil_tmp6_15^post11, tmp_20^0'=tmp_20^post11, length_10^0'=length_10^post11, head_12^0'=head_12^post11, __disjvr_1^0'=__disjvr_1^post11, x_18^0'=x_18^post11, lt_21^0'=lt_21^post11, Result_4^0'=Result_4^post11, len_47^0'=len_47^post11, a_16^0'=a_16^post11, tmp_13^0'=tmp_13^post11, __disjvr_0^0'=__disjvr_0^post11, tmp___0_14^0'=tmp___0_14^post11, length_19^0'=length_19^post11, i_11^0'=i_11^post11, (0 == 0 /\ length_19^0-length_19^post11 == 0 /\ -i_11^post11+i_11^0 == 0 /\ Result_4^0-Result_4^post11 == 0 /\ -__disjvr_1^post11+__disjvr_1^0 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post11 == 0 /\ -len_47^post11+len_47^0 == 0 /\ tmp_20^0-tmp_20^post11 == 0 /\ a_16^0-a_16^post11 == 0 /\ -__disjvr_0^post11+__disjvr_0^0 == 0 /\ -head_12^post11+head_12^0 == 0 /\ a_140^0-a_140^post11 == 0 /\ -tmp_13^post11+tmp_13^0 == 0 /\ length_10^0-length_10^post11 == 0 /\ -x_18^0+t_17^post11 == 0 /\ -lt_21^11+x_18^post11 == 0 /\ -tmp___0_14^post11+tmp___0_14^0 == 0), cost: 1
  12: l8 -> l5 : a_140^0'=a_140^post12, t_17^0'=t_17^post12, __cil_tmp6_15^0'=__cil_tmp6_15^post12, tmp_20^0'=tmp_20^post12, length_10^0'=length_10^post12, head_12^0'=head_12^post12, __disjvr_1^0'=__disjvr_1^post12, x_18^0'=x_18^post12, lt_21^0'=lt_21^post12, Result_4^0'=Result_4^post12, len_47^0'=len_47^post12, a_16^0'=a_16^post12, tmp_13^0'=tmp_13^post12, __disjvr_0^0'=__disjvr_0^post12, tmp___0_14^0'=tmp___0_14^post12, length_19^0'=length_19^post12, i_11^0'=i_11^post12, (-lt_21^post12+lt_21^0 == 0 /\ -length_19^post12+length_19^0 == 0 /\ tmp_20^0-tmp_20^post12 == 0 /\ -Result_4^post12+Result_4^0 == 0 /\ -a_16^post12+a_16^0 == 0 /\ -tmp___0_14^post12+tmp___0_14^0 == 0 /\ len_47^0-len_47^post12 == 0 /\ __disjvr_1^0-__disjvr_1^post12 == 0 /\ length_10^0-length_10^post12 == 0 /\ -head_12^post12+head_12^0 == 0 /\ -tmp_13^post12+tmp_13^0 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post12 == 0 /\ -i_11^post12+i_11^0 == 0 /\ x_18^0-x_18^post12 == 0 /\ -__disjvr_0^post12+__disjvr_0^0 == 0 /\ a_140^0-a_140^post12 == 0 /\ -t_17^post12+t_17^0 == 0), cost: 1
  13: l11 -> l0 : a_140^0'=a_140^post13, t_17^0'=t_17^post13, __cil_tmp6_15^0'=__cil_tmp6_15^post13, tmp_20^0'=tmp_20^post13, length_10^0'=length_10^post13, head_12^0'=head_12^post13, __disjvr_1^0'=__disjvr_1^post13, x_18^0'=x_18^post13, lt_21^0'=lt_21^post13, Result_4^0'=Result_4^post13, len_47^0'=len_47^post13, a_16^0'=a_16^post13, tmp_13^0'=tmp_13^post13, __disjvr_0^0'=__disjvr_0^post13, tmp___0_14^0'=tmp___0_14^post13, length_19^0'=length_19^post13, i_11^0'=i_11^post13, (head_12^0-head_12^post13 == 0 /\ t_17^0-t_17^post13 == 0 /\ -len_47^post13+len_47^0 == 0 /\ __disjvr_0^0-__disjvr_0^post13 == 0 /\ -i_11^post13+i_11^0 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post13 == 0 /\ -length_10^post13+length_10^0 == 0 /\ Result_4^0-Result_4^post13 == 0 /\ tmp_13^0-tmp_13^post13 == 0 /\ __disjvr_1^0-__disjvr_1^post13 == 0 /\ a_140^0-a_140^post13 == 0 /\ -tmp_20^post13+tmp_20^0 == 0 /\ -length_19^post13+length_19^0 == 0 /\ -x_18^post13+x_18^0 == 0 /\ -a_16^post13+a_16^0 == 0 /\ -tmp___0_14^post13+tmp___0_14^0 == 0 /\ -lt_21^post13+lt_21^0 == 0), cost: 1


Applied preprocessing
Original rule:
l0 -> l1 : a_140^0'=a_140^post0, t_17^0'=t_17^post0, __cil_tmp6_15^0'=__cil_tmp6_15^post0, tmp_20^0'=tmp_20^post0, length_10^0'=length_10^post0, head_12^0'=head_12^post0, __disjvr_1^0'=__disjvr_1^post0, x_18^0'=x_18^post0, lt_21^0'=lt_21^post0, Result_4^0'=Result_4^post0, len_47^0'=len_47^post0, a_16^0'=a_16^post0, tmp_13^0'=tmp_13^post0, __disjvr_0^0'=__disjvr_0^post0, tmp___0_14^0'=tmp___0_14^post0, length_19^0'=length_19^post0, i_11^0'=i_11^post0, (0 == 0 /\ -tmp___0_14^post0+tmp___0_14^0 == 0 /\ -__disjvr_1^post0+__disjvr_1^0 == 0 /\ lt_21^0-lt_21^post0 == 0 /\ t_17^0-t_17^post0 == 0 /\ __disjvr_0^0-__disjvr_0^post0 == 0 /\ -len_47^post0+len_47^0 == 0 /\ -x_18^post0+x_18^0 == 0 /\ -a_16^post0+a_16^0 == 0 /\ tmp_13^0-tmp_13^post0 == 0 /\ Result_4^0-Result_4^post0 == 0 /\ length_10^0-length_10^post0 == 0 /\ head_12^post0 == 0 /\ i_11^post0 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post0 == 0 /\ a_140^0-a_140^post0 == 0 /\ -tmp_20^post0+tmp_20^0 == 0), cost: 1
New rule:
l0 -> l1 : head_12^0'=0, length_19^0'=length_19^post0, i_11^0'=0, 0 == 0, cost: 1

Applied preprocessing
Original rule:
l1 -> l2 : a_140^0'=a_140^post1, t_17^0'=t_17^post1, __cil_tmp6_15^0'=__cil_tmp6_15^post1, tmp_20^0'=tmp_20^post1, length_10^0'=length_10^post1, head_12^0'=head_12^post1, __disjvr_1^0'=__disjvr_1^post1, x_18^0'=x_18^post1, lt_21^0'=lt_21^post1, Result_4^0'=Result_4^post1, len_47^0'=len_47^post1, a_16^0'=a_16^post1, tmp_13^0'=tmp_13^post1, __disjvr_0^0'=__disjvr_0^post1, tmp___0_14^0'=tmp___0_14^post1, length_19^0'=length_19^post1, i_11^0'=i_11^post1, (0 == 0 /\ tmp_20^0-tmp_20^post1 == 0 /\ a_140^0-a_140^post1 == 0 /\ -1+i_11^post1-i_11^0 == 0 /\ -length_19^post1+length_19^0 == 0 /\ Result_4^0-Result_4^post1 == 0 /\ length_10^0-length_10^post1 == 0 /\ -__disjvr_1^post1+__disjvr_1^0 == 0 /\ tmp_13^post1-tmp___0_14^post1 == 0 /\ -tmp_13^post1+head_12^post1 == 0 /\ x_18^0-x_18^post1 == 0 /\ a_16^0-a_16^post1 == 0 /\ 2-length_10^0+i_11^0 <= 0 /\ -len_47^post1+len_47^0 == 0 /\ -__disjvr_0^post1+__disjvr_0^0 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post1 == 0 /\ t_17^0-t_17^post1 == 0 /\ lt_21^0-lt_21^post1 == 0), cost: 1
New rule:
l1 -> l2 : head_12^0'=head_12^post1, tmp_13^0'=head_12^post1, tmp___0_14^0'=head_12^post1, i_11^0'=1+i_11^0, 2-length_10^0+i_11^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l2 -> l4 : a_140^0'=a_140^post3, t_17^0'=t_17^post3, __cil_tmp6_15^0'=__cil_tmp6_15^post3, tmp_20^0'=tmp_20^post3, length_10^0'=length_10^post3, head_12^0'=head_12^post3, __disjvr_1^0'=__disjvr_1^post3, x_18^0'=x_18^post3, lt_21^0'=lt_21^post3, Result_4^0'=Result_4^post3, len_47^0'=len_47^post3, a_16^0'=a_16^post3, tmp_13^0'=tmp_13^post3, __disjvr_0^0'=__disjvr_0^post3, tmp___0_14^0'=tmp___0_14^post3, length_19^0'=length_19^post3, i_11^0'=i_11^post3, (0 == 0 /\ -1+i_11^post3-i_11^0 == 0 /\ -lt_21^post3+lt_21^0 == 0 /\ t_17^0-t_17^post3 == 0 /\ a_140^0-a_140^post3 == 0 /\ length_19^0-length_19^post3 == 0 /\ tmp_20^0-tmp_20^post3 == 0 /\ -__disjvr_0^post3+__disjvr_0^0 == 0 /\ head_12^post3-tmp_13^post3 == 0 /\ 2-length_10^0+i_11^0 <= 0 /\ __disjvr_1^0-__disjvr_1^post3 == 0 /\ a_16^0-a_16^post3 == 0 /\ length_10^0-length_10^post3 == 0 /\ x_18^0-x_18^post3 == 0 /\ len_47^0-len_47^post3 == 0 /\ tmp_13^post3-tmp___0_14^post3 == 0 /\ -Result_4^post3+Result_4^0 == 0 /\ -len_47^0 <= 0 /\ -__cil_tmp6_15^post3+__cil_tmp6_15^0 == 0), cost: 1
New rule:
l2 -> l4 : head_12^0'=tmp___0_14^post3, tmp_13^0'=tmp___0_14^post3, tmp___0_14^0'=tmp___0_14^post3, i_11^0'=1+i_11^0, (len_47^0 >= 0 /\ 2-length_10^0+i_11^0 <= 0), cost: 1

Applied preprocessing
Original rule:
l4 -> l2 : a_140^0'=a_140^post4, t_17^0'=t_17^post4, __cil_tmp6_15^0'=__cil_tmp6_15^post4, tmp_20^0'=tmp_20^post4, length_10^0'=length_10^post4, head_12^0'=head_12^post4, __disjvr_1^0'=__disjvr_1^post4, x_18^0'=x_18^post4, lt_21^0'=lt_21^post4, Result_4^0'=Result_4^post4, len_47^0'=len_47^post4, a_16^0'=a_16^post4, tmp_13^0'=tmp_13^post4, __disjvr_0^0'=__disjvr_0^post4, tmp___0_14^0'=tmp___0_14^post4, length_19^0'=length_19^post4, i_11^0'=i_11^post4, (tmp___0_14^0-tmp___0_14^post4 == 0 /\ len_47^0-len_47^post4 == 0 /\ __disjvr_1^0-__disjvr_1^post4 == 0 /\ a_140^0-a_140^post4 == 0 /\ tmp_20^0-tmp_20^post4 == 0 /\ -tmp_13^post4+tmp_13^0 == 0 /\ -i_11^post4+i_11^0 == 0 /\ -head_12^post4+head_12^0 == 0 /\ -__disjvr_0^post4+__disjvr_0^0 == 0 /\ length_10^0-length_10^post4 == 0 /\ x_18^0-x_18^post4 == 0 /\ t_17^0-t_17^post4 == 0 /\ -length_19^post4+length_19^0 == 0 /\ -Result_4^post4+Result_4^0 == 0 /\ -a_16^post4+a_16^0 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post4 == 0 /\ -lt_21^post4+lt_21^0 == 0), cost: 1
New rule:
l4 -> l2 : TRUE, cost: 1

Applied preprocessing
Original rule:
l2 -> l6 : a_140^0'=a_140^post5, t_17^0'=t_17^post5, __cil_tmp6_15^0'=__cil_tmp6_15^post5, tmp_20^0'=tmp_20^post5, length_10^0'=length_10^post5, head_12^0'=head_12^post5, __disjvr_1^0'=__disjvr_1^post5, x_18^0'=x_18^post5, lt_21^0'=lt_21^post5, Result_4^0'=Result_4^post5, len_47^0'=len_47^post5, a_16^0'=a_16^post5, tmp_13^0'=tmp_13^post5, __disjvr_0^0'=__disjvr_0^post5, tmp___0_14^0'=tmp___0_14^post5, length_19^0'=length_19^post5, i_11^0'=i_11^post5, (0 == 0 /\ -tmp___0_14^post5+tmp___0_14^0 == 0 /\ -__disjvr_1^post5+__disjvr_1^0 == 0 /\ length_10^0-length_10^post5 == 0 /\ a_140^0-a_140^post5 == 0 /\ -1+length_10^0-i_11^0 <= 0 /\ -a_16^post5+a_16^0 == 0 /\ __cil_tmp6_15^post5-head_12^0 == 0 /\ -Result_4^11+tmp_20^post5 == 0 /\ -len_47^post5+len_47^0 == 0 /\ x_18^post5-a_16^0 == 0 /\ lt_21^0-lt_21^post5 == 0 /\ -__disjvr_0^post5+__disjvr_0^0 == 0 /\ t_17^0-t_17^post5 == 0 /\ -length_19^post5+length_19^0 == 0 /\ -__cil_tmp6_15^post5+Result_4^11 == 0 /\ -i_11^post5+i_11^0 == 0 /\ head_12^0-head_12^post5 == 0 /\ -len_47^0 <= 0 /\ tmp_13^0-tmp_13^post5 == 0), cost: 1
New rule:
l2 -> l6 : __cil_tmp6_15^0'=head_12^0, tmp_20^0'=head_12^0, x_18^0'=a_16^0, Result_4^0'=Result_4^post5, (-1+length_10^0-i_11^0 <= 0 /\ len_47^0 >= 0), cost: 1

Applied preprocessing
Original rule:
l6 -> l7 : a_140^0'=a_140^post6, t_17^0'=t_17^post6, __cil_tmp6_15^0'=__cil_tmp6_15^post6, tmp_20^0'=tmp_20^post6, length_10^0'=length_10^post6, head_12^0'=head_12^post6, __disjvr_1^0'=__disjvr_1^post6, x_18^0'=x_18^post6, lt_21^0'=lt_21^post6, Result_4^0'=Result_4^post6, len_47^0'=len_47^post6, a_16^0'=a_16^post6, tmp_13^0'=tmp_13^post6, __disjvr_0^0'=__disjvr_0^post6, tmp___0_14^0'=tmp___0_14^post6, length_19^0'=length_19^post6, i_11^0'=i_11^post6, (x_18^0-x_18^post6 == 0 /\ -lt_21^post6+lt_21^0 == 0 /\ -__cil_tmp6_15^post6+__cil_tmp6_15^0 == 0 /\ -tmp_13^post6+tmp_13^0 == 0 /\ -head_12^post6+head_12^0 == 0 /\ -i_11^post6+i_11^0 == 0 /\ -length_19^post6+length_19^0 == 0 /\ -Result_4^post6+Result_4^0 == 0 /\ t_17^0-t_17^post6 == 0 /\ len_47^0-len_47^post6 == 0 /\ -tmp___0_14^post6+tmp___0_14^0 == 0 /\ -__disjvr_1^post6+__disjvr_1^0 == 0 /\ tmp_20^0-tmp_20^post6 == 0 /\ a_140^0-a_140^post6 == 0 /\ __disjvr_0^post6-__disjvr_0^0 == 0 /\ length_10^0-length_10^post6 == 0 /\ -a_16^post6+a_16^0 == 0 /\ -__disjvr_0^post6+__disjvr_0^0 == 0), cost: 1
New rule:
l6 -> l7 : 0 == 0, cost: 1

Applied preprocessing
Original rule:
l7 -> l5 : a_140^0'=a_140^post7, t_17^0'=t_17^post7, __cil_tmp6_15^0'=__cil_tmp6_15^post7, tmp_20^0'=tmp_20^post7, length_10^0'=length_10^post7, head_12^0'=head_12^post7, __disjvr_1^0'=__disjvr_1^post7, x_18^0'=x_18^post7, lt_21^0'=lt_21^post7, Result_4^0'=Result_4^post7, len_47^0'=len_47^post7, a_16^0'=a_16^post7, tmp_13^0'=tmp_13^post7, __disjvr_0^0'=__disjvr_0^post7, tmp___0_14^0'=tmp___0_14^post7, length_19^0'=length_19^post7, i_11^0'=i_11^post7, (0 == 0 /\ tmp___0_14^0-tmp___0_14^post7 == 0 /\ a_140^0-a_140^post7 == 0 /\ -i_11^post7+i_11^0 == 0 /\ __disjvr_1^0-__disjvr_1^post7 == 0 /\ Result_4^0-Result_4^post7 == 0 /\ -length_19^post7+length_19^0 == 0 /\ a_16^0-a_16^post7 == 0 /\ -tmp_13^post7+tmp_13^0 == 0 /\ x_18^post7-lt_21^10 == 0 /\ -len_47^post7+len_47^0 == 0 /\ head_12^0-head_12^post7 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post7 == 0 /\ tmp_20^0-tmp_20^post7 == 0 /\ -__disjvr_0^post7+__disjvr_0^0 == 0 /\ t_17^post7-x_18^0 == 0 /\ -length_10^post7+length_10^0 == 0), cost: 1
New rule:
l7 -> l5 : t_17^0'=x_18^0, x_18^0'=lt_21^10, lt_21^0'=lt_21^post7, 0 == 0, cost: 1

Applied preprocessing
Original rule:
l5 -> l9 : a_140^0'=a_140^post9, t_17^0'=t_17^post9, __cil_tmp6_15^0'=__cil_tmp6_15^post9, tmp_20^0'=tmp_20^post9, length_10^0'=length_10^post9, head_12^0'=head_12^post9, __disjvr_1^0'=__disjvr_1^post9, x_18^0'=x_18^post9, lt_21^0'=lt_21^post9, Result_4^0'=Result_4^post9, len_47^0'=len_47^post9, a_16^0'=a_16^post9, tmp_13^0'=tmp_13^post9, __disjvr_0^0'=__disjvr_0^post9, tmp___0_14^0'=tmp___0_14^post9, length_19^0'=length_19^post9, i_11^0'=i_11^post9, (__disjvr_1^0-__disjvr_1^post9 == 0 /\ t_17^0-t_17^post9 == 0 /\ -length_19^post9+length_19^0 == 0 /\ -i_11^post9+i_11^0 == 0 /\ -tmp_13^post9+tmp_13^0 == 0 /\ len_47^0-len_47^post9 == 0 /\ tmp_20^0-tmp_20^post9 == 0 /\ -tmp___0_14^post9+tmp___0_14^0 == 0 /\ -Result_4^post9+Result_4^0 == 0 /\ length_10^0-length_10^post9 == 0 /\ -lt_21^post9+lt_21^0 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post9 == 0 /\ -head_12^post9+head_12^0 == 0 /\ -a_140^0 <= 0 /\ -a_16^post9+a_16^0 == 0 /\ a_140^0-a_140^post9 == 0 /\ x_18^0-x_18^post9 == 0 /\ -__disjvr_0^post9+__disjvr_0^0 == 0), cost: 1
New rule:
l5 -> l9 : a_140^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l9 -> l10 : a_140^0'=a_140^post10, t_17^0'=t_17^post10, __cil_tmp6_15^0'=__cil_tmp6_15^post10, tmp_20^0'=tmp_20^post10, length_10^0'=length_10^post10, head_12^0'=head_12^post10, __disjvr_1^0'=__disjvr_1^post10, x_18^0'=x_18^post10, lt_21^0'=lt_21^post10, Result_4^0'=Result_4^post10, len_47^0'=len_47^post10, a_16^0'=a_16^post10, tmp_13^0'=tmp_13^post10, __disjvr_0^0'=__disjvr_0^post10, tmp___0_14^0'=tmp___0_14^post10, length_19^0'=length_19^post10, i_11^0'=i_11^post10, (tmp___0_14^0-tmp___0_14^post10 == 0 /\ tmp_13^0-tmp_13^post10 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post10 == 0 /\ -length_10^post10+length_10^0 == 0 /\ -length_19^post10+length_19^0 == 0 /\ -i_11^post10+i_11^0 == 0 /\ -Result_4^post10+Result_4^0 == 0 /\ -x_18^post10+x_18^0 == 0 /\ a_140^0-a_140^post10 == 0 /\ lt_21^0-lt_21^post10 == 0 /\ __disjvr_1^0-__disjvr_1^post10 == 0 /\ t_17^0-t_17^post10 == 0 /\ -len_47^post10+len_47^0 == 0 /\ -__disjvr_1^0+__disjvr_1^post10 == 0 /\ head_12^0-head_12^post10 == 0 /\ -a_16^post10+a_16^0 == 0 /\ tmp_20^0-tmp_20^post10 == 0 /\ -__disjvr_0^post10+__disjvr_0^0 == 0), cost: 1
New rule:
l9 -> l10 : 0 == 0, cost: 1

Applied preprocessing
Original rule:
l10 -> l8 : a_140^0'=a_140^post11, t_17^0'=t_17^post11, __cil_tmp6_15^0'=__cil_tmp6_15^post11, tmp_20^0'=tmp_20^post11, length_10^0'=length_10^post11, head_12^0'=head_12^post11, __disjvr_1^0'=__disjvr_1^post11, x_18^0'=x_18^post11, lt_21^0'=lt_21^post11, Result_4^0'=Result_4^post11, len_47^0'=len_47^post11, a_16^0'=a_16^post11, tmp_13^0'=tmp_13^post11, __disjvr_0^0'=__disjvr_0^post11, tmp___0_14^0'=tmp___0_14^post11, length_19^0'=length_19^post11, i_11^0'=i_11^post11, (0 == 0 /\ length_19^0-length_19^post11 == 0 /\ -i_11^post11+i_11^0 == 0 /\ Result_4^0-Result_4^post11 == 0 /\ -__disjvr_1^post11+__disjvr_1^0 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post11 == 0 /\ -len_47^post11+len_47^0 == 0 /\ tmp_20^0-tmp_20^post11 == 0 /\ a_16^0-a_16^post11 == 0 /\ -__disjvr_0^post11+__disjvr_0^0 == 0 /\ -head_12^post11+head_12^0 == 0 /\ a_140^0-a_140^post11 == 0 /\ -tmp_13^post11+tmp_13^0 == 0 /\ length_10^0-length_10^post11 == 0 /\ -x_18^0+t_17^post11 == 0 /\ -lt_21^11+x_18^post11 == 0 /\ -tmp___0_14^post11+tmp___0_14^0 == 0), cost: 1
New rule:
l10 -> l8 : t_17^0'=x_18^0, x_18^0'=lt_21^11, lt_21^0'=lt_21^post11, 0 == 0, cost: 1

Applied preprocessing
Original rule:
l8 -> l5 : a_140^0'=a_140^post12, t_17^0'=t_17^post12, __cil_tmp6_15^0'=__cil_tmp6_15^post12, tmp_20^0'=tmp_20^post12, length_10^0'=length_10^post12, head_12^0'=head_12^post12, __disjvr_1^0'=__disjvr_1^post12, x_18^0'=x_18^post12, lt_21^0'=lt_21^post12, Result_4^0'=Result_4^post12, len_47^0'=len_47^post12, a_16^0'=a_16^post12, tmp_13^0'=tmp_13^post12, __disjvr_0^0'=__disjvr_0^post12, tmp___0_14^0'=tmp___0_14^post12, length_19^0'=length_19^post12, i_11^0'=i_11^post12, (-lt_21^post12+lt_21^0 == 0 /\ -length_19^post12+length_19^0 == 0 /\ tmp_20^0-tmp_20^post12 == 0 /\ -Result_4^post12+Result_4^0 == 0 /\ -a_16^post12+a_16^0 == 0 /\ -tmp___0_14^post12+tmp___0_14^0 == 0 /\ len_47^0-len_47^post12 == 0 /\ __disjvr_1^0-__disjvr_1^post12 == 0 /\ length_10^0-length_10^post12 == 0 /\ -head_12^post12+head_12^0 == 0 /\ -tmp_13^post12+tmp_13^0 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post12 == 0 /\ -i_11^post12+i_11^0 == 0 /\ x_18^0-x_18^post12 == 0 /\ -__disjvr_0^post12+__disjvr_0^0 == 0 /\ a_140^0-a_140^post12 == 0 /\ -t_17^post12+t_17^0 == 0), cost: 1
New rule:
l8 -> l5 : TRUE, cost: 1

Applied preprocessing
Original rule:
l11 -> l0 : a_140^0'=a_140^post13, t_17^0'=t_17^post13, __cil_tmp6_15^0'=__cil_tmp6_15^post13, tmp_20^0'=tmp_20^post13, length_10^0'=length_10^post13, head_12^0'=head_12^post13, __disjvr_1^0'=__disjvr_1^post13, x_18^0'=x_18^post13, lt_21^0'=lt_21^post13, Result_4^0'=Result_4^post13, len_47^0'=len_47^post13, a_16^0'=a_16^post13, tmp_13^0'=tmp_13^post13, __disjvr_0^0'=__disjvr_0^post13, tmp___0_14^0'=tmp___0_14^post13, length_19^0'=length_19^post13, i_11^0'=i_11^post13, (head_12^0-head_12^post13 == 0 /\ t_17^0-t_17^post13 == 0 /\ -len_47^post13+len_47^0 == 0 /\ __disjvr_0^0-__disjvr_0^post13 == 0 /\ -i_11^post13+i_11^0 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post13 == 0 /\ -length_10^post13+length_10^0 == 0 /\ Result_4^0-Result_4^post13 == 0 /\ tmp_13^0-tmp_13^post13 == 0 /\ __disjvr_1^0-__disjvr_1^post13 == 0 /\ a_140^0-a_140^post13 == 0 /\ -tmp_20^post13+tmp_20^0 == 0 /\ -length_19^post13+length_19^0 == 0 /\ -x_18^post13+x_18^0 == 0 /\ -a_16^post13+a_16^0 == 0 /\ -tmp___0_14^post13+tmp___0_14^0 == 0 /\ -lt_21^post13+lt_21^0 == 0), cost: 1
New rule:
l11 -> l0 : TRUE, cost: 1

Simplified rules
Start location: l11
  14: l0 -> l1 : head_12^0'=0, length_19^0'=length_19^post0, i_11^0'=0, 0 == 0, cost: 1
  15: l1 -> l2 : head_12^0'=head_12^post1, tmp_13^0'=head_12^post1, tmp___0_14^0'=head_12^post1, i_11^0'=1+i_11^0, 2-length_10^0+i_11^0 <= 0, cost: 1
  16: l2 -> l4 : head_12^0'=tmp___0_14^post3, tmp_13^0'=tmp___0_14^post3, tmp___0_14^0'=tmp___0_14^post3, i_11^0'=1+i_11^0, (len_47^0 >= 0 /\ 2-length_10^0+i_11^0 <= 0), cost: 1
  18: l2 -> l6 : __cil_tmp6_15^0'=head_12^0, tmp_20^0'=head_12^0, x_18^0'=a_16^0, Result_4^0'=Result_4^post5, (-1+length_10^0-i_11^0 <= 0 /\ len_47^0 >= 0), cost: 1
  17: l4 -> l2 : TRUE, cost: 1
  19: l6 -> l7 : 0 == 0, cost: 1
  20: l7 -> l5 : t_17^0'=x_18^0, x_18^0'=lt_21^10, lt_21^0'=lt_21^post7, 0 == 0, cost: 1
  21: l5 -> l9 : a_140^0 >= 0, cost: 1
  22: l9 -> l10 : 0 == 0, cost: 1
  23: l10 -> l8 : t_17^0'=x_18^0, x_18^0'=lt_21^11, lt_21^0'=lt_21^post11, 0 == 0, cost: 1
  24: l8 -> l5 : TRUE, cost: 1
  25: l11 -> l0 : TRUE, cost: 1


Eliminating location l0 by chaining:

Applied chaining
First rule:
l11 -> l0 : TRUE, cost: 1
Second rule:
l0 -> l1 : head_12^0'=0, length_19^0'=length_19^post0, i_11^0'=0, 0 == 0, cost: 1
New rule:
l11 -> l1 : head_12^0'=0, length_19^0'=length_19^post0, i_11^0'=0, 0 == 0, cost: 2

Applied deletion
Removed the following rules: 14 25

Eliminating location l1 by chaining:

Applied chaining
First rule:
l11 -> l1 : head_12^0'=0, length_19^0'=length_19^post0, i_11^0'=0, 0 == 0, cost: 2
Second rule:
l1 -> l2 : head_12^0'=head_12^post1, tmp_13^0'=head_12^post1, tmp___0_14^0'=head_12^post1, i_11^0'=1+i_11^0, 2-length_10^0+i_11^0 <= 0, cost: 1
New rule:
l11 -> l2 : head_12^0'=head_12^post1, tmp_13^0'=head_12^post1, tmp___0_14^0'=head_12^post1, length_19^0'=length_19^post0, i_11^0'=1, (0 == 0 /\ 2-length_10^0 <= 0), cost: 3

Applied simplification
Original rule:
l11 -> l2 : head_12^0'=head_12^post1, tmp_13^0'=head_12^post1, tmp___0_14^0'=head_12^post1, length_19^0'=length_19^post0, i_11^0'=1, (0 == 0 /\ 2-length_10^0 <= 0), cost: 3
New rule:
l11 -> l2 : head_12^0'=head_12^post1, tmp_13^0'=head_12^post1, tmp___0_14^0'=head_12^post1, length_19^0'=length_19^post0, i_11^0'=1, -2+length_10^0 >= 0, cost: 3

Applied deletion
Removed the following rules: 15 26

Eliminating location l4 by chaining:

Applied chaining
First rule:
l2 -> l4 : head_12^0'=tmp___0_14^post3, tmp_13^0'=tmp___0_14^post3, tmp___0_14^0'=tmp___0_14^post3, i_11^0'=1+i_11^0, (len_47^0 >= 0 /\ 2-length_10^0+i_11^0 <= 0), cost: 1
Second rule:
l4 -> l2 : TRUE, cost: 1
New rule:
l2 -> l2 : head_12^0'=tmp___0_14^post3, tmp_13^0'=tmp___0_14^post3, tmp___0_14^0'=tmp___0_14^post3, i_11^0'=1+i_11^0, (len_47^0 >= 0 /\ 2-length_10^0+i_11^0 <= 0), cost: 2

Applied deletion
Removed the following rules: 16 17

Eliminating location l6 by chaining:

Applied chaining
First rule:
l2 -> l6 : __cil_tmp6_15^0'=head_12^0, tmp_20^0'=head_12^0, x_18^0'=a_16^0, Result_4^0'=Result_4^post5, (-1+length_10^0-i_11^0 <= 0 /\ len_47^0 >= 0), cost: 1
Second rule:
l6 -> l7 : 0 == 0, cost: 1
New rule:
l2 -> l7 : __cil_tmp6_15^0'=head_12^0, tmp_20^0'=head_12^0, x_18^0'=a_16^0, Result_4^0'=Result_4^post5, (0 == 0 /\ -1+length_10^0-i_11^0 <= 0 /\ len_47^0 >= 0), cost: 2

Applied simplification
Original rule:
l2 -> l7 : __cil_tmp6_15^0'=head_12^0, tmp_20^0'=head_12^0, x_18^0'=a_16^0, Result_4^0'=Result_4^post5, (0 == 0 /\ -1+length_10^0-i_11^0 <= 0 /\ len_47^0 >= 0), cost: 2
New rule:
l2 -> l7 : __cil_tmp6_15^0'=head_12^0, tmp_20^0'=head_12^0, x_18^0'=a_16^0, Result_4^0'=Result_4^post5, (-1+length_10^0-i_11^0 <= 0 /\ len_47^0 >= 0), cost: 2

Applied deletion
Removed the following rules: 18 19

Eliminating location l7 by chaining:

Applied chaining
First rule:
l2 -> l7 : __cil_tmp6_15^0'=head_12^0, tmp_20^0'=head_12^0, x_18^0'=a_16^0, Result_4^0'=Result_4^post5, (-1+length_10^0-i_11^0 <= 0 /\ len_47^0 >= 0), cost: 2
Second rule:
l7 -> l5 : t_17^0'=x_18^0, x_18^0'=lt_21^10, lt_21^0'=lt_21^post7, 0 == 0, cost: 1
New rule:
l2 -> l5 : t_17^0'=a_16^0, __cil_tmp6_15^0'=head_12^0, tmp_20^0'=head_12^0, x_18^0'=lt_21^10, lt_21^0'=lt_21^post7, Result_4^0'=Result_4^post5, (0 == 0 /\ -1+length_10^0-i_11^0 <= 0 /\ len_47^0 >= 0), cost: 3

Applied simplification
Original rule:
l2 -> l5 : t_17^0'=a_16^0, __cil_tmp6_15^0'=head_12^0, tmp_20^0'=head_12^0, x_18^0'=lt_21^10, lt_21^0'=lt_21^post7, Result_4^0'=Result_4^post5, (0 == 0 /\ -1+length_10^0-i_11^0 <= 0 /\ len_47^0 >= 0), cost: 3
New rule:
l2 -> l5 : t_17^0'=a_16^0, __cil_tmp6_15^0'=head_12^0, tmp_20^0'=head_12^0, x_18^0'=lt_21^10, lt_21^0'=lt_21^post7, Result_4^0'=Result_4^post5, (-1+length_10^0-i_11^0 <= 0 /\ len_47^0 >= 0), cost: 3

Applied deletion
Removed the following rules: 20 29

Eliminating location l9 by chaining:

Applied chaining
First rule:
l5 -> l9 : a_140^0 >= 0, cost: 1
Second rule:
l9 -> l10 : 0 == 0, cost: 1
New rule:
l5 -> l10 : (0 == 0 /\ a_140^0 >= 0), cost: 2

Applied simplification
Original rule:
l5 -> l10 : (0 == 0 /\ a_140^0 >= 0), cost: 2
New rule:
l5 -> l10 : a_140^0 >= 0, cost: 2

Applied deletion
Removed the following rules: 21 22

Eliminating location l10 by chaining:

Applied chaining
First rule:
l5 -> l10 : a_140^0 >= 0, cost: 2
Second rule:
l10 -> l8 : t_17^0'=x_18^0, x_18^0'=lt_21^11, lt_21^0'=lt_21^post11, 0 == 0, cost: 1
New rule:
l5 -> l8 : t_17^0'=x_18^0, x_18^0'=lt_21^11, lt_21^0'=lt_21^post11, (0 == 0 /\ a_140^0 >= 0), cost: 3

Applied simplification
Original rule:
l5 -> l8 : t_17^0'=x_18^0, x_18^0'=lt_21^11, lt_21^0'=lt_21^post11, (0 == 0 /\ a_140^0 >= 0), cost: 3
New rule:
l5 -> l8 : t_17^0'=x_18^0, x_18^0'=lt_21^11, lt_21^0'=lt_21^post11, a_140^0 >= 0, cost: 3

Applied deletion
Removed the following rules: 23 31

Eliminating location l8 by chaining:

Applied chaining
First rule:
l5 -> l8 : t_17^0'=x_18^0, x_18^0'=lt_21^11, lt_21^0'=lt_21^post11, a_140^0 >= 0, cost: 3
Second rule:
l8 -> l5 : TRUE, cost: 1
New rule:
l5 -> l5 : t_17^0'=x_18^0, x_18^0'=lt_21^11, lt_21^0'=lt_21^post11, a_140^0 >= 0, cost: 4

Applied deletion
Removed the following rules: 24 32

Eliminated locations on linear paths
Start location: l11
  28: l2 -> l2 : head_12^0'=tmp___0_14^post3, tmp_13^0'=tmp___0_14^post3, tmp___0_14^0'=tmp___0_14^post3, i_11^0'=1+i_11^0, (len_47^0 >= 0 /\ 2-length_10^0+i_11^0 <= 0), cost: 2
  30: l2 -> l5 : t_17^0'=a_16^0, __cil_tmp6_15^0'=head_12^0, tmp_20^0'=head_12^0, x_18^0'=lt_21^10, lt_21^0'=lt_21^post7, Result_4^0'=Result_4^post5, (-1+length_10^0-i_11^0 <= 0 /\ len_47^0 >= 0), cost: 3
  33: l5 -> l5 : t_17^0'=x_18^0, x_18^0'=lt_21^11, lt_21^0'=lt_21^post11, a_140^0 >= 0, cost: 4
  27: l11 -> l2 : head_12^0'=head_12^post1, tmp_13^0'=head_12^post1, tmp___0_14^0'=head_12^post1, length_19^0'=length_19^post0, i_11^0'=1, -2+length_10^0 >= 0, cost: 3


Applied acceleration
Original rule:
l2 -> l2 : head_12^0'=tmp___0_14^post3, tmp_13^0'=tmp___0_14^post3, tmp___0_14^0'=tmp___0_14^post3, i_11^0'=1+i_11^0, (len_47^0 >= 0 /\ 2-length_10^0+i_11^0 <= 0), cost: 2
New rule:
l2 -> l2 : head_12^0'=tmp___0_14^post3, tmp_13^0'=tmp___0_14^post3, tmp___0_14^0'=tmp___0_14^post3, i_11^0'=n+i_11^0, (-1+length_10^0-n-i_11^0 >= 0 /\ -1+n >= 0 /\ len_47^0 >= 0), cost: 2*n
Sub-proof via acceration calculus written to file:///tmp/tmpnam_BlChML.txt

Applied instantiation
Original rule:
l2 -> l2 : head_12^0'=tmp___0_14^post3, tmp_13^0'=tmp___0_14^post3, tmp___0_14^0'=tmp___0_14^post3, i_11^0'=n+i_11^0, (-1+length_10^0-n-i_11^0 >= 0 /\ -1+n >= 0 /\ len_47^0 >= 0), cost: 2*n
New rule:
l2 -> l2 : head_12^0'=tmp___0_14^post3, tmp_13^0'=tmp___0_14^post3, tmp___0_14^0'=tmp___0_14^post3, i_11^0'=-1+length_10^0, (0 >= 0 /\ len_47^0 >= 0 /\ -2+length_10^0-i_11^0 >= 0), cost: -2+2*length_10^0-2*i_11^0

Applied simplification
Original rule:
l2 -> l2 : head_12^0'=tmp___0_14^post3, tmp_13^0'=tmp___0_14^post3, tmp___0_14^0'=tmp___0_14^post3, i_11^0'=-1+length_10^0, (0 >= 0 /\ len_47^0 >= 0 /\ -2+length_10^0-i_11^0 >= 0), cost: -2+2*length_10^0-2*i_11^0
New rule:
l2 -> l2 : head_12^0'=tmp___0_14^post3, tmp_13^0'=tmp___0_14^post3, tmp___0_14^0'=tmp___0_14^post3, i_11^0'=-1+length_10^0, (len_47^0 >= 0 /\ -2+length_10^0-i_11^0 >= 0), cost: -2+2*length_10^0-2*i_11^0

Applied deletion
Removed the following rules: 28

Applied nonterm
Original rule:
l5 -> l5 : t_17^0'=x_18^0, x_18^0'=lt_21^11, lt_21^0'=lt_21^post11, a_140^0 >= 0, cost: 4
New rule:
l5 -> [13] : (a_140^0 >= 0 /\ -2+n0 >= 0), cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_mIfpMI.txt

Accelerated simple loops
Start location: l11
  30: l2 -> l5 : t_17^0'=a_16^0, __cil_tmp6_15^0'=head_12^0, tmp_20^0'=head_12^0, x_18^0'=lt_21^10, lt_21^0'=lt_21^post7, Result_4^0'=Result_4^post5, (-1+length_10^0-i_11^0 <= 0 /\ len_47^0 >= 0), cost: 3
  35: l2 -> l2 : head_12^0'=tmp___0_14^post3, tmp_13^0'=tmp___0_14^post3, tmp___0_14^0'=tmp___0_14^post3, i_11^0'=-1+length_10^0, (len_47^0 >= 0 /\ -2+length_10^0-i_11^0 >= 0), cost: -2+2*length_10^0-2*i_11^0
  33: l5 -> l5 : t_17^0'=x_18^0, x_18^0'=lt_21^11, lt_21^0'=lt_21^post11, a_140^0 >= 0, cost: 4
  36: l5 -> [13] : (a_140^0 >= 0 /\ -2+n0 >= 0), cost: NONTERM
  27: l11 -> l2 : head_12^0'=head_12^post1, tmp_13^0'=head_12^post1, tmp___0_14^0'=head_12^post1, length_19^0'=length_19^post0, i_11^0'=1, -2+length_10^0 >= 0, cost: 3


Applied chaining
First rule:
l11 -> l2 : head_12^0'=head_12^post1, tmp_13^0'=head_12^post1, tmp___0_14^0'=head_12^post1, length_19^0'=length_19^post0, i_11^0'=1, -2+length_10^0 >= 0, cost: 3
Second rule:
l2 -> l2 : head_12^0'=tmp___0_14^post3, tmp_13^0'=tmp___0_14^post3, tmp___0_14^0'=tmp___0_14^post3, i_11^0'=-1+length_10^0, (len_47^0 >= 0 /\ -2+length_10^0-i_11^0 >= 0), cost: -2+2*length_10^0-2*i_11^0
New rule:
l11 -> l2 : head_12^0'=tmp___0_14^post3, tmp_13^0'=tmp___0_14^post3, tmp___0_14^0'=tmp___0_14^post3, length_19^0'=length_19^post0, i_11^0'=-1+length_10^0, (-3+length_10^0 >= 0 /\ len_47^0 >= 0), cost: -1+2*length_10^0

Applied deletion
Removed the following rules: 35

Applied chaining
First rule:
l2 -> l5 : t_17^0'=a_16^0, __cil_tmp6_15^0'=head_12^0, tmp_20^0'=head_12^0, x_18^0'=lt_21^10, lt_21^0'=lt_21^post7, Result_4^0'=Result_4^post5, (-1+length_10^0-i_11^0 <= 0 /\ len_47^0 >= 0), cost: 3
Second rule:
l5 -> l5 : t_17^0'=x_18^0, x_18^0'=lt_21^11, lt_21^0'=lt_21^post11, a_140^0 >= 0, cost: 4
New rule:
l2 -> l5 : t_17^0'=lt_21^10, __cil_tmp6_15^0'=head_12^0, tmp_20^0'=head_12^0, x_18^0'=lt_21^11, lt_21^0'=lt_21^post11, Result_4^0'=Result_4^post5, (a_140^0 >= 0 /\ -1+length_10^0-i_11^0 <= 0 /\ len_47^0 >= 0), cost: 7

Applied chaining
First rule:
l2 -> l5 : t_17^0'=a_16^0, __cil_tmp6_15^0'=head_12^0, tmp_20^0'=head_12^0, x_18^0'=lt_21^10, lt_21^0'=lt_21^post7, Result_4^0'=Result_4^post5, (-1+length_10^0-i_11^0 <= 0 /\ len_47^0 >= 0), cost: 3
Second rule:
l5 -> [13] : (a_140^0 >= 0 /\ -2+n0 >= 0), cost: NONTERM
New rule:
l2 -> [13] : (a_140^0 >= 0 /\ -1+length_10^0-i_11^0 <= 0 /\ len_47^0 >= 0), cost: NONTERM

Applied deletion
Removed the following rules: 33 36

Chained accelerated rules with incoming rules
Start location: l11
  30: l2 -> l5 : t_17^0'=a_16^0, __cil_tmp6_15^0'=head_12^0, tmp_20^0'=head_12^0, x_18^0'=lt_21^10, lt_21^0'=lt_21^post7, Result_4^0'=Result_4^post5, (-1+length_10^0-i_11^0 <= 0 /\ len_47^0 >= 0), cost: 3
  38: l2 -> l5 : t_17^0'=lt_21^10, __cil_tmp6_15^0'=head_12^0, tmp_20^0'=head_12^0, x_18^0'=lt_21^11, lt_21^0'=lt_21^post11, Result_4^0'=Result_4^post5, (a_140^0 >= 0 /\ -1+length_10^0-i_11^0 <= 0 /\ len_47^0 >= 0), cost: 7
  39: l2 -> [13] : (a_140^0 >= 0 /\ -1+length_10^0-i_11^0 <= 0 /\ len_47^0 >= 0), cost: NONTERM
  27: l11 -> l2 : head_12^0'=head_12^post1, tmp_13^0'=head_12^post1, tmp___0_14^0'=head_12^post1, length_19^0'=length_19^post0, i_11^0'=1, -2+length_10^0 >= 0, cost: 3
  37: l11 -> l2 : head_12^0'=tmp___0_14^post3, tmp_13^0'=tmp___0_14^post3, tmp___0_14^0'=tmp___0_14^post3, length_19^0'=length_19^post0, i_11^0'=-1+length_10^0, (-3+length_10^0 >= 0 /\ len_47^0 >= 0), cost: -1+2*length_10^0


Removed unreachable locations and irrelevant leafs
Start location: l11
  39: l2 -> [13] : (a_140^0 >= 0 /\ -1+length_10^0-i_11^0 <= 0 /\ len_47^0 >= 0), cost: NONTERM
  27: l11 -> l2 : head_12^0'=head_12^post1, tmp_13^0'=head_12^post1, tmp___0_14^0'=head_12^post1, length_19^0'=length_19^post0, i_11^0'=1, -2+length_10^0 >= 0, cost: 3
  37: l11 -> l2 : head_12^0'=tmp___0_14^post3, tmp_13^0'=tmp___0_14^post3, tmp___0_14^0'=tmp___0_14^post3, length_19^0'=length_19^post0, i_11^0'=-1+length_10^0, (-3+length_10^0 >= 0 /\ len_47^0 >= 0), cost: -1+2*length_10^0


Eliminating location l2 by chaining:

Applied chaining
First rule:
l11 -> l2 : head_12^0'=head_12^post1, tmp_13^0'=head_12^post1, tmp___0_14^0'=head_12^post1, length_19^0'=length_19^post0, i_11^0'=1, -2+length_10^0 >= 0, cost: 3
Second rule:
l2 -> [13] : (a_140^0 >= 0 /\ -1+length_10^0-i_11^0 <= 0 /\ len_47^0 >= 0), cost: NONTERM
New rule:
l11 -> [13] : (a_140^0 >= 0 /\ -2+length_10^0 <= 0 /\ -2+length_10^0 >= 0 /\ len_47^0 >= 0), cost: NONTERM

Applied chaining
First rule:
l11 -> l2 : head_12^0'=tmp___0_14^post3, tmp_13^0'=tmp___0_14^post3, tmp___0_14^0'=tmp___0_14^post3, length_19^0'=length_19^post0, i_11^0'=-1+length_10^0, (-3+length_10^0 >= 0 /\ len_47^0 >= 0), cost: -1+2*length_10^0
Second rule:
l2 -> [13] : (a_140^0 >= 0 /\ -1+length_10^0-i_11^0 <= 0 /\ len_47^0 >= 0), cost: NONTERM
New rule:
l11 -> [13] : (0 <= 0 /\ a_140^0 >= 0 /\ -3+length_10^0 >= 0 /\ len_47^0 >= 0), cost: NONTERM

Applied simplification
Original rule:
l11 -> [13] : (0 <= 0 /\ a_140^0 >= 0 /\ -3+length_10^0 >= 0 /\ len_47^0 >= 0), cost: NONTERM
New rule:
l11 -> [13] : (a_140^0 >= 0 /\ -3+length_10^0 >= 0 /\ len_47^0 >= 0), cost: NONTERM

Applied deletion
Removed the following rules: 27 37 39

Eliminated locations on tree-shaped paths
Start location: l11
  40: l11 -> [13] : (a_140^0 >= 0 /\ -2+length_10^0 <= 0 /\ -2+length_10^0 >= 0 /\ len_47^0 >= 0), cost: NONTERM
  41: l11 -> [13] : (a_140^0 >= 0 /\ -3+length_10^0 >= 0 /\ len_47^0 >= 0), cost: NONTERM


Computing asymptotic complexity
Proved nontermination of rule 40 via SMT.

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

Solved cost: NONTERM
Rule cost:   NONTERM
Rule guard:  (a_140^0 >= 0 /\ -2+length_10^0 <= 0 /\ -2+length_10^0 >= 0 /\ len_47^0 >= 0)