Add extra test for address-of objects and pointer dereferencing to integers.

Author: NlightNFotis

regression/cbmc-incr-smt2/pointers/pointers_simple.c

@@ -0,0 +1,14 @@
+int main()
+{
+  int a = 10;
+  int *b = &a;
+  int c;
+
+  *b = 12;
+
+  __CPROVER_assert(a != *b, "a should be different than b");
+  __CPROVER_assert(a == *b, "a should not be different than b");
+  __CPROVER_assert(
+    *b != c,
+    "c can get assigned a value that makes it the same what b points to");
+}

regression/cbmc-incr-smt2/pointers/pointers_simple.desc

@@ -0,0 +1,12 @@
+CORE
+pointers_simple.c
+--trace
+Passing problem to incremental SMT2 solving
+\[main\.assertion.\d\] line \d a should be different than b: FAILURE
+\[main\.assertion.\d\] line \d+ a should not be different than b: SUCCESS
+\[main\.assertion.\d\] line \d+ c can get assigned a value that makes it the same what b points to: FAILURE
+c=12
+^EXIT=10$
+^SIGNAL=0$
+--
+--