Verification Condition of Assume(e)

As far as I can see from the notes, vc [assume(e)] Q = {}
Can I count it as True because it does not need any condition to fulfill.

It’s similar to the vc for all the other simple statements.

In the end, we require that (among other things) all formulas in the vc set are valid, and if they are none, then they are in fact all valid by vacuous truth.

1 Like