diff --git a/solver.ml b/solver.ml
index 2856931dd161a2fd78cfb85c1d4562b4e299ef36..858deba1aeca04713a1b532ef9a96612a99d8e79 100644
--- a/solver.ml
+++ b/solver.ml
@@ -108,6 +108,23 @@ let exe_path_of_solver solver =
         Ok exe
   end
 
+let string_valid_of_solver = function
+  | Pyrat -> "True"
+  | Marabou -> "\\(s\\|S\\)at\\|SAT"
+
+let string_invalid_of_solver = function
+  | Pyrat -> "False"
+  | Marabou -> "\\(u\\|U\\)nsat\\|UNSAT"
+
+let string_timeout_of_solver = function
+  | Pyrat -> "Timeout"
+  | Marabou -> "\\(t\\|T\\)imeout\\|TIMEOUT"
+
+let string_unknown_of_solver = function
+  | Pyrat -> "Unknown"
+  | Marabou -> "\\(u\\|U\\)nknown\\|UNKNOWN"
+
+
 (* Configuration. *)
 
 type version =
@@ -279,6 +296,15 @@ let detect ~file =
 
 (* Verification. *)
 
+(* Verification result. *)
+type result =
+  | Valid
+  | Invalid
+  | Timeout
+  | Unknown
+  | Failure
+[@@deriving show { with_path = false }, eq]
+
 let check_availability config =
   Logs.debug
     (fun m -> m "Checking actual availability of `%a'."
@@ -342,6 +368,12 @@ let build_command ~raw_options confg_solver property model =
   end >>= fun prop ->
   (* Build actual command-line. *)
   try
+    let stdout = Filename.temp_file "output" (show_solver solver) in
+    let summary =
+      match solver with
+      | Pyrat -> None
+      | Marabou -> Some (Filename.temp_file "summary" (show_solver solver))
+    in
     let cmd =
       let exe = confg_solver.exe in
       let args =
@@ -365,14 +397,57 @@ let build_command ~raw_options confg_solver property model =
           "--property" ::  prop ::
           "--input" :: model.Model.filename ::
           "--verbosity" :: Int.to_string verbosity_level ::
+          "--summary-file" :: Option.value_exn summary ::
           raw_options
       in
-      Filename.quote_command exe args
+      Filename.quote_command ~stdout ~stderr:stdout exe args
     in
-    Ok (prop, cmd)
+    Ok (prop, cmd, (stdout, summary))
   with Failure e ->
     Error (Format.sprintf "Unexpected failure:@ %s." e)
 
+let extract_result config stdout summary =
+  Logs.info (fun m -> m "Extracting result of verification.");
+  let solver = config.solver in
+  let output =
+    let file =
+      match solver with
+      | Pyrat -> stdout
+      | Marabou -> Option.value_exn summary
+    in
+    let in_channel = Stdlib.open_in file in
+    let buf = Buffer.create 512 in
+    try
+      while true do
+        Stdlib.Buffer.add_channel buf in_channel 512;
+      done;
+      assert false
+    with End_of_file ->
+      Stdlib.close_in in_channel;
+      Buffer.contents buf
+  in
+  let regexps_result =
+    [ (string_valid_of_solver, Valid);
+      (string_invalid_of_solver, Invalid);
+      (string_timeout_of_solver, Timeout);
+      (string_unknown_of_solver, Unknown); ]
+  in
+  List.fold
+    regexps_result
+    ~init:Failure
+    ~f:(fun acc (f, result) ->
+        let regexp = Str.regexp (f solver) in
+        let found =
+          try Str.search_forward regexp output 0 >= 0
+          with Stdlib.Not_found -> false
+        in
+        if found
+        then result
+        else acc)
+
+let pretty_result fmt result =
+  Format.fprintf fmt "%s" (String.uppercase (show_result result))
+
 let exec ~raw_options config model property =
   let open Result in
   (* Check solver availability. *)
@@ -380,20 +455,30 @@ let exec ~raw_options config model property =
   (* 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 (prop, cmd, (stdout, summary)) ->
   (* Execute the command. *)
   begin
+    Logs.app (fun m ->
+        m "Launching verification with `%a'." pp_solver config.solver);
     try
-      Logs.app
-        (fun m -> m "Launching verification with `%a'." pp_solver config.solver);
-      Logs.debug (fun m -> m "Executing command `%s'." cmd);
+      Logs.info (fun m -> m "Executing command `%s'." cmd);
       let retcode = Sys.command cmd in
-      Sys.remove tmp;
+      Sys.remove prop;
       if retcode <> 0
       then
         Error (Format.sprintf "Command `%s' failed." cmd)
-      else
+      else begin
+        (* Extract and pretty-print verification result. *)
+        let result = extract_result config stdout summary in
+        Logs.app (fun m -> m "Result: %a." pretty_result result);
+        if equal_result result Failure
+        then Logs.app (fun m ->
+            m "See error messages in `%s' for more information." stdout)
+        else Sys.remove stdout;
+        Option.value_map summary ~default:() ~f:Sys.remove;
         Ok ()
+      end
     with _ ->
       Error "Unexpected failure."
   end