VCs that follow statements like:
Clears(S);
Do not reflect that S should be the empty_string.
Log in to post a comment.
