Hello,

I'm a teaching assistant and I supervise the lab sessions of a course on automated reasoning.  During these lab sessions, the students use Alloy.  In the frame of these lab sessions, I found a weird bug of Alloy.  Here is a way to reproduce it.


sig A {}
sig B {}
fact {
   #B = #(A -> A - iden)
}
run {} for exactly 18 B, exactly 2 A


There are two signatures and a fact constraining the cardinality of both sets: the number of Bs must be equal to the number of all possible couples of disjoint As.
Running the given command, Alloy finds an instance where there are 18 Bs and 2 As, while such an instance shouldn't be allowed by the model.  Furthermore, the Evaluator says that, for this instance, the number of As is 2 and the number of Bs is also 2 (while the visualizer displays 2 As and 18 Bs).

Could you confirm that this is a bug?

Thank you,

Simon