diff --git a/regression/cbmc/Quantifiers-assertion/main.c b/regression/cbmc/Quantifiers-assertion/main.c
index 65bd350eae1..8fc2442c03b 100644
--- a/regression/cbmc/Quantifiers-assertion/main.c
+++ b/regression/cbmc/Quantifiers-assertion/main.c
@@ -7,9 +7,12 @@ int main()
   c[1][0]=1;
   c[1][1]=2;
 
+  // clang-format off
+  // clang-format would rewrite the "==>" as "== >"
   __CPROVER_assert(__CPROVER_exists { int i; (i>=0 && i<2) ==> (__CPROVER_exists{int j; (j>=0 && j<2) ==> c[i][j]>=1 && c[i][j]<=10}) }, "Exists-Exists: successful");
 
-  __CPROVER_assert(!__CPROVER_exists { int i; (i>=0 && i<2) ==> (!__CPROVER_exists{int j; (j>=0 && j<2) ==> c[i][j]>=1 && c[i][j]<=10}) }, "NotExists-NotExists: successful");
+  // NOLINTNEXTLINE(whitespace/line_length)
+  __CPROVER_assert(!__CPROVER_exists { int i; (i>=0 && i<2) ==> (!__CPROVER_exists{int j; (j>=0 && j<2) ==> c[i][j]>=1 && c[i][j]<=10}) }, "NotExists-NotExists: failed");
 
   __CPROVER_assert(!__CPROVER_exists { int i; (i>=0 && i<2) ==> (__CPROVER_exists{int j; (j>=0 && j<2) ==> c[i][j]>=1 && c[i][j]<=10}) }, "NotExists-Exists: failed");
 
@@ -18,6 +21,7 @@ int main()
   __CPROVER_assert(!__CPROVER_forall { int i; (i>=0 && i<2) ==> (__CPROVER_forall{int j; (j>=0 && j<2) ==> c[i][j]>=1 && c[i][j]<=10}) }, "NotForall-Forall: successful");
 
   __CPROVER_assert(!__CPROVER_forall { int i; (i>=0 && i<2) ==> (!__CPROVER_forall{int j; (j>=0 && j<2) ==> c[i][j]>=1 && c[i][j]<=10}) }, "NotForall-NotForall: successful");
+  // clang-format on
 
   return 0;
 }
diff --git a/regression/cbmc/Quantifiers-assertion/test.desc b/regression/cbmc/Quantifiers-assertion/test.desc
index 8f2e25b3d90..419831fd273 100644
--- a/regression/cbmc/Quantifiers-assertion/test.desc
+++ b/regression/cbmc/Quantifiers-assertion/test.desc
@@ -1,14 +1,16 @@
-CORE
+KNOWNBUG
 main.c
 
 ^\*\* Results:$
 ^\[main.assertion.1\] .* Exists-Exists: successful: SUCCESS$
-^\[main.assertion.2\] .* NotExists-NotExists: successful: SUCCESS$
+^\[main.assertion.2\] .* NotExists-NotExists: failed: FAILURE$
 ^\[main.assertion.3\] .* NotExists-Exists: failed: FAILURE$
 ^\[main.assertion.4\] .* NotExists-Forall: failed: FAILURE$
 ^\[main.assertion.5\] .* NotForall-Forall: successful: SUCCESS$
 ^\[main.assertion.6\] .* NotForall-NotForall: successful: SUCCESS$
-^\*\* 2 of 6 failed
+^\*\* 3 of 6 failed
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/cbmc/Quantifiers-assignment/main.c b/regression/cbmc/Quantifiers-assignment/main.c
index 3d1efd43bd2..276311fa1ed 100644
--- a/regression/cbmc/Quantifiers-assignment/main.c
+++ b/regression/cbmc/Quantifiers-assignment/main.c
@@ -4,10 +4,13 @@ int main()
   a[0]=1;
   a[1]=2;
 
