  We present a novel approach for solving quantified bit-vector formulas in
Satisfiability Modulo Theories (SMT) based on computing symbolic inverses of
bit-vector operators. We derive conditions that precisely characterize when
bit-vector constraints are invertible for a representative set of bit-vector
operators commonly supported by SMT solvers. We utilize syntax-guided synthesis
techniques to aid in establishing these conditions and verify them
independently by using several SMT solvers. We show that invertibility
conditions can be embedded into quantifier instantiations using Hilbert choice
expressions, and give experimental evidence that a counterexample-guided
approach for quantifier instantiation utilizing these techniques leads to
performance improvements with respect to state-of-the-art solvers for
quantified bit-vector constraints.
