From a2809215ae7c215ffae4c072d33fd68478986602 Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Thu, 4 Feb 2016 23:51:53 +0100
Subject: [PATCH] Update the binary for better output when checking proofs

---
 main.ml             | 20 ++++++++++++--------
 util/parsedimacs.ml |  1 +
 2 files changed, 13 insertions(+), 8 deletions(-)

diff --git a/main.ml b/main.ml
index deb7b1ee..d602410f 100644
--- a/main.ml
+++ b/main.ml
@@ -228,19 +228,21 @@ let main () =
     Gc.delete_alarm al;
     begin match res with
       | Smt.Sat ->
-        print "Sat (%f)" (Sys.time ());
+        let t = Sys.time () in
         if !p_check then
           if not (List.for_all (List.exists Smt.eval) cnf) then
-            raise Incorrect_model
+            raise Incorrect_model;
+        print "Sat (%f/%f)" t (Sys.time () -. t)
       | Smt.Unsat ->
-        print "Unsat (%f)" (Sys.time ());
+        let t = Sys.time () in
         if !p_check then begin
           let p = Smt.get_proof () in
           Smt.Proof.check p;
           print_proof p;
           if !p_unsat_core then
             print_unsat_core (Smt.unsat_core p)
-        end
+        end;
+        print "Unsat (%f/%f)" t (Sys.time () -. t)
     end
   | Mcsat ->
     Mcsat.assume cnf;
@@ -248,19 +250,21 @@ let main () =
     Gc.delete_alarm al;
     begin match res with
       | Mcsat.Sat ->
-        print "Sat (%f)" (Sys.time ());
+        let t = Sys.time () in
         if !p_check then
           if not (List.for_all (List.exists Mcsat.eval) cnf) then
-            raise Incorrect_model
+            raise Incorrect_model;
+        print "Sat (%f/%f)" t (Sys.time () -. t)
       | Mcsat.Unsat ->
-        print "Unsat (%f)" (Sys.time ());
+        let t = Sys.time () in
         if !p_check then begin
           let p = Mcsat.get_proof () in
           Mcsat.Proof.check p;
           print_mcproof p;
           if !p_unsat_core then
             print_mc_unsat_core (Mcsat.unsat_core p)
-        end
+        end;
+        print "Unsat (%f/%f)" t (Sys.time () -. t)
     end
 
 let () =
diff --git a/util/parsedimacs.ml b/util/parsedimacs.ml
index cde0f4cf..df5c3c8c 100644
--- a/util/parsedimacs.ml
+++ b/util/parsedimacs.ml
@@ -21,6 +21,7 @@ let rec _read_word s acc i len =
       let acc = String.sub s i len :: acc in
       _skip_space s acc (i+len+1)
     | _ -> _read_word s acc i (len+1)
+
 and _skip_space s acc i =
   if i=String.length s
   then acc