unknown Initial ITS Start location: l19 Program variables: __const_100^0 __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 : __const_100^0'=__const_100^post1, __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, (-size17^post1+size17^0 == 0 /\ size15^0-size15^post1 == 0 /\ -__len21^post1+__len21^0 == 0 /\ -tmp___0^post1+tmp___0^0 == 0 /\ size11^0-size11^post1 == 0 /\ -tmp13^post1+tmp13^0 == 0 /\ -tmp9^post1+tmp9^0 == 0 /\ -retval^post1+retval^0 == 0 /\ tmp___1^0-tmp___1^post1 == 0 /\ tmp^0-tmp^post1 == 0 /\ size7^0-size7^post1 == 0 /\ -__const_100^post1+__const_100^0 == 0 /\ tmp22^0-tmp22^post1 == 0 /\ ret_my_malloc10^post1 == 0 /\ -ret_my_malloc14^post1+ret_my_malloc14^0 == 0), cost: 1 1: l0 -> l1 : __const_100^0'=__const_100^post2, __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, (-size17^post2+size17^0 == 0 /\ tmp^0-tmp^post2 == 0 /\ -tmp___0^post2+tmp___0^0 == 0 /\ -__len21^post2+__len21^0 == 0 /\ -1+ret_my_malloc10^post2 == 0 /\ size7^0-size7^post2 == 0 /\ tmp___1^0-tmp___1^post2 == 0 /\ -retval^post2+retval^0 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post2 == 0 /\ __const_100^0-__const_100^post2 == 0 /\ tmp13^0-tmp13^post2 == 0 /\ -tmp9^post2+tmp9^0 == 0 /\ size15^0-size15^post2 == 0 /\ size11^0-size11^post2 == 0 /\ -tmp22^post2+tmp22^0 == 0), cost: 1 28: l1 -> l17 : __const_100^0'=__const_100^post29, __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_malloc10^0-ret_my_malloc10^post29 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post29 == 0 /\ -tmp___0^post29+tmp___0^0 == 0 /\ tmp___1^0-tmp___1^post29 == 0 /\ -__const_100^post29+__const_100^0 == 0 /\ tmp22^0-tmp22^post29 == 0 /\ size15^0-size15^post29 == 0 /\ __len21^0-__len21^post29 == 0 /\ -tmp9^post29+tmp9^0 == 0 /\ size7^0-size7^post29 == 0 /\ size11^0-size11^post29 == 0 /\ -size17^post29+size17^0 == 0 /\ -tmp13^post29+tmp13^0 == 0 /\ -tmp^post29+retval^post29 == 0 /\ tmp^post29-ret_my_malloc10^0 == 0), cost: 1 2: l2 -> l3 : __const_100^0'=__const_100^post3, __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, (-__const_100^post3+__const_100^0 == 0 /\ -__len21^post3+__len21^0 == 0 /\ tmp^0-tmp^post3 == 0 /\ size7^0-size7^post3 == 0 /\ -ret_my_malloc10^post3+ret_my_malloc10^0 == 0 /\ -size17^post3+size17^0 == 0 /\ -retval^post3+retval^0 == 0 /\ tmp___1^0-tmp___1^post3 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post3 == 0 /\ tmp13^0-tmp13^post3 == 0 /\ size15^0-size15^post3 == 0 /\ -tmp9^post3+tmp9^0 == 0 /\ tmp___0^0-tmp___0^post3 == 0 /\ -tmp22^post3+tmp22^0 == 0 /\ size11^0-size11^post3 == 0), cost: 1 3: l4 -> l2 : __const_100^0'=__const_100^post4, __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 /\ -__len21^post4+__len21^0 == 0 /\ size15^0-size15^post4 == 0 /\ -ret_my_malloc10^post4+ret_my_malloc10^0 == 0 /\ -size7^post4+size7^0 == 0 /\ -tmp___1^post4+tmp___1^0 == 0 /\ -tmp9^post4+tmp9^0 == 0 /\ -tmp13^post4+tmp13^0 == 0 /\ size17^0-size17^post4 == 0 /\ tmp^0-tmp^post4 == 0 /\ -__const_100^post4+__const_100^0 == 0 /\ -size11^post4+size11^0 == 0 /\ retval^0-retval^post4 == 0 /\ tmp22^0-tmp22^post4 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post4 == 0), cost: 1 4: l5 -> l2 : __const_100^0'=__const_100^post5, __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 /\ size15^0-size15^post5 == 0 /\ -size17^post5+size17^0 == 0 /\ -tmp___0^post5+tmp___0^0 == 0 /\ __len21^post5-__const_100^0 == 0 /\ size11^0-size11^post5 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post5 == 0 /\ -retval^post5+retval^0 == 0 /\ -tmp9^post5+tmp9^0 == 0 /\ -tmp13^post5+tmp13^0 == 0 /\ 1+tmp___1^0 <= 0 /\ -1-tmp___1^0 <= 0 /\ size7^0-size7^post5 == 0 /\ tmp^0-tmp^post5 == 0 /\ -__const_100^post5+__const_100^0 == 0 /\ tmp___1^0-tmp___1^post5 == 0 /\ -ret_my_malloc14^post5+ret_my_malloc14^0 == 0), cost: 1 5: l5 -> l4 : __const_100^0'=__const_100^post6, __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, (tmp^0-tmp^post6 == 0 /\ -tmp___0^post6+tmp___0^0 == 0 /\ size7^0-size7^post6 == 0 /\ -size17^post6+size17^0 == 0 /\ -tmp___1^0 <= 0 /\ ret_my_malloc14^0-ret_my_malloc14^post6 == 0 /\ -tmp9^post6+tmp9^0 == 0 /\ -retval^post6+retval^0 == 0 /\ tmp13^0-tmp13^post6 == 0 /\ tmp___1^0-tmp___1^post6 == 0 /\ size15^0-size15^post6 == 0 /\ -ret_my_malloc10^post6+ret_my_malloc10^0 == 0 /\ size11^0-size11^post6 == 0 /\ -__const_100^post6+__const_100^0 == 0 /\ -__len21^post6+__len21^0 == 0 /\ -tmp22^post6+tmp22^0 == 0), cost: 1 6: l5 -> l4 : __const_100^0'=__const_100^post7, __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, (tmp^0-tmp^post7 == 0 /\ size7^0-size7^post7 == 0 /\ -retval^post7+retval^0 == 0 /\ size11^0-size11^post7 == 0 /\ tmp___1^0-tmp___1^post7 == 0 /\ -tmp22^post7+tmp22^0 == 0 /\ tmp13^0-tmp13^post7 == 0 /\ -tmp9^post7+tmp9^0 == 0 /\ -ret_my_malloc10^post7+ret_my_malloc10^0 == 0 /\ tmp___0^0-tmp___0^post7 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post7 == 0 /\ -__const_100^post7+__const_100^0 == 0 /\ size15^0-size15^post7 == 0 /\ -size17^post7+size17^0 == 0 /\ __len21^0-__len21^post7 == 0 /\ 2+tmp___1^0 <= 0), cost: 1 7: l6 -> l3 : __const_100^0'=__const_100^post8, __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, (tmp___0^0-tmp___0^post8 == 0 /\ size15^0-size15^post8 == 0 /\ -size11^post8+size11^0 == 0 /\ -size7^post8+size7^0 == 0 /\ -tmp___1^post8+tmp___1^0 == 0 /\ -tmp13^post8+tmp13^0 == 0 /\ -tmp9^post8+tmp9^0 == 0 /\ -__const_100^post8+__const_100^0 == 0 /\ tmp^0-tmp^post8 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post8 == 0 /\ -ret_my_malloc10^post8+ret_my_malloc10^0 == 0 /\ -retval^post8+retval^0 == 0 /\ __len21^0-__len21^post8 == 0 /\ tmp22^0-tmp22^post8 == 0 /\ size17^0-size17^post8 == 0), cost: 1 8: l7 -> l6 : __const_100^0'=__const_100^post9, __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, (size15^0-size15^post9 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post9 == 0 /\ -size17^post9+size17^0 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post9 == 0 /\ __len21^0-__len21^post9 == 0 /\ size11^0-size11^post9 == 0 /\ -tmp13^post9+tmp13^0 == 0 /\ -__const_100^post9+__const_100^0 == 0 /\ tmp^0-tmp^post9 == 0 /\ -tmp9^post9+tmp9^0 == 0 /\ size7^0-size7^post9 == 0 /\ -retval^post9+retval^0 == 0 /\ tmp22^0-tmp22^post9 == 0 /\ -tmp___0^post9+tmp___0^0 == 0 /\ tmp___1^0-tmp___1^post9 == 0), cost: 1 9: l8 -> l7 : __const_100^0'=__const_100^post10, __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, (tmp^0-tmp^post10 == 0 /\ size7^0-size7^post10 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post10 == 0 /\ -size17^post10+size17^0 == 0 /\ size15^0-size15^post10 == 0 /\ -size11^post10+size11^0 == 0 /\ tmp13^0-tmp13^post10 == 0 /\ tmp___1^0-tmp___1^post10 == 0 /\ -ret_my_malloc10^post10+ret_my_malloc10^0 == 0 /\ -tmp22^post10+tmp22^0 == 0 /\ tmp___0^0-tmp___0^post10 == 0 /\ -tmp9^post10+tmp9^0 == 0 /\ -__const_100^post10+__const_100^0 == 0 /\ -__len21^post10+__len21^0 == 0 /\ -retval^post10+retval^0 == 0), cost: 1 10: l8 -> l6 : __const_100^0'=__const_100^post11, __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, (tmp^0-tmp^post11 == 0 /\ -size7^post11+size7^0 == 0 /\ -size11^post11+size11^0 == 0 /\ tmp___1^0-tmp___1^post11 == 0 /\ -ret_my_malloc10^post11+ret_my_malloc10^0 == 0 /\ tmp___0^0-tmp___0^post11 == 0 /\ tmp13^0-tmp13^post11 == 0 /\ retval^0-retval^post11 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post11 == 0 /\ -size17^post11+size17^0 == 0 /\ -tmp22^post11+tmp22^0 == 0 /\ -__const_100^post11+__const_100^0 == 0 /\ -tmp9^post11+tmp9^0 == 0 /\ size15^0-size15^post11 == 0 /\ __len21^0-__len21^post11 == 0), cost: 1 11: l8 -> l7 : __const_100^0'=__const_100^post12, __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^0-tmp___0^post12 == 0 /\ -size17^post12+size17^0 == 0 /\ -tmp___1^post12+tmp___1^0 == 0 /\ -tmp13^post12+tmp13^0 == 0 /\ tmp^0-tmp^post12 == 0 /\ -__const_100^post12+__const_100^0 == 0 /\ -ret_my_malloc10^post12+ret_my_malloc10^0 == 0 /\ -retval^post12+retval^0 == 0 /\ -tmp9^post12+tmp9^0 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post12 == 0 /\ -size11^post12+size11^0 == 0 /\ -size7^post12+size7^0 == 0 /\ __len21^0-__len21^post12 == 0 /\ size15^0-size15^post12 == 0 /\ tmp22^0-tmp22^post12 == 0), cost: 1 12: l9 -> l8 : __const_100^0'=__const_100^post13, __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, (-tmp13^post13+tmp13^0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post13 == 0 /\ size11^0-size11^post13 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post13 == 0 /\ __len21^0-__len21^post13 == 0 /\ size7^0-size7^post13 == 0 /\ size17^post13-__const_100^0 == 0 /\ size15^0-size15^post13 == 0 /\ -tmp9^post13+tmp9^0 == 0 /\ tmp^0-tmp^post13 == 0 /\ -__const_100^post13+__const_100^0 == 0 /\ -retval^post13+retval^0 == 0 /\ -tmp___0^post13+tmp___0^0 == 0 /\ tmp22^0-tmp22^post13 == 0 /\ tmp___1^0-tmp___1^post13 == 0), cost: 1 13: l10 -> l3 : __const_100^0'=__const_100^post14, __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, (tmp^0-tmp^post14 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post14 == 0 /\ size15^0-size15^post14 == 0 /\ -size11^post14+size11^0 == 0 /\ tmp___1^0-tmp___1^post14 == 0 /\ -__len21^post14+__len21^0 == 0 /\ -tmp9^post14+tmp9^0 == 0 /\ tmp___0^0-tmp___0^post14 == 0 /\ tmp22^0-tmp22^post14 == 0 /\ -__const_100^post14+__const_100^0 == 0 /\ -size17^post14+size17^0 == 0 /\ -size7^post14+size7^0 == 0 /\ -ret_my_malloc10^post14+ret_my_malloc10^0 == 0 /\ -retval^post14+retval^0 == 0 /\ -tmp13^post14+tmp13^0 == 0), cost: 1 14: l11 -> l10 : __const_100^0'=__const_100^post15, __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, (tmp9^0-tmp9^post15 == 0 /\ tmp___1^0-tmp___1^post15 == 0 /\ -tmp13^post15+tmp13^0 == 0 /\ tmp22^0-tmp22^post15 == 0 /\ -size11^post15+size11^0 == 0 /\ -tmp___0^post15+tmp___0^0 == 0 /\ -__const_100^post15+__const_100^0 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post15 == 0 /\ -size7^post15+size7^0 == 0 /\ -size17^post15+size17^0 == 0 /\ -ret_my_malloc10^post15+ret_my_malloc10^0 == 0 /\ size15^0-size15^post15 == 0 /\ __len21^0-__len21^post15 == 0 /\ -retval^post15+retval^0 == 0 /\ tmp^0-tmp^post15 == 0), cost: 1 15: l12 -> l11 : __const_100^0'=__const_100^post16, __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, (-__len21^post16+__len21^0 == 0 /\ -tmp13^post16+tmp13^0 == 0 /\ -tmp9^post16+tmp9^0 == 0 /\ size15^0-size15^post16 == 0 /\ tmp___1^0-tmp___1^post16 == 0 /\ -size11^post16+size11^0 == 0 /\ -retval^post16+retval^0 == 0 /\ size17^0-size17^post16 == 0 /\ tmp^0-tmp^post16 == 0 /\ tmp___0^0-tmp___0^post16 == 0 /\ tmp22^0-tmp22^post16 == 0 /\ -__const_100^post16+__const_100^0 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post16 == 0 /\ -size7^post16+size7^0 == 0 /\ -ret_my_malloc10^post16+ret_my_malloc10^0 == 0), cost: 1 16: l12 -> l10 : __const_100^0'=__const_100^post17, __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, (tmp9^0-tmp9^post17 == 0 /\ size7^0-size7^post17 == 0 /\ tmp^0-tmp^post17 == 0 /\ tmp22^0-tmp22^post17 == 0 /\ -tmp13^post17+tmp13^0 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post17 == 0 /\ tmp___0^0-tmp___0^post17 == 0 /\ -size17^post17+size17^0 == 0 /\ -retval^post17+retval^0 == 0 /\ -size11^post17+size11^0 == 0 /\ tmp___1^0-tmp___1^post17 == 0 /\ __len21^0-__len21^post17 == 0 /\ -__const_100^post17+__const_100^0 == 0 /\ size15^0-size15^post17 == 0 /\ -ret_my_malloc10^post17+ret_my_malloc10^0 == 0), cost: 1 17: l12 -> l11 : __const_100^0'=__const_100^post18, __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, (-tmp22^post18+tmp22^0 == 0 /\ tmp___1^0-tmp___1^post18 == 0 /\ -tmp9^post18+tmp9^0 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post18 == 0 /\ tmp13^0-tmp13^post18 == 0 /\ -__len21^post18+__len21^0 == 0 /\ -size17^post18+size17^0 == 0 /\ -tmp___0^post18+tmp___0^0 == 0 /\ size11^0-size11^post18 == 0 /\ -retval^post18+retval^0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post18 == 0 /\ size7^0-size7^post18 == 0 /\ tmp^0-tmp^post18 == 0 /\ size15^0-size15^post18 == 0 /\ -__const_100^post18+__const_100^0 == 0), cost: 1 18: l13 -> l12 : __const_100^0'=__const_100^post19, __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, (size15^post19-__const_100^0 == 0 /\ -tmp___1^post19+tmp___1^0 == 0 /\ -tmp9^post19+tmp9^0 == 0 /\ -tmp13^post19+tmp13^0 == 0 /\ tmp^0-tmp^post19 == 0 /\ -__len21^post19+__len21^0 == 0 /\ -size11^post19+size11^0 == 0 /\ -retval^post19+retval^0 == 0 /\ tmp22^0-tmp22^post19 == 0 /\ size17^0-size17^post19 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post19 == 0 /\ -ret_my_malloc10^post19+ret_my_malloc10^0 == 0 /\ tmp___0^0-tmp___0^post19 == 0 /\ -__const_100^post19+__const_100^0 == 0 /\ -size7^post19+size7^0 == 0), cost: 1 19: l14 -> l15 : __const_100^0'=__const_100^post20, __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, (-size7^post20+size7^0 == 0 /\ retval^post20-ret_my_malloc14^0 == 0 /\ size15^0-size15^post20 == 0 /\ -tmp___1^post20+tmp___1^0 == 0 /\ -tmp9^post20+tmp9^0 == 0 /\ -__len21^post20+__len21^0 == 0 /\ -tmp13^post20+tmp13^0 == 0 /\ -__const_100^post20+__const_100^0 == 0 /\ size17^0-size17^post20 == 0 /\ tmp^0-tmp^post20 == 0 /\ tmp22^0-tmp22^post20 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post20 == 0 /\ -ret_my_malloc10^post20+ret_my_malloc10^0 == 0 /\ -size11^post20+size11^0 == 0 /\ tmp___0^0-tmp___0^post20 == 0), cost: 1 20: l15 -> l5 : __const_100^0'=__const_100^post21, __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 /\ -size17^post21+size17^0 == 0 /\ tmp^0-tmp^post21 == 0 /\ size7^0-size7^post21 == 0 /\ tmp9^0-tmp9^post21 == 0 /\ -tmp13^post21+tmp13^0 == 0 /\ tmp22^0-tmp22^post21 == 0 /\ -__const_100^post21+__const_100^0 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post21 == 0 /\ tmp___0^0-tmp___0^post21 == 0 /\ __len21^0-__len21^post21 == 0 /\ -retval^post21+retval^0 == 0 /\ size15^0-size15^post21 == 0 /\ 1-retval^0 <= 0 /\ -1+retval^0 <= 0 /\ -ret_my_malloc10^post21+ret_my_malloc10^0 == 0 /\ -size11^post21+size11^0 == 0), cost: 1 21: l15 -> l13 : __const_100^0'=__const_100^post22, __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, (-tmp___0^post22+tmp___0^0 == 0 /\ -tmp22^post22+tmp22^0 == 0 /\ tmp^0-tmp^post22 == 0 /\ -__const_100^post22+__const_100^0 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post22 == 0 /\ tmp13^0-tmp13^post22 == 0 /\ tmp___1^0-tmp___1^post22 == 0 /\ -tmp9^post22+tmp9^0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post22 == 0 /\ -size17^post22+size17^0 == 0 /\ size11^0-size11^post22 == 0 /\ -retval^post22+retval^0 == 0 /\ -__len21^post22+__len21^0 == 0 /\ size7^0-size7^post22 == 0 /\ 2-retval^0 <= 0 /\ size15^0-size15^post22 == 0), cost: 1 22: l15 -> l13 : __const_100^0'=__const_100^post23, __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___1^post23+tmp___1^0 == 0 /\ -tmp13^post23+tmp13^0 == 0 /\ -ret_my_malloc10^post23+ret_my_malloc10^0 == 0 /\ -tmp9^post23+tmp9^0 == 0 /\ -__const_100^post23+__const_100^0 == 0 /\ size15^0-size15^post23 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post23 == 0 /\ -size11^post23+size11^0 == 0 /\ -retval^post23+retval^0 == 0 /\ size17^0-size17^post23 == 0 /\ tmp^0-tmp^post23 == 0 /\ tmp22^0-tmp22^post23 == 0 /\ retval^0 <= 0 /\ __len21^0-__len21^post23 == 0 /\ tmp___0^0-tmp___0^post23 == 0 /\ -size7^post23+size7^0 == 0), cost: 1 23: l16 -> l14 : __const_100^0'=__const_100^post24, __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, (-retval^post24+retval^0 == 0 /\ -size7^post24+size7^0 == 0 /\ size15^0-size15^post24 == 0 /\ -tmp___1^post24+tmp___1^0 == 0 /\ -ret_my_malloc10^post24+ret_my_malloc10^0 == 0 /\ -tmp13^post24+tmp13^0 == 0 /\ ret_my_malloc14^post24 == 0 /\ __len21^0-__len21^post24 == 0 /\ -__const_100^post24+__const_100^0 == 0 /\ -tmp9^post24+tmp9^0 == 0 /\ size17^0-size17^post24 == 0 /\ tmp^0-tmp^post24 == 0 /\ tmp22^0-tmp22^post24 == 0 /\ tmp___0^0-tmp___0^post24 == 0 /\ -size11^post24+size11^0 == 0), cost: 1 24: l16 -> l14 : __const_100^0'=__const_100^post25, __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, (-size17^post25+size17^0 == 0 /\ tmp9^0-tmp9^post25 == 0 /\ tmp^0-tmp^post25 == 0 /\ size7^0-size7^post25 == 0 /\ tmp___1^0-tmp___1^post25 == 0 /\ -tmp13^post25+tmp13^0 == 0 /\ -__const_100^post25+__const_100^0 == 0 /\ tmp22^0-tmp22^post25 == 0 /\ -ret_my_malloc10^post25+ret_my_malloc10^0 == 0 /\ tmp___0^0-tmp___0^post25 == 0 /\ __len21^0-__len21^post25 == 0 /\ size11^0-size11^post25 == 0 /\ size15^0-size15^post25 == 0 /\ -1+ret_my_malloc14^post25 == 0 /\ -retval^post25+retval^0 == 0), cost: 1 25: l17 -> l9 : __const_100^0'=__const_100^post26, __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, (-size17^post26+size17^0 == 0 /\ -tmp___0^post26+tmp___0^0 == 0 /\ -ret_my_malloc14^post26+ret_my_malloc14^0 == 0 /\ size7^0-size7^post26 == 0 /\ tmp^0-tmp^post26 == 0 /\ -tmp9^post26+tmp9^0 == 0 /\ tmp___1^0-tmp___1^post26 == 0 /\ -__const_100^post26+__const_100^0 == 0 /\ tmp13^0-tmp13^post26 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post26 == 0 /\ -__len21^post26+__len21^0 == 0 /\ size15^0-size15^post26 == 0 /\ 2-retval^0 <= 0 /\ -tmp22^post26+tmp22^0 == 0 /\ -retval^post26+retval^0 == 0 /\ size11^0-size11^post26 == 0), cost: 1 26: l17 -> l9 : __const_100^0'=__const_100^post27, __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, (-tmp___1^post27+tmp___1^0 == 0 /\ -size7^post27+size7^0 == 0 /\ -size11^post27+size11^0 == 0 /\ size15^0-size15^post27 == 0 /\ -tmp9^post27+tmp9^0 == 0 /\ -tmp13^post27+tmp13^0 == 0 /\ -__const_100^post27+__const_100^0 == 0 /\ -ret_my_malloc10^post27+ret_my_malloc10^0 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post27 == 0 /\ tmp^0-tmp^post27 == 0 /\ tmp22^0-tmp22^post27 == 0 /\ retval^0 <= 0 /\ __len21^0-__len21^post27 == 0 /\ size17^0-size17^post27 == 0 /\ retval^0-retval^post27 == 0 /\ tmp___0^0-tmp___0^post27 == 0), cost: 1 27: l17 -> l16 : __const_100^0'=__const_100^post28, __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 /\ size7^0-size7^post28 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post28 == 0 /\ -retval^post28+retval^0 == 0 /\ -tmp___1^post28+tmp___1^0 == 0 /\ -__const_100^post28+__const_100^0 == 0 /\ size11^post28-__const_100^0 == 0 /\ __len21^0-__len21^post28 == 0 /\ -tmp9^post28+tmp9^0 == 0 /\ -ret_my_malloc10^post28+ret_my_malloc10^0 == 0 /\ 1-retval^0 <= 0 /\ -1+retval^0 <= 0 /\ tmp^0-tmp^post28 == 0 /\ size15^0-size15^post28 == 0 /\ tmp22^0-tmp22^post28 == 0 /\ tmp___0^0-tmp___0^post28 == 0 /\ -size17^post28+size17^0 == 0), cost: 1 29: l18 -> l0 : __const_100^0'=__const_100^post30, __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 /\ tmp^0-tmp^post30 == 0 /\ tmp13^0-tmp13^post30 == 0 /\ -tmp___0^post30+tmp___0^0 == 0 /\ tmp___1^0-tmp___1^post30 == 0 /\ -tmp22^post30+tmp22^0 == 0 /\ -ret_my_malloc14^post30+ret_my_malloc14^0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post30 == 0 /\ -size17^post30+size17^0 == 0 /\ -__const_100^post30+__const_100^0 == 0 /\ -__len21^post30+__len21^0 == 0 /\ size15^0-size15^post30 == 0 /\ -retval^post30+retval^0 == 0 /\ size7^post30-__const_100^0 == 0 /\ size11^0-size11^post30 == 0), cost: 1 30: l19 -> l18 : __const_100^0'=__const_100^post31, __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, (-size11^post31+size11^0 == 0 /\ tmp22^0-tmp22^post31 == 0 /\ size15^0-size15^post31 == 0 /\ -tmp___1^post31+tmp___1^0 == 0 /\ -__const_100^post31+__const_100^0 == 0 /\ -ret_my_malloc10^post31+ret_my_malloc10^0 == 0 /\ -size7^post31+size7^0 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post31 == 0 /\ tmp^0-tmp^post31 == 0 /\ size17^0-size17^post31 == 0 /\ -tmp9^post31+tmp9^0 == 0 /\ -tmp13^post31+tmp13^0 == 0 /\ tmp___0^0-tmp___0^post31 == 0 /\ __len21^0-__len21^post31 == 0 /\ retval^0-retval^post31 == 0), cost: 1 Chained Linear Paths Start location: l19 Program variables: __const_100^0 __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 : __const_100^0'=__const_100^post1, __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, (-size17^post1+size17^0 == 0 /\ size15^0-size15^post1 == 0 /\ -__len21^post1+__len21^0 == 0 /\ -tmp___0^post1+tmp___0^0 == 0 /\ size11^0-size11^post1 == 0 /\ -tmp13^post1+tmp13^0 == 0 /\ -tmp9^post1+tmp9^0 == 0 /\ -retval^post1+retval^0 == 0 /\ tmp___1^0-tmp___1^post1 == 0 /\ tmp^0-tmp^post1 == 0 /\ size7^0-size7^post1 == 0 /\ -__const_100^post1+__const_100^0 == 0 /\ tmp22^0-tmp22^post1 == 0 /\ ret_my_malloc10^post1 == 0 /\ -ret_my_malloc14^post1+ret_my_malloc14^0 == 0), cost: 1 1: l0 -> l1 : __const_100^0'=__const_100^post2, __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, (-size17^post2+size17^0 == 0 /\ tmp^0-tmp^post2 == 0 /\ -tmp___0^post2+tmp___0^0 == 0 /\ -__len21^post2+__len21^0 == 0 /\ -1+ret_my_malloc10^post2 == 0 /\ size7^0-size7^post2 == 0 /\ tmp___1^0-tmp___1^post2 == 0 /\ -retval^post2+retval^0 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post2 == 0 /\ __const_100^0-__const_100^post2 == 0 /\ tmp13^0-tmp13^post2 == 0 /\ -tmp9^post2+tmp9^0 == 0 /\ size15^0-size15^post2 == 0 /\ size11^0-size11^post2 == 0 /\ -tmp22^post2+tmp22^0 == 0), cost: 1 28: l1 -> l17 : __const_100^0'=__const_100^post29, __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_malloc10^0-ret_my_malloc10^post29 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post29 == 0 /\ -tmp___0^post29+tmp___0^0 == 0 /\ tmp___1^0-tmp___1^post29 == 0 /\ -__const_100^post29+__const_100^0 == 0 /\ tmp22^0-tmp22^post29 == 0 /\ size15^0-size15^post29 == 0 /\ __len21^0-__len21^post29 == 0 /\ -tmp9^post29+tmp9^0 == 0 /\ size7^0-size7^post29 == 0 /\ size11^0-size11^post29 == 0 /\ -size17^post29+size17^0 == 0 /\ -tmp13^post29+tmp13^0 == 0 /\ -tmp^post29+retval^post29 == 0 /\ tmp^post29-ret_my_malloc10^0 == 0), cost: 1 2: l2 -> l3 : __const_100^0'=__const_100^post3, __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, (-__const_100^post3+__const_100^0 == 0 /\ -__len21^post3+__len21^0 == 0 /\ tmp^0-tmp^post3 == 0 /\ size7^0-size7^post3 == 0 /\ -ret_my_malloc10^post3+ret_my_malloc10^0 == 0 /\ -size17^post3+size17^0 == 0 /\ -retval^post3+retval^0 == 0 /\ tmp___1^0-tmp___1^post3 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post3 == 0 /\ tmp13^0-tmp13^post3 == 0 /\ size15^0-size15^post3 == 0 /\ -tmp9^post3+tmp9^0 == 0 /\ tmp___0^0-tmp___0^post3 == 0 /\ -tmp22^post3+tmp22^0 == 0 /\ size11^0-size11^post3 == 0), cost: 1 3: l4 -> l2 : __const_100^0'=__const_100^post4, __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 /\ -__len21^post4+__len21^0 == 0 /\ size15^0-size15^post4 == 0 /\ -ret_my_malloc10^post4+ret_my_malloc10^0 == 0 /\ -size7^post4+size7^0 == 0 /\ -tmp___1^post4+tmp___1^0 == 0 /\ -tmp9^post4+tmp9^0 == 0 /\ -tmp13^post4+tmp13^0 == 0 /\ size17^0-size17^post4 == 0 /\ tmp^0-tmp^post4 == 0 /\ -__const_100^post4+__const_100^0 == 0 /\ -size11^post4+size11^0 == 0 /\ retval^0-retval^post4 == 0 /\ tmp22^0-tmp22^post4 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post4 == 0), cost: 1 4: l5 -> l2 : __const_100^0'=__const_100^post5, __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 /\ size15^0-size15^post5 == 0 /\ -size17^post5+size17^0 == 0 /\ -tmp___0^post5+tmp___0^0 == 0 /\ __len21^post5-__const_100^0 == 0 /\ size11^0-size11^post5 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post5 == 0 /\ -retval^post5+retval^0 == 0 /\ -tmp9^post5+tmp9^0 == 0 /\ -tmp13^post5+tmp13^0 == 0 /\ 1+tmp___1^0 <= 0 /\ -1-tmp___1^0 <= 0 /\ size7^0-size7^post5 == 0 /\ tmp^0-tmp^post5 == 0 /\ -__const_100^post5+__const_100^0 == 0 /\ tmp___1^0-tmp___1^post5 == 0 /\ -ret_my_malloc14^post5+ret_my_malloc14^0 == 0), cost: 1 5: l5 -> l4 : __const_100^0'=__const_100^post6, __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, (tmp^0-tmp^post6 == 0 /\ -tmp___0^post6+tmp___0^0 == 0 /\ size7^0-size7^post6 == 0 /\ -size17^post6+size17^0 == 0 /\ -tmp___1^0 <= 0 /\ ret_my_malloc14^0-ret_my_malloc14^post6 == 0 /\ -tmp9^post6+tmp9^0 == 0 /\ -retval^post6+retval^0 == 0 /\ tmp13^0-tmp13^post6 == 0 /\ tmp___1^0-tmp___1^post6 == 0 /\ size15^0-size15^post6 == 0 /\ -ret_my_malloc10^post6+ret_my_malloc10^0 == 0 /\ size11^0-size11^post6 == 0 /\ -__const_100^post6+__const_100^0 == 0 /\ -__len21^post6+__len21^0 == 0 /\ -tmp22^post6+tmp22^0 == 0), cost: 1 6: l5 -> l4 : __const_100^0'=__const_100^post7, __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, (tmp^0-tmp^post7 == 0 /\ size7^0-size7^post7 == 0 /\ -retval^post7+retval^0 == 0 /\ size11^0-size11^post7 == 0 /\ tmp___1^0-tmp___1^post7 == 0 /\ -tmp22^post7+tmp22^0 == 0 /\ tmp13^0-tmp13^post7 == 0 /\ -tmp9^post7+tmp9^0 == 0 /\ -ret_my_malloc10^post7+ret_my_malloc10^0 == 0 /\ tmp___0^0-tmp___0^post7 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post7 == 0 /\ -__const_100^post7+__const_100^0 == 0 /\ size15^0-size15^post7 == 0 /\ -size17^post7+size17^0 == 0 /\ __len21^0-__len21^post7 == 0 /\ 2+tmp___1^0 <= 0), cost: 1 7: l6 -> l3 : __const_100^0'=__const_100^post8, __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, (tmp___0^0-tmp___0^post8 == 0 /\ size15^0-size15^post8 == 0 /\ -size11^post8+size11^0 == 0 /\ -size7^post8+size7^0 == 0 /\ -tmp___1^post8+tmp___1^0 == 0 /\ -tmp13^post8+tmp13^0 == 0 /\ -tmp9^post8+tmp9^0 == 0 /\ -__const_100^post8+__const_100^0 == 0 /\ tmp^0-tmp^post8 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post8 == 0 /\ -ret_my_malloc10^post8+ret_my_malloc10^0 == 0 /\ -retval^post8+retval^0 == 0 /\ __len21^0-__len21^post8 == 0 /\ tmp22^0-tmp22^post8 == 0 /\ size17^0-size17^post8 == 0), cost: 1 8: l7 -> l6 : __const_100^0'=__const_100^post9, __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, (size15^0-size15^post9 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post9 == 0 /\ -size17^post9+size17^0 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post9 == 0 /\ __len21^0-__len21^post9 == 0 /\ size11^0-size11^post9 == 0 /\ -tmp13^post9+tmp13^0 == 0 /\ -__const_100^post9+__const_100^0 == 0 /\ tmp^0-tmp^post9 == 0 /\ -tmp9^post9+tmp9^0 == 0 /\ size7^0-size7^post9 == 0 /\ -retval^post9+retval^0 == 0 /\ tmp22^0-tmp22^post9 == 0 /\ -tmp___0^post9+tmp___0^0 == 0 /\ tmp___1^0-tmp___1^post9 == 0), cost: 1 9: l8 -> l7 : __const_100^0'=__const_100^post10, __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, (tmp^0-tmp^post10 == 0 /\ size7^0-size7^post10 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post10 == 0 /\ -size17^post10+size17^0 == 0 /\ size15^0-size15^post10 == 0 /\ -size11^post10+size11^0 == 0 /\ tmp13^0-tmp13^post10 == 0 /\ tmp___1^0-tmp___1^post10 == 0 /\ -ret_my_malloc10^post10+ret_my_malloc10^0 == 0 /\ -tmp22^post10+tmp22^0 == 0 /\ tmp___0^0-tmp___0^post10 == 0 /\ -tmp9^post10+tmp9^0 == 0 /\ -__const_100^post10+__const_100^0 == 0 /\ -__len21^post10+__len21^0 == 0 /\ -retval^post10+retval^0 == 0), cost: 1 10: l8 -> l6 : __const_100^0'=__const_100^post11, __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, (tmp^0-tmp^post11 == 0 /\ -size7^post11+size7^0 == 0 /\ -size11^post11+size11^0 == 0 /\ tmp___1^0-tmp___1^post11 == 0 /\ -ret_my_malloc10^post11+ret_my_malloc10^0 == 0 /\ tmp___0^0-tmp___0^post11 == 0 /\ tmp13^0-tmp13^post11 == 0 /\ retval^0-retval^post11 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post11 == 0 /\ -size17^post11+size17^0 == 0 /\ -tmp22^post11+tmp22^0 == 0 /\ -__const_100^post11+__const_100^0 == 0 /\ -tmp9^post11+tmp9^0 == 0 /\ size15^0-size15^post11 == 0 /\ __len21^0-__len21^post11 == 0), cost: 1 11: l8 -> l7 : __const_100^0'=__const_100^post12, __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^0-tmp___0^post12 == 0 /\ -size17^post12+size17^0 == 0 /\ -tmp___1^post12+tmp___1^0 == 0 /\ -tmp13^post12+tmp13^0 == 0 /\ tmp^0-tmp^post12 == 0 /\ -__const_100^post12+__const_100^0 == 0 /\ -ret_my_malloc10^post12+ret_my_malloc10^0 == 0 /\ -retval^post12+retval^0 == 0 /\ -tmp9^post12+tmp9^0 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post12 == 0 /\ -size11^post12+size11^0 == 0 /\ -size7^post12+size7^0 == 0 /\ __len21^0-__len21^post12 == 0 /\ size15^0-size15^post12 == 0 /\ tmp22^0-tmp22^post12 == 0), cost: 1 12: l9 -> l8 : __const_100^0'=__const_100^post13, __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, (-tmp13^post13+tmp13^0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post13 == 0 /\ size11^0-size11^post13 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post13 == 0 /\ __len21^0-__len21^post13 == 0 /\ size7^0-size7^post13 == 0 /\ size17^post13-__const_100^0 == 0 /\ size15^0-size15^post13 == 0 /\ -tmp9^post13+tmp9^0 == 0 /\ tmp^0-tmp^post13 == 0 /\ -__const_100^post13+__const_100^0 == 0 /\ -retval^post13+retval^0 == 0 /\ -tmp___0^post13+tmp___0^0 == 0 /\ tmp22^0-tmp22^post13 == 0 /\ tmp___1^0-tmp___1^post13 == 0), cost: 1 13: l10 -> l3 : __const_100^0'=__const_100^post14, __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, (tmp^0-tmp^post14 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post14 == 0 /\ size15^0-size15^post14 == 0 /\ -size11^post14+size11^0 == 0 /\ tmp___1^0-tmp___1^post14 == 0 /\ -__len21^post14+__len21^0 == 0 /\ -tmp9^post14+tmp9^0 == 0 /\ tmp___0^0-tmp___0^post14 == 0 /\ tmp22^0-tmp22^post14 == 0 /\ -__const_100^post14+__const_100^0 == 0 /\ -size17^post14+size17^0 == 0 /\ -size7^post14+size7^0 == 0 /\ -ret_my_malloc10^post14+ret_my_malloc10^0 == 0 /\ -retval^post14+retval^0 == 0 /\ -tmp13^post14+tmp13^0 == 0), cost: 1 14: l11 -> l10 : __const_100^0'=__const_100^post15, __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, (tmp9^0-tmp9^post15 == 0 /\ tmp___1^0-tmp___1^post15 == 0 /\ -tmp13^post15+tmp13^0 == 0 /\ tmp22^0-tmp22^post15 == 0 /\ -size11^post15+size11^0 == 0 /\ -tmp___0^post15+tmp___0^0 == 0 /\ -__const_100^post15+__const_100^0 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post15 == 0 /\ -size7^post15+size7^0 == 0 /\ -size17^post15+size17^0 == 0 /\ -ret_my_malloc10^post15+ret_my_malloc10^0 == 0 /\ size15^0-size15^post15 == 0 /\ __len21^0-__len21^post15 == 0 /\ -retval^post15+retval^0 == 0 /\ tmp^0-tmp^post15 == 0), cost: 1 15: l12 -> l11 : __const_100^0'=__const_100^post16, __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, (-__len21^post16+__len21^0 == 0 /\ -tmp13^post16+tmp13^0 == 0 /\ -tmp9^post16+tmp9^0 == 0 /\ size15^0-size15^post16 == 0 /\ tmp___1^0-tmp___1^post16 == 0 /\ -size11^post16+size11^0 == 0 /\ -retval^post16+retval^0 == 0 /\ size17^0-size17^post16 == 0 /\ tmp^0-tmp^post16 == 0 /\ tmp___0^0-tmp___0^post16 == 0 /\ tmp22^0-tmp22^post16 == 0 /\ -__const_100^post16+__const_100^0 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post16 == 0 /\ -size7^post16+size7^0 == 0 /\ -ret_my_malloc10^post16+ret_my_malloc10^0 == 0), cost: 1 16: l12 -> l10 : __const_100^0'=__const_100^post17, __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, (tmp9^0-tmp9^post17 == 0 /\ size7^0-size7^post17 == 0 /\ tmp^0-tmp^post17 == 0 /\ tmp22^0-tmp22^post17 == 0 /\ -tmp13^post17+tmp13^0 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post17 == 0 /\ tmp___0^0-tmp___0^post17 == 0 /\ -size17^post17+size17^0 == 0 /\ -retval^post17+retval^0 == 0 /\ -size11^post17+size11^0 == 0 /\ tmp___1^0-tmp___1^post17 == 0 /\ __len21^0-__len21^post17 == 0 /\ -__const_100^post17+__const_100^0 == 0 /\ size15^0-size15^post17 == 0 /\ -ret_my_malloc10^post17+ret_my_malloc10^0 == 0), cost: 1 17: l12 -> l11 : __const_100^0'=__const_100^post18, __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, (-tmp22^post18+tmp22^0 == 0 /\ tmp___1^0-tmp___1^post18 == 0 /\ -tmp9^post18+tmp9^0 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post18 == 0 /\ tmp13^0-tmp13^post18 == 0 /\ -__len21^post18+__len21^0 == 0 /\ -size17^post18+size17^0 == 0 /\ -tmp___0^post18+tmp___0^0 == 0 /\ size11^0-size11^post18 == 0 /\ -retval^post18+retval^0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post18 == 0 /\ size7^0-size7^post18 == 0 /\ tmp^0-tmp^post18 == 0 /\ size15^0-size15^post18 == 0 /\ -__const_100^post18+__const_100^0 == 0), cost: 1 18: l13 -> l12 : __const_100^0'=__const_100^post19, __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, (size15^post19-__const_100^0 == 0 /\ -tmp___1^post19+tmp___1^0 == 0 /\ -tmp9^post19+tmp9^0 == 0 /\ -tmp13^post19+tmp13^0 == 0 /\ tmp^0-tmp^post19 == 0 /\ -__len21^post19+__len21^0 == 0 /\ -size11^post19+size11^0 == 0 /\ -retval^post19+retval^0 == 0 /\ tmp22^0-tmp22^post19 == 0 /\ size17^0-size17^post19 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post19 == 0 /\ -ret_my_malloc10^post19+ret_my_malloc10^0 == 0 /\ tmp___0^0-tmp___0^post19 == 0 /\ -__const_100^post19+__const_100^0 == 0 /\ -size7^post19+size7^0 == 0), cost: 1 19: l14 -> l15 : __const_100^0'=__const_100^post20, __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, (-size7^post20+size7^0 == 0 /\ retval^post20-ret_my_malloc14^0 == 0 /\ size15^0-size15^post20 == 0 /\ -tmp___1^post20+tmp___1^0 == 0 /\ -tmp9^post20+tmp9^0 == 0 /\ -__len21^post20+__len21^0 == 0 /\ -tmp13^post20+tmp13^0 == 0 /\ -__const_100^post20+__const_100^0 == 0 /\ size17^0-size17^post20 == 0 /\ tmp^0-tmp^post20 == 0 /\ tmp22^0-tmp22^post20 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post20 == 0 /\ -ret_my_malloc10^post20+ret_my_malloc10^0 == 0 /\ -size11^post20+size11^0 == 0 /\ tmp___0^0-tmp___0^post20 == 0), cost: 1 20: l15 -> l5 : __const_100^0'=__const_100^post21, __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 /\ -size17^post21+size17^0 == 0 /\ tmp^0-tmp^post21 == 0 /\ size7^0-size7^post21 == 0 /\ tmp9^0-tmp9^post21 == 0 /\ -tmp13^post21+tmp13^0 == 0 /\ tmp22^0-tmp22^post21 == 0 /\ -__const_100^post21+__const_100^0 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post21 == 0 /\ tmp___0^0-tmp___0^post21 == 0 /\ __len21^0-__len21^post21 == 0 /\ -retval^post21+retval^0 == 0 /\ size15^0-size15^post21 == 0 /\ 1-retval^0 <= 0 /\ -1+retval^0 <= 0 /\ -ret_my_malloc10^post21+ret_my_malloc10^0 == 0 /\ -size11^post21+size11^0 == 0), cost: 1 21: l15 -> l13 : __const_100^0'=__const_100^post22, __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, (-tmp___0^post22+tmp___0^0 == 0 /\ -tmp22^post22+tmp22^0 == 0 /\ tmp^0-tmp^post22 == 0 /\ -__const_100^post22+__const_100^0 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post22 == 0 /\ tmp13^0-tmp13^post22 == 0 /\ tmp___1^0-tmp___1^post22 == 0 /\ -tmp9^post22+tmp9^0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post22 == 0 /\ -size17^post22+size17^0 == 0 /\ size11^0-size11^post22 == 0 /\ -retval^post22+retval^0 == 0 /\ -__len21^post22+__len21^0 == 0 /\ size7^0-size7^post22 == 0 /\ 2-retval^0 <= 0 /\ size15^0-size15^post22 == 0), cost: 1 22: l15 -> l13 : __const_100^0'=__const_100^post23, __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___1^post23+tmp___1^0 == 0 /\ -tmp13^post23+tmp13^0 == 0 /\ -ret_my_malloc10^post23+ret_my_malloc10^0 == 0 /\ -tmp9^post23+tmp9^0 == 0 /\ -__const_100^post23+__const_100^0 == 0 /\ size15^0-size15^post23 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post23 == 0 /\ -size11^post23+size11^0 == 0 /\ -retval^post23+retval^0 == 0 /\ size17^0-size17^post23 == 0 /\ tmp^0-tmp^post23 == 0 /\ tmp22^0-tmp22^post23 == 0 /\ retval^0 <= 0 /\ __len21^0-__len21^post23 == 0 /\ tmp___0^0-tmp___0^post23 == 0 /\ -size7^post23+size7^0 == 0), cost: 1 23: l16 -> l14 : __const_100^0'=__const_100^post24, __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, (-retval^post24+retval^0 == 0 /\ -size7^post24+size7^0 == 0 /\ size15^0-size15^post24 == 0 /\ -tmp___1^post24+tmp___1^0 == 0 /\ -ret_my_malloc10^post24+ret_my_malloc10^0 == 0 /\ -tmp13^post24+tmp13^0 == 0 /\ ret_my_malloc14^post24 == 0 /\ __len21^0-__len21^post24 == 0 /\ -__const_100^post24+__const_100^0 == 0 /\ -tmp9^post24+tmp9^0 == 0 /\ size17^0-size17^post24 == 0 /\ tmp^0-tmp^post24 == 0 /\ tmp22^0-tmp22^post24 == 0 /\ tmp___0^0-tmp___0^post24 == 0 /\ -size11^post24+size11^0 == 0), cost: 1 24: l16 -> l14 : __const_100^0'=__const_100^post25, __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, (-size17^post25+size17^0 == 0 /\ tmp9^0-tmp9^post25 == 0 /\ tmp^0-tmp^post25 == 0 /\ size7^0-size7^post25 == 0 /\ tmp___1^0-tmp___1^post25 == 0 /\ -tmp13^post25+tmp13^0 == 0 /\ -__const_100^post25+__const_100^0 == 0 /\ tmp22^0-tmp22^post25 == 0 /\ -ret_my_malloc10^post25+ret_my_malloc10^0 == 0 /\ tmp___0^0-tmp___0^post25 == 0 /\ __len21^0-__len21^post25 == 0 /\ size11^0-size11^post25 == 0 /\ size15^0-size15^post25 == 0 /\ -1+ret_my_malloc14^post25 == 0 /\ -retval^post25+retval^0 == 0), cost: 1 25: l17 -> l9 : __const_100^0'=__const_100^post26, __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, (-size17^post26+size17^0 == 0 /\ -tmp___0^post26+tmp___0^0 == 0 /\ -ret_my_malloc14^post26+ret_my_malloc14^0 == 0 /\ size7^0-size7^post26 == 0 /\ tmp^0-tmp^post26 == 0 /\ -tmp9^post26+tmp9^0 == 0 /\ tmp___1^0-tmp___1^post26 == 0 /\ -__const_100^post26+__const_100^0 == 0 /\ tmp13^0-tmp13^post26 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post26 == 0 /\ -__len21^post26+__len21^0 == 0 /\ size15^0-size15^post26 == 0 /\ 2-retval^0 <= 0 /\ -tmp22^post26+tmp22^0 == 0 /\ -retval^post26+retval^0 == 0 /\ size11^0-size11^post26 == 0), cost: 1 26: l17 -> l9 : __const_100^0'=__const_100^post27, __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, (-tmp___1^post27+tmp___1^0 == 0 /\ -size7^post27+size7^0 == 0 /\ -size11^post27+size11^0 == 0 /\ size15^0-size15^post27 == 0 /\ -tmp9^post27+tmp9^0 == 0 /\ -tmp13^post27+tmp13^0 == 0 /\ -__const_100^post27+__const_100^0 == 0 /\ -ret_my_malloc10^post27+ret_my_malloc10^0 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post27 == 0 /\ tmp^0-tmp^post27 == 0 /\ tmp22^0-tmp22^post27 == 0 /\ retval^0 <= 0 /\ __len21^0-__len21^post27 == 0 /\ size17^0-size17^post27 == 0 /\ retval^0-retval^post27 == 0 /\ tmp___0^0-tmp___0^post27 == 0), cost: 1 27: l17 -> l16 : __const_100^0'=__const_100^post28, __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 /\ size7^0-size7^post28 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post28 == 0 /\ -retval^post28+retval^0 == 0 /\ -tmp___1^post28+tmp___1^0 == 0 /\ -__const_100^post28+__const_100^0 == 0 /\ size11^post28-__const_100^0 == 0 /\ __len21^0-__len21^post28 == 0 /\ -tmp9^post28+tmp9^0 == 0 /\ -ret_my_malloc10^post28+ret_my_malloc10^0 == 0 /\ 1-retval^0 <= 0 /\ -1+retval^0 <= 0 /\ tmp^0-tmp^post28 == 0 /\ size15^0-size15^post28 == 0 /\ tmp22^0-tmp22^post28 == 0 /\ tmp___0^0-tmp___0^post28 == 0 /\ -size17^post28+size17^0 == 0), cost: 1 31: l19 -> l0 : __const_100^0'=__const_100^post30, __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 /\ -size11^post31+size11^0 == 0 /\ tmp22^0-tmp22^post31 == 0 /\ -__const_100^post30+__const_100^post31 == 0 /\ ret_my_malloc10^post31-ret_my_malloc10^post30 == 0 /\ tmp13^post31-tmp13^post30 == 0 /\ size15^0-size15^post31 == 0 /\ -ret_my_malloc14^post30+ret_my_malloc14^post31 == 0 /\ -tmp___1^post31+tmp___1^0 == 0 /\ -__const_100^post31+__const_100^0 == 0 /\ size7^post30-__const_100^post31 == 0 /\ -ret_my_malloc10^post31+ret_my_malloc10^0 == 0 /\ -__len21^post30+__len21^post31 == 0 /\ -tmp22^post30+tmp22^post31 == 0 /\ -size7^post31+size7^0 == 0 /\ -retval^post30+retval^post31 == 0 /\ size15^post31-size15^post30 == 0 /\ -size17^post30+size17^post31 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post31 == 0 /\ tmp___1^post31-tmp___1^post30 == 0 /\ tmp^0-tmp^post31 == 0 /\ -tmp___0^post30+tmp___0^post31 == 0 /\ tmp^post31-tmp^post30 == 0 /\ size17^0-size17^post31 == 0 /\ -tmp9^post31+tmp9^0 == 0 /\ -tmp13^post31+tmp13^0 == 0 /\ tmp___0^0-tmp___0^post31 == 0 /\ __len21^0-__len21^post31 == 0 /\ size11^post31-size11^post30 == 0 /\ retval^0-retval^post31 == 0), cost: 1 Eliminating location l18 by chaining: Applied chaining First rule: l19 -> l18 : __const_100^0'=__const_100^post31, __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, (-size11^post31+size11^0 == 0 /\ tmp22^0-tmp22^post31 == 0 /\ size15^0-size15^post31 == 0 /\ -tmp___1^post31+tmp___1^0 == 0 /\ -__const_100^post31+__const_100^0 == 0 /\ -ret_my_malloc10^post31+ret_my_malloc10^0 == 0 /\ -size7^post31+size7^0 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post31 == 0 /\ tmp^0-tmp^post31 == 0 /\ size17^0-size17^post31 == 0 /\ -tmp9^post31+tmp9^0 == 0 /\ -tmp13^post31+tmp13^0 == 0 /\ tmp___0^0-tmp___0^post31 == 0 /\ __len21^0-__len21^post31 == 0 /\ retval^0-retval^post31 == 0), cost: 1 Second rule: l18 -> l0 : __const_100^0'=__const_100^post30, __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 /\ tmp^0-tmp^post30 == 0 /\ tmp13^0-tmp13^post30 == 0 /\ -tmp___0^post30+tmp___0^0 == 0 /\ tmp___1^0-tmp___1^post30 == 0 /\ -tmp22^post30+tmp22^0 == 0 /\ -ret_my_malloc14^post30+ret_my_malloc14^0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post30 == 0 /\ -size17^post30+size17^0 == 0 /\ -__const_100^post30+__const_100^0 == 0 /\ -__len21^post30+__len21^0 == 0 /\ size15^0-size15^post30 == 0 /\ -retval^post30+retval^0 == 0 /\ size7^post30-__const_100^0 == 0 /\ size11^0-size11^post30 == 0), cost: 1 New rule: l19 -> l0 : __const_100^0'=__const_100^post30, __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 /\ -size11^post31+size11^0 == 0 /\ tmp22^0-tmp22^post31 == 0 /\ -__const_100^post30+__const_100^post31 == 0 /\ ret_my_malloc10^post31-ret_my_malloc10^post30 == 0 /\ tmp13^post31-tmp13^post30 == 0 /\ size15^0-size15^post31 == 0 /\ -ret_my_malloc14^post30+ret_my_malloc14^post31 == 0 /\ -tmp___1^post31+tmp___1^0 == 0 /\ -__const_100^post31+__const_100^0 == 0 /\ size7^post30-__const_100^post31 == 0 /\ -ret_my_malloc10^post31+ret_my_malloc10^0 == 0 /\ -__len21^post30+__len21^post31 == 0 /\ -tmp22^post30+tmp22^post31 == 0 /\ -size7^post31+size7^0 == 0 /\ -retval^post30+retval^post31 == 0 /\ size15^post31-size15^post30 == 0 /\ -size17^post30+size17^post31 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post31 == 0 /\ tmp___1^post31-tmp___1^post30 == 0 /\ tmp^0-tmp^post31 == 0 /\ -tmp___0^post30+tmp___0^post31 == 0 /\ tmp^post31-tmp^post30 == 0 /\ size17^0-size17^post31 == 0 /\ -tmp9^post31+tmp9^0 == 0 /\ -tmp13^post31+tmp13^0 == 0 /\ tmp___0^0-tmp___0^post31 == 0 /\ __len21^0-__len21^post31 == 0 /\ size11^post31-size11^post30 == 0 /\ retval^0-retval^post31 == 0), cost: 1 Applied deletion Removed the following rules: 29 30 Simplified Transitions Start location: l19 Program variables: __const_100^0 __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'=__const_100^0, 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'=__const_100^0, 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'=__const_100^0, 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'=__const_100^0, tmp13^0'=tmp13^post28, (1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0), cost: 1 61: l19 -> l0 : size7^0'=__const_100^0, tmp9^0'=tmp9^post30, T, cost: 1 Propagated Equalities Original rule: l0 -> l1 : __const_100^0'=__const_100^post1, __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, (-size17^post1+size17^0 == 0 /\ size15^0-size15^post1 == 0 /\ -__len21^post1+__len21^0 == 0 /\ -tmp___0^post1+tmp___0^0 == 0 /\ size11^0-size11^post1 == 0 /\ -tmp13^post1+tmp13^0 == 0 /\ -tmp9^post1+tmp9^0 == 0 /\ -retval^post1+retval^0 == 0 /\ tmp___1^0-tmp___1^post1 == 0 /\ tmp^0-tmp^post1 == 0 /\ size7^0-size7^post1 == 0 /\ -__const_100^post1+__const_100^0 == 0 /\ tmp22^0-tmp22^post1 == 0 /\ ret_my_malloc10^post1 == 0 /\ -ret_my_malloc14^post1+ret_my_malloc14^0 == 0), cost: 1 New rule: l0 -> l1 : __const_100^0'=__const_100^0, __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 size17^post1 = size17^0 propagated equality size15^post1 = size15^0 propagated equality __len21^post1 = __len21^0 propagated equality tmp___0^post1 = tmp___0^0 propagated equality size11^post1 = size11^0 propagated equality tmp13^post1 = tmp13^0 propagated equality tmp9^post1 = tmp9^0 propagated equality retval^post1 = retval^0 propagated equality tmp___1^post1 = tmp___1^0 propagated equality tmp^post1 = tmp^0 propagated equality size7^post1 = size7^0 propagated equality __const_100^post1 = __const_100^0 propagated equality tmp22^post1 = tmp22^0 propagated equality ret_my_malloc10^post1 = 0 propagated equality ret_my_malloc14^post1 = ret_my_malloc14^0 Simplified Guard Original rule: l0 -> l1 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^post2, __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, (-size17^post2+size17^0 == 0 /\ tmp^0-tmp^post2 == 0 /\ -tmp___0^post2+tmp___0^0 == 0 /\ -__len21^post2+__len21^0 == 0 /\ -1+ret_my_malloc10^post2 == 0 /\ size7^0-size7^post2 == 0 /\ tmp___1^0-tmp___1^post2 == 0 /\ -retval^post2+retval^0 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post2 == 0 /\ __const_100^0-__const_100^post2 == 0 /\ tmp13^0-tmp13^post2 == 0 /\ -tmp9^post2+tmp9^0 == 0 /\ size15^0-size15^post2 == 0 /\ size11^0-size11^post2 == 0 /\ -tmp22^post2+tmp22^0 == 0), cost: 1 New rule: l0 -> l1 : __const_100^0'=__const_100^0, __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 size17^post2 = size17^0 propagated equality tmp^post2 = tmp^0 propagated equality tmp___0^post2 = tmp___0^0 propagated equality __len21^post2 = __len21^0 propagated equality ret_my_malloc10^post2 = 1 propagated equality size7^post2 = size7^0 propagated equality tmp___1^post2 = tmp___1^0 propagated equality retval^post2 = retval^0 propagated equality ret_my_malloc14^post2 = ret_my_malloc14^0 propagated equality __const_100^post2 = __const_100^0 propagated equality tmp13^post2 = tmp13^0 propagated equality tmp9^post2 = tmp9^0 propagated equality size15^post2 = size15^0 propagated equality size11^post2 = size11^0 propagated equality tmp22^post2 = tmp22^0 Simplified Guard Original rule: l0 -> l1 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^post3, __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, (-__const_100^post3+__const_100^0 == 0 /\ -__len21^post3+__len21^0 == 0 /\ tmp^0-tmp^post3 == 0 /\ size7^0-size7^post3 == 0 /\ -ret_my_malloc10^post3+ret_my_malloc10^0 == 0 /\ -size17^post3+size17^0 == 0 /\ -retval^post3+retval^0 == 0 /\ tmp___1^0-tmp___1^post3 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post3 == 0 /\ tmp13^0-tmp13^post3 == 0 /\ size15^0-size15^post3 == 0 /\ -tmp9^post3+tmp9^0 == 0 /\ tmp___0^0-tmp___0^post3 == 0 /\ -tmp22^post3+tmp22^0 == 0 /\ size11^0-size11^post3 == 0), cost: 1 New rule: l2 -> l3 : __const_100^0'=__const_100^0, __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 __const_100^post3 = __const_100^0 propagated equality __len21^post3 = __len21^0 propagated equality tmp^post3 = tmp^0 propagated equality size7^post3 = size7^0 propagated equality ret_my_malloc10^post3 = ret_my_malloc10^0 propagated equality size17^post3 = size17^0 propagated equality retval^post3 = retval^0 propagated equality tmp___1^post3 = tmp___1^0 propagated equality ret_my_malloc14^post3 = ret_my_malloc14^0 propagated equality tmp13^post3 = tmp13^0 propagated equality size15^post3 = size15^0 propagated equality tmp9^post3 = tmp9^0 propagated equality tmp___0^post3 = tmp___0^0 propagated equality tmp22^post3 = tmp22^0 propagated equality size11^post3 = size11^0 Simplified Guard Original rule: l2 -> l3 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^post4, __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 /\ -__len21^post4+__len21^0 == 0 /\ size15^0-size15^post4 == 0 /\ -ret_my_malloc10^post4+ret_my_malloc10^0 == 0 /\ -size7^post4+size7^0 == 0 /\ -tmp___1^post4+tmp___1^0 == 0 /\ -tmp9^post4+tmp9^0 == 0 /\ -tmp13^post4+tmp13^0 == 0 /\ size17^0-size17^post4 == 0 /\ tmp^0-tmp^post4 == 0 /\ -__const_100^post4+__const_100^0 == 0 /\ -size11^post4+size11^0 == 0 /\ retval^0-retval^post4 == 0 /\ tmp22^0-tmp22^post4 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post4 == 0), cost: 1 New rule: l4 -> l2 : __const_100^0'=__const_100^0, __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 __len21^post4 = __len21^0 propagated equality size15^post4 = size15^0 propagated equality ret_my_malloc10^post4 = ret_my_malloc10^0 propagated equality size7^post4 = size7^0 propagated equality tmp___1^post4 = tmp___1^0 propagated equality tmp9^post4 = tmp9^0 propagated equality tmp13^post4 = tmp13^0 propagated equality size17^post4 = size17^0 propagated equality tmp^post4 = tmp^0 propagated equality __const_100^post4 = __const_100^0 propagated equality size11^post4 = size11^0 propagated equality retval^post4 = retval^0 propagated equality tmp22^post4 = tmp22^0 propagated equality ret_my_malloc14^post4 = ret_my_malloc14^0 Simplified Guard Original rule: l4 -> l2 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^post5, __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 /\ size15^0-size15^post5 == 0 /\ -size17^post5+size17^0 == 0 /\ -tmp___0^post5+tmp___0^0 == 0 /\ __len21^post5-__const_100^0 == 0 /\ size11^0-size11^post5 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post5 == 0 /\ -retval^post5+retval^0 == 0 /\ -tmp9^post5+tmp9^0 == 0 /\ -tmp13^post5+tmp13^0 == 0 /\ 1+tmp___1^0 <= 0 /\ -1-tmp___1^0 <= 0 /\ size7^0-size7^post5 == 0 /\ tmp^0-tmp^post5 == 0 /\ -__const_100^post5+__const_100^0 == 0 /\ tmp___1^0-tmp___1^post5 == 0 /\ -ret_my_malloc14^post5+ret_my_malloc14^0 == 0), cost: 1 New rule: l5 -> l2 : __const_100^0'=__const_100^post5, __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 /\ size15^0-size15^post5 == 0 /\ -size17^post5+size17^0 == 0 /\ -tmp___0^post5+tmp___0^0 == 0 /\ __len21^post5-__const_100^0 == 0 /\ size11^0-size11^post5 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post5 == 0 /\ -retval^post5+retval^0 == 0 /\ -tmp9^post5+tmp9^0 == 0 /\ -tmp13^post5+tmp13^0 == 0 /\ 1+tmp___1^0 <= 0 /\ 1+tmp___1^0 == 0 /\ -1-tmp___1^0 <= 0 /\ size7^0-size7^post5 == 0 /\ tmp^0-tmp^post5 == 0 /\ -__const_100^post5+__const_100^0 == 0 /\ tmp___1^0-tmp___1^post5 == 0 /\ -ret_my_malloc14^post5+ret_my_malloc14^0 == 0), cost: 1 Propagated Equalities Original rule: l5 -> l2 : __const_100^0'=__const_100^post5, __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 /\ size15^0-size15^post5 == 0 /\ -size17^post5+size17^0 == 0 /\ -tmp___0^post5+tmp___0^0 == 0 /\ __len21^post5-__const_100^0 == 0 /\ size11^0-size11^post5 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post5 == 0 /\ -retval^post5+retval^0 == 0 /\ -tmp9^post5+tmp9^0 == 0 /\ -tmp13^post5+tmp13^0 == 0 /\ 1+tmp___1^0 <= 0 /\ 1+tmp___1^0 == 0 /\ -1-tmp___1^0 <= 0 /\ size7^0-size7^post5 == 0 /\ tmp^0-tmp^post5 == 0 /\ -__const_100^post5+__const_100^0 == 0 /\ tmp___1^0-tmp___1^post5 == 0 /\ -ret_my_malloc14^post5+ret_my_malloc14^0 == 0), cost: 1 New rule: l5 -> l2 : __const_100^0'=__const_100^0, __len21^0'=__const_100^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^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 size15^post5 = size15^0 propagated equality size17^post5 = size17^0 propagated equality tmp___0^post5 = tmp___0^0 propagated equality __len21^post5 = __const_100^0 propagated equality size11^post5 = size11^0 propagated equality ret_my_malloc10^post5 = ret_my_malloc10^0 propagated equality retval^post5 = retval^0 propagated equality tmp9^post5 = tmp9^0 propagated equality tmp13^post5 = tmp13^0 propagated equality size7^post5 = size7^0 propagated equality tmp^post5 = tmp^0 propagated equality __const_100^post5 = __const_100^0 propagated equality tmp___1^post5 = tmp___1^0 propagated equality ret_my_malloc14^post5 = ret_my_malloc14^0 Simplified Guard Original rule: l5 -> l2 : __const_100^0'=__const_100^0, __len21^0'=__const_100^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^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 : __const_100^0'=__const_100^0, __len21^0'=__const_100^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^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 : __const_100^0'=__const_100^0, __len21^0'=__const_100^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^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 : __const_100^0'=__const_100^0, __len21^0'=__const_100^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^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 : __const_100^0'=__const_100^0, __len21^0'=__const_100^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^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'=__const_100^0, 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 : __const_100^0'=__const_100^post6, __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, (tmp^0-tmp^post6 == 0 /\ -tmp___0^post6+tmp___0^0 == 0 /\ size7^0-size7^post6 == 0 /\ -size17^post6+size17^0 == 0 /\ -tmp___1^0 <= 0 /\ ret_my_malloc14^0-ret_my_malloc14^post6 == 0 /\ -tmp9^post6+tmp9^0 == 0 /\ -retval^post6+retval^0 == 0 /\ tmp13^0-tmp13^post6 == 0 /\ tmp___1^0-tmp___1^post6 == 0 /\ size15^0-size15^post6 == 0 /\ -ret_my_malloc10^post6+ret_my_malloc10^0 == 0 /\ size11^0-size11^post6 == 0 /\ -__const_100^post6+__const_100^0 == 0 /\ -__len21^post6+__len21^0 == 0 /\ -tmp22^post6+tmp22^0 == 0), cost: 1 New rule: l5 -> l4 : __const_100^0'=__const_100^0, __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 tmp^post6 = tmp^0 propagated equality tmp___0^post6 = tmp___0^0 propagated equality size7^post6 = size7^0 propagated equality size17^post6 = size17^0 propagated equality ret_my_malloc14^post6 = ret_my_malloc14^0 propagated equality tmp9^post6 = tmp9^0 propagated equality retval^post6 = retval^0 propagated equality tmp13^post6 = tmp13^0 propagated equality tmp___1^post6 = tmp___1^0 propagated equality size15^post6 = size15^0 propagated equality ret_my_malloc10^post6 = ret_my_malloc10^0 propagated equality size11^post6 = size11^0 propagated equality __const_100^post6 = __const_100^0 propagated equality __len21^post6 = __len21^0 propagated equality tmp22^post6 = tmp22^0 Simplified Guard Original rule: l5 -> l4 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^post7, __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, (tmp^0-tmp^post7 == 0 /\ size7^0-size7^post7 == 0 /\ -retval^post7+retval^0 == 0 /\ size11^0-size11^post7 == 0 /\ tmp___1^0-tmp___1^post7 == 0 /\ -tmp22^post7+tmp22^0 == 0 /\ tmp13^0-tmp13^post7 == 0 /\ -tmp9^post7+tmp9^0 == 0 /\ -ret_my_malloc10^post7+ret_my_malloc10^0 == 0 /\ tmp___0^0-tmp___0^post7 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post7 == 0 /\ -__const_100^post7+__const_100^0 == 0 /\ size15^0-size15^post7 == 0 /\ -size17^post7+size17^0 == 0 /\ __len21^0-__len21^post7 == 0 /\ 2+tmp___1^0 <= 0), cost: 1 New rule: l5 -> l4 : __const_100^0'=__const_100^0, __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 tmp^post7 = tmp^0 propagated equality size7^post7 = size7^0 propagated equality retval^post7 = retval^0 propagated equality size11^post7 = size11^0 propagated equality tmp___1^post7 = tmp___1^0 propagated equality tmp22^post7 = tmp22^0 propagated equality tmp13^post7 = tmp13^0 propagated equality tmp9^post7 = tmp9^0 propagated equality ret_my_malloc10^post7 = ret_my_malloc10^0 propagated equality tmp___0^post7 = tmp___0^0 propagated equality ret_my_malloc14^post7 = ret_my_malloc14^0 propagated equality __const_100^post7 = __const_100^0 propagated equality size15^post7 = size15^0 propagated equality size17^post7 = size17^0 propagated equality __len21^post7 = __len21^0 Simplified Guard Original rule: l5 -> l4 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^post8, __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, (tmp___0^0-tmp___0^post8 == 0 /\ size15^0-size15^post8 == 0 /\ -size11^post8+size11^0 == 0 /\ -size7^post8+size7^0 == 0 /\ -tmp___1^post8+tmp___1^0 == 0 /\ -tmp13^post8+tmp13^0 == 0 /\ -tmp9^post8+tmp9^0 == 0 /\ -__const_100^post8+__const_100^0 == 0 /\ tmp^0-tmp^post8 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post8 == 0 /\ -ret_my_malloc10^post8+ret_my_malloc10^0 == 0 /\ -retval^post8+retval^0 == 0 /\ __len21^0-__len21^post8 == 0 /\ tmp22^0-tmp22^post8 == 0 /\ size17^0-size17^post8 == 0), cost: 1 New rule: l6 -> l3 : __const_100^0'=__const_100^0, __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^post8 = tmp___0^0 propagated equality size15^post8 = size15^0 propagated equality size11^post8 = size11^0 propagated equality size7^post8 = size7^0 propagated equality tmp___1^post8 = tmp___1^0 propagated equality tmp13^post8 = tmp13^0 propagated equality tmp9^post8 = tmp9^0 propagated equality __const_100^post8 = __const_100^0 propagated equality tmp^post8 = tmp^0 propagated equality ret_my_malloc14^post8 = ret_my_malloc14^0 propagated equality ret_my_malloc10^post8 = ret_my_malloc10^0 propagated equality retval^post8 = retval^0 propagated equality __len21^post8 = __len21^0 propagated equality tmp22^post8 = tmp22^0 propagated equality size17^post8 = size17^0 Simplified Guard Original rule: l6 -> l3 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^post9, __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, (size15^0-size15^post9 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post9 == 0 /\ -size17^post9+size17^0 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post9 == 0 /\ __len21^0-__len21^post9 == 0 /\ size11^0-size11^post9 == 0 /\ -tmp13^post9+tmp13^0 == 0 /\ -__const_100^post9+__const_100^0 == 0 /\ tmp^0-tmp^post9 == 0 /\ -tmp9^post9+tmp9^0 == 0 /\ size7^0-size7^post9 == 0 /\ -retval^post9+retval^0 == 0 /\ tmp22^0-tmp22^post9 == 0 /\ -tmp___0^post9+tmp___0^0 == 0 /\ tmp___1^0-tmp___1^post9 == 0), cost: 1 New rule: l7 -> l6 : __const_100^0'=__const_100^0, __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^post9 = size15^0 propagated equality ret_my_malloc10^post9 = ret_my_malloc10^0 propagated equality size17^post9 = size17^0 propagated equality ret_my_malloc14^post9 = ret_my_malloc14^0 propagated equality __len21^post9 = __len21^0 propagated equality size11^post9 = size11^0 propagated equality tmp13^post9 = tmp13^0 propagated equality __const_100^post9 = __const_100^0 propagated equality tmp^post9 = tmp^0 propagated equality tmp9^post9 = tmp9^0 propagated equality size7^post9 = size7^0 propagated equality retval^post9 = retval^0 propagated equality tmp22^post9 = tmp22^0 propagated equality tmp___0^post9 = tmp___0^0 propagated equality tmp___1^post9 = tmp___1^0 Simplified Guard Original rule: l7 -> l6 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^post10, __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, (tmp^0-tmp^post10 == 0 /\ size7^0-size7^post10 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post10 == 0 /\ -size17^post10+size17^0 == 0 /\ size15^0-size15^post10 == 0 /\ -size11^post10+size11^0 == 0 /\ tmp13^0-tmp13^post10 == 0 /\ tmp___1^0-tmp___1^post10 == 0 /\ -ret_my_malloc10^post10+ret_my_malloc10^0 == 0 /\ -tmp22^post10+tmp22^0 == 0 /\ tmp___0^0-tmp___0^post10 == 0 /\ -tmp9^post10+tmp9^0 == 0 /\ -__const_100^post10+__const_100^0 == 0 /\ -__len21^post10+__len21^0 == 0 /\ -retval^post10+retval^0 == 0), cost: 1 New rule: l8 -> l7 : __const_100^0'=__const_100^0, __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^post10 = tmp^0 propagated equality size7^post10 = size7^0 propagated equality ret_my_malloc14^post10 = ret_my_malloc14^0 propagated equality size17^post10 = size17^0 propagated equality size15^post10 = size15^0 propagated equality size11^post10 = size11^0 propagated equality tmp13^post10 = tmp13^0 propagated equality tmp___1^post10 = tmp___1^0 propagated equality ret_my_malloc10^post10 = ret_my_malloc10^0 propagated equality tmp22^post10 = tmp22^0 propagated equality tmp___0^post10 = tmp___0^0 propagated equality tmp9^post10 = tmp9^0 propagated equality __const_100^post10 = __const_100^0 propagated equality __len21^post10 = __len21^0 propagated equality retval^post10 = retval^0 Simplified Guard Original rule: l8 -> l7 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^post11, __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, (tmp^0-tmp^post11 == 0 /\ -size7^post11+size7^0 == 0 /\ -size11^post11+size11^0 == 0 /\ tmp___1^0-tmp___1^post11 == 0 /\ -ret_my_malloc10^post11+ret_my_malloc10^0 == 0 /\ tmp___0^0-tmp___0^post11 == 0 /\ tmp13^0-tmp13^post11 == 0 /\ retval^0-retval^post11 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post11 == 0 /\ -size17^post11+size17^0 == 0 /\ -tmp22^post11+tmp22^0 == 0 /\ -__const_100^post11+__const_100^0 == 0 /\ -tmp9^post11+tmp9^0 == 0 /\ size15^0-size15^post11 == 0 /\ __len21^0-__len21^post11 == 0), cost: 1 New rule: l8 -> l6 : __const_100^0'=__const_100^0, __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^post11 = tmp^0 propagated equality size7^post11 = size7^0 propagated equality size11^post11 = size11^0 propagated equality tmp___1^post11 = tmp___1^0 propagated equality ret_my_malloc10^post11 = ret_my_malloc10^0 propagated equality tmp___0^post11 = tmp___0^0 propagated equality tmp13^post11 = tmp13^0 propagated equality retval^post11 = retval^0 propagated equality ret_my_malloc14^post11 = ret_my_malloc14^0 propagated equality size17^post11 = size17^0 propagated equality tmp22^post11 = tmp22^0 propagated equality __const_100^post11 = __const_100^0 propagated equality tmp9^post11 = tmp9^0 propagated equality size15^post11 = size15^0 propagated equality __len21^post11 = __len21^0 Simplified Guard Original rule: l8 -> l6 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^post12, __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^0-tmp___0^post12 == 0 /\ -size17^post12+size17^0 == 0 /\ -tmp___1^post12+tmp___1^0 == 0 /\ -tmp13^post12+tmp13^0 == 0 /\ tmp^0-tmp^post12 == 0 /\ -__const_100^post12+__const_100^0 == 0 /\ -ret_my_malloc10^post12+ret_my_malloc10^0 == 0 /\ -retval^post12+retval^0 == 0 /\ -tmp9^post12+tmp9^0 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post12 == 0 /\ -size11^post12+size11^0 == 0 /\ -size7^post12+size7^0 == 0 /\ __len21^0-__len21^post12 == 0 /\ size15^0-size15^post12 == 0 /\ tmp22^0-tmp22^post12 == 0), cost: 1 New rule: l8 -> l7 : __const_100^0'=__const_100^0, __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^post12 = tmp___0^0 propagated equality size17^post12 = size17^0 propagated equality tmp___1^post12 = tmp___1^0 propagated equality tmp13^post12 = tmp13^0 propagated equality tmp^post12 = tmp^0 propagated equality __const_100^post12 = __const_100^0 propagated equality ret_my_malloc10^post12 = ret_my_malloc10^0 propagated equality retval^post12 = retval^0 propagated equality tmp9^post12 = tmp9^0 propagated equality ret_my_malloc14^post12 = ret_my_malloc14^0 propagated equality size11^post12 = size11^0 propagated equality size7^post12 = size7^0 propagated equality __len21^post12 = __len21^0 propagated equality size15^post12 = size15^0 propagated equality tmp22^post12 = tmp22^0 Simplified Guard Original rule: l8 -> l7 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^post13, __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, (-tmp13^post13+tmp13^0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post13 == 0 /\ size11^0-size11^post13 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post13 == 0 /\ __len21^0-__len21^post13 == 0 /\ size7^0-size7^post13 == 0 /\ size17^post13-__const_100^0 == 0 /\ size15^0-size15^post13 == 0 /\ -tmp9^post13+tmp9^0 == 0 /\ tmp^0-tmp^post13 == 0 /\ -__const_100^post13+__const_100^0 == 0 /\ -retval^post13+retval^0 == 0 /\ -tmp___0^post13+tmp___0^0 == 0 /\ tmp22^0-tmp22^post13 == 0 /\ tmp___1^0-tmp___1^post13 == 0), cost: 1 New rule: l9 -> l8 : __const_100^0'=__const_100^0, __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'=__const_100^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 tmp13^post13 = tmp13^0 propagated equality ret_my_malloc10^post13 = ret_my_malloc10^0 propagated equality size11^post13 = size11^0 propagated equality ret_my_malloc14^post13 = ret_my_malloc14^0 propagated equality __len21^post13 = __len21^0 propagated equality size7^post13 = size7^0 propagated equality size17^post13 = __const_100^0 propagated equality size15^post13 = size15^0 propagated equality tmp9^post13 = tmp9^0 propagated equality tmp^post13 = tmp^0 propagated equality __const_100^post13 = __const_100^0 propagated equality retval^post13 = retval^0 propagated equality tmp___0^post13 = tmp___0^0 propagated equality tmp22^post13 = tmp22^0 propagated equality tmp___1^post13 = tmp___1^0 Simplified Guard Original rule: l9 -> l8 : __const_100^0'=__const_100^0, __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'=__const_100^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: l9 -> l8 : __const_100^0'=__const_100^0, __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'=__const_100^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: l9 -> l8 : __const_100^0'=__const_100^0, __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'=__const_100^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: l9 -> l8 : size17^0'=__const_100^0, T, cost: 1 Propagated Equalities Original rule: l10 -> l3 : __const_100^0'=__const_100^post14, __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, (tmp^0-tmp^post14 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post14 == 0 /\ size15^0-size15^post14 == 0 /\ -size11^post14+size11^0 == 0 /\ tmp___1^0-tmp___1^post14 == 0 /\ -__len21^post14+__len21^0 == 0 /\ -tmp9^post14+tmp9^0 == 0 /\ tmp___0^0-tmp___0^post14 == 0 /\ tmp22^0-tmp22^post14 == 0 /\ -__const_100^post14+__const_100^0 == 0 /\ -size17^post14+size17^0 == 0 /\ -size7^post14+size7^0 == 0 /\ -ret_my_malloc10^post14+ret_my_malloc10^0 == 0 /\ -retval^post14+retval^0 == 0 /\ -tmp13^post14+tmp13^0 == 0), cost: 1 New rule: l10 -> l3 : __const_100^0'=__const_100^0, __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^post14 = tmp^0 propagated equality ret_my_malloc14^post14 = ret_my_malloc14^0 propagated equality size15^post14 = size15^0 propagated equality size11^post14 = size11^0 propagated equality tmp___1^post14 = tmp___1^0 propagated equality __len21^post14 = __len21^0 propagated equality tmp9^post14 = tmp9^0 propagated equality tmp___0^post14 = tmp___0^0 propagated equality tmp22^post14 = tmp22^0 propagated equality __const_100^post14 = __const_100^0 propagated equality size17^post14 = size17^0 propagated equality size7^post14 = size7^0 propagated equality ret_my_malloc10^post14 = ret_my_malloc10^0 propagated equality retval^post14 = retval^0 propagated equality tmp13^post14 = tmp13^0 Simplified Guard Original rule: l10 -> l3 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^post15, __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, (tmp9^0-tmp9^post15 == 0 /\ tmp___1^0-tmp___1^post15 == 0 /\ -tmp13^post15+tmp13^0 == 0 /\ tmp22^0-tmp22^post15 == 0 /\ -size11^post15+size11^0 == 0 /\ -tmp___0^post15+tmp___0^0 == 0 /\ -__const_100^post15+__const_100^0 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post15 == 0 /\ -size7^post15+size7^0 == 0 /\ -size17^post15+size17^0 == 0 /\ -ret_my_malloc10^post15+ret_my_malloc10^0 == 0 /\ size15^0-size15^post15 == 0 /\ __len21^0-__len21^post15 == 0 /\ -retval^post15+retval^0 == 0 /\ tmp^0-tmp^post15 == 0), cost: 1 New rule: l11 -> l10 : __const_100^0'=__const_100^0, __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 tmp9^post15 = tmp9^0 propagated equality tmp___1^post15 = tmp___1^0 propagated equality tmp13^post15 = tmp13^0 propagated equality tmp22^post15 = tmp22^0 propagated equality size11^post15 = size11^0 propagated equality tmp___0^post15 = tmp___0^0 propagated equality __const_100^post15 = __const_100^0 propagated equality ret_my_malloc14^post15 = ret_my_malloc14^0 propagated equality size7^post15 = size7^0 propagated equality size17^post15 = size17^0 propagated equality ret_my_malloc10^post15 = ret_my_malloc10^0 propagated equality size15^post15 = size15^0 propagated equality __len21^post15 = __len21^0 propagated equality retval^post15 = retval^0 propagated equality tmp^post15 = tmp^0 Simplified Guard Original rule: l11 -> l10 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^post16, __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, (-__len21^post16+__len21^0 == 0 /\ -tmp13^post16+tmp13^0 == 0 /\ -tmp9^post16+tmp9^0 == 0 /\ size15^0-size15^post16 == 0 /\ tmp___1^0-tmp___1^post16 == 0 /\ -size11^post16+size11^0 == 0 /\ -retval^post16+retval^0 == 0 /\ size17^0-size17^post16 == 0 /\ tmp^0-tmp^post16 == 0 /\ tmp___0^0-tmp___0^post16 == 0 /\ tmp22^0-tmp22^post16 == 0 /\ -__const_100^post16+__const_100^0 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post16 == 0 /\ -size7^post16+size7^0 == 0 /\ -ret_my_malloc10^post16+ret_my_malloc10^0 == 0), cost: 1 New rule: l12 -> l11 : __const_100^0'=__const_100^0, __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 __len21^post16 = __len21^0 propagated equality tmp13^post16 = tmp13^0 propagated equality tmp9^post16 = tmp9^0 propagated equality size15^post16 = size15^0 propagated equality tmp___1^post16 = tmp___1^0 propagated equality size11^post16 = size11^0 propagated equality retval^post16 = retval^0 propagated equality size17^post16 = size17^0 propagated equality tmp^post16 = tmp^0 propagated equality tmp___0^post16 = tmp___0^0 propagated equality tmp22^post16 = tmp22^0 propagated equality __const_100^post16 = __const_100^0 propagated equality ret_my_malloc14^post16 = ret_my_malloc14^0 propagated equality size7^post16 = size7^0 propagated equality ret_my_malloc10^post16 = ret_my_malloc10^0 Simplified Guard Original rule: l12 -> l11 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^post17, __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, (tmp9^0-tmp9^post17 == 0 /\ size7^0-size7^post17 == 0 /\ tmp^0-tmp^post17 == 0 /\ tmp22^0-tmp22^post17 == 0 /\ -tmp13^post17+tmp13^0 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post17 == 0 /\ tmp___0^0-tmp___0^post17 == 0 /\ -size17^post17+size17^0 == 0 /\ -retval^post17+retval^0 == 0 /\ -size11^post17+size11^0 == 0 /\ tmp___1^0-tmp___1^post17 == 0 /\ __len21^0-__len21^post17 == 0 /\ -__const_100^post17+__const_100^0 == 0 /\ size15^0-size15^post17 == 0 /\ -ret_my_malloc10^post17+ret_my_malloc10^0 == 0), cost: 1 New rule: l12 -> l10 : __const_100^0'=__const_100^0, __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 tmp9^post17 = tmp9^0 propagated equality size7^post17 = size7^0 propagated equality tmp^post17 = tmp^0 propagated equality tmp22^post17 = tmp22^0 propagated equality tmp13^post17 = tmp13^0 propagated equality ret_my_malloc14^post17 = ret_my_malloc14^0 propagated equality tmp___0^post17 = tmp___0^0 propagated equality size17^post17 = size17^0 propagated equality retval^post17 = retval^0 propagated equality size11^post17 = size11^0 propagated equality tmp___1^post17 = tmp___1^0 propagated equality __len21^post17 = __len21^0 propagated equality __const_100^post17 = __const_100^0 propagated equality size15^post17 = size15^0 propagated equality ret_my_malloc10^post17 = ret_my_malloc10^0 Simplified Guard Original rule: l12 -> l10 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^post18, __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, (-tmp22^post18+tmp22^0 == 0 /\ tmp___1^0-tmp___1^post18 == 0 /\ -tmp9^post18+tmp9^0 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post18 == 0 /\ tmp13^0-tmp13^post18 == 0 /\ -__len21^post18+__len21^0 == 0 /\ -size17^post18+size17^0 == 0 /\ -tmp___0^post18+tmp___0^0 == 0 /\ size11^0-size11^post18 == 0 /\ -retval^post18+retval^0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post18 == 0 /\ size7^0-size7^post18 == 0 /\ tmp^0-tmp^post18 == 0 /\ size15^0-size15^post18 == 0 /\ -__const_100^post18+__const_100^0 == 0), cost: 1 New rule: l12 -> l11 : __const_100^0'=__const_100^0, __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^post18 = tmp22^0 propagated equality tmp___1^post18 = tmp___1^0 propagated equality tmp9^post18 = tmp9^0 propagated equality ret_my_malloc14^post18 = ret_my_malloc14^0 propagated equality tmp13^post18 = tmp13^0 propagated equality __len21^post18 = __len21^0 propagated equality size17^post18 = size17^0 propagated equality tmp___0^post18 = tmp___0^0 propagated equality size11^post18 = size11^0 propagated equality retval^post18 = retval^0 propagated equality ret_my_malloc10^post18 = ret_my_malloc10^0 propagated equality size7^post18 = size7^0 propagated equality tmp^post18 = tmp^0 propagated equality size15^post18 = size15^0 propagated equality __const_100^post18 = __const_100^0 Simplified Guard Original rule: l12 -> l11 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^post19, __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, (size15^post19-__const_100^0 == 0 /\ -tmp___1^post19+tmp___1^0 == 0 /\ -tmp9^post19+tmp9^0 == 0 /\ -tmp13^post19+tmp13^0 == 0 /\ tmp^0-tmp^post19 == 0 /\ -__len21^post19+__len21^0 == 0 /\ -size11^post19+size11^0 == 0 /\ -retval^post19+retval^0 == 0 /\ tmp22^0-tmp22^post19 == 0 /\ size17^0-size17^post19 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post19 == 0 /\ -ret_my_malloc10^post19+ret_my_malloc10^0 == 0 /\ tmp___0^0-tmp___0^post19 == 0 /\ -__const_100^post19+__const_100^0 == 0 /\ -size7^post19+size7^0 == 0), cost: 1 New rule: l13 -> l12 : __const_100^0'=__const_100^0, __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'=__const_100^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^post19 = __const_100^0 propagated equality tmp___1^post19 = tmp___1^0 propagated equality tmp9^post19 = tmp9^0 propagated equality tmp13^post19 = tmp13^0 propagated equality tmp^post19 = tmp^0 propagated equality __len21^post19 = __len21^0 propagated equality size11^post19 = size11^0 propagated equality retval^post19 = retval^0 propagated equality tmp22^post19 = tmp22^0 propagated equality size17^post19 = size17^0 propagated equality ret_my_malloc14^post19 = ret_my_malloc14^0 propagated equality ret_my_malloc10^post19 = ret_my_malloc10^0 propagated equality tmp___0^post19 = tmp___0^0 propagated equality __const_100^post19 = __const_100^0 propagated equality size7^post19 = size7^0 Simplified Guard Original rule: l13 -> l12 : __const_100^0'=__const_100^0, __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'=__const_100^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: l13 -> l12 : __const_100^0'=__const_100^0, __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'=__const_100^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: l13 -> l12 : __const_100^0'=__const_100^0, __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'=__const_100^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: l13 -> l12 : size15^0'=__const_100^0, T, cost: 1 Propagated Equalities Original rule: l14 -> l15 : __const_100^0'=__const_100^post20, __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, (-size7^post20+size7^0 == 0 /\ retval^post20-ret_my_malloc14^0 == 0 /\ size15^0-size15^post20 == 0 /\ -tmp___1^post20+tmp___1^0 == 0 /\ -tmp9^post20+tmp9^0 == 0 /\ -__len21^post20+__len21^0 == 0 /\ -tmp13^post20+tmp13^0 == 0 /\ -__const_100^post20+__const_100^0 == 0 /\ size17^0-size17^post20 == 0 /\ tmp^0-tmp^post20 == 0 /\ tmp22^0-tmp22^post20 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post20 == 0 /\ -ret_my_malloc10^post20+ret_my_malloc10^0 == 0 /\ -size11^post20+size11^0 == 0 /\ tmp___0^0-tmp___0^post20 == 0), cost: 1 New rule: l14 -> l15 : __const_100^0'=__const_100^0, __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 size7^post20 = size7^0 propagated equality retval^post20 = ret_my_malloc14^0 propagated equality size15^post20 = size15^0 propagated equality tmp___1^post20 = tmp___1^0 propagated equality tmp9^post20 = tmp9^0 propagated equality __len21^post20 = __len21^0 propagated equality tmp13^post20 = tmp13^0 propagated equality __const_100^post20 = __const_100^0 propagated equality size17^post20 = size17^0 propagated equality tmp^post20 = tmp^0 propagated equality tmp22^post20 = tmp22^0 propagated equality ret_my_malloc14^post20 = ret_my_malloc14^0 propagated equality ret_my_malloc10^post20 = ret_my_malloc10^0 propagated equality size11^post20 = size11^0 propagated equality tmp___0^post20 = tmp___0^0 Simplified Guard Original rule: l14 -> l15 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^post21, __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 /\ -size17^post21+size17^0 == 0 /\ tmp^0-tmp^post21 == 0 /\ size7^0-size7^post21 == 0 /\ tmp9^0-tmp9^post21 == 0 /\ -tmp13^post21+tmp13^0 == 0 /\ tmp22^0-tmp22^post21 == 0 /\ -__const_100^post21+__const_100^0 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post21 == 0 /\ tmp___0^0-tmp___0^post21 == 0 /\ __len21^0-__len21^post21 == 0 /\ -retval^post21+retval^0 == 0 /\ size15^0-size15^post21 == 0 /\ 1-retval^0 <= 0 /\ -1+retval^0 <= 0 /\ -ret_my_malloc10^post21+ret_my_malloc10^0 == 0 /\ -size11^post21+size11^0 == 0), cost: 1 New rule: l15 -> l5 : __const_100^0'=__const_100^post21, __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 /\ -size17^post21+size17^0 == 0 /\ tmp^0-tmp^post21 == 0 /\ size7^0-size7^post21 == 0 /\ tmp9^0-tmp9^post21 == 0 /\ -tmp13^post21+tmp13^0 == 0 /\ tmp22^0-tmp22^post21 == 0 /\ -__const_100^post21+__const_100^0 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post21 == 0 /\ tmp___0^0-tmp___0^post21 == 0 /\ __len21^0-__len21^post21 == 0 /\ -retval^post21+retval^0 == 0 /\ size15^0-size15^post21 == 0 /\ 1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0 /\ -ret_my_malloc10^post21+ret_my_malloc10^0 == 0 /\ -size11^post21+size11^0 == 0), cost: 1 Propagated Equalities Original rule: l15 -> l5 : __const_100^0'=__const_100^post21, __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 /\ -size17^post21+size17^0 == 0 /\ tmp^0-tmp^post21 == 0 /\ size7^0-size7^post21 == 0 /\ tmp9^0-tmp9^post21 == 0 /\ -tmp13^post21+tmp13^0 == 0 /\ tmp22^0-tmp22^post21 == 0 /\ -__const_100^post21+__const_100^0 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post21 == 0 /\ tmp___0^0-tmp___0^post21 == 0 /\ __len21^0-__len21^post21 == 0 /\ -retval^post21+retval^0 == 0 /\ size15^0-size15^post21 == 0 /\ 1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0 /\ -ret_my_malloc10^post21+ret_my_malloc10^0 == 0 /\ -size11^post21+size11^0 == 0), cost: 1 New rule: l15 -> l5 : __const_100^0'=__const_100^0, __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 size17^post21 = size17^0 propagated equality tmp^post21 = tmp^0 propagated equality size7^post21 = size7^0 propagated equality tmp9^post21 = tmp9^0 propagated equality tmp13^post21 = tmp13^0 propagated equality tmp22^post21 = tmp22^0 propagated equality __const_100^post21 = __const_100^0 propagated equality ret_my_malloc14^post21 = ret_my_malloc14^0 propagated equality tmp___0^post21 = tmp___0^0 propagated equality __len21^post21 = __len21^0 propagated equality retval^post21 = retval^0 propagated equality size15^post21 = size15^0 propagated equality ret_my_malloc10^post21 = ret_my_malloc10^0 propagated equality size11^post21 = size11^0 Simplified Guard Original rule: l15 -> l5 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^post22, __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, (-tmp___0^post22+tmp___0^0 == 0 /\ -tmp22^post22+tmp22^0 == 0 /\ tmp^0-tmp^post22 == 0 /\ -__const_100^post22+__const_100^0 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post22 == 0 /\ tmp13^0-tmp13^post22 == 0 /\ tmp___1^0-tmp___1^post22 == 0 /\ -tmp9^post22+tmp9^0 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post22 == 0 /\ -size17^post22+size17^0 == 0 /\ size11^0-size11^post22 == 0 /\ -retval^post22+retval^0 == 0 /\ -__len21^post22+__len21^0 == 0 /\ size7^0-size7^post22 == 0 /\ 2-retval^0 <= 0 /\ size15^0-size15^post22 == 0), cost: 1 New rule: l15 -> l13 : __const_100^0'=__const_100^0, __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___0^post22 = tmp___0^0 propagated equality tmp22^post22 = tmp22^0 propagated equality tmp^post22 = tmp^0 propagated equality __const_100^post22 = __const_100^0 propagated equality ret_my_malloc14^post22 = ret_my_malloc14^0 propagated equality tmp13^post22 = tmp13^0 propagated equality tmp___1^post22 = tmp___1^0 propagated equality tmp9^post22 = tmp9^0 propagated equality ret_my_malloc10^post22 = ret_my_malloc10^0 propagated equality size17^post22 = size17^0 propagated equality size11^post22 = size11^0 propagated equality retval^post22 = retval^0 propagated equality __len21^post22 = __len21^0 propagated equality size7^post22 = size7^0 propagated equality size15^post22 = size15^0 Simplified Guard Original rule: l15 -> l13 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^post23, __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___1^post23+tmp___1^0 == 0 /\ -tmp13^post23+tmp13^0 == 0 /\ -ret_my_malloc10^post23+ret_my_malloc10^0 == 0 /\ -tmp9^post23+tmp9^0 == 0 /\ -__const_100^post23+__const_100^0 == 0 /\ size15^0-size15^post23 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post23 == 0 /\ -size11^post23+size11^0 == 0 /\ -retval^post23+retval^0 == 0 /\ size17^0-size17^post23 == 0 /\ tmp^0-tmp^post23 == 0 /\ tmp22^0-tmp22^post23 == 0 /\ retval^0 <= 0 /\ __len21^0-__len21^post23 == 0 /\ tmp___0^0-tmp___0^post23 == 0 /\ -size7^post23+size7^0 == 0), cost: 1 New rule: l15 -> l13 : __const_100^0'=__const_100^0, __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___1^post23 = tmp___1^0 propagated equality tmp13^post23 = tmp13^0 propagated equality ret_my_malloc10^post23 = ret_my_malloc10^0 propagated equality tmp9^post23 = tmp9^0 propagated equality __const_100^post23 = __const_100^0 propagated equality size15^post23 = size15^0 propagated equality ret_my_malloc14^post23 = ret_my_malloc14^0 propagated equality size11^post23 = size11^0 propagated equality retval^post23 = retval^0 propagated equality size17^post23 = size17^0 propagated equality tmp^post23 = tmp^0 propagated equality tmp22^post23 = tmp22^0 propagated equality __len21^post23 = __len21^0 propagated equality tmp___0^post23 = tmp___0^0 propagated equality size7^post23 = size7^0 Simplified Guard Original rule: l15 -> l13 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^post24, __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, (-retval^post24+retval^0 == 0 /\ -size7^post24+size7^0 == 0 /\ size15^0-size15^post24 == 0 /\ -tmp___1^post24+tmp___1^0 == 0 /\ -ret_my_malloc10^post24+ret_my_malloc10^0 == 0 /\ -tmp13^post24+tmp13^0 == 0 /\ ret_my_malloc14^post24 == 0 /\ __len21^0-__len21^post24 == 0 /\ -__const_100^post24+__const_100^0 == 0 /\ -tmp9^post24+tmp9^0 == 0 /\ size17^0-size17^post24 == 0 /\ tmp^0-tmp^post24 == 0 /\ tmp22^0-tmp22^post24 == 0 /\ tmp___0^0-tmp___0^post24 == 0 /\ -size11^post24+size11^0 == 0), cost: 1 New rule: l16 -> l14 : __const_100^0'=__const_100^0, __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 retval^post24 = retval^0 propagated equality size7^post24 = size7^0 propagated equality size15^post24 = size15^0 propagated equality tmp___1^post24 = tmp___1^0 propagated equality ret_my_malloc10^post24 = ret_my_malloc10^0 propagated equality tmp13^post24 = tmp13^0 propagated equality ret_my_malloc14^post24 = 0 propagated equality __len21^post24 = __len21^0 propagated equality __const_100^post24 = __const_100^0 propagated equality tmp9^post24 = tmp9^0 propagated equality size17^post24 = size17^0 propagated equality tmp^post24 = tmp^0 propagated equality tmp22^post24 = tmp22^0 propagated equality tmp___0^post24 = tmp___0^0 propagated equality size11^post24 = size11^0 Simplified Guard Original rule: l16 -> l14 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^post25, __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, (-size17^post25+size17^0 == 0 /\ tmp9^0-tmp9^post25 == 0 /\ tmp^0-tmp^post25 == 0 /\ size7^0-size7^post25 == 0 /\ tmp___1^0-tmp___1^post25 == 0 /\ -tmp13^post25+tmp13^0 == 0 /\ -__const_100^post25+__const_100^0 == 0 /\ tmp22^0-tmp22^post25 == 0 /\ -ret_my_malloc10^post25+ret_my_malloc10^0 == 0 /\ tmp___0^0-tmp___0^post25 == 0 /\ __len21^0-__len21^post25 == 0 /\ size11^0-size11^post25 == 0 /\ size15^0-size15^post25 == 0 /\ -1+ret_my_malloc14^post25 == 0 /\ -retval^post25+retval^0 == 0), cost: 1 New rule: l16 -> l14 : __const_100^0'=__const_100^0, __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 size17^post25 = size17^0 propagated equality tmp9^post25 = tmp9^0 propagated equality tmp^post25 = tmp^0 propagated equality size7^post25 = size7^0 propagated equality tmp___1^post25 = tmp___1^0 propagated equality tmp13^post25 = tmp13^0 propagated equality __const_100^post25 = __const_100^0 propagated equality tmp22^post25 = tmp22^0 propagated equality ret_my_malloc10^post25 = ret_my_malloc10^0 propagated equality tmp___0^post25 = tmp___0^0 propagated equality __len21^post25 = __len21^0 propagated equality size11^post25 = size11^0 propagated equality size15^post25 = size15^0 propagated equality ret_my_malloc14^post25 = 1 propagated equality retval^post25 = retval^0 Simplified Guard Original rule: l16 -> l14 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^post26, __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, (-size17^post26+size17^0 == 0 /\ -tmp___0^post26+tmp___0^0 == 0 /\ -ret_my_malloc14^post26+ret_my_malloc14^0 == 0 /\ size7^0-size7^post26 == 0 /\ tmp^0-tmp^post26 == 0 /\ -tmp9^post26+tmp9^0 == 0 /\ tmp___1^0-tmp___1^post26 == 0 /\ -__const_100^post26+__const_100^0 == 0 /\ tmp13^0-tmp13^post26 == 0 /\ ret_my_malloc10^0-ret_my_malloc10^post26 == 0 /\ -__len21^post26+__len21^0 == 0 /\ size15^0-size15^post26 == 0 /\ 2-retval^0 <= 0 /\ -tmp22^post26+tmp22^0 == 0 /\ -retval^post26+retval^0 == 0 /\ size11^0-size11^post26 == 0), cost: 1 New rule: l17 -> l9 : __const_100^0'=__const_100^0, __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 size17^post26 = size17^0 propagated equality tmp___0^post26 = tmp___0^0 propagated equality ret_my_malloc14^post26 = ret_my_malloc14^0 propagated equality size7^post26 = size7^0 propagated equality tmp^post26 = tmp^0 propagated equality tmp9^post26 = tmp9^0 propagated equality tmp___1^post26 = tmp___1^0 propagated equality __const_100^post26 = __const_100^0 propagated equality tmp13^post26 = tmp13^0 propagated equality ret_my_malloc10^post26 = ret_my_malloc10^0 propagated equality __len21^post26 = __len21^0 propagated equality size15^post26 = size15^0 propagated equality tmp22^post26 = tmp22^0 propagated equality retval^post26 = retval^0 propagated equality size11^post26 = size11^0 Simplified Guard Original rule: l17 -> l9 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^post27, __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, (-tmp___1^post27+tmp___1^0 == 0 /\ -size7^post27+size7^0 == 0 /\ -size11^post27+size11^0 == 0 /\ size15^0-size15^post27 == 0 /\ -tmp9^post27+tmp9^0 == 0 /\ -tmp13^post27+tmp13^0 == 0 /\ -__const_100^post27+__const_100^0 == 0 /\ -ret_my_malloc10^post27+ret_my_malloc10^0 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post27 == 0 /\ tmp^0-tmp^post27 == 0 /\ tmp22^0-tmp22^post27 == 0 /\ retval^0 <= 0 /\ __len21^0-__len21^post27 == 0 /\ size17^0-size17^post27 == 0 /\ retval^0-retval^post27 == 0 /\ tmp___0^0-tmp___0^post27 == 0), cost: 1 New rule: l17 -> l9 : __const_100^0'=__const_100^0, __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___1^post27 = tmp___1^0 propagated equality size7^post27 = size7^0 propagated equality size11^post27 = size11^0 propagated equality size15^post27 = size15^0 propagated equality tmp9^post27 = tmp9^0 propagated equality tmp13^post27 = tmp13^0 propagated equality __const_100^post27 = __const_100^0 propagated equality ret_my_malloc10^post27 = ret_my_malloc10^0 propagated equality ret_my_malloc14^post27 = ret_my_malloc14^0 propagated equality tmp^post27 = tmp^0 propagated equality tmp22^post27 = tmp22^0 propagated equality __len21^post27 = __len21^0 propagated equality size17^post27 = size17^0 propagated equality retval^post27 = retval^0 propagated equality tmp___0^post27 = tmp___0^0 Simplified Guard Original rule: l17 -> l9 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^post28, __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 /\ size7^0-size7^post28 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post28 == 0 /\ -retval^post28+retval^0 == 0 /\ -tmp___1^post28+tmp___1^0 == 0 /\ -__const_100^post28+__const_100^0 == 0 /\ size11^post28-__const_100^0 == 0 /\ __len21^0-__len21^post28 == 0 /\ -tmp9^post28+tmp9^0 == 0 /\ -ret_my_malloc10^post28+ret_my_malloc10^0 == 0 /\ 1-retval^0 <= 0 /\ -1+retval^0 <= 0 /\ tmp^0-tmp^post28 == 0 /\ size15^0-size15^post28 == 0 /\ tmp22^0-tmp22^post28 == 0 /\ tmp___0^0-tmp___0^post28 == 0 /\ -size17^post28+size17^0 == 0), cost: 1 New rule: l17 -> l16 : __const_100^0'=__const_100^post28, __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 /\ size7^0-size7^post28 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post28 == 0 /\ -retval^post28+retval^0 == 0 /\ -tmp___1^post28+tmp___1^0 == 0 /\ -__const_100^post28+__const_100^0 == 0 /\ size11^post28-__const_100^0 == 0 /\ __len21^0-__len21^post28 == 0 /\ -tmp9^post28+tmp9^0 == 0 /\ -ret_my_malloc10^post28+ret_my_malloc10^0 == 0 /\ 1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0 /\ tmp^0-tmp^post28 == 0 /\ size15^0-size15^post28 == 0 /\ tmp22^0-tmp22^post28 == 0 /\ tmp___0^0-tmp___0^post28 == 0 /\ -size17^post28+size17^0 == 0), cost: 1 Propagated Equalities Original rule: l17 -> l16 : __const_100^0'=__const_100^post28, __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 /\ size7^0-size7^post28 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post28 == 0 /\ -retval^post28+retval^0 == 0 /\ -tmp___1^post28+tmp___1^0 == 0 /\ -__const_100^post28+__const_100^0 == 0 /\ size11^post28-__const_100^0 == 0 /\ __len21^0-__len21^post28 == 0 /\ -tmp9^post28+tmp9^0 == 0 /\ -ret_my_malloc10^post28+ret_my_malloc10^0 == 0 /\ 1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0 /\ tmp^0-tmp^post28 == 0 /\ size15^0-size15^post28 == 0 /\ tmp22^0-tmp22^post28 == 0 /\ tmp___0^0-tmp___0^post28 == 0 /\ -size17^post28+size17^0 == 0), cost: 1 New rule: l17 -> l16 : __const_100^0'=__const_100^0, __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'=__const_100^0, 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 size7^post28 = size7^0 propagated equality ret_my_malloc14^post28 = ret_my_malloc14^0 propagated equality retval^post28 = retval^0 propagated equality tmp___1^post28 = tmp___1^0 propagated equality __const_100^post28 = __const_100^0 propagated equality size11^post28 = __const_100^0 propagated equality __len21^post28 = __len21^0 propagated equality tmp9^post28 = tmp9^0 propagated equality ret_my_malloc10^post28 = ret_my_malloc10^0 propagated equality tmp^post28 = tmp^0 propagated equality size15^post28 = size15^0 propagated equality tmp22^post28 = tmp22^0 propagated equality tmp___0^post28 = tmp___0^0 propagated equality size17^post28 = size17^0 Simplified Guard Original rule: l17 -> l16 : __const_100^0'=__const_100^0, __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'=__const_100^0, 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 : __const_100^0'=__const_100^0, __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'=__const_100^0, 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 : __const_100^0'=__const_100^0, __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'=__const_100^0, 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 : __const_100^0'=__const_100^0, __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'=__const_100^0, 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 : __const_100^0'=__const_100^0, __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'=__const_100^0, 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'=__const_100^0, tmp13^0'=tmp13^post28, (1-retval^0 <= 0 /\ 1-retval^0 == 0 /\ -1+retval^0 <= 0), cost: 1 Propagated Equalities Original rule: l1 -> l17 : __const_100^0'=__const_100^post29, __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_malloc10^0-ret_my_malloc10^post29 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post29 == 0 /\ -tmp___0^post29+tmp___0^0 == 0 /\ tmp___1^0-tmp___1^post29 == 0 /\ -__const_100^post29+__const_100^0 == 0 /\ tmp22^0-tmp22^post29 == 0 /\ size15^0-size15^post29 == 0 /\ __len21^0-__len21^post29 == 0 /\ -tmp9^post29+tmp9^0 == 0 /\ size7^0-size7^post29 == 0 /\ size11^0-size11^post29 == 0 /\ -size17^post29+size17^0 == 0 /\ -tmp13^post29+tmp13^0 == 0 /\ -tmp^post29+retval^post29 == 0 /\ tmp^post29-ret_my_malloc10^0 == 0), cost: 1 New rule: l1 -> l17 : __const_100^0'=__const_100^0, __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_malloc10^post29 = ret_my_malloc10^0 propagated equality ret_my_malloc14^post29 = ret_my_malloc14^0 propagated equality tmp___0^post29 = tmp___0^0 propagated equality tmp___1^post29 = tmp___1^0 propagated equality __const_100^post29 = __const_100^0 propagated equality tmp22^post29 = tmp22^0 propagated equality size15^post29 = size15^0 propagated equality __len21^post29 = __len21^0 propagated equality tmp9^post29 = tmp9^0 propagated equality size7^post29 = size7^0 propagated equality size11^post29 = size11^0 propagated equality size17^post29 = size17^0 propagated equality tmp13^post29 = tmp13^0 propagated equality retval^post29 = tmp^post29 propagated equality tmp^post29 = ret_my_malloc10^0 Simplified Guard Original rule: l1 -> l17 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^0, __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 : __const_100^0'=__const_100^post30, __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 /\ -size11^post31+size11^0 == 0 /\ tmp22^0-tmp22^post31 == 0 /\ -__const_100^post30+__const_100^post31 == 0 /\ ret_my_malloc10^post31-ret_my_malloc10^post30 == 0 /\ tmp13^post31-tmp13^post30 == 0 /\ size15^0-size15^post31 == 0 /\ -ret_my_malloc14^post30+ret_my_malloc14^post31 == 0 /\ -tmp___1^post31+tmp___1^0 == 0 /\ -__const_100^post31+__const_100^0 == 0 /\ size7^post30-__const_100^post31 == 0 /\ -ret_my_malloc10^post31+ret_my_malloc10^0 == 0 /\ -__len21^post30+__len21^post31 == 0 /\ -tmp22^post30+tmp22^post31 == 0 /\ -size7^post31+size7^0 == 0 /\ -retval^post30+retval^post31 == 0 /\ size15^post31-size15^post30 == 0 /\ -size17^post30+size17^post31 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post31 == 0 /\ tmp___1^post31-tmp___1^post30 == 0 /\ tmp^0-tmp^post31 == 0 /\ -tmp___0^post30+tmp___0^post31 == 0 /\ tmp^post31-tmp^post30 == 0 /\ size17^0-size17^post31 == 0 /\ -tmp9^post31+tmp9^0 == 0 /\ -tmp13^post31+tmp13^0 == 0 /\ tmp___0^0-tmp___0^post31 == 0 /\ __len21^0-__len21^post31 == 0 /\ size11^post31-size11^post30 == 0 /\ retval^0-retval^post31 == 0), cost: 1 New rule: l19 -> l0 : __const_100^0'=__const_100^post31, __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'=__const_100^post31, 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 /\ -size11^post31+size11^0 == 0 /\ tmp22^0-tmp22^post31 == 0 /\ size15^0-size15^post31 == 0 /\ -tmp___1^post31+tmp___1^0 == 0 /\ -__const_100^post31+__const_100^0 == 0 /\ -ret_my_malloc10^post31+ret_my_malloc10^0 == 0 /\ -size7^post31+size7^0 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post31 == 0 /\ tmp^0-tmp^post31 == 0 /\ size17^0-size17^post31 == 0 /\ -tmp9^post31+tmp9^0 == 0 /\ -tmp13^post31+tmp13^0 == 0 /\ tmp___0^0-tmp___0^post31 == 0 /\ __len21^0-__len21^post31 == 0 /\ retval^0-retval^post31 == 0), cost: 1 propagated equality __const_100^post30 = __const_100^post31 propagated equality ret_my_malloc10^post30 = ret_my_malloc10^post31 propagated equality tmp13^post30 = tmp13^post31 propagated equality ret_my_malloc14^post30 = ret_my_malloc14^post31 propagated equality size7^post30 = __const_100^post31 propagated equality __len21^post30 = __len21^post31 propagated equality tmp22^post30 = tmp22^post31 propagated equality retval^post30 = retval^post31 propagated equality size15^post30 = size15^post31 propagated equality size17^post30 = size17^post31 propagated equality tmp___1^post30 = tmp___1^post31 propagated equality tmp___0^post30 = tmp___0^post31 propagated equality tmp^post30 = tmp^post31 propagated equality size11^post30 = size11^post31 Propagated Equalities Original rule: l19 -> l0 : __const_100^0'=__const_100^post31, __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'=__const_100^post31, 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 /\ -size11^post31+size11^0 == 0 /\ tmp22^0-tmp22^post31 == 0 /\ size15^0-size15^post31 == 0 /\ -tmp___1^post31+tmp___1^0 == 0 /\ -__const_100^post31+__const_100^0 == 0 /\ -ret_my_malloc10^post31+ret_my_malloc10^0 == 0 /\ -size7^post31+size7^0 == 0 /\ ret_my_malloc14^0-ret_my_malloc14^post31 == 0 /\ tmp^0-tmp^post31 == 0 /\ size17^0-size17^post31 == 0 /\ -tmp9^post31+tmp9^0 == 0 /\ -tmp13^post31+tmp13^0 == 0 /\ tmp___0^0-tmp___0^post31 == 0 /\ __len21^0-__len21^post31 == 0 /\ retval^0-retval^post31 == 0), cost: 1 New rule: l19 -> l0 : __const_100^0'=__const_100^0, __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'=__const_100^0, 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 size11^post31 = size11^0 propagated equality tmp22^post31 = tmp22^0 propagated equality size15^post31 = size15^0 propagated equality tmp___1^post31 = tmp___1^0 propagated equality __const_100^post31 = __const_100^0 propagated equality ret_my_malloc10^post31 = ret_my_malloc10^0 propagated equality size7^post31 = size7^0 propagated equality ret_my_malloc14^post31 = ret_my_malloc14^0 propagated equality tmp^post31 = tmp^0 propagated equality size17^post31 = size17^0 propagated equality tmp9^post31 = tmp9^0 propagated equality tmp13^post31 = tmp13^0 propagated equality tmp___0^post31 = tmp___0^0 propagated equality __len21^post31 = __len21^0 propagated equality retval^post31 = retval^0 Simplified Guard Original rule: l19 -> l0 : __const_100^0'=__const_100^0, __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'=__const_100^0, 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 : __const_100^0'=__const_100^0, __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'=__const_100^0, 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 : __const_100^0'=__const_100^0, __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'=__const_100^0, 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'=__const_100^0, 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