From 92ca9c328f730d43460106989ebf489a44873bea Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Sat, 16 Feb 2019 12:16:00 -0600
Subject: [PATCH] refactor(main): catch resolution errors properly; style

---
 src/main/main.ml | 17 +++++++++++------
 1 file changed, 11 insertions(+), 6 deletions(-)

diff --git a/src/main/main.ml b/src/main/main.ml
index 8822b501..be123efb 100644
--- a/src/main/main.ml
+++ b/src/main/main.ml
@@ -48,14 +48,16 @@ module Process() = struct
         let t' = Sys.time () -. t in
         Format.printf "Sat (%f/%f)@." t t'
       | S.Unsat state ->
-        if !p_check then begin
+        if !p_check then (
           let p = state.Msat.get_proof () in
           S.Proof.check p;
-          if !p_dot_proof <> "" then begin
-            let fmt = Format.formatter_of_out_channel (open_out !p_dot_proof) in
-            D.pp fmt p
-          end
-        end;
+          if !p_dot_proof <> "" then (
+            let oc = open_out !p_dot_proof in
+            let fmt = Format.formatter_of_out_channel oc in
+            Format.fprintf fmt "%a@?" D.pp p;
+            flush oc; close_out_noerr oc;
+          )
+        );
         let t' = Sys.time () -. t in
         Format.printf "Unsat (%f/%f)@." t t'
     end
@@ -171,4 +173,7 @@ let () =
   | Incorrect_model ->
     Format.printf "Internal error : incorrect *sat* model@.";
     exit 4
+  | S.Proof.Resolution_error msg  ->
+    Format.printf "Internal error: incorrect *unsat* proof:\n%s@." msg;
+    exit 5