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