Process completed with exit code 2.

(58) * Error 58 at /__w/pulse/pulse/pulse/src/extraction/ExtractPulse.fst(121,6-121,52): - Expected a ghost expression. - Because: arguments to short circuiting operators must be pure or ghost. - Got an expression let _ = FStarC.Extraction.ML.Syntax.string_of_mlpath p in _ = "Pulse.Lib.ArrayPtr.null" with effect 'FStarC.Effect.ALL'.

(58) * Error 58 at /__w/pulse/pulse/pulse/src/extraction/ExtractPulseC.fst(89,4-89,79): - Expected a ghost expression. - Because: arguments to short circuiting operators must be pure or ghost. - Got an expression let _ = FStarC.Extraction.ML.Syntax.string_of_mlpath p in FStarC.Util.starts_with _ "Pulse.C.Types.Struct.struct_t0" with effect 'FStarC.Effect.ALL'.

(58) * Error 58 at /__w/pulse/pulse/pulse/src/syntax_extension/PulseSyntaxExtension.Sugar.fst(400,20-400,25): - Expected a ghost expression. - Because: arguments to short circuiting operators must be pure or ghost. - Got an expression f x y with effect 'FStarC.Effect.ML'.

(58) * Error 58 at /__w/pulse/pulse/pulse/src/extraction/ExtractPulseOCaml.fst(137,11-137,71): - Expected a ghost expression. - Because: arguments to short circuiting operators must be pure or ghost. - Got an expression let _ = FStarC.Ident.lid_of_str "Pulse.Lib.Reference.read" in FStarC.Syntax.Syntax.fv_eq_lid fv _ with effect 'FStarC.Effect.ML'.

Node.js 20 actions are deprecated. The following actions are running on Node.js 20 and may not work as expected: actions/cache/restore@v4, zulip/github-actions-zulip/send-message@v1. Actions will be forced to run with Node.js 24 by default starting June 2nd, 2026. Please check if updated versions of these actions are available that support Node.js 24. To opt into Node.js 24 now, set the FORCE_JAVASCRIPT_ACTIONS_TO_NODE24=true environment variable on the runner or in your workflow file. Once Node.js 24 becomes the default, you can temporarily opt out by setting ACTIONS_ALLOW_USE_UNSECURE_NODE_VERSION=true. For more information see: https://github.blog/changelog/2025-09-19-deprecation-of-node-20-on-github-actions-runners/

(290) * Warning 290 at /__w/pulse/pulse/pulse/src/checker/Pulse.Syntax.Base.fst(292,15-292,17): - In the decreases clause for this function, the SMT solver may not be able to prove that the types of b1 (bound in Pulse.Syntax.Base.fst(292,15-292,17)) and t1 (bound in Pulse.Syntax.Base.fst(173,20-173,22)) are equal. - The type of the first term is: Pulse.Syntax.Base.branch - The type of the second term is: Pulse.Syntax.Base.st_term - If the proof fails, try annotating these with the same type.

(290) * Warning 290 at /__w/pulse/pulse/pulse/src/checker/Pulse.Syntax.Base.fst(297,14-297,16): - In the decreases clause for this function, the SMT solver may not be able to prove that the types of q1 (bound in Pulse.Syntax.Base.fst(297,14-297,16)) and t1 (bound in Pulse.Syntax.Base.fst(173,20-173,22)) are equal. - The type of the first term is: Pulse.Syntax.Base.qualifier - The type of the second term is: Pulse.Syntax.Base.st_term - If the proof fails, try annotating these with the same type.

(290) * Warning 290 at /__w/pulse/pulse/pulse/src/checker/Pulse.Syntax.Base.fst(123,20-123,22): - In the decreases clause for this function, the SMT solver may not be able to prove that the types of p1 (bound in Pulse.Syntax.Base.fst(123,20-123,22)) and pb1 (bound in Pulse.Syntax.Base.fst(139,16-139,19)) are equal. - The type of the first term is: Pulse.Syntax.Base.pattern - The type of the second term is: Pulse.Syntax.Base.pattern & Prims.bool - If the proof fails, try annotating these with the same type.

(290) * Warning 290 at /__w/pulse/pulse/pulse/src/checker/Pulse.Syntax.Base.fst(139,16-139,19): - In the decreases clause for this function, the SMT solver may not be able to prove that the types of pb1 (bound in Pulse.Syntax.Base.fst(139,16-139,19)) and p1 (bound in Pulse.Syntax.Base.fst(123,20-123,22)) are equal. - The type of the first term is: Pulse.Syntax.Base.pattern & Prims.bool - The type of the second term is: Pulse.Syntax.Base.pattern - If the proof fails, try annotating these with the same type.

(318) * Warning 318 at /__w/pulse/pulse/pulse/lib/common/Pulse.Lib.Raise.fst(21,4-21,12): - Values of type `raisable` will be erased during extraction, but its interface hides this fact. - Add the `must_erase_for_extraction` attribute to the `val raisable` declaration for this symbol in the interface

(337) * Warning 337 at /__w/pulse/pulse/pulse/src/checker/Pulse.Common.fst(84,11-84,12): - 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 '@'.

(239) * Warning 239 at /__w/pulse/pulse/pulse/src/syntax_extension/PulseSyntaxExtension.SyntaxWrapper.fsti(90,5-90,11): - Adding an implicit 'assume new' qualifier on PulseSyntaxExtension.SyntaxWrapper.branch

(272) * Warning 272 at /__w/pulse/pulse/pulse/src/extraction/ExtractPulse.fst(66,0-66,41): - Top-level let-bindings must be total; this term may have effects

(272) * Warning 272 at /__w/pulse/pulse/pulse/src/extraction/ExtractPulse.fst(32,0-32,39): - Top-level let-bindings must be total; this term may have effects