NO Initial ITS Start location: l11 Program variables: __cil_tmp6_15^0 __disjvr_0^0 __disjvr_1^0 a_140^0 a_16^0 head_12^0 i_11^0 len_47^0 length_10^0 length_19^0 lt_21^0 result_4^0 t_17^0 tmp_13^0 tmp_20^0 tmp___0_14^0 x_18^0 0: l0 -> l1 : __cil_tmp6_15^0'=__cil_tmp6_15^post1, __disjvr_0^0'=__disjvr_0^post1, __disjvr_1^0'=__disjvr_1^post1, a_140^0'=a_140^post1, a_16^0'=a_16^post1, head_12^0'=head_12^post1, i_11^0'=i_11^post1, len_47^0'=len_47^post1, length_10^0'=length_10^post1, length_19^0'=length_19^post1, lt_21^0'=lt_21^post1, result_4^0'=result_4^post1, t_17^0'=t_17^post1, tmp_13^0'=tmp_13^post1, tmp_20^0'=tmp_20^post1, tmp___0_14^0'=tmp___0_14^post1, x_18^0'=x_18^post1, (0 == 0 /\ head_12^post1 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post1 == 0 /\ -x_18^post1+x_18^0 == 0 /\ i_11^post1 == 0 /\ -a_16^post1+a_16^0 == 0 /\ len_47^0-len_47^post1 == 0 /\ tmp___0_14^0-tmp___0_14^post1 == 0 /\ -tmp_13^post1+tmp_13^0 == 0 /\ lt_21^0-lt_21^post1 == 0 /\ -__disjvr_0^post1+__disjvr_0^0 == 0 /\ length_10^0-length_10^post1 == 0 /\ -__disjvr_1^post1+__disjvr_1^0 == 0 /\ tmp_20^0-tmp_20^post1 == 0 /\ t_17^0-t_17^post1 == 0 /\ a_140^0-a_140^post1 == 0 /\ result_4^0-result_4^post1 == 0), cost: 1 1: l1 -> l2 : __cil_tmp6_15^0'=__cil_tmp6_15^post2, __disjvr_0^0'=__disjvr_0^post2, __disjvr_1^0'=__disjvr_1^post2, a_140^0'=a_140^post2, a_16^0'=a_16^post2, head_12^0'=head_12^post2, i_11^0'=i_11^post2, len_47^0'=len_47^post2, length_10^0'=length_10^post2, length_19^0'=length_19^post2, lt_21^0'=lt_21^post2, result_4^0'=result_4^post2, t_17^0'=t_17^post2, tmp_13^0'=tmp_13^post2, tmp_20^0'=tmp_20^post2, tmp___0_14^0'=tmp___0_14^post2, x_18^0'=x_18^post2, (0 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post2 == 0 /\ tmp_13^post2-tmp___0_14^post2 == 0 /\ -__disjvr_0^post2+__disjvr_0^0 == 0 /\ -tmp_13^post2+head_12^post2 == 0 /\ -result_4^post2+result_4^0 == 0 /\ __disjvr_1^0-__disjvr_1^post2 == 0 /\ tmp_20^0-tmp_20^post2 == 0 /\ -lt_21^post2+lt_21^0 == 0 /\ 2-length_10^0+i_11^0 <= 0 /\ a_140^0-a_140^post2 == 0 /\ -1-i_11^0+i_11^post2 == 0 /\ t_17^0-t_17^post2 == 0 /\ -a_16^post2+a_16^0 == 0 /\ length_10^0-length_10^post2 == 0 /\ -x_18^post2+x_18^0 == 0 /\ length_19^0-length_19^post2 == 0 /\ -len_47^post2+len_47^0 == 0), cost: 1 2: l1 -> l3 : __cil_tmp6_15^0'=__cil_tmp6_15^post3, __disjvr_0^0'=__disjvr_0^post3, __disjvr_1^0'=__disjvr_1^post3, a_140^0'=a_140^post3, a_16^0'=a_16^post3, head_12^0'=head_12^post3, i_11^0'=i_11^post3, len_47^0'=len_47^post3, length_10^0'=length_10^post3, length_19^0'=length_19^post3, lt_21^0'=lt_21^post3, result_4^0'=result_4^post3, t_17^0'=t_17^post3, tmp_13^0'=tmp_13^post3, tmp_20^0'=tmp_20^post3, tmp___0_14^0'=tmp___0_14^post3, x_18^0'=x_18^post3, (0 == 0 /\ -t_17^post3+t_17^0 == 0 /\ -tmp___0_14^post3+tmp___0_14^0 == 0 /\ -tmp_13^post3+tmp_13^0 == 0 /\ -lt_21^post3+lt_21^0 == 0 /\ -__disjvr_0^post3+__disjvr_0^0 == 0 /\ x_18^post3-a_16^0 == 0 /\ __disjvr_1^0-__disjvr_1^post3 == 0 /\ x_18^post3 <= 0 /\ -i_11^post3+i_11^0 == 0 /\ -result_4^1+tmp_20^post3 == 0 /\ len_47^0-len_47^post3 == 0 /\ -1+length_10^0-i_11^0 <= 0 /\ -length_19^post3+length_19^0 == 0 /\ -head_12^0+__cil_tmp6_15^post3 == 0 /\ length_10^0-length_10^post3 == 0 /\ -__cil_tmp6_15^post3+result_4^1 == 0 /\ -head_12^post3+head_12^0 == 0 /\ a_140^0-a_140^post3 == 0 /\ -x_18^post3 <= 0 /\ -a_16^post3+a_16^0 == 0), cost: 1 3: l2 -> l4 : __cil_tmp6_15^0'=__cil_tmp6_15^post4, __disjvr_0^0'=__disjvr_0^post4, __disjvr_1^0'=__disjvr_1^post4, a_140^0'=a_140^post4, a_16^0'=a_16^post4, head_12^0'=head_12^post4, i_11^0'=i_11^post4, len_47^0'=len_47^post4, length_10^0'=length_10^post4, length_19^0'=length_19^post4, lt_21^0'=lt_21^post4, result_4^0'=result_4^post4, t_17^0'=t_17^post4, tmp_13^0'=tmp_13^post4, tmp_20^0'=tmp_20^post4, tmp___0_14^0'=tmp___0_14^post4, x_18^0'=x_18^post4, (0 == 0 /\ -length_19^post4+length_19^0 == 0 /\ -result_4^post4+result_4^0 == 0 /\ -x_18^post4+x_18^0 == 0 /\ -1+i_11^post4-i_11^0 == 0 /\ len_47^0-len_47^post4 == 0 /\ -tmp___0_14^post4+tmp_13^post4 == 0 /\ length_10^0-length_10^post4 == 0 /\ 2-length_10^0+i_11^0 <= 0 /\ a_140^0-a_140^post4 == 0 /\ head_12^post4-tmp_13^post4 == 0 /\ tmp_20^0-tmp_20^post4 == 0 /\ lt_21^0-lt_21^post4 == 0 /\ -__disjvr_1^post4+__disjvr_1^0 == 0 /\ -__disjvr_0^post4+__disjvr_0^0 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post4 == 0 /\ t_17^0-t_17^post4 == 0 /\ -len_47^0 <= 0 /\ a_16^0-a_16^post4 == 0), cost: 1 5: l2 -> l6 : __cil_tmp6_15^0'=__cil_tmp6_15^post6, __disjvr_0^0'=__disjvr_0^post6, __disjvr_1^0'=__disjvr_1^post6, a_140^0'=a_140^post6, a_16^0'=a_16^post6, head_12^0'=head_12^post6, i_11^0'=i_11^post6, len_47^0'=len_47^post6, length_10^0'=length_10^post6, length_19^0'=length_19^post6, lt_21^0'=lt_21^post6, result_4^0'=result_4^post6, t_17^0'=t_17^post6, tmp_13^0'=tmp_13^post6, tmp_20^0'=tmp_20^post6, tmp___0_14^0'=tmp___0_14^post6, x_18^0'=x_18^post6, (0 == 0 /\ -__disjvr_1^post6+__disjvr_1^0 == 0 /\ __cil_tmp6_15^post6-head_12^0 == 0 /\ -result_4^1+tmp_20^post6 == 0 /\ -__cil_tmp6_15^post6+result_4^1 == 0 /\ length_10^0-length_10^post6 == 0 /\ -1+length_10^0-i_11^0 <= 0 /\ -i_11^post6+i_11^0 == 0 /\ tmp___0_14^0-tmp___0_14^post6 == 0 /\ lt_21^0-lt_21^post6 == 0 /\ len_47^0-len_47^post6 == 0 /\ -tmp_13^post6+tmp_13^0 == 0 /\ -__disjvr_0^post6+__disjvr_0^0 == 0 /\ a_16^0-a_16^post6 == 0 /\ a_140^0-a_140^post6 == 0 /\ -head_12^post6+head_12^0 == 0 /\ -len_47^0 <= 0 /\ x_18^post6-a_16^0 == 0 /\ -length_19^post6+length_19^0 == 0 /\ t_17^0-t_17^post6 == 0), cost: 1 4: l4 -> l2 : __cil_tmp6_15^0'=__cil_tmp6_15^post5, __disjvr_0^0'=__disjvr_0^post5, __disjvr_1^0'=__disjvr_1^post5, a_140^0'=a_140^post5, a_16^0'=a_16^post5, head_12^0'=head_12^post5, i_11^0'=i_11^post5, len_47^0'=len_47^post5, length_10^0'=length_10^post5, length_19^0'=length_19^post5, lt_21^0'=lt_21^post5, result_4^0'=result_4^post5, t_17^0'=t_17^post5, tmp_13^0'=tmp_13^post5, tmp_20^0'=tmp_20^post5, tmp___0_14^0'=tmp___0_14^post5, x_18^0'=x_18^post5, (__cil_tmp6_15^0-__cil_tmp6_15^post5 == 0 /\ t_17^0-t_17^post5 == 0 /\ -tmp_20^post5+tmp_20^0 == 0 /\ -lt_21^post5+lt_21^0 == 0 /\ x_18^0-x_18^post5 == 0 /\ -__disjvr_0^post5+__disjvr_0^0 == 0 /\ __disjvr_1^0-__disjvr_1^post5 == 0 /\ -a_16^post5+a_16^0 == 0 /\ -len_47^post5+len_47^0 == 0 /\ head_12^0-head_12^post5 == 0 /\ -length_19^post5+length_19^0 == 0 /\ -result_4^post5+result_4^0 == 0 /\ length_10^0-length_10^post5 == 0 /\ tmp___0_14^0-tmp___0_14^post5 == 0 /\ -tmp_13^post5+tmp_13^0 == 0 /\ i_11^0-i_11^post5 == 0 /\ a_140^0-a_140^post5 == 0), cost: 1 6: l6 -> l7 : __cil_tmp6_15^0'=__cil_tmp6_15^post7, __disjvr_0^0'=__disjvr_0^post7, __disjvr_1^0'=__disjvr_1^post7, a_140^0'=a_140^post7, a_16^0'=a_16^post7, head_12^0'=head_12^post7, i_11^0'=i_11^post7, len_47^0'=len_47^post7, length_10^0'=length_10^post7, length_19^0'=length_19^post7, lt_21^0'=lt_21^post7, result_4^0'=result_4^post7, t_17^0'=t_17^post7, tmp_13^0'=tmp_13^post7, tmp_20^0'=tmp_20^post7, tmp___0_14^0'=tmp___0_14^post7, x_18^0'=x_18^post7, (tmp_13^0-tmp_13^post7 == 0 /\ -a_16^post7+a_16^0 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post7 == 0 /\ x_18^0-x_18^post7 == 0 /\ -tmp_20^post7+tmp_20^0 == 0 /\ __disjvr_0^post7-__disjvr_0^0 == 0 /\ t_17^0-t_17^post7 == 0 /\ -length_19^post7+length_19^0 == 0 /\ -result_4^post7+result_4^0 == 0 /\ -lt_21^post7+lt_21^0 == 0 /\ -__disjvr_0^post7+__disjvr_0^0 == 0 /\ head_12^0-head_12^post7 == 0 /\ length_10^0-length_10^post7 == 0 /\ a_140^0-a_140^post7 == 0 /\ -len_47^post7+len_47^0 == 0 /\ __disjvr_1^0-__disjvr_1^post7 == 0 /\ tmp___0_14^0-tmp___0_14^post7 == 0 /\ i_11^0-i_11^post7 == 0), cost: 1 7: l7 -> l5 : __cil_tmp6_15^0'=__cil_tmp6_15^post8, __disjvr_0^0'=__disjvr_0^post8, __disjvr_1^0'=__disjvr_1^post8, a_140^0'=a_140^post8, a_16^0'=a_16^post8, head_12^0'=head_12^post8, i_11^0'=i_11^post8, len_47^0'=len_47^post8, length_10^0'=length_10^post8, length_19^0'=length_19^post8, lt_21^0'=lt_21^post8, result_4^0'=result_4^post8, t_17^0'=t_17^post8, tmp_13^0'=tmp_13^post8, tmp_20^0'=tmp_20^post8, tmp___0_14^0'=tmp___0_14^post8, x_18^0'=x_18^post8, (0 == 0 /\ tmp_20^0-tmp_20^post8 == 0 /\ -length_19^post8+length_19^0 == 0 /\ t_17^post8-x_18^0 == 0 /\ -__disjvr_0^post8+__disjvr_0^0 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post8 == 0 /\ -tmp_13^post8+tmp_13^0 == 0 /\ a_140^0-a_140^post8 == 0 /\ result_4^0-result_4^post8 == 0 /\ -lt_21^1+x_18^post8 == 0 /\ tmp___0_14^0-tmp___0_14^post8 == 0 /\ head_12^0-head_12^post8 == 0 /\ -a_16^post8+a_16^0 == 0 /\ -__disjvr_1^post8+__disjvr_1^0 == 0 /\ -i_11^post8+i_11^0 == 0 /\ len_47^0-len_47^post8 == 0 /\ length_10^0-length_10^post8 == 0), cost: 1 8: l5 -> l3 : __cil_tmp6_15^0'=__cil_tmp6_15^post9, __disjvr_0^0'=__disjvr_0^post9, __disjvr_1^0'=__disjvr_1^post9, a_140^0'=a_140^post9, a_16^0'=a_16^post9, head_12^0'=head_12^post9, i_11^0'=i_11^post9, len_47^0'=len_47^post9, length_10^0'=length_10^post9, length_19^0'=length_19^post9, lt_21^0'=lt_21^post9, result_4^0'=result_4^post9, t_17^0'=t_17^post9, tmp_13^0'=tmp_13^post9, tmp_20^0'=tmp_20^post9, tmp___0_14^0'=tmp___0_14^post9, x_18^0'=x_18^post9, (0 == 0 /\ len_47^0-len_47^post9 == 0 /\ -a_140^0 <= 0 /\ length_10^0-length_10^post9 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post9 == 0 /\ -x_18^0 <= 0 /\ lt_21^0-lt_21^post9 == 0 /\ i_11^0-i_11^post9 == 0 /\ a_140^0-a_140^post9 == 0 /\ -x_18^post9+x_18^0 == 0 /\ -tmp_20^post9+tmp_20^0 == 0 /\ tmp___0_14^0-tmp___0_14^post9 == 0 /\ t_17^0-t_17^post9 == 0 /\ x_18^0 <= 0 /\ a_16^0-a_16^post9 == 0 /\ -__disjvr_0^post9+__disjvr_0^0 == 0 /\ -length_19^post9+length_19^0 == 0 /\ -__disjvr_1^post9+__disjvr_1^0 == 0 /\ -tmp_13^post9+tmp_13^0 == 0 /\ head_12^0-head_12^post9 == 0), cost: 1 9: l5 -> l9 : __cil_tmp6_15^0'=__cil_tmp6_15^post10, __disjvr_0^0'=__disjvr_0^post10, __disjvr_1^0'=__disjvr_1^post10, a_140^0'=a_140^post10, a_16^0'=a_16^post10, head_12^0'=head_12^post10, i_11^0'=i_11^post10, len_47^0'=len_47^post10, length_10^0'=length_10^post10, length_19^0'=length_19^post10, lt_21^0'=lt_21^post10, result_4^0'=result_4^post10, t_17^0'=t_17^post10, tmp_13^0'=tmp_13^post10, tmp_20^0'=tmp_20^post10, tmp___0_14^0'=tmp___0_14^post10, x_18^0'=x_18^post10, (-tmp_13^post10+tmp_13^0 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post10 == 0 /\ -__disjvr_0^post10+__disjvr_0^0 == 0 /\ -a_140^0 <= 0 /\ -tmp___0_14^post10+tmp___0_14^0 == 0 /\ __disjvr_1^0-__disjvr_1^post10 == 0 /\ result_4^0-result_4^post10 == 0 /\ -t_17^post10+t_17^0 == 0 /\ head_12^0-head_12^post10 == 0 /\ a_140^0-a_140^post10 == 0 /\ len_47^0-len_47^post10 == 0 /\ -lt_21^post10+lt_21^0 == 0 /\ length_10^0-length_10^post10 == 0 /\ tmp_20^0-tmp_20^post10 == 0 /\ -length_19^post10+length_19^0 == 0 /\ -a_16^post10+a_16^0 == 0 /\ -x_18^post10+x_18^0 == 0 /\ -i_11^post10+i_11^0 == 0), cost: 1 10: l9 -> l10 : __cil_tmp6_15^0'=__cil_tmp6_15^post11, __disjvr_0^0'=__disjvr_0^post11, __disjvr_1^0'=__disjvr_1^post11, a_140^0'=a_140^post11, a_16^0'=a_16^post11, head_12^0'=head_12^post11, i_11^0'=i_11^post11, len_47^0'=len_47^post11, length_10^0'=length_10^post11, length_19^0'=length_19^post11, lt_21^0'=lt_21^post11, result_4^0'=result_4^post11, t_17^0'=t_17^post11, tmp_13^0'=tmp_13^post11, tmp_20^0'=tmp_20^post11, tmp___0_14^0'=tmp___0_14^post11, x_18^0'=x_18^post11, (-i_11^post11+i_11^0 == 0 /\ length_10^0-length_10^post11 == 0 /\ -x_18^post11+x_18^0 == 0 /\ -length_19^post11+length_19^0 == 0 /\ lt_21^0-lt_21^post11 == 0 /\ a_140^0-a_140^post11 == 0 /\ len_47^0-len_47^post11 == 0 /\ -result_4^post11+result_4^0 == 0 /\ -__disjvr_0^post11+__disjvr_0^0 == 0 /\ -__disjvr_1^post11+__disjvr_1^0 == 0 /\ -tmp_13^post11+tmp_13^0 == 0 /\ tmp___0_14^0-tmp___0_14^post11 == 0 /\ -head_12^post11+head_12^0 == 0 /\ a_16^0-a_16^post11 == 0 /\ tmp_20^0-tmp_20^post11 == 0 /\ __disjvr_1^post11-__disjvr_1^0 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post11 == 0 /\ t_17^0-t_17^post11 == 0), cost: 1 11: l10 -> l8 : __cil_tmp6_15^0'=__cil_tmp6_15^post12, __disjvr_0^0'=__disjvr_0^post12, __disjvr_1^0'=__disjvr_1^post12, a_140^0'=a_140^post12, a_16^0'=a_16^post12, head_12^0'=head_12^post12, i_11^0'=i_11^post12, len_47^0'=len_47^post12, length_10^0'=length_10^post12, length_19^0'=length_19^post12, lt_21^0'=lt_21^post12, result_4^0'=result_4^post12, t_17^0'=t_17^post12, tmp_13^0'=tmp_13^post12, tmp_20^0'=tmp_20^post12, tmp___0_14^0'=tmp___0_14^post12, x_18^0'=x_18^post12, (0 == 0 /\ -tmp_20^post12+tmp_20^0 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post12 == 0 /\ -__disjvr_0^post12+__disjvr_0^0 == 0 /\ -length_19^post12+length_19^0 == 0 /\ tmp_13^0-tmp_13^post12 == 0 /\ i_11^0-i_11^post12 == 0 /\ __disjvr_1^0-__disjvr_1^post12 == 0 /\ -result_4^post12+result_4^0 == 0 /\ a_140^0-a_140^post12 == 0 /\ head_12^0-head_12^post12 == 0 /\ -lt_21^1+x_18^post12 == 0 /\ tmp___0_14^0-tmp___0_14^post12 == 0 /\ length_10^0-length_10^post12 == 0 /\ -a_16^post12+a_16^0 == 0 /\ -len_47^post12+len_47^0 == 0 /\ -x_18^0+t_17^post12 == 0), cost: 1 12: l8 -> l5 : __cil_tmp6_15^0'=__cil_tmp6_15^post13, __disjvr_0^0'=__disjvr_0^post13, __disjvr_1^0'=__disjvr_1^post13, a_140^0'=a_140^post13, a_16^0'=a_16^post13, head_12^0'=head_12^post13, i_11^0'=i_11^post13, len_47^0'=len_47^post13, length_10^0'=length_10^post13, length_19^0'=length_19^post13, lt_21^0'=lt_21^post13, result_4^0'=result_4^post13, t_17^0'=t_17^post13, tmp_13^0'=tmp_13^post13, tmp_20^0'=tmp_20^post13, tmp___0_14^0'=tmp___0_14^post13, x_18^0'=x_18^post13, (__disjvr_1^0-__disjvr_1^post13 == 0 /\ length_10^0-length_10^post13 == 0 /\ tmp___0_14^0-tmp___0_14^post13 == 0 /\ lt_21^0-lt_21^post13 == 0 /\ a_140^0-a_140^post13 == 0 /\ -a_16^post13+a_16^0 == 0 /\ -tmp_20^post13+tmp_20^0 == 0 /\ -i_11^post13+i_11^0 == 0 /\ t_17^0-t_17^post13 == 0 /\ x_18^0-x_18^post13 == 0 /\ -len_47^post13+len_47^0 == 0 /\ -__cil_tmp6_15^post13+__cil_tmp6_15^0 == 0 /\ -__disjvr_0^post13+__disjvr_0^0 == 0 /\ -result_4^post13+result_4^0 == 0 /\ length_19^0-length_19^post13 == 0 /\ head_12^0-head_12^post13 == 0 /\ -tmp_13^post13+tmp_13^0 == 0), cost: 1 13: l11 -> l0 : __cil_tmp6_15^0'=__cil_tmp6_15^post14, __disjvr_0^0'=__disjvr_0^post14, __disjvr_1^0'=__disjvr_1^post14, a_140^0'=a_140^post14, a_16^0'=a_16^post14, head_12^0'=head_12^post14, i_11^0'=i_11^post14, len_47^0'=len_47^post14, length_10^0'=length_10^post14, length_19^0'=length_19^post14, lt_21^0'=lt_21^post14, result_4^0'=result_4^post14, t_17^0'=t_17^post14, tmp_13^0'=tmp_13^post14, tmp_20^0'=tmp_20^post14, tmp___0_14^0'=tmp___0_14^post14, x_18^0'=x_18^post14, (-result_4^post14+result_4^0 == 0 /\ -x_18^post14+x_18^0 == 0 /\ -len_47^post14+len_47^0 == 0 /\ -__cil_tmp6_15^post14+__cil_tmp6_15^0 == 0 /\ tmp___0_14^0-tmp___0_14^post14 == 0 /\ -tmp_13^post14+tmp_13^0 == 0 /\ head_12^0-head_12^post14 == 0 /\ -lt_21^post14+lt_21^0 == 0 /\ length_10^0-length_10^post14 == 0 /\ -a_16^post14+a_16^0 == 0 /\ -__disjvr_0^post14+__disjvr_0^0 == 0 /\ a_140^0-a_140^post14 == 0 /\ length_19^0-length_19^post14 == 0 /\ t_17^0-t_17^post14 == 0 /\ i_11^0-i_11^post14 == 0 /\ __disjvr_1^0-__disjvr_1^post14 == 0 /\ -tmp_20^post14+tmp_20^0 == 0), cost: 1 Chained Linear Paths Start location: l11 Program variables: __cil_tmp6_15^0 __disjvr_0^0 __disjvr_1^0 a_140^0 a_16^0 head_12^0 i_11^0 len_47^0 length_10^0 length_19^0 lt_21^0 result_4^0 t_17^0 tmp_13^0 tmp_20^0 tmp___0_14^0 x_18^0 1: l1 -> l2 : __cil_tmp6_15^0'=__cil_tmp6_15^post2, __disjvr_0^0'=__disjvr_0^post2, __disjvr_1^0'=__disjvr_1^post2, a_140^0'=a_140^post2, a_16^0'=a_16^post2, head_12^0'=head_12^post2, i_11^0'=i_11^post2, len_47^0'=len_47^post2, length_10^0'=length_10^post2, length_19^0'=length_19^post2, lt_21^0'=lt_21^post2, result_4^0'=result_4^post2, t_17^0'=t_17^post2, tmp_13^0'=tmp_13^post2, tmp_20^0'=tmp_20^post2, tmp___0_14^0'=tmp___0_14^post2, x_18^0'=x_18^post2, (0 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post2 == 0 /\ tmp_13^post2-tmp___0_14^post2 == 0 /\ -__disjvr_0^post2+__disjvr_0^0 == 0 /\ -tmp_13^post2+head_12^post2 == 0 /\ -result_4^post2+result_4^0 == 0 /\ __disjvr_1^0-__disjvr_1^post2 == 0 /\ tmp_20^0-tmp_20^post2 == 0 /\ -lt_21^post2+lt_21^0 == 0 /\ 2-length_10^0+i_11^0 <= 0 /\ a_140^0-a_140^post2 == 0 /\ -1-i_11^0+i_11^post2 == 0 /\ t_17^0-t_17^post2 == 0 /\ -a_16^post2+a_16^0 == 0 /\ length_10^0-length_10^post2 == 0 /\ -x_18^post2+x_18^0 == 0 /\ length_19^0-length_19^post2 == 0 /\ -len_47^post2+len_47^0 == 0), cost: 1 2: l1 -> l3 : __cil_tmp6_15^0'=__cil_tmp6_15^post3, __disjvr_0^0'=__disjvr_0^post3, __disjvr_1^0'=__disjvr_1^post3, a_140^0'=a_140^post3, a_16^0'=a_16^post3, head_12^0'=head_12^post3, i_11^0'=i_11^post3, len_47^0'=len_47^post3, length_10^0'=length_10^post3, length_19^0'=length_19^post3, lt_21^0'=lt_21^post3, result_4^0'=result_4^post3, t_17^0'=t_17^post3, tmp_13^0'=tmp_13^post3, tmp_20^0'=tmp_20^post3, tmp___0_14^0'=tmp___0_14^post3, x_18^0'=x_18^post3, (0 == 0 /\ -t_17^post3+t_17^0 == 0 /\ -tmp___0_14^post3+tmp___0_14^0 == 0 /\ -tmp_13^post3+tmp_13^0 == 0 /\ -lt_21^post3+lt_21^0 == 0 /\ -__disjvr_0^post3+__disjvr_0^0 == 0 /\ x_18^post3-a_16^0 == 0 /\ __disjvr_1^0-__disjvr_1^post3 == 0 /\ x_18^post3 <= 0 /\ -i_11^post3+i_11^0 == 0 /\ -result_4^1+tmp_20^post3 == 0 /\ len_47^0-len_47^post3 == 0 /\ -1+length_10^0-i_11^0 <= 0 /\ -length_19^post3+length_19^0 == 0 /\ -head_12^0+__cil_tmp6_15^post3 == 0 /\ length_10^0-length_10^post3 == 0 /\ -__cil_tmp6_15^post3+result_4^1 == 0 /\ -head_12^post3+head_12^0 == 0 /\ a_140^0-a_140^post3 == 0 /\ -x_18^post3 <= 0 /\ -a_16^post3+a_16^0 == 0), cost: 1 15: l2 -> l2 : __cil_tmp6_15^0'=__cil_tmp6_15^post5, __disjvr_0^0'=__disjvr_0^post5, __disjvr_1^0'=__disjvr_1^post5, a_140^0'=a_140^post5, a_16^0'=a_16^post5, head_12^0'=head_12^post5, i_11^0'=i_11^post5, len_47^0'=len_47^post5, length_10^0'=length_10^post5, length_19^0'=length_19^post5, lt_21^0'=lt_21^post5, result_4^0'=result_4^post5, t_17^0'=t_17^post5, tmp_13^0'=tmp_13^post5, tmp_20^0'=tmp_20^post5, tmp___0_14^0'=tmp___0_14^post5, x_18^0'=x_18^post5, (0 == 0 /\ -length_19^post4+length_19^0 == 0 /\ -lt_21^post5+lt_21^post4 == 0 /\ -result_4^post4+result_4^0 == 0 /\ __disjvr_0^post4-__disjvr_0^post5 == 0 /\ a_140^post4-a_140^post5 == 0 /\ -len_47^post5+len_47^post4 == 0 /\ -x_18^post4+x_18^0 == 0 /\ i_11^post4-i_11^post5 == 0 /\ __cil_tmp6_15^post4-__cil_tmp6_15^post5 == 0 /\ t_17^post4-t_17^post5 == 0 /\ -1+i_11^post4-i_11^0 == 0 /\ len_47^0-len_47^post4 == 0 /\ tmp___0_14^post4-tmp___0_14^post5 == 0 /\ -tmp_13^post5+tmp_13^post4 == 0 /\ -tmp___0_14^post4+tmp_13^post4 == 0 /\ length_10^0-length_10^post4 == 0 /\ -a_16^post5+a_16^post4 == 0 /\ length_19^post4-length_19^post5 == 0 /\ 2-length_10^0+i_11^0 <= 0 /\ a_140^0-a_140^post4 == 0 /\ head_12^post4-tmp_13^post4 == 0 /\ tmp_20^0-tmp_20^post4 == 0 /\ lt_21^0-lt_21^post4 == 0 /\ -__disjvr_1^post4+__disjvr_1^0 == 0 /\ -__disjvr_0^post4+__disjvr_0^0 == 0 /\ result_4^post4-result_4^post5 == 0 /\ head_12^post4-head_12^post5 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post4 == 0 /\ length_10^post4-length_10^post5 == 0 /\ t_17^0-t_17^post4 == 0 /\ -len_47^0 <= 0 /\ a_16^0-a_16^post4 == 0 /\ __disjvr_1^post4-__disjvr_1^post5 == 0 /\ -tmp_20^post5+tmp_20^post4 == 0 /\ x_18^post4-x_18^post5 == 0), cost: 1 17: l2 -> l5 : __cil_tmp6_15^0'=__cil_tmp6_15^post8, __disjvr_0^0'=__disjvr_0^post8, __disjvr_1^0'=__disjvr_1^post8, a_140^0'=a_140^post8, a_16^0'=a_16^post8, head_12^0'=head_12^post8, i_11^0'=i_11^post8, len_47^0'=len_47^post8, length_10^0'=length_10^post8, length_19^0'=length_19^post8, lt_21^0'=lt_21^post8, result_4^0'=result_4^post8, t_17^0'=t_17^post8, tmp_13^0'=tmp_13^post8, tmp_20^0'=tmp_20^post8, tmp___0_14^0'=tmp___0_14^post8, x_18^0'=x_18^post8, (0 == 0 /\ -__disjvr_1^post6+__disjvr_1^0 == 0 /\ tmp_20^post7-tmp_20^post8 == 0 /\ -a_16^post7+a_16^post6 == 0 /\ -__cil_tmp6_15^post8+__cil_tmp6_15^post7 == 0 /\ __cil_tmp6_15^post6-head_12^0 == 0 /\ len_47^post7-len_47^post8 == 0 /\ a_140^post6-a_140^post7 == 0 /\ -result_4^1+tmp_20^post6 == 0 /\ t_17^post6-t_17^post7 == 0 /\ __cil_tmp6_15^post6-__cil_tmp6_15^post7 == 0 /\ -__cil_tmp6_15^post6+result_4^1 == 0 /\ -len_47^post7+len_47^post6 == 0 /\ -__disjvr_1^post8+__disjvr_1^post7 == 0 /\ -i_11^post8+i_11^post7 == 0 /\ i_11^post6-i_11^post7 == 0 /\ -tmp_13^post8+tmp_13^post7 == 0 /\ length_10^0-length_10^post6 == 0 /\ head_12^post7-head_12^post8 == 0 /\ length_19^post6-length_19^post7 == 0 /\ -lt_21^post7+lt_21^post6 == 0 /\ length_10^post7-length_10^post8 == 0 /\ __disjvr_0^post7-__disjvr_0^post6 == 0 /\ -tmp___0_14^post8+tmp___0_14^post7 == 0 /\ -1+length_10^0-i_11^0 <= 0 /\ -i_11^post6+i_11^0 == 0 /\ tmp___0_14^0-tmp___0_14^post6 == 0 /\ -result_4^post7+result_4^post6 == 0 /\ -lt_21^1+x_18^post8 == 0 /\ tmp___0_14^post6-tmp___0_14^post7 == 0 /\ length_10^post6-length_10^post7 == 0 /\ lt_21^0-lt_21^post6 == 0 /\ result_4^post7-result_4^post8 == 0 /\ len_47^0-len_47^post6 == 0 /\ x_18^post6-x_18^post7 == 0 /\ __disjvr_1^post6-__disjvr_1^post7 == 0 /\ -tmp_13^post6+tmp_13^0 == 0 /\ -__disjvr_0^post6+__disjvr_0^0 == 0 /\ -__disjvr_0^post7+__disjvr_0^post6 == 0 /\ t_17^post8-x_18^post7 == 0 /\ a_16^0-a_16^post6 == 0 /\ a_140^0-a_140^post6 == 0 /\ tmp_13^post6-tmp_13^post7 == 0 /\ -a_140^post8+a_140^post7 == 0 /\ -head_12^post6+head_12^0 == 0 /\ -len_47^0 <= 0 /\ -length_19^post8+length_19^post7 == 0 /\ -tmp_20^post7+tmp_20^post6 == 0 /\ a_16^post7-a_16^post8 == 0 /\ head_12^post6-head_12^post7 == 0 /\ x_18^post6-a_16^0 == 0 /\ -length_19^post6+length_19^0 == 0 /\ __disjvr_0^post7-__disjvr_0^post8 == 0 /\ t_17^0-t_17^post6 == 0), cost: 1 8: l5 -> l3 : __cil_tmp6_15^0'=__cil_tmp6_15^post9, __disjvr_0^0'=__disjvr_0^post9, __disjvr_1^0'=__disjvr_1^post9, a_140^0'=a_140^post9, a_16^0'=a_16^post9, head_12^0'=head_12^post9, i_11^0'=i_11^post9, len_47^0'=len_47^post9, length_10^0'=length_10^post9, length_19^0'=length_19^post9, lt_21^0'=lt_21^post9, result_4^0'=result_4^post9, t_17^0'=t_17^post9, tmp_13^0'=tmp_13^post9, tmp_20^0'=tmp_20^post9, tmp___0_14^0'=tmp___0_14^post9, x_18^0'=x_18^post9, (0 == 0 /\ len_47^0-len_47^post9 == 0 /\ -a_140^0 <= 0 /\ length_10^0-length_10^post9 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post9 == 0 /\ -x_18^0 <= 0 /\ lt_21^0-lt_21^post9 == 0 /\ i_11^0-i_11^post9 == 0 /\ a_140^0-a_140^post9 == 0 /\ -x_18^post9+x_18^0 == 0 /\ -tmp_20^post9+tmp_20^0 == 0 /\ tmp___0_14^0-tmp___0_14^post9 == 0 /\ t_17^0-t_17^post9 == 0 /\ x_18^0 <= 0 /\ a_16^0-a_16^post9 == 0 /\ -__disjvr_0^post9+__disjvr_0^0 == 0 /\ -length_19^post9+length_19^0 == 0 /\ -__disjvr_1^post9+__disjvr_1^0 == 0 /\ -tmp_13^post9+tmp_13^0 == 0 /\ head_12^0-head_12^post9 == 0), cost: 1 20: l5 -> l5 : __cil_tmp6_15^0'=__cil_tmp6_15^post13, __disjvr_0^0'=__disjvr_0^post13, __disjvr_1^0'=__disjvr_1^post13, a_140^0'=a_140^post13, a_16^0'=a_16^post13, head_12^0'=head_12^post13, i_11^0'=i_11^post13, len_47^0'=len_47^post13, length_10^0'=length_10^post13, length_19^0'=length_19^post13, lt_21^0'=lt_21^post13, result_4^0'=result_4^post13, t_17^0'=t_17^post13, tmp_13^0'=tmp_13^post13, tmp_20^0'=tmp_20^post13, tmp___0_14^0'=tmp___0_14^post13, x_18^0'=x_18^post13, (0 == 0 /\ -tmp_13^post10+tmp_13^0 == 0 /\ -i_11^post13+i_11^post12 == 0 /\ __cil_tmp6_15^post11-__cil_tmp6_15^post12 == 0 /\ -length_10^post11+length_10^post10 == 0 /\ __disjvr_1^post12-__disjvr_1^post13 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post10 == 0 /\ -__disjvr_0^post10+__disjvr_0^0 == 0 /\ length_19^post12-length_19^post13 == 0 /\ -a_140^post13+a_140^post12 == 0 /\ __disjvr_0^post11-__disjvr_0^post12 == 0 /\ -a_140^0 <= 0 /\ a_140^post10-a_140^post11 == 0 /\ -result_4^post13+result_4^post12 == 0 /\ -result_4^post11+result_4^post10 == 0 /\ -x_18^post13+x_18^post12 == 0 /\ i_11^post11-i_11^post12 == 0 /\ -tmp___0_14^post10+tmp___0_14^0 == 0 /\ __disjvr_1^0-__disjvr_1^post10 == 0 /\ lt_21^post10-lt_21^post11 == 0 /\ tmp___0_14^post10-tmp___0_14^post11 == 0 /\ -__cil_tmp6_15^post13+__cil_tmp6_15^post12 == 0 /\ __cil_tmp6_15^post10-__cil_tmp6_15^post11 == 0 /\ -x_18^post11+t_17^post12 == 0 /\ -__disjvr_0^post11+__disjvr_0^post10 == 0 /\ a_140^post11-a_140^post12 == 0 /\ length_10^post11-length_10^post12 == 0 /\ head_12^post12-head_12^post13 == 0 /\ result_4^0-result_4^post10 == 0 /\ length_10^post12-length_10^post13 == 0 /\ -__disjvr_1^post11+__disjvr_1^post10 == 0 /\ -len_47^post12+len_47^post11 == 0 /\ -lt_21^post13+lt_21^post12 == 0 /\ -t_17^post13+t_17^post12 == 0 /\ -a_16^post12+a_16^post11 == 0 /\ -t_17^post10+t_17^0 == 0 /\ -tmp___0_14^post13+tmp___0_14^post12 == 0 /\ head_12^0-head_12^post10 == 0 /\ tmp___0_14^post11-tmp___0_14^post12 == 0 /\ a_140^0-a_140^post10 == 0 /\ tmp_20^post10-tmp_20^post11 == 0 /\ head_12^post11-head_12^post12 == 0 /\ -lt_21^1+x_18^post12 == 0 /\ result_4^post11-result_4^post12 == 0 /\ tmp_13^post10-tmp_13^post11 == 0 /\ i_11^post10-i_11^post11 == 0 /\ __disjvr_1^post11-__disjvr_1^post12 == 0 /\ __disjvr_1^post11-__disjvr_1^post10 == 0 /\ a_16^post10-a_16^post11 == 0 /\ -tmp_13^post13+tmp_13^post12 == 0 /\ len_47^0-len_47^post10 == 0 /\ t_17^post10-t_17^post11 == 0 /\ -lt_21^post10+lt_21^0 == 0 /\ len_47^post12-len_47^post13 == 0 /\ -tmp_20^post12+tmp_20^post11 == 0 /\ length_19^post11-length_19^post12 == 0 /\ a_16^post12-a_16^post13 == 0 /\ len_47^post10-len_47^post11 == 0 /\ length_10^0-length_10^post10 == 0 /\ x_18^post10-x_18^post11 == 0 /\ tmp_20^0-tmp_20^post10 == 0 /\ length_19^post10-length_19^post11 == 0 /\ -head_12^post11+head_12^post10 == 0 /\ tmp_13^post11-tmp_13^post12 == 0 /\ -length_19^post10+length_19^0 == 0 /\ -tmp_20^post13+tmp_20^post12 == 0 /\ -a_16^post10+a_16^0 == 0 /\ __disjvr_0^post12-__disjvr_0^post13 == 0 /\ -x_18^post10+x_18^0 == 0 /\ -i_11^post10+i_11^0 == 0), cost: 1 14: l11 -> l1 : __cil_tmp6_15^0'=__cil_tmp6_15^post1, __disjvr_0^0'=__disjvr_0^post1, __disjvr_1^0'=__disjvr_1^post1, a_140^0'=a_140^post1, a_16^0'=a_16^post1, head_12^0'=head_12^post1, i_11^0'=i_11^post1, len_47^0'=len_47^post1, length_10^0'=length_10^post1, length_19^0'=length_19^post1, lt_21^0'=lt_21^post1, result_4^0'=result_4^post1, t_17^0'=t_17^post1, tmp_13^0'=tmp_13^post1, tmp_20^0'=tmp_20^post1, tmp___0_14^0'=tmp___0_14^post1, x_18^0'=x_18^post1, (0 == 0 /\ head_12^post1 == 0 /\ -__disjvr_1^post1+__disjvr_1^post14 == 0 /\ -result_4^post14+result_4^0 == 0 /\ a_16^post14-a_16^post1 == 0 /\ -x_18^post14+x_18^0 == 0 /\ x_18^post14-x_18^post1 == 0 /\ -len_47^post14+len_47^0 == 0 /\ -tmp___0_14^post1+tmp___0_14^post14 == 0 /\ i_11^post1 == 0 /\ -__cil_tmp6_15^post14+__cil_tmp6_15^0 == 0 /\ tmp___0_14^0-tmp___0_14^post14 == 0 /\ -a_140^post1+a_140^post14 == 0 /\ tmp_20^post14-tmp_20^post1 == 0 /\ -tmp_13^post14+tmp_13^0 == 0 /\ head_12^0-head_12^post14 == 0 /\ length_10^post14-length_10^post1 == 0 /\ result_4^post14-result_4^post1 == 0 /\ __cil_tmp6_15^post14-__cil_tmp6_15^post1 == 0 /\ len_47^post14-len_47^post1 == 0 /\ -lt_21^post14+lt_21^0 == 0 /\ -t_17^post1+t_17^post14 == 0 /\ length_10^0-length_10^post14 == 0 /\ __disjvr_0^post14-__disjvr_0^post1 == 0 /\ -a_16^post14+a_16^0 == 0 /\ -__disjvr_0^post14+__disjvr_0^0 == 0 /\ tmp_13^post14-tmp_13^post1 == 0 /\ a_140^0-a_140^post14 == 0 /\ length_19^0-length_19^post14 == 0 /\ lt_21^post14-lt_21^post1 == 0 /\ t_17^0-t_17^post14 == 0 /\ i_11^0-i_11^post14 == 0 /\ __disjvr_1^0-__disjvr_1^post14 == 0 /\ -tmp_20^post14+tmp_20^0 == 0), cost: 1 Eliminating location l0 by chaining: Applied chaining First rule: l11 -> l0 : __cil_tmp6_15^0'=__cil_tmp6_15^post14, __disjvr_0^0'=__disjvr_0^post14, __disjvr_1^0'=__disjvr_1^post14, a_140^0'=a_140^post14, a_16^0'=a_16^post14, head_12^0'=head_12^post14, i_11^0'=i_11^post14, len_47^0'=len_47^post14, length_10^0'=length_10^post14, length_19^0'=length_19^post14, lt_21^0'=lt_21^post14, result_4^0'=result_4^post14, t_17^0'=t_17^post14, tmp_13^0'=tmp_13^post14, tmp_20^0'=tmp_20^post14, tmp___0_14^0'=tmp___0_14^post14, x_18^0'=x_18^post14, (-result_4^post14+result_4^0 == 0 /\ -x_18^post14+x_18^0 == 0 /\ -len_47^post14+len_47^0 == 0 /\ -__cil_tmp6_15^post14+__cil_tmp6_15^0 == 0 /\ tmp___0_14^0-tmp___0_14^post14 == 0 /\ -tmp_13^post14+tmp_13^0 == 0 /\ head_12^0-head_12^post14 == 0 /\ -lt_21^post14+lt_21^0 == 0 /\ length_10^0-length_10^post14 == 0 /\ -a_16^post14+a_16^0 == 0 /\ -__disjvr_0^post14+__disjvr_0^0 == 0 /\ a_140^0-a_140^post14 == 0 /\ length_19^0-length_19^post14 == 0 /\ t_17^0-t_17^post14 == 0 /\ i_11^0-i_11^post14 == 0 /\ __disjvr_1^0-__disjvr_1^post14 == 0 /\ -tmp_20^post14+tmp_20^0 == 0), cost: 1 Second rule: l0 -> l1 : __cil_tmp6_15^0'=__cil_tmp6_15^post1, __disjvr_0^0'=__disjvr_0^post1, __disjvr_1^0'=__disjvr_1^post1, a_140^0'=a_140^post1, a_16^0'=a_16^post1, head_12^0'=head_12^post1, i_11^0'=i_11^post1, len_47^0'=len_47^post1, length_10^0'=length_10^post1, length_19^0'=length_19^post1, lt_21^0'=lt_21^post1, result_4^0'=result_4^post1, t_17^0'=t_17^post1, tmp_13^0'=tmp_13^post1, tmp_20^0'=tmp_20^post1, tmp___0_14^0'=tmp___0_14^post1, x_18^0'=x_18^post1, (0 == 0 /\ head_12^post1 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post1 == 0 /\ -x_18^post1+x_18^0 == 0 /\ i_11^post1 == 0 /\ -a_16^post1+a_16^0 == 0 /\ len_47^0-len_47^post1 == 0 /\ tmp___0_14^0-tmp___0_14^post1 == 0 /\ -tmp_13^post1+tmp_13^0 == 0 /\ lt_21^0-lt_21^post1 == 0 /\ -__disjvr_0^post1+__disjvr_0^0 == 0 /\ length_10^0-length_10^post1 == 0 /\ -__disjvr_1^post1+__disjvr_1^0 == 0 /\ tmp_20^0-tmp_20^post1 == 0 /\ t_17^0-t_17^post1 == 0 /\ a_140^0-a_140^post1 == 0 /\ result_4^0-result_4^post1 == 0), cost: 1 New rule: l11 -> l1 : __cil_tmp6_15^0'=__cil_tmp6_15^post1, __disjvr_0^0'=__disjvr_0^post1, __disjvr_1^0'=__disjvr_1^post1, a_140^0'=a_140^post1, a_16^0'=a_16^post1, head_12^0'=head_12^post1, i_11^0'=i_11^post1, len_47^0'=len_47^post1, length_10^0'=length_10^post1, length_19^0'=length_19^post1, lt_21^0'=lt_21^post1, result_4^0'=result_4^post1, t_17^0'=t_17^post1, tmp_13^0'=tmp_13^post1, tmp_20^0'=tmp_20^post1, tmp___0_14^0'=tmp___0_14^post1, x_18^0'=x_18^post1, (0 == 0 /\ head_12^post1 == 0 /\ -__disjvr_1^post1+__disjvr_1^post14 == 0 /\ -result_4^post14+result_4^0 == 0 /\ a_16^post14-a_16^post1 == 0 /\ -x_18^post14+x_18^0 == 0 /\ x_18^post14-x_18^post1 == 0 /\ -len_47^post14+len_47^0 == 0 /\ -tmp___0_14^post1+tmp___0_14^post14 == 0 /\ i_11^post1 == 0 /\ -__cil_tmp6_15^post14+__cil_tmp6_15^0 == 0 /\ tmp___0_14^0-tmp___0_14^post14 == 0 /\ -a_140^post1+a_140^post14 == 0 /\ tmp_20^post14-tmp_20^post1 == 0 /\ -tmp_13^post14+tmp_13^0 == 0 /\ head_12^0-head_12^post14 == 0 /\ length_10^post14-length_10^post1 == 0 /\ result_4^post14-result_4^post1 == 0 /\ __cil_tmp6_15^post14-__cil_tmp6_15^post1 == 0 /\ len_47^post14-len_47^post1 == 0 /\ -lt_21^post14+lt_21^0 == 0 /\ -t_17^post1+t_17^post14 == 0 /\ length_10^0-length_10^post14 == 0 /\ __disjvr_0^post14-__disjvr_0^post1 == 0 /\ -a_16^post14+a_16^0 == 0 /\ -__disjvr_0^post14+__disjvr_0^0 == 0 /\ tmp_13^post14-tmp_13^post1 == 0 /\ a_140^0-a_140^post14 == 0 /\ length_19^0-length_19^post14 == 0 /\ lt_21^post14-lt_21^post1 == 0 /\ t_17^0-t_17^post14 == 0 /\ i_11^0-i_11^post14 == 0 /\ __disjvr_1^0-__disjvr_1^post14 == 0 /\ -tmp_20^post14+tmp_20^0 == 0), cost: 1 Applied deletion Removed the following rules: 0 13 Eliminating location l4 by chaining: Applied chaining First rule: l2 -> l4 : __cil_tmp6_15^0'=__cil_tmp6_15^post4, __disjvr_0^0'=__disjvr_0^post4, __disjvr_1^0'=__disjvr_1^post4, a_140^0'=a_140^post4, a_16^0'=a_16^post4, head_12^0'=head_12^post4, i_11^0'=i_11^post4, len_47^0'=len_47^post4, length_10^0'=length_10^post4, length_19^0'=length_19^post4, lt_21^0'=lt_21^post4, result_4^0'=result_4^post4, t_17^0'=t_17^post4, tmp_13^0'=tmp_13^post4, tmp_20^0'=tmp_20^post4, tmp___0_14^0'=tmp___0_14^post4, x_18^0'=x_18^post4, (0 == 0 /\ -length_19^post4+length_19^0 == 0 /\ -result_4^post4+result_4^0 == 0 /\ -x_18^post4+x_18^0 == 0 /\ -1+i_11^post4-i_11^0 == 0 /\ len_47^0-len_47^post4 == 0 /\ -tmp___0_14^post4+tmp_13^post4 == 0 /\ length_10^0-length_10^post4 == 0 /\ 2-length_10^0+i_11^0 <= 0 /\ a_140^0-a_140^post4 == 0 /\ head_12^post4-tmp_13^post4 == 0 /\ tmp_20^0-tmp_20^post4 == 0 /\ lt_21^0-lt_21^post4 == 0 /\ -__disjvr_1^post4+__disjvr_1^0 == 0 /\ -__disjvr_0^post4+__disjvr_0^0 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post4 == 0 /\ t_17^0-t_17^post4 == 0 /\ -len_47^0 <= 0 /\ a_16^0-a_16^post4 == 0), cost: 1 Second rule: l4 -> l2 : __cil_tmp6_15^0'=__cil_tmp6_15^post5, __disjvr_0^0'=__disjvr_0^post5, __disjvr_1^0'=__disjvr_1^post5, a_140^0'=a_140^post5, a_16^0'=a_16^post5, head_12^0'=head_12^post5, i_11^0'=i_11^post5, len_47^0'=len_47^post5, length_10^0'=length_10^post5, length_19^0'=length_19^post5, lt_21^0'=lt_21^post5, result_4^0'=result_4^post5, t_17^0'=t_17^post5, tmp_13^0'=tmp_13^post5, tmp_20^0'=tmp_20^post5, tmp___0_14^0'=tmp___0_14^post5, x_18^0'=x_18^post5, (__cil_tmp6_15^0-__cil_tmp6_15^post5 == 0 /\ t_17^0-t_17^post5 == 0 /\ -tmp_20^post5+tmp_20^0 == 0 /\ -lt_21^post5+lt_21^0 == 0 /\ x_18^0-x_18^post5 == 0 /\ -__disjvr_0^post5+__disjvr_0^0 == 0 /\ __disjvr_1^0-__disjvr_1^post5 == 0 /\ -a_16^post5+a_16^0 == 0 /\ -len_47^post5+len_47^0 == 0 /\ head_12^0-head_12^post5 == 0 /\ -length_19^post5+length_19^0 == 0 /\ -result_4^post5+result_4^0 == 0 /\ length_10^0-length_10^post5 == 0 /\ tmp___0_14^0-tmp___0_14^post5 == 0 /\ -tmp_13^post5+tmp_13^0 == 0 /\ i_11^0-i_11^post5 == 0 /\ a_140^0-a_140^post5 == 0), cost: 1 New rule: l2 -> l2 : __cil_tmp6_15^0'=__cil_tmp6_15^post5, __disjvr_0^0'=__disjvr_0^post5, __disjvr_1^0'=__disjvr_1^post5, a_140^0'=a_140^post5, a_16^0'=a_16^post5, head_12^0'=head_12^post5, i_11^0'=i_11^post5, len_47^0'=len_47^post5, length_10^0'=length_10^post5, length_19^0'=length_19^post5, lt_21^0'=lt_21^post5, result_4^0'=result_4^post5, t_17^0'=t_17^post5, tmp_13^0'=tmp_13^post5, tmp_20^0'=tmp_20^post5, tmp___0_14^0'=tmp___0_14^post5, x_18^0'=x_18^post5, (0 == 0 /\ -length_19^post4+length_19^0 == 0 /\ -lt_21^post5+lt_21^post4 == 0 /\ -result_4^post4+result_4^0 == 0 /\ __disjvr_0^post4-__disjvr_0^post5 == 0 /\ a_140^post4-a_140^post5 == 0 /\ -len_47^post5+len_47^post4 == 0 /\ -x_18^post4+x_18^0 == 0 /\ i_11^post4-i_11^post5 == 0 /\ __cil_tmp6_15^post4-__cil_tmp6_15^post5 == 0 /\ t_17^post4-t_17^post5 == 0 /\ -1+i_11^post4-i_11^0 == 0 /\ len_47^0-len_47^post4 == 0 /\ tmp___0_14^post4-tmp___0_14^post5 == 0 /\ -tmp_13^post5+tmp_13^post4 == 0 /\ -tmp___0_14^post4+tmp_13^post4 == 0 /\ length_10^0-length_10^post4 == 0 /\ -a_16^post5+a_16^post4 == 0 /\ length_19^post4-length_19^post5 == 0 /\ 2-length_10^0+i_11^0 <= 0 /\ a_140^0-a_140^post4 == 0 /\ head_12^post4-tmp_13^post4 == 0 /\ tmp_20^0-tmp_20^post4 == 0 /\ lt_21^0-lt_21^post4 == 0 /\ -__disjvr_1^post4+__disjvr_1^0 == 0 /\ -__disjvr_0^post4+__disjvr_0^0 == 0 /\ result_4^post4-result_4^post5 == 0 /\ head_12^post4-head_12^post5 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post4 == 0 /\ length_10^post4-length_10^post5 == 0 /\ t_17^0-t_17^post4 == 0 /\ -len_47^0 <= 0 /\ a_16^0-a_16^post4 == 0 /\ __disjvr_1^post4-__disjvr_1^post5 == 0 /\ -tmp_20^post5+tmp_20^post4 == 0 /\ x_18^post4-x_18^post5 == 0), cost: 1 Applied deletion Removed the following rules: 3 4 Eliminating location l6 by chaining: Applied chaining First rule: l2 -> l6 : __cil_tmp6_15^0'=__cil_tmp6_15^post6, __disjvr_0^0'=__disjvr_0^post6, __disjvr_1^0'=__disjvr_1^post6, a_140^0'=a_140^post6, a_16^0'=a_16^post6, head_12^0'=head_12^post6, i_11^0'=i_11^post6, len_47^0'=len_47^post6, length_10^0'=length_10^post6, length_19^0'=length_19^post6, lt_21^0'=lt_21^post6, result_4^0'=result_4^post6, t_17^0'=t_17^post6, tmp_13^0'=tmp_13^post6, tmp_20^0'=tmp_20^post6, tmp___0_14^0'=tmp___0_14^post6, x_18^0'=x_18^post6, (0 == 0 /\ -__disjvr_1^post6+__disjvr_1^0 == 0 /\ __cil_tmp6_15^post6-head_12^0 == 0 /\ -result_4^1+tmp_20^post6 == 0 /\ -__cil_tmp6_15^post6+result_4^1 == 0 /\ length_10^0-length_10^post6 == 0 /\ -1+length_10^0-i_11^0 <= 0 /\ -i_11^post6+i_11^0 == 0 /\ tmp___0_14^0-tmp___0_14^post6 == 0 /\ lt_21^0-lt_21^post6 == 0 /\ len_47^0-len_47^post6 == 0 /\ -tmp_13^post6+tmp_13^0 == 0 /\ -__disjvr_0^post6+__disjvr_0^0 == 0 /\ a_16^0-a_16^post6 == 0 /\ a_140^0-a_140^post6 == 0 /\ -head_12^post6+head_12^0 == 0 /\ -len_47^0 <= 0 /\ x_18^post6-a_16^0 == 0 /\ -length_19^post6+length_19^0 == 0 /\ t_17^0-t_17^post6 == 0), cost: 1 Second rule: l6 -> l7 : __cil_tmp6_15^0'=__cil_tmp6_15^post7, __disjvr_0^0'=__disjvr_0^post7, __disjvr_1^0'=__disjvr_1^post7, a_140^0'=a_140^post7, a_16^0'=a_16^post7, head_12^0'=head_12^post7, i_11^0'=i_11^post7, len_47^0'=len_47^post7, length_10^0'=length_10^post7, length_19^0'=length_19^post7, lt_21^0'=lt_21^post7, result_4^0'=result_4^post7, t_17^0'=t_17^post7, tmp_13^0'=tmp_13^post7, tmp_20^0'=tmp_20^post7, tmp___0_14^0'=tmp___0_14^post7, x_18^0'=x_18^post7, (tmp_13^0-tmp_13^post7 == 0 /\ -a_16^post7+a_16^0 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post7 == 0 /\ x_18^0-x_18^post7 == 0 /\ -tmp_20^post7+tmp_20^0 == 0 /\ __disjvr_0^post7-__disjvr_0^0 == 0 /\ t_17^0-t_17^post7 == 0 /\ -length_19^post7+length_19^0 == 0 /\ -result_4^post7+result_4^0 == 0 /\ -lt_21^post7+lt_21^0 == 0 /\ -__disjvr_0^post7+__disjvr_0^0 == 0 /\ head_12^0-head_12^post7 == 0 /\ length_10^0-length_10^post7 == 0 /\ a_140^0-a_140^post7 == 0 /\ -len_47^post7+len_47^0 == 0 /\ __disjvr_1^0-__disjvr_1^post7 == 0 /\ tmp___0_14^0-tmp___0_14^post7 == 0 /\ i_11^0-i_11^post7 == 0), cost: 1 New rule: l2 -> l7 : __cil_tmp6_15^0'=__cil_tmp6_15^post7, __disjvr_0^0'=__disjvr_0^post7, __disjvr_1^0'=__disjvr_1^post7, a_140^0'=a_140^post7, a_16^0'=a_16^post7, head_12^0'=head_12^post7, i_11^0'=i_11^post7, len_47^0'=len_47^post7, length_10^0'=length_10^post7, length_19^0'=length_19^post7, lt_21^0'=lt_21^post7, result_4^0'=result_4^post7, t_17^0'=t_17^post7, tmp_13^0'=tmp_13^post7, tmp_20^0'=tmp_20^post7, tmp___0_14^0'=tmp___0_14^post7, x_18^0'=x_18^post7, (0 == 0 /\ -__disjvr_1^post6+__disjvr_1^0 == 0 /\ -a_16^post7+a_16^post6 == 0 /\ __cil_tmp6_15^post6-head_12^0 == 0 /\ a_140^post6-a_140^post7 == 0 /\ -result_4^1+tmp_20^post6 == 0 /\ t_17^post6-t_17^post7 == 0 /\ __cil_tmp6_15^post6-__cil_tmp6_15^post7 == 0 /\ -__cil_tmp6_15^post6+result_4^1 == 0 /\ -len_47^post7+len_47^post6 == 0 /\ i_11^post6-i_11^post7 == 0 /\ length_10^0-length_10^post6 == 0 /\ length_19^post6-length_19^post7 == 0 /\ -lt_21^post7+lt_21^post6 == 0 /\ __disjvr_0^post7-__disjvr_0^post6 == 0 /\ -1+length_10^0-i_11^0 <= 0 /\ -i_11^post6+i_11^0 == 0 /\ tmp___0_14^0-tmp___0_14^post6 == 0 /\ -result_4^post7+result_4^post6 == 0 /\ tmp___0_14^post6-tmp___0_14^post7 == 0 /\ length_10^post6-length_10^post7 == 0 /\ lt_21^0-lt_21^post6 == 0 /\ len_47^0-len_47^post6 == 0 /\ x_18^post6-x_18^post7 == 0 /\ __disjvr_1^post6-__disjvr_1^post7 == 0 /\ -tmp_13^post6+tmp_13^0 == 0 /\ -__disjvr_0^post6+__disjvr_0^0 == 0 /\ -__disjvr_0^post7+__disjvr_0^post6 == 0 /\ a_16^0-a_16^post6 == 0 /\ a_140^0-a_140^post6 == 0 /\ tmp_13^post6-tmp_13^post7 == 0 /\ -head_12^post6+head_12^0 == 0 /\ -len_47^0 <= 0 /\ -tmp_20^post7+tmp_20^post6 == 0 /\ head_12^post6-head_12^post7 == 0 /\ x_18^post6-a_16^0 == 0 /\ -length_19^post6+length_19^0 == 0 /\ t_17^0-t_17^post6 == 0), cost: 1 Applied deletion Removed the following rules: 5 6 Eliminating location l7 by chaining: Applied chaining First rule: l2 -> l7 : __cil_tmp6_15^0'=__cil_tmp6_15^post7, __disjvr_0^0'=__disjvr_0^post7, __disjvr_1^0'=__disjvr_1^post7, a_140^0'=a_140^post7, a_16^0'=a_16^post7, head_12^0'=head_12^post7, i_11^0'=i_11^post7, len_47^0'=len_47^post7, length_10^0'=length_10^post7, length_19^0'=length_19^post7, lt_21^0'=lt_21^post7, result_4^0'=result_4^post7, t_17^0'=t_17^post7, tmp_13^0'=tmp_13^post7, tmp_20^0'=tmp_20^post7, tmp___0_14^0'=tmp___0_14^post7, x_18^0'=x_18^post7, (0 == 0 /\ -__disjvr_1^post6+__disjvr_1^0 == 0 /\ -a_16^post7+a_16^post6 == 0 /\ __cil_tmp6_15^post6-head_12^0 == 0 /\ a_140^post6-a_140^post7 == 0 /\ -result_4^1+tmp_20^post6 == 0 /\ t_17^post6-t_17^post7 == 0 /\ __cil_tmp6_15^post6-__cil_tmp6_15^post7 == 0 /\ -__cil_tmp6_15^post6+result_4^1 == 0 /\ -len_47^post7+len_47^post6 == 0 /\ i_11^post6-i_11^post7 == 0 /\ length_10^0-length_10^post6 == 0 /\ length_19^post6-length_19^post7 == 0 /\ -lt_21^post7+lt_21^post6 == 0 /\ __disjvr_0^post7-__disjvr_0^post6 == 0 /\ -1+length_10^0-i_11^0 <= 0 /\ -i_11^post6+i_11^0 == 0 /\ tmp___0_14^0-tmp___0_14^post6 == 0 /\ -result_4^post7+result_4^post6 == 0 /\ tmp___0_14^post6-tmp___0_14^post7 == 0 /\ length_10^post6-length_10^post7 == 0 /\ lt_21^0-lt_21^post6 == 0 /\ len_47^0-len_47^post6 == 0 /\ x_18^post6-x_18^post7 == 0 /\ __disjvr_1^post6-__disjvr_1^post7 == 0 /\ -tmp_13^post6+tmp_13^0 == 0 /\ -__disjvr_0^post6+__disjvr_0^0 == 0 /\ -__disjvr_0^post7+__disjvr_0^post6 == 0 /\ a_16^0-a_16^post6 == 0 /\ a_140^0-a_140^post6 == 0 /\ tmp_13^post6-tmp_13^post7 == 0 /\ -head_12^post6+head_12^0 == 0 /\ -len_47^0 <= 0 /\ -tmp_20^post7+tmp_20^post6 == 0 /\ head_12^post6-head_12^post7 == 0 /\ x_18^post6-a_16^0 == 0 /\ -length_19^post6+length_19^0 == 0 /\ t_17^0-t_17^post6 == 0), cost: 1 Second rule: l7 -> l5 : __cil_tmp6_15^0'=__cil_tmp6_15^post8, __disjvr_0^0'=__disjvr_0^post8, __disjvr_1^0'=__disjvr_1^post8, a_140^0'=a_140^post8, a_16^0'=a_16^post8, head_12^0'=head_12^post8, i_11^0'=i_11^post8, len_47^0'=len_47^post8, length_10^0'=length_10^post8, length_19^0'=length_19^post8, lt_21^0'=lt_21^post8, result_4^0'=result_4^post8, t_17^0'=t_17^post8, tmp_13^0'=tmp_13^post8, tmp_20^0'=tmp_20^post8, tmp___0_14^0'=tmp___0_14^post8, x_18^0'=x_18^post8, (0 == 0 /\ tmp_20^0-tmp_20^post8 == 0 /\ -length_19^post8+length_19^0 == 0 /\ t_17^post8-x_18^0 == 0 /\ -__disjvr_0^post8+__disjvr_0^0 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post8 == 0 /\ -tmp_13^post8+tmp_13^0 == 0 /\ a_140^0-a_140^post8 == 0 /\ result_4^0-result_4^post8 == 0 /\ -lt_21^1+x_18^post8 == 0 /\ tmp___0_14^0-tmp___0_14^post8 == 0 /\ head_12^0-head_12^post8 == 0 /\ -a_16^post8+a_16^0 == 0 /\ -__disjvr_1^post8+__disjvr_1^0 == 0 /\ -i_11^post8+i_11^0 == 0 /\ len_47^0-len_47^post8 == 0 /\ length_10^0-length_10^post8 == 0), cost: 1 New rule: l2 -> l5 : __cil_tmp6_15^0'=__cil_tmp6_15^post8, __disjvr_0^0'=__disjvr_0^post8, __disjvr_1^0'=__disjvr_1^post8, a_140^0'=a_140^post8, a_16^0'=a_16^post8, head_12^0'=head_12^post8, i_11^0'=i_11^post8, len_47^0'=len_47^post8, length_10^0'=length_10^post8, length_19^0'=length_19^post8, lt_21^0'=lt_21^post8, result_4^0'=result_4^post8, t_17^0'=t_17^post8, tmp_13^0'=tmp_13^post8, tmp_20^0'=tmp_20^post8, tmp___0_14^0'=tmp___0_14^post8, x_18^0'=x_18^post8, (0 == 0 /\ -__disjvr_1^post6+__disjvr_1^0 == 0 /\ tmp_20^post7-tmp_20^post8 == 0 /\ -a_16^post7+a_16^post6 == 0 /\ -__cil_tmp6_15^post8+__cil_tmp6_15^post7 == 0 /\ __cil_tmp6_15^post6-head_12^0 == 0 /\ len_47^post7-len_47^post8 == 0 /\ a_140^post6-a_140^post7 == 0 /\ -result_4^1+tmp_20^post6 == 0 /\ t_17^post6-t_17^post7 == 0 /\ __cil_tmp6_15^post6-__cil_tmp6_15^post7 == 0 /\ -__cil_tmp6_15^post6+result_4^1 == 0 /\ -len_47^post7+len_47^post6 == 0 /\ -__disjvr_1^post8+__disjvr_1^post7 == 0 /\ -i_11^post8+i_11^post7 == 0 /\ i_11^post6-i_11^post7 == 0 /\ -tmp_13^post8+tmp_13^post7 == 0 /\ length_10^0-length_10^post6 == 0 /\ head_12^post7-head_12^post8 == 0 /\ length_19^post6-length_19^post7 == 0 /\ -lt_21^post7+lt_21^post6 == 0 /\ length_10^post7-length_10^post8 == 0 /\ __disjvr_0^post7-__disjvr_0^post6 == 0 /\ -tmp___0_14^post8+tmp___0_14^post7 == 0 /\ -1+length_10^0-i_11^0 <= 0 /\ -i_11^post6+i_11^0 == 0 /\ tmp___0_14^0-tmp___0_14^post6 == 0 /\ -result_4^post7+result_4^post6 == 0 /\ -lt_21^1+x_18^post8 == 0 /\ tmp___0_14^post6-tmp___0_14^post7 == 0 /\ length_10^post6-length_10^post7 == 0 /\ lt_21^0-lt_21^post6 == 0 /\ result_4^post7-result_4^post8 == 0 /\ len_47^0-len_47^post6 == 0 /\ x_18^post6-x_18^post7 == 0 /\ __disjvr_1^post6-__disjvr_1^post7 == 0 /\ -tmp_13^post6+tmp_13^0 == 0 /\ -__disjvr_0^post6+__disjvr_0^0 == 0 /\ -__disjvr_0^post7+__disjvr_0^post6 == 0 /\ t_17^post8-x_18^post7 == 0 /\ a_16^0-a_16^post6 == 0 /\ a_140^0-a_140^post6 == 0 /\ tmp_13^post6-tmp_13^post7 == 0 /\ -a_140^post8+a_140^post7 == 0 /\ -head_12^post6+head_12^0 == 0 /\ -len_47^0 <= 0 /\ -length_19^post8+length_19^post7 == 0 /\ -tmp_20^post7+tmp_20^post6 == 0 /\ a_16^post7-a_16^post8 == 0 /\ head_12^post6-head_12^post7 == 0 /\ x_18^post6-a_16^0 == 0 /\ -length_19^post6+length_19^0 == 0 /\ __disjvr_0^post7-__disjvr_0^post8 == 0 /\ t_17^0-t_17^post6 == 0), cost: 1 Applied deletion Removed the following rules: 7 16 Eliminating location l9 by chaining: Applied chaining First rule: l5 -> l9 : __cil_tmp6_15^0'=__cil_tmp6_15^post10, __disjvr_0^0'=__disjvr_0^post10, __disjvr_1^0'=__disjvr_1^post10, a_140^0'=a_140^post10, a_16^0'=a_16^post10, head_12^0'=head_12^post10, i_11^0'=i_11^post10, len_47^0'=len_47^post10, length_10^0'=length_10^post10, length_19^0'=length_19^post10, lt_21^0'=lt_21^post10, result_4^0'=result_4^post10, t_17^0'=t_17^post10, tmp_13^0'=tmp_13^post10, tmp_20^0'=tmp_20^post10, tmp___0_14^0'=tmp___0_14^post10, x_18^0'=x_18^post10, (-tmp_13^post10+tmp_13^0 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post10 == 0 /\ -__disjvr_0^post10+__disjvr_0^0 == 0 /\ -a_140^0 <= 0 /\ -tmp___0_14^post10+tmp___0_14^0 == 0 /\ __disjvr_1^0-__disjvr_1^post10 == 0 /\ result_4^0-result_4^post10 == 0 /\ -t_17^post10+t_17^0 == 0 /\ head_12^0-head_12^post10 == 0 /\ a_140^0-a_140^post10 == 0 /\ len_47^0-len_47^post10 == 0 /\ -lt_21^post10+lt_21^0 == 0 /\ length_10^0-length_10^post10 == 0 /\ tmp_20^0-tmp_20^post10 == 0 /\ -length_19^post10+length_19^0 == 0 /\ -a_16^post10+a_16^0 == 0 /\ -x_18^post10+x_18^0 == 0 /\ -i_11^post10+i_11^0 == 0), cost: 1 Second rule: l9 -> l10 : __cil_tmp6_15^0'=__cil_tmp6_15^post11, __disjvr_0^0'=__disjvr_0^post11, __disjvr_1^0'=__disjvr_1^post11, a_140^0'=a_140^post11, a_16^0'=a_16^post11, head_12^0'=head_12^post11, i_11^0'=i_11^post11, len_47^0'=len_47^post11, length_10^0'=length_10^post11, length_19^0'=length_19^post11, lt_21^0'=lt_21^post11, result_4^0'=result_4^post11, t_17^0'=t_17^post11, tmp_13^0'=tmp_13^post11, tmp_20^0'=tmp_20^post11, tmp___0_14^0'=tmp___0_14^post11, x_18^0'=x_18^post11, (-i_11^post11+i_11^0 == 0 /\ length_10^0-length_10^post11 == 0 /\ -x_18^post11+x_18^0 == 0 /\ -length_19^post11+length_19^0 == 0 /\ lt_21^0-lt_21^post11 == 0 /\ a_140^0-a_140^post11 == 0 /\ len_47^0-len_47^post11 == 0 /\ -result_4^post11+result_4^0 == 0 /\ -__disjvr_0^post11+__disjvr_0^0 == 0 /\ -__disjvr_1^post11+__disjvr_1^0 == 0 /\ -tmp_13^post11+tmp_13^0 == 0 /\ tmp___0_14^0-tmp___0_14^post11 == 0 /\ -head_12^post11+head_12^0 == 0 /\ a_16^0-a_16^post11 == 0 /\ tmp_20^0-tmp_20^post11 == 0 /\ __disjvr_1^post11-__disjvr_1^0 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post11 == 0 /\ t_17^0-t_17^post11 == 0), cost: 1 New rule: l5 -> l10 : __cil_tmp6_15^0'=__cil_tmp6_15^post11, __disjvr_0^0'=__disjvr_0^post11, __disjvr_1^0'=__disjvr_1^post11, a_140^0'=a_140^post11, a_16^0'=a_16^post11, head_12^0'=head_12^post11, i_11^0'=i_11^post11, len_47^0'=len_47^post11, length_10^0'=length_10^post11, length_19^0'=length_19^post11, lt_21^0'=lt_21^post11, result_4^0'=result_4^post11, t_17^0'=t_17^post11, tmp_13^0'=tmp_13^post11, tmp_20^0'=tmp_20^post11, tmp___0_14^0'=tmp___0_14^post11, x_18^0'=x_18^post11, (-tmp_13^post10+tmp_13^0 == 0 /\ -length_10^post11+length_10^post10 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post10 == 0 /\ -__disjvr_0^post10+__disjvr_0^0 == 0 /\ -a_140^0 <= 0 /\ a_140^post10-a_140^post11 == 0 /\ -result_4^post11+result_4^post10 == 0 /\ -tmp___0_14^post10+tmp___0_14^0 == 0 /\ __disjvr_1^0-__disjvr_1^post10 == 0 /\ lt_21^post10-lt_21^post11 == 0 /\ tmp___0_14^post10-tmp___0_14^post11 == 0 /\ __cil_tmp6_15^post10-__cil_tmp6_15^post11 == 0 /\ -__disjvr_0^post11+__disjvr_0^post10 == 0 /\ result_4^0-result_4^post10 == 0 /\ -__disjvr_1^post11+__disjvr_1^post10 == 0 /\ -t_17^post10+t_17^0 == 0 /\ head_12^0-head_12^post10 == 0 /\ a_140^0-a_140^post10 == 0 /\ tmp_20^post10-tmp_20^post11 == 0 /\ tmp_13^post10-tmp_13^post11 == 0 /\ i_11^post10-i_11^post11 == 0 /\ __disjvr_1^post11-__disjvr_1^post10 == 0 /\ a_16^post10-a_16^post11 == 0 /\ len_47^0-len_47^post10 == 0 /\ t_17^post10-t_17^post11 == 0 /\ -lt_21^post10+lt_21^0 == 0 /\ len_47^post10-len_47^post11 == 0 /\ length_10^0-length_10^post10 == 0 /\ x_18^post10-x_18^post11 == 0 /\ tmp_20^0-tmp_20^post10 == 0 /\ length_19^post10-length_19^post11 == 0 /\ -head_12^post11+head_12^post10 == 0 /\ -length_19^post10+length_19^0 == 0 /\ -a_16^post10+a_16^0 == 0 /\ -x_18^post10+x_18^0 == 0 /\ -i_11^post10+i_11^0 == 0), cost: 1 Applied deletion Removed the following rules: 9 10 Eliminating location l10 by chaining: Applied chaining First rule: l5 -> l10 : __cil_tmp6_15^0'=__cil_tmp6_15^post11, __disjvr_0^0'=__disjvr_0^post11, __disjvr_1^0'=__disjvr_1^post11, a_140^0'=a_140^post11, a_16^0'=a_16^post11, head_12^0'=head_12^post11, i_11^0'=i_11^post11, len_47^0'=len_47^post11, length_10^0'=length_10^post11, length_19^0'=length_19^post11, lt_21^0'=lt_21^post11, result_4^0'=result_4^post11, t_17^0'=t_17^post11, tmp_13^0'=tmp_13^post11, tmp_20^0'=tmp_20^post11, tmp___0_14^0'=tmp___0_14^post11, x_18^0'=x_18^post11, (-tmp_13^post10+tmp_13^0 == 0 /\ -length_10^post11+length_10^post10 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post10 == 0 /\ -__disjvr_0^post10+__disjvr_0^0 == 0 /\ -a_140^0 <= 0 /\ a_140^post10-a_140^post11 == 0 /\ -result_4^post11+result_4^post10 == 0 /\ -tmp___0_14^post10+tmp___0_14^0 == 0 /\ __disjvr_1^0-__disjvr_1^post10 == 0 /\ lt_21^post10-lt_21^post11 == 0 /\ tmp___0_14^post10-tmp___0_14^post11 == 0 /\ __cil_tmp6_15^post10-__cil_tmp6_15^post11 == 0 /\ -__disjvr_0^post11+__disjvr_0^post10 == 0 /\ result_4^0-result_4^post10 == 0 /\ -__disjvr_1^post11+__disjvr_1^post10 == 0 /\ -t_17^post10+t_17^0 == 0 /\ head_12^0-head_12^post10 == 0 /\ a_140^0-a_140^post10 == 0 /\ tmp_20^post10-tmp_20^post11 == 0 /\ tmp_13^post10-tmp_13^post11 == 0 /\ i_11^post10-i_11^post11 == 0 /\ __disjvr_1^post11-__disjvr_1^post10 == 0 /\ a_16^post10-a_16^post11 == 0 /\ len_47^0-len_47^post10 == 0 /\ t_17^post10-t_17^post11 == 0 /\ -lt_21^post10+lt_21^0 == 0 /\ len_47^post10-len_47^post11 == 0 /\ length_10^0-length_10^post10 == 0 /\ x_18^post10-x_18^post11 == 0 /\ tmp_20^0-tmp_20^post10 == 0 /\ length_19^post10-length_19^post11 == 0 /\ -head_12^post11+head_12^post10 == 0 /\ -length_19^post10+length_19^0 == 0 /\ -a_16^post10+a_16^0 == 0 /\ -x_18^post10+x_18^0 == 0 /\ -i_11^post10+i_11^0 == 0), cost: 1 Second rule: l10 -> l8 : __cil_tmp6_15^0'=__cil_tmp6_15^post12, __disjvr_0^0'=__disjvr_0^post12, __disjvr_1^0'=__disjvr_1^post12, a_140^0'=a_140^post12, a_16^0'=a_16^post12, head_12^0'=head_12^post12, i_11^0'=i_11^post12, len_47^0'=len_47^post12, length_10^0'=length_10^post12, length_19^0'=length_19^post12, lt_21^0'=lt_21^post12, result_4^0'=result_4^post12, t_17^0'=t_17^post12, tmp_13^0'=tmp_13^post12, tmp_20^0'=tmp_20^post12, tmp___0_14^0'=tmp___0_14^post12, x_18^0'=x_18^post12, (0 == 0 /\ -tmp_20^post12+tmp_20^0 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post12 == 0 /\ -__disjvr_0^post12+__disjvr_0^0 == 0 /\ -length_19^post12+length_19^0 == 0 /\ tmp_13^0-tmp_13^post12 == 0 /\ i_11^0-i_11^post12 == 0 /\ __disjvr_1^0-__disjvr_1^post12 == 0 /\ -result_4^post12+result_4^0 == 0 /\ a_140^0-a_140^post12 == 0 /\ head_12^0-head_12^post12 == 0 /\ -lt_21^1+x_18^post12 == 0 /\ tmp___0_14^0-tmp___0_14^post12 == 0 /\ length_10^0-length_10^post12 == 0 /\ -a_16^post12+a_16^0 == 0 /\ -len_47^post12+len_47^0 == 0 /\ -x_18^0+t_17^post12 == 0), cost: 1 New rule: l5 -> l8 : __cil_tmp6_15^0'=__cil_tmp6_15^post12, __disjvr_0^0'=__disjvr_0^post12, __disjvr_1^0'=__disjvr_1^post12, a_140^0'=a_140^post12, a_16^0'=a_16^post12, head_12^0'=head_12^post12, i_11^0'=i_11^post12, len_47^0'=len_47^post12, length_10^0'=length_10^post12, length_19^0'=length_19^post12, lt_21^0'=lt_21^post12, result_4^0'=result_4^post12, t_17^0'=t_17^post12, tmp_13^0'=tmp_13^post12, tmp_20^0'=tmp_20^post12, tmp___0_14^0'=tmp___0_14^post12, x_18^0'=x_18^post12, (0 == 0 /\ -tmp_13^post10+tmp_13^0 == 0 /\ __cil_tmp6_15^post11-__cil_tmp6_15^post12 == 0 /\ -length_10^post11+length_10^post10 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post10 == 0 /\ -__disjvr_0^post10+__disjvr_0^0 == 0 /\ __disjvr_0^post11-__disjvr_0^post12 == 0 /\ -a_140^0 <= 0 /\ a_140^post10-a_140^post11 == 0 /\ -result_4^post11+result_4^post10 == 0 /\ i_11^post11-i_11^post12 == 0 /\ -tmp___0_14^post10+tmp___0_14^0 == 0 /\ __disjvr_1^0-__disjvr_1^post10 == 0 /\ lt_21^post10-lt_21^post11 == 0 /\ tmp___0_14^post10-tmp___0_14^post11 == 0 /\ __cil_tmp6_15^post10-__cil_tmp6_15^post11 == 0 /\ -x_18^post11+t_17^post12 == 0 /\ -__disjvr_0^post11+__disjvr_0^post10 == 0 /\ a_140^post11-a_140^post12 == 0 /\ length_10^post11-length_10^post12 == 0 /\ result_4^0-result_4^post10 == 0 /\ -__disjvr_1^post11+__disjvr_1^post10 == 0 /\ -len_47^post12+len_47^post11 == 0 /\ -a_16^post12+a_16^post11 == 0 /\ -t_17^post10+t_17^0 == 0 /\ head_12^0-head_12^post10 == 0 /\ tmp___0_14^post11-tmp___0_14^post12 == 0 /\ a_140^0-a_140^post10 == 0 /\ tmp_20^post10-tmp_20^post11 == 0 /\ head_12^post11-head_12^post12 == 0 /\ -lt_21^1+x_18^post12 == 0 /\ result_4^post11-result_4^post12 == 0 /\ tmp_13^post10-tmp_13^post11 == 0 /\ i_11^post10-i_11^post11 == 0 /\ __disjvr_1^post11-__disjvr_1^post12 == 0 /\ __disjvr_1^post11-__disjvr_1^post10 == 0 /\ a_16^post10-a_16^post11 == 0 /\ len_47^0-len_47^post10 == 0 /\ t_17^post10-t_17^post11 == 0 /\ -lt_21^post10+lt_21^0 == 0 /\ -tmp_20^post12+tmp_20^post11 == 0 /\ length_19^post11-length_19^post12 == 0 /\ len_47^post10-len_47^post11 == 0 /\ length_10^0-length_10^post10 == 0 /\ x_18^post10-x_18^post11 == 0 /\ tmp_20^0-tmp_20^post10 == 0 /\ length_19^post10-length_19^post11 == 0 /\ -head_12^post11+head_12^post10 == 0 /\ tmp_13^post11-tmp_13^post12 == 0 /\ -length_19^post10+length_19^0 == 0 /\ -a_16^post10+a_16^0 == 0 /\ -x_18^post10+x_18^0 == 0 /\ -i_11^post10+i_11^0 == 0), cost: 1 Applied deletion Removed the following rules: 11 18 Eliminating location l8 by chaining: Applied chaining First rule: l5 -> l8 : __cil_tmp6_15^0'=__cil_tmp6_15^post12, __disjvr_0^0'=__disjvr_0^post12, __disjvr_1^0'=__disjvr_1^post12, a_140^0'=a_140^post12, a_16^0'=a_16^post12, head_12^0'=head_12^post12, i_11^0'=i_11^post12, len_47^0'=len_47^post12, length_10^0'=length_10^post12, length_19^0'=length_19^post12, lt_21^0'=lt_21^post12, result_4^0'=result_4^post12, t_17^0'=t_17^post12, tmp_13^0'=tmp_13^post12, tmp_20^0'=tmp_20^post12, tmp___0_14^0'=tmp___0_14^post12, x_18^0'=x_18^post12, (0 == 0 /\ -tmp_13^post10+tmp_13^0 == 0 /\ __cil_tmp6_15^post11-__cil_tmp6_15^post12 == 0 /\ -length_10^post11+length_10^post10 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post10 == 0 /\ -__disjvr_0^post10+__disjvr_0^0 == 0 /\ __disjvr_0^post11-__disjvr_0^post12 == 0 /\ -a_140^0 <= 0 /\ a_140^post10-a_140^post11 == 0 /\ -result_4^post11+result_4^post10 == 0 /\ i_11^post11-i_11^post12 == 0 /\ -tmp___0_14^post10+tmp___0_14^0 == 0 /\ __disjvr_1^0-__disjvr_1^post10 == 0 /\ lt_21^post10-lt_21^post11 == 0 /\ tmp___0_14^post10-tmp___0_14^post11 == 0 /\ __cil_tmp6_15^post10-__cil_tmp6_15^post11 == 0 /\ -x_18^post11+t_17^post12 == 0 /\ -__disjvr_0^post11+__disjvr_0^post10 == 0 /\ a_140^post11-a_140^post12 == 0 /\ length_10^post11-length_10^post12 == 0 /\ result_4^0-result_4^post10 == 0 /\ -__disjvr_1^post11+__disjvr_1^post10 == 0 /\ -len_47^post12+len_47^post11 == 0 /\ -a_16^post12+a_16^post11 == 0 /\ -t_17^post10+t_17^0 == 0 /\ head_12^0-head_12^post10 == 0 /\ tmp___0_14^post11-tmp___0_14^post12 == 0 /\ a_140^0-a_140^post10 == 0 /\ tmp_20^post10-tmp_20^post11 == 0 /\ head_12^post11-head_12^post12 == 0 /\ -lt_21^1+x_18^post12 == 0 /\ result_4^post11-result_4^post12 == 0 /\ tmp_13^post10-tmp_13^post11 == 0 /\ i_11^post10-i_11^post11 == 0 /\ __disjvr_1^post11-__disjvr_1^post12 == 0 /\ __disjvr_1^post11-__disjvr_1^post10 == 0 /\ a_16^post10-a_16^post11 == 0 /\ len_47^0-len_47^post10 == 0 /\ t_17^post10-t_17^post11 == 0 /\ -lt_21^post10+lt_21^0 == 0 /\ -tmp_20^post12+tmp_20^post11 == 0 /\ length_19^post11-length_19^post12 == 0 /\ len_47^post10-len_47^post11 == 0 /\ length_10^0-length_10^post10 == 0 /\ x_18^post10-x_18^post11 == 0 /\ tmp_20^0-tmp_20^post10 == 0 /\ length_19^post10-length_19^post11 == 0 /\ -head_12^post11+head_12^post10 == 0 /\ tmp_13^post11-tmp_13^post12 == 0 /\ -length_19^post10+length_19^0 == 0 /\ -a_16^post10+a_16^0 == 0 /\ -x_18^post10+x_18^0 == 0 /\ -i_11^post10+i_11^0 == 0), cost: 1 Second rule: l8 -> l5 : __cil_tmp6_15^0'=__cil_tmp6_15^post13, __disjvr_0^0'=__disjvr_0^post13, __disjvr_1^0'=__disjvr_1^post13, a_140^0'=a_140^post13, a_16^0'=a_16^post13, head_12^0'=head_12^post13, i_11^0'=i_11^post13, len_47^0'=len_47^post13, length_10^0'=length_10^post13, length_19^0'=length_19^post13, lt_21^0'=lt_21^post13, result_4^0'=result_4^post13, t_17^0'=t_17^post13, tmp_13^0'=tmp_13^post13, tmp_20^0'=tmp_20^post13, tmp___0_14^0'=tmp___0_14^post13, x_18^0'=x_18^post13, (__disjvr_1^0-__disjvr_1^post13 == 0 /\ length_10^0-length_10^post13 == 0 /\ tmp___0_14^0-tmp___0_14^post13 == 0 /\ lt_21^0-lt_21^post13 == 0 /\ a_140^0-a_140^post13 == 0 /\ -a_16^post13+a_16^0 == 0 /\ -tmp_20^post13+tmp_20^0 == 0 /\ -i_11^post13+i_11^0 == 0 /\ t_17^0-t_17^post13 == 0 /\ x_18^0-x_18^post13 == 0 /\ -len_47^post13+len_47^0 == 0 /\ -__cil_tmp6_15^post13+__cil_tmp6_15^0 == 0 /\ -__disjvr_0^post13+__disjvr_0^0 == 0 /\ -result_4^post13+result_4^0 == 0 /\ length_19^0-length_19^post13 == 0 /\ head_12^0-head_12^post13 == 0 /\ -tmp_13^post13+tmp_13^0 == 0), cost: 1 New rule: l5 -> l5 : __cil_tmp6_15^0'=__cil_tmp6_15^post13, __disjvr_0^0'=__disjvr_0^post13, __disjvr_1^0'=__disjvr_1^post13, a_140^0'=a_140^post13, a_16^0'=a_16^post13, head_12^0'=head_12^post13, i_11^0'=i_11^post13, len_47^0'=len_47^post13, length_10^0'=length_10^post13, length_19^0'=length_19^post13, lt_21^0'=lt_21^post13, result_4^0'=result_4^post13, t_17^0'=t_17^post13, tmp_13^0'=tmp_13^post13, tmp_20^0'=tmp_20^post13, tmp___0_14^0'=tmp___0_14^post13, x_18^0'=x_18^post13, (0 == 0 /\ -tmp_13^post10+tmp_13^0 == 0 /\ -i_11^post13+i_11^post12 == 0 /\ __cil_tmp6_15^post11-__cil_tmp6_15^post12 == 0 /\ -length_10^post11+length_10^post10 == 0 /\ __disjvr_1^post12-__disjvr_1^post13 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post10 == 0 /\ -__disjvr_0^post10+__disjvr_0^0 == 0 /\ length_19^post12-length_19^post13 == 0 /\ -a_140^post13+a_140^post12 == 0 /\ __disjvr_0^post11-__disjvr_0^post12 == 0 /\ -a_140^0 <= 0 /\ a_140^post10-a_140^post11 == 0 /\ -result_4^post13+result_4^post12 == 0 /\ -result_4^post11+result_4^post10 == 0 /\ -x_18^post13+x_18^post12 == 0 /\ i_11^post11-i_11^post12 == 0 /\ -tmp___0_14^post10+tmp___0_14^0 == 0 /\ __disjvr_1^0-__disjvr_1^post10 == 0 /\ lt_21^post10-lt_21^post11 == 0 /\ tmp___0_14^post10-tmp___0_14^post11 == 0 /\ -__cil_tmp6_15^post13+__cil_tmp6_15^post12 == 0 /\ __cil_tmp6_15^post10-__cil_tmp6_15^post11 == 0 /\ -x_18^post11+t_17^post12 == 0 /\ -__disjvr_0^post11+__disjvr_0^post10 == 0 /\ a_140^post11-a_140^post12 == 0 /\ length_10^post11-length_10^post12 == 0 /\ head_12^post12-head_12^post13 == 0 /\ result_4^0-result_4^post10 == 0 /\ length_10^post12-length_10^post13 == 0 /\ -__disjvr_1^post11+__disjvr_1^post10 == 0 /\ -len_47^post12+len_47^post11 == 0 /\ -lt_21^post13+lt_21^post12 == 0 /\ -t_17^post13+t_17^post12 == 0 /\ -a_16^post12+a_16^post11 == 0 /\ -t_17^post10+t_17^0 == 0 /\ -tmp___0_14^post13+tmp___0_14^post12 == 0 /\ head_12^0-head_12^post10 == 0 /\ tmp___0_14^post11-tmp___0_14^post12 == 0 /\ a_140^0-a_140^post10 == 0 /\ tmp_20^post10-tmp_20^post11 == 0 /\ head_12^post11-head_12^post12 == 0 /\ -lt_21^1+x_18^post12 == 0 /\ result_4^post11-result_4^post12 == 0 /\ tmp_13^post10-tmp_13^post11 == 0 /\ i_11^post10-i_11^post11 == 0 /\ __disjvr_1^post11-__disjvr_1^post12 == 0 /\ __disjvr_1^post11-__disjvr_1^post10 == 0 /\ a_16^post10-a_16^post11 == 0 /\ -tmp_13^post13+tmp_13^post12 == 0 /\ len_47^0-len_47^post10 == 0 /\ t_17^post10-t_17^post11 == 0 /\ -lt_21^post10+lt_21^0 == 0 /\ len_47^post12-len_47^post13 == 0 /\ -tmp_20^post12+tmp_20^post11 == 0 /\ length_19^post11-length_19^post12 == 0 /\ a_16^post12-a_16^post13 == 0 /\ len_47^post10-len_47^post11 == 0 /\ length_10^0-length_10^post10 == 0 /\ x_18^post10-x_18^post11 == 0 /\ tmp_20^0-tmp_20^post10 == 0 /\ length_19^post10-length_19^post11 == 0 /\ -head_12^post11+head_12^post10 == 0 /\ tmp_13^post11-tmp_13^post12 == 0 /\ -length_19^post10+length_19^0 == 0 /\ -tmp_20^post13+tmp_20^post12 == 0 /\ -a_16^post10+a_16^0 == 0 /\ __disjvr_0^post12-__disjvr_0^post13 == 0 /\ -x_18^post10+x_18^0 == 0 /\ -i_11^post10+i_11^0 == 0), cost: 1 Applied deletion Removed the following rules: 12 19 Simplified Transitions Start location: l11 Program variables: __cil_tmp6_15^0 a_140^0 a_16^0 head_12^0 i_11^0 len_47^0 length_10^0 length_19^0 lt_21^0 result_4^0 t_17^0 tmp_13^0 tmp_20^0 tmp___0_14^0 x_18^0 21: l1 -> l2 : head_12^0'=tmp___0_14^post2, i_11^0'=1+i_11^0, tmp_13^0'=tmp___0_14^post2, tmp___0_14^0'=tmp___0_14^post2, 2-length_10^0+i_11^0 <= 0, cost: 1 22: l1 -> l3 : __cil_tmp6_15^0'=head_12^0, result_4^0'=result_4^post3, tmp_20^0'=head_12^0, x_18^0'=a_16^0, (-1+length_10^0-i_11^0 <= 0 /\ -a_16^0 <= 0 /\ a_16^0 <= 0 /\ a_16^0 == 0), cost: 1 25: l2 -> l2 : head_12^0'=tmp___0_14^post4, i_11^0'=1+i_11^0, tmp_13^0'=tmp___0_14^post4, tmp___0_14^0'=tmp___0_14^post4, (2-length_10^0+i_11^0 <= 0 /\ -len_47^0 <= 0), cost: 1 26: l2 -> l5 : __cil_tmp6_15^0'=head_12^0, lt_21^0'=lt_21^post8, result_4^0'=result_4^post7, t_17^0'=a_16^0, tmp_20^0'=head_12^0, x_18^0'=lt_21^1, (-1+length_10^0-i_11^0 <= 0 /\ -len_47^0 <= 0), cost: 1 23: l5 -> l3 : result_4^0'=result_4^post9, (-a_140^0 <= 0 /\ -x_18^0 <= 0 /\ -x_18^0 == 0 /\ x_18^0 <= 0), cost: 1 27: l5 -> l5 : lt_21^0'=lt_21^post12, t_17^0'=x_18^0, x_18^0'=x_18^post12, -a_140^0 <= 0, cost: 1 24: l11 -> l1 : head_12^0'=0, i_11^0'=0, length_19^0'=length_19^post1, T, cost: 1 Propagated Equalities Original rule: l1 -> l2 : __cil_tmp6_15^0'=__cil_tmp6_15^post2, __disjvr_0^0'=__disjvr_0^post2, __disjvr_1^0'=__disjvr_1^post2, a_140^0'=a_140^post2, a_16^0'=a_16^post2, head_12^0'=head_12^post2, i_11^0'=i_11^post2, len_47^0'=len_47^post2, length_10^0'=length_10^post2, length_19^0'=length_19^post2, lt_21^0'=lt_21^post2, result_4^0'=result_4^post2, t_17^0'=t_17^post2, tmp_13^0'=tmp_13^post2, tmp_20^0'=tmp_20^post2, tmp___0_14^0'=tmp___0_14^post2, x_18^0'=x_18^post2, (0 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post2 == 0 /\ tmp_13^post2-tmp___0_14^post2 == 0 /\ -__disjvr_0^post2+__disjvr_0^0 == 0 /\ -tmp_13^post2+head_12^post2 == 0 /\ -result_4^post2+result_4^0 == 0 /\ __disjvr_1^0-__disjvr_1^post2 == 0 /\ tmp_20^0-tmp_20^post2 == 0 /\ -lt_21^post2+lt_21^0 == 0 /\ 2-length_10^0+i_11^0 <= 0 /\ a_140^0-a_140^post2 == 0 /\ -1-i_11^0+i_11^post2 == 0 /\ t_17^0-t_17^post2 == 0 /\ -a_16^post2+a_16^0 == 0 /\ length_10^0-length_10^post2 == 0 /\ -x_18^post2+x_18^0 == 0 /\ length_19^0-length_19^post2 == 0 /\ -len_47^post2+len_47^0 == 0), cost: 1 New rule: l1 -> l2 : __cil_tmp6_15^0'=__cil_tmp6_15^0, __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, a_140^0'=a_140^0, a_16^0'=a_16^0, head_12^0'=tmp___0_14^post2, i_11^0'=1+i_11^0, len_47^0'=len_47^0, length_10^0'=length_10^0, length_19^0'=length_19^0, lt_21^0'=lt_21^0, result_4^0'=result_4^0, t_17^0'=t_17^0, tmp_13^0'=tmp___0_14^post2, tmp_20^0'=tmp_20^0, tmp___0_14^0'=tmp___0_14^post2, x_18^0'=x_18^0, (0 == 0 /\ 2-length_10^0+i_11^0 <= 0), cost: 1 propagated equality __cil_tmp6_15^post2 = __cil_tmp6_15^0 propagated equality tmp_13^post2 = tmp___0_14^post2 propagated equality __disjvr_0^post2 = __disjvr_0^0 propagated equality head_12^post2 = tmp___0_14^post2 propagated equality result_4^post2 = result_4^0 propagated equality __disjvr_1^post2 = __disjvr_1^0 propagated equality tmp_20^post2 = tmp_20^0 propagated equality lt_21^post2 = lt_21^0 propagated equality a_140^post2 = a_140^0 propagated equality i_11^post2 = 1+i_11^0 propagated equality t_17^post2 = t_17^0 propagated equality a_16^post2 = a_16^0 propagated equality length_10^post2 = length_10^0 propagated equality x_18^post2 = x_18^0 propagated equality length_19^post2 = length_19^0 propagated equality len_47^post2 = len_47^0 Simplified Guard Original rule: l1 -> l2 : __cil_tmp6_15^0'=__cil_tmp6_15^0, __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, a_140^0'=a_140^0, a_16^0'=a_16^0, head_12^0'=tmp___0_14^post2, i_11^0'=1+i_11^0, len_47^0'=len_47^0, length_10^0'=length_10^0, length_19^0'=length_19^0, lt_21^0'=lt_21^0, result_4^0'=result_4^0, t_17^0'=t_17^0, tmp_13^0'=tmp___0_14^post2, tmp_20^0'=tmp_20^0, tmp___0_14^0'=tmp___0_14^post2, x_18^0'=x_18^0, (0 == 0 /\ 2-length_10^0+i_11^0 <= 0), cost: 1 New rule: l1 -> l2 : __cil_tmp6_15^0'=__cil_tmp6_15^0, __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, a_140^0'=a_140^0, a_16^0'=a_16^0, head_12^0'=tmp___0_14^post2, i_11^0'=1+i_11^0, len_47^0'=len_47^0, length_10^0'=length_10^0, length_19^0'=length_19^0, lt_21^0'=lt_21^0, result_4^0'=result_4^0, t_17^0'=t_17^0, tmp_13^0'=tmp___0_14^post2, tmp_20^0'=tmp_20^0, tmp___0_14^0'=tmp___0_14^post2, x_18^0'=x_18^0, 2-length_10^0+i_11^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l1 -> l2 : __cil_tmp6_15^0'=__cil_tmp6_15^0, __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, a_140^0'=a_140^0, a_16^0'=a_16^0, head_12^0'=tmp___0_14^post2, i_11^0'=1+i_11^0, len_47^0'=len_47^0, length_10^0'=length_10^0, length_19^0'=length_19^0, lt_21^0'=lt_21^0, result_4^0'=result_4^0, t_17^0'=t_17^0, tmp_13^0'=tmp___0_14^post2, tmp_20^0'=tmp_20^0, tmp___0_14^0'=tmp___0_14^post2, x_18^0'=x_18^0, 2-length_10^0+i_11^0 <= 0, cost: 1 New rule: l1 -> l2 : head_12^0'=tmp___0_14^post2, i_11^0'=1+i_11^0, tmp_13^0'=tmp___0_14^post2, tmp___0_14^0'=tmp___0_14^post2, 2-length_10^0+i_11^0 <= 0, cost: 1 made implied equalities explicit Original rule: l1 -> l3 : __cil_tmp6_15^0'=__cil_tmp6_15^post3, __disjvr_0^0'=__disjvr_0^post3, __disjvr_1^0'=__disjvr_1^post3, a_140^0'=a_140^post3, a_16^0'=a_16^post3, head_12^0'=head_12^post3, i_11^0'=i_11^post3, len_47^0'=len_47^post3, length_10^0'=length_10^post3, length_19^0'=length_19^post3, lt_21^0'=lt_21^post3, result_4^0'=result_4^post3, t_17^0'=t_17^post3, tmp_13^0'=tmp_13^post3, tmp_20^0'=tmp_20^post3, tmp___0_14^0'=tmp___0_14^post3, x_18^0'=x_18^post3, (0 == 0 /\ -t_17^post3+t_17^0 == 0 /\ -tmp___0_14^post3+tmp___0_14^0 == 0 /\ -tmp_13^post3+tmp_13^0 == 0 /\ -lt_21^post3+lt_21^0 == 0 /\ -__disjvr_0^post3+__disjvr_0^0 == 0 /\ x_18^post3-a_16^0 == 0 /\ __disjvr_1^0-__disjvr_1^post3 == 0 /\ x_18^post3 <= 0 /\ -i_11^post3+i_11^0 == 0 /\ -result_4^1+tmp_20^post3 == 0 /\ len_47^0-len_47^post3 == 0 /\ -1+length_10^0-i_11^0 <= 0 /\ -length_19^post3+length_19^0 == 0 /\ -head_12^0+__cil_tmp6_15^post3 == 0 /\ length_10^0-length_10^post3 == 0 /\ -__cil_tmp6_15^post3+result_4^1 == 0 /\ -head_12^post3+head_12^0 == 0 /\ a_140^0-a_140^post3 == 0 /\ -x_18^post3 <= 0 /\ -a_16^post3+a_16^0 == 0), cost: 1 New rule: l1 -> l3 : __cil_tmp6_15^0'=__cil_tmp6_15^post3, __disjvr_0^0'=__disjvr_0^post3, __disjvr_1^0'=__disjvr_1^post3, a_140^0'=a_140^post3, a_16^0'=a_16^post3, head_12^0'=head_12^post3, i_11^0'=i_11^post3, len_47^0'=len_47^post3, length_10^0'=length_10^post3, length_19^0'=length_19^post3, lt_21^0'=lt_21^post3, result_4^0'=result_4^post3, t_17^0'=t_17^post3, tmp_13^0'=tmp_13^post3, tmp_20^0'=tmp_20^post3, tmp___0_14^0'=tmp___0_14^post3, x_18^0'=x_18^post3, (0 == 0 /\ -t_17^post3+t_17^0 == 0 /\ -tmp___0_14^post3+tmp___0_14^0 == 0 /\ -tmp_13^post3+tmp_13^0 == 0 /\ -lt_21^post3+lt_21^0 == 0 /\ -__disjvr_0^post3+__disjvr_0^0 == 0 /\ x_18^post3-a_16^0 == 0 /\ __disjvr_1^0-__disjvr_1^post3 == 0 /\ x_18^post3 <= 0 /\ x_18^post3 == 0 /\ -i_11^post3+i_11^0 == 0 /\ -result_4^1+tmp_20^post3 == 0 /\ len_47^0-len_47^post3 == 0 /\ -1+length_10^0-i_11^0 <= 0 /\ -length_19^post3+length_19^0 == 0 /\ -head_12^0+__cil_tmp6_15^post3 == 0 /\ length_10^0-length_10^post3 == 0 /\ -__cil_tmp6_15^post3+result_4^1 == 0 /\ -head_12^post3+head_12^0 == 0 /\ a_140^0-a_140^post3 == 0 /\ -x_18^post3 <= 0 /\ -a_16^post3+a_16^0 == 0), cost: 1 Propagated Equalities Original rule: l1 -> l3 : __cil_tmp6_15^0'=__cil_tmp6_15^post3, __disjvr_0^0'=__disjvr_0^post3, __disjvr_1^0'=__disjvr_1^post3, a_140^0'=a_140^post3, a_16^0'=a_16^post3, head_12^0'=head_12^post3, i_11^0'=i_11^post3, len_47^0'=len_47^post3, length_10^0'=length_10^post3, length_19^0'=length_19^post3, lt_21^0'=lt_21^post3, result_4^0'=result_4^post3, t_17^0'=t_17^post3, tmp_13^0'=tmp_13^post3, tmp_20^0'=tmp_20^post3, tmp___0_14^0'=tmp___0_14^post3, x_18^0'=x_18^post3, (0 == 0 /\ -t_17^post3+t_17^0 == 0 /\ -tmp___0_14^post3+tmp___0_14^0 == 0 /\ -tmp_13^post3+tmp_13^0 == 0 /\ -lt_21^post3+lt_21^0 == 0 /\ -__disjvr_0^post3+__disjvr_0^0 == 0 /\ x_18^post3-a_16^0 == 0 /\ __disjvr_1^0-__disjvr_1^post3 == 0 /\ x_18^post3 <= 0 /\ x_18^post3 == 0 /\ -i_11^post3+i_11^0 == 0 /\ -result_4^1+tmp_20^post3 == 0 /\ len_47^0-len_47^post3 == 0 /\ -1+length_10^0-i_11^0 <= 0 /\ -length_19^post3+length_19^0 == 0 /\ -head_12^0+__cil_tmp6_15^post3 == 0 /\ length_10^0-length_10^post3 == 0 /\ -__cil_tmp6_15^post3+result_4^1 == 0 /\ -head_12^post3+head_12^0 == 0 /\ a_140^0-a_140^post3 == 0 /\ -x_18^post3 <= 0 /\ -a_16^post3+a_16^0 == 0), cost: 1 New rule: l1 -> l3 : __cil_tmp6_15^0'=head_12^0, __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, a_140^0'=a_140^0, a_16^0'=a_16^0, head_12^0'=head_12^0, i_11^0'=i_11^0, len_47^0'=len_47^0, length_10^0'=length_10^0, length_19^0'=length_19^0, lt_21^0'=lt_21^0, result_4^0'=result_4^post3, t_17^0'=t_17^0, tmp_13^0'=tmp_13^0, tmp_20^0'=result_4^1, tmp___0_14^0'=tmp___0_14^0, x_18^0'=a_16^0, (0 == 0 /\ -1+length_10^0-i_11^0 <= 0 /\ -a_16^0 <= 0 /\ -head_12^0+result_4^1 == 0 /\ a_16^0 <= 0 /\ a_16^0 == 0), cost: 1 propagated equality t_17^post3 = t_17^0 propagated equality tmp___0_14^post3 = tmp___0_14^0 propagated equality tmp_13^post3 = tmp_13^0 propagated equality lt_21^post3 = lt_21^0 propagated equality __disjvr_0^post3 = __disjvr_0^0 propagated equality x_18^post3 = a_16^0 propagated equality __disjvr_1^post3 = __disjvr_1^0 propagated equality i_11^post3 = i_11^0 propagated equality tmp_20^post3 = result_4^1 propagated equality len_47^post3 = len_47^0 propagated equality length_19^post3 = length_19^0 propagated equality __cil_tmp6_15^post3 = head_12^0 propagated equality length_10^post3 = length_10^0 propagated equality head_12^post3 = head_12^0 propagated equality a_140^post3 = a_140^0 propagated equality a_16^post3 = a_16^0 Propagated Equalities Original rule: l1 -> l3 : __cil_tmp6_15^0'=head_12^0, __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, a_140^0'=a_140^0, a_16^0'=a_16^0, head_12^0'=head_12^0, i_11^0'=i_11^0, len_47^0'=len_47^0, length_10^0'=length_10^0, length_19^0'=length_19^0, lt_21^0'=lt_21^0, result_4^0'=result_4^post3, t_17^0'=t_17^0, tmp_13^0'=tmp_13^0, tmp_20^0'=result_4^1, tmp___0_14^0'=tmp___0_14^0, x_18^0'=a_16^0, (0 == 0 /\ -1+length_10^0-i_11^0 <= 0 /\ -a_16^0 <= 0 /\ -head_12^0+result_4^1 == 0 /\ a_16^0 <= 0 /\ a_16^0 == 0), cost: 1 New rule: l1 -> l3 : __cil_tmp6_15^0'=head_12^0, __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, a_140^0'=a_140^0, a_16^0'=a_16^0, head_12^0'=head_12^0, i_11^0'=i_11^0, len_47^0'=len_47^0, length_10^0'=length_10^0, length_19^0'=length_19^0, lt_21^0'=lt_21^0, result_4^0'=result_4^post3, t_17^0'=t_17^0, tmp_13^0'=tmp_13^0, tmp_20^0'=head_12^0, tmp___0_14^0'=tmp___0_14^0, x_18^0'=a_16^0, (0 == 0 /\ -1+length_10^0-i_11^0 <= 0 /\ -a_16^0 <= 0 /\ a_16^0 <= 0 /\ a_16^0 == 0), cost: 1 propagated equality result_4^1 = head_12^0 Simplified Guard Original rule: l1 -> l3 : __cil_tmp6_15^0'=head_12^0, __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, a_140^0'=a_140^0, a_16^0'=a_16^0, head_12^0'=head_12^0, i_11^0'=i_11^0, len_47^0'=len_47^0, length_10^0'=length_10^0, length_19^0'=length_19^0, lt_21^0'=lt_21^0, result_4^0'=result_4^post3, t_17^0'=t_17^0, tmp_13^0'=tmp_13^0, tmp_20^0'=head_12^0, tmp___0_14^0'=tmp___0_14^0, x_18^0'=a_16^0, (0 == 0 /\ -1+length_10^0-i_11^0 <= 0 /\ -a_16^0 <= 0 /\ a_16^0 <= 0 /\ a_16^0 == 0), cost: 1 New rule: l1 -> l3 : __cil_tmp6_15^0'=head_12^0, __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, a_140^0'=a_140^0, a_16^0'=a_16^0, head_12^0'=head_12^0, i_11^0'=i_11^0, len_47^0'=len_47^0, length_10^0'=length_10^0, length_19^0'=length_19^0, lt_21^0'=lt_21^0, result_4^0'=result_4^post3, t_17^0'=t_17^0, tmp_13^0'=tmp_13^0, tmp_20^0'=head_12^0, tmp___0_14^0'=tmp___0_14^0, x_18^0'=a_16^0, (-1+length_10^0-i_11^0 <= 0 /\ -a_16^0 <= 0 /\ a_16^0 <= 0 /\ a_16^0 == 0), cost: 1 made implied equalities explicit Original rule: l1 -> l3 : __cil_tmp6_15^0'=head_12^0, __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, a_140^0'=a_140^0, a_16^0'=a_16^0, head_12^0'=head_12^0, i_11^0'=i_11^0, len_47^0'=len_47^0, length_10^0'=length_10^0, length_19^0'=length_19^0, lt_21^0'=lt_21^0, result_4^0'=result_4^post3, t_17^0'=t_17^0, tmp_13^0'=tmp_13^0, tmp_20^0'=head_12^0, tmp___0_14^0'=tmp___0_14^0, x_18^0'=a_16^0, (-1+length_10^0-i_11^0 <= 0 /\ -a_16^0 <= 0 /\ a_16^0 <= 0 /\ a_16^0 == 0), cost: 1 New rule: l1 -> l3 : __cil_tmp6_15^0'=head_12^0, __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, a_140^0'=a_140^0, a_16^0'=a_16^0, head_12^0'=head_12^0, i_11^0'=i_11^0, len_47^0'=len_47^0, length_10^0'=length_10^0, length_19^0'=length_19^0, lt_21^0'=lt_21^0, result_4^0'=result_4^post3, t_17^0'=t_17^0, tmp_13^0'=tmp_13^0, tmp_20^0'=head_12^0, tmp___0_14^0'=tmp___0_14^0, x_18^0'=a_16^0, (-1+length_10^0-i_11^0 <= 0 /\ -a_16^0 <= 0 /\ -a_16^0 == 0 /\ a_16^0 <= 0 /\ a_16^0 == 0), cost: 1 Removed Trivial Updates Original rule: l1 -> l3 : __cil_tmp6_15^0'=head_12^0, __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, a_140^0'=a_140^0, a_16^0'=a_16^0, head_12^0'=head_12^0, i_11^0'=i_11^0, len_47^0'=len_47^0, length_10^0'=length_10^0, length_19^0'=length_19^0, lt_21^0'=lt_21^0, result_4^0'=result_4^post3, t_17^0'=t_17^0, tmp_13^0'=tmp_13^0, tmp_20^0'=head_12^0, tmp___0_14^0'=tmp___0_14^0, x_18^0'=a_16^0, (-1+length_10^0-i_11^0 <= 0 /\ -a_16^0 <= 0 /\ a_16^0 <= 0 /\ a_16^0 == 0), cost: 1 New rule: l1 -> l3 : __cil_tmp6_15^0'=head_12^0, result_4^0'=result_4^post3, tmp_20^0'=head_12^0, x_18^0'=a_16^0, (-1+length_10^0-i_11^0 <= 0 /\ -a_16^0 <= 0 /\ a_16^0 <= 0 /\ a_16^0 == 0), cost: 1 made implied equalities explicit Original rule: l5 -> l3 : __cil_tmp6_15^0'=__cil_tmp6_15^post9, __disjvr_0^0'=__disjvr_0^post9, __disjvr_1^0'=__disjvr_1^post9, a_140^0'=a_140^post9, a_16^0'=a_16^post9, head_12^0'=head_12^post9, i_11^0'=i_11^post9, len_47^0'=len_47^post9, length_10^0'=length_10^post9, length_19^0'=length_19^post9, lt_21^0'=lt_21^post9, result_4^0'=result_4^post9, t_17^0'=t_17^post9, tmp_13^0'=tmp_13^post9, tmp_20^0'=tmp_20^post9, tmp___0_14^0'=tmp___0_14^post9, x_18^0'=x_18^post9, (0 == 0 /\ len_47^0-len_47^post9 == 0 /\ -a_140^0 <= 0 /\ length_10^0-length_10^post9 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post9 == 0 /\ -x_18^0 <= 0 /\ lt_21^0-lt_21^post9 == 0 /\ i_11^0-i_11^post9 == 0 /\ a_140^0-a_140^post9 == 0 /\ -x_18^post9+x_18^0 == 0 /\ -tmp_20^post9+tmp_20^0 == 0 /\ tmp___0_14^0-tmp___0_14^post9 == 0 /\ t_17^0-t_17^post9 == 0 /\ x_18^0 <= 0 /\ a_16^0-a_16^post9 == 0 /\ -__disjvr_0^post9+__disjvr_0^0 == 0 /\ -length_19^post9+length_19^0 == 0 /\ -__disjvr_1^post9+__disjvr_1^0 == 0 /\ -tmp_13^post9+tmp_13^0 == 0 /\ head_12^0-head_12^post9 == 0), cost: 1 New rule: l5 -> l3 : __cil_tmp6_15^0'=__cil_tmp6_15^post9, __disjvr_0^0'=__disjvr_0^post9, __disjvr_1^0'=__disjvr_1^post9, a_140^0'=a_140^post9, a_16^0'=a_16^post9, head_12^0'=head_12^post9, i_11^0'=i_11^post9, len_47^0'=len_47^post9, length_10^0'=length_10^post9, length_19^0'=length_19^post9, lt_21^0'=lt_21^post9, result_4^0'=result_4^post9, t_17^0'=t_17^post9, tmp_13^0'=tmp_13^post9, tmp_20^0'=tmp_20^post9, tmp___0_14^0'=tmp___0_14^post9, x_18^0'=x_18^post9, (0 == 0 /\ len_47^0-len_47^post9 == 0 /\ -a_140^0 <= 0 /\ length_10^0-length_10^post9 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post9 == 0 /\ -x_18^0 <= 0 /\ -x_18^0 == 0 /\ lt_21^0-lt_21^post9 == 0 /\ i_11^0-i_11^post9 == 0 /\ a_140^0-a_140^post9 == 0 /\ -x_18^post9+x_18^0 == 0 /\ -tmp_20^post9+tmp_20^0 == 0 /\ tmp___0_14^0-tmp___0_14^post9 == 0 /\ t_17^0-t_17^post9 == 0 /\ x_18^0 <= 0 /\ a_16^0-a_16^post9 == 0 /\ -__disjvr_0^post9+__disjvr_0^0 == 0 /\ -length_19^post9+length_19^0 == 0 /\ -__disjvr_1^post9+__disjvr_1^0 == 0 /\ -tmp_13^post9+tmp_13^0 == 0 /\ head_12^0-head_12^post9 == 0), cost: 1 Propagated Equalities Original rule: l5 -> l3 : __cil_tmp6_15^0'=__cil_tmp6_15^post9, __disjvr_0^0'=__disjvr_0^post9, __disjvr_1^0'=__disjvr_1^post9, a_140^0'=a_140^post9, a_16^0'=a_16^post9, head_12^0'=head_12^post9, i_11^0'=i_11^post9, len_47^0'=len_47^post9, length_10^0'=length_10^post9, length_19^0'=length_19^post9, lt_21^0'=lt_21^post9, result_4^0'=result_4^post9, t_17^0'=t_17^post9, tmp_13^0'=tmp_13^post9, tmp_20^0'=tmp_20^post9, tmp___0_14^0'=tmp___0_14^post9, x_18^0'=x_18^post9, (0 == 0 /\ len_47^0-len_47^post9 == 0 /\ -a_140^0 <= 0 /\ length_10^0-length_10^post9 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post9 == 0 /\ -x_18^0 <= 0 /\ -x_18^0 == 0 /\ lt_21^0-lt_21^post9 == 0 /\ i_11^0-i_11^post9 == 0 /\ a_140^0-a_140^post9 == 0 /\ -x_18^post9+x_18^0 == 0 /\ -tmp_20^post9+tmp_20^0 == 0 /\ tmp___0_14^0-tmp___0_14^post9 == 0 /\ t_17^0-t_17^post9 == 0 /\ x_18^0 <= 0 /\ a_16^0-a_16^post9 == 0 /\ -__disjvr_0^post9+__disjvr_0^0 == 0 /\ -length_19^post9+length_19^0 == 0 /\ -__disjvr_1^post9+__disjvr_1^0 == 0 /\ -tmp_13^post9+tmp_13^0 == 0 /\ head_12^0-head_12^post9 == 0), cost: 1 New rule: l5 -> l3 : __cil_tmp6_15^0'=__cil_tmp6_15^0, __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, a_140^0'=a_140^0, a_16^0'=a_16^0, head_12^0'=head_12^0, i_11^0'=i_11^0, len_47^0'=len_47^0, length_10^0'=length_10^0, length_19^0'=length_19^0, lt_21^0'=lt_21^0, result_4^0'=result_4^post9, t_17^0'=t_17^0, tmp_13^0'=tmp_13^0, tmp_20^0'=tmp_20^0, tmp___0_14^0'=tmp___0_14^0, x_18^0'=x_18^0, (0 == 0 /\ -a_140^0 <= 0 /\ -x_18^0 <= 0 /\ -x_18^0 == 0 /\ x_18^0 <= 0), cost: 1 propagated equality len_47^post9 = len_47^0 propagated equality length_10^post9 = length_10^0 propagated equality __cil_tmp6_15^post9 = __cil_tmp6_15^0 propagated equality lt_21^post9 = lt_21^0 propagated equality i_11^post9 = i_11^0 propagated equality a_140^post9 = a_140^0 propagated equality x_18^post9 = x_18^0 propagated equality tmp_20^post9 = tmp_20^0 propagated equality tmp___0_14^post9 = tmp___0_14^0 propagated equality t_17^post9 = t_17^0 propagated equality a_16^post9 = a_16^0 propagated equality __disjvr_0^post9 = __disjvr_0^0 propagated equality length_19^post9 = length_19^0 propagated equality __disjvr_1^post9 = __disjvr_1^0 propagated equality tmp_13^post9 = tmp_13^0 propagated equality head_12^post9 = head_12^0 Simplified Guard Original rule: l5 -> l3 : __cil_tmp6_15^0'=__cil_tmp6_15^0, __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, a_140^0'=a_140^0, a_16^0'=a_16^0, head_12^0'=head_12^0, i_11^0'=i_11^0, len_47^0'=len_47^0, length_10^0'=length_10^0, length_19^0'=length_19^0, lt_21^0'=lt_21^0, result_4^0'=result_4^post9, t_17^0'=t_17^0, tmp_13^0'=tmp_13^0, tmp_20^0'=tmp_20^0, tmp___0_14^0'=tmp___0_14^0, x_18^0'=x_18^0, (0 == 0 /\ -a_140^0 <= 0 /\ -x_18^0 <= 0 /\ -x_18^0 == 0 /\ x_18^0 <= 0), cost: 1 New rule: l5 -> l3 : __cil_tmp6_15^0'=__cil_tmp6_15^0, __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, a_140^0'=a_140^0, a_16^0'=a_16^0, head_12^0'=head_12^0, i_11^0'=i_11^0, len_47^0'=len_47^0, length_10^0'=length_10^0, length_19^0'=length_19^0, lt_21^0'=lt_21^0, result_4^0'=result_4^post9, t_17^0'=t_17^0, tmp_13^0'=tmp_13^0, tmp_20^0'=tmp_20^0, tmp___0_14^0'=tmp___0_14^0, x_18^0'=x_18^0, (-a_140^0 <= 0 /\ -x_18^0 <= 0 /\ -x_18^0 == 0 /\ x_18^0 <= 0), cost: 1 made implied equalities explicit Original rule: l5 -> l3 : __cil_tmp6_15^0'=__cil_tmp6_15^0, __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, a_140^0'=a_140^0, a_16^0'=a_16^0, head_12^0'=head_12^0, i_11^0'=i_11^0, len_47^0'=len_47^0, length_10^0'=length_10^0, length_19^0'=length_19^0, lt_21^0'=lt_21^0, result_4^0'=result_4^post9, t_17^0'=t_17^0, tmp_13^0'=tmp_13^0, tmp_20^0'=tmp_20^0, tmp___0_14^0'=tmp___0_14^0, x_18^0'=x_18^0, (-a_140^0 <= 0 /\ -x_18^0 <= 0 /\ -x_18^0 == 0 /\ x_18^0 <= 0), cost: 1 New rule: l5 -> l3 : __cil_tmp6_15^0'=__cil_tmp6_15^0, __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, a_140^0'=a_140^0, a_16^0'=a_16^0, head_12^0'=head_12^0, i_11^0'=i_11^0, len_47^0'=len_47^0, length_10^0'=length_10^0, length_19^0'=length_19^0, lt_21^0'=lt_21^0, result_4^0'=result_4^post9, t_17^0'=t_17^0, tmp_13^0'=tmp_13^0, tmp_20^0'=tmp_20^0, tmp___0_14^0'=tmp___0_14^0, x_18^0'=x_18^0, (-a_140^0 <= 0 /\ -x_18^0 <= 0 /\ -x_18^0 == 0 /\ x_18^0 <= 0), cost: 1 Removed Trivial Updates Original rule: l5 -> l3 : __cil_tmp6_15^0'=__cil_tmp6_15^0, __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, a_140^0'=a_140^0, a_16^0'=a_16^0, head_12^0'=head_12^0, i_11^0'=i_11^0, len_47^0'=len_47^0, length_10^0'=length_10^0, length_19^0'=length_19^0, lt_21^0'=lt_21^0, result_4^0'=result_4^post9, t_17^0'=t_17^0, tmp_13^0'=tmp_13^0, tmp_20^0'=tmp_20^0, tmp___0_14^0'=tmp___0_14^0, x_18^0'=x_18^0, (-a_140^0 <= 0 /\ -x_18^0 <= 0 /\ -x_18^0 == 0 /\ x_18^0 <= 0), cost: 1 New rule: l5 -> l3 : result_4^0'=result_4^post9, (-a_140^0 <= 0 /\ -x_18^0 <= 0 /\ -x_18^0 == 0 /\ x_18^0 <= 0), cost: 1 Propagated Equalities Original rule: l11 -> l1 : __cil_tmp6_15^0'=__cil_tmp6_15^post1, __disjvr_0^0'=__disjvr_0^post1, __disjvr_1^0'=__disjvr_1^post1, a_140^0'=a_140^post1, a_16^0'=a_16^post1, head_12^0'=head_12^post1, i_11^0'=i_11^post1, len_47^0'=len_47^post1, length_10^0'=length_10^post1, length_19^0'=length_19^post1, lt_21^0'=lt_21^post1, result_4^0'=result_4^post1, t_17^0'=t_17^post1, tmp_13^0'=tmp_13^post1, tmp_20^0'=tmp_20^post1, tmp___0_14^0'=tmp___0_14^post1, x_18^0'=x_18^post1, (0 == 0 /\ head_12^post1 == 0 /\ -__disjvr_1^post1+__disjvr_1^post14 == 0 /\ -result_4^post14+result_4^0 == 0 /\ a_16^post14-a_16^post1 == 0 /\ -x_18^post14+x_18^0 == 0 /\ x_18^post14-x_18^post1 == 0 /\ -len_47^post14+len_47^0 == 0 /\ -tmp___0_14^post1+tmp___0_14^post14 == 0 /\ i_11^post1 == 0 /\ -__cil_tmp6_15^post14+__cil_tmp6_15^0 == 0 /\ tmp___0_14^0-tmp___0_14^post14 == 0 /\ -a_140^post1+a_140^post14 == 0 /\ tmp_20^post14-tmp_20^post1 == 0 /\ -tmp_13^post14+tmp_13^0 == 0 /\ head_12^0-head_12^post14 == 0 /\ length_10^post14-length_10^post1 == 0 /\ result_4^post14-result_4^post1 == 0 /\ __cil_tmp6_15^post14-__cil_tmp6_15^post1 == 0 /\ len_47^post14-len_47^post1 == 0 /\ -lt_21^post14+lt_21^0 == 0 /\ -t_17^post1+t_17^post14 == 0 /\ length_10^0-length_10^post14 == 0 /\ __disjvr_0^post14-__disjvr_0^post1 == 0 /\ -a_16^post14+a_16^0 == 0 /\ -__disjvr_0^post14+__disjvr_0^0 == 0 /\ tmp_13^post14-tmp_13^post1 == 0 /\ a_140^0-a_140^post14 == 0 /\ length_19^0-length_19^post14 == 0 /\ lt_21^post14-lt_21^post1 == 0 /\ t_17^0-t_17^post14 == 0 /\ i_11^0-i_11^post14 == 0 /\ __disjvr_1^0-__disjvr_1^post14 == 0 /\ -tmp_20^post14+tmp_20^0 == 0), cost: 1 New rule: l11 -> l1 : __cil_tmp6_15^0'=__cil_tmp6_15^post14, __disjvr_0^0'=__disjvr_0^post14, __disjvr_1^0'=__disjvr_1^post14, a_140^0'=a_140^post14, a_16^0'=a_16^post14, head_12^0'=0, i_11^0'=0, len_47^0'=len_47^post14, length_10^0'=length_10^post14, length_19^0'=length_19^post1, lt_21^0'=lt_21^post14, result_4^0'=result_4^post14, t_17^0'=t_17^post14, tmp_13^0'=tmp_13^post14, tmp_20^0'=tmp_20^post14, tmp___0_14^0'=tmp___0_14^post14, x_18^0'=x_18^post14, (0 == 0 /\ -result_4^post14+result_4^0 == 0 /\ -x_18^post14+x_18^0 == 0 /\ -len_47^post14+len_47^0 == 0 /\ -__cil_tmp6_15^post14+__cil_tmp6_15^0 == 0 /\ tmp___0_14^0-tmp___0_14^post14 == 0 /\ -tmp_13^post14+tmp_13^0 == 0 /\ head_12^0-head_12^post14 == 0 /\ -lt_21^post14+lt_21^0 == 0 /\ length_10^0-length_10^post14 == 0 /\ -a_16^post14+a_16^0 == 0 /\ -__disjvr_0^post14+__disjvr_0^0 == 0 /\ a_140^0-a_140^post14 == 0 /\ length_19^0-length_19^post14 == 0 /\ t_17^0-t_17^post14 == 0 /\ i_11^0-i_11^post14 == 0 /\ __disjvr_1^0-__disjvr_1^post14 == 0 /\ -tmp_20^post14+tmp_20^0 == 0), cost: 1 propagated equality head_12^post1 = 0 propagated equality __disjvr_1^post1 = __disjvr_1^post14 propagated equality a_16^post1 = a_16^post14 propagated equality x_18^post1 = x_18^post14 propagated equality tmp___0_14^post1 = tmp___0_14^post14 propagated equality i_11^post1 = 0 propagated equality a_140^post1 = a_140^post14 propagated equality tmp_20^post1 = tmp_20^post14 propagated equality length_10^post1 = length_10^post14 propagated equality result_4^post1 = result_4^post14 propagated equality __cil_tmp6_15^post1 = __cil_tmp6_15^post14 propagated equality len_47^post1 = len_47^post14 propagated equality t_17^post1 = t_17^post14 propagated equality __disjvr_0^post1 = __disjvr_0^post14 propagated equality tmp_13^post1 = tmp_13^post14 propagated equality lt_21^post1 = lt_21^post14 Propagated Equalities Original rule: l11 -> l1 : __cil_tmp6_15^0'=__cil_tmp6_15^post14, __disjvr_0^0'=__disjvr_0^post14, __disjvr_1^0'=__disjvr_1^post14, a_140^0'=a_140^post14, a_16^0'=a_16^post14, head_12^0'=0, i_11^0'=0, len_47^0'=len_47^post14, length_10^0'=length_10^post14, length_19^0'=length_19^post1, lt_21^0'=lt_21^post14, result_4^0'=result_4^post14, t_17^0'=t_17^post14, tmp_13^0'=tmp_13^post14, tmp_20^0'=tmp_20^post14, tmp___0_14^0'=tmp___0_14^post14, x_18^0'=x_18^post14, (0 == 0 /\ -result_4^post14+result_4^0 == 0 /\ -x_18^post14+x_18^0 == 0 /\ -len_47^post14+len_47^0 == 0 /\ -__cil_tmp6_15^post14+__cil_tmp6_15^0 == 0 /\ tmp___0_14^0-tmp___0_14^post14 == 0 /\ -tmp_13^post14+tmp_13^0 == 0 /\ head_12^0-head_12^post14 == 0 /\ -lt_21^post14+lt_21^0 == 0 /\ length_10^0-length_10^post14 == 0 /\ -a_16^post14+a_16^0 == 0 /\ -__disjvr_0^post14+__disjvr_0^0 == 0 /\ a_140^0-a_140^post14 == 0 /\ length_19^0-length_19^post14 == 0 /\ t_17^0-t_17^post14 == 0 /\ i_11^0-i_11^post14 == 0 /\ __disjvr_1^0-__disjvr_1^post14 == 0 /\ -tmp_20^post14+tmp_20^0 == 0), cost: 1 New rule: l11 -> l1 : __cil_tmp6_15^0'=__cil_tmp6_15^0, __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, a_140^0'=a_140^0, a_16^0'=a_16^0, head_12^0'=0, i_11^0'=0, len_47^0'=len_47^0, length_10^0'=length_10^0, length_19^0'=length_19^post1, lt_21^0'=lt_21^0, result_4^0'=result_4^0, t_17^0'=t_17^0, tmp_13^0'=tmp_13^0, tmp_20^0'=tmp_20^0, tmp___0_14^0'=tmp___0_14^0, x_18^0'=x_18^0, 0 == 0, cost: 1 propagated equality result_4^post14 = result_4^0 propagated equality x_18^post14 = x_18^0 propagated equality len_47^post14 = len_47^0 propagated equality __cil_tmp6_15^post14 = __cil_tmp6_15^0 propagated equality tmp___0_14^post14 = tmp___0_14^0 propagated equality tmp_13^post14 = tmp_13^0 propagated equality head_12^post14 = head_12^0 propagated equality lt_21^post14 = lt_21^0 propagated equality length_10^post14 = length_10^0 propagated equality a_16^post14 = a_16^0 propagated equality __disjvr_0^post14 = __disjvr_0^0 propagated equality a_140^post14 = a_140^0 propagated equality length_19^post14 = length_19^0 propagated equality t_17^post14 = t_17^0 propagated equality i_11^post14 = i_11^0 propagated equality __disjvr_1^post14 = __disjvr_1^0 propagated equality tmp_20^post14 = tmp_20^0 Simplified Guard Original rule: l11 -> l1 : __cil_tmp6_15^0'=__cil_tmp6_15^0, __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, a_140^0'=a_140^0, a_16^0'=a_16^0, head_12^0'=0, i_11^0'=0, len_47^0'=len_47^0, length_10^0'=length_10^0, length_19^0'=length_19^post1, lt_21^0'=lt_21^0, result_4^0'=result_4^0, t_17^0'=t_17^0, tmp_13^0'=tmp_13^0, tmp_20^0'=tmp_20^0, tmp___0_14^0'=tmp___0_14^0, x_18^0'=x_18^0, 0 == 0, cost: 1 New rule: l11 -> l1 : __cil_tmp6_15^0'=__cil_tmp6_15^0, __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, a_140^0'=a_140^0, a_16^0'=a_16^0, head_12^0'=0, i_11^0'=0, len_47^0'=len_47^0, length_10^0'=length_10^0, length_19^0'=length_19^post1, lt_21^0'=lt_21^0, result_4^0'=result_4^0, t_17^0'=t_17^0, tmp_13^0'=tmp_13^0, tmp_20^0'=tmp_20^0, tmp___0_14^0'=tmp___0_14^0, x_18^0'=x_18^0, T, cost: 1 Removed Trivial Updates Original rule: l11 -> l1 : __cil_tmp6_15^0'=__cil_tmp6_15^0, __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, a_140^0'=a_140^0, a_16^0'=a_16^0, head_12^0'=0, i_11^0'=0, len_47^0'=len_47^0, length_10^0'=length_10^0, length_19^0'=length_19^post1, lt_21^0'=lt_21^0, result_4^0'=result_4^0, t_17^0'=t_17^0, tmp_13^0'=tmp_13^0, tmp_20^0'=tmp_20^0, tmp___0_14^0'=tmp___0_14^0, x_18^0'=x_18^0, T, cost: 1 New rule: l11 -> l1 : head_12^0'=0, i_11^0'=0, length_19^0'=length_19^post1, T, cost: 1 Propagated Equalities Original rule: l2 -> l2 : __cil_tmp6_15^0'=__cil_tmp6_15^post5, __disjvr_0^0'=__disjvr_0^post5, __disjvr_1^0'=__disjvr_1^post5, a_140^0'=a_140^post5, a_16^0'=a_16^post5, head_12^0'=head_12^post5, i_11^0'=i_11^post5, len_47^0'=len_47^post5, length_10^0'=length_10^post5, length_19^0'=length_19^post5, lt_21^0'=lt_21^post5, result_4^0'=result_4^post5, t_17^0'=t_17^post5, tmp_13^0'=tmp_13^post5, tmp_20^0'=tmp_20^post5, tmp___0_14^0'=tmp___0_14^post5, x_18^0'=x_18^post5, (0 == 0 /\ -length_19^post4+length_19^0 == 0 /\ -lt_21^post5+lt_21^post4 == 0 /\ -result_4^post4+result_4^0 == 0 /\ __disjvr_0^post4-__disjvr_0^post5 == 0 /\ a_140^post4-a_140^post5 == 0 /\ -len_47^post5+len_47^post4 == 0 /\ -x_18^post4+x_18^0 == 0 /\ i_11^post4-i_11^post5 == 0 /\ __cil_tmp6_15^post4-__cil_tmp6_15^post5 == 0 /\ t_17^post4-t_17^post5 == 0 /\ -1+i_11^post4-i_11^0 == 0 /\ len_47^0-len_47^post4 == 0 /\ tmp___0_14^post4-tmp___0_14^post5 == 0 /\ -tmp_13^post5+tmp_13^post4 == 0 /\ -tmp___0_14^post4+tmp_13^post4 == 0 /\ length_10^0-length_10^post4 == 0 /\ -a_16^post5+a_16^post4 == 0 /\ length_19^post4-length_19^post5 == 0 /\ 2-length_10^0+i_11^0 <= 0 /\ a_140^0-a_140^post4 == 0 /\ head_12^post4-tmp_13^post4 == 0 /\ tmp_20^0-tmp_20^post4 == 0 /\ lt_21^0-lt_21^post4 == 0 /\ -__disjvr_1^post4+__disjvr_1^0 == 0 /\ -__disjvr_0^post4+__disjvr_0^0 == 0 /\ result_4^post4-result_4^post5 == 0 /\ head_12^post4-head_12^post5 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post4 == 0 /\ length_10^post4-length_10^post5 == 0 /\ t_17^0-t_17^post4 == 0 /\ -len_47^0 <= 0 /\ a_16^0-a_16^post4 == 0 /\ __disjvr_1^post4-__disjvr_1^post5 == 0 /\ -tmp_20^post5+tmp_20^post4 == 0 /\ x_18^post4-x_18^post5 == 0), cost: 1 New rule: l2 -> l2 : __cil_tmp6_15^0'=__cil_tmp6_15^post4, __disjvr_0^0'=__disjvr_0^post4, __disjvr_1^0'=__disjvr_1^post4, a_140^0'=a_140^post4, a_16^0'=a_16^post4, head_12^0'=head_12^post4, i_11^0'=i_11^post4, len_47^0'=len_47^post4, length_10^0'=length_10^post4, length_19^0'=length_19^post4, lt_21^0'=lt_21^post4, result_4^0'=result_4^post4, t_17^0'=t_17^post4, tmp_13^0'=tmp_13^post4, tmp_20^0'=tmp_20^post4, tmp___0_14^0'=tmp___0_14^post4, x_18^0'=x_18^post4, (0 == 0 /\ -length_19^post4+length_19^0 == 0 /\ -result_4^post4+result_4^0 == 0 /\ -x_18^post4+x_18^0 == 0 /\ -1+i_11^post4-i_11^0 == 0 /\ len_47^0-len_47^post4 == 0 /\ -tmp___0_14^post4+tmp_13^post4 == 0 /\ length_10^0-length_10^post4 == 0 /\ 2-length_10^0+i_11^0 <= 0 /\ a_140^0-a_140^post4 == 0 /\ head_12^post4-tmp_13^post4 == 0 /\ tmp_20^0-tmp_20^post4 == 0 /\ lt_21^0-lt_21^post4 == 0 /\ -__disjvr_1^post4+__disjvr_1^0 == 0 /\ -__disjvr_0^post4+__disjvr_0^0 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post4 == 0 /\ t_17^0-t_17^post4 == 0 /\ -len_47^0 <= 0 /\ a_16^0-a_16^post4 == 0), cost: 1 propagated equality lt_21^post5 = lt_21^post4 propagated equality __disjvr_0^post5 = __disjvr_0^post4 propagated equality a_140^post5 = a_140^post4 propagated equality len_47^post5 = len_47^post4 propagated equality i_11^post5 = i_11^post4 propagated equality __cil_tmp6_15^post5 = __cil_tmp6_15^post4 propagated equality t_17^post5 = t_17^post4 propagated equality tmp___0_14^post5 = tmp___0_14^post4 propagated equality tmp_13^post5 = tmp_13^post4 propagated equality a_16^post5 = a_16^post4 propagated equality length_19^post5 = length_19^post4 propagated equality result_4^post5 = result_4^post4 propagated equality head_12^post5 = head_12^post4 propagated equality length_10^post5 = length_10^post4 propagated equality __disjvr_1^post5 = __disjvr_1^post4 propagated equality tmp_20^post5 = tmp_20^post4 propagated equality x_18^post5 = x_18^post4 Propagated Equalities Original rule: l2 -> l2 : __cil_tmp6_15^0'=__cil_tmp6_15^post4, __disjvr_0^0'=__disjvr_0^post4, __disjvr_1^0'=__disjvr_1^post4, a_140^0'=a_140^post4, a_16^0'=a_16^post4, head_12^0'=head_12^post4, i_11^0'=i_11^post4, len_47^0'=len_47^post4, length_10^0'=length_10^post4, length_19^0'=length_19^post4, lt_21^0'=lt_21^post4, result_4^0'=result_4^post4, t_17^0'=t_17^post4, tmp_13^0'=tmp_13^post4, tmp_20^0'=tmp_20^post4, tmp___0_14^0'=tmp___0_14^post4, x_18^0'=x_18^post4, (0 == 0 /\ -length_19^post4+length_19^0 == 0 /\ -result_4^post4+result_4^0 == 0 /\ -x_18^post4+x_18^0 == 0 /\ -1+i_11^post4-i_11^0 == 0 /\ len_47^0-len_47^post4 == 0 /\ -tmp___0_14^post4+tmp_13^post4 == 0 /\ length_10^0-length_10^post4 == 0 /\ 2-length_10^0+i_11^0 <= 0 /\ a_140^0-a_140^post4 == 0 /\ head_12^post4-tmp_13^post4 == 0 /\ tmp_20^0-tmp_20^post4 == 0 /\ lt_21^0-lt_21^post4 == 0 /\ -__disjvr_1^post4+__disjvr_1^0 == 0 /\ -__disjvr_0^post4+__disjvr_0^0 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post4 == 0 /\ t_17^0-t_17^post4 == 0 /\ -len_47^0 <= 0 /\ a_16^0-a_16^post4 == 0), cost: 1 New rule: l2 -> l2 : __cil_tmp6_15^0'=__cil_tmp6_15^0, __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, a_140^0'=a_140^0, a_16^0'=a_16^0, head_12^0'=tmp___0_14^post4, i_11^0'=1+i_11^0, len_47^0'=len_47^0, length_10^0'=length_10^0, length_19^0'=length_19^0, lt_21^0'=lt_21^0, result_4^0'=result_4^0, t_17^0'=t_17^0, tmp_13^0'=tmp___0_14^post4, tmp_20^0'=tmp_20^0, tmp___0_14^0'=tmp___0_14^post4, x_18^0'=x_18^0, (0 == 0 /\ 2-length_10^0+i_11^0 <= 0 /\ -len_47^0 <= 0), cost: 1 propagated equality length_19^post4 = length_19^0 propagated equality result_4^post4 = result_4^0 propagated equality x_18^post4 = x_18^0 propagated equality i_11^post4 = 1+i_11^0 propagated equality len_47^post4 = len_47^0 propagated equality tmp_13^post4 = tmp___0_14^post4 propagated equality length_10^post4 = length_10^0 propagated equality a_140^post4 = a_140^0 propagated equality head_12^post4 = tmp___0_14^post4 propagated equality tmp_20^post4 = tmp_20^0 propagated equality lt_21^post4 = lt_21^0 propagated equality __disjvr_1^post4 = __disjvr_1^0 propagated equality __disjvr_0^post4 = __disjvr_0^0 propagated equality __cil_tmp6_15^post4 = __cil_tmp6_15^0 propagated equality t_17^post4 = t_17^0 propagated equality a_16^post4 = a_16^0 Simplified Guard Original rule: l2 -> l2 : __cil_tmp6_15^0'=__cil_tmp6_15^0, __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, a_140^0'=a_140^0, a_16^0'=a_16^0, head_12^0'=tmp___0_14^post4, i_11^0'=1+i_11^0, len_47^0'=len_47^0, length_10^0'=length_10^0, length_19^0'=length_19^0, lt_21^0'=lt_21^0, result_4^0'=result_4^0, t_17^0'=t_17^0, tmp_13^0'=tmp___0_14^post4, tmp_20^0'=tmp_20^0, tmp___0_14^0'=tmp___0_14^post4, x_18^0'=x_18^0, (0 == 0 /\ 2-length_10^0+i_11^0 <= 0 /\ -len_47^0 <= 0), cost: 1 New rule: l2 -> l2 : __cil_tmp6_15^0'=__cil_tmp6_15^0, __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, a_140^0'=a_140^0, a_16^0'=a_16^0, head_12^0'=tmp___0_14^post4, i_11^0'=1+i_11^0, len_47^0'=len_47^0, length_10^0'=length_10^0, length_19^0'=length_19^0, lt_21^0'=lt_21^0, result_4^0'=result_4^0, t_17^0'=t_17^0, tmp_13^0'=tmp___0_14^post4, tmp_20^0'=tmp_20^0, tmp___0_14^0'=tmp___0_14^post4, x_18^0'=x_18^0, (2-length_10^0+i_11^0 <= 0 /\ -len_47^0 <= 0), cost: 1 Removed Trivial Updates Original rule: l2 -> l2 : __cil_tmp6_15^0'=__cil_tmp6_15^0, __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, a_140^0'=a_140^0, a_16^0'=a_16^0, head_12^0'=tmp___0_14^post4, i_11^0'=1+i_11^0, len_47^0'=len_47^0, length_10^0'=length_10^0, length_19^0'=length_19^0, lt_21^0'=lt_21^0, result_4^0'=result_4^0, t_17^0'=t_17^0, tmp_13^0'=tmp___0_14^post4, tmp_20^0'=tmp_20^0, tmp___0_14^0'=tmp___0_14^post4, x_18^0'=x_18^0, (2-length_10^0+i_11^0 <= 0 /\ -len_47^0 <= 0), cost: 1 New rule: l2 -> l2 : head_12^0'=tmp___0_14^post4, i_11^0'=1+i_11^0, tmp_13^0'=tmp___0_14^post4, tmp___0_14^0'=tmp___0_14^post4, (2-length_10^0+i_11^0 <= 0 /\ -len_47^0 <= 0), cost: 1 Propagated Equalities Original rule: l2 -> l5 : __cil_tmp6_15^0'=__cil_tmp6_15^post8, __disjvr_0^0'=__disjvr_0^post8, __disjvr_1^0'=__disjvr_1^post8, a_140^0'=a_140^post8, a_16^0'=a_16^post8, head_12^0'=head_12^post8, i_11^0'=i_11^post8, len_47^0'=len_47^post8, length_10^0'=length_10^post8, length_19^0'=length_19^post8, lt_21^0'=lt_21^post8, result_4^0'=result_4^post8, t_17^0'=t_17^post8, tmp_13^0'=tmp_13^post8, tmp_20^0'=tmp_20^post8, tmp___0_14^0'=tmp___0_14^post8, x_18^0'=x_18^post8, (0 == 0 /\ -__disjvr_1^post6+__disjvr_1^0 == 0 /\ tmp_20^post7-tmp_20^post8 == 0 /\ -a_16^post7+a_16^post6 == 0 /\ -__cil_tmp6_15^post8+__cil_tmp6_15^post7 == 0 /\ __cil_tmp6_15^post6-head_12^0 == 0 /\ len_47^post7-len_47^post8 == 0 /\ a_140^post6-a_140^post7 == 0 /\ -result_4^1+tmp_20^post6 == 0 /\ t_17^post6-t_17^post7 == 0 /\ __cil_tmp6_15^post6-__cil_tmp6_15^post7 == 0 /\ -__cil_tmp6_15^post6+result_4^1 == 0 /\ -len_47^post7+len_47^post6 == 0 /\ -__disjvr_1^post8+__disjvr_1^post7 == 0 /\ -i_11^post8+i_11^post7 == 0 /\ i_11^post6-i_11^post7 == 0 /\ -tmp_13^post8+tmp_13^post7 == 0 /\ length_10^0-length_10^post6 == 0 /\ head_12^post7-head_12^post8 == 0 /\ length_19^post6-length_19^post7 == 0 /\ -lt_21^post7+lt_21^post6 == 0 /\ length_10^post7-length_10^post8 == 0 /\ __disjvr_0^post7-__disjvr_0^post6 == 0 /\ -tmp___0_14^post8+tmp___0_14^post7 == 0 /\ -1+length_10^0-i_11^0 <= 0 /\ -i_11^post6+i_11^0 == 0 /\ tmp___0_14^0-tmp___0_14^post6 == 0 /\ -result_4^post7+result_4^post6 == 0 /\ -lt_21^1+x_18^post8 == 0 /\ tmp___0_14^post6-tmp___0_14^post7 == 0 /\ length_10^post6-length_10^post7 == 0 /\ lt_21^0-lt_21^post6 == 0 /\ result_4^post7-result_4^post8 == 0 /\ len_47^0-len_47^post6 == 0 /\ x_18^post6-x_18^post7 == 0 /\ __disjvr_1^post6-__disjvr_1^post7 == 0 /\ -tmp_13^post6+tmp_13^0 == 0 /\ -__disjvr_0^post6+__disjvr_0^0 == 0 /\ -__disjvr_0^post7+__disjvr_0^post6 == 0 /\ t_17^post8-x_18^post7 == 0 /\ a_16^0-a_16^post6 == 0 /\ a_140^0-a_140^post6 == 0 /\ tmp_13^post6-tmp_13^post7 == 0 /\ -a_140^post8+a_140^post7 == 0 /\ -head_12^post6+head_12^0 == 0 /\ -len_47^0 <= 0 /\ -length_19^post8+length_19^post7 == 0 /\ -tmp_20^post7+tmp_20^post6 == 0 /\ a_16^post7-a_16^post8 == 0 /\ head_12^post6-head_12^post7 == 0 /\ x_18^post6-a_16^0 == 0 /\ -length_19^post6+length_19^0 == 0 /\ __disjvr_0^post7-__disjvr_0^post8 == 0 /\ t_17^0-t_17^post6 == 0), cost: 1 New rule: l2 -> l5 : __cil_tmp6_15^0'=__cil_tmp6_15^post7, __disjvr_0^0'=__disjvr_0^post7, __disjvr_1^0'=__disjvr_1^post7, a_140^0'=a_140^post7, a_16^0'=a_16^post7, head_12^0'=head_12^post7, i_11^0'=i_11^post7, len_47^0'=len_47^post7, length_10^0'=length_10^post7, length_19^0'=length_19^post7, lt_21^0'=lt_21^post8, result_4^0'=result_4^post7, t_17^0'=x_18^post7, tmp_13^0'=tmp_13^post7, tmp_20^0'=tmp_20^post7, tmp___0_14^0'=tmp___0_14^post7, x_18^0'=lt_21^1, (0 == 0 /\ -__disjvr_1^post6+__disjvr_1^0 == 0 /\ -a_16^post7+a_16^post6 == 0 /\ __cil_tmp6_15^post6-head_12^0 == 0 /\ a_140^post6-a_140^post7 == 0 /\ -result_4^1+tmp_20^post6 == 0 /\ t_17^post6-t_17^post7 == 0 /\ __cil_tmp6_15^post6-__cil_tmp6_15^post7 == 0 /\ -__cil_tmp6_15^post6+result_4^1 == 0 /\ -len_47^post7+len_47^post6 == 0 /\ i_11^post6-i_11^post7 == 0 /\ length_10^0-length_10^post6 == 0 /\ length_19^post6-length_19^post7 == 0 /\ -lt_21^post7+lt_21^post6 == 0 /\ __disjvr_0^post7-__disjvr_0^post6 == 0 /\ -1+length_10^0-i_11^0 <= 0 /\ -i_11^post6+i_11^0 == 0 /\ tmp___0_14^0-tmp___0_14^post6 == 0 /\ -result_4^post7+result_4^post6 == 0 /\ tmp___0_14^post6-tmp___0_14^post7 == 0 /\ length_10^post6-length_10^post7 == 0 /\ lt_21^0-lt_21^post6 == 0 /\ len_47^0-len_47^post6 == 0 /\ x_18^post6-x_18^post7 == 0 /\ __disjvr_1^post6-__disjvr_1^post7 == 0 /\ -tmp_13^post6+tmp_13^0 == 0 /\ -__disjvr_0^post6+__disjvr_0^0 == 0 /\ -__disjvr_0^post7+__disjvr_0^post6 == 0 /\ a_16^0-a_16^post6 == 0 /\ a_140^0-a_140^post6 == 0 /\ tmp_13^post6-tmp_13^post7 == 0 /\ -head_12^post6+head_12^0 == 0 /\ -len_47^0 <= 0 /\ -tmp_20^post7+tmp_20^post6 == 0 /\ head_12^post6-head_12^post7 == 0 /\ x_18^post6-a_16^0 == 0 /\ -length_19^post6+length_19^0 == 0 /\ t_17^0-t_17^post6 == 0), cost: 1 propagated equality tmp_20^post8 = tmp_20^post7 propagated equality __cil_tmp6_15^post8 = __cil_tmp6_15^post7 propagated equality len_47^post8 = len_47^post7 propagated equality __disjvr_1^post8 = __disjvr_1^post7 propagated equality i_11^post8 = i_11^post7 propagated equality tmp_13^post8 = tmp_13^post7 propagated equality head_12^post8 = head_12^post7 propagated equality length_10^post8 = length_10^post7 propagated equality tmp___0_14^post8 = tmp___0_14^post7 propagated equality x_18^post8 = lt_21^1 propagated equality result_4^post8 = result_4^post7 propagated equality t_17^post8 = x_18^post7 propagated equality a_140^post8 = a_140^post7 propagated equality length_19^post8 = length_19^post7 propagated equality a_16^post8 = a_16^post7 propagated equality __disjvr_0^post8 = __disjvr_0^post7 Propagated Equalities Original rule: l2 -> l5 : __cil_tmp6_15^0'=__cil_tmp6_15^post7, __disjvr_0^0'=__disjvr_0^post7, __disjvr_1^0'=__disjvr_1^post7, a_140^0'=a_140^post7, a_16^0'=a_16^post7, head_12^0'=head_12^post7, i_11^0'=i_11^post7, len_47^0'=len_47^post7, length_10^0'=length_10^post7, length_19^0'=length_19^post7, lt_21^0'=lt_21^post8, result_4^0'=result_4^post7, t_17^0'=x_18^post7, tmp_13^0'=tmp_13^post7, tmp_20^0'=tmp_20^post7, tmp___0_14^0'=tmp___0_14^post7, x_18^0'=lt_21^1, (0 == 0 /\ -__disjvr_1^post6+__disjvr_1^0 == 0 /\ -a_16^post7+a_16^post6 == 0 /\ __cil_tmp6_15^post6-head_12^0 == 0 /\ a_140^post6-a_140^post7 == 0 /\ -result_4^1+tmp_20^post6 == 0 /\ t_17^post6-t_17^post7 == 0 /\ __cil_tmp6_15^post6-__cil_tmp6_15^post7 == 0 /\ -__cil_tmp6_15^post6+result_4^1 == 0 /\ -len_47^post7+len_47^post6 == 0 /\ i_11^post6-i_11^post7 == 0 /\ length_10^0-length_10^post6 == 0 /\ length_19^post6-length_19^post7 == 0 /\ -lt_21^post7+lt_21^post6 == 0 /\ __disjvr_0^post7-__disjvr_0^post6 == 0 /\ -1+length_10^0-i_11^0 <= 0 /\ -i_11^post6+i_11^0 == 0 /\ tmp___0_14^0-tmp___0_14^post6 == 0 /\ -result_4^post7+result_4^post6 == 0 /\ tmp___0_14^post6-tmp___0_14^post7 == 0 /\ length_10^post6-length_10^post7 == 0 /\ lt_21^0-lt_21^post6 == 0 /\ len_47^0-len_47^post6 == 0 /\ x_18^post6-x_18^post7 == 0 /\ __disjvr_1^post6-__disjvr_1^post7 == 0 /\ -tmp_13^post6+tmp_13^0 == 0 /\ -__disjvr_0^post6+__disjvr_0^0 == 0 /\ -__disjvr_0^post7+__disjvr_0^post6 == 0 /\ a_16^0-a_16^post6 == 0 /\ a_140^0-a_140^post6 == 0 /\ tmp_13^post6-tmp_13^post7 == 0 /\ -head_12^post6+head_12^0 == 0 /\ -len_47^0 <= 0 /\ -tmp_20^post7+tmp_20^post6 == 0 /\ head_12^post6-head_12^post7 == 0 /\ x_18^post6-a_16^0 == 0 /\ -length_19^post6+length_19^0 == 0 /\ t_17^0-t_17^post6 == 0), cost: 1 New rule: l2 -> l5 : __cil_tmp6_15^0'=head_12^0, __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, a_140^0'=a_140^0, a_16^0'=a_16^0, head_12^0'=head_12^0, i_11^0'=i_11^0, len_47^0'=len_47^0, length_10^0'=length_10^0, length_19^0'=length_19^0, lt_21^0'=lt_21^post8, result_4^0'=result_4^post7, t_17^0'=a_16^0, tmp_13^0'=tmp_13^0, tmp_20^0'=head_12^0, tmp___0_14^0'=tmp___0_14^0, x_18^0'=lt_21^1, (0 == 0 /\ -1+length_10^0-i_11^0 <= 0 /\ -len_47^0 <= 0), cost: 1 propagated equality __disjvr_1^post6 = __disjvr_1^0 propagated equality a_16^post6 = a_16^post7 propagated equality __cil_tmp6_15^post6 = head_12^0 propagated equality a_140^post6 = a_140^post7 propagated equality result_4^1 = tmp_20^post6 propagated equality t_17^post6 = t_17^post7 propagated equality __cil_tmp6_15^post7 = head_12^0 propagated equality tmp_20^post6 = head_12^0 propagated equality len_47^post6 = len_47^post7 propagated equality i_11^post6 = i_11^post7 propagated equality length_10^post6 = length_10^0 propagated equality length_19^post6 = length_19^post7 propagated equality lt_21^post6 = lt_21^post7 propagated equality __disjvr_0^post6 = __disjvr_0^post7 propagated equality i_11^post7 = i_11^0 propagated equality tmp___0_14^post6 = tmp___0_14^0 propagated equality result_4^post6 = result_4^post7 propagated equality tmp___0_14^post7 = tmp___0_14^0 propagated equality length_10^post7 = length_10^0 propagated equality lt_21^post7 = lt_21^0 propagated equality len_47^post7 = len_47^0 propagated equality x_18^post6 = x_18^post7 propagated equality __disjvr_1^post7 = __disjvr_1^0 propagated equality tmp_13^post6 = tmp_13^0 propagated equality __disjvr_0^post7 = __disjvr_0^0 propagated equality a_16^post7 = a_16^0 propagated equality a_140^post7 = a_140^0 propagated equality tmp_13^post7 = tmp_13^0 propagated equality head_12^post6 = head_12^0 propagated equality tmp_20^post7 = head_12^0 propagated equality head_12^post7 = head_12^0 propagated equality x_18^post7 = a_16^0 propagated equality length_19^post7 = length_19^0 propagated equality t_17^post7 = t_17^0 Simplified Guard Original rule: l2 -> l5 : __cil_tmp6_15^0'=head_12^0, __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, a_140^0'=a_140^0, a_16^0'=a_16^0, head_12^0'=head_12^0, i_11^0'=i_11^0, len_47^0'=len_47^0, length_10^0'=length_10^0, length_19^0'=length_19^0, lt_21^0'=lt_21^post8, result_4^0'=result_4^post7, t_17^0'=a_16^0, tmp_13^0'=tmp_13^0, tmp_20^0'=head_12^0, tmp___0_14^0'=tmp___0_14^0, x_18^0'=lt_21^1, (0 == 0 /\ -1+length_10^0-i_11^0 <= 0 /\ -len_47^0 <= 0), cost: 1 New rule: l2 -> l5 : __cil_tmp6_15^0'=head_12^0, __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, a_140^0'=a_140^0, a_16^0'=a_16^0, head_12^0'=head_12^0, i_11^0'=i_11^0, len_47^0'=len_47^0, length_10^0'=length_10^0, length_19^0'=length_19^0, lt_21^0'=lt_21^post8, result_4^0'=result_4^post7, t_17^0'=a_16^0, tmp_13^0'=tmp_13^0, tmp_20^0'=head_12^0, tmp___0_14^0'=tmp___0_14^0, x_18^0'=lt_21^1, (-1+length_10^0-i_11^0 <= 0 /\ -len_47^0 <= 0), cost: 1 Removed Trivial Updates Original rule: l2 -> l5 : __cil_tmp6_15^0'=head_12^0, __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, a_140^0'=a_140^0, a_16^0'=a_16^0, head_12^0'=head_12^0, i_11^0'=i_11^0, len_47^0'=len_47^0, length_10^0'=length_10^0, length_19^0'=length_19^0, lt_21^0'=lt_21^post8, result_4^0'=result_4^post7, t_17^0'=a_16^0, tmp_13^0'=tmp_13^0, tmp_20^0'=head_12^0, tmp___0_14^0'=tmp___0_14^0, x_18^0'=lt_21^1, (-1+length_10^0-i_11^0 <= 0 /\ -len_47^0 <= 0), cost: 1 New rule: l2 -> l5 : __cil_tmp6_15^0'=head_12^0, lt_21^0'=lt_21^post8, result_4^0'=result_4^post7, t_17^0'=a_16^0, tmp_20^0'=head_12^0, x_18^0'=lt_21^1, (-1+length_10^0-i_11^0 <= 0 /\ -len_47^0 <= 0), cost: 1 Propagated Equalities Original rule: l5 -> l5 : __cil_tmp6_15^0'=__cil_tmp6_15^post13, __disjvr_0^0'=__disjvr_0^post13, __disjvr_1^0'=__disjvr_1^post13, a_140^0'=a_140^post13, a_16^0'=a_16^post13, head_12^0'=head_12^post13, i_11^0'=i_11^post13, len_47^0'=len_47^post13, length_10^0'=length_10^post13, length_19^0'=length_19^post13, lt_21^0'=lt_21^post13, result_4^0'=result_4^post13, t_17^0'=t_17^post13, tmp_13^0'=tmp_13^post13, tmp_20^0'=tmp_20^post13, tmp___0_14^0'=tmp___0_14^post13, x_18^0'=x_18^post13, (0 == 0 /\ -tmp_13^post10+tmp_13^0 == 0 /\ -i_11^post13+i_11^post12 == 0 /\ __cil_tmp6_15^post11-__cil_tmp6_15^post12 == 0 /\ -length_10^post11+length_10^post10 == 0 /\ __disjvr_1^post12-__disjvr_1^post13 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post10 == 0 /\ -__disjvr_0^post10+__disjvr_0^0 == 0 /\ length_19^post12-length_19^post13 == 0 /\ -a_140^post13+a_140^post12 == 0 /\ __disjvr_0^post11-__disjvr_0^post12 == 0 /\ -a_140^0 <= 0 /\ a_140^post10-a_140^post11 == 0 /\ -result_4^post13+result_4^post12 == 0 /\ -result_4^post11+result_4^post10 == 0 /\ -x_18^post13+x_18^post12 == 0 /\ i_11^post11-i_11^post12 == 0 /\ -tmp___0_14^post10+tmp___0_14^0 == 0 /\ __disjvr_1^0-__disjvr_1^post10 == 0 /\ lt_21^post10-lt_21^post11 == 0 /\ tmp___0_14^post10-tmp___0_14^post11 == 0 /\ -__cil_tmp6_15^post13+__cil_tmp6_15^post12 == 0 /\ __cil_tmp6_15^post10-__cil_tmp6_15^post11 == 0 /\ -x_18^post11+t_17^post12 == 0 /\ -__disjvr_0^post11+__disjvr_0^post10 == 0 /\ a_140^post11-a_140^post12 == 0 /\ length_10^post11-length_10^post12 == 0 /\ head_12^post12-head_12^post13 == 0 /\ result_4^0-result_4^post10 == 0 /\ length_10^post12-length_10^post13 == 0 /\ -__disjvr_1^post11+__disjvr_1^post10 == 0 /\ -len_47^post12+len_47^post11 == 0 /\ -lt_21^post13+lt_21^post12 == 0 /\ -t_17^post13+t_17^post12 == 0 /\ -a_16^post12+a_16^post11 == 0 /\ -t_17^post10+t_17^0 == 0 /\ -tmp___0_14^post13+tmp___0_14^post12 == 0 /\ head_12^0-head_12^post10 == 0 /\ tmp___0_14^post11-tmp___0_14^post12 == 0 /\ a_140^0-a_140^post10 == 0 /\ tmp_20^post10-tmp_20^post11 == 0 /\ head_12^post11-head_12^post12 == 0 /\ -lt_21^1+x_18^post12 == 0 /\ result_4^post11-result_4^post12 == 0 /\ tmp_13^post10-tmp_13^post11 == 0 /\ i_11^post10-i_11^post11 == 0 /\ __disjvr_1^post11-__disjvr_1^post12 == 0 /\ __disjvr_1^post11-__disjvr_1^post10 == 0 /\ a_16^post10-a_16^post11 == 0 /\ -tmp_13^post13+tmp_13^post12 == 0 /\ len_47^0-len_47^post10 == 0 /\ t_17^post10-t_17^post11 == 0 /\ -lt_21^post10+lt_21^0 == 0 /\ len_47^post12-len_47^post13 == 0 /\ -tmp_20^post12+tmp_20^post11 == 0 /\ length_19^post11-length_19^post12 == 0 /\ a_16^post12-a_16^post13 == 0 /\ len_47^post10-len_47^post11 == 0 /\ length_10^0-length_10^post10 == 0 /\ x_18^post10-x_18^post11 == 0 /\ tmp_20^0-tmp_20^post10 == 0 /\ length_19^post10-length_19^post11 == 0 /\ -head_12^post11+head_12^post10 == 0 /\ tmp_13^post11-tmp_13^post12 == 0 /\ -length_19^post10+length_19^0 == 0 /\ -tmp_20^post13+tmp_20^post12 == 0 /\ -a_16^post10+a_16^0 == 0 /\ __disjvr_0^post12-__disjvr_0^post13 == 0 /\ -x_18^post10+x_18^0 == 0 /\ -i_11^post10+i_11^0 == 0), cost: 1 New rule: l5 -> l5 : __cil_tmp6_15^0'=__cil_tmp6_15^post12, __disjvr_0^0'=__disjvr_0^post12, __disjvr_1^0'=__disjvr_1^post12, a_140^0'=a_140^post12, a_16^0'=a_16^post12, head_12^0'=head_12^post12, i_11^0'=i_11^post12, len_47^0'=len_47^post12, length_10^0'=length_10^post12, length_19^0'=length_19^post12, lt_21^0'=lt_21^post12, result_4^0'=result_4^post12, t_17^0'=t_17^post12, tmp_13^0'=tmp_13^post12, tmp_20^0'=tmp_20^post12, tmp___0_14^0'=tmp___0_14^post12, x_18^0'=x_18^post12, (0 == 0 /\ -tmp_13^post10+tmp_13^0 == 0 /\ __cil_tmp6_15^post11-__cil_tmp6_15^post12 == 0 /\ -length_10^post11+length_10^post10 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post10 == 0 /\ -__disjvr_0^post10+__disjvr_0^0 == 0 /\ __disjvr_0^post11-__disjvr_0^post12 == 0 /\ -a_140^0 <= 0 /\ a_140^post10-a_140^post11 == 0 /\ -result_4^post11+result_4^post10 == 0 /\ i_11^post11-i_11^post12 == 0 /\ -tmp___0_14^post10+tmp___0_14^0 == 0 /\ __disjvr_1^0-__disjvr_1^post10 == 0 /\ lt_21^post10-lt_21^post11 == 0 /\ tmp___0_14^post10-tmp___0_14^post11 == 0 /\ __cil_tmp6_15^post10-__cil_tmp6_15^post11 == 0 /\ -x_18^post11+t_17^post12 == 0 /\ -__disjvr_0^post11+__disjvr_0^post10 == 0 /\ a_140^post11-a_140^post12 == 0 /\ length_10^post11-length_10^post12 == 0 /\ result_4^0-result_4^post10 == 0 /\ -__disjvr_1^post11+__disjvr_1^post10 == 0 /\ -len_47^post12+len_47^post11 == 0 /\ -a_16^post12+a_16^post11 == 0 /\ -t_17^post10+t_17^0 == 0 /\ head_12^0-head_12^post10 == 0 /\ tmp___0_14^post11-tmp___0_14^post12 == 0 /\ a_140^0-a_140^post10 == 0 /\ tmp_20^post10-tmp_20^post11 == 0 /\ head_12^post11-head_12^post12 == 0 /\ -lt_21^1+x_18^post12 == 0 /\ result_4^post11-result_4^post12 == 0 /\ tmp_13^post10-tmp_13^post11 == 0 /\ i_11^post10-i_11^post11 == 0 /\ __disjvr_1^post11-__disjvr_1^post12 == 0 /\ __disjvr_1^post11-__disjvr_1^post10 == 0 /\ a_16^post10-a_16^post11 == 0 /\ len_47^0-len_47^post10 == 0 /\ t_17^post10-t_17^post11 == 0 /\ -lt_21^post10+lt_21^0 == 0 /\ -tmp_20^post12+tmp_20^post11 == 0 /\ length_19^post11-length_19^post12 == 0 /\ len_47^post10-len_47^post11 == 0 /\ length_10^0-length_10^post10 == 0 /\ x_18^post10-x_18^post11 == 0 /\ tmp_20^0-tmp_20^post10 == 0 /\ length_19^post10-length_19^post11 == 0 /\ -head_12^post11+head_12^post10 == 0 /\ tmp_13^post11-tmp_13^post12 == 0 /\ -length_19^post10+length_19^0 == 0 /\ -a_16^post10+a_16^0 == 0 /\ -x_18^post10+x_18^0 == 0 /\ -i_11^post10+i_11^0 == 0), cost: 1 propagated equality i_11^post13 = i_11^post12 propagated equality __disjvr_1^post13 = __disjvr_1^post12 propagated equality length_19^post13 = length_19^post12 propagated equality a_140^post13 = a_140^post12 propagated equality result_4^post13 = result_4^post12 propagated equality x_18^post13 = x_18^post12 propagated equality __cil_tmp6_15^post13 = __cil_tmp6_15^post12 propagated equality head_12^post13 = head_12^post12 propagated equality length_10^post13 = length_10^post12 propagated equality lt_21^post13 = lt_21^post12 propagated equality t_17^post13 = t_17^post12 propagated equality tmp___0_14^post13 = tmp___0_14^post12 propagated equality tmp_13^post13 = tmp_13^post12 propagated equality len_47^post13 = len_47^post12 propagated equality a_16^post13 = a_16^post12 propagated equality tmp_20^post13 = tmp_20^post12 propagated equality __disjvr_0^post13 = __disjvr_0^post12 Propagated Equalities Original rule: l5 -> l5 : __cil_tmp6_15^0'=__cil_tmp6_15^post12, __disjvr_0^0'=__disjvr_0^post12, __disjvr_1^0'=__disjvr_1^post12, a_140^0'=a_140^post12, a_16^0'=a_16^post12, head_12^0'=head_12^post12, i_11^0'=i_11^post12, len_47^0'=len_47^post12, length_10^0'=length_10^post12, length_19^0'=length_19^post12, lt_21^0'=lt_21^post12, result_4^0'=result_4^post12, t_17^0'=t_17^post12, tmp_13^0'=tmp_13^post12, tmp_20^0'=tmp_20^post12, tmp___0_14^0'=tmp___0_14^post12, x_18^0'=x_18^post12, (0 == 0 /\ -tmp_13^post10+tmp_13^0 == 0 /\ __cil_tmp6_15^post11-__cil_tmp6_15^post12 == 0 /\ -length_10^post11+length_10^post10 == 0 /\ __cil_tmp6_15^0-__cil_tmp6_15^post10 == 0 /\ -__disjvr_0^post10+__disjvr_0^0 == 0 /\ __disjvr_0^post11-__disjvr_0^post12 == 0 /\ -a_140^0 <= 0 /\ a_140^post10-a_140^post11 == 0 /\ -result_4^post11+result_4^post10 == 0 /\ i_11^post11-i_11^post12 == 0 /\ -tmp___0_14^post10+tmp___0_14^0 == 0 /\ __disjvr_1^0-__disjvr_1^post10 == 0 /\ lt_21^post10-lt_21^post11 == 0 /\ tmp___0_14^post10-tmp___0_14^post11 == 0 /\ __cil_tmp6_15^post10-__cil_tmp6_15^post11 == 0 /\ -x_18^post11+t_17^post12 == 0 /\ -__disjvr_0^post11+__disjvr_0^post10 == 0 /\ a_140^post11-a_140^post12 == 0 /\ length_10^post11-length_10^post12 == 0 /\ result_4^0-result_4^post10 == 0 /\ -__disjvr_1^post11+__disjvr_1^post10 == 0 /\ -len_47^post12+len_47^post11 == 0 /\ -a_16^post12+a_16^post11 == 0 /\ -t_17^post10+t_17^0 == 0 /\ head_12^0-head_12^post10 == 0 /\ tmp___0_14^post11-tmp___0_14^post12 == 0 /\ a_140^0-a_140^post10 == 0 /\ tmp_20^post10-tmp_20^post11 == 0 /\ head_12^post11-head_12^post12 == 0 /\ -lt_21^1+x_18^post12 == 0 /\ result_4^post11-result_4^post12 == 0 /\ tmp_13^post10-tmp_13^post11 == 0 /\ i_11^post10-i_11^post11 == 0 /\ __disjvr_1^post11-__disjvr_1^post12 == 0 /\ __disjvr_1^post11-__disjvr_1^post10 == 0 /\ a_16^post10-a_16^post11 == 0 /\ len_47^0-len_47^post10 == 0 /\ t_17^post10-t_17^post11 == 0 /\ -lt_21^post10+lt_21^0 == 0 /\ -tmp_20^post12+tmp_20^post11 == 0 /\ length_19^post11-length_19^post12 == 0 /\ len_47^post10-len_47^post11 == 0 /\ length_10^0-length_10^post10 == 0 /\ x_18^post10-x_18^post11 == 0 /\ tmp_20^0-tmp_20^post10 == 0 /\ length_19^post10-length_19^post11 == 0 /\ -head_12^post11+head_12^post10 == 0 /\ tmp_13^post11-tmp_13^post12 == 0 /\ -length_19^post10+length_19^0 == 0 /\ -a_16^post10+a_16^0 == 0 /\ -x_18^post10+x_18^0 == 0 /\ -i_11^post10+i_11^0 == 0), cost: 1 New rule: l5 -> l5 : __cil_tmp6_15^0'=__cil_tmp6_15^0, __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, a_140^0'=a_140^0, a_16^0'=a_16^0, head_12^0'=head_12^0, i_11^0'=i_11^0, len_47^0'=len_47^0, length_10^0'=length_10^0, length_19^0'=length_19^0, lt_21^0'=lt_21^post12, result_4^0'=result_4^0, t_17^0'=x_18^0, tmp_13^0'=tmp_13^0, tmp_20^0'=tmp_20^0, tmp___0_14^0'=tmp___0_14^0, x_18^0'=x_18^post12, (0 == 0 /\ -a_140^0 <= 0), cost: 1 propagated equality tmp_13^post10 = tmp_13^0 propagated equality __cil_tmp6_15^post11 = __cil_tmp6_15^post12 propagated equality length_10^post10 = length_10^post11 propagated equality __cil_tmp6_15^post10 = __cil_tmp6_15^0 propagated equality __disjvr_0^post10 = __disjvr_0^0 propagated equality __disjvr_0^post11 = __disjvr_0^post12 propagated equality a_140^post10 = a_140^post11 propagated equality result_4^post10 = result_4^post11 propagated equality i_11^post11 = i_11^post12 propagated equality tmp___0_14^post10 = tmp___0_14^0 propagated equality __disjvr_1^post10 = __disjvr_1^0 propagated equality lt_21^post10 = lt_21^post11 propagated equality tmp___0_14^post11 = tmp___0_14^0 propagated equality __cil_tmp6_15^post12 = __cil_tmp6_15^0 propagated equality t_17^post12 = x_18^post11 propagated equality __disjvr_0^post12 = __disjvr_0^0 propagated equality a_140^post11 = a_140^post12 propagated equality length_10^post11 = length_10^post12 propagated equality result_4^post11 = result_4^0 propagated equality __disjvr_1^post11 = __disjvr_1^0 propagated equality len_47^post11 = len_47^post12 propagated equality a_16^post11 = a_16^post12 propagated equality t_17^post10 = t_17^0 propagated equality head_12^post10 = head_12^0 propagated equality tmp___0_14^post12 = tmp___0_14^0 propagated equality a_140^post12 = a_140^0 propagated equality tmp_20^post10 = tmp_20^post11 propagated equality head_12^post11 = head_12^post12 propagated equality lt_21^1 = x_18^post12 propagated equality result_4^post12 = result_4^0 propagated equality tmp_13^post11 = tmp_13^0 propagated equality i_11^post10 = i_11^post12 propagated equality __disjvr_1^post12 = __disjvr_1^0 propagated equality a_16^post10 = a_16^post12 propagated equality len_47^post10 = len_47^0 propagated equality t_17^post11 = t_17^0 propagated equality lt_21^post11 = lt_21^0 propagated equality tmp_20^post11 = tmp_20^post12 propagated equality length_19^post11 = length_19^post12 propagated equality len_47^post12 = len_47^0 propagated equality length_10^post12 = length_10^0 propagated equality x_18^post10 = x_18^post11 propagated equality tmp_20^post12 = tmp_20^0 propagated equality length_19^post10 = length_19^post12 propagated equality head_12^post12 = head_12^0 propagated equality tmp_13^post12 = tmp_13^0 propagated equality length_19^post12 = length_19^0 propagated equality a_16^post12 = a_16^0 propagated equality x_18^post11 = x_18^0 propagated equality i_11^post12 = i_11^0 Simplified Guard Original rule: l5 -> l5 : __cil_tmp6_15^0'=__cil_tmp6_15^0, __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, a_140^0'=a_140^0, a_16^0'=a_16^0, head_12^0'=head_12^0, i_11^0'=i_11^0, len_47^0'=len_47^0, length_10^0'=length_10^0, length_19^0'=length_19^0, lt_21^0'=lt_21^post12, result_4^0'=result_4^0, t_17^0'=x_18^0, tmp_13^0'=tmp_13^0, tmp_20^0'=tmp_20^0, tmp___0_14^0'=tmp___0_14^0, x_18^0'=x_18^post12, (0 == 0 /\ -a_140^0 <= 0), cost: 1 New rule: l5 -> l5 : __cil_tmp6_15^0'=__cil_tmp6_15^0, __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, a_140^0'=a_140^0, a_16^0'=a_16^0, head_12^0'=head_12^0, i_11^0'=i_11^0, len_47^0'=len_47^0, length_10^0'=length_10^0, length_19^0'=length_19^0, lt_21^0'=lt_21^post12, result_4^0'=result_4^0, t_17^0'=x_18^0, tmp_13^0'=tmp_13^0, tmp_20^0'=tmp_20^0, tmp___0_14^0'=tmp___0_14^0, x_18^0'=x_18^post12, -a_140^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l5 -> l5 : __cil_tmp6_15^0'=__cil_tmp6_15^0, __disjvr_0^0'=__disjvr_0^0, __disjvr_1^0'=__disjvr_1^0, a_140^0'=a_140^0, a_16^0'=a_16^0, head_12^0'=head_12^0, i_11^0'=i_11^0, len_47^0'=len_47^0, length_10^0'=length_10^0, length_19^0'=length_19^0, lt_21^0'=lt_21^post12, result_4^0'=result_4^0, t_17^0'=x_18^0, tmp_13^0'=tmp_13^0, tmp_20^0'=tmp_20^0, tmp___0_14^0'=tmp___0_14^0, x_18^0'=x_18^post12, -a_140^0 <= 0, cost: 1 New rule: l5 -> l5 : lt_21^0'=lt_21^post12, t_17^0'=x_18^0, x_18^0'=x_18^post12, -a_140^0 <= 0, cost: 1 Unrolled Loops Start location: l11 Program variables: __cil_tmp6_15^0 a_140^0 a_16^0 head_12^0 i_11^0 len_47^0 length_10^0 length_19^0 lt_21^0 result_4^0 t_17^0 tmp_13^0 tmp_20^0 tmp___0_14^0 x_18^0 21: l1 -> l2 : head_12^0'=tmp___0_14^post2, i_11^0'=1+i_11^0, tmp_13^0'=tmp___0_14^post2, tmp___0_14^0'=tmp___0_14^post2, 2-length_10^0+i_11^0 <= 0, cost: 1 22: l1 -> l3 : __cil_tmp6_15^0'=head_12^0, result_4^0'=result_4^post3, tmp_20^0'=head_12^0, x_18^0'=a_16^0, (-1+length_10^0-i_11^0 <= 0 /\ -a_16^0 <= 0 /\ a_16^0 <= 0 /\ a_16^0 == 0), cost: 1 25: l2 -> l2 : head_12^0'=tmp___0_14^post4, i_11^0'=1+i_11^0, tmp_13^0'=tmp___0_14^post4, tmp___0_14^0'=tmp___0_14^post4, (2-length_10^0+i_11^0 <= 0 /\ -len_47^0 <= 0), cost: 1 26: l2 -> l5 : __cil_tmp6_15^0'=head_12^0, lt_21^0'=lt_21^post8, result_4^0'=result_4^post7, t_17^0'=a_16^0, tmp_20^0'=head_12^0, x_18^0'=lt_21^1, (-1+length_10^0-i_11^0 <= 0 /\ -len_47^0 <= 0), cost: 1 23: l5 -> l3 : result_4^0'=result_4^post9, (-a_140^0 <= 0 /\ -x_18^0 <= 0 /\ -x_18^0 == 0 /\ x_18^0 <= 0), cost: 1 27: l5 -> l5 : lt_21^0'=lt_21^post12, t_17^0'=x_18^0, x_18^0'=x_18^post12, -a_140^0 <= 0, cost: 1 28: l5 -> l5 : lt_21^0'=lt_21^post121, t_17^0'=x_18^post12, x_18^0'=x_18^post121, -a_140^0 <= 0, cost: 1 24: l11 -> l1 : head_12^0'=0, i_11^0'=0, length_19^0'=length_19^post1, T, cost: 1 Unrolling Original rule: l5 -> l5 : lt_21^0'=lt_21^post12, t_17^0'=x_18^0, x_18^0'=x_18^post12, -a_140^0 <= 0, cost: 1 New rule: l5 -> l5 : lt_21^0'=lt_21^post121, t_17^0'=x_18^post12, x_18^0'=x_18^post121, -a_140^0 <= 0, cost: 1 Step with 24 Trace 24[T] Blocked [{}, {}] Step with 21 Trace 24[T], 21[(2-length_10^0+i_11^0 <= 0)] Blocked [{}, {}, {}] Step with 26 Trace 24[T], 21[(2-length_10^0+i_11^0 <= 0)], 26[(-1+length_10^0-i_11^0 <= 0 /\ -len_47^0 <= 0)] Blocked [{}, {}, {}, {}] Step with 23 Trace 24[T], 21[(2-length_10^0+i_11^0 <= 0)], 26[(-1+length_10^0-i_11^0 <= 0 /\ -len_47^0 <= 0)], 23[(-a_140^0 <= 0 /\ -x_18^0 <= 0 /\ -x_18^0 == 0 /\ x_18^0 <= 0)] Blocked [{}, {}, {}, {}, {}] Backtrack Trace 24[T], 21[(2-length_10^0+i_11^0 <= 0)], 26[(-1+length_10^0-i_11^0 <= 0 /\ -len_47^0 <= 0)] Blocked [{}, {}, {}, {23[T]}] Step with 27 Trace 24[T], 21[(2-length_10^0+i_11^0 <= 0)], 26[(-1+length_10^0-i_11^0 <= 0 /\ -len_47^0 <= 0)], 27[(-a_140^0 <= 0)] Blocked [{}, {}, {}, {23[T]}, {}] Nonterm Start location: l11 Program variables: __cil_tmp6_15^0 a_140^0 a_16^0 head_12^0 i_11^0 len_47^0 length_10^0 length_19^0 lt_21^0 result_4^0 t_17^0 tmp_13^0 tmp_20^0 tmp___0_14^0 x_18^0 21: l1 -> l2 : head_12^0'=tmp___0_14^post2, i_11^0'=1+i_11^0, tmp_13^0'=tmp___0_14^post2, tmp___0_14^0'=tmp___0_14^post2, 2-length_10^0+i_11^0 <= 0, cost: 1 22: l1 -> l3 : __cil_tmp6_15^0'=head_12^0, result_4^0'=result_4^post3, tmp_20^0'=head_12^0, x_18^0'=a_16^0, (-1+length_10^0-i_11^0 <= 0 /\ -a_16^0 <= 0 /\ a_16^0 <= 0 /\ a_16^0 == 0), cost: 1 25: l2 -> l2 : head_12^0'=tmp___0_14^post4, i_11^0'=1+i_11^0, tmp_13^0'=tmp___0_14^post4, tmp___0_14^0'=tmp___0_14^post4, (2-length_10^0+i_11^0 <= 0 /\ -len_47^0 <= 0), cost: 1 26: l2 -> l5 : __cil_tmp6_15^0'=head_12^0, lt_21^0'=lt_21^post8, result_4^0'=result_4^post7, t_17^0'=a_16^0, tmp_20^0'=head_12^0, x_18^0'=lt_21^1, (-1+length_10^0-i_11^0 <= 0 /\ -len_47^0 <= 0), cost: 1 23: l5 -> l3 : result_4^0'=result_4^post9, (-a_140^0 <= 0 /\ -x_18^0 <= 0 /\ -x_18^0 == 0 /\ x_18^0 <= 0), cost: 1 27: l5 -> l5 : lt_21^0'=lt_21^post12, t_17^0'=x_18^0, x_18^0'=x_18^post12, -a_140^0 <= 0, cost: 1 28: l5 -> l5 : lt_21^0'=lt_21^post121, t_17^0'=x_18^post12, x_18^0'=x_18^post121, -a_140^0 <= 0, cost: 1 29: l5 -> LoAT_sink : (a_140^0 >= 0 /\ -1+n >= 0), cost: NONTERM 30: l5 -> l5 : lt_21^0'=lt_21^post123, t_17^0'=x_18^post12, x_18^0'=x_18^post123, (a_140^0 >= 0), cost: 1 24: l11 -> l1 : head_12^0'=0, i_11^0'=0, length_19^0'=length_19^post1, T, cost: 1 unrolling Original rule: l5 -> l5 : lt_21^0'=lt_21^post12, t_17^0'=x_18^0, x_18^0'=x_18^post12, (-a_140^0 <= 0), cost: 1 New rule: l5 -> l5 : lt_21^0'=lt_21^post123, t_17^0'=x_18^post12, x_18^0'=x_18^post123, -a_140^0 <= 0, cost: 1 Certificate of Non-Termination Original rule: l5 -> l5 : lt_21^0'=lt_21^post123, t_17^0'=x_18^post12, x_18^0'=x_18^post123, -a_140^0 <= 0, cost: 1 New rule: l5 -> LoAT_sink : (a_140^0 >= 0 /\ -1+n >= 0), cost: NONTERM a_140^0 >= 0 [0]: monotonic increase yields a_140^0 >= 0 Replacement map: {a_140^0 >= 0 -> a_140^0 >= 0} Loop Acceleration Original rule: l5 -> l5 : lt_21^0'=lt_21^post123, t_17^0'=x_18^post12, x_18^0'=x_18^post123, -a_140^0 <= 0, cost: 1 New rule: l5 -> l5 : lt_21^0'=lt_21^post123, t_17^0'=x_18^post12, x_18^0'=x_18^post123, (a_140^0 >= 0 /\ -1+n >= 0), cost: 1 a_140^0 >= 0 [0]: monotonic increase yields a_140^0 >= 0 Replacement map: {a_140^0 >= 0 -> a_140^0 >= 0} Eliminated Temporary Variables via Transitive Closure Original rule: l5 -> l5 : lt_21^0'=lt_21^post123, t_17^0'=x_18^post12, x_18^0'=x_18^post123, (a_140^0 >= 0 /\ -1+n >= 0), cost: 1 New rule: l5 -> l5 : lt_21^0'=lt_21^post123, t_17^0'=x_18^post12, x_18^0'=x_18^post123, (a_140^0 >= 0), cost: 1 Step with 29 Trace 24[T], 21[(2-length_10^0+i_11^0 <= 0)], 26[(-1+length_10^0-i_11^0 <= 0 /\ -len_47^0 <= 0)], 29[(a_140^0 >= 0 /\ -1+n >= 0)] Blocked [{}, {}, {}, {23[T]}, {29[T]}] Refute Counterexample [ __cil_tmp6_15^0=0 a_140^0=0 a_16^0=0 head_12^0=0 i_11^0=0 len_47^0=0 length_10^0=2 length_19^0=0 lt_21^0=0 result_4^0=0 t_17^0=0 tmp_13^0=0 tmp_20^0=0 tmp___0_14^0=0 x_18^0=0 ] 24 [ __cil_tmp6_15^0=0 a_140^0=0 a_16^0=0 head_12^0=0 i_11^0=1 len_47^0=0 length_10^0=2 length_19^0=0 lt_21^0=0 result_4^0=0 t_17^0=0 tmp_13^0=0 tmp_20^0=0 tmp___0_14^0=0 x_18^0=0 ] 21 [ __cil_tmp6_15^0=0 a_140^0=0 a_16^0=0 head_12^0=0 i_11^0=1 len_47^0=0 length_10^0=2 length_19^0=0 lt_21^0=0 result_4^0=0 t_17^0=0 tmp_13^0=0 tmp_20^0=0 tmp___0_14^0=0 x_18^0=0 ] 26 [ __cil_tmp6_15^0=0 a_140^0=0 a_16^0=0 head_12^0=head_12^0 i_11^0=i_11^0 len_47^0=0 length_10^0=2 length_19^0=length_19^0 lt_21^0=0 result_4^0=0 t_17^0=0 tmp_13^0=0 tmp_20^0=0 tmp___0_14^0=0 x_18^0=0 ] 29 NO Build SHA: a05f16bf13df659c382799650051f91bf6828c7b