don't fail on quantifiers with more than one symbol

This adds support for eager instantiation of forall or exists quantifier
expressions that have more than one symbol using the trivial rewrite.

Author: kroening

regression/smt2_solver/quantifiers/boolean-quantifier.desc

@@ -0,0 +1,7 @@
+CORE
+boolean-quantifier.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^sat$
+--

regression/smt2_solver/quantifiers/boolean-quantifier.smt2

@@ -0,0 +1,13 @@
+(assert (exists ((b Bool)) b))
+(assert (exists ((b Bool)) (not b)))
+
+(assert (not (forall ((b Bool)) b)))
+(assert (not (forall ((b Bool)) (not b))))
+
+(assert (exists ((a Bool) (b Bool)) (= a b)))
+(assert (not (forall ((a Bool) (b Bool)) (= a b))))
+
+(assert (forall ((a Bool)) (exists ((b Bool)) (= a b))))
+
+(check-sat)
+(get-model)

src/solvers/flattening/boolbv_quantifier.cpp

@@ -142,6 +142,18 @@ static optionalt<exprt> eager_quantifier_instantiation(
   const quantifier_exprt &expr,
   const namespacet &ns)
 {
+  if(expr.variables().size() > 1)
+  {
+    // Qx,y.P(x,y) is the same as Qx.Qy.P(x,y)
+    auto new_variables = expr.variables();
+    new_variables.pop_back();
+    auto new_expression = quantifier_exprt(
+      expr.id(),
+      expr.variables().back(),
+      quantifier_exprt(expr.id(), new_variables, expr.where()));
+    return eager_quantifier_instantiation(new_expression, ns);
+  }
+
   const symbol_exprt &var_expr = expr.symbol();
 
   /**