NO Initial ITS Start location: l9 Program variables: ___rho_1_^0 ___rho_2_^0 a^0 dobreak^0 n^0 r^0 0: l0 -> l1 : ___rho_1_^0'=___rho_1_^post1, ___rho_2_^0'=___rho_2_^post1, a^0'=a^post1, dobreak^0'=dobreak^post1, n^0'=n^post1, r^0'=r^post1, (-___rho_2_^post1+___rho_2_^0 == 0 /\ dobreak^0-dobreak^post1 == 0 /\ -n^post1+n^0 == 0 /\ -___rho_1_^post1+___rho_1_^0 == 0 /\ -a^post1+a^0 == 0 /\ r^0-r^post1 == 0), cost: 1 7: l1 -> l2 : ___rho_1_^0'=___rho_1_^post8, ___rho_2_^0'=___rho_2_^post8, a^0'=a^post8, dobreak^0'=dobreak^post8, n^0'=n^post8, r^0'=r^post8, (0 == 0 /\ a^post8 == 0 /\ -___rho_2_^post8+n^post8 == 0 /\ -1+a^1 == 0 /\ dobreak^0 <= 0 /\ dobreak^0-dobreak^post8 == 0 /\ -___rho_1_^post8+___rho_1_^0 == 0 /\ -r^post8+r^0 == 0), cost: 1 8: l1 -> l6 : ___rho_1_^0'=___rho_1_^post9, ___rho_2_^0'=___rho_2_^post9, a^0'=a^post9, dobreak^0'=dobreak^post9, n^0'=n^post9, r^0'=r^post9, (-r^post9+r^0 == 0 /\ 1-dobreak^0 <= 0 /\ -___rho_1_^post9+___rho_1_^0 == 0 /\ -a^post9+a^0 == 0 /\ ___rho_2_^0-___rho_2_^post9 == 0 /\ n^0-n^post9 == 0 /\ dobreak^0-dobreak^post9 == 0), cost: 1 1: l2 -> l3 : ___rho_1_^0'=___rho_1_^post2, ___rho_2_^0'=___rho_2_^post2, a^0'=a^post2, dobreak^0'=dobreak^post2, n^0'=n^post2, r^0'=r^post2, (-a^post2+a^0 == 0 /\ -___rho_1_^post2+___rho_1_^0 == 0 /\ -r^post2+r^0 == 0 /\ ___rho_2_^0-___rho_2_^post2 == 0 /\ n^0-n^post2 == 0 /\ dobreak^0-dobreak^post2 == 0), cost: 1 5: l3 -> l2 : ___rho_1_^0'=___rho_1_^post6, ___rho_2_^0'=___rho_2_^post6, a^0'=a^post6, dobreak^0'=dobreak^post6, n^0'=n^post6, r^0'=r^post6, (dobreak^0-dobreak^post6 == 0 /\ ___rho_1_^0-___rho_1_^post6 == 0 /\ -___rho_2_^post6+___rho_2_^0 == 0 /\ r^0-r^post6 == 0 /\ 1-n^0 <= 0 /\ -n^post6+n^0 == 0 /\ a^0-a^post6 == 0), cost: 1 6: l3 -> l0 : ___rho_1_^0'=___rho_1_^post7, ___rho_2_^0'=___rho_2_^post7, a^0'=a^post7, dobreak^0'=dobreak^post7, n^0'=n^post7, r^0'=r^post7, (0 == 0 /\ -n^post7+n^0 == 0 /\ ___rho_2_^0-___rho_2_^post7 == 0 /\ a^0-a^post7 == 0 /\ dobreak^post7-___rho_1_^post7 == 0 /\ n^0 <= 0 /\ r^post7 == 0 /\ -1+r^1 == 0), cost: 1 2: l4 -> l5 : ___rho_1_^0'=___rho_1_^post3, ___rho_2_^0'=___rho_2_^post3, a^0'=a^post3, dobreak^0'=dobreak^post3, n^0'=n^post3, r^0'=r^post3, (-n^post3+n^0 == 0 /\ dobreak^0-dobreak^post3 == 0 /\ r^0-r^post3 == 0 /\ ___rho_2_^0-___rho_2_^post3 == 0 /\ -a^post3+a^0 == 0 /\ -___rho_1_^post3+___rho_1_^0 == 0), cost: 1 3: l6 -> l7 : ___rho_1_^0'=___rho_1_^post4, ___rho_2_^0'=___rho_2_^post4, a^0'=a^post4, dobreak^0'=dobreak^post4, n^0'=n^post4, r^0'=r^post4, (-n^post4+n^0 == 0 /\ ___rho_2_^0-___rho_2_^post4 == 0 /\ a^0-a^post4 == 0 /\ dobreak^0-dobreak^post4 == 0 /\ r^0-r^post4 == 0 /\ -___rho_1_^post4+___rho_1_^0 == 0), cost: 1 4: l7 -> l6 : ___rho_1_^0'=___rho_1_^post5, ___rho_2_^0'=___rho_2_^post5, a^0'=a^post5, dobreak^0'=dobreak^post5, n^0'=n^post5, r^0'=r^post5, (r^0-r^post5 == 0 /\ -dobreak^post5+dobreak^0 == 0 /\ -___rho_2_^post5+___rho_2_^0 == 0 /\ -___rho_1_^post5+___rho_1_^0 == 0 /\ a^0-a^post5 == 0 /\ -n^post5+n^0 == 0), cost: 1 9: l8 -> l0 : ___rho_1_^0'=___rho_1_^post10, ___rho_2_^0'=___rho_2_^post10, a^0'=a^post10, dobreak^0'=dobreak^post10, n^0'=n^post10, r^0'=r^post10, (0 == 0 /\ ___rho_2_^0-___rho_2_^post10 == 0 /\ a^post10 == 0 /\ -n^post10+n^0 == 0 /\ dobreak^post10-___rho_1_^post10 == 0 /\ r^post10 == 0), cost: 1 10: l9 -> l8 : ___rho_1_^0'=___rho_1_^post11, ___rho_2_^0'=___rho_2_^post11, a^0'=a^post11, dobreak^0'=dobreak^post11, n^0'=n^post11, r^0'=r^post11, (-n^post11+n^0 == 0 /\ ___rho_2_^0-___rho_2_^post11 == 0 /\ dobreak^0-dobreak^post11 == 0 /\ -a^post11+a^0 == 0 /\ r^0-r^post11 == 0 /\ -___rho_1_^post11+___rho_1_^0 == 0), cost: 1 Chained Linear Paths Start location: l9 Program variables: ___rho_1_^0 ___rho_2_^0 a^0 dobreak^0 n^0 r^0 0: l0 -> l1 : ___rho_1_^0'=___rho_1_^post1, ___rho_2_^0'=___rho_2_^post1, a^0'=a^post1, dobreak^0'=dobreak^post1, n^0'=n^post1, r^0'=r^post1, (-___rho_2_^post1+___rho_2_^0 == 0 /\ dobreak^0-dobreak^post1 == 0 /\ -n^post1+n^0 == 0 /\ -___rho_1_^post1+___rho_1_^0 == 0 /\ -a^post1+a^0 == 0 /\ r^0-r^post1 == 0), cost: 1 7: l1 -> l2 : ___rho_1_^0'=___rho_1_^post8, ___rho_2_^0'=___rho_2_^post8, a^0'=a^post8, dobreak^0'=dobreak^post8, n^0'=n^post8, r^0'=r^post8, (0 == 0 /\ a^post8 == 0 /\ -___rho_2_^post8+n^post8 == 0 /\ -1+a^1 == 0 /\ dobreak^0 <= 0 /\ dobreak^0-dobreak^post8 == 0 /\ -___rho_1_^post8+___rho_1_^0 == 0 /\ -r^post8+r^0 == 0), cost: 1 8: l1 -> l6 : ___rho_1_^0'=___rho_1_^post9, ___rho_2_^0'=___rho_2_^post9, a^0'=a^post9, dobreak^0'=dobreak^post9, n^0'=n^post9, r^0'=r^post9, (-r^post9+r^0 == 0 /\ 1-dobreak^0 <= 0 /\ -___rho_1_^post9+___rho_1_^0 == 0 /\ -a^post9+a^0 == 0 /\ ___rho_2_^0-___rho_2_^post9 == 0 /\ n^0-n^post9 == 0 /\ dobreak^0-dobreak^post9 == 0), cost: 1 1: l2 -> l3 : ___rho_1_^0'=___rho_1_^post2, ___rho_2_^0'=___rho_2_^post2, a^0'=a^post2, dobreak^0'=dobreak^post2, n^0'=n^post2, r^0'=r^post2, (-a^post2+a^0 == 0 /\ -___rho_1_^post2+___rho_1_^0 == 0 /\ -r^post2+r^0 == 0 /\ ___rho_2_^0-___rho_2_^post2 == 0 /\ n^0-n^post2 == 0 /\ dobreak^0-dobreak^post2 == 0), cost: 1 5: l3 -> l2 : ___rho_1_^0'=___rho_1_^post6, ___rho_2_^0'=___rho_2_^post6, a^0'=a^post6, dobreak^0'=dobreak^post6, n^0'=n^post6, r^0'=r^post6, (dobreak^0-dobreak^post6 == 0 /\ ___rho_1_^0-___rho_1_^post6 == 0 /\ -___rho_2_^post6+___rho_2_^0 == 0 /\ r^0-r^post6 == 0 /\ 1-n^0 <= 0 /\ -n^post6+n^0 == 0 /\ a^0-a^post6 == 0), cost: 1 6: l3 -> l0 : ___rho_1_^0'=___rho_1_^post7, ___rho_2_^0'=___rho_2_^post7, a^0'=a^post7, dobreak^0'=dobreak^post7, n^0'=n^post7, r^0'=r^post7, (0 == 0 /\ -n^post7+n^0 == 0 /\ ___rho_2_^0-___rho_2_^post7 == 0 /\ a^0-a^post7 == 0 /\ dobreak^post7-___rho_1_^post7 == 0 /\ n^0 <= 0 /\ r^post7 == 0 /\ -1+r^1 == 0), cost: 1 2: l4 -> l5 : ___rho_1_^0'=___rho_1_^post3, ___rho_2_^0'=___rho_2_^post3, a^0'=a^post3, dobreak^0'=dobreak^post3, n^0'=n^post3, r^0'=r^post3, (-n^post3+n^0 == 0 /\ dobreak^0-dobreak^post3 == 0 /\ r^0-r^post3 == 0 /\ ___rho_2_^0-___rho_2_^post3 == 0 /\ -a^post3+a^0 == 0 /\ -___rho_1_^post3+___rho_1_^0 == 0), cost: 1 12: l6 -> l6 : ___rho_1_^0'=___rho_1_^post5, ___rho_2_^0'=___rho_2_^post5, a^0'=a^post5, dobreak^0'=dobreak^post5, n^0'=n^post5, r^0'=r^post5, (-r^post5+r^post4 == 0 /\ -n^post4+n^0 == 0 /\ -dobreak^post5+dobreak^post4 == 0 /\ ___rho_2_^0-___rho_2_^post4 == 0 /\ a^0-a^post4 == 0 /\ -a^post5+a^post4 == 0 /\ -n^post5+n^post4 == 0 /\ -___rho_2_^post5+___rho_2_^post4 == 0 /\ dobreak^0-dobreak^post4 == 0 /\ -___rho_1_^post5+___rho_1_^post4 == 0 /\ r^0-r^post4 == 0 /\ -___rho_1_^post4+___rho_1_^0 == 0), cost: 1 11: l9 -> l0 : ___rho_1_^0'=___rho_1_^post10, ___rho_2_^0'=___rho_2_^post10, a^0'=a^post10, dobreak^0'=dobreak^post10, n^0'=n^post10, r^0'=r^post10, (0 == 0 /\ a^post10 == 0 /\ -n^post11+n^0 == 0 /\ ___rho_2_^0-___rho_2_^post11 == 0 /\ dobreak^0-dobreak^post11 == 0 /\ -a^post11+a^0 == 0 /\ ___rho_2_^post11-___rho_2_^post10 == 0 /\ r^0-r^post11 == 0 /\ n^post11-n^post10 == 0 /\ -___rho_1_^post11+___rho_1_^0 == 0 /\ dobreak^post10-___rho_1_^post10 == 0 /\ r^post10 == 0), cost: 1 Eliminating location l8 by chaining: Applied chaining First rule: l9 -> l8 : ___rho_1_^0'=___rho_1_^post11, ___rho_2_^0'=___rho_2_^post11, a^0'=a^post11, dobreak^0'=dobreak^post11, n^0'=n^post11, r^0'=r^post11, (-n^post11+n^0 == 0 /\ ___rho_2_^0-___rho_2_^post11 == 0 /\ dobreak^0-dobreak^post11 == 0 /\ -a^post11+a^0 == 0 /\ r^0-r^post11 == 0 /\ -___rho_1_^post11+___rho_1_^0 == 0), cost: 1 Second rule: l8 -> l0 : ___rho_1_^0'=___rho_1_^post10, ___rho_2_^0'=___rho_2_^post10, a^0'=a^post10, dobreak^0'=dobreak^post10, n^0'=n^post10, r^0'=r^post10, (0 == 0 /\ ___rho_2_^0-___rho_2_^post10 == 0 /\ a^post10 == 0 /\ -n^post10+n^0 == 0 /\ dobreak^post10-___rho_1_^post10 == 0 /\ r^post10 == 0), cost: 1 New rule: l9 -> l0 : ___rho_1_^0'=___rho_1_^post10, ___rho_2_^0'=___rho_2_^post10, a^0'=a^post10, dobreak^0'=dobreak^post10, n^0'=n^post10, r^0'=r^post10, (0 == 0 /\ a^post10 == 0 /\ -n^post11+n^0 == 0 /\ ___rho_2_^0-___rho_2_^post11 == 0 /\ dobreak^0-dobreak^post11 == 0 /\ -a^post11+a^0 == 0 /\ ___rho_2_^post11-___rho_2_^post10 == 0 /\ r^0-r^post11 == 0 /\ n^post11-n^post10 == 0 /\ -___rho_1_^post11+___rho_1_^0 == 0 /\ dobreak^post10-___rho_1_^post10 == 0 /\ r^post10 == 0), cost: 1 Applied deletion Removed the following rules: 9 10 Eliminating location l7 by chaining: Applied chaining First rule: l6 -> l7 : ___rho_1_^0'=___rho_1_^post4, ___rho_2_^0'=___rho_2_^post4, a^0'=a^post4, dobreak^0'=dobreak^post4, n^0'=n^post4, r^0'=r^post4, (-n^post4+n^0 == 0 /\ ___rho_2_^0-___rho_2_^post4 == 0 /\ a^0-a^post4 == 0 /\ dobreak^0-dobreak^post4 == 0 /\ r^0-r^post4 == 0 /\ -___rho_1_^post4+___rho_1_^0 == 0), cost: 1 Second rule: l7 -> l6 : ___rho_1_^0'=___rho_1_^post5, ___rho_2_^0'=___rho_2_^post5, a^0'=a^post5, dobreak^0'=dobreak^post5, n^0'=n^post5, r^0'=r^post5, (r^0-r^post5 == 0 /\ -dobreak^post5+dobreak^0 == 0 /\ -___rho_2_^post5+___rho_2_^0 == 0 /\ -___rho_1_^post5+___rho_1_^0 == 0 /\ a^0-a^post5 == 0 /\ -n^post5+n^0 == 0), cost: 1 New rule: l6 -> l6 : ___rho_1_^0'=___rho_1_^post5, ___rho_2_^0'=___rho_2_^post5, a^0'=a^post5, dobreak^0'=dobreak^post5, n^0'=n^post5, r^0'=r^post5, (-r^post5+r^post4 == 0 /\ -n^post4+n^0 == 0 /\ -dobreak^post5+dobreak^post4 == 0 /\ ___rho_2_^0-___rho_2_^post4 == 0 /\ a^0-a^post4 == 0 /\ -a^post5+a^post4 == 0 /\ -n^post5+n^post4 == 0 /\ -___rho_2_^post5+___rho_2_^post4 == 0 /\ dobreak^0-dobreak^post4 == 0 /\ -___rho_1_^post5+___rho_1_^post4 == 0 /\ r^0-r^post4 == 0 /\ -___rho_1_^post4+___rho_1_^0 == 0), cost: 1 Applied deletion Removed the following rules: 3 4 Simplified Transitions Start location: l9 Program variables: ___rho_1_^0 ___rho_2_^0 a^0 dobreak^0 n^0 r^0 13: l0 -> l1 : T, cost: 1 18: l1 -> l2 : ___rho_2_^0'=n^post8, a^0'=0, n^0'=n^post8, dobreak^0 <= 0, cost: 1 19: l1 -> l6 : 1-dobreak^0 <= 0, cost: 1 14: l2 -> l3 : T, cost: 1 16: l3 -> l2 : 1-n^0 <= 0, cost: 1 17: l3 -> l0 : ___rho_1_^0'=dobreak^post7, dobreak^0'=dobreak^post7, r^0'=0, n^0 <= 0, cost: 1 15: l4 -> l5 : T, cost: 1 21: l6 -> l6 : T, cost: 1 20: l9 -> l0 : ___rho_1_^0'=dobreak^post10, a^0'=0, dobreak^0'=dobreak^post10, r^0'=0, T, cost: 1 Propagated Equalities Original rule: l0 -> l1 : ___rho_1_^0'=___rho_1_^post1, ___rho_2_^0'=___rho_2_^post1, a^0'=a^post1, dobreak^0'=dobreak^post1, n^0'=n^post1, r^0'=r^post1, (-___rho_2_^post1+___rho_2_^0 == 0 /\ dobreak^0-dobreak^post1 == 0 /\ -n^post1+n^0 == 0 /\ -___rho_1_^post1+___rho_1_^0 == 0 /\ -a^post1+a^0 == 0 /\ r^0-r^post1 == 0), cost: 1 New rule: l0 -> l1 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, a^0'=a^0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, 0 == 0, cost: 1 propagated equality ___rho_2_^post1 = ___rho_2_^0 propagated equality dobreak^post1 = dobreak^0 propagated equality n^post1 = n^0 propagated equality ___rho_1_^post1 = ___rho_1_^0 propagated equality a^post1 = a^0 propagated equality r^post1 = r^0 Simplified Guard Original rule: l0 -> l1 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, a^0'=a^0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, 0 == 0, cost: 1 New rule: l0 -> l1 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, a^0'=a^0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, T, cost: 1 Removed Trivial Updates Original rule: l0 -> l1 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, a^0'=a^0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, T, cost: 1 New rule: l0 -> l1 : T, cost: 1 Propagated Equalities Original rule: l2 -> l3 : ___rho_1_^0'=___rho_1_^post2, ___rho_2_^0'=___rho_2_^post2, a^0'=a^post2, dobreak^0'=dobreak^post2, n^0'=n^post2, r^0'=r^post2, (-a^post2+a^0 == 0 /\ -___rho_1_^post2+___rho_1_^0 == 0 /\ -r^post2+r^0 == 0 /\ ___rho_2_^0-___rho_2_^post2 == 0 /\ n^0-n^post2 == 0 /\ dobreak^0-dobreak^post2 == 0), cost: 1 New rule: l2 -> l3 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, a^0'=a^0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, 0 == 0, cost: 1 propagated equality a^post2 = a^0 propagated equality ___rho_1_^post2 = ___rho_1_^0 propagated equality r^post2 = r^0 propagated equality ___rho_2_^post2 = ___rho_2_^0 propagated equality n^post2 = n^0 propagated equality dobreak^post2 = dobreak^0 Simplified Guard Original rule: l2 -> l3 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, a^0'=a^0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, 0 == 0, cost: 1 New rule: l2 -> l3 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, a^0'=a^0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, T, cost: 1 Removed Trivial Updates Original rule: l2 -> l3 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, a^0'=a^0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, T, cost: 1 New rule: l2 -> l3 : T, cost: 1 Propagated Equalities Original rule: l4 -> l5 : ___rho_1_^0'=___rho_1_^post3, ___rho_2_^0'=___rho_2_^post3, a^0'=a^post3, dobreak^0'=dobreak^post3, n^0'=n^post3, r^0'=r^post3, (-n^post3+n^0 == 0 /\ dobreak^0-dobreak^post3 == 0 /\ r^0-r^post3 == 0 /\ ___rho_2_^0-___rho_2_^post3 == 0 /\ -a^post3+a^0 == 0 /\ -___rho_1_^post3+___rho_1_^0 == 0), cost: 1 New rule: l4 -> l5 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, a^0'=a^0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, 0 == 0, cost: 1 propagated equality n^post3 = n^0 propagated equality dobreak^post3 = dobreak^0 propagated equality r^post3 = r^0 propagated equality ___rho_2_^post3 = ___rho_2_^0 propagated equality a^post3 = a^0 propagated equality ___rho_1_^post3 = ___rho_1_^0 Simplified Guard Original rule: l4 -> l5 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, a^0'=a^0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, 0 == 0, cost: 1 New rule: l4 -> l5 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, a^0'=a^0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, T, cost: 1 Removed Trivial Updates Original rule: l4 -> l5 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, a^0'=a^0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, T, cost: 1 New rule: l4 -> l5 : T, cost: 1 Propagated Equalities Original rule: l3 -> l2 : ___rho_1_^0'=___rho_1_^post6, ___rho_2_^0'=___rho_2_^post6, a^0'=a^post6, dobreak^0'=dobreak^post6, n^0'=n^post6, r^0'=r^post6, (dobreak^0-dobreak^post6 == 0 /\ ___rho_1_^0-___rho_1_^post6 == 0 /\ -___rho_2_^post6+___rho_2_^0 == 0 /\ r^0-r^post6 == 0 /\ 1-n^0 <= 0 /\ -n^post6+n^0 == 0 /\ a^0-a^post6 == 0), cost: 1 New rule: l3 -> l2 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, a^0'=a^0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, (0 == 0 /\ 1-n^0 <= 0), cost: 1 propagated equality dobreak^post6 = dobreak^0 propagated equality ___rho_1_^post6 = ___rho_1_^0 propagated equality ___rho_2_^post6 = ___rho_2_^0 propagated equality r^post6 = r^0 propagated equality n^post6 = n^0 propagated equality a^post6 = a^0 Simplified Guard Original rule: l3 -> l2 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, a^0'=a^0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, (0 == 0 /\ 1-n^0 <= 0), cost: 1 New rule: l3 -> l2 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, a^0'=a^0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, 1-n^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l3 -> l2 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, a^0'=a^0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, 1-n^0 <= 0, cost: 1 New rule: l3 -> l2 : 1-n^0 <= 0, cost: 1 Propagated Equalities Original rule: l3 -> l0 : ___rho_1_^0'=___rho_1_^post7, ___rho_2_^0'=___rho_2_^post7, a^0'=a^post7, dobreak^0'=dobreak^post7, n^0'=n^post7, r^0'=r^post7, (0 == 0 /\ -n^post7+n^0 == 0 /\ ___rho_2_^0-___rho_2_^post7 == 0 /\ a^0-a^post7 == 0 /\ dobreak^post7-___rho_1_^post7 == 0 /\ n^0 <= 0 /\ r^post7 == 0 /\ -1+r^1 == 0), cost: 1 New rule: l3 -> l0 : ___rho_1_^0'=dobreak^post7, ___rho_2_^0'=___rho_2_^0, a^0'=a^0, dobreak^0'=dobreak^post7, n^0'=n^0, r^0'=0, (0 == 0 /\ n^0 <= 0 /\ -1+r^1 == 0), cost: 1 propagated equality n^post7 = n^0 propagated equality ___rho_2_^post7 = ___rho_2_^0 propagated equality a^post7 = a^0 propagated equality ___rho_1_^post7 = dobreak^post7 propagated equality r^post7 = 0 Propagated Equalities Original rule: l3 -> l0 : ___rho_1_^0'=dobreak^post7, ___rho_2_^0'=___rho_2_^0, a^0'=a^0, dobreak^0'=dobreak^post7, n^0'=n^0, r^0'=0, (0 == 0 /\ n^0 <= 0 /\ -1+r^1 == 0), cost: 1 New rule: l3 -> l0 : ___rho_1_^0'=dobreak^post7, ___rho_2_^0'=___rho_2_^0, a^0'=a^0, dobreak^0'=dobreak^post7, n^0'=n^0, r^0'=0, (0 == 0 /\ n^0 <= 0), cost: 1 propagated equality r^1 = 1 Simplified Guard Original rule: l3 -> l0 : ___rho_1_^0'=dobreak^post7, ___rho_2_^0'=___rho_2_^0, a^0'=a^0, dobreak^0'=dobreak^post7, n^0'=n^0, r^0'=0, (0 == 0 /\ n^0 <= 0), cost: 1 New rule: l3 -> l0 : ___rho_1_^0'=dobreak^post7, ___rho_2_^0'=___rho_2_^0, a^0'=a^0, dobreak^0'=dobreak^post7, n^0'=n^0, r^0'=0, n^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l3 -> l0 : ___rho_1_^0'=dobreak^post7, ___rho_2_^0'=___rho_2_^0, a^0'=a^0, dobreak^0'=dobreak^post7, n^0'=n^0, r^0'=0, n^0 <= 0, cost: 1 New rule: l3 -> l0 : ___rho_1_^0'=dobreak^post7, dobreak^0'=dobreak^post7, r^0'=0, n^0 <= 0, cost: 1 Propagated Equalities Original rule: l1 -> l2 : ___rho_1_^0'=___rho_1_^post8, ___rho_2_^0'=___rho_2_^post8, a^0'=a^post8, dobreak^0'=dobreak^post8, n^0'=n^post8, r^0'=r^post8, (0 == 0 /\ a^post8 == 0 /\ -___rho_2_^post8+n^post8 == 0 /\ -1+a^1 == 0 /\ dobreak^0 <= 0 /\ dobreak^0-dobreak^post8 == 0 /\ -___rho_1_^post8+___rho_1_^0 == 0 /\ -r^post8+r^0 == 0), cost: 1 New rule: l1 -> l2 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=n^post8, a^0'=0, dobreak^0'=dobreak^0, n^0'=n^post8, r^0'=r^0, (0 == 0 /\ -1+a^1 == 0 /\ dobreak^0 <= 0), cost: 1 propagated equality a^post8 = 0 propagated equality ___rho_2_^post8 = n^post8 propagated equality dobreak^post8 = dobreak^0 propagated equality ___rho_1_^post8 = ___rho_1_^0 propagated equality r^post8 = r^0 Propagated Equalities Original rule: l1 -> l2 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=n^post8, a^0'=0, dobreak^0'=dobreak^0, n^0'=n^post8, r^0'=r^0, (0 == 0 /\ -1+a^1 == 0 /\ dobreak^0 <= 0), cost: 1 New rule: l1 -> l2 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=n^post8, a^0'=0, dobreak^0'=dobreak^0, n^0'=n^post8, r^0'=r^0, (0 == 0 /\ dobreak^0 <= 0), cost: 1 propagated equality a^1 = 1 Simplified Guard Original rule: l1 -> l2 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=n^post8, a^0'=0, dobreak^0'=dobreak^0, n^0'=n^post8, r^0'=r^0, (0 == 0 /\ dobreak^0 <= 0), cost: 1 New rule: l1 -> l2 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=n^post8, a^0'=0, dobreak^0'=dobreak^0, n^0'=n^post8, r^0'=r^0, dobreak^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l1 -> l2 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=n^post8, a^0'=0, dobreak^0'=dobreak^0, n^0'=n^post8, r^0'=r^0, dobreak^0 <= 0, cost: 1 New rule: l1 -> l2 : ___rho_2_^0'=n^post8, a^0'=0, n^0'=n^post8, dobreak^0 <= 0, cost: 1 Propagated Equalities Original rule: l1 -> l6 : ___rho_1_^0'=___rho_1_^post9, ___rho_2_^0'=___rho_2_^post9, a^0'=a^post9, dobreak^0'=dobreak^post9, n^0'=n^post9, r^0'=r^post9, (-r^post9+r^0 == 0 /\ 1-dobreak^0 <= 0 /\ -___rho_1_^post9+___rho_1_^0 == 0 /\ -a^post9+a^0 == 0 /\ ___rho_2_^0-___rho_2_^post9 == 0 /\ n^0-n^post9 == 0 /\ dobreak^0-dobreak^post9 == 0), cost: 1 New rule: l1 -> l6 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, a^0'=a^0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, (0 == 0 /\ 1-dobreak^0 <= 0), cost: 1 propagated equality r^post9 = r^0 propagated equality ___rho_1_^post9 = ___rho_1_^0 propagated equality a^post9 = a^0 propagated equality ___rho_2_^post9 = ___rho_2_^0 propagated equality n^post9 = n^0 propagated equality dobreak^post9 = dobreak^0 Simplified Guard Original rule: l1 -> l6 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, a^0'=a^0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, (0 == 0 /\ 1-dobreak^0 <= 0), cost: 1 New rule: l1 -> l6 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, a^0'=a^0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, 1-dobreak^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l1 -> l6 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, a^0'=a^0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, 1-dobreak^0 <= 0, cost: 1 New rule: l1 -> l6 : 1-dobreak^0 <= 0, cost: 1 Propagated Equalities Original rule: l9 -> l0 : ___rho_1_^0'=___rho_1_^post10, ___rho_2_^0'=___rho_2_^post10, a^0'=a^post10, dobreak^0'=dobreak^post10, n^0'=n^post10, r^0'=r^post10, (0 == 0 /\ a^post10 == 0 /\ -n^post11+n^0 == 0 /\ ___rho_2_^0-___rho_2_^post11 == 0 /\ dobreak^0-dobreak^post11 == 0 /\ -a^post11+a^0 == 0 /\ ___rho_2_^post11-___rho_2_^post10 == 0 /\ r^0-r^post11 == 0 /\ n^post11-n^post10 == 0 /\ -___rho_1_^post11+___rho_1_^0 == 0 /\ dobreak^post10-___rho_1_^post10 == 0 /\ r^post10 == 0), cost: 1 New rule: l9 -> l0 : ___rho_1_^0'=dobreak^post10, ___rho_2_^0'=___rho_2_^post11, a^0'=0, dobreak^0'=dobreak^post10, n^0'=n^post11, r^0'=0, (0 == 0 /\ -n^post11+n^0 == 0 /\ ___rho_2_^0-___rho_2_^post11 == 0 /\ dobreak^0-dobreak^post11 == 0 /\ -a^post11+a^0 == 0 /\ r^0-r^post11 == 0 /\ -___rho_1_^post11+___rho_1_^0 == 0), cost: 1 propagated equality a^post10 = 0 propagated equality ___rho_2_^post10 = ___rho_2_^post11 propagated equality n^post10 = n^post11 propagated equality ___rho_1_^post10 = dobreak^post10 propagated equality r^post10 = 0 Propagated Equalities Original rule: l9 -> l0 : ___rho_1_^0'=dobreak^post10, ___rho_2_^0'=___rho_2_^post11, a^0'=0, dobreak^0'=dobreak^post10, n^0'=n^post11, r^0'=0, (0 == 0 /\ -n^post11+n^0 == 0 /\ ___rho_2_^0-___rho_2_^post11 == 0 /\ dobreak^0-dobreak^post11 == 0 /\ -a^post11+a^0 == 0 /\ r^0-r^post11 == 0 /\ -___rho_1_^post11+___rho_1_^0 == 0), cost: 1 New rule: l9 -> l0 : ___rho_1_^0'=dobreak^post10, ___rho_2_^0'=___rho_2_^0, a^0'=0, dobreak^0'=dobreak^post10, n^0'=n^0, r^0'=0, 0 == 0, cost: 1 propagated equality n^post11 = n^0 propagated equality ___rho_2_^post11 = ___rho_2_^0 propagated equality dobreak^post11 = dobreak^0 propagated equality a^post11 = a^0 propagated equality r^post11 = r^0 propagated equality ___rho_1_^post11 = ___rho_1_^0 Simplified Guard Original rule: l9 -> l0 : ___rho_1_^0'=dobreak^post10, ___rho_2_^0'=___rho_2_^0, a^0'=0, dobreak^0'=dobreak^post10, n^0'=n^0, r^0'=0, 0 == 0, cost: 1 New rule: l9 -> l0 : ___rho_1_^0'=dobreak^post10, ___rho_2_^0'=___rho_2_^0, a^0'=0, dobreak^0'=dobreak^post10, n^0'=n^0, r^0'=0, T, cost: 1 Removed Trivial Updates Original rule: l9 -> l0 : ___rho_1_^0'=dobreak^post10, ___rho_2_^0'=___rho_2_^0, a^0'=0, dobreak^0'=dobreak^post10, n^0'=n^0, r^0'=0, T, cost: 1 New rule: l9 -> l0 : ___rho_1_^0'=dobreak^post10, a^0'=0, dobreak^0'=dobreak^post10, r^0'=0, T, cost: 1 Propagated Equalities Original rule: l6 -> l6 : ___rho_1_^0'=___rho_1_^post5, ___rho_2_^0'=___rho_2_^post5, a^0'=a^post5, dobreak^0'=dobreak^post5, n^0'=n^post5, r^0'=r^post5, (-r^post5+r^post4 == 0 /\ -n^post4+n^0 == 0 /\ -dobreak^post5+dobreak^post4 == 0 /\ ___rho_2_^0-___rho_2_^post4 == 0 /\ a^0-a^post4 == 0 /\ -a^post5+a^post4 == 0 /\ -n^post5+n^post4 == 0 /\ -___rho_2_^post5+___rho_2_^post4 == 0 /\ dobreak^0-dobreak^post4 == 0 /\ -___rho_1_^post5+___rho_1_^post4 == 0 /\ r^0-r^post4 == 0 /\ -___rho_1_^post4+___rho_1_^0 == 0), cost: 1 New rule: l6 -> l6 : ___rho_1_^0'=___rho_1_^post4, ___rho_2_^0'=___rho_2_^post4, a^0'=a^post4, dobreak^0'=dobreak^post4, n^0'=n^post4, r^0'=r^post4, (0 == 0 /\ -n^post4+n^0 == 0 /\ ___rho_2_^0-___rho_2_^post4 == 0 /\ a^0-a^post4 == 0 /\ dobreak^0-dobreak^post4 == 0 /\ r^0-r^post4 == 0 /\ -___rho_1_^post4+___rho_1_^0 == 0), cost: 1 propagated equality r^post5 = r^post4 propagated equality dobreak^post5 = dobreak^post4 propagated equality a^post5 = a^post4 propagated equality n^post5 = n^post4 propagated equality ___rho_2_^post5 = ___rho_2_^post4 propagated equality ___rho_1_^post5 = ___rho_1_^post4 Propagated Equalities Original rule: l6 -> l6 : ___rho_1_^0'=___rho_1_^post4, ___rho_2_^0'=___rho_2_^post4, a^0'=a^post4, dobreak^0'=dobreak^post4, n^0'=n^post4, r^0'=r^post4, (0 == 0 /\ -n^post4+n^0 == 0 /\ ___rho_2_^0-___rho_2_^post4 == 0 /\ a^0-a^post4 == 0 /\ dobreak^0-dobreak^post4 == 0 /\ r^0-r^post4 == 0 /\ -___rho_1_^post4+___rho_1_^0 == 0), cost: 1 New rule: l6 -> l6 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, a^0'=a^0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, 0 == 0, cost: 1 propagated equality n^post4 = n^0 propagated equality ___rho_2_^post4 = ___rho_2_^0 propagated equality a^post4 = a^0 propagated equality dobreak^post4 = dobreak^0 propagated equality r^post4 = r^0 propagated equality ___rho_1_^post4 = ___rho_1_^0 Simplified Guard Original rule: l6 -> l6 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, a^0'=a^0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, 0 == 0, cost: 1 New rule: l6 -> l6 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, a^0'=a^0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, T, cost: 1 Removed Trivial Updates Original rule: l6 -> l6 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, a^0'=a^0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, T, cost: 1 New rule: l6 -> l6 : T, cost: 1 Step with 20 Trace 20[T] Blocked [{}, {}] Step with 13 Trace 20[T], 13[T] Blocked [{}, {}, {}] Step with 19 Trace 20[T], 13[T], 19[(1-dobreak^0 <= 0)] Blocked [{}, {}, {}, {}] Step with 21 Trace 20[T], 13[T], 19[(1-dobreak^0 <= 0)], 21[T] Blocked [{}, {}, {}, {}, {}] Nonterm Start location: l9 Program variables: ___rho_1_^0 ___rho_2_^0 a^0 dobreak^0 n^0 r^0 13: l0 -> l1 : T, cost: 1 18: l1 -> l2 : ___rho_2_^0'=n^post8, a^0'=0, n^0'=n^post8, dobreak^0 <= 0, cost: 1 19: l1 -> l6 : 1-dobreak^0 <= 0, cost: 1 14: l2 -> l3 : T, cost: 1 16: l3 -> l2 : 1-n^0 <= 0, cost: 1 17: l3 -> l0 : ___rho_1_^0'=dobreak^post7, dobreak^0'=dobreak^post7, r^0'=0, n^0 <= 0, cost: 1 15: l4 -> l5 : T, cost: 1 21: l6 -> l6 : T, cost: 1 22: l6 -> LoAT_sink : -1+n >= 0, cost: NONTERM 20: l9 -> l0 : ___rho_1_^0'=dobreak^post10, a^0'=0, dobreak^0'=dobreak^post10, r^0'=0, T, cost: 1 Certificate of Non-Termination Original rule: l6 -> l6 : T, cost: 1 New rule: l6 -> LoAT_sink : -1+n >= 0, cost: NONTERM Replacement map: {} Step with 22 Trace 20[T], 13[T], 19[(1-dobreak^0 <= 0)], 22[-1+n >= 0] Blocked [{}, {}, {}, {}, {22[T]}] Refute Counterexample [ ___rho_1_^0=1 ___rho_2_^0=0 a^0=0 dobreak^0=1 n^0=0 r^0=0 ] 20 [ ___rho_1_^0=1 ___rho_2_^0=0 a^0=0 dobreak^0=1 n^0=0 r^0=0 ] 13 [ ___rho_1_^0=1 ___rho_2_^0=0 a^0=0 dobreak^0=1 n^0=0 r^0=0 ] 19 [ ___rho_1_^0=___rho_1_^0 ___rho_2_^0=0 a^0=a^0 dobreak^0=dobreak^0 n^0=0 r^0=r^0 ] 22 NO Build SHA: a05f16bf13df659c382799650051f91bf6828c7b