split_all_full raises out of memory on float theory
Hello,
Using split_all_full on goals containing the ieee_float theory can result in out of memory (see attached file b.mlw ). Most likely, on the hypothesis fma_special, the negative monoid generated by split_core grows exponentially (which eventually eat all available memory).
I encountered this problem when launching the strategy "1" (problem which should be solved by #282 (closed)).
Is it possible to optimize the generation of monoids during the transformation, stop the splitting done by the transformation when it grows to a critical size, or disallow part of the splitting ?