diff --git a/regression/contracts/quantifiers-exists-both-01/main.c b/regression/contracts/quantifiers-exists-both-01/main.c
deleted file mode 100644
index c123d0c837d..00000000000
--- a/regression/contracts/quantifiers-exists-both-01/main.c
+++ /dev/null
@@ -1,18 +0,0 @@
-// clang-format off
-int f1(int *arr) __CPROVER_requires(__CPROVER_exists {
-  int i;
-  (0 <= i && i < 8) ==> arr[i] == 0
-}) __CPROVER_ensures(__CPROVER_exists {
-  int i;
-  (0 <= i && i < 8) ==> arr[i] == 0
-})
-// clang-format on
-{
-  return 0;
-}
-
-int main()
-{
-  int arr[8];
-  f1(arr);
-}
diff --git a/regression/contracts/quantifiers-exists-both-01/test.desc b/regression/contracts/quantifiers-exists-both-01/test.desc
deleted file mode 100644
index ee6c03641c5..00000000000
--- a/regression/contracts/quantifiers-exists-both-01/test.desc
+++ /dev/null
@@ -1,13 +0,0 @@
-CORE
-main.c
---enforce-all-contracts
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
---
-The purpose of this test is to ensure that we can safely use __CPROVER_exists
-in a negative context (which is currently not always the case). By using the
---enforce-all-contracts flag, this test assumes the statement in 
-__CPROVER_requires, then asserts the same statement (in __CPROVER_ensures),
-thus, verification should be successful.
diff --git a/regression/contracts/quantifiers-exists-both-02/main.c b/regression/contracts/quantifiers-exists-both-02/main.c
deleted file mode 100644
index d5a5655bb3d..00000000000
--- a/regression/contracts/quantifiers-exists-both-02/main.c
+++ /dev/null
@@ -1,18 +0,0 @@
-// clang-format off
-int f1(int *arr, int *len) __CPROVER_requires(__CPROVER_exists {
-  int i;
-  (0 <= i && i < len) ==> arr[i] == 0
-}) __CPROVER_ensures(__CPROVER_exists {
-  int i;
-  (0 <= i && i < len) ==> arr[i] == 0
-})
-// clang-format on
-{
-  return 0;
-}
-
-int main()
-{
-  int len, arr[8];
-  f1(arr, len);
-}
diff --git a/regression/contracts/quantifiers-exists-both-02/test.desc b/regression/contracts/quantifiers-exists-both-02/test.desc
deleted file mode 100644
index a8ecf5ff952..00000000000
--- a/regression/contracts/quantifiers-exists-both-02/test.desc
+++ /dev/null
@@ -1,19 +0,0 @@
-KNOWNBUG
-main.c
---enforce-all-contracts
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
---
-The purpose of this test is to ensure that we can safely use __CPROVER_exists
-in a negative context (which is currently not always the case). By using the
---enforce-all-contracts flag, this test assumes the statement in 
-__CPROVER_requires, then asserts the same statement (in __CPROVER_ensures),
-thus, verification should be successful.
-
-Known bug:
-The current implementation cannot handle a structure such as
-__CPROVER_assume(__CPROVER_exists(int i; pred(i))), where i is
-not explicitly bounded to a predefined range (i.e. if at least
-one of its bound is only declared and not defined).
diff --git a/regression/contracts/quantifiers-exists-ensures-01/main.c b/regression/contracts/quantifiers-exists-both-enforce/main.c
similarity index 51%
rename from regression/contracts/quantifiers-exists-ensures-01/main.c
rename to regression/contracts/quantifiers-exists-both-enforce/main.c
index ad4d3964ed3..d245284d067 100644
--- a/regression/contracts/quantifiers-exists-ensures-01/main.c
+++ b/regression/contracts/quantifiers-exists-both-enforce/main.c
@@ -1,22 +1,20 @@
 // clang-format off
 int f1(int *arr)
-  __CPROVER_assigns(*arr)
+  __CPROVER_requires(__CPROVER_exists {
+    int i;
+    (0 <= i && i < 8) && arr[i] == 0
+  })
   __CPROVER_ensures(__CPROVER_exists {
     int i;
-    (0 <= i && i < 10) ==> arr[i] == i
+    (0 <= i && i < 8) && arr[i] == 0
   })
 // clang-format on
 {
-  for(int i = 0; i < 10; i++)
-  {
-    arr[i] = i;
-  }
-
   return 0;
 }
 
 int main()
 {
-  int arr[10];
+  int arr[8];
   f1(arr);
 }
