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,11 @@
+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$
+--
+--