diff --git a/src/language.ml b/src/language.ml
index 09c4813a0d4a6314295ad29b37561f13c1f14c3a..6d9a186638aa5d1270848491c0e6c5280b89906d 100644
--- a/src/language.ml
+++ b/src/language.ml
@@ -244,8 +244,7 @@ let create_nn_onnx =
               Logs.warn (fun m ->
                 m "Cannot build network intermediate representation:@ %s" msg);
               None
-            | Ok nier ->
-              Some nier
+            | Ok nier -> Some nier
           in
           {
             nn_nb_inputs = n_inputs;
diff --git a/src/logging.ml b/src/logging.ml
index 78b3cfd9a8f5a9e2f8f6f12525da604e07d07368..e9642b4282b103496a3102ed0b26b41bde9f67c2 100644
--- a/src/logging.ml
+++ b/src/logging.ml
@@ -81,6 +81,9 @@ let code_error ?src f =
 
 exception User_error
 
+let info ?src f =
+  Logs.info ?src f
+
 let user_error ?src f =
   Logs.err ?src f;
   raise User_error
diff --git a/src/logging.mli b/src/logging.mli
index 7ebf4c3c0d2b0059b19927df38b52ec064779db6..417e35cb557d7fcafdbe75476c2a5daee0261cf5 100644
--- a/src/logging.mli
+++ b/src/logging.mli
@@ -38,6 +38,9 @@ val setup :
 
 val is_debug_level : Logs.src -> bool
 
+val info : ?src:Logs.src -> (_, unit) Logs.msgf -> unit
+(** Log a message to the user and continue the execution. *)
+
 val code_error : ?src:Logs.src -> (_, unit) Logs.msgf -> 'b
 (** Terminate execution with a [code error] message. *)
 
diff --git a/src/verification.ml b/src/verification.ml
index e59c1bc4c13a741996814fedae18705c54bdd78d..2fc3646614bfa90ed429877a5e4c339baa6f9c90 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -261,11 +261,10 @@ let answer_generic limit config prover config_prover driver ~proof_strategy
           | Some { nn_nier = Some g; _ } -> (
             try
               Onnx.write g f;
-              Logs.info (fun m -> m "@[Wrote ONNX file at '%s'@]" f)
+              Logging.info (fun m -> m "@[Wrote ONNX file at '%s'@]" f)
             with Sys_error msg ->
-              Logs.err (fun m ->
-                m "@[System error: tried to write ONNX file a '%s', got '%s'@]"
-                  f msg))
+              Logging.user_error (fun m ->
+                m "@[Tried to write ONNX file at '%s', got '%s'@]" f msg))
           | None -> ()
           | _ -> ()
         in
diff --git a/tests/nier_to_onnx.t b/tests/nier_to_onnx.t
index bda0cefba377507275b182601979b3ea8abf474c..8cd9fb3b9a621f8a767bc0dd0d3783dd8b7e0d1f 100644
--- a/tests/nier_to_onnx.t
+++ b/tests/nier_to_onnx.t
@@ -4,7 +4,7 @@ Test verify
   $ bin/pyrat.py --version
   PyRAT 1.1
 
-  $ caisar verify --format whyml --prover=PyRAT --onnx-out-file="out.onnx" - 2>&1 <<EOF | ./filter_tmpdir.sh
+  $ caisar verify --format whyml --prover=PyRAT -v --onnx-out-file="out.onnx" - 2>&1 <<EOF | ./filter_tmpdir.sh
   > theory NIER_to_ONNX
   >   use ieee_float.Float64
   >   use bool.Bool
@@ -21,6 +21,8 @@ Test verify
   >       (0.5:t) .< (nn@@i)[0] .< (0.5:t)
   > end
   > EOF
+  [INFO] Wrote ONNX file at 'out.onnx'
+  [INFO] Verification results for theory 'NIER_to_ONNX'
   Goal G: Unknown ()
 
 Data should be 0.135