diff --git a/src/smtencoding/FStarC.SMTEncoding.EncodeTerm.fsti b/src/smtencoding/FStarC.SMTEncoding.EncodeTerm.fsti
index 1dfe9db8dd9..407d9ba724b 100644
--- a/src/smtencoding/FStarC.SMTEncoding.EncodeTerm.fsti
+++ b/src/smtencoding/FStarC.SMTEncoding.EncodeTerm.fsti
@@ -18,7 +18,7 @@ module FStarC.SMTEncoding.EncodeTerm
 open Prims
 open FStar.Pervasives
 open FStarC.Effect
-open FStar open FStarC
+open FStar
 open FStarC
 open FStarC.TypeChecker.Env
 open FStarC.Syntax
@@ -30,7 +30,7 @@ open FStarC.Const
 open FStarC.SMTEncoding
 open FStarC.SMTEncoding.Util
 open FStarC.SMTEncoding.Env
-module BU = FStarC.Compiler.Util
+
 val isTotFun_axioms: Range.range -> head:term -> extra_vars:fvs -> vars:fvs -> guards:list term -> bool -> term
 val mk_Apply : e:term -> vars:fvs -> term
 val maybe_curry_app : rng:Range.range -> head:either op term -> arity:int -> args:list term -> term
diff --git a/ulib/experimental/FStar.InteractiveHelpers.PostProcess.fst b/ulib/experimental/FStar.InteractiveHelpers.PostProcess.fst
index cf8f9122c77..7c9873bd9e2 100644
--- a/ulib/experimental/FStar.InteractiveHelpers.PostProcess.fst
+++ b/ulib/experimental/FStar.InteractiveHelpers.PostProcess.fst
@@ -597,6 +597,8 @@ let rec strip_implicit_parameters tm =
   | _ -> tm
 
 val unfold_in_assert_or_assume : bool -> exploration_result term -> Tac unit
+#push-options "--z3rlimit_factor 2 --fuel 0"
+#restart-solver
 let unfold_in_assert_or_assume dbg ares =
   print_dbg dbg ("[> unfold_in_assert_or_assume:\n" ^ term_to_string ares.res);
   (* Find the focused term inside the assert, and on which side of the
@@ -733,6 +735,7 @@ let unfold_in_assert_or_assume dbg ares =
   let ge3, asserts = subst_shadowed_with_abs_in_assertions dbg ge2 None asserts in
   (* Output *)
   printout_success ge3 asserts
+#pop-options
 
 [@plugin]
 val pp_unfold_in_assert_or_assume : bool -> unit -> Tac unit