Add an extra test to the regression test suite, suggested by Thomas S.

Author: NlightNFotis

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

@@ -0,0 +1,14 @@
+#include <assert.h>
+#include <stdbool.h>
+
+int main()
+{
+  int x;
+  int y;
+  int z;
+  bool nondet1;
+  bool nondet2;
+  int *a = nondet1 ? &x : &y;
+  int *b = nondet2 ? &y : &z;
+  __CPROVER_assert(!__CPROVER_same_object(a, b), "Can be violated.");
+}

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

@@ -0,0 +1,17 @@
+CORE
+pointer_object2.c
+--trace --verbosity 10
+\[main\.assertion\.1\] line 13 Can be violated.: FAILURE
+nondet1=FALSE
+nondet2=TRUE
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Ensure that two variables which can get assigned the address of the
+same object satisfy the __CPROVER_same_object predicate. In the code
+under test, we negate the predicate to be able to get a failure and a
+trace which we can then match against expected values which guide
+through the path that leads to the two variables getting assigned the
+same object.