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 prop

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?