NO

Initial ITS
Start location: l12
   0: l0 -> l1 : curtime^0'=curtime^post0, tmp99^0'=tmp99^post0, a33^0'=a33^post0, wakend^0'=wakend^post0, ret_time77^0'=ret_time77^post0, last_copy_time^0'=last_copy_time^post0, a88^0'=a88^post0, tmp66^0'=tmp66^post0, ___rho_1_^0'=___rho_1_^post0, ret_time1010^0'=ret_time1010^post0, got_SIGHUP^0'=got_SIGHUP^post0, tt1^0'=tt1^post0, a55^0'=a55^post0, tmp2^0'=tmp2^post0, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post0, (-last_copy_time^post0+last_copy_time^0 == 0 /\ -tt1^post0+tt1^0 == 0 /\ -___rho_1_^post0+___rho_1_^0 == 0 /\ -a55^post0+a55^0 == 0 /\ ret_time1010^0-ret_time1010^post0 == 0 /\ tmp99^0-tmp99^post0 == 0 /\ wakend^0-wakend^post0 == 0 /\ a33^0-a33^post0 == 0 /\ ret_time77^0-ret_time77^post0 == 0 /\ got_SIGHUP^0 <= 0 /\ -curtime^post0+curtime^0 == 0 /\ -tmp2^post0+tmp2^0 == 0 /\ a88^0-a88^post0 == 0 /\ -ret_XLogArchivingActive44^post0+ret_XLogArchivingActive44^0 == 0 /\ -got_SIGHUP^post0+got_SIGHUP^0 == 0 /\ -tmp66^post0+tmp66^0 == 0), cost: 1
   1: l0 -> l2 : curtime^0'=curtime^post1, tmp99^0'=tmp99^post1, a33^0'=a33^post1, wakend^0'=wakend^post1, ret_time77^0'=ret_time77^post1, last_copy_time^0'=last_copy_time^post1, a88^0'=a88^post1, tmp66^0'=tmp66^post1, ___rho_1_^0'=___rho_1_^post1, ret_time1010^0'=ret_time1010^post1, got_SIGHUP^0'=got_SIGHUP^post1, tt1^0'=tt1^post1, a55^0'=a55^post1, tmp2^0'=tmp2^post1, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, (0 == 0 /\ -tmp2^post1+tt1^post1 == 0 /\ ret_time77^0-ret_time77^post1 == 0 /\ -last_copy_time^post1+last_copy_time^0 == 0 /\ curtime^0-curtime^post1 == 0 /\ -1+a33^post1 == 0 /\ a88^0-a88^post1 == 0 /\ -a55^post1+a55^0 == 0 /\ 1-got_SIGHUP^0 <= 0 /\ tmp66^0-tmp66^post1 == 0 /\ -tmp99^post1+tmp99^0 == 0 /\ -ret_time1010^post1+ret_time1010^0 == 0 /\ -___rho_1_^post1+ret_XLogArchivingActive44^post1 == 0 /\ got_SIGHUP^post1 == 0 /\ tmp2^post1-ret_XLogArchivingActive44^post1 == 0 /\ wakend^0-wakend^post1 == 0), cost: 1
   9: l1 -> l9 : curtime^0'=curtime^post9, tmp99^0'=tmp99^post9, a33^0'=a33^post9, wakend^0'=wakend^post9, ret_time77^0'=ret_time77^post9, last_copy_time^0'=last_copy_time^post9, a88^0'=a88^post9, tmp66^0'=tmp66^post9, ___rho_1_^0'=___rho_1_^post9, ret_time1010^0'=ret_time1010^post9, got_SIGHUP^0'=got_SIGHUP^post9, tt1^0'=tt1^post9, a55^0'=a55^post9, tmp2^0'=tmp2^post9, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post9, (-wakend^post9+wakend^0 == 0 /\ a88^0-a88^post9 == 0 /\ wakend^0 <= 0 /\ -tt1^post9+tt1^0 == 0 /\ -___rho_1_^post9+___rho_1_^0 == 0 /\ tmp99^0-tmp99^post9 == 0 /\ ret_time77^0-ret_time77^post9 == 0 /\ -tmp2^post9+tmp2^0 == 0 /\ -ret_XLogArchivingActive44^post9+ret_XLogArchivingActive44^0 == 0 /\ -a55^post9+a55^0 == 0 /\ got_SIGHUP^0-got_SIGHUP^post9 == 0 /\ a33^0-a33^post9 == 0 /\ tmp66^0-tmp66^post9 == 0 /\ last_copy_time^0-last_copy_time^post9 == 0 /\ curtime^0-curtime^post9 == 0 /\ -ret_time1010^post9+ret_time1010^0 == 0), cost: 1
  10: l1 -> l9 : curtime^0'=curtime^post10, tmp99^0'=tmp99^post10, a33^0'=a33^post10, wakend^0'=wakend^post10, ret_time77^0'=ret_time77^post10, last_copy_time^0'=last_copy_time^post10, a88^0'=a88^post10, tmp66^0'=tmp66^post10, ___rho_1_^0'=___rho_1_^post10, ret_time1010^0'=ret_time1010^post10, got_SIGHUP^0'=got_SIGHUP^post10, tt1^0'=tt1^post10, a55^0'=a55^post10, tmp2^0'=tmp2^post10, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post10, (0 == 0 /\ -tt1^post10+tt1^0 == 0 /\ curtime^0-curtime^post10 == 0 /\ ret_time77^post10-tmp66^post10 == 0 /\ -ret_XLogArchivingActive44^post10+ret_XLogArchivingActive44^0 == 0 /\ a55^post10 == 0 /\ -tmp2^post10+tmp2^0 == 0 /\ 1-wakend^0 <= 0 /\ -a33^post10+a33^0 == 0 /\ tmp99^0-tmp99^post10 == 0 /\ ___rho_1_^0-___rho_1_^post10 == 0 /\ -ret_time77^post10+last_copy_time^post10 == 0 /\ -ret_time1010^post10+ret_time1010^0 == 0 /\ -a88^post10+a88^0 == 0 /\ wakend^post10 == 0 /\ -got_SIGHUP^post10+got_SIGHUP^0 == 0), cost: 1
  13: l2 -> l1 : curtime^0'=curtime^post13, tmp99^0'=tmp99^post13, a33^0'=a33^post13, wakend^0'=wakend^post13, ret_time77^0'=ret_time77^post13, last_copy_time^0'=last_copy_time^post13, a88^0'=a88^post13, tmp66^0'=tmp66^post13, ___rho_1_^0'=___rho_1_^post13, ret_time1010^0'=ret_time1010^post13, got_SIGHUP^0'=got_SIGHUP^post13, tt1^0'=tt1^post13, a55^0'=a55^post13, tmp2^0'=tmp2^post13, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post13, (last_copy_time^0-last_copy_time^post13 == 0 /\ curtime^0-curtime^post13 == 0 /\ ___rho_1_^0-___rho_1_^post13 == 0 /\ -a55^post13+a55^0 == 0 /\ -ret_time77^post13+ret_time77^0 == 0 /\ -got_SIGHUP^post13+got_SIGHUP^0 == 0 /\ 1-tt1^0 <= 0 /\ -a88^post13+a88^0 == 0 /\ -ret_time1010^post13+ret_time1010^0 == 0 /\ tt1^0-tt1^post13 == 0 /\ -tmp2^post13+tmp2^0 == 0 /\ -ret_XLogArchivingActive44^post13+ret_XLogArchivingActive44^0 == 0 /\ tmp99^0-tmp99^post13 == 0 /\ wakend^0-wakend^post13 == 0 /\ a33^0-a33^post13 == 0 /\ -tmp66^post13+tmp66^0 == 0), cost: 1
  14: l2 -> l5 : curtime^0'=curtime^post14, tmp99^0'=tmp99^post14, a33^0'=a33^post14, wakend^0'=wakend^post14, ret_time77^0'=ret_time77^post14, last_copy_time^0'=last_copy_time^post14, a88^0'=a88^post14, tmp66^0'=tmp66^post14, ___rho_1_^0'=___rho_1_^post14, ret_time1010^0'=ret_time1010^post14, got_SIGHUP^0'=got_SIGHUP^post14, tt1^0'=tt1^post14, a55^0'=a55^post14, tmp2^0'=tmp2^post14, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post14, (-last_copy_time^post14+last_copy_time^0 == 0 /\ -a55^post14+a55^0 == 0 /\ ret_time1010^0-ret_time1010^post14 == 0 /\ tmp99^0-tmp99^post14 == 0 /\ wakend^0-wakend^post14 == 0 /\ a33^0-a33^post14 == 0 /\ ret_time77^0-ret_time77^post14 == 0 /\ curtime^0-curtime^post14 == 0 /\ tt1^0 <= 0 /\ -___rho_1_^post14+___rho_1_^0 == 0 /\ -ret_XLogArchivingActive44^post14+ret_XLogArchivingActive44^0 == 0 /\ -tmp2^post14+tmp2^0 == 0 /\ a88^0-a88^post14 == 0 /\ -tt1^post14+tt1^0 == 0 /\ -got_SIGHUP^post14+got_SIGHUP^0 == 0 /\ -tmp66^post14+tmp66^0 == 0), cost: 1
   2: l3 -> l4 : curtime^0'=curtime^post2, tmp99^0'=tmp99^post2, a33^0'=a33^post2, wakend^0'=wakend^post2, ret_time77^0'=ret_time77^post2, last_copy_time^0'=last_copy_time^post2, a88^0'=a88^post2, tmp66^0'=tmp66^post2, ___rho_1_^0'=___rho_1_^post2, ret_time1010^0'=ret_time1010^post2, got_SIGHUP^0'=got_SIGHUP^post2, tt1^0'=tt1^post2, a55^0'=a55^post2, tmp2^0'=tmp2^post2, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post2, (-got_SIGHUP^post2+got_SIGHUP^0 == 0 /\ last_copy_time^0-last_copy_time^post2 == 0 /\ ___rho_1_^0-___rho_1_^post2 == 0 /\ curtime^0-curtime^post2 == 0 /\ -ret_time77^post2+ret_time77^0 == 0 /\ -tmp2^post2+tmp2^0 == 0 /\ -tt1^post2+tt1^0 == 0 /\ -a88^post2+a88^0 == 0 /\ -ret_time1010^post2+ret_time1010^0 == 0 /\ -a55^post2+a55^0 == 0 /\ -ret_XLogArchivingActive44^post2+ret_XLogArchivingActive44^0 == 0 /\ -tmp66^post2+tmp66^0 == 0 /\ a33^0-a33^post2 == 0 /\ tmp99^0-tmp99^post2 == 0 /\ wakend^0-wakend^post2 == 0), cost: 1
   3: l5 -> l6 : curtime^0'=curtime^post3, tmp99^0'=tmp99^post3, a33^0'=a33^post3, wakend^0'=wakend^post3, ret_time77^0'=ret_time77^post3, last_copy_time^0'=last_copy_time^post3, a88^0'=a88^post3, tmp66^0'=tmp66^post3, ___rho_1_^0'=___rho_1_^post3, ret_time1010^0'=ret_time1010^post3, got_SIGHUP^0'=got_SIGHUP^post3, tt1^0'=tt1^post3, a55^0'=a55^post3, tmp2^0'=tmp2^post3, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post3, (-got_SIGHUP^post3+got_SIGHUP^0 == 0 /\ -last_copy_time^post3+last_copy_time^0 == 0 /\ -tmp2^post3+tmp2^0 == 0 /\ -ret_XLogArchivingActive44^post3+ret_XLogArchivingActive44^0 == 0 /\ -a55^post3+a55^0 == 0 /\ ret_time1010^0-ret_time1010^post3 == 0 /\ a33^0-a33^post3 == 0 /\ tmp99^0-tmp99^post3 == 0 /\ -tt1^post3+tt1^0 == 0 /\ wakend^0-wakend^post3 == 0 /\ ret_time77^0-ret_time77^post3 == 0 /\ curtime^0-curtime^post3 == 0 /\ -___rho_1_^post3+___rho_1_^0 == 0 /\ -tmp66^post3+tmp66^0 == 0 /\ a88^0-a88^post3 == 0), cost: 1
  11: l6 -> l10 : curtime^0'=curtime^post11, tmp99^0'=tmp99^post11, a33^0'=a33^post11, wakend^0'=wakend^post11, ret_time77^0'=ret_time77^post11, last_copy_time^0'=last_copy_time^post11, a88^0'=a88^post11, tmp66^0'=tmp66^post11, ___rho_1_^0'=___rho_1_^post11, ret_time1010^0'=ret_time1010^post11, got_SIGHUP^0'=got_SIGHUP^post11, tt1^0'=tt1^post11, a55^0'=a55^post11, tmp2^0'=tmp2^post11, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post11, (-tt1^post11+tt1^0 == 0 /\ -1+wakend^post11 == 0 /\ -___rho_1_^post11+___rho_1_^0 == 0 /\ a33^0-a33^post11 == 0 /\ -tmp2^post11+tmp2^0 == 0 /\ -ret_XLogArchivingActive44^post11+ret_XLogArchivingActive44^0 == 0 /\ a55^0-a55^post11 == 0 /\ ret_time1010^0-ret_time1010^post11 == 0 /\ -tmp66^post11+tmp66^0 == 0 /\ curtime^0-curtime^post11 == 0 /\ -last_copy_time^post11+last_copy_time^0 == 0 /\ a88^0-a88^post11 == 0 /\ tmp99^0-tmp99^post11 == 0 /\ ret_time77^0-ret_time77^post11 == 0 /\ -got_SIGHUP^post11+got_SIGHUP^0 == 0), cost: 1
   4: l7 -> l5 : curtime^0'=curtime^post4, tmp99^0'=tmp99^post4, a33^0'=a33^post4, wakend^0'=wakend^post4, ret_time77^0'=ret_time77^post4, last_copy_time^0'=last_copy_time^post4, a88^0'=a88^post4, tmp66^0'=tmp66^post4, ___rho_1_^0'=___rho_1_^post4, ret_time1010^0'=ret_time1010^post4, got_SIGHUP^0'=got_SIGHUP^post4, tt1^0'=tt1^post4, a55^0'=a55^post4, tmp2^0'=tmp2^post4, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post4, (-ret_time1010^post4+ret_time1010^0 == 0 /\ -ret_XLogArchivingActive44^post4+ret_XLogArchivingActive44^0 == 0 /\ -tmp2^post4+tmp2^0 == 0 /\ -a55^post4+a55^0 == 0 /\ tmp99^0-tmp99^post4 == 0 /\ -a88^post4+a88^0 == 0 /\ tmp66^0-tmp66^post4 == 0 /\ last_copy_time^0-last_copy_time^post4 == 0 /\ ___rho_1_^0-___rho_1_^post4 == 0 /\ ret_time77^0-ret_time77^post4 == 0 /\ -wakend^post4+wakend^0 == 0 /\ -got_SIGHUP^post4+got_SIGHUP^0 == 0 /\ -a33^post4+a33^0 == 0 /\ tt1^0-tt1^post4 == 0 /\ curtime^0-curtime^post4 == 0), cost: 1
   5: l8 -> l7 : curtime^0'=curtime^post5, tmp99^0'=tmp99^post5, a33^0'=a33^post5, wakend^0'=wakend^post5, ret_time77^0'=ret_time77^post5, last_copy_time^0'=last_copy_time^post5, a88^0'=a88^post5, tmp66^0'=tmp66^post5, ___rho_1_^0'=___rho_1_^post5, ret_time1010^0'=ret_time1010^post5, got_SIGHUP^0'=got_SIGHUP^post5, tt1^0'=tt1^post5, a55^0'=a55^post5, tmp2^0'=tmp2^post5, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post5, (ret_time1010^0-ret_time1010^post5 == 0 /\ tmp99^0-tmp99^post5 == 0 /\ -ret_XLogArchivingActive44^post5+ret_XLogArchivingActive44^0 == 0 /\ -a88^post5+a88^0 == 0 /\ -ret_time77^post5+ret_time77^0 == 0 /\ -tmp66^post5+tmp66^0 == 0 /\ -999+curtime^0-last_copy_time^0 <= 0 /\ curtime^0-curtime^post5 == 0 /\ a33^0-a33^post5 == 0 /\ -tmp2^post5+tmp2^0 == 0 /\ -got_SIGHUP^post5+got_SIGHUP^0 == 0 /\ -tt1^post5+tt1^0 == 0 /\ wakend^0-wakend^post5 == 0 /\ ___rho_1_^0-___rho_1_^post5 == 0 /\ last_copy_time^0-last_copy_time^post5 == 0 /\ -a55^post5+a55^0 == 0), cost: 1
   6: l8 -> l7 : curtime^0'=curtime^post6, tmp99^0'=tmp99^post6, a33^0'=a33^post6, wakend^0'=wakend^post6, ret_time77^0'=ret_time77^post6, last_copy_time^0'=last_copy_time^post6, a88^0'=a88^post6, tmp66^0'=tmp66^post6, ___rho_1_^0'=___rho_1_^post6, ret_time1010^0'=ret_time1010^post6, got_SIGHUP^0'=got_SIGHUP^post6, tt1^0'=tt1^post6, a55^0'=a55^post6, tmp2^0'=tmp2^post6, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post6, (a88^0-a88^post6 == 0 /\ curtime^0-curtime^post6 == 0 /\ -___rho_1_^post6+___rho_1_^0 == 0 /\ -ret_XLogArchivingActive44^post6+ret_XLogArchivingActive44^0 == 0 /\ -tt1^post6+tt1^0 == 0 /\ ret_time77^0-ret_time77^post6 == 0 /\ -1+wakend^post6 == 0 /\ a55^0-a55^post6 == 0 /\ tmp99^0-tmp99^post6 == 0 /\ -tmp2^post6+tmp2^0 == 0 /\ 1000-curtime^0+last_copy_time^0 <= 0 /\ tmp66^0-tmp66^post6 == 0 /\ got_SIGHUP^0-got_SIGHUP^post6 == 0 /\ a33^0-a33^post6 == 0 /\ last_copy_time^0-last_copy_time^post6 == 0 /\ -ret_time1010^post6+ret_time1010^0 == 0), cost: 1
   7: l9 -> l7 : curtime^0'=curtime^post7, tmp99^0'=tmp99^post7, a33^0'=a33^post7, wakend^0'=wakend^post7, ret_time77^0'=ret_time77^post7, last_copy_time^0'=last_copy_time^post7, a88^0'=a88^post7, tmp66^0'=tmp66^post7, ___rho_1_^0'=___rho_1_^post7, ret_time1010^0'=ret_time1010^post7, got_SIGHUP^0'=got_SIGHUP^post7, tt1^0'=tt1^post7, a55^0'=a55^post7, tmp2^0'=tmp2^post7, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post7, (-ret_XLogArchivingActive44^post7+ret_XLogArchivingActive44^0 == 0 /\ curtime^0-curtime^post7 == 0 /\ tmp66^0-tmp66^post7 == 0 /\ -a88^post7+a88^0 == 0 /\ ___rho_1_^0-___rho_1_^post7 == 0 /\ last_copy_time^0-last_copy_time^post7 == 0 /\ tmp99^0-tmp99^post7 == 0 /\ -tmp2^post7+tmp2^0 == 0 /\ -a55^post7+a55^0 == 0 /\ 1-wakend^0 <= 0 /\ tt1^0-tt1^post7 == 0 /\ -wakend^post7+wakend^0 == 0 /\ a33^0-a33^post7 == 0 /\ -got_SIGHUP^post7+got_SIGHUP^0 == 0 /\ -ret_time1010^post7+ret_time1010^0 == 0 /\ ret_time77^0-ret_time77^post7 == 0), cost: 1
   8: l9 -> l8 : curtime^0'=curtime^post8, tmp99^0'=tmp99^post8, a33^0'=a33^post8, wakend^0'=wakend^post8, ret_time77^0'=ret_time77^post8, last_copy_time^0'=last_copy_time^post8, a88^0'=a88^post8, tmp66^0'=tmp66^post8, ___rho_1_^0'=___rho_1_^post8, ret_time1010^0'=ret_time1010^post8, got_SIGHUP^0'=got_SIGHUP^post8, tt1^0'=tt1^post8, a55^0'=a55^post8, tmp2^0'=tmp2^post8, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post8, (0 == 0 /\ -ret_XLogArchivingActive44^post8+ret_XLogArchivingActive44^0 == 0 /\ -tt1^post8+tt1^0 == 0 /\ wakend^0 <= 0 /\ -___rho_1_^post8+___rho_1_^0 == 0 /\ a33^0-a33^post8 == 0 /\ wakend^0-wakend^post8 == 0 /\ -last_copy_time^post8+last_copy_time^0 == 0 /\ curtime^post8-ret_time1010^post8 == 0 /\ -tmp2^post8+tmp2^0 == 0 /\ -tmp66^post8+tmp66^0 == 0 /\ -ret_time77^post8+ret_time77^0 == 0 /\ -got_SIGHUP^post8+got_SIGHUP^0 == 0 /\ a88^post8 == 0 /\ -a55^post8+a55^0 == 0 /\ -tmp99^post8+ret_time1010^post8 == 0), cost: 1
  12: l10 -> l6 : curtime^0'=curtime^post12, tmp99^0'=tmp99^post12, a33^0'=a33^post12, wakend^0'=wakend^post12, ret_time77^0'=ret_time77^post12, last_copy_time^0'=last_copy_time^post12, a88^0'=a88^post12, tmp66^0'=tmp66^post12, ___rho_1_^0'=___rho_1_^post12, ret_time1010^0'=ret_time1010^post12, got_SIGHUP^0'=got_SIGHUP^post12, tt1^0'=tt1^post12, a55^0'=a55^post12, tmp2^0'=tmp2^post12, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post12, (a88^0-a88^post12 == 0 /\ tmp99^0-tmp99^post12 == 0 /\ ret_time77^0-ret_time77^post12 == 0 /\ -ret_time1010^post12+ret_time1010^0 == 0 /\ -tmp2^post12+tmp2^0 == 0 /\ -___rho_1_^post12+___rho_1_^0 == 0 /\ -ret_XLogArchivingActive44^post12+ret_XLogArchivingActive44^0 == 0 /\ -wakend^post12+wakend^0 == 0 /\ got_SIGHUP^0-got_SIGHUP^post12 == 0 /\ -tt1^post12+tt1^0 == 0 /\ -a55^post12+a55^0 == 0 /\ a33^0-a33^post12 == 0 /\ last_copy_time^0-last_copy_time^post12 == 0 /\ tmp66^0-tmp66^post12 == 0 /\ curtime^0-curtime^post12 == 0), cost: 1
  15: l11 -> l0 : curtime^0'=curtime^post15, tmp99^0'=tmp99^post15, a33^0'=a33^post15, wakend^0'=wakend^post15, ret_time77^0'=ret_time77^post15, last_copy_time^0'=last_copy_time^post15, a88^0'=a88^post15, tmp66^0'=tmp66^post15, ___rho_1_^0'=___rho_1_^post15, ret_time1010^0'=ret_time1010^post15, got_SIGHUP^0'=got_SIGHUP^post15, tt1^0'=tt1^post15, a55^0'=a55^post15, tmp2^0'=tmp2^post15, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post15, (0 == 0 /\ tmp99^0-tmp99^post15 == 0 /\ tmp66^0-tmp66^post15 == 0 /\ -tmp2^post15+tmp2^0 == 0 /\ -a88^post15+a88^0 == 0 /\ -ret_XLogArchivingActive44^post15+ret_XLogArchivingActive44^0 == 0 /\ ___rho_1_^0-___rho_1_^post15 == 0 /\ -ret_time1010^post15+ret_time1010^0 == 0 /\ -1+wakend^post15 == 0 /\ a33^0-a33^post15 == 0 /\ tt1^0-tt1^post15 == 0 /\ -a55^post15+a55^0 == 0 /\ -ret_time77^post15+ret_time77^0 == 0 /\ last_copy_time^0-last_copy_time^post15 == 0 /\ -1+wakend^10 == 0 /\ curtime^0-curtime^post15 == 0), cost: 1
  16: l12 -> l11 : curtime^0'=curtime^post16, tmp99^0'=tmp99^post16, a33^0'=a33^post16, wakend^0'=wakend^post16, ret_time77^0'=ret_time77^post16, last_copy_time^0'=last_copy_time^post16, a88^0'=a88^post16, tmp66^0'=tmp66^post16, ___rho_1_^0'=___rho_1_^post16, ret_time1010^0'=ret_time1010^post16, got_SIGHUP^0'=got_SIGHUP^post16, tt1^0'=tt1^post16, a55^0'=a55^post16, tmp2^0'=tmp2^post16, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post16, (-tmp2^post16+tmp2^0 == 0 /\ -ret_time77^post16+ret_time77^0 == 0 /\ -a88^post16+a88^0 == 0 /\ -got_SIGHUP^post16+got_SIGHUP^0 == 0 /\ -a55^post16+a55^0 == 0 /\ a33^0-a33^post16 == 0 /\ -ret_XLogArchivingActive44^post16+ret_XLogArchivingActive44^0 == 0 /\ -tmp66^post16+tmp66^0 == 0 /\ -tt1^post16+tt1^0 == 0 /\ tmp99^0-tmp99^post16 == 0 /\ wakend^0-wakend^post16 == 0 /\ curtime^0-curtime^post16 == 0 /\ ___rho_1_^0-___rho_1_^post16 == 0 /\ last_copy_time^0-last_copy_time^post16 == 0 /\ -ret_time1010^post16+ret_time1010^0 == 0), cost: 1


