I see there is an option in the Alloy Analyzer to allow recursion up to a certain depth (1-3).
But what happens when a counterexample cannot be found because of the limited recursion depth?
Will there be an error or a warning, or are such counterexamples silently ignored?