unknown

Initial ITS

Start location: l19
Program variables: ___len21^0 ret_my_malloc10^0 ret_my_malloc14^0 retval^0 size11^0 size15^0 size17^0 size7^0 tmp13^0 tmp22^0 tmp9^0 tmp^0 tmp___0^0 tmp___1^0
   0: l0 -> l1 : ___len21^0'=___len21^post1, ret_my_malloc10^0'=ret_my_malloc10^post1, ret_my_malloc14^0'=ret_my_malloc14^post1, retval^0'=retval^post1, size11^0'=size11^post1, size15^0'=size15^post1, size17^0'=size17^post1, size7^0'=size7^post1, tmp13^0'=tmp13^post1, tmp22^0'=tmp22^post1, tmp9^0'=tmp9^post1, tmp^0'=tmp^post1, tmp___0^0'=tmp___0^post1, tmp___1^0'=tmp___1^post1, (tmp9^0-tmp9^post1 == 0 /\ -ret_my_malloc14^post1+ret_my_malloc14^0 == 0 /\ tmp___1^0-tmp___1^post1 == 0 /\ -___len21^post1+___len21^0 == 0 /\ tmp13^0-tmp13^post1 == 0 /\ -size15^post1+size15^0 == 0 /\ size11^0-size11^post1 == 0 /\ -size7^post1+size7^0 == 0 /\ retval^0-retval^post1 == 0 /\ -tmp___0^post1+tmp___0^0 == 0 /\ -tmp22^post1+tmp22^0 == 0 /\ -tmp^post1+tmp^0 == 0 /\ size17^0-size17^post1 == 0 /\ ret_my_malloc10^post1 == 0), cost: 1
   1: l0 -> l1 : ___len21^0'=___len21^post2, ret_my_malloc10^0'=ret_my_malloc10^post2, ret_my_malloc14^0'=ret_my_malloc14^post2, retval^0'=retval^post2, size11^0'=size11^post2, size15^0'=size15^post2, size17^0'=size17^post2, size7^0'=size7^post2, tmp13^0'=tmp13^post2, tmp22^0'=tmp22^post2, tmp9^0'=tmp9^post2, tmp^0'=tmp^post2, tmp___0^0'=tmp___0^post2, tmp___1^0'=tmp___1^post2, (-___len21^post2+___len21^0 == 0 /\ -tmp9^post2+tmp9^0 == 0 /\ tmp^0-tmp^post2 == 0 /\ retval^0-retval^post2 == 0 /\ tmp22^0-tmp22^post2 == 0 /\ -size7^post2+size7^0 == 0 /\ tmp13^0-tmp13^post2 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post2 == 0 /\ -tmp___1^post2+tmp___1^0 == 0 /\ -1+ret_my_malloc10^post2 == 0 /\ size15^0-size15^post2 == 0 /\ -size11^post2+size11^0 == 0 /\ size17^0-size17^post2 == 0 /\ -tmp___0^post2+tmp___0^0 == 0), cost: 1
  28: l1 -> l17 : ___len21^0'=___len21^post29, ret_my_malloc10^0'=ret_my_malloc10^post29, ret_my_malloc14^0'=ret_my_malloc14^post29, retval^0'=retval^post29, size11^0'=size11^post29, size15^0'=size15^post29, size17^0'=size17^post29, size7^0'=size7^post29, tmp13^0'=tmp13^post29, tmp22^0'=tmp22^post29, tmp9^0'=tmp9^post29, tmp^0'=tmp^post29, tmp___0^0'=tmp___0^post29, tmp___1^0'=tmp___1^post29, (-ret_my_malloc14^post29+ret_my_malloc14^0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post29 == 0 /\ -tmp___0^post29+tmp___0^0 == 0 /\ -size15^post29+size15^0 == 0 /\ size17^0-size17^post29 == 0 /\ tmp13^0-tmp13^post29 == 0 /\ -tmp22^post29+tmp22^0 == 0 /\ -___len21^post29+___len21^0 == 0 /\ -tmp^post29+retval^post29 == 0 /\ tmp9^0-tmp9^post29 == 0 /\ size7^0-size7^post29 == 0 /\ -ret_my_malloc10^0+tmp^post29 == 0 /\ size11^0-size11^post29 == 0 /\ tmp___1^0-tmp___1^post29 == 0), cost: 1
   2: l2 -> l3 : ___len21^0'=___len21^post3, ret_my_malloc10^0'=ret_my_malloc10^post3, ret_my_malloc14^0'=ret_my_malloc14^post3, retval^0'=retval^post3, size11^0'=size11^post3, size15^0'=size15^post3, size17^0'=size17^post3, size7^0'=size7^post3, tmp13^0'=tmp13^post3, tmp22^0'=tmp22^post3, tmp9^0'=tmp9^post3, tmp^0'=tmp^post3, tmp___0^0'=tmp___0^post3, tmp___1^0'=tmp___1^post3, (size17^0-size17^post3 == 0 /\ tmp___1^0-tmp___1^post3 == 0 /\ -ret_my_malloc14^post3+ret_my_malloc14^0 == 0 /\ retval^0-retval^post3 == 0 /\ -tmp___0^post3+tmp___0^0 == 0 /\ tmp13^0-tmp13^post3 == 0 /\ -___len21^post3+___len21^0 == 0 /\ -tmp22^post3+tmp22^0 == 0 /\ -tmp^post3+tmp^0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post3 == 0 /\ size7^0-size7^post3 == 0 /\ tmp9^0-tmp9^post3 == 0 /\ -size15^post3+size15^0 == 0 /\ size11^0-size11^post3 == 0), cost: 1
   3: l4 -> l2 : ___len21^0'=___len21^post4, ret_my_malloc10^0'=ret_my_malloc10^post4, ret_my_malloc14^0'=ret_my_malloc14^post4, retval^0'=retval^post4, size11^0'=size11^post4, size15^0'=size15^post4, size17^0'=size17^post4, size7^0'=size7^post4, tmp13^0'=tmp13^post4, tmp22^0'=tmp22^post4, tmp9^0'=tmp9^post4, tmp^0'=tmp^post4, tmp___0^0'=tmp___0^post4, tmp___1^0'=tmp___1^post4, (0 == 0 /\ tmp13^0-tmp13^post4 == 0 /\ -size17^post4+size17^0 == 0 /\ tmp22^0-tmp22^post4 == 0 /\ retval^0-retval^post4 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post4 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post4 == 0 /\ -tmp___1^post4+tmp___1^0 == 0 /\ size15^0-size15^post4 == 0 /\ -size11^post4+size11^0 == 0 /\ -tmp9^post4+tmp9^0 == 0 /\ tmp^0-tmp^post4 == 0 /\ -___len21^post4+___len21^0 == 0 /\ -size7^post4+size7^0 == 0), cost: 1
   4: l5 -> l2 : ___len21^0'=___len21^post5, ret_my_malloc10^0'=ret_my_malloc10^post5, ret_my_malloc14^0'=ret_my_malloc14^post5, retval^0'=retval^post5, size11^0'=size11^post5, size15^0'=size15^post5, size17^0'=size17^post5, size7^0'=size7^post5, tmp13^0'=tmp13^post5, tmp22^0'=tmp22^post5, tmp9^0'=tmp9^post5, tmp^0'=tmp^post5, tmp___0^0'=tmp___0^post5, tmp___1^0'=tmp___1^post5, (0 == 0 /\ -size7^post5+size7^0 == 0 /\ tmp^0-tmp^post5 == 0 /\ -size11^post5+size11^0 == 0 /\ retval^0-retval^post5 == 0 /\ -ret_my_malloc14^post5+ret_my_malloc14^0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post5 == 0 /\ tmp9^0-tmp9^post5 == 0 /\ size17^0-size17^post5 == 0 /\ -tmp___1^post5+tmp___1^0 == 0 /\ -tmp___0^post5+tmp___0^0 == 0 /\ 1+tmp___1^0 <= 0 /\ -1-tmp___1^0 <= 0 /\ -size15^post5+size15^0 == 0 /\ -100+___len21^post5 == 0 /\ tmp13^0-tmp13^post5 == 0), cost: 1
   5: l5 -> l4 : ___len21^0'=___len21^post6, ret_my_malloc10^0'=ret_my_malloc10^post6, ret_my_malloc14^0'=ret_my_malloc14^post6, retval^0'=retval^post6, size11^0'=size11^post6, size15^0'=size15^post6, size17^0'=size17^post6, size7^0'=size7^post6, tmp13^0'=tmp13^post6, tmp22^0'=tmp22^post6, tmp9^0'=tmp9^post6, tmp^0'=tmp^post6, tmp___0^0'=tmp___0^post6, tmp___1^0'=tmp___1^post6, (-___len21^post6+___len21^0 == 0 /\ -tmp___1^0 <= 0 /\ size17^0-size17^post6 == 0 /\ -tmp^post6+tmp^0 == 0 /\ tmp13^0-tmp13^post6 == 0 /\ -ret_my_malloc14^post6+ret_my_malloc14^0 == 0 /\ -ret_my_malloc10^post6+ret_my_malloc10^0 == 0 /\ -tmp22^post6+tmp22^0 == 0 /\ tmp9^0-tmp9^post6 == 0 /\ tmp___1^0-tmp___1^post6 == 0 /\ -size15^post6+size15^0 == 0 /\ size11^0-size11^post6 == 0 /\ size7^0-size7^post6 == 0 /\ retval^0-retval^post6 == 0 /\ -tmp___0^post6+tmp___0^0 == 0), cost: 1
   6: l5 -> l4 : ___len21^0'=___len21^post7, ret_my_malloc10^0'=ret_my_malloc10^post7, ret_my_malloc14^0'=ret_my_malloc14^post7, retval^0'=retval^post7, size11^0'=size11^post7, size15^0'=size15^post7, size17^0'=size17^post7, size7^0'=size7^post7, tmp13^0'=tmp13^post7, tmp22^0'=tmp22^post7, tmp9^0'=tmp9^post7, tmp^0'=tmp^post7, tmp___0^0'=tmp___0^post7, tmp___1^0'=tmp___1^post7, (-size17^post7+size17^0 == 0 /\ -retval^post7+retval^0 == 0 /\ -size11^post7+size11^0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post7 == 0 /\ tmp22^0-tmp22^post7 == 0 /\ -tmp___0^post7+tmp___0^0 == 0 /\ -___len21^post7+___len21^0 == 0 /\ -tmp9^post7+tmp9^0 == 0 /\ tmp13^0-tmp13^post7 == 0 /\ -size7^post7+size7^0 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post7 == 0 /\ 2+tmp___1^0 <= 0 /\ size15^0-size15^post7 == 0 /\ tmp^0-tmp^post7 == 0 /\ -tmp___1^post7+tmp___1^0 == 0), cost: 1
   7: l6 -> l3 : ___len21^0'=___len21^post8, ret_my_malloc10^0'=ret_my_malloc10^post8, ret_my_malloc14^0'=ret_my_malloc14^post8, retval^0'=retval^post8, size11^0'=size11^post8, size15^0'=size15^post8, size17^0'=size17^post8, size7^0'=size7^post8, tmp13^0'=tmp13^post8, tmp22^0'=tmp22^post8, tmp9^0'=tmp9^post8, tmp^0'=tmp^post8, tmp___0^0'=tmp___0^post8, tmp___1^0'=tmp___1^post8, (-ret_my_malloc10^post8+ret_my_malloc10^0 == 0 /\ -tmp^post8+tmp^0 == 0 /\ -tmp22^post8+tmp22^0 == 0 /\ size17^0-size17^post8 == 0 /\ -size11^post8+size11^0 == 0 /\ -ret_my_malloc14^post8+ret_my_malloc14^0 == 0 /\ size7^0-size7^post8 == 0 /\ -size15^post8+size15^0 == 0 /\ tmp9^0-tmp9^post8 == 0 /\ retval^0-retval^post8 == 0 /\ tmp___1^0-tmp___1^post8 == 0 /\ tmp13^0-tmp13^post8 == 0 /\ -___len21^post8+___len21^0 == 0 /\ -tmp___0^post8+tmp___0^0 == 0), cost: 1
   8: l7 -> l6 : ___len21^0'=___len21^post9, ret_my_malloc10^0'=ret_my_malloc10^post9, ret_my_malloc14^0'=ret_my_malloc14^post9, retval^0'=retval^post9, size11^0'=size11^post9, size15^0'=size15^post9, size17^0'=size17^post9, size7^0'=size7^post9, tmp13^0'=tmp13^post9, tmp22^0'=tmp22^post9, tmp9^0'=tmp9^post9, tmp^0'=tmp^post9, tmp___0^0'=tmp___0^post9, tmp___1^0'=tmp___1^post9, (tmp___0^0-tmp___0^post9 == 0 /\ -size7^post9+size7^0 == 0 /\ size17^0-size17^post9 == 0 /\ -___len21^post9+___len21^0 == 0 /\ tmp13^0-tmp13^post9 == 0 /\ -tmp___1^post9+tmp___1^0 == 0 /\ size15^0-size15^post9 == 0 /\ -size11^post9+size11^0 == 0 /\ -tmp22^post9+tmp22^0 == 0 /\ tmp^0-tmp^post9 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post9 == 0 /\ tmp9^0-tmp9^post9 == 0 /\ -retval^post9+retval^0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post9 == 0), cost: 1
   9: l8 -> l7 : ___len21^0'=___len21^post10, ret_my_malloc10^0'=ret_my_malloc10^post10, ret_my_malloc14^0'=ret_my_malloc14^post10, retval^0'=retval^post10, size11^0'=size11^post10, size15^0'=size15^post10, size17^0'=size17^post10, size7^0'=size7^post10, tmp13^0'=tmp13^post10, tmp22^0'=tmp22^post10, tmp9^0'=tmp9^post10, tmp^0'=tmp^post10, tmp___0^0'=tmp___0^post10, tmp___1^0'=tmp___1^post10, (ret_my_malloc10^0-ret_my_malloc10^post10 == 0 /\ -size11^post10+size11^0 == 0 /\ -ret_my_malloc14^post10+ret_my_malloc14^0 == 0 /\ -tmp___0^post10+tmp___0^0 == 0 /\ tmp9^0-tmp9^post10 == 0 /\ tmp^0-tmp^post10 == 0 /\ retval^0-retval^post10 == 0 /\ size17^0-size17^post10 == 0 /\ -___len21^post10+___len21^0 == 0 /\ tmp13^0-tmp13^post10 == 0 /\ -tmp22^post10+tmp22^0 == 0 /\ -size7^post10+size7^0 == 0 /\ -size15^post10+size15^0 == 0 /\ -tmp___1^post10+tmp___1^0 == 0), cost: 1
  10: l8 -> l6 : ___len21^0'=___len21^post11, ret_my_malloc10^0'=ret_my_malloc10^post11, ret_my_malloc14^0'=ret_my_malloc14^post11, retval^0'=retval^post11, size11^0'=size11^post11, size15^0'=size15^post11, size17^0'=size17^post11, size7^0'=size7^post11, tmp13^0'=tmp13^post11, tmp22^0'=tmp22^post11, tmp9^0'=tmp9^post11, tmp^0'=tmp^post11, tmp___0^0'=tmp___0^post11, tmp___1^0'=tmp___1^post11, (-ret_my_malloc10^post11+ret_my_malloc10^0 == 0 /\ -size11^post11+size11^0 == 0 /\ -size15^post11+size15^0 == 0 /\ -size7^post11+size7^0 == 0 /\ tmp9^0-tmp9^post11 == 0 /\ -ret_my_malloc14^post11+ret_my_malloc14^0 == 0 /\ -tmp___0^post11+tmp___0^0 == 0 /\ tmp22^0-tmp22^post11 == 0 /\ size17^0-size17^post11 == 0 /\ tmp___1^0-tmp___1^post11 == 0 /\ -tmp^post11+tmp^0 == 0 /\ retval^0-retval^post11 == 0 /\ -___len21^post11+___len21^0 == 0 /\ tmp13^0-tmp13^post11 == 0), cost: 1
  11: l8 -> l7 : ___len21^0'=___len21^post12, ret_my_malloc10^0'=ret_my_malloc10^post12, ret_my_malloc14^0'=ret_my_malloc14^post12, retval^0'=retval^post12, size11^0'=size11^post12, size15^0'=size15^post12, size17^0'=size17^post12, size7^0'=size7^post12, tmp13^0'=tmp13^post12, tmp22^0'=tmp22^post12, tmp9^0'=tmp9^post12, tmp^0'=tmp^post12, tmp___0^0'=tmp___0^post12, tmp___1^0'=tmp___1^post12, (tmp^0-tmp^post12 == 0 /\ size15^0-size15^post12 == 0 /\ -tmp13^post12+tmp13^0 == 0 /\ -tmp22^post12+tmp22^0 == 0 /\ -___len21^post12+___len21^0 == 0 /\ tmp9^0-tmp9^post12 == 0 /\ tmp___1^0-tmp___1^post12 == 0 /\ -size11^post12+size11^0 == 0 /\ -size7^post12+size7^0 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post12 == 0 /\ -retval^post12+retval^0 == 0 /\ -tmp___0^post12+tmp___0^0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post12 == 0 /\ size17^0-size17^post12 == 0), cost: 1
  12: l9 -> l8 : ___len21^0'=___len21^post13, ret_my_malloc10^0'=ret_my_malloc10^post13, ret_my_malloc14^0'=ret_my_malloc14^post13, retval^0'=retval^post13, size11^0'=size11^post13, size15^0'=size15^post13, size17^0'=size17^post13, size7^0'=size7^post13, tmp13^0'=tmp13^post13, tmp22^0'=tmp22^post13, tmp9^0'=tmp9^post13, tmp^0'=tmp^post13, tmp___0^0'=tmp___0^post13, tmp___1^0'=tmp___1^post13, (-ret_my_malloc14^post13+ret_my_malloc14^0 == 0 /\ retval^0-retval^post13 == 0 /\ -tmp___1^post13+tmp___1^0 == 0 /\ -tmp___0^post13+tmp___0^0 == 0 /\ -___len21^post13+___len21^0 == 0 /\ -tmp^post13+tmp^0 == 0 /\ -100+size17^post13 == 0 /\ tmp22^0-tmp22^post13 == 0 /\ -size15^post13+size15^0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post13 == 0 /\ -size7^post13+size7^0 == 0 /\ tmp13^0-tmp13^post13 == 0 /\ -size11^post13+size11^0 == 0 /\ -tmp9^post13+tmp9^0 == 0), cost: 1
  13: l10 -> l3 : ___len21^0'=___len21^post14, ret_my_malloc10^0'=ret_my_malloc10^post14, ret_my_malloc14^0'=ret_my_malloc14^post14, retval^0'=retval^post14, size11^0'=size11^post14, size15^0'=size15^post14, size17^0'=size17^post14, size7^0'=size7^post14, tmp13^0'=tmp13^post14, tmp22^0'=tmp22^post14, tmp9^0'=tmp9^post14, tmp^0'=tmp^post14, tmp___0^0'=tmp___0^post14, tmp___1^0'=tmp___1^post14, (-tmp22^post14+tmp22^0 == 0 /\ size15^0-size15^post14 == 0 /\ retval^0-retval^post14 == 0 /\ tmp___0^0-tmp___0^post14 == 0 /\ -size7^post14+size7^0 == 0 /\ size17^0-size17^post14 == 0 /\ -___len21^post14+___len21^0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post14 == 0 /\ -size11^post14+size11^0 == 0 /\ -tmp___1^post14+tmp___1^0 == 0 /\ tmp13^0-tmp13^post14 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post14 == 0 /\ tmp9^0-tmp9^post14 == 0 /\ tmp^0-tmp^post14 == 0), cost: 1
  14: l11 -> l10 : ___len21^0'=___len21^post15, ret_my_malloc10^0'=ret_my_malloc10^post15, ret_my_malloc14^0'=ret_my_malloc14^post15, retval^0'=retval^post15, size11^0'=size11^post15, size15^0'=size15^post15, size17^0'=size17^post15, size7^0'=size7^post15, tmp13^0'=tmp13^post15, tmp22^0'=tmp22^post15, tmp9^0'=tmp9^post15, tmp^0'=tmp^post15, tmp___0^0'=tmp___0^post15, tmp___1^0'=tmp___1^post15, (tmp^0-tmp^post15 == 0 /\ -tmp22^post15+tmp22^0 == 0 /\ tmp9^0-tmp9^post15 == 0 /\ tmp___1^0-tmp___1^post15 == 0 /\ -tmp13^post15+tmp13^0 == 0 /\ retval^0-retval^post15 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post15 == 0 /\ -size7^post15+size7^0 == 0 /\ -ret_my_malloc14^post15+ret_my_malloc14^0 == 0 /\ -tmp___0^post15+tmp___0^0 == 0 /\ -size11^post15+size11^0 == 0 /\ -size15^post15+size15^0 == 0 /\ size17^0-size17^post15 == 0 /\ -___len21^post15+___len21^0 == 0), cost: 1
  15: l12 -> l11 : ___len21^0'=___len21^post16, ret_my_malloc10^0'=ret_my_malloc10^post16, ret_my_malloc14^0'=ret_my_malloc14^post16, retval^0'=retval^post16, size11^0'=size11^post16, size15^0'=size15^post16, size17^0'=size17^post16, size7^0'=size7^post16, tmp13^0'=tmp13^post16, tmp22^0'=tmp22^post16, tmp9^0'=tmp9^post16, tmp^0'=tmp^post16, tmp___0^0'=tmp___0^post16, tmp___1^0'=tmp___1^post16, (-size7^post16+size7^0 == 0 /\ -___len21^post16+___len21^0 == 0 /\ -ret_my_malloc14^post16+ret_my_malloc14^0 == 0 /\ -size11^post16+size11^0 == 0 /\ -tmp___0^post16+tmp___0^0 == 0 /\ retval^0-retval^post16 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post16 == 0 /\ tmp22^0-tmp22^post16 == 0 /\ size17^0-size17^post16 == 0 /\ -tmp^post16+tmp^0 == 0 /\ tmp___1^0-tmp___1^post16 == 0 /\ size15^0-size15^post16 == 0 /\ tmp13^0-tmp13^post16 == 0 /\ -tmp9^post16+tmp9^0 == 0), cost: 1
  16: l12 -> l10 : ___len21^0'=___len21^post17, ret_my_malloc10^0'=ret_my_malloc10^post17, ret_my_malloc14^0'=ret_my_malloc14^post17, retval^0'=retval^post17, size11^0'=size11^post17, size15^0'=size15^post17, size17^0'=size17^post17, size7^0'=size7^post17, tmp13^0'=tmp13^post17, tmp22^0'=tmp22^post17, tmp9^0'=tmp9^post17, tmp^0'=tmp^post17, tmp___0^0'=tmp___0^post17, tmp___1^0'=tmp___1^post17, (retval^0-retval^post17 == 0 /\ size17^0-size17^post17 == 0 /\ -size15^post17+size15^0 == 0 /\ tmp9^0-tmp9^post17 == 0 /\ -size7^post17+size7^0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post17 == 0 /\ -___len21^post17+___len21^0 == 0 /\ tmp___1^0-tmp___1^post17 == 0 /\ -size11^post17+size11^0 == 0 /\ -tmp___0^post17+tmp___0^0 == 0 /\ -tmp22^post17+tmp22^0 == 0 /\ tmp13^0-tmp13^post17 == 0 /\ -tmp^post17+tmp^0 == 0 /\ -ret_my_malloc14^post17+ret_my_malloc14^0 == 0), cost: 1
  17: l12 -> l11 : ___len21^0'=___len21^post18, ret_my_malloc10^0'=ret_my_malloc10^post18, ret_my_malloc14^0'=ret_my_malloc14^post18, retval^0'=retval^post18, size11^0'=size11^post18, size15^0'=size15^post18, size17^0'=size17^post18, size7^0'=size7^post18, tmp13^0'=tmp13^post18, tmp22^0'=tmp22^post18, tmp9^0'=tmp9^post18, tmp^0'=tmp^post18, tmp___0^0'=tmp___0^post18, tmp___1^0'=tmp___1^post18, (size15^0-size15^post18 == 0 /\ tmp___0^0-tmp___0^post18 == 0 /\ -tmp___1^post18+tmp___1^0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post18 == 0 /\ -tmp22^post18+tmp22^0 == 0 /\ size17^0-size17^post18 == 0 /\ -___len21^post18+___len21^0 == 0 /\ -size7^post18+size7^0 == 0 /\ -size11^post18+size11^0 == 0 /\ tmp^0-tmp^post18 == 0 /\ tmp9^0-tmp9^post18 == 0 /\ tmp13^0-tmp13^post18 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post18 == 0 /\ retval^0-retval^post18 == 0), cost: 1
  18: l13 -> l12 : ___len21^0'=___len21^post19, ret_my_malloc10^0'=ret_my_malloc10^post19, ret_my_malloc14^0'=ret_my_malloc14^post19, retval^0'=retval^post19, size11^0'=size11^post19, size15^0'=size15^post19, size17^0'=size17^post19, size7^0'=size7^post19, tmp13^0'=tmp13^post19, tmp22^0'=tmp22^post19, tmp9^0'=tmp9^post19, tmp^0'=tmp^post19, tmp___0^0'=tmp___0^post19, tmp___1^0'=tmp___1^post19, (tmp^0-tmp^post19 == 0 /\ -100+size15^post19 == 0 /\ -size7^post19+size7^0 == 0 /\ -tmp___0^post19+tmp___0^0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post19 == 0 /\ tmp9^0-tmp9^post19 == 0 /\ -tmp22^post19+tmp22^0 == 0 /\ tmp___1^0-tmp___1^post19 == 0 /\ -size11^post19+size11^0 == 0 /\ size17^0-size17^post19 == 0 /\ -___len21^post19+___len21^0 == 0 /\ retval^0-retval^post19 == 0 /\ tmp13^0-tmp13^post19 == 0 /\ -ret_my_malloc14^post19+ret_my_malloc14^0 == 0), cost: 1
  19: l14 -> l15 : ___len21^0'=___len21^post20, ret_my_malloc10^0'=ret_my_malloc10^post20, ret_my_malloc14^0'=ret_my_malloc14^post20, retval^0'=retval^post20, size11^0'=size11^post20, size15^0'=size15^post20, size17^0'=size17^post20, size7^0'=size7^post20, tmp13^0'=tmp13^post20, tmp22^0'=tmp22^post20, tmp9^0'=tmp9^post20, tmp^0'=tmp^post20, tmp___0^0'=tmp___0^post20, tmp___1^0'=tmp___1^post20, (-size15^post20+size15^0 == 0 /\ -tmp___0^post20+tmp___0^0 == 0 /\ -___len21^post20+___len21^0 == 0 /\ tmp___1^0-tmp___1^post20 == 0 /\ tmp22^0-tmp22^post20 == 0 /\ -tmp9^post20+tmp9^0 == 0 /\ tmp13^0-tmp13^post20 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post20 == 0 /\ -tmp^post20+tmp^0 == 0 /\ size17^0-size17^post20 == 0 /\ -ret_my_malloc14^0+retval^post20 == 0 /\ -size11^post20+size11^0 == 0 /\ -size7^post20+size7^0 == 0 /\ -ret_my_malloc14^post20+ret_my_malloc14^0 == 0), cost: 1
  20: l15 -> l5 : ___len21^0'=___len21^post21, ret_my_malloc10^0'=ret_my_malloc10^post21, ret_my_malloc14^0'=ret_my_malloc14^post21, retval^0'=retval^post21, size11^0'=size11^post21, size15^0'=size15^post21, size17^0'=size17^post21, size7^0'=size7^post21, tmp13^0'=tmp13^post21, tmp22^0'=tmp22^post21, tmp9^0'=tmp9^post21, tmp^0'=tmp^post21, tmp___0^0'=tmp___0^post21, tmp___1^0'=tmp___1^post21, (0 == 0 /\ -size7^post21+size7^0 == 0 /\ size15^0-size15^post21 == 0 /\ size17^0-size17^post21 == 0 /\ tmp9^0-tmp9^post21 == 0 /\ 1-retval^0 <= 0 /\ -1+retval^0 <= 0 /\ tmp13^0-tmp13^post21 == 0 /\ -retval^post21+retval^0 == 0 /\ -size11^post21+size11^0 == 0 /\ -___len21^post21+___len21^0 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post21 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post21 == 0 /\ -tmp___0^post21+tmp___0^0 == 0 /\ -tmp22^post21+tmp22^0 == 0 /\ -tmp^post21+tmp^0 == 0), cost: 1
  21: l15 -> l13 : ___len21^0'=___len21^post22, ret_my_malloc10^0'=ret_my_malloc10^post22, ret_my_malloc14^0'=ret_my_malloc14^post22, retval^0'=retval^post22, size11^0'=size11^post22, size15^0'=size15^post22, size17^0'=size17^post22, size7^0'=size7^post22, tmp13^0'=tmp13^post22, tmp22^0'=tmp22^post22, tmp9^0'=tmp9^post22, tmp^0'=tmp^post22, tmp___0^0'=tmp___0^post22, tmp___1^0'=tmp___1^post22, (retval^0-retval^post22 == 0 /\ 2-retval^0 <= 0 /\ -tmp___1^post22+tmp___1^0 == 0 /\ -tmp___0^post22+tmp___0^0 == 0 /\ -size11^post22+size11^0 == 0 /\ -ret_my_malloc14^post22+ret_my_malloc14^0 == 0 /\ tmp^0-tmp^post22 == 0 /\ -tmp9^post22+tmp9^0 == 0 /\ size15^0-size15^post22 == 0 /\ -___len21^post22+___len21^0 == 0 /\ tmp13^0-tmp13^post22 == 0 /\ tmp22^0-tmp22^post22 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post22 == 0 /\ size17^0-size17^post22 == 0 /\ -size7^post22+size7^0 == 0), cost: 1
  22: l15 -> l13 : ___len21^0'=___len21^post23, ret_my_malloc10^0'=ret_my_malloc10^post23, ret_my_malloc14^0'=ret_my_malloc14^post23, retval^0'=retval^post23, size11^0'=size11^post23, size15^0'=size15^post23, size17^0'=size17^post23, size7^0'=size7^post23, tmp13^0'=tmp13^post23, tmp22^0'=tmp22^post23, tmp9^0'=tmp9^post23, tmp^0'=tmp^post23, tmp___0^0'=tmp___0^post23, tmp___1^0'=tmp___1^post23, (tmp___0^0-tmp___0^post23 == 0 /\ retval^0-retval^post23 == 0 /\ -tmp___1^post23+tmp___1^0 == 0 /\ retval^0 <= 0 /\ tmp^0-tmp^post23 == 0 /\ size17^0-size17^post23 == 0 /\ size15^0-size15^post23 == 0 /\ tmp9^0-tmp9^post23 == 0 /\ -size7^post23+size7^0 == 0 /\ -___len21^post23+___len21^0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post23 == 0 /\ -size11^post23+size11^0 == 0 /\ tmp13^0-tmp13^post23 == 0 /\ -tmp22^post23+tmp22^0 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post23 == 0), cost: 1
  23: l16 -> l14 : ___len21^0'=___len21^post24, ret_my_malloc10^0'=ret_my_malloc10^post24, ret_my_malloc14^0'=ret_my_malloc14^post24, retval^0'=retval^post24, size11^0'=size11^post24, size15^0'=size15^post24, size17^0'=size17^post24, size7^0'=size7^post24, tmp13^0'=tmp13^post24, tmp22^0'=tmp22^post24, tmp9^0'=tmp9^post24, tmp^0'=tmp^post24, tmp___0^0'=tmp___0^post24, tmp___1^0'=tmp___1^post24, (-tmp22^post24+tmp22^0 == 0 /\ tmp9^0-tmp9^post24 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post24 == 0 /\ ret_my_malloc14^post24 == 0 /\ tmp^0-tmp^post24 == 0 /\ -size15^post24+size15^0 == 0 /\ -size7^post24+size7^0 == 0 /\ tmp13^0-tmp13^post24 == 0 /\ tmp___1^0-tmp___1^post24 == 0 /\ -___len21^post24+___len21^0 == 0 /\ retval^0-retval^post24 == 0 /\ -tmp___0^post24+tmp___0^0 == 0 /\ -size11^post24+size11^0 == 0 /\ size17^0-size17^post24 == 0), cost: 1
  24: l16 -> l14 : ___len21^0'=___len21^post25, ret_my_malloc10^0'=ret_my_malloc10^post25, ret_my_malloc14^0'=ret_my_malloc14^post25, retval^0'=retval^post25, size11^0'=size11^post25, size15^0'=size15^post25, size17^0'=size17^post25, size7^0'=size7^post25, tmp13^0'=tmp13^post25, tmp22^0'=tmp22^post25, tmp9^0'=tmp9^post25, tmp^0'=tmp^post25, tmp___0^0'=tmp___0^post25, tmp___1^0'=tmp___1^post25, (-tmp___1^post25+tmp___1^0 == 0 /\ -size7^post25+size7^0 == 0 /\ -tmp___0^post25+tmp___0^0 == 0 /\ tmp^0-tmp^post25 == 0 /\ -1+ret_my_malloc14^post25 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post25 == 0 /\ retval^0-retval^post25 == 0 /\ tmp22^0-tmp22^post25 == 0 /\ size15^0-size15^post25 == 0 /\ -size11^post25+size11^0 == 0 /\ size17^0-size17^post25 == 0 /\ tmp13^0-tmp13^post25 == 0 /\ -___len21^post25+___len21^0 == 0 /\ -tmp9^post25+tmp9^0 == 0), cost: 1
  25: l17 -> l9 : ___len21^0'=___len21^post26, ret_my_malloc10^0'=ret_my_malloc10^post26, ret_my_malloc14^0'=ret_my_malloc14^post26, retval^0'=retval^post26, size11^0'=size11^post26, size15^0'=size15^post26, size17^0'=size17^post26, size7^0'=size7^post26, tmp13^0'=tmp13^post26, tmp22^0'=tmp22^post26, tmp9^0'=tmp9^post26, tmp^0'=tmp^post26, tmp___0^0'=tmp___0^post26, tmp___1^0'=tmp___1^post26, (tmp___1^0-tmp___1^post26 == 0 /\ tmp13^0-tmp13^post26 == 0 /\ 2-retval^0 <= 0 /\ -ret_my_malloc14^post26+ret_my_malloc14^0 == 0 /\ -size15^post26+size15^0 == 0 /\ size17^0-size17^post26 == 0 /\ -tmp___0^post26+tmp___0^0 == 0 /\ retval^0-retval^post26 == 0 /\ -tmp^post26+tmp^0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post26 == 0 /\ -tmp22^post26+tmp22^0 == 0 /\ -___len21^post26+___len21^0 == 0 /\ size11^0-size11^post26 == 0 /\ tmp9^0-tmp9^post26 == 0 /\ size7^0-size7^post26 == 0), cost: 1
  26: l17 -> l9 : ___len21^0'=___len21^post27, ret_my_malloc10^0'=ret_my_malloc10^post27, ret_my_malloc14^0'=ret_my_malloc14^post27, retval^0'=retval^post27, size11^0'=size11^post27, size15^0'=size15^post27, size17^0'=size17^post27, size7^0'=size7^post27, tmp13^0'=tmp13^post27, tmp22^0'=tmp22^post27, tmp9^0'=tmp9^post27, tmp^0'=tmp^post27, tmp___0^0'=tmp___0^post27, tmp___1^0'=tmp___1^post27, (tmp22^0-tmp22^post27 == 0 /\ retval^0 <= 0 /\ ret_my_malloc14^0-ret_my_malloc14^post27 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post27 == 0 /\ retval^0-retval^post27 == 0 /\ tmp13^0-tmp13^post27 == 0 /\ -tmp9^post27+tmp9^0 == 0 /\ -size7^post27+size7^0 == 0 /\ -tmp___1^post27+tmp___1^0 == 0 /\ -tmp___0^post27+tmp___0^0 == 0 /\ tmp^0-tmp^post27 == 0 /\ -___len21^post27+___len21^0 == 0 /\ size17^0-size17^post27 == 0 /\ -size11^post27+size11^0 == 0 /\ size15^0-size15^post27 == 0), cost: 1
  27: l17 -> l16 : ___len21^0'=___len21^post28, ret_my_malloc10^0'=ret_my_malloc10^post28, ret_my_malloc14^0'=ret_my_malloc14^post28, retval^0'=retval^post28, size11^0'=size11^post28, size15^0'=size15^post28, size17^0'=size17^post28, size7^0'=size7^post28, tmp13^0'=tmp13^post28, tmp22^0'=tmp22^post28, tmp9^0'=tmp9^post28, tmp^0'=tmp^post28, tmp___0^0'=tmp___0^post28, tmp___1^0'=tmp___1^post28, (0 == 0 /\ retval^0-retval^post28 == 0 /\ -___len21^post28+___len21^0 == 0 /\ -tmp22^post28+tmp22^0 == 0 /\ -size7^post28+size7^0 == 0 /\ -tmp___1^post28+tmp___1^0 == 0 /\ size15^0-size15^post28 == 0 /\ -ret_my_malloc14^post28+ret_my_malloc14^0 == 0 /\ -100+size11^post28 == 0 /\ 1-retval^0 <= 0 /\ -1+retval^0 <= 0 /\ ret_my_malloc10^0-ret_my_malloc10^post28 == 0 /\ size17^0-size17^post28 == 0 /\ tmp9^0-tmp9^post28 == 0 /\ tmp^0-tmp^post28 == 0 /\ -tmp___0^post28+tmp___0^0 == 0), cost: 1
  29: l18 -> l0 : ___len21^0'=___len21^post30, ret_my_malloc10^0'=ret_my_malloc10^post30, ret_my_malloc14^0'=ret_my_malloc14^post30, retval^0'=retval^post30, size11^0'=size11^post30, size15^0'=size15^post30, size17^0'=size17^post30, size7^0'=size7^post30, tmp13^0'=tmp13^post30, tmp22^0'=tmp22^post30, tmp9^0'=tmp9^post30, tmp^0'=tmp^post30, tmp___0^0'=tmp___0^post30, tmp___1^0'=tmp___1^post30, (0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post30 == 0 /\ tmp22^0-tmp22^post30 == 0 /\ -retval^post30+retval^0 == 0 /\ tmp13^0-tmp13^post30 == 0 /\ tmp^0-tmp^post30 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post30 == 0 /\ -tmp___0^post30+tmp___0^0 == 0 /\ -100+size7^post30 == 0 /\ -___len21^post30+___len21^0 == 0 /\ size17^0-size17^post30 == 0 /\ -size11^post30+size11^0 == 0 /\ size15^0-size15^post30 == 0 /\ -tmp___1^post30+tmp___1^0 == 0), cost: 1
  30: l19 -> l18 : ___len21^0'=___len21^post31, ret_my_malloc10^0'=ret_my_malloc10^post31, ret_my_malloc14^0'=ret_my_malloc14^post31, retval^0'=retval^post31, size11^0'=size11^post31, size15^0'=size15^post31, size17^0'=size17^post31, size7^0'=size7^post31, tmp13^0'=tmp13^post31, tmp22^0'=tmp22^post31, tmp9^0'=tmp9^post31, tmp^0'=tmp^post31, tmp___0^0'=tmp___0^post31, tmp___1^0'=tmp___1^post31, (size17^0-size17^post31 == 0 /\ -ret_my_malloc10^post31+ret_my_malloc10^0 == 0 /\ tmp13^0-tmp13^post31 == 0 /\ -tmp22^post31+tmp22^0 == 0 /\ -tmp^post31+tmp^0 == 0 /\ size7^0-size7^post31 == 0 /\ -ret_my_malloc14^post31+ret_my_malloc14^0 == 0 /\ tmp___1^0-tmp___1^post31 == 0 /\ -tmp___0^post31+tmp___0^0 == 0 /\ tmp9^0-tmp9^post31 == 0 /\ size11^0-size11^post31 == 0 /\ -___len21^post31+___len21^0 == 0 /\ retval^0-retval^post31 == 0 /\ -size15^post31+size15^0 == 0), cost: 1

