diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml
index aff531aaf5e..fb96e3ac480 100644
--- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml
+++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml
@@ -4067,7 +4067,9 @@ let (simplify_guard :
                 FStar_TypeChecker_Env.Eager_unfolding;
                 FStar_TypeChecker_Env.Simplify;
                 FStar_TypeChecker_Env.Primops;
-                FStar_TypeChecker_Env.NoFullNorm] env f in
+                FStar_TypeChecker_Env.NoFullNorm;
+                FStar_TypeChecker_Env.Exclude FStar_TypeChecker_Env.Zeta] env
+                f in
             (let uu___2 =
                FStar_Compiler_Effect.op_Less_Bar
                  (FStar_TypeChecker_Env.debug env)
@@ -13646,7 +13648,9 @@ let (discharge_guard' :
                            FStar_TypeChecker_Normalize.normalize
                              [FStar_TypeChecker_Env.Eager_unfolding;
                              FStar_TypeChecker_Env.Simplify;
-                             FStar_TypeChecker_Env.Primops] env vc) uu___4
+                             FStar_TypeChecker_Env.Primops;
+                             FStar_TypeChecker_Env.Exclude
+                               FStar_TypeChecker_Env.Zeta] env vc) uu___4
                         "FStar.TypeChecker.Rel.vc_normalization" in
                     if debug1
                     then
@@ -13728,7 +13732,9 @@ let (discharge_guard' :
                                                      norm_with_steps
                                                        "FStar.TypeChecker.Rel.norm_with_steps.7"
                                                        [FStar_TypeChecker_Env.Simplify;
-                                                       FStar_TypeChecker_Env.Primops]
+                                                       FStar_TypeChecker_Env.Primops;
+                                                       FStar_TypeChecker_Env.Exclude
+                                                         FStar_TypeChecker_Env.Zeta]
                                                        env1 goal in
                                                    (env1, uu___15, opts))
                                             vcs1 in
diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_TcTerm.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_TcTerm.ml
index 2fdef39eedd..159464fbbd1 100644
--- a/ocaml/fstar-lib/generated/FStar_TypeChecker_TcTerm.ml
+++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_TcTerm.ml
@@ -172,7 +172,8 @@ let steps : 'uuuuu . 'uuuuu -> FStar_TypeChecker_Env.step Prims.list =
   fun env ->
     [FStar_TypeChecker_Env.Beta;
     FStar_TypeChecker_Env.Eager_unfolding;
-    FStar_TypeChecker_Env.NoFullNorm]
+    FStar_TypeChecker_Env.NoFullNorm;
+    FStar_TypeChecker_Env.Exclude FStar_TypeChecker_Env.Zeta]
 let (norm :
   FStar_TypeChecker_Env.env ->
     FStar_Syntax_Syntax.term -> FStar_Syntax_Syntax.term)
diff --git a/src/typechecker/FStar.TypeChecker.Rel.fst b/src/typechecker/FStar.TypeChecker.Rel.fst
index bbab71fce5b..16f6d9e875d 100644
--- a/src/typechecker/FStar.TypeChecker.Rel.fst
+++ b/src/typechecker/FStar.TypeChecker.Rel.fst
@@ -1836,7 +1836,7 @@ let simplify_guard env g = match g.guard_f with
     | NonTrivial f ->
       if Env.debug env <| Options.Other "Simplification" then BU.print1 "Simplifying guard %s\n" (Print.term_to_string f);
       let f = norm_with_steps "FStar.TypeChecker.Rel.norm_with_steps.6"
-              [Env.Beta; Env.Eager_unfolding; Env.Simplify; Env.Primops; Env.NoFullNorm] env f in
+              [Env.Beta; Env.Eager_unfolding; Env.Simplify; Env.Primops; Env.NoFullNorm; Env.Exclude Env.Zeta] env f in
       if Env.debug env <| Options.Other "Simplification" then BU.print1 "Simplified guard to %s\n" (Print.term_to_string f);
       let f =
         let g = U.unmeta f in
@@ -4944,7 +4944,7 @@ let discharge_guard' use_env_range_msg env (g:guard_t) (use_smt:bool) : option g
                        (BU.format1 "Before normalization VC=\n%s\n" (Print.term_to_string vc));
       let vc =
         Profiling.profile
-          (fun () -> N.normalize [Env.Eager_unfolding; Env.Simplify; Env.Primops] env vc)
+          (fun () -> N.normalize [Env.Eager_unfolding; Env.Simplify; Env.Primops; Env.Exclude Env.Zeta] env vc)
           (Some (Ident.string_of_lid (Env.current_module env)))
           "FStar.TypeChecker.Rel.vc_normalization"
       in
@@ -4974,7 +4974,7 @@ let discharge_guard' use_env_range_msg env (g:guard_t) (use_smt:bool) : option g
                         if Options.profile_enabled None "FStar.TypeChecker"
                         then BU.print1 "Tactic preprocessing produced %s goals\n" (BU.string_of_int (List.length vcs));
                         let vcs = List.map (fun (env, goal, opts) ->
-                        env, norm_with_steps "FStar.TypeChecker.Rel.norm_with_steps.7" [Env.Simplify; Env.Primops] env goal, opts) vcs in
+                        env, norm_with_steps "FStar.TypeChecker.Rel.norm_with_steps.7" [Env.Simplify; Env.Primops; Env.Exclude Env.Zeta] env goal, opts) vcs in
                         let vcs = List.map (fun (env, goal, opts) ->
                           env.solver.handle_smt_goal env goal |>
                             (* Keep the same SMT options if the goals were transformed *)
diff --git a/src/typechecker/FStar.TypeChecker.TcTerm.fst b/src/typechecker/FStar.TypeChecker.TcTerm.fst
index e43eb0639fb..b7ce9633c3d 100644
--- a/src/typechecker/FStar.TypeChecker.TcTerm.fst
+++ b/src/typechecker/FStar.TypeChecker.TcTerm.fst
@@ -53,7 +53,7 @@ let no_inst env = {env with Env.instantiate_imp=false}
 let is_eq = function
     | Some Equality -> true
     | _ -> false
-let steps env = [Env.Beta; Env.Eager_unfolding; Env.NoFullNorm]
+let steps env = [Env.Beta; Env.Eager_unfolding; Env.NoFullNorm; Env.Exclude Env.Zeta]
 let norm   env t = N.normalize (steps env) env t
 let norm_c env c = N.normalize_comp (steps env) env c
 let check_no_escape head_opt env (fvs:list bv) kt : term * guard_t =