Removed unreachable rules and leafs
Start location: l12
   0: l0 -> l1 : curtime^0'=curtime^post0, tmp99^0'=tmp99^post0, a33^0'=a33^post0, wakend^0'=wakend^post0, ret_time77^0'=ret_time77^post0, last_copy_time^0'=last_copy_time^post0, a88^0'=a88^post0, tmp66^0'=tmp66^post0, ___rho_1_^0'=___rho_1_^post0, ret_time1010^0'=ret_time1010^post0, got_SIGHUP^0'=got_SIGHUP^post0, tt1^0'=tt1^post0, a55^0'=a55^post0, tmp2^0'=tmp2^post0, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post0, (-last_copy_time^post0+last_copy_time^0 == 0 /\ -tt1^post0+tt1^0 == 0 /\ -___rho_1_^post0+___rho_1_^0 == 0 /\ -a55^post0+a55^0 == 0 /\ ret_time1010^0-ret_time1010^post0 == 0 /\ tmp99^0-tmp99^post0 == 0 /\ wakend^0-wakend^post0 == 0 /\ a33^0-a33^post0 == 0 /\ ret_time77^0-ret_time77^post0 == 0 /\ got_SIGHUP^0 <= 0 /\ -curtime^post0+curtime^0 == 0 /\ -tmp2^post0+tmp2^0 == 0 /\ a88^0-a88^post0 == 0 /\ -ret_XLogArchivingActive44^post0+ret_XLogArchivingActive44^0 == 0 /\ -got_SIGHUP^post0+got_SIGHUP^0 == 0 /\ -tmp66^post0+tmp66^0 == 0), cost: 1
   1: l0 -> l2 : curtime^0'=curtime^post1, tmp99^0'=tmp99^post1, a33^0'=a33^post1, wakend^0'=wakend^post1, ret_time77^0'=ret_time77^post1, last_copy_time^0'=last_copy_time^post1, a88^0'=a88^post1, tmp66^0'=tmp66^post1, ___rho_1_^0'=___rho_1_^post1, ret_time1010^0'=ret_time1010^post1, got_SIGHUP^0'=got_SIGHUP^post1, tt1^0'=tt1^post1, a55^0'=a55^post1, tmp2^0'=tmp2^post1, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, (0 == 0 /\ -tmp2^post1+tt1^post1 == 0 /\ ret_time77^0-ret_time77^post1 == 0 /\ -last_copy_time^post1+last_copy_time^0 == 0 /\ curtime^0-curtime^post1 == 0 /\ -1+a33^post1 == 0 /\ a88^0-a88^post1 == 0 /\ -a55^post1+a55^0 == 0 /\ 1-got_SIGHUP^0 <= 0 /\ tmp66^0-tmp66^post1 == 0 /\ -tmp99^post1+tmp99^0 == 0 /\ -ret_time1010^post1+ret_time1010^0 == 0 /\ -___rho_1_^post1+ret_XLogArchivingActive44^post1 == 0 /\ got_SIGHUP^post1 == 0 /\ tmp2^post1-ret_XLogArchivingActive44^post1 == 0 /\ wakend^0-wakend^post1 == 0), cost: 1
   9: l1 -> l9 : curtime^0'=curtime^post9, tmp99^0'=tmp99^post9, a33^0'=a33^post9, wakend^0'=wakend^post9, ret_time77^0'=ret_time77^post9, last_copy_time^0'=last_copy_time^post9, a88^0'=a88^post9, tmp66^0'=tmp66^post9, ___rho_1_^0'=___rho_1_^post9, ret_time1010^0'=ret_time1010^post9, got_SIGHUP^0'=got_SIGHUP^post9, tt1^0'=tt1^post9, a55^0'=a55^post9, tmp2^0'=tmp2^post9, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post9, (-wakend^post9+wakend^0 == 0 /\ a88^0-a88^post9 == 0 /\ wakend^0 <= 0 /\ -tt1^post9+tt1^0 == 0 /\ -___rho_1_^post9+___rho_1_^0 == 0 /\ tmp99^0-tmp99^post9 == 0 /\ ret_time77^0-ret_time77^post9 == 0 /\ -tmp2^post9+tmp2^0 == 0 /\ -ret_XLogArchivingActive44^post9+ret_XLogArchivingActive44^0 == 0 /\ -a55^post9+a55^0 == 0 /\ got_SIGHUP^0-got_SIGHUP^post9 == 0 /\ a33^0-a33^post9 == 0 /\ tmp66^0-tmp66^post9 == 0 /\ last_copy_time^0-last_copy_time^post9 == 0 /\ curtime^0-curtime^post9 == 0 /\ -ret_time1010^post9+ret_time1010^0 == 0), cost: 1
  10: l1 -> l9 : curtime^0'=curtime^post10, tmp99^0'=tmp99^post10, a33^0'=a33^post10, wakend^0'=wakend^post10, ret_time77^0'=ret_time77^post10, last_copy_time^0'=last_copy_time^post10, a88^0'=a88^post10, tmp66^0'=tmp66^post10, ___rho_1_^0'=___rho_1_^post10, ret_time1010^0'=ret_time1010^post10, got_SIGHUP^0'=got_SIGHUP^post10, tt1^0'=tt1^post10, a55^0'=a55^post10, tmp2^0'=tmp2^post10, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post10, (0 == 0 /\ -tt1^post10+tt1^0 == 0 /\ curtime^0-curtime^post10 == 0 /\ ret_time77^post10-tmp66^post10 == 0 /\ -ret_XLogArchivingActive44^post10+ret_XLogArchivingActive44^0 == 0 /\ a55^post10 == 0 /\ -tmp2^post10+tmp2^0 == 0 /\ 1-wakend^0 <= 0 /\ -a33^post10+a33^0 == 0 /\ tmp99^0-tmp99^post10 == 0 /\ ___rho_1_^0-___rho_1_^post10 == 0 /\ -ret_time77^post10+last_copy_time^post10 == 0 /\ -ret_time1010^post10+ret_time1010^0 == 0 /\ -a88^post10+a88^0 == 0 /\ wakend^post10 == 0 /\ -got_SIGHUP^post10+got_SIGHUP^0 == 0), cost: 1
  13: l2 -> l1 : curtime^0'=curtime^post13, tmp99^0'=tmp99^post13, a33^0'=a33^post13, wakend^0'=wakend^post13, ret_time77^0'=ret_time77^post13, last_copy_time^0'=last_copy_time^post13, a88^0'=a88^post13, tmp66^0'=tmp66^post13, ___rho_1_^0'=___rho_1_^post13, ret_time1010^0'=ret_time1010^post13, got_SIGHUP^0'=got_SIGHUP^post13, tt1^0'=tt1^post13, a55^0'=a55^post13, tmp2^0'=tmp2^post13, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post13, (last_copy_time^0-last_copy_time^post13 == 0 /\ curtime^0-curtime^post13 == 0 /\ ___rho_1_^0-___rho_1_^post13 == 0 /\ -a55^post13+a55^0 == 0 /\ -ret_time77^post13+ret_time77^0 == 0 /\ -got_SIGHUP^post13+got_SIGHUP^0 == 0 /\ 1-tt1^0 <= 0 /\ -a88^post13+a88^0 == 0 /\ -ret_time1010^post13+ret_time1010^0 == 0 /\ tt1^0-tt1^post13 == 0 /\ -tmp2^post13+tmp2^0 == 0 /\ -ret_XLogArchivingActive44^post13+ret_XLogArchivingActive44^0 == 0 /\ tmp99^0-tmp99^post13 == 0 /\ wakend^0-wakend^post13 == 0 /\ a33^0-a33^post13 == 0 /\ -tmp66^post13+tmp66^0 == 0), cost: 1
  14: l2 -> l5 : curtime^0'=curtime^post14, tmp99^0'=tmp99^post14, a33^0'=a33^post14, wakend^0'=wakend^post14, ret_time77^0'=ret_time77^post14, last_copy_time^0'=last_copy_time^post14, a88^0'=a88^post14, tmp66^0'=tmp66^post14, ___rho_1_^0'=___rho_1_^post14, ret_time1010^0'=ret_time1010^post14, got_SIGHUP^0'=got_SIGHUP^post14, tt1^0'=tt1^post14, a55^0'=a55^post14, tmp2^0'=tmp2^post14, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post14, (-last_copy_time^post14+last_copy_time^0 == 0 /\ -a55^post14+a55^0 == 0 /\ ret_time1010^0-ret_time1010^post14 == 0 /\ tmp99^0-tmp99^post14 == 0 /\ wakend^0-wakend^post14 == 0 /\ a33^0-a33^post14 == 0 /\ ret_time77^0-ret_time77^post14 == 0 /\ curtime^0-curtime^post14 == 0 /\ tt1^0 <= 0 /\ -___rho_1_^post14+___rho_1_^0 == 0 /\ -ret_XLogArchivingActive44^post14+ret_XLogArchivingActive44^0 == 0 /\ -tmp2^post14+tmp2^0 == 0 /\ a88^0-a88^post14 == 0 /\ -tt1^post14+tt1^0 == 0 /\ -got_SIGHUP^post14+got_SIGHUP^0 == 0 /\ -tmp66^post14+tmp66^0 == 0), cost: 1
   3: l5 -> l6 : curtime^0'=curtime^post3, tmp99^0'=tmp99^post3, a33^0'=a33^post3, wakend^0'=wakend^post3, ret_time77^0'=ret_time77^post3, last_copy_time^0'=last_copy_time^post3, a88^0'=a88^post3, tmp66^0'=tmp66^post3, ___rho_1_^0'=___rho_1_^post3, ret_time1010^0'=ret_time1010^post3, got_SIGHUP^0'=got_SIGHUP^post3, tt1^0'=tt1^post3, a55^0'=a55^post3, tmp2^0'=tmp2^post3, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post3, (-got_SIGHUP^post3+got_SIGHUP^0 == 0 /\ -last_copy_time^post3+last_copy_time^0 == 0 /\ -tmp2^post3+tmp2^0 == 0 /\ -ret_XLogArchivingActive44^post3+ret_XLogArchivingActive44^0 == 0 /\ -a55^post3+a55^0 == 0 /\ ret_time1010^0-ret_time1010^post3 == 0 /\ a33^0-a33^post3 == 0 /\ tmp99^0-tmp99^post3 == 0 /\ -tt1^post3+tt1^0 == 0 /\ wakend^0-wakend^post3 == 0 /\ ret_time77^0-ret_time77^post3 == 0 /\ curtime^0-curtime^post3 == 0 /\ -___rho_1_^post3+___rho_1_^0 == 0 /\ -tmp66^post3+tmp66^0 == 0 /\ a88^0-a88^post3 == 0), cost: 1
  11: l6 -> l10 : curtime^0'=curtime^post11, tmp99^0'=tmp99^post11, a33^0'=a33^post11, wakend^0'=wakend^post11, ret_time77^0'=ret_time77^post11, last_copy_time^0'=last_copy_time^post11, a88^0'=a88^post11, tmp66^0'=tmp66^post11, ___rho_1_^0'=___rho_1_^post11, ret_time1010^0'=ret_time1010^post11, got_SIGHUP^0'=got_SIGHUP^post11, tt1^0'=tt1^post11, a55^0'=a55^post11, tmp2^0'=tmp2^post11, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post11, (-tt1^post11+tt1^0 == 0 /\ -1+wakend^post11 == 0 /\ -___rho_1_^post11+___rho_1_^0 == 0 /\ a33^0-a33^post11 == 0 /\ -tmp2^post11+tmp2^0 == 0 /\ -ret_XLogArchivingActive44^post11+ret_XLogArchivingActive44^0 == 0 /\ a55^0-a55^post11 == 0 /\ ret_time1010^0-ret_time1010^post11 == 0 /\ -tmp66^post11+tmp66^0 == 0 /\ curtime^0-curtime^post11 == 0 /\ -last_copy_time^post11+last_copy_time^0 == 0 /\ a88^0-a88^post11 == 0 /\ tmp99^0-tmp99^post11 == 0 /\ ret_time77^0-ret_time77^post11 == 0 /\ -got_SIGHUP^post11+got_SIGHUP^0 == 0), cost: 1
   4: l7 -> l5 : curtime^0'=curtime^post4, tmp99^0'=tmp99^post4, a33^0'=a33^post4, wakend^0'=wakend^post4, ret_time77^0'=ret_time77^post4, last_copy_time^0'=last_copy_time^post4, a88^0'=a88^post4, tmp66^0'=tmp66^post4, ___rho_1_^0'=___rho_1_^post4, ret_time1010^0'=ret_time1010^post4, got_SIGHUP^0'=got_SIGHUP^post4, tt1^0'=tt1^post4, a55^0'=a55^post4, tmp2^0'=tmp2^post4, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post4, (-ret_time1010^post4+ret_time1010^0 == 0 /\ -ret_XLogArchivingActive44^post4+ret_XLogArchivingActive44^0 == 0 /\ -tmp2^post4+tmp2^0 == 0 /\ -a55^post4+a55^0 == 0 /\ tmp99^0-tmp99^post4 == 0 /\ -a88^post4+a88^0 == 0 /\ tmp66^0-tmp66^post4 == 0 /\ last_copy_time^0-last_copy_time^post4 == 0 /\ ___rho_1_^0-___rho_1_^post4 == 0 /\ ret_time77^0-ret_time77^post4 == 0 /\ -wakend^post4+wakend^0 == 0 /\ -got_SIGHUP^post4+got_SIGHUP^0 == 0 /\ -a33^post4+a33^0 == 0 /\ tt1^0-tt1^post4 == 0 /\ curtime^0-curtime^post4 == 0), cost: 1
   5: l8 -> l7 : curtime^0'=curtime^post5, tmp99^0'=tmp99^post5, a33^0'=a33^post5, wakend^0'=wakend^post5, ret_time77^0'=ret_time77^post5, last_copy_time^0'=last_copy_time^post5, a88^0'=a88^post5, tmp66^0'=tmp66^post5, ___rho_1_^0'=___rho_1_^post5, ret_time1010^0'=ret_time1010^post5, got_SIGHUP^0'=got_SIGHUP^post5, tt1^0'=tt1^post5, a55^0'=a55^post5, tmp2^0'=tmp2^post5, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post5, (ret_time1010^0-ret_time1010^post5 == 0 /\ tmp99^0-tmp99^post5 == 0 /\ -ret_XLogArchivingActive44^post5+ret_XLogArchivingActive44^0 == 0 /\ -a88^post5+a88^0 == 0 /\ -ret_time77^post5+ret_time77^0 == 0 /\ -tmp66^post5+tmp66^0 == 0 /\ -999+curtime^0-last_copy_time^0 <= 0 /\ curtime^0-curtime^post5 == 0 /\ a33^0-a33^post5 == 0 /\ -tmp2^post5+tmp2^0 == 0 /\ -got_SIGHUP^post5+got_SIGHUP^0 == 0 /\ -tt1^post5+tt1^0 == 0 /\ wakend^0-wakend^post5 == 0 /\ ___rho_1_^0-___rho_1_^post5 == 0 /\ last_copy_time^0-last_copy_time^post5 == 0 /\ -a55^post5+a55^0 == 0), cost: 1
   6: l8 -> l7 : curtime^0'=curtime^post6, tmp99^0'=tmp99^post6, a33^0'=a33^post6, wakend^0'=wakend^post6, ret_time77^0'=ret_time77^post6, last_copy_time^0'=last_copy_time^post6, a88^0'=a88^post6, tmp66^0'=tmp66^post6, ___rho_1_^0'=___rho_1_^post6, ret_time1010^0'=ret_time1010^post6, got_SIGHUP^0'=got_SIGHUP^post6, tt1^0'=tt1^post6, a55^0'=a55^post6, tmp2^0'=tmp2^post6, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post6, (a88^0-a88^post6 == 0 /\ curtime^0-curtime^post6 == 0 /\ -___rho_1_^post6+___rho_1_^0 == 0 /\ -ret_XLogArchivingActive44^post6+ret_XLogArchivingActive44^0 == 0 /\ -tt1^post6+tt1^0 == 0 /\ ret_time77^0-ret_time77^post6 == 0 /\ -1+wakend^post6 == 0 /\ a55^0-a55^post6 == 0 /\ tmp99^0-tmp99^post6 == 0 /\ -tmp2^post6+tmp2^0 == 0 /\ 1000-curtime^0+last_copy_time^0 <= 0 /\ tmp66^0-tmp66^post6 == 0 /\ got_SIGHUP^0-got_SIGHUP^post6 == 0 /\ a33^0-a33^post6 == 0 /\ last_copy_time^0-last_copy_time^post6 == 0 /\ -ret_time1010^post6+ret_time1010^0 == 0), cost: 1
   7: l9 -> l7 : curtime^0'=curtime^post7, tmp99^0'=tmp99^post7, a33^0'=a33^post7, wakend^0'=wakend^post7, ret_time77^0'=ret_time77^post7, last_copy_time^0'=last_copy_time^post7, a88^0'=a88^post7, tmp66^0'=tmp66^post7, ___rho_1_^0'=___rho_1_^post7, ret_time1010^0'=ret_time1010^post7, got_SIGHUP^0'=got_SIGHUP^post7, tt1^0'=tt1^post7, a55^0'=a55^post7, tmp2^0'=tmp2^post7, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post7, (-ret_XLogArchivingActive44^post7+ret_XLogArchivingActive44^0 == 0 /\ curtime^0-curtime^post7 == 0 /\ tmp66^0-tmp66^post7 == 0 /\ -a88^post7+a88^0 == 0 /\ ___rho_1_^0-___rho_1_^post7 == 0 /\ last_copy_time^0-last_copy_time^post7 == 0 /\ tmp99^0-tmp99^post7 == 0 /\ -tmp2^post7+tmp2^0 == 0 /\ -a55^post7+a55^0 == 0 /\ 1-wakend^0 <= 0 /\ tt1^0-tt1^post7 == 0 /\ -wakend^post7+wakend^0 == 0 /\ a33^0-a33^post7 == 0 /\ -got_SIGHUP^post7+got_SIGHUP^0 == 0 /\ -ret_time1010^post7+ret_time1010^0 == 0 /\ ret_time77^0-ret_time77^post7 == 0), cost: 1
   8: l9 -> l8 : curtime^0'=curtime^post8, tmp99^0'=tmp99^post8, a33^0'=a33^post8, wakend^0'=wakend^post8, ret_time77^0'=ret_time77^post8, last_copy_time^0'=last_copy_time^post8, a88^0'=a88^post8, tmp66^0'=tmp66^post8, ___rho_1_^0'=___rho_1_^post8, ret_time1010^0'=ret_time1010^post8, got_SIGHUP^0'=got_SIGHUP^post8, tt1^0'=tt1^post8, a55^0'=a55^post8, tmp2^0'=tmp2^post8, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post8, (0 == 0 /\ -ret_XLogArchivingActive44^post8+ret_XLogArchivingActive44^0 == 0 /\ -tt1^post8+tt1^0 == 0 /\ wakend^0 <= 0 /\ -___rho_1_^post8+___rho_1_^0 == 0 /\ a33^0-a33^post8 == 0 /\ wakend^0-wakend^post8 == 0 /\ -last_copy_time^post8+last_copy_time^0 == 0 /\ curtime^post8-ret_time1010^post8 == 0 /\ -tmp2^post8+tmp2^0 == 0 /\ -tmp66^post8+tmp66^0 == 0 /\ -ret_time77^post8+ret_time77^0 == 0 /\ -got_SIGHUP^post8+got_SIGHUP^0 == 0 /\ a88^post8 == 0 /\ -a55^post8+a55^0 == 0 /\ -tmp99^post8+ret_time1010^post8 == 0), cost: 1
  12: l10 -> l6 : curtime^0'=curtime^post12, tmp99^0'=tmp99^post12, a33^0'=a33^post12, wakend^0'=wakend^post12, ret_time77^0'=ret_time77^post12, last_copy_time^0'=last_copy_time^post12, a88^0'=a88^post12, tmp66^0'=tmp66^post12, ___rho_1_^0'=___rho_1_^post12, ret_time1010^0'=ret_time1010^post12, got_SIGHUP^0'=got_SIGHUP^post12, tt1^0'=tt1^post12, a55^0'=a55^post12, tmp2^0'=tmp2^post12, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post12, (a88^0-a88^post12 == 0 /\ tmp99^0-tmp99^post12 == 0 /\ ret_time77^0-ret_time77^post12 == 0 /\ -ret_time1010^post12+ret_time1010^0 == 0 /\ -tmp2^post12+tmp2^0 == 0 /\ -___rho_1_^post12+___rho_1_^0 == 0 /\ -ret_XLogArchivingActive44^post12+ret_XLogArchivingActive44^0 == 0 /\ -wakend^post12+wakend^0 == 0 /\ got_SIGHUP^0-got_SIGHUP^post12 == 0 /\ -tt1^post12+tt1^0 == 0 /\ -a55^post12+a55^0 == 0 /\ a33^0-a33^post12 == 0 /\ last_copy_time^0-last_copy_time^post12 == 0 /\ tmp66^0-tmp66^post12 == 0 /\ curtime^0-curtime^post12 == 0), cost: 1
  15: l11 -> l0 : curtime^0'=curtime^post15, tmp99^0'=tmp99^post15, a33^0'=a33^post15, wakend^0'=wakend^post15, ret_time77^0'=ret_time77^post15, last_copy_time^0'=last_copy_time^post15, a88^0'=a88^post15, tmp66^0'=tmp66^post15, ___rho_1_^0'=___rho_1_^post15, ret_time1010^0'=ret_time1010^post15, got_SIGHUP^0'=got_SIGHUP^post15, tt1^0'=tt1^post15, a55^0'=a55^post15, tmp2^0'=tmp2^post15, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post15, (0 == 0 /\ tmp99^0-tmp99^post15 == 0 /\ tmp66^0-tmp66^post15 == 0 /\ -tmp2^post15+tmp2^0 == 0 /\ -a88^post15+a88^0 == 0 /\ -ret_XLogArchivingActive44^post15+ret_XLogArchivingActive44^0 == 0 /\ ___rho_1_^0-___rho_1_^post15 == 0 /\ -ret_time1010^post15+ret_time1010^0 == 0 /\ -1+wakend^post15 == 0 /\ a33^0-a33^post15 == 0 /\ tt1^0-tt1^post15 == 0 /\ -a55^post15+a55^0 == 0 /\ -ret_time77^post15+ret_time77^0 == 0 /\ last_copy_time^0-last_copy_time^post15 == 0 /\ -1+wakend^10 == 0 /\ curtime^0-curtime^post15 == 0), cost: 1
  16: l12 -> l11 : curtime^0'=curtime^post16, tmp99^0'=tmp99^post16, a33^0'=a33^post16, wakend^0'=wakend^post16, ret_time77^0'=ret_time77^post16, last_copy_time^0'=last_copy_time^post16, a88^0'=a88^post16, tmp66^0'=tmp66^post16, ___rho_1_^0'=___rho_1_^post16, ret_time1010^0'=ret_time1010^post16, got_SIGHUP^0'=got_SIGHUP^post16, tt1^0'=tt1^post16, a55^0'=a55^post16, tmp2^0'=tmp2^post16, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post16, (-tmp2^post16+tmp2^0 == 0 /\ -ret_time77^post16+ret_time77^0 == 0 /\ -a88^post16+a88^0 == 0 /\ -got_SIGHUP^post16+got_SIGHUP^0 == 0 /\ -a55^post16+a55^0 == 0 /\ a33^0-a33^post16 == 0 /\ -ret_XLogArchivingActive44^post16+ret_XLogArchivingActive44^0 == 0 /\ -tmp66^post16+tmp66^0 == 0 /\ -tt1^post16+tt1^0 == 0 /\ tmp99^0-tmp99^post16 == 0 /\ wakend^0-wakend^post16 == 0 /\ curtime^0-curtime^post16 == 0 /\ ___rho_1_^0-___rho_1_^post16 == 0 /\ last_copy_time^0-last_copy_time^post16 == 0 /\ -ret_time1010^post16+ret_time1010^0 == 0), cost: 1