Chained Linear Paths

Start location: l19
Program variables: ___len21^0 ret_my_malloc10^0 ret_my_malloc14^0 retval^0 size11^0 size15^0 size17^0 size7^0 tmp13^0 tmp22^0 tmp9^0 tmp^0 tmp___0^0 tmp___1^0
   0: l0 -> l1 : ___len21^0'=___len21^post1, ret_my_malloc10^0'=ret_my_malloc10^post1, ret_my_malloc14^0'=ret_my_malloc14^post1, retval^0'=retval^post1, size11^0'=size11^post1, size15^0'=size15^post1, size17^0'=size17^post1, size7^0'=size7^post1, tmp13^0'=tmp13^post1, tmp22^0'=tmp22^post1, tmp9^0'=tmp9^post1, tmp^0'=tmp^post1, tmp___0^0'=tmp___0^post1, tmp___1^0'=tmp___1^post1, (tmp9^0-tmp9^post1 == 0 /\ -ret_my_malloc14^post1+ret_my_malloc14^0 == 0 /\ tmp___1^0-tmp___1^post1 == 0 /\ -___len21^post1+___len21^0 == 0 /\ tmp13^0-tmp13^post1 == 0 /\ -size15^post1+size15^0 == 0 /\ size11^0-size11^post1 == 0 /\ -size7^post1+size7^0 == 0 /\ retval^0-retval^post1 == 0 /\ -tmp___0^post1+tmp___0^0 == 0 /\ -tmp22^post1+tmp22^0 == 0 /\ -tmp^post1+tmp^0 == 0 /\ size17^0-size17^post1 == 0 /\ ret_my_malloc10^post1 == 0), cost: 1
   1: l0 -> l1 : ___len21^0'=___len21^post2, ret_my_malloc10^0'=ret_my_malloc10^post2, ret_my_malloc14^0'=ret_my_malloc14^post2, retval^0'=retval^post2, size11^0'=size11^post2, size15^0'=size15^post2, size17^0'=size17^post2, size7^0'=size7^post2, tmp13^0'=tmp13^post2, tmp22^0'=tmp22^post2, tmp9^0'=tmp9^post2, tmp^0'=tmp^post2, tmp___0^0'=tmp___0^post2, tmp___1^0'=tmp___1^post2, (-___len21^post2+___len21^0 == 0 /\ -tmp9^post2+tmp9^0 == 0 /\ tmp^0-tmp^post2 == 0 /\ retval^0-retval^post2 == 0 /\ tmp22^0-tmp22^post2 == 0 /\ -size7^post2+size7^0 == 0 /\ tmp13^0-tmp13^post2 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post2 == 0 /\ -tmp___1^post2+tmp___1^0 == 0 /\ -1+ret_my_malloc10^post2 == 0 /\ size15^0-size15^post2 == 0 /\ -size11^post2+size11^0 == 0 /\ size17^0-size17^post2 == 0 /\ -tmp___0^post2+tmp___0^0 == 0), cost: 1
  28: l1 -> l17 : ___len21^0'=___len21^post29, ret_my_malloc10^0'=ret_my_malloc10^post29, ret_my_malloc14^0'=ret_my_malloc14^post29, retval^0'=retval^post29, size11^0'=size11^post29, size15^0'=size15^post29, size17^0'=size17^post29, size7^0'=size7^post29, tmp13^0'=tmp13^post29, tmp22^0'=tmp22^post29, tmp9^0'=tmp9^post29, tmp^0'=tmp^post29, tmp___0^0'=tmp___0^post29, tmp___1^0'=tmp___1^post29, (-ret_my_malloc14^post29+ret_my_malloc14^0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post29 == 0 /\ -tmp___0^post29+tmp___0^0 == 0 /\ -size15^post29+size15^0 == 0 /\ size17^0-size17^post29 == 0 /\ tmp13^0-tmp13^post29 == 0 /\ -tmp22^post29+tmp22^0 == 0 /\ -___len21^post29+___len21^0 == 0 /\ -tmp^post29+retval^post29 == 0 /\ tmp9^0-tmp9^post29 == 0 /\ size7^0-size7^post29 == 0 /\ -ret_my_malloc10^0+tmp^post29 == 0 /\ size11^0-size11^post29 == 0 /\ tmp___1^0-tmp___1^post29 == 0), cost: 1
   2: l2 -> l3 : ___len21^0'=___len21^post3, ret_my_malloc10^0'=ret_my_malloc10^post3, ret_my_malloc14^0'=ret_my_malloc14^post3, retval^0'=retval^post3, size11^0'=size11^post3, size15^0'=size15^post3, size17^0'=size17^post3, size7^0'=size7^post3, tmp13^0'=tmp13^post3, tmp22^0'=tmp22^post3, tmp9^0'=tmp9^post3, tmp^0'=tmp^post3, tmp___0^0'=tmp___0^post3, tmp___1^0'=tmp___1^post3, (size17^0-size17^post3 == 0 /\ tmp___1^0-tmp___1^post3 == 0 /\ -ret_my_malloc14^post3+ret_my_malloc14^0 == 0 /\ retval^0-retval^post3 == 0 /\ -tmp___0^post3+tmp___0^0 == 0 /\ tmp13^0-tmp13^post3 == 0 /\ -___len21^post3+___len21^0 == 0 /\ -tmp22^post3+tmp22^0 == 0 /\ -tmp^post3+tmp^0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post3 == 0 /\ size7^0-size7^post3 == 0 /\ tmp9^0-tmp9^post3 == 0 /\ -size15^post3+size15^0 == 0 /\ size11^0-size11^post3 == 0), cost: 1
   3: l4 -> l2 : ___len21^0'=___len21^post4, ret_my_malloc10^0'=ret_my_malloc10^post4, ret_my_malloc14^0'=ret_my_malloc14^post4, retval^0'=retval^post4, size11^0'=size11^post4, size15^0'=size15^post4, size17^0'=size17^post4, size7^0'=size7^post4, tmp13^0'=tmp13^post4, tmp22^0'=tmp22^post4, tmp9^0'=tmp9^post4, tmp^0'=tmp^post4, tmp___0^0'=tmp___0^post4, tmp___1^0'=tmp___1^post4, (0 == 0 /\ tmp13^0-tmp13^post4 == 0 /\ -size17^post4+size17^0 == 0 /\ tmp22^0-tmp22^post4 == 0 /\ retval^0-retval^post4 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post4 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post4 == 0 /\ -tmp___1^post4+tmp___1^0 == 0 /\ size15^0-size15^post4 == 0 /\ -size11^post4+size11^0 == 0 /\ -tmp9^post4+tmp9^0 == 0 /\ tmp^0-tmp^post4 == 0 /\ -___len21^post4+___len21^0 == 0 /\ -size7^post4+size7^0 == 0), cost: 1
   4: l5 -> l2 : ___len21^0'=___len21^post5, ret_my_malloc10^0'=ret_my_malloc10^post5, ret_my_malloc14^0'=ret_my_malloc14^post5, retval^0'=retval^post5, size11^0'=size11^post5, size15^0'=size15^post5, size17^0'=size17^post5, size7^0'=size7^post5, tmp13^0'=tmp13^post5, tmp22^0'=tmp22^post5, tmp9^0'=tmp9^post5, tmp^0'=tmp^post5, tmp___0^0'=tmp___0^post5, tmp___1^0'=tmp___1^post5, (0 == 0 /\ -size7^post5+size7^0 == 0 /\ tmp^0-tmp^post5 == 0 /\ -size11^post5+size11^0 == 0 /\ retval^0-retval^post5 == 0 /\ -ret_my_malloc14^post5+ret_my_malloc14^0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post5 == 0 /\ tmp9^0-tmp9^post5 == 0 /\ size17^0-size17^post5 == 0 /\ -tmp___1^post5+tmp___1^0 == 0 /\ -tmp___0^post5+tmp___0^0 == 0 /\ 1+tmp___1^0 <= 0 /\ -1-tmp___1^0 <= 0 /\ -size15^post5+size15^0 == 0 /\ -100+___len21^post5 == 0 /\ tmp13^0-tmp13^post5 == 0), cost: 1
   5: l5 -> l4 : ___len21^0'=___len21^post6, ret_my_malloc10^0'=ret_my_malloc10^post6, ret_my_malloc14^0'=ret_my_malloc14^post6, retval^0'=retval^post6, size11^0'=size11^post6, size15^0'=size15^post6, size17^0'=size17^post6, size7^0'=size7^post6, tmp13^0'=tmp13^post6, tmp22^0'=tmp22^post6, tmp9^0'=tmp9^post6, tmp^0'=tmp^post6, tmp___0^0'=tmp___0^post6, tmp___1^0'=tmp___1^post6, (-___len21^post6+___len21^0 == 0 /\ -tmp___1^0 <= 0 /\ size17^0-size17^post6 == 0 /\ -tmp^post6+tmp^0 == 0 /\ tmp13^0-tmp13^post6 == 0 /\ -ret_my_malloc14^post6+ret_my_malloc14^0 == 0 /\ -ret_my_malloc10^post6+ret_my_malloc10^0 == 0 /\ -tmp22^post6+tmp22^0 == 0 /\ tmp9^0-tmp9^post6 == 0 /\ tmp___1^0-tmp___1^post6 == 0 /\ -size15^post6+size15^0 == 0 /\ size11^0-size11^post6 == 0 /\ size7^0-size7^post6 == 0 /\ retval^0-retval^post6 == 0 /\ -tmp___0^post6+tmp___0^0 == 0), cost: 1
   6: l5 -> l4 : ___len21^0'=___len21^post7, ret_my_malloc10^0'=ret_my_malloc10^post7, ret_my_malloc14^0'=ret_my_malloc14^post7, retval^0'=retval^post7, size11^0'=size11^post7, size15^0'=size15^post7, size17^0'=size17^post7, size7^0'=size7^post7, tmp13^0'=tmp13^post7, tmp22^0'=tmp22^post7, tmp9^0'=tmp9^post7, tmp^0'=tmp^post7, tmp___0^0'=tmp___0^post7, tmp___1^0'=tmp___1^post7, (-size17^post7+size17^0 == 0 /\ -retval^post7+retval^0 == 0 /\ -size11^post7+size11^0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post7 == 0 /\ tmp22^0-tmp22^post7 == 0 /\ -tmp___0^post7+tmp___0^0 == 0 /\ -___len21^post7+___len21^0 == 0 /\ -tmp9^post7+tmp9^0 == 0 /\ tmp13^0-tmp13^post7 == 0 /\ -size7^post7+size7^0 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post7 == 0 /\ 2+tmp___1^0 <= 0 /\ size15^0-size15^post7 == 0 /\ tmp^0-tmp^post7 == 0 /\ -tmp___1^post7+tmp___1^0 == 0), cost: 1
   7: l6 -> l3 : ___len21^0'=___len21^post8, ret_my_malloc10^0'=ret_my_malloc10^post8, ret_my_malloc14^0'=ret_my_malloc14^post8, retval^0'=retval^post8, size11^0'=size11^post8, size15^0'=size15^post8, size17^0'=size17^post8, size7^0'=size7^post8, tmp13^0'=tmp13^post8, tmp22^0'=tmp22^post8, tmp9^0'=tmp9^post8, tmp^0'=tmp^post8, tmp___0^0'=tmp___0^post8, tmp___1^0'=tmp___1^post8, (-ret_my_malloc10^post8+ret_my_malloc10^0 == 0 /\ -tmp^post8+tmp^0 == 0 /\ -tmp22^post8+tmp22^0 == 0 /\ size17^0-size17^post8 == 0 /\ -size11^post8+size11^0 == 0 /\ -ret_my_malloc14^post8+ret_my_malloc14^0 == 0 /\ size7^0-size7^post8 == 0 /\ -size15^post8+size15^0 == 0 /\ tmp9^0-tmp9^post8 == 0 /\ retval^0-retval^post8 == 0 /\ tmp___1^0-tmp___1^post8 == 0 /\ tmp13^0-tmp13^post8 == 0 /\ -___len21^post8+___len21^0 == 0 /\ -tmp___0^post8+tmp___0^0 == 0), cost: 1
   8: l7 -> l6 : ___len21^0'=___len21^post9, ret_my_malloc10^0'=ret_my_malloc10^post9, ret_my_malloc14^0'=ret_my_malloc14^post9, retval^0'=retval^post9, size11^0'=size11^post9, size15^0'=size15^post9, size17^0'=size17^post9, size7^0'=size7^post9, tmp13^0'=tmp13^post9, tmp22^0'=tmp22^post9, tmp9^0'=tmp9^post9, tmp^0'=tmp^post9, tmp___0^0'=tmp___0^post9, tmp___1^0'=tmp___1^post9, (tmp___0^0-tmp___0^post9 == 0 /\ -size7^post9+size7^0 == 0 /\ size17^0-size17^post9 == 0 /\ -___len21^post9+___len21^0 == 0 /\ tmp13^0-tmp13^post9 == 0 /\ -tmp___1^post9+tmp___1^0 == 0 /\ size15^0-size15^post9 == 0 /\ -size11^post9+size11^0 == 0 /\ -tmp22^post9+tmp22^0 == 0 /\ tmp^0-tmp^post9 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post9 == 0 /\ tmp9^0-tmp9^post9 == 0 /\ -retval^post9+retval^0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post9 == 0), cost: 1
   9: l8 -> l7 : ___len21^0'=___len21^post10, ret_my_malloc10^0'=ret_my_malloc10^post10, ret_my_malloc14^0'=ret_my_malloc14^post10, retval^0'=retval^post10, size11^0'=size11^post10, size15^0'=size15^post10, size17^0'=size17^post10, size7^0'=size7^post10, tmp13^0'=tmp13^post10, tmp22^0'=tmp22^post10, tmp9^0'=tmp9^post10, tmp^0'=tmp^post10, tmp___0^0'=tmp___0^post10, tmp___1^0'=tmp___1^post10, (ret_my_malloc10^0-ret_my_malloc10^post10 == 0 /\ -size11^post10+size11^0 == 0 /\ -ret_my_malloc14^post10+ret_my_malloc14^0 == 0 /\ -tmp___0^post10+tmp___0^0 == 0 /\ tmp9^0-tmp9^post10 == 0 /\ tmp^0-tmp^post10 == 0 /\ retval^0-retval^post10 == 0 /\ size17^0-size17^post10 == 0 /\ -___len21^post10+___len21^0 == 0 /\ tmp13^0-tmp13^post10 == 0 /\ -tmp22^post10+tmp22^0 == 0 /\ -size7^post10+size7^0 == 0 /\ -size15^post10+size15^0 == 0 /\ -tmp___1^post10+tmp___1^0 == 0), cost: 1
  10: l8 -> l6 : ___len21^0'=___len21^post11, ret_my_malloc10^0'=ret_my_malloc10^post11, ret_my_malloc14^0'=ret_my_malloc14^post11, retval^0'=retval^post11, size11^0'=size11^post11, size15^0'=size15^post11, size17^0'=size17^post11, size7^0'=size7^post11, tmp13^0'=tmp13^post11, tmp22^0'=tmp22^post11, tmp9^0'=tmp9^post11, tmp^0'=tmp^post11, tmp___0^0'=tmp___0^post11, tmp___1^0'=tmp___1^post11, (-ret_my_malloc10^post11+ret_my_malloc10^0 == 0 /\ -size11^post11+size11^0 == 0 /\ -size15^post11+size15^0 == 0 /\ -size7^post11+size7^0 == 0 /\ tmp9^0-tmp9^post11 == 0 /\ -ret_my_malloc14^post11+ret_my_malloc14^0 == 0 /\ -tmp___0^post11+tmp___0^0 == 0 /\ tmp22^0-tmp22^post11 == 0 /\ size17^0-size17^post11 == 0 /\ tmp___1^0-tmp___1^post11 == 0 /\ -tmp^post11+tmp^0 == 0 /\ retval^0-retval^post11 == 0 /\ -___len21^post11+___len21^0 == 0 /\ tmp13^0-tmp13^post11 == 0), cost: 1
  11: l8 -> l7 : ___len21^0'=___len21^post12, ret_my_malloc10^0'=ret_my_malloc10^post12, ret_my_malloc14^0'=ret_my_malloc14^post12, retval^0'=retval^post12, size11^0'=size11^post12, size15^0'=size15^post12, size17^0'=size17^post12, size7^0'=size7^post12, tmp13^0'=tmp13^post12, tmp22^0'=tmp22^post12, tmp9^0'=tmp9^post12, tmp^0'=tmp^post12, tmp___0^0'=tmp___0^post12, tmp___1^0'=tmp___1^post12, (tmp^0-tmp^post12 == 0 /\ size15^0-size15^post12 == 0 /\ -tmp13^post12+tmp13^0 == 0 /\ -tmp22^post12+tmp22^0 == 0 /\ -___len21^post12+___len21^0 == 0 /\ tmp9^0-tmp9^post12 == 0 /\ tmp___1^0-tmp___1^post12 == 0 /\ -size11^post12+size11^0 == 0 /\ -size7^post12+size7^0 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post12 == 0 /\ -retval^post12+retval^0 == 0 /\ -tmp___0^post12+tmp___0^0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post12 == 0 /\ size17^0-size17^post12 == 0), cost: 1
  12: l9 -> l8 : ___len21^0'=___len21^post13, ret_my_malloc10^0'=ret_my_malloc10^post13, ret_my_malloc14^0'=ret_my_malloc14^post13, retval^0'=retval^post13, size11^0'=size11^post13, size15^0'=size15^post13, size17^0'=size17^post13, size7^0'=size7^post13, tmp13^0'=tmp13^post13, tmp22^0'=tmp22^post13, tmp9^0'=tmp9^post13, tmp^0'=tmp^post13, tmp___0^0'=tmp___0^post13, tmp___1^0'=tmp___1^post13, (-ret_my_malloc14^post13+ret_my_malloc14^0 == 0 /\ retval^0-retval^post13 == 0 /\ -tmp___1^post13+tmp___1^0 == 0 /\ -tmp___0^post13+tmp___0^0 == 0 /\ -___len21^post13+___len21^0 == 0 /\ -tmp^post13+tmp^0 == 0 /\ -100+size17^post13 == 0 /\ tmp22^0-tmp22^post13 == 0 /\ -size15^post13+size15^0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post13 == 0 /\ -size7^post13+size7^0 == 0 /\ tmp13^0-tmp13^post13 == 0 /\ -size11^post13+size11^0 == 0 /\ -tmp9^post13+tmp9^0 == 0), cost: 1
  13: l10 -> l3 : ___len21^0'=___len21^post14, ret_my_malloc10^0'=ret_my_malloc10^post14, ret_my_malloc14^0'=ret_my_malloc14^post14, retval^0'=retval^post14, size11^0'=size11^post14, size15^0'=size15^post14, size17^0'=size17^post14, size7^0'=size7^post14, tmp13^0'=tmp13^post14, tmp22^0'=tmp22^post14, tmp9^0'=tmp9^post14, tmp^0'=tmp^post14, tmp___0^0'=tmp___0^post14, tmp___1^0'=tmp___1^post14, (-tmp22^post14+tmp22^0 == 0 /\ size15^0-size15^post14 == 0 /\ retval^0-retval^post14 == 0 /\ tmp___0^0-tmp___0^post14 == 0 /\ -size7^post14+size7^0 == 0 /\ size17^0-size17^post14 == 0 /\ -___len21^post14+___len21^0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post14 == 0 /\ -size11^post14+size11^0 == 0 /\ -tmp___1^post14+tmp___1^0 == 0 /\ tmp13^0-tmp13^post14 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post14 == 0 /\ tmp9^0-tmp9^post14 == 0 /\ tmp^0-tmp^post14 == 0), cost: 1
  14: l11 -> l10 : ___len21^0'=___len21^post15, ret_my_malloc10^0'=ret_my_malloc10^post15, ret_my_malloc14^0'=ret_my_malloc14^post15, retval^0'=retval^post15, size11^0'=size11^post15, size15^0'=size15^post15, size17^0'=size17^post15, size7^0'=size7^post15, tmp13^0'=tmp13^post15, tmp22^0'=tmp22^post15, tmp9^0'=tmp9^post15, tmp^0'=tmp^post15, tmp___0^0'=tmp___0^post15, tmp___1^0'=tmp___1^post15, (tmp^0-tmp^post15 == 0 /\ -tmp22^post15+tmp22^0 == 0 /\ tmp9^0-tmp9^post15 == 0 /\ tmp___1^0-tmp___1^post15 == 0 /\ -tmp13^post15+tmp13^0 == 0 /\ retval^0-retval^post15 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post15 == 0 /\ -size7^post15+size7^0 == 0 /\ -ret_my_malloc14^post15+ret_my_malloc14^0 == 0 /\ -tmp___0^post15+tmp___0^0 == 0 /\ -size11^post15+size11^0 == 0 /\ -size15^post15+size15^0 == 0 /\ size17^0-size17^post15 == 0 /\ -___len21^post15+___len21^0 == 0), cost: 1
  15: l12 -> l11 : ___len21^0'=___len21^post16, ret_my_malloc10^0'=ret_my_malloc10^post16, ret_my_malloc14^0'=ret_my_malloc14^post16, retval^0'=retval^post16, size11^0'=size11^post16, size15^0'=size15^post16, size17^0'=size17^post16, size7^0'=size7^post16, tmp13^0'=tmp13^post16, tmp22^0'=tmp22^post16, tmp9^0'=tmp9^post16, tmp^0'=tmp^post16, tmp___0^0'=tmp___0^post16, tmp___1^0'=tmp___1^post16, (-size7^post16+size7^0 == 0 /\ -___len21^post16+___len21^0 == 0 /\ -ret_my_malloc14^post16+ret_my_malloc14^0 == 0 /\ -size11^post16+size11^0 == 0 /\ -tmp___0^post16+tmp___0^0 == 0 /\ retval^0-retval^post16 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post16 == 0 /\ tmp22^0-tmp22^post16 == 0 /\ size17^0-size17^post16 == 0 /\ -tmp^post16+tmp^0 == 0 /\ tmp___1^0-tmp___1^post16 == 0 /\ size15^0-size15^post16 == 0 /\ tmp13^0-tmp13^post16 == 0 /\ -tmp9^post16+tmp9^0 == 0), cost: 1
  16: l12 -> l10 : ___len21^0'=___len21^post17, ret_my_malloc10^0'=ret_my_malloc10^post17, ret_my_malloc14^0'=ret_my_malloc14^post17, retval^0'=retval^post17, size11^0'=size11^post17, size15^0'=size15^post17, size17^0'=size17^post17, size7^0'=size7^post17, tmp13^0'=tmp13^post17, tmp22^0'=tmp22^post17, tmp9^0'=tmp9^post17, tmp^0'=tmp^post17, tmp___0^0'=tmp___0^post17, tmp___1^0'=tmp___1^post17, (retval^0-retval^post17 == 0 /\ size17^0-size17^post17 == 0 /\ -size15^post17+size15^0 == 0 /\ tmp9^0-tmp9^post17 == 0 /\ -size7^post17+size7^0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post17 == 0 /\ -___len21^post17+___len21^0 == 0 /\ tmp___1^0-tmp___1^post17 == 0 /\ -size11^post17+size11^0 == 0 /\ -tmp___0^post17+tmp___0^0 == 0 /\ -tmp22^post17+tmp22^0 == 0 /\ tmp13^0-tmp13^post17 == 0 /\ -tmp^post17+tmp^0 == 0 /\ -ret_my_malloc14^post17+ret_my_malloc14^0 == 0), cost: 1
  17: l12 -> l11 : ___len21^0'=___len21^post18, ret_my_malloc10^0'=ret_my_malloc10^post18, ret_my_malloc14^0'=ret_my_malloc14^post18, retval^0'=retval^post18, size11^0'=size11^post18, size15^0'=size15^post18, size17^0'=size17^post18, size7^0'=size7^post18, tmp13^0'=tmp13^post18, tmp22^0'=tmp22^post18, tmp9^0'=tmp9^post18, tmp^0'=tmp^post18, tmp___0^0'=tmp___0^post18, tmp___1^0'=tmp___1^post18, (size15^0-size15^post18 == 0 /\ tmp___0^0-tmp___0^post18 == 0 /\ -tmp___1^post18+tmp___1^0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post18 == 0 /\ -tmp22^post18+tmp22^0 == 0 /\ size17^0-size17^post18 == 0 /\ -___len21^post18+___len21^0 == 0 /\ -size7^post18+size7^0 == 0 /\ -size11^post18+size11^0 == 0 /\ tmp^0-tmp^post18 == 0 /\ tmp9^0-tmp9^post18 == 0 /\ tmp13^0-tmp13^post18 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post18 == 0 /\ retval^0-retval^post18 == 0), cost: 1
  18: l13 -> l12 : ___len21^0'=___len21^post19, ret_my_malloc10^0'=ret_my_malloc10^post19, ret_my_malloc14^0'=ret_my_malloc14^post19, retval^0'=retval^post19, size11^0'=size11^post19, size15^0'=size15^post19, size17^0'=size17^post19, size7^0'=size7^post19, tmp13^0'=tmp13^post19, tmp22^0'=tmp22^post19, tmp9^0'=tmp9^post19, tmp^0'=tmp^post19, tmp___0^0'=tmp___0^post19, tmp___1^0'=tmp___1^post19, (tmp^0-tmp^post19 == 0 /\ -100+size15^post19 == 0 /\ -size7^post19+size7^0 == 0 /\ -tmp___0^post19+tmp___0^0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post19 == 0 /\ tmp9^0-tmp9^post19 == 0 /\ -tmp22^post19+tmp22^0 == 0 /\ tmp___1^0-tmp___1^post19 == 0 /\ -size11^post19+size11^0 == 0 /\ size17^0-size17^post19 == 0 /\ -___len21^post19+___len21^0 == 0 /\ retval^0-retval^post19 == 0 /\ tmp13^0-tmp13^post19 == 0 /\ -ret_my_malloc14^post19+ret_my_malloc14^0 == 0), cost: 1
  19: l14 -> l15 : ___len21^0'=___len21^post20, ret_my_malloc10^0'=ret_my_malloc10^post20, ret_my_malloc14^0'=ret_my_malloc14^post20, retval^0'=retval^post20, size11^0'=size11^post20, size15^0'=size15^post20, size17^0'=size17^post20, size7^0'=size7^post20, tmp13^0'=tmp13^post20, tmp22^0'=tmp22^post20, tmp9^0'=tmp9^post20, tmp^0'=tmp^post20, tmp___0^0'=tmp___0^post20, tmp___1^0'=tmp___1^post20, (-size15^post20+size15^0 == 0 /\ -tmp___0^post20+tmp___0^0 == 0 /\ -___len21^post20+___len21^0 == 0 /\ tmp___1^0-tmp___1^post20 == 0 /\ tmp22^0-tmp22^post20 == 0 /\ -tmp9^post20+tmp9^0 == 0 /\ tmp13^0-tmp13^post20 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post20 == 0 /\ -tmp^post20+tmp^0 == 0 /\ size17^0-size17^post20 == 0 /\ -ret_my_malloc14^0+retval^post20 == 0 /\ -size11^post20+size11^0 == 0 /\ -size7^post20+size7^0 == 0 /\ -ret_my_malloc14^post20+ret_my_malloc14^0 == 0), cost: 1
  20: l15 -> l5 : ___len21^0'=___len21^post21, ret_my_malloc10^0'=ret_my_malloc10^post21, ret_my_malloc14^0'=ret_my_malloc14^post21, retval^0'=retval^post21, size11^0'=size11^post21, size15^0'=size15^post21, size17^0'=size17^post21, size7^0'=size7^post21, tmp13^0'=tmp13^post21, tmp22^0'=tmp22^post21, tmp9^0'=tmp9^post21, tmp^0'=tmp^post21, tmp___0^0'=tmp___0^post21, tmp___1^0'=tmp___1^post21, (0 == 0 /\ -size7^post21+size7^0 == 0 /\ size15^0-size15^post21 == 0 /\ size17^0-size17^post21 == 0 /\ tmp9^0-tmp9^post21 == 0 /\ 1-retval^0 <= 0 /\ -1+retval^0 <= 0 /\ tmp13^0-tmp13^post21 == 0 /\ -retval^post21+retval^0 == 0 /\ -size11^post21+size11^0 == 0 /\ -___len21^post21+___len21^0 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post21 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post21 == 0 /\ -tmp___0^post21+tmp___0^0 == 0 /\ -tmp22^post21+tmp22^0 == 0 /\ -tmp^post21+tmp^0 == 0), cost: 1
  21: l15 -> l13 : ___len21^0'=___len21^post22, ret_my_malloc10^0'=ret_my_malloc10^post22, ret_my_malloc14^0'=ret_my_malloc14^post22, retval^0'=retval^post22, size11^0'=size11^post22, size15^0'=size15^post22, size17^0'=size17^post22, size7^0'=size7^post22, tmp13^0'=tmp13^post22, tmp22^0'=tmp22^post22, tmp9^0'=tmp9^post22, tmp^0'=tmp^post22, tmp___0^0'=tmp___0^post22, tmp___1^0'=tmp___1^post22, (retval^0-retval^post22 == 0 /\ 2-retval^0 <= 0 /\ -tmp___1^post22+tmp___1^0 == 0 /\ -tmp___0^post22+tmp___0^0 == 0 /\ -size11^post22+size11^0 == 0 /\ -ret_my_malloc14^post22+ret_my_malloc14^0 == 0 /\ tmp^0-tmp^post22 == 0 /\ -tmp9^post22+tmp9^0 == 0 /\ size15^0-size15^post22 == 0 /\ -___len21^post22+___len21^0 == 0 /\ tmp13^0-tmp13^post22 == 0 /\ tmp22^0-tmp22^post22 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post22 == 0 /\ size17^0-size17^post22 == 0 /\ -size7^post22+size7^0 == 0), cost: 1
  22: l15 -> l13 : ___len21^0'=___len21^post23, ret_my_malloc10^0'=ret_my_malloc10^post23, ret_my_malloc14^0'=ret_my_malloc14^post23, retval^0'=retval^post23, size11^0'=size11^post23, size15^0'=size15^post23, size17^0'=size17^post23, size7^0'=size7^post23, tmp13^0'=tmp13^post23, tmp22^0'=tmp22^post23, tmp9^0'=tmp9^post23, tmp^0'=tmp^post23, tmp___0^0'=tmp___0^post23, tmp___1^0'=tmp___1^post23, (tmp___0^0-tmp___0^post23 == 0 /\ retval^0-retval^post23 == 0 /\ -tmp___1^post23+tmp___1^0 == 0 /\ retval^0 <= 0 /\ tmp^0-tmp^post23 == 0 /\ size17^0-size17^post23 == 0 /\ size15^0-size15^post23 == 0 /\ tmp9^0-tmp9^post23 == 0 /\ -size7^post23+size7^0 == 0 /\ -___len21^post23+___len21^0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post23 == 0 /\ -size11^post23+size11^0 == 0 /\ tmp13^0-tmp13^post23 == 0 /\ -tmp22^post23+tmp22^0 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post23 == 0), cost: 1
  23: l16 -> l14 : ___len21^0'=___len21^post24, ret_my_malloc10^0'=ret_my_malloc10^post24, ret_my_malloc14^0'=ret_my_malloc14^post24, retval^0'=retval^post24, size11^0'=size11^post24, size15^0'=size15^post24, size17^0'=size17^post24, size7^0'=size7^post24, tmp13^0'=tmp13^post24, tmp22^0'=tmp22^post24, tmp9^0'=tmp9^post24, tmp^0'=tmp^post24, tmp___0^0'=tmp___0^post24, tmp___1^0'=tmp___1^post24, (-tmp22^post24+tmp22^0 == 0 /\ tmp9^0-tmp9^post24 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post24 == 0 /\ ret_my_malloc14^post24 == 0 /\ tmp^0-tmp^post24 == 0 /\ -size15^post24+size15^0 == 0 /\ -size7^post24+size7^0 == 0 /\ tmp13^0-tmp13^post24 == 0 /\ tmp___1^0-tmp___1^post24 == 0 /\ -___len21^post24+___len21^0 == 0 /\ retval^0-retval^post24 == 0 /\ -tmp___0^post24+tmp___0^0 == 0 /\ -size11^post24+size11^0 == 0 /\ size17^0-size17^post24 == 0), cost: 1
  24: l16 -> l14 : ___len21^0'=___len21^post25, ret_my_malloc10^0'=ret_my_malloc10^post25, ret_my_malloc14^0'=ret_my_malloc14^post25, retval^0'=retval^post25, size11^0'=size11^post25, size15^0'=size15^post25, size17^0'=size17^post25, size7^0'=size7^post25, tmp13^0'=tmp13^post25, tmp22^0'=tmp22^post25, tmp9^0'=tmp9^post25, tmp^0'=tmp^post25, tmp___0^0'=tmp___0^post25, tmp___1^0'=tmp___1^post25, (-tmp___1^post25+tmp___1^0 == 0 /\ -size7^post25+size7^0 == 0 /\ -tmp___0^post25+tmp___0^0 == 0 /\ tmp^0-tmp^post25 == 0 /\ -1+ret_my_malloc14^post25 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post25 == 0 /\ retval^0-retval^post25 == 0 /\ tmp22^0-tmp22^post25 == 0 /\ size15^0-size15^post25 == 0 /\ -size11^post25+size11^0 == 0 /\ size17^0-size17^post25 == 0 /\ tmp13^0-tmp13^post25 == 0 /\ -___len21^post25+___len21^0 == 0 /\ -tmp9^post25+tmp9^0 == 0), cost: 1
  25: l17 -> l9 : ___len21^0'=___len21^post26, ret_my_malloc10^0'=ret_my_malloc10^post26, ret_my_malloc14^0'=ret_my_malloc14^post26, retval^0'=retval^post26, size11^0'=size11^post26, size15^0'=size15^post26, size17^0'=size17^post26, size7^0'=size7^post26, tmp13^0'=tmp13^post26, tmp22^0'=tmp22^post26, tmp9^0'=tmp9^post26, tmp^0'=tmp^post26, tmp___0^0'=tmp___0^post26, tmp___1^0'=tmp___1^post26, (tmp___1^0-tmp___1^post26 == 0 /\ tmp13^0-tmp13^post26 == 0 /\ 2-retval^0 <= 0 /\ -ret_my_malloc14^post26+ret_my_malloc14^0 == 0 /\ -size15^post26+size15^0 == 0 /\ size17^0-size17^post26 == 0 /\ -tmp___0^post26+tmp___0^0 == 0 /\ retval^0-retval^post26 == 0 /\ -tmp^post26+tmp^0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post26 == 0 /\ -tmp22^post26+tmp22^0 == 0 /\ -___len21^post26+___len21^0 == 0 /\ size11^0-size11^post26 == 0 /\ tmp9^0-tmp9^post26 == 0 /\ size7^0-size7^post26 == 0), cost: 1
  26: l17 -> l9 : ___len21^0'=___len21^post27, ret_my_malloc10^0'=ret_my_malloc10^post27, ret_my_malloc14^0'=ret_my_malloc14^post27, retval^0'=retval^post27, size11^0'=size11^post27, size15^0'=size15^post27, size17^0'=size17^post27, size7^0'=size7^post27, tmp13^0'=tmp13^post27, tmp22^0'=tmp22^post27, tmp9^0'=tmp9^post27, tmp^0'=tmp^post27, tmp___0^0'=tmp___0^post27, tmp___1^0'=tmp___1^post27, (tmp22^0-tmp22^post27 == 0 /\ retval^0 <= 0 /\ ret_my_malloc14^0-ret_my_malloc14^post27 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post27 == 0 /\ retval^0-retval^post27 == 0 /\ tmp13^0-tmp13^post27 == 0 /\ -tmp9^post27+tmp9^0 == 0 /\ -size7^post27+size7^0 == 0 /\ -tmp___1^post27+tmp___1^0 == 0 /\ -tmp___0^post27+tmp___0^0 == 0 /\ tmp^0-tmp^post27 == 0 /\ -___len21^post27+___len21^0 == 0 /\ size17^0-size17^post27 == 0 /\ -size11^post27+size11^0 == 0 /\ size15^0-size15^post27 == 0), cost: 1
  27: l17 -> l16 : ___len21^0'=___len21^post28, ret_my_malloc10^0'=ret_my_malloc10^post28, ret_my_malloc14^0'=ret_my_malloc14^post28, retval^0'=retval^post28, size11^0'=size11^post28, size15^0'=size15^post28, size17^0'=size17^post28, size7^0'=size7^post28, tmp13^0'=tmp13^post28, tmp22^0'=tmp22^post28, tmp9^0'=tmp9^post28, tmp^0'=tmp^post28, tmp___0^0'=tmp___0^post28, tmp___1^0'=tmp___1^post28, (0 == 0 /\ retval^0-retval^post28 == 0 /\ -___len21^post28+___len21^0 == 0 /\ -tmp22^post28+tmp22^0 == 0 /\ -size7^post28+size7^0 == 0 /\ -tmp___1^post28+tmp___1^0 == 0 /\ size15^0-size15^post28 == 0 /\ -ret_my_malloc14^post28+ret_my_malloc14^0 == 0 /\ -100+size11^post28 == 0 /\ 1-retval^0 <= 0 /\ -1+retval^0 <= 0 /\ ret_my_malloc10^0-ret_my_malloc10^post28 == 0 /\ size17^0-size17^post28 == 0 /\ tmp9^0-tmp9^post28 == 0 /\ tmp^0-tmp^post28 == 0 /\ -tmp___0^post28+tmp___0^0 == 0), cost: 1
  31: l19 -> l0 : ___len21^0'=___len21^post30, ret_my_malloc10^0'=ret_my_malloc10^post30, ret_my_malloc14^0'=ret_my_malloc14^post30, retval^0'=retval^post30, size11^0'=size11^post30, size15^0'=size15^post30, size17^0'=size17^post30, size7^0'=size7^post30, tmp13^0'=tmp13^post30, tmp22^0'=tmp22^post30, tmp9^0'=tmp9^post30, tmp^0'=tmp^post30, tmp___0^0'=tmp___0^post30, tmp___1^0'=tmp___1^post30, (0 == 0 /\ size17^0-size17^post31 == 0 /\ size15^post31-size15^post30 == 0 /\ -ret_my_malloc10^post31+ret_my_malloc10^0 == 0 /\ -tmp___1^post30+tmp___1^post31 == 0 /\ tmp13^0-tmp13^post31 == 0 /\ -tmp22^post31+tmp22^0 == 0 /\ -tmp^post31+tmp^0 == 0 /\ -retval^post30+retval^post31 == 0 /\ tmp^post31-tmp^post30 == 0 /\ tmp22^post31-tmp22^post30 == 0 /\ size7^0-size7^post31 == 0 /\ ret_my_malloc14^post31-ret_my_malloc14^post30 == 0 /\ -100+size7^post30 == 0 /\ -tmp___0^post30+tmp___0^post31 == 0 /\ -size11^post30+size11^post31 == 0 /\ -ret_my_malloc14^post31+ret_my_malloc14^0 == 0 /\ tmp___1^0-tmp___1^post31 == 0 /\ tmp13^post31-tmp13^post30 == 0 /\ -tmp___0^post31+tmp___0^0 == 0 /\ tmp9^0-tmp9^post31 == 0 /\ -___len21^post30+___len21^post31 == 0 /\ size11^0-size11^post31 == 0 /\ -___len21^post31+___len21^0 == 0 /\ retval^0-retval^post31 == 0 /\ ret_my_malloc10^post31-ret_my_malloc10^post30 == 0 /\ size17^post31-size17^post30 == 0 /\ -size15^post31+size15^0 == 0), cost: 1

	Eliminating location l18 by chaining:

	Applied chaining

	First rule:
	l19 -> l18 : ___len21^0'=___len21^post31, ret_my_malloc10^0'=ret_my_malloc10^post31, ret_my_malloc14^0'=ret_my_malloc14^post31, retval^0'=retval^post31, size11^0'=size11^post31, size15^0'=size15^post31, size17^0'=size17^post31, size7^0'=size7^post31, tmp13^0'=tmp13^post31, tmp22^0'=tmp22^post31, tmp9^0'=tmp9^post31, tmp^0'=tmp^post31, tmp___0^0'=tmp___0^post31, tmp___1^0'=tmp___1^post31, (size17^0-size17^post31 == 0 /\ -ret_my_malloc10^post31+ret_my_malloc10^0 == 0 /\ tmp13^0-tmp13^post31 == 0 /\ -tmp22^post31+tmp22^0 == 0 /\ -tmp^post31+tmp^0 == 0 /\ size7^0-size7^post31 == 0 /\ -ret_my_malloc14^post31+ret_my_malloc14^0 == 0 /\ tmp___1^0-tmp___1^post31 == 0 /\ -tmp___0^post31+tmp___0^0 == 0 /\ tmp9^0-tmp9^post31 == 0 /\ size11^0-size11^post31 == 0 /\ -___len21^post31+___len21^0 == 0 /\ retval^0-retval^post31 == 0 /\ -size15^post31+size15^0 == 0), cost: 1
	Second rule:
	l18 -> l0 : ___len21^0'=___len21^post30, ret_my_malloc10^0'=ret_my_malloc10^post30, ret_my_malloc14^0'=ret_my_malloc14^post30, retval^0'=retval^post30, size11^0'=size11^post30, size15^0'=size15^post30, size17^0'=size17^post30, size7^0'=size7^post30, tmp13^0'=tmp13^post30, tmp22^0'=tmp22^post30, tmp9^0'=tmp9^post30, tmp^0'=tmp^post30, tmp___0^0'=tmp___0^post30, tmp___1^0'=tmp___1^post30, (0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post30 == 0 /\ tmp22^0-tmp22^post30 == 0 /\ -retval^post30+retval^0 == 0 /\ tmp13^0-tmp13^post30 == 0 /\ tmp^0-tmp^post30 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post30 == 0 /\ -tmp___0^post30+tmp___0^0 == 0 /\ -100+size7^post30 == 0 /\ -___len21^post30+___len21^0 == 0 /\ size17^0-size17^post30 == 0 /\ -size11^post30+size11^0 == 0 /\ size15^0-size15^post30 == 0 /\ -tmp___1^post30+tmp___1^0 == 0), cost: 1
	New rule:
	l19 -> l0 : ___len21^0'=___len21^post30, ret_my_malloc10^0'=ret_my_malloc10^post30, ret_my_malloc14^0'=ret_my_malloc14^post30, retval^0'=retval^post30, size11^0'=size11^post30, size15^0'=size15^post30, size17^0'=size17^post30, size7^0'=size7^post30, tmp13^0'=tmp13^post30, tmp22^0'=tmp22^post30, tmp9^0'=tmp9^post30, tmp^0'=tmp^post30, tmp___0^0'=tmp___0^post30, tmp___1^0'=tmp___1^post30, (0 == 0 /\ size17^0-size17^post31 == 0 /\ size15^post31-size15^post30 == 0 /\ -ret_my_malloc10^post31+ret_my_malloc10^0 == 0 /\ -tmp___1^post30+tmp___1^post31 == 0 /\ tmp13^0-tmp13^post31 == 0 /\ -tmp22^post31+tmp22^0 == 0 /\ -tmp^post31+tmp^0 == 0 /\ -retval^post30+retval^post31 == 0 /\ tmp^post31-tmp^post30 == 0 /\ tmp22^post31-tmp22^post30 == 0 /\ size7^0-size7^post31 == 0 /\ ret_my_malloc14^post31-ret_my_malloc14^post30 == 0 /\ -100+size7^post30 == 0 /\ -tmp___0^post30+tmp___0^post31 == 0 /\ -size11^post30+size11^post31 == 0 /\ -ret_my_malloc14^post31+ret_my_malloc14^0 == 0 /\ tmp___1^0-tmp___1^post31 == 0 /\ tmp13^post31-tmp13^post30 == 0 /\ -tmp___0^post31+tmp___0^0 == 0 /\ tmp9^0-tmp9^post31 == 0 /\ -___len21^post30+___len21^post31 == 0 /\ size11^0-size11^post31 == 0 /\ -___len21^post31+___len21^0 == 0 /\ retval^0-retval^post31 == 0 /\ ret_my_malloc10^post31-ret_my_malloc10^post30 == 0 /\ size17^post31-size17^post30 == 0 /\ -size15^post31+size15^0 == 0), cost: 1
	
	Applied deletion

	Removed the following rules: 29 30

