There's a corner case I've just discovered:
If the type is the unit type (scalar type of cardinality 1), yices_new_uninterpreted_term returns the unique inhabitant of the type.
It's satisfiability-preserving, but not ideal.
In particular, yices_subst_term will then complain if you try to substitute what you thought was an uninterpreted term (but is actually this constant) by an expression of type unit. In a model, I suspect the value for what the user thought was an uninterpreted term may also be missing, because the uninterpreted term never existed in the first place (to be checked).
Obviously, there's little point introducing uninterpreted terms of type unit, perhaps even less substituting them, but the user code may be generic over Yices types, so now we're pushing onto the user the burden to do a case analysis on the type, for an optimization that isn't documented.

@BrunoDutertre : Did the trick provide speed-ups? If we want to keep it, we may want to do a case analysis in yices_subst_term so that it doesn't complain but instead ignores the substitution on type unit, trying to pretend there is actually an uninterpreted term of type unit even if internally there isn't. And perhaps make sure a value is returned in the model for an uninterpreted term of type unit? Any thoughts?