  Given a formula $F$ of satisfiability modulo theory (SMT), the classical SMT
solver tries to (1) abstract $F$ as a Boolean formula $F_B$, (2) find a Boolean
solution to $F_B$, and (3) check whether the Boolean solution is consistent
with the theory. Steps~{(2)} and (3) may need to be performed back and forth
until a consistent solution is found. In this work, we develop a quantum SMT
solver for the bit-vector theory. With the characteristic of superposition in
quantum system, our solver is able to consider all the inputs simultaneously
and check their consistency between Boolean and the theory domains in one shot.
