The strongest-postcondition (i.e. forward propagation) verifier is approaching feature parity with the weakest-precondition (i.e. backwards propagation) verifier. As we consider changes which will break compatibility with the weakest-precondition verifier, we should decide at what point it's worth simply deprecating it rather than porting those changes.
The following changes would break the backward-propagation verifier and likely motivate deprecating it:
Changing the stack equivalence domain to be addressed by stack slots (rather than pointers)
Removing the polarity flag from the equivalence domain (i.e. only supporting negative polarities)
The strongest-postcondition (i.e. forward propagation) verifier is approaching feature parity with the weakest-precondition (i.e. backwards propagation) verifier. As we consider changes which will break compatibility with the weakest-precondition verifier, we should decide at what point it's worth simply deprecating it rather than porting those changes.
The following changes would break the backward-propagation verifier and likely motivate deprecating it: