cnf export does not handle mutuable signatures and fields

[goens]

I was exporting some models that were taking a long time to solve to CNF to check with an external solver. I was surprised when, for models I knew instances existed, the solver returned that they were unsatisfiable.

I then noticed that the exported CNF instances are identical independent of the number of steps I give them.

A simple example to reproduce:

sig B {}
sig A{ var b : set B }

fact init { no b }
pred step { some bval : B | bval not in A.b and A.b' = A.b + bval }
pred end { A.b = B}
fact stepsuntilend { step until end and eventually end }

run {} for exactly 3 A,  exactly 2 B, 3 steps
run {} for exactly 3 A,  exactly 2 B, 1 steps

The first one will find an instance just fine, while the second one won't (as 1 step is not enough). However, exporting to CNF will produce the same SAT instance (corresponding to one step, I presume).

[goens]

By the way, this issue does not show up when exporting to Kodkod.

[grayswandyr]

Pinging @nmacedo