The behavior is expected because the ECF states that EiffelBase uses the `application options' and the ECF of the application is requesting for precondition checking so they are always checked regardless of that `supplier_precondition' value. I've changed the Ace for that test to not use `application options' for EiffelBase and the test passes. I haven't committed the change, I just want to confirm with you first.