Consider not removing all props in `smt-lib-floats.gen`
Currently the smt-lib-floats.gen
removes all props. Probably it aims at using exclusively the built-in support for floats in SMT solvers. Yet, there are properties that are removed that are not known by solvers, so it might be better to remove less props.
An example are the lemma max_int_def
and max_real_def
which are removed, thus the counterexample exhibit values 0 and 0.0 for them, which is clearly incorrect.