  We consider the satisfiability problem for the two-variable fragment of the
first-order logic extended with modulo counting quantifiers and interpreted
over finite words or trees. We prove a small-model property of this logic,
which gives a technique for deciding the satisfiability problem. In the case of
words this gives a new proof of EXPSPACE upper bound, and in the case of trees
it gives a 2EXPTIME algorithm. This algorithm is optimal: we prove a matching
lower bound by a generic reduction from alternating Turing machines working in
exponential space; the reduction involves a development of a new version of
tiling games.
