added special syntax to reason about the return value of methods in the post condition, added some equivalent mutants (c# code), changed while loops to generate smaller wlp formulas if the loop does not affect the post condition