diff --git a/regression/cbmc-primitives/implication_statement_checks_1/test.c b/regression/cbmc-primitives/implication_statement_checks_1/test.c
new file mode 100644
index 00000000000..a340bce64d6
--- /dev/null
+++ b/regression/cbmc-primitives/implication_statement_checks_1/test.c
@@ -0,0 +1,10 @@
+// clang-format off
+int main(int argc, char **argv)
+{
+    int y;
+
+    __CPROVER_assert(
+        y != 0 ==> 10 / y <= 10,
+        "10 / y is expected to succeed");
+}
+// clang-format on
diff --git a/regression/cbmc-primitives/implication_statement_checks_1/test.desc b/regression/cbmc-primitives/implication_statement_checks_1/test.desc
new file mode 100644
index 00000000000..2342fe5ad35
--- /dev/null
+++ b/regression/cbmc-primitives/implication_statement_checks_1/test.desc
@@ -0,0 +1,16 @@
+CORE
+--div-by-zero-check
+test.c
+^EXIT=0$
+^SIGNAL=0$
+\[main\.assertion\.1\] line \d 10 / y is expected to succeed: SUCCESS
+\[main\.division-by-zero\.1\] line \d division by zero in 10 / y: SUCCESS
+^VERIFICATION SUCCESSFUL$
+--
+\[main\.division-by-zero\.1\] line \d division by zero in 10 / y: FAILURE
+--
+Without the change that drives the refinement of the guard for a `ID_implies`
+statement in `goto-check`, this will fail with a counterexample of `y = 0`.
+With the bug fix, the `--div-by-zero-check` will succeed because the
+antecedent of the conditional is becoming the guard for the consequent,
+guarding any checks performed there.
diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
index b65855454d4..1bdb812a092 100644
--- a/src/analyses/goto_check.cpp
+++ b/src/analyses/goto_check.cpp
@@ -1606,6 +1606,8 @@ void goto_checkt::check_rec_address(const exprt &expr, guardt &guard)
 
 void goto_checkt::check_rec_logical_op(const exprt &expr, guardt &guard)
 {
+  PRECONDITION(
+    expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_implies);
   INVARIANT(
     expr.is_boolean(),
     "'" + expr.id_string() + "' must be Boolean, but got " + expr.pretty());
@@ -1736,7 +1738,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;