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