Applied preprocessing
Original rule:
l0 -> l1 : curtime^0'=curtime^post0, tmp99^0'=tmp99^post0, a33^0'=a33^post0, wakend^0'=wakend^post0, ret_time77^0'=ret_time77^post0, last_copy_time^0'=last_copy_time^post0, a88^0'=a88^post0, tmp66^0'=tmp66^post0, ___rho_1_^0'=___rho_1_^post0, ret_time1010^0'=ret_time1010^post0, got_SIGHUP^0'=got_SIGHUP^post0, tt1^0'=tt1^post0, a55^0'=a55^post0, tmp2^0'=tmp2^post0, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post0, (-last_copy_time^post0+last_copy_time^0 == 0 /\ -tt1^post0+tt1^0 == 0 /\ -___rho_1_^post0+___rho_1_^0 == 0 /\ -a55^post0+a55^0 == 0 /\ ret_time1010^0-ret_time1010^post0 == 0 /\ tmp99^0-tmp99^post0 == 0 /\ wakend^0-wakend^post0 == 0 /\ a33^0-a33^post0 == 0 /\ ret_time77^0-ret_time77^post0 == 0 /\ got_SIGHUP^0 <= 0 /\ -curtime^post0+curtime^0 == 0 /\ -tmp2^post0+tmp2^0 == 0 /\ a88^0-a88^post0 == 0 /\ -ret_XLogArchivingActive44^post0+ret_XLogArchivingActive44^0 == 0 /\ -got_SIGHUP^post0+got_SIGHUP^0 == 0 /\ -tmp66^post0+tmp66^0 == 0), cost: 1
New rule:
l0 -> l1 : got_SIGHUP^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l0 -> l2 : curtime^0'=curtime^post1, tmp99^0'=tmp99^post1, a33^0'=a33^post1, wakend^0'=wakend^post1, ret_time77^0'=ret_time77^post1, last_copy_time^0'=last_copy_time^post1, a88^0'=a88^post1, tmp66^0'=tmp66^post1, ___rho_1_^0'=___rho_1_^post1, ret_time1010^0'=ret_time1010^post1, got_SIGHUP^0'=got_SIGHUP^post1, tt1^0'=tt1^post1, a55^0'=a55^post1, tmp2^0'=tmp2^post1, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, (0 == 0 /\ -tmp2^post1+tt1^post1 == 0 /\ ret_time77^0-ret_time77^post1 == 0 /\ -last_copy_time^post1+last_copy_time^0 == 0 /\ curtime^0-curtime^post1 == 0 /\ -1+a33^post1 == 0 /\ a88^0-a88^post1 == 0 /\ -a55^post1+a55^0 == 0 /\ 1-got_SIGHUP^0 <= 0 /\ tmp66^0-tmp66^post1 == 0 /\ -tmp99^post1+tmp99^0 == 0 /\ -ret_time1010^post1+ret_time1010^0 == 0 /\ -___rho_1_^post1+ret_XLogArchivingActive44^post1 == 0 /\ got_SIGHUP^post1 == 0 /\ tmp2^post1-ret_XLogArchivingActive44^post1 == 0 /\ wakend^0-wakend^post1 == 0), cost: 1
New rule:
l0 -> l2 : a33^0'=1, ___rho_1_^0'=ret_XLogArchivingActive44^post1, got_SIGHUP^0'=0, tt1^0'=ret_XLogArchivingActive44^post1, tmp2^0'=ret_XLogArchivingActive44^post1, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, -1+got_SIGHUP^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l5 -> l6 : curtime^0'=curtime^post3, tmp99^0'=tmp99^post3, a33^0'=a33^post3, wakend^0'=wakend^post3, ret_time77^0'=ret_time77^post3, last_copy_time^0'=last_copy_time^post3, a88^0'=a88^post3, tmp66^0'=tmp66^post3, ___rho_1_^0'=___rho_1_^post3, ret_time1010^0'=ret_time1010^post3, got_SIGHUP^0'=got_SIGHUP^post3, tt1^0'=tt1^post3, a55^0'=a55^post3, tmp2^0'=tmp2^post3, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post3, (-got_SIGHUP^post3+got_SIGHUP^0 == 0 /\ -last_copy_time^post3+last_copy_time^0 == 0 /\ -tmp2^post3+tmp2^0 == 0 /\ -ret_XLogArchivingActive44^post3+ret_XLogArchivingActive44^0 == 0 /\ -a55^post3+a55^0 == 0 /\ ret_time1010^0-ret_time1010^post3 == 0 /\ a33^0-a33^post3 == 0 /\ tmp99^0-tmp99^post3 == 0 /\ -tt1^post3+tt1^0 == 0 /\ wakend^0-wakend^post3 == 0 /\ ret_time77^0-ret_time77^post3 == 0 /\ curtime^0-curtime^post3 == 0 /\ -___rho_1_^post3+___rho_1_^0 == 0 /\ -tmp66^post3+tmp66^0 == 0 /\ a88^0-a88^post3 == 0), cost: 1
New rule:
l5 -> l6 : TRUE, cost: 1