+  // clang-format off
+  // clang-format would rewrite the "==>" as "== >"
   int x=__CPROVER_forall { int i; (i>=0 && i<2) ==> a[i]>=1 && a[i]<=10 };
   int y=__CPROVER_forall { int i; (i>=0 && i<2) ==> a[i]>=1 && a[i]<2 };
   int z1=__CPROVER_exists { int i; (i>=0 && i<2) ==> a[i]>=1 && a[i]<1.5 };
   int z2=__CPROVER_exists { int i; (i>=0 && i<2) ==> a[i]>=1 && a[i]<2*10 };
+  // clang-format on
 
   assert(x);
   assert(y);
diff --git a/regression/cbmc/Quantifiers-assignment/test.desc b/regression/cbmc/Quantifiers-assignment/test.desc
index d9183316f55..a584f718857 100644
--- a/regression/cbmc/Quantifiers-assignment/test.desc
+++ b/regression/cbmc/Quantifiers-assignment/test.desc
@@ -10,3 +10,5 @@ main.c
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/cbmc/Quantifiers-copy/main.c b/regression/cbmc/Quantifiers-copy/main.c
index d939227149f..60bcfca23de 100644
--- a/regression/cbmc/Quantifiers-copy/main.c
+++ b/regression/cbmc/Quantifiers-copy/main.c
@@ -9,7 +9,10 @@ int main()
   a[3]=3;
   a[4]=4;
 
+  // clang-format off
+  // clang-format would rewrite the "==>" as "== >"
   __CPROVER_assume(__CPROVER_forall { int i; (i>=0 && i<5) ==> b[i]==a[i]});
+  // clang-format on
 
   assert(b[0]==0);
   assert(b[1]==1);
diff --git a/regression/cbmc/Quantifiers-copy/test.desc b/regression/cbmc/Quantifiers-copy/test.desc
index 8b1083602d9..9df184ba1f9 100644
--- a/regression/cbmc/Quantifiers-copy/test.desc
+++ b/regression/cbmc/Quantifiers-copy/test.desc
@@ -11,3 +11,5 @@ main.c
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/cbmc/Quantifiers-if/main.c b/regression/cbmc/Quantifiers-if/main.c
index f8c0bb33f9d..66bfe889214 100644
--- a/regression/cbmc/Quantifiers-if/main.c
+++ b/regression/cbmc/Quantifiers-if/main.c
@@ -4,6 +4,8 @@ int main()
   a[0]=1;
   a[1]=2;
 
+  // clang-format off
+  // clang-format would rewrite the "==>" as "== >"
   if(__CPROVER_forall { int i; (i>=0 && i<2) ==> a[i]>=1 && a[i]<=10 })
     __CPROVER_assert(0, "failure 1");
 
@@ -18,6 +20,7 @@ int main()
 
   if(__CPROVER_exists { int i; (i>=0 && i<2) ==> a[i]>=5 && a[i]<=10 })
     __CPROVER_assert(0, "success 2");
+  // clang-format on
 
   return 0;
 }
diff --git a/regression/cbmc/Quantifiers-if/test.desc b/regression/cbmc/Quantifiers-if/test.desc
index 76bb5083f90..0797ac525b4 100644
--- a/regression/cbmc/Quantifiers-if/test.desc
+++ b/regression/cbmc/Quantifiers-if/test.desc
@@ -11,3 +11,5 @@ main.c
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/cbmc/Quantifiers-initialisation/main.c b/regression/cbmc/Quantifiers-initialisation/main.c
index 99eaa53de95..cef5e169580 100644
--- a/regression/cbmc/Quantifiers-initialisation/main.c
+++ b/regression/cbmc/Quantifiers-initialisation/main.c
@@ -2,7 +2,10 @@ int main()
 {
   int a[5];
 
+  // clang-format off
+  // clang-format would rewrite the "==>" as "== >"
   __CPROVER_assume(__CPROVER_forall { int i; (i>=0 && i<5) ==> a[i]==i+1});
+  // clang-format on
 
   assert(a[0]==1);
   assert(a[1]==2);
diff --git a/regression/cbmc/Quantifiers-initialisation/test.desc b/regression/cbmc/Quantifiers-initialisation/test.desc
index f11fe701a7a..13409c8fa2d 100644
--- a/regression/cbmc/Quantifiers-initialisation/test.desc
+++ b/regression/cbmc/Quantifiers-initialisation/test.desc
@@ -11,3 +11,5 @@ main.c
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/cbmc/Quantifiers-initialisation2/main.c b/regression/cbmc/Quantifiers-initialisation2/main.c
index c4996c3b485..b01c7d2009f 100644
--- a/regression/cbmc/Quantifiers-initialisation2/main.c
+++ b/regression/cbmc/Quantifiers-initialisation2/main.c
@@ -3,6 +3,8 @@ int main()
   int a[10];
   int c[10];
 
+  // clang-format off
+  // clang-format would rewrite the "==>" as "== >"
   // C# style
   __CPROVER_assume(__CPROVER_forall { int i; (i>=0 && i<9+1) ==> a[i]>=1 && a[i]<=10 });
   __CPROVER_assume(__CPROVER_forall { int i; (i>=0 && i<10) ==>  __CPROVER_forall{int j; (j>i && j<10) ==> a[j]>a[i]} });
@@ -14,5 +16,6 @@ int main()
   assert(a[2]>a[3]);
   __CPROVER_assert(__CPROVER_forall {unsigned i; (i>=1 && i<10) ==> c[i-1]<=c[i]}, "forall c[]");
   assert(c[3]>=c[1]);
+  // clang-format on
   return 0;
 }
