Process completed with exit code 2.

(19) * Error 19 at CLRS.Ch22.BFS.Impl.fst(1374,3-1450,5): - Could not prove subtyping of adj: A.array int -> n: SZ.t -> source: SZ.t -> color: A.array int -> dist: A.array int -> pred: A.array int -> queue_data: A.array SZ.t -> ctr: GR.ref nat -> fn requires A.pts_to adj sadj ** A.pts_to color scolor ** A.pts_to dist sdist ** A.pts_to pred spred ** A.pts_to queue_data squeue ** GR.pts_to ctr c0 ** pure (SZ.v n > 0 /\ SZ.v source < SZ.v n /\ Seq.length sadj == SZ.v n * SZ.v n /\ Seq.length sadj <= A.length adj /\ Seq.length scolor == SZ.v n /\ Seq.length scolor <= A.length color /\ Seq.length sdist == SZ.v n /\ Seq.length sdist <= A.length dist /\ Seq.length spred == SZ.v n /\ Seq.length spred <= A.length pred /\ Seq.length squeue == SZ.v n /\ Seq.length squeue <= A.length queue_data /\ SZ.fits (SZ.v n * SZ.v n)) ensures exists* (scolor': Seq.seq int) (sdist': Seq.seq int) (spred': Seq.seq int) (squeue': Seq.seq SZ.t) (cf: nat). A.pts_to adj sadj ** A.pts_to color scolor' ** A.pts_to dist sdist' ** A.pts_to pred spred' ** A.pts_to queue_data squeue' ** GR.pts_to ctr cf ** pure (Seq.length scolor' == SZ.v n /\ Seq.length sdist' == SZ.v n /\ Seq.length spred' == SZ.v n /\ Seq.length squeue' == SZ.v n /\ SZ.v source < SZ.v n /\ Seq.index scolor' (SZ.v source) <> 0 /\ Seq.index sdist' (SZ.v source) == 0 /\ (forall (w: nat). w < SZ.v n /\ Seq.index scolor' w <> 0 ==> Seq.index sdist' w >= 0) /\ (forall (w: nat). w < SZ.v n /\ Seq.index scolor' w <> 0 ==> reachable_in sadj (SZ.v n) (SZ.v source) w (Seq.index sdist' w)) /\ (forall (v: nat) (k: nat). v < SZ.v n /\ reachable_in sadj (SZ.v n) (SZ.v source) v k ==> Seq.index scolor' v <> 0) /\ (forall (v: nat). v < SZ.v n /\ Seq.index scolor' v <> 0 /\ Seq.index spred' v >= 0 /\ Seq.index spred' v < SZ.v n ==> Seq.index scolor' (Seq.index spred' v) <> 0 /\ Seq.index sdist' v == Seq.index sdist' (Seq.index spred' v) + 1) /\ cf >= c0 /\ cf - c0 <= 2 * (SZ.v n * SZ.v n) /\ (forall (w: nat) (k: nat). w < SZ.v n /\ reachable_in sadj (SZ.v n) (SZ.v source) w k ==> Seq.index sdist' w <= k)) and adj: A.array int -> n: SZ.t -> source: SZ.t -> color: A.array int -> dist: A.array int -> pred: A.array int -> queue_data: A.array SZ.t -> ctr: GR.ref nat -> fn requires A.pts_to adj sadj ** A.pts_to color scolor ** A.pts_to dist sdist ** A.pts_to pred spred ** A.pts_to queue_data squeue ** GR.pts_to ctr c0 ** pure (SZ.v n > 0 /\ SZ.v source < SZ.v n /\ Seq.length sadj == SZ.v n * SZ.v n /\ Seq.length sadj <= A.length adj /\ Seq.length scolor == SZ.v n /\ Seq.length scolor <= A.length color /\ Seq.length sdist == SZ.v n /\ Seq.length sdist <= A.length dist /\ Seq.length spred == SZ.v n /\ Seq.length spred <= A.length pred /\ Seq.le

Node.js 20 actions are deprecated. The following actions are running on Node.js 20 and may not work as expected: actions/checkout@v4. Actions will be forced to run with Node.js 24 by default starting June 2nd, 2026. Node.js 20 will be removed from the runner on September 16th, 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/

(349) * Warning 349 at CLRS.Ch23.Kruskal.Spec.fst(1408,4-1571,9): - The verification condition succeeded after splitting it to localize potential errors, although the original non-split verification condition failed. If you want to rely on splitting queries for verifying your program please use the '--split_queries always' option rather than relying on it implicitly.