Stop skipping of quantifier expressions in check_rec.

This now allows us to generate checks inside `__CPROVER_forall`
and `__CPROVER_exists` statements.

Related to issue #6231.

Author: NlightNFotis

src/analyses/goto_check.cpp

@@ -1583,10 +1583,6 @@ void goto_checkt::add_guarded_property(
 
 void goto_checkt::check_rec_address(const exprt &expr, guardt &guard)
 {
-  // we don't look into quantifiers
-  if(expr.id() == ID_exists || expr.id() == ID_forall)
-    return;
-
   if(expr.id() == ID_dereference)
   {
     check_rec(to_dereference_expr(expr).pointer(), guard);
@@ -1729,10 +1725,6 @@ void goto_checkt::check_rec_arithmetic_op(const exprt &expr, guardt &guard)
 
 void goto_checkt::check_rec(const exprt &expr, guardt &guard)
 {
-  // we don't look into quantifiers
-  if(expr.id() == ID_exists || expr.id() == ID_forall)
-    return;
-
   if(expr.id() == ID_address_of)
   {
     check_rec_address(to_address_of_expr(expr).object(), guard);