Applied preprocessing
Original rule:
l7 -> l5 : curtime^0'=curtime^post4, tmp99^0'=tmp99^post4, a33^0'=a33^post4, wakend^0'=wakend^post4, ret_time77^0'=ret_time77^post4, last_copy_time^0'=last_copy_time^post4, a88^0'=a88^post4, tmp66^0'=tmp66^post4, ___rho_1_^0'=___rho_1_^post4, ret_time1010^0'=ret_time1010^post4, got_SIGHUP^0'=got_SIGHUP^post4, tt1^0'=tt1^post4, a55^0'=a55^post4, tmp2^0'=tmp2^post4, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post4, (-ret_time1010^post4+ret_time1010^0 == 0 /\ -ret_XLogArchivingActive44^post4+ret_XLogArchivingActive44^0 == 0 /\ -tmp2^post4+tmp2^0 == 0 /\ -a55^post4+a55^0 == 0 /\ tmp99^0-tmp99^post4 == 0 /\ -a88^post4+a88^0 == 0 /\ tmp66^0-tmp66^post4 == 0 /\ last_copy_time^0-last_copy_time^post4 == 0 /\ ___rho_1_^0-___rho_1_^post4 == 0 /\ ret_time77^0-ret_time77^post4 == 0 /\ -wakend^post4+wakend^0 == 0 /\ -got_SIGHUP^post4+got_SIGHUP^0 == 0 /\ -a33^post4+a33^0 == 0 /\ tt1^0-tt1^post4 == 0 /\ curtime^0-curtime^post4 == 0), cost: 1
New rule:
l7 -> l5 : TRUE, cost: 1