diff --git a/regression/contracts/quantifiers-exists-both-enforce/test.desc b/regression/contracts/quantifiers-exists-both-enforce/test.desc
new file mode 100644
index 00000000000..433b9abb6a1
--- /dev/null
+++ b/regression/contracts/quantifiers-exists-both-enforce/test.desc
@@ -0,0 +1,16 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^\[1\] assertion: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+The purpose of this test is to ensure that we can safely use __CPROVER_exists within both
+positive and negative contexts (ENSURES and REQUIRES clauses).
+
+With the SAT backend existential quantifiers in a positive context,
+e.g., the ENSURES clause being enforced in this case,
+are supported only if the quantifier is bound to a constant range.
diff --git a/regression/contracts/quantifiers-exists-both-replace/main.c b/regression/contracts/quantifiers-exists-both-replace/main.c
new file mode 100644
index 00000000000..85360a7f075
--- /dev/null
+++ b/regression/contracts/quantifiers-exists-both-replace/main.c
@@ -0,0 +1,42 @@
+#include <stdlib.h>
+
+#define MAX_LEN 8
+
+// clang-format off
+int f1(int *arr, int len)
+  __CPROVER_requires(
+    len > 0 ==> __CPROVER_exists {
+      int i;
+      // constant bounds for explicit unrolling with SAT backend
+      (0 <= i && i < MAX_LEN) && (
+        // actual symbolic bound for `i`
+        i < len && arr[i] == 0
+      )
+    }
+  )
+  __CPROVER_ensures(
+    len > 0 ==> __CPROVER_exists {
+      int i;
+      // constant bounds for explicit unrolling with SAT backend
+      (0 <= i && i < MAX_LEN) && (
+        // actual symbolic bound for `i`
+        i < len && arr[i] == 0
+      )
+    }
+  )
+// clang-format on
+{
+  return 0;
+}
+
+int main()
+{
+  int len;
+  __CPROVER_assume(0 <= len && len <= MAX_LEN);
+
+  int *arr = malloc(len);
+  if(len > 0)
+    arr[0] = 0;
+
+  f1(arr, len);
+}
diff --git a/regression/contracts/quantifiers-exists-both-replace/test.desc b/regression/contracts/quantifiers-exists-both-replace/test.desc
new file mode 100644
index 00000000000..2bafb11eaf0
--- /dev/null
+++ b/regression/contracts/quantifiers-exists-both-replace/test.desc
@@ -0,0 +1,16 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=0$
+^SIGNAL=0$
+^\[1\] assertion: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+The purpose of this test is to ensure that we can safely use __CPROVER_exists within both
+positive and negative contexts (ENSURES and REQUIRES clauses).
+
+With the SAT backend existential quantifiers in a positive context,
+e.g., the REQUIRES clause being replaced in this case,
+are supported only if the quantifier is bound to a constant range.
diff --git a/regression/contracts/quantifiers-exists-ensures-01/test.desc b/regression/contracts/quantifiers-exists-ensures-01/test.desc
deleted file mode 100644
index f1d037caa5f..00000000000
--- a/regression/contracts/quantifiers-exists-ensures-01/test.desc
+++ /dev/null
@@ -1,12 +0,0 @@
-CORE
-main.c
---enforce-all-contracts
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
---
-The purpose of this test is to ensure that we can safely use __CPROVER_exists
-in __CPROVER_ensures clauses. By using the --enforce-all-contracts flag, 
-goto-instrument will transform the __CPROVER_ensures clauses into an
-assertion and the verification remains sound when using __CPROVER_exists.
diff --git a/regression/contracts/quantifiers-exists-ensures-02/main.c b/regression/contracts/quantifiers-exists-ensures-02/main.c
deleted file mode 100644
index ea2a2fa88ac..00000000000
--- a/regression/contracts/quantifiers-exists-ensures-02/main.c
+++ /dev/null
@@ -1,20 +0,0 @@
-// clang-format off
-int f1(int *arr) __CPROVER_ensures(__CPROVER_exists {
-  int i;
-  (0 <= i && i < 10) ==> arr[i] != 0
-})
-// clang-format on
-{
-  for(int i = 0; i < 10; i++)
-  {
-    arr[i] = 0;
-  }
-
-  return 0;
-}
-
-int main()
-{
-  int arr[10];
-  f1(arr);
-}
diff --git a/regression/contracts/quantifiers-exists-ensures-02/test.desc b/regression/contracts/quantifiers-exists-ensures-02/test.desc
deleted file mode 100644
index 473f8e20622..00000000000
--- a/regression/contracts/quantifiers-exists-ensures-02/test.desc
+++ /dev/null
@@ -1,19 +0,0 @@
-CORE
-main.c
---enforce-all-contracts
-^EXIT=10$
-^SIGNAL=0$
-^VERIFICATION FAILED$
---
---
-The purpose of this test is to ensure that we can safely use __CPROVER_exists
-in __CPROVER_ensures clauses. By using the --enforce-all-contracts flag, 
-goto-instrument will transform the __CPROVER_ensures clauses into an
-assertion and the verification remains sound when using __CPROVER_exists.
-
-Known Bug:
-We expect verification to fail because arr[i] is always equal to 0 for
-[0 <= i < 10]. In fact, we expect the (0 <= i && i < 10) statement to act as a
-range for i. However, in the current implementation of quantifier handling,
-the (0 <= i && i < 10) statement is not interpreted as an explicit range, but
-instead, as part of a logic formula, which causes verification to succeed.
diff --git a/regression/contracts/quantifiers-exists-ensures-enforce/main.c b/regression/contracts/quantifiers-exists-ensures-enforce/main.c
new file mode 100644
index 00000000000..1194c2968de
--- /dev/null
+++ b/regression/contracts/quantifiers-exists-ensures-enforce/main.c
@@ -0,0 +1,40 @@
+// clang-format off
+int f1(int *arr)
+  __CPROVER_assigns(*arr)
+  __CPROVER_ensures(__CPROVER_exists {
+    int i;
+    (0 <= i && i < 10) && arr[i] == i
+  })
+// clang-format on
+{
+  for(int i = 0; i < 10; i++)
+  {
+    arr[i] = i;
+  }
+
+  return 0;
+}
+
+// clang-format off
+int f2(int *arr)
+  __CPROVER_assigns(*arr)
+  __CPROVER_ensures(__CPROVER_exists {
+    int i;
+    (0 <= i && i < 10) && arr[i] != 0
+  })
+// clang-format on
+{
+  for(int i = 0; i < 10; i++)
+  {
+    arr[i] = 0;
+  }
+
+  return 0;
+}
+
+int main()
+{
+  int arr[10];
+  f2(arr);
+  f1(arr);
+}
diff --git a/regression/contracts/quantifiers-exists-ensures-enforce/test.desc b/regression/contracts/quantifiers-exists-ensures-enforce/test.desc
new file mode 100644
index 00000000000..dfe6e1ae24c
--- /dev/null
+++ b/regression/contracts/quantifiers-exists-ensures-enforce/test.desc
@@ -0,0 +1,15 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
+The purpose of this test is to ensure that we can safely use __CPROVER_exists
+within positive contexts (enforced ENSURES clauses).
+
+With the SAT backend existential quantifiers in a positive context,
+e.g., the ENSURES clause being enforced in this case,
+are supported only if the quantifier is bound to a constant range.
diff --git a/regression/contracts/quantifiers-exists-ensures-replace/main.c b/regression/contracts/quantifiers-exists-ensures-replace/main.c
new file mode 100644
index 00000000000..caacb3e5ccb
--- /dev/null
+++ b/regression/contracts/quantifiers-exists-ensures-replace/main.c
@@ -0,0 +1,41 @@
+#include <assert.h>
+#include <stdbool.h>
+#include <stdlib.h>
+
+#define MAX_LEN 128
+
+// clang-format off
+int f1(int *arr, int len)
+  __CPROVER_ensures(
+    len > 0 ==> __CPROVER_exists {
+      int i;
+      // test replacement with symbolic bound
+      (0 <= i && i < len) && arr[i] == 0
+    }
+  )
+// clang-format on
+{
+  // we are only checking for contract replacement
+  return 0;
+}
+
+int main()
+{
+  int len;
+  __CPROVER_assume(0 <= len && len <= MAX_LEN);
+
+  int *arr = malloc(len * sizeof(int));
+
+  f1(arr, len);
+
+  bool found_zero = false;
+  for(int i = 0; i <= MAX_LEN; i++)
+  {
+    if(i < len)
+      found_zero |= (arr[i] == 0);
+  }
+
+  // clang-format off
+  assert(len > 0 ==> found_zero);
+  // clang-format on
+}
diff --git a/regression/contracts/quantifiers-exists-ensures-replace/test.desc b/regression/contracts/quantifiers-exists-ensures-replace/test.desc
new file mode 100644
index 00000000000..09144241702
--- /dev/null
+++ b/regression/contracts/quantifiers-exists-ensures-replace/test.desc
@@ -0,0 +1,14 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] line .* assertion len > 0 ==> found_zero: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+The purpose of this test is to ensure that we can safely use __CPROVER_exists
+within negative contexts (replaced ENSURES clauses).
+
+This is fully supported (without requiring full unrolling) with the SAT backend.
diff --git a/regression/contracts/quantifiers-exists-requires-01/main.c b/regression/contracts/quantifiers-exists-requires-01/main.c
deleted file mode 100644
index aefde2c93bc..00000000000
--- a/regression/contracts/quantifiers-exists-requires-01/main.c
+++ /dev/null
@@ -1,15 +0,0 @@
-// clang-format off
-int f1(int *arr) __CPROVER_requires(__CPROVER_exists {
-  int i;
-  (0 <= i && i < 10) ==> arr[i] == 4
-}) __CPROVER_ensures(__CPROVER_return_value == 0)
-// clang-format on
-{
-  return 0;
-}
-
-int main()
-{
-  int arr[10] = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9};
-  f1(arr);
-}
diff --git a/regression/contracts/quantifiers-exists-requires-01/test.desc b/regression/contracts/quantifiers-exists-requires-01/test.desc
deleted file mode 100644
index 60d164515f5..00000000000
--- a/regression/contracts/quantifiers-exists-requires-01/test.desc
+++ /dev/null
@@ -1,12 +0,0 @@
-CORE
-main.c
---replace-all-calls-with-contracts
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
---
-The purpose of this test is to ensure that we can safely use __CPROVER_exists
-in __CPROVER_requires clauses. By using the --replace-all-calls-with-contracts
-flag, goto-instrument will transform the __CPROVER_requires clauses into an
-assertion and the verification remains sound when using __CPROVER_exists.
diff --git a/regression/contracts/quantifiers-exists-requires-02/main.c b/regression/contracts/quantifiers-exists-requires-02/main.c
deleted file mode 100644
index db36c3c41c9..00000000000
--- a/regression/contracts/quantifiers-exists-requires-02/main.c
+++ /dev/null
@@ -1,15 +0,0 @@
-// clang-format off
-int f1(int *arr) __CPROVER_requires(__CPROVER_exists {
-  int i;
-  (0 <= i && i < 10) ==> arr[i] == 1
-}) __CPROVER_ensures(__CPROVER_return_value == 0)
-// clang-format on
-{
-  return 0;
-}
-
-int main()
-{
-  int arr[10] = {0, 0, 0, 0, 0, 0, 0, 0, 0, 0};
-  f1(arr);
-}
diff --git a/regression/contracts/quantifiers-exists-requires-02/test.desc b/regression/contracts/quantifiers-exists-requires-02/test.desc
deleted file mode 100644
index f00b0c7fdb2..00000000000
--- a/regression/contracts/quantifiers-exists-requires-02/test.desc
+++ /dev/null
@@ -1,19 +0,0 @@
-KNOWNBUG
-main.c
---replace-all-calls-with-contracts
-^EXIT=10$
-^SIGNAL=0$
-^VERIFICATION FAILED$
---
---
-The purpose of this test is to ensure that we can safely use __CPROVER_exists
-in __CPROVER_requires clauses. By using the --replace-all-calls-with-contracts
-flag, goto-instrument will transform the __CPROVER_requires clauses into an
-assertion and the verification remains sound when using __CPROVER_exists.
-
-Known Bug:
-We expect verification to fail because arr[i] is never equal to 1 for
-[0 <= i < 10]. In fact, we expect the (0 <= i && i < 10) statement to act as a
-range for i. However, in the current implementation of quantifier handling,
-the (0 <= i && i < 10) statement is not interpreted as an explicit range, but
-instead, as part of a logic formula, which causes verification to succeed.
diff --git a/regression/contracts/quantifiers-exists-requires-enforce/main.c b/regression/contracts/quantifiers-exists-requires-enforce/main.c
new file mode 100644
index 00000000000..7985f57de3b
--- /dev/null
+++ b/regression/contracts/quantifiers-exists-requires-enforce/main.c
@@ -0,0 +1,39 @@
+#include <stdbool.h>
+#include <stdlib.h>
+
+#define MAX_LEN 64
+
+// clang-format off
+bool f1(int *arr, int len)
+  __CPROVER_requires(
+    len > 0 ==> __CPROVER_exists {
+      int i;
+      // test enforcement with symbolic bound
+      (0 <= i && i < len) && arr[i] == 4
+    }
+  )
+  __CPROVER_ensures(
+    __CPROVER_return_value == true
+  )
+// clang-format on
+{
+  bool found_four = false;
+  for(int i = 0; i <= MAX_LEN; i++)
+  {
+    if(i < len)
+      found_four |= (arr[i] == 4);
+  }
+
+  // clang-format off
+  return (len > 0 ==> found_four);
+  // clang-format on
+}
+
+int main()
+{
+  int len;
+  __CPROVER_assume(0 <= len && len <= MAX_LEN);
+
+  int *arr = malloc(len * sizeof(int));
+  f1(arr, len);
+}
diff --git a/regression/contracts/quantifiers-exists-requires-enforce/test.desc b/regression/contracts/quantifiers-exists-requires-enforce/test.desc
new file mode 100644
index 00000000000..898df96cf06
--- /dev/null
+++ b/regression/contracts/quantifiers-exists-requires-enforce/test.desc
@@ -0,0 +1,14 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^\[1\] assertion: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+The purpose of this test is to ensure that we can safely use __CPROVER_exists
+within both negative contexts (enforced REQUIRES clauses).
+
+This is fully supported (without requiring full unrolling) with the SAT backend.
diff --git a/regression/contracts/quantifiers-exists-requires-replace/main.c b/regression/contracts/quantifiers-exists-requires-replace/main.c
new file mode 100644
index 00000000000..f7c1e5f896a
--- /dev/null
+++ b/regression/contracts/quantifiers-exists-requires-replace/main.c
@@ -0,0 +1,34 @@
+// clang-format off
+int f1(int *arr)
+  __CPROVER_requires(__CPROVER_exists {
+    int i;
+    (0 <= i && i < 10) && arr[i] == 0
+  })
+  __CPROVER_ensures(
+    __CPROVER_return_value == 0
+  )
+// clang-format on
+{
+  return 0;
+}
+
+// clang-format off
+int f2(int *arr)
+  __CPROVER_requires(__CPROVER_exists {
+    int i;
+    (0 <= i && i < 10) && arr[i] == 1
+  })
+  __CPROVER_ensures(
+    __CPROVER_return_value == 0
+  )
+// clang-format on
+{
+  return 0;
+}
+
+int main()
+{
+  int arr[10] = {0, 0, 0, 0, 0, 0, 0, 0, 0, 0};
+  f1(arr);
+  f2(arr);
+}
diff --git a/regression/contracts/quantifiers-exists-requires-replace/test.desc b/regression/contracts/quantifiers-exists-requires-replace/test.desc
new file mode 100644
index 00000000000..9d310e67dd7
--- /dev/null
+++ b/regression/contracts/quantifiers-exists-requires-replace/test.desc
@@ -0,0 +1,17 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=10$
+^SIGNAL=0$
+^\[1\] assertion: SUCCESS$
+^\[2\] assertion: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
+The purpose of this test is to ensure that we can safely use __CPROVER_exists
+within both positive contexts (replaced REQUIRES clauses).
+
+With the SAT backend existential quantifiers in a positive context,
+e.g., the REQUIRES clause being replaced in this case,
+are supported only if the quantifier is bound to a constant range.
diff --git a/regression/contracts/quantifiers-forall-both-01/main.c b/regression/contracts/quantifiers-forall-both-01/main.c
deleted file mode 100644
index a9533000171..00000000000
--- a/regression/contracts/quantifiers-forall-both-01/main.c
+++ /dev/null
@@ -1,18 +0,0 @@
-// clang-format off
-int f1(int *arr) __CPROVER_requires(__CPROVER_forall {
-  int i;
-  (0 <= i && i < 8) ==> arr[i] == 0
-}) __CPROVER_ensures(__CPROVER_forall {
-  int i;
-  (0 <= i && i < 8) ==> arr[i] == 0
-})
-// clang-format on
-{
-  return 0;
-}
-
-int main()
-{
-  int arr[8];
-  f1(arr);
-}
diff --git a/regression/contracts/quantifiers-forall-both-01/test.desc b/regression/contracts/quantifiers-forall-both-01/test.desc
deleted file mode 100644
index c7f16fc8c51..00000000000
--- a/regression/contracts/quantifiers-forall-both-01/test.desc
+++ /dev/null
@@ -1,13 +0,0 @@
-CORE
-main.c
---enforce-all-contracts
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
---
-The purpose of this test is to ensure that we can safely use __CPROVER_forall
-in a negative context (which is currently not always the case). By using the
---enforce-all-contracts flag, this test assumes the statement in
-__CPROVER_requires, then asserts the same statement (in __CPROVER_ensures), 
-thus, verification should be successful.
diff --git a/regression/contracts/quantifiers-forall-both-02/main.c b/regression/contracts/quantifiers-forall-both-02/main.c
deleted file mode 100644
index d173dba1469..00000000000
--- a/regression/contracts/quantifiers-forall-both-02/main.c
+++ /dev/null
@@ -1,18 +0,0 @@
-// clang-format off
-int f1(int *arr, int len) __CPROVER_requires(__CPROVER_forall {
-  int i;
-  (0 <= i && i < len) ==> arr[i] == 0
-}) __CPROVER_ensures(__CPROVER_forall {
-  int i;
-  (0 <= i && i < len) ==> arr[i] == 0
-})
-// clang-format on
-{
-  return 0;
-}
-
-int main()
-{
-  int len, arr[8];
-  f1(arr, len);
-}
diff --git a/regression/contracts/quantifiers-forall-both-02/test.desc b/regression/contracts/quantifiers-forall-both-02/test.desc
deleted file mode 100644
index 8b2381cfb3f..00000000000
--- a/regression/contracts/quantifiers-forall-both-02/test.desc
+++ /dev/null
@@ -1,19 +0,0 @@
-KNOWNBUG
-main.c
---enforce-all-contracts
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
---
-The purpose of this test is to ensure that we can safely use __CPROVER_forall
-in a negative context (which is currently not always the case). By using the
---enforce-all-contracts flag, this test assumes the statement in
-__CPROVER_requires, then asserts the same statement (in __CPROVER_ensures), 
-thus, verification should be successful.
-
-Known bug:
-The current implementation cannot handle a structure such as
-__CPROVER_assume(__CPROVER_forall(int i; pred(i))), where i is
-not explicitly bounded to a predefined range (i.e. if at least
-one of its bound is only declared and not defined).
diff --git a/regression/contracts/quantifiers-forall-ensures-01/main.c b/regression/contracts/quantifiers-forall-both-enforce/main.c
similarity index 51%
rename from regression/contracts/quantifiers-forall-ensures-01/main.c
rename to regression/contracts/quantifiers-forall-both-enforce/main.c
index 7e601ea0282..d47d59bcc3e 100644
--- a/regression/contracts/quantifiers-forall-ensures-01/main.c
+++ b/regression/contracts/quantifiers-forall-both-enforce/main.c
@@ -1,22 +1,20 @@
 // clang-format off
 int f1(int *arr)
