NO
Nontermination proof succeeded
Found this recurrent set for cutpoint 52: Irp_0 == 0 and Irql_0 == 0 and IsochDetachData_post == 0 and ___rho_10__post == 1 and ___rho_1__0 == 1 and ___rho_1__post == 1 and ___rho_2__post == 0 and ___rho_6__post == 0 and a11_post == 1 and a1818_post == 0 and b22_post == 0 and i___01313_post == 0 and i___01717_post == 0 and i___099_post == 0 and k1_0 == 0 and k1_post == 0 and k2_0 == 0 and k2_post == 0 and k3_0 == 1 and k3_post == 0 and keA_1 == 1 and keA_2 == 0 and keA_3 == 1 and keA_post == 0 and keR_1 == 1 and keR_2 == 0 and keR_3 == 1 and keR_post == 0 and ntStatus_post == 0 and ret_IoSetDeviceInterfaceState44_post == 0 and ret_t1394Diag_PnpStopDevice33_post == 0
Errors: