SMT support for solvers which do not support quantifiers
We should support SMT solvers even if they do not support quantifiers, like Yices 2 and mathsat.
This can be done by applying a transformation that removes quantified hypotheses, like it is done already for Colibri I think (see !112 (closed))