-  __CPROVER_assigns(*arr)
+  __CPROVER_requires(__CPROVER_forall {
+    int i;
+    (0 <= i && i < 8) ==> arr[i] == 0
+  })
   __CPROVER_ensures(__CPROVER_forall {
     int i;
-    (0 <= i && i < 10) ==> arr[i] == 0
+    (0 <= i && i < 8) ==> arr[i] == 0
   })
 // clang-format on
 {
-  for(int i = 0; i < 10; i++)
-  {
-    arr[i] = 0;
-  }
-
   return 0;
 }
 
 int main()
 {
-  int arr[10];
+  int arr[8];
   f1(arr);
 }
diff --git a/regression/contracts/quantifiers-forall-both-enforce/test.desc b/regression/contracts/quantifiers-forall-both-enforce/test.desc
new file mode 100644
index 00000000000..994099cac27
--- /dev/null
+++ b/regression/contracts/quantifiers-forall-both-enforce/test.desc
@@ -0,0 +1,16 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^\[1\] assertion: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+The purpose of this test is to ensure that we can safely use __CPROVER_forall within both
+positive and negative contexts (ENSURES and REQUIRES clauses).
+
+With the SAT backend universal quantifiers in a negative context,
+e.g., the REQUIRES clause being enforced in this case,
+are supported only if the quantifier is bound to a constant range.
diff --git a/regression/contracts/quantifiers-forall-both-replace/main.c b/regression/contracts/quantifiers-forall-both-replace/main.c
new file mode 100644
index 00000000000..0bfda4af0e1
--- /dev/null
+++ b/regression/contracts/quantifiers-forall-both-replace/main.c
@@ -0,0 +1,38 @@
+#include <stdlib.h>
+
+#define MAX_LEN 8
+
+// clang-format off
+int f1(int *arr, int len)
+  __CPROVER_requires(__CPROVER_forall {
+    int i;
+    // constant bounds for explicit unrolling with SAT backend
+    (0 <= i && i < MAX_LEN) ==> (
+      // actual symbolic bound for `i`
+      i < len ==> arr[i] == 0
+    )
+  })
+  __CPROVER_ensures(__CPROVER_forall {
+    int i;
+    // positive context, so symbolic bounds are fine
+    (0 <= i && i < len) ==> arr[i] == 0
+  })
+// clang-format on
+{
+  return 0;
+}
+
+int main()
+{
+  int len;
+  __CPROVER_assume(0 <= len && len <= MAX_LEN);
+
+  int *arr = malloc(len);
+  for(int i = 0; i < MAX_LEN; ++i)
+  {
+    if(i < len)
+      arr[i] = 0;
+  }
+
+  f1(arr, len);
+}
diff --git a/regression/contracts/quantifiers-forall-both-replace/test.desc b/regression/contracts/quantifiers-forall-both-replace/test.desc
new file mode 100644
index 00000000000..6b1e25a914c
--- /dev/null
+++ b/regression/contracts/quantifiers-forall-both-replace/test.desc
@@ -0,0 +1,16 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=0$
+^SIGNAL=0$
+^\[1\] assertion: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+The purpose of this test is to ensure that we can safely use __CPROVER_forall within both
+positive and negative contexts (ENSURES and REQUIRES clauses).
+
+With the SAT backend universal quantifiers in a negative context,
+e.g., the ENSURES clause being replaced in this case,
+are supported only if the quantifier is bound to a constant range.
diff --git a/regression/contracts/quantifiers-forall-ensures-01/test.desc b/regression/contracts/quantifiers-forall-ensures-01/test.desc
deleted file mode 100644
index 44769e5ca27..00000000000
--- a/regression/contracts/quantifiers-forall-ensures-01/test.desc
+++ /dev/null
@@ -1,12 +0,0 @@
-CORE
-main.c
---enforce-all-contracts
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
---
-The purpose of this test is to ensure that we can safely use __CPROVER_forall
-in __CPROVER_ensures clauses. By using the --enforce-all-contracts
-flag, goto-instrument will transform the __CPROVER_ensures clauses into an
-assertion and the verification remains sound when using __CPROVER_forall.
diff --git a/regression/contracts/quantifiers-forall-ensures-02/main.c b/regression/contracts/quantifiers-forall-ensures-02/main.c
deleted file mode 100644
index 7904224f227..00000000000
--- a/regression/contracts/quantifiers-forall-ensures-02/main.c
+++ /dev/null
@@ -1,23 +0,0 @@
-// clang-format off
-int f1(int *arr) __CPROVER_ensures(__CPROVER_forall {
-  int i;
-  (0 <= i && i < 10) ==> arr[i] == i
-})
-// clang-format on
-{
-  for(int i = 0; i < 10; i++)
-  {
-    if(i == 0)
-      arr[i] = -1;
-    else
-      arr[i] = i;
-  }
-
-  return 0;
-}
-
-int main()
-{
-  int arr[10];
-  f1(arr);
-}
diff --git a/regression/contracts/quantifiers-forall-ensures-02/test.desc b/regression/contracts/quantifiers-forall-ensures-02/test.desc
deleted file mode 100644
index 3058ae57fd4..00000000000
--- a/regression/contracts/quantifiers-forall-ensures-02/test.desc
+++ /dev/null
@@ -1,12 +0,0 @@
-CORE
-main.c
---enforce-all-contracts
-^EXIT=10$
-^SIGNAL=0$
-^VERIFICATION FAILED$
---
---
-The purpose of this test is to ensure that we can safely use __CPROVER_forall
-in __CPROVER_ensures clauses. By using the --enforce-all-contracts
-flag, goto-instrument will transform the __CPROVER_ensures clauses into an
-assertion and the verification remains sound when using __CPROVER_forall.
diff --git a/regression/contracts/quantifiers-forall-ensures-enforce/main.c b/regression/contracts/quantifiers-forall-ensures-enforce/main.c
new file mode 100644
index 00000000000..78271197aec
--- /dev/null
+++ b/regression/contracts/quantifiers-forall-ensures-enforce/main.c
@@ -0,0 +1,30 @@
+#include <stdlib.h>
+
+#define MAX_LEN 16
+
+// clang-format off
+int f1(int *arr, int len)
+  __CPROVER_assigns(*arr)
+  __CPROVER_ensures(__CPROVER_forall {
+    int i;
+    // test enforcement with symbolic bound
+    (0 <= i && i < len) ==> arr[i] == 0
+  })
+// clang-format on
+{
+  for(int i = 0; i < MAX_LEN; i++)
+  {
+    if(i < len)
+      arr[i] = 0;
+  }
+  return 0;
+}
+
+int main()
+{
+  int len;
+  __CPROVER_assume(0 <= len && len <= MAX_LEN);
+
+  int *arr = malloc(len * sizeof(int));
+  f1(arr, len);
+}
diff --git a/regression/contracts/quantifiers-forall-ensures-enforce/test.desc b/regression/contracts/quantifiers-forall-ensures-enforce/test.desc
new file mode 100644
index 00000000000..63cc32c4b1d
--- /dev/null
+++ b/regression/contracts/quantifiers-forall-ensures-enforce/test.desc
@@ -0,0 +1,14 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^\[1\] assertion: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+The purpose of this test is to ensure that we can safely use __CPROVER_forall
+within positive contexts (enforced ENSURES clauses).
+
+This is fully supported (without requiring full unrolling) with the SAT backend.
diff --git a/regression/contracts/quantifiers-forall-ensures-replace/main.c b/regression/contracts/quantifiers-forall-ensures-replace/main.c
new file mode 100644
index 00000000000..8a9da439097
--- /dev/null
+++ b/regression/contracts/quantifiers-forall-ensures-replace/main.c
@@ -0,0 +1,30 @@
+#include <assert.h>
+#include <stdbool.h>
+
+// clang-format off
+int f1(int *arr)
+  __CPROVER_ensures(__CPROVER_forall {
+    int i;
+    (0 <= i && i < 10) ==> arr[i] == i
+  })
+// clang-format on
+{
+  return 0;
+}
+
+int main()
+{
+  int arr[10];
+
+  f1(arr);
+
+  bool check = true;
+  for(int i = 0; i < 10; i++)
+  {
+    if(i == 0)
+      check &= (arr[i] = -1);
+    else
+      check &= (arr[i] = i);
+  }
+  assert(check);
+}
diff --git a/regression/contracts/quantifiers-forall-ensures-replace/test.desc b/regression/contracts/quantifiers-forall-ensures-replace/test.desc
new file mode 100644
index 00000000000..2fb1c6b035c
--- /dev/null
+++ b/regression/contracts/quantifiers-forall-ensures-replace/test.desc
@@ -0,0 +1,16 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=10$
+^SIGNAL=0$
+^\[main.assertion.1\] line .* assertion check: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
+The purpose of this test is to ensure that we can safely use __CPROVER_forall
+within negative contexts (replaced ENSURES clauses).
+
+With the SAT backend universal quantifiers within a negative context,
+e.g., the ENSURES clause being replaced in this case,
+are supported only if the quantifier is bound to a constant range.
diff --git a/regression/contracts/quantifiers-forall-requires-01/main.c b/regression/contracts/quantifiers-forall-requires-01/main.c
deleted file mode 100644
index 6470ce98056..00000000000
--- a/regression/contracts/quantifiers-forall-requires-01/main.c
+++ /dev/null
@@ -1,15 +0,0 @@
-// clang-format off
-int f1(int *arr) __CPROVER_requires(__CPROVER_forall {
-  int i;
-  (0 <= i && i < 10) ==> arr[i] == i
-}) __CPROVER_ensures(__CPROVER_return_value == 0)
-// clang-format on
-{
-  return 0;
-}
-
-int main()
-{
-  int arr[10] = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9};
-  f1(arr);
-}
diff --git a/regression/contracts/quantifiers-forall-requires-01/test.desc b/regression/contracts/quantifiers-forall-requires-01/test.desc
deleted file mode 100644
index cb5fe8567b9..00000000000
--- a/regression/contracts/quantifiers-forall-requires-01/test.desc
+++ /dev/null
@@ -1,12 +0,0 @@
-CORE
-main.c
---replace-all-calls-with-contracts
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
---
-The purpose of this test is to ensure that we can safely use __CPROVER_forall
-in __CPROVER_requires clauses. By using the --replace-all-calls-with-contracts
-flag, goto-instrument will transform the __CPROVER_requires clauses into an
-assertion and the verification remains sound when using __CPROVER_forall.
diff --git a/regression/contracts/quantifiers-forall-requires-02/main.c b/regression/contracts/quantifiers-forall-requires-02/main.c
deleted file mode 100644
index b8c4caab137..00000000000
--- a/regression/contracts/quantifiers-forall-requires-02/main.c
+++ /dev/null
@@ -1,15 +0,0 @@
-// clang-format off
-int f1(int *arr) __CPROVER_requires(__CPROVER_forall {
-  int i;
-  (0 <= i && i < 10) ==> arr[i] == i
-}) __CPROVER_ensures(__CPROVER_return_value == 0)
-// clang-format on
-{
-  return 0;
-}
-
-int main()
-{
-  int arr[10] = {-1, 1, 2, 3, 4, 5, 6, 7, 8, 9};
-  f1(arr);
-}
diff --git a/regression/contracts/quantifiers-forall-requires-02/test.desc b/regression/contracts/quantifiers-forall-requires-02/test.desc
deleted file mode 100644
index f841a39d8c8..00000000000
--- a/regression/contracts/quantifiers-forall-requires-02/test.desc
+++ /dev/null
@@ -1,12 +0,0 @@
-CORE
-main.c
---replace-all-calls-with-contracts
-^EXIT=10$
-^SIGNAL=0$
-^VERIFICATION FAILED$
---
---
-The purpose of this test is to ensure that we can safely use __CPROVER_forall
-in __CPROVER_requires clauses. By using the --replace-all-calls-with-contracts
-flag, goto-instrument will transform the __CPROVER_requires clauses into an
-assertion and the verification remains sound when using __CPROVER_forall.
diff --git a/regression/contracts/quantifiers-forall-requires-enforce/main.c b/regression/contracts/quantifiers-forall-requires-enforce/main.c
new file mode 100644
index 00000000000..fe0da19e0ca
--- /dev/null
+++ b/regression/contracts/quantifiers-forall-requires-enforce/main.c
@@ -0,0 +1,24 @@
+#include <stdbool.h>
+
+// clang-format off
+bool f1(int *arr)
+  __CPROVER_requires(__CPROVER_forall {
+    int i;
+    (0 <= i && i < 10) ==> arr[i] == i
+  })
+  __CPROVER_ensures(
+    __CPROVER_return_value == true
+  )
+// clang-format on
+{
+  bool is_identity = true;
+  for(int i = 0; i < 10; ++i)
+    is_identity &= (arr[i] == i);
+  return is_identity;
+}
+
+int main()
+{
+  int arr[10];
+  f1(arr);
+}
diff --git a/regression/contracts/quantifiers-forall-requires-enforce/test.desc b/regression/contracts/quantifiers-forall-requires-enforce/test.desc
new file mode 100644
index 00000000000..143e769cc31
--- /dev/null
+++ b/regression/contracts/quantifiers-forall-requires-enforce/test.desc
@@ -0,0 +1,16 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^\[1\] assertion: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+The purpose of this test is to ensure that we can safely use __CPROVER_forall
+within negative contexts (enforced REQUIRES clauses).
+
+With the SAT backend universal quantifiers within a negative context,
+e.g., the REQUIRES clause being enforced in this case,
+are supported only if the quantifier is bound to a constant range.
diff --git a/regression/contracts/quantifiers-forall-requires-replace/main.c b/regression/contracts/quantifiers-forall-requires-replace/main.c
new file mode 100644
index 00000000000..6c086f98719
--- /dev/null
+++ b/regression/contracts/quantifiers-forall-requires-replace/main.c
@@ -0,0 +1,33 @@
+#include <stdlib.h>
+
+#define MAX_LEN 16
+
+// clang-format off
+int f1(int *arr, int len)
+  __CPROVER_requires(__CPROVER_forall {
+    int i;
+    // test replacement with symbolic bound
+    (0 <= i && i < len) ==> arr[i] == i
+  })
+  __CPROVER_ensures(
+    __CPROVER_return_value == 0
+  )
+// clang-format on
+{
+  return 0;
+}
+
+int main()
+{
+  int len;
+  __CPROVER_assume(0 <= len && len <= MAX_LEN);
+
+  int *arr = malloc(len * sizeof(int));
+  for(int i = 0; i < MAX_LEN; ++i)
+  {
+    if(i < len)
+      arr[i] = i;
+  }
+
+  f1(arr, len);
+}
diff --git a/regression/contracts/quantifiers-forall-requires-replace/test.desc b/regression/contracts/quantifiers-forall-requires-replace/test.desc
new file mode 100644
index 00000000000..63970dc4173
--- /dev/null
+++ b/regression/contracts/quantifiers-forall-requires-replace/test.desc
@@ -0,0 +1,14 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=0$
+^SIGNAL=0$
+^\[1\] assertion: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+The purpose of this test is to ensure that we can safely use __CPROVER_forall
+within positive contexts (replaced REQUIRES clauses).
+
+This is fully supported (without requiring full unrolling) with the SAT backend.
\ No newline at end of file
diff --git a/regression/contracts/quantifiers-loop-01/test.desc b/regression/contracts/quantifiers-loop-01/test.desc
index b5f89638ead..be46c230b33 100644
--- a/regression/contracts/quantifiers-loop-01/test.desc
+++ b/regression/contracts/quantifiers-loop-01/test.desc
@@ -8,6 +8,7 @@ main.c
 ^\[main.assertion.1\] line .* assertion a\[10\] == 1: SUCCESS
 ^VERIFICATION SUCCESSFUL$
 --
