unknown Initial ITS Start location: l6 Program variables: i^0 j^0 y4^0 y6^0 y8^0 0: l0 -> l1 : i^0'=i^post1, j^0'=j^post1, y4^0'=y4^post1, y6^0'=y6^post1, y8^0'=y8^post1, (-y8^post1+y8^0 == 0 /\ -y6^post1+y6^0 == 0 /\ -i^post1+i^0 == 0 /\ 100-i^0 <= 0 /\ y4^0-y4^post1 == 0 /\ -100+j^post1 == 0), cost: 1 1: l0 -> l2 : i^0'=i^post2, j^0'=j^post2, y4^0'=y4^post2, y6^0'=y6^post2, y8^0'=y8^post2, (-99+i^0 <= 0 /\ -1-i^0+i^post2 == 0 /\ y4^post2-i^0 == 0 /\ y6^post2-i^0 == 0 /\ y8^0-y8^post2 == 0 /\ -j^post2+j^0 == 0), cost: 1 5: l1 -> l3 : i^0'=i^post6, j^0'=j^post6, y4^0'=y4^post6, y6^0'=y6^post6, y8^0'=y8^post6, (i^0-i^post6 == 0 /\ -j^post6+j^0 == 0 /\ -y8^post6+y8^0 == 0 /\ -y4^post6+y4^0 == 0 /\ y6^0-y6^post6 == 0), cost: 1 2: l2 -> l0 : i^0'=i^post3, j^0'=j^post3, y4^0'=y4^post3, y6^0'=y6^post3, y8^0'=y8^post3, (-i^post3+i^0 == 0 /\ j^0-j^post3 == 0 /\ -y6^post3+y6^0 == 0 /\ -y8^post3+y8^0 == 0 /\ y4^0-y4^post3 == 0), cost: 1 3: l3 -> l4 : i^0'=i^post4, j^0'=j^post4, y4^0'=y4^post4, y6^0'=y6^post4, y8^0'=y8^post4, (-j^post4+j^0 == 0 /\ i^0-i^post4 == 0 /\ 200-j^0 <= 0 /\ -y4^post4+y4^0 == 0 /\ y8^0-y8^post4 == 0 /\ y6^0-y6^post4 == 0), cost: 1 4: l3 -> l1 : i^0'=i^post5, j^0'=j^post5, y4^0'=y4^post5, y6^0'=y6^post5, y8^0'=y8^post5, (-j^0+y8^post5 == 0 /\ -1-j^0+j^post5 == 0 /\ -199+j^0 <= 0 /\ -i^post5+i^0 == 0 /\ y4^0-y4^post5 == 0 /\ -y6^post5+y6^0 == 0), cost: 1 6: l5 -> l2 : i^0'=i^post7, j^0'=j^post7, y4^0'=y4^post7, y6^0'=y6^post7, y8^0'=y8^post7, (y6^0-y6^post7 == 0 /\ -y8^post7+y8^0 == 0 /\ i^post7 == 0 /\ j^0-j^post7 == 0 /\ y4^0-y4^post7 == 0), cost: 1 7: l6 -> l5 : i^0'=i^post8, j^0'=j^post8, y4^0'=y4^post8, y6^0'=y6^post8, y8^0'=y8^post8, (i^0-i^post8 == 0 /\ y4^0-y4^post8 == 0 /\ -y8^post8+y8^0 == 0 /\ y6^0-y6^post8 == 0 /\ -j^post8+j^0 == 0), cost: 1 Chained Linear Paths Start location: l6 Program variables: i^0 j^0 y4^0 y6^0 y8^0 0: l0 -> l1 : i^0'=i^post1, j^0'=j^post1, y4^0'=y4^post1, y6^0'=y6^post1, y8^0'=y8^post1, (-y8^post1+y8^0 == 0 /\ -y6^post1+y6^0 == 0 /\ -i^post1+i^0 == 0 /\ 100-i^0 <= 0 /\ y4^0-y4^post1 == 0 /\ -100+j^post1 == 0), cost: 1 1: l0 -> l2 : i^0'=i^post2, j^0'=j^post2, y4^0'=y4^post2, y6^0'=y6^post2, y8^0'=y8^post2, (-99+i^0 <= 0 /\ -1-i^0+i^post2 == 0 /\ y4^post2-i^0 == 0 /\ y6^post2-i^0 == 0 /\ y8^0-y8^post2 == 0 /\ -j^post2+j^0 == 0), cost: 1 5: l1 -> l3 : i^0'=i^post6, j^0'=j^post6, y4^0'=y4^post6, y6^0'=y6^post6, y8^0'=y8^post6, (i^0-i^post6 == 0 /\ -j^post6+j^0 == 0 /\ -y8^post6+y8^0 == 0 /\ -y4^post6+y4^0 == 0 /\ y6^0-y6^post6 == 0), cost: 1 2: l2 -> l0 : i^0'=i^post3, j^0'=j^post3, y4^0'=y4^post3, y6^0'=y6^post3, y8^0'=y8^post3, (-i^post3+i^0 == 0 /\ j^0-j^post3 == 0 /\ -y6^post3+y6^0 == 0 /\ -y8^post3+y8^0 == 0 /\ y4^0-y4^post3 == 0), cost: 1 3: l3 -> l4 : i^0'=i^post4, j^0'=j^post4, y4^0'=y4^post4, y6^0'=y6^post4, y8^0'=y8^post4, (-j^post4+j^0 == 0 /\ i^0-i^post4 == 0 /\ 200-j^0 <= 0 /\ -y4^post4+y4^0 == 0 /\ y8^0-y8^post4 == 0 /\ y6^0-y6^post4 == 0), cost: 1 4: l3 -> l1 : i^0'=i^post5, j^0'=j^post5, y4^0'=y4^post5, y6^0'=y6^post5, y8^0'=y8^post5, (-j^0+y8^post5 == 0 /\ -1-j^0+j^post5 == 0 /\ -199+j^0 <= 0 /\ -i^post5+i^0 == 0 /\ y4^0-y4^post5 == 0 /\ -y6^post5+y6^0 == 0), cost: 1 8: l6 -> l2 : i^0'=i^post7, j^0'=j^post7, y4^0'=y4^post7, y6^0'=y6^post7, y8^0'=y8^post7, (j^post8-j^post7 == 0 /\ i^0-i^post8 == 0 /\ y4^0-y4^post8 == 0 /\ i^post7 == 0 /\ -y8^post8+y8^0 == 0 /\ y6^0-y6^post8 == 0 /\ y8^post8-y8^post7 == 0 /\ -y6^post7+y6^post8 == 0 /\ -j^post8+j^0 == 0 /\ y4^post8-y4^post7 == 0), cost: 1 Eliminating location l5 by chaining: Applied chaining First rule: l6 -> l5 : i^0'=i^post8, j^0'=j^post8, y4^0'=y4^post8, y6^0'=y6^post8, y8^0'=y8^post8, (i^0-i^post8 == 0 /\ y4^0-y4^post8 == 0 /\ -y8^post8+y8^0 == 0 /\ y6^0-y6^post8 == 0 /\ -j^post8+j^0 == 0), cost: 1 Second rule: l5 -> l2 : i^0'=i^post7, j^0'=j^post7, y4^0'=y4^post7, y6^0'=y6^post7, y8^0'=y8^post7, (y6^0-y6^post7 == 0 /\ -y8^post7+y8^0 == 0 /\ i^post7 == 0 /\ j^0-j^post7 == 0 /\ y4^0-y4^post7 == 0), cost: 1 New rule: l6 -> l2 : i^0'=i^post7, j^0'=j^post7, y4^0'=y4^post7, y6^0'=y6^post7, y8^0'=y8^post7, (j^post8-j^post7 == 0 /\ i^0-i^post8 == 0 /\ y4^0-y4^post8 == 0 /\ i^post7 == 0 /\ -y8^post8+y8^0 == 0 /\ y6^0-y6^post8 == 0 /\ y8^post8-y8^post7 == 0 /\ -y6^post7+y6^post8 == 0 /\ -j^post8+j^0 == 0 /\ y4^post8-y4^post7 == 0), cost: 1 Applied deletion Removed the following rules: 6 7 Simplified Transitions Start location: l6 Program variables: i^0 j^0 y4^0 y6^0 y8^0 9: l0 -> l1 : j^0'=100, 100-i^0 <= 0, cost: 1 10: l0 -> l2 : i^0'=1+i^0, y4^0'=i^0, y6^0'=i^0, -99+i^0 <= 0, cost: 1 14: l1 -> l3 : T, cost: 1 11: l2 -> l0 : T, cost: 1 12: l3 -> l4 : 200-j^0 <= 0, cost: 1 13: l3 -> l1 : j^0'=1+j^0, y8^0'=j^0, -199+j^0 <= 0, cost: 1 15: l6 -> l2 : i^0'=0, T, cost: 1 Propagated Equalities Original rule: l0 -> l1 : i^0'=i^post1, j^0'=j^post1, y4^0'=y4^post1, y6^0'=y6^post1, y8^0'=y8^post1, (-y8^post1+y8^0 == 0 /\ -y6^post1+y6^0 == 0 /\ -i^post1+i^0 == 0 /\ 100-i^0 <= 0 /\ y4^0-y4^post1 == 0 /\ -100+j^post1 == 0), cost: 1 New rule: l0 -> l1 : i^0'=i^0, j^0'=100, y4^0'=y4^0, y6^0'=y6^0, y8^0'=y8^0, (0 == 0 /\ 100-i^0 <= 0), cost: 1 propagated equality y8^post1 = y8^0 propagated equality y6^post1 = y6^0 propagated equality i^post1 = i^0 propagated equality y4^post1 = y4^0 propagated equality j^post1 = 100 Simplified Guard Original rule: l0 -> l1 : i^0'=i^0, j^0'=100, y4^0'=y4^0, y6^0'=y6^0, y8^0'=y8^0, (0 == 0 /\ 100-i^0 <= 0), cost: 1 New rule: l0 -> l1 : i^0'=i^0, j^0'=100, y4^0'=y4^0, y6^0'=y6^0, y8^0'=y8^0, 100-i^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l0 -> l1 : i^0'=i^0, j^0'=100, y4^0'=y4^0, y6^0'=y6^0, y8^0'=y8^0, 100-i^0 <= 0, cost: 1 New rule: l0 -> l1 : j^0'=100, 100-i^0 <= 0, cost: 1 Propagated Equalities Original rule: l0 -> l2 : i^0'=i^post2, j^0'=j^post2, y4^0'=y4^post2, y6^0'=y6^post2, y8^0'=y8^post2, (-99+i^0 <= 0 /\ -1-i^0+i^post2 == 0 /\ y4^post2-i^0 == 0 /\ y6^post2-i^0 == 0 /\ y8^0-y8^post2 == 0 /\ -j^post2+j^0 == 0), cost: 1 New rule: l0 -> l2 : i^0'=1+i^0, j^0'=j^0, y4^0'=i^0, y6^0'=i^0, y8^0'=y8^0, (0 == 0 /\ -99+i^0 <= 0), cost: 1 propagated equality i^post2 = 1+i^0 propagated equality y4^post2 = i^0 propagated equality y6^post2 = i^0 propagated equality y8^post2 = y8^0 propagated equality j^post2 = j^0 Simplified Guard Original rule: l0 -> l2 : i^0'=1+i^0, j^0'=j^0, y4^0'=i^0, y6^0'=i^0, y8^0'=y8^0, (0 == 0 /\ -99+i^0 <= 0), cost: 1 New rule: l0 -> l2 : i^0'=1+i^0, j^0'=j^0, y4^0'=i^0, y6^0'=i^0, y8^0'=y8^0, -99+i^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l0 -> l2 : i^0'=1+i^0, j^0'=j^0, y4^0'=i^0, y6^0'=i^0, y8^0'=y8^0, -99+i^0 <= 0, cost: 1 New rule: l0 -> l2 : i^0'=1+i^0, y4^0'=i^0, y6^0'=i^0, -99+i^0 <= 0, cost: 1 Propagated Equalities Original rule: l2 -> l0 : i^0'=i^post3, j^0'=j^post3, y4^0'=y4^post3, y6^0'=y6^post3, y8^0'=y8^post3, (-i^post3+i^0 == 0 /\ j^0-j^post3 == 0 /\ -y6^post3+y6^0 == 0 /\ -y8^post3+y8^0 == 0 /\ y4^0-y4^post3 == 0), cost: 1 New rule: l2 -> l0 : i^0'=i^0, j^0'=j^0, y4^0'=y4^0, y6^0'=y6^0, y8^0'=y8^0, 0 == 0, cost: 1 propagated equality i^post3 = i^0 propagated equality j^post3 = j^0 propagated equality y6^post3 = y6^0 propagated equality y8^post3 = y8^0 propagated equality y4^post3 = y4^0 Simplified Guard Original rule: l2 -> l0 : i^0'=i^0, j^0'=j^0, y4^0'=y4^0, y6^0'=y6^0, y8^0'=y8^0, 0 == 0, cost: 1 New rule: l2 -> l0 : i^0'=i^0, j^0'=j^0, y4^0'=y4^0, y6^0'=y6^0, y8^0'=y8^0, T, cost: 1 Removed Trivial Updates Original rule: l2 -> l0 : i^0'=i^0, j^0'=j^0, y4^0'=y4^0, y6^0'=y6^0, y8^0'=y8^0, T, cost: 1 New rule: l2 -> l0 : T, cost: 1 Propagated Equalities Original rule: l3 -> l4 : i^0'=i^post4, j^0'=j^post4, y4^0'=y4^post4, y6^0'=y6^post4, y8^0'=y8^post4, (-j^post4+j^0 == 0 /\ i^0-i^post4 == 0 /\ 200-j^0 <= 0 /\ -y4^post4+y4^0 == 0 /\ y8^0-y8^post4 == 0 /\ y6^0-y6^post4 == 0), cost: 1 New rule: l3 -> l4 : i^0'=i^0, j^0'=j^0, y4^0'=y4^0, y6^0'=y6^0, y8^0'=y8^0, (0 == 0 /\ 200-j^0 <= 0), cost: 1 propagated equality j^post4 = j^0 propagated equality i^post4 = i^0 propagated equality y4^post4 = y4^0 propagated equality y8^post4 = y8^0 propagated equality y6^post4 = y6^0 Simplified Guard Original rule: l3 -> l4 : i^0'=i^0, j^0'=j^0, y4^0'=y4^0, y6^0'=y6^0, y8^0'=y8^0, (0 == 0 /\ 200-j^0 <= 0), cost: 1 New rule: l3 -> l4 : i^0'=i^0, j^0'=j^0, y4^0'=y4^0, y6^0'=y6^0, y8^0'=y8^0, 200-j^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l3 -> l4 : i^0'=i^0, j^0'=j^0, y4^0'=y4^0, y6^0'=y6^0, y8^0'=y8^0, 200-j^0 <= 0, cost: 1 New rule: l3 -> l4 : 200-j^0 <= 0, cost: 1 Propagated Equalities Original rule: l3 -> l1 : i^0'=i^post5, j^0'=j^post5, y4^0'=y4^post5, y6^0'=y6^post5, y8^0'=y8^post5, (-j^0+y8^post5 == 0 /\ -1-j^0+j^post5 == 0 /\ -199+j^0 <= 0 /\ -i^post5+i^0 == 0 /\ y4^0-y4^post5 == 0 /\ -y6^post5+y6^0 == 0), cost: 1 New rule: l3 -> l1 : i^0'=i^0, j^0'=1+j^0, y4^0'=y4^0, y6^0'=y6^0, y8^0'=j^0, (0 == 0 /\ -199+j^0 <= 0), cost: 1 propagated equality y8^post5 = j^0 propagated equality j^post5 = 1+j^0 propagated equality i^post5 = i^0 propagated equality y4^post5 = y4^0 propagated equality y6^post5 = y6^0 Simplified Guard Original rule: l3 -> l1 : i^0'=i^0, j^0'=1+j^0, y4^0'=y4^0, y6^0'=y6^0, y8^0'=j^0, (0 == 0 /\ -199+j^0 <= 0), cost: 1 New rule: l3 -> l1 : i^0'=i^0, j^0'=1+j^0, y4^0'=y4^0, y6^0'=y6^0, y8^0'=j^0, -199+j^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l3 -> l1 : i^0'=i^0, j^0'=1+j^0, y4^0'=y4^0, y6^0'=y6^0, y8^0'=j^0, -199+j^0 <= 0, cost: 1 New rule: l3 -> l1 : j^0'=1+j^0, y8^0'=j^0, -199+j^0 <= 0, cost: 1 Propagated Equalities Original rule: l1 -> l3 : i^0'=i^post6, j^0'=j^post6, y4^0'=y4^post6, y6^0'=y6^post6, y8^0'=y8^post6, (i^0-i^post6 == 0 /\ -j^post6+j^0 == 0 /\ -y8^post6+y8^0 == 0 /\ -y4^post6+y4^0 == 0 /\ y6^0-y6^post6 == 0), cost: 1 New rule: l1 -> l3 : i^0'=i^0, j^0'=j^0, y4^0'=y4^0, y6^0'=y6^0, y8^0'=y8^0, 0 == 0, cost: 1 propagated equality i^post6 = i^0 propagated equality j^post6 = j^0 propagated equality y8^post6 = y8^0 propagated equality y4^post6 = y4^0 propagated equality y6^post6 = y6^0 Simplified Guard Original rule: l1 -> l3 : i^0'=i^0, j^0'=j^0, y4^0'=y4^0, y6^0'=y6^0, y8^0'=y8^0, 0 == 0, cost: 1 New rule: l1 -> l3 : i^0'=i^0, j^0'=j^0, y4^0'=y4^0, y6^0'=y6^0, y8^0'=y8^0, T, cost: 1 Removed Trivial Updates Original rule: l1 -> l3 : i^0'=i^0, j^0'=j^0, y4^0'=y4^0, y6^0'=y6^0, y8^0'=y8^0, T, cost: 1 New rule: l1 -> l3 : T, cost: 1 Propagated Equalities Original rule: l6 -> l2 : i^0'=i^post7, j^0'=j^post7, y4^0'=y4^post7, y6^0'=y6^post7, y8^0'=y8^post7, (j^post8-j^post7 == 0 /\ i^0-i^post8 == 0 /\ y4^0-y4^post8 == 0 /\ i^post7 == 0 /\ -y8^post8+y8^0 == 0 /\ y6^0-y6^post8 == 0 /\ y8^post8-y8^post7 == 0 /\ -y6^post7+y6^post8 == 0 /\ -j^post8+j^0 == 0 /\ y4^post8-y4^post7 == 0), cost: 1 New rule: l6 -> l2 : i^0'=0, j^0'=j^post8, y4^0'=y4^post8, y6^0'=y6^post8, y8^0'=y8^post8, (0 == 0 /\ i^0-i^post8 == 0 /\ y4^0-y4^post8 == 0 /\ -y8^post8+y8^0 == 0 /\ y6^0-y6^post8 == 0 /\ -j^post8+j^0 == 0), cost: 1 propagated equality j^post7 = j^post8 propagated equality i^post7 = 0 propagated equality y8^post7 = y8^post8 propagated equality y6^post7 = y6^post8 propagated equality y4^post7 = y4^post8 Propagated Equalities Original rule: l6 -> l2 : i^0'=0, j^0'=j^post8, y4^0'=y4^post8, y6^0'=y6^post8, y8^0'=y8^post8, (0 == 0 /\ i^0-i^post8 == 0 /\ y4^0-y4^post8 == 0 /\ -y8^post8+y8^0 == 0 /\ y6^0-y6^post8 == 0 /\ -j^post8+j^0 == 0), cost: 1 New rule: l6 -> l2 : i^0'=0, j^0'=j^0, y4^0'=y4^0, y6^0'=y6^0, y8^0'=y8^0, 0 == 0, cost: 1 propagated equality i^post8 = i^0 propagated equality y4^post8 = y4^0 propagated equality y8^post8 = y8^0 propagated equality y6^post8 = y6^0 propagated equality j^post8 = j^0 Simplified Guard Original rule: l6 -> l2 : i^0'=0, j^0'=j^0, y4^0'=y4^0, y6^0'=y6^0, y8^0'=y8^0, 0 == 0, cost: 1 New rule: l6 -> l2 : i^0'=0, j^0'=j^0, y4^0'=y4^0, y6^0'=y6^0, y8^0'=y8^0, T, cost: 1 Removed Trivial Updates Original rule: l6 -> l2 : i^0'=0, j^0'=j^0, y4^0'=y4^0, y6^0'=y6^0, y8^0'=y8^0, T, cost: 1 New rule: l6 -> l2 : i^0'=0, T, cost: 1 Step with 15 Trace 15[T] Blocked [{}, {}] Step with 11 Trace 15[T], 11[T] Blocked [{}, {}, {}] Step with 10 Trace 15[T], 11[T], 10[(-99+i^0 <= 0)] Blocked [{}, {}, {9[T]}, {}] Accelerate Start location: l6 Program variables: i^0 j^0 y4^0 y6^0 y8^0 9: l0 -> l1 : j^0'=100, 100-i^0 <= 0, cost: 1 10: l0 -> l2 : i^0'=1+i^0, y4^0'=i^0, y6^0'=i^0, -99+i^0 <= 0, cost: 1 14: l1 -> l3 : T, cost: 1 11: l2 -> l0 : T, cost: 1 16: l2 -> l2 : i^0'=i^0+n, y4^0'=-1+i^0+n, y6^0'=-1+i^0+n, (100-i^0-n >= 0 /\ -1+n >= 0), cost: 1 12: l3 -> l4 : 200-j^0 <= 0, cost: 1 13: l3 -> l1 : j^0'=1+j^0, y8^0'=j^0, -199+j^0 <= 0, cost: 1 15: l6 -> l2 : i^0'=0, T, cost: 1 Loop Acceleration Original rule: l2 -> l2 : i^0'=1+i^0, y4^0'=i^0, y6^0'=i^0, -99+i^0 <= 0, cost: 1 New rule: l2 -> l2 : i^0'=i^0+n, y4^0'=-1+i^0+n, y6^0'=-1+i^0+n, (100-i^0-n >= 0 /\ -1+n >= 0), cost: 1 99-i^0 >= 0 [0]: montonic decrease yields 100-i^0-n >= 0 99-i^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ 99-i^0 >= 0) Replacement map: {99-i^0 >= 0 -> 100-i^0-n >= 0} Trace 15[T], 16[(100-i^0-n >= 0 /\ -1+n >= 0)] Blocked [{}, {}, {16[T]}] Step with 11 Trace 15[T], 16[(100-i^0-n >= 0 /\ -1+n >= 0)], 11[T] Blocked [{}, {}, {16[T]}, {}] Step with 10 Trace 15[T], 16[(100-i^0-n >= 0 /\ -1+n >= 0)], 11[T], 10[(-99+i^0 <= 0)] Blocked [{}, {}, {16[T]}, {}, {}] Covered Trace 15[T], 16[(100-i^0-n >= 0 /\ -1+n >= 0)], 11[T] Blocked [{}, {}, {16[T]}, {10[T]}] Step with 9 Trace 15[T], 16[(100-i^0-n >= 0 /\ -1+n >= 0)], 11[T], 9[(100-i^0 <= 0)] Blocked [{}, {}, {16[T]}, {10[T]}, {}] Step with 14 Trace 15[T], 16[(100-i^0-n >= 0 /\ -1+n >= 0)], 11[T], 9[(100-i^0 <= 0)], 14[T] Blocked [{}, {}, {16[T]}, {10[T]}, {}, {}] Step with 13 Trace 15[T], 16[(100-i^0-n >= 0 /\ -1+n >= 0)], 11[T], 9[(100-i^0 <= 0)], 14[T], 13[(-199+j^0 <= 0)] Blocked [{}, {}, {16[T]}, {10[T]}, {}, {12[T]}, {}] Accelerate Start location: l6 Program variables: i^0 j^0 y4^0 y6^0 y8^0 9: l0 -> l1 : j^0'=100, 100-i^0 <= 0, cost: 1 10: l0 -> l2 : i^0'=1+i^0, y4^0'=i^0, y6^0'=i^0, -99+i^0 <= 0, cost: 1 14: l1 -> l3 : T, cost: 1 17: l1 -> l1 : j^0'=j^0+n2, y8^0'=-1+j^0+n2, (200-j^0-n2 >= 0 /\ -1+n2 >= 0), cost: 1 11: l2 -> l0 : T, cost: 1 16: l2 -> l2 : i^0'=i^0+n, y4^0'=-1+i^0+n, y6^0'=-1+i^0+n, (100-i^0-n >= 0 /\ -1+n >= 0), cost: 1 12: l3 -> l4 : 200-j^0 <= 0, cost: 1 13: l3 -> l1 : j^0'=1+j^0, y8^0'=j^0, -199+j^0 <= 0, cost: 1 15: l6 -> l2 : i^0'=0, T, cost: 1 Loop Acceleration Original rule: l1 -> l1 : j^0'=1+j^0, y8^0'=j^0, -199+j^0 <= 0, cost: 1 New rule: l1 -> l1 : j^0'=j^0+n2, y8^0'=-1+j^0+n2, (200-j^0-n2 >= 0 /\ -1+n2 >= 0), cost: 1 199-j^0 >= 0 [0]: montonic decrease yields 200-j^0-n2 >= 0 199-j^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ 199-j^0 >= 0) Replacement map: {199-j^0 >= 0 -> 200-j^0-n2 >= 0} Trace 15[T], 16[(100-i^0-n >= 0 /\ -1+n >= 0)], 11[T], 9[(100-i^0 <= 0)], 17[(200-j^0-n2 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {}, {16[T]}, {10[T]}, {}, {17[T]}] Step with 14 Trace 15[T], 16[(100-i^0-n >= 0 /\ -1+n >= 0)], 11[T], 9[(100-i^0 <= 0)], 17[(200-j^0-n2 >= 0 /\ -1+n2 >= 0)], 14[T] Blocked [{}, {}, {16[T]}, {10[T]}, {}, {17[T]}, {}] Step with 13 Trace 15[T], 16[(100-i^0-n >= 0 /\ -1+n >= 0)], 11[T], 9[(100-i^0 <= 0)], 17[(200-j^0-n2 >= 0 /\ -1+n2 >= 0)], 14[T], 13[(-199+j^0 <= 0)] Blocked [{}, {}, {16[T]}, {10[T]}, {}, {17[T]}, {}, {}] Covered Trace 15[T], 16[(100-i^0-n >= 0 /\ -1+n >= 0)], 11[T], 9[(100-i^0 <= 0)], 17[(200-j^0-n2 >= 0 /\ -1+n2 >= 0)], 14[T] Blocked [{}, {}, {16[T]}, {10[T]}, {}, {17[T]}, {13[T]}] Step with 12 Trace 15[T], 16[(100-i^0-n >= 0 /\ -1+n >= 0)], 11[T], 9[(100-i^0 <= 0)], 17[(200-j^0-n2 >= 0 /\ -1+n2 >= 0)], 14[T], 12[(200-j^0 <= 0)] Blocked [{}, {}, {16[T]}, {10[T]}, {}, {17[T]}, {13[T]}, {}] Backtrack Trace 15[T], 16[(100-i^0-n >= 0 /\ -1+n >= 0)], 11[T], 9[(100-i^0 <= 0)], 17[(200-j^0-n2 >= 0 /\ -1+n2 >= 0)], 14[T] Blocked [{}, {}, {16[T]}, {10[T]}, {}, {17[T]}, {12[T], 13[T]}] Backtrack Trace 15[T], 16[(100-i^0-n >= 0 /\ -1+n >= 0)], 11[T], 9[(100-i^0 <= 0)], 17[(200-j^0-n2 >= 0 /\ -1+n2 >= 0)] Blocked [{}, {}, {16[T]}, {10[T]}, {}, {14[T], 17[T]}] Backtrack Trace 15[T], 16[(100-i^0-n >= 0 /\ -1+n >= 0)], 11[T], 9[(100-i^0 <= 0)] Blocked [{}, {}, {16[T]}, {10[T]}, {17[T]}] Step with 14 Trace 15[T], 16[(100-i^0-n >= 0 /\ -1+n >= 0)], 11[T], 9[(100-i^0 <= 0)], 14[T] Blocked [{}, {}, {16[T]}, {10[T]}, {17[T]}, {}] Step with 13 Trace 15[T], 16[(100-i^0-n >= 0 /\ -1+n >= 0)], 11[T], 9[(100-i^0 <= 0)], 14[T], 13[(-199+j^0 <= 0)] Blocked [{}, {}, {16[T]}, {10[T]}, {17[T]}, {12[T]}, {}] Covered Trace 15[T], 16[(100-i^0-n >= 0 /\ -1+n >= 0)], 11[T], 9[(100-i^0 <= 0)], 14[T] Blocked [{}, {}, {16[T]}, {10[T]}, {17[T]}, {12[T], 13[T]}] Backtrack Trace 15[T], 16[(100-i^0-n >= 0 /\ -1+n >= 0)], 11[T], 9[(100-i^0 <= 0)] Blocked [{}, {}, {16[T]}, {10[T]}, {14[T], 17[T]}] Backtrack Trace 15[T], 16[(100-i^0-n >= 0 /\ -1+n >= 0)], 11[T] Blocked [{}, {}, {16[T]}, {9[T], 10[T]}] Backtrack Trace 15[T], 16[(100-i^0-n >= 0 /\ -1+n >= 0)] Blocked [{}, {}, {11[T], 16[T]}] Backtrack Trace 15[T] Blocked [{}, {16[T]}] Step with 11 Trace 15[T], 11[T] Blocked [{}, {16[T]}, {}] Step with 10 Trace 15[T], 11[T], 10[(-99+i^0 <= 0)] Blocked [{}, {16[T]}, {9[T]}, {}] Covered Trace 15[T], 11[T] Blocked [{}, {16[T]}, {9[T], 10[T]}] Backtrack Trace 15[T] Blocked [{}, {11[T], 16[T]}] Backtrack Trace Blocked [{15[T]}] Accept unknown Build SHA: a05f16bf13df659c382799650051f91bf6828c7b