diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml
index 40d46ea51..476630bcd 100644
--- a/src/bin/common/solving_loop.ml
+++ b/src/bin/common/solving_loop.ml
@@ -97,6 +97,13 @@ let enable_maxsmt b =
   else
     DStd.Extensions.Smtlib2.(disable maxsmt)
 
+let cmd_on_modes st modes cmd =
+  if O.get_input_format () = Some Options.Smtlib2 then begin
+    let curr_mode = DO.Mode.get st in
+    if not @@ (List.exists (Util.equal_mode curr_mode)) modes then
+      Errors.forbidden_command curr_mode cmd
+  end
+
 (* Dolmen util *)
 
 (** Adds the named terms of the statement [stmt] to the map accumulator [acc] *)
@@ -117,6 +124,11 @@ let add_if_named
 (* We currently use the full state of the solver as model. *)
 type model = Model : 'a sat_module * 'a -> model
 
+type solve_res =
+  | Sat of model
+  | Unknown of model option
+  | Unsat
+
 let main () =
   let () = Dolmen_loop.Code.init [] in
 
@@ -155,13 +167,21 @@ let main () =
         Profiling.print true
           (Steps.get_steps ())
           (Options.Output.get_fmt_diagnostic ());
+      let partial_model = ftdn_env.sat_env in
       (* If the status of the SAT environment is inconsistent,
          we have to drop the partial model in order to prevent
          printing wrong model. *)
       match ftdn_env.FE.res with
-      | `Sat | `Unknown ->
+      | `Sat ->
+        begin
+          let mdl = Model ((module SAT), partial_model) in
+          if Options.(get_interpretation () && get_dump_models ()) then begin
+            FE.print_model (Options.Output.get_fmt_models ()) partial_model
+          end;
+          Sat mdl
+        end
+      | `Unknown ->
         begin
-          let partial_model = ftdn_env.sat_env in
           let mdl = Model ((module SAT), partial_model) in
           if Options.(get_interpretation () && get_dump_models ()) then begin
             let ur = SAT.get_unknown_reason partial_model in
@@ -170,14 +190,14 @@ let main () =
               Sat_solver_sig.pp_ae_unknown_reason_opt ur;
             FE.print_model (Options.Output.get_fmt_models ()) partial_model
           end;
-          Some mdl
+          Unknown (Some mdl)
         end
-      | `Unsat -> None
+      | `Unsat -> Unsat
     with Util.Timeout ->
       (* It is still necessary to leave this catch here, because we may
          trigger this exception in between calls of the sat solver. *)
       if not (Options.get_timelimit_per_goal()) then exit_as_timeout ();
-      None
+      Unknown None
   in
 
   let typed_loop all_context state td =
@@ -384,6 +404,22 @@ let main () =
           "The output format %s is not supported by the Dolmen frontend."
           s
   in
+  let set_partial_model_and_mode solve_res st =
+    match solve_res with
+    | Unsat ->
+      st
+      |> DO.Mode.set Util.Unsat
+      |> State.set partial_model_key None
+    | Unknown None ->
+      st
+      |> DO.Mode.set Util.Sat
+      |> State.set partial_model_key None
+    | Unknown (Some m)
+    | Sat m ->
+      st
+      |> DO.Mode.set Util.Sat
+      |> State.set partial_model_key (Some m)
+  in
   (* The function In_channel.input_all is not available before OCaml 4.14. *)
   let read_all ch =
     let b = Buffer.create 113 in
@@ -398,8 +434,7 @@ let main () =
   let mk_state ?(debug = false) ?(report_style = State.Contextual)
       ?(max_warn = max_int) ?(time_limit = Float.infinity)
       ?(size_limit = Float.infinity) ?(type_check = true)
