diff --git a/src/bin/common/parse_command.ml b/src/bin/common/parse_command.ml
index fc6947dd3..7aaa7d240 100644
--- a/src/bin/common/parse_command.ml
+++ b/src/bin/common/parse_command.ml
@@ -319,7 +319,8 @@ let mk_execution_opt input_format parse_only ()
   set_preludes preludes;
   `Ok()
 
-let mk_internal_opt disable_weaks enable_assertions warning_as_error gc_policy
+let mk_internal_opt
+    disable_weaks enable_assertions warning_as_error continue_on_error gc_policy
   =
   let gc_policy = match gc_policy with
     | 0 | 1 | 2 -> gc_policy
@@ -330,6 +331,7 @@ let mk_internal_opt disable_weaks enable_assertions warning_as_error gc_policy
   set_disable_weaks disable_weaks;
   set_enable_assertions enable_assertions;
   set_warning_as_error warning_as_error;
+  set_exit_on_error (not continue_on_error);
   `Ok(gc_policy)
 
 let mk_limit_opt age_bound fm_cross_limit timelimit_interpretation
@@ -491,7 +493,7 @@ let halt_opt version_info where =
     | Some w -> handle_where w; `Ok true
     | None -> if version_info then (handle_version_info version_info; `Ok true)
       else `Ok false
-  with Failure f -> `Error (false, f)
+  with Failure f -> `Error (false, f) (* TODO(Steven): dead code? *)
      | Error (b, m) -> `Error (b, m)
 
 let get_verbose_t =
@@ -774,6 +776,10 @@ let parse_internal_opt =
     let doc = "Enable warning as error" in
     Arg.(value & flag & info ["warning-as-error"] ~docs ~doc) in
 
+  let continue_on_error =
+    let doc = "Sets Alt-ergo's behavior to continue on errors" in
+    Arg.(value & flag & info ["continue-on-error"] ~docs ~doc) in
+
   let gc_policy =
     let doc =
       "Set the gc policy allocation. 0 = next-fit policy, 1 = \
@@ -783,7 +789,8 @@ let parse_internal_opt =
     Arg.(value & opt int 0 & info ["gc-policy"] ~docv ~docs ~doc) in
 
   Term.(ret (const mk_internal_opt $
-             disable_weaks $ enable_assertions $ warning_as_error $ gc_policy
+             disable_weaks $ enable_assertions $
+             warning_as_error $ continue_on_error $ gc_policy
             ))
 
 let parse_limit_opt =
diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml
index b39d80f87..3746d9a99 100644
--- a/src/bin/common/solving_loop.ml
+++ b/src/bin/common/solving_loop.ml
@@ -50,8 +50,34 @@ let empty_solver_ctx = {
   global = [];
 }
 
-let unsupported_opt () =
-  Printer.print_std "unsupported"
+let recoverable_error ?(code = 1) =
+  Format.kasprintf (fun msg ->
+      let () =
+        if msg <> "" then
+          match Options.get_output_format () with
+          | Smtlib2 -> Printer.print_smtlib_err "%s" msg
+          | _ -> Printer.print_err "%s" msg
+      in
+      if Options.get_exit_on_error () then exit code)
+
+let fatal_error ?(code = 1) =
+  Format.kasprintf (fun msg -> recoverable_error ~code "%s" msg; exit code)
+
+let exit_as_timeout () = fatal_error ~code:142 "timeout"
+
+let warning (msg : ('a, Format.formatter, unit, unit, unit, 'b) format6) : 'a =
+  if Options.get_warning_as_error () then
+    recoverable_error msg
+  else
+    Printer.print_wrn msg
+
+let unsupported_opt opt =
+  let () =
+    match Options.get_output_format () with
+    | Options.Smtlib2 -> Printer.print_std "unsupported"
+    | _ -> ()
+  in
+  warning "unsupported option %s" opt
 
 let main () =
   let () = Dolmen_loop.Code.init [] in
