(330) * Warning 330 at C:\gh\3\_work\FStar\FStar\fstar\ulib\experimental\FStar.NMST.fst(200,45-200,58): - Polymonadic binds ((DIV, NMSTATE) |> NMSTATE) in this case) is an experimental feature;it is subject to some redesign in the future. Please keep us informed (on github etc.) about how you are using it

(318) * Warning 318 at C:\gh\3\_work\FStar\FStar\fstar\ulib\FStar.TSet.fst(27,4-27,7): - Values of type `set` cannot be erased during extraction, but the `must_erase_for_extraction` attribute claims that it can. - Please remove the attribute.

(318) * Warning 318 at C:\gh\3\_work\FStar\FStar\fstar\ulib\FStar.GSet.fst(23,4-23,7): - Values of type `set` cannot be erased during extraction, but the `must_erase_for_extraction` attribute claims that it can. - Please remove the attribute.

(352) * Warning 352 at C:\gh\3\_work\FStar\FStar\fstar\ulib\experimental\FStar.MST.fst(247,42-247,60): - Combinator FStar.MSTTotal.MSTATETOT ~> FStar.MST.MSTATE is not a substitutive indexed effect combinator, it is better to make it one if possible for better performance and ease of use

(330) * Warning 330 at C:\gh\3\_work\FStar\FStar\fstar\ulib\experimental\FStar.MST.fst(222,43-222,55): - Polymonadic binds ((DIV, MSTATE) |> MSTATE) in this case) is an experimental feature;it is subject to some redesign in the future. Please keep us informed (on github etc.) about how you are using it

(318) * Warning 318 at C:\gh\3\_work\FStar\FStar\fstar\ulib\FStar.GhostSet.fst(23,4-23,7): - Values of type `set` cannot be erased during extraction, but the `must_erase_for_extraction` attribute claims that it can. - Please remove the attribute.

(242) * Warning 242 at C:\gh\3\_work\FStar\FStar\fstar\ulib\FStar.WellFounded.fst(122,0-131,33): - Definitions of inner let-rec aux and its enclosing top-level letbinding are not encoded to the solver, you will only be able to reason with their types - Also see: C:\gh\3\_work\FStar\FStar\fstar\ulib\FStar.WellFounded.fst(126,12-126,15)

(242) * Warning 242 at C:\gh\3\_work\FStar\FStar\fstar\ulib\FStar.WellFounded.fst(122,0-131,33): - Definitions of inner let-rec aux and its enclosing top-level letbinding are not encoded to the solver, you will only be able to reason with their types - Also see: C:\gh\3\_work\FStar\FStar\fstar\ulib\FStar.WellFounded.fst(86,12-86,15)

(271) * Warning 271 at C:\gh\3\_work\FStar\FStar\fstar\ulib\FStar.UInt.fsti(435,8-435,51): - Pattern uses these theory symbols or terms that should not be in an SMT pattern: Prims.op_Subtraction