  Expressing system specifications using Computation Tree Logic (CTL) formulas,
formalising programs using Kripke structures, and then model checking the
system is an established workflow in program verification and has wide
applications in AI. In this paper, we consider the task of model enumeration,
which asks for a uniform stream of output systems that satisfy the given
specification. We show that, given a CTL formula and a system (potentially
falsified by the formula), enumerating satisfying submodels is always hard for
CTL - regardless of which subset of CTL operators is considered. As a silver
lining on the horizon, we present fragments via restrictions on the allowed
Boolean functions that still allow for fast enumeration.
