unknown Initial ITS Start location: l5 Program variables: __len9^0 __val8^0 tmp10^0 tmp^0 tmp___0^0 tmp___1^0 0: l0 -> l1 : __len9^0'=__len9^post1, __val8^0'=__val8^post1, tmp10^0'=tmp10^post1, tmp^0'=tmp^post1, tmp___0^0'=tmp___0^post1, tmp___1^0'=tmp___1^post1, (-tmp^post1+tmp^0 == 0 /\ -tmp___0^post1+tmp___0^0 == 0 /\ __len9^0-__len9^post1 == 0 /\ -tmp10^post1+tmp10^0 == 0 /\ -tmp___1^post1+tmp___1^0 == 0 /\ -__val8^post1+__val8^0 == 0), cost: 1 1: l2 -> l0 : __len9^0'=__len9^post2, __val8^0'=__val8^post2, tmp10^0'=tmp10^post2, tmp^0'=tmp^post2, tmp___0^0'=tmp___0^post2, tmp___1^0'=tmp___1^post2, (0 == 0 /\ -tmp10^post2+tmp10^0 == 0 /\ -tmp___1^post2+tmp___1^0 == 0 /\ __val8^0-__val8^post2 == 0 /\ -tmp^post2+tmp^0 == 0 /\ -__len9^post2+__len9^0 == 0), cost: 1 2: l3 -> l0 : __len9^0'=__len9^post3, __val8^0'=__val8^post3, tmp10^0'=tmp10^post3, tmp^0'=tmp^post3, tmp___0^0'=tmp___0^post3, tmp___1^0'=tmp___1^post3, (0 == 0 /\ -tmp^post3+tmp^0 == 0 /\ 1+tmp___1^0 <= 0 /\ -1-tmp___1^0 <= 0 /\ tmp___1^0-tmp___1^post3 == 0 /\ tmp___0^0-tmp___0^post3 == 0 /\ __val8^post3 == 0), cost: 1 3: l3 -> l2 : __len9^0'=__len9^post4, __val8^0'=__val8^post4, tmp10^0'=tmp10^post4, tmp^0'=tmp^post4, tmp___0^0'=tmp___0^post4, tmp___1^0'=tmp___1^post4, (tmp___0^0-tmp___0^post4 == 0 /\ -tmp^post4+tmp^0 == 0 /\ __val8^0-__val8^post4 == 0 /\ -__len9^post4+__len9^0 == 0 /\ -tmp___1^0 <= 0 /\ tmp10^0-tmp10^post4 == 0 /\ tmp___1^0-tmp___1^post4 == 0), cost: 1 4: l3 -> l2 : __len9^0'=__len9^post5, __val8^0'=__val8^post5, tmp10^0'=tmp10^post5, tmp^0'=tmp^post5, tmp___0^0'=tmp___0^post5, tmp___1^0'=tmp___1^post5, (tmp10^0-tmp10^post5 == 0 /\ -__len9^post5+__len9^0 == 0 /\ 2+tmp___1^0 <= 0 /\ -tmp___1^post5+tmp___1^0 == 0 /\ tmp___0^0-tmp___0^post5 == 0 /\ __val8^0-__val8^post5 == 0 /\ -tmp^post5+tmp^0 == 0), cost: 1 5: l4 -> l3 : __len9^0'=__len9^post6, __val8^0'=__val8^post6, tmp10^0'=tmp10^post6, tmp^0'=tmp^post6, tmp___0^0'=tmp___0^post6, tmp___1^0'=tmp___1^post6, (0 == 0 /\ tmp10^0-tmp10^post6 == 0 /\ __len9^0-__len9^post6 == 0 /\ tmp___0^0-tmp___0^post6 == 0 /\ -__val8^post6+__val8^0 == 0), cost: 1 6: l5 -> l4 : __len9^0'=__len9^post7, __val8^0'=__val8^post7, tmp10^0'=tmp10^post7, tmp^0'=tmp^post7, tmp___0^0'=tmp___0^post7, tmp___1^0'=tmp___1^post7, (__len9^0-__len9^post7 == 0 /\ -tmp___1^post7+tmp___1^0 == 0 /\ -__val8^post7+__val8^0 == 0 /\ tmp10^0-tmp10^post7 == 0 /\ -tmp^post7+tmp^0 == 0 /\ tmp___0^0-tmp___0^post7 == 0), cost: 1 Chained Linear Paths Start location: l5 Program variables: __len9^0 __val8^0 tmp10^0 tmp^0 tmp___0^0 tmp___1^0 0: l0 -> l1 : __len9^0'=__len9^post1, __val8^0'=__val8^post1, tmp10^0'=tmp10^post1, tmp^0'=tmp^post1, tmp___0^0'=tmp___0^post1, tmp___1^0'=tmp___1^post1, (-tmp^post1+tmp^0 == 0 /\ -tmp___0^post1+tmp___0^0 == 0 /\ __len9^0-__len9^post1 == 0 /\ -tmp10^post1+tmp10^0 == 0 /\ -tmp___1^post1+tmp___1^0 == 0 /\ -__val8^post1+__val8^0 == 0), cost: 1 1: l2 -> l0 : __len9^0'=__len9^post2, __val8^0'=__val8^post2, tmp10^0'=tmp10^post2, tmp^0'=tmp^post2, tmp___0^0'=tmp___0^post2, tmp___1^0'=tmp___1^post2, (0 == 0 /\ -tmp10^post2+tmp10^0 == 0 /\ -tmp___1^post2+tmp___1^0 == 0 /\ __val8^0-__val8^post2 == 0 /\ -tmp^post2+tmp^0 == 0 /\ -__len9^post2+__len9^0 == 0), cost: 1 2: l3 -> l0 : __len9^0'=__len9^post3, __val8^0'=__val8^post3, tmp10^0'=tmp10^post3, tmp^0'=tmp^post3, tmp___0^0'=tmp___0^post3, tmp___1^0'=tmp___1^post3, (0 == 0 /\ -tmp^post3+tmp^0 == 0 /\ 1+tmp___1^0 <= 0 /\ -1-tmp___1^0 <= 0 /\ tmp___1^0-tmp___1^post3 == 0 /\ tmp___0^0-tmp___0^post3 == 0 /\ __val8^post3 == 0), cost: 1 3: l3 -> l2 : __len9^0'=__len9^post4, __val8^0'=__val8^post4, tmp10^0'=tmp10^post4, tmp^0'=tmp^post4, tmp___0^0'=tmp___0^post4, tmp___1^0'=tmp___1^post4, (tmp___0^0-tmp___0^post4 == 0 /\ -tmp^post4+tmp^0 == 0 /\ __val8^0-__val8^post4 == 0 /\ -__len9^post4+__len9^0 == 0 /\ -tmp___1^0 <= 0 /\ tmp10^0-tmp10^post4 == 0 /\ tmp___1^0-tmp___1^post4 == 0), cost: 1 4: l3 -> l2 : __len9^0'=__len9^post5, __val8^0'=__val8^post5, tmp10^0'=tmp10^post5, tmp^0'=tmp^post5, tmp___0^0'=tmp___0^post5, tmp___1^0'=tmp___1^post5, (tmp10^0-tmp10^post5 == 0 /\ -__len9^post5+__len9^0 == 0 /\ 2+tmp___1^0 <= 0 /\ -tmp___1^post5+tmp___1^0 == 0 /\ tmp___0^0-tmp___0^post5 == 0 /\ __val8^0-__val8^post5 == 0 /\ -tmp^post5+tmp^0 == 0), cost: 1 7: l5 -> l3 : __len9^0'=__len9^post6, __val8^0'=__val8^post6, tmp10^0'=tmp10^post6, tmp^0'=tmp^post6, tmp___0^0'=tmp___0^post6, tmp___1^0'=tmp___1^post6, (0 == 0 /\ __val8^post7-__val8^post6 == 0 /\ __len9^0-__len9^post7 == 0 /\ tmp10^post7-tmp10^post6 == 0 /\ __len9^post7-__len9^post6 == 0 /\ -tmp___1^post7+tmp___1^0 == 0 /\ -__val8^post7+__val8^0 == 0 /\ tmp___0^post7-tmp___0^post6 == 0 /\ tmp10^0-tmp10^post7 == 0 /\ -tmp^post7+tmp^0 == 0 /\ tmp___0^0-tmp___0^post7 == 0), cost: 1 Eliminating location l4 by chaining: Applied chaining First rule: l5 -> l4 : __len9^0'=__len9^post7, __val8^0'=__val8^post7, tmp10^0'=tmp10^post7, tmp^0'=tmp^post7, tmp___0^0'=tmp___0^post7, tmp___1^0'=tmp___1^post7, (__len9^0-__len9^post7 == 0 /\ -tmp___1^post7+tmp___1^0 == 0 /\ -__val8^post7+__val8^0 == 0 /\ tmp10^0-tmp10^post7 == 0 /\ -tmp^post7+tmp^0 == 0 /\ tmp___0^0-tmp___0^post7 == 0), cost: 1 Second rule: l4 -> l3 : __len9^0'=__len9^post6, __val8^0'=__val8^post6, tmp10^0'=tmp10^post6, tmp^0'=tmp^post6, tmp___0^0'=tmp___0^post6, tmp___1^0'=tmp___1^post6, (0 == 0 /\ tmp10^0-tmp10^post6 == 0 /\ __len9^0-__len9^post6 == 0 /\ tmp___0^0-tmp___0^post6 == 0 /\ -__val8^post6+__val8^0 == 0), cost: 1 New rule: l5 -> l3 : __len9^0'=__len9^post6, __val8^0'=__val8^post6, tmp10^0'=tmp10^post6, tmp^0'=tmp^post6, tmp___0^0'=tmp___0^post6, tmp___1^0'=tmp___1^post6, (0 == 0 /\ __val8^post7-__val8^post6 == 0 /\ __len9^0-__len9^post7 == 0 /\ tmp10^post7-tmp10^post6 == 0 /\ __len9^post7-__len9^post6 == 0 /\ -tmp___1^post7+tmp___1^0 == 0 /\ -__val8^post7+__val8^0 == 0 /\ tmp___0^post7-tmp___0^post6 == 0 /\ tmp10^0-tmp10^post7 == 0 /\ -tmp^post7+tmp^0 == 0 /\ tmp___0^0-tmp___0^post7 == 0), cost: 1 Applied deletion Removed the following rules: 5 6 Simplified Transitions Start location: l5 Program variables: __len9^0 __val8^0 tmp10^0 tmp^0 tmp___0^0 tmp___1^0 8: l0 -> l1 : T, cost: 1 9: l2 -> l0 : tmp___0^0'=tmp___0^post2, T, cost: 1 10: l3 -> l0 : __len9^0'=__len9^post3, __val8^0'=0, tmp10^0'=tmp10^post3, (1+tmp___1^0 <= 0 /\ 1+tmp___1^0 == 0 /\ -1-tmp___1^0 <= 0), cost: 1 11: l3 -> l2 : -tmp___1^0 <= 0, cost: 1 12: l3 -> l2 : 2+tmp___1^0 <= 0, cost: 1 13: l5 -> l3 : tmp^0'=tmp^post6, tmp___1^0'=tmp___1^post6, T, cost: 1 Propagated Equalities Original rule: l0 -> l1 : __len9^0'=__len9^post1, __val8^0'=__val8^post1, tmp10^0'=tmp10^post1, tmp^0'=tmp^post1, tmp___0^0'=tmp___0^post1, tmp___1^0'=tmp___1^post1, (-tmp^post1+tmp^0 == 0 /\ -tmp___0^post1+tmp___0^0 == 0 /\ __len9^0-__len9^post1 == 0 /\ -tmp10^post1+tmp10^0 == 0 /\ -tmp___1^post1+tmp___1^0 == 0 /\ -__val8^post1+__val8^0 == 0), cost: 1 New rule: l0 -> l1 : __len9^0'=__len9^0, __val8^0'=__val8^0, tmp10^0'=tmp10^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1 propagated equality tmp^post1 = tmp^0 propagated equality tmp___0^post1 = tmp___0^0 propagated equality __len9^post1 = __len9^0 propagated equality tmp10^post1 = tmp10^0 propagated equality tmp___1^post1 = tmp___1^0 propagated equality __val8^post1 = __val8^0 Simplified Guard Original rule: l0 -> l1 : __len9^0'=__len9^0, __val8^0'=__val8^0, tmp10^0'=tmp10^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1 New rule: l0 -> l1 : __len9^0'=__len9^0, __val8^0'=__val8^0, tmp10^0'=tmp10^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, T, cost: 1 Removed Trivial Updates Original rule: l0 -> l1 : __len9^0'=__len9^0, __val8^0'=__val8^0, tmp10^0'=tmp10^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, T, cost: 1 New rule: l0 -> l1 : T, cost: 1 Propagated Equalities Original rule: l2 -> l0 : __len9^0'=__len9^post2, __val8^0'=__val8^post2, tmp10^0'=tmp10^post2, tmp^0'=tmp^post2, tmp___0^0'=tmp___0^post2, tmp___1^0'=tmp___1^post2, (0 == 0 /\ -tmp10^post2+tmp10^0 == 0 /\ -tmp___1^post2+tmp___1^0 == 0 /\ __val8^0-__val8^post2 == 0 /\ -tmp^post2+tmp^0 == 0 /\ -__len9^post2+__len9^0 == 0), cost: 1 New rule: l2 -> l0 : __len9^0'=__len9^0, __val8^0'=__val8^0, tmp10^0'=tmp10^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^post2, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1 propagated equality tmp10^post2 = tmp10^0 propagated equality tmp___1^post2 = tmp___1^0 propagated equality __val8^post2 = __val8^0 propagated equality tmp^post2 = tmp^0 propagated equality __len9^post2 = __len9^0 Simplified Guard Original rule: l2 -> l0 : __len9^0'=__len9^0, __val8^0'=__val8^0, tmp10^0'=tmp10^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^post2, tmp___1^0'=tmp___1^0, 0 == 0, cost: 1 New rule: l2 -> l0 : __len9^0'=__len9^0, __val8^0'=__val8^0, tmp10^0'=tmp10^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^post2, tmp___1^0'=tmp___1^0, T, cost: 1 Removed Trivial Updates Original rule: l2 -> l0 : __len9^0'=__len9^0, __val8^0'=__val8^0, tmp10^0'=tmp10^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^post2, tmp___1^0'=tmp___1^0, T, cost: 1 New rule: l2 -> l0 : tmp___0^0'=tmp___0^post2, T, cost: 1 made implied equalities explicit Original rule: l3 -> l0 : __len9^0'=__len9^post3, __val8^0'=__val8^post3, tmp10^0'=tmp10^post3, tmp^0'=tmp^post3, tmp___0^0'=tmp___0^post3, tmp___1^0'=tmp___1^post3, (0 == 0 /\ -tmp^post3+tmp^0 == 0 /\ 1+tmp___1^0 <= 0 /\ -1-tmp___1^0 <= 0 /\ tmp___1^0-tmp___1^post3 == 0 /\ tmp___0^0-tmp___0^post3 == 0 /\ __val8^post3 == 0), cost: 1 New rule: l3 -> l0 : __len9^0'=__len9^post3, __val8^0'=__val8^post3, tmp10^0'=tmp10^post3, tmp^0'=tmp^post3, tmp___0^0'=tmp___0^post3, tmp___1^0'=tmp___1^post3, (0 == 0 /\ -tmp^post3+tmp^0 == 0 /\ 1+tmp___1^0 <= 0 /\ 1+tmp___1^0 == 0 /\ -1-tmp___1^0 <= 0 /\ tmp___1^0-tmp___1^post3 == 0 /\ tmp___0^0-tmp___0^post3 == 0 /\ __val8^post3 == 0), cost: 1 Propagated Equalities Original rule: l3 -> l0 : __len9^0'=__len9^post3, __val8^0'=__val8^post3, tmp10^0'=tmp10^post3, tmp^0'=tmp^post3, tmp___0^0'=tmp___0^post3, tmp___1^0'=tmp___1^post3, (0 == 0 /\ -tmp^post3+tmp^0 == 0 /\ 1+tmp___1^0 <= 0 /\ 1+tmp___1^0 == 0 /\ -1-tmp___1^0 <= 0 /\ tmp___1^0-tmp___1^post3 == 0 /\ tmp___0^0-tmp___0^post3 == 0 /\ __val8^post3 == 0), cost: 1 New rule: l3 -> l0 : __len9^0'=__len9^post3, __val8^0'=0, tmp10^0'=tmp10^post3, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, (0 == 0 /\ 1+tmp___1^0 <= 0 /\ 1+tmp___1^0 == 0 /\ -1-tmp___1^0 <= 0), cost: 1 propagated equality tmp^post3 = tmp^0 propagated equality tmp___1^post3 = tmp___1^0 propagated equality tmp___0^post3 = tmp___0^0 propagated equality __val8^post3 = 0 Simplified Guard Original rule: l3 -> l0 : __len9^0'=__len9^post3, __val8^0'=0, tmp10^0'=tmp10^post3, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, (0 == 0 /\ 1+tmp___1^0 <= 0 /\ 1+tmp___1^0 == 0 /\ -1-tmp___1^0 <= 0), cost: 1 New rule: l3 -> l0 : __len9^0'=__len9^post3, __val8^0'=0, tmp10^0'=tmp10^post3, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, (1+tmp___1^0 <= 0 /\ 1+tmp___1^0 == 0 /\ -1-tmp___1^0 <= 0), cost: 1 made implied equalities explicit Original rule: l3 -> l0 : __len9^0'=__len9^post3, __val8^0'=0, tmp10^0'=tmp10^post3, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, (1+tmp___1^0 <= 0 /\ 1+tmp___1^0 == 0 /\ -1-tmp___1^0 <= 0), cost: 1 New rule: l3 -> l0 : __len9^0'=__len9^post3, __val8^0'=0, tmp10^0'=tmp10^post3, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, (1+tmp___1^0 <= 0 /\ 1+tmp___1^0 == 0 /\ -1-tmp___1^0 <= 0), cost: 1 Removed Trivial Updates Original rule: l3 -> l0 : __len9^0'=__len9^post3, __val8^0'=0, tmp10^0'=tmp10^post3, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, (1+tmp___1^0 <= 0 /\ 1+tmp___1^0 == 0 /\ -1-tmp___1^0 <= 0), cost: 1 New rule: l3 -> l0 : __len9^0'=__len9^post3, __val8^0'=0, tmp10^0'=tmp10^post3, (1+tmp___1^0 <= 0 /\ 1+tmp___1^0 == 0 /\ -1-tmp___1^0 <= 0), cost: 1 Propagated Equalities Original rule: l3 -> l2 : __len9^0'=__len9^post4, __val8^0'=__val8^post4, tmp10^0'=tmp10^post4, tmp^0'=tmp^post4, tmp___0^0'=tmp___0^post4, tmp___1^0'=tmp___1^post4, (tmp___0^0-tmp___0^post4 == 0 /\ -tmp^post4+tmp^0 == 0 /\ __val8^0-__val8^post4 == 0 /\ -__len9^post4+__len9^0 == 0 /\ -tmp___1^0 <= 0 /\ tmp10^0-tmp10^post4 == 0 /\ tmp___1^0-tmp___1^post4 == 0), cost: 1 New rule: l3 -> l2 : __len9^0'=__len9^0, __val8^0'=__val8^0, tmp10^0'=tmp10^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, (0 == 0 /\ -tmp___1^0 <= 0), cost: 1 propagated equality tmp___0^post4 = tmp___0^0 propagated equality tmp^post4 = tmp^0 propagated equality __val8^post4 = __val8^0 propagated equality __len9^post4 = __len9^0 propagated equality tmp10^post4 = tmp10^0 propagated equality tmp___1^post4 = tmp___1^0 Simplified Guard Original rule: l3 -> l2 : __len9^0'=__len9^0, __val8^0'=__val8^0, tmp10^0'=tmp10^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, (0 == 0 /\ -tmp___1^0 <= 0), cost: 1 New rule: l3 -> l2 : __len9^0'=__len9^0, __val8^0'=__val8^0, tmp10^0'=tmp10^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, -tmp___1^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l3 -> l2 : __len9^0'=__len9^0, __val8^0'=__val8^0, tmp10^0'=tmp10^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, -tmp___1^0 <= 0, cost: 1 New rule: l3 -> l2 : -tmp___1^0 <= 0, cost: 1 Propagated Equalities Original rule: l3 -> l2 : __len9^0'=__len9^post5, __val8^0'=__val8^post5, tmp10^0'=tmp10^post5, tmp^0'=tmp^post5, tmp___0^0'=tmp___0^post5, tmp___1^0'=tmp___1^post5, (tmp10^0-tmp10^post5 == 0 /\ -__len9^post5+__len9^0 == 0 /\ 2+tmp___1^0 <= 0 /\ -tmp___1^post5+tmp___1^0 == 0 /\ tmp___0^0-tmp___0^post5 == 0 /\ __val8^0-__val8^post5 == 0 /\ -tmp^post5+tmp^0 == 0), cost: 1 New rule: l3 -> l2 : __len9^0'=__len9^0, __val8^0'=__val8^0, tmp10^0'=tmp10^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, (0 == 0 /\ 2+tmp___1^0 <= 0), cost: 1 propagated equality tmp10^post5 = tmp10^0 propagated equality __len9^post5 = __len9^0 propagated equality tmp___1^post5 = tmp___1^0 propagated equality tmp___0^post5 = tmp___0^0 propagated equality __val8^post5 = __val8^0 propagated equality tmp^post5 = tmp^0 Simplified Guard Original rule: l3 -> l2 : __len9^0'=__len9^0, __val8^0'=__val8^0, tmp10^0'=tmp10^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, (0 == 0 /\ 2+tmp___1^0 <= 0), cost: 1 New rule: l3 -> l2 : __len9^0'=__len9^0, __val8^0'=__val8^0, tmp10^0'=tmp10^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 2+tmp___1^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l3 -> l2 : __len9^0'=__len9^0, __val8^0'=__val8^0, tmp10^0'=tmp10^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^0, 2+tmp___1^0 <= 0, cost: 1 New rule: l3 -> l2 : 2+tmp___1^0 <= 0, cost: 1 Propagated Equalities Original rule: l5 -> l3 : __len9^0'=__len9^post6, __val8^0'=__val8^post6, tmp10^0'=tmp10^post6, tmp^0'=tmp^post6, tmp___0^0'=tmp___0^post6, tmp___1^0'=tmp___1^post6, (0 == 0 /\ __val8^post7-__val8^post6 == 0 /\ __len9^0-__len9^post7 == 0 /\ tmp10^post7-tmp10^post6 == 0 /\ __len9^post7-__len9^post6 == 0 /\ -tmp___1^post7+tmp___1^0 == 0 /\ -__val8^post7+__val8^0 == 0 /\ tmp___0^post7-tmp___0^post6 == 0 /\ tmp10^0-tmp10^post7 == 0 /\ -tmp^post7+tmp^0 == 0 /\ tmp___0^0-tmp___0^post7 == 0), cost: 1 New rule: l5 -> l3 : __len9^0'=__len9^post7, __val8^0'=__val8^post7, tmp10^0'=tmp10^post7, tmp^0'=tmp^post6, tmp___0^0'=tmp___0^post7, tmp___1^0'=tmp___1^post6, (0 == 0 /\ __len9^0-__len9^post7 == 0 /\ -tmp___1^post7+tmp___1^0 == 0 /\ -__val8^post7+__val8^0 == 0 /\ tmp10^0-tmp10^post7 == 0 /\ -tmp^post7+tmp^0 == 0 /\ tmp___0^0-tmp___0^post7 == 0), cost: 1 propagated equality __val8^post6 = __val8^post7 propagated equality tmp10^post6 = tmp10^post7 propagated equality __len9^post6 = __len9^post7 propagated equality tmp___0^post6 = tmp___0^post7 Propagated Equalities Original rule: l5 -> l3 : __len9^0'=__len9^post7, __val8^0'=__val8^post7, tmp10^0'=tmp10^post7, tmp^0'=tmp^post6, tmp___0^0'=tmp___0^post7, tmp___1^0'=tmp___1^post6, (0 == 0 /\ __len9^0-__len9^post7 == 0 /\ -tmp___1^post7+tmp___1^0 == 0 /\ -__val8^post7+__val8^0 == 0 /\ tmp10^0-tmp10^post7 == 0 /\ -tmp^post7+tmp^0 == 0 /\ tmp___0^0-tmp___0^post7 == 0), cost: 1 New rule: l5 -> l3 : __len9^0'=__len9^0, __val8^0'=__val8^0, tmp10^0'=tmp10^0, tmp^0'=tmp^post6, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^post6, 0 == 0, cost: 1 propagated equality __len9^post7 = __len9^0 propagated equality tmp___1^post7 = tmp___1^0 propagated equality __val8^post7 = __val8^0 propagated equality tmp10^post7 = tmp10^0 propagated equality tmp^post7 = tmp^0 propagated equality tmp___0^post7 = tmp___0^0 Simplified Guard Original rule: l5 -> l3 : __len9^0'=__len9^0, __val8^0'=__val8^0, tmp10^0'=tmp10^0, tmp^0'=tmp^post6, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^post6, 0 == 0, cost: 1 New rule: l5 -> l3 : __len9^0'=__len9^0, __val8^0'=__val8^0, tmp10^0'=tmp10^0, tmp^0'=tmp^post6, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^post6, T, cost: 1 Removed Trivial Updates Original rule: l5 -> l3 : __len9^0'=__len9^0, __val8^0'=__val8^0, tmp10^0'=tmp10^0, tmp^0'=tmp^post6, tmp___0^0'=tmp___0^0, tmp___1^0'=tmp___1^post6, T, cost: 1 New rule: l5 -> l3 : tmp^0'=tmp^post6, tmp___1^0'=tmp___1^post6, T, cost: 1 Step with 13 Trace 13[T] Blocked [{}, {}] Step with 10 Trace 13[T], 10[(1+tmp___1^0 <= 0 /\ 1+tmp___1^0 == 0 /\ -1-tmp___1^0 <= 0)] Blocked [{}, {}, {}] Step with 8 Trace 13[T], 10[(1+tmp___1^0 <= 0 /\ 1+tmp___1^0 == 0 /\ -1-tmp___1^0 <= 0)], 8[T] Blocked [{}, {}, {}, {}] Backtrack Trace 13[T], 10[(1+tmp___1^0 <= 0 /\ 1+tmp___1^0 == 0 /\ -1-tmp___1^0 <= 0)] Blocked [{}, {}, {8[T]}] Backtrack Trace 13[T] Blocked [{}, {10[T]}] Step with 11 Trace 13[T], 11[(-tmp___1^0 <= 0)] Blocked [{}, {10[T]}, {}] Step with 9 Trace 13[T], 11[(-tmp___1^0 <= 0)], 9[T] Blocked [{}, {10[T]}, {}, {}] Step with 8 Trace 13[T], 11[(-tmp___1^0 <= 0)], 9[T], 8[T] Blocked [{}, {10[T]}, {}, {}, {}] Backtrack Trace 13[T], 11[(-tmp___1^0 <= 0)], 9[T] Blocked [{}, {10[T]}, {}, {8[T]}] Backtrack Trace 13[T], 11[(-tmp___1^0 <= 0)] Blocked [{}, {10[T]}, {9[T]}] Backtrack Trace 13[T] Blocked [{}, {10[T], 11[T]}] Step with 12 Trace 13[T], 12[(2+tmp___1^0 <= 0)] Blocked [{}, {10[T], 11[T]}, {}] Step with 9 Trace 13[T], 12[(2+tmp___1^0 <= 0)], 9[T] Blocked [{}, {10[T], 11[T]}, {}, {}] Step with 8 Trace 13[T], 12[(2+tmp___1^0 <= 0)], 9[T], 8[T] Blocked [{}, {10[T], 11[T]}, {}, {}, {}] Backtrack Trace 13[T], 12[(2+tmp___1^0 <= 0)], 9[T] Blocked [{}, {10[T], 11[T]}, {}, {8[T]}] Backtrack Trace 13[T], 12[(2+tmp___1^0 <= 0)] Blocked [{}, {10[T], 11[T]}, {9[T]}] Backtrack Trace 13[T] Blocked [{}, {10[T], 11[T], 12[T]}] Backtrack Trace Blocked [{13[T]}] Accept unknown Build SHA: a05f16bf13df659c382799650051f91bf6828c7b