-      ?(solver_ctx = empty_solver_ctx)
-      ?(partial_model = None) path =
+      ?(solver_ctx = empty_solver_ctx) path =
     let reports =
       Dolmen_loop.Report.Conf.(
         let disable m t =
@@ -469,7 +504,7 @@ let main () =
     logic_file,
     State.empty
     |> State.set solver_ctx_key solver_ctx
-    |> State.set partial_model_key partial_model
+    |> State.set partial_model_key None
     |> State.set named_terms Util.MS.empty
     |> DO.init
     |> State.init ~debug ~report_style ~reports ~max_warn ~time_limit
@@ -658,10 +693,13 @@ let main () =
   let handle_custom_statement id args st =
     match id, args with
     | Dolmen.Std.Id.{name = Simple "minimize"; _}, [term] ->
+      cmd_on_modes st [Assert] "minimize";
       handle_minimize_term term st
     | Dolmen.Std.Id.{name = Simple "maximize"; _}, [term] ->
+      cmd_on_modes st [Assert] "maximize";
       handle_maximize_term term st
     | Dolmen.Std.Id.{name = Simple "get-objectives"; _}, args ->
+      cmd_on_modes st [Sat] "get-objectives";
       handle_get_objectives args st
     | Dolmen.Std.Id.{name = Simple (("minimize" | "maximize") as ext); _}, _ ->
       recoverable_error
@@ -721,6 +759,10 @@ let main () =
 
   (* Fetches the term value in the current model. *)
   let evaluate_term get_value name term =
+    (* There are two ways to evaluate a term:
+       - if its name is registered in the environment, get its value;
+       - if not, check if the formula is in the environment.
+    *)
     let simple_form =
       Expr.mk_term
         (Sy.name name)
@@ -764,9 +806,13 @@ let main () =
       let file_loc = (State.get State.logic_file st).loc in
       let solver_ctx = State.get solver_ctx_key st in
       match td with
+      | { contents = `Set_logic _; _} ->
+        cmd_on_modes st [Start] "set-logic";
+        DO.Mode.set Util.Assert st
       (* When the next statement is a goal, the solver is called and provided
          the goal and the current context *)
       | { id; contents = (`Solve _ as contents); loc ; attrs; implicit } ->
+        cmd_on_modes st [Assert; Sat; Unsat] "solve";
         let l =
           solver_ctx.local @
           solver_ctx.global @
@@ -806,7 +852,7 @@ let main () =
             List.rev (cnf :: hyps), is_thm
           | _ -> assert false
         in
-        let partial_model =
+        let solve_res =
           solve
             (DO.SatSolverModule.get st)
             all_context
@@ -818,13 +864,13 @@ let main () =
             let solver_ctx = State.get solver_ctx_key st in
             { solver_ctx with global = []; local = [] }
           ) st
-          |> State.set partial_model_key partial_model
+          |> set_partial_model_and_mode solve_res
         else
           State.set solver_ctx_key (
             let solver_ctx = State.get solver_ctx_key st in
             { solver_ctx with local = [] }
           ) st
-          |> State.set partial_model_key partial_model
+          |> set_partial_model_and_mode solve_res
 
       | {contents = `Set_option
              { DStd.Term.term =
@@ -840,6 +886,7 @@ let main () =
         st
 
       | {contents = `Get_model; _ } ->
+        cmd_on_modes st [Sat] "get-model";
         if Options.get_interpretation () then
           let () = match State.get partial_model_key st with
             | Some (Model ((module SAT), env)) ->
@@ -862,8 +909,10 @@ let main () =
         st
         |> State.set partial_model_key None
         |> State.set solver_ctx_key empty_solver_ctx
-        |> DO.Optimize.reset
-        |> DO.ProduceAssignment.reset
+        |> DO.Mode.clear
+        |> DO.Optimize.clear
+        |> DO.ProduceAssignment.clear
+        |> DO.init
         |> State.set named_terms Util.MS.empty
 
       | {contents = `Exit; _} -> raise Exit
@@ -882,6 +931,7 @@ let main () =
 
       | {contents = `Get_assignment; _} ->
         begin
+          cmd_on_modes st [Sat] "get-assignment";
           match State.get partial_model_key st with
           | Some Model ((module SAT), partial_model) ->
             if DO.ProduceAssignment.get st then
diff --git a/src/lib/frontend/d_state_option.ml b/src/lib/frontend/d_state_option.ml
index 5fdf04332..3c5d807c7 100644
--- a/src/lib/frontend/d_state_option.ml
+++ b/src/lib/frontend/d_state_option.ml
@@ -47,8 +47,8 @@ module type S = sig
   (** Sets the option on the dolmen state. *)
   val set : t -> D_loop.Typer.state -> D_loop.Typer.state
 
-  (** Resets the option to its default value in Options. *)
-  val reset : D_loop.Typer.state -> D_loop.Typer.state
+  (** Clears the option from the state. *)
+  val clear : D_loop.Typer.state -> D_loop.Typer.state
 end
 
 let create_opt
