Merging Verification Conditions in one Formula

Here is a definition for PC and VC

Ekran görüntüsü 2022-07-28 012813

As we can see at last line, we can have conditions in a set structure, and we can unite them with union operator. However, the return type of the function getVerificationConditions() should be one formula. I guess we should merge them with “AND” operator. Is that right?

I wanted to be sure about it and wanted to hear your comments.


It’s your function, it can be whatever you want it to be

1 Like

But the function in the file is documented as mentioned. I guess I have to return it as a one formula. I might be mistaken though.
Thanks for giving answers at this late at night.

Yes, but this is not just the vc formula. See also

1 Like