  We study the precise computational complexity of deciding satisfiability of
first-order quantified formulas over the theory of fixed-size bit-vectors with
binary-encoded bit-widths and constants. This problem is known to be in
EXPSPACE and to be NEXPTIME-hard. We show that this problem is complete for the
complexity class AEXP(poly) -- the class of problems decidable by an
alternating Turing machine using exponential time, but only a polynomial number
of alternations between existential and universal states.
