diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml
index 885b12cc0b..6514dbb52b 100644
--- a/src/bin/common/solving_loop.ml
+++ b/src/bin/common/solving_loop.ml
@@ -290,7 +290,9 @@ let main () =
     | Util.Timeout ->
       Printer.print_status_timeout None None None None;
       exit_as_timeout ()
-    | Errors.Error e -> recoverable_error "%a" Errors.report e; st
+    | 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 =
@@ -560,6 +562,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
diff --git a/src/lib/util/printer.ml b/src/lib/util/printer.ml
index 983cbaa674..b4e6641e33 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 b89d125c07..26b3c60519 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
@@ -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/everything/testfile-smt-instr-get-info.dolmen.expected b/tests/everything/testfile-smt-instr-get-info.dolmen.expected
deleted file mode 100644
index d3e05dee0c..0000000000
--- a/tests/everything/testfile-smt-instr-get-info.dolmen.expected
+++ /dev/null
@@ -1,13 +0,0 @@
-(error "Invalid (get-info :reason-unknown)")
-
-unknown
-unsupported
-
-unsupported
-
-(:authors "Alt-Ergo developers")
-(:error-behavior immediate-exit)
-(:name "Alt-Ergo")
-(:reason-unknown Incomplete)
-(:version dev)
-unsupported
diff --git a/tests/everything/testfile-smt-instr-get-info.dolmen.smt2 b/tests/everything/testfile-smt-instr-get-info.dolmen.smt2
deleted file mode 100644
index 4fd233ce50..0000000000
--- a/tests/everything/testfile-smt-instr-get-info.dolmen.smt2
+++ /dev/null
@@ -1,17 +0,0 @@
-(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)
-(get-info :authors)
-(get-info :error-behavior)
-(get-info :name)
-(get-info :reason-unknown)
-(get-info :version)
-(get-info :foo)
\ No newline at end of file
diff --git a/tests/models/issues/719.models.expected b/tests/models/issues/719.models.expected
deleted file mode 100644
index 1b1ed6e846..0000000000
--- a/tests/models/issues/719.models.expected
+++ /dev/null
@@ -1,3 +0,0 @@
-
-unsat
-(error "No model produced.")
diff --git a/tests/models/issues/719.models.smt2 b/tests/models/issues/719.models.smt2
deleted file mode 100644
index d717b2e509..0000000000
--- a/tests/models/issues/719.models.smt2
+++ /dev/null
@@ -1,18 +0,0 @@
-(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)