Process completed with exit code 2.

(19) * Error 19 at CommonUtils.fst(37,3-38,7): - Assertion failed - The SMT solver could not prove the query. Use --query_stats for more details. - This query was retried due to the --proof_recovery option, yet it still failed on all attempts. - See also /__w/FStar/FStar/fstar/lib/fstar/ulib/Prims.fst(335,38-335,57)

(12) * Error 12 at BeyondCriteria.fst(22,23-22,28): - Expected type Prims.prop but s2 tr has type Type0

(12) * Error 12 at BeyondCriteria.fst(22,13-22,18): - Expected type Prims.prop but s1 tr has type Type0

(12) * Error 12 at ExtraTactics.fst(9,34-9,39): - Expected type Prims.prop but p x has type Type0

(12) * Error 12 at ExtraTactics.fst(8,15-8,18): - Expected type Prims.prop but p x has type Type0

(12) * Error 12 at Hist.fst(24,97-24,104): - Expected type Prims.prop but p2 lt r has type Type0

(12) * Error 12 at Hist.fst(24,85-24,92): - Expected type Prims.prop but p1 lt r has type Type0

(12) * Error 12 at TC.Checkable.fst(4,33-4,36): - Expected type Prims.prop but p x has type Type0

Process completed with exit code 2.

(134) * Error 134 at STLC.fst(501,11-501,13): - Namespace 'FStar.ST' cannot be found.

(34) * Error 34 at BeyondCriteria.fst(66,8-67,154): - Computed type Type0 and effect Tot is not compatible with the annotated type Prims.prop and effect GTot

(12) * Error 12 at BeyondCriteria.fst(67,10-67,154): - Expected type Prims.prop but comp.rel_sem (comp.source.beh (comp.source.link ps cs)) (comp.target.beh (comp.target.link (comp.compile_pprog ps) ct)) has type Type0

(134) * Error 134 at MST.Repr.fst(7,21-7,25): - Namespace 'FStar.Monotonic.Heap' cannot be found.

Process completed with exit code 2.

(12) * Error 12 at /__w/FStar/FStar/steel/lib/steel/Steel.Witnessed.Core.fsti(9,40-9,44): - Expected type Prims.prop but p s1 has type Type0

(12) * Error 12 at /__w/FStar/FStar/steel/lib/steel/Steel.Witnessed.Core.fsti(9,17-9,21): - Expected type Prims.prop but p s0 has type Type0

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

Process completed with exit code 1.

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

Process completed with exit code 1.

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

Process completed with exit code 1.

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

Repository path '/tmp/FStar' is not under '/__w/FStar/FStar'

