NO Initial ITS Start location: l9 Program variables: ___rho_1_^0 a^0 dobreak^0 n^0 r^0 0: l0 -> l1 : ___rho_1_^0'=___rho_1_^post1, a^0'=a^post1, dobreak^0'=dobreak^post1, n^0'=n^post1, r^0'=r^post1, (-n^post1+n^0 == 0 /\ r^0-r^post1 == 0 /\ -___rho_1_^post1+___rho_1_^0 == 0 /\ dobreak^0-dobreak^post1 == 0 /\ -a^post1+a^0 == 0), cost: 1 7: l1 -> l2 : ___rho_1_^0'=___rho_1_^post8, a^0'=a^post8, dobreak^0'=dobreak^post8, n^0'=n^post8, r^0'=r^post8, (0 == 0 /\ n^post8-___rho_1_^post8 == 0 /\ dobreak^0 <= 0 /\ -1+a^1 == 0 /\ -dobreak^post8+dobreak^0 == 0 /\ a^post8 == 0 /\ r^0-r^post8 == 0), cost: 1 8: l1 -> l6 : ___rho_1_^0'=___rho_1_^post9, a^0'=a^post9, dobreak^0'=dobreak^post9, n^0'=n^post9, r^0'=r^post9, (1-dobreak^0 <= 0 /\ -n^post9+n^0 == 0 /\ -___rho_1_^post9+___rho_1_^0 == 0 /\ r^0-r^post9 == 0 /\ -a^post9+a^0 == 0 /\ dobreak^0-dobreak^post9 == 0), cost: 1 1: l2 -> l3 : ___rho_1_^0'=___rho_1_^post2, a^0'=a^post2, dobreak^0'=dobreak^post2, n^0'=n^post2, r^0'=r^post2, (-___rho_1_^post2+___rho_1_^0 == 0 /\ -dobreak^post2+dobreak^0 == 0 /\ -a^post2+a^0 == 0 /\ r^0-r^post2 == 0 /\ n^0-n^post2 == 0), cost: 1 5: l3 -> l2 : ___rho_1_^0'=___rho_1_^post6, a^0'=a^post6, dobreak^0'=dobreak^post6, n^0'=n^post6, r^0'=r^post6, (-a^post6+a^0 == 0 /\ 1-n^0 <= 0 /\ -dobreak^post6+dobreak^0 == 0 /\ n^0-n^post6 == 0 /\ -r^post6+r^0 == 0 /\ -___rho_1_^post6+___rho_1_^0 == 0), cost: 1 6: l3 -> l0 : ___rho_1_^0'=___rho_1_^post7, a^0'=a^post7, dobreak^0'=dobreak^post7, n^0'=n^post7, r^0'=r^post7, (0 == 0 /\ a^0-a^post7 == 0 /\ n^0 <= 0 /\ dobreak^post7-___rho_1_^post7 == 0 /\ n^0-n^post7 == 0 /\ -1+r^1 == 0 /\ r^post7 == 0), cost: 1 2: l4 -> l5 : ___rho_1_^0'=___rho_1_^post3, a^0'=a^post3, dobreak^0'=dobreak^post3, n^0'=n^post3, r^0'=r^post3, (-a^post3+a^0 == 0 /\ r^0-r^post3 == 0 /\ n^0-n^post3 == 0 /\ dobreak^0-dobreak^post3 == 0 /\ -___rho_1_^post3+___rho_1_^0 == 0), cost: 1 3: l6 -> l7 : ___rho_1_^0'=___rho_1_^post4, a^0'=a^post4, dobreak^0'=dobreak^post4, n^0'=n^post4, r^0'=r^post4, (-dobreak^post4+dobreak^0 == 0 /\ r^0-r^post4 == 0 /\ n^0-n^post4 == 0 /\ -___rho_1_^post4+___rho_1_^0 == 0 /\ -a^post4+a^0 == 0), cost: 1 4: l7 -> l6 : ___rho_1_^0'=___rho_1_^post5, a^0'=a^post5, dobreak^0'=dobreak^post5, n^0'=n^post5, r^0'=r^post5, (-a^post5+a^0 == 0 /\ n^0-n^post5 == 0 /\ r^0-r^post5 == 0 /\ dobreak^0-dobreak^post5 == 0 /\ -___rho_1_^post5+___rho_1_^0 == 0), cost: 1 9: l8 -> l0 : ___rho_1_^0'=___rho_1_^post10, a^0'=a^post10, dobreak^0'=dobreak^post10, n^0'=n^post10, r^0'=r^post10, (0 == 0 /\ a^post10 == 0 /\ n^0-n^post10 == 0 /\ dobreak^post10-___rho_1_^post10 == 0 /\ r^post10 == 0), cost: 1 10: l9 -> l8 : ___rho_1_^0'=___rho_1_^post11, a^0'=a^post11, dobreak^0'=dobreak^post11, n^0'=n^post11, r^0'=r^post11, (a^0-a^post11 == 0 /\ -___rho_1_^post11+___rho_1_^0 == 0 /\ r^0-r^post11 == 0 /\ n^0-n^post11 == 0 /\ -dobreak^post11+dobreak^0 == 0), cost: 1 Chained Linear Paths Start location: l9 Program variables: ___rho_1_^0 a^0 dobreak^0 n^0 r^0 0: l0 -> l1 : ___rho_1_^0'=___rho_1_^post1, a^0'=a^post1, dobreak^0'=dobreak^post1, n^0'=n^post1, r^0'=r^post1, (-n^post1+n^0 == 0 /\ r^0-r^post1 == 0 /\ -___rho_1_^post1+___rho_1_^0 == 0 /\ dobreak^0-dobreak^post1 == 0 /\ -a^post1+a^0 == 0), cost: 1 7: l1 -> l2 : ___rho_1_^0'=___rho_1_^post8, a^0'=a^post8, dobreak^0'=dobreak^post8, n^0'=n^post8, r^0'=r^post8, (0 == 0 /\ n^post8-___rho_1_^post8 == 0 /\ dobreak^0 <= 0 /\ -1+a^1 == 0 /\ -dobreak^post8+dobreak^0 == 0 /\ a^post8 == 0 /\ r^0-r^post8 == 0), cost: 1 8: l1 -> l6 : ___rho_1_^0'=___rho_1_^post9, a^0'=a^post9, dobreak^0'=dobreak^post9, n^0'=n^post9, r^0'=r^post9, (1-dobreak^0 <= 0 /\ -n^post9+n^0 == 0 /\ -___rho_1_^post9+___rho_1_^0 == 0 /\ r^0-r^post9 == 0 /\ -a^post9+a^0 == 0 /\ dobreak^0-dobreak^post9 == 0), cost: 1 1: l2 -> l3 : ___rho_1_^0'=___rho_1_^post2, a^0'=a^post2, dobreak^0'=dobreak^post2, n^0'=n^post2, r^0'=r^post2, (-___rho_1_^post2+___rho_1_^0 == 0 /\ -dobreak^post2+dobreak^0 == 0 /\ -a^post2+a^0 == 0 /\ r^0-r^post2 == 0 /\ n^0-n^post2 == 0), cost: 1 5: l3 -> l2 : ___rho_1_^0'=___rho_1_^post6, a^0'=a^post6, dobreak^0'=dobreak^post6, n^0'=n^post6, r^0'=r^post6, (-a^post6+a^0 == 0 /\ 1-n^0 <= 0 /\ -dobreak^post6+dobreak^0 == 0 /\ n^0-n^post6 == 0 /\ -r^post6+r^0 == 0 /\ -___rho_1_^post6+___rho_1_^0 == 0), cost: 1 6: l3 -> l0 : ___rho_1_^0'=___rho_1_^post7, a^0'=a^post7, dobreak^0'=dobreak^post7, n^0'=n^post7, r^0'=r^post7, (0 == 0 /\ a^0-a^post7 == 0 /\ n^0 <= 0 /\ dobreak^post7-___rho_1_^post7 == 0 /\ n^0-n^post7 == 0 /\ -1+r^1 == 0 /\ r^post7 == 0), cost: 1 2: l4 -> l5 : ___rho_1_^0'=___rho_1_^post3, a^0'=a^post3, dobreak^0'=dobreak^post3, n^0'=n^post3, r^0'=r^post3, (-a^post3+a^0 == 0 /\ r^0-r^post3 == 0 /\ n^0-n^post3 == 0 /\ dobreak^0-dobreak^post3 == 0 /\ -___rho_1_^post3+___rho_1_^0 == 0), cost: 1 12: l6 -> l6 : ___rho_1_^0'=___rho_1_^post5, a^0'=a^post5, dobreak^0'=dobreak^post5, n^0'=n^post5, r^0'=r^post5, (-r^post5+r^post4 == 0 /\ dobreak^post4-dobreak^post5 == 0 /\ -___rho_1_^post5+___rho_1_^post4 == 0 /\ -dobreak^post4+dobreak^0 == 0 /\ r^0-r^post4 == 0 /\ n^0-n^post4 == 0 /\ -___rho_1_^post4+___rho_1_^0 == 0 /\ -n^post5+n^post4 == 0 /\ -a^post4+a^0 == 0 /\ a^post4-a^post5 == 0), cost: 1 11: l9 -> l0 : ___rho_1_^0'=___rho_1_^post10, a^0'=a^post10, dobreak^0'=dobreak^post10, n^0'=n^post10, r^0'=r^post10, (0 == 0 /\ a^0-a^post11 == 0 /\ a^post10 == 0 /\ dobreak^post10-___rho_1_^post10 == 0 /\ r^post10 == 0 /\ n^post11-n^post10 == 0 /\ -___rho_1_^post11+___rho_1_^0 == 0 /\ r^0-r^post11 == 0 /\ n^0-n^post11 == 0 /\ -dobreak^post11+dobreak^0 == 0), cost: 1 Eliminating location l8 by chaining: Applied chaining First rule: l9 -> l8 : ___rho_1_^0'=___rho_1_^post11, a^0'=a^post11, dobreak^0'=dobreak^post11, n^0'=n^post11, r^0'=r^post11, (a^0-a^post11 == 0 /\ -___rho_1_^post11+___rho_1_^0 == 0 /\ r^0-r^post11 == 0 /\ n^0-n^post11 == 0 /\ -dobreak^post11+dobreak^0 == 0), cost: 1 Second rule: l8 -> l0 : ___rho_1_^0'=___rho_1_^post10, a^0'=a^post10, dobreak^0'=dobreak^post10, n^0'=n^post10, r^0'=r^post10, (0 == 0 /\ a^post10 == 0 /\ n^0-n^post10 == 0 /\ dobreak^post10-___rho_1_^post10 == 0 /\ r^post10 == 0), cost: 1 New rule: l9 -> l0 : ___rho_1_^0'=___rho_1_^post10, a^0'=a^post10, dobreak^0'=dobreak^post10, n^0'=n^post10, r^0'=r^post10, (0 == 0 /\ a^0-a^post11 == 0 /\ a^post10 == 0 /\ dobreak^post10-___rho_1_^post10 == 0 /\ r^post10 == 0 /\ n^post11-n^post10 == 0 /\ -___rho_1_^post11+___rho_1_^0 == 0 /\ r^0-r^post11 == 0 /\ n^0-n^post11 == 0 /\ -dobreak^post11+dobreak^0 == 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, a^0'=a^post4, dobreak^0'=dobreak^post4, n^0'=n^post4, r^0'=r^post4, (-dobreak^post4+dobreak^0 == 0 /\ r^0-r^post4 == 0 /\ n^0-n^post4 == 0 /\ -___rho_1_^post4+___rho_1_^0 == 0 /\ -a^post4+a^0 == 0), cost: 1 Second rule: l7 -> l6 : ___rho_1_^0'=___rho_1_^post5, a^0'=a^post5, dobreak^0'=dobreak^post5, n^0'=n^post5, r^0'=r^post5, (-a^post5+a^0 == 0 /\ n^0-n^post5 == 0 /\ r^0-r^post5 == 0 /\ dobreak^0-dobreak^post5 == 0 /\ -___rho_1_^post5+___rho_1_^0 == 0), cost: 1 New rule: l6 -> l6 : ___rho_1_^0'=___rho_1_^post5, a^0'=a^post5, dobreak^0'=dobreak^post5, n^0'=n^post5, r^0'=r^post5, (-r^post5+r^post4 == 0 /\ dobreak^post4-dobreak^post5 == 0 /\ -___rho_1_^post5+___rho_1_^post4 == 0 /\ -dobreak^post4+dobreak^0 == 0 /\ r^0-r^post4 == 0 /\ n^0-n^post4 == 0 /\ -___rho_1_^post4+___rho_1_^0 == 0 /\ -n^post5+n^post4 == 0 /\ -a^post4+a^0 == 0 /\ a^post4-a^post5 == 0), cost: 1 Applied deletion Removed the following rules: 3 4 Simplified Transitions Start location: l9 Program variables: ___rho_1_^0 a^0 dobreak^0 n^0 r^0 13: l0 -> l1 : T, cost: 1 18: l1 -> l2 : ___rho_1_^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, a^0'=a^post1, dobreak^0'=dobreak^post1, n^0'=n^post1, r^0'=r^post1, (-n^post1+n^0 == 0 /\ r^0-r^post1 == 0 /\ -___rho_1_^post1+___rho_1_^0 == 0 /\ dobreak^0-dobreak^post1 == 0 /\ -a^post1+a^0 == 0), cost: 1 New rule: l0 -> l1 : ___rho_1_^0'=___rho_1_^0, a^0'=a^0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, 0 == 0, cost: 1 propagated equality n^post1 = n^0 propagated equality r^post1 = r^0 propagated equality ___rho_1_^post1 = ___rho_1_^0 propagated equality dobreak^post1 = dobreak^0 propagated equality a^post1 = a^0 Simplified Guard Original rule: l0 -> l1 : ___rho_1_^0'=___rho_1_^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, 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, 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, a^0'=a^post2, dobreak^0'=dobreak^post2, n^0'=n^post2, r^0'=r^post2, (-___rho_1_^post2+___rho_1_^0 == 0 /\ -dobreak^post2+dobreak^0 == 0 /\ -a^post2+a^0 == 0 /\ r^0-r^post2 == 0 /\ n^0-n^post2 == 0), cost: 1 New rule: l2 -> l3 : ___rho_1_^0'=___rho_1_^0, a^0'=a^0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, 0 == 0, cost: 1 propagated equality ___rho_1_^post2 = ___rho_1_^0 propagated equality dobreak^post2 = dobreak^0 propagated equality a^post2 = a^0 propagated equality r^post2 = r^0 propagated equality n^post2 = n^0 Simplified Guard Original rule: l2 -> l3 : ___rho_1_^0'=___rho_1_^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, 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, 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, a^0'=a^post3, dobreak^0'=dobreak^post3, n^0'=n^post3, r^0'=r^post3, (-a^post3+a^0 == 0 /\ r^0-r^post3 == 0 /\ n^0-n^post3 == 0 /\ dobreak^0-dobreak^post3 == 0 /\ -___rho_1_^post3+___rho_1_^0 == 0), cost: 1 New rule: l4 -> l5 : ___rho_1_^0'=___rho_1_^0, a^0'=a^0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, 0 == 0, cost: 1 propagated equality a^post3 = a^0 propagated equality r^post3 = r^0 propagated equality n^post3 = n^0 propagated equality dobreak^post3 = dobreak^0 propagated equality ___rho_1_^post3 = ___rho_1_^0 Simplified Guard Original rule: l4 -> l5 : ___rho_1_^0'=___rho_1_^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, 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, 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, a^0'=a^post6, dobreak^0'=dobreak^post6, n^0'=n^post6, r^0'=r^post6, (-a^post6+a^0 == 0 /\ 1-n^0 <= 0 /\ -dobreak^post6+dobreak^0 == 0 /\ n^0-n^post6 == 0 /\ -r^post6+r^0 == 0 /\ -___rho_1_^post6+___rho_1_^0 == 0), cost: 1 New rule: l3 -> l2 : ___rho_1_^0'=___rho_1_^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 a^post6 = a^0 propagated equality dobreak^post6 = dobreak^0 propagated equality n^post6 = n^0 propagated equality r^post6 = r^0 propagated equality ___rho_1_^post6 = ___rho_1_^0 Simplified Guard Original rule: l3 -> l2 : ___rho_1_^0'=___rho_1_^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, 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, 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, a^0'=a^post7, dobreak^0'=dobreak^post7, n^0'=n^post7, r^0'=r^post7, (0 == 0 /\ a^0-a^post7 == 0 /\ n^0 <= 0 /\ dobreak^post7-___rho_1_^post7 == 0 /\ n^0-n^post7 == 0 /\ -1+r^1 == 0 /\ r^post7 == 0), cost: 1 New rule: l3 -> l0 : ___rho_1_^0'=dobreak^post7, 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 a^post7 = a^0 propagated equality ___rho_1_^post7 = dobreak^post7 propagated equality n^post7 = n^0 propagated equality r^post7 = 0 Propagated Equalities Original rule: l3 -> l0 : ___rho_1_^0'=dobreak^post7, 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, 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, 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, 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, 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, a^0'=a^post8, dobreak^0'=dobreak^post8, n^0'=n^post8, r^0'=r^post8, (0 == 0 /\ n^post8-___rho_1_^post8 == 0 /\ dobreak^0 <= 0 /\ -1+a^1 == 0 /\ -dobreak^post8+dobreak^0 == 0 /\ a^post8 == 0 /\ r^0-r^post8 == 0), cost: 1 New rule: l1 -> l2 : ___rho_1_^0'=n^post8, a^0'=0, dobreak^0'=dobreak^0, n^0'=n^post8, r^0'=r^0, (0 == 0 /\ dobreak^0 <= 0 /\ -1+a^1 == 0), cost: 1 propagated equality ___rho_1_^post8 = n^post8 propagated equality dobreak^post8 = dobreak^0 propagated equality a^post8 = 0 propagated equality r^post8 = r^0 Propagated Equalities Original rule: l1 -> l2 : ___rho_1_^0'=n^post8, a^0'=0, dobreak^0'=dobreak^0, n^0'=n^post8, r^0'=r^0, (0 == 0 /\ dobreak^0 <= 0 /\ -1+a^1 == 0), cost: 1 New rule: l1 -> l2 : ___rho_1_^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'=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'=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'=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_1_^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, a^0'=a^post9, dobreak^0'=dobreak^post9, n^0'=n^post9, r^0'=r^post9, (1-dobreak^0 <= 0 /\ -n^post9+n^0 == 0 /\ -___rho_1_^post9+___rho_1_^0 == 0 /\ r^0-r^post9 == 0 /\ -a^post9+a^0 == 0 /\ dobreak^0-dobreak^post9 == 0), cost: 1 New rule: l1 -> l6 : ___rho_1_^0'=___rho_1_^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 n^post9 = n^0 propagated equality ___rho_1_^post9 = ___rho_1_^0 propagated equality r^post9 = r^0 propagated equality a^post9 = a^0 propagated equality dobreak^post9 = dobreak^0 Simplified Guard Original rule: l1 -> l6 : ___rho_1_^0'=___rho_1_^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, 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, 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, a^0'=a^post10, dobreak^0'=dobreak^post10, n^0'=n^post10, r^0'=r^post10, (0 == 0 /\ a^0-a^post11 == 0 /\ a^post10 == 0 /\ dobreak^post10-___rho_1_^post10 == 0 /\ r^post10 == 0 /\ n^post11-n^post10 == 0 /\ -___rho_1_^post11+___rho_1_^0 == 0 /\ r^0-r^post11 == 0 /\ n^0-n^post11 == 0 /\ -dobreak^post11+dobreak^0 == 0), cost: 1 New rule: l9 -> l0 : ___rho_1_^0'=dobreak^post10, a^0'=0, dobreak^0'=dobreak^post10, n^0'=n^post11, r^0'=0, (0 == 0 /\ a^0-a^post11 == 0 /\ -___rho_1_^post11+___rho_1_^0 == 0 /\ r^0-r^post11 == 0 /\ n^0-n^post11 == 0 /\ -dobreak^post11+dobreak^0 == 0), cost: 1 propagated equality a^post10 = 0 propagated equality ___rho_1_^post10 = dobreak^post10 propagated equality r^post10 = 0 propagated equality n^post10 = n^post11 Propagated Equalities Original rule: l9 -> l0 : ___rho_1_^0'=dobreak^post10, a^0'=0, dobreak^0'=dobreak^post10, n^0'=n^post11, r^0'=0, (0 == 0 /\ a^0-a^post11 == 0 /\ -___rho_1_^post11+___rho_1_^0 == 0 /\ r^0-r^post11 == 0 /\ n^0-n^post11 == 0 /\ -dobreak^post11+dobreak^0 == 0), cost: 1 New rule: l9 -> l0 : ___rho_1_^0'=dobreak^post10, a^0'=0, dobreak^0'=dobreak^post10, n^0'=n^0, r^0'=0, 0 == 0, cost: 1 propagated equality a^post11 = a^0 propagated equality ___rho_1_^post11 = ___rho_1_^0 propagated equality r^post11 = r^0 propagated equality n^post11 = n^0 propagated equality dobreak^post11 = dobreak^0 Simplified Guard Original rule: l9 -> l0 : ___rho_1_^0'=dobreak^post10, 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, 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, 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, a^0'=a^post5, dobreak^0'=dobreak^post5, n^0'=n^post5, r^0'=r^post5, (-r^post5+r^post4 == 0 /\ dobreak^post4-dobreak^post5 == 0 /\ -___rho_1_^post5+___rho_1_^post4 == 0 /\ -dobreak^post4+dobreak^0 == 0 /\ r^0-r^post4 == 0 /\ n^0-n^post4 == 0 /\ -___rho_1_^post4+___rho_1_^0 == 0 /\ -n^post5+n^post4 == 0 /\ -a^post4+a^0 == 0 /\ a^post4-a^post5 == 0), cost: 1 New rule: l6 -> l6 : ___rho_1_^0'=___rho_1_^post4, a^0'=a^post4, dobreak^0'=dobreak^post4, n^0'=n^post4, r^0'=r^post4, (0 == 0 /\ -dobreak^post4+dobreak^0 == 0 /\ r^0-r^post4 == 0 /\ n^0-n^post4 == 0 /\ -___rho_1_^post4+___rho_1_^0 == 0 /\ -a^post4+a^0 == 0), cost: 1 propagated equality r^post5 = r^post4 propagated equality dobreak^post5 = dobreak^post4 propagated equality ___rho_1_^post5 = ___rho_1_^post4 propagated equality n^post5 = n^post4 propagated equality a^post5 = a^post4 Propagated Equalities Original rule: l6 -> l6 : ___rho_1_^0'=___rho_1_^post4, a^0'=a^post4, dobreak^0'=dobreak^post4, n^0'=n^post4, r^0'=r^post4, (0 == 0 /\ -dobreak^post4+dobreak^0 == 0 /\ r^0-r^post4 == 0 /\ n^0-n^post4 == 0 /\ -___rho_1_^post4+___rho_1_^0 == 0 /\ -a^post4+a^0 == 0), cost: 1 New rule: l6 -> l6 : ___rho_1_^0'=___rho_1_^0, a^0'=a^0, dobreak^0'=dobreak^0, n^0'=n^0, r^0'=r^0, 0 == 0, cost: 1 propagated equality dobreak^post4 = dobreak^0 propagated equality r^post4 = r^0 propagated equality n^post4 = n^0 propagated equality ___rho_1_^post4 = ___rho_1_^0 propagated equality a^post4 = a^0 Simplified Guard Original rule: l6 -> l6 : ___rho_1_^0'=___rho_1_^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, 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, 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 a^0 dobreak^0 n^0 r^0 13: l0 -> l1 : T, cost: 1 18: l1 -> l2 : ___rho_1_^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 a^0=0 dobreak^0=1 n^0=0 r^0=0 ] 20 [ ___rho_1_^0=1 a^0=0 dobreak^0=1 n^0=0 r^0=0 ] 13 [ ___rho_1_^0=1 a^0=0 dobreak^0=1 n^0=0 r^0=0 ] 19 [ ___rho_1_^0=___rho_1_^0 a^0=a^0 dobreak^0=dobreak^0 n^0=0 r^0=r^0 ] 22 NO Build SHA: a05f16bf13df659c382799650051f91bf6828c7b