Fixed nasty bug in maxvar updating

[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 4968d3290030c7e1b47441bf79d2b9242006db7f..d0129279065f1ec620d4aa9d824a6fa978f301b0 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -6,7 +6,7 @@ let debug s =
 
 let nparamod rdb metasenv subst context t table =
   let max_nb_iter = 999999999 in
-  let amount_of_time = 10.0 in
+  let amount_of_time = 300.0 in
   let module C = struct
     let metasenv = metasenv
     let subst = subst
@@ -42,12 +42,11 @@ let nparamod rdb metasenv subst context t table =
   in
   let rec given_clause bag maxvar actives      
       passives g_actives g_passives =
-    
-    incr nb_iter; if !nb_iter = max_nb_iter then 
-      (*(prerr_endline "Bag :"; prerr_endline (Pp.pp_bag bag);
+    (* prerr_endline "Bag :"; prerr_endline (Pp.pp_bag bag);
       prerr_endline "Active table :"; 
        (List.iter (fun x -> prerr_endline (Pp.pp_unit_clause x))
-         (fst actives));*)
+         (fst actives)); *)
+    incr nb_iter; if !nb_iter = max_nb_iter then       
       raise (Failure "No iterations left !");
     if Unix.gettimeofday () > timeout then
       raise (Failure "Timeout !");
@@ -124,7 +123,7 @@ let nparamod rdb metasenv subst context t table =
        let bag, maxvar, new_goals = 
          List.fold_left 
            (fun (bag,m,acc) g -> 
-              let bag, m, ng = Sup.infer_left bag maxvar g
+              let bag, m, ng = Sup.infer_left bag m g
                 ([current],ctable) in
                 bag,m,ng@acc) 
            (bag,maxvar,[]) g_actives