From cc74e69409c73baf7bcfc522a7dfe7cbc92f2369 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 22 Oct 2004 13:01:06 +0000 Subject: [PATCH] bugfix: handle overflow in powerset cardinality --- helm/ocaml/tactics/metadataQuery.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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 -- 2.39.2