unknown Initial ITS Start location: l6 Program variables: constant22^0 i20^0 lx2^0 tmp03^0 tmp1011^0 tmp1112^0 tmp1213^0 tmp1314^0 tmp14^0 tmp25^0 tmp36^0 tmp47^0 tmp58^0 tmp69^0 tmp710^0 z115^0 z216^0 z317^0 z418^0 z519^0 0: l0 -> l1 : constant22^0'=constant22^post1, i20^0'=i20^post1, lx2^0'=lx2^post1, tmp03^0'=tmp03^post1, tmp1011^0'=tmp1011^post1, tmp1112^0'=tmp1112^post1, tmp1213^0'=tmp1213^post1, tmp1314^0'=tmp1314^post1, tmp14^0'=tmp14^post1, tmp25^0'=tmp25^post1, tmp36^0'=tmp36^post1, tmp47^0'=tmp47^post1, tmp58^0'=tmp58^post1, tmp69^0'=tmp69^post1, tmp710^0'=tmp710^post1, z115^0'=z115^post1, z216^0'=z216^post1, z317^0'=z317^post1, z418^0'=z418^post1, z519^0'=z519^post1, (lx2^0-lx2^post1 == 0 /\ tmp1314^0-tmp1314^post1 == 0 /\ -tmp03^post1+tmp03^0 == 0 /\ 8-i20^0 <= 0 /\ tmp710^0-tmp710^post1 == 0 /\ tmp14^0-tmp14^post1 == 0 /\ -tmp69^post1+tmp69^0 == 0 /\ -tmp25^post1+tmp25^0 == 0 /\ tmp47^0-tmp47^post1 == 0 /\ tmp1112^0-tmp1112^post1 == 0 /\ tmp1011^0-tmp1011^post1 == 0 /\ -z115^post1+z115^0 == 0 /\ i20^post1 == 0 /\ -z216^post1+z216^0 == 0 /\ z317^0-z317^post1 == 0 /\ -z519^post1+z519^0 == 0 /\ -z418^post1+z418^0 == 0 /\ -tmp1213^post1+tmp1213^0 == 0 /\ constant22^0-constant22^post1 == 0 /\ -tmp36^post1+tmp36^0 == 0 /\ -tmp58^post1+tmp58^0 == 0), cost: 1 1: l0 -> l2 : constant22^0'=constant22^post2, i20^0'=i20^post2, lx2^0'=lx2^post2, tmp03^0'=tmp03^post2, tmp1011^0'=tmp1011^post2, tmp1112^0'=tmp1112^post2, tmp1213^0'=tmp1213^post2, tmp1314^0'=tmp1314^post2, tmp14^0'=tmp14^post2, tmp25^0'=tmp25^post2, tmp36^0'=tmp36^post2, tmp47^0'=tmp47^post2, tmp58^0'=tmp58^post2, tmp69^0'=tmp69^post2, tmp710^0'=tmp710^post2, z115^0'=z115^post2, z216^0'=z216^post2, z317^0'=z317^post2, z418^0'=z418^post2, z519^0'=z519^post2, (0 == 0 /\ 20995+constant22^10 == 0 /\ -2446+constant22^5 == 0 /\ 7373+constant22^9 == 0 /\ tmp1314^post2-tmp03^post2+tmp36^post2 == 0 /\ -lx2^post2+lx2^0 == 0 /\ 16069+constant22^11 == 0 /\ -6270+constant22^2 == 0 /\ -9633+constant22^4 == 0 /\ -25172+constant22^7 == 0 /\ -tmp14^post2+tmp25^post2+tmp1213^post2 == 0 /\ z418^1-tmp58^1-tmp710^1 == 0 /\ -1+i20^post2-i20^0 == 0 /\ 15137+constant22^3 == 0 /\ -12299+constant22^8 == 0 /\ z317^post2-z317^2-z519^post2 == 0 /\ tmp1011^post2-tmp03^post2-tmp36^post2 == 0 /\ z418^post2-z418^2-z519^post2 == 0 /\ -tmp14^post2+tmp1112^post2-tmp25^post2 == 0 /\ -16819+constant22^6 == 0 /\ 3196+constant22^post2 == 0 /\ z317^1-tmp69^1-tmp47^1 == 0 /\ -tmp69^1-tmp58^1+z216^1 == 0 /\ -7+i20^0 <= 0 /\ z115^2-tmp47^1-tmp710^1 == 0 /\ -4433+constant22^1 == 0), cost: 1 5: l1 -> l3 : constant22^0'=constant22^post6, i20^0'=i20^post6, lx2^0'=lx2^post6, tmp03^0'=tmp03^post6, tmp1011^0'=tmp1011^post6, tmp1112^0'=tmp1112^post6, tmp1213^0'=tmp1213^post6, tmp1314^0'=tmp1314^post6, tmp14^0'=tmp14^post6, tmp25^0'=tmp25^post6, tmp36^0'=tmp36^post6, tmp47^0'=tmp47^post6, tmp58^0'=tmp58^post6, tmp69^0'=tmp69^post6, tmp710^0'=tmp710^post6, z115^0'=z115^post6, z216^0'=z216^post6, z317^0'=z317^post6, z418^0'=z418^post6, z519^0'=z519^post6, (z519^0-z519^post6 == 0 /\ tmp58^0-tmp58^post6 == 0 /\ -tmp36^post6+tmp36^0 == 0 /\ z317^0-z317^post6 == 0 /\ -tmp1112^post6+tmp1112^0 == 0 /\ tmp25^0-tmp25^post6 == 0 /\ tmp1213^0-tmp1213^post6 == 0 /\ -z115^post6+z115^0 == 0 /\ -tmp1314^post6+tmp1314^0 == 0 /\ -tmp710^post6+tmp710^0 == 0 /\ -i20^post6+i20^0 == 0 /\ constant22^0-constant22^post6 == 0 /\ z216^0-z216^post6 == 0 /\ tmp1011^0-tmp1011^post6 == 0 /\ -tmp69^post6+tmp69^0 == 0 /\ -lx2^post6+lx2^0 == 0 /\ tmp03^0-tmp03^post6 == 0 /\ -tmp47^post6+tmp47^0 == 0 /\ -tmp14^post6+tmp14^0 == 0 /\ -z418^post6+z418^0 == 0), cost: 1 4: l2 -> l0 : constant22^0'=constant22^post5, i20^0'=i20^post5, lx2^0'=lx2^post5, tmp03^0'=tmp03^post5, tmp1011^0'=tmp1011^post5, tmp1112^0'=tmp1112^post5, tmp1213^0'=tmp1213^post5, tmp1314^0'=tmp1314^post5, tmp14^0'=tmp14^post5, tmp25^0'=tmp25^post5, tmp36^0'=tmp36^post5, tmp47^0'=tmp47^post5, tmp58^0'=tmp58^post5, tmp69^0'=tmp69^post5, tmp710^0'=tmp710^post5, z115^0'=z115^post5, z216^0'=z216^post5, z317^0'=z317^post5, z418^0'=z418^post5, z519^0'=z519^post5, (-tmp1112^post5+tmp1112^0 == 0 /\ -tmp47^post5+tmp47^0 == 0 /\ -tmp1011^post5+tmp1011^0 == 0 /\ -tmp14^post5+tmp14^0 == 0 /\ -tmp1314^post5+tmp1314^0 == 0 /\ -tmp36^post5+tmp36^0 == 0 /\ -lx2^post5+lx2^0 == 0 /\ z216^0-z216^post5 == 0 /\ -z115^post5+z115^0 == 0 /\ tmp25^0-tmp25^post5 == 0 /\ -z317^post5+z317^0 == 0 /\ tmp1213^0-tmp1213^post5 == 0 /\ tmp58^0-tmp58^post5 == 0 /\ -tmp710^post5+tmp710^0 == 0 /\ -i20^post5+i20^0 == 0 /\ tmp69^0-tmp69^post5 == 0 /\ tmp03^0-tmp03^post5 == 0 /\ z519^0-z519^post5 == 0 /\ -z418^post5+z418^0 == 0 /\ constant22^0-constant22^post5 == 0), cost: 1 2: l3 -> l4 : constant22^0'=constant22^post3, i20^0'=i20^post3, lx2^0'=lx2^post3, tmp03^0'=tmp03^post3, tmp1011^0'=tmp1011^post3, tmp1112^0'=tmp1112^post3, tmp1213^0'=tmp1213^post3, tmp1314^0'=tmp1314^post3, tmp14^0'=tmp14^post3, tmp25^0'=tmp25^post3, tmp36^0'=tmp36^post3, tmp47^0'=tmp47^post3, tmp58^0'=tmp58^post3, tmp69^0'=tmp69^post3, tmp710^0'=tmp710^post3, z115^0'=z115^post3, z216^0'=z216^post3, z317^0'=z317^post3, z418^0'=z418^post3, z519^0'=z519^post3, (-z115^post3+z115^0 == 0 /\ z519^0-z519^post3 == 0 /\ tmp58^0-tmp58^post3 == 0 /\ tmp1213^0-tmp1213^post3 == 0 /\ -z216^post3+z216^0 == 0 /\ -tmp14^post3+tmp14^0 == 0 /\ 8-i20^0 <= 0 /\ z317^0-z317^post3 == 0 /\ -tmp1112^post3+tmp1112^0 == 0 /\ -tmp36^post3+tmp36^0 == 0 /\ -tmp710^post3+tmp710^0 == 0 /\ -i20^post3+i20^0 == 0 /\ tmp1314^0-tmp1314^post3 == 0 /\ tmp1011^0-tmp1011^post3 == 0 /\ constant22^0-constant22^post3 == 0 /\ tmp25^0-tmp25^post3 == 0 /\ -lx2^post3+lx2^0 == 0 /\ tmp03^0-tmp03^post3 == 0 /\ -tmp69^post3+tmp69^0 == 0 /\ -z418^post3+z418^0 == 0 /\ -tmp47^post3+tmp47^0 == 0), cost: 1 3: l3 -> l1 : constant22^0'=constant22^post4, i20^0'=i20^post4, lx2^0'=lx2^post4, tmp03^0'=tmp03^post4, tmp1011^0'=tmp1011^post4, tmp1112^0'=tmp1112^post4, tmp1213^0'=tmp1213^post4, tmp1314^0'=tmp1314^post4, tmp14^0'=tmp14^post4, tmp25^0'=tmp25^post4, tmp36^0'=tmp36^post4, tmp47^0'=tmp47^post4, tmp58^0'=tmp58^post4, tmp69^0'=tmp69^post4, tmp710^0'=tmp710^post4, z115^0'=z115^post4, z216^0'=z216^post4, z317^0'=z317^post4, z418^0'=z418^post4, z519^0'=z519^post4, (0 == 0 /\ 20995+constant22^10 == 0 /\ -2446+constant22^5 == 0 /\ 7373+constant22^9 == 0 /\ -tmp14^post4+tmp1112^post4-tmp25^post4 == 0 /\ 3196+constant22^post4 == 0 /\ -tmp03^post4-tmp36^post4+tmp1011^post4 == 0 /\ 16069+constant22^11 == 0 /\ -6270+constant22^2 == 0 /\ -lx2^post4+lx2^0 == 0 /\ -9633+constant22^4 == 0 /\ -25172+constant22^7 == 0 /\ z418^1-tmp58^1-tmp710^1 == 0 /\ -z317^2-z519^post4+z317^post4 == 0 /\ 15137+constant22^3 == 0 /\ -12299+constant22^8 == 0 /\ -tmp03^post4+tmp36^post4+tmp1314^post4 == 0 /\ -16819+constant22^6 == 0 /\ -tmp14^post4+tmp25^post4+tmp1213^post4 == 0 /\ z317^1-tmp69^1-tmp47^1 == 0 /\ -tmp69^1-tmp58^1+z216^1 == 0 /\ -7+i20^0 <= 0 /\ -1+i20^post4-i20^0 == 0 /\ z115^2-tmp47^1-tmp710^1 == 0 /\ z418^post4-z519^post4-z418^2 == 0 /\ -4433+constant22^1 == 0), cost: 1 6: l5 -> l2 : constant22^0'=constant22^post7, i20^0'=i20^post7, lx2^0'=lx2^post7, tmp03^0'=tmp03^post7, tmp1011^0'=tmp1011^post7, tmp1112^0'=tmp1112^post7, tmp1213^0'=tmp1213^post7, tmp1314^0'=tmp1314^post7, tmp14^0'=tmp14^post7, tmp25^0'=tmp25^post7, tmp36^0'=tmp36^post7, tmp47^0'=tmp47^post7, tmp58^0'=tmp58^post7, tmp69^0'=tmp69^post7, tmp710^0'=tmp710^post7, z115^0'=z115^post7, z216^0'=z216^post7, z317^0'=z317^post7, z418^0'=z418^post7, z519^0'=z519^post7, (-z115^post7+z115^0 == 0 /\ z519^0-z519^post7 == 0 /\ tmp1011^0-tmp1011^post7 == 0 /\ tmp710^0-tmp710^post7 == 0 /\ tmp58^0-tmp58^post7 == 0 /\ tmp1213^0-tmp1213^post7 == 0 /\ -z216^post7+z216^0 == 0 /\ -tmp14^post7+tmp14^0 == 0 /\ z317^0-z317^post7 == 0 /\ -tmp36^post7+tmp36^0 == 0 /\ -constant22^post7+constant22^0 == 0 /\ tmp1314^0-tmp1314^post7 == 0 /\ i20^post7 == 0 /\ -tmp03^post7+tmp03^0 == 0 /\ -8+lx2^post7 == 0 /\ -tmp69^post7+tmp69^0 == 0 /\ -tmp25^post7+tmp25^0 == 0 /\ -z418^post7+z418^0 == 0 /\ tmp47^0-tmp47^post7 == 0 /\ tmp1112^0-tmp1112^post7 == 0), cost: 1 7: l6 -> l5 : constant22^0'=constant22^post8, i20^0'=i20^post8, lx2^0'=lx2^post8, tmp03^0'=tmp03^post8, tmp1011^0'=tmp1011^post8, tmp1112^0'=tmp1112^post8, tmp1213^0'=tmp1213^post8, tmp1314^0'=tmp1314^post8, tmp14^0'=tmp14^post8, tmp25^0'=tmp25^post8, tmp36^0'=tmp36^post8, tmp47^0'=tmp47^post8, tmp58^0'=tmp58^post8, tmp69^0'=tmp69^post8, tmp710^0'=tmp710^post8, z115^0'=z115^post8, z216^0'=z216^post8, z317^0'=z317^post8, z418^0'=z418^post8, z519^0'=z519^post8, (-tmp36^post8+tmp36^0 == 0 /\ -tmp47^post8+tmp47^0 == 0 /\ -lx2^post8+lx2^0 == 0 /\ -z317^post8+z317^0 == 0 /\ -tmp14^post8+tmp14^0 == 0 /\ -tmp1314^post8+tmp1314^0 == 0 /\ constant22^0-constant22^post8 == 0 /\ -z115^post8+z115^0 == 0 /\ -tmp1011^post8+tmp1011^0 == 0 /\ -tmp1112^post8+tmp1112^0 == 0 /\ -i20^post8+i20^0 == 0 /\ tmp25^0-tmp25^post8 == 0 /\ -tmp710^post8+tmp710^0 == 0 /\ -z418^post8+z418^0 == 0 /\ tmp1213^0-tmp1213^post8 == 0 /\ tmp69^0-tmp69^post8 == 0 /\ tmp58^0-tmp58^post8 == 0 /\ z216^0-z216^post8 == 0 /\ tmp03^0-tmp03^post8 == 0 /\ z519^0-z519^post8 == 0), cost: 1 Chained Linear Paths Start location: l6 Program variables: constant22^0 i20^0 lx2^0 tmp03^0 tmp1011^0 tmp1112^0 tmp1213^0 tmp1314^0 tmp14^0 tmp25^0 tmp36^0 tmp47^0 tmp58^0 tmp69^0 tmp710^0 z115^0 z216^0 z317^0 z418^0 z519^0 0: l0 -> l1 : constant22^0'=constant22^post1, i20^0'=i20^post1, lx2^0'=lx2^post1, tmp03^0'=tmp03^post1, tmp1011^0'=tmp1011^post1, tmp1112^0'=tmp1112^post1, tmp1213^0'=tmp1213^post1, tmp1314^0'=tmp1314^post1, tmp14^0'=tmp14^post1, tmp25^0'=tmp25^post1, tmp36^0'=tmp36^post1, tmp47^0'=tmp47^post1, tmp58^0'=tmp58^post1, tmp69^0'=tmp69^post1, tmp710^0'=tmp710^post1, z115^0'=z115^post1, z216^0'=z216^post1, z317^0'=z317^post1, z418^0'=z418^post1, z519^0'=z519^post1, (lx2^0-lx2^post1 == 0 /\ tmp1314^0-tmp1314^post1 == 0 /\ -tmp03^post1+tmp03^0 == 0 /\ 8-i20^0 <= 0 /\ tmp710^0-tmp710^post1 == 0 /\ tmp14^0-tmp14^post1 == 0 /\ -tmp69^post1+tmp69^0 == 0 /\ -tmp25^post1+tmp25^0 == 0 /\ tmp47^0-tmp47^post1 == 0 /\ tmp1112^0-tmp1112^post1 == 0 /\ tmp1011^0-tmp1011^post1 == 0 /\ -z115^post1+z115^0 == 0 /\ i20^post1 == 0 /\ -z216^post1+z216^0 == 0 /\ z317^0-z317^post1 == 0 /\ -z519^post1+z519^0 == 0 /\ -z418^post1+z418^0 == 0 /\ -tmp1213^post1+tmp1213^0 == 0 /\ constant22^0-constant22^post1 == 0 /\ -tmp36^post1+tmp36^0 == 0 /\ -tmp58^post1+tmp58^0 == 0), cost: 1 1: l0 -> l2 : constant22^0'=constant22^post2, i20^0'=i20^post2, lx2^0'=lx2^post2, tmp03^0'=tmp03^post2, tmp1011^0'=tmp1011^post2, tmp1112^0'=tmp1112^post2, tmp1213^0'=tmp1213^post2, tmp1314^0'=tmp1314^post2, tmp14^0'=tmp14^post2, tmp25^0'=tmp25^post2, tmp36^0'=tmp36^post2, tmp47^0'=tmp47^post2, tmp58^0'=tmp58^post2, tmp69^0'=tmp69^post2, tmp710^0'=tmp710^post2, z115^0'=z115^post2, z216^0'=z216^post2, z317^0'=z317^post2, z418^0'=z418^post2, z519^0'=z519^post2, (0 == 0 /\ 20995+constant22^10 == 0 /\ -2446+constant22^5 == 0 /\ 7373+constant22^9 == 0 /\ tmp1314^post2-tmp03^post2+tmp36^post2 == 0 /\ -lx2^post2+lx2^0 == 0 /\ 16069+constant22^11 == 0 /\ -6270+constant22^2 == 0 /\ -9633+constant22^4 == 0 /\ -25172+constant22^7 == 0 /\ -tmp14^post2+tmp25^post2+tmp1213^post2 == 0 /\ z418^1-tmp58^1-tmp710^1 == 0 /\ -1+i20^post2-i20^0 == 0 /\ 15137+constant22^3 == 0 /\ -12299+constant22^8 == 0 /\ z317^post2-z317^2-z519^post2 == 0 /\ tmp1011^post2-tmp03^post2-tmp36^post2 == 0 /\ z418^post2-z418^2-z519^post2 == 0 /\ -tmp14^post2+tmp1112^post2-tmp25^post2 == 0 /\ -16819+constant22^6 == 0 /\ 3196+constant22^post2 == 0 /\ z317^1-tmp69^1-tmp47^1 == 0 /\ -tmp69^1-tmp58^1+z216^1 == 0 /\ -7+i20^0 <= 0 /\ z115^2-tmp47^1-tmp710^1 == 0 /\ -4433+constant22^1 == 0), cost: 1 5: l1 -> l3 : constant22^0'=constant22^post6, i20^0'=i20^post6, lx2^0'=lx2^post6, tmp03^0'=tmp03^post6, tmp1011^0'=tmp1011^post6, tmp1112^0'=tmp1112^post6, tmp1213^0'=tmp1213^post6, tmp1314^0'=tmp1314^post6, tmp14^0'=tmp14^post6, tmp25^0'=tmp25^post6, tmp36^0'=tmp36^post6, tmp47^0'=tmp47^post6, tmp58^0'=tmp58^post6, tmp69^0'=tmp69^post6, tmp710^0'=tmp710^post6, z115^0'=z115^post6, z216^0'=z216^post6, z317^0'=z317^post6, z418^0'=z418^post6, z519^0'=z519^post6, (z519^0-z519^post6 == 0 /\ tmp58^0-tmp58^post6 == 0 /\ -tmp36^post6+tmp36^0 == 0 /\ z317^0-z317^post6 == 0 /\ -tmp1112^post6+tmp1112^0 == 0 /\ tmp25^0-tmp25^post6 == 0 /\ tmp1213^0-tmp1213^post6 == 0 /\ -z115^post6+z115^0 == 0 /\ -tmp1314^post6+tmp1314^0 == 0 /\ -tmp710^post6+tmp710^0 == 0 /\ -i20^post6+i20^0 == 0 /\ constant22^0-constant22^post6 == 0 /\ z216^0-z216^post6 == 0 /\ tmp1011^0-tmp1011^post6 == 0 /\ -tmp69^post6+tmp69^0 == 0 /\ -lx2^post6+lx2^0 == 0 /\ tmp03^0-tmp03^post6 == 0 /\ -tmp47^post6+tmp47^0 == 0 /\ -tmp14^post6+tmp14^0 == 0 /\ -z418^post6+z418^0 == 0), cost: 1 4: l2 -> l0 : constant22^0'=constant22^post5, i20^0'=i20^post5, lx2^0'=lx2^post5, tmp03^0'=tmp03^post5, tmp1011^0'=tmp1011^post5, tmp1112^0'=tmp1112^post5, tmp1213^0'=tmp1213^post5, tmp1314^0'=tmp1314^post5, tmp14^0'=tmp14^post5, tmp25^0'=tmp25^post5, tmp36^0'=tmp36^post5, tmp47^0'=tmp47^post5, tmp58^0'=tmp58^post5, tmp69^0'=tmp69^post5, tmp710^0'=tmp710^post5, z115^0'=z115^post5, z216^0'=z216^post5, z317^0'=z317^post5, z418^0'=z418^post5, z519^0'=z519^post5, (-tmp1112^post5+tmp1112^0 == 0 /\ -tmp47^post5+tmp47^0 == 0 /\ -tmp1011^post5+tmp1011^0 == 0 /\ -tmp14^post5+tmp14^0 == 0 /\ -tmp1314^post5+tmp1314^0 == 0 /\ -tmp36^post5+tmp36^0 == 0 /\ -lx2^post5+lx2^0 == 0 /\ z216^0-z216^post5 == 0 /\ -z115^post5+z115^0 == 0 /\ tmp25^0-tmp25^post5 == 0 /\ -z317^post5+z317^0 == 0 /\ tmp1213^0-tmp1213^post5 == 0 /\ tmp58^0-tmp58^post5 == 0 /\ -tmp710^post5+tmp710^0 == 0 /\ -i20^post5+i20^0 == 0 /\ tmp69^0-tmp69^post5 == 0 /\ tmp03^0-tmp03^post5 == 0 /\ z519^0-z519^post5 == 0 /\ -z418^post5+z418^0 == 0 /\ constant22^0-constant22^post5 == 0), cost: 1 2: l3 -> l4 : constant22^0'=constant22^post3, i20^0'=i20^post3, lx2^0'=lx2^post3, tmp03^0'=tmp03^post3, tmp1011^0'=tmp1011^post3, tmp1112^0'=tmp1112^post3, tmp1213^0'=tmp1213^post3, tmp1314^0'=tmp1314^post3, tmp14^0'=tmp14^post3, tmp25^0'=tmp25^post3, tmp36^0'=tmp36^post3, tmp47^0'=tmp47^post3, tmp58^0'=tmp58^post3, tmp69^0'=tmp69^post3, tmp710^0'=tmp710^post3, z115^0'=z115^post3, z216^0'=z216^post3, z317^0'=z317^post3, z418^0'=z418^post3, z519^0'=z519^post3, (-z115^post3+z115^0 == 0 /\ z519^0-z519^post3 == 0 /\ tmp58^0-tmp58^post3 == 0 /\ tmp1213^0-tmp1213^post3 == 0 /\ -z216^post3+z216^0 == 0 /\ -tmp14^post3+tmp14^0 == 0 /\ 8-i20^0 <= 0 /\ z317^0-z317^post3 == 0 /\ -tmp1112^post3+tmp1112^0 == 0 /\ -tmp36^post3+tmp36^0 == 0 /\ -tmp710^post3+tmp710^0 == 0 /\ -i20^post3+i20^0 == 0 /\ tmp1314^0-tmp1314^post3 == 0 /\ tmp1011^0-tmp1011^post3 == 0 /\ constant22^0-constant22^post3 == 0 /\ tmp25^0-tmp25^post3 == 0 /\ -lx2^post3+lx2^0 == 0 /\ tmp03^0-tmp03^post3 == 0 /\ -tmp69^post3+tmp69^0 == 0 /\ -z418^post3+z418^0 == 0 /\ -tmp47^post3+tmp47^0 == 0), cost: 1 3: l3 -> l1 : constant22^0'=constant22^post4, i20^0'=i20^post4, lx2^0'=lx2^post4, tmp03^0'=tmp03^post4, tmp1011^0'=tmp1011^post4, tmp1112^0'=tmp1112^post4, tmp1213^0'=tmp1213^post4, tmp1314^0'=tmp1314^post4, tmp14^0'=tmp14^post4, tmp25^0'=tmp25^post4, tmp36^0'=tmp36^post4, tmp47^0'=tmp47^post4, tmp58^0'=tmp58^post4, tmp69^0'=tmp69^post4, tmp710^0'=tmp710^post4, z115^0'=z115^post4, z216^0'=z216^post4, z317^0'=z317^post4, z418^0'=z418^post4, z519^0'=z519^post4, (0 == 0 /\ 20995+constant22^10 == 0 /\ -2446+constant22^5 == 0 /\ 7373+constant22^9 == 0 /\ -tmp14^post4+tmp1112^post4-tmp25^post4 == 0 /\ 3196+constant22^post4 == 0 /\ -tmp03^post4-tmp36^post4+tmp1011^post4 == 0 /\ 16069+constant22^11 == 0 /\ -6270+constant22^2 == 0 /\ -lx2^post4+lx2^0 == 0 /\ -9633+constant22^4 == 0 /\ -25172+constant22^7 == 0 /\ z418^1-tmp58^1-tmp710^1 == 0 /\ -z317^2-z519^post4+z317^post4 == 0 /\ 15137+constant22^3 == 0 /\ -12299+constant22^8 == 0 /\ -tmp03^post4+tmp36^post4+tmp1314^post4 == 0 /\ -16819+constant22^6 == 0 /\ -tmp14^post4+tmp25^post4+tmp1213^post4 == 0 /\ z317^1-tmp69^1-tmp47^1 == 0 /\ -tmp69^1-tmp58^1+z216^1 == 0 /\ -7+i20^0 <= 0 /\ -1+i20^post4-i20^0 == 0 /\ z115^2-tmp47^1-tmp710^1 == 0 /\ z418^post4-z519^post4-z418^2 == 0 /\ -4433+constant22^1 == 0), cost: 1 8: l6 -> l2 : constant22^0'=constant22^post7, i20^0'=i20^post7, lx2^0'=lx2^post7, tmp03^0'=tmp03^post7, tmp1011^0'=tmp1011^post7, tmp1112^0'=tmp1112^post7, tmp1213^0'=tmp1213^post7, tmp1314^0'=tmp1314^post7, tmp14^0'=tmp14^post7, tmp25^0'=tmp25^post7, tmp36^0'=tmp36^post7, tmp47^0'=tmp47^post7, tmp58^0'=tmp58^post7, tmp69^0'=tmp69^post7, tmp710^0'=tmp710^post7, z115^0'=z115^post7, z216^0'=z216^post7, z317^0'=z317^post7, z418^0'=z418^post7, z519^0'=z519^post7, (-tmp36^post8+tmp36^0 == 0 /\ -tmp47^post8+tmp47^0 == 0 /\ tmp710^post8-tmp710^post7 == 0 /\ -lx2^post8+lx2^0 == 0 /\ -z317^post8+z317^0 == 0 /\ -tmp14^post8+tmp14^0 == 0 /\ -z115^post7+z115^post8 == 0 /\ tmp1314^post8-tmp1314^post7 == 0 /\ -tmp1314^post8+tmp1314^0 == 0 /\ -tmp58^post7+tmp58^post8 == 0 /\ -tmp03^post7+tmp03^post8 == 0 /\ constant22^0-constant22^post8 == 0 /\ -z115^post8+z115^0 == 0 /\ -tmp1011^post8+tmp1011^0 == 0 /\ -tmp1112^post8+tmp1112^0 == 0 /\ -tmp25^post7+tmp25^post8 == 0 /\ -i20^post8+i20^0 == 0 /\ tmp25^0-tmp25^post8 == 0 /\ -tmp710^post8+tmp710^0 == 0 /\ -tmp36^post7+tmp36^post8 == 0 /\ tmp1112^post8-tmp1112^post7 == 0 /\ -z418^post8+z418^0 == 0 /\ i20^post7 == 0 /\ tmp1213^0-tmp1213^post8 == 0 /\ tmp47^post8-tmp47^post7 == 0 /\ z317^post8-z317^post7 == 0 /\ -tmp14^post7+tmp14^post8 == 0 /\ tmp69^0-tmp69^post8 == 0 /\ -z519^post7+z519^post8 == 0 /\ -z216^post7+z216^post8 == 0 /\ -8+lx2^post7 == 0 /\ tmp58^0-tmp58^post8 == 0 /\ -constant22^post7+constant22^post8 == 0 /\ -z418^post7+z418^post8 == 0 /\ z216^0-z216^post8 == 0 /\ -tmp69^post7+tmp69^post8 == 0 /\ tmp1011^post8-tmp1011^post7 == 0 /\ -tmp1213^post7+tmp1213^post8 == 0 /\ tmp03^0-tmp03^post8 == 0 /\ z519^0-z519^post8 == 0), cost: 1 Eliminating location l5 by chaining: Applied chaining First rule: l6 -> l5 : constant22^0'=constant22^post8, i20^0'=i20^post8, lx2^0'=lx2^post8, tmp03^0'=tmp03^post8, tmp1011^0'=tmp1011^post8, tmp1112^0'=tmp1112^post8, tmp1213^0'=tmp1213^post8, tmp1314^0'=tmp1314^post8, tmp14^0'=tmp14^post8, tmp25^0'=tmp25^post8, tmp36^0'=tmp36^post8, tmp47^0'=tmp47^post8, tmp58^0'=tmp58^post8, tmp69^0'=tmp69^post8, tmp710^0'=tmp710^post8, z115^0'=z115^post8, z216^0'=z216^post8, z317^0'=z317^post8, z418^0'=z418^post8, z519^0'=z519^post8, (-tmp36^post8+tmp36^0 == 0 /\ -tmp47^post8+tmp47^0 == 0 /\ -lx2^post8+lx2^0 == 0 /\ -z317^post8+z317^0 == 0 /\ -tmp14^post8+tmp14^0 == 0 /\ -tmp1314^post8+tmp1314^0 == 0 /\ constant22^0-constant22^post8 == 0 /\ -z115^post8+z115^0 == 0 /\ -tmp1011^post8+tmp1011^0 == 0 /\ -tmp1112^post8+tmp1112^0 == 0 /\ -i20^post8+i20^0 == 0 /\ tmp25^0-tmp25^post8 == 0 /\ -tmp710^post8+tmp710^0 == 0 /\ -z418^post8+z418^0 == 0 /\ tmp1213^0-tmp1213^post8 == 0 /\ tmp69^0-tmp69^post8 == 0 /\ tmp58^0-tmp58^post8 == 0 /\ z216^0-z216^post8 == 0 /\ tmp03^0-tmp03^post8 == 0 /\ z519^0-z519^post8 == 0), cost: 1 Second rule: l5 -> l2 : constant22^0'=constant22^post7, i20^0'=i20^post7, lx2^0'=lx2^post7, tmp03^0'=tmp03^post7, tmp1011^0'=tmp1011^post7, tmp1112^0'=tmp1112^post7, tmp1213^0'=tmp1213^post7, tmp1314^0'=tmp1314^post7, tmp14^0'=tmp14^post7, tmp25^0'=tmp25^post7, tmp36^0'=tmp36^post7, tmp47^0'=tmp47^post7, tmp58^0'=tmp58^post7, tmp69^0'=tmp69^post7, tmp710^0'=tmp710^post7, z115^0'=z115^post7, z216^0'=z216^post7, z317^0'=z317^post7, z418^0'=z418^post7, z519^0'=z519^post7, (-z115^post7+z115^0 == 0 /\ z519^0-z519^post7 == 0 /\ tmp1011^0-tmp1011^post7 == 0 /\ tmp710^0-tmp710^post7 == 0 /\ tmp58^0-tmp58^post7 == 0 /\ tmp1213^0-tmp1213^post7 == 0 /\ -z216^post7+z216^0 == 0 /\ -tmp14^post7+tmp14^0 == 0 /\ z317^0-z317^post7 == 0 /\ -tmp36^post7+tmp36^0 == 0 /\ -constant22^post7+constant22^0 == 0 /\ tmp1314^0-tmp1314^post7 == 0 /\ i20^post7 == 0 /\ -tmp03^post7+tmp03^0 == 0 /\ -8+lx2^post7 == 0 /\ -tmp69^post7+tmp69^0 == 0 /\ -tmp25^post7+tmp25^0 == 0 /\ -z418^post7+z418^0 == 0 /\ tmp47^0-tmp47^post7 == 0 /\ tmp1112^0-tmp1112^post7 == 0), cost: 1 New rule: l6 -> l2 : constant22^0'=constant22^post7, i20^0'=i20^post7, lx2^0'=lx2^post7, tmp03^0'=tmp03^post7, tmp1011^0'=tmp1011^post7, tmp1112^0'=tmp1112^post7, tmp1213^0'=tmp1213^post7, tmp1314^0'=tmp1314^post7, tmp14^0'=tmp14^post7, tmp25^0'=tmp25^post7, tmp36^0'=tmp36^post7, tmp47^0'=tmp47^post7, tmp58^0'=tmp58^post7, tmp69^0'=tmp69^post7, tmp710^0'=tmp710^post7, z115^0'=z115^post7, z216^0'=z216^post7, z317^0'=z317^post7, z418^0'=z418^post7, z519^0'=z519^post7, (-tmp36^post8+tmp36^0 == 0 /\ -tmp47^post8+tmp47^0 == 0 /\ tmp710^post8-tmp710^post7 == 0 /\ -lx2^post8+lx2^0 == 0 /\ -z317^post8+z317^0 == 0 /\ -tmp14^post8+tmp14^0 == 0 /\ -z115^post7+z115^post8 == 0 /\ tmp1314^post8-tmp1314^post7 == 0 /\ -tmp1314^post8+tmp1314^0 == 0 /\ -tmp58^post7+tmp58^post8 == 0 /\ -tmp03^post7+tmp03^post8 == 0 /\ constant22^0-constant22^post8 == 0 /\ -z115^post8+z115^0 == 0 /\ -tmp1011^post8+tmp1011^0 == 0 /\ -tmp1112^post8+tmp1112^0 == 0 /\ -tmp25^post7+tmp25^post8 == 0 /\ -i20^post8+i20^0 == 0 /\ tmp25^0-tmp25^post8 == 0 /\ -tmp710^post8+tmp710^0 == 0 /\ -tmp36^post7+tmp36^post8 == 0 /\ tmp1112^post8-tmp1112^post7 == 0 /\ -z418^post8+z418^0 == 0 /\ i20^post7 == 0 /\ tmp1213^0-tmp1213^post8 == 0 /\ tmp47^post8-tmp47^post7 == 0 /\ z317^post8-z317^post7 == 0 /\ -tmp14^post7+tmp14^post8 == 0 /\ tmp69^0-tmp69^post8 == 0 /\ -z519^post7+z519^post8 == 0 /\ -z216^post7+z216^post8 == 0 /\ -8+lx2^post7 == 0 /\ tmp58^0-tmp58^post8 == 0 /\ -constant22^post7+constant22^post8 == 0 /\ -z418^post7+z418^post8 == 0 /\ z216^0-z216^post8 == 0 /\ -tmp69^post7+tmp69^post8 == 0 /\ tmp1011^post8-tmp1011^post7 == 0 /\ -tmp1213^post7+tmp1213^post8 == 0 /\ tmp03^0-tmp03^post8 == 0 /\ z519^0-z519^post8 == 0), cost: 1 Applied deletion Removed the following rules: 6 7 Simplified Transitions Start location: l6 Program variables: constant22^0 i20^0 lx2^0 tmp03^0 tmp1011^0 tmp1112^0 tmp1213^0 tmp1314^0 tmp14^0 tmp25^0 tmp36^0 tmp47^0 tmp58^0 tmp69^0 tmp710^0 z115^0 z216^0 z317^0 z418^0 z519^0 9: l0 -> l1 : i20^0'=0, 8-i20^0 <= 0, cost: 1 10: l0 -> l2 : constant22^0'=-3196, i20^0'=1+i20^0, tmp03^0'=tmp1314^post2+tmp36^post2, tmp1011^0'=tmp1314^post2+2*tmp36^post2, tmp1112^0'=tmp14^post2+tmp25^post2, tmp1213^0'=tmp14^post2-tmp25^post2, tmp1314^0'=tmp1314^post2, tmp14^0'=tmp14^post2, tmp25^0'=tmp25^post2, tmp36^0'=tmp36^post2, tmp47^0'=tmp47^post2, tmp58^0'=tmp58^post2, tmp69^0'=tmp69^post2, tmp710^0'=tmp710^post2, z115^0'=z115^post2, z216^0'=z216^post2, z317^0'=z317^2+z519^post2, z418^0'=z418^2+z519^post2, z519^0'=z519^post2, -7+i20^0 <= 0, cost: 1 14: l1 -> l3 : T, cost: 1 13: l2 -> l0 : T, cost: 1 11: l3 -> l4 : 8-i20^0 <= 0, cost: 1 12: l3 -> l1 : constant22^0'=-3196, i20^0'=1+i20^0, tmp03^0'=tmp36^post4+tmp1314^post4, tmp1011^0'=2*tmp36^post4+tmp1314^post4, tmp1112^0'=tmp14^post4+tmp25^post4, tmp1213^0'=tmp14^post4-tmp25^post4, tmp1314^0'=tmp1314^post4, tmp14^0'=tmp14^post4, tmp25^0'=tmp25^post4, tmp36^0'=tmp36^post4, tmp47^0'=tmp47^post4, tmp58^0'=tmp58^post4, tmp69^0'=tmp69^post4, tmp710^0'=tmp710^post4, z115^0'=z115^post4, z216^0'=z216^post4, z317^0'=z317^2+z519^post4, z418^0'=z519^post4+z418^2, z519^0'=z519^post4, -7+i20^0 <= 0, cost: 1 15: l6 -> l2 : i20^0'=0, lx2^0'=8, T, cost: 1 Propagated Equalities Original rule: l0 -> l1 : constant22^0'=constant22^post1, i20^0'=i20^post1, lx2^0'=lx2^post1, tmp03^0'=tmp03^post1, tmp1011^0'=tmp1011^post1, tmp1112^0'=tmp1112^post1, tmp1213^0'=tmp1213^post1, tmp1314^0'=tmp1314^post1, tmp14^0'=tmp14^post1, tmp25^0'=tmp25^post1, tmp36^0'=tmp36^post1, tmp47^0'=tmp47^post1, tmp58^0'=tmp58^post1, tmp69^0'=tmp69^post1, tmp710^0'=tmp710^post1, z115^0'=z115^post1, z216^0'=z216^post1, z317^0'=z317^post1, z418^0'=z418^post1, z519^0'=z519^post1, (lx2^0-lx2^post1 == 0 /\ tmp1314^0-tmp1314^post1 == 0 /\ -tmp03^post1+tmp03^0 == 0 /\ 8-i20^0 <= 0 /\ tmp710^0-tmp710^post1 == 0 /\ tmp14^0-tmp14^post1 == 0 /\ -tmp69^post1+tmp69^0 == 0 /\ -tmp25^post1+tmp25^0 == 0 /\ tmp47^0-tmp47^post1 == 0 /\ tmp1112^0-tmp1112^post1 == 0 /\ tmp1011^0-tmp1011^post1 == 0 /\ -z115^post1+z115^0 == 0 /\ i20^post1 == 0 /\ -z216^post1+z216^0 == 0 /\ z317^0-z317^post1 == 0 /\ -z519^post1+z519^0 == 0 /\ -z418^post1+z418^0 == 0 /\ -tmp1213^post1+tmp1213^0 == 0 /\ constant22^0-constant22^post1 == 0 /\ -tmp36^post1+tmp36^0 == 0 /\ -tmp58^post1+tmp58^0 == 0), cost: 1 New rule: l0 -> l1 : constant22^0'=constant22^0, i20^0'=0, lx2^0'=lx2^0, tmp03^0'=tmp03^0, tmp1011^0'=tmp1011^0, tmp1112^0'=tmp1112^0, tmp1213^0'=tmp1213^0, tmp1314^0'=tmp1314^0, tmp14^0'=tmp14^0, tmp25^0'=tmp25^0, tmp36^0'=tmp36^0, tmp47^0'=tmp47^0, tmp58^0'=tmp58^0, tmp69^0'=tmp69^0, tmp710^0'=tmp710^0, z115^0'=z115^0, z216^0'=z216^0, z317^0'=z317^0, z418^0'=z418^0, z519^0'=z519^0, (0 == 0 /\ 8-i20^0 <= 0), cost: 1 propagated equality lx2^post1 = lx2^0 propagated equality tmp1314^post1 = tmp1314^0 propagated equality tmp03^post1 = tmp03^0 propagated equality tmp710^post1 = tmp710^0 propagated equality tmp14^post1 = tmp14^0 propagated equality tmp69^post1 = tmp69^0 propagated equality tmp25^post1 = tmp25^0 propagated equality tmp47^post1 = tmp47^0 propagated equality tmp1112^post1 = tmp1112^0 propagated equality tmp1011^post1 = tmp1011^0 propagated equality z115^post1 = z115^0 propagated equality i20^post1 = 0 propagated equality z216^post1 = z216^0 propagated equality z317^post1 = z317^0 propagated equality z519^post1 = z519^0 propagated equality z418^post1 = z418^0 propagated equality tmp1213^post1 = tmp1213^0 propagated equality constant22^post1 = constant22^0 propagated equality tmp36^post1 = tmp36^0 propagated equality tmp58^post1 = tmp58^0 Simplified Guard Original rule: l0 -> l1 : constant22^0'=constant22^0, i20^0'=0, lx2^0'=lx2^0, tmp03^0'=tmp03^0, tmp1011^0'=tmp1011^0, tmp1112^0'=tmp1112^0, tmp1213^0'=tmp1213^0, tmp1314^0'=tmp1314^0, tmp14^0'=tmp14^0, tmp25^0'=tmp25^0, tmp36^0'=tmp36^0, tmp47^0'=tmp47^0, tmp58^0'=tmp58^0, tmp69^0'=tmp69^0, tmp710^0'=tmp710^0, z115^0'=z115^0, z216^0'=z216^0, z317^0'=z317^0, z418^0'=z418^0, z519^0'=z519^0, (0 == 0 /\ 8-i20^0 <= 0), cost: 1 New rule: l0 -> l1 : constant22^0'=constant22^0, i20^0'=0, lx2^0'=lx2^0, tmp03^0'=tmp03^0, tmp1011^0'=tmp1011^0, tmp1112^0'=tmp1112^0, tmp1213^0'=tmp1213^0, tmp1314^0'=tmp1314^0, tmp14^0'=tmp14^0, tmp25^0'=tmp25^0, tmp36^0'=tmp36^0, tmp47^0'=tmp47^0, tmp58^0'=tmp58^0, tmp69^0'=tmp69^0, tmp710^0'=tmp710^0, z115^0'=z115^0, z216^0'=z216^0, z317^0'=z317^0, z418^0'=z418^0, z519^0'=z519^0, 8-i20^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l0 -> l1 : constant22^0'=constant22^0, i20^0'=0, lx2^0'=lx2^0, tmp03^0'=tmp03^0, tmp1011^0'=tmp1011^0, tmp1112^0'=tmp1112^0, tmp1213^0'=tmp1213^0, tmp1314^0'=tmp1314^0, tmp14^0'=tmp14^0, tmp25^0'=tmp25^0, tmp36^0'=tmp36^0, tmp47^0'=tmp47^0, tmp58^0'=tmp58^0, tmp69^0'=tmp69^0, tmp710^0'=tmp710^0, z115^0'=z115^0, z216^0'=z216^0, z317^0'=z317^0, z418^0'=z418^0, z519^0'=z519^0, 8-i20^0 <= 0, cost: 1 New rule: l0 -> l1 : i20^0'=0, 8-i20^0 <= 0, cost: 1 Propagated Equalities Original rule: l0 -> l2 : constant22^0'=constant22^post2, i20^0'=i20^post2, lx2^0'=lx2^post2, tmp03^0'=tmp03^post2, tmp1011^0'=tmp1011^post2, tmp1112^0'=tmp1112^post2, tmp1213^0'=tmp1213^post2, tmp1314^0'=tmp1314^post2, tmp14^0'=tmp14^post2, tmp25^0'=tmp25^post2, tmp36^0'=tmp36^post2, tmp47^0'=tmp47^post2, tmp58^0'=tmp58^post2, tmp69^0'=tmp69^post2, tmp710^0'=tmp710^post2, z115^0'=z115^post2, z216^0'=z216^post2, z317^0'=z317^post2, z418^0'=z418^post2, z519^0'=z519^post2, (0 == 0 /\ 20995+constant22^10 == 0 /\ -2446+constant22^5 == 0 /\ 7373+constant22^9 == 0 /\ tmp1314^post2-tmp03^post2+tmp36^post2 == 0 /\ -lx2^post2+lx2^0 == 0 /\ 16069+constant22^11 == 0 /\ -6270+constant22^2 == 0 /\ -9633+constant22^4 == 0 /\ -25172+constant22^7 == 0 /\ -tmp14^post2+tmp25^post2+tmp1213^post2 == 0 /\ z418^1-tmp58^1-tmp710^1 == 0 /\ -1+i20^post2-i20^0 == 0 /\ 15137+constant22^3 == 0 /\ -12299+constant22^8 == 0 /\ z317^post2-z317^2-z519^post2 == 0 /\ tmp1011^post2-tmp03^post2-tmp36^post2 == 0 /\ z418^post2-z418^2-z519^post2 == 0 /\ -tmp14^post2+tmp1112^post2-tmp25^post2 == 0 /\ -16819+constant22^6 == 0 /\ 3196+constant22^post2 == 0 /\ z317^1-tmp69^1-tmp47^1 == 0 /\ -tmp69^1-tmp58^1+z216^1 == 0 /\ -7+i20^0 <= 0 /\ z115^2-tmp47^1-tmp710^1 == 0 /\ -4433+constant22^1 == 0), cost: 1 New rule: l0 -> l2 : constant22^0'=-3196, i20^0'=1+i20^0, lx2^0'=lx2^0, tmp03^0'=tmp1314^post2+tmp36^post2, tmp1011^0'=tmp1314^post2+2*tmp36^post2, tmp1112^0'=tmp14^post2+tmp25^post2, tmp1213^0'=tmp14^post2-tmp25^post2, tmp1314^0'=tmp1314^post2, tmp14^0'=tmp14^post2, tmp25^0'=tmp25^post2, tmp36^0'=tmp36^post2, tmp47^0'=tmp47^post2, tmp58^0'=tmp58^post2, tmp69^0'=tmp69^post2, tmp710^0'=tmp710^post2, z115^0'=z115^post2, z216^0'=z216^post2, z317^0'=z317^2+z519^post2, z418^0'=z418^2+z519^post2, z519^0'=z519^post2, (0 == 0 /\ 20995+constant22^10 == 0 /\ -2446+constant22^5 == 0 /\ 7373+constant22^9 == 0 /\ 16069+constant22^11 == 0 /\ -6270+constant22^2 == 0 /\ -9633+constant22^4 == 0 /\ -25172+constant22^7 == 0 /\ z418^1-tmp58^1-tmp710^1 == 0 /\ 15137+constant22^3 == 0 /\ -12299+constant22^8 == 0 /\ -16819+constant22^6 == 0 /\ z317^1-tmp69^1-tmp47^1 == 0 /\ -tmp69^1-tmp58^1+z216^1 == 0 /\ -7+i20^0 <= 0 /\ z115^2-tmp47^1-tmp710^1 == 0 /\ -4433+constant22^1 == 0), cost: 1 propagated equality tmp03^post2 = tmp1314^post2+tmp36^post2 propagated equality lx2^post2 = lx2^0 propagated equality tmp1213^post2 = tmp14^post2-tmp25^post2 propagated equality i20^post2 = 1+i20^0 propagated equality z317^post2 = z317^2+z519^post2 propagated equality tmp1011^post2 = tmp1314^post2+2*tmp36^post2 propagated equality z418^post2 = z418^2+z519^post2 propagated equality tmp1112^post2 = tmp14^post2+tmp25^post2 propagated equality constant22^post2 = -3196 Propagated Equalities Original rule: l0 -> l2 : constant22^0'=-3196, i20^0'=1+i20^0, lx2^0'=lx2^0, tmp03^0'=tmp1314^post2+tmp36^post2, tmp1011^0'=tmp1314^post2+2*tmp36^post2, tmp1112^0'=tmp14^post2+tmp25^post2, tmp1213^0'=tmp14^post2-tmp25^post2, tmp1314^0'=tmp1314^post2, tmp14^0'=tmp14^post2, tmp25^0'=tmp25^post2, tmp36^0'=tmp36^post2, tmp47^0'=tmp47^post2, tmp58^0'=tmp58^post2, tmp69^0'=tmp69^post2, tmp710^0'=tmp710^post2, z115^0'=z115^post2, z216^0'=z216^post2, z317^0'=z317^2+z519^post2, z418^0'=z418^2+z519^post2, z519^0'=z519^post2, (0 == 0 /\ 20995+constant22^10 == 0 /\ -2446+constant22^5 == 0 /\ 7373+constant22^9 == 0 /\ 16069+constant22^11 == 0 /\ -6270+constant22^2 == 0 /\ -9633+constant22^4 == 0 /\ -25172+constant22^7 == 0 /\ z418^1-tmp58^1-tmp710^1 == 0 /\ 15137+constant22^3 == 0 /\ -12299+constant22^8 == 0 /\ -16819+constant22^6 == 0 /\ z317^1-tmp69^1-tmp47^1 == 0 /\ -tmp69^1-tmp58^1+z216^1 == 0 /\ -7+i20^0 <= 0 /\ z115^2-tmp47^1-tmp710^1 == 0 /\ -4433+constant22^1 == 0), cost: 1 New rule: l0 -> l2 : constant22^0'=-3196, i20^0'=1+i20^0, lx2^0'=lx2^0, tmp03^0'=tmp1314^post2+tmp36^post2, tmp1011^0'=tmp1314^post2+2*tmp36^post2, tmp1112^0'=tmp14^post2+tmp25^post2, tmp1213^0'=tmp14^post2-tmp25^post2, tmp1314^0'=tmp1314^post2, tmp14^0'=tmp14^post2, tmp25^0'=tmp25^post2, tmp36^0'=tmp36^post2, tmp47^0'=tmp47^post2, tmp58^0'=tmp58^post2, tmp69^0'=tmp69^post2, tmp710^0'=tmp710^post2, z115^0'=z115^post2, z216^0'=z216^post2, z317^0'=z317^2+z519^post2, z418^0'=z418^2+z519^post2, z519^0'=z519^post2, (0 == 0 /\ -7+i20^0 <= 0), cost: 1 propagated equality constant22^10 = -20995 propagated equality constant22^5 = 2446 propagated equality constant22^9 = -7373 propagated equality constant22^11 = -16069 propagated equality constant22^2 = 6270 propagated equality constant22^4 = 9633 propagated equality constant22^7 = 25172 propagated equality tmp58^1 = z418^1-tmp710^1 propagated equality constant22^3 = -15137 propagated equality constant22^8 = 12299 propagated equality constant22^6 = 16819 propagated equality tmp47^1 = z317^1-tmp69^1 propagated equality tmp69^1 = -z418^1+z216^1+tmp710^1 propagated equality z115^2 = z317^1+z418^1-z216^1 propagated equality constant22^1 = 4433 Simplified Guard Original rule: l0 -> l2 : constant22^0'=-3196, i20^0'=1+i20^0, lx2^0'=lx2^0, tmp03^0'=tmp1314^post2+tmp36^post2, tmp1011^0'=tmp1314^post2+2*tmp36^post2, tmp1112^0'=tmp14^post2+tmp25^post2, tmp1213^0'=tmp14^post2-tmp25^post2, tmp1314^0'=tmp1314^post2, tmp14^0'=tmp14^post2, tmp25^0'=tmp25^post2, tmp36^0'=tmp36^post2, tmp47^0'=tmp47^post2, tmp58^0'=tmp58^post2, tmp69^0'=tmp69^post2, tmp710^0'=tmp710^post2, z115^0'=z115^post2, z216^0'=z216^post2, z317^0'=z317^2+z519^post2, z418^0'=z418^2+z519^post2, z519^0'=z519^post2, (0 == 0 /\ -7+i20^0 <= 0), cost: 1 New rule: l0 -> l2 : constant22^0'=-3196, i20^0'=1+i20^0, lx2^0'=lx2^0, tmp03^0'=tmp1314^post2+tmp36^post2, tmp1011^0'=tmp1314^post2+2*tmp36^post2, tmp1112^0'=tmp14^post2+tmp25^post2, tmp1213^0'=tmp14^post2-tmp25^post2, tmp1314^0'=tmp1314^post2, tmp14^0'=tmp14^post2, tmp25^0'=tmp25^post2, tmp36^0'=tmp36^post2, tmp47^0'=tmp47^post2, tmp58^0'=tmp58^post2, tmp69^0'=tmp69^post2, tmp710^0'=tmp710^post2, z115^0'=z115^post2, z216^0'=z216^post2, z317^0'=z317^2+z519^post2, z418^0'=z418^2+z519^post2, z519^0'=z519^post2, -7+i20^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l0 -> l2 : constant22^0'=-3196, i20^0'=1+i20^0, lx2^0'=lx2^0, tmp03^0'=tmp1314^post2+tmp36^post2, tmp1011^0'=tmp1314^post2+2*tmp36^post2, tmp1112^0'=tmp14^post2+tmp25^post2, tmp1213^0'=tmp14^post2-tmp25^post2, tmp1314^0'=tmp1314^post2, tmp14^0'=tmp14^post2, tmp25^0'=tmp25^post2, tmp36^0'=tmp36^post2, tmp47^0'=tmp47^post2, tmp58^0'=tmp58^post2, tmp69^0'=tmp69^post2, tmp710^0'=tmp710^post2, z115^0'=z115^post2, z216^0'=z216^post2, z317^0'=z317^2+z519^post2, z418^0'=z418^2+z519^post2, z519^0'=z519^post2, -7+i20^0 <= 0, cost: 1 New rule: l0 -> l2 : constant22^0'=-3196, i20^0'=1+i20^0, tmp03^0'=tmp1314^post2+tmp36^post2, tmp1011^0'=tmp1314^post2+2*tmp36^post2, tmp1112^0'=tmp14^post2+tmp25^post2, tmp1213^0'=tmp14^post2-tmp25^post2, tmp1314^0'=tmp1314^post2, tmp14^0'=tmp14^post2, tmp25^0'=tmp25^post2, tmp36^0'=tmp36^post2, tmp47^0'=tmp47^post2, tmp58^0'=tmp58^post2, tmp69^0'=tmp69^post2, tmp710^0'=tmp710^post2, z115^0'=z115^post2, z216^0'=z216^post2, z317^0'=z317^2+z519^post2, z418^0'=z418^2+z519^post2, z519^0'=z519^post2, -7+i20^0 <= 0, cost: 1 Propagated Equalities Original rule: l3 -> l4 : constant22^0'=constant22^post3, i20^0'=i20^post3, lx2^0'=lx2^post3, tmp03^0'=tmp03^post3, tmp1011^0'=tmp1011^post3, tmp1112^0'=tmp1112^post3, tmp1213^0'=tmp1213^post3, tmp1314^0'=tmp1314^post3, tmp14^0'=tmp14^post3, tmp25^0'=tmp25^post3, tmp36^0'=tmp36^post3, tmp47^0'=tmp47^post3, tmp58^0'=tmp58^post3, tmp69^0'=tmp69^post3, tmp710^0'=tmp710^post3, z115^0'=z115^post3, z216^0'=z216^post3, z317^0'=z317^post3, z418^0'=z418^post3, z519^0'=z519^post3, (-z115^post3+z115^0 == 0 /\ z519^0-z519^post3 == 0 /\ tmp58^0-tmp58^post3 == 0 /\ tmp1213^0-tmp1213^post3 == 0 /\ -z216^post3+z216^0 == 0 /\ -tmp14^post3+tmp14^0 == 0 /\ 8-i20^0 <= 0 /\ z317^0-z317^post3 == 0 /\ -tmp1112^post3+tmp1112^0 == 0 /\ -tmp36^post3+tmp36^0 == 0 /\ -tmp710^post3+tmp710^0 == 0 /\ -i20^post3+i20^0 == 0 /\ tmp1314^0-tmp1314^post3 == 0 /\ tmp1011^0-tmp1011^post3 == 0 /\ constant22^0-constant22^post3 == 0 /\ tmp25^0-tmp25^post3 == 0 /\ -lx2^post3+lx2^0 == 0 /\ tmp03^0-tmp03^post3 == 0 /\ -tmp69^post3+tmp69^0 == 0 /\ -z418^post3+z418^0 == 0 /\ -tmp47^post3+tmp47^0 == 0), cost: 1 New rule: l3 -> l4 : constant22^0'=constant22^0, i20^0'=i20^0, lx2^0'=lx2^0, tmp03^0'=tmp03^0, tmp1011^0'=tmp1011^0, tmp1112^0'=tmp1112^0, tmp1213^0'=tmp1213^0, tmp1314^0'=tmp1314^0, tmp14^0'=tmp14^0, tmp25^0'=tmp25^0, tmp36^0'=tmp36^0, tmp47^0'=tmp47^0, tmp58^0'=tmp58^0, tmp69^0'=tmp69^0, tmp710^0'=tmp710^0, z115^0'=z115^0, z216^0'=z216^0, z317^0'=z317^0, z418^0'=z418^0, z519^0'=z519^0, (0 == 0 /\ 8-i20^0 <= 0), cost: 1 propagated equality z115^post3 = z115^0 propagated equality z519^post3 = z519^0 propagated equality tmp58^post3 = tmp58^0 propagated equality tmp1213^post3 = tmp1213^0 propagated equality z216^post3 = z216^0 propagated equality tmp14^post3 = tmp14^0 propagated equality z317^post3 = z317^0 propagated equality tmp1112^post3 = tmp1112^0 propagated equality tmp36^post3 = tmp36^0 propagated equality tmp710^post3 = tmp710^0 propagated equality i20^post3 = i20^0 propagated equality tmp1314^post3 = tmp1314^0 propagated equality tmp1011^post3 = tmp1011^0 propagated equality constant22^post3 = constant22^0 propagated equality tmp25^post3 = tmp25^0 propagated equality lx2^post3 = lx2^0 propagated equality tmp03^post3 = tmp03^0 propagated equality tmp69^post3 = tmp69^0 propagated equality z418^post3 = z418^0 propagated equality tmp47^post3 = tmp47^0 Simplified Guard Original rule: l3 -> l4 : constant22^0'=constant22^0, i20^0'=i20^0, lx2^0'=lx2^0, tmp03^0'=tmp03^0, tmp1011^0'=tmp1011^0, tmp1112^0'=tmp1112^0, tmp1213^0'=tmp1213^0, tmp1314^0'=tmp1314^0, tmp14^0'=tmp14^0, tmp25^0'=tmp25^0, tmp36^0'=tmp36^0, tmp47^0'=tmp47^0, tmp58^0'=tmp58^0, tmp69^0'=tmp69^0, tmp710^0'=tmp710^0, z115^0'=z115^0, z216^0'=z216^0, z317^0'=z317^0, z418^0'=z418^0, z519^0'=z519^0, (0 == 0 /\ 8-i20^0 <= 0), cost: 1 New rule: l3 -> l4 : constant22^0'=constant22^0, i20^0'=i20^0, lx2^0'=lx2^0, tmp03^0'=tmp03^0, tmp1011^0'=tmp1011^0, tmp1112^0'=tmp1112^0, tmp1213^0'=tmp1213^0, tmp1314^0'=tmp1314^0, tmp14^0'=tmp14^0, tmp25^0'=tmp25^0, tmp36^0'=tmp36^0, tmp47^0'=tmp47^0, tmp58^0'=tmp58^0, tmp69^0'=tmp69^0, tmp710^0'=tmp710^0, z115^0'=z115^0, z216^0'=z216^0, z317^0'=z317^0, z418^0'=z418^0, z519^0'=z519^0, 8-i20^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l3 -> l4 : constant22^0'=constant22^0, i20^0'=i20^0, lx2^0'=lx2^0, tmp03^0'=tmp03^0, tmp1011^0'=tmp1011^0, tmp1112^0'=tmp1112^0, tmp1213^0'=tmp1213^0, tmp1314^0'=tmp1314^0, tmp14^0'=tmp14^0, tmp25^0'=tmp25^0, tmp36^0'=tmp36^0, tmp47^0'=tmp47^0, tmp58^0'=tmp58^0, tmp69^0'=tmp69^0, tmp710^0'=tmp710^0, z115^0'=z115^0, z216^0'=z216^0, z317^0'=z317^0, z418^0'=z418^0, z519^0'=z519^0, 8-i20^0 <= 0, cost: 1 New rule: l3 -> l4 : 8-i20^0 <= 0, cost: 1 Propagated Equalities Original rule: l3 -> l1 : constant22^0'=constant22^post4, i20^0'=i20^post4, lx2^0'=lx2^post4, tmp03^0'=tmp03^post4, tmp1011^0'=tmp1011^post4, tmp1112^0'=tmp1112^post4, tmp1213^0'=tmp1213^post4, tmp1314^0'=tmp1314^post4, tmp14^0'=tmp14^post4, tmp25^0'=tmp25^post4, tmp36^0'=tmp36^post4, tmp47^0'=tmp47^post4, tmp58^0'=tmp58^post4, tmp69^0'=tmp69^post4, tmp710^0'=tmp710^post4, z115^0'=z115^post4, z216^0'=z216^post4, z317^0'=z317^post4, z418^0'=z418^post4, z519^0'=z519^post4, (0 == 0 /\ 20995+constant22^10 == 0 /\ -2446+constant22^5 == 0 /\ 7373+constant22^9 == 0 /\ -tmp14^post4+tmp1112^post4-tmp25^post4 == 0 /\ 3196+constant22^post4 == 0 /\ -tmp03^post4-tmp36^post4+tmp1011^post4 == 0 /\ 16069+constant22^11 == 0 /\ -6270+constant22^2 == 0 /\ -lx2^post4+lx2^0 == 0 /\ -9633+constant22^4 == 0 /\ -25172+constant22^7 == 0 /\ z418^1-tmp58^1-tmp710^1 == 0 /\ -z317^2-z519^post4+z317^post4 == 0 /\ 15137+constant22^3 == 0 /\ -12299+constant22^8 == 0 /\ -tmp03^post4+tmp36^post4+tmp1314^post4 == 0 /\ -16819+constant22^6 == 0 /\ -tmp14^post4+tmp25^post4+tmp1213^post4 == 0 /\ z317^1-tmp69^1-tmp47^1 == 0 /\ -tmp69^1-tmp58^1+z216^1 == 0 /\ -7+i20^0 <= 0 /\ -1+i20^post4-i20^0 == 0 /\ z115^2-tmp47^1-tmp710^1 == 0 /\ z418^post4-z519^post4-z418^2 == 0 /\ -4433+constant22^1 == 0), cost: 1 New rule: l3 -> l1 : constant22^0'=-3196, i20^0'=1+i20^0, lx2^0'=lx2^0, tmp03^0'=tmp36^post4+tmp1314^post4, tmp1011^0'=2*tmp36^post4+tmp1314^post4, tmp1112^0'=tmp14^post4+tmp25^post4, tmp1213^0'=tmp14^post4-tmp25^post4, tmp1314^0'=tmp1314^post4, tmp14^0'=tmp14^post4, tmp25^0'=tmp25^post4, tmp36^0'=tmp36^post4, tmp47^0'=tmp47^post4, tmp58^0'=tmp58^post4, tmp69^0'=tmp69^post4, tmp710^0'=tmp710^post4, z115^0'=z115^post4, z216^0'=z216^post4, z317^0'=z317^2+z519^post4, z418^0'=z519^post4+z418^2, z519^0'=z519^post4, (0 == 0 /\ 20995+constant22^10 == 0 /\ -2446+constant22^5 == 0 /\ 7373+constant22^9 == 0 /\ 16069+constant22^11 == 0 /\ -6270+constant22^2 == 0 /\ -9633+constant22^4 == 0 /\ -25172+constant22^7 == 0 /\ z418^1-tmp58^1-tmp710^1 == 0 /\ 15137+constant22^3 == 0 /\ -12299+constant22^8 == 0 /\ -16819+constant22^6 == 0 /\ z317^1-tmp69^1-tmp47^1 == 0 /\ -tmp69^1-tmp58^1+z216^1 == 0 /\ -7+i20^0 <= 0 /\ z115^2-tmp47^1-tmp710^1 == 0 /\ -4433+constant22^1 == 0), cost: 1 propagated equality tmp1112^post4 = tmp14^post4+tmp25^post4 propagated equality constant22^post4 = -3196 propagated equality tmp03^post4 = -tmp36^post4+tmp1011^post4 propagated equality lx2^post4 = lx2^0 propagated equality z317^post4 = z317^2+z519^post4 propagated equality tmp1011^post4 = 2*tmp36^post4+tmp1314^post4 propagated equality tmp1213^post4 = tmp14^post4-tmp25^post4 propagated equality i20^post4 = 1+i20^0 propagated equality z418^post4 = z519^post4+z418^2 Propagated Equalities Original rule: l3 -> l1 : constant22^0'=-3196, i20^0'=1+i20^0, lx2^0'=lx2^0, tmp03^0'=tmp36^post4+tmp1314^post4, tmp1011^0'=2*tmp36^post4+tmp1314^post4, tmp1112^0'=tmp14^post4+tmp25^post4, tmp1213^0'=tmp14^post4-tmp25^post4, tmp1314^0'=tmp1314^post4, tmp14^0'=tmp14^post4, tmp25^0'=tmp25^post4, tmp36^0'=tmp36^post4, tmp47^0'=tmp47^post4, tmp58^0'=tmp58^post4, tmp69^0'=tmp69^post4, tmp710^0'=tmp710^post4, z115^0'=z115^post4, z216^0'=z216^post4, z317^0'=z317^2+z519^post4, z418^0'=z519^post4+z418^2, z519^0'=z519^post4, (0 == 0 /\ 20995+constant22^10 == 0 /\ -2446+constant22^5 == 0 /\ 7373+constant22^9 == 0 /\ 16069+constant22^11 == 0 /\ -6270+constant22^2 == 0 /\ -9633+constant22^4 == 0 /\ -25172+constant22^7 == 0 /\ z418^1-tmp58^1-tmp710^1 == 0 /\ 15137+constant22^3 == 0 /\ -12299+constant22^8 == 0 /\ -16819+constant22^6 == 0 /\ z317^1-tmp69^1-tmp47^1 == 0 /\ -tmp69^1-tmp58^1+z216^1 == 0 /\ -7+i20^0 <= 0 /\ z115^2-tmp47^1-tmp710^1 == 0 /\ -4433+constant22^1 == 0), cost: 1 New rule: l3 -> l1 : constant22^0'=-3196, i20^0'=1+i20^0, lx2^0'=lx2^0, tmp03^0'=tmp36^post4+tmp1314^post4, tmp1011^0'=2*tmp36^post4+tmp1314^post4, tmp1112^0'=tmp14^post4+tmp25^post4, tmp1213^0'=tmp14^post4-tmp25^post4, tmp1314^0'=tmp1314^post4, tmp14^0'=tmp14^post4, tmp25^0'=tmp25^post4, tmp36^0'=tmp36^post4, tmp47^0'=tmp47^post4, tmp58^0'=tmp58^post4, tmp69^0'=tmp69^post4, tmp710^0'=tmp710^post4, z115^0'=z115^post4, z216^0'=z216^post4, z317^0'=z317^2+z519^post4, z418^0'=z519^post4+z418^2, z519^0'=z519^post4, (0 == 0 /\ -7+i20^0 <= 0), cost: 1 propagated equality constant22^10 = -20995 propagated equality constant22^5 = 2446 propagated equality constant22^9 = -7373 propagated equality constant22^11 = -16069 propagated equality constant22^2 = 6270 propagated equality constant22^4 = 9633 propagated equality constant22^7 = 25172 propagated equality tmp58^1 = z418^1-tmp710^1 propagated equality constant22^3 = -15137 propagated equality constant22^8 = 12299 propagated equality constant22^6 = 16819 propagated equality tmp47^1 = z317^1-tmp69^1 propagated equality tmp69^1 = -z418^1+z216^1+tmp710^1 propagated equality z115^2 = z317^1+z418^1-z216^1 propagated equality constant22^1 = 4433 Simplified Guard Original rule: l3 -> l1 : constant22^0'=-3196, i20^0'=1+i20^0, lx2^0'=lx2^0, tmp03^0'=tmp36^post4+tmp1314^post4, tmp1011^0'=2*tmp36^post4+tmp1314^post4, tmp1112^0'=tmp14^post4+tmp25^post4, tmp1213^0'=tmp14^post4-tmp25^post4, tmp1314^0'=tmp1314^post4, tmp14^0'=tmp14^post4, tmp25^0'=tmp25^post4, tmp36^0'=tmp36^post4, tmp47^0'=tmp47^post4, tmp58^0'=tmp58^post4, tmp69^0'=tmp69^post4, tmp710^0'=tmp710^post4, z115^0'=z115^post4, z216^0'=z216^post4, z317^0'=z317^2+z519^post4, z418^0'=z519^post4+z418^2, z519^0'=z519^post4, (0 == 0 /\ -7+i20^0 <= 0), cost: 1 New rule: l3 -> l1 : constant22^0'=-3196, i20^0'=1+i20^0, lx2^0'=lx2^0, tmp03^0'=tmp36^post4+tmp1314^post4, tmp1011^0'=2*tmp36^post4+tmp1314^post4, tmp1112^0'=tmp14^post4+tmp25^post4, tmp1213^0'=tmp14^post4-tmp25^post4, tmp1314^0'=tmp1314^post4, tmp14^0'=tmp14^post4, tmp25^0'=tmp25^post4, tmp36^0'=tmp36^post4, tmp47^0'=tmp47^post4, tmp58^0'=tmp58^post4, tmp69^0'=tmp69^post4, tmp710^0'=tmp710^post4, z115^0'=z115^post4, z216^0'=z216^post4, z317^0'=z317^2+z519^post4, z418^0'=z519^post4+z418^2, z519^0'=z519^post4, -7+i20^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l3 -> l1 : constant22^0'=-3196, i20^0'=1+i20^0, lx2^0'=lx2^0, tmp03^0'=tmp36^post4+tmp1314^post4, tmp1011^0'=2*tmp36^post4+tmp1314^post4, tmp1112^0'=tmp14^post4+tmp25^post4, tmp1213^0'=tmp14^post4-tmp25^post4, tmp1314^0'=tmp1314^post4, tmp14^0'=tmp14^post4, tmp25^0'=tmp25^post4, tmp36^0'=tmp36^post4, tmp47^0'=tmp47^post4, tmp58^0'=tmp58^post4, tmp69^0'=tmp69^post4, tmp710^0'=tmp710^post4, z115^0'=z115^post4, z216^0'=z216^post4, z317^0'=z317^2+z519^post4, z418^0'=z519^post4+z418^2, z519^0'=z519^post4, -7+i20^0 <= 0, cost: 1 New rule: l3 -> l1 : constant22^0'=-3196, i20^0'=1+i20^0, tmp03^0'=tmp36^post4+tmp1314^post4, tmp1011^0'=2*tmp36^post4+tmp1314^post4, tmp1112^0'=tmp14^post4+tmp25^post4, tmp1213^0'=tmp14^post4-tmp25^post4, tmp1314^0'=tmp1314^post4, tmp14^0'=tmp14^post4, tmp25^0'=tmp25^post4, tmp36^0'=tmp36^post4, tmp47^0'=tmp47^post4, tmp58^0'=tmp58^post4, tmp69^0'=tmp69^post4, tmp710^0'=tmp710^post4, z115^0'=z115^post4, z216^0'=z216^post4, z317^0'=z317^2+z519^post4, z418^0'=z519^post4+z418^2, z519^0'=z519^post4, -7+i20^0 <= 0, cost: 1 Propagated Equalities Original rule: l2 -> l0 : constant22^0'=constant22^post5, i20^0'=i20^post5, lx2^0'=lx2^post5, tmp03^0'=tmp03^post5, tmp1011^0'=tmp1011^post5, tmp1112^0'=tmp1112^post5, tmp1213^0'=tmp1213^post5, tmp1314^0'=tmp1314^post5, tmp14^0'=tmp14^post5, tmp25^0'=tmp25^post5, tmp36^0'=tmp36^post5, tmp47^0'=tmp47^post5, tmp58^0'=tmp58^post5, tmp69^0'=tmp69^post5, tmp710^0'=tmp710^post5, z115^0'=z115^post5, z216^0'=z216^post5, z317^0'=z317^post5, z418^0'=z418^post5, z519^0'=z519^post5, (-tmp1112^post5+tmp1112^0 == 0 /\ -tmp47^post5+tmp47^0 == 0 /\ -tmp1011^post5+tmp1011^0 == 0 /\ -tmp14^post5+tmp14^0 == 0 /\ -tmp1314^post5+tmp1314^0 == 0 /\ -tmp36^post5+tmp36^0 == 0 /\ -lx2^post5+lx2^0 == 0 /\ z216^0-z216^post5 == 0 /\ -z115^post5+z115^0 == 0 /\ tmp25^0-tmp25^post5 == 0 /\ -z317^post5+z317^0 == 0 /\ tmp1213^0-tmp1213^post5 == 0 /\ tmp58^0-tmp58^post5 == 0 /\ -tmp710^post5+tmp710^0 == 0 /\ -i20^post5+i20^0 == 0 /\ tmp69^0-tmp69^post5 == 0 /\ tmp03^0-tmp03^post5 == 0 /\ z519^0-z519^post5 == 0 /\ -z418^post5+z418^0 == 0 /\ constant22^0-constant22^post5 == 0), cost: 1 New rule: l2 -> l0 : constant22^0'=constant22^0, i20^0'=i20^0, lx2^0'=lx2^0, tmp03^0'=tmp03^0, tmp1011^0'=tmp1011^0, tmp1112^0'=tmp1112^0, tmp1213^0'=tmp1213^0, tmp1314^0'=tmp1314^0, tmp14^0'=tmp14^0, tmp25^0'=tmp25^0, tmp36^0'=tmp36^0, tmp47^0'=tmp47^0, tmp58^0'=tmp58^0, tmp69^0'=tmp69^0, tmp710^0'=tmp710^0, z115^0'=z115^0, z216^0'=z216^0, z317^0'=z317^0, z418^0'=z418^0, z519^0'=z519^0, 0 == 0, cost: 1 propagated equality tmp1112^post5 = tmp1112^0 propagated equality tmp47^post5 = tmp47^0 propagated equality tmp1011^post5 = tmp1011^0 propagated equality tmp14^post5 = tmp14^0 propagated equality tmp1314^post5 = tmp1314^0 propagated equality tmp36^post5 = tmp36^0 propagated equality lx2^post5 = lx2^0 propagated equality z216^post5 = z216^0 propagated equality z115^post5 = z115^0 propagated equality tmp25^post5 = tmp25^0 propagated equality z317^post5 = z317^0 propagated equality tmp1213^post5 = tmp1213^0 propagated equality tmp58^post5 = tmp58^0 propagated equality tmp710^post5 = tmp710^0 propagated equality i20^post5 = i20^0 propagated equality tmp69^post5 = tmp69^0 propagated equality tmp03^post5 = tmp03^0 propagated equality z519^post5 = z519^0 propagated equality z418^post5 = z418^0 propagated equality constant22^post5 = constant22^0 Simplified Guard Original rule: l2 -> l0 : constant22^0'=constant22^0, i20^0'=i20^0, lx2^0'=lx2^0, tmp03^0'=tmp03^0, tmp1011^0'=tmp1011^0, tmp1112^0'=tmp1112^0, tmp1213^0'=tmp1213^0, tmp1314^0'=tmp1314^0, tmp14^0'=tmp14^0, tmp25^0'=tmp25^0, tmp36^0'=tmp36^0, tmp47^0'=tmp47^0, tmp58^0'=tmp58^0, tmp69^0'=tmp69^0, tmp710^0'=tmp710^0, z115^0'=z115^0, z216^0'=z216^0, z317^0'=z317^0, z418^0'=z418^0, z519^0'=z519^0, 0 == 0, cost: 1 New rule: l2 -> l0 : constant22^0'=constant22^0, i20^0'=i20^0, lx2^0'=lx2^0, tmp03^0'=tmp03^0, tmp1011^0'=tmp1011^0, tmp1112^0'=tmp1112^0, tmp1213^0'=tmp1213^0, tmp1314^0'=tmp1314^0, tmp14^0'=tmp14^0, tmp25^0'=tmp25^0, tmp36^0'=tmp36^0, tmp47^0'=tmp47^0, tmp58^0'=tmp58^0, tmp69^0'=tmp69^0, tmp710^0'=tmp710^0, z115^0'=z115^0, z216^0'=z216^0, z317^0'=z317^0, z418^0'=z418^0, z519^0'=z519^0, T, cost: 1 Removed Trivial Updates Original rule: l2 -> l0 : constant22^0'=constant22^0, i20^0'=i20^0, lx2^0'=lx2^0, tmp03^0'=tmp03^0, tmp1011^0'=tmp1011^0, tmp1112^0'=tmp1112^0, tmp1213^0'=tmp1213^0, tmp1314^0'=tmp1314^0, tmp14^0'=tmp14^0, tmp25^0'=tmp25^0, tmp36^0'=tmp36^0, tmp47^0'=tmp47^0, tmp58^0'=tmp58^0, tmp69^0'=tmp69^0, tmp710^0'=tmp710^0, z115^0'=z115^0, z216^0'=z216^0, z317^0'=z317^0, z418^0'=z418^0, z519^0'=z519^0, T, cost: 1 New rule: l2 -> l0 : T, cost: 1 Propagated Equalities Original rule: l1 -> l3 : constant22^0'=constant22^post6, i20^0'=i20^post6, lx2^0'=lx2^post6, tmp03^0'=tmp03^post6, tmp1011^0'=tmp1011^post6, tmp1112^0'=tmp1112^post6, tmp1213^0'=tmp1213^post6, tmp1314^0'=tmp1314^post6, tmp14^0'=tmp14^post6, tmp25^0'=tmp25^post6, tmp36^0'=tmp36^post6, tmp47^0'=tmp47^post6, tmp58^0'=tmp58^post6, tmp69^0'=tmp69^post6, tmp710^0'=tmp710^post6, z115^0'=z115^post6, z216^0'=z216^post6, z317^0'=z317^post6, z418^0'=z418^post6, z519^0'=z519^post6, (z519^0-z519^post6 == 0 /\ tmp58^0-tmp58^post6 == 0 /\ -tmp36^post6+tmp36^0 == 0 /\ z317^0-z317^post6 == 0 /\ -tmp1112^post6+tmp1112^0 == 0 /\ tmp25^0-tmp25^post6 == 0 /\ tmp1213^0-tmp1213^post6 == 0 /\ -z115^post6+z115^0 == 0 /\ -tmp1314^post6+tmp1314^0 == 0 /\ -tmp710^post6+tmp710^0 == 0 /\ -i20^post6+i20^0 == 0 /\ constant22^0-constant22^post6 == 0 /\ z216^0-z216^post6 == 0 /\ tmp1011^0-tmp1011^post6 == 0 /\ -tmp69^post6+tmp69^0 == 0 /\ -lx2^post6+lx2^0 == 0 /\ tmp03^0-tmp03^post6 == 0 /\ -tmp47^post6+tmp47^0 == 0 /\ -tmp14^post6+tmp14^0 == 0 /\ -z418^post6+z418^0 == 0), cost: 1 New rule: l1 -> l3 : constant22^0'=constant22^0, i20^0'=i20^0, lx2^0'=lx2^0, tmp03^0'=tmp03^0, tmp1011^0'=tmp1011^0, tmp1112^0'=tmp1112^0, tmp1213^0'=tmp1213^0, tmp1314^0'=tmp1314^0, tmp14^0'=tmp14^0, tmp25^0'=tmp25^0, tmp36^0'=tmp36^0, tmp47^0'=tmp47^0, tmp58^0'=tmp58^0, tmp69^0'=tmp69^0, tmp710^0'=tmp710^0, z115^0'=z115^0, z216^0'=z216^0, z317^0'=z317^0, z418^0'=z418^0, z519^0'=z519^0, 0 == 0, cost: 1 propagated equality z519^post6 = z519^0 propagated equality tmp58^post6 = tmp58^0 propagated equality tmp36^post6 = tmp36^0 propagated equality z317^post6 = z317^0 propagated equality tmp1112^post6 = tmp1112^0 propagated equality tmp25^post6 = tmp25^0 propagated equality tmp1213^post6 = tmp1213^0 propagated equality z115^post6 = z115^0 propagated equality tmp1314^post6 = tmp1314^0 propagated equality tmp710^post6 = tmp710^0 propagated equality i20^post6 = i20^0 propagated equality constant22^post6 = constant22^0 propagated equality z216^post6 = z216^0 propagated equality tmp1011^post6 = tmp1011^0 propagated equality tmp69^post6 = tmp69^0 propagated equality lx2^post6 = lx2^0 propagated equality tmp03^post6 = tmp03^0 propagated equality tmp47^post6 = tmp47^0 propagated equality tmp14^post6 = tmp14^0 propagated equality z418^post6 = z418^0 Simplified Guard Original rule: l1 -> l3 : constant22^0'=constant22^0, i20^0'=i20^0, lx2^0'=lx2^0, tmp03^0'=tmp03^0, tmp1011^0'=tmp1011^0, tmp1112^0'=tmp1112^0, tmp1213^0'=tmp1213^0, tmp1314^0'=tmp1314^0, tmp14^0'=tmp14^0, tmp25^0'=tmp25^0, tmp36^0'=tmp36^0, tmp47^0'=tmp47^0, tmp58^0'=tmp58^0, tmp69^0'=tmp69^0, tmp710^0'=tmp710^0, z115^0'=z115^0, z216^0'=z216^0, z317^0'=z317^0, z418^0'=z418^0, z519^0'=z519^0, 0 == 0, cost: 1 New rule: l1 -> l3 : constant22^0'=constant22^0, i20^0'=i20^0, lx2^0'=lx2^0, tmp03^0'=tmp03^0, tmp1011^0'=tmp1011^0, tmp1112^0'=tmp1112^0, tmp1213^0'=tmp1213^0, tmp1314^0'=tmp1314^0, tmp14^0'=tmp14^0, tmp25^0'=tmp25^0, tmp36^0'=tmp36^0, tmp47^0'=tmp47^0, tmp58^0'=tmp58^0, tmp69^0'=tmp69^0, tmp710^0'=tmp710^0, z115^0'=z115^0, z216^0'=z216^0, z317^0'=z317^0, z418^0'=z418^0, z519^0'=z519^0, T, cost: 1 Removed Trivial Updates Original rule: l1 -> l3 : constant22^0'=constant22^0, i20^0'=i20^0, lx2^0'=lx2^0, tmp03^0'=tmp03^0, tmp1011^0'=tmp1011^0, tmp1112^0'=tmp1112^0, tmp1213^0'=tmp1213^0, tmp1314^0'=tmp1314^0, tmp14^0'=tmp14^0, tmp25^0'=tmp25^0, tmp36^0'=tmp36^0, tmp47^0'=tmp47^0, tmp58^0'=tmp58^0, tmp69^0'=tmp69^0, tmp710^0'=tmp710^0, z115^0'=z115^0, z216^0'=z216^0, z317^0'=z317^0, z418^0'=z418^0, z519^0'=z519^0, T, cost: 1 New rule: l1 -> l3 : T, cost: 1 Propagated Equalities Original rule: l6 -> l2 : constant22^0'=constant22^post7, i20^0'=i20^post7, lx2^0'=lx2^post7, tmp03^0'=tmp03^post7, tmp1011^0'=tmp1011^post7, tmp1112^0'=tmp1112^post7, tmp1213^0'=tmp1213^post7, tmp1314^0'=tmp1314^post7, tmp14^0'=tmp14^post7, tmp25^0'=tmp25^post7, tmp36^0'=tmp36^post7, tmp47^0'=tmp47^post7, tmp58^0'=tmp58^post7, tmp69^0'=tmp69^post7, tmp710^0'=tmp710^post7, z115^0'=z115^post7, z216^0'=z216^post7, z317^0'=z317^post7, z418^0'=z418^post7, z519^0'=z519^post7, (-tmp36^post8+tmp36^0 == 0 /\ -tmp47^post8+tmp47^0 == 0 /\ tmp710^post8-tmp710^post7 == 0 /\ -lx2^post8+lx2^0 == 0 /\ -z317^post8+z317^0 == 0 /\ -tmp14^post8+tmp14^0 == 0 /\ -z115^post7+z115^post8 == 0 /\ tmp1314^post8-tmp1314^post7 == 0 /\ -tmp1314^post8+tmp1314^0 == 0 /\ -tmp58^post7+tmp58^post8 == 0 /\ -tmp03^post7+tmp03^post8 == 0 /\ constant22^0-constant22^post8 == 0 /\ -z115^post8+z115^0 == 0 /\ -tmp1011^post8+tmp1011^0 == 0 /\ -tmp1112^post8+tmp1112^0 == 0 /\ -tmp25^post7+tmp25^post8 == 0 /\ -i20^post8+i20^0 == 0 /\ tmp25^0-tmp25^post8 == 0 /\ -tmp710^post8+tmp710^0 == 0 /\ -tmp36^post7+tmp36^post8 == 0 /\ tmp1112^post8-tmp1112^post7 == 0 /\ -z418^post8+z418^0 == 0 /\ i20^post7 == 0 /\ tmp1213^0-tmp1213^post8 == 0 /\ tmp47^post8-tmp47^post7 == 0 /\ z317^post8-z317^post7 == 0 /\ -tmp14^post7+tmp14^post8 == 0 /\ tmp69^0-tmp69^post8 == 0 /\ -z519^post7+z519^post8 == 0 /\ -z216^post7+z216^post8 == 0 /\ -8+lx2^post7 == 0 /\ tmp58^0-tmp58^post8 == 0 /\ -constant22^post7+constant22^post8 == 0 /\ -z418^post7+z418^post8 == 0 /\ z216^0-z216^post8 == 0 /\ -tmp69^post7+tmp69^post8 == 0 /\ tmp1011^post8-tmp1011^post7 == 0 /\ -tmp1213^post7+tmp1213^post8 == 0 /\ tmp03^0-tmp03^post8 == 0 /\ z519^0-z519^post8 == 0), cost: 1 New rule: l6 -> l2 : constant22^0'=constant22^post8, i20^0'=0, lx2^0'=8, tmp03^0'=tmp03^post8, tmp1011^0'=tmp1011^post8, tmp1112^0'=tmp1112^post8, tmp1213^0'=tmp1213^post8, tmp1314^0'=tmp1314^post8, tmp14^0'=tmp14^post8, tmp25^0'=tmp25^post8, tmp36^0'=tmp36^post8, tmp47^0'=tmp47^post8, tmp58^0'=tmp58^post8, tmp69^0'=tmp69^post8, tmp710^0'=tmp710^post8, z115^0'=z115^post8, z216^0'=z216^post8, z317^0'=z317^post8, z418^0'=z418^post8, z519^0'=z519^post8, (0 == 0 /\ -tmp36^post8+tmp36^0 == 0 /\ -tmp47^post8+tmp47^0 == 0 /\ -lx2^post8+lx2^0 == 0 /\ -z317^post8+z317^0 == 0 /\ -tmp14^post8+tmp14^0 == 0 /\ -tmp1314^post8+tmp1314^0 == 0 /\ constant22^0-constant22^post8 == 0 /\ -z115^post8+z115^0 == 0 /\ -tmp1011^post8+tmp1011^0 == 0 /\ -tmp1112^post8+tmp1112^0 == 0 /\ -i20^post8+i20^0 == 0 /\ tmp25^0-tmp25^post8 == 0 /\ -tmp710^post8+tmp710^0 == 0 /\ -z418^post8+z418^0 == 0 /\ tmp1213^0-tmp1213^post8 == 0 /\ tmp69^0-tmp69^post8 == 0 /\ tmp58^0-tmp58^post8 == 0 /\ z216^0-z216^post8 == 0 /\ tmp03^0-tmp03^post8 == 0 /\ z519^0-z519^post8 == 0), cost: 1 propagated equality tmp710^post7 = tmp710^post8 propagated equality z115^post7 = z115^post8 propagated equality tmp1314^post7 = tmp1314^post8 propagated equality tmp58^post7 = tmp58^post8 propagated equality tmp03^post7 = tmp03^post8 propagated equality tmp25^post7 = tmp25^post8 propagated equality tmp36^post7 = tmp36^post8 propagated equality tmp1112^post7 = tmp1112^post8 propagated equality i20^post7 = 0 propagated equality tmp47^post7 = tmp47^post8 propagated equality z317^post7 = z317^post8 propagated equality tmp14^post7 = tmp14^post8 propagated equality z519^post7 = z519^post8 propagated equality z216^post7 = z216^post8 propagated equality lx2^post7 = 8 propagated equality constant22^post7 = constant22^post8 propagated equality z418^post7 = z418^post8 propagated equality tmp69^post7 = tmp69^post8 propagated equality tmp1011^post7 = tmp1011^post8 propagated equality tmp1213^post7 = tmp1213^post8 Propagated Equalities Original rule: l6 -> l2 : constant22^0'=constant22^post8, i20^0'=0, lx2^0'=8, tmp03^0'=tmp03^post8, tmp1011^0'=tmp1011^post8, tmp1112^0'=tmp1112^post8, tmp1213^0'=tmp1213^post8, tmp1314^0'=tmp1314^post8, tmp14^0'=tmp14^post8, tmp25^0'=tmp25^post8, tmp36^0'=tmp36^post8, tmp47^0'=tmp47^post8, tmp58^0'=tmp58^post8, tmp69^0'=tmp69^post8, tmp710^0'=tmp710^post8, z115^0'=z115^post8, z216^0'=z216^post8, z317^0'=z317^post8, z418^0'=z418^post8, z519^0'=z519^post8, (0 == 0 /\ -tmp36^post8+tmp36^0 == 0 /\ -tmp47^post8+tmp47^0 == 0 /\ -lx2^post8+lx2^0 == 0 /\ -z317^post8+z317^0 == 0 /\ -tmp14^post8+tmp14^0 == 0 /\ -tmp1314^post8+tmp1314^0 == 0 /\ constant22^0-constant22^post8 == 0 /\ -z115^post8+z115^0 == 0 /\ -tmp1011^post8+tmp1011^0 == 0 /\ -tmp1112^post8+tmp1112^0 == 0 /\ -i20^post8+i20^0 == 0 /\ tmp25^0-tmp25^post8 == 0 /\ -tmp710^post8+tmp710^0 == 0 /\ -z418^post8+z418^0 == 0 /\ tmp1213^0-tmp1213^post8 == 0 /\ tmp69^0-tmp69^post8 == 0 /\ tmp58^0-tmp58^post8 == 0 /\ z216^0-z216^post8 == 0 /\ tmp03^0-tmp03^post8 == 0 /\ z519^0-z519^post8 == 0), cost: 1 New rule: l6 -> l2 : constant22^0'=constant22^0, i20^0'=0, lx2^0'=8, tmp03^0'=tmp03^0, tmp1011^0'=tmp1011^0, tmp1112^0'=tmp1112^0, tmp1213^0'=tmp1213^0, tmp1314^0'=tmp1314^0, tmp14^0'=tmp14^0, tmp25^0'=tmp25^0, tmp36^0'=tmp36^0, tmp47^0'=tmp47^0, tmp58^0'=tmp58^0, tmp69^0'=tmp69^0, tmp710^0'=tmp710^0, z115^0'=z115^0, z216^0'=z216^0, z317^0'=z317^0, z418^0'=z418^0, z519^0'=z519^0, 0 == 0, cost: 1 propagated equality tmp36^post8 = tmp36^0 propagated equality tmp47^post8 = tmp47^0 propagated equality lx2^post8 = lx2^0 propagated equality z317^post8 = z317^0 propagated equality tmp14^post8 = tmp14^0 propagated equality tmp1314^post8 = tmp1314^0 propagated equality constant22^post8 = constant22^0 propagated equality z115^post8 = z115^0 propagated equality tmp1011^post8 = tmp1011^0 propagated equality tmp1112^post8 = tmp1112^0 propagated equality i20^post8 = i20^0 propagated equality tmp25^post8 = tmp25^0 propagated equality tmp710^post8 = tmp710^0 propagated equality z418^post8 = z418^0 propagated equality tmp1213^post8 = tmp1213^0 propagated equality tmp69^post8 = tmp69^0 propagated equality tmp58^post8 = tmp58^0 propagated equality z216^post8 = z216^0 propagated equality tmp03^post8 = tmp03^0 propagated equality z519^post8 = z519^0 Simplified Guard Original rule: l6 -> l2 : constant22^0'=constant22^0, i20^0'=0, lx2^0'=8, tmp03^0'=tmp03^0, tmp1011^0'=tmp1011^0, tmp1112^0'=tmp1112^0, tmp1213^0'=tmp1213^0, tmp1314^0'=tmp1314^0, tmp14^0'=tmp14^0, tmp25^0'=tmp25^0, tmp36^0'=tmp36^0, tmp47^0'=tmp47^0, tmp58^0'=tmp58^0, tmp69^0'=tmp69^0, tmp710^0'=tmp710^0, z115^0'=z115^0, z216^0'=z216^0, z317^0'=z317^0, z418^0'=z418^0, z519^0'=z519^0, 0 == 0, cost: 1 New rule: l6 -> l2 : constant22^0'=constant22^0, i20^0'=0, lx2^0'=8, tmp03^0'=tmp03^0, tmp1011^0'=tmp1011^0, tmp1112^0'=tmp1112^0, tmp1213^0'=tmp1213^0, tmp1314^0'=tmp1314^0, tmp14^0'=tmp14^0, tmp25^0'=tmp25^0, tmp36^0'=tmp36^0, tmp47^0'=tmp47^0, tmp58^0'=tmp58^0, tmp69^0'=tmp69^0, tmp710^0'=tmp710^0, z115^0'=z115^0, z216^0'=z216^0, z317^0'=z317^0, z418^0'=z418^0, z519^0'=z519^0, T, cost: 1 Removed Trivial Updates Original rule: l6 -> l2 : constant22^0'=constant22^0, i20^0'=0, lx2^0'=8, tmp03^0'=tmp03^0, tmp1011^0'=tmp1011^0, tmp1112^0'=tmp1112^0, tmp1213^0'=tmp1213^0, tmp1314^0'=tmp1314^0, tmp14^0'=tmp14^0, tmp25^0'=tmp25^0, tmp36^0'=tmp36^0, tmp47^0'=tmp47^0, tmp58^0'=tmp58^0, tmp69^0'=tmp69^0, tmp710^0'=tmp710^0, z115^0'=z115^0, z216^0'=z216^0, z317^0'=z317^0, z418^0'=z418^0, z519^0'=z519^0, T, cost: 1 New rule: l6 -> l2 : i20^0'=0, lx2^0'=8, T, cost: 1 Step with 15 Trace 15[T] Blocked [{}, {}] Step with 13 Trace 15[T], 13[T] Blocked [{}, {}, {}] Step with 10 Trace 15[T], 13[T], 10[(-7+i20^0 <= 0)] Blocked [{}, {}, {9[T]}, {}] Accelerate Start location: l6 Program variables: constant22^0 i20^0 lx2^0 tmp03^0 tmp1011^0 tmp1112^0 tmp1213^0 tmp1314^0 tmp14^0 tmp25^0 tmp36^0 tmp47^0 tmp58^0 tmp69^0 tmp710^0 z115^0 z216^0 z317^0 z418^0 z519^0 9: l0 -> l1 : i20^0'=0, 8-i20^0 <= 0, cost: 1 10: l0 -> l2 : constant22^0'=-3196, i20^0'=1+i20^0, tmp03^0'=tmp1314^post2+tmp36^post2, tmp1011^0'=tmp1314^post2+2*tmp36^post2, tmp1112^0'=tmp14^post2+tmp25^post2, tmp1213^0'=tmp14^post2-tmp25^post2, tmp1314^0'=tmp1314^post2, tmp14^0'=tmp14^post2, tmp25^0'=tmp25^post2, tmp36^0'=tmp36^post2, tmp47^0'=tmp47^post2, tmp58^0'=tmp58^post2, tmp69^0'=tmp69^post2, tmp710^0'=tmp710^post2, z115^0'=z115^post2, z216^0'=z216^post2, z317^0'=z317^2+z519^post2, z418^0'=z418^2+z519^post2, z519^0'=z519^post2, -7+i20^0 <= 0, cost: 1 14: l1 -> l3 : T, cost: 1 13: l2 -> l0 : T, cost: 1 16: l2 -> l2 : constant22^0'=-3196, i20^0'=i20^0+n, tmp03^0'=tmp1314^post2+tmp36^post2, tmp1011^0'=tmp1314^post2+2*tmp36^post2, tmp1112^0'=tmp14^post2+tmp25^post2, tmp1213^0'=tmp14^post2-tmp25^post2, tmp1314^0'=tmp1314^post2, tmp14^0'=tmp14^post2, tmp25^0'=tmp25^post2, tmp36^0'=tmp36^post2, tmp47^0'=tmp47^post2, tmp58^0'=tmp58^post2, tmp69^0'=tmp69^post2, tmp710^0'=tmp710^post2, z115^0'=z115^post2, z216^0'=z216^post2, z317^0'=z317^2+z519^post2, z418^0'=z418^2+z519^post2, z519^0'=z519^post2, (8-i20^0-n >= 0 /\ -1+n >= 0), cost: 1 11: l3 -> l4 : 8-i20^0 <= 0, cost: 1 12: l3 -> l1 : constant22^0'=-3196, i20^0'=1+i20^0, tmp03^0'=tmp36^post4+tmp1314^post4, tmp1011^0'=2*tmp36^post4+tmp1314^post4, tmp1112^0'=tmp14^post4+tmp25^post4, tmp1213^0'=tmp14^post4-tmp25^post4, tmp1314^0'=tmp1314^post4, tmp14^0'=tmp14^post4, tmp25^0'=tmp25^post4, tmp36^0'=tmp36^post4, tmp47^0'=tmp47^post4, tmp58^0'=tmp58^post4, tmp69^0'=tmp69^post4, tmp710^0'=tmp710^post4, z115^0'=z115^post4, z216^0'=z216^post4, z317^0'=z317^2+z519^post4, z418^0'=z519^post4+z418^2, z519^0'=z519^post4, -7+i20^0 <= 0, cost: 1 15: l6 -> l2 : i20^0'=0, lx2^0'=8, T, cost: 1 Loop Acceleration Original rule: l2 -> l2 : constant22^0'=-3196, i20^0'=1+i20^0, tmp03^0'=tmp1314^post2+tmp36^post2, tmp1011^0'=tmp1314^post2+2*tmp36^post2, tmp1112^0'=tmp14^post2+tmp25^post2, tmp1213^0'=tmp14^post2-tmp25^post2, tmp1314^0'=tmp1314^post2, tmp14^0'=tmp14^post2, tmp25^0'=tmp25^post2, tmp36^0'=tmp36^post2, tmp47^0'=tmp47^post2, tmp58^0'=tmp58^post2, tmp69^0'=tmp69^post2, tmp710^0'=tmp710^post2, z115^0'=z115^post2, z216^0'=z216^post2, z317^0'=z317^2+z519^post2, z418^0'=z418^2+z519^post2, z519^0'=z519^post2, -7+i20^0 <= 0, cost: 1 New rule: l2 -> l2 : constant22^0'=-3196, i20^0'=i20^0+n, tmp03^0'=tmp1314^post2+tmp36^post2, tmp1011^0'=tmp1314^post2+2*tmp36^post2, tmp1112^0'=tmp14^post2+tmp25^post2, tmp1213^0'=tmp14^post2-tmp25^post2, tmp1314^0'=tmp1314^post2, tmp14^0'=tmp14^post2, tmp25^0'=tmp25^post2, tmp36^0'=tmp36^post2, tmp47^0'=tmp47^post2, tmp58^0'=tmp58^post2, tmp69^0'=tmp69^post2, tmp710^0'=tmp710^post2, z115^0'=z115^post2, z216^0'=z216^post2, z317^0'=z317^2+z519^post2, z418^0'=z418^2+z519^post2, z519^0'=z519^post2, (8-i20^0-n >= 0 /\ -1+n >= 0), cost: 1 7-i20^0 >= 0 [0]: montonic decrease yields 8-i20^0-n >= 0 7-i20^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ 7-i20^0 >= 0) Replacement map: {7-i20^0 >= 0 -> 8-i20^0-n >= 0} Trace 15[T], 16[(8-i20^0-n >= 0 /\ -1+n >= 0)] Blocked [{}, {}, {16[T]}] Step with 13 Trace 15[T], 16[(8-i20^0-n >= 0 /\ -1+n >= 0)], 13[T] Blocked [{}, {}, {16[T]}, {}] Step with 10 Trace 15[T], 16[(8-i20^0-n >= 0 /\ -1+n >= 0)], 13[T], 10[(-7+i20^0 <= 0)] Blocked [{}, {}, {16[T]}, {}, {}] Covered Trace 15[T], 16[(8-i20^0-n >= 0 /\ -1+n >= 0)], 13[T] Blocked [{}, {}, {16[T]}, {10[T]}] Step with 9 Trace 15[T], 16[(8-i20^0-n >= 0 /\ -1+n >= 0)], 13[T], 9[(8-i20^0 <= 0)] Blocked [{}, {}, {16[T]}, {10[T]}, {}] Step with 14 Trace 15[T], 16[(8-i20^0-n >= 0 /\ -1+n >= 0)], 13[T], 9[(8-i20^0 <= 0)], 14[T] Blocked [{}, {}, {16[T]}, {10[T]}, {}, {}] Step with 12 Trace 15[T], 16[(8-i20^0-n >= 0 /\ -1+n >= 0)], 13[T], 9[(8-i20^0 <= 0)], 14[T], 12[(-7+i20^0 <= 0)] Blocked [{}, {}, {16[T]}, {10[T]}, {}, {11[T]}, {}] Accelerate Start location: l6 Program variables: constant22^0 i20^0 lx2^0 tmp03^0 tmp1011^0 tmp1112^0 tmp1213^0 tmp1314^0 tmp14^0 tmp25^0 tmp36^0 tmp47^0 tmp58^0 tmp69^0 tmp710^0 z115^0 z216^0 z317^0 z418^0 z519^0 9: l0 -> l1 : i20^0'=0, 8-i20^0 <= 0, cost: 1 10: l0 -> l2 : constant22^0'=-3196, i20^0'=1+i20^0, tmp03^0'=tmp1314^post2+tmp36^post2, tmp1011^0'=tmp1314^post2+2*tmp36^post2, tmp1112^0'=tmp14^post2+tmp25^post2, tmp1213^0'=tmp14^post2-tmp25^post2, tmp1314^0'=tmp1314^post2, tmp14^0'=tmp14^post2, tmp25^0'=tmp25^post2, tmp36^0'=tmp36^post2, tmp47^0'=tmp47^post2, tmp58^0'=tmp58^post2, tmp69^0'=tmp69^post2, tmp710^0'=tmp710^post2, z115^0'=z115^post2, z216^0'=z216^post2, z317^0'=z317^2+z519^post2, z418^0'=z418^2+z519^post2, z519^0'=z519^post2, -7+i20^0 <= 0, cost: 1 14: l1 -> l3 : T, cost: 1 17: l1 -> l1 : constant22^0'=-3196, i20^0'=n2+i20^0, tmp03^0'=tmp36^post4+tmp1314^post4, tmp1011^0'=2*tmp36^post4+tmp1314^post4, tmp1112^0'=tmp14^post4+tmp25^post4, tmp1213^0'=tmp14^post4-tmp25^post4, tmp1314^0'=tmp1314^post4, tmp14^0'=tmp14^post4, tmp25^0'=tmp25^post4, tmp36^0'=tmp36^post4, tmp47^0'=tmp47^post4, tmp58^0'=tmp58^post4, tmp69^0'=tmp69^post4, tmp710^0'=tmp710^post4, z115^0'=z115^post4, z216^0'=z216^post4, z317^0'=z317^2+z519^post4, z418^0'=z519^post4+z418^2, z519^0'=z519^post4, (8-n2-i20^0 >= 0 /\ -1+n2 >= 0), cost: 1 13: l2 -> l0 : T, cost: 1 16: l2 -> l2 : constant22^0'=-3196, i20^0'=i20^0+n, tmp03^0'=tmp1314^post2+tmp36^post2, tmp1011^0'=tmp1314^post2+2*tmp36^post2, tmp1112^0'=tmp14^post2+tmp25^post2, tmp1213^0'=tmp14^post2-tmp25^post2, tmp1314^0'=tmp1314^post2, tmp14^0'=tmp14^post2, tmp25^0'=tmp25^post2, tmp36^0'=tmp36^post2, tmp47^0'=tmp47^post2, tmp58^0'=tmp58^post2, tmp69^0'=tmp69^post2, tmp710^0'=tmp710^post2, z115^0'=z115^post2, z216^0'=z216^post2, z317^0'=z317^2+z519^post2, z418^0'=z418^2+z519^post2, z519^0'=z519^post2, (8-i20^0-n >= 0 /\ -1+n >= 0), cost: 1 11: l3 -> l4 : 8-i20^0 <= 0, cost: 1 12: l3 -> l1 : constant22^0'=-3196, i20^0'=1+i20^0, tmp03^0'=tmp36^post4+tmp1314^post4, tmp1011^0'=2*tmp36^post4+tmp1314^post4, tmp1112^0'=tmp14^post4+tmp25^post4, tmp1213^0'=tmp14^post4-tmp25^post4, tmp1314^0'=tmp1314^post4, tmp14^0'=tmp14^post4, tmp25^0'=tmp25^post4, tmp36^0'=tmp36^post4, tmp47^0'=tmp47^post4, tmp58^0'=tmp58^post4, tmp69^0'=tmp69^post4, tmp710^0'=tmp710^post4, z115^0'=z115^post4, z216^0'=z216^post4, z317^0'=z317^2+z519^post4, z418^0'=z519^post4+z418^2, z519^0'=z519^post4, -7+i20^0 <= 0, cost: 1 15: l6 -> l2 : i20^0'=0, lx2^0'=8, T, cost: 1 Loop Acceleration Original rule: l1 -> l1 : constant22^0'=-3196, i20^0'=1+i20^0, tmp03^0'=tmp36^post4+tmp1314^post4, tmp1011^0'=2*tmp36^post4+tmp1314^post4, tmp1112^0'=tmp14^post4+tmp25^post4, tmp1213^0'=tmp14^post4-tmp25^post4, tmp1314^0'=tmp1314^post4, tmp14^0'=tmp14^post4, tmp25^0'=tmp25^post4, tmp36^0'=tmp36^post4, tmp47^0'=tmp47^post4, tmp58^0'=tmp58^post4, tmp69^0'=tmp69^post4, tmp710^0'=tmp710^post4, z115^0'=z115^post4, z216^0'=z216^post4, z317^0'=z317^2+z519^post4, z418^0'=z519^post4+z418^2, z519^0'=z519^post4, -7+i20^0 <= 0, cost: 1 New rule: l1 -> l1 : constant22^0'=-3196, i20^0'=n2+i20^0, tmp03^0'=tmp36^post4+tmp1314^post4, tmp1011^0'=2*tmp36^post4+tmp1314^post4, tmp1112^0'=tmp14^post4+tmp25^post4, tmp1213^0'=tmp14^post4-tmp25^post4, tmp1314^0'=tmp1314^post4, tmp14^0'=tmp14^post4, tmp25^0'=tmp25^post4, tmp36^0'=tmp36^post4, tmp47^0'=tmp47^post4, tmp58^0'=tmp58^post4, tmp69^0'=tmp69^post4, tmp710^0'=tmp710^post4, z115^0'=z115^post4, z216^0'=z216^post4, z317^0'=z317^2+z519^post4, z418^0'=z519^post4+z418^2, z519^0'=z519^post4, (8-n2-i20^0 >= 0 /\ -1+n2 >= 0), cost: 1 7-i20^0 >= 0 [0]: montonic decrease yields 8-n2-i20^0 >= 0 7-i20^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ 7-i20^0 >= 0) Replacement map: {7-i20^0 >= 0 -> 8-n2-i20^0 >= 0} Trace 15[T], 16[(8-i20^0-n >= 0 /\ -1+n >= 0)], 13[T], 9[(8-i20^0 <= 0)], 17[(8-n2-i20^0 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {}, {16[T]}, {10[T]}, {}, {17[T]}] Step with 14 Trace 15[T], 16[(8-i20^0-n >= 0 /\ -1+n >= 0)], 13[T], 9[(8-i20^0 <= 0)], 17[(8-n2-i20^0 >= 0 /\ -1+n2 >= 0)], 14[T] Blocked [{}, {}, {16[T]}, {10[T]}, {}, {17[T]}, {}] Step with 12 Trace 15[T], 16[(8-i20^0-n >= 0 /\ -1+n >= 0)], 13[T], 9[(8-i20^0 <= 0)], 17[(8-n2-i20^0 >= 0 /\ -1+n2 >= 0)], 14[T], 12[(-7+i20^0 <= 0)] Blocked [{}, {}, {16[T]}, {10[T]}, {}, {17[T]}, {}, {}] Covered Trace 15[T], 16[(8-i20^0-n >= 0 /\ -1+n >= 0)], 13[T], 9[(8-i20^0 <= 0)], 17[(8-n2-i20^0 >= 0 /\ -1+n2 >= 0)], 14[T] Blocked [{}, {}, {16[T]}, {10[T]}, {}, {17[T]}, {12[T]}] Step with 11 Trace 15[T], 16[(8-i20^0-n >= 0 /\ -1+n >= 0)], 13[T], 9[(8-i20^0 <= 0)], 17[(8-n2-i20^0 >= 0 /\ -1+n2 >= 0)], 14[T], 11[(8-i20^0 <= 0)] Blocked [{}, {}, {16[T]}, {10[T]}, {}, {17[T]}, {12[T]}, {}] Backtrack Trace 15[T], 16[(8-i20^0-n >= 0 /\ -1+n >= 0)], 13[T], 9[(8-i20^0 <= 0)], 17[(8-n2-i20^0 >= 0 /\ -1+n2 >= 0)], 14[T] Blocked [{}, {}, {16[T]}, {10[T]}, {}, {17[T]}, {11[T], 12[T]}] Backtrack Trace 15[T], 16[(8-i20^0-n >= 0 /\ -1+n >= 0)], 13[T], 9[(8-i20^0 <= 0)], 17[(8-n2-i20^0 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {}, {16[T]}, {10[T]}, {}, {14[T], 17[T]}] Backtrack Trace 15[T], 16[(8-i20^0-n >= 0 /\ -1+n >= 0)], 13[T], 9[(8-i20^0 <= 0)] Blocked [{}, {}, {16[T]}, {10[T]}, {17[T]}] Step with 14 Trace 15[T], 16[(8-i20^0-n >= 0 /\ -1+n >= 0)], 13[T], 9[(8-i20^0 <= 0)], 14[T] Blocked [{}, {}, {16[T]}, {10[T]}, {17[T]}, {}] Step with 12 Trace 15[T], 16[(8-i20^0-n >= 0 /\ -1+n >= 0)], 13[T], 9[(8-i20^0 <= 0)], 14[T], 12[(-7+i20^0 <= 0)] Blocked [{}, {}, {16[T]}, {10[T]}, {17[T]}, {11[T]}, {}] Covered Trace 15[T], 16[(8-i20^0-n >= 0 /\ -1+n >= 0)], 13[T], 9[(8-i20^0 <= 0)], 14[T] Blocked [{}, {}, {16[T]}, {10[T]}, {17[T]}, {11[T], 12[T]}] Backtrack Trace 15[T], 16[(8-i20^0-n >= 0 /\ -1+n >= 0)], 13[T], 9[(8-i20^0 <= 0)] Blocked [{}, {}, {16[T]}, {10[T]}, {14[T], 17[T]}] Backtrack Trace 15[T], 16[(8-i20^0-n >= 0 /\ -1+n >= 0)], 13[T] Blocked [{}, {}, {16[T]}, {9[T], 10[T]}] Backtrack Trace 15[T], 16[(8-i20^0-n >= 0 /\ -1+n >= 0)] Blocked [{}, {}, {13[T], 16[T]}] Backtrack Trace 15[T] Blocked [{}, {16[T]}] Step with 13 Trace 15[T], 13[T] Blocked [{}, {16[T]}, {}] Step with 10 Trace 15[T], 13[T], 10[(-7+i20^0 <= 0)] Blocked [{}, {16[T]}, {9[T]}, {}] Covered Trace 15[T], 13[T] Blocked [{}, {16[T]}, {9[T], 10[T]}] Backtrack Trace 15[T] Blocked [{}, {13[T], 16[T]}] Backtrack Trace Blocked [{15[T]}] Accept unknown Build SHA: a05f16bf13df659c382799650051f91bf6828c7b