On 18 February 2013 17:21, Colin Adams <colinpauladams@gmail.com> wrote:
Having temporarily switched off invariant checking for the et_tools cluster, I now get a precondition violation:

The value of an_int is 74440, which way exceeds the platform maximum of 255.
The last_literal concerned is 0xFFFD. 

an_int_small_enough: PRECONDITION_VIOLATION raised (PRECONDITION_VIOLATION)

And if I bypass the precondition check, then the postcondition fails.