Simplified Transitions

Start location: l19
Program variables: ___len21^0 ret_my_malloc10^0 ret_my_malloc14^0 retval^0 size11^0 size15^0 size17^0 size7^0 tmp13^0 tmp22^0 tmp9^0 tmp^0 tmp___0^0 tmp___1^0
  32: l0 -> l1 : ret_my_malloc10^0'=0, T, cost: 1
  33: l0 -> l1 : ret_my_malloc10^0'=1, T, cost: 1
  60: l1 -> l17 : retval^0'=ret_my_malloc10^0, tmp^0'=ret_my_malloc10^0, T, cost: 1
  34: l2 -> l3 : T, cost: 1
  35: l4 -> l2 : tmp___0^0'=tmp___0^post4, T, cost: 1
  36: l5 -> l2 : ___len21^0'=100, tmp22^0'=tmp22^post5, (1+tmp___1^0 <= 0 /\ 1+tmp___1^0 == 0 /\ -1-tmp___1^0 <= 0), cost: 1
  37: l5 -> l4 : -tmp___1^0 <= 0, cost: 1
  38: l5 -> l4 : 2+tmp___1^0 <= 0, cost: 1
  39: l6 -> l3 : T, cost: 1
  40: l7 -> l6 : T, cost: 1
  41: l8 -> l7 : T, cost: 1
  42: l8 -> l6 : T, cost: 1
  43: l8 -> l7 : T, cost: 1
  44: l9 -> l8 : size17^0'=100, T, cost: 1
  45: l10 -> l3 : T, cost: 1
  46: l11 -> l10 : T, cost: 1
  47: l12 -> l11 : T, cost: 1
  48: l12 -> l10 : T, cost: 1
  49: l12 -> l11 : T, cost: 1
  50: l13 -> l12 : size15^0'=100, T, cost: 1
  51: l14 -> l15 : retval^0'=ret_my_malloc14^0, T, cost: 1
  52: l15 -> l5 : tmp___1^0'=tmp___1^post21, (1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0), cost: 1
  53: l15 -> l13 : 2-retval^0 <= 0, cost: 1
  54: l15 -> l13 : retval^0 <= 0, cost: 1
  55: l16 -> l14 : ret_my_malloc14^0'=0, T, cost: 1
  56: l16 -> l14 : ret_my_malloc14^0'=1, T, cost: 1
  57: l17 -> l9 : 2-retval^0 <= 0, cost: 1
  58: l17 -> l9 : retval^0 <= 0, cost: 1
  59: l17 -> l16 : size11^0'=100, tmp13^0'=tmp13^post28, (1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0), cost: 1
  61: l19 -> l0 : size7^0'=100, tmp9^0'=tmp9^post30, T, cost: 1

	Propagated Equalities

	Original rule:
	l0 -> l1 : ___len21^0'=___len21^post1, ret_my_malloc10^0'=ret_my_malloc10^post1, ret_my_malloc14^0'=ret_my_malloc14^post1, retval^0'=retval^post1, size11^0'=size11^post1, size15^0'=size15^post1, size17^0'=size17^post1, size7^0'=size7^post1, tmp13^0'=tmp13^post1, tmp22^0'=tmp22^post1, tmp9^0'=tmp9^post1, tmp^0'=tmp^post1, tmp___0^0'=tmp___0^post1, tmp___1^0'=tmp___1^post1, (tmp9^0-tmp9^post1 == 0 /\ -ret_my_malloc14^post1+ret_my_malloc14^0 == 0 /\ tmp___1^0-tmp___1^post1 == 0 /\ -___len21^post1+___len21^0 == 0 /\ tmp13^0-tmp13^post1 == 0 /\ -size15^post1+size15^0 == 0 /\ size11^0-size11^post1 == 0 /\ -size7^post1+size7^0 == 0 /\ retval^0-retval^post1 == 0 /\ -tmp___0^post1+tmp___0^0 == 0 /\ -tmp22^post1+tmp22^0 == 0 /\ -tmp^post1+tmp^0 == 0 /\ size17^0-size17^post1 == 0 /\ ret_my_malloc10^post1 == 0), cost: 1
	New rule:
	l0 -> l1 : ___len21^0'=___len21^0, ret_my_malloc10^0'=0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1
	
		propagated equality tmp9^post1 = tmp9^0
		
		propagated equality ret_my_malloc14^post1 = ret_my_malloc14^0
		
		propagated equality tmp___1^post1 = tmp___1^0
		
		propagated equality ___len21^post1 = ___len21^0
		
		propagated equality tmp13^post1 = tmp13^0
		
		propagated equality size15^post1 = size15^0
		
		propagated equality size11^post1 = size11^0
		
		propagated equality size7^post1 = size7^0
		
		propagated equality retval^post1 = retval^0
		
		propagated equality tmp___0^post1 = tmp___0^0
		
		propagated equality tmp22^post1 = tmp22^0
		
		propagated equality tmp^post1 = tmp^0
		
		propagated equality size17^post1 = size17^0
		
		propagated equality ret_my_malloc10^post1 = 0
		
	Simplified Guard

	Original rule:
	l0 -> l1 : ___len21^0'=___len21^0, ret_my_malloc10^0'=0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1
	New rule:
	l0 -> l1 : ___len21^0'=___len21^0, ret_my_malloc10^0'=0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l0 -> l1 : ___len21^0'=___len21^0, ret_my_malloc10^0'=0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, T, cost: 1
	New rule:
	l0 -> l1 : ret_my_malloc10^0'=0, T, cost: 1
	
	Propagated Equalities

	Original rule:
	l0 -> l1 : ___len21^0'=___len21^post2, ret_my_malloc10^0'=ret_my_malloc10^post2, ret_my_malloc14^0'=ret_my_malloc14^post2, retval^0'=retval^post2, size11^0'=size11^post2, size15^0'=size15^post2, size17^0'=size17^post2, size7^0'=size7^post2, tmp13^0'=tmp13^post2, tmp22^0'=tmp22^post2, tmp9^0'=tmp9^post2, tmp^0'=tmp^post2, tmp___0^0'=tmp___0^post2, tmp___1^0'=tmp___1^post2, (-___len21^post2+___len21^0 == 0 /\ -tmp9^post2+tmp9^0 == 0 /\ tmp^0-tmp^post2 == 0 /\ retval^0-retval^post2 == 0 /\ tmp22^0-tmp22^post2 == 0 /\ -size7^post2+size7^0 == 0 /\ tmp13^0-tmp13^post2 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post2 == 0 /\ -tmp___1^post2+tmp___1^0 == 0 /\ -1+ret_my_malloc10^post2 == 0 /\ size15^0-size15^post2 == 0 /\ -size11^post2+size11^0 == 0 /\ size17^0-size17^post2 == 0 /\ -tmp___0^post2+tmp___0^0 == 0), cost: 1
	New rule:
	l0 -> l1 : ___len21^0'=___len21^0, ret_my_malloc10^0'=1, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1
	
		propagated equality ___len21^post2 = ___len21^0
		
		propagated equality tmp9^post2 = tmp9^0
		
		propagated equality tmp^post2 = tmp^0
		
		propagated equality retval^post2 = retval^0
		
		propagated equality tmp22^post2 = tmp22^0
		
		propagated equality size7^post2 = size7^0
		
		propagated equality tmp13^post2 = tmp13^0
		
		propagated equality ret_my_malloc14^post2 = ret_my_malloc14^0
		
		propagated equality tmp___1^post2 = tmp___1^0
		
		propagated equality ret_my_malloc10^post2 = 1
		
		propagated equality size15^post2 = size15^0
		
		propagated equality size11^post2 = size11^0
		
		propagated equality size17^post2 = size17^0
		
		propagated equality tmp___0^post2 = tmp___0^0
		
	Simplified Guard

	Original rule:
	l0 -> l1 : ___len21^0'=___len21^0, ret_my_malloc10^0'=1, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1
	New rule:
	l0 -> l1 : ___len21^0'=___len21^0, ret_my_malloc10^0'=1, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l0 -> l1 : ___len21^0'=___len21^0, ret_my_malloc10^0'=1, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, T, cost: 1
	New rule:
	l0 -> l1 : ret_my_malloc10^0'=1, T, cost: 1
	
	Propagated Equalities

	Original rule:
	l2 -> l3 : ___len21^0'=___len21^post3, ret_my_malloc10^0'=ret_my_malloc10^post3, ret_my_malloc14^0'=ret_my_malloc14^post3, retval^0'=retval^post3, size11^0'=size11^post3, size15^0'=size15^post3, size17^0'=size17^post3, size7^0'=size7^post3, tmp13^0'=tmp13^post3, tmp22^0'=tmp22^post3, tmp9^0'=tmp9^post3, tmp^0'=tmp^post3, tmp___0^0'=tmp___0^post3, tmp___1^0'=tmp___1^post3, (size17^0-size17^post3 == 0 /\ tmp___1^0-tmp___1^post3 == 0 /\ -ret_my_malloc14^post3+ret_my_malloc14^0 == 0 /\ retval^0-retval^post3 == 0 /\ -tmp___0^post3+tmp___0^0 == 0 /\ tmp13^0-tmp13^post3 == 0 /\ -___len21^post3+___len21^0 == 0 /\ -tmp22^post3+tmp22^0 == 0 /\ -tmp^post3+tmp^0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post3 == 0 /\ size7^0-size7^post3 == 0 /\ tmp9^0-tmp9^post3 == 0 /\ -size15^post3+size15^0 == 0 /\ size11^0-size11^post3 == 0), cost: 1
	New rule:
	l2 -> l3 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1
	
		propagated equality size17^post3 = size17^0
		
		propagated equality tmp___1^post3 = tmp___1^0
		
		propagated equality ret_my_malloc14^post3 = ret_my_malloc14^0
		
		propagated equality retval^post3 = retval^0
		
		propagated equality tmp___0^post3 = tmp___0^0
		
		propagated equality tmp13^post3 = tmp13^0
		
		propagated equality ___len21^post3 = ___len21^0
		
		propagated equality tmp22^post3 = tmp22^0
		
		propagated equality tmp^post3 = tmp^0
		
		propagated equality ret_my_malloc10^post3 = ret_my_malloc10^0
		
		propagated equality size7^post3 = size7^0
		
		propagated equality tmp9^post3 = tmp9^0
		
		propagated equality size15^post3 = size15^0
		
		propagated equality size11^post3 = size11^0
		
	Simplified Guard

	Original rule:
	l2 -> l3 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1
	New rule:
	l2 -> l3 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l2 -> l3 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, T, cost: 1
	New rule:
	l2 -> l3 : T, cost: 1
	
	Propagated Equalities

	Original rule:
	l4 -> l2 : ___len21^0'=___len21^post4, ret_my_malloc10^0'=ret_my_malloc10^post4, ret_my_malloc14^0'=ret_my_malloc14^post4, retval^0'=retval^post4, size11^0'=size11^post4, size15^0'=size15^post4, size17^0'=size17^post4, size7^0'=size7^post4, tmp13^0'=tmp13^post4, tmp22^0'=tmp22^post4, tmp9^0'=tmp9^post4, tmp^0'=tmp^post4, tmp___0^0'=tmp___0^post4, tmp___1^0'=tmp___1^post4, (0 == 0 /\ tmp13^0-tmp13^post4 == 0 /\ -size17^post4+size17^0 == 0 /\ tmp22^0-tmp22^post4 == 0 /\ retval^0-retval^post4 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post4 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post4 == 0 /\ -tmp___1^post4+tmp___1^0 == 0 /\ size15^0-size15^post4 == 0 /\ -size11^post4+size11^0 == 0 /\ -tmp9^post4+tmp9^0 == 0 /\ tmp^0-tmp^post4 == 0 /\ -___len21^post4+___len21^0 == 0 /\ -size7^post4+size7^0 == 0), cost: 1
	New rule:
	l4 -> l2 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^post4, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1
	
		propagated equality tmp13^post4 = tmp13^0
		
		propagated equality size17^post4 = size17^0
		
		propagated equality tmp22^post4 = tmp22^0
		
		propagated equality retval^post4 = retval^0
		
		propagated equality ret_my_malloc14^post4 = ret_my_malloc14^0
		
		propagated equality ret_my_malloc10^post4 = ret_my_malloc10^0
		
		propagated equality tmp___1^post4 = tmp___1^0
		
		propagated equality size15^post4 = size15^0
		
		propagated equality size11^post4 = size11^0
		
		propagated equality tmp9^post4 = tmp9^0
		
		propagated equality tmp^post4 = tmp^0
		
		propagated equality ___len21^post4 = ___len21^0
		
		propagated equality size7^post4 = size7^0
		
	Simplified Guard

	Original rule:
	l4 -> l2 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^post4, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1
	New rule:
	l4 -> l2 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^post4, tmp___1^0'=tmp___1^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l4 -> l2 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^post4, tmp___1^0'=tmp___1^0, T, cost: 1
	New rule:
	l4 -> l2 : tmp___0^0'=tmp___0^post4, T, cost: 1
	
	made implied equalities explicit

	Original rule:
	l5 -> l2 : ___len21^0'=___len21^post5, ret_my_malloc10^0'=ret_my_malloc10^post5, ret_my_malloc14^0'=ret_my_malloc14^post5, retval^0'=retval^post5, size11^0'=size11^post5, size15^0'=size15^post5, size17^0'=size17^post5, size7^0'=size7^post5, tmp13^0'=tmp13^post5, tmp22^0'=tmp22^post5, tmp9^0'=tmp9^post5, tmp^0'=tmp^post5, tmp___0^0'=tmp___0^post5, tmp___1^0'=tmp___1^post5, (0 == 0 /\ -size7^post5+size7^0 == 0 /\ tmp^0-tmp^post5 == 0 /\ -size11^post5+size11^0 == 0 /\ retval^0-retval^post5 == 0 /\ -ret_my_malloc14^post5+ret_my_malloc14^0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post5 == 0 /\ tmp9^0-tmp9^post5 == 0 /\ size17^0-size17^post5 == 0 /\ -tmp___1^post5+tmp___1^0 == 0 /\ -tmp___0^post5+tmp___0^0 == 0 /\ 1+tmp___1^0 <= 0 /\ -1-tmp___1^0 <= 0 /\ -size15^post5+size15^0 == 0 /\ -100+___len21^post5 == 0 /\ tmp13^0-tmp13^post5 == 0), cost: 1
	New rule:
	l5 -> l2 : ___len21^0'=___len21^post5, ret_my_malloc10^0'=ret_my_malloc10^post5, ret_my_malloc14^0'=ret_my_malloc14^post5, retval^0'=retval^post5, size11^0'=size11^post5, size15^0'=size15^post5, size17^0'=size17^post5, size7^0'=size7^post5, tmp13^0'=tmp13^post5, tmp22^0'=tmp22^post5, tmp9^0'=tmp9^post5, tmp^0'=tmp^post5, tmp___0^0'=tmp___0^post5, tmp___1^0'=tmp___1^post5, (0 == 0 /\ -size7^post5+size7^0 == 0 /\ tmp^0-tmp^post5 == 0 /\ -size11^post5+size11^0 == 0 /\ retval^0-retval^post5 == 0 /\ -ret_my_malloc14^post5+ret_my_malloc14^0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post5 == 0 /\ tmp9^0-tmp9^post5 == 0 /\ size17^0-size17^post5 == 0 /\ -tmp___1^post5+tmp___1^0 == 0 /\ -tmp___0^post5+tmp___0^0 == 0 /\ 1+tmp___1^0 <= 0 /\ 1+tmp___1^0 == 0 /\ -1-tmp___1^0 <= 0 /\ -size15^post5+size15^0 == 0 /\ -100+___len21^post5 == 0 /\ tmp13^0-tmp13^post5 == 0), cost: 1
	
	Propagated Equalities

	Original rule:
	l5 -> l2 : ___len21^0'=___len21^post5, ret_my_malloc10^0'=ret_my_malloc10^post5, ret_my_malloc14^0'=ret_my_malloc14^post5, retval^0'=retval^post5, size11^0'=size11^post5, size15^0'=size15^post5, size17^0'=size17^post5, size7^0'=size7^post5, tmp13^0'=tmp13^post5, tmp22^0'=tmp22^post5, tmp9^0'=tmp9^post5, tmp^0'=tmp^post5, tmp___0^0'=tmp___0^post5, tmp___1^0'=tmp___1^post5, (0 == 0 /\ -size7^post5+size7^0 == 0 /\ tmp^0-tmp^post5 == 0 /\ -size11^post5+size11^0 == 0 /\ retval^0-retval^post5 == 0 /\ -ret_my_malloc14^post5+ret_my_malloc14^0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post5 == 0 /\ tmp9^0-tmp9^post5 == 0 /\ size17^0-size17^post5 == 0 /\ -tmp___1^post5+tmp___1^0 == 0 /\ -tmp___0^post5+tmp___0^0 == 0 /\ 1+tmp___1^0 <= 0 /\ 1+tmp___1^0 == 0 /\ -1-tmp___1^0 <= 0 /\ -size15^post5+size15^0 == 0 /\ -100+___len21^post5 == 0 /\ tmp13^0-tmp13^post5 == 0), cost: 1
	New rule:
	l5 -> l2 : ___len21^0'=100, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^post5, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, (0 == 0 /\ 1+tmp___1^0 <= 0 /\ 1+tmp___1^0 == 0 /\ -1-tmp___1^0 <= 0), cost: 1
	
		propagated equality size7^post5 = size7^0
		
		propagated equality tmp^post5 = tmp^0
		
		propagated equality size11^post5 = size11^0
		
		propagated equality retval^post5 = retval^0
		
		propagated equality ret_my_malloc14^post5 = ret_my_malloc14^0
		
		propagated equality ret_my_malloc10^post5 = ret_my_malloc10^0
		
		propagated equality tmp9^post5 = tmp9^0
		
		propagated equality size17^post5 = size17^0
		
		propagated equality tmp___1^post5 = tmp___1^0
		
		propagated equality tmp___0^post5 = tmp___0^0
		
		propagated equality size15^post5 = size15^0
		
		propagated equality ___len21^post5 = 100
		
		propagated equality tmp13^post5 = tmp13^0
		
	Simplified Guard

	Original rule:
	l5 -> l2 : ___len21^0'=100, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^post5, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, (0 == 0 /\ 1+tmp___1^0 <= 0 /\ 1+tmp___1^0 == 0 /\ -1-tmp___1^0 <= 0), cost: 1
	New rule:
	l5 -> l2 : ___len21^0'=100, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^post5, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, (1+tmp___1^0 <= 0 /\ 1+tmp___1^0 == 0 /\ -1-tmp___1^0 <= 0), cost: 1
	
	made implied equalities explicit

	Original rule:
	l5 -> l2 : ___len21^0'=100, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^post5, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, (1+tmp___1^0 <= 0 /\ 1+tmp___1^0 == 0 /\ -1-tmp___1^0 <= 0), cost: 1
	New rule:
	l5 -> l2 : ___len21^0'=100, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^post5, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, (1+tmp___1^0 <= 0 /\ 1+tmp___1^0 == 0 /\ -1-tmp___1^0 <= 0), cost: 1
	
	Removed Trivial Updates

	Original rule:
	l5 -> l2 : ___len21^0'=100, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^post5, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, (1+tmp___1^0 <= 0 /\ 1+tmp___1^0 == 0 /\ -1-tmp___1^0 <= 0), cost: 1
	New rule:
	l5 -> l2 : ___len21^0'=100, tmp22^0'=tmp22^post5, (1+tmp___1^0 <= 0 /\ 1+tmp___1^0 == 0 /\ -1-tmp___1^0 <= 0), cost: 1
	
	Propagated Equalities

	Original rule:
	l5 -> l4 : ___len21^0'=___len21^post6, ret_my_malloc10^0'=ret_my_malloc10^post6, ret_my_malloc14^0'=ret_my_malloc14^post6, retval^0'=retval^post6, size11^0'=size11^post6, size15^0'=size15^post6, size17^0'=size17^post6, size7^0'=size7^post6, tmp13^0'=tmp13^post6, tmp22^0'=tmp22^post6, tmp9^0'=tmp9^post6, tmp^0'=tmp^post6, tmp___0^0'=tmp___0^post6, tmp___1^0'=tmp___1^post6, (-___len21^post6+___len21^0 == 0 /\ -tmp___1^0 <= 0 /\ size17^0-size17^post6 == 0 /\ -tmp^post6+tmp^0 == 0 /\ tmp13^0-tmp13^post6 == 0 /\ -ret_my_malloc14^post6+ret_my_malloc14^0 == 0 /\ -ret_my_malloc10^post6+ret_my_malloc10^0 == 0 /\ -tmp22^post6+tmp22^0 == 0 /\ tmp9^0-tmp9^post6 == 0 /\ tmp___1^0-tmp___1^post6 == 0 /\ -size15^post6+size15^0 == 0 /\ size11^0-size11^post6 == 0 /\ size7^0-size7^post6 == 0 /\ retval^0-retval^post6 == 0 /\ -tmp___0^post6+tmp___0^0 == 0), cost: 1
	New rule:
	l5 -> l4 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, (0 == 0 /\ -tmp___1^0 <= 0), cost: 1
	
		propagated equality ___len21^post6 = ___len21^0
		
		propagated equality size17^post6 = size17^0
		
		propagated equality tmp^post6 = tmp^0
		
		propagated equality tmp13^post6 = tmp13^0
		
		propagated equality ret_my_malloc14^post6 = ret_my_malloc14^0
		
		propagated equality ret_my_malloc10^post6 = ret_my_malloc10^0
		
		propagated equality tmp22^post6 = tmp22^0
		
		propagated equality tmp9^post6 = tmp9^0
		
		propagated equality tmp___1^post6 = tmp___1^0
		
		propagated equality size15^post6 = size15^0
		
		propagated equality size11^post6 = size11^0
		
		propagated equality size7^post6 = size7^0
		
		propagated equality retval^post6 = retval^0
		
		propagated equality tmp___0^post6 = tmp___0^0
		
	Simplified Guard

	Original rule:
	l5 -> l4 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, (0 == 0 /\ -tmp___1^0 <= 0), cost: 1
	New rule:
	l5 -> l4 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, -tmp___1^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l5 -> l4 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, -tmp___1^0 <= 0, cost: 1
	New rule:
	l5 -> l4 : -tmp___1^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l5 -> l4 : ___len21^0'=___len21^post7, ret_my_malloc10^0'=ret_my_malloc10^post7, ret_my_malloc14^0'=ret_my_malloc14^post7, retval^0'=retval^post7, size11^0'=size11^post7, size15^0'=size15^post7, size17^0'=size17^post7, size7^0'=size7^post7, tmp13^0'=tmp13^post7, tmp22^0'=tmp22^post7, tmp9^0'=tmp9^post7, tmp^0'=tmp^post7, tmp___0^0'=tmp___0^post7, tmp___1^0'=tmp___1^post7, (-size17^post7+size17^0 == 0 /\ -retval^post7+retval^0 == 0 /\ -size11^post7+size11^0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post7 == 0 /\ tmp22^0-tmp22^post7 == 0 /\ -tmp___0^post7+tmp___0^0 == 0 /\ -___len21^post7+___len21^0 == 0 /\ -tmp9^post7+tmp9^0 == 0 /\ tmp13^0-tmp13^post7 == 0 /\ -size7^post7+size7^0 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post7 == 0 /\ 2+tmp___1^0 <= 0 /\ size15^0-size15^post7 == 0 /\ tmp^0-tmp^post7 == 0 /\ -tmp___1^post7+tmp___1^0 == 0), cost: 1
	New rule:
	l5 -> l4 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, (0 == 0 /\ 2+tmp___1^0 <= 0), cost: 1
	
		propagated equality size17^post7 = size17^0
		
		propagated equality retval^post7 = retval^0
		
		propagated equality size11^post7 = size11^0
		
		propagated equality ret_my_malloc10^post7 = ret_my_malloc10^0
		
		propagated equality tmp22^post7 = tmp22^0
		
		propagated equality tmp___0^post7 = tmp___0^0
		
		propagated equality ___len21^post7 = ___len21^0
		
		propagated equality tmp9^post7 = tmp9^0
		
		propagated equality tmp13^post7 = tmp13^0
		
		propagated equality size7^post7 = size7^0
		
		propagated equality ret_my_malloc14^post7 = ret_my_malloc14^0
		
		propagated equality size15^post7 = size15^0
		
		propagated equality tmp^post7 = tmp^0
		
		propagated equality tmp___1^post7 = tmp___1^0
		
	Simplified Guard

	Original rule:
	l5 -> l4 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, (0 == 0 /\ 2+tmp___1^0 <= 0), cost: 1
	New rule:
	l5 -> l4 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 2+tmp___1^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l5 -> l4 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 2+tmp___1^0 <= 0, cost: 1
	New rule:
	l5 -> l4 : 2+tmp___1^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l6 -> l3 : ___len21^0'=___len21^post8, ret_my_malloc10^0'=ret_my_malloc10^post8, ret_my_malloc14^0'=ret_my_malloc14^post8, retval^0'=retval^post8, size11^0'=size11^post8, size15^0'=size15^post8, size17^0'=size17^post8, size7^0'=size7^post8, tmp13^0'=tmp13^post8, tmp22^0'=tmp22^post8, tmp9^0'=tmp9^post8, tmp^0'=tmp^post8, tmp___0^0'=tmp___0^post8, tmp___1^0'=tmp___1^post8, (-ret_my_malloc10^post8+ret_my_malloc10^0 == 0 /\ -tmp^post8+tmp^0 == 0 /\ -tmp22^post8+tmp22^0 == 0 /\ size17^0-size17^post8 == 0 /\ -size11^post8+size11^0 == 0 /\ -ret_my_malloc14^post8+ret_my_malloc14^0 == 0 /\ size7^0-size7^post8 == 0 /\ -size15^post8+size15^0 == 0 /\ tmp9^0-tmp9^post8 == 0 /\ retval^0-retval^post8 == 0 /\ tmp___1^0-tmp___1^post8 == 0 /\ tmp13^0-tmp13^post8 == 0 /\ -___len21^post8+___len21^0 == 0 /\ -tmp___0^post8+tmp___0^0 == 0), cost: 1
	New rule:
	l6 -> l3 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1
	
		propagated equality ret_my_malloc10^post8 = ret_my_malloc10^0
		
		propagated equality tmp^post8 = tmp^0
		
		propagated equality tmp22^post8 = tmp22^0
		
		propagated equality size17^post8 = size17^0
		
		propagated equality size11^post8 = size11^0
		
		propagated equality ret_my_malloc14^post8 = ret_my_malloc14^0
		
		propagated equality size7^post8 = size7^0
		
		propagated equality size15^post8 = size15^0
		
		propagated equality tmp9^post8 = tmp9^0
		
		propagated equality retval^post8 = retval^0
		
		propagated equality tmp___1^post8 = tmp___1^0
		
		propagated equality tmp13^post8 = tmp13^0
		
		propagated equality ___len21^post8 = ___len21^0
		
		propagated equality tmp___0^post8 = tmp___0^0
		
	Simplified Guard

	Original rule:
	l6 -> l3 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1
	New rule:
	l6 -> l3 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l6 -> l3 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, T, cost: 1
	New rule:
	l6 -> l3 : T, cost: 1
	
	Propagated Equalities

	Original rule:
	l7 -> l6 : ___len21^0'=___len21^post9, ret_my_malloc10^0'=ret_my_malloc10^post9, ret_my_malloc14^0'=ret_my_malloc14^post9, retval^0'=retval^post9, size11^0'=size11^post9, size15^0'=size15^post9, size17^0'=size17^post9, size7^0'=size7^post9, tmp13^0'=tmp13^post9, tmp22^0'=tmp22^post9, tmp9^0'=tmp9^post9, tmp^0'=tmp^post9, tmp___0^0'=tmp___0^post9, tmp___1^0'=tmp___1^post9, (tmp___0^0-tmp___0^post9 == 0 /\ -size7^post9+size7^0 == 0 /\ size17^0-size17^post9 == 0 /\ -___len21^post9+___len21^0 == 0 /\ tmp13^0-tmp13^post9 == 0 /\ -tmp___1^post9+tmp___1^0 == 0 /\ size15^0-size15^post9 == 0 /\ -size11^post9+size11^0 == 0 /\ -tmp22^post9+tmp22^0 == 0 /\ tmp^0-tmp^post9 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post9 == 0 /\ tmp9^0-tmp9^post9 == 0 /\ -retval^post9+retval^0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post9 == 0), cost: 1
	New rule:
	l7 -> l6 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1
	
		propagated equality tmp___0^post9 = tmp___0^0
		
		propagated equality size7^post9 = size7^0
		
		propagated equality size17^post9 = size17^0
		
		propagated equality ___len21^post9 = ___len21^0
		
		propagated equality tmp13^post9 = tmp13^0
		
		propagated equality tmp___1^post9 = tmp___1^0
		
		propagated equality size15^post9 = size15^0
		
		propagated equality size11^post9 = size11^0
		
		propagated equality tmp22^post9 = tmp22^0
		
		propagated equality tmp^post9 = tmp^0
		
		propagated equality ret_my_malloc14^post9 = ret_my_malloc14^0
		
		propagated equality tmp9^post9 = tmp9^0
		
		propagated equality retval^post9 = retval^0
		
		propagated equality ret_my_malloc10^post9 = ret_my_malloc10^0
		
	Simplified Guard

	Original rule:
	l7 -> l6 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1
	New rule:
	l7 -> l6 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l7 -> l6 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, T, cost: 1
	New rule:
	l7 -> l6 : T, cost: 1
	
	Propagated Equalities

	Original rule:
	l8 -> l7 : ___len21^0'=___len21^post10, ret_my_malloc10^0'=ret_my_malloc10^post10, ret_my_malloc14^0'=ret_my_malloc14^post10, retval^0'=retval^post10, size11^0'=size11^post10, size15^0'=size15^post10, size17^0'=size17^post10, size7^0'=size7^post10, tmp13^0'=tmp13^post10, tmp22^0'=tmp22^post10, tmp9^0'=tmp9^post10, tmp^0'=tmp^post10, tmp___0^0'=tmp___0^post10, tmp___1^0'=tmp___1^post10, (ret_my_malloc10^0-ret_my_malloc10^post10 == 0 /\ -size11^post10+size11^0 == 0 /\ -ret_my_malloc14^post10+ret_my_malloc14^0 == 0 /\ -tmp___0^post10+tmp___0^0 == 0 /\ tmp9^0-tmp9^post10 == 0 /\ tmp^0-tmp^post10 == 0 /\ retval^0-retval^post10 == 0 /\ size17^0-size17^post10 == 0 /\ -___len21^post10+___len21^0 == 0 /\ tmp13^0-tmp13^post10 == 0 /\ -tmp22^post10+tmp22^0 == 0 /\ -size7^post10+size7^0 == 0 /\ -size15^post10+size15^0 == 0 /\ -tmp___1^post10+tmp___1^0 == 0), cost: 1
	New rule:
	l8 -> l7 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1
	
		propagated equality ret_my_malloc10^post10 = ret_my_malloc10^0
		
		propagated equality size11^post10 = size11^0
		
		propagated equality ret_my_malloc14^post10 = ret_my_malloc14^0
		
		propagated equality tmp___0^post10 = tmp___0^0
		
		propagated equality tmp9^post10 = tmp9^0
		
		propagated equality tmp^post10 = tmp^0
		
		propagated equality retval^post10 = retval^0
		
		propagated equality size17^post10 = size17^0
		
		propagated equality ___len21^post10 = ___len21^0
		
		propagated equality tmp13^post10 = tmp13^0
		
		propagated equality tmp22^post10 = tmp22^0
		
		propagated equality size7^post10 = size7^0
		
		propagated equality size15^post10 = size15^0
		
		propagated equality tmp___1^post10 = tmp___1^0
		
	Simplified Guard

	Original rule:
	l8 -> l7 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1
	New rule:
	l8 -> l7 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l8 -> l7 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, T, cost: 1
	New rule:
	l8 -> l7 : T, cost: 1
	
	Propagated Equalities

	Original rule:
	l8 -> l6 : ___len21^0'=___len21^post11, ret_my_malloc10^0'=ret_my_malloc10^post11, ret_my_malloc14^0'=ret_my_malloc14^post11, retval^0'=retval^post11, size11^0'=size11^post11, size15^0'=size15^post11, size17^0'=size17^post11, size7^0'=size7^post11, tmp13^0'=tmp13^post11, tmp22^0'=tmp22^post11, tmp9^0'=tmp9^post11, tmp^0'=tmp^post11, tmp___0^0'=tmp___0^post11, tmp___1^0'=tmp___1^post11, (-ret_my_malloc10^post11+ret_my_malloc10^0 == 0 /\ -size11^post11+size11^0 == 0 /\ -size15^post11+size15^0 == 0 /\ -size7^post11+size7^0 == 0 /\ tmp9^0-tmp9^post11 == 0 /\ -ret_my_malloc14^post11+ret_my_malloc14^0 == 0 /\ -tmp___0^post11+tmp___0^0 == 0 /\ tmp22^0-tmp22^post11 == 0 /\ size17^0-size17^post11 == 0 /\ tmp___1^0-tmp___1^post11 == 0 /\ -tmp^post11+tmp^0 == 0 /\ retval^0-retval^post11 == 0 /\ -___len21^post11+___len21^0 == 0 /\ tmp13^0-tmp13^post11 == 0), cost: 1
	New rule:
	l8 -> l6 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1
	
		propagated equality ret_my_malloc10^post11 = ret_my_malloc10^0
		
		propagated equality size11^post11 = size11^0
		
		propagated equality size15^post11 = size15^0
		
		propagated equality size7^post11 = size7^0
		
		propagated equality tmp9^post11 = tmp9^0
		
		propagated equality ret_my_malloc14^post11 = ret_my_malloc14^0
		
		propagated equality tmp___0^post11 = tmp___0^0
		
		propagated equality tmp22^post11 = tmp22^0
		
		propagated equality size17^post11 = size17^0
		
		propagated equality tmp___1^post11 = tmp___1^0
		
		propagated equality tmp^post11 = tmp^0
		
		propagated equality retval^post11 = retval^0
		
		propagated equality ___len21^post11 = ___len21^0
		
		propagated equality tmp13^post11 = tmp13^0
		
	Simplified Guard

	Original rule:
	l8 -> l6 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1
	New rule:
	l8 -> l6 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l8 -> l6 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, T, cost: 1
	New rule:
	l8 -> l6 : T, cost: 1
	
	Propagated Equalities

	Original rule:
	l8 -> l7 : ___len21^0'=___len21^post12, ret_my_malloc10^0'=ret_my_malloc10^post12, ret_my_malloc14^0'=ret_my_malloc14^post12, retval^0'=retval^post12, size11^0'=size11^post12, size15^0'=size15^post12, size17^0'=size17^post12, size7^0'=size7^post12, tmp13^0'=tmp13^post12, tmp22^0'=tmp22^post12, tmp9^0'=tmp9^post12, tmp^0'=tmp^post12, tmp___0^0'=tmp___0^post12, tmp___1^0'=tmp___1^post12, (tmp^0-tmp^post12 == 0 /\ size15^0-size15^post12 == 0 /\ -tmp13^post12+tmp13^0 == 0 /\ -tmp22^post12+tmp22^0 == 0 /\ -___len21^post12+___len21^0 == 0 /\ tmp9^0-tmp9^post12 == 0 /\ tmp___1^0-tmp___1^post12 == 0 /\ -size11^post12+size11^0 == 0 /\ -size7^post12+size7^0 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post12 == 0 /\ -retval^post12+retval^0 == 0 /\ -tmp___0^post12+tmp___0^0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post12 == 0 /\ size17^0-size17^post12 == 0), cost: 1
	New rule:
	l8 -> l7 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1
	
		propagated equality tmp^post12 = tmp^0
		
		propagated equality size15^post12 = size15^0
		
		propagated equality tmp13^post12 = tmp13^0
		
		propagated equality tmp22^post12 = tmp22^0
		
		propagated equality ___len21^post12 = ___len21^0
		
		propagated equality tmp9^post12 = tmp9^0
		
		propagated equality tmp___1^post12 = tmp___1^0
		
		propagated equality size11^post12 = size11^0
		
		propagated equality size7^post12 = size7^0
		
		propagated equality ret_my_malloc14^post12 = ret_my_malloc14^0
		
		propagated equality retval^post12 = retval^0
		
		propagated equality tmp___0^post12 = tmp___0^0
		
		propagated equality ret_my_malloc10^post12 = ret_my_malloc10^0
		
		propagated equality size17^post12 = size17^0
		
	Simplified Guard

	Original rule:
	l8 -> l7 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1
	New rule:
	l8 -> l7 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l8 -> l7 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, T, cost: 1
	New rule:
	l8 -> l7 : T, cost: 1
	
	Propagated Equalities

	Original rule:
	l9 -> l8 : ___len21^0'=___len21^post13, ret_my_malloc10^0'=ret_my_malloc10^post13, ret_my_malloc14^0'=ret_my_malloc14^post13, retval^0'=retval^post13, size11^0'=size11^post13, size15^0'=size15^post13, size17^0'=size17^post13, size7^0'=size7^post13, tmp13^0'=tmp13^post13, tmp22^0'=tmp22^post13, tmp9^0'=tmp9^post13, tmp^0'=tmp^post13, tmp___0^0'=tmp___0^post13, tmp___1^0'=tmp___1^post13, (-ret_my_malloc14^post13+ret_my_malloc14^0 == 0 /\ retval^0-retval^post13 == 0 /\ -tmp___1^post13+tmp___1^0 == 0 /\ -tmp___0^post13+tmp___0^0 == 0 /\ -___len21^post13+___len21^0 == 0 /\ -tmp^post13+tmp^0 == 0 /\ -100+size17^post13 == 0 /\ tmp22^0-tmp22^post13 == 0 /\ -size15^post13+size15^0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post13 == 0 /\ -size7^post13+size7^0 == 0 /\ tmp13^0-tmp13^post13 == 0 /\ -size11^post13+size11^0 == 0 /\ -tmp9^post13+tmp9^0 == 0), cost: 1
	New rule:
	l9 -> l8 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=100, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1
	
		propagated equality ret_my_malloc14^post13 = ret_my_malloc14^0
		
		propagated equality retval^post13 = retval^0
		
		propagated equality tmp___1^post13 = tmp___1^0
		
		propagated equality tmp___0^post13 = tmp___0^0
		
		propagated equality ___len21^post13 = ___len21^0
		
		propagated equality tmp^post13 = tmp^0
		
		propagated equality size17^post13 = 100
		
		propagated equality tmp22^post13 = tmp22^0
		
		propagated equality size15^post13 = size15^0
		
		propagated equality ret_my_malloc10^post13 = ret_my_malloc10^0
		
		propagated equality size7^post13 = size7^0
		
		propagated equality tmp13^post13 = tmp13^0
		
		propagated equality size11^post13 = size11^0
		
		propagated equality tmp9^post13 = tmp9^0
		
	Simplified Guard

	Original rule:
	l9 -> l8 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=100, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1
	New rule:
	l9 -> l8 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=100, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l9 -> l8 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=100, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, T, cost: 1
	New rule:
	l9 -> l8 : size17^0'=100, T, cost: 1
	
	Propagated Equalities

	Original rule:
	l10 -> l3 : ___len21^0'=___len21^post14, ret_my_malloc10^0'=ret_my_malloc10^post14, ret_my_malloc14^0'=ret_my_malloc14^post14, retval^0'=retval^post14, size11^0'=size11^post14, size15^0'=size15^post14, size17^0'=size17^post14, size7^0'=size7^post14, tmp13^0'=tmp13^post14, tmp22^0'=tmp22^post14, tmp9^0'=tmp9^post14, tmp^0'=tmp^post14, tmp___0^0'=tmp___0^post14, tmp___1^0'=tmp___1^post14, (-tmp22^post14+tmp22^0 == 0 /\ size15^0-size15^post14 == 0 /\ retval^0-retval^post14 == 0 /\ tmp___0^0-tmp___0^post14 == 0 /\ -size7^post14+size7^0 == 0 /\ size17^0-size17^post14 == 0 /\ -___len21^post14+___len21^0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post14 == 0 /\ -size11^post14+size11^0 == 0 /\ -tmp___1^post14+tmp___1^0 == 0 /\ tmp13^0-tmp13^post14 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post14 == 0 /\ tmp9^0-tmp9^post14 == 0 /\ tmp^0-tmp^post14 == 0), cost: 1
	New rule:
	l10 -> l3 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1
	
		propagated equality tmp22^post14 = tmp22^0
		
		propagated equality size15^post14 = size15^0
		
		propagated equality retval^post14 = retval^0
		
		propagated equality tmp___0^post14 = tmp___0^0
		
		propagated equality size7^post14 = size7^0
		
		propagated equality size17^post14 = size17^0
		
		propagated equality ___len21^post14 = ___len21^0
		
		propagated equality ret_my_malloc10^post14 = ret_my_malloc10^0
		
		propagated equality size11^post14 = size11^0
		
		propagated equality tmp___1^post14 = tmp___1^0
		
		propagated equality tmp13^post14 = tmp13^0
		
		propagated equality ret_my_malloc14^post14 = ret_my_malloc14^0
		
		propagated equality tmp9^post14 = tmp9^0
		
		propagated equality tmp^post14 = tmp^0
		
	Simplified Guard

	Original rule:
	l10 -> l3 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1
	New rule:
	l10 -> l3 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l10 -> l3 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, T, cost: 1
	New rule:
	l10 -> l3 : T, cost: 1
	
	Propagated Equalities

	Original rule:
	l11 -> l10 : ___len21^0'=___len21^post15, ret_my_malloc10^0'=ret_my_malloc10^post15, ret_my_malloc14^0'=ret_my_malloc14^post15, retval^0'=retval^post15, size11^0'=size11^post15, size15^0'=size15^post15, size17^0'=size17^post15, size7^0'=size7^post15, tmp13^0'=tmp13^post15, tmp22^0'=tmp22^post15, tmp9^0'=tmp9^post15, tmp^0'=tmp^post15, tmp___0^0'=tmp___0^post15, tmp___1^0'=tmp___1^post15, (tmp^0-tmp^post15 == 0 /\ -tmp22^post15+tmp22^0 == 0 /\ tmp9^0-tmp9^post15 == 0 /\ tmp___1^0-tmp___1^post15 == 0 /\ -tmp13^post15+tmp13^0 == 0 /\ retval^0-retval^post15 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post15 == 0 /\ -size7^post15+size7^0 == 0 /\ -ret_my_malloc14^post15+ret_my_malloc14^0 == 0 /\ -tmp___0^post15+tmp___0^0 == 0 /\ -size11^post15+size11^0 == 0 /\ -size15^post15+size15^0 == 0 /\ size17^0-size17^post15 == 0 /\ -___len21^post15+___len21^0 == 0), cost: 1
	New rule:
	l11 -> l10 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1
	
		propagated equality tmp^post15 = tmp^0
		
		propagated equality tmp22^post15 = tmp22^0
		
		propagated equality tmp9^post15 = tmp9^0
		
		propagated equality tmp___1^post15 = tmp___1^0
		
		propagated equality tmp13^post15 = tmp13^0
		
		propagated equality retval^post15 = retval^0
		
		propagated equality ret_my_malloc10^post15 = ret_my_malloc10^0
		
		propagated equality size7^post15 = size7^0
		
		propagated equality ret_my_malloc14^post15 = ret_my_malloc14^0
		
		propagated equality tmp___0^post15 = tmp___0^0
		
		propagated equality size11^post15 = size11^0
		
		propagated equality size15^post15 = size15^0
		
		propagated equality size17^post15 = size17^0
		
		propagated equality ___len21^post15 = ___len21^0
		
	Simplified Guard

	Original rule:
	l11 -> l10 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1
	New rule:
	l11 -> l10 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l11 -> l10 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, T, cost: 1
	New rule:
	l11 -> l10 : T, cost: 1
	
	Propagated Equalities

	Original rule:
	l12 -> l11 : ___len21^0'=___len21^post16, ret_my_malloc10^0'=ret_my_malloc10^post16, ret_my_malloc14^0'=ret_my_malloc14^post16, retval^0'=retval^post16, size11^0'=size11^post16, size15^0'=size15^post16, size17^0'=size17^post16, size7^0'=size7^post16, tmp13^0'=tmp13^post16, tmp22^0'=tmp22^post16, tmp9^0'=tmp9^post16, tmp^0'=tmp^post16, tmp___0^0'=tmp___0^post16, tmp___1^0'=tmp___1^post16, (-size7^post16+size7^0 == 0 /\ -___len21^post16+___len21^0 == 0 /\ -ret_my_malloc14^post16+ret_my_malloc14^0 == 0 /\ -size11^post16+size11^0 == 0 /\ -tmp___0^post16+tmp___0^0 == 0 /\ retval^0-retval^post16 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post16 == 0 /\ tmp22^0-tmp22^post16 == 0 /\ size17^0-size17^post16 == 0 /\ -tmp^post16+tmp^0 == 0 /\ tmp___1^0-tmp___1^post16 == 0 /\ size15^0-size15^post16 == 0 /\ tmp13^0-tmp13^post16 == 0 /\ -tmp9^post16+tmp9^0 == 0), cost: 1
	New rule:
	l12 -> l11 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1
	
		propagated equality size7^post16 = size7^0
		
		propagated equality ___len21^post16 = ___len21^0
		
		propagated equality ret_my_malloc14^post16 = ret_my_malloc14^0
		
		propagated equality size11^post16 = size11^0
		
		propagated equality tmp___0^post16 = tmp___0^0
		
		propagated equality retval^post16 = retval^0
		
		propagated equality ret_my_malloc10^post16 = ret_my_malloc10^0
		
		propagated equality tmp22^post16 = tmp22^0
		
		propagated equality size17^post16 = size17^0
		
		propagated equality tmp^post16 = tmp^0
		
		propagated equality tmp___1^post16 = tmp___1^0
		
		propagated equality size15^post16 = size15^0
		
		propagated equality tmp13^post16 = tmp13^0
		
		propagated equality tmp9^post16 = tmp9^0
		
	Simplified Guard

	Original rule:
	l12 -> l11 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1
	New rule:
	l12 -> l11 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l12 -> l11 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, T, cost: 1
	New rule:
	l12 -> l11 : T, cost: 1
	
	Propagated Equalities

	Original rule:
	l12 -> l10 : ___len21^0'=___len21^post17, ret_my_malloc10^0'=ret_my_malloc10^post17, ret_my_malloc14^0'=ret_my_malloc14^post17, retval^0'=retval^post17, size11^0'=size11^post17, size15^0'=size15^post17, size17^0'=size17^post17, size7^0'=size7^post17, tmp13^0'=tmp13^post17, tmp22^0'=tmp22^post17, tmp9^0'=tmp9^post17, tmp^0'=tmp^post17, tmp___0^0'=tmp___0^post17, tmp___1^0'=tmp___1^post17, (retval^0-retval^post17 == 0 /\ size17^0-size17^post17 == 0 /\ -size15^post17+size15^0 == 0 /\ tmp9^0-tmp9^post17 == 0 /\ -size7^post17+size7^0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post17 == 0 /\ -___len21^post17+___len21^0 == 0 /\ tmp___1^0-tmp___1^post17 == 0 /\ -size11^post17+size11^0 == 0 /\ -tmp___0^post17+tmp___0^0 == 0 /\ -tmp22^post17+tmp22^0 == 0 /\ tmp13^0-tmp13^post17 == 0 /\ -tmp^post17+tmp^0 == 0 /\ -ret_my_malloc14^post17+ret_my_malloc14^0 == 0), cost: 1
	New rule:
	l12 -> l10 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1
	
		propagated equality retval^post17 = retval^0
		
		propagated equality size17^post17 = size17^0
		
		propagated equality size15^post17 = size15^0
		
		propagated equality tmp9^post17 = tmp9^0
		
		propagated equality size7^post17 = size7^0
		
		propagated equality ret_my_malloc10^post17 = ret_my_malloc10^0
		
		propagated equality ___len21^post17 = ___len21^0
		
		propagated equality tmp___1^post17 = tmp___1^0
		
		propagated equality size11^post17 = size11^0
		
		propagated equality tmp___0^post17 = tmp___0^0
		
		propagated equality tmp22^post17 = tmp22^0
		
		propagated equality tmp13^post17 = tmp13^0
		
		propagated equality tmp^post17 = tmp^0
		
		propagated equality ret_my_malloc14^post17 = ret_my_malloc14^0
		
	Simplified Guard

	Original rule:
	l12 -> l10 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1
	New rule:
	l12 -> l10 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l12 -> l10 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, T, cost: 1
	New rule:
	l12 -> l10 : T, cost: 1
	
	Propagated Equalities

	Original rule:
	l12 -> l11 : ___len21^0'=___len21^post18, ret_my_malloc10^0'=ret_my_malloc10^post18, ret_my_malloc14^0'=ret_my_malloc14^post18, retval^0'=retval^post18, size11^0'=size11^post18, size15^0'=size15^post18, size17^0'=size17^post18, size7^0'=size7^post18, tmp13^0'=tmp13^post18, tmp22^0'=tmp22^post18, tmp9^0'=tmp9^post18, tmp^0'=tmp^post18, tmp___0^0'=tmp___0^post18, tmp___1^0'=tmp___1^post18, (size15^0-size15^post18 == 0 /\ tmp___0^0-tmp___0^post18 == 0 /\ -tmp___1^post18+tmp___1^0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post18 == 0 /\ -tmp22^post18+tmp22^0 == 0 /\ size17^0-size17^post18 == 0 /\ -___len21^post18+___len21^0 == 0 /\ -size7^post18+size7^0 == 0 /\ -size11^post18+size11^0 == 0 /\ tmp^0-tmp^post18 == 0 /\ tmp9^0-tmp9^post18 == 0 /\ tmp13^0-tmp13^post18 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post18 == 0 /\ retval^0-retval^post18 == 0), cost: 1
	New rule:
	l12 -> l11 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1
	
		propagated equality size15^post18 = size15^0
		
		propagated equality tmp___0^post18 = tmp___0^0
		
		propagated equality tmp___1^post18 = tmp___1^0
		
		propagated equality ret_my_malloc10^post18 = ret_my_malloc10^0
		
		propagated equality tmp22^post18 = tmp22^0
		
		propagated equality size17^post18 = size17^0
		
		propagated equality ___len21^post18 = ___len21^0
		
		propagated equality size7^post18 = size7^0
		
		propagated equality size11^post18 = size11^0
		
		propagated equality tmp^post18 = tmp^0
		
		propagated equality tmp9^post18 = tmp9^0
		
		propagated equality tmp13^post18 = tmp13^0
		
		propagated equality ret_my_malloc14^post18 = ret_my_malloc14^0
		
		propagated equality retval^post18 = retval^0
		
	Simplified Guard

	Original rule:
	l12 -> l11 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1
	New rule:
	l12 -> l11 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l12 -> l11 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, T, cost: 1
	New rule:
	l12 -> l11 : T, cost: 1
	
	Propagated Equalities

	Original rule:
	l13 -> l12 : ___len21^0'=___len21^post19, ret_my_malloc10^0'=ret_my_malloc10^post19, ret_my_malloc14^0'=ret_my_malloc14^post19, retval^0'=retval^post19, size11^0'=size11^post19, size15^0'=size15^post19, size17^0'=size17^post19, size7^0'=size7^post19, tmp13^0'=tmp13^post19, tmp22^0'=tmp22^post19, tmp9^0'=tmp9^post19, tmp^0'=tmp^post19, tmp___0^0'=tmp___0^post19, tmp___1^0'=tmp___1^post19, (tmp^0-tmp^post19 == 0 /\ -100+size15^post19 == 0 /\ -size7^post19+size7^0 == 0 /\ -tmp___0^post19+tmp___0^0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post19 == 0 /\ tmp9^0-tmp9^post19 == 0 /\ -tmp22^post19+tmp22^0 == 0 /\ tmp___1^0-tmp___1^post19 == 0 /\ -size11^post19+size11^0 == 0 /\ size17^0-size17^post19 == 0 /\ -___len21^post19+___len21^0 == 0 /\ retval^0-retval^post19 == 0 /\ tmp13^0-tmp13^post19 == 0 /\ -ret_my_malloc14^post19+ret_my_malloc14^0 == 0), cost: 1
	New rule:
	l13 -> l12 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=100, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1
	
		propagated equality tmp^post19 = tmp^0
		
		propagated equality size15^post19 = 100
		
		propagated equality size7^post19 = size7^0
		
		propagated equality tmp___0^post19 = tmp___0^0
		
		propagated equality ret_my_malloc10^post19 = ret_my_malloc10^0
		
		propagated equality tmp9^post19 = tmp9^0
		
		propagated equality tmp22^post19 = tmp22^0
		
		propagated equality tmp___1^post19 = tmp___1^0
		
		propagated equality size11^post19 = size11^0
		
		propagated equality size17^post19 = size17^0
		
		propagated equality ___len21^post19 = ___len21^0
		
		propagated equality retval^post19 = retval^0
		
		propagated equality tmp13^post19 = tmp13^0
		
		propagated equality ret_my_malloc14^post19 = ret_my_malloc14^0
		
	Simplified Guard

	Original rule:
	l13 -> l12 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=100, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1
	New rule:
	l13 -> l12 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=100, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l13 -> l12 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=100, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, T, cost: 1
	New rule:
	l13 -> l12 : size15^0'=100, T, cost: 1
	
	Propagated Equalities

	Original rule:
	l14 -> l15 : ___len21^0'=___len21^post20, ret_my_malloc10^0'=ret_my_malloc10^post20, ret_my_malloc14^0'=ret_my_malloc14^post20, retval^0'=retval^post20, size11^0'=size11^post20, size15^0'=size15^post20, size17^0'=size17^post20, size7^0'=size7^post20, tmp13^0'=tmp13^post20, tmp22^0'=tmp22^post20, tmp9^0'=tmp9^post20, tmp^0'=tmp^post20, tmp___0^0'=tmp___0^post20, tmp___1^0'=tmp___1^post20, (-size15^post20+size15^0 == 0 /\ -tmp___0^post20+tmp___0^0 == 0 /\ -___len21^post20+___len21^0 == 0 /\ tmp___1^0-tmp___1^post20 == 0 /\ tmp22^0-tmp22^post20 == 0 /\ -tmp9^post20+tmp9^0 == 0 /\ tmp13^0-tmp13^post20 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post20 == 0 /\ -tmp^post20+tmp^0 == 0 /\ size17^0-size17^post20 == 0 /\ -ret_my_malloc14^0+retval^post20 == 0 /\ -size11^post20+size11^0 == 0 /\ -size7^post20+size7^0 == 0 /\ -ret_my_malloc14^post20+ret_my_malloc14^0 == 0), cost: 1
	New rule:
	l14 -> l15 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=ret_my_malloc14^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1
	
		propagated equality size15^post20 = size15^0
		
		propagated equality tmp___0^post20 = tmp___0^0
		
		propagated equality ___len21^post20 = ___len21^0
		
		propagated equality tmp___1^post20 = tmp___1^0
		
		propagated equality tmp22^post20 = tmp22^0
		
		propagated equality tmp9^post20 = tmp9^0
		
		propagated equality tmp13^post20 = tmp13^0
		
		propagated equality ret_my_malloc10^post20 = ret_my_malloc10^0
		
		propagated equality tmp^post20 = tmp^0
		
		propagated equality size17^post20 = size17^0
		
		propagated equality retval^post20 = ret_my_malloc14^0
		
		propagated equality size11^post20 = size11^0
		
		propagated equality size7^post20 = size7^0
		
		propagated equality ret_my_malloc14^post20 = ret_my_malloc14^0
		
	Simplified Guard

	Original rule:
	l14 -> l15 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=ret_my_malloc14^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1
	New rule:
	l14 -> l15 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=ret_my_malloc14^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l14 -> l15 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=ret_my_malloc14^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, T, cost: 1
	New rule:
	l14 -> l15 : retval^0'=ret_my_malloc14^0, T, cost: 1
	
	made implied equalities explicit

	Original rule:
	l15 -> l5 : ___len21^0'=___len21^post21, ret_my_malloc10^0'=ret_my_malloc10^post21, ret_my_malloc14^0'=ret_my_malloc14^post21, retval^0'=retval^post21, size11^0'=size11^post21, size15^0'=size15^post21, size17^0'=size17^post21, size7^0'=size7^post21, tmp13^0'=tmp13^post21, tmp22^0'=tmp22^post21, tmp9^0'=tmp9^post21, tmp^0'=tmp^post21, tmp___0^0'=tmp___0^post21, tmp___1^0'=tmp___1^post21, (0 == 0 /\ -size7^post21+size7^0 == 0 /\ size15^0-size15^post21 == 0 /\ size17^0-size17^post21 == 0 /\ tmp9^0-tmp9^post21 == 0 /\ 1-retval^0 <= 0 /\ -1+retval^0 <= 0 /\ tmp13^0-tmp13^post21 == 0 /\ -retval^post21+retval^0 == 0 /\ -size11^post21+size11^0 == 0 /\ -___len21^post21+___len21^0 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post21 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post21 == 0 /\ -tmp___0^post21+tmp___0^0 == 0 /\ -tmp22^post21+tmp22^0 == 0 /\ -tmp^post21+tmp^0 == 0), cost: 1
	New rule:
	l15 -> l5 : ___len21^0'=___len21^post21, ret_my_malloc10^0'=ret_my_malloc10^post21, ret_my_malloc14^0'=ret_my_malloc14^post21, retval^0'=retval^post21, size11^0'=size11^post21, size15^0'=size15^post21, size17^0'=size17^post21, size7^0'=size7^post21, tmp13^0'=tmp13^post21, tmp22^0'=tmp22^post21, tmp9^0'=tmp9^post21, tmp^0'=tmp^post21, tmp___0^0'=tmp___0^post21, tmp___1^0'=tmp___1^post21, (0 == 0 /\ -size7^post21+size7^0 == 0 /\ size15^0-size15^post21 == 0 /\ size17^0-size17^post21 == 0 /\ tmp9^0-tmp9^post21 == 0 /\ 1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0 /\ tmp13^0-tmp13^post21 == 0 /\ -retval^post21+retval^0 == 0 /\ -size11^post21+size11^0 == 0 /\ -___len21^post21+___len21^0 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post21 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post21 == 0 /\ -tmp___0^post21+tmp___0^0 == 0 /\ -tmp22^post21+tmp22^0 == 0 /\ -tmp^post21+tmp^0 == 0), cost: 1
	
	Propagated Equalities

	Original rule:
	l15 -> l5 : ___len21^0'=___len21^post21, ret_my_malloc10^0'=ret_my_malloc10^post21, ret_my_malloc14^0'=ret_my_malloc14^post21, retval^0'=retval^post21, size11^0'=size11^post21, size15^0'=size15^post21, size17^0'=size17^post21, size7^0'=size7^post21, tmp13^0'=tmp13^post21, tmp22^0'=tmp22^post21, tmp9^0'=tmp9^post21, tmp^0'=tmp^post21, tmp___0^0'=tmp___0^post21, tmp___1^0'=tmp___1^post21, (0 == 0 /\ -size7^post21+size7^0 == 0 /\ size15^0-size15^post21 == 0 /\ size17^0-size17^post21 == 0 /\ tmp9^0-tmp9^post21 == 0 /\ 1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0 /\ tmp13^0-tmp13^post21 == 0 /\ -retval^post21+retval^0 == 0 /\ -size11^post21+size11^0 == 0 /\ -___len21^post21+___len21^0 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post21 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post21 == 0 /\ -tmp___0^post21+tmp___0^0 == 0 /\ -tmp22^post21+tmp22^0 == 0 /\ -tmp^post21+tmp^0 == 0), cost: 1
	New rule:
	l15 -> l5 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^post21, (0 == 0 /\ 1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0), cost: 1
	
		propagated equality size7^post21 = size7^0
		
		propagated equality size15^post21 = size15^0
		
		propagated equality size17^post21 = size17^0
		
		propagated equality tmp9^post21 = tmp9^0
		
		propagated equality tmp13^post21 = tmp13^0
		
		propagated equality retval^post21 = retval^0
		
		propagated equality size11^post21 = size11^0
		
		propagated equality ___len21^post21 = ___len21^0
		
		propagated equality ret_my_malloc14^post21 = ret_my_malloc14^0
		
		propagated equality ret_my_malloc10^post21 = ret_my_malloc10^0
		
		propagated equality tmp___0^post21 = tmp___0^0
		
		propagated equality tmp22^post21 = tmp22^0
		
		propagated equality tmp^post21 = tmp^0
		
	Simplified Guard

	Original rule:
	l15 -> l5 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^post21, (0 == 0 /\ 1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0), cost: 1
	New rule:
	l15 -> l5 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^post21, (1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0), cost: 1
	
	made implied equalities explicit

	Original rule:
	l15 -> l5 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^post21, (1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0), cost: 1
	New rule:
	l15 -> l5 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^post21, (1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0), cost: 1
	
	Removed Trivial Updates

	Original rule:
	l15 -> l5 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^post21, (1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0), cost: 1
	New rule:
	l15 -> l5 : tmp___1^0'=tmp___1^post21, (1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0), cost: 1
	
	Propagated Equalities

	Original rule:
	l15 -> l13 : ___len21^0'=___len21^post22, ret_my_malloc10^0'=ret_my_malloc10^post22, ret_my_malloc14^0'=ret_my_malloc14^post22, retval^0'=retval^post22, size11^0'=size11^post22, size15^0'=size15^post22, size17^0'=size17^post22, size7^0'=size7^post22, tmp13^0'=tmp13^post22, tmp22^0'=tmp22^post22, tmp9^0'=tmp9^post22, tmp^0'=tmp^post22, tmp___0^0'=tmp___0^post22, tmp___1^0'=tmp___1^post22, (retval^0-retval^post22 == 0 /\ 2-retval^0 <= 0 /\ -tmp___1^post22+tmp___1^0 == 0 /\ -tmp___0^post22+tmp___0^0 == 0 /\ -size11^post22+size11^0 == 0 /\ -ret_my_malloc14^post22+ret_my_malloc14^0 == 0 /\ tmp^0-tmp^post22 == 0 /\ -tmp9^post22+tmp9^0 == 0 /\ size15^0-size15^post22 == 0 /\ -___len21^post22+___len21^0 == 0 /\ tmp13^0-tmp13^post22 == 0 /\ tmp22^0-tmp22^post22 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post22 == 0 /\ size17^0-size17^post22 == 0 /\ -size7^post22+size7^0 == 0), cost: 1
	New rule:
	l15 -> l13 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, (0 == 0 /\ 2-retval^0 <= 0), cost: 1
	
		propagated equality retval^post22 = retval^0
		
		propagated equality tmp___1^post22 = tmp___1^0
		
		propagated equality tmp___0^post22 = tmp___0^0
		
		propagated equality size11^post22 = size11^0
		
		propagated equality ret_my_malloc14^post22 = ret_my_malloc14^0
		
		propagated equality tmp^post22 = tmp^0
		
		propagated equality tmp9^post22 = tmp9^0
		
		propagated equality size15^post22 = size15^0
		
		propagated equality ___len21^post22 = ___len21^0
		
		propagated equality tmp13^post22 = tmp13^0
		
		propagated equality tmp22^post22 = tmp22^0
		
		propagated equality ret_my_malloc10^post22 = ret_my_malloc10^0
		
		propagated equality size17^post22 = size17^0
		
		propagated equality size7^post22 = size7^0
		
	Simplified Guard

	Original rule:
	l15 -> l13 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, (0 == 0 /\ 2-retval^0 <= 0), cost: 1
	New rule:
	l15 -> l13 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 2-retval^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l15 -> l13 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 2-retval^0 <= 0, cost: 1
	New rule:
	l15 -> l13 : 2-retval^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l15 -> l13 : ___len21^0'=___len21^post23, ret_my_malloc10^0'=ret_my_malloc10^post23, ret_my_malloc14^0'=ret_my_malloc14^post23, retval^0'=retval^post23, size11^0'=size11^post23, size15^0'=size15^post23, size17^0'=size17^post23, size7^0'=size7^post23, tmp13^0'=tmp13^post23, tmp22^0'=tmp22^post23, tmp9^0'=tmp9^post23, tmp^0'=tmp^post23, tmp___0^0'=tmp___0^post23, tmp___1^0'=tmp___1^post23, (tmp___0^0-tmp___0^post23 == 0 /\ retval^0-retval^post23 == 0 /\ -tmp___1^post23+tmp___1^0 == 0 /\ retval^0 <= 0 /\ tmp^0-tmp^post23 == 0 /\ size17^0-size17^post23 == 0 /\ size15^0-size15^post23 == 0 /\ tmp9^0-tmp9^post23 == 0 /\ -size7^post23+size7^0 == 0 /\ -___len21^post23+___len21^0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post23 == 0 /\ -size11^post23+size11^0 == 0 /\ tmp13^0-tmp13^post23 == 0 /\ -tmp22^post23+tmp22^0 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post23 == 0), cost: 1
	New rule:
	l15 -> l13 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, (0 == 0 /\ retval^0 <= 0), cost: 1
	
		propagated equality tmp___0^post23 = tmp___0^0
		
		propagated equality retval^post23 = retval^0
		
		propagated equality tmp___1^post23 = tmp___1^0
		
		propagated equality tmp^post23 = tmp^0
		
		propagated equality size17^post23 = size17^0
		
		propagated equality size15^post23 = size15^0
		
		propagated equality tmp9^post23 = tmp9^0
		
		propagated equality size7^post23 = size7^0
		
		propagated equality ___len21^post23 = ___len21^0
		
		propagated equality ret_my_malloc10^post23 = ret_my_malloc10^0
		
		propagated equality size11^post23 = size11^0
		
		propagated equality tmp13^post23 = tmp13^0
		
		propagated equality tmp22^post23 = tmp22^0
		
		propagated equality ret_my_malloc14^post23 = ret_my_malloc14^0
		
	Simplified Guard

	Original rule:
	l15 -> l13 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, (0 == 0 /\ retval^0 <= 0), cost: 1
	New rule:
	l15 -> l13 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, retval^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l15 -> l13 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, retval^0 <= 0, cost: 1
	New rule:
	l15 -> l13 : retval^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l16 -> l14 : ___len21^0'=___len21^post24, ret_my_malloc10^0'=ret_my_malloc10^post24, ret_my_malloc14^0'=ret_my_malloc14^post24, retval^0'=retval^post24, size11^0'=size11^post24, size15^0'=size15^post24, size17^0'=size17^post24, size7^0'=size7^post24, tmp13^0'=tmp13^post24, tmp22^0'=tmp22^post24, tmp9^0'=tmp9^post24, tmp^0'=tmp^post24, tmp___0^0'=tmp___0^post24, tmp___1^0'=tmp___1^post24, (-tmp22^post24+tmp22^0 == 0 /\ tmp9^0-tmp9^post24 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post24 == 0 /\ ret_my_malloc14^post24 == 0 /\ tmp^0-tmp^post24 == 0 /\ -size15^post24+size15^0 == 0 /\ -size7^post24+size7^0 == 0 /\ tmp13^0-tmp13^post24 == 0 /\ tmp___1^0-tmp___1^post24 == 0 /\ -___len21^post24+___len21^0 == 0 /\ retval^0-retval^post24 == 0 /\ -tmp___0^post24+tmp___0^0 == 0 /\ -size11^post24+size11^0 == 0 /\ size17^0-size17^post24 == 0), cost: 1
	New rule:
	l16 -> l14 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1
	
		propagated equality tmp22^post24 = tmp22^0
		
		propagated equality tmp9^post24 = tmp9^0
		
		propagated equality ret_my_malloc10^post24 = ret_my_malloc10^0
		
		propagated equality ret_my_malloc14^post24 = 0
		
		propagated equality tmp^post24 = tmp^0
		
		propagated equality size15^post24 = size15^0
		
		propagated equality size7^post24 = size7^0
		
		propagated equality tmp13^post24 = tmp13^0
		
		propagated equality tmp___1^post24 = tmp___1^0
		
		propagated equality ___len21^post24 = ___len21^0
		
		propagated equality retval^post24 = retval^0
		
		propagated equality tmp___0^post24 = tmp___0^0
		
		propagated equality size11^post24 = size11^0
		
		propagated equality size17^post24 = size17^0
		
	Simplified Guard

	Original rule:
	l16 -> l14 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1
	New rule:
	l16 -> l14 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l16 -> l14 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, T, cost: 1
	New rule:
	l16 -> l14 : ret_my_malloc14^0'=0, T, cost: 1
	
	Propagated Equalities

	Original rule:
	l16 -> l14 : ___len21^0'=___len21^post25, ret_my_malloc10^0'=ret_my_malloc10^post25, ret_my_malloc14^0'=ret_my_malloc14^post25, retval^0'=retval^post25, size11^0'=size11^post25, size15^0'=size15^post25, size17^0'=size17^post25, size7^0'=size7^post25, tmp13^0'=tmp13^post25, tmp22^0'=tmp22^post25, tmp9^0'=tmp9^post25, tmp^0'=tmp^post25, tmp___0^0'=tmp___0^post25, tmp___1^0'=tmp___1^post25, (-tmp___1^post25+tmp___1^0 == 0 /\ -size7^post25+size7^0 == 0 /\ -tmp___0^post25+tmp___0^0 == 0 /\ tmp^0-tmp^post25 == 0 /\ -1+ret_my_malloc14^post25 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post25 == 0 /\ retval^0-retval^post25 == 0 /\ tmp22^0-tmp22^post25 == 0 /\ size15^0-size15^post25 == 0 /\ -size11^post25+size11^0 == 0 /\ size17^0-size17^post25 == 0 /\ tmp13^0-tmp13^post25 == 0 /\ -___len21^post25+___len21^0 == 0 /\ -tmp9^post25+tmp9^0 == 0), cost: 1
	New rule:
	l16 -> l14 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=1, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1
	
		propagated equality tmp___1^post25 = tmp___1^0
		
		propagated equality size7^post25 = size7^0
		
		propagated equality tmp___0^post25 = tmp___0^0
		
		propagated equality tmp^post25 = tmp^0
		
		propagated equality ret_my_malloc14^post25 = 1
		
		propagated equality ret_my_malloc10^post25 = ret_my_malloc10^0
		
		propagated equality retval^post25 = retval^0
		
		propagated equality tmp22^post25 = tmp22^0
		
		propagated equality size15^post25 = size15^0
		
		propagated equality size11^post25 = size11^0
		
		propagated equality size17^post25 = size17^0
		
		propagated equality tmp13^post25 = tmp13^0
		
		propagated equality ___len21^post25 = ___len21^0
		
		propagated equality tmp9^post25 = tmp9^0
		
	Simplified Guard

	Original rule:
	l16 -> l14 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=1, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1
	New rule:
	l16 -> l14 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=1, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l16 -> l14 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=1, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, T, cost: 1
	New rule:
	l16 -> l14 : ret_my_malloc14^0'=1, T, cost: 1
	
	Propagated Equalities

	Original rule:
	l17 -> l9 : ___len21^0'=___len21^post26, ret_my_malloc10^0'=ret_my_malloc10^post26, ret_my_malloc14^0'=ret_my_malloc14^post26, retval^0'=retval^post26, size11^0'=size11^post26, size15^0'=size15^post26, size17^0'=size17^post26, size7^0'=size7^post26, tmp13^0'=tmp13^post26, tmp22^0'=tmp22^post26, tmp9^0'=tmp9^post26, tmp^0'=tmp^post26, tmp___0^0'=tmp___0^post26, tmp___1^0'=tmp___1^post26, (tmp___1^0-tmp___1^post26 == 0 /\ tmp13^0-tmp13^post26 == 0 /\ 2-retval^0 <= 0 /\ -ret_my_malloc14^post26+ret_my_malloc14^0 == 0 /\ -size15^post26+size15^0 == 0 /\ size17^0-size17^post26 == 0 /\ -tmp___0^post26+tmp___0^0 == 0 /\ retval^0-retval^post26 == 0 /\ -tmp^post26+tmp^0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post26 == 0 /\ -tmp22^post26+tmp22^0 == 0 /\ -___len21^post26+___len21^0 == 0 /\ size11^0-size11^post26 == 0 /\ tmp9^0-tmp9^post26 == 0 /\ size7^0-size7^post26 == 0), cost: 1
	New rule:
	l17 -> l9 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, (0 == 0 /\ 2-retval^0 <= 0), cost: 1
	
		propagated equality tmp___1^post26 = tmp___1^0
		
		propagated equality tmp13^post26 = tmp13^0
		
		propagated equality ret_my_malloc14^post26 = ret_my_malloc14^0
		
		propagated equality size15^post26 = size15^0
		
		propagated equality size17^post26 = size17^0
		
		propagated equality tmp___0^post26 = tmp___0^0
		
		propagated equality retval^post26 = retval^0
		
		propagated equality tmp^post26 = tmp^0
		
		propagated equality ret_my_malloc10^post26 = ret_my_malloc10^0
		
		propagated equality tmp22^post26 = tmp22^0
		
		propagated equality ___len21^post26 = ___len21^0
		
		propagated equality size11^post26 = size11^0
		
		propagated equality tmp9^post26 = tmp9^0
		
		propagated equality size7^post26 = size7^0
		
	Simplified Guard

	Original rule:
	l17 -> l9 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, (0 == 0 /\ 2-retval^0 <= 0), cost: 1
	New rule:
	l17 -> l9 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 2-retval^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l17 -> l9 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 2-retval^0 <= 0, cost: 1
	New rule:
	l17 -> l9 : 2-retval^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l17 -> l9 : ___len21^0'=___len21^post27, ret_my_malloc10^0'=ret_my_malloc10^post27, ret_my_malloc14^0'=ret_my_malloc14^post27, retval^0'=retval^post27, size11^0'=size11^post27, size15^0'=size15^post27, size17^0'=size17^post27, size7^0'=size7^post27, tmp13^0'=tmp13^post27, tmp22^0'=tmp22^post27, tmp9^0'=tmp9^post27, tmp^0'=tmp^post27, tmp___0^0'=tmp___0^post27, tmp___1^0'=tmp___1^post27, (tmp22^0-tmp22^post27 == 0 /\ retval^0 <= 0 /\ ret_my_malloc14^0-ret_my_malloc14^post27 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post27 == 0 /\ retval^0-retval^post27 == 0 /\ tmp13^0-tmp13^post27 == 0 /\ -tmp9^post27+tmp9^0 == 0 /\ -size7^post27+size7^0 == 0 /\ -tmp___1^post27+tmp___1^0 == 0 /\ -tmp___0^post27+tmp___0^0 == 0 /\ tmp^0-tmp^post27 == 0 /\ -___len21^post27+___len21^0 == 0 /\ size17^0-size17^post27 == 0 /\ -size11^post27+size11^0 == 0 /\ size15^0-size15^post27 == 0), cost: 1
	New rule:
	l17 -> l9 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, (0 == 0 /\ retval^0 <= 0), cost: 1
	
		propagated equality tmp22^post27 = tmp22^0
		
		propagated equality ret_my_malloc14^post27 = ret_my_malloc14^0
		
		propagated equality ret_my_malloc10^post27 = ret_my_malloc10^0
		
		propagated equality retval^post27 = retval^0
		
		propagated equality tmp13^post27 = tmp13^0
		
		propagated equality tmp9^post27 = tmp9^0
		
		propagated equality size7^post27 = size7^0
		
		propagated equality tmp___1^post27 = tmp___1^0
		
		propagated equality tmp___0^post27 = tmp___0^0
		
		propagated equality tmp^post27 = tmp^0
		
		propagated equality ___len21^post27 = ___len21^0
		
		propagated equality size17^post27 = size17^0
		
		propagated equality size11^post27 = size11^0
		
		propagated equality size15^post27 = size15^0
		
	Simplified Guard

	Original rule:
	l17 -> l9 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, (0 == 0 /\ retval^0 <= 0), cost: 1
	New rule:
	l17 -> l9 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, retval^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l17 -> l9 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, retval^0 <= 0, cost: 1
	New rule:
	l17 -> l9 : retval^0 <= 0, cost: 1
	
	made implied equalities explicit

	Original rule:
	l17 -> l16 : ___len21^0'=___len21^post28, ret_my_malloc10^0'=ret_my_malloc10^post28, ret_my_malloc14^0'=ret_my_malloc14^post28, retval^0'=retval^post28, size11^0'=size11^post28, size15^0'=size15^post28, size17^0'=size17^post28, size7^0'=size7^post28, tmp13^0'=tmp13^post28, tmp22^0'=tmp22^post28, tmp9^0'=tmp9^post28, tmp^0'=tmp^post28, tmp___0^0'=tmp___0^post28, tmp___1^0'=tmp___1^post28, (0 == 0 /\ retval^0-retval^post28 == 0 /\ -___len21^post28+___len21^0 == 0 /\ -tmp22^post28+tmp22^0 == 0 /\ -size7^post28+size7^0 == 0 /\ -tmp___1^post28+tmp___1^0 == 0 /\ size15^0-size15^post28 == 0 /\ -ret_my_malloc14^post28+ret_my_malloc14^0 == 0 /\ -100+size11^post28 == 0 /\ 1-retval^0 <= 0 /\ -1+retval^0 <= 0 /\ ret_my_malloc10^0-ret_my_malloc10^post28 == 0 /\ size17^0-size17^post28 == 0 /\ tmp9^0-tmp9^post28 == 0 /\ tmp^0-tmp^post28 == 0 /\ -tmp___0^post28+tmp___0^0 == 0), cost: 1
	New rule:
	l17 -> l16 : ___len21^0'=___len21^post28, ret_my_malloc10^0'=ret_my_malloc10^post28, ret_my_malloc14^0'=ret_my_malloc14^post28, retval^0'=retval^post28, size11^0'=size11^post28, size15^0'=size15^post28, size17^0'=size17^post28, size7^0'=size7^post28, tmp13^0'=tmp13^post28, tmp22^0'=tmp22^post28, tmp9^0'=tmp9^post28, tmp^0'=tmp^post28, tmp___0^0'=tmp___0^post28, tmp___1^0'=tmp___1^post28, (0 == 0 /\ retval^0-retval^post28 == 0 /\ -___len21^post28+___len21^0 == 0 /\ -tmp22^post28+tmp22^0 == 0 /\ -size7^post28+size7^0 == 0 /\ -tmp___1^post28+tmp___1^0 == 0 /\ size15^0-size15^post28 == 0 /\ -ret_my_malloc14^post28+ret_my_malloc14^0 == 0 /\ -100+size11^post28 == 0 /\ 1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0 /\ ret_my_malloc10^0-ret_my_malloc10^post28 == 0 /\ size17^0-size17^post28 == 0 /\ tmp9^0-tmp9^post28 == 0 /\ tmp^0-tmp^post28 == 0 /\ -tmp___0^post28+tmp___0^0 == 0), cost: 1
	
	Propagated Equalities

	Original rule:
	l17 -> l16 : ___len21^0'=___len21^post28, ret_my_malloc10^0'=ret_my_malloc10^post28, ret_my_malloc14^0'=ret_my_malloc14^post28, retval^0'=retval^post28, size11^0'=size11^post28, size15^0'=size15^post28, size17^0'=size17^post28, size7^0'=size7^post28, tmp13^0'=tmp13^post28, tmp22^0'=tmp22^post28, tmp9^0'=tmp9^post28, tmp^0'=tmp^post28, tmp___0^0'=tmp___0^post28, tmp___1^0'=tmp___1^post28, (0 == 0 /\ retval^0-retval^post28 == 0 /\ -___len21^post28+___len21^0 == 0 /\ -tmp22^post28+tmp22^0 == 0 /\ -size7^post28+size7^0 == 0 /\ -tmp___1^post28+tmp___1^0 == 0 /\ size15^0-size15^post28 == 0 /\ -ret_my_malloc14^post28+ret_my_malloc14^0 == 0 /\ -100+size11^post28 == 0 /\ 1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0 /\ ret_my_malloc10^0-ret_my_malloc10^post28 == 0 /\ size17^0-size17^post28 == 0 /\ tmp9^0-tmp9^post28 == 0 /\ tmp^0-tmp^post28 == 0 /\ -tmp___0^post28+tmp___0^0 == 0), cost: 1
	New rule:
	l17 -> l16 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=100, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^post28, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, (0 == 0 /\ 1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0), cost: 1
	
		propagated equality retval^post28 = retval^0
		
		propagated equality ___len21^post28 = ___len21^0
		
		propagated equality tmp22^post28 = tmp22^0
		
		propagated equality size7^post28 = size7^0
		
		propagated equality tmp___1^post28 = tmp___1^0
		
		propagated equality size15^post28 = size15^0
		
		propagated equality ret_my_malloc14^post28 = ret_my_malloc14^0
		
		propagated equality size11^post28 = 100
		
		propagated equality ret_my_malloc10^post28 = ret_my_malloc10^0
		
		propagated equality size17^post28 = size17^0
		
		propagated equality tmp9^post28 = tmp9^0
		
		propagated equality tmp^post28 = tmp^0
		
		propagated equality tmp___0^post28 = tmp___0^0
		
	Simplified Guard

	Original rule:
	l17 -> l16 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=100, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^post28, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, (0 == 0 /\ 1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0), cost: 1
	New rule:
	l17 -> l16 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=100, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^post28, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, (1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0), cost: 1
	
	made implied equalities explicit

	Original rule:
	l17 -> l16 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=100, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^post28, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, (1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0), cost: 1
	New rule:
	l17 -> l16 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=100, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^post28, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, (1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0), cost: 1
	
	Removed Trivial Updates

	Original rule:
	l17 -> l16 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=100, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^post28, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, (1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0), cost: 1
	New rule:
	l17 -> l16 : size11^0'=100, tmp13^0'=tmp13^post28, (1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0), cost: 1
	
	Propagated Equalities

	Original rule:
	l1 -> l17 : ___len21^0'=___len21^post29, ret_my_malloc10^0'=ret_my_malloc10^post29, ret_my_malloc14^0'=ret_my_malloc14^post29, retval^0'=retval^post29, size11^0'=size11^post29, size15^0'=size15^post29, size17^0'=size17^post29, size7^0'=size7^post29, tmp13^0'=tmp13^post29, tmp22^0'=tmp22^post29, tmp9^0'=tmp9^post29, tmp^0'=tmp^post29, tmp___0^0'=tmp___0^post29, tmp___1^0'=tmp___1^post29, (-ret_my_malloc14^post29+ret_my_malloc14^0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post29 == 0 /\ -tmp___0^post29+tmp___0^0 == 0 /\ -size15^post29+size15^0 == 0 /\ size17^0-size17^post29 == 0 /\ tmp13^0-tmp13^post29 == 0 /\ -tmp22^post29+tmp22^0 == 0 /\ -___len21^post29+___len21^0 == 0 /\ -tmp^post29+retval^post29 == 0 /\ tmp9^0-tmp9^post29 == 0 /\ size7^0-size7^post29 == 0 /\ -ret_my_malloc10^0+tmp^post29 == 0 /\ size11^0-size11^post29 == 0 /\ tmp___1^0-tmp___1^post29 == 0), cost: 1
	New rule:
	l1 -> l17 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=ret_my_malloc10^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=ret_my_malloc10^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1
	
		propagated equality ret_my_malloc14^post29 = ret_my_malloc14^0
		
		propagated equality ret_my_malloc10^post29 = ret_my_malloc10^0
		
		propagated equality tmp___0^post29 = tmp___0^0
		
		propagated equality size15^post29 = size15^0
		
		propagated equality size17^post29 = size17^0
		
		propagated equality tmp13^post29 = tmp13^0
		
		propagated equality tmp22^post29 = tmp22^0
		
		propagated equality ___len21^post29 = ___len21^0
		
		propagated equality retval^post29 = tmp^post29
		
		propagated equality tmp9^post29 = tmp9^0
		
		propagated equality size7^post29 = size7^0
		
		propagated equality tmp^post29 = ret_my_malloc10^0
		
		propagated equality size11^post29 = size11^0
		
		propagated equality tmp___1^post29 = tmp___1^0
		
	Simplified Guard

	Original rule:
	l1 -> l17 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=ret_my_malloc10^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=ret_my_malloc10^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1
	New rule:
	l1 -> l17 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=ret_my_malloc10^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=ret_my_malloc10^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l1 -> l17 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=ret_my_malloc10^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=size7^0, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^0, tmp^0'=ret_my_malloc10^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, T, cost: 1
	New rule:
	l1 -> l17 : retval^0'=ret_my_malloc10^0, tmp^0'=ret_my_malloc10^0, T, cost: 1
	
	Propagated Equalities

	Original rule:
	l19 -> l0 : ___len21^0'=___len21^post30, ret_my_malloc10^0'=ret_my_malloc10^post30, ret_my_malloc14^0'=ret_my_malloc14^post30, retval^0'=retval^post30, size11^0'=size11^post30, size15^0'=size15^post30, size17^0'=size17^post30, size7^0'=size7^post30, tmp13^0'=tmp13^post30, tmp22^0'=tmp22^post30, tmp9^0'=tmp9^post30, tmp^0'=tmp^post30, tmp___0^0'=tmp___0^post30, tmp___1^0'=tmp___1^post30, (0 == 0 /\ size17^0-size17^post31 == 0 /\ size15^post31-size15^post30 == 0 /\ -ret_my_malloc10^post31+ret_my_malloc10^0 == 0 /\ -tmp___1^post30+tmp___1^post31 == 0 /\ tmp13^0-tmp13^post31 == 0 /\ -tmp22^post31+tmp22^0 == 0 /\ -tmp^post31+tmp^0 == 0 /\ -retval^post30+retval^post31 == 0 /\ tmp^post31-tmp^post30 == 0 /\ tmp22^post31-tmp22^post30 == 0 /\ size7^0-size7^post31 == 0 /\ ret_my_malloc14^post31-ret_my_malloc14^post30 == 0 /\ -100+size7^post30 == 0 /\ -tmp___0^post30+tmp___0^post31 == 0 /\ -size11^post30+size11^post31 == 0 /\ -ret_my_malloc14^post31+ret_my_malloc14^0 == 0 /\ tmp___1^0-tmp___1^post31 == 0 /\ tmp13^post31-tmp13^post30 == 0 /\ -tmp___0^post31+tmp___0^0 == 0 /\ tmp9^0-tmp9^post31 == 0 /\ -___len21^post30+___len21^post31 == 0 /\ size11^0-size11^post31 == 0 /\ -___len21^post31+___len21^0 == 0 /\ retval^0-retval^post31 == 0 /\ ret_my_malloc10^post31-ret_my_malloc10^post30 == 0 /\ size17^post31-size17^post30 == 0 /\ -size15^post31+size15^0 == 0), cost: 1
	New rule:
	l19 -> l0 : ___len21^0'=___len21^post31, ret_my_malloc10^0'=ret_my_malloc10^post31, ret_my_malloc14^0'=ret_my_malloc14^post31, retval^0'=retval^post31, size11^0'=size11^post31, size15^0'=size15^post31, size17^0'=size17^post31, size7^0'=100, tmp13^0'=tmp13^post31, tmp22^0'=tmp22^post31, tmp9^0'=tmp9^post30, tmp^0'=tmp^post31, tmp___0^0'=tmp___0^post31, tmp___1^0'=tmp___1^post31, (0 == 0 /\ size17^0-size17^post31 == 0 /\ -ret_my_malloc10^post31+ret_my_malloc10^0 == 0 /\ tmp13^0-tmp13^post31 == 0 /\ -tmp22^post31+tmp22^0 == 0 /\ -tmp^post31+tmp^0 == 0 /\ size7^0-size7^post31 == 0 /\ -ret_my_malloc14^post31+ret_my_malloc14^0 == 0 /\ tmp___1^0-tmp___1^post31 == 0 /\ -tmp___0^post31+tmp___0^0 == 0 /\ tmp9^0-tmp9^post31 == 0 /\ size11^0-size11^post31 == 0 /\ -___len21^post31+___len21^0 == 0 /\ retval^0-retval^post31 == 0 /\ -size15^post31+size15^0 == 0), cost: 1
	
		propagated equality size15^post30 = size15^post31
		
		propagated equality tmp___1^post30 = tmp___1^post31
		
		propagated equality retval^post30 = retval^post31
		
		propagated equality tmp^post30 = tmp^post31
		
		propagated equality tmp22^post30 = tmp22^post31
		
		propagated equality ret_my_malloc14^post30 = ret_my_malloc14^post31
		
		propagated equality size7^post30 = 100
		
		propagated equality tmp___0^post30 = tmp___0^post31
		
		propagated equality size11^post30 = size11^post31
		
		propagated equality tmp13^post30 = tmp13^post31
		
		propagated equality ___len21^post30 = ___len21^post31
		
		propagated equality ret_my_malloc10^post30 = ret_my_malloc10^post31
		
		propagated equality size17^post30 = size17^post31
		
	Propagated Equalities

	Original rule:
	l19 -> l0 : ___len21^0'=___len21^post31, ret_my_malloc10^0'=ret_my_malloc10^post31, ret_my_malloc14^0'=ret_my_malloc14^post31, retval^0'=retval^post31, size11^0'=size11^post31, size15^0'=size15^post31, size17^0'=size17^post31, size7^0'=100, tmp13^0'=tmp13^post31, tmp22^0'=tmp22^post31, tmp9^0'=tmp9^post30, tmp^0'=tmp^post31, tmp___0^0'=tmp___0^post31, tmp___1^0'=tmp___1^post31, (0 == 0 /\ size17^0-size17^post31 == 0 /\ -ret_my_malloc10^post31+ret_my_malloc10^0 == 0 /\ tmp13^0-tmp13^post31 == 0 /\ -tmp22^post31+tmp22^0 == 0 /\ -tmp^post31+tmp^0 == 0 /\ size7^0-size7^post31 == 0 /\ -ret_my_malloc14^post31+ret_my_malloc14^0 == 0 /\ tmp___1^0-tmp___1^post31 == 0 /\ -tmp___0^post31+tmp___0^0 == 0 /\ tmp9^0-tmp9^post31 == 0 /\ size11^0-size11^post31 == 0 /\ -___len21^post31+___len21^0 == 0 /\ retval^0-retval^post31 == 0 /\ -size15^post31+size15^0 == 0), cost: 1
	New rule:
	l19 -> l0 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=100, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^post30, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1
	
		propagated equality size17^post31 = size17^0
		
		propagated equality ret_my_malloc10^post31 = ret_my_malloc10^0
		
		propagated equality tmp13^post31 = tmp13^0
		
		propagated equality tmp22^post31 = tmp22^0
		
		propagated equality tmp^post31 = tmp^0
		
		propagated equality size7^post31 = size7^0
		
		propagated equality ret_my_malloc14^post31 = ret_my_malloc14^0
		
		propagated equality tmp___1^post31 = tmp___1^0
		
		propagated equality tmp___0^post31 = tmp___0^0
		
		propagated equality tmp9^post31 = tmp9^0
		
		propagated equality size11^post31 = size11^0
		
		propagated equality ___len21^post31 = ___len21^0
		
		propagated equality retval^post31 = retval^0
		
		propagated equality size15^post31 = size15^0
		
	Simplified Guard

	Original rule:
	l19 -> l0 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=100, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^post30, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1
	New rule:
	l19 -> l0 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=100, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^post30, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l19 -> l0 : ___len21^0'=___len21^0, ret_my_malloc10^0'=ret_my_malloc10^0, ret_my_malloc14^0'=ret_my_malloc14^0, retval^0'=retval^0, size11^0'=size11^0, size15^0'=size15^0, size17^0'=size17^0, size7^0'=100, tmp13^0'=tmp13^0, tmp22^0'=tmp22^0, tmp9^0'=tmp9^post30, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, T, cost: 1
	New rule:
	l19 -> l0 : size7^0'=100, tmp9^0'=tmp9^post30, T, cost: 1