@@ -66,19 +66,43 @@ let create_opt
       |> on_update key opt
       |> State.set key opt
 
-    let reset st = set (get ()) st
+    let unsafe_get st = State.get key st
+
+    let clear st = State.update_opt key (fun _ -> None) st
 
     let get st =
-      try State.get key st with
+      try unsafe_get st with
       | State.Key_not_found _ -> get ()
   end)
 
-module ProduceAssignment =
-  (val (create_opt "produce_assignment" (fun _ -> false)))
+(* The current mode of the sat solver. Serves as a flag for some options that
+   cannot be updated outside start mode. *)
+module Mode = (val (create_opt "start_mode") (fun _ -> Util.Start))
+
+(* Similar to `create_opt`, except we fail if we set the option while we are not
+   in start mode. *)
+let create_opt_only_start_mode
+    (type t)
+    ?(on_update=(fun _ _ -> Fun.id))
+    (key : string)
+    (get : unit -> t) : (module S with type t = t) =
+  let on_update k opt st =
+    match Mode.get st with
+    | Util.Start -> on_update k opt st
+    | curr_mode -> Errors.invalid_set_option curr_mode key
+  in
+  create_opt ~on_update key get
+
+(* Any mode options. *)
 
 module Optimize =
   (val (create_opt "optimize" O.get_optimize))
 
+(* Start mode options. *)
+
+module ProduceAssignment =
+  (val (create_opt_only_start_mode "produce_assignment" (fun _ -> false)))
+
 let get_sat_solver
     ?(sat = O.get_sat_solver ())
     ?(no_th = O.get_no_theory ())
@@ -89,19 +113,22 @@ let get_sat_solver
   (module SatCont.Make(TH) : Sat_solver_sig.S)
 
 module SatSolverModule =
-  (val (create_opt "sat_solver_module" (fun _ -> get_sat_solver ())))
+  (val (
+     create_opt_only_start_mode
+       "sat_solver_module"
+       (fun _ -> get_sat_solver ())))
 
 let msatsolver =
   let on_update _ sat st =
     SatSolverModule.set (get_sat_solver ~sat ()) st
   in
-  (create_opt ~on_update "sat_solver" O.get_sat_solver)
+  (create_opt_only_start_mode ~on_update "sat_solver" O.get_sat_solver)
 
 module SatSolver = (val msatsolver)
 
 let msteps =
   let on_update _ sat st = Steps.set_steps_bound sat; st in
-  (create_opt ~on_update "steps_bound" O.get_steps_bound)
+  (create_opt_only_start_mode ~on_update "steps_bound" O.get_steps_bound)
 
 module Steps = (val msteps)
 
