Consider raw options as a string list rather than a mere string.

main.ml

@@ -67,7 +67,7 @@ let verify cmd raw_options config_file model property solver () =
     Model.build ~filename:model >>= fun model ->
     Property.build ~filename:property >>= fun property ->
     Solver.get_config solver ~file:config_file >>= fun config ->
-    Solver.exec ?raw_options config model property
+    Solver.exec ~raw_options config model property
   in
   match do_verify () with
   | Ok () -> Logs.app (fun m -> m "Done.")
@@ -144,7 +144,8 @@ let verify_cmd =
   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)
+    Arg.(value & opt (list ~sep:' ' string) []
+         & info ["raw"; "raw-options"] ~doc)
   in
   let config_filename =
     let doc = "$(b,FILE) to read the configuration from." in

solver.ml

@@ -286,7 +286,7 @@ let check_compatibility config model =
   | _ ->
     Ok ()
 
-let build_command ?raw_options confg_solver property model =
+let build_command ~raw_options confg_solver property model =
   let module Filename = Caml.Filename in
   let open Result in
   let solver = confg_solver.solver in
@@ -307,46 +307,44 @@ let build_command ?raw_options confg_solver property model =
   (* Build actual command-line. *)
   try
     let cmd =
-      let raw_options = Option.to_list raw_options in
       let exe = confg_solver.exe in
-      match solver with
-      | Pyrat ->
-        let verbose =
-          match Logs.level () with
-          | None | Some (App | Error | Warning) -> false
-          | Some (Info | Debug) -> true
-        in
-        Filename.quote_command
-          exe
-          (model.Model.filename ::
-           prop ::
-           if verbose then "--verbose" :: raw_options else raw_options)
-      | Marabou ->
-        let verbosity_level =
-          match Logs.level () with
-          | None | Some (App | Error | Warning) -> 0
-          | Some Info -> 1
-          | Some Debug -> 2
-        in
-        Filename.quote_command
-          exe
-          ("--property" ::  prop ::
-           "--input" :: model.Model.filename ::
-           "--verbosity" :: Int.to_string verbosity_level ::
-           raw_options)
+      let args =
+        match solver with
+        | Pyrat ->
+          let verbose =
+            match Logs.level () with
+            | None | Some (App | Error | Warning) -> false
+            | Some (Info | Debug) -> true
+          in
+          model.Model.filename ::
+          prop ::
+          if verbose then "--verbose" :: raw_options else raw_options
+        | Marabou ->
+          let verbosity_level =
+            match Logs.level () with
+            | None | Some (App | Error | Warning) -> 0
+            | Some Info -> 1
+            | Some Debug -> 2
+          in
+          "--property" ::  prop ::
+          "--input" :: model.Model.filename ::
+          "--verbosity" :: Int.to_string verbosity_level ::
+          raw_options
+      in
+      Filename.quote_command exe args
     in
     Ok (prop, cmd)
   with Failure e ->
     Error (Format.sprintf "Unexpected failure@ `%s'." e)
 
-let exec ?raw_options config model property =
+let exec ~raw_options config model property =
   let open Result in
   (* Check solver availability. *)
   check_availability config >>= fun () ->
   (* Check solver and model compatibility. *)
   check_compatibility config model >>= fun () ->
   (* Build the required command-line. *)
-  build_command ?raw_options config property model >>= fun (tmp, cmd) ->
+  build_command ~raw_options config property model >>= fun (tmp, cmd) ->
   (* Execute the command. *)
   begin
     try

solver.mli

@@ -23,9 +23,9 @@ type config
     the given [file]. *)
 val get_config: file:string -> solver -> (config, string) Result.t
 
-(** [exec ?raw_options config model property] runs a solver wrt the given
+(** [exec ~raw_options config model property] runs a solver wrt the given
     [config] on [property] for [model] with the provided [raw_options], if any.
 *)
 val exec:
-  ?raw_options:string ->
+  raw_options:string list ->
   config -> Model.t -> Property.t -> (unit, string) Result.t