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