Since v4.2, Alloy features an option to prevent (arithmetic) overflows. I was wondering whether people use it always/sometimes/never and what is the justification for their choice?
I’ve been over this with Aleksandar a long time ago, remember it was a long discussion. The problem with limiting overflow was that it doesn’t give you a solution when it happens which can be extremely puzzling. It would be more useful imho if it could create an error. I think we could do many very simple checks for integer sanity anyway. Having an error model where we have booleans representing error cases might be useful anyway, that are or’ed with the model’s solution for run sounds intuitively like an interesting idea? Post resolving we could then inspect them and generate warnings.
The other thing I remember is that setting the option in the environment is quite wrong since, the model very much depends on that setting. We should set this in the run/check statement or in a general option. (I once proposed to allow the options that influence the model’s solutions to be set with e.g. --overflow false options. It is part of the API branch think.