From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 22 Oct 2004 13:01:06 +0000 (+0000)
Subject: bugfix: handle overflow in powerset cardinality
X-Git-Tag: V_0_0_10~20
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cc74e69409c73baf7bcfc522a7dfe7cbc92f2369;p=helm.git

bugfix: handle overflow in powerset cardinality
---

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index 619af110b..cbca9a9c2 100644
--- a/helm/ocaml/tactics/metadataQuery.ml
+++ b/helm/ocaml/tactics/metadataQuery.ml
@@ -118,7 +118,8 @@ let hint ~(dbh:Dbi.connection) ?signature ((proof, goal) as status) =
   in
   let other_constants = Constr.StringSet.union sig_constants hyp_constants in
   let uris = 
-    if (List.length uris < 2 ** (Constr.StringSet.cardinal other_constants))
+    let pow = 2 ** (Constr.StringSet.cardinal other_constants) in
+    if ((List.length uris < pow) or (pow <= 0))
     then begin
       prerr_endline "MetadataQuery: large sig, falling back to old method";
       filter_uris_forward ~dbh (main, other_constants) uris