Oracles provide a way to discard candidate invariants. The safety and
correctness of Cubicle does not depend on the oracle, so any answer
can be returned. However the efficiency of BRAB does. So the more
precise the oracle, the better !
module type S =