@@ -103,9 +129,8 @@ let main () =
       | `Sat partial_model | `Unknown partial_model ->
         Some partial_model
       | `Unsat -> None
-    with
-    | Util.Timeout ->
-      if not (Options.get_timelimit_per_goal()) then exit 142;
+    with Util.Timeout ->
+      if not (Options.get_timelimit_per_goal()) then exit_as_timeout ();
       None
   in
 
@@ -186,14 +211,18 @@ let main () =
       with
       | Util.Timeout ->
         FE.print_status (FE.Timeout None) 0;
-        exit 142
+        exit_as_timeout ()
       | Parsing.Parse_error ->
-        Printer.print_err "%a" Errors.report
-          (Syntax_error ((Lexing.dummy_pos,Lexing.dummy_pos),""));
-        exit 1
+        (* TODO(Steven): displaying a dummy value is a bad idea.
+           This should only be executed with the legacy frontend, which should
+           be deprecated in a near future, so this code will be removed (or at
+           least, its behavior unspecified). *)
+        fatal_error
+          "%a"
+          Errors.report
+          (Syntax_error ((Lexing.dummy_pos,Lexing.dummy_pos),""))
       | Errors.Error e ->
-        Printer.print_err "%a" Errors.report e;
-        exit 1
+        fatal_error "%a" Errors.report e
     in
 
     let all_used_context = FE.init_all_used_context () in
@@ -207,9 +236,13 @@ let main () =
           List.fold_left (typed_loop all_used_context) { state with env; } l
         with
         | Errors.Error e ->
-          if e != Warning_as_error then
-            Printer.print_err "%a" Errors.report e;
-          exit 1
+          let () =
+            if e != Warning_as_error then
+              recoverable_error "%a" Errors.report e
+            else
+              recoverable_error ""
+          in
+          state
         | Exit -> exit 0
       end
     in
@@ -224,7 +257,7 @@ let main () =
       Options.Time.unset_timeout ();
     with Util.Timeout ->
       FE.print_status (FE.Timeout None) 0;
-      exit 142
+      exit_as_timeout ()
   in
 
   let solver_ctx_key: solver_ctx State.key =
@@ -255,22 +288,21 @@ let main () =
     else
       st, `Continue stmt
   in
