check
added support for contract cases, length/max/min attributes, if
expressions
added support for loop invariant and loop variant
updating expected results