NO Initial ITS Start location: l12 Program variables: ___rho_1_^0 ___rho_2_^0 ___rho_4_^0 a33^0 a55^0 a88^0 curtime^0 got_sighup^0 last_copy_time^0 ret_time1010^0 ret_time77^0 ret_xlogarchivingactive44^0 tmp2^0 tmp66^0 tmp99^0 tt1^0 wakend^0 0: l0 -> l1 : ___rho_1_^0'=___rho_1_^post1, ___rho_2_^0'=___rho_2_^post1, ___rho_4_^0'=___rho_4_^post1, a33^0'=a33^post1, a55^0'=a55^post1, a88^0'=a88^post1, curtime^0'=curtime^post1, got_sighup^0'=got_sighup^post1, last_copy_time^0'=last_copy_time^post1, ret_time1010^0'=ret_time1010^post1, ret_time77^0'=ret_time77^post1, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post1, tmp2^0'=tmp2^post1, tmp66^0'=tmp66^post1, tmp99^0'=tmp99^post1, tt1^0'=tt1^post1, wakend^0'=wakend^post1, (tmp99^0-tmp99^post1 == 0 /\ -wakend^post1+wakend^0 == 0 /\ -a88^post1+a88^0 == 0 /\ -___rho_1_^post1+___rho_1_^0 == 0 /\ -___rho_4_^post1+___rho_4_^0 == 0 /\ -a33^post1+a33^0 == 0 /\ -tt1^post1+tt1^0 == 0 /\ tmp2^0-tmp2^post1 == 0 /\ ret_time77^0-ret_time77^post1 == 0 /\ last_copy_time^0-last_copy_time^post1 == 0 /\ ___rho_2_^0-___rho_2_^post1 == 0 /\ got_sighup^0 <= 0 /\ -ret_time1010^post1+ret_time1010^0 == 0 /\ a55^0-a55^post1 == 0 /\ -curtime^post1+curtime^0 == 0 /\ -got_sighup^post1+got_sighup^0 == 0 /\ -tmp66^post1+tmp66^0 == 0 /\ ret_xlogarchivingactive44^0-ret_xlogarchivingactive44^post1 == 0), cost: 1 1: l0 -> l2 : ___rho_1_^0'=___rho_1_^post2, ___rho_2_^0'=___rho_2_^post2, ___rho_4_^0'=___rho_4_^post2, a33^0'=a33^post2, a55^0'=a55^post2, a88^0'=a88^post2, curtime^0'=curtime^post2, got_sighup^0'=got_sighup^post2, last_copy_time^0'=last_copy_time^post2, ret_time1010^0'=ret_time1010^post2, ret_time77^0'=ret_time77^post2, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post2, tmp2^0'=tmp2^post2, tmp66^0'=tmp66^post2, tmp99^0'=tmp99^post2, tt1^0'=tt1^post2, wakend^0'=wakend^post2, (0 == 0 /\ got_sighup^post2 == 0 /\ -ret_time77^post2+ret_time77^0 == 0 /\ -last_copy_time^post2+last_copy_time^0 == 0 /\ ___rho_4_^0-___rho_4_^post2 == 0 /\ ret_time1010^0-ret_time1010^post2 == 0 /\ -tmp66^post2+tmp66^0 == 0 /\ 1-got_sighup^0 <= 0 /\ -curtime^post2+curtime^0 == 0 /\ -1+a33^post2 == 0 /\ -a55^post2+a55^0 == 0 /\ -___rho_2_^post2+ret_xlogarchivingactive44^post2 == 0 /\ -___rho_1_^post2+___rho_1_^0 == 0 /\ -ret_xlogarchivingactive44^post2+tmp2^post2 == 0 /\ -wakend^post2+wakend^0 == 0 /\ tmp99^0-tmp99^post2 == 0 /\ a88^0-a88^post2 == 0 /\ tt1^post2-tmp2^post2 == 0), cost: 1 9: l1 -> l9 : ___rho_1_^0'=___rho_1_^post10, ___rho_2_^0'=___rho_2_^post10, ___rho_4_^0'=___rho_4_^post10, a33^0'=a33^post10, a55^0'=a55^post10, a88^0'=a88^post10, curtime^0'=curtime^post10, got_sighup^0'=got_sighup^post10, last_copy_time^0'=last_copy_time^post10, ret_time1010^0'=ret_time1010^post10, ret_time77^0'=ret_time77^post10, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post10, tmp2^0'=tmp2^post10, tmp66^0'=tmp66^post10, tmp99^0'=tmp99^post10, tt1^0'=tt1^post10, wakend^0'=wakend^post10, (ret_xlogarchivingactive44^0-ret_xlogarchivingactive44^post10 == 0 /\ -wakend^post10+wakend^0 == 0 /\ -last_copy_time^post10+last_copy_time^0 == 0 /\ -tt1^post10+tt1^0 == 0 /\ tmp2^0-tmp2^post10 == 0 /\ -tmp99^post10+tmp99^0 == 0 /\ -ret_time1010^post10+ret_time1010^0 == 0 /\ -got_sighup^post10+got_sighup^0 == 0 /\ a88^0-a88^post10 == 0 /\ wakend^0 <= 0 /\ -a33^post10+a33^0 == 0 /\ -a55^post10+a55^0 == 0 /\ -___rho_2_^post10+___rho_2_^0 == 0 /\ curtime^0-curtime^post10 == 0 /\ -___rho_1_^post10+___rho_1_^0 == 0 /\ -ret_time77^post10+ret_time77^0 == 0 /\ ___rho_4_^0-___rho_4_^post10 == 0 /\ -tmp66^post10+tmp66^0 == 0), cost: 1 10: l1 -> l9 : ___rho_1_^0'=___rho_1_^post11, ___rho_2_^0'=___rho_2_^post11, ___rho_4_^0'=___rho_4_^post11, a33^0'=a33^post11, a55^0'=a55^post11, a88^0'=a88^post11, curtime^0'=curtime^post11, got_sighup^0'=got_sighup^post11, last_copy_time^0'=last_copy_time^post11, ret_time1010^0'=ret_time1010^post11, ret_time77^0'=ret_time77^post11, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post11, tmp2^0'=tmp2^post11, tmp66^0'=tmp66^post11, tmp99^0'=tmp99^post11, tt1^0'=tt1^post11, wakend^0'=wakend^post11, (0 == 0 /\ -a88^post11+a88^0 == 0 /\ 1-wakend^0 <= 0 /\ -___rho_4_^post11+___rho_4_^0 == 0 /\ -a33^post11+a33^0 == 0 /\ -___rho_1_^post11+___rho_1_^0 == 0 /\ tmp99^0-tmp99^post11 == 0 /\ wakend^post11 == 0 /\ ___rho_2_^0-___rho_2_^post11 == 0 /\ -tt1^post11+tt1^0 == 0 /\ a55^post11 == 0 /\ ret_xlogarchivingactive44^0-ret_xlogarchivingactive44^post11 == 0 /\ -tmp66^post11+ret_time77^post11 == 0 /\ -ret_time1010^post11+ret_time1010^0 == 0 /\ -tmp2^post11+tmp2^0 == 0 /\ -curtime^post11+curtime^0 == 0 /\ -got_sighup^post11+got_sighup^0 == 0 /\ -ret_time77^post11+last_copy_time^post11 == 0), cost: 1 13: l2 -> l1 : ___rho_1_^0'=___rho_1_^post14, ___rho_2_^0'=___rho_2_^post14, ___rho_4_^0'=___rho_4_^post14, a33^0'=a33^post14, a55^0'=a55^post14, a88^0'=a88^post14, curtime^0'=curtime^post14, got_sighup^0'=got_sighup^post14, last_copy_time^0'=last_copy_time^post14, ret_time1010^0'=ret_time1010^post14, ret_time77^0'=ret_time77^post14, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post14, tmp2^0'=tmp2^post14, tmp66^0'=tmp66^post14, tmp99^0'=tmp99^post14, tt1^0'=tt1^post14, wakend^0'=wakend^post14, (-ret_xlogarchivingactive44^post14+ret_xlogarchivingactive44^0 == 0 /\ -tmp99^post14+tmp99^0 == 0 /\ got_sighup^0-got_sighup^post14 == 0 /\ -curtime^post14+curtime^0 == 0 /\ -___rho_2_^post14+___rho_2_^0 == 0 /\ -last_copy_time^post14+last_copy_time^0 == 0 /\ tmp2^0-tmp2^post14 == 0 /\ -a33^post14+a33^0 == 0 /\ ___rho_4_^0-___rho_4_^post14 == 0 /\ ret_time77^0-ret_time77^post14 == 0 /\ a88^0-a88^post14 == 0 /\ -___rho_1_^post14+___rho_1_^0 == 0 /\ -a55^post14+a55^0 == 0 /\ -tt1^post14+tt1^0 == 0 /\ 1-tt1^0 <= 0 /\ wakend^0-wakend^post14 == 0 /\ tmp66^0-tmp66^post14 == 0 /\ -ret_time1010^post14+ret_time1010^0 == 0), cost: 1 14: l2 -> l5 : ___rho_1_^0'=___rho_1_^post15, ___rho_2_^0'=___rho_2_^post15, ___rho_4_^0'=___rho_4_^post15, a33^0'=a33^post15, a55^0'=a55^post15, a88^0'=a88^post15, curtime^0'=curtime^post15, got_sighup^0'=got_sighup^post15, last_copy_time^0'=last_copy_time^post15, ret_time1010^0'=ret_time1010^post15, ret_time77^0'=ret_time77^post15, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post15, tmp2^0'=tmp2^post15, tmp66^0'=tmp66^post15, tmp99^0'=tmp99^post15, tt1^0'=tt1^post15, wakend^0'=wakend^post15, (ret_xlogarchivingactive44^0-ret_xlogarchivingactive44^post15 == 0 /\ -last_copy_time^post15+last_copy_time^0 == 0 /\ ___rho_4_^0-___rho_4_^post15 == 0 /\ -a55^post15+a55^0 == 0 /\ -___rho_1_^post15+___rho_1_^0 == 0 /\ -got_sighup^post15+got_sighup^0 == 0 /\ a88^0-a88^post15 == 0 /\ -tt1^post15+tt1^0 == 0 /\ -ret_time1010^post15+ret_time1010^0 == 0 /\ -tmp99^post15+tmp99^0 == 0 /\ curtime^0-curtime^post15 == 0 /\ wakend^0-wakend^post15 == 0 /\ -tmp66^post15+tmp66^0 == 0 /\ -a33^post15+a33^0 == 0 /\ -___rho_2_^post15+___rho_2_^0 == 0 /\ tmp2^0-tmp2^post15 == 0 /\ tt1^0 <= 0 /\ -ret_time77^post15+ret_time77^0 == 0), cost: 1 2: l3 -> l4 : ___rho_1_^0'=___rho_1_^post3, ___rho_2_^0'=___rho_2_^post3, ___rho_4_^0'=___rho_4_^post3, a33^0'=a33^post3, a55^0'=a55^post3, a88^0'=a88^post3, curtime^0'=curtime^post3, got_sighup^0'=got_sighup^post3, last_copy_time^0'=last_copy_time^post3, ret_time1010^0'=ret_time1010^post3, ret_time77^0'=ret_time77^post3, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post3, tmp2^0'=tmp2^post3, tmp66^0'=tmp66^post3, tmp99^0'=tmp99^post3, tt1^0'=tt1^post3, wakend^0'=wakend^post3, (-___rho_1_^post3+___rho_1_^0 == 0 /\ -got_sighup^post3+got_sighup^0 == 0 /\ tmp99^0-tmp99^post3 == 0 /\ tmp2^0-tmp2^post3 == 0 /\ -last_copy_time^post3+last_copy_time^0 == 0 /\ -___rho_4_^post3+___rho_4_^0 == 0 /\ -tt1^post3+tt1^0 == 0 /\ ret_time77^0-ret_time77^post3 == 0 /\ ___rho_2_^0-___rho_2_^post3 == 0 /\ -curtime^post3+curtime^0 == 0 /\ -ret_time1010^post3+ret_time1010^0 == 0 /\ -tmp66^post3+tmp66^0 == 0 /\ -wakend^post3+wakend^0 == 0 /\ a88^0-a88^post3 == 0 /\ ret_xlogarchivingactive44^0-ret_xlogarchivingactive44^post3 == 0 /\ a55^0-a55^post3 == 0 /\ -a33^post3+a33^0 == 0), cost: 1 3: l5 -> l6 : ___rho_1_^0'=___rho_1_^post4, ___rho_2_^0'=___rho_2_^post4, ___rho_4_^0'=___rho_4_^post4, a33^0'=a33^post4, a55^0'=a55^post4, a88^0'=a88^post4, curtime^0'=curtime^post4, got_sighup^0'=got_sighup^post4, last_copy_time^0'=last_copy_time^post4, ret_time1010^0'=ret_time1010^post4, ret_time77^0'=ret_time77^post4, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post4, tmp2^0'=tmp2^post4, tmp66^0'=tmp66^post4, tmp99^0'=tmp99^post4, tt1^0'=tt1^post4, wakend^0'=wakend^post4, (wakend^0-wakend^post4 == 0 /\ -curtime^post4+curtime^0 == 0 /\ -ret_time1010^post4+ret_time1010^0 == 0 /\ -tmp66^post4+tmp66^0 == 0 /\ -a33^post4+a33^0 == 0 /\ ___rho_4_^0-___rho_4_^post4 == 0 /\ tmp2^0-tmp2^post4 == 0 /\ -___rho_2_^post4+___rho_2_^0 == 0 /\ got_sighup^0-got_sighup^post4 == 0 /\ -tt1^post4+tt1^0 == 0 /\ a88^0-a88^post4 == 0 /\ ret_time77^0-ret_time77^post4 == 0 /\ -ret_xlogarchivingactive44^post4+ret_xlogarchivingactive44^0 == 0 /\ -___rho_1_^post4+___rho_1_^0 == 0 /\ -a55^post4+a55^0 == 0 /\ -tmp99^post4+tmp99^0 == 0 /\ -last_copy_time^post4+last_copy_time^0 == 0), cost: 1 11: l6 -> l10 : ___rho_1_^0'=___rho_1_^post12, ___rho_2_^0'=___rho_2_^post12, ___rho_4_^0'=___rho_4_^post12, a33^0'=a33^post12, a55^0'=a55^post12, a88^0'=a88^post12, curtime^0'=curtime^post12, got_sighup^0'=got_sighup^post12, last_copy_time^0'=last_copy_time^post12, ret_time1010^0'=ret_time1010^post12, ret_time77^0'=ret_time77^post12, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post12, tmp2^0'=tmp2^post12, tmp66^0'=tmp66^post12, tmp99^0'=tmp99^post12, tt1^0'=tt1^post12, wakend^0'=wakend^post12, (tmp99^0-tmp99^post12 == 0 /\ -last_copy_time^post12+last_copy_time^0 == 0 /\ -tmp66^post12+tmp66^0 == 0 /\ tmp2^0-tmp2^post12 == 0 /\ wakend^0-wakend^post12 == 0 /\ a55^0-a55^post12 == 0 /\ got_sighup^0-got_sighup^post12 == 0 /\ ret_time77^0-ret_time77^post12 == 0 /\ -ret_time1010^post12+ret_time1010^0 == 0 /\ a88^0-a88^post12 == 0 /\ -curtime^post12+curtime^0 == 0 /\ -ret_xlogarchivingactive44^post12+ret_xlogarchivingactive44^0 == 0 /\ -___rho_1_^post12+___rho_1_^0 == 0 /\ -tt1^post12+tt1^0 == 0 /\ -a33^post12+a33^0 == 0 /\ ___rho_4_^0-___rho_4_^post12 == 0 /\ ___rho_2_^0-___rho_2_^post12 == 0), cost: 1 4: l7 -> l5 : ___rho_1_^0'=___rho_1_^post5, ___rho_2_^0'=___rho_2_^post5, ___rho_4_^0'=___rho_4_^post5, a33^0'=a33^post5, a55^0'=a55^post5, a88^0'=a88^post5, curtime^0'=curtime^post5, got_sighup^0'=got_sighup^post5, last_copy_time^0'=last_copy_time^post5, ret_time1010^0'=ret_time1010^post5, ret_time77^0'=ret_time77^post5, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post5, tmp2^0'=tmp2^post5, tmp66^0'=tmp66^post5, tmp99^0'=tmp99^post5, tt1^0'=tt1^post5, wakend^0'=wakend^post5, (0 == 0 /\ -tt1^post5+tt1^0 == 0 /\ -___rho_2_^post5+___rho_2_^0 == 0 /\ -___rho_1_^post5+___rho_1_^0 == 0 /\ tmp2^0-tmp2^post5 == 0 /\ -wakend^post5+wakend^0 == 0 /\ -last_copy_time^post5+last_copy_time^0 == 0 /\ -tmp99^post5+tmp99^0 == 0 /\ -a55^post5+a55^0 == 0 /\ curtime^0-curtime^post5 == 0 /\ a33^0-a33^post5 == 0 /\ -got_sighup^post5+got_sighup^0 == 0 /\ -ret_time1010^post5+ret_time1010^0 == 0 /\ -ret_time77^post5+ret_time77^0 == 0 /\ -tmp66^post5+tmp66^0 == 0 /\ a88^0-a88^post5 == 0 /\ ret_xlogarchivingactive44^0-ret_xlogarchivingactive44^post5 == 0), cost: 1 5: l8 -> l7 : ___rho_1_^0'=___rho_1_^post6, ___rho_2_^0'=___rho_2_^post6, ___rho_4_^0'=___rho_4_^post6, a33^0'=a33^post6, a55^0'=a55^post6, a88^0'=a88^post6, curtime^0'=curtime^post6, got_sighup^0'=got_sighup^post6, last_copy_time^0'=last_copy_time^post6, ret_time1010^0'=ret_time1010^post6, ret_time77^0'=ret_time77^post6, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post6, tmp2^0'=tmp2^post6, tmp66^0'=tmp66^post6, tmp99^0'=tmp99^post6, tt1^0'=tt1^post6, wakend^0'=wakend^post6, (tmp2^0-tmp2^post6 == 0 /\ -tmp66^post6+tmp66^0 == 0 /\ -last_copy_time^post6+last_copy_time^0 == 0 /\ tmp99^0-tmp99^post6 == 0 /\ ___rho_2_^0-___rho_2_^post6 == 0 /\ -curtime^post6+curtime^0 == 0 /\ ret_time77^0-ret_time77^post6 == 0 /\ a88^0-a88^post6 == 0 /\ got_sighup^0-got_sighup^post6 == 0 /\ -999-last_copy_time^0+curtime^0 <= 0 /\ ___rho_4_^0-___rho_4_^post6 == 0 /\ wakend^0-wakend^post6 == 0 /\ -a33^post6+a33^0 == 0 /\ -ret_time1010^post6+ret_time1010^0 == 0 /\ a55^0-a55^post6 == 0 /\ -ret_xlogarchivingactive44^post6+ret_xlogarchivingactive44^0 == 0 /\ -tt1^post6+tt1^0 == 0 /\ -___rho_1_^post6+___rho_1_^0 == 0), cost: 1 6: l8 -> l7 : ___rho_1_^0'=___rho_1_^post7, ___rho_2_^0'=___rho_2_^post7, ___rho_4_^0'=___rho_4_^post7, a33^0'=a33^post7, a55^0'=a55^post7, a88^0'=a88^post7, curtime^0'=curtime^post7, got_sighup^0'=got_sighup^post7, last_copy_time^0'=last_copy_time^post7, ret_time1010^0'=ret_time1010^post7, ret_time77^0'=ret_time77^post7, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post7, tmp2^0'=tmp2^post7, tmp66^0'=tmp66^post7, tmp99^0'=tmp99^post7, tt1^0'=tt1^post7, wakend^0'=wakend^post7, (a88^0-a88^post7 == 0 /\ -a55^post7+a55^0 == 0 /\ -___rho_1_^post7+___rho_1_^0 == 0 /\ -tt1^post7+tt1^0 == 0 /\ -ret_time77^post7+ret_time77^0 == 0 /\ -tmp66^post7+tmp66^0 == 0 /\ 1000+last_copy_time^0-curtime^0 <= 0 /\ -tmp99^post7+tmp99^0 == 0 /\ ___rho_4_^0-___rho_4_^post7 == 0 /\ -last_copy_time^post7+last_copy_time^0 == 0 /\ -a33^post7+a33^0 == 0 /\ -___rho_2_^post7+___rho_2_^0 == 0 /\ -got_sighup^post7+got_sighup^0 == 0 /\ tmp2^0-tmp2^post7 == 0 /\ ret_xlogarchivingactive44^0-ret_xlogarchivingactive44^post7 == 0 /\ -ret_time1010^post7+ret_time1010^0 == 0 /\ -1+wakend^post7 == 0 /\ curtime^0-curtime^post7 == 0), cost: 1 7: l9 -> l7 : ___rho_1_^0'=___rho_1_^post8, ___rho_2_^0'=___rho_2_^post8, ___rho_4_^0'=___rho_4_^post8, a33^0'=a33^post8, a55^0'=a55^post8, a88^0'=a88^post8, curtime^0'=curtime^post8, got_sighup^0'=got_sighup^post8, last_copy_time^0'=last_copy_time^post8, ret_time1010^0'=ret_time1010^post8, ret_time77^0'=ret_time77^post8, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post8, tmp2^0'=tmp2^post8, tmp66^0'=tmp66^post8, tmp99^0'=tmp99^post8, tt1^0'=tt1^post8, wakend^0'=wakend^post8, (1-wakend^0 <= 0 /\ tmp2^0-tmp2^post8 == 0 /\ ret_xlogarchivingactive44^0-ret_xlogarchivingactive44^post8 == 0 /\ -tmp66^post8+tmp66^0 == 0 /\ -last_copy_time^post8+last_copy_time^0 == 0 /\ tmp99^0-tmp99^post8 == 0 /\ -got_sighup^post8+got_sighup^0 == 0 /\ a88^0-a88^post8 == 0 /\ -a55^post8+a55^0 == 0 /\ -wakend^post8+wakend^0 == 0 /\ -___rho_2_^post8+___rho_2_^0 == 0 /\ -ret_time1010^post8+ret_time1010^0 == 0 /\ ___rho_4_^0-___rho_4_^post8 == 0 /\ -curtime^post8+curtime^0 == 0 /\ -a33^post8+a33^0 == 0 /\ -___rho_1_^post8+___rho_1_^0 == 0 /\ -tt1^post8+tt1^0 == 0 /\ -ret_time77^post8+ret_time77^0 == 0), cost: 1 8: l9 -> l8 : ___rho_1_^0'=___rho_1_^post9, ___rho_2_^0'=___rho_2_^post9, ___rho_4_^0'=___rho_4_^post9, a33^0'=a33^post9, a55^0'=a55^post9, a88^0'=a88^post9, curtime^0'=curtime^post9, got_sighup^0'=got_sighup^post9, last_copy_time^0'=last_copy_time^post9, ret_time1010^0'=ret_time1010^post9, ret_time77^0'=ret_time77^post9, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post9, tmp2^0'=tmp2^post9, tmp66^0'=tmp66^post9, tmp99^0'=tmp99^post9, tt1^0'=tt1^post9, wakend^0'=wakend^post9, (0 == 0 /\ ret_time77^0-ret_time77^post9 == 0 /\ a88^post9 == 0 /\ a55^0-a55^post9 == 0 /\ -a33^post9+a33^0 == 0 /\ -___rho_1_^post9+___rho_1_^0 == 0 /\ -tt1^post9+tt1^0 == 0 /\ ___rho_2_^0-___rho_2_^post9 == 0 /\ last_copy_time^0-last_copy_time^post9 == 0 /\ wakend^0 <= 0 /\ got_sighup^0-got_sighup^post9 == 0 /\ -tmp66^post9+tmp66^0 == 0 /\ -ret_time1010^post9+curtime^post9 == 0 /\ -___rho_4_^post9+___rho_4_^0 == 0 /\ ret_xlogarchivingactive44^0-ret_xlogarchivingactive44^post9 == 0 /\ tmp2^0-tmp2^post9 == 0 /\ -wakend^post9+wakend^0 == 0 /\ ret_time1010^post9-tmp99^post9 == 0), cost: 1 12: l10 -> l6 : ___rho_1_^0'=___rho_1_^post13, ___rho_2_^0'=___rho_2_^post13, ___rho_4_^0'=___rho_4_^post13, a33^0'=a33^post13, a55^0'=a55^post13, a88^0'=a88^post13, curtime^0'=curtime^post13, got_sighup^0'=got_sighup^post13, last_copy_time^0'=last_copy_time^post13, ret_time1010^0'=ret_time1010^post13, ret_time77^0'=ret_time77^post13, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post13, tmp2^0'=tmp2^post13, tmp66^0'=tmp66^post13, tmp99^0'=tmp99^post13, tt1^0'=tt1^post13, wakend^0'=wakend^post13, (-a55^post13+a55^0 == 0 /\ a88^0-a88^post13 == 0 /\ -___rho_1_^post13+___rho_1_^0 == 0 /\ -___rho_2_^post13+___rho_2_^0 == 0 /\ -ret_time77^post13+ret_time77^0 == 0 /\ -tt1^post13+tt1^0 == 0 /\ tmp99^0-tmp99^post13 == 0 /\ ___rho_4_^0-___rho_4_^post13 == 0 /\ -last_copy_time^post13+last_copy_time^0 == 0 /\ ret_xlogarchivingactive44^0-ret_xlogarchivingactive44^post13 == 0 /\ -ret_time1010^post13+ret_time1010^0 == 0 /\ -wakend^post13+wakend^0 == 0 /\ tmp66^0-tmp66^post13 == 0 /\ tmp2^0-tmp2^post13 == 0 /\ -got_sighup^post13+got_sighup^0 == 0 /\ curtime^0-curtime^post13 == 0 /\ a33^0-a33^post13 == 0), cost: 1 15: l11 -> l0 : ___rho_1_^0'=___rho_1_^post16, ___rho_2_^0'=___rho_2_^post16, ___rho_4_^0'=___rho_4_^post16, a33^0'=a33^post16, a55^0'=a55^post16, a88^0'=a88^post16, curtime^0'=curtime^post16, got_sighup^0'=got_sighup^post16, last_copy_time^0'=last_copy_time^post16, ret_time1010^0'=ret_time1010^post16, ret_time77^0'=ret_time77^post16, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post16, tmp2^0'=tmp2^post16, tmp66^0'=tmp66^post16, tmp99^0'=tmp99^post16, tt1^0'=tt1^post16, wakend^0'=wakend^post16, (0 == 0 /\ a55^0-a55^post16 == 0 /\ -last_copy_time^post16+last_copy_time^0 == 0 /\ -1+wakend^post16 == 0 /\ -ret_time1010^post16+ret_time1010^0 == 0 /\ -tmp66^post16+tmp66^0 == 0 /\ a88^0-a88^post16 == 0 /\ -curtime^post16+curtime^0 == 0 /\ tmp2^0-tmp2^post16 == 0 /\ -___rho_4_^post16+___rho_4_^0 == 0 /\ -a33^post16+a33^0 == 0 /\ -tt1^post16+tt1^0 == 0 /\ -1+wakend^1 == 0 /\ ret_time77^0-ret_time77^post16 == 0 /\ -___rho_2_^0+got_sighup^post16 == 0 /\ ___rho_2_^0-___rho_2_^post16 == 0 /\ -tmp99^post16+tmp99^0 == 0 /\ -ret_xlogarchivingactive44^post16+ret_xlogarchivingactive44^0 == 0), cost: 1 16: l12 -> l11 : ___rho_1_^0'=___rho_1_^post17, ___rho_2_^0'=___rho_2_^post17, ___rho_4_^0'=___rho_4_^post17, a33^0'=a33^post17, a55^0'=a55^post17, a88^0'=a88^post17, curtime^0'=curtime^post17, got_sighup^0'=got_sighup^post17, last_copy_time^0'=last_copy_time^post17, ret_time1010^0'=ret_time1010^post17, ret_time77^0'=ret_time77^post17, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post17, tmp2^0'=tmp2^post17, tmp66^0'=tmp66^post17, tmp99^0'=tmp99^post17, tt1^0'=tt1^post17, wakend^0'=wakend^post17, (-___rho_1_^post17+___rho_1_^0 == 0 /\ -___rho_2_^post17+___rho_2_^0 == 0 /\ -a55^post17+a55^0 == 0 /\ -got_sighup^post17+got_sighup^0 == 0 /\ a88^0-a88^post17 == 0 /\ -tmp2^post17+tmp2^0 == 0 /\ ret_xlogarchivingactive44^0-ret_xlogarchivingactive44^post17 == 0 /\ -tt1^post17+tt1^0 == 0 /\ -ret_time77^post17+ret_time77^0 == 0 /\ -ret_time1010^post17+ret_time1010^0 == 0 /\ ___rho_4_^0-___rho_4_^post17 == 0 /\ -tmp66^post17+tmp66^0 == 0 /\ -wakend^post17+wakend^0 == 0 /\ tmp99^0-tmp99^post17 == 0 /\ -last_copy_time^post17+last_copy_time^0 == 0 /\ curtime^0-curtime^post17 == 0 /\ a33^0-a33^post17 == 0), cost: 1 Chained Linear Paths Start location: l12 Program variables: ___rho_1_^0 ___rho_2_^0 ___rho_4_^0 a33^0 a55^0 a88^0 curtime^0 got_sighup^0 last_copy_time^0 ret_time1010^0 ret_time77^0 ret_xlogarchivingactive44^0 tmp2^0 tmp66^0 tmp99^0 tt1^0 wakend^0 0: l0 -> l1 : ___rho_1_^0'=___rho_1_^post1, ___rho_2_^0'=___rho_2_^post1, ___rho_4_^0'=___rho_4_^post1, a33^0'=a33^post1, a55^0'=a55^post1, a88^0'=a88^post1, curtime^0'=curtime^post1, got_sighup^0'=got_sighup^post1, last_copy_time^0'=last_copy_time^post1, ret_time1010^0'=ret_time1010^post1, ret_time77^0'=ret_time77^post1, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post1, tmp2^0'=tmp2^post1, tmp66^0'=tmp66^post1, tmp99^0'=tmp99^post1, tt1^0'=tt1^post1, wakend^0'=wakend^post1, (tmp99^0-tmp99^post1 == 0 /\ -wakend^post1+wakend^0 == 0 /\ -a88^post1+a88^0 == 0 /\ -___rho_1_^post1+___rho_1_^0 == 0 /\ -___rho_4_^post1+___rho_4_^0 == 0 /\ -a33^post1+a33^0 == 0 /\ -tt1^post1+tt1^0 == 0 /\ tmp2^0-tmp2^post1 == 0 /\ ret_time77^0-ret_time77^post1 == 0 /\ last_copy_time^0-last_copy_time^post1 == 0 /\ ___rho_2_^0-___rho_2_^post1 == 0 /\ got_sighup^0 <= 0 /\ -ret_time1010^post1+ret_time1010^0 == 0 /\ a55^0-a55^post1 == 0 /\ -curtime^post1+curtime^0 == 0 /\ -got_sighup^post1+got_sighup^0 == 0 /\ -tmp66^post1+tmp66^0 == 0 /\ ret_xlogarchivingactive44^0-ret_xlogarchivingactive44^post1 == 0), cost: 1 1: l0 -> l2 : ___rho_1_^0'=___rho_1_^post2, ___rho_2_^0'=___rho_2_^post2, ___rho_4_^0'=___rho_4_^post2, a33^0'=a33^post2, a55^0'=a55^post2, a88^0'=a88^post2, curtime^0'=curtime^post2, got_sighup^0'=got_sighup^post2, last_copy_time^0'=last_copy_time^post2, ret_time1010^0'=ret_time1010^post2, ret_time77^0'=ret_time77^post2, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post2, tmp2^0'=tmp2^post2, tmp66^0'=tmp66^post2, tmp99^0'=tmp99^post2, tt1^0'=tt1^post2, wakend^0'=wakend^post2, (0 == 0 /\ got_sighup^post2 == 0 /\ -ret_time77^post2+ret_time77^0 == 0 /\ -last_copy_time^post2+last_copy_time^0 == 0 /\ ___rho_4_^0-___rho_4_^post2 == 0 /\ ret_time1010^0-ret_time1010^post2 == 0 /\ -tmp66^post2+tmp66^0 == 0 /\ 1-got_sighup^0 <= 0 /\ -curtime^post2+curtime^0 == 0 /\ -1+a33^post2 == 0 /\ -a55^post2+a55^0 == 0 /\ -___rho_2_^post2+ret_xlogarchivingactive44^post2 == 0 /\ -___rho_1_^post2+___rho_1_^0 == 0 /\ -ret_xlogarchivingactive44^post2+tmp2^post2 == 0 /\ -wakend^post2+wakend^0 == 0 /\ tmp99^0-tmp99^post2 == 0 /\ a88^0-a88^post2 == 0 /\ tt1^post2-tmp2^post2 == 0), cost: 1 9: l1 -> l9 : ___rho_1_^0'=___rho_1_^post10, ___rho_2_^0'=___rho_2_^post10, ___rho_4_^0'=___rho_4_^post10, a33^0'=a33^post10, a55^0'=a55^post10, a88^0'=a88^post10, curtime^0'=curtime^post10, got_sighup^0'=got_sighup^post10, last_copy_time^0'=last_copy_time^post10, ret_time1010^0'=ret_time1010^post10, ret_time77^0'=ret_time77^post10, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post10, tmp2^0'=tmp2^post10, tmp66^0'=tmp66^post10, tmp99^0'=tmp99^post10, tt1^0'=tt1^post10, wakend^0'=wakend^post10, (ret_xlogarchivingactive44^0-ret_xlogarchivingactive44^post10 == 0 /\ -wakend^post10+wakend^0 == 0 /\ -last_copy_time^post10+last_copy_time^0 == 0 /\ -tt1^post10+tt1^0 == 0 /\ tmp2^0-tmp2^post10 == 0 /\ -tmp99^post10+tmp99^0 == 0 /\ -ret_time1010^post10+ret_time1010^0 == 0 /\ -got_sighup^post10+got_sighup^0 == 0 /\ a88^0-a88^post10 == 0 /\ wakend^0 <= 0 /\ -a33^post10+a33^0 == 0 /\ -a55^post10+a55^0 == 0 /\ -___rho_2_^post10+___rho_2_^0 == 0 /\ curtime^0-curtime^post10 == 0 /\ -___rho_1_^post10+___rho_1_^0 == 0 /\ -ret_time77^post10+ret_time77^0 == 0 /\ ___rho_4_^0-___rho_4_^post10 == 0 /\ -tmp66^post10+tmp66^0 == 0), cost: 1 10: l1 -> l9 : ___rho_1_^0'=___rho_1_^post11, ___rho_2_^0'=___rho_2_^post11, ___rho_4_^0'=___rho_4_^post11, a33^0'=a33^post11, a55^0'=a55^post11, a88^0'=a88^post11, curtime^0'=curtime^post11, got_sighup^0'=got_sighup^post11, last_copy_time^0'=last_copy_time^post11, ret_time1010^0'=ret_time1010^post11, ret_time77^0'=ret_time77^post11, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post11, tmp2^0'=tmp2^post11, tmp66^0'=tmp66^post11, tmp99^0'=tmp99^post11, tt1^0'=tt1^post11, wakend^0'=wakend^post11, (0 == 0 /\ -a88^post11+a88^0 == 0 /\ 1-wakend^0 <= 0 /\ -___rho_4_^post11+___rho_4_^0 == 0 /\ -a33^post11+a33^0 == 0 /\ -___rho_1_^post11+___rho_1_^0 == 0 /\ tmp99^0-tmp99^post11 == 0 /\ wakend^post11 == 0 /\ ___rho_2_^0-___rho_2_^post11 == 0 /\ -tt1^post11+tt1^0 == 0 /\ a55^post11 == 0 /\ ret_xlogarchivingactive44^0-ret_xlogarchivingactive44^post11 == 0 /\ -tmp66^post11+ret_time77^post11 == 0 /\ -ret_time1010^post11+ret_time1010^0 == 0 /\ -tmp2^post11+tmp2^0 == 0 /\ -curtime^post11+curtime^0 == 0 /\ -got_sighup^post11+got_sighup^0 == 0 /\ -ret_time77^post11+last_copy_time^post11 == 0), cost: 1 13: l2 -> l1 : ___rho_1_^0'=___rho_1_^post14, ___rho_2_^0'=___rho_2_^post14, ___rho_4_^0'=___rho_4_^post14, a33^0'=a33^post14, a55^0'=a55^post14, a88^0'=a88^post14, curtime^0'=curtime^post14, got_sighup^0'=got_sighup^post14, last_copy_time^0'=last_copy_time^post14, ret_time1010^0'=ret_time1010^post14, ret_time77^0'=ret_time77^post14, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post14, tmp2^0'=tmp2^post14, tmp66^0'=tmp66^post14, tmp99^0'=tmp99^post14, tt1^0'=tt1^post14, wakend^0'=wakend^post14, (-ret_xlogarchivingactive44^post14+ret_xlogarchivingactive44^0 == 0 /\ -tmp99^post14+tmp99^0 == 0 /\ got_sighup^0-got_sighup^post14 == 0 /\ -curtime^post14+curtime^0 == 0 /\ -___rho_2_^post14+___rho_2_^0 == 0 /\ -last_copy_time^post14+last_copy_time^0 == 0 /\ tmp2^0-tmp2^post14 == 0 /\ -a33^post14+a33^0 == 0 /\ ___rho_4_^0-___rho_4_^post14 == 0 /\ ret_time77^0-ret_time77^post14 == 0 /\ a88^0-a88^post14 == 0 /\ -___rho_1_^post14+___rho_1_^0 == 0 /\ -a55^post14+a55^0 == 0 /\ -tt1^post14+tt1^0 == 0 /\ 1-tt1^0 <= 0 /\ wakend^0-wakend^post14 == 0 /\ tmp66^0-tmp66^post14 == 0 /\ -ret_time1010^post14+ret_time1010^0 == 0), cost: 1 14: l2 -> l5 : ___rho_1_^0'=___rho_1_^post15, ___rho_2_^0'=___rho_2_^post15, ___rho_4_^0'=___rho_4_^post15, a33^0'=a33^post15, a55^0'=a55^post15, a88^0'=a88^post15, curtime^0'=curtime^post15, got_sighup^0'=got_sighup^post15, last_copy_time^0'=last_copy_time^post15, ret_time1010^0'=ret_time1010^post15, ret_time77^0'=ret_time77^post15, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post15, tmp2^0'=tmp2^post15, tmp66^0'=tmp66^post15, tmp99^0'=tmp99^post15, tt1^0'=tt1^post15, wakend^0'=wakend^post15, (ret_xlogarchivingactive44^0-ret_xlogarchivingactive44^post15 == 0 /\ -last_copy_time^post15+last_copy_time^0 == 0 /\ ___rho_4_^0-___rho_4_^post15 == 0 /\ -a55^post15+a55^0 == 0 /\ -___rho_1_^post15+___rho_1_^0 == 0 /\ -got_sighup^post15+got_sighup^0 == 0 /\ a88^0-a88^post15 == 0 /\ -tt1^post15+tt1^0 == 0 /\ -ret_time1010^post15+ret_time1010^0 == 0 /\ -tmp99^post15+tmp99^0 == 0 /\ curtime^0-curtime^post15 == 0 /\ wakend^0-wakend^post15 == 0 /\ -tmp66^post15+tmp66^0 == 0 /\ -a33^post15+a33^0 == 0 /\ -___rho_2_^post15+___rho_2_^0 == 0 /\ tmp2^0-tmp2^post15 == 0 /\ tt1^0 <= 0 /\ -ret_time77^post15+ret_time77^0 == 0), cost: 1 2: l3 -> l4 : ___rho_1_^0'=___rho_1_^post3, ___rho_2_^0'=___rho_2_^post3, ___rho_4_^0'=___rho_4_^post3, a33^0'=a33^post3, a55^0'=a55^post3, a88^0'=a88^post3, curtime^0'=curtime^post3, got_sighup^0'=got_sighup^post3, last_copy_time^0'=last_copy_time^post3, ret_time1010^0'=ret_time1010^post3, ret_time77^0'=ret_time77^post3, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post3, tmp2^0'=tmp2^post3, tmp66^0'=tmp66^post3, tmp99^0'=tmp99^post3, tt1^0'=tt1^post3, wakend^0'=wakend^post3, (-___rho_1_^post3+___rho_1_^0 == 0 /\ -got_sighup^post3+got_sighup^0 == 0 /\ tmp99^0-tmp99^post3 == 0 /\ tmp2^0-tmp2^post3 == 0 /\ -last_copy_time^post3+last_copy_time^0 == 0 /\ -___rho_4_^post3+___rho_4_^0 == 0 /\ -tt1^post3+tt1^0 == 0 /\ ret_time77^0-ret_time77^post3 == 0 /\ ___rho_2_^0-___rho_2_^post3 == 0 /\ -curtime^post3+curtime^0 == 0 /\ -ret_time1010^post3+ret_time1010^0 == 0 /\ -tmp66^post3+tmp66^0 == 0 /\ -wakend^post3+wakend^0 == 0 /\ a88^0-a88^post3 == 0 /\ ret_xlogarchivingactive44^0-ret_xlogarchivingactive44^post3 == 0 /\ a55^0-a55^post3 == 0 /\ -a33^post3+a33^0 == 0), cost: 1 3: l5 -> l6 : ___rho_1_^0'=___rho_1_^post4, ___rho_2_^0'=___rho_2_^post4, ___rho_4_^0'=___rho_4_^post4, a33^0'=a33^post4, a55^0'=a55^post4, a88^0'=a88^post4, curtime^0'=curtime^post4, got_sighup^0'=got_sighup^post4, last_copy_time^0'=last_copy_time^post4, ret_time1010^0'=ret_time1010^post4, ret_time77^0'=ret_time77^post4, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post4, tmp2^0'=tmp2^post4, tmp66^0'=tmp66^post4, tmp99^0'=tmp99^post4, tt1^0'=tt1^post4, wakend^0'=wakend^post4, (wakend^0-wakend^post4 == 0 /\ -curtime^post4+curtime^0 == 0 /\ -ret_time1010^post4+ret_time1010^0 == 0 /\ -tmp66^post4+tmp66^0 == 0 /\ -a33^post4+a33^0 == 0 /\ ___rho_4_^0-___rho_4_^post4 == 0 /\ tmp2^0-tmp2^post4 == 0 /\ -___rho_2_^post4+___rho_2_^0 == 0 /\ got_sighup^0-got_sighup^post4 == 0 /\ -tt1^post4+tt1^0 == 0 /\ a88^0-a88^post4 == 0 /\ ret_time77^0-ret_time77^post4 == 0 /\ -ret_xlogarchivingactive44^post4+ret_xlogarchivingactive44^0 == 0 /\ -___rho_1_^post4+___rho_1_^0 == 0 /\ -a55^post4+a55^0 == 0 /\ -tmp99^post4+tmp99^0 == 0 /\ -last_copy_time^post4+last_copy_time^0 == 0), cost: 1 18: l6 -> l6 : ___rho_1_^0'=___rho_1_^post13, ___rho_2_^0'=___rho_2_^post13, ___rho_4_^0'=___rho_4_^post13, a33^0'=a33^post13, a55^0'=a55^post13, a88^0'=a88^post13, curtime^0'=curtime^post13, got_sighup^0'=got_sighup^post13, last_copy_time^0'=last_copy_time^post13, ret_time1010^0'=ret_time1010^post13, ret_time77^0'=ret_time77^post13, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post13, tmp2^0'=tmp2^post13, tmp66^0'=tmp66^post13, tmp99^0'=tmp99^post13, tt1^0'=tt1^post13, wakend^0'=wakend^post13, (-ret_time77^post13+ret_time77^post12 == 0 /\ tmp99^0-tmp99^post12 == 0 /\ -last_copy_time^post12+last_copy_time^0 == 0 /\ -tmp66^post12+tmp66^0 == 0 /\ tmp2^0-tmp2^post12 == 0 /\ wakend^0-wakend^post12 == 0 /\ curtime^post12-curtime^post13 == 0 /\ a55^0-a55^post12 == 0 /\ tmp66^post12-tmp66^post13 == 0 /\ -got_sighup^post13+got_sighup^post12 == 0 /\ -tt1^post13+tt1^post12 == 0 /\ got_sighup^0-got_sighup^post12 == 0 /\ -a55^post13+a55^post12 == 0 /\ ret_time77^0-ret_time77^post12 == 0 /\ -ret_time1010^post12+ret_time1010^0 == 0 /\ a88^0-a88^post12 == 0 /\ -curtime^post12+curtime^0 == 0 /\ ret_time1010^post12-ret_time1010^post13 == 0 /\ tmp2^post12-tmp2^post13 == 0 /\ a33^post12-a33^post13 == 0 /\ -tmp99^post13+tmp99^post12 == 0 /\ -wakend^post13+wakend^post12 == 0 /\ -ret_xlogarchivingactive44^post12+ret_xlogarchivingactive44^0 == 0 /\ -___rho_1_^post12+___rho_1_^0 == 0 /\ ___rho_4_^post12-___rho_4_^post13 == 0 /\ -tt1^post12+tt1^0 == 0 /\ -a33^post12+a33^0 == 0 /\ ___rho_4_^0-___rho_4_^post12 == 0 /\ ret_xlogarchivingactive44^post12-ret_xlogarchivingactive44^post13 == 0 /\ -___rho_2_^post13+___rho_2_^post12 == 0 /\ ___rho_2_^0-___rho_2_^post12 == 0 /\ last_copy_time^post12-last_copy_time^post13 == 0 /\ ___rho_1_^post12-___rho_1_^post13 == 0 /\ a88^post12-a88^post13 == 0), cost: 1 4: l7 -> l5 : ___rho_1_^0'=___rho_1_^post5, ___rho_2_^0'=___rho_2_^post5, ___rho_4_^0'=___rho_4_^post5, a33^0'=a33^post5, a55^0'=a55^post5, a88^0'=a88^post5, curtime^0'=curtime^post5, got_sighup^0'=got_sighup^post5, last_copy_time^0'=last_copy_time^post5, ret_time1010^0'=ret_time1010^post5, ret_time77^0'=ret_time77^post5, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post5, tmp2^0'=tmp2^post5, tmp66^0'=tmp66^post5, tmp99^0'=tmp99^post5, tt1^0'=tt1^post5, wakend^0'=wakend^post5, (0 == 0 /\ -tt1^post5+tt1^0 == 0 /\ -___rho_2_^post5+___rho_2_^0 == 0 /\ -___rho_1_^post5+___rho_1_^0 == 0 /\ tmp2^0-tmp2^post5 == 0 /\ -wakend^post5+wakend^0 == 0 /\ -last_copy_time^post5+last_copy_time^0 == 0 /\ -tmp99^post5+tmp99^0 == 0 /\ -a55^post5+a55^0 == 0 /\ curtime^0-curtime^post5 == 0 /\ a33^0-a33^post5 == 0 /\ -got_sighup^post5+got_sighup^0 == 0 /\ -ret_time1010^post5+ret_time1010^0 == 0 /\ -ret_time77^post5+ret_time77^0 == 0 /\ -tmp66^post5+tmp66^0 == 0 /\ a88^0-a88^post5 == 0 /\ ret_xlogarchivingactive44^0-ret_xlogarchivingactive44^post5 == 0), cost: 1 5: l8 -> l7 : ___rho_1_^0'=___rho_1_^post6, ___rho_2_^0'=___rho_2_^post6, ___rho_4_^0'=___rho_4_^post6, a33^0'=a33^post6, a55^0'=a55^post6, a88^0'=a88^post6, curtime^0'=curtime^post6, got_sighup^0'=got_sighup^post6, last_copy_time^0'=last_copy_time^post6, ret_time1010^0'=ret_time1010^post6, ret_time77^0'=ret_time77^post6, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post6, tmp2^0'=tmp2^post6, tmp66^0'=tmp66^post6, tmp99^0'=tmp99^post6, tt1^0'=tt1^post6, wakend^0'=wakend^post6, (tmp2^0-tmp2^post6 == 0 /\ -tmp66^post6+tmp66^0 == 0 /\ -last_copy_time^post6+last_copy_time^0 == 0 /\ tmp99^0-tmp99^post6 == 0 /\ ___rho_2_^0-___rho_2_^post6 == 0 /\ -curtime^post6+curtime^0 == 0 /\ ret_time77^0-ret_time77^post6 == 0 /\ a88^0-a88^post6 == 0 /\ got_sighup^0-got_sighup^post6 == 0 /\ -999-last_copy_time^0+curtime^0 <= 0 /\ ___rho_4_^0-___rho_4_^post6 == 0 /\ wakend^0-wakend^post6 == 0 /\ -a33^post6+a33^0 == 0 /\ -ret_time1010^post6+ret_time1010^0 == 0 /\ a55^0-a55^post6 == 0 /\ -ret_xlogarchivingactive44^post6+ret_xlogarchivingactive44^0 == 0 /\ -tt1^post6+tt1^0 == 0 /\ -___rho_1_^post6+___rho_1_^0 == 0), cost: 1 6: l8 -> l7 : ___rho_1_^0'=___rho_1_^post7, ___rho_2_^0'=___rho_2_^post7, ___rho_4_^0'=___rho_4_^post7, a33^0'=a33^post7, a55^0'=a55^post7, a88^0'=a88^post7, curtime^0'=curtime^post7, got_sighup^0'=got_sighup^post7, last_copy_time^0'=last_copy_time^post7, ret_time1010^0'=ret_time1010^post7, ret_time77^0'=ret_time77^post7, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post7, tmp2^0'=tmp2^post7, tmp66^0'=tmp66^post7, tmp99^0'=tmp99^post7, tt1^0'=tt1^post7, wakend^0'=wakend^post7, (a88^0-a88^post7 == 0 /\ -a55^post7+a55^0 == 0 /\ -___rho_1_^post7+___rho_1_^0 == 0 /\ -tt1^post7+tt1^0 == 0 /\ -ret_time77^post7+ret_time77^0 == 0 /\ -tmp66^post7+tmp66^0 == 0 /\ 1000+last_copy_time^0-curtime^0 <= 0 /\ -tmp99^post7+tmp99^0 == 0 /\ ___rho_4_^0-___rho_4_^post7 == 0 /\ -last_copy_time^post7+last_copy_time^0 == 0 /\ -a33^post7+a33^0 == 0 /\ -___rho_2_^post7+___rho_2_^0 == 0 /\ -got_sighup^post7+got_sighup^0 == 0 /\ tmp2^0-tmp2^post7 == 0 /\ ret_xlogarchivingactive44^0-ret_xlogarchivingactive44^post7 == 0 /\ -ret_time1010^post7+ret_time1010^0 == 0 /\ -1+wakend^post7 == 0 /\ curtime^0-curtime^post7 == 0), cost: 1 7: l9 -> l7 : ___rho_1_^0'=___rho_1_^post8, ___rho_2_^0'=___rho_2_^post8, ___rho_4_^0'=___rho_4_^post8, a33^0'=a33^post8, a55^0'=a55^post8, a88^0'=a88^post8, curtime^0'=curtime^post8, got_sighup^0'=got_sighup^post8, last_copy_time^0'=last_copy_time^post8, ret_time1010^0'=ret_time1010^post8, ret_time77^0'=ret_time77^post8, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post8, tmp2^0'=tmp2^post8, tmp66^0'=tmp66^post8, tmp99^0'=tmp99^post8, tt1^0'=tt1^post8, wakend^0'=wakend^post8, (1-wakend^0 <= 0 /\ tmp2^0-tmp2^post8 == 0 /\ ret_xlogarchivingactive44^0-ret_xlogarchivingactive44^post8 == 0 /\ -tmp66^post8+tmp66^0 == 0 /\ -last_copy_time^post8+last_copy_time^0 == 0 /\ tmp99^0-tmp99^post8 == 0 /\ -got_sighup^post8+got_sighup^0 == 0 /\ a88^0-a88^post8 == 0 /\ -a55^post8+a55^0 == 0 /\ -wakend^post8+wakend^0 == 0 /\ -___rho_2_^post8+___rho_2_^0 == 0 /\ -ret_time1010^post8+ret_time1010^0 == 0 /\ ___rho_4_^0-___rho_4_^post8 == 0 /\ -curtime^post8+curtime^0 == 0 /\ -a33^post8+a33^0 == 0 /\ -___rho_1_^post8+___rho_1_^0 == 0 /\ -tt1^post8+tt1^0 == 0 /\ -ret_time77^post8+ret_time77^0 == 0), cost: 1 8: l9 -> l8 : ___rho_1_^0'=___rho_1_^post9, ___rho_2_^0'=___rho_2_^post9, ___rho_4_^0'=___rho_4_^post9, a33^0'=a33^post9, a55^0'=a55^post9, a88^0'=a88^post9, curtime^0'=curtime^post9, got_sighup^0'=got_sighup^post9, last_copy_time^0'=last_copy_time^post9, ret_time1010^0'=ret_time1010^post9, ret_time77^0'=ret_time77^post9, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post9, tmp2^0'=tmp2^post9, tmp66^0'=tmp66^post9, tmp99^0'=tmp99^post9, tt1^0'=tt1^post9, wakend^0'=wakend^post9, (0 == 0 /\ ret_time77^0-ret_time77^post9 == 0 /\ a88^post9 == 0 /\ a55^0-a55^post9 == 0 /\ -a33^post9+a33^0 == 0 /\ -___rho_1_^post9+___rho_1_^0 == 0 /\ -tt1^post9+tt1^0 == 0 /\ ___rho_2_^0-___rho_2_^post9 == 0 /\ last_copy_time^0-last_copy_time^post9 == 0 /\ wakend^0 <= 0 /\ got_sighup^0-got_sighup^post9 == 0 /\ -tmp66^post9+tmp66^0 == 0 /\ -ret_time1010^post9+curtime^post9 == 0 /\ -___rho_4_^post9+___rho_4_^0 == 0 /\ ret_xlogarchivingactive44^0-ret_xlogarchivingactive44^post9 == 0 /\ tmp2^0-tmp2^post9 == 0 /\ -wakend^post9+wakend^0 == 0 /\ ret_time1010^post9-tmp99^post9 == 0), cost: 1 17: l12 -> l0 : ___rho_1_^0'=___rho_1_^post16, ___rho_2_^0'=___rho_2_^post16, ___rho_4_^0'=___rho_4_^post16, a33^0'=a33^post16, a55^0'=a55^post16, a88^0'=a88^post16, curtime^0'=curtime^post16, got_sighup^0'=got_sighup^post16, last_copy_time^0'=last_copy_time^post16, ret_time1010^0'=ret_time1010^post16, ret_time77^0'=ret_time77^post16, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post16, tmp2^0'=tmp2^post16, tmp66^0'=tmp66^post16, tmp99^0'=tmp99^post16, tt1^0'=tt1^post16, wakend^0'=wakend^post16, (0 == 0 /\ a55^post17-a55^post16 == 0 /\ -___rho_1_^post17+___rho_1_^0 == 0 /\ -___rho_2_^post17+___rho_2_^0 == 0 /\ -a55^post17+a55^0 == 0 /\ -got_sighup^post17+got_sighup^0 == 0 /\ -ret_xlogarchivingactive44^post16+ret_xlogarchivingactive44^post17 == 0 /\ tmp66^post17-tmp66^post16 == 0 /\ a88^0-a88^post17 == 0 /\ -tmp99^post16+tmp99^post17 == 0 /\ -tmp2^post17+tmp2^0 == 0 /\ -1+wakend^post16 == 0 /\ -curtime^post16+curtime^post17 == 0 /\ ret_xlogarchivingactive44^0-ret_xlogarchivingactive44^post17 == 0 /\ ret_time77^post17-ret_time77^post16 == 0 /\ -tt1^post17+tt1^0 == 0 /\ -ret_time77^post17+ret_time77^0 == 0 /\ -ret_time1010^post17+ret_time1010^0 == 0 /\ ___rho_4_^0-___rho_4_^post17 == 0 /\ -1+wakend^1 == 0 /\ -tt1^post16+tt1^post17 == 0 /\ -a88^post16+a88^post17 == 0 /\ tmp2^post17-tmp2^post16 == 0 /\ -___rho_2_^post17+got_sighup^post16 == 0 /\ ___rho_2_^post17-___rho_2_^post16 == 0 /\ -tmp66^post17+tmp66^0 == 0 /\ -last_copy_time^post16+last_copy_time^post17 == 0 /\ -wakend^post17+wakend^0 == 0 /\ -___rho_4_^post16+___rho_4_^post17 == 0 /\ tmp99^0-tmp99^post17 == 0 /\ -last_copy_time^post17+last_copy_time^0 == 0 /\ ret_time1010^post17-ret_time1010^post16 == 0 /\ curtime^0-curtime^post17 == 0 /\ a33^0-a33^post17 == 0 /\ -a33^post16+a33^post17 == 0), cost: 1 Eliminating location l11 by chaining: Applied chaining First rule: l12 -> l11 : ___rho_1_^0'=___rho_1_^post17, ___rho_2_^0'=___rho_2_^post17, ___rho_4_^0'=___rho_4_^post17, a33^0'=a33^post17, a55^0'=a55^post17, a88^0'=a88^post17, curtime^0'=curtime^post17, got_sighup^0'=got_sighup^post17, last_copy_time^0'=last_copy_time^post17, ret_time1010^0'=ret_time1010^post17, ret_time77^0'=ret_time77^post17, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post17, tmp2^0'=tmp2^post17, tmp66^0'=tmp66^post17, tmp99^0'=tmp99^post17, tt1^0'=tt1^post17, wakend^0'=wakend^post17, (-___rho_1_^post17+___rho_1_^0 == 0 /\ -___rho_2_^post17+___rho_2_^0 == 0 /\ -a55^post17+a55^0 == 0 /\ -got_sighup^post17+got_sighup^0 == 0 /\ a88^0-a88^post17 == 0 /\ -tmp2^post17+tmp2^0 == 0 /\ ret_xlogarchivingactive44^0-ret_xlogarchivingactive44^post17 == 0 /\ -tt1^post17+tt1^0 == 0 /\ -ret_time77^post17+ret_time77^0 == 0 /\ -ret_time1010^post17+ret_time1010^0 == 0 /\ ___rho_4_^0-___rho_4_^post17 == 0 /\ -tmp66^post17+tmp66^0 == 0 /\ -wakend^post17+wakend^0 == 0 /\ tmp99^0-tmp99^post17 == 0 /\ -last_copy_time^post17+last_copy_time^0 == 0 /\ curtime^0-curtime^post17 == 0 /\ a33^0-a33^post17 == 0), cost: 1 Second rule: l11 -> l0 : ___rho_1_^0'=___rho_1_^post16, ___rho_2_^0'=___rho_2_^post16, ___rho_4_^0'=___rho_4_^post16, a33^0'=a33^post16, a55^0'=a55^post16, a88^0'=a88^post16, curtime^0'=curtime^post16, got_sighup^0'=got_sighup^post16, last_copy_time^0'=last_copy_time^post16, ret_time1010^0'=ret_time1010^post16, ret_time77^0'=ret_time77^post16, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post16, tmp2^0'=tmp2^post16, tmp66^0'=tmp66^post16, tmp99^0'=tmp99^post16, tt1^0'=tt1^post16, wakend^0'=wakend^post16, (0 == 0 /\ a55^0-a55^post16 == 0 /\ -last_copy_time^post16+last_copy_time^0 == 0 /\ -1+wakend^post16 == 0 /\ -ret_time1010^post16+ret_time1010^0 == 0 /\ -tmp66^post16+tmp66^0 == 0 /\ a88^0-a88^post16 == 0 /\ -curtime^post16+curtime^0 == 0 /\ tmp2^0-tmp2^post16 == 0 /\ -___rho_4_^post16+___rho_4_^0 == 0 /\ -a33^post16+a33^0 == 0 /\ -tt1^post16+tt1^0 == 0 /\ -1+wakend^1 == 0 /\ ret_time77^0-ret_time77^post16 == 0 /\ -___rho_2_^0+got_sighup^post16 == 0 /\ ___rho_2_^0-___rho_2_^post16 == 0 /\ -tmp99^post16+tmp99^0 == 0 /\ -ret_xlogarchivingactive44^post16+ret_xlogarchivingactive44^0 == 0), cost: 1 New rule: l12 -> l0 : ___rho_1_^0'=___rho_1_^post16, ___rho_2_^0'=___rho_2_^post16, ___rho_4_^0'=___rho_4_^post16, a33^0'=a33^post16, a55^0'=a55^post16, a88^0'=a88^post16, curtime^0'=curtime^post16, got_sighup^0'=got_sighup^post16, last_copy_time^0'=last_copy_time^post16, ret_time1010^0'=ret_time1010^post16, ret_time77^0'=ret_time77^post16, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post16, tmp2^0'=tmp2^post16, tmp66^0'=tmp66^post16, tmp99^0'=tmp99^post16, tt1^0'=tt1^post16, wakend^0'=wakend^post16, (0 == 0 /\ a55^post17-a55^post16 == 0 /\ -___rho_1_^post17+___rho_1_^0 == 0 /\ -___rho_2_^post17+___rho_2_^0 == 0 /\ -a55^post17+a55^0 == 0 /\ -got_sighup^post17+got_sighup^0 == 0 /\ -ret_xlogarchivingactive44^post16+ret_xlogarchivingactive44^post17 == 0 /\ tmp66^post17-tmp66^post16 == 0 /\ a88^0-a88^post17 == 0 /\ -tmp99^post16+tmp99^post17 == 0 /\ -tmp2^post17+tmp2^0 == 0 /\ -1+wakend^post16 == 0 /\ -curtime^post16+curtime^post17 == 0 /\ ret_xlogarchivingactive44^0-ret_xlogarchivingactive44^post17 == 0 /\ ret_time77^post17-ret_time77^post16 == 0 /\ -tt1^post17+tt1^0 == 0 /\ -ret_time77^post17+ret_time77^0 == 0 /\ -ret_time1010^post17+ret_time1010^0 == 0 /\ ___rho_4_^0-___rho_4_^post17 == 0 /\ -1+wakend^1 == 0 /\ -tt1^post16+tt1^post17 == 0 /\ -a88^post16+a88^post17 == 0 /\ tmp2^post17-tmp2^post16 == 0 /\ -___rho_2_^post17+got_sighup^post16 == 0 /\ ___rho_2_^post17-___rho_2_^post16 == 0 /\ -tmp66^post17+tmp66^0 == 0 /\ -last_copy_time^post16+last_copy_time^post17 == 0 /\ -wakend^post17+wakend^0 == 0 /\ -___rho_4_^post16+___rho_4_^post17 == 0 /\ tmp99^0-tmp99^post17 == 0 /\ -last_copy_time^post17+last_copy_time^0 == 0 /\ ret_time1010^post17-ret_time1010^post16 == 0 /\ curtime^0-curtime^post17 == 0 /\ a33^0-a33^post17 == 0 /\ -a33^post16+a33^post17 == 0), cost: 1 Applied deletion Removed the following rules: 15 16 Eliminating location l10 by chaining: Applied chaining First rule: l6 -> l10 : ___rho_1_^0'=___rho_1_^post12, ___rho_2_^0'=___rho_2_^post12, ___rho_4_^0'=___rho_4_^post12, a33^0'=a33^post12, a55^0'=a55^post12, a88^0'=a88^post12, curtime^0'=curtime^post12, got_sighup^0'=got_sighup^post12, last_copy_time^0'=last_copy_time^post12, ret_time1010^0'=ret_time1010^post12, ret_time77^0'=ret_time77^post12, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post12, tmp2^0'=tmp2^post12, tmp66^0'=tmp66^post12, tmp99^0'=tmp99^post12, tt1^0'=tt1^post12, wakend^0'=wakend^post12, (tmp99^0-tmp99^post12 == 0 /\ -last_copy_time^post12+last_copy_time^0 == 0 /\ -tmp66^post12+tmp66^0 == 0 /\ tmp2^0-tmp2^post12 == 0 /\ wakend^0-wakend^post12 == 0 /\ a55^0-a55^post12 == 0 /\ got_sighup^0-got_sighup^post12 == 0 /\ ret_time77^0-ret_time77^post12 == 0 /\ -ret_time1010^post12+ret_time1010^0 == 0 /\ a88^0-a88^post12 == 0 /\ -curtime^post12+curtime^0 == 0 /\ -ret_xlogarchivingactive44^post12+ret_xlogarchivingactive44^0 == 0 /\ -___rho_1_^post12+___rho_1_^0 == 0 /\ -tt1^post12+tt1^0 == 0 /\ -a33^post12+a33^0 == 0 /\ ___rho_4_^0-___rho_4_^post12 == 0 /\ ___rho_2_^0-___rho_2_^post12 == 0), cost: 1 Second rule: l10 -> l6 : ___rho_1_^0'=___rho_1_^post13, ___rho_2_^0'=___rho_2_^post13, ___rho_4_^0'=___rho_4_^post13, a33^0'=a33^post13, a55^0'=a55^post13, a88^0'=a88^post13, curtime^0'=curtime^post13, got_sighup^0'=got_sighup^post13, last_copy_time^0'=last_copy_time^post13, ret_time1010^0'=ret_time1010^post13, ret_time77^0'=ret_time77^post13, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post13, tmp2^0'=tmp2^post13, tmp66^0'=tmp66^post13, tmp99^0'=tmp99^post13, tt1^0'=tt1^post13, wakend^0'=wakend^post13, (-a55^post13+a55^0 == 0 /\ a88^0-a88^post13 == 0 /\ -___rho_1_^post13+___rho_1_^0 == 0 /\ -___rho_2_^post13+___rho_2_^0 == 0 /\ -ret_time77^post13+ret_time77^0 == 0 /\ -tt1^post13+tt1^0 == 0 /\ tmp99^0-tmp99^post13 == 0 /\ ___rho_4_^0-___rho_4_^post13 == 0 /\ -last_copy_time^post13+last_copy_time^0 == 0 /\ ret_xlogarchivingactive44^0-ret_xlogarchivingactive44^post13 == 0 /\ -ret_time1010^post13+ret_time1010^0 == 0 /\ -wakend^post13+wakend^0 == 0 /\ tmp66^0-tmp66^post13 == 0 /\ tmp2^0-tmp2^post13 == 0 /\ -got_sighup^post13+got_sighup^0 == 0 /\ curtime^0-curtime^post13 == 0 /\ a33^0-a33^post13 == 0), cost: 1 New rule: l6 -> l6 : ___rho_1_^0'=___rho_1_^post13, ___rho_2_^0'=___rho_2_^post13, ___rho_4_^0'=___rho_4_^post13, a33^0'=a33^post13, a55^0'=a55^post13, a88^0'=a88^post13, curtime^0'=curtime^post13, got_sighup^0'=got_sighup^post13, last_copy_time^0'=last_copy_time^post13, ret_time1010^0'=ret_time1010^post13, ret_time77^0'=ret_time77^post13, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post13, tmp2^0'=tmp2^post13, tmp66^0'=tmp66^post13, tmp99^0'=tmp99^post13, tt1^0'=tt1^post13, wakend^0'=wakend^post13, (-ret_time77^post13+ret_time77^post12 == 0 /\ tmp99^0-tmp99^post12 == 0 /\ -last_copy_time^post12+last_copy_time^0 == 0 /\ -tmp66^post12+tmp66^0 == 0 /\ tmp2^0-tmp2^post12 == 0 /\ wakend^0-wakend^post12 == 0 /\ curtime^post12-curtime^post13 == 0 /\ a55^0-a55^post12 == 0 /\ tmp66^post12-tmp66^post13 == 0 /\ -got_sighup^post13+got_sighup^post12 == 0 /\ -tt1^post13+tt1^post12 == 0 /\ got_sighup^0-got_sighup^post12 == 0 /\ -a55^post13+a55^post12 == 0 /\ ret_time77^0-ret_time77^post12 == 0 /\ -ret_time1010^post12+ret_time1010^0 == 0 /\ a88^0-a88^post12 == 0 /\ -curtime^post12+curtime^0 == 0 /\ ret_time1010^post12-ret_time1010^post13 == 0 /\ tmp2^post12-tmp2^post13 == 0 /\ a33^post12-a33^post13 == 0 /\ -tmp99^post13+tmp99^post12 == 0 /\ -wakend^post13+wakend^post12 == 0 /\ -ret_xlogarchivingactive44^post12+ret_xlogarchivingactive44^0 == 0 /\ -___rho_1_^post12+___rho_1_^0 == 0 /\ ___rho_4_^post12-___rho_4_^post13 == 0 /\ -tt1^post12+tt1^0 == 0 /\ -a33^post12+a33^0 == 0 /\ ___rho_4_^0-___rho_4_^post12 == 0 /\ ret_xlogarchivingactive44^post12-ret_xlogarchivingactive44^post13 == 0 /\ -___rho_2_^post13+___rho_2_^post12 == 0 /\ ___rho_2_^0-___rho_2_^post12 == 0 /\ last_copy_time^post12-last_copy_time^post13 == 0 /\ ___rho_1_^post12-___rho_1_^post13 == 0 /\ a88^post12-a88^post13 == 0), cost: 1 Applied deletion Removed the following rules: 11 12 Simplified Transitions Start location: l12 Program variables: ___rho_1_^0 ___rho_2_^0 ___rho_4_^0 a33^0 a55^0 a88^0 curtime^0 got_sighup^0 last_copy_time^0 ret_time1010^0 ret_time77^0 ret_xlogarchivingactive44^0 tmp2^0 tmp66^0 tmp99^0 tt1^0 wakend^0 19: l0 -> l1 : got_sighup^0 <= 0, cost: 1 20: l0 -> l2 : ___rho_2_^0'=tt1^post2, a33^0'=1, got_sighup^0'=0, ret_xlogarchivingactive44^0'=tt1^post2, tmp2^0'=tt1^post2, tt1^0'=tt1^post2, 1-got_sighup^0 <= 0, cost: 1 28: l1 -> l9 : wakend^0 <= 0, cost: 1 29: l1 -> l9 : a55^0'=0, last_copy_time^0'=tmp66^post11, ret_time77^0'=tmp66^post11, tmp66^0'=tmp66^post11, 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_4_^0'=___rho_4_^post5, T, cost: 1 24: l8 -> l7 : -999-last_copy_time^0+curtime^0 <= 0, cost: 1 25: l8 -> l7 : wakend^0'=1, 1000+last_copy_time^0-curtime^0 <= 0, cost: 1 26: l9 -> l7 : 1-wakend^0 <= 0, cost: 1 27: l9 -> l8 : a88^0'=0, curtime^0'=tmp99^post9, ret_time1010^0'=tmp99^post9, tmp99^0'=tmp99^post9, wakend^0 <= 0, cost: 1 32: l12 -> l0 : ___rho_1_^0'=___rho_1_^post16, got_sighup^0'=___rho_2_^0, wakend^0'=1, T, cost: 1 Propagated Equalities Original rule: l0 -> l1 : ___rho_1_^0'=___rho_1_^post1, ___rho_2_^0'=___rho_2_^post1, ___rho_4_^0'=___rho_4_^post1, a33^0'=a33^post1, a55^0'=a55^post1, a88^0'=a88^post1, curtime^0'=curtime^post1, got_sighup^0'=got_sighup^post1, last_copy_time^0'=last_copy_time^post1, ret_time1010^0'=ret_time1010^post1, ret_time77^0'=ret_time77^post1, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post1, tmp2^0'=tmp2^post1, tmp66^0'=tmp66^post1, tmp99^0'=tmp99^post1, tt1^0'=tt1^post1, wakend^0'=wakend^post1, (tmp99^0-tmp99^post1 == 0 /\ -wakend^post1+wakend^0 == 0 /\ -a88^post1+a88^0 == 0 /\ -___rho_1_^post1+___rho_1_^0 == 0 /\ -___rho_4_^post1+___rho_4_^0 == 0 /\ -a33^post1+a33^0 == 0 /\ -tt1^post1+tt1^0 == 0 /\ tmp2^0-tmp2^post1 == 0 /\ ret_time77^0-ret_time77^post1 == 0 /\ last_copy_time^0-last_copy_time^post1 == 0 /\ ___rho_2_^0-___rho_2_^post1 == 0 /\ got_sighup^0 <= 0 /\ -ret_time1010^post1+ret_time1010^0 == 0 /\ a55^0-a55^post1 == 0 /\ -curtime^post1+curtime^0 == 0 /\ -got_sighup^post1+got_sighup^0 == 0 /\ -tmp66^post1+tmp66^0 == 0 /\ ret_xlogarchivingactive44^0-ret_xlogarchivingactive44^post1 == 0), cost: 1 New rule: l0 -> l1 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^0, a33^0'=a33^0, a55^0'=a55^0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=ret_time1010^0, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^0, tmp99^0'=tmp99^0, tt1^0'=tt1^0, wakend^0'=wakend^0, (0 == 0 /\ got_sighup^0 <= 0), cost: 1 propagated equality tmp99^post1 = tmp99^0 propagated equality wakend^post1 = wakend^0 propagated equality a88^post1 = a88^0 propagated equality ___rho_1_^post1 = ___rho_1_^0 propagated equality ___rho_4_^post1 = ___rho_4_^0 propagated equality a33^post1 = a33^0 propagated equality tt1^post1 = tt1^0 propagated equality tmp2^post1 = tmp2^0 propagated equality ret_time77^post1 = ret_time77^0 propagated equality last_copy_time^post1 = last_copy_time^0 propagated equality ___rho_2_^post1 = ___rho_2_^0 propagated equality ret_time1010^post1 = ret_time1010^0 propagated equality a55^post1 = a55^0 propagated equality curtime^post1 = curtime^0 propagated equality got_sighup^post1 = got_sighup^0 propagated equality tmp66^post1 = tmp66^0 propagated equality ret_xlogarchivingactive44^post1 = ret_xlogarchivingactive44^0 Simplified Guard Original rule: l0 -> l1 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^0, a33^0'=a33^0, a55^0'=a55^0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=ret_time1010^0, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^0, tmp99^0'=tmp99^0, tt1^0'=tt1^0, wakend^0'=wakend^0, (0 == 0 /\ got_sighup^0 <= 0), cost: 1 New rule: l0 -> l1 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^0, a33^0'=a33^0, a55^0'=a55^0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=ret_time1010^0, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^0, tmp99^0'=tmp99^0, tt1^0'=tt1^0, wakend^0'=wakend^0, got_sighup^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l0 -> l1 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^0, a33^0'=a33^0, a55^0'=a55^0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=ret_time1010^0, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^0, tmp99^0'=tmp99^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_1_^0'=___rho_1_^post2, ___rho_2_^0'=___rho_2_^post2, ___rho_4_^0'=___rho_4_^post2, a33^0'=a33^post2, a55^0'=a55^post2, a88^0'=a88^post2, curtime^0'=curtime^post2, got_sighup^0'=got_sighup^post2, last_copy_time^0'=last_copy_time^post2, ret_time1010^0'=ret_time1010^post2, ret_time77^0'=ret_time77^post2, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post2, tmp2^0'=tmp2^post2, tmp66^0'=tmp66^post2, tmp99^0'=tmp99^post2, tt1^0'=tt1^post2, wakend^0'=wakend^post2, (0 == 0 /\ got_sighup^post2 == 0 /\ -ret_time77^post2+ret_time77^0 == 0 /\ -last_copy_time^post2+last_copy_time^0 == 0 /\ ___rho_4_^0-___rho_4_^post2 == 0 /\ ret_time1010^0-ret_time1010^post2 == 0 /\ -tmp66^post2+tmp66^0 == 0 /\ 1-got_sighup^0 <= 0 /\ -curtime^post2+curtime^0 == 0 /\ -1+a33^post2 == 0 /\ -a55^post2+a55^0 == 0 /\ -___rho_2_^post2+ret_xlogarchivingactive44^post2 == 0 /\ -___rho_1_^post2+___rho_1_^0 == 0 /\ -ret_xlogarchivingactive44^post2+tmp2^post2 == 0 /\ -wakend^post2+wakend^0 == 0 /\ tmp99^0-tmp99^post2 == 0 /\ a88^0-a88^post2 == 0 /\ tt1^post2-tmp2^post2 == 0), cost: 1 New rule: l0 -> l2 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=tt1^post2, ___rho_4_^0'=___rho_4_^0, a33^0'=1, a55^0'=a55^0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=ret_time1010^0, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=tt1^post2, tmp2^0'=tt1^post2, tmp66^0'=tmp66^0, tmp99^0'=tmp99^0, tt1^0'=tt1^post2, wakend^0'=wakend^0, (0 == 0 /\ 1-got_sighup^0 <= 0), cost: 1 propagated equality got_sighup^post2 = 0 propagated equality ret_time77^post2 = ret_time77^0 propagated equality last_copy_time^post2 = last_copy_time^0 propagated equality ___rho_4_^post2 = ___rho_4_^0 propagated equality ret_time1010^post2 = ret_time1010^0 propagated equality tmp66^post2 = tmp66^0 propagated equality curtime^post2 = curtime^0 propagated equality a33^post2 = 1 propagated equality a55^post2 = a55^0 propagated equality ___rho_2_^post2 = ret_xlogarchivingactive44^post2 propagated equality ___rho_1_^post2 = ___rho_1_^0 propagated equality ret_xlogarchivingactive44^post2 = tmp2^post2 propagated equality wakend^post2 = wakend^0 propagated equality tmp99^post2 = tmp99^0 propagated equality a88^post2 = a88^0 propagated equality tmp2^post2 = tt1^post2 Simplified Guard Original rule: l0 -> l2 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=tt1^post2, ___rho_4_^0'=___rho_4_^0, a33^0'=1, a55^0'=a55^0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=ret_time1010^0, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=tt1^post2, tmp2^0'=tt1^post2, tmp66^0'=tmp66^0, tmp99^0'=tmp99^0, tt1^0'=tt1^post2, wakend^0'=wakend^0, (0 == 0 /\ 1-got_sighup^0 <= 0), cost: 1 New rule: l0 -> l2 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=tt1^post2, ___rho_4_^0'=___rho_4_^0, a33^0'=1, a55^0'=a55^0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=ret_time1010^0, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=tt1^post2, tmp2^0'=tt1^post2, tmp66^0'=tmp66^0, tmp99^0'=tmp99^0, tt1^0'=tt1^post2, wakend^0'=wakend^0, 1-got_sighup^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l0 -> l2 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=tt1^post2, ___rho_4_^0'=___rho_4_^0, a33^0'=1, a55^0'=a55^0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=ret_time1010^0, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=tt1^post2, tmp2^0'=tt1^post2, tmp66^0'=tmp66^0, tmp99^0'=tmp99^0, tt1^0'=tt1^post2, wakend^0'=wakend^0, 1-got_sighup^0 <= 0, cost: 1 New rule: l0 -> l2 : ___rho_2_^0'=tt1^post2, a33^0'=1, got_sighup^0'=0, ret_xlogarchivingactive44^0'=tt1^post2, tmp2^0'=tt1^post2, tt1^0'=tt1^post2, 1-got_sighup^0 <= 0, cost: 1 Propagated Equalities Original rule: l3 -> l4 : ___rho_1_^0'=___rho_1_^post3, ___rho_2_^0'=___rho_2_^post3, ___rho_4_^0'=___rho_4_^post3, a33^0'=a33^post3, a55^0'=a55^post3, a88^0'=a88^post3, curtime^0'=curtime^post3, got_sighup^0'=got_sighup^post3, last_copy_time^0'=last_copy_time^post3, ret_time1010^0'=ret_time1010^post3, ret_time77^0'=ret_time77^post3, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post3, tmp2^0'=tmp2^post3, tmp66^0'=tmp66^post3, tmp99^0'=tmp99^post3, tt1^0'=tt1^post3, wakend^0'=wakend^post3, (-___rho_1_^post3+___rho_1_^0 == 0 /\ -got_sighup^post3+got_sighup^0 == 0 /\ tmp99^0-tmp99^post3 == 0 /\ tmp2^0-tmp2^post3 == 0 /\ -last_copy_time^post3+last_copy_time^0 == 0 /\ -___rho_4_^post3+___rho_4_^0 == 0 /\ -tt1^post3+tt1^0 == 0 /\ ret_time77^0-ret_time77^post3 == 0 /\ ___rho_2_^0-___rho_2_^post3 == 0 /\ -curtime^post3+curtime^0 == 0 /\ -ret_time1010^post3+ret_time1010^0 == 0 /\ -tmp66^post3+tmp66^0 == 0 /\ -wakend^post3+wakend^0 == 0 /\ a88^0-a88^post3 == 0 /\ ret_xlogarchivingactive44^0-ret_xlogarchivingactive44^post3 == 0 /\ a55^0-a55^post3 == 0 /\ -a33^post3+a33^0 == 0), cost: 1 New rule: l3 -> l4 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^0, a33^0'=a33^0, a55^0'=a55^0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=ret_time1010^0, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^0, tmp99^0'=tmp99^0, tt1^0'=tt1^0, wakend^0'=wakend^0, 0 == 0, cost: 1 propagated equality ___rho_1_^post3 = ___rho_1_^0 propagated equality got_sighup^post3 = got_sighup^0 propagated equality tmp99^post3 = tmp99^0 propagated equality tmp2^post3 = tmp2^0 propagated equality last_copy_time^post3 = last_copy_time^0 propagated equality ___rho_4_^post3 = ___rho_4_^0 propagated equality tt1^post3 = tt1^0 propagated equality ret_time77^post3 = ret_time77^0 propagated equality ___rho_2_^post3 = ___rho_2_^0 propagated equality curtime^post3 = curtime^0 propagated equality ret_time1010^post3 = ret_time1010^0 propagated equality tmp66^post3 = tmp66^0 propagated equality wakend^post3 = wakend^0 propagated equality a88^post3 = a88^0 propagated equality ret_xlogarchivingactive44^post3 = ret_xlogarchivingactive44^0 propagated equality a55^post3 = a55^0 propagated equality a33^post3 = a33^0 Simplified Guard Original rule: l3 -> l4 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^0, a33^0'=a33^0, a55^0'=a55^0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=ret_time1010^0, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^0, tmp99^0'=tmp99^0, tt1^0'=tt1^0, wakend^0'=wakend^0, 0 == 0, cost: 1 New rule: l3 -> l4 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^0, a33^0'=a33^0, a55^0'=a55^0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=ret_time1010^0, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^0, tmp99^0'=tmp99^0, tt1^0'=tt1^0, wakend^0'=wakend^0, T, cost: 1 Removed Trivial Updates Original rule: l3 -> l4 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^0, a33^0'=a33^0, a55^0'=a55^0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=ret_time1010^0, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^0, tmp99^0'=tmp99^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_1_^0'=___rho_1_^post4, ___rho_2_^0'=___rho_2_^post4, ___rho_4_^0'=___rho_4_^post4, a33^0'=a33^post4, a55^0'=a55^post4, a88^0'=a88^post4, curtime^0'=curtime^post4, got_sighup^0'=got_sighup^post4, last_copy_time^0'=last_copy_time^post4, ret_time1010^0'=ret_time1010^post4, ret_time77^0'=ret_time77^post4, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post4, tmp2^0'=tmp2^post4, tmp66^0'=tmp66^post4, tmp99^0'=tmp99^post4, tt1^0'=tt1^post4, wakend^0'=wakend^post4, (wakend^0-wakend^post4 == 0 /\ -curtime^post4+curtime^0 == 0 /\ -ret_time1010^post4+ret_time1010^0 == 0 /\ -tmp66^post4+tmp66^0 == 0 /\ -a33^post4+a33^0 == 0 /\ ___rho_4_^0-___rho_4_^post4 == 0 /\ tmp2^0-tmp2^post4 == 0 /\ -___rho_2_^post4+___rho_2_^0 == 0 /\ got_sighup^0-got_sighup^post4 == 0 /\ -tt1^post4+tt1^0 == 0 /\ a88^0-a88^post4 == 0 /\ ret_time77^0-ret_time77^post4 == 0 /\ -ret_xlogarchivingactive44^post4+ret_xlogarchivingactive44^0 == 0 /\ -___rho_1_^post4+___rho_1_^0 == 0 /\ -a55^post4+a55^0 == 0 /\ -tmp99^post4+tmp99^0 == 0 /\ -last_copy_time^post4+last_copy_time^0 == 0), cost: 1 New rule: l5 -> l6 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^0, a33^0'=a33^0, a55^0'=a55^0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=ret_time1010^0, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^0, tmp99^0'=tmp99^0, tt1^0'=tt1^0, wakend^0'=wakend^0, 0 == 0, cost: 1 propagated equality wakend^post4 = wakend^0 propagated equality curtime^post4 = curtime^0 propagated equality ret_time1010^post4 = ret_time1010^0 propagated equality tmp66^post4 = tmp66^0 propagated equality a33^post4 = a33^0 propagated equality ___rho_4_^post4 = ___rho_4_^0 propagated equality tmp2^post4 = tmp2^0 propagated equality ___rho_2_^post4 = ___rho_2_^0 propagated equality got_sighup^post4 = got_sighup^0 propagated equality tt1^post4 = tt1^0 propagated equality a88^post4 = a88^0 propagated equality ret_time77^post4 = ret_time77^0 propagated equality ret_xlogarchivingactive44^post4 = ret_xlogarchivingactive44^0 propagated equality ___rho_1_^post4 = ___rho_1_^0 propagated equality a55^post4 = a55^0 propagated equality tmp99^post4 = tmp99^0 propagated equality last_copy_time^post4 = last_copy_time^0 Simplified Guard Original rule: l5 -> l6 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^0, a33^0'=a33^0, a55^0'=a55^0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=ret_time1010^0, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^0, tmp99^0'=tmp99^0, tt1^0'=tt1^0, wakend^0'=wakend^0, 0 == 0, cost: 1 New rule: l5 -> l6 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^0, a33^0'=a33^0, a55^0'=a55^0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=ret_time1010^0, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^0, tmp99^0'=tmp99^0, tt1^0'=tt1^0, wakend^0'=wakend^0, T, cost: 1 Removed Trivial Updates Original rule: l5 -> l6 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^0, a33^0'=a33^0, a55^0'=a55^0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=ret_time1010^0, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^0, tmp99^0'=tmp99^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_1_^0'=___rho_1_^post5, ___rho_2_^0'=___rho_2_^post5, ___rho_4_^0'=___rho_4_^post5, a33^0'=a33^post5, a55^0'=a55^post5, a88^0'=a88^post5, curtime^0'=curtime^post5, got_sighup^0'=got_sighup^post5, last_copy_time^0'=last_copy_time^post5, ret_time1010^0'=ret_time1010^post5, ret_time77^0'=ret_time77^post5, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post5, tmp2^0'=tmp2^post5, tmp66^0'=tmp66^post5, tmp99^0'=tmp99^post5, tt1^0'=tt1^post5, wakend^0'=wakend^post5, (0 == 0 /\ -tt1^post5+tt1^0 == 0 /\ -___rho_2_^post5+___rho_2_^0 == 0 /\ -___rho_1_^post5+___rho_1_^0 == 0 /\ tmp2^0-tmp2^post5 == 0 /\ -wakend^post5+wakend^0 == 0 /\ -last_copy_time^post5+last_copy_time^0 == 0 /\ -tmp99^post5+tmp99^0 == 0 /\ -a55^post5+a55^0 == 0 /\ curtime^0-curtime^post5 == 0 /\ a33^0-a33^post5 == 0 /\ -got_sighup^post5+got_sighup^0 == 0 /\ -ret_time1010^post5+ret_time1010^0 == 0 /\ -ret_time77^post5+ret_time77^0 == 0 /\ -tmp66^post5+tmp66^0 == 0 /\ a88^0-a88^post5 == 0 /\ ret_xlogarchivingactive44^0-ret_xlogarchivingactive44^post5 == 0), cost: 1 New rule: l7 -> l5 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^post5, a33^0'=a33^0, a55^0'=a55^0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=ret_time1010^0, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^0, tmp99^0'=tmp99^0, tt1^0'=tt1^0, wakend^0'=wakend^0, 0 == 0, cost: 1 propagated equality tt1^post5 = tt1^0 propagated equality ___rho_2_^post5 = ___rho_2_^0 propagated equality ___rho_1_^post5 = ___rho_1_^0 propagated equality tmp2^post5 = tmp2^0 propagated equality wakend^post5 = wakend^0 propagated equality last_copy_time^post5 = last_copy_time^0 propagated equality tmp99^post5 = tmp99^0 propagated equality a55^post5 = a55^0 propagated equality curtime^post5 = curtime^0 propagated equality a33^post5 = a33^0 propagated equality got_sighup^post5 = got_sighup^0 propagated equality ret_time1010^post5 = ret_time1010^0 propagated equality ret_time77^post5 = ret_time77^0 propagated equality tmp66^post5 = tmp66^0 propagated equality a88^post5 = a88^0 propagated equality ret_xlogarchivingactive44^post5 = ret_xlogarchivingactive44^0 Simplified Guard Original rule: l7 -> l5 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^post5, a33^0'=a33^0, a55^0'=a55^0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=ret_time1010^0, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^0, tmp99^0'=tmp99^0, tt1^0'=tt1^0, wakend^0'=wakend^0, 0 == 0, cost: 1 New rule: l7 -> l5 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^post5, a33^0'=a33^0, a55^0'=a55^0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=ret_time1010^0, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^0, tmp99^0'=tmp99^0, tt1^0'=tt1^0, wakend^0'=wakend^0, T, cost: 1 Removed Trivial Updates Original rule: l7 -> l5 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^post5, a33^0'=a33^0, a55^0'=a55^0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=ret_time1010^0, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^0, tmp99^0'=tmp99^0, tt1^0'=tt1^0, wakend^0'=wakend^0, T, cost: 1 New rule: l7 -> l5 : ___rho_4_^0'=___rho_4_^post5, T, cost: 1 Propagated Equalities Original rule: l8 -> l7 : ___rho_1_^0'=___rho_1_^post6, ___rho_2_^0'=___rho_2_^post6, ___rho_4_^0'=___rho_4_^post6, a33^0'=a33^post6, a55^0'=a55^post6, a88^0'=a88^post6, curtime^0'=curtime^post6, got_sighup^0'=got_sighup^post6, last_copy_time^0'=last_copy_time^post6, ret_time1010^0'=ret_time1010^post6, ret_time77^0'=ret_time77^post6, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post6, tmp2^0'=tmp2^post6, tmp66^0'=tmp66^post6, tmp99^0'=tmp99^post6, tt1^0'=tt1^post6, wakend^0'=wakend^post6, (tmp2^0-tmp2^post6 == 0 /\ -tmp66^post6+tmp66^0 == 0 /\ -last_copy_time^post6+last_copy_time^0 == 0 /\ tmp99^0-tmp99^post6 == 0 /\ ___rho_2_^0-___rho_2_^post6 == 0 /\ -curtime^post6+curtime^0 == 0 /\ ret_time77^0-ret_time77^post6 == 0 /\ a88^0-a88^post6 == 0 /\ got_sighup^0-got_sighup^post6 == 0 /\ -999-last_copy_time^0+curtime^0 <= 0 /\ ___rho_4_^0-___rho_4_^post6 == 0 /\ wakend^0-wakend^post6 == 0 /\ -a33^post6+a33^0 == 0 /\ -ret_time1010^post6+ret_time1010^0 == 0 /\ a55^0-a55^post6 == 0 /\ -ret_xlogarchivingactive44^post6+ret_xlogarchivingactive44^0 == 0 /\ -tt1^post6+tt1^0 == 0 /\ -___rho_1_^post6+___rho_1_^0 == 0), cost: 1 New rule: l8 -> l7 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^0, a33^0'=a33^0, a55^0'=a55^0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=ret_time1010^0, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^0, tmp99^0'=tmp99^0, tt1^0'=tt1^0, wakend^0'=wakend^0, (0 == 0 /\ -999-last_copy_time^0+curtime^0 <= 0), cost: 1 propagated equality tmp2^post6 = tmp2^0 propagated equality tmp66^post6 = tmp66^0 propagated equality last_copy_time^post6 = last_copy_time^0 propagated equality tmp99^post6 = tmp99^0 propagated equality ___rho_2_^post6 = ___rho_2_^0 propagated equality curtime^post6 = curtime^0 propagated equality ret_time77^post6 = ret_time77^0 propagated equality a88^post6 = a88^0 propagated equality got_sighup^post6 = got_sighup^0 propagated equality ___rho_4_^post6 = ___rho_4_^0 propagated equality wakend^post6 = wakend^0 propagated equality a33^post6 = a33^0 propagated equality ret_time1010^post6 = ret_time1010^0 propagated equality a55^post6 = a55^0 propagated equality ret_xlogarchivingactive44^post6 = ret_xlogarchivingactive44^0 propagated equality tt1^post6 = tt1^0 propagated equality ___rho_1_^post6 = ___rho_1_^0 Simplified Guard Original rule: l8 -> l7 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^0, a33^0'=a33^0, a55^0'=a55^0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=ret_time1010^0, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^0, tmp99^0'=tmp99^0, tt1^0'=tt1^0, wakend^0'=wakend^0, (0 == 0 /\ -999-last_copy_time^0+curtime^0 <= 0), cost: 1 New rule: l8 -> l7 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^0, a33^0'=a33^0, a55^0'=a55^0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=ret_time1010^0, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^0, tmp99^0'=tmp99^0, tt1^0'=tt1^0, wakend^0'=wakend^0, -999-last_copy_time^0+curtime^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l8 -> l7 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^0, a33^0'=a33^0, a55^0'=a55^0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=ret_time1010^0, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^0, tmp99^0'=tmp99^0, tt1^0'=tt1^0, wakend^0'=wakend^0, -999-last_copy_time^0+curtime^0 <= 0, cost: 1 New rule: l8 -> l7 : -999-last_copy_time^0+curtime^0 <= 0, cost: 1 Propagated Equalities Original rule: l8 -> l7 : ___rho_1_^0'=___rho_1_^post7, ___rho_2_^0'=___rho_2_^post7, ___rho_4_^0'=___rho_4_^post7, a33^0'=a33^post7, a55^0'=a55^post7, a88^0'=a88^post7, curtime^0'=curtime^post7, got_sighup^0'=got_sighup^post7, last_copy_time^0'=last_copy_time^post7, ret_time1010^0'=ret_time1010^post7, ret_time77^0'=ret_time77^post7, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post7, tmp2^0'=tmp2^post7, tmp66^0'=tmp66^post7, tmp99^0'=tmp99^post7, tt1^0'=tt1^post7, wakend^0'=wakend^post7, (a88^0-a88^post7 == 0 /\ -a55^post7+a55^0 == 0 /\ -___rho_1_^post7+___rho_1_^0 == 0 /\ -tt1^post7+tt1^0 == 0 /\ -ret_time77^post7+ret_time77^0 == 0 /\ -tmp66^post7+tmp66^0 == 0 /\ 1000+last_copy_time^0-curtime^0 <= 0 /\ -tmp99^post7+tmp99^0 == 0 /\ ___rho_4_^0-___rho_4_^post7 == 0 /\ -last_copy_time^post7+last_copy_time^0 == 0 /\ -a33^post7+a33^0 == 0 /\ -___rho_2_^post7+___rho_2_^0 == 0 /\ -got_sighup^post7+got_sighup^0 == 0 /\ tmp2^0-tmp2^post7 == 0 /\ ret_xlogarchivingactive44^0-ret_xlogarchivingactive44^post7 == 0 /\ -ret_time1010^post7+ret_time1010^0 == 0 /\ -1+wakend^post7 == 0 /\ curtime^0-curtime^post7 == 0), cost: 1 New rule: l8 -> l7 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^0, a33^0'=a33^0, a55^0'=a55^0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=ret_time1010^0, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^0, tmp99^0'=tmp99^0, tt1^0'=tt1^0, wakend^0'=1, (0 == 0 /\ 1000+last_copy_time^0-curtime^0 <= 0), cost: 1 propagated equality a88^post7 = a88^0 propagated equality a55^post7 = a55^0 propagated equality ___rho_1_^post7 = ___rho_1_^0 propagated equality tt1^post7 = tt1^0 propagated equality ret_time77^post7 = ret_time77^0 propagated equality tmp66^post7 = tmp66^0 propagated equality tmp99^post7 = tmp99^0 propagated equality ___rho_4_^post7 = ___rho_4_^0 propagated equality last_copy_time^post7 = last_copy_time^0 propagated equality a33^post7 = a33^0 propagated equality ___rho_2_^post7 = ___rho_2_^0 propagated equality got_sighup^post7 = got_sighup^0 propagated equality tmp2^post7 = tmp2^0 propagated equality ret_xlogarchivingactive44^post7 = ret_xlogarchivingactive44^0 propagated equality ret_time1010^post7 = ret_time1010^0 propagated equality wakend^post7 = 1 propagated equality curtime^post7 = curtime^0 Simplified Guard Original rule: l8 -> l7 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^0, a33^0'=a33^0, a55^0'=a55^0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=ret_time1010^0, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^0, tmp99^0'=tmp99^0, tt1^0'=tt1^0, wakend^0'=1, (0 == 0 /\ 1000+last_copy_time^0-curtime^0 <= 0), cost: 1 New rule: l8 -> l7 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^0, a33^0'=a33^0, a55^0'=a55^0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=ret_time1010^0, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^0, tmp99^0'=tmp99^0, tt1^0'=tt1^0, wakend^0'=1, 1000+last_copy_time^0-curtime^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l8 -> l7 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^0, a33^0'=a33^0, a55^0'=a55^0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=ret_time1010^0, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^0, tmp99^0'=tmp99^0, tt1^0'=tt1^0, wakend^0'=1, 1000+last_copy_time^0-curtime^0 <= 0, cost: 1 New rule: l8 -> l7 : wakend^0'=1, 1000+last_copy_time^0-curtime^0 <= 0, cost: 1 Propagated Equalities Original rule: l9 -> l7 : ___rho_1_^0'=___rho_1_^post8, ___rho_2_^0'=___rho_2_^post8, ___rho_4_^0'=___rho_4_^post8, a33^0'=a33^post8, a55^0'=a55^post8, a88^0'=a88^post8, curtime^0'=curtime^post8, got_sighup^0'=got_sighup^post8, last_copy_time^0'=last_copy_time^post8, ret_time1010^0'=ret_time1010^post8, ret_time77^0'=ret_time77^post8, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post8, tmp2^0'=tmp2^post8, tmp66^0'=tmp66^post8, tmp99^0'=tmp99^post8, tt1^0'=tt1^post8, wakend^0'=wakend^post8, (1-wakend^0 <= 0 /\ tmp2^0-tmp2^post8 == 0 /\ ret_xlogarchivingactive44^0-ret_xlogarchivingactive44^post8 == 0 /\ -tmp66^post8+tmp66^0 == 0 /\ -last_copy_time^post8+last_copy_time^0 == 0 /\ tmp99^0-tmp99^post8 == 0 /\ -got_sighup^post8+got_sighup^0 == 0 /\ a88^0-a88^post8 == 0 /\ -a55^post8+a55^0 == 0 /\ -wakend^post8+wakend^0 == 0 /\ -___rho_2_^post8+___rho_2_^0 == 0 /\ -ret_time1010^post8+ret_time1010^0 == 0 /\ ___rho_4_^0-___rho_4_^post8 == 0 /\ -curtime^post8+curtime^0 == 0 /\ -a33^post8+a33^0 == 0 /\ -___rho_1_^post8+___rho_1_^0 == 0 /\ -tt1^post8+tt1^0 == 0 /\ -ret_time77^post8+ret_time77^0 == 0), cost: 1 New rule: l9 -> l7 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^0, a33^0'=a33^0, a55^0'=a55^0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=ret_time1010^0, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^0, tmp99^0'=tmp99^0, tt1^0'=tt1^0, wakend^0'=wakend^0, (0 == 0 /\ 1-wakend^0 <= 0), cost: 1 propagated equality tmp2^post8 = tmp2^0 propagated equality ret_xlogarchivingactive44^post8 = ret_xlogarchivingactive44^0 propagated equality tmp66^post8 = tmp66^0 propagated equality last_copy_time^post8 = last_copy_time^0 propagated equality tmp99^post8 = tmp99^0 propagated equality got_sighup^post8 = got_sighup^0 propagated equality a88^post8 = a88^0 propagated equality a55^post8 = a55^0 propagated equality wakend^post8 = wakend^0 propagated equality ___rho_2_^post8 = ___rho_2_^0 propagated equality ret_time1010^post8 = ret_time1010^0 propagated equality ___rho_4_^post8 = ___rho_4_^0 propagated equality curtime^post8 = curtime^0 propagated equality a33^post8 = a33^0 propagated equality ___rho_1_^post8 = ___rho_1_^0 propagated equality tt1^post8 = tt1^0 propagated equality ret_time77^post8 = ret_time77^0 Simplified Guard Original rule: l9 -> l7 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^0, a33^0'=a33^0, a55^0'=a55^0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=ret_time1010^0, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^0, tmp99^0'=tmp99^0, tt1^0'=tt1^0, wakend^0'=wakend^0, (0 == 0 /\ 1-wakend^0 <= 0), cost: 1 New rule: l9 -> l7 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^0, a33^0'=a33^0, a55^0'=a55^0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=ret_time1010^0, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^0, tmp99^0'=tmp99^0, tt1^0'=tt1^0, wakend^0'=wakend^0, 1-wakend^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l9 -> l7 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^0, a33^0'=a33^0, a55^0'=a55^0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=ret_time1010^0, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^0, tmp99^0'=tmp99^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_1_^0'=___rho_1_^post9, ___rho_2_^0'=___rho_2_^post9, ___rho_4_^0'=___rho_4_^post9, a33^0'=a33^post9, a55^0'=a55^post9, a88^0'=a88^post9, curtime^0'=curtime^post9, got_sighup^0'=got_sighup^post9, last_copy_time^0'=last_copy_time^post9, ret_time1010^0'=ret_time1010^post9, ret_time77^0'=ret_time77^post9, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post9, tmp2^0'=tmp2^post9, tmp66^0'=tmp66^post9, tmp99^0'=tmp99^post9, tt1^0'=tt1^post9, wakend^0'=wakend^post9, (0 == 0 /\ ret_time77^0-ret_time77^post9 == 0 /\ a88^post9 == 0 /\ a55^0-a55^post9 == 0 /\ -a33^post9+a33^0 == 0 /\ -___rho_1_^post9+___rho_1_^0 == 0 /\ -tt1^post9+tt1^0 == 0 /\ ___rho_2_^0-___rho_2_^post9 == 0 /\ last_copy_time^0-last_copy_time^post9 == 0 /\ wakend^0 <= 0 /\ got_sighup^0-got_sighup^post9 == 0 /\ -tmp66^post9+tmp66^0 == 0 /\ -ret_time1010^post9+curtime^post9 == 0 /\ -___rho_4_^post9+___rho_4_^0 == 0 /\ ret_xlogarchivingactive44^0-ret_xlogarchivingactive44^post9 == 0 /\ tmp2^0-tmp2^post9 == 0 /\ -wakend^post9+wakend^0 == 0 /\ ret_time1010^post9-tmp99^post9 == 0), cost: 1 New rule: l9 -> l8 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^0, a33^0'=a33^0, a55^0'=a55^0, a88^0'=0, curtime^0'=tmp99^post9, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=tmp99^post9, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^0, tmp99^0'=tmp99^post9, tt1^0'=tt1^0, wakend^0'=wakend^0, (0 == 0 /\ wakend^0 <= 0), cost: 1 propagated equality ret_time77^post9 = ret_time77^0 propagated equality a88^post9 = 0 propagated equality a55^post9 = a55^0 propagated equality a33^post9 = a33^0 propagated equality ___rho_1_^post9 = ___rho_1_^0 propagated equality tt1^post9 = tt1^0 propagated equality ___rho_2_^post9 = ___rho_2_^0 propagated equality last_copy_time^post9 = last_copy_time^0 propagated equality got_sighup^post9 = got_sighup^0 propagated equality tmp66^post9 = tmp66^0 propagated equality curtime^post9 = ret_time1010^post9 propagated equality ___rho_4_^post9 = ___rho_4_^0 propagated equality ret_xlogarchivingactive44^post9 = ret_xlogarchivingactive44^0 propagated equality tmp2^post9 = tmp2^0 propagated equality wakend^post9 = wakend^0 propagated equality ret_time1010^post9 = tmp99^post9 Simplified Guard Original rule: l9 -> l8 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^0, a33^0'=a33^0, a55^0'=a55^0, a88^0'=0, curtime^0'=tmp99^post9, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=tmp99^post9, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^0, tmp99^0'=tmp99^post9, tt1^0'=tt1^0, wakend^0'=wakend^0, (0 == 0 /\ wakend^0 <= 0), cost: 1 New rule: l9 -> l8 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^0, a33^0'=a33^0, a55^0'=a55^0, a88^0'=0, curtime^0'=tmp99^post9, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=tmp99^post9, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^0, tmp99^0'=tmp99^post9, tt1^0'=tt1^0, wakend^0'=wakend^0, wakend^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l9 -> l8 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^0, a33^0'=a33^0, a55^0'=a55^0, a88^0'=0, curtime^0'=tmp99^post9, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=tmp99^post9, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^0, tmp99^0'=tmp99^post9, tt1^0'=tt1^0, wakend^0'=wakend^0, wakend^0 <= 0, cost: 1 New rule: l9 -> l8 : a88^0'=0, curtime^0'=tmp99^post9, ret_time1010^0'=tmp99^post9, tmp99^0'=tmp99^post9, wakend^0 <= 0, cost: 1 Propagated Equalities Original rule: l1 -> l9 : ___rho_1_^0'=___rho_1_^post10, ___rho_2_^0'=___rho_2_^post10, ___rho_4_^0'=___rho_4_^post10, a33^0'=a33^post10, a55^0'=a55^post10, a88^0'=a88^post10, curtime^0'=curtime^post10, got_sighup^0'=got_sighup^post10, last_copy_time^0'=last_copy_time^post10, ret_time1010^0'=ret_time1010^post10, ret_time77^0'=ret_time77^post10, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post10, tmp2^0'=tmp2^post10, tmp66^0'=tmp66^post10, tmp99^0'=tmp99^post10, tt1^0'=tt1^post10, wakend^0'=wakend^post10, (ret_xlogarchivingactive44^0-ret_xlogarchivingactive44^post10 == 0 /\ -wakend^post10+wakend^0 == 0 /\ -last_copy_time^post10+last_copy_time^0 == 0 /\ -tt1^post10+tt1^0 == 0 /\ tmp2^0-tmp2^post10 == 0 /\ -tmp99^post10+tmp99^0 == 0 /\ -ret_time1010^post10+ret_time1010^0 == 0 /\ -got_sighup^post10+got_sighup^0 == 0 /\ a88^0-a88^post10 == 0 /\ wakend^0 <= 0 /\ -a33^post10+a33^0 == 0 /\ -a55^post10+a55^0 == 0 /\ -___rho_2_^post10+___rho_2_^0 == 0 /\ curtime^0-curtime^post10 == 0 /\ -___rho_1_^post10+___rho_1_^0 == 0 /\ -ret_time77^post10+ret_time77^0 == 0 /\ ___rho_4_^0-___rho_4_^post10 == 0 /\ -tmp66^post10+tmp66^0 == 0), cost: 1 New rule: l1 -> l9 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^0, a33^0'=a33^0, a55^0'=a55^0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=ret_time1010^0, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^0, tmp99^0'=tmp99^0, tt1^0'=tt1^0, wakend^0'=wakend^0, (0 == 0 /\ wakend^0 <= 0), cost: 1 propagated equality ret_xlogarchivingactive44^post10 = ret_xlogarchivingactive44^0 propagated equality wakend^post10 = wakend^0 propagated equality last_copy_time^post10 = last_copy_time^0 propagated equality tt1^post10 = tt1^0 propagated equality tmp2^post10 = tmp2^0 propagated equality tmp99^post10 = tmp99^0 propagated equality ret_time1010^post10 = ret_time1010^0 propagated equality got_sighup^post10 = got_sighup^0 propagated equality a88^post10 = a88^0 propagated equality a33^post10 = a33^0 propagated equality a55^post10 = a55^0 propagated equality ___rho_2_^post10 = ___rho_2_^0 propagated equality curtime^post10 = curtime^0 propagated equality ___rho_1_^post10 = ___rho_1_^0 propagated equality ret_time77^post10 = ret_time77^0 propagated equality ___rho_4_^post10 = ___rho_4_^0 propagated equality tmp66^post10 = tmp66^0 Simplified Guard Original rule: l1 -> l9 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^0, a33^0'=a33^0, a55^0'=a55^0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=ret_time1010^0, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^0, tmp99^0'=tmp99^0, tt1^0'=tt1^0, wakend^0'=wakend^0, (0 == 0 /\ wakend^0 <= 0), cost: 1 New rule: l1 -> l9 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^0, a33^0'=a33^0, a55^0'=a55^0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=ret_time1010^0, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^0, tmp99^0'=tmp99^0, tt1^0'=tt1^0, wakend^0'=wakend^0, wakend^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l1 -> l9 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^0, a33^0'=a33^0, a55^0'=a55^0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=ret_time1010^0, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^0, tmp99^0'=tmp99^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_1_^0'=___rho_1_^post11, ___rho_2_^0'=___rho_2_^post11, ___rho_4_^0'=___rho_4_^post11, a33^0'=a33^post11, a55^0'=a55^post11, a88^0'=a88^post11, curtime^0'=curtime^post11, got_sighup^0'=got_sighup^post11, last_copy_time^0'=last_copy_time^post11, ret_time1010^0'=ret_time1010^post11, ret_time77^0'=ret_time77^post11, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post11, tmp2^0'=tmp2^post11, tmp66^0'=tmp66^post11, tmp99^0'=tmp99^post11, tt1^0'=tt1^post11, wakend^0'=wakend^post11, (0 == 0 /\ -a88^post11+a88^0 == 0 /\ 1-wakend^0 <= 0 /\ -___rho_4_^post11+___rho_4_^0 == 0 /\ -a33^post11+a33^0 == 0 /\ -___rho_1_^post11+___rho_1_^0 == 0 /\ tmp99^0-tmp99^post11 == 0 /\ wakend^post11 == 0 /\ ___rho_2_^0-___rho_2_^post11 == 0 /\ -tt1^post11+tt1^0 == 0 /\ a55^post11 == 0 /\ ret_xlogarchivingactive44^0-ret_xlogarchivingactive44^post11 == 0 /\ -tmp66^post11+ret_time77^post11 == 0 /\ -ret_time1010^post11+ret_time1010^0 == 0 /\ -tmp2^post11+tmp2^0 == 0 /\ -curtime^post11+curtime^0 == 0 /\ -got_sighup^post11+got_sighup^0 == 0 /\ -ret_time77^post11+last_copy_time^post11 == 0), cost: 1 New rule: l1 -> l9 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^0, a33^0'=a33^0, a55^0'=0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=tmp66^post11, ret_time1010^0'=ret_time1010^0, ret_time77^0'=tmp66^post11, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^post11, tmp99^0'=tmp99^0, tt1^0'=tt1^0, wakend^0'=0, (0 == 0 /\ 1-wakend^0 <= 0), cost: 1 propagated equality a88^post11 = a88^0 propagated equality ___rho_4_^post11 = ___rho_4_^0 propagated equality a33^post11 = a33^0 propagated equality ___rho_1_^post11 = ___rho_1_^0 propagated equality tmp99^post11 = tmp99^0 propagated equality wakend^post11 = 0 propagated equality ___rho_2_^post11 = ___rho_2_^0 propagated equality tt1^post11 = tt1^0 propagated equality a55^post11 = 0 propagated equality ret_xlogarchivingactive44^post11 = ret_xlogarchivingactive44^0 propagated equality ret_time77^post11 = tmp66^post11 propagated equality ret_time1010^post11 = ret_time1010^0 propagated equality tmp2^post11 = tmp2^0 propagated equality curtime^post11 = curtime^0 propagated equality got_sighup^post11 = got_sighup^0 propagated equality last_copy_time^post11 = tmp66^post11 Simplified Guard Original rule: l1 -> l9 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^0, a33^0'=a33^0, a55^0'=0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=tmp66^post11, ret_time1010^0'=ret_time1010^0, ret_time77^0'=tmp66^post11, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^post11, tmp99^0'=tmp99^0, tt1^0'=tt1^0, wakend^0'=0, (0 == 0 /\ 1-wakend^0 <= 0), cost: 1 New rule: l1 -> l9 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^0, a33^0'=a33^0, a55^0'=0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=tmp66^post11, ret_time1010^0'=ret_time1010^0, ret_time77^0'=tmp66^post11, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^post11, tmp99^0'=tmp99^0, tt1^0'=tt1^0, wakend^0'=0, 1-wakend^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l1 -> l9 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^0, a33^0'=a33^0, a55^0'=0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=tmp66^post11, ret_time1010^0'=ret_time1010^0, ret_time77^0'=tmp66^post11, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^post11, tmp99^0'=tmp99^0, tt1^0'=tt1^0, wakend^0'=0, 1-wakend^0 <= 0, cost: 1 New rule: l1 -> l9 : a55^0'=0, last_copy_time^0'=tmp66^post11, ret_time77^0'=tmp66^post11, tmp66^0'=tmp66^post11, wakend^0'=0, 1-wakend^0 <= 0, cost: 1 Propagated Equalities Original rule: l2 -> l1 : ___rho_1_^0'=___rho_1_^post14, ___rho_2_^0'=___rho_2_^post14, ___rho_4_^0'=___rho_4_^post14, a33^0'=a33^post14, a55^0'=a55^post14, a88^0'=a88^post14, curtime^0'=curtime^post14, got_sighup^0'=got_sighup^post14, last_copy_time^0'=last_copy_time^post14, ret_time1010^0'=ret_time1010^post14, ret_time77^0'=ret_time77^post14, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post14, tmp2^0'=tmp2^post14, tmp66^0'=tmp66^post14, tmp99^0'=tmp99^post14, tt1^0'=tt1^post14, wakend^0'=wakend^post14, (-ret_xlogarchivingactive44^post14+ret_xlogarchivingactive44^0 == 0 /\ -tmp99^post14+tmp99^0 == 0 /\ got_sighup^0-got_sighup^post14 == 0 /\ -curtime^post14+curtime^0 == 0 /\ -___rho_2_^post14+___rho_2_^0 == 0 /\ -last_copy_time^post14+last_copy_time^0 == 0 /\ tmp2^0-tmp2^post14 == 0 /\ -a33^post14+a33^0 == 0 /\ ___rho_4_^0-___rho_4_^post14 == 0 /\ ret_time77^0-ret_time77^post14 == 0 /\ a88^0-a88^post14 == 0 /\ -___rho_1_^post14+___rho_1_^0 == 0 /\ -a55^post14+a55^0 == 0 /\ -tt1^post14+tt1^0 == 0 /\ 1-tt1^0 <= 0 /\ wakend^0-wakend^post14 == 0 /\ tmp66^0-tmp66^post14 == 0 /\ -ret_time1010^post14+ret_time1010^0 == 0), cost: 1 New rule: l2 -> l1 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^0, a33^0'=a33^0, a55^0'=a55^0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=ret_time1010^0, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^0, tmp99^0'=tmp99^0, tt1^0'=tt1^0, wakend^0'=wakend^0, (0 == 0 /\ 1-tt1^0 <= 0), cost: 1 propagated equality ret_xlogarchivingactive44^post14 = ret_xlogarchivingactive44^0 propagated equality tmp99^post14 = tmp99^0 propagated equality got_sighup^post14 = got_sighup^0 propagated equality curtime^post14 = curtime^0 propagated equality ___rho_2_^post14 = ___rho_2_^0 propagated equality last_copy_time^post14 = last_copy_time^0 propagated equality tmp2^post14 = tmp2^0 propagated equality a33^post14 = a33^0 propagated equality ___rho_4_^post14 = ___rho_4_^0 propagated equality ret_time77^post14 = ret_time77^0 propagated equality a88^post14 = a88^0 propagated equality ___rho_1_^post14 = ___rho_1_^0 propagated equality a55^post14 = a55^0 propagated equality tt1^post14 = tt1^0 propagated equality wakend^post14 = wakend^0 propagated equality tmp66^post14 = tmp66^0 propagated equality ret_time1010^post14 = ret_time1010^0 Simplified Guard Original rule: l2 -> l1 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^0, a33^0'=a33^0, a55^0'=a55^0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=ret_time1010^0, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^0, tmp99^0'=tmp99^0, tt1^0'=tt1^0, wakend^0'=wakend^0, (0 == 0 /\ 1-tt1^0 <= 0), cost: 1 New rule: l2 -> l1 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^0, a33^0'=a33^0, a55^0'=a55^0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=ret_time1010^0, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^0, tmp99^0'=tmp99^0, tt1^0'=tt1^0, wakend^0'=wakend^0, 1-tt1^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l2 -> l1 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^0, a33^0'=a33^0, a55^0'=a55^0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=ret_time1010^0, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^0, tmp99^0'=tmp99^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_1_^0'=___rho_1_^post15, ___rho_2_^0'=___rho_2_^post15, ___rho_4_^0'=___rho_4_^post15, a33^0'=a33^post15, a55^0'=a55^post15, a88^0'=a88^post15, curtime^0'=curtime^post15, got_sighup^0'=got_sighup^post15, last_copy_time^0'=last_copy_time^post15, ret_time1010^0'=ret_time1010^post15, ret_time77^0'=ret_time77^post15, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post15, tmp2^0'=tmp2^post15, tmp66^0'=tmp66^post15, tmp99^0'=tmp99^post15, tt1^0'=tt1^post15, wakend^0'=wakend^post15, (ret_xlogarchivingactive44^0-ret_xlogarchivingactive44^post15 == 0 /\ -last_copy_time^post15+last_copy_time^0 == 0 /\ ___rho_4_^0-___rho_4_^post15 == 0 /\ -a55^post15+a55^0 == 0 /\ -___rho_1_^post15+___rho_1_^0 == 0 /\ -got_sighup^post15+got_sighup^0 == 0 /\ a88^0-a88^post15 == 0 /\ -tt1^post15+tt1^0 == 0 /\ -ret_time1010^post15+ret_time1010^0 == 0 /\ -tmp99^post15+tmp99^0 == 0 /\ curtime^0-curtime^post15 == 0 /\ wakend^0-wakend^post15 == 0 /\ -tmp66^post15+tmp66^0 == 0 /\ -a33^post15+a33^0 == 0 /\ -___rho_2_^post15+___rho_2_^0 == 0 /\ tmp2^0-tmp2^post15 == 0 /\ tt1^0 <= 0 /\ -ret_time77^post15+ret_time77^0 == 0), cost: 1 New rule: l2 -> l5 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^0, a33^0'=a33^0, a55^0'=a55^0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=ret_time1010^0, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^0, tmp99^0'=tmp99^0, tt1^0'=tt1^0, wakend^0'=wakend^0, (0 == 0 /\ tt1^0 <= 0), cost: 1 propagated equality ret_xlogarchivingactive44^post15 = ret_xlogarchivingactive44^0 propagated equality last_copy_time^post15 = last_copy_time^0 propagated equality ___rho_4_^post15 = ___rho_4_^0 propagated equality a55^post15 = a55^0 propagated equality ___rho_1_^post15 = ___rho_1_^0 propagated equality got_sighup^post15 = got_sighup^0 propagated equality a88^post15 = a88^0 propagated equality tt1^post15 = tt1^0 propagated equality ret_time1010^post15 = ret_time1010^0 propagated equality tmp99^post15 = tmp99^0 propagated equality curtime^post15 = curtime^0 propagated equality wakend^post15 = wakend^0 propagated equality tmp66^post15 = tmp66^0 propagated equality a33^post15 = a33^0 propagated equality ___rho_2_^post15 = ___rho_2_^0 propagated equality tmp2^post15 = tmp2^0 propagated equality ret_time77^post15 = ret_time77^0 Simplified Guard Original rule: l2 -> l5 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^0, a33^0'=a33^0, a55^0'=a55^0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=ret_time1010^0, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^0, tmp99^0'=tmp99^0, tt1^0'=tt1^0, wakend^0'=wakend^0, (0 == 0 /\ tt1^0 <= 0), cost: 1 New rule: l2 -> l5 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^0, a33^0'=a33^0, a55^0'=a55^0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=ret_time1010^0, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^0, tmp99^0'=tmp99^0, tt1^0'=tt1^0, wakend^0'=wakend^0, tt1^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l2 -> l5 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^0, a33^0'=a33^0, a55^0'=a55^0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=ret_time1010^0, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^0, tmp99^0'=tmp99^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_1_^0'=___rho_1_^post16, ___rho_2_^0'=___rho_2_^post16, ___rho_4_^0'=___rho_4_^post16, a33^0'=a33^post16, a55^0'=a55^post16, a88^0'=a88^post16, curtime^0'=curtime^post16, got_sighup^0'=got_sighup^post16, last_copy_time^0'=last_copy_time^post16, ret_time1010^0'=ret_time1010^post16, ret_time77^0'=ret_time77^post16, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post16, tmp2^0'=tmp2^post16, tmp66^0'=tmp66^post16, tmp99^0'=tmp99^post16, tt1^0'=tt1^post16, wakend^0'=wakend^post16, (0 == 0 /\ a55^post17-a55^post16 == 0 /\ -___rho_1_^post17+___rho_1_^0 == 0 /\ -___rho_2_^post17+___rho_2_^0 == 0 /\ -a55^post17+a55^0 == 0 /\ -got_sighup^post17+got_sighup^0 == 0 /\ -ret_xlogarchivingactive44^post16+ret_xlogarchivingactive44^post17 == 0 /\ tmp66^post17-tmp66^post16 == 0 /\ a88^0-a88^post17 == 0 /\ -tmp99^post16+tmp99^post17 == 0 /\ -tmp2^post17+tmp2^0 == 0 /\ -1+wakend^post16 == 0 /\ -curtime^post16+curtime^post17 == 0 /\ ret_xlogarchivingactive44^0-ret_xlogarchivingactive44^post17 == 0 /\ ret_time77^post17-ret_time77^post16 == 0 /\ -tt1^post17+tt1^0 == 0 /\ -ret_time77^post17+ret_time77^0 == 0 /\ -ret_time1010^post17+ret_time1010^0 == 0 /\ ___rho_4_^0-___rho_4_^post17 == 0 /\ -1+wakend^1 == 0 /\ -tt1^post16+tt1^post17 == 0 /\ -a88^post16+a88^post17 == 0 /\ tmp2^post17-tmp2^post16 == 0 /\ -___rho_2_^post17+got_sighup^post16 == 0 /\ ___rho_2_^post17-___rho_2_^post16 == 0 /\ -tmp66^post17+tmp66^0 == 0 /\ -last_copy_time^post16+last_copy_time^post17 == 0 /\ -wakend^post17+wakend^0 == 0 /\ -___rho_4_^post16+___rho_4_^post17 == 0 /\ tmp99^0-tmp99^post17 == 0 /\ -last_copy_time^post17+last_copy_time^0 == 0 /\ ret_time1010^post17-ret_time1010^post16 == 0 /\ curtime^0-curtime^post17 == 0 /\ a33^0-a33^post17 == 0 /\ -a33^post16+a33^post17 == 0), cost: 1 New rule: l12 -> l0 : ___rho_1_^0'=___rho_1_^post16, ___rho_2_^0'=___rho_2_^post17, ___rho_4_^0'=___rho_4_^post17, a33^0'=a33^post17, a55^0'=a55^post17, a88^0'=a88^post17, curtime^0'=curtime^post17, got_sighup^0'=___rho_2_^post17, last_copy_time^0'=last_copy_time^post17, ret_time1010^0'=ret_time1010^post17, ret_time77^0'=ret_time77^post17, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post17, tmp2^0'=tmp2^post17, tmp66^0'=tmp66^post17, tmp99^0'=tmp99^post17, tt1^0'=tt1^post17, wakend^0'=1, (0 == 0 /\ -___rho_1_^post17+___rho_1_^0 == 0 /\ -___rho_2_^post17+___rho_2_^0 == 0 /\ -a55^post17+a55^0 == 0 /\ -got_sighup^post17+got_sighup^0 == 0 /\ a88^0-a88^post17 == 0 /\ -tmp2^post17+tmp2^0 == 0 /\ ret_xlogarchivingactive44^0-ret_xlogarchivingactive44^post17 == 0 /\ -tt1^post17+tt1^0 == 0 /\ -ret_time77^post17+ret_time77^0 == 0 /\ -ret_time1010^post17+ret_time1010^0 == 0 /\ ___rho_4_^0-___rho_4_^post17 == 0 /\ -1+wakend^1 == 0 /\ -tmp66^post17+tmp66^0 == 0 /\ -wakend^post17+wakend^0 == 0 /\ tmp99^0-tmp99^post17 == 0 /\ -last_copy_time^post17+last_copy_time^0 == 0 /\ curtime^0-curtime^post17 == 0 /\ a33^0-a33^post17 == 0), cost: 1 propagated equality a55^post16 = a55^post17 propagated equality ret_xlogarchivingactive44^post16 = ret_xlogarchivingactive44^post17 propagated equality tmp66^post16 = tmp66^post17 propagated equality tmp99^post16 = tmp99^post17 propagated equality wakend^post16 = 1 propagated equality curtime^post16 = curtime^post17 propagated equality ret_time77^post16 = ret_time77^post17 propagated equality tt1^post16 = tt1^post17 propagated equality a88^post16 = a88^post17 propagated equality tmp2^post16 = tmp2^post17 propagated equality got_sighup^post16 = ___rho_2_^post17 propagated equality ___rho_2_^post16 = ___rho_2_^post17 propagated equality last_copy_time^post16 = last_copy_time^post17 propagated equality ___rho_4_^post16 = ___rho_4_^post17 propagated equality ret_time1010^post16 = ret_time1010^post17 propagated equality a33^post16 = a33^post17 Propagated Equalities Original rule: l12 -> l0 : ___rho_1_^0'=___rho_1_^post16, ___rho_2_^0'=___rho_2_^post17, ___rho_4_^0'=___rho_4_^post17, a33^0'=a33^post17, a55^0'=a55^post17, a88^0'=a88^post17, curtime^0'=curtime^post17, got_sighup^0'=___rho_2_^post17, last_copy_time^0'=last_copy_time^post17, ret_time1010^0'=ret_time1010^post17, ret_time77^0'=ret_time77^post17, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post17, tmp2^0'=tmp2^post17, tmp66^0'=tmp66^post17, tmp99^0'=tmp99^post17, tt1^0'=tt1^post17, wakend^0'=1, (0 == 0 /\ -___rho_1_^post17+___rho_1_^0 == 0 /\ -___rho_2_^post17+___rho_2_^0 == 0 /\ -a55^post17+a55^0 == 0 /\ -got_sighup^post17+got_sighup^0 == 0 /\ a88^0-a88^post17 == 0 /\ -tmp2^post17+tmp2^0 == 0 /\ ret_xlogarchivingactive44^0-ret_xlogarchivingactive44^post17 == 0 /\ -tt1^post17+tt1^0 == 0 /\ -ret_time77^post17+ret_time77^0 == 0 /\ -ret_time1010^post17+ret_time1010^0 == 0 /\ ___rho_4_^0-___rho_4_^post17 == 0 /\ -1+wakend^1 == 0 /\ -tmp66^post17+tmp66^0 == 0 /\ -wakend^post17+wakend^0 == 0 /\ tmp99^0-tmp99^post17 == 0 /\ -last_copy_time^post17+last_copy_time^0 == 0 /\ curtime^0-curtime^post17 == 0 /\ a33^0-a33^post17 == 0), cost: 1 New rule: l12 -> l0 : ___rho_1_^0'=___rho_1_^post16, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^0, a33^0'=a33^0, a55^0'=a55^0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=___rho_2_^0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=ret_time1010^0, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^0, tmp99^0'=tmp99^0, tt1^0'=tt1^0, wakend^0'=1, 0 == 0, cost: 1 propagated equality ___rho_1_^post17 = ___rho_1_^0 propagated equality ___rho_2_^post17 = ___rho_2_^0 propagated equality a55^post17 = a55^0 propagated equality got_sighup^post17 = got_sighup^0 propagated equality a88^post17 = a88^0 propagated equality tmp2^post17 = tmp2^0 propagated equality ret_xlogarchivingactive44^post17 = ret_xlogarchivingactive44^0 propagated equality tt1^post17 = tt1^0 propagated equality ret_time77^post17 = ret_time77^0 propagated equality ret_time1010^post17 = ret_time1010^0 propagated equality ___rho_4_^post17 = ___rho_4_^0 propagated equality wakend^1 = 1 propagated equality tmp66^post17 = tmp66^0 propagated equality wakend^post17 = wakend^0 propagated equality tmp99^post17 = tmp99^0 propagated equality last_copy_time^post17 = last_copy_time^0 propagated equality curtime^post17 = curtime^0 propagated equality a33^post17 = a33^0 Simplified Guard Original rule: l12 -> l0 : ___rho_1_^0'=___rho_1_^post16, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^0, a33^0'=a33^0, a55^0'=a55^0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=___rho_2_^0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=ret_time1010^0, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^0, tmp99^0'=tmp99^0, tt1^0'=tt1^0, wakend^0'=1, 0 == 0, cost: 1 New rule: l12 -> l0 : ___rho_1_^0'=___rho_1_^post16, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^0, a33^0'=a33^0, a55^0'=a55^0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=___rho_2_^0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=ret_time1010^0, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^0, tmp99^0'=tmp99^0, tt1^0'=tt1^0, wakend^0'=1, T, cost: 1 Removed Trivial Updates Original rule: l12 -> l0 : ___rho_1_^0'=___rho_1_^post16, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^0, a33^0'=a33^0, a55^0'=a55^0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=___rho_2_^0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=ret_time1010^0, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^0, tmp99^0'=tmp99^0, tt1^0'=tt1^0, wakend^0'=1, T, cost: 1 New rule: l12 -> l0 : ___rho_1_^0'=___rho_1_^post16, got_sighup^0'=___rho_2_^0, wakend^0'=1, T, cost: 1 Propagated Equalities Original rule: l6 -> l6 : ___rho_1_^0'=___rho_1_^post13, ___rho_2_^0'=___rho_2_^post13, ___rho_4_^0'=___rho_4_^post13, a33^0'=a33^post13, a55^0'=a55^post13, a88^0'=a88^post13, curtime^0'=curtime^post13, got_sighup^0'=got_sighup^post13, last_copy_time^0'=last_copy_time^post13, ret_time1010^0'=ret_time1010^post13, ret_time77^0'=ret_time77^post13, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post13, tmp2^0'=tmp2^post13, tmp66^0'=tmp66^post13, tmp99^0'=tmp99^post13, tt1^0'=tt1^post13, wakend^0'=wakend^post13, (-ret_time77^post13+ret_time77^post12 == 0 /\ tmp99^0-tmp99^post12 == 0 /\ -last_copy_time^post12+last_copy_time^0 == 0 /\ -tmp66^post12+tmp66^0 == 0 /\ tmp2^0-tmp2^post12 == 0 /\ wakend^0-wakend^post12 == 0 /\ curtime^post12-curtime^post13 == 0 /\ a55^0-a55^post12 == 0 /\ tmp66^post12-tmp66^post13 == 0 /\ -got_sighup^post13+got_sighup^post12 == 0 /\ -tt1^post13+tt1^post12 == 0 /\ got_sighup^0-got_sighup^post12 == 0 /\ -a55^post13+a55^post12 == 0 /\ ret_time77^0-ret_time77^post12 == 0 /\ -ret_time1010^post12+ret_time1010^0 == 0 /\ a88^0-a88^post12 == 0 /\ -curtime^post12+curtime^0 == 0 /\ ret_time1010^post12-ret_time1010^post13 == 0 /\ tmp2^post12-tmp2^post13 == 0 /\ a33^post12-a33^post13 == 0 /\ -tmp99^post13+tmp99^post12 == 0 /\ -wakend^post13+wakend^post12 == 0 /\ -ret_xlogarchivingactive44^post12+ret_xlogarchivingactive44^0 == 0 /\ -___rho_1_^post12+___rho_1_^0 == 0 /\ ___rho_4_^post12-___rho_4_^post13 == 0 /\ -tt1^post12+tt1^0 == 0 /\ -a33^post12+a33^0 == 0 /\ ___rho_4_^0-___rho_4_^post12 == 0 /\ ret_xlogarchivingactive44^post12-ret_xlogarchivingactive44^post13 == 0 /\ -___rho_2_^post13+___rho_2_^post12 == 0 /\ ___rho_2_^0-___rho_2_^post12 == 0 /\ last_copy_time^post12-last_copy_time^post13 == 0 /\ ___rho_1_^post12-___rho_1_^post13 == 0 /\ a88^post12-a88^post13 == 0), cost: 1 New rule: l6 -> l6 : ___rho_1_^0'=___rho_1_^post12, ___rho_2_^0'=___rho_2_^post12, ___rho_4_^0'=___rho_4_^post12, a33^0'=a33^post12, a55^0'=a55^post12, a88^0'=a88^post12, curtime^0'=curtime^post12, got_sighup^0'=got_sighup^post12, last_copy_time^0'=last_copy_time^post12, ret_time1010^0'=ret_time1010^post12, ret_time77^0'=ret_time77^post12, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post12, tmp2^0'=tmp2^post12, tmp66^0'=tmp66^post12, tmp99^0'=tmp99^post12, tt1^0'=tt1^post12, wakend^0'=wakend^post12, (0 == 0 /\ tmp99^0-tmp99^post12 == 0 /\ -last_copy_time^post12+last_copy_time^0 == 0 /\ -tmp66^post12+tmp66^0 == 0 /\ tmp2^0-tmp2^post12 == 0 /\ wakend^0-wakend^post12 == 0 /\ a55^0-a55^post12 == 0 /\ got_sighup^0-got_sighup^post12 == 0 /\ ret_time77^0-ret_time77^post12 == 0 /\ -ret_time1010^post12+ret_time1010^0 == 0 /\ a88^0-a88^post12 == 0 /\ -curtime^post12+curtime^0 == 0 /\ -ret_xlogarchivingactive44^post12+ret_xlogarchivingactive44^0 == 0 /\ -___rho_1_^post12+___rho_1_^0 == 0 /\ -tt1^post12+tt1^0 == 0 /\ -a33^post12+a33^0 == 0 /\ ___rho_4_^0-___rho_4_^post12 == 0 /\ ___rho_2_^0-___rho_2_^post12 == 0), cost: 1 propagated equality ret_time77^post13 = ret_time77^post12 propagated equality curtime^post13 = curtime^post12 propagated equality tmp66^post13 = tmp66^post12 propagated equality got_sighup^post13 = got_sighup^post12 propagated equality tt1^post13 = tt1^post12 propagated equality a55^post13 = a55^post12 propagated equality ret_time1010^post13 = ret_time1010^post12 propagated equality tmp2^post13 = tmp2^post12 propagated equality a33^post13 = a33^post12 propagated equality tmp99^post13 = tmp99^post12 propagated equality wakend^post13 = wakend^post12 propagated equality ___rho_4_^post13 = ___rho_4_^post12 propagated equality ret_xlogarchivingactive44^post13 = ret_xlogarchivingactive44^post12 propagated equality ___rho_2_^post13 = ___rho_2_^post12 propagated equality last_copy_time^post13 = last_copy_time^post12 propagated equality ___rho_1_^post13 = ___rho_1_^post12 propagated equality a88^post13 = a88^post12 Propagated Equalities Original rule: l6 -> l6 : ___rho_1_^0'=___rho_1_^post12, ___rho_2_^0'=___rho_2_^post12, ___rho_4_^0'=___rho_4_^post12, a33^0'=a33^post12, a55^0'=a55^post12, a88^0'=a88^post12, curtime^0'=curtime^post12, got_sighup^0'=got_sighup^post12, last_copy_time^0'=last_copy_time^post12, ret_time1010^0'=ret_time1010^post12, ret_time77^0'=ret_time77^post12, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^post12, tmp2^0'=tmp2^post12, tmp66^0'=tmp66^post12, tmp99^0'=tmp99^post12, tt1^0'=tt1^post12, wakend^0'=wakend^post12, (0 == 0 /\ tmp99^0-tmp99^post12 == 0 /\ -last_copy_time^post12+last_copy_time^0 == 0 /\ -tmp66^post12+tmp66^0 == 0 /\ tmp2^0-tmp2^post12 == 0 /\ wakend^0-wakend^post12 == 0 /\ a55^0-a55^post12 == 0 /\ got_sighup^0-got_sighup^post12 == 0 /\ ret_time77^0-ret_time77^post12 == 0 /\ -ret_time1010^post12+ret_time1010^0 == 0 /\ a88^0-a88^post12 == 0 /\ -curtime^post12+curtime^0 == 0 /\ -ret_xlogarchivingactive44^post12+ret_xlogarchivingactive44^0 == 0 /\ -___rho_1_^post12+___rho_1_^0 == 0 /\ -tt1^post12+tt1^0 == 0 /\ -a33^post12+a33^0 == 0 /\ ___rho_4_^0-___rho_4_^post12 == 0 /\ ___rho_2_^0-___rho_2_^post12 == 0), cost: 1 New rule: l6 -> l6 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^0, a33^0'=a33^0, a55^0'=a55^0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=ret_time1010^0, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^0, tmp99^0'=tmp99^0, tt1^0'=tt1^0, wakend^0'=wakend^0, 0 == 0, cost: 1 propagated equality tmp99^post12 = tmp99^0 propagated equality last_copy_time^post12 = last_copy_time^0 propagated equality tmp66^post12 = tmp66^0 propagated equality tmp2^post12 = tmp2^0 propagated equality wakend^post12 = wakend^0 propagated equality a55^post12 = a55^0 propagated equality got_sighup^post12 = got_sighup^0 propagated equality ret_time77^post12 = ret_time77^0 propagated equality ret_time1010^post12 = ret_time1010^0 propagated equality a88^post12 = a88^0 propagated equality curtime^post12 = curtime^0 propagated equality ret_xlogarchivingactive44^post12 = ret_xlogarchivingactive44^0 propagated equality ___rho_1_^post12 = ___rho_1_^0 propagated equality tt1^post12 = tt1^0 propagated equality a33^post12 = a33^0 propagated equality ___rho_4_^post12 = ___rho_4_^0 propagated equality ___rho_2_^post12 = ___rho_2_^0 Simplified Guard Original rule: l6 -> l6 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^0, a33^0'=a33^0, a55^0'=a55^0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=ret_time1010^0, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^0, tmp99^0'=tmp99^0, tt1^0'=tt1^0, wakend^0'=wakend^0, 0 == 0, cost: 1 New rule: l6 -> l6 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^0, a33^0'=a33^0, a55^0'=a55^0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=ret_time1010^0, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^0, tmp99^0'=tmp99^0, tt1^0'=tt1^0, wakend^0'=wakend^0, T, cost: 1 Removed Trivial Updates Original rule: l6 -> l6 : ___rho_1_^0'=___rho_1_^0, ___rho_2_^0'=___rho_2_^0, ___rho_4_^0'=___rho_4_^0, a33^0'=a33^0, a55^0'=a55^0, a88^0'=a88^0, curtime^0'=curtime^0, got_sighup^0'=got_sighup^0, last_copy_time^0'=last_copy_time^0, ret_time1010^0'=ret_time1010^0, ret_time77^0'=ret_time77^0, ret_xlogarchivingactive44^0'=ret_xlogarchivingactive44^0, tmp2^0'=tmp2^0, tmp66^0'=tmp66^0, tmp99^0'=tmp99^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-last_copy_time^0+curtime^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-last_copy_time^0+curtime^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-last_copy_time^0+curtime^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-last_copy_time^0+curtime^0 <= 0)], 23[T], 22[T], 33[T] Blocked [{}, {}, {28[T]}, {26[T]}, {}, {}, {}, {}, {}] Nonterm Start location: l12 Program variables: ___rho_1_^0 ___rho_2_^0 ___rho_4_^0 a33^0 a55^0 a88^0 curtime^0 got_sighup^0 last_copy_time^0 ret_time1010^0 ret_time77^0 ret_xlogarchivingactive44^0 tmp2^0 tmp66^0 tmp99^0 tt1^0 wakend^0 19: l0 -> l1 : got_sighup^0 <= 0, cost: 1 20: l0 -> l2 : ___rho_2_^0'=tt1^post2, a33^0'=1, got_sighup^0'=0, ret_xlogarchivingactive44^0'=tt1^post2, tmp2^0'=tt1^post2, tt1^0'=tt1^post2, 1-got_sighup^0 <= 0, cost: 1 28: l1 -> l9 : wakend^0 <= 0, cost: 1 29: l1 -> l9 : a55^0'=0, last_copy_time^0'=tmp66^post11, ret_time77^0'=tmp66^post11, tmp66^0'=tmp66^post11, 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_4_^0'=___rho_4_^post5, T, cost: 1 24: l8 -> l7 : -999-last_copy_time^0+curtime^0 <= 0, cost: 1 25: l8 -> l7 : wakend^0'=1, 1000+last_copy_time^0-curtime^0 <= 0, cost: 1 26: l9 -> l7 : 1-wakend^0 <= 0, cost: 1 27: l9 -> l8 : a88^0'=0, curtime^0'=tmp99^post9, ret_time1010^0'=tmp99^post9, tmp99^0'=tmp99^post9, wakend^0 <= 0, cost: 1 32: l12 -> l0 : ___rho_1_^0'=___rho_1_^post16, got_sighup^0'=___rho_2_^0, 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-last_copy_time^0+curtime^0 <= 0)], 23[T], 22[T], 34[-1+n >= 0] Blocked [{}, {}, {28[T]}, {26[T]}, {}, {}, {}, {}, {34[T]}] Refute Counterexample [ ___rho_1_^0=0 ___rho_2_^0=0 ___rho_4_^0=0 a33^0=0 a55^0=0 a88^0=0 curtime^0=0 got_sighup^0=0 last_copy_time^0=0 ret_time1010^0=0 ret_time77^0=0 ret_xlogarchivingactive44^0=0 tmp2^0=0 tmp66^0=0 tmp99^0=0 tt1^0=0 wakend^0=1 ] 32 [ ___rho_1_^0=0 ___rho_2_^0=0 ___rho_4_^0=0 a33^0=0 a55^0=0 a88^0=0 curtime^0=0 got_sighup^0=0 last_copy_time^0=0 ret_time1010^0=0 ret_time77^0=0 ret_xlogarchivingactive44^0=0 tmp2^0=0 tmp66^0=0 tmp99^0=0 tt1^0=0 wakend^0=1 ] 19 [ ___rho_1_^0=0 ___rho_2_^0=0 ___rho_4_^0=0 a33^0=0 a55^0=0 a88^0=0 curtime^0=0 got_sighup^0=0 last_copy_time^0=0 ret_time1010^0=0 ret_time77^0=0 ret_xlogarchivingactive44^0=0 tmp2^0=0 tmp66^0=0 tmp99^0=0 tt1^0=0 wakend^0=0 ] 29 [ ___rho_1_^0=0 ___rho_2_^0=0 ___rho_4_^0=0 a33^0=0 a55^0=0 a88^0=0 curtime^0=0 got_sighup^0=0 last_copy_time^0=0 ret_time1010^0=0 ret_time77^0=0 ret_xlogarchivingactive44^0=0 tmp2^0=0 tmp66^0=0 tmp99^0=0 tt1^0=0 wakend^0=0 ] 27 [ ___rho_1_^0=0 ___rho_2_^0=0 ___rho_4_^0=0 a33^0=0 a55^0=0 a88^0=0 curtime^0=0 got_sighup^0=0 last_copy_time^0=0 ret_time1010^0=0 ret_time77^0=0 ret_xlogarchivingactive44^0=0 tmp2^0=0 tmp66^0=0 tmp99^0=0 tt1^0=0 wakend^0=0 ] 24 [ ___rho_1_^0=0 ___rho_2_^0=0 ___rho_4_^0=0 a33^0=0 a55^0=0 a88^0=0 curtime^0=0 got_sighup^0=0 last_copy_time^0=0 ret_time1010^0=0 ret_time77^0=0 ret_xlogarchivingactive44^0=0 tmp2^0=0 tmp66^0=0 tmp99^0=0 tt1^0=0 wakend^0=0 ] 23 [ ___rho_1_^0=0 ___rho_2_^0=0 ___rho_4_^0=0 a33^0=0 a55^0=0 a88^0=0 curtime^0=0 got_sighup^0=0 last_copy_time^0=0 ret_time1010^0=0 ret_time77^0=0 ret_xlogarchivingactive44^0=0 tmp2^0=0 tmp66^0=0 tmp99^0=0 tt1^0=0 wakend^0=0 ] 22 [ ___rho_1_^0=___rho_1_^0 ___rho_2_^0=0 ___rho_4_^0=0 a33^0=0 a55^0=0 a88^0=0 curtime^0=0 got_sighup^0=got_sighup^0 last_copy_time^0=0 ret_time1010^0=0 ret_time77^0=0 ret_xlogarchivingactive44^0=0 tmp2^0=0 tmp66^0=0 tmp99^0=0 tt1^0=0 wakend^0=wakend^0 ] 34 NO Build SHA: a05f16bf13df659c382799650051f91bf6828c7b