X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fsaturation.ml;h=c5f3132e9aa5e5e1cb56849862f78e09175f0aed;hb=e78cf74f8976cf0ca554f64baa9979d0423ee927;hp=be3d21aa141e07b43628ffd594a8596a40fd1aa0;hpb=25564c06c570e5ab9be455904c0b381842f8d4c4;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index be3d21aa1..c5f3132e9 100644
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -1195,9 +1195,15 @@ let add_to_active bag active passive env ty term newmetas =
    | Some eq_uri -> 
        try 
          let bag, current = Equality.equality_of_term bag term ty newmetas in
-         let bag, current = Equality.fix_metas bag current in
-         match add_to_active_aux bag active passive env eq_uri current with
-         | _,a,p,b -> a,p,b
+         let w,_,_,_,_ = Equality.open_equality current in
+         if w > 100 then 
+           (HLog.debug 
+             ("skipping giant " ^ CicPp.ppterm term ^ " of weight " ^
+                string_of_int w); active, passive, bag)
+         else
+          let bag, current = Equality.fix_metas bag current in
+          match add_to_active_aux bag active passive env eq_uri current with
+          | _,a,p,b -> a,p,b
        with
        | Equality.TermIsNotAnEquality -> active, passive, bag
 ;;