Step with 61

	Trace

	61[T]
	
	Blocked

	[{}, {}]

Step with 32

	Trace

	61[T], 32[T]
	
	Blocked

	[{}, {}, {}]

Step with 60

	Trace

	61[T], 32[T], 60[T]
	
	Blocked

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

Step with 58

	Trace

	61[T], 32[T], 60[T], 58[(retval^0 <= 0)]
	
	Blocked

	[{}, {}, {}, {57[T]}, {}]

Step with 44

	Trace

	61[T], 32[T], 60[T], 58[(retval^0 <= 0)], 44[T]
	
	Blocked

	[{}, {}, {}, {57[T]}, {}, {}]

Step with 41

	Trace

	61[T], 32[T], 60[T], 58[(retval^0 <= 0)], 44[T], 41[T]
	
	Blocked

	[{}, {}, {}, {57[T]}, {}, {}, {}]

Step with 40

	Trace

	61[T], 32[T], 60[T], 58[(retval^0 <= 0)], 44[T], 41[T], 40[T]
	
	Blocked

	[{}, {}, {}, {57[T]}, {}, {}, {}, {}]

Step with 39

	Trace

	61[T], 32[T], 60[T], 58[(retval^0 <= 0)], 44[T], 41[T], 40[T], 39[T]
	
	Blocked

	[{}, {}, {}, {57[T]}, {}, {}, {}, {}, {}]

