Add tests for the quantifier statements inside an assume context,

to make sure they behave as expected.

Author: NlightNFotis

regression/cbmc-primitives/exists_assume_6231/test.c

@@ -0,0 +1,18 @@
+#include <stdlib.h>
+
+// clang-format off
+int main(int argc, char **argv)
+{
+    int *i = malloc(sizeof(int));
+    *i = 1;
+
+    // The exists inside the assume will evaluate to true,
+    // and be flipped by the negation in front of it, resulting
+    // to assume(false), which will allow the assertion to evaluate
+    // to true. 
+    __CPROVER_assume(
+        !__CPROVER_exists{int z; (z > 1 && z < 10) && z > *i}
+    );
+    __CPROVER_assert(0, "this assertion should be satified");
+}
+// clang-format on

regression/cbmc-primitives/exists_assume_6231/test.desc

@@ -0,0 +1,10 @@
+CORE
+test.c
+--pointer-check
+^EXIT=0$
+^SIGNAL=0$
+\[main\.assertion\.1\] line \d+ this assertion should be satified: SUCCESS
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring forall
+--

regression/cbmc-primitives/exists_assume_6231/test2.c

@@ -0,0 +1,16 @@
+#include <stdlib.h>
+
+// clang-format off
+int main(int argc, char **argv)
+{
+    int *i = malloc(sizeof(int));
+    *i = 1;
+
+    // The exists inside the assume will evaluate to true,
+    // and as such, the assertion below will fail as expected.
+    __CPROVER_assume(
+        __CPROVER_exists{int z; (z > 1 && z < 10) && z > *i}
+    );
+    __CPROVER_assert(0, "this should come out as failure");
+}
+// clang-format on

regression/cbmc-primitives/exists_assume_6231/test2.desc

@@ -0,0 +1,10 @@
+CORE
+test2.c
+--pointer-check
+^EXIT=10$
+^SIGNAL=0$
+\[main\.assertion\.1\] line \d+ this should come out as failure: FAILURE
+^VERIFICATION FAILED$
+--
+^warning: ignoring forall
+--