diff --git a/regression/ansi-c/code_contracts1/main.c b/regression/ansi-c/code_contracts1/main.c
new file mode 100644
index 00000000000..114d2437322
--- /dev/null
+++ b/regression/ansi-c/code_contracts1/main.c
@@ -0,0 +1,22 @@
+// clang-format off
+int foo()
+__CPROVER_ensures(__CPROVER_forall {int i; 1 == 1})
+// clang-format on
+{
+  return 1;
+}
+
+// clang-format off
+int bar()
+__CPROVER_ensures(__CPROVER_forall {int i; 1 == 1} &&
+                  __CPROVER_return_value == 1)
+// clang-format on
+{
+  return 1;
+}
+
+int main()
+{
+  foo();
+  bar();
+}
diff --git a/regression/ansi-c/code_contracts1/test.desc b/regression/ansi-c/code_contracts1/test.desc
new file mode 100644
index 00000000000..466da18b2b5
--- /dev/null
+++ b/regression/ansi-c/code_contracts1/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$
diff --git a/regression/contracts/function_check_02/main.c b/regression/contracts/function_check_02/main.c
index 020113bd1d5..a959109ea0e 100644
--- a/regression/contracts/function_check_02/main.c
+++ b/regression/contracts/function_check_02/main.c
@@ -1,8 +1,6 @@
 // function_check_02
 
 // This test checks the use of quantifiers in ensures clauses.
-// A known bug (resolved in PR #2278) causes the use of quantifiers
-// in ensures to fail.
 
 int initialize(int *arr)
   __CPROVER_ensures(
diff --git a/regression/contracts/function_check_02/test.desc b/regression/contracts/function_check_02/test.desc
index 9c4d3556c69..587dc8622eb 100644
--- a/regression/contracts/function_check_02/test.desc
+++ b/regression/contracts/function_check_02/test.desc
@@ -1,10 +1,7 @@
-KNOWNBUG
+CORE
 main.c
---check-code-contracts
+--apply-code-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
---
-Ensures statements currently do not allow quantified predicates unless the
-function has void return type.
diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp
index 5ff383ec0a8..872dfedd4c5 100644
--- a/src/ansi-c/c_typecheck_base.cpp
+++ b/src/ansi-c/c_typecheck_base.cpp
@@ -748,11 +748,15 @@ void c_typecheck_baset::typecheck_declaration(
       typet ret_type = void_type();
       if(new_symbol.type.id()==ID_code)
         ret_type=to_code_type(new_symbol.type).return_type();
-      assert(parameter_map.empty());
       if(ret_type.id()!=ID_empty)
+      {
+        DATA_INVARIANT(
+          parameter_map.empty(), "parameter map should be cleared");
         parameter_map[CPROVER_PREFIX "return_value"] = ret_type;
+      }
       typecheck_spec_expr(static_cast<codet &>(contract), ID_C_spec_ensures);
-      parameter_map.clear();
+      if(ret_type.id() != ID_empty)
+        parameter_map.clear();
 
       irept assigns_to_add = contract.find(ID_C_spec_assigns);
       if(assigns_to_add.is_not_nil())