NO

Initial ITS

Start location: l7
Program variables: __cil_tmp5_9^0 a_10^0 a_178^0 k_121^0 k_83^0 len_181^0 len_54^0 lt_15^0 result_4^0 tmp_8^0 x_12^0 x_13^0 x_7^0 y_11^0 y_14^0
   0: l0 -> l1 : __cil_tmp5_9^0'=__cil_tmp5_9^post1, a_10^0'=a_10^post1, a_178^0'=a_178^post1, k_121^0'=k_121^post1, k_83^0'=k_83^post1, len_181^0'=len_181^post1, len_54^0'=len_54^post1, lt_15^0'=lt_15^post1, result_4^0'=result_4^post1, tmp_8^0'=tmp_8^post1, x_12^0'=x_12^post1, x_13^0'=x_13^post1, x_7^0'=x_7^post1, y_11^0'=y_11^post1, y_14^0'=y_14^post1, (-y_11^post1+y_11^0 == 0 /\ -result_4^post1+result_4^0 == 0 /\ a_178^0-a_178^post1 == 0 /\ k_83^0-k_83^post1 == 0 /\ -__cil_tmp5_9^post1+__cil_tmp5_9^0 == 0 /\ -len_54^post1+len_54^0 == 0 /\ x_7^0-x_7^post1 == 0 /\ a_10^0-a_10^post1 == 0 /\ -k_121^0 <= 0 /\ 1-x_12^post1+y_11^0 <= 0 /\ x_13^0-x_13^post1 == 0 /\ y_14^0-y_14^post1 == 0 /\ len_181^0-len_181^post1 == 0 /\ -a_10^0+x_12^post1 == 0 /\ -k_121^post1+k_121^0 == 0 /\ lt_15^0-lt_15^post1 == 0 /\ -tmp_8^post1+tmp_8^0 == 0), cost: 1
   1: l0 -> l1 : __cil_tmp5_9^0'=__cil_tmp5_9^post2, a_10^0'=a_10^post2, a_178^0'=a_178^post2, k_121^0'=k_121^post2, k_83^0'=k_83^post2, len_181^0'=len_181^post2, len_54^0'=len_54^post2, lt_15^0'=lt_15^post2, result_4^0'=result_4^post2, tmp_8^0'=tmp_8^post2, x_12^0'=x_12^post2, x_13^0'=x_13^post2, x_7^0'=x_7^post2, y_11^0'=y_11^post2, y_14^0'=y_14^post2, (-k_83^post2+k_83^0 == 0 /\ k_121^0-k_121^post2 == 0 /\ -result_4^post2+result_4^0 == 0 /\ 1+x_12^post2-y_11^0 <= 0 /\ -y_11^post2+y_11^0 == 0 /\ len_181^0-len_181^post2 == 0 /\ -lt_15^post2+lt_15^0 == 0 /\ len_54^0-len_54^post2 == 0 /\ y_14^0-y_14^post2 == 0 /\ -k_121^0 <= 0 /\ __cil_tmp5_9^0-__cil_tmp5_9^post2 == 0 /\ a_178^0-a_178^post2 == 0 /\ -x_13^post2+x_13^0 == 0 /\ x_12^post2-a_10^0 == 0 /\ x_7^0-x_7^post2 == 0 /\ a_10^0-a_10^post2 == 0 /\ -tmp_8^post2+tmp_8^0 == 0), cost: 1
   3: l1 -> l3 : __cil_tmp5_9^0'=__cil_tmp5_9^post4, a_10^0'=a_10^post4, a_178^0'=a_178^post4, k_121^0'=k_121^post4, k_83^0'=k_83^post4, len_181^0'=len_181^post4, len_54^0'=len_54^post4, lt_15^0'=lt_15^post4, result_4^0'=result_4^post4, tmp_8^0'=tmp_8^post4, x_12^0'=x_12^post4, x_13^0'=x_13^post4, x_7^0'=x_7^post4, y_11^0'=y_11^post4, y_14^0'=y_14^post4, (0 == 0 /\ -1+len_181^post4 == 0 /\ x_12^post4-lt_15^1 == 0 /\ 1+y_11^0-x_12^0 <= 0 /\ -k_121^0 <= 0 /\ -k_121^post4+k_121^0 == 0 /\ len_54^0-len_54^post4 == 0 /\ -__cil_tmp5_9^post4+__cil_tmp5_9^0 == 0 /\ x_7^0-x_7^post4 == 0 /\ a_10^0-a_10^post4 == 0 /\ -k_83^post4+k_83^0 == 0 /\ -tmp_8^post4+tmp_8^0 == 0 /\ -result_4^post4+result_4^0 == 0 /\ a_178^0-a_178^post4 == 0 /\ y_14^0-y_14^post4 == 0 /\ -y_11^post4+y_11^0 == 0 /\ -x_13^post4+x_13^0 == 0), cost: 1
   4: l1 -> l3 : __cil_tmp5_9^0'=__cil_tmp5_9^post5, a_10^0'=a_10^post5, a_178^0'=a_178^post5, k_121^0'=k_121^post5, k_83^0'=k_83^post5, len_181^0'=len_181^post5, len_54^0'=len_54^post5, lt_15^0'=lt_15^post5, result_4^0'=result_4^post5, tmp_8^0'=tmp_8^post5, x_12^0'=x_12^post5, x_13^0'=x_13^post5, x_7^0'=x_7^post5, y_11^0'=y_11^post5, y_14^0'=y_14^post5, (0 == 0 /\ 1-y_11^0+x_12^0 <= 0 /\ y_14^0-y_14^post5 == 0 /\ -a_10^post5+a_10^0 == 0 /\ a_178^0-a_178^post5 == 0 /\ k_121^0-k_121^post5 == 0 /\ -k_121^0 <= 0 /\ -len_54^post5+len_54^0 == 0 /\ -k_83^post5+k_83^0 == 0 /\ -tmp_8^post5+tmp_8^0 == 0 /\ x_7^0-x_7^post5 == 0 /\ -result_4^post5+result_4^0 == 0 /\ -1+len_181^post5 == 0 /\ __cil_tmp5_9^0-__cil_tmp5_9^post5 == 0 /\ -y_11^post5+y_11^0 == 0 /\ -lt_15^1+x_12^post5 == 0 /\ -x_13^post5+x_13^0 == 0), cost: 1
   2: l2 -> l0 : __cil_tmp5_9^0'=__cil_tmp5_9^post3, a_10^0'=a_10^post3, a_178^0'=a_178^post3, k_121^0'=k_121^post3, k_83^0'=k_83^post3, len_181^0'=len_181^post3, len_54^0'=len_54^post3, lt_15^0'=lt_15^post3, result_4^0'=result_4^post3, tmp_8^0'=tmp_8^post3, x_12^0'=x_12^post3, x_13^0'=x_13^post3, x_7^0'=x_7^post3, y_11^0'=y_11^post3, y_14^0'=y_14^post3, (0 == 0 /\ -x_12^post3+x_12^0 == 0 /\ -tmp_8^1+x_7^1 == 0 /\ x_13^post3-result_4^7 == 0 /\ result_4^3-__cil_tmp5_9^2 == 0 /\ -len_54^post3 <= 0 /\ -x_7^3+__cil_tmp5_9^3 == 0 /\ -tmp_8^2+x_7^2 == 0 /\ result_4^5-__cil_tmp5_9^3 == 0 /\ -k_121^0 <= 0 /\ a_178^0-a_178^post3 == 0 /\ a_10^0-a_10^post3 == 0 /\ y_14^post3 == 0 /\ -1-len_54^post3+k_83^post3 == 0 /\ result_4^1-__cil_tmp5_9^1 == 0 /\ len_181^0-len_181^post3 == 0 /\ -x_7^2+__cil_tmp5_9^2 == 0 /\ -result_4^5+x_13^4 == 0 /\ -result_4^3+x_13^3 == 0 /\ x_7^3-tmp_8^3 == 0 /\ -x_7^1+__cil_tmp5_9^1 == 0 /\ -tmp_8^post3+x_7^post3 == 0 /\ -y_11^post3+y_11^0 == 0 /\ -2+len_54^post3 == 0 /\ -__cil_tmp5_9^post3+result_4^7 == 0 /\ -k_121^post3+k_121^0 == 0 /\ __cil_tmp5_9^post3-x_7^post3 == 0 /\ lt_15^0-lt_15^post3 == 0 /\ -result_4^1+x_13^2 == 0 /\ -k_83^post3 <= 0 /\ x_13^1 == 0), cost: 1
   5: l3 -> l4 : __cil_tmp5_9^0'=__cil_tmp5_9^post6, a_10^0'=a_10^post6, a_178^0'=a_178^post6, k_121^0'=k_121^post6, k_83^0'=k_83^post6, len_181^0'=len_181^post6, len_54^0'=len_54^post6, lt_15^0'=lt_15^post6, result_4^0'=result_4^post6, tmp_8^0'=tmp_8^post6, x_12^0'=x_12^post6, x_13^0'=x_13^post6, x_7^0'=x_7^post6, y_11^0'=y_11^post6, y_14^0'=y_14^post6, (0 == 0 /\ -y_11^0+x_12^0 <= 0 /\ x_12^0-x_12^post6 == 0 /\ -len_181^0 <= 0 /\ y_11^0-x_12^0 <= 0 /\ -a_178^post6+a_178^0 == 0 /\ -tmp_8^post6+tmp_8^0 == 0 /\ y_14^0-y_14^post6 == 0 /\ x_7^0-x_7^post6 == 0 /\ y_11^0-y_11^post6 == 0 /\ k_121^0-k_121^post6 == 0 /\ len_181^0-len_181^post6 == 0 /\ -k_83^post6+k_83^0 == 0 /\ -a_10^post6+a_10^0 == 0 /\ -x_13^post6+x_13^0 == 0 /\ __cil_tmp5_9^0-__cil_tmp5_9^post6 == 0 /\ -a_178^0 <= 0 /\ -len_54^post6+len_54^0 == 0 /\ lt_15^0-lt_15^post6 == 0), cost: 1
   6: l3 -> l5 : __cil_tmp5_9^0'=__cil_tmp5_9^post7, a_10^0'=a_10^post7, a_178^0'=a_178^post7, k_121^0'=k_121^post7, k_83^0'=k_83^post7, len_181^0'=len_181^post7, len_54^0'=len_54^post7, lt_15^0'=lt_15^post7, result_4^0'=result_4^post7, tmp_8^0'=tmp_8^post7, x_12^0'=x_12^post7, x_13^0'=x_13^post7, x_7^0'=x_7^post7, y_11^0'=y_11^post7, y_14^0'=y_14^post7, (0 == 0 /\ y_14^0-y_14^post7 == 0 /\ x_7^0-x_7^post7 == 0 /\ -len_181^0 <= 0 /\ 1+y_11^0-x_12^0 <= 0 /\ -y_11^post7+y_11^0 == 0 /\ __cil_tmp5_9^0-__cil_tmp5_9^post7 == 0 /\ x_12^post7-lt_15^1 == 0 /\ -a_178^post7+a_178^0 == 0 /\ k_83^0-k_83^post7 == 0 /\ -tmp_8^post7+tmp_8^0 == 0 /\ -k_121^post7+k_121^0 == 0 /\ x_13^0-x_13^post7 == 0 /\ -1+len_181^post7-len_181^0 == 0 /\ -result_4^post7+result_4^0 == 0 /\ -a_178^0 <= 0 /\ -len_54^post7+len_54^0 == 0 /\ a_10^0-a_10^post7 == 0), cost: 1
   8: l3 -> l6 : __cil_tmp5_9^0'=__cil_tmp5_9^post9, a_10^0'=a_10^post9, a_178^0'=a_178^post9, k_121^0'=k_121^post9, k_83^0'=k_83^post9, len_181^0'=len_181^post9, len_54^0'=len_54^post9, lt_15^0'=lt_15^post9, result_4^0'=result_4^post9, tmp_8^0'=tmp_8^post9, x_12^0'=x_12^post9, x_13^0'=x_13^post9, x_7^0'=x_7^post9, y_11^0'=y_11^post9, y_14^0'=y_14^post9, (0 == 0 /\ -a_178^post9+a_178^0 == 0 /\ 1-y_11^0+x_12^0 <= 0 /\ __cil_tmp5_9^0-__cil_tmp5_9^post9 == 0 /\ -1-len_181^0+len_181^post9 == 0 /\ -a_10^post9+a_10^0 == 0 /\ -len_181^0 <= 0 /\ k_121^0-k_121^post9 == 0 /\ -tmp_8^post9+tmp_8^0 == 0 /\ y_14^0-y_14^post9 == 0 /\ y_11^0-y_11^post9 == 0 /\ x_7^0-x_7^post9 == 0 /\ -result_4^post9+result_4^0 == 0 /\ -lt_15^1+x_12^post9 == 0 /\ -k_83^post9+k_83^0 == 0 /\ -len_54^post9+len_54^0 == 0 /\ -x_13^post9+x_13^0 == 0 /\ -a_178^0 <= 0), cost: 1
   7: l5 -> l3 : __cil_tmp5_9^0'=__cil_tmp5_9^post8, a_10^0'=a_10^post8, a_178^0'=a_178^post8, k_121^0'=k_121^post8, k_83^0'=k_83^post8, len_181^0'=len_181^post8, len_54^0'=len_54^post8, lt_15^0'=lt_15^post8, result_4^0'=result_4^post8, tmp_8^0'=tmp_8^post8, x_12^0'=x_12^post8, x_13^0'=x_13^post8, x_7^0'=x_7^post8, y_11^0'=y_11^post8, y_14^0'=y_14^post8, (y_14^0-y_14^post8 == 0 /\ len_181^0-len_181^post8 == 0 /\ x_7^0-x_7^post8 == 0 /\ len_54^0-len_54^post8 == 0 /\ -lt_15^post8+lt_15^0 == 0 /\ -y_11^post8+y_11^0 == 0 /\ -k_121^post8+k_121^0 == 0 /\ -__cil_tmp5_9^post8+__cil_tmp5_9^0 == 0 /\ a_10^0-a_10^post8 == 0 /\ -k_83^post8+k_83^0 == 0 /\ -tmp_8^post8+tmp_8^0 == 0 /\ -result_4^post8+result_4^0 == 0 /\ a_178^0-a_178^post8 == 0 /\ -x_12^post8+x_12^0 == 0 /\ -x_13^post8+x_13^0 == 0), cost: 1
   9: l6 -> l3 : __cil_tmp5_9^0'=__cil_tmp5_9^post10, a_10^0'=a_10^post10, a_178^0'=a_178^post10, k_121^0'=k_121^post10, k_83^0'=k_83^post10, len_181^0'=len_181^post10, len_54^0'=len_54^post10, lt_15^0'=lt_15^post10, result_4^0'=result_4^post10, tmp_8^0'=tmp_8^post10, x_12^0'=x_12^post10, x_13^0'=x_13^post10, x_7^0'=x_7^post10, y_11^0'=y_11^post10, y_14^0'=y_14^post10, (-y_14^post10+y_14^0 == 0 /\ x_12^0-x_12^post10 == 0 /\ -a_178^post10+a_178^0 == 0 /\ -tmp_8^post10+tmp_8^0 == 0 /\ y_11^0-y_11^post10 == 0 /\ len_181^0-len_181^post10 == 0 /\ x_7^0-x_7^post10 == 0 /\ k_121^0-k_121^post10 == 0 /\ a_10^0-a_10^post10 == 0 /\ -x_13^post10+x_13^0 == 0 /\ -len_54^post10+len_54^0 == 0 /\ -result_4^post10+result_4^0 == 0 /\ lt_15^0-lt_15^post10 == 0 /\ -k_83^post10+k_83^0 == 0 /\ -__cil_tmp5_9^post10+__cil_tmp5_9^0 == 0), cost: 1
  10: l7 -> l2 : __cil_tmp5_9^0'=__cil_tmp5_9^post11, a_10^0'=a_10^post11, a_178^0'=a_178^post11, k_121^0'=k_121^post11, k_83^0'=k_83^post11, len_181^0'=len_181^post11, len_54^0'=len_54^post11, lt_15^0'=lt_15^post11, result_4^0'=result_4^post11, tmp_8^0'=tmp_8^post11, x_12^0'=x_12^post11, x_13^0'=x_13^post11, x_7^0'=x_7^post11, y_11^0'=y_11^post11, y_14^0'=y_14^post11, (-y_11^post11+y_11^0 == 0 /\ x_7^0-x_7^post11 == 0 /\ a_10^0-a_10^post11 == 0 /\ -len_181^post11+len_181^0 == 0 /\ y_14^0-y_14^post11 == 0 /\ k_83^0-k_83^post11 == 0 /\ lt_15^0-lt_15^post11 == 0 /\ -tmp_8^post11+tmp_8^0 == 0 /\ -k_121^post11+k_121^0 == 0 /\ -__cil_tmp5_9^post11+__cil_tmp5_9^0 == 0 /\ -len_54^post11+len_54^0 == 0 /\ x_13^0-x_13^post11 == 0 /\ -x_12^post11+x_12^0 == 0 /\ -a_178^post11+a_178^0 == 0 /\ -result_4^post11+result_4^0 == 0), cost: 1

