bugfix: handle overflow in powerset cardinality

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index 619af110b73afe54387826ed1f22af6ec96e2739..cbca9a9c270304d6feb62fee26b580e39da551cf 100644 (file)
--- 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