Quantifier test: The second assertion does not hold [blocks: #2574, #3725, #3924]

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;
 }

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

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);

regression/cbmc/Quantifiers-assignment/test.desc

@@ -10,3 +10,5 @@ main.c
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
+--
+^warning: ignoring

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);

regression/cbmc/Quantifiers-copy/test.desc

@@ -11,3 +11,5 @@ main.c
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
+--
+^warning: ignoring

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;
 }

regression/cbmc/Quantifiers-if/test.desc

@@ -11,3 +11,5 @@ main.c
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
+--
+^warning: ignoring

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);

regression/cbmc/Quantifiers-initialisation/test.desc

@@ -11,3 +11,5 @@ main.c
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
+--
+^warning: ignoring

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;
 }

regression/cbmc/Quantifiers-initialisation2/test.desc

@@ -11,3 +11,5 @@ main.c
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
+--
+^warning: ignoring

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);
 

regression/cbmc/Quantifiers-invalid-var-range/test.desc

@@ -1,8 +1,13 @@
-CORE
+KNOWNBUG
 main.c
 
 ^\*\* Results:$
 ^\*\* 0 of 1 failed
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
+--
+^warning: ignoring
+--
+This produces the expected verification result, but actually ignores some
+quantifiers.

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;
+}

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

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);
 

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).

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;
 }

regression/cbmc/Quantifiers-not/test.desc

@@ -11,3 +11,5 @@ main.c
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
+--
+^warning: ignoring

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;
+}

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

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);

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.

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);