If we're fuzzing as input to simulators, then it can be helpful to make sure the number of variables doesn't exceed the number of variables that can be passed in registers, hence avoiding introducing the stack. We can likely model this in the same way as we model thread caps: make an integer parameter, and consult it as part of the precondition of variable introductions.
It's not yet clear whether we'd want a thread-local cap (cap on variables visible to a thread) or a global one (cap on variables visible throughout), or both.
If we're fuzzing as input to simulators, then it can be helpful to make sure the number of variables doesn't exceed the number of variables that can be passed in registers, hence avoiding introducing the stack. We can likely model this in the same way as we model thread caps: make an integer parameter, and consult it as part of the precondition of variable introductions.
It's not yet clear whether we'd want a thread-local cap (cap on variables visible to a thread) or a global one (cap on variables visible throughout), or both.