Hi,

Suppose pred1 look for a sequence to satisfy constraint C1:

pred1 [seq of Object] {C1}

Alloy translates C1 to CNF, searches for the sequence
and gives a result as no instance found.
Good, because it is expected.

Now, consider pred2 that extends pred1 as follows:

pred2 [seq of Object] {C1 && C2}

Alloy then translates C1 && C2 to CNF. Since C2 is complicated somehow the CNF translation takes extremely long to allow the search to happen to finally say no instance found.

Is it possible my imagination? Do you see my point?

Thanks in advance.