Answer:

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

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).