unknown Initial ITS Start location: l8 Program variables: id^0 maxid^0 tmp^0 tmp___0^0 0: l0 -> l1 : id^0'=id^post1, maxid^0'=maxid^post1, tmp^0'=tmp^post1, tmp___0^0'=tmp___0^post1, (tmp^post1 == 0 /\ 1+maxid^0-tmp^0 <= 0 /\ maxid^0-maxid^post1 == 0 /\ -tmp___0^post1+tmp___0^0 == 0 /\ -id^post1+id^0 == 0), cost: 1 1: l0 -> l1 : id^0'=id^post2, maxid^0'=maxid^post2, tmp^0'=tmp^post2, tmp___0^0'=tmp___0^post2, (tmp___0^0-tmp___0^post2 == 0 /\ -maxid^post2+maxid^0 == 0 /\ -maxid^0+tmp^0 <= 0 /\ id^0-id^post2 == 0 /\ -1+tmp^post2-tmp^0 == 0), cost: 1 9: l1 -> l5 : id^0'=id^post10, maxid^0'=maxid^post10, tmp^0'=tmp^post10, tmp___0^0'=tmp___0^post10, (maxid^0-maxid^post10 == 0 /\ tmp___0^0-tmp___0^post10 == 0 /\ id^0-id^post10 == 0 /\ -tmp^post10+tmp^0 == 0), cost: 1 2: l2 -> l3 : id^0'=id^post3, maxid^0'=maxid^post3, tmp^0'=tmp^post3, tmp___0^0'=tmp___0^post3, (-tmp___0^0 <= 0 /\ -maxid^post3+maxid^0 == 0 /\ -id^post3+id^0 == 0 /\ -tmp^post3+tmp^0 == 0 /\ tmp___0^0 <= 0 /\ tmp___0^0-tmp___0^post3 == 0), cost: 1 3: l2 -> l0 : id^0'=id^post4, maxid^0'=maxid^post4, tmp^0'=tmp^post4, tmp___0^0'=tmp___0^post4, (-id^post4+id^0 == 0 /\ 1-tmp___0^0 <= 0 /\ -maxid^post4+maxid^0 == 0 /\ -tmp^post4+tmp^0 == 0 /\ -tmp___0^post4+tmp___0^0 == 0), cost: 1 4: l2 -> l0 : id^0'=id^post5, maxid^0'=maxid^post5, tmp^0'=tmp^post5, tmp___0^0'=tmp___0^post5, (-id^post5+id^0 == 0 /\ -tmp^post5+tmp^0 == 0 /\ maxid^0-maxid^post5 == 0 /\ -tmp___0^post5+tmp___0^0 == 0 /\ 1+tmp___0^0 <= 0), cost: 1 10: l3 -> l6 : id^0'=id^post11, maxid^0'=maxid^post11, tmp^0'=tmp^post11, tmp___0^0'=tmp___0^post11, (-maxid^post11+maxid^0 == 0 /\ tmp___0^0-tmp___0^post11 == 0 /\ id^0-id^post11 == 0 /\ -tmp^post11+tmp^0 == 0), cost: 1 5: l4 -> l2 : id^0'=id^post6, maxid^0'=maxid^post6, tmp^0'=tmp^post6, tmp___0^0'=tmp___0^post6, (0 == 0 /\ maxid^0-maxid^post6 == 0 /\ id^0-id^post6 == 0 /\ -tmp^post6+tmp^0 == 0), cost: 1 6: l5 -> l3 : id^0'=id^post7, maxid^0'=maxid^post7, tmp^0'=tmp^post7, tmp___0^0'=tmp___0^post7, (-tmp^post7+tmp^0 == 0 /\ -id^0+tmp^0 <= 0 /\ id^0-id^post7 == 0 /\ -maxid^post7+maxid^0 == 0 /\ tmp___0^0-tmp___0^post7 == 0 /\ id^0-tmp^0 <= 0), cost: 1 7: l5 -> l4 : id^0'=id^post8, maxid^0'=maxid^post8, tmp^0'=tmp^post8, tmp___0^0'=tmp___0^post8, (-tmp___0^post8+tmp___0^0 == 0 /\ -tmp^post8+tmp^0 == 0 /\ -id^post8+id^0 == 0 /\ -maxid^post8+maxid^0 == 0 /\ 1+id^0-tmp^0 <= 0), cost: 1 8: l5 -> l4 : id^0'=id^post9, maxid^0'=maxid^post9, tmp^0'=tmp^post9, tmp___0^0'=tmp___0^post9, (-tmp^post9+tmp^0 == 0 /\ -tmp___0^post9+tmp___0^0 == 0 /\ -id^post9+id^0 == 0 /\ 1-id^0+tmp^0 <= 0 /\ -maxid^post9+maxid^0 == 0), cost: 1 11: l7 -> l1 : id^0'=id^post12, maxid^0'=maxid^post12, tmp^0'=tmp^post12, tmp___0^0'=tmp___0^post12, (-1-id^0+tmp^post12 == 0 /\ -id^0 <= 0 /\ id^0-maxid^0 <= 0 /\ -tmp___0^post12+tmp___0^0 == 0 /\ -maxid^post12+maxid^0 == 0 /\ -id^post12+id^0 == 0), cost: 1 12: l8 -> l7 : id^0'=id^post13, maxid^0'=maxid^post13, tmp^0'=tmp^post13, tmp___0^0'=tmp___0^post13, (-tmp___0^post13+tmp___0^0 == 0 /\ -id^post13+id^0 == 0 /\ maxid^0-maxid^post13 == 0 /\ -tmp^post13+tmp^0 == 0), cost: 1 Chained Linear Paths Start location: l8 Program variables: id^0 maxid^0 tmp^0 tmp___0^0 0: l0 -> l1 : id^0'=id^post1, maxid^0'=maxid^post1, tmp^0'=tmp^post1, tmp___0^0'=tmp___0^post1, (tmp^post1 == 0 /\ 1+maxid^0-tmp^0 <= 0 /\ maxid^0-maxid^post1 == 0 /\ -tmp___0^post1+tmp___0^0 == 0 /\ -id^post1+id^0 == 0), cost: 1 1: l0 -> l1 : id^0'=id^post2, maxid^0'=maxid^post2, tmp^0'=tmp^post2, tmp___0^0'=tmp___0^post2, (tmp___0^0-tmp___0^post2 == 0 /\ -maxid^post2+maxid^0 == 0 /\ -maxid^0+tmp^0 <= 0 /\ id^0-id^post2 == 0 /\ -1+tmp^post2-tmp^0 == 0), cost: 1 9: l1 -> l5 : id^0'=id^post10, maxid^0'=maxid^post10, tmp^0'=tmp^post10, tmp___0^0'=tmp___0^post10, (maxid^0-maxid^post10 == 0 /\ tmp___0^0-tmp___0^post10 == 0 /\ id^0-id^post10 == 0 /\ -tmp^post10+tmp^0 == 0), cost: 1 2: l2 -> l3 : id^0'=id^post3, maxid^0'=maxid^post3, tmp^0'=tmp^post3, tmp___0^0'=tmp___0^post3, (-tmp___0^0 <= 0 /\ -maxid^post3+maxid^0 == 0 /\ -id^post3+id^0 == 0 /\ -tmp^post3+tmp^0 == 0 /\ tmp___0^0 <= 0 /\ tmp___0^0-tmp___0^post3 == 0), cost: 1 3: l2 -> l0 : id^0'=id^post4, maxid^0'=maxid^post4, tmp^0'=tmp^post4, tmp___0^0'=tmp___0^post4, (-id^post4+id^0 == 0 /\ 1-tmp___0^0 <= 0 /\ -maxid^post4+maxid^0 == 0 /\ -tmp^post4+tmp^0 == 0 /\ -tmp___0^post4+tmp___0^0 == 0), cost: 1 4: l2 -> l0 : id^0'=id^post5, maxid^0'=maxid^post5, tmp^0'=tmp^post5, tmp___0^0'=tmp___0^post5, (-id^post5+id^0 == 0 /\ -tmp^post5+tmp^0 == 0 /\ maxid^0-maxid^post5 == 0 /\ -tmp___0^post5+tmp___0^0 == 0 /\ 1+tmp___0^0 <= 0), cost: 1 10: l3 -> l6 : id^0'=id^post11, maxid^0'=maxid^post11, tmp^0'=tmp^post11, tmp___0^0'=tmp___0^post11, (-maxid^post11+maxid^0 == 0 /\ tmp___0^0-tmp___0^post11 == 0 /\ id^0-id^post11 == 0 /\ -tmp^post11+tmp^0 == 0), cost: 1 5: l4 -> l2 : id^0'=id^post6, maxid^0'=maxid^post6, tmp^0'=tmp^post6, tmp___0^0'=tmp___0^post6, (0 == 0 /\ maxid^0-maxid^post6 == 0 /\ id^0-id^post6 == 0 /\ -tmp^post6+tmp^0 == 0), cost: 1 6: l5 -> l3 : id^0'=id^post7, maxid^0'=maxid^post7, tmp^0'=tmp^post7, tmp___0^0'=tmp___0^post7, (-tmp^post7+tmp^0 == 0 /\ -id^0+tmp^0 <= 0 /\ id^0-id^post7 == 0 /\ -maxid^post7+maxid^0 == 0 /\ tmp___0^0-tmp___0^post7 == 0 /\ id^0-tmp^0 <= 0), cost: 1 7: l5 -> l4 : id^0'=id^post8, maxid^0'=maxid^post8, tmp^0'=tmp^post8, tmp___0^0'=tmp___0^post8, (-tmp___0^post8+tmp___0^0 == 0 /\ -tmp^post8+tmp^0 == 0 /\ -id^post8+id^0 == 0 /\ -maxid^post8+maxid^0 == 0 /\ 1+id^0-tmp^0 <= 0), cost: 1 8: l5 -> l4 : id^0'=id^post9, maxid^0'=maxid^post9, tmp^0'=tmp^post9, tmp___0^0'=tmp___0^post9, (-tmp^post9+tmp^0 == 0 /\ -tmp___0^post9+tmp___0^0 == 0 /\ -id^post9+id^0 == 0 /\ 1-id^0+tmp^0 <= 0 /\ -maxid^post9+maxid^0 == 0), cost: 1 13: l8 -> l1 : id^0'=id^post12, maxid^0'=maxid^post12, tmp^0'=tmp^post12, tmp___0^0'=tmp___0^post12, (-id^post12+id^post13 == 0 /\ -tmp___0^post13+tmp___0^0 == 0 /\ -id^post13+id^0 == 0 /\ id^post13-maxid^post13 <= 0 /\ maxid^0-maxid^post13 == 0 /\ -maxid^post12+maxid^post13 == 0 /\ -id^post13 <= 0 /\ -tmp___0^post12+tmp___0^post13 == 0 /\ -tmp^post13+tmp^0 == 0 /\ -1-id^post13+tmp^post12 == 0), cost: 1 Eliminating location l7 by chaining: Applied chaining First rule: l8 -> l7 : id^0'=id^post13, maxid^0'=maxid^post13, tmp^0'=tmp^post13, tmp___0^0'=tmp___0^post13, (-tmp___0^post13+tmp___0^0 == 0 /\ -id^post13+id^0 == 0 /\ maxid^0-maxid^post13 == 0 /\ -tmp^post13+tmp^0 == 0), cost: 1 Second rule: l7 -> l1 : id^0'=id^post12, maxid^0'=maxid^post12, tmp^0'=tmp^post12, tmp___0^0'=tmp___0^post12, (-1-id^0+tmp^post12 == 0 /\ -id^0 <= 0 /\ id^0-maxid^0 <= 0 /\ -tmp___0^post12+tmp___0^0 == 0 /\ -maxid^post12+maxid^0 == 0 /\ -id^post12+id^0 == 0), cost: 1 New rule: l8 -> l1 : id^0'=id^post12, maxid^0'=maxid^post12, tmp^0'=tmp^post12, tmp___0^0'=tmp___0^post12, (-id^post12+id^post13 == 0 /\ -tmp___0^post13+tmp___0^0 == 0 /\ -id^post13+id^0 == 0 /\ id^post13-maxid^post13 <= 0 /\ maxid^0-maxid^post13 == 0 /\ -maxid^post12+maxid^post13 == 0 /\ -id^post13 <= 0 /\ -tmp___0^post12+tmp___0^post13 == 0 /\ -tmp^post13+tmp^0 == 0 /\ -1-id^post13+tmp^post12 == 0), cost: 1 Applied deletion Removed the following rules: 11 12 Simplified Transitions Start location: l8 Program variables: id^0 maxid^0 tmp^0 tmp___0^0 14: l0 -> l1 : tmp^0'=0, 1+maxid^0-tmp^0 <= 0, cost: 1 15: l0 -> l1 : tmp^0'=1+tmp^0, -maxid^0+tmp^0 <= 0, cost: 1 23: l1 -> l5 : T, cost: 1 16: l2 -> l3 : (-tmp___0^0 <= 0 /\ -tmp___0^0 == 0 /\ tmp___0^0 <= 0), cost: 1 17: l2 -> l0 : 1-tmp___0^0 <= 0, cost: 1 18: l2 -> l0 : 1+tmp___0^0 <= 0, cost: 1 24: l3 -> l6 : T, cost: 1 19: l4 -> l2 : tmp___0^0'=tmp___0^post6, T, cost: 1 20: l5 -> l3 : (-id^0+tmp^0 <= 0 /\ -id^0+tmp^0 == 0 /\ id^0-tmp^0 <= 0), cost: 1 21: l5 -> l4 : 1+id^0-tmp^0 <= 0, cost: 1 22: l5 -> l4 : 1-id^0+tmp^0 <= 0, cost: 1 25: l8 -> l1 : tmp^0'=1+id^0, (-id^0 <= 0 /\ id^0-maxid^0 <= 0), cost: 1 Propagated Equalities Original rule: l0 -> l1 : id^0'=id^post1, maxid^0'=maxid^post1, tmp^0'=tmp^post1, tmp___0^0'=tmp___0^post1, (tmp^post1 == 0 /\ 1+maxid^0-tmp^0 <= 0 /\ maxid^0-maxid^post1 == 0 /\ -tmp___0^post1+tmp___0^0 == 0 /\ -id^post1+id^0 == 0), cost: 1 New rule: l0 -> l1 : id^0'=id^0, maxid^0'=maxid^0, tmp^0'=0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 1+maxid^0-tmp^0 <= 0), cost: 1 propagated equality tmp^post1 = 0 propagated equality maxid^post1 = maxid^0 propagated equality tmp___0^post1 = tmp___0^0 propagated equality id^post1 = id^0 Simplified Guard Original rule: l0 -> l1 : id^0'=id^0, maxid^0'=maxid^0, tmp^0'=0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 1+maxid^0-tmp^0 <= 0), cost: 1 New rule: l0 -> l1 : id^0'=id^0, maxid^0'=maxid^0, tmp^0'=0, tmp___0^0'=tmp___0^0, 1+maxid^0-tmp^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l0 -> l1 : id^0'=id^0, maxid^0'=maxid^0, tmp^0'=0, tmp___0^0'=tmp___0^0, 1+maxid^0-tmp^0 <= 0, cost: 1 New rule: l0 -> l1 : tmp^0'=0, 1+maxid^0-tmp^0 <= 0, cost: 1 Propagated Equalities Original rule: l0 -> l1 : id^0'=id^post2, maxid^0'=maxid^post2, tmp^0'=tmp^post2, tmp___0^0'=tmp___0^post2, (tmp___0^0-tmp___0^post2 == 0 /\ -maxid^post2+maxid^0 == 0 /\ -maxid^0+tmp^0 <= 0 /\ id^0-id^post2 == 0 /\ -1+tmp^post2-tmp^0 == 0), cost: 1 New rule: l0 -> l1 : id^0'=id^0, maxid^0'=maxid^0, tmp^0'=1+tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ -maxid^0+tmp^0 <= 0), cost: 1 propagated equality tmp___0^post2 = tmp___0^0 propagated equality maxid^post2 = maxid^0 propagated equality id^post2 = id^0 propagated equality tmp^post2 = 1+tmp^0 Simplified Guard Original rule: l0 -> l1 : id^0'=id^0, maxid^0'=maxid^0, tmp^0'=1+tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ -maxid^0+tmp^0 <= 0), cost: 1 New rule: l0 -> l1 : id^0'=id^0, maxid^0'=maxid^0, tmp^0'=1+tmp^0, tmp___0^0'=tmp___0^0, -maxid^0+tmp^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l0 -> l1 : id^0'=id^0, maxid^0'=maxid^0, tmp^0'=1+tmp^0, tmp___0^0'=tmp___0^0, -maxid^0+tmp^0 <= 0, cost: 1 New rule: l0 -> l1 : tmp^0'=1+tmp^0, -maxid^0+tmp^0 <= 0, cost: 1 made implied equalities explicit Original rule: l2 -> l3 : id^0'=id^post3, maxid^0'=maxid^post3, tmp^0'=tmp^post3, tmp___0^0'=tmp___0^post3, (-tmp___0^0 <= 0 /\ -maxid^post3+maxid^0 == 0 /\ -id^post3+id^0 == 0 /\ -tmp^post3+tmp^0 == 0 /\ tmp___0^0 <= 0 /\ tmp___0^0-tmp___0^post3 == 0), cost: 1 New rule: l2 -> l3 : id^0'=id^post3, maxid^0'=maxid^post3, tmp^0'=tmp^post3, tmp___0^0'=tmp___0^post3, (-tmp___0^0 <= 0 /\ -tmp___0^0 == 0 /\ -maxid^post3+maxid^0 == 0 /\ -id^post3+id^0 == 0 /\ -tmp^post3+tmp^0 == 0 /\ tmp___0^0 <= 0 /\ tmp___0^0-tmp___0^post3 == 0), cost: 1 Propagated Equalities Original rule: l2 -> l3 : id^0'=id^post3, maxid^0'=maxid^post3, tmp^0'=tmp^post3, tmp___0^0'=tmp___0^post3, (-tmp___0^0 <= 0 /\ -tmp___0^0 == 0 /\ -maxid^post3+maxid^0 == 0 /\ -id^post3+id^0 == 0 /\ -tmp^post3+tmp^0 == 0 /\ tmp___0^0 <= 0 /\ tmp___0^0-tmp___0^post3 == 0), cost: 1 New rule: l2 -> l3 : id^0'=id^0, maxid^0'=maxid^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ -tmp___0^0 <= 0 /\ -tmp___0^0 == 0 /\ tmp___0^0 <= 0), cost: 1 propagated equality maxid^post3 = maxid^0 propagated equality id^post3 = id^0 propagated equality tmp^post3 = tmp^0 propagated equality tmp___0^post3 = tmp___0^0 Simplified Guard Original rule: l2 -> l3 : id^0'=id^0, maxid^0'=maxid^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ -tmp___0^0 <= 0 /\ -tmp___0^0 == 0 /\ tmp___0^0 <= 0), cost: 1 New rule: l2 -> l3 : id^0'=id^0, maxid^0'=maxid^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (-tmp___0^0 <= 0 /\ -tmp___0^0 == 0 /\ tmp___0^0 <= 0), cost: 1 made implied equalities explicit Original rule: l2 -> l3 : id^0'=id^0, maxid^0'=maxid^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (-tmp___0^0 <= 0 /\ -tmp___0^0 == 0 /\ tmp___0^0 <= 0), cost: 1 New rule: l2 -> l3 : id^0'=id^0, maxid^0'=maxid^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (-tmp___0^0 <= 0 /\ -tmp___0^0 == 0 /\ tmp___0^0 <= 0), cost: 1 Removed Trivial Updates Original rule: l2 -> l3 : id^0'=id^0, maxid^0'=maxid^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (-tmp___0^0 <= 0 /\ -tmp___0^0 == 0 /\ tmp___0^0 <= 0), cost: 1 New rule: l2 -> l3 : (-tmp___0^0 <= 0 /\ -tmp___0^0 == 0 /\ tmp___0^0 <= 0), cost: 1 Propagated Equalities Original rule: l2 -> l0 : id^0'=id^post4, maxid^0'=maxid^post4, tmp^0'=tmp^post4, tmp___0^0'=tmp___0^post4, (-id^post4+id^0 == 0 /\ 1-tmp___0^0 <= 0 /\ -maxid^post4+maxid^0 == 0 /\ -tmp^post4+tmp^0 == 0 /\ -tmp___0^post4+tmp___0^0 == 0), cost: 1 New rule: l2 -> l0 : id^0'=id^0, maxid^0'=maxid^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 1-tmp___0^0 <= 0), cost: 1 propagated equality id^post4 = id^0 propagated equality maxid^post4 = maxid^0 propagated equality tmp^post4 = tmp^0 propagated equality tmp___0^post4 = tmp___0^0 Simplified Guard Original rule: l2 -> l0 : id^0'=id^0, maxid^0'=maxid^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 1-tmp___0^0 <= 0), cost: 1 New rule: l2 -> l0 : id^0'=id^0, maxid^0'=maxid^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 1-tmp___0^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l2 -> l0 : id^0'=id^0, maxid^0'=maxid^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 1-tmp___0^0 <= 0, cost: 1 New rule: l2 -> l0 : 1-tmp___0^0 <= 0, cost: 1 Propagated Equalities Original rule: l2 -> l0 : id^0'=id^post5, maxid^0'=maxid^post5, tmp^0'=tmp^post5, tmp___0^0'=tmp___0^post5, (-id^post5+id^0 == 0 /\ -tmp^post5+tmp^0 == 0 /\ maxid^0-maxid^post5 == 0 /\ -tmp___0^post5+tmp___0^0 == 0 /\ 1+tmp___0^0 <= 0), cost: 1 New rule: l2 -> l0 : id^0'=id^0, maxid^0'=maxid^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 1+tmp___0^0 <= 0), cost: 1 propagated equality id^post5 = id^0 propagated equality tmp^post5 = tmp^0 propagated equality maxid^post5 = maxid^0 propagated equality tmp___0^post5 = tmp___0^0 Simplified Guard Original rule: l2 -> l0 : id^0'=id^0, maxid^0'=maxid^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 1+tmp___0^0 <= 0), cost: 1 New rule: l2 -> l0 : id^0'=id^0, maxid^0'=maxid^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 1+tmp___0^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l2 -> l0 : id^0'=id^0, maxid^0'=maxid^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 1+tmp___0^0 <= 0, cost: 1 New rule: l2 -> l0 : 1+tmp___0^0 <= 0, cost: 1 Propagated Equalities Original rule: l4 -> l2 : id^0'=id^post6, maxid^0'=maxid^post6, tmp^0'=tmp^post6, tmp___0^0'=tmp___0^post6, (0 == 0 /\ maxid^0-maxid^post6 == 0 /\ id^0-id^post6 == 0 /\ -tmp^post6+tmp^0 == 0), cost: 1 New rule: l4 -> l2 : id^0'=id^0, maxid^0'=maxid^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^post6, 0 == 0, cost: 1 propagated equality maxid^post6 = maxid^0 propagated equality id^post6 = id^0 propagated equality tmp^post6 = tmp^0 Simplified Guard Original rule: l4 -> l2 : id^0'=id^0, maxid^0'=maxid^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^post6, 0 == 0, cost: 1 New rule: l4 -> l2 : id^0'=id^0, maxid^0'=maxid^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^post6, T, cost: 1 Removed Trivial Updates Original rule: l4 -> l2 : id^0'=id^0, maxid^0'=maxid^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^post6, T, cost: 1 New rule: l4 -> l2 : tmp___0^0'=tmp___0^post6, T, cost: 1 made implied equalities explicit Original rule: l5 -> l3 : id^0'=id^post7, maxid^0'=maxid^post7, tmp^0'=tmp^post7, tmp___0^0'=tmp___0^post7, (-tmp^post7+tmp^0 == 0 /\ -id^0+tmp^0 <= 0 /\ id^0-id^post7 == 0 /\ -maxid^post7+maxid^0 == 0 /\ tmp___0^0-tmp___0^post7 == 0 /\ id^0-tmp^0 <= 0), cost: 1 New rule: l5 -> l3 : id^0'=id^post7, maxid^0'=maxid^post7, tmp^0'=tmp^post7, tmp___0^0'=tmp___0^post7, (-tmp^post7+tmp^0 == 0 /\ -id^0+tmp^0 <= 0 /\ -id^0+tmp^0 == 0 /\ id^0-id^post7 == 0 /\ -maxid^post7+maxid^0 == 0 /\ tmp___0^0-tmp___0^post7 == 0 /\ id^0-tmp^0 <= 0), cost: 1 Propagated Equalities Original rule: l5 -> l3 : id^0'=id^post7, maxid^0'=maxid^post7, tmp^0'=tmp^post7, tmp___0^0'=tmp___0^post7, (-tmp^post7+tmp^0 == 0 /\ -id^0+tmp^0 <= 0 /\ -id^0+tmp^0 == 0 /\ id^0-id^post7 == 0 /\ -maxid^post7+maxid^0 == 0 /\ tmp___0^0-tmp___0^post7 == 0 /\ id^0-tmp^0 <= 0), cost: 1 New rule: l5 -> l3 : id^0'=id^0, maxid^0'=maxid^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ -id^0+tmp^0 <= 0 /\ -id^0+tmp^0 == 0 /\ id^0-tmp^0 <= 0), cost: 1 propagated equality tmp^post7 = tmp^0 propagated equality id^post7 = id^0 propagated equality maxid^post7 = maxid^0 propagated equality tmp___0^post7 = tmp___0^0 Simplified Guard Original rule: l5 -> l3 : id^0'=id^0, maxid^0'=maxid^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ -id^0+tmp^0 <= 0 /\ -id^0+tmp^0 == 0 /\ id^0-tmp^0 <= 0), cost: 1 New rule: l5 -> l3 : id^0'=id^0, maxid^0'=maxid^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (-id^0+tmp^0 <= 0 /\ -id^0+tmp^0 == 0 /\ id^0-tmp^0 <= 0), cost: 1 made implied equalities explicit Original rule: l5 -> l3 : id^0'=id^0, maxid^0'=maxid^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (-id^0+tmp^0 <= 0 /\ -id^0+tmp^0 == 0 /\ id^0-tmp^0 <= 0), cost: 1 New rule: l5 -> l3 : id^0'=id^0, maxid^0'=maxid^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (-id^0+tmp^0 <= 0 /\ -id^0+tmp^0 == 0 /\ id^0-tmp^0 <= 0), cost: 1 Removed Trivial Updates Original rule: l5 -> l3 : id^0'=id^0, maxid^0'=maxid^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (-id^0+tmp^0 <= 0 /\ -id^0+tmp^0 == 0 /\ id^0-tmp^0 <= 0), cost: 1 New rule: l5 -> l3 : (-id^0+tmp^0 <= 0 /\ -id^0+tmp^0 == 0 /\ id^0-tmp^0 <= 0), cost: 1 Propagated Equalities Original rule: l5 -> l4 : id^0'=id^post8, maxid^0'=maxid^post8, tmp^0'=tmp^post8, tmp___0^0'=tmp___0^post8, (-tmp___0^post8+tmp___0^0 == 0 /\ -tmp^post8+tmp^0 == 0 /\ -id^post8+id^0 == 0 /\ -maxid^post8+maxid^0 == 0 /\ 1+id^0-tmp^0 <= 0), cost: 1 New rule: l5 -> l4 : id^0'=id^0, maxid^0'=maxid^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 1+id^0-tmp^0 <= 0), cost: 1 propagated equality tmp___0^post8 = tmp___0^0 propagated equality tmp^post8 = tmp^0 propagated equality id^post8 = id^0 propagated equality maxid^post8 = maxid^0 Simplified Guard Original rule: l5 -> l4 : id^0'=id^0, maxid^0'=maxid^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 1+id^0-tmp^0 <= 0), cost: 1 New rule: l5 -> l4 : id^0'=id^0, maxid^0'=maxid^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 1+id^0-tmp^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l5 -> l4 : id^0'=id^0, maxid^0'=maxid^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 1+id^0-tmp^0 <= 0, cost: 1 New rule: l5 -> l4 : 1+id^0-tmp^0 <= 0, cost: 1 Propagated Equalities Original rule: l5 -> l4 : id^0'=id^post9, maxid^0'=maxid^post9, tmp^0'=tmp^post9, tmp___0^0'=tmp___0^post9, (-tmp^post9+tmp^0 == 0 /\ -tmp___0^post9+tmp___0^0 == 0 /\ -id^post9+id^0 == 0 /\ 1-id^0+tmp^0 <= 0 /\ -maxid^post9+maxid^0 == 0), cost: 1 New rule: l5 -> l4 : id^0'=id^0, maxid^0'=maxid^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 1-id^0+tmp^0 <= 0), cost: 1 propagated equality tmp^post9 = tmp^0 propagated equality tmp___0^post9 = tmp___0^0 propagated equality id^post9 = id^0 propagated equality maxid^post9 = maxid^0 Simplified Guard Original rule: l5 -> l4 : id^0'=id^0, maxid^0'=maxid^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ 1-id^0+tmp^0 <= 0), cost: 1 New rule: l5 -> l4 : id^0'=id^0, maxid^0'=maxid^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 1-id^0+tmp^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l5 -> l4 : id^0'=id^0, maxid^0'=maxid^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 1-id^0+tmp^0 <= 0, cost: 1 New rule: l5 -> l4 : 1-id^0+tmp^0 <= 0, cost: 1 Propagated Equalities Original rule: l1 -> l5 : id^0'=id^post10, maxid^0'=maxid^post10, tmp^0'=tmp^post10, tmp___0^0'=tmp___0^post10, (maxid^0-maxid^post10 == 0 /\ tmp___0^0-tmp___0^post10 == 0 /\ id^0-id^post10 == 0 /\ -tmp^post10+tmp^0 == 0), cost: 1 New rule: l1 -> l5 : id^0'=id^0, maxid^0'=maxid^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1 propagated equality maxid^post10 = maxid^0 propagated equality tmp___0^post10 = tmp___0^0 propagated equality id^post10 = id^0 propagated equality tmp^post10 = tmp^0 Simplified Guard Original rule: l1 -> l5 : id^0'=id^0, maxid^0'=maxid^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1 New rule: l1 -> l5 : id^0'=id^0, maxid^0'=maxid^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1 Removed Trivial Updates Original rule: l1 -> l5 : id^0'=id^0, maxid^0'=maxid^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1 New rule: l1 -> l5 : T, cost: 1 Propagated Equalities Original rule: l3 -> l6 : id^0'=id^post11, maxid^0'=maxid^post11, tmp^0'=tmp^post11, tmp___0^0'=tmp___0^post11, (-maxid^post11+maxid^0 == 0 /\ tmp___0^0-tmp___0^post11 == 0 /\ id^0-id^post11 == 0 /\ -tmp^post11+tmp^0 == 0), cost: 1 New rule: l3 -> l6 : id^0'=id^0, maxid^0'=maxid^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1 propagated equality maxid^post11 = maxid^0 propagated equality tmp___0^post11 = tmp___0^0 propagated equality id^post11 = id^0 propagated equality tmp^post11 = tmp^0 Simplified Guard Original rule: l3 -> l6 : id^0'=id^0, maxid^0'=maxid^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, 0 == 0, cost: 1 New rule: l3 -> l6 : id^0'=id^0, maxid^0'=maxid^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1 Removed Trivial Updates Original rule: l3 -> l6 : id^0'=id^0, maxid^0'=maxid^0, tmp^0'=tmp^0, tmp___0^0'=tmp___0^0, T, cost: 1 New rule: l3 -> l6 : T, cost: 1 Propagated Equalities Original rule: l8 -> l1 : id^0'=id^post12, maxid^0'=maxid^post12, tmp^0'=tmp^post12, tmp___0^0'=tmp___0^post12, (-id^post12+id^post13 == 0 /\ -tmp___0^post13+tmp___0^0 == 0 /\ -id^post13+id^0 == 0 /\ id^post13-maxid^post13 <= 0 /\ maxid^0-maxid^post13 == 0 /\ -maxid^post12+maxid^post13 == 0 /\ -id^post13 <= 0 /\ -tmp___0^post12+tmp___0^post13 == 0 /\ -tmp^post13+tmp^0 == 0 /\ -1-id^post13+tmp^post12 == 0), cost: 1 New rule: l8 -> l1 : id^0'=id^post13, maxid^0'=maxid^post13, tmp^0'=1+id^post13, tmp___0^0'=tmp___0^post13, (0 == 0 /\ -tmp___0^post13+tmp___0^0 == 0 /\ -id^post13+id^0 == 0 /\ id^post13-maxid^post13 <= 0 /\ maxid^0-maxid^post13 == 0 /\ -id^post13 <= 0 /\ -tmp^post13+tmp^0 == 0), cost: 1 propagated equality id^post12 = id^post13 propagated equality maxid^post12 = maxid^post13 propagated equality tmp___0^post12 = tmp___0^post13 propagated equality tmp^post12 = 1+id^post13 Propagated Equalities Original rule: l8 -> l1 : id^0'=id^post13, maxid^0'=maxid^post13, tmp^0'=1+id^post13, tmp___0^0'=tmp___0^post13, (0 == 0 /\ -tmp___0^post13+tmp___0^0 == 0 /\ -id^post13+id^0 == 0 /\ id^post13-maxid^post13 <= 0 /\ maxid^0-maxid^post13 == 0 /\ -id^post13 <= 0 /\ -tmp^post13+tmp^0 == 0), cost: 1 New rule: l8 -> l1 : id^0'=id^0, maxid^0'=maxid^0, tmp^0'=1+id^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ -id^0 <= 0 /\ id^0-maxid^0 <= 0), cost: 1 propagated equality tmp___0^post13 = tmp___0^0 propagated equality id^post13 = id^0 propagated equality maxid^post13 = maxid^0 propagated equality tmp^post13 = tmp^0 Simplified Guard Original rule: l8 -> l1 : id^0'=id^0, maxid^0'=maxid^0, tmp^0'=1+id^0, tmp___0^0'=tmp___0^0, (0 == 0 /\ -id^0 <= 0 /\ id^0-maxid^0 <= 0), cost: 1 New rule: l8 -> l1 : id^0'=id^0, maxid^0'=maxid^0, tmp^0'=1+id^0, tmp___0^0'=tmp___0^0, (-id^0 <= 0 /\ id^0-maxid^0 <= 0), cost: 1 Removed Trivial Updates Original rule: l8 -> l1 : id^0'=id^0, maxid^0'=maxid^0, tmp^0'=1+id^0, tmp___0^0'=tmp___0^0, (-id^0 <= 0 /\ id^0-maxid^0 <= 0), cost: 1 New rule: l8 -> l1 : tmp^0'=1+id^0, (-id^0 <= 0 /\ id^0-maxid^0 <= 0), cost: 1 Step with 25 Trace 25[(-id^0 <= 0 /\ id^0-maxid^0 <= 0)] Blocked [{}, {}] Step with 23 Trace 25[(-id^0 <= 0 /\ id^0-maxid^0 <= 0)], 23[T] Blocked [{}, {}, {}] Step with 21 Trace 25[(-id^0 <= 0 /\ id^0-maxid^0 <= 0)], 23[T], 21[(1+id^0-tmp^0 <= 0)] Blocked [{}, {}, {20[T]}, {}] Step with 19 Trace 25[(-id^0 <= 0 /\ id^0-maxid^0 <= 0)], 23[T], 21[(1+id^0-tmp^0 <= 0)], 19[T] Blocked [{}, {}, {20[T]}, {}, {}] Step with 16 Trace 25[(-id^0 <= 0 /\ id^0-maxid^0 <= 0)], 23[T], 21[(1+id^0-tmp^0 <= 0)], 19[T], 16[(-tmp___0^0 <= 0 /\ -tmp___0^0 == 0 /\ tmp___0^0 <= 0)] Blocked [{}, {}, {20[T]}, {}, {}, {}] Step with 24 Trace 25[(-id^0 <= 0 /\ id^0-maxid^0 <= 0)], 23[T], 21[(1+id^0-tmp^0 <= 0)], 19[T], 16[(-tmp___0^0 <= 0 /\ -tmp___0^0 == 0 /\ tmp___0^0 <= 0)], 24[T] Blocked [{}, {}, {20[T]}, {}, {}, {}, {}] Backtrack Trace 25[(-id^0 <= 0 /\ id^0-maxid^0 <= 0)], 23[T], 21[(1+id^0-tmp^0 <= 0)], 19[T], 16[(-tmp___0^0 <= 0 /\ -tmp___0^0 == 0 /\ tmp___0^0 <= 0)] Blocked [{}, {}, {20[T]}, {}, {}, {24[T]}] Backtrack Trace 25[(-id^0 <= 0 /\ id^0-maxid^0 <= 0)], 23[T], 21[(1+id^0-tmp^0 <= 0)], 19[T] Blocked [{}, {}, {20[T]}, {}, {16[T]}] Step with 17 Trace 25[(-id^0 <= 0 /\ id^0-maxid^0 <= 0)], 23[T], 21[(1+id^0-tmp^0 <= 0)], 19[T], 17[(1-tmp___0^0 <= 0)] Blocked [{}, {}, {20[T]}, {}, {16[T]}, {}] Step with 14 Trace 25[(-id^0 <= 0 /\ id^0-maxid^0 <= 0)], 23[T], 21[(1+id^0-tmp^0 <= 0)], 19[T], 17[(1-tmp___0^0 <= 0)], 14[(1+maxid^0-tmp^0 <= 0)] Blocked [{}, {}, {20[T]}, {}, {16[T]}, {}, {}] Accelerate and Drop Start location: l8 Program variables: id^0 maxid^0 tmp^0 tmp___0^0 14: l0 -> l1 : tmp^0'=0, 1+maxid^0-tmp^0 <= 0, cost: 1 15: l0 -> l1 : tmp^0'=1+tmp^0, -maxid^0+tmp^0 <= 0, cost: 1 23: l1 -> l5 : T, cost: 1 26: l1 -> LoAT_sink : (-1+tmp___0^post61 >= 0 /\ -1-id^0+tmp^0 >= 0 /\ -1-maxid^0+tmp^0 >= 0 /\ tmp^0 <= 0), cost: NONTERM 16: l2 -> l3 : (-tmp___0^0 <= 0 /\ -tmp___0^0 == 0 /\ tmp___0^0 <= 0), cost: 1 17: l2 -> l0 : 1-tmp___0^0 <= 0, cost: 1 18: l2 -> l0 : 1+tmp___0^0 <= 0, cost: 1 24: l3 -> l6 : T, cost: 1 19: l4 -> l2 : tmp___0^0'=tmp___0^post6, T, cost: 1 20: l5 -> l3 : (-id^0+tmp^0 <= 0 /\ -id^0+tmp^0 == 0 /\ id^0-tmp^0 <= 0), cost: 1 21: l5 -> l4 : 1+id^0-tmp^0 <= 0, cost: 1 22: l5 -> l4 : 1-id^0+tmp^0 <= 0, cost: 1 25: l8 -> l1 : tmp^0'=1+id^0, (-id^0 <= 0 /\ id^0-maxid^0 <= 0), cost: 1 Certificate of Non-Termination Original rule: l1 -> l1 : tmp^0'=0, tmp___0^0'=tmp___0^post61, (1-tmp___0^post61 <= 0 /\ 1+maxid^0-tmp^0 <= 0 /\ 1+id^0-tmp^0 <= 0), cost: 1 New rule: l1 -> LoAT_sink : (-1+tmp___0^post61 >= 0 /\ -1-id^0+tmp^0 >= 0 /\ -1-maxid^0+tmp^0 >= 0 /\ tmp^0 <= 0), cost: NONTERM -1+tmp___0^post61 >= 0 [0]: monotonic increase yields -1+tmp___0^post61 >= 0 -1-id^0+tmp^0 >= 0 [0]: eventual decrease yields (-1-id^0+tmp^0 >= 0 /\ -1-id^0 >= 0) -1-id^0+tmp^0 >= 0 [1]: eventual increase yields (-1-id^0+tmp^0 >= 0 /\ tmp^0 <= 0) -1-maxid^0+tmp^0 >= 0 [0]: eventual decrease yields (-1-maxid^0 >= 0 /\ -1-maxid^0+tmp^0 >= 0) -1-maxid^0+tmp^0 >= 0 [1]: eventual increase yields (-1-maxid^0+tmp^0 >= 0 /\ tmp^0 <= 0) Replacement map: {-1+tmp___0^post61 >= 0 -> -1+tmp___0^post61 >= 0, -1-id^0+tmp^0 >= 0 -> (-1-id^0+tmp^0 >= 0 /\ tmp^0 <= 0), -1-maxid^0+tmp^0 >= 0 -> (-1-maxid^0+tmp^0 >= 0 /\ tmp^0 <= 0)} Trace 25[(-id^0 <= 0 /\ id^0-maxid^0 <= 0)] Blocked [{}, {23[T]}] Backtrack Trace Blocked [{25[T]}] Accept unknown Build SHA: a05f16bf13df659c382799650051f91bf6828c7b