diff --git a/regression/cbmc/Quantifiers-initialisation2/test.desc b/regression/cbmc/Quantifiers-initialisation2/test.desc
index 5bc13a1a52d..ab42e172aea 100644
--- a/regression/cbmc/Quantifiers-initialisation2/test.desc
+++ b/regression/cbmc/Quantifiers-initialisation2/test.desc
@@ -11,3 +11,5 @@ main.c
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/cbmc/Quantifiers-invalid-var-range/main.c b/regression/cbmc/Quantifiers-invalid-var-range/main.c
index 5bcb3d7c535..41e0ad38908 100644
--- a/regression/cbmc/Quantifiers-invalid-var-range/main.c
+++ b/regression/cbmc/Quantifiers-invalid-var-range/main.c
@@ -2,7 +2,10 @@ int main()
 {
 
   int a[3][3];
+  // clang-format off
+  // clang-format would rewrite the "==>" as "== >"
   __CPROVER_assume(__CPROVER_forall { int i; (i>=0 && i<5) ==>  __CPROVER_exists{int j; (j>=i && j<3) ==> a[i][j]==10} });
+  // clang-format on
 
   assert(a[0][0]==10||a[0][1]==10||a[0][2]==10);
 
diff --git a/regression/cbmc/Quantifiers-invalid-var-range/test.desc b/regression/cbmc/Quantifiers-invalid-var-range/test.desc
index e160567e531..44f67109c0d 100644
--- a/regression/cbmc/Quantifiers-invalid-var-range/test.desc
+++ b/regression/cbmc/Quantifiers-invalid-var-range/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^\*\* Results:$
@@ -6,3 +6,8 @@ main.c
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
+--
+^warning: ignoring
+--
+This produces the expected verification result, but actually ignores some
+quantifiers.
diff --git a/regression/cbmc/Quantifiers-not-exists/fixed.c b/regression/cbmc/Quantifiers-not-exists/fixed.c
new file mode 100644
index 00000000000..800571a3033
--- /dev/null
+++ b/regression/cbmc/Quantifiers-not-exists/fixed.c
@@ -0,0 +1,42 @@
+int main()
+{
+  int a[2][2];
+  int b[2][2];
+  int c[2][2];
+  int d[2][2];
+
+  // clang-format off
+  // clang-format would rewrite the "==>" as "== >"
+  // NOLINTNEXTLINE(whitespace/line_length)
+  __CPROVER_assume(!__CPROVER_exists { int i; (i>=0 && i<2) && (__CPROVER_exists{int j; (j>=0 && j<2) && a[i][j]<=10}) });
+
+  assert(0);
+
+  // NOLINTNEXTLINE(whitespace/line_length)
+  __CPROVER_assume(__CPROVER_forall { int i; (i>=0 && i<2) ==> (!__CPROVER_exists{int j; (j>=0 && j<2) && b[i][j]>=1 && b[i][j]<=10}) });
+
+  assert(0);
+
+  // NOLINTNEXTLINE(whitespace/line_length)
+  __CPROVER_assume(!__CPROVER_exists { int i; (i>=0 && i<2) && (!__CPROVER_exists{int j; (j>=0 && j<2) && (c[i][j]==0 || c[i][j]<=10)}) });
+
+  assert(0);
+
+  // NOLINTNEXTLINE(whitespace/line_length)
+  __CPROVER_assume(!__CPROVER_exists { int i; (i>=0 && i<2) && (__CPROVER_forall{int j; (j>=0 && j<2) ==> d[i][j]>=1 && d[i][j]<=10}) });
+  // clang-format on
+
+  assert(0);
+
+  assert(a[0][0] > 10);
+
+  assert((b[0][0] < 1 || b[0][0] > 10) && (b[0][1] < 1 || b[0][1] > 10));
+  assert((b[1][0] < 1 || b[1][0] > 10) && (b[1][1] < 1 || b[1][1] > 10));
+
+  assert(c[0][0] == 0 || c[0][1] == 0 || c[1][0] <= 10 || c[1][1] <= 10);
+
+  assert(((d[0][0] < 1 || d[0][0] > 10) || (d[0][1] < 1 || d[0][1] > 10)));
+  assert(((d[1][0] < 1 || d[1][0] > 10) || (d[1][1] < 1 || d[1][1] > 10)));
+
+  return 0;
+}
diff --git a/regression/cbmc/Quantifiers-not-exists/fixed.desc b/regression/cbmc/Quantifiers-not-exists/fixed.desc
new file mode 100644
index 00000000000..6d41315fd94
--- /dev/null
+++ b/regression/cbmc/Quantifiers-not-exists/fixed.desc
@@ -0,0 +1,16 @@
+CORE
+fixed.c
+
+^\*\* Results:$
+^\[main.assertion.5\] line 31 assertion a\[.*\]\[.*\] > 10: SUCCESS$
+^\[main.assertion.6\] line 33 assertion tmp_if_expr\$\d+: SUCCESS$
+^\[main.assertion.7\] line 34 assertion tmp_if_expr\$\d+: SUCCESS$
+^\[main.assertion.8\] line 36 assertion tmp_if_expr\$\d+: SUCCESS$
+^\[main.assertion.9\] line 38 assertion tmp_if_expr\$\d+: SUCCESS$
+^\[main.assertion.10\] line 39 assertion tmp_if_expr\$\d+: SUCCESS$
+^\*\* 4 of 10 failed
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/cbmc/Quantifiers-not-exists/main.c b/regression/cbmc/Quantifiers-not-exists/main.c
index d19124f4548..60a3e7cc2bd 100644
--- a/regression/cbmc/Quantifiers-not-exists/main.c
+++ b/regression/cbmc/Quantifiers-not-exists/main.c
@@ -6,14 +6,24 @@ int main()
   int c[2][2];
   int d[2][2];
 
+  // clang-format off
+  // clang-format would rewrite the "==>" as "== >"
   __CPROVER_assume(!__CPROVER_exists { int i; (i>=0 && i<2) ==> (__CPROVER_exists{int j; (j>=0 && j<2) ==> a[i][j]<=10}) });
 
+  assert(0);
+
   __CPROVER_assume(__CPROVER_forall { int i; (i>=0 && i<2) ==> (!__CPROVER_exists{int j; (j>=0 && j<2) ==> b[i][j]>=1 && b[i][j]<=10}) });
 
+  assert(0);
+
   __CPROVER_assume(!__CPROVER_exists { int i; (i>=0 && i<2) ==> (!__CPROVER_exists{int j; (j>=0 && j<2) ==> c[i][j]>=1 && c[i][j]<=10}) });
 
+  assert(0);
+
   __CPROVER_assume(!__CPROVER_exists { int i; (i>=0 && i<2) ==> (__CPROVER_forall{int j; (j>=0 && j<2) ==> d[i][j]>=1 && d[i][j]<=10}) });
+  // clang-format on
 
+  assert(0);
 
   assert(a[0][0]>10);
 
diff --git a/regression/cbmc/Quantifiers-not-exists/test.desc b/regression/cbmc/Quantifiers-not-exists/test.desc
index 3de92781b61..62a58c2e4d9 100644
--- a/regression/cbmc/Quantifiers-not-exists/test.desc
+++ b/regression/cbmc/Quantifiers-not-exists/test.desc
@@ -1,14 +1,20 @@
-CORE
+KNOWNBUG
 main.c
 
 ^\*\* Results:$
-^\[main.assertion.1\] line 18 assertion a\[.*\]\[.*\] > 10: SUCCESS$
-^\[main.assertion.2\] line 20 assertion tmp_if_expr\$\d+: SUCCESS$
-^\[main.assertion.3\] line 21 assertion tmp_if_expr\$\d+: SUCCESS$
-^\[main.assertion.4\] line 23 assertion tmp_if_expr\$\d+: SUCCESS$
-^\[main.assertion.5\] line 25 assertion tmp_if_expr\$\d+: SUCCESS$
-^\[main.assertion.6\] line 26 assertion tmp_if_expr\$\d+: SUCCESS$
-^\*\* 0 of 6 failed
+^\[main.assertion.5\] line 28 assertion a\[.*\]\[.*\] > 10: SUCCESS$
+^\[main.assertion.6\] line 30 assertion tmp_if_expr\$\d+: SUCCESS$
+^\[main.assertion.7\] line 31 assertion tmp_if_expr\$\d+: SUCCESS$
+^\[main.assertion.8\] line 33 assertion tmp_if_expr\$\d+: SUCCESS$
+^\[main.assertion.9\] line 35 assertion tmp_if_expr\$\d+: SUCCESS$
+^\[main.assertion.10\] line 36 assertion tmp_if_expr\$\d+: SUCCESS$
+^\*\* 0 of 10 failed
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
+--
+^warning: ignoring
+--
+All assertions are unreachable as each of the __CPROVER_assume evaluate to false
+(!exists i. i>=0 && i<2 ==> ... is equivalent to forall i. i>=0 && i<2 && ...,
+where neither i>=0 nor i<2 is actually true for all values of i).
diff --git a/regression/cbmc/Quantifiers-not/main.c b/regression/cbmc/Quantifiers-not/main.c
index e5759bd8d22..6a2b82e8fb2 100644
--- a/regression/cbmc/Quantifiers-not/main.c
+++ b/regression/cbmc/Quantifiers-not/main.c
@@ -4,6 +4,8 @@ int main()
   a[0]=1;
   a[1]=2;
 
+  // clang-format off
+  // clang-format would rewrite the "==>" as "== >"
   if(!__CPROVER_forall { int i; (i>=0 && i<2) ==> a[i]>=1 && a[i]<=10 })
     __CPROVER_assert(0, "success 1");
 
@@ -18,6 +20,7 @@ int main()
 
   if(!__CPROVER_exists { int i; (i>=0 && i<2) ==> a[i]>=5 && a[i]<=10 })
     __CPROVER_assert(0, "failure 2");
+  // clang-format on
 
   return 0;
 }
