Poetry

src/bin/common/solving_loop.ml

@@ -480,7 +480,6 @@ let main () =
     State.empty
     |> State.set solver_ctx_key solver_ctx
     |> State.set partial_model_key partial_model
-    |> set_steps_bound (O.get_steps_bound ())
     |> State.set named_terms Util.MS.empty
     |> DO.init
     |> State.init ~debug ~report_style ~reports ~max_warn ~time_limit

src/lib/frontend/d_state_option.ml

@@ -99,11 +99,11 @@ let msatsolver =
 
 module SatSolver = (val msatsolver)
 
-let mstate =
+let msteps =
   let on_update _ sat st = Steps.set_steps_bound sat; st in
   (create_opt ~on_update "steps_bound" O.get_steps_bound)
 
-module Steps = (val mstate)
+module Steps = (val msteps)
 
 (* Some options can be initialized to gain some performance. *)
 let options_requiring_initialization = [

src/lib/frontend/d_state_option.mli

@@ -64,7 +64,8 @@ module SatSolver : S with type t = Util.sat_solver
     on SatSolver: when SatSolver is updated, this one also is. *)
 module SatSolverModule : Accessor with type t = (module Sat_solver_sig.S)
 
-(** Option for setting the max number of steps. Interfaces with Steps.
+(** Option for setting the max number of steps. Interfaces with the toplevel
+    Steps module.
     The [set] function may raise Invalid_arg from the Steps.set_steps_bound call
     if the new option value is lower than the current number of steps. *)
 module Steps : S with type t = int