Applied preprocessing
Original rule:
l8 -> l7 : curtime^0'=curtime^post5, tmp99^0'=tmp99^post5, a33^0'=a33^post5, wakend^0'=wakend^post5, ret_time77^0'=ret_time77^post5, last_copy_time^0'=last_copy_time^post5, a88^0'=a88^post5, tmp66^0'=tmp66^post5, ___rho_1_^0'=___rho_1_^post5, ret_time1010^0'=ret_time1010^post5, got_SIGHUP^0'=got_SIGHUP^post5, tt1^0'=tt1^post5, a55^0'=a55^post5, tmp2^0'=tmp2^post5, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post5, (ret_time1010^0-ret_time1010^post5 == 0 /\ tmp99^0-tmp99^post5 == 0 /\ -ret_XLogArchivingActive44^post5+ret_XLogArchivingActive44^0 == 0 /\ -a88^post5+a88^0 == 0 /\ -ret_time77^post5+ret_time77^0 == 0 /\ -tmp66^post5+tmp66^0 == 0 /\ -999+curtime^0-last_copy_time^0 <= 0 /\ curtime^0-curtime^post5 == 0 /\ a33^0-a33^post5 == 0 /\ -tmp2^post5+tmp2^0 == 0 /\ -got_SIGHUP^post5+got_SIGHUP^0 == 0 /\ -tt1^post5+tt1^0 == 0 /\ wakend^0-wakend^post5 == 0 /\ ___rho_1_^0-___rho_1_^post5 == 0 /\ last_copy_time^0-last_copy_time^post5 == 0 /\ -a55^post5+a55^0 == 0), cost: 1
New rule:
l8 -> l7 : -999+curtime^0-last_copy_time^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l8 -> l7 : curtime^0'=curtime^post6, tmp99^0'=tmp99^post6, a33^0'=a33^post6, wakend^0'=wakend^post6, ret_time77^0'=ret_time77^post6, last_copy_time^0'=last_copy_time^post6, a88^0'=a88^post6, tmp66^0'=tmp66^post6, ___rho_1_^0'=___rho_1_^post6, ret_time1010^0'=ret_time1010^post6, got_SIGHUP^0'=got_SIGHUP^post6, tt1^0'=tt1^post6, a55^0'=a55^post6, tmp2^0'=tmp2^post6, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post6, (a88^0-a88^post6 == 0 /\ curtime^0-curtime^post6 == 0 /\ -___rho_1_^post6+___rho_1_^0 == 0 /\ -ret_XLogArchivingActive44^post6+ret_XLogArchivingActive44^0 == 0 /\ -tt1^post6+tt1^0 == 0 /\ ret_time77^0-ret_time77^post6 == 0 /\ -1+wakend^post6 == 0 /\ a55^0-a55^post6 == 0 /\ tmp99^0-tmp99^post6 == 0 /\ -tmp2^post6+tmp2^0 == 0 /\ 1000-curtime^0+last_copy_time^0 <= 0 /\ tmp66^0-tmp66^post6 == 0 /\ got_SIGHUP^0-got_SIGHUP^post6 == 0 /\ a33^0-a33^post6 == 0 /\ last_copy_time^0-last_copy_time^post6 == 0 /\ -ret_time1010^post6+ret_time1010^0 == 0), cost: 1
New rule:
l8 -> l7 : wakend^0'=1, 1000-curtime^0+last_copy_time^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l9 -> l7 : curtime^0'=curtime^post7, tmp99^0'=tmp99^post7, a33^0'=a33^post7, wakend^0'=wakend^post7, ret_time77^0'=ret_time77^post7, last_copy_time^0'=last_copy_time^post7, a88^0'=a88^post7, tmp66^0'=tmp66^post7, ___rho_1_^0'=___rho_1_^post7, ret_time1010^0'=ret_time1010^post7, got_SIGHUP^0'=got_SIGHUP^post7, tt1^0'=tt1^post7, a55^0'=a55^post7, tmp2^0'=tmp2^post7, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post7, (-ret_XLogArchivingActive44^post7+ret_XLogArchivingActive44^0 == 0 /\ curtime^0-curtime^post7 == 0 /\ tmp66^0-tmp66^post7 == 0 /\ -a88^post7+a88^0 == 0 /\ ___rho_1_^0-___rho_1_^post7 == 0 /\ last_copy_time^0-last_copy_time^post7 == 0 /\ tmp99^0-tmp99^post7 == 0 /\ -tmp2^post7+tmp2^0 == 0 /\ -a55^post7+a55^0 == 0 /\ 1-wakend^0 <= 0 /\ tt1^0-tt1^post7 == 0 /\ -wakend^post7+wakend^0 == 0 /\ a33^0-a33^post7 == 0 /\ -got_SIGHUP^post7+got_SIGHUP^0 == 0 /\ -ret_time1010^post7+ret_time1010^0 == 0 /\ ret_time77^0-ret_time77^post7 == 0), cost: 1
New rule:
l9 -> l7 : -1+wakend^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l9 -> l8 : curtime^0'=curtime^post8, tmp99^0'=tmp99^post8, a33^0'=a33^post8, wakend^0'=wakend^post8, ret_time77^0'=ret_time77^post8, last_copy_time^0'=last_copy_time^post8, a88^0'=a88^post8, tmp66^0'=tmp66^post8, ___rho_1_^0'=___rho_1_^post8, ret_time1010^0'=ret_time1010^post8, got_SIGHUP^0'=got_SIGHUP^post8, tt1^0'=tt1^post8, a55^0'=a55^post8, tmp2^0'=tmp2^post8, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post8, (0 == 0 /\ -ret_XLogArchivingActive44^post8+ret_XLogArchivingActive44^0 == 0 /\ -tt1^post8+tt1^0 == 0 /\ wakend^0 <= 0 /\ -___rho_1_^post8+___rho_1_^0 == 0 /\ a33^0-a33^post8 == 0 /\ wakend^0-wakend^post8 == 0 /\ -last_copy_time^post8+last_copy_time^0 == 0 /\ curtime^post8-ret_time1010^post8 == 0 /\ -tmp2^post8+tmp2^0 == 0 /\ -tmp66^post8+tmp66^0 == 0 /\ -ret_time77^post8+ret_time77^0 == 0 /\ -got_SIGHUP^post8+got_SIGHUP^0 == 0 /\ a88^post8 == 0 /\ -a55^post8+a55^0 == 0 /\ -tmp99^post8+ret_time1010^post8 == 0), cost: 1
New rule:
l9 -> l8 : curtime^0'=ret_time1010^post8, tmp99^0'=ret_time1010^post8, a88^0'=0, ret_time1010^0'=ret_time1010^post8, wakend^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l1 -> l9 : curtime^0'=curtime^post9, tmp99^0'=tmp99^post9, a33^0'=a33^post9, wakend^0'=wakend^post9, ret_time77^0'=ret_time77^post9, last_copy_time^0'=last_copy_time^post9, a88^0'=a88^post9, tmp66^0'=tmp66^post9, ___rho_1_^0'=___rho_1_^post9, ret_time1010^0'=ret_time1010^post9, got_SIGHUP^0'=got_SIGHUP^post9, tt1^0'=tt1^post9, a55^0'=a55^post9, tmp2^0'=tmp2^post9, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post9, (-wakend^post9+wakend^0 == 0 /\ a88^0-a88^post9 == 0 /\ wakend^0 <= 0 /\ -tt1^post9+tt1^0 == 0 /\ -___rho_1_^post9+___rho_1_^0 == 0 /\ tmp99^0-tmp99^post9 == 0 /\ ret_time77^0-ret_time77^post9 == 0 /\ -tmp2^post9+tmp2^0 == 0 /\ -ret_XLogArchivingActive44^post9+ret_XLogArchivingActive44^0 == 0 /\ -a55^post9+a55^0 == 0 /\ got_SIGHUP^0-got_SIGHUP^post9 == 0 /\ a33^0-a33^post9 == 0 /\ tmp66^0-tmp66^post9 == 0 /\ last_copy_time^0-last_copy_time^post9 == 0 /\ curtime^0-curtime^post9 == 0 /\ -ret_time1010^post9+ret_time1010^0 == 0), cost: 1
New rule:
l1 -> l9 : wakend^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l1 -> l9 : curtime^0'=curtime^post10, tmp99^0'=tmp99^post10, a33^0'=a33^post10, wakend^0'=wakend^post10, ret_time77^0'=ret_time77^post10, last_copy_time^0'=last_copy_time^post10, a88^0'=a88^post10, tmp66^0'=tmp66^post10, ___rho_1_^0'=___rho_1_^post10, ret_time1010^0'=ret_time1010^post10, got_SIGHUP^0'=got_SIGHUP^post10, tt1^0'=tt1^post10, a55^0'=a55^post10, tmp2^0'=tmp2^post10, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post10, (0 == 0 /\ -tt1^post10+tt1^0 == 0 /\ curtime^0-curtime^post10 == 0 /\ ret_time77^post10-tmp66^post10 == 0 /\ -ret_XLogArchivingActive44^post10+ret_XLogArchivingActive44^0 == 0 /\ a55^post10 == 0 /\ -tmp2^post10+tmp2^0 == 0 /\ 1-wakend^0 <= 0 /\ -a33^post10+a33^0 == 0 /\ tmp99^0-tmp99^post10 == 0 /\ ___rho_1_^0-___rho_1_^post10 == 0 /\ -ret_time77^post10+last_copy_time^post10 == 0 /\ -ret_time1010^post10+ret_time1010^0 == 0 /\ -a88^post10+a88^0 == 0 /\ wakend^post10 == 0 /\ -got_SIGHUP^post10+got_SIGHUP^0 == 0), cost: 1
New rule:
l1 -> l9 : wakend^0'=0, ret_time77^0'=last_copy_time^post10, last_copy_time^0'=last_copy_time^post10, tmp66^0'=last_copy_time^post10, a55^0'=0, -1+wakend^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l6 -> l10 : curtime^0'=curtime^post11, tmp99^0'=tmp99^post11, a33^0'=a33^post11, wakend^0'=wakend^post11, ret_time77^0'=ret_time77^post11, last_copy_time^0'=last_copy_time^post11, a88^0'=a88^post11, tmp66^0'=tmp66^post11, ___rho_1_^0'=___rho_1_^post11, ret_time1010^0'=ret_time1010^post11, got_SIGHUP^0'=got_SIGHUP^post11, tt1^0'=tt1^post11, a55^0'=a55^post11, tmp2^0'=tmp2^post11, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post11, (-tt1^post11+tt1^0 == 0 /\ -1+wakend^post11 == 0 /\ -___rho_1_^post11+___rho_1_^0 == 0 /\ a33^0-a33^post11 == 0 /\ -tmp2^post11+tmp2^0 == 0 /\ -ret_XLogArchivingActive44^post11+ret_XLogArchivingActive44^0 == 0 /\ a55^0-a55^post11 == 0 /\ ret_time1010^0-ret_time1010^post11 == 0 /\ -tmp66^post11+tmp66^0 == 0 /\ curtime^0-curtime^post11 == 0 /\ -last_copy_time^post11+last_copy_time^0 == 0 /\ a88^0-a88^post11 == 0 /\ tmp99^0-tmp99^post11 == 0 /\ ret_time77^0-ret_time77^post11 == 0 /\ -got_SIGHUP^post11+got_SIGHUP^0 == 0), cost: 1
New rule:
l6 -> l10 : wakend^0'=1, TRUE, cost: 1

Applied preprocessing
Original rule:
l10 -> l6 : curtime^0'=curtime^post12, tmp99^0'=tmp99^post12, a33^0'=a33^post12, wakend^0'=wakend^post12, ret_time77^0'=ret_time77^post12, last_copy_time^0'=last_copy_time^post12, a88^0'=a88^post12, tmp66^0'=tmp66^post12, ___rho_1_^0'=___rho_1_^post12, ret_time1010^0'=ret_time1010^post12, got_SIGHUP^0'=got_SIGHUP^post12, tt1^0'=tt1^post12, a55^0'=a55^post12, tmp2^0'=tmp2^post12, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post12, (a88^0-a88^post12 == 0 /\ tmp99^0-tmp99^post12 == 0 /\ ret_time77^0-ret_time77^post12 == 0 /\ -ret_time1010^post12+ret_time1010^0 == 0 /\ -tmp2^post12+tmp2^0 == 0 /\ -___rho_1_^post12+___rho_1_^0 == 0 /\ -ret_XLogArchivingActive44^post12+ret_XLogArchivingActive44^0 == 0 /\ -wakend^post12+wakend^0 == 0 /\ got_SIGHUP^0-got_SIGHUP^post12 == 0 /\ -tt1^post12+tt1^0 == 0 /\ -a55^post12+a55^0 == 0 /\ a33^0-a33^post12 == 0 /\ last_copy_time^0-last_copy_time^post12 == 0 /\ tmp66^0-tmp66^post12 == 0 /\ curtime^0-curtime^post12 == 0), cost: 1
New rule:
l10 -> l6 : TRUE, cost: 1

Applied preprocessing
Original rule:
l2 -> l1 : curtime^0'=curtime^post13, tmp99^0'=tmp99^post13, a33^0'=a33^post13, wakend^0'=wakend^post13, ret_time77^0'=ret_time77^post13, last_copy_time^0'=last_copy_time^post13, a88^0'=a88^post13, tmp66^0'=tmp66^post13, ___rho_1_^0'=___rho_1_^post13, ret_time1010^0'=ret_time1010^post13, got_SIGHUP^0'=got_SIGHUP^post13, tt1^0'=tt1^post13, a55^0'=a55^post13, tmp2^0'=tmp2^post13, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post13, (last_copy_time^0-last_copy_time^post13 == 0 /\ curtime^0-curtime^post13 == 0 /\ ___rho_1_^0-___rho_1_^post13 == 0 /\ -a55^post13+a55^0 == 0 /\ -ret_time77^post13+ret_time77^0 == 0 /\ -got_SIGHUP^post13+got_SIGHUP^0 == 0 /\ 1-tt1^0 <= 0 /\ -a88^post13+a88^0 == 0 /\ -ret_time1010^post13+ret_time1010^0 == 0 /\ tt1^0-tt1^post13 == 0 /\ -tmp2^post13+tmp2^0 == 0 /\ -ret_XLogArchivingActive44^post13+ret_XLogArchivingActive44^0 == 0 /\ tmp99^0-tmp99^post13 == 0 /\ wakend^0-wakend^post13 == 0 /\ a33^0-a33^post13 == 0 /\ -tmp66^post13+tmp66^0 == 0), cost: 1
New rule:
l2 -> l1 : -1+tt1^0 >= 0, cost: 1

