diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index 0408db351..37457ba98 100644 --- a/src/bin/common/solving_loop.ml +++ b/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 diff --git a/src/lib/frontend/d_state_option.ml b/src/lib/frontend/d_state_option.ml index 0b454cd95..5fdf04332 100644 --- a/src/lib/frontend/d_state_option.ml +++ b/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 = [ diff --git a/src/lib/frontend/d_state_option.mli b/src/lib/frontend/d_state_option.mli index 56ec3d432..70472f77a 100644 --- a/src/lib/frontend/d_state_option.mli +++ b/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