Chained Linear Paths

Start location: l7
Program variables: __cil_tmp5_9^0 a_10^0 a_178^0 k_121^0 k_83^0 len_181^0 len_54^0 lt_15^0 result_4^0 tmp_8^0 x_12^0 x_13^0 x_7^0 y_11^0 y_14^0
   0: l0 -> l1 : __cil_tmp5_9^0'=__cil_tmp5_9^post1, a_10^0'=a_10^post1, a_178^0'=a_178^post1, k_121^0'=k_121^post1, k_83^0'=k_83^post1, len_181^0'=len_181^post1, len_54^0'=len_54^post1, lt_15^0'=lt_15^post1, result_4^0'=result_4^post1, tmp_8^0'=tmp_8^post1, x_12^0'=x_12^post1, x_13^0'=x_13^post1, x_7^0'=x_7^post1, y_11^0'=y_11^post1, y_14^0'=y_14^post1, (-y_11^post1+y_11^0 == 0 /\ -result_4^post1+result_4^0 == 0 /\ a_178^0-a_178^post1 == 0 /\ k_83^0-k_83^post1 == 0 /\ -__cil_tmp5_9^post1+__cil_tmp5_9^0 == 0 /\ -len_54^post1+len_54^0 == 0 /\ x_7^0-x_7^post1 == 0 /\ a_10^0-a_10^post1 == 0 /\ -k_121^0 <= 0 /\ 1-x_12^post1+y_11^0 <= 0 /\ x_13^0-x_13^post1 == 0 /\ y_14^0-y_14^post1 == 0 /\ len_181^0-len_181^post1 == 0 /\ -a_10^0+x_12^post1 == 0 /\ -k_121^post1+k_121^0 == 0 /\ lt_15^0-lt_15^post1 == 0 /\ -tmp_8^post1+tmp_8^0 == 0), cost: 1
   1: l0 -> l1 : __cil_tmp5_9^0'=__cil_tmp5_9^post2, a_10^0'=a_10^post2, a_178^0'=a_178^post2, k_121^0'=k_121^post2, k_83^0'=k_83^post2, len_181^0'=len_181^post2, len_54^0'=len_54^post2, lt_15^0'=lt_15^post2, result_4^0'=result_4^post2, tmp_8^0'=tmp_8^post2, x_12^0'=x_12^post2, x_13^0'=x_13^post2, x_7^0'=x_7^post2, y_11^0'=y_11^post2, y_14^0'=y_14^post2, (-k_83^post2+k_83^0 == 0 /\ k_121^0-k_121^post2 == 0 /\ -result_4^post2+result_4^0 == 0 /\ 1+x_12^post2-y_11^0 <= 0 /\ -y_11^post2+y_11^0 == 0 /\ len_181^0-len_181^post2 == 0 /\ -lt_15^post2+lt_15^0 == 0 /\ len_54^0-len_54^post2 == 0 /\ y_14^0-y_14^post2 == 0 /\ -k_121^0 <= 0 /\ __cil_tmp5_9^0-__cil_tmp5_9^post2 == 0 /\ a_178^0-a_178^post2 == 0 /\ -x_13^post2+x_13^0 == 0 /\ x_12^post2-a_10^0 == 0 /\ x_7^0-x_7^post2 == 0 /\ a_10^0-a_10^post2 == 0 /\ -tmp_8^post2+tmp_8^0 == 0), cost: 1
   3: l1 -> l3 : __cil_tmp5_9^0'=__cil_tmp5_9^post4, a_10^0'=a_10^post4, a_178^0'=a_178^post4, k_121^0'=k_121^post4, k_83^0'=k_83^post4, len_181^0'=len_181^post4, len_54^0'=len_54^post4, lt_15^0'=lt_15^post4, result_4^0'=result_4^post4, tmp_8^0'=tmp_8^post4, x_12^0'=x_12^post4, x_13^0'=x_13^post4, x_7^0'=x_7^post4, y_11^0'=y_11^post4, y_14^0'=y_14^post4, (0 == 0 /\ -1+len_181^post4 == 0 /\ x_12^post4-lt_15^1 == 0 /\ 1+y_11^0-x_12^0 <= 0 /\ -k_121^0 <= 0 /\ -k_121^post4+k_121^0 == 0 /\ len_54^0-len_54^post4 == 0 /\ -__cil_tmp5_9^post4+__cil_tmp5_9^0 == 0 /\ x_7^0-x_7^post4 == 0 /\ a_10^0-a_10^post4 == 0 /\ -k_83^post4+k_83^0 == 0 /\ -tmp_8^post4+tmp_8^0 == 0 /\ -result_4^post4+result_4^0 == 0 /\ a_178^0-a_178^post4 == 0 /\ y_14^0-y_14^post4 == 0 /\ -y_11^post4+y_11^0 == 0 /\ -x_13^post4+x_13^0 == 0), cost: 1
   4: l1 -> l3 : __cil_tmp5_9^0'=__cil_tmp5_9^post5, a_10^0'=a_10^post5, a_178^0'=a_178^post5, k_121^0'=k_121^post5, k_83^0'=k_83^post5, len_181^0'=len_181^post5, len_54^0'=len_54^post5, lt_15^0'=lt_15^post5, result_4^0'=result_4^post5, tmp_8^0'=tmp_8^post5, x_12^0'=x_12^post5, x_13^0'=x_13^post5, x_7^0'=x_7^post5, y_11^0'=y_11^post5, y_14^0'=y_14^post5, (0 == 0 /\ 1-y_11^0+x_12^0 <= 0 /\ y_14^0-y_14^post5 == 0 /\ -a_10^post5+a_10^0 == 0 /\ a_178^0-a_178^post5 == 0 /\ k_121^0-k_121^post5 == 0 /\ -k_121^0 <= 0 /\ -len_54^post5+len_54^0 == 0 /\ -k_83^post5+k_83^0 == 0 /\ -tmp_8^post5+tmp_8^0 == 0 /\ x_7^0-x_7^post5 == 0 /\ -result_4^post5+result_4^0 == 0 /\ -1+len_181^post5 == 0 /\ __cil_tmp5_9^0-__cil_tmp5_9^post5 == 0 /\ -y_11^post5+y_11^0 == 0 /\ -lt_15^1+x_12^post5 == 0 /\ -x_13^post5+x_13^0 == 0), cost: 1
   5: l3 -> l4 : __cil_tmp5_9^0'=__cil_tmp5_9^post6, a_10^0'=a_10^post6, a_178^0'=a_178^post6, k_121^0'=k_121^post6, k_83^0'=k_83^post6, len_181^0'=len_181^post6, len_54^0'=len_54^post6, lt_15^0'=lt_15^post6, result_4^0'=result_4^post6, tmp_8^0'=tmp_8^post6, x_12^0'=x_12^post6, x_13^0'=x_13^post6, x_7^0'=x_7^post6, y_11^0'=y_11^post6, y_14^0'=y_14^post6, (0 == 0 /\ -y_11^0+x_12^0 <= 0 /\ x_12^0-x_12^post6 == 0 /\ -len_181^0 <= 0 /\ y_11^0-x_12^0 <= 0 /\ -a_178^post6+a_178^0 == 0 /\ -tmp_8^post6+tmp_8^0 == 0 /\ y_14^0-y_14^post6 == 0 /\ x_7^0-x_7^post6 == 0 /\ y_11^0-y_11^post6 == 0 /\ k_121^0-k_121^post6 == 0 /\ len_181^0-len_181^post6 == 0 /\ -k_83^post6+k_83^0 == 0 /\ -a_10^post6+a_10^0 == 0 /\ -x_13^post6+x_13^0 == 0 /\ __cil_tmp5_9^0-__cil_tmp5_9^post6 == 0 /\ -a_178^0 <= 0 /\ -len_54^post6+len_54^0 == 0 /\ lt_15^0-lt_15^post6 == 0), cost: 1
  12: l3 -> l3 : __cil_tmp5_9^0'=__cil_tmp5_9^post8, a_10^0'=a_10^post8, a_178^0'=a_178^post8, k_121^0'=k_121^post8, k_83^0'=k_83^post8, len_181^0'=len_181^post8, len_54^0'=len_54^post8, lt_15^0'=lt_15^post8, result_4^0'=result_4^post8, tmp_8^0'=tmp_8^post8, x_12^0'=x_12^post8, x_13^0'=x_13^post8, x_7^0'=x_7^post8, y_11^0'=y_11^post8, y_14^0'=y_14^post8, (0 == 0 /\ -a_10^post8+a_10^post7 == 0 /\ len_54^post7-len_54^post8 == 0 /\ y_14^0-y_14^post7 == 0 /\ -x_13^post8+x_13^post7 == 0 /\ x_7^0-x_7^post7 == 0 /\ -len_181^0 <= 0 /\ len_181^post7-len_181^post8 == 0 /\ 1+y_11^0-x_12^0 <= 0 /\ -y_11^post7+y_11^0 == 0 /\ __cil_tmp5_9^0-__cil_tmp5_9^post7 == 0 /\ -y_11^post8+y_11^post7 == 0 /\ x_12^post7-lt_15^1 == 0 /\ result_4^post7-result_4^post8 == 0 /\ -__cil_tmp5_9^post8+__cil_tmp5_9^post7 == 0 /\ -a_178^post7+a_178^0 == 0 /\ k_83^0-k_83^post7 == 0 /\ -y_14^post8+y_14^post7 == 0 /\ tmp_8^post7-tmp_8^post8 == 0 /\ -tmp_8^post7+tmp_8^0 == 0 /\ -k_121^post7+k_121^0 == 0 /\ a_178^post7-a_178^post8 == 0 /\ -lt_15^post8+lt_15^post7 == 0 /\ -x_12^post8+x_12^post7 == 0 /\ -k_121^post8+k_121^post7 == 0 /\ x_13^0-x_13^post7 == 0 /\ -1+len_181^post7-len_181^0 == 0 /\ -result_4^post7+result_4^0 == 0 /\ -a_178^0 <= 0 /\ -len_54^post7+len_54^0 == 0 /\ -k_83^post8+k_83^post7 == 0 /\ a_10^0-a_10^post7 == 0 /\ x_7^post7-x_7^post8 == 0), cost: 1
  13: l3 -> l3 : __cil_tmp5_9^0'=__cil_tmp5_9^post10, a_10^0'=a_10^post10, a_178^0'=a_178^post10, k_121^0'=k_121^post10, k_83^0'=k_83^post10, len_181^0'=len_181^post10, len_54^0'=len_54^post10, lt_15^0'=lt_15^post10, result_4^0'=result_4^post10, tmp_8^0'=tmp_8^post10, x_12^0'=x_12^post10, x_13^0'=x_13^post10, x_7^0'=x_7^post10, y_11^0'=y_11^post10, y_14^0'=y_14^post10, (0 == 0 /\ -a_178^post9+a_178^0 == 0 /\ -lt_15^post10+lt_15^post9 == 0 /\ 1-y_11^0+x_12^0 <= 0 /\ __cil_tmp5_9^0-__cil_tmp5_9^post9 == 0 /\ -y_14^post10+y_14^post9 == 0 /\ -1-len_181^0+len_181^post9 == 0 /\ -k_83^post10+k_83^post9 == 0 /\ -x_7^post10+x_7^post9 == 0 /\ -a_10^post9+a_10^0 == 0 /\ -len_181^0 <= 0 /\ -k_121^post10+k_121^post9 == 0 /\ k_121^0-k_121^post9 == 0 /\ -tmp_8^post10+tmp_8^post9 == 0 /\ -a_178^post10+a_178^post9 == 0 /\ a_10^post9-a_10^post10 == 0 /\ -x_12^post10+x_12^post9 == 0 /\ -x_13^post10+x_13^post9 == 0 /\ -__cil_tmp5_9^post10+__cil_tmp5_9^post9 == 0 /\ -tmp_8^post9+tmp_8^0 == 0 /\ y_14^0-y_14^post9 == 0 /\ y_11^0-y_11^post9 == 0 /\ -result_4^post10+result_4^post9 == 0 /\ -y_11^post10+y_11^post9 == 0 /\ x_7^0-x_7^post9 == 0 /\ -result_4^post9+result_4^0 == 0 /\ -len_181^post10+len_181^post9 == 0 /\ -lt_15^1+x_12^post9 == 0 /\ -k_83^post9+k_83^0 == 0 /\ -len_54^post10+len_54^post9 == 0 /\ -len_54^post9+len_54^0 == 0 /\ -x_13^post9+x_13^0 == 0 /\ -a_178^0 <= 0), cost: 1
  11: l7 -> l0 : __cil_tmp5_9^0'=__cil_tmp5_9^post3, a_10^0'=a_10^post3, a_178^0'=a_178^post3, k_121^0'=k_121^post3, k_83^0'=k_83^post3, len_181^0'=len_181^post3, len_54^0'=len_54^post3, lt_15^0'=lt_15^post3, result_4^0'=result_4^post3, tmp_8^0'=tmp_8^post3, x_12^0'=x_12^post3, x_13^0'=x_13^post3, x_7^0'=x_7^post3, y_11^0'=y_11^post3, y_14^0'=y_14^post3, (0 == 0 /\ -x_12^post3+x_12^post11 == 0 /\ -tmp_8^1+x_7^1 == 0 /\ -a_10^post3+a_10^post11 == 0 /\ x_13^post3-result_4^7 == 0 /\ result_4^3-__cil_tmp5_9^2 == 0 /\ -y_11^post11+y_11^0 == 0 /\ x_7^0-x_7^post11 == 0 /\ -len_54^post3 <= 0 /\ a_10^0-a_10^post11 == 0 /\ -x_7^3+__cil_tmp5_9^3 == 0 /\ -tmp_8^2+x_7^2 == 0 /\ result_4^5-__cil_tmp5_9^3 == 0 /\ -len_181^post11+len_181^0 == 0 /\ y_14^0-y_14^post11 == 0 /\ -k_121^post3+k_121^post11 == 0 /\ k_83^0-k_83^post11 == 0 /\ lt_15^0-lt_15^post11 == 0 /\ y_14^post3 == 0 /\ -1-len_54^post3+k_83^post3 == 0 /\ result_4^1-__cil_tmp5_9^1 == 0 /\ -tmp_8^post11+tmp_8^0 == 0 /\ -y_11^post3+y_11^post11 == 0 /\ -k_121^post11+k_121^0 == 0 /\ -__cil_tmp5_9^post11+__cil_tmp5_9^0 == 0 /\ a_178^post11-a_178^post3 == 0 /\ -x_7^2+__cil_tmp5_9^2 == 0 /\ -result_4^5+x_13^4 == 0 /\ len_181^post11-len_181^post3 == 0 /\ -result_4^3+x_13^3 == 0 /\ x_7^3-tmp_8^3 == 0 /\ -x_7^1+__cil_tmp5_9^1 == 0 /\ -tmp_8^post3+x_7^post3 == 0 /\ -2+len_54^post3 == 0 /\ -len_54^post11+len_54^0 == 0 /\ -__cil_tmp5_9^post3+result_4^7 == 0 /\ x_13^0-x_13^post11 == 0 /\ __cil_tmp5_9^post3-x_7^post3 == 0 /\ -x_12^post11+x_12^0 == 0 /\ -a_178^post11+a_178^0 == 0 /\ -result_4^1+x_13^2 == 0 /\ -k_83^post3 <= 0 /\ x_13^1 == 0 /\ -result_4^post11+result_4^0 == 0 /\ -k_121^post11 <= 0 /\ -lt_15^post3+lt_15^post11 == 0), cost: 1

	Eliminating location l2 by chaining:

	Applied chaining

	First rule:
	l7 -> l2 : __cil_tmp5_9^0'=__cil_tmp5_9^post11, a_10^0'=a_10^post11, a_178^0'=a_178^post11, k_121^0'=k_121^post11, k_83^0'=k_83^post11, len_181^0'=len_181^post11, len_54^0'=len_54^post11, lt_15^0'=lt_15^post11, result_4^0'=result_4^post11, tmp_8^0'=tmp_8^post11, x_12^0'=x_12^post11, x_13^0'=x_13^post11, x_7^0'=x_7^post11, y_11^0'=y_11^post11, y_14^0'=y_14^post11, (-y_11^post11+y_11^0 == 0 /\ x_7^0-x_7^post11 == 0 /\ a_10^0-a_10^post11 == 0 /\ -len_181^post11+len_181^0 == 0 /\ y_14^0-y_14^post11 == 0 /\ k_83^0-k_83^post11 == 0 /\ lt_15^0-lt_15^post11 == 0 /\ -tmp_8^post11+tmp_8^0 == 0 /\ -k_121^post11+k_121^0 == 0 /\ -__cil_tmp5_9^post11+__cil_tmp5_9^0 == 0 /\ -len_54^post11+len_54^0 == 0 /\ x_13^0-x_13^post11 == 0 /\ -x_12^post11+x_12^0 == 0 /\ -a_178^post11+a_178^0 == 0 /\ -result_4^post11+result_4^0 == 0), cost: 1
	Second rule:
	l2 -> l0 : __cil_tmp5_9^0'=__cil_tmp5_9^post3, a_10^0'=a_10^post3, a_178^0'=a_178^post3, k_121^0'=k_121^post3, k_83^0'=k_83^post3, len_181^0'=len_181^post3, len_54^0'=len_54^post3, lt_15^0'=lt_15^post3, result_4^0'=result_4^post3, tmp_8^0'=tmp_8^post3, x_12^0'=x_12^post3, x_13^0'=x_13^post3, x_7^0'=x_7^post3, y_11^0'=y_11^post3, y_14^0'=y_14^post3, (0 == 0 /\ -x_12^post3+x_12^0 == 0 /\ -tmp_8^1+x_7^1 == 0 /\ x_13^post3-result_4^7 == 0 /\ result_4^3-__cil_tmp5_9^2 == 0 /\ -len_54^post3 <= 0 /\ -x_7^3+__cil_tmp5_9^3 == 0 /\ -tmp_8^2+x_7^2 == 0 /\ result_4^5-__cil_tmp5_9^3 == 0 /\ -k_121^0 <= 0 /\ a_178^0-a_178^post3 == 0 /\ a_10^0-a_10^post3 == 0 /\ y_14^post3 == 0 /\ -1-len_54^post3+k_83^post3 == 0 /\ result_4^1-__cil_tmp5_9^1 == 0 /\ len_181^0-len_181^post3 == 0 /\ -x_7^2+__cil_tmp5_9^2 == 0 /\ -result_4^5+x_13^4 == 0 /\ -result_4^3+x_13^3 == 0 /\ x_7^3-tmp_8^3 == 0 /\ -x_7^1+__cil_tmp5_9^1 == 0 /\ -tmp_8^post3+x_7^post3 == 0 /\ -y_11^post3+y_11^0 == 0 /\ -2+len_54^post3 == 0 /\ -__cil_tmp5_9^post3+result_4^7 == 0 /\ -k_121^post3+k_121^0 == 0 /\ __cil_tmp5_9^post3-x_7^post3 == 0 /\ lt_15^0-lt_15^post3 == 0 /\ -result_4^1+x_13^2 == 0 /\ -k_83^post3 <= 0 /\ x_13^1 == 0), cost: 1
	New rule:
	l7 -> l0 : __cil_tmp5_9^0'=__cil_tmp5_9^post3, a_10^0'=a_10^post3, a_178^0'=a_178^post3, k_121^0'=k_121^post3, k_83^0'=k_83^post3, len_181^0'=len_181^post3, len_54^0'=len_54^post3, lt_15^0'=lt_15^post3, result_4^0'=result_4^post3, tmp_8^0'=tmp_8^post3, x_12^0'=x_12^post3, x_13^0'=x_13^post3, x_7^0'=x_7^post3, y_11^0'=y_11^post3, y_14^0'=y_14^post3, (0 == 0 /\ -x_12^post3+x_12^post11 == 0 /\ -tmp_8^1+x_7^1 == 0 /\ -a_10^post3+a_10^post11 == 0 /\ x_13^post3-result_4^7 == 0 /\ result_4^3-__cil_tmp5_9^2 == 0 /\ -y_11^post11+y_11^0 == 0 /\ x_7^0-x_7^post11 == 0 /\ -len_54^post3 <= 0 /\ a_10^0-a_10^post11 == 0 /\ -x_7^3+__cil_tmp5_9^3 == 0 /\ -tmp_8^2+x_7^2 == 0 /\ result_4^5-__cil_tmp5_9^3 == 0 /\ -len_181^post11+len_181^0 == 0 /\ y_14^0-y_14^post11 == 0 /\ -k_121^post3+k_121^post11 == 0 /\ k_83^0-k_83^post11 == 0 /\ lt_15^0-lt_15^post11 == 0 /\ y_14^post3 == 0 /\ -1-len_54^post3+k_83^post3 == 0 /\ result_4^1-__cil_tmp5_9^1 == 0 /\ -tmp_8^post11+tmp_8^0 == 0 /\ -y_11^post3+y_11^post11 == 0 /\ -k_121^post11+k_121^0 == 0 /\ -__cil_tmp5_9^post11+__cil_tmp5_9^0 == 0 /\ a_178^post11-a_178^post3 == 0 /\ -x_7^2+__cil_tmp5_9^2 == 0 /\ -result_4^5+x_13^4 == 0 /\ len_181^post11-len_181^post3 == 0 /\ -result_4^3+x_13^3 == 0 /\ x_7^3-tmp_8^3 == 0 /\ -x_7^1+__cil_tmp5_9^1 == 0 /\ -tmp_8^post3+x_7^post3 == 0 /\ -2+len_54^post3 == 0 /\ -len_54^post11+len_54^0 == 0 /\ -__cil_tmp5_9^post3+result_4^7 == 0 /\ x_13^0-x_13^post11 == 0 /\ __cil_tmp5_9^post3-x_7^post3 == 0 /\ -x_12^post11+x_12^0 == 0 /\ -a_178^post11+a_178^0 == 0 /\ -result_4^1+x_13^2 == 0 /\ -k_83^post3 <= 0 /\ x_13^1 == 0 /\ -result_4^post11+result_4^0 == 0 /\ -k_121^post11 <= 0 /\ -lt_15^post3+lt_15^post11 == 0), cost: 1
	
	Applied deletion

	Removed the following rules: 2 10
	
	Eliminating location l5 by chaining:

	Applied chaining

	First rule:
	l3 -> l5 : __cil_tmp5_9^0'=__cil_tmp5_9^post7, a_10^0'=a_10^post7, a_178^0'=a_178^post7, k_121^0'=k_121^post7, k_83^0'=k_83^post7, len_181^0'=len_181^post7, len_54^0'=len_54^post7, lt_15^0'=lt_15^post7, result_4^0'=result_4^post7, tmp_8^0'=tmp_8^post7, x_12^0'=x_12^post7, x_13^0'=x_13^post7, x_7^0'=x_7^post7, y_11^0'=y_11^post7, y_14^0'=y_14^post7, (0 == 0 /\ y_14^0-y_14^post7 == 0 /\ x_7^0-x_7^post7 == 0 /\ -len_181^0 <= 0 /\ 1+y_11^0-x_12^0 <= 0 /\ -y_11^post7+y_11^0 == 0 /\ __cil_tmp5_9^0-__cil_tmp5_9^post7 == 0 /\ x_12^post7-lt_15^1 == 0 /\ -a_178^post7+a_178^0 == 0 /\ k_83^0-k_83^post7 == 0 /\ -tmp_8^post7+tmp_8^0 == 0 /\ -k_121^post7+k_121^0 == 0 /\ x_13^0-x_13^post7 == 0 /\ -1+len_181^post7-len_181^0 == 0 /\ -result_4^post7+result_4^0 == 0 /\ -a_178^0 <= 0 /\ -len_54^post7+len_54^0 == 0 /\ a_10^0-a_10^post7 == 0), cost: 1
	Second rule:
	l5 -> l3 : __cil_tmp5_9^0'=__cil_tmp5_9^post8, a_10^0'=a_10^post8, a_178^0'=a_178^post8, k_121^0'=k_121^post8, k_83^0'=k_83^post8, len_181^0'=len_181^post8, len_54^0'=len_54^post8, lt_15^0'=lt_15^post8, result_4^0'=result_4^post8, tmp_8^0'=tmp_8^post8, x_12^0'=x_12^post8, x_13^0'=x_13^post8, x_7^0'=x_7^post8, y_11^0'=y_11^post8, y_14^0'=y_14^post8, (y_14^0-y_14^post8 == 0 /\ len_181^0-len_181^post8 == 0 /\ x_7^0-x_7^post8 == 0 /\ len_54^0-len_54^post8 == 0 /\ -lt_15^post8+lt_15^0 == 0 /\ -y_11^post8+y_11^0 == 0 /\ -k_121^post8+k_121^0 == 0 /\ -__cil_tmp5_9^post8+__cil_tmp5_9^0 == 0 /\ a_10^0-a_10^post8 == 0 /\ -k_83^post8+k_83^0 == 0 /\ -tmp_8^post8+tmp_8^0 == 0 /\ -result_4^post8+result_4^0 == 0 /\ a_178^0-a_178^post8 == 0 /\ -x_12^post8+x_12^0 == 0 /\ -x_13^post8+x_13^0 == 0), cost: 1
	New rule:
	l3 -> l3 : __cil_tmp5_9^0'=__cil_tmp5_9^post8, a_10^0'=a_10^post8, a_178^0'=a_178^post8, k_121^0'=k_121^post8, k_83^0'=k_83^post8, len_181^0'=len_181^post8, len_54^0'=len_54^post8, lt_15^0'=lt_15^post8, result_4^0'=result_4^post8, tmp_8^0'=tmp_8^post8, x_12^0'=x_12^post8, x_13^0'=x_13^post8, x_7^0'=x_7^post8, y_11^0'=y_11^post8, y_14^0'=y_14^post8, (0 == 0 /\ -a_10^post8+a_10^post7 == 0 /\ len_54^post7-len_54^post8 == 0 /\ y_14^0-y_14^post7 == 0 /\ -x_13^post8+x_13^post7 == 0 /\ x_7^0-x_7^post7 == 0 /\ -len_181^0 <= 0 /\ len_181^post7-len_181^post8 == 0 /\ 1+y_11^0-x_12^0 <= 0 /\ -y_11^post7+y_11^0 == 0 /\ __cil_tmp5_9^0-__cil_tmp5_9^post7 == 0 /\ -y_11^post8+y_11^post7 == 0 /\ x_12^post7-lt_15^1 == 0 /\ result_4^post7-result_4^post8 == 0 /\ -__cil_tmp5_9^post8+__cil_tmp5_9^post7 == 0 /\ -a_178^post7+a_178^0 == 0 /\ k_83^0-k_83^post7 == 0 /\ -y_14^post8+y_14^post7 == 0 /\ tmp_8^post7-tmp_8^post8 == 0 /\ -tmp_8^post7+tmp_8^0 == 0 /\ -k_121^post7+k_121^0 == 0 /\ a_178^post7-a_178^post8 == 0 /\ -lt_15^post8+lt_15^post7 == 0 /\ -x_12^post8+x_12^post7 == 0 /\ -k_121^post8+k_121^post7 == 0 /\ x_13^0-x_13^post7 == 0 /\ -1+len_181^post7-len_181^0 == 0 /\ -result_4^post7+result_4^0 == 0 /\ -a_178^0 <= 0 /\ -len_54^post7+len_54^0 == 0 /\ -k_83^post8+k_83^post7 == 0 /\ a_10^0-a_10^post7 == 0 /\ x_7^post7-x_7^post8 == 0), cost: 1
	
	Applied deletion

	Removed the following rules: 6 7
	
	Eliminating location l6 by chaining:

	Applied chaining

	First rule:
	l3 -> l6 : __cil_tmp5_9^0'=__cil_tmp5_9^post9, a_10^0'=a_10^post9, a_178^0'=a_178^post9, k_121^0'=k_121^post9, k_83^0'=k_83^post9, len_181^0'=len_181^post9, len_54^0'=len_54^post9, lt_15^0'=lt_15^post9, result_4^0'=result_4^post9, tmp_8^0'=tmp_8^post9, x_12^0'=x_12^post9, x_13^0'=x_13^post9, x_7^0'=x_7^post9, y_11^0'=y_11^post9, y_14^0'=y_14^post9, (0 == 0 /\ -a_178^post9+a_178^0 == 0 /\ 1-y_11^0+x_12^0 <= 0 /\ __cil_tmp5_9^0-__cil_tmp5_9^post9 == 0 /\ -1-len_181^0+len_181^post9 == 0 /\ -a_10^post9+a_10^0 == 0 /\ -len_181^0 <= 0 /\ k_121^0-k_121^post9 == 0 /\ -tmp_8^post9+tmp_8^0 == 0 /\ y_14^0-y_14^post9 == 0 /\ y_11^0-y_11^post9 == 0 /\ x_7^0-x_7^post9 == 0 /\ -result_4^post9+result_4^0 == 0 /\ -lt_15^1+x_12^post9 == 0 /\ -k_83^post9+k_83^0 == 0 /\ -len_54^post9+len_54^0 == 0 /\ -x_13^post9+x_13^0 == 0 /\ -a_178^0 <= 0), cost: 1
	Second rule:
	l6 -> l3 : __cil_tmp5_9^0'=__cil_tmp5_9^post10, a_10^0'=a_10^post10, a_178^0'=a_178^post10, k_121^0'=k_121^post10, k_83^0'=k_83^post10, len_181^0'=len_181^post10, len_54^0'=len_54^post10, lt_15^0'=lt_15^post10, result_4^0'=result_4^post10, tmp_8^0'=tmp_8^post10, x_12^0'=x_12^post10, x_13^0'=x_13^post10, x_7^0'=x_7^post10, y_11^0'=y_11^post10, y_14^0'=y_14^post10, (-y_14^post10+y_14^0 == 0 /\ x_12^0-x_12^post10 == 0 /\ -a_178^post10+a_178^0 == 0 /\ -tmp_8^post10+tmp_8^0 == 0 /\ y_11^0-y_11^post10 == 0 /\ len_181^0-len_181^post10 == 0 /\ x_7^0-x_7^post10 == 0 /\ k_121^0-k_121^post10 == 0 /\ a_10^0-a_10^post10 == 0 /\ -x_13^post10+x_13^0 == 0 /\ -len_54^post10+len_54^0 == 0 /\ -result_4^post10+result_4^0 == 0 /\ lt_15^0-lt_15^post10 == 0 /\ -k_83^post10+k_83^0 == 0 /\ -__cil_tmp5_9^post10+__cil_tmp5_9^0 == 0), cost: 1
	New rule:
	l3 -> l3 : __cil_tmp5_9^0'=__cil_tmp5_9^post10, a_10^0'=a_10^post10, a_178^0'=a_178^post10, k_121^0'=k_121^post10, k_83^0'=k_83^post10, len_181^0'=len_181^post10, len_54^0'=len_54^post10, lt_15^0'=lt_15^post10, result_4^0'=result_4^post10, tmp_8^0'=tmp_8^post10, x_12^0'=x_12^post10, x_13^0'=x_13^post10, x_7^0'=x_7^post10, y_11^0'=y_11^post10, y_14^0'=y_14^post10, (0 == 0 /\ -a_178^post9+a_178^0 == 0 /\ -lt_15^post10+lt_15^post9 == 0 /\ 1-y_11^0+x_12^0 <= 0 /\ __cil_tmp5_9^0-__cil_tmp5_9^post9 == 0 /\ -y_14^post10+y_14^post9 == 0 /\ -1-len_181^0+len_181^post9 == 0 /\ -k_83^post10+k_83^post9 == 0 /\ -x_7^post10+x_7^post9 == 0 /\ -a_10^post9+a_10^0 == 0 /\ -len_181^0 <= 0 /\ -k_121^post10+k_121^post9 == 0 /\ k_121^0-k_121^post9 == 0 /\ -tmp_8^post10+tmp_8^post9 == 0 /\ -a_178^post10+a_178^post9 == 0 /\ a_10^post9-a_10^post10 == 0 /\ -x_12^post10+x_12^post9 == 0 /\ -x_13^post10+x_13^post9 == 0 /\ -__cil_tmp5_9^post10+__cil_tmp5_9^post9 == 0 /\ -tmp_8^post9+tmp_8^0 == 0 /\ y_14^0-y_14^post9 == 0 /\ y_11^0-y_11^post9 == 0 /\ -result_4^post10+result_4^post9 == 0 /\ -y_11^post10+y_11^post9 == 0 /\ x_7^0-x_7^post9 == 0 /\ -result_4^post9+result_4^0 == 0 /\ -len_181^post10+len_181^post9 == 0 /\ -lt_15^1+x_12^post9 == 0 /\ -k_83^post9+k_83^0 == 0 /\ -len_54^post10+len_54^post9 == 0 /\ -len_54^post9+len_54^0 == 0 /\ -x_13^post9+x_13^0 == 0 /\ -a_178^0 <= 0), cost: 1
	
	Applied deletion

	Removed the following rules: 8 9

