NO
Nontermination proof succeeded
Found this recurrent set for cutpoint 61: DeviceObject_0 == 0 and Irp_0 == 0 and Irql_0 == 0 and ___rho_10__post == 0 and ___rho_11__post == 0 and ___rho_12__post == 0 and ___rho_1__0 == 1 and ___rho_1__post == 1 and ___rho_4__post == 0 and ___rho_5__post == 0 and a11_post == 0 and b22_post == 0 and i___01313_post == 0 and i___02020_post == 0 and i___04040_post == 0 and i___04848_post == 0 and i___099_post == 0 and ioA_post == 0 and ioR_post == 0 and k1_0 == 0 and k1_post == 0 and k2_0 == 0 and k2_post == 0 and k3_0 == 0 and k3_post == 0 and k4_0 == 0 and k4_post == 0 and k5_0 == 0 and k5_post == 0 and keA_1 == 1 and keA_post == 0 and keR_1 == 1 and keR_post == 0 and ntStatus_0 == 0 and ntStatus_post == 0 and phi_io_compl_post == 0 and phi_nSUC_ret_post == 1 and ret_IoSetDeviceInterfaceState44_post == 0 and ret_t1394Diag_PnpStopDevice33_post == 0
Errors: