Register custom printers for the used exceptions in order to display clean error messages.

src/main.ml

@@ -215,6 +215,15 @@ let default_info =
 
 let default_cmd = Term.(ret (const (fun _ -> `Help (`Pager, None)) $ const ()))
 
+let () =
+  (* We register custom printers for a selection of exceptions otherwise Why3
+     will print the related messages as "anomaly: <exception with message>". *)
+  Why3.Exn_printer.register (fun fmt exn ->
+    match exn with
+    | Invalid_argument msg -> Fmt.pf fmt "Invalid argument: %s" msg
+    | Failure msg -> Fmt.pf fmt "Failure: %s" msg
+    | _ -> raise exn)
+
 let () =
   try
     Cmd.group ~default:default_cmd default_info [ config_cmd; verify_cmd ]

src/verification.ml

@@ -77,7 +77,7 @@ let answer_saver limit config task env prover dataset_csv =
   let handle_task_saver task env dataset_csv command =
     let dataset_filename =
       match dataset_csv with
-      | None -> failwith "Error, no dataset provided for SAVer."
+      | None -> invalid_arg "No dataset provided for SAVer"
       | Some s -> s
     in
     let goal = Task.task_goal_fmla task in
@@ -104,13 +104,14 @@ let answer_saver limit config task env prover dataset_csv =
             let svm_filename =
               match Language.lookup_loaded_svms svm_app_sym with
               | Some t -> t.filename
-              | None -> failwith "SVM file not found in environment."
+              | None -> invalid_arg "No SVM model found in task"
             in
             (eps, svm_filename)
-          else failwith "Wrong predicate found."
-        (* no other predicate than robust_to is supported *)
-        | _ -> failwith "Unsupported by SAVer.")
-      | _ -> failwith "Unsupported by SAVer."
+          else failwith "Wrong predicate found"
+        | _ ->
+          (* no other predicate than robust_to is supported *)
+          failwith "Unsupported predicate by SAVer")
+      | _ -> failwith "Unsupported predicate by SAVer"
     in
     let svm_file = Unix.realpath svm_filename in
     let dataset_file = Unix.realpath dataset_filename in
@@ -175,7 +176,7 @@ let answer_generic limit config task driver (prover : Whyconf.config_prover) =
     match Task.on_meta_excl Native_nn_prover.meta_nn_filename task_prepared with
     | Some [ MAstr nn_file ] -> nn_file
     | Some _ -> assert false (* By construction of the meta. *)
-    | None -> invalid_arg (Fmt.str "No neural network model found in task")
+    | None -> invalid_arg "No neural network model found in task"
   in
   let nn_file = Unix.realpath nn_file in
   let command = Re__Core.replace_string nnet_or_onnx ~by:nn_file command in