SMT solvers have throughout the years been able to cope with increasingly expressive formulas, from ground logics to full first-order logic (FOL). Nevertheless, higher-order logic (HOL) within SMT is still little explored. We propose a pragmatic extension for SMT solvers to natively support HOL reasoning without compromising performance on FOL reasoning, thus leveraging the extensive research and implementation efforts dedicated to efficient SMT solving. We show how to generalize data structures and the ground decision procedure to support partial applications and extensionality, as well as how to reconcile instantiation techniques with functional variables. We also discuss a separate approach for redesigning an SMT solver to HOL via new data structures and algorithms. We apply the pragmatic extension to the CVC4 SMT solver and redesign the veriT solver. Our evaluation shows they are competitive with state-of-the-art HOL provers and often outperform the traditional encoding into FOL.