Simplified Transitions

Start location: l7
Program variables: __cil_tmp5_9^0 a_10^0 a_178^0 k_121^0 k_83^0 len_181^0 len_54^0 lt_15^0 result_4^0 tmp_8^0 x_12^0 x_13^0 x_7^0 y_11^0 y_14^0
  14: l0 -> l1 : x_12^0'=a_10^0, (1-a_10^0+y_11^0 <= 0 /\ -k_121^0 <= 0), cost: 1
  15: l0 -> l1 : x_12^0'=a_10^0, (-k_121^0 <= 0 /\ 1+a_10^0-y_11^0 <= 0), cost: 1
  16: l1 -> l3 : len_181^0'=1, lt_15^0'=lt_15^post4, x_12^0'=lt_15^1, (1+y_11^0-x_12^0 <= 0 /\ -k_121^0 <= 0), cost: 1
  17: l1 -> l3 : len_181^0'=1, lt_15^0'=lt_15^post5, x_12^0'=lt_15^1, (1-y_11^0+x_12^0 <= 0 /\ -k_121^0 <= 0), cost: 1
  18: l3 -> l4 : result_4^0'=result_4^post6, (-y_11^0+x_12^0 <= 0 /\ -y_11^0+x_12^0 == 0 /\ -len_181^0 <= 0 /\ y_11^0-x_12^0 <= 0 /\ -a_178^0 <= 0), cost: 1
  20: l3 -> l3 : len_181^0'=1+len_181^0, lt_15^0'=lt_15^post7, x_12^0'=x_12^post7, (-len_181^0 <= 0 /\ 1+y_11^0-x_12^0 <= 0 /\ -a_178^0 <= 0), cost: 1
  21: l3 -> l3 : len_181^0'=1+len_181^0, lt_15^0'=lt_15^post9, x_12^0'=x_12^post9, (1-y_11^0+x_12^0 <= 0 /\ -len_181^0 <= 0 /\ -a_178^0 <= 0), cost: 1
  19: l7 -> l0 : __cil_tmp5_9^0'=result_4^7, k_83^0'=3, len_54^0'=2, result_4^0'=result_4^post3, tmp_8^0'=result_4^7, x_13^0'=result_4^7, x_7^0'=result_4^7, y_14^0'=0, -k_121^0 <= 0, cost: 1

	Propagated Equalities

	Original rule:
	l0 -> l1 : __cil_tmp5_9^0'=__cil_tmp5_9^post1, a_10^0'=a_10^post1, a_178^0'=a_178^post1, k_121^0'=k_121^post1, k_83^0'=k_83^post1, len_181^0'=len_181^post1, len_54^0'=len_54^post1, lt_15^0'=lt_15^post1, result_4^0'=result_4^post1, tmp_8^0'=tmp_8^post1, x_12^0'=x_12^post1, x_13^0'=x_13^post1, x_7^0'=x_7^post1, y_11^0'=y_11^post1, y_14^0'=y_14^post1, (-y_11^post1+y_11^0 == 0 /\ -result_4^post1+result_4^0 == 0 /\ a_178^0-a_178^post1 == 0 /\ k_83^0-k_83^post1 == 0 /\ -__cil_tmp5_9^post1+__cil_tmp5_9^0 == 0 /\ -len_54^post1+len_54^0 == 0 /\ x_7^0-x_7^post1 == 0 /\ a_10^0-a_10^post1 == 0 /\ -k_121^0 <= 0 /\ 1-x_12^post1+y_11^0 <= 0 /\ x_13^0-x_13^post1 == 0 /\ y_14^0-y_14^post1 == 0 /\ len_181^0-len_181^post1 == 0 /\ -a_10^0+x_12^post1 == 0 /\ -k_121^post1+k_121^0 == 0 /\ lt_15^0-lt_15^post1 == 0 /\ -tmp_8^post1+tmp_8^0 == 0), cost: 1
	New rule:
	l0 -> l1 : __cil_tmp5_9^0'=__cil_tmp5_9^0, a_10^0'=a_10^0, a_178^0'=a_178^0, k_121^0'=k_121^0, k_83^0'=k_83^0, len_181^0'=len_181^0, len_54^0'=len_54^0, lt_15^0'=lt_15^0, result_4^0'=result_4^0, tmp_8^0'=tmp_8^0, x_12^0'=a_10^0, x_13^0'=x_13^0, x_7^0'=x_7^0, y_11^0'=y_11^0, y_14^0'=y_14^0, (0 == 0 /\ 1-a_10^0+y_11^0 <= 0 /\ -k_121^0 <= 0), cost: 1
	
		propagated equality y_11^post1 = y_11^0
		
		propagated equality result_4^post1 = result_4^0
		
		propagated equality a_178^post1 = a_178^0
		
		propagated equality k_83^post1 = k_83^0
		
		propagated equality __cil_tmp5_9^post1 = __cil_tmp5_9^0
		
		propagated equality len_54^post1 = len_54^0
		
		propagated equality x_7^post1 = x_7^0
		
		propagated equality a_10^post1 = a_10^0
		
		propagated equality x_13^post1 = x_13^0
		
		propagated equality y_14^post1 = y_14^0
		
		propagated equality len_181^post1 = len_181^0
		
		propagated equality x_12^post1 = a_10^0
		
		propagated equality k_121^post1 = k_121^0
		
		propagated equality lt_15^post1 = lt_15^0
		
		propagated equality tmp_8^post1 = tmp_8^0
		
	Simplified Guard

	Original rule:
	l0 -> l1 : __cil_tmp5_9^0'=__cil_tmp5_9^0, a_10^0'=a_10^0, a_178^0'=a_178^0, k_121^0'=k_121^0, k_83^0'=k_83^0, len_181^0'=len_181^0, len_54^0'=len_54^0, lt_15^0'=lt_15^0, result_4^0'=result_4^0, tmp_8^0'=tmp_8^0, x_12^0'=a_10^0, x_13^0'=x_13^0, x_7^0'=x_7^0, y_11^0'=y_11^0, y_14^0'=y_14^0, (0 == 0 /\ 1-a_10^0+y_11^0 <= 0 /\ -k_121^0 <= 0), cost: 1
	New rule:
	l0 -> l1 : __cil_tmp5_9^0'=__cil_tmp5_9^0, a_10^0'=a_10^0, a_178^0'=a_178^0, k_121^0'=k_121^0, k_83^0'=k_83^0, len_181^0'=len_181^0, len_54^0'=len_54^0, lt_15^0'=lt_15^0, result_4^0'=result_4^0, tmp_8^0'=tmp_8^0, x_12^0'=a_10^0, x_13^0'=x_13^0, x_7^0'=x_7^0, y_11^0'=y_11^0, y_14^0'=y_14^0, (1-a_10^0+y_11^0 <= 0 /\ -k_121^0 <= 0), cost: 1
	
	Removed Trivial Updates

	Original rule:
	l0 -> l1 : __cil_tmp5_9^0'=__cil_tmp5_9^0, a_10^0'=a_10^0, a_178^0'=a_178^0, k_121^0'=k_121^0, k_83^0'=k_83^0, len_181^0'=len_181^0, len_54^0'=len_54^0, lt_15^0'=lt_15^0, result_4^0'=result_4^0, tmp_8^0'=tmp_8^0, x_12^0'=a_10^0, x_13^0'=x_13^0, x_7^0'=x_7^0, y_11^0'=y_11^0, y_14^0'=y_14^0, (1-a_10^0+y_11^0 <= 0 /\ -k_121^0 <= 0), cost: 1
	New rule:
	l0 -> l1 : x_12^0'=a_10^0, (1-a_10^0+y_11^0 <= 0 /\ -k_121^0 <= 0), cost: 1
	
	Propagated Equalities

	Original rule:
	l0 -> l1 : __cil_tmp5_9^0'=__cil_tmp5_9^post2, a_10^0'=a_10^post2, a_178^0'=a_178^post2, k_121^0'=k_121^post2, k_83^0'=k_83^post2, len_181^0'=len_181^post2, len_54^0'=len_54^post2, lt_15^0'=lt_15^post2, result_4^0'=result_4^post2, tmp_8^0'=tmp_8^post2, x_12^0'=x_12^post2, x_13^0'=x_13^post2, x_7^0'=x_7^post2, y_11^0'=y_11^post2, y_14^0'=y_14^post2, (-k_83^post2+k_83^0 == 0 /\ k_121^0-k_121^post2 == 0 /\ -result_4^post2+result_4^0 == 0 /\ 1+x_12^post2-y_11^0 <= 0 /\ -y_11^post2+y_11^0 == 0 /\ len_181^0-len_181^post2 == 0 /\ -lt_15^post2+lt_15^0 == 0 /\ len_54^0-len_54^post2 == 0 /\ y_14^0-y_14^post2 == 0 /\ -k_121^0 <= 0 /\ __cil_tmp5_9^0-__cil_tmp5_9^post2 == 0 /\ a_178^0-a_178^post2 == 0 /\ -x_13^post2+x_13^0 == 0 /\ x_12^post2-a_10^0 == 0 /\ x_7^0-x_7^post2 == 0 /\ a_10^0-a_10^post2 == 0 /\ -tmp_8^post2+tmp_8^0 == 0), cost: 1
	New rule:
	l0 -> l1 : __cil_tmp5_9^0'=__cil_tmp5_9^0, a_10^0'=a_10^0, a_178^0'=a_178^0, k_121^0'=k_121^0, k_83^0'=k_83^0, len_181^0'=len_181^0, len_54^0'=len_54^0, lt_15^0'=lt_15^0, result_4^0'=result_4^0, tmp_8^0'=tmp_8^0, x_12^0'=a_10^0, x_13^0'=x_13^0, x_7^0'=x_7^0, y_11^0'=y_11^0, y_14^0'=y_14^0, (0 == 0 /\ -k_121^0 <= 0 /\ 1+a_10^0-y_11^0 <= 0), cost: 1
	
		propagated equality k_83^post2 = k_83^0
		
		propagated equality k_121^post2 = k_121^0
		
		propagated equality result_4^post2 = result_4^0
		
		propagated equality y_11^post2 = y_11^0
		
		propagated equality len_181^post2 = len_181^0
		
		propagated equality lt_15^post2 = lt_15^0
		
		propagated equality len_54^post2 = len_54^0
		
		propagated equality y_14^post2 = y_14^0
		
		propagated equality __cil_tmp5_9^post2 = __cil_tmp5_9^0
		
		propagated equality a_178^post2 = a_178^0
		
		propagated equality x_13^post2 = x_13^0
		
		propagated equality x_12^post2 = a_10^0
		
		propagated equality x_7^post2 = x_7^0
		
		propagated equality a_10^post2 = a_10^0
		
		propagated equality tmp_8^post2 = tmp_8^0
		
	Simplified Guard

	Original rule:
	l0 -> l1 : __cil_tmp5_9^0'=__cil_tmp5_9^0, a_10^0'=a_10^0, a_178^0'=a_178^0, k_121^0'=k_121^0, k_83^0'=k_83^0, len_181^0'=len_181^0, len_54^0'=len_54^0, lt_15^0'=lt_15^0, result_4^0'=result_4^0, tmp_8^0'=tmp_8^0, x_12^0'=a_10^0, x_13^0'=x_13^0, x_7^0'=x_7^0, y_11^0'=y_11^0, y_14^0'=y_14^0, (0 == 0 /\ -k_121^0 <= 0 /\ 1+a_10^0-y_11^0 <= 0), cost: 1
	New rule:
	l0 -> l1 : __cil_tmp5_9^0'=__cil_tmp5_9^0, a_10^0'=a_10^0, a_178^0'=a_178^0, k_121^0'=k_121^0, k_83^0'=k_83^0, len_181^0'=len_181^0, len_54^0'=len_54^0, lt_15^0'=lt_15^0, result_4^0'=result_4^0, tmp_8^0'=tmp_8^0, x_12^0'=a_10^0, x_13^0'=x_13^0, x_7^0'=x_7^0, y_11^0'=y_11^0, y_14^0'=y_14^0, (-k_121^0 <= 0 /\ 1+a_10^0-y_11^0 <= 0), cost: 1
	
	Removed Trivial Updates

	Original rule:
	l0 -> l1 : __cil_tmp5_9^0'=__cil_tmp5_9^0, a_10^0'=a_10^0, a_178^0'=a_178^0, k_121^0'=k_121^0, k_83^0'=k_83^0, len_181^0'=len_181^0, len_54^0'=len_54^0, lt_15^0'=lt_15^0, result_4^0'=result_4^0, tmp_8^0'=tmp_8^0, x_12^0'=a_10^0, x_13^0'=x_13^0, x_7^0'=x_7^0, y_11^0'=y_11^0, y_14^0'=y_14^0, (-k_121^0 <= 0 /\ 1+a_10^0-y_11^0 <= 0), cost: 1
	New rule:
	l0 -> l1 : x_12^0'=a_10^0, (-k_121^0 <= 0 /\ 1+a_10^0-y_11^0 <= 0), cost: 1
	
	Propagated Equalities

	Original rule:
	l1 -> l3 : __cil_tmp5_9^0'=__cil_tmp5_9^post4, a_10^0'=a_10^post4, a_178^0'=a_178^post4, k_121^0'=k_121^post4, k_83^0'=k_83^post4, len_181^0'=len_181^post4, len_54^0'=len_54^post4, lt_15^0'=lt_15^post4, result_4^0'=result_4^post4, tmp_8^0'=tmp_8^post4, x_12^0'=x_12^post4, x_13^0'=x_13^post4, x_7^0'=x_7^post4, y_11^0'=y_11^post4, y_14^0'=y_14^post4, (0 == 0 /\ -1+len_181^post4 == 0 /\ x_12^post4-lt_15^1 == 0 /\ 1+y_11^0-x_12^0 <= 0 /\ -k_121^0 <= 0 /\ -k_121^post4+k_121^0 == 0 /\ len_54^0-len_54^post4 == 0 /\ -__cil_tmp5_9^post4+__cil_tmp5_9^0 == 0 /\ x_7^0-x_7^post4 == 0 /\ a_10^0-a_10^post4 == 0 /\ -k_83^post4+k_83^0 == 0 /\ -tmp_8^post4+tmp_8^0 == 0 /\ -result_4^post4+result_4^0 == 0 /\ a_178^0-a_178^post4 == 0 /\ y_14^0-y_14^post4 == 0 /\ -y_11^post4+y_11^0 == 0 /\ -x_13^post4+x_13^0 == 0), cost: 1
	New rule:
	l1 -> l3 : __cil_tmp5_9^0'=__cil_tmp5_9^0, a_10^0'=a_10^0, a_178^0'=a_178^0, k_121^0'=k_121^0, k_83^0'=k_83^0, len_181^0'=1, len_54^0'=len_54^0, lt_15^0'=lt_15^post4, result_4^0'=result_4^0, tmp_8^0'=tmp_8^0, x_12^0'=lt_15^1, x_13^0'=x_13^0, x_7^0'=x_7^0, y_11^0'=y_11^0, y_14^0'=y_14^0, (0 == 0 /\ 1+y_11^0-x_12^0 <= 0 /\ -k_121^0 <= 0), cost: 1
	
		propagated equality len_181^post4 = 1
		
		propagated equality x_12^post4 = lt_15^1
		
		propagated equality k_121^post4 = k_121^0
		
		propagated equality len_54^post4 = len_54^0
		
		propagated equality __cil_tmp5_9^post4 = __cil_tmp5_9^0
		
		propagated equality x_7^post4 = x_7^0
		
		propagated equality a_10^post4 = a_10^0
		
		propagated equality k_83^post4 = k_83^0
		
		propagated equality tmp_8^post4 = tmp_8^0
		
		propagated equality result_4^post4 = result_4^0
		
		propagated equality a_178^post4 = a_178^0
		
		propagated equality y_14^post4 = y_14^0
		
		propagated equality y_11^post4 = y_11^0
		
		propagated equality x_13^post4 = x_13^0
		
	Simplified Guard

	Original rule:
	l1 -> l3 : __cil_tmp5_9^0'=__cil_tmp5_9^0, a_10^0'=a_10^0, a_178^0'=a_178^0, k_121^0'=k_121^0, k_83^0'=k_83^0, len_181^0'=1, len_54^0'=len_54^0, lt_15^0'=lt_15^post4, result_4^0'=result_4^0, tmp_8^0'=tmp_8^0, x_12^0'=lt_15^1, x_13^0'=x_13^0, x_7^0'=x_7^0, y_11^0'=y_11^0, y_14^0'=y_14^0, (0 == 0 /\ 1+y_11^0-x_12^0 <= 0 /\ -k_121^0 <= 0), cost: 1
	New rule:
	l1 -> l3 : __cil_tmp5_9^0'=__cil_tmp5_9^0, a_10^0'=a_10^0, a_178^0'=a_178^0, k_121^0'=k_121^0, k_83^0'=k_83^0, len_181^0'=1, len_54^0'=len_54^0, lt_15^0'=lt_15^post4, result_4^0'=result_4^0, tmp_8^0'=tmp_8^0, x_12^0'=lt_15^1, x_13^0'=x_13^0, x_7^0'=x_7^0, y_11^0'=y_11^0, y_14^0'=y_14^0, (1+y_11^0-x_12^0 <= 0 /\ -k_121^0 <= 0), cost: 1
	
	Removed Trivial Updates

	Original rule:
	l1 -> l3 : __cil_tmp5_9^0'=__cil_tmp5_9^0, a_10^0'=a_10^0, a_178^0'=a_178^0, k_121^0'=k_121^0, k_83^0'=k_83^0, len_181^0'=1, len_54^0'=len_54^0, lt_15^0'=lt_15^post4, result_4^0'=result_4^0, tmp_8^0'=tmp_8^0, x_12^0'=lt_15^1, x_13^0'=x_13^0, x_7^0'=x_7^0, y_11^0'=y_11^0, y_14^0'=y_14^0, (1+y_11^0-x_12^0 <= 0 /\ -k_121^0 <= 0), cost: 1
	New rule:
	l1 -> l3 : len_181^0'=1, lt_15^0'=lt_15^post4, x_12^0'=lt_15^1, (1+y_11^0-x_12^0 <= 0 /\ -k_121^0 <= 0), cost: 1
	
	Propagated Equalities

	Original rule:
	l1 -> l3 : __cil_tmp5_9^0'=__cil_tmp5_9^post5, a_10^0'=a_10^post5, a_178^0'=a_178^post5, k_121^0'=k_121^post5, k_83^0'=k_83^post5, len_181^0'=len_181^post5, len_54^0'=len_54^post5, lt_15^0'=lt_15^post5, result_4^0'=result_4^post5, tmp_8^0'=tmp_8^post5, x_12^0'=x_12^post5, x_13^0'=x_13^post5, x_7^0'=x_7^post5, y_11^0'=y_11^post5, y_14^0'=y_14^post5, (0 == 0 /\ 1-y_11^0+x_12^0 <= 0 /\ y_14^0-y_14^post5 == 0 /\ -a_10^post5+a_10^0 == 0 /\ a_178^0-a_178^post5 == 0 /\ k_121^0-k_121^post5 == 0 /\ -k_121^0 <= 0 /\ -len_54^post5+len_54^0 == 0 /\ -k_83^post5+k_83^0 == 0 /\ -tmp_8^post5+tmp_8^0 == 0 /\ x_7^0-x_7^post5 == 0 /\ -result_4^post5+result_4^0 == 0 /\ -1+len_181^post5 == 0 /\ __cil_tmp5_9^0-__cil_tmp5_9^post5 == 0 /\ -y_11^post5+y_11^0 == 0 /\ -lt_15^1+x_12^post5 == 0 /\ -x_13^post5+x_13^0 == 0), cost: 1
	New rule:
	l1 -> l3 : __cil_tmp5_9^0'=__cil_tmp5_9^0, a_10^0'=a_10^0, a_178^0'=a_178^0, k_121^0'=k_121^0, k_83^0'=k_83^0, len_181^0'=1, len_54^0'=len_54^0, lt_15^0'=lt_15^post5, result_4^0'=result_4^0, tmp_8^0'=tmp_8^0, x_12^0'=lt_15^1, x_13^0'=x_13^0, x_7^0'=x_7^0, y_11^0'=y_11^0, y_14^0'=y_14^0, (0 == 0 /\ 1-y_11^0+x_12^0 <= 0 /\ -k_121^0 <= 0), cost: 1
	
		propagated equality y_14^post5 = y_14^0
		
		propagated equality a_10^post5 = a_10^0
		
		propagated equality a_178^post5 = a_178^0
		
		propagated equality k_121^post5 = k_121^0
		
		propagated equality len_54^post5 = len_54^0
		
		propagated equality k_83^post5 = k_83^0
		
		propagated equality tmp_8^post5 = tmp_8^0
		
		propagated equality x_7^post5 = x_7^0
		
		propagated equality result_4^post5 = result_4^0
		
		propagated equality len_181^post5 = 1
		
		propagated equality __cil_tmp5_9^post5 = __cil_tmp5_9^0
		
		propagated equality y_11^post5 = y_11^0
		
		propagated equality x_12^post5 = lt_15^1
		
		propagated equality x_13^post5 = x_13^0
		
	Simplified Guard

	Original rule:
	l1 -> l3 : __cil_tmp5_9^0'=__cil_tmp5_9^0, a_10^0'=a_10^0, a_178^0'=a_178^0, k_121^0'=k_121^0, k_83^0'=k_83^0, len_181^0'=1, len_54^0'=len_54^0, lt_15^0'=lt_15^post5, result_4^0'=result_4^0, tmp_8^0'=tmp_8^0, x_12^0'=lt_15^1, x_13^0'=x_13^0, x_7^0'=x_7^0, y_11^0'=y_11^0, y_14^0'=y_14^0, (0 == 0 /\ 1-y_11^0+x_12^0 <= 0 /\ -k_121^0 <= 0), cost: 1
	New rule:
	l1 -> l3 : __cil_tmp5_9^0'=__cil_tmp5_9^0, a_10^0'=a_10^0, a_178^0'=a_178^0, k_121^0'=k_121^0, k_83^0'=k_83^0, len_181^0'=1, len_54^0'=len_54^0, lt_15^0'=lt_15^post5, result_4^0'=result_4^0, tmp_8^0'=tmp_8^0, x_12^0'=lt_15^1, x_13^0'=x_13^0, x_7^0'=x_7^0, y_11^0'=y_11^0, y_14^0'=y_14^0, (1-y_11^0+x_12^0 <= 0 /\ -k_121^0 <= 0), cost: 1
	
	Removed Trivial Updates

	Original rule:
	l1 -> l3 : __cil_tmp5_9^0'=__cil_tmp5_9^0, a_10^0'=a_10^0, a_178^0'=a_178^0, k_121^0'=k_121^0, k_83^0'=k_83^0, len_181^0'=1, len_54^0'=len_54^0, lt_15^0'=lt_15^post5, result_4^0'=result_4^0, tmp_8^0'=tmp_8^0, x_12^0'=lt_15^1, x_13^0'=x_13^0, x_7^0'=x_7^0, y_11^0'=y_11^0, y_14^0'=y_14^0, (1-y_11^0+x_12^0 <= 0 /\ -k_121^0 <= 0), cost: 1
	New rule:
	l1 -> l3 : len_181^0'=1, lt_15^0'=lt_15^post5, x_12^0'=lt_15^1, (1-y_11^0+x_12^0 <= 0 /\ -k_121^0 <= 0), cost: 1
	
	made implied equalities explicit

	Original rule:
	l3 -> l4 : __cil_tmp5_9^0'=__cil_tmp5_9^post6, a_10^0'=a_10^post6, a_178^0'=a_178^post6, k_121^0'=k_121^post6, k_83^0'=k_83^post6, len_181^0'=len_181^post6, len_54^0'=len_54^post6, lt_15^0'=lt_15^post6, result_4^0'=result_4^post6, tmp_8^0'=tmp_8^post6, x_12^0'=x_12^post6, x_13^0'=x_13^post6, x_7^0'=x_7^post6, y_11^0'=y_11^post6, y_14^0'=y_14^post6, (0 == 0 /\ -y_11^0+x_12^0 <= 0 /\ x_12^0-x_12^post6 == 0 /\ -len_181^0 <= 0 /\ y_11^0-x_12^0 <= 0 /\ -a_178^post6+a_178^0 == 0 /\ -tmp_8^post6+tmp_8^0 == 0 /\ y_14^0-y_14^post6 == 0 /\ x_7^0-x_7^post6 == 0 /\ y_11^0-y_11^post6 == 0 /\ k_121^0-k_121^post6 == 0 /\ len_181^0-len_181^post6 == 0 /\ -k_83^post6+k_83^0 == 0 /\ -a_10^post6+a_10^0 == 0 /\ -x_13^post6+x_13^0 == 0 /\ __cil_tmp5_9^0-__cil_tmp5_9^post6 == 0 /\ -a_178^0 <= 0 /\ -len_54^post6+len_54^0 == 0 /\ lt_15^0-lt_15^post6 == 0), cost: 1
	New rule:
	l3 -> l4 : __cil_tmp5_9^0'=__cil_tmp5_9^post6, a_10^0'=a_10^post6, a_178^0'=a_178^post6, k_121^0'=k_121^post6, k_83^0'=k_83^post6, len_181^0'=len_181^post6, len_54^0'=len_54^post6, lt_15^0'=lt_15^post6, result_4^0'=result_4^post6, tmp_8^0'=tmp_8^post6, x_12^0'=x_12^post6, x_13^0'=x_13^post6, x_7^0'=x_7^post6, y_11^0'=y_11^post6, y_14^0'=y_14^post6, (0 == 0 /\ -y_11^0+x_12^0 <= 0 /\ -y_11^0+x_12^0 == 0 /\ x_12^0-x_12^post6 == 0 /\ -len_181^0 <= 0 /\ y_11^0-x_12^0 <= 0 /\ -a_178^post6+a_178^0 == 0 /\ -tmp_8^post6+tmp_8^0 == 0 /\ y_14^0-y_14^post6 == 0 /\ x_7^0-x_7^post6 == 0 /\ y_11^0-y_11^post6 == 0 /\ k_121^0-k_121^post6 == 0 /\ len_181^0-len_181^post6 == 0 /\ -k_83^post6+k_83^0 == 0 /\ -a_10^post6+a_10^0 == 0 /\ -x_13^post6+x_13^0 == 0 /\ __cil_tmp5_9^0-__cil_tmp5_9^post6 == 0 /\ -a_178^0 <= 0 /\ -len_54^post6+len_54^0 == 0 /\ lt_15^0-lt_15^post6 == 0), cost: 1
	
	Propagated Equalities

	Original rule:
	l3 -> l4 : __cil_tmp5_9^0'=__cil_tmp5_9^post6, a_10^0'=a_10^post6, a_178^0'=a_178^post6, k_121^0'=k_121^post6, k_83^0'=k_83^post6, len_181^0'=len_181^post6, len_54^0'=len_54^post6, lt_15^0'=lt_15^post6, result_4^0'=result_4^post6, tmp_8^0'=tmp_8^post6, x_12^0'=x_12^post6, x_13^0'=x_13^post6, x_7^0'=x_7^post6, y_11^0'=y_11^post6, y_14^0'=y_14^post6, (0 == 0 /\ -y_11^0+x_12^0 <= 0 /\ -y_11^0+x_12^0 == 0 /\ x_12^0-x_12^post6 == 0 /\ -len_181^0 <= 0 /\ y_11^0-x_12^0 <= 0 /\ -a_178^post6+a_178^0 == 0 /\ -tmp_8^post6+tmp_8^0 == 0 /\ y_14^0-y_14^post6 == 0 /\ x_7^0-x_7^post6 == 0 /\ y_11^0-y_11^post6 == 0 /\ k_121^0-k_121^post6 == 0 /\ len_181^0-len_181^post6 == 0 /\ -k_83^post6+k_83^0 == 0 /\ -a_10^post6+a_10^0 == 0 /\ -x_13^post6+x_13^0 == 0 /\ __cil_tmp5_9^0-__cil_tmp5_9^post6 == 0 /\ -a_178^0 <= 0 /\ -len_54^post6+len_54^0 == 0 /\ lt_15^0-lt_15^post6 == 0), cost: 1
	New rule:
	l3 -> l4 : __cil_tmp5_9^0'=__cil_tmp5_9^0, a_10^0'=a_10^0, a_178^0'=a_178^0, k_121^0'=k_121^0, k_83^0'=k_83^0, len_181^0'=len_181^0, len_54^0'=len_54^0, lt_15^0'=lt_15^0, result_4^0'=result_4^post6, tmp_8^0'=tmp_8^0, x_12^0'=x_12^0, x_13^0'=x_13^0, x_7^0'=x_7^0, y_11^0'=y_11^0, y_14^0'=y_14^0, (0 == 0 /\ -y_11^0+x_12^0 <= 0 /\ -y_11^0+x_12^0 == 0 /\ -len_181^0 <= 0 /\ y_11^0-x_12^0 <= 0 /\ -a_178^0 <= 0), cost: 1
	
		propagated equality x_12^post6 = x_12^0
		
		propagated equality a_178^post6 = a_178^0
		
		propagated equality tmp_8^post6 = tmp_8^0
		
		propagated equality y_14^post6 = y_14^0
		
		propagated equality x_7^post6 = x_7^0
		
		propagated equality y_11^post6 = y_11^0
		
		propagated equality k_121^post6 = k_121^0
		
		propagated equality len_181^post6 = len_181^0
		
		propagated equality k_83^post6 = k_83^0
		
		propagated equality a_10^post6 = a_10^0
		
		propagated equality x_13^post6 = x_13^0
		
		propagated equality __cil_tmp5_9^post6 = __cil_tmp5_9^0
		
		propagated equality len_54^post6 = len_54^0
		
		propagated equality lt_15^post6 = lt_15^0
		
	Simplified Guard

	Original rule:
	l3 -> l4 : __cil_tmp5_9^0'=__cil_tmp5_9^0, a_10^0'=a_10^0, a_178^0'=a_178^0, k_121^0'=k_121^0, k_83^0'=k_83^0, len_181^0'=len_181^0, len_54^0'=len_54^0, lt_15^0'=lt_15^0, result_4^0'=result_4^post6, tmp_8^0'=tmp_8^0, x_12^0'=x_12^0, x_13^0'=x_13^0, x_7^0'=x_7^0, y_11^0'=y_11^0, y_14^0'=y_14^0, (0 == 0 /\ -y_11^0+x_12^0 <= 0 /\ -y_11^0+x_12^0 == 0 /\ -len_181^0 <= 0 /\ y_11^0-x_12^0 <= 0 /\ -a_178^0 <= 0), cost: 1
	New rule:
	l3 -> l4 : __cil_tmp5_9^0'=__cil_tmp5_9^0, a_10^0'=a_10^0, a_178^0'=a_178^0, k_121^0'=k_121^0, k_83^0'=k_83^0, len_181^0'=len_181^0, len_54^0'=len_54^0, lt_15^0'=lt_15^0, result_4^0'=result_4^post6, tmp_8^0'=tmp_8^0, x_12^0'=x_12^0, x_13^0'=x_13^0, x_7^0'=x_7^0, y_11^0'=y_11^0, y_14^0'=y_14^0, (-y_11^0+x_12^0 <= 0 /\ -y_11^0+x_12^0 == 0 /\ -len_181^0 <= 0 /\ y_11^0-x_12^0 <= 0 /\ -a_178^0 <= 0), cost: 1
	
	made implied equalities explicit

	Original rule:
	l3 -> l4 : __cil_tmp5_9^0'=__cil_tmp5_9^0, a_10^0'=a_10^0, a_178^0'=a_178^0, k_121^0'=k_121^0, k_83^0'=k_83^0, len_181^0'=len_181^0, len_54^0'=len_54^0, lt_15^0'=lt_15^0, result_4^0'=result_4^post6, tmp_8^0'=tmp_8^0, x_12^0'=x_12^0, x_13^0'=x_13^0, x_7^0'=x_7^0, y_11^0'=y_11^0, y_14^0'=y_14^0, (-y_11^0+x_12^0 <= 0 /\ -y_11^0+x_12^0 == 0 /\ -len_181^0 <= 0 /\ y_11^0-x_12^0 <= 0 /\ -a_178^0 <= 0), cost: 1
	New rule:
	l3 -> l4 : __cil_tmp5_9^0'=__cil_tmp5_9^0, a_10^0'=a_10^0, a_178^0'=a_178^0, k_121^0'=k_121^0, k_83^0'=k_83^0, len_181^0'=len_181^0, len_54^0'=len_54^0, lt_15^0'=lt_15^0, result_4^0'=result_4^post6, tmp_8^0'=tmp_8^0, x_12^0'=x_12^0, x_13^0'=x_13^0, x_7^0'=x_7^0, y_11^0'=y_11^0, y_14^0'=y_14^0, (-y_11^0+x_12^0 <= 0 /\ -y_11^0+x_12^0 == 0 /\ -len_181^0 <= 0 /\ y_11^0-x_12^0 <= 0 /\ -a_178^0 <= 0), cost: 1
	
	Removed Trivial Updates

	Original rule:
	l3 -> l4 : __cil_tmp5_9^0'=__cil_tmp5_9^0, a_10^0'=a_10^0, a_178^0'=a_178^0, k_121^0'=k_121^0, k_83^0'=k_83^0, len_181^0'=len_181^0, len_54^0'=len_54^0, lt_15^0'=lt_15^0, result_4^0'=result_4^post6, tmp_8^0'=tmp_8^0, x_12^0'=x_12^0, x_13^0'=x_13^0, x_7^0'=x_7^0, y_11^0'=y_11^0, y_14^0'=y_14^0, (-y_11^0+x_12^0 <= 0 /\ -y_11^0+x_12^0 == 0 /\ -len_181^0 <= 0 /\ y_11^0-x_12^0 <= 0 /\ -a_178^0 <= 0), cost: 1
	New rule:
	l3 -> l4 : result_4^0'=result_4^post6, (-y_11^0+x_12^0 <= 0 /\ -y_11^0+x_12^0 == 0 /\ -len_181^0 <= 0 /\ y_11^0-x_12^0 <= 0 /\ -a_178^0 <= 0), cost: 1
	
	Propagated Equalities

	Original rule:
	l7 -> l0 : __cil_tmp5_9^0'=__cil_tmp5_9^post3, a_10^0'=a_10^post3, a_178^0'=a_178^post3, k_121^0'=k_121^post3, k_83^0'=k_83^post3, len_181^0'=len_181^post3, len_54^0'=len_54^post3, lt_15^0'=lt_15^post3, result_4^0'=result_4^post3, tmp_8^0'=tmp_8^post3, x_12^0'=x_12^post3, x_13^0'=x_13^post3, x_7^0'=x_7^post3, y_11^0'=y_11^post3, y_14^0'=y_14^post3, (0 == 0 /\ -x_12^post3+x_12^post11 == 0 /\ -tmp_8^1+x_7^1 == 0 /\ -a_10^post3+a_10^post11 == 0 /\ x_13^post3-result_4^7 == 0 /\ result_4^3-__cil_tmp5_9^2 == 0 /\ -y_11^post11+y_11^0 == 0 /\ x_7^0-x_7^post11 == 0 /\ -len_54^post3 <= 0 /\ a_10^0-a_10^post11 == 0 /\ -x_7^3+__cil_tmp5_9^3 == 0 /\ -tmp_8^2+x_7^2 == 0 /\ result_4^5-__cil_tmp5_9^3 == 0 /\ -len_181^post11+len_181^0 == 0 /\ y_14^0-y_14^post11 == 0 /\ -k_121^post3+k_121^post11 == 0 /\ k_83^0-k_83^post11 == 0 /\ lt_15^0-lt_15^post11 == 0 /\ y_14^post3 == 0 /\ -1-len_54^post3+k_83^post3 == 0 /\ result_4^1-__cil_tmp5_9^1 == 0 /\ -tmp_8^post11+tmp_8^0 == 0 /\ -y_11^post3+y_11^post11 == 0 /\ -k_121^post11+k_121^0 == 0 /\ -__cil_tmp5_9^post11+__cil_tmp5_9^0 == 0 /\ a_178^post11-a_178^post3 == 0 /\ -x_7^2+__cil_tmp5_9^2 == 0 /\ -result_4^5+x_13^4 == 0 /\ len_181^post11-len_181^post3 == 0 /\ -result_4^3+x_13^3 == 0 /\ x_7^3-tmp_8^3 == 0 /\ -x_7^1+__cil_tmp5_9^1 == 0 /\ -tmp_8^post3+x_7^post3 == 0 /\ -2+len_54^post3 == 0 /\ -len_54^post11+len_54^0 == 0 /\ -__cil_tmp5_9^post3+result_4^7 == 0 /\ x_13^0-x_13^post11 == 0 /\ __cil_tmp5_9^post3-x_7^post3 == 0 /\ -x_12^post11+x_12^0 == 0 /\ -a_178^post11+a_178^0 == 0 /\ -result_4^1+x_13^2 == 0 /\ -k_83^post3 <= 0 /\ x_13^1 == 0 /\ -result_4^post11+result_4^0 == 0 /\ -k_121^post11 <= 0 /\ -lt_15^post3+lt_15^post11 == 0), cost: 1
	New rule:
	l7 -> l0 : __cil_tmp5_9^0'=result_4^7, a_10^0'=a_10^post11, a_178^0'=a_178^post11, k_121^0'=k_121^post11, k_83^0'=3, len_181^0'=len_181^post11, len_54^0'=2, lt_15^0'=lt_15^post11, result_4^0'=result_4^post3, tmp_8^0'=result_4^7, x_12^0'=x_12^post11, x_13^0'=result_4^7, x_7^0'=result_4^7, y_11^0'=y_11^post11, y_14^0'=0, (0 == 0 /\ -3 <= 0 /\ -tmp_8^1+x_7^1 == 0 /\ result_4^3-__cil_tmp5_9^2 == 0 /\ -2 <= 0 /\ -y_11^post11+y_11^0 == 0 /\ x_7^0-x_7^post11 == 0 /\ a_10^0-a_10^post11 == 0 /\ -x_7^3+__cil_tmp5_9^3 == 0 /\ -tmp_8^2+x_7^2 == 0 /\ result_4^5-__cil_tmp5_9^3 == 0 /\ -len_181^post11+len_181^0 == 0 /\ y_14^0-y_14^post11 == 0 /\ k_83^0-k_83^post11 == 0 /\ lt_15^0-lt_15^post11 == 0 /\ result_4^1-__cil_tmp5_9^1 == 0 /\ -tmp_8^post11+tmp_8^0 == 0 /\ -k_121^post11+k_121^0 == 0 /\ -__cil_tmp5_9^post11+__cil_tmp5_9^0 == 0 /\ -x_7^2+__cil_tmp5_9^2 == 0 /\ -result_4^5+x_13^4 == 0 /\ -result_4^3+x_13^3 == 0 /\ x_7^3-tmp_8^3 == 0 /\ -x_7^1+__cil_tmp5_9^1 == 0 /\ -len_54^post11+len_54^0 == 0 /\ x_13^0-x_13^post11 == 0 /\ -x_12^post11+x_12^0 == 0 /\ -a_178^post11+a_178^0 == 0 /\ -result_4^1+x_13^2 == 0 /\ x_13^1 == 0 /\ -result_4^post11+result_4^0 == 0 /\ -k_121^post11 <= 0), cost: 1
	
		propagated equality x_12^post3 = x_12^post11
		
		propagated equality a_10^post3 = a_10^post11
		
		propagated equality x_13^post3 = result_4^7
		
		propagated equality k_121^post3 = k_121^post11
		
		propagated equality y_14^post3 = 0
		
		propagated equality k_83^post3 = 1+len_54^post3
		
		propagated equality y_11^post3 = y_11^post11
		
		propagated equality a_178^post3 = a_178^post11
		
		propagated equality len_181^post3 = len_181^post11
		
		propagated equality tmp_8^post3 = x_7^post3
		
		propagated equality len_54^post3 = 2
		
		propagated equality __cil_tmp5_9^post3 = result_4^7
		
		propagated equality x_7^post3 = result_4^7
		
		propagated equality lt_15^post3 = lt_15^post11
		
	Propagated Equalities

	Original rule:
	l7 -> l0 : __cil_tmp5_9^0'=result_4^7, a_10^0'=a_10^post11, a_178^0'=a_178^post11, k_121^0'=k_121^post11, k_83^0'=3, len_181^0'=len_181^post11, len_54^0'=2, lt_15^0'=lt_15^post11, result_4^0'=result_4^post3, tmp_8^0'=result_4^7, x_12^0'=x_12^post11, x_13^0'=result_4^7, x_7^0'=result_4^7, y_11^0'=y_11^post11, y_14^0'=0, (0 == 0 /\ -3 <= 0 /\ -tmp_8^1+x_7^1 == 0 /\ result_4^3-__cil_tmp5_9^2 == 0 /\ -2 <= 0 /\ -y_11^post11+y_11^0 == 0 /\ x_7^0-x_7^post11 == 0 /\ a_10^0-a_10^post11 == 0 /\ -x_7^3+__cil_tmp5_9^3 == 0 /\ -tmp_8^2+x_7^2 == 0 /\ result_4^5-__cil_tmp5_9^3 == 0 /\ -len_181^post11+len_181^0 == 0 /\ y_14^0-y_14^post11 == 0 /\ k_83^0-k_83^post11 == 0 /\ lt_15^0-lt_15^post11 == 0 /\ result_4^1-__cil_tmp5_9^1 == 0 /\ -tmp_8^post11+tmp_8^0 == 0 /\ -k_121^post11+k_121^0 == 0 /\ -__cil_tmp5_9^post11+__cil_tmp5_9^0 == 0 /\ -x_7^2+__cil_tmp5_9^2 == 0 /\ -result_4^5+x_13^4 == 0 /\ -result_4^3+x_13^3 == 0 /\ x_7^3-tmp_8^3 == 0 /\ -x_7^1+__cil_tmp5_9^1 == 0 /\ -len_54^post11+len_54^0 == 0 /\ x_13^0-x_13^post11 == 0 /\ -x_12^post11+x_12^0 == 0 /\ -a_178^post11+a_178^0 == 0 /\ -result_4^1+x_13^2 == 0 /\ x_13^1 == 0 /\ -result_4^post11+result_4^0 == 0 /\ -k_121^post11 <= 0), cost: 1
	New rule:
	l7 -> l0 : __cil_tmp5_9^0'=result_4^7, a_10^0'=a_10^0, a_178^0'=a_178^0, k_121^0'=k_121^0, k_83^0'=3, len_181^0'=len_181^0, len_54^0'=2, lt_15^0'=lt_15^0, result_4^0'=result_4^post3, tmp_8^0'=result_4^7, x_12^0'=x_12^0, x_13^0'=result_4^7, x_7^0'=result_4^7, y_11^0'=y_11^0, y_14^0'=0, (0 == 0 /\ -3 <= 0 /\ -2 <= 0 /\ -k_121^0 <= 0), cost: 1
	
		propagated equality tmp_8^1 = x_7^1
		
		propagated equality __cil_tmp5_9^2 = result_4^3
		
		propagated equality y_11^post11 = y_11^0
		
		propagated equality x_7^post11 = x_7^0
		
		propagated equality a_10^post11 = a_10^0
		
		propagated equality __cil_tmp5_9^3 = x_7^3
		
		propagated equality tmp_8^2 = x_7^2
		
		propagated equality result_4^5 = x_7^3
		
		propagated equality len_181^post11 = len_181^0
		
		propagated equality y_14^post11 = y_14^0
		
		propagated equality k_83^post11 = k_83^0
		
		propagated equality lt_15^post11 = lt_15^0
		
		propagated equality __cil_tmp5_9^1 = result_4^1
		
		propagated equality tmp_8^post11 = tmp_8^0
		
		propagated equality k_121^post11 = k_121^0
		
		propagated equality __cil_tmp5_9^post11 = __cil_tmp5_9^0
		
		propagated equality result_4^3 = x_7^2
		
		propagated equality x_13^4 = x_7^3
		
		propagated equality x_13^3 = x_7^2
		
		propagated equality tmp_8^3 = x_7^3
		
		propagated equality result_4^1 = x_7^1
		
		propagated equality len_54^post11 = len_54^0
		
		propagated equality x_13^post11 = x_13^0
		
		propagated equality x_12^post11 = x_12^0
		
		propagated equality a_178^post11 = a_178^0
		
		propagated equality x_13^2 = x_7^1
		
		propagated equality x_13^1 = 0
		
		propagated equality result_4^post11 = result_4^0
		
	Simplified Guard

	Original rule:
	l7 -> l0 : __cil_tmp5_9^0'=result_4^7, a_10^0'=a_10^0, a_178^0'=a_178^0, k_121^0'=k_121^0, k_83^0'=3, len_181^0'=len_181^0, len_54^0'=2, lt_15^0'=lt_15^0, result_4^0'=result_4^post3, tmp_8^0'=result_4^7, x_12^0'=x_12^0, x_13^0'=result_4^7, x_7^0'=result_4^7, y_11^0'=y_11^0, y_14^0'=0, (0 == 0 /\ -3 <= 0 /\ -2 <= 0 /\ -k_121^0 <= 0), cost: 1
	New rule:
	l7 -> l0 : __cil_tmp5_9^0'=result_4^7, a_10^0'=a_10^0, a_178^0'=a_178^0, k_121^0'=k_121^0, k_83^0'=3, len_181^0'=len_181^0, len_54^0'=2, lt_15^0'=lt_15^0, result_4^0'=result_4^post3, tmp_8^0'=result_4^7, x_12^0'=x_12^0, x_13^0'=result_4^7, x_7^0'=result_4^7, y_11^0'=y_11^0, y_14^0'=0, -k_121^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l7 -> l0 : __cil_tmp5_9^0'=result_4^7, a_10^0'=a_10^0, a_178^0'=a_178^0, k_121^0'=k_121^0, k_83^0'=3, len_181^0'=len_181^0, len_54^0'=2, lt_15^0'=lt_15^0, result_4^0'=result_4^post3, tmp_8^0'=result_4^7, x_12^0'=x_12^0, x_13^0'=result_4^7, x_7^0'=result_4^7, y_11^0'=y_11^0, y_14^0'=0, -k_121^0 <= 0, cost: 1
	New rule:
	l7 -> l0 : __cil_tmp5_9^0'=result_4^7, k_83^0'=3, len_54^0'=2, result_4^0'=result_4^post3, tmp_8^0'=result_4^7, x_13^0'=result_4^7, x_7^0'=result_4^7, y_14^0'=0, -k_121^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l3 -> l3 : __cil_tmp5_9^0'=__cil_tmp5_9^post8, a_10^0'=a_10^post8, a_178^0'=a_178^post8, k_121^0'=k_121^post8, k_83^0'=k_83^post8, len_181^0'=len_181^post8, len_54^0'=len_54^post8, lt_15^0'=lt_15^post8, result_4^0'=result_4^post8, tmp_8^0'=tmp_8^post8, x_12^0'=x_12^post8, x_13^0'=x_13^post8, x_7^0'=x_7^post8, y_11^0'=y_11^post8, y_14^0'=y_14^post8, (0 == 0 /\ -a_10^post8+a_10^post7 == 0 /\ len_54^post7-len_54^post8 == 0 /\ y_14^0-y_14^post7 == 0 /\ -x_13^post8+x_13^post7 == 0 /\ x_7^0-x_7^post7 == 0 /\ -len_181^0 <= 0 /\ len_181^post7-len_181^post8 == 0 /\ 1+y_11^0-x_12^0 <= 0 /\ -y_11^post7+y_11^0 == 0 /\ __cil_tmp5_9^0-__cil_tmp5_9^post7 == 0 /\ -y_11^post8+y_11^post7 == 0 /\ x_12^post7-lt_15^1 == 0 /\ result_4^post7-result_4^post8 == 0 /\ -__cil_tmp5_9^post8+__cil_tmp5_9^post7 == 0 /\ -a_178^post7+a_178^0 == 0 /\ k_83^0-k_83^post7 == 0 /\ -y_14^post8+y_14^post7 == 0 /\ tmp_8^post7-tmp_8^post8 == 0 /\ -tmp_8^post7+tmp_8^0 == 0 /\ -k_121^post7+k_121^0 == 0 /\ a_178^post7-a_178^post8 == 0 /\ -lt_15^post8+lt_15^post7 == 0 /\ -x_12^post8+x_12^post7 == 0 /\ -k_121^post8+k_121^post7 == 0 /\ x_13^0-x_13^post7 == 0 /\ -1+len_181^post7-len_181^0 == 0 /\ -result_4^post7+result_4^0 == 0 /\ -a_178^0 <= 0 /\ -len_54^post7+len_54^0 == 0 /\ -k_83^post8+k_83^post7 == 0 /\ a_10^0-a_10^post7 == 0 /\ x_7^post7-x_7^post8 == 0), cost: 1
	New rule:
	l3 -> l3 : __cil_tmp5_9^0'=__cil_tmp5_9^post7, a_10^0'=a_10^post7, a_178^0'=a_178^post7, k_121^0'=k_121^post7, k_83^0'=k_83^post7, len_181^0'=len_181^post7, len_54^0'=len_54^post7, lt_15^0'=lt_15^post7, result_4^0'=result_4^post7, tmp_8^0'=tmp_8^post7, x_12^0'=x_12^post7, x_13^0'=x_13^post7, x_7^0'=x_7^post7, y_11^0'=y_11^post7, y_14^0'=y_14^post7, (0 == 0 /\ y_14^0-y_14^post7 == 0 /\ x_7^0-x_7^post7 == 0 /\ -len_181^0 <= 0 /\ 1+y_11^0-x_12^0 <= 0 /\ -y_11^post7+y_11^0 == 0 /\ __cil_tmp5_9^0-__cil_tmp5_9^post7 == 0 /\ x_12^post7-lt_15^1 == 0 /\ -a_178^post7+a_178^0 == 0 /\ k_83^0-k_83^post7 == 0 /\ -tmp_8^post7+tmp_8^0 == 0 /\ -k_121^post7+k_121^0 == 0 /\ x_13^0-x_13^post7 == 0 /\ -1+len_181^post7-len_181^0 == 0 /\ -result_4^post7+result_4^0 == 0 /\ -a_178^0 <= 0 /\ -len_54^post7+len_54^0 == 0 /\ a_10^0-a_10^post7 == 0), cost: 1
	
		propagated equality a_10^post8 = a_10^post7
		
		propagated equality len_54^post8 = len_54^post7
		
		propagated equality x_13^post8 = x_13^post7
		
		propagated equality len_181^post8 = len_181^post7
		
		propagated equality y_11^post8 = y_11^post7
		
		propagated equality result_4^post8 = result_4^post7
		
		propagated equality __cil_tmp5_9^post8 = __cil_tmp5_9^post7
		
		propagated equality y_14^post8 = y_14^post7
		
		propagated equality tmp_8^post8 = tmp_8^post7
		
		propagated equality a_178^post8 = a_178^post7
		
		propagated equality lt_15^post8 = lt_15^post7
		
		propagated equality x_12^post8 = x_12^post7
		
		propagated equality k_121^post8 = k_121^post7
		
		propagated equality k_83^post8 = k_83^post7
		
		propagated equality x_7^post8 = x_7^post7
		
	Propagated Equalities

	Original rule:
	l3 -> l3 : __cil_tmp5_9^0'=__cil_tmp5_9^post7, a_10^0'=a_10^post7, a_178^0'=a_178^post7, k_121^0'=k_121^post7, k_83^0'=k_83^post7, len_181^0'=len_181^post7, len_54^0'=len_54^post7, lt_15^0'=lt_15^post7, result_4^0'=result_4^post7, tmp_8^0'=tmp_8^post7, x_12^0'=x_12^post7, x_13^0'=x_13^post7, x_7^0'=x_7^post7, y_11^0'=y_11^post7, y_14^0'=y_14^post7, (0 == 0 /\ y_14^0-y_14^post7 == 0 /\ x_7^0-x_7^post7 == 0 /\ -len_181^0 <= 0 /\ 1+y_11^0-x_12^0 <= 0 /\ -y_11^post7+y_11^0 == 0 /\ __cil_tmp5_9^0-__cil_tmp5_9^post7 == 0 /\ x_12^post7-lt_15^1 == 0 /\ -a_178^post7+a_178^0 == 0 /\ k_83^0-k_83^post7 == 0 /\ -tmp_8^post7+tmp_8^0 == 0 /\ -k_121^post7+k_121^0 == 0 /\ x_13^0-x_13^post7 == 0 /\ -1+len_181^post7-len_181^0 == 0 /\ -result_4^post7+result_4^0 == 0 /\ -a_178^0 <= 0 /\ -len_54^post7+len_54^0 == 0 /\ a_10^0-a_10^post7 == 0), cost: 1
	New rule:
	l3 -> l3 : __cil_tmp5_9^0'=__cil_tmp5_9^0, a_10^0'=a_10^0, a_178^0'=a_178^0, k_121^0'=k_121^0, k_83^0'=k_83^0, len_181^0'=1+len_181^0, len_54^0'=len_54^0, lt_15^0'=lt_15^post7, result_4^0'=result_4^0, tmp_8^0'=tmp_8^0, x_12^0'=x_12^post7, x_13^0'=x_13^0, x_7^0'=x_7^0, y_11^0'=y_11^0, y_14^0'=y_14^0, (0 == 0 /\ -len_181^0 <= 0 /\ 1+y_11^0-x_12^0 <= 0 /\ -a_178^0 <= 0), cost: 1
	
		propagated equality y_14^post7 = y_14^0
		
		propagated equality x_7^post7 = x_7^0
		
		propagated equality y_11^post7 = y_11^0
		
		propagated equality __cil_tmp5_9^post7 = __cil_tmp5_9^0
		
		propagated equality lt_15^1 = x_12^post7
		
		propagated equality a_178^post7 = a_178^0
		
		propagated equality k_83^post7 = k_83^0
		
		propagated equality tmp_8^post7 = tmp_8^0
		
		propagated equality k_121^post7 = k_121^0
		
		propagated equality x_13^post7 = x_13^0
		
		propagated equality len_181^post7 = 1+len_181^0
		
		propagated equality result_4^post7 = result_4^0
		
		propagated equality len_54^post7 = len_54^0
		
		propagated equality a_10^post7 = a_10^0
		
	Simplified Guard

	Original rule:
	l3 -> l3 : __cil_tmp5_9^0'=__cil_tmp5_9^0, a_10^0'=a_10^0, a_178^0'=a_178^0, k_121^0'=k_121^0, k_83^0'=k_83^0, len_181^0'=1+len_181^0, len_54^0'=len_54^0, lt_15^0'=lt_15^post7, result_4^0'=result_4^0, tmp_8^0'=tmp_8^0, x_12^0'=x_12^post7, x_13^0'=x_13^0, x_7^0'=x_7^0, y_11^0'=y_11^0, y_14^0'=y_14^0, (0 == 0 /\ -len_181^0 <= 0 /\ 1+y_11^0-x_12^0 <= 0 /\ -a_178^0 <= 0), cost: 1
	New rule:
	l3 -> l3 : __cil_tmp5_9^0'=__cil_tmp5_9^0, a_10^0'=a_10^0, a_178^0'=a_178^0, k_121^0'=k_121^0, k_83^0'=k_83^0, len_181^0'=1+len_181^0, len_54^0'=len_54^0, lt_15^0'=lt_15^post7, result_4^0'=result_4^0, tmp_8^0'=tmp_8^0, x_12^0'=x_12^post7, x_13^0'=x_13^0, x_7^0'=x_7^0, y_11^0'=y_11^0, y_14^0'=y_14^0, (-len_181^0 <= 0 /\ 1+y_11^0-x_12^0 <= 0 /\ -a_178^0 <= 0), cost: 1
	
	Removed Trivial Updates

	Original rule:
	l3 -> l3 : __cil_tmp5_9^0'=__cil_tmp5_9^0, a_10^0'=a_10^0, a_178^0'=a_178^0, k_121^0'=k_121^0, k_83^0'=k_83^0, len_181^0'=1+len_181^0, len_54^0'=len_54^0, lt_15^0'=lt_15^post7, result_4^0'=result_4^0, tmp_8^0'=tmp_8^0, x_12^0'=x_12^post7, x_13^0'=x_13^0, x_7^0'=x_7^0, y_11^0'=y_11^0, y_14^0'=y_14^0, (-len_181^0 <= 0 /\ 1+y_11^0-x_12^0 <= 0 /\ -a_178^0 <= 0), cost: 1
	New rule:
	l3 -> l3 : len_181^0'=1+len_181^0, lt_15^0'=lt_15^post7, x_12^0'=x_12^post7, (-len_181^0 <= 0 /\ 1+y_11^0-x_12^0 <= 0 /\ -a_178^0 <= 0), cost: 1
	
	Propagated Equalities

	Original rule:
	l3 -> l3 : __cil_tmp5_9^0'=__cil_tmp5_9^post10, a_10^0'=a_10^post10, a_178^0'=a_178^post10, k_121^0'=k_121^post10, k_83^0'=k_83^post10, len_181^0'=len_181^post10, len_54^0'=len_54^post10, lt_15^0'=lt_15^post10, result_4^0'=result_4^post10, tmp_8^0'=tmp_8^post10, x_12^0'=x_12^post10, x_13^0'=x_13^post10, x_7^0'=x_7^post10, y_11^0'=y_11^post10, y_14^0'=y_14^post10, (0 == 0 /\ -a_178^post9+a_178^0 == 0 /\ -lt_15^post10+lt_15^post9 == 0 /\ 1-y_11^0+x_12^0 <= 0 /\ __cil_tmp5_9^0-__cil_tmp5_9^post9 == 0 /\ -y_14^post10+y_14^post9 == 0 /\ -1-len_181^0+len_181^post9 == 0 /\ -k_83^post10+k_83^post9 == 0 /\ -x_7^post10+x_7^post9 == 0 /\ -a_10^post9+a_10^0 == 0 /\ -len_181^0 <= 0 /\ -k_121^post10+k_121^post9 == 0 /\ k_121^0-k_121^post9 == 0 /\ -tmp_8^post10+tmp_8^post9 == 0 /\ -a_178^post10+a_178^post9 == 0 /\ a_10^post9-a_10^post10 == 0 /\ -x_12^post10+x_12^post9 == 0 /\ -x_13^post10+x_13^post9 == 0 /\ -__cil_tmp5_9^post10+__cil_tmp5_9^post9 == 0 /\ -tmp_8^post9+tmp_8^0 == 0 /\ y_14^0-y_14^post9 == 0 /\ y_11^0-y_11^post9 == 0 /\ -result_4^post10+result_4^post9 == 0 /\ -y_11^post10+y_11^post9 == 0 /\ x_7^0-x_7^post9 == 0 /\ -result_4^post9+result_4^0 == 0 /\ -len_181^post10+len_181^post9 == 0 /\ -lt_15^1+x_12^post9 == 0 /\ -k_83^post9+k_83^0 == 0 /\ -len_54^post10+len_54^post9 == 0 /\ -len_54^post9+len_54^0 == 0 /\ -x_13^post9+x_13^0 == 0 /\ -a_178^0 <= 0), cost: 1
	New rule:
	l3 -> l3 : __cil_tmp5_9^0'=__cil_tmp5_9^post9, a_10^0'=a_10^post9, a_178^0'=a_178^post9, k_121^0'=k_121^post9, k_83^0'=k_83^post9, len_181^0'=len_181^post9, len_54^0'=len_54^post9, lt_15^0'=lt_15^post9, result_4^0'=result_4^post9, tmp_8^0'=tmp_8^post9, x_12^0'=x_12^post9, x_13^0'=x_13^post9, x_7^0'=x_7^post9, y_11^0'=y_11^post9, y_14^0'=y_14^post9, (0 == 0 /\ -a_178^post9+a_178^0 == 0 /\ 1-y_11^0+x_12^0 <= 0 /\ __cil_tmp5_9^0-__cil_tmp5_9^post9 == 0 /\ -1-len_181^0+len_181^post9 == 0 /\ -a_10^post9+a_10^0 == 0 /\ -len_181^0 <= 0 /\ k_121^0-k_121^post9 == 0 /\ -tmp_8^post9+tmp_8^0 == 0 /\ y_14^0-y_14^post9 == 0 /\ y_11^0-y_11^post9 == 0 /\ x_7^0-x_7^post9 == 0 /\ -result_4^post9+result_4^0 == 0 /\ -lt_15^1+x_12^post9 == 0 /\ -k_83^post9+k_83^0 == 0 /\ -len_54^post9+len_54^0 == 0 /\ -x_13^post9+x_13^0 == 0 /\ -a_178^0 <= 0), cost: 1
	
		propagated equality lt_15^post10 = lt_15^post9
		
		propagated equality y_14^post10 = y_14^post9
		
		propagated equality k_83^post10 = k_83^post9
		
		propagated equality x_7^post10 = x_7^post9
		
		propagated equality k_121^post10 = k_121^post9
		
		propagated equality tmp_8^post10 = tmp_8^post9
		
		propagated equality a_178^post10 = a_178^post9
		
		propagated equality a_10^post10 = a_10^post9
		
		propagated equality x_12^post10 = x_12^post9
		
		propagated equality x_13^post10 = x_13^post9
		
		propagated equality __cil_tmp5_9^post10 = __cil_tmp5_9^post9
		
		propagated equality result_4^post10 = result_4^post9
		
		propagated equality y_11^post10 = y_11^post9
		
		propagated equality len_181^post10 = len_181^post9
		
		propagated equality len_54^post10 = len_54^post9
		
	Propagated Equalities

	Original rule:
	l3 -> l3 : __cil_tmp5_9^0'=__cil_tmp5_9^post9, a_10^0'=a_10^post9, a_178^0'=a_178^post9, k_121^0'=k_121^post9, k_83^0'=k_83^post9, len_181^0'=len_181^post9, len_54^0'=len_54^post9, lt_15^0'=lt_15^post9, result_4^0'=result_4^post9, tmp_8^0'=tmp_8^post9, x_12^0'=x_12^post9, x_13^0'=x_13^post9, x_7^0'=x_7^post9, y_11^0'=y_11^post9, y_14^0'=y_14^post9, (0 == 0 /\ -a_178^post9+a_178^0 == 0 /\ 1-y_11^0+x_12^0 <= 0 /\ __cil_tmp5_9^0-__cil_tmp5_9^post9 == 0 /\ -1-len_181^0+len_181^post9 == 0 /\ -a_10^post9+a_10^0 == 0 /\ -len_181^0 <= 0 /\ k_121^0-k_121^post9 == 0 /\ -tmp_8^post9+tmp_8^0 == 0 /\ y_14^0-y_14^post9 == 0 /\ y_11^0-y_11^post9 == 0 /\ x_7^0-x_7^post9 == 0 /\ -result_4^post9+result_4^0 == 0 /\ -lt_15^1+x_12^post9 == 0 /\ -k_83^post9+k_83^0 == 0 /\ -len_54^post9+len_54^0 == 0 /\ -x_13^post9+x_13^0 == 0 /\ -a_178^0 <= 0), cost: 1
	New rule:
	l3 -> l3 : __cil_tmp5_9^0'=__cil_tmp5_9^0, a_10^0'=a_10^0, a_178^0'=a_178^0, k_121^0'=k_121^0, k_83^0'=k_83^0, len_181^0'=1+len_181^0, len_54^0'=len_54^0, lt_15^0'=lt_15^post9, result_4^0'=result_4^0, tmp_8^0'=tmp_8^0, x_12^0'=x_12^post9, x_13^0'=x_13^0, x_7^0'=x_7^0, y_11^0'=y_11^0, y_14^0'=y_14^0, (0 == 0 /\ 1-y_11^0+x_12^0 <= 0 /\ -len_181^0 <= 0 /\ -a_178^0 <= 0), cost: 1
	
		propagated equality a_178^post9 = a_178^0
		
		propagated equality __cil_tmp5_9^post9 = __cil_tmp5_9^0
		
		propagated equality len_181^post9 = 1+len_181^0
		
		propagated equality a_10^post9 = a_10^0
		
		propagated equality k_121^post9 = k_121^0
		
		propagated equality tmp_8^post9 = tmp_8^0
		
		propagated equality y_14^post9 = y_14^0
		
		propagated equality y_11^post9 = y_11^0
		
		propagated equality x_7^post9 = x_7^0
		
		propagated equality result_4^post9 = result_4^0
		
		propagated equality lt_15^1 = x_12^post9
		
		propagated equality k_83^post9 = k_83^0
		
		propagated equality len_54^post9 = len_54^0
		
		propagated equality x_13^post9 = x_13^0
		
	Simplified Guard

	Original rule:
	l3 -> l3 : __cil_tmp5_9^0'=__cil_tmp5_9^0, a_10^0'=a_10^0, a_178^0'=a_178^0, k_121^0'=k_121^0, k_83^0'=k_83^0, len_181^0'=1+len_181^0, len_54^0'=len_54^0, lt_15^0'=lt_15^post9, result_4^0'=result_4^0, tmp_8^0'=tmp_8^0, x_12^0'=x_12^post9, x_13^0'=x_13^0, x_7^0'=x_7^0, y_11^0'=y_11^0, y_14^0'=y_14^0, (0 == 0 /\ 1-y_11^0+x_12^0 <= 0 /\ -len_181^0 <= 0 /\ -a_178^0 <= 0), cost: 1
	New rule:
	l3 -> l3 : __cil_tmp5_9^0'=__cil_tmp5_9^0, a_10^0'=a_10^0, a_178^0'=a_178^0, k_121^0'=k_121^0, k_83^0'=k_83^0, len_181^0'=1+len_181^0, len_54^0'=len_54^0, lt_15^0'=lt_15^post9, result_4^0'=result_4^0, tmp_8^0'=tmp_8^0, x_12^0'=x_12^post9, x_13^0'=x_13^0, x_7^0'=x_7^0, y_11^0'=y_11^0, y_14^0'=y_14^0, (1-y_11^0+x_12^0 <= 0 /\ -len_181^0 <= 0 /\ -a_178^0 <= 0), cost: 1
	
	Removed Trivial Updates

	Original rule:
	l3 -> l3 : __cil_tmp5_9^0'=__cil_tmp5_9^0, a_10^0'=a_10^0, a_178^0'=a_178^0, k_121^0'=k_121^0, k_83^0'=k_83^0, len_181^0'=1+len_181^0, len_54^0'=len_54^0, lt_15^0'=lt_15^post9, result_4^0'=result_4^0, tmp_8^0'=tmp_8^0, x_12^0'=x_12^post9, x_13^0'=x_13^0, x_7^0'=x_7^0, y_11^0'=y_11^0, y_14^0'=y_14^0, (1-y_11^0+x_12^0 <= 0 /\ -len_181^0 <= 0 /\ -a_178^0 <= 0), cost: 1
	New rule:
	l3 -> l3 : len_181^0'=1+len_181^0, lt_15^0'=lt_15^post9, x_12^0'=x_12^post9, (1-y_11^0+x_12^0 <= 0 /\ -len_181^0 <= 0 /\ -a_178^0 <= 0), cost: 1

