add an option to do WDBA-minimization only when we are sure it will succeed
This includes cases where the input formula is an Obligation, or when the automaton has a good form. The intent is to avoid translating and minimizing the negation, and then making some products, and emptiness checks.
We could do that for --determinize --low
, maybe.