This adds a ReqCheckVacuousResult to report invariants that are enforced by vacuous requirements.
A vacuous requirement enforces an invariant if there exists only one location in its PEA representation in which the maximal phase of its corresponding countertrace is not active.
Reporting such invariants may help to better understand vacuous results (e.g. as in #530) and their implications, as for example needed to approach #438.
This adds a ReqCheckVacuousResult to report invariants that are enforced by vacuous requirements. A vacuous requirement enforces an invariant if there exists only one location in its PEA representation in which the maximal phase of its corresponding countertrace is not active. Reporting such invariants may help to better understand vacuous results (e.g. as in #530) and their implications, as for example needed to approach #438.