if paramodulation_ok then (
debug_print (lazy "USO PARAMODULATION...");
(* try *)
- Saturation.saturate dbd ~depth ~width ~full (proof, goal)
+ try
+ let rc = Saturation.saturate dbd ~depth ~width ~full (proof, goal) in
+ prerr_endline (Saturation.get_stats ());
+ rc
+ with exn ->
+ prerr_endline (Saturation.get_stats ());
+ raise exn
+
(* with ProofEngineTypes.Fail _ -> *)
(* normal_auto () *)
) else