Using exists in __CPROVER_assume requires care

In some cases the assume is trivially true or trivially false.

Author: tautschnig

regression/cbmc/Quantifiers-not-exists/main.c

@@ -10,13 +10,20 @@ int main()
   // 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,16 +1,20 @@
-CORE
+KNOWNBUG
 main.c
 
 ^\*\* Results:$
-^\[main.assertion.1\] line 21 assertion a\[.*\]\[.*\] > 10: SUCCESS$
-^\[main.assertion.2\] line 23 assertion tmp_if_expr\$\d+: SUCCESS$
-^\[main.assertion.3\] line 24 assertion tmp_if_expr\$\d+: SUCCESS$
-^\[main.assertion.4\] line 26 assertion tmp_if_expr\$\d+: SUCCESS$
-^\[main.assertion.5\] line 28 assertion tmp_if_expr\$\d+: SUCCESS$
-^\[main.assertion.6\] line 29 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-two-dimension-array/test.desc

@@ -1,15 +1,18 @@
-CORE
+KNOWNBUG
 main.c
 
 ^\*\* Results:$
 ^\[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+: SUCCESS$
-^\*\* 0 of 5 failed
-^VERIFICATION SUCCESSFUL$
-^EXIT=0$
+^\[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.