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,
	__const_8_0 -__const_8_post == 0,
	__const_7_0 -__const_7_post == 0,
	__const_6_0 -__const_6_post == 0,
	__const_63_0 -__const_63_post == 0,
	__const_5_0 -__const_5_post == 0,
	__const_41_0 -__const_41_post == 0,
	__const_37_0 -__const_37_post == 0,
	__const_36_0 -__const_36_post == 0,
	__const_35_0 -__const_35_post == 0,
	__const_34_0 -__const_34_post == 0,
	__const_33_0 -__const_33_post == 0,
	__const_32_0 -__const_32_post == 0,
	__const_31_0 -__const_31_post == 0,
	__const_30_0 -__const_30_post == 0,
	__const_29_0 -__const_29_post == 0,
	__const_28_0 -__const_28_post == 0,
	__const_27_0 -__const_27_post == 0,
	__const_26_0 -__const_26_post == 0,
	__const_25_0 -__const_25_post == 0,
	__const_255_0 -__const_255_post == 0,
	__const_24_0 -__const_24_post == 0,
	__const_15_0 -__const_15_post == 0,
	__const_127_0 -__const_127_post == 0,
	__const_11_0 -__const_11_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 -X99 == 0,
	y6464_0 -X98 == 0,
	y2929_0 -X97 == 0,
	y2323_0 -X96 == 0,
	y1414_0 -X95 == 0,
	x66_0 -X94 == 0,
	DeviceObject_0 -X93 == 0,
	x6363_0 -X92 == 0,
	x4646_0 -X91 == 0,
	x2828_0 -X90 == 0,
	x2222_0 -X89 == 0,
	x1313_0 -X88 == 0,
	x1010_0 -X87 == 0,
	status_0 -X86 == 0,
	length_0 -X85 == 0,
	X84 == 0,
	X83 == 0,
	ip1919_0 -X82 == 0,
	ip1818_0 -X81 == 0,
	i6262_0 -X80 == 0,
	i5858_0 -X79 == 0,
	i55_0 -X78 == 0,
	i5454_0 -X77 == 0,
	i5050_0 -X76 == 0,
	i4545_0 -X75 == 0,
	i4141_0 -X74 == 0,
	i3737_0 -X73 == 0,
	i3333_0 -X72 == 0,
	i2727_0 -X71 == 0,
	i2121_0 -X70 == 0,
	i1212_0 -X69 == 0,
	__rho_9__0 -X68 == 0,
	__rho_91__0 -X67 == 0,
	__rho_8__0 -X66 == 0,
	__rho_7__0 -X65 == 0,
	__rho_6__0 -X64 == 0,
	__rho_5__0 -X63 == 0,
	__rho_4__0 -X62 == 0,
	__rho_3__0 -X61 == 0,
	__rho_34__0 -X60 == 0,
	__rho_33__0 -X59 == 0,
	__rho_32__0 -X58 == 0,
	__rho_31__0 -X57 == 0,
	__rho_30__0 -X56 == 0,
	__rho_2__0 -X55 == 0,
	__rho_29__0 -X54 == 0,
	__rho_28__0 -X53 == 0,
	__rho_27__0 -X52 == 0,
	__rho_26__0 -X51 == 0,
	__rho_25__0 -X50 == 0,
	__rho_24__0 -X49 == 0,
	__rho_23__0 -X48 == 0,
	__rho_22__0 -X47 == 0,
	__rho_21__0 -X46 == 0,
	__rho_20__0 -X45 == 0,
	__rho_1__0 -X44 == 0,
	__rho_19__0 -X43 == 0,
	__rho_18__0 -X42 == 0,
	__rho_17__0 -X41 == 0,
	__rho_16__0 -X40 == 0,
	__rho_15__0 -X39 == 0,
	__rho_14__0 -X38 == 0,
	__rho_13__0 -X37 == 0,
	__rho_12__0 -X36 == 0,
	__rho_11__0 -X35 == 0,
	__rho_10__0 -X34 == 0,
	__const_8_0 -X33 == 0,
	__const_7_0 -X32 == 0,
	__const_6_0 -X31 == 0,
	__const_63_0 -X30 == 0,
	__const_5_0 -X29 == 0,
	__const_41_0 -X28 == 0,
	__const_37_0 -X27 == 0,
	__const_36_0 -X26 == 0,
	__const_35_0 -X25 == 0,
	__const_34_0 -X24 == 0,
	__const_33_0 -X23 == 0,
	__const_32_0 -X22 == 0,
	__const_31_0 -X21 == 0,
	__const_30_0 -X20 == 0,
	__const_29_0 -X19 == 0,
	__const_28_0 -X18 == 0,
	__const_27_0 -X17 == 0,
	__const_26_0 -X16 == 0,
	__const_25_0 -X15 == 0,
	__const_255_0 -X14 == 0,
	__const_24_0 -X13 == 0,
	__const_15_0 -X12 == 0,
	__const_127_0 -X11 == 0,
	__const_11_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