WyC: Updated CodeGenerator for Various Invariants.

After the introduction of the new Assert and Assume blocks, the
CodeGenerator has now been updated to create appropriate assert and
assume blocks for loop invariants and pre/post-conditions.
WyIL: Working on getting the asserts vs assumptions to work.