From a5ae1f9778ff863f7124454008426d5bf7c0fd71 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 29 May 2006 20:32:58 +0000 Subject: [PATCH] profilings are printed --- helm/software/components/tactics/autoTactic.ml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/helm/software/components/tactics/autoTactic.ml b/helm/software/components/tactics/autoTactic.ml index 9db6ed1c9..7aabf9f33 100644 --- a/helm/software/components/tactics/autoTactic.ml +++ b/helm/software/components/tactics/autoTactic.ml @@ -339,7 +339,12 @@ let auto_tac ?(depth=default_depth) ?(width=default_width) ?paramodulation if paramodulation_ok then ( debug_print (lazy "USO PARAMODULATION..."); (* try *) - Saturation.saturate dbd ~depth ~width ~full (proof, goal) + try + Saturation.saturate dbd ~depth ~width ~full (proof, goal) + with exn -> + prerr_endline (Saturation.get_stats ()); + raise exn + (* with ProofEngineTypes.Fail _ -> *) (* normal_auto () *) ) else -- 2.39.2