diff --git a/regression/cbmc/Quantifiers-not/test.desc b/regression/cbmc/Quantifiers-not/test.desc
index d853d107258..815e388b2d0 100644
--- a/regression/cbmc/Quantifiers-not/test.desc
+++ b/regression/cbmc/Quantifiers-not/test.desc
@@ -11,3 +11,5 @@ main.c
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/cbmc/Quantifiers-two-dimension-array/fixed.c b/regression/cbmc/Quantifiers-two-dimension-array/fixed.c
new file mode 100644
index 00000000000..83e4bc46258
--- /dev/null
+++ b/regression/cbmc/Quantifiers-two-dimension-array/fixed.c
@@ -0,0 +1,20 @@
+int main()
+{
+  int a[2][2];
+  int b[2][2];
+
+  // clang-format off
+  // clang-format would rewrite the "==>" as "== >"
+  // NOLINTNEXTLINE(whitespace/line_length)
+  __CPROVER_assume(__CPROVER_forall { int i; (i>=0 && i<2) ==> (__CPROVER_forall{int j; (j>=0 && j<2) ==> a[i][j]==i+j}) });
+  // NOLINTNEXTLINE(whitespace/line_length)
+  __CPROVER_assume(__CPROVER_exists { int i; (i>=0 && i<2) && (__CPROVER_exists{int j; (j>=0 && j<2) && b[i][j]==i+j+1}) });
+  // clang-format on
+
+  assert(a[0][0] == 0);
+  assert(a[0][1] == 1);
+  assert(a[1][0] == 1);
+  assert(a[1][1] == 2);
+  assert(b[0][0] == 1 || b[0][1] == 2 || b[1][0] == 2 || b[1][1] == 3);
+  return 0;
+}
diff --git a/regression/cbmc/Quantifiers-two-dimension-array/fixed.desc b/regression/cbmc/Quantifiers-two-dimension-array/fixed.desc
new file mode 100644
index 00000000000..74a171427a2
--- /dev/null
+++ b/regression/cbmc/Quantifiers-two-dimension-array/fixed.desc
@@ -0,0 +1,15 @@
+CORE
+fixed.c
+
+^\*\* Results:$
+^\[main.assertion.1\] line 14 assertion a\[.*\]\[.*\] == 0: SUCCESS$
+^\[main.assertion.2\] line 15 assertion a\[.*\]\[.*\] == 1: SUCCESS$
+^\[main.assertion.3\] line 16 assertion a\[.*\]\[.*\] == 1: SUCCESS$
+^\[main.assertion.4\] line 17 assertion a\[.*\]\[.*\] == 2: SUCCESS$
+^\[main.assertion.5\] line 18 assertion tmp_if_expr\$\d+: SUCCESS$
+^\*\* 0 of 5 failed
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/cbmc/Quantifiers-two-dimension-array/main.c b/regression/cbmc/Quantifiers-two-dimension-array/main.c
index b0be6e32f7a..1ddd02fd9ac 100644
--- a/regression/cbmc/Quantifiers-two-dimension-array/main.c
+++ b/regression/cbmc/Quantifiers-two-dimension-array/main.c
@@ -3,8 +3,11 @@ int main()
   int a[2][2];
   int b[2][2];
 
