From: Alberto Griggio <griggio@fbk.eu>
Date: Wed, 31 Aug 2005 23:08:10 +0000 (+0000)
Subject: fixed bug in compute_equality_weight caused by wrong assumption on function
X-Git-Tag: working_equations_only~5
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fed37f1a768b314bf88e43be1af96f2c507ce933;p=helm.git

fixed bug in compute_equality_weight caused by wrong assumption on function
arguments evaluation order
---

diff --git a/helm/ocaml/paramodulation/utils.ml b/helm/ocaml/paramodulation/utils.ml
index f2ece4baa..525ed9ca2 100644
--- a/helm/ocaml/paramodulation/utils.ml
+++ b/helm/ocaml/paramodulation/utils.ml
@@ -107,8 +107,8 @@ 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
+  let w = (weight_of ty) + (weight_of left) + (weight_of right) in
+  w + !metasw
 (*     (4 * IntSet.cardinal !metasw) *)
 ;;