Add positive test for fix of implication statement antecedent guard refinement.

Before this change the division-by-zero check would fail because the antecedent
part of the implication statement wouldn't be used to refine the guard of any
checks performed in the consequent part of the statement.

Author: NlightNFotis

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

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.