(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

(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/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

(285) * Warning 285 at Compiler.StlcToFStar.fst(9,11-9,31): - No modules in namespace FStar.StrongExcludedMiddle and no file with that name either

(285) * Warning 285 at Examples.HOC.fst(4,21-4,25): - No modules in namespace FStar.Monotonic.Heap and no file with that name either

(285) * Warning 285 at Examples.Autograder.fst(5,21-5,25): - No modules in namespace FStar.Monotonic.Heap and no file with that name either

(285) * Warning 285 at STLC.fst(501,11-501,13): - No modules in namespace FStar.ST and no file with that name either

(285) * Warning 285 at LabeledRefs.fsti(6,24-6,28): - No modules in namespace FStar.Monotonic.Heap and no file with that name either

(285) * Warning 285 at MST.Repr.fst(10,27-10,36): - module not found in search path: fstar.monotonic.witnessed

(285) * Warning 285 at MST.Repr.fst(7,21-7,25): - No modules in namespace FStar.Monotonic.Heap and no file with that name either

(285) * Warning 285 at MST.Tot.fst(6,21-6,25): - No modules in namespace FStar.Monotonic.Heap and no file with that name either

(285) * Warning 285 at FullGroundType.fst(6,21-6,25): - No modules in namespace FStar.Monotonic.Heap and no file with that name either

(285) * Warning 285 at Witnessable.fst(8,21-8,25): - No modules in namespace FStar.Monotonic.Heap and no file with that name either

(285) * Warning 285 at SpecTree.fst(4,21-4,25): - No modules in namespace FStar.Monotonic.Heap and no file with that name either

(337) * Warning 337 at /__w/FStar/FStar/steel/src/extraction/ExtractSteel.Krml.fst(33,41-33,42): - 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 '@'.

(288) * Warning 288 at Unsigned_negation.fst(93,32-93,47): - FStar.Int.Cast.uint64_to_int64 is deprecated - with care; in C the result is implementation-defined when not representable - See also Unsigned_negation.fst(93,2-93,73)

(288) * Warning 288 at Unsigned_negation.fst(93,32-93,47): - FStar.Int.Cast.uint64_to_int64 is deprecated - with care; in C the result is implementation-defined when not representable - See also Unsigned_negation.fst(93,2-93,73)

(288) * Warning 288 at Unsigned_negation.fst(81,32-81,47): - FStar.Int.Cast.uint32_to_int32 is deprecated - with care; in C the result is implementation-defined when not representable - See also Unsigned_negation.fst(81,2-81,73)

(288) * Warning 288 at Unsigned_negation.fst(81,32-81,47): - FStar.Int.Cast.uint32_to_int32 is deprecated - with care; in C the result is implementation-defined when not representable - See also Unsigned_negation.fst(81,2-81,73)

(288) * Warning 288 at Pulse.Lib.C.Casts.fst(25,4-25,19): - FStar.Int.Cast.uint64_to_int64 is deprecated - with care; in C the result is implementation-defined when not representable - See also /__w/FStar/FStar/fstar/lib/fstar/ulib/FStar.Int.Cast.fst(170,4-170,19)

(288) * Warning 288 at Pulse.Lib.C.Casts.fst(25,4-25,19): - FStar.Int.Cast.uint64_to_int64 is deprecated - with care; in C the result is implementation-defined when not representable - See also /__w/FStar/FStar/fstar/lib/fstar/ulib/FStar.Int.Cast.fst(170,4-170,19)

(288) * Warning 288 at Pulse.Lib.C.Casts.fst(21,4-21,19): - FStar.Int.Cast.uint32_to_int32 is deprecated - with care; in C the result is implementation-defined when not representable - See also /__w/FStar/FStar/fstar/lib/fstar/ulib/FStar.Int.Cast.fst(155,4-155,19)

(288) * Warning 288 at Pulse.Lib.C.Casts.fst(21,4-21,19): - FStar.Int.Cast.uint32_to_int32 is deprecated - with care; in C the result is implementation-defined when not representable - See also /__w/FStar/FStar/fstar/lib/fstar/ulib/FStar.Int.Cast.fst(155,4-155,19)

(321) * Warning 321: - Did not expect module Pulse.Main to be already checked. - Found it in an unexpected location: /__w/FStar/FStar/fstar/lib/fstar/pulse/common.checked/Pulse.Main.fsti.checked instead of _cache/Pulse.Main.fsti.checked

(321) * Warning 321: - Did not expect module Pulse to be already checked. - Found it in an unexpected location: /__w/FStar/FStar/fstar/lib/fstar/pulse/pulse.checked/Pulse.fst.checked instead of _cache/Pulse.fst.checked

(335) * Warning 335 at /__w/FStar/FStar/fstar/lib/fstar/ulib/FStar.Char.fsti(0,0-0,0): - Interface FStar.Char is admitted without an implementation

(335) * Warning 335 at /__w/FStar/FStar/fstar/lib/fstar/ulib/FStar.Attributes.fsti(0,0-0,0): - Interface FStar.Attributes is admitted without an implementation

(335) * Warning 335 at /__w/FStar/FStar/fstar/lib/fstar/ulib/FStar.All.fsti(0,0-0,0): - Interface FStar.All is admitted without an implementation

(335) * Warning 335 at /__w/FStar/FStar/fstar/lib/fstar/pulse/common/Pulse.Main.fsti(0,0-0,0): - Interface Pulse.Main is admitted without an implementation

(335) * Warning 335 at /__w/FStar/FStar/fstar/lib/fstar/pulse/common/Pulse.Lib.NonInformative.fsti(0,0-0,0): - Interface Pulse.Lib.NonInformative is admitted without an implementation

(335) * Warning 335 at /__w/FStar/FStar/fstar/lib/fstar/pulse/common/Pulse.Lib.Loc.fsti(0,0-0,0): - Interface Pulse.Lib.Loc is admitted without an implementation

(335) * Warning 335 at /__w/FStar/FStar/fstar/lib/fstar/pulse/common/Pulse.Lib.Dv.fsti(0,0-0,0): - Interface Pulse.Lib.Dv is admitted without an implementation

(335) * Warning 335 at /__w/FStar/FStar/fstar/lib/fstar/pulse/common/Pulse.Lib.Core.fsti(0,0-0,0): - Interface Pulse.Lib.Core is admitted without an implementation

(335) * Warning 335 at /__w/FStar/FStar/fstar/lib/fstar/pulse/common/Pulse.Lib.Core.Refs.fsti(0,0-0,0): - Interface Pulse.Lib.Core.Refs is admitted without an implementation

(335) * Warning 335 at /__w/FStar/FStar/fstar/lib/fstar/pulse/common/Pulse.Lib.Core.Inv.fsti(0,0-0,0): - Interface Pulse.Lib.Core.Inv is admitted without an implementation

(285) * Warning 285 at src/lowparse/LowParse.Low.Combinators.fsti(5,29-5,35): - module not found in search path: lowstar.monotonic.buffer

(285) * Warning 285 at src/lowparse/LowParse.Low.FLData.fst(8,18-8,28): - module not found in search path: fstar.hyperstack

(285) * Warning 285 at src/lowparse/LowParse.Low.FLData.fst(7,30-7,32): - module not found in search path: fstar.hyperstack.st

(285) * Warning 285 at src/lowparse/LowParse.Low.FLData.fst(5,19-5,25): - module not found in search path: lowstar.buffer

(285) * Warning 285 at src/lowparse/LowParse.Low.VLData.fst(44,18-44,28): - module not found in search path: fstar.hyperstack

(285) * Warning 285 at src/lowparse/LowParse.Low.VLData.fst(7,30-7,32): - module not found in search path: fstar.hyperstack.st

(285) * Warning 285 at src/lowparse/LowParse.Low.VLData.fst(6,19-6,25): - module not found in search path: lowstar.buffer

(285) * Warning 285 at src/lowparse/LowParse.Low.Array.fst(205,18-205,28): - module not found in search path: fstar.hyperstack

(285) * Warning 285 at src/lowparse/LowParse.Low.Array.fst(173,19-173,25): - module not found in search path: lowstar.buffer

(285) * Warning 285 at src/lowparse/LowParse.Low.Array.fst(10,30-10,32): - module not found in search path: fstar.hyperstack.st