  We propose $\omega$MSO$\Join$BAPA, an expressive logic for describing
countable structures, which subsumes and transcends both Counting Monadic
Second-Order Logic (CMSO) and Boolean Algebra with Presburger Arithmetic
(BAPA). We show that satisfiability of $\omega$MSO$\Join$BAPA is decidable over
the class of labeled infinite binary trees, whereas it becomes undecidable even
for a rather mild relaxations. The decidability result is established by an
elaborate multi-step transformation into a particular normal form, followed by
the deployment of Parikh-Muller Tree Automata, a novel kind of automaton for
infinite labeled binary trees, integrating and generalizing both Muller and
Parikh automata while still exhibiting a decidable (in fact PSpace-complete)
emptiness problem. By means of MSO-interpretations, we lift the decidability
result to all tree-interpretable classes of structures, including the classes
of finite/countable structures of bounded treewidth/cliquewidth/partitionwidth.
We generalize the result further by showing that decidability is even preserved
when coupling width-restricted $\omega$MSO$\Join$BAPA with width-unrestricted
two-variable logic with advanced counting. A final showcase demonstrates how
our results can be leveraged to harvest decidability results for expressive
$\mu$-calculi extended by global Presburger constraints.
