During the recent years, the development of tools for deciding Quantified Boolean Formulas (QBFs) has been accompanied by a steady supply of real-world instances, i.e., QBFs originated by translations from application domains. Instances of this kind showed to be challenging for current state-of-the-art QBF solvers, while the ability to deal effectively with them is necessary to foster adoption of QBF-based reasoning in practice. In this paper we describe some reasoning techniques that we conceived, implemented and combined into our solver QuBE++ to increase its effectiveness on real-world instances. We present the results of an experimental campaign conducted to assess the relative efficienty of each technique, and of their combination. Our data also show that QuBE++, on real-world SAT instances, is comparable to current state-of-the-art SAT solvers.