safeWordLength doesn't work for the new formulas with letter quantifiers

[juanrh]

safeWordLength can now only be compute for the subset of formulas corresponding to the old formulas. For example we can have a formula that uses a Now that builds an eventually with a timeout defined on the value of the current word, which is completely dynamic and cannot be bounded at the time the formula is defined. Hence safeWordLength should now be def safeWordLength : Option[Timeout] and use the Option monad to propagate None up in a formula as required

[juanrh]

for now this only applies to the branch quantifiers_experiments