Add regression test for pointer address being found in the trace in new SMT backend.

The difference is that the previous test was effectively exercising NULL and any
other pointer value (1, for instance) whereas this one specifically matches the
decimal value of 0xDEADBEEF.

Author: NlightNFotis

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

@@ -0,0 +1,8 @@
+int main()
+{
+    int *a;
+    int *b;
+    __CPROVER_assume(a == 0xDEADBEEF);
+
+    __CPROVER_assert(a != b, "should fail as b can also be assigned 0xDEADBEEF");
+}

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

@@ -0,0 +1,12 @@
+CORE
+pointer_values_2.c
+--trace --slice-formula
+\[main\.assertion\.1\] line \d should fail as b can also be assigned 0xDEADBEEF: FAILURE
+a=\(signed int \*\)3735928559
+b=\(signed int \*\)3735928559
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+3735928559 is the decimal value of the hex constant 0xDEADBEEF that
+the pointer is assumed to point to in this example.

src/solvers/smt2_incremental/construct_value_expr_from_smt.cpp

@@ -44,7 +44,7 @@ class value_expr_from_smt_factoryt : public smt_term_const_downcast_visitort
     {
       INVARIANT(
         pointer_type->get_width() == sort_width,
-        "Width of smt bit vector term must match the width of pointer  type.");
+        "Width of smt bit vector term must match the width of pointer type.");
       if(bit_vector_constant.value() == 0)
       {
         result = null_pointer_exprt{*pointer_type};