diff --git a/src/core/Internal.ml b/src/core/Internal.ml
index 7ff26748..12259a04 100644
--- a/src/core/Internal.ml
+++ b/src/core/Internal.ml
@@ -712,11 +712,12 @@ module Make(Plugin : PLUGIN)
       Stack.push (Enter p) s;
       fold_aux s h f acc
 
-    let check (p:t) =
+    let check_empty_conclusion (p:t) =
       if Array.length p.atoms > 0 then (
         error_res_f "@[<2>Proof.check: non empty conclusion for claus@ %a@]" Clause.debug p;
-      );
-      fold (fun () _ -> ()) () p
+      )
+
+    let check (p:t) = fold (fun () _ -> ()) () p
   end
   type proof = Proof.t
 
diff --git a/src/core/Solver_intf.ml b/src/core/Solver_intf.ml
index e7d48900..e099485f 100644
--- a/src/core/Solver_intf.ml
+++ b/src/core/Solver_intf.ml
@@ -349,8 +349,12 @@ module type PROOF = sig
 
   (** {3 Misc} *)
 
+  val check_empty_conclusion : t -> unit
+  (** Check that the proof's conclusion is the empty clause,
+      @raise Resolution_error otherwise *)
+
   val check : t -> unit
-  (** Check the contents of a proof. Mainly for internal use *)
+  (** Check the contents of a proof. Mainly for internal use. *)
 
   module Tbl : Hashtbl.S with type key = t
 end
diff --git a/src/main/main.ml b/src/main/main.ml
index be123efb..a8988f48 100644
--- a/src/main/main.ml
+++ b/src/main/main.ml
@@ -50,6 +50,7 @@ module Process() = struct
       | S.Unsat state ->
         if !p_check then (
           let p = state.Msat.get_proof () in
+          S.Proof.check_empty_conclusion p;
           S.Proof.check p;
           if !p_dot_proof <> "" then (
             let oc = open_out !p_dot_proof in