Typecast to pointer: support all bitvector types

Even floating-point values are ok to just be re-interpreted as bit strings.

Author: tautschnig

src/solvers/flattening/bv_pointers.cpp

@@ -254,11 +254,10 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
     if(op_type.id()==ID_pointer)
       return convert_bv(op);
     else if(
-      op_type.id() == ID_signedbv || op_type.id() == ID_unsignedbv ||
-      op_type.id() == ID_bool || op_type.id() == ID_c_enum ||
-      op_type.id() == ID_c_enum_tag || op_type.id() == ID_bv)
+      can_cast_type<bitvector_typet>(op_type) || op_type.id() == ID_bool ||
+      op_type.id() == ID_c_enum || op_type.id() == ID_c_enum_tag)
     {
-      // Cast from integer to pointer.
+      // Cast from a bitvector type to pointer.
       // We just do a zero extension.
 
       const bvt &op_bv=convert_bv(op);

src/solvers/smt2/smt2_conv.cpp

@@ -829,6 +829,10 @@ std::string smt2_convt::type2id(const typet &type) const
   {
     return type2id(ns.follow_tag(to_c_enum_tag_type(type)).subtype());
   }
+  else if(type.id() == ID_pointer)
+  {
+    return "p" + std::to_string(to_pointer_type(type).get_width());
+  }
   else
   {
     UNREACHABLE;