diff --git a/colibri2/solver/scheduler.ml b/colibri2/solver/scheduler.ml index fa881cd4a1748d9cb434c03c7b87c1d964d3d4e9..222107b599489d08763201af36c204e0f9e96a17 100644 --- a/colibri2/solver/scheduler.ml +++ b/colibri2/solver/scheduler.ml @@ -52,6 +52,12 @@ let stats_con_fix = Debug.register_stats_int "Scheduler.conflict_fix_model" let stats_step = Debug.register_stats_int "Scheduler.step" let stats_fix_model = Debug.register_stats_int "Scheduler.fix_model" +let no_fixmodel_option = + Colibri2_core.Options.register ~pp:Fmt.bool "Scheduler.fixmodel" + Cmdliner.Arg.( + value & flag + & info [ "no-fix-model" ] ~doc:"Stop at the start of FixModel") + exception Contradiction exception ReachStepLimit @@ -657,7 +663,11 @@ let run_one_step ~nodec t = Context.Ref.set t.solve_step step; make_choice t choice choices; true) - | FixModel -> run_one_step_fix_model ~nodec t + | FixModel -> + let d = Backtrackable.get_delayed t.solver_state in + if Colibri2_core.Options.get d no_fixmodel_option then + raise ReachStepLimit; + run_one_step_fix_model ~nodec t let rec flush t = try Backtrackable.flush t.solver_state