Step with 19

	Trace

	19[(-k_121^0 <= 0)]
	
	Blocked

	[{}, {}]

Step with 14

	Trace

	19[(-k_121^0 <= 0)], 14[(1-a_10^0+y_11^0 <= 0 /\ -k_121^0 <= 0)]
	
	Blocked

	[{}, {}, {}]

Step with 16

	Trace

	19[(-k_121^0 <= 0)], 14[(1-a_10^0+y_11^0 <= 0 /\ -k_121^0 <= 0)], 16[(1+y_11^0-x_12^0 <= 0 /\ -k_121^0 <= 0)]
	
	Blocked

	[{}, {}, {}, {}]

Step with 18

	Trace

	19[(-k_121^0 <= 0)], 14[(1-a_10^0+y_11^0 <= 0 /\ -k_121^0 <= 0)], 16[(1+y_11^0-x_12^0 <= 0 /\ -k_121^0 <= 0)], 18[(-y_11^0+x_12^0 <= 0 /\ -y_11^0+x_12^0 == 0 /\ -len_181^0 <= 0 /\ y_11^0-x_12^0 <= 0 /\ -a_178^0 <= 0)]
	
	Blocked

	[{}, {}, {}, {}, {}]

Backtrack

	Trace

	19[(-k_121^0 <= 0)], 14[(1-a_10^0+y_11^0 <= 0 /\ -k_121^0 <= 0)], 16[(1+y_11^0-x_12^0 <= 0 /\ -k_121^0 <= 0)]
	
	Blocked

	[{}, {}, {}, {18[T]}]

