FStarLang · mtzguido · Oct 8, 2024 · Oct 8, 2024
diff --git a/ulib/FStar.Int.fsti b/ulib/FStar.Int.fsti
@@ -183,8 +183,6 @@ let gte #n (a:int_t n) (b:int_t n) : Tot bool = a >= b
 let lt #n (a:int_t n) (b:int_t n) : Tot bool = a < b
 let lte #n (a:int_t n) (b:int_t n) : Tot bool = a <= b
 
-#push-options "--initial_fuel 1 --max_fuel 1"
-
 /// Casts
 
 let to_uint (#n:pos) (x:int_t n) : Tot (UInt.uint_t n) = 

diff --git a/ulib/FStar.LexicographicOrdering.fst b/ulib/FStar.LexicographicOrdering.fst
@@ -17,7 +17,7 @@
 *)
 
 module FStar.LexicographicOrdering
-#push-options "--warn_error -242" //no inner let recs in SMT
+#set-options "--warn_error -242" //no inner let recs in SMT
 open FStar.ReflexiveTransitiveClosure
 open FStar.WellFounded
 

diff --git a/ulib/FStar.Math.Lemmas.fst b/ulib/FStar.Math.Lemmas.fst
@@ -18,7 +18,7 @@ module FStar.Math.Lemmas
 open FStar.Mul
 open FStar.Math.Lib
 
-#push-options "--fuel 0 --ifuel 0"
+#set-options "--fuel 0 --ifuel 0"
 
 (* Lemma: definition of Euclidean division *)
 let euclidean_div_axiom a b = ()

diff --git a/ulib/FStar.UInt128.fst b/ulib/FStar.UInt128.fst
@@ -337,6 +337,8 @@ let sub_mod_wrap1_ok a b =
       ()
     end
 #pop-options
+#pop-options
+
 
 let sum_lt (a1 a2 b1 b2:nat) : Lemma
   (requires (a1 + a2 < b1 + b2 /\ a1 >= b1))
@@ -372,6 +374,7 @@ let sub_mod (a b: t) : Pure t
     else sub_mod_wrap_ok a b);
   sub_mod_impl a b
 #pop-options
+
 #restart-solver
 
 val shift_bound : #n:nat -> num:UInt.uint_t n -> n':nat ->

diff --git a/ulib/FStar.WellFounded.Util.fst b/ulib/FStar.WellFounded.Util.fst
@@ -1,7 +1,7 @@
 module FStar.WellFounded.Util
 open FStar.WellFounded
 
-#push-options "--warn_error -242" //inner let recs not encoded to SMT; ok
+#set-options "--warn_error -242" //inner let recs not encoded to SMT; ok
 
 let intro_lift_binrel (#a:Type) (r:binrel a) (y:a) (x:a)
   : Lemma

diff --git a/ulib/FStar.WellFounded.fst b/ulib/FStar.WellFounded.fst
@@ -22,7 +22,7 @@
 
 module FStar.WellFounded
 
-#push-options "--warn_error -242" //inner let recs not encoded to SMT; ok
+#set-options "--warn_error -242" //inner let recs not encoded to SMT; ok
 
 let binrel (a:Type) = a -> a -> Type
 

diff --git a/ulib/LowStar.BufferView.Down.fst b/ulib/LowStar.BufferView.Down.fst
@@ -209,6 +209,7 @@ let sel'_tail #a #b v es i =
   FStar.Math.Lemmas.lemma_mod_sub i n 1;
   FStar.Math.Lemmas.add_div_mod_1 j n;
   assert (j / n == (i / n) - 1)
+#pop-options
 
 val as_seq'_sel' (#a #b: _)
                  (v:view a b)
@@ -220,13 +221,6 @@ val as_seq'_sel' (#a #b: _)
        sel' v es i == Seq.index (as_seq' es v) i))
      (decreases (Seq.length es))
 
-//flaky
-#reset-options
-#set-options "--smtencoding.elim_box true"
-#set-options "--smtencoding.l_arith_repr native"
-#set-options "--smtencoding.nl_arith_repr wrapped"
-#set-options "--z3rlimit_factor 10" //just being conservative
-#set-options "--initial_fuel 1 --max_fuel 1 --max_ifuel 0"
 let rec as_seq'_sel' #a #b v es i =
   as_seq'_len es v;
   let n : pos = View?.n v in
@@ -251,7 +245,6 @@ let rec as_seq'_sel' #a #b v es i =
                    Seq.index (as_seq' as' v) j);
            sel'_tail v es i
          end
-#reset-options
 
 let as_seq_sel #b h vb i =
   indexing vb i;
