From 7776b6e2f05d49b4a74efe3f7f0f08013876ad1e Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Wed, 15 Feb 2017 14:03:10 +0100
Subject: [PATCH] Fix use of asprintf (missing in 4.00.1)

---
 src/core/res.ml | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/src/core/res.ml b/src/core/res.ml
index d5601523..fdf391da 100644
--- a/src/core/res.ml
+++ b/src/core/res.ml
@@ -19,7 +19,7 @@ module Make(St : Solver_types.S) = struct
   exception Resolution_error of string
 
   (* Log levels *)
-  (* let error = 1 *)
+  let error = 1
   let warn = 3
   let info = 10
   let debug = 80
@@ -132,8 +132,8 @@ module Make(St : Solver_types.S) = struct
         c'
       end
     | _ ->
-      raise (Resolution_error
-               (Format.asprintf "Cannot prove atom %a" St.pp_atom a))
+      Log.debugf error "Error while proving atom %a" (fun k -> k St.pp_atom a);
+      raise (Resolution_error "Cannot prove atom")
 
   let prove_unsat conflict =
     if Array.length conflict.St.atoms = 0 then conflict
@@ -179,9 +179,9 @@ module Make(St : Solver_types.S) = struct
               chain_res (new_clause, l) r
           end
         | _ ->
-          raise (Resolution_error (
-              Format.asprintf "Cannot resolve the clauses: %a && %a"
-                St.pp_clause c St.pp_clause d))
+          Log.debugf error "While resolving clauses:@[<hov>%a@\n%a@]"
+            (fun k -> k St.pp_clause c St.pp_clause d);
+          raise (Resolution_error "Clause mismatch")
       end
     | _ ->
       raise (Resolution_error "Bad history")
@@ -196,8 +196,8 @@ module Make(St : Solver_types.S) = struct
     | St.Local ->
       { conclusion; step = Assumption; }
     | St.History [] ->
-      raise (Resolution_error (
-          Format.asprintf "Empty history for %a" St.pp_clause conclusion))
+      Log.debugf error "Empty history for clause: %a" (fun k -> k St.pp_clause conclusion);
+      raise (Resolution_error "Empty history")
     | St.History [ c ] ->
       let duplicates, res = analyze (list c) in
       assert (cmp_cl res (list conclusion) = 0);