Are there premice that are $\omega_1$-iterable but not $(\omega_1+1)$-iterable? For (hopefully) simplicity, let a premouse be defined coarsely as in Martin and Steel's 1994 paper, Iteration Trees.
Is (or is it consistent that) there is a premouse that is $\omega_1$-iterable but not $(\omega_1+1)$-iterable?
Note: if adding some extra conditions will get partial answers, that would also be very helpful.
 A: It is consistent (relative to large cardinals). There is an example given in Example 3.6 here. For a brief summary: the model is the minimal proper class mouse $S$ such that $\mathbb{R}^S$ is closed under the $M_1^\#$-operator. In particular, $M_1^\#$ is a proper segment of $S$. And $S$ satisfies "$(M_1,\delta^{M_1})$ is a premouse and $(M_1,\delta^{M_1})$ is $\omega_1$-iterable but not $(\omega_1+1)$-iterable" (with these definitions in the sense of "Iteration trees"). In $S$, there is a tree $\mathcal{T}$ on $M_1$, formed via a variant of self-genericity iteration, which has length $\omega_1$ and no cofinal branch in $S$. (The usual sort of self-genericity iteration would be formed by iterating to make some initial segment of $S$ generic for the $\delta$-generator extender algebra. In the variant used, one also interweaves countable linear iterations at appropriate stages of the process, each of which "moves past the next instance of the $M_1^\#$-operator on the $S$-sequence"; this ensures that $\delta(\mathcal{T})$ is a limit of $M_1^\#$-operator instances on the $S$-sequence, which in turn ensures that $\delta(\mathcal{T})=\mathrm{lh}(\mathcal{T})=\omega_1^S$.)
