From 96e463f296f872ba07a3a3e969672883479cbc1f Mon Sep 17 00:00:00 2001
From: Steven de Oliveira <de.oliveira.steven@gmail.com>
Date: Mon, 23 Oct 2023 12:21:47 +0200
Subject: [PATCH] Activating options where they should

---
 src/bin/common/solving_loop.ml | 26 ++++++++++++--------------
 1 file changed, 12 insertions(+), 14 deletions(-)

diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml
index 78b84a0b9..1dba8541a 100644
--- a/src/bin/common/solving_loop.ml
+++ b/src/bin/common/solving_loop.ml
@@ -89,6 +89,12 @@ let unsupported_opt opt =
   in
   warning "unsupported option %s" opt
 
+let enable_maxsmt b =
+  if b then
+    DStd.Extensions.Smtlib2.(enable maxsmt)
+  else
+    DStd.Extensions.Smtlib2.(disable maxsmt)
+
 (* We currently use the full state of the solver as model. *)
 type model = Model : 'a sat_module * 'a -> model
 
@@ -103,7 +109,7 @@ let main () =
       (val
         (if Options.get_no_theory() then (module Theory.Main_Empty : Theory.S)
          else (module Theory.Main_Default : Theory.S)) : Theory.S ) in
-    Options.get_sat_solver (),
+    O.get_sat_solver (),
     (module SatCont.Make(TH) : Sat_solver_sig.S)
   in
 
@@ -402,7 +408,6 @@ let main () =
     |> State.set sat_solver_key (make_sat ())
     |> State.set solver_ctx_key solver_ctx
     |> State.set partial_model_key partial_model
-    |> State.set Typer.additional_builtins D_cnf.builtins
     |> State.set optimize_key (O.get_optimize ())
     |> State.init ~debug ~report_style ~reports ~max_warn ~time_limit
       ~size_limit ~response_file
@@ -428,7 +433,8 @@ let main () =
       st
     | Tableaux | Tableaux_CDCL | CDCL | CDCL_Tableaux ->
       O.set_sat_solver sat;
-      (* `make_sat` returns the sat solver corresponding to the new sat_solver option. *)
+      (* `make_sat` returns the sat solver corresponding to the new sat_solver
+         option. *)
       State.set
         sat_solver_key
         (make_sat ())
@@ -436,12 +442,6 @@ let main () =
   in
 
   let set_optimize optim st =
-    let () =
-      if optim then
-        DStd.Extensions.Smtlib2.(enable maxsmt)
-      else
-        DStd.Extensions.Smtlib2.(disable maxsmt)
-    in
     let sat, _ = State.get sat_solver_key st in
     match sat with
     | Util.Tableaux | Tableaux_CDCL when optim ->
@@ -451,7 +451,7 @@ let main () =
         sat;
       st
     | Tableaux | Tableaux_CDCL | CDCL | CDCL_Tableaux ->
-      O.set_optimize optim;
+      enable_maxsmt optim;
       State.set optimize_key optim st
   in
 
@@ -800,10 +800,7 @@ let main () =
     let logic_file, st = mk_state filename in
     let () =
       (* Activating maxsmt if the optimize option is ON. *)
-      if O.get_optimize () then
-        DStd.Extensions.Smtlib2.(enable maxsmt)
-      else
-        DStd.Extensions.Smtlib2.(disable maxsmt)
+      enable_maxsmt (O.get_optimize ())
     in
     try
       Options.with_timelimit_if (not (Options.get_timelimit_per_goal ()))
@@ -826,6 +823,7 @@ let main () =
       let g =
         Parser.parse_logic ~preludes logic_file
       in
+      let st = State.set Typer.additional_builtins D_cnf.builtins st in
       let all_used_context = Frontend.init_all_used_context () in
       let finally = finally ~handle_exn in
       let st =