Add a handling of the case of ID_implies to the check_rec dispatcher in goto_check.

That allows the `guard` expression to be properly instantiated based on the antecedent
expression of the implication statement instead of it inheriting a `true_exprt` as
a `guard`.

This allows checks that are constrained by an expression in the antecedent, such
as pointer checks in the consequent of an implication inside a `__CPROVER_forall`
statement to be correctly bound and checked.

Author: NlightNFotis

src/analyses/goto_check.cpp

@@ -1736,7 +1736,7 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard)
     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;