src/HOL/Library/Tools/smt_word.ML

   (*CVC4 does not support "_bvk T" when k does not fit in the BV of size T, so remove the bits that
    will be ignored according to the SMT-LIB*)
   fun word_num (Type (\<^type_name>\<open>word\<close>, [T])) k =
         let
           val size = try dest_binT T
-          fun max_int size = IntInf.pow (2, size)
+          fun max_int size = Integer.pow size 2
         in
           (case size of
             NONE => NONE
           | SOME size => SOME (index1 ("bv" ^ string_of_int (Int.rem(k, max_int size))) size))
         end