+^warning: ignoring
 --
 This test case checks the handling of a `forall` quantifier within a loop invariant.
 
diff --git a/regression/contracts/quantifiers-loop-02/test.desc b/regression/contracts/quantifiers-loop-02/test.desc
index 7774449f536..d5367bac034 100644
--- a/regression/contracts/quantifiers-loop-02/test.desc
+++ b/regression/contracts/quantifiers-loop-02/test.desc
@@ -1,6 +1,6 @@
-KNOWNBUG smt-backend broken-cprover-smt-backend
+CORE
 main.c
---enforce-all-contracts
+--enforce-all-contracts _ --z3
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.1\] line .* Check loop invariant before entry: SUCCESS
@@ -8,14 +8,15 @@ main.c
 ^\[main.assertion.1\] line .* assertion .*: SUCCESS
 ^VERIFICATION SUCCESSFUL$
 --
+^warning: ignoring
 --
 This test case checks the handling of a universal quantifier, with a symbolic
 upper bound, within a loop invariant.
 
-The test is tagged:
-- `smt-backend`:
+TODO: This test should:
+- be tagged `smt-backend`:
   because the SAT backend does not support (simply ignores) `forall` in negative (e.g. assume) contexts.
-- `broken-cprover-smt-backend`:
+- be tagged `broken-cprover-smt-backend`:
   because the CPROVER SMT2 solver cannot handle (errors out on) `forall` in negative (e.g. assume) contexts.
