When I use "weak monadic second-order" here I'm just distinguishing between the theory of $(\mathbb{N}, \mathcal{F}(\mathbb{N}), \in, \leq)$ and $(\mathbb{N}, \mathcal{P}(\mathbb{N}), \in, \leq)$ where $\mathcal{F}$ is finite subsets and $\mathcal{P}$ is the full powerset. The theories are very similar, but only in the former do sets necessarily have largest elements, and the latter requires Buchi automata to analyze. On the other hand, my question is just about whether there is an omitting types-like theorem that I should be looking into.

Yes, but not just any model with order type $\omega+\zeta$ in the first order part (finding these is easy). I'm looking for a nonstandard model of the theory of $(\mathbb{N}, \mathcal{F}(\mathbb{N}), \in, \leq)$ with first order type $\mathbb{N} + \mathbb{Z}$ that also realizes the continuum many types specifying the $C_K$.

The set you provide is the periodic set $L(\{1,2\};3)$ over the cone $L(0;3)$. In my construction, I'm allowing arbitrary periodic behavior over each piece. My goal with my construction is to make it easier to see that the semilinear sets are closed under boolean operations: The complement of a piecewise periodic set is a piecewise periodic set with the same pieces, but complemented periodic behavior. The intersection of piecewise periodic sets has pieces that are boolean combinations of the initial pieces, and the intersection of two periodic patterns is intuitively periodic.

The stated theorem isn't enough for my needs, but perhaps the proof is. I think my claim would follow if the linear sets in Ito's construction are mutually disjoint either because their cones are disjoint or because they have the same periods and different starting constants. I'll keep working through the paper, but is this how the proof works?

I just found A. L. Semenov's "On Certain Extensions of the Arithmetic of Addition of Natural Numbers" (1980), which seems to address this exact question. I'll answer my own question if I can make sense of it.

I am curious about the history of how this mistake got corrected into Büchi arithmetic, but I'm more interested in the specific case of various unary predicates; this is what Büchi is interested in in "Weak Second-Order Arithmetic and Finite Automata".

This is correct! The result is documented in "Decision Problems for Multiple Successor Arithmetics" by J.W. Thatcher. You can implement a finite state automaton by having a separate word $x_q$ for each state, and require that the nth character of $x_q$ is a marker character $a$ iff the automaton is in state $q$ just before reading the nth character of the input. The equal length predicate lets you line everything up even without being able to use variables for natural numbers.