review changes

src/bin/common/solving_loop.ml

@@ -32,7 +32,7 @@ module DO = D_state_option
 module Sy = Symbols
 module O = Options
 
-exception Exit_on_error of int
+exception Exit_with_code of int
 
 type solver_ctx = {
   ctx    : Commands.sat_tdecl list;
@@ -60,13 +60,13 @@ let recoverable_error ?(code = 1) =
           | Smtlib2 _ -> Printer.print_smtlib_err "%s" msg
           | _ -> Printer.print_err "%s" msg
       in
-      if Options.get_exit_on_error () then raise (Exit_on_error code))
+      if Options.get_exit_on_error () then raise (Exit_with_code code))
 
 let fatal_error ?(code = 1) =
   Format.kasprintf
     (fun msg ->
        recoverable_error ~code "%s" msg;
-       raise (Exit_on_error code))
+       raise (Exit_with_code code))
 
 let exit_as_timeout () = fatal_error ~code:142 "timeout"
 
@@ -257,7 +257,7 @@ let process_source ?selector_inst ~print_status src =
     | Errors.Error e ->
       recoverable_error "%a" Errors.report e;
       st
-    | Exit -> raise (Exit_on_error 0)
+    | Exit -> raise (Exit_with_code 0)
     | _ as exn -> Printexc.raise_with_backtrace exn bt
   in
   let finally ~handle_exn st e =
@@ -902,4 +902,4 @@ let main () =
       process_source ~print_status:Frontend.print_status `Stdin
     else
       process_source ~print_status:Frontend.print_status @@ (`File path)
-  with Exit_on_error code -> exit code
+  with Exit_with_code code -> exit code

src/bin/common/solving_loop.mli

@@ -25,7 +25,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-exception Exit_on_error of int
+exception Exit_with_code of int
 (** Exception raised to notify that [process_source] cannot continue.
     The integer corresponds to an error code. *)
 
@@ -42,5 +42,6 @@ val process_source :
     input source [src] and call [print_status] on each answers.
     The hook [selector_inst] allows to track generated instantiations.
 
-    @raise Exit_on_error if a fatal error occurs. Recovarable errors
-           raise this exception if [Options.get_exit_on_error ()] is [true]. *)
+    @raise Exit_with_code c with c <> 0 if a fatal error occurs.
+           Recovarable errors raise this exception if
+           [Options.get_exit_on_error ()] is [true]. *)

src/bin/js/worker_js.ml

@@ -146,7 +146,7 @@ let main worker_id filename filecontent =
       Worker_interface.diagnostic =
         Some [Format.asprintf "%a" Errors.report e]
     }
-  | Solving_loop.Exit_on_error code ->
+  | Solving_loop.Exit_with_code code ->
     let res = Worker_interface.init_results () in
     let msg = Fmt.str "exit code %d" code in
     { res with

src/lib/structures/errors.ml

@@ -82,7 +82,6 @@ type run_error =
   | Unsupported_feature of string
   | Dynlink_error of string
   | Stack_underflow
-  | Exit_on_error of int
 
 type mode_error =
   | Invalid_set_option of string
@@ -251,8 +250,6 @@ let report_run_error fmt = function
     fprintf fmt "[Dynlink] %s" s
   | Stack_underflow ->
     fprintf fmt "The stack of the assertion levels is empty"
-  | Exit_on_error code ->
-    Fmt.pf fmt "error code %d" code
 
 let report_mode_error fmt = function
   | Invalid_set_option s ->

src/lib/structures/errors.mli

@@ -89,7 +89,6 @@ type run_error =
   | Unsupported_feature of string
   | Dynlink_error of string
   | Stack_underflow
-  | Exit_on_error of int
 
 (** Errors raised when performing actions forbidden in some modes. *)
 type mode_error =