Step with 20

	Trace

	19[(-k_121^0 <= 0)], 14[(1-a_10^0+y_11^0 <= 0 /\ -k_121^0 <= 0)], 16[(1+y_11^0-x_12^0 <= 0 /\ -k_121^0 <= 0)], 20[(-len_181^0 <= 0 /\ 1+y_11^0-x_12^0 <= 0 /\ -a_178^0 <= 0)]
	
	Blocked

	[{}, {}, {}, {18[T]}, {}]

Nonterm

Start location: l7
Program variables: __cil_tmp5_9^0 a_10^0 a_178^0 k_121^0 k_83^0 len_181^0 len_54^0 lt_15^0 result_4^0 tmp_8^0 x_12^0 x_13^0 x_7^0 y_11^0 y_14^0
  14: l0 -> l1 : x_12^0'=a_10^0, (1-a_10^0+y_11^0 <= 0 /\ -k_121^0 <= 0), cost: 1
  15: l0 -> l1 : x_12^0'=a_10^0, (-k_121^0 <= 0 /\ 1+a_10^0-y_11^0 <= 0), cost: 1
  16: l1 -> l3 : len_181^0'=1, lt_15^0'=lt_15^post4, x_12^0'=lt_15^1, (1+y_11^0-x_12^0 <= 0 /\ -k_121^0 <= 0), cost: 1
  17: l1 -> l3 : len_181^0'=1, lt_15^0'=lt_15^post5, x_12^0'=lt_15^1, (1-y_11^0+x_12^0 <= 0 /\ -k_121^0 <= 0), cost: 1
  18: l3 -> l4 : result_4^0'=result_4^post6, (-y_11^0+x_12^0 <= 0 /\ -y_11^0+x_12^0 == 0 /\ -len_181^0 <= 0 /\ y_11^0-x_12^0 <= 0 /\ -a_178^0 <= 0), cost: 1
  20: l3 -> l3 : len_181^0'=1+len_181^0, lt_15^0'=lt_15^post7, x_12^0'=x_12^post7, (-len_181^0 <= 0 /\ 1+y_11^0-x_12^0 <= 0 /\ -a_178^0 <= 0), cost: 1
  21: l3 -> l3 : len_181^0'=1+len_181^0, lt_15^0'=lt_15^post9, x_12^0'=x_12^post9, (1-y_11^0+x_12^0 <= 0 /\ -len_181^0 <= 0 /\ -a_178^0 <= 0), cost: 1
  22: l3 -> LoAT_sink : (len_181^0 >= 0 /\ a_178^0 >= 0 /\ x_12^0-x_12^post7 <= 0 /\ -1-y_11^0+x_12^0 >= 0), cost: NONTERM
  23: l3 -> l3 : len_181^0'=len_181^0+n, lt_15^0'=lt_15^post7, x_12^0'=x_12^post7, (len_181^0 >= 0 /\ -1+n >= 0 /\ a_178^0 >= 0 /\ -1-y_11^0+x_12^0 >= 0 /\ -1-y_11^0+x_12^post7 >= 0), cost: 1
  19: l7 -> l0 : __cil_tmp5_9^0'=result_4^7, k_83^0'=3, len_54^0'=2, result_4^0'=result_4^post3, tmp_8^0'=result_4^7, x_13^0'=result_4^7, x_7^0'=result_4^7, y_14^0'=0, -k_121^0 <= 0, cost: 1

	Certificate of Non-Termination

	Original rule:
	l3 -> l3 : len_181^0'=1+len_181^0, lt_15^0'=lt_15^post7, x_12^0'=x_12^post7, (-len_181^0 <= 0 /\ 1+y_11^0-x_12^0 <= 0 /\ -a_178^0 <= 0), cost: 1
	New rule:
	l3 -> LoAT_sink : (len_181^0 >= 0 /\ a_178^0 >= 0 /\ x_12^0-x_12^post7 <= 0 /\ -1-y_11^0+x_12^0 >= 0), cost: NONTERM

		len_181^0 >= 0 [0]: monotonic increase yields len_181^0 >= 0
		
		a_178^0 >= 0 [0]: monotonic increase yields a_178^0 >= 0
		
		-1-y_11^0+x_12^0 >= 0 [0]: eventual decrease yields (-1-y_11^0+x_12^0 >= 0 /\ -1-y_11^0+x_12^post7 >= 0)
		
		-1-y_11^0+x_12^0 >= 0 [1]: eventual increase yields (x_12^0-x_12^post7 <= 0 /\ -1-y_11^0+x_12^0 >= 0)
		
		Replacement map: {len_181^0 >= 0 -> len_181^0 >= 0, a_178^0 >= 0 -> a_178^0 >= 0, -1-y_11^0+x_12^0 >= 0 -> (x_12^0-x_12^post7 <= 0 /\ -1-y_11^0+x_12^0 >= 0)}

	Loop Acceleration

	Original rule:
	l3 -> l3 : len_181^0'=1+len_181^0, lt_15^0'=lt_15^post7, x_12^0'=x_12^post7, (-len_181^0 <= 0 /\ 1+y_11^0-x_12^0 <= 0 /\ -a_178^0 <= 0), cost: 1
	New rule:
	l3 -> l3 : len_181^0'=len_181^0+n, lt_15^0'=lt_15^post7, x_12^0'=x_12^post7, (len_181^0 >= 0 /\ -1+n >= 0 /\ a_178^0 >= 0 /\ -1-y_11^0+x_12^0 >= 0 /\ -1-y_11^0+x_12^post7 >= 0), cost: 1

		len_181^0 >= 0 [0]: monotonic increase yields len_181^0 >= 0
		
		a_178^0 >= 0 [0]: monotonic increase yields a_178^0 >= 0
		
		-1-y_11^0+x_12^0 >= 0 [0]: eventual decrease yields (-1-y_11^0+x_12^0 >= 0 /\ -1-y_11^0+x_12^post7 >= 0)
		
		-1-y_11^0+x_12^0 >= 0 [1]: eventual increase yields (x_12^0-x_12^post7 <= 0 /\ -1-y_11^0+x_12^0 >= 0)
		
		Replacement map: {len_181^0 >= 0 -> len_181^0 >= 0, a_178^0 >= 0 -> a_178^0 >= 0, -1-y_11^0+x_12^0 >= 0 -> (-1-y_11^0+x_12^0 >= 0 /\ -1-y_11^0+x_12^post7 >= 0)}

