  The finite satisfiability problem of monadic second order logic is decidable
only on classes of structures of bounded tree-width by the classic result of
Seese (1991). We prove the following problem is decidable:
  Input: (i) A monadic second order logic sentence $\alpha$, and (ii) a
sentence $\beta$ in the two-variable fragment of first order logic extended
with counting quantifiers. The vocabularies of $\alpha$ and $\beta$ may
intersect.
  Output: Is there a finite structure which satisfies $\alpha\land\beta$ such
that the restriction of the structure to the vocabulary of $\alpha$ has bounded
tree-width? (The tree-width of the desired structure is not bounded.)
  As a consequence, we prove the decidability of the satisfiability problem by
a finite structure of bounded tree-width of a logic extending monadic second
order logic with linear cardinality constraints of the form
$|X_{1}|+\cdots+|X_{r}|<|Y_{1}|+\cdots+|Y_{s}|$, where the $X_{i}$ and $Y_{j}$
are monadic second order variables. We prove the decidability of a similar
extension of WS1S.
