unknown Initial ITS Start location: l11 Program variables: b_16^0 rt_11^0 st_15^0 x_14^0 0: l0 -> l1 : b_16^0'=b_16^post1, rt_11^0'=rt_11^post1, st_15^0'=st_15^post1, x_14^0'=x_14^post1, (1-x_14^0 <= 0 /\ -st_15^post1+st_15^0 == 0 /\ rt_11^0-rt_11^post1 == 0 /\ -1+b_16^post1 == 0 /\ -x_14^post1+x_14^0 == 0), cost: 1 4: l1 -> l5 : b_16^0'=b_16^post5, rt_11^0'=rt_11^post5, st_15^0'=st_15^post5, x_14^0'=x_14^post5, (-x_14^0 <= 0 /\ -st_15^post5+st_15^0 == 0 /\ -b_16^post5+b_16^0 == 0 /\ x_14^0 <= 0 /\ -x_14^post5+x_14^0 == 0 /\ rt_11^post5-st_15^0 == 0), cost: 1 5: l1 -> l6 : b_16^0'=b_16^post6, rt_11^0'=rt_11^post6, st_15^0'=st_15^post6, x_14^0'=x_14^post6, (-b_16^post6+b_16^0 == 0 /\ -x_14^post6+x_14^0 == 0 /\ 1-x_14^0 <= 0 /\ rt_11^0-rt_11^post6 == 0 /\ -st_15^post6+st_15^0 == 0), cost: 1 6: l1 -> l6 : b_16^0'=b_16^post7, rt_11^0'=rt_11^post7, st_15^0'=st_15^post7, x_14^0'=x_14^post7, (-st_15^post7+st_15^0 == 0 /\ -rt_11^post7+rt_11^0 == 0 /\ x_14^0-x_14^post7 == 0 /\ b_16^0-b_16^post7 == 0 /\ 1+x_14^0 <= 0), cost: 1 1: l2 -> l4 : b_16^0'=b_16^post2, rt_11^0'=rt_11^post2, st_15^0'=st_15^post2, x_14^0'=x_14^post2, (1-x_14^0 <= 0 /\ -st_15^post2+st_15^0 == 0 /\ x_14^0-x_14^post2 == 0 /\ -b_16^post2+b_16^0 == 0 /\ -rt_11^post2+rt_11^0 == 0), cost: 1 2: l2 -> l4 : b_16^0'=b_16^post3, rt_11^0'=rt_11^post3, st_15^0'=st_15^post3, x_14^0'=x_14^post3, (x_14^0-x_14^post3 == 0 /\ -st_15^post3+st_15^0 == 0 /\ 1+x_14^0 <= 0 /\ -b_16^post3+b_16^0 == 0 /\ rt_11^0-rt_11^post3 == 0), cost: 1 3: l4 -> l3 : b_16^0'=b_16^post4, rt_11^0'=rt_11^post4, st_15^0'=st_15^post4, x_14^0'=x_14^post4, (b_16^post4 == 0 /\ rt_11^0-rt_11^post4 == 0 /\ -st_15^post4+st_15^0 == 0 /\ 1-b_16^0 <= 0 /\ -1+b_16^0 <= 0 /\ 1+x_14^post4-x_14^0 == 0), cost: 1 14: l3 -> l7 : b_16^0'=b_16^post15, rt_11^0'=rt_11^post15, st_15^0'=st_15^post15, x_14^0'=x_14^post15, (x_14^post15+x_14^0 == 0 /\ -st_15^post15+st_15^0 == 0 /\ -b_16^post15+b_16^0 == 0 /\ rt_11^0-rt_11^post15 == 0), cost: 1 7: l6 -> l3 : b_16^0'=b_16^post8, rt_11^0'=rt_11^post8, st_15^0'=st_15^post8, x_14^0'=x_14^post8, (1+x_14^post8-x_14^0 == 0 /\ -st_15^post8+st_15^0 == 0 /\ b_16^post8 == 0 /\ rt_11^0-rt_11^post8 == 0 /\ 1-b_16^0 <= 0 /\ -1+b_16^0 <= 0), cost: 1 8: l7 -> l5 : b_16^0'=b_16^post9, rt_11^0'=rt_11^post9, st_15^0'=st_15^post9, x_14^0'=x_14^post9, (st_15^0-st_15^post9 == 0 /\ rt_11^post9-st_15^0 == 0 /\ -x_14^0 <= 0 /\ -x_14^post9+x_14^0 == 0 /\ x_14^0 <= 0 /\ -b_16^post9+b_16^0 == 0), cost: 1 9: l7 -> l8 : b_16^0'=b_16^post10, rt_11^0'=rt_11^post10, st_15^0'=st_15^post10, x_14^0'=x_14^post10, (-x_14^post10+x_14^0 == 0 /\ -b_16^post10+b_16^0 == 0 /\ 1-x_14^0 <= 0 /\ rt_11^0-rt_11^post10 == 0 /\ -st_15^post10+st_15^0 == 0), cost: 1 10: l7 -> l8 : b_16^0'=b_16^post11, rt_11^0'=rt_11^post11, st_15^0'=st_15^post11, x_14^0'=x_14^post11, (-rt_11^post11+rt_11^0 == 0 /\ x_14^0-x_14^post11 == 0 /\ 1+x_14^0 <= 0 /\ -st_15^post11+st_15^0 == 0 /\ b_16^0-b_16^post11 == 0), cost: 1 11: l8 -> l9 : b_16^0'=b_16^post12, rt_11^0'=rt_11^post12, st_15^0'=st_15^post12, x_14^0'=x_14^post12, (-b_16^post12+b_16^0 == 0 /\ -x_14^post12+x_14^0 == 0 /\ rt_11^0-rt_11^post12 == 0 /\ 2-b_16^0 <= 0 /\ -st_15^post12+st_15^0 == 0), cost: 1 12: l8 -> l9 : b_16^0'=b_16^post13, rt_11^0'=rt_11^post13, st_15^0'=st_15^post13, x_14^0'=x_14^post13, (-b_16^post13+b_16^0 == 0 /\ rt_11^0-rt_11^post13 == 0 /\ -x_14^post13+x_14^0 == 0 /\ b_16^0 <= 0 /\ -st_15^post13+st_15^0 == 0), cost: 1 13: l9 -> l1 : b_16^0'=b_16^post14, rt_11^0'=rt_11^post14, st_15^0'=st_15^post14, x_14^0'=x_14^post14, (-st_15^post14+st_15^0 == 0 /\ rt_11^0-rt_11^post14 == 0 /\ -1+b_16^post14 == 0 /\ x_14^post14+x_14^1 == 0 /\ -1-x_14^0+x_14^1 == 0), cost: 1 15: l10 -> l7 : b_16^0'=b_16^post16, rt_11^0'=rt_11^post16, st_15^0'=st_15^post16, x_14^0'=x_14^post16, (x_14^0+x_14^post16 == 0 /\ -b_16^post16+b_16^0 == 0 /\ -st_15^post16+st_15^0 == 0 /\ -rt_11^post16+rt_11^0 == 0), cost: 1 16: l11 -> l0 : b_16^0'=b_16^post17, rt_11^0'=rt_11^post17, st_15^0'=st_15^post17, x_14^0'=x_14^post17, (-x_14^post17+x_14^0 == 0 /\ -st_15^post17+st_15^0 == 0 /\ b_16^0-b_16^post17 == 0 /\ rt_11^0-rt_11^post17 == 0), cost: 1 Chained Linear Paths Start location: l11 Program variables: b_16^0 rt_11^0 st_15^0 x_14^0 4: l1 -> l5 : b_16^0'=b_16^post5, rt_11^0'=rt_11^post5, st_15^0'=st_15^post5, x_14^0'=x_14^post5, (-x_14^0 <= 0 /\ -st_15^post5+st_15^0 == 0 /\ -b_16^post5+b_16^0 == 0 /\ x_14^0 <= 0 /\ -x_14^post5+x_14^0 == 0 /\ rt_11^post5-st_15^0 == 0), cost: 1 5: l1 -> l6 : b_16^0'=b_16^post6, rt_11^0'=rt_11^post6, st_15^0'=st_15^post6, x_14^0'=x_14^post6, (-b_16^post6+b_16^0 == 0 /\ -x_14^post6+x_14^0 == 0 /\ 1-x_14^0 <= 0 /\ rt_11^0-rt_11^post6 == 0 /\ -st_15^post6+st_15^0 == 0), cost: 1 6: l1 -> l6 : b_16^0'=b_16^post7, rt_11^0'=rt_11^post7, st_15^0'=st_15^post7, x_14^0'=x_14^post7, (-st_15^post7+st_15^0 == 0 /\ -rt_11^post7+rt_11^0 == 0 /\ x_14^0-x_14^post7 == 0 /\ b_16^0-b_16^post7 == 0 /\ 1+x_14^0 <= 0), cost: 1 1: l2 -> l4 : b_16^0'=b_16^post2, rt_11^0'=rt_11^post2, st_15^0'=st_15^post2, x_14^0'=x_14^post2, (1-x_14^0 <= 0 /\ -st_15^post2+st_15^0 == 0 /\ x_14^0-x_14^post2 == 0 /\ -b_16^post2+b_16^0 == 0 /\ -rt_11^post2+rt_11^0 == 0), cost: 1 2: l2 -> l4 : b_16^0'=b_16^post3, rt_11^0'=rt_11^post3, st_15^0'=st_15^post3, x_14^0'=x_14^post3, (x_14^0-x_14^post3 == 0 /\ -st_15^post3+st_15^0 == 0 /\ 1+x_14^0 <= 0 /\ -b_16^post3+b_16^0 == 0 /\ rt_11^0-rt_11^post3 == 0), cost: 1 3: l4 -> l3 : b_16^0'=b_16^post4, rt_11^0'=rt_11^post4, st_15^0'=st_15^post4, x_14^0'=x_14^post4, (b_16^post4 == 0 /\ rt_11^0-rt_11^post4 == 0 /\ -st_15^post4+st_15^0 == 0 /\ 1-b_16^0 <= 0 /\ -1+b_16^0 <= 0 /\ 1+x_14^post4-x_14^0 == 0), cost: 1 14: l3 -> l7 : b_16^0'=b_16^post15, rt_11^0'=rt_11^post15, st_15^0'=st_15^post15, x_14^0'=x_14^post15, (x_14^post15+x_14^0 == 0 /\ -st_15^post15+st_15^0 == 0 /\ -b_16^post15+b_16^0 == 0 /\ rt_11^0-rt_11^post15 == 0), cost: 1 7: l6 -> l3 : b_16^0'=b_16^post8, rt_11^0'=rt_11^post8, st_15^0'=st_15^post8, x_14^0'=x_14^post8, (1+x_14^post8-x_14^0 == 0 /\ -st_15^post8+st_15^0 == 0 /\ b_16^post8 == 0 /\ rt_11^0-rt_11^post8 == 0 /\ 1-b_16^0 <= 0 /\ -1+b_16^0 <= 0), cost: 1 8: l7 -> l5 : b_16^0'=b_16^post9, rt_11^0'=rt_11^post9, st_15^0'=st_15^post9, x_14^0'=x_14^post9, (st_15^0-st_15^post9 == 0 /\ rt_11^post9-st_15^0 == 0 /\ -x_14^0 <= 0 /\ -x_14^post9+x_14^0 == 0 /\ x_14^0 <= 0 /\ -b_16^post9+b_16^0 == 0), cost: 1 9: l7 -> l8 : b_16^0'=b_16^post10, rt_11^0'=rt_11^post10, st_15^0'=st_15^post10, x_14^0'=x_14^post10, (-x_14^post10+x_14^0 == 0 /\ -b_16^post10+b_16^0 == 0 /\ 1-x_14^0 <= 0 /\ rt_11^0-rt_11^post10 == 0 /\ -st_15^post10+st_15^0 == 0), cost: 1 10: l7 -> l8 : b_16^0'=b_16^post11, rt_11^0'=rt_11^post11, st_15^0'=st_15^post11, x_14^0'=x_14^post11, (-rt_11^post11+rt_11^0 == 0 /\ x_14^0-x_14^post11 == 0 /\ 1+x_14^0 <= 0 /\ -st_15^post11+st_15^0 == 0 /\ b_16^0-b_16^post11 == 0), cost: 1 11: l8 -> l9 : b_16^0'=b_16^post12, rt_11^0'=rt_11^post12, st_15^0'=st_15^post12, x_14^0'=x_14^post12, (-b_16^post12+b_16^0 == 0 /\ -x_14^post12+x_14^0 == 0 /\ rt_11^0-rt_11^post12 == 0 /\ 2-b_16^0 <= 0 /\ -st_15^post12+st_15^0 == 0), cost: 1 12: l8 -> l9 : b_16^0'=b_16^post13, rt_11^0'=rt_11^post13, st_15^0'=st_15^post13, x_14^0'=x_14^post13, (-b_16^post13+b_16^0 == 0 /\ rt_11^0-rt_11^post13 == 0 /\ -x_14^post13+x_14^0 == 0 /\ b_16^0 <= 0 /\ -st_15^post13+st_15^0 == 0), cost: 1 13: l9 -> l1 : b_16^0'=b_16^post14, rt_11^0'=rt_11^post14, st_15^0'=st_15^post14, x_14^0'=x_14^post14, (-st_15^post14+st_15^0 == 0 /\ rt_11^0-rt_11^post14 == 0 /\ -1+b_16^post14 == 0 /\ x_14^post14+x_14^1 == 0 /\ -1-x_14^0+x_14^1 == 0), cost: 1 15: l10 -> l7 : b_16^0'=b_16^post16, rt_11^0'=rt_11^post16, st_15^0'=st_15^post16, x_14^0'=x_14^post16, (x_14^0+x_14^post16 == 0 /\ -b_16^post16+b_16^0 == 0 /\ -st_15^post16+st_15^0 == 0 /\ -rt_11^post16+rt_11^0 == 0), cost: 1 17: l11 -> l1 : b_16^0'=b_16^post1, rt_11^0'=rt_11^post1, st_15^0'=st_15^post1, x_14^0'=x_14^post1, (1-x_14^post17 <= 0 /\ -st_15^post1+st_15^post17 == 0 /\ -x_14^post17+x_14^0 == 0 /\ -st_15^post17+st_15^0 == 0 /\ x_14^post17-x_14^post1 == 0 /\ b_16^0-b_16^post17 == 0 /\ rt_11^post17-rt_11^post1 == 0 /\ rt_11^0-rt_11^post17 == 0 /\ -1+b_16^post1 == 0), cost: 1 Eliminating location l0 by chaining: Applied chaining First rule: l11 -> l0 : b_16^0'=b_16^post17, rt_11^0'=rt_11^post17, st_15^0'=st_15^post17, x_14^0'=x_14^post17, (-x_14^post17+x_14^0 == 0 /\ -st_15^post17+st_15^0 == 0 /\ b_16^0-b_16^post17 == 0 /\ rt_11^0-rt_11^post17 == 0), cost: 1 Second rule: l0 -> l1 : b_16^0'=b_16^post1, rt_11^0'=rt_11^post1, st_15^0'=st_15^post1, x_14^0'=x_14^post1, (1-x_14^0 <= 0 /\ -st_15^post1+st_15^0 == 0 /\ rt_11^0-rt_11^post1 == 0 /\ -1+b_16^post1 == 0 /\ -x_14^post1+x_14^0 == 0), cost: 1 New rule: l11 -> l1 : b_16^0'=b_16^post1, rt_11^0'=rt_11^post1, st_15^0'=st_15^post1, x_14^0'=x_14^post1, (1-x_14^post17 <= 0 /\ -st_15^post1+st_15^post17 == 0 /\ -x_14^post17+x_14^0 == 0 /\ -st_15^post17+st_15^0 == 0 /\ x_14^post17-x_14^post1 == 0 /\ b_16^0-b_16^post17 == 0 /\ rt_11^post17-rt_11^post1 == 0 /\ rt_11^0-rt_11^post17 == 0 /\ -1+b_16^post1 == 0), cost: 1 Applied deletion Removed the following rules: 0 16 Simplified Transitions Start location: l11 Program variables: b_16^0 rt_11^0 st_15^0 x_14^0 21: l1 -> l5 : rt_11^0'=st_15^0, (-x_14^0 <= 0 /\ -x_14^0 == 0 /\ x_14^0 <= 0), cost: 1 22: l1 -> l6 : 1-x_14^0 <= 0, cost: 1 23: l1 -> l6 : 1+x_14^0 <= 0, cost: 1 18: l2 -> l4 : 1-x_14^0 <= 0, cost: 1 19: l2 -> l4 : 1+x_14^0 <= 0, cost: 1 20: l4 -> l3 : b_16^0'=0, x_14^0'=-1+x_14^0, (1-b_16^0 <= 0 /\ 1-b_16^0 == 0 /\ -1+b_16^0 <= 0), cost: 1 31: l3 -> l7 : x_14^0'=-x_14^0, T, cost: 1 24: l6 -> l3 : b_16^0'=0, x_14^0'=-1+x_14^0, (1-b_16^0 <= 0 /\ 1-b_16^0 == 0 /\ -1+b_16^0 <= 0), cost: 1 25: l7 -> l5 : rt_11^0'=st_15^0, (-x_14^0 <= 0 /\ -x_14^0 == 0 /\ x_14^0 <= 0), cost: 1 26: l7 -> l8 : 1-x_14^0 <= 0, cost: 1 27: l7 -> l8 : 1+x_14^0 <= 0, cost: 1 28: l8 -> l9 : 2-b_16^0 <= 0, cost: 1 29: l8 -> l9 : b_16^0 <= 0, cost: 1 30: l9 -> l1 : b_16^0'=1, x_14^0'=-1-x_14^0, T, cost: 1 32: l10 -> l7 : x_14^0'=-x_14^0, T, cost: 1 33: l11 -> l1 : b_16^0'=1, 1-x_14^0 <= 0, cost: 1 Propagated Equalities Original rule: l2 -> l4 : b_16^0'=b_16^post2, rt_11^0'=rt_11^post2, st_15^0'=st_15^post2, x_14^0'=x_14^post2, (1-x_14^0 <= 0 /\ -st_15^post2+st_15^0 == 0 /\ x_14^0-x_14^post2 == 0 /\ -b_16^post2+b_16^0 == 0 /\ -rt_11^post2+rt_11^0 == 0), cost: 1 New rule: l2 -> l4 : b_16^0'=b_16^0, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=x_14^0, (0 == 0 /\ 1-x_14^0 <= 0), cost: 1 propagated equality st_15^post2 = st_15^0 propagated equality x_14^post2 = x_14^0 propagated equality b_16^post2 = b_16^0 propagated equality rt_11^post2 = rt_11^0 Simplified Guard Original rule: l2 -> l4 : b_16^0'=b_16^0, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=x_14^0, (0 == 0 /\ 1-x_14^0 <= 0), cost: 1 New rule: l2 -> l4 : b_16^0'=b_16^0, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=x_14^0, 1-x_14^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l2 -> l4 : b_16^0'=b_16^0, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=x_14^0, 1-x_14^0 <= 0, cost: 1 New rule: l2 -> l4 : 1-x_14^0 <= 0, cost: 1 Propagated Equalities Original rule: l2 -> l4 : b_16^0'=b_16^post3, rt_11^0'=rt_11^post3, st_15^0'=st_15^post3, x_14^0'=x_14^post3, (x_14^0-x_14^post3 == 0 /\ -st_15^post3+st_15^0 == 0 /\ 1+x_14^0 <= 0 /\ -b_16^post3+b_16^0 == 0 /\ rt_11^0-rt_11^post3 == 0), cost: 1 New rule: l2 -> l4 : b_16^0'=b_16^0, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=x_14^0, (0 == 0 /\ 1+x_14^0 <= 0), cost: 1 propagated equality x_14^post3 = x_14^0 propagated equality st_15^post3 = st_15^0 propagated equality b_16^post3 = b_16^0 propagated equality rt_11^post3 = rt_11^0 Simplified Guard Original rule: l2 -> l4 : b_16^0'=b_16^0, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=x_14^0, (0 == 0 /\ 1+x_14^0 <= 0), cost: 1 New rule: l2 -> l4 : b_16^0'=b_16^0, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=x_14^0, 1+x_14^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l2 -> l4 : b_16^0'=b_16^0, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=x_14^0, 1+x_14^0 <= 0, cost: 1 New rule: l2 -> l4 : 1+x_14^0 <= 0, cost: 1 made implied equalities explicit Original rule: l4 -> l3 : b_16^0'=b_16^post4, rt_11^0'=rt_11^post4, st_15^0'=st_15^post4, x_14^0'=x_14^post4, (b_16^post4 == 0 /\ rt_11^0-rt_11^post4 == 0 /\ -st_15^post4+st_15^0 == 0 /\ 1-b_16^0 <= 0 /\ -1+b_16^0 <= 0 /\ 1+x_14^post4-x_14^0 == 0), cost: 1 New rule: l4 -> l3 : b_16^0'=b_16^post4, rt_11^0'=rt_11^post4, st_15^0'=st_15^post4, x_14^0'=x_14^post4, (b_16^post4 == 0 /\ rt_11^0-rt_11^post4 == 0 /\ -st_15^post4+st_15^0 == 0 /\ 1-b_16^0 <= 0 /\ 1-b_16^0 == 0 /\ -1+b_16^0 <= 0 /\ 1+x_14^post4-x_14^0 == 0), cost: 1 Propagated Equalities Original rule: l4 -> l3 : b_16^0'=b_16^post4, rt_11^0'=rt_11^post4, st_15^0'=st_15^post4, x_14^0'=x_14^post4, (b_16^post4 == 0 /\ rt_11^0-rt_11^post4 == 0 /\ -st_15^post4+st_15^0 == 0 /\ 1-b_16^0 <= 0 /\ 1-b_16^0 == 0 /\ -1+b_16^0 <= 0 /\ 1+x_14^post4-x_14^0 == 0), cost: 1 New rule: l4 -> l3 : b_16^0'=0, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=-1+x_14^0, (0 == 0 /\ 1-b_16^0 <= 0 /\ 1-b_16^0 == 0 /\ -1+b_16^0 <= 0), cost: 1 propagated equality b_16^post4 = 0 propagated equality rt_11^post4 = rt_11^0 propagated equality st_15^post4 = st_15^0 propagated equality x_14^post4 = -1+x_14^0 Simplified Guard Original rule: l4 -> l3 : b_16^0'=0, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=-1+x_14^0, (0 == 0 /\ 1-b_16^0 <= 0 /\ 1-b_16^0 == 0 /\ -1+b_16^0 <= 0), cost: 1 New rule: l4 -> l3 : b_16^0'=0, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=-1+x_14^0, (1-b_16^0 <= 0 /\ 1-b_16^0 == 0 /\ -1+b_16^0 <= 0), cost: 1 made implied equalities explicit Original rule: l4 -> l3 : b_16^0'=0, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=-1+x_14^0, (1-b_16^0 <= 0 /\ 1-b_16^0 == 0 /\ -1+b_16^0 <= 0), cost: 1 New rule: l4 -> l3 : b_16^0'=0, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=-1+x_14^0, (1-b_16^0 <= 0 /\ 1-b_16^0 == 0 /\ -1+b_16^0 <= 0), cost: 1 Removed Trivial Updates Original rule: l4 -> l3 : b_16^0'=0, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=-1+x_14^0, (1-b_16^0 <= 0 /\ 1-b_16^0 == 0 /\ -1+b_16^0 <= 0), cost: 1 New rule: l4 -> l3 : b_16^0'=0, x_14^0'=-1+x_14^0, (1-b_16^0 <= 0 /\ 1-b_16^0 == 0 /\ -1+b_16^0 <= 0), cost: 1 made implied equalities explicit Original rule: l1 -> l5 : b_16^0'=b_16^post5, rt_11^0'=rt_11^post5, st_15^0'=st_15^post5, x_14^0'=x_14^post5, (-x_14^0 <= 0 /\ -st_15^post5+st_15^0 == 0 /\ -b_16^post5+b_16^0 == 0 /\ x_14^0 <= 0 /\ -x_14^post5+x_14^0 == 0 /\ rt_11^post5-st_15^0 == 0), cost: 1 New rule: l1 -> l5 : b_16^0'=b_16^post5, rt_11^0'=rt_11^post5, st_15^0'=st_15^post5, x_14^0'=x_14^post5, (-x_14^0 <= 0 /\ -x_14^0 == 0 /\ -st_15^post5+st_15^0 == 0 /\ -b_16^post5+b_16^0 == 0 /\ x_14^0 <= 0 /\ -x_14^post5+x_14^0 == 0 /\ rt_11^post5-st_15^0 == 0), cost: 1 Propagated Equalities Original rule: l1 -> l5 : b_16^0'=b_16^post5, rt_11^0'=rt_11^post5, st_15^0'=st_15^post5, x_14^0'=x_14^post5, (-x_14^0 <= 0 /\ -x_14^0 == 0 /\ -st_15^post5+st_15^0 == 0 /\ -b_16^post5+b_16^0 == 0 /\ x_14^0 <= 0 /\ -x_14^post5+x_14^0 == 0 /\ rt_11^post5-st_15^0 == 0), cost: 1 New rule: l1 -> l5 : b_16^0'=b_16^0, rt_11^0'=st_15^0, st_15^0'=st_15^0, x_14^0'=x_14^0, (0 == 0 /\ -x_14^0 <= 0 /\ -x_14^0 == 0 /\ x_14^0 <= 0), cost: 1 propagated equality st_15^post5 = st_15^0 propagated equality b_16^post5 = b_16^0 propagated equality x_14^post5 = x_14^0 propagated equality rt_11^post5 = st_15^0 Simplified Guard Original rule: l1 -> l5 : b_16^0'=b_16^0, rt_11^0'=st_15^0, st_15^0'=st_15^0, x_14^0'=x_14^0, (0 == 0 /\ -x_14^0 <= 0 /\ -x_14^0 == 0 /\ x_14^0 <= 0), cost: 1 New rule: l1 -> l5 : b_16^0'=b_16^0, rt_11^0'=st_15^0, st_15^0'=st_15^0, x_14^0'=x_14^0, (-x_14^0 <= 0 /\ -x_14^0 == 0 /\ x_14^0 <= 0), cost: 1 made implied equalities explicit Original rule: l1 -> l5 : b_16^0'=b_16^0, rt_11^0'=st_15^0, st_15^0'=st_15^0, x_14^0'=x_14^0, (-x_14^0 <= 0 /\ -x_14^0 == 0 /\ x_14^0 <= 0), cost: 1 New rule: l1 -> l5 : b_16^0'=b_16^0, rt_11^0'=st_15^0, st_15^0'=st_15^0, x_14^0'=x_14^0, (-x_14^0 <= 0 /\ -x_14^0 == 0 /\ x_14^0 <= 0), cost: 1 Removed Trivial Updates Original rule: l1 -> l5 : b_16^0'=b_16^0, rt_11^0'=st_15^0, st_15^0'=st_15^0, x_14^0'=x_14^0, (-x_14^0 <= 0 /\ -x_14^0 == 0 /\ x_14^0 <= 0), cost: 1 New rule: l1 -> l5 : rt_11^0'=st_15^0, (-x_14^0 <= 0 /\ -x_14^0 == 0 /\ x_14^0 <= 0), cost: 1 Propagated Equalities Original rule: l1 -> l6 : b_16^0'=b_16^post6, rt_11^0'=rt_11^post6, st_15^0'=st_15^post6, x_14^0'=x_14^post6, (-b_16^post6+b_16^0 == 0 /\ -x_14^post6+x_14^0 == 0 /\ 1-x_14^0 <= 0 /\ rt_11^0-rt_11^post6 == 0 /\ -st_15^post6+st_15^0 == 0), cost: 1 New rule: l1 -> l6 : b_16^0'=b_16^0, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=x_14^0, (0 == 0 /\ 1-x_14^0 <= 0), cost: 1 propagated equality b_16^post6 = b_16^0 propagated equality x_14^post6 = x_14^0 propagated equality rt_11^post6 = rt_11^0 propagated equality st_15^post6 = st_15^0 Simplified Guard Original rule: l1 -> l6 : b_16^0'=b_16^0, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=x_14^0, (0 == 0 /\ 1-x_14^0 <= 0), cost: 1 New rule: l1 -> l6 : b_16^0'=b_16^0, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=x_14^0, 1-x_14^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l1 -> l6 : b_16^0'=b_16^0, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=x_14^0, 1-x_14^0 <= 0, cost: 1 New rule: l1 -> l6 : 1-x_14^0 <= 0, cost: 1 Propagated Equalities Original rule: l1 -> l6 : b_16^0'=b_16^post7, rt_11^0'=rt_11^post7, st_15^0'=st_15^post7, x_14^0'=x_14^post7, (-st_15^post7+st_15^0 == 0 /\ -rt_11^post7+rt_11^0 == 0 /\ x_14^0-x_14^post7 == 0 /\ b_16^0-b_16^post7 == 0 /\ 1+x_14^0 <= 0), cost: 1 New rule: l1 -> l6 : b_16^0'=b_16^0, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=x_14^0, (0 == 0 /\ 1+x_14^0 <= 0), cost: 1 propagated equality st_15^post7 = st_15^0 propagated equality rt_11^post7 = rt_11^0 propagated equality x_14^post7 = x_14^0 propagated equality b_16^post7 = b_16^0 Simplified Guard Original rule: l1 -> l6 : b_16^0'=b_16^0, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=x_14^0, (0 == 0 /\ 1+x_14^0 <= 0), cost: 1 New rule: l1 -> l6 : b_16^0'=b_16^0, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=x_14^0, 1+x_14^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l1 -> l6 : b_16^0'=b_16^0, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=x_14^0, 1+x_14^0 <= 0, cost: 1 New rule: l1 -> l6 : 1+x_14^0 <= 0, cost: 1 made implied equalities explicit Original rule: l6 -> l3 : b_16^0'=b_16^post8, rt_11^0'=rt_11^post8, st_15^0'=st_15^post8, x_14^0'=x_14^post8, (1+x_14^post8-x_14^0 == 0 /\ -st_15^post8+st_15^0 == 0 /\ b_16^post8 == 0 /\ rt_11^0-rt_11^post8 == 0 /\ 1-b_16^0 <= 0 /\ -1+b_16^0 <= 0), cost: 1 New rule: l6 -> l3 : b_16^0'=b_16^post8, rt_11^0'=rt_11^post8, st_15^0'=st_15^post8, x_14^0'=x_14^post8, (1+x_14^post8-x_14^0 == 0 /\ -st_15^post8+st_15^0 == 0 /\ b_16^post8 == 0 /\ rt_11^0-rt_11^post8 == 0 /\ 1-b_16^0 <= 0 /\ 1-b_16^0 == 0 /\ -1+b_16^0 <= 0), cost: 1 Propagated Equalities Original rule: l6 -> l3 : b_16^0'=b_16^post8, rt_11^0'=rt_11^post8, st_15^0'=st_15^post8, x_14^0'=x_14^post8, (1+x_14^post8-x_14^0 == 0 /\ -st_15^post8+st_15^0 == 0 /\ b_16^post8 == 0 /\ rt_11^0-rt_11^post8 == 0 /\ 1-b_16^0 <= 0 /\ 1-b_16^0 == 0 /\ -1+b_16^0 <= 0), cost: 1 New rule: l6 -> l3 : b_16^0'=0, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=-1+x_14^0, (0 == 0 /\ 1-b_16^0 <= 0 /\ 1-b_16^0 == 0 /\ -1+b_16^0 <= 0), cost: 1 propagated equality x_14^post8 = -1+x_14^0 propagated equality st_15^post8 = st_15^0 propagated equality b_16^post8 = 0 propagated equality rt_11^post8 = rt_11^0 Simplified Guard Original rule: l6 -> l3 : b_16^0'=0, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=-1+x_14^0, (0 == 0 /\ 1-b_16^0 <= 0 /\ 1-b_16^0 == 0 /\ -1+b_16^0 <= 0), cost: 1 New rule: l6 -> l3 : b_16^0'=0, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=-1+x_14^0, (1-b_16^0 <= 0 /\ 1-b_16^0 == 0 /\ -1+b_16^0 <= 0), cost: 1 made implied equalities explicit Original rule: l6 -> l3 : b_16^0'=0, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=-1+x_14^0, (1-b_16^0 <= 0 /\ 1-b_16^0 == 0 /\ -1+b_16^0 <= 0), cost: 1 New rule: l6 -> l3 : b_16^0'=0, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=-1+x_14^0, (1-b_16^0 <= 0 /\ 1-b_16^0 == 0 /\ -1+b_16^0 <= 0), cost: 1 Removed Trivial Updates Original rule: l6 -> l3 : b_16^0'=0, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=-1+x_14^0, (1-b_16^0 <= 0 /\ 1-b_16^0 == 0 /\ -1+b_16^0 <= 0), cost: 1 New rule: l6 -> l3 : b_16^0'=0, x_14^0'=-1+x_14^0, (1-b_16^0 <= 0 /\ 1-b_16^0 == 0 /\ -1+b_16^0 <= 0), cost: 1 made implied equalities explicit Original rule: l7 -> l5 : b_16^0'=b_16^post9, rt_11^0'=rt_11^post9, st_15^0'=st_15^post9, x_14^0'=x_14^post9, (st_15^0-st_15^post9 == 0 /\ rt_11^post9-st_15^0 == 0 /\ -x_14^0 <= 0 /\ -x_14^post9+x_14^0 == 0 /\ x_14^0 <= 0 /\ -b_16^post9+b_16^0 == 0), cost: 1 New rule: l7 -> l5 : b_16^0'=b_16^post9, rt_11^0'=rt_11^post9, st_15^0'=st_15^post9, x_14^0'=x_14^post9, (st_15^0-st_15^post9 == 0 /\ rt_11^post9-st_15^0 == 0 /\ -x_14^0 <= 0 /\ -x_14^0 == 0 /\ -x_14^post9+x_14^0 == 0 /\ x_14^0 <= 0 /\ -b_16^post9+b_16^0 == 0), cost: 1 Propagated Equalities Original rule: l7 -> l5 : b_16^0'=b_16^post9, rt_11^0'=rt_11^post9, st_15^0'=st_15^post9, x_14^0'=x_14^post9, (st_15^0-st_15^post9 == 0 /\ rt_11^post9-st_15^0 == 0 /\ -x_14^0 <= 0 /\ -x_14^0 == 0 /\ -x_14^post9+x_14^0 == 0 /\ x_14^0 <= 0 /\ -b_16^post9+b_16^0 == 0), cost: 1 New rule: l7 -> l5 : b_16^0'=b_16^0, rt_11^0'=st_15^0, st_15^0'=st_15^0, x_14^0'=x_14^0, (0 == 0 /\ -x_14^0 <= 0 /\ -x_14^0 == 0 /\ x_14^0 <= 0), cost: 1 propagated equality st_15^post9 = st_15^0 propagated equality rt_11^post9 = st_15^0 propagated equality x_14^post9 = x_14^0 propagated equality b_16^post9 = b_16^0 Simplified Guard Original rule: l7 -> l5 : b_16^0'=b_16^0, rt_11^0'=st_15^0, st_15^0'=st_15^0, x_14^0'=x_14^0, (0 == 0 /\ -x_14^0 <= 0 /\ -x_14^0 == 0 /\ x_14^0 <= 0), cost: 1 New rule: l7 -> l5 : b_16^0'=b_16^0, rt_11^0'=st_15^0, st_15^0'=st_15^0, x_14^0'=x_14^0, (-x_14^0 <= 0 /\ -x_14^0 == 0 /\ x_14^0 <= 0), cost: 1 made implied equalities explicit Original rule: l7 -> l5 : b_16^0'=b_16^0, rt_11^0'=st_15^0, st_15^0'=st_15^0, x_14^0'=x_14^0, (-x_14^0 <= 0 /\ -x_14^0 == 0 /\ x_14^0 <= 0), cost: 1 New rule: l7 -> l5 : b_16^0'=b_16^0, rt_11^0'=st_15^0, st_15^0'=st_15^0, x_14^0'=x_14^0, (-x_14^0 <= 0 /\ -x_14^0 == 0 /\ x_14^0 <= 0), cost: 1 Removed Trivial Updates Original rule: l7 -> l5 : b_16^0'=b_16^0, rt_11^0'=st_15^0, st_15^0'=st_15^0, x_14^0'=x_14^0, (-x_14^0 <= 0 /\ -x_14^0 == 0 /\ x_14^0 <= 0), cost: 1 New rule: l7 -> l5 : rt_11^0'=st_15^0, (-x_14^0 <= 0 /\ -x_14^0 == 0 /\ x_14^0 <= 0), cost: 1 Propagated Equalities Original rule: l7 -> l8 : b_16^0'=b_16^post10, rt_11^0'=rt_11^post10, st_15^0'=st_15^post10, x_14^0'=x_14^post10, (-x_14^post10+x_14^0 == 0 /\ -b_16^post10+b_16^0 == 0 /\ 1-x_14^0 <= 0 /\ rt_11^0-rt_11^post10 == 0 /\ -st_15^post10+st_15^0 == 0), cost: 1 New rule: l7 -> l8 : b_16^0'=b_16^0, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=x_14^0, (0 == 0 /\ 1-x_14^0 <= 0), cost: 1 propagated equality x_14^post10 = x_14^0 propagated equality b_16^post10 = b_16^0 propagated equality rt_11^post10 = rt_11^0 propagated equality st_15^post10 = st_15^0 Simplified Guard Original rule: l7 -> l8 : b_16^0'=b_16^0, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=x_14^0, (0 == 0 /\ 1-x_14^0 <= 0), cost: 1 New rule: l7 -> l8 : b_16^0'=b_16^0, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=x_14^0, 1-x_14^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l7 -> l8 : b_16^0'=b_16^0, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=x_14^0, 1-x_14^0 <= 0, cost: 1 New rule: l7 -> l8 : 1-x_14^0 <= 0, cost: 1 Propagated Equalities Original rule: l7 -> l8 : b_16^0'=b_16^post11, rt_11^0'=rt_11^post11, st_15^0'=st_15^post11, x_14^0'=x_14^post11, (-rt_11^post11+rt_11^0 == 0 /\ x_14^0-x_14^post11 == 0 /\ 1+x_14^0 <= 0 /\ -st_15^post11+st_15^0 == 0 /\ b_16^0-b_16^post11 == 0), cost: 1 New rule: l7 -> l8 : b_16^0'=b_16^0, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=x_14^0, (0 == 0 /\ 1+x_14^0 <= 0), cost: 1 propagated equality rt_11^post11 = rt_11^0 propagated equality x_14^post11 = x_14^0 propagated equality st_15^post11 = st_15^0 propagated equality b_16^post11 = b_16^0 Simplified Guard Original rule: l7 -> l8 : b_16^0'=b_16^0, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=x_14^0, (0 == 0 /\ 1+x_14^0 <= 0), cost: 1 New rule: l7 -> l8 : b_16^0'=b_16^0, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=x_14^0, 1+x_14^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l7 -> l8 : b_16^0'=b_16^0, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=x_14^0, 1+x_14^0 <= 0, cost: 1 New rule: l7 -> l8 : 1+x_14^0 <= 0, cost: 1 Propagated Equalities Original rule: l8 -> l9 : b_16^0'=b_16^post12, rt_11^0'=rt_11^post12, st_15^0'=st_15^post12, x_14^0'=x_14^post12, (-b_16^post12+b_16^0 == 0 /\ -x_14^post12+x_14^0 == 0 /\ rt_11^0-rt_11^post12 == 0 /\ 2-b_16^0 <= 0 /\ -st_15^post12+st_15^0 == 0), cost: 1 New rule: l8 -> l9 : b_16^0'=b_16^0, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=x_14^0, (0 == 0 /\ 2-b_16^0 <= 0), cost: 1 propagated equality b_16^post12 = b_16^0 propagated equality x_14^post12 = x_14^0 propagated equality rt_11^post12 = rt_11^0 propagated equality st_15^post12 = st_15^0 Simplified Guard Original rule: l8 -> l9 : b_16^0'=b_16^0, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=x_14^0, (0 == 0 /\ 2-b_16^0 <= 0), cost: 1 New rule: l8 -> l9 : b_16^0'=b_16^0, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=x_14^0, 2-b_16^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l8 -> l9 : b_16^0'=b_16^0, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=x_14^0, 2-b_16^0 <= 0, cost: 1 New rule: l8 -> l9 : 2-b_16^0 <= 0, cost: 1 Propagated Equalities Original rule: l8 -> l9 : b_16^0'=b_16^post13, rt_11^0'=rt_11^post13, st_15^0'=st_15^post13, x_14^0'=x_14^post13, (-b_16^post13+b_16^0 == 0 /\ rt_11^0-rt_11^post13 == 0 /\ -x_14^post13+x_14^0 == 0 /\ b_16^0 <= 0 /\ -st_15^post13+st_15^0 == 0), cost: 1 New rule: l8 -> l9 : b_16^0'=b_16^0, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=x_14^0, (0 == 0 /\ b_16^0 <= 0), cost: 1 propagated equality b_16^post13 = b_16^0 propagated equality rt_11^post13 = rt_11^0 propagated equality x_14^post13 = x_14^0 propagated equality st_15^post13 = st_15^0 Simplified Guard Original rule: l8 -> l9 : b_16^0'=b_16^0, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=x_14^0, (0 == 0 /\ b_16^0 <= 0), cost: 1 New rule: l8 -> l9 : b_16^0'=b_16^0, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=x_14^0, b_16^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l8 -> l9 : b_16^0'=b_16^0, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=x_14^0, b_16^0 <= 0, cost: 1 New rule: l8 -> l9 : b_16^0 <= 0, cost: 1 Propagated Equalities Original rule: l9 -> l1 : b_16^0'=b_16^post14, rt_11^0'=rt_11^post14, st_15^0'=st_15^post14, x_14^0'=x_14^post14, (-st_15^post14+st_15^0 == 0 /\ rt_11^0-rt_11^post14 == 0 /\ -1+b_16^post14 == 0 /\ x_14^post14+x_14^1 == 0 /\ -1-x_14^0+x_14^1 == 0), cost: 1 New rule: l9 -> l1 : b_16^0'=1, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=-x_14^1, (0 == 0 /\ -1-x_14^0+x_14^1 == 0), cost: 1 propagated equality st_15^post14 = st_15^0 propagated equality rt_11^post14 = rt_11^0 propagated equality b_16^post14 = 1 propagated equality x_14^post14 = -x_14^1 Propagated Equalities Original rule: l9 -> l1 : b_16^0'=1, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=-x_14^1, (0 == 0 /\ -1-x_14^0+x_14^1 == 0), cost: 1 New rule: l9 -> l1 : b_16^0'=1, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=-1-x_14^0, 0 == 0, cost: 1 propagated equality x_14^1 = 1+x_14^0 Simplified Guard Original rule: l9 -> l1 : b_16^0'=1, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=-1-x_14^0, 0 == 0, cost: 1 New rule: l9 -> l1 : b_16^0'=1, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=-1-x_14^0, T, cost: 1 Removed Trivial Updates Original rule: l9 -> l1 : b_16^0'=1, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=-1-x_14^0, T, cost: 1 New rule: l9 -> l1 : b_16^0'=1, x_14^0'=-1-x_14^0, T, cost: 1 Propagated Equalities Original rule: l3 -> l7 : b_16^0'=b_16^post15, rt_11^0'=rt_11^post15, st_15^0'=st_15^post15, x_14^0'=x_14^post15, (x_14^post15+x_14^0 == 0 /\ -st_15^post15+st_15^0 == 0 /\ -b_16^post15+b_16^0 == 0 /\ rt_11^0-rt_11^post15 == 0), cost: 1 New rule: l3 -> l7 : b_16^0'=b_16^0, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=-x_14^0, 0 == 0, cost: 1 propagated equality x_14^post15 = -x_14^0 propagated equality st_15^post15 = st_15^0 propagated equality b_16^post15 = b_16^0 propagated equality rt_11^post15 = rt_11^0 Simplified Guard Original rule: l3 -> l7 : b_16^0'=b_16^0, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=-x_14^0, 0 == 0, cost: 1 New rule: l3 -> l7 : b_16^0'=b_16^0, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=-x_14^0, T, cost: 1 Removed Trivial Updates Original rule: l3 -> l7 : b_16^0'=b_16^0, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=-x_14^0, T, cost: 1 New rule: l3 -> l7 : x_14^0'=-x_14^0, T, cost: 1 Propagated Equalities Original rule: l10 -> l7 : b_16^0'=b_16^post16, rt_11^0'=rt_11^post16, st_15^0'=st_15^post16, x_14^0'=x_14^post16, (x_14^0+x_14^post16 == 0 /\ -b_16^post16+b_16^0 == 0 /\ -st_15^post16+st_15^0 == 0 /\ -rt_11^post16+rt_11^0 == 0), cost: 1 New rule: l10 -> l7 : b_16^0'=b_16^0, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=-x_14^0, 0 == 0, cost: 1 propagated equality x_14^post16 = -x_14^0 propagated equality b_16^post16 = b_16^0 propagated equality st_15^post16 = st_15^0 propagated equality rt_11^post16 = rt_11^0 Simplified Guard Original rule: l10 -> l7 : b_16^0'=b_16^0, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=-x_14^0, 0 == 0, cost: 1 New rule: l10 -> l7 : b_16^0'=b_16^0, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=-x_14^0, T, cost: 1 Removed Trivial Updates Original rule: l10 -> l7 : b_16^0'=b_16^0, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=-x_14^0, T, cost: 1 New rule: l10 -> l7 : x_14^0'=-x_14^0, T, cost: 1 Propagated Equalities Original rule: l11 -> l1 : b_16^0'=b_16^post1, rt_11^0'=rt_11^post1, st_15^0'=st_15^post1, x_14^0'=x_14^post1, (1-x_14^post17 <= 0 /\ -st_15^post1+st_15^post17 == 0 /\ -x_14^post17+x_14^0 == 0 /\ -st_15^post17+st_15^0 == 0 /\ x_14^post17-x_14^post1 == 0 /\ b_16^0-b_16^post17 == 0 /\ rt_11^post17-rt_11^post1 == 0 /\ rt_11^0-rt_11^post17 == 0 /\ -1+b_16^post1 == 0), cost: 1 New rule: l11 -> l1 : b_16^0'=1, rt_11^0'=rt_11^post17, st_15^0'=st_15^post17, x_14^0'=x_14^post17, (0 == 0 /\ 1-x_14^post17 <= 0 /\ -x_14^post17+x_14^0 == 0 /\ -st_15^post17+st_15^0 == 0 /\ b_16^0-b_16^post17 == 0 /\ rt_11^0-rt_11^post17 == 0), cost: 1 propagated equality st_15^post1 = st_15^post17 propagated equality x_14^post1 = x_14^post17 propagated equality rt_11^post1 = rt_11^post17 propagated equality b_16^post1 = 1 Propagated Equalities Original rule: l11 -> l1 : b_16^0'=1, rt_11^0'=rt_11^post17, st_15^0'=st_15^post17, x_14^0'=x_14^post17, (0 == 0 /\ 1-x_14^post17 <= 0 /\ -x_14^post17+x_14^0 == 0 /\ -st_15^post17+st_15^0 == 0 /\ b_16^0-b_16^post17 == 0 /\ rt_11^0-rt_11^post17 == 0), cost: 1 New rule: l11 -> l1 : b_16^0'=1, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=x_14^0, (0 == 0 /\ 1-x_14^0 <= 0), cost: 1 propagated equality x_14^post17 = x_14^0 propagated equality st_15^post17 = st_15^0 propagated equality b_16^post17 = b_16^0 propagated equality rt_11^post17 = rt_11^0 Simplified Guard Original rule: l11 -> l1 : b_16^0'=1, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=x_14^0, (0 == 0 /\ 1-x_14^0 <= 0), cost: 1 New rule: l11 -> l1 : b_16^0'=1, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=x_14^0, 1-x_14^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l11 -> l1 : b_16^0'=1, rt_11^0'=rt_11^0, st_15^0'=st_15^0, x_14^0'=x_14^0, 1-x_14^0 <= 0, cost: 1 New rule: l11 -> l1 : b_16^0'=1, 1-x_14^0 <= 0, cost: 1 Step with 33 Trace 33[(1-x_14^0 <= 0)] Blocked [{}, {}] Step with 22 Trace 33[(1-x_14^0 <= 0)], 22[(1-x_14^0 <= 0)] Blocked [{}, {21[T]}, {}] Step with 24 Trace 33[(1-x_14^0 <= 0)], 22[(1-x_14^0 <= 0)], 24[(1-b_16^0 <= 0 /\ 1-b_16^0 == 0 /\ -1+b_16^0 <= 0)] Blocked [{}, {21[T]}, {}, {}] Step with 31 Trace 33[(1-x_14^0 <= 0)], 22[(1-x_14^0 <= 0)], 24[(1-b_16^0 <= 0 /\ 1-b_16^0 == 0 /\ -1+b_16^0 <= 0)], 31[T] Blocked [{}, {21[T]}, {}, {}, {}] Step with 25 Trace 33[(1-x_14^0 <= 0)], 22[(1-x_14^0 <= 0)], 24[(1-b_16^0 <= 0 /\ 1-b_16^0 == 0 /\ -1+b_16^0 <= 0)], 31[T], 25[(-x_14^0 <= 0 /\ -x_14^0 == 0 /\ x_14^0 <= 0)] Blocked [{}, {21[T]}, {}, {}, {}, {}] Backtrack Trace 33[(1-x_14^0 <= 0)], 22[(1-x_14^0 <= 0)], 24[(1-b_16^0 <= 0 /\ 1-b_16^0 == 0 /\ -1+b_16^0 <= 0)], 31[T] Blocked [{}, {21[T]}, {}, {}, {25[T]}] Step with 27 Trace 33[(1-x_14^0 <= 0)], 22[(1-x_14^0 <= 0)], 24[(1-b_16^0 <= 0 /\ 1-b_16^0 == 0 /\ -1+b_16^0 <= 0)], 31[T], 27[(1+x_14^0 <= 0)] Blocked [{}, {21[T]}, {}, {}, {25[T], 26[T]}, {}] Step with 29 Trace 33[(1-x_14^0 <= 0)], 22[(1-x_14^0 <= 0)], 24[(1-b_16^0 <= 0 /\ 1-b_16^0 == 0 /\ -1+b_16^0 <= 0)], 31[T], 27[(1+x_14^0 <= 0)], 29[(b_16^0 <= 0)] Blocked [{}, {21[T]}, {}, {}, {25[T], 26[T]}, {28[T]}, {}] Step with 30 Trace 33[(1-x_14^0 <= 0)], 22[(1-x_14^0 <= 0)], 24[(1-b_16^0 <= 0 /\ 1-b_16^0 == 0 /\ -1+b_16^0 <= 0)], 31[T], 27[(1+x_14^0 <= 0)], 29[(b_16^0 <= 0)], 30[T] Blocked [{}, {21[T]}, {}, {}, {25[T], 26[T]}, {28[T]}, {}, {}] Accelerate Start location: l11 Program variables: b_16^0 rt_11^0 st_15^0 x_14^0 21: l1 -> l5 : rt_11^0'=st_15^0, (-x_14^0 <= 0 /\ -x_14^0 == 0 /\ x_14^0 <= 0), cost: 1 22: l1 -> l6 : 1-x_14^0 <= 0, cost: 1 23: l1 -> l6 : 1+x_14^0 <= 0, cost: 1 34: l1 -> l1 : b_16^0'=1, x_14^0'=-2*n+x_14^0, (-1+n >= 0 /\ 1-b_16^0 >= 0 /\ -1+b_16^0 >= 0 /\ -2*n+x_14^0 >= 0 /\ 1-2*n+x_14^0 >= 0), cost: 1 18: l2 -> l4 : 1-x_14^0 <= 0, cost: 1 19: l2 -> l4 : 1+x_14^0 <= 0, cost: 1 20: l4 -> l3 : b_16^0'=0, x_14^0'=-1+x_14^0, (1-b_16^0 <= 0 /\ 1-b_16^0 == 0 /\ -1+b_16^0 <= 0), cost: 1 31: l3 -> l7 : x_14^0'=-x_14^0, T, cost: 1 24: l6 -> l3 : b_16^0'=0, x_14^0'=-1+x_14^0, (1-b_16^0 <= 0 /\ 1-b_16^0 == 0 /\ -1+b_16^0 <= 0), cost: 1 25: l7 -> l5 : rt_11^0'=st_15^0, (-x_14^0 <= 0 /\ -x_14^0 == 0 /\ x_14^0 <= 0), cost: 1 26: l7 -> l8 : 1-x_14^0 <= 0, cost: 1 27: l7 -> l8 : 1+x_14^0 <= 0, cost: 1 28: l8 -> l9 : 2-b_16^0 <= 0, cost: 1 29: l8 -> l9 : b_16^0 <= 0, cost: 1 30: l9 -> l1 : b_16^0'=1, x_14^0'=-1-x_14^0, T, cost: 1 32: l10 -> l7 : x_14^0'=-x_14^0, T, cost: 1 33: l11 -> l1 : b_16^0'=1, 1-x_14^0 <= 0, cost: 1 Loop Acceleration Original rule: l1 -> l1 : b_16^0'=1, x_14^0'=-2+x_14^0, (2-x_14^0 <= 0 /\ 1-x_14^0 <= 0 /\ 1-b_16^0 <= 0 /\ 1-b_16^0 == 0 /\ -1+b_16^0 <= 0), cost: 1 New rule: l1 -> l1 : b_16^0'=1, x_14^0'=-2*n+x_14^0, (-1+n >= 0 /\ 1-b_16^0 >= 0 /\ -1+b_16^0 >= 0 /\ -2*n+x_14^0 >= 0 /\ 1-2*n+x_14^0 >= 0), cost: 1 -1+x_14^0 >= 0 [0]: montonic decrease yields 1-2*n+x_14^0 >= 0 -1+x_14^0 >= 0 [1]: eventual increase yields (-1+x_14^0 >= 0 /\ 2 <= 0) 1-b_16^0 >= 0 [0]: monotonic increase yields 1-b_16^0 >= 0 -1+b_16^0 >= 0 [0]: monotonic increase yields -1+b_16^0 >= 0 -2+x_14^0 >= 0 [0]: montonic decrease yields -2*n+x_14^0 >= 0 -2+x_14^0 >= 0 [1]: eventual increase yields (2 <= 0 /\ -2+x_14^0 >= 0) Replacement map: {-1+x_14^0 >= 0 -> 1-2*n+x_14^0 >= 0, 1-b_16^0 >= 0 -> 1-b_16^0 >= 0, -1+b_16^0 >= 0 -> -1+b_16^0 >= 0, -2+x_14^0 >= 0 -> -2*n+x_14^0 >= 0} Trace 33[(1-x_14^0 <= 0)], 34[(-1+n >= 0 /\ 1-b_16^0 >= 0 /\ -1+b_16^0 >= 0 /\ -2*n+x_14^0 >= 0 /\ 1-2*n+x_14^0 >= 0)] Blocked [{}, {21[T]}, {34[T]}] Step with 21 Trace 33[(1-x_14^0 <= 0)], 34[(-1+n >= 0 /\ 1-b_16^0 >= 0 /\ -1+b_16^0 >= 0 /\ -2*n+x_14^0 >= 0 /\ 1-2*n+x_14^0 >= 0)], 21[(-x_14^0 <= 0 /\ -x_14^0 == 0 /\ x_14^0 <= 0)] Blocked [{}, {21[T]}, {34[T]}, {}] Backtrack Trace 33[(1-x_14^0 <= 0)], 34[(-1+n >= 0 /\ 1-b_16^0 >= 0 /\ -1+b_16^0 >= 0 /\ -2*n+x_14^0 >= 0 /\ 1-2*n+x_14^0 >= 0)] Blocked [{}, {21[T]}, {21[T], 34[T]}] Step with 22 Trace 33[(1-x_14^0 <= 0)], 34[(-1+n >= 0 /\ 1-b_16^0 >= 0 /\ -1+b_16^0 >= 0 /\ -2*n+x_14^0 >= 0 /\ 1-2*n+x_14^0 >= 0)], 22[(1-x_14^0 <= 0)] Blocked [{}, {21[T]}, {21[T], 34[T]}, {}] Step with 24 Trace 33[(1-x_14^0 <= 0)], 34[(-1+n >= 0 /\ 1-b_16^0 >= 0 /\ -1+b_16^0 >= 0 /\ -2*n+x_14^0 >= 0 /\ 1-2*n+x_14^0 >= 0)], 22[(1-x_14^0 <= 0)], 24[(1-b_16^0 <= 0 /\ 1-b_16^0 == 0 /\ -1+b_16^0 <= 0)] Blocked [{}, {21[T]}, {21[T], 34[T]}, {}, {}] Step with 31 Trace 33[(1-x_14^0 <= 0)], 34[(-1+n >= 0 /\ 1-b_16^0 >= 0 /\ -1+b_16^0 >= 0 /\ -2*n+x_14^0 >= 0 /\ 1-2*n+x_14^0 >= 0)], 22[(1-x_14^0 <= 0)], 24[(1-b_16^0 <= 0 /\ 1-b_16^0 == 0 /\ -1+b_16^0 <= 0)], 31[T] Blocked [{}, {21[T]}, {21[T], 34[T]}, {}, {}, {}] Step with 27 Trace 33[(1-x_14^0 <= 0)], 34[(-1+n >= 0 /\ 1-b_16^0 >= 0 /\ -1+b_16^0 >= 0 /\ -2*n+x_14^0 >= 0 /\ 1-2*n+x_14^0 >= 0)], 22[(1-x_14^0 <= 0)], 24[(1-b_16^0 <= 0 /\ 1-b_16^0 == 0 /\ -1+b_16^0 <= 0)], 31[T], 27[(1+x_14^0 <= 0)] Blocked [{}, {21[T]}, {21[T], 34[T]}, {}, {}, {}, {}] Step with 29 Trace 33[(1-x_14^0 <= 0)], 34[(-1+n >= 0 /\ 1-b_16^0 >= 0 /\ -1+b_16^0 >= 0 /\ -2*n+x_14^0 >= 0 /\ 1-2*n+x_14^0 >= 0)], 22[(1-x_14^0 <= 0)], 24[(1-b_16^0 <= 0 /\ 1-b_16^0 == 0 /\ -1+b_16^0 <= 0)], 31[T], 27[(1+x_14^0 <= 0)], 29[(b_16^0 <= 0)] Blocked [{}, {21[T]}, {21[T], 34[T]}, {}, {}, {}, {}, {}] Step with 30 Trace 33[(1-x_14^0 <= 0)], 34[(-1+n >= 0 /\ 1-b_16^0 >= 0 /\ -1+b_16^0 >= 0 /\ -2*n+x_14^0 >= 0 /\ 1-2*n+x_14^0 >= 0)], 22[(1-x_14^0 <= 0)], 24[(1-b_16^0 <= 0 /\ 1-b_16^0 == 0 /\ -1+b_16^0 <= 0)], 31[T], 27[(1+x_14^0 <= 0)], 29[(b_16^0 <= 0)], 30[T] Blocked [{}, {21[T]}, {21[T], 34[T]}, {}, {}, {}, {}, {}, {}] Covered Trace 33[(1-x_14^0 <= 0)], 34[(-1+n >= 0 /\ 1-b_16^0 >= 0 /\ -1+b_16^0 >= 0 /\ -2*n+x_14^0 >= 0 /\ 1-2*n+x_14^0 >= 0)], 22[(1-x_14^0 <= 0)], 24[(1-b_16^0 <= 0 /\ 1-b_16^0 == 0 /\ -1+b_16^0 <= 0)], 31[T], 27[(1+x_14^0 <= 0)], 29[(b_16^0 <= 0)] Blocked [{}, {21[T]}, {21[T], 34[T]}, {}, {}, {}, {}, {30[T]}] Backtrack Trace 33[(1-x_14^0 <= 0)], 34[(-1+n >= 0 /\ 1-b_16^0 >= 0 /\ -1+b_16^0 >= 0 /\ -2*n+x_14^0 >= 0 /\ 1-2*n+x_14^0 >= 0)], 22[(1-x_14^0 <= 0)], 24[(1-b_16^0 <= 0 /\ 1-b_16^0 == 0 /\ -1+b_16^0 <= 0)], 31[T], 27[(1+x_14^0 <= 0)] Blocked [{}, {21[T]}, {21[T], 34[T]}, {}, {}, {}, {29[T]}] Backtrack Trace 33[(1-x_14^0 <= 0)], 34[(-1+n >= 0 /\ 1-b_16^0 >= 0 /\ -1+b_16^0 >= 0 /\ -2*n+x_14^0 >= 0 /\ 1-2*n+x_14^0 >= 0)], 22[(1-x_14^0 <= 0)], 24[(1-b_16^0 <= 0 /\ 1-b_16^0 == 0 /\ -1+b_16^0 <= 0)], 31[T] Blocked [{}, {21[T]}, {21[T], 34[T]}, {}, {}, {27[T]}] Step with 25 Trace 33[(1-x_14^0 <= 0)], 34[(-1+n >= 0 /\ 1-b_16^0 >= 0 /\ -1+b_16^0 >= 0 /\ -2*n+x_14^0 >= 0 /\ 1-2*n+x_14^0 >= 0)], 22[(1-x_14^0 <= 0)], 24[(1-b_16^0 <= 0 /\ 1-b_16^0 == 0 /\ -1+b_16^0 <= 0)], 31[T], 25[(-x_14^0 <= 0 /\ -x_14^0 == 0 /\ x_14^0 <= 0)] Blocked [{}, {21[T]}, {21[T], 34[T]}, {}, {}, {27[T]}, {}] Backtrack Trace 33[(1-x_14^0 <= 0)], 34[(-1+n >= 0 /\ 1-b_16^0 >= 0 /\ -1+b_16^0 >= 0 /\ -2*n+x_14^0 >= 0 /\ 1-2*n+x_14^0 >= 0)], 22[(1-x_14^0 <= 0)], 24[(1-b_16^0 <= 0 /\ 1-b_16^0 == 0 /\ -1+b_16^0 <= 0)], 31[T] Blocked [{}, {21[T]}, {21[T], 34[T]}, {}, {}, {25[T], 27[T]}] Backtrack Trace 33[(1-x_14^0 <= 0)], 34[(-1+n >= 0 /\ 1-b_16^0 >= 0 /\ -1+b_16^0 >= 0 /\ -2*n+x_14^0 >= 0 /\ 1-2*n+x_14^0 >= 0)], 22[(1-x_14^0 <= 0)], 24[(1-b_16^0 <= 0 /\ 1-b_16^0 == 0 /\ -1+b_16^0 <= 0)] Blocked [{}, {21[T]}, {21[T], 34[T]}, {}, {31[T]}] Backtrack Trace 33[(1-x_14^0 <= 0)], 34[(-1+n >= 0 /\ 1-b_16^0 >= 0 /\ -1+b_16^0 >= 0 /\ -2*n+x_14^0 >= 0 /\ 1-2*n+x_14^0 >= 0)], 22[(1-x_14^0 <= 0)] Blocked [{}, {21[T]}, {21[T], 34[T]}, {24[T]}] Backtrack Trace 33[(1-x_14^0 <= 0)], 34[(-1+n >= 0 /\ 1-b_16^0 >= 0 /\ -1+b_16^0 >= 0 /\ -2*n+x_14^0 >= 0 /\ 1-2*n+x_14^0 >= 0)] Blocked [{}, {21[T]}, {21[T], 22[T], 34[T]}] Backtrack Trace 33[(1-x_14^0 <= 0)] Blocked [{}, {21[T], 34[T]}] Step with 22 Trace 33[(1-x_14^0 <= 0)], 22[(1-x_14^0 <= 0)] Blocked [{}, {21[T], 34[T]}, {}] Step with 24 Trace 33[(1-x_14^0 <= 0)], 22[(1-x_14^0 <= 0)], 24[(1-b_16^0 <= 0 /\ 1-b_16^0 == 0 /\ -1+b_16^0 <= 0)] Blocked [{}, {21[T], 34[T]}, {}, {}] Step with 31 Trace 33[(1-x_14^0 <= 0)], 22[(1-x_14^0 <= 0)], 24[(1-b_16^0 <= 0 /\ 1-b_16^0 == 0 /\ -1+b_16^0 <= 0)], 31[T] Blocked [{}, {21[T], 34[T]}, {}, {}, {}] Step with 25 Trace 33[(1-x_14^0 <= 0)], 22[(1-x_14^0 <= 0)], 24[(1-b_16^0 <= 0 /\ 1-b_16^0 == 0 /\ -1+b_16^0 <= 0)], 31[T], 25[(-x_14^0 <= 0 /\ -x_14^0 == 0 /\ x_14^0 <= 0)] Blocked [{}, {21[T], 34[T]}, {}, {}, {}, {}] Backtrack Trace 33[(1-x_14^0 <= 0)], 22[(1-x_14^0 <= 0)], 24[(1-b_16^0 <= 0 /\ 1-b_16^0 == 0 /\ -1+b_16^0 <= 0)], 31[T] Blocked [{}, {21[T], 34[T]}, {}, {}, {25[T]}] Step with 27 Trace 33[(1-x_14^0 <= 0)], 22[(1-x_14^0 <= 0)], 24[(1-b_16^0 <= 0 /\ 1-b_16^0 == 0 /\ -1+b_16^0 <= 0)], 31[T], 27[(1+x_14^0 <= 0)] Blocked [{}, {21[T], 34[T]}, {}, {}, {25[T], 26[T]}, {}] Step with 29 Trace 33[(1-x_14^0 <= 0)], 22[(1-x_14^0 <= 0)], 24[(1-b_16^0 <= 0 /\ 1-b_16^0 == 0 /\ -1+b_16^0 <= 0)], 31[T], 27[(1+x_14^0 <= 0)], 29[(b_16^0 <= 0)] Blocked [{}, {21[T], 34[T]}, {}, {}, {25[T], 26[T]}, {}, {}] Step with 30 Trace 33[(1-x_14^0 <= 0)], 22[(1-x_14^0 <= 0)], 24[(1-b_16^0 <= 0 /\ 1-b_16^0 == 0 /\ -1+b_16^0 <= 0)], 31[T], 27[(1+x_14^0 <= 0)], 29[(b_16^0 <= 0)], 30[T] Blocked [{}, {21[T], 34[T]}, {}, {}, {25[T], 26[T]}, {}, {}, {}] Covered Trace 33[(1-x_14^0 <= 0)], 22[(1-x_14^0 <= 0)], 24[(1-b_16^0 <= 0 /\ 1-b_16^0 == 0 /\ -1+b_16^0 <= 0)], 31[T], 27[(1+x_14^0 <= 0)], 29[(b_16^0 <= 0)] Blocked [{}, {21[T], 34[T]}, {}, {}, {25[T], 26[T]}, {}, {30[T]}] Backtrack Trace 33[(1-x_14^0 <= 0)], 22[(1-x_14^0 <= 0)], 24[(1-b_16^0 <= 0 /\ 1-b_16^0 == 0 /\ -1+b_16^0 <= 0)], 31[T], 27[(1+x_14^0 <= 0)] Blocked [{}, {21[T], 34[T]}, {}, {}, {25[T], 26[T]}, {29[T]}] Backtrack Trace 33[(1-x_14^0 <= 0)], 22[(1-x_14^0 <= 0)], 24[(1-b_16^0 <= 0 /\ 1-b_16^0 == 0 /\ -1+b_16^0 <= 0)], 31[T] Blocked [{}, {21[T], 34[T]}, {}, {}, {25[T], 26[T], 27[T]}] Backtrack Trace 33[(1-x_14^0 <= 0)], 22[(1-x_14^0 <= 0)], 24[(1-b_16^0 <= 0 /\ 1-b_16^0 == 0 /\ -1+b_16^0 <= 0)] Blocked [{}, {21[T], 34[T]}, {}, {31[T]}] Backtrack Trace 33[(1-x_14^0 <= 0)], 22[(1-x_14^0 <= 0)] Blocked [{}, {21[T], 34[T]}, {24[T]}] Backtrack Trace 33[(1-x_14^0 <= 0)] Blocked [{}, {21[T], 22[T], 34[T]}] Backtrack Trace Blocked [{33[T]}] Accept unknown Build SHA: a05f16bf13df659c382799650051f91bf6828c7b