Abstract We extend the mono-modal CEGAR-tableaux of Goré and Kikkert to normal multi-modal logic $$\textrm{K}_{\textrm{n}}$$ K n with global assumptions. We then extend these CEGAR-tableaux to multi-modal tense logic $$\textrm{Kt}_{\textrm{n}}$$ Kt n without global assumptions by “compiling in” the residuation conditions between “future” and “past” modalities. Our new implementation uses $$\mathrm {C^{++}}$$ C + + and includes multiple optimisations which speed up proof-search. $$\texttt {CEGARBox++}$$ CEGARBox + + is the best satisfiability-checker for mono-modal tense logic $$\textrm{Kt}_{\textrm{1}}$$ Kt 1 but is not competitive for global assumptions.