unknown Initial ITS Start location: l13 Program variables: __const_10^0 a10^0 a15^0 b11^0 b16^0 c12^0 c17^0 m13^0 ret_max24^0 ret_min14^0 tmp620^0 tmp923^0 tmp9^0 tmp^0 tmp___0^0 tmp___1^0 x_promoted_1^0 y_promoted_2^0 z^0 0: l0 -> l1 : __const_10^0'=__const_10^post1, a10^0'=a10^post1, a15^0'=a15^post1, b11^0'=b11^post1, b16^0'=b16^post1, c12^0'=c12^post1, c17^0'=c17^post1, m13^0'=m13^post1, ret_max24^0'=ret_max24^post1, ret_min14^0'=ret_min14^post1, tmp620^0'=tmp620^post1, tmp923^0'=tmp923^post1, tmp9^0'=tmp9^post1, tmp^0'=tmp^post1, tmp___0^0'=tmp___0^post1, tmp___1^0'=tmp___1^post1, x_promoted_1^0'=x_promoted_1^post1, y_promoted_2^0'=y_promoted_2^post1, z^0'=z^post1, (b16^0-b16^post1 == 0 /\ -tmp___1^post1+tmp___1^0 == 0 /\ -y_promoted_2^post1+y_promoted_2^0 == 0 /\ -z^post1+z^0 == 0 /\ b11^0-b11^post1 == 0 /\ ret_min14^0-ret_min14^post1 == 0 /\ -tmp___0^post1+tmp___0^0 == 0 /\ -ret_max24^post1+ret_max24^0 == 0 /\ -tmp923^post1+tmp923^0 == 0 /\ c17^0-c17^post1 == 0 /\ -a10^post1+a10^0 == 0 /\ -tmp^post1+tmp^0 == 0 /\ -a15^post1+a15^0 == 0 /\ -c12^post1+c12^0 == 0 /\ __const_10^0-__const_10^post1 == 0 /\ tmp9^0-tmp9^post1 == 0 /\ x_promoted_1^0-x_promoted_1^post1 == 0 /\ tmp620^0-tmp620^post1 == 0 /\ m13^0-m13^post1 == 0), cost: 1 1: l2 -> l3 : __const_10^0'=__const_10^post2, a10^0'=a10^post2, a15^0'=a15^post2, b11^0'=b11^post2, b16^0'=b16^post2, c12^0'=c12^post2, c17^0'=c17^post2, m13^0'=m13^post2, ret_max24^0'=ret_max24^post2, ret_min14^0'=ret_min14^post2, tmp620^0'=tmp620^post2, tmp923^0'=tmp923^post2, tmp9^0'=tmp9^post2, tmp^0'=tmp^post2, tmp___0^0'=tmp___0^post2, tmp___1^0'=tmp___1^post2, x_promoted_1^0'=x_promoted_1^post2, y_promoted_2^0'=y_promoted_2^post2, z^0'=z^post2, (0 == 0 /\ tmp___0^post2-ret_max24^post2 == 0 /\ c17^0-c17^post2 == 0 /\ y_promoted_2^0-y_promoted_2^post2 == 0 /\ -tmp923^post2+tmp923^0 == 0 /\ m13^0-m13^post2 == 0 /\ -tmp___1^post2+tmp___1^0 == 0 /\ b16^0-b16^post2 == 0 /\ -tmp620^post2+tmp620^0 == 0 /\ b11^0-b11^post2 == 0 /\ __const_10^0-__const_10^post2 == 0 /\ x_promoted_1^0-x_promoted_1^post2 == 0 /\ ret_min14^0-ret_min14^post2 == 0 /\ ret_max24^post2-a15^0 == 0 /\ -a15^post2+a15^0 == 0 /\ -a10^post2+a10^0 == 0 /\ tmp9^0-tmp9^post2 == 0 /\ -tmp^post2+tmp^0 == 0 /\ -c12^post2+c12^0 == 0), cost: 1 17: l3 -> l0 : __const_10^0'=__const_10^post18, a10^0'=a10^post18, a15^0'=a15^post18, b11^0'=b11^post18, b16^0'=b16^post18, c12^0'=c12^post18, c17^0'=c17^post18, m13^0'=m13^post18, ret_max24^0'=ret_max24^post18, ret_min14^0'=ret_min14^post18, tmp620^0'=tmp620^post18, tmp923^0'=tmp923^post18, tmp9^0'=tmp9^post18, tmp^0'=tmp^post18, tmp___0^0'=tmp___0^post18, tmp___1^0'=tmp___1^post18, x_promoted_1^0'=x_promoted_1^post18, y_promoted_2^0'=y_promoted_2^post18, z^0'=z^post18, (c17^0-c17^post18 == 0 /\ -ret_max24^post18+ret_max24^0 == 0 /\ 1-y_promoted_2^0+z^0 <= 0 /\ -x_promoted_1^post18+x_promoted_1^0 == 0 /\ -c12^post18+c12^0 == 0 /\ -z^post18+z^0 == 0 /\ tmp9^0-tmp9^post18 == 0 /\ -b11^post18+b11^0 == 0 /\ __const_10^0-__const_10^post18 == 0 /\ -y_promoted_2^0+tmp___1^post18+z^0 == 0 /\ -tmp___0^post18+tmp___0^0 == 0 /\ b16^0-b16^post18 == 0 /\ y_promoted_2^0-y_promoted_2^post18 == 0 /\ -tmp923^post18+tmp923^0 == 0 /\ m13^0-m13^post18 == 0 /\ -a15^post18+a15^0 == 0 /\ -tmp620^post18+tmp620^0 == 0 /\ ret_min14^0-ret_min14^post18 == 0 /\ -tmp^post18+tmp^0 == 0 /\ a10^0-a10^post18 == 0), cost: 1 18: l3 -> l0 : __const_10^0'=__const_10^post19, a10^0'=a10^post19, a15^0'=a15^post19, b11^0'=b11^post19, b16^0'=b16^post19, c12^0'=c12^post19, c17^0'=c17^post19, m13^0'=m13^post19, ret_max24^0'=ret_max24^post19, ret_min14^0'=ret_min14^post19, tmp620^0'=tmp620^post19, tmp923^0'=tmp923^post19, tmp9^0'=tmp9^post19, tmp^0'=tmp^post19, tmp___0^0'=tmp___0^post19, tmp___1^0'=tmp___1^post19, x_promoted_1^0'=x_promoted_1^post19, y_promoted_2^0'=y_promoted_2^post19, z^0'=z^post19, (ret_max24^0-ret_max24^post19 == 0 /\ a15^0-a15^post19 == 0 /\ -__const_10^post19+__const_10^0 == 0 /\ -y_promoted_2^0-z^0+tmp___1^post19 == 0 /\ -tmp9^post19+tmp9^0 == 0 /\ y_promoted_2^0-z^0 <= 0 /\ -tmp923^post19+tmp923^0 == 0 /\ -x_promoted_1^post19+x_promoted_1^0 == 0 /\ -c17^post19+c17^0 == 0 /\ a10^0-a10^post19 == 0 /\ -tmp620^post19+tmp620^0 == 0 /\ y_promoted_2^0-y_promoted_2^post19 == 0 /\ -tmp^post19+tmp^0 == 0 /\ z^0-z^post19 == 0 /\ c12^0-c12^post19 == 0 /\ -ret_min14^post19+ret_min14^0 == 0 /\ -b11^post19+b11^0 == 0 /\ tmp___0^0-tmp___0^post19 == 0 /\ b16^0-b16^post19 == 0 /\ m13^0-m13^post19 == 0), cost: 1 2: l4 -> l5 : __const_10^0'=__const_10^post3, a10^0'=a10^post3, a15^0'=a15^post3, b11^0'=b11^post3, b16^0'=b16^post3, c12^0'=c12^post3, c17^0'=c17^post3, m13^0'=m13^post3, ret_max24^0'=ret_max24^post3, ret_min14^0'=ret_min14^post3, tmp620^0'=tmp620^post3, tmp923^0'=tmp923^post3, tmp9^0'=tmp9^post3, tmp^0'=tmp^post3, tmp___0^0'=tmp___0^post3, tmp___1^0'=tmp___1^post3, x_promoted_1^0'=x_promoted_1^post3, y_promoted_2^0'=y_promoted_2^post3, z^0'=z^post3, (c17^0-c17^post3 == 0 /\ -tmp923^post3+tmp923^0 == 0 /\ -z^post3+z^0 == 0 /\ m13^0-m13^post3 == 0 /\ -__const_10^post3+__const_10^0 == 0 /\ -tmp___1^post3+tmp___1^0 == 0 /\ -a15^post3+a15^0 == 0 /\ b16^0-b16^post3 == 0 /\ -tmp620^post3+tmp620^0 == 0 /\ b11^0-b11^post3 == 0 /\ ret_min14^0-ret_min14^post3 == 0 /\ -tmp___0^post3+tmp___0^0 == 0 /\ -ret_max24^post3+ret_max24^0 == 0 /\ -y_promoted_2^post3+y_promoted_2^0 == 0 /\ 1+y_promoted_2^0-x_promoted_1^0 <= 0 /\ tmp9^0-tmp9^post3 == 0 /\ -tmp^post3+tmp^0 == 0 /\ a10^0-a10^post3 == 0 /\ -c12^post3+c12^0 == 0 /\ x_promoted_1^0-x_promoted_1^post3 == 0), cost: 1 3: l4 -> l3 : __const_10^0'=__const_10^post4, a10^0'=a10^post4, a15^0'=a15^post4, b11^0'=b11^post4, b16^0'=b16^post4, c12^0'=c12^post4, c17^0'=c17^post4, m13^0'=m13^post4, ret_max24^0'=ret_max24^post4, ret_min14^0'=ret_min14^post4, tmp620^0'=tmp620^post4, tmp923^0'=tmp923^post4, tmp9^0'=tmp9^post4, tmp^0'=tmp^post4, tmp___0^0'=tmp___0^post4, tmp___1^0'=tmp___1^post4, x_promoted_1^0'=x_promoted_1^post4, y_promoted_2^0'=y_promoted_2^post4, z^0'=z^post4, (0 == 0 /\ b11^0-b11^post4 == 0 /\ -tmp___0^post4+tmp___0^0 == 0 /\ ret_min14^0-ret_min14^post4 == 0 /\ -tmp923^post4+tmp923^0 == 0 /\ -ret_max24^post4+ret_max24^0 == 0 /\ __const_10^0-__const_10^post4 == 0 /\ -z^post4+z^0 == 0 /\ -a15^post4+a15^0 == 0 /\ -tmp^post4+tmp^0 == 0 /\ -b16^post4+b16^0 == 0 /\ tmp620^0-tmp620^post4 == 0 /\ -y_promoted_2^0+x_promoted_1^0 <= 0 /\ c17^0-c17^post4 == 0 /\ -tmp___1^post4+tmp___1^0 == 0 /\ -y_promoted_2^post4+y_promoted_2^0 == 0 /\ -a10^post4+a10^0 == 0 /\ -c12^post4+c12^0 == 0 /\ m13^0-m13^post4 == 0 /\ x_promoted_1^0-x_promoted_1^post4 == 0), cost: 1 15: l5 -> l7 : __const_10^0'=__const_10^post16, a10^0'=a10^post16, a15^0'=a15^post16, b11^0'=b11^post16, b16^0'=b16^post16, c12^0'=c12^post16, c17^0'=c17^post16, m13^0'=m13^post16, ret_max24^0'=ret_max24^post16, ret_min14^0'=ret_min14^post16, tmp620^0'=tmp620^post16, tmp923^0'=tmp923^post16, tmp9^0'=tmp9^post16, tmp^0'=tmp^post16, tmp___0^0'=tmp___0^post16, tmp___1^0'=tmp___1^post16, x_promoted_1^0'=x_promoted_1^post16, y_promoted_2^0'=y_promoted_2^post16, z^0'=z^post16, (-ret_min14^post16+ret_min14^0 == 0 /\ -x_promoted_1^post16+x_promoted_1^0 == 0 /\ c17^post16-x_promoted_1^0 == 0 /\ a10^0-a10^post16 == 0 /\ tmp___1^0-tmp___1^post16 == 0 /\ -y_promoted_2^0+b16^post16 == 0 /\ -tmp9^post16+tmp9^0 == 0 /\ -tmp923^post16+tmp923^0 == 0 /\ tmp___0^0-tmp___0^post16 == 0 /\ -b11^post16+b11^0 == 0 /\ -__const_10^post16+__const_10^0 == 0 /\ -ret_max24^post16+ret_max24^0 == 0 /\ z^0-z^post16 == 0 /\ 1-x_promoted_1^0+z^0 <= 0 /\ -tmp^post16+tmp^0 == 0 /\ -z^0+a15^post16 == 0 /\ m13^0-m13^post16 == 0 /\ -tmp620^post16+tmp620^0 == 0 /\ y_promoted_2^0-y_promoted_2^post16 == 0 /\ c12^0-c12^post16 == 0), cost: 1 16: l5 -> l11 : __const_10^0'=__const_10^post17, a10^0'=a10^post17, a15^0'=a15^post17, b11^0'=b11^post17, b16^0'=b16^post17, c12^0'=c12^post17, c17^0'=c17^post17, m13^0'=m13^post17, ret_max24^0'=ret_max24^post17, ret_min14^0'=ret_min14^post17, tmp620^0'=tmp620^post17, tmp923^0'=tmp923^post17, tmp9^0'=tmp9^post17, tmp^0'=tmp^post17, tmp___0^0'=tmp___0^post17, tmp___1^0'=tmp___1^post17, x_promoted_1^0'=x_promoted_1^post17, y_promoted_2^0'=y_promoted_2^post17, z^0'=z^post17, (-z^post17+z^0 == 0 /\ tmp___0^0-tmp___0^post17 == 0 /\ -ret_max24^post17+ret_max24^0 == 0 /\ tmp9^0-tmp9^post17 == 0 /\ c17^0-c17^post17 == 0 /\ -x_promoted_1^post17+x_promoted_1^0 == 0 /\ b16^0-b16^post17 == 0 /\ -tmp___1^post17+tmp___1^0 == 0 /\ -tmp^post17+tmp^0 == 0 /\ a10^post17-x_promoted_1^0 == 0 /\ y_promoted_2^0-y_promoted_2^post17 == 0 /\ m13^0-m13^post17 == 0 /\ -tmp923^post17+tmp923^0 == 0 /\ -__const_10^post17+__const_10^0 == 0 /\ b11^post17-y_promoted_2^0 == 0 /\ -a15^post17+a15^0 == 0 /\ -tmp620^post17+tmp620^0 == 0 /\ x_promoted_1^0-z^0 <= 0 /\ ret_min14^0-ret_min14^post17 == 0 /\ c12^post17-z^0 == 0), cost: 1 4: l6 -> l2 : __const_10^0'=__const_10^post5, a10^0'=a10^post5, a15^0'=a15^post5, b11^0'=b11^post5, b16^0'=b16^post5, c12^0'=c12^post5, c17^0'=c17^post5, m13^0'=m13^post5, ret_max24^0'=ret_max24^post5, ret_min14^0'=ret_min14^post5, tmp620^0'=tmp620^post5, tmp923^0'=tmp923^post5, tmp9^0'=tmp9^post5, tmp^0'=tmp^post5, tmp___0^0'=tmp___0^post5, tmp___1^0'=tmp___1^post5, x_promoted_1^0'=x_promoted_1^post5, y_promoted_2^0'=y_promoted_2^post5, z^0'=z^post5, (-x_promoted_1^post5+x_promoted_1^0 == 0 /\ -z^post5+z^0 == 0 /\ b11^0-b11^post5 == 0 /\ ret_min14^0-ret_min14^post5 == 0 /\ 1+c17^0-a15^0 <= 0 /\ -tmp___1^post5+tmp___1^0 == 0 /\ tmp9^0-tmp9^post5 == 0 /\ __const_10^0-__const_10^post5 == 0 /\ -tmp___0^post5+tmp___0^0 == 0 /\ y_promoted_2^0-y_promoted_2^post5 == 0 /\ -b16^post5+b16^0 == 0 /\ -tmp923^post5+tmp923^0 == 0 /\ -a15^post5+a15^0 == 0 /\ -c12^post5+c12^0 == 0 /\ -ret_max24^post5+ret_max24^0 == 0 /\ -tmp^post5+tmp^0 == 0 /\ -tmp620^post5+tmp620^0 == 0 /\ m13^0-m13^post5 == 0 /\ c17^0-c17^post5 == 0 /\ -a10^post5+a10^0 == 0), cost: 1 5: l6 -> l2 : __const_10^0'=__const_10^post6, a10^0'=a10^post6, a15^0'=a15^post6, b11^0'=b11^post6, b16^0'=b16^post6, c12^0'=c12^post6, c17^0'=c17^post6, m13^0'=m13^post6, ret_max24^0'=ret_max24^post6, ret_min14^0'=ret_min14^post6, tmp620^0'=tmp620^post6, tmp923^0'=tmp923^post6, tmp9^0'=tmp9^post6, tmp^0'=tmp^post6, tmp___0^0'=tmp___0^post6, tmp___1^0'=tmp___1^post6, x_promoted_1^0'=x_promoted_1^post6, y_promoted_2^0'=y_promoted_2^post6, z^0'=z^post6, (0 == 0 /\ -tmp___1^post6+tmp___1^0 == 0 /\ -x_promoted_1^post6+x_promoted_1^0 == 0 /\ -z^post6+z^0 == 0 /\ __const_10^0-__const_10^post6 == 0 /\ tmp9^0-tmp9^post6 == 0 /\ c17^0-c17^post6 == 0 /\ -tmp___0^post6+tmp___0^0 == 0 /\ -ret_max24^post6+ret_max24^0 == 0 /\ -c17^0+a15^0 <= 0 /\ m13^0-m13^post6 == 0 /\ y_promoted_2^0-y_promoted_2^post6 == 0 /\ b16^0-b16^post6 == 0 /\ -a10^post6+a10^0 == 0 /\ -a15^post6+a15^0 == 0 /\ -tmp^post6+tmp^0 == 0 /\ b11^0-b11^post6 == 0 /\ -c12^post6+c12^0 == 0 /\ ret_min14^0-ret_min14^post6 == 0 /\ -tmp620^post6+tmp620^0 == 0), cost: 1 6: l7 -> l6 : __const_10^0'=__const_10^post7, a10^0'=a10^post7, a15^0'=a15^post7, b11^0'=b11^post7, b16^0'=b16^post7, c12^0'=c12^post7, c17^0'=c17^post7, m13^0'=m13^post7, ret_max24^0'=ret_max24^post7, ret_min14^0'=ret_min14^post7, tmp620^0'=tmp620^post7, tmp923^0'=tmp923^post7, tmp9^0'=tmp9^post7, tmp^0'=tmp^post7, tmp___0^0'=tmp___0^post7, tmp___1^0'=tmp___1^post7, x_promoted_1^0'=x_promoted_1^post7, y_promoted_2^0'=y_promoted_2^post7, z^0'=z^post7, (-ret_max24^post7+ret_max24^0 == 0 /\ -m13^post7+m13^0 == 0 /\ -y_promoted_2^post7+y_promoted_2^0 == 0 /\ __const_10^0-__const_10^post7 == 0 /\ -tmp___1^post7+tmp___1^0 == 0 /\ -c12^post7+c12^0 == 0 /\ -z^post7+z^0 == 0 /\ 1+b16^0-a15^0 <= 0 /\ ret_min14^0-ret_min14^post7 == 0 /\ -b16^post7+b16^0 == 0 /\ -tmp___0^post7+tmp___0^0 == 0 /\ -tmp923^post7+tmp923^0 == 0 /\ c17^0-c17^post7 == 0 /\ tmp9^0-tmp9^post7 == 0 /\ -tmp^post7+tmp^0 == 0 /\ -a15^post7+a15^0 == 0 /\ b11^0-b11^post7 == 0 /\ -a10^post7+a10^0 == 0 /\ x_promoted_1^0-x_promoted_1^post7 == 0 /\ tmp620^0-tmp620^post7 == 0), cost: 1 7: l7 -> l6 : __const_10^0'=__const_10^post8, a10^0'=a10^post8, a15^0'=a15^post8, b11^0'=b11^post8, b16^0'=b16^post8, c12^0'=c12^post8, c17^0'=c17^post8, m13^0'=m13^post8, ret_max24^0'=ret_max24^post8, ret_min14^0'=ret_min14^post8, tmp620^0'=tmp620^post8, tmp923^0'=tmp923^post8, tmp9^0'=tmp9^post8, tmp^0'=tmp^post8, tmp___0^0'=tmp___0^post8, tmp___1^0'=tmp___1^post8, x_promoted_1^0'=x_promoted_1^post8, y_promoted_2^0'=y_promoted_2^post8, z^0'=z^post8, (0 == 0 /\ y_promoted_2^0-y_promoted_2^post8 == 0 /\ -tmp___1^post8+tmp___1^0 == 0 /\ -a15^post8+a15^0 == 0 /\ ret_min14^0-ret_min14^post8 == 0 /\ -a10^post8+a10^0 == 0 /\ -b16^post8+b16^0 == 0 /\ -z^post8+z^0 == 0 /\ -ret_max24^post8+ret_max24^0 == 0 /\ -tmp923^post8+tmp923^0 == 0 /\ -tmp___0^post8+tmp___0^0 == 0 /\ -b16^0+a15^0 <= 0 /\ -tmp^post8+tmp^0 == 0 /\ __const_10^0-__const_10^post8 == 0 /\ c17^0-c17^post8 == 0 /\ tmp9^0-tmp9^post8 == 0 /\ x_promoted_1^0-x_promoted_1^post8 == 0 /\ -c12^post8+c12^0 == 0 /\ m13^0-m13^post8 == 0 /\ b11^0-b11^post8 == 0), cost: 1 8: l8 -> l9 : __const_10^0'=__const_10^post9, a10^0'=a10^post9, a15^0'=a15^post9, b11^0'=b11^post9, b16^0'=b16^post9, c12^0'=c12^post9, c17^0'=c17^post9, m13^0'=m13^post9, ret_max24^0'=ret_max24^post9, ret_min14^0'=ret_min14^post9, tmp620^0'=tmp620^post9, tmp923^0'=tmp923^post9, tmp9^0'=tmp9^post9, tmp^0'=tmp^post9, tmp___0^0'=tmp___0^post9, tmp___1^0'=tmp___1^post9, x_promoted_1^0'=x_promoted_1^post9, y_promoted_2^0'=y_promoted_2^post9, z^0'=z^post9, (y_promoted_2^0-y_promoted_2^post9 == 0 /\ m13^post9-c12^0 == 0 /\ c17^0-c17^post9 == 0 /\ tmp___0^0-tmp___0^post9 == 0 /\ -tmp923^post9+tmp923^0 == 0 /\ -ret_max24^post9+ret_max24^0 == 0 /\ -z^post9+z^0 == 0 /\ -x_promoted_1^post9+x_promoted_1^0 == 0 /\ -a15^post9+a15^0 == 0 /\ -__const_10^post9+__const_10^0 == 0 /\ -tmp620^post9+tmp620^0 == 0 /\ b16^0-b16^post9 == 0 /\ b11^0-b11^post9 == 0 /\ ret_min14^0-ret_min14^post9 == 0 /\ 1-b11^0+c12^0 <= 0 /\ tmp9^0-tmp9^post9 == 0 /\ -tmp___1^post9+tmp___1^0 == 0 /\ a10^0-a10^post9 == 0 /\ -c12^post9+c12^0 == 0 /\ -tmp^post9+tmp^0 == 0), cost: 1 9: l8 -> l9 : __const_10^0'=__const_10^post10, a10^0'=a10^post10, a15^0'=a15^post10, b11^0'=b11^post10, b16^0'=b16^post10, c12^0'=c12^post10, c17^0'=c17^post10, m13^0'=m13^post10, ret_max24^0'=ret_max24^post10, ret_min14^0'=ret_min14^post10, tmp620^0'=tmp620^post10, tmp923^0'=tmp923^post10, tmp9^0'=tmp9^post10, tmp^0'=tmp^post10, tmp___0^0'=tmp___0^post10, tmp___1^0'=tmp___1^post10, x_promoted_1^0'=x_promoted_1^post10, y_promoted_2^0'=y_promoted_2^post10, z^0'=z^post10, (-tmp___0^post10+tmp___0^0 == 0 /\ c17^0-c17^post10 == 0 /\ -tmp620^post10+tmp620^0 == 0 /\ -tmp^post10+tmp^0 == 0 /\ -z^post10+z^0 == 0 /\ -a15^post10+a15^0 == 0 /\ b16^0-b16^post10 == 0 /\ -__const_10^post10+__const_10^0 == 0 /\ ret_min14^0-ret_min14^post10 == 0 /\ tmp9^0-tmp9^post10 == 0 /\ b11^0-b11^post10 == 0 /\ -c12^post10+c12^0 == 0 /\ -ret_max24^post10+ret_max24^0 == 0 /\ -tmp923^post10+tmp923^0 == 0 /\ m13^post10-b11^0 == 0 /\ -tmp___1^post10+tmp___1^0 == 0 /\ -y_promoted_2^post10+y_promoted_2^0 == 0 /\ x_promoted_1^0-x_promoted_1^post10 == 0 /\ a10^0-a10^post10 == 0 /\ b11^0-c12^0 <= 0), cost: 1 10: l9 -> l3 : __const_10^0'=__const_10^post11, a10^0'=a10^post11, a15^0'=a15^post11, b11^0'=b11^post11, b16^0'=b16^post11, c12^0'=c12^post11, c17^0'=c17^post11, m13^0'=m13^post11, ret_max24^0'=ret_max24^post11, ret_min14^0'=ret_min14^post11, tmp620^0'=tmp620^post11, tmp923^0'=tmp923^post11, tmp9^0'=tmp9^post11, tmp^0'=tmp^post11, tmp___0^0'=tmp___0^post11, tmp___1^0'=tmp___1^post11, x_promoted_1^0'=x_promoted_1^post11, y_promoted_2^0'=y_promoted_2^post11, z^0'=z^post11, (b11^0-b11^post11 == 0 /\ -m13^0+ret_min14^post11 == 0 /\ -tmp___0^post11+tmp___0^0 == 0 /\ -ret_max24^post11+ret_max24^0 == 0 /\ -ret_min14^post11+tmp^post11 == 0 /\ __const_10^0-__const_10^post11 == 0 /\ -b16^post11+b16^0 == 0 /\ -a15^post11+a15^0 == 0 /\ -z^post11+z^0 == 0 /\ -x_promoted_1^0+x_promoted_1^post11-tmp^post11 == 0 /\ tmp9^0-tmp9^post11 == 0 /\ c17^0-c17^post11 == 0 /\ -tmp923^post11+tmp923^0 == 0 /\ tmp620^0-tmp620^post11 == 0 /\ -tmp___1^post11+tmp___1^0 == 0 /\ m13^0-m13^post11 == 0 /\ -c12^post11+c12^0 == 0 /\ -a10^post11+a10^0 == 0 /\ -y_promoted_2^post11+y_promoted_2^0 == 0), cost: 1 11: l10 -> l9 : __const_10^0'=__const_10^post12, a10^0'=a10^post12, a15^0'=a15^post12, b11^0'=b11^post12, b16^0'=b16^post12, c12^0'=c12^post12, c17^0'=c17^post12, m13^0'=m13^post12, ret_max24^0'=ret_max24^post12, ret_min14^0'=ret_min14^post12, tmp620^0'=tmp620^post12, tmp923^0'=tmp923^post12, tmp9^0'=tmp9^post12, tmp^0'=tmp^post12, tmp___0^0'=tmp___0^post12, tmp___1^0'=tmp___1^post12, x_promoted_1^0'=x_promoted_1^post12, y_promoted_2^0'=y_promoted_2^post12, z^0'=z^post12, (m13^post12-c12^0 == 0 /\ ret_max24^0-ret_max24^post12 == 0 /\ b16^0-b16^post12 == 0 /\ b11^0-b11^post12 == 0 /\ -x_promoted_1^post12+x_promoted_1^0 == 0 /\ tmp___1^0-tmp___1^post12 == 0 /\ -c17^post12+c17^0 == 0 /\ __const_10^0-__const_10^post12 == 0 /\ -tmp9^post12+tmp9^0 == 0 /\ -tmp923^post12+tmp923^0 == 0 /\ -tmp^post12+tmp^0 == 0 /\ -a15^post12+a15^0 == 0 /\ -tmp620^post12+tmp620^0 == 0 /\ 1-a10^0+c12^0 <= 0 /\ tmp___0^0-tmp___0^post12 == 0 /\ -ret_min14^post12+ret_min14^0 == 0 /\ y_promoted_2^0-y_promoted_2^post12 == 0 /\ c12^0-c12^post12 == 0 /\ -a10^post12+a10^0 == 0 /\ z^0-z^post12 == 0), cost: 1 12: l10 -> l9 : __const_10^0'=__const_10^post13, a10^0'=a10^post13, a15^0'=a15^post13, b11^0'=b11^post13, b16^0'=b16^post13, c12^0'=c12^post13, c17^0'=c17^post13, m13^0'=m13^post13, ret_max24^0'=ret_max24^post13, ret_min14^0'=ret_min14^post13, tmp620^0'=tmp620^post13, tmp923^0'=tmp923^post13, tmp9^0'=tmp9^post13, tmp^0'=tmp^post13, tmp___0^0'=tmp___0^post13, tmp___1^0'=tmp___1^post13, x_promoted_1^0'=x_promoted_1^post13, y_promoted_2^0'=y_promoted_2^post13, z^0'=z^post13, (ret_max24^0-ret_max24^post13 == 0 /\ a15^0-a15^post13 == 0 /\ -tmp923^post13+tmp923^0 == 0 /\ -z^post13+z^0 == 0 /\ tmp9^0-tmp9^post13 == 0 /\ -c17^post13+c17^0 == 0 /\ -tmp___1^post13+tmp___1^0 == 0 /\ -tmp620^post13+tmp620^0 == 0 /\ a10^0-a10^post13 == 0 /\ c12^0-c12^post13 == 0 /\ y_promoted_2^0-y_promoted_2^post13 == 0 /\ -__const_10^post13+__const_10^0 == 0 /\ -x_promoted_1^post13+x_promoted_1^0 == 0 /\ a10^0-c12^0 <= 0 /\ -ret_min14^post13+ret_min14^0 == 0 /\ tmp___0^0-tmp___0^post13 == 0 /\ -a10^0+m13^post13 == 0 /\ -tmp^post13+tmp^0 == 0 /\ -b11^post13+b11^0 == 0 /\ b16^0-b16^post13 == 0), cost: 1 13: l11 -> l8 : __const_10^0'=__const_10^post14, a10^0'=a10^post14, a15^0'=a15^post14, b11^0'=b11^post14, b16^0'=b16^post14, c12^0'=c12^post14, c17^0'=c17^post14, m13^0'=m13^post14, ret_max24^0'=ret_max24^post14, ret_min14^0'=ret_min14^post14, tmp620^0'=tmp620^post14, tmp923^0'=tmp923^post14, tmp9^0'=tmp9^post14, tmp^0'=tmp^post14, tmp___0^0'=tmp___0^post14, tmp___1^0'=tmp___1^post14, x_promoted_1^0'=x_promoted_1^post14, y_promoted_2^0'=y_promoted_2^post14, z^0'=z^post14, (y_promoted_2^0-y_promoted_2^post14 == 0 /\ 1-a10^0+b11^0 <= 0 /\ c17^0-c17^post14 == 0 /\ tmp9^0-tmp9^post14 == 0 /\ -__const_10^post14+__const_10^0 == 0 /\ -ret_max24^post14+ret_max24^0 == 0 /\ -tmp923^post14+tmp923^0 == 0 /\ -z^post14+z^0 == 0 /\ -x_promoted_1^post14+x_promoted_1^0 == 0 /\ -a15^post14+a15^0 == 0 /\ m13^0-m13^post14 == 0 /\ b16^0-b16^post14 == 0 /\ -tmp___0^post14+tmp___0^0 == 0 /\ -tmp620^post14+tmp620^0 == 0 /\ b11^0-b11^post14 == 0 /\ -tmp^post14+tmp^0 == 0 /\ ret_min14^0-ret_min14^post14 == 0 /\ -c12^post14+c12^0 == 0 /\ -tmp___1^post14+tmp___1^0 == 0 /\ a10^0-a10^post14 == 0), cost: 1 14: l11 -> l10 : __const_10^0'=__const_10^post15, a10^0'=a10^post15, a15^0'=a15^post15, b11^0'=b11^post15, b16^0'=b16^post15, c12^0'=c12^post15, c17^0'=c17^post15, m13^0'=m13^post15, ret_max24^0'=ret_max24^post15, ret_min14^0'=ret_min14^post15, tmp620^0'=tmp620^post15, tmp923^0'=tmp923^post15, tmp9^0'=tmp9^post15, tmp^0'=tmp^post15, tmp___0^0'=tmp___0^post15, tmp___1^0'=tmp___1^post15, x_promoted_1^0'=x_promoted_1^post15, y_promoted_2^0'=y_promoted_2^post15, z^0'=z^post15, (-x_promoted_1^post15+x_promoted_1^0 == 0 /\ -tmp9^post15+tmp9^0 == 0 /\ c17^0-c17^post15 == 0 /\ -tmp923^post15+tmp923^0 == 0 /\ -tmp^post15+tmp^0 == 0 /\ a10^0-b11^0 <= 0 /\ -__const_10^post15+__const_10^0 == 0 /\ -ret_max24^post15+ret_max24^0 == 0 /\ -a15^post15+a15^0 == 0 /\ m13^0-m13^post15 == 0 /\ -tmp620^post15+tmp620^0 == 0 /\ b16^0-b16^post15 == 0 /\ z^0-z^post15 == 0 /\ b11^0-b11^post15 == 0 /\ ret_min14^0-ret_min14^post15 == 0 /\ tmp___0^0-tmp___0^post15 == 0 /\ -tmp___1^post15+tmp___1^0 == 0 /\ a10^0-a10^post15 == 0 /\ y_promoted_2^0-y_promoted_2^post15 == 0 /\ -c12^post15+c12^0 == 0), cost: 1 19: l12 -> l4 : __const_10^0'=__const_10^post20, a10^0'=a10^post20, a15^0'=a15^post20, b11^0'=b11^post20, b16^0'=b16^post20, c12^0'=c12^post20, c17^0'=c17^post20, m13^0'=m13^post20, ret_max24^0'=ret_max24^post20, ret_min14^0'=ret_min14^post20, tmp620^0'=tmp620^post20, tmp923^0'=tmp923^post20, tmp9^0'=tmp9^post20, tmp^0'=tmp^post20, tmp___0^0'=tmp___0^post20, tmp___1^0'=tmp___1^post20, x_promoted_1^0'=x_promoted_1^post20, y_promoted_2^0'=y_promoted_2^post20, z^0'=z^post20, (ret_max24^0-ret_max24^post20 == 0 /\ tmp___0^0-tmp___0^post20 == 0 /\ -2+y_promoted_2^post20 == 0 /\ -tmp923^post20+tmp923^0 == 0 /\ x_promoted_1^post20-__const_10^0 == 0 /\ tmp9^0-tmp9^post20 == 0 /\ -__const_10^post20+__const_10^0 == 0 /\ a10^0-a10^post20 == 0 /\ -c17^post20+c17^0 == 0 /\ -a15^post20+a15^0 == 0 /\ -tmp620^post20+tmp620^0 == 0 /\ -tmp^post20+tmp^0 == 0 /\ -1+z^post20 == 0 /\ c12^0-c12^post20 == 0 /\ -ret_min14^post20+ret_min14^0 == 0 /\ m13^0-m13^post20 == 0 /\ -tmp___1^post20+tmp___1^0 == 0 /\ b16^0-b16^post20 == 0 /\ -b11^post20+b11^0 == 0), cost: 1 20: l13 -> l12 : __const_10^0'=__const_10^post21, a10^0'=a10^post21, a15^0'=a15^post21, b11^0'=b11^post21, b16^0'=b16^post21, c12^0'=c12^post21, c17^0'=c17^post21, m13^0'=m13^post21, ret_max24^0'=ret_max24^post21, ret_min14^0'=ret_min14^post21, tmp620^0'=tmp620^post21, tmp923^0'=tmp923^post21, tmp9^0'=tmp9^post21, tmp^0'=tmp^post21, tmp___0^0'=tmp___0^post21, tmp___1^0'=tmp___1^post21, x_promoted_1^0'=x_promoted_1^post21, y_promoted_2^0'=y_promoted_2^post21, z^0'=z^post21, (tmp9^0-tmp9^post21 == 0 /\ y_promoted_2^0-y_promoted_2^post21 == 0 /\ c17^0-c17^post21 == 0 /\ tmp___0^0-tmp___0^post21 == 0 /\ -a15^post21+a15^0 == 0 /\ -x_promoted_1^post21+x_promoted_1^0 == 0 /\ -__const_10^post21+__const_10^0 == 0 /\ -ret_max24^post21+ret_max24^0 == 0 /\ m13^0-m13^post21 == 0 /\ -tmp^post21+tmp^0 == 0 /\ -z^post21+z^0 == 0 /\ b16^0-b16^post21 == 0 /\ b11^0-b11^post21 == 0 /\ ret_min14^0-ret_min14^post21 == 0 /\ -tmp923^post21+tmp923^0 == 0 /\ -tmp___1^post21+tmp___1^0 == 0 /\ -tmp620^post21+tmp620^0 == 0 /\ -c12^post21+c12^0 == 0 /\ a10^0-a10^post21 == 0), cost: 1 Chained Linear Paths Start location: l13 Program variables: __const_10^0 a10^0 a15^0 b11^0 b16^0 c12^0 c17^0 m13^0 ret_max24^0 ret_min14^0 tmp620^0 tmp923^0 tmp9^0 tmp^0 tmp___0^0 tmp___1^0 x_promoted_1^0 y_promoted_2^0 z^0 0: l0 -> l1 : __const_10^0'=__const_10^post1, a10^0'=a10^post1, a15^0'=a15^post1, b11^0'=b11^post1, b16^0'=b16^post1, c12^0'=c12^post1, c17^0'=c17^post1, m13^0'=m13^post1, ret_max24^0'=ret_max24^post1, ret_min14^0'=ret_min14^post1, tmp620^0'=tmp620^post1, tmp923^0'=tmp923^post1, tmp9^0'=tmp9^post1, tmp^0'=tmp^post1, tmp___0^0'=tmp___0^post1, tmp___1^0'=tmp___1^post1, x_promoted_1^0'=x_promoted_1^post1, y_promoted_2^0'=y_promoted_2^post1, z^0'=z^post1, (b16^0-b16^post1 == 0 /\ -tmp___1^post1+tmp___1^0 == 0 /\ -y_promoted_2^post1+y_promoted_2^0 == 0 /\ -z^post1+z^0 == 0 /\ b11^0-b11^post1 == 0 /\ ret_min14^0-ret_min14^post1 == 0 /\ -tmp___0^post1+tmp___0^0 == 0 /\ -ret_max24^post1+ret_max24^0 == 0 /\ -tmp923^post1+tmp923^0 == 0 /\ c17^0-c17^post1 == 0 /\ -a10^post1+a10^0 == 0 /\ -tmp^post1+tmp^0 == 0 /\ -a15^post1+a15^0 == 0 /\ -c12^post1+c12^0 == 0 /\ __const_10^0-__const_10^post1 == 0 /\ tmp9^0-tmp9^post1 == 0 /\ x_promoted_1^0-x_promoted_1^post1 == 0 /\ tmp620^0-tmp620^post1 == 0 /\ m13^0-m13^post1 == 0), cost: 1 1: l2 -> l3 : __const_10^0'=__const_10^post2, a10^0'=a10^post2, a15^0'=a15^post2, b11^0'=b11^post2, b16^0'=b16^post2, c12^0'=c12^post2, c17^0'=c17^post2, m13^0'=m13^post2, ret_max24^0'=ret_max24^post2, ret_min14^0'=ret_min14^post2, tmp620^0'=tmp620^post2, tmp923^0'=tmp923^post2, tmp9^0'=tmp9^post2, tmp^0'=tmp^post2, tmp___0^0'=tmp___0^post2, tmp___1^0'=tmp___1^post2, x_promoted_1^0'=x_promoted_1^post2, y_promoted_2^0'=y_promoted_2^post2, z^0'=z^post2, (0 == 0 /\ tmp___0^post2-ret_max24^post2 == 0 /\ c17^0-c17^post2 == 0 /\ y_promoted_2^0-y_promoted_2^post2 == 0 /\ -tmp923^post2+tmp923^0 == 0 /\ m13^0-m13^post2 == 0 /\ -tmp___1^post2+tmp___1^0 == 0 /\ b16^0-b16^post2 == 0 /\ -tmp620^post2+tmp620^0 == 0 /\ b11^0-b11^post2 == 0 /\ __const_10^0-__const_10^post2 == 0 /\ x_promoted_1^0-x_promoted_1^post2 == 0 /\ ret_min14^0-ret_min14^post2 == 0 /\ ret_max24^post2-a15^0 == 0 /\ -a15^post2+a15^0 == 0 /\ -a10^post2+a10^0 == 0 /\ tmp9^0-tmp9^post2 == 0 /\ -tmp^post2+tmp^0 == 0 /\ -c12^post2+c12^0 == 0), cost: 1 17: l3 -> l0 : __const_10^0'=__const_10^post18, a10^0'=a10^post18, a15^0'=a15^post18, b11^0'=b11^post18, b16^0'=b16^post18, c12^0'=c12^post18, c17^0'=c17^post18, m13^0'=m13^post18, ret_max24^0'=ret_max24^post18, ret_min14^0'=ret_min14^post18, tmp620^0'=tmp620^post18, tmp923^0'=tmp923^post18, tmp9^0'=tmp9^post18, tmp^0'=tmp^post18, tmp___0^0'=tmp___0^post18, tmp___1^0'=tmp___1^post18, x_promoted_1^0'=x_promoted_1^post18, y_promoted_2^0'=y_promoted_2^post18, z^0'=z^post18, (c17^0-c17^post18 == 0 /\ -ret_max24^post18+ret_max24^0 == 0 /\ 1-y_promoted_2^0+z^0 <= 0 /\ -x_promoted_1^post18+x_promoted_1^0 == 0 /\ -c12^post18+c12^0 == 0 /\ -z^post18+z^0 == 0 /\ tmp9^0-tmp9^post18 == 0 /\ -b11^post18+b11^0 == 0 /\ __const_10^0-__const_10^post18 == 0 /\ -y_promoted_2^0+tmp___1^post18+z^0 == 0 /\ -tmp___0^post18+tmp___0^0 == 0 /\ b16^0-b16^post18 == 0 /\ y_promoted_2^0-y_promoted_2^post18 == 0 /\ -tmp923^post18+tmp923^0 == 0 /\ m13^0-m13^post18 == 0 /\ -a15^post18+a15^0 == 0 /\ -tmp620^post18+tmp620^0 == 0 /\ ret_min14^0-ret_min14^post18 == 0 /\ -tmp^post18+tmp^0 == 0 /\ a10^0-a10^post18 == 0), cost: 1 18: l3 -> l0 : __const_10^0'=__const_10^post19, a10^0'=a10^post19, a15^0'=a15^post19, b11^0'=b11^post19, b16^0'=b16^post19, c12^0'=c12^post19, c17^0'=c17^post19, m13^0'=m13^post19, ret_max24^0'=ret_max24^post19, ret_min14^0'=ret_min14^post19, tmp620^0'=tmp620^post19, tmp923^0'=tmp923^post19, tmp9^0'=tmp9^post19, tmp^0'=tmp^post19, tmp___0^0'=tmp___0^post19, tmp___1^0'=tmp___1^post19, x_promoted_1^0'=x_promoted_1^post19, y_promoted_2^0'=y_promoted_2^post19, z^0'=z^post19, (ret_max24^0-ret_max24^post19 == 0 /\ a15^0-a15^post19 == 0 /\ -__const_10^post19+__const_10^0 == 0 /\ -y_promoted_2^0-z^0+tmp___1^post19 == 0 /\ -tmp9^post19+tmp9^0 == 0 /\ y_promoted_2^0-z^0 <= 0 /\ -tmp923^post19+tmp923^0 == 0 /\ -x_promoted_1^post19+x_promoted_1^0 == 0 /\ -c17^post19+c17^0 == 0 /\ a10^0-a10^post19 == 0 /\ -tmp620^post19+tmp620^0 == 0 /\ y_promoted_2^0-y_promoted_2^post19 == 0 /\ -tmp^post19+tmp^0 == 0 /\ z^0-z^post19 == 0 /\ c12^0-c12^post19 == 0 /\ -ret_min14^post19+ret_min14^0 == 0 /\ -b11^post19+b11^0 == 0 /\ tmp___0^0-tmp___0^post19 == 0 /\ b16^0-b16^post19 == 0 /\ m13^0-m13^post19 == 0), cost: 1 2: l4 -> l5 : __const_10^0'=__const_10^post3, a10^0'=a10^post3, a15^0'=a15^post3, b11^0'=b11^post3, b16^0'=b16^post3, c12^0'=c12^post3, c17^0'=c17^post3, m13^0'=m13^post3, ret_max24^0'=ret_max24^post3, ret_min14^0'=ret_min14^post3, tmp620^0'=tmp620^post3, tmp923^0'=tmp923^post3, tmp9^0'=tmp9^post3, tmp^0'=tmp^post3, tmp___0^0'=tmp___0^post3, tmp___1^0'=tmp___1^post3, x_promoted_1^0'=x_promoted_1^post3, y_promoted_2^0'=y_promoted_2^post3, z^0'=z^post3, (c17^0-c17^post3 == 0 /\ -tmp923^post3+tmp923^0 == 0 /\ -z^post3+z^0 == 0 /\ m13^0-m13^post3 == 0 /\ -__const_10^post3+__const_10^0 == 0 /\ -tmp___1^post3+tmp___1^0 == 0 /\ -a15^post3+a15^0 == 0 /\ b16^0-b16^post3 == 0 /\ -tmp620^post3+tmp620^0 == 0 /\ b11^0-b11^post3 == 0 /\ ret_min14^0-ret_min14^post3 == 0 /\ -tmp___0^post3+tmp___0^0 == 0 /\ -ret_max24^post3+ret_max24^0 == 0 /\ -y_promoted_2^post3+y_promoted_2^0 == 0 /\ 1+y_promoted_2^0-x_promoted_1^0 <= 0 /\ tmp9^0-tmp9^post3 == 0 /\ -tmp^post3+tmp^0 == 0 /\ a10^0-a10^post3 == 0 /\ -c12^post3+c12^0 == 0 /\ x_promoted_1^0-x_promoted_1^post3 == 0), cost: 1 3: l4 -> l3 : __const_10^0'=__const_10^post4, a10^0'=a10^post4, a15^0'=a15^post4, b11^0'=b11^post4, b16^0'=b16^post4, c12^0'=c12^post4, c17^0'=c17^post4, m13^0'=m13^post4, ret_max24^0'=ret_max24^post4, ret_min14^0'=ret_min14^post4, tmp620^0'=tmp620^post4, tmp923^0'=tmp923^post4, tmp9^0'=tmp9^post4, tmp^0'=tmp^post4, tmp___0^0'=tmp___0^post4, tmp___1^0'=tmp___1^post4, x_promoted_1^0'=x_promoted_1^post4, y_promoted_2^0'=y_promoted_2^post4, z^0'=z^post4, (0 == 0 /\ b11^0-b11^post4 == 0 /\ -tmp___0^post4+tmp___0^0 == 0 /\ ret_min14^0-ret_min14^post4 == 0 /\ -tmp923^post4+tmp923^0 == 0 /\ -ret_max24^post4+ret_max24^0 == 0 /\ __const_10^0-__const_10^post4 == 0 /\ -z^post4+z^0 == 0 /\ -a15^post4+a15^0 == 0 /\ -tmp^post4+tmp^0 == 0 /\ -b16^post4+b16^0 == 0 /\ tmp620^0-tmp620^post4 == 0 /\ -y_promoted_2^0+x_promoted_1^0 <= 0 /\ c17^0-c17^post4 == 0 /\ -tmp___1^post4+tmp___1^0 == 0 /\ -y_promoted_2^post4+y_promoted_2^0 == 0 /\ -a10^post4+a10^0 == 0 /\ -c12^post4+c12^0 == 0 /\ m13^0-m13^post4 == 0 /\ x_promoted_1^0-x_promoted_1^post4 == 0), cost: 1 15: l5 -> l7 : __const_10^0'=__const_10^post16, a10^0'=a10^post16, a15^0'=a15^post16, b11^0'=b11^post16, b16^0'=b16^post16, c12^0'=c12^post16, c17^0'=c17^post16, m13^0'=m13^post16, ret_max24^0'=ret_max24^post16, ret_min14^0'=ret_min14^post16, tmp620^0'=tmp620^post16, tmp923^0'=tmp923^post16, tmp9^0'=tmp9^post16, tmp^0'=tmp^post16, tmp___0^0'=tmp___0^post16, tmp___1^0'=tmp___1^post16, x_promoted_1^0'=x_promoted_1^post16, y_promoted_2^0'=y_promoted_2^post16, z^0'=z^post16, (-ret_min14^post16+ret_min14^0 == 0 /\ -x_promoted_1^post16+x_promoted_1^0 == 0 /\ c17^post16-x_promoted_1^0 == 0 /\ a10^0-a10^post16 == 0 /\ tmp___1^0-tmp___1^post16 == 0 /\ -y_promoted_2^0+b16^post16 == 0 /\ -tmp9^post16+tmp9^0 == 0 /\ -tmp923^post16+tmp923^0 == 0 /\ tmp___0^0-tmp___0^post16 == 0 /\ -b11^post16+b11^0 == 0 /\ -__const_10^post16+__const_10^0 == 0 /\ -ret_max24^post16+ret_max24^0 == 0 /\ z^0-z^post16 == 0 /\ 1-x_promoted_1^0+z^0 <= 0 /\ -tmp^post16+tmp^0 == 0 /\ -z^0+a15^post16 == 0 /\ m13^0-m13^post16 == 0 /\ -tmp620^post16+tmp620^0 == 0 /\ y_promoted_2^0-y_promoted_2^post16 == 0 /\ c12^0-c12^post16 == 0), cost: 1 16: l5 -> l11 : __const_10^0'=__const_10^post17, a10^0'=a10^post17, a15^0'=a15^post17, b11^0'=b11^post17, b16^0'=b16^post17, c12^0'=c12^post17, c17^0'=c17^post17, m13^0'=m13^post17, ret_max24^0'=ret_max24^post17, ret_min14^0'=ret_min14^post17, tmp620^0'=tmp620^post17, tmp923^0'=tmp923^post17, tmp9^0'=tmp9^post17, tmp^0'=tmp^post17, tmp___0^0'=tmp___0^post17, tmp___1^0'=tmp___1^post17, x_promoted_1^0'=x_promoted_1^post17, y_promoted_2^0'=y_promoted_2^post17, z^0'=z^post17, (-z^post17+z^0 == 0 /\ tmp___0^0-tmp___0^post17 == 0 /\ -ret_max24^post17+ret_max24^0 == 0 /\ tmp9^0-tmp9^post17 == 0 /\ c17^0-c17^post17 == 0 /\ -x_promoted_1^post17+x_promoted_1^0 == 0 /\ b16^0-b16^post17 == 0 /\ -tmp___1^post17+tmp___1^0 == 0 /\ -tmp^post17+tmp^0 == 0 /\ a10^post17-x_promoted_1^0 == 0 /\ y_promoted_2^0-y_promoted_2^post17 == 0 /\ m13^0-m13^post17 == 0 /\ -tmp923^post17+tmp923^0 == 0 /\ -__const_10^post17+__const_10^0 == 0 /\ b11^post17-y_promoted_2^0 == 0 /\ -a15^post17+a15^0 == 0 /\ -tmp620^post17+tmp620^0 == 0 /\ x_promoted_1^0-z^0 <= 0 /\ ret_min14^0-ret_min14^post17 == 0 /\ c12^post17-z^0 == 0), cost: 1 4: l6 -> l2 : __const_10^0'=__const_10^post5, a10^0'=a10^post5, a15^0'=a15^post5, b11^0'=b11^post5, b16^0'=b16^post5, c12^0'=c12^post5, c17^0'=c17^post5, m13^0'=m13^post5, ret_max24^0'=ret_max24^post5, ret_min14^0'=ret_min14^post5, tmp620^0'=tmp620^post5, tmp923^0'=tmp923^post5, tmp9^0'=tmp9^post5, tmp^0'=tmp^post5, tmp___0^0'=tmp___0^post5, tmp___1^0'=tmp___1^post5, x_promoted_1^0'=x_promoted_1^post5, y_promoted_2^0'=y_promoted_2^post5, z^0'=z^post5, (-x_promoted_1^post5+x_promoted_1^0 == 0 /\ -z^post5+z^0 == 0 /\ b11^0-b11^post5 == 0 /\ ret_min14^0-ret_min14^post5 == 0 /\ 1+c17^0-a15^0 <= 0 /\ -tmp___1^post5+tmp___1^0 == 0 /\ tmp9^0-tmp9^post5 == 0 /\ __const_10^0-__const_10^post5 == 0 /\ -tmp___0^post5+tmp___0^0 == 0 /\ y_promoted_2^0-y_promoted_2^post5 == 0 /\ -b16^post5+b16^0 == 0 /\ -tmp923^post5+tmp923^0 == 0 /\ -a15^post5+a15^0 == 0 /\ -c12^post5+c12^0 == 0 /\ -ret_max24^post5+ret_max24^0 == 0 /\ -tmp^post5+tmp^0 == 0 /\ -tmp620^post5+tmp620^0 == 0 /\ m13^0-m13^post5 == 0 /\ c17^0-c17^post5 == 0 /\ -a10^post5+a10^0 == 0), cost: 1 5: l6 -> l2 : __const_10^0'=__const_10^post6, a10^0'=a10^post6, a15^0'=a15^post6, b11^0'=b11^post6, b16^0'=b16^post6, c12^0'=c12^post6, c17^0'=c17^post6, m13^0'=m13^post6, ret_max24^0'=ret_max24^post6, ret_min14^0'=ret_min14^post6, tmp620^0'=tmp620^post6, tmp923^0'=tmp923^post6, tmp9^0'=tmp9^post6, tmp^0'=tmp^post6, tmp___0^0'=tmp___0^post6, tmp___1^0'=tmp___1^post6, x_promoted_1^0'=x_promoted_1^post6, y_promoted_2^0'=y_promoted_2^post6, z^0'=z^post6, (0 == 0 /\ -tmp___1^post6+tmp___1^0 == 0 /\ -x_promoted_1^post6+x_promoted_1^0 == 0 /\ -z^post6+z^0 == 0 /\ __const_10^0-__const_10^post6 == 0 /\ tmp9^0-tmp9^post6 == 0 /\ c17^0-c17^post6 == 0 /\ -tmp___0^post6+tmp___0^0 == 0 /\ -ret_max24^post6+ret_max24^0 == 0 /\ -c17^0+a15^0 <= 0 /\ m13^0-m13^post6 == 0 /\ y_promoted_2^0-y_promoted_2^post6 == 0 /\ b16^0-b16^post6 == 0 /\ -a10^post6+a10^0 == 0 /\ -a15^post6+a15^0 == 0 /\ -tmp^post6+tmp^0 == 0 /\ b11^0-b11^post6 == 0 /\ -c12^post6+c12^0 == 0 /\ ret_min14^0-ret_min14^post6 == 0 /\ -tmp620^post6+tmp620^0 == 0), cost: 1 6: l7 -> l6 : __const_10^0'=__const_10^post7, a10^0'=a10^post7, a15^0'=a15^post7, b11^0'=b11^post7, b16^0'=b16^post7, c12^0'=c12^post7, c17^0'=c17^post7, m13^0'=m13^post7, ret_max24^0'=ret_max24^post7, ret_min14^0'=ret_min14^post7, tmp620^0'=tmp620^post7, tmp923^0'=tmp923^post7, tmp9^0'=tmp9^post7, tmp^0'=tmp^post7, tmp___0^0'=tmp___0^post7, tmp___1^0'=tmp___1^post7, x_promoted_1^0'=x_promoted_1^post7, y_promoted_2^0'=y_promoted_2^post7, z^0'=z^post7, (-ret_max24^post7+ret_max24^0 == 0 /\ -m13^post7+m13^0 == 0 /\ -y_promoted_2^post7+y_promoted_2^0 == 0 /\ __const_10^0-__const_10^post7 == 0 /\ -tmp___1^post7+tmp___1^0 == 0 /\ -c12^post7+c12^0 == 0 /\ -z^post7+z^0 == 0 /\ 1+b16^0-a15^0 <= 0 /\ ret_min14^0-ret_min14^post7 == 0 /\ -b16^post7+b16^0 == 0 /\ -tmp___0^post7+tmp___0^0 == 0 /\ -tmp923^post7+tmp923^0 == 0 /\ c17^0-c17^post7 == 0 /\ tmp9^0-tmp9^post7 == 0 /\ -tmp^post7+tmp^0 == 0 /\ -a15^post7+a15^0 == 0 /\ b11^0-b11^post7 == 0 /\ -a10^post7+a10^0 == 0 /\ x_promoted_1^0-x_promoted_1^post7 == 0 /\ tmp620^0-tmp620^post7 == 0), cost: 1 7: l7 -> l6 : __const_10^0'=__const_10^post8, a10^0'=a10^post8, a15^0'=a15^post8, b11^0'=b11^post8, b16^0'=b16^post8, c12^0'=c12^post8, c17^0'=c17^post8, m13^0'=m13^post8, ret_max24^0'=ret_max24^post8, ret_min14^0'=ret_min14^post8, tmp620^0'=tmp620^post8, tmp923^0'=tmp923^post8, tmp9^0'=tmp9^post8, tmp^0'=tmp^post8, tmp___0^0'=tmp___0^post8, tmp___1^0'=tmp___1^post8, x_promoted_1^0'=x_promoted_1^post8, y_promoted_2^0'=y_promoted_2^post8, z^0'=z^post8, (0 == 0 /\ y_promoted_2^0-y_promoted_2^post8 == 0 /\ -tmp___1^post8+tmp___1^0 == 0 /\ -a15^post8+a15^0 == 0 /\ ret_min14^0-ret_min14^post8 == 0 /\ -a10^post8+a10^0 == 0 /\ -b16^post8+b16^0 == 0 /\ -z^post8+z^0 == 0 /\ -ret_max24^post8+ret_max24^0 == 0 /\ -tmp923^post8+tmp923^0 == 0 /\ -tmp___0^post8+tmp___0^0 == 0 /\ -b16^0+a15^0 <= 0 /\ -tmp^post8+tmp^0 == 0 /\ __const_10^0-__const_10^post8 == 0 /\ c17^0-c17^post8 == 0 /\ tmp9^0-tmp9^post8 == 0 /\ x_promoted_1^0-x_promoted_1^post8 == 0 /\ -c12^post8+c12^0 == 0 /\ m13^0-m13^post8 == 0 /\ b11^0-b11^post8 == 0), cost: 1 8: l8 -> l9 : __const_10^0'=__const_10^post9, a10^0'=a10^post9, a15^0'=a15^post9, b11^0'=b11^post9, b16^0'=b16^post9, c12^0'=c12^post9, c17^0'=c17^post9, m13^0'=m13^post9, ret_max24^0'=ret_max24^post9, ret_min14^0'=ret_min14^post9, tmp620^0'=tmp620^post9, tmp923^0'=tmp923^post9, tmp9^0'=tmp9^post9, tmp^0'=tmp^post9, tmp___0^0'=tmp___0^post9, tmp___1^0'=tmp___1^post9, x_promoted_1^0'=x_promoted_1^post9, y_promoted_2^0'=y_promoted_2^post9, z^0'=z^post9, (y_promoted_2^0-y_promoted_2^post9 == 0 /\ m13^post9-c12^0 == 0 /\ c17^0-c17^post9 == 0 /\ tmp___0^0-tmp___0^post9 == 0 /\ -tmp923^post9+tmp923^0 == 0 /\ -ret_max24^post9+ret_max24^0 == 0 /\ -z^post9+z^0 == 0 /\ -x_promoted_1^post9+x_promoted_1^0 == 0 /\ -a15^post9+a15^0 == 0 /\ -__const_10^post9+__const_10^0 == 0 /\ -tmp620^post9+tmp620^0 == 0 /\ b16^0-b16^post9 == 0 /\ b11^0-b11^post9 == 0 /\ ret_min14^0-ret_min14^post9 == 0 /\ 1-b11^0+c12^0 <= 0 /\ tmp9^0-tmp9^post9 == 0 /\ -tmp___1^post9+tmp___1^0 == 0 /\ a10^0-a10^post9 == 0 /\ -c12^post9+c12^0 == 0 /\ -tmp^post9+tmp^0 == 0), cost: 1 9: l8 -> l9 : __const_10^0'=__const_10^post10, a10^0'=a10^post10, a15^0'=a15^post10, b11^0'=b11^post10, b16^0'=b16^post10, c12^0'=c12^post10, c17^0'=c17^post10, m13^0'=m13^post10, ret_max24^0'=ret_max24^post10, ret_min14^0'=ret_min14^post10, tmp620^0'=tmp620^post10, tmp923^0'=tmp923^post10, tmp9^0'=tmp9^post10, tmp^0'=tmp^post10, tmp___0^0'=tmp___0^post10, tmp___1^0'=tmp___1^post10, x_promoted_1^0'=x_promoted_1^post10, y_promoted_2^0'=y_promoted_2^post10, z^0'=z^post10, (-tmp___0^post10+tmp___0^0 == 0 /\ c17^0-c17^post10 == 0 /\ -tmp620^post10+tmp620^0 == 0 /\ -tmp^post10+tmp^0 == 0 /\ -z^post10+z^0 == 0 /\ -a15^post10+a15^0 == 0 /\ b16^0-b16^post10 == 0 /\ -__const_10^post10+__const_10^0 == 0 /\ ret_min14^0-ret_min14^post10 == 0 /\ tmp9^0-tmp9^post10 == 0 /\ b11^0-b11^post10 == 0 /\ -c12^post10+c12^0 == 0 /\ -ret_max24^post10+ret_max24^0 == 0 /\ -tmp923^post10+tmp923^0 == 0 /\ m13^post10-b11^0 == 0 /\ -tmp___1^post10+tmp___1^0 == 0 /\ -y_promoted_2^post10+y_promoted_2^0 == 0 /\ x_promoted_1^0-x_promoted_1^post10 == 0 /\ a10^0-a10^post10 == 0 /\ b11^0-c12^0 <= 0), cost: 1 10: l9 -> l3 : __const_10^0'=__const_10^post11, a10^0'=a10^post11, a15^0'=a15^post11, b11^0'=b11^post11, b16^0'=b16^post11, c12^0'=c12^post11, c17^0'=c17^post11, m13^0'=m13^post11, ret_max24^0'=ret_max24^post11, ret_min14^0'=ret_min14^post11, tmp620^0'=tmp620^post11, tmp923^0'=tmp923^post11, tmp9^0'=tmp9^post11, tmp^0'=tmp^post11, tmp___0^0'=tmp___0^post11, tmp___1^0'=tmp___1^post11, x_promoted_1^0'=x_promoted_1^post11, y_promoted_2^0'=y_promoted_2^post11, z^0'=z^post11, (b11^0-b11^post11 == 0 /\ -m13^0+ret_min14^post11 == 0 /\ -tmp___0^post11+tmp___0^0 == 0 /\ -ret_max24^post11+ret_max24^0 == 0 /\ -ret_min14^post11+tmp^post11 == 0 /\ __const_10^0-__const_10^post11 == 0 /\ -b16^post11+b16^0 == 0 /\ -a15^post11+a15^0 == 0 /\ -z^post11+z^0 == 0 /\ -x_promoted_1^0+x_promoted_1^post11-tmp^post11 == 0 /\ tmp9^0-tmp9^post11 == 0 /\ c17^0-c17^post11 == 0 /\ -tmp923^post11+tmp923^0 == 0 /\ tmp620^0-tmp620^post11 == 0 /\ -tmp___1^post11+tmp___1^0 == 0 /\ m13^0-m13^post11 == 0 /\ -c12^post11+c12^0 == 0 /\ -a10^post11+a10^0 == 0 /\ -y_promoted_2^post11+y_promoted_2^0 == 0), cost: 1 11: l10 -> l9 : __const_10^0'=__const_10^post12, a10^0'=a10^post12, a15^0'=a15^post12, b11^0'=b11^post12, b16^0'=b16^post12, c12^0'=c12^post12, c17^0'=c17^post12, m13^0'=m13^post12, ret_max24^0'=ret_max24^post12, ret_min14^0'=ret_min14^post12, tmp620^0'=tmp620^post12, tmp923^0'=tmp923^post12, tmp9^0'=tmp9^post12, tmp^0'=tmp^post12, tmp___0^0'=tmp___0^post12, tmp___1^0'=tmp___1^post12, x_promoted_1^0'=x_promoted_1^post12, y_promoted_2^0'=y_promoted_2^post12, z^0'=z^post12, (m13^post12-c12^0 == 0 /\ ret_max24^0-ret_max24^post12 == 0 /\ b16^0-b16^post12 == 0 /\ b11^0-b11^post12 == 0 /\ -x_promoted_1^post12+x_promoted_1^0 == 0 /\ tmp___1^0-tmp___1^post12 == 0 /\ -c17^post12+c17^0 == 0 /\ __const_10^0-__const_10^post12 == 0 /\ -tmp9^post12+tmp9^0 == 0 /\ -tmp923^post12+tmp923^0 == 0 /\ -tmp^post12+tmp^0 == 0 /\ -a15^post12+a15^0 == 0 /\ -tmp620^post12+tmp620^0 == 0 /\ 1-a10^0+c12^0 <= 0 /\ tmp___0^0-tmp___0^post12 == 0 /\ -ret_min14^post12+ret_min14^0 == 0 /\ y_promoted_2^0-y_promoted_2^post12 == 0 /\ c12^0-c12^post12 == 0 /\ -a10^post12+a10^0 == 0 /\ z^0-z^post12 == 0), cost: 1 12: l10 -> l9 : __const_10^0'=__const_10^post13, a10^0'=a10^post13, a15^0'=a15^post13, b11^0'=b11^post13, b16^0'=b16^post13, c12^0'=c12^post13, c17^0'=c17^post13, m13^0'=m13^post13, ret_max24^0'=ret_max24^post13, ret_min14^0'=ret_min14^post13, tmp620^0'=tmp620^post13, tmp923^0'=tmp923^post13, tmp9^0'=tmp9^post13, tmp^0'=tmp^post13, tmp___0^0'=tmp___0^post13, tmp___1^0'=tmp___1^post13, x_promoted_1^0'=x_promoted_1^post13, y_promoted_2^0'=y_promoted_2^post13, z^0'=z^post13, (ret_max24^0-ret_max24^post13 == 0 /\ a15^0-a15^post13 == 0 /\ -tmp923^post13+tmp923^0 == 0 /\ -z^post13+z^0 == 0 /\ tmp9^0-tmp9^post13 == 0 /\ -c17^post13+c17^0 == 0 /\ -tmp___1^post13+tmp___1^0 == 0 /\ -tmp620^post13+tmp620^0 == 0 /\ a10^0-a10^post13 == 0 /\ c12^0-c12^post13 == 0 /\ y_promoted_2^0-y_promoted_2^post13 == 0 /\ -__const_10^post13+__const_10^0 == 0 /\ -x_promoted_1^post13+x_promoted_1^0 == 0 /\ a10^0-c12^0 <= 0 /\ -ret_min14^post13+ret_min14^0 == 0 /\ tmp___0^0-tmp___0^post13 == 0 /\ -a10^0+m13^post13 == 0 /\ -tmp^post13+tmp^0 == 0 /\ -b11^post13+b11^0 == 0 /\ b16^0-b16^post13 == 0), cost: 1 13: l11 -> l8 : __const_10^0'=__const_10^post14, a10^0'=a10^post14, a15^0'=a15^post14, b11^0'=b11^post14, b16^0'=b16^post14, c12^0'=c12^post14, c17^0'=c17^post14, m13^0'=m13^post14, ret_max24^0'=ret_max24^post14, ret_min14^0'=ret_min14^post14, tmp620^0'=tmp620^post14, tmp923^0'=tmp923^post14, tmp9^0'=tmp9^post14, tmp^0'=tmp^post14, tmp___0^0'=tmp___0^post14, tmp___1^0'=tmp___1^post14, x_promoted_1^0'=x_promoted_1^post14, y_promoted_2^0'=y_promoted_2^post14, z^0'=z^post14, (y_promoted_2^0-y_promoted_2^post14 == 0 /\ 1-a10^0+b11^0 <= 0 /\ c17^0-c17^post14 == 0 /\ tmp9^0-tmp9^post14 == 0 /\ -__const_10^post14+__const_10^0 == 0 /\ -ret_max24^post14+ret_max24^0 == 0 /\ -tmp923^post14+tmp923^0 == 0 /\ -z^post14+z^0 == 0 /\ -x_promoted_1^post14+x_promoted_1^0 == 0 /\ -a15^post14+a15^0 == 0 /\ m13^0-m13^post14 == 0 /\ b16^0-b16^post14 == 0 /\ -tmp___0^post14+tmp___0^0 == 0 /\ -tmp620^post14+tmp620^0 == 0 /\ b11^0-b11^post14 == 0 /\ -tmp^post14+tmp^0 == 0 /\ ret_min14^0-ret_min14^post14 == 0 /\ -c12^post14+c12^0 == 0 /\ -tmp___1^post14+tmp___1^0 == 0 /\ a10^0-a10^post14 == 0), cost: 1 14: l11 -> l10 : __const_10^0'=__const_10^post15, a10^0'=a10^post15, a15^0'=a15^post15, b11^0'=b11^post15, b16^0'=b16^post15, c12^0'=c12^post15, c17^0'=c17^post15, m13^0'=m13^post15, ret_max24^0'=ret_max24^post15, ret_min14^0'=ret_min14^post15, tmp620^0'=tmp620^post15, tmp923^0'=tmp923^post15, tmp9^0'=tmp9^post15, tmp^0'=tmp^post15, tmp___0^0'=tmp___0^post15, tmp___1^0'=tmp___1^post15, x_promoted_1^0'=x_promoted_1^post15, y_promoted_2^0'=y_promoted_2^post15, z^0'=z^post15, (-x_promoted_1^post15+x_promoted_1^0 == 0 /\ -tmp9^post15+tmp9^0 == 0 /\ c17^0-c17^post15 == 0 /\ -tmp923^post15+tmp923^0 == 0 /\ -tmp^post15+tmp^0 == 0 /\ a10^0-b11^0 <= 0 /\ -__const_10^post15+__const_10^0 == 0 /\ -ret_max24^post15+ret_max24^0 == 0 /\ -a15^post15+a15^0 == 0 /\ m13^0-m13^post15 == 0 /\ -tmp620^post15+tmp620^0 == 0 /\ b16^0-b16^post15 == 0 /\ z^0-z^post15 == 0 /\ b11^0-b11^post15 == 0 /\ ret_min14^0-ret_min14^post15 == 0 /\ tmp___0^0-tmp___0^post15 == 0 /\ -tmp___1^post15+tmp___1^0 == 0 /\ a10^0-a10^post15 == 0 /\ y_promoted_2^0-y_promoted_2^post15 == 0 /\ -c12^post15+c12^0 == 0), cost: 1 21: l13 -> l4 : __const_10^0'=__const_10^post20, a10^0'=a10^post20, a15^0'=a15^post20, b11^0'=b11^post20, b16^0'=b16^post20, c12^0'=c12^post20, c17^0'=c17^post20, m13^0'=m13^post20, ret_max24^0'=ret_max24^post20, ret_min14^0'=ret_min14^post20, tmp620^0'=tmp620^post20, tmp923^0'=tmp923^post20, tmp9^0'=tmp9^post20, tmp^0'=tmp^post20, tmp___0^0'=tmp___0^post20, tmp___1^0'=tmp___1^post20, x_promoted_1^0'=x_promoted_1^post20, y_promoted_2^0'=y_promoted_2^post20, z^0'=z^post20, (a15^post21-a15^post20 == 0 /\ tmp923^post21-tmp923^post20 == 0 /\ tmp9^0-tmp9^post21 == 0 /\ -b11^post20+b11^post21 == 0 /\ y_promoted_2^0-y_promoted_2^post21 == 0 /\ tmp620^post21-tmp620^post20 == 0 /\ -2+y_promoted_2^post20 == 0 /\ c17^0-c17^post21 == 0 /\ tmp___0^0-tmp___0^post21 == 0 /\ a10^post21-a10^post20 == 0 /\ -__const_10^post21+x_promoted_1^post20 == 0 /\ m13^post21-m13^post20 == 0 /\ -a15^post21+a15^0 == 0 /\ -x_promoted_1^post21+x_promoted_1^0 == 0 /\ -__const_10^post21+__const_10^0 == 0 /\ -ret_max24^post21+ret_max24^0 == 0 /\ m13^0-m13^post21 == 0 /\ -tmp^post21+tmp^0 == 0 /\ -c17^post20+c17^post21 == 0 /\ -z^post21+z^0 == 0 /\ tmp___0^post21-tmp___0^post20 == 0 /\ b16^post21-b16^post20 == 0 /\ -1+z^post20 == 0 /\ b16^0-b16^post21 == 0 /\ b11^0-b11^post21 == 0 /\ tmp^post21-tmp^post20 == 0 /\ c12^post21-c12^post20 == 0 /\ ret_min14^0-ret_min14^post21 == 0 /\ -tmp923^post21+tmp923^0 == 0 /\ -ret_min14^post20+ret_min14^post21 == 0 /\ __const_10^post21-__const_10^post20 == 0 /\ tmp___1^post21-tmp___1^post20 == 0 /\ -tmp___1^post21+tmp___1^0 == 0 /\ ret_max24^post21-ret_max24^post20 == 0 /\ tmp9^post21-tmp9^post20 == 0 /\ -tmp620^post21+tmp620^0 == 0 /\ -c12^post21+c12^0 == 0 /\ a10^0-a10^post21 == 0), cost: 1 Eliminating location l12 by chaining: Applied chaining First rule: l13 -> l12 : __const_10^0'=__const_10^post21, a10^0'=a10^post21, a15^0'=a15^post21, b11^0'=b11^post21, b16^0'=b16^post21, c12^0'=c12^post21, c17^0'=c17^post21, m13^0'=m13^post21, ret_max24^0'=ret_max24^post21, ret_min14^0'=ret_min14^post21, tmp620^0'=tmp620^post21, tmp923^0'=tmp923^post21, tmp9^0'=tmp9^post21, tmp^0'=tmp^post21, tmp___0^0'=tmp___0^post21, tmp___1^0'=tmp___1^post21, x_promoted_1^0'=x_promoted_1^post21, y_promoted_2^0'=y_promoted_2^post21, z^0'=z^post21, (tmp9^0-tmp9^post21 == 0 /\ y_promoted_2^0-y_promoted_2^post21 == 0 /\ c17^0-c17^post21 == 0 /\ tmp___0^0-tmp___0^post21 == 0 /\ -a15^post21+a15^0 == 0 /\ -x_promoted_1^post21+x_promoted_1^0 == 0 /\ -__const_10^post21+__const_10^0 == 0 /\ -ret_max24^post21+ret_max24^0 == 0 /\ m13^0-m13^post21 == 0 /\ -tmp^post21+tmp^0 == 0 /\ -z^post21+z^0 == 0 /\ b16^0-b16^post21 == 0 /\ b11^0-b11^post21 == 0 /\ ret_min14^0-ret_min14^post21 == 0 /\ -tmp923^post21+tmp923^0 == 0 /\ -tmp___1^post21+tmp___1^0 == 0 /\ -tmp620^post21+tmp620^0 == 0 /\ -c12^post21+c12^0 == 0 /\ a10^0-a10^post21 == 0), cost: 1 Second rule: l12 -> l4 : __const_10^0'=__const_10^post20, a10^0'=a10^post20, a15^0'=a15^post20, b11^0'=b11^post20, b16^0'=b16^post20, c12^0'=c12^post20, c17^0'=c17^post20, m13^0'=m13^post20, ret_max24^0'=ret_max24^post20, ret_min14^0'=ret_min14^post20, tmp620^0'=tmp620^post20, tmp923^0'=tmp923^post20, tmp9^0'=tmp9^post20, tmp^0'=tmp^post20, tmp___0^0'=tmp___0^post20, tmp___1^0'=tmp___1^post20, x_promoted_1^0'=x_promoted_1^post20, y_promoted_2^0'=y_promoted_2^post20, z^0'=z^post20, (ret_max24^0-ret_max24^post20 == 0 /\ tmp___0^0-tmp___0^post20 == 0 /\ -2+y_promoted_2^post20 == 0 /\ -tmp923^post20+tmp923^0 == 0 /\ x_promoted_1^post20-__const_10^0 == 0 /\ tmp9^0-tmp9^post20 == 0 /\ -__const_10^post20+__const_10^0 == 0 /\ a10^0-a10^post20 == 0 /\ -c17^post20+c17^0 == 0 /\ -a15^post20+a15^0 == 0 /\ -tmp620^post20+tmp620^0 == 0 /\ -tmp^post20+tmp^0 == 0 /\ -1+z^post20 == 0 /\ c12^0-c12^post20 == 0 /\ -ret_min14^post20+ret_min14^0 == 0 /\ m13^0-m13^post20 == 0 /\ -tmp___1^post20+tmp___1^0 == 0 /\ b16^0-b16^post20 == 0 /\ -b11^post20+b11^0 == 0), cost: 1 New rule: l13 -> l4 : __const_10^0'=__const_10^post20, a10^0'=a10^post20, a15^0'=a15^post20, b11^0'=b11^post20, b16^0'=b16^post20, c12^0'=c12^post20, c17^0'=c17^post20, m13^0'=m13^post20, ret_max24^0'=ret_max24^post20, ret_min14^0'=ret_min14^post20, tmp620^0'=tmp620^post20, tmp923^0'=tmp923^post20, tmp9^0'=tmp9^post20, tmp^0'=tmp^post20, tmp___0^0'=tmp___0^post20, tmp___1^0'=tmp___1^post20, x_promoted_1^0'=x_promoted_1^post20, y_promoted_2^0'=y_promoted_2^post20, z^0'=z^post20, (a15^post21-a15^post20 == 0 /\ tmp923^post21-tmp923^post20 == 0 /\ tmp9^0-tmp9^post21 == 0 /\ -b11^post20+b11^post21 == 0 /\ y_promoted_2^0-y_promoted_2^post21 == 0 /\ tmp620^post21-tmp620^post20 == 0 /\ -2+y_promoted_2^post20 == 0 /\ c17^0-c17^post21 == 0 /\ tmp___0^0-tmp___0^post21 == 0 /\ a10^post21-a10^post20 == 0 /\ -__const_10^post21+x_promoted_1^post20 == 0 /\ m13^post21-m13^post20 == 0 /\ -a15^post21+a15^0 == 0 /\ -x_promoted_1^post21+x_promoted_1^0 == 0 /\ -__const_10^post21+__const_10^0 == 0 /\ -ret_max24^post21+ret_max24^0 == 0 /\ m13^0-m13^post21 == 0 /\ -tmp^post21+tmp^0 == 0 /\ -c17^post20+c17^post21 == 0 /\ -z^post21+z^0 == 0 /\ tmp___0^post21-tmp___0^post20 == 0 /\ b16^post21-b16^post20 == 0 /\ -1+z^post20 == 0 /\ b16^0-b16^post21 == 0 /\ b11^0-b11^post21 == 0 /\ tmp^post21-tmp^post20 == 0 /\ c12^post21-c12^post20 == 0 /\ ret_min14^0-ret_min14^post21 == 0 /\ -tmp923^post21+tmp923^0 == 0 /\ -ret_min14^post20+ret_min14^post21 == 0 /\ __const_10^post21-__const_10^post20 == 0 /\ tmp___1^post21-tmp___1^post20 == 0 /\ -tmp___1^post21+tmp___1^0 == 0 /\ ret_max24^post21-ret_max24^post20 == 0 /\ tmp9^post21-tmp9^post20 == 0 /\ -tmp620^post21+tmp620^0 == 0 /\ -c12^post21+c12^0 == 0 /\ a10^0-a10^post21 == 0), cost: 1 Applied deletion Removed the following rules: 19 20 Simplified Transitions Start location: l13 Program variables: __const_10^0 a10^0 a15^0 b11^0 b16^0 c12^0 c17^0 m13^0 ret_max24^0 ret_min14^0 tmp620^0 tmp923^0 tmp9^0 tmp^0 tmp___0^0 tmp___1^0 x_promoted_1^0 y_promoted_2^0 z^0 22: l0 -> l1 : T, cost: 1 23: l2 -> l3 : ret_max24^0'=a15^0, tmp___0^0'=a15^0, z^0'=z^post2, T, cost: 1 39: l3 -> l0 : tmp___1^0'=y_promoted_2^0-z^0, 1-y_promoted_2^0+z^0 <= 0, cost: 1 40: l3 -> l0 : tmp___1^0'=y_promoted_2^0+z^0, y_promoted_2^0-z^0 <= 0, cost: 1 24: l4 -> l5 : 1+y_promoted_2^0-x_promoted_1^0 <= 0, cost: 1 25: l4 -> l3 : tmp9^0'=tmp9^post4, -y_promoted_2^0+x_promoted_1^0 <= 0, cost: 1 37: l5 -> l7 : a15^0'=z^0, b16^0'=y_promoted_2^0, c17^0'=x_promoted_1^0, 1-x_promoted_1^0+z^0 <= 0, cost: 1 38: l5 -> l11 : a10^0'=x_promoted_1^0, b11^0'=y_promoted_2^0, c12^0'=z^0, x_promoted_1^0-z^0 <= 0, cost: 1 26: l6 -> l2 : 1+c17^0-a15^0 <= 0, cost: 1 27: l6 -> l2 : tmp923^0'=tmp923^post6, -c17^0+a15^0 <= 0, cost: 1 28: l7 -> l6 : 1+b16^0-a15^0 <= 0, cost: 1 29: l7 -> l6 : tmp620^0'=tmp620^post8, -b16^0+a15^0 <= 0, cost: 1 30: l8 -> l9 : m13^0'=c12^0, 1-b11^0+c12^0 <= 0, cost: 1 31: l8 -> l9 : m13^0'=b11^0, b11^0-c12^0 <= 0, cost: 1 32: l9 -> l3 : ret_min14^0'=m13^0, tmp^0'=m13^0, x_promoted_1^0'=m13^0+x_promoted_1^0, T, cost: 1 33: l10 -> l9 : m13^0'=c12^0, 1-a10^0+c12^0 <= 0, cost: 1 34: l10 -> l9 : m13^0'=a10^0, a10^0-c12^0 <= 0, cost: 1 35: l11 -> l8 : 1-a10^0+b11^0 <= 0, cost: 1 36: l11 -> l10 : a10^0-b11^0 <= 0, cost: 1 41: l13 -> l4 : x_promoted_1^0'=__const_10^0, y_promoted_2^0'=2, z^0'=1, T, cost: 1 Propagated Equalities Original rule: l0 -> l1 : __const_10^0'=__const_10^post1, a10^0'=a10^post1, a15^0'=a15^post1, b11^0'=b11^post1, b16^0'=b16^post1, c12^0'=c12^post1, c17^0'=c17^post1, m13^0'=m13^post1, ret_max24^0'=ret_max24^post1, ret_min14^0'=ret_min14^post1, tmp620^0'=tmp620^post1, tmp923^0'=tmp923^post1, tmp9^0'=tmp9^post1, tmp^0'=tmp^post1, tmp___0^0'=tmp___0^post1, tmp___1^0'=tmp___1^post1, x_promoted_1^0'=x_promoted_1^post1, y_promoted_2^0'=y_promoted_2^post1, z^0'=z^post1, (b16^0-b16^post1 == 0 /\ -tmp___1^post1+tmp___1^0 == 0 /\ -y_promoted_2^post1+y_promoted_2^0 == 0 /\ -z^post1+z^0 == 0 /\ b11^0-b11^post1 == 0 /\ ret_min14^0-ret_min14^post1 == 0 /\ -tmp___0^post1+tmp___0^0 == 0 /\ -ret_max24^post1+ret_max24^0 == 0 /\ -tmp923^post1+tmp923^0 == 0 /\ c17^0-c17^post1 == 0 /\ -a10^post1+a10^0 == 0 /\ -tmp^post1+tmp^0 == 0 /\ -a15^post1+a15^0 == 0 /\ -c12^post1+c12^0 == 0 /\ __const_10^0-__const_10^post1 == 0 /\ tmp9^0-tmp9^post1 == 0 /\ x_promoted_1^0-x_promoted_1^post1 == 0 /\ tmp620^0-tmp620^post1 == 0 /\ m13^0-m13^post1 == 0), cost: 1 New rule: l0 -> l1 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, 0 == 0, cost: 1 propagated equality b16^post1 = b16^0 propagated equality tmp___1^post1 = tmp___1^0 propagated equality y_promoted_2^post1 = y_promoted_2^0 propagated equality z^post1 = z^0 propagated equality b11^post1 = b11^0 propagated equality ret_min14^post1 = ret_min14^0 propagated equality tmp___0^post1 = tmp___0^0 propagated equality ret_max24^post1 = ret_max24^0 propagated equality tmp923^post1 = tmp923^0 propagated equality c17^post1 = c17^0 propagated equality a10^post1 = a10^0 propagated equality tmp^post1 = tmp^0 propagated equality a15^post1 = a15^0 propagated equality c12^post1 = c12^0 propagated equality __const_10^post1 = __const_10^0 propagated equality tmp9^post1 = tmp9^0 propagated equality x_promoted_1^post1 = x_promoted_1^0 propagated equality tmp620^post1 = tmp620^0 propagated equality m13^post1 = m13^0 Simplified Guard Original rule: l0 -> l1 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, 0 == 0, cost: 1 New rule: l0 -> l1 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, T, cost: 1 Removed Trivial Updates Original rule: l0 -> l1 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, T, cost: 1 New rule: l0 -> l1 : T, cost: 1 Propagated Equalities Original rule: l2 -> l3 : __const_10^0'=__const_10^post2, a10^0'=a10^post2, a15^0'=a15^post2, b11^0'=b11^post2, b16^0'=b16^post2, c12^0'=c12^post2, c17^0'=c17^post2, m13^0'=m13^post2, ret_max24^0'=ret_max24^post2, ret_min14^0'=ret_min14^post2, tmp620^0'=tmp620^post2, tmp923^0'=tmp923^post2, tmp9^0'=tmp9^post2, tmp^0'=tmp^post2, tmp___0^0'=tmp___0^post2, tmp___1^0'=tmp___1^post2, x_promoted_1^0'=x_promoted_1^post2, y_promoted_2^0'=y_promoted_2^post2, z^0'=z^post2, (0 == 0 /\ tmp___0^post2-ret_max24^post2 == 0 /\ c17^0-c17^post2 == 0 /\ y_promoted_2^0-y_promoted_2^post2 == 0 /\ -tmp923^post2+tmp923^0 == 0 /\ m13^0-m13^post2 == 0 /\ -tmp___1^post2+tmp___1^0 == 0 /\ b16^0-b16^post2 == 0 /\ -tmp620^post2+tmp620^0 == 0 /\ b11^0-b11^post2 == 0 /\ __const_10^0-__const_10^post2 == 0 /\ x_promoted_1^0-x_promoted_1^post2 == 0 /\ ret_min14^0-ret_min14^post2 == 0 /\ ret_max24^post2-a15^0 == 0 /\ -a15^post2+a15^0 == 0 /\ -a10^post2+a10^0 == 0 /\ tmp9^0-tmp9^post2 == 0 /\ -tmp^post2+tmp^0 == 0 /\ -c12^post2+c12^0 == 0), cost: 1 New rule: l2 -> l3 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=a15^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=a15^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^post2, 0 == 0, cost: 1 propagated equality ret_max24^post2 = tmp___0^post2 propagated equality c17^post2 = c17^0 propagated equality y_promoted_2^post2 = y_promoted_2^0 propagated equality tmp923^post2 = tmp923^0 propagated equality m13^post2 = m13^0 propagated equality tmp___1^post2 = tmp___1^0 propagated equality b16^post2 = b16^0 propagated equality tmp620^post2 = tmp620^0 propagated equality b11^post2 = b11^0 propagated equality __const_10^post2 = __const_10^0 propagated equality x_promoted_1^post2 = x_promoted_1^0 propagated equality ret_min14^post2 = ret_min14^0 propagated equality tmp___0^post2 = a15^0 propagated equality a15^post2 = a15^0 propagated equality a10^post2 = a10^0 propagated equality tmp9^post2 = tmp9^0 propagated equality tmp^post2 = tmp^0 propagated equality c12^post2 = c12^0 Simplified Guard Original rule: l2 -> l3 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=a15^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=a15^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^post2, 0 == 0, cost: 1 New rule: l2 -> l3 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=a15^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=a15^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^post2, T, cost: 1 Removed Trivial Updates Original rule: l2 -> l3 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=a15^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=a15^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^post2, T, cost: 1 New rule: l2 -> l3 : ret_max24^0'=a15^0, tmp___0^0'=a15^0, z^0'=z^post2, T, cost: 1 Propagated Equalities Original rule: l4 -> l5 : __const_10^0'=__const_10^post3, a10^0'=a10^post3, a15^0'=a15^post3, b11^0'=b11^post3, b16^0'=b16^post3, c12^0'=c12^post3, c17^0'=c17^post3, m13^0'=m13^post3, ret_max24^0'=ret_max24^post3, ret_min14^0'=ret_min14^post3, tmp620^0'=tmp620^post3, tmp923^0'=tmp923^post3, tmp9^0'=tmp9^post3, tmp^0'=tmp^post3, tmp___0^0'=tmp___0^post3, tmp___1^0'=tmp___1^post3, x_promoted_1^0'=x_promoted_1^post3, y_promoted_2^0'=y_promoted_2^post3, z^0'=z^post3, (c17^0-c17^post3 == 0 /\ -tmp923^post3+tmp923^0 == 0 /\ -z^post3+z^0 == 0 /\ m13^0-m13^post3 == 0 /\ -__const_10^post3+__const_10^0 == 0 /\ -tmp___1^post3+tmp___1^0 == 0 /\ -a15^post3+a15^0 == 0 /\ b16^0-b16^post3 == 0 /\ -tmp620^post3+tmp620^0 == 0 /\ b11^0-b11^post3 == 0 /\ ret_min14^0-ret_min14^post3 == 0 /\ -tmp___0^post3+tmp___0^0 == 0 /\ -ret_max24^post3+ret_max24^0 == 0 /\ -y_promoted_2^post3+y_promoted_2^0 == 0 /\ 1+y_promoted_2^0-x_promoted_1^0 <= 0 /\ tmp9^0-tmp9^post3 == 0 /\ -tmp^post3+tmp^0 == 0 /\ a10^0-a10^post3 == 0 /\ -c12^post3+c12^0 == 0 /\ x_promoted_1^0-x_promoted_1^post3 == 0), cost: 1 New rule: l4 -> l5 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, (0 == 0 /\ 1+y_promoted_2^0-x_promoted_1^0 <= 0), cost: 1 propagated equality c17^post3 = c17^0 propagated equality tmp923^post3 = tmp923^0 propagated equality z^post3 = z^0 propagated equality m13^post3 = m13^0 propagated equality __const_10^post3 = __const_10^0 propagated equality tmp___1^post3 = tmp___1^0 propagated equality a15^post3 = a15^0 propagated equality b16^post3 = b16^0 propagated equality tmp620^post3 = tmp620^0 propagated equality b11^post3 = b11^0 propagated equality ret_min14^post3 = ret_min14^0 propagated equality tmp___0^post3 = tmp___0^0 propagated equality ret_max24^post3 = ret_max24^0 propagated equality y_promoted_2^post3 = y_promoted_2^0 propagated equality tmp9^post3 = tmp9^0 propagated equality tmp^post3 = tmp^0 propagated equality a10^post3 = a10^0 propagated equality c12^post3 = c12^0 propagated equality x_promoted_1^post3 = x_promoted_1^0 Simplified Guard Original rule: l4 -> l5 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, (0 == 0 /\ 1+y_promoted_2^0-x_promoted_1^0 <= 0), cost: 1 New rule: l4 -> l5 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, 1+y_promoted_2^0-x_promoted_1^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l4 -> l5 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, 1+y_promoted_2^0-x_promoted_1^0 <= 0, cost: 1 New rule: l4 -> l5 : 1+y_promoted_2^0-x_promoted_1^0 <= 0, cost: 1 Propagated Equalities Original rule: l4 -> l3 : __const_10^0'=__const_10^post4, a10^0'=a10^post4, a15^0'=a15^post4, b11^0'=b11^post4, b16^0'=b16^post4, c12^0'=c12^post4, c17^0'=c17^post4, m13^0'=m13^post4, ret_max24^0'=ret_max24^post4, ret_min14^0'=ret_min14^post4, tmp620^0'=tmp620^post4, tmp923^0'=tmp923^post4, tmp9^0'=tmp9^post4, tmp^0'=tmp^post4, tmp___0^0'=tmp___0^post4, tmp___1^0'=tmp___1^post4, x_promoted_1^0'=x_promoted_1^post4, y_promoted_2^0'=y_promoted_2^post4, z^0'=z^post4, (0 == 0 /\ b11^0-b11^post4 == 0 /\ -tmp___0^post4+tmp___0^0 == 0 /\ ret_min14^0-ret_min14^post4 == 0 /\ -tmp923^post4+tmp923^0 == 0 /\ -ret_max24^post4+ret_max24^0 == 0 /\ __const_10^0-__const_10^post4 == 0 /\ -z^post4+z^0 == 0 /\ -a15^post4+a15^0 == 0 /\ -tmp^post4+tmp^0 == 0 /\ -b16^post4+b16^0 == 0 /\ tmp620^0-tmp620^post4 == 0 /\ -y_promoted_2^0+x_promoted_1^0 <= 0 /\ c17^0-c17^post4 == 0 /\ -tmp___1^post4+tmp___1^0 == 0 /\ -y_promoted_2^post4+y_promoted_2^0 == 0 /\ -a10^post4+a10^0 == 0 /\ -c12^post4+c12^0 == 0 /\ m13^0-m13^post4 == 0 /\ x_promoted_1^0-x_promoted_1^post4 == 0), cost: 1 New rule: l4 -> l3 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^post4, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, (0 == 0 /\ -y_promoted_2^0+x_promoted_1^0 <= 0), cost: 1 propagated equality b11^post4 = b11^0 propagated equality tmp___0^post4 = tmp___0^0 propagated equality ret_min14^post4 = ret_min14^0 propagated equality tmp923^post4 = tmp923^0 propagated equality ret_max24^post4 = ret_max24^0 propagated equality __const_10^post4 = __const_10^0 propagated equality z^post4 = z^0 propagated equality a15^post4 = a15^0 propagated equality tmp^post4 = tmp^0 propagated equality b16^post4 = b16^0 propagated equality tmp620^post4 = tmp620^0 propagated equality c17^post4 = c17^0 propagated equality tmp___1^post4 = tmp___1^0 propagated equality y_promoted_2^post4 = y_promoted_2^0 propagated equality a10^post4 = a10^0 propagated equality c12^post4 = c12^0 propagated equality m13^post4 = m13^0 propagated equality x_promoted_1^post4 = x_promoted_1^0 Simplified Guard Original rule: l4 -> l3 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^post4, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, (0 == 0 /\ -y_promoted_2^0+x_promoted_1^0 <= 0), cost: 1 New rule: l4 -> l3 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^post4, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, -y_promoted_2^0+x_promoted_1^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l4 -> l3 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^post4, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, -y_promoted_2^0+x_promoted_1^0 <= 0, cost: 1 New rule: l4 -> l3 : tmp9^0'=tmp9^post4, -y_promoted_2^0+x_promoted_1^0 <= 0, cost: 1 Propagated Equalities Original rule: l6 -> l2 : __const_10^0'=__const_10^post5, a10^0'=a10^post5, a15^0'=a15^post5, b11^0'=b11^post5, b16^0'=b16^post5, c12^0'=c12^post5, c17^0'=c17^post5, m13^0'=m13^post5, ret_max24^0'=ret_max24^post5, ret_min14^0'=ret_min14^post5, tmp620^0'=tmp620^post5, tmp923^0'=tmp923^post5, tmp9^0'=tmp9^post5, tmp^0'=tmp^post5, tmp___0^0'=tmp___0^post5, tmp___1^0'=tmp___1^post5, x_promoted_1^0'=x_promoted_1^post5, y_promoted_2^0'=y_promoted_2^post5, z^0'=z^post5, (-x_promoted_1^post5+x_promoted_1^0 == 0 /\ -z^post5+z^0 == 0 /\ b11^0-b11^post5 == 0 /\ ret_min14^0-ret_min14^post5 == 0 /\ 1+c17^0-a15^0 <= 0 /\ -tmp___1^post5+tmp___1^0 == 0 /\ tmp9^0-tmp9^post5 == 0 /\ __const_10^0-__const_10^post5 == 0 /\ -tmp___0^post5+tmp___0^0 == 0 /\ y_promoted_2^0-y_promoted_2^post5 == 0 /\ -b16^post5+b16^0 == 0 /\ -tmp923^post5+tmp923^0 == 0 /\ -a15^post5+a15^0 == 0 /\ -c12^post5+c12^0 == 0 /\ -ret_max24^post5+ret_max24^0 == 0 /\ -tmp^post5+tmp^0 == 0 /\ -tmp620^post5+tmp620^0 == 0 /\ m13^0-m13^post5 == 0 /\ c17^0-c17^post5 == 0 /\ -a10^post5+a10^0 == 0), cost: 1 New rule: l6 -> l2 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, (0 == 0 /\ 1+c17^0-a15^0 <= 0), cost: 1 propagated equality x_promoted_1^post5 = x_promoted_1^0 propagated equality z^post5 = z^0 propagated equality b11^post5 = b11^0 propagated equality ret_min14^post5 = ret_min14^0 propagated equality tmp___1^post5 = tmp___1^0 propagated equality tmp9^post5 = tmp9^0 propagated equality __const_10^post5 = __const_10^0 propagated equality tmp___0^post5 = tmp___0^0 propagated equality y_promoted_2^post5 = y_promoted_2^0 propagated equality b16^post5 = b16^0 propagated equality tmp923^post5 = tmp923^0 propagated equality a15^post5 = a15^0 propagated equality c12^post5 = c12^0 propagated equality ret_max24^post5 = ret_max24^0 propagated equality tmp^post5 = tmp^0 propagated equality tmp620^post5 = tmp620^0 propagated equality m13^post5 = m13^0 propagated equality c17^post5 = c17^0 propagated equality a10^post5 = a10^0 Simplified Guard Original rule: l6 -> l2 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, (0 == 0 /\ 1+c17^0-a15^0 <= 0), cost: 1 New rule: l6 -> l2 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, 1+c17^0-a15^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l6 -> l2 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, 1+c17^0-a15^0 <= 0, cost: 1 New rule: l6 -> l2 : 1+c17^0-a15^0 <= 0, cost: 1 Propagated Equalities Original rule: l6 -> l2 : __const_10^0'=__const_10^post6, a10^0'=a10^post6, a15^0'=a15^post6, b11^0'=b11^post6, b16^0'=b16^post6, c12^0'=c12^post6, c17^0'=c17^post6, m13^0'=m13^post6, ret_max24^0'=ret_max24^post6, ret_min14^0'=ret_min14^post6, tmp620^0'=tmp620^post6, tmp923^0'=tmp923^post6, tmp9^0'=tmp9^post6, tmp^0'=tmp^post6, tmp___0^0'=tmp___0^post6, tmp___1^0'=tmp___1^post6, x_promoted_1^0'=x_promoted_1^post6, y_promoted_2^0'=y_promoted_2^post6, z^0'=z^post6, (0 == 0 /\ -tmp___1^post6+tmp___1^0 == 0 /\ -x_promoted_1^post6+x_promoted_1^0 == 0 /\ -z^post6+z^0 == 0 /\ __const_10^0-__const_10^post6 == 0 /\ tmp9^0-tmp9^post6 == 0 /\ c17^0-c17^post6 == 0 /\ -tmp___0^post6+tmp___0^0 == 0 /\ -ret_max24^post6+ret_max24^0 == 0 /\ -c17^0+a15^0 <= 0 /\ m13^0-m13^post6 == 0 /\ y_promoted_2^0-y_promoted_2^post6 == 0 /\ b16^0-b16^post6 == 0 /\ -a10^post6+a10^0 == 0 /\ -a15^post6+a15^0 == 0 /\ -tmp^post6+tmp^0 == 0 /\ b11^0-b11^post6 == 0 /\ -c12^post6+c12^0 == 0 /\ ret_min14^0-ret_min14^post6 == 0 /\ -tmp620^post6+tmp620^0 == 0), cost: 1 New rule: l6 -> l2 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^post6, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, (0 == 0 /\ -c17^0+a15^0 <= 0), cost: 1 propagated equality tmp___1^post6 = tmp___1^0 propagated equality x_promoted_1^post6 = x_promoted_1^0 propagated equality z^post6 = z^0 propagated equality __const_10^post6 = __const_10^0 propagated equality tmp9^post6 = tmp9^0 propagated equality c17^post6 = c17^0 propagated equality tmp___0^post6 = tmp___0^0 propagated equality ret_max24^post6 = ret_max24^0 propagated equality m13^post6 = m13^0 propagated equality y_promoted_2^post6 = y_promoted_2^0 propagated equality b16^post6 = b16^0 propagated equality a10^post6 = a10^0 propagated equality a15^post6 = a15^0 propagated equality tmp^post6 = tmp^0 propagated equality b11^post6 = b11^0 propagated equality c12^post6 = c12^0 propagated equality ret_min14^post6 = ret_min14^0 propagated equality tmp620^post6 = tmp620^0 Simplified Guard Original rule: l6 -> l2 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^post6, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, (0 == 0 /\ -c17^0+a15^0 <= 0), cost: 1 New rule: l6 -> l2 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^post6, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, -c17^0+a15^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l6 -> l2 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^post6, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, -c17^0+a15^0 <= 0, cost: 1 New rule: l6 -> l2 : tmp923^0'=tmp923^post6, -c17^0+a15^0 <= 0, cost: 1 Propagated Equalities Original rule: l7 -> l6 : __const_10^0'=__const_10^post7, a10^0'=a10^post7, a15^0'=a15^post7, b11^0'=b11^post7, b16^0'=b16^post7, c12^0'=c12^post7, c17^0'=c17^post7, m13^0'=m13^post7, ret_max24^0'=ret_max24^post7, ret_min14^0'=ret_min14^post7, tmp620^0'=tmp620^post7, tmp923^0'=tmp923^post7, tmp9^0'=tmp9^post7, tmp^0'=tmp^post7, tmp___0^0'=tmp___0^post7, tmp___1^0'=tmp___1^post7, x_promoted_1^0'=x_promoted_1^post7, y_promoted_2^0'=y_promoted_2^post7, z^0'=z^post7, (-ret_max24^post7+ret_max24^0 == 0 /\ -m13^post7+m13^0 == 0 /\ -y_promoted_2^post7+y_promoted_2^0 == 0 /\ __const_10^0-__const_10^post7 == 0 /\ -tmp___1^post7+tmp___1^0 == 0 /\ -c12^post7+c12^0 == 0 /\ -z^post7+z^0 == 0 /\ 1+b16^0-a15^0 <= 0 /\ ret_min14^0-ret_min14^post7 == 0 /\ -b16^post7+b16^0 == 0 /\ -tmp___0^post7+tmp___0^0 == 0 /\ -tmp923^post7+tmp923^0 == 0 /\ c17^0-c17^post7 == 0 /\ tmp9^0-tmp9^post7 == 0 /\ -tmp^post7+tmp^0 == 0 /\ -a15^post7+a15^0 == 0 /\ b11^0-b11^post7 == 0 /\ -a10^post7+a10^0 == 0 /\ x_promoted_1^0-x_promoted_1^post7 == 0 /\ tmp620^0-tmp620^post7 == 0), cost: 1 New rule: l7 -> l6 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, (0 == 0 /\ 1+b16^0-a15^0 <= 0), cost: 1 propagated equality ret_max24^post7 = ret_max24^0 propagated equality m13^post7 = m13^0 propagated equality y_promoted_2^post7 = y_promoted_2^0 propagated equality __const_10^post7 = __const_10^0 propagated equality tmp___1^post7 = tmp___1^0 propagated equality c12^post7 = c12^0 propagated equality z^post7 = z^0 propagated equality ret_min14^post7 = ret_min14^0 propagated equality b16^post7 = b16^0 propagated equality tmp___0^post7 = tmp___0^0 propagated equality tmp923^post7 = tmp923^0 propagated equality c17^post7 = c17^0 propagated equality tmp9^post7 = tmp9^0 propagated equality tmp^post7 = tmp^0 propagated equality a15^post7 = a15^0 propagated equality b11^post7 = b11^0 propagated equality a10^post7 = a10^0 propagated equality x_promoted_1^post7 = x_promoted_1^0 propagated equality tmp620^post7 = tmp620^0 Simplified Guard Original rule: l7 -> l6 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, (0 == 0 /\ 1+b16^0-a15^0 <= 0), cost: 1 New rule: l7 -> l6 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, 1+b16^0-a15^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l7 -> l6 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, 1+b16^0-a15^0 <= 0, cost: 1 New rule: l7 -> l6 : 1+b16^0-a15^0 <= 0, cost: 1 Propagated Equalities Original rule: l7 -> l6 : __const_10^0'=__const_10^post8, a10^0'=a10^post8, a15^0'=a15^post8, b11^0'=b11^post8, b16^0'=b16^post8, c12^0'=c12^post8, c17^0'=c17^post8, m13^0'=m13^post8, ret_max24^0'=ret_max24^post8, ret_min14^0'=ret_min14^post8, tmp620^0'=tmp620^post8, tmp923^0'=tmp923^post8, tmp9^0'=tmp9^post8, tmp^0'=tmp^post8, tmp___0^0'=tmp___0^post8, tmp___1^0'=tmp___1^post8, x_promoted_1^0'=x_promoted_1^post8, y_promoted_2^0'=y_promoted_2^post8, z^0'=z^post8, (0 == 0 /\ y_promoted_2^0-y_promoted_2^post8 == 0 /\ -tmp___1^post8+tmp___1^0 == 0 /\ -a15^post8+a15^0 == 0 /\ ret_min14^0-ret_min14^post8 == 0 /\ -a10^post8+a10^0 == 0 /\ -b16^post8+b16^0 == 0 /\ -z^post8+z^0 == 0 /\ -ret_max24^post8+ret_max24^0 == 0 /\ -tmp923^post8+tmp923^0 == 0 /\ -tmp___0^post8+tmp___0^0 == 0 /\ -b16^0+a15^0 <= 0 /\ -tmp^post8+tmp^0 == 0 /\ __const_10^0-__const_10^post8 == 0 /\ c17^0-c17^post8 == 0 /\ tmp9^0-tmp9^post8 == 0 /\ x_promoted_1^0-x_promoted_1^post8 == 0 /\ -c12^post8+c12^0 == 0 /\ m13^0-m13^post8 == 0 /\ b11^0-b11^post8 == 0), cost: 1 New rule: l7 -> l6 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^post8, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, (0 == 0 /\ -b16^0+a15^0 <= 0), cost: 1 propagated equality y_promoted_2^post8 = y_promoted_2^0 propagated equality tmp___1^post8 = tmp___1^0 propagated equality a15^post8 = a15^0 propagated equality ret_min14^post8 = ret_min14^0 propagated equality a10^post8 = a10^0 propagated equality b16^post8 = b16^0 propagated equality z^post8 = z^0 propagated equality ret_max24^post8 = ret_max24^0 propagated equality tmp923^post8 = tmp923^0 propagated equality tmp___0^post8 = tmp___0^0 propagated equality tmp^post8 = tmp^0 propagated equality __const_10^post8 = __const_10^0 propagated equality c17^post8 = c17^0 propagated equality tmp9^post8 = tmp9^0 propagated equality x_promoted_1^post8 = x_promoted_1^0 propagated equality c12^post8 = c12^0 propagated equality m13^post8 = m13^0 propagated equality b11^post8 = b11^0 Simplified Guard Original rule: l7 -> l6 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^post8, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, (0 == 0 /\ -b16^0+a15^0 <= 0), cost: 1 New rule: l7 -> l6 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^post8, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, -b16^0+a15^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l7 -> l6 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^post8, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, -b16^0+a15^0 <= 0, cost: 1 New rule: l7 -> l6 : tmp620^0'=tmp620^post8, -b16^0+a15^0 <= 0, cost: 1 Propagated Equalities Original rule: l8 -> l9 : __const_10^0'=__const_10^post9, a10^0'=a10^post9, a15^0'=a15^post9, b11^0'=b11^post9, b16^0'=b16^post9, c12^0'=c12^post9, c17^0'=c17^post9, m13^0'=m13^post9, ret_max24^0'=ret_max24^post9, ret_min14^0'=ret_min14^post9, tmp620^0'=tmp620^post9, tmp923^0'=tmp923^post9, tmp9^0'=tmp9^post9, tmp^0'=tmp^post9, tmp___0^0'=tmp___0^post9, tmp___1^0'=tmp___1^post9, x_promoted_1^0'=x_promoted_1^post9, y_promoted_2^0'=y_promoted_2^post9, z^0'=z^post9, (y_promoted_2^0-y_promoted_2^post9 == 0 /\ m13^post9-c12^0 == 0 /\ c17^0-c17^post9 == 0 /\ tmp___0^0-tmp___0^post9 == 0 /\ -tmp923^post9+tmp923^0 == 0 /\ -ret_max24^post9+ret_max24^0 == 0 /\ -z^post9+z^0 == 0 /\ -x_promoted_1^post9+x_promoted_1^0 == 0 /\ -a15^post9+a15^0 == 0 /\ -__const_10^post9+__const_10^0 == 0 /\ -tmp620^post9+tmp620^0 == 0 /\ b16^0-b16^post9 == 0 /\ b11^0-b11^post9 == 0 /\ ret_min14^0-ret_min14^post9 == 0 /\ 1-b11^0+c12^0 <= 0 /\ tmp9^0-tmp9^post9 == 0 /\ -tmp___1^post9+tmp___1^0 == 0 /\ a10^0-a10^post9 == 0 /\ -c12^post9+c12^0 == 0 /\ -tmp^post9+tmp^0 == 0), cost: 1 New rule: l8 -> l9 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=c12^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, (0 == 0 /\ 1-b11^0+c12^0 <= 0), cost: 1 propagated equality y_promoted_2^post9 = y_promoted_2^0 propagated equality m13^post9 = c12^0 propagated equality c17^post9 = c17^0 propagated equality tmp___0^post9 = tmp___0^0 propagated equality tmp923^post9 = tmp923^0 propagated equality ret_max24^post9 = ret_max24^0 propagated equality z^post9 = z^0 propagated equality x_promoted_1^post9 = x_promoted_1^0 propagated equality a15^post9 = a15^0 propagated equality __const_10^post9 = __const_10^0 propagated equality tmp620^post9 = tmp620^0 propagated equality b16^post9 = b16^0 propagated equality b11^post9 = b11^0 propagated equality ret_min14^post9 = ret_min14^0 propagated equality tmp9^post9 = tmp9^0 propagated equality tmp___1^post9 = tmp___1^0 propagated equality a10^post9 = a10^0 propagated equality c12^post9 = c12^0 propagated equality tmp^post9 = tmp^0 Simplified Guard Original rule: l8 -> l9 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=c12^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, (0 == 0 /\ 1-b11^0+c12^0 <= 0), cost: 1 New rule: l8 -> l9 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=c12^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, 1-b11^0+c12^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l8 -> l9 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=c12^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, 1-b11^0+c12^0 <= 0, cost: 1 New rule: l8 -> l9 : m13^0'=c12^0, 1-b11^0+c12^0 <= 0, cost: 1 Propagated Equalities Original rule: l8 -> l9 : __const_10^0'=__const_10^post10, a10^0'=a10^post10, a15^0'=a15^post10, b11^0'=b11^post10, b16^0'=b16^post10, c12^0'=c12^post10, c17^0'=c17^post10, m13^0'=m13^post10, ret_max24^0'=ret_max24^post10, ret_min14^0'=ret_min14^post10, tmp620^0'=tmp620^post10, tmp923^0'=tmp923^post10, tmp9^0'=tmp9^post10, tmp^0'=tmp^post10, tmp___0^0'=tmp___0^post10, tmp___1^0'=tmp___1^post10, x_promoted_1^0'=x_promoted_1^post10, y_promoted_2^0'=y_promoted_2^post10, z^0'=z^post10, (-tmp___0^post10+tmp___0^0 == 0 /\ c17^0-c17^post10 == 0 /\ -tmp620^post10+tmp620^0 == 0 /\ -tmp^post10+tmp^0 == 0 /\ -z^post10+z^0 == 0 /\ -a15^post10+a15^0 == 0 /\ b16^0-b16^post10 == 0 /\ -__const_10^post10+__const_10^0 == 0 /\ ret_min14^0-ret_min14^post10 == 0 /\ tmp9^0-tmp9^post10 == 0 /\ b11^0-b11^post10 == 0 /\ -c12^post10+c12^0 == 0 /\ -ret_max24^post10+ret_max24^0 == 0 /\ -tmp923^post10+tmp923^0 == 0 /\ m13^post10-b11^0 == 0 /\ -tmp___1^post10+tmp___1^0 == 0 /\ -y_promoted_2^post10+y_promoted_2^0 == 0 /\ x_promoted_1^0-x_promoted_1^post10 == 0 /\ a10^0-a10^post10 == 0 /\ b11^0-c12^0 <= 0), cost: 1 New rule: l8 -> l9 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=b11^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, (0 == 0 /\ b11^0-c12^0 <= 0), cost: 1 propagated equality tmp___0^post10 = tmp___0^0 propagated equality c17^post10 = c17^0 propagated equality tmp620^post10 = tmp620^0 propagated equality tmp^post10 = tmp^0 propagated equality z^post10 = z^0 propagated equality a15^post10 = a15^0 propagated equality b16^post10 = b16^0 propagated equality __const_10^post10 = __const_10^0 propagated equality ret_min14^post10 = ret_min14^0 propagated equality tmp9^post10 = tmp9^0 propagated equality b11^post10 = b11^0 propagated equality c12^post10 = c12^0 propagated equality ret_max24^post10 = ret_max24^0 propagated equality tmp923^post10 = tmp923^0 propagated equality m13^post10 = b11^0 propagated equality tmp___1^post10 = tmp___1^0 propagated equality y_promoted_2^post10 = y_promoted_2^0 propagated equality x_promoted_1^post10 = x_promoted_1^0 propagated equality a10^post10 = a10^0 Simplified Guard Original rule: l8 -> l9 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=b11^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, (0 == 0 /\ b11^0-c12^0 <= 0), cost: 1 New rule: l8 -> l9 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=b11^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, b11^0-c12^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l8 -> l9 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=b11^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, b11^0-c12^0 <= 0, cost: 1 New rule: l8 -> l9 : m13^0'=b11^0, b11^0-c12^0 <= 0, cost: 1 Propagated Equalities Original rule: l9 -> l3 : __const_10^0'=__const_10^post11, a10^0'=a10^post11, a15^0'=a15^post11, b11^0'=b11^post11, b16^0'=b16^post11, c12^0'=c12^post11, c17^0'=c17^post11, m13^0'=m13^post11, ret_max24^0'=ret_max24^post11, ret_min14^0'=ret_min14^post11, tmp620^0'=tmp620^post11, tmp923^0'=tmp923^post11, tmp9^0'=tmp9^post11, tmp^0'=tmp^post11, tmp___0^0'=tmp___0^post11, tmp___1^0'=tmp___1^post11, x_promoted_1^0'=x_promoted_1^post11, y_promoted_2^0'=y_promoted_2^post11, z^0'=z^post11, (b11^0-b11^post11 == 0 /\ -m13^0+ret_min14^post11 == 0 /\ -tmp___0^post11+tmp___0^0 == 0 /\ -ret_max24^post11+ret_max24^0 == 0 /\ -ret_min14^post11+tmp^post11 == 0 /\ __const_10^0-__const_10^post11 == 0 /\ -b16^post11+b16^0 == 0 /\ -a15^post11+a15^0 == 0 /\ -z^post11+z^0 == 0 /\ -x_promoted_1^0+x_promoted_1^post11-tmp^post11 == 0 /\ tmp9^0-tmp9^post11 == 0 /\ c17^0-c17^post11 == 0 /\ -tmp923^post11+tmp923^0 == 0 /\ tmp620^0-tmp620^post11 == 0 /\ -tmp___1^post11+tmp___1^0 == 0 /\ m13^0-m13^post11 == 0 /\ -c12^post11+c12^0 == 0 /\ -a10^post11+a10^0 == 0 /\ -y_promoted_2^post11+y_promoted_2^0 == 0), cost: 1 New rule: l9 -> l3 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=m13^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=m13^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=m13^0+x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, 0 == 0, cost: 1 propagated equality b11^post11 = b11^0 propagated equality ret_min14^post11 = m13^0 propagated equality tmp___0^post11 = tmp___0^0 propagated equality ret_max24^post11 = ret_max24^0 propagated equality tmp^post11 = m13^0 propagated equality __const_10^post11 = __const_10^0 propagated equality b16^post11 = b16^0 propagated equality a15^post11 = a15^0 propagated equality z^post11 = z^0 propagated equality x_promoted_1^post11 = m13^0+x_promoted_1^0 propagated equality tmp9^post11 = tmp9^0 propagated equality c17^post11 = c17^0 propagated equality tmp923^post11 = tmp923^0 propagated equality tmp620^post11 = tmp620^0 propagated equality tmp___1^post11 = tmp___1^0 propagated equality m13^post11 = m13^0 propagated equality c12^post11 = c12^0 propagated equality a10^post11 = a10^0 propagated equality y_promoted_2^post11 = y_promoted_2^0 Simplified Guard Original rule: l9 -> l3 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=m13^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=m13^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=m13^0+x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, 0 == 0, cost: 1 New rule: l9 -> l3 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=m13^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=m13^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=m13^0+x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, T, cost: 1 Removed Trivial Updates Original rule: l9 -> l3 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=m13^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=m13^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=m13^0+x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, T, cost: 1 New rule: l9 -> l3 : ret_min14^0'=m13^0, tmp^0'=m13^0, x_promoted_1^0'=m13^0+x_promoted_1^0, T, cost: 1 Propagated Equalities Original rule: l10 -> l9 : __const_10^0'=__const_10^post12, a10^0'=a10^post12, a15^0'=a15^post12, b11^0'=b11^post12, b16^0'=b16^post12, c12^0'=c12^post12, c17^0'=c17^post12, m13^0'=m13^post12, ret_max24^0'=ret_max24^post12, ret_min14^0'=ret_min14^post12, tmp620^0'=tmp620^post12, tmp923^0'=tmp923^post12, tmp9^0'=tmp9^post12, tmp^0'=tmp^post12, tmp___0^0'=tmp___0^post12, tmp___1^0'=tmp___1^post12, x_promoted_1^0'=x_promoted_1^post12, y_promoted_2^0'=y_promoted_2^post12, z^0'=z^post12, (m13^post12-c12^0 == 0 /\ ret_max24^0-ret_max24^post12 == 0 /\ b16^0-b16^post12 == 0 /\ b11^0-b11^post12 == 0 /\ -x_promoted_1^post12+x_promoted_1^0 == 0 /\ tmp___1^0-tmp___1^post12 == 0 /\ -c17^post12+c17^0 == 0 /\ __const_10^0-__const_10^post12 == 0 /\ -tmp9^post12+tmp9^0 == 0 /\ -tmp923^post12+tmp923^0 == 0 /\ -tmp^post12+tmp^0 == 0 /\ -a15^post12+a15^0 == 0 /\ -tmp620^post12+tmp620^0 == 0 /\ 1-a10^0+c12^0 <= 0 /\ tmp___0^0-tmp___0^post12 == 0 /\ -ret_min14^post12+ret_min14^0 == 0 /\ y_promoted_2^0-y_promoted_2^post12 == 0 /\ c12^0-c12^post12 == 0 /\ -a10^post12+a10^0 == 0 /\ z^0-z^post12 == 0), cost: 1 New rule: l10 -> l9 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=c12^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, (0 == 0 /\ 1-a10^0+c12^0 <= 0), cost: 1 propagated equality m13^post12 = c12^0 propagated equality ret_max24^post12 = ret_max24^0 propagated equality b16^post12 = b16^0 propagated equality b11^post12 = b11^0 propagated equality x_promoted_1^post12 = x_promoted_1^0 propagated equality tmp___1^post12 = tmp___1^0 propagated equality c17^post12 = c17^0 propagated equality __const_10^post12 = __const_10^0 propagated equality tmp9^post12 = tmp9^0 propagated equality tmp923^post12 = tmp923^0 propagated equality tmp^post12 = tmp^0 propagated equality a15^post12 = a15^0 propagated equality tmp620^post12 = tmp620^0 propagated equality tmp___0^post12 = tmp___0^0 propagated equality ret_min14^post12 = ret_min14^0 propagated equality y_promoted_2^post12 = y_promoted_2^0 propagated equality c12^post12 = c12^0 propagated equality a10^post12 = a10^0 propagated equality z^post12 = z^0 Simplified Guard Original rule: l10 -> l9 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=c12^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, (0 == 0 /\ 1-a10^0+c12^0 <= 0), cost: 1 New rule: l10 -> l9 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=c12^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, 1-a10^0+c12^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l10 -> l9 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=c12^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, 1-a10^0+c12^0 <= 0, cost: 1 New rule: l10 -> l9 : m13^0'=c12^0, 1-a10^0+c12^0 <= 0, cost: 1 Propagated Equalities Original rule: l10 -> l9 : __const_10^0'=__const_10^post13, a10^0'=a10^post13, a15^0'=a15^post13, b11^0'=b11^post13, b16^0'=b16^post13, c12^0'=c12^post13, c17^0'=c17^post13, m13^0'=m13^post13, ret_max24^0'=ret_max24^post13, ret_min14^0'=ret_min14^post13, tmp620^0'=tmp620^post13, tmp923^0'=tmp923^post13, tmp9^0'=tmp9^post13, tmp^0'=tmp^post13, tmp___0^0'=tmp___0^post13, tmp___1^0'=tmp___1^post13, x_promoted_1^0'=x_promoted_1^post13, y_promoted_2^0'=y_promoted_2^post13, z^0'=z^post13, (ret_max24^0-ret_max24^post13 == 0 /\ a15^0-a15^post13 == 0 /\ -tmp923^post13+tmp923^0 == 0 /\ -z^post13+z^0 == 0 /\ tmp9^0-tmp9^post13 == 0 /\ -c17^post13+c17^0 == 0 /\ -tmp___1^post13+tmp___1^0 == 0 /\ -tmp620^post13+tmp620^0 == 0 /\ a10^0-a10^post13 == 0 /\ c12^0-c12^post13 == 0 /\ y_promoted_2^0-y_promoted_2^post13 == 0 /\ -__const_10^post13+__const_10^0 == 0 /\ -x_promoted_1^post13+x_promoted_1^0 == 0 /\ a10^0-c12^0 <= 0 /\ -ret_min14^post13+ret_min14^0 == 0 /\ tmp___0^0-tmp___0^post13 == 0 /\ -a10^0+m13^post13 == 0 /\ -tmp^post13+tmp^0 == 0 /\ -b11^post13+b11^0 == 0 /\ b16^0-b16^post13 == 0), cost: 1 New rule: l10 -> l9 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=a10^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, (0 == 0 /\ a10^0-c12^0 <= 0), cost: 1 propagated equality ret_max24^post13 = ret_max24^0 propagated equality a15^post13 = a15^0 propagated equality tmp923^post13 = tmp923^0 propagated equality z^post13 = z^0 propagated equality tmp9^post13 = tmp9^0 propagated equality c17^post13 = c17^0 propagated equality tmp___1^post13 = tmp___1^0 propagated equality tmp620^post13 = tmp620^0 propagated equality a10^post13 = a10^0 propagated equality c12^post13 = c12^0 propagated equality y_promoted_2^post13 = y_promoted_2^0 propagated equality __const_10^post13 = __const_10^0 propagated equality x_promoted_1^post13 = x_promoted_1^0 propagated equality ret_min14^post13 = ret_min14^0 propagated equality tmp___0^post13 = tmp___0^0 propagated equality m13^post13 = a10^0 propagated equality tmp^post13 = tmp^0 propagated equality b11^post13 = b11^0 propagated equality b16^post13 = b16^0 Simplified Guard Original rule: l10 -> l9 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=a10^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, (0 == 0 /\ a10^0-c12^0 <= 0), cost: 1 New rule: l10 -> l9 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=a10^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, a10^0-c12^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l10 -> l9 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=a10^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, a10^0-c12^0 <= 0, cost: 1 New rule: l10 -> l9 : m13^0'=a10^0, a10^0-c12^0 <= 0, cost: 1 Propagated Equalities Original rule: l11 -> l8 : __const_10^0'=__const_10^post14, a10^0'=a10^post14, a15^0'=a15^post14, b11^0'=b11^post14, b16^0'=b16^post14, c12^0'=c12^post14, c17^0'=c17^post14, m13^0'=m13^post14, ret_max24^0'=ret_max24^post14, ret_min14^0'=ret_min14^post14, tmp620^0'=tmp620^post14, tmp923^0'=tmp923^post14, tmp9^0'=tmp9^post14, tmp^0'=tmp^post14, tmp___0^0'=tmp___0^post14, tmp___1^0'=tmp___1^post14, x_promoted_1^0'=x_promoted_1^post14, y_promoted_2^0'=y_promoted_2^post14, z^0'=z^post14, (y_promoted_2^0-y_promoted_2^post14 == 0 /\ 1-a10^0+b11^0 <= 0 /\ c17^0-c17^post14 == 0 /\ tmp9^0-tmp9^post14 == 0 /\ -__const_10^post14+__const_10^0 == 0 /\ -ret_max24^post14+ret_max24^0 == 0 /\ -tmp923^post14+tmp923^0 == 0 /\ -z^post14+z^0 == 0 /\ -x_promoted_1^post14+x_promoted_1^0 == 0 /\ -a15^post14+a15^0 == 0 /\ m13^0-m13^post14 == 0 /\ b16^0-b16^post14 == 0 /\ -tmp___0^post14+tmp___0^0 == 0 /\ -tmp620^post14+tmp620^0 == 0 /\ b11^0-b11^post14 == 0 /\ -tmp^post14+tmp^0 == 0 /\ ret_min14^0-ret_min14^post14 == 0 /\ -c12^post14+c12^0 == 0 /\ -tmp___1^post14+tmp___1^0 == 0 /\ a10^0-a10^post14 == 0), cost: 1 New rule: l11 -> l8 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, (0 == 0 /\ 1-a10^0+b11^0 <= 0), cost: 1 propagated equality y_promoted_2^post14 = y_promoted_2^0 propagated equality c17^post14 = c17^0 propagated equality tmp9^post14 = tmp9^0 propagated equality __const_10^post14 = __const_10^0 propagated equality ret_max24^post14 = ret_max24^0 propagated equality tmp923^post14 = tmp923^0 propagated equality z^post14 = z^0 propagated equality x_promoted_1^post14 = x_promoted_1^0 propagated equality a15^post14 = a15^0 propagated equality m13^post14 = m13^0 propagated equality b16^post14 = b16^0 propagated equality tmp___0^post14 = tmp___0^0 propagated equality tmp620^post14 = tmp620^0 propagated equality b11^post14 = b11^0 propagated equality tmp^post14 = tmp^0 propagated equality ret_min14^post14 = ret_min14^0 propagated equality c12^post14 = c12^0 propagated equality tmp___1^post14 = tmp___1^0 propagated equality a10^post14 = a10^0 Simplified Guard Original rule: l11 -> l8 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, (0 == 0 /\ 1-a10^0+b11^0 <= 0), cost: 1 New rule: l11 -> l8 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, 1-a10^0+b11^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l11 -> l8 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, 1-a10^0+b11^0 <= 0, cost: 1 New rule: l11 -> l8 : 1-a10^0+b11^0 <= 0, cost: 1 Propagated Equalities Original rule: l11 -> l10 : __const_10^0'=__const_10^post15, a10^0'=a10^post15, a15^0'=a15^post15, b11^0'=b11^post15, b16^0'=b16^post15, c12^0'=c12^post15, c17^0'=c17^post15, m13^0'=m13^post15, ret_max24^0'=ret_max24^post15, ret_min14^0'=ret_min14^post15, tmp620^0'=tmp620^post15, tmp923^0'=tmp923^post15, tmp9^0'=tmp9^post15, tmp^0'=tmp^post15, tmp___0^0'=tmp___0^post15, tmp___1^0'=tmp___1^post15, x_promoted_1^0'=x_promoted_1^post15, y_promoted_2^0'=y_promoted_2^post15, z^0'=z^post15, (-x_promoted_1^post15+x_promoted_1^0 == 0 /\ -tmp9^post15+tmp9^0 == 0 /\ c17^0-c17^post15 == 0 /\ -tmp923^post15+tmp923^0 == 0 /\ -tmp^post15+tmp^0 == 0 /\ a10^0-b11^0 <= 0 /\ -__const_10^post15+__const_10^0 == 0 /\ -ret_max24^post15+ret_max24^0 == 0 /\ -a15^post15+a15^0 == 0 /\ m13^0-m13^post15 == 0 /\ -tmp620^post15+tmp620^0 == 0 /\ b16^0-b16^post15 == 0 /\ z^0-z^post15 == 0 /\ b11^0-b11^post15 == 0 /\ ret_min14^0-ret_min14^post15 == 0 /\ tmp___0^0-tmp___0^post15 == 0 /\ -tmp___1^post15+tmp___1^0 == 0 /\ a10^0-a10^post15 == 0 /\ y_promoted_2^0-y_promoted_2^post15 == 0 /\ -c12^post15+c12^0 == 0), cost: 1 New rule: l11 -> l10 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, (0 == 0 /\ a10^0-b11^0 <= 0), cost: 1 propagated equality x_promoted_1^post15 = x_promoted_1^0 propagated equality tmp9^post15 = tmp9^0 propagated equality c17^post15 = c17^0 propagated equality tmp923^post15 = tmp923^0 propagated equality tmp^post15 = tmp^0 propagated equality __const_10^post15 = __const_10^0 propagated equality ret_max24^post15 = ret_max24^0 propagated equality a15^post15 = a15^0 propagated equality m13^post15 = m13^0 propagated equality tmp620^post15 = tmp620^0 propagated equality b16^post15 = b16^0 propagated equality z^post15 = z^0 propagated equality b11^post15 = b11^0 propagated equality ret_min14^post15 = ret_min14^0 propagated equality tmp___0^post15 = tmp___0^0 propagated equality tmp___1^post15 = tmp___1^0 propagated equality a10^post15 = a10^0 propagated equality y_promoted_2^post15 = y_promoted_2^0 propagated equality c12^post15 = c12^0 Simplified Guard Original rule: l11 -> l10 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, (0 == 0 /\ a10^0-b11^0 <= 0), cost: 1 New rule: l11 -> l10 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, a10^0-b11^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l11 -> l10 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, a10^0-b11^0 <= 0, cost: 1 New rule: l11 -> l10 : a10^0-b11^0 <= 0, cost: 1 Propagated Equalities Original rule: l5 -> l7 : __const_10^0'=__const_10^post16, a10^0'=a10^post16, a15^0'=a15^post16, b11^0'=b11^post16, b16^0'=b16^post16, c12^0'=c12^post16, c17^0'=c17^post16, m13^0'=m13^post16, ret_max24^0'=ret_max24^post16, ret_min14^0'=ret_min14^post16, tmp620^0'=tmp620^post16, tmp923^0'=tmp923^post16, tmp9^0'=tmp9^post16, tmp^0'=tmp^post16, tmp___0^0'=tmp___0^post16, tmp___1^0'=tmp___1^post16, x_promoted_1^0'=x_promoted_1^post16, y_promoted_2^0'=y_promoted_2^post16, z^0'=z^post16, (-ret_min14^post16+ret_min14^0 == 0 /\ -x_promoted_1^post16+x_promoted_1^0 == 0 /\ c17^post16-x_promoted_1^0 == 0 /\ a10^0-a10^post16 == 0 /\ tmp___1^0-tmp___1^post16 == 0 /\ -y_promoted_2^0+b16^post16 == 0 /\ -tmp9^post16+tmp9^0 == 0 /\ -tmp923^post16+tmp923^0 == 0 /\ tmp___0^0-tmp___0^post16 == 0 /\ -b11^post16+b11^0 == 0 /\ -__const_10^post16+__const_10^0 == 0 /\ -ret_max24^post16+ret_max24^0 == 0 /\ z^0-z^post16 == 0 /\ 1-x_promoted_1^0+z^0 <= 0 /\ -tmp^post16+tmp^0 == 0 /\ -z^0+a15^post16 == 0 /\ m13^0-m13^post16 == 0 /\ -tmp620^post16+tmp620^0 == 0 /\ y_promoted_2^0-y_promoted_2^post16 == 0 /\ c12^0-c12^post16 == 0), cost: 1 New rule: l5 -> l7 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=z^0, b11^0'=b11^0, b16^0'=y_promoted_2^0, c12^0'=c12^0, c17^0'=x_promoted_1^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, (0 == 0 /\ 1-x_promoted_1^0+z^0 <= 0), cost: 1 propagated equality ret_min14^post16 = ret_min14^0 propagated equality x_promoted_1^post16 = x_promoted_1^0 propagated equality c17^post16 = x_promoted_1^0 propagated equality a10^post16 = a10^0 propagated equality tmp___1^post16 = tmp___1^0 propagated equality b16^post16 = y_promoted_2^0 propagated equality tmp9^post16 = tmp9^0 propagated equality tmp923^post16 = tmp923^0 propagated equality tmp___0^post16 = tmp___0^0 propagated equality b11^post16 = b11^0 propagated equality __const_10^post16 = __const_10^0 propagated equality ret_max24^post16 = ret_max24^0 propagated equality z^post16 = z^0 propagated equality tmp^post16 = tmp^0 propagated equality a15^post16 = z^0 propagated equality m13^post16 = m13^0 propagated equality tmp620^post16 = tmp620^0 propagated equality y_promoted_2^post16 = y_promoted_2^0 propagated equality c12^post16 = c12^0 Simplified Guard Original rule: l5 -> l7 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=z^0, b11^0'=b11^0, b16^0'=y_promoted_2^0, c12^0'=c12^0, c17^0'=x_promoted_1^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, (0 == 0 /\ 1-x_promoted_1^0+z^0 <= 0), cost: 1 New rule: l5 -> l7 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=z^0, b11^0'=b11^0, b16^0'=y_promoted_2^0, c12^0'=c12^0, c17^0'=x_promoted_1^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, 1-x_promoted_1^0+z^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l5 -> l7 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=z^0, b11^0'=b11^0, b16^0'=y_promoted_2^0, c12^0'=c12^0, c17^0'=x_promoted_1^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, 1-x_promoted_1^0+z^0 <= 0, cost: 1 New rule: l5 -> l7 : a15^0'=z^0, b16^0'=y_promoted_2^0, c17^0'=x_promoted_1^0, 1-x_promoted_1^0+z^0 <= 0, cost: 1 Propagated Equalities Original rule: l5 -> l11 : __const_10^0'=__const_10^post17, a10^0'=a10^post17, a15^0'=a15^post17, b11^0'=b11^post17, b16^0'=b16^post17, c12^0'=c12^post17, c17^0'=c17^post17, m13^0'=m13^post17, ret_max24^0'=ret_max24^post17, ret_min14^0'=ret_min14^post17, tmp620^0'=tmp620^post17, tmp923^0'=tmp923^post17, tmp9^0'=tmp9^post17, tmp^0'=tmp^post17, tmp___0^0'=tmp___0^post17, tmp___1^0'=tmp___1^post17, x_promoted_1^0'=x_promoted_1^post17, y_promoted_2^0'=y_promoted_2^post17, z^0'=z^post17, (-z^post17+z^0 == 0 /\ tmp___0^0-tmp___0^post17 == 0 /\ -ret_max24^post17+ret_max24^0 == 0 /\ tmp9^0-tmp9^post17 == 0 /\ c17^0-c17^post17 == 0 /\ -x_promoted_1^post17+x_promoted_1^0 == 0 /\ b16^0-b16^post17 == 0 /\ -tmp___1^post17+tmp___1^0 == 0 /\ -tmp^post17+tmp^0 == 0 /\ a10^post17-x_promoted_1^0 == 0 /\ y_promoted_2^0-y_promoted_2^post17 == 0 /\ m13^0-m13^post17 == 0 /\ -tmp923^post17+tmp923^0 == 0 /\ -__const_10^post17+__const_10^0 == 0 /\ b11^post17-y_promoted_2^0 == 0 /\ -a15^post17+a15^0 == 0 /\ -tmp620^post17+tmp620^0 == 0 /\ x_promoted_1^0-z^0 <= 0 /\ ret_min14^0-ret_min14^post17 == 0 /\ c12^post17-z^0 == 0), cost: 1 New rule: l5 -> l11 : __const_10^0'=__const_10^0, a10^0'=x_promoted_1^0, a15^0'=a15^0, b11^0'=y_promoted_2^0, b16^0'=b16^0, c12^0'=z^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, (0 == 0 /\ x_promoted_1^0-z^0 <= 0), cost: 1 propagated equality z^post17 = z^0 propagated equality tmp___0^post17 = tmp___0^0 propagated equality ret_max24^post17 = ret_max24^0 propagated equality tmp9^post17 = tmp9^0 propagated equality c17^post17 = c17^0 propagated equality x_promoted_1^post17 = x_promoted_1^0 propagated equality b16^post17 = b16^0 propagated equality tmp___1^post17 = tmp___1^0 propagated equality tmp^post17 = tmp^0 propagated equality a10^post17 = x_promoted_1^0 propagated equality y_promoted_2^post17 = y_promoted_2^0 propagated equality m13^post17 = m13^0 propagated equality tmp923^post17 = tmp923^0 propagated equality __const_10^post17 = __const_10^0 propagated equality b11^post17 = y_promoted_2^0 propagated equality a15^post17 = a15^0 propagated equality tmp620^post17 = tmp620^0 propagated equality ret_min14^post17 = ret_min14^0 propagated equality c12^post17 = z^0 Simplified Guard Original rule: l5 -> l11 : __const_10^0'=__const_10^0, a10^0'=x_promoted_1^0, a15^0'=a15^0, b11^0'=y_promoted_2^0, b16^0'=b16^0, c12^0'=z^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, (0 == 0 /\ x_promoted_1^0-z^0 <= 0), cost: 1 New rule: l5 -> l11 : __const_10^0'=__const_10^0, a10^0'=x_promoted_1^0, a15^0'=a15^0, b11^0'=y_promoted_2^0, b16^0'=b16^0, c12^0'=z^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, x_promoted_1^0-z^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l5 -> l11 : __const_10^0'=__const_10^0, a10^0'=x_promoted_1^0, a15^0'=a15^0, b11^0'=y_promoted_2^0, b16^0'=b16^0, c12^0'=z^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, x_promoted_1^0-z^0 <= 0, cost: 1 New rule: l5 -> l11 : a10^0'=x_promoted_1^0, b11^0'=y_promoted_2^0, c12^0'=z^0, x_promoted_1^0-z^0 <= 0, cost: 1 Propagated Equalities Original rule: l3 -> l0 : __const_10^0'=__const_10^post18, a10^0'=a10^post18, a15^0'=a15^post18, b11^0'=b11^post18, b16^0'=b16^post18, c12^0'=c12^post18, c17^0'=c17^post18, m13^0'=m13^post18, ret_max24^0'=ret_max24^post18, ret_min14^0'=ret_min14^post18, tmp620^0'=tmp620^post18, tmp923^0'=tmp923^post18, tmp9^0'=tmp9^post18, tmp^0'=tmp^post18, tmp___0^0'=tmp___0^post18, tmp___1^0'=tmp___1^post18, x_promoted_1^0'=x_promoted_1^post18, y_promoted_2^0'=y_promoted_2^post18, z^0'=z^post18, (c17^0-c17^post18 == 0 /\ -ret_max24^post18+ret_max24^0 == 0 /\ 1-y_promoted_2^0+z^0 <= 0 /\ -x_promoted_1^post18+x_promoted_1^0 == 0 /\ -c12^post18+c12^0 == 0 /\ -z^post18+z^0 == 0 /\ tmp9^0-tmp9^post18 == 0 /\ -b11^post18+b11^0 == 0 /\ __const_10^0-__const_10^post18 == 0 /\ -y_promoted_2^0+tmp___1^post18+z^0 == 0 /\ -tmp___0^post18+tmp___0^0 == 0 /\ b16^0-b16^post18 == 0 /\ y_promoted_2^0-y_promoted_2^post18 == 0 /\ -tmp923^post18+tmp923^0 == 0 /\ m13^0-m13^post18 == 0 /\ -a15^post18+a15^0 == 0 /\ -tmp620^post18+tmp620^0 == 0 /\ ret_min14^0-ret_min14^post18 == 0 /\ -tmp^post18+tmp^0 == 0 /\ a10^0-a10^post18 == 0), cost: 1 New rule: l3 -> l0 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=y_promoted_2^0-z^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, (0 == 0 /\ 1-y_promoted_2^0+z^0 <= 0), cost: 1 propagated equality c17^post18 = c17^0 propagated equality ret_max24^post18 = ret_max24^0 propagated equality x_promoted_1^post18 = x_promoted_1^0 propagated equality c12^post18 = c12^0 propagated equality z^post18 = z^0 propagated equality tmp9^post18 = tmp9^0 propagated equality b11^post18 = b11^0 propagated equality __const_10^post18 = __const_10^0 propagated equality tmp___1^post18 = y_promoted_2^0-z^0 propagated equality tmp___0^post18 = tmp___0^0 propagated equality b16^post18 = b16^0 propagated equality y_promoted_2^post18 = y_promoted_2^0 propagated equality tmp923^post18 = tmp923^0 propagated equality m13^post18 = m13^0 propagated equality a15^post18 = a15^0 propagated equality tmp620^post18 = tmp620^0 propagated equality ret_min14^post18 = ret_min14^0 propagated equality tmp^post18 = tmp^0 propagated equality a10^post18 = a10^0 Simplified Guard Original rule: l3 -> l0 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=y_promoted_2^0-z^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, (0 == 0 /\ 1-y_promoted_2^0+z^0 <= 0), cost: 1 New rule: l3 -> l0 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=y_promoted_2^0-z^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, 1-y_promoted_2^0+z^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l3 -> l0 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=y_promoted_2^0-z^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, 1-y_promoted_2^0+z^0 <= 0, cost: 1 New rule: l3 -> l0 : tmp___1^0'=y_promoted_2^0-z^0, 1-y_promoted_2^0+z^0 <= 0, cost: 1 Propagated Equalities Original rule: l3 -> l0 : __const_10^0'=__const_10^post19, a10^0'=a10^post19, a15^0'=a15^post19, b11^0'=b11^post19, b16^0'=b16^post19, c12^0'=c12^post19, c17^0'=c17^post19, m13^0'=m13^post19, ret_max24^0'=ret_max24^post19, ret_min14^0'=ret_min14^post19, tmp620^0'=tmp620^post19, tmp923^0'=tmp923^post19, tmp9^0'=tmp9^post19, tmp^0'=tmp^post19, tmp___0^0'=tmp___0^post19, tmp___1^0'=tmp___1^post19, x_promoted_1^0'=x_promoted_1^post19, y_promoted_2^0'=y_promoted_2^post19, z^0'=z^post19, (ret_max24^0-ret_max24^post19 == 0 /\ a15^0-a15^post19 == 0 /\ -__const_10^post19+__const_10^0 == 0 /\ -y_promoted_2^0-z^0+tmp___1^post19 == 0 /\ -tmp9^post19+tmp9^0 == 0 /\ y_promoted_2^0-z^0 <= 0 /\ -tmp923^post19+tmp923^0 == 0 /\ -x_promoted_1^post19+x_promoted_1^0 == 0 /\ -c17^post19+c17^0 == 0 /\ a10^0-a10^post19 == 0 /\ -tmp620^post19+tmp620^0 == 0 /\ y_promoted_2^0-y_promoted_2^post19 == 0 /\ -tmp^post19+tmp^0 == 0 /\ z^0-z^post19 == 0 /\ c12^0-c12^post19 == 0 /\ -ret_min14^post19+ret_min14^0 == 0 /\ -b11^post19+b11^0 == 0 /\ tmp___0^0-tmp___0^post19 == 0 /\ b16^0-b16^post19 == 0 /\ m13^0-m13^post19 == 0), cost: 1 New rule: l3 -> l0 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=y_promoted_2^0+z^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, (0 == 0 /\ y_promoted_2^0-z^0 <= 0), cost: 1 propagated equality ret_max24^post19 = ret_max24^0 propagated equality a15^post19 = a15^0 propagated equality __const_10^post19 = __const_10^0 propagated equality tmp___1^post19 = y_promoted_2^0+z^0 propagated equality tmp9^post19 = tmp9^0 propagated equality tmp923^post19 = tmp923^0 propagated equality x_promoted_1^post19 = x_promoted_1^0 propagated equality c17^post19 = c17^0 propagated equality a10^post19 = a10^0 propagated equality tmp620^post19 = tmp620^0 propagated equality y_promoted_2^post19 = y_promoted_2^0 propagated equality tmp^post19 = tmp^0 propagated equality z^post19 = z^0 propagated equality c12^post19 = c12^0 propagated equality ret_min14^post19 = ret_min14^0 propagated equality b11^post19 = b11^0 propagated equality tmp___0^post19 = tmp___0^0 propagated equality b16^post19 = b16^0 propagated equality m13^post19 = m13^0 Simplified Guard Original rule: l3 -> l0 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=y_promoted_2^0+z^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, (0 == 0 /\ y_promoted_2^0-z^0 <= 0), cost: 1 New rule: l3 -> l0 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=y_promoted_2^0+z^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, y_promoted_2^0-z^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l3 -> l0 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=y_promoted_2^0+z^0, x_promoted_1^0'=x_promoted_1^0, y_promoted_2^0'=y_promoted_2^0, z^0'=z^0, y_promoted_2^0-z^0 <= 0, cost: 1 New rule: l3 -> l0 : tmp___1^0'=y_promoted_2^0+z^0, y_promoted_2^0-z^0 <= 0, cost: 1 Propagated Equalities Original rule: l13 -> l4 : __const_10^0'=__const_10^post20, a10^0'=a10^post20, a15^0'=a15^post20, b11^0'=b11^post20, b16^0'=b16^post20, c12^0'=c12^post20, c17^0'=c17^post20, m13^0'=m13^post20, ret_max24^0'=ret_max24^post20, ret_min14^0'=ret_min14^post20, tmp620^0'=tmp620^post20, tmp923^0'=tmp923^post20, tmp9^0'=tmp9^post20, tmp^0'=tmp^post20, tmp___0^0'=tmp___0^post20, tmp___1^0'=tmp___1^post20, x_promoted_1^0'=x_promoted_1^post20, y_promoted_2^0'=y_promoted_2^post20, z^0'=z^post20, (a15^post21-a15^post20 == 0 /\ tmp923^post21-tmp923^post20 == 0 /\ tmp9^0-tmp9^post21 == 0 /\ -b11^post20+b11^post21 == 0 /\ y_promoted_2^0-y_promoted_2^post21 == 0 /\ tmp620^post21-tmp620^post20 == 0 /\ -2+y_promoted_2^post20 == 0 /\ c17^0-c17^post21 == 0 /\ tmp___0^0-tmp___0^post21 == 0 /\ a10^post21-a10^post20 == 0 /\ -__const_10^post21+x_promoted_1^post20 == 0 /\ m13^post21-m13^post20 == 0 /\ -a15^post21+a15^0 == 0 /\ -x_promoted_1^post21+x_promoted_1^0 == 0 /\ -__const_10^post21+__const_10^0 == 0 /\ -ret_max24^post21+ret_max24^0 == 0 /\ m13^0-m13^post21 == 0 /\ -tmp^post21+tmp^0 == 0 /\ -c17^post20+c17^post21 == 0 /\ -z^post21+z^0 == 0 /\ tmp___0^post21-tmp___0^post20 == 0 /\ b16^post21-b16^post20 == 0 /\ -1+z^post20 == 0 /\ b16^0-b16^post21 == 0 /\ b11^0-b11^post21 == 0 /\ tmp^post21-tmp^post20 == 0 /\ c12^post21-c12^post20 == 0 /\ ret_min14^0-ret_min14^post21 == 0 /\ -tmp923^post21+tmp923^0 == 0 /\ -ret_min14^post20+ret_min14^post21 == 0 /\ __const_10^post21-__const_10^post20 == 0 /\ tmp___1^post21-tmp___1^post20 == 0 /\ -tmp___1^post21+tmp___1^0 == 0 /\ ret_max24^post21-ret_max24^post20 == 0 /\ tmp9^post21-tmp9^post20 == 0 /\ -tmp620^post21+tmp620^0 == 0 /\ -c12^post21+c12^0 == 0 /\ a10^0-a10^post21 == 0), cost: 1 New rule: l13 -> l4 : __const_10^0'=__const_10^post21, a10^0'=a10^post21, a15^0'=a15^post21, b11^0'=b11^post21, b16^0'=b16^post21, c12^0'=c12^post21, c17^0'=c17^post21, m13^0'=m13^post21, ret_max24^0'=ret_max24^post21, ret_min14^0'=ret_min14^post21, tmp620^0'=tmp620^post21, tmp923^0'=tmp923^post21, tmp9^0'=tmp9^post21, tmp^0'=tmp^post21, tmp___0^0'=tmp___0^post21, tmp___1^0'=tmp___1^post21, x_promoted_1^0'=__const_10^post21, y_promoted_2^0'=2, z^0'=1, (0 == 0 /\ tmp9^0-tmp9^post21 == 0 /\ y_promoted_2^0-y_promoted_2^post21 == 0 /\ c17^0-c17^post21 == 0 /\ tmp___0^0-tmp___0^post21 == 0 /\ -a15^post21+a15^0 == 0 /\ -x_promoted_1^post21+x_promoted_1^0 == 0 /\ -__const_10^post21+__const_10^0 == 0 /\ -ret_max24^post21+ret_max24^0 == 0 /\ m13^0-m13^post21 == 0 /\ -tmp^post21+tmp^0 == 0 /\ -z^post21+z^0 == 0 /\ b16^0-b16^post21 == 0 /\ b11^0-b11^post21 == 0 /\ ret_min14^0-ret_min14^post21 == 0 /\ -tmp923^post21+tmp923^0 == 0 /\ -tmp___1^post21+tmp___1^0 == 0 /\ -tmp620^post21+tmp620^0 == 0 /\ -c12^post21+c12^0 == 0 /\ a10^0-a10^post21 == 0), cost: 1 propagated equality a15^post20 = a15^post21 propagated equality tmp923^post20 = tmp923^post21 propagated equality b11^post20 = b11^post21 propagated equality tmp620^post20 = tmp620^post21 propagated equality y_promoted_2^post20 = 2 propagated equality a10^post20 = a10^post21 propagated equality x_promoted_1^post20 = __const_10^post21 propagated equality m13^post20 = m13^post21 propagated equality c17^post20 = c17^post21 propagated equality tmp___0^post20 = tmp___0^post21 propagated equality b16^post20 = b16^post21 propagated equality z^post20 = 1 propagated equality tmp^post20 = tmp^post21 propagated equality c12^post20 = c12^post21 propagated equality ret_min14^post20 = ret_min14^post21 propagated equality __const_10^post20 = __const_10^post21 propagated equality tmp___1^post20 = tmp___1^post21 propagated equality ret_max24^post20 = ret_max24^post21 propagated equality tmp9^post20 = tmp9^post21 Propagated Equalities Original rule: l13 -> l4 : __const_10^0'=__const_10^post21, a10^0'=a10^post21, a15^0'=a15^post21, b11^0'=b11^post21, b16^0'=b16^post21, c12^0'=c12^post21, c17^0'=c17^post21, m13^0'=m13^post21, ret_max24^0'=ret_max24^post21, ret_min14^0'=ret_min14^post21, tmp620^0'=tmp620^post21, tmp923^0'=tmp923^post21, tmp9^0'=tmp9^post21, tmp^0'=tmp^post21, tmp___0^0'=tmp___0^post21, tmp___1^0'=tmp___1^post21, x_promoted_1^0'=__const_10^post21, y_promoted_2^0'=2, z^0'=1, (0 == 0 /\ tmp9^0-tmp9^post21 == 0 /\ y_promoted_2^0-y_promoted_2^post21 == 0 /\ c17^0-c17^post21 == 0 /\ tmp___0^0-tmp___0^post21 == 0 /\ -a15^post21+a15^0 == 0 /\ -x_promoted_1^post21+x_promoted_1^0 == 0 /\ -__const_10^post21+__const_10^0 == 0 /\ -ret_max24^post21+ret_max24^0 == 0 /\ m13^0-m13^post21 == 0 /\ -tmp^post21+tmp^0 == 0 /\ -z^post21+z^0 == 0 /\ b16^0-b16^post21 == 0 /\ b11^0-b11^post21 == 0 /\ ret_min14^0-ret_min14^post21 == 0 /\ -tmp923^post21+tmp923^0 == 0 /\ -tmp___1^post21+tmp___1^0 == 0 /\ -tmp620^post21+tmp620^0 == 0 /\ -c12^post21+c12^0 == 0 /\ a10^0-a10^post21 == 0), cost: 1 New rule: l13 -> l4 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=__const_10^0, y_promoted_2^0'=2, z^0'=1, 0 == 0, cost: 1 propagated equality tmp9^post21 = tmp9^0 propagated equality y_promoted_2^post21 = y_promoted_2^0 propagated equality c17^post21 = c17^0 propagated equality tmp___0^post21 = tmp___0^0 propagated equality a15^post21 = a15^0 propagated equality x_promoted_1^post21 = x_promoted_1^0 propagated equality __const_10^post21 = __const_10^0 propagated equality ret_max24^post21 = ret_max24^0 propagated equality m13^post21 = m13^0 propagated equality tmp^post21 = tmp^0 propagated equality z^post21 = z^0 propagated equality b16^post21 = b16^0 propagated equality b11^post21 = b11^0 propagated equality ret_min14^post21 = ret_min14^0 propagated equality tmp923^post21 = tmp923^0 propagated equality tmp___1^post21 = tmp___1^0 propagated equality tmp620^post21 = tmp620^0 propagated equality c12^post21 = c12^0 propagated equality a10^post21 = a10^0 Simplified Guard Original rule: l13 -> l4 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=__const_10^0, y_promoted_2^0'=2, z^0'=1, 0 == 0, cost: 1 New rule: l13 -> l4 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=__const_10^0, y_promoted_2^0'=2, z^0'=1, T, cost: 1 Removed Trivial Updates Original rule: l13 -> l4 : __const_10^0'=__const_10^0, a10^0'=a10^0, a15^0'=a15^0, b11^0'=b11^0, b16^0'=b16^0, c12^0'=c12^0, c17^0'=c17^0, m13^0'=m13^0, ret_max24^0'=ret_max24^0, ret_min14^0'=ret_min14^0, tmp620^0'=tmp620^0, tmp923^0'=tmp923^0, tmp9^0'=tmp9^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, x_promoted_1^0'=__const_10^0, y_promoted_2^0'=2, z^0'=1, T, cost: 1 New rule: l13 -> l4 : x_promoted_1^0'=__const_10^0, y_promoted_2^0'=2, z^0'=1, T, cost: 1 Step with 41 Trace 41[T] Blocked [{}, {}] Step with 24 Trace 41[T], 24[(1+y_promoted_2^0-x_promoted_1^0 <= 0)] Blocked [{}, {}, {}] Step with 37 Trace 41[T], 24[(1+y_promoted_2^0-x_promoted_1^0 <= 0)], 37[(1-x_promoted_1^0+z^0 <= 0)] Blocked [{}, {}, {}, {}] Step with 29 Trace 41[T], 24[(1+y_promoted_2^0-x_promoted_1^0 <= 0)], 37[(1-x_promoted_1^0+z^0 <= 0)], 29[(-b16^0+a15^0 <= 0)] Blocked [{}, {}, {}, {28[T]}, {}] Step with 27 Trace 41[T], 24[(1+y_promoted_2^0-x_promoted_1^0 <= 0)], 37[(1-x_promoted_1^0+z^0 <= 0)], 29[(-b16^0+a15^0 <= 0)], 27[(-c17^0+a15^0 <= 0)] Blocked [{}, {}, {}, {28[T]}, {26[T]}, {}] Step with 23 Trace 41[T], 24[(1+y_promoted_2^0-x_promoted_1^0 <= 0)], 37[(1-x_promoted_1^0+z^0 <= 0)], 29[(-b16^0+a15^0 <= 0)], 27[(-c17^0+a15^0 <= 0)], 23[T] Blocked [{}, {}, {}, {28[T]}, {26[T]}, {}, {}] Step with 39 Trace 41[T], 24[(1+y_promoted_2^0-x_promoted_1^0 <= 0)], 37[(1-x_promoted_1^0+z^0 <= 0)], 29[(-b16^0+a15^0 <= 0)], 27[(-c17^0+a15^0 <= 0)], 23[T], 39[(1-y_promoted_2^0+z^0 <= 0)] Blocked [{}, {}, {}, {28[T]}, {26[T]}, {}, {}, {}] Step with 22 Trace 41[T], 24[(1+y_promoted_2^0-x_promoted_1^0 <= 0)], 37[(1-x_promoted_1^0+z^0 <= 0)], 29[(-b16^0+a15^0 <= 0)], 27[(-c17^0+a15^0 <= 0)], 23[T], 39[(1-y_promoted_2^0+z^0 <= 0)], 22[T] Blocked [{}, {}, {}, {28[T]}, {26[T]}, {}, {}, {}, {}] Backtrack Trace 41[T], 24[(1+y_promoted_2^0-x_promoted_1^0 <= 0)], 37[(1-x_promoted_1^0+z^0 <= 0)], 29[(-b16^0+a15^0 <= 0)], 27[(-c17^0+a15^0 <= 0)], 23[T], 39[(1-y_promoted_2^0+z^0 <= 0)] Blocked [{}, {}, {}, {28[T]}, {26[T]}, {}, {}, {22[T]}] Backtrack Trace 41[T], 24[(1+y_promoted_2^0-x_promoted_1^0 <= 0)], 37[(1-x_promoted_1^0+z^0 <= 0)], 29[(-b16^0+a15^0 <= 0)], 27[(-c17^0+a15^0 <= 0)], 23[T] Blocked [{}, {}, {}, {28[T]}, {26[T]}, {}, {39[T]}] Step with 40 Trace 41[T], 24[(1+y_promoted_2^0-x_promoted_1^0 <= 0)], 37[(1-x_promoted_1^0+z^0 <= 0)], 29[(-b16^0+a15^0 <= 0)], 27[(-c17^0+a15^0 <= 0)], 23[T], 40[(y_promoted_2^0-z^0 <= 0)] Blocked [{}, {}, {}, {28[T]}, {26[T]}, {}, {39[T]}, {}] Step with 22 Trace 41[T], 24[(1+y_promoted_2^0-x_promoted_1^0 <= 0)], 37[(1-x_promoted_1^0+z^0 <= 0)], 29[(-b16^0+a15^0 <= 0)], 27[(-c17^0+a15^0 <= 0)], 23[T], 40[(y_promoted_2^0-z^0 <= 0)], 22[T] Blocked [{}, {}, {}, {28[T]}, {26[T]}, {}, {39[T]}, {}, {}] Backtrack Trace 41[T], 24[(1+y_promoted_2^0-x_promoted_1^0 <= 0)], 37[(1-x_promoted_1^0+z^0 <= 0)], 29[(-b16^0+a15^0 <= 0)], 27[(-c17^0+a15^0 <= 0)], 23[T], 40[(y_promoted_2^0-z^0 <= 0)] Blocked [{}, {}, {}, {28[T]}, {26[T]}, {}, {39[T]}, {22[T]}] Backtrack Trace 41[T], 24[(1+y_promoted_2^0-x_promoted_1^0 <= 0)], 37[(1-x_promoted_1^0+z^0 <= 0)], 29[(-b16^0+a15^0 <= 0)], 27[(-c17^0+a15^0 <= 0)], 23[T] Blocked [{}, {}, {}, {28[T]}, {26[T]}, {}, {39[T], 40[T]}] Backtrack Trace 41[T], 24[(1+y_promoted_2^0-x_promoted_1^0 <= 0)], 37[(1-x_promoted_1^0+z^0 <= 0)], 29[(-b16^0+a15^0 <= 0)], 27[(-c17^0+a15^0 <= 0)] Blocked [{}, {}, {}, {28[T]}, {26[T]}, {23[T]}] Backtrack Trace 41[T], 24[(1+y_promoted_2^0-x_promoted_1^0 <= 0)], 37[(1-x_promoted_1^0+z^0 <= 0)], 29[(-b16^0+a15^0 <= 0)] Blocked [{}, {}, {}, {28[T]}, {26[T], 27[T]}] Backtrack Trace 41[T], 24[(1+y_promoted_2^0-x_promoted_1^0 <= 0)], 37[(1-x_promoted_1^0+z^0 <= 0)] Blocked [{}, {}, {}, {28[T], 29[T]}] Backtrack Trace 41[T], 24[(1+y_promoted_2^0-x_promoted_1^0 <= 0)] Blocked [{}, {}, {37[T]}] Backtrack Trace 41[T] Blocked [{}, {24[T]}] Step with 25 Trace 41[T], 25[(-y_promoted_2^0+x_promoted_1^0 <= 0)] Blocked [{}, {24[T]}, {}] Step with 39 Trace 41[T], 25[(-y_promoted_2^0+x_promoted_1^0 <= 0)], 39[(1-y_promoted_2^0+z^0 <= 0)] Blocked [{}, {24[T]}, {40[T]}, {}] Step with 22 Trace 41[T], 25[(-y_promoted_2^0+x_promoted_1^0 <= 0)], 39[(1-y_promoted_2^0+z^0 <= 0)], 22[T] Blocked [{}, {24[T]}, {40[T]}, {}, {}] Backtrack Trace 41[T], 25[(-y_promoted_2^0+x_promoted_1^0 <= 0)], 39[(1-y_promoted_2^0+z^0 <= 0)] Blocked [{}, {24[T]}, {40[T]}, {22[T]}] Backtrack Trace 41[T], 25[(-y_promoted_2^0+x_promoted_1^0 <= 0)] Blocked [{}, {24[T]}, {39[T], 40[T]}] Backtrack Trace 41[T] Blocked [{}, {24[T], 25[T]}] Backtrack Trace Blocked [{41[T]}] Accept unknown Build SHA: a05f16bf13df659c382799650051f91bf6828c7b