-  let handle_exn _ bt = function
+  let handle_exn st bt = function
     | Dolmen.Std.Loc.Syntax_error (_, `Regular msg) ->
-      Printer.print_err "%t" msg;
-      exit 1
+      recoverable_error "%t" msg; st
     | Util.Timeout ->
       Printer.print_status_timeout None None None None;
-      exit 142
+      exit_as_timeout ()
     | Errors.Error e ->
-      Printer.print_err "%a" Errors.report e;
-      exit 1
+      recoverable_error "%a" Errors.report e;
+      st
     | Exit -> exit 0
     | _ as exn -> Printexc.raise_with_backtrace exn bt
   in
   let finally ~handle_exn st e =
     match e with
-    | Some (bt, exn) -> handle_exn st bt exn; st
+    | Some (bt, exn) -> handle_exn st bt exn
     | _ -> st
   in
   let set_output_format fmt =
@@ -279,8 +311,9 @@ let main () =
       | ".ae" -> Options.set_output_format Native
       | ".smt2" | ".psmt2" -> Options.set_output_format Smtlib2
       | s ->
-        Printer.print_wrn
-          "The output format %s is not supported by the Dolmen frontend." s
+        warning
+          "The output format %s is not supported by the Dolmen frontend."
+          s
   in
   (* The function In_channel.input_all is not available before OCaml 4.14. *)
   let read_all ch =
@@ -353,7 +386,8 @@ let main () =
   in
 
   let print_wrn_opt ~name loc ty value =
-    Printer.print_wrn "%a The option %s expects a %s, got %a"
+    warning
+      "%a The option %s expects a %s, got %a"
       Loc.report loc name ty DStd.Term.print value
   in
 
@@ -374,9 +408,11 @@ let main () =
          solver Tableaux. *)
       if Stdlib.(Options.get_sat_solver () = Tableaux) then
         Options.set_unsat_core true
-      else Printer.print_wrn "%a The generation of unsat cores is not \
-                              supported for the current SAT solver. Please \
-                              choose the SAT solver Tableaux."
+      else
+        warning
+          "%a The generation of unsat cores is not \
+           supported for the current SAT solver. Please \
+           choose the SAT solver Tableaux."
           Loc.report st_loc
     | ":produce-unsat-cores", Symbol { name = Simple "false"; _ } ->
       Options.set_unsat_core false
@@ -408,11 +444,9 @@ let main () =
       | ":print-success"
       | ":random-seed"), _
       ->
-      unsupported_opt ();
-      Printer.print_wrn "unsupported option '%s'" name
+      unsupported_opt name
     | _ ->
-      unsupported_opt ();
-      Printer.print_err "unknown option '%s'" name
+      unsupported_opt name
   in
 
   let handle_get_info (st : State.t) (name: string) =
@@ -422,8 +456,7 @@ let main () =
     in
     let pp_reason_unknown st =
       let err () =
-        let msg = "Invalid (get-info :reason-unknown)" in
-        Printer.print_smtlib_err "%s" msg
+        recoverable_error "Invalid (get-info :reason-unknown)"
       in
       match State.get partial_model_key st with
       | None -> err ()
@@ -439,7 +472,13 @@ let main () =
     | ":authors" ->
       print_std (fun fmt -> Fmt.pf fmt "%S") "Alt-Ergo developers"
     | ":error-behavior" ->
-      print_std Fmt.string "immediate-exit"
+      let behavior =
+        if Options.get_exit_on_error () then
+          "immediate-exit"
+        else
+          "continued-execution"
+      in
+      print_std Fmt.string behavior
     | ":name" ->
       print_std (fun fmt -> Fmt.pf fmt "%S") "Alt-Ergo"
     | ":reason-unknown" ->
@@ -448,11 +487,9 @@ let main () =
       print_std Fmt.string Version._version
     | ":all-statistics"
     | ":assertion-stack-levels" ->
-      unsupported_opt ();
-      Printer.print_wrn "unsupported option '%s'" name
+      unsupported_opt name
     | _ ->
-      unsupported_opt ();
-      Printer.print_err "unknown option '%s'" name
+      unsupported_opt name
   in
 
   let handle_stmt :
@@ -530,6 +567,10 @@ let main () =
         handle_option loc name value;
         st
 
+      | {contents = `Set_option _; _} ->
+        recoverable_error "Invalid set-option";
+        st
+
       | {contents = `Get_model; _ } ->
         if Options.get_interpretation () then
           match State.get partial_model_key st with
@@ -546,12 +587,11 @@ let main () =
             end
           | None ->
             (* TODO: add the location of the statement. *)
-            Printer.print_smtlib_err "No model produced.";
-            st
+            recoverable_error "No model produced."; st
         else
           begin
             (* TODO: add the location of the statement. *)
-            Printer.print_smtlib_err
+            recoverable_error
               "Model generation disabled (try --produce-models)";
             st
           end
@@ -623,7 +663,7 @@ let main () =
       State.flush st () |> ignore
     with exn ->
       let bt = Printexc.get_raw_backtrace () in
-      handle_exn st bt exn
+      ignore (handle_exn st bt exn)
   in
 
   let filename = get_file () in
diff --git a/src/lib/structures/errors.ml b/src/lib/structures/errors.ml
index 3e68fe623..4ec89aaa5 100644
--- a/src/lib/structures/errors.ml
+++ b/src/lib/structures/errors.ml
@@ -240,24 +240,20 @@ let report_run_error fmt = function
 
 let report fmt = function
   | Parser_error s ->
-    Options.pp_comment fmt
-      (Format.sprintf "Parser Error: %s" s);
+    Format.fprintf fmt "Parser Error: %s" s;
   | Lexical_error (l,s) ->
     Loc.report fmt l;
-    Options.pp_comment fmt
-      (Format.sprintf "Lexical Error: %s" s);
+    Format.fprintf fmt "Lexical Error: %s" s;
   | Syntax_error (l,s) ->
     Loc.report fmt l;
-    Options.pp_comment fmt
-      (Format.sprintf "Syntax Error: %s" s);
+    Format.fprintf fmt "Syntax Error: %s" s;
   | Typing_error (l,e) ->
     Loc.report fmt l;
-    Options.pp_comment fmt "Typing Error: ";
+    Format.fprintf fmt "Typing Error: ";
     report_typing_error fmt e
   | Run_error e ->
-    Options.pp_comment fmt "Fatal Error: ";
+    Format.fprintf fmt "Fatal Error: ";
     report_run_error fmt e
   | Dolmen_error (code, descr) ->
-    Options.pp_comment fmt
-      (Format.sprintf "Error %s (code %i)" descr code);
+    Format.fprintf fmt "Error %s (code %i)" descr code;
   | Warning_as_error -> ()
diff --git a/src/lib/util/options.ml b/src/lib/util/options.ml
index 70fac991f..f5b420b1b 100644
--- a/src/lib/util/options.ml
+++ b/src/lib/util/options.ml
@@ -299,14 +299,17 @@ let get_type_smt2 () = !type_smt2
 let disable_weaks = ref false
 let enable_assertions = ref false
 let warning_as_error = ref false
+let exit_on_error = ref true
 
 let set_disable_weaks b = disable_weaks := b
 let set_enable_assertions b = enable_assertions := b
 let set_warning_as_error b = warning_as_error := b
+let set_exit_on_error b = exit_on_error := b
 
 let get_disable_weaks () = !disable_weaks
 let get_enable_assertions () = !enable_assertions
 let get_warning_as_error () = !warning_as_error
+let get_exit_on_error () = !exit_on_error
 
 (** Limit options *)
 
diff --git a/src/lib/util/options.mli b/src/lib/util/options.mli
index bdc4fd924..9002960b3 100644
--- a/src/lib/util/options.mli
+++ b/src/lib/util/options.mli
@@ -356,6 +356,9 @@ val set_enable_assertions : bool -> unit
 (** Set [warning_as_error] accessible with {!val:get_warning_as_error} *)
 val set_warning_as_error : bool -> unit
 
+(** Set [exit_on_error] accessible with {!val:get_exit_on_error} *)
+val set_exit_on_error : bool -> unit
+
 (** Set [timelimit_interpretation] accessible with
     {!val:get_timelimit_interpretation} *)
 val set_timelimit_interpretation : float -> unit
@@ -653,6 +656,10 @@ val get_enable_assertions : unit -> bool
 val get_warning_as_error : unit -> bool
 (** Default to [false] *)
 
+(** [true] if alt-ergo exits on all errors. *)
+val get_exit_on_error : unit -> bool
+(** Default to [true] *)
+
 (** {4 Limit options} *)
 
 (** Value specifying the age limit bound. *)
diff --git a/src/lib/util/printer.ml b/src/lib/util/printer.ml
index 983cbaa67..b4e6641e3 100644
--- a/src/lib/util/printer.ml
+++ b/src/lib/util/printer.ml
@@ -386,6 +386,7 @@ let print_status_preprocess ?(validity_mode=true)
 
 let print_smtlib_err ?(flushed=true) s =
   (* The smtlib error messages are printed on the regular output. *)
+  pp_std_smt ();
   let fmt = Options.Output.get_fmt_regular () in
   let k fmt =
     if flushed || Options.get_output_with_forced_flush () then
diff --git a/tests/cram.t/run.t b/tests/cram.t/run.t
index ff932c959..26b3c6051 100644
--- a/tests/cram.t/run.t
+++ b/tests/cram.t/run.t
@@ -1,5 +1,5 @@
   $ echo '(check-sat)' | alt-ergo --inequalities-plugin does-not-exist -i smtlib2 -o smtlib2 2>&1 >/dev/null | sed -E 's/\(\\".*\\"\)//'
-  alt-ergo: ; Fatal Error: [Dynlink] Loading the 'inequalities' reasoner (FM module) plugin in "does-not-exist" failed!
+  alt-ergo: Fatal Error: [Dynlink] Loading the 'inequalities' reasoner (FM module) plugin in "does-not-exist" failed!
             >> Failure message: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure")
 
 Now we will have some tests for the models. Note that it is okay if the format
@@ -43,21 +43,21 @@ combinations of produce-models et al.
 First, 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
+  $ echo '(get-model)' | alt-ergo -i smtlib2 -o smtlib2 --continue-on-error
   (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
+  $ echo '(get-model)' | alt-ergo --sat-solver Tableaux -i smtlib2 -o smtlib2 --continue-on-error
   (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
+  $ echo '(get-model)' | alt-ergo --produce-models -i smtlib2 -o smtlib2 --continue-on-error
   (error "No model produced.")
 
-  $ echo '(set-option :produce-models true)(get-model)' | alt-ergo --sat-solver Tableaux -i smtlib2 -o smtlib2
+  $ echo '(set-option :produce-models true)(get-model)' | alt-ergo --sat-solver Tableaux -i smtlib2 -o smtlib2 --continue-on-error
   (error "No model produced.")
 
 And now some cases where it should work (using either `--produce-models` or `set-option`):
@@ -78,3 +78,18 @@ And now some cases where it should work (using either `--produce-models` or `set
   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
+  unsupported
+  
+  (error "Invalid set-option")
+  
+  unknown
+
+Some errors are unescapable though. It its the case of syntax error in commands.
+  $ echo '(get-info :foo) (set-option :bar) (exil) (check-sat)' | alt-ergo -i smtlib2 -o smtlib2 --continue-on-error 2>/dev/null
+  unsupported
+  
+  (error "Invalid set-option")
+  (error "Error on parsing errors (code 3)")
diff --git a/tests/dune.inc b/tests/dune.inc
index b35bde54b..5ef5b2b99 100644
--- a/tests/dune.inc
+++ b/tests/dune.inc
@@ -155091,27 +155091,6 @@
      (package alt-ergo)
       (action
        (diff testfile-tab001.expected testfile-tab001_fpa.output)))
