It’s unclear from your description is this Z3 problem or this is the nature of such problems (and it’s a wish).

Are there other tools that do it better or proposal how Z3 would do it?