[SAVer] Modified comment.

src/language.ml

@@ -7,8 +7,8 @@
 open Why3
 open Base
 
-(* -- Support for the NNet and ONNX neural network formats, as well as SVM under
-   the .ovo format *)
+(* Support for several model formats: - NNet and ONNX for neural networks, - OVO
+   for for SVM *)
 
 type nnshape = {
   nb_inputs : int;
@@ -57,7 +57,8 @@ let register_svm nb_inputs nb_outputs filename env =
   let ls_svm_apply =
     Term.create_fsymbol
       (Ident.id_fresh "svm_apply")
-      [] (Ty.ty_func asarray_input_type asarray_input_type)
+      []
+      (Ty.ty_func asarray_input_type asarray_input_type)
   in
   Why3.Term.Hls.add loaded_svms ls_svm_apply
     { filename; nb_inputs; nb_outputs; ty_data = asarray_input_type };

src/verification.ml

@@ -87,7 +87,7 @@ 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 -> failwith "SVM file not found in environment."
             in
             (eps, svm_filename)
           else failwith "Wrong predicate found."
@@ -136,9 +136,8 @@ let answer_saver limit config task env prover dataset_csv =
         then Call_provers.Valid
         else Call_provers.Invalid
       | None -> Call_provers.HighFailure
-      (* Any other answer than HighFailure should
-       * never happen as we do not define
-       * anything in SAVer's driver *))
+      (* Any other answer than HighFailure should never happen as we do not
+         define anything in SAVer's driver *))
     | _ -> assert false
   in
   answer