diff --git a/lib/core/PulseCore.BaseHeapSig.fst b/lib/core/PulseCore.BaseHeapSig.fst
index 0c7cf9c19..47fd9cbc0 100644
--- a/lib/core/PulseCore.BaseHeapSig.fst
+++ b/lib/core/PulseCore.BaseHeapSig.fst
@@ -89,10 +89,9 @@ let emp_unit (p:slprop) : Lemma (p == (p `star` emp)) =
     star_equiv p emp h
   );
   slprop_extensionality p (p `star` emp)
-
-let pure_true_emp () : Lemma (pure True == emp) =
-  introduce forall h. interp (pure True) h <==> interp emp h with H2.intro_emp h;
-  slprop_extensionality (pure True) emp
+let pure_true_emp () : Lemma (pure u#a True == emp) =
+  introduce forall h. interp (pure u#a True) h <==> interp emp h with H2.intro_emp h;
+  slprop_extensionality (pure u#a True) emp
 let intro_emp (h:mem) : Lemma (interp emp h) = H2.intro_emp h
 let pure_interp (p:prop) (c:mem) : Lemma (interp (pure p) c == p) =
   H2.pure_interp p c; PropositionalExtensionality.apply (interp (pure p) c) p
diff --git a/lib/core/PulseCore.Heap2.fst b/lib/core/PulseCore.Heap2.fst
index 223cfe273..60b91c5ae 100644
--- a/lib/core/PulseCore.Heap2.fst
+++ b/lib/core/PulseCore.Heap2.fst
@@ -161,9 +161,9 @@ let lift_star (l:tag) (p q:H.slprop)
   );
   slprop_extensionality (llift l (p `H.star` q)) (llift l p `star` llift l q)
 #pop-options
-let lift_emp : squash (lift H.emp == emp) = 
-  FStar.Classical.forall_intro H.intro_emp;
-  slprop_extensionality (lift H.emp) emp
+let lift_emp : squash (lift H.emp == emp u#a) = 
+  FStar.Classical.forall_intro (H.intro_emp u#a);
+  slprop_extensionality (lift u#a H.emp) (emp u#a)
 
 let pts_to_compatible #a #pcm (x:ref a pcm) (v0 v1:a) h = 
   H.pts_to_compatible #a #pcm x v0 v1 h.concrete;
@@ -571,9 +571,9 @@ let lift_action_ghost
 let ni_erased a : non_informative (erased a) = fun x -> reveal x
 let ni_unit : non_informative unit = fun x -> reveal x
 
-let lift_ghost_emp : squash (llift GHOST H.emp == emp) = 
-  FStar.Classical.forall_intro H.intro_emp;
-  slprop_extensionality (llift GHOST H.emp) emp
+let lift_ghost_emp : squash (llift GHOST H.emp == emp u#a) = 
+  FStar.Classical.forall_intro (H.intro_emp u#a);
+  slprop_extensionality (llift GHOST H.emp) (emp u#a)
 
 let core_ghost_ref_as_addr i = H.core_ref_as_addr i
 let core_ghost_ref_is_null c = H.core_ref_is_null c
diff --git a/lib/core/PulseCore.MemoryAlt.fst b/lib/core/PulseCore.MemoryAlt.fst
index 4bb00c312..8a15d36f5 100644
--- a/lib/core/PulseCore.MemoryAlt.fst
+++ b/lib/core/PulseCore.MemoryAlt.fst
@@ -60,8 +60,10 @@ let emp_unit (p:slprop)
 : Lemma (p `equiv` (p `star` emp))
 = B.emp_unit p
 
+#push-options "--print_implicits --print_universes"
+
 let pure_equiv (p q:prop)
-: Lemma ((p <==> q) ==> (pure p `equiv` pure q))
+: Lemma ((p <==> q) ==> (pure u#a p `equiv` pure u#a q))
 = FStar.PropositionalExtensionality.apply p q
 
 let pure_true_emp (_:unit)
diff --git a/lib/pulse/lib/Pulse.Lib.HashTable.fst b/lib/pulse/lib/Pulse.Lib.HashTable.fst
index 745c0c588..52f273282 100644
--- a/lib/pulse/lib/Pulse.Lib.HashTable.fst
+++ b/lib/pulse/lib/Pulse.Lib.HashTable.fst
@@ -505,6 +505,7 @@ fn insert_if_not_full
   }
 }
 
+#restart-solver
 #push-options "--z3rlimit_factor 6"
 fn delete
   (#[@@@ Rust_generics_bounds ["Copy"; "PartialEq"; "Clone"]] kt:eqtype)
diff --git a/mk/checker.mk b/mk/checker.mk
index 9a48fb58d..0c55d6951 100644
--- a/mk/checker.mk
+++ b/mk/checker.mk
@@ -9,6 +9,8 @@ ROOTS += lib/common/Pulse.Lib.Tactics.fsti
 
 FSTAR_OPTIONS += --already_cached 'Prims,FStar'
 FSTAR_OPTIONS += --include lib/common
+FSTAR_OPTIONS += --smtencoding.elim_box true
+FSTAR_OPTIONS += --z3smtopt '(set-option :smt.arith.nl false)'
 EXTRACT += --extract '-*,+Pulse,+PulseSyntaxExtension'
 DEPFLAGS += --already_cached 'Prims,FStar,FStarC'
 
diff --git a/src/checker/Pulse.Checker.AssertWithBinders.fst b/src/checker/Pulse.Checker.AssertWithBinders.fst
index 0b64784c6..afa84306b 100644
--- a/src/checker/Pulse.Checker.AssertWithBinders.fst
+++ b/src/checker/Pulse.Checker.AssertWithBinders.fst
@@ -410,6 +410,7 @@ let rec add_rem_uvs (g:env) (t:typ) (uvs:env { Env.disjoint g uvs }) (v:slprop)
     let v = tm_pureapp v qopt (tm_var {nm_index = x; nm_ppname = ppname}) in
     add_rem_uvs g (comp_res ct) uvs v
 
+#push-options "--fuel 0 --ifuel 0"
 let check
   (g:env)
   (pre:term)
@@ -424,7 +425,7 @@ let check
   let g = push_context g "check_assert" st.range in
 
   let Tm_ProofHintWithBinders { hint_type; binders=bs; t=body } = st.term in
-
+  allow_invert hint_type;
   match hint_type with
   | WILD ->
     let st = check_wild g pre st in
@@ -543,3 +544,4 @@ let check
         { t with effect_tag = st.effect_tag }
     in
     check g pre pre_typing post_hint res_ppname st
+#pop-options
\ No newline at end of file
diff --git a/src/checker/Pulse.Checker.Base.fst b/src/checker/Pulse.Checker.Base.fst
index d6968dc6a..438475b5c 100644
--- a/src/checker/Pulse.Checker.Base.fst
+++ b/src/checker/Pulse.Checker.Base.fst
@@ -176,6 +176,7 @@ let post_hint_from_comp_typing #g #c ct =
   in
   p
 
+#push-options "--z3rlimit_factor 4"
 let comp_typing_from_post_hint
     (#g: env)
     (c: comp_st)
@@ -297,7 +298,7 @@ let comp_with_pre (c:comp_st) (pre:term) =
   | C_STGhost i st -> C_STGhost i { st with pre }
   | C_STAtomic i obs st -> C_STAtomic i obs {st with pre}
 
-
+#push-options "--fuel 0 --ifuel 0"
 let st_equiv_pre (#g:env) (#t:st_term) (#c:comp_st) (d:st_typing g t c)
                  (pre:term)
                  (veq: slprop_equiv g (comp_pre c) pre)
@@ -312,8 +313,6 @@ let st_equiv_pre (#g:env) (#t:st_term) (#c:comp_st) (d:st_typing g t c)
       in
       t_equiv d st_equiv
 
-
-#push-options "--z3rlimit_factor 4 --ifuel 2 --fuel 0"
 let k_elab_equiv_continuation (#g1:env) (#g2:env { g2 `env_extends` g1 }) (#ctxt #ctxt1 #ctxt2:term)
   (k:continuation_elaborator g1 ctxt g2 ctxt1)
   (d:slprop_equiv g2 ctxt1 ctxt2)
@@ -324,7 +323,6 @@ let k_elab_equiv_continuation (#g1:env) (#g2:env { g2 `env_extends` g1 }) (#ctxt
     assert (comp_pre c == ctxt2);
     let st_d' : st_typing g2 st (comp_with_pre c ctxt1) = st_equiv_pre st_d _ (VE_Sym _ _ _ d) in
     k post_hint (| st, _, st_d' |)
-#pop-options
 
 let slprop_equiv_typing_fwd (#g:env) (#ctxt:_) (ctxt_typing:tot_typing g ctxt tm_slprop)
                            (#p:_) (d:slprop_equiv g ctxt p)
@@ -332,7 +330,6 @@ let slprop_equiv_typing_fwd (#g:env) (#ctxt:_) (ctxt_typing:tot_typing g ctxt tm
   = let fwd, _ = slprop_equiv_typing d in
     fwd ctxt_typing
 
-#push-options "--z3rlimit_factor 4 --ifuel 1 --fuel 0"
 let k_elab_equiv_prefix
   (#g1:env) (#g2:env { g2 `env_extends` g1 }) (#ctxt1 #ctxt2 #ctxt:term)
   (k:continuation_elaborator g1 ctxt1 g2 ctxt)
@@ -347,7 +344,6 @@ let k_elab_equiv_prefix
   let (| st, c, st_d |) = res in
   assert (comp_pre c == ctxt1);
   (| _, _, st_equiv_pre st_d _ d |)
- #pop-options
 
 let k_elab_equiv
   (#g1:env) (#g2:env { g2 `env_extends` g1 }) (#ctxt1 #ctxt1' #ctxt2 #ctxt2':term)                 
@@ -362,7 +358,7 @@ let k_elab_equiv
     k_elab_equiv_prefix k d1 in
   k
 
-#push-options "--fuel 3 --ifuel 2 --split_queries no --z3rlimit_factor 20"
+#push-options "--fuel 3 --ifuel 1 --split_queries no --z3rlimit_factor 20"
 open Pulse.PP
 let continuation_elaborator_with_bind' (#g:env) (ctxt:term)
   (#c1:comp{stateful_comp c1})
@@ -571,6 +567,7 @@ let emp_inames_included (g:env) (i:term) (_:tot_typing g i tm_inames)
 : prop_validity g (tm_inames_subset tm_emp_inames i)
 = RU.magic()
 
+#push-options "--ifuel 1"
 let return_in_ctxt (g:env) (y:var) (y_ppname:ppname) (u:universe) (ty:term) (ctxt:slprop)
   (ty_typing:universe_of g ty u)
   (post_hint0:post_hint_opt g { PostHint? post_hint0 /\ checker_res_matches_post_hint g post_hint0 y ty ctxt})
@@ -614,8 +611,9 @@ let return_in_ctxt (g:env) (y:var) (y_ppname:ppname) (u:universe) (ty:term) (ctx
   | _ -> 
     (| _, _, d |)
 
-#push-options "--z3rlimit_factor 2"
+#push-options "--z3rlimit_factor 4 --ifuel 1 --split_queries always"
 #restart-solver
+#show-options
 let match_comp_res_with_post_hint (#g:env) (#t:st_term) (#c:comp_st)
   (d:st_typing g t c)
   (post_hint:post_hint_opt g)
@@ -651,6 +649,7 @@ let match_comp_res_with_post_hint (#g:env) (#t:st_term) (#c:comp_st)
 
            (| t, c', Pulse.Typing.Combinators.t_equiv d d_stequiv |)
 #pop-options
+#pop-options
 
 let apply_checker_result_k (#g:env) (#ctxt:slprop) (#post_hint:post_hint_for_env g)
   (r:checker_result_t g ctxt (PostHint post_hint))
@@ -667,7 +666,7 @@ let apply_checker_result_k (#g:env) (#ctxt:slprop) (#post_hint:post_hint_for_env
 
   k (PostHint post_hint) d
 
-#push-options "--z3rlimit_factor 4 --fuel 0 --ifuel 1"
+#push-options "--z3rlimit_factor 4 --fuel 0 --ifuel 0"
 //TODO: refactor and merge with continuation_elaborator_with_bind
 let checker_result_for_st_typing (#g:env) (#ctxt:slprop) (#post_hint:post_hint_opt g)
   (d:st_typing_in_ctxt g ctxt post_hint)
@@ -723,6 +722,7 @@ let readback_comp_res_as_comp (c:T.comp) : option comp =
   )
   | _ -> None
 
+#push-options "--ifuel 1"
 let rec is_stateful_arrow (g:env) (c:option comp) (args:list T.argv) (out:list T.argv)
   : T.Tac (option (list T.argv & T.argv))
   = let open R in
@@ -779,6 +779,7 @@ let rec is_stateful_arrow (g:env) (c:option comp) (args:list T.argv) (out:list T
         )
         else None
     )
+#pop-options
 
 let checker_result_t_equiv_ctxt (g:env) (ctxt ctxt' : slprop)
   (post_hint:post_hint_opt g)
@@ -796,14 +797,17 @@ let is_stateful_application (g:env) (e:term)
 : T.Tac (option st_term) = 
   RU.record_stats "Pulse.is_stateful_application" fun _ -> 
   let head, args = T.collect_app_ln e in
-  if Nil? args then None else
-  match RU.tc_term_phase1 (elab_env g) head false with
-  | None, _ -> None
-  | Some (_, ht, _), _ -> 
-    let head_t = wr ht (T.range_of_term ht) in
-    match is_stateful_arrow g (Some (C_Tot head_t)) args [] with 
-    | None -> None
-    | Some _ -> Some (as_stateful_application e head args)
+  match args with
+  | _ :: _ -> (
+    match RU.tc_term_phase1 (elab_env g) head false with
+    | None, _ -> None
+    | Some (_, ht, _), _ -> 
+      let head_t = wr ht (T.range_of_term ht) in
+      match is_stateful_arrow g (Some (C_Tot head_t)) args [] with 
+      | None -> None
+      | Some _ -> Some (as_stateful_application e head args)
+  )
+  | _ -> None
 
 let apply_conversion
       (#g:env) (#e:term) (#eff:_) (#t0:term)
@@ -888,6 +892,7 @@ let norm_st_typing_inverse
 
 open FStar.List.Tot    
 module RT = FStar.Reflection.Typing
+#push-options "--ifuel 1"
 let decompose_app (g:env) (tt:either term st_term)
 : T.Tac (option (term & list T.argv & (args:list T.argv{ Cons? args } -> T.Tac (res:either term st_term { Inr? tt ==> Inr? res }))))
 = let decompose_st_app (t:st_term)
@@ -919,6 +924,7 @@ let decompose_app (g:env) (tt:either term st_term)
       Some (head, args, rebuild)
   )
   | Inr st -> decompose_st_app st
+#pop-options
 
 let anf_binder name = T.pack (T.Tv_FVar (T.pack_fv (Pulse.Reflection.Util.mk_pulse_lib_core_lid (Printf.sprintf "__%s_binder__" name))))
 
@@ -958,11 +964,14 @@ let rec maybe_hoist (g:env) (arg:T.argv)
   )
   | Some _ -> (
     let g, binders, args = maybe_hoist_args g args in
-    if Nil? args then T.fail "Impossible";
-    let st_app = as_stateful_application t head args  in
-    let g, b, x, t = bind_st_term g st_app in
-    let arg = t, q in
-    g, binders@[b, x, st_app], arg
+    if Cons? args 
+    then (
+      let st_app = as_stateful_application t head args  in
+      let g, b, x, t = bind_st_term g st_app in
+      let arg = t, q in
+      g, binders@[b, x, st_app], arg
+    )
+    else T.fail "Impossible: is_stateful_application returned true but no args to hoist"
   )
 
 and maybe_hoist_args (g:env) (args:list T.argv)
@@ -975,6 +984,7 @@ and maybe_hoist_args (g:env) (args:list T.argv)
     args
     (g, [], [])
 
+#push-options "--ifuel 1"
 let maybe_hoist_top 
   (hoist_top_level:bool)
   (g:env)
diff --git a/src/checker/Pulse.Checker.Bind.fst b/src/checker/Pulse.Checker.Bind.fst
index 37b4c77c2..639419e9c 100644
--- a/src/checker/Pulse.Checker.Bind.fst
+++ b/src/checker/Pulse.Checker.Bind.fst
@@ -31,7 +31,7 @@ module Metatheory = Pulse.Typing.Metatheory
 module Abs = Pulse.Checker.Abs
 module RU = Pulse.Reflection.Util
 
-#push-options "--z3rlimit_factor 4 --split_queries no"
+#push-options "--z3rlimit_factor 8 --split_queries no --query_stats --fuel 0 --ifuel 1"
 let check_bind_fn
   (g:env)
   (ctxt:slprop)
@@ -62,7 +62,6 @@ let check_bind_fn
     checker_result_for_st_typing d res_ppname
   )
   | _ -> fail g (Some t.range) "check_bind_fn: head is not an abstraction"
-#pop-options
 
 let check_if_seq_lhs
   (g:env) (ctxt : slprop) (post_hint : post_hint_opt g)
@@ -226,4 +225,5 @@ let check_tot_bind
       Printf.sprintf "Elaborated and proceeding back to top-level\n%s\nto\n%s\n" 
       (show t)
       (show t'));
-    check g pre pre_typing post_hint res_ppname t'
\ No newline at end of file
+    check g pre pre_typing post_hint res_ppname t'
+#pop-options
\ No newline at end of file
diff --git a/src/checker/Pulse.Checker.If.fst b/src/checker/Pulse.Checker.If.fst
index df757e0c8..085acc0e1 100644
--- a/src/checker/Pulse.Checker.If.fst
+++ b/src/checker/Pulse.Checker.If.fst
@@ -43,7 +43,7 @@ let retype_checker_result (#g:env) (#ctxt:slprop) (#ph:post_hint_opt g) (ph':pos
 = let (| x, g1, t, ctxt, k |) = r in
   (| x, g1, t, ctxt, k |)
 
-#push-options "--fuel 0 --ifuel 1 --z3rlimit_factor 2"
+#push-options "--fuel 0 --ifuel 0 --z3rlimit_factor 2"
 #restart-solver
 let check
   (g:env)
diff --git a/src/checker/Pulse.Checker.Match.fst b/src/checker/Pulse.Checker.Match.fst
index b951a5df0..4a6813795 100644
--- a/src/checker/Pulse.Checker.Match.fst
+++ b/src/checker/Pulse.Checker.Match.fst
@@ -139,6 +139,8 @@ let lemma_map_opt_dec_index (top:'z) (f : (x:'a{x << top}) -> option 'b) (xs : l
           (ensures forall i. f (xs `L.index` i) == Some (ys `L.index` i))
   = Classical.forall_intro (Classical.move_requires (__lemma_map_opt_dec_index top f xs ys))
 
+#push-options "--fuel 2 --ifuel 2 --z3rlimit_factor 2 --query_stats"
+#restart-solver
 let rec elab_readback_pat_x (rp : R.pattern) (p : pattern)
   : Lemma (requires readback_pat rp == Some p)
           (ensures elab_pat p == rp)
@@ -195,6 +197,7 @@ and elab_readback_subpat (pb : R.pattern & bool)
           (ensures elab_sub_pat (Some?.v (readback_sub_pat pb)) == pb)
   = let (p, b) = pb in
     elab_readback_pat_x p (Some?.v (readback_pat p))
+#pop-options
 
 val tot_typing_weakening_n
    (#g:env) (#t:term) (#ty:term)
@@ -236,8 +239,8 @@ let rec bindings_to_string (bs : list binding) : T.Tac string =
   | b::bs ->
     (string_of_int (fst b) ^ ":" ^ Pulse.Syntax.Printer.term_to_string (snd b) ^ " ") ^ bindings_to_string bs
 
-#push-options "--z3rlimit 20"
-
+#push-options "--z3rlimit 40 --fuel 0 --ifuel 1"
+#restart-solver
 let check_branch
         (norw:bool)
         (g:env)
@@ -437,7 +440,7 @@ let rec least_tag (#g #pre #post_hint #sc_u #sc_ty #sc:_)
     | C_STAtomic i _ _ -> STT_Atomic
 
 
-#push-options "--z3rlimit_factor 4 --fuel 0 --ifuel 1"
+#push-options "--z3rlimit_factor 4 --fuel 0 --ifuel 0"
 #restart-solver
 let weaken_branch_tag_to 
       (#g #pre #post_hint #sc_u #sc_ty #sc:_) 
@@ -448,6 +451,7 @@ let weaken_branch_tag_to
   if ctag_of_comp_st c = ct then br
   else
     let r = pe.e.range in
+    allow_invert ct; allow_invert c;
     match ct, c with
     | STT_Ghost, C_STAtomic _ _ _
     | STT_Ghost, C_ST _ -> T.fail "Unexpected least effect"
@@ -464,6 +468,7 @@ let weaken_branch_tag_to
       let d = TBRV g sc_u sc_ty sc _ p e bs pf1 pf2 pf3 h d in
       (| pe, _, d |)
     )
+    
 
 
 let weaken_branch_tags
@@ -473,7 +478,9 @@ let weaken_branch_tags
 = let ct = least_tag checked_brs in
   let brs = T.map (weaken_branch_tag_to ct) checked_brs in
   (| ct, brs |)
+#pop-options
 
+#push-options "--z3rlimit_factor 4 --fuel 0 --ifuel 1"
 let maybe_weaken_branch_tags
       (#g #pre #post_hint #sc_u #sc_ty #sc:_) 
       (checked_brs : list (check_branches_aux_t #g pre post_hint sc_u sc_ty sc))
@@ -531,7 +538,7 @@ let check_branches
   let brs = List.Tot.map dfst checked_brs in
   let d : brs_typing g sc_u sc_ty sc brs c0 = check_branches_aux2 g sc_u sc_ty sc c0 checked_brs in
   (| brs, c0, d |)
-
+#push-options "--fuel 0 --ifuel 1 --z3rlimit_factor 4 --query_stats"
 let check
         (g:env)
         (pre:term)
@@ -598,3 +605,4 @@ let check
   let c_typing = comp_typing_from_post_hint c pre_typing post_hint in
   let d = T_Match g sc_u sc_ty sc sc_ty_typing sc_typing c (E c_typing) brs brs_d complete_d in
   checker_result_for_st_typing (| _, _, d |) res_ppname
+#pop-options
\ No newline at end of file
diff --git a/src/checker/Pulse.Checker.Prover.Base.fst b/src/checker/Pulse.Checker.Prover.Base.fst
index 0fcd3826a..a95348211 100644
--- a/src/checker/Pulse.Checker.Prover.Base.fst
+++ b/src/checker/Pulse.Checker.Prover.Base.fst
@@ -78,7 +78,7 @@ let canon_right (#g:env) (#ctxt:term) (#frame:term)
       = VE_Ctxt _ _ _ _ _ veq (VE_Refl _ _) in
     (| _, VP.slprop_equiv_typing_fwd ctxt_frame_typing veq, k_elab_equiv (k_elab_unit _ _) (VE_Refl _ _) veq |)
 
-
+#push-options "--fuel 0 --ifuel 0"
 let elim_one (#g:env)
   (ctxt:term) (frame:slprop) (p:slprop)
   (ctxt_frame_p_typing:tot_typing g (tm_star (tm_star ctxt frame) p) tm_slprop)
@@ -185,3 +185,4 @@ let rec add_elims (#g:env) (#ctxt:term) (#frame:term)
       let (| g'', ctxt'', ctxt''_typing, k' |) = add_elims f mk ctxt'_typing uvs in
       (| g'', ctxt'', ctxt''_typing, k_elab_trans k k' |)
      )
+#pop-options
\ No newline at end of file
diff --git a/src/checker/Pulse.Checker.Prover.ElimExists.fst b/src/checker/Pulse.Checker.Prover.ElimExists.fst
index 66a6bf51a..baf20b829 100644
--- a/src/checker/Pulse.Checker.Prover.ElimExists.fst
+++ b/src/checker/Pulse.Checker.Prover.ElimExists.fst
@@ -15,7 +15,7 @@
 *)
 
 module Pulse.Checker.Prover.ElimExists
-
+#set-options "--z3rlimit 10" //base rlimit x 2
 open Pulse.Syntax
 open Pulse.Typing
 open Pulse.Typing.Combinators
diff --git a/src/checker/Pulse.Checker.Prover.ElimPure.fst b/src/checker/Pulse.Checker.Prover.ElimPure.fst
index a7eba742d..25ff68628 100644
--- a/src/checker/Pulse.Checker.Prover.ElimPure.fst
+++ b/src/checker/Pulse.Checker.Prover.ElimPure.fst
@@ -15,7 +15,7 @@
 *)
 
 module Pulse.Checker.Prover.ElimPure
-
+#set-options "--z3rlimit 10" //base rlimit x 2
 module RT = FStar.Reflection.Typing
 module R = FStar.Reflection.V2
 module T = FStar.Tactics.V2
diff --git a/src/checker/Pulse.Checker.Prover.ElimWithPure.fst b/src/checker/Pulse.Checker.Prover.ElimWithPure.fst
index 4842a1509..49a2dacba 100644
--- a/src/checker/Pulse.Checker.Prover.ElimWithPure.fst
+++ b/src/checker/Pulse.Checker.Prover.ElimWithPure.fst
@@ -59,6 +59,7 @@ let is_elim_with_pure (vp:term) : T.Tac bool =
   | Tm_WithPure .. -> true
   | _ -> false
 
+#push-options "--fuel 0 --ifuel 0"
 let mk (#g:env) (#v:slprop) (v_typing:tot_typing g v tm_slprop)
   : T.Tac (option (x:ppname &
                    t:st_term &
@@ -84,6 +85,7 @@ let elim_with_pure_frame (#g:env) (#ctxt:term) (#frame:term)
 
 // a lot of this is copy-pasted from elim_exists_pst,
 //   can add a common function to Prover.Common
+#push-options "--z3rlimit_factor 4 --ifuel 1"
 let elim_with_pure_pst (#preamble:_) (pst:prover_state preamble)
   : T.Tac (pst':prover_state preamble { pst' `pst_extends` pst /\
                                         pst'.unsolved == pst.unsolved }) =
@@ -133,3 +135,5 @@ let elim_with_pure_pst (#preamble:_) (pst:prover_state preamble)
     goals_inv = RU.magic ();  // weakening of pst.goals_inv
     solved_inv = ();
   }
+#pop-options
+#pop-options
\ No newline at end of file
diff --git a/src/checker/Pulse.Checker.Prover.IntroExists.fst b/src/checker/Pulse.Checker.Prover.IntroExists.fst
index 3f531c7e8..109ab4d5a 100644
--- a/src/checker/Pulse.Checker.Prover.IntroExists.fst
+++ b/src/checker/Pulse.Checker.Prover.IntroExists.fst
@@ -15,7 +15,7 @@
 *)
 
 module Pulse.Checker.Prover.IntroExists
-
+#set-options "--z3rlimit 20" //base rlimit x 4
 open Pulse.Syntax
 open Pulse.Typing
 open Pulse.Typing.Combinators
diff --git a/src/checker/Pulse.Checker.Prover.IntroPure.fst b/src/checker/Pulse.Checker.Prover.IntroPure.fst
index 6027d0d06..7ae753b7f 100644
--- a/src/checker/Pulse.Checker.Prover.IntroPure.fst
+++ b/src/checker/Pulse.Checker.Prover.IntroPure.fst
@@ -32,7 +32,7 @@ module P = Pulse.Syntax.Printer
 module PS = Pulse.Checker.Prover.Substs
 
 let coerce_eq (#a #b:Type) (x:a) (_:squash (a == b)) : y:b{y == x} = x
-
+#push-options "--z3rlimit_factor 4"
 let k_intro_pure (g:env) (p:term)
   (d:tot_typing g p tm_prop)
   (token:prop_validity g p) (frame:slprop)
@@ -74,7 +74,7 @@ let k_intro_pure (g:env) (p:term)
       (push_binding g x ppname_default tm_unit) in
 
   k post_hint (| t1, c1, d1 |)
-
+#pop-options
 module R = FStar.Reflection.V2
 
 // let is_eq2 (t:R.term) : option (R.term & R.term) =
@@ -210,6 +210,7 @@ let rec try_collect_substs (uvs:env) (t:term)
 
   | _ -> PS.empty
 
+#push-options "--z3rlimit_factor 4"
 let intro_pure (#preamble:_) (pst:prover_state preamble)
   (t:term)
   (unsolved':list slprop)
@@ -358,3 +359,4 @@ let intro_pure (#preamble:_) (pst:prover_state preamble)
                                                    solved_inv = () } in
 
   Some pst_new
+#pop-options
\ No newline at end of file
diff --git a/src/checker/Pulse.Checker.Prover.Match.Comb.fst b/src/checker/Pulse.Checker.Prover.Match.Comb.fst
index 727ea7bab..33379971b 100644
--- a/src/checker/Pulse.Checker.Prover.Match.Comb.fst
+++ b/src/checker/Pulse.Checker.Prover.Match.Comb.fst
@@ -102,6 +102,8 @@ let frame_match_from_context
     proof      = mm.proof;
 }
 
+#push-options "--z3rlimit_factor 4"
+(* The result of a match pass, trying to match all of ctxt to all of unsolved. *)
 (* Returns all successful matches of q in ps. *)
 let rec get_all_matches_aux
   (label : string)
@@ -152,6 +154,7 @@ let rec get_all_matches_aux
       get_all_matches_aux label matcher pst q (p::ps0) ps'
     in
     thisone @ rest
+#pop-options 
 
 let get_all_matches
   (label : string)
diff --git a/src/checker/Pulse.Checker.Prover.fst b/src/checker/Pulse.Checker.Prover.fst
index 8b39add61..c4b55f540 100644
--- a/src/checker/Pulse.Checker.Prover.fst
+++ b/src/checker/Pulse.Checker.Prover.fst
@@ -139,6 +139,7 @@ let normalize_slprop_context
       goals_inv = RU.magic ();
   }
 
+#push-options "--z3rlimit_factor 4"
 let rec __intro_any_exists (n:nat)
   (#preamble:_)
   (pst:prover_state preamble)
@@ -172,6 +173,7 @@ let rec __intro_any_exists (n:nat)
         } in
         __intro_any_exists (n-1) pst prover
   )
+#pop-options
 
 let unsolved_equiv_pst (#preamble:_) (pst:prover_state preamble) (unsolved':list slprop)
   (d:slprop_equiv (push_env pst.pg pst.uvs) (list_as_slprop pst.unsolved) (list_as_slprop unsolved'))
@@ -205,6 +207,7 @@ let rec collect_pures (g:env) (l:list slprop)
     | Tm_Pure _ -> (| hd::pures, rest, RU.magic #(slprop_equiv _ _ _) () |)
     | _ -> (| pures, hd::rest, RU.magic #(slprop_equiv _ _ _) () |)
 #push-options "--fuel 0"
+#push-options "--z3rlimit_factor 4"
 let rec prove_pures #preamble (pst:prover_state preamble)
   : T.Tac (pst':prover_state preamble { pst' `pst_extends` pst /\
                                         is_terminal pst' }) =
@@ -231,6 +234,7 @@ let rec prove_pures #preamble (pst:prover_state preamble)
       fail pst.pg None
         (Printf.sprintf "Impossible! prover.prove_pures: %s is not a pure, please file a bug-report"
            (P.term_to_string (L.hd pst.unsolved)))
+#pop-options
 
 let intro_any_exists 
   (#preamble:_)
@@ -327,7 +331,8 @@ let prover_iteration
     P "match_full"        Match.match_full;
   ]
 
-#push-options "--z3rlimit_factor 6 --ifuel 2"
+#push-options "--z3rlimit_factor 40 --ifuel 2"
+#restart-solver
 let rec prover
   (#preamble:_)
   (pst0:prover_state preamble)
@@ -587,7 +592,7 @@ let typing_canon #g #t (#c:comp_st) (d:st_typing g t c) : st_typing g t (canon_p
   assume false;
   d
 
-#push-options "--z3rlimit_factor 8 --fuel 0 --ifuel 2 --split_queries no"
+#push-options "--z3rlimit_factor 10 --fuel 0 --ifuel 2 --split_queries no"
 #restart-solver
 let try_frame_pre_uvs
   (allow_ambiguous : bool)
@@ -690,6 +695,8 @@ let try_frame_pre
   assert (equal g (push_env g uvs));
   try_frame_pre_uvs allow_ambiguous ctxt_typing uvs d res_ppname
 
+#push-options "--z3rlimit_factor 4"
+#restart-solver
 let prove_post_hint (#g:env) (#ctxt:slprop)
   (r:checker_result_t g ctxt NoHint)
   (post_hint:post_hint_opt g)
@@ -762,3 +769,4 @@ let elim_exists_and_pure (#g:env) (#ctxt:slprop)
 
   let (| g', _nts, _labels, ctxt', k |) = prove false #g #ctxt ctxt_typing (mk_env (fstar_env g)) emp_typing in
   (| g', ctxt', E (RU.magic ()), k_elab_equiv k (VE_Refl _ _) (VE_Unit _ _) |)
+#pop-options
\ No newline at end of file
diff --git a/src/checker/Pulse.Checker.Return.fst b/src/checker/Pulse.Checker.Return.fst
index ff9fa2170..68efab5d4 100644
--- a/src/checker/Pulse.Checker.Return.fst
+++ b/src/checker/Pulse.Checker.Return.fst
@@ -69,7 +69,7 @@ let compute_tot_or_ghost_term_type_and_u (g:env) (e:term) (c:option ctag)
   let (| c, e, d |) = check_effect d c in
   R c e u ty ud d
 
-#push-options "--z3rlimit_factor 8 --fuel 0 --ifuel 1"
+#push-options "--z3rlimit_factor 16 --fuel 0 --ifuel 1 --query_stats --split_queries no --log_queries"
 #restart-solver
 let check_core
   (g:env)
diff --git a/src/checker/Pulse.Checker.ST.fst b/src/checker/Pulse.Checker.ST.fst
index 9efcaa707..2b22a0e64 100644
--- a/src/checker/Pulse.Checker.ST.fst
+++ b/src/checker/Pulse.Checker.ST.fst
@@ -62,7 +62,7 @@ let instantiate_term_implicits_uvs (g:env) (t:term)
   add_implicits uvs t ty
 
 open Pulse.PP
-
+#push-options "--fuel 0 --ifuel 1 --z3rlimit_factor 2"
 let check
   (g0:env)
   (ctxt:slprop)
diff --git a/src/checker/Pulse.Checker.While.fst b/src/checker/Pulse.Checker.While.fst
index 3cff8dd88..af9892c9a 100644
--- a/src/checker/Pulse.Checker.While.fst
+++ b/src/checker/Pulse.Checker.While.fst
@@ -38,7 +38,7 @@ let while_body_comp_typing (#g:env) (u:universe) (x:ppname) (ty:term) (inv_body:
   : Dv (comp_typing_u g (comp_while_body x inv_body))
   = Metatheory.admit_comp_typing g (comp_while_body x inv_body)
 
-#push-options "--fuel 0 --ifuel 1 --z3rlimit_factor 8"
+#push-options "--fuel 0 --ifuel 0 --z3rlimit_factor 8 --query_stats"
 #restart-solver
 let check
   (g:env)
@@ -154,7 +154,7 @@ let inv_as_post_hint (#g:env) (#inv:slprop) (inv_typing:tot_typing g inv tm_slpr
     x; post_typing_src; post_typing=RU.magic() }
 
 
-#push-options "--fuel 0 --ifuel 1 --z3rlimit_factor 8"
+#push-options "--fuel 0 --ifuel 0 --z3rlimit_factor 8"
 
 let check_nuwhile
   (g:env)
diff --git a/src/checker/Pulse.Checker.WithInv.fst b/src/checker/Pulse.Checker.WithInv.fst
index ce2b50860..a519215f2 100644
--- a/src/checker/Pulse.Checker.WithInv.fst
+++ b/src/checker/Pulse.Checker.WithInv.fst
@@ -236,7 +236,7 @@ let withinv_post (#g:env) (#p:term) (#i:term) (#post:term)
   let (| post, _, post_typing |) = Prover.normalize_slprop_welltyped g post post_typing in
   __withinv_post #g #p #i #post p_typing i_typing post_typing
 
-#push-options "--z3rlimit_factor 40 --split_queries no --fuel 0 --ifuel 1 --z3cliopt 'smt.qi.eager_threshold=100'"
+#push-options "--fuel 0 --ifuel 0 --query_stats" 
 #restart-solver
 let mk_post_hint g returns_inv i p (ph:post_hint_opt g) rng
 : T.Tac (q:post_hint_for_env g { PostHint? ph ==> q == PostHint?.v ph })
@@ -295,6 +295,8 @@ let mk_post_hint g returns_inv i p (ph:post_hint_opt g) rng
   in
   post_hint
 
+#push-options "--z3rlimit_factor 25 --split_queries no"
+#restart-solver
 let check0
   (g:env)
   (pre:term)
@@ -366,7 +368,7 @@ let check0
             (show i) (show p) (show p'));
   assert (p == p');
   let post_body = tm_star (tm_later p) post_frame in
-  
+  allow_invert post_hint.effect_annot; 
   let (| opens, opens_typing |) 
     : t:term & tot_typing g t tm_inames 
     = match post_hint.effect_annot with
diff --git a/src/checker/Pulse.Checker.WithLocal.fst b/src/checker/Pulse.Checker.WithLocal.fst
index 6c74c8e89..8b34a657d 100644
--- a/src/checker/Pulse.Checker.WithLocal.fst
+++ b/src/checker/Pulse.Checker.WithLocal.fst
@@ -46,7 +46,8 @@ let with_local_pre_typing (#g:env) (#pre:term) (pre_typing:tot_typing g pre tm_s
                tm_slprop
   = admit()
 
-#push-options "--z3rlimit_factor 10 --fuel 0 --ifuel 1 --split_queries no"
+#push-options "--z3rlimit_factor 10 --fuel 0 --ifuel 0 --query_stats"
+
 let head_range (t:st_term {Tm_WithLocal? t.term}) : range =
   let Tm_WithLocal { initializer } = t.term in
   (RU.range_of_term initializer)
@@ -60,7 +61,8 @@ let check
   (t:st_term { Tm_WithLocal? t.term })
   (check:check_t)
 : T.Tac (checker_result_t g pre post_hint)
-= match post_hint with
+= allow_invert post_hint;
+  match post_hint with
   | NoHint | TypeHint _ ->
     fail g (Some <| head_range t)
       "Allocating a mutable local variable expects an annotated post-condition"
@@ -113,11 +115,10 @@ let check
                           please file a bug-report"
         else
           let open Pulse.Typing.Combinators in
-          let body_post = extend_post_hint_for_local g post init_t x in
-          let (| opened_body, c_body, body_typing |) =
-            let r =
-              check g_extended body_pre body_pre_typing (PostHint body_post) binder.binder_ppname (open_st_term_nv body px) in
-            apply_checker_result_k r binder.binder_ppname in
+          let body_post : post_hint_for_env g_extended = extend_post_hint_for_local g post init_t x in
+          let r = check g_extended body_pre body_pre_typing (PostHint body_post) binder.binder_ppname (open_st_term_nv body px) in
+          let r: checker_result_t g_extended body_pre (PostHint body_post) = r in
+          let (| opened_body, c_body, body_typing |) = apply_checker_result_k #g_extended #body_pre #body_post r binder.binder_ppname in
           let body = close_st_term opened_body x in
           assume (open_st_term (close_st_term opened_body x) x == opened_body);
           let c = C_ST {u=comp_u c_body;res=comp_res c_body;pre;post=post.post} in
diff --git a/src/checker/Pulse.Checker.fst b/src/checker/Pulse.Checker.fst
index dd839b3dd..f2082e98d 100644
--- a/src/checker/Pulse.Checker.fst
+++ b/src/checker/Pulse.Checker.fst
@@ -177,7 +177,7 @@ let maybe_setting_error_bound (t:st_term) (f : unit -> T.Tac 'a) : T.Tac 'a =
 
 #push-options "--z3rlimit_factor 4 --fuel 0 --ifuel 1"
 
-let rec maybe_elaborate_stateful_head (g:env) (t:st_term)
+let maybe_elaborate_stateful_head (g:env) (t:st_term)
 : T.Tac (option st_term)
 = match t.term with
   | Tm_ST .. ->
@@ -229,7 +229,10 @@ let rec maybe_elaborate_stateful_head (g:env) (t:st_term)
   )
 
   | _ -> None
+#pop-options
+#restart-solver
 
+#push-options "--fuel 0 --ifuel 1 --query_stats --z3rlimit 200"
 let rec check
   (g0:env)
   (pre0:term)
@@ -261,7 +264,7 @@ let rec check
     );
 
     match maybe_elaborate_stateful_head g0 t with
-    | Some t -> 
+    | Some t ->
       check g0 pre0 pre0_typing post_hint res_ppname t
     | None -> 
       let (| g, pre, pre_typing, k_elim_pure |) = 
@@ -274,12 +277,6 @@ let rec check
           Return.check g pre pre_typing post_hint res_ppname t check
         
         | Tm_Abs _ ->
-          // let (| t, c, typing |) = Pulse.Checker.Abs.check_abs g t check in
-          // Pulse.Checker.Prover.prove_post_hint (
-          //   Pulse.Checker.Prover.try_frame_pre
-          //     pre_typing
-              
-          // )
           T.fail "Tm_Abs check should not have been called in the checker"
 
         | Tm_ST _ ->
@@ -289,8 +286,7 @@ let rec check
         | Tm_ElimExists _ ->
           Exists.check_elim_exists g pre pre_typing post_hint res_ppname t
 
-        | Tm_IntroExists _ ->
-          (
+        | Tm_IntroExists _ -> (
           (* First of all, elaborate *)
           let prep (t:st_term{Tm_IntroExists? t.term}) : T.Tac (t:st_term{Tm_IntroExists? t.term}) =
             let Tm_IntroExists { p; witnesses } = t.term in
@@ -311,7 +307,9 @@ let rec check
               Exists.check_intro_exists g pre pre_typing post_hint res_ppname t None 
             | _ ->
               let t = transform_to_unary_intro_exists g p witnesses in
-              check g pre pre_typing post_hint res_ppname t)
+              check g pre pre_typing post_hint res_ppname t
+        )
+
         | Tm_Bind _ ->
           Bind.check_bind g pre pre_typing post_hint res_ppname t check
 
diff --git a/src/checker/Pulse.Recursion.fst b/src/checker/Pulse.Recursion.fst
index a36e4f0fd..e838cf4bc 100644
--- a/src/checker/Pulse.Recursion.fst
+++ b/src/checker/Pulse.Recursion.fst
@@ -114,13 +114,13 @@ let rec recover_bs (g: env) (qbs: list (option qualifier & binder & bv)) (ty: te
   | [], _ ->
     [], ty
 
+#push-options "--fuel 2 --ifuel 0 --z3rlimit_factor 2"
 let add_knot (g : env) (rng : R.range)
              (d : decl{FnDefn? d.d})
 : Tac (d : decl{FnDefn? d.d})
-=
-  let FnDefn { id; isrec; us; bs; comp; meas; body } = d.d in
-  if List.length bs < 2 then
-    fail g (Some d.range) "main: FnDefn does not have binders";
+= let FnDefn { id; isrec; us; bs; comp; meas; body } = d.d in
+  allow_invert bs;
+  if List.length bs < 2 then fail g (Some d.range) "main: FnDefn does not have binders";
   (* NB: bs, comp, body are open *)
   debug_main g
     (fun _ -> Printf.sprintf "add_knot: bs = %s\n"
@@ -240,7 +240,8 @@ let add_knot (g : env) (rng : R.range)
   { d with d =
     FnDefn { id=id'; isrec=false; us; bs=bs'; comp = C_Tot comp; meas=None; body }
   }
-
+#pop-options
+#push-options "--fuel 0 --ifuel 0"
 let tie_knot (g : env)
              (rng : R.range)
              (nm_orig nm_aux : string)
@@ -251,9 +252,9 @@ let tie_knot (g : env)
     (* Remove the last arguments from r_typ, as that is the recursive knot.
     After doing that, we now have the needed type for elaboration. *)
     let bs, c = collect_arr_bs r_typ in
-    if Nil? bs then fail g (Some rng) "tie_knot: impossible (1)";
+    if not (Cons? bs) then fail g (Some rng) "tie_knot: impossible (1)";
     let bs = init bs in
-    if Nil? bs then fail g (Some rng) "tie_knot: impossible (2)";
+    if not (Cons? bs) then fail g (Some rng) "tie_knot: impossible (2)";
     mk_arr bs c
   in
   (* This is a temporary implementation. It will just create
@@ -262,3 +263,4 @@ let tie_knot (g : env)
   let nm = string_as_term nm_aux in 
   let sig = RU.add_attribute sig (`("pulse.recursive.knot", `#(nm))) in
   flag, sig, Some blob
+#pop-options
\ No newline at end of file
diff --git a/src/checker/Pulse.Syntax.Base.fsti b/src/checker/Pulse.Syntax.Base.fsti
index 7e955abc0..5ffc0ad25 100644
--- a/src/checker/Pulse.Syntax.Base.fsti
+++ b/src/checker/Pulse.Syntax.Base.fsti
@@ -20,6 +20,8 @@ module R = FStar.Reflection.V2
 module T = FStar.Tactics.V2
 open FStar.List.Tot
 
+let allow_invert (#a:Type) (x:a) : Lemma (inversion a) = allow_inversion a
+
 type constant = R.vconst
 
 let var = nat
@@ -37,7 +39,7 @@ let range_singleton (r:FStar.Range.range)
   = FStar.Sealed.sealed_singl r FStar.Range.range_0
 
 noeq
-type ppname = {
+type ppname0 = {
   name : RT.pp_name_t;
   range : range
 }
@@ -48,6 +50,13 @@ let ppname_default =  {
     range = FStar.Range.range_0
 }
 
+let ppname_singleton_trigger (r:ppname0) = True
+let ppname_singleton (x:ppname0)
+  : Lemma 
+    (ensures x == ppname_default)
+    [SMTPat (ppname_singleton_trigger x)]
+  = FStar.Sealed.sealed_singl x.name ppname_default.name
+let ppname = p:ppname0 { ppname_singleton_trigger p }
 let mk_ppname (name:RT.pp_name_t) (range:FStar.Range.range) : ppname = {
     name = name;
     range = range
@@ -116,7 +125,9 @@ type comp =
 val range_of_st_comp (st:st_comp) : R.range
 val range_of_comp (c:comp) : R.range
 
-let comp_st = c:comp {not (C_Tot? c) }
+
+let stateful_comp (c:comp) = not (C_Tot? c)
+let comp_st = c:comp { stateful_comp c }
 
 noeq
 type pattern =
@@ -403,22 +414,19 @@ let comp_res (c:comp) : term =
   | C_STAtomic _ _ s
   | C_STGhost _ s -> s.res
 
-let stateful_comp (c:comp) =
-  C_ST? c || C_STAtomic? c || C_STGhost? c
-
-let st_comp_of_comp (c:comp{stateful_comp c}) : st_comp =
+let st_comp_of_comp (c:comp_st) : st_comp =
   match c with
   | C_ST s
   | C_STAtomic _ _ s
   | C_STGhost _ s -> s
 
-let with_st_comp (c:comp{stateful_comp c}) (s:st_comp) : comp =
+let with_st_comp (c:comp_st) (s:st_comp) : comp =
   match c with
   | C_ST _ -> C_ST s
   | C_STAtomic inames obs _ -> C_STAtomic inames obs s
   | C_STGhost inames _ -> C_STGhost inames s
 
-let comp_u (c:comp { stateful_comp c }) = (st_comp_of_comp c).u
+let comp_u (c:comp_st) = (st_comp_of_comp c).u
 
 let universe_of_comp (c:comp_st) =
   match c with
@@ -442,3 +450,4 @@ let ppname_for_uvar (p : ppname) : T.Tac ppname =
   {
     p with name = T.seal ("?" ^ T.unseal p.name);
   }
+
diff --git a/src/checker/Pulse.Typing.Combinators.fst b/src/checker/Pulse.Typing.Combinators.fst
index 7a432c7b6..fe1b5c265 100644
--- a/src/checker/Pulse.Typing.Combinators.fst
+++ b/src/checker/Pulse.Typing.Combinators.fst
@@ -197,7 +197,7 @@ let bind_t (case_c1 case_c2:comp_st -> bool) =
               open_term (comp_post c1) x == comp_pre c2 /\
               (~ (x `Set.mem` freevars (comp_post c2)))))
            (ensures fun _ -> True)
-
+#push-options "--fuel 0 --ifuel 0"
 let mk_bind_st_st
   : bind_t C_ST? C_ST?
   = fun g pre e1 e2 c1 c2 px d_e1 d_c1res d_e2 res_typing post_typing _ ->
@@ -205,7 +205,7 @@ let mk_bind_st_st
       let b = nvar_as_binder px (comp_res c1) in
       let bc = Bind_comp g x c1 c2 res_typing x post_typing in
       (| _, _, T_Bind _ e1 e2 _ _ b _ _ d_e1 d_c1res d_e2 bc |)
-
+#pop-options
 let inames_of (c:comp_st) : term =
   match c with
   | C_ST _ -> tm_emp_inames
@@ -264,7 +264,8 @@ let lift_ghost_atomic (#g:env) (#e:st_term) (#c:comp_st { C_STGhost? c }) (d:st_
   | Some d ->
     d
 
-#push-options "--z3rlimit_factor 8 --ifuel 1 --fuel 2"
+#push-options "--z3rlimit_factor 2 --ifuel 0 --fuel 0 --query_stats --split_queries no"
+#restart-solver
 let mk_bind_ghost_ghost : bind_t C_STGhost? C_STGhost? =
   fun g pre e1 e2 c1 c2 px d_e1 d_c1res d_e2 res_typing post_typing post_hint ->
   let _, x = px in
@@ -335,7 +336,7 @@ let mk_bind_atomic_atomic
       )
 #pop-options
 
-#push-options "--z3rlimit_factor 20 --fuel 0 --ifuel 1 --z3cliopt 'smt.qi.eager_threshold=100'"
+#push-options "--z3rlimit_factor 20 --fuel 0 --ifuel 0 --z3cliopt 'smt.qi.eager_threshold=100'"
 #restart-solver
 let rec mk_bind (g:env) 
                 (pre:term)
@@ -454,6 +455,7 @@ let rec mk_bind (g:env)
       let (| t, c, d |) = mk_bind g pre e1 e2 _ _ px d_e1 d_c1res d_e2 res_typing post_typing post_hint in
       (| t, c, d |)
     )
+  | _ -> T.fail "Impossible: unexpected combination of effects"
 #pop-options
 
 let bind_res_and_post_typing g c2 x post_hint 
@@ -488,6 +490,7 @@ let add_frame (#g:env) (#t:st_term) (#c:comp_st) (t_typing:st_typing g t c)
 
   (| t, add_frame c frame, T_Frame _ _ _ _ frame_typing t_typing |)
 
+#push-options "--fuel 0 --ifuel 0"
 let apply_frame (#g:env)
                 (#t:st_term)
                 (#ctxt:term)
@@ -519,6 +522,7 @@ let apply_frame (#g:env)
     let t_typing = t_equiv t_typing st_equiv in
     (| c'', t_typing |)
 
+#push-options "--query_stats --z3rlimit_factor 2"
 let comp_for_post_hint #g (#pre:slprop) (pre_typing:tot_typing g pre tm_slprop)
   (post:post_hint_t { g `env_extends` post.g })
   (x:var { lookup g x == None })
@@ -549,3 +553,5 @@ let comp_for_post_hint #g (#pre:slprop) (pre_typing:tot_typing g pre tm_slprop)
     assert (g `env_extends` post.g);
     let d_opens : tot_typing g opens tm_inames = RU.magic () in  // weakening
     (| _, CT_STAtomic _ opens Neutral _ d_opens d_s |)
+  | _ -> T.fail "Impossible"
+#pop-options
\ No newline at end of file
diff --git a/src/checker/Pulse.Typing.FV.fst b/src/checker/Pulse.Typing.FV.fst
index 3fafd0d0b..9d5d150f1 100644
--- a/src/checker/Pulse.Typing.FV.fst
+++ b/src/checker/Pulse.Typing.FV.fst
@@ -539,7 +539,8 @@ fun d cb ->
       x 0;
     freevars_open_term post e 0
 #pop-options
-
+#restart-solver
+#push-options "--z3rlimit_factor 4 --fuel 1 --ifuel 1 --split_queries always"
 let st_typing_freevars_bind : st_typing_freevars_case T_Bind? =
 fun d cb ->
   match d with
@@ -578,8 +579,9 @@ fun #g #t #c d cb ->
       vars_of_env g;
     };
     comp_typing_freevars ct
-
-#push-options "--z3rlimit 40"
+#pop-options
+#restart-solver
+#push-options "--z3rlimit_factor 8"
 let st_typing_freevars_frame : st_typing_freevars_case T_Frame? =
 fun d cb ->
   match d with
@@ -588,6 +590,8 @@ fun d cb ->
     cb dc
 #pop-options
 
+#restart-solver
+#push-options "--z3rlimit_factor 4 --fuel 2 --ifuel 1 --query_stats"
 let st_typing_freevars_elimexists : st_typing_freevars_case T_ElimExists? =
 fun #g #t #c d cb ->
   match d with
diff --git a/src/checker/Pulse.Typing.LN.fst b/src/checker/Pulse.Typing.LN.fst
index a8217219b..0e3fccd7e 100644
--- a/src/checker/Pulse.Typing.LN.fst
+++ b/src/checker/Pulse.Typing.LN.fst
@@ -50,13 +50,15 @@ let open_term_ln' (e:term)
     (decreases e)
   = open_term_ln_host' e x i
 
+#push-options "--fuel 2 --ifuel 1 --z3rlimit_factor 4"
 let open_comp_ln' (c:comp)
                   (x:term)
                   (i:index)
   : Lemma 
     (requires ln_c' (open_comp' c x i) (i - 1))
     (ensures ln_c' c i)
-  = match c with
+  = allow_invert c;
+    match c with
     | C_Tot t ->
       open_term_ln' t x i
     | C_ST s ->
@@ -138,9 +140,11 @@ let open_pattern_args' (ps:list (pattern & bool)) (v:term) (i:index) =
 let close_pattern_args' (ps:list (pattern & bool)) (x:var) (i:index) =
   subst_pat_args ps [RT.ND x i]
 
+#push-options "--ifuel 2"
 let rec pattern_shift_subst_invariant (p:pattern) (s:subst)
   : Lemma
     (ensures pattern_shift_n p == pattern_shift_n (subst_pat p s))
+    (decreases p)
     [SMTPat (pattern_shift_n (subst_pat p s))]
   = match p with
     | Pat_Cons _ subpats -> admit()
@@ -148,7 +152,9 @@ let rec pattern_shift_subst_invariant (p:pattern) (s:subst)
 and pattern_args_shift_subst_invariant (ps:list (pattern & bool)) (s:subst)
   : Lemma
     (ensures pattern_args_shift_n ps == pattern_args_shift_n (subst_pat_args ps s))
-  = match ps with
+    (decreases ps)
+  = allow_invert ps;
+    match ps with
     | [] -> ()
     | (hd, _)::tl ->
       pattern_shift_subst_invariant hd s;
@@ -832,7 +838,7 @@ let close_proof_hint_ln (ht:proof_hint_type) (v:var) (i:index)
     | WILD
     | SHOW_PROOF_STATE _ -> ()
 
-#push-options "--fuel 2 --ifuel 2 --z3rlimit_factor 8 --split_queries no"
+#push-options "--fuel 2 --ifuel 2 --z3rlimit_factor 10 --split_queries no"
 let rec close_st_term_ln' (t:st_term) (x:var) (i:index)
   : Lemma
     (requires ln_st' t (i - 1))
@@ -981,7 +987,7 @@ let tot_typing_ln
   : Lemma 
     (ensures ln e /\ ln t)
   = tot_or_ghost_typing_ln d
-
+#push-options "--fuel 4 --ifuel 4"
 let rec slprop_equiv_ln (#g:_) (#t0 #t1:_) (v:slprop_equiv g t0 t1)
   : Lemma (ensures ln t0 <==> ln t1)
           (decreases v)
@@ -1017,7 +1023,7 @@ let rec slprop_equiv_ln (#g:_) (#t0 #t1:_) (v:slprop_equiv g t0 t1)
         open_term_ln t1' x;
         open_term_ln t0' x
       )
-      
+#pop-options      
 
 let st_equiv_ln #g #c1 #c2 (d:st_equiv g c1 c2)
   : Lemma 
@@ -1120,6 +1126,7 @@ let par_post_ln (uL uR aL aR postL postR x : _)
 =
   admit ()
 
+#push-options "--fuel 4 --ifuel 4"
 let comp_par_ln (cL : comp{C_ST? cL}) (cR : comp{C_ST? cR}) (x : var)
   : Lemma
       (requires ln_c cL /\ ln_c cR)
@@ -1136,7 +1143,9 @@ let comp_par_ln (cL : comp{C_ST? cL}) (cR : comp{C_ST? cR}) (x : var)
   assert (ln' post 0);
   assert (ln_c (comp_par cL cR x));
   ()
+#pop-options
 
+#push-options "--fuel 1 --ifuel 1 --z3rlimit_factor 10 --split_queries no --z3cliopt 'smt.qi.eager_threshold=100'"
 let st_typing_ln_par
   (#g:_) (#t:_) (#c:_)
   (d:st_typing g t c{T_Par? d})
diff --git a/src/checker/PulseChecker.fst.config.json b/src/checker/PulseChecker.fst.config.json
index 73361eac7..529368fbc 100644
--- a/src/checker/PulseChecker.fst.config.json
+++ b/src/checker/PulseChecker.fst.config.json
@@ -3,7 +3,13 @@
   "options": [
     "--query_cache",
     "--ext",
-    "optimize_let_vc"
+    "optimize_let_vc",
+    "--z3version",
+    "4.13.3",
+    "--smtencoding.elim_box",
+    "true",
+    "--z3smtopt",
+    "(set-option :smt.arith.nl false)"
   ],
   "include_dirs": [
     "--include", "../../build/checker.checked"