New unification and new matching.

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

diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml
index b3fa5f3fcd955d283fede4fef9ef6eea912a1edf..b6678683d5d73688473e9d91b9849d429030df57 100644 (file)
--- a/components/tactics/paramodulation/saturation.ml
+++ b/components/tactics/paramodulation/saturation.ml
@@ -468,8 +468,12 @@ let infer env sign current (active_list, active_table) =
               let neg, pos = infer_positive table tl in
               neg, res @ pos
         in
+        let maxm, copy_of_current = Inference.fix_metas !maxmeta current in
+        maxmeta := maxm;
         let curr_table = Indexing.index Indexing.empty current in
-        let neg, pos = infer_positive curr_table active_list in
+        let neg, pos = 
+         infer_positive curr_table ((sign,copy_of_current)::active_list) 
+       in
          if Utils.debug_metas then 
            ignore(List.map 
                     (function current -> 
@@ -1774,7 +1778,7 @@ and given_clause_fullred_aux dbd env goals theorems passive active =
                  " LOCALMAX: " ^ string_of_int !Indexing.local_max ^
                 " #ACTIVES: " ^ string_of_int (size_of_active active) ^
                  " #PASSIVES: " ^ string_of_int (size_of_passive passive));
-  if (size_of_active active) mod 54 = 0 then
+  if (size_of_active active) mod 50 = 0 then
     (let s = Printf.sprintf "actives:\n%s\n"
       (String.concat "\n"
          ((List.map
@@ -1828,6 +1832,7 @@ and given_clause_fullred_aux dbd env goals theorems passive active =
       forward_simpl_time := !forward_simpl_time +. (time2 -. time1);
       match res with
       | None ->
+          (* weight_age_counter := !weight_age_counter + 1; *)
           given_clause_fullred dbd env goals theorems passive active
       | Some (sign, current) ->
           if (sign = Negative) && (is_identity env current) then (