@@ -349,7 +342,7 @@ let rec upd_seq'_spec (#a #b: _) (v:view a b) (s:Seq.seq b{Seq.length s % View?.
          assert (es `Seq.equal` Seq.cons (View?.put v pfx) as');
          as_seq'_cons v (View?.put v pfx) as'
 
-#set-options "--z3rlimit 20"
+#push-options "--z3rlimit 20"
 let upd_seq_spec (#b: _) (h:HS.mem) (vb:buffer b{live h vb}) (s:Seq.seq b{Seq.length s = length vb})
   = let h' = upd_seq h vb s in
     Math.cancel_mul_mod (B.length (as_buffer vb)) (View?.n (get_view vb));
@@ -367,3 +360,4 @@ let upd_seq_spec (#b: _) (h:HS.mem) (vb:buffer b{live h vb}) (s:Seq.seq b{Seq.le
     FStar.Classical.forall_intro_2 (fun as1 as2 ->
       Classical.move_requires (as_seq'_injective v as1) as2
          <: Lemma ((as_seq' as1 v `Seq.equal` as_seq' as2 v) ==> (as1 `Seq.equal` as2)))
+#pop-options
diff --git a/ulib/LowStar.Monotonic.Buffer.fst b/ulib/LowStar.Monotonic.Buffer.fst
@@ -1876,6 +1876,7 @@ let blit #a #rrel1 #rrel2 #rel1 #rel2 src idx_src dst idx_dst len =
       assert (h1 == g_upd_seq dst (Seq.slice s2' 0 (U32.v length2)) h);
       g_upd_seq_as_seq dst (Seq.slice s2' 0 (U32.v length2)) h  //for modifies clause
   | _, _ -> ()
+#pop-options
 
 #restart-solver
 #push-options "--z3rlimit 256 --max_fuel 0 --max_ifuel 1 --initial_ifuel 1 --z3cliopt smt.qi.EAGER_THRESHOLD=4"

diff --git a/ulib/experimental/FStar.InteractiveHelpers.Base.fst b/ulib/experimental/FStar.InteractiveHelpers.Base.fst
@@ -4,7 +4,7 @@ open FStar.List.Tot
 open FStar.Tactics
 open FStar.Mul
 
-#push-options "--z3rlimit 15 --fuel 0 --ifuel 1"
+#set-options "--z3rlimit 15 --fuel 0 --ifuel 1"
 
 (*** Utilities *)
 val bv_eq : bv -> bv -> Tot bool

diff --git a/ulib/experimental/FStar.InteractiveHelpers.Effectful.fst b/ulib/experimental/FStar.InteractiveHelpers.Effectful.fst
@@ -14,7 +14,7 @@ let term_eq = FStar.Reflection.TermEq.Simple.term_eq
 /// Effectful term analysis: retrieve information about an effectful term, including
 /// its return type, its arguments, its correctly instantiated pre/postcondition, etc.
 
-#push-options "--z3rlimit 15 --fuel 0 --ifuel 1"
+#set-options "--z3rlimit 15 --fuel 0 --ifuel 1"
 
 
 (*** Effectful term analysis *)

diff --git a/ulib/experimental/FStar.InteractiveHelpers.ExploreTerm.fst b/ulib/experimental/FStar.InteractiveHelpers.ExploreTerm.fst
@@ -5,7 +5,7 @@ open FStar.Tactics
 open FStar.Mul
 open FStar.InteractiveHelpers.Base
 
-#push-options "--z3rlimit 15 --fuel 0 --ifuel 1"
+#set-options "--z3rlimit 15 --fuel 0 --ifuel 1"
 
 (*** Types and effects *)
 /// Define utilities to handle and carry types and effects

diff --git a/ulib/experimental/FStar.InteractiveHelpers.Output.fst b/ulib/experimental/FStar.InteractiveHelpers.Output.fst
@@ -10,7 +10,7 @@ open FStar.InteractiveHelpers.Propositions
 /// Facilities to output results to the IDE/emacs/whatever.
 /// Contains datatypes and functions to carry information.
 
-#push-options "--z3rlimit 15 --fuel 0 --ifuel 1"
+#set-options "--z3rlimit 15 --fuel 0 --ifuel 1"
 
 (*** Convert terms to string *)
 /// The important point is to handle variable shadowing properly, so that the

diff --git a/ulib/experimental/FStar.InteractiveHelpers.PostProcess.fst b/ulib/experimental/FStar.InteractiveHelpers.PostProcess.fst
@@ -13,7 +13,7 @@ open FStar.InteractiveHelpers.Output
 /// information from the context and generate output which can be exploited
 /// on the IDE side.
 
-#push-options "--z3rlimit 15 --fuel 0 --ifuel 1" 
+#set-options "--z3rlimit 15 --fuel 0 --ifuel 1"
 
 (*** General utilities *)
 /// We declare some identifiers that we will use to guide the meta processing

diff --git a/ulib/experimental/FStar.InteractiveHelpers.Propositions.fst b/ulib/experimental/FStar.InteractiveHelpers.Propositions.fst
@@ -17,7 +17,7 @@ let term_eq = FStar.Reflection.TermEq.Simple.term_eq
 /// [> let z = x / y in // term of interest
 /// [> assert(...); // post assertion
 
-#push-options "--z3rlimit 15 --fuel 0 --ifuel 1"
+#set-options "--z3rlimit 15 --fuel 0 --ifuel 1"
 
 /// Analyze a term to retrieve its effectful information
 

diff --git a/ulib/experimental/FStar.Sequence.Permutation.fst b/ulib/experimental/FStar.Sequence.Permutation.fst
@@ -196,6 +196,8 @@ let rec permutation_from_equal_counts (#a:eqtype) (s0:seq a) (s1:seq a{(forall x
             )
       );
       reveal_is_permutation_nopats s0 s1 f; f)
+#pop-options
+
 #restart-solver
 
 module CM = FStar.Algebra.CommMonoid
@@ -254,6 +256,7 @@ let rec foldm_back_append #a (m:CM.cm a) (s1 s2: seq a)
         m.mult (foldm_back m s1) (foldm_back m s2);
       }
     )
+#pop-options
 
 let foldm_back_sym #a (m:CM.cm a) (s1 s2: seq a)
   : Lemma