In recent years, bit-precise reasoning has gained importance in hardware and software veriﬁcation. Of renewed interest is the use of symbolic reasoning for synthesising loop invariants, ranking functions, or whole program fragments and hardware circuits. Solvers for the quantiﬁer-free fragment of bit-vector logic exist and often rely on SAT solvers for eﬃciency. However, many techniques require quantiﬁers in bit-vector formulas to avoid an exponential blow-up during construction. Solvers for quantiﬁed formulas usually ﬂatten the input to obtain a quantiﬁed Boolean formula, losing much of the word-level information in the formula. We present a new approach based on a set of eﬀective word-level simpliﬁcations that are traditionally employed in automated theorem proving, heuristic quantiﬁer instantiation methods used in SMT solvers, and model ﬁnding techniques based on skeletons/templates. Experimental results on two diﬀerent types of benchmarks indicate that our method outperforms the traditional ﬂattening approach by multiple orders of magnitude of runtime.