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