NO


NON-Termination:
----------------
SCC:
+--transitions: t122,t123
+--nodes: l21,l68
Closed walk: 2 -> t122, t123
Reachability checked!
- Recurrent Set Found:
{
	y77_0 -y77_post == 0,
	y6464_0 -y6464_post == 0,
	y2929_0 -y2929_post == 0,
	y2323_0 -y2323_post == 0,
	y1414_0 -y1414_post == 0,
	x66_0 -x66_post == 0,
	DeviceObject_0 -x6565_post == 0,
	x6363_0 -x6363_post == 0,
	x4646_0 -x4646_post == 0,
	x2828_0 -x2828_post == 0,
	x2222_0 -x2222_post == 0,
	x1313_0 -x1313_post == 0,
	x1010_0 -x1010_post == 0,
	status_0 -status_post == 0,
	length_0 -length_post == 0,
	keR_post == 0,
	keA_post == 0,
	ip1919_0 -ip1919_post == 0,
	ip1818_0 -ip1818_post == 0,
	i6262_0 -i6262_post == 0,
	i5858_0 -i5858_post == 0,
	i55_0 -i55_post == 0,
	i5454_0 -i5454_post == 0,
	i5050_0 -i5050_post == 0,
	i4545_0 -i4545_post == 0,
	i4141_0 -i4141_post == 0,
	i3737_0 -i3737_post == 0,
	i3333_0 -i3333_post == 0,
	i2727_0 -i2727_post == 0,
	i2121_0 -i2121_post == 0,
	i1212_0 -i1212_post == 0,
	___rho_9__0 -___rho_9__post == 0,
	___rho_91__0 -___rho_91__post == 0,
	___rho_8__0 -___rho_8__post == 0,
	___rho_7__0 -___rho_7__post == 0,
	___rho_6__0 -___rho_6__post == 0,
	___rho_5__0 -___rho_5__post == 0,
	___rho_4__0 -___rho_4__post == 0,
	___rho_3__0 -___rho_3__post == 0,
	___rho_34__0 -___rho_34__post == 0,
	___rho_33__0 -___rho_33__post == 0,
	___rho_32__0 -___rho_32__post == 0,
	___rho_31__0 -___rho_31__post == 0,
	___rho_30__0 -___rho_30__post == 0,
	___rho_2__0 -___rho_2__post == 0,
	___rho_29__0 -___rho_29__post == 0,
	___rho_28__0 -___rho_28__post == 0,
	___rho_27__0 -___rho_27__post == 0,
	___rho_26__0 -___rho_26__post == 0,
	___rho_25__0 -___rho_25__post == 0,
	___rho_24__0 -___rho_24__post == 0,
	___rho_23__0 -___rho_23__post == 0,
	___rho_22__0 -___rho_22__post == 0,
	___rho_21__0 -___rho_21__post == 0,
	___rho_20__0 -___rho_20__post == 0,
	___rho_1__0 -___rho_1__post == 0,
	___rho_19__0 -___rho_19__post == 0,
	___rho_18__0 -___rho_18__post == 0,
	___rho_17__0 -___rho_17__post == 0,
	___rho_16__0 -___rho_16__post == 0,
	___rho_15__0 -___rho_15__post == 0,
	___rho_14__0 -___rho_14__post == 0,
	___rho_13__0 -___rho_13__post == 0,
	___rho_12__0 -___rho_12__post == 0,
	___rho_11__0 -___rho_11__post == 0,
	___rho_10__0 -___rho_10__post == 0,
	OldIrql_0 -OldIrql_post == 0,
	Mask_0 -Mask_post == 0,
	LStop_0 -LStop_post == 0,
	LParity_0 -LParity_post == 0,
	LData_0 -LData_post == 0,
	Irp_0 -Irp_post == 0,
	DeviceObject_0 -DeviceObject_post == 0,
	CurrentWaitIrp_0 -CurrentWaitIrp_post == 0,
	CancelIrql_0 -CancelIrql_post == 0,
	CancelIrp_0 -CancelIrp_post == 0,
	y77_0 -X75 == 0,
	y6464_0 -X74 == 0,
	y2929_0 -X73 == 0,
	y2323_0 -X72 == 0,
	y1414_0 -X71 == 0,
	x66_0 -X70 == 0,
	DeviceObject_0 -X69 == 0,
	x6363_0 -X68 == 0,
	x4646_0 -X67 == 0,
	x2828_0 -X66 == 0,
	x2222_0 -X65 == 0,
	x1313_0 -X64 == 0,
	x1010_0 -X63 == 0,
	status_0 -X62 == 0,
	length_0 -X61 == 0,
	X60 == 0,
	X59 == 0,
	ip1919_0 -X58 == 0,
	ip1818_0 -X57 == 0,
	i6262_0 -X56 == 0,
	i5858_0 -X55 == 0,
	i55_0 -X54 == 0,
	i5454_0 -X53 == 0,
	i5050_0 -X52 == 0,
	i4545_0 -X51 == 0,
	i4141_0 -X50 == 0,
	i3737_0 -X49 == 0,
	i3333_0 -X48 == 0,
	i2727_0 -X47 == 0,
	i2121_0 -X46 == 0,
	i1212_0 -X45 == 0,
	___rho_9__0 -X44 == 0,
	___rho_91__0 -X43 == 0,
	___rho_8__0 -X42 == 0,
	___rho_7__0 -X41 == 0,
	___rho_6__0 -X40 == 0,
	___rho_5__0 -X39 == 0,
	___rho_4__0 -X38 == 0,
	___rho_3__0 -X37 == 0,
	___rho_34__0 -X36 == 0,
	___rho_33__0 -X35 == 0,
	___rho_32__0 -X34 == 0,
	___rho_31__0 -X33 == 0,
	___rho_30__0 -X32 == 0,
	___rho_2__0 -X31 == 0,
	___rho_29__0 -X30 == 0,
	___rho_28__0 -X29 == 0,
	___rho_27__0 -X28 == 0,
	___rho_26__0 -X27 == 0,
	___rho_25__0 -X26 == 0,
	___rho_24__0 -X25 == 0,
	___rho_23__0 -X24 == 0,
	___rho_22__0 -X23 == 0,
	___rho_21__0 -X22 == 0,
	___rho_20__0 -X21 == 0,
	___rho_1__0 -X20 == 0,
	___rho_19__0 -X19 == 0,
	___rho_18__0 -X18 == 0,
	___rho_17__0 -X17 == 0,
	___rho_16__0 -X16 == 0,
	___rho_15__0 -X15 == 0,
	___rho_14__0 -X14 == 0,
	___rho_13__0 -X13 == 0,
	___rho_12__0 -X12 == 0,
	___rho_11__0 -X11 == 0,
	___rho_10__0 -X10 == 0,
	OldIrql_0 -X9 == 0,
	Mask_0 -X8 == 0,
	LStop_0 -X7 == 0,
	LParity_0 -X6 == 0,
	LData_0 -X5 == 0,
	Irp_0 -X4 == 0,
	DeviceObject_0 -X3 == 0,
	CurrentWaitIrp_0 -X2 == 0,
	CancelIrql_0 -X1 == 0,
	CancelIrp_0 -X0 == 0,
	DeviceObject_0 -x6565_0 == 0,
	keR_0 == 0,
	keA_0 == 0
}
Connected Subgraphs where we couldn't prove Termination:
--------------------------------------------------------
SCC:
+--transitions: t26,t27
+--nodes: l17,l18
SCC:
+--transitions: t148,t149,t150,t79
+--nodes: l46,l47,l83


method 1