Applied preprocessing
Original rule:
l2 -> l5 : curtime^0'=curtime^post14, tmp99^0'=tmp99^post14, a33^0'=a33^post14, wakend^0'=wakend^post14, ret_time77^0'=ret_time77^post14, last_copy_time^0'=last_copy_time^post14, a88^0'=a88^post14, tmp66^0'=tmp66^post14, ___rho_1_^0'=___rho_1_^post14, ret_time1010^0'=ret_time1010^post14, got_SIGHUP^0'=got_SIGHUP^post14, tt1^0'=tt1^post14, a55^0'=a55^post14, tmp2^0'=tmp2^post14, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post14, (-last_copy_time^post14+last_copy_time^0 == 0 /\ -a55^post14+a55^0 == 0 /\ ret_time1010^0-ret_time1010^post14 == 0 /\ tmp99^0-tmp99^post14 == 0 /\ wakend^0-wakend^post14 == 0 /\ a33^0-a33^post14 == 0 /\ ret_time77^0-ret_time77^post14 == 0 /\ curtime^0-curtime^post14 == 0 /\ tt1^0 <= 0 /\ -___rho_1_^post14+___rho_1_^0 == 0 /\ -ret_XLogArchivingActive44^post14+ret_XLogArchivingActive44^0 == 0 /\ -tmp2^post14+tmp2^0 == 0 /\ a88^0-a88^post14 == 0 /\ -tt1^post14+tt1^0 == 0 /\ -got_SIGHUP^post14+got_SIGHUP^0 == 0 /\ -tmp66^post14+tmp66^0 == 0), cost: 1
New rule:
l2 -> l5 : tt1^0 <= 0, cost: 1

Applied preprocessing
Original rule:
l11 -> l0 : curtime^0'=curtime^post15, tmp99^0'=tmp99^post15, a33^0'=a33^post15, wakend^0'=wakend^post15, ret_time77^0'=ret_time77^post15, last_copy_time^0'=last_copy_time^post15, a88^0'=a88^post15, tmp66^0'=tmp66^post15, ___rho_1_^0'=___rho_1_^post15, ret_time1010^0'=ret_time1010^post15, got_SIGHUP^0'=got_SIGHUP^post15, tt1^0'=tt1^post15, a55^0'=a55^post15, tmp2^0'=tmp2^post15, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post15, (0 == 0 /\ tmp99^0-tmp99^post15 == 0 /\ tmp66^0-tmp66^post15 == 0 /\ -tmp2^post15+tmp2^0 == 0 /\ -a88^post15+a88^0 == 0 /\ -ret_XLogArchivingActive44^post15+ret_XLogArchivingActive44^0 == 0 /\ ___rho_1_^0-___rho_1_^post15 == 0 /\ -ret_time1010^post15+ret_time1010^0 == 0 /\ -1+wakend^post15 == 0 /\ a33^0-a33^post15 == 0 /\ tt1^0-tt1^post15 == 0 /\ -a55^post15+a55^0 == 0 /\ -ret_time77^post15+ret_time77^0 == 0 /\ last_copy_time^0-last_copy_time^post15 == 0 /\ -1+wakend^10 == 0 /\ curtime^0-curtime^post15 == 0), cost: 1
New rule:
l11 -> l0 : wakend^0'=1, got_SIGHUP^0'=got_SIGHUP^post15, 0 == 0, cost: 1