-
-It has been tagged `KNOWNBUG` for now since `contracts` regression tests are not run with SMT backend yet.
+- not use the `_ --z3` parameters:
+  once SMT-related tags are supported by the `Makefile`.
diff --git a/regression/contracts/quantifiers-loop-03/test.desc b/regression/contracts/quantifiers-loop-03/test.desc
index e728ab44d5b..429c07e0ec2 100644
--- a/regression/contracts/quantifiers-loop-03/test.desc
+++ b/regression/contracts/quantifiers-loop-03/test.desc
@@ -8,6 +8,7 @@ main.c
 ^\[main.assertion.1\] line .* assertion .*: SUCCESS
 ^VERIFICATION SUCCESSFUL$
 --
+^warning: ignoring
 --
 This test case checks the handling of an existential quantifier, with a symbolic
 upper bound, within a loop invariant.
diff --git a/regression/contracts/quantifiers-nested-01/test.desc b/regression/contracts/quantifiers-nested-01/test.desc
index 3a6b85c370b..cb7cecc36ae 100644
--- a/regression/contracts/quantifiers-nested-01/test.desc
+++ b/regression/contracts/quantifiers-nested-01/test.desc
@@ -5,7 +5,7 @@ main.c
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
+^warning: ignoring
 --
-Verification:
 This test case checks the handling of a forall expression
 nested within another forall expression.
