unknown Initial ITS Start location: l6 Program variables: result_11^0 temp0_14^0 x_13^0 x_27^0 x_32^0 y_16^0 y_28^0 y_33^0 0: l0 -> l1 : result_11^0'=result_11^post1, temp0_14^0'=temp0_14^post1, x_13^0'=x_13^post1, x_27^0'=x_27^post1, x_32^0'=x_32^post1, y_16^0'=y_16^post1, y_28^0'=y_28^post1, y_33^0'=y_33^post1, (0 == 0 /\ -y_33^post1+y_33^0 == 0 /\ x_32^0-x_32^post1 == 0 /\ x_27^0-x_27^post1 == 0 /\ -result_11^post1+result_11^0 == 0 /\ -temp0_14^post1+temp0_14^0 == 0 /\ y_28^0-y_28^post1 == 0), cost: 1 1: l1 -> l2 : result_11^0'=result_11^post2, temp0_14^0'=temp0_14^post2, x_13^0'=x_13^post2, x_27^0'=x_27^post2, x_32^0'=x_32^post2, y_16^0'=y_16^post2, y_28^0'=y_28^post2, y_33^0'=y_33^post2, (0 == 0 /\ 1-x_13^0 <= 0 /\ x_13^0-x_13^post2 == 0 /\ result_11^0-result_11^post2 == 0 /\ -x_27^post2+x_27^0 == 0 /\ -y_28^post2+y_28^0 == 0 /\ x_32^0-x_32^post2 == 0 /\ -temp0_14^post2+temp0_14^0 == 0 /\ 1-y_16^post2 <= 0 /\ y_33^0-y_33^post2 == 0), cost: 1 2: l1 -> l3 : result_11^0'=result_11^post3, temp0_14^0'=temp0_14^post3, x_13^0'=x_13^post3, x_27^0'=x_27^post3, x_32^0'=x_32^post3, y_16^0'=y_16^post3, y_28^0'=y_28^post3, y_33^0'=y_33^post3, (-x_32^post3+x_32^0 == 0 /\ x_13^0 <= 0 /\ -temp0_14^post3+temp0_14^0 == 0 /\ -y_28^post3+y_28^0 == 0 /\ -y_16^post3+y_16^0 == 0 /\ -y_33^post3+y_33^0 == 0 /\ result_11^post3-temp0_14^0 == 0 /\ x_27^0-x_27^post3 == 0 /\ x_13^0-x_13^post3 == 0), cost: 1 4: l2 -> l1 : result_11^0'=result_11^post5, temp0_14^0'=temp0_14^post5, x_13^0'=x_13^post5, x_27^0'=x_27^post5, x_32^0'=x_32^post5, y_16^0'=y_16^post5, y_28^0'=y_28^post5, y_33^0'=y_33^post5, (-temp0_14^post5+temp0_14^0 == 0 /\ x_13^0-x_13^post5 == 0 /\ y_16^0-y_16^post5 == 0 /\ y_16^0 <= 0 /\ result_11^0-result_11^post5 == 0 /\ x_32^0-x_32^post5 == 0 /\ -y_33^post5+y_33^0 == 0 /\ x_27^0-x_27^post5 == 0 /\ y_28^0-y_28^post5 == 0), cost: 1 5: l2 -> l5 : result_11^0'=result_11^post6, temp0_14^0'=temp0_14^post6, x_13^0'=x_13^post6, x_27^0'=x_27^post6, x_32^0'=x_32^post6, y_16^0'=y_16^post6, y_28^0'=y_28^post6, y_33^0'=y_33^post6, (0 == 0 /\ -1-x_13^post6+x_32^post6 <= 0 /\ -1-y_16^post6+y_33^post6 <= 0 /\ -temp0_14^post6+temp0_14^0 == 0 /\ 1+x_13^post6-x_13^0 == 0 /\ -x_27^post6+x_27^0 == 0 /\ result_11^0-result_11^post6 == 0 /\ 1+x_13^post6-x_32^post6 <= 0 /\ 1+y_16^post6-y_33^post6 <= 0 /\ 1+y_16^post6-y_16^0 == 0 /\ 1-y_33^post6 <= 0 /\ 1-y_16^0 <= 0 /\ -y_28^post6+y_28^0 == 0), cost: 1 3: l4 -> l2 : result_11^0'=result_11^post4, temp0_14^0'=temp0_14^post4, x_13^0'=x_13^post4, x_27^0'=x_27^post4, x_32^0'=x_32^post4, y_16^0'=y_16^post4, y_28^0'=y_28^post4, y_33^0'=y_33^post4, (0 == 0 /\ -1+x_27^post4-x_13^post4 <= 0 /\ 1-y_16^0+y_16^post4 == 0 /\ -temp0_14^post4+temp0_14^0 == 0 /\ -1+y_28^post4-y_16^post4 <= 0 /\ 1-x_27^post4 <= 0 /\ 1-y_28^post4 <= 0 /\ x_32^0-x_32^post4 == 0 /\ 1-x_13^0+x_13^post4 == 0 /\ 1-x_27^post4+x_13^post4 <= 0 /\ 1-y_16^0 <= 0 /\ y_33^0-y_33^post4 == 0 /\ result_11^0-result_11^post4 == 0 /\ 1-y_28^post4+y_16^post4 <= 0), cost: 1 6: l5 -> l2 : result_11^0'=result_11^post7, temp0_14^0'=temp0_14^post7, x_13^0'=x_13^post7, x_27^0'=x_27^post7, x_32^0'=x_32^post7, y_16^0'=y_16^post7, y_28^0'=y_28^post7, y_33^0'=y_33^post7, (x_32^0-x_32^post7 == 0 /\ -result_11^post7+result_11^0 == 0 /\ -y_33^post7+y_33^0 == 0 /\ -y_28^post7+y_28^0 == 0 /\ x_13^0-x_13^post7 == 0 /\ -x_27^post7+x_27^0 == 0 /\ y_16^0-y_16^post7 == 0 /\ -temp0_14^post7+temp0_14^0 == 0), cost: 1 7: l6 -> l0 : result_11^0'=result_11^post8, temp0_14^0'=temp0_14^post8, x_13^0'=x_13^post8, x_27^0'=x_27^post8, x_32^0'=x_32^post8, y_16^0'=y_16^post8, y_28^0'=y_28^post8, y_33^0'=y_33^post8, (y_33^0-y_33^post8 == 0 /\ result_11^0-result_11^post8 == 0 /\ -y_28^post8+y_28^0 == 0 /\ temp0_14^0-temp0_14^post8 == 0 /\ x_27^0-x_27^post8 == 0 /\ -x_32^post8+x_32^0 == 0 /\ x_13^0-x_13^post8 == 0 /\ -y_16^post8+y_16^0 == 0), cost: 1 Chained Linear Paths Start location: l6 Program variables: result_11^0 temp0_14^0 x_13^0 x_27^0 x_32^0 y_16^0 y_28^0 y_33^0 1: l1 -> l2 : result_11^0'=result_11^post2, temp0_14^0'=temp0_14^post2, x_13^0'=x_13^post2, x_27^0'=x_27^post2, x_32^0'=x_32^post2, y_16^0'=y_16^post2, y_28^0'=y_28^post2, y_33^0'=y_33^post2, (0 == 0 /\ 1-x_13^0 <= 0 /\ x_13^0-x_13^post2 == 0 /\ result_11^0-result_11^post2 == 0 /\ -x_27^post2+x_27^0 == 0 /\ -y_28^post2+y_28^0 == 0 /\ x_32^0-x_32^post2 == 0 /\ -temp0_14^post2+temp0_14^0 == 0 /\ 1-y_16^post2 <= 0 /\ y_33^0-y_33^post2 == 0), cost: 1 2: l1 -> l3 : result_11^0'=result_11^post3, temp0_14^0'=temp0_14^post3, x_13^0'=x_13^post3, x_27^0'=x_27^post3, x_32^0'=x_32^post3, y_16^0'=y_16^post3, y_28^0'=y_28^post3, y_33^0'=y_33^post3, (-x_32^post3+x_32^0 == 0 /\ x_13^0 <= 0 /\ -temp0_14^post3+temp0_14^0 == 0 /\ -y_28^post3+y_28^0 == 0 /\ -y_16^post3+y_16^0 == 0 /\ -y_33^post3+y_33^0 == 0 /\ result_11^post3-temp0_14^0 == 0 /\ x_27^0-x_27^post3 == 0 /\ x_13^0-x_13^post3 == 0), cost: 1 4: l2 -> l1 : result_11^0'=result_11^post5, temp0_14^0'=temp0_14^post5, x_13^0'=x_13^post5, x_27^0'=x_27^post5, x_32^0'=x_32^post5, y_16^0'=y_16^post5, y_28^0'=y_28^post5, y_33^0'=y_33^post5, (-temp0_14^post5+temp0_14^0 == 0 /\ x_13^0-x_13^post5 == 0 /\ y_16^0-y_16^post5 == 0 /\ y_16^0 <= 0 /\ result_11^0-result_11^post5 == 0 /\ x_32^0-x_32^post5 == 0 /\ -y_33^post5+y_33^0 == 0 /\ x_27^0-x_27^post5 == 0 /\ y_28^0-y_28^post5 == 0), cost: 1 9: l2 -> l2 : result_11^0'=result_11^post7, temp0_14^0'=temp0_14^post7, x_13^0'=x_13^post7, x_27^0'=x_27^post7, x_32^0'=x_32^post7, y_16^0'=y_16^post7, y_28^0'=y_28^post7, y_33^0'=y_33^post7, (0 == 0 /\ y_16^post6-y_16^post7 == 0 /\ -x_27^post7+x_27^post6 == 0 /\ -x_32^post7+x_32^post6 == 0 /\ -1-x_13^post6+x_32^post6 <= 0 /\ -1-y_16^post6+y_33^post6 <= 0 /\ -temp0_14^post6+temp0_14^0 == 0 /\ -y_28^post7+y_28^post6 == 0 /\ -result_11^post7+result_11^post6 == 0 /\ -temp0_14^post7+temp0_14^post6 == 0 /\ 1+x_13^post6-x_13^0 == 0 /\ -x_27^post6+x_27^0 == 0 /\ result_11^0-result_11^post6 == 0 /\ 1+x_13^post6-x_32^post6 <= 0 /\ -y_33^post7+y_33^post6 == 0 /\ 1+y_16^post6-y_33^post6 <= 0 /\ 1+y_16^post6-y_16^0 == 0 /\ 1-y_33^post6 <= 0 /\ x_13^post6-x_13^post7 == 0 /\ 1-y_16^0 <= 0 /\ -y_28^post6+y_28^0 == 0), cost: 1 3: l4 -> l2 : result_11^0'=result_11^post4, temp0_14^0'=temp0_14^post4, x_13^0'=x_13^post4, x_27^0'=x_27^post4, x_32^0'=x_32^post4, y_16^0'=y_16^post4, y_28^0'=y_28^post4, y_33^0'=y_33^post4, (0 == 0 /\ -1+x_27^post4-x_13^post4 <= 0 /\ 1-y_16^0+y_16^post4 == 0 /\ -temp0_14^post4+temp0_14^0 == 0 /\ -1+y_28^post4-y_16^post4 <= 0 /\ 1-x_27^post4 <= 0 /\ 1-y_28^post4 <= 0 /\ x_32^0-x_32^post4 == 0 /\ 1-x_13^0+x_13^post4 == 0 /\ 1-x_27^post4+x_13^post4 <= 0 /\ 1-y_16^0 <= 0 /\ y_33^0-y_33^post4 == 0 /\ result_11^0-result_11^post4 == 0 /\ 1-y_28^post4+y_16^post4 <= 0), cost: 1 8: l6 -> l1 : result_11^0'=result_11^post1, temp0_14^0'=temp0_14^post1, x_13^0'=x_13^post1, x_27^0'=x_27^post1, x_32^0'=x_32^post1, y_16^0'=y_16^post1, y_28^0'=y_28^post1, y_33^0'=y_33^post1, (0 == 0 /\ y_33^0-y_33^post8 == 0 /\ -y_33^post1+y_33^post8 == 0 /\ result_11^0-result_11^post8 == 0 /\ y_28^post8-y_28^post1 == 0 /\ -y_28^post8+y_28^0 == 0 /\ temp0_14^0-temp0_14^post8 == 0 /\ x_27^0-x_27^post8 == 0 /\ -result_11^post1+result_11^post8 == 0 /\ -x_32^post8+x_32^0 == 0 /\ x_13^0-x_13^post8 == 0 /\ -y_16^post8+y_16^0 == 0 /\ -temp0_14^post1+temp0_14^post8 == 0 /\ x_27^post8-x_27^post1 == 0 /\ x_32^post8-x_32^post1 == 0), cost: 1 Eliminating location l0 by chaining: Applied chaining First rule: l6 -> l0 : result_11^0'=result_11^post8, temp0_14^0'=temp0_14^post8, x_13^0'=x_13^post8, x_27^0'=x_27^post8, x_32^0'=x_32^post8, y_16^0'=y_16^post8, y_28^0'=y_28^post8, y_33^0'=y_33^post8, (y_33^0-y_33^post8 == 0 /\ result_11^0-result_11^post8 == 0 /\ -y_28^post8+y_28^0 == 0 /\ temp0_14^0-temp0_14^post8 == 0 /\ x_27^0-x_27^post8 == 0 /\ -x_32^post8+x_32^0 == 0 /\ x_13^0-x_13^post8 == 0 /\ -y_16^post8+y_16^0 == 0), cost: 1 Second rule: l0 -> l1 : result_11^0'=result_11^post1, temp0_14^0'=temp0_14^post1, x_13^0'=x_13^post1, x_27^0'=x_27^post1, x_32^0'=x_32^post1, y_16^0'=y_16^post1, y_28^0'=y_28^post1, y_33^0'=y_33^post1, (0 == 0 /\ -y_33^post1+y_33^0 == 0 /\ x_32^0-x_32^post1 == 0 /\ x_27^0-x_27^post1 == 0 /\ -result_11^post1+result_11^0 == 0 /\ -temp0_14^post1+temp0_14^0 == 0 /\ y_28^0-y_28^post1 == 0), cost: 1 New rule: l6 -> l1 : result_11^0'=result_11^post1, temp0_14^0'=temp0_14^post1, x_13^0'=x_13^post1, x_27^0'=x_27^post1, x_32^0'=x_32^post1, y_16^0'=y_16^post1, y_28^0'=y_28^post1, y_33^0'=y_33^post1, (0 == 0 /\ y_33^0-y_33^post8 == 0 /\ -y_33^post1+y_33^post8 == 0 /\ result_11^0-result_11^post8 == 0 /\ y_28^post8-y_28^post1 == 0 /\ -y_28^post8+y_28^0 == 0 /\ temp0_14^0-temp0_14^post8 == 0 /\ x_27^0-x_27^post8 == 0 /\ -result_11^post1+result_11^post8 == 0 /\ -x_32^post8+x_32^0 == 0 /\ x_13^0-x_13^post8 == 0 /\ -y_16^post8+y_16^0 == 0 /\ -temp0_14^post1+temp0_14^post8 == 0 /\ x_27^post8-x_27^post1 == 0 /\ x_32^post8-x_32^post1 == 0), cost: 1 Applied deletion Removed the following rules: 0 7 Eliminating location l5 by chaining: Applied chaining First rule: l2 -> l5 : result_11^0'=result_11^post6, temp0_14^0'=temp0_14^post6, x_13^0'=x_13^post6, x_27^0'=x_27^post6, x_32^0'=x_32^post6, y_16^0'=y_16^post6, y_28^0'=y_28^post6, y_33^0'=y_33^post6, (0 == 0 /\ -1-x_13^post6+x_32^post6 <= 0 /\ -1-y_16^post6+y_33^post6 <= 0 /\ -temp0_14^post6+temp0_14^0 == 0 /\ 1+x_13^post6-x_13^0 == 0 /\ -x_27^post6+x_27^0 == 0 /\ result_11^0-result_11^post6 == 0 /\ 1+x_13^post6-x_32^post6 <= 0 /\ 1+y_16^post6-y_33^post6 <= 0 /\ 1+y_16^post6-y_16^0 == 0 /\ 1-y_33^post6 <= 0 /\ 1-y_16^0 <= 0 /\ -y_28^post6+y_28^0 == 0), cost: 1 Second rule: l5 -> l2 : result_11^0'=result_11^post7, temp0_14^0'=temp0_14^post7, x_13^0'=x_13^post7, x_27^0'=x_27^post7, x_32^0'=x_32^post7, y_16^0'=y_16^post7, y_28^0'=y_28^post7, y_33^0'=y_33^post7, (x_32^0-x_32^post7 == 0 /\ -result_11^post7+result_11^0 == 0 /\ -y_33^post7+y_33^0 == 0 /\ -y_28^post7+y_28^0 == 0 /\ x_13^0-x_13^post7 == 0 /\ -x_27^post7+x_27^0 == 0 /\ y_16^0-y_16^post7 == 0 /\ -temp0_14^post7+temp0_14^0 == 0), cost: 1 New rule: l2 -> l2 : result_11^0'=result_11^post7, temp0_14^0'=temp0_14^post7, x_13^0'=x_13^post7, x_27^0'=x_27^post7, x_32^0'=x_32^post7, y_16^0'=y_16^post7, y_28^0'=y_28^post7, y_33^0'=y_33^post7, (0 == 0 /\ y_16^post6-y_16^post7 == 0 /\ -x_27^post7+x_27^post6 == 0 /\ -x_32^post7+x_32^post6 == 0 /\ -1-x_13^post6+x_32^post6 <= 0 /\ -1-y_16^post6+y_33^post6 <= 0 /\ -temp0_14^post6+temp0_14^0 == 0 /\ -y_28^post7+y_28^post6 == 0 /\ -result_11^post7+result_11^post6 == 0 /\ -temp0_14^post7+temp0_14^post6 == 0 /\ 1+x_13^post6-x_13^0 == 0 /\ -x_27^post6+x_27^0 == 0 /\ result_11^0-result_11^post6 == 0 /\ 1+x_13^post6-x_32^post6 <= 0 /\ -y_33^post7+y_33^post6 == 0 /\ 1+y_16^post6-y_33^post6 <= 0 /\ 1+y_16^post6-y_16^0 == 0 /\ 1-y_33^post6 <= 0 /\ x_13^post6-x_13^post7 == 0 /\ 1-y_16^0 <= 0 /\ -y_28^post6+y_28^0 == 0), cost: 1 Applied deletion Removed the following rules: 5 6 Simplified Transitions Start location: l6 Program variables: result_11^0 temp0_14^0 x_13^0 x_27^0 x_32^0 y_16^0 y_28^0 y_33^0 10: l1 -> l2 : y_16^0'=y_16^post2, (1-x_13^0 <= 0 /\ 1-y_16^post2 <= 0), cost: 1 11: l1 -> l3 : result_11^0'=temp0_14^0, x_13^0 <= 0, cost: 1 13: l2 -> l1 : y_16^0 <= 0, cost: 1 15: l2 -> l2 : x_13^0'=-1+x_13^0, x_32^0'=x_13^0, y_16^0'=-1+y_16^0, y_33^0'=y_16^0, 1-y_16^0 <= 0, cost: 1 12: l4 -> l2 : x_13^0'=-1+x_13^0, x_27^0'=x_13^0, y_16^0'=-1+y_16^0, y_28^0'=y_16^0, (1-x_13^0 <= 0 /\ 1-y_16^0 <= 0), cost: 1 14: l6 -> l1 : x_13^0'=x_13^post1, y_16^0'=y_16^post1, T, cost: 1 Propagated Equalities Original rule: l1 -> l2 : result_11^0'=result_11^post2, temp0_14^0'=temp0_14^post2, x_13^0'=x_13^post2, x_27^0'=x_27^post2, x_32^0'=x_32^post2, y_16^0'=y_16^post2, y_28^0'=y_28^post2, y_33^0'=y_33^post2, (0 == 0 /\ 1-x_13^0 <= 0 /\ x_13^0-x_13^post2 == 0 /\ result_11^0-result_11^post2 == 0 /\ -x_27^post2+x_27^0 == 0 /\ -y_28^post2+y_28^0 == 0 /\ x_32^0-x_32^post2 == 0 /\ -temp0_14^post2+temp0_14^0 == 0 /\ 1-y_16^post2 <= 0 /\ y_33^0-y_33^post2 == 0), cost: 1 New rule: l1 -> l2 : result_11^0'=result_11^0, temp0_14^0'=temp0_14^0, x_13^0'=x_13^0, x_27^0'=x_27^0, x_32^0'=x_32^0, y_16^0'=y_16^post2, y_28^0'=y_28^0, y_33^0'=y_33^0, (0 == 0 /\ 1-x_13^0 <= 0 /\ 1-y_16^post2 <= 0), cost: 1 propagated equality x_13^post2 = x_13^0 propagated equality result_11^post2 = result_11^0 propagated equality x_27^post2 = x_27^0 propagated equality y_28^post2 = y_28^0 propagated equality x_32^post2 = x_32^0 propagated equality temp0_14^post2 = temp0_14^0 propagated equality y_33^post2 = y_33^0 Simplified Guard Original rule: l1 -> l2 : result_11^0'=result_11^0, temp0_14^0'=temp0_14^0, x_13^0'=x_13^0, x_27^0'=x_27^0, x_32^0'=x_32^0, y_16^0'=y_16^post2, y_28^0'=y_28^0, y_33^0'=y_33^0, (0 == 0 /\ 1-x_13^0 <= 0 /\ 1-y_16^post2 <= 0), cost: 1 New rule: l1 -> l2 : result_11^0'=result_11^0, temp0_14^0'=temp0_14^0, x_13^0'=x_13^0, x_27^0'=x_27^0, x_32^0'=x_32^0, y_16^0'=y_16^post2, y_28^0'=y_28^0, y_33^0'=y_33^0, (1-x_13^0 <= 0 /\ 1-y_16^post2 <= 0), cost: 1 Removed Trivial Updates Original rule: l1 -> l2 : result_11^0'=result_11^0, temp0_14^0'=temp0_14^0, x_13^0'=x_13^0, x_27^0'=x_27^0, x_32^0'=x_32^0, y_16^0'=y_16^post2, y_28^0'=y_28^0, y_33^0'=y_33^0, (1-x_13^0 <= 0 /\ 1-y_16^post2 <= 0), cost: 1 New rule: l1 -> l2 : y_16^0'=y_16^post2, (1-x_13^0 <= 0 /\ 1-y_16^post2 <= 0), cost: 1 Propagated Equalities Original rule: l1 -> l3 : result_11^0'=result_11^post3, temp0_14^0'=temp0_14^post3, x_13^0'=x_13^post3, x_27^0'=x_27^post3, x_32^0'=x_32^post3, y_16^0'=y_16^post3, y_28^0'=y_28^post3, y_33^0'=y_33^post3, (-x_32^post3+x_32^0 == 0 /\ x_13^0 <= 0 /\ -temp0_14^post3+temp0_14^0 == 0 /\ -y_28^post3+y_28^0 == 0 /\ -y_16^post3+y_16^0 == 0 /\ -y_33^post3+y_33^0 == 0 /\ result_11^post3-temp0_14^0 == 0 /\ x_27^0-x_27^post3 == 0 /\ x_13^0-x_13^post3 == 0), cost: 1 New rule: l1 -> l3 : result_11^0'=temp0_14^0, temp0_14^0'=temp0_14^0, x_13^0'=x_13^0, x_27^0'=x_27^0, x_32^0'=x_32^0, y_16^0'=y_16^0, y_28^0'=y_28^0, y_33^0'=y_33^0, (0 == 0 /\ x_13^0 <= 0), cost: 1 propagated equality x_32^post3 = x_32^0 propagated equality temp0_14^post3 = temp0_14^0 propagated equality y_28^post3 = y_28^0 propagated equality y_16^post3 = y_16^0 propagated equality y_33^post3 = y_33^0 propagated equality result_11^post3 = temp0_14^0 propagated equality x_27^post3 = x_27^0 propagated equality x_13^post3 = x_13^0 Simplified Guard Original rule: l1 -> l3 : result_11^0'=temp0_14^0, temp0_14^0'=temp0_14^0, x_13^0'=x_13^0, x_27^0'=x_27^0, x_32^0'=x_32^0, y_16^0'=y_16^0, y_28^0'=y_28^0, y_33^0'=y_33^0, (0 == 0 /\ x_13^0 <= 0), cost: 1 New rule: l1 -> l3 : result_11^0'=temp0_14^0, temp0_14^0'=temp0_14^0, x_13^0'=x_13^0, x_27^0'=x_27^0, x_32^0'=x_32^0, y_16^0'=y_16^0, y_28^0'=y_28^0, y_33^0'=y_33^0, x_13^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l1 -> l3 : result_11^0'=temp0_14^0, temp0_14^0'=temp0_14^0, x_13^0'=x_13^0, x_27^0'=x_27^0, x_32^0'=x_32^0, y_16^0'=y_16^0, y_28^0'=y_28^0, y_33^0'=y_33^0, x_13^0 <= 0, cost: 1 New rule: l1 -> l3 : result_11^0'=temp0_14^0, x_13^0 <= 0, cost: 1 made implied equalities explicit Original rule: l4 -> l2 : result_11^0'=result_11^post4, temp0_14^0'=temp0_14^post4, x_13^0'=x_13^post4, x_27^0'=x_27^post4, x_32^0'=x_32^post4, y_16^0'=y_16^post4, y_28^0'=y_28^post4, y_33^0'=y_33^post4, (0 == 0 /\ -1+x_27^post4-x_13^post4 <= 0 /\ 1-y_16^0+y_16^post4 == 0 /\ -temp0_14^post4+temp0_14^0 == 0 /\ -1+y_28^post4-y_16^post4 <= 0 /\ 1-x_27^post4 <= 0 /\ 1-y_28^post4 <= 0 /\ x_32^0-x_32^post4 == 0 /\ 1-x_13^0+x_13^post4 == 0 /\ 1-x_27^post4+x_13^post4 <= 0 /\ 1-y_16^0 <= 0 /\ y_33^0-y_33^post4 == 0 /\ result_11^0-result_11^post4 == 0 /\ 1-y_28^post4+y_16^post4 <= 0), cost: 1 New rule: l4 -> l2 : result_11^0'=result_11^post4, temp0_14^0'=temp0_14^post4, x_13^0'=x_13^post4, x_27^0'=x_27^post4, x_32^0'=x_32^post4, y_16^0'=y_16^post4, y_28^0'=y_28^post4, y_33^0'=y_33^post4, (0 == 0 /\ -1+x_27^post4-x_13^post4 <= 0 /\ -1+x_27^post4-x_13^post4 == 0 /\ 1-y_16^0+y_16^post4 == 0 /\ -temp0_14^post4+temp0_14^0 == 0 /\ -1+y_28^post4-y_16^post4 <= 0 /\ -1+y_28^post4-y_16^post4 == 0 /\ 1-x_27^post4 <= 0 /\ 1-y_28^post4 <= 0 /\ x_32^0-x_32^post4 == 0 /\ 1-x_13^0+x_13^post4 == 0 /\ 1-x_27^post4+x_13^post4 <= 0 /\ 1-y_16^0 <= 0 /\ y_33^0-y_33^post4 == 0 /\ result_11^0-result_11^post4 == 0 /\ 1-y_28^post4+y_16^post4 <= 0), cost: 1 Propagated Equalities Original rule: l4 -> l2 : result_11^0'=result_11^post4, temp0_14^0'=temp0_14^post4, x_13^0'=x_13^post4, x_27^0'=x_27^post4, x_32^0'=x_32^post4, y_16^0'=y_16^post4, y_28^0'=y_28^post4, y_33^0'=y_33^post4, (0 == 0 /\ -1+x_27^post4-x_13^post4 <= 0 /\ -1+x_27^post4-x_13^post4 == 0 /\ 1-y_16^0+y_16^post4 == 0 /\ -temp0_14^post4+temp0_14^0 == 0 /\ -1+y_28^post4-y_16^post4 <= 0 /\ -1+y_28^post4-y_16^post4 == 0 /\ 1-x_27^post4 <= 0 /\ 1-y_28^post4 <= 0 /\ x_32^0-x_32^post4 == 0 /\ 1-x_13^0+x_13^post4 == 0 /\ 1-x_27^post4+x_13^post4 <= 0 /\ 1-y_16^0 <= 0 /\ y_33^0-y_33^post4 == 0 /\ result_11^0-result_11^post4 == 0 /\ 1-y_28^post4+y_16^post4 <= 0), cost: 1 New rule: l4 -> l2 : result_11^0'=result_11^0, temp0_14^0'=temp0_14^0, x_13^0'=-1+x_13^0, x_27^0'=x_13^0, x_32^0'=x_32^0, y_16^0'=-1+y_16^0, y_28^0'=y_16^0, y_33^0'=y_33^0, (0 <= 0 /\ 0 == 0 /\ 1-x_13^0 <= 0 /\ 1-y_16^0 <= 0), cost: 1 propagated equality x_13^post4 = -1+x_27^post4 propagated equality y_16^post4 = -1+y_16^0 propagated equality temp0_14^post4 = temp0_14^0 propagated equality y_28^post4 = y_16^0 propagated equality x_32^post4 = x_32^0 propagated equality x_27^post4 = x_13^0 propagated equality y_33^post4 = y_33^0 propagated equality result_11^post4 = result_11^0 Simplified Guard Original rule: l4 -> l2 : result_11^0'=result_11^0, temp0_14^0'=temp0_14^0, x_13^0'=-1+x_13^0, x_27^0'=x_13^0, x_32^0'=x_32^0, y_16^0'=-1+y_16^0, y_28^0'=y_16^0, y_33^0'=y_33^0, (0 <= 0 /\ 0 == 0 /\ 1-x_13^0 <= 0 /\ 1-y_16^0 <= 0), cost: 1 New rule: l4 -> l2 : result_11^0'=result_11^0, temp0_14^0'=temp0_14^0, x_13^0'=-1+x_13^0, x_27^0'=x_13^0, x_32^0'=x_32^0, y_16^0'=-1+y_16^0, y_28^0'=y_16^0, y_33^0'=y_33^0, (1-x_13^0 <= 0 /\ 1-y_16^0 <= 0), cost: 1 Removed Trivial Updates Original rule: l4 -> l2 : result_11^0'=result_11^0, temp0_14^0'=temp0_14^0, x_13^0'=-1+x_13^0, x_27^0'=x_13^0, x_32^0'=x_32^0, y_16^0'=-1+y_16^0, y_28^0'=y_16^0, y_33^0'=y_33^0, (1-x_13^0 <= 0 /\ 1-y_16^0 <= 0), cost: 1 New rule: l4 -> l2 : x_13^0'=-1+x_13^0, x_27^0'=x_13^0, y_16^0'=-1+y_16^0, y_28^0'=y_16^0, (1-x_13^0 <= 0 /\ 1-y_16^0 <= 0), cost: 1 Propagated Equalities Original rule: l2 -> l1 : result_11^0'=result_11^post5, temp0_14^0'=temp0_14^post5, x_13^0'=x_13^post5, x_27^0'=x_27^post5, x_32^0'=x_32^post5, y_16^0'=y_16^post5, y_28^0'=y_28^post5, y_33^0'=y_33^post5, (-temp0_14^post5+temp0_14^0 == 0 /\ x_13^0-x_13^post5 == 0 /\ y_16^0-y_16^post5 == 0 /\ y_16^0 <= 0 /\ result_11^0-result_11^post5 == 0 /\ x_32^0-x_32^post5 == 0 /\ -y_33^post5+y_33^0 == 0 /\ x_27^0-x_27^post5 == 0 /\ y_28^0-y_28^post5 == 0), cost: 1 New rule: l2 -> l1 : result_11^0'=result_11^0, temp0_14^0'=temp0_14^0, x_13^0'=x_13^0, x_27^0'=x_27^0, x_32^0'=x_32^0, y_16^0'=y_16^0, y_28^0'=y_28^0, y_33^0'=y_33^0, (0 == 0 /\ y_16^0 <= 0), cost: 1 propagated equality temp0_14^post5 = temp0_14^0 propagated equality x_13^post5 = x_13^0 propagated equality y_16^post5 = y_16^0 propagated equality result_11^post5 = result_11^0 propagated equality x_32^post5 = x_32^0 propagated equality y_33^post5 = y_33^0 propagated equality x_27^post5 = x_27^0 propagated equality y_28^post5 = y_28^0 Simplified Guard Original rule: l2 -> l1 : result_11^0'=result_11^0, temp0_14^0'=temp0_14^0, x_13^0'=x_13^0, x_27^0'=x_27^0, x_32^0'=x_32^0, y_16^0'=y_16^0, y_28^0'=y_28^0, y_33^0'=y_33^0, (0 == 0 /\ y_16^0 <= 0), cost: 1 New rule: l2 -> l1 : result_11^0'=result_11^0, temp0_14^0'=temp0_14^0, x_13^0'=x_13^0, x_27^0'=x_27^0, x_32^0'=x_32^0, y_16^0'=y_16^0, y_28^0'=y_28^0, y_33^0'=y_33^0, y_16^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l2 -> l1 : result_11^0'=result_11^0, temp0_14^0'=temp0_14^0, x_13^0'=x_13^0, x_27^0'=x_27^0, x_32^0'=x_32^0, y_16^0'=y_16^0, y_28^0'=y_28^0, y_33^0'=y_33^0, y_16^0 <= 0, cost: 1 New rule: l2 -> l1 : y_16^0 <= 0, cost: 1 Propagated Equalities Original rule: l6 -> l1 : result_11^0'=result_11^post1, temp0_14^0'=temp0_14^post1, x_13^0'=x_13^post1, x_27^0'=x_27^post1, x_32^0'=x_32^post1, y_16^0'=y_16^post1, y_28^0'=y_28^post1, y_33^0'=y_33^post1, (0 == 0 /\ y_33^0-y_33^post8 == 0 /\ -y_33^post1+y_33^post8 == 0 /\ result_11^0-result_11^post8 == 0 /\ y_28^post8-y_28^post1 == 0 /\ -y_28^post8+y_28^0 == 0 /\ temp0_14^0-temp0_14^post8 == 0 /\ x_27^0-x_27^post8 == 0 /\ -result_11^post1+result_11^post8 == 0 /\ -x_32^post8+x_32^0 == 0 /\ x_13^0-x_13^post8 == 0 /\ -y_16^post8+y_16^0 == 0 /\ -temp0_14^post1+temp0_14^post8 == 0 /\ x_27^post8-x_27^post1 == 0 /\ x_32^post8-x_32^post1 == 0), cost: 1 New rule: l6 -> l1 : result_11^0'=result_11^post8, temp0_14^0'=temp0_14^post8, x_13^0'=x_13^post1, x_27^0'=x_27^post8, x_32^0'=x_32^post8, y_16^0'=y_16^post1, y_28^0'=y_28^post8, y_33^0'=y_33^post8, (0 == 0 /\ y_33^0-y_33^post8 == 0 /\ result_11^0-result_11^post8 == 0 /\ -y_28^post8+y_28^0 == 0 /\ temp0_14^0-temp0_14^post8 == 0 /\ x_27^0-x_27^post8 == 0 /\ -x_32^post8+x_32^0 == 0 /\ x_13^0-x_13^post8 == 0 /\ -y_16^post8+y_16^0 == 0), cost: 1 propagated equality y_33^post1 = y_33^post8 propagated equality y_28^post1 = y_28^post8 propagated equality result_11^post1 = result_11^post8 propagated equality temp0_14^post1 = temp0_14^post8 propagated equality x_27^post1 = x_27^post8 propagated equality x_32^post1 = x_32^post8 Propagated Equalities Original rule: l6 -> l1 : result_11^0'=result_11^post8, temp0_14^0'=temp0_14^post8, x_13^0'=x_13^post1, x_27^0'=x_27^post8, x_32^0'=x_32^post8, y_16^0'=y_16^post1, y_28^0'=y_28^post8, y_33^0'=y_33^post8, (0 == 0 /\ y_33^0-y_33^post8 == 0 /\ result_11^0-result_11^post8 == 0 /\ -y_28^post8+y_28^0 == 0 /\ temp0_14^0-temp0_14^post8 == 0 /\ x_27^0-x_27^post8 == 0 /\ -x_32^post8+x_32^0 == 0 /\ x_13^0-x_13^post8 == 0 /\ -y_16^post8+y_16^0 == 0), cost: 1 New rule: l6 -> l1 : result_11^0'=result_11^0, temp0_14^0'=temp0_14^0, x_13^0'=x_13^post1, x_27^0'=x_27^0, x_32^0'=x_32^0, y_16^0'=y_16^post1, y_28^0'=y_28^0, y_33^0'=y_33^0, 0 == 0, cost: 1 propagated equality y_33^post8 = y_33^0 propagated equality result_11^post8 = result_11^0 propagated equality y_28^post8 = y_28^0 propagated equality temp0_14^post8 = temp0_14^0 propagated equality x_27^post8 = x_27^0 propagated equality x_32^post8 = x_32^0 propagated equality x_13^post8 = x_13^0 propagated equality y_16^post8 = y_16^0 Simplified Guard Original rule: l6 -> l1 : result_11^0'=result_11^0, temp0_14^0'=temp0_14^0, x_13^0'=x_13^post1, x_27^0'=x_27^0, x_32^0'=x_32^0, y_16^0'=y_16^post1, y_28^0'=y_28^0, y_33^0'=y_33^0, 0 == 0, cost: 1 New rule: l6 -> l1 : result_11^0'=result_11^0, temp0_14^0'=temp0_14^0, x_13^0'=x_13^post1, x_27^0'=x_27^0, x_32^0'=x_32^0, y_16^0'=y_16^post1, y_28^0'=y_28^0, y_33^0'=y_33^0, T, cost: 1 Removed Trivial Updates Original rule: l6 -> l1 : result_11^0'=result_11^0, temp0_14^0'=temp0_14^0, x_13^0'=x_13^post1, x_27^0'=x_27^0, x_32^0'=x_32^0, y_16^0'=y_16^post1, y_28^0'=y_28^0, y_33^0'=y_33^0, T, cost: 1 New rule: l6 -> l1 : x_13^0'=x_13^post1, y_16^0'=y_16^post1, T, cost: 1 made implied equalities explicit Original rule: l2 -> l2 : result_11^0'=result_11^post7, temp0_14^0'=temp0_14^post7, x_13^0'=x_13^post7, x_27^0'=x_27^post7, x_32^0'=x_32^post7, y_16^0'=y_16^post7, y_28^0'=y_28^post7, y_33^0'=y_33^post7, (0 == 0 /\ y_16^post6-y_16^post7 == 0 /\ -x_27^post7+x_27^post6 == 0 /\ -x_32^post7+x_32^post6 == 0 /\ -1-x_13^post6+x_32^post6 <= 0 /\ -1-y_16^post6+y_33^post6 <= 0 /\ -temp0_14^post6+temp0_14^0 == 0 /\ -y_28^post7+y_28^post6 == 0 /\ -result_11^post7+result_11^post6 == 0 /\ -temp0_14^post7+temp0_14^post6 == 0 /\ 1+x_13^post6-x_13^0 == 0 /\ -x_27^post6+x_27^0 == 0 /\ result_11^0-result_11^post6 == 0 /\ 1+x_13^post6-x_32^post6 <= 0 /\ -y_33^post7+y_33^post6 == 0 /\ 1+y_16^post6-y_33^post6 <= 0 /\ 1+y_16^post6-y_16^0 == 0 /\ 1-y_33^post6 <= 0 /\ x_13^post6-x_13^post7 == 0 /\ 1-y_16^0 <= 0 /\ -y_28^post6+y_28^0 == 0), cost: 1 New rule: l2 -> l2 : result_11^0'=result_11^post7, temp0_14^0'=temp0_14^post7, x_13^0'=x_13^post7, x_27^0'=x_27^post7, x_32^0'=x_32^post7, y_16^0'=y_16^post7, y_28^0'=y_28^post7, y_33^0'=y_33^post7, (0 == 0 /\ y_16^post6-y_16^post7 == 0 /\ -x_27^post7+x_27^post6 == 0 /\ -x_32^post7+x_32^post6 == 0 /\ -1-x_13^post6+x_32^post6 <= 0 /\ -1-x_13^post6+x_32^post6 == 0 /\ -1-y_16^post6+y_33^post6 <= 0 /\ -1-y_16^post6+y_33^post6 == 0 /\ -temp0_14^post6+temp0_14^0 == 0 /\ -y_28^post7+y_28^post6 == 0 /\ -result_11^post7+result_11^post6 == 0 /\ -temp0_14^post7+temp0_14^post6 == 0 /\ 1+x_13^post6-x_13^0 == 0 /\ -x_27^post6+x_27^0 == 0 /\ result_11^0-result_11^post6 == 0 /\ 1+x_13^post6-x_32^post6 <= 0 /\ -y_33^post7+y_33^post6 == 0 /\ 1+y_16^post6-y_33^post6 <= 0 /\ 1+y_16^post6-y_16^0 == 0 /\ 1-y_33^post6 <= 0 /\ x_13^post6-x_13^post7 == 0 /\ 1-y_16^0 <= 0 /\ -y_28^post6+y_28^0 == 0), cost: 1 Propagated Equalities Original rule: l2 -> l2 : result_11^0'=result_11^post7, temp0_14^0'=temp0_14^post7, x_13^0'=x_13^post7, x_27^0'=x_27^post7, x_32^0'=x_32^post7, y_16^0'=y_16^post7, y_28^0'=y_28^post7, y_33^0'=y_33^post7, (0 == 0 /\ y_16^post6-y_16^post7 == 0 /\ -x_27^post7+x_27^post6 == 0 /\ -x_32^post7+x_32^post6 == 0 /\ -1-x_13^post6+x_32^post6 <= 0 /\ -1-x_13^post6+x_32^post6 == 0 /\ -1-y_16^post6+y_33^post6 <= 0 /\ -1-y_16^post6+y_33^post6 == 0 /\ -temp0_14^post6+temp0_14^0 == 0 /\ -y_28^post7+y_28^post6 == 0 /\ -result_11^post7+result_11^post6 == 0 /\ -temp0_14^post7+temp0_14^post6 == 0 /\ 1+x_13^post6-x_13^0 == 0 /\ -x_27^post6+x_27^0 == 0 /\ result_11^0-result_11^post6 == 0 /\ 1+x_13^post6-x_32^post6 <= 0 /\ -y_33^post7+y_33^post6 == 0 /\ 1+y_16^post6-y_33^post6 <= 0 /\ 1+y_16^post6-y_16^0 == 0 /\ 1-y_33^post6 <= 0 /\ x_13^post6-x_13^post7 == 0 /\ 1-y_16^0 <= 0 /\ -y_28^post6+y_28^0 == 0), cost: 1 New rule: l2 -> l2 : result_11^0'=result_11^post6, temp0_14^0'=temp0_14^post6, x_13^0'=x_13^post6, x_27^0'=x_27^post6, x_32^0'=x_32^post6, y_16^0'=y_16^post6, y_28^0'=y_28^post6, y_33^0'=y_33^post6, (0 == 0 /\ -1-x_13^post6+x_32^post6 <= 0 /\ -1-x_13^post6+x_32^post6 == 0 /\ -1-y_16^post6+y_33^post6 <= 0 /\ -1-y_16^post6+y_33^post6 == 0 /\ -temp0_14^post6+temp0_14^0 == 0 /\ 1+x_13^post6-x_13^0 == 0 /\ -x_27^post6+x_27^0 == 0 /\ result_11^0-result_11^post6 == 0 /\ 1+x_13^post6-x_32^post6 <= 0 /\ 1+y_16^post6-y_33^post6 <= 0 /\ 1+y_16^post6-y_16^0 == 0 /\ 1-y_33^post6 <= 0 /\ 1-y_16^0 <= 0 /\ -y_28^post6+y_28^0 == 0), cost: 1 propagated equality y_16^post7 = y_16^post6 propagated equality x_27^post7 = x_27^post6 propagated equality x_32^post7 = x_32^post6 propagated equality y_28^post7 = y_28^post6 propagated equality result_11^post7 = result_11^post6 propagated equality temp0_14^post7 = temp0_14^post6 propagated equality y_33^post7 = y_33^post6 propagated equality x_13^post7 = x_13^post6 Propagated Equalities Original rule: l2 -> l2 : result_11^0'=result_11^post6, temp0_14^0'=temp0_14^post6, x_13^0'=x_13^post6, x_27^0'=x_27^post6, x_32^0'=x_32^post6, y_16^0'=y_16^post6, y_28^0'=y_28^post6, y_33^0'=y_33^post6, (0 == 0 /\ -1-x_13^post6+x_32^post6 <= 0 /\ -1-x_13^post6+x_32^post6 == 0 /\ -1-y_16^post6+y_33^post6 <= 0 /\ -1-y_16^post6+y_33^post6 == 0 /\ -temp0_14^post6+temp0_14^0 == 0 /\ 1+x_13^post6-x_13^0 == 0 /\ -x_27^post6+x_27^0 == 0 /\ result_11^0-result_11^post6 == 0 /\ 1+x_13^post6-x_32^post6 <= 0 /\ 1+y_16^post6-y_33^post6 <= 0 /\ 1+y_16^post6-y_16^0 == 0 /\ 1-y_33^post6 <= 0 /\ 1-y_16^0 <= 0 /\ -y_28^post6+y_28^0 == 0), cost: 1 New rule: l2 -> l2 : result_11^0'=result_11^0, temp0_14^0'=temp0_14^0, x_13^0'=-1+x_13^0, x_27^0'=x_27^0, x_32^0'=x_13^0, y_16^0'=-1+y_16^0, y_28^0'=y_28^0, y_33^0'=y_16^0, (0 <= 0 /\ 0 == 0 /\ 1-y_16^0 <= 0), cost: 1 propagated equality x_13^post6 = -1+x_32^post6 propagated equality y_16^post6 = -1+y_33^post6 propagated equality temp0_14^post6 = temp0_14^0 propagated equality x_32^post6 = x_13^0 propagated equality x_27^post6 = x_27^0 propagated equality result_11^post6 = result_11^0 propagated equality y_33^post6 = y_16^0 propagated equality y_28^post6 = y_28^0 Simplified Guard Original rule: l2 -> l2 : result_11^0'=result_11^0, temp0_14^0'=temp0_14^0, x_13^0'=-1+x_13^0, x_27^0'=x_27^0, x_32^0'=x_13^0, y_16^0'=-1+y_16^0, y_28^0'=y_28^0, y_33^0'=y_16^0, (0 <= 0 /\ 0 == 0 /\ 1-y_16^0 <= 0), cost: 1 New rule: l2 -> l2 : result_11^0'=result_11^0, temp0_14^0'=temp0_14^0, x_13^0'=-1+x_13^0, x_27^0'=x_27^0, x_32^0'=x_13^0, y_16^0'=-1+y_16^0, y_28^0'=y_28^0, y_33^0'=y_16^0, 1-y_16^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l2 -> l2 : result_11^0'=result_11^0, temp0_14^0'=temp0_14^0, x_13^0'=-1+x_13^0, x_27^0'=x_27^0, x_32^0'=x_13^0, y_16^0'=-1+y_16^0, y_28^0'=y_28^0, y_33^0'=y_16^0, 1-y_16^0 <= 0, cost: 1 New rule: l2 -> l2 : x_13^0'=-1+x_13^0, x_32^0'=x_13^0, y_16^0'=-1+y_16^0, y_33^0'=y_16^0, 1-y_16^0 <= 0, cost: 1 Step with 14 Trace 14[T] Blocked [{}, {}] Step with 11 Trace 14[T], 11[(x_13^0 <= 0)] Blocked [{}, {}, {}] Backtrack Trace 14[T] Blocked [{}, {11[T]}] Step with 10 Trace 14[T], 10[(1-x_13^0 <= 0 /\ 1-y_16^post2 <= 0)] Blocked [{}, {11[T]}, {}] Step with 15 Trace 14[T], 10[(1-x_13^0 <= 0 /\ 1-y_16^post2 <= 0)], 15[(1-y_16^0 <= 0)] Blocked [{}, {11[T]}, {13[T]}, {}] Accelerate Start location: l6 Program variables: result_11^0 temp0_14^0 x_13^0 x_27^0 x_32^0 y_16^0 y_28^0 y_33^0 10: l1 -> l2 : y_16^0'=y_16^post2, (1-x_13^0 <= 0 /\ 1-y_16^post2 <= 0), cost: 1 11: l1 -> l3 : result_11^0'=temp0_14^0, x_13^0 <= 0, cost: 1 13: l2 -> l1 : y_16^0 <= 0, cost: 1 15: l2 -> l2 : x_13^0'=-1+x_13^0, x_32^0'=x_13^0, y_16^0'=-1+y_16^0, y_33^0'=y_16^0, 1-y_16^0 <= 0, cost: 1 16: l2 -> l2 : x_13^0'=x_13^0-n, x_32^0'=1+x_13^0-n, y_16^0'=y_16^0-n, y_33^0'=1+y_16^0-n, (-1+n >= 0 /\ y_16^0-n >= 0), cost: 1 12: l4 -> l2 : x_13^0'=-1+x_13^0, x_27^0'=x_13^0, y_16^0'=-1+y_16^0, y_28^0'=y_16^0, (1-x_13^0 <= 0 /\ 1-y_16^0 <= 0), cost: 1 14: l6 -> l1 : x_13^0'=x_13^post1, y_16^0'=y_16^post1, T, cost: 1 Loop Acceleration Original rule: l2 -> l2 : x_13^0'=-1+x_13^0, x_32^0'=x_13^0, y_16^0'=-1+y_16^0, y_33^0'=y_16^0, (1-y_16^0 <= 0), cost: 1 New rule: l2 -> l2 : x_13^0'=x_13^0-n, x_32^0'=1+x_13^0-n, y_16^0'=y_16^0-n, y_33^0'=1+y_16^0-n, (-1+n >= 0 /\ y_16^0-n >= 0), cost: 1 -1+y_16^0 >= 0 [0]: montonic decrease yields y_16^0-n >= 0 -1+y_16^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ -1+y_16^0 >= 0) Replacement map: {-1+y_16^0 >= 0 -> y_16^0-n >= 0} Trace 14[T], 10[(1-x_13^0 <= 0 /\ 1-y_16^post2 <= 0)], 16[(-1+n >= 0 /\ y_16^0-n >= 0)] Blocked [{}, {11[T]}, {13[T]}, {15[T], 16[T]}] Step with 13 Trace 14[T], 10[(1-x_13^0 <= 0 /\ 1-y_16^post2 <= 0)], 16[(-1+n >= 0 /\ y_16^0-n >= 0)], 13[(y_16^0 <= 0)] Blocked [{}, {11[T]}, {13[T]}, {15[T], 16[T]}, {}] Accelerate Start location: l6 Program variables: result_11^0 temp0_14^0 x_13^0 x_27^0 x_32^0 y_16^0 y_28^0 y_33^0 10: l1 -> l2 : y_16^0'=y_16^post2, (1-x_13^0 <= 0 /\ 1-y_16^post2 <= 0), cost: 1 11: l1 -> l3 : result_11^0'=temp0_14^0, x_13^0 <= 0, cost: 1 17: l1 -> l1 : x_13^0'=x_13^0-y_16^post21*n2, x_32^0'=1+x_13^0-y_16^post21-y_16^post21*(-1+n2), y_16^0'=0, y_33^0'=1, (-1+x_13^0-y_16^post21*(-1+n2) >= 0 /\ -1+n2 >= 0 /\ -1+y_16^post21 >= 0), cost: 1 13: l2 -> l1 : y_16^0 <= 0, cost: 1 15: l2 -> l2 : x_13^0'=-1+x_13^0, x_32^0'=x_13^0, y_16^0'=-1+y_16^0, y_33^0'=y_16^0, 1-y_16^0 <= 0, cost: 1 16: l2 -> l2 : x_13^0'=x_13^0-n, x_32^0'=1+x_13^0-n, y_16^0'=y_16^0-n, y_33^0'=1+y_16^0-n, (-1+n >= 0 /\ y_16^0-n >= 0), cost: 1 12: l4 -> l2 : x_13^0'=-1+x_13^0, x_27^0'=x_13^0, y_16^0'=-1+y_16^0, y_28^0'=y_16^0, (1-x_13^0 <= 0 /\ 1-y_16^0 <= 0), cost: 1 14: l6 -> l1 : x_13^0'=x_13^post1, y_16^0'=y_16^post1, T, cost: 1 Loop Acceleration Original rule: l1 -> l1 : x_13^0'=x_13^0-y_16^post21, x_32^0'=1+x_13^0-y_16^post21, y_16^0'=0, y_33^0'=1, (1-x_13^0 <= 0 /\ 1-y_16^post21 <= 0 /\ -1+y_16^post21 >= 0), cost: 1 New rule: l1 -> l1 : x_13^0'=x_13^0-y_16^post21*n2, x_32^0'=1+x_13^0-y_16^post21-y_16^post21*(-1+n2), y_16^0'=0, y_33^0'=1, (-1+x_13^0-y_16^post21*(-1+n2) >= 0 /\ -1+n2 >= 0 /\ -1+y_16^post21 >= 0), cost: 1 -1+x_13^0 >= 0 [0]: montonic decrease yields -1+x_13^0-y_16^post21*(-1+n2) >= 0, dependencies: -1+y_16^post21 >= 0 -1+x_13^0 >= 0 [1]: eventual decrease yields (-1+x_13^0-y_16^post21*(-1+n2) >= 0 /\ -1+x_13^0 >= 0) -1+x_13^0 >= 0 [2]: eventual increase yields (y_16^post21 <= 0 /\ -1+x_13^0 >= 0) -1+y_16^post21 >= 0 [0]: monotonic increase yields -1+y_16^post21 >= 0 Replacement map: {-1+x_13^0 >= 0 -> -1+x_13^0-y_16^post21*(-1+n2) >= 0, -1+y_16^post21 >= 0 -> -1+y_16^post21 >= 0} Trace 14[T], 17[(-1+x_13^0-y_16^post21*(-1+n2) >= 0 /\ -1+n2 >= 0 /\ -1+y_16^post21 >= 0)] Blocked [{}, {11[T]}, {17[T]}] Step with 11 Trace 14[T], 17[(-1+x_13^0-y_16^post21*(-1+n2) >= 0 /\ -1+n2 >= 0 /\ -1+y_16^post21 >= 0)], 11[(x_13^0 <= 0)] Blocked [{}, {11[T]}, {17[T]}, {}] Backtrack Trace 14[T], 17[(-1+x_13^0-y_16^post21*(-1+n2) >= 0 /\ -1+n2 >= 0 /\ -1+y_16^post21 >= 0)] Blocked [{}, {11[T]}, {11[T], 17[T]}] Step with 10 Trace 14[T], 17[(-1+x_13^0-y_16^post21*(-1+n2) >= 0 /\ -1+n2 >= 0 /\ -1+y_16^post21 >= 0)], 10[(1-x_13^0 <= 0 /\ 1-y_16^post2 <= 0)] Blocked [{}, {11[T]}, {11[T], 17[T]}, {}] Step with 15 Trace 14[T], 17[(-1+x_13^0-y_16^post21*(-1+n2) >= 0 /\ -1+n2 >= 0 /\ -1+y_16^post21 >= 0)], 10[(1-x_13^0 <= 0 /\ 1-y_16^post2 <= 0)], 15[(1-y_16^0 <= 0)] Blocked [{}, {11[T]}, {11[T], 17[T]}, {13[T]}, {}] Covered Trace 14[T], 17[(-1+x_13^0-y_16^post21*(-1+n2) >= 0 /\ -1+n2 >= 0 /\ -1+y_16^post21 >= 0)], 10[(1-x_13^0 <= 0 /\ 1-y_16^post2 <= 0)] Blocked [{}, {11[T]}, {11[T], 17[T]}, {13[T], 15[T]}] Step with 16 Trace 14[T], 17[(-1+x_13^0-y_16^post21*(-1+n2) >= 0 /\ -1+n2 >= 0 /\ -1+y_16^post21 >= 0)], 10[(1-x_13^0 <= 0 /\ 1-y_16^post2 <= 0)], 16[(-1+n >= 0 /\ y_16^0-n >= 0)] Blocked [{}, {11[T]}, {11[T], 17[T]}, {13[T], 15[T]}, {16[T]}] Step with 13 Trace 14[T], 17[(-1+x_13^0-y_16^post21*(-1+n2) >= 0 /\ -1+n2 >= 0 /\ -1+y_16^post21 >= 0)], 10[(1-x_13^0 <= 0 /\ 1-y_16^post2 <= 0)], 16[(-1+n >= 0 /\ y_16^0-n >= 0)], 13[(y_16^0 <= 0)] Blocked [{}, {11[T]}, {11[T], 17[T]}, {13[T], 15[T]}, {16[T]}, {}] Covered Trace 14[T], 17[(-1+x_13^0-y_16^post21*(-1+n2) >= 0 /\ -1+n2 >= 0 /\ -1+y_16^post21 >= 0)], 10[(1-x_13^0 <= 0 /\ 1-y_16^post2 <= 0)], 16[(-1+n >= 0 /\ y_16^0-n >= 0)] Blocked [{}, {11[T]}, {11[T], 17[T]}, {13[T], 15[T]}, {13[T], 16[T]}] Step with 15 Trace 14[T], 17[(-1+x_13^0-y_16^post21*(-1+n2) >= 0 /\ -1+n2 >= 0 /\ -1+y_16^post21 >= 0)], 10[(1-x_13^0 <= 0 /\ 1-y_16^post2 <= 0)], 16[(-1+n >= 0 /\ y_16^0-n >= 0)], 15[(1-y_16^0 <= 0)] Blocked [{}, {11[T]}, {11[T], 17[T]}, {13[T], 15[T]}, {13[T], 16[T]}, {}] Covered Trace 14[T], 17[(-1+x_13^0-y_16^post21*(-1+n2) >= 0 /\ -1+n2 >= 0 /\ -1+y_16^post21 >= 0)], 10[(1-x_13^0 <= 0 /\ 1-y_16^post2 <= 0)], 16[(-1+n >= 0 /\ y_16^0-n >= 0)] Blocked [{}, {11[T]}, {11[T], 17[T]}, {13[T], 15[T]}, {13[T], 15[T], 16[T]}] Backtrack Trace 14[T], 17[(-1+x_13^0-y_16^post21*(-1+n2) >= 0 /\ -1+n2 >= 0 /\ -1+y_16^post21 >= 0)], 10[(1-x_13^0 <= 0 /\ 1-y_16^post2 <= 0)] Blocked [{}, {11[T]}, {11[T], 17[T]}, {13[T], 15[T], 16[T]}] Backtrack Trace 14[T], 17[(-1+x_13^0-y_16^post21*(-1+n2) >= 0 /\ -1+n2 >= 0 /\ -1+y_16^post21 >= 0)] Blocked [{}, {11[T]}, {10[T], 11[T], 17[T]}] Backtrack Trace 14[T] Blocked [{}, {11[T], 17[T]}] Step with 10 Trace 14[T], 10[(1-x_13^0 <= 0 /\ 1-y_16^post2 <= 0)] Blocked [{}, {11[T], 17[T]}, {}] Step with 15 Trace 14[T], 10[(1-x_13^0 <= 0 /\ 1-y_16^post2 <= 0)], 15[(1-y_16^0 <= 0)] Blocked [{}, {11[T], 17[T]}, {}, {}] Covered Trace 14[T], 10[(1-x_13^0 <= 0 /\ 1-y_16^post2 <= 0)] Blocked [{}, {11[T], 17[T]}, {15[T]}] Step with 16 Trace 14[T], 10[(1-x_13^0 <= 0 /\ 1-y_16^post2 <= 0)], 16[(-1+n >= 0 /\ y_16^0-n >= 0)] Blocked [{}, {11[T], 17[T]}, {15[T]}, {16[T]}] Step with 13 Trace 14[T], 10[(1-x_13^0 <= 0 /\ 1-y_16^post2 <= 0)], 16[(-1+n >= 0 /\ y_16^0-n >= 0)], 13[(y_16^0 <= 0)] Blocked [{}, {11[T], 17[T]}, {15[T]}, {16[T]}, {}] Covered Trace 14[T], 10[(1-x_13^0 <= 0 /\ 1-y_16^post2 <= 0)], 16[(-1+n >= 0 /\ y_16^0-n >= 0)] Blocked [{}, {11[T], 17[T]}, {15[T]}, {13[T], 16[T]}] Step with 15 Trace 14[T], 10[(1-x_13^0 <= 0 /\ 1-y_16^post2 <= 0)], 16[(-1+n >= 0 /\ y_16^0-n >= 0)], 15[(1-y_16^0 <= 0)] Blocked [{}, {11[T], 17[T]}, {15[T]}, {13[T], 16[T]}, {}] Covered Trace 14[T], 10[(1-x_13^0 <= 0 /\ 1-y_16^post2 <= 0)], 16[(-1+n >= 0 /\ y_16^0-n >= 0)] Blocked [{}, {11[T], 17[T]}, {15[T]}, {13[T], 15[T], 16[T]}] Backtrack Trace 14[T], 10[(1-x_13^0 <= 0 /\ 1-y_16^post2 <= 0)] Blocked [{}, {11[T], 17[T]}, {15[T], 16[T]}] Backtrack Trace 14[T] Blocked [{}, {10[T], 11[T], 17[T]}] Backtrack Trace Blocked [{14[T]}] Accept unknown Build SHA: a05f16bf13df659c382799650051f91bf6828c7b