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

@@ -253,13 +253,11 @@ 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)
+    else if(
+      can_cast_type<bitvector_typet>(op_type) || 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

@@ -723,6 +723,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;