NO Initial ITS Start location: l17 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 -> l0 : ___rho_1_^0'=___rho_1_^post2, ___rho_2_^0'=___rho_2_^post2, witemsnum^0'=witemsnum^post2, (-___rho_2_^post2+___rho_2_^0 == 0 /\ ___rho_1_^0-___rho_1_^post2 == 0 /\ -witemsnum^post2+witemsnum^0 == 0), cost: 1 2: l2 -> l3 : ___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 3: l3 -> l4 : ___rho_1_^0'=___rho_1_^post4, ___rho_2_^0'=___rho_2_^post4, witemsnum^0'=witemsnum^post4, (0 == 0 /\ -witemsnum^post4+witemsnum^0 == 0 /\ ___rho_1_^0-___rho_1_^post4 == 0), cost: 1 15: l4 -> l12 : ___rho_1_^0'=___rho_1_^post16, ___rho_2_^0'=___rho_2_^post16, witemsnum^0'=witemsnum^post16, (-___rho_2_^post16+___rho_2_^0 == 0 /\ -witemsnum^post16+witemsnum^0 == 0 /\ 6-witemsnum^0 <= 0 /\ ___rho_1_^0-___rho_1_^post16 == 0), cost: 1 16: l4 -> l13 : ___rho_1_^0'=___rho_1_^post17, ___rho_2_^0'=___rho_2_^post17, witemsnum^0'=witemsnum^post17, (-___rho_2_^post17+___rho_2_^0 == 0 /\ ___rho_1_^0-___rho_1_^post17 == 0 /\ -witemsnum^post17+witemsnum^0 == 0 /\ -5+witemsnum^0 <= 0), cost: 1 4: l5 -> l6 : ___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 5: l7 -> l8 : ___rho_1_^0'=___rho_1_^post6, ___rho_2_^0'=___rho_2_^post6, witemsnum^0'=witemsnum^post6, (___rho_1_^0-___rho_1_^post6 == 0 /\ -___rho_2_^post6+___rho_2_^0 == 0 /\ -witemsnum^post6+witemsnum^0 == 0), cost: 1 9: l8 -> l11 : ___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 /\ witemsnum^0-witemsnum^post10 == 0), cost: 1 6: l9 -> l10 : ___rho_1_^0'=___rho_1_^post7, ___rho_2_^0'=___rho_2_^post7, witemsnum^0'=witemsnum^post7, (___rho_1_^0-___rho_1_^post7 == 0 /\ -___rho_2_^post7+___rho_2_^0 == 0 /\ -witemsnum^post7+witemsnum^0 == 0), cost: 1 7: l10 -> l9 : ___rho_1_^0'=___rho_1_^post8, ___rho_2_^0'=___rho_2_^post8, witemsnum^0'=witemsnum^post8, (3-witemsnum^0 <= 0 /\ 1-witemsnum^0+witemsnum^post8 == 0 /\ -___rho_2_^post8+___rho_2_^0 == 0 /\ ___rho_1_^0-___rho_1_^post8 == 0), cost: 1 8: l10 -> l2 : ___rho_1_^0'=___rho_1_^post9, ___rho_2_^0'=___rho_2_^post9, witemsnum^0'=witemsnum^post9, (witemsnum^0-witemsnum^post9 == 0 /\ -2+witemsnum^0 <= 0 /\ -___rho_1_^post9+___rho_1_^0 == 0 /\ -___rho_2_^post9+___rho_2_^0 == 0), cost: 1 10: l11 -> l8 : ___rho_1_^0'=___rho_1_^post11, ___rho_2_^0'=___rho_2_^post11, witemsnum^0'=witemsnum^post11, (-___rho_2_^post11+___rho_2_^0 == 0 /\ witemsnum^0-witemsnum^post11 == 0 /\ -___rho_1_^post11+___rho_1_^0 == 0), cost: 1 11: l12 -> l3 : ___rho_1_^0'=___rho_1_^post12, ___rho_2_^0'=___rho_2_^post12, witemsnum^0'=witemsnum^post12, (-1+witemsnum^post12-witemsnum^0 == 0 /\ -___rho_1_^post12+___rho_1_^0 == 0 /\ -___rho_2_^post12+___rho_2_^0 == 0 /\ 6-witemsnum^0 <= 0), cost: 1 12: l12 -> l3 : ___rho_1_^0'=___rho_1_^post13, ___rho_2_^0'=___rho_2_^post13, witemsnum^0'=witemsnum^post13, (-1-witemsnum^0+witemsnum^post13 == 0 /\ ___rho_1_^0-___rho_1_^post13 == 0 /\ -___rho_2_^post13+___rho_2_^0 == 0 /\ -5+witemsnum^0 <= 0), cost: 1 13: l13 -> l12 : ___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 /\ ___rho_2_^0 <= 0), cost: 1 14: l13 -> l9 : ___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 /\ 1-___rho_2_^0 <= 0), cost: 1 17: l14 -> l2 : ___rho_1_^0'=___rho_1_^post18, ___rho_2_^0'=___rho_2_^post18, witemsnum^0'=witemsnum^post18, (___rho_1_^0-___rho_1_^post18 == 0 /\ -witemsnum^post18+witemsnum^0 == 0 /\ -___rho_2_^post18+___rho_2_^0 == 0), cost: 1 18: l15 -> l2 : ___rho_1_^0'=___rho_1_^post19, ___rho_2_^0'=___rho_2_^post19, witemsnum^0'=witemsnum^post19, (-witemsnum^post19+witemsnum^0 == 0 /\ -witemsnum^0 <= 0 /\ ___rho_1_^0-___rho_1_^post19 == 0 /\ -___rho_2_^post19+___rho_2_^0 == 0), cost: 1 19: l15 -> l0 : ___rho_1_^0'=___rho_1_^post20, ___rho_2_^0'=___rho_2_^post20, witemsnum^0'=witemsnum^post20, (-___rho_2_^post20+___rho_2_^0 == 0 /\ -witemsnum^post20+witemsnum^0 == 0 /\ ___rho_1_^0-___rho_1_^post20 == 0 /\ 1+witemsnum^0 <= 0), cost: 1 20: l16 -> l15 : ___rho_1_^0'=___rho_1_^post21, ___rho_2_^0'=___rho_2_^post21, witemsnum^0'=witemsnum^post21, (0 == 0 /\ -___rho_2_^post21+___rho_2_^0 == 0 /\ -___rho_1_^post21+witemsnum^post21 == 0), cost: 1 21: l17 -> l16 : ___rho_1_^0'=___rho_1_^post22, ___rho_2_^0'=___rho_2_^post22, witemsnum^0'=witemsnum^post22, (-___rho_2_^post22+___rho_2_^0 == 0 /\ -___rho_1_^post22+___rho_1_^0 == 0 /\ witemsnum^0-witemsnum^post22 == 0), cost: 1 Chained Linear Paths Start location: l17 Program variables: ___rho_1_^0 ___rho_2_^0 witemsnum^0 23: l0 -> l0 : ___rho_1_^0'=___rho_1_^post2, ___rho_2_^0'=___rho_2_^post2, witemsnum^0'=witemsnum^post2, (-___rho_2_^post2+___rho_2_^post1 == 0 /\ -witemsnum^post2+witemsnum^post1 == 0 /\ -___rho_2_^post1+___rho_2_^0 == 0 /\ -___rho_1_^post2+___rho_1_^post1 == 0 /\ -witemsnum^post1+witemsnum^0 == 0 /\ ___rho_1_^0-___rho_1_^post1 == 0), cost: 1 2: l2 -> l3 : ___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 3: l3 -> l4 : ___rho_1_^0'=___rho_1_^post4, ___rho_2_^0'=___rho_2_^post4, witemsnum^0'=witemsnum^post4, (0 == 0 /\ -witemsnum^post4+witemsnum^0 == 0 /\ ___rho_1_^0-___rho_1_^post4 == 0), cost: 1 15: l4 -> l12 : ___rho_1_^0'=___rho_1_^post16, ___rho_2_^0'=___rho_2_^post16, witemsnum^0'=witemsnum^post16, (-___rho_2_^post16+___rho_2_^0 == 0 /\ -witemsnum^post16+witemsnum^0 == 0 /\ 6-witemsnum^0 <= 0 /\ ___rho_1_^0-___rho_1_^post16 == 0), cost: 1 16: l4 -> l13 : ___rho_1_^0'=___rho_1_^post17, ___rho_2_^0'=___rho_2_^post17, witemsnum^0'=witemsnum^post17, (-___rho_2_^post17+___rho_2_^0 == 0 /\ ___rho_1_^0-___rho_1_^post17 == 0 /\ -witemsnum^post17+witemsnum^0 == 0 /\ -5+witemsnum^0 <= 0), cost: 1 4: l5 -> l6 : ___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 5: l7 -> l8 : ___rho_1_^0'=___rho_1_^post6, ___rho_2_^0'=___rho_2_^post6, witemsnum^0'=witemsnum^post6, (___rho_1_^0-___rho_1_^post6 == 0 /\ -___rho_2_^post6+___rho_2_^0 == 0 /\ -witemsnum^post6+witemsnum^0 == 0), cost: 1 9: l8 -> l11 : ___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 /\ witemsnum^0-witemsnum^post10 == 0), cost: 1 6: l9 -> l10 : ___rho_1_^0'=___rho_1_^post7, ___rho_2_^0'=___rho_2_^post7, witemsnum^0'=witemsnum^post7, (___rho_1_^0-___rho_1_^post7 == 0 /\ -___rho_2_^post7+___rho_2_^0 == 0 /\ -witemsnum^post7+witemsnum^0 == 0), cost: 1 7: l10 -> l9 : ___rho_1_^0'=___rho_1_^post8, ___rho_2_^0'=___rho_2_^post8, witemsnum^0'=witemsnum^post8, (3-witemsnum^0 <= 0 /\ 1-witemsnum^0+witemsnum^post8 == 0 /\ -___rho_2_^post8+___rho_2_^0 == 0 /\ ___rho_1_^0-___rho_1_^post8 == 0), cost: 1 8: l10 -> l2 : ___rho_1_^0'=___rho_1_^post9, ___rho_2_^0'=___rho_2_^post9, witemsnum^0'=witemsnum^post9, (witemsnum^0-witemsnum^post9 == 0 /\ -2+witemsnum^0 <= 0 /\ -___rho_1_^post9+___rho_1_^0 == 0 /\ -___rho_2_^post9+___rho_2_^0 == 0), cost: 1 10: l11 -> l8 : ___rho_1_^0'=___rho_1_^post11, ___rho_2_^0'=___rho_2_^post11, witemsnum^0'=witemsnum^post11, (-___rho_2_^post11+___rho_2_^0 == 0 /\ witemsnum^0-witemsnum^post11 == 0 /\ -___rho_1_^post11+___rho_1_^0 == 0), cost: 1 11: l12 -> l3 : ___rho_1_^0'=___rho_1_^post12, ___rho_2_^0'=___rho_2_^post12, witemsnum^0'=witemsnum^post12, (-1+witemsnum^post12-witemsnum^0 == 0 /\ -___rho_1_^post12+___rho_1_^0 == 0 /\ -___rho_2_^post12+___rho_2_^0 == 0 /\ 6-witemsnum^0 <= 0), cost: 1 12: l12 -> l3 : ___rho_1_^0'=___rho_1_^post13, ___rho_2_^0'=___rho_2_^post13, witemsnum^0'=witemsnum^post13, (-1-witemsnum^0+witemsnum^post13 == 0 /\ ___rho_1_^0-___rho_1_^post13 == 0 /\ -___rho_2_^post13+___rho_2_^0 == 0 /\ -5+witemsnum^0 <= 0), cost: 1 13: l13 -> l12 : ___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 /\ ___rho_2_^0 <= 0), cost: 1 14: l13 -> l9 : ___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 /\ 1-___rho_2_^0 <= 0), cost: 1 17: l14 -> l2 : ___rho_1_^0'=___rho_1_^post18, ___rho_2_^0'=___rho_2_^post18, witemsnum^0'=witemsnum^post18, (___rho_1_^0-___rho_1_^post18 == 0 /\ -witemsnum^post18+witemsnum^0 == 0 /\ -___rho_2_^post18+___rho_2_^0 == 0), cost: 1 18: l15 -> l2 : ___rho_1_^0'=___rho_1_^post19, ___rho_2_^0'=___rho_2_^post19, witemsnum^0'=witemsnum^post19, (-witemsnum^post19+witemsnum^0 == 0 /\ -witemsnum^0 <= 0 /\ ___rho_1_^0-___rho_1_^post19 == 0 /\ -___rho_2_^post19+___rho_2_^0 == 0), cost: 1 19: l15 -> l0 : ___rho_1_^0'=___rho_1_^post20, ___rho_2_^0'=___rho_2_^post20, witemsnum^0'=witemsnum^post20, (-___rho_2_^post20+___rho_2_^0 == 0 /\ -witemsnum^post20+witemsnum^0 == 0 /\ ___rho_1_^0-___rho_1_^post20 == 0 /\ 1+witemsnum^0 <= 0), cost: 1 22: l17 -> l15 : ___rho_1_^0'=___rho_1_^post21, ___rho_2_^0'=___rho_2_^post21, witemsnum^0'=witemsnum^post21, (0 == 0 /\ -___rho_2_^post22+___rho_2_^0 == 0 /\ -___rho_1_^post22+___rho_1_^0 == 0 /\ witemsnum^0-witemsnum^post22 == 0 /\ -___rho_1_^post21+witemsnum^post21 == 0 /\ ___rho_2_^post22-___rho_2_^post21 == 0), cost: 1 Eliminating location l16 by chaining: Applied chaining First rule: l17 -> l16 : ___rho_1_^0'=___rho_1_^post22, ___rho_2_^0'=___rho_2_^post22, witemsnum^0'=witemsnum^post22, (-___rho_2_^post22+___rho_2_^0 == 0 /\ -___rho_1_^post22+___rho_1_^0 == 0 /\ witemsnum^0-witemsnum^post22 == 0), cost: 1 Second rule: l16 -> l15 : ___rho_1_^0'=___rho_1_^post21, ___rho_2_^0'=___rho_2_^post21, witemsnum^0'=witemsnum^post21, (0 == 0 /\ -___rho_2_^post21+___rho_2_^0 == 0 /\ -___rho_1_^post21+witemsnum^post21 == 0), cost: 1 New rule: l17 -> l15 : ___rho_1_^0'=___rho_1_^post21, ___rho_2_^0'=___rho_2_^post21, witemsnum^0'=witemsnum^post21, (0 == 0 /\ -___rho_2_^post22+___rho_2_^0 == 0 /\ -___rho_1_^post22+___rho_1_^0 == 0 /\ witemsnum^0-witemsnum^post22 == 0 /\ -___rho_1_^post21+witemsnum^post21 == 0 /\ ___rho_2_^post22-___rho_2_^post21 == 0), cost: 1 Applied deletion Removed the following rules: 20 21 Eliminating location l1 by chaining: Applied chaining First 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 Second rule: l1 -> l0 : ___rho_1_^0'=___rho_1_^post2, ___rho_2_^0'=___rho_2_^post2, witemsnum^0'=witemsnum^post2, (-___rho_2_^post2+___rho_2_^0 == 0 /\ ___rho_1_^0-___rho_1_^post2 == 0 /\ -witemsnum^post2+witemsnum^0 == 0), cost: 1 New rule: l0 -> l0 : ___rho_1_^0'=___rho_1_^post2, ___rho_2_^0'=___rho_2_^post2, witemsnum^0'=witemsnum^post2, (-___rho_2_^post2+___rho_2_^post1 == 0 /\ -witemsnum^post2+witemsnum^post1 == 0 /\ -___rho_2_^post1+___rho_2_^0 == 0 /\ -___rho_1_^post2+___rho_1_^post1 == 0 /\ -witemsnum^post1+witemsnum^0 == 0 /\ ___rho_1_^0-___rho_1_^post1 == 0), cost: 1 Applied deletion Removed the following rules: 0 1 Simplified Transitions Start location: l17 Program variables: ___rho_1_^0 ___rho_2_^0 witemsnum^0 43: l0 -> l0 : T, cost: 1 24: l2 -> l3 : T, cost: 1 25: l3 -> l4 : ___rho_2_^0'=___rho_2_^post4, T, cost: 1 37: l4 -> l12 : 6-witemsnum^0 <= 0, cost: 1 38: l4 -> l13 : -5+witemsnum^0 <= 0, cost: 1 26: l5 -> l6 : T, cost: 1 27: l7 -> l8 : T, cost: 1 31: l8 -> l11 : T, cost: 1 28: l9 -> l10 : T, cost: 1 29: l10 -> l9 : witemsnum^0'=-1+witemsnum^0, 3-witemsnum^0 <= 0, cost: 1 30: l10 -> l2 : -2+witemsnum^0 <= 0, cost: 1 32: l11 -> l8 : T, cost: 1 33: l12 -> l3 : witemsnum^0'=1+witemsnum^0, 6-witemsnum^0 <= 0, cost: 1 34: l12 -> l3 : witemsnum^0'=1+witemsnum^0, -5+witemsnum^0 <= 0, cost: 1 35: l13 -> l12 : ___rho_2_^0 <= 0, cost: 1 36: l13 -> l9 : 1-___rho_2_^0 <= 0, cost: 1 39: l14 -> l2 : T, cost: 1 40: l15 -> l2 : -witemsnum^0 <= 0, cost: 1 41: l15 -> l0 : 1+witemsnum^0 <= 0, cost: 1 42: l17 -> l15 : ___rho_1_^0'=witemsnum^post21, witemsnum^0'=witemsnum^post21, T, cost: 1 Propagated Equalities Original rule: l2 -> l3 : ___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: l2 -> l3 : ___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: l2 -> l3 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, 0 == 0, cost: 1 New rule: l2 -> l3 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, T, cost: 1 Removed Trivial Updates Original rule: l2 -> l3 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, T, cost: 1 New rule: l2 -> l3 : T, cost: 1 Propagated Equalities Original rule: l3 -> l4 : ___rho_1_^0'=___rho_1_^post4, ___rho_2_^0'=___rho_2_^post4, witemsnum^0'=witemsnum^post4, (0 == 0 /\ -witemsnum^post4+witemsnum^0 == 0 /\ ___rho_1_^0-___rho_1_^post4 == 0), cost: 1 New rule: l3 -> l4 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^post4, witemsnum^0'=witemsnum^0, 0 == 0, cost: 1 propagated equality witemsnum^post4 = witemsnum^0 propagated equality ___rho_1_^post4 = ___rho_1_^0 Simplified Guard Original rule: l3 -> l4 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^post4, witemsnum^0'=witemsnum^0, 0 == 0, cost: 1 New rule: l3 -> l4 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^post4, 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_^post4, witemsnum^0'=witemsnum^0, T, cost: 1 New rule: l3 -> l4 : ___rho_2_^0'=___rho_2_^post4, T, cost: 1 Propagated Equalities Original rule: l5 -> l6 : ___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: l5 -> l6 : ___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: 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_^post6, ___rho_2_^0'=___rho_2_^post6, witemsnum^0'=witemsnum^post6, (___rho_1_^0-___rho_1_^post6 == 0 /\ -___rho_2_^post6+___rho_2_^0 == 0 /\ -witemsnum^post6+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_^post6 = ___rho_1_^0 propagated equality ___rho_2_^post6 = ___rho_2_^0 propagated equality witemsnum^post6 = 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: l9 -> l10 : ___rho_1_^0'=___rho_1_^post7, ___rho_2_^0'=___rho_2_^post7, witemsnum^0'=witemsnum^post7, (___rho_1_^0-___rho_1_^post7 == 0 /\ -___rho_2_^post7+___rho_2_^0 == 0 /\ -witemsnum^post7+witemsnum^0 == 0), cost: 1 New rule: l9 -> l10 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, 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: l9 -> l10 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, 0 == 0, cost: 1 New rule: l9 -> l10 : ___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 -> l10 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, T, cost: 1 New rule: l9 -> l10 : T, cost: 1 Propagated Equalities Original rule: l10 -> l9 : ___rho_1_^0'=___rho_1_^post8, ___rho_2_^0'=___rho_2_^post8, witemsnum^0'=witemsnum^post8, (3-witemsnum^0 <= 0 /\ 1-witemsnum^0+witemsnum^post8 == 0 /\ -___rho_2_^post8+___rho_2_^0 == 0 /\ ___rho_1_^0-___rho_1_^post8 == 0), cost: 1 New rule: l10 -> l9 : ___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 witemsnum^post8 = -1+witemsnum^0 propagated equality ___rho_2_^post8 = ___rho_2_^0 propagated equality ___rho_1_^post8 = ___rho_1_^0 Simplified Guard Original rule: l10 -> l9 : ___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: l10 -> l9 : ___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: l10 -> l9 : ___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: l10 -> l9 : witemsnum^0'=-1+witemsnum^0, 3-witemsnum^0 <= 0, cost: 1 Propagated Equalities Original rule: l10 -> l2 : ___rho_1_^0'=___rho_1_^post9, ___rho_2_^0'=___rho_2_^post9, witemsnum^0'=witemsnum^post9, (witemsnum^0-witemsnum^post9 == 0 /\ -2+witemsnum^0 <= 0 /\ -___rho_1_^post9+___rho_1_^0 == 0 /\ -___rho_2_^post9+___rho_2_^0 == 0), cost: 1 New rule: l10 -> l2 : ___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 witemsnum^post9 = witemsnum^0 propagated equality ___rho_1_^post9 = ___rho_1_^0 propagated equality ___rho_2_^post9 = ___rho_2_^0 Simplified Guard Original rule: l10 -> l2 : ___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: l10 -> l2 : ___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: l10 -> l2 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, -2+witemsnum^0 <= 0, cost: 1 New rule: l10 -> l2 : -2+witemsnum^0 <= 0, cost: 1 Propagated Equalities Original rule: l8 -> l11 : ___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 /\ witemsnum^0-witemsnum^post10 == 0), cost: 1 New rule: l8 -> l11 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, 0 == 0, cost: 1 propagated equality ___rho_2_^post10 = ___rho_2_^0 propagated equality ___rho_1_^post10 = ___rho_1_^0 propagated equality witemsnum^post10 = witemsnum^0 Simplified Guard Original rule: l8 -> l11 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, 0 == 0, cost: 1 New rule: l8 -> l11 : ___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 -> l11 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, T, cost: 1 New rule: l8 -> l11 : T, cost: 1 Propagated Equalities Original rule: l11 -> l8 : ___rho_1_^0'=___rho_1_^post11, ___rho_2_^0'=___rho_2_^post11, witemsnum^0'=witemsnum^post11, (-___rho_2_^post11+___rho_2_^0 == 0 /\ witemsnum^0-witemsnum^post11 == 0 /\ -___rho_1_^post11+___rho_1_^0 == 0), cost: 1 New rule: l11 -> l8 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, 0 == 0, cost: 1 propagated equality ___rho_2_^post11 = ___rho_2_^0 propagated equality witemsnum^post11 = witemsnum^0 propagated equality ___rho_1_^post11 = ___rho_1_^0 Simplified Guard Original rule: l11 -> l8 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, 0 == 0, cost: 1 New rule: l11 -> 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: l11 -> l8 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, T, cost: 1 New rule: l11 -> l8 : T, cost: 1 Propagated Equalities Original rule: l12 -> l3 : ___rho_1_^0'=___rho_1_^post12, ___rho_2_^0'=___rho_2_^post12, witemsnum^0'=witemsnum^post12, (-1+witemsnum^post12-witemsnum^0 == 0 /\ -___rho_1_^post12+___rho_1_^0 == 0 /\ -___rho_2_^post12+___rho_2_^0 == 0 /\ 6-witemsnum^0 <= 0), cost: 1 New rule: l12 -> l3 : ___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 witemsnum^post12 = 1+witemsnum^0 propagated equality ___rho_1_^post12 = ___rho_1_^0 propagated equality ___rho_2_^post12 = ___rho_2_^0 Simplified Guard Original rule: l12 -> l3 : ___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: l12 -> l3 : ___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: l12 -> l3 : ___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: l12 -> l3 : witemsnum^0'=1+witemsnum^0, 6-witemsnum^0 <= 0, cost: 1 Propagated Equalities Original rule: l12 -> l3 : ___rho_1_^0'=___rho_1_^post13, ___rho_2_^0'=___rho_2_^post13, witemsnum^0'=witemsnum^post13, (-1-witemsnum^0+witemsnum^post13 == 0 /\ ___rho_1_^0-___rho_1_^post13 == 0 /\ -___rho_2_^post13+___rho_2_^0 == 0 /\ -5+witemsnum^0 <= 0), cost: 1 New rule: l12 -> l3 : ___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^post13 = 1+witemsnum^0 propagated equality ___rho_1_^post13 = ___rho_1_^0 propagated equality ___rho_2_^post13 = ___rho_2_^0 Simplified Guard Original rule: l12 -> l3 : ___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: l12 -> l3 : ___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: l12 -> l3 : ___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: l12 -> l3 : witemsnum^0'=1+witemsnum^0, -5+witemsnum^0 <= 0, cost: 1 Propagated Equalities Original rule: l13 -> l12 : ___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 /\ ___rho_2_^0 <= 0), cost: 1 New rule: l13 -> l12 : ___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 witemsnum^post14 = witemsnum^0 propagated equality ___rho_1_^post14 = ___rho_1_^0 propagated equality ___rho_2_^post14 = ___rho_2_^0 Simplified Guard Original rule: l13 -> l12 : ___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: l13 -> l12 : ___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: l13 -> l12 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, ___rho_2_^0 <= 0, cost: 1 New rule: l13 -> l12 : ___rho_2_^0 <= 0, cost: 1 Propagated Equalities Original rule: l13 -> l9 : ___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 /\ 1-___rho_2_^0 <= 0), cost: 1 New rule: l13 -> l9 : ___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_2_^post15 = ___rho_2_^0 propagated equality witemsnum^post15 = witemsnum^0 propagated equality ___rho_1_^post15 = ___rho_1_^0 Simplified Guard Original rule: l13 -> l9 : ___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: l13 -> l9 : ___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: l13 -> l9 : ___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: l13 -> l9 : 1-___rho_2_^0 <= 0, cost: 1 Propagated Equalities Original rule: l4 -> l12 : ___rho_1_^0'=___rho_1_^post16, ___rho_2_^0'=___rho_2_^post16, witemsnum^0'=witemsnum^post16, (-___rho_2_^post16+___rho_2_^0 == 0 /\ -witemsnum^post16+witemsnum^0 == 0 /\ 6-witemsnum^0 <= 0 /\ ___rho_1_^0-___rho_1_^post16 == 0), cost: 1 New rule: l4 -> l12 : ___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 ___rho_2_^post16 = ___rho_2_^0 propagated equality witemsnum^post16 = witemsnum^0 propagated equality ___rho_1_^post16 = ___rho_1_^0 Simplified Guard Original rule: l4 -> l12 : ___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: l4 -> l12 : ___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: l4 -> l12 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, 6-witemsnum^0 <= 0, cost: 1 New rule: l4 -> l12 : 6-witemsnum^0 <= 0, cost: 1 Propagated Equalities Original rule: l4 -> l13 : ___rho_1_^0'=___rho_1_^post17, ___rho_2_^0'=___rho_2_^post17, witemsnum^0'=witemsnum^post17, (-___rho_2_^post17+___rho_2_^0 == 0 /\ ___rho_1_^0-___rho_1_^post17 == 0 /\ -witemsnum^post17+witemsnum^0 == 0 /\ -5+witemsnum^0 <= 0), cost: 1 New rule: l4 -> l13 : ___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_^post17 = ___rho_2_^0 propagated equality ___rho_1_^post17 = ___rho_1_^0 propagated equality witemsnum^post17 = witemsnum^0 Simplified Guard Original rule: l4 -> l13 : ___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: l4 -> l13 : ___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: l4 -> l13 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, -5+witemsnum^0 <= 0, cost: 1 New rule: l4 -> l13 : -5+witemsnum^0 <= 0, cost: 1 Propagated Equalities Original rule: l14 -> l2 : ___rho_1_^0'=___rho_1_^post18, ___rho_2_^0'=___rho_2_^post18, witemsnum^0'=witemsnum^post18, (___rho_1_^0-___rho_1_^post18 == 0 /\ -witemsnum^post18+witemsnum^0 == 0 /\ -___rho_2_^post18+___rho_2_^0 == 0), cost: 1 New rule: l14 -> l2 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, 0 == 0, cost: 1 propagated equality ___rho_1_^post18 = ___rho_1_^0 propagated equality witemsnum^post18 = witemsnum^0 propagated equality ___rho_2_^post18 = ___rho_2_^0 Simplified Guard Original rule: l14 -> l2 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, 0 == 0, cost: 1 New rule: l14 -> l2 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, T, cost: 1 Removed Trivial Updates Original rule: l14 -> l2 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, T, cost: 1 New rule: l14 -> l2 : T, cost: 1 Propagated Equalities Original rule: l15 -> l2 : ___rho_1_^0'=___rho_1_^post19, ___rho_2_^0'=___rho_2_^post19, witemsnum^0'=witemsnum^post19, (-witemsnum^post19+witemsnum^0 == 0 /\ -witemsnum^0 <= 0 /\ ___rho_1_^0-___rho_1_^post19 == 0 /\ -___rho_2_^post19+___rho_2_^0 == 0), cost: 1 New rule: l15 -> l2 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, (0 == 0 /\ -witemsnum^0 <= 0), cost: 1 propagated equality witemsnum^post19 = witemsnum^0 propagated equality ___rho_1_^post19 = ___rho_1_^0 propagated equality ___rho_2_^post19 = ___rho_2_^0 Simplified Guard Original rule: l15 -> l2 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, (0 == 0 /\ -witemsnum^0 <= 0), cost: 1 New rule: l15 -> l2 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, -witemsnum^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l15 -> l2 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, -witemsnum^0 <= 0, cost: 1 New rule: l15 -> l2 : -witemsnum^0 <= 0, cost: 1 Propagated Equalities Original rule: l15 -> l0 : ___rho_1_^0'=___rho_1_^post20, ___rho_2_^0'=___rho_2_^post20, witemsnum^0'=witemsnum^post20, (-___rho_2_^post20+___rho_2_^0 == 0 /\ -witemsnum^post20+witemsnum^0 == 0 /\ ___rho_1_^0-___rho_1_^post20 == 0 /\ 1+witemsnum^0 <= 0), cost: 1 New rule: l15 -> l0 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, (0 == 0 /\ 1+witemsnum^0 <= 0), cost: 1 propagated equality ___rho_2_^post20 = ___rho_2_^0 propagated equality witemsnum^post20 = witemsnum^0 propagated equality ___rho_1_^post20 = ___rho_1_^0 Simplified Guard Original rule: l15 -> l0 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, (0 == 0 /\ 1+witemsnum^0 <= 0), cost: 1 New rule: l15 -> l0 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, 1+witemsnum^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l15 -> l0 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, 1+witemsnum^0 <= 0, cost: 1 New rule: l15 -> l0 : 1+witemsnum^0 <= 0, cost: 1 Propagated Equalities Original rule: l17 -> l15 : ___rho_1_^0'=___rho_1_^post21, ___rho_2_^0'=___rho_2_^post21, witemsnum^0'=witemsnum^post21, (0 == 0 /\ -___rho_2_^post22+___rho_2_^0 == 0 /\ -___rho_1_^post22+___rho_1_^0 == 0 /\ witemsnum^0-witemsnum^post22 == 0 /\ -___rho_1_^post21+witemsnum^post21 == 0 /\ ___rho_2_^post22-___rho_2_^post21 == 0), cost: 1 New rule: l17 -> l15 : ___rho_1_^0'=witemsnum^post21, ___rho_2_^0'=___rho_2_^post22, witemsnum^0'=witemsnum^post21, (0 == 0 /\ -___rho_2_^post22+___rho_2_^0 == 0 /\ -___rho_1_^post22+___rho_1_^0 == 0 /\ witemsnum^0-witemsnum^post22 == 0), cost: 1 propagated equality ___rho_1_^post21 = witemsnum^post21 propagated equality ___rho_2_^post21 = ___rho_2_^post22 Propagated Equalities Original rule: l17 -> l15 : ___rho_1_^0'=witemsnum^post21, ___rho_2_^0'=___rho_2_^post22, witemsnum^0'=witemsnum^post21, (0 == 0 /\ -___rho_2_^post22+___rho_2_^0 == 0 /\ -___rho_1_^post22+___rho_1_^0 == 0 /\ witemsnum^0-witemsnum^post22 == 0), cost: 1 New rule: l17 -> l15 : ___rho_1_^0'=witemsnum^post21, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^post21, 0 == 0, cost: 1 propagated equality ___rho_2_^post22 = ___rho_2_^0 propagated equality ___rho_1_^post22 = ___rho_1_^0 propagated equality witemsnum^post22 = witemsnum^0 Simplified Guard Original rule: l17 -> l15 : ___rho_1_^0'=witemsnum^post21, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^post21, 0 == 0, cost: 1 New rule: l17 -> l15 : ___rho_1_^0'=witemsnum^post21, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^post21, T, cost: 1 Removed Trivial Updates Original rule: l17 -> l15 : ___rho_1_^0'=witemsnum^post21, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^post21, T, cost: 1 New rule: l17 -> l15 : ___rho_1_^0'=witemsnum^post21, witemsnum^0'=witemsnum^post21, T, cost: 1 Propagated Equalities Original rule: l0 -> l0 : ___rho_1_^0'=___rho_1_^post2, ___rho_2_^0'=___rho_2_^post2, witemsnum^0'=witemsnum^post2, (-___rho_2_^post2+___rho_2_^post1 == 0 /\ -witemsnum^post2+witemsnum^post1 == 0 /\ -___rho_2_^post1+___rho_2_^0 == 0 /\ -___rho_1_^post2+___rho_1_^post1 == 0 /\ -witemsnum^post1+witemsnum^0 == 0 /\ ___rho_1_^0-___rho_1_^post1 == 0), cost: 1 New rule: l0 -> l0 : ___rho_1_^0'=___rho_1_^post1, ___rho_2_^0'=___rho_2_^post1, witemsnum^0'=witemsnum^post1, (0 == 0 /\ -___rho_2_^post1+___rho_2_^0 == 0 /\ -witemsnum^post1+witemsnum^0 == 0 /\ ___rho_1_^0-___rho_1_^post1 == 0), cost: 1 propagated equality ___rho_2_^post2 = ___rho_2_^post1 propagated equality witemsnum^post2 = witemsnum^post1 propagated equality ___rho_1_^post2 = ___rho_1_^post1 Propagated Equalities Original rule: l0 -> l0 : ___rho_1_^0'=___rho_1_^post1, ___rho_2_^0'=___rho_2_^post1, witemsnum^0'=witemsnum^post1, (0 == 0 /\ -___rho_2_^post1+___rho_2_^0 == 0 /\ -witemsnum^post1+witemsnum^0 == 0 /\ ___rho_1_^0-___rho_1_^post1 == 0), cost: 1 New rule: l0 -> l0 : ___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 -> l0 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, 0 == 0, cost: 1 New rule: l0 -> l0 : ___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 -> l0 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, witemsnum^0'=witemsnum^0, T, cost: 1 New rule: l0 -> l0 : T, cost: 1 Step with 42 Trace 42[T] Blocked [{}, {}] Step with 40 Trace 42[T], 40[(-witemsnum^0 <= 0)] Blocked [{}, {}, {}] Step with 24 Trace 42[T], 40[(-witemsnum^0 <= 0)], 24[T] Blocked [{}, {}, {}, {}] Step with 25 Trace 42[T], 40[(-witemsnum^0 <= 0)], 24[T], 25[T] Blocked [{}, {}, {}, {}, {}] Step with 37 Trace 42[T], 40[(-witemsnum^0 <= 0)], 24[T], 25[T], 37[(6-witemsnum^0 <= 0)] Blocked [{}, {}, {}, {}, {}, {}] Step with 33 Trace 42[T], 40[(-witemsnum^0 <= 0)], 24[T], 25[T], 37[(6-witemsnum^0 <= 0)], 33[(6-witemsnum^0 <= 0)] Blocked [{}, {}, {}, {}, {}, {}, {}] Nonterm Start location: l17 Program variables: ___rho_1_^0 ___rho_2_^0 witemsnum^0 43: l0 -> l0 : T, cost: 1 24: l2 -> l3 : T, cost: 1 25: l3 -> l4 : ___rho_2_^0'=___rho_2_^post4, T, cost: 1 44: l3 -> LoAT_sink : (-1+n >= 0 /\ -6+witemsnum^0 >= 0), cost: NONTERM 45: l3 -> l3 : ___rho_2_^0'=___rho_2_^post41, witemsnum^0'=n+witemsnum^0, (-1+n >= 0 /\ -6+witemsnum^0 >= 0), cost: 1 37: l4 -> l12 : 6-witemsnum^0 <= 0, cost: 1 38: l4 -> l13 : -5+witemsnum^0 <= 0, cost: 1 26: l5 -> l6 : T, cost: 1 27: l7 -> l8 : T, cost: 1 31: l8 -> l11 : T, cost: 1 28: l9 -> l10 : T, cost: 1 29: l10 -> l9 : witemsnum^0'=-1+witemsnum^0, 3-witemsnum^0 <= 0, cost: 1 30: l10 -> l2 : -2+witemsnum^0 <= 0, cost: 1 32: l11 -> l8 : T, cost: 1 33: l12 -> l3 : witemsnum^0'=1+witemsnum^0, 6-witemsnum^0 <= 0, cost: 1 34: l12 -> l3 : witemsnum^0'=1+witemsnum^0, -5+witemsnum^0 <= 0, cost: 1 35: l13 -> l12 : ___rho_2_^0 <= 0, cost: 1 36: l13 -> l9 : 1-___rho_2_^0 <= 0, cost: 1 39: l14 -> l2 : T, cost: 1 40: l15 -> l2 : -witemsnum^0 <= 0, cost: 1 41: l15 -> l0 : 1+witemsnum^0 <= 0, cost: 1 42: l17 -> l15 : ___rho_1_^0'=witemsnum^post21, witemsnum^0'=witemsnum^post21, T, cost: 1 Certificate of Non-Termination Original rule: l3 -> l3 : ___rho_2_^0'=___rho_2_^post41, witemsnum^0'=1+witemsnum^0, 6-witemsnum^0 <= 0, cost: 1 New rule: l3 -> 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: l3 -> l3 : ___rho_2_^0'=___rho_2_^post41, witemsnum^0'=1+witemsnum^0, 6-witemsnum^0 <= 0, cost: 1 New rule: l3 -> l3 : ___rho_2_^0'=___rho_2_^post41, 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 44 Trace 42[T], 40[(-witemsnum^0 <= 0)], 24[T], 44[(-1+n >= 0 /\ -6+witemsnum^0 >= 0)] Blocked [{}, {}, {}, {}, {44[T]}] Refute Counterexample [ ___rho_1_^0=6 ___rho_2_^0=0 witemsnum^0=6 ] 42 [ ___rho_1_^0=6 ___rho_2_^0=0 witemsnum^0=6 ] 40 [ ___rho_1_^0=6 ___rho_2_^0=0 witemsnum^0=6 ] 24 [ ___rho_1_^0=___rho_1_^0 ___rho_2_^0=0 witemsnum^0=witemsnum^0 ] 44 NO Build SHA: a05f16bf13df659c382799650051f91bf6828c7b