Class-invariant is being executed after post-condition throws an AssertionError

[BenRomberg]

This probably also happens if the pre-condition throws an AssertionError. The only time the class-invariant is not executed is when the method itself throws a non-AssertionError.

To sum up, the behavior should be as follows:

• Pre-condition fails -> no further execution
• Method fails with AssertionError -> no further execution
• Method fails with non-AE -> execute Post-Condition
• Post-condition fails -> no further execution