diff --git a/solver.ml b/solver.ml
index 85f52fcbd05c4c2bc1b3e85072ec55fb4e31d2c8..0a609ad3996943ce114e3f0d2578f82615b638be 100644
--- a/solver.ml
+++ b/solver.ml
@@ -34,10 +34,12 @@ let rec pp_property_marabou property =
     let s2 = pp_property_marabou p2 in
     Format.sprintf "%s\n%s" s1 s2
 
+let pp_property_pyrat = pp_property_marabou
+
 let pp_property solver property =
   match solver with
   | Pyrat ->
-    Error "Not implemented yet."
+    Ok (pp_property_pyrat property)
   | Marabou ->
     Ok (pp_property_marabou property)
 
@@ -45,7 +47,7 @@ let env_var_of_solver solver = String.uppercase (show_solver solver ^ "_exe")
 let env_vars = List.map ~f:env_var_of_solver [ Pyrat; Marabou ]
 
 let default_exe_name_of_solver = function
-  | Pyrat -> "pyrat"
+  | Pyrat -> "pyrat.py"
   | Marabou -> "Marabou"
 
 let exe_name_of_solver solver =
@@ -97,7 +99,7 @@ let check_availability solver =
 
 let check_compatibility solver model =
   match solver, model.Model.format with
-  | Marabou, (Model.Onnx as f) ->
+  | (Pyrat | Marabou), (Model.Onnx as f) ->
     Error
       (Format.sprintf
          "Cannot deal with `%s' and model format `%s'."
@@ -122,11 +124,22 @@ let build_command ?raw_options solver property model =
       Ok tmp
     with Sys_error e ->
       Error (Format.sprintf "Unexpected failure@ `%s'." e)
-  end >>= fun tmp ->
+  end >>= fun prop ->
   (* Build actual command-line. *)
-  begin match solver with
+  let cmd =
+    let raw_options = Option.to_list raw_options in
+    match solver with
     | Pyrat ->
-      Error "Not implemented yet."
+      let verbose =
+        match Logs.level () with
+        | None | Some (App | Error | Warning) -> false
+        | Some (Info | Debug) -> true
+      in
+      Filename.quote_command
+        (exe_name_of_solver solver)
+        (model.Model.filename ::
+         prop ::
+         if verbose then "--verbose" :: raw_options else raw_options)
     | Marabou ->
       let verbosity_level =
         match Logs.level () with
@@ -134,16 +147,14 @@ let build_command ?raw_options solver property model =
         | Some Info -> 1
         | Some Debug -> 2
       in
-      let cmd =
-        Filename.quote_command
-          (exe_name_of_solver solver)
-          ("--property" ::  tmp ::
-           "--input" :: model.Model.filename ::
-           "--verbosity" :: Int.to_string verbosity_level ::
-           Option.to_list raw_options)
-      in
-      Ok (tmp, cmd)
-  end
+      Filename.quote_command
+        (exe_name_of_solver solver)
+        ("--property" ::  prop ::
+         "--input" :: model.Model.filename ::
+         "--verbosity" :: Int.to_string verbosity_level ::
+         raw_options)
+  in
+  Ok (prop, cmd)
 
 let exec ?raw_options solver model property =
   let open Result in