+  // clang-format off
+  // clang-format would rewrite the "==>" as "== >"
   __CPROVER_assume(__CPROVER_forall { int i; (i>=0 && i<2) ==> (__CPROVER_forall{int j; (j>=0 && j<2) ==> a[i][j]==i+j}) });
   __CPROVER_assume(__CPROVER_exists { int i; (i>=0 && i<2) ==> (__CPROVER_exists{int j; (j>=0 && j<2) ==> b[i][j]==i+j+1}) });
+  // clang-format on
 
   assert(a[0][0]==0);
   assert(a[0][1]==1);
diff --git a/regression/cbmc/Quantifiers-two-dimension-array/test.desc b/regression/cbmc/Quantifiers-two-dimension-array/test.desc
index fb34f594248..1ab76094ef1 100644
--- a/regression/cbmc/Quantifiers-two-dimension-array/test.desc
+++ b/regression/cbmc/Quantifiers-two-dimension-array/test.desc
@@ -1,13 +1,18 @@
-CORE
+KNOWNBUG
 main.c
 
 ^\*\* Results:$
-^\[main.assertion.1\] line 9 assertion a\[.*\]\[.*\] == 0: SUCCESS$
-^\[main.assertion.2\] line 10 assertion a\[.*\]\[.*\] == 1: SUCCESS$
-^\[main.assertion.3\] line 11 assertion a\[.*\]\[.*\] == 1: SUCCESS$
-^\[main.assertion.4\] line 12 assertion a\[.*\]\[.*\] == 2: SUCCESS$
-^\[main.assertion.5\] line 13 assertion tmp_if_expr\$\d+: SUCCESS$
-^\*\* 0 of 5 failed
-^VERIFICATION SUCCESSFUL$
-^EXIT=0$
+^\[main.assertion.1\] line 12 assertion a\[.*\]\[.*\] == 0: SUCCESS$
+^\[main.assertion.2\] line 13 assertion a\[.*\]\[.*\] == 1: SUCCESS$
+^\[main.assertion.3\] line 14 assertion a\[.*\]\[.*\] == 1: SUCCESS$
+^\[main.assertion.4\] line 15 assertion a\[.*\]\[.*\] == 2: SUCCESS$
+^\[main.assertion.5\] line 16 assertion tmp_if_expr\$\d+: FAILURE$
+^\*\* 1 of 5 failed
+^VERIFICATION FAILED$
+^EXIT=10$
 ^SIGNAL=0$
