Answer:

In Alloy, integers are represented using 2's complement arithmetic.

The most significant bit is used as the sign bit, and arithmetic operations overflow silently.
For example: if you executes a command with the integer bitwidth set to 4, then 6+3 is equal to -7
(Intuitively, you start at 6, and add 1 to it three times, where if we go beyond +7 we wrap around to -8)

By default, the integer bitwidth is 4. so the available integers are
{ -8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7 }.

When Alloy4 executes a command, it says "Solver=SAT4J Bitwidth=4 Symmetry=20...",
the "bitwidth" part is telling you the integer bitwidth chosen for that command.

To change the bitwidth for a particular command, use the "int" keyword.
For example, to check an assertion with an integer bitwidth of 7,
write "check SomeAssertion for 5 but 2 A, 3 B, 7 int"

Currently the bitwidth must be between 1 and 30, though realistically
you should probably use a bitwidth somewhere between 1 and 7
(otherwise the analysis will likely run out of memory or take too long to complete).