Add tests containing alternating (nested) quantifiers.

And make sure that properties are asserted two levels deep into them.

Author: NlightNFotis

regression/cbmc-primitives/alternating_quantifiers_6231/exists_in_forall.c

@@ -0,0 +1,14 @@
+#include <stdlib.h>
+
+// clang-format off
+int main(int argc, char **argv)
+{
+    int *i = malloc(sizeof(int));
+    *i = 1;
+
+    __CPROVER_assert(
+        __CPROVER_forall { int z; (0 < z && z < 10) ==>
+            __CPROVER_exists { int y; ( 10 < y && y < 20) && y == z + 10 && y > *i } },
+        "for all z, there exists a y so that y = z + 10 and y > 1");
+}
+// clang-format on

regression/cbmc-primitives/alternating_quantifiers_6231/exists_in_forall.desc

@@ -0,0 +1,16 @@
+CORE
+exists_in_forall.c
+--pointer-check
+^EXIT=0$
+^SIGNAL=0$
+\[main\.assertion\.1\] line \d* for all z, there exists a y so that y = z \+ 10 and y > 1: SUCCESS
+\[main\.pointer_dereference\.7\] line \d+ dereference failure: pointer NULL in \*i: SUCCESS
+\[main\.pointer_dereference\.8\] line \d+ dereference failure: pointer invalid in \*i: SUCCESS
+\[main\.pointer_dereference\.9\] line \d+ dereference failure: deallocated dynamic object in \*i: SUCCESS
+\[main\.pointer_dereference\.10\] line \d+ dereference failure: dead object in \*i: SUCCESS
+\[main\.pointer_dereference\.11\] line \d+ dereference failure: pointer outside object bounds in \*i: SUCCESS
+\[main\.pointer_dereference\.12\] line \d+ dereference failure: invalid integer address in \*i: SUCCESS
+--
+--
+The assertion reference number here is present so that we make sure
+we always match the properties of the dereference inside the exists.

regression/cbmc-primitives/alternating_quantifiers_6231/forall_in_exists.c

@@ -0,0 +1,14 @@
+#include <stdlib.h>
+
+// clang-format off
+int main(int argc, char **argv)
+{
+    int *i = malloc(sizeof(int));
+    *i = 1;
+
+    __CPROVER_assert(
+        __CPROVER_exists { int z; (0 < z && z < 2) &&
+            __CPROVER_forall { int o; (10 < o && o < 20) ==> o > z && z == * i }},
+        "there exists a z between 0 and 2 so that for all o between 10 and 20, o > z and z = 1");
+}
+// clang-format on

regression/cbmc-primitives/alternating_quantifiers_6231/forall_in_exists.desc

@@ -0,0 +1,14 @@
+CORE
+forall_in_exists.c
+--pointer-check
+^EXIT=0$
+^SIGNAL=0$
+\[main\.assertion\.1\] line \d* there exists a z between 0 and 2 so that for all o between 10 and 20, o > z and z = 1: SUCCESS
+\[main\.pointer_dereference\.7\] line \d+ dereference failure: pointer NULL in \*i: SUCCESS
+\[main\.pointer_dereference\.8\] line \d+ dereference failure: pointer invalid in \*i: SUCCESS
+\[main\.pointer_dereference\.9\] line \d+ dereference failure: deallocated dynamic object in \*i: SUCCESS
+\[main\.pointer_dereference\.10\] line \d+ dereference failure: dead object in \*i: SUCCESS
+\[main\.pointer_dereference\.11\] line \d+ dereference failure: pointer outside object bounds in \*i: SUCCESS
+\[main\.pointer_dereference\.12\] line \d+ dereference failure: invalid integer address in \*i: SUCCESS
+--
+--