Insufficient preconditions in modules of `mach.float`
The predicates representing preconditions expressed in real, such as add_pre_real
, should also require that arguments are both finite, otherwise the preconditions with a disjunction would accept non finite numbers.
Alternatively, those modules may define another type t
as a record with one field and an invariant that the value of the field is finite. Yet it should be carefully reviewed that adding a type invariant here would not induced a too large extra bunch of VCs.