Added an implicit parameter to branch_tac to allow branching on a

[helm.git] / helm / software / components / ng_paramodulation / paramod.ml

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index f7bc2eac9d5f237b3181fc7d42e23da39c9a4d47..0558e89c7432309155c4f07ead3c8dc794b8d88e 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -367,13 +367,15 @@ module Paramod (B : Orderings.Blob) = struct
       (List.iter
        (fun x -> 
            ignore 
-             (Sup.simplify_goal ~no_demod:true maxvar active_t bag [] x))
+            (debug (lazy("ckecking goal vs a: " ^ Pp.pp_unit_clause x));
+               Sup.simplify_goal ~no_demod:true maxvar active_t bag [] x))
        g_passives); 
       ignore
       (List.iter
         (fun x -> 
            ignore 
-             (Sup.simplify_goal ~no_demod:true maxvar passive_t bag [] x))
+             (debug (lazy("ckecking goal vs p: " ^ Pp.pp_unit_clause x));
+       Sup.simplify_goal ~no_demod:true maxvar passive_t bag [] x))
         (g_actives@g_passives)); 
     raise (Stop (Timeout (maxvar,bag)))