diff --git a/regression/contracts/quantifiers-nested-02/main.c b/regression/contracts/quantifiers-nested-02/main.c
index 7cfa3051c01..0e43fb11d53 100644
--- a/regression/contracts/quantifiers-nested-02/main.c
+++ b/regression/contracts/quantifiers-nested-02/main.c
@@ -1,12 +1,16 @@
 // clang-format off
-int f1(int *arr) __CPROVER_requires(__CPROVER_forall {
-  int i;
-  0 <= i && i < 9 ==> __CPROVER_forall
-  {
-    int j;
-    (i <= j && j < 10) ==> arr[i] <= arr[j]
-  }
-}) __CPROVER_ensures(__CPROVER_return_value == 0)
+int f1(int *arr)
+  __CPROVER_requires(
+    __CPROVER_forall {
+    int i;
+    (0 <= i && i < 9) ==> __CPROVER_forall {
+      int j;
+      (i <= j && j < 10) ==> arr[i] <= arr[j]
+    }}
+  )
+  __CPROVER_ensures(
+    __CPROVER_return_value == 0
+  )
 // clang-format on
 {
   return 0;
diff --git a/regression/contracts/quantifiers-nested-02/test.desc b/regression/contracts/quantifiers-nested-02/test.desc
index 218e27b3671..0aaf256d1f9 100644
--- a/regression/contracts/quantifiers-nested-02/test.desc
+++ b/regression/contracts/quantifiers-nested-02/test.desc
@@ -5,7 +5,7 @@ main.c
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
+^warning: ignoring
 --
-Verification:
 This test case checks the handling of a forall expression
 nested within an implication.
diff --git a/regression/contracts/quantifiers-nested-03/main.c b/regression/contracts/quantifiers-nested-03/main.c
index eb991a2c8b2..ec26b365f81 100644
--- a/regression/contracts/quantifiers-nested-03/main.c
+++ b/regression/contracts/quantifiers-nested-03/main.c
@@ -1,8 +1,14 @@
-int f1(int *arr) __CPROVER_assigns(*arr)
-  __CPROVER_ensures(__CPROVER_return_value == 0 && __CPROVER_exists {
-    int i;
-    (0 <= i && i < 10) && arr[i] == i
-  })
+// clang-format off
+int f1(int *arr)
+__CPROVER_assigns(*arr)
+  __CPROVER_ensures(
+    __CPROVER_return_value == 0 &&
+    __CPROVER_exists {
+      int i;
+      (0 <= i && i < 10) && arr[i] == i
+    }
+  )
+// clang-format on
 {
   for(int i = 0; i < 10; i++)
   {
diff --git a/regression/contracts/quantifiers-nested-03/test.desc b/regression/contracts/quantifiers-nested-03/test.desc
index ceeb1710f4b..4a811b6dcf8 100644
--- a/regression/contracts/quantifiers-nested-03/test.desc
+++ b/regression/contracts/quantifiers-nested-03/test.desc
@@ -5,7 +5,7 @@ main.c
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
+^warning: ignoring
 --
-Verification:
 This test case checks the handling of an exists expression
 nested within a conjunction.
diff --git a/regression/contracts/quantifiers-nested-04/main.c b/regression/contracts/quantifiers-nested-04/main.c
index 82def4f61ce..41d875577dd 100644
--- a/regression/contracts/quantifiers-nested-04/main.c
+++ b/regression/contracts/quantifiers-nested-04/main.c
@@ -1,14 +1,19 @@
 // clang-format off
-int f1(int *arr) __CPROVER_requires(
-  __CPROVER_forall {
-    int i;
-    (0 <= i && i < 10) ==> arr[i] == 0
-  } ||
-  arr[9] == -1 ||
-  __CPROVER_exists {
-    int i;
-    (0 <= i && i < 10) && arr[i] == i
-  }) __CPROVER_ensures(__CPROVER_return_value == 0)
+int f1(int *arr)
+  __CPROVER_requires(
+    __CPROVER_forall {
+      int i;
+      (0 <= i && i < 10) ==> arr[i] == 0
+    } ||
+    arr[9] == -1 ||
+    __CPROVER_exists {
+      int i;
+      (0 <= i && i < 10) && arr[i] == i
+    }
+  )
+  __CPROVER_ensures(
+    __CPROVER_return_value == 0
+  )
 // clang-format on
 {
   return 0;
diff --git a/regression/contracts/quantifiers-nested-04/test.desc b/regression/contracts/quantifiers-nested-04/test.desc
index 8bd89966cbb..4f92cb05f86 100644
--- a/regression/contracts/quantifiers-nested-04/test.desc
+++ b/regression/contracts/quantifiers-nested-04/test.desc
@@ -5,7 +5,7 @@ main.c
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
+^warning: ignoring
 --
-Verification:
 This test case checks the handling of both a forall expression
 and an exists expression nested within a disjunction.
diff --git a/regression/contracts/quantifiers-nested-05/main.c b/regression/contracts/quantifiers-nested-05/main.c
index 6aa20e2cc7f..f667b14b177 100644
--- a/regression/contracts/quantifiers-nested-05/main.c
+++ b/regression/contracts/quantifiers-nested-05/main.c
@@ -1,8 +1,14 @@
 // clang-format off
-int f1(int *arr) __CPROVER_requires(!__CPROVER_forall {
-    int i;
-    (0 <= i && i < 10) ==> arr[i] == 0
-  }) __CPROVER_ensures(__CPROVER_return_value == 0)
+int f1(int *arr)
+  __CPROVER_requires(
+    !__CPROVER_forall {
+      int i;
+      (0 <= i && i < 10) ==> arr[i] == 0
+    }
+  )
+  __CPROVER_ensures(
+    __CPROVER_return_value == 0
+  )
 // clang-format on
 {
   return 0;
diff --git a/regression/contracts/quantifiers-nested-05/test.desc b/regression/contracts/quantifiers-nested-05/test.desc
index ceb27f76675..674b9bfc0b4 100644
--- a/regression/contracts/quantifiers-nested-05/test.desc
+++ b/regression/contracts/quantifiers-nested-05/test.desc
@@ -5,7 +5,7 @@ main.c
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
+^warning: ignoring
 --
-Verification:
 This test case checks the handling of a forall expression
 nested within a negation.
diff --git a/regression/contracts/quantifiers-nested-06/main.c b/regression/contracts/quantifiers-nested-06/main.c
index 28d2bf24add..fda936fb03e 100644
--- a/regression/contracts/quantifiers-nested-06/main.c
+++ b/regression/contracts/quantifiers-nested-06/main.c
@@ -1,20 +1,31 @@
+#include <stdbool.h>
+
 // clang-format off
-int f1(int *arr) __CPROVER_requires(
-  (__CPROVER_forall {
-    int i;
-    (0 <= i && i < 10) ==> arr[i] == 0
-  } ? __CPROVER_exists {
-    int i;
-    (0 <= i && i < 10) ==> arr[i] == 0
-  } : 1 == 0) &&
-  (__CPROVER_forall {
-    int i;
-    (0 <= i && i < 10) ==> arr[i] == i
-  } ? 1 == 0 :
+int f1(int *arr)
+  __CPROVER_requires(
+    (
+      __CPROVER_forall {
+        int i;
+        (0 <= i && i < 10) ==> arr[i] == 0
+      } ?
+      __CPROVER_exists {
+        int i;
+        (0 <= i && i < 10) ==> arr[i] == 0
+      } : false
+  ) && (
     __CPROVER_forall {
       int i;
-      (0 <= i && i < 10) ==> arr[i] == 0
-  })) __CPROVER_ensures(__CPROVER_return_value == 0)
+      (0 <= i && i < 10) ==> arr[i] == i
+    } ? false :
+      __CPROVER_forall {
+        int i;
+        (0 <= i && i < 10) ==> arr[i] == 0
+      }
+    )
+  )
+  __CPROVER_ensures(
+    __CPROVER_return_value == 0
+  )
 // clang-format on
 {
   return 0;
diff --git a/regression/contracts/quantifiers-nested-06/test.desc b/regression/contracts/quantifiers-nested-06/test.desc
index c2485334e38..941828fdeca 100644
--- a/regression/contracts/quantifiers-nested-06/test.desc
+++ b/regression/contracts/quantifiers-nested-06/test.desc
@@ -5,7 +5,7 @@ main.c
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
+^warning: ignoring
 --
-Verification:
 This test case checks the handling of forall and exists expressions
 nested within ternary ITE expressions (condition ? true : false).