@@ -112,6 +139,6 @@ let options_requiring_initialization = [
 
 let init st =
   List.fold_left
-    (fun st (module S : S) -> S.reset st)
+    (fun st (module S : S) -> S.set (S.get (S.clear st)) st)
     st
     options_requiring_initialization
diff --git a/src/lib/frontend/d_state_option.mli b/src/lib/frontend/d_state_option.mli
index 70472f77a..0d373c3c0 100644
--- a/src/lib/frontend/d_state_option.mli
+++ b/src/lib/frontend/d_state_option.mli
@@ -48,15 +48,26 @@ module type S = sig
   val set : t -> D_loop.Typer.state -> D_loop.Typer.state
 
   (** Resets the option to its default value in Options. *)
-  val reset : D_loop.Typer.state -> D_loop.Typer.state
+  val clear : D_loop.Typer.state -> D_loop.Typer.state
 end
 
-(** Option for enabling/disabling the get-assignment instruction. *)
-module ProduceAssignment : S with type t = bool
+(** The current mode of the solver. *)
+module Mode : S with type t = Util.mode
+
+(** Options are divided in two categories:
+    1. options that can be updated anytime;
+    2. options that can only be updated during start mode. *)
+
+(** 1. Options that can be updated anytime. *)
 
 (** Option for enabling/disabling the optimization engine. *)
 module Optimize : S with type t = bool
 
+(** 2. Options that can only be updated during start mode. *)
+
+(** Option for enabling/disabling the get-assignment instruction. *)
+module ProduceAssignment : S with type t = bool
+
 (** The Sat solver used. When set, updates the SatSolverModule defined below. *)
 module SatSolver : S with type t = Util.sat_solver
 
diff --git a/src/lib/structures/errors.ml b/src/lib/structures/errors.ml
index c2f2d108f..d0ec32d90 100644
--- a/src/lib/structures/errors.ml
+++ b/src/lib/structures/errors.ml
@@ -85,6 +85,10 @@ type run_error =
   | Unsupported_feature of string
   | Dynlink_error of string
 
+type mode_error =
+  | Invalid_set_option of string
+  | Forbidden_command of string
+
 type error =
   | Parser_error of string
   | Lexical_error of Loc.t * string
@@ -93,6 +97,7 @@ type error =
   | Run_error of run_error
   | Warning_as_error
   | Dolmen_error of (int * string)
+  | Mode_error of Util.mode * mode_error
 
 exception Error of error
 
@@ -108,6 +113,12 @@ let warning_as_error () =
   if Options.get_warning_as_error () then
     error (Warning_as_error)
 
+let invalid_set_option mode opt_key =
+  error (Mode_error (mode, Invalid_set_option opt_key))
+
+let forbidden_command mode cmd_name =
+  error (Mode_error (mode, Forbidden_command cmd_name))
+
 let report_typing_error fmt = function
   | BitvExtract(i,j) ->
     fprintf fmt "bitvector extraction malformed (%d>%d)" i j
@@ -235,6 +246,12 @@ let report_run_error fmt = function
   | Dynlink_error s ->
     fprintf fmt "[Dynlink] %s" s
 
+let report_mode_error fmt = function
+  | Invalid_set_option s ->
+    fprintf fmt "Set option %s" s
+  | Forbidden_command s ->
+    fprintf fmt "Command %s" s
+
 let report fmt = function
   | Parser_error s ->
     Format.fprintf fmt "Parser Error: %s" s;
@@ -254,3 +271,9 @@ let report fmt = function
   | Dolmen_error (code, descr) ->
     Format.fprintf fmt "Error %s (code %i)" descr code;
   | Warning_as_error -> ()
+  | Mode_error (mode, merr) ->
+    Format.fprintf
+      fmt
+      "Invalid action during %a mode: %a"
+      Util.pp_mode mode
+      report_mode_error merr;
diff --git a/src/lib/structures/errors.mli b/src/lib/structures/errors.mli
index 59563364d..b0ca4ddc0 100644
--- a/src/lib/structures/errors.mli
+++ b/src/lib/structures/errors.mli
@@ -92,6 +92,11 @@ type run_error =
   | Unsupported_feature of string
   | Dynlink_error of string
 
+(** Errors raised when performing actions forbidden in some modes. *)
+type mode_error =
+  | Invalid_set_option of string
+  | Forbidden_command of string
+
 (** All types of error that can be raised *)
 type error =
   | Parser_error of string (** Error used at parser loading *)
@@ -102,6 +107,8 @@ type error =
   | Warning_as_error
   | Dolmen_error of (int * string)
   (** Error code + description raised by dolmen. *)
+  | Mode_error of Util.mode * mode_error
+  (** Error used when performing actions forbidden in some modes. *)
 
 (** {2 Exceptions } *)
 
@@ -123,6 +130,14 @@ val run_error : run_error -> 'a
     This function can be use after warning *)
 val warning_as_error : unit -> unit
 
+(** Raise [Mode_error (Invalid_set_option str)] as {!Error} if an option is
+    being set when it should be immutable. *)
+val invalid_set_option : Util.mode -> string -> 'a
+
+(** Raise [Mode_error (Forbidden_command str)] as {!Error} if a command is
+    being used in a mode where it should not be available. *)
+val forbidden_command : Util.mode -> string -> 'a
+
 (** {2 Printing } *)
 
 (** Print a message on the formatter corresponding to the error *)
diff --git a/src/lib/util/util.ml b/src/lib/util/util.ml
index 2ac39acfa..a2d7048f6 100644
--- a/src/lib/util/util.ml
+++ b/src/lib/util/util.ml
@@ -98,6 +98,29 @@ type theories_extensions =
 
 type axiom_kind = Default | Propagator
 
+type mode =
+  | Start
+  | Assert
+  | Sat
+  | Unsat
+
+let pp_mode fmt m =
+  Format.pp_print_string fmt begin
+    match m with
+    | Start -> "Start"
+    | Assert -> "Assert"
+    | Sat -> "Sat"
+    | Unsat -> "Unsat"
+  end
+
+let equal_mode x y = match x, y with
+  | Start, Start
+  | Assert, Assert
+  | Sat, Sat
+  | Unsat, Unsat -> true
+  | (Start | Assert | Sat | Unsat), (Start | Assert | Sat | Unsat) ->
+    false
+
 let th_ext_of_string ext =
   match ext with
   | "Sum" -> Some Sum
