tweaks to restore some tests

FStarLang · Jan 13, 2025 · 2e3480e · 2e3480e
1 parent 3b77d08
commit 2e3480e
Show file tree

Hide file tree

Showing 5 changed files with 9 additions and 5 deletions.
diff --git a/tests/micro-benchmarks/Effects.Coherence.fst b/tests/micro-benchmarks/Effects.Coherence.fst
@@ -36,9 +36,9 @@ layered_effect {
 new_effect M2 = M1
 new_effect M3 = M1
 
-let lift_pure_m (a:Type) (wp:_) (f:eqtype_as_type unit -> PURE a wp)
+let lift_pure_m (a:Type u#a) (wp:_) (f:eqtype_as_type unit -> PURE a wp)
   : Pure (repr a ()) (requires wp (fun _ -> True)) (ensures fun _ -> True)
-  = FStar.Monotonic.Pure.elim_pure_wp_monotonicity_forall ();
+  = FStar.Monotonic.Pure.elim_pure_wp_monotonicity_forall u#a ();
     f ()
 sub_effect PURE ~> M1 = lift_pure_m
 

diff --git a/tests/micro-benchmarks/Unit1.WPsAndTriples.fst b/tests/micro-benchmarks/Unit1.WPsAndTriples.fst
@@ -51,9 +51,9 @@ val good_hoare : unit -> Pure int True (fun r -> r == 3)
 (*
  * An example from Dominique Unruh
  *)
-let mono a (wp:pure_wp a) (p q:pure_post a) (_:squash(forall (x:a). p x ==> q x)) : 
+let mono (a:Type u#a) (wp:pure_wp a) (p q:pure_post a) (_:squash(forall (x:a). p x ==> q x)) : 
     Lemma (wp p ==> wp q) = 
-	FStar.Monotonic.Pure.elim_pure_wp_monotonicity_forall ()
+	FStar.Monotonic.Pure.elim_pure_wp_monotonicity_forall u#a ()
 
 [@@ expect_failure]
 let contradiction () : Lemma(False) = 

diff --git a/tests/tactics/Clear.fst b/tests/tactics/Clear.fst
@@ -19,7 +19,7 @@ open FStar.Tactics.V2
 
 assume val phi : Type
 assume val psi : Type
-assume val xi : Type
+assume val xi : Type u#0
 
 assume val p : squash xi
 

diff --git a/tests/vale/X64.Vale.Decls.fst b/tests/vale/X64.Vale.Decls.fst
@@ -25,6 +25,7 @@ module P = X64.Print_s
 #reset-options "--z3smtopt '(set-option :smt.arith.nl true)' --using_facts_from Prims --using_facts_from FStar.Math"
 let lemma_mul_nat (x:nat) (y:nat) : Lemma (ensures 0 <= (x `op_Multiply` y)) = ()
 #reset-options "--initial_fuel 2 --max_fuel 2 --initial_ifuel 1 --z3rlimit_factor 10 --retry 5 --query_stats"
+#set-options "--z3smtopt '(set-option :smt.qi.eager_threshold 20)'"
 let cf = Lemmas_i.cf
 let ins = S.ins
 type ocmp = S.ocmp

diff --git a/ulib/FStar.ModifiesGen.fst b/ulib/FStar.ModifiesGen.fst
@@ -1961,8 +1961,11 @@ let union_loc_of_loc_disjoint_intro
     xs.addr `GSet.mem` addrs_of_loc_weak smaller xs.region /\
     aloc_disjoint xl xs
   )) by (
+    let open FStar.Stubs.Tactics.V2.Builtins in
     let open FStar.Tactics.SMT in
     set_rlimit 15;
+    set_options "--z3cliopt 'smt.qi.eager_threshold=1'";
+    set_options "--retry 5";
     ()
   );
   assert (auxl ` loc_aux_disjoint` doms);