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

@@ -1580,10 +1580,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);
@@ -1724,16 +1720,12 @@ 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);
     return;
   }
-  else if(expr.id() == ID_and || expr.id() == ID_or)
+  else if(expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_implies)
   {
     check_rec_logical_op(expr, guard);
     return;