diff --git a/src/lib/util/util.mli b/src/lib/util/util.mli
index 7fa2b0976..0bc8a194c 100644
--- a/src/lib/util/util.mli
+++ b/src/lib/util/util.mli
@@ -76,6 +76,19 @@ type theories_extensions =
 
 type axiom_kind = Default | Propagator
 
+(** The different modes alt-ergo can be in.
+    https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf#52
+*)
+type mode =
+  | Start
+  | Assert
+  | Sat
+  | Unsat
+
+val equal_mode : mode -> mode -> bool
+
+val pp_mode : Format.formatter -> mode -> unit
+
 val th_ext_of_string : string -> theories_extensions option
 val string_of_th_ext : theories_extensions -> string
 
diff --git a/tests/cram.t/run.t b/tests/cram.t/run.t
index 7826ace58..bf837bf48 100644
--- a/tests/cram.t/run.t
+++ b/tests/cram.t/run.t
@@ -40,47 +40,68 @@ And some SMT2 action.
 Here are some tests to check that we have sane behavior given the insane
 combinations of produce-models et al.
 
-First, if model generation is not enabled, we should error out when a
+First, if (get-model) is called outside the SAT mode, we should fail.
+  $ echo '(get-model)' | alt-ergo -i smtlib2 -o smtlib2 --continue-on-error 2> /dev/null
+  (error "Invalid action during Start mode: Command get-model")
+
+
+  $ echo '(set-logic ALL)(get-model)' | alt-ergo -i smtlib2 -o smtlib2 --continue-on-error 2> /dev/null
+  (error "Invalid action during Assert mode: Command get-model")
+
+  $ echo '(set-logic ALL)(assert false)(check-sat)(get-model)' | alt-ergo -i smtlib2 -o smtlib2 --continue-on-error 2> /dev/null
+  
+  unsat
+  (error "Invalid action during Unsat mode: Command get-model")
+
+Then, if model generation is not enabled, we should error out when a
 `(get-model)` statement is issued:
 
-  $ echo '(get-model)' | alt-ergo -i smtlib2 -o smtlib2 --continue-on-error
+  $ echo '(set-logic ALL)(check-sat)(get-model)' | alt-ergo -i smtlib2 -o smtlib2 --continue-on-error 2> /dev/null
+  
+  unknown
   (error "Model generation disabled (try --produce-models)")
 
 This should be the case Tableaux solver as well:
 
-  $ echo '(get-model)' | alt-ergo --sat-solver Tableaux -i smtlib2 -o smtlib2 --continue-on-error
+  $ echo '(set-logic ALL)(check-sat)(get-model)' | alt-ergo --sat-solver Tableaux -i smtlib2 -o smtlib2 --continue-on-error 2> /dev/null
+  
+  unknown
   (error "Model generation disabled (try --produce-models)")
 
 The messages above mention `--produce-models`, but we can also use
 `set-option`.
 
-  $ echo '(get-model)' | alt-ergo --produce-models -i smtlib2 -o smtlib2 --continue-on-error
-  (error "No model produced.")
+  $ echo '(set-option :produce-models false)(set-logic ALL)(check-sat)(get-model)' | alt-ergo --produce-models -i smtlib2 -o smtlib2 --continue-on-error 2> /dev/null
+  
+  unknown
+  (error "Model generation disabled (try --produce-models)")
 
-  $ echo '(set-option :produce-models true)(get-model)' | alt-ergo --sat-solver Tableaux -i smtlib2 -o smtlib2 --continue-on-error
-  (error "No model produced.")
+  $ echo '(set-option :produce-models false)(set-logic ALL)(check-sat)(get-model)' | alt-ergo --sat-solver Tableaux -i smtlib2 -o smtlib2 --continue-on-error 2> /dev/null
+  
+  unknown
+  (error "Model generation disabled (try --produce-models)")
 
 And now some cases where it should work (using either `--produce-models` or `set-option`):
 
-  $ echo '(check-sat)(get-model)' | alt-ergo --produce-models -i smtlib2 -o smtlib2 2>/dev/null
+  $ echo '(set-logic ALL)(check-sat)(get-model)' | alt-ergo --produce-models -i smtlib2 -o smtlib2 2>/dev/null
   
   unknown
   (
   )
 
