Нарушение симметрии сплава не работает

Да, нарушение симметрии включено по умолчанию. (На самом деле я не знаю, как это отключить, поэтому слово «по умолчанию» может быть не совсем подходящим для этого.)

Если среди результатов вы обнаружите несколько изоморфных моделей, значит, анализатор сплавов делает компромисс между производительностью и симметрией. Компромисс обсуждается в разделе 5.2.1 Абстракции программного обеспечения:

[Анализатор] создает из модели ограничения, нарушающие симметрию, и соединяет их с ограничением анализа. Если бы они были идеальными, эти ограничения исключали бы все присваивания, кроме одного, в каждом классе эквивалентности, но оказывается, что для этого требуются очень большие ограничения, нарушающие симметрию, которые перегружали бы решатель и фактически снижали производительность. Таким образом, анализатор генерирует гораздо меньшее ограничение, которое нарушает только некоторые симметрии, но на практике устраняет очень большую долю (более 99%) назначений.