(318) * Warning 318 at /home/runner/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.

(271) * Warning 271 at /home/runner/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

(318) * Warning 318 at /home/runner/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 /home/runner/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: /home/runner/work/FStar/FStar/fstar/ulib/FStar.WellFounded.fst:86.12-86.15

(242) * Warning 242 at /home/runner/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: /home/runner/work/FStar/FStar/fstar/ulib/FStar.WellFounded.fst:126.12-126.15

(271) * Warning 271 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.UInt.fst:293.8-293.25: - Pattern uses these theory symbols or terms that should not be in an SMT pattern: Prims.op_Subtraction - See also /home/runner/work/FStar/FStar/fstar/ulib/FStar.UInt.fsti:435.8-435.51

(271) * Warning 271 at /home/runner/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

(242) * Warning 242 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.LexicographicOrdering.fsti:187.0-194.59: - Definitions of inner let-rec lex_t_wf_aux_y and its enclosing top-level letbinding are not encoded to the solver, you will only be able to reason with their types - Also see: /home/runner/work/FStar/FStar/fstar/ulib/FStar.LexicographicOrdering.fst:75.14-75.28

(242) * Warning 242 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.LexicographicOrdering.fsti:187.0-194.59: - Definitions of inner let-rec get_acc and its enclosing top-level letbinding are not encoded to the solver, you will only be able to reason with their types - Also see: /home/runner/work/FStar/FStar/fstar/ulib/FStar.LexicographicOrdering.fst:124.10-124.17