TESTING: added yet another test case.
WYCS: minor tweaking.
WYIL: added support for verification condition generation through try-catch blocks.