Bit-vector theories with concatenation and extraction have been shown
to be useful and important for hardware verification. We have
implemented an extended theory which includes arithmetic. Although
deciding equality in such a theory is NP-hard, our implementation is
efficient for many practical examples. We believe this to be the first
such implementation which is efficient, automatic, and complete.