The one place for your designs
To enable design management, you'll need to meet the requirements. If you need help, reach out to our support team for assistance.
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)