The Entscheidungsproblem, or the classical decision problem, asks whether a given formula of first-order logic is satisfiable. This problem has been a fundamental piece in advancing the state of the art in formal reasoning about programs. What happens when we ask the decision problem not for a single formula, but for an infinite collection of formulae? This talk delves deeper in this question and explains connections to many programming languages tasks (testing, verification, synthesis, learning etc). More precisely, I will talk about an extension of the Entscheidungsproblem problem to regular first-order theories, i.e., (infinite) regular sets of formulae. I will discuss our initial recent results from an ongoing investigation of the decidability landscape of this problem. Building on the elegant classification of syntactic classes as decidable or undecidable for the classical decision problem, we show that some classes (specifically, the EPR and Gurevich classes), which are decidable in the classical setting, become undecidable for regular theories. On the other hand, for each of these classes, we identify a subclass that remains decidable in our setting. Finally, we observe that our problem generalises prior work on automata-theoretic verification of uninterpreted programs and propose a semantic class of existential formulae for which the problem is decidable. This talk builds upon our work published at POPL 2025 with a similar title.