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

(271) * Warning 271 at /home/runner/work/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/ulib/FStar.UInt.fsti(435,8-435,51)

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

(288) * Warning 288 at /home/runner/work/FStar/FStar/ulib/FStar.Reflection.V2.Arith.fst(116,20-116,31): - FStar.Stubs.Tactics.V2.Builtins.term_eq_old is deprecated - Use Reflection.term_eq instead - See also /home/runner/work/FStar/FStar/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti(446,0-446,42)

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

(337) * Warning 337 at /home/runner/work/FStar/FStar/src/data/FStarC.RBSet.fst(105,30-105,31): - The operator '@' has been resolved to FStar.List.Tot.append even though FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop relying on this deprecated, special treatment of '@'.

(337) * Warning 337 at /home/runner/work/FStar/FStar/src/data/FStarC.RBSet.fst(105,36-105,37): - The operator '@' has been resolved to FStar.List.Tot.append even though FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop relying on this deprecated, special treatment of '@'.

(337) * Warning 337 at /home/runner/work/FStar/FStar/src/basic/FStarC.Plugins.fst(86,16-86,17): - The operator '@' has been resolved to FStar.List.Tot.append even though FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop relying on this deprecated, special treatment of '@'.

(337) * Warning 337 at /home/runner/work/FStar/FStar/src/basic/FStarC.Plugins.fst(87,16-87,17): - The operator '@' has been resolved to FStar.List.Tot.append even though FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop relying on this deprecated, special treatment of '@'.

(337) * Warning 337 at /home/runner/work/FStar/FStar/src/basic/FStarC.Plugins.fst(88,16-88,17): - The operator '@' has been resolved to FStar.List.Tot.append even though FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop relying on this deprecated, special treatment of '@'.

No files were found with the provided path: fstar/fstar-*.zip. No artifacts will be uploaded.

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

(288) * Warning 288 at ulib/FStar.Reflection.V2.Arith.fst(116,20-116,31): - FStar.Stubs.Tactics.V2.Builtins.term_eq_old is deprecated - Use Reflection.term_eq instead - See also ulib/FStar.Stubs.Tactics.V2.Builtins.fsti(446,0-446,42)

(271) * Warning 271 at ulib/legacy/FStar.Buffer.fst(1005,2-1005,69): - Pattern uses these theory symbols or terms that should not be in an SMT pattern: Prims.op_Addition

(271) * Warning 271 at ulib/legacy/FStar.Buffer.Quantifiers.fst(32,2-32,77): - Pattern uses these theory symbols or terms that should not be in an SMT pattern: Prims.op_Addition

(330) * Warning 330 at 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

(352) * Warning 352 at 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 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

(352) * Warning 352 at ulib/experimental/FStar.NMST.fst(224,45-224,65): - Combinator FStar.NMSTTotal.NMSTATETOT ~> FStar.NMST.NMSTATE is not a substitutive indexed effect combinator, it is better to make it one if possible for better performance and ease of use

(318) * Warning 318 at ulib/FStar.SizeT.fst(35,4-35,12): - Values of type `fits_u32` will be erased during extraction, but its interface hides this fact. - Add the `must_erase_for_extraction` attribute to the `val fits_u32` declaration for this symbol in the interface