Hi Lorenzo, I am now now playing with Contract library and trying to break it. I checked that the framework checks the class invariant even when member function exits via an exception. This is an expected behavior and the framework is working fine. However, I note that the precondition of a (non-member) function is not checked when the function exits via throwing an exception. See the following program: # include <contract.hpp> double get_random_weight() { return -1.0; // erroneous implementation } CONTRACT_FUNCTION ( void (set_weight)( (double&) w ) postcondition(w >= 0.0) ) { w = get_random_weight(); if (w < 0.0) throw 1; // (*) } int main() try { double w = 0.0; set_weight(w); } catch (...) { std::cerr << "CAUGHT EXCEPTION" << std::endl; } Function set_weight() is intended to assign its (output) argument with a value representing weight (in the physical sense). We guarantee that the value we set is always non-negative. The function clumsily attempts to verify the condition itself (the line with *). It signals the failure with an exception, but unfortunately fails to satisfy the postcondition. I expect that this situation should be reported as a postcondition violation. But no violation is reported, and the program successfully outputs "CAUGHT EXCEPTION". Regards, &rzej