NO
Nontermination proof succeeded
Found this recurrent set for cutpoint 51: DeviceObject_0 == 0 and 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 == 0 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: