X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fsuperposition.ml;fp=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fsuperposition.ml;h=413ab93b657d41d4a1da2189d8d3f3491b59a555;hb=ddba563cd3f42a7947a0e0b464d5dd3c5f9b299d;hp=47119d4770e25beab157df62540aa120c0d1533e;hpb=befd0e7820308a9a09d3499c8131e26578efc462;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index 47119d477..413ab93b6 100644
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -258,12 +258,19 @@ module Superposition (B : Orderings.Blob) =
     (* move away *)
     let is_identity_clause ~unify = function
       | _, [], [Terms.Equation (_,_,_,Terms.Eq),_], _, _ -> true
-      | _, [], [Terms.Equation (l,r,_,_),_], vl, proof when unify ->
+      | _, [], [Terms.Equation (l,r,_,_),_], vl, _ when unify ->
           (try ignore(Unif.unification (* vl *) [] l r); true
           with FoUnif.UnificationFailure _ -> false)
       | _ -> false
     ;;
 
+    let is_goal_trivial = function
+      | _, [Terms.Equation (_,_,_,Terms.Eq),_], [], _, _ -> true
+      | _, [Terms.Equation (l,r,_,_),_], [], vl, _ ->
+          (try ignore(Unif.unification (* vl *) [] l r); true
+          with FoUnif.UnificationFailure _ -> false)
+      | _ -> false
+
     let build_new_clause bag maxvar filter rule t subst id id2 pos dir =
       let maxvar, _vl, subst = Utils.relocate maxvar (Terms.vars_of_term
       (Subst.apply_subst subst t)) subst in
@@ -553,7 +560,7 @@ module Superposition (B : Orderings.Blob) =
         if no_demod then bag, clause else demodulate bag clause table 
       in
       if List.exists (are_alpha_eq clause) g_actives then None else
-      if (is_identity_clause ~unify:true clause)
+      if (is_goal_trivial clause)
       then raise (Success (bag, maxvar, clause))
       else   
         let (id,nlit,plit,vl,_) = clause in