Satisfiability modulo theories (SMT) solvers are widely used for determining the satisfiability of logical formulas with respect to background theories. SMT solvers are traditionally based on first-order logic, but some also support higher-order logic. Recently, Kondylidou et al. introduced model-based quantifier instantiation with fast enumeration (MBQI-Enum), a quantifier instantiation strategy that works for both logics. A weakness of MBQI-Enum is that it does not find refutations when Hilbert choice terms are necessary. In this work, we present an extension of MBQI-Enum that enables it to reason effectively about Hilbert’s choice operator. The extended strategy substantially increases the success rate of the SMT solver cvc5 on higher-order benchmarks.