This paper presents an encoding of B proof obligations in SMT-LIB 2.7, leveraging the recent extensions of SMT-LIB to higher-order logic. Our encoding improves upon previous approaches by eliminating uninterpreted membership predicates and by avoiding the complexity of encoding functions as relations. Through SMT-LIB’s support for higher-order constructs, we achieve a more natural representation of B’s set theory, while ensuring soundness of the translation. Preliminary experimental results are promising and indicate that our encoding allows certain proof obligations that previously failed to be discharged.