unknown Initial ITS Start location: l10 Program variables: i^0 j^0 k^0 tmp^0 tmp___0^0 0: l0 -> l1 : i^0'=i^post1, j^0'=j^post1, k^0'=k^post1, tmp^0'=tmp^post1, tmp___0^0'=tmp___0^post1, (0 == 0 /\ i^post1 == 0 /\ -tmp^post1+tmp^0 == 0 /\ k^0-k^post1 == 0 /\ -100+k^0 <= 0 /\ -j^post1+j^0 == 0), cost: 1 1: l0 -> l2 : i^0'=i^post2, j^0'=j^post2, k^0'=k^post2, tmp^0'=tmp^post2, tmp___0^0'=tmp___0^post2, (-k^post2+k^0 == 0 /\ 101-k^0 <= 0 /\ -j^post2+j^0 == 0 /\ tmp^0-tmp^post2 == 0 /\ tmp___0^0-tmp___0^post2 == 0 /\ i^0-i^post2 == 0), cost: 1 4: l1 -> l4 : i^0'=i^post5, j^0'=j^post5, k^0'=k^post5, tmp^0'=tmp^post5, tmp___0^0'=tmp___0^post5, (-j^post5+j^0 == 0 /\ tmp___0^0-tmp___0^post5 == 0 /\ k^0-k^post5 == 0 /\ i^0-i^post5 == 0 /\ -tmp^post5+tmp^0 == 0), cost: 1 2: l3 -> l0 : i^0'=i^post3, j^0'=j^post3, k^0'=k^post3, tmp^0'=tmp^post3, tmp___0^0'=tmp___0^post3, (k^0-k^post3 == 0 /\ -j^post3+j^0 == 0 /\ 1-k^0 <= 0 /\ i^0-i^post3 == 0 /\ tmp___0^0-tmp___0^post3 == 0 /\ -tmp^post3+tmp^0 == 0), cost: 1 3: l3 -> l2 : i^0'=i^post4, j^0'=j^post4, k^0'=k^post4, tmp^0'=tmp^post4, tmp___0^0'=tmp___0^post4, (tmp^0-tmp^post4 == 0 /\ tmp___0^0-tmp___0^post4 == 0 /\ i^0-i^post4 == 0 /\ -j^post4+j^0 == 0 /\ k^0 <= 0 /\ -k^post4+k^0 == 0), cost: 1 11: l4 -> l7 : i^0'=i^post12, j^0'=j^post12, k^0'=k^post12, tmp^0'=tmp^post12, tmp___0^0'=tmp___0^post12, (i^0-k^0 <= 0 /\ j^0-j^post12 == 0 /\ tmp___0^0-tmp___0^post12 == 0 /\ -i^0+k^0 <= 0 /\ -tmp^post12+tmp^0 == 0 /\ i^0-i^post12 == 0 /\ -k^post12+k^0 == 0), cost: 1 12: l4 -> l8 : i^0'=i^post13, j^0'=j^post13, k^0'=k^post13, tmp^0'=tmp^post13, tmp___0^0'=tmp___0^post13, (-i^post13+i^0 == 0 /\ -j^post13+j^0 == 0 /\ tmp^0-tmp^post13 == 0 /\ k^0-k^post13 == 0 /\ -tmp___0^post13+tmp___0^0 == 0 /\ 1-i^0+k^0 <= 0), cost: 1 13: l4 -> l8 : i^0'=i^post14, j^0'=j^post14, k^0'=k^post14, tmp^0'=tmp^post14, tmp___0^0'=tmp___0^post14, (-j^post14+j^0 == 0 /\ -k^post14+k^0 == 0 /\ tmp^0-tmp^post14 == 0 /\ tmp___0^0-tmp___0^post14 == 0 /\ 1+i^0-k^0 <= 0 /\ i^0-i^post14 == 0), cost: 1 5: l5 -> l2 : i^0'=i^post6, j^0'=j^post6, k^0'=k^post6, tmp^0'=tmp^post6, tmp___0^0'=tmp___0^post6, (tmp^0-tmp^post6 == 0 /\ i^0-i^post6 == 0 /\ -j^post6+j^0 == 0 /\ i^0-j^0 <= 0 /\ -k^post6+k^0 == 0 /\ -tmp___0^post6+tmp___0^0 == 0), cost: 1 6: l5 -> l6 : i^0'=i^post7, j^0'=j^post7, k^0'=k^post7, tmp^0'=tmp^post7, tmp___0^0'=tmp___0^post7, (k^0-k^post7 == 0 /\ -tmp^post7+tmp^0 == 0 /\ i^0-i^post7 == 0 /\ 1-i^0+j^0 <= 0 /\ tmp___0^0-tmp___0^post7 == 0 /\ -1-j^0+j^post7 == 0), cost: 1 8: l6 -> l5 : i^0'=i^post9, j^0'=j^post9, k^0'=k^post9, tmp^0'=tmp^post9, tmp___0^0'=tmp___0^post9, (tmp___0^0-tmp___0^post9 == 0 /\ j^0-j^post9 == 0 /\ -tmp^post9+tmp^0 == 0 /\ -k^post9+k^0 == 0 /\ i^0-i^post9 == 0), cost: 1 7: l7 -> l6 : i^0'=i^post8, j^0'=j^post8, k^0'=k^post8, tmp^0'=tmp^post8, tmp___0^0'=tmp___0^post8, (-k^post8+k^0 == 0 /\ -tmp___0^post8+tmp___0^0 == 0 /\ j^post8 == 0 /\ 1-i^0+i^post8 == 0 /\ tmp^0-tmp^post8 == 0), cost: 1 9: l8 -> l1 : i^0'=i^post10, j^0'=j^post10, k^0'=k^post10, tmp^0'=tmp^post10, tmp___0^0'=tmp___0^post10, (-tmp^post10+tmp^0 == 0 /\ -j^post10+j^0 == 0 /\ -tmp___0^post10+tmp___0^0 == 0 /\ k^0-k^post10 == 0 /\ -1+i^post10-i^0 == 0), cost: 1 10: l8 -> l7 : i^0'=i^post11, j^0'=j^post11, k^0'=k^post11, tmp^0'=tmp^post11, tmp___0^0'=tmp___0^post11, (-j^post11+j^0 == 0 /\ -tmp___0^post11+tmp___0^0 == 0 /\ i^0-i^post11 == 0 /\ -k^post11+k^0 == 0 /\ tmp^0-tmp^post11 == 0), cost: 1 14: l9 -> l3 : i^0'=i^post15, j^0'=j^post15, k^0'=k^post15, tmp^0'=tmp^post15, tmp___0^0'=tmp___0^post15, (0 == 0 /\ -j^post15+j^0 == 0 /\ tmp___0^0-tmp___0^post15 == 0 /\ -tmp^post15+k^post15 == 0 /\ i^0-i^post15 == 0), cost: 1 15: l10 -> l9 : i^0'=i^post16, j^0'=j^post16, k^0'=k^post16, tmp^0'=tmp^post16, tmp___0^0'=tmp___0^post16, (tmp^0-tmp^post16 == 0 /\ -j^post16+j^0 == 0 /\ i^0-i^post16 == 0 /\ -k^post16+k^0 == 0 /\ -tmp___0^post16+tmp___0^0 == 0), cost: 1 Chained Linear Paths Start location: l10 Program variables: i^0 j^0 k^0 tmp^0 tmp___0^0 0: l0 -> l1 : i^0'=i^post1, j^0'=j^post1, k^0'=k^post1, tmp^0'=tmp^post1, tmp___0^0'=tmp___0^post1, (0 == 0 /\ i^post1 == 0 /\ -tmp^post1+tmp^0 == 0 /\ k^0-k^post1 == 0 /\ -100+k^0 <= 0 /\ -j^post1+j^0 == 0), cost: 1 1: l0 -> l2 : i^0'=i^post2, j^0'=j^post2, k^0'=k^post2, tmp^0'=tmp^post2, tmp___0^0'=tmp___0^post2, (-k^post2+k^0 == 0 /\ 101-k^0 <= 0 /\ -j^post2+j^0 == 0 /\ tmp^0-tmp^post2 == 0 /\ tmp___0^0-tmp___0^post2 == 0 /\ i^0-i^post2 == 0), cost: 1 4: l1 -> l4 : i^0'=i^post5, j^0'=j^post5, k^0'=k^post5, tmp^0'=tmp^post5, tmp___0^0'=tmp___0^post5, (-j^post5+j^0 == 0 /\ tmp___0^0-tmp___0^post5 == 0 /\ k^0-k^post5 == 0 /\ i^0-i^post5 == 0 /\ -tmp^post5+tmp^0 == 0), cost: 1 2: l3 -> l0 : i^0'=i^post3, j^0'=j^post3, k^0'=k^post3, tmp^0'=tmp^post3, tmp___0^0'=tmp___0^post3, (k^0-k^post3 == 0 /\ -j^post3+j^0 == 0 /\ 1-k^0 <= 0 /\ i^0-i^post3 == 0 /\ tmp___0^0-tmp___0^post3 == 0 /\ -tmp^post3+tmp^0 == 0), cost: 1 3: l3 -> l2 : i^0'=i^post4, j^0'=j^post4, k^0'=k^post4, tmp^0'=tmp^post4, tmp___0^0'=tmp___0^post4, (tmp^0-tmp^post4 == 0 /\ tmp___0^0-tmp___0^post4 == 0 /\ i^0-i^post4 == 0 /\ -j^post4+j^0 == 0 /\ k^0 <= 0 /\ -k^post4+k^0 == 0), cost: 1 11: l4 -> l7 : i^0'=i^post12, j^0'=j^post12, k^0'=k^post12, tmp^0'=tmp^post12, tmp___0^0'=tmp___0^post12, (i^0-k^0 <= 0 /\ j^0-j^post12 == 0 /\ tmp___0^0-tmp___0^post12 == 0 /\ -i^0+k^0 <= 0 /\ -tmp^post12+tmp^0 == 0 /\ i^0-i^post12 == 0 /\ -k^post12+k^0 == 0), cost: 1 12: l4 -> l8 : i^0'=i^post13, j^0'=j^post13, k^0'=k^post13, tmp^0'=tmp^post13, tmp___0^0'=tmp___0^post13, (-i^post13+i^0 == 0 /\ -j^post13+j^0 == 0 /\ tmp^0-tmp^post13 == 0 /\ k^0-k^post13 == 0 /\ -tmp___0^post13+tmp___0^0 == 0 /\ 1-i^0+k^0 <= 0), cost: 1 13: l4 -> l8 : i^0'=i^post14, j^0'=j^post14, k^0'=k^post14, tmp^0'=tmp^post14, tmp___0^0'=tmp___0^post14, (-j^post14+j^0 == 0 /\ -k^post14+k^0 == 0 /\ tmp^0-tmp^post14 == 0 /\ tmp___0^0-tmp___0^post14 == 0 /\ 1+i^0-k^0 <= 0 /\ i^0-i^post14 == 0), cost: 1 5: l5 -> l2 : i^0'=i^post6, j^0'=j^post6, k^0'=k^post6, tmp^0'=tmp^post6, tmp___0^0'=tmp___0^post6, (tmp^0-tmp^post6 == 0 /\ i^0-i^post6 == 0 /\ -j^post6+j^0 == 0 /\ i^0-j^0 <= 0 /\ -k^post6+k^0 == 0 /\ -tmp___0^post6+tmp___0^0 == 0), cost: 1 6: l5 -> l6 : i^0'=i^post7, j^0'=j^post7, k^0'=k^post7, tmp^0'=tmp^post7, tmp___0^0'=tmp___0^post7, (k^0-k^post7 == 0 /\ -tmp^post7+tmp^0 == 0 /\ i^0-i^post7 == 0 /\ 1-i^0+j^0 <= 0 /\ tmp___0^0-tmp___0^post7 == 0 /\ -1-j^0+j^post7 == 0), cost: 1 8: l6 -> l5 : i^0'=i^post9, j^0'=j^post9, k^0'=k^post9, tmp^0'=tmp^post9, tmp___0^0'=tmp___0^post9, (tmp___0^0-tmp___0^post9 == 0 /\ j^0-j^post9 == 0 /\ -tmp^post9+tmp^0 == 0 /\ -k^post9+k^0 == 0 /\ i^0-i^post9 == 0), cost: 1 7: l7 -> l6 : i^0'=i^post8, j^0'=j^post8, k^0'=k^post8, tmp^0'=tmp^post8, tmp___0^0'=tmp___0^post8, (-k^post8+k^0 == 0 /\ -tmp___0^post8+tmp___0^0 == 0 /\ j^post8 == 0 /\ 1-i^0+i^post8 == 0 /\ tmp^0-tmp^post8 == 0), cost: 1 9: l8 -> l1 : i^0'=i^post10, j^0'=j^post10, k^0'=k^post10, tmp^0'=tmp^post10, tmp___0^0'=tmp___0^post10, (-tmp^post10+tmp^0 == 0 /\ -j^post10+j^0 == 0 /\ -tmp___0^post10+tmp___0^0 == 0 /\ k^0-k^post10 == 0 /\ -1+i^post10-i^0 == 0), cost: 1 10: l8 -> l7 : i^0'=i^post11, j^0'=j^post11, k^0'=k^post11, tmp^0'=tmp^post11, tmp___0^0'=tmp___0^post11, (-j^post11+j^0 == 0 /\ -tmp___0^post11+tmp___0^0 == 0 /\ i^0-i^post11 == 0 /\ -k^post11+k^0 == 0 /\ tmp^0-tmp^post11 == 0), cost: 1 16: l10 -> l3 : i^0'=i^post15, j^0'=j^post15, k^0'=k^post15, tmp^0'=tmp^post15, tmp___0^0'=tmp___0^post15, (0 == 0 /\ tmp^0-tmp^post16 == 0 /\ j^post16-j^post15 == 0 /\ -tmp^post15+k^post15 == 0 /\ -j^post16+j^0 == 0 /\ i^0-i^post16 == 0 /\ tmp___0^post16-tmp___0^post15 == 0 /\ -i^post15+i^post16 == 0 /\ -k^post16+k^0 == 0 /\ -tmp___0^post16+tmp___0^0 == 0), cost: 1 Eliminating location l9 by chaining: Applied chaining First rule: l10 -> l9 : i^0'=i^post16, j^0'=j^post16, k^0'=k^post16, tmp^0'=tmp^post16, tmp___0^0'=tmp___0^post16, (tmp^0-tmp^post16 == 0 /\ -j^post16+j^0 == 0 /\ i^0-i^post16 == 0 /\ -k^post16+k^0 == 0 /\ -tmp___0^post16+tmp___0^0 == 0), cost: 1 Second rule: l9 -> l3 : i^0'=i^post15, j^0'=j^post15, k^0'=k^post15, tmp^0'=tmp^post15, tmp___0^0'=tmp___0^post15, (0 == 0 /\ -j^post15+j^0 == 0 /\ tmp___0^0-tmp___0^post15 == 0 /\ -tmp^post15+k^post15 == 0 /\ i^0-i^post15 == 0), cost: 1 New rule: l10 -> l3 : i^0'=i^post15, j^0'=j^post15, k^0'=k^post15, tmp^0'=tmp^post15, tmp___0^0'=tmp___0^post15, (0 == 0 /\ tmp^0-tmp^post16 == 0 /\ j^post16-j^post15 == 0 /\ -tmp^post15+k^post15 == 0 /\ -j^post16+j^0 == 0 /\ i^0-i^post16 == 0 /\ tmp___0^post16-tmp___0^post15 == 0 /\ -i^post15+i^post16 == 0 /\ -k^post16+k^0 == 0 /\ -tmp___0^post16+tmp___0^0 == 0), cost: 1 Applied deletion Removed the following rules: 14 15 Simplified Transitions Start location: l10 Program variables: i^0 j^0 k^0 tmp^0 tmp___0^0 17: l0 -> l1 : i^0'=0, tmp___0^0'=tmp___0^post1, -100+k^0 <= 0, cost: 1 18: l0 -> l2 : 101-k^0 <= 0, cost: 1 21: l1 -> l4 : T, cost: 1 19: l3 -> l0 : 1-k^0 <= 0, cost: 1 20: l3 -> l2 : k^0 <= 0, cost: 1 28: l4 -> l7 : (i^0-k^0 <= 0 /\ i^0-k^0 == 0 /\ -i^0+k^0 <= 0), cost: 1 29: l4 -> l8 : 1-i^0+k^0 <= 0, cost: 1 30: l4 -> l8 : 1+i^0-k^0 <= 0, cost: 1 22: l5 -> l2 : i^0-j^0 <= 0, cost: 1 23: l5 -> l6 : j^0'=1+j^0, 1-i^0+j^0 <= 0, cost: 1 25: l6 -> l5 : T, cost: 1 24: l7 -> l6 : i^0'=-1+i^0, j^0'=0, T, cost: 1 26: l8 -> l1 : i^0'=1+i^0, T, cost: 1 27: l8 -> l7 : T, cost: 1 31: l10 -> l3 : k^0'=tmp^post15, tmp^0'=tmp^post15, T, cost: 1 Propagated Equalities Original rule: l0 -> l1 : i^0'=i^post1, j^0'=j^post1, k^0'=k^post1, tmp^0'=tmp^post1, tmp___0^0'=tmp___0^post1, (0 == 0 /\ i^post1 == 0 /\ -tmp^post1+tmp^0 == 0 /\ k^0-k^post1 == 0 /\ -100+k^0 <= 0 /\ -j^post1+j^0 == 0), cost: 1 New rule: l0 -> l1 : i^0'=0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^post1, (0 == 0 /\ -100+k^0 <= 0), cost: 1 propagated equality i^post1 = 0 propagated equality tmp^post1 = tmp^0 propagated equality k^post1 = k^0 propagated equality j^post1 = j^0 Simplified Guard Original rule: l0 -> l1 : i^0'=0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^post1, (0 == 0 /\ -100+k^0 <= 0), cost: 1 New rule: l0 -> l1 : i^0'=0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^post1, -100+k^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l0 -> l1 : i^0'=0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^post1, -100+k^0 <= 0, cost: 1 New rule: l0 -> l1 : i^0'=0, tmp___0^0'=tmp___0^post1, -100+k^0 <= 0, cost: 1 Propagated Equalities Original rule: l0 -> l2 : i^0'=i^post2, j^0'=j^post2, k^0'=k^post2, tmp^0'=tmp^post2, tmp___0^0'=tmp___0^post2, (-k^post2+k^0 == 0 /\ 101-k^0 <= 0 /\ -j^post2+j^0 == 0 /\ tmp^0-tmp^post2 == 0 /\ tmp___0^0-tmp___0^post2 == 0 /\ i^0-i^post2 == 0), cost: 1 New rule: l0 -> l2 : i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 101-k^0 <= 0), cost: 1 propagated equality k^post2 = k^0 propagated equality j^post2 = j^0 propagated equality tmp^post2 = tmp^0 propagated equality tmp___0^post2 = tmp___0^0 propagated equality i^post2 = i^0 Simplified Guard Original rule: l0 -> l2 : i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 101-k^0 <= 0), cost: 1 New rule: l0 -> l2 : i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 101-k^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l0 -> l2 : i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 101-k^0 <= 0, cost: 1 New rule: l0 -> l2 : 101-k^0 <= 0, cost: 1 Propagated Equalities Original rule: l3 -> l0 : i^0'=i^post3, j^0'=j^post3, k^0'=k^post3, tmp^0'=tmp^post3, tmp___0^0'=tmp___0^post3, (k^0-k^post3 == 0 /\ -j^post3+j^0 == 0 /\ 1-k^0 <= 0 /\ i^0-i^post3 == 0 /\ tmp___0^0-tmp___0^post3 == 0 /\ -tmp^post3+tmp^0 == 0), cost: 1 New rule: l3 -> l0 : i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 1-k^0 <= 0), cost: 1 propagated equality k^post3 = k^0 propagated equality j^post3 = j^0 propagated equality i^post3 = i^0 propagated equality tmp___0^post3 = tmp___0^0 propagated equality tmp^post3 = tmp^0 Simplified Guard Original rule: l3 -> l0 : i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 1-k^0 <= 0), cost: 1 New rule: l3 -> l0 : i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 1-k^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l3 -> l0 : i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 1-k^0 <= 0, cost: 1 New rule: l3 -> l0 : 1-k^0 <= 0, cost: 1 Propagated Equalities Original rule: l3 -> l2 : i^0'=i^post4, j^0'=j^post4, k^0'=k^post4, tmp^0'=tmp^post4, tmp___0^0'=tmp___0^post4, (tmp^0-tmp^post4 == 0 /\ tmp___0^0-tmp___0^post4 == 0 /\ i^0-i^post4 == 0 /\ -j^post4+j^0 == 0 /\ k^0 <= 0 /\ -k^post4+k^0 == 0), cost: 1 New rule: l3 -> l2 : i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ k^0 <= 0), cost: 1 propagated equality tmp^post4 = tmp^0 propagated equality tmp___0^post4 = tmp___0^0 propagated equality i^post4 = i^0 propagated equality j^post4 = j^0 propagated equality k^post4 = k^0 Simplified Guard Original rule: l3 -> l2 : i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ k^0 <= 0), cost: 1 New rule: l3 -> l2 : i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, k^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l3 -> l2 : i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, k^0 <= 0, cost: 1 New rule: l3 -> l2 : k^0 <= 0, cost: 1 Propagated Equalities Original rule: l1 -> l4 : i^0'=i^post5, j^0'=j^post5, k^0'=k^post5, tmp^0'=tmp^post5, tmp___0^0'=tmp___0^post5, (-j^post5+j^0 == 0 /\ tmp___0^0-tmp___0^post5 == 0 /\ k^0-k^post5 == 0 /\ i^0-i^post5 == 0 /\ -tmp^post5+tmp^0 == 0), cost: 1 New rule: l1 -> l4 : i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1 propagated equality j^post5 = j^0 propagated equality tmp___0^post5 = tmp___0^0 propagated equality k^post5 = k^0 propagated equality i^post5 = i^0 propagated equality tmp^post5 = tmp^0 Simplified Guard Original rule: l1 -> l4 : i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1 New rule: l1 -> l4 : i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1 Removed Trivial Updates Original rule: l1 -> l4 : i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1 New rule: l1 -> l4 : T, cost: 1 Propagated Equalities Original rule: l5 -> l2 : i^0'=i^post6, j^0'=j^post6, k^0'=k^post6, tmp^0'=tmp^post6, tmp___0^0'=tmp___0^post6, (tmp^0-tmp^post6 == 0 /\ i^0-i^post6 == 0 /\ -j^post6+j^0 == 0 /\ i^0-j^0 <= 0 /\ -k^post6+k^0 == 0 /\ -tmp___0^post6+tmp___0^0 == 0), cost: 1 New rule: l5 -> l2 : i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ i^0-j^0 <= 0), cost: 1 propagated equality tmp^post6 = tmp^0 propagated equality i^post6 = i^0 propagated equality j^post6 = j^0 propagated equality k^post6 = k^0 propagated equality tmp___0^post6 = tmp___0^0 Simplified Guard Original rule: l5 -> l2 : i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ i^0-j^0 <= 0), cost: 1 New rule: l5 -> l2 : i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, i^0-j^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l5 -> l2 : i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, i^0-j^0 <= 0, cost: 1 New rule: l5 -> l2 : i^0-j^0 <= 0, cost: 1 Propagated Equalities Original rule: l5 -> l6 : i^0'=i^post7, j^0'=j^post7, k^0'=k^post7, tmp^0'=tmp^post7, tmp___0^0'=tmp___0^post7, (k^0-k^post7 == 0 /\ -tmp^post7+tmp^0 == 0 /\ i^0-i^post7 == 0 /\ 1-i^0+j^0 <= 0 /\ tmp___0^0-tmp___0^post7 == 0 /\ -1-j^0+j^post7 == 0), cost: 1 New rule: l5 -> l6 : i^0'=i^0, j^0'=1+j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 1-i^0+j^0 <= 0), cost: 1 propagated equality k^post7 = k^0 propagated equality tmp^post7 = tmp^0 propagated equality i^post7 = i^0 propagated equality tmp___0^post7 = tmp___0^0 propagated equality j^post7 = 1+j^0 Simplified Guard Original rule: l5 -> l6 : i^0'=i^0, j^0'=1+j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 1-i^0+j^0 <= 0), cost: 1 New rule: l5 -> l6 : i^0'=i^0, j^0'=1+j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 1-i^0+j^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l5 -> l6 : i^0'=i^0, j^0'=1+j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 1-i^0+j^0 <= 0, cost: 1 New rule: l5 -> l6 : j^0'=1+j^0, 1-i^0+j^0 <= 0, cost: 1 Propagated Equalities Original rule: l7 -> l6 : i^0'=i^post8, j^0'=j^post8, k^0'=k^post8, tmp^0'=tmp^post8, tmp___0^0'=tmp___0^post8, (-k^post8+k^0 == 0 /\ -tmp___0^post8+tmp___0^0 == 0 /\ j^post8 == 0 /\ 1-i^0+i^post8 == 0 /\ tmp^0-tmp^post8 == 0), cost: 1 New rule: l7 -> l6 : i^0'=-1+i^0, j^0'=0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1 propagated equality k^post8 = k^0 propagated equality tmp___0^post8 = tmp___0^0 propagated equality j^post8 = 0 propagated equality i^post8 = -1+i^0 propagated equality tmp^post8 = tmp^0 Simplified Guard Original rule: l7 -> l6 : i^0'=-1+i^0, j^0'=0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1 New rule: l7 -> l6 : i^0'=-1+i^0, j^0'=0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1 Removed Trivial Updates Original rule: l7 -> l6 : i^0'=-1+i^0, j^0'=0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1 New rule: l7 -> l6 : i^0'=-1+i^0, j^0'=0, T, cost: 1 Propagated Equalities Original rule: l6 -> l5 : i^0'=i^post9, j^0'=j^post9, k^0'=k^post9, tmp^0'=tmp^post9, tmp___0^0'=tmp___0^post9, (tmp___0^0-tmp___0^post9 == 0 /\ j^0-j^post9 == 0 /\ -tmp^post9+tmp^0 == 0 /\ -k^post9+k^0 == 0 /\ i^0-i^post9 == 0), cost: 1 New rule: l6 -> l5 : i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1 propagated equality tmp___0^post9 = tmp___0^0 propagated equality j^post9 = j^0 propagated equality tmp^post9 = tmp^0 propagated equality k^post9 = k^0 propagated equality i^post9 = i^0 Simplified Guard Original rule: l6 -> l5 : i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1 New rule: l6 -> l5 : i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1 Removed Trivial Updates Original rule: l6 -> l5 : i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1 New rule: l6 -> l5 : T, cost: 1 Propagated Equalities Original rule: l8 -> l1 : i^0'=i^post10, j^0'=j^post10, k^0'=k^post10, tmp^0'=tmp^post10, tmp___0^0'=tmp___0^post10, (-tmp^post10+tmp^0 == 0 /\ -j^post10+j^0 == 0 /\ -tmp___0^post10+tmp___0^0 == 0 /\ k^0-k^post10 == 0 /\ -1+i^post10-i^0 == 0), cost: 1 New rule: l8 -> l1 : i^0'=1+i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1 propagated equality tmp^post10 = tmp^0 propagated equality j^post10 = j^0 propagated equality tmp___0^post10 = tmp___0^0 propagated equality k^post10 = k^0 propagated equality i^post10 = 1+i^0 Simplified Guard Original rule: l8 -> l1 : i^0'=1+i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1 New rule: l8 -> l1 : i^0'=1+i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1 Removed Trivial Updates Original rule: l8 -> l1 : i^0'=1+i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1 New rule: l8 -> l1 : i^0'=1+i^0, T, cost: 1 Propagated Equalities Original rule: l8 -> l7 : i^0'=i^post11, j^0'=j^post11, k^0'=k^post11, tmp^0'=tmp^post11, tmp___0^0'=tmp___0^post11, (-j^post11+j^0 == 0 /\ -tmp___0^post11+tmp___0^0 == 0 /\ i^0-i^post11 == 0 /\ -k^post11+k^0 == 0 /\ tmp^0-tmp^post11 == 0), cost: 1 New rule: l8 -> l7 : i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1 propagated equality j^post11 = j^0 propagated equality tmp___0^post11 = tmp___0^0 propagated equality i^post11 = i^0 propagated equality k^post11 = k^0 propagated equality tmp^post11 = tmp^0 Simplified Guard Original rule: l8 -> l7 : i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1 New rule: l8 -> l7 : i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1 Removed Trivial Updates Original rule: l8 -> l7 : i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1 New rule: l8 -> l7 : T, cost: 1 made implied equalities explicit Original rule: l4 -> l7 : i^0'=i^post12, j^0'=j^post12, k^0'=k^post12, tmp^0'=tmp^post12, tmp___0^0'=tmp___0^post12, (i^0-k^0 <= 0 /\ j^0-j^post12 == 0 /\ tmp___0^0-tmp___0^post12 == 0 /\ -i^0+k^0 <= 0 /\ -tmp^post12+tmp^0 == 0 /\ i^0-i^post12 == 0 /\ -k^post12+k^0 == 0), cost: 1 New rule: l4 -> l7 : i^0'=i^post12, j^0'=j^post12, k^0'=k^post12, tmp^0'=tmp^post12, tmp___0^0'=tmp___0^post12, (i^0-k^0 <= 0 /\ i^0-k^0 == 0 /\ j^0-j^post12 == 0 /\ tmp___0^0-tmp___0^post12 == 0 /\ -i^0+k^0 <= 0 /\ -tmp^post12+tmp^0 == 0 /\ i^0-i^post12 == 0 /\ -k^post12+k^0 == 0), cost: 1 Propagated Equalities Original rule: l4 -> l7 : i^0'=i^post12, j^0'=j^post12, k^0'=k^post12, tmp^0'=tmp^post12, tmp___0^0'=tmp___0^post12, (i^0-k^0 <= 0 /\ i^0-k^0 == 0 /\ j^0-j^post12 == 0 /\ tmp___0^0-tmp___0^post12 == 0 /\ -i^0+k^0 <= 0 /\ -tmp^post12+tmp^0 == 0 /\ i^0-i^post12 == 0 /\ -k^post12+k^0 == 0), cost: 1 New rule: l4 -> l7 : i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ i^0-k^0 <= 0 /\ i^0-k^0 == 0 /\ -i^0+k^0 <= 0), cost: 1 propagated equality j^post12 = j^0 propagated equality tmp___0^post12 = tmp___0^0 propagated equality tmp^post12 = tmp^0 propagated equality i^post12 = i^0 propagated equality k^post12 = k^0 Simplified Guard Original rule: l4 -> l7 : i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ i^0-k^0 <= 0 /\ i^0-k^0 == 0 /\ -i^0+k^0 <= 0), cost: 1 New rule: l4 -> l7 : i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (i^0-k^0 <= 0 /\ i^0-k^0 == 0 /\ -i^0+k^0 <= 0), cost: 1 made implied equalities explicit Original rule: l4 -> l7 : i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (i^0-k^0 <= 0 /\ i^0-k^0 == 0 /\ -i^0+k^0 <= 0), cost: 1 New rule: l4 -> l7 : i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (i^0-k^0 <= 0 /\ i^0-k^0 == 0 /\ -i^0+k^0 <= 0), cost: 1 Removed Trivial Updates Original rule: l4 -> l7 : i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (i^0-k^0 <= 0 /\ i^0-k^0 == 0 /\ -i^0+k^0 <= 0), cost: 1 New rule: l4 -> l7 : (i^0-k^0 <= 0 /\ i^0-k^0 == 0 /\ -i^0+k^0 <= 0), cost: 1 Propagated Equalities Original rule: l4 -> l8 : i^0'=i^post13, j^0'=j^post13, k^0'=k^post13, tmp^0'=tmp^post13, tmp___0^0'=tmp___0^post13, (-i^post13+i^0 == 0 /\ -j^post13+j^0 == 0 /\ tmp^0-tmp^post13 == 0 /\ k^0-k^post13 == 0 /\ -tmp___0^post13+tmp___0^0 == 0 /\ 1-i^0+k^0 <= 0), cost: 1 New rule: l4 -> l8 : i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 1-i^0+k^0 <= 0), cost: 1 propagated equality i^post13 = i^0 propagated equality j^post13 = j^0 propagated equality tmp^post13 = tmp^0 propagated equality k^post13 = k^0 propagated equality tmp___0^post13 = tmp___0^0 Simplified Guard Original rule: l4 -> l8 : i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 1-i^0+k^0 <= 0), cost: 1 New rule: l4 -> l8 : i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 1-i^0+k^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l4 -> l8 : i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 1-i^0+k^0 <= 0, cost: 1 New rule: l4 -> l8 : 1-i^0+k^0 <= 0, cost: 1 Propagated Equalities Original rule: l4 -> l8 : i^0'=i^post14, j^0'=j^post14, k^0'=k^post14, tmp^0'=tmp^post14, tmp___0^0'=tmp___0^post14, (-j^post14+j^0 == 0 /\ -k^post14+k^0 == 0 /\ tmp^0-tmp^post14 == 0 /\ tmp___0^0-tmp___0^post14 == 0 /\ 1+i^0-k^0 <= 0 /\ i^0-i^post14 == 0), cost: 1 New rule: l4 -> l8 : i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 1+i^0-k^0 <= 0), cost: 1 propagated equality j^post14 = j^0 propagated equality k^post14 = k^0 propagated equality tmp^post14 = tmp^0 propagated equality tmp___0^post14 = tmp___0^0 propagated equality i^post14 = i^0 Simplified Guard Original rule: l4 -> l8 : i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 1+i^0-k^0 <= 0), cost: 1 New rule: l4 -> l8 : i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 1+i^0-k^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l4 -> l8 : i^0'=i^0, j^0'=j^0, k^0'=k^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 1+i^0-k^0 <= 0, cost: 1 New rule: l4 -> l8 : 1+i^0-k^0 <= 0, cost: 1 Propagated Equalities Original rule: l10 -> l3 : i^0'=i^post15, j^0'=j^post15, k^0'=k^post15, tmp^0'=tmp^post15, tmp___0^0'=tmp___0^post15, (0 == 0 /\ tmp^0-tmp^post16 == 0 /\ j^post16-j^post15 == 0 /\ -tmp^post15+k^post15 == 0 /\ -j^post16+j^0 == 0 /\ i^0-i^post16 == 0 /\ tmp___0^post16-tmp___0^post15 == 0 /\ -i^post15+i^post16 == 0 /\ -k^post16+k^0 == 0 /\ -tmp___0^post16+tmp___0^0 == 0), cost: 1 New rule: l10 -> l3 : i^0'=i^post16, j^0'=j^post16, k^0'=tmp^post15, tmp^0'=tmp^post15, tmp___0^0'=tmp___0^post16, (0 == 0 /\ tmp^0-tmp^post16 == 0 /\ -j^post16+j^0 == 0 /\ i^0-i^post16 == 0 /\ -k^post16+k^0 == 0 /\ -tmp___0^post16+tmp___0^0 == 0), cost: 1 propagated equality j^post15 = j^post16 propagated equality k^post15 = tmp^post15 propagated equality tmp___0^post15 = tmp___0^post16 propagated equality i^post15 = i^post16 Propagated Equalities Original rule: l10 -> l3 : i^0'=i^post16, j^0'=j^post16, k^0'=tmp^post15, tmp^0'=tmp^post15, tmp___0^0'=tmp___0^post16, (0 == 0 /\ tmp^0-tmp^post16 == 0 /\ -j^post16+j^0 == 0 /\ i^0-i^post16 == 0 /\ -k^post16+k^0 == 0 /\ -tmp___0^post16+tmp___0^0 == 0), cost: 1 New rule: l10 -> l3 : i^0'=i^0, j^0'=j^0, k^0'=tmp^post15, tmp^0'=tmp^post15, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1 propagated equality tmp^post16 = tmp^0 propagated equality j^post16 = j^0 propagated equality i^post16 = i^0 propagated equality k^post16 = k^0 propagated equality tmp___0^post16 = tmp___0^0 Simplified Guard Original rule: l10 -> l3 : i^0'=i^0, j^0'=j^0, k^0'=tmp^post15, tmp^0'=tmp^post15, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1 New rule: l10 -> l3 : i^0'=i^0, j^0'=j^0, k^0'=tmp^post15, tmp^0'=tmp^post15, tmp___0^0'=tmp___0^0, T, cost: 1 Removed Trivial Updates Original rule: l10 -> l3 : i^0'=i^0, j^0'=j^0, k^0'=tmp^post15, tmp^0'=tmp^post15, tmp___0^0'=tmp___0^0, T, cost: 1 New rule: l10 -> l3 : k^0'=tmp^post15, tmp^0'=tmp^post15, T, cost: 1 Step with 31 Trace 31[T] Blocked [{}, {}] Step with 19 Trace 31[T], 19[(1-k^0 <= 0)] Blocked [{}, {}, {}] Step with 17 Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)] Blocked [{}, {}, {}, {}] Step with 21 Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 21[T] Blocked [{}, {}, {}, {}, {}] Step with 30 Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 21[T], 30[(1+i^0-k^0 <= 0)] Blocked [{}, {}, {}, {}, {28[T], 29[T]}, {}] Step with 27 Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 21[T], 30[(1+i^0-k^0 <= 0)], 27[T] Blocked [{}, {}, {}, {}, {28[T], 29[T]}, {}, {}] Step with 24 Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 21[T], 30[(1+i^0-k^0 <= 0)], 27[T], 24[T] Blocked [{}, {}, {}, {}, {28[T], 29[T]}, {}, {}, {}] Step with 25 Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 21[T], 30[(1+i^0-k^0 <= 0)], 27[T], 24[T], 25[T] Blocked [{}, {}, {}, {}, {28[T], 29[T]}, {}, {}, {}, {}] Step with 22 Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 21[T], 30[(1+i^0-k^0 <= 0)], 27[T], 24[T], 25[T], 22[(i^0-j^0 <= 0)] Blocked [{}, {}, {}, {}, {28[T], 29[T]}, {}, {}, {}, {}, {}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 21[T], 30[(1+i^0-k^0 <= 0)], 27[T], 24[T], 25[T] Blocked [{}, {}, {}, {}, {28[T], 29[T]}, {}, {}, {}, {22[T]}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 21[T], 30[(1+i^0-k^0 <= 0)], 27[T], 24[T] Blocked [{}, {}, {}, {}, {28[T], 29[T]}, {}, {}, {25[T]}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 21[T], 30[(1+i^0-k^0 <= 0)], 27[T] Blocked [{}, {}, {}, {}, {28[T], 29[T]}, {}, {24[T]}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 21[T], 30[(1+i^0-k^0 <= 0)] Blocked [{}, {}, {}, {}, {28[T], 29[T]}, {27[T]}] Step with 26 Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 21[T], 30[(1+i^0-k^0 <= 0)], 26[T] Blocked [{}, {}, {}, {}, {28[T], 29[T]}, {27[T]}, {}] Accelerate Start location: l10 Program variables: i^0 j^0 k^0 tmp^0 tmp___0^0 17: l0 -> l1 : i^0'=0, tmp___0^0'=tmp___0^post1, -100+k^0 <= 0, cost: 1 18: l0 -> l2 : 101-k^0 <= 0, cost: 1 21: l1 -> l4 : T, cost: 1 32: l1 -> l1 : i^0'=i^0+n, (-1+n >= 0 /\ -i^0-n+k^0 >= 0), cost: 1 19: l3 -> l0 : 1-k^0 <= 0, cost: 1 20: l3 -> l2 : k^0 <= 0, cost: 1 28: l4 -> l7 : (i^0-k^0 <= 0 /\ i^0-k^0 == 0 /\ -i^0+k^0 <= 0), cost: 1 29: l4 -> l8 : 1-i^0+k^0 <= 0, cost: 1 30: l4 -> l8 : 1+i^0-k^0 <= 0, cost: 1 22: l5 -> l2 : i^0-j^0 <= 0, cost: 1 23: l5 -> l6 : j^0'=1+j^0, 1-i^0+j^0 <= 0, cost: 1 25: l6 -> l5 : T, cost: 1 24: l7 -> l6 : i^0'=-1+i^0, j^0'=0, T, cost: 1 26: l8 -> l1 : i^0'=1+i^0, T, cost: 1 27: l8 -> l7 : T, cost: 1 31: l10 -> l3 : k^0'=tmp^post15, tmp^0'=tmp^post15, T, cost: 1 Loop Acceleration Original rule: l1 -> l1 : i^0'=1+i^0, 1+i^0-k^0 <= 0, cost: 1 New rule: l1 -> l1 : i^0'=i^0+n, (-1+n >= 0 /\ -i^0-n+k^0 >= 0), cost: 1 -1-i^0+k^0 >= 0 [0]: montonic decrease yields -i^0-n+k^0 >= 0 -1-i^0+k^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ -1-i^0+k^0 >= 0) Replacement map: {-1-i^0+k^0 >= 0 -> -i^0-n+k^0 >= 0} Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 32[(-1+n >= 0 /\ -i^0-n+k^0 >= 0)] Blocked [{}, {}, {}, {}, {32[T]}] Step with 21 Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 32[(-1+n >= 0 /\ -i^0-n+k^0 >= 0)], 21[T] Blocked [{}, {}, {}, {}, {32[T]}, {}] Step with 30 Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 32[(-1+n >= 0 /\ -i^0-n+k^0 >= 0)], 21[T], 30[(1+i^0-k^0 <= 0)] Blocked [{}, {}, {}, {}, {32[T]}, {}, {}] Step with 26 Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 32[(-1+n >= 0 /\ -i^0-n+k^0 >= 0)], 21[T], 30[(1+i^0-k^0 <= 0)], 26[T] Blocked [{}, {}, {}, {}, {32[T]}, {}, {}, {}] Covered Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 32[(-1+n >= 0 /\ -i^0-n+k^0 >= 0)], 21[T], 30[(1+i^0-k^0 <= 0)] Blocked [{}, {}, {}, {}, {32[T]}, {}, {26[T]}] Step with 27 Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 32[(-1+n >= 0 /\ -i^0-n+k^0 >= 0)], 21[T], 30[(1+i^0-k^0 <= 0)], 27[T] Blocked [{}, {}, {}, {}, {32[T]}, {}, {26[T]}, {}] Step with 24 Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 32[(-1+n >= 0 /\ -i^0-n+k^0 >= 0)], 21[T], 30[(1+i^0-k^0 <= 0)], 27[T], 24[T] Blocked [{}, {}, {}, {}, {32[T]}, {}, {26[T]}, {}, {}] Step with 25 Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 32[(-1+n >= 0 /\ -i^0-n+k^0 >= 0)], 21[T], 30[(1+i^0-k^0 <= 0)], 27[T], 24[T], 25[T] Blocked [{}, {}, {}, {}, {32[T]}, {}, {26[T]}, {}, {}, {}] Step with 22 Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 32[(-1+n >= 0 /\ -i^0-n+k^0 >= 0)], 21[T], 30[(1+i^0-k^0 <= 0)], 27[T], 24[T], 25[T], 22[(i^0-j^0 <= 0)] Blocked [{}, {}, {}, {}, {32[T]}, {}, {26[T]}, {}, {}, {}, {}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 32[(-1+n >= 0 /\ -i^0-n+k^0 >= 0)], 21[T], 30[(1+i^0-k^0 <= 0)], 27[T], 24[T], 25[T] Blocked [{}, {}, {}, {}, {32[T]}, {}, {26[T]}, {}, {}, {22[T]}] Step with 23 Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 32[(-1+n >= 0 /\ -i^0-n+k^0 >= 0)], 21[T], 30[(1+i^0-k^0 <= 0)], 27[T], 24[T], 25[T], 23[(1-i^0+j^0 <= 0)] Blocked [{}, {}, {}, {}, {32[T]}, {}, {26[T]}, {}, {}, {22[T]}, {}] Accelerate Start location: l10 Program variables: i^0 j^0 k^0 tmp^0 tmp___0^0 17: l0 -> l1 : i^0'=0, tmp___0^0'=tmp___0^post1, -100+k^0 <= 0, cost: 1 18: l0 -> l2 : 101-k^0 <= 0, cost: 1 21: l1 -> l4 : T, cost: 1 32: l1 -> l1 : i^0'=i^0+n, (-1+n >= 0 /\ -i^0-n+k^0 >= 0), cost: 1 19: l3 -> l0 : 1-k^0 <= 0, cost: 1 20: l3 -> l2 : k^0 <= 0, cost: 1 28: l4 -> l7 : (i^0-k^0 <= 0 /\ i^0-k^0 == 0 /\ -i^0+k^0 <= 0), cost: 1 29: l4 -> l8 : 1-i^0+k^0 <= 0, cost: 1 30: l4 -> l8 : 1+i^0-k^0 <= 0, cost: 1 22: l5 -> l2 : i^0-j^0 <= 0, cost: 1 23: l5 -> l6 : j^0'=1+j^0, 1-i^0+j^0 <= 0, cost: 1 25: l6 -> l5 : T, cost: 1 33: l6 -> l6 : j^0'=j^0+n2, (-1+n2 >= 0 /\ i^0-j^0-n2 >= 0), cost: 1 24: l7 -> l6 : i^0'=-1+i^0, j^0'=0, T, cost: 1 26: l8 -> l1 : i^0'=1+i^0, T, cost: 1 27: l8 -> l7 : T, cost: 1 31: l10 -> l3 : k^0'=tmp^post15, tmp^0'=tmp^post15, T, cost: 1 Loop Acceleration Original rule: l6 -> l6 : j^0'=1+j^0, 1-i^0+j^0 <= 0, cost: 1 New rule: l6 -> l6 : j^0'=j^0+n2, (-1+n2 >= 0 /\ i^0-j^0-n2 >= 0), cost: 1 -1+i^0-j^0 >= 0 [0]: montonic decrease yields i^0-j^0-n2 >= 0 -1+i^0-j^0 >= 0 [1]: eventual increase yields (-1+i^0-j^0 >= 0 /\ 1 <= 0) Replacement map: {-1+i^0-j^0 >= 0 -> i^0-j^0-n2 >= 0} Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 32[(-1+n >= 0 /\ -i^0-n+k^0 >= 0)], 21[T], 30[(1+i^0-k^0 <= 0)], 27[T], 24[T], 33[(-1+n2 >= 0 /\ i^0-j^0-n2 >= 0)] Blocked [{}, {}, {}, {}, {32[T]}, {}, {26[T]}, {}, {}, {33[T]}] Step with 25 Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 32[(-1+n >= 0 /\ -i^0-n+k^0 >= 0)], 21[T], 30[(1+i^0-k^0 <= 0)], 27[T], 24[T], 33[(-1+n2 >= 0 /\ i^0-j^0-n2 >= 0)], 25[T] Blocked [{}, {}, {}, {}, {32[T]}, {}, {26[T]}, {}, {}, {33[T]}, {}] Step with 23 Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 32[(-1+n >= 0 /\ -i^0-n+k^0 >= 0)], 21[T], 30[(1+i^0-k^0 <= 0)], 27[T], 24[T], 33[(-1+n2 >= 0 /\ i^0-j^0-n2 >= 0)], 25[T], 23[(1-i^0+j^0 <= 0)] Blocked [{}, {}, {}, {}, {32[T]}, {}, {26[T]}, {}, {}, {33[T]}, {}, {}] Covered Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 32[(-1+n >= 0 /\ -i^0-n+k^0 >= 0)], 21[T], 30[(1+i^0-k^0 <= 0)], 27[T], 24[T], 33[(-1+n2 >= 0 /\ i^0-j^0-n2 >= 0)], 25[T] Blocked [{}, {}, {}, {}, {32[T]}, {}, {26[T]}, {}, {}, {33[T]}, {23[T]}] Step with 22 Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 32[(-1+n >= 0 /\ -i^0-n+k^0 >= 0)], 21[T], 30[(1+i^0-k^0 <= 0)], 27[T], 24[T], 33[(-1+n2 >= 0 /\ i^0-j^0-n2 >= 0)], 25[T], 22[(i^0-j^0 <= 0)] Blocked [{}, {}, {}, {}, {32[T]}, {}, {26[T]}, {}, {}, {33[T]}, {23[T]}, {}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 32[(-1+n >= 0 /\ -i^0-n+k^0 >= 0)], 21[T], 30[(1+i^0-k^0 <= 0)], 27[T], 24[T], 33[(-1+n2 >= 0 /\ i^0-j^0-n2 >= 0)], 25[T] Blocked [{}, {}, {}, {}, {32[T]}, {}, {26[T]}, {}, {}, {33[T]}, {22[T], 23[T]}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 32[(-1+n >= 0 /\ -i^0-n+k^0 >= 0)], 21[T], 30[(1+i^0-k^0 <= 0)], 27[T], 24[T], 33[(-1+n2 >= 0 /\ i^0-j^0-n2 >= 0)] Blocked [{}, {}, {}, {}, {32[T]}, {}, {26[T]}, {}, {}, {25[T], 33[T]}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 32[(-1+n >= 0 /\ -i^0-n+k^0 >= 0)], 21[T], 30[(1+i^0-k^0 <= 0)], 27[T], 24[T] Blocked [{}, {}, {}, {}, {32[T]}, {}, {26[T]}, {}, {33[T]}] Step with 25 Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 32[(-1+n >= 0 /\ -i^0-n+k^0 >= 0)], 21[T], 30[(1+i^0-k^0 <= 0)], 27[T], 24[T], 25[T] Blocked [{}, {}, {}, {}, {32[T]}, {}, {26[T]}, {}, {33[T]}, {}] Step with 22 Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 32[(-1+n >= 0 /\ -i^0-n+k^0 >= 0)], 21[T], 30[(1+i^0-k^0 <= 0)], 27[T], 24[T], 25[T], 22[(i^0-j^0 <= 0)] Blocked [{}, {}, {}, {}, {32[T]}, {}, {26[T]}, {}, {33[T]}, {}, {}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 32[(-1+n >= 0 /\ -i^0-n+k^0 >= 0)], 21[T], 30[(1+i^0-k^0 <= 0)], 27[T], 24[T], 25[T] Blocked [{}, {}, {}, {}, {32[T]}, {}, {26[T]}, {}, {33[T]}, {22[T]}] Step with 23 Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 32[(-1+n >= 0 /\ -i^0-n+k^0 >= 0)], 21[T], 30[(1+i^0-k^0 <= 0)], 27[T], 24[T], 25[T], 23[(1-i^0+j^0 <= 0)] Blocked [{}, {}, {}, {}, {32[T]}, {}, {26[T]}, {}, {33[T]}, {22[T]}, {}] Covered Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 32[(-1+n >= 0 /\ -i^0-n+k^0 >= 0)], 21[T], 30[(1+i^0-k^0 <= 0)], 27[T], 24[T], 25[T] Blocked [{}, {}, {}, {}, {32[T]}, {}, {26[T]}, {}, {33[T]}, {22[T], 23[T]}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 32[(-1+n >= 0 /\ -i^0-n+k^0 >= 0)], 21[T], 30[(1+i^0-k^0 <= 0)], 27[T], 24[T] Blocked [{}, {}, {}, {}, {32[T]}, {}, {26[T]}, {}, {25[T], 33[T]}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 32[(-1+n >= 0 /\ -i^0-n+k^0 >= 0)], 21[T], 30[(1+i^0-k^0 <= 0)], 27[T] Blocked [{}, {}, {}, {}, {32[T]}, {}, {26[T]}, {24[T]}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 32[(-1+n >= 0 /\ -i^0-n+k^0 >= 0)], 21[T], 30[(1+i^0-k^0 <= 0)] Blocked [{}, {}, {}, {}, {32[T]}, {}, {26[T], 27[T]}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 32[(-1+n >= 0 /\ -i^0-n+k^0 >= 0)], 21[T] Blocked [{}, {}, {}, {}, {32[T]}, {30[T]}] Step with 28 Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 32[(-1+n >= 0 /\ -i^0-n+k^0 >= 0)], 21[T], 28[(i^0-k^0 <= 0 /\ i^0-k^0 == 0 /\ -i^0+k^0 <= 0)] Blocked [{}, {}, {}, {}, {32[T]}, {30[T]}, {}] Step with 24 Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 32[(-1+n >= 0 /\ -i^0-n+k^0 >= 0)], 21[T], 28[(i^0-k^0 <= 0 /\ i^0-k^0 == 0 /\ -i^0+k^0 <= 0)], 24[T] Blocked [{}, {}, {}, {}, {32[T]}, {30[T]}, {}, {}] Step with 25 Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 32[(-1+n >= 0 /\ -i^0-n+k^0 >= 0)], 21[T], 28[(i^0-k^0 <= 0 /\ i^0-k^0 == 0 /\ -i^0+k^0 <= 0)], 24[T], 25[T] Blocked [{}, {}, {}, {}, {32[T]}, {30[T]}, {}, {}, {}] Step with 23 Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 32[(-1+n >= 0 /\ -i^0-n+k^0 >= 0)], 21[T], 28[(i^0-k^0 <= 0 /\ i^0-k^0 == 0 /\ -i^0+k^0 <= 0)], 24[T], 25[T], 23[(1-i^0+j^0 <= 0)] Blocked [{}, {}, {}, {}, {32[T]}, {30[T]}, {}, {}, {}, {}] Covered Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 32[(-1+n >= 0 /\ -i^0-n+k^0 >= 0)], 21[T], 28[(i^0-k^0 <= 0 /\ i^0-k^0 == 0 /\ -i^0+k^0 <= 0)], 24[T], 25[T] Blocked [{}, {}, {}, {}, {32[T]}, {30[T]}, {}, {}, {23[T]}] Step with 22 Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 32[(-1+n >= 0 /\ -i^0-n+k^0 >= 0)], 21[T], 28[(i^0-k^0 <= 0 /\ i^0-k^0 == 0 /\ -i^0+k^0 <= 0)], 24[T], 25[T], 22[(i^0-j^0 <= 0)] Blocked [{}, {}, {}, {}, {32[T]}, {30[T]}, {}, {}, {23[T]}, {}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 32[(-1+n >= 0 /\ -i^0-n+k^0 >= 0)], 21[T], 28[(i^0-k^0 <= 0 /\ i^0-k^0 == 0 /\ -i^0+k^0 <= 0)], 24[T], 25[T] Blocked [{}, {}, {}, {}, {32[T]}, {30[T]}, {}, {}, {22[T], 23[T]}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 32[(-1+n >= 0 /\ -i^0-n+k^0 >= 0)], 21[T], 28[(i^0-k^0 <= 0 /\ i^0-k^0 == 0 /\ -i^0+k^0 <= 0)], 24[T] Blocked [{}, {}, {}, {}, {32[T]}, {30[T]}, {}, {25[T]}] Step with 33 Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 32[(-1+n >= 0 /\ -i^0-n+k^0 >= 0)], 21[T], 28[(i^0-k^0 <= 0 /\ i^0-k^0 == 0 /\ -i^0+k^0 <= 0)], 24[T], 33[(-1+n2 >= 0 /\ i^0-j^0-n2 >= 0)] Blocked [{}, {}, {}, {}, {32[T]}, {30[T]}, {}, {25[T]}, {33[T]}] Step with 25 Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 32[(-1+n >= 0 /\ -i^0-n+k^0 >= 0)], 21[T], 28[(i^0-k^0 <= 0 /\ i^0-k^0 == 0 /\ -i^0+k^0 <= 0)], 24[T], 33[(-1+n2 >= 0 /\ i^0-j^0-n2 >= 0)], 25[T] Blocked [{}, {}, {}, {}, {32[T]}, {30[T]}, {}, {25[T]}, {33[T]}, {}] Step with 22 Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 32[(-1+n >= 0 /\ -i^0-n+k^0 >= 0)], 21[T], 28[(i^0-k^0 <= 0 /\ i^0-k^0 == 0 /\ -i^0+k^0 <= 0)], 24[T], 33[(-1+n2 >= 0 /\ i^0-j^0-n2 >= 0)], 25[T], 22[(i^0-j^0 <= 0)] Blocked [{}, {}, {}, {}, {32[T]}, {30[T]}, {}, {25[T]}, {33[T]}, {}, {}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 32[(-1+n >= 0 /\ -i^0-n+k^0 >= 0)], 21[T], 28[(i^0-k^0 <= 0 /\ i^0-k^0 == 0 /\ -i^0+k^0 <= 0)], 24[T], 33[(-1+n2 >= 0 /\ i^0-j^0-n2 >= 0)], 25[T] Blocked [{}, {}, {}, {}, {32[T]}, {30[T]}, {}, {25[T]}, {33[T]}, {22[T]}] Step with 23 Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 32[(-1+n >= 0 /\ -i^0-n+k^0 >= 0)], 21[T], 28[(i^0-k^0 <= 0 /\ i^0-k^0 == 0 /\ -i^0+k^0 <= 0)], 24[T], 33[(-1+n2 >= 0 /\ i^0-j^0-n2 >= 0)], 25[T], 23[(1-i^0+j^0 <= 0)] Blocked [{}, {}, {}, {}, {32[T]}, {30[T]}, {}, {25[T]}, {33[T]}, {22[T]}, {}] Covered Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 32[(-1+n >= 0 /\ -i^0-n+k^0 >= 0)], 21[T], 28[(i^0-k^0 <= 0 /\ i^0-k^0 == 0 /\ -i^0+k^0 <= 0)], 24[T], 33[(-1+n2 >= 0 /\ i^0-j^0-n2 >= 0)], 25[T] Blocked [{}, {}, {}, {}, {32[T]}, {30[T]}, {}, {25[T]}, {33[T]}, {22[T], 23[T]}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 32[(-1+n >= 0 /\ -i^0-n+k^0 >= 0)], 21[T], 28[(i^0-k^0 <= 0 /\ i^0-k^0 == 0 /\ -i^0+k^0 <= 0)], 24[T], 33[(-1+n2 >= 0 /\ i^0-j^0-n2 >= 0)] Blocked [{}, {}, {}, {}, {32[T]}, {30[T]}, {}, {25[T]}, {25[T], 33[T]}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 32[(-1+n >= 0 /\ -i^0-n+k^0 >= 0)], 21[T], 28[(i^0-k^0 <= 0 /\ i^0-k^0 == 0 /\ -i^0+k^0 <= 0)], 24[T] Blocked [{}, {}, {}, {}, {32[T]}, {30[T]}, {}, {25[T], 33[T]}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 32[(-1+n >= 0 /\ -i^0-n+k^0 >= 0)], 21[T], 28[(i^0-k^0 <= 0 /\ i^0-k^0 == 0 /\ -i^0+k^0 <= 0)] Blocked [{}, {}, {}, {}, {32[T]}, {30[T]}, {24[T]}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 32[(-1+n >= 0 /\ -i^0-n+k^0 >= 0)], 21[T] Blocked [{}, {}, {}, {}, {32[T]}, {28[T], 30[T]}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 32[(-1+n >= 0 /\ -i^0-n+k^0 >= 0)] Blocked [{}, {}, {}, {}, {21[T], 32[T]}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)] Blocked [{}, {}, {}, {32[T]}] Step with 21 Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 21[T] Blocked [{}, {}, {}, {32[T]}, {}] Step with 30 Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 21[T], 30[(1+i^0-k^0 <= 0)] Blocked [{}, {}, {}, {32[T]}, {28[T], 29[T]}, {}] Step with 27 Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 21[T], 30[(1+i^0-k^0 <= 0)], 27[T] Blocked [{}, {}, {}, {32[T]}, {28[T], 29[T]}, {}, {}] Step with 24 Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 21[T], 30[(1+i^0-k^0 <= 0)], 27[T], 24[T] Blocked [{}, {}, {}, {32[T]}, {28[T], 29[T]}, {}, {}, {}] Step with 25 Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 21[T], 30[(1+i^0-k^0 <= 0)], 27[T], 24[T], 25[T] Blocked [{}, {}, {}, {32[T]}, {28[T], 29[T]}, {}, {}, {}, {}] Step with 22 Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 21[T], 30[(1+i^0-k^0 <= 0)], 27[T], 24[T], 25[T], 22[(i^0-j^0 <= 0)] Blocked [{}, {}, {}, {32[T]}, {28[T], 29[T]}, {}, {}, {}, {23[T]}, {}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 21[T], 30[(1+i^0-k^0 <= 0)], 27[T], 24[T], 25[T] Blocked [{}, {}, {}, {32[T]}, {28[T], 29[T]}, {}, {}, {}, {22[T], 23[T]}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 21[T], 30[(1+i^0-k^0 <= 0)], 27[T], 24[T] Blocked [{}, {}, {}, {32[T]}, {28[T], 29[T]}, {}, {}, {25[T]}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 21[T], 30[(1+i^0-k^0 <= 0)], 27[T] Blocked [{}, {}, {}, {32[T]}, {28[T], 29[T]}, {}, {24[T]}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 21[T], 30[(1+i^0-k^0 <= 0)] Blocked [{}, {}, {}, {32[T]}, {28[T], 29[T]}, {27[T]}] Step with 26 Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 21[T], 30[(1+i^0-k^0 <= 0)], 26[T] Blocked [{}, {}, {}, {32[T]}, {28[T], 29[T]}, {27[T]}, {}] Covered Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 21[T], 30[(1+i^0-k^0 <= 0)] Blocked [{}, {}, {}, {32[T]}, {28[T], 29[T]}, {26[T], 27[T]}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)], 21[T] Blocked [{}, {}, {}, {32[T]}, {28[T], 29[T], 30[T]}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)], 17[(-100+k^0 <= 0)] Blocked [{}, {}, {}, {21[T], 32[T]}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)] Blocked [{}, {}, {17[T]}] Step with 18 Trace 31[T], 19[(1-k^0 <= 0)], 18[(101-k^0 <= 0)] Blocked [{}, {}, {17[T]}, {}] Backtrack Trace 31[T], 19[(1-k^0 <= 0)] Blocked [{}, {}, {17[T], 18[T]}] Backtrack Trace 31[T] Blocked [{}, {19[T]}] Step with 20 Trace 31[T], 20[(k^0 <= 0)] Blocked [{}, {19[T]}, {}] Backtrack Trace 31[T] Blocked [{}, {19[T], 20[T]}] Backtrack Trace Blocked [{31[T]}] Accept unknown Build SHA: a05f16bf13df659c382799650051f91bf6828c7b