Add regression test for matching against pointer values in traces of new SMT backend.

Author: NlightNFotis

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

@@ -0,0 +1,12 @@
+int main()
+{
+  int *a;
+  int *b = 0;
+  int *c;
+  __CPROVER_assume(c != 0);
+
+  __CPROVER_assert(
+    a != b, "should fail because a can be any pointer val, including NULL");
+  __CPROVER_assert(
+    a != c, "should fail because a and c can point to same object");
+}

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

@@ -0,0 +1,12 @@
+CORE
+pointer_values.c
+--trace
+\[main\.assertion\.1\] line \d+ should fail because a can be any pointer val, including NULL: FAILURE
+\[main\.assertion\.2\] line \d+ should fail because a and c can point to same object: FAILURE
+a=\(\(signed int \*\)NULL\)
+c=\(signed int \*\)1
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Test printing of NULL pointer values in trace.