Since I guess the divergence bug is fixed, I activate the test again.

[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 6037354794d61963bce35c0c22c586a894bb4f17..994a141c93f5d8215ac4f7e9930b6528aa1e6cfe 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -730,8 +730,8 @@ module Superposition (B : Orderings.Blob) =
       in
         debug "Another superposition";
       let new_clauses = new_clauses @ additional_new_clauses in
-        debug (Printf.sprintf "Demodulating %d clauses"
-                 (List.length new_clauses));
+        debug (lazy (Printf.sprintf "Demodulating %d clauses"
+                 (List.length new_clauses)));
       let bag, new_clauses = 
         HExtlib.filter_map_monad (simplify atable maxvar) bag new_clauses
       in