When validator connects contract inputs to assume, guarantees and modes. The outputs of the components subject to verification should not be connected with Assume and Require. As they cannot be mentioning this outputs.
If it is difficult to differentiate between input signals and the output signal of the component to verify in Validator callback. The user should be aware of this issue and remove by himself these signals, if not Kind2 will complain.
When validator connects contract inputs to assume, guarantees and modes. The outputs of the components subject to verification should not be connected with Assume and Require. As they cannot be mentioning this outputs.
If it is difficult to differentiate between input signals and the output signal of the component to verify in Validator callback. The user should be aware of this issue and remove by himself these signals, if not Kind2 will complain.