x = new()

Becomes:

assume (t notin S);
x := t;
S = S U {t};

We will obtain formulas with sets, in FOL eliminate them using quantifiers.