NO Initial ITS Start location: l12 0: l0 -> l1 : a33^0'=a33^post0, ret_time88^0'=ret_time88^post0, __rho_1_^0'=__rho_1_^post0, tt1^0'=tt1^post0, last_copy_time^0'=last_copy_time^post0, a77^0'=a77^post0, __rho_3_^0'=__rho_3_^post0, ret_time66^0'=ret_time66^post0, __const_1000^0'=__const_1000^post0, got_SIGHUP^0'=got_SIGHUP^post0, a55^0'=a55^post0, tmp2^0'=tmp2^post0, __rho_2_^0'=__rho_2_^post0, wakend^0'=wakend^post0, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post0, curtime^0'=curtime^post0, (-got_SIGHUP^post0+got_SIGHUP^0 == 0 /\ __rho_3_^0-__rho_3_^post0 == 0 /\ -a77^post0+a77^0 == 0 /\ tt1^0-tt1^post0 == 0 /\ -__const_1000^post0+__const_1000^0 == 0 /\ a33^0-a33^post0 == 0 /\ a55^0-a55^post0 == 0 /\ last_copy_time^0-last_copy_time^post0 == 0 /\ -wakend^post0+wakend^0 == 0 /\ got_SIGHUP^0 <= 0 /\ __rho_1_^0-__rho_1_^post0 == 0 /\ ret_time66^0-ret_time66^post0 == 0 /\ -ret_time88^post0+ret_time88^0 == 0 /\ -tmp2^post0+tmp2^0 == 0 /\ -curtime^post0+curtime^0 == 0 /\ -__rho_2_^post0+__rho_2_^0 == 0 /\ -ret_XLogArchivingActive44^post0+ret_XLogArchivingActive44^0 == 0), cost: 1 1: l0 -> l2 : a33^0'=a33^post1, ret_time88^0'=ret_time88^post1, __rho_1_^0'=__rho_1_^post1, tt1^0'=tt1^post1, last_copy_time^0'=last_copy_time^post1, a77^0'=a77^post1, __rho_3_^0'=__rho_3_^post1, ret_time66^0'=ret_time66^post1, __const_1000^0'=__const_1000^post1, got_SIGHUP^0'=got_SIGHUP^post1, a55^0'=a55^post1, tmp2^0'=tmp2^post1, __rho_2_^0'=__rho_2_^post1, wakend^0'=wakend^post1, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, curtime^0'=curtime^post1, (0 == 0 /\ ret_time88^0-ret_time88^post1 == 0 /\ -curtime^post1+curtime^0 == 0 /\ -tmp2^post1+tt1^post1 == 0 /\ -__const_1000^post1+__const_1000^0 == 0 /\ -a77^post1+a77^0 == 0 /\ -wakend^post1+wakend^0 == 0 /\ __rho_3_^0-__rho_3_^post1 == 0 /\ got_SIGHUP^post1 == 0 /\ a55^0-a55^post1 == 0 /\ -__rho_1_^post1+ret_XLogArchivingActive44^post1 == 0 /\ -last_copy_time^post1+last_copy_time^0 == 0 /\ ret_time66^0-ret_time66^post1 == 0 /\ -__rho_2_^post1+__rho_2_^0 == 0 /\ 1-got_SIGHUP^0 <= 0 /\ -1+a33^post1 == 0 /\ tmp2^post1-ret_XLogArchivingActive44^post1 == 0), cost: 1 9: l1 -> l9 : a33^0'=a33^post9, ret_time88^0'=ret_time88^post9, __rho_1_^0'=__rho_1_^post9, tt1^0'=tt1^post9, last_copy_time^0'=last_copy_time^post9, a77^0'=a77^post9, __rho_3_^0'=__rho_3_^post9, ret_time66^0'=ret_time66^post9, __const_1000^0'=__const_1000^post9, got_SIGHUP^0'=got_SIGHUP^post9, a55^0'=a55^post9, tmp2^0'=tmp2^post9, __rho_2_^0'=__rho_2_^post9, wakend^0'=wakend^post9, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post9, curtime^0'=curtime^post9, (-tt1^post9+tt1^0 == 0 /\ -__rho_3_^post9+__rho_3_^0 == 0 /\ ret_time88^0-ret_time88^post9 == 0 /\ __rho_2_^0-__rho_2_^post9 == 0 /\ a77^0-a77^post9 == 0 /\ last_copy_time^0-last_copy_time^post9 == 0 /\ __rho_1_^0-__rho_1_^post9 == 0 /\ -wakend^post9+wakend^0 == 0 /\ -a55^post9+a55^0 == 0 /\ -ret_time66^post9+ret_time66^0 == 0 /\ a33^0-a33^post9 == 0 /\ -curtime^post9+curtime^0 == 0 /\ -ret_XLogArchivingActive44^post9+ret_XLogArchivingActive44^0 == 0 /\ -tmp2^post9+tmp2^0 == 0 /\ wakend^0 <= 0 /\ __const_1000^0-__const_1000^post9 == 0 /\ -got_SIGHUP^post9+got_SIGHUP^0 == 0), cost: 1 10: l1 -> l9 : a33^0'=a33^post10, ret_time88^0'=ret_time88^post10, __rho_1_^0'=__rho_1_^post10, tt1^0'=tt1^post10, last_copy_time^0'=last_copy_time^post10, a77^0'=a77^post10, __rho_3_^0'=__rho_3_^post10, ret_time66^0'=ret_time66^post10, __const_1000^0'=__const_1000^post10, got_SIGHUP^0'=got_SIGHUP^post10, a55^0'=a55^post10, tmp2^0'=tmp2^post10, __rho_2_^0'=__rho_2_^post10, wakend^0'=wakend^post10, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post10, curtime^0'=curtime^post10, (0 == 0 /\ ret_time88^0-ret_time88^post10 == 0 /\ -curtime^post10+curtime^0 == 0 /\ wakend^post10 == 0 /\ a55^post10 == 0 /\ a77^0-a77^post10 == 0 /\ 1-wakend^0 <= 0 /\ -__rho_2_^post10+__rho_2_^0 == 0 /\ got_SIGHUP^0-got_SIGHUP^post10 == 0 /\ -tmp2^post10+tmp2^0 == 0 /\ __rho_1_^0-__rho_1_^post10 == 0 /\ -ret_XLogArchivingActive44^post10+ret_XLogArchivingActive44^0 == 0 /\ ret_time66^post10-__rho_3_^post10 == 0 /\ -ret_time66^post10+last_copy_time^post10 == 0 /\ a33^0-a33^post10 == 0 /\ tt1^0-tt1^post10 == 0 /\ -__const_1000^post10+__const_1000^0 == 0), cost: 1 13: l2 -> l1 : a33^0'=a33^post13, ret_time88^0'=ret_time88^post13, __rho_1_^0'=__rho_1_^post13, tt1^0'=tt1^post13, last_copy_time^0'=last_copy_time^post13, a77^0'=a77^post13, __rho_3_^0'=__rho_3_^post13, ret_time66^0'=ret_time66^post13, __const_1000^0'=__const_1000^post13, got_SIGHUP^0'=got_SIGHUP^post13, a55^0'=a55^post13, tmp2^0'=tmp2^post13, __rho_2_^0'=__rho_2_^post13, wakend^0'=wakend^post13, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post13, curtime^0'=curtime^post13, (__rho_2_^0-__rho_2_^post13 == 0 /\ -wakend^post13+wakend^0 == 0 /\ -ret_time66^post13+ret_time66^0 == 0 /\ -ret_XLogArchivingActive44^post13+ret_XLogArchivingActive44^0 == 0 /\ got_SIGHUP^0-got_SIGHUP^post13 == 0 /\ -a55^post13+a55^0 == 0 /\ __rho_1_^0-__rho_1_^post13 == 0 /\ a33^0-a33^post13 == 0 /\ a77^0-a77^post13 == 0 /\ -tt1^post13+tt1^0 == 0 /\ 1-tt1^0 <= 0 /\ __const_1000^0-__const_1000^post13 == 0 /\ ret_time88^0-ret_time88^post13 == 0 /\ -tmp2^post13+tmp2^0 == 0 /\ -curtime^post13+curtime^0 == 0 /\ last_copy_time^0-last_copy_time^post13 == 0 /\ __rho_3_^0-__rho_3_^post13 == 0), cost: 1 14: l2 -> l5 : a33^0'=a33^post14, ret_time88^0'=ret_time88^post14, __rho_1_^0'=__rho_1_^post14, tt1^0'=tt1^post14, last_copy_time^0'=last_copy_time^post14, a77^0'=a77^post14, __rho_3_^0'=__rho_3_^post14, ret_time66^0'=ret_time66^post14, __const_1000^0'=__const_1000^post14, got_SIGHUP^0'=got_SIGHUP^post14, a55^0'=a55^post14, tmp2^0'=tmp2^post14, __rho_2_^0'=__rho_2_^post14, wakend^0'=wakend^post14, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post14, curtime^0'=curtime^post14, (-last_copy_time^post14+last_copy_time^0 == 0 /\ __rho_1_^0-__rho_1_^post14 == 0 /\ tt1^0 <= 0 /\ wakend^0-wakend^post14 == 0 /\ ret_time88^0-ret_time88^post14 == 0 /\ -ret_time66^post14+ret_time66^0 == 0 /\ a33^0-a33^post14 == 0 /\ -__const_1000^post14+__const_1000^0 == 0 /\ got_SIGHUP^0-got_SIGHUP^post14 == 0 /\ -curtime^post14+curtime^0 == 0 /\ -a55^post14+a55^0 == 0 /\ __rho_3_^0-__rho_3_^post14 == 0 /\ -__rho_2_^post14+__rho_2_^0 == 0 /\ tt1^0-tt1^post14 == 0 /\ a77^0-a77^post14 == 0 /\ -tmp2^post14+tmp2^0 == 0 /\ -ret_XLogArchivingActive44^post14+ret_XLogArchivingActive44^0 == 0), cost: 1 2: l3 -> l4 : a33^0'=a33^post2, ret_time88^0'=ret_time88^post2, __rho_1_^0'=__rho_1_^post2, tt1^0'=tt1^post2, last_copy_time^0'=last_copy_time^post2, a77^0'=a77^post2, __rho_3_^0'=__rho_3_^post2, ret_time66^0'=ret_time66^post2, __const_1000^0'=__const_1000^post2, got_SIGHUP^0'=got_SIGHUP^post2, a55^0'=a55^post2, tmp2^0'=tmp2^post2, __rho_2_^0'=__rho_2_^post2, wakend^0'=wakend^post2, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post2, curtime^0'=curtime^post2, (-__rho_2_^post2+__rho_2_^0 == 0 /\ -wakend^post2+wakend^0 == 0 /\ ret_time88^0-ret_time88^post2 == 0 /\ __rho_1_^0-__rho_1_^post2 == 0 /\ tt1^0-tt1^post2 == 0 /\ -curtime^post2+curtime^0 == 0 /\ -ret_XLogArchivingActive44^post2+ret_XLogArchivingActive44^0 == 0 /\ -got_SIGHUP^post2+got_SIGHUP^0 == 0 /\ a55^0-a55^post2 == 0 /\ -__const_1000^post2+__const_1000^0 == 0 /\ -a77^post2+a77^0 == 0 /\ -tmp2^post2+tmp2^0 == 0 /\ last_copy_time^0-last_copy_time^post2 == 0 /\ __rho_3_^0-__rho_3_^post2 == 0 /\ ret_time66^0-ret_time66^post2 == 0 /\ a33^0-a33^post2 == 0), cost: 1 3: l5 -> l6 : a33^0'=a33^post3, ret_time88^0'=ret_time88^post3, __rho_1_^0'=__rho_1_^post3, tt1^0'=tt1^post3, last_copy_time^0'=last_copy_time^post3, a77^0'=a77^post3, __rho_3_^0'=__rho_3_^post3, ret_time66^0'=ret_time66^post3, __const_1000^0'=__const_1000^post3, got_SIGHUP^0'=got_SIGHUP^post3, a55^0'=a55^post3, tmp2^0'=tmp2^post3, __rho_2_^0'=__rho_2_^post3, wakend^0'=wakend^post3, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post3, curtime^0'=curtime^post3, (-__rho_2_^post3+__rho_2_^0 == 0 /\ __rho_3_^0-__rho_3_^post3 == 0 /\ -got_SIGHUP^post3+got_SIGHUP^0 == 0 /\ -__const_1000^post3+__const_1000^0 == 0 /\ a33^0-a33^post3 == 0 /\ -ret_XLogArchivingActive44^post3+ret_XLogArchivingActive44^0 == 0 /\ tt1^0-tt1^post3 == 0 /\ -curtime^post3+curtime^0 == 0 /\ -tmp2^post3+tmp2^0 == 0 /\ a55^0-a55^post3 == 0 /\ last_copy_time^0-last_copy_time^post3 == 0 /\ ret_time88^0-ret_time88^post3 == 0 /\ __rho_1_^0-__rho_1_^post3 == 0 /\ ret_time66^0-ret_time66^post3 == 0 /\ -a77^post3+a77^0 == 0 /\ -wakend^post3+wakend^0 == 0), cost: 1 11: l6 -> l10 : a33^0'=a33^post11, ret_time88^0'=ret_time88^post11, __rho_1_^0'=__rho_1_^post11, tt1^0'=tt1^post11, last_copy_time^0'=last_copy_time^post11, a77^0'=a77^post11, __rho_3_^0'=__rho_3_^post11, ret_time66^0'=ret_time66^post11, __const_1000^0'=__const_1000^post11, got_SIGHUP^0'=got_SIGHUP^post11, a55^0'=a55^post11, tmp2^0'=tmp2^post11, __rho_2_^0'=__rho_2_^post11, wakend^0'=wakend^post11, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post11, curtime^0'=curtime^post11, (__rho_2_^0-__rho_2_^post11 == 0 /\ -ret_time66^post11+ret_time66^0 == 0 /\ got_SIGHUP^0-got_SIGHUP^post11 == 0 /\ __rho_1_^0-__rho_1_^post11 == 0 /\ -a55^post11+a55^0 == 0 /\ a77^0-a77^post11 == 0 /\ ret_time88^0-ret_time88^post11 == 0 /\ -tt1^post11+tt1^0 == 0 /\ __const_1000^0-__const_1000^post11 == 0 /\ -tmp2^post11+tmp2^0 == 0 /\ a33^0-a33^post11 == 0 /\ -curtime^post11+curtime^0 == 0 /\ -ret_XLogArchivingActive44^post11+ret_XLogArchivingActive44^0 == 0 /\ __rho_3_^0-__rho_3_^post11 == 0 /\ last_copy_time^0-last_copy_time^post11 == 0 /\ -wakend^post11+wakend^0 == 0), cost: 1 4: l7 -> l5 : a33^0'=a33^post4, ret_time88^0'=ret_time88^post4, __rho_1_^0'=__rho_1_^post4, tt1^0'=tt1^post4, last_copy_time^0'=last_copy_time^post4, a77^0'=a77^post4, __rho_3_^0'=__rho_3_^post4, ret_time66^0'=ret_time66^post4, __const_1000^0'=__const_1000^post4, got_SIGHUP^0'=got_SIGHUP^post4, a55^0'=a55^post4, tmp2^0'=tmp2^post4, __rho_2_^0'=__rho_2_^post4, wakend^0'=wakend^post4, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post4, curtime^0'=curtime^post4, (__const_1000^0-__const_1000^post4 == 0 /\ -__rho_2_^post4+__rho_2_^0 == 0 /\ -ret_XLogArchivingActive44^post4+ret_XLogArchivingActive44^0 == 0 /\ a33^0-a33^post4 == 0 /\ -got_SIGHUP^post4+got_SIGHUP^0 == 0 /\ last_copy_time^0-last_copy_time^post4 == 0 /\ ret_time88^0-ret_time88^post4 == 0 /\ -a55^post4+a55^0 == 0 /\ ret_time66^0-ret_time66^post4 == 0 /\ -__rho_1_^post4+__rho_1_^0 == 0 /\ -curtime^post4+curtime^0 == 0 /\ tmp2^0-tmp2^post4 == 0 /\ a77^0-a77^post4 == 0 /\ -__rho_3_^post4+__rho_3_^0 == 0 /\ -wakend^post4+wakend^0 == 0 /\ tt1^0-tt1^post4 == 0), cost: 1 5: l8 -> l7 : a33^0'=a33^post5, ret_time88^0'=ret_time88^post5, __rho_1_^0'=__rho_1_^post5, tt1^0'=tt1^post5, last_copy_time^0'=last_copy_time^post5, a77^0'=a77^post5, __rho_3_^0'=__rho_3_^post5, ret_time66^0'=ret_time66^post5, __const_1000^0'=__const_1000^post5, got_SIGHUP^0'=got_SIGHUP^post5, a55^0'=a55^post5, tmp2^0'=tmp2^post5, __rho_2_^0'=__rho_2_^post5, wakend^0'=wakend^post5, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post5, curtime^0'=curtime^post5, (1-last_copy_time^0-__const_1000^0+curtime^0 <= 0 /\ -got_SIGHUP^post5+got_SIGHUP^0 == 0 /\ a33^0-a33^post5 == 0 /\ last_copy_time^0-last_copy_time^post5 == 0 /\ -__rho_3_^post5+__rho_3_^0 == 0 /\ ret_time66^0-ret_time66^post5 == 0 /\ __const_1000^0-__const_1000^post5 == 0 /\ -__rho_1_^post5+__rho_1_^0 == 0 /\ -a55^post5+a55^0 == 0 /\ -wakend^post5+wakend^0 == 0 /\ -__rho_2_^post5+__rho_2_^0 == 0 /\ -ret_XLogArchivingActive44^post5+ret_XLogArchivingActive44^0 == 0 /\ tt1^0-tt1^post5 == 0 /\ -curtime^post5+curtime^0 == 0 /\ ret_time88^0-ret_time88^post5 == 0 /\ tmp2^0-tmp2^post5 == 0 /\ a77^0-a77^post5 == 0), cost: 1 6: l8 -> l7 : a33^0'=a33^post6, ret_time88^0'=ret_time88^post6, __rho_1_^0'=__rho_1_^post6, tt1^0'=tt1^post6, last_copy_time^0'=last_copy_time^post6, a77^0'=a77^post6, __rho_3_^0'=__rho_3_^post6, ret_time66^0'=ret_time66^post6, __const_1000^0'=__const_1000^post6, got_SIGHUP^0'=got_SIGHUP^post6, a55^0'=a55^post6, tmp2^0'=tmp2^post6, __rho_2_^0'=__rho_2_^post6, wakend^0'=wakend^post6, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post6, curtime^0'=curtime^post6, (a33^0-a33^post6 == 0 /\ -tmp2^post6+tmp2^0 == 0 /\ -curtime^post6+curtime^0 == 0 /\ last_copy_time^0+__const_1000^0-curtime^0 <= 0 /\ __rho_2_^0-__rho_2_^post6 == 0 /\ -tt1^post6+tt1^0 == 0 /\ -1+wakend^post6 == 0 /\ last_copy_time^0-last_copy_time^post6 == 0 /\ -__rho_3_^post6+__rho_3_^0 == 0 /\ ret_time88^0-ret_time88^post6 == 0 /\ a77^0-a77^post6 == 0 /\ -ret_XLogArchivingActive44^post6+ret_XLogArchivingActive44^0 == 0 /\ -got_SIGHUP^post6+got_SIGHUP^0 == 0 /\ __const_1000^0-__const_1000^post6 == 0 /\ -ret_time66^post6+ret_time66^0 == 0 /\ __rho_1_^0-__rho_1_^post6 == 0 /\ -a55^post6+a55^0 == 0), cost: 1 7: l9 -> l7 : a33^0'=a33^post7, ret_time88^0'=ret_time88^post7, __rho_1_^0'=__rho_1_^post7, tt1^0'=tt1^post7, last_copy_time^0'=last_copy_time^post7, a77^0'=a77^post7, __rho_3_^0'=__rho_3_^post7, ret_time66^0'=ret_time66^post7, __const_1000^0'=__const_1000^post7, got_SIGHUP^0'=got_SIGHUP^post7, a55^0'=a55^post7, tmp2^0'=tmp2^post7, __rho_2_^0'=__rho_2_^post7, wakend^0'=wakend^post7, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post7, curtime^0'=curtime^post7, (-wakend^post7+wakend^0 == 0 /\ __const_1000^0-__const_1000^post7 == 0 /\ tmp2^0-tmp2^post7 == 0 /\ -a55^post7+a55^0 == 0 /\ ret_time88^0-ret_time88^post7 == 0 /\ last_copy_time^0-last_copy_time^post7 == 0 /\ -curtime^post7+curtime^0 == 0 /\ 1-wakend^0 <= 0 /\ -ret_XLogArchivingActive44^post7+ret_XLogArchivingActive44^0 == 0 /\ -__rho_2_^post7+__rho_2_^0 == 0 /\ -got_SIGHUP^post7+got_SIGHUP^0 == 0 /\ ret_time66^0-ret_time66^post7 == 0 /\ -__rho_3_^post7+__rho_3_^0 == 0 /\ a77^0-a77^post7 == 0 /\ __rho_1_^0-__rho_1_^post7 == 0 /\ tt1^0-tt1^post7 == 0 /\ a33^0-a33^post7 == 0), cost: 1 8: l9 -> l8 : a33^0'=a33^post8, ret_time88^0'=ret_time88^post8, __rho_1_^0'=__rho_1_^post8, tt1^0'=tt1^post8, last_copy_time^0'=last_copy_time^post8, a77^0'=a77^post8, __rho_3_^0'=__rho_3_^post8, ret_time66^0'=ret_time66^post8, __const_1000^0'=__const_1000^post8, got_SIGHUP^0'=got_SIGHUP^post8, a55^0'=a55^post8, tmp2^0'=tmp2^post8, __rho_2_^0'=__rho_2_^post8, wakend^0'=wakend^post8, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post8, curtime^0'=curtime^post8, (0 == 0 /\ -ret_time88^post8+curtime^post8 == 0 /\ got_SIGHUP^0-got_SIGHUP^post8 == 0 /\ __rho_2_^0-__rho_2_^post8 == 0 /\ -ret_XLogArchivingActive44^post8+ret_XLogArchivingActive44^0 == 0 /\ -ret_time66^post8+ret_time66^0 == 0 /\ -a55^post8+a55^0 == 0 /\ __rho_1_^0-__rho_1_^post8 == 0 /\ last_copy_time^0-last_copy_time^post8 == 0 /\ a77^post8 == 0 /\ a33^0-a33^post8 == 0 /\ wakend^0 <= 0 /\ -wakend^post8+wakend^0 == 0 /\ -__rho_3_^post8+ret_time88^post8 == 0 /\ -tmp2^post8+tmp2^0 == 0 /\ -tt1^post8+tt1^0 == 0 /\ __const_1000^0-__const_1000^post8 == 0), cost: 1 12: l10 -> l6 : a33^0'=a33^post12, ret_time88^0'=ret_time88^post12, __rho_1_^0'=__rho_1_^post12, tt1^0'=tt1^post12, last_copy_time^0'=last_copy_time^post12, a77^0'=a77^post12, __rho_3_^0'=__rho_3_^post12, ret_time66^0'=ret_time66^post12, __const_1000^0'=__const_1000^post12, got_SIGHUP^0'=got_SIGHUP^post12, a55^0'=a55^post12, tmp2^0'=tmp2^post12, __rho_2_^0'=__rho_2_^post12, wakend^0'=wakend^post12, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post12, curtime^0'=curtime^post12, (-a55^post12+a55^0 == 0 /\ ret_time88^0-ret_time88^post12 == 0 /\ -curtime^post12+curtime^0 == 0 /\ -wakend^post12+wakend^0 == 0 /\ a77^0-a77^post12 == 0 /\ -__rho_2_^post12+__rho_2_^0 == 0 /\ got_SIGHUP^0-got_SIGHUP^post12 == 0 /\ __rho_1_^0-__rho_1_^post12 == 0 /\ -tmp2^post12+tmp2^0 == 0 /\ -ret_XLogArchivingActive44^post12+ret_XLogArchivingActive44^0 == 0 /\ a33^0-a33^post12 == 0 /\ tt1^0-tt1^post12 == 0 /\ -__const_1000^post12+__const_1000^0 == 0 /\ __rho_3_^0-__rho_3_^post12 == 0 /\ -ret_time66^post12+ret_time66^0 == 0 /\ last_copy_time^0-last_copy_time^post12 == 0), cost: 1 15: l11 -> l0 : a33^0'=a33^post15, ret_time88^0'=ret_time88^post15, __rho_1_^0'=__rho_1_^post15, tt1^0'=tt1^post15, last_copy_time^0'=last_copy_time^post15, a77^0'=a77^post15, __rho_3_^0'=__rho_3_^post15, ret_time66^0'=ret_time66^post15, __const_1000^0'=__const_1000^post15, got_SIGHUP^0'=got_SIGHUP^post15, a55^0'=a55^post15, tmp2^0'=tmp2^post15, __rho_2_^0'=__rho_2_^post15, wakend^0'=wakend^post15, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post15, curtime^0'=curtime^post15, (0 == 0 /\ got_SIGHUP^post15-__rho_2_^post15 == 0 /\ a33^0-a33^post15 == 0 /\ __rho_1_^0-__rho_1_^post15 == 0 /\ tt1^0-tt1^post15 == 0 /\ -1+wakend^post15 == 0 /\ a55^0-a55^post15 == 0 /\ -__const_1000^post15+__const_1000^0 == 0 /\ -1+wakend^10 == 0 /\ -a77^post15+a77^0 == 0 /\ -tmp2^post15+tmp2^0 == 0 /\ -ret_time88^post15+ret_time88^0 == 0 /\ __rho_3_^0-__rho_3_^post15 == 0 /\ last_copy_time^0-last_copy_time^post15 == 0 /\ ret_time66^0-ret_time66^post15 == 0 /\ -curtime^post15+curtime^0 == 0 /\ -ret_XLogArchivingActive44^post15+ret_XLogArchivingActive44^0 == 0), cost: 1 16: l12 -> l11 : a33^0'=a33^post16, ret_time88^0'=ret_time88^post16, __rho_1_^0'=__rho_1_^post16, tt1^0'=tt1^post16, last_copy_time^0'=last_copy_time^post16, a77^0'=a77^post16, __rho_3_^0'=__rho_3_^post16, ret_time66^0'=ret_time66^post16, __const_1000^0'=__const_1000^post16, got_SIGHUP^0'=got_SIGHUP^post16, a55^0'=a55^post16, tmp2^0'=tmp2^post16, __rho_2_^0'=__rho_2_^post16, wakend^0'=wakend^post16, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post16, curtime^0'=curtime^post16, (tt1^0-tt1^post16 == 0 /\ __rho_3_^0-__rho_3_^post16 == 0 /\ wakend^0-wakend^post16 == 0 /\ -__rho_2_^post16+__rho_2_^0 == 0 /\ -a77^post16+a77^0 == 0 /\ -curtime^post16+curtime^0 == 0 /\ a33^0-a33^post16 == 0 /\ -__const_1000^post16+__const_1000^0 == 0 /\ __rho_1_^0-__rho_1_^post16 == 0 /\ last_copy_time^0-last_copy_time^post16 == 0 /\ -tmp2^post16+tmp2^0 == 0 /\ a55^0-a55^post16 == 0 /\ ret_time66^0-ret_time66^post16 == 0 /\ -ret_XLogArchivingActive44^post16+ret_XLogArchivingActive44^0 == 0 /\ -got_SIGHUP^post16+got_SIGHUP^0 == 0 /\ ret_time88^0-ret_time88^post16 == 0), cost: 1 Removed unreachable rules and leafs Start location: l12 0: l0 -> l1 : a33^0'=a33^post0, ret_time88^0'=ret_time88^post0, __rho_1_^0'=__rho_1_^post0, tt1^0'=tt1^post0, last_copy_time^0'=last_copy_time^post0, a77^0'=a77^post0, __rho_3_^0'=__rho_3_^post0, ret_time66^0'=ret_time66^post0, __const_1000^0'=__const_1000^post0, got_SIGHUP^0'=got_SIGHUP^post0, a55^0'=a55^post0, tmp2^0'=tmp2^post0, __rho_2_^0'=__rho_2_^post0, wakend^0'=wakend^post0, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post0, curtime^0'=curtime^post0, (-got_SIGHUP^post0+got_SIGHUP^0 == 0 /\ __rho_3_^0-__rho_3_^post0 == 0 /\ -a77^post0+a77^0 == 0 /\ tt1^0-tt1^post0 == 0 /\ -__const_1000^post0+__const_1000^0 == 0 /\ a33^0-a33^post0 == 0 /\ a55^0-a55^post0 == 0 /\ last_copy_time^0-last_copy_time^post0 == 0 /\ -wakend^post0+wakend^0 == 0 /\ got_SIGHUP^0 <= 0 /\ __rho_1_^0-__rho_1_^post0 == 0 /\ ret_time66^0-ret_time66^post0 == 0 /\ -ret_time88^post0+ret_time88^0 == 0 /\ -tmp2^post0+tmp2^0 == 0 /\ -curtime^post0+curtime^0 == 0 /\ -__rho_2_^post0+__rho_2_^0 == 0 /\ -ret_XLogArchivingActive44^post0+ret_XLogArchivingActive44^0 == 0), cost: 1 1: l0 -> l2 : a33^0'=a33^post1, ret_time88^0'=ret_time88^post1, __rho_1_^0'=__rho_1_^post1, tt1^0'=tt1^post1, last_copy_time^0'=last_copy_time^post1, a77^0'=a77^post1, __rho_3_^0'=__rho_3_^post1, ret_time66^0'=ret_time66^post1, __const_1000^0'=__const_1000^post1, got_SIGHUP^0'=got_SIGHUP^post1, a55^0'=a55^post1, tmp2^0'=tmp2^post1, __rho_2_^0'=__rho_2_^post1, wakend^0'=wakend^post1, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, curtime^0'=curtime^post1, (0 == 0 /\ ret_time88^0-ret_time88^post1 == 0 /\ -curtime^post1+curtime^0 == 0 /\ -tmp2^post1+tt1^post1 == 0 /\ -__const_1000^post1+__const_1000^0 == 0 /\ -a77^post1+a77^0 == 0 /\ -wakend^post1+wakend^0 == 0 /\ __rho_3_^0-__rho_3_^post1 == 0 /\ got_SIGHUP^post1 == 0 /\ a55^0-a55^post1 == 0 /\ -__rho_1_^post1+ret_XLogArchivingActive44^post1 == 0 /\ -last_copy_time^post1+last_copy_time^0 == 0 /\ ret_time66^0-ret_time66^post1 == 0 /\ -__rho_2_^post1+__rho_2_^0 == 0 /\ 1-got_SIGHUP^0 <= 0 /\ -1+a33^post1 == 0 /\ tmp2^post1-ret_XLogArchivingActive44^post1 == 0), cost: 1 9: l1 -> l9 : a33^0'=a33^post9, ret_time88^0'=ret_time88^post9, __rho_1_^0'=__rho_1_^post9, tt1^0'=tt1^post9, last_copy_time^0'=last_copy_time^post9, a77^0'=a77^post9, __rho_3_^0'=__rho_3_^post9, ret_time66^0'=ret_time66^post9, __const_1000^0'=__const_1000^post9, got_SIGHUP^0'=got_SIGHUP^post9, a55^0'=a55^post9, tmp2^0'=tmp2^post9, __rho_2_^0'=__rho_2_^post9, wakend^0'=wakend^post9, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post9, curtime^0'=curtime^post9, (-tt1^post9+tt1^0 == 0 /\ -__rho_3_^post9+__rho_3_^0 == 0 /\ ret_time88^0-ret_time88^post9 == 0 /\ __rho_2_^0-__rho_2_^post9 == 0 /\ a77^0-a77^post9 == 0 /\ last_copy_time^0-last_copy_time^post9 == 0 /\ __rho_1_^0-__rho_1_^post9 == 0 /\ -wakend^post9+wakend^0 == 0 /\ -a55^post9+a55^0 == 0 /\ -ret_time66^post9+ret_time66^0 == 0 /\ a33^0-a33^post9 == 0 /\ -curtime^post9+curtime^0 == 0 /\ -ret_XLogArchivingActive44^post9+ret_XLogArchivingActive44^0 == 0 /\ -tmp2^post9+tmp2^0 == 0 /\ wakend^0 <= 0 /\ __const_1000^0-__const_1000^post9 == 0 /\ -got_SIGHUP^post9+got_SIGHUP^0 == 0), cost: 1 10: l1 -> l9 : a33^0'=a33^post10, ret_time88^0'=ret_time88^post10, __rho_1_^0'=__rho_1_^post10, tt1^0'=tt1^post10, last_copy_time^0'=last_copy_time^post10, a77^0'=a77^post10, __rho_3_^0'=__rho_3_^post10, ret_time66^0'=ret_time66^post10, __const_1000^0'=__const_1000^post10, got_SIGHUP^0'=got_SIGHUP^post10, a55^0'=a55^post10, tmp2^0'=tmp2^post10, __rho_2_^0'=__rho_2_^post10, wakend^0'=wakend^post10, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post10, curtime^0'=curtime^post10, (0 == 0 /\ ret_time88^0-ret_time88^post10 == 0 /\ -curtime^post10+curtime^0 == 0 /\ wakend^post10 == 0 /\ a55^post10 == 0 /\ a77^0-a77^post10 == 0 /\ 1-wakend^0 <= 0 /\ -__rho_2_^post10+__rho_2_^0 == 0 /\ got_SIGHUP^0-got_SIGHUP^post10 == 0 /\ -tmp2^post10+tmp2^0 == 0 /\ __rho_1_^0-__rho_1_^post10 == 0 /\ -ret_XLogArchivingActive44^post10+ret_XLogArchivingActive44^0 == 0 /\ ret_time66^post10-__rho_3_^post10 == 0 /\ -ret_time66^post10+last_copy_time^post10 == 0 /\ a33^0-a33^post10 == 0 /\ tt1^0-tt1^post10 == 0 /\ -__const_1000^post10+__const_1000^0 == 0), cost: 1 13: l2 -> l1 : a33^0'=a33^post13, ret_time88^0'=ret_time88^post13, __rho_1_^0'=__rho_1_^post13, tt1^0'=tt1^post13, last_copy_time^0'=last_copy_time^post13, a77^0'=a77^post13, __rho_3_^0'=__rho_3_^post13, ret_time66^0'=ret_time66^post13, __const_1000^0'=__const_1000^post13, got_SIGHUP^0'=got_SIGHUP^post13, a55^0'=a55^post13, tmp2^0'=tmp2^post13, __rho_2_^0'=__rho_2_^post13, wakend^0'=wakend^post13, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post13, curtime^0'=curtime^post13, (__rho_2_^0-__rho_2_^post13 == 0 /\ -wakend^post13+wakend^0 == 0 /\ -ret_time66^post13+ret_time66^0 == 0 /\ -ret_XLogArchivingActive44^post13+ret_XLogArchivingActive44^0 == 0 /\ got_SIGHUP^0-got_SIGHUP^post13 == 0 /\ -a55^post13+a55^0 == 0 /\ __rho_1_^0-__rho_1_^post13 == 0 /\ a33^0-a33^post13 == 0 /\ a77^0-a77^post13 == 0 /\ -tt1^post13+tt1^0 == 0 /\ 1-tt1^0 <= 0 /\ __const_1000^0-__const_1000^post13 == 0 /\ ret_time88^0-ret_time88^post13 == 0 /\ -tmp2^post13+tmp2^0 == 0 /\ -curtime^post13+curtime^0 == 0 /\ last_copy_time^0-last_copy_time^post13 == 0 /\ __rho_3_^0-__rho_3_^post13 == 0), cost: 1 14: l2 -> l5 : a33^0'=a33^post14, ret_time88^0'=ret_time88^post14, __rho_1_^0'=__rho_1_^post14, tt1^0'=tt1^post14, last_copy_time^0'=last_copy_time^post14, a77^0'=a77^post14, __rho_3_^0'=__rho_3_^post14, ret_time66^0'=ret_time66^post14, __const_1000^0'=__const_1000^post14, got_SIGHUP^0'=got_SIGHUP^post14, a55^0'=a55^post14, tmp2^0'=tmp2^post14, __rho_2_^0'=__rho_2_^post14, wakend^0'=wakend^post14, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post14, curtime^0'=curtime^post14, (-last_copy_time^post14+last_copy_time^0 == 0 /\ __rho_1_^0-__rho_1_^post14 == 0 /\ tt1^0 <= 0 /\ wakend^0-wakend^post14 == 0 /\ ret_time88^0-ret_time88^post14 == 0 /\ -ret_time66^post14+ret_time66^0 == 0 /\ a33^0-a33^post14 == 0 /\ -__const_1000^post14+__const_1000^0 == 0 /\ got_SIGHUP^0-got_SIGHUP^post14 == 0 /\ -curtime^post14+curtime^0 == 0 /\ -a55^post14+a55^0 == 0 /\ __rho_3_^0-__rho_3_^post14 == 0 /\ -__rho_2_^post14+__rho_2_^0 == 0 /\ tt1^0-tt1^post14 == 0 /\ a77^0-a77^post14 == 0 /\ -tmp2^post14+tmp2^0 == 0 /\ -ret_XLogArchivingActive44^post14+ret_XLogArchivingActive44^0 == 0), cost: 1 3: l5 -> l6 : a33^0'=a33^post3, ret_time88^0'=ret_time88^post3, __rho_1_^0'=__rho_1_^post3, tt1^0'=tt1^post3, last_copy_time^0'=last_copy_time^post3, a77^0'=a77^post3, __rho_3_^0'=__rho_3_^post3, ret_time66^0'=ret_time66^post3, __const_1000^0'=__const_1000^post3, got_SIGHUP^0'=got_SIGHUP^post3, a55^0'=a55^post3, tmp2^0'=tmp2^post3, __rho_2_^0'=__rho_2_^post3, wakend^0'=wakend^post3, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post3, curtime^0'=curtime^post3, (-__rho_2_^post3+__rho_2_^0 == 0 /\ __rho_3_^0-__rho_3_^post3 == 0 /\ -got_SIGHUP^post3+got_SIGHUP^0 == 0 /\ -__const_1000^post3+__const_1000^0 == 0 /\ a33^0-a33^post3 == 0 /\ -ret_XLogArchivingActive44^post3+ret_XLogArchivingActive44^0 == 0 /\ tt1^0-tt1^post3 == 0 /\ -curtime^post3+curtime^0 == 0 /\ -tmp2^post3+tmp2^0 == 0 /\ a55^0-a55^post3 == 0 /\ last_copy_time^0-last_copy_time^post3 == 0 /\ ret_time88^0-ret_time88^post3 == 0 /\ __rho_1_^0-__rho_1_^post3 == 0 /\ ret_time66^0-ret_time66^post3 == 0 /\ -a77^post3+a77^0 == 0 /\ -wakend^post3+wakend^0 == 0), cost: 1 11: l6 -> l10 : a33^0'=a33^post11, ret_time88^0'=ret_time88^post11, __rho_1_^0'=__rho_1_^post11, tt1^0'=tt1^post11, last_copy_time^0'=last_copy_time^post11, a77^0'=a77^post11, __rho_3_^0'=__rho_3_^post11, ret_time66^0'=ret_time66^post11, __const_1000^0'=__const_1000^post11, got_SIGHUP^0'=got_SIGHUP^post11, a55^0'=a55^post11, tmp2^0'=tmp2^post11, __rho_2_^0'=__rho_2_^post11, wakend^0'=wakend^post11, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post11, curtime^0'=curtime^post11, (__rho_2_^0-__rho_2_^post11 == 0 /\ -ret_time66^post11+ret_time66^0 == 0 /\ got_SIGHUP^0-got_SIGHUP^post11 == 0 /\ __rho_1_^0-__rho_1_^post11 == 0 /\ -a55^post11+a55^0 == 0 /\ a77^0-a77^post11 == 0 /\ ret_time88^0-ret_time88^post11 == 0 /\ -tt1^post11+tt1^0 == 0 /\ __const_1000^0-__const_1000^post11 == 0 /\ -tmp2^post11+tmp2^0 == 0 /\ a33^0-a33^post11 == 0 /\ -curtime^post11+curtime^0 == 0 /\ -ret_XLogArchivingActive44^post11+ret_XLogArchivingActive44^0 == 0 /\ __rho_3_^0-__rho_3_^post11 == 0 /\ last_copy_time^0-last_copy_time^post11 == 0 /\ -wakend^post11+wakend^0 == 0), cost: 1 4: l7 -> l5 : a33^0'=a33^post4, ret_time88^0'=ret_time88^post4, __rho_1_^0'=__rho_1_^post4, tt1^0'=tt1^post4, last_copy_time^0'=last_copy_time^post4, a77^0'=a77^post4, __rho_3_^0'=__rho_3_^post4, ret_time66^0'=ret_time66^post4, __const_1000^0'=__const_1000^post4, got_SIGHUP^0'=got_SIGHUP^post4, a55^0'=a55^post4, tmp2^0'=tmp2^post4, __rho_2_^0'=__rho_2_^post4, wakend^0'=wakend^post4, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post4, curtime^0'=curtime^post4, (__const_1000^0-__const_1000^post4 == 0 /\ -__rho_2_^post4+__rho_2_^0 == 0 /\ -ret_XLogArchivingActive44^post4+ret_XLogArchivingActive44^0 == 0 /\ a33^0-a33^post4 == 0 /\ -got_SIGHUP^post4+got_SIGHUP^0 == 0 /\ last_copy_time^0-last_copy_time^post4 == 0 /\ ret_time88^0-ret_time88^post4 == 0 /\ -a55^post4+a55^0 == 0 /\ ret_time66^0-ret_time66^post4 == 0 /\ -__rho_1_^post4+__rho_1_^0 == 0 /\ -curtime^post4+curtime^0 == 0 /\ tmp2^0-tmp2^post4 == 0 /\ a77^0-a77^post4 == 0 /\ -__rho_3_^post4+__rho_3_^0 == 0 /\ -wakend^post4+wakend^0 == 0 /\ tt1^0-tt1^post4 == 0), cost: 1 5: l8 -> l7 : a33^0'=a33^post5, ret_time88^0'=ret_time88^post5, __rho_1_^0'=__rho_1_^post5, tt1^0'=tt1^post5, last_copy_time^0'=last_copy_time^post5, a77^0'=a77^post5, __rho_3_^0'=__rho_3_^post5, ret_time66^0'=ret_time66^post5, __const_1000^0'=__const_1000^post5, got_SIGHUP^0'=got_SIGHUP^post5, a55^0'=a55^post5, tmp2^0'=tmp2^post5, __rho_2_^0'=__rho_2_^post5, wakend^0'=wakend^post5, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post5, curtime^0'=curtime^post5, (1-last_copy_time^0-__const_1000^0+curtime^0 <= 0 /\ -got_SIGHUP^post5+got_SIGHUP^0 == 0 /\ a33^0-a33^post5 == 0 /\ last_copy_time^0-last_copy_time^post5 == 0 /\ -__rho_3_^post5+__rho_3_^0 == 0 /\ ret_time66^0-ret_time66^post5 == 0 /\ __const_1000^0-__const_1000^post5 == 0 /\ -__rho_1_^post5+__rho_1_^0 == 0 /\ -a55^post5+a55^0 == 0 /\ -wakend^post5+wakend^0 == 0 /\ -__rho_2_^post5+__rho_2_^0 == 0 /\ -ret_XLogArchivingActive44^post5+ret_XLogArchivingActive44^0 == 0 /\ tt1^0-tt1^post5 == 0 /\ -curtime^post5+curtime^0 == 0 /\ ret_time88^0-ret_time88^post5 == 0 /\ tmp2^0-tmp2^post5 == 0 /\ a77^0-a77^post5 == 0), cost: 1 6: l8 -> l7 : a33^0'=a33^post6, ret_time88^0'=ret_time88^post6, __rho_1_^0'=__rho_1_^post6, tt1^0'=tt1^post6, last_copy_time^0'=last_copy_time^post6, a77^0'=a77^post6, __rho_3_^0'=__rho_3_^post6, ret_time66^0'=ret_time66^post6, __const_1000^0'=__const_1000^post6, got_SIGHUP^0'=got_SIGHUP^post6, a55^0'=a55^post6, tmp2^0'=tmp2^post6, __rho_2_^0'=__rho_2_^post6, wakend^0'=wakend^post6, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post6, curtime^0'=curtime^post6, (a33^0-a33^post6 == 0 /\ -tmp2^post6+tmp2^0 == 0 /\ -curtime^post6+curtime^0 == 0 /\ last_copy_time^0+__const_1000^0-curtime^0 <= 0 /\ __rho_2_^0-__rho_2_^post6 == 0 /\ -tt1^post6+tt1^0 == 0 /\ -1+wakend^post6 == 0 /\ last_copy_time^0-last_copy_time^post6 == 0 /\ -__rho_3_^post6+__rho_3_^0 == 0 /\ ret_time88^0-ret_time88^post6 == 0 /\ a77^0-a77^post6 == 0 /\ -ret_XLogArchivingActive44^post6+ret_XLogArchivingActive44^0 == 0 /\ -got_SIGHUP^post6+got_SIGHUP^0 == 0 /\ __const_1000^0-__const_1000^post6 == 0 /\ -ret_time66^post6+ret_time66^0 == 0 /\ __rho_1_^0-__rho_1_^post6 == 0 /\ -a55^post6+a55^0 == 0), cost: 1 7: l9 -> l7 : a33^0'=a33^post7, ret_time88^0'=ret_time88^post7, __rho_1_^0'=__rho_1_^post7, tt1^0'=tt1^post7, last_copy_time^0'=last_copy_time^post7, a77^0'=a77^post7, __rho_3_^0'=__rho_3_^post7, ret_time66^0'=ret_time66^post7, __const_1000^0'=__const_1000^post7, got_SIGHUP^0'=got_SIGHUP^post7, a55^0'=a55^post7, tmp2^0'=tmp2^post7, __rho_2_^0'=__rho_2_^post7, wakend^0'=wakend^post7, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post7, curtime^0'=curtime^post7, (-wakend^post7+wakend^0 == 0 /\ __const_1000^0-__const_1000^post7 == 0 /\ tmp2^0-tmp2^post7 == 0 /\ -a55^post7+a55^0 == 0 /\ ret_time88^0-ret_time88^post7 == 0 /\ last_copy_time^0-last_copy_time^post7 == 0 /\ -curtime^post7+curtime^0 == 0 /\ 1-wakend^0 <= 0 /\ -ret_XLogArchivingActive44^post7+ret_XLogArchivingActive44^0 == 0 /\ -__rho_2_^post7+__rho_2_^0 == 0 /\ -got_SIGHUP^post7+got_SIGHUP^0 == 0 /\ ret_time66^0-ret_time66^post7 == 0 /\ -__rho_3_^post7+__rho_3_^0 == 0 /\ a77^0-a77^post7 == 0 /\ __rho_1_^0-__rho_1_^post7 == 0 /\ tt1^0-tt1^post7 == 0 /\ a33^0-a33^post7 == 0), cost: 1 8: l9 -> l8 : a33^0'=a33^post8, ret_time88^0'=ret_time88^post8, __rho_1_^0'=__rho_1_^post8, tt1^0'=tt1^post8, last_copy_time^0'=last_copy_time^post8, a77^0'=a77^post8, __rho_3_^0'=__rho_3_^post8, ret_time66^0'=ret_time66^post8, __const_1000^0'=__const_1000^post8, got_SIGHUP^0'=got_SIGHUP^post8, a55^0'=a55^post8, tmp2^0'=tmp2^post8, __rho_2_^0'=__rho_2_^post8, wakend^0'=wakend^post8, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post8, curtime^0'=curtime^post8, (0 == 0 /\ -ret_time88^post8+curtime^post8 == 0 /\ got_SIGHUP^0-got_SIGHUP^post8 == 0 /\ __rho_2_^0-__rho_2_^post8 == 0 /\ -ret_XLogArchivingActive44^post8+ret_XLogArchivingActive44^0 == 0 /\ -ret_time66^post8+ret_time66^0 == 0 /\ -a55^post8+a55^0 == 0 /\ __rho_1_^0-__rho_1_^post8 == 0 /\ last_copy_time^0-last_copy_time^post8 == 0 /\ a77^post8 == 0 /\ a33^0-a33^post8 == 0 /\ wakend^0 <= 0 /\ -wakend^post8+wakend^0 == 0 /\ -__rho_3_^post8+ret_time88^post8 == 0 /\ -tmp2^post8+tmp2^0 == 0 /\ -tt1^post8+tt1^0 == 0 /\ __const_1000^0-__const_1000^post8 == 0), cost: 1 12: l10 -> l6 : a33^0'=a33^post12, ret_time88^0'=ret_time88^post12, __rho_1_^0'=__rho_1_^post12, tt1^0'=tt1^post12, last_copy_time^0'=last_copy_time^post12, a77^0'=a77^post12, __rho_3_^0'=__rho_3_^post12, ret_time66^0'=ret_time66^post12, __const_1000^0'=__const_1000^post12, got_SIGHUP^0'=got_SIGHUP^post12, a55^0'=a55^post12, tmp2^0'=tmp2^post12, __rho_2_^0'=__rho_2_^post12, wakend^0'=wakend^post12, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post12, curtime^0'=curtime^post12, (-a55^post12+a55^0 == 0 /\ ret_time88^0-ret_time88^post12 == 0 /\ -curtime^post12+curtime^0 == 0 /\ -wakend^post12+wakend^0 == 0 /\ a77^0-a77^post12 == 0 /\ -__rho_2_^post12+__rho_2_^0 == 0 /\ got_SIGHUP^0-got_SIGHUP^post12 == 0 /\ __rho_1_^0-__rho_1_^post12 == 0 /\ -tmp2^post12+tmp2^0 == 0 /\ -ret_XLogArchivingActive44^post12+ret_XLogArchivingActive44^0 == 0 /\ a33^0-a33^post12 == 0 /\ tt1^0-tt1^post12 == 0 /\ -__const_1000^post12+__const_1000^0 == 0 /\ __rho_3_^0-__rho_3_^post12 == 0 /\ -ret_time66^post12+ret_time66^0 == 0 /\ last_copy_time^0-last_copy_time^post12 == 0), cost: 1 15: l11 -> l0 : a33^0'=a33^post15, ret_time88^0'=ret_time88^post15, __rho_1_^0'=__rho_1_^post15, tt1^0'=tt1^post15, last_copy_time^0'=last_copy_time^post15, a77^0'=a77^post15, __rho_3_^0'=__rho_3_^post15, ret_time66^0'=ret_time66^post15, __const_1000^0'=__const_1000^post15, got_SIGHUP^0'=got_SIGHUP^post15, a55^0'=a55^post15, tmp2^0'=tmp2^post15, __rho_2_^0'=__rho_2_^post15, wakend^0'=wakend^post15, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post15, curtime^0'=curtime^post15, (0 == 0 /\ got_SIGHUP^post15-__rho_2_^post15 == 0 /\ a33^0-a33^post15 == 0 /\ __rho_1_^0-__rho_1_^post15 == 0 /\ tt1^0-tt1^post15 == 0 /\ -1+wakend^post15 == 0 /\ a55^0-a55^post15 == 0 /\ -__const_1000^post15+__const_1000^0 == 0 /\ -1+wakend^10 == 0 /\ -a77^post15+a77^0 == 0 /\ -tmp2^post15+tmp2^0 == 0 /\ -ret_time88^post15+ret_time88^0 == 0 /\ __rho_3_^0-__rho_3_^post15 == 0 /\ last_copy_time^0-last_copy_time^post15 == 0 /\ ret_time66^0-ret_time66^post15 == 0 /\ -curtime^post15+curtime^0 == 0 /\ -ret_XLogArchivingActive44^post15+ret_XLogArchivingActive44^0 == 0), cost: 1 16: l12 -> l11 : a33^0'=a33^post16, ret_time88^0'=ret_time88^post16, __rho_1_^0'=__rho_1_^post16, tt1^0'=tt1^post16, last_copy_time^0'=last_copy_time^post16, a77^0'=a77^post16, __rho_3_^0'=__rho_3_^post16, ret_time66^0'=ret_time66^post16, __const_1000^0'=__const_1000^post16, got_SIGHUP^0'=got_SIGHUP^post16, a55^0'=a55^post16, tmp2^0'=tmp2^post16, __rho_2_^0'=__rho_2_^post16, wakend^0'=wakend^post16, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post16, curtime^0'=curtime^post16, (tt1^0-tt1^post16 == 0 /\ __rho_3_^0-__rho_3_^post16 == 0 /\ wakend^0-wakend^post16 == 0 /\ -__rho_2_^post16+__rho_2_^0 == 0 /\ -a77^post16+a77^0 == 0 /\ -curtime^post16+curtime^0 == 0 /\ a33^0-a33^post16 == 0 /\ -__const_1000^post16+__const_1000^0 == 0 /\ __rho_1_^0-__rho_1_^post16 == 0 /\ last_copy_time^0-last_copy_time^post16 == 0 /\ -tmp2^post16+tmp2^0 == 0 /\ a55^0-a55^post16 == 0 /\ ret_time66^0-ret_time66^post16 == 0 /\ -ret_XLogArchivingActive44^post16+ret_XLogArchivingActive44^0 == 0 /\ -got_SIGHUP^post16+got_SIGHUP^0 == 0 /\ ret_time88^0-ret_time88^post16 == 0), cost: 1 Applied preprocessing Original rule: l0 -> l1 : a33^0'=a33^post0, ret_time88^0'=ret_time88^post0, __rho_1_^0'=__rho_1_^post0, tt1^0'=tt1^post0, last_copy_time^0'=last_copy_time^post0, a77^0'=a77^post0, __rho_3_^0'=__rho_3_^post0, ret_time66^0'=ret_time66^post0, __const_1000^0'=__const_1000^post0, got_SIGHUP^0'=got_SIGHUP^post0, a55^0'=a55^post0, tmp2^0'=tmp2^post0, __rho_2_^0'=__rho_2_^post0, wakend^0'=wakend^post0, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post0, curtime^0'=curtime^post0, (-got_SIGHUP^post0+got_SIGHUP^0 == 0 /\ __rho_3_^0-__rho_3_^post0 == 0 /\ -a77^post0+a77^0 == 0 /\ tt1^0-tt1^post0 == 0 /\ -__const_1000^post0+__const_1000^0 == 0 /\ a33^0-a33^post0 == 0 /\ a55^0-a55^post0 == 0 /\ last_copy_time^0-last_copy_time^post0 == 0 /\ -wakend^post0+wakend^0 == 0 /\ got_SIGHUP^0 <= 0 /\ __rho_1_^0-__rho_1_^post0 == 0 /\ ret_time66^0-ret_time66^post0 == 0 /\ -ret_time88^post0+ret_time88^0 == 0 /\ -tmp2^post0+tmp2^0 == 0 /\ -curtime^post0+curtime^0 == 0 /\ -__rho_2_^post0+__rho_2_^0 == 0 /\ -ret_XLogArchivingActive44^post0+ret_XLogArchivingActive44^0 == 0), cost: 1 New rule: l0 -> l1 : got_SIGHUP^0 <= 0, cost: 1 Applied preprocessing Original rule: l0 -> l2 : a33^0'=a33^post1, ret_time88^0'=ret_time88^post1, __rho_1_^0'=__rho_1_^post1, tt1^0'=tt1^post1, last_copy_time^0'=last_copy_time^post1, a77^0'=a77^post1, __rho_3_^0'=__rho_3_^post1, ret_time66^0'=ret_time66^post1, __const_1000^0'=__const_1000^post1, got_SIGHUP^0'=got_SIGHUP^post1, a55^0'=a55^post1, tmp2^0'=tmp2^post1, __rho_2_^0'=__rho_2_^post1, wakend^0'=wakend^post1, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, curtime^0'=curtime^post1, (0 == 0 /\ ret_time88^0-ret_time88^post1 == 0 /\ -curtime^post1+curtime^0 == 0 /\ -tmp2^post1+tt1^post1 == 0 /\ -__const_1000^post1+__const_1000^0 == 0 /\ -a77^post1+a77^0 == 0 /\ -wakend^post1+wakend^0 == 0 /\ __rho_3_^0-__rho_3_^post1 == 0 /\ got_SIGHUP^post1 == 0 /\ a55^0-a55^post1 == 0 /\ -__rho_1_^post1+ret_XLogArchivingActive44^post1 == 0 /\ -last_copy_time^post1+last_copy_time^0 == 0 /\ ret_time66^0-ret_time66^post1 == 0 /\ -__rho_2_^post1+__rho_2_^0 == 0 /\ 1-got_SIGHUP^0 <= 0 /\ -1+a33^post1 == 0 /\ tmp2^post1-ret_XLogArchivingActive44^post1 == 0), cost: 1 New rule: l0 -> l2 : a33^0'=1, __rho_1_^0'=ret_XLogArchivingActive44^post1, tt1^0'=ret_XLogArchivingActive44^post1, got_SIGHUP^0'=0, tmp2^0'=ret_XLogArchivingActive44^post1, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, -1+got_SIGHUP^0 >= 0, cost: 1 Applied preprocessing Original rule: l5 -> l6 : a33^0'=a33^post3, ret_time88^0'=ret_time88^post3, __rho_1_^0'=__rho_1_^post3, tt1^0'=tt1^post3, last_copy_time^0'=last_copy_time^post3, a77^0'=a77^post3, __rho_3_^0'=__rho_3_^post3, ret_time66^0'=ret_time66^post3, __const_1000^0'=__const_1000^post3, got_SIGHUP^0'=got_SIGHUP^post3, a55^0'=a55^post3, tmp2^0'=tmp2^post3, __rho_2_^0'=__rho_2_^post3, wakend^0'=wakend^post3, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post3, curtime^0'=curtime^post3, (-__rho_2_^post3+__rho_2_^0 == 0 /\ __rho_3_^0-__rho_3_^post3 == 0 /\ -got_SIGHUP^post3+got_SIGHUP^0 == 0 /\ -__const_1000^post3+__const_1000^0 == 0 /\ a33^0-a33^post3 == 0 /\ -ret_XLogArchivingActive44^post3+ret_XLogArchivingActive44^0 == 0 /\ tt1^0-tt1^post3 == 0 /\ -curtime^post3+curtime^0 == 0 /\ -tmp2^post3+tmp2^0 == 0 /\ a55^0-a55^post3 == 0 /\ last_copy_time^0-last_copy_time^post3 == 0 /\ ret_time88^0-ret_time88^post3 == 0 /\ __rho_1_^0-__rho_1_^post3 == 0 /\ ret_time66^0-ret_time66^post3 == 0 /\ -a77^post3+a77^0 == 0 /\ -wakend^post3+wakend^0 == 0), cost: 1 New rule: l5 -> l6 : TRUE, cost: 1 Applied preprocessing Original rule: l7 -> l5 : a33^0'=a33^post4, ret_time88^0'=ret_time88^post4, __rho_1_^0'=__rho_1_^post4, tt1^0'=tt1^post4, last_copy_time^0'=last_copy_time^post4, a77^0'=a77^post4, __rho_3_^0'=__rho_3_^post4, ret_time66^0'=ret_time66^post4, __const_1000^0'=__const_1000^post4, got_SIGHUP^0'=got_SIGHUP^post4, a55^0'=a55^post4, tmp2^0'=tmp2^post4, __rho_2_^0'=__rho_2_^post4, wakend^0'=wakend^post4, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post4, curtime^0'=curtime^post4, (__const_1000^0-__const_1000^post4 == 0 /\ -__rho_2_^post4+__rho_2_^0 == 0 /\ -ret_XLogArchivingActive44^post4+ret_XLogArchivingActive44^0 == 0 /\ a33^0-a33^post4 == 0 /\ -got_SIGHUP^post4+got_SIGHUP^0 == 0 /\ last_copy_time^0-last_copy_time^post4 == 0 /\ ret_time88^0-ret_time88^post4 == 0 /\ -a55^post4+a55^0 == 0 /\ ret_time66^0-ret_time66^post4 == 0 /\ -__rho_1_^post4+__rho_1_^0 == 0 /\ -curtime^post4+curtime^0 == 0 /\ tmp2^0-tmp2^post4 == 0 /\ a77^0-a77^post4 == 0 /\ -__rho_3_^post4+__rho_3_^0 == 0 /\ -wakend^post4+wakend^0 == 0 /\ tt1^0-tt1^post4 == 0), cost: 1 New rule: l7 -> l5 : TRUE, cost: 1 Applied preprocessing Original rule: l8 -> l7 : a33^0'=a33^post5, ret_time88^0'=ret_time88^post5, __rho_1_^0'=__rho_1_^post5, tt1^0'=tt1^post5, last_copy_time^0'=last_copy_time^post5, a77^0'=a77^post5, __rho_3_^0'=__rho_3_^post5, ret_time66^0'=ret_time66^post5, __const_1000^0'=__const_1000^post5, got_SIGHUP^0'=got_SIGHUP^post5, a55^0'=a55^post5, tmp2^0'=tmp2^post5, __rho_2_^0'=__rho_2_^post5, wakend^0'=wakend^post5, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post5, curtime^0'=curtime^post5, (1-last_copy_time^0-__const_1000^0+curtime^0 <= 0 /\ -got_SIGHUP^post5+got_SIGHUP^0 == 0 /\ a33^0-a33^post5 == 0 /\ last_copy_time^0-last_copy_time^post5 == 0 /\ -__rho_3_^post5+__rho_3_^0 == 0 /\ ret_time66^0-ret_time66^post5 == 0 /\ __const_1000^0-__const_1000^post5 == 0 /\ -__rho_1_^post5+__rho_1_^0 == 0 /\ -a55^post5+a55^0 == 0 /\ -wakend^post5+wakend^0 == 0 /\ -__rho_2_^post5+__rho_2_^0 == 0 /\ -ret_XLogArchivingActive44^post5+ret_XLogArchivingActive44^0 == 0 /\ tt1^0-tt1^post5 == 0 /\ -curtime^post5+curtime^0 == 0 /\ ret_time88^0-ret_time88^post5 == 0 /\ tmp2^0-tmp2^post5 == 0 /\ a77^0-a77^post5 == 0), cost: 1 New rule: l8 -> l7 : 1-last_copy_time^0-__const_1000^0+curtime^0 <= 0, cost: 1 Applied preprocessing Original rule: l8 -> l7 : a33^0'=a33^post6, ret_time88^0'=ret_time88^post6, __rho_1_^0'=__rho_1_^post6, tt1^0'=tt1^post6, last_copy_time^0'=last_copy_time^post6, a77^0'=a77^post6, __rho_3_^0'=__rho_3_^post6, ret_time66^0'=ret_time66^post6, __const_1000^0'=__const_1000^post6, got_SIGHUP^0'=got_SIGHUP^post6, a55^0'=a55^post6, tmp2^0'=tmp2^post6, __rho_2_^0'=__rho_2_^post6, wakend^0'=wakend^post6, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post6, curtime^0'=curtime^post6, (a33^0-a33^post6 == 0 /\ -tmp2^post6+tmp2^0 == 0 /\ -curtime^post6+curtime^0 == 0 /\ last_copy_time^0+__const_1000^0-curtime^0 <= 0 /\ __rho_2_^0-__rho_2_^post6 == 0 /\ -tt1^post6+tt1^0 == 0 /\ -1+wakend^post6 == 0 /\ last_copy_time^0-last_copy_time^post6 == 0 /\ -__rho_3_^post6+__rho_3_^0 == 0 /\ ret_time88^0-ret_time88^post6 == 0 /\ a77^0-a77^post6 == 0 /\ -ret_XLogArchivingActive44^post6+ret_XLogArchivingActive44^0 == 0 /\ -got_SIGHUP^post6+got_SIGHUP^0 == 0 /\ __const_1000^0-__const_1000^post6 == 0 /\ -ret_time66^post6+ret_time66^0 == 0 /\ __rho_1_^0-__rho_1_^post6 == 0 /\ -a55^post6+a55^0 == 0), cost: 1 New rule: l8 -> l7 : wakend^0'=1, last_copy_time^0+__const_1000^0-curtime^0 <= 0, cost: 1 Applied preprocessing Original rule: l9 -> l7 : a33^0'=a33^post7, ret_time88^0'=ret_time88^post7, __rho_1_^0'=__rho_1_^post7, tt1^0'=tt1^post7, last_copy_time^0'=last_copy_time^post7, a77^0'=a77^post7, __rho_3_^0'=__rho_3_^post7, ret_time66^0'=ret_time66^post7, __const_1000^0'=__const_1000^post7, got_SIGHUP^0'=got_SIGHUP^post7, a55^0'=a55^post7, tmp2^0'=tmp2^post7, __rho_2_^0'=__rho_2_^post7, wakend^0'=wakend^post7, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post7, curtime^0'=curtime^post7, (-wakend^post7+wakend^0 == 0 /\ __const_1000^0-__const_1000^post7 == 0 /\ tmp2^0-tmp2^post7 == 0 /\ -a55^post7+a55^0 == 0 /\ ret_time88^0-ret_time88^post7 == 0 /\ last_copy_time^0-last_copy_time^post7 == 0 /\ -curtime^post7+curtime^0 == 0 /\ 1-wakend^0 <= 0 /\ -ret_XLogArchivingActive44^post7+ret_XLogArchivingActive44^0 == 0 /\ -__rho_2_^post7+__rho_2_^0 == 0 /\ -got_SIGHUP^post7+got_SIGHUP^0 == 0 /\ ret_time66^0-ret_time66^post7 == 0 /\ -__rho_3_^post7+__rho_3_^0 == 0 /\ a77^0-a77^post7 == 0 /\ __rho_1_^0-__rho_1_^post7 == 0 /\ tt1^0-tt1^post7 == 0 /\ a33^0-a33^post7 == 0), cost: 1 New rule: l9 -> l7 : -1+wakend^0 >= 0, cost: 1 Applied preprocessing Original rule: l9 -> l8 : a33^0'=a33^post8, ret_time88^0'=ret_time88^post8, __rho_1_^0'=__rho_1_^post8, tt1^0'=tt1^post8, last_copy_time^0'=last_copy_time^post8, a77^0'=a77^post8, __rho_3_^0'=__rho_3_^post8, ret_time66^0'=ret_time66^post8, __const_1000^0'=__const_1000^post8, got_SIGHUP^0'=got_SIGHUP^post8, a55^0'=a55^post8, tmp2^0'=tmp2^post8, __rho_2_^0'=__rho_2_^post8, wakend^0'=wakend^post8, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post8, curtime^0'=curtime^post8, (0 == 0 /\ -ret_time88^post8+curtime^post8 == 0 /\ got_SIGHUP^0-got_SIGHUP^post8 == 0 /\ __rho_2_^0-__rho_2_^post8 == 0 /\ -ret_XLogArchivingActive44^post8+ret_XLogArchivingActive44^0 == 0 /\ -ret_time66^post8+ret_time66^0 == 0 /\ -a55^post8+a55^0 == 0 /\ __rho_1_^0-__rho_1_^post8 == 0 /\ last_copy_time^0-last_copy_time^post8 == 0 /\ a77^post8 == 0 /\ a33^0-a33^post8 == 0 /\ wakend^0 <= 0 /\ -wakend^post8+wakend^0 == 0 /\ -__rho_3_^post8+ret_time88^post8 == 0 /\ -tmp2^post8+tmp2^0 == 0 /\ -tt1^post8+tt1^0 == 0 /\ __const_1000^0-__const_1000^post8 == 0), cost: 1 New rule: l9 -> l8 : ret_time88^0'=curtime^post8, a77^0'=0, __rho_3_^0'=curtime^post8, curtime^0'=curtime^post8, wakend^0 <= 0, cost: 1 Applied preprocessing Original rule: l1 -> l9 : a33^0'=a33^post9, ret_time88^0'=ret_time88^post9, __rho_1_^0'=__rho_1_^post9, tt1^0'=tt1^post9, last_copy_time^0'=last_copy_time^post9, a77^0'=a77^post9, __rho_3_^0'=__rho_3_^post9, ret_time66^0'=ret_time66^post9, __const_1000^0'=__const_1000^post9, got_SIGHUP^0'=got_SIGHUP^post9, a55^0'=a55^post9, tmp2^0'=tmp2^post9, __rho_2_^0'=__rho_2_^post9, wakend^0'=wakend^post9, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post9, curtime^0'=curtime^post9, (-tt1^post9+tt1^0 == 0 /\ -__rho_3_^post9+__rho_3_^0 == 0 /\ ret_time88^0-ret_time88^post9 == 0 /\ __rho_2_^0-__rho_2_^post9 == 0 /\ a77^0-a77^post9 == 0 /\ last_copy_time^0-last_copy_time^post9 == 0 /\ __rho_1_^0-__rho_1_^post9 == 0 /\ -wakend^post9+wakend^0 == 0 /\ -a55^post9+a55^0 == 0 /\ -ret_time66^post9+ret_time66^0 == 0 /\ a33^0-a33^post9 == 0 /\ -curtime^post9+curtime^0 == 0 /\ -ret_XLogArchivingActive44^post9+ret_XLogArchivingActive44^0 == 0 /\ -tmp2^post9+tmp2^0 == 0 /\ wakend^0 <= 0 /\ __const_1000^0-__const_1000^post9 == 0 /\ -got_SIGHUP^post9+got_SIGHUP^0 == 0), cost: 1 New rule: l1 -> l9 : wakend^0 <= 0, cost: 1 Applied preprocessing Original rule: l1 -> l9 : a33^0'=a33^post10, ret_time88^0'=ret_time88^post10, __rho_1_^0'=__rho_1_^post10, tt1^0'=tt1^post10, last_copy_time^0'=last_copy_time^post10, a77^0'=a77^post10, __rho_3_^0'=__rho_3_^post10, ret_time66^0'=ret_time66^post10, __const_1000^0'=__const_1000^post10, got_SIGHUP^0'=got_SIGHUP^post10, a55^0'=a55^post10, tmp2^0'=tmp2^post10, __rho_2_^0'=__rho_2_^post10, wakend^0'=wakend^post10, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post10, curtime^0'=curtime^post10, (0 == 0 /\ ret_time88^0-ret_time88^post10 == 0 /\ -curtime^post10+curtime^0 == 0 /\ wakend^post10 == 0 /\ a55^post10 == 0 /\ a77^0-a77^post10 == 0 /\ 1-wakend^0 <= 0 /\ -__rho_2_^post10+__rho_2_^0 == 0 /\ got_SIGHUP^0-got_SIGHUP^post10 == 0 /\ -tmp2^post10+tmp2^0 == 0 /\ __rho_1_^0-__rho_1_^post10 == 0 /\ -ret_XLogArchivingActive44^post10+ret_XLogArchivingActive44^0 == 0 /\ ret_time66^post10-__rho_3_^post10 == 0 /\ -ret_time66^post10+last_copy_time^post10 == 0 /\ a33^0-a33^post10 == 0 /\ tt1^0-tt1^post10 == 0 /\ -__const_1000^post10+__const_1000^0 == 0), cost: 1 New rule: l1 -> l9 : last_copy_time^0'=__rho_3_^post10, __rho_3_^0'=__rho_3_^post10, ret_time66^0'=__rho_3_^post10, a55^0'=0, wakend^0'=0, -1+wakend^0 >= 0, cost: 1 Applied preprocessing Original rule: l6 -> l10 : a33^0'=a33^post11, ret_time88^0'=ret_time88^post11, __rho_1_^0'=__rho_1_^post11, tt1^0'=tt1^post11, last_copy_time^0'=last_copy_time^post11, a77^0'=a77^post11, __rho_3_^0'=__rho_3_^post11, ret_time66^0'=ret_time66^post11, __const_1000^0'=__const_1000^post11, got_SIGHUP^0'=got_SIGHUP^post11, a55^0'=a55^post11, tmp2^0'=tmp2^post11, __rho_2_^0'=__rho_2_^post11, wakend^0'=wakend^post11, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post11, curtime^0'=curtime^post11, (__rho_2_^0-__rho_2_^post11 == 0 /\ -ret_time66^post11+ret_time66^0 == 0 /\ got_SIGHUP^0-got_SIGHUP^post11 == 0 /\ __rho_1_^0-__rho_1_^post11 == 0 /\ -a55^post11+a55^0 == 0 /\ a77^0-a77^post11 == 0 /\ ret_time88^0-ret_time88^post11 == 0 /\ -tt1^post11+tt1^0 == 0 /\ __const_1000^0-__const_1000^post11 == 0 /\ -tmp2^post11+tmp2^0 == 0 /\ a33^0-a33^post11 == 0 /\ -curtime^post11+curtime^0 == 0 /\ -ret_XLogArchivingActive44^post11+ret_XLogArchivingActive44^0 == 0 /\ __rho_3_^0-__rho_3_^post11 == 0 /\ last_copy_time^0-last_copy_time^post11 == 0 /\ -wakend^post11+wakend^0 == 0), cost: 1 New rule: l6 -> l10 : TRUE, cost: 1 Applied preprocessing Original rule: l10 -> l6 : a33^0'=a33^post12, ret_time88^0'=ret_time88^post12, __rho_1_^0'=__rho_1_^post12, tt1^0'=tt1^post12, last_copy_time^0'=last_copy_time^post12, a77^0'=a77^post12, __rho_3_^0'=__rho_3_^post12, ret_time66^0'=ret_time66^post12, __const_1000^0'=__const_1000^post12, got_SIGHUP^0'=got_SIGHUP^post12, a55^0'=a55^post12, tmp2^0'=tmp2^post12, __rho_2_^0'=__rho_2_^post12, wakend^0'=wakend^post12, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post12, curtime^0'=curtime^post12, (-a55^post12+a55^0 == 0 /\ ret_time88^0-ret_time88^post12 == 0 /\ -curtime^post12+curtime^0 == 0 /\ -wakend^post12+wakend^0 == 0 /\ a77^0-a77^post12 == 0 /\ -__rho_2_^post12+__rho_2_^0 == 0 /\ got_SIGHUP^0-got_SIGHUP^post12 == 0 /\ __rho_1_^0-__rho_1_^post12 == 0 /\ -tmp2^post12+tmp2^0 == 0 /\ -ret_XLogArchivingActive44^post12+ret_XLogArchivingActive44^0 == 0 /\ a33^0-a33^post12 == 0 /\ tt1^0-tt1^post12 == 0 /\ -__const_1000^post12+__const_1000^0 == 0 /\ __rho_3_^0-__rho_3_^post12 == 0 /\ -ret_time66^post12+ret_time66^0 == 0 /\ last_copy_time^0-last_copy_time^post12 == 0), cost: 1 New rule: l10 -> l6 : TRUE, cost: 1 Applied preprocessing Original rule: l2 -> l1 : a33^0'=a33^post13, ret_time88^0'=ret_time88^post13, __rho_1_^0'=__rho_1_^post13, tt1^0'=tt1^post13, last_copy_time^0'=last_copy_time^post13, a77^0'=a77^post13, __rho_3_^0'=__rho_3_^post13, ret_time66^0'=ret_time66^post13, __const_1000^0'=__const_1000^post13, got_SIGHUP^0'=got_SIGHUP^post13, a55^0'=a55^post13, tmp2^0'=tmp2^post13, __rho_2_^0'=__rho_2_^post13, wakend^0'=wakend^post13, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post13, curtime^0'=curtime^post13, (__rho_2_^0-__rho_2_^post13 == 0 /\ -wakend^post13+wakend^0 == 0 /\ -ret_time66^post13+ret_time66^0 == 0 /\ -ret_XLogArchivingActive44^post13+ret_XLogArchivingActive44^0 == 0 /\ got_SIGHUP^0-got_SIGHUP^post13 == 0 /\ -a55^post13+a55^0 == 0 /\ __rho_1_^0-__rho_1_^post13 == 0 /\ a33^0-a33^post13 == 0 /\ a77^0-a77^post13 == 0 /\ -tt1^post13+tt1^0 == 0 /\ 1-tt1^0 <= 0 /\ __const_1000^0-__const_1000^post13 == 0 /\ ret_time88^0-ret_time88^post13 == 0 /\ -tmp2^post13+tmp2^0 == 0 /\ -curtime^post13+curtime^0 == 0 /\ last_copy_time^0-last_copy_time^post13 == 0 /\ __rho_3_^0-__rho_3_^post13 == 0), cost: 1 New rule: l2 -> l1 : -1+tt1^0 >= 0, cost: 1 Applied preprocessing Original rule: l2 -> l5 : a33^0'=a33^post14, ret_time88^0'=ret_time88^post14, __rho_1_^0'=__rho_1_^post14, tt1^0'=tt1^post14, last_copy_time^0'=last_copy_time^post14, a77^0'=a77^post14, __rho_3_^0'=__rho_3_^post14, ret_time66^0'=ret_time66^post14, __const_1000^0'=__const_1000^post14, got_SIGHUP^0'=got_SIGHUP^post14, a55^0'=a55^post14, tmp2^0'=tmp2^post14, __rho_2_^0'=__rho_2_^post14, wakend^0'=wakend^post14, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post14, curtime^0'=curtime^post14, (-last_copy_time^post14+last_copy_time^0 == 0 /\ __rho_1_^0-__rho_1_^post14 == 0 /\ tt1^0 <= 0 /\ wakend^0-wakend^post14 == 0 /\ ret_time88^0-ret_time88^post14 == 0 /\ -ret_time66^post14+ret_time66^0 == 0 /\ a33^0-a33^post14 == 0 /\ -__const_1000^post14+__const_1000^0 == 0 /\ got_SIGHUP^0-got_SIGHUP^post14 == 0 /\ -curtime^post14+curtime^0 == 0 /\ -a55^post14+a55^0 == 0 /\ __rho_3_^0-__rho_3_^post14 == 0 /\ -__rho_2_^post14+__rho_2_^0 == 0 /\ tt1^0-tt1^post14 == 0 /\ a77^0-a77^post14 == 0 /\ -tmp2^post14+tmp2^0 == 0 /\ -ret_XLogArchivingActive44^post14+ret_XLogArchivingActive44^0 == 0), cost: 1 New rule: l2 -> l5 : tt1^0 <= 0, cost: 1 Applied preprocessing Original rule: l11 -> l0 : a33^0'=a33^post15, ret_time88^0'=ret_time88^post15, __rho_1_^0'=__rho_1_^post15, tt1^0'=tt1^post15, last_copy_time^0'=last_copy_time^post15, a77^0'=a77^post15, __rho_3_^0'=__rho_3_^post15, ret_time66^0'=ret_time66^post15, __const_1000^0'=__const_1000^post15, got_SIGHUP^0'=got_SIGHUP^post15, a55^0'=a55^post15, tmp2^0'=tmp2^post15, __rho_2_^0'=__rho_2_^post15, wakend^0'=wakend^post15, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post15, curtime^0'=curtime^post15, (0 == 0 /\ got_SIGHUP^post15-__rho_2_^post15 == 0 /\ a33^0-a33^post15 == 0 /\ __rho_1_^0-__rho_1_^post15 == 0 /\ tt1^0-tt1^post15 == 0 /\ -1+wakend^post15 == 0 /\ a55^0-a55^post15 == 0 /\ -__const_1000^post15+__const_1000^0 == 0 /\ -1+wakend^10 == 0 /\ -a77^post15+a77^0 == 0 /\ -tmp2^post15+tmp2^0 == 0 /\ -ret_time88^post15+ret_time88^0 == 0 /\ __rho_3_^0-__rho_3_^post15 == 0 /\ last_copy_time^0-last_copy_time^post15 == 0 /\ ret_time66^0-ret_time66^post15 == 0 /\ -curtime^post15+curtime^0 == 0 /\ -ret_XLogArchivingActive44^post15+ret_XLogArchivingActive44^0 == 0), cost: 1 New rule: l11 -> l0 : got_SIGHUP^0'=__rho_2_^post15, __rho_2_^0'=__rho_2_^post15, wakend^0'=1, 0 == 0, cost: 1 Applied preprocessing Original rule: l12 -> l11 : a33^0'=a33^post16, ret_time88^0'=ret_time88^post16, __rho_1_^0'=__rho_1_^post16, tt1^0'=tt1^post16, last_copy_time^0'=last_copy_time^post16, a77^0'=a77^post16, __rho_3_^0'=__rho_3_^post16, ret_time66^0'=ret_time66^post16, __const_1000^0'=__const_1000^post16, got_SIGHUP^0'=got_SIGHUP^post16, a55^0'=a55^post16, tmp2^0'=tmp2^post16, __rho_2_^0'=__rho_2_^post16, wakend^0'=wakend^post16, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post16, curtime^0'=curtime^post16, (tt1^0-tt1^post16 == 0 /\ __rho_3_^0-__rho_3_^post16 == 0 /\ wakend^0-wakend^post16 == 0 /\ -__rho_2_^post16+__rho_2_^0 == 0 /\ -a77^post16+a77^0 == 0 /\ -curtime^post16+curtime^0 == 0 /\ a33^0-a33^post16 == 0 /\ -__const_1000^post16+__const_1000^0 == 0 /\ __rho_1_^0-__rho_1_^post16 == 0 /\ last_copy_time^0-last_copy_time^post16 == 0 /\ -tmp2^post16+tmp2^0 == 0 /\ a55^0-a55^post16 == 0 /\ ret_time66^0-ret_time66^post16 == 0 /\ -ret_XLogArchivingActive44^post16+ret_XLogArchivingActive44^0 == 0 /\ -got_SIGHUP^post16+got_SIGHUP^0 == 0 /\ ret_time88^0-ret_time88^post16 == 0), cost: 1 New rule: l12 -> l11 : TRUE, cost: 1 Simplified rules Start location: l12 17: l0 -> l1 : got_SIGHUP^0 <= 0, cost: 1 18: l0 -> l2 : a33^0'=1, __rho_1_^0'=ret_XLogArchivingActive44^post1, tt1^0'=ret_XLogArchivingActive44^post1, got_SIGHUP^0'=0, tmp2^0'=ret_XLogArchivingActive44^post1, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, -1+got_SIGHUP^0 >= 0, cost: 1 25: l1 -> l9 : wakend^0 <= 0, cost: 1 26: l1 -> l9 : last_copy_time^0'=__rho_3_^post10, __rho_3_^0'=__rho_3_^post10, ret_time66^0'=__rho_3_^post10, a55^0'=0, wakend^0'=0, -1+wakend^0 >= 0, cost: 1 29: l2 -> l1 : -1+tt1^0 >= 0, cost: 1 30: l2 -> l5 : tt1^0 <= 0, cost: 1 19: l5 -> l6 : TRUE, cost: 1 27: l6 -> l10 : TRUE, cost: 1 20: l7 -> l5 : TRUE, cost: 1 21: l8 -> l7 : 1-last_copy_time^0-__const_1000^0+curtime^0 <= 0, cost: 1 22: l8 -> l7 : wakend^0'=1, last_copy_time^0+__const_1000^0-curtime^0 <= 0, cost: 1 23: l9 -> l7 : -1+wakend^0 >= 0, cost: 1 24: l9 -> l8 : ret_time88^0'=curtime^post8, a77^0'=0, __rho_3_^0'=curtime^post8, curtime^0'=curtime^post8, wakend^0 <= 0, cost: 1 28: l10 -> l6 : TRUE, cost: 1 31: l11 -> l0 : got_SIGHUP^0'=__rho_2_^post15, __rho_2_^0'=__rho_2_^post15, wakend^0'=1, 0 == 0, cost: 1 32: l12 -> l11 : TRUE, cost: 1 Eliminating location l11 by chaining: Applied chaining First rule: l12 -> l11 : TRUE, cost: 1 Second rule: l11 -> l0 : got_SIGHUP^0'=__rho_2_^post15, __rho_2_^0'=__rho_2_^post15, wakend^0'=1, 0 == 0, cost: 1 New rule: l12 -> l0 : got_SIGHUP^0'=__rho_2_^post15, __rho_2_^0'=__rho_2_^post15, wakend^0'=1, 0 == 0, cost: 2 Applied deletion Removed the following rules: 31 32 Eliminating location l10 by chaining: Applied chaining First rule: l6 -> l10 : TRUE, cost: 1 Second rule: l10 -> l6 : TRUE, cost: 1 New rule: l6 -> l6 : TRUE, cost: 2 Applied deletion Removed the following rules: 27 28 Eliminated locations on linear paths Start location: l12 17: l0 -> l1 : got_SIGHUP^0 <= 0, cost: 1 18: l0 -> l2 : a33^0'=1, __rho_1_^0'=ret_XLogArchivingActive44^post1, tt1^0'=ret_XLogArchivingActive44^post1, got_SIGHUP^0'=0, tmp2^0'=ret_XLogArchivingActive44^post1, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, -1+got_SIGHUP^0 >= 0, cost: 1 25: l1 -> l9 : wakend^0 <= 0, cost: 1 26: l1 -> l9 : last_copy_time^0'=__rho_3_^post10, __rho_3_^0'=__rho_3_^post10, ret_time66^0'=__rho_3_^post10, a55^0'=0, wakend^0'=0, -1+wakend^0 >= 0, cost: 1 29: l2 -> l1 : -1+tt1^0 >= 0, cost: 1 30: l2 -> l5 : tt1^0 <= 0, cost: 1 19: l5 -> l6 : TRUE, cost: 1 34: l6 -> l6 : TRUE, cost: 2 20: l7 -> l5 : TRUE, cost: 1 21: l8 -> l7 : 1-last_copy_time^0-__const_1000^0+curtime^0 <= 0, cost: 1 22: l8 -> l7 : wakend^0'=1, last_copy_time^0+__const_1000^0-curtime^0 <= 0, cost: 1 23: l9 -> l7 : -1+wakend^0 >= 0, cost: 1 24: l9 -> l8 : ret_time88^0'=curtime^post8, a77^0'=0, __rho_3_^0'=curtime^post8, curtime^0'=curtime^post8, wakend^0 <= 0, cost: 1 33: l12 -> l0 : got_SIGHUP^0'=__rho_2_^post15, __rho_2_^0'=__rho_2_^post15, wakend^0'=1, 0 == 0, cost: 2 Applied nonterm Original rule: l6 -> l6 : TRUE, cost: 2 New rule: l6 -> [13] : n >= 0, cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_kFJOmK.txt Applied deletion Removed the following rules: 34 Accelerated simple loops Start location: l12 17: l0 -> l1 : got_SIGHUP^0 <= 0, cost: 1 18: l0 -> l2 : a33^0'=1, __rho_1_^0'=ret_XLogArchivingActive44^post1, tt1^0'=ret_XLogArchivingActive44^post1, got_SIGHUP^0'=0, tmp2^0'=ret_XLogArchivingActive44^post1, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, -1+got_SIGHUP^0 >= 0, cost: 1 25: l1 -> l9 : wakend^0 <= 0, cost: 1 26: l1 -> l9 : last_copy_time^0'=__rho_3_^post10, __rho_3_^0'=__rho_3_^post10, ret_time66^0'=__rho_3_^post10, a55^0'=0, wakend^0'=0, -1+wakend^0 >= 0, cost: 1 29: l2 -> l1 : -1+tt1^0 >= 0, cost: 1 30: l2 -> l5 : tt1^0 <= 0, cost: 1 19: l5 -> l6 : TRUE, cost: 1 35: l6 -> [13] : n >= 0, cost: NONTERM 20: l7 -> l5 : TRUE, cost: 1 21: l8 -> l7 : 1-last_copy_time^0-__const_1000^0+curtime^0 <= 0, cost: 1 22: l8 -> l7 : wakend^0'=1, last_copy_time^0+__const_1000^0-curtime^0 <= 0, cost: 1 23: l9 -> l7 : -1+wakend^0 >= 0, cost: 1 24: l9 -> l8 : ret_time88^0'=curtime^post8, a77^0'=0, __rho_3_^0'=curtime^post8, curtime^0'=curtime^post8, wakend^0 <= 0, cost: 1 33: l12 -> l0 : got_SIGHUP^0'=__rho_2_^post15, __rho_2_^0'=__rho_2_^post15, wakend^0'=1, 0 == 0, cost: 2 Applied chaining First rule: l5 -> l6 : TRUE, cost: 1 Second rule: l6 -> [13] : n >= 0, cost: NONTERM New rule: l5 -> [13] : TRUE, cost: NONTERM Applied deletion Removed the following rules: 35 Chained accelerated rules with incoming rules Start location: l12 17: l0 -> l1 : got_SIGHUP^0 <= 0, cost: 1 18: l0 -> l2 : a33^0'=1, __rho_1_^0'=ret_XLogArchivingActive44^post1, tt1^0'=ret_XLogArchivingActive44^post1, got_SIGHUP^0'=0, tmp2^0'=ret_XLogArchivingActive44^post1, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, -1+got_SIGHUP^0 >= 0, cost: 1 25: l1 -> l9 : wakend^0 <= 0, cost: 1 26: l1 -> l9 : last_copy_time^0'=__rho_3_^post10, __rho_3_^0'=__rho_3_^post10, ret_time66^0'=__rho_3_^post10, a55^0'=0, wakend^0'=0, -1+wakend^0 >= 0, cost: 1 29: l2 -> l1 : -1+tt1^0 >= 0, cost: 1 30: l2 -> l5 : tt1^0 <= 0, cost: 1 19: l5 -> l6 : TRUE, cost: 1 36: l5 -> [13] : TRUE, cost: NONTERM 20: l7 -> l5 : TRUE, cost: 1 21: l8 -> l7 : 1-last_copy_time^0-__const_1000^0+curtime^0 <= 0, cost: 1 22: l8 -> l7 : wakend^0'=1, last_copy_time^0+__const_1000^0-curtime^0 <= 0, cost: 1 23: l9 -> l7 : -1+wakend^0 >= 0, cost: 1 24: l9 -> l8 : ret_time88^0'=curtime^post8, a77^0'=0, __rho_3_^0'=curtime^post8, curtime^0'=curtime^post8, wakend^0 <= 0, cost: 1 33: l12 -> l0 : got_SIGHUP^0'=__rho_2_^post15, __rho_2_^0'=__rho_2_^post15, wakend^0'=1, 0 == 0, cost: 2 Removed unreachable locations and irrelevant leafs Start location: l12 17: l0 -> l1 : got_SIGHUP^0 <= 0, cost: 1 18: l0 -> l2 : a33^0'=1, __rho_1_^0'=ret_XLogArchivingActive44^post1, tt1^0'=ret_XLogArchivingActive44^post1, got_SIGHUP^0'=0, tmp2^0'=ret_XLogArchivingActive44^post1, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, -1+got_SIGHUP^0 >= 0, cost: 1 25: l1 -> l9 : wakend^0 <= 0, cost: 1 26: l1 -> l9 : last_copy_time^0'=__rho_3_^post10, __rho_3_^0'=__rho_3_^post10, ret_time66^0'=__rho_3_^post10, a55^0'=0, wakend^0'=0, -1+wakend^0 >= 0, cost: 1 29: l2 -> l1 : -1+tt1^0 >= 0, cost: 1 30: l2 -> l5 : tt1^0 <= 0, cost: 1 36: l5 -> [13] : TRUE, cost: NONTERM 20: l7 -> l5 : TRUE, cost: 1 21: l8 -> l7 : 1-last_copy_time^0-__const_1000^0+curtime^0 <= 0, cost: 1 22: l8 -> l7 : wakend^0'=1, last_copy_time^0+__const_1000^0-curtime^0 <= 0, cost: 1 23: l9 -> l7 : -1+wakend^0 >= 0, cost: 1 24: l9 -> l8 : ret_time88^0'=curtime^post8, a77^0'=0, __rho_3_^0'=curtime^post8, curtime^0'=curtime^post8, wakend^0 <= 0, cost: 1 33: l12 -> l0 : got_SIGHUP^0'=__rho_2_^post15, __rho_2_^0'=__rho_2_^post15, wakend^0'=1, 0 == 0, cost: 2 Eliminating location l0 by chaining: Applied chaining First rule: l12 -> l0 : got_SIGHUP^0'=__rho_2_^post15, __rho_2_^0'=__rho_2_^post15, wakend^0'=1, 0 == 0, cost: 2 Second rule: l0 -> l1 : got_SIGHUP^0 <= 0, cost: 1 New rule: l12 -> l1 : got_SIGHUP^0'=__rho_2_^post15, __rho_2_^0'=__rho_2_^post15, wakend^0'=1, (0 == 0 /\ __rho_2_^post15 <= 0), cost: 3 Applied simplification Original rule: l12 -> l1 : got_SIGHUP^0'=__rho_2_^post15, __rho_2_^0'=__rho_2_^post15, wakend^0'=1, (0 == 0 /\ __rho_2_^post15 <= 0), cost: 3 New rule: l12 -> l1 : got_SIGHUP^0'=__rho_2_^post15, __rho_2_^0'=__rho_2_^post15, wakend^0'=1, __rho_2_^post15 <= 0, cost: 3 Applied chaining First rule: l12 -> l0 : got_SIGHUP^0'=__rho_2_^post15, __rho_2_^0'=__rho_2_^post15, wakend^0'=1, 0 == 0, cost: 2 Second rule: l0 -> l2 : a33^0'=1, __rho_1_^0'=ret_XLogArchivingActive44^post1, tt1^0'=ret_XLogArchivingActive44^post1, got_SIGHUP^0'=0, tmp2^0'=ret_XLogArchivingActive44^post1, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, -1+got_SIGHUP^0 >= 0, cost: 1 New rule: l12 -> l2 : a33^0'=1, __rho_1_^0'=ret_XLogArchivingActive44^post1, tt1^0'=ret_XLogArchivingActive44^post1, got_SIGHUP^0'=0, tmp2^0'=ret_XLogArchivingActive44^post1, __rho_2_^0'=__rho_2_^post15, wakend^0'=1, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, (0 == 0 /\ -1+__rho_2_^post15 >= 0), cost: 3 Applied simplification Original rule: l12 -> l2 : a33^0'=1, __rho_1_^0'=ret_XLogArchivingActive44^post1, tt1^0'=ret_XLogArchivingActive44^post1, got_SIGHUP^0'=0, tmp2^0'=ret_XLogArchivingActive44^post1, __rho_2_^0'=__rho_2_^post15, wakend^0'=1, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, (0 == 0 /\ -1+__rho_2_^post15 >= 0), cost: 3 New rule: l12 -> l2 : a33^0'=1, __rho_1_^0'=ret_XLogArchivingActive44^post1, tt1^0'=ret_XLogArchivingActive44^post1, got_SIGHUP^0'=0, tmp2^0'=ret_XLogArchivingActive44^post1, __rho_2_^0'=__rho_2_^post15, wakend^0'=1, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, -1+__rho_2_^post15 >= 0, cost: 3 Applied deletion Removed the following rules: 17 18 33 Eliminating location l9 by chaining: Applied chaining First rule: l1 -> l9 : wakend^0 <= 0, cost: 1 Second rule: l9 -> l8 : ret_time88^0'=curtime^post8, a77^0'=0, __rho_3_^0'=curtime^post8, curtime^0'=curtime^post8, wakend^0 <= 0, cost: 1 New rule: l1 -> l8 : ret_time88^0'=curtime^post8, a77^0'=0, __rho_3_^0'=curtime^post8, curtime^0'=curtime^post8, wakend^0 <= 0, cost: 2 Applied chaining First rule: l1 -> l9 : last_copy_time^0'=__rho_3_^post10, __rho_3_^0'=__rho_3_^post10, ret_time66^0'=__rho_3_^post10, a55^0'=0, wakend^0'=0, -1+wakend^0 >= 0, cost: 1 Second rule: l9 -> l8 : ret_time88^0'=curtime^post8, a77^0'=0, __rho_3_^0'=curtime^post8, curtime^0'=curtime^post8, wakend^0 <= 0, cost: 1 New rule: l1 -> l8 : ret_time88^0'=curtime^post8, last_copy_time^0'=__rho_3_^post10, a77^0'=0, __rho_3_^0'=curtime^post8, ret_time66^0'=__rho_3_^post10, a55^0'=0, wakend^0'=0, curtime^0'=curtime^post8, (0 <= 0 /\ -1+wakend^0 >= 0), cost: 2 Applied simplification Original rule: l1 -> l8 : ret_time88^0'=curtime^post8, last_copy_time^0'=__rho_3_^post10, a77^0'=0, __rho_3_^0'=curtime^post8, ret_time66^0'=__rho_3_^post10, a55^0'=0, wakend^0'=0, curtime^0'=curtime^post8, (0 <= 0 /\ -1+wakend^0 >= 0), cost: 2 New rule: l1 -> l8 : ret_time88^0'=curtime^post8, last_copy_time^0'=__rho_3_^post10, a77^0'=0, __rho_3_^0'=curtime^post8, ret_time66^0'=__rho_3_^post10, a55^0'=0, wakend^0'=0, curtime^0'=curtime^post8, -1+wakend^0 >= 0, cost: 2 Applied deletion Removed the following rules: 23 24 25 26 Eliminating location l7 by chaining: Applied chaining First rule: l8 -> l7 : 1-last_copy_time^0-__const_1000^0+curtime^0 <= 0, cost: 1 Second rule: l7 -> l5 : TRUE, cost: 1 New rule: l8 -> l5 : 1-last_copy_time^0-__const_1000^0+curtime^0 <= 0, cost: 2 Applied chaining First rule: l8 -> l7 : wakend^0'=1, last_copy_time^0+__const_1000^0-curtime^0 <= 0, cost: 1 Second rule: l7 -> l5 : TRUE, cost: 1 New rule: l8 -> l5 : wakend^0'=1, last_copy_time^0+__const_1000^0-curtime^0 <= 0, cost: 2 Applied deletion Removed the following rules: 20 21 22 Eliminated locations on tree-shaped paths Start location: l12 39: l1 -> l8 : ret_time88^0'=curtime^post8, a77^0'=0, __rho_3_^0'=curtime^post8, curtime^0'=curtime^post8, wakend^0 <= 0, cost: 2 40: l1 -> l8 : ret_time88^0'=curtime^post8, last_copy_time^0'=__rho_3_^post10, a77^0'=0, __rho_3_^0'=curtime^post8, ret_time66^0'=__rho_3_^post10, a55^0'=0, wakend^0'=0, curtime^0'=curtime^post8, -1+wakend^0 >= 0, cost: 2 29: l2 -> l1 : -1+tt1^0 >= 0, cost: 1 30: l2 -> l5 : tt1^0 <= 0, cost: 1 36: l5 -> [13] : TRUE, cost: NONTERM 41: l8 -> l5 : 1-last_copy_time^0-__const_1000^0+curtime^0 <= 0, cost: 2 42: l8 -> l5 : wakend^0'=1, last_copy_time^0+__const_1000^0-curtime^0 <= 0, cost: 2 37: l12 -> l1 : got_SIGHUP^0'=__rho_2_^post15, __rho_2_^0'=__rho_2_^post15, wakend^0'=1, __rho_2_^post15 <= 0, cost: 3 38: l12 -> l2 : a33^0'=1, __rho_1_^0'=ret_XLogArchivingActive44^post1, tt1^0'=ret_XLogArchivingActive44^post1, got_SIGHUP^0'=0, tmp2^0'=ret_XLogArchivingActive44^post1, __rho_2_^0'=__rho_2_^post15, wakend^0'=1, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, -1+__rho_2_^post15 >= 0, cost: 3 Eliminating location l2 by chaining: Applied chaining First rule: l12 -> l2 : a33^0'=1, __rho_1_^0'=ret_XLogArchivingActive44^post1, tt1^0'=ret_XLogArchivingActive44^post1, got_SIGHUP^0'=0, tmp2^0'=ret_XLogArchivingActive44^post1, __rho_2_^0'=__rho_2_^post15, wakend^0'=1, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, -1+__rho_2_^post15 >= 0, cost: 3 Second rule: l2 -> l1 : -1+tt1^0 >= 0, cost: 1 New rule: l12 -> l1 : a33^0'=1, __rho_1_^0'=ret_XLogArchivingActive44^post1, tt1^0'=ret_XLogArchivingActive44^post1, got_SIGHUP^0'=0, tmp2^0'=ret_XLogArchivingActive44^post1, __rho_2_^0'=__rho_2_^post15, wakend^0'=1, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, (-1+ret_XLogArchivingActive44^post1 >= 0 /\ -1+__rho_2_^post15 >= 0), cost: 4 Applied chaining First rule: l12 -> l2 : a33^0'=1, __rho_1_^0'=ret_XLogArchivingActive44^post1, tt1^0'=ret_XLogArchivingActive44^post1, got_SIGHUP^0'=0, tmp2^0'=ret_XLogArchivingActive44^post1, __rho_2_^0'=__rho_2_^post15, wakend^0'=1, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, -1+__rho_2_^post15 >= 0, cost: 3 Second rule: l2 -> l5 : tt1^0 <= 0, cost: 1 New rule: l12 -> l5 : a33^0'=1, __rho_1_^0'=ret_XLogArchivingActive44^post1, tt1^0'=ret_XLogArchivingActive44^post1, got_SIGHUP^0'=0, tmp2^0'=ret_XLogArchivingActive44^post1, __rho_2_^0'=__rho_2_^post15, wakend^0'=1, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, (-1+__rho_2_^post15 >= 0 /\ ret_XLogArchivingActive44^post1 <= 0), cost: 4 Applied deletion Removed the following rules: 29 30 38 Eliminating location l8 by chaining: Applied chaining First rule: l1 -> l8 : ret_time88^0'=curtime^post8, a77^0'=0, __rho_3_^0'=curtime^post8, curtime^0'=curtime^post8, wakend^0 <= 0, cost: 2 Second rule: l8 -> l5 : 1-last_copy_time^0-__const_1000^0+curtime^0 <= 0, cost: 2 New rule: l1 -> l5 : ret_time88^0'=curtime^post8, a77^0'=0, __rho_3_^0'=curtime^post8, curtime^0'=curtime^post8, (1-last_copy_time^0-__const_1000^0+curtime^post8 <= 0 /\ wakend^0 <= 0), cost: 4 Applied chaining First rule: l1 -> l8 : ret_time88^0'=curtime^post8, a77^0'=0, __rho_3_^0'=curtime^post8, curtime^0'=curtime^post8, wakend^0 <= 0, cost: 2 Second rule: l8 -> l5 : wakend^0'=1, last_copy_time^0+__const_1000^0-curtime^0 <= 0, cost: 2 New rule: l1 -> l5 : ret_time88^0'=curtime^post8, a77^0'=0, __rho_3_^0'=curtime^post8, wakend^0'=1, curtime^0'=curtime^post8, (last_copy_time^0+__const_1000^0-curtime^post8 <= 0 /\ wakend^0 <= 0), cost: 4 Applied chaining First rule: l1 -> l8 : ret_time88^0'=curtime^post8, last_copy_time^0'=__rho_3_^post10, a77^0'=0, __rho_3_^0'=curtime^post8, ret_time66^0'=__rho_3_^post10, a55^0'=0, wakend^0'=0, curtime^0'=curtime^post8, -1+wakend^0 >= 0, cost: 2 Second rule: l8 -> l5 : 1-last_copy_time^0-__const_1000^0+curtime^0 <= 0, cost: 2 New rule: l1 -> l5 : ret_time88^0'=curtime^post8, last_copy_time^0'=__rho_3_^post10, a77^0'=0, __rho_3_^0'=curtime^post8, ret_time66^0'=__rho_3_^post10, a55^0'=0, wakend^0'=0, curtime^0'=curtime^post8, (1-__const_1000^0-__rho_3_^post10+curtime^post8 <= 0 /\ -1+wakend^0 >= 0), cost: 4 Applied chaining First rule: l1 -> l8 : ret_time88^0'=curtime^post8, last_copy_time^0'=__rho_3_^post10, a77^0'=0, __rho_3_^0'=curtime^post8, ret_time66^0'=__rho_3_^post10, a55^0'=0, wakend^0'=0, curtime^0'=curtime^post8, -1+wakend^0 >= 0, cost: 2 Second rule: l8 -> l5 : wakend^0'=1, last_copy_time^0+__const_1000^0-curtime^0 <= 0, cost: 2 New rule: l1 -> l5 : ret_time88^0'=curtime^post8, last_copy_time^0'=__rho_3_^post10, a77^0'=0, __rho_3_^0'=curtime^post8, ret_time66^0'=__rho_3_^post10, a55^0'=0, wakend^0'=1, curtime^0'=curtime^post8, (__const_1000^0+__rho_3_^post10-curtime^post8 <= 0 /\ -1+wakend^0 >= 0), cost: 4 Applied deletion Removed the following rules: 39 40 41 42 Eliminated locations on tree-shaped paths Start location: l12 45: l1 -> l5 : ret_time88^0'=curtime^post8, a77^0'=0, __rho_3_^0'=curtime^post8, curtime^0'=curtime^post8, (1-last_copy_time^0-__const_1000^0+curtime^post8 <= 0 /\ wakend^0 <= 0), cost: 4 46: l1 -> l5 : ret_time88^0'=curtime^post8, a77^0'=0, __rho_3_^0'=curtime^post8, wakend^0'=1, curtime^0'=curtime^post8, (last_copy_time^0+__const_1000^0-curtime^post8 <= 0 /\ wakend^0 <= 0), cost: 4 47: l1 -> l5 : ret_time88^0'=curtime^post8, last_copy_time^0'=__rho_3_^post10, a77^0'=0, __rho_3_^0'=curtime^post8, ret_time66^0'=__rho_3_^post10, a55^0'=0, wakend^0'=0, curtime^0'=curtime^post8, (1-__const_1000^0-__rho_3_^post10+curtime^post8 <= 0 /\ -1+wakend^0 >= 0), cost: 4 48: l1 -> l5 : ret_time88^0'=curtime^post8, last_copy_time^0'=__rho_3_^post10, a77^0'=0, __rho_3_^0'=curtime^post8, ret_time66^0'=__rho_3_^post10, a55^0'=0, wakend^0'=1, curtime^0'=curtime^post8, (__const_1000^0+__rho_3_^post10-curtime^post8 <= 0 /\ -1+wakend^0 >= 0), cost: 4 36: l5 -> [13] : TRUE, cost: NONTERM 37: l12 -> l1 : got_SIGHUP^0'=__rho_2_^post15, __rho_2_^0'=__rho_2_^post15, wakend^0'=1, __rho_2_^post15 <= 0, cost: 3 43: l12 -> l1 : a33^0'=1, __rho_1_^0'=ret_XLogArchivingActive44^post1, tt1^0'=ret_XLogArchivingActive44^post1, got_SIGHUP^0'=0, tmp2^0'=ret_XLogArchivingActive44^post1, __rho_2_^0'=__rho_2_^post15, wakend^0'=1, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, (-1+ret_XLogArchivingActive44^post1 >= 0 /\ -1+__rho_2_^post15 >= 0), cost: 4 44: l12 -> l5 : a33^0'=1, __rho_1_^0'=ret_XLogArchivingActive44^post1, tt1^0'=ret_XLogArchivingActive44^post1, got_SIGHUP^0'=0, tmp2^0'=ret_XLogArchivingActive44^post1, __rho_2_^0'=__rho_2_^post15, wakend^0'=1, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, (-1+__rho_2_^post15 >= 0 /\ ret_XLogArchivingActive44^post1 <= 0), cost: 4 Eliminating location l1 by chaining: Applied chaining First rule: l12 -> l1 : got_SIGHUP^0'=__rho_2_^post15, __rho_2_^0'=__rho_2_^post15, wakend^0'=1, __rho_2_^post15 <= 0, cost: 3 Second rule: l1 -> l5 : ret_time88^0'=curtime^post8, last_copy_time^0'=__rho_3_^post10, a77^0'=0, __rho_3_^0'=curtime^post8, ret_time66^0'=__rho_3_^post10, a55^0'=0, wakend^0'=0, curtime^0'=curtime^post8, (1-__const_1000^0-__rho_3_^post10+curtime^post8 <= 0 /\ -1+wakend^0 >= 0), cost: 4 New rule: l12 -> l5 : ret_time88^0'=curtime^post8, last_copy_time^0'=__rho_3_^post10, a77^0'=0, __rho_3_^0'=curtime^post8, ret_time66^0'=__rho_3_^post10, got_SIGHUP^0'=__rho_2_^post15, a55^0'=0, __rho_2_^0'=__rho_2_^post15, wakend^0'=0, curtime^0'=curtime^post8, (0 >= 0 /\ 1-__const_1000^0-__rho_3_^post10+curtime^post8 <= 0 /\ __rho_2_^post15 <= 0), cost: 7 Applied simplification Original rule: l12 -> l5 : ret_time88^0'=curtime^post8, last_copy_time^0'=__rho_3_^post10, a77^0'=0, __rho_3_^0'=curtime^post8, ret_time66^0'=__rho_3_^post10, got_SIGHUP^0'=__rho_2_^post15, a55^0'=0, __rho_2_^0'=__rho_2_^post15, wakend^0'=0, curtime^0'=curtime^post8, (0 >= 0 /\ 1-__const_1000^0-__rho_3_^post10+curtime^post8 <= 0 /\ __rho_2_^post15 <= 0), cost: 7 New rule: l12 -> l5 : ret_time88^0'=curtime^post8, last_copy_time^0'=__rho_3_^post10, a77^0'=0, __rho_3_^0'=curtime^post8, ret_time66^0'=__rho_3_^post10, got_SIGHUP^0'=__rho_2_^post15, a55^0'=0, __rho_2_^0'=__rho_2_^post15, wakend^0'=0, curtime^0'=curtime^post8, (1-__const_1000^0-__rho_3_^post10+curtime^post8 <= 0 /\ __rho_2_^post15 <= 0), cost: 7 Applied chaining First rule: l12 -> l1 : got_SIGHUP^0'=__rho_2_^post15, __rho_2_^0'=__rho_2_^post15, wakend^0'=1, __rho_2_^post15 <= 0, cost: 3 Second rule: l1 -> l5 : ret_time88^0'=curtime^post8, last_copy_time^0'=__rho_3_^post10, a77^0'=0, __rho_3_^0'=curtime^post8, ret_time66^0'=__rho_3_^post10, a55^0'=0, wakend^0'=1, curtime^0'=curtime^post8, (__const_1000^0+__rho_3_^post10-curtime^post8 <= 0 /\ -1+wakend^0 >= 0), cost: 4 New rule: l12 -> l5 : ret_time88^0'=curtime^post8, last_copy_time^0'=__rho_3_^post10, a77^0'=0, __rho_3_^0'=curtime^post8, ret_time66^0'=__rho_3_^post10, got_SIGHUP^0'=__rho_2_^post15, a55^0'=0, __rho_2_^0'=__rho_2_^post15, wakend^0'=1, curtime^0'=curtime^post8, (0 >= 0 /\ __const_1000^0+__rho_3_^post10-curtime^post8 <= 0 /\ __rho_2_^post15 <= 0), cost: 7 Applied simplification Original rule: l12 -> l5 : ret_time88^0'=curtime^post8, last_copy_time^0'=__rho_3_^post10, a77^0'=0, __rho_3_^0'=curtime^post8, ret_time66^0'=__rho_3_^post10, got_SIGHUP^0'=__rho_2_^post15, a55^0'=0, __rho_2_^0'=__rho_2_^post15, wakend^0'=1, curtime^0'=curtime^post8, (0 >= 0 /\ __const_1000^0+__rho_3_^post10-curtime^post8 <= 0 /\ __rho_2_^post15 <= 0), cost: 7 New rule: l12 -> l5 : ret_time88^0'=curtime^post8, last_copy_time^0'=__rho_3_^post10, a77^0'=0, __rho_3_^0'=curtime^post8, ret_time66^0'=__rho_3_^post10, got_SIGHUP^0'=__rho_2_^post15, a55^0'=0, __rho_2_^0'=__rho_2_^post15, wakend^0'=1, curtime^0'=curtime^post8, (__const_1000^0+__rho_3_^post10-curtime^post8 <= 0 /\ __rho_2_^post15 <= 0), cost: 7 Applied chaining First rule: l12 -> l1 : a33^0'=1, __rho_1_^0'=ret_XLogArchivingActive44^post1, tt1^0'=ret_XLogArchivingActive44^post1, got_SIGHUP^0'=0, tmp2^0'=ret_XLogArchivingActive44^post1, __rho_2_^0'=__rho_2_^post15, wakend^0'=1, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, (-1+ret_XLogArchivingActive44^post1 >= 0 /\ -1+__rho_2_^post15 >= 0), cost: 4 Second rule: l1 -> l5 : ret_time88^0'=curtime^post8, last_copy_time^0'=__rho_3_^post10, a77^0'=0, __rho_3_^0'=curtime^post8, ret_time66^0'=__rho_3_^post10, a55^0'=0, wakend^0'=0, curtime^0'=curtime^post8, (1-__const_1000^0-__rho_3_^post10+curtime^post8 <= 0 /\ -1+wakend^0 >= 0), cost: 4 New rule: l12 -> l5 : a33^0'=1, ret_time88^0'=curtime^post8, __rho_1_^0'=ret_XLogArchivingActive44^post1, tt1^0'=ret_XLogArchivingActive44^post1, last_copy_time^0'=__rho_3_^post10, a77^0'=0, __rho_3_^0'=curtime^post8, ret_time66^0'=__rho_3_^post10, got_SIGHUP^0'=0, a55^0'=0, tmp2^0'=ret_XLogArchivingActive44^post1, __rho_2_^0'=__rho_2_^post15, wakend^0'=0, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, curtime^0'=curtime^post8, (0 >= 0 /\ 1-__const_1000^0-__rho_3_^post10+curtime^post8 <= 0 /\ -1+ret_XLogArchivingActive44^post1 >= 0 /\ -1+__rho_2_^post15 >= 0), cost: 8 Applied simplification Original rule: l12 -> l5 : a33^0'=1, ret_time88^0'=curtime^post8, __rho_1_^0'=ret_XLogArchivingActive44^post1, tt1^0'=ret_XLogArchivingActive44^post1, last_copy_time^0'=__rho_3_^post10, a77^0'=0, __rho_3_^0'=curtime^post8, ret_time66^0'=__rho_3_^post10, got_SIGHUP^0'=0, a55^0'=0, tmp2^0'=ret_XLogArchivingActive44^post1, __rho_2_^0'=__rho_2_^post15, wakend^0'=0, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, curtime^0'=curtime^post8, (0 >= 0 /\ 1-__const_1000^0-__rho_3_^post10+curtime^post8 <= 0 /\ -1+ret_XLogArchivingActive44^post1 >= 0 /\ -1+__rho_2_^post15 >= 0), cost: 8 New rule: l12 -> l5 : a33^0'=1, ret_time88^0'=curtime^post8, __rho_1_^0'=ret_XLogArchivingActive44^post1, tt1^0'=ret_XLogArchivingActive44^post1, last_copy_time^0'=__rho_3_^post10, a77^0'=0, __rho_3_^0'=curtime^post8, ret_time66^0'=__rho_3_^post10, got_SIGHUP^0'=0, a55^0'=0, tmp2^0'=ret_XLogArchivingActive44^post1, __rho_2_^0'=__rho_2_^post15, wakend^0'=0, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, curtime^0'=curtime^post8, (1-__const_1000^0-__rho_3_^post10+curtime^post8 <= 0 /\ -1+ret_XLogArchivingActive44^post1 >= 0 /\ -1+__rho_2_^post15 >= 0), cost: 8 Applied chaining First rule: l12 -> l1 : a33^0'=1, __rho_1_^0'=ret_XLogArchivingActive44^post1, tt1^0'=ret_XLogArchivingActive44^post1, got_SIGHUP^0'=0, tmp2^0'=ret_XLogArchivingActive44^post1, __rho_2_^0'=__rho_2_^post15, wakend^0'=1, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, (-1+ret_XLogArchivingActive44^post1 >= 0 /\ -1+__rho_2_^post15 >= 0), cost: 4 Second rule: l1 -> l5 : ret_time88^0'=curtime^post8, last_copy_time^0'=__rho_3_^post10, a77^0'=0, __rho_3_^0'=curtime^post8, ret_time66^0'=__rho_3_^post10, a55^0'=0, wakend^0'=1, curtime^0'=curtime^post8, (__const_1000^0+__rho_3_^post10-curtime^post8 <= 0 /\ -1+wakend^0 >= 0), cost: 4 New rule: l12 -> l5 : a33^0'=1, ret_time88^0'=curtime^post8, __rho_1_^0'=ret_XLogArchivingActive44^post1, tt1^0'=ret_XLogArchivingActive44^post1, last_copy_time^0'=__rho_3_^post10, a77^0'=0, __rho_3_^0'=curtime^post8, ret_time66^0'=__rho_3_^post10, got_SIGHUP^0'=0, a55^0'=0, tmp2^0'=ret_XLogArchivingActive44^post1, __rho_2_^0'=__rho_2_^post15, wakend^0'=1, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, curtime^0'=curtime^post8, (0 >= 0 /\ -1+ret_XLogArchivingActive44^post1 >= 0 /\ __const_1000^0+__rho_3_^post10-curtime^post8 <= 0 /\ -1+__rho_2_^post15 >= 0), cost: 8 Applied simplification Original rule: l12 -> l5 : a33^0'=1, ret_time88^0'=curtime^post8, __rho_1_^0'=ret_XLogArchivingActive44^post1, tt1^0'=ret_XLogArchivingActive44^post1, last_copy_time^0'=__rho_3_^post10, a77^0'=0, __rho_3_^0'=curtime^post8, ret_time66^0'=__rho_3_^post10, got_SIGHUP^0'=0, a55^0'=0, tmp2^0'=ret_XLogArchivingActive44^post1, __rho_2_^0'=__rho_2_^post15, wakend^0'=1, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, curtime^0'=curtime^post8, (0 >= 0 /\ -1+ret_XLogArchivingActive44^post1 >= 0 /\ __const_1000^0+__rho_3_^post10-curtime^post8 <= 0 /\ -1+__rho_2_^post15 >= 0), cost: 8 New rule: l12 -> l5 : a33^0'=1, ret_time88^0'=curtime^post8, __rho_1_^0'=ret_XLogArchivingActive44^post1, tt1^0'=ret_XLogArchivingActive44^post1, last_copy_time^0'=__rho_3_^post10, a77^0'=0, __rho_3_^0'=curtime^post8, ret_time66^0'=__rho_3_^post10, got_SIGHUP^0'=0, a55^0'=0, tmp2^0'=ret_XLogArchivingActive44^post1, __rho_2_^0'=__rho_2_^post15, wakend^0'=1, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, curtime^0'=curtime^post8, (-1+ret_XLogArchivingActive44^post1 >= 0 /\ __const_1000^0+__rho_3_^post10-curtime^post8 <= 0 /\ -1+__rho_2_^post15 >= 0), cost: 8 Applied deletion Removed the following rules: 37 43 45 46 47 48 Eliminating location l5 by chaining: Applied chaining First rule: l12 -> l5 : a33^0'=1, __rho_1_^0'=ret_XLogArchivingActive44^post1, tt1^0'=ret_XLogArchivingActive44^post1, got_SIGHUP^0'=0, tmp2^0'=ret_XLogArchivingActive44^post1, __rho_2_^0'=__rho_2_^post15, wakend^0'=1, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, (-1+__rho_2_^post15 >= 0 /\ ret_XLogArchivingActive44^post1 <= 0), cost: 4 Second rule: l5 -> [13] : TRUE, cost: NONTERM New rule: l12 -> [13] : (-1+__rho_2_^post15 >= 0 /\ ret_XLogArchivingActive44^post1 <= 0), cost: NONTERM Applied chaining First rule: l12 -> l5 : ret_time88^0'=curtime^post8, last_copy_time^0'=__rho_3_^post10, a77^0'=0, __rho_3_^0'=curtime^post8, ret_time66^0'=__rho_3_^post10, got_SIGHUP^0'=__rho_2_^post15, a55^0'=0, __rho_2_^0'=__rho_2_^post15, wakend^0'=0, curtime^0'=curtime^post8, (1-__const_1000^0-__rho_3_^post10+curtime^post8 <= 0 /\ __rho_2_^post15 <= 0), cost: 7 Second rule: l5 -> [13] : TRUE, cost: NONTERM New rule: l12 -> [13] : (1-__const_1000^0-__rho_3_^post10+curtime^post8 <= 0 /\ __rho_2_^post15 <= 0), cost: NONTERM Applied chaining First rule: l12 -> l5 : ret_time88^0'=curtime^post8, last_copy_time^0'=__rho_3_^post10, a77^0'=0, __rho_3_^0'=curtime^post8, ret_time66^0'=__rho_3_^post10, got_SIGHUP^0'=__rho_2_^post15, a55^0'=0, __rho_2_^0'=__rho_2_^post15, wakend^0'=1, curtime^0'=curtime^post8, (__const_1000^0+__rho_3_^post10-curtime^post8 <= 0 /\ __rho_2_^post15 <= 0), cost: 7 Second rule: l5 -> [13] : TRUE, cost: NONTERM New rule: l12 -> [13] : (__const_1000^0+__rho_3_^post10-curtime^post8 <= 0 /\ __rho_2_^post15 <= 0), cost: NONTERM Applied chaining First rule: l12 -> l5 : a33^0'=1, ret_time88^0'=curtime^post8, __rho_1_^0'=ret_XLogArchivingActive44^post1, tt1^0'=ret_XLogArchivingActive44^post1, last_copy_time^0'=__rho_3_^post10, a77^0'=0, __rho_3_^0'=curtime^post8, ret_time66^0'=__rho_3_^post10, got_SIGHUP^0'=0, a55^0'=0, tmp2^0'=ret_XLogArchivingActive44^post1, __rho_2_^0'=__rho_2_^post15, wakend^0'=0, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, curtime^0'=curtime^post8, (1-__const_1000^0-__rho_3_^post10+curtime^post8 <= 0 /\ -1+ret_XLogArchivingActive44^post1 >= 0 /\ -1+__rho_2_^post15 >= 0), cost: 8 Second rule: l5 -> [13] : TRUE, cost: NONTERM New rule: l12 -> [13] : (1-__const_1000^0-__rho_3_^post10+curtime^post8 <= 0 /\ -1+ret_XLogArchivingActive44^post1 >= 0 /\ -1+__rho_2_^post15 >= 0), cost: NONTERM Applied chaining First rule: l12 -> l5 : a33^0'=1, ret_time88^0'=curtime^post8, __rho_1_^0'=ret_XLogArchivingActive44^post1, tt1^0'=ret_XLogArchivingActive44^post1, last_copy_time^0'=__rho_3_^post10, a77^0'=0, __rho_3_^0'=curtime^post8, ret_time66^0'=__rho_3_^post10, got_SIGHUP^0'=0, a55^0'=0, tmp2^0'=ret_XLogArchivingActive44^post1, __rho_2_^0'=__rho_2_^post15, wakend^0'=1, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, curtime^0'=curtime^post8, (-1+ret_XLogArchivingActive44^post1 >= 0 /\ __const_1000^0+__rho_3_^post10-curtime^post8 <= 0 /\ -1+__rho_2_^post15 >= 0), cost: 8 Second rule: l5 -> [13] : TRUE, cost: NONTERM New rule: l12 -> [13] : (-1+ret_XLogArchivingActive44^post1 >= 0 /\ __const_1000^0+__rho_3_^post10-curtime^post8 <= 0 /\ -1+__rho_2_^post15 >= 0), cost: NONTERM Applied deletion Removed the following rules: 36 44 49 50 51 52 Eliminated locations on tree-shaped paths Start location: l12 53: l12 -> [13] : (-1+__rho_2_^post15 >= 0 /\ ret_XLogArchivingActive44^post1 <= 0), cost: NONTERM 54: l12 -> [13] : (1-__const_1000^0-__rho_3_^post10+curtime^post8 <= 0 /\ __rho_2_^post15 <= 0), cost: NONTERM 55: l12 -> [13] : (__const_1000^0+__rho_3_^post10-curtime^post8 <= 0 /\ __rho_2_^post15 <= 0), cost: NONTERM 56: l12 -> [13] : (1-__const_1000^0-__rho_3_^post10+curtime^post8 <= 0 /\ -1+ret_XLogArchivingActive44^post1 >= 0 /\ -1+__rho_2_^post15 >= 0), cost: NONTERM 57: l12 -> [13] : (-1+ret_XLogArchivingActive44^post1 >= 0 /\ __const_1000^0+__rho_3_^post10-curtime^post8 <= 0 /\ -1+__rho_2_^post15 >= 0), cost: NONTERM Computing asymptotic complexity Proved nontermination of rule 53 via SMT. Proved the following lower bound Complexity: Nonterm Cpx degree: Nonterm Solved cost: NONTERM Rule cost: NONTERM Rule guard: (-1+__rho_2_^post15 >= 0 /\ ret_XLogArchivingActive44^post1 <= 0)