NO
Nontermination proof succeeded
Found this recurrent set for cutpoint 15: DName_0 == 1 and DName_post == 1 and PdoType_0 == 0 and Pdolen_0 == 0 and ____rho_2__post == 1 and a11_post == 0 and b22_post == 0 and c33_post == 0 and d44_post == 0 and dcIdi_0 == 0 and i_0 == -1 and lptNamei_0 == 0 and num_0 == 0 and num_post == 0 and ret_PPMakeDeviceName66_post == 1 and set_1 == 0 and set_2 == 1 and set_post == 0 and tmp55_post == 1 and unset_post == 0
Errors: