SMT solving for higher order logic has been around for a few years and many challenges remain to tackle. In this talk, I will present an assessment of the current state of research in higher-order SMT and focus on the challenge of quantifier instantiation, following a conflict-based approach inspired from first-order logic.