Bug fixes and added invariant evaluation modulo basic ops.
Refined Case2 and fixed Case3.