-  (rule
-   (target testfile-smt-instr-get-info.dolmen_dolmen.output)
-   (deps (:input testfile-smt-instr-get-info.dolmen.smt2))
-   (package alt-ergo)
-   (action
-    (chdir %{workspace_root}
-     (with-stdout-to %{target}
-      (ignore-stderr
-       (with-accepted-exit-codes 0
-        (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
-             --output=smtlib2
-             --frontend dolmen
-             %{input})))))))
-  (rule
-   (deps testfile-smt-instr-get-info.dolmen_dolmen.output)
-    (alias runtest-quick)
-     (package alt-ergo)
-      (action
-       (diff testfile-smt-instr-get-info.dolmen.expected testfile-smt-instr-get-info.dolmen_dolmen.output)))
   (rule
    (target testfile-predicate002_ci_cdcl_no_minimal_bj.output)
    (deps (:input testfile-predicate002.ae))
@@ -192528,14 +192507,14 @@
 ; Auto-generated part begin
 (subdir models/issues
   (rule
-   (target 719.models_tableaux.output)
-   (deps (:input 719.models.smt2))
+   (target 719.models.err_tableaux.output)
+   (deps (:input 719.models.err.smt2))
    (package alt-ergo)
    (action
     (chdir %{workspace_root}
      (with-stdout-to %{target}
       (ignore-stderr
-       (with-accepted-exit-codes 0
+       (with-accepted-exit-codes 1
         (run %{bin:alt-ergo}
              --timelimit=2
              --enable-assertions
@@ -192544,11 +192523,11 @@
              --sat-solver Tableaux
              %{input})))))))
   (rule
-   (deps 719.models_tableaux.output)
+   (deps 719.models.err_tableaux.output)
     (alias runtest-quick)
      (package alt-ergo)
       (action
-       (diff 719.models.expected 719.models_tableaux.output))))
+       (diff 719.models.err.expected 719.models.err_tableaux.output))))
 ; Auto-generated part end
 ; File auto-generated by gentests
 
