NO Initial ITS Start location: l12 Program variables: ___rho_2_^0 ___rho_3_^0 ___rho_4_^0 ___rho_5_^0 a22^0 curtime^0 got_sighup^0 last_copy_time^0 tt1^0 wakend^0 0: l0 -> l1 : ___rho_2_^0'=___rho_2_^post1, ___rho_3_^0'=___rho_3_^post1, ___rho_4_^0'=___rho_4_^post1, ___rho_5_^0'=___rho_5_^post1, a22^0'=a22^post1, curtime^0'=curtime^post1, got_sighup^0'=got_sighup^post1, last_copy_time^0'=last_copy_time^post1, tt1^0'=tt1^post1, wakend^0'=wakend^post1, (-___rho_5_^post1+___rho_5_^0 == 0 /\ -___rho_3_^post1+___rho_3_^0 == 0 /\ ___rho_4_^0-___rho_4_^post1 == 0 /\ curtime^0-curtime^post1 == 0 /\ got_sighup^0 <= 0 /\ a22^0-a22^post1 == 0 /\ -___rho_2_^post1+___rho_2_^0 == 0 /\ last_copy_time^0-last_copy_time^post1 == 0 /\ -tt1^post1+tt1^0 == 0 /\ wakend^0-wakend^post1 == 0 /\ -got_sighup^post1+got_sighup^0 == 0), cost: 1 1: l0 -> l2 : ___rho_2_^0'=___rho_2_^post2, ___rho_3_^0'=___rho_3_^post2, ___rho_4_^0'=___rho_4_^post2, ___rho_5_^0'=___rho_5_^post2, a22^0'=a22^post2, curtime^0'=curtime^post2, got_sighup^0'=got_sighup^post2, last_copy_time^0'=last_copy_time^post2, tt1^0'=tt1^post2, wakend^0'=wakend^post2, (0 == 0 /\ ___rho_4_^0-___rho_4_^post2 == 0 /\ got_sighup^post2 == 0 /\ -___rho_5_^post2+___rho_5_^0 == 0 /\ 1-got_sighup^0 <= 0 /\ -___rho_3_^post2+tt1^post2 == 0 /\ -wakend^post2+wakend^0 == 0 /\ curtime^0-curtime^post2 == 0 /\ -___rho_2_^post2+___rho_2_^0 == 0 /\ last_copy_time^0-last_copy_time^post2 == 0 /\ -1+a22^post2 == 0), cost: 1 11: l1 -> l9 : ___rho_2_^0'=___rho_2_^post12, ___rho_3_^0'=___rho_3_^post12, ___rho_4_^0'=___rho_4_^post12, ___rho_5_^0'=___rho_5_^post12, a22^0'=a22^post12, curtime^0'=curtime^post12, got_sighup^0'=got_sighup^post12, last_copy_time^0'=last_copy_time^post12, tt1^0'=tt1^post12, wakend^0'=wakend^post12, (curtime^0-curtime^post12 == 0 /\ got_sighup^0-got_sighup^post12 == 0 /\ -tt1^post12+tt1^0 == 0 /\ wakend^0 <= 0 /\ last_copy_time^0-last_copy_time^post12 == 0 /\ -___rho_3_^post12+___rho_3_^0 == 0 /\ wakend^0-wakend^post12 == 0 /\ ___rho_5_^0-___rho_5_^post12 == 0 /\ -a22^post12+a22^0 == 0 /\ ___rho_4_^0-___rho_4_^post12 == 0 /\ -___rho_2_^post12+___rho_2_^0 == 0), cost: 1 12: l1 -> l9 : ___rho_2_^0'=___rho_2_^post13, ___rho_3_^0'=___rho_3_^post13, ___rho_4_^0'=___rho_4_^post13, ___rho_5_^0'=___rho_5_^post13, a22^0'=a22^post13, curtime^0'=curtime^post13, got_sighup^0'=got_sighup^post13, last_copy_time^0'=last_copy_time^post13, tt1^0'=tt1^post13, wakend^0'=wakend^post13, (0 == 0 /\ wakend^post13 == 0 /\ -got_sighup^post13+got_sighup^0 == 0 /\ -___rho_2_^post13+___rho_2_^0 == 0 /\ -___rho_3_^post13+___rho_3_^0 == 0 /\ -___rho_5_^post13+___rho_5_^0 == 0 /\ a22^0-a22^post13 == 0 /\ last_copy_time^post13-___rho_4_^post13 == 0 /\ -tt1^post13+tt1^0 == 0 /\ curtime^0-curtime^post13 == 0 /\ 1-wakend^0 <= 0), cost: 1 13: l2 -> l1 : ___rho_2_^0'=___rho_2_^post14, ___rho_3_^0'=___rho_3_^post14, ___rho_4_^0'=___rho_4_^post14, ___rho_5_^0'=___rho_5_^post14, a22^0'=a22^post14, curtime^0'=curtime^post14, got_sighup^0'=got_sighup^post14, last_copy_time^0'=last_copy_time^post14, tt1^0'=tt1^post14, wakend^0'=wakend^post14, (-got_sighup^post14+got_sighup^0 == 0 /\ ___rho_3_^0-___rho_3_^post14 == 0 /\ ___rho_4_^0-___rho_4_^post14 == 0 /\ 1-tt1^0 <= 0 /\ -___rho_5_^post14+___rho_5_^0 == 0 /\ -___rho_2_^post14+___rho_2_^0 == 0 /\ a22^0-a22^post14 == 0 /\ -wakend^post14+wakend^0 == 0 /\ -tt1^post14+tt1^0 == 0 /\ last_copy_time^0-last_copy_time^post14 == 0 /\ curtime^0-curtime^post14 == 0), cost: 1 14: l2 -> l5 : ___rho_2_^0'=___rho_2_^post15, ___rho_3_^0'=___rho_3_^post15, ___rho_4_^0'=___rho_4_^post15, ___rho_5_^0'=___rho_5_^post15, a22^0'=a22^post15, curtime^0'=curtime^post15, got_sighup^0'=got_sighup^post15, last_copy_time^0'=last_copy_time^post15, tt1^0'=tt1^post15, wakend^0'=wakend^post15, (tt1^0-tt1^post15 == 0 /\ ___rho_3_^0-___rho_3_^post15 == 0 /\ ___rho_4_^0-___rho_4_^post15 == 0 /\ -___rho_5_^post15+___rho_5_^0 == 0 /\ -___rho_2_^post15+___rho_2_^0 == 0 /\ curtime^0-curtime^post15 == 0 /\ a22^0-a22^post15 == 0 /\ tt1^0 <= 0 /\ -got_sighup^post15+got_sighup^0 == 0 /\ -wakend^post15+wakend^0 == 0 /\ last_copy_time^0-last_copy_time^post15 == 0), cost: 1 2: l3 -> l4 : ___rho_2_^0'=___rho_2_^post3, ___rho_3_^0'=___rho_3_^post3, ___rho_4_^0'=___rho_4_^post3, ___rho_5_^0'=___rho_5_^post3, a22^0'=a22^post3, curtime^0'=curtime^post3, got_sighup^0'=got_sighup^post3, last_copy_time^0'=last_copy_time^post3, tt1^0'=tt1^post3, wakend^0'=wakend^post3, (last_copy_time^0-last_copy_time^post3 == 0 /\ -got_sighup^post3+got_sighup^0 == 0 /\ ___rho_3_^0-___rho_3_^post3 == 0 /\ ___rho_4_^0-___rho_4_^post3 == 0 /\ tt1^0-tt1^post3 == 0 /\ -wakend^post3+wakend^0 == 0 /\ -___rho_2_^post3+___rho_2_^0 == 0 /\ -___rho_5_^post3+___rho_5_^0 == 0 /\ a22^0-a22^post3 == 0 /\ curtime^0-curtime^post3 == 0), cost: 1 3: l5 -> l6 : ___rho_2_^0'=___rho_2_^post4, ___rho_3_^0'=___rho_3_^post4, ___rho_4_^0'=___rho_4_^post4, ___rho_5_^0'=___rho_5_^post4, a22^0'=a22^post4, curtime^0'=curtime^post4, got_sighup^0'=got_sighup^post4, last_copy_time^0'=last_copy_time^post4, tt1^0'=tt1^post4, wakend^0'=wakend^post4, (curtime^0-curtime^post4 == 0 /\ a22^0-a22^post4 == 0 /\ -tt1^post4+tt1^0 == 0 /\ last_copy_time^0-last_copy_time^post4 == 0 /\ -___rho_5_^post4+___rho_5_^0 == 0 /\ ___rho_3_^0-___rho_3_^post4 == 0 /\ -wakend^post4+wakend^0 == 0 /\ -got_sighup^post4+got_sighup^0 == 0 /\ -___rho_4_^post4+___rho_4_^0 == 0 /\ -___rho_2_^post4+___rho_2_^0 == 0), cost: 1 9: l6 -> l10 : ___rho_2_^0'=___rho_2_^post10, ___rho_3_^0'=___rho_3_^post10, ___rho_4_^0'=___rho_4_^post10, ___rho_5_^0'=___rho_5_^post10, a22^0'=a22^post10, curtime^0'=curtime^post10, got_sighup^0'=got_sighup^post10, last_copy_time^0'=last_copy_time^post10, tt1^0'=tt1^post10, wakend^0'=wakend^post10, (curtime^0-curtime^post10 == 0 /\ a22^0-a22^post10 == 0 /\ -tt1^post10+tt1^0 == 0 /\ -___rho_5_^post10+___rho_5_^0 == 0 /\ last_copy_time^0-last_copy_time^post10 == 0 /\ -wakend^post10+wakend^0 == 0 /\ ___rho_3_^0-___rho_3_^post10 == 0 /\ -___rho_2_^post10+___rho_2_^0 == 0 /\ -___rho_4_^post10+___rho_4_^0 == 0 /\ -got_sighup^post10+got_sighup^0 == 0), cost: 1 4: l7 -> l5 : ___rho_2_^0'=___rho_2_^post5, ___rho_3_^0'=___rho_3_^post5, ___rho_4_^0'=___rho_4_^post5, ___rho_5_^0'=___rho_5_^post5, a22^0'=a22^post5, curtime^0'=curtime^post5, got_sighup^0'=got_sighup^post5, last_copy_time^0'=last_copy_time^post5, tt1^0'=tt1^post5, wakend^0'=wakend^post5, (0 == 0 /\ -___rho_2_^post5+___rho_2_^0 == 0 /\ -___rho_3_^post5+___rho_3_^0 == 0 /\ -a22^post5+a22^0 == 0 /\ curtime^0-curtime^post5 == 0 /\ last_copy_time^0-last_copy_time^post5 == 0 /\ got_sighup^0-got_sighup^post5 == 0 /\ wakend^0-wakend^post5 == 0 /\ -tt1^post5+tt1^0 == 0 /\ ___rho_4_^0-___rho_4_^post5 == 0), cost: 1 5: l8 -> l7 : ___rho_2_^0'=___rho_2_^post6, ___rho_3_^0'=___rho_3_^post6, ___rho_4_^0'=___rho_4_^post6, ___rho_5_^0'=___rho_5_^post6, a22^0'=a22^post6, curtime^0'=curtime^post6, got_sighup^0'=got_sighup^post6, last_copy_time^0'=last_copy_time^post6, tt1^0'=tt1^post6, wakend^0'=wakend^post6, (-999+curtime^0-last_copy_time^0 <= 0 /\ curtime^0-curtime^post6 == 0 /\ -___rho_3_^post6+___rho_3_^0 == 0 /\ -got_sighup^post6+got_sighup^0 == 0 /\ last_copy_time^0-last_copy_time^post6 == 0 /\ -tt1^post6+tt1^0 == 0 /\ ___rho_5_^0-___rho_5_^post6 == 0 /\ wakend^0-wakend^post6 == 0 /\ ___rho_4_^0-___rho_4_^post6 == 0 /\ -___rho_2_^post6+___rho_2_^0 == 0 /\ -a22^post6+a22^0 == 0), cost: 1 6: l8 -> l7 : ___rho_2_^0'=___rho_2_^post7, ___rho_3_^0'=___rho_3_^post7, ___rho_4_^0'=___rho_4_^post7, ___rho_5_^0'=___rho_5_^post7, a22^0'=a22^post7, curtime^0'=curtime^post7, got_sighup^0'=got_sighup^post7, last_copy_time^0'=last_copy_time^post7, tt1^0'=tt1^post7, wakend^0'=wakend^post7, (-got_sighup^post7+got_sighup^0 == 0 /\ -1+wakend^post7 == 0 /\ -___rho_5_^post7+___rho_5_^0 == 0 /\ -___rho_3_^post7+___rho_3_^0 == 0 /\ a22^0-a22^post7 == 0 /\ ___rho_4_^0-___rho_4_^post7 == 0 /\ curtime^0-curtime^post7 == 0 /\ last_copy_time^0-last_copy_time^post7 == 0 /\ -___rho_2_^post7+___rho_2_^0 == 0 /\ 1000-curtime^0+last_copy_time^0 <= 0 /\ tt1^0-tt1^post7 == 0), cost: 1 7: l9 -> l7 : ___rho_2_^0'=___rho_2_^post8, ___rho_3_^0'=___rho_3_^post8, ___rho_4_^0'=___rho_4_^post8, ___rho_5_^0'=___rho_5_^post8, a22^0'=a22^post8, curtime^0'=curtime^post8, got_sighup^0'=got_sighup^post8, last_copy_time^0'=last_copy_time^post8, tt1^0'=tt1^post8, wakend^0'=wakend^post8, (___rho_4_^0-___rho_4_^post8 == 0 /\ -___rho_5_^post8+___rho_5_^0 == 0 /\ -got_sighup^post8+got_sighup^0 == 0 /\ ___rho_3_^0-___rho_3_^post8 == 0 /\ a22^0-a22^post8 == 0 /\ -tt1^post8+tt1^0 == 0 /\ -wakend^post8+wakend^0 == 0 /\ -___rho_2_^post8+___rho_2_^0 == 0 /\ curtime^0-curtime^post8 == 0 /\ 1-wakend^0 <= 0 /\ last_copy_time^0-last_copy_time^post8 == 0), cost: 1 8: l9 -> l8 : ___rho_2_^0'=___rho_2_^post9, ___rho_3_^0'=___rho_3_^post9, ___rho_4_^0'=___rho_4_^post9, ___rho_5_^0'=___rho_5_^post9, a22^0'=a22^post9, curtime^0'=curtime^post9, got_sighup^0'=got_sighup^post9, last_copy_time^0'=last_copy_time^post9, tt1^0'=tt1^post9, wakend^0'=wakend^post9, (0 == 0 /\ ___rho_3_^0-___rho_3_^post9 == 0 /\ wakend^0 <= 0 /\ tt1^0-tt1^post9 == 0 /\ ___rho_4_^0-___rho_4_^post9 == 0 /\ -wakend^post9+wakend^0 == 0 /\ -___rho_5_^post9+___rho_5_^0 == 0 /\ a22^0-a22^post9 == 0 /\ -___rho_2_^post9+___rho_2_^0 == 0 /\ -got_sighup^post9+got_sighup^0 == 0 /\ last_copy_time^0-last_copy_time^post9 == 0), cost: 1 10: l10 -> l6 : ___rho_2_^0'=___rho_2_^post11, ___rho_3_^0'=___rho_3_^post11, ___rho_4_^0'=___rho_4_^post11, ___rho_5_^0'=___rho_5_^post11, a22^0'=a22^post11, curtime^0'=curtime^post11, got_sighup^0'=got_sighup^post11, last_copy_time^0'=last_copy_time^post11, tt1^0'=tt1^post11, wakend^0'=wakend^post11, (-a22^post11+a22^0 == 0 /\ last_copy_time^0-last_copy_time^post11 == 0 /\ got_sighup^0-got_sighup^post11 == 0 /\ wakend^0-wakend^post11 == 0 /\ -___rho_2_^post11+___rho_2_^0 == 0 /\ -___rho_5_^post11+___rho_5_^0 == 0 /\ ___rho_4_^0-___rho_4_^post11 == 0 /\ curtime^0-curtime^post11 == 0 /\ ___rho_3_^0-___rho_3_^post11 == 0 /\ -tt1^post11+tt1^0 == 0), cost: 1 15: l11 -> l0 : ___rho_2_^0'=___rho_2_^post16, ___rho_3_^0'=___rho_3_^post16, ___rho_4_^0'=___rho_4_^post16, ___rho_5_^0'=___rho_5_^post16, a22^0'=a22^post16, curtime^0'=curtime^post16, got_sighup^0'=got_sighup^post16, last_copy_time^0'=last_copy_time^post16, tt1^0'=tt1^post16, wakend^0'=wakend^post16, (0 == 0 /\ -1+wakend^post16 == 0 /\ ___rho_4_^0-___rho_4_^post16 == 0 /\ -tt1^post16+tt1^0 == 0 /\ -___rho_5_^post16+___rho_5_^0 == 0 /\ curtime^0-curtime^post16 == 0 /\ -___rho_3_^post16+___rho_3_^0 == 0 /\ got_sighup^post16-___rho_2_^post16 == 0 /\ -1+wakend^1 == 0 /\ last_copy_time^0-last_copy_time^post16 == 0 /\ -a22^post16+a22^0 == 0), cost: 1 16: l12 -> l11 : ___rho_2_^0'=___rho_2_^post17, ___rho_3_^0'=___rho_3_^post17, ___rho_4_^0'=___rho_4_^post17, ___rho_5_^0'=___rho_5_^post17, a22^0'=a22^post17, curtime^0'=curtime^post17, got_sighup^0'=got_sighup^post17, last_copy_time^0'=last_copy_time^post17, tt1^0'=tt1^post17, wakend^0'=wakend^post17, (got_sighup^0-got_sighup^post17 == 0 /\ -a22^post17+a22^0 == 0 /\ -___rho_2_^post17+___rho_2_^0 == 0 /\ -wakend^post17+wakend^0 == 0 /\ ___rho_5_^0-___rho_5_^post17 == 0 /\ ___rho_4_^0-___rho_4_^post17 == 0 /\ -tt1^post17+tt1^0 == 0 /\ curtime^0-curtime^post17 == 0 /\ last_copy_time^0-last_copy_time^post17 == 0 /\ -___rho_3_^post17+___rho_3_^0 == 0), cost: 1 Chained Linear Paths Start location: l12 Program variables: ___rho_2_^0 ___rho_3_^0 ___rho_4_^0 ___rho_5_^0 a22^0 curtime^0 got_sighup^0 last_copy_time^0 tt1^0 wakend^0 0: l0 -> l1 : ___rho_2_^0'=___rho_2_^post1, ___rho_3_^0'=___rho_3_^post1, ___rho_4_^0'=___rho_4_^post1, ___rho_5_^0'=___rho_5_^post1, a22^0'=a22^post1, curtime^0'=curtime^post1, got_sighup^0'=got_sighup^post1, last_copy_time^0'=last_copy_time^post1, tt1^0'=tt1^post1, wakend^0'=wakend^post1, (-___rho_5_^post1+___rho_5_^0 == 0 /\ -___rho_3_^post1+___rho_3_^0 == 0 /\ ___rho_4_^0-___rho_4_^post1 == 0 /\ curtime^0-curtime^post1 == 0 /\ got_sighup^0 <= 0 /\ a22^0-a22^post1 == 0 /\ -___rho_2_^post1+___rho_2_^0 == 0 /\ last_copy_time^0-last_copy_time^post1 == 0 /\ -tt1^post1+tt1^0 == 0 /\ wakend^0-wakend^post1 == 0 /\ -got_sighup^post1+got_sighup^0 == 0), cost: 1 1: l0 -> l2 : ___rho_2_^0'=___rho_2_^post2, ___rho_3_^0'=___rho_3_^post2, ___rho_4_^0'=___rho_4_^post2, ___rho_5_^0'=___rho_5_^post2, a22^0'=a22^post2, curtime^0'=curtime^post2, got_sighup^0'=got_sighup^post2, last_copy_time^0'=last_copy_time^post2, tt1^0'=tt1^post2, wakend^0'=wakend^post2, (0 == 0 /\ ___rho_4_^0-___rho_4_^post2 == 0 /\ got_sighup^post2 == 0 /\ -___rho_5_^post2+___rho_5_^0 == 0 /\ 1-got_sighup^0 <= 0 /\ -___rho_3_^post2+tt1^post2 == 0 /\ -wakend^post2+wakend^0 == 0 /\ curtime^0-curtime^post2 == 0 /\ -___rho_2_^post2+___rho_2_^0 == 0 /\ last_copy_time^0-last_copy_time^post2 == 0 /\ -1+a22^post2 == 0), cost: 1 11: l1 -> l9 : ___rho_2_^0'=___rho_2_^post12, ___rho_3_^0'=___rho_3_^post12, ___rho_4_^0'=___rho_4_^post12, ___rho_5_^0'=___rho_5_^post12, a22^0'=a22^post12, curtime^0'=curtime^post12, got_sighup^0'=got_sighup^post12, last_copy_time^0'=last_copy_time^post12, tt1^0'=tt1^post12, wakend^0'=wakend^post12, (curtime^0-curtime^post12 == 0 /\ got_sighup^0-got_sighup^post12 == 0 /\ -tt1^post12+tt1^0 == 0 /\ wakend^0 <= 0 /\ last_copy_time^0-last_copy_time^post12 == 0 /\ -___rho_3_^post12+___rho_3_^0 == 0 /\ wakend^0-wakend^post12 == 0 /\ ___rho_5_^0-___rho_5_^post12 == 0 /\ -a22^post12+a22^0 == 0 /\ ___rho_4_^0-___rho_4_^post12 == 0 /\ -___rho_2_^post12+___rho_2_^0 == 0), cost: 1 12: l1 -> l9 : ___rho_2_^0'=___rho_2_^post13, ___rho_3_^0'=___rho_3_^post13, ___rho_4_^0'=___rho_4_^post13, ___rho_5_^0'=___rho_5_^post13, a22^0'=a22^post13, curtime^0'=curtime^post13, got_sighup^0'=got_sighup^post13, last_copy_time^0'=last_copy_time^post13, tt1^0'=tt1^post13, wakend^0'=wakend^post13, (0 == 0 /\ wakend^post13 == 0 /\ -got_sighup^post13+got_sighup^0 == 0 /\ -___rho_2_^post13+___rho_2_^0 == 0 /\ -___rho_3_^post13+___rho_3_^0 == 0 /\ -___rho_5_^post13+___rho_5_^0 == 0 /\ a22^0-a22^post13 == 0 /\ last_copy_time^post13-___rho_4_^post13 == 0 /\ -tt1^post13+tt1^0 == 0 /\ curtime^0-curtime^post13 == 0 /\ 1-wakend^0 <= 0), cost: 1 13: l2 -> l1 : ___rho_2_^0'=___rho_2_^post14, ___rho_3_^0'=___rho_3_^post14, ___rho_4_^0'=___rho_4_^post14, ___rho_5_^0'=___rho_5_^post14, a22^0'=a22^post14, curtime^0'=curtime^post14, got_sighup^0'=got_sighup^post14, last_copy_time^0'=last_copy_time^post14, tt1^0'=tt1^post14, wakend^0'=wakend^post14, (-got_sighup^post14+got_sighup^0 == 0 /\ ___rho_3_^0-___rho_3_^post14 == 0 /\ ___rho_4_^0-___rho_4_^post14 == 0 /\ 1-tt1^0 <= 0 /\ -___rho_5_^post14+___rho_5_^0 == 0 /\ -___rho_2_^post14+___rho_2_^0 == 0 /\ a22^0-a22^post14 == 0 /\ -wakend^post14+wakend^0 == 0 /\ -tt1^post14+tt1^0 == 0 /\ last_copy_time^0-last_copy_time^post14 == 0 /\ curtime^0-curtime^post14 == 0), cost: 1 14: l2 -> l5 : ___rho_2_^0'=___rho_2_^post15, ___rho_3_^0'=___rho_3_^post15, ___rho_4_^0'=___rho_4_^post15, ___rho_5_^0'=___rho_5_^post15, a22^0'=a22^post15, curtime^0'=curtime^post15, got_sighup^0'=got_sighup^post15, last_copy_time^0'=last_copy_time^post15, tt1^0'=tt1^post15, wakend^0'=wakend^post15, (tt1^0-tt1^post15 == 0 /\ ___rho_3_^0-___rho_3_^post15 == 0 /\ ___rho_4_^0-___rho_4_^post15 == 0 /\ -___rho_5_^post15+___rho_5_^0 == 0 /\ -___rho_2_^post15+___rho_2_^0 == 0 /\ curtime^0-curtime^post15 == 0 /\ a22^0-a22^post15 == 0 /\ tt1^0 <= 0 /\ -got_sighup^post15+got_sighup^0 == 0 /\ -wakend^post15+wakend^0 == 0 /\ last_copy_time^0-last_copy_time^post15 == 0), cost: 1 2: l3 -> l4 : ___rho_2_^0'=___rho_2_^post3, ___rho_3_^0'=___rho_3_^post3, ___rho_4_^0'=___rho_4_^post3, ___rho_5_^0'=___rho_5_^post3, a22^0'=a22^post3, curtime^0'=curtime^post3, got_sighup^0'=got_sighup^post3, last_copy_time^0'=last_copy_time^post3, tt1^0'=tt1^post3, wakend^0'=wakend^post3, (last_copy_time^0-last_copy_time^post3 == 0 /\ -got_sighup^post3+got_sighup^0 == 0 /\ ___rho_3_^0-___rho_3_^post3 == 0 /\ ___rho_4_^0-___rho_4_^post3 == 0 /\ tt1^0-tt1^post3 == 0 /\ -wakend^post3+wakend^0 == 0 /\ -___rho_2_^post3+___rho_2_^0 == 0 /\ -___rho_5_^post3+___rho_5_^0 == 0 /\ a22^0-a22^post3 == 0 /\ curtime^0-curtime^post3 == 0), cost: 1 3: l5 -> l6 : ___rho_2_^0'=___rho_2_^post4, ___rho_3_^0'=___rho_3_^post4, ___rho_4_^0'=___rho_4_^post4, ___rho_5_^0'=___rho_5_^post4, a22^0'=a22^post4, curtime^0'=curtime^post4, got_sighup^0'=got_sighup^post4, last_copy_time^0'=last_copy_time^post4, tt1^0'=tt1^post4, wakend^0'=wakend^post4, (curtime^0-curtime^post4 == 0 /\ a22^0-a22^post4 == 0 /\ -tt1^post4+tt1^0 == 0 /\ last_copy_time^0-last_copy_time^post4 == 0 /\ -___rho_5_^post4+___rho_5_^0 == 0 /\ ___rho_3_^0-___rho_3_^post4 == 0 /\ -wakend^post4+wakend^0 == 0 /\ -got_sighup^post4+got_sighup^0 == 0 /\ -___rho_4_^post4+___rho_4_^0 == 0 /\ -___rho_2_^post4+___rho_2_^0 == 0), cost: 1 18: l6 -> l6 : ___rho_2_^0'=___rho_2_^post11, ___rho_3_^0'=___rho_3_^post11, ___rho_4_^0'=___rho_4_^post11, ___rho_5_^0'=___rho_5_^post11, a22^0'=a22^post11, curtime^0'=curtime^post11, got_sighup^0'=got_sighup^post11, last_copy_time^0'=last_copy_time^post11, tt1^0'=tt1^post11, wakend^0'=wakend^post11, (curtime^0-curtime^post10 == 0 /\ wakend^post10-wakend^post11 == 0 /\ a22^0-a22^post10 == 0 /\ -last_copy_time^post11+last_copy_time^post10 == 0 /\ ___rho_2_^post10-___rho_2_^post11 == 0 /\ -tt1^post10+tt1^0 == 0 /\ -___rho_5_^post10+___rho_5_^0 == 0 /\ last_copy_time^0-last_copy_time^post10 == 0 /\ -a22^post11+a22^post10 == 0 /\ got_sighup^post10-got_sighup^post11 == 0 /\ ___rho_4_^post10-___rho_4_^post11 == 0 /\ -wakend^post10+wakend^0 == 0 /\ ___rho_5_^post10-___rho_5_^post11 == 0 /\ ___rho_3_^0-___rho_3_^post10 == 0 /\ tt1^post10-tt1^post11 == 0 /\ -___rho_2_^post10+___rho_2_^0 == 0 /\ curtime^post10-curtime^post11 == 0 /\ -___rho_4_^post10+___rho_4_^0 == 0 /\ ___rho_3_^post10-___rho_3_^post11 == 0 /\ -got_sighup^post10+got_sighup^0 == 0), cost: 1 4: l7 -> l5 : ___rho_2_^0'=___rho_2_^post5, ___rho_3_^0'=___rho_3_^post5, ___rho_4_^0'=___rho_4_^post5, ___rho_5_^0'=___rho_5_^post5, a22^0'=a22^post5, curtime^0'=curtime^post5, got_sighup^0'=got_sighup^post5, last_copy_time^0'=last_copy_time^post5, tt1^0'=tt1^post5, wakend^0'=wakend^post5, (0 == 0 /\ -___rho_2_^post5+___rho_2_^0 == 0 /\ -___rho_3_^post5+___rho_3_^0 == 0 /\ -a22^post5+a22^0 == 0 /\ curtime^0-curtime^post5 == 0 /\ last_copy_time^0-last_copy_time^post5 == 0 /\ got_sighup^0-got_sighup^post5 == 0 /\ wakend^0-wakend^post5 == 0 /\ -tt1^post5+tt1^0 == 0 /\ ___rho_4_^0-___rho_4_^post5 == 0), cost: 1 5: l8 -> l7 : ___rho_2_^0'=___rho_2_^post6, ___rho_3_^0'=___rho_3_^post6, ___rho_4_^0'=___rho_4_^post6, ___rho_5_^0'=___rho_5_^post6, a22^0'=a22^post6, curtime^0'=curtime^post6, got_sighup^0'=got_sighup^post6, last_copy_time^0'=last_copy_time^post6, tt1^0'=tt1^post6, wakend^0'=wakend^post6, (-999+curtime^0-last_copy_time^0 <= 0 /\ curtime^0-curtime^post6 == 0 /\ -___rho_3_^post6+___rho_3_^0 == 0 /\ -got_sighup^post6+got_sighup^0 == 0 /\ last_copy_time^0-last_copy_time^post6 == 0 /\ -tt1^post6+tt1^0 == 0 /\ ___rho_5_^0-___rho_5_^post6 == 0 /\ wakend^0-wakend^post6 == 0 /\ ___rho_4_^0-___rho_4_^post6 == 0 /\ -___rho_2_^post6+___rho_2_^0 == 0 /\ -a22^post6+a22^0 == 0), cost: 1 6: l8 -> l7 : ___rho_2_^0'=___rho_2_^post7, ___rho_3_^0'=___rho_3_^post7, ___rho_4_^0'=___rho_4_^post7, ___rho_5_^0'=___rho_5_^post7, a22^0'=a22^post7, curtime^0'=curtime^post7, got_sighup^0'=got_sighup^post7, last_copy_time^0'=last_copy_time^post7, tt1^0'=tt1^post7, wakend^0'=wakend^post7, (-got_sighup^post7+got_sighup^0 == 0 /\ -1+wakend^post7 == 0 /\ -___rho_5_^post7+___rho_5_^0 == 0 /\ -___rho_3_^post7+___rho_3_^0 == 0 /\ a22^0-a22^post7 == 0 /\ ___rho_4_^0-___rho_4_^post7 == 0 /\ curtime^0-curtime^post7 == 0 /\ last_copy_time^0-last_copy_time^post7 == 0 /\ -___rho_2_^post7+___rho_2_^0 == 0 /\ 1000-curtime^0+last_copy_time^0 <= 0 /\ tt1^0-tt1^post7 == 0), cost: 1 7: l9 -> l7 : ___rho_2_^0'=___rho_2_^post8, ___rho_3_^0'=___rho_3_^post8, ___rho_4_^0'=___rho_4_^post8, ___rho_5_^0'=___rho_5_^post8, a22^0'=a22^post8, curtime^0'=curtime^post8, got_sighup^0'=got_sighup^post8, last_copy_time^0'=last_copy_time^post8, tt1^0'=tt1^post8, wakend^0'=wakend^post8, (___rho_4_^0-___rho_4_^post8 == 0 /\ -___rho_5_^post8+___rho_5_^0 == 0 /\ -got_sighup^post8+got_sighup^0 == 0 /\ ___rho_3_^0-___rho_3_^post8 == 0 /\ a22^0-a22^post8 == 0 /\ -tt1^post8+tt1^0 == 0 /\ -wakend^post8+wakend^0 == 0 /\ -___rho_2_^post8+___rho_2_^0 == 0 /\ curtime^0-curtime^post8 == 0 /\ 1-wakend^0 <= 0 /\ last_copy_time^0-last_copy_time^post8 == 0), cost: 1 8: l9 -> l8 : ___rho_2_^0'=___rho_2_^post9, ___rho_3_^0'=___rho_3_^post9, ___rho_4_^0'=___rho_4_^post9, ___rho_5_^0'=___rho_5_^post9, a22^0'=a22^post9, curtime^0'=curtime^post9, got_sighup^0'=got_sighup^post9, last_copy_time^0'=last_copy_time^post9, tt1^0'=tt1^post9, wakend^0'=wakend^post9, (0 == 0 /\ ___rho_3_^0-___rho_3_^post9 == 0 /\ wakend^0 <= 0 /\ tt1^0-tt1^post9 == 0 /\ ___rho_4_^0-___rho_4_^post9 == 0 /\ -wakend^post9+wakend^0 == 0 /\ -___rho_5_^post9+___rho_5_^0 == 0 /\ a22^0-a22^post9 == 0 /\ -___rho_2_^post9+___rho_2_^0 == 0 /\ -got_sighup^post9+got_sighup^0 == 0 /\ last_copy_time^0-last_copy_time^post9 == 0), cost: 1 17: l12 -> l0 : ___rho_2_^0'=___rho_2_^post16, ___rho_3_^0'=___rho_3_^post16, ___rho_4_^0'=___rho_4_^post16, ___rho_5_^0'=___rho_5_^post16, a22^0'=a22^post16, curtime^0'=curtime^post16, got_sighup^0'=got_sighup^post16, last_copy_time^0'=last_copy_time^post16, tt1^0'=tt1^post16, wakend^0'=wakend^post16, (0 == 0 /\ -1+wakend^post16 == 0 /\ last_copy_time^post17-last_copy_time^post16 == 0 /\ got_sighup^0-got_sighup^post17 == 0 /\ -a22^post16+a22^post17 == 0 /\ -a22^post17+a22^0 == 0 /\ -tt1^post16+tt1^post17 == 0 /\ -___rho_2_^post17+___rho_2_^0 == 0 /\ -wakend^post17+wakend^0 == 0 /\ -___rho_5_^post16+___rho_5_^post17 == 0 /\ ___rho_5_^0-___rho_5_^post17 == 0 /\ ___rho_4_^0-___rho_4_^post17 == 0 /\ -tt1^post17+tt1^0 == 0 /\ -curtime^post16+curtime^post17 == 0 /\ got_sighup^post16-___rho_2_^post16 == 0 /\ -1+wakend^1 == 0 /\ curtime^0-curtime^post17 == 0 /\ last_copy_time^0-last_copy_time^post17 == 0 /\ -___rho_3_^post16+___rho_3_^post17 == 0 /\ -___rho_4_^post16+___rho_4_^post17 == 0 /\ -___rho_3_^post17+___rho_3_^0 == 0), cost: 1 Eliminating location l11 by chaining: Applied chaining First rule: l12 -> l11 : ___rho_2_^0'=___rho_2_^post17, ___rho_3_^0'=___rho_3_^post17, ___rho_4_^0'=___rho_4_^post17, ___rho_5_^0'=___rho_5_^post17, a22^0'=a22^post17, curtime^0'=curtime^post17, got_sighup^0'=got_sighup^post17, last_copy_time^0'=last_copy_time^post17, tt1^0'=tt1^post17, wakend^0'=wakend^post17, (got_sighup^0-got_sighup^post17 == 0 /\ -a22^post17+a22^0 == 0 /\ -___rho_2_^post17+___rho_2_^0 == 0 /\ -wakend^post17+wakend^0 == 0 /\ ___rho_5_^0-___rho_5_^post17 == 0 /\ ___rho_4_^0-___rho_4_^post17 == 0 /\ -tt1^post17+tt1^0 == 0 /\ curtime^0-curtime^post17 == 0 /\ last_copy_time^0-last_copy_time^post17 == 0 /\ -___rho_3_^post17+___rho_3_^0 == 0), cost: 1 Second rule: l11 -> l0 : ___rho_2_^0'=___rho_2_^post16, ___rho_3_^0'=___rho_3_^post16, ___rho_4_^0'=___rho_4_^post16, ___rho_5_^0'=___rho_5_^post16, a22^0'=a22^post16, curtime^0'=curtime^post16, got_sighup^0'=got_sighup^post16, last_copy_time^0'=last_copy_time^post16, tt1^0'=tt1^post16, wakend^0'=wakend^post16, (0 == 0 /\ -1+wakend^post16 == 0 /\ ___rho_4_^0-___rho_4_^post16 == 0 /\ -tt1^post16+tt1^0 == 0 /\ -___rho_5_^post16+___rho_5_^0 == 0 /\ curtime^0-curtime^post16 == 0 /\ -___rho_3_^post16+___rho_3_^0 == 0 /\ got_sighup^post16-___rho_2_^post16 == 0 /\ -1+wakend^1 == 0 /\ last_copy_time^0-last_copy_time^post16 == 0 /\ -a22^post16+a22^0 == 0), cost: 1 New rule: l12 -> l0 : ___rho_2_^0'=___rho_2_^post16, ___rho_3_^0'=___rho_3_^post16, ___rho_4_^0'=___rho_4_^post16, ___rho_5_^0'=___rho_5_^post16, a22^0'=a22^post16, curtime^0'=curtime^post16, got_sighup^0'=got_sighup^post16, last_copy_time^0'=last_copy_time^post16, tt1^0'=tt1^post16, wakend^0'=wakend^post16, (0 == 0 /\ -1+wakend^post16 == 0 /\ last_copy_time^post17-last_copy_time^post16 == 0 /\ got_sighup^0-got_sighup^post17 == 0 /\ -a22^post16+a22^post17 == 0 /\ -a22^post17+a22^0 == 0 /\ -tt1^post16+tt1^post17 == 0 /\ -___rho_2_^post17+___rho_2_^0 == 0 /\ -wakend^post17+wakend^0 == 0 /\ -___rho_5_^post16+___rho_5_^post17 == 0 /\ ___rho_5_^0-___rho_5_^post17 == 0 /\ ___rho_4_^0-___rho_4_^post17 == 0 /\ -tt1^post17+tt1^0 == 0 /\ -curtime^post16+curtime^post17 == 0 /\ got_sighup^post16-___rho_2_^post16 == 0 /\ -1+wakend^1 == 0 /\ curtime^0-curtime^post17 == 0 /\ last_copy_time^0-last_copy_time^post17 == 0 /\ -___rho_3_^post16+___rho_3_^post17 == 0 /\ -___rho_4_^post16+___rho_4_^post17 == 0 /\ -___rho_3_^post17+___rho_3_^0 == 0), cost: 1 Applied deletion Removed the following rules: 15 16 Eliminating location l10 by chaining: Applied chaining First rule: l6 -> l10 : ___rho_2_^0'=___rho_2_^post10, ___rho_3_^0'=___rho_3_^post10, ___rho_4_^0'=___rho_4_^post10, ___rho_5_^0'=___rho_5_^post10, a22^0'=a22^post10, curtime^0'=curtime^post10, got_sighup^0'=got_sighup^post10, last_copy_time^0'=last_copy_time^post10, tt1^0'=tt1^post10, wakend^0'=wakend^post10, (curtime^0-curtime^post10 == 0 /\ a22^0-a22^post10 == 0 /\ -tt1^post10+tt1^0 == 0 /\ -___rho_5_^post10+___rho_5_^0 == 0 /\ last_copy_time^0-last_copy_time^post10 == 0 /\ -wakend^post10+wakend^0 == 0 /\ ___rho_3_^0-___rho_3_^post10 == 0 /\ -___rho_2_^post10+___rho_2_^0 == 0 /\ -___rho_4_^post10+___rho_4_^0 == 0 /\ -got_sighup^post10+got_sighup^0 == 0), cost: 1 Second rule: l10 -> l6 : ___rho_2_^0'=___rho_2_^post11, ___rho_3_^0'=___rho_3_^post11, ___rho_4_^0'=___rho_4_^post11, ___rho_5_^0'=___rho_5_^post11, a22^0'=a22^post11, curtime^0'=curtime^post11, got_sighup^0'=got_sighup^post11, last_copy_time^0'=last_copy_time^post11, tt1^0'=tt1^post11, wakend^0'=wakend^post11, (-a22^post11+a22^0 == 0 /\ last_copy_time^0-last_copy_time^post11 == 0 /\ got_sighup^0-got_sighup^post11 == 0 /\ wakend^0-wakend^post11 == 0 /\ -___rho_2_^post11+___rho_2_^0 == 0 /\ -___rho_5_^post11+___rho_5_^0 == 0 /\ ___rho_4_^0-___rho_4_^post11 == 0 /\ curtime^0-curtime^post11 == 0 /\ ___rho_3_^0-___rho_3_^post11 == 0 /\ -tt1^post11+tt1^0 == 0), cost: 1 New rule: l6 -> l6 : ___rho_2_^0'=___rho_2_^post11, ___rho_3_^0'=___rho_3_^post11, ___rho_4_^0'=___rho_4_^post11, ___rho_5_^0'=___rho_5_^post11, a22^0'=a22^post11, curtime^0'=curtime^post11, got_sighup^0'=got_sighup^post11, last_copy_time^0'=last_copy_time^post11, tt1^0'=tt1^post11, wakend^0'=wakend^post11, (curtime^0-curtime^post10 == 0 /\ wakend^post10-wakend^post11 == 0 /\ a22^0-a22^post10 == 0 /\ -last_copy_time^post11+last_copy_time^post10 == 0 /\ ___rho_2_^post10-___rho_2_^post11 == 0 /\ -tt1^post10+tt1^0 == 0 /\ -___rho_5_^post10+___rho_5_^0 == 0 /\ last_copy_time^0-last_copy_time^post10 == 0 /\ -a22^post11+a22^post10 == 0 /\ got_sighup^post10-got_sighup^post11 == 0 /\ ___rho_4_^post10-___rho_4_^post11 == 0 /\ -wakend^post10+wakend^0 == 0 /\ ___rho_5_^post10-___rho_5_^post11 == 0 /\ ___rho_3_^0-___rho_3_^post10 == 0 /\ tt1^post10-tt1^post11 == 0 /\ -___rho_2_^post10+___rho_2_^0 == 0 /\ curtime^post10-curtime^post11 == 0 /\ -___rho_4_^post10+___rho_4_^0 == 0 /\ ___rho_3_^post10-___rho_3_^post11 == 0 /\ -got_sighup^post10+got_sighup^0 == 0), cost: 1 Applied deletion Removed the following rules: 9 10 Simplified Transitions Start location: l12 Program variables: ___rho_2_^0 ___rho_3_^0 ___rho_4_^0 ___rho_5_^0 a22^0 curtime^0 got_sighup^0 last_copy_time^0 tt1^0 wakend^0 19: l0 -> l1 : got_sighup^0 <= 0, cost: 1 20: l0 -> l2 : ___rho_3_^0'=tt1^post2, a22^0'=1, got_sighup^0'=0, tt1^0'=tt1^post2, 1-got_sighup^0 <= 0, cost: 1 28: l1 -> l9 : wakend^0 <= 0, cost: 1 29: l1 -> l9 : ___rho_4_^0'=last_copy_time^post13, last_copy_time^0'=last_copy_time^post13, wakend^0'=0, 1-wakend^0 <= 0, cost: 1 30: l2 -> l1 : 1-tt1^0 <= 0, cost: 1 31: l2 -> l5 : tt1^0 <= 0, cost: 1 21: l3 -> l4 : T, cost: 1 22: l5 -> l6 : T, cost: 1 33: l6 -> l6 : T, cost: 1 23: l7 -> l5 : ___rho_5_^0'=___rho_5_^post5, T, cost: 1 24: l8 -> l7 : -999+curtime^0-last_copy_time^0 <= 0, cost: 1 25: l8 -> l7 : wakend^0'=1, 1000-curtime^0+last_copy_time^0 <= 0, cost: 1 26: l9 -> l7 : 1-wakend^0 <= 0, cost: 1 27: l9 -> l8 : curtime^0'=curtime^post9, wakend^0 <= 0, cost: 1 32: l12 -> l0 : ___rho_2_^0'=got_sighup^post16, got_sighup^0'=got_sighup^post16, wakend^0'=1, T, cost: 1 Propagated Equalities Original rule: l0 -> l1 : ___rho_2_^0'=___rho_2_^post1, ___rho_3_^0'=___rho_3_^post1, ___rho_4_^0'=___rho_4_^post1, ___rho_5_^0'=___rho_5_^post1, a22^0'=a22^post1, curtime^0'=curtime^post1, got_sighup^0'=got_sighup^post1, last_copy_time^0'=last_copy_time^post1, tt1^0'=tt1^post1, wakend^0'=wakend^post1, (-___rho_5_^post1+___rho_5_^0 == 0 /\ -___rho_3_^post1+___rho_3_^0 == 0 /\ ___rho_4_^0-___rho_4_^post1 == 0 /\ curtime^0-curtime^post1 == 0 /\ got_sighup^0 <= 0 /\ a22^0-a22^post1 == 0 /\ -___rho_2_^post1+___rho_2_^0 == 0 /\ last_copy_time^0-last_copy_time^post1 == 0 /\ -tt1^post1+tt1^0 == 0 /\ wakend^0-wakend^post1 == 0 /\ -got_sighup^post1+got_sighup^0 == 0), cost: 1 New rule: l0 -> l1 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^0, a22^0'=a22^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^0, wakend^0'=wakend^0, (0 == 0 /\ got_sighup^0 <= 0), cost: 1 propagated equality ___rho_5_^post1 = ___rho_5_^0 propagated equality ___rho_3_^post1 = ___rho_3_^0 propagated equality ___rho_4_^post1 = ___rho_4_^0 propagated equality curtime^post1 = curtime^0 propagated equality a22^post1 = a22^0 propagated equality ___rho_2_^post1 = ___rho_2_^0 propagated equality last_copy_time^post1 = last_copy_time^0 propagated equality tt1^post1 = tt1^0 propagated equality wakend^post1 = wakend^0 propagated equality got_sighup^post1 = got_sighup^0 Simplified Guard Original rule: l0 -> l1 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^0, a22^0'=a22^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^0, wakend^0'=wakend^0, (0 == 0 /\ got_sighup^0 <= 0), cost: 1 New rule: l0 -> l1 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^0, a22^0'=a22^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^0, wakend^0'=wakend^0, got_sighup^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l0 -> l1 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^0, a22^0'=a22^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^0, wakend^0'=wakend^0, got_sighup^0 <= 0, cost: 1 New rule: l0 -> l1 : got_sighup^0 <= 0, cost: 1 Propagated Equalities Original rule: l0 -> l2 : ___rho_2_^0'=___rho_2_^post2, ___rho_3_^0'=___rho_3_^post2, ___rho_4_^0'=___rho_4_^post2, ___rho_5_^0'=___rho_5_^post2, a22^0'=a22^post2, curtime^0'=curtime^post2, got_sighup^0'=got_sighup^post2, last_copy_time^0'=last_copy_time^post2, tt1^0'=tt1^post2, wakend^0'=wakend^post2, (0 == 0 /\ ___rho_4_^0-___rho_4_^post2 == 0 /\ got_sighup^post2 == 0 /\ -___rho_5_^post2+___rho_5_^0 == 0 /\ 1-got_sighup^0 <= 0 /\ -___rho_3_^post2+tt1^post2 == 0 /\ -wakend^post2+wakend^0 == 0 /\ curtime^0-curtime^post2 == 0 /\ -___rho_2_^post2+___rho_2_^0 == 0 /\ last_copy_time^0-last_copy_time^post2 == 0 /\ -1+a22^post2 == 0), cost: 1 New rule: l0 -> l2 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=tt1^post2, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^0, a22^0'=1, curtime^0'=curtime^0, got_sighup^0'=0, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^post2, wakend^0'=wakend^0, (0 == 0 /\ 1-got_sighup^0 <= 0), cost: 1 propagated equality ___rho_4_^post2 = ___rho_4_^0 propagated equality got_sighup^post2 = 0 propagated equality ___rho_5_^post2 = ___rho_5_^0 propagated equality ___rho_3_^post2 = tt1^post2 propagated equality wakend^post2 = wakend^0 propagated equality curtime^post2 = curtime^0 propagated equality ___rho_2_^post2 = ___rho_2_^0 propagated equality last_copy_time^post2 = last_copy_time^0 propagated equality a22^post2 = 1 Simplified Guard Original rule: l0 -> l2 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=tt1^post2, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^0, a22^0'=1, curtime^0'=curtime^0, got_sighup^0'=0, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^post2, wakend^0'=wakend^0, (0 == 0 /\ 1-got_sighup^0 <= 0), cost: 1 New rule: l0 -> l2 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=tt1^post2, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^0, a22^0'=1, curtime^0'=curtime^0, got_sighup^0'=0, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^post2, wakend^0'=wakend^0, 1-got_sighup^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l0 -> l2 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=tt1^post2, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^0, a22^0'=1, curtime^0'=curtime^0, got_sighup^0'=0, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^post2, wakend^0'=wakend^0, 1-got_sighup^0 <= 0, cost: 1 New rule: l0 -> l2 : ___rho_3_^0'=tt1^post2, a22^0'=1, got_sighup^0'=0, tt1^0'=tt1^post2, 1-got_sighup^0 <= 0, cost: 1 Propagated Equalities Original rule: l3 -> l4 : ___rho_2_^0'=___rho_2_^post3, ___rho_3_^0'=___rho_3_^post3, ___rho_4_^0'=___rho_4_^post3, ___rho_5_^0'=___rho_5_^post3, a22^0'=a22^post3, curtime^0'=curtime^post3, got_sighup^0'=got_sighup^post3, last_copy_time^0'=last_copy_time^post3, tt1^0'=tt1^post3, wakend^0'=wakend^post3, (last_copy_time^0-last_copy_time^post3 == 0 /\ -got_sighup^post3+got_sighup^0 == 0 /\ ___rho_3_^0-___rho_3_^post3 == 0 /\ ___rho_4_^0-___rho_4_^post3 == 0 /\ tt1^0-tt1^post3 == 0 /\ -wakend^post3+wakend^0 == 0 /\ -___rho_2_^post3+___rho_2_^0 == 0 /\ -___rho_5_^post3+___rho_5_^0 == 0 /\ a22^0-a22^post3 == 0 /\ curtime^0-curtime^post3 == 0), cost: 1 New rule: l3 -> l4 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^0, a22^0'=a22^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^0, wakend^0'=wakend^0, 0 == 0, cost: 1 propagated equality last_copy_time^post3 = last_copy_time^0 propagated equality got_sighup^post3 = got_sighup^0 propagated equality ___rho_3_^post3 = ___rho_3_^0 propagated equality ___rho_4_^post3 = ___rho_4_^0 propagated equality tt1^post3 = tt1^0 propagated equality wakend^post3 = wakend^0 propagated equality ___rho_2_^post3 = ___rho_2_^0 propagated equality ___rho_5_^post3 = ___rho_5_^0 propagated equality a22^post3 = a22^0 propagated equality curtime^post3 = curtime^0 Simplified Guard Original rule: l3 -> l4 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^0, a22^0'=a22^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^0, wakend^0'=wakend^0, 0 == 0, cost: 1 New rule: l3 -> l4 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^0, a22^0'=a22^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^0, wakend^0'=wakend^0, T, cost: 1 Removed Trivial Updates Original rule: l3 -> l4 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^0, a22^0'=a22^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^0, wakend^0'=wakend^0, T, cost: 1 New rule: l3 -> l4 : T, cost: 1 Propagated Equalities Original rule: l5 -> l6 : ___rho_2_^0'=___rho_2_^post4, ___rho_3_^0'=___rho_3_^post4, ___rho_4_^0'=___rho_4_^post4, ___rho_5_^0'=___rho_5_^post4, a22^0'=a22^post4, curtime^0'=curtime^post4, got_sighup^0'=got_sighup^post4, last_copy_time^0'=last_copy_time^post4, tt1^0'=tt1^post4, wakend^0'=wakend^post4, (curtime^0-curtime^post4 == 0 /\ a22^0-a22^post4 == 0 /\ -tt1^post4+tt1^0 == 0 /\ last_copy_time^0-last_copy_time^post4 == 0 /\ -___rho_5_^post4+___rho_5_^0 == 0 /\ ___rho_3_^0-___rho_3_^post4 == 0 /\ -wakend^post4+wakend^0 == 0 /\ -got_sighup^post4+got_sighup^0 == 0 /\ -___rho_4_^post4+___rho_4_^0 == 0 /\ -___rho_2_^post4+___rho_2_^0 == 0), cost: 1 New rule: l5 -> l6 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^0, a22^0'=a22^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^0, wakend^0'=wakend^0, 0 == 0, cost: 1 propagated equality curtime^post4 = curtime^0 propagated equality a22^post4 = a22^0 propagated equality tt1^post4 = tt1^0 propagated equality last_copy_time^post4 = last_copy_time^0 propagated equality ___rho_5_^post4 = ___rho_5_^0 propagated equality ___rho_3_^post4 = ___rho_3_^0 propagated equality wakend^post4 = wakend^0 propagated equality got_sighup^post4 = got_sighup^0 propagated equality ___rho_4_^post4 = ___rho_4_^0 propagated equality ___rho_2_^post4 = ___rho_2_^0 Simplified Guard Original rule: l5 -> l6 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^0, a22^0'=a22^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^0, wakend^0'=wakend^0, 0 == 0, cost: 1 New rule: l5 -> l6 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^0, a22^0'=a22^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^0, wakend^0'=wakend^0, T, cost: 1 Removed Trivial Updates Original rule: l5 -> l6 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^0, a22^0'=a22^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^0, wakend^0'=wakend^0, T, cost: 1 New rule: l5 -> l6 : T, cost: 1 Propagated Equalities Original rule: l7 -> l5 : ___rho_2_^0'=___rho_2_^post5, ___rho_3_^0'=___rho_3_^post5, ___rho_4_^0'=___rho_4_^post5, ___rho_5_^0'=___rho_5_^post5, a22^0'=a22^post5, curtime^0'=curtime^post5, got_sighup^0'=got_sighup^post5, last_copy_time^0'=last_copy_time^post5, tt1^0'=tt1^post5, wakend^0'=wakend^post5, (0 == 0 /\ -___rho_2_^post5+___rho_2_^0 == 0 /\ -___rho_3_^post5+___rho_3_^0 == 0 /\ -a22^post5+a22^0 == 0 /\ curtime^0-curtime^post5 == 0 /\ last_copy_time^0-last_copy_time^post5 == 0 /\ got_sighup^0-got_sighup^post5 == 0 /\ wakend^0-wakend^post5 == 0 /\ -tt1^post5+tt1^0 == 0 /\ ___rho_4_^0-___rho_4_^post5 == 0), cost: 1 New rule: l7 -> l5 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^post5, a22^0'=a22^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^0, wakend^0'=wakend^0, 0 == 0, cost: 1 propagated equality ___rho_2_^post5 = ___rho_2_^0 propagated equality ___rho_3_^post5 = ___rho_3_^0 propagated equality a22^post5 = a22^0 propagated equality curtime^post5 = curtime^0 propagated equality last_copy_time^post5 = last_copy_time^0 propagated equality got_sighup^post5 = got_sighup^0 propagated equality wakend^post5 = wakend^0 propagated equality tt1^post5 = tt1^0 propagated equality ___rho_4_^post5 = ___rho_4_^0 Simplified Guard Original rule: l7 -> l5 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^post5, a22^0'=a22^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^0, wakend^0'=wakend^0, 0 == 0, cost: 1 New rule: l7 -> l5 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^post5, a22^0'=a22^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^0, wakend^0'=wakend^0, T, cost: 1 Removed Trivial Updates Original rule: l7 -> l5 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^post5, a22^0'=a22^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^0, wakend^0'=wakend^0, T, cost: 1 New rule: l7 -> l5 : ___rho_5_^0'=___rho_5_^post5, T, cost: 1 Propagated Equalities Original rule: l8 -> l7 : ___rho_2_^0'=___rho_2_^post6, ___rho_3_^0'=___rho_3_^post6, ___rho_4_^0'=___rho_4_^post6, ___rho_5_^0'=___rho_5_^post6, a22^0'=a22^post6, curtime^0'=curtime^post6, got_sighup^0'=got_sighup^post6, last_copy_time^0'=last_copy_time^post6, tt1^0'=tt1^post6, wakend^0'=wakend^post6, (-999+curtime^0-last_copy_time^0 <= 0 /\ curtime^0-curtime^post6 == 0 /\ -___rho_3_^post6+___rho_3_^0 == 0 /\ -got_sighup^post6+got_sighup^0 == 0 /\ last_copy_time^0-last_copy_time^post6 == 0 /\ -tt1^post6+tt1^0 == 0 /\ ___rho_5_^0-___rho_5_^post6 == 0 /\ wakend^0-wakend^post6 == 0 /\ ___rho_4_^0-___rho_4_^post6 == 0 /\ -___rho_2_^post6+___rho_2_^0 == 0 /\ -a22^post6+a22^0 == 0), cost: 1 New rule: l8 -> l7 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^0, a22^0'=a22^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^0, wakend^0'=wakend^0, (0 == 0 /\ -999+curtime^0-last_copy_time^0 <= 0), cost: 1 propagated equality curtime^post6 = curtime^0 propagated equality ___rho_3_^post6 = ___rho_3_^0 propagated equality got_sighup^post6 = got_sighup^0 propagated equality last_copy_time^post6 = last_copy_time^0 propagated equality tt1^post6 = tt1^0 propagated equality ___rho_5_^post6 = ___rho_5_^0 propagated equality wakend^post6 = wakend^0 propagated equality ___rho_4_^post6 = ___rho_4_^0 propagated equality ___rho_2_^post6 = ___rho_2_^0 propagated equality a22^post6 = a22^0 Simplified Guard Original rule: l8 -> l7 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^0, a22^0'=a22^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^0, wakend^0'=wakend^0, (0 == 0 /\ -999+curtime^0-last_copy_time^0 <= 0), cost: 1 New rule: l8 -> l7 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^0, a22^0'=a22^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^0, wakend^0'=wakend^0, -999+curtime^0-last_copy_time^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l8 -> l7 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^0, a22^0'=a22^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^0, wakend^0'=wakend^0, -999+curtime^0-last_copy_time^0 <= 0, cost: 1 New rule: l8 -> l7 : -999+curtime^0-last_copy_time^0 <= 0, cost: 1 Propagated Equalities Original rule: l8 -> l7 : ___rho_2_^0'=___rho_2_^post7, ___rho_3_^0'=___rho_3_^post7, ___rho_4_^0'=___rho_4_^post7, ___rho_5_^0'=___rho_5_^post7, a22^0'=a22^post7, curtime^0'=curtime^post7, got_sighup^0'=got_sighup^post7, last_copy_time^0'=last_copy_time^post7, tt1^0'=tt1^post7, wakend^0'=wakend^post7, (-got_sighup^post7+got_sighup^0 == 0 /\ -1+wakend^post7 == 0 /\ -___rho_5_^post7+___rho_5_^0 == 0 /\ -___rho_3_^post7+___rho_3_^0 == 0 /\ a22^0-a22^post7 == 0 /\ ___rho_4_^0-___rho_4_^post7 == 0 /\ curtime^0-curtime^post7 == 0 /\ last_copy_time^0-last_copy_time^post7 == 0 /\ -___rho_2_^post7+___rho_2_^0 == 0 /\ 1000-curtime^0+last_copy_time^0 <= 0 /\ tt1^0-tt1^post7 == 0), cost: 1 New rule: l8 -> l7 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^0, a22^0'=a22^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^0, wakend^0'=1, (0 == 0 /\ 1000-curtime^0+last_copy_time^0 <= 0), cost: 1 propagated equality got_sighup^post7 = got_sighup^0 propagated equality wakend^post7 = 1 propagated equality ___rho_5_^post7 = ___rho_5_^0 propagated equality ___rho_3_^post7 = ___rho_3_^0 propagated equality a22^post7 = a22^0 propagated equality ___rho_4_^post7 = ___rho_4_^0 propagated equality curtime^post7 = curtime^0 propagated equality last_copy_time^post7 = last_copy_time^0 propagated equality ___rho_2_^post7 = ___rho_2_^0 propagated equality tt1^post7 = tt1^0 Simplified Guard Original rule: l8 -> l7 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^0, a22^0'=a22^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^0, wakend^0'=1, (0 == 0 /\ 1000-curtime^0+last_copy_time^0 <= 0), cost: 1 New rule: l8 -> l7 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^0, a22^0'=a22^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^0, wakend^0'=1, 1000-curtime^0+last_copy_time^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l8 -> l7 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^0, a22^0'=a22^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^0, wakend^0'=1, 1000-curtime^0+last_copy_time^0 <= 0, cost: 1 New rule: l8 -> l7 : wakend^0'=1, 1000-curtime^0+last_copy_time^0 <= 0, cost: 1 Propagated Equalities Original rule: l9 -> l7 : ___rho_2_^0'=___rho_2_^post8, ___rho_3_^0'=___rho_3_^post8, ___rho_4_^0'=___rho_4_^post8, ___rho_5_^0'=___rho_5_^post8, a22^0'=a22^post8, curtime^0'=curtime^post8, got_sighup^0'=got_sighup^post8, last_copy_time^0'=last_copy_time^post8, tt1^0'=tt1^post8, wakend^0'=wakend^post8, (___rho_4_^0-___rho_4_^post8 == 0 /\ -___rho_5_^post8+___rho_5_^0 == 0 /\ -got_sighup^post8+got_sighup^0 == 0 /\ ___rho_3_^0-___rho_3_^post8 == 0 /\ a22^0-a22^post8 == 0 /\ -tt1^post8+tt1^0 == 0 /\ -wakend^post8+wakend^0 == 0 /\ -___rho_2_^post8+___rho_2_^0 == 0 /\ curtime^0-curtime^post8 == 0 /\ 1-wakend^0 <= 0 /\ last_copy_time^0-last_copy_time^post8 == 0), cost: 1 New rule: l9 -> l7 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^0, a22^0'=a22^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^0, wakend^0'=wakend^0, (0 == 0 /\ 1-wakend^0 <= 0), cost: 1 propagated equality ___rho_4_^post8 = ___rho_4_^0 propagated equality ___rho_5_^post8 = ___rho_5_^0 propagated equality got_sighup^post8 = got_sighup^0 propagated equality ___rho_3_^post8 = ___rho_3_^0 propagated equality a22^post8 = a22^0 propagated equality tt1^post8 = tt1^0 propagated equality wakend^post8 = wakend^0 propagated equality ___rho_2_^post8 = ___rho_2_^0 propagated equality curtime^post8 = curtime^0 propagated equality last_copy_time^post8 = last_copy_time^0 Simplified Guard Original rule: l9 -> l7 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^0, a22^0'=a22^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^0, wakend^0'=wakend^0, (0 == 0 /\ 1-wakend^0 <= 0), cost: 1 New rule: l9 -> l7 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^0, a22^0'=a22^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^0, wakend^0'=wakend^0, 1-wakend^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l9 -> l7 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^0, a22^0'=a22^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^0, wakend^0'=wakend^0, 1-wakend^0 <= 0, cost: 1 New rule: l9 -> l7 : 1-wakend^0 <= 0, cost: 1 Propagated Equalities Original rule: l9 -> l8 : ___rho_2_^0'=___rho_2_^post9, ___rho_3_^0'=___rho_3_^post9, ___rho_4_^0'=___rho_4_^post9, ___rho_5_^0'=___rho_5_^post9, a22^0'=a22^post9, curtime^0'=curtime^post9, got_sighup^0'=got_sighup^post9, last_copy_time^0'=last_copy_time^post9, tt1^0'=tt1^post9, wakend^0'=wakend^post9, (0 == 0 /\ ___rho_3_^0-___rho_3_^post9 == 0 /\ wakend^0 <= 0 /\ tt1^0-tt1^post9 == 0 /\ ___rho_4_^0-___rho_4_^post9 == 0 /\ -wakend^post9+wakend^0 == 0 /\ -___rho_5_^post9+___rho_5_^0 == 0 /\ a22^0-a22^post9 == 0 /\ -___rho_2_^post9+___rho_2_^0 == 0 /\ -got_sighup^post9+got_sighup^0 == 0 /\ last_copy_time^0-last_copy_time^post9 == 0), cost: 1 New rule: l9 -> l8 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^0, a22^0'=a22^0, curtime^0'=curtime^post9, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^0, wakend^0'=wakend^0, (0 == 0 /\ wakend^0 <= 0), cost: 1 propagated equality ___rho_3_^post9 = ___rho_3_^0 propagated equality tt1^post9 = tt1^0 propagated equality ___rho_4_^post9 = ___rho_4_^0 propagated equality wakend^post9 = wakend^0 propagated equality ___rho_5_^post9 = ___rho_5_^0 propagated equality a22^post9 = a22^0 propagated equality ___rho_2_^post9 = ___rho_2_^0 propagated equality got_sighup^post9 = got_sighup^0 propagated equality last_copy_time^post9 = last_copy_time^0 Simplified Guard Original rule: l9 -> l8 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^0, a22^0'=a22^0, curtime^0'=curtime^post9, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^0, wakend^0'=wakend^0, (0 == 0 /\ wakend^0 <= 0), cost: 1 New rule: l9 -> l8 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^0, a22^0'=a22^0, curtime^0'=curtime^post9, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^0, wakend^0'=wakend^0, wakend^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l9 -> l8 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^0, a22^0'=a22^0, curtime^0'=curtime^post9, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^0, wakend^0'=wakend^0, wakend^0 <= 0, cost: 1 New rule: l9 -> l8 : curtime^0'=curtime^post9, wakend^0 <= 0, cost: 1 Propagated Equalities Original rule: l1 -> l9 : ___rho_2_^0'=___rho_2_^post12, ___rho_3_^0'=___rho_3_^post12, ___rho_4_^0'=___rho_4_^post12, ___rho_5_^0'=___rho_5_^post12, a22^0'=a22^post12, curtime^0'=curtime^post12, got_sighup^0'=got_sighup^post12, last_copy_time^0'=last_copy_time^post12, tt1^0'=tt1^post12, wakend^0'=wakend^post12, (curtime^0-curtime^post12 == 0 /\ got_sighup^0-got_sighup^post12 == 0 /\ -tt1^post12+tt1^0 == 0 /\ wakend^0 <= 0 /\ last_copy_time^0-last_copy_time^post12 == 0 /\ -___rho_3_^post12+___rho_3_^0 == 0 /\ wakend^0-wakend^post12 == 0 /\ ___rho_5_^0-___rho_5_^post12 == 0 /\ -a22^post12+a22^0 == 0 /\ ___rho_4_^0-___rho_4_^post12 == 0 /\ -___rho_2_^post12+___rho_2_^0 == 0), cost: 1 New rule: l1 -> l9 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^0, a22^0'=a22^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^0, wakend^0'=wakend^0, (0 == 0 /\ wakend^0 <= 0), cost: 1 propagated equality curtime^post12 = curtime^0 propagated equality got_sighup^post12 = got_sighup^0 propagated equality tt1^post12 = tt1^0 propagated equality last_copy_time^post12 = last_copy_time^0 propagated equality ___rho_3_^post12 = ___rho_3_^0 propagated equality wakend^post12 = wakend^0 propagated equality ___rho_5_^post12 = ___rho_5_^0 propagated equality a22^post12 = a22^0 propagated equality ___rho_4_^post12 = ___rho_4_^0 propagated equality ___rho_2_^post12 = ___rho_2_^0 Simplified Guard Original rule: l1 -> l9 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^0, a22^0'=a22^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^0, wakend^0'=wakend^0, (0 == 0 /\ wakend^0 <= 0), cost: 1 New rule: l1 -> l9 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^0, a22^0'=a22^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^0, wakend^0'=wakend^0, wakend^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l1 -> l9 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^0, a22^0'=a22^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^0, wakend^0'=wakend^0, wakend^0 <= 0, cost: 1 New rule: l1 -> l9 : wakend^0 <= 0, cost: 1 Propagated Equalities Original rule: l1 -> l9 : ___rho_2_^0'=___rho_2_^post13, ___rho_3_^0'=___rho_3_^post13, ___rho_4_^0'=___rho_4_^post13, ___rho_5_^0'=___rho_5_^post13, a22^0'=a22^post13, curtime^0'=curtime^post13, got_sighup^0'=got_sighup^post13, last_copy_time^0'=last_copy_time^post13, tt1^0'=tt1^post13, wakend^0'=wakend^post13, (0 == 0 /\ wakend^post13 == 0 /\ -got_sighup^post13+got_sighup^0 == 0 /\ -___rho_2_^post13+___rho_2_^0 == 0 /\ -___rho_3_^post13+___rho_3_^0 == 0 /\ -___rho_5_^post13+___rho_5_^0 == 0 /\ a22^0-a22^post13 == 0 /\ last_copy_time^post13-___rho_4_^post13 == 0 /\ -tt1^post13+tt1^0 == 0 /\ curtime^0-curtime^post13 == 0 /\ 1-wakend^0 <= 0), cost: 1 New rule: l1 -> l9 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=last_copy_time^post13, ___rho_5_^0'=___rho_5_^0, a22^0'=a22^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^post13, tt1^0'=tt1^0, wakend^0'=0, (0 == 0 /\ 1-wakend^0 <= 0), cost: 1 propagated equality wakend^post13 = 0 propagated equality got_sighup^post13 = got_sighup^0 propagated equality ___rho_2_^post13 = ___rho_2_^0 propagated equality ___rho_3_^post13 = ___rho_3_^0 propagated equality ___rho_5_^post13 = ___rho_5_^0 propagated equality a22^post13 = a22^0 propagated equality ___rho_4_^post13 = last_copy_time^post13 propagated equality tt1^post13 = tt1^0 propagated equality curtime^post13 = curtime^0 Simplified Guard Original rule: l1 -> l9 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=last_copy_time^post13, ___rho_5_^0'=___rho_5_^0, a22^0'=a22^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^post13, tt1^0'=tt1^0, wakend^0'=0, (0 == 0 /\ 1-wakend^0 <= 0), cost: 1 New rule: l1 -> l9 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=last_copy_time^post13, ___rho_5_^0'=___rho_5_^0, a22^0'=a22^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^post13, tt1^0'=tt1^0, wakend^0'=0, 1-wakend^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l1 -> l9 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=last_copy_time^post13, ___rho_5_^0'=___rho_5_^0, a22^0'=a22^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^post13, tt1^0'=tt1^0, wakend^0'=0, 1-wakend^0 <= 0, cost: 1 New rule: l1 -> l9 : ___rho_4_^0'=last_copy_time^post13, last_copy_time^0'=last_copy_time^post13, wakend^0'=0, 1-wakend^0 <= 0, cost: 1 Propagated Equalities Original rule: l2 -> l1 : ___rho_2_^0'=___rho_2_^post14, ___rho_3_^0'=___rho_3_^post14, ___rho_4_^0'=___rho_4_^post14, ___rho_5_^0'=___rho_5_^post14, a22^0'=a22^post14, curtime^0'=curtime^post14, got_sighup^0'=got_sighup^post14, last_copy_time^0'=last_copy_time^post14, tt1^0'=tt1^post14, wakend^0'=wakend^post14, (-got_sighup^post14+got_sighup^0 == 0 /\ ___rho_3_^0-___rho_3_^post14 == 0 /\ ___rho_4_^0-___rho_4_^post14 == 0 /\ 1-tt1^0 <= 0 /\ -___rho_5_^post14+___rho_5_^0 == 0 /\ -___rho_2_^post14+___rho_2_^0 == 0 /\ a22^0-a22^post14 == 0 /\ -wakend^post14+wakend^0 == 0 /\ -tt1^post14+tt1^0 == 0 /\ last_copy_time^0-last_copy_time^post14 == 0 /\ curtime^0-curtime^post14 == 0), cost: 1 New rule: l2 -> l1 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^0, a22^0'=a22^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^0, wakend^0'=wakend^0, (0 == 0 /\ 1-tt1^0 <= 0), cost: 1 propagated equality got_sighup^post14 = got_sighup^0 propagated equality ___rho_3_^post14 = ___rho_3_^0 propagated equality ___rho_4_^post14 = ___rho_4_^0 propagated equality ___rho_5_^post14 = ___rho_5_^0 propagated equality ___rho_2_^post14 = ___rho_2_^0 propagated equality a22^post14 = a22^0 propagated equality wakend^post14 = wakend^0 propagated equality tt1^post14 = tt1^0 propagated equality last_copy_time^post14 = last_copy_time^0 propagated equality curtime^post14 = curtime^0 Simplified Guard Original rule: l2 -> l1 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^0, a22^0'=a22^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^0, wakend^0'=wakend^0, (0 == 0 /\ 1-tt1^0 <= 0), cost: 1 New rule: l2 -> l1 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^0, a22^0'=a22^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^0, wakend^0'=wakend^0, 1-tt1^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l2 -> l1 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^0, a22^0'=a22^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^0, wakend^0'=wakend^0, 1-tt1^0 <= 0, cost: 1 New rule: l2 -> l1 : 1-tt1^0 <= 0, cost: 1 Propagated Equalities Original rule: l2 -> l5 : ___rho_2_^0'=___rho_2_^post15, ___rho_3_^0'=___rho_3_^post15, ___rho_4_^0'=___rho_4_^post15, ___rho_5_^0'=___rho_5_^post15, a22^0'=a22^post15, curtime^0'=curtime^post15, got_sighup^0'=got_sighup^post15, last_copy_time^0'=last_copy_time^post15, tt1^0'=tt1^post15, wakend^0'=wakend^post15, (tt1^0-tt1^post15 == 0 /\ ___rho_3_^0-___rho_3_^post15 == 0 /\ ___rho_4_^0-___rho_4_^post15 == 0 /\ -___rho_5_^post15+___rho_5_^0 == 0 /\ -___rho_2_^post15+___rho_2_^0 == 0 /\ curtime^0-curtime^post15 == 0 /\ a22^0-a22^post15 == 0 /\ tt1^0 <= 0 /\ -got_sighup^post15+got_sighup^0 == 0 /\ -wakend^post15+wakend^0 == 0 /\ last_copy_time^0-last_copy_time^post15 == 0), cost: 1 New rule: l2 -> l5 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^0, a22^0'=a22^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^0, wakend^0'=wakend^0, (0 == 0 /\ tt1^0 <= 0), cost: 1 propagated equality tt1^post15 = tt1^0 propagated equality ___rho_3_^post15 = ___rho_3_^0 propagated equality ___rho_4_^post15 = ___rho_4_^0 propagated equality ___rho_5_^post15 = ___rho_5_^0 propagated equality ___rho_2_^post15 = ___rho_2_^0 propagated equality curtime^post15 = curtime^0 propagated equality a22^post15 = a22^0 propagated equality got_sighup^post15 = got_sighup^0 propagated equality wakend^post15 = wakend^0 propagated equality last_copy_time^post15 = last_copy_time^0 Simplified Guard Original rule: l2 -> l5 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^0, a22^0'=a22^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^0, wakend^0'=wakend^0, (0 == 0 /\ tt1^0 <= 0), cost: 1 New rule: l2 -> l5 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^0, a22^0'=a22^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^0, wakend^0'=wakend^0, tt1^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l2 -> l5 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^0, a22^0'=a22^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^0, wakend^0'=wakend^0, tt1^0 <= 0, cost: 1 New rule: l2 -> l5 : tt1^0 <= 0, cost: 1 Propagated Equalities Original rule: l12 -> l0 : ___rho_2_^0'=___rho_2_^post16, ___rho_3_^0'=___rho_3_^post16, ___rho_4_^0'=___rho_4_^post16, ___rho_5_^0'=___rho_5_^post16, a22^0'=a22^post16, curtime^0'=curtime^post16, got_sighup^0'=got_sighup^post16, last_copy_time^0'=last_copy_time^post16, tt1^0'=tt1^post16, wakend^0'=wakend^post16, (0 == 0 /\ -1+wakend^post16 == 0 /\ last_copy_time^post17-last_copy_time^post16 == 0 /\ got_sighup^0-got_sighup^post17 == 0 /\ -a22^post16+a22^post17 == 0 /\ -a22^post17+a22^0 == 0 /\ -tt1^post16+tt1^post17 == 0 /\ -___rho_2_^post17+___rho_2_^0 == 0 /\ -wakend^post17+wakend^0 == 0 /\ -___rho_5_^post16+___rho_5_^post17 == 0 /\ ___rho_5_^0-___rho_5_^post17 == 0 /\ ___rho_4_^0-___rho_4_^post17 == 0 /\ -tt1^post17+tt1^0 == 0 /\ -curtime^post16+curtime^post17 == 0 /\ got_sighup^post16-___rho_2_^post16 == 0 /\ -1+wakend^1 == 0 /\ curtime^0-curtime^post17 == 0 /\ last_copy_time^0-last_copy_time^post17 == 0 /\ -___rho_3_^post16+___rho_3_^post17 == 0 /\ -___rho_4_^post16+___rho_4_^post17 == 0 /\ -___rho_3_^post17+___rho_3_^0 == 0), cost: 1 New rule: l12 -> l0 : ___rho_2_^0'=got_sighup^post16, ___rho_3_^0'=___rho_3_^post17, ___rho_4_^0'=___rho_4_^post17, ___rho_5_^0'=___rho_5_^post17, a22^0'=a22^post17, curtime^0'=curtime^post17, got_sighup^0'=got_sighup^post16, last_copy_time^0'=last_copy_time^post17, tt1^0'=tt1^post17, wakend^0'=1, (0 == 0 /\ got_sighup^0-got_sighup^post17 == 0 /\ -a22^post17+a22^0 == 0 /\ -___rho_2_^post17+___rho_2_^0 == 0 /\ -wakend^post17+wakend^0 == 0 /\ ___rho_5_^0-___rho_5_^post17 == 0 /\ ___rho_4_^0-___rho_4_^post17 == 0 /\ -tt1^post17+tt1^0 == 0 /\ -1+wakend^1 == 0 /\ curtime^0-curtime^post17 == 0 /\ last_copy_time^0-last_copy_time^post17 == 0 /\ -___rho_3_^post17+___rho_3_^0 == 0), cost: 1 propagated equality wakend^post16 = 1 propagated equality last_copy_time^post16 = last_copy_time^post17 propagated equality a22^post16 = a22^post17 propagated equality tt1^post16 = tt1^post17 propagated equality ___rho_5_^post16 = ___rho_5_^post17 propagated equality curtime^post16 = curtime^post17 propagated equality ___rho_2_^post16 = got_sighup^post16 propagated equality ___rho_3_^post16 = ___rho_3_^post17 propagated equality ___rho_4_^post16 = ___rho_4_^post17 Propagated Equalities Original rule: l12 -> l0 : ___rho_2_^0'=got_sighup^post16, ___rho_3_^0'=___rho_3_^post17, ___rho_4_^0'=___rho_4_^post17, ___rho_5_^0'=___rho_5_^post17, a22^0'=a22^post17, curtime^0'=curtime^post17, got_sighup^0'=got_sighup^post16, last_copy_time^0'=last_copy_time^post17, tt1^0'=tt1^post17, wakend^0'=1, (0 == 0 /\ got_sighup^0-got_sighup^post17 == 0 /\ -a22^post17+a22^0 == 0 /\ -___rho_2_^post17+___rho_2_^0 == 0 /\ -wakend^post17+wakend^0 == 0 /\ ___rho_5_^0-___rho_5_^post17 == 0 /\ ___rho_4_^0-___rho_4_^post17 == 0 /\ -tt1^post17+tt1^0 == 0 /\ -1+wakend^1 == 0 /\ curtime^0-curtime^post17 == 0 /\ last_copy_time^0-last_copy_time^post17 == 0 /\ -___rho_3_^post17+___rho_3_^0 == 0), cost: 1 New rule: l12 -> l0 : ___rho_2_^0'=got_sighup^post16, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^0, a22^0'=a22^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^post16, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^0, wakend^0'=1, 0 == 0, cost: 1 propagated equality got_sighup^post17 = got_sighup^0 propagated equality a22^post17 = a22^0 propagated equality ___rho_2_^post17 = ___rho_2_^0 propagated equality wakend^post17 = wakend^0 propagated equality ___rho_5_^post17 = ___rho_5_^0 propagated equality ___rho_4_^post17 = ___rho_4_^0 propagated equality tt1^post17 = tt1^0 propagated equality wakend^1 = 1 propagated equality curtime^post17 = curtime^0 propagated equality last_copy_time^post17 = last_copy_time^0 propagated equality ___rho_3_^post17 = ___rho_3_^0 Simplified Guard Original rule: l12 -> l0 : ___rho_2_^0'=got_sighup^post16, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^0, a22^0'=a22^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^post16, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^0, wakend^0'=1, 0 == 0, cost: 1 New rule: l12 -> l0 : ___rho_2_^0'=got_sighup^post16, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^0, a22^0'=a22^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^post16, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^0, wakend^0'=1, T, cost: 1 Removed Trivial Updates Original rule: l12 -> l0 : ___rho_2_^0'=got_sighup^post16, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^0, a22^0'=a22^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^post16, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^0, wakend^0'=1, T, cost: 1 New rule: l12 -> l0 : ___rho_2_^0'=got_sighup^post16, got_sighup^0'=got_sighup^post16, wakend^0'=1, T, cost: 1 Propagated Equalities Original rule: l6 -> l6 : ___rho_2_^0'=___rho_2_^post11, ___rho_3_^0'=___rho_3_^post11, ___rho_4_^0'=___rho_4_^post11, ___rho_5_^0'=___rho_5_^post11, a22^0'=a22^post11, curtime^0'=curtime^post11, got_sighup^0'=got_sighup^post11, last_copy_time^0'=last_copy_time^post11, tt1^0'=tt1^post11, wakend^0'=wakend^post11, (curtime^0-curtime^post10 == 0 /\ wakend^post10-wakend^post11 == 0 /\ a22^0-a22^post10 == 0 /\ -last_copy_time^post11+last_copy_time^post10 == 0 /\ ___rho_2_^post10-___rho_2_^post11 == 0 /\ -tt1^post10+tt1^0 == 0 /\ -___rho_5_^post10+___rho_5_^0 == 0 /\ last_copy_time^0-last_copy_time^post10 == 0 /\ -a22^post11+a22^post10 == 0 /\ got_sighup^post10-got_sighup^post11 == 0 /\ ___rho_4_^post10-___rho_4_^post11 == 0 /\ -wakend^post10+wakend^0 == 0 /\ ___rho_5_^post10-___rho_5_^post11 == 0 /\ ___rho_3_^0-___rho_3_^post10 == 0 /\ tt1^post10-tt1^post11 == 0 /\ -___rho_2_^post10+___rho_2_^0 == 0 /\ curtime^post10-curtime^post11 == 0 /\ -___rho_4_^post10+___rho_4_^0 == 0 /\ ___rho_3_^post10-___rho_3_^post11 == 0 /\ -got_sighup^post10+got_sighup^0 == 0), cost: 1 New rule: l6 -> l6 : ___rho_2_^0'=___rho_2_^post10, ___rho_3_^0'=___rho_3_^post10, ___rho_4_^0'=___rho_4_^post10, ___rho_5_^0'=___rho_5_^post10, a22^0'=a22^post10, curtime^0'=curtime^post10, got_sighup^0'=got_sighup^post10, last_copy_time^0'=last_copy_time^post10, tt1^0'=tt1^post10, wakend^0'=wakend^post10, (0 == 0 /\ curtime^0-curtime^post10 == 0 /\ a22^0-a22^post10 == 0 /\ -tt1^post10+tt1^0 == 0 /\ -___rho_5_^post10+___rho_5_^0 == 0 /\ last_copy_time^0-last_copy_time^post10 == 0 /\ -wakend^post10+wakend^0 == 0 /\ ___rho_3_^0-___rho_3_^post10 == 0 /\ -___rho_2_^post10+___rho_2_^0 == 0 /\ -___rho_4_^post10+___rho_4_^0 == 0 /\ -got_sighup^post10+got_sighup^0 == 0), cost: 1 propagated equality wakend^post11 = wakend^post10 propagated equality last_copy_time^post11 = last_copy_time^post10 propagated equality ___rho_2_^post11 = ___rho_2_^post10 propagated equality a22^post11 = a22^post10 propagated equality got_sighup^post11 = got_sighup^post10 propagated equality ___rho_4_^post11 = ___rho_4_^post10 propagated equality ___rho_5_^post11 = ___rho_5_^post10 propagated equality tt1^post11 = tt1^post10 propagated equality curtime^post11 = curtime^post10 propagated equality ___rho_3_^post11 = ___rho_3_^post10 Propagated Equalities Original rule: l6 -> l6 : ___rho_2_^0'=___rho_2_^post10, ___rho_3_^0'=___rho_3_^post10, ___rho_4_^0'=___rho_4_^post10, ___rho_5_^0'=___rho_5_^post10, a22^0'=a22^post10, curtime^0'=curtime^post10, got_sighup^0'=got_sighup^post10, last_copy_time^0'=last_copy_time^post10, tt1^0'=tt1^post10, wakend^0'=wakend^post10, (0 == 0 /\ curtime^0-curtime^post10 == 0 /\ a22^0-a22^post10 == 0 /\ -tt1^post10+tt1^0 == 0 /\ -___rho_5_^post10+___rho_5_^0 == 0 /\ last_copy_time^0-last_copy_time^post10 == 0 /\ -wakend^post10+wakend^0 == 0 /\ ___rho_3_^0-___rho_3_^post10 == 0 /\ -___rho_2_^post10+___rho_2_^0 == 0 /\ -___rho_4_^post10+___rho_4_^0 == 0 /\ -got_sighup^post10+got_sighup^0 == 0), cost: 1 New rule: l6 -> l6 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^0, a22^0'=a22^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^0, wakend^0'=wakend^0, 0 == 0, cost: 1 propagated equality curtime^post10 = curtime^0 propagated equality a22^post10 = a22^0 propagated equality tt1^post10 = tt1^0 propagated equality ___rho_5_^post10 = ___rho_5_^0 propagated equality last_copy_time^post10 = last_copy_time^0 propagated equality wakend^post10 = wakend^0 propagated equality ___rho_3_^post10 = ___rho_3_^0 propagated equality ___rho_2_^post10 = ___rho_2_^0 propagated equality ___rho_4_^post10 = ___rho_4_^0 propagated equality got_sighup^post10 = got_sighup^0 Simplified Guard Original rule: l6 -> l6 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^0, a22^0'=a22^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^0, wakend^0'=wakend^0, 0 == 0, cost: 1 New rule: l6 -> l6 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^0, a22^0'=a22^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^0, wakend^0'=wakend^0, T, cost: 1 Removed Trivial Updates Original rule: l6 -> l6 : ___rho_2_^0'=___rho_2_^0, ___rho_3_^0'=___rho_3_^0, ___rho_4_^0'=___rho_4_^0, ___rho_5_^0'=___rho_5_^0, a22^0'=a22^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, tt1^0'=tt1^0, wakend^0'=wakend^0, T, cost: 1 New rule: l6 -> l6 : T, cost: 1 Step with 32 Trace 32[T] Blocked [{}, {}] Step with 19 Trace 32[T], 19[(got_sighup^0 <= 0)] Blocked [{}, {}, {}] Step with 29 Trace 32[T], 19[(got_sighup^0 <= 0)], 29[(1-wakend^0 <= 0)] Blocked [{}, {}, {28[T]}, {}] Step with 27 Trace 32[T], 19[(got_sighup^0 <= 0)], 29[(1-wakend^0 <= 0)], 27[(wakend^0 <= 0)] Blocked [{}, {}, {28[T]}, {26[T]}, {}] Step with 24 Trace 32[T], 19[(got_sighup^0 <= 0)], 29[(1-wakend^0 <= 0)], 27[(wakend^0 <= 0)], 24[(-999+curtime^0-last_copy_time^0 <= 0)] Blocked [{}, {}, {28[T]}, {26[T]}, {}, {}] Step with 23 Trace 32[T], 19[(got_sighup^0 <= 0)], 29[(1-wakend^0 <= 0)], 27[(wakend^0 <= 0)], 24[(-999+curtime^0-last_copy_time^0 <= 0)], 23[T] Blocked [{}, {}, {28[T]}, {26[T]}, {}, {}, {}] Step with 22 Trace 32[T], 19[(got_sighup^0 <= 0)], 29[(1-wakend^0 <= 0)], 27[(wakend^0 <= 0)], 24[(-999+curtime^0-last_copy_time^0 <= 0)], 23[T], 22[T] Blocked [{}, {}, {28[T]}, {26[T]}, {}, {}, {}, {}] Step with 33 Trace 32[T], 19[(got_sighup^0 <= 0)], 29[(1-wakend^0 <= 0)], 27[(wakend^0 <= 0)], 24[(-999+curtime^0-last_copy_time^0 <= 0)], 23[T], 22[T], 33[T] Blocked [{}, {}, {28[T]}, {26[T]}, {}, {}, {}, {}, {}] Nonterm Start location: l12 Program variables: ___rho_2_^0 ___rho_3_^0 ___rho_4_^0 ___rho_5_^0 a22^0 curtime^0 got_sighup^0 last_copy_time^0 tt1^0 wakend^0 19: l0 -> l1 : got_sighup^0 <= 0, cost: 1 20: l0 -> l2 : ___rho_3_^0'=tt1^post2, a22^0'=1, got_sighup^0'=0, tt1^0'=tt1^post2, 1-got_sighup^0 <= 0, cost: 1 28: l1 -> l9 : wakend^0 <= 0, cost: 1 29: l1 -> l9 : ___rho_4_^0'=last_copy_time^post13, last_copy_time^0'=last_copy_time^post13, wakend^0'=0, 1-wakend^0 <= 0, cost: 1 30: l2 -> l1 : 1-tt1^0 <= 0, cost: 1 31: l2 -> l5 : tt1^0 <= 0, cost: 1 21: l3 -> l4 : T, cost: 1 22: l5 -> l6 : T, cost: 1 33: l6 -> l6 : T, cost: 1 34: l6 -> LoAT_sink : -1+n >= 0, cost: NONTERM 23: l7 -> l5 : ___rho_5_^0'=___rho_5_^post5, T, cost: 1 24: l8 -> l7 : -999+curtime^0-last_copy_time^0 <= 0, cost: 1 25: l8 -> l7 : wakend^0'=1, 1000-curtime^0+last_copy_time^0 <= 0, cost: 1 26: l9 -> l7 : 1-wakend^0 <= 0, cost: 1 27: l9 -> l8 : curtime^0'=curtime^post9, wakend^0 <= 0, cost: 1 32: l12 -> l0 : ___rho_2_^0'=got_sighup^post16, got_sighup^0'=got_sighup^post16, wakend^0'=1, T, cost: 1 Certificate of Non-Termination Original rule: l6 -> l6 : T, cost: 1 New rule: l6 -> LoAT_sink : -1+n >= 0, cost: NONTERM Replacement map: {} Step with 34 Trace 32[T], 19[(got_sighup^0 <= 0)], 29[(1-wakend^0 <= 0)], 27[(wakend^0 <= 0)], 24[(-999+curtime^0-last_copy_time^0 <= 0)], 23[T], 22[T], 34[-1+n >= 0] Blocked [{}, {}, {28[T]}, {26[T]}, {}, {}, {}, {}, {34[T]}] Refute Counterexample [ ___rho_2_^0=0 ___rho_3_^0=0 ___rho_4_^0=0 ___rho_5_^0=0 a22^0=0 curtime^0=0 got_sighup^0=0 last_copy_time^0=0 tt1^0=0 wakend^0=1 ] 32 [ ___rho_2_^0=0 ___rho_3_^0=0 ___rho_4_^0=0 ___rho_5_^0=0 a22^0=0 curtime^0=0 got_sighup^0=0 last_copy_time^0=0 tt1^0=0 wakend^0=1 ] 19 [ ___rho_2_^0=0 ___rho_3_^0=0 ___rho_4_^0=0 ___rho_5_^0=0 a22^0=0 curtime^0=0 got_sighup^0=0 last_copy_time^0=0 tt1^0=0 wakend^0=0 ] 29 [ ___rho_2_^0=0 ___rho_3_^0=0 ___rho_4_^0=0 ___rho_5_^0=0 a22^0=0 curtime^0=0 got_sighup^0=0 last_copy_time^0=0 tt1^0=0 wakend^0=0 ] 27 [ ___rho_2_^0=0 ___rho_3_^0=0 ___rho_4_^0=0 ___rho_5_^0=0 a22^0=0 curtime^0=0 got_sighup^0=0 last_copy_time^0=0 tt1^0=0 wakend^0=0 ] 24 [ ___rho_2_^0=0 ___rho_3_^0=0 ___rho_4_^0=0 ___rho_5_^0=0 a22^0=0 curtime^0=0 got_sighup^0=0 last_copy_time^0=0 tt1^0=0 wakend^0=0 ] 23 [ ___rho_2_^0=0 ___rho_3_^0=0 ___rho_4_^0=0 ___rho_5_^0=0 a22^0=0 curtime^0=0 got_sighup^0=0 last_copy_time^0=0 tt1^0=0 wakend^0=0 ] 22 [ ___rho_2_^0=___rho_2_^0 ___rho_3_^0=0 ___rho_4_^0=0 ___rho_5_^0=0 a22^0=0 curtime^0=0 got_sighup^0=got_sighup^0 last_copy_time^0=0 tt1^0=0 wakend^0=wakend^0 ] 34 NO Build SHA: a05f16bf13df659c382799650051f91bf6828c7b