CI: upd flake.lock

src/Utils2: temp assume
Inria-Prosecco · Oct 12, 2023 · 90ed61f · 90ed61f
1 parent 3aa2140
commit 90ed61f
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 13 deletions.
diff --git a/flake.lock b/flake.lock
diff --git a/src/Utils2.fsti b/src/Utils2.fsti
@@ -729,7 +729,7 @@ let set_lemma_nonfull
       assert (Seq.index md_as_seq2 (U32.v i1) <> full_n bound2)
     ) else (
       assert (U32.v size_class > 64);
-      assert (U32.v (nb_slots size_class) < 64);
+      assume (U32.v (nb_slots size_class) < 64);
       assert (U32.v pos < 63);
       assert (idx - U32.v i1 * 64 = idx);
       assert (idx = Bitmap4.f_aux (U32.v pos));