Backtrack

	Trace

	61[T], 32[T], 60[T], 58[(retval^0 <= 0)], 44[T], 41[T], 40[T]
	
	Blocked

	[{}, {}, {}, {57[T]}, {}, {}, {}, {39[T]}]

Backtrack

	Trace

	61[T], 32[T], 60[T], 58[(retval^0 <= 0)], 44[T], 41[T]
	
	Blocked

	[{}, {}, {}, {57[T]}, {}, {}, {40[T]}]

Backtrack

	Trace

	61[T], 32[T], 60[T], 58[(retval^0 <= 0)], 44[T]
	
	Blocked

	[{}, {}, {}, {57[T]}, {}, {41[T]}]

Step with 42

	Trace

	61[T], 32[T], 60[T], 58[(retval^0 <= 0)], 44[T], 42[T]
	
	Blocked

	[{}, {}, {}, {57[T]}, {}, {41[T]}, {}]

Step with 39

	Trace

	61[T], 32[T], 60[T], 58[(retval^0 <= 0)], 44[T], 42[T], 39[T]
	
	Blocked

	[{}, {}, {}, {57[T]}, {}, {41[T]}, {}, {}]

Backtrack

	Trace

	61[T], 32[T], 60[T], 58[(retval^0 <= 0)], 44[T], 42[T]
	
	Blocked

	[{}, {}, {}, {57[T]}, {}, {41[T]}, {39[T]}]

