diff --git a/tools/booster/Proxy.hs b/tools/booster/Proxy.hs
index f20877861..8d834c954 100644
--- a/tools/booster/Proxy.hs
+++ b/tools/booster/Proxy.hs
@@ -62,10 +62,11 @@ respondEither ::
     Log.MonadLogger m =>
     MonadIO m =>
     Maybe StatsVar ->
+    Depth ->
     Respond (API 'Req) m (API 'Res) ->
     Respond (API 'Req) m (API 'Res) ->
     Respond (API 'Req) m (API 'Res)
-respondEither mbStatsVar booster kore req = case req of
+respondEither mbStatsVar koreFallbackDepth booster kore req = case req of
     Execute execReq
         | isJust execReq.stepTimeout || isJust execReq.movingAverageStepTimeout ->
             loggedKore ExecuteM req
@@ -215,7 +216,7 @@ respondEither mbStatsVar booster kore req = case req of
                                         ( Execute
                                             r
                                                 { state = execStateToKoreJson simplifiedBoosterState
-                                                , maxDepth = Just $ Depth 1
+                                                , maxDepth = Just koreFallbackDepth
                                                 }
                                         )
                             when (isJust mbStatsVar) $
diff --git a/tools/booster/Server.hs b/tools/booster/Server.hs
index 81557fe09..ea4ff64d6 100644
--- a/tools/booster/Server.hs
+++ b/tools/booster/Server.hs
@@ -50,7 +50,7 @@ import Kore.JsonRpc (ServerState (..))
 import Kore.JsonRpc qualified as Kore
 import Kore.JsonRpc.Error
 import Kore.JsonRpc.Server
-import Kore.JsonRpc.Types (API, ReqOrRes (Req, Res))
+import Kore.JsonRpc.Types (API, Depth (..), ReqOrRes (Req, Res))
 import Kore.Log (
     ExeName (..),
     KoreLogType (LogSomeAction),
@@ -62,6 +62,7 @@ import Kore.Log (
  )
 import Kore.Log qualified as Log
 import Kore.Log.DebugSolver qualified as Log
+import Kore.Parser.ParserUtils (readPositiveIntegral)
 import Kore.Rewrite.SMT.Lemma (declareSMTLemmas)
 import Kore.Syntax.Definition (ModuleName (ModuleName), SentenceAxiom)
 import Options.SMT (KoreSolverOptions (..), parseKoreSolverOptions)
@@ -85,7 +86,7 @@ main = do
                     , eventlogEnabledUserEvents
                     }
             , koreSolverOptions
-            , proxyOptions = ProxyOptions{printStats}
+            , proxyOptions = ProxyOptions{printStats, koreFallbackDepth}
             , debugSolverOptions
             } = options
         (logLevel, customLevels) = adjustLogLevels logLevels
@@ -142,7 +143,7 @@ main = do
                         server =
                             jsonRpcServer
                                 srvSettings
-                                (const $ Proxy.respondEither statVar boosterRespond koreRespond)
+                                (const $ Proxy.respondEither statVar koreFallbackDepth boosterRespond koreRespond)
                                 [handleErrorCall, handleSomeException]
                         interruptHandler _ = do
                             when (logLevel >= LevelInfo) $
@@ -177,9 +178,11 @@ data CLProxyOptions = CLProxyOptions
     , debugSolverOptions :: !Log.DebugSolverOptions
     }
 
-newtype ProxyOptions = ProxyOptions
+data ProxyOptions = ProxyOptions
     { printStats :: Bool
     -- ^ print timing statistics per request and on shutdown
+    , koreFallbackDepth :: Depth
+    -- ^ maximum number of rewriting steps to be preformed when falling back to Kore
     }
 
 parserInfoModifiers :: InfoMod options
@@ -201,6 +204,23 @@ clProxyOptionsParser =
                 ( long "print-stats"
                     <> help "(development) Print timing information per request and on shutdown"
                 )
+            <*> option
+                readKoreFallpackLimit
+                ( long "kore-fallback-depth"
+                    <> help "Maximum number of rewriting steps to be preformed when falling back to Kore"
+                    <> value defaultKoreFallpackLimit
+                )
+      where
+        readKoreFallpackLimit = readPositiveIntegral Depth "kore-fallback-depth"
+        defaultKoreFallpackLimit = 1
+
+-- option
+--     readRetryLimit
+--     ( metavar "SMT_RETRY_LIMIT"
+--         <> long "smt-retry-limit"
+--         <> help "Limit how many times an SMT query can be retried (with scaling timeouts)"
+--         <> value defaultRetryLimit
+--     )
 
 mkKoreServer :: Log.LoggerEnv IO -> CLOptions -> KoreSolverOptions -> IO KoreServer
 mkKoreServer loggerEnv@Log.LoggerEnv{logAction} CLOptions{definitionFile, mainModuleName} koreSolverOptions =