Fixed a few bugs

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

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index f38acb536a707eeb5d0871b781af25cd2af412eb..c5bb640a2ba8bdb5c532f7bcf89a3686c0c29fa9 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -412,6 +412,7 @@ module Superposition (B : Orderings.Blob) =
       match acc with 
       | None -> None
       | Some(bag,maxvar,(id,lit,vl,p),subst) -> 
+          (* prerr_endline ("input subst = "^Pp.pp_substitution subst); *)
           let l = Subst.apply_subst subst l in 
           let r = Subst.apply_subst subst r in 
             try 
@@ -426,6 +427,8 @@ module Superposition (B : Orderings.Blob) =
             with FoUnif.UnificationFailure _ -> 
               match rewrite_eq ~unify l r ty vl table with
               | Some (id2, dir, subst1) ->
+                 (* prerr_endline ("subst1 = "^Pp.pp_substitution subst1);
+                    prerr_endline ("old subst = "^Pp.pp_substitution subst);*)
                   let newsubst = Subst.concat subst1 subst in
                   let id_t = 
                     FoSubst.apply_subst newsubst
@@ -437,7 +440,9 @@ module Superposition (B : Orderings.Blob) =
                         subst1 id id2 (pos@[2]) dir 
                     with
                     | Some ((bag, maxvar), c), r ->
-                       let newsubst = Subst.concat r newsubst in
+                       (* prerr_endline ("r = "^Pp.pp_substitution r); *)
+                       let newsubst = Subst.flat 
+                         (Subst.concat r subst) in
                         Some(bag,maxvar,c,newsubst)
                     | None, _ -> assert false)
               | None ->