-  $ echo '(set-option :produce-models true)(check-sat)(get-model)' | alt-ergo -i smtlib2 -o smtlib2 2>/dev/null
+  $ echo '(set-option :produce-models true)(set-logic ALL)(check-sat)(get-model)' | alt-ergo -i smtlib2 -o smtlib2 2>/dev/null
   
   unknown
   (
   )
-  $ echo '(set-option :produce-models true)(check-sat)(get-model)' | alt-ergo --sat-solver Tableaux -i smtlib2 -o smtlib2 2>/dev/null
+  $ echo '(set-option :produce-models true)(set-logic ALL)(check-sat)(get-model)' | alt-ergo --sat-solver Tableaux -i smtlib2 -o smtlib2 2>/dev/null
   
   unknown
   (
   )
 
 We now test the --continue-on-error strategy where alt-ergo fails (legitimately) on some commands but keeps running.
-  $ echo '(get-info :foo) (set-option :bar) (check-sat)' | alt-ergo -i smtlib2 -o smtlib2 --continue-on-error 2>/dev/null
+  $ echo '(get-info :foo) (set-option :bar) (set-logic ALL) (check-sat)' | alt-ergo -i smtlib2 -o smtlib2 --continue-on-error 2>/dev/null
   unsupported
   
   (error "Invalid set-option")
