Answer:

The "core" in this case refers to "unsat core".
And it is only enabled when you change
the SAT solver to "MiniSat with Unsat Core".

When Alloy Analyzer figured out the core, if you click it,
Alloy Analyzer will try to highlight the part of the model
that is relevant to the assertion you were checking.

Suppose you are modeling a system where there are Teacher and Students,
and there are also Airplanes and Airports.  When you are checking
a general assertion about students, then maybe only the Student part
of the model (and maybe some of the definitions from Teacher)
will be highlighted.

But if you are checking an assertion about students flying
to attend a conference, then maybe the entire model will be highlighted.

It is simply a hint to the user about which part of the model
is relevant to the particular assertion you are checking.
(And it only shows up when a predicate or assertion is unsatisfiable).