Module Instance Sub Fields not Used in Connection Checking Sometimes

[dz333]

In the generated z3, the constraints appropriately use module instance names, e.g. inst.io.in := bits turns into something like (assert (= (field_in (field_io inst)) bits))

However the label checking that uses these fields as labels doesn't do the right thing, e.g. the label inst.io.lbl is turned in to (field_lbl io) instead of (field_lbl (field io) inst)