diff --git a/src/core/Internal.ml b/src/core/Internal.ml
index 03511c7d..bb2d52b7 100644
--- a/src/core/Internal.ml
+++ b/src/core/Internal.ml
@@ -712,7 +712,11 @@ module Make(Plugin : PLUGIN)
       Stack.push (Enter p) s;
       fold_aux s h f acc
 
-    let check p = fold (fun () _ -> ()) () p
+    let check (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
   end
   type proof = Proof.t