but not use it by default, because of bad caching of smt_encoding
transformations. Because of this, new function symbols appear again
and again, and since we don't forget function symbols in trans-based
printers, we obtain names like at234.