diff --git a/ocaml/fstar-lib/generated/FStar_SMTEncoding_Solver.ml b/ocaml/fstar-lib/generated/FStar_SMTEncoding_Solver.ml
index 578ce8827e0..f239e41e4eb 100644
--- a/ocaml/fstar-lib/generated/FStar_SMTEncoding_Solver.ml
+++ b/ocaml/fstar-lib/generated/FStar_SMTEncoding_Solver.ml
@@ -2092,22 +2092,28 @@ let (do_solve_maybe_split :
   fun use_env_msg ->
     fun tcenv ->
       fun q ->
-        let uu___ = FStar_Options.split_queries () in
-        match uu___ with
-        | FStar_Options.No -> do_solve false false use_env_msg tcenv q
-        | FStar_Options.OnFailure ->
-            let can_split =
-              let uu___1 =
-                let uu___2 = FStar_Options.quake_hi () in
-                uu___2 > Prims.int_one in
-              Prims.op_Negation uu___1 in
-            (try
-               (fun uu___1 ->
-                  match () with
-                  | () -> do_solve can_split false use_env_msg tcenv q) ()
-             with
-             | SplitQueryAndRetry -> split_and_solve true use_env_msg tcenv q)
-        | FStar_Options.Always -> split_and_solve false use_env_msg tcenv q
+        let uu___ = FStar_Options.admit_smt_queries () in
+        if uu___
+        then ()
+        else
+          (let uu___2 = FStar_Options.split_queries () in
+           match uu___2 with
+           | FStar_Options.No -> do_solve false false use_env_msg tcenv q
+           | FStar_Options.OnFailure ->
+               let can_split =
+                 let uu___3 =
+                   let uu___4 = FStar_Options.quake_hi () in
+                   uu___4 > Prims.int_one in
+                 Prims.op_Negation uu___3 in
+               (try
+                  (fun uu___3 ->
+                     match () with
+                     | () -> do_solve can_split false use_env_msg tcenv q) ()
+                with
+                | SplitQueryAndRetry ->
+                    split_and_solve true use_env_msg tcenv q)
+           | FStar_Options.Always ->
+               split_and_solve false use_env_msg tcenv q)
 let (solve :
   (unit -> Prims.string) FStar_Pervasives_Native.option ->
     FStar_TypeChecker_Env.env -> FStar_Syntax_Syntax.term -> unit)
diff --git a/src/smtencoding/FStar.SMTEncoding.Solver.fst b/src/smtencoding/FStar.SMTEncoding.Solver.fst
index 503759dab04..8b4cb4aad94 100644
--- a/src/smtencoding/FStar.SMTEncoding.Solver.fst
+++ b/src/smtencoding/FStar.SMTEncoding.Solver.fst
@@ -1220,6 +1220,9 @@ let disable_quake_for (f : unit -> 'a) : 'a =
 (* Split queries if needed according to --split_queries option. Note:
 sync SMT queries do not pass via this function. *)
 let do_solve_maybe_split use_env_msg tcenv q : unit =
+  (* If we are admiting queries, don't do anything, and bail out
+  right now to save time/memory *)
+  if Options.admit_smt_queries () then () else begin
     match Options.split_queries () with
     | Options.No -> do_solve false false use_env_msg tcenv q
     | Options.OnFailure ->
@@ -1234,7 +1237,7 @@ let do_solve_maybe_split use_env_msg tcenv q : unit =
     | Options.Always ->
       (* Set retrying=false so queries go through the full config list, etc. *)
       split_and_solve false use_env_msg tcenv q
-
+  end
 (* Attempt to discharge a VC through the SMT solver. Will
 automatically retry increasing fuel as needed, and perform quake testing
 (repeating the query to make sure it is robust). This function will