@@ -203531,6 +203510,69 @@
      (package alt-ergo)
       (action
        (diff testfile-push-pop1.err.dolmen.expected testfile-push-pop1.err.dolmen_dolmen.output)))
+  (rule
+   (target testfile-get-info3.dolmen_dolmen.output)
+   (deps (:input testfile-get-info3.dolmen.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             %{input})))))))
+  (rule
+   (deps testfile-get-info3.dolmen_dolmen.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff testfile-get-info3.dolmen.expected testfile-get-info3.dolmen_dolmen.output)))
+  (rule
+   (target testfile-get-info2.err.dolmen_dolmen.output)
+   (deps (:input testfile-get-info2.err.dolmen.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 1
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             %{input})))))))
+  (rule
+   (deps testfile-get-info2.err.dolmen_dolmen.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff testfile-get-info2.err.dolmen.expected testfile-get-info2.err.dolmen_dolmen.output)))
+  (rule
+   (target testfile-get-info1.dolmen_dolmen.output)
+   (deps (:input testfile-get-info1.dolmen.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             %{input})))))))
+  (rule
+   (deps testfile-get-info1.dolmen_dolmen.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff testfile-get-info1.dolmen.expected testfile-get-info1.dolmen_dolmen.output)))
   (rule
    (target testfile-exit_ci_cdcl_no_minimal_bj.output)
    (deps (:input testfile-exit.smt2))
diff --git a/tests/models/issues/719.models.expected b/tests/models/issues/719.models.err.expected
similarity index 100%
rename from tests/models/issues/719.models.expected
rename to tests/models/issues/719.models.err.expected
diff --git a/tests/models/issues/719.models.smt2 b/tests/models/issues/719.models.err.smt2
similarity index 92%
rename from tests/models/issues/719.models.smt2
rename to tests/models/issues/719.models.err.smt2
index d717b2e50..66c07f37c 100644
--- a/tests/models/issues/719.models.smt2
+++ b/tests/models/issues/719.models.err.smt2
@@ -16,3 +16,4 @@
     (=> (and (<= 0 p) (< p q) (<= q 10)) (<= (select a p) (select a q))))))
 (check-sat)
 (get-model)
