simplifier now simplifies !(exists/forall) with multiple bindings

The simplifier can now simplify !exists and !forall with multiple bindings.

Author: kroening

src/util/simplify_expr_boolean.cpp

@@ -204,14 +204,14 @@ simplify_exprt::resultt<> simplify_exprt::simplify_not(const not_exprt &expr)
   else if(op.id()==ID_exists) // !(exists: a) <-> forall: not a
   {
     auto const &op_as_exists = to_exists_expr(op);
-    return forall_exprt{op_as_exists.symbol(),
-                        simplify_not(not_exprt(op_as_exists.where()))};
+    return forall_exprt{
+      op_as_exists.variables(), simplify_not(not_exprt(op_as_exists.where()))};
   }
   else if(op.id() == ID_forall) // !(forall: a) <-> exists: not a
   {
     auto const &op_as_forall = to_forall_expr(op);
-    return exists_exprt{op_as_forall.symbol(),
-                        simplify_not(not_exprt(op_as_forall.where()))};
+    return exists_exprt{
+      op_as_forall.variables(), simplify_not(not_exprt(op_as_forall.where()))};
   }
 
   return unchanged(expr);