Berthelot's conjecture D for arithmetic D-modules

Let ${\mathcal X}$ be a smooth formal scheme, let $Z$ be a divisor of its special fibre, and write ${\mathcal U}$ for the complement of $Z$. Let ${\mathcal E}^\dagger$ be a coherent $F$-${\mathcal D}^\dagger_{{\mathcal X},{\bf Q}}(^\dagger Z)$-module whose restriction to ${\mathcal U}$ is holonomic. Denote by

$${\bf res}({\mathcal E}^\dagger)$$

the corresponding restriction or extension functor to ${\mathcal D}^\dagger_{{\mathcal X},{\bf Q}}$-modules. Berthelot's conjecture D. The module ${\bf res}({\mathcal E}^\dagger)$ is a holonomic $F$-${\mathcal D}^\dagger_{{\mathcal X},{\bf Q}}$-module. This is the conjecture cited as Berthelot's conjecture D and concerns preservation of holonomicity when removing the overconvergent singularities along $Z$; the supplied passage gives no resolution status.