Fix exclusion criteria for codatatype model values (#7546)

Fix exclusion criteria for codatatype model values (#7546)

This fixes codatatype model value construction.

Model construction for codatatypes is non-standard since it requires analyzing whether (possibly recursively defined) terms are alpha equivalent to others during model construction. This is currently handled as a special case within the theory model builder. (This should eventually be moved somewhere more appropriate via a new callback to theory).

This fixes the criteria which was too permissive about which values can be used in models. We now exclude values that match the skeleton of representative codatatype terms. Previously we additionally required that the terms were bisimilar.

Fixes #4851.