Simplify effects further

doc/book/PoP-in-FStar/book/part5/part5_meta.rst

@@ -226,13 +226,11 @@ goals.
 In the following simplified example, we are looking to prove ``s``
 from ``p`` given some lemmas. The first thing we do is apply the
 ``qr_s`` lemma, which gives us two subgoals, for ``q`` and ``r``
-respectively. We then need to proceed to solve the first goal for
-``q``. In order to isolate the proofs of both goals, we can ``focus``
-on the current goal making all others temporarily invisible. To prove
-``q``, we then just use the ``p_r`` lemma and obtain a subgoal for
-``p``. This one we will just just leave to the SMT solver, hence we
-call ``smt()`` to move it to the list of SMT goals. We prove ``r``
-similarly, using ``p_r``.
+respectively. We then proceed to solve the first goal for ``q`` using
+the ``p_q`` lemma, and the second one for ``r`` using ``p_r``. The
+precondition ``p`` of each of these lemmas is an implicit argument, so
+it is left to the SMT solver, just as it would be at an ordinary call
+site.
 
 .. literalinclude:: ../code/Part5.Mapply.fst
    :language: fstar

doc/book/code/Alex.fst

@@ -7,7 +7,9 @@ val f : (f:(nat -> int){unbounded f})
 
 let g : (nat -> int) = fun x -> f (x+1)
 
-#push-options "--fuel 0 --ifuel 0 --z3smtopt '(set-option :smt.qi.eager_threshold 2)'"
+(* eager_threshold 3, not 2: [unbounded]'s quantifier now needs one more round
+   of eager instantiation to reach the goal. *)
+#push-options "--fuel 0 --ifuel 0 --z3smtopt '(set-option :smt.qi.eager_threshold 3)'"
 let find_above_for_g (m:nat) : Lemma(exists (i:nat). abs(g i) > m) = 
   assert (unbounded f); // apply forall to m
   eliminate exists (n:nat). abs(f n) > m

doc/book/code/Part3.DataTypesALaCarte.fst

@@ -442,6 +442,10 @@ let ex6' = ex5'_l +^ ex5'_r
 let test56 = assert_norm (rewrite_distr () ex6 == ex6')
 //SNIPPET_END: rewrite_test$
 
+(* The `Add` branch's obligation sits just above this file's default budget
+   (it needs ~24 rlimit units of the 20 that `--z3rlimit_factor 4` buys).
+   Kept outside the snippet markers so the book text is unaffected. *)
+#push-options "--z3rlimit_factor 8"
 //SNIPPET_START: rewrite_soundness$
 let rec rewrite_soundness 
     (x:expr (value ++ add ++ mul))
@@ -460,6 +464,7 @@ let rec rewrite_soundness
       rewrite_soundness a l; rewrite_soundness b l;
       l.soundness()
 //SNIPPET_END: rewrite_soundness$
+#pop-options
 
 //SNIPPET_START: rewrite_distr_soundness$
 let rewrite_distr_soundness