From 2e3480ec882eceb2295a609a743913653cf59378 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy <nikswamy@users.noreply.github.com> Date: Mon, 13 Jan 2025 13:41:46 -0800 Subject: [PATCH] tweaks to restore some tests --- tests/micro-benchmarks/Effects.Coherence.fst | 4 ++-- tests/micro-benchmarks/Unit1.WPsAndTriples.fst | 4 ++-- tests/tactics/Clear.fst | 2 +- tests/vale/X64.Vale.Decls.fst | 1 + ulib/FStar.ModifiesGen.fst | 3 +++ 5 files changed, 9 insertions(+), 5 deletions(-) diff --git a/tests/micro-benchmarks/Effects.Coherence.fst b/tests/micro-benchmarks/Effects.Coherence.fst index 002c11995c7..746e30e79cd 100644 --- 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 index 2c203075ecd..799e58bb6f6 100644 --- 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 index e30e81f31ec..ad7149f74c9 100644 --- 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 index 5ce333515a5..c184f0897e8 100644 --- 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 index b7f3643d7b0..1b20f9db42f 100644 --- 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);