WyCS: added support for reporting time out errors.
This is particularly useful for debugging, since it tells you
immediately what kind of problem it is.
WyC: added test case for loop invariant + quantifiers.
Since loop invariants and quantifiers are the current blind spot, this
seems like a sensible option!