Newline at the beginning of smt printing and fix tests

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

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

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)")