option to limit stack depth in emptiness checks
It would be nice to be able to limit the depth of the DFS used in the various emptiness checks. This can be used as a form of bounded model checking; and it would have been useful to the people preparing the model-checking contest and looking for cases where the emptiness check is still undecided after having explored a large part of the state space.
Note that when the emptiness check does not find a counterexample, it should be able to tell whether it hit the depth-limit (in which case a counterexample could exist nonetheless) or not (full state-space explored).