(228) * Error 228 at /__w/FStar/FStar/FStar/pulse/lib/pulse/lib/Pulse.Lib.PriorityQueue.fst(1346,45-1346,54): - Tactic failed - Expected a term with a non-informative (e.g., erased) type. - Got: ‘Seq.seq t’ - See also /__w/FStar/FStar/FStar/pulse/lib/pulse/lib/Pulse.Lib.PriorityQueue.fst(1325,2-1362,3)

(228) * Error 228 at /__w/FStar/FStar/FStar/pulse/lib/pulse/lib/Pulse.Lib.Task.fst(530,2-530,27): - Tactic failed - Cannot prove: AR.pts_to_full gr_task_st (*?u201*)_ - In the context: pre AR.pts_to_full gr_task_st task_st B.pts_to r_task_st task_st pool_alive p

(66) * Error 66 at /__w/FStar/FStar/FStar/pulse/lib/pulse/lib/Pulse.Lib.RWLock.fst(461,4-464,16): - Ill-typed term - Failed to resolve implicit argument ?674 of type _: PulseCore.FractionalPermission.perm -> Pulse.Lib.Core.slprop introduced for user-provided implicit term at Pulse.Lib.RWLock.fst(461,4-464,16)

(66) * Error 66 at /__w/FStar/FStar/FStar/pulse/lib/pulse/lib/Pulse.Lib.CountingSemaphore.fst(155,20-155,37): - Ill-typed term - Failed to resolve implicit argument ?308 of type Pulse.Lib.Core.slprop introduced for user-provided implicit term at Pulse.Lib.CountingSemaphore.fst(155,20-155,37)

(66) * Error 66 at /__w/FStar/FStar/FStar/pulse/lib/pulse/lib/Pulse.Lib.Deque.fst(471,4-472,16): - Ill-typed term - Failed to resolve implicit argument ?1193 of type Type0 introduced for user-provided implicit term at Pulse.Lib.Deque.fst(471,4-472,16)

(66) * Error 66 at /__w/FStar/FStar/FStar/pulse/lib/pulse/lib/Pulse.Lib.HashTableChained.fst(2196,88-2196,90): - Ill-typed term - Failed to resolve implicit argument ?2234 of type Type introduced for Instantiating implicit argument ‘a’

(228) * Error 228 at /__w/FStar/FStar/FStar/pulse/lib/pulse/lib/Pulse.Lib.ResizableVec.fst(98,2-98,56): - Tactic failed - Cannot prove: pts_to vec_box vec - In the context: pts_to size_box (SZ.uint_to_t 0) pts_to cap_box cap pts_to vec_box vec V.pts_to vec (Seq.create (SZ.v capacity) None)

(19) * Error 19 at /__w/FStar/FStar/FStar/pulse/lib/pulse/lib/Pulse.Lib.AVLTree.fst(465,2-465,31): - Ill-typed term - Assertion failed - The SMT solver could not prove the query. - Env = (a : Type0) (tree : Pulse.Lib.AVLTree.tree_t a) (t : t: FStar.Ghost.erased (Pulse.Lib.Spec.AVLTree.tree a) {Node? t}) (p : Pulse.Lib.AVLTree.node_ptr a) (_node5 : FStar.Ghost.erased (Pulse.Lib.AVLTree.node a)) (_ltree6 : FStar.Ghost.erased (Pulse.Lib.Spec.AVLTree.tree a)) (_rtree7 : FStar.Ghost.erased (Pulse.Lib.Spec.AVLTree.tree a)) (__ : Prims.squash (tree == FStar.Pervasives.Native.Some p)) (__ : Prims.squash (t == Pulse.Lib.Spec.AVLTree.Node _node5.data _ltree6 _rtree7)) (n : Pulse.Lib.AVLTree.node a) (__ : Prims.squash (Pulse.Lib.Core.rewrites_to_p n _node5)) (__ : Prims.unit) (__ : FStar.Pervasives.Native.option (Pulse.Lib.Box.box (Pulse.Lib.AVLTree.node a)) & a & FStar.Pervasives.Native.option (Pulse.Lib.Box.box (Pulse.Lib.AVLTree.node a)) & Prims.unit) (__ : Prims.squash (__ == (_node5.left, _node5.data, _node5.right, ()))) - VC = forall (x: Prims.unit). Prims.l_True == (Some? tree == true) - Also see: Prims.fst(165,27-165,38)

(19) * Error 19 at /__w/FStar/FStar/FStar/pulse/lib/pulse/lib/pledge/Pulse.Lib.Shift.fst(111,40-111,96): - Ill-typed term - Assertion failed - The SMT solver could not prove the query. - Env = (is : Pulse.Lib.Core.inames) (hyp : Pulse.Lib.Core.slprop) (concl : Pulse.Lib.Core.slprop) (_extra3 : FStar.Ghost.erased Pulse.Lib.Core.slprop) (d : Pulse.Class.Duplicable.duplicable _extra3) (e : Pulse.Lib.Shift.shift_elim_t is hyp _extra3 concl) (res : _: Pulse.Lib.Core.slprop & (Pulse.Class.Duplicable.duplicable _extra3 & Pulse.Lib.Shift.shift_elim_t is hyp _extra3 concl)) (__ : Prims.squash (res == (| _extra3, (d, e) |))) - VC = forall (_: Pulse.Lib.Core.slprop). _extra3 == _ - See also /__w/FStar/FStar/FStar/pulse/lib/pulse/lib/pledge/Pulse.Lib.Shift.fst(110,48-111,18)

(228) * Error 228 at /__w/FStar/FStar/FStar/pulse/lib/pulse/lib/Pulse.Lib.ConditionVar.fst(310,47-310,72): - Tactic failed - Cannot compose computations in this atomic block: - This computation has effect: ‘stt_ghost emp_inames’ - The continuation has effect: ‘stt_atomic emp_inames’

(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