diff --git a/regression/ansi-c/contracts_scope1/main.c b/regression/ansi-c/contracts_scope1/main.c
new file mode 100644
index 00000000000..5c9cc925eb5
--- /dev/null
+++ b/regression/ansi-c/contracts_scope1/main.c
@@ -0,0 +1,28 @@
+#define C 8
+
+typedef unsigned st[C];
+
+// clang-format off
+void init_st(st dst)
+  __CPROVER_requires(__CPROVER_is_fresh(dst, sizeof(st)))
+  __CPROVER_assigns(__CPROVER_object_whole(dst))
+  __CPROVER_ensures(__CPROVER_forall {
+    unsigned i; (0 <= i && i < C) ==> dst[i] == 0
+  });
+// clang-format on
+
+void init_st(st dst)
+{
+  __CPROVER_size_t i;
+  for(i = 0; i < C; i++)
+  {
+    dst[i] = 0;
+  }
+}
+
+int main()
+{
+  st dest;
+
+  init_st(dest);
+}
diff --git a/regression/ansi-c/contracts_scope1/test.desc b/regression/ansi-c/contracts_scope1/test.desc
new file mode 100644
index 00000000000..466da18b2b5
--- /dev/null
+++ b/regression/ansi-c/contracts_scope1/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$
diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y
index 92ce6cae565..59e320f7112 100644
--- a/src/ansi-c/parser.y
+++ b/src/ansi-c/parser.y
@@ -3337,17 +3337,27 @@ parameter_abstract_declarator:
         ;
 
 cprover_function_contract:
-          TOK_CPROVER_ENSURES '(' ACSL_binding_expression ')'
+          TOK_CPROVER_ENSURES
+        {
+          PARSER.new_scope("ensures::");
+        }
+          '(' ACSL_binding_expression ')'
         {
           $$=$1;
           set($$, ID_C_spec_ensures);
-          mto($$, $3);
+          mto($$, $4);
+          PARSER.pop_scope();
         }
-        | TOK_CPROVER_REQUIRES '(' ACSL_binding_expression ')'
+        | TOK_CPROVER_REQUIRES
+        {
+          PARSER.new_scope("requires::");
+        }
+          '(' ACSL_binding_expression ')'
         {
           $$=$1;
           set($$, ID_C_spec_requires);
-          mto($$, $3);
+          mto($$, $4);
+          PARSER.pop_scope();
         }
         | cprover_contract_assigns
         | cprover_contract_frees