tweak a couple of rlimits

FStarLang · Dec 12, 2024 · a8bdbd1 · a8bdbd1
1 parent cafec0f
commit a8bdbd1
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 2 deletions.
diff --git a/lib/pulse/lib/Pulse.Lib.HashTable.Spec.fst b/lib/pulse/lib/Pulse.Lib.HashTable.Spec.fst
@@ -543,7 +543,8 @@ let not_full #kt #vt (r:repr_t kt vt) : Type0 =
   exists i. ~(Used? (r @@ i ))
 
 #set-options "--split_queries always"
-
+#restart-solver
+#push-options "--z3rlimit_factor 4"
 let rec insert_repr_walk #kt #vt #sz (#spec : erased (spec_t kt vt)) 
   (repr : repr_t_sz kt vt sz{pht_models spec repr /\ not_full repr}) (k : kt) (v : vt) 
   (off:nat{off <= sz})
@@ -611,6 +612,7 @@ let rec insert_repr_walk #kt #vt #sz (#spec : erased (spec_t kt vt))
           (**)lemma_zombie_upd spec repr off k v;
           upd_ repr idx k v
         )
+#pop-options
 
 let insert_repr #kt #vt #sz
                 (#spec : erased (spec_t kt vt))

diff --git a/lib/pulse/lib/Pulse.Lib.PCM.FractionalPreorder.fst b/lib/pulse/lib/Pulse.Lib.PCM.FractionalPreorder.fst
@@ -57,10 +57,10 @@ let fp_pcm' (#a:Type) (p:preorder a) : pcm' (pcm_carrier p) = {
 let fp_lem_commutative (#a:Type) (p:preorder a) : lem_commutative (fp_pcm' p) =
   fun _ _ -> ()
 
+#push-options "--z3rlimit_factor 4"
 let fp_lem_assoc_l (#a:Type) (p:preorder a) : lem_assoc_l (fp_pcm' p) =
   fun _ _ _ -> ()
 
-#push-options "--z3rlimit_factor 4"
 let fp_lem_assoc_r (#a:Type) (p:preorder a) : lem_assoc_r (fp_pcm' p) =
   fun _ _ _ -> ()
 #pop-options