Backtrack

	Trace

	61[T], 32[T], 60[T], 58[(retval^0 <= 0)], 44[T]
	
	Blocked

	[{}, {}, {}, {57[T]}, {}, {41[T], 42[T]}]

Step with 43

	Trace

	61[T], 32[T], 60[T], 58[(retval^0 <= 0)], 44[T], 43[T]
	
	Blocked

	[{}, {}, {}, {57[T]}, {}, {41[T], 42[T]}, {}]

Step with 40

	Trace

	61[T], 32[T], 60[T], 58[(retval^0 <= 0)], 44[T], 43[T], 40[T]
	
	Blocked

	[{}, {}, {}, {57[T]}, {}, {41[T], 42[T]}, {}, {}]

Step with 39

	Trace

	61[T], 32[T], 60[T], 58[(retval^0 <= 0)], 44[T], 43[T], 40[T], 39[T]
	
	Blocked

	[{}, {}, {}, {57[T]}, {}, {41[T], 42[T]}, {}, {}, {}]

Backtrack

	Trace

	61[T], 32[T], 60[T], 58[(retval^0 <= 0)], 44[T], 43[T], 40[T]
	
	Blocked

	[{}, {}, {}, {57[T]}, {}, {41[T], 42[T]}, {}, {39[T]}]

