CI: upd everything + partial fixes

Main.Meta.fst and Main.fst need some work
Inria-Prosecco · Dec 21, 2023 · e83b714 · e83b714
1 parent 63be294
commit e83b714
Show file tree

Hide file tree

Showing 3 changed files with 17 additions and 13 deletions.
diff --git a/flake.lock b/flake.lock
diff --git a/src/SlabsAlloc.fst b/src/SlabsAlloc.fst
@@ -546,6 +546,8 @@ let allocate_slab_aux_2_full
     md_count_v (G.hide (Seq.upd (G.reveal md_region_lv) (US.v idx2) 2ul))
     idx1 idx2' idx2 idx4 idx5
 
+#restart-solver
+
 // Slab moves from partial to partial
 inline_for_extraction noextract
 let allocate_slab_aux_2_partial
@@ -612,6 +614,8 @@ let allocate_slab_aux_2_partial
     md_count_v md_region_lv
     idx1 idx2 idx3 idx4 idx5
 
+#restart-solver
+
 // Slab initially partial
 inline_for_extraction noextract
 let allocate_slab_aux_2

diff --git a/src/SlotsAlloc.fst b/src/SlotsAlloc.fst
@@ -883,7 +883,7 @@ let elim_slab_vprop (#opened:_)
   md_as_seq2
 #pop-options
 
-#push-options "--z3rlimit 100 --fuel 0 --ifuel 0"
+#push-options "--z3rlimit 150 --fuel 0 --ifuel 0"
 let bound2_inv
   (size_class: sc)
   (md_as_seq: Seq.lseq U64.t 4)