NO Initial ITS Start location: l31 Program variables: r0^0 r^0 x1^0 x^0 0: l0 -> l1 : r0^0'=r0^post1, r^0'=r^post1, x1^0'=x1^post1, x^0'=x^post1, (-r0^0 <= 0 /\ -x1^post1+x1^0 == 0 /\ -x^post1+x^0 == 0 /\ r0^0 <= 0 /\ -r0^post1+r0^0 == 0 /\ -r^post1+r^0 == 0), cost: 1 1: l2 -> l3 : r0^0'=r0^post2, r^0'=r^post2, x1^0'=x1^post2, x^0'=x^post2, (-x^post2+x^0 == 0 /\ r0^0-r0^post2 == 0 /\ -x1^post2+x1^0 == 0 /\ -r^post2+r^0 == 0 /\ 1-r^0 <= 0 /\ -1+r^0 <= 0), cost: 1 2: l4 -> l3 : r0^0'=r0^post3, r^0'=r^post3, x1^0'=x1^post3, x^0'=x^post3, (x^0-x^post3 == 0 /\ x1^0-x1^post3 == 0 /\ -r0^post3+r0^0 == 0 /\ -r^post3+r^0 == 0 /\ 1-r^0 <= 0 /\ -1+r^0 <= 0), cost: 1 3: l5 -> l3 : r0^0'=r0^post4, r^0'=r^post4, x1^0'=x1^post4, x^0'=x^post4, (-x^post4+x^0 == 0 /\ -r0^post4+r0^0 == 0 /\ -r^post4+r^0 == 0 /\ x1^0-x1^post4 == 0 /\ 1-r^0 <= 0 /\ -1+r^0 <= 0), cost: 1 4: l6 -> l7 : r0^0'=r0^post5, r^0'=r^post5, x1^0'=x1^post5, x^0'=x^post5, (x1^post5-x^0 == 0 /\ -x^post5+x^0 == 0 /\ -r0^post5+r0^0 == 0 /\ -r^post5+r^0 == 0), cost: 1 5: l6 -> l8 : r0^0'=r0^post6, r^0'=r^post6, x1^0'=x1^post6, x^0'=x^post6, (-r^post6+r^0 == 0 /\ -x1^post6+x1^0 == 0 /\ -x^post6+x^0 == 0 /\ -r0^post6+r0^0 == 0), cost: 1 7: l6 -> l3 : r0^0'=r0^post8, r^0'=r^post8, x1^0'=x1^post8, x^0'=x^post8, (x1^0-x1^post8 == 0 /\ -r0^post8+r0^0 == 0 /\ -r^post8+r^0 == 0 /\ -x^post8+x^0 == 0), cost: 1 8: l7 -> l9 : r0^0'=r0^post9, r^0'=r^post9, x1^0'=x1^post9, x^0'=x^post9, (-1+x1^0 <= 0 /\ -r0^post9+r0^0 == 0 /\ -r^post9+r^0 == 0 /\ x1^0-x1^post9 == 0 /\ -x^post9+x^0 == 0), cost: 1 9: l7 -> l9 : r0^0'=r0^post10, r^0'=r^post10, x1^0'=x1^post10, x^0'=x^post10, (-x1^post10+x1^0 == 0 /\ 3-x1^0 <= 0 /\ r^0-r^post10 == 0 /\ -x^post10+x^0 == 0 /\ r0^0-r0^post10 == 0), cost: 1 11: l7 -> l2 : r0^0'=r0^post12, r^0'=r^post12, x1^0'=x1^post12, x^0'=x^post12, (-x^post12+x^0 == 0 /\ -r0^post12+r0^0 == 0 /\ x1^0-x1^post12 == 0 /\ -1+r^post12 == 0), cost: 1 12: l7 -> l10 : r0^0'=r0^post13, r^0'=r^post13, x1^0'=x1^post13, x^0'=x^post13, (-r^post13+r^0 == 0 /\ -x1^post13+x1^0 == 0 /\ -x^post13+x^0 == 0 /\ -r0^post13+r0^0 == 0), cost: 1 6: l8 -> l6 : r0^0'=r0^post7, r^0'=r^post7, x1^0'=x1^post7, x^0'=x^post7, (-r^post7+r^0 == 0 /\ r0^0-r0^post7 == 0 /\ -x1^post7+x1^0 == 0 /\ -x^post7+x^0 == 0), cost: 1 10: l9 -> l2 : r0^0'=r0^post11, r^0'=r^post11, x1^0'=x1^post11, x^0'=x^post11, (r0^0-r0^post11 == 0 /\ r^post11 == 0 /\ x1^0-x1^post11 == 0 /\ -x^post11+x^0 == 0), cost: 1 13: l10 -> l7 : r0^0'=r0^post14, r^0'=r^post14, x1^0'=x1^post14, x^0'=x^post14, (r0^0-r0^post14 == 0 /\ x1^0-x1^post14 == 0 /\ -x^post14+x^0 == 0 /\ -r^post14+r^0 == 0), cost: 1 14: l11 -> l12 : r0^0'=r0^post15, r^0'=r^post15, x1^0'=x1^post15, x^0'=x^post15, (-1+x1^0 <= 0 /\ -x^post15+x^0 == 0 /\ -r0^post15+r0^0 == 0 /\ x1^0-x1^post15 == 0 /\ -r^post15+r^0 == 0), cost: 1 15: l11 -> l12 : r0^0'=r0^post16, r^0'=r^post16, x1^0'=x1^post16, x^0'=x^post16, (-x1^post16+x1^0 == 0 /\ -r^post16+r^0 == 0 /\ 3-x1^0 <= 0 /\ -x^post16+x^0 == 0 /\ -r0^post16+r0^0 == 0), cost: 1 17: l11 -> l4 : r0^0'=r0^post18, r^0'=r^post18, x1^0'=x1^post18, x^0'=x^post18, (x^0-x^post18 == 0 /\ x1^0-x1^post18 == 0 /\ -r0^post18+r0^0 == 0 /\ -1+r^post18 == 0), cost: 1 18: l11 -> l13 : r0^0'=r0^post19, r^0'=r^post19, x1^0'=x1^post19, x^0'=x^post19, (-x^post19+x^0 == 0 /\ -r0^post19+r0^0 == 0 /\ -r^post19+r^0 == 0 /\ x1^0-x1^post19 == 0), cost: 1 16: l12 -> l4 : r0^0'=r0^post17, r^0'=r^post17, x1^0'=x1^post17, x^0'=x^post17, (-x1^post17+x1^0 == 0 /\ r0^0-r0^post17 == 0 /\ -x^post17+x^0 == 0 /\ r^post17 == 0), cost: 1 19: l13 -> l11 : r0^0'=r0^post20, r^0'=r^post20, x1^0'=x1^post20, x^0'=x^post20, (-x^post20+x^0 == 0 /\ -x1^post20+x1^0 == 0 /\ -r0^post20+r0^0 == 0 /\ -r^post20+r^0 == 0), cost: 1 20: l14 -> l15 : r0^0'=r0^post21, r^0'=r^post21, x1^0'=x1^post21, x^0'=x^post21, (-1+x1^0 <= 0 /\ -x1^post21+x1^0 == 0 /\ -x^post21+x^0 == 0 /\ r0^0-r0^post21 == 0 /\ -r^post21+r^0 == 0), cost: 1 21: l14 -> l15 : r0^0'=r0^post22, r^0'=r^post22, x1^0'=x1^post22, x^0'=x^post22, (3-x1^0 <= 0 /\ -r^post22+r^0 == 0 /\ r0^0-r0^post22 == 0 /\ -x1^post22+x1^0 == 0 /\ -x^post22+x^0 == 0), cost: 1 23: l14 -> l5 : r0^0'=r0^post24, r^0'=r^post24, x1^0'=x1^post24, x^0'=x^post24, (-r0^post24+r0^0 == 0 /\ -1+r^post24 == 0 /\ x1^0-x1^post24 == 0 /\ -x^post24+x^0 == 0), cost: 1 24: l14 -> l16 : r0^0'=r0^post25, r^0'=r^post25, x1^0'=x1^post25, x^0'=x^post25, (-x^post25+x^0 == 0 /\ -r0^post25+r0^0 == 0 /\ -x1^post25+x1^0 == 0 /\ -r^post25+r^0 == 0), cost: 1 22: l15 -> l5 : r0^0'=r0^post23, r^0'=r^post23, x1^0'=x1^post23, x^0'=x^post23, (x1^0-x1^post23 == 0 /\ -r0^post23+r0^0 == 0 /\ r^post23 == 0 /\ -x^post23+x^0 == 0), cost: 1 25: l16 -> l14 : r0^0'=r0^post26, r^0'=r^post26, x1^0'=x1^post26, x^0'=x^post26, (r0^0-r0^post26 == 0 /\ -r^post26+r^0 == 0 /\ x1^0-x1^post26 == 0 /\ -x^post26+x^0 == 0), cost: 1 26: l17 -> l18 : r0^0'=r0^post27, r^0'=r^post27, x1^0'=x1^post27, x^0'=x^post27, (-1+x1^0 <= 0 /\ -r^post27+r^0 == 0 /\ -x^post27+x^0 == 0 /\ -r0^post27+r0^0 == 0 /\ x1^0-x1^post27 == 0), cost: 1 27: l17 -> l18 : r0^0'=r0^post28, r^0'=r^post28, x1^0'=x1^post28, x^0'=x^post28, (-r^post28+r^0 == 0 /\ -x1^post28+x1^0 == 0 /\ 3-x1^0 <= 0 /\ -x^post28+x^0 == 0 /\ -r0^post28+r0^0 == 0), cost: 1 29: l17 -> l2 : r0^0'=r0^post30, r^0'=r^post30, x1^0'=x1^post30, x^0'=x^post30, (-x^post30+x^0 == 0 /\ -r0^post30+r0^0 == 0 /\ x1^0-x1^post30 == 0 /\ -1+r^post30 == 0), cost: 1 30: l17 -> l7 : r0^0'=r0^post31, r^0'=r^post31, x1^0'=x1^post31, x^0'=x^post31, (-x1^post31+x1^0 == 0 /\ -r^post31+r^0 == 0 /\ -2+x^post31 == 0 /\ -r0^post31+r0^0 == 0), cost: 1 28: l18 -> l2 : r0^0'=r0^post29, r^0'=r^post29, x1^0'=x1^post29, x^0'=x^post29, (-r0^post29+r0^0 == 0 /\ -x^post29+x^0 == 0 /\ -x1^post29+x1^0 == 0 /\ r^post29 == 0), cost: 1 31: l19 -> l20 : r0^0'=r0^post32, r^0'=r^post32, x1^0'=x1^post32, x^0'=x^post32, (-1+x1^0 <= 0 /\ -r^post32+r^0 == 0 /\ -x1^post32+x1^0 == 0 /\ -x^post32+x^0 == 0 /\ -r0^post32+r0^0 == 0), cost: 1 32: l19 -> l20 : r0^0'=r0^post33, r^0'=r^post33, x1^0'=x1^post33, x^0'=x^post33, (-r^post33+r^0 == 0 /\ r0^0-r0^post33 == 0 /\ -x1^post33+x1^0 == 0 /\ 3-x1^0 <= 0 /\ -x^post33+x^0 == 0), cost: 1 34: l19 -> l4 : r0^0'=r0^post35, r^0'=r^post35, x1^0'=x1^post35, x^0'=x^post35, (-x1^post35+x1^0 == 0 /\ -x^post35+x^0 == 0 /\ -1+r^post35 == 0 /\ -r0^post35+r0^0 == 0), cost: 1 35: l19 -> l11 : r0^0'=r0^post36, r^0'=r^post36, x1^0'=x1^post36, x^0'=x^post36, (-x1^post36+x1^0 == 0 /\ r0^0-r0^post36 == 0 /\ -2+x^post36 == 0 /\ -r^post36+r^0 == 0), cost: 1 33: l20 -> l4 : r0^0'=r0^post34, r^0'=r^post34, x1^0'=x1^post34, x^0'=x^post34, (-x^post34+x^0 == 0 /\ -r0^post34+r0^0 == 0 /\ r^post34 == 0 /\ x1^0-x1^post34 == 0), cost: 1 36: l21 -> l22 : r0^0'=r0^post37, r^0'=r^post37, x1^0'=x1^post37, x^0'=x^post37, (-1+x1^0 <= 0 /\ r0^0-r0^post37 == 0 /\ x1^0-x1^post37 == 0 /\ -x^post37+x^0 == 0 /\ -r^post37+r^0 == 0), cost: 1 37: l21 -> l22 : r0^0'=r0^post38, r^0'=r^post38, x1^0'=x1^post38, x^0'=x^post38, (x1^0-x1^post38 == 0 /\ -r0^post38+r0^0 == 0 /\ -r^post38+r^0 == 0 /\ 3-x1^0 <= 0 /\ -x^post38+x^0 == 0), cost: 1 39: l21 -> l5 : r0^0'=r0^post40, r^0'=r^post40, x1^0'=x1^post40, x^0'=x^post40, (-x^post40+x^0 == 0 /\ -r0^post40+r0^0 == 0 /\ -x1^post40+x1^0 == 0 /\ -1+r^post40 == 0), cost: 1 40: l21 -> l14 : r0^0'=r0^post41, r^0'=r^post41, x1^0'=x1^post41, x^0'=x^post41, (r0^0-r0^post41 == 0 /\ -2+x^post41 == 0 /\ -r^post41+r^0 == 0 /\ -x1^post41+x1^0 == 0), cost: 1 38: l22 -> l5 : r0^0'=r0^post39, r^0'=r^post39, x1^0'=x1^post39, x^0'=x^post39, (-x^post39+x^0 == 0 /\ -r0^post39+r0^0 == 0 /\ r^post39 == 0 /\ x1^0-x1^post39 == 0), cost: 1 41: l23 -> l24 : r0^0'=r0^post42, r^0'=r^post42, x1^0'=x1^post42, x^0'=x^post42, (-1+x1^0 <= 0 /\ -r^post42+r^0 == 0 /\ -x^post42+x^0 == 0 /\ -r0^post42+r0^0 == 0 /\ x1^0-x1^post42 == 0), cost: 1 42: l23 -> l24 : r0^0'=r0^post43, r^0'=r^post43, x1^0'=x1^post43, x^0'=x^post43, (-r0^post43+r0^0 == 0 /\ 3-x1^0 <= 0 /\ -r^post43+r^0 == 0 /\ x1^0-x1^post43 == 0 /\ -x^post43+x^0 == 0), cost: 1 44: l23 -> l2 : r0^0'=r0^post45, r^0'=r^post45, x1^0'=x1^post45, x^0'=x^post45, (-1+r^post45 == 0 /\ r0^0-r0^post45 == 0 /\ -x^post45+x^0 == 0 /\ -x1^post45+x1^0 == 0), cost: 1 45: l23 -> l17 : r0^0'=r0^post46, r^0'=r^post46, x1^0'=x1^post46, x^0'=x^post46, (-r^post46+r^0 == 0 /\ -x1^post46+x1^0 == 0 /\ -1+x^post46 == 0 /\ -r0^post46+r0^0 == 0), cost: 1 43: l24 -> l2 : r0^0'=r0^post44, r^0'=r^post44, x1^0'=x1^post44, x^0'=x^post44, (-r0^post44+r0^0 == 0 /\ -x1^post44+x1^0 == 0 /\ -x^post44+x^0 == 0 /\ r^post44 == 0), cost: 1 46: l25 -> l26 : r0^0'=r0^post47, r^0'=r^post47, x1^0'=x1^post47, x^0'=x^post47, (-1+x1^0 <= 0 /\ -r^post47+r^0 == 0 /\ -x1^post47+x1^0 == 0 /\ -x^post47+x^0 == 0 /\ -r0^post47+r0^0 == 0), cost: 1 47: l25 -> l26 : r0^0'=r0^post48, r^0'=r^post48, x1^0'=x1^post48, x^0'=x^post48, (r0^0-r0^post48 == 0 /\ -r^post48+r^0 == 0 /\ -x1^post48+x1^0 == 0 /\ 3-x1^0 <= 0 /\ -x^post48+x^0 == 0), cost: 1 49: l25 -> l4 : r0^0'=r0^post50, r^0'=r^post50, x1^0'=x1^post50, x^0'=x^post50, (-x^post50+x^0 == 0 /\ -x1^post50+x1^0 == 0 /\ -1+r^post50 == 0 /\ -r0^post50+r0^0 == 0), cost: 1 50: l25 -> l19 : r0^0'=r0^post51, r^0'=r^post51, x1^0'=x1^post51, x^0'=x^post51, (-1+x^post51 == 0 /\ -x1^post51+x1^0 == 0 /\ r0^0-r0^post51 == 0 /\ -r^post51+r^0 == 0), cost: 1 48: l26 -> l4 : r0^0'=r0^post49, r^0'=r^post49, x1^0'=x1^post49, x^0'=x^post49, (x1^0-x1^post49 == 0 /\ -r0^post49+r0^0 == 0 /\ r^post49 == 0 /\ -x^post49+x^0 == 0), cost: 1 51: l27 -> l28 : r0^0'=r0^post52, r^0'=r^post52, x1^0'=x1^post52, x^0'=x^post52, (-1+x1^0 <= 0 /\ r0^0-r0^post52 == 0 /\ x1^0-x1^post52 == 0 /\ -x^post52+x^0 == 0 /\ -r^post52+r^0 == 0), cost: 1 52: l27 -> l28 : r0^0'=r0^post53, r^0'=r^post53, x1^0'=x1^post53, x^0'=x^post53, (-r^post53+r^0 == 0 /\ 3-x1^0 <= 0 /\ -x^post53+x^0 == 0 /\ -r0^post53+r0^0 == 0 /\ x1^0-x1^post53 == 0), cost: 1 54: l27 -> l5 : r0^0'=r0^post55, r^0'=r^post55, x1^0'=x1^post55, x^0'=x^post55, (-x^post55+x^0 == 0 /\ -r0^post55+r0^0 == 0 /\ -x1^post55+x1^0 == 0 /\ -1+r^post55 == 0), cost: 1 55: l27 -> l21 : r0^0'=r0^post56, r^0'=r^post56, x1^0'=x1^post56, x^0'=x^post56, (r0^0-r0^post56 == 0 /\ -1+x^post56 == 0 /\ -r^post56+r^0 == 0 /\ -x1^post56+x1^0 == 0), cost: 1 53: l28 -> l5 : r0^0'=r0^post54, r^0'=r^post54, x1^0'=x1^post54, x^0'=x^post54, (-x^post54+x^0 == 0 /\ -r0^post54+r0^0 == 0 /\ r^post54 == 0 /\ x1^0-x1^post54 == 0), cost: 1 56: l29 -> l19 : r0^0'=r0^post57, r^0'=r^post57, x1^0'=x1^post57, x^0'=x^post57, (x^0-x^post57 == 0 /\ x1^post57-x^0 == 0 /\ -r0^post57+r0^0 == 0 /\ -r^post57+r^0 == 0), cost: 1 57: l29 -> l6 : r0^0'=r0^post58, r^0'=r^post58, x1^0'=x1^post58, x^0'=x^post58, (-r0^post58+r0^0 == 0 /\ -2+x^post58 == 0 /\ -r^post58+r^0 == 0 /\ x1^0-x1^post58 == 0), cost: 1 58: l29 -> l3 : r0^0'=r0^post59, r^0'=r^post59, x1^0'=x1^post59, x^0'=x^post59, (-r0^post59+r0^0 == 0 /\ -r^post59+r^0 == 0 /\ -x^post59+x^0 == 0 /\ -x1^post59+x1^0 == 0), cost: 1 59: l30 -> l27 : r0^0'=r0^post60, r^0'=r^post60, x1^0'=x1^post60, x^0'=x^post60, (-r^post60+r^0 == 0 /\ r0^0-r0^post60 == 0 /\ x1^post60-x^0 == 0 /\ -x^post60+x^0 == 0), cost: 1 60: l30 -> l29 : r0^0'=r0^post61, r^0'=r^post61, x1^0'=x1^post61, x^0'=x^post61, (x1^0-x1^post61 == 0 /\ -r0^post61+r0^0 == 0 /\ -r^post61+r^0 == 0 /\ -1+x^post61 == 0), cost: 1 61: l30 -> l3 : r0^0'=r0^post62, r^0'=r^post62, x1^0'=x1^post62, x^0'=x^post62, (-r^post62+r^0 == 0 /\ r0^0-r0^post62 == 0 /\ -x1^post62+x1^0 == 0 /\ -x^post62+x^0 == 0), cost: 1 62: l31 -> l30 : r0^0'=r0^post63, r^0'=r^post63, x1^0'=x1^post63, x^0'=x^post63, (x1^0-x1^post63 == 0 /\ -r0^post63+r0^0 == 0 /\ -r^post63+r^0 == 0 /\ -x^post63+x^0 == 0), cost: 1 Chained Linear Paths Start location: l31 Program variables: r0^0 r^0 x1^0 x^0 0: l0 -> l1 : r0^0'=r0^post1, r^0'=r^post1, x1^0'=x1^post1, x^0'=x^post1, (-r0^0 <= 0 /\ -x1^post1+x1^0 == 0 /\ -x^post1+x^0 == 0 /\ r0^0 <= 0 /\ -r0^post1+r0^0 == 0 /\ -r^post1+r^0 == 0), cost: 1 1: l2 -> l3 : r0^0'=r0^post2, r^0'=r^post2, x1^0'=x1^post2, x^0'=x^post2, (-x^post2+x^0 == 0 /\ r0^0-r0^post2 == 0 /\ -x1^post2+x1^0 == 0 /\ -r^post2+r^0 == 0 /\ 1-r^0 <= 0 /\ -1+r^0 <= 0), cost: 1 2: l4 -> l3 : r0^0'=r0^post3, r^0'=r^post3, x1^0'=x1^post3, x^0'=x^post3, (x^0-x^post3 == 0 /\ x1^0-x1^post3 == 0 /\ -r0^post3+r0^0 == 0 /\ -r^post3+r^0 == 0 /\ 1-r^0 <= 0 /\ -1+r^0 <= 0), cost: 1 3: l5 -> l3 : r0^0'=r0^post4, r^0'=r^post4, x1^0'=x1^post4, x^0'=x^post4, (-x^post4+x^0 == 0 /\ -r0^post4+r0^0 == 0 /\ -r^post4+r^0 == 0 /\ x1^0-x1^post4 == 0 /\ 1-r^0 <= 0 /\ -1+r^0 <= 0), cost: 1 4: l6 -> l7 : r0^0'=r0^post5, r^0'=r^post5, x1^0'=x1^post5, x^0'=x^post5, (x1^post5-x^0 == 0 /\ -x^post5+x^0 == 0 /\ -r0^post5+r0^0 == 0 /\ -r^post5+r^0 == 0), cost: 1 7: l6 -> l3 : r0^0'=r0^post8, r^0'=r^post8, x1^0'=x1^post8, x^0'=x^post8, (x1^0-x1^post8 == 0 /\ -r0^post8+r0^0 == 0 /\ -r^post8+r^0 == 0 /\ -x^post8+x^0 == 0), cost: 1 64: l6 -> l6 : r0^0'=r0^post7, r^0'=r^post7, x1^0'=x1^post7, x^0'=x^post7, (-r^post6+r^0 == 0 /\ -x1^post6+x1^0 == 0 /\ r0^post6-r0^post7 == 0 /\ -r^post7+r^post6 == 0 /\ x1^post6-x1^post7 == 0 /\ -x^post6+x^0 == 0 /\ x^post6-x^post7 == 0 /\ -r0^post6+r0^0 == 0), cost: 1 8: l7 -> l9 : r0^0'=r0^post9, r^0'=r^post9, x1^0'=x1^post9, x^0'=x^post9, (-1+x1^0 <= 0 /\ -r0^post9+r0^0 == 0 /\ -r^post9+r^0 == 0 /\ x1^0-x1^post9 == 0 /\ -x^post9+x^0 == 0), cost: 1 9: l7 -> l9 : r0^0'=r0^post10, r^0'=r^post10, x1^0'=x1^post10, x^0'=x^post10, (-x1^post10+x1^0 == 0 /\ 3-x1^0 <= 0 /\ r^0-r^post10 == 0 /\ -x^post10+x^0 == 0 /\ r0^0-r0^post10 == 0), cost: 1 11: l7 -> l2 : r0^0'=r0^post12, r^0'=r^post12, x1^0'=x1^post12, x^0'=x^post12, (-x^post12+x^0 == 0 /\ -r0^post12+r0^0 == 0 /\ x1^0-x1^post12 == 0 /\ -1+r^post12 == 0), cost: 1 65: l7 -> l7 : r0^0'=r0^post14, r^0'=r^post14, x1^0'=x1^post14, x^0'=x^post14, (-r^post13+r^0 == 0 /\ r0^post13-r0^post14 == 0 /\ -x1^post13+x1^0 == 0 /\ x1^post13-x1^post14 == 0 /\ -r^post14+r^post13 == 0 /\ -x^post13+x^0 == 0 /\ x^post13-x^post14 == 0 /\ -r0^post13+r0^0 == 0), cost: 1 10: l9 -> l2 : r0^0'=r0^post11, r^0'=r^post11, x1^0'=x1^post11, x^0'=x^post11, (r0^0-r0^post11 == 0 /\ r^post11 == 0 /\ x1^0-x1^post11 == 0 /\ -x^post11+x^0 == 0), cost: 1 14: l11 -> l12 : r0^0'=r0^post15, r^0'=r^post15, x1^0'=x1^post15, x^0'=x^post15, (-1+x1^0 <= 0 /\ -x^post15+x^0 == 0 /\ -r0^post15+r0^0 == 0 /\ x1^0-x1^post15 == 0 /\ -r^post15+r^0 == 0), cost: 1 15: l11 -> l12 : r0^0'=r0^post16, r^0'=r^post16, x1^0'=x1^post16, x^0'=x^post16, (-x1^post16+x1^0 == 0 /\ -r^post16+r^0 == 0 /\ 3-x1^0 <= 0 /\ -x^post16+x^0 == 0 /\ -r0^post16+r0^0 == 0), cost: 1 17: l11 -> l4 : r0^0'=r0^post18, r^0'=r^post18, x1^0'=x1^post18, x^0'=x^post18, (x^0-x^post18 == 0 /\ x1^0-x1^post18 == 0 /\ -r0^post18+r0^0 == 0 /\ -1+r^post18 == 0), cost: 1 66: l11 -> l11 : r0^0'=r0^post20, r^0'=r^post20, x1^0'=x1^post20, x^0'=x^post20, (x^post19-x^post20 == 0 /\ -x^post19+x^0 == 0 /\ -r0^post19+r0^0 == 0 /\ r0^post19-r0^post20 == 0 /\ -x1^post20+x1^post19 == 0 /\ -r^post19+r^0 == 0 /\ r^post19-r^post20 == 0 /\ x1^0-x1^post19 == 0), cost: 1 16: l12 -> l4 : r0^0'=r0^post17, r^0'=r^post17, x1^0'=x1^post17, x^0'=x^post17, (-x1^post17+x1^0 == 0 /\ r0^0-r0^post17 == 0 /\ -x^post17+x^0 == 0 /\ r^post17 == 0), cost: 1 20: l14 -> l15 : r0^0'=r0^post21, r^0'=r^post21, x1^0'=x1^post21, x^0'=x^post21, (-1+x1^0 <= 0 /\ -x1^post21+x1^0 == 0 /\ -x^post21+x^0 == 0 /\ r0^0-r0^post21 == 0 /\ -r^post21+r^0 == 0), cost: 1 21: l14 -> l15 : r0^0'=r0^post22, r^0'=r^post22, x1^0'=x1^post22, x^0'=x^post22, (3-x1^0 <= 0 /\ -r^post22+r^0 == 0 /\ r0^0-r0^post22 == 0 /\ -x1^post22+x1^0 == 0 /\ -x^post22+x^0 == 0), cost: 1 23: l14 -> l5 : r0^0'=r0^post24, r^0'=r^post24, x1^0'=x1^post24, x^0'=x^post24, (-r0^post24+r0^0 == 0 /\ -1+r^post24 == 0 /\ x1^0-x1^post24 == 0 /\ -x^post24+x^0 == 0), cost: 1 63: l14 -> l14 : r0^0'=r0^post26, r^0'=r^post26, x1^0'=x1^post26, x^0'=x^post26, (-x^post25+x^0 == 0 /\ -r0^post25+r0^0 == 0 /\ x^post25-x^post26 == 0 /\ -r^post26+r^post25 == 0 /\ -x1^post25+x1^0 == 0 /\ -r^post25+r^0 == 0 /\ x1^post25-x1^post26 == 0 /\ r0^post25-r0^post26 == 0), cost: 1 22: l15 -> l5 : r0^0'=r0^post23, r^0'=r^post23, x1^0'=x1^post23, x^0'=x^post23, (x1^0-x1^post23 == 0 /\ -r0^post23+r0^0 == 0 /\ r^post23 == 0 /\ -x^post23+x^0 == 0), cost: 1 26: l17 -> l18 : r0^0'=r0^post27, r^0'=r^post27, x1^0'=x1^post27, x^0'=x^post27, (-1+x1^0 <= 0 /\ -r^post27+r^0 == 0 /\ -x^post27+x^0 == 0 /\ -r0^post27+r0^0 == 0 /\ x1^0-x1^post27 == 0), cost: 1 27: l17 -> l18 : r0^0'=r0^post28, r^0'=r^post28, x1^0'=x1^post28, x^0'=x^post28, (-r^post28+r^0 == 0 /\ -x1^post28+x1^0 == 0 /\ 3-x1^0 <= 0 /\ -x^post28+x^0 == 0 /\ -r0^post28+r0^0 == 0), cost: 1 29: l17 -> l2 : r0^0'=r0^post30, r^0'=r^post30, x1^0'=x1^post30, x^0'=x^post30, (-x^post30+x^0 == 0 /\ -r0^post30+r0^0 == 0 /\ x1^0-x1^post30 == 0 /\ -1+r^post30 == 0), cost: 1 30: l17 -> l7 : r0^0'=r0^post31, r^0'=r^post31, x1^0'=x1^post31, x^0'=x^post31, (-x1^post31+x1^0 == 0 /\ -r^post31+r^0 == 0 /\ -2+x^post31 == 0 /\ -r0^post31+r0^0 == 0), cost: 1 28: l18 -> l2 : r0^0'=r0^post29, r^0'=r^post29, x1^0'=x1^post29, x^0'=x^post29, (-r0^post29+r0^0 == 0 /\ -x^post29+x^0 == 0 /\ -x1^post29+x1^0 == 0 /\ r^post29 == 0), cost: 1 31: l19 -> l20 : r0^0'=r0^post32, r^0'=r^post32, x1^0'=x1^post32, x^0'=x^post32, (-1+x1^0 <= 0 /\ -r^post32+r^0 == 0 /\ -x1^post32+x1^0 == 0 /\ -x^post32+x^0 == 0 /\ -r0^post32+r0^0 == 0), cost: 1 32: l19 -> l20 : r0^0'=r0^post33, r^0'=r^post33, x1^0'=x1^post33, x^0'=x^post33, (-r^post33+r^0 == 0 /\ r0^0-r0^post33 == 0 /\ -x1^post33+x1^0 == 0 /\ 3-x1^0 <= 0 /\ -x^post33+x^0 == 0), cost: 1 34: l19 -> l4 : r0^0'=r0^post35, r^0'=r^post35, x1^0'=x1^post35, x^0'=x^post35, (-x1^post35+x1^0 == 0 /\ -x^post35+x^0 == 0 /\ -1+r^post35 == 0 /\ -r0^post35+r0^0 == 0), cost: 1 35: l19 -> l11 : r0^0'=r0^post36, r^0'=r^post36, x1^0'=x1^post36, x^0'=x^post36, (-x1^post36+x1^0 == 0 /\ r0^0-r0^post36 == 0 /\ -2+x^post36 == 0 /\ -r^post36+r^0 == 0), cost: 1 33: l20 -> l4 : r0^0'=r0^post34, r^0'=r^post34, x1^0'=x1^post34, x^0'=x^post34, (-x^post34+x^0 == 0 /\ -r0^post34+r0^0 == 0 /\ r^post34 == 0 /\ x1^0-x1^post34 == 0), cost: 1 36: l21 -> l22 : r0^0'=r0^post37, r^0'=r^post37, x1^0'=x1^post37, x^0'=x^post37, (-1+x1^0 <= 0 /\ r0^0-r0^post37 == 0 /\ x1^0-x1^post37 == 0 /\ -x^post37+x^0 == 0 /\ -r^post37+r^0 == 0), cost: 1 37: l21 -> l22 : r0^0'=r0^post38, r^0'=r^post38, x1^0'=x1^post38, x^0'=x^post38, (x1^0-x1^post38 == 0 /\ -r0^post38+r0^0 == 0 /\ -r^post38+r^0 == 0 /\ 3-x1^0 <= 0 /\ -x^post38+x^0 == 0), cost: 1 39: l21 -> l5 : r0^0'=r0^post40, r^0'=r^post40, x1^0'=x1^post40, x^0'=x^post40, (-x^post40+x^0 == 0 /\ -r0^post40+r0^0 == 0 /\ -x1^post40+x1^0 == 0 /\ -1+r^post40 == 0), cost: 1 40: l21 -> l14 : r0^0'=r0^post41, r^0'=r^post41, x1^0'=x1^post41, x^0'=x^post41, (r0^0-r0^post41 == 0 /\ -2+x^post41 == 0 /\ -r^post41+r^0 == 0 /\ -x1^post41+x1^0 == 0), cost: 1 38: l22 -> l5 : r0^0'=r0^post39, r^0'=r^post39, x1^0'=x1^post39, x^0'=x^post39, (-x^post39+x^0 == 0 /\ -r0^post39+r0^0 == 0 /\ r^post39 == 0 /\ x1^0-x1^post39 == 0), cost: 1 41: l23 -> l24 : r0^0'=r0^post42, r^0'=r^post42, x1^0'=x1^post42, x^0'=x^post42, (-1+x1^0 <= 0 /\ -r^post42+r^0 == 0 /\ -x^post42+x^0 == 0 /\ -r0^post42+r0^0 == 0 /\ x1^0-x1^post42 == 0), cost: 1 42: l23 -> l24 : r0^0'=r0^post43, r^0'=r^post43, x1^0'=x1^post43, x^0'=x^post43, (-r0^post43+r0^0 == 0 /\ 3-x1^0 <= 0 /\ -r^post43+r^0 == 0 /\ x1^0-x1^post43 == 0 /\ -x^post43+x^0 == 0), cost: 1 44: l23 -> l2 : r0^0'=r0^post45, r^0'=r^post45, x1^0'=x1^post45, x^0'=x^post45, (-1+r^post45 == 0 /\ r0^0-r0^post45 == 0 /\ -x^post45+x^0 == 0 /\ -x1^post45+x1^0 == 0), cost: 1 45: l23 -> l17 : r0^0'=r0^post46, r^0'=r^post46, x1^0'=x1^post46, x^0'=x^post46, (-r^post46+r^0 == 0 /\ -x1^post46+x1^0 == 0 /\ -1+x^post46 == 0 /\ -r0^post46+r0^0 == 0), cost: 1 43: l24 -> l2 : r0^0'=r0^post44, r^0'=r^post44, x1^0'=x1^post44, x^0'=x^post44, (-r0^post44+r0^0 == 0 /\ -x1^post44+x1^0 == 0 /\ -x^post44+x^0 == 0 /\ r^post44 == 0), cost: 1 46: l25 -> l26 : r0^0'=r0^post47, r^0'=r^post47, x1^0'=x1^post47, x^0'=x^post47, (-1+x1^0 <= 0 /\ -r^post47+r^0 == 0 /\ -x1^post47+x1^0 == 0 /\ -x^post47+x^0 == 0 /\ -r0^post47+r0^0 == 0), cost: 1 47: l25 -> l26 : r0^0'=r0^post48, r^0'=r^post48, x1^0'=x1^post48, x^0'=x^post48, (r0^0-r0^post48 == 0 /\ -r^post48+r^0 == 0 /\ -x1^post48+x1^0 == 0 /\ 3-x1^0 <= 0 /\ -x^post48+x^0 == 0), cost: 1 49: l25 -> l4 : r0^0'=r0^post50, r^0'=r^post50, x1^0'=x1^post50, x^0'=x^post50, (-x^post50+x^0 == 0 /\ -x1^post50+x1^0 == 0 /\ -1+r^post50 == 0 /\ -r0^post50+r0^0 == 0), cost: 1 50: l25 -> l19 : r0^0'=r0^post51, r^0'=r^post51, x1^0'=x1^post51, x^0'=x^post51, (-1+x^post51 == 0 /\ -x1^post51+x1^0 == 0 /\ r0^0-r0^post51 == 0 /\ -r^post51+r^0 == 0), cost: 1 48: l26 -> l4 : r0^0'=r0^post49, r^0'=r^post49, x1^0'=x1^post49, x^0'=x^post49, (x1^0-x1^post49 == 0 /\ -r0^post49+r0^0 == 0 /\ r^post49 == 0 /\ -x^post49+x^0 == 0), cost: 1 51: l27 -> l28 : r0^0'=r0^post52, r^0'=r^post52, x1^0'=x1^post52, x^0'=x^post52, (-1+x1^0 <= 0 /\ r0^0-r0^post52 == 0 /\ x1^0-x1^post52 == 0 /\ -x^post52+x^0 == 0 /\ -r^post52+r^0 == 0), cost: 1 52: l27 -> l28 : r0^0'=r0^post53, r^0'=r^post53, x1^0'=x1^post53, x^0'=x^post53, (-r^post53+r^0 == 0 /\ 3-x1^0 <= 0 /\ -x^post53+x^0 == 0 /\ -r0^post53+r0^0 == 0 /\ x1^0-x1^post53 == 0), cost: 1 54: l27 -> l5 : r0^0'=r0^post55, r^0'=r^post55, x1^0'=x1^post55, x^0'=x^post55, (-x^post55+x^0 == 0 /\ -r0^post55+r0^0 == 0 /\ -x1^post55+x1^0 == 0 /\ -1+r^post55 == 0), cost: 1 55: l27 -> l21 : r0^0'=r0^post56, r^0'=r^post56, x1^0'=x1^post56, x^0'=x^post56, (r0^0-r0^post56 == 0 /\ -1+x^post56 == 0 /\ -r^post56+r^0 == 0 /\ -x1^post56+x1^0 == 0), cost: 1 53: l28 -> l5 : r0^0'=r0^post54, r^0'=r^post54, x1^0'=x1^post54, x^0'=x^post54, (-x^post54+x^0 == 0 /\ -r0^post54+r0^0 == 0 /\ r^post54 == 0 /\ x1^0-x1^post54 == 0), cost: 1 56: l29 -> l19 : r0^0'=r0^post57, r^0'=r^post57, x1^0'=x1^post57, x^0'=x^post57, (x^0-x^post57 == 0 /\ x1^post57-x^0 == 0 /\ -r0^post57+r0^0 == 0 /\ -r^post57+r^0 == 0), cost: 1 57: l29 -> l6 : r0^0'=r0^post58, r^0'=r^post58, x1^0'=x1^post58, x^0'=x^post58, (-r0^post58+r0^0 == 0 /\ -2+x^post58 == 0 /\ -r^post58+r^0 == 0 /\ x1^0-x1^post58 == 0), cost: 1 58: l29 -> l3 : r0^0'=r0^post59, r^0'=r^post59, x1^0'=x1^post59, x^0'=x^post59, (-r0^post59+r0^0 == 0 /\ -r^post59+r^0 == 0 /\ -x^post59+x^0 == 0 /\ -x1^post59+x1^0 == 0), cost: 1 59: l30 -> l27 : r0^0'=r0^post60, r^0'=r^post60, x1^0'=x1^post60, x^0'=x^post60, (-r^post60+r^0 == 0 /\ r0^0-r0^post60 == 0 /\ x1^post60-x^0 == 0 /\ -x^post60+x^0 == 0), cost: 1 60: l30 -> l29 : r0^0'=r0^post61, r^0'=r^post61, x1^0'=x1^post61, x^0'=x^post61, (x1^0-x1^post61 == 0 /\ -r0^post61+r0^0 == 0 /\ -r^post61+r^0 == 0 /\ -1+x^post61 == 0), cost: 1 61: l30 -> l3 : r0^0'=r0^post62, r^0'=r^post62, x1^0'=x1^post62, x^0'=x^post62, (-r^post62+r^0 == 0 /\ r0^0-r0^post62 == 0 /\ -x1^post62+x1^0 == 0 /\ -x^post62+x^0 == 0), cost: 1 62: l31 -> l30 : r0^0'=r0^post63, r^0'=r^post63, x1^0'=x1^post63, x^0'=x^post63, (x1^0-x1^post63 == 0 /\ -r0^post63+r0^0 == 0 /\ -r^post63+r^0 == 0 /\ -x^post63+x^0 == 0), cost: 1 Eliminating location l16 by chaining: Applied chaining First rule: l14 -> l16 : r0^0'=r0^post25, r^0'=r^post25, x1^0'=x1^post25, x^0'=x^post25, (-x^post25+x^0 == 0 /\ -r0^post25+r0^0 == 0 /\ -x1^post25+x1^0 == 0 /\ -r^post25+r^0 == 0), cost: 1 Second rule: l16 -> l14 : r0^0'=r0^post26, r^0'=r^post26, x1^0'=x1^post26, x^0'=x^post26, (r0^0-r0^post26 == 0 /\ -r^post26+r^0 == 0 /\ x1^0-x1^post26 == 0 /\ -x^post26+x^0 == 0), cost: 1 New rule: l14 -> l14 : r0^0'=r0^post26, r^0'=r^post26, x1^0'=x1^post26, x^0'=x^post26, (-x^post25+x^0 == 0 /\ -r0^post25+r0^0 == 0 /\ x^post25-x^post26 == 0 /\ -r^post26+r^post25 == 0 /\ -x1^post25+x1^0 == 0 /\ -r^post25+r^0 == 0 /\ x1^post25-x1^post26 == 0 /\ r0^post25-r0^post26 == 0), cost: 1 Applied deletion Removed the following rules: 24 25 Eliminating location l8 by chaining: Applied chaining First rule: l6 -> l8 : r0^0'=r0^post6, r^0'=r^post6, x1^0'=x1^post6, x^0'=x^post6, (-r^post6+r^0 == 0 /\ -x1^post6+x1^0 == 0 /\ -x^post6+x^0 == 0 /\ -r0^post6+r0^0 == 0), cost: 1 Second rule: l8 -> l6 : r0^0'=r0^post7, r^0'=r^post7, x1^0'=x1^post7, x^0'=x^post7, (-r^post7+r^0 == 0 /\ r0^0-r0^post7 == 0 /\ -x1^post7+x1^0 == 0 /\ -x^post7+x^0 == 0), cost: 1 New rule: l6 -> l6 : r0^0'=r0^post7, r^0'=r^post7, x1^0'=x1^post7, x^0'=x^post7, (-r^post6+r^0 == 0 /\ -x1^post6+x1^0 == 0 /\ r0^post6-r0^post7 == 0 /\ -r^post7+r^post6 == 0 /\ x1^post6-x1^post7 == 0 /\ -x^post6+x^0 == 0 /\ x^post6-x^post7 == 0 /\ -r0^post6+r0^0 == 0), cost: 1 Applied deletion Removed the following rules: 5 6 Eliminating location l10 by chaining: Applied chaining First rule: l7 -> l10 : r0^0'=r0^post13, r^0'=r^post13, x1^0'=x1^post13, x^0'=x^post13, (-r^post13+r^0 == 0 /\ -x1^post13+x1^0 == 0 /\ -x^post13+x^0 == 0 /\ -r0^post13+r0^0 == 0), cost: 1 Second rule: l10 -> l7 : r0^0'=r0^post14, r^0'=r^post14, x1^0'=x1^post14, x^0'=x^post14, (r0^0-r0^post14 == 0 /\ x1^0-x1^post14 == 0 /\ -x^post14+x^0 == 0 /\ -r^post14+r^0 == 0), cost: 1 New rule: l7 -> l7 : r0^0'=r0^post14, r^0'=r^post14, x1^0'=x1^post14, x^0'=x^post14, (-r^post13+r^0 == 0 /\ r0^post13-r0^post14 == 0 /\ -x1^post13+x1^0 == 0 /\ x1^post13-x1^post14 == 0 /\ -r^post14+r^post13 == 0 /\ -x^post13+x^0 == 0 /\ x^post13-x^post14 == 0 /\ -r0^post13+r0^0 == 0), cost: 1 Applied deletion Removed the following rules: 12 13 Eliminating location l13 by chaining: Applied chaining First rule: l11 -> l13 : r0^0'=r0^post19, r^0'=r^post19, x1^0'=x1^post19, x^0'=x^post19, (-x^post19+x^0 == 0 /\ -r0^post19+r0^0 == 0 /\ -r^post19+r^0 == 0 /\ x1^0-x1^post19 == 0), cost: 1 Second rule: l13 -> l11 : r0^0'=r0^post20, r^0'=r^post20, x1^0'=x1^post20, x^0'=x^post20, (-x^post20+x^0 == 0 /\ -x1^post20+x1^0 == 0 /\ -r0^post20+r0^0 == 0 /\ -r^post20+r^0 == 0), cost: 1 New rule: l11 -> l11 : r0^0'=r0^post20, r^0'=r^post20, x1^0'=x1^post20, x^0'=x^post20, (x^post19-x^post20 == 0 /\ -x^post19+x^0 == 0 /\ -r0^post19+r0^0 == 0 /\ r0^post19-r0^post20 == 0 /\ -x1^post20+x1^post19 == 0 /\ -r^post19+r^0 == 0 /\ r^post19-r^post20 == 0 /\ x1^0-x1^post19 == 0), cost: 1 Applied deletion Removed the following rules: 18 19 Simplified Transitions Start location: l31 Program variables: r0^0 r^0 x1^0 x^0 67: l0 -> l1 : (-r0^0 <= 0 /\ -r0^0 == 0 /\ r0^0 <= 0), cost: 1 68: l2 -> l3 : (1-r^0 <= 0 /\ 1-r^0 == 0 /\ -1+r^0 <= 0), cost: 1 69: l4 -> l3 : (1-r^0 <= 0 /\ 1-r^0 == 0 /\ -1+r^0 <= 0), cost: 1 70: l5 -> l3 : (1-r^0 <= 0 /\ 1-r^0 == 0 /\ -1+r^0 <= 0), cost: 1 71: l6 -> l7 : x1^0'=x^0, T, cost: 1 72: l6 -> l3 : T, cost: 1 123: l6 -> l6 : T, cost: 1 73: l7 -> l9 : -1+x1^0 <= 0, cost: 1 74: l7 -> l9 : 3-x1^0 <= 0, cost: 1 76: l7 -> l2 : r^0'=1, T, cost: 1 124: l7 -> l7 : T, cost: 1 75: l9 -> l2 : r^0'=0, T, cost: 1 77: l11 -> l12 : -1+x1^0 <= 0, cost: 1 78: l11 -> l12 : 3-x1^0 <= 0, cost: 1 80: l11 -> l4 : r^0'=1, T, cost: 1 125: l11 -> l11 : T, cost: 1 79: l12 -> l4 : r^0'=0, T, cost: 1 81: l14 -> l15 : -1+x1^0 <= 0, cost: 1 82: l14 -> l15 : 3-x1^0 <= 0, cost: 1 84: l14 -> l5 : r^0'=1, T, cost: 1 122: l14 -> l14 : T, cost: 1 83: l15 -> l5 : r^0'=0, T, cost: 1 85: l17 -> l18 : -1+x1^0 <= 0, cost: 1 86: l17 -> l18 : 3-x1^0 <= 0, cost: 1 88: l17 -> l2 : r^0'=1, T, cost: 1 89: l17 -> l7 : x^0'=2, T, cost: 1 87: l18 -> l2 : r^0'=0, T, cost: 1 90: l19 -> l20 : -1+x1^0 <= 0, cost: 1 91: l19 -> l20 : 3-x1^0 <= 0, cost: 1 93: l19 -> l4 : r^0'=1, T, cost: 1 94: l19 -> l11 : x^0'=2, T, cost: 1 92: l20 -> l4 : r^0'=0, T, cost: 1 95: l21 -> l22 : -1+x1^0 <= 0, cost: 1 96: l21 -> l22 : 3-x1^0 <= 0, cost: 1 98: l21 -> l5 : r^0'=1, T, cost: 1 99: l21 -> l14 : x^0'=2, T, cost: 1 97: l22 -> l5 : r^0'=0, T, cost: 1 100: l23 -> l24 : -1+x1^0 <= 0, cost: 1 101: l23 -> l24 : 3-x1^0 <= 0, cost: 1 103: l23 -> l2 : r^0'=1, T, cost: 1 104: l23 -> l17 : x^0'=1, T, cost: 1 102: l24 -> l2 : r^0'=0, T, cost: 1 105: l25 -> l26 : -1+x1^0 <= 0, cost: 1 106: l25 -> l26 : 3-x1^0 <= 0, cost: 1 108: l25 -> l4 : r^0'=1, T, cost: 1 109: l25 -> l19 : x^0'=1, T, cost: 1 107: l26 -> l4 : r^0'=0, T, cost: 1 110: l27 -> l28 : -1+x1^0 <= 0, cost: 1 111: l27 -> l28 : 3-x1^0 <= 0, cost: 1 113: l27 -> l5 : r^0'=1, T, cost: 1 114: l27 -> l21 : x^0'=1, T, cost: 1 112: l28 -> l5 : r^0'=0, T, cost: 1 115: l29 -> l19 : x1^0'=x^0, T, cost: 1 116: l29 -> l6 : x^0'=2, T, cost: 1 117: l29 -> l3 : T, cost: 1 118: l30 -> l27 : x1^0'=x^0, T, cost: 1 119: l30 -> l29 : x^0'=1, T, cost: 1 120: l30 -> l3 : T, cost: 1 121: l31 -> l30 : T, cost: 1 made implied equalities explicit Original rule: l0 -> l1 : r0^0'=r0^post1, r^0'=r^post1, x1^0'=x1^post1, x^0'=x^post1, (-r0^0 <= 0 /\ -x1^post1+x1^0 == 0 /\ -x^post1+x^0 == 0 /\ r0^0 <= 0 /\ -r0^post1+r0^0 == 0 /\ -r^post1+r^0 == 0), cost: 1 New rule: l0 -> l1 : r0^0'=r0^post1, r^0'=r^post1, x1^0'=x1^post1, x^0'=x^post1, (-r0^0 <= 0 /\ -r0^0 == 0 /\ -x1^post1+x1^0 == 0 /\ -x^post1+x^0 == 0 /\ r0^0 <= 0 /\ -r0^post1+r0^0 == 0 /\ -r^post1+r^0 == 0), cost: 1 Propagated Equalities Original rule: l0 -> l1 : r0^0'=r0^post1, r^0'=r^post1, x1^0'=x1^post1, x^0'=x^post1, (-r0^0 <= 0 /\ -r0^0 == 0 /\ -x1^post1+x1^0 == 0 /\ -x^post1+x^0 == 0 /\ r0^0 <= 0 /\ -r0^post1+r0^0 == 0 /\ -r^post1+r^0 == 0), cost: 1 New rule: l0 -> l1 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (0 == 0 /\ -r0^0 <= 0 /\ -r0^0 == 0 /\ r0^0 <= 0), cost: 1 propagated equality x1^post1 = x1^0 propagated equality x^post1 = x^0 propagated equality r0^post1 = r0^0 propagated equality r^post1 = r^0 Simplified Guard Original rule: l0 -> l1 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (0 == 0 /\ -r0^0 <= 0 /\ -r0^0 == 0 /\ r0^0 <= 0), cost: 1 New rule: l0 -> l1 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (-r0^0 <= 0 /\ -r0^0 == 0 /\ r0^0 <= 0), cost: 1 made implied equalities explicit Original rule: l0 -> l1 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (-r0^0 <= 0 /\ -r0^0 == 0 /\ r0^0 <= 0), cost: 1 New rule: l0 -> l1 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (-r0^0 <= 0 /\ -r0^0 == 0 /\ r0^0 <= 0), cost: 1 Removed Trivial Updates Original rule: l0 -> l1 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (-r0^0 <= 0 /\ -r0^0 == 0 /\ r0^0 <= 0), cost: 1 New rule: l0 -> l1 : (-r0^0 <= 0 /\ -r0^0 == 0 /\ r0^0 <= 0), cost: 1 made implied equalities explicit Original rule: l2 -> l3 : r0^0'=r0^post2, r^0'=r^post2, x1^0'=x1^post2, x^0'=x^post2, (-x^post2+x^0 == 0 /\ r0^0-r0^post2 == 0 /\ -x1^post2+x1^0 == 0 /\ -r^post2+r^0 == 0 /\ 1-r^0 <= 0 /\ -1+r^0 <= 0), cost: 1 New rule: l2 -> l3 : r0^0'=r0^post2, r^0'=r^post2, x1^0'=x1^post2, x^0'=x^post2, (-x^post2+x^0 == 0 /\ r0^0-r0^post2 == 0 /\ -x1^post2+x1^0 == 0 /\ -r^post2+r^0 == 0 /\ 1-r^0 <= 0 /\ 1-r^0 == 0 /\ -1+r^0 <= 0), cost: 1 Propagated Equalities Original rule: l2 -> l3 : r0^0'=r0^post2, r^0'=r^post2, x1^0'=x1^post2, x^0'=x^post2, (-x^post2+x^0 == 0 /\ r0^0-r0^post2 == 0 /\ -x1^post2+x1^0 == 0 /\ -r^post2+r^0 == 0 /\ 1-r^0 <= 0 /\ 1-r^0 == 0 /\ -1+r^0 <= 0), cost: 1 New rule: l2 -> l3 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (0 == 0 /\ 1-r^0 <= 0 /\ 1-r^0 == 0 /\ -1+r^0 <= 0), cost: 1 propagated equality x^post2 = x^0 propagated equality r0^post2 = r0^0 propagated equality x1^post2 = x1^0 propagated equality r^post2 = r^0 Simplified Guard Original rule: l2 -> l3 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (0 == 0 /\ 1-r^0 <= 0 /\ 1-r^0 == 0 /\ -1+r^0 <= 0), cost: 1 New rule: l2 -> l3 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (1-r^0 <= 0 /\ 1-r^0 == 0 /\ -1+r^0 <= 0), cost: 1 made implied equalities explicit Original rule: l2 -> l3 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (1-r^0 <= 0 /\ 1-r^0 == 0 /\ -1+r^0 <= 0), cost: 1 New rule: l2 -> l3 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (1-r^0 <= 0 /\ 1-r^0 == 0 /\ -1+r^0 <= 0), cost: 1 Removed Trivial Updates Original rule: l2 -> l3 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (1-r^0 <= 0 /\ 1-r^0 == 0 /\ -1+r^0 <= 0), cost: 1 New rule: l2 -> l3 : (1-r^0 <= 0 /\ 1-r^0 == 0 /\ -1+r^0 <= 0), cost: 1 made implied equalities explicit Original rule: l4 -> l3 : r0^0'=r0^post3, r^0'=r^post3, x1^0'=x1^post3, x^0'=x^post3, (x^0-x^post3 == 0 /\ x1^0-x1^post3 == 0 /\ -r0^post3+r0^0 == 0 /\ -r^post3+r^0 == 0 /\ 1-r^0 <= 0 /\ -1+r^0 <= 0), cost: 1 New rule: l4 -> l3 : r0^0'=r0^post3, r^0'=r^post3, x1^0'=x1^post3, x^0'=x^post3, (x^0-x^post3 == 0 /\ x1^0-x1^post3 == 0 /\ -r0^post3+r0^0 == 0 /\ -r^post3+r^0 == 0 /\ 1-r^0 <= 0 /\ 1-r^0 == 0 /\ -1+r^0 <= 0), cost: 1 Propagated Equalities Original rule: l4 -> l3 : r0^0'=r0^post3, r^0'=r^post3, x1^0'=x1^post3, x^0'=x^post3, (x^0-x^post3 == 0 /\ x1^0-x1^post3 == 0 /\ -r0^post3+r0^0 == 0 /\ -r^post3+r^0 == 0 /\ 1-r^0 <= 0 /\ 1-r^0 == 0 /\ -1+r^0 <= 0), cost: 1 New rule: l4 -> l3 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (0 == 0 /\ 1-r^0 <= 0 /\ 1-r^0 == 0 /\ -1+r^0 <= 0), cost: 1 propagated equality x^post3 = x^0 propagated equality x1^post3 = x1^0 propagated equality r0^post3 = r0^0 propagated equality r^post3 = r^0 Simplified Guard Original rule: l4 -> l3 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (0 == 0 /\ 1-r^0 <= 0 /\ 1-r^0 == 0 /\ -1+r^0 <= 0), cost: 1 New rule: l4 -> l3 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (1-r^0 <= 0 /\ 1-r^0 == 0 /\ -1+r^0 <= 0), cost: 1 made implied equalities explicit Original rule: l4 -> l3 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (1-r^0 <= 0 /\ 1-r^0 == 0 /\ -1+r^0 <= 0), cost: 1 New rule: l4 -> l3 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (1-r^0 <= 0 /\ 1-r^0 == 0 /\ -1+r^0 <= 0), cost: 1 Removed Trivial Updates Original rule: l4 -> l3 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (1-r^0 <= 0 /\ 1-r^0 == 0 /\ -1+r^0 <= 0), cost: 1 New rule: l4 -> l3 : (1-r^0 <= 0 /\ 1-r^0 == 0 /\ -1+r^0 <= 0), cost: 1 made implied equalities explicit Original rule: l5 -> l3 : r0^0'=r0^post4, r^0'=r^post4, x1^0'=x1^post4, x^0'=x^post4, (-x^post4+x^0 == 0 /\ -r0^post4+r0^0 == 0 /\ -r^post4+r^0 == 0 /\ x1^0-x1^post4 == 0 /\ 1-r^0 <= 0 /\ -1+r^0 <= 0), cost: 1 New rule: l5 -> l3 : r0^0'=r0^post4, r^0'=r^post4, x1^0'=x1^post4, x^0'=x^post4, (-x^post4+x^0 == 0 /\ -r0^post4+r0^0 == 0 /\ -r^post4+r^0 == 0 /\ x1^0-x1^post4 == 0 /\ 1-r^0 <= 0 /\ 1-r^0 == 0 /\ -1+r^0 <= 0), cost: 1 Propagated Equalities Original rule: l5 -> l3 : r0^0'=r0^post4, r^0'=r^post4, x1^0'=x1^post4, x^0'=x^post4, (-x^post4+x^0 == 0 /\ -r0^post4+r0^0 == 0 /\ -r^post4+r^0 == 0 /\ x1^0-x1^post4 == 0 /\ 1-r^0 <= 0 /\ 1-r^0 == 0 /\ -1+r^0 <= 0), cost: 1 New rule: l5 -> l3 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (0 == 0 /\ 1-r^0 <= 0 /\ 1-r^0 == 0 /\ -1+r^0 <= 0), cost: 1 propagated equality x^post4 = x^0 propagated equality r0^post4 = r0^0 propagated equality r^post4 = r^0 propagated equality x1^post4 = x1^0 Simplified Guard Original rule: l5 -> l3 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (0 == 0 /\ 1-r^0 <= 0 /\ 1-r^0 == 0 /\ -1+r^0 <= 0), cost: 1 New rule: l5 -> l3 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (1-r^0 <= 0 /\ 1-r^0 == 0 /\ -1+r^0 <= 0), cost: 1 made implied equalities explicit Original rule: l5 -> l3 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (1-r^0 <= 0 /\ 1-r^0 == 0 /\ -1+r^0 <= 0), cost: 1 New rule: l5 -> l3 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (1-r^0 <= 0 /\ 1-r^0 == 0 /\ -1+r^0 <= 0), cost: 1 Removed Trivial Updates Original rule: l5 -> l3 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (1-r^0 <= 0 /\ 1-r^0 == 0 /\ -1+r^0 <= 0), cost: 1 New rule: l5 -> l3 : (1-r^0 <= 0 /\ 1-r^0 == 0 /\ -1+r^0 <= 0), cost: 1 Propagated Equalities Original rule: l6 -> l7 : r0^0'=r0^post5, r^0'=r^post5, x1^0'=x1^post5, x^0'=x^post5, (x1^post5-x^0 == 0 /\ -x^post5+x^0 == 0 /\ -r0^post5+r0^0 == 0 /\ -r^post5+r^0 == 0), cost: 1 New rule: l6 -> l7 : r0^0'=r0^0, r^0'=r^0, x1^0'=x^0, x^0'=x^0, 0 == 0, cost: 1 propagated equality x1^post5 = x^0 propagated equality x^post5 = x^0 propagated equality r0^post5 = r0^0 propagated equality r^post5 = r^0 Simplified Guard Original rule: l6 -> l7 : r0^0'=r0^0, r^0'=r^0, x1^0'=x^0, x^0'=x^0, 0 == 0, cost: 1 New rule: l6 -> l7 : r0^0'=r0^0, r^0'=r^0, x1^0'=x^0, x^0'=x^0, T, cost: 1 Removed Trivial Updates Original rule: l6 -> l7 : r0^0'=r0^0, r^0'=r^0, x1^0'=x^0, x^0'=x^0, T, cost: 1 New rule: l6 -> l7 : x1^0'=x^0, T, cost: 1 Propagated Equalities Original rule: l6 -> l3 : r0^0'=r0^post8, r^0'=r^post8, x1^0'=x1^post8, x^0'=x^post8, (x1^0-x1^post8 == 0 /\ -r0^post8+r0^0 == 0 /\ -r^post8+r^0 == 0 /\ -x^post8+x^0 == 0), cost: 1 New rule: l6 -> l3 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, 0 == 0, cost: 1 propagated equality x1^post8 = x1^0 propagated equality r0^post8 = r0^0 propagated equality r^post8 = r^0 propagated equality x^post8 = x^0 Simplified Guard Original rule: l6 -> l3 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, 0 == 0, cost: 1 New rule: l6 -> l3 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, T, cost: 1 Removed Trivial Updates Original rule: l6 -> l3 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, T, cost: 1 New rule: l6 -> l3 : T, cost: 1 Propagated Equalities Original rule: l7 -> l9 : r0^0'=r0^post9, r^0'=r^post9, x1^0'=x1^post9, x^0'=x^post9, (-1+x1^0 <= 0 /\ -r0^post9+r0^0 == 0 /\ -r^post9+r^0 == 0 /\ x1^0-x1^post9 == 0 /\ -x^post9+x^0 == 0), cost: 1 New rule: l7 -> l9 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (0 == 0 /\ -1+x1^0 <= 0), cost: 1 propagated equality r0^post9 = r0^0 propagated equality r^post9 = r^0 propagated equality x1^post9 = x1^0 propagated equality x^post9 = x^0 Simplified Guard Original rule: l7 -> l9 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (0 == 0 /\ -1+x1^0 <= 0), cost: 1 New rule: l7 -> l9 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, -1+x1^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l7 -> l9 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, -1+x1^0 <= 0, cost: 1 New rule: l7 -> l9 : -1+x1^0 <= 0, cost: 1 Propagated Equalities Original rule: l7 -> l9 : r0^0'=r0^post10, r^0'=r^post10, x1^0'=x1^post10, x^0'=x^post10, (-x1^post10+x1^0 == 0 /\ 3-x1^0 <= 0 /\ r^0-r^post10 == 0 /\ -x^post10+x^0 == 0 /\ r0^0-r0^post10 == 0), cost: 1 New rule: l7 -> l9 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (0 == 0 /\ 3-x1^0 <= 0), cost: 1 propagated equality x1^post10 = x1^0 propagated equality r^post10 = r^0 propagated equality x^post10 = x^0 propagated equality r0^post10 = r0^0 Simplified Guard Original rule: l7 -> l9 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (0 == 0 /\ 3-x1^0 <= 0), cost: 1 New rule: l7 -> l9 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, 3-x1^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l7 -> l9 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, 3-x1^0 <= 0, cost: 1 New rule: l7 -> l9 : 3-x1^0 <= 0, cost: 1 Propagated Equalities Original rule: l9 -> l2 : r0^0'=r0^post11, r^0'=r^post11, x1^0'=x1^post11, x^0'=x^post11, (r0^0-r0^post11 == 0 /\ r^post11 == 0 /\ x1^0-x1^post11 == 0 /\ -x^post11+x^0 == 0), cost: 1 New rule: l9 -> l2 : r0^0'=r0^0, r^0'=0, x1^0'=x1^0, x^0'=x^0, 0 == 0, cost: 1 propagated equality r0^post11 = r0^0 propagated equality r^post11 = 0 propagated equality x1^post11 = x1^0 propagated equality x^post11 = x^0 Simplified Guard Original rule: l9 -> l2 : r0^0'=r0^0, r^0'=0, x1^0'=x1^0, x^0'=x^0, 0 == 0, cost: 1 New rule: l9 -> l2 : r0^0'=r0^0, r^0'=0, x1^0'=x1^0, x^0'=x^0, T, cost: 1 Removed Trivial Updates Original rule: l9 -> l2 : r0^0'=r0^0, r^0'=0, x1^0'=x1^0, x^0'=x^0, T, cost: 1 New rule: l9 -> l2 : r^0'=0, T, cost: 1 Propagated Equalities Original rule: l7 -> l2 : r0^0'=r0^post12, r^0'=r^post12, x1^0'=x1^post12, x^0'=x^post12, (-x^post12+x^0 == 0 /\ -r0^post12+r0^0 == 0 /\ x1^0-x1^post12 == 0 /\ -1+r^post12 == 0), cost: 1 New rule: l7 -> l2 : r0^0'=r0^0, r^0'=1, x1^0'=x1^0, x^0'=x^0, 0 == 0, cost: 1 propagated equality x^post12 = x^0 propagated equality r0^post12 = r0^0 propagated equality x1^post12 = x1^0 propagated equality r^post12 = 1 Simplified Guard Original rule: l7 -> l2 : r0^0'=r0^0, r^0'=1, x1^0'=x1^0, x^0'=x^0, 0 == 0, cost: 1 New rule: l7 -> l2 : r0^0'=r0^0, r^0'=1, x1^0'=x1^0, x^0'=x^0, T, cost: 1 Removed Trivial Updates Original rule: l7 -> l2 : r0^0'=r0^0, r^0'=1, x1^0'=x1^0, x^0'=x^0, T, cost: 1 New rule: l7 -> l2 : r^0'=1, T, cost: 1 Propagated Equalities Original rule: l11 -> l12 : r0^0'=r0^post15, r^0'=r^post15, x1^0'=x1^post15, x^0'=x^post15, (-1+x1^0 <= 0 /\ -x^post15+x^0 == 0 /\ -r0^post15+r0^0 == 0 /\ x1^0-x1^post15 == 0 /\ -r^post15+r^0 == 0), cost: 1 New rule: l11 -> l12 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (0 == 0 /\ -1+x1^0 <= 0), cost: 1 propagated equality x^post15 = x^0 propagated equality r0^post15 = r0^0 propagated equality x1^post15 = x1^0 propagated equality r^post15 = r^0 Simplified Guard Original rule: l11 -> l12 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (0 == 0 /\ -1+x1^0 <= 0), cost: 1 New rule: l11 -> l12 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, -1+x1^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l11 -> l12 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, -1+x1^0 <= 0, cost: 1 New rule: l11 -> l12 : -1+x1^0 <= 0, cost: 1 Propagated Equalities Original rule: l11 -> l12 : r0^0'=r0^post16, r^0'=r^post16, x1^0'=x1^post16, x^0'=x^post16, (-x1^post16+x1^0 == 0 /\ -r^post16+r^0 == 0 /\ 3-x1^0 <= 0 /\ -x^post16+x^0 == 0 /\ -r0^post16+r0^0 == 0), cost: 1 New rule: l11 -> l12 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (0 == 0 /\ 3-x1^0 <= 0), cost: 1 propagated equality x1^post16 = x1^0 propagated equality r^post16 = r^0 propagated equality x^post16 = x^0 propagated equality r0^post16 = r0^0 Simplified Guard Original rule: l11 -> l12 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (0 == 0 /\ 3-x1^0 <= 0), cost: 1 New rule: l11 -> l12 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, 3-x1^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l11 -> l12 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, 3-x1^0 <= 0, cost: 1 New rule: l11 -> l12 : 3-x1^0 <= 0, cost: 1 Propagated Equalities Original rule: l12 -> l4 : r0^0'=r0^post17, r^0'=r^post17, x1^0'=x1^post17, x^0'=x^post17, (-x1^post17+x1^0 == 0 /\ r0^0-r0^post17 == 0 /\ -x^post17+x^0 == 0 /\ r^post17 == 0), cost: 1 New rule: l12 -> l4 : r0^0'=r0^0, r^0'=0, x1^0'=x1^0, x^0'=x^0, 0 == 0, cost: 1 propagated equality x1^post17 = x1^0 propagated equality r0^post17 = r0^0 propagated equality x^post17 = x^0 propagated equality r^post17 = 0 Simplified Guard Original rule: l12 -> l4 : r0^0'=r0^0, r^0'=0, x1^0'=x1^0, x^0'=x^0, 0 == 0, cost: 1 New rule: l12 -> l4 : r0^0'=r0^0, r^0'=0, x1^0'=x1^0, x^0'=x^0, T, cost: 1 Removed Trivial Updates Original rule: l12 -> l4 : r0^0'=r0^0, r^0'=0, x1^0'=x1^0, x^0'=x^0, T, cost: 1 New rule: l12 -> l4 : r^0'=0, T, cost: 1 Propagated Equalities Original rule: l11 -> l4 : r0^0'=r0^post18, r^0'=r^post18, x1^0'=x1^post18, x^0'=x^post18, (x^0-x^post18 == 0 /\ x1^0-x1^post18 == 0 /\ -r0^post18+r0^0 == 0 /\ -1+r^post18 == 0), cost: 1 New rule: l11 -> l4 : r0^0'=r0^0, r^0'=1, x1^0'=x1^0, x^0'=x^0, 0 == 0, cost: 1 propagated equality x^post18 = x^0 propagated equality x1^post18 = x1^0 propagated equality r0^post18 = r0^0 propagated equality r^post18 = 1 Simplified Guard Original rule: l11 -> l4 : r0^0'=r0^0, r^0'=1, x1^0'=x1^0, x^0'=x^0, 0 == 0, cost: 1 New rule: l11 -> l4 : r0^0'=r0^0, r^0'=1, x1^0'=x1^0, x^0'=x^0, T, cost: 1 Removed Trivial Updates Original rule: l11 -> l4 : r0^0'=r0^0, r^0'=1, x1^0'=x1^0, x^0'=x^0, T, cost: 1 New rule: l11 -> l4 : r^0'=1, T, cost: 1 Propagated Equalities Original rule: l14 -> l15 : r0^0'=r0^post21, r^0'=r^post21, x1^0'=x1^post21, x^0'=x^post21, (-1+x1^0 <= 0 /\ -x1^post21+x1^0 == 0 /\ -x^post21+x^0 == 0 /\ r0^0-r0^post21 == 0 /\ -r^post21+r^0 == 0), cost: 1 New rule: l14 -> l15 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (0 == 0 /\ -1+x1^0 <= 0), cost: 1 propagated equality x1^post21 = x1^0 propagated equality x^post21 = x^0 propagated equality r0^post21 = r0^0 propagated equality r^post21 = r^0 Simplified Guard Original rule: l14 -> l15 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (0 == 0 /\ -1+x1^0 <= 0), cost: 1 New rule: l14 -> l15 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, -1+x1^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l14 -> l15 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, -1+x1^0 <= 0, cost: 1 New rule: l14 -> l15 : -1+x1^0 <= 0, cost: 1 Propagated Equalities Original rule: l14 -> l15 : r0^0'=r0^post22, r^0'=r^post22, x1^0'=x1^post22, x^0'=x^post22, (3-x1^0 <= 0 /\ -r^post22+r^0 == 0 /\ r0^0-r0^post22 == 0 /\ -x1^post22+x1^0 == 0 /\ -x^post22+x^0 == 0), cost: 1 New rule: l14 -> l15 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (0 == 0 /\ 3-x1^0 <= 0), cost: 1 propagated equality r^post22 = r^0 propagated equality r0^post22 = r0^0 propagated equality x1^post22 = x1^0 propagated equality x^post22 = x^0 Simplified Guard Original rule: l14 -> l15 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (0 == 0 /\ 3-x1^0 <= 0), cost: 1 New rule: l14 -> l15 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, 3-x1^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l14 -> l15 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, 3-x1^0 <= 0, cost: 1 New rule: l14 -> l15 : 3-x1^0 <= 0, cost: 1 Propagated Equalities Original rule: l15 -> l5 : r0^0'=r0^post23, r^0'=r^post23, x1^0'=x1^post23, x^0'=x^post23, (x1^0-x1^post23 == 0 /\ -r0^post23+r0^0 == 0 /\ r^post23 == 0 /\ -x^post23+x^0 == 0), cost: 1 New rule: l15 -> l5 : r0^0'=r0^0, r^0'=0, x1^0'=x1^0, x^0'=x^0, 0 == 0, cost: 1 propagated equality x1^post23 = x1^0 propagated equality r0^post23 = r0^0 propagated equality r^post23 = 0 propagated equality x^post23 = x^0 Simplified Guard Original rule: l15 -> l5 : r0^0'=r0^0, r^0'=0, x1^0'=x1^0, x^0'=x^0, 0 == 0, cost: 1 New rule: l15 -> l5 : r0^0'=r0^0, r^0'=0, x1^0'=x1^0, x^0'=x^0, T, cost: 1 Removed Trivial Updates Original rule: l15 -> l5 : r0^0'=r0^0, r^0'=0, x1^0'=x1^0, x^0'=x^0, T, cost: 1 New rule: l15 -> l5 : r^0'=0, T, cost: 1 Propagated Equalities Original rule: l14 -> l5 : r0^0'=r0^post24, r^0'=r^post24, x1^0'=x1^post24, x^0'=x^post24, (-r0^post24+r0^0 == 0 /\ -1+r^post24 == 0 /\ x1^0-x1^post24 == 0 /\ -x^post24+x^0 == 0), cost: 1 New rule: l14 -> l5 : r0^0'=r0^0, r^0'=1, x1^0'=x1^0, x^0'=x^0, 0 == 0, cost: 1 propagated equality r0^post24 = r0^0 propagated equality r^post24 = 1 propagated equality x1^post24 = x1^0 propagated equality x^post24 = x^0 Simplified Guard Original rule: l14 -> l5 : r0^0'=r0^0, r^0'=1, x1^0'=x1^0, x^0'=x^0, 0 == 0, cost: 1 New rule: l14 -> l5 : r0^0'=r0^0, r^0'=1, x1^0'=x1^0, x^0'=x^0, T, cost: 1 Removed Trivial Updates Original rule: l14 -> l5 : r0^0'=r0^0, r^0'=1, x1^0'=x1^0, x^0'=x^0, T, cost: 1 New rule: l14 -> l5 : r^0'=1, T, cost: 1 Propagated Equalities Original rule: l17 -> l18 : r0^0'=r0^post27, r^0'=r^post27, x1^0'=x1^post27, x^0'=x^post27, (-1+x1^0 <= 0 /\ -r^post27+r^0 == 0 /\ -x^post27+x^0 == 0 /\ -r0^post27+r0^0 == 0 /\ x1^0-x1^post27 == 0), cost: 1 New rule: l17 -> l18 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (0 == 0 /\ -1+x1^0 <= 0), cost: 1 propagated equality r^post27 = r^0 propagated equality x^post27 = x^0 propagated equality r0^post27 = r0^0 propagated equality x1^post27 = x1^0 Simplified Guard Original rule: l17 -> l18 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (0 == 0 /\ -1+x1^0 <= 0), cost: 1 New rule: l17 -> l18 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, -1+x1^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l17 -> l18 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, -1+x1^0 <= 0, cost: 1 New rule: l17 -> l18 : -1+x1^0 <= 0, cost: 1 Propagated Equalities Original rule: l17 -> l18 : r0^0'=r0^post28, r^0'=r^post28, x1^0'=x1^post28, x^0'=x^post28, (-r^post28+r^0 == 0 /\ -x1^post28+x1^0 == 0 /\ 3-x1^0 <= 0 /\ -x^post28+x^0 == 0 /\ -r0^post28+r0^0 == 0), cost: 1 New rule: l17 -> l18 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (0 == 0 /\ 3-x1^0 <= 0), cost: 1 propagated equality r^post28 = r^0 propagated equality x1^post28 = x1^0 propagated equality x^post28 = x^0 propagated equality r0^post28 = r0^0 Simplified Guard Original rule: l17 -> l18 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (0 == 0 /\ 3-x1^0 <= 0), cost: 1 New rule: l17 -> l18 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, 3-x1^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l17 -> l18 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, 3-x1^0 <= 0, cost: 1 New rule: l17 -> l18 : 3-x1^0 <= 0, cost: 1 Propagated Equalities Original rule: l18 -> l2 : r0^0'=r0^post29, r^0'=r^post29, x1^0'=x1^post29, x^0'=x^post29, (-r0^post29+r0^0 == 0 /\ -x^post29+x^0 == 0 /\ -x1^post29+x1^0 == 0 /\ r^post29 == 0), cost: 1 New rule: l18 -> l2 : r0^0'=r0^0, r^0'=0, x1^0'=x1^0, x^0'=x^0, 0 == 0, cost: 1 propagated equality r0^post29 = r0^0 propagated equality x^post29 = x^0 propagated equality x1^post29 = x1^0 propagated equality r^post29 = 0 Simplified Guard Original rule: l18 -> l2 : r0^0'=r0^0, r^0'=0, x1^0'=x1^0, x^0'=x^0, 0 == 0, cost: 1 New rule: l18 -> l2 : r0^0'=r0^0, r^0'=0, x1^0'=x1^0, x^0'=x^0, T, cost: 1 Removed Trivial Updates Original rule: l18 -> l2 : r0^0'=r0^0, r^0'=0, x1^0'=x1^0, x^0'=x^0, T, cost: 1 New rule: l18 -> l2 : r^0'=0, T, cost: 1 Propagated Equalities Original rule: l17 -> l2 : r0^0'=r0^post30, r^0'=r^post30, x1^0'=x1^post30, x^0'=x^post30, (-x^post30+x^0 == 0 /\ -r0^post30+r0^0 == 0 /\ x1^0-x1^post30 == 0 /\ -1+r^post30 == 0), cost: 1 New rule: l17 -> l2 : r0^0'=r0^0, r^0'=1, x1^0'=x1^0, x^0'=x^0, 0 == 0, cost: 1 propagated equality x^post30 = x^0 propagated equality r0^post30 = r0^0 propagated equality x1^post30 = x1^0 propagated equality r^post30 = 1 Simplified Guard Original rule: l17 -> l2 : r0^0'=r0^0, r^0'=1, x1^0'=x1^0, x^0'=x^0, 0 == 0, cost: 1 New rule: l17 -> l2 : r0^0'=r0^0, r^0'=1, x1^0'=x1^0, x^0'=x^0, T, cost: 1 Removed Trivial Updates Original rule: l17 -> l2 : r0^0'=r0^0, r^0'=1, x1^0'=x1^0, x^0'=x^0, T, cost: 1 New rule: l17 -> l2 : r^0'=1, T, cost: 1 Propagated Equalities Original rule: l17 -> l7 : r0^0'=r0^post31, r^0'=r^post31, x1^0'=x1^post31, x^0'=x^post31, (-x1^post31+x1^0 == 0 /\ -r^post31+r^0 == 0 /\ -2+x^post31 == 0 /\ -r0^post31+r0^0 == 0), cost: 1 New rule: l17 -> l7 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=2, 0 == 0, cost: 1 propagated equality x1^post31 = x1^0 propagated equality r^post31 = r^0 propagated equality x^post31 = 2 propagated equality r0^post31 = r0^0 Simplified Guard Original rule: l17 -> l7 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=2, 0 == 0, cost: 1 New rule: l17 -> l7 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=2, T, cost: 1 Removed Trivial Updates Original rule: l17 -> l7 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=2, T, cost: 1 New rule: l17 -> l7 : x^0'=2, T, cost: 1 Propagated Equalities Original rule: l19 -> l20 : r0^0'=r0^post32, r^0'=r^post32, x1^0'=x1^post32, x^0'=x^post32, (-1+x1^0 <= 0 /\ -r^post32+r^0 == 0 /\ -x1^post32+x1^0 == 0 /\ -x^post32+x^0 == 0 /\ -r0^post32+r0^0 == 0), cost: 1 New rule: l19 -> l20 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (0 == 0 /\ -1+x1^0 <= 0), cost: 1 propagated equality r^post32 = r^0 propagated equality x1^post32 = x1^0 propagated equality x^post32 = x^0 propagated equality r0^post32 = r0^0 Simplified Guard Original rule: l19 -> l20 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (0 == 0 /\ -1+x1^0 <= 0), cost: 1 New rule: l19 -> l20 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, -1+x1^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l19 -> l20 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, -1+x1^0 <= 0, cost: 1 New rule: l19 -> l20 : -1+x1^0 <= 0, cost: 1 Propagated Equalities Original rule: l19 -> l20 : r0^0'=r0^post33, r^0'=r^post33, x1^0'=x1^post33, x^0'=x^post33, (-r^post33+r^0 == 0 /\ r0^0-r0^post33 == 0 /\ -x1^post33+x1^0 == 0 /\ 3-x1^0 <= 0 /\ -x^post33+x^0 == 0), cost: 1 New rule: l19 -> l20 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (0 == 0 /\ 3-x1^0 <= 0), cost: 1 propagated equality r^post33 = r^0 propagated equality r0^post33 = r0^0 propagated equality x1^post33 = x1^0 propagated equality x^post33 = x^0 Simplified Guard Original rule: l19 -> l20 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (0 == 0 /\ 3-x1^0 <= 0), cost: 1 New rule: l19 -> l20 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, 3-x1^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l19 -> l20 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, 3-x1^0 <= 0, cost: 1 New rule: l19 -> l20 : 3-x1^0 <= 0, cost: 1 Propagated Equalities Original rule: l20 -> l4 : r0^0'=r0^post34, r^0'=r^post34, x1^0'=x1^post34, x^0'=x^post34, (-x^post34+x^0 == 0 /\ -r0^post34+r0^0 == 0 /\ r^post34 == 0 /\ x1^0-x1^post34 == 0), cost: 1 New rule: l20 -> l4 : r0^0'=r0^0, r^0'=0, x1^0'=x1^0, x^0'=x^0, 0 == 0, cost: 1 propagated equality x^post34 = x^0 propagated equality r0^post34 = r0^0 propagated equality r^post34 = 0 propagated equality x1^post34 = x1^0 Simplified Guard Original rule: l20 -> l4 : r0^0'=r0^0, r^0'=0, x1^0'=x1^0, x^0'=x^0, 0 == 0, cost: 1 New rule: l20 -> l4 : r0^0'=r0^0, r^0'=0, x1^0'=x1^0, x^0'=x^0, T, cost: 1 Removed Trivial Updates Original rule: l20 -> l4 : r0^0'=r0^0, r^0'=0, x1^0'=x1^0, x^0'=x^0, T, cost: 1 New rule: l20 -> l4 : r^0'=0, T, cost: 1 Propagated Equalities Original rule: l19 -> l4 : r0^0'=r0^post35, r^0'=r^post35, x1^0'=x1^post35, x^0'=x^post35, (-x1^post35+x1^0 == 0 /\ -x^post35+x^0 == 0 /\ -1+r^post35 == 0 /\ -r0^post35+r0^0 == 0), cost: 1 New rule: l19 -> l4 : r0^0'=r0^0, r^0'=1, x1^0'=x1^0, x^0'=x^0, 0 == 0, cost: 1 propagated equality x1^post35 = x1^0 propagated equality x^post35 = x^0 propagated equality r^post35 = 1 propagated equality r0^post35 = r0^0 Simplified Guard Original rule: l19 -> l4 : r0^0'=r0^0, r^0'=1, x1^0'=x1^0, x^0'=x^0, 0 == 0, cost: 1 New rule: l19 -> l4 : r0^0'=r0^0, r^0'=1, x1^0'=x1^0, x^0'=x^0, T, cost: 1 Removed Trivial Updates Original rule: l19 -> l4 : r0^0'=r0^0, r^0'=1, x1^0'=x1^0, x^0'=x^0, T, cost: 1 New rule: l19 -> l4 : r^0'=1, T, cost: 1 Propagated Equalities Original rule: l19 -> l11 : r0^0'=r0^post36, r^0'=r^post36, x1^0'=x1^post36, x^0'=x^post36, (-x1^post36+x1^0 == 0 /\ r0^0-r0^post36 == 0 /\ -2+x^post36 == 0 /\ -r^post36+r^0 == 0), cost: 1 New rule: l19 -> l11 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=2, 0 == 0, cost: 1 propagated equality x1^post36 = x1^0 propagated equality r0^post36 = r0^0 propagated equality x^post36 = 2 propagated equality r^post36 = r^0 Simplified Guard Original rule: l19 -> l11 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=2, 0 == 0, cost: 1 New rule: l19 -> l11 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=2, T, cost: 1 Removed Trivial Updates Original rule: l19 -> l11 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=2, T, cost: 1 New rule: l19 -> l11 : x^0'=2, T, cost: 1 Propagated Equalities Original rule: l21 -> l22 : r0^0'=r0^post37, r^0'=r^post37, x1^0'=x1^post37, x^0'=x^post37, (-1+x1^0 <= 0 /\ r0^0-r0^post37 == 0 /\ x1^0-x1^post37 == 0 /\ -x^post37+x^0 == 0 /\ -r^post37+r^0 == 0), cost: 1 New rule: l21 -> l22 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (0 == 0 /\ -1+x1^0 <= 0), cost: 1 propagated equality r0^post37 = r0^0 propagated equality x1^post37 = x1^0 propagated equality x^post37 = x^0 propagated equality r^post37 = r^0 Simplified Guard Original rule: l21 -> l22 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (0 == 0 /\ -1+x1^0 <= 0), cost: 1 New rule: l21 -> l22 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, -1+x1^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l21 -> l22 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, -1+x1^0 <= 0, cost: 1 New rule: l21 -> l22 : -1+x1^0 <= 0, cost: 1 Propagated Equalities Original rule: l21 -> l22 : r0^0'=r0^post38, r^0'=r^post38, x1^0'=x1^post38, x^0'=x^post38, (x1^0-x1^post38 == 0 /\ -r0^post38+r0^0 == 0 /\ -r^post38+r^0 == 0 /\ 3-x1^0 <= 0 /\ -x^post38+x^0 == 0), cost: 1 New rule: l21 -> l22 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (0 == 0 /\ 3-x1^0 <= 0), cost: 1 propagated equality x1^post38 = x1^0 propagated equality r0^post38 = r0^0 propagated equality r^post38 = r^0 propagated equality x^post38 = x^0 Simplified Guard Original rule: l21 -> l22 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (0 == 0 /\ 3-x1^0 <= 0), cost: 1 New rule: l21 -> l22 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, 3-x1^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l21 -> l22 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, 3-x1^0 <= 0, cost: 1 New rule: l21 -> l22 : 3-x1^0 <= 0, cost: 1 Propagated Equalities Original rule: l22 -> l5 : r0^0'=r0^post39, r^0'=r^post39, x1^0'=x1^post39, x^0'=x^post39, (-x^post39+x^0 == 0 /\ -r0^post39+r0^0 == 0 /\ r^post39 == 0 /\ x1^0-x1^post39 == 0), cost: 1 New rule: l22 -> l5 : r0^0'=r0^0, r^0'=0, x1^0'=x1^0, x^0'=x^0, 0 == 0, cost: 1 propagated equality x^post39 = x^0 propagated equality r0^post39 = r0^0 propagated equality r^post39 = 0 propagated equality x1^post39 = x1^0 Simplified Guard Original rule: l22 -> l5 : r0^0'=r0^0, r^0'=0, x1^0'=x1^0, x^0'=x^0, 0 == 0, cost: 1 New rule: l22 -> l5 : r0^0'=r0^0, r^0'=0, x1^0'=x1^0, x^0'=x^0, T, cost: 1 Removed Trivial Updates Original rule: l22 -> l5 : r0^0'=r0^0, r^0'=0, x1^0'=x1^0, x^0'=x^0, T, cost: 1 New rule: l22 -> l5 : r^0'=0, T, cost: 1 Propagated Equalities Original rule: l21 -> l5 : r0^0'=r0^post40, r^0'=r^post40, x1^0'=x1^post40, x^0'=x^post40, (-x^post40+x^0 == 0 /\ -r0^post40+r0^0 == 0 /\ -x1^post40+x1^0 == 0 /\ -1+r^post40 == 0), cost: 1 New rule: l21 -> l5 : r0^0'=r0^0, r^0'=1, x1^0'=x1^0, x^0'=x^0, 0 == 0, cost: 1 propagated equality x^post40 = x^0 propagated equality r0^post40 = r0^0 propagated equality x1^post40 = x1^0 propagated equality r^post40 = 1 Simplified Guard Original rule: l21 -> l5 : r0^0'=r0^0, r^0'=1, x1^0'=x1^0, x^0'=x^0, 0 == 0, cost: 1 New rule: l21 -> l5 : r0^0'=r0^0, r^0'=1, x1^0'=x1^0, x^0'=x^0, T, cost: 1 Removed Trivial Updates Original rule: l21 -> l5 : r0^0'=r0^0, r^0'=1, x1^0'=x1^0, x^0'=x^0, T, cost: 1 New rule: l21 -> l5 : r^0'=1, T, cost: 1 Propagated Equalities Original rule: l21 -> l14 : r0^0'=r0^post41, r^0'=r^post41, x1^0'=x1^post41, x^0'=x^post41, (r0^0-r0^post41 == 0 /\ -2+x^post41 == 0 /\ -r^post41+r^0 == 0 /\ -x1^post41+x1^0 == 0), cost: 1 New rule: l21 -> l14 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=2, 0 == 0, cost: 1 propagated equality r0^post41 = r0^0 propagated equality x^post41 = 2 propagated equality r^post41 = r^0 propagated equality x1^post41 = x1^0 Simplified Guard Original rule: l21 -> l14 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=2, 0 == 0, cost: 1 New rule: l21 -> l14 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=2, T, cost: 1 Removed Trivial Updates Original rule: l21 -> l14 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=2, T, cost: 1 New rule: l21 -> l14 : x^0'=2, T, cost: 1 Propagated Equalities Original rule: l23 -> l24 : r0^0'=r0^post42, r^0'=r^post42, x1^0'=x1^post42, x^0'=x^post42, (-1+x1^0 <= 0 /\ -r^post42+r^0 == 0 /\ -x^post42+x^0 == 0 /\ -r0^post42+r0^0 == 0 /\ x1^0-x1^post42 == 0), cost: 1 New rule: l23 -> l24 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (0 == 0 /\ -1+x1^0 <= 0), cost: 1 propagated equality r^post42 = r^0 propagated equality x^post42 = x^0 propagated equality r0^post42 = r0^0 propagated equality x1^post42 = x1^0 Simplified Guard Original rule: l23 -> l24 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (0 == 0 /\ -1+x1^0 <= 0), cost: 1 New rule: l23 -> l24 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, -1+x1^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l23 -> l24 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, -1+x1^0 <= 0, cost: 1 New rule: l23 -> l24 : -1+x1^0 <= 0, cost: 1 Propagated Equalities Original rule: l23 -> l24 : r0^0'=r0^post43, r^0'=r^post43, x1^0'=x1^post43, x^0'=x^post43, (-r0^post43+r0^0 == 0 /\ 3-x1^0 <= 0 /\ -r^post43+r^0 == 0 /\ x1^0-x1^post43 == 0 /\ -x^post43+x^0 == 0), cost: 1 New rule: l23 -> l24 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (0 == 0 /\ 3-x1^0 <= 0), cost: 1 propagated equality r0^post43 = r0^0 propagated equality r^post43 = r^0 propagated equality x1^post43 = x1^0 propagated equality x^post43 = x^0 Simplified Guard Original rule: l23 -> l24 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (0 == 0 /\ 3-x1^0 <= 0), cost: 1 New rule: l23 -> l24 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, 3-x1^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l23 -> l24 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, 3-x1^0 <= 0, cost: 1 New rule: l23 -> l24 : 3-x1^0 <= 0, cost: 1 Propagated Equalities Original rule: l24 -> l2 : r0^0'=r0^post44, r^0'=r^post44, x1^0'=x1^post44, x^0'=x^post44, (-r0^post44+r0^0 == 0 /\ -x1^post44+x1^0 == 0 /\ -x^post44+x^0 == 0 /\ r^post44 == 0), cost: 1 New rule: l24 -> l2 : r0^0'=r0^0, r^0'=0, x1^0'=x1^0, x^0'=x^0, 0 == 0, cost: 1 propagated equality r0^post44 = r0^0 propagated equality x1^post44 = x1^0 propagated equality x^post44 = x^0 propagated equality r^post44 = 0 Simplified Guard Original rule: l24 -> l2 : r0^0'=r0^0, r^0'=0, x1^0'=x1^0, x^0'=x^0, 0 == 0, cost: 1 New rule: l24 -> l2 : r0^0'=r0^0, r^0'=0, x1^0'=x1^0, x^0'=x^0, T, cost: 1 Removed Trivial Updates Original rule: l24 -> l2 : r0^0'=r0^0, r^0'=0, x1^0'=x1^0, x^0'=x^0, T, cost: 1 New rule: l24 -> l2 : r^0'=0, T, cost: 1 Propagated Equalities Original rule: l23 -> l2 : r0^0'=r0^post45, r^0'=r^post45, x1^0'=x1^post45, x^0'=x^post45, (-1+r^post45 == 0 /\ r0^0-r0^post45 == 0 /\ -x^post45+x^0 == 0 /\ -x1^post45+x1^0 == 0), cost: 1 New rule: l23 -> l2 : r0^0'=r0^0, r^0'=1, x1^0'=x1^0, x^0'=x^0, 0 == 0, cost: 1 propagated equality r^post45 = 1 propagated equality r0^post45 = r0^0 propagated equality x^post45 = x^0 propagated equality x1^post45 = x1^0 Simplified Guard Original rule: l23 -> l2 : r0^0'=r0^0, r^0'=1, x1^0'=x1^0, x^0'=x^0, 0 == 0, cost: 1 New rule: l23 -> l2 : r0^0'=r0^0, r^0'=1, x1^0'=x1^0, x^0'=x^0, T, cost: 1 Removed Trivial Updates Original rule: l23 -> l2 : r0^0'=r0^0, r^0'=1, x1^0'=x1^0, x^0'=x^0, T, cost: 1 New rule: l23 -> l2 : r^0'=1, T, cost: 1 Propagated Equalities Original rule: l23 -> l17 : r0^0'=r0^post46, r^0'=r^post46, x1^0'=x1^post46, x^0'=x^post46, (-r^post46+r^0 == 0 /\ -x1^post46+x1^0 == 0 /\ -1+x^post46 == 0 /\ -r0^post46+r0^0 == 0), cost: 1 New rule: l23 -> l17 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=1, 0 == 0, cost: 1 propagated equality r^post46 = r^0 propagated equality x1^post46 = x1^0 propagated equality x^post46 = 1 propagated equality r0^post46 = r0^0 Simplified Guard Original rule: l23 -> l17 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=1, 0 == 0, cost: 1 New rule: l23 -> l17 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=1, T, cost: 1 Removed Trivial Updates Original rule: l23 -> l17 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=1, T, cost: 1 New rule: l23 -> l17 : x^0'=1, T, cost: 1 Propagated Equalities Original rule: l25 -> l26 : r0^0'=r0^post47, r^0'=r^post47, x1^0'=x1^post47, x^0'=x^post47, (-1+x1^0 <= 0 /\ -r^post47+r^0 == 0 /\ -x1^post47+x1^0 == 0 /\ -x^post47+x^0 == 0 /\ -r0^post47+r0^0 == 0), cost: 1 New rule: l25 -> l26 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (0 == 0 /\ -1+x1^0 <= 0), cost: 1 propagated equality r^post47 = r^0 propagated equality x1^post47 = x1^0 propagated equality x^post47 = x^0 propagated equality r0^post47 = r0^0 Simplified Guard Original rule: l25 -> l26 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (0 == 0 /\ -1+x1^0 <= 0), cost: 1 New rule: l25 -> l26 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, -1+x1^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l25 -> l26 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, -1+x1^0 <= 0, cost: 1 New rule: l25 -> l26 : -1+x1^0 <= 0, cost: 1 Propagated Equalities Original rule: l25 -> l26 : r0^0'=r0^post48, r^0'=r^post48, x1^0'=x1^post48, x^0'=x^post48, (r0^0-r0^post48 == 0 /\ -r^post48+r^0 == 0 /\ -x1^post48+x1^0 == 0 /\ 3-x1^0 <= 0 /\ -x^post48+x^0 == 0), cost: 1 New rule: l25 -> l26 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (0 == 0 /\ 3-x1^0 <= 0), cost: 1 propagated equality r0^post48 = r0^0 propagated equality r^post48 = r^0 propagated equality x1^post48 = x1^0 propagated equality x^post48 = x^0 Simplified Guard Original rule: l25 -> l26 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (0 == 0 /\ 3-x1^0 <= 0), cost: 1 New rule: l25 -> l26 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, 3-x1^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l25 -> l26 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, 3-x1^0 <= 0, cost: 1 New rule: l25 -> l26 : 3-x1^0 <= 0, cost: 1 Propagated Equalities Original rule: l26 -> l4 : r0^0'=r0^post49, r^0'=r^post49, x1^0'=x1^post49, x^0'=x^post49, (x1^0-x1^post49 == 0 /\ -r0^post49+r0^0 == 0 /\ r^post49 == 0 /\ -x^post49+x^0 == 0), cost: 1 New rule: l26 -> l4 : r0^0'=r0^0, r^0'=0, x1^0'=x1^0, x^0'=x^0, 0 == 0, cost: 1 propagated equality x1^post49 = x1^0 propagated equality r0^post49 = r0^0 propagated equality r^post49 = 0 propagated equality x^post49 = x^0 Simplified Guard Original rule: l26 -> l4 : r0^0'=r0^0, r^0'=0, x1^0'=x1^0, x^0'=x^0, 0 == 0, cost: 1 New rule: l26 -> l4 : r0^0'=r0^0, r^0'=0, x1^0'=x1^0, x^0'=x^0, T, cost: 1 Removed Trivial Updates Original rule: l26 -> l4 : r0^0'=r0^0, r^0'=0, x1^0'=x1^0, x^0'=x^0, T, cost: 1 New rule: l26 -> l4 : r^0'=0, T, cost: 1 Propagated Equalities Original rule: l25 -> l4 : r0^0'=r0^post50, r^0'=r^post50, x1^0'=x1^post50, x^0'=x^post50, (-x^post50+x^0 == 0 /\ -x1^post50+x1^0 == 0 /\ -1+r^post50 == 0 /\ -r0^post50+r0^0 == 0), cost: 1 New rule: l25 -> l4 : r0^0'=r0^0, r^0'=1, x1^0'=x1^0, x^0'=x^0, 0 == 0, cost: 1 propagated equality x^post50 = x^0 propagated equality x1^post50 = x1^0 propagated equality r^post50 = 1 propagated equality r0^post50 = r0^0 Simplified Guard Original rule: l25 -> l4 : r0^0'=r0^0, r^0'=1, x1^0'=x1^0, x^0'=x^0, 0 == 0, cost: 1 New rule: l25 -> l4 : r0^0'=r0^0, r^0'=1, x1^0'=x1^0, x^0'=x^0, T, cost: 1 Removed Trivial Updates Original rule: l25 -> l4 : r0^0'=r0^0, r^0'=1, x1^0'=x1^0, x^0'=x^0, T, cost: 1 New rule: l25 -> l4 : r^0'=1, T, cost: 1 Propagated Equalities Original rule: l25 -> l19 : r0^0'=r0^post51, r^0'=r^post51, x1^0'=x1^post51, x^0'=x^post51, (-1+x^post51 == 0 /\ -x1^post51+x1^0 == 0 /\ r0^0-r0^post51 == 0 /\ -r^post51+r^0 == 0), cost: 1 New rule: l25 -> l19 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=1, 0 == 0, cost: 1 propagated equality x^post51 = 1 propagated equality x1^post51 = x1^0 propagated equality r0^post51 = r0^0 propagated equality r^post51 = r^0 Simplified Guard Original rule: l25 -> l19 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=1, 0 == 0, cost: 1 New rule: l25 -> l19 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=1, T, cost: 1 Removed Trivial Updates Original rule: l25 -> l19 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=1, T, cost: 1 New rule: l25 -> l19 : x^0'=1, T, cost: 1 Propagated Equalities Original rule: l27 -> l28 : r0^0'=r0^post52, r^0'=r^post52, x1^0'=x1^post52, x^0'=x^post52, (-1+x1^0 <= 0 /\ r0^0-r0^post52 == 0 /\ x1^0-x1^post52 == 0 /\ -x^post52+x^0 == 0 /\ -r^post52+r^0 == 0), cost: 1 New rule: l27 -> l28 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (0 == 0 /\ -1+x1^0 <= 0), cost: 1 propagated equality r0^post52 = r0^0 propagated equality x1^post52 = x1^0 propagated equality x^post52 = x^0 propagated equality r^post52 = r^0 Simplified Guard Original rule: l27 -> l28 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (0 == 0 /\ -1+x1^0 <= 0), cost: 1 New rule: l27 -> l28 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, -1+x1^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l27 -> l28 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, -1+x1^0 <= 0, cost: 1 New rule: l27 -> l28 : -1+x1^0 <= 0, cost: 1 Propagated Equalities Original rule: l27 -> l28 : r0^0'=r0^post53, r^0'=r^post53, x1^0'=x1^post53, x^0'=x^post53, (-r^post53+r^0 == 0 /\ 3-x1^0 <= 0 /\ -x^post53+x^0 == 0 /\ -r0^post53+r0^0 == 0 /\ x1^0-x1^post53 == 0), cost: 1 New rule: l27 -> l28 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (0 == 0 /\ 3-x1^0 <= 0), cost: 1 propagated equality r^post53 = r^0 propagated equality x^post53 = x^0 propagated equality r0^post53 = r0^0 propagated equality x1^post53 = x1^0 Simplified Guard Original rule: l27 -> l28 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, (0 == 0 /\ 3-x1^0 <= 0), cost: 1 New rule: l27 -> l28 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, 3-x1^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l27 -> l28 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, 3-x1^0 <= 0, cost: 1 New rule: l27 -> l28 : 3-x1^0 <= 0, cost: 1 Propagated Equalities Original rule: l28 -> l5 : r0^0'=r0^post54, r^0'=r^post54, x1^0'=x1^post54, x^0'=x^post54, (-x^post54+x^0 == 0 /\ -r0^post54+r0^0 == 0 /\ r^post54 == 0 /\ x1^0-x1^post54 == 0), cost: 1 New rule: l28 -> l5 : r0^0'=r0^0, r^0'=0, x1^0'=x1^0, x^0'=x^0, 0 == 0, cost: 1 propagated equality x^post54 = x^0 propagated equality r0^post54 = r0^0 propagated equality r^post54 = 0 propagated equality x1^post54 = x1^0 Simplified Guard Original rule: l28 -> l5 : r0^0'=r0^0, r^0'=0, x1^0'=x1^0, x^0'=x^0, 0 == 0, cost: 1 New rule: l28 -> l5 : r0^0'=r0^0, r^0'=0, x1^0'=x1^0, x^0'=x^0, T, cost: 1 Removed Trivial Updates Original rule: l28 -> l5 : r0^0'=r0^0, r^0'=0, x1^0'=x1^0, x^0'=x^0, T, cost: 1 New rule: l28 -> l5 : r^0'=0, T, cost: 1 Propagated Equalities Original rule: l27 -> l5 : r0^0'=r0^post55, r^0'=r^post55, x1^0'=x1^post55, x^0'=x^post55, (-x^post55+x^0 == 0 /\ -r0^post55+r0^0 == 0 /\ -x1^post55+x1^0 == 0 /\ -1+r^post55 == 0), cost: 1 New rule: l27 -> l5 : r0^0'=r0^0, r^0'=1, x1^0'=x1^0, x^0'=x^0, 0 == 0, cost: 1 propagated equality x^post55 = x^0 propagated equality r0^post55 = r0^0 propagated equality x1^post55 = x1^0 propagated equality r^post55 = 1 Simplified Guard Original rule: l27 -> l5 : r0^0'=r0^0, r^0'=1, x1^0'=x1^0, x^0'=x^0, 0 == 0, cost: 1 New rule: l27 -> l5 : r0^0'=r0^0, r^0'=1, x1^0'=x1^0, x^0'=x^0, T, cost: 1 Removed Trivial Updates Original rule: l27 -> l5 : r0^0'=r0^0, r^0'=1, x1^0'=x1^0, x^0'=x^0, T, cost: 1 New rule: l27 -> l5 : r^0'=1, T, cost: 1 Propagated Equalities Original rule: l27 -> l21 : r0^0'=r0^post56, r^0'=r^post56, x1^0'=x1^post56, x^0'=x^post56, (r0^0-r0^post56 == 0 /\ -1+x^post56 == 0 /\ -r^post56+r^0 == 0 /\ -x1^post56+x1^0 == 0), cost: 1 New rule: l27 -> l21 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=1, 0 == 0, cost: 1 propagated equality r0^post56 = r0^0 propagated equality x^post56 = 1 propagated equality r^post56 = r^0 propagated equality x1^post56 = x1^0 Simplified Guard Original rule: l27 -> l21 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=1, 0 == 0, cost: 1 New rule: l27 -> l21 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=1, T, cost: 1 Removed Trivial Updates Original rule: l27 -> l21 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=1, T, cost: 1 New rule: l27 -> l21 : x^0'=1, T, cost: 1 Propagated Equalities Original rule: l29 -> l19 : r0^0'=r0^post57, r^0'=r^post57, x1^0'=x1^post57, x^0'=x^post57, (x^0-x^post57 == 0 /\ x1^post57-x^0 == 0 /\ -r0^post57+r0^0 == 0 /\ -r^post57+r^0 == 0), cost: 1 New rule: l29 -> l19 : r0^0'=r0^0, r^0'=r^0, x1^0'=x^0, x^0'=x^0, 0 == 0, cost: 1 propagated equality x^post57 = x^0 propagated equality x1^post57 = x^0 propagated equality r0^post57 = r0^0 propagated equality r^post57 = r^0 Simplified Guard Original rule: l29 -> l19 : r0^0'=r0^0, r^0'=r^0, x1^0'=x^0, x^0'=x^0, 0 == 0, cost: 1 New rule: l29 -> l19 : r0^0'=r0^0, r^0'=r^0, x1^0'=x^0, x^0'=x^0, T, cost: 1 Removed Trivial Updates Original rule: l29 -> l19 : r0^0'=r0^0, r^0'=r^0, x1^0'=x^0, x^0'=x^0, T, cost: 1 New rule: l29 -> l19 : x1^0'=x^0, T, cost: 1 Propagated Equalities Original rule: l29 -> l6 : r0^0'=r0^post58, r^0'=r^post58, x1^0'=x1^post58, x^0'=x^post58, (-r0^post58+r0^0 == 0 /\ -2+x^post58 == 0 /\ -r^post58+r^0 == 0 /\ x1^0-x1^post58 == 0), cost: 1 New rule: l29 -> l6 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=2, 0 == 0, cost: 1 propagated equality r0^post58 = r0^0 propagated equality x^post58 = 2 propagated equality r^post58 = r^0 propagated equality x1^post58 = x1^0 Simplified Guard Original rule: l29 -> l6 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=2, 0 == 0, cost: 1 New rule: l29 -> l6 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=2, T, cost: 1 Removed Trivial Updates Original rule: l29 -> l6 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=2, T, cost: 1 New rule: l29 -> l6 : x^0'=2, T, cost: 1 Propagated Equalities Original rule: l29 -> l3 : r0^0'=r0^post59, r^0'=r^post59, x1^0'=x1^post59, x^0'=x^post59, (-r0^post59+r0^0 == 0 /\ -r^post59+r^0 == 0 /\ -x^post59+x^0 == 0 /\ -x1^post59+x1^0 == 0), cost: 1 New rule: l29 -> l3 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, 0 == 0, cost: 1 propagated equality r0^post59 = r0^0 propagated equality r^post59 = r^0 propagated equality x^post59 = x^0 propagated equality x1^post59 = x1^0 Simplified Guard Original rule: l29 -> l3 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, 0 == 0, cost: 1 New rule: l29 -> l3 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, T, cost: 1 Removed Trivial Updates Original rule: l29 -> l3 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, T, cost: 1 New rule: l29 -> l3 : T, cost: 1 Propagated Equalities Original rule: l30 -> l27 : r0^0'=r0^post60, r^0'=r^post60, x1^0'=x1^post60, x^0'=x^post60, (-r^post60+r^0 == 0 /\ r0^0-r0^post60 == 0 /\ x1^post60-x^0 == 0 /\ -x^post60+x^0 == 0), cost: 1 New rule: l30 -> l27 : r0^0'=r0^0, r^0'=r^0, x1^0'=x^0, x^0'=x^0, 0 == 0, cost: 1 propagated equality r^post60 = r^0 propagated equality r0^post60 = r0^0 propagated equality x1^post60 = x^0 propagated equality x^post60 = x^0 Simplified Guard Original rule: l30 -> l27 : r0^0'=r0^0, r^0'=r^0, x1^0'=x^0, x^0'=x^0, 0 == 0, cost: 1 New rule: l30 -> l27 : r0^0'=r0^0, r^0'=r^0, x1^0'=x^0, x^0'=x^0, T, cost: 1 Removed Trivial Updates Original rule: l30 -> l27 : r0^0'=r0^0, r^0'=r^0, x1^0'=x^0, x^0'=x^0, T, cost: 1 New rule: l30 -> l27 : x1^0'=x^0, T, cost: 1 Propagated Equalities Original rule: l30 -> l29 : r0^0'=r0^post61, r^0'=r^post61, x1^0'=x1^post61, x^0'=x^post61, (x1^0-x1^post61 == 0 /\ -r0^post61+r0^0 == 0 /\ -r^post61+r^0 == 0 /\ -1+x^post61 == 0), cost: 1 New rule: l30 -> l29 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=1, 0 == 0, cost: 1 propagated equality x1^post61 = x1^0 propagated equality r0^post61 = r0^0 propagated equality r^post61 = r^0 propagated equality x^post61 = 1 Simplified Guard Original rule: l30 -> l29 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=1, 0 == 0, cost: 1 New rule: l30 -> l29 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=1, T, cost: 1 Removed Trivial Updates Original rule: l30 -> l29 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=1, T, cost: 1 New rule: l30 -> l29 : x^0'=1, T, cost: 1 Propagated Equalities Original rule: l30 -> l3 : r0^0'=r0^post62, r^0'=r^post62, x1^0'=x1^post62, x^0'=x^post62, (-r^post62+r^0 == 0 /\ r0^0-r0^post62 == 0 /\ -x1^post62+x1^0 == 0 /\ -x^post62+x^0 == 0), cost: 1 New rule: l30 -> l3 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, 0 == 0, cost: 1 propagated equality r^post62 = r^0 propagated equality r0^post62 = r0^0 propagated equality x1^post62 = x1^0 propagated equality x^post62 = x^0 Simplified Guard Original rule: l30 -> l3 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, 0 == 0, cost: 1 New rule: l30 -> l3 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, T, cost: 1 Removed Trivial Updates Original rule: l30 -> l3 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, T, cost: 1 New rule: l30 -> l3 : T, cost: 1 Propagated Equalities Original rule: l31 -> l30 : r0^0'=r0^post63, r^0'=r^post63, x1^0'=x1^post63, x^0'=x^post63, (x1^0-x1^post63 == 0 /\ -r0^post63+r0^0 == 0 /\ -r^post63+r^0 == 0 /\ -x^post63+x^0 == 0), cost: 1 New rule: l31 -> l30 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, 0 == 0, cost: 1 propagated equality x1^post63 = x1^0 propagated equality r0^post63 = r0^0 propagated equality r^post63 = r^0 propagated equality x^post63 = x^0 Simplified Guard Original rule: l31 -> l30 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, 0 == 0, cost: 1 New rule: l31 -> l30 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, T, cost: 1 Removed Trivial Updates Original rule: l31 -> l30 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, T, cost: 1 New rule: l31 -> l30 : T, cost: 1 Propagated Equalities Original rule: l14 -> l14 : r0^0'=r0^post26, r^0'=r^post26, x1^0'=x1^post26, x^0'=x^post26, (-x^post25+x^0 == 0 /\ -r0^post25+r0^0 == 0 /\ x^post25-x^post26 == 0 /\ -r^post26+r^post25 == 0 /\ -x1^post25+x1^0 == 0 /\ -r^post25+r^0 == 0 /\ x1^post25-x1^post26 == 0 /\ r0^post25-r0^post26 == 0), cost: 1 New rule: l14 -> l14 : r0^0'=r0^post25, r^0'=r^post25, x1^0'=x1^post25, x^0'=x^post25, (0 == 0 /\ -x^post25+x^0 == 0 /\ -r0^post25+r0^0 == 0 /\ -x1^post25+x1^0 == 0 /\ -r^post25+r^0 == 0), cost: 1 propagated equality x^post26 = x^post25 propagated equality r^post26 = r^post25 propagated equality x1^post26 = x1^post25 propagated equality r0^post26 = r0^post25 Propagated Equalities Original rule: l14 -> l14 : r0^0'=r0^post25, r^0'=r^post25, x1^0'=x1^post25, x^0'=x^post25, (0 == 0 /\ -x^post25+x^0 == 0 /\ -r0^post25+r0^0 == 0 /\ -x1^post25+x1^0 == 0 /\ -r^post25+r^0 == 0), cost: 1 New rule: l14 -> l14 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, 0 == 0, cost: 1 propagated equality x^post25 = x^0 propagated equality r0^post25 = r0^0 propagated equality x1^post25 = x1^0 propagated equality r^post25 = r^0 Simplified Guard Original rule: l14 -> l14 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, 0 == 0, cost: 1 New rule: l14 -> l14 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, T, cost: 1 Removed Trivial Updates Original rule: l14 -> l14 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, T, cost: 1 New rule: l14 -> l14 : T, cost: 1 Propagated Equalities Original rule: l6 -> l6 : r0^0'=r0^post7, r^0'=r^post7, x1^0'=x1^post7, x^0'=x^post7, (-r^post6+r^0 == 0 /\ -x1^post6+x1^0 == 0 /\ r0^post6-r0^post7 == 0 /\ -r^post7+r^post6 == 0 /\ x1^post6-x1^post7 == 0 /\ -x^post6+x^0 == 0 /\ x^post6-x^post7 == 0 /\ -r0^post6+r0^0 == 0), cost: 1 New rule: l6 -> l6 : r0^0'=r0^post6, r^0'=r^post6, x1^0'=x1^post6, x^0'=x^post6, (0 == 0 /\ -r^post6+r^0 == 0 /\ -x1^post6+x1^0 == 0 /\ -x^post6+x^0 == 0 /\ -r0^post6+r0^0 == 0), cost: 1 propagated equality r0^post7 = r0^post6 propagated equality r^post7 = r^post6 propagated equality x1^post7 = x1^post6 propagated equality x^post7 = x^post6 Propagated Equalities Original rule: l6 -> l6 : r0^0'=r0^post6, r^0'=r^post6, x1^0'=x1^post6, x^0'=x^post6, (0 == 0 /\ -r^post6+r^0 == 0 /\ -x1^post6+x1^0 == 0 /\ -x^post6+x^0 == 0 /\ -r0^post6+r0^0 == 0), cost: 1 New rule: l6 -> l6 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, 0 == 0, cost: 1 propagated equality r^post6 = r^0 propagated equality x1^post6 = x1^0 propagated equality x^post6 = x^0 propagated equality r0^post6 = r0^0 Simplified Guard Original rule: l6 -> l6 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, 0 == 0, cost: 1 New rule: l6 -> l6 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, T, cost: 1 Removed Trivial Updates Original rule: l6 -> l6 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, T, cost: 1 New rule: l6 -> l6 : T, cost: 1 Propagated Equalities Original rule: l7 -> l7 : r0^0'=r0^post14, r^0'=r^post14, x1^0'=x1^post14, x^0'=x^post14, (-r^post13+r^0 == 0 /\ r0^post13-r0^post14 == 0 /\ -x1^post13+x1^0 == 0 /\ x1^post13-x1^post14 == 0 /\ -r^post14+r^post13 == 0 /\ -x^post13+x^0 == 0 /\ x^post13-x^post14 == 0 /\ -r0^post13+r0^0 == 0), cost: 1 New rule: l7 -> l7 : r0^0'=r0^post13, r^0'=r^post13, x1^0'=x1^post13, x^0'=x^post13, (0 == 0 /\ -r^post13+r^0 == 0 /\ -x1^post13+x1^0 == 0 /\ -x^post13+x^0 == 0 /\ -r0^post13+r0^0 == 0), cost: 1 propagated equality r0^post14 = r0^post13 propagated equality x1^post14 = x1^post13 propagated equality r^post14 = r^post13 propagated equality x^post14 = x^post13 Propagated Equalities Original rule: l7 -> l7 : r0^0'=r0^post13, r^0'=r^post13, x1^0'=x1^post13, x^0'=x^post13, (0 == 0 /\ -r^post13+r^0 == 0 /\ -x1^post13+x1^0 == 0 /\ -x^post13+x^0 == 0 /\ -r0^post13+r0^0 == 0), cost: 1 New rule: l7 -> l7 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, 0 == 0, cost: 1 propagated equality r^post13 = r^0 propagated equality x1^post13 = x1^0 propagated equality x^post13 = x^0 propagated equality r0^post13 = r0^0 Simplified Guard Original rule: l7 -> l7 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, 0 == 0, cost: 1 New rule: l7 -> l7 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, T, cost: 1 Removed Trivial Updates Original rule: l7 -> l7 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, T, cost: 1 New rule: l7 -> l7 : T, cost: 1 Propagated Equalities Original rule: l11 -> l11 : r0^0'=r0^post20, r^0'=r^post20, x1^0'=x1^post20, x^0'=x^post20, (x^post19-x^post20 == 0 /\ -x^post19+x^0 == 0 /\ -r0^post19+r0^0 == 0 /\ r0^post19-r0^post20 == 0 /\ -x1^post20+x1^post19 == 0 /\ -r^post19+r^0 == 0 /\ r^post19-r^post20 == 0 /\ x1^0-x1^post19 == 0), cost: 1 New rule: l11 -> l11 : r0^0'=r0^post19, r^0'=r^post19, x1^0'=x1^post19, x^0'=x^post19, (0 == 0 /\ -x^post19+x^0 == 0 /\ -r0^post19+r0^0 == 0 /\ -r^post19+r^0 == 0 /\ x1^0-x1^post19 == 0), cost: 1 propagated equality x^post20 = x^post19 propagated equality r0^post20 = r0^post19 propagated equality x1^post20 = x1^post19 propagated equality r^post20 = r^post19 Propagated Equalities Original rule: l11 -> l11 : r0^0'=r0^post19, r^0'=r^post19, x1^0'=x1^post19, x^0'=x^post19, (0 == 0 /\ -x^post19+x^0 == 0 /\ -r0^post19+r0^0 == 0 /\ -r^post19+r^0 == 0 /\ x1^0-x1^post19 == 0), cost: 1 New rule: l11 -> l11 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, 0 == 0, cost: 1 propagated equality x^post19 = x^0 propagated equality r0^post19 = r0^0 propagated equality r^post19 = r^0 propagated equality x1^post19 = x1^0 Simplified Guard Original rule: l11 -> l11 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, 0 == 0, cost: 1 New rule: l11 -> l11 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, T, cost: 1 Removed Trivial Updates Original rule: l11 -> l11 : r0^0'=r0^0, r^0'=r^0, x1^0'=x1^0, x^0'=x^0, T, cost: 1 New rule: l11 -> l11 : T, cost: 1 Step with 121 Trace 121[T] Blocked [{}, {}] Step with 118 Trace 121[T], 118[T] Blocked [{}, {}, {}] Step with 110 Trace 121[T], 118[T], 110[(-1+x1^0 <= 0)] Blocked [{}, {}, {}, {}] Step with 112 Trace 121[T], 118[T], 110[(-1+x1^0 <= 0)], 112[T] Blocked [{}, {}, {}, {}, {}] Backtrack Trace 121[T], 118[T], 110[(-1+x1^0 <= 0)] Blocked [{}, {}, {}, {112[T]}] Backtrack Trace 121[T], 118[T] Blocked [{}, {}, {110[T]}] Step with 111 Trace 121[T], 118[T], 111[(3-x1^0 <= 0)] Blocked [{}, {}, {110[T]}, {}] Step with 112 Trace 121[T], 118[T], 111[(3-x1^0 <= 0)], 112[T] Blocked [{}, {}, {110[T]}, {}, {}] Backtrack Trace 121[T], 118[T], 111[(3-x1^0 <= 0)] Blocked [{}, {}, {110[T]}, {112[T]}] Backtrack Trace 121[T], 118[T] Blocked [{}, {}, {110[T], 111[T]}] Step with 113 Trace 121[T], 118[T], 113[T] Blocked [{}, {}, {110[T], 111[T]}, {}] Step with 70 Trace 121[T], 118[T], 113[T], 70[(1-r^0 <= 0 /\ 1-r^0 == 0 /\ -1+r^0 <= 0)] Blocked [{}, {}, {110[T], 111[T]}, {}, {}] Backtrack Trace 121[T], 118[T], 113[T] Blocked [{}, {}, {110[T], 111[T]}, {70[T]}] Backtrack Trace 121[T], 118[T] Blocked [{}, {}, {110[T], 111[T], 113[T]}] Step with 114 Trace 121[T], 118[T], 114[T] Blocked [{}, {}, {110[T], 111[T], 113[T]}, {}] Step with 95 Trace 121[T], 118[T], 114[T], 95[(-1+x1^0 <= 0)] Blocked [{}, {}, {110[T], 111[T], 113[T]}, {}, {}] Step with 97 Trace 121[T], 118[T], 114[T], 95[(-1+x1^0 <= 0)], 97[T] Blocked [{}, {}, {110[T], 111[T], 113[T]}, {}, {}, {}] Backtrack Trace 121[T], 118[T], 114[T], 95[(-1+x1^0 <= 0)] Blocked [{}, {}, {110[T], 111[T], 113[T]}, {}, {97[T]}] Backtrack Trace 121[T], 118[T], 114[T] Blocked [{}, {}, {110[T], 111[T], 113[T]}, {95[T]}] Step with 96 Trace 121[T], 118[T], 114[T], 96[(3-x1^0 <= 0)] Blocked [{}, {}, {110[T], 111[T], 113[T]}, {95[T]}, {}] Step with 97 Trace 121[T], 118[T], 114[T], 96[(3-x1^0 <= 0)], 97[T] Blocked [{}, {}, {110[T], 111[T], 113[T]}, {95[T]}, {}, {}] Backtrack Trace 121[T], 118[T], 114[T], 96[(3-x1^0 <= 0)] Blocked [{}, {}, {110[T], 111[T], 113[T]}, {95[T]}, {97[T]}] Backtrack Trace 121[T], 118[T], 114[T] Blocked [{}, {}, {110[T], 111[T], 113[T]}, {95[T], 96[T]}] Step with 98 Trace 121[T], 118[T], 114[T], 98[T] Blocked [{}, {}, {110[T], 111[T], 113[T]}, {95[T], 96[T]}, {}] Step with 70 Trace 121[T], 118[T], 114[T], 98[T], 70[(1-r^0 <= 0 /\ 1-r^0 == 0 /\ -1+r^0 <= 0)] Blocked [{}, {}, {110[T], 111[T], 113[T]}, {95[T], 96[T]}, {}, {}] Backtrack Trace 121[T], 118[T], 114[T], 98[T] Blocked [{}, {}, {110[T], 111[T], 113[T]}, {95[T], 96[T]}, {70[T]}] Backtrack Trace 121[T], 118[T], 114[T] Blocked [{}, {}, {110[T], 111[T], 113[T]}, {95[T], 96[T], 98[T]}] Step with 99 Trace 121[T], 118[T], 114[T], 99[T] Blocked [{}, {}, {110[T], 111[T], 113[T]}, {95[T], 96[T], 98[T]}, {}] Step with 81 Trace 121[T], 118[T], 114[T], 99[T], 81[(-1+x1^0 <= 0)] Blocked [{}, {}, {110[T], 111[T], 113[T]}, {95[T], 96[T], 98[T]}, {}, {}] Step with 83 Trace 121[T], 118[T], 114[T], 99[T], 81[(-1+x1^0 <= 0)], 83[T] Blocked [{}, {}, {110[T], 111[T], 113[T]}, {95[T], 96[T], 98[T]}, {}, {}, {}] Backtrack Trace 121[T], 118[T], 114[T], 99[T], 81[(-1+x1^0 <= 0)] Blocked [{}, {}, {110[T], 111[T], 113[T]}, {95[T], 96[T], 98[T]}, {}, {83[T]}] Backtrack Trace 121[T], 118[T], 114[T], 99[T] Blocked [{}, {}, {110[T], 111[T], 113[T]}, {95[T], 96[T], 98[T]}, {81[T]}] Step with 82 Trace 121[T], 118[T], 114[T], 99[T], 82[(3-x1^0 <= 0)] Blocked [{}, {}, {110[T], 111[T], 113[T]}, {95[T], 96[T], 98[T]}, {81[T]}, {}] Step with 83 Trace 121[T], 118[T], 114[T], 99[T], 82[(3-x1^0 <= 0)], 83[T] Blocked [{}, {}, {110[T], 111[T], 113[T]}, {95[T], 96[T], 98[T]}, {81[T]}, {}, {}] Backtrack Trace 121[T], 118[T], 114[T], 99[T], 82[(3-x1^0 <= 0)] Blocked [{}, {}, {110[T], 111[T], 113[T]}, {95[T], 96[T], 98[T]}, {81[T]}, {83[T]}] Backtrack Trace 121[T], 118[T], 114[T], 99[T] Blocked [{}, {}, {110[T], 111[T], 113[T]}, {95[T], 96[T], 98[T]}, {81[T], 82[T]}] Step with 84 Trace 121[T], 118[T], 114[T], 99[T], 84[T] Blocked [{}, {}, {110[T], 111[T], 113[T]}, {95[T], 96[T], 98[T]}, {81[T], 82[T]}, {}] Step with 70 Trace 121[T], 118[T], 114[T], 99[T], 84[T], 70[(1-r^0 <= 0 /\ 1-r^0 == 0 /\ -1+r^0 <= 0)] Blocked [{}, {}, {110[T], 111[T], 113[T]}, {95[T], 96[T], 98[T]}, {81[T], 82[T]}, {}, {}] Backtrack Trace 121[T], 118[T], 114[T], 99[T], 84[T] Blocked [{}, {}, {110[T], 111[T], 113[T]}, {95[T], 96[T], 98[T]}, {81[T], 82[T]}, {70[T]}] Backtrack Trace 121[T], 118[T], 114[T], 99[T] Blocked [{}, {}, {110[T], 111[T], 113[T]}, {95[T], 96[T], 98[T]}, {81[T], 82[T], 84[T]}] Step with 122 Trace 121[T], 118[T], 114[T], 99[T], 122[T] Blocked [{}, {}, {110[T], 111[T], 113[T]}, {95[T], 96[T], 98[T]}, {81[T], 82[T], 84[T]}, {}] Nonterm Start location: l31 Program variables: r0^0 r^0 x1^0 x^0 67: l0 -> l1 : (-r0^0 <= 0 /\ -r0^0 == 0 /\ r0^0 <= 0), cost: 1 68: l2 -> l3 : (1-r^0 <= 0 /\ 1-r^0 == 0 /\ -1+r^0 <= 0), cost: 1 69: l4 -> l3 : (1-r^0 <= 0 /\ 1-r^0 == 0 /\ -1+r^0 <= 0), cost: 1 70: l5 -> l3 : (1-r^0 <= 0 /\ 1-r^0 == 0 /\ -1+r^0 <= 0), cost: 1 71: l6 -> l7 : x1^0'=x^0, T, cost: 1 72: l6 -> l3 : T, cost: 1 123: l6 -> l6 : T, cost: 1 73: l7 -> l9 : -1+x1^0 <= 0, cost: 1 74: l7 -> l9 : 3-x1^0 <= 0, cost: 1 76: l7 -> l2 : r^0'=1, T, cost: 1 124: l7 -> l7 : T, cost: 1 75: l9 -> l2 : r^0'=0, T, cost: 1 77: l11 -> l12 : -1+x1^0 <= 0, cost: 1 78: l11 -> l12 : 3-x1^0 <= 0, cost: 1 80: l11 -> l4 : r^0'=1, T, cost: 1 125: l11 -> l11 : T, cost: 1 79: l12 -> l4 : r^0'=0, T, cost: 1 81: l14 -> l15 : -1+x1^0 <= 0, cost: 1 82: l14 -> l15 : 3-x1^0 <= 0, cost: 1 84: l14 -> l5 : r^0'=1, T, cost: 1 122: l14 -> l14 : T, cost: 1 126: l14 -> LoAT_sink : -1+n >= 0, cost: NONTERM 83: l15 -> l5 : r^0'=0, T, cost: 1 85: l17 -> l18 : -1+x1^0 <= 0, cost: 1 86: l17 -> l18 : 3-x1^0 <= 0, cost: 1 88: l17 -> l2 : r^0'=1, T, cost: 1 89: l17 -> l7 : x^0'=2, T, cost: 1 87: l18 -> l2 : r^0'=0, T, cost: 1 90: l19 -> l20 : -1+x1^0 <= 0, cost: 1 91: l19 -> l20 : 3-x1^0 <= 0, cost: 1 93: l19 -> l4 : r^0'=1, T, cost: 1 94: l19 -> l11 : x^0'=2, T, cost: 1 92: l20 -> l4 : r^0'=0, T, cost: 1 95: l21 -> l22 : -1+x1^0 <= 0, cost: 1 96: l21 -> l22 : 3-x1^0 <= 0, cost: 1 98: l21 -> l5 : r^0'=1, T, cost: 1 99: l21 -> l14 : x^0'=2, T, cost: 1 97: l22 -> l5 : r^0'=0, T, cost: 1 100: l23 -> l24 : -1+x1^0 <= 0, cost: 1 101: l23 -> l24 : 3-x1^0 <= 0, cost: 1 103: l23 -> l2 : r^0'=1, T, cost: 1 104: l23 -> l17 : x^0'=1, T, cost: 1 102: l24 -> l2 : r^0'=0, T, cost: 1 105: l25 -> l26 : -1+x1^0 <= 0, cost: 1 106: l25 -> l26 : 3-x1^0 <= 0, cost: 1 108: l25 -> l4 : r^0'=1, T, cost: 1 109: l25 -> l19 : x^0'=1, T, cost: 1 107: l26 -> l4 : r^0'=0, T, cost: 1 110: l27 -> l28 : -1+x1^0 <= 0, cost: 1 111: l27 -> l28 : 3-x1^0 <= 0, cost: 1 113: l27 -> l5 : r^0'=1, T, cost: 1 114: l27 -> l21 : x^0'=1, T, cost: 1 112: l28 -> l5 : r^0'=0, T, cost: 1 115: l29 -> l19 : x1^0'=x^0, T, cost: 1 116: l29 -> l6 : x^0'=2, T, cost: 1 117: l29 -> l3 : T, cost: 1 118: l30 -> l27 : x1^0'=x^0, T, cost: 1 119: l30 -> l29 : x^0'=1, T, cost: 1 120: l30 -> l3 : T, cost: 1 121: l31 -> l30 : T, cost: 1 Certificate of Non-Termination Original rule: l14 -> l14 : T, cost: 1 New rule: l14 -> LoAT_sink : -1+n >= 0, cost: NONTERM Replacement map: {} Step with 126 Trace 121[T], 118[T], 114[T], 99[T], 126[-1+n >= 0] Blocked [{}, {}, {110[T], 111[T], 113[T]}, {95[T], 96[T], 98[T]}, {81[T], 82[T], 84[T]}, {126[T]}] Refute Counterexample [ r0^0=0 r^0=0 x1^0=0 x^0=3 ] 121 [ r0^0=0 r^0=0 x1^0=3 x^0=3 ] 118 [ r0^0=0 r^0=0 x1^0=3 x^0=1 ] 114 [ r0^0=0 r^0=0 x1^0=3 x^0=2 ] 99 [ r0^0=0 r^0=0 x1^0=0 x^0=3 ] 126 NO Build SHA: a05f16bf13df659c382799650051f91bf6828c7b