Minor fixing for last chance

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index 6a2950b0e3da34514327d96f988bb0599e50d3c9..fad0a12d28a7df72ad7acad75eb45abf0d70efbe 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -342,7 +342,6 @@ module Superposition (B : Orderings.Blob) =
       in
        bag, maxvar, res
     ;;
-
     
     let rewrite_eq ~unify l r ty vl table =
       let retrieve = if unify then IDX.DT.retrieve_unifiables
@@ -613,7 +612,10 @@ module Superposition (B : Orderings.Blob) =
       then raise (Success (bag, maxvar, clause))
       else   
         let (id,lit,vl,_) = clause in 
-        if vl = [] then Some (bag,clause)
+        (* this optimization makes sense only if we demodulated, since in 
+          that case the clause should have been turned into an identity *)
+        if (vl = [] && not(no_demod)) 
+       then Some (bag,clause)
         else
          let l,r,ty = 
            match lit with
@@ -624,15 +626,15 @@ module Superposition (B : Orderings.Blob) =
            table (Some(bag,maxvar,clause,Subst.id_subst)) with
          | None -> Some (bag,clause)
          | Some (bag,maxvar,cl,subst) -> 
-             prerr_endline "Goal subsumed";
-             raise (Success (bag,maxvar,cl))
+             debug (lazy "Goal subsumed");
+             raise (Success (bag,maxvar,cl)))
 (*
-      else match is_subsumed ~unify:true bag maxvar clause table with
+        match is_subsumed ~unify:true bag maxvar clause table with
         | None -> Some (bag, clause)
         | Some ((bag,maxvar),c) -> 
             prerr_endline "Goal subsumed";
             raise (Success (bag,maxvar,c))
-*) 
+*)
     ;;
 
     let prof_simplify_goal = HExtlib.profile ~enable "simplify_goal";;