In addition to the answers above, it is worth mentioning that the existential fragment of Presburger arithmetic can actually be extended by a **full divisibility** predicate while retaining decidability [1]. Satisfiability in the resulting fragment is in NEXP, the lower bound being NP [2].

Also, it is possible to define a family of formulas $\Phi_n(x,m)$ such that for every natural number $m$ representable using $n$-bits, $\Phi_n(x,m)$ holds if and only if $x \equiv 0 \bmod m$ [3].

<p>
[1] L. Lipshitz, “The Diophantine problem for addition and divisibility,”
Transactions of the American Mathematical Society, vol. 235, pp. 271–
283, 1976.
</p><p>
[2] Lechner, A.; Ouaknine, J.; Worrell, J., "On the Complexity of Linear Arithmetic with Divisibility," in Proceedings of the 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pp. 667-676, 2015.
</p><p>
[3] Haase, C., "Subclasses of Presburger arithmetic and the weak EXP hierarchy," in Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (CSL-LICS '14). ACM, New York, NY, USA, Article 47, 2014.
</p>