The talk will explain a naive approach to deciding the satisfiability of quantified bitvector formulae based on binary decision diagrams. We then describe techniques and improvements that make this approach competitive, namely simplifications of formulas with unconstrained variables, approximations based on effective bit-width reduction, and operation abstraction. Finally, we present some future research directions.