WORST_CASE(Omega(0),?)

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


Removed unreachable rules and leafs
Start location: l19
  <empty>


Computing asymptotic complexity

Proved the following lower bound
Complexity:  Unknown
Cpx degree: ?

Solved cost: 0
Rule cost:   0