WyC: added support for parsing while-loop invariants.
WyC: for simplicity commented out verification from all valid tests (for now)
WyC: updated the syntax for references on the new valid test cases.