feat: Proof.check_empty_conclusion as a separate function

this allows the validity checking of proofs of 0-level lits

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
 

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

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