Require globally unique symbol names

Z3 can distinguish between constants that have the same symbol as
long as their sort differ. In contrast, MathSAT5 requires globally
unique symbol names, regardless of sorts.