This restricts the time spent in translating sub-formulas for
implication tests by limiting the associated automata to 64 states by
default.  Doing so this does worsen any test case, and actually remove
all calls the BuDDy's GC in bdd.test.

* spot/twaalgos/translate.cc, spot/twaalgos/translate.hh,
spot/tl/simplify.cc, spot/tl/simplify.hh, spot/tl/contain.hh,
spot/tl/contain.cc, spot/twaalgos/ltl2tgba_fm.cc,
spot/twaalgos/ltl2tgba_fm.hh: Add support for the option or
its constraint via an output_aborter.
* bin/spot-x.cc, NEWS: Document it.
* tests/core/bdd.test: Adjust and augment test case.