Как преодолеть проблему сколемизации в выражении assert

Question

У меня есть следующий простой пример.

sig B {}
pred P2 {some x1, x2: lone B | x1 != x2}
run P2 for 2

Мой вопрос: как переписать ограничение pred в assert без ошибки сколемизации?

assert S { some x1, x2: lone B | x1 != x2} 
check S for 2

Answer 1

Удаление лишнего одиночного квантификатора в вашем утверждении решает проблему.

assert S { some x1, x2:  B | x1 != x2} 

Что бы вы хотели оценить?Я сомневаюсь, что использование lone B - это то, что вы намеревались сделать.