Two-variable logic with counting is decidable

We prove that the satisfiability and the finite satisfiability problems for C^2 are decidable. C^2 is first-order logic with only two variables in the presence of arbitrary counting quantifiers, "there exist at least m elements x", for m a natural number. It considerably extends L^2, plain first-order with only two variables, which is known to be decidable by a result of Mortimer's. Unlike L^2, C^2 does not have the finite model property.