Do not apply fmfBound to standard quantifiers when only stringsExp is enabled (#6816)

Do not apply fmfBound to standard quantifiers when only stringsExp is enabled (#6816)

There are compelling use cases that combine strings/sequences and quantifiers. Prior to this PR, strings enabled "bounded integer" quantifier instantiation so that internally generated quantifiers for strings reductions are handled in a complete manner. However, this enabled bounded integer quantifier instantiation globally. This degrades performance for "unsat" on quantified formulas in general.

After this PR, we do not enable bounded integer quantifier globally. Instead, we ensure that bounded integer quantification is applied to at least the internally generated quantified formulas; all other quantified formulas are handled as usual.

Notice this required ensuring that all quantified formulas generated by strings are marked properly. It also required adding --fmf-bound to a few regressions that explicitly require it.