diff --git a/src/bin/common/parse_command.ml b/src/bin/common/parse_command.ml
index d09cc1d02f..6582c8a519 100644
--- a/src/bin/common/parse_command.ml
+++ b/src/bin/common/parse_command.ml
@@ -324,7 +324,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
@@ -335,6 +336,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
@@ -496,7 +498,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 =
@@ -779,6 +781,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 = \
@@ -788,7 +794,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 e28f6e33ff..0f4c8bb353 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
@@ -104,7 +130,7 @@ let main () =
         Some partial_model
       | `Unsat -> None
     with Util.Timeout ->
-      if not (Options.get_timelimit_per_goal()) then exit 142;
+      if not (Options.get_timelimit_per_goal()) then exit_as_timeout ();
       None
   in
 
@@ -182,14 +208,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): display 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
@@ -203,9 +233,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
       end
     in
 
@@ -219,7 +253,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 =
@@ -250,21 +284,18 @@ 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
-    | Errors.Error e ->
-      Printer.print_err "%a" Errors.report e;
-      exit 1
+      exit_as_timeout ()
+    | Errors.Error e -> recoverable_error "%a" Errors.report e; st
     | _ 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 =
@@ -273,8 +304,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 =
@@ -348,7 +380,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
 
@@ -369,9 +402,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
@@ -403,11 +438,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) =
@@ -417,8 +450,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 ()
@@ -434,7 +466,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" ->
@@ -443,11 +481,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 :
@@ -541,15 +577,13 @@ 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
-              "Model generation disabled (try --produce-models)";
-            st
-          end
+          (* TODO: add the location of the statement. *)
+          let () =
+            recoverable_error "Model generation disabled (try --produce-models)"
+          in
+          st
 
       | {contents = `Get_info kind; _ } ->
         handle_get_info st kind;
@@ -611,7 +645,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 3e68fe6238..4ec89aaa54 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 8895a8809e..cb729dfbb6 100644
--- a/src/lib/util/options.ml
+++ b/src/lib/util/options.ml
@@ -302,14 +302,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 f146f33d07..4b42895b52 100644
--- a/src/lib/util/options.mli
+++ b/src/lib/util/options.mli
@@ -359,6 +359,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
@@ -658,6 +661,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/tests/cram.t/run.t b/tests/cram.t/run.t
index 187dc2748c..521b07e6cb 100644
--- a/tests/cram.t/run.t
+++ b/tests/cram.t/run.t
@@ -50,21 +50,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 --frontend dolmen -i smtlib2 -o smtlib2
+  $ echo '(get-model)' | alt-ergo --frontend dolmen -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 --frontend dolmen --sat-solver Tableaux -i smtlib2 -o smtlib2
+  $ echo '(get-model)' | alt-ergo --frontend dolmen --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 --frontend dolmen --produce-models -i smtlib2 -o smtlib2
+  $ echo '(get-model)' | alt-ergo --frontend dolmen --produce-models -i smtlib2 -o smtlib2 --continue-on-error
   (error "No model produced.")
 
-  $ echo '(set-option :produce-models true)(get-model)' | alt-ergo --frontend dolmen --sat-solver Tableaux -i smtlib2 -o smtlib2
+  $ echo '(set-option :produce-models true)(get-model)' | alt-ergo --frontend dolmen --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`):
diff --git a/tests/dune.inc b/tests/dune.inc
index ffbb781854..325c2fc323 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))
@@ -192457,14 +192436,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
@@ -192473,11 +192452,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
 
@@ -203168,7 +203147,70 @@
     (alias runtest-quick)
      (package alt-ergo)
       (action
-       (diff testfile-push-pop1.err.dolmen.expected testfile-push-pop1.err.dolmen_dolmen.output))))
+       (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))))
 ; Auto-generated part end
 ; File auto-generated by gentests
 
diff --git a/tests/models/issues/719.models.err.expected b/tests/models/issues/719.models.err.expected
new file mode 100644
index 0000000000..1b1ed6e846
--- /dev/null
+++ b/tests/models/issues/719.models.err.expected
@@ -0,0 +1,3 @@
+
+unsat
+(error "No model produced.")
diff --git a/tests/models/issues/719.models.err.smt2 b/tests/models/issues/719.models.err.smt2
new file mode 100644
index 0000000000..66c07f37cf
--- /dev/null
+++ b/tests/models/issues/719.models.err.smt2
@@ -0,0 +1,19 @@
+(set-logic ALL)
+(set-option :produce-models true)
+(declare-const a (Array Int Int))
+(declare-const s Int)
+(assert (and (<= 0 s) (<= s 10)))
+(assert (forall ((k Int)) (=> (and (<= 0 k) (< k s)) (<= (select a k) (select a s)))))
+(assert (forall ((k Int)) (=> (and (< s k) (<= k 10)) (<= (select a s) (select a k)))))
+(assert (
+  forall ((p Int) (q Int))
+    (=> (and (<= 0 p) (< p q) (<= q (- s 1))) (<= (select a p) (select a q)))))
+(assert (
+  forall ((p Int) (q Int))
+    (=> (and (<= (+ s 1) p) (< p q) (<= q 10)) (<= (select a p) (select a q)))))
+(assert (not (
+  forall ((p Int) (q Int))
+    (=> (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/smtlib/testfile-get-info1.dolmen.expected b/tests/smtlib/testfile-get-info1.dolmen.expected
new file mode 100644
index 0000000000..ac5fd363b1
--- /dev/null
+++ b/tests/smtlib/testfile-get-info1.dolmen.expected
@@ -0,0 +1,11 @@
+
+unknown
+unsupported
+
+unsupported
+
+(:authors "Alt-Ergo developers")
+(:error-behavior immediate-exit)
+(:name "Alt-Ergo")
+(:reason-unknown Incomplete)
+(:version dev)
diff --git a/tests/smtlib/testfile-get-info1.dolmen.smt2 b/tests/smtlib/testfile-get-info1.dolmen.smt2
new file mode 100644
index 0000000000..b7f2454f34
--- /dev/null
+++ b/tests/smtlib/testfile-get-info1.dolmen.smt2
@@ -0,0 +1,14 @@
+(set-logic ALL)
+
+(declare-const x Int)
+
+(assert (= (* x x) 4))
+
+(check-sat)
+(get-info :all-statistics)
+(get-info :assertion-stack-levels)
+(get-info :authors)
+(get-info :error-behavior)
+(get-info :name)
+(get-info :reason-unknown)
+(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 0000000000..2079d2e6f5
--- /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 0000000000..9ae8a8ec5f
--- /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 0000000000..ad7ccf7ada
--- /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 0000000000..7d60bad84e
--- /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 2321d46f4d..a33405c36e 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)")