Backtrack

	Trace

	61[T], 32[T], 60[T], 58[(retval^0 <= 0)], 44[T], 43[T]
	
	Blocked

	[{}, {}, {}, {57[T]}, {}, {41[T], 42[T]}, {40[T]}]

Backtrack

	Trace

	61[T], 32[T], 60[T], 58[(retval^0 <= 0)], 44[T]
	
	Blocked

	[{}, {}, {}, {57[T]}, {}, {41[T], 42[T], 43[T]}]

Backtrack

	Trace

	61[T], 32[T], 60[T], 58[(retval^0 <= 0)]
	
	Blocked

	[{}, {}, {}, {57[T]}, {44[T]}]

Backtrack

	Trace

	61[T], 32[T], 60[T]
	
	Blocked

	[{}, {}, {}, {57[T], 58[T]}]

Backtrack

	Trace

	61[T], 32[T]
	
	Blocked

	[{}, {}, {60[T]}]

Backtrack

	Trace

	61[T]
	
	Blocked

	[{}, {32[T]}]

Step with 33

	Trace

	61[T], 33[T]
	
	Blocked

	[{}, {32[T]}, {}]

Step with 60

	Trace

	61[T], 33[T], 60[T]
	
	Blocked

	[{}, {32[T]}, {}, {}]

