  We consider a first-order logic for the integers with addition. This logic
extends classical first-order logic by modulo-counting, threshold-counting and
exact-counting quantifiers, all applied to tuples of variables (here, residues
are given as terms while moduli and thresholds are given explicitly). Our main
result shows that satisfaction for this logic is decidable in two-fold
exponential space. If only threshold- and exact-counting quantifiers are
allowed, we prove an upper bound of alternating two-fold exponential time with
linearly many alternations. This latter result almost matches Berman's exact
complexity of first-order logic without counting quantifiers.
  To obtain these results, we first translate threshold- and exact-counting
quantifiers into classical first-order logic in polynomial time (which already
proves the second result). To handle the remaining modulo-counting quantifiers
for tuples, we first reduce them in doubly exponential time to modulo-counting
quantifiers for single elements. For these quantifiers, we provide a quantifier
elimination procedure similar to Reddy and Loveland's procedure for first-order
logic and analyse the growth of coefficients, constants, and moduli appearing
in this process. The bounds obtained this way allow to restrict quantification
in the original formula to integers of bounded size which then implies the
first result mentioned above.
  Our logic is incomparable with the logic considered by Chistikov et al. in
2022. They allow more general counting operations in quantifiers, but only
unary quantifiers. The move from unary to non-unary quantifiers is non-trivial,
since, e.g., the non-unary version of the H\"artig quantifier results in an
undecidable theory.
