Satisfiability Modulo Theories (SMT) is a growing field in computer science and logic. Given a mathematical formula, solving the SMT problem means determining whether the formula is satisfiable within the context of a specific theory. One such theory is Presburger arithmetic (also known as Linear Integer Arithmetic), which is the first-order theory of integers with addition. A method for defining the satisfiability of formulae in this theoryinvolves the use of finite automata [10]. In this project, we extend the cvc5 solver [2] by incorporating an automata-based tool for solving Presburger arithmetic formulae and compare it with state of the art solvers such as Lash [42] and Amaya [24]. Our tool is based on the Mata automata library [15]. As future work, we plan to also add the preprocessing steps described in [24] for the construction of more efficient automata.