Step with 59

	Trace

	61[T], 33[T], 60[T], 59[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)]
	
	Blocked

	[{}, {32[T]}, {}, {58[T]}, {}]

Step with 55

	Trace

	61[T], 33[T], 60[T], 59[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 55[T]
	
	Blocked

	[{}, {32[T]}, {}, {58[T]}, {}, {}]

Step with 51

	Trace

	61[T], 33[T], 60[T], 59[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 55[T], 51[T]
	
	Blocked

	[{}, {32[T]}, {}, {58[T]}, {}, {}, {}]

Step with 54

	Trace

	61[T], 33[T], 60[T], 59[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 55[T], 51[T], 54[(retval^0 <= 0)]
	
	Blocked

	[{}, {32[T]}, {}, {58[T]}, {}, {}, {52[T], 53[T]}, {}]

Step with 50

	Trace

	61[T], 33[T], 60[T], 59[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 55[T], 51[T], 54[(retval^0 <= 0)], 50[T]
	
	Blocked

	[{}, {32[T]}, {}, {58[T]}, {}, {}, {52[T], 53[T]}, {}, {}]

Step with 47

	Trace

	61[T], 33[T], 60[T], 59[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 55[T], 51[T], 54[(retval^0 <= 0)], 50[T], 47[T]
	
	Blocked

	[{}, {32[T]}, {}, {58[T]}, {}, {}, {52[T], 53[T]}, {}, {}, {}]

Step with 46

	Trace

	61[T], 33[T], 60[T], 59[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 55[T], 51[T], 54[(retval^0 <= 0)], 50[T], 47[T], 46[T]
	
	Blocked

	[{}, {32[T]}, {}, {58[T]}, {}, {}, {52[T], 53[T]}, {}, {}, {}, {}]

Step with 45

	Trace

	61[T], 33[T], 60[T], 59[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 55[T], 51[T], 54[(retval^0 <= 0)], 50[T], 47[T], 46[T], 45[T]
	
	Blocked

	[{}, {32[T]}, {}, {58[T]}, {}, {}, {52[T], 53[T]}, {}, {}, {}, {}, {}]

Backtrack

	Trace

	61[T], 33[T], 60[T], 59[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 55[T], 51[T], 54[(retval^0 <= 0)], 50[T], 47[T], 46[T]
	
	Blocked

	[{}, {32[T]}, {}, {58[T]}, {}, {}, {52[T], 53[T]}, {}, {}, {}, {45[T]}]

Backtrack

	Trace

	61[T], 33[T], 60[T], 59[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 55[T], 51[T], 54[(retval^0 <= 0)], 50[T], 47[T]
	
	Blocked

	[{}, {32[T]}, {}, {58[T]}, {}, {}, {52[T], 53[T]}, {}, {}, {46[T]}]

Backtrack

	Trace

	61[T], 33[T], 60[T], 59[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 55[T], 51[T], 54[(retval^0 <= 0)], 50[T]
	
	Blocked

	[{}, {32[T]}, {}, {58[T]}, {}, {}, {52[T], 53[T]}, {}, {47[T]}]

Step with 48

	Trace

	61[T], 33[T], 60[T], 59[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 55[T], 51[T], 54[(retval^0 <= 0)], 50[T], 48[T]
	
	Blocked

	[{}, {32[T]}, {}, {58[T]}, {}, {}, {52[T], 53[T]}, {}, {47[T]}, {}]

Step with 45

	Trace

	61[T], 33[T], 60[T], 59[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 55[T], 51[T], 54[(retval^0 <= 0)], 50[T], 48[T], 45[T]
	
	Blocked

	[{}, {32[T]}, {}, {58[T]}, {}, {}, {52[T], 53[T]}, {}, {47[T]}, {}, {}]

Backtrack

	Trace

	61[T], 33[T], 60[T], 59[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 55[T], 51[T], 54[(retval^0 <= 0)], 50[T], 48[T]
	
	Blocked

	[{}, {32[T]}, {}, {58[T]}, {}, {}, {52[T], 53[T]}, {}, {47[T]}, {45[T]}]

Backtrack

	Trace

	61[T], 33[T], 60[T], 59[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 55[T], 51[T], 54[(retval^0 <= 0)], 50[T]
	
	Blocked

	[{}, {32[T]}, {}, {58[T]}, {}, {}, {52[T], 53[T]}, {}, {47[T], 48[T]}]

Step with 49

	Trace

	61[T], 33[T], 60[T], 59[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 55[T], 51[T], 54[(retval^0 <= 0)], 50[T], 49[T]
	
	Blocked

	[{}, {32[T]}, {}, {58[T]}, {}, {}, {52[T], 53[T]}, {}, {47[T], 48[T]}, {}]

Step with 46

	Trace

	61[T], 33[T], 60[T], 59[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 55[T], 51[T], 54[(retval^0 <= 0)], 50[T], 49[T], 46[T]
	
	Blocked

	[{}, {32[T]}, {}, {58[T]}, {}, {}, {52[T], 53[T]}, {}, {47[T], 48[T]}, {}, {}]

Step with 45

	Trace

	61[T], 33[T], 60[T], 59[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 55[T], 51[T], 54[(retval^0 <= 0)], 50[T], 49[T], 46[T], 45[T]
	
	Blocked

	[{}, {32[T]}, {}, {58[T]}, {}, {}, {52[T], 53[T]}, {}, {47[T], 48[T]}, {}, {}, {}]

Backtrack

	Trace

	61[T], 33[T], 60[T], 59[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 55[T], 51[T], 54[(retval^0 <= 0)], 50[T], 49[T], 46[T]
	
	Blocked

	[{}, {32[T]}, {}, {58[T]}, {}, {}, {52[T], 53[T]}, {}, {47[T], 48[T]}, {}, {45[T]}]

Backtrack

	Trace

	61[T], 33[T], 60[T], 59[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 55[T], 51[T], 54[(retval^0 <= 0)], 50[T], 49[T]
	
	Blocked

	[{}, {32[T]}, {}, {58[T]}, {}, {}, {52[T], 53[T]}, {}, {47[T], 48[T]}, {46[T]}]

Backtrack

	Trace

	61[T], 33[T], 60[T], 59[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 55[T], 51[T], 54[(retval^0 <= 0)], 50[T]
	
	Blocked

	[{}, {32[T]}, {}, {58[T]}, {}, {}, {52[T], 53[T]}, {}, {47[T], 48[T], 49[T]}]

Backtrack

	Trace

	61[T], 33[T], 60[T], 59[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 55[T], 51[T], 54[(retval^0 <= 0)]
	
	Blocked

	[{}, {32[T]}, {}, {58[T]}, {}, {}, {52[T], 53[T]}, {50[T]}]

Backtrack

	Trace

	61[T], 33[T], 60[T], 59[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 55[T], 51[T]
	
	Blocked

	[{}, {32[T]}, {}, {58[T]}, {}, {}, {52[T], 53[T], 54[T]}]

Backtrack

	Trace

	61[T], 33[T], 60[T], 59[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 55[T]
	
	Blocked

	[{}, {32[T]}, {}, {58[T]}, {}, {51[T]}]

Backtrack

	Trace

	61[T], 33[T], 60[T], 59[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)]
	
	Blocked

	[{}, {32[T]}, {}, {58[T]}, {55[T]}]

Step with 56

	Trace

	61[T], 33[T], 60[T], 59[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 56[T]
	
	Blocked

	[{}, {32[T]}, {}, {58[T]}, {55[T]}, {}]

Step with 51

	Trace

	61[T], 33[T], 60[T], 59[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 56[T], 51[T]
	
	Blocked

	[{}, {32[T]}, {}, {58[T]}, {55[T]}, {}, {}]

Step with 52

	Trace

	61[T], 33[T], 60[T], 59[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 56[T], 51[T], 52[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)]
	
	Blocked

	[{}, {32[T]}, {}, {58[T]}, {55[T]}, {}, {54[T]}, {}]

Step with 36

	Trace

	61[T], 33[T], 60[T], 59[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 56[T], 51[T], 52[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 36[(1+tmp___1^0 <= 0 /\ 1+tmp___1^0 == 0 /\ -1-tmp___1^0 <= 0)]
	
	Blocked

	[{}, {32[T]}, {}, {58[T]}, {55[T]}, {}, {54[T]}, {}, {}]

Step with 34

	Trace

	61[T], 33[T], 60[T], 59[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 56[T], 51[T], 52[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 36[(1+tmp___1^0 <= 0 /\ 1+tmp___1^0 == 0 /\ -1-tmp___1^0 <= 0)], 34[T]
	
	Blocked

	[{}, {32[T]}, {}, {58[T]}, {55[T]}, {}, {54[T]}, {}, {}, {}]

Backtrack

	Trace

	61[T], 33[T], 60[T], 59[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 56[T], 51[T], 52[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 36[(1+tmp___1^0 <= 0 /\ 1+tmp___1^0 == 0 /\ -1-tmp___1^0 <= 0)]
	
	Blocked

	[{}, {32[T]}, {}, {58[T]}, {55[T]}, {}, {54[T]}, {}, {34[T]}]

Backtrack

	Trace

	61[T], 33[T], 60[T], 59[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 56[T], 51[T], 52[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)]
	
	Blocked

	[{}, {32[T]}, {}, {58[T]}, {55[T]}, {}, {54[T]}, {36[T]}]

Step with 37

	Trace

	61[T], 33[T], 60[T], 59[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 56[T], 51[T], 52[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 37[(-tmp___1^0 <= 0)]
	
	Blocked

	[{}, {32[T]}, {}, {58[T]}, {55[T]}, {}, {54[T]}, {36[T]}, {}]

Step with 35

	Trace

	61[T], 33[T], 60[T], 59[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 56[T], 51[T], 52[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 37[(-tmp___1^0 <= 0)], 35[T]
	
	Blocked

	[{}, {32[T]}, {}, {58[T]}, {55[T]}, {}, {54[T]}, {36[T]}, {}, {}]

Step with 34

	Trace

	61[T], 33[T], 60[T], 59[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 56[T], 51[T], 52[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 37[(-tmp___1^0 <= 0)], 35[T], 34[T]
	
	Blocked

	[{}, {32[T]}, {}, {58[T]}, {55[T]}, {}, {54[T]}, {36[T]}, {}, {}, {}]

Backtrack

	Trace

	61[T], 33[T], 60[T], 59[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 56[T], 51[T], 52[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 37[(-tmp___1^0 <= 0)], 35[T]
	
	Blocked

	[{}, {32[T]}, {}, {58[T]}, {55[T]}, {}, {54[T]}, {36[T]}, {}, {34[T]}]

Backtrack

	Trace

	61[T], 33[T], 60[T], 59[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 56[T], 51[T], 52[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 37[(-tmp___1^0 <= 0)]
	
	Blocked

	[{}, {32[T]}, {}, {58[T]}, {55[T]}, {}, {54[T]}, {36[T]}, {35[T]}]

Backtrack

	Trace

	61[T], 33[T], 60[T], 59[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 56[T], 51[T], 52[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)]
	
	Blocked

	[{}, {32[T]}, {}, {58[T]}, {55[T]}, {}, {54[T]}, {36[T], 37[T]}]

Step with 38

	Trace

	61[T], 33[T], 60[T], 59[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 56[T], 51[T], 52[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 38[(2+tmp___1^0 <= 0)]
	
	Blocked

	[{}, {32[T]}, {}, {58[T]}, {55[T]}, {}, {54[T]}, {36[T], 37[T]}, {}]

Step with 35

	Trace

	61[T], 33[T], 60[T], 59[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 56[T], 51[T], 52[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 38[(2+tmp___1^0 <= 0)], 35[T]
	
	Blocked

	[{}, {32[T]}, {}, {58[T]}, {55[T]}, {}, {54[T]}, {36[T], 37[T]}, {}, {}]

Step with 34

	Trace

	61[T], 33[T], 60[T], 59[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 56[T], 51[T], 52[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 38[(2+tmp___1^0 <= 0)], 35[T], 34[T]
	
	Blocked

	[{}, {32[T]}, {}, {58[T]}, {55[T]}, {}, {54[T]}, {36[T], 37[T]}, {}, {}, {}]

Backtrack

	Trace

	61[T], 33[T], 60[T], 59[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 56[T], 51[T], 52[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 38[(2+tmp___1^0 <= 0)], 35[T]
	
	Blocked

	[{}, {32[T]}, {}, {58[T]}, {55[T]}, {}, {54[T]}, {36[T], 37[T]}, {}, {34[T]}]

Backtrack

	Trace

	61[T], 33[T], 60[T], 59[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 56[T], 51[T], 52[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 38[(2+tmp___1^0 <= 0)]
	
	Blocked

	[{}, {32[T]}, {}, {58[T]}, {55[T]}, {}, {54[T]}, {36[T], 37[T]}, {35[T]}]

Backtrack

	Trace

	61[T], 33[T], 60[T], 59[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 56[T], 51[T], 52[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)]
	
	Blocked

	[{}, {32[T]}, {}, {58[T]}, {55[T]}, {}, {54[T]}, {36[T], 37[T], 38[T]}]

Backtrack

	Trace

	61[T], 33[T], 60[T], 59[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 56[T], 51[T]
	
	Blocked

	[{}, {32[T]}, {}, {58[T]}, {55[T]}, {}, {52[T], 54[T]}]

Backtrack

	Trace

	61[T], 33[T], 60[T], 59[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)], 56[T]
	
	Blocked

	[{}, {32[T]}, {}, {58[T]}, {55[T]}, {51[T]}]

Backtrack

	Trace

	61[T], 33[T], 60[T], 59[(1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0)]
	
	Blocked

	[{}, {32[T]}, {}, {58[T]}, {55[T], 56[T]}]

Backtrack

	Trace

	61[T], 33[T], 60[T]
	
	Blocked

	[{}, {32[T]}, {}, {58[T], 59[T]}]

Backtrack

	Trace

	61[T], 33[T]
	
	Blocked

	[{}, {32[T]}, {60[T]}]

Backtrack

	Trace

	61[T]
	
	Blocked

	[{}, {32[T], 33[T]}]

Backtrack

	Trace

	Blocked

	[{61[T]}]

Accept

unknown

Build SHA: a05f16bf13df659c382799650051f91bf6828c7b