Support non-NULL pointer constants in the SMT back-end

We just treat them as bit vectors. Such constants arise when more
constant propagation is enabled (via union field sensitivity) in the
havoc_slice regression tests.

Author: tautschnig

regression/cbmc/union13/no-arch.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --arch none --little-endian
 (Starting CEGAR Loop|^Generated 1 VCC\(s\), 1 remaining after simplification$)

src/solvers/smt2/smt2_conv.cpp

@@ -3318,8 +3318,14 @@ void smt2_convt::convert_constant(const constant_exprt &expr)
           << ")";
     }
     else
-      UNEXPECTEDCASE(
-        "unknown pointer constant: " + id2string(expr.get_value()));
+    {
+      // just treat the pointer as a bit vector
+      const std::size_t width = boolbv_width(expr_type);
+
+      const mp_integer value = bvrep2integer(expr.get_value(), width, false);
+
+      out << "(_ bv" << value << " " << width << ")";
+    }
   }
   else if(expr_type.id()==ID_bool)
   {