From fed37f1a768b314bf88e43be1af96f2c507ce933 Mon Sep 17 00:00:00 2001 From: Alberto Griggio Date: Wed, 31 Aug 2005 23:08:10 +0000 Subject: [PATCH] fixed bug in compute_equality_weight caused by wrong assumption on function arguments evaluation order --- helm/ocaml/paramodulation/utils.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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) *) ;; -- 2.39.2