+--
+^warning: ignoring
+--
+The assertion on line 13 need not hold as the assume can be satisfied by picking
+a value for i that does not fulfil the left-hand side of the implication.
diff --git a/regression/cbmc/Quantifiers-type/main.c b/regression/cbmc/Quantifiers-type/main.c
index 33d6e48305b..89c9afb9dc8 100644
--- a/regression/cbmc/Quantifiers-type/main.c
+++ b/regression/cbmc/Quantifiers-type/main.c
@@ -3,8 +3,11 @@ int main()
   int a[2];
   int b[2];
 
+  // clang-format off
+  // clang-format would rewrite the "==>" as "== >"
   __CPROVER_assume( __CPROVER_forall { float i; (i>=0 && i<2) ==> a[i]>=10 && a[i]<=10 } );
   __CPROVER_assume( __CPROVER_forall { char i; (i>=0 && i<2) ==> b[i]>=10 && b[i]<=10 } );
+  // clang-format on
 
   assert(a[0]==10 && a[1]==10);
   assert(b[0]==10 && b[1]==10);
diff --git a/regression/cbmc/Quantifiers-type/test.desc b/regression/cbmc/Quantifiers-type/test.desc
index 7e7eb754d52..88f7f2726ae 100644
--- a/regression/cbmc/Quantifiers-type/test.desc
+++ b/regression/cbmc/Quantifiers-type/test.desc
@@ -1,10 +1,15 @@
-CORE
+KNOWNBUG
 main.c
 
 ^\*\* Results:$