diff --git a/tests/dune.inc b/tests/dune.inc
index 1ee60d42c..834fd3cff 100644
--- a/tests/dune.inc
+++ b/tests/dune.inc
@@ -205082,8 +205082,8 @@
 ; Auto-generated part begin
 (subdir smtlib
   (rule
-   (target testfile-steps-bound.dolmen_dolmen.output)
-   (deps (:input testfile-steps-bound.dolmen.smt2))
+   (target testfile-steps-bound2.dolmen_dolmen.output)
+   (deps (:input testfile-steps-bound2.dolmen.smt2))
    (package alt-ergo)
    (action
     (chdir %{workspace_root}
@@ -205097,11 +205097,32 @@
              --frontend dolmen
              %{input})))))))
   (rule
-   (deps testfile-steps-bound.dolmen_dolmen.output)
+   (deps testfile-steps-bound2.dolmen_dolmen.output)
     (alias runtest-quick)
      (package alt-ergo)
       (action
-       (diff testfile-steps-bound.dolmen.expected testfile-steps-bound.dolmen_dolmen.output)))
+       (diff testfile-steps-bound2.dolmen.expected testfile-steps-bound2.dolmen_dolmen.output)))
+  (rule
+   (target testfile-steps-bound1.dolmen.err_dolmen.output)
+   (deps (:input testfile-steps-bound1.dolmen.err.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes (or 1)
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             %{input})))))))
+  (rule
+   (deps testfile-steps-bound1.dolmen.err_dolmen.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff testfile-steps-bound1.dolmen.err.expected testfile-steps-bound1.dolmen.err_dolmen.output)))
   (rule
    (target testfile-reset_ci_cdcl_no_minimal_bj.output)
    (deps (:input testfile-reset.smt2))
diff --git a/tests/models/bool/bool1.models.smt2 b/tests/models/bool/bool1.models.smt2
index d6d90b5a8..a4e6549ec 100644
--- a/tests/models/bool/bool1.models.smt2
+++ b/tests/models/bool/bool1.models.smt2
@@ -1,6 +1,6 @@
-(set-logic QF_UF)
 (set-option :produce-models true) ; enable model generation
 (set-option :produce-assignments true) ; enable get assignment
+(set-logic QF_UF)
 (declare-const p Bool)
 (declare-const q Bool)
 ; (declare-const t Int)
diff --git a/tests/models/bool/bool2.models.smt2 b/tests/models/bool/bool2.models.smt2
index 30321c945..28f16ef23 100644
--- a/tests/models/bool/bool2.models.smt2
+++ b/tests/models/bool/bool2.models.smt2
@@ -1,6 +1,6 @@
-(set-logic QF_UF)
 (set-option :produce-models true)
 (set-option :produce-assignments true)
+(set-logic QF_UF)
 (declare-const x Bool)
 (declare-const y Bool)
 (assert (or x (! (not x) :named notx)))
diff --git a/tests/models/bool/bool3.models.smt2 b/tests/models/bool/bool3.models.smt2
index 759cd3bb2..1d417aec4 100644
--- a/tests/models/bool/bool3.models.smt2
+++ b/tests/models/bool/bool3.models.smt2
@@ -1,6 +1,6 @@
-(set-logic ALL)
 (set-option :produce-assignments true)
 (set-option :produce-models true)
+(set-logic ALL)
 (declare-const x Bool)
 (declare-const y Bool)
 (assert (or (! (and x y) :named foo) (! (and (not x) (not y)) :named bar)))
diff --git a/tests/smtlib/testfile-get-assignment3.dolmen.smt2 b/tests/smtlib/testfile-get-assignment3.dolmen.smt2
index ad1960cbd..5aea879f7 100644
--- a/tests/smtlib/testfile-get-assignment3.dolmen.smt2
+++ b/tests/smtlib/testfile-get-assignment3.dolmen.smt2
@@ -1,5 +1,5 @@
-(set-logic ALL)
 (set-option :produce-assignments true)
+(set-logic ALL)
 (declare-const x Int)
 (assert (! (= x 0) :named foo))
 (check-sat)
diff --git a/tests/smtlib/testfile-steps-bound.dolmen.smt2 b/tests/smtlib/testfile-steps-bound.dolmen.smt2
deleted file mode 100644
index ed9711b98..000000000
--- a/tests/smtlib/testfile-steps-bound.dolmen.smt2
+++ /dev/null
@@ -1,26 +0,0 @@
-(set-logic ALL)
-
-(declare-const x Int)
-(declare-const y Int)
-(assert (= (* x x) 3))
-
-(push 1)
-; Setting this option here should fail because the previous assertion takes
-; more than 2 steps. It does not because AE does not execute SMTLIB instruction
-; imperatively; here, the option is actually set before the assertion is
-; executed.
-(set-option :steps-bound 2)
-; Should answer 'unknown'
-(check-sat)
-(get-info :reason-unknown)
-(pop 1)
-
-(reset)
-
-(set-logic ALL)
-(declare-const x Int)
-(declare-const y Int)
-(set-option :steps-bound 100)
-; Should answer 'unsat'
-(assert (= (* x x) 3))
-(check-sat)
\ No newline at end of file
diff --git a/tests/smtlib/testfile-steps-bound1.dolmen.err.expected b/tests/smtlib/testfile-steps-bound1.dolmen.err.expected
new file mode 100644
index 000000000..4536febdd
--- /dev/null
+++ b/tests/smtlib/testfile-steps-bound1.dolmen.err.expected
@@ -0,0 +1 @@
+(error "Invalid action during Assert mode: Set option steps_bound")
diff --git a/tests/smtlib/testfile-steps-bound1.dolmen.err.smt2 b/tests/smtlib/testfile-steps-bound1.dolmen.err.smt2
new file mode 100644
index 000000000..2da3ac5d7
--- /dev/null
+++ b/tests/smtlib/testfile-steps-bound1.dolmen.err.smt2
@@ -0,0 +1,7 @@
+(set-logic ALL)
+
+(declare-const x Int)
+(assert (= (* x x) 3))
+(set-option :steps-bound 2)
+; Should fail because this option cannot be set after set-logic
+(check-sat)
\ No newline at end of file
diff --git a/tests/smtlib/testfile-steps-bound.dolmen.expected b/tests/smtlib/testfile-steps-bound2.dolmen.expected
similarity index 100%
rename from tests/smtlib/testfile-steps-bound.dolmen.expected
rename to tests/smtlib/testfile-steps-bound2.dolmen.expected
diff --git a/tests/smtlib/testfile-steps-bound2.dolmen.smt2 b/tests/smtlib/testfile-steps-bound2.dolmen.smt2
new file mode 100644
index 000000000..3d578cf45
--- /dev/null
+++ b/tests/smtlib/testfile-steps-bound2.dolmen.smt2
@@ -0,0 +1,17 @@
+(set-option :steps-bound 2)
+(set-logic ALL)
+
+(declare-const x Int)
+(assert (= (* x x) 3))
+; Should answer 'unknown'
+(check-sat)
+(get-info :reason-unknown)
+
+(reset)
+
+(set-option :steps-bound 100)
+(set-logic ALL)
+(declare-const x Int)
+(assert (= (* x x) 3))
+; Should answer 'unsat'
+(check-sat)
\ No newline at end of file