[WIP] Add rudimentary tests for the exists quantifier.

Author: NlightNFotis

regression/cbmc-primitives/exists_6231_1/test.c

@@ -0,0 +1,18 @@
+#include <assert.h>
+#include <stdlib.h>
+
+// clang-format off
+int main() {
+  char *a = malloc(1);
+
+  // lots of errors with `--pointer-check` enabled
+  assert(*a == *a);
+
+  // no errors even with `--pointer-check` enabled
+  assert(
+    __CPROVER_exists {
+      int i ; (0 <= i && i < 1) && *(a+i) == *(a+i)
+    }
+  );
+}
+// clang-format on

regression/cbmc-primitives/exists_6231_1/test.desc

@@ -0,0 +1,8 @@
+CORE
+test.c
+--pointer-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--

regression/cbmc-primitives/exists_6231_2/test.c

@@ -0,0 +1,18 @@
+#include <assert.h>
+#include <stdlib.h>
+
+// clang-format off
+int main() {
+  char *a = malloc(1);
+
+  // lots of errors with `--pointer-check` enabled
+  assert(*a == *a);
+
+  // no errors even with `--pointer-check` enabled
+  assert(
+    __CPROVER_exists {
+      int i ; (0 <= i && i < 10) && *(a+i) == *(a+i)
+    }
+  );
+}
+// clang-format on

regression/cbmc-primitives/exists_6231_2/test.desc

@@ -0,0 +1,8 @@
+CORE
+test.c
+--pointer-check
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--