Step with 22

	Trace

	19[(-k_121^0 <= 0)], 14[(1-a_10^0+y_11^0 <= 0 /\ -k_121^0 <= 0)], 16[(1+y_11^0-x_12^0 <= 0 /\ -k_121^0 <= 0)], 22[(len_181^0 >= 0 /\ a_178^0 >= 0 /\ x_12^0-x_12^post7 <= 0 /\ -1-y_11^0+x_12^0 >= 0)]
	
	Blocked

	[{}, {}, {}, {18[T]}, {22[T]}]

Refute

	Counterexample

	[ __cil_tmp5_9^0=0 a_10^0=0 a_178^0=0 k_121^0=0 k_83^0=3 len_181^0=0 len_54^0=2 lt_15^0=0 result_4^0=0 tmp_8^0=0 x_12^0=0 x_13^0=0 x_7^0=0 y_11^0=-1 y_14^0=0 ] 19 [ __cil_tmp5_9^0=0 a_10^0=0 a_178^0=0 k_121^0=0 k_83^0=3 len_181^0=0 len_54^0=2 lt_15^0=0 result_4^0=0 tmp_8^0=0 x_12^0=0 x_13^0=0 x_7^0=0 y_11^0=-1 y_14^0=0 ] 14 [ __cil_tmp5_9^0=0 a_10^0=0 a_178^0=0 k_121^0=0 k_83^0=3 len_181^0=1 len_54^0=2 lt_15^0=0 result_4^0=0 tmp_8^0=0 x_12^0=0 x_13^0=0 x_7^0=0 y_11^0=-1 y_14^0=0 ] 16 [ __cil_tmp5_9^0=__cil_tmp5_9^0 a_10^0=0 a_178^0=0 k_121^0=0 k_83^0=k_83^0 len_181^0=0 len_54^0=len_54^0 lt_15^0=0 result_4^0=result_4^0 tmp_8^0=tmp_8^0 x_12^0=0 x_13^0=x_13^0 x_7^0=x_7^0 y_11^0=-1 y_14^0=y_14^0 ] 22
	
NO

Build SHA: a05f16bf13df659c382799650051f91bf6828c7b