+; (get-model) should fail because the problem is UNSAT.
\ No newline at end of file
diff --git a/tests/everything/testfile-smt-instr-get-info.dolmen.expected b/tests/smtlib/testfile-get-info1.dolmen.expected
similarity index 74%
rename from tests/everything/testfile-smt-instr-get-info.dolmen.expected
rename to tests/smtlib/testfile-get-info1.dolmen.expected
index d3e05dee0..ac5fd363b 100644
--- a/tests/everything/testfile-smt-instr-get-info.dolmen.expected
+++ b/tests/smtlib/testfile-get-info1.dolmen.expected
@@ -1,4 +1,3 @@
-(error "Invalid (get-info :reason-unknown)")
 
 unknown
 unsupported
@@ -10,4 +9,3 @@ unsupported
 (:name "Alt-Ergo")
 (:reason-unknown Incomplete)
 (:version dev)
-unsupported
diff --git a/tests/everything/testfile-smt-instr-get-info.dolmen.smt2 b/tests/smtlib/testfile-get-info1.dolmen.smt2
similarity index 73%
rename from tests/everything/testfile-smt-instr-get-info.dolmen.smt2
rename to tests/smtlib/testfile-get-info1.dolmen.smt2
index 4fd233ce5..b7f2454f3 100644
--- a/tests/everything/testfile-smt-instr-get-info.dolmen.smt2
+++ b/tests/smtlib/testfile-get-info1.dolmen.smt2
@@ -1,11 +1,9 @@
 (set-logic ALL)
 
 (declare-const x Int)
-(declare-const y Int)
 
 (assert (= (* x x) 4))
 
-(get-info :reason-unknown)
 (check-sat)
 (get-info :all-statistics)
 (get-info :assertion-stack-levels)
@@ -13,5 +11,4 @@
 (get-info :error-behavior)
 (get-info :name)
 (get-info :reason-unknown)
-(get-info :version)
-(get-info :foo)
\ No newline at end of file
+(get-info :version)
\ No newline at end of file
diff --git a/tests/smtlib/testfile-get-info2.err.dolmen.expected b/tests/smtlib/testfile-get-info2.err.dolmen.expected
new file mode 100644
index 000000000..2079d2e6f
--- /dev/null
+++ b/tests/smtlib/testfile-get-info2.err.dolmen.expected
@@ -0,0 +1 @@
+(error "Invalid (get-info :reason-unknown)")
diff --git a/tests/smtlib/testfile-get-info2.err.dolmen.smt2 b/tests/smtlib/testfile-get-info2.err.dolmen.smt2
new file mode 100644
index 000000000..9ae8a8ec5
--- /dev/null
+++ b/tests/smtlib/testfile-get-info2.err.dolmen.smt2
@@ -0,0 +1,8 @@
+(set-logic ALL)
+
+(declare-const x Int)
+
+(assert (= (* x x) 4))
+
+(get-info :reason-unknown)
+(check-sat)
\ No newline at end of file
diff --git a/tests/smtlib/testfile-get-info3.dolmen.expected b/tests/smtlib/testfile-get-info3.dolmen.expected
new file mode 100644
index 000000000..ad7ccf7ad
--- /dev/null
+++ b/tests/smtlib/testfile-get-info3.dolmen.expected
@@ -0,0 +1 @@
+unsupported
diff --git a/tests/smtlib/testfile-get-info3.dolmen.smt2 b/tests/smtlib/testfile-get-info3.dolmen.smt2
new file mode 100644
index 000000000..7d60bad84
--- /dev/null
+++ b/tests/smtlib/testfile-get-info3.dolmen.smt2
@@ -0,0 +1 @@
+(get-info :foo)
\ No newline at end of file
diff --git a/tests/smtlib/testfile-push-pop1.err.dolmen.expected b/tests/smtlib/testfile-push-pop1.err.dolmen.expected
index 2321d46f4..a33405c36 100644
--- a/tests/smtlib/testfile-push-pop1.err.dolmen.expected
+++ b/tests/smtlib/testfile-push-pop1.err.dolmen.expected
@@ -2,3 +2,4 @@
 unknown
 
 unknown
+(error "Error on typing errors (code 4)")