Applied preprocessing
Original rule:
l12 -> l11 : curtime^0'=curtime^post16, tmp99^0'=tmp99^post16, a33^0'=a33^post16, wakend^0'=wakend^post16, ret_time77^0'=ret_time77^post16, last_copy_time^0'=last_copy_time^post16, a88^0'=a88^post16, tmp66^0'=tmp66^post16, ___rho_1_^0'=___rho_1_^post16, ret_time1010^0'=ret_time1010^post16, got_SIGHUP^0'=got_SIGHUP^post16, tt1^0'=tt1^post16, a55^0'=a55^post16, tmp2^0'=tmp2^post16, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post16, (-tmp2^post16+tmp2^0 == 0 /\ -ret_time77^post16+ret_time77^0 == 0 /\ -a88^post16+a88^0 == 0 /\ -got_SIGHUP^post16+got_SIGHUP^0 == 0 /\ -a55^post16+a55^0 == 0 /\ a33^0-a33^post16 == 0 /\ -ret_XLogArchivingActive44^post16+ret_XLogArchivingActive44^0 == 0 /\ -tmp66^post16+tmp66^0 == 0 /\ -tt1^post16+tt1^0 == 0 /\ tmp99^0-tmp99^post16 == 0 /\ wakend^0-wakend^post16 == 0 /\ curtime^0-curtime^post16 == 0 /\ ___rho_1_^0-___rho_1_^post16 == 0 /\ last_copy_time^0-last_copy_time^post16 == 0 /\ -ret_time1010^post16+ret_time1010^0 == 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, got_SIGHUP^0'=0, tt1^0'=ret_XLogArchivingActive44^post1, 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 : wakend^0'=0, ret_time77^0'=last_copy_time^post10, last_copy_time^0'=last_copy_time^post10, tmp66^0'=last_copy_time^post10, a55^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 : wakend^0'=1, TRUE, cost: 1
  20: l7 -> l5 : TRUE, cost: 1
  21: l8 -> l7 : -999+curtime^0-last_copy_time^0 <= 0, cost: 1
  22: l8 -> l7 : wakend^0'=1, 1000-curtime^0+last_copy_time^0 <= 0, cost: 1
  23: l9 -> l7 : -1+wakend^0 >= 0, cost: 1
  24: l9 -> l8 : curtime^0'=ret_time1010^post8, tmp99^0'=ret_time1010^post8, a88^0'=0, ret_time1010^0'=ret_time1010^post8, wakend^0 <= 0, cost: 1
  28: l10 -> l6 : TRUE, cost: 1
  31: l11 -> l0 : wakend^0'=1, got_SIGHUP^0'=got_SIGHUP^post15, 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 : wakend^0'=1, got_SIGHUP^0'=got_SIGHUP^post15, 0 == 0, cost: 1
New rule:
l12 -> l0 : wakend^0'=1, got_SIGHUP^0'=got_SIGHUP^post15, 0 == 0, cost: 2

Applied deletion
Removed the following rules: 31 32

Eliminating location l10 by chaining:

Applied chaining
First rule:
l6 -> l10 : wakend^0'=1, TRUE, cost: 1
Second rule:
l10 -> l6 : TRUE, cost: 1
New rule:
l6 -> l6 : wakend^0'=1, 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, got_SIGHUP^0'=0, tt1^0'=ret_XLogArchivingActive44^post1, 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 : wakend^0'=0, ret_time77^0'=last_copy_time^post10, last_copy_time^0'=last_copy_time^post10, tmp66^0'=last_copy_time^post10, a55^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 : wakend^0'=1, TRUE, cost: 2
  20: l7 -> l5 : TRUE, cost: 1
  21: l8 -> l7 : -999+curtime^0-last_copy_time^0 <= 0, cost: 1
  22: l8 -> l7 : wakend^0'=1, 1000-curtime^0+last_copy_time^0 <= 0, cost: 1
  23: l9 -> l7 : -1+wakend^0 >= 0, cost: 1
  24: l9 -> l8 : curtime^0'=ret_time1010^post8, tmp99^0'=ret_time1010^post8, a88^0'=0, ret_time1010^0'=ret_time1010^post8, wakend^0 <= 0, cost: 1
  33: l12 -> l0 : wakend^0'=1, got_SIGHUP^0'=got_SIGHUP^post15, 0 == 0, cost: 2


Applied nonterm
Original rule:
l6 -> l6 : wakend^0'=1, TRUE, cost: 2
New rule:
l6 -> [13] : -1+n >= 0, cost: NONTERM
Sub-proof via acceration calculus written to file:///tmp/tmpnam_cdpmKp.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, got_SIGHUP^0'=0, tt1^0'=ret_XLogArchivingActive44^post1, 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 : wakend^0'=0, ret_time77^0'=last_copy_time^post10, last_copy_time^0'=last_copy_time^post10, tmp66^0'=last_copy_time^post10, a55^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] : -1+n >= 0, cost: NONTERM
  20: l7 -> l5 : TRUE, cost: 1
  21: l8 -> l7 : -999+curtime^0-last_copy_time^0 <= 0, cost: 1
  22: l8 -> l7 : wakend^0'=1, 1000-curtime^0+last_copy_time^0 <= 0, cost: 1
  23: l9 -> l7 : -1+wakend^0 >= 0, cost: 1
  24: l9 -> l8 : curtime^0'=ret_time1010^post8, tmp99^0'=ret_time1010^post8, a88^0'=0, ret_time1010^0'=ret_time1010^post8, wakend^0 <= 0, cost: 1
  33: l12 -> l0 : wakend^0'=1, got_SIGHUP^0'=got_SIGHUP^post15, 0 == 0, cost: 2


Applied chaining
First rule:
l5 -> l6 : TRUE, cost: 1
Second rule:
l6 -> [13] : -1+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, got_SIGHUP^0'=0, tt1^0'=ret_XLogArchivingActive44^post1, 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 : wakend^0'=0, ret_time77^0'=last_copy_time^post10, last_copy_time^0'=last_copy_time^post10, tmp66^0'=last_copy_time^post10, a55^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 : -999+curtime^0-last_copy_time^0 <= 0, cost: 1
  22: l8 -> l7 : wakend^0'=1, 1000-curtime^0+last_copy_time^0 <= 0, cost: 1
  23: l9 -> l7 : -1+wakend^0 >= 0, cost: 1
  24: l9 -> l8 : curtime^0'=ret_time1010^post8, tmp99^0'=ret_time1010^post8, a88^0'=0, ret_time1010^0'=ret_time1010^post8, wakend^0 <= 0, cost: 1
  33: l12 -> l0 : wakend^0'=1, got_SIGHUP^0'=got_SIGHUP^post15, 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, got_SIGHUP^0'=0, tt1^0'=ret_XLogArchivingActive44^post1, 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 : wakend^0'=0, ret_time77^0'=last_copy_time^post10, last_copy_time^0'=last_copy_time^post10, tmp66^0'=last_copy_time^post10, a55^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 : -999+curtime^0-last_copy_time^0 <= 0, cost: 1
  22: l8 -> l7 : wakend^0'=1, 1000-curtime^0+last_copy_time^0 <= 0, cost: 1
  23: l9 -> l7 : -1+wakend^0 >= 0, cost: 1
  24: l9 -> l8 : curtime^0'=ret_time1010^post8, tmp99^0'=ret_time1010^post8, a88^0'=0, ret_time1010^0'=ret_time1010^post8, wakend^0 <= 0, cost: 1
  33: l12 -> l0 : wakend^0'=1, got_SIGHUP^0'=got_SIGHUP^post15, 0 == 0, cost: 2


Eliminating location l0 by chaining:

Applied chaining
First rule:
l12 -> l0 : wakend^0'=1, got_SIGHUP^0'=got_SIGHUP^post15, 0 == 0, cost: 2
Second rule:
l0 -> l1 : got_SIGHUP^0 <= 0, cost: 1
New rule:
l12 -> l1 : wakend^0'=1, got_SIGHUP^0'=got_SIGHUP^post15, (0 == 0 /\ got_SIGHUP^post15 <= 0), cost: 3

Applied simplification
Original rule:
l12 -> l1 : wakend^0'=1, got_SIGHUP^0'=got_SIGHUP^post15, (0 == 0 /\ got_SIGHUP^post15 <= 0), cost: 3
New rule:
l12 -> l1 : wakend^0'=1, got_SIGHUP^0'=got_SIGHUP^post15, got_SIGHUP^post15 <= 0, cost: 3

Applied chaining
First rule:
l12 -> l0 : wakend^0'=1, got_SIGHUP^0'=got_SIGHUP^post15, 0 == 0, cost: 2
Second rule:
l0 -> l2 : a33^0'=1, ___rho_1_^0'=ret_XLogArchivingActive44^post1, got_SIGHUP^0'=0, tt1^0'=ret_XLogArchivingActive44^post1, 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, wakend^0'=1, ___rho_1_^0'=ret_XLogArchivingActive44^post1, got_SIGHUP^0'=0, tt1^0'=ret_XLogArchivingActive44^post1, tmp2^0'=ret_XLogArchivingActive44^post1, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, (0 == 0 /\ -1+got_SIGHUP^post15 >= 0), cost: 3

Applied simplification
Original rule:
l12 -> l2 : a33^0'=1, wakend^0'=1, ___rho_1_^0'=ret_XLogArchivingActive44^post1, got_SIGHUP^0'=0, tt1^0'=ret_XLogArchivingActive44^post1, tmp2^0'=ret_XLogArchivingActive44^post1, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, (0 == 0 /\ -1+got_SIGHUP^post15 >= 0), cost: 3
New rule:
l12 -> l2 : a33^0'=1, wakend^0'=1, ___rho_1_^0'=ret_XLogArchivingActive44^post1, got_SIGHUP^0'=0, tt1^0'=ret_XLogArchivingActive44^post1, tmp2^0'=ret_XLogArchivingActive44^post1, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, -1+got_SIGHUP^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 : curtime^0'=ret_time1010^post8, tmp99^0'=ret_time1010^post8, a88^0'=0, ret_time1010^0'=ret_time1010^post8, wakend^0 <= 0, cost: 1
New rule:
l1 -> l8 : curtime^0'=ret_time1010^post8, tmp99^0'=ret_time1010^post8, a88^0'=0, ret_time1010^0'=ret_time1010^post8, wakend^0 <= 0, cost: 2

Applied chaining
First rule:
l1 -> l9 : wakend^0'=0, ret_time77^0'=last_copy_time^post10, last_copy_time^0'=last_copy_time^post10, tmp66^0'=last_copy_time^post10, a55^0'=0, -1+wakend^0 >= 0, cost: 1
Second rule:
l9 -> l8 : curtime^0'=ret_time1010^post8, tmp99^0'=ret_time1010^post8, a88^0'=0, ret_time1010^0'=ret_time1010^post8, wakend^0 <= 0, cost: 1
New rule:
l1 -> l8 : curtime^0'=ret_time1010^post8, tmp99^0'=ret_time1010^post8, wakend^0'=0, ret_time77^0'=last_copy_time^post10, last_copy_time^0'=last_copy_time^post10, a88^0'=0, tmp66^0'=last_copy_time^post10, ret_time1010^0'=ret_time1010^post8, a55^0'=0, (0 <= 0 /\ -1+wakend^0 >= 0), cost: 2

Applied simplification
Original rule:
l1 -> l8 : curtime^0'=ret_time1010^post8, tmp99^0'=ret_time1010^post8, wakend^0'=0, ret_time77^0'=last_copy_time^post10, last_copy_time^0'=last_copy_time^post10, a88^0'=0, tmp66^0'=last_copy_time^post10, ret_time1010^0'=ret_time1010^post8, a55^0'=0, (0 <= 0 /\ -1+wakend^0 >= 0), cost: 2
New rule:
l1 -> l8 : curtime^0'=ret_time1010^post8, tmp99^0'=ret_time1010^post8, wakend^0'=0, ret_time77^0'=last_copy_time^post10, last_copy_time^0'=last_copy_time^post10, a88^0'=0, tmp66^0'=last_copy_time^post10, ret_time1010^0'=ret_time1010^post8, a55^0'=0, -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 : -999+curtime^0-last_copy_time^0 <= 0, cost: 1
Second rule:
l7 -> l5 : TRUE, cost: 1
New rule:
l8 -> l5 : -999+curtime^0-last_copy_time^0 <= 0, cost: 2

Applied chaining
First rule:
l8 -> l7 : wakend^0'=1, 1000-curtime^0+last_copy_time^0 <= 0, cost: 1
Second rule:
l7 -> l5 : TRUE, cost: 1
New rule:
l8 -> l5 : wakend^0'=1, 1000-curtime^0+last_copy_time^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 : curtime^0'=ret_time1010^post8, tmp99^0'=ret_time1010^post8, a88^0'=0, ret_time1010^0'=ret_time1010^post8, wakend^0 <= 0, cost: 2
  40: l1 -> l8 : curtime^0'=ret_time1010^post8, tmp99^0'=ret_time1010^post8, wakend^0'=0, ret_time77^0'=last_copy_time^post10, last_copy_time^0'=last_copy_time^post10, a88^0'=0, tmp66^0'=last_copy_time^post10, ret_time1010^0'=ret_time1010^post8, a55^0'=0, -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 : -999+curtime^0-last_copy_time^0 <= 0, cost: 2
  42: l8 -> l5 : wakend^0'=1, 1000-curtime^0+last_copy_time^0 <= 0, cost: 2
  37: l12 -> l1 : wakend^0'=1, got_SIGHUP^0'=got_SIGHUP^post15, got_SIGHUP^post15 <= 0, cost: 3
  38: l12 -> l2 : a33^0'=1, wakend^0'=1, ___rho_1_^0'=ret_XLogArchivingActive44^post1, got_SIGHUP^0'=0, tt1^0'=ret_XLogArchivingActive44^post1, tmp2^0'=ret_XLogArchivingActive44^post1, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, -1+got_SIGHUP^post15 >= 0, cost: 3


Eliminating location l2 by chaining:

Applied chaining
First rule:
l12 -> l2 : a33^0'=1, wakend^0'=1, ___rho_1_^0'=ret_XLogArchivingActive44^post1, got_SIGHUP^0'=0, tt1^0'=ret_XLogArchivingActive44^post1, tmp2^0'=ret_XLogArchivingActive44^post1, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, -1+got_SIGHUP^post15 >= 0, cost: 3
Second rule:
l2 -> l1 : -1+tt1^0 >= 0, cost: 1
New rule:
l12 -> l1 : a33^0'=1, wakend^0'=1, ___rho_1_^0'=ret_XLogArchivingActive44^post1, got_SIGHUP^0'=0, tt1^0'=ret_XLogArchivingActive44^post1, tmp2^0'=ret_XLogArchivingActive44^post1, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, (-1+ret_XLogArchivingActive44^post1 >= 0 /\ -1+got_SIGHUP^post15 >= 0), cost: 4

Applied chaining
First rule:
l12 -> l2 : a33^0'=1, wakend^0'=1, ___rho_1_^0'=ret_XLogArchivingActive44^post1, got_SIGHUP^0'=0, tt1^0'=ret_XLogArchivingActive44^post1, tmp2^0'=ret_XLogArchivingActive44^post1, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, -1+got_SIGHUP^post15 >= 0, cost: 3
Second rule:
l2 -> l5 : tt1^0 <= 0, cost: 1
New rule:
l12 -> l5 : a33^0'=1, wakend^0'=1, ___rho_1_^0'=ret_XLogArchivingActive44^post1, got_SIGHUP^0'=0, tt1^0'=ret_XLogArchivingActive44^post1, tmp2^0'=ret_XLogArchivingActive44^post1, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, (ret_XLogArchivingActive44^post1 <= 0 /\ -1+got_SIGHUP^post15 >= 0), cost: 4

Applied deletion
Removed the following rules: 29 30 38

Eliminating location l8 by chaining:

Applied chaining
First rule:
l1 -> l8 : curtime^0'=ret_time1010^post8, tmp99^0'=ret_time1010^post8, a88^0'=0, ret_time1010^0'=ret_time1010^post8, wakend^0 <= 0, cost: 2
Second rule:
l8 -> l5 : -999+curtime^0-last_copy_time^0 <= 0, cost: 2
New rule:
l1 -> l5 : curtime^0'=ret_time1010^post8, tmp99^0'=ret_time1010^post8, a88^0'=0, ret_time1010^0'=ret_time1010^post8, (wakend^0 <= 0 /\ -999-last_copy_time^0+ret_time1010^post8 <= 0), cost: 4

Applied chaining
First rule:
l1 -> l8 : curtime^0'=ret_time1010^post8, tmp99^0'=ret_time1010^post8, a88^0'=0, ret_time1010^0'=ret_time1010^post8, wakend^0 <= 0, cost: 2
Second rule:
l8 -> l5 : wakend^0'=1, 1000-curtime^0+last_copy_time^0 <= 0, cost: 2
New rule:
l1 -> l5 : curtime^0'=ret_time1010^post8, tmp99^0'=ret_time1010^post8, wakend^0'=1, a88^0'=0, ret_time1010^0'=ret_time1010^post8, (1000+last_copy_time^0-ret_time1010^post8 <= 0 /\ wakend^0 <= 0), cost: 4

Applied chaining
First rule:
l1 -> l8 : curtime^0'=ret_time1010^post8, tmp99^0'=ret_time1010^post8, wakend^0'=0, ret_time77^0'=last_copy_time^post10, last_copy_time^0'=last_copy_time^post10, a88^0'=0, tmp66^0'=last_copy_time^post10, ret_time1010^0'=ret_time1010^post8, a55^0'=0, -1+wakend^0 >= 0, cost: 2
Second rule:
l8 -> l5 : -999+curtime^0-last_copy_time^0 <= 0, cost: 2
New rule:
l1 -> l5 : curtime^0'=ret_time1010^post8, tmp99^0'=ret_time1010^post8, wakend^0'=0, ret_time77^0'=last_copy_time^post10, last_copy_time^0'=last_copy_time^post10, a88^0'=0, tmp66^0'=last_copy_time^post10, ret_time1010^0'=ret_time1010^post8, a55^0'=0, (-999-last_copy_time^post10+ret_time1010^post8 <= 0 /\ -1+wakend^0 >= 0), cost: 4

Applied chaining
First rule:
l1 -> l8 : curtime^0'=ret_time1010^post8, tmp99^0'=ret_time1010^post8, wakend^0'=0, ret_time77^0'=last_copy_time^post10, last_copy_time^0'=last_copy_time^post10, a88^0'=0, tmp66^0'=last_copy_time^post10, ret_time1010^0'=ret_time1010^post8, a55^0'=0, -1+wakend^0 >= 0, cost: 2
Second rule:
l8 -> l5 : wakend^0'=1, 1000-curtime^0+last_copy_time^0 <= 0, cost: 2
New rule:
l1 -> l5 : curtime^0'=ret_time1010^post8, tmp99^0'=ret_time1010^post8, wakend^0'=1, ret_time77^0'=last_copy_time^post10, last_copy_time^0'=last_copy_time^post10, a88^0'=0, tmp66^0'=last_copy_time^post10, ret_time1010^0'=ret_time1010^post8, a55^0'=0, (-1+wakend^0 >= 0 /\ 1000+last_copy_time^post10-ret_time1010^post8 <= 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 : curtime^0'=ret_time1010^post8, tmp99^0'=ret_time1010^post8, a88^0'=0, ret_time1010^0'=ret_time1010^post8, (wakend^0 <= 0 /\ -999-last_copy_time^0+ret_time1010^post8 <= 0), cost: 4
  46: l1 -> l5 : curtime^0'=ret_time1010^post8, tmp99^0'=ret_time1010^post8, wakend^0'=1, a88^0'=0, ret_time1010^0'=ret_time1010^post8, (1000+last_copy_time^0-ret_time1010^post8 <= 0 /\ wakend^0 <= 0), cost: 4
  47: l1 -> l5 : curtime^0'=ret_time1010^post8, tmp99^0'=ret_time1010^post8, wakend^0'=0, ret_time77^0'=last_copy_time^post10, last_copy_time^0'=last_copy_time^post10, a88^0'=0, tmp66^0'=last_copy_time^post10, ret_time1010^0'=ret_time1010^post8, a55^0'=0, (-999-last_copy_time^post10+ret_time1010^post8 <= 0 /\ -1+wakend^0 >= 0), cost: 4
  48: l1 -> l5 : curtime^0'=ret_time1010^post8, tmp99^0'=ret_time1010^post8, wakend^0'=1, ret_time77^0'=last_copy_time^post10, last_copy_time^0'=last_copy_time^post10, a88^0'=0, tmp66^0'=last_copy_time^post10, ret_time1010^0'=ret_time1010^post8, a55^0'=0, (-1+wakend^0 >= 0 /\ 1000+last_copy_time^post10-ret_time1010^post8 <= 0), cost: 4
  36: l5 -> [13] : TRUE, cost: NONTERM
  37: l12 -> l1 : wakend^0'=1, got_SIGHUP^0'=got_SIGHUP^post15, got_SIGHUP^post15 <= 0, cost: 3
  43: l12 -> l1 : a33^0'=1, wakend^0'=1, ___rho_1_^0'=ret_XLogArchivingActive44^post1, got_SIGHUP^0'=0, tt1^0'=ret_XLogArchivingActive44^post1, tmp2^0'=ret_XLogArchivingActive44^post1, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, (-1+ret_XLogArchivingActive44^post1 >= 0 /\ -1+got_SIGHUP^post15 >= 0), cost: 4
  44: l12 -> l5 : a33^0'=1, wakend^0'=1, ___rho_1_^0'=ret_XLogArchivingActive44^post1, got_SIGHUP^0'=0, tt1^0'=ret_XLogArchivingActive44^post1, tmp2^0'=ret_XLogArchivingActive44^post1, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, (ret_XLogArchivingActive44^post1 <= 0 /\ -1+got_SIGHUP^post15 >= 0), cost: 4


Eliminating location l1 by chaining:

Applied chaining
First rule:
l12 -> l1 : wakend^0'=1, got_SIGHUP^0'=got_SIGHUP^post15, got_SIGHUP^post15 <= 0, cost: 3
Second rule:
l1 -> l5 : curtime^0'=ret_time1010^post8, tmp99^0'=ret_time1010^post8, wakend^0'=0, ret_time77^0'=last_copy_time^post10, last_copy_time^0'=last_copy_time^post10, a88^0'=0, tmp66^0'=last_copy_time^post10, ret_time1010^0'=ret_time1010^post8, a55^0'=0, (-999-last_copy_time^post10+ret_time1010^post8 <= 0 /\ -1+wakend^0 >= 0), cost: 4
New rule:
l12 -> l5 : curtime^0'=ret_time1010^post8, tmp99^0'=ret_time1010^post8, wakend^0'=0, ret_time77^0'=last_copy_time^post10, last_copy_time^0'=last_copy_time^post10, a88^0'=0, tmp66^0'=last_copy_time^post10, ret_time1010^0'=ret_time1010^post8, got_SIGHUP^0'=got_SIGHUP^post15, a55^0'=0, (0 >= 0 /\ -999-last_copy_time^post10+ret_time1010^post8 <= 0 /\ got_SIGHUP^post15 <= 0), cost: 7

Applied simplification
Original rule:
l12 -> l5 : curtime^0'=ret_time1010^post8, tmp99^0'=ret_time1010^post8, wakend^0'=0, ret_time77^0'=last_copy_time^post10, last_copy_time^0'=last_copy_time^post10, a88^0'=0, tmp66^0'=last_copy_time^post10, ret_time1010^0'=ret_time1010^post8, got_SIGHUP^0'=got_SIGHUP^post15, a55^0'=0, (0 >= 0 /\ -999-last_copy_time^post10+ret_time1010^post8 <= 0 /\ got_SIGHUP^post15 <= 0), cost: 7
New rule:
l12 -> l5 : curtime^0'=ret_time1010^post8, tmp99^0'=ret_time1010^post8, wakend^0'=0, ret_time77^0'=last_copy_time^post10, last_copy_time^0'=last_copy_time^post10, a88^0'=0, tmp66^0'=last_copy_time^post10, ret_time1010^0'=ret_time1010^post8, got_SIGHUP^0'=got_SIGHUP^post15, a55^0'=0, (-999-last_copy_time^post10+ret_time1010^post8 <= 0 /\ got_SIGHUP^post15 <= 0), cost: 7

Applied chaining
First rule:
l12 -> l1 : wakend^0'=1, got_SIGHUP^0'=got_SIGHUP^post15, got_SIGHUP^post15 <= 0, cost: 3
Second rule:
l1 -> l5 : curtime^0'=ret_time1010^post8, tmp99^0'=ret_time1010^post8, wakend^0'=1, ret_time77^0'=last_copy_time^post10, last_copy_time^0'=last_copy_time^post10, a88^0'=0, tmp66^0'=last_copy_time^post10, ret_time1010^0'=ret_time1010^post8, a55^0'=0, (-1+wakend^0 >= 0 /\ 1000+last_copy_time^post10-ret_time1010^post8 <= 0), cost: 4
New rule:
l12 -> l5 : curtime^0'=ret_time1010^post8, tmp99^0'=ret_time1010^post8, wakend^0'=1, ret_time77^0'=last_copy_time^post10, last_copy_time^0'=last_copy_time^post10, a88^0'=0, tmp66^0'=last_copy_time^post10, ret_time1010^0'=ret_time1010^post8, got_SIGHUP^0'=got_SIGHUP^post15, a55^0'=0, (0 >= 0 /\ got_SIGHUP^post15 <= 0 /\ 1000+last_copy_time^post10-ret_time1010^post8 <= 0), cost: 7

Applied simplification
Original rule:
l12 -> l5 : curtime^0'=ret_time1010^post8, tmp99^0'=ret_time1010^post8, wakend^0'=1, ret_time77^0'=last_copy_time^post10, last_copy_time^0'=last_copy_time^post10, a88^0'=0, tmp66^0'=last_copy_time^post10, ret_time1010^0'=ret_time1010^post8, got_SIGHUP^0'=got_SIGHUP^post15, a55^0'=0, (0 >= 0 /\ got_SIGHUP^post15 <= 0 /\ 1000+last_copy_time^post10-ret_time1010^post8 <= 0), cost: 7
New rule:
l12 -> l5 : curtime^0'=ret_time1010^post8, tmp99^0'=ret_time1010^post8, wakend^0'=1, ret_time77^0'=last_copy_time^post10, last_copy_time^0'=last_copy_time^post10, a88^0'=0, tmp66^0'=last_copy_time^post10, ret_time1010^0'=ret_time1010^post8, got_SIGHUP^0'=got_SIGHUP^post15, a55^0'=0, (got_SIGHUP^post15 <= 0 /\ 1000+last_copy_time^post10-ret_time1010^post8 <= 0), cost: 7

Applied chaining
First rule:
l12 -> l1 : a33^0'=1, wakend^0'=1, ___rho_1_^0'=ret_XLogArchivingActive44^post1, got_SIGHUP^0'=0, tt1^0'=ret_XLogArchivingActive44^post1, tmp2^0'=ret_XLogArchivingActive44^post1, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, (-1+ret_XLogArchivingActive44^post1 >= 0 /\ -1+got_SIGHUP^post15 >= 0), cost: 4
Second rule:
l1 -> l5 : curtime^0'=ret_time1010^post8, tmp99^0'=ret_time1010^post8, wakend^0'=0, ret_time77^0'=last_copy_time^post10, last_copy_time^0'=last_copy_time^post10, a88^0'=0, tmp66^0'=last_copy_time^post10, ret_time1010^0'=ret_time1010^post8, a55^0'=0, (-999-last_copy_time^post10+ret_time1010^post8 <= 0 /\ -1+wakend^0 >= 0), cost: 4
New rule:
l12 -> l5 : curtime^0'=ret_time1010^post8, tmp99^0'=ret_time1010^post8, a33^0'=1, wakend^0'=0, ret_time77^0'=last_copy_time^post10, last_copy_time^0'=last_copy_time^post10, a88^0'=0, tmp66^0'=last_copy_time^post10, ___rho_1_^0'=ret_XLogArchivingActive44^post1, ret_time1010^0'=ret_time1010^post8, got_SIGHUP^0'=0, tt1^0'=ret_XLogArchivingActive44^post1, a55^0'=0, tmp2^0'=ret_XLogArchivingActive44^post1, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, (0 >= 0 /\ -1+ret_XLogArchivingActive44^post1 >= 0 /\ -999-last_copy_time^post10+ret_time1010^post8 <= 0 /\ -1+got_SIGHUP^post15 >= 0), cost: 8

Applied simplification
Original rule:
l12 -> l5 : curtime^0'=ret_time1010^post8, tmp99^0'=ret_time1010^post8, a33^0'=1, wakend^0'=0, ret_time77^0'=last_copy_time^post10, last_copy_time^0'=last_copy_time^post10, a88^0'=0, tmp66^0'=last_copy_time^post10, ___rho_1_^0'=ret_XLogArchivingActive44^post1, ret_time1010^0'=ret_time1010^post8, got_SIGHUP^0'=0, tt1^0'=ret_XLogArchivingActive44^post1, a55^0'=0, tmp2^0'=ret_XLogArchivingActive44^post1, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, (0 >= 0 /\ -1+ret_XLogArchivingActive44^post1 >= 0 /\ -999-last_copy_time^post10+ret_time1010^post8 <= 0 /\ -1+got_SIGHUP^post15 >= 0), cost: 8
New rule:
l12 -> l5 : curtime^0'=ret_time1010^post8, tmp99^0'=ret_time1010^post8, a33^0'=1, wakend^0'=0, ret_time77^0'=last_copy_time^post10, last_copy_time^0'=last_copy_time^post10, a88^0'=0, tmp66^0'=last_copy_time^post10, ___rho_1_^0'=ret_XLogArchivingActive44^post1, ret_time1010^0'=ret_time1010^post8, got_SIGHUP^0'=0, tt1^0'=ret_XLogArchivingActive44^post1, a55^0'=0, tmp2^0'=ret_XLogArchivingActive44^post1, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, (-1+ret_XLogArchivingActive44^post1 >= 0 /\ -999-last_copy_time^post10+ret_time1010^post8 <= 0 /\ -1+got_SIGHUP^post15 >= 0), cost: 8

Applied chaining
First rule:
l12 -> l1 : a33^0'=1, wakend^0'=1, ___rho_1_^0'=ret_XLogArchivingActive44^post1, got_SIGHUP^0'=0, tt1^0'=ret_XLogArchivingActive44^post1, tmp2^0'=ret_XLogArchivingActive44^post1, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, (-1+ret_XLogArchivingActive44^post1 >= 0 /\ -1+got_SIGHUP^post15 >= 0), cost: 4
Second rule:
l1 -> l5 : curtime^0'=ret_time1010^post8, tmp99^0'=ret_time1010^post8, wakend^0'=1, ret_time77^0'=last_copy_time^post10, last_copy_time^0'=last_copy_time^post10, a88^0'=0, tmp66^0'=last_copy_time^post10, ret_time1010^0'=ret_time1010^post8, a55^0'=0, (-1+wakend^0 >= 0 /\ 1000+last_copy_time^post10-ret_time1010^post8 <= 0), cost: 4
New rule:
l12 -> l5 : curtime^0'=ret_time1010^post8, tmp99^0'=ret_time1010^post8, a33^0'=1, wakend^0'=1, ret_time77^0'=last_copy_time^post10, last_copy_time^0'=last_copy_time^post10, a88^0'=0, tmp66^0'=last_copy_time^post10, ___rho_1_^0'=ret_XLogArchivingActive44^post1, ret_time1010^0'=ret_time1010^post8, got_SIGHUP^0'=0, tt1^0'=ret_XLogArchivingActive44^post1, a55^0'=0, tmp2^0'=ret_XLogArchivingActive44^post1, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, (0 >= 0 /\ -1+ret_XLogArchivingActive44^post1 >= 0 /\ -1+got_SIGHUP^post15 >= 0 /\ 1000+last_copy_time^post10-ret_time1010^post8 <= 0), cost: 8

Applied simplification
Original rule:
l12 -> l5 : curtime^0'=ret_time1010^post8, tmp99^0'=ret_time1010^post8, a33^0'=1, wakend^0'=1, ret_time77^0'=last_copy_time^post10, last_copy_time^0'=last_copy_time^post10, a88^0'=0, tmp66^0'=last_copy_time^post10, ___rho_1_^0'=ret_XLogArchivingActive44^post1, ret_time1010^0'=ret_time1010^post8, got_SIGHUP^0'=0, tt1^0'=ret_XLogArchivingActive44^post1, a55^0'=0, tmp2^0'=ret_XLogArchivingActive44^post1, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, (0 >= 0 /\ -1+ret_XLogArchivingActive44^post1 >= 0 /\ -1+got_SIGHUP^post15 >= 0 /\ 1000+last_copy_time^post10-ret_time1010^post8 <= 0), cost: 8
New rule:
l12 -> l5 : curtime^0'=ret_time1010^post8, tmp99^0'=ret_time1010^post8, a33^0'=1, wakend^0'=1, ret_time77^0'=last_copy_time^post10, last_copy_time^0'=last_copy_time^post10, a88^0'=0, tmp66^0'=last_copy_time^post10, ___rho_1_^0'=ret_XLogArchivingActive44^post1, ret_time1010^0'=ret_time1010^post8, got_SIGHUP^0'=0, tt1^0'=ret_XLogArchivingActive44^post1, a55^0'=0, tmp2^0'=ret_XLogArchivingActive44^post1, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, (-1+ret_XLogArchivingActive44^post1 >= 0 /\ -1+got_SIGHUP^post15 >= 0 /\ 1000+last_copy_time^post10-ret_time1010^post8 <= 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, wakend^0'=1, ___rho_1_^0'=ret_XLogArchivingActive44^post1, got_SIGHUP^0'=0, tt1^0'=ret_XLogArchivingActive44^post1, tmp2^0'=ret_XLogArchivingActive44^post1, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, (ret_XLogArchivingActive44^post1 <= 0 /\ -1+got_SIGHUP^post15 >= 0), cost: 4
Second rule:
l5 -> [13] : TRUE, cost: NONTERM
New rule:
l12 -> [13] : (ret_XLogArchivingActive44^post1 <= 0 /\ -1+got_SIGHUP^post15 >= 0), cost: NONTERM

Applied chaining
First rule:
l12 -> l5 : curtime^0'=ret_time1010^post8, tmp99^0'=ret_time1010^post8, wakend^0'=0, ret_time77^0'=last_copy_time^post10, last_copy_time^0'=last_copy_time^post10, a88^0'=0, tmp66^0'=last_copy_time^post10, ret_time1010^0'=ret_time1010^post8, got_SIGHUP^0'=got_SIGHUP^post15, a55^0'=0, (-999-last_copy_time^post10+ret_time1010^post8 <= 0 /\ got_SIGHUP^post15 <= 0), cost: 7
Second rule:
l5 -> [13] : TRUE, cost: NONTERM
New rule:
l12 -> [13] : (-999-last_copy_time^post10+ret_time1010^post8 <= 0 /\ got_SIGHUP^post15 <= 0), cost: NONTERM

Applied chaining
First rule:
l12 -> l5 : curtime^0'=ret_time1010^post8, tmp99^0'=ret_time1010^post8, wakend^0'=1, ret_time77^0'=last_copy_time^post10, last_copy_time^0'=last_copy_time^post10, a88^0'=0, tmp66^0'=last_copy_time^post10, ret_time1010^0'=ret_time1010^post8, got_SIGHUP^0'=got_SIGHUP^post15, a55^0'=0, (got_SIGHUP^post15 <= 0 /\ 1000+last_copy_time^post10-ret_time1010^post8 <= 0), cost: 7
Second rule:
l5 -> [13] : TRUE, cost: NONTERM
New rule:
l12 -> [13] : (got_SIGHUP^post15 <= 0 /\ 1000+last_copy_time^post10-ret_time1010^post8 <= 0), cost: NONTERM

Applied chaining
First rule:
l12 -> l5 : curtime^0'=ret_time1010^post8, tmp99^0'=ret_time1010^post8, a33^0'=1, wakend^0'=0, ret_time77^0'=last_copy_time^post10, last_copy_time^0'=last_copy_time^post10, a88^0'=0, tmp66^0'=last_copy_time^post10, ___rho_1_^0'=ret_XLogArchivingActive44^post1, ret_time1010^0'=ret_time1010^post8, got_SIGHUP^0'=0, tt1^0'=ret_XLogArchivingActive44^post1, a55^0'=0, tmp2^0'=ret_XLogArchivingActive44^post1, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, (-1+ret_XLogArchivingActive44^post1 >= 0 /\ -999-last_copy_time^post10+ret_time1010^post8 <= 0 /\ -1+got_SIGHUP^post15 >= 0), cost: 8
Second rule:
l5 -> [13] : TRUE, cost: NONTERM
New rule:
l12 -> [13] : (-1+ret_XLogArchivingActive44^post1 >= 0 /\ -999-last_copy_time^post10+ret_time1010^post8 <= 0 /\ -1+got_SIGHUP^post15 >= 0), cost: NONTERM

Applied chaining
First rule:
l12 -> l5 : curtime^0'=ret_time1010^post8, tmp99^0'=ret_time1010^post8, a33^0'=1, wakend^0'=1, ret_time77^0'=last_copy_time^post10, last_copy_time^0'=last_copy_time^post10, a88^0'=0, tmp66^0'=last_copy_time^post10, ___rho_1_^0'=ret_XLogArchivingActive44^post1, ret_time1010^0'=ret_time1010^post8, got_SIGHUP^0'=0, tt1^0'=ret_XLogArchivingActive44^post1, a55^0'=0, tmp2^0'=ret_XLogArchivingActive44^post1, ret_XLogArchivingActive44^0'=ret_XLogArchivingActive44^post1, (-1+ret_XLogArchivingActive44^post1 >= 0 /\ -1+got_SIGHUP^post15 >= 0 /\ 1000+last_copy_time^post10-ret_time1010^post8 <= 0), cost: 8
Second rule:
l5 -> [13] : TRUE, cost: NONTERM
New rule:
l12 -> [13] : (-1+ret_XLogArchivingActive44^post1 >= 0 /\ -1+got_SIGHUP^post15 >= 0 /\ 1000+last_copy_time^post10-ret_time1010^post8 <= 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] : (ret_XLogArchivingActive44^post1 <= 0 /\ -1+got_SIGHUP^post15 >= 0), cost: NONTERM
  54: l12 -> [13] : (-999-last_copy_time^post10+ret_time1010^post8 <= 0 /\ got_SIGHUP^post15 <= 0), cost: NONTERM
  55: l12 -> [13] : (got_SIGHUP^post15 <= 0 /\ 1000+last_copy_time^post10-ret_time1010^post8 <= 0), cost: NONTERM
  56: l12 -> [13] : (-1+ret_XLogArchivingActive44^post1 >= 0 /\ -999-last_copy_time^post10+ret_time1010^post8 <= 0 /\ -1+got_SIGHUP^post15 >= 0), cost: NONTERM
  57: l12 -> [13] : (-1+ret_XLogArchivingActive44^post1 >= 0 /\ -1+got_SIGHUP^post15 >= 0 /\ 1000+last_copy_time^post10-ret_time1010^post8 <= 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:  (ret_XLogArchivingActive44^post1 <= 0 /\ -1+got_SIGHUP^post15 >= 0)