Quantifier test: The second assertion does not hold

The assertion requires, among other things, that (i>=0 && i<2) be true for all
values of i, and thus i>=0 (or i<2) for all values of i.

Author: tautschnig

regression/cbmc/Quantifiers-assertion/main.c

@@ -9,7 +9,7 @@ int main()
 
   __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");
+  __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");
 

regression/cbmc/Quantifiers-assertion/test.desc

@@ -1,14 +1,14 @@
-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$