Fixed logic in assumptions

Use appropriate Boolean connectives to actually make assertions hold.

Author: tautschnig

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