diff --git a/main.ml b/main.ml
index 9ff0112062091d553f8210386a378c47c2d21cee..3f2da3a8ddd093b56d461b03d5aaf8953974e25b 100644
--- a/main.ml
+++ b/main.ml
@@ -52,7 +52,7 @@ let verify cmd model property solver raw_options () =
     let open Result in
     Model.build ~filename:model >>= fun model ->
     Property.build ~filename:property >>= fun property ->
-    Solver.exec ?raw_options solver property model
+    Solver.exec ?raw_options solver model property
   in
   match do_verify () with
   | Ok () -> Logs.app (fun m -> m "Done.")
@@ -88,18 +88,18 @@ let verify_cmd =
   let docv_model = "MODEL" in
   let model =
     let doc = "The $(b,filename) of a neural network model." in
-    Arg.(required & pos 1 (some file) None & info [] ~docv:docv_model ~doc)
+    Arg.(required & pos 0 (some file) None & info [] ~docv:docv_model ~doc)
   in
   let docv_property = "PROPERTY" in
   let property =
     let doc = "The $(b,filename) of a property to verify." in
-    Arg.(required & pos 0 (some file) None & info [] ~docv:docv_property ~doc)
+    Arg.(required & pos 1 (some file) None & info [] ~docv:docv_property ~doc)
   in
   let solver_raw_options =
     let doc = "Additional options provided to the solver." in
     Arg.(value & opt (some string) None & info ["raw"; "raw-options"] ~doc)
   in
-  let doc = "property verification of neural networks" in
+  let doc = "Property verification of neural networks." in
   let exits = Term.default_exits in
   let man = [
     `S Manpage.s_description;
@@ -115,11 +115,12 @@ let verify_cmd =
   in
   Term.(const verify
         $ const cmdname
-        $ model $ property $ solver $ solver_raw_options $ setup_logs),
+        $ model $ property $ solver
+        $ solver_raw_options $ setup_logs),
   Term.info cmdname ~sdocs:Manpage.s_common_options ~envs ~exits ~doc ~man
 
 let default_cmd =
-  let doc = "framework for neural networks property verification and more" in
+  let doc = "Framework for neural networks property verification and more." in
   let sdocs = Manpage.s_common_options in
   let man =
     [ `S Manpage.s_common_options;
diff --git a/property.ml b/property.ml
index 560006b5b2179d05973eaa008ffab2468372731a..44146733cbab7a6b8b94cd9221eda254cdbcb568 100644
--- a/property.ml
+++ b/property.ml
@@ -27,7 +27,7 @@ let do_build ~property line =
   | Property_parser.Error ->
     Error
       (Format.sprintf
-         "At offset %d: syntax error."
+         "Property syntax error at offset %d."
          (Lexing.lexeme_start linebuf))
 
 let build ~filename =
diff --git a/property_lexer.mll b/property_lexer.mll
index e6fe6d7875b921ad90af760d5f0f1c6cc9110430..14bc3f47ff03ec6a4ad2b2f7658838647b0454dd 100644
--- a/property_lexer.mll
+++ b/property_lexer.mll
@@ -53,4 +53,4 @@ and token = parse
 | '\n'
     { EOL }
 | _
-    { raise (Error (Printf.sprintf "At offset %d: unexpected character.\n" (Lexing.lexeme_start lexbuf))) }
+    { raise (Error (Printf.sprintf "Property lexer at offset %d: unexpected character.\n" (Lexing.lexeme_start lexbuf))) }
diff --git a/solver.ml b/solver.ml
index 3c7029e3024fb6a203c69da16ae3cc982f1d9858..85f52fcbd05c4c2bc1b3e85072ec55fb4e31d2c8 100644
--- a/solver.ml
+++ b/solver.ml
@@ -76,7 +76,7 @@ let check_availability solver =
         (Format.sprintf
            "Command `%s' failed.@ \
             Hint: Set either the PATH or \
-            use variable `%s' to directly provide the executable."
+            use variable `%s' to directly provide the path to the executable."
            cmd (env_var_of_solver solver))
     else begin
       (try
@@ -145,7 +145,7 @@ let build_command ?raw_options solver property model =
       Ok (tmp, cmd)
   end
 
-let exec ?raw_options solver property model =
+let exec ?raw_options solver model property =
   let open Result in
   (* Check solver availability in PATH. *)
   check_availability solver >>= fun () ->
diff --git a/solver.mli b/solver.mli
index c89f7ee3d47917ba8f8345c2291e06a5700e68eb..e85cb9cb227de09c365849c2d0f6285f27310da4 100644
--- a/solver.mli
+++ b/solver.mli
@@ -13,4 +13,4 @@ val env_vars: string list
     [model] with the provided [raw_options], if any. *)
 val exec:
   ?raw_options:string ->
-  solver -> Property.t -> Model.t -> (unit, string) Result.t
+  solver -> Model.t -> Property.t -> (unit, string) Result.t