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