nasty change in the lexer/parser:

[helm.git] / helm / software / components / tactics / paramodulation / saturation.ml

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index be3d21aa141e07b43628ffd594a8596a40fd1aa0..c5f3132e9aa5e5e1cb56849862f78e09175f0aed 100644 (file)
--- 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
 ;;