diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml
index b78a5504583..0b093080d64 100644
--- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml
+++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml
@@ -1994,7 +1994,7 @@ type env_t = env
 type sigtable = FStar_Syntax_Syntax.sigelt FStar_Compiler_Util.smap
 let (should_verify : env -> Prims.bool) =
   fun env1 ->
-    ((Prims.op_Negation env1.lax) && (Prims.op_Negation env1.admit)) &&
+    (Prims.op_Negation env1.admit) &&
       (let uu___ = FStar_Ident.string_of_lid env1.curmodule in
        FStar_Options.should_verify uu___)
 let (visible_at : delta_level -> FStar_Syntax_Syntax.qualifier -> Prims.bool)
diff --git a/src/typechecker/FStar.TypeChecker.Env.fst b/src/typechecker/FStar.TypeChecker.Env.fst
index c430eca96f0..8cb7d415e5e 100644
--- a/src/typechecker/FStar.TypeChecker.Env.fst
+++ b/src/typechecker/FStar.TypeChecker.Env.fst
@@ -176,8 +176,7 @@ let missing_definition_list (e:env) : list lident =
 type sigtable = BU.smap sigelt
 
 let should_verify env =
-    not env.lax
-    && not env.admit
+    not env.admit
     && Options.should_verify (string_of_lid env.curmodule)
 
 let visible_at d q = match d, q with