I guess they have to be unique (since they are just functions), according to https://smt-lib.org/papers/smt-lib-reference-v2.6-r2017-07-18.pdf, page 61, where it says: "Similarly, constructors and selectors are function symbols, so none of them can be a previous declared/defined function symbol. This has the effect of also prohibiting, for instance, the use of the same constructor in different datatypes or the use of repeated instances of the same selector in the same datatype."

However, it seems to work partially which is interesting.