Model checking is one of the successful program verification methodologies. Since the seminal work by Ong, the model checking of higher-order programs—called \emph{higher-order model checking}, or HOMC for short—has gained attention. It is also crucial for making HOMC applicable to real-world software to address programs involving computational effects. Recently, Dal Lago and Ghyselen considered an extension of HOMC to \emph{algebraic effect handlers}, an emerging construct to enable programming the semantics of effects. Dal Lago and Ghyselen shows a negative result for the HOMC problem with algebraic effect handlers–it is undecidable.

In this work, we explorer a restriction on programs with algebraic effect handlers such that it ensures the decidability of the HOMC problem while allowing implementations of various effects. We identify the crux of the undecidability is that unrestricted programs allow the use of an unbounded number of effect handlers. To restrict such a use of effect handlers, we introduce \emph{answer-type modification} (ATM), which can bound the number of effect handlers that can be active at the same time. We prove that ATM can ensure the decidability of the HOMC problem and show that it accommodates a wide range of effects. To evaluate our approach, we implemented and tested an automated verifier based on the presented techniques. We also confirmed that the program examples discussed in this paper can be automatically verified.