SwInE is an SMT solver with support for integer exponentitaion. In our corresponding paper, the underlying approach is explained in detail.

It is based on "standard" SMT solvers without support for integer exponentiation. This is the original implementation, where the underlying SMT solver can be exchanged via a command line flag. Here you can find a reimplementation that directly uses the API of Z3. Hence, the reimplementation is more efficient and robust than the original, but the underlying solver is fixed.