NO Initial ITS Start location: l13 Program variables: ___rho_1_^0 ___rho_2_^0 witemsnum^0 0: l0 -> l1 : ___rho_1_^0'=___rho_1_^post1, ___rho_2_^0'=___rho_2_^post1, witemsnum^0'=witemsnum^post1, (-___rho_2_^post1+___rho_2_^0 == 0 /\ -witemsnum^post1+witemsnum^0 == 0 /\ ___rho_1_^0-___rho_1_^post1 == 0), cost: 1 1: l1 -> l2 : ___rho_1_^0'=___rho_1_^post2, ___rho_2_^0'=___rho_2_^post2, witemsnum^0'=witemsnum^post2, (0 == 0 /\ ___rho_1_^0-___rho_1_^post2 == 0 /\ -witemsnum^post2+witemsnum^0 == 0), cost: 1 13: l2 -> l10 : ___rho_1_^0'=___rho_1_^post14, ___rho_2_^0'=___rho_2_^post14, witemsnum^0'=witemsnum^post14, (-witemsnum^post14+witemsnum^0 == 0 /\ ___rho_1_^0-___rho_1_^post14 == 0 /\ -___rho_2_^post14+___rho_2_^0 == 0 /\ 6-witemsnum^0 <= 0), cost: 1 14: l2 -> l11 : ___rho_1_^0'=___rho_1_^post15, ___rho_2_^0'=___rho_2_^post15, witemsnum^0'=witemsnum^post15, (-___rho_2_^post15+___rho_2_^0 == 0 /\ -witemsnum^post15+witemsnum^0 == 0 /\ ___rho_1_^0-___rho_1_^post15 == 0 /\ -5+witemsnum^0 <= 0), cost: 1 2: l3 -> l4 : ___rho_1_^0'=___rho_1_^post3, ___rho_2_^0'=___rho_2_^post3, witemsnum^0'=witemsnum^post3, (-___rho_2_^post3+___rho_2_^0 == 0 /\ ___rho_1_^0-___rho_1_^post3 == 0 /\ -witemsnum^post3+witemsnum^0 == 0), cost: 1 5: l4 -> l3 : ___rho_1_^0'=___rho_1_^post6, ___rho_2_^0'=___rho_2_^post6, witemsnum^0'=witemsnum^post6, (3-witemsnum^0 <= 0 /\ ___rho_1_^0-___rho_1_^post6 == 0 /\ -___rho_2_^post6+___rho_2_^0 == 0 /\ 1+witemsnum^post6-witemsnum^0 == 0), cost: 1 6: l4 -> l0 : ___rho_1_^0'=___rho_1_^post7, ___rho_2_^0'=___rho_2_^post7, witemsnum^0'=witemsnum^post7, (___rho_1_^0-___rho_1_^post7 == 0 /\ -2+witemsnum^0 <= 0 /\ -___rho_2_^post7+___rho_2_^0 == 0 /\ -witemsnum^post7+witemsnum^0 == 0), cost: 1 3: l5 -> l6 : ___rho_1_^0'=___rho_1_^post4, ___rho_2_^0'=___rho_2_^post4, witemsnum^0'=witemsnum^post4, (-witemsnum^post4+witemsnum^0 == 0 /\ ___rho_1_^0-___rho_1_^post4 == 0 /\ -___rho_2_^post4+___rho_2_^0 == 0), cost: 1 4: l7 -> l8 : ___rho_1_^0'=___rho_1_^post5, ___rho_2_^0'=___rho_2_^post5, witemsnum^0'=witemsnum^post5, (___rho_1_^0-___rho_1_^post5 == 0 /\ ___rho_2_^0-___rho_2_^post5 == 0 /\ -witemsnum^post5+witemsnum^0 == 0), cost: 1 7: l8 -> l9 : ___rho_1_^0'=___rho_1_^post8, ___rho_2_^0'=___rho_2_^post8, witemsnum^0'=witemsnum^post8, (witemsnum^0-witemsnum^post8 == 0 /\ -___rho_2_^post8+___rho_2_^0 == 0 /\ ___rho_1_^0-___rho_1_^post8 == 0), cost: 1 8: l9 -> l8 : ___rho_1_^0'=___rho_1_^post9, ___rho_2_^0'=___rho_2_^post9, witemsnum^0'=witemsnum^post9, (witemsnum^0-witemsnum^post9 == 0 /\ -___rho_1_^post9+___rho_1_^0 == 0 /\ -___rho_2_^post9+___rho_2_^0 == 0), cost: 1 9: l10 -> l1 : ___rho_1_^0'=___rho_1_^post10, ___rho_2_^0'=___rho_2_^post10, witemsnum^0'=witemsnum^post10, (-___rho_2_^post10+___rho_2_^0 == 0 /\ -___rho_1_^post10+___rho_1_^0 == 0 /\ -1-witemsnum^0+witemsnum^post10 == 0 /\ 6-witemsnum^0 <= 0), cost: 1 10: l10 -> l1 : ___rho_1_^0'=___rho_1_^post11, ___rho_2_^0'=___rho_2_^post11, witemsnum^0'=witemsnum^post11, (-1-witemsnum^0+witemsnum^post11 == 0 /\ -___rho_2_^post11+___rho_2_^0 == 0 /\ -___rho_1_^post11+___rho_1_^0 == 0 /\ -5+witemsnum^0 <= 0), cost: 1 11: l11 -> l10 : ___rho_1_^0'=___rho_1_^post12, ___rho_2_^0'=___rho_2_^post12, witemsnum^0'=witemsnum^post12, (-___rho_1_^post12+___rho_1_^0 == 0 /\ -___rho_2_^post12+___rho_2_^0 == 0 /\ -witemsnum^post12+witemsnum^0 == 0 /\ ___rho_2_^0 <= 0), cost: 1 12: l11 -> l3 : ___rho_1_^0'=___rho_1_^post13, ___rho_2_^0'=___rho_2_^post13, witemsnum^0'=witemsnum^post13, (___rho_1_^0-___rho_1_^post13 == 0 /\ witemsnum^0-witemsnum^post13 == 0 /\ 1-___rho_2_^0 <= 0 /\ -___rho_2_^post13+___rho_2_^0 == 0), cost: 1 15: l12 -> l0 : ___rho_1_^0'=___rho_1_^post16, ___rho_2_^0'=___rho_2_^post16, witemsnum^0'=witemsnum^post16, (0 == 0 /\ -___rho_1_^post16+witemsnum^post16 == 0 /\ -___rho_2_^post16+___rho_2_^0 == 0), cost: 1 16: l13 -> l12 : ___rho_1_^0'=___rho_1_^post17, ___rho_2_^0'=___rho_2_^post17, witemsnum^0'=witemsnum^post17, (-___rho_2_^post17+___rho_2_^0 == 0 /\ witemsnum^0-witemsnum^post17 == 0 /\ -___rho_1_^post17+___rho_1_^0 == 0), cost: 1 Chained Linear Paths Start location: l13 Program variables: ___rho_1_^0 ___rho_2_^0 witemsnum^0 0: l0 -> l1 : ___rho_1_^0'=___rho_1_^post1, ___rho_2_^0'=___rho_2_^post1, witemsnum^0'=witemsnum^post1, (-___rho_2_^post1+___rho_2_^0 == 0 /\ -witemsnum^post1+witemsnum^0 == 0 /\ ___rho_1_^0-___rho_1_^post1 == 0), cost: 1 1: l1 -> l2 : ___rho_1_^0'=___rho_1_^post2, ___rho_2_^0'=___rho_2_^post2, witemsnum^0'=witemsnum^post2, (0 == 0 /\ ___rho_1_^0-___rho_1_^post2 == 0 /\ -witemsnum^post2+witemsnum^0 == 0), cost: 1 13: l2 -> l10 : ___rho_1_^0'=___rho_1_^post14, ___rho_2_^0'=___rho_2_^post14, witemsnum^0'=witemsnum^post14, (-witemsnum^post14+witemsnum^0 == 0 /\ ___rho_1_^0-___rho_1_^post14 == 0 /\ -___rho_2_^post14+___rho_2_^0 == 0 /\ 6-witemsnum^0 <= 0), cost: 1 14: l2 -> l11 : ___rho_1_^0'=___rho_1_^post15, ___rho_2_^0'=___rho_2_^post15, witemsnum^0'=witemsnum^post15, (-___rho_2_^post15+___rho_2_^0 == 0 /\ -witemsnum^post15+witemsnum^0 == 0 /\ ___rho_1_^0-___rho_1_^post15 == 0 /\ -5+witemsnum^0 <= 0), cost: 1 2: l3 -> l4 : ___rho_1_^0'=___rho_1_^post3, ___rho_2_^0'=___rho_2_^post3, witemsnum^0'=witemsnum^post3, (-___rho_2_^post3+___rho_2_^0 == 0 /\ ___rho_1_^0-___rho_1_^post3 == 0 /\ -witemsnum^post3+witemsnum^0 == 0), cost: 1 5: l4 -> l3 : ___rho_1_^0'=___rho_1_^post6, ___rho_2_^0'=___rho_2_^post6, witemsnum^0'=witemsnum^post6, (3-witemsnum^0 <= 0 /\ ___rho_1_^0-___rho_1_^post6 == 0 /\ -___rho_2_^post6+___rho_2_^0 == 0 /\ 1+witemsnum^post6-witemsnum^0 == 0), cost: 1 6: l4 -> l0 : ___rho_1_^0'=___rho_1_^post7, ___rho_2_^0'=___rho_2_^post7, witemsnum^0'=witemsnum^post7, (___rho_1_^0-___rho_1_^post7 == 0 /\ -2+witemsnum^0 <= 0 /\ -___rho_2_^post7+___rho_2_^0 == 0 /\ -witemsnum^post7+witemsnum^0 == 0), cost: 1 3: l5 -> l6 : ___rho_1_^0'=___rho_1_^post4, ___rho_2_^0'=___rho_2_^post4, witemsnum^0'=witemsnum^post4, (-witemsnum^post4+witemsnum^0 == 0 /\ ___rho_1_^0-___rho_1_^post4 == 0 /\ -___rho_2_^post4+___rho_2_^0 == 0), cost: 1 4: l7 -> l8 : ___rho_1_^0'=___rho_1_^post5, ___rho_2_^0'=___rho_2_^post5, witemsnum^0'=witemsnum^post5, (___rho_1_^0-___rho_1_^post5 == 0 /\ ___rho_2_^0-___rho_2_^post5 == 0 /\ -witemsnum^post5+witemsnum^0 == 0), cost: 1 7: l8 -> l9 : ___rho_1_^0'=___rho_1_^post8, ___rho_2_^0'=___rho_2_^post8, witemsnum^0'=witemsnum^post8, (witemsnum^0-witemsnum^post8 == 0 /\ -___rho_2_^post8+___rho_2_^0 == 0 /\ ___rho_1_^0-___rho_1_^post8 == 0), cost: 1 8: l9 -> l8 : ___rho_1_^0'=___rho_1_^post9, ___rho_2_^0'=___rho_2_^post9, witemsnum^0'=witemsnum^post9, (witemsnum^0-witemsnum^post9 == 0 /\ -___rho_1_^post9+___rho_1_^0 == 0 /\ -___rho_2_^post9+___rho_2_^0 == 0), cost: 1 9: l10 -> l1 : ___rho_1_^0'=___rho_1_^post10, ___rho_2_^0'=___rho_2_^post10, witemsnum^0'=witemsnum^post10, (-___rho_2_^post10+___rho_2_^0 == 0 /\ -___rho_1_^post10+___rho_1_^0 == 0 /\ -1-witemsnum^0+witemsnum^post10 == 0 /\ 6-witemsnum^0 <= 0), cost: 1 10: l10 -> l1 : ___rho_1_^0'=___rho_1_^post11, ___rho_2_^0'=___rho_2_^post11, witemsnum^0'=witemsnum^post11, (-1-witemsnum^0+witemsnum^post11 == 0 /\ -___rho_2_^post11+___rho_2_^0 == 0 /\ -___rho_1_^post11+___rho_1_^0 == 0 /\ -5+witemsnum^0 <= 0), cost: 1 11: l11 -> l10 : ___rho_1_^0'=___rho_1_^post12, ___rho_2_^0'=___rho_2_^post12, witemsnum^0'=witemsnum^post12, (-___rho_1_^post12+___rho_1_^0 == 0 /\ -___rho_2_^post12+___rho_2_^0 == 0 /\ -witemsnum^post12+witemsnum^0 == 0 /\ ___rho_2_^0 <= 0), cost: 1 12: l11 -> l3 : ___rho_1_^0'=___rho_1_^post13, ___rho_2_^0'=___rho_2_^post13, witemsnum^0'=witemsnum^post13, (___rho_1_^0-___rho_1_^post13 == 0 /\ witemsnum^0-witemsnum^post13 == 0 /\ 1-___rho_2_^0 <= 0 /\ -___rho_2_^post13+___rho_2_^0 == 0), cost: 1 17: l13 -> l0 : ___rho_1_^0'=___rho_1_^post16, ___rho_2_^0'=___rho_2_^post16, witemsnum^0'=witemsnum^post16, (0 == 0 /\ ___rho_2_^post17-___rho_2_^post16 == 0 /\ -___rho_1_^post16+witemsnum^post16 == 0 /\ -___rho_2_^post17+___rho_2_^0 == 0 /\ witemsnum^0-witemsnum^post17 == 0 /\ -___rho_1_^post17+___rho_1_^0 == 0), cost: 1 Eliminating location l12 by chaining: Applied chaining First rule: l13 -> l12 : ___rho_1_^0'=___rho_1_^post17, ___rho_2_^0'=___rho_2_^post17, witemsnum^0'=witemsnum^post17, (-___rho_2_^post17+___rho_2_^0 == 0 /\ witemsnum^0-witemsnum^post17 == 0 /\ -___rho_1_^post17+___rho_1_^0 == 0), cost: 1 Second rule: l12 -> l0 : ___rho_1_^0'=___rho_1_^post16, ___rho_2_^0'=___rho_2_^post16, witemsnum^0'=witemsnum^post16, (0 == 0 /\ -___rho_1_^post16+witemsnum^post16 == 0 /\ -___rho_2_^post16+___rho_2_^0 == 0), cost: 1 New rule: l13 -> l0 : ___rho_1_^0'=___rho_1_^post16, ___rho_2_^0'=___rho_2_^post16, witemsnum^0'=witemsnum^post16, (0 == 0 /\ ___rho_2_^post17-___rho_2_^post16 == 0 /\ -___rho_1_^post16+witemsnum^post16 == 0 /\ -___rho_2_^post17+___rho_2_^0 == 0 /\ witemsnum^0-witemsnum^post17 == 0 /\ -___rho_1_^post17+___rho_1_^0 == 0), cost: 1 Applied deletion Removed the following rules: 15 16 Simplified Transitions Start location: l13 Program variables: ___rho_1_^0 ___rho_2_^0 witemsnum^0 18: l0 -> l1 : T, cost: 1 19: l1 -> l2 : ___rho_2_^0'=___rho_2_^post2, T, cost: 1 31: l2 -> l10 : 6-witemsnum^0 <= 0, cost: 1 32: l2 -> l11 : -5+witemsnum^0 <= 0, cost: 1 20: l3 -> l4 : T, cost: 1 23: l4 -> l3 : witemsnum^0'=-1+witemsnum^0, 3-witemsnum^0 <= 0, cost: 1 24: l4 -> l0 : -2+witemsnum^0 <= 0, cost: 1 21: l5 -> l6 : T, cost: 1 22: l7 -> l8 : T, cost: 1 25: l8 -> l9 : T, cost: 1 26: l9 -> l8 : T, cost: 1 27: l10 -> l1 : witemsnum^0'=1+witemsnum^0, 6-witemsnum^0 <= 0, cost: 1 28: l10 -> l1 : witemsnum^0'=1+witemsnum^0, -5+witemsnum^0 <= 0, cost: 1 29: l11 -> l10 : ___rho_2_^0 <= 0, cost: 1 30: l11 -> l3 : 1-___rho_2_^0 <= 0, cost: 1 33: l13 -> l0 : ___rho_1_^0'=witemsnum^post16, witemsnum^0'=witemsnum^post16, T, cost: 1 Propagated Equalities Original rule: l0 -> l1 : ___rho_1_^0'=___rho_1_^post1, ___rho_2_^0'=___rho_2_^post1, witemsnum^0'=witemsnum^post1, (-___rho_2_^post1+___rho_2_^0 == 0 /\ -witemsnum^post1+witemsnum^0 == 0 /\ ___rho_1_^0-___rho_1_^post1 == 0), cost: 1 New rule: l0 -> l1 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, 0 == 0, cost: 1 propagated equality ___rho_2_^post1 = ___rho_2_^0 propagated equality witemsnum^post1 = witemsnum^0 propagated equality ___rho_1_^post1 = ___rho_1_^0 Simplified Guard Original rule: l0 -> l1 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, 0 == 0, cost: 1 New rule: l0 -> l1 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, T, cost: 1 Removed Trivial Updates Original rule: l0 -> l1 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, T, cost: 1 New rule: l0 -> l1 : T, cost: 1 Propagated Equalities Original rule: l1 -> l2 : ___rho_1_^0'=___rho_1_^post2, ___rho_2_^0'=___rho_2_^post2, witemsnum^0'=witemsnum^post2, (0 == 0 /\ ___rho_1_^0-___rho_1_^post2 == 0 /\ -witemsnum^post2+witemsnum^0 == 0), cost: 1 New rule: l1 -> l2 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^post2, witemsnum^0'=witemsnum^0, 0 == 0, cost: 1 propagated equality ___rho_1_^post2 = ___rho_1_^0 propagated equality witemsnum^post2 = witemsnum^0 Simplified Guard Original rule: l1 -> l2 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^post2, witemsnum^0'=witemsnum^0, 0 == 0, cost: 1 New rule: l1 -> l2 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^post2, witemsnum^0'=witemsnum^0, T, cost: 1 Removed Trivial Updates Original rule: l1 -> l2 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^post2, witemsnum^0'=witemsnum^0, T, cost: 1 New rule: l1 -> l2 : ___rho_2_^0'=___rho_2_^post2, T, cost: 1 Propagated Equalities Original rule: l3 -> l4 : ___rho_1_^0'=___rho_1_^post3, ___rho_2_^0'=___rho_2_^post3, witemsnum^0'=witemsnum^post3, (-___rho_2_^post3+___rho_2_^0 == 0 /\ ___rho_1_^0-___rho_1_^post3 == 0 /\ -witemsnum^post3+witemsnum^0 == 0), cost: 1 New rule: l3 -> l4 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, 0 == 0, cost: 1 propagated equality ___rho_2_^post3 = ___rho_2_^0 propagated equality ___rho_1_^post3 = ___rho_1_^0 propagated equality witemsnum^post3 = witemsnum^0 Simplified Guard Original rule: l3 -> l4 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, 0 == 0, cost: 1 New rule: l3 -> l4 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, T, cost: 1 Removed Trivial Updates Original rule: l3 -> l4 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, T, cost: 1 New rule: l3 -> l4 : T, cost: 1 Propagated Equalities Original rule: l5 -> l6 : ___rho_1_^0'=___rho_1_^post4, ___rho_2_^0'=___rho_2_^post4, witemsnum^0'=witemsnum^post4, (-witemsnum^post4+witemsnum^0 == 0 /\ ___rho_1_^0-___rho_1_^post4 == 0 /\ -___rho_2_^post4+___rho_2_^0 == 0), cost: 1 New rule: l5 -> l6 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, 0 == 0, cost: 1 propagated equality witemsnum^post4 = witemsnum^0 propagated equality ___rho_1_^post4 = ___rho_1_^0 propagated equality ___rho_2_^post4 = ___rho_2_^0 Simplified Guard Original rule: l5 -> l6 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, 0 == 0, cost: 1 New rule: l5 -> l6 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, T, cost: 1 Removed Trivial Updates Original rule: l5 -> l6 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, T, cost: 1 New rule: l5 -> l6 : T, cost: 1 Propagated Equalities Original rule: l7 -> l8 : ___rho_1_^0'=___rho_1_^post5, ___rho_2_^0'=___rho_2_^post5, witemsnum^0'=witemsnum^post5, (___rho_1_^0-___rho_1_^post5 == 0 /\ ___rho_2_^0-___rho_2_^post5 == 0 /\ -witemsnum^post5+witemsnum^0 == 0), cost: 1 New rule: l7 -> l8 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, 0 == 0, cost: 1 propagated equality ___rho_1_^post5 = ___rho_1_^0 propagated equality ___rho_2_^post5 = ___rho_2_^0 propagated equality witemsnum^post5 = witemsnum^0 Simplified Guard Original rule: l7 -> l8 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, 0 == 0, cost: 1 New rule: l7 -> l8 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, T, cost: 1 Removed Trivial Updates Original rule: l7 -> l8 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, T, cost: 1 New rule: l7 -> l8 : T, cost: 1 Propagated Equalities Original rule: l4 -> l3 : ___rho_1_^0'=___rho_1_^post6, ___rho_2_^0'=___rho_2_^post6, witemsnum^0'=witemsnum^post6, (3-witemsnum^0 <= 0 /\ ___rho_1_^0-___rho_1_^post6 == 0 /\ -___rho_2_^post6+___rho_2_^0 == 0 /\ 1+witemsnum^post6-witemsnum^0 == 0), cost: 1 New rule: l4 -> l3 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=-1+witemsnum^0, (0 == 0 /\ 3-witemsnum^0 <= 0), cost: 1 propagated equality ___rho_1_^post6 = ___rho_1_^0 propagated equality ___rho_2_^post6 = ___rho_2_^0 propagated equality witemsnum^post6 = -1+witemsnum^0 Simplified Guard Original rule: l4 -> l3 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=-1+witemsnum^0, (0 == 0 /\ 3-witemsnum^0 <= 0), cost: 1 New rule: l4 -> l3 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=-1+witemsnum^0, 3-witemsnum^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l4 -> l3 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=-1+witemsnum^0, 3-witemsnum^0 <= 0, cost: 1 New rule: l4 -> l3 : witemsnum^0'=-1+witemsnum^0, 3-witemsnum^0 <= 0, cost: 1 Propagated Equalities Original rule: l4 -> l0 : ___rho_1_^0'=___rho_1_^post7, ___rho_2_^0'=___rho_2_^post7, witemsnum^0'=witemsnum^post7, (___rho_1_^0-___rho_1_^post7 == 0 /\ -2+witemsnum^0 <= 0 /\ -___rho_2_^post7+___rho_2_^0 == 0 /\ -witemsnum^post7+witemsnum^0 == 0), cost: 1 New rule: l4 -> l0 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, (0 == 0 /\ -2+witemsnum^0 <= 0), cost: 1 propagated equality ___rho_1_^post7 = ___rho_1_^0 propagated equality ___rho_2_^post7 = ___rho_2_^0 propagated equality witemsnum^post7 = witemsnum^0 Simplified Guard Original rule: l4 -> l0 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, (0 == 0 /\ -2+witemsnum^0 <= 0), cost: 1 New rule: l4 -> l0 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, -2+witemsnum^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l4 -> l0 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, -2+witemsnum^0 <= 0, cost: 1 New rule: l4 -> l0 : -2+witemsnum^0 <= 0, cost: 1 Propagated Equalities Original rule: l8 -> l9 : ___rho_1_^0'=___rho_1_^post8, ___rho_2_^0'=___rho_2_^post8, witemsnum^0'=witemsnum^post8, (witemsnum^0-witemsnum^post8 == 0 /\ -___rho_2_^post8+___rho_2_^0 == 0 /\ ___rho_1_^0-___rho_1_^post8 == 0), cost: 1 New rule: l8 -> l9 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, 0 == 0, cost: 1 propagated equality witemsnum^post8 = witemsnum^0 propagated equality ___rho_2_^post8 = ___rho_2_^0 propagated equality ___rho_1_^post8 = ___rho_1_^0 Simplified Guard Original rule: l8 -> l9 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, 0 == 0, cost: 1 New rule: l8 -> l9 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, T, cost: 1 Removed Trivial Updates Original rule: l8 -> l9 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, T, cost: 1 New rule: l8 -> l9 : T, cost: 1 Propagated Equalities Original rule: l9 -> l8 : ___rho_1_^0'=___rho_1_^post9, ___rho_2_^0'=___rho_2_^post9, witemsnum^0'=witemsnum^post9, (witemsnum^0-witemsnum^post9 == 0 /\ -___rho_1_^post9+___rho_1_^0 == 0 /\ -___rho_2_^post9+___rho_2_^0 == 0), cost: 1 New rule: l9 -> l8 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, 0 == 0, cost: 1 propagated equality witemsnum^post9 = witemsnum^0 propagated equality ___rho_1_^post9 = ___rho_1_^0 propagated equality ___rho_2_^post9 = ___rho_2_^0 Simplified Guard Original rule: l9 -> l8 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, 0 == 0, cost: 1 New rule: l9 -> l8 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, T, cost: 1 Removed Trivial Updates Original rule: l9 -> l8 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, T, cost: 1 New rule: l9 -> l8 : T, cost: 1 Propagated Equalities Original rule: l10 -> l1 : ___rho_1_^0'=___rho_1_^post10, ___rho_2_^0'=___rho_2_^post10, witemsnum^0'=witemsnum^post10, (-___rho_2_^post10+___rho_2_^0 == 0 /\ -___rho_1_^post10+___rho_1_^0 == 0 /\ -1-witemsnum^0+witemsnum^post10 == 0 /\ 6-witemsnum^0 <= 0), cost: 1 New rule: l10 -> l1 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=1+witemsnum^0, (0 == 0 /\ 6-witemsnum^0 <= 0), cost: 1 propagated equality ___rho_2_^post10 = ___rho_2_^0 propagated equality ___rho_1_^post10 = ___rho_1_^0 propagated equality witemsnum^post10 = 1+witemsnum^0 Simplified Guard Original rule: l10 -> l1 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=1+witemsnum^0, (0 == 0 /\ 6-witemsnum^0 <= 0), cost: 1 New rule: l10 -> l1 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=1+witemsnum^0, 6-witemsnum^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l10 -> l1 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=1+witemsnum^0, 6-witemsnum^0 <= 0, cost: 1 New rule: l10 -> l1 : witemsnum^0'=1+witemsnum^0, 6-witemsnum^0 <= 0, cost: 1 Propagated Equalities Original rule: l10 -> l1 : ___rho_1_^0'=___rho_1_^post11, ___rho_2_^0'=___rho_2_^post11, witemsnum^0'=witemsnum^post11, (-1-witemsnum^0+witemsnum^post11 == 0 /\ -___rho_2_^post11+___rho_2_^0 == 0 /\ -___rho_1_^post11+___rho_1_^0 == 0 /\ -5+witemsnum^0 <= 0), cost: 1 New rule: l10 -> l1 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=1+witemsnum^0, (0 == 0 /\ -5+witemsnum^0 <= 0), cost: 1 propagated equality witemsnum^post11 = 1+witemsnum^0 propagated equality ___rho_2_^post11 = ___rho_2_^0 propagated equality ___rho_1_^post11 = ___rho_1_^0 Simplified Guard Original rule: l10 -> l1 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=1+witemsnum^0, (0 == 0 /\ -5+witemsnum^0 <= 0), cost: 1 New rule: l10 -> l1 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=1+witemsnum^0, -5+witemsnum^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l10 -> l1 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=1+witemsnum^0, -5+witemsnum^0 <= 0, cost: 1 New rule: l10 -> l1 : witemsnum^0'=1+witemsnum^0, -5+witemsnum^0 <= 0, cost: 1 Propagated Equalities Original rule: l11 -> l10 : ___rho_1_^0'=___rho_1_^post12, ___rho_2_^0'=___rho_2_^post12, witemsnum^0'=witemsnum^post12, (-___rho_1_^post12+___rho_1_^0 == 0 /\ -___rho_2_^post12+___rho_2_^0 == 0 /\ -witemsnum^post12+witemsnum^0 == 0 /\ ___rho_2_^0 <= 0), cost: 1 New rule: l11 -> l10 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, (0 == 0 /\ ___rho_2_^0 <= 0), cost: 1 propagated equality ___rho_1_^post12 = ___rho_1_^0 propagated equality ___rho_2_^post12 = ___rho_2_^0 propagated equality witemsnum^post12 = witemsnum^0 Simplified Guard Original rule: l11 -> l10 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, (0 == 0 /\ ___rho_2_^0 <= 0), cost: 1 New rule: l11 -> l10 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, ___rho_2_^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l11 -> l10 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, ___rho_2_^0 <= 0, cost: 1 New rule: l11 -> l10 : ___rho_2_^0 <= 0, cost: 1 Propagated Equalities Original rule: l11 -> l3 : ___rho_1_^0'=___rho_1_^post13, ___rho_2_^0'=___rho_2_^post13, witemsnum^0'=witemsnum^post13, (___rho_1_^0-___rho_1_^post13 == 0 /\ witemsnum^0-witemsnum^post13 == 0 /\ 1-___rho_2_^0 <= 0 /\ -___rho_2_^post13+___rho_2_^0 == 0), cost: 1 New rule: l11 -> l3 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, (0 == 0 /\ 1-___rho_2_^0 <= 0), cost: 1 propagated equality ___rho_1_^post13 = ___rho_1_^0 propagated equality witemsnum^post13 = witemsnum^0 propagated equality ___rho_2_^post13 = ___rho_2_^0 Simplified Guard Original rule: l11 -> l3 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, (0 == 0 /\ 1-___rho_2_^0 <= 0), cost: 1 New rule: l11 -> l3 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, 1-___rho_2_^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l11 -> l3 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, 1-___rho_2_^0 <= 0, cost: 1 New rule: l11 -> l3 : 1-___rho_2_^0 <= 0, cost: 1 Propagated Equalities Original rule: l2 -> l10 : ___rho_1_^0'=___rho_1_^post14, ___rho_2_^0'=___rho_2_^post14, witemsnum^0'=witemsnum^post14, (-witemsnum^post14+witemsnum^0 == 0 /\ ___rho_1_^0-___rho_1_^post14 == 0 /\ -___rho_2_^post14+___rho_2_^0 == 0 /\ 6-witemsnum^0 <= 0), cost: 1 New rule: l2 -> l10 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, (0 == 0 /\ 6-witemsnum^0 <= 0), cost: 1 propagated equality witemsnum^post14 = witemsnum^0 propagated equality ___rho_1_^post14 = ___rho_1_^0 propagated equality ___rho_2_^post14 = ___rho_2_^0 Simplified Guard Original rule: l2 -> l10 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, (0 == 0 /\ 6-witemsnum^0 <= 0), cost: 1 New rule: l2 -> l10 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, 6-witemsnum^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l2 -> l10 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, 6-witemsnum^0 <= 0, cost: 1 New rule: l2 -> l10 : 6-witemsnum^0 <= 0, cost: 1 Propagated Equalities Original rule: l2 -> l11 : ___rho_1_^0'=___rho_1_^post15, ___rho_2_^0'=___rho_2_^post15, witemsnum^0'=witemsnum^post15, (-___rho_2_^post15+___rho_2_^0 == 0 /\ -witemsnum^post15+witemsnum^0 == 0 /\ ___rho_1_^0-___rho_1_^post15 == 0 /\ -5+witemsnum^0 <= 0), cost: 1 New rule: l2 -> l11 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, (0 == 0 /\ -5+witemsnum^0 <= 0), cost: 1 propagated equality ___rho_2_^post15 = ___rho_2_^0 propagated equality witemsnum^post15 = witemsnum^0 propagated equality ___rho_1_^post15 = ___rho_1_^0 Simplified Guard Original rule: l2 -> l11 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, (0 == 0 /\ -5+witemsnum^0 <= 0), cost: 1 New rule: l2 -> l11 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, -5+witemsnum^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l2 -> l11 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, -5+witemsnum^0 <= 0, cost: 1 New rule: l2 -> l11 : -5+witemsnum^0 <= 0, cost: 1 Propagated Equalities Original rule: l13 -> l0 : ___rho_1_^0'=___rho_1_^post16, ___rho_2_^0'=___rho_2_^post16, witemsnum^0'=witemsnum^post16, (0 == 0 /\ ___rho_2_^post17-___rho_2_^post16 == 0 /\ -___rho_1_^post16+witemsnum^post16 == 0 /\ -___rho_2_^post17+___rho_2_^0 == 0 /\ witemsnum^0-witemsnum^post17 == 0 /\ -___rho_1_^post17+___rho_1_^0 == 0), cost: 1 New rule: l13 -> l0 : ___rho_1_^0'=witemsnum^post16, ___rho_2_^0'=___rho_2_^post17, witemsnum^0'=witemsnum^post16, (0 == 0 /\ -___rho_2_^post17+___rho_2_^0 == 0 /\ witemsnum^0-witemsnum^post17 == 0 /\ -___rho_1_^post17+___rho_1_^0 == 0), cost: 1 propagated equality ___rho_2_^post16 = ___rho_2_^post17 propagated equality ___rho_1_^post16 = witemsnum^post16 Propagated Equalities Original rule: l13 -> l0 : ___rho_1_^0'=witemsnum^post16, ___rho_2_^0'=___rho_2_^post17, witemsnum^0'=witemsnum^post16, (0 == 0 /\ -___rho_2_^post17+___rho_2_^0 == 0 /\ witemsnum^0-witemsnum^post17 == 0 /\ -___rho_1_^post17+___rho_1_^0 == 0), cost: 1 New rule: l13 -> l0 : ___rho_1_^0'=witemsnum^post16, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^post16, 0 == 0, cost: 1 propagated equality ___rho_2_^post17 = ___rho_2_^0 propagated equality witemsnum^post17 = witemsnum^0 propagated equality ___rho_1_^post17 = ___rho_1_^0 Simplified Guard Original rule: l13 -> l0 : ___rho_1_^0'=witemsnum^post16, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^post16, 0 == 0, cost: 1 New rule: l13 -> l0 : ___rho_1_^0'=witemsnum^post16, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^post16, T, cost: 1 Removed Trivial Updates Original rule: l13 -> l0 : ___rho_1_^0'=witemsnum^post16, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^post16, T, cost: 1 New rule: l13 -> l0 : ___rho_1_^0'=witemsnum^post16, witemsnum^0'=witemsnum^post16, T, cost: 1 Step with 33 Trace 33[T] Blocked [{}, {}] Step with 18 Trace 33[T], 18[T] Blocked [{}, {}, {}] Step with 19 Trace 33[T], 18[T], 19[T] Blocked [{}, {}, {}, {}] Step with 31 Trace 33[T], 18[T], 19[T], 31[(6-witemsnum^0 <= 0)] Blocked [{}, {}, {}, {}, {}] Step with 27 Trace 33[T], 18[T], 19[T], 31[(6-witemsnum^0 <= 0)], 27[(6-witemsnum^0 <= 0)] Blocked [{}, {}, {}, {}, {}, {}] Nonterm Start location: l13 Program variables: ___rho_1_^0 ___rho_2_^0 witemsnum^0 18: l0 -> l1 : T, cost: 1 19: l1 -> l2 : ___rho_2_^0'=___rho_2_^post2, T, cost: 1 34: l1 -> LoAT_sink : (-1+n >= 0 /\ -6+witemsnum^0 >= 0), cost: NONTERM 35: l1 -> l1 : ___rho_2_^0'=___rho_2_^post21, witemsnum^0'=n+witemsnum^0, (-1+n >= 0 /\ -6+witemsnum^0 >= 0), cost: 1 31: l2 -> l10 : 6-witemsnum^0 <= 0, cost: 1 32: l2 -> l11 : -5+witemsnum^0 <= 0, cost: 1 20: l3 -> l4 : T, cost: 1 23: l4 -> l3 : witemsnum^0'=-1+witemsnum^0, 3-witemsnum^0 <= 0, cost: 1 24: l4 -> l0 : -2+witemsnum^0 <= 0, cost: 1 21: l5 -> l6 : T, cost: 1 22: l7 -> l8 : T, cost: 1 25: l8 -> l9 : T, cost: 1 26: l9 -> l8 : T, cost: 1 27: l10 -> l1 : witemsnum^0'=1+witemsnum^0, 6-witemsnum^0 <= 0, cost: 1 28: l10 -> l1 : witemsnum^0'=1+witemsnum^0, -5+witemsnum^0 <= 0, cost: 1 29: l11 -> l10 : ___rho_2_^0 <= 0, cost: 1 30: l11 -> l3 : 1-___rho_2_^0 <= 0, cost: 1 33: l13 -> l0 : ___rho_1_^0'=witemsnum^post16, witemsnum^0'=witemsnum^post16, T, cost: 1 Certificate of Non-Termination Original rule: l1 -> l1 : ___rho_2_^0'=___rho_2_^post21, witemsnum^0'=1+witemsnum^0, 6-witemsnum^0 <= 0, cost: 1 New rule: l1 -> LoAT_sink : (-1+n >= 0 /\ -6+witemsnum^0 >= 0), cost: NONTERM -6+witemsnum^0 >= 0 [0]: monotonic increase yields -6+witemsnum^0 >= 0 Replacement map: {-6+witemsnum^0 >= 0 -> -6+witemsnum^0 >= 0} Loop Acceleration Original rule: l1 -> l1 : ___rho_2_^0'=___rho_2_^post21, witemsnum^0'=1+witemsnum^0, 6-witemsnum^0 <= 0, cost: 1 New rule: l1 -> l1 : ___rho_2_^0'=___rho_2_^post21, witemsnum^0'=n+witemsnum^0, (-1+n >= 0 /\ -6+witemsnum^0 >= 0), cost: 1 -6+witemsnum^0 >= 0 [0]: monotonic increase yields -6+witemsnum^0 >= 0 Replacement map: {-6+witemsnum^0 >= 0 -> -6+witemsnum^0 >= 0} Step with 34 Trace 33[T], 18[T], 34[(-1+n >= 0 /\ -6+witemsnum^0 >= 0)] Blocked [{}, {}, {}, {34[T]}] Refute Counterexample [ ___rho_1_^0=6 ___rho_2_^0=0 witemsnum^0=6 ] 33 [ ___rho_1_^0=6 ___rho_2_^0=0 witemsnum^0=6 ] 18 [ ___rho_1_^0=___rho_1_^0 ___rho_2_^0=0 witemsnum^0=witemsnum^0 ] 34 NO Build SHA: a05f16bf13df659c382799650051f91bf6828c7b