Unable to authenticate to FlakeHub. Individuals must register at FlakeHub.com; Organizations must create an organization at FlakeHub.com.

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

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

(239) * Warning 239 at /__w/FStar/FStar/FStar/src/data/FStarC.PIMap.fsti(7,5-7,6): - Adding an implicit 'assume new' qualifier on FStarC.PIMap.t

(239) * Warning 239 at /__w/FStar/FStar/FStar/src/data/FStarC.IMap.fsti(7,5-7,6): - Adding an implicit 'assume new' qualifier on FStarC.IMap.t

(239) * Warning 239 at /__w/FStar/FStar/FStar/src/basic/FStarC.Unionfind.fsti(21,5-21,11): - Adding an implicit 'assume new' qualifier on FStarC.Unionfind.p_uvar

(239) * Warning 239 at /__w/FStar/FStar/FStar/src/basic/FStarC.Unionfind.fsti(20,5-20,8): - Adding an implicit 'assume new' qualifier on FStarC.Unionfind.puf

(239) * Warning 239 at /__w/FStar/FStar/FStar/src/basic/FStarC.Hash.fsti(4,5-4,14): - Adding an implicit 'assume new' qualifier on FStarC.Hash.hash_code

(239) * Warning 239 at /__w/FStar/FStar/FStar/src/basic/FStarC.Timing.fsti(20,5-20,12): - Adding an implicit 'assume new' qualifier on FStarC.Timing.time_ns

(239) * Warning 239 at /__w/FStar/FStar/FStar/src/data/FStarC.SMap.fsti(7,5-7,6): - Adding an implicit 'assume new' qualifier on FStarC.SMap.t

(239) * Warning 239 at /__w/FStar/FStar/FStar/src/data/FStarC.PSMap.fsti(7,5-7,6): - Adding an implicit 'assume new' qualifier on FStarC.PSMap.t

(239) * Warning 239 at /home/runner/work/FStar/FStar/fstar/src/data/FStarC.PSMap.fsti(7,5-7,6): - Adding an implicit 'assume new' qualifier on FStarC.PSMap.t

(290) * Warning 290 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.WellFoundedRelation.fst(148,21-148,46): - In the decreases clause for this function, the SMT solver may not be able to prove that the types of wfr_a.decreaser (FStar.Pervasives.dfst xy) (bound in FStar.WellFoundedRelation.fst(148,21-148,46)) and wfr_a.decreaser (FStar.Pervasives.dfst xy) (bound in FStar.WellFoundedRelation.fst(148,21-148,46)) are equal. - The type of the first term is: FStar.WellFoundedRelation.acc_classical wfr_a.relation (FStar.Pervasives.dfst xy) - The type of the second term is: FStar.WellFoundedRelation.acc_classical wfr_a.relation (FStar.Pervasives.dfst xy) - If the proof fails, try annotating these with the same type.

(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.Ghost.fst(24,4-24,8): - Values of type `hide` will be erased during extraction, but its interface hides this fact. - Add the `erasable` attribute to the `val hide` declaration for this symbol in the interface

(239) * Warning 239 at /home/runner/work/FStar/FStar/fstar/src/data/FStarC.IMap.fsti(7,5-7,6): - Adding an implicit 'assume new' qualifier on FStarC.IMap.t

(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.Ghost.fst(24,4-24,8): - Values of type `hide` will be erased during extraction, but its interface hides this fact. - Add the `erasable` attribute to the `val hide` declaration for this symbol in the interface

(239) * Warning 239 at /home/runner/work/FStar/FStar/fstar/src/basic/FStarC.Timing.fsti(20,5-20,12): - Adding an implicit 'assume new' qualifier on FStarC.Timing.time_ns

(239) * Warning 239 at /home/runner/work/FStar/FStar/fstar/src/data/FStarC.SMap.fsti(7,5-7,6): - Adding an implicit 'assume new' qualifier on FStarC.SMap.t

(239) * Warning 239 at /home/runner/work/FStar/FStar/fstar/src/basic/FStarC.Unionfind.fsti(21,5-21,11): - Adding an implicit 'assume new' qualifier on FStarC.Unionfind.p_uvar

(239) * Warning 239 at /home/runner/work/FStar/FStar/fstar/src/basic/FStarC.Unionfind.fsti(20,5-20,8): - Adding an implicit 'assume new' qualifier on FStarC.Unionfind.puf

(239) * Warning 239 at /home/runner/work/FStar/FStar/fstar/src/basic/FStarC.Hash.fsti(4,5-4,14): - Adding an implicit 'assume new' qualifier on FStarC.Hash.hash_code

(239) * Warning 239 at /home/runner/work/FStar/FStar/fstar/src/data/FStarC.PIMap.fsti(7,5-7,6): - Adding an implicit 'assume new' qualifier on FStarC.PIMap.t

(239) * Warning 239 at /home/runner/work/FStar/FStar/fstar/src/data/FStarC.PSMap.fsti(7,5-7,6): - Adding an implicit 'assume new' qualifier on FStarC.PSMap.t

(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.Ghost.fst(24,4-24,8): - Values of type `hide` will be erased during extraction, but its interface hides this fact. - Add the `erasable` attribute to the `val hide` declaration for this symbol in the interface

(239) * Warning 239 at /home/runner/work/FStar/FStar/fstar/src/data/FStarC.IMap.fsti(7,5-7,6): - Adding an implicit 'assume new' qualifier on FStarC.IMap.t

(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.Ghost.fst(24,4-24,8): - Values of type `hide` will be erased during extraction, but its interface hides this fact. - Add the `erasable` attribute to the `val hide` declaration for this symbol in the interface

(239) * Warning 239 at /home/runner/work/FStar/FStar/fstar/src/basic/FStarC.Timing.fsti(20,5-20,12): - Adding an implicit 'assume new' qualifier on FStarC.Timing.time_ns

(239) * Warning 239 at /home/runner/work/FStar/FStar/fstar/src/data/FStarC.SMap.fsti(7,5-7,6): - Adding an implicit 'assume new' qualifier on FStarC.SMap.t

(239) * Warning 239 at /home/runner/work/FStar/FStar/fstar/src/basic/FStarC.Unionfind.fsti(21,5-21,11): - Adding an implicit 'assume new' qualifier on FStarC.Unionfind.p_uvar

(239) * Warning 239 at /home/runner/work/FStar/FStar/fstar/src/basic/FStarC.Unionfind.fsti(20,5-20,8): - Adding an implicit 'assume new' qualifier on FStarC.Unionfind.puf