NO Initial ITS Start location: l18 Program variables: result_4^0 w_5^0 x_6^0 0: l0 -> l2 : result_4^0'=result_4^post1, w_5^0'=w_5^post1, x_6^0'=x_6^post1, (-2+w_5^0 <= 0 /\ -1+x_6^post1-x_6^0 == 0 /\ 2-x_6^0 <= 0 /\ -result_4^post1+result_4^0 == 0 /\ -1+w_5^post1-w_5^0 == 0), cost: 1 6: l0 -> l5 : result_4^0'=result_4^post7, w_5^0'=w_5^post7, x_6^0'=x_6^post7, (-1+w_5^post7-w_5^0 == 0 /\ -2+w_5^0 <= 0 /\ 2-x_6^0 <= 0 /\ -1+x_6^post7-x_6^0 == 0 /\ -result_4^post7+result_4^0 == 0), cost: 1 11: l0 -> l8 : result_4^0'=result_4^post12, w_5^0'=w_5^post12, x_6^0'=x_6^post12, (-1+w_5^post12-w_5^0 == 0 /\ -1+x_6^0 <= 0 /\ -1+x_6^post12-x_6^0 == 0 /\ -result_4^post12+result_4^0 == 0), cost: 1 17: l0 -> l11 : result_4^0'=result_4^post18, w_5^0'=w_5^post18, x_6^0'=x_6^post18, (-result_4^post18+result_4^0 == 0 /\ -1+w_5^post18-w_5^0 == 0 /\ -1+x_6^0 <= 0 /\ -1+x_6^post18-x_6^0 == 0), cost: 1 22: l0 -> l14 : result_4^0'=result_4^post23, w_5^0'=w_5^post23, x_6^0'=x_6^post23, (-result_4^post23+result_4^0 == 0 /\ -1+x_6^0 <= 0 /\ -2+x_6^post23 <= 0 /\ -1+x_6^post23-x_6^0 == 0 /\ -1-w_5^0+w_5^post23 == 0 /\ 2-x_6^post23 <= 0), cost: 1 26: l0 -> l15 : result_4^0'=result_4^post27, w_5^0'=w_5^post27, x_6^0'=x_6^post27, (-2+w_5^1 <= 0 /\ -2+x_6^post27 <= 0 /\ -1+w_5^post27 == 0 /\ -1+x_6^post27-x_6^0 == 0 /\ -1+x_6^0 <= 0 /\ 2-w_5^1 <= 0 /\ 2-x_6^post27 <= 0 /\ -1+w_5^1-w_5^0 == 0 /\ -result_4^post27+result_4^0 == 0), cost: 1 28: l0 -> l16 : result_4^0'=result_4^post29, w_5^0'=w_5^post29, x_6^0'=x_6^post29, (0 == 0 /\ 2-x_6^0 <= 0 /\ 3-w_5^0 <= 0 /\ -w_5^post29+w_5^0 == 0 /\ -x_6^post29+x_6^0 == 0), cost: 1 1: l2 -> l3 : result_4^0'=result_4^post2, w_5^0'=w_5^post2, x_6^0'=x_6^post2, (-1+x_6^0 <= 0 /\ -w_5^post2+w_5^0 == 0 /\ -x_6^post2+x_6^0 == 0 /\ -result_4^post2+result_4^0 == 0), cost: 1 2: l2 -> l3 : result_4^0'=result_4^post3, w_5^0'=w_5^post3, x_6^0'=x_6^post3, (3-x_6^0 <= 0 /\ -w_5^post3+w_5^0 == 0 /\ -result_4^post3+result_4^0 == 0 /\ -x_6^post3+x_6^0 == 0), cost: 1 3: l3 -> l1 : result_4^0'=result_4^post4, w_5^0'=w_5^post4, x_6^0'=x_6^post4, (-x_6^post4+x_6^0 == 0 /\ -result_4^post4+result_4^0 == 0 /\ -w_5^post4+w_5^0 == 0 /\ -1+w_5^0 <= 0), cost: 1 4: l3 -> l1 : result_4^0'=result_4^post5, w_5^0'=w_5^post5, x_6^0'=x_6^post5, (-w_5^post5+w_5^0 == 0 /\ -x_6^post5+x_6^0 == 0 /\ -result_4^post5+result_4^0 == 0 /\ 3-w_5^0 <= 0), cost: 1 5: l1 -> l0 : result_4^0'=result_4^post6, w_5^0'=w_5^post6, x_6^0'=x_6^post6, (-w_5^post6+w_5^0 == 0 /\ -result_4^post6+result_4^0 == 0 /\ -x_6^post6+x_6^0 == 0), cost: 1 7: l5 -> l6 : result_4^0'=result_4^post8, w_5^0'=w_5^post8, x_6^0'=x_6^post8, (x_6^0-x_6^post8 == 0 /\ -result_4^post8+result_4^0 == 0 /\ -w_5^post8+w_5^0 == 0 /\ -1+x_6^0 <= 0), cost: 1 8: l5 -> l6 : result_4^0'=result_4^post9, w_5^0'=w_5^post9, x_6^0'=x_6^post9, (3-x_6^0 <= 0 /\ x_6^0-x_6^post9 == 0 /\ -w_5^post9+w_5^0 == 0 /\ -result_4^post9+result_4^0 == 0), cost: 1 9: l6 -> l4 : result_4^0'=result_4^post10, w_5^0'=w_5^post10, x_6^0'=x_6^post10, (-2+w_5^0 <= 0 /\ -result_4^post10+result_4^0 == 0 /\ x_6^0-x_6^post10 == 0 /\ 2-w_5^0 <= 0 /\ -1+w_5^post10 == 0), cost: 1 10: l4 -> l0 : result_4^0'=result_4^post11, w_5^0'=w_5^post11, x_6^0'=x_6^post11, (-w_5^post11+w_5^0 == 0 /\ -result_4^post11+result_4^0 == 0 /\ x_6^0-x_6^post11 == 0), cost: 1 12: l8 -> l9 : result_4^0'=result_4^post13, w_5^0'=w_5^post13, x_6^0'=x_6^post13, (result_4^0-result_4^post13 == 0 /\ -1+x_6^0 <= 0 /\ x_6^0-x_6^post13 == 0 /\ -w_5^post13+w_5^0 == 0), cost: 1 13: l8 -> l9 : result_4^0'=result_4^post14, w_5^0'=w_5^post14, x_6^0'=x_6^post14, (-x_6^post14+x_6^0 == 0 /\ 3-x_6^0 <= 0 /\ result_4^0-result_4^post14 == 0 /\ -w_5^post14+w_5^0 == 0), cost: 1 14: l9 -> l7 : result_4^0'=result_4^post15, w_5^0'=w_5^post15, x_6^0'=x_6^post15, (result_4^0-result_4^post15 == 0 /\ -w_5^post15+w_5^0 == 0 /\ -x_6^post15+x_6^0 == 0 /\ -1+w_5^0 <= 0), cost: 1 15: l9 -> l7 : result_4^0'=result_4^post16, w_5^0'=w_5^post16, x_6^0'=x_6^post16, (-w_5^post16+w_5^0 == 0 /\ -x_6^post16+x_6^0 == 0 /\ -result_4^post16+result_4^0 == 0 /\ 3-w_5^0 <= 0), cost: 1 16: l7 -> l0 : result_4^0'=result_4^post17, w_5^0'=w_5^post17, x_6^0'=x_6^post17, (-w_5^post17+w_5^0 == 0 /\ -x_6^post17+x_6^0 == 0 /\ -result_4^post17+result_4^0 == 0), cost: 1 18: l11 -> l12 : result_4^0'=result_4^post19, w_5^0'=w_5^post19, x_6^0'=x_6^post19, (-x_6^post19+x_6^0 == 0 /\ result_4^0-result_4^post19 == 0 /\ -1+x_6^0 <= 0 /\ -w_5^post19+w_5^0 == 0), cost: 1 19: l11 -> l12 : result_4^0'=result_4^post20, w_5^0'=w_5^post20, x_6^0'=x_6^post20, (-w_5^post20+w_5^0 == 0 /\ 3-x_6^0 <= 0 /\ -result_4^post20+result_4^0 == 0 /\ -x_6^post20+x_6^0 == 0), cost: 1 20: l12 -> l10 : result_4^0'=result_4^post21, w_5^0'=w_5^post21, x_6^0'=x_6^post21, (-2+w_5^0 <= 0 /\ -1+w_5^post21 == 0 /\ 2-w_5^0 <= 0 /\ -x_6^post21+x_6^0 == 0 /\ -result_4^post21+result_4^0 == 0), cost: 1 21: l10 -> l0 : result_4^0'=result_4^post22, w_5^0'=w_5^post22, x_6^0'=x_6^post22, (-x_6^post22+x_6^0 == 0 /\ -result_4^post22+result_4^0 == 0 /\ -w_5^post22+w_5^0 == 0), cost: 1 23: l14 -> l13 : result_4^0'=result_4^post24, w_5^0'=w_5^post24, x_6^0'=x_6^post24, (-x_6^post24+x_6^0 == 0 /\ -result_4^post24+result_4^0 == 0 /\ -w_5^post24+w_5^0 == 0 /\ -1+w_5^0 <= 0), cost: 1 24: l14 -> l13 : result_4^0'=result_4^post25, w_5^0'=w_5^post25, x_6^0'=x_6^post25, (-w_5^post25+w_5^0 == 0 /\ -result_4^post25+result_4^0 == 0 /\ -x_6^post25+x_6^0 == 0 /\ 3-w_5^0 <= 0), cost: 1 25: l13 -> l0 : result_4^0'=result_4^post26, w_5^0'=w_5^post26, x_6^0'=x_6^post26, (-w_5^post26+w_5^0 == 0 /\ -result_4^post26+result_4^0 == 0 /\ -x_6^post26+x_6^0 == 0), cost: 1 27: l15 -> l0 : result_4^0'=result_4^post28, w_5^0'=w_5^post28, x_6^0'=x_6^post28, (-x_6^post28+x_6^0 == 0 /\ -result_4^post28+result_4^0 == 0 /\ -w_5^post28+w_5^0 == 0), cost: 1 29: l17 -> l0 : result_4^0'=result_4^post30, w_5^0'=w_5^post30, x_6^0'=x_6^post30, (-result_4^post30+result_4^0 == 0 /\ -x_6^post30+x_6^0 == 0 /\ -w_5^post30+w_5^0 == 0), cost: 1 30: l18 -> l17 : result_4^0'=result_4^post31, w_5^0'=w_5^post31, x_6^0'=x_6^post31, (-w_5^post31+w_5^0 == 0 /\ -x_6^post31+x_6^0 == 0 /\ -result_4^post31+result_4^0 == 0), cost: 1 Chained Linear Paths Start location: l18 Program variables: result_4^0 w_5^0 x_6^0 0: l0 -> l2 : result_4^0'=result_4^post1, w_5^0'=w_5^post1, x_6^0'=x_6^post1, (-2+w_5^0 <= 0 /\ -1+x_6^post1-x_6^0 == 0 /\ 2-x_6^0 <= 0 /\ -result_4^post1+result_4^0 == 0 /\ -1+w_5^post1-w_5^0 == 0), cost: 1 6: l0 -> l5 : result_4^0'=result_4^post7, w_5^0'=w_5^post7, x_6^0'=x_6^post7, (-1+w_5^post7-w_5^0 == 0 /\ -2+w_5^0 <= 0 /\ 2-x_6^0 <= 0 /\ -1+x_6^post7-x_6^0 == 0 /\ -result_4^post7+result_4^0 == 0), cost: 1 11: l0 -> l8 : result_4^0'=result_4^post12, w_5^0'=w_5^post12, x_6^0'=x_6^post12, (-1+w_5^post12-w_5^0 == 0 /\ -1+x_6^0 <= 0 /\ -1+x_6^post12-x_6^0 == 0 /\ -result_4^post12+result_4^0 == 0), cost: 1 17: l0 -> l11 : result_4^0'=result_4^post18, w_5^0'=w_5^post18, x_6^0'=x_6^post18, (-result_4^post18+result_4^0 == 0 /\ -1+w_5^post18-w_5^0 == 0 /\ -1+x_6^0 <= 0 /\ -1+x_6^post18-x_6^0 == 0), cost: 1 22: l0 -> l14 : result_4^0'=result_4^post23, w_5^0'=w_5^post23, x_6^0'=x_6^post23, (-result_4^post23+result_4^0 == 0 /\ -1+x_6^0 <= 0 /\ -2+x_6^post23 <= 0 /\ -1+x_6^post23-x_6^0 == 0 /\ -1-w_5^0+w_5^post23 == 0 /\ 2-x_6^post23 <= 0), cost: 1 28: l0 -> l16 : result_4^0'=result_4^post29, w_5^0'=w_5^post29, x_6^0'=x_6^post29, (0 == 0 /\ 2-x_6^0 <= 0 /\ 3-w_5^0 <= 0 /\ -w_5^post29+w_5^0 == 0 /\ -x_6^post29+x_6^0 == 0), cost: 1 32: l0 -> l0 : result_4^0'=result_4^post28, w_5^0'=w_5^post28, x_6^0'=x_6^post28, (-2+w_5^1 <= 0 /\ -2+x_6^post27 <= 0 /\ -w_5^post28+w_5^post27 == 0 /\ -1+w_5^post27 == 0 /\ -result_4^post28+result_4^post27 == 0 /\ -1+x_6^post27-x_6^0 == 0 /\ -1+x_6^0 <= 0 /\ 2-w_5^1 <= 0 /\ -x_6^post28+x_6^post27 == 0 /\ 2-x_6^post27 <= 0 /\ -1+w_5^1-w_5^0 == 0 /\ -result_4^post27+result_4^0 == 0), cost: 1 1: l2 -> l3 : result_4^0'=result_4^post2, w_5^0'=w_5^post2, x_6^0'=x_6^post2, (-1+x_6^0 <= 0 /\ -w_5^post2+w_5^0 == 0 /\ -x_6^post2+x_6^0 == 0 /\ -result_4^post2+result_4^0 == 0), cost: 1 2: l2 -> l3 : result_4^0'=result_4^post3, w_5^0'=w_5^post3, x_6^0'=x_6^post3, (3-x_6^0 <= 0 /\ -w_5^post3+w_5^0 == 0 /\ -result_4^post3+result_4^0 == 0 /\ -x_6^post3+x_6^0 == 0), cost: 1 3: l3 -> l1 : result_4^0'=result_4^post4, w_5^0'=w_5^post4, x_6^0'=x_6^post4, (-x_6^post4+x_6^0 == 0 /\ -result_4^post4+result_4^0 == 0 /\ -w_5^post4+w_5^0 == 0 /\ -1+w_5^0 <= 0), cost: 1 4: l3 -> l1 : result_4^0'=result_4^post5, w_5^0'=w_5^post5, x_6^0'=x_6^post5, (-w_5^post5+w_5^0 == 0 /\ -x_6^post5+x_6^0 == 0 /\ -result_4^post5+result_4^0 == 0 /\ 3-w_5^0 <= 0), cost: 1 5: l1 -> l0 : result_4^0'=result_4^post6, w_5^0'=w_5^post6, x_6^0'=x_6^post6, (-w_5^post6+w_5^0 == 0 /\ -result_4^post6+result_4^0 == 0 /\ -x_6^post6+x_6^0 == 0), cost: 1 7: l5 -> l6 : result_4^0'=result_4^post8, w_5^0'=w_5^post8, x_6^0'=x_6^post8, (x_6^0-x_6^post8 == 0 /\ -result_4^post8+result_4^0 == 0 /\ -w_5^post8+w_5^0 == 0 /\ -1+x_6^0 <= 0), cost: 1 8: l5 -> l6 : result_4^0'=result_4^post9, w_5^0'=w_5^post9, x_6^0'=x_6^post9, (3-x_6^0 <= 0 /\ x_6^0-x_6^post9 == 0 /\ -w_5^post9+w_5^0 == 0 /\ -result_4^post9+result_4^0 == 0), cost: 1 33: l6 -> l0 : result_4^0'=result_4^post11, w_5^0'=w_5^post11, x_6^0'=x_6^post11, (-2+w_5^0 <= 0 /\ -result_4^post11+result_4^post10 == 0 /\ -result_4^post10+result_4^0 == 0 /\ -x_6^post11+x_6^post10 == 0 /\ x_6^0-x_6^post10 == 0 /\ -w_5^post11+w_5^post10 == 0 /\ 2-w_5^0 <= 0 /\ -1+w_5^post10 == 0), cost: 1 12: l8 -> l9 : result_4^0'=result_4^post13, w_5^0'=w_5^post13, x_6^0'=x_6^post13, (result_4^0-result_4^post13 == 0 /\ -1+x_6^0 <= 0 /\ x_6^0-x_6^post13 == 0 /\ -w_5^post13+w_5^0 == 0), cost: 1 13: l8 -> l9 : result_4^0'=result_4^post14, w_5^0'=w_5^post14, x_6^0'=x_6^post14, (-x_6^post14+x_6^0 == 0 /\ 3-x_6^0 <= 0 /\ result_4^0-result_4^post14 == 0 /\ -w_5^post14+w_5^0 == 0), cost: 1 14: l9 -> l7 : result_4^0'=result_4^post15, w_5^0'=w_5^post15, x_6^0'=x_6^post15, (result_4^0-result_4^post15 == 0 /\ -w_5^post15+w_5^0 == 0 /\ -x_6^post15+x_6^0 == 0 /\ -1+w_5^0 <= 0), cost: 1 15: l9 -> l7 : result_4^0'=result_4^post16, w_5^0'=w_5^post16, x_6^0'=x_6^post16, (-w_5^post16+w_5^0 == 0 /\ -x_6^post16+x_6^0 == 0 /\ -result_4^post16+result_4^0 == 0 /\ 3-w_5^0 <= 0), cost: 1 16: l7 -> l0 : result_4^0'=result_4^post17, w_5^0'=w_5^post17, x_6^0'=x_6^post17, (-w_5^post17+w_5^0 == 0 /\ -x_6^post17+x_6^0 == 0 /\ -result_4^post17+result_4^0 == 0), cost: 1 18: l11 -> l12 : result_4^0'=result_4^post19, w_5^0'=w_5^post19, x_6^0'=x_6^post19, (-x_6^post19+x_6^0 == 0 /\ result_4^0-result_4^post19 == 0 /\ -1+x_6^0 <= 0 /\ -w_5^post19+w_5^0 == 0), cost: 1 19: l11 -> l12 : result_4^0'=result_4^post20, w_5^0'=w_5^post20, x_6^0'=x_6^post20, (-w_5^post20+w_5^0 == 0 /\ 3-x_6^0 <= 0 /\ -result_4^post20+result_4^0 == 0 /\ -x_6^post20+x_6^0 == 0), cost: 1 34: l12 -> l0 : result_4^0'=result_4^post22, w_5^0'=w_5^post22, x_6^0'=x_6^post22, (-2+w_5^0 <= 0 /\ -1+w_5^post21 == 0 /\ -w_5^post22+w_5^post21 == 0 /\ -result_4^post22+result_4^post21 == 0 /\ 2-w_5^0 <= 0 /\ -x_6^post22+x_6^post21 == 0 /\ -x_6^post21+x_6^0 == 0 /\ -result_4^post21+result_4^0 == 0), cost: 1 23: l14 -> l13 : result_4^0'=result_4^post24, w_5^0'=w_5^post24, x_6^0'=x_6^post24, (-x_6^post24+x_6^0 == 0 /\ -result_4^post24+result_4^0 == 0 /\ -w_5^post24+w_5^0 == 0 /\ -1+w_5^0 <= 0), cost: 1 24: l14 -> l13 : result_4^0'=result_4^post25, w_5^0'=w_5^post25, x_6^0'=x_6^post25, (-w_5^post25+w_5^0 == 0 /\ -result_4^post25+result_4^0 == 0 /\ -x_6^post25+x_6^0 == 0 /\ 3-w_5^0 <= 0), cost: 1 25: l13 -> l0 : result_4^0'=result_4^post26, w_5^0'=w_5^post26, x_6^0'=x_6^post26, (-w_5^post26+w_5^0 == 0 /\ -result_4^post26+result_4^0 == 0 /\ -x_6^post26+x_6^0 == 0), cost: 1 31: l18 -> l0 : result_4^0'=result_4^post30, w_5^0'=w_5^post30, x_6^0'=x_6^post30, (-w_5^post31+w_5^0 == 0 /\ result_4^post31-result_4^post30 == 0 /\ w_5^post31-w_5^post30 == 0 /\ x_6^post31-x_6^post30 == 0 /\ -x_6^post31+x_6^0 == 0 /\ -result_4^post31+result_4^0 == 0), cost: 1 Eliminating location l17 by chaining: Applied chaining First rule: l18 -> l17 : result_4^0'=result_4^post31, w_5^0'=w_5^post31, x_6^0'=x_6^post31, (-w_5^post31+w_5^0 == 0 /\ -x_6^post31+x_6^0 == 0 /\ -result_4^post31+result_4^0 == 0), cost: 1 Second rule: l17 -> l0 : result_4^0'=result_4^post30, w_5^0'=w_5^post30, x_6^0'=x_6^post30, (-result_4^post30+result_4^0 == 0 /\ -x_6^post30+x_6^0 == 0 /\ -w_5^post30+w_5^0 == 0), cost: 1 New rule: l18 -> l0 : result_4^0'=result_4^post30, w_5^0'=w_5^post30, x_6^0'=x_6^post30, (-w_5^post31+w_5^0 == 0 /\ result_4^post31-result_4^post30 == 0 /\ w_5^post31-w_5^post30 == 0 /\ x_6^post31-x_6^post30 == 0 /\ -x_6^post31+x_6^0 == 0 /\ -result_4^post31+result_4^0 == 0), cost: 1 Applied deletion Removed the following rules: 29 30 Eliminating location l15 by chaining: Applied chaining First rule: l0 -> l15 : result_4^0'=result_4^post27, w_5^0'=w_5^post27, x_6^0'=x_6^post27, (-2+w_5^1 <= 0 /\ -2+x_6^post27 <= 0 /\ -1+w_5^post27 == 0 /\ -1+x_6^post27-x_6^0 == 0 /\ -1+x_6^0 <= 0 /\ 2-w_5^1 <= 0 /\ 2-x_6^post27 <= 0 /\ -1+w_5^1-w_5^0 == 0 /\ -result_4^post27+result_4^0 == 0), cost: 1 Second rule: l15 -> l0 : result_4^0'=result_4^post28, w_5^0'=w_5^post28, x_6^0'=x_6^post28, (-x_6^post28+x_6^0 == 0 /\ -result_4^post28+result_4^0 == 0 /\ -w_5^post28+w_5^0 == 0), cost: 1 New rule: l0 -> l0 : result_4^0'=result_4^post28, w_5^0'=w_5^post28, x_6^0'=x_6^post28, (-2+w_5^1 <= 0 /\ -2+x_6^post27 <= 0 /\ -w_5^post28+w_5^post27 == 0 /\ -1+w_5^post27 == 0 /\ -result_4^post28+result_4^post27 == 0 /\ -1+x_6^post27-x_6^0 == 0 /\ -1+x_6^0 <= 0 /\ 2-w_5^1 <= 0 /\ -x_6^post28+x_6^post27 == 0 /\ 2-x_6^post27 <= 0 /\ -1+w_5^1-w_5^0 == 0 /\ -result_4^post27+result_4^0 == 0), cost: 1 Applied deletion Removed the following rules: 26 27 Eliminating location l4 by chaining: Applied chaining First rule: l6 -> l4 : result_4^0'=result_4^post10, w_5^0'=w_5^post10, x_6^0'=x_6^post10, (-2+w_5^0 <= 0 /\ -result_4^post10+result_4^0 == 0 /\ x_6^0-x_6^post10 == 0 /\ 2-w_5^0 <= 0 /\ -1+w_5^post10 == 0), cost: 1 Second rule: l4 -> l0 : result_4^0'=result_4^post11, w_5^0'=w_5^post11, x_6^0'=x_6^post11, (-w_5^post11+w_5^0 == 0 /\ -result_4^post11+result_4^0 == 0 /\ x_6^0-x_6^post11 == 0), cost: 1 New rule: l6 -> l0 : result_4^0'=result_4^post11, w_5^0'=w_5^post11, x_6^0'=x_6^post11, (-2+w_5^0 <= 0 /\ -result_4^post11+result_4^post10 == 0 /\ -result_4^post10+result_4^0 == 0 /\ -x_6^post11+x_6^post10 == 0 /\ x_6^0-x_6^post10 == 0 /\ -w_5^post11+w_5^post10 == 0 /\ 2-w_5^0 <= 0 /\ -1+w_5^post10 == 0), cost: 1 Applied deletion Removed the following rules: 9 10 Eliminating location l10 by chaining: Applied chaining First rule: l12 -> l10 : result_4^0'=result_4^post21, w_5^0'=w_5^post21, x_6^0'=x_6^post21, (-2+w_5^0 <= 0 /\ -1+w_5^post21 == 0 /\ 2-w_5^0 <= 0 /\ -x_6^post21+x_6^0 == 0 /\ -result_4^post21+result_4^0 == 0), cost: 1 Second rule: l10 -> l0 : result_4^0'=result_4^post22, w_5^0'=w_5^post22, x_6^0'=x_6^post22, (-x_6^post22+x_6^0 == 0 /\ -result_4^post22+result_4^0 == 0 /\ -w_5^post22+w_5^0 == 0), cost: 1 New rule: l12 -> l0 : result_4^0'=result_4^post22, w_5^0'=w_5^post22, x_6^0'=x_6^post22, (-2+w_5^0 <= 0 /\ -1+w_5^post21 == 0 /\ -w_5^post22+w_5^post21 == 0 /\ -result_4^post22+result_4^post21 == 0 /\ 2-w_5^0 <= 0 /\ -x_6^post22+x_6^post21 == 0 /\ -x_6^post21+x_6^0 == 0 /\ -result_4^post21+result_4^0 == 0), cost: 1 Applied deletion Removed the following rules: 20 21 Simplified Transitions Start location: l18 Program variables: result_4^0 w_5^0 x_6^0 35: l0 -> l2 : w_5^0'=1+w_5^0, x_6^0'=1+x_6^0, (-2+w_5^0 <= 0 /\ 2-x_6^0 <= 0), cost: 1 41: l0 -> l5 : w_5^0'=1+w_5^0, x_6^0'=1+x_6^0, (-2+w_5^0 <= 0 /\ 2-x_6^0 <= 0), cost: 1 44: l0 -> l8 : w_5^0'=1+w_5^0, x_6^0'=1+x_6^0, -1+x_6^0 <= 0, cost: 1 50: l0 -> l11 : w_5^0'=1+w_5^0, x_6^0'=1+x_6^0, -1+x_6^0 <= 0, cost: 1 53: l0 -> l14 : w_5^0'=1+w_5^0, x_6^0'=2, (1-x_6^0 == 0 /\ -1+x_6^0 <= 0), cost: 1 57: l0 -> l16 : result_4^0'=result_4^post29, (2-x_6^0 <= 0 /\ 3-w_5^0 <= 0), cost: 1 59: l0 -> l0 : w_5^0'=1, x_6^0'=2, (1-x_6^0 == 0 /\ -1+x_6^0 <= 0 /\ 1-w_5^0 == 0), cost: 1 36: l2 -> l3 : -1+x_6^0 <= 0, cost: 1 37: l2 -> l3 : 3-x_6^0 <= 0, cost: 1 38: l3 -> l1 : -1+w_5^0 <= 0, cost: 1 39: l3 -> l1 : 3-w_5^0 <= 0, cost: 1 40: l1 -> l0 : T, cost: 1 42: l5 -> l6 : -1+x_6^0 <= 0, cost: 1 43: l5 -> l6 : 3-x_6^0 <= 0, cost: 1 60: l6 -> l0 : w_5^0'=1, (-2+w_5^0 <= 0 /\ -2+w_5^0 == 0 /\ 2-w_5^0 <= 0), cost: 1 45: l8 -> l9 : -1+x_6^0 <= 0, cost: 1 46: l8 -> l9 : 3-x_6^0 <= 0, cost: 1 47: l9 -> l7 : -1+w_5^0 <= 0, cost: 1 48: l9 -> l7 : 3-w_5^0 <= 0, cost: 1 49: l7 -> l0 : T, cost: 1 51: l11 -> l12 : -1+x_6^0 <= 0, cost: 1 52: l11 -> l12 : 3-x_6^0 <= 0, cost: 1 61: l12 -> l0 : w_5^0'=1, (-2+w_5^0 <= 0 /\ -2+w_5^0 == 0 /\ 2-w_5^0 <= 0), cost: 1 54: l14 -> l13 : -1+w_5^0 <= 0, cost: 1 55: l14 -> l13 : 3-w_5^0 <= 0, cost: 1 56: l13 -> l0 : T, cost: 1 58: l18 -> l0 : T, cost: 1 Propagated Equalities Original rule: l0 -> l2 : result_4^0'=result_4^post1, w_5^0'=w_5^post1, x_6^0'=x_6^post1, (-2+w_5^0 <= 0 /\ -1+x_6^post1-x_6^0 == 0 /\ 2-x_6^0 <= 0 /\ -result_4^post1+result_4^0 == 0 /\ -1+w_5^post1-w_5^0 == 0), cost: 1 New rule: l0 -> l2 : result_4^0'=result_4^0, w_5^0'=1+w_5^0, x_6^0'=1+x_6^0, (0 == 0 /\ -2+w_5^0 <= 0 /\ 2-x_6^0 <= 0), cost: 1 propagated equality x_6^post1 = 1+x_6^0 propagated equality result_4^post1 = result_4^0 propagated equality w_5^post1 = 1+w_5^0 Simplified Guard Original rule: l0 -> l2 : result_4^0'=result_4^0, w_5^0'=1+w_5^0, x_6^0'=1+x_6^0, (0 == 0 /\ -2+w_5^0 <= 0 /\ 2-x_6^0 <= 0), cost: 1 New rule: l0 -> l2 : result_4^0'=result_4^0, w_5^0'=1+w_5^0, x_6^0'=1+x_6^0, (-2+w_5^0 <= 0 /\ 2-x_6^0 <= 0), cost: 1 Removed Trivial Updates Original rule: l0 -> l2 : result_4^0'=result_4^0, w_5^0'=1+w_5^0, x_6^0'=1+x_6^0, (-2+w_5^0 <= 0 /\ 2-x_6^0 <= 0), cost: 1 New rule: l0 -> l2 : w_5^0'=1+w_5^0, x_6^0'=1+x_6^0, (-2+w_5^0 <= 0 /\ 2-x_6^0 <= 0), cost: 1 Propagated Equalities Original rule: l2 -> l3 : result_4^0'=result_4^post2, w_5^0'=w_5^post2, x_6^0'=x_6^post2, (-1+x_6^0 <= 0 /\ -w_5^post2+w_5^0 == 0 /\ -x_6^post2+x_6^0 == 0 /\ -result_4^post2+result_4^0 == 0), cost: 1 New rule: l2 -> l3 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, (0 == 0 /\ -1+x_6^0 <= 0), cost: 1 propagated equality w_5^post2 = w_5^0 propagated equality x_6^post2 = x_6^0 propagated equality result_4^post2 = result_4^0 Simplified Guard Original rule: l2 -> l3 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, (0 == 0 /\ -1+x_6^0 <= 0), cost: 1 New rule: l2 -> l3 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, -1+x_6^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l2 -> l3 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, -1+x_6^0 <= 0, cost: 1 New rule: l2 -> l3 : -1+x_6^0 <= 0, cost: 1 Propagated Equalities Original rule: l2 -> l3 : result_4^0'=result_4^post3, w_5^0'=w_5^post3, x_6^0'=x_6^post3, (3-x_6^0 <= 0 /\ -w_5^post3+w_5^0 == 0 /\ -result_4^post3+result_4^0 == 0 /\ -x_6^post3+x_6^0 == 0), cost: 1 New rule: l2 -> l3 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, (0 == 0 /\ 3-x_6^0 <= 0), cost: 1 propagated equality w_5^post3 = w_5^0 propagated equality result_4^post3 = result_4^0 propagated equality x_6^post3 = x_6^0 Simplified Guard Original rule: l2 -> l3 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, (0 == 0 /\ 3-x_6^0 <= 0), cost: 1 New rule: l2 -> l3 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, 3-x_6^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l2 -> l3 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, 3-x_6^0 <= 0, cost: 1 New rule: l2 -> l3 : 3-x_6^0 <= 0, cost: 1 Propagated Equalities Original rule: l3 -> l1 : result_4^0'=result_4^post4, w_5^0'=w_5^post4, x_6^0'=x_6^post4, (-x_6^post4+x_6^0 == 0 /\ -result_4^post4+result_4^0 == 0 /\ -w_5^post4+w_5^0 == 0 /\ -1+w_5^0 <= 0), cost: 1 New rule: l3 -> l1 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, (0 == 0 /\ -1+w_5^0 <= 0), cost: 1 propagated equality x_6^post4 = x_6^0 propagated equality result_4^post4 = result_4^0 propagated equality w_5^post4 = w_5^0 Simplified Guard Original rule: l3 -> l1 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, (0 == 0 /\ -1+w_5^0 <= 0), cost: 1 New rule: l3 -> l1 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, -1+w_5^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l3 -> l1 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, -1+w_5^0 <= 0, cost: 1 New rule: l3 -> l1 : -1+w_5^0 <= 0, cost: 1 Propagated Equalities Original rule: l3 -> l1 : result_4^0'=result_4^post5, w_5^0'=w_5^post5, x_6^0'=x_6^post5, (-w_5^post5+w_5^0 == 0 /\ -x_6^post5+x_6^0 == 0 /\ -result_4^post5+result_4^0 == 0 /\ 3-w_5^0 <= 0), cost: 1 New rule: l3 -> l1 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, (0 == 0 /\ 3-w_5^0 <= 0), cost: 1 propagated equality w_5^post5 = w_5^0 propagated equality x_6^post5 = x_6^0 propagated equality result_4^post5 = result_4^0 Simplified Guard Original rule: l3 -> l1 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, (0 == 0 /\ 3-w_5^0 <= 0), cost: 1 New rule: l3 -> l1 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, 3-w_5^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l3 -> l1 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, 3-w_5^0 <= 0, cost: 1 New rule: l3 -> l1 : 3-w_5^0 <= 0, cost: 1 Propagated Equalities Original rule: l1 -> l0 : result_4^0'=result_4^post6, w_5^0'=w_5^post6, x_6^0'=x_6^post6, (-w_5^post6+w_5^0 == 0 /\ -result_4^post6+result_4^0 == 0 /\ -x_6^post6+x_6^0 == 0), cost: 1 New rule: l1 -> l0 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, 0 == 0, cost: 1 propagated equality w_5^post6 = w_5^0 propagated equality result_4^post6 = result_4^0 propagated equality x_6^post6 = x_6^0 Simplified Guard Original rule: l1 -> l0 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, 0 == 0, cost: 1 New rule: l1 -> l0 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, T, cost: 1 Removed Trivial Updates Original rule: l1 -> l0 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, T, cost: 1 New rule: l1 -> l0 : T, cost: 1 Propagated Equalities Original rule: l0 -> l5 : result_4^0'=result_4^post7, w_5^0'=w_5^post7, x_6^0'=x_6^post7, (-1+w_5^post7-w_5^0 == 0 /\ -2+w_5^0 <= 0 /\ 2-x_6^0 <= 0 /\ -1+x_6^post7-x_6^0 == 0 /\ -result_4^post7+result_4^0 == 0), cost: 1 New rule: l0 -> l5 : result_4^0'=result_4^0, w_5^0'=1+w_5^0, x_6^0'=1+x_6^0, (0 == 0 /\ -2+w_5^0 <= 0 /\ 2-x_6^0 <= 0), cost: 1 propagated equality w_5^post7 = 1+w_5^0 propagated equality x_6^post7 = 1+x_6^0 propagated equality result_4^post7 = result_4^0 Simplified Guard Original rule: l0 -> l5 : result_4^0'=result_4^0, w_5^0'=1+w_5^0, x_6^0'=1+x_6^0, (0 == 0 /\ -2+w_5^0 <= 0 /\ 2-x_6^0 <= 0), cost: 1 New rule: l0 -> l5 : result_4^0'=result_4^0, w_5^0'=1+w_5^0, x_6^0'=1+x_6^0, (-2+w_5^0 <= 0 /\ 2-x_6^0 <= 0), cost: 1 Removed Trivial Updates Original rule: l0 -> l5 : result_4^0'=result_4^0, w_5^0'=1+w_5^0, x_6^0'=1+x_6^0, (-2+w_5^0 <= 0 /\ 2-x_6^0 <= 0), cost: 1 New rule: l0 -> l5 : w_5^0'=1+w_5^0, x_6^0'=1+x_6^0, (-2+w_5^0 <= 0 /\ 2-x_6^0 <= 0), cost: 1 Propagated Equalities Original rule: l5 -> l6 : result_4^0'=result_4^post8, w_5^0'=w_5^post8, x_6^0'=x_6^post8, (x_6^0-x_6^post8 == 0 /\ -result_4^post8+result_4^0 == 0 /\ -w_5^post8+w_5^0 == 0 /\ -1+x_6^0 <= 0), cost: 1 New rule: l5 -> l6 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, (0 == 0 /\ -1+x_6^0 <= 0), cost: 1 propagated equality x_6^post8 = x_6^0 propagated equality result_4^post8 = result_4^0 propagated equality w_5^post8 = w_5^0 Simplified Guard Original rule: l5 -> l6 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, (0 == 0 /\ -1+x_6^0 <= 0), cost: 1 New rule: l5 -> l6 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, -1+x_6^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l5 -> l6 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, -1+x_6^0 <= 0, cost: 1 New rule: l5 -> l6 : -1+x_6^0 <= 0, cost: 1 Propagated Equalities Original rule: l5 -> l6 : result_4^0'=result_4^post9, w_5^0'=w_5^post9, x_6^0'=x_6^post9, (3-x_6^0 <= 0 /\ x_6^0-x_6^post9 == 0 /\ -w_5^post9+w_5^0 == 0 /\ -result_4^post9+result_4^0 == 0), cost: 1 New rule: l5 -> l6 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, (0 == 0 /\ 3-x_6^0 <= 0), cost: 1 propagated equality x_6^post9 = x_6^0 propagated equality w_5^post9 = w_5^0 propagated equality result_4^post9 = result_4^0 Simplified Guard Original rule: l5 -> l6 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, (0 == 0 /\ 3-x_6^0 <= 0), cost: 1 New rule: l5 -> l6 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, 3-x_6^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l5 -> l6 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, 3-x_6^0 <= 0, cost: 1 New rule: l5 -> l6 : 3-x_6^0 <= 0, cost: 1 Propagated Equalities Original rule: l0 -> l8 : result_4^0'=result_4^post12, w_5^0'=w_5^post12, x_6^0'=x_6^post12, (-1+w_5^post12-w_5^0 == 0 /\ -1+x_6^0 <= 0 /\ -1+x_6^post12-x_6^0 == 0 /\ -result_4^post12+result_4^0 == 0), cost: 1 New rule: l0 -> l8 : result_4^0'=result_4^0, w_5^0'=1+w_5^0, x_6^0'=1+x_6^0, (0 == 0 /\ -1+x_6^0 <= 0), cost: 1 propagated equality w_5^post12 = 1+w_5^0 propagated equality x_6^post12 = 1+x_6^0 propagated equality result_4^post12 = result_4^0 Simplified Guard Original rule: l0 -> l8 : result_4^0'=result_4^0, w_5^0'=1+w_5^0, x_6^0'=1+x_6^0, (0 == 0 /\ -1+x_6^0 <= 0), cost: 1 New rule: l0 -> l8 : result_4^0'=result_4^0, w_5^0'=1+w_5^0, x_6^0'=1+x_6^0, -1+x_6^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l0 -> l8 : result_4^0'=result_4^0, w_5^0'=1+w_5^0, x_6^0'=1+x_6^0, -1+x_6^0 <= 0, cost: 1 New rule: l0 -> l8 : w_5^0'=1+w_5^0, x_6^0'=1+x_6^0, -1+x_6^0 <= 0, cost: 1 Propagated Equalities Original rule: l8 -> l9 : result_4^0'=result_4^post13, w_5^0'=w_5^post13, x_6^0'=x_6^post13, (result_4^0-result_4^post13 == 0 /\ -1+x_6^0 <= 0 /\ x_6^0-x_6^post13 == 0 /\ -w_5^post13+w_5^0 == 0), cost: 1 New rule: l8 -> l9 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, (0 == 0 /\ -1+x_6^0 <= 0), cost: 1 propagated equality result_4^post13 = result_4^0 propagated equality x_6^post13 = x_6^0 propagated equality w_5^post13 = w_5^0 Simplified Guard Original rule: l8 -> l9 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, (0 == 0 /\ -1+x_6^0 <= 0), cost: 1 New rule: l8 -> l9 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, -1+x_6^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l8 -> l9 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, -1+x_6^0 <= 0, cost: 1 New rule: l8 -> l9 : -1+x_6^0 <= 0, cost: 1 Propagated Equalities Original rule: l8 -> l9 : result_4^0'=result_4^post14, w_5^0'=w_5^post14, x_6^0'=x_6^post14, (-x_6^post14+x_6^0 == 0 /\ 3-x_6^0 <= 0 /\ result_4^0-result_4^post14 == 0 /\ -w_5^post14+w_5^0 == 0), cost: 1 New rule: l8 -> l9 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, (0 == 0 /\ 3-x_6^0 <= 0), cost: 1 propagated equality x_6^post14 = x_6^0 propagated equality result_4^post14 = result_4^0 propagated equality w_5^post14 = w_5^0 Simplified Guard Original rule: l8 -> l9 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, (0 == 0 /\ 3-x_6^0 <= 0), cost: 1 New rule: l8 -> l9 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, 3-x_6^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l8 -> l9 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, 3-x_6^0 <= 0, cost: 1 New rule: l8 -> l9 : 3-x_6^0 <= 0, cost: 1 Propagated Equalities Original rule: l9 -> l7 : result_4^0'=result_4^post15, w_5^0'=w_5^post15, x_6^0'=x_6^post15, (result_4^0-result_4^post15 == 0 /\ -w_5^post15+w_5^0 == 0 /\ -x_6^post15+x_6^0 == 0 /\ -1+w_5^0 <= 0), cost: 1 New rule: l9 -> l7 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, (0 == 0 /\ -1+w_5^0 <= 0), cost: 1 propagated equality result_4^post15 = result_4^0 propagated equality w_5^post15 = w_5^0 propagated equality x_6^post15 = x_6^0 Simplified Guard Original rule: l9 -> l7 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, (0 == 0 /\ -1+w_5^0 <= 0), cost: 1 New rule: l9 -> l7 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, -1+w_5^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l9 -> l7 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, -1+w_5^0 <= 0, cost: 1 New rule: l9 -> l7 : -1+w_5^0 <= 0, cost: 1 Propagated Equalities Original rule: l9 -> l7 : result_4^0'=result_4^post16, w_5^0'=w_5^post16, x_6^0'=x_6^post16, (-w_5^post16+w_5^0 == 0 /\ -x_6^post16+x_6^0 == 0 /\ -result_4^post16+result_4^0 == 0 /\ 3-w_5^0 <= 0), cost: 1 New rule: l9 -> l7 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, (0 == 0 /\ 3-w_5^0 <= 0), cost: 1 propagated equality w_5^post16 = w_5^0 propagated equality x_6^post16 = x_6^0 propagated equality result_4^post16 = result_4^0 Simplified Guard Original rule: l9 -> l7 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, (0 == 0 /\ 3-w_5^0 <= 0), cost: 1 New rule: l9 -> l7 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, 3-w_5^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l9 -> l7 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, 3-w_5^0 <= 0, cost: 1 New rule: l9 -> l7 : 3-w_5^0 <= 0, cost: 1 Propagated Equalities Original rule: l7 -> l0 : result_4^0'=result_4^post17, w_5^0'=w_5^post17, x_6^0'=x_6^post17, (-w_5^post17+w_5^0 == 0 /\ -x_6^post17+x_6^0 == 0 /\ -result_4^post17+result_4^0 == 0), cost: 1 New rule: l7 -> l0 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, 0 == 0, cost: 1 propagated equality w_5^post17 = w_5^0 propagated equality x_6^post17 = x_6^0 propagated equality result_4^post17 = result_4^0 Simplified Guard Original rule: l7 -> l0 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, 0 == 0, cost: 1 New rule: l7 -> l0 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, T, cost: 1 Removed Trivial Updates Original rule: l7 -> l0 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, T, cost: 1 New rule: l7 -> l0 : T, cost: 1 Propagated Equalities Original rule: l0 -> l11 : result_4^0'=result_4^post18, w_5^0'=w_5^post18, x_6^0'=x_6^post18, (-result_4^post18+result_4^0 == 0 /\ -1+w_5^post18-w_5^0 == 0 /\ -1+x_6^0 <= 0 /\ -1+x_6^post18-x_6^0 == 0), cost: 1 New rule: l0 -> l11 : result_4^0'=result_4^0, w_5^0'=1+w_5^0, x_6^0'=1+x_6^0, (0 == 0 /\ -1+x_6^0 <= 0), cost: 1 propagated equality result_4^post18 = result_4^0 propagated equality w_5^post18 = 1+w_5^0 propagated equality x_6^post18 = 1+x_6^0 Simplified Guard Original rule: l0 -> l11 : result_4^0'=result_4^0, w_5^0'=1+w_5^0, x_6^0'=1+x_6^0, (0 == 0 /\ -1+x_6^0 <= 0), cost: 1 New rule: l0 -> l11 : result_4^0'=result_4^0, w_5^0'=1+w_5^0, x_6^0'=1+x_6^0, -1+x_6^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l0 -> l11 : result_4^0'=result_4^0, w_5^0'=1+w_5^0, x_6^0'=1+x_6^0, -1+x_6^0 <= 0, cost: 1 New rule: l0 -> l11 : w_5^0'=1+w_5^0, x_6^0'=1+x_6^0, -1+x_6^0 <= 0, cost: 1 Propagated Equalities Original rule: l11 -> l12 : result_4^0'=result_4^post19, w_5^0'=w_5^post19, x_6^0'=x_6^post19, (-x_6^post19+x_6^0 == 0 /\ result_4^0-result_4^post19 == 0 /\ -1+x_6^0 <= 0 /\ -w_5^post19+w_5^0 == 0), cost: 1 New rule: l11 -> l12 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, (0 == 0 /\ -1+x_6^0 <= 0), cost: 1 propagated equality x_6^post19 = x_6^0 propagated equality result_4^post19 = result_4^0 propagated equality w_5^post19 = w_5^0 Simplified Guard Original rule: l11 -> l12 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, (0 == 0 /\ -1+x_6^0 <= 0), cost: 1 New rule: l11 -> l12 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, -1+x_6^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l11 -> l12 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, -1+x_6^0 <= 0, cost: 1 New rule: l11 -> l12 : -1+x_6^0 <= 0, cost: 1 Propagated Equalities Original rule: l11 -> l12 : result_4^0'=result_4^post20, w_5^0'=w_5^post20, x_6^0'=x_6^post20, (-w_5^post20+w_5^0 == 0 /\ 3-x_6^0 <= 0 /\ -result_4^post20+result_4^0 == 0 /\ -x_6^post20+x_6^0 == 0), cost: 1 New rule: l11 -> l12 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, (0 == 0 /\ 3-x_6^0 <= 0), cost: 1 propagated equality w_5^post20 = w_5^0 propagated equality result_4^post20 = result_4^0 propagated equality x_6^post20 = x_6^0 Simplified Guard Original rule: l11 -> l12 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, (0 == 0 /\ 3-x_6^0 <= 0), cost: 1 New rule: l11 -> l12 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, 3-x_6^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l11 -> l12 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, 3-x_6^0 <= 0, cost: 1 New rule: l11 -> l12 : 3-x_6^0 <= 0, cost: 1 made implied equalities explicit Original rule: l0 -> l14 : result_4^0'=result_4^post23, w_5^0'=w_5^post23, x_6^0'=x_6^post23, (-result_4^post23+result_4^0 == 0 /\ -1+x_6^0 <= 0 /\ -2+x_6^post23 <= 0 /\ -1+x_6^post23-x_6^0 == 0 /\ -1-w_5^0+w_5^post23 == 0 /\ 2-x_6^post23 <= 0), cost: 1 New rule: l0 -> l14 : result_4^0'=result_4^post23, w_5^0'=w_5^post23, x_6^0'=x_6^post23, (-result_4^post23+result_4^0 == 0 /\ -1+x_6^0 <= 0 /\ -2+x_6^post23 <= 0 /\ -2+x_6^post23 == 0 /\ -1+x_6^post23-x_6^0 == 0 /\ -1-w_5^0+w_5^post23 == 0 /\ 2-x_6^post23 <= 0), cost: 1 Propagated Equalities Original rule: l0 -> l14 : result_4^0'=result_4^post23, w_5^0'=w_5^post23, x_6^0'=x_6^post23, (-result_4^post23+result_4^0 == 0 /\ -1+x_6^0 <= 0 /\ -2+x_6^post23 <= 0 /\ -2+x_6^post23 == 0 /\ -1+x_6^post23-x_6^0 == 0 /\ -1-w_5^0+w_5^post23 == 0 /\ 2-x_6^post23 <= 0), cost: 1 New rule: l0 -> l14 : result_4^0'=result_4^0, w_5^0'=1+w_5^0, x_6^0'=2, (0 <= 0 /\ 0 == 0 /\ 1-x_6^0 == 0 /\ -1+x_6^0 <= 0), cost: 1 propagated equality result_4^post23 = result_4^0 propagated equality x_6^post23 = 2 propagated equality w_5^post23 = 1+w_5^0 Simplified Guard Original rule: l0 -> l14 : result_4^0'=result_4^0, w_5^0'=1+w_5^0, x_6^0'=2, (0 <= 0 /\ 0 == 0 /\ 1-x_6^0 == 0 /\ -1+x_6^0 <= 0), cost: 1 New rule: l0 -> l14 : result_4^0'=result_4^0, w_5^0'=1+w_5^0, x_6^0'=2, (1-x_6^0 == 0 /\ -1+x_6^0 <= 0), cost: 1 Removed Trivial Updates Original rule: l0 -> l14 : result_4^0'=result_4^0, w_5^0'=1+w_5^0, x_6^0'=2, (1-x_6^0 == 0 /\ -1+x_6^0 <= 0), cost: 1 New rule: l0 -> l14 : w_5^0'=1+w_5^0, x_6^0'=2, (1-x_6^0 == 0 /\ -1+x_6^0 <= 0), cost: 1 Propagated Equalities Original rule: l14 -> l13 : result_4^0'=result_4^post24, w_5^0'=w_5^post24, x_6^0'=x_6^post24, (-x_6^post24+x_6^0 == 0 /\ -result_4^post24+result_4^0 == 0 /\ -w_5^post24+w_5^0 == 0 /\ -1+w_5^0 <= 0), cost: 1 New rule: l14 -> l13 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, (0 == 0 /\ -1+w_5^0 <= 0), cost: 1 propagated equality x_6^post24 = x_6^0 propagated equality result_4^post24 = result_4^0 propagated equality w_5^post24 = w_5^0 Simplified Guard Original rule: l14 -> l13 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, (0 == 0 /\ -1+w_5^0 <= 0), cost: 1 New rule: l14 -> l13 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, -1+w_5^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l14 -> l13 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, -1+w_5^0 <= 0, cost: 1 New rule: l14 -> l13 : -1+w_5^0 <= 0, cost: 1 Propagated Equalities Original rule: l14 -> l13 : result_4^0'=result_4^post25, w_5^0'=w_5^post25, x_6^0'=x_6^post25, (-w_5^post25+w_5^0 == 0 /\ -result_4^post25+result_4^0 == 0 /\ -x_6^post25+x_6^0 == 0 /\ 3-w_5^0 <= 0), cost: 1 New rule: l14 -> l13 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, (0 == 0 /\ 3-w_5^0 <= 0), cost: 1 propagated equality w_5^post25 = w_5^0 propagated equality result_4^post25 = result_4^0 propagated equality x_6^post25 = x_6^0 Simplified Guard Original rule: l14 -> l13 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, (0 == 0 /\ 3-w_5^0 <= 0), cost: 1 New rule: l14 -> l13 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, 3-w_5^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l14 -> l13 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, 3-w_5^0 <= 0, cost: 1 New rule: l14 -> l13 : 3-w_5^0 <= 0, cost: 1 Propagated Equalities Original rule: l13 -> l0 : result_4^0'=result_4^post26, w_5^0'=w_5^post26, x_6^0'=x_6^post26, (-w_5^post26+w_5^0 == 0 /\ -result_4^post26+result_4^0 == 0 /\ -x_6^post26+x_6^0 == 0), cost: 1 New rule: l13 -> l0 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, 0 == 0, cost: 1 propagated equality w_5^post26 = w_5^0 propagated equality result_4^post26 = result_4^0 propagated equality x_6^post26 = x_6^0 Simplified Guard Original rule: l13 -> l0 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, 0 == 0, cost: 1 New rule: l13 -> l0 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, T, cost: 1 Removed Trivial Updates Original rule: l13 -> l0 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, T, cost: 1 New rule: l13 -> l0 : T, cost: 1 Propagated Equalities Original rule: l0 -> l16 : result_4^0'=result_4^post29, w_5^0'=w_5^post29, x_6^0'=x_6^post29, (0 == 0 /\ 2-x_6^0 <= 0 /\ 3-w_5^0 <= 0 /\ -w_5^post29+w_5^0 == 0 /\ -x_6^post29+x_6^0 == 0), cost: 1 New rule: l0 -> l16 : result_4^0'=result_4^post29, w_5^0'=w_5^0, x_6^0'=x_6^0, (0 == 0 /\ 2-x_6^0 <= 0 /\ 3-w_5^0 <= 0), cost: 1 propagated equality w_5^post29 = w_5^0 propagated equality x_6^post29 = x_6^0 Simplified Guard Original rule: l0 -> l16 : result_4^0'=result_4^post29, w_5^0'=w_5^0, x_6^0'=x_6^0, (0 == 0 /\ 2-x_6^0 <= 0 /\ 3-w_5^0 <= 0), cost: 1 New rule: l0 -> l16 : result_4^0'=result_4^post29, w_5^0'=w_5^0, x_6^0'=x_6^0, (2-x_6^0 <= 0 /\ 3-w_5^0 <= 0), cost: 1 Removed Trivial Updates Original rule: l0 -> l16 : result_4^0'=result_4^post29, w_5^0'=w_5^0, x_6^0'=x_6^0, (2-x_6^0 <= 0 /\ 3-w_5^0 <= 0), cost: 1 New rule: l0 -> l16 : result_4^0'=result_4^post29, (2-x_6^0 <= 0 /\ 3-w_5^0 <= 0), cost: 1 Propagated Equalities Original rule: l18 -> l0 : result_4^0'=result_4^post30, w_5^0'=w_5^post30, x_6^0'=x_6^post30, (-w_5^post31+w_5^0 == 0 /\ result_4^post31-result_4^post30 == 0 /\ w_5^post31-w_5^post30 == 0 /\ x_6^post31-x_6^post30 == 0 /\ -x_6^post31+x_6^0 == 0 /\ -result_4^post31+result_4^0 == 0), cost: 1 New rule: l18 -> l0 : result_4^0'=result_4^post31, w_5^0'=w_5^post31, x_6^0'=x_6^post31, (0 == 0 /\ -w_5^post31+w_5^0 == 0 /\ -x_6^post31+x_6^0 == 0 /\ -result_4^post31+result_4^0 == 0), cost: 1 propagated equality result_4^post30 = result_4^post31 propagated equality w_5^post30 = w_5^post31 propagated equality x_6^post30 = x_6^post31 Propagated Equalities Original rule: l18 -> l0 : result_4^0'=result_4^post31, w_5^0'=w_5^post31, x_6^0'=x_6^post31, (0 == 0 /\ -w_5^post31+w_5^0 == 0 /\ -x_6^post31+x_6^0 == 0 /\ -result_4^post31+result_4^0 == 0), cost: 1 New rule: l18 -> l0 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, 0 == 0, cost: 1 propagated equality w_5^post31 = w_5^0 propagated equality x_6^post31 = x_6^0 propagated equality result_4^post31 = result_4^0 Simplified Guard Original rule: l18 -> l0 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, 0 == 0, cost: 1 New rule: l18 -> l0 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, T, cost: 1 Removed Trivial Updates Original rule: l18 -> l0 : result_4^0'=result_4^0, w_5^0'=w_5^0, x_6^0'=x_6^0, T, cost: 1 New rule: l18 -> l0 : T, cost: 1 made implied equalities explicit Original rule: l0 -> l0 : result_4^0'=result_4^post28, w_5^0'=w_5^post28, x_6^0'=x_6^post28, (-2+w_5^1 <= 0 /\ -2+x_6^post27 <= 0 /\ -w_5^post28+w_5^post27 == 0 /\ -1+w_5^post27 == 0 /\ -result_4^post28+result_4^post27 == 0 /\ -1+x_6^post27-x_6^0 == 0 /\ -1+x_6^0 <= 0 /\ 2-w_5^1 <= 0 /\ -x_6^post28+x_6^post27 == 0 /\ 2-x_6^post27 <= 0 /\ -1+w_5^1-w_5^0 == 0 /\ -result_4^post27+result_4^0 == 0), cost: 1 New rule: l0 -> l0 : result_4^0'=result_4^post28, w_5^0'=w_5^post28, x_6^0'=x_6^post28, (-2+w_5^1 <= 0 /\ -2+w_5^1 == 0 /\ -2+x_6^post27 <= 0 /\ -2+x_6^post27 == 0 /\ -w_5^post28+w_5^post27 == 0 /\ -1+w_5^post27 == 0 /\ -result_4^post28+result_4^post27 == 0 /\ -1+x_6^post27-x_6^0 == 0 /\ -1+x_6^0 <= 0 /\ 2-w_5^1 <= 0 /\ -x_6^post28+x_6^post27 == 0 /\ 2-x_6^post27 <= 0 /\ -1+w_5^1-w_5^0 == 0 /\ -result_4^post27+result_4^0 == 0), cost: 1 Propagated Equalities Original rule: l0 -> l0 : result_4^0'=result_4^post28, w_5^0'=w_5^post28, x_6^0'=x_6^post28, (-2+w_5^1 <= 0 /\ -2+w_5^1 == 0 /\ -2+x_6^post27 <= 0 /\ -2+x_6^post27 == 0 /\ -w_5^post28+w_5^post27 == 0 /\ -1+w_5^post27 == 0 /\ -result_4^post28+result_4^post27 == 0 /\ -1+x_6^post27-x_6^0 == 0 /\ -1+x_6^0 <= 0 /\ 2-w_5^1 <= 0 /\ -x_6^post28+x_6^post27 == 0 /\ 2-x_6^post27 <= 0 /\ -1+w_5^1-w_5^0 == 0 /\ -result_4^post27+result_4^0 == 0), cost: 1 New rule: l0 -> l0 : result_4^0'=result_4^post27, w_5^0'=w_5^post27, x_6^0'=x_6^post27, (0 == 0 /\ -2+w_5^1 <= 0 /\ -2+w_5^1 == 0 /\ -2+x_6^post27 <= 0 /\ -2+x_6^post27 == 0 /\ -1+w_5^post27 == 0 /\ -1+x_6^post27-x_6^0 == 0 /\ -1+x_6^0 <= 0 /\ 2-w_5^1 <= 0 /\ 2-x_6^post27 <= 0 /\ -1+w_5^1-w_5^0 == 0 /\ -result_4^post27+result_4^0 == 0), cost: 1 propagated equality w_5^post28 = w_5^post27 propagated equality result_4^post28 = result_4^post27 propagated equality x_6^post28 = x_6^post27 Propagated Equalities Original rule: l0 -> l0 : result_4^0'=result_4^post27, w_5^0'=w_5^post27, x_6^0'=x_6^post27, (0 == 0 /\ -2+w_5^1 <= 0 /\ -2+w_5^1 == 0 /\ -2+x_6^post27 <= 0 /\ -2+x_6^post27 == 0 /\ -1+w_5^post27 == 0 /\ -1+x_6^post27-x_6^0 == 0 /\ -1+x_6^0 <= 0 /\ 2-w_5^1 <= 0 /\ 2-x_6^post27 <= 0 /\ -1+w_5^1-w_5^0 == 0 /\ -result_4^post27+result_4^0 == 0), cost: 1 New rule: l0 -> l0 : result_4^0'=result_4^0, w_5^0'=1, x_6^0'=2, (0 <= 0 /\ 0 == 0 /\ 1-x_6^0 == 0 /\ -1+x_6^0 <= 0 /\ 1-w_5^0 == 0), cost: 1 propagated equality w_5^1 = 2 propagated equality x_6^post27 = 2 propagated equality w_5^post27 = 1 propagated equality result_4^post27 = result_4^0 Simplified Guard Original rule: l0 -> l0 : result_4^0'=result_4^0, w_5^0'=1, x_6^0'=2, (0 <= 0 /\ 0 == 0 /\ 1-x_6^0 == 0 /\ -1+x_6^0 <= 0 /\ 1-w_5^0 == 0), cost: 1 New rule: l0 -> l0 : result_4^0'=result_4^0, w_5^0'=1, x_6^0'=2, (1-x_6^0 == 0 /\ -1+x_6^0 <= 0 /\ 1-w_5^0 == 0), cost: 1 Removed Trivial Updates Original rule: l0 -> l0 : result_4^0'=result_4^0, w_5^0'=1, x_6^0'=2, (1-x_6^0 == 0 /\ -1+x_6^0 <= 0 /\ 1-w_5^0 == 0), cost: 1 New rule: l0 -> l0 : w_5^0'=1, x_6^0'=2, (1-x_6^0 == 0 /\ -1+x_6^0 <= 0 /\ 1-w_5^0 == 0), cost: 1 made implied equalities explicit Original rule: l6 -> l0 : result_4^0'=result_4^post11, w_5^0'=w_5^post11, x_6^0'=x_6^post11, (-2+w_5^0 <= 0 /\ -result_4^post11+result_4^post10 == 0 /\ -result_4^post10+result_4^0 == 0 /\ -x_6^post11+x_6^post10 == 0 /\ x_6^0-x_6^post10 == 0 /\ -w_5^post11+w_5^post10 == 0 /\ 2-w_5^0 <= 0 /\ -1+w_5^post10 == 0), cost: 1 New rule: l6 -> l0 : result_4^0'=result_4^post11, w_5^0'=w_5^post11, x_6^0'=x_6^post11, (-2+w_5^0 <= 0 /\ -2+w_5^0 == 0 /\ -result_4^post11+result_4^post10 == 0 /\ -result_4^post10+result_4^0 == 0 /\ -x_6^post11+x_6^post10 == 0 /\ x_6^0-x_6^post10 == 0 /\ -w_5^post11+w_5^post10 == 0 /\ 2-w_5^0 <= 0 /\ -1+w_5^post10 == 0), cost: 1 Propagated Equalities Original rule: l6 -> l0 : result_4^0'=result_4^post11, w_5^0'=w_5^post11, x_6^0'=x_6^post11, (-2+w_5^0 <= 0 /\ -2+w_5^0 == 0 /\ -result_4^post11+result_4^post10 == 0 /\ -result_4^post10+result_4^0 == 0 /\ -x_6^post11+x_6^post10 == 0 /\ x_6^0-x_6^post10 == 0 /\ -w_5^post11+w_5^post10 == 0 /\ 2-w_5^0 <= 0 /\ -1+w_5^post10 == 0), cost: 1 New rule: l6 -> l0 : result_4^0'=result_4^post10, w_5^0'=w_5^post10, x_6^0'=x_6^post10, (0 == 0 /\ -2+w_5^0 <= 0 /\ -2+w_5^0 == 0 /\ -result_4^post10+result_4^0 == 0 /\ x_6^0-x_6^post10 == 0 /\ 2-w_5^0 <= 0 /\ -1+w_5^post10 == 0), cost: 1 propagated equality result_4^post11 = result_4^post10 propagated equality x_6^post11 = x_6^post10 propagated equality w_5^post11 = w_5^post10 Propagated Equalities Original rule: l6 -> l0 : result_4^0'=result_4^post10, w_5^0'=w_5^post10, x_6^0'=x_6^post10, (0 == 0 /\ -2+w_5^0 <= 0 /\ -2+w_5^0 == 0 /\ -result_4^post10+result_4^0 == 0 /\ x_6^0-x_6^post10 == 0 /\ 2-w_5^0 <= 0 /\ -1+w_5^post10 == 0), cost: 1 New rule: l6 -> l0 : result_4^0'=result_4^0, w_5^0'=1, x_6^0'=x_6^0, (0 == 0 /\ -2+w_5^0 <= 0 /\ -2+w_5^0 == 0 /\ 2-w_5^0 <= 0), cost: 1 propagated equality result_4^post10 = result_4^0 propagated equality x_6^post10 = x_6^0 propagated equality w_5^post10 = 1 Simplified Guard Original rule: l6 -> l0 : result_4^0'=result_4^0, w_5^0'=1, x_6^0'=x_6^0, (0 == 0 /\ -2+w_5^0 <= 0 /\ -2+w_5^0 == 0 /\ 2-w_5^0 <= 0), cost: 1 New rule: l6 -> l0 : result_4^0'=result_4^0, w_5^0'=1, x_6^0'=x_6^0, (-2+w_5^0 <= 0 /\ -2+w_5^0 == 0 /\ 2-w_5^0 <= 0), cost: 1 made implied equalities explicit Original rule: l6 -> l0 : result_4^0'=result_4^0, w_5^0'=1, x_6^0'=x_6^0, (-2+w_5^0 <= 0 /\ -2+w_5^0 == 0 /\ 2-w_5^0 <= 0), cost: 1 New rule: l6 -> l0 : result_4^0'=result_4^0, w_5^0'=1, x_6^0'=x_6^0, (-2+w_5^0 <= 0 /\ -2+w_5^0 == 0 /\ 2-w_5^0 <= 0), cost: 1 Removed Trivial Updates Original rule: l6 -> l0 : result_4^0'=result_4^0, w_5^0'=1, x_6^0'=x_6^0, (-2+w_5^0 <= 0 /\ -2+w_5^0 == 0 /\ 2-w_5^0 <= 0), cost: 1 New rule: l6 -> l0 : w_5^0'=1, (-2+w_5^0 <= 0 /\ -2+w_5^0 == 0 /\ 2-w_5^0 <= 0), cost: 1 made implied equalities explicit Original rule: l12 -> l0 : result_4^0'=result_4^post22, w_5^0'=w_5^post22, x_6^0'=x_6^post22, (-2+w_5^0 <= 0 /\ -1+w_5^post21 == 0 /\ -w_5^post22+w_5^post21 == 0 /\ -result_4^post22+result_4^post21 == 0 /\ 2-w_5^0 <= 0 /\ -x_6^post22+x_6^post21 == 0 /\ -x_6^post21+x_6^0 == 0 /\ -result_4^post21+result_4^0 == 0), cost: 1 New rule: l12 -> l0 : result_4^0'=result_4^post22, w_5^0'=w_5^post22, x_6^0'=x_6^post22, (-2+w_5^0 <= 0 /\ -2+w_5^0 == 0 /\ -1+w_5^post21 == 0 /\ -w_5^post22+w_5^post21 == 0 /\ -result_4^post22+result_4^post21 == 0 /\ 2-w_5^0 <= 0 /\ -x_6^post22+x_6^post21 == 0 /\ -x_6^post21+x_6^0 == 0 /\ -result_4^post21+result_4^0 == 0), cost: 1 Propagated Equalities Original rule: l12 -> l0 : result_4^0'=result_4^post22, w_5^0'=w_5^post22, x_6^0'=x_6^post22, (-2+w_5^0 <= 0 /\ -2+w_5^0 == 0 /\ -1+w_5^post21 == 0 /\ -w_5^post22+w_5^post21 == 0 /\ -result_4^post22+result_4^post21 == 0 /\ 2-w_5^0 <= 0 /\ -x_6^post22+x_6^post21 == 0 /\ -x_6^post21+x_6^0 == 0 /\ -result_4^post21+result_4^0 == 0), cost: 1 New rule: l12 -> l0 : result_4^0'=result_4^post21, w_5^0'=w_5^post21, x_6^0'=x_6^post21, (0 == 0 /\ -2+w_5^0 <= 0 /\ -2+w_5^0 == 0 /\ -1+w_5^post21 == 0 /\ 2-w_5^0 <= 0 /\ -x_6^post21+x_6^0 == 0 /\ -result_4^post21+result_4^0 == 0), cost: 1 propagated equality w_5^post22 = w_5^post21 propagated equality result_4^post22 = result_4^post21 propagated equality x_6^post22 = x_6^post21 Propagated Equalities Original rule: l12 -> l0 : result_4^0'=result_4^post21, w_5^0'=w_5^post21, x_6^0'=x_6^post21, (0 == 0 /\ -2+w_5^0 <= 0 /\ -2+w_5^0 == 0 /\ -1+w_5^post21 == 0 /\ 2-w_5^0 <= 0 /\ -x_6^post21+x_6^0 == 0 /\ -result_4^post21+result_4^0 == 0), cost: 1 New rule: l12 -> l0 : result_4^0'=result_4^0, w_5^0'=1, x_6^0'=x_6^0, (0 == 0 /\ -2+w_5^0 <= 0 /\ -2+w_5^0 == 0 /\ 2-w_5^0 <= 0), cost: 1 propagated equality w_5^post21 = 1 propagated equality x_6^post21 = x_6^0 propagated equality result_4^post21 = result_4^0 Simplified Guard Original rule: l12 -> l0 : result_4^0'=result_4^0, w_5^0'=1, x_6^0'=x_6^0, (0 == 0 /\ -2+w_5^0 <= 0 /\ -2+w_5^0 == 0 /\ 2-w_5^0 <= 0), cost: 1 New rule: l12 -> l0 : result_4^0'=result_4^0, w_5^0'=1, x_6^0'=x_6^0, (-2+w_5^0 <= 0 /\ -2+w_5^0 == 0 /\ 2-w_5^0 <= 0), cost: 1 made implied equalities explicit Original rule: l12 -> l0 : result_4^0'=result_4^0, w_5^0'=1, x_6^0'=x_6^0, (-2+w_5^0 <= 0 /\ -2+w_5^0 == 0 /\ 2-w_5^0 <= 0), cost: 1 New rule: l12 -> l0 : result_4^0'=result_4^0, w_5^0'=1, x_6^0'=x_6^0, (-2+w_5^0 <= 0 /\ -2+w_5^0 == 0 /\ 2-w_5^0 <= 0), cost: 1 Removed Trivial Updates Original rule: l12 -> l0 : result_4^0'=result_4^0, w_5^0'=1, x_6^0'=x_6^0, (-2+w_5^0 <= 0 /\ -2+w_5^0 == 0 /\ 2-w_5^0 <= 0), cost: 1 New rule: l12 -> l0 : w_5^0'=1, (-2+w_5^0 <= 0 /\ -2+w_5^0 == 0 /\ 2-w_5^0 <= 0), cost: 1 Step with 58 Trace 58[T] Blocked [{}, {}] Step with 57 Trace 58[T], 57[(2-x_6^0 <= 0 /\ 3-w_5^0 <= 0)] Blocked [{}, {}, {}] Backtrack Trace 58[T] Blocked [{}, {57[T]}] Step with 35 Trace 58[T], 35[(-2+w_5^0 <= 0 /\ 2-x_6^0 <= 0)] Blocked [{}, {57[T]}, {}] Step with 37 Trace 58[T], 35[(-2+w_5^0 <= 0 /\ 2-x_6^0 <= 0)], 37[(3-x_6^0 <= 0)] Blocked [{}, {57[T]}, {36[T]}, {}] Step with 38 Trace 58[T], 35[(-2+w_5^0 <= 0 /\ 2-x_6^0 <= 0)], 37[(3-x_6^0 <= 0)], 38[(-1+w_5^0 <= 0)] Blocked [{}, {57[T]}, {36[T]}, {}, {}] Step with 40 Trace 58[T], 35[(-2+w_5^0 <= 0 /\ 2-x_6^0 <= 0)], 37[(3-x_6^0 <= 0)], 38[(-1+w_5^0 <= 0)], 40[T] Blocked [{}, {57[T]}, {36[T]}, {}, {}, {}] Accelerate Start location: l18 Program variables: result_4^0 w_5^0 x_6^0 35: l0 -> l2 : w_5^0'=1+w_5^0, x_6^0'=1+x_6^0, (-2+w_5^0 <= 0 /\ 2-x_6^0 <= 0), cost: 1 41: l0 -> l5 : w_5^0'=1+w_5^0, x_6^0'=1+x_6^0, (-2+w_5^0 <= 0 /\ 2-x_6^0 <= 0), cost: 1 44: l0 -> l8 : w_5^0'=1+w_5^0, x_6^0'=1+x_6^0, -1+x_6^0 <= 0, cost: 1 50: l0 -> l11 : w_5^0'=1+w_5^0, x_6^0'=1+x_6^0, -1+x_6^0 <= 0, cost: 1 53: l0 -> l14 : w_5^0'=1+w_5^0, x_6^0'=2, (1-x_6^0 == 0 /\ -1+x_6^0 <= 0), cost: 1 57: l0 -> l16 : result_4^0'=result_4^post29, (2-x_6^0 <= 0 /\ 3-w_5^0 <= 0), cost: 1 59: l0 -> l0 : w_5^0'=1, x_6^0'=2, (1-x_6^0 == 0 /\ -1+x_6^0 <= 0 /\ 1-w_5^0 == 0), cost: 1 62: l0 -> l0 : w_5^0'=n+w_5^0, x_6^0'=n+x_6^0, (-1+n >= 0 /\ 2-w_5^0 >= 0 /\ 1-n-w_5^0 >= 0 /\ -2+x_6^0 >= 0), cost: 1 36: l2 -> l3 : -1+x_6^0 <= 0, cost: 1 37: l2 -> l3 : 3-x_6^0 <= 0, cost: 1 38: l3 -> l1 : -1+w_5^0 <= 0, cost: 1 39: l3 -> l1 : 3-w_5^0 <= 0, cost: 1 40: l1 -> l0 : T, cost: 1 42: l5 -> l6 : -1+x_6^0 <= 0, cost: 1 43: l5 -> l6 : 3-x_6^0 <= 0, cost: 1 60: l6 -> l0 : w_5^0'=1, (-2+w_5^0 <= 0 /\ -2+w_5^0 == 0 /\ 2-w_5^0 <= 0), cost: 1 45: l8 -> l9 : -1+x_6^0 <= 0, cost: 1 46: l8 -> l9 : 3-x_6^0 <= 0, cost: 1 47: l9 -> l7 : -1+w_5^0 <= 0, cost: 1 48: l9 -> l7 : 3-w_5^0 <= 0, cost: 1 49: l7 -> l0 : T, cost: 1 51: l11 -> l12 : -1+x_6^0 <= 0, cost: 1 52: l11 -> l12 : 3-x_6^0 <= 0, cost: 1 61: l12 -> l0 : w_5^0'=1, (-2+w_5^0 <= 0 /\ -2+w_5^0 == 0 /\ 2-w_5^0 <= 0), cost: 1 54: l14 -> l13 : -1+w_5^0 <= 0, cost: 1 55: l14 -> l13 : 3-w_5^0 <= 0, cost: 1 56: l13 -> l0 : T, cost: 1 58: l18 -> l0 : T, cost: 1 Loop Acceleration Original rule: l0 -> l0 : w_5^0'=1+w_5^0, x_6^0'=1+x_6^0, (-2+w_5^0 <= 0 /\ 2-x_6^0 <= 0 /\ w_5^0 <= 0), cost: 1 New rule: l0 -> l0 : w_5^0'=n+w_5^0, x_6^0'=n+x_6^0, (-1+n >= 0 /\ 2-w_5^0 >= 0 /\ 1-n-w_5^0 >= 0 /\ -2+x_6^0 >= 0), cost: 1 2-w_5^0 >= 0 [0]: monotonic increase yields 2-w_5^0 >= 0, dependencies: -w_5^0 >= 0 2-w_5^0 >= 0 [1]: montonic decrease yields 3-n-w_5^0 >= 0 2-w_5^0 >= 0 [2]: eventual increase yields (1 <= 0 /\ 2-w_5^0 >= 0) -2+x_6^0 >= 0 [0]: monotonic increase yields -2+x_6^0 >= 0 -w_5^0 >= 0 [0]: montonic decrease yields 1-n-w_5^0 >= 0 -w_5^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ -w_5^0 >= 0) Replacement map: {2-w_5^0 >= 0 -> 2-w_5^0 >= 0, -2+x_6^0 >= 0 -> -2+x_6^0 >= 0, -w_5^0 >= 0 -> 1-n-w_5^0 >= 0} Trace 58[T], 62[(-1+n >= 0 /\ 2-w_5^0 >= 0 /\ 1-n-w_5^0 >= 0 /\ -2+x_6^0 >= 0)] Blocked [{}, {57[T]}, {62[T]}] Step with 35 Trace 58[T], 62[(-1+n >= 0 /\ 2-w_5^0 >= 0 /\ 1-n-w_5^0 >= 0 /\ -2+x_6^0 >= 0)], 35[(-2+w_5^0 <= 0 /\ 2-x_6^0 <= 0)] Blocked [{}, {57[T]}, {57[T], 62[T]}, {}] Step with 37 Trace 58[T], 62[(-1+n >= 0 /\ 2-w_5^0 >= 0 /\ 1-n-w_5^0 >= 0 /\ -2+x_6^0 >= 0)], 35[(-2+w_5^0 <= 0 /\ 2-x_6^0 <= 0)], 37[(3-x_6^0 <= 0)] Blocked [{}, {57[T]}, {57[T], 62[T]}, {}, {}] Step with 38 Trace 58[T], 62[(-1+n >= 0 /\ 2-w_5^0 >= 0 /\ 1-n-w_5^0 >= 0 /\ -2+x_6^0 >= 0)], 35[(-2+w_5^0 <= 0 /\ 2-x_6^0 <= 0)], 37[(3-x_6^0 <= 0)], 38[(-1+w_5^0 <= 0)] Blocked [{}, {57[T]}, {57[T], 62[T]}, {}, {}, {}] Step with 40 Trace 58[T], 62[(-1+n >= 0 /\ 2-w_5^0 >= 0 /\ 1-n-w_5^0 >= 0 /\ -2+x_6^0 >= 0)], 35[(-2+w_5^0 <= 0 /\ 2-x_6^0 <= 0)], 37[(3-x_6^0 <= 0)], 38[(-1+w_5^0 <= 0)], 40[T] Blocked [{}, {57[T]}, {57[T], 62[T]}, {}, {}, {}, {}] Covered Trace 58[T], 62[(-1+n >= 0 /\ 2-w_5^0 >= 0 /\ 1-n-w_5^0 >= 0 /\ -2+x_6^0 >= 0)], 35[(-2+w_5^0 <= 0 /\ 2-x_6^0 <= 0)], 37[(3-x_6^0 <= 0)], 38[(-1+w_5^0 <= 0)] Blocked [{}, {57[T]}, {57[T], 62[T]}, {}, {}, {40[T]}] Backtrack Trace 58[T], 62[(-1+n >= 0 /\ 2-w_5^0 >= 0 /\ 1-n-w_5^0 >= 0 /\ -2+x_6^0 >= 0)], 35[(-2+w_5^0 <= 0 /\ 2-x_6^0 <= 0)], 37[(3-x_6^0 <= 0)] Blocked [{}, {57[T]}, {57[T], 62[T]}, {}, {38[T]}] Backtrack Trace 58[T], 62[(-1+n >= 0 /\ 2-w_5^0 >= 0 /\ 1-n-w_5^0 >= 0 /\ -2+x_6^0 >= 0)], 35[(-2+w_5^0 <= 0 /\ 2-x_6^0 <= 0)] Blocked [{}, {57[T]}, {57[T], 62[T]}, {37[T]}] Backtrack Trace 58[T], 62[(-1+n >= 0 /\ 2-w_5^0 >= 0 /\ 1-n-w_5^0 >= 0 /\ -2+x_6^0 >= 0)] Blocked [{}, {57[T]}, {35[T], 57[T], 62[T]}] Step with 41 Trace 58[T], 62[(-1+n >= 0 /\ 2-w_5^0 >= 0 /\ 1-n-w_5^0 >= 0 /\ -2+x_6^0 >= 0)], 41[(-2+w_5^0 <= 0 /\ 2-x_6^0 <= 0)] Blocked [{}, {57[T]}, {35[T], 57[T], 62[T]}, {}] Step with 43 Trace 58[T], 62[(-1+n >= 0 /\ 2-w_5^0 >= 0 /\ 1-n-w_5^0 >= 0 /\ -2+x_6^0 >= 0)], 41[(-2+w_5^0 <= 0 /\ 2-x_6^0 <= 0)], 43[(3-x_6^0 <= 0)] Blocked [{}, {57[T]}, {35[T], 57[T], 62[T]}, {42[T]}, {}] Step with 60 Trace 58[T], 62[(-1+n >= 0 /\ 2-w_5^0 >= 0 /\ 1-n-w_5^0 >= 0 /\ -2+x_6^0 >= 0)], 41[(-2+w_5^0 <= 0 /\ 2-x_6^0 <= 0)], 43[(3-x_6^0 <= 0)], 60[(-2+w_5^0 <= 0 /\ -2+w_5^0 == 0 /\ 2-w_5^0 <= 0)] Blocked [{}, {57[T]}, {35[T], 57[T], 62[T]}, {42[T]}, {}, {}] Nonterm Start location: l18 Program variables: result_4^0 w_5^0 x_6^0 35: l0 -> l2 : w_5^0'=1+w_5^0, x_6^0'=1+x_6^0, (-2+w_5^0 <= 0 /\ 2-x_6^0 <= 0), cost: 1 41: l0 -> l5 : w_5^0'=1+w_5^0, x_6^0'=1+x_6^0, (-2+w_5^0 <= 0 /\ 2-x_6^0 <= 0), cost: 1 44: l0 -> l8 : w_5^0'=1+w_5^0, x_6^0'=1+x_6^0, -1+x_6^0 <= 0, cost: 1 50: l0 -> l11 : w_5^0'=1+w_5^0, x_6^0'=1+x_6^0, -1+x_6^0 <= 0, cost: 1 53: l0 -> l14 : w_5^0'=1+w_5^0, x_6^0'=2, (1-x_6^0 == 0 /\ -1+x_6^0 <= 0), cost: 1 57: l0 -> l16 : result_4^0'=result_4^post29, (2-x_6^0 <= 0 /\ 3-w_5^0 <= 0), cost: 1 59: l0 -> l0 : w_5^0'=1, x_6^0'=2, (1-x_6^0 == 0 /\ -1+x_6^0 <= 0 /\ 1-w_5^0 == 0), cost: 1 62: l0 -> l0 : w_5^0'=n+w_5^0, x_6^0'=n+x_6^0, (-1+n >= 0 /\ 2-w_5^0 >= 0 /\ 1-n-w_5^0 >= 0 /\ -2+x_6^0 >= 0), cost: 1 63: l0 -> LoAT_sink : (-1+n2 >= 0 /\ 2-w_5^0 >= 0 /\ -2+x_6^0 >= 0 /\ 1-w_5^0 >= 0 /\ -1+w_5^0 >= 0), cost: NONTERM 64: l0 -> l0 : w_5^0'=1, x_6^0'=n2+x_6^0, (-1+n2 >= 0 /\ 2-w_5^0 >= 0 /\ -2+x_6^0 >= 0 /\ 1-w_5^0 >= 0 /\ -1+w_5^0 >= 0), cost: 1 36: l2 -> l3 : -1+x_6^0 <= 0, cost: 1 37: l2 -> l3 : 3-x_6^0 <= 0, cost: 1 38: l3 -> l1 : -1+w_5^0 <= 0, cost: 1 39: l3 -> l1 : 3-w_5^0 <= 0, cost: 1 40: l1 -> l0 : T, cost: 1 42: l5 -> l6 : -1+x_6^0 <= 0, cost: 1 43: l5 -> l6 : 3-x_6^0 <= 0, cost: 1 60: l6 -> l0 : w_5^0'=1, (-2+w_5^0 <= 0 /\ -2+w_5^0 == 0 /\ 2-w_5^0 <= 0), cost: 1 45: l8 -> l9 : -1+x_6^0 <= 0, cost: 1 46: l8 -> l9 : 3-x_6^0 <= 0, cost: 1 47: l9 -> l7 : -1+w_5^0 <= 0, cost: 1 48: l9 -> l7 : 3-w_5^0 <= 0, cost: 1 49: l7 -> l0 : T, cost: 1 51: l11 -> l12 : -1+x_6^0 <= 0, cost: 1 52: l11 -> l12 : 3-x_6^0 <= 0, cost: 1 61: l12 -> l0 : w_5^0'=1, (-2+w_5^0 <= 0 /\ -2+w_5^0 == 0 /\ 2-w_5^0 <= 0), cost: 1 54: l14 -> l13 : -1+w_5^0 <= 0, cost: 1 55: l14 -> l13 : 3-w_5^0 <= 0, cost: 1 56: l13 -> l0 : T, cost: 1 58: l18 -> l0 : T, cost: 1 Certificate of Non-Termination Original rule: l0 -> l0 : w_5^0'=1, x_6^0'=1+x_6^0, (-2+w_5^0 <= 0 /\ 2-x_6^0 <= 0 /\ 1-w_5^0 <= 0 /\ -1+w_5^0 <= 0 /\ -1+w_5^0 == 0), cost: 1 New rule: l0 -> LoAT_sink : (-1+n2 >= 0 /\ 2-w_5^0 >= 0 /\ -2+x_6^0 >= 0 /\ 1-w_5^0 >= 0 /\ -1+w_5^0 >= 0), cost: NONTERM 2-w_5^0 >= 0 [0]: monotonic increase yields 2-w_5^0 >= 0 -2+x_6^0 >= 0 [0]: monotonic increase yields -2+x_6^0 >= 0 1-w_5^0 >= 0 [0]: monotonic increase yields 1-w_5^0 >= 0 -1+w_5^0 >= 0 [0]: monotonic increase yields -1+w_5^0 >= 0 Replacement map: {2-w_5^0 >= 0 -> 2-w_5^0 >= 0, -2+x_6^0 >= 0 -> -2+x_6^0 >= 0, 1-w_5^0 >= 0 -> 1-w_5^0 >= 0, -1+w_5^0 >= 0 -> -1+w_5^0 >= 0} Loop Acceleration Original rule: l0 -> l0 : w_5^0'=1, x_6^0'=1+x_6^0, (-2+w_5^0 <= 0 /\ 2-x_6^0 <= 0 /\ 1-w_5^0 <= 0 /\ -1+w_5^0 <= 0 /\ -1+w_5^0 == 0), cost: 1 New rule: l0 -> l0 : w_5^0'=1, x_6^0'=n2+x_6^0, (-1+n2 >= 0 /\ 2-w_5^0 >= 0 /\ -2+x_6^0 >= 0 /\ 1-w_5^0 >= 0 /\ -1+w_5^0 >= 0), cost: 1 2-w_5^0 >= 0 [0]: monotonic increase yields 2-w_5^0 >= 0 -2+x_6^0 >= 0 [0]: monotonic increase yields -2+x_6^0 >= 0 1-w_5^0 >= 0 [0]: monotonic increase yields 1-w_5^0 >= 0 -1+w_5^0 >= 0 [0]: monotonic increase yields -1+w_5^0 >= 0 Replacement map: {2-w_5^0 >= 0 -> 2-w_5^0 >= 0, -2+x_6^0 >= 0 -> -2+x_6^0 >= 0, 1-w_5^0 >= 0 -> 1-w_5^0 >= 0, -1+w_5^0 >= 0 -> -1+w_5^0 >= 0} Step with 63 Trace 58[T], 62[(-1+n >= 0 /\ 2-w_5^0 >= 0 /\ 1-n-w_5^0 >= 0 /\ -2+x_6^0 >= 0)], 63[(-1+n2 >= 0 /\ 2-w_5^0 >= 0 /\ -2+x_6^0 >= 0 /\ 1-w_5^0 >= 0 /\ -1+w_5^0 >= 0)] Blocked [{}, {57[T]}, {35[T], 57[T], 62[T]}, {63[T]}] Refute Counterexample [ result_4^0=0 w_5^0=0 x_6^0=2 ] 58 [ result_4^0=0 w_5^0=1 x_6^0=3 ] 62 [ result_4^0=0 w_5^0=0 x_6^0=2 ] 63 NO Build SHA: a05f16bf13df659c382799650051f91bf6828c7b