-^\[main.assertion.1\] line 9 assertion tmp_if_expr(\$\d+)?: FAILURE$
-^\[main.assertion.2\] line 10 assertion tmp_if_expr\$\d+: SUCCESS$
+^\[main.assertion.1\] line 12 assertion tmp_if_expr(\$\d+)?: FAILURE$
+^\[main.assertion.2\] line 13 assertion tmp_if_expr\$\d+: SUCCESS$
 ^\*\* 1 of 2 failed
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
+--
+^warning: ignoring
+--
+This produces the expected verification result, but actually ignores some
+quantifiers.
diff --git a/regression/cbmc/Quantifiers1/main.c b/regression/cbmc/Quantifiers1/main.c
index 77cafc5231e..e3d860e32c9 100644
--- a/regression/cbmc/Quantifiers1/main.c
+++ b/regression/cbmc/Quantifiers1/main.c
@@ -2,6 +2,8 @@ int zero_array[10];
 
 int main()
 {
+  // clang-format off
+  // clang-format would rewrite the "==>" as "== >"
   // C# style
   assert(__CPROVER_forall { int i; (i>=0 && i<10) ==> zero_array[i]==0 });
 
@@ -20,4 +22,5 @@ int main()
 
   assert(__CPROVER_forall {unsigned i; i>9 || c[i]==i});
   return 0;
+  // clang-format on
 }
diff --git a/regression/cbmc/Quantifiers1/quantifier-with-side-effect.desc b/regression/cbmc/Quantifiers1/quantifier-with-side-effect.desc
index 144a4c31572..04d89eeef82 100644
--- a/regression/cbmc/Quantifiers1/quantifier-with-side-effect.desc
+++ b/regression/cbmc/Quantifiers1/quantifier-with-side-effect.desc
@@ -5,3 +5,4 @@ quantifier-with-side-effect.c
 ^SIGNAL=0$
 ^file .* line 10 function main: quantifier must not contain side effects$
 --
+^warning: ignoring