X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Futils.ml;h=c1c9086de1ccf4db4570125ea0f2963bcfd1495f;hb=3e8363bec852afb37160d8144db8d94bbff447d6;hp=f2ece4baa9f8478716212d4bf13e89d42b5b40ff;hpb=d622a1ce338d9db774ddc8b98fa58cdcec7b22e5;p=helm.git

diff --git a/helm/ocaml/paramodulation/utils.ml b/helm/ocaml/paramodulation/utils.ml
index f2ece4baa..c1c9086de 100644
--- a/helm/ocaml/paramodulation/utils.ml
+++ b/helm/ocaml/paramodulation/utils.ml
@@ -107,8 +107,10 @@ let compute_equality_weight ty left right =
 (*     metasw := List.fold_left (fun s (i, _) -> IntSet.add i s) !metasw m; *)
     w
   in
-  (weight_of ty) + (weight_of left) + (weight_of right) +
-    !metasw
+  (* Warning: the following let cannot be expanded since it forces the
+     right evaluation order!!!! *)
+  let w = (weight_of ty) + (weight_of left) + (weight_of right) in
+  w + !metasw
 (*     (4 * IntSet.cardinal !metasw) *)
 ;;