Answer:

It is due to integer wrap around.

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

"#f" takes the number of entries, then truncates the number to fit in
the current integer bitwidth. So given the default integer bitwidth of 4,
"#f=3" simply says that the lowest 4 bits should be 0011.

An instance with 3 entries in f is valid, since 3 is 11 in binary.
An instance with 19 entries in f is also valid, since 19 is 10011 in binary.

There are a few ways to get around this problem:

a) If you manually choose a higher bitwidth, high enough
   that #f can never legally overflow it, then you can
   be sure that #f=3 means what you want it to mean.

   For example, if F is a relation from A to A, and the scope of A is 3,
   then there are at most 9 tuples in f.  If you then pick a bitwidth of 5,
   the possible integers range from -16 to +15,
   thus "#f" will never overflow, and you're safe.

   Try "check SomeAssertion for 3 A, 5 int"

b) Instead of writing "#f=3", you can express it by
   saying that f is the union of three distinct values.

   For example, if f is a subset of A, you can try
   some disj a, b, c: one A | F=a+b+c

   For example, if F is binary from A to A, you can try
   some disj a, b, c: one (A->A) | F=a+b+c

   This is more expensive, but it will do the right thing.

One might ask "Why is the Alloy semanics designed this way?"

In terms of semantics, every well-typed expression in Alloy
is legal, since we cannot have any runtime errors or exceptions
in a declarative logic. This is also why Alloy doesn't
have partial functions (since you might then call a function
with an illegal input). Every function and every operator in Alloy
is total. So "#" must always produce an integer. But in general we
do not know the possible value range prior to the analysis,
so we have to assign a meaning to # when it overflows,
and the meaning we chose is for the number to get truncated
if it overflows.