Supporting quantified formulas?

[rainoftime]

Is there any plan for supporting quantified SMT formulas?

[ccadar]

@rainoftime sorry for the huge delay, but in short we have no plans to add support for quantified formulas.

Such formulas would be extremely expensive to handle via fuzzing because we would need to resort to brute force to evaluate them. We discussed this, and some ideas for making this feasible could be:

• Use skolemization to remove universal quantifiers
• Replace each quantified expression with a boolean variable. If we can find a solution via fuzzing, ask Z3 to solve the quantified expressions along with the model that we found by fuzzing. This is basically breaking the original constraints into subproblems and trying to get different solvers to solver the subproblems, in the hope that we can combine the solutions to the subproblems.