From c6ee1124bbfd9ecf01ed5fd5b92e0b32b2c47d97 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 17 Oct 2010 09:09:12 +0000 Subject: [PATCH] fixed List.for_all2 called without knowing if the two lists have the same length --- helm/software/components/ng_paramodulation/orderings.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/helm/software/components/ng_paramodulation/orderings.ml b/helm/software/components/ng_paramodulation/orderings.ml index 1e143605b..f7062b3ab 100644 --- a/helm/software/components/ng_paramodulation/orderings.ml +++ b/helm/software/components/ng_paramodulation/orderings.ml @@ -40,7 +40,8 @@ let rec eq_foterm f x y = match x, y with | Terms.Leaf t1, Terms.Leaf t2 -> f t1 t2 | Terms.Var i, Terms.Var j -> i = j - | Terms.Node l1, Terms.Node l2 -> List.for_all2 (eq_foterm f) l1 l2 + | Terms.Node l1, Terms.Node l2 when List.length l1 = List.length l2 -> + List.for_all2 (eq_foterm f) l1 l2 | _ -> false ;; -- 2.39.2