diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-invalid-cast-const-fp/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-invalid-cast-const-fp/test.desc
index b2f2a12d4ee..da896db86eb 100644
--- a/regression/goto-analyzer/approx-const-fp-array-variable-invalid-cast-const-fp/test.desc
+++ b/regression/goto-analyzer/approx-const-fp-array-variable-invalid-cast-const-fp/test.desc
@@ -2,9 +2,9 @@ CORE
 main.c
 --show-goto-functions --verbosity 10 --pointer-check
 ^Removing function pointers and virtual functions$
-^\s*IF fp == \(const void_fp\)f2 THEN GOTO [0-9]$
-^\s*IF fp == \(const void_fp\)f3 THEN GOTO [0-9]$
-^\s*IF fp == \(const void_fp\)f4 THEN GOTO [0-9]$
+^\s*IF fp == \(.*\)f2 THEN GOTO [0-9]$
+^\s*IF fp == \(.*\)f3 THEN GOTO [0-9]$
+^\s*IF fp == \(.*\)f4 THEN GOTO [0-9]$
 ^SIGNAL=0$
 --
 ^warning: ignoring
diff --git a/src/ansi-c/ansi_c_convert_type.cpp b/src/ansi-c/ansi_c_convert_type.cpp
index 4b3a4a0f339..3c00f08f39d 100644
--- a/src/ansi-c/ansi_c_convert_type.cpp
+++ b/src/ansi-c/ansi_c_convert_type.cpp
@@ -14,9 +14,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <cassert>
 
 #include <util/c_types.h>
+#include <util/config.h>
 #include <util/namespace.h>
 #include <util/simplify_expr.h>
-#include <util/config.h>
 #include <util/arith_tools.h>
 #include <util/std_types.h>
 
@@ -221,9 +221,11 @@ void ansi_c_convert_typet::read_rec(const typet &type)
     // We turn ID_frontend_pointer to ID_pointer
     // Pointers have a width, much like integers,
     // which is added here.
-    typet tmp(type);
-    tmp.id(ID_pointer);
-    tmp.set(ID_width, config.ansi_c.pointer_width);
+    pointer_typet tmp(type.subtype(), config.ansi_c.pointer_width);
+    tmp.add_source_location()=type.source_location();
+    const irep_idt typedef_identifier=type.get(ID_C_typedef);
+    if(!typedef_identifier.empty())
+      tmp.set(ID_C_typedef, typedef_identifier);
     other.push_back(tmp);
   }
   else if(type.id()==ID_pointer)
diff --git a/src/ansi-c/c_preprocess.cpp b/src/ansi-c/c_preprocess.cpp
index 26fb22355ff..a9466d83c4a 100644
--- a/src/ansi-c/c_preprocess.cpp
+++ b/src/ansi-c/c_preprocess.cpp
@@ -25,6 +25,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/c_types.h>
 #include <util/config.h>
+#include <util/invariant.h>
 #include <util/message.h>
 #include <util/tempfile.h>
 #include <util/unicode.h>
@@ -430,7 +431,7 @@ bool c_preprocess_visual_studio(
     command_file << "/D__CPROVER__" << "\n";
     command_file << "/D__WORDSIZE=" << config.ansi_c.pointer_width << "\n";
 
-    if(config.ansi_c.pointer_width==64)
+    if(pointer_diff_type()==signed_long_long_int_type())
     {
       command_file << "\"/D__PTRDIFF_TYPE__=long long int\""  << "\n";
       // yes, both _WIN32 and _WIN64 get defined
@@ -438,6 +439,9 @@ bool c_preprocess_visual_studio(
     }
     else
     {
+      DATA_INVARIANT(
+        pointer_diff_type()==signed_int_type(),
+        "Pointer difference expected to be int typed");
       command_file << "/D__PTRDIFF_TYPE__=int" << "\n";
       command_file << "/U_WIN64" << "\n";
     }
diff --git a/src/ansi-c/padding.cpp b/src/ansi-c/padding.cpp
index 58e349ee0e6..9970298b440 100644
--- a/src/ansi-c/padding.cpp
+++ b/src/ansi-c/padding.cpp
@@ -73,20 +73,15 @@ mp_integer alignment(const typet &type, const namespacet &ns)
           type.id()==ID_signedbv ||
           type.id()==ID_fixedbv ||
           type.id()==ID_floatbv ||
-          type.id()==ID_c_bool)
+          type.id()==ID_c_bool ||
+          type.id()==ID_pointer)
   {
-    std::size_t width=to_bitvector_type(type).get_width();
-    result=width%8?width/8+1:width/8;
+    result=pointer_offset_size(type, ns);
   }
   else if(type.id()==ID_c_enum)
     result=alignment(type.subtype(), ns);
   else if(type.id()==ID_c_enum_tag)
     result=alignment(ns.follow_tag(to_c_enum_tag_type(type)), ns);
-  else if(type.id()==ID_pointer)
-  {
-    std::size_t width=config.ansi_c.pointer_width;
-    result=width%8?width/8+1:width/8;
-  }
   else if(type.id()==ID_symbol)
     result=alignment(ns.follow(type), ns);
   else if(type.id()==ID_c_bit_field)
diff --git a/src/cpp/cpp_convert_type.cpp b/src/cpp/cpp_convert_type.cpp
index 23d4ae5acbd..e3dfff685d4 100644
--- a/src/cpp/cpp_convert_type.cpp
+++ b/src/cpp/cpp_convert_type.cpp
@@ -162,9 +162,12 @@ void cpp_convert_typet::read_rec(const typet &type)
   else if(type.id()==ID_frontend_pointer)
   {
     // add width and turn into ID_pointer
-    typet tmp=type;
-    tmp.id(ID_pointer);
-    tmp.set(ID_width, config.ansi_c.pointer_width);
+    pointer_typet tmp(type.subtype(), config.ansi_c.pointer_width);
+    tmp.add_source_location()=type.source_location();
+    if(type.get_bool(ID_C_reference))
+      tmp.set(ID_C_reference, true);
+    if(type.get_bool(ID_C_rvalue_reference))
+      tmp.set(ID_C_rvalue_reference, true);
     other.push_back(tmp);
   }
   else if(type.id()==ID_pointer)
diff --git a/src/cpp/cpp_typecheck_type.cpp b/src/cpp/cpp_typecheck_type.cpp
index 5258633b16e..1c2ba93ec14 100644
--- a/src/cpp/cpp_typecheck_type.cpp
+++ b/src/cpp/cpp_typecheck_type.cpp
@@ -14,7 +14,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #include <util/source_location.h>
 #include <util/simplify_expr.h>
 #include <util/c_types.h>
-#include <util/config.h>
 
 #include <ansi-c/c_qualifiers.h>
 
@@ -79,12 +78,10 @@ void cpp_typecheckt::typecheck_type(typet &type)
   }
   else if(type.id()==ID_pointer)
   {
-    // the pointer might have a qualifier, but do subtype first
+    // the pointer/reference might have a qualifier,
+    // but do subtype first
     typecheck_type(type.subtype());
 
-    // we add a width, much like with integers
-    to_pointer_type(type).set_width(config.ansi_c.pointer_width);
-
     // Check if it is a pointer-to-member
     if(type.find("to-member").is_not_nil())
     {
diff --git a/src/goto-instrument/accelerate/polynomial_accelerator.cpp b/src/goto-instrument/accelerate/polynomial_accelerator.cpp
index 7ff1a9e5679..10f1793fcef 100644
--- a/src/goto-instrument/accelerate/polynomial_accelerator.cpp
+++ b/src/goto-instrument/accelerate/polynomial_accelerator.cpp
@@ -37,7 +37,6 @@ Author: Matt Lewis
 #include <util/simplify_expr.h>
 #include <util/replace_expr.h>
 #include <util/arith_tools.h>
-#include <util/config.h>
 
 #include "accelerator.h"
 #include "util.h"
@@ -345,9 +344,7 @@ bool polynomial_acceleratort::fit_polynomial_sliced(
     return false;
   }
 
-  unsigned width=to_bitvector_type(var.type()).get_width();
-  if(var.type().id()==ID_pointer)
-    width=config.ansi_c.pointer_width;
+  std::size_t width=to_bitvector_type(var.type()).get_width();
   assert(width>0);
 
   for(std::vector<expr_listt>::iterator it=parameters.begin();
diff --git a/src/solvers/cvc/cvc_conv.cpp b/src/solvers/cvc/cvc_conv.cpp
index c9f2ecb0211..47008f4f7b5 100644
--- a/src/solvers/cvc/cvc_conv.cpp
+++ b/src/solvers/cvc/cvc_conv.cpp
@@ -13,9 +13,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <string>
 
 #include <util/arith_tools.h>
+#include <util/c_types.h>
 #include <util/std_types.h>
 #include <util/std_expr.h>
-#include <util/config.h>
 #include <util/find_symbols.h>
 #include <util/pointer_offset_size.h>
 #include <util/string2int.h>
@@ -159,8 +159,9 @@ void cvc_convt::convert_constant_expr(const exprt &expr)
     {
       out << "(# object:="
           << pointer_logic.get_null_object()
-          << ", offset:="
-          << bin_zero(config.ansi_c.pointer_width) << " #)";
+          << ", offset:=";
+      convert_expr(from_integer(0, size_type()));
+      out << " #)";
     }
     else
       throw "unknown pointer constant: "+id2string(value);
@@ -176,7 +177,9 @@ void cvc_convt::convert_constant_expr(const exprt &expr)
   }
   else if(expr.type().id()==ID_array)
   {
-    out << "ARRAY (i: " << array_index_type() << "):";
+    out << "ARRAY (i: ";
+    convert_type(index_type());
+    out << "):";
 
     assert(!expr.operands().empty());
 
@@ -188,7 +191,9 @@ void cvc_convt::convert_constant_expr(const exprt &expr)
       else
         out << "\n  ELSIF ";
 
-      out << "i=" << array_index(i) << " THEN ";
+      out << "i=";
+      convert_expr(from_integer(i, index_type()));
+      out << " THEN ";
       convert_array_value(*it);
       i++;
     }
@@ -247,7 +252,7 @@ void cvc_convt::convert_plus_expr(const exprt &expr)
       out << "(LET P: " << cvc_pointer_type() << " = ";
       convert_expr(*p);
       out << " IN P WITH .offset:=BVPLUS("
-          << config.ansi_c.pointer_width
+          << pointer_offset_bits(pointer_type(void_type()), ns)
           << ", P.offset, ";
       convert_expr(*i);
       out << "))";
@@ -487,52 +492,24 @@ void cvc_convt::convert_literal(const literalt l)
     out << ")";
 }
 
-std::string cvc_convt::bin_zero(unsigned bits)
+std::string cvc_convt::cvc_pointer_type() const
 {
-  assert(bits!=0);
-  std::string result="0bin";
-  while(bits!=0)
-  {
-    result+='0';
-    bits--;
-  }
-  return result;
-}
-
-std::string cvc_convt::cvc_pointer_type()
-{
-  assert(config.ansi_c.pointer_width!=0);
-  return "[# object: INT, offset: BITVECTOR("+
-         std::to_string(config.ansi_c.pointer_width)+") #]";
-}
-
-std::string cvc_convt::array_index_type()
-{
-  return std::string("BITVECTOR(")+
-         std::to_string(32)+")";
-}
-
-typet cvc_convt::gen_array_index_type()
-{
-  typet t(ID_signedbv);
-  t.set(ID_width, 32);
-  return t;
-}
-
-std::string cvc_convt::array_index(unsigned i)
-{
-  return "0bin"+integer2binary(i, config.ansi_c.int_width);
+  return
+    "[# object: INT, offset: BITVECTOR("+
+    std::to_string(
+      integer2size_t(
+        pointer_offset_bits(pointer_type(void_type()), ns)))+") #]";
 }
 
 void cvc_convt::convert_array_index(const exprt &expr)
 {
-  if(expr.type()==gen_array_index_type())
+  if(expr.type()==index_type())
   {
     convert_expr(expr);
   }
   else
   {
-    exprt tmp(ID_typecast, gen_array_index_type());
+    exprt tmp(ID_typecast, index_type());
     tmp.copy_to_operands(expr);
     convert_expr(tmp);
   }
@@ -547,8 +524,9 @@ void cvc_convt::convert_address_of_rec(const exprt &expr)
     out
       << "(# object:="
       << pointer_logic.add_object(expr)
-      << ", offset:="
-      << bin_zero(config.ansi_c.pointer_width) << " #)";
+      << ", offset:=";
+    convert_expr(from_integer(0, size_type()));
+    out << " #)";
   }
   else if(expr.id()==ID_index)
   {
@@ -581,7 +559,7 @@ void cvc_convt::convert_address_of_rec(const exprt &expr)
         assert(false);
 
       out << " IN P WITH .offset:=BVPLUS("
-                   << config.ansi_c.pointer_width
+                   << pointer_offset_bits(pointer_type(void_type()), ns)
                    << ", P.offset, ";
       convert_expr(index);
       out << "))";
@@ -609,13 +587,10 @@ void cvc_convt::convert_address_of_rec(const exprt &expr)
       ns);
     assert(offset>=0);
 
-    typet index_type(ID_unsignedbv);
-    index_type.set(ID_width, config.ansi_c.pointer_width);
-
-    exprt index=from_integer(offset, index_type);
+    exprt index=from_integer(offset, size_type());
 
     out << " IN P WITH .offset:=BVPLUS("
-                 << config.ansi_c.pointer_width
+                 << pointer_offset_bits(pointer_type(void_type()), ns)
                  << ", P.offset, ";
     convert_expr(index);
     out << "))";
@@ -1035,7 +1010,9 @@ void cvc_convt::convert_expr(const exprt &expr)
   {
     assert(expr.type().id()==ID_array);
     assert(expr.operands().size()==1);
-    out << "(ARRAY (i: " << array_index_type() << "): ";
+    out << "(ARRAY (i: ";
+    convert_type(index_type());
+    out << "): ";
     convert_array_value(expr.op0());
     out << ")";
   }
@@ -1273,8 +1250,9 @@ void cvc_convt::convert_type(const typet &type)
   {
     const array_typet &array_type=to_array_type(type);
 
-    out << "ARRAY " << array_index_type()
-                 << " OF ";
+    out << "ARRAY ";
+    convert_type(index_type());
+    out << " OF ";
 
     if(array_type.subtype().id()==ID_bool)
       out << "BITVECTOR(1)";
diff --git a/src/solvers/cvc/cvc_conv.h b/src/solvers/cvc/cvc_conv.h
index c3fc7dbe182..53c148cb88b 100644
--- a/src/solvers/cvc/cvc_conv.h
+++ b/src/solvers/cvc/cvc_conv.h
@@ -79,11 +79,7 @@ class cvc_convt:public prop_convt
   void convert_array_value(const exprt &expr);
   void convert_as_bv(const exprt &expr);
   void convert_array_index(const exprt &expr);
-  static typet gen_array_index_type();
-  static std::string bin_zero(unsigned bits);
-  static std::string array_index_type();
-  static std::string array_index(unsigned i);
-  static std::string cvc_pointer_type();
+  std::string cvc_pointer_type() const;
 };
 
 #endif // CPROVER_SOLVERS_CVC_CVC_CONV_H
diff --git a/src/solvers/flattening/boolbv_update.cpp b/src/solvers/flattening/boolbv_update.cpp
index e48e5990f07..f5121f8bf91 100644
--- a/src/solvers/flattening/boolbv_update.cpp
+++ b/src/solvers/flattening/boolbv_update.cpp
@@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/std_expr.h>
 #include <util/arith_tools.h>
 #include <util/base_type.h>
-#include <util/config.h>
 #include <util/pointer_offset_size.h>
 
 #include <util/c_types.h>
diff --git a/src/solvers/flattening/boolbv_width.cpp b/src/solvers/flattening/boolbv_width.cpp
index 4c2bd1c86c2..4bb2341f208 100644
--- a/src/solvers/flattening/boolbv_width.cpp
+++ b/src/solvers/flattening/boolbv_width.cpp
@@ -11,7 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <algorithm>
 
 #include <util/arith_tools.h>
-#include <util/config.h>
+#include <util/invariant.h>
 #include <util/std_types.h>
 
 boolbv_widtht::boolbv_widtht(const namespacet &_ns):ns(_ns)
@@ -195,7 +195,8 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
   }
   else if(type_id==ID_pointer)
   {
-    entry.total_width=config.ansi_c.pointer_width;
+    entry.total_width=to_pointer_type(type).get_width();
+    DATA_INVARIANT(entry.total_width!=0, "pointer must have width");
   }
   else if(type_id==ID_symbol)
     entry=get_entry(ns.follow(type));
diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp
index 85ec254a0e6..c430c44ff06 100644
--- a/src/solvers/flattening/bv_pointers.cpp
+++ b/src/solvers/flattening/bv_pointers.cpp
@@ -96,8 +96,9 @@ bv_pointerst::bv_pointerst(
   pointer_logic(_ns)
 {
   object_bits=config.bv_encoding.object_bits;
-  offset_bits=config.ansi_c.pointer_width-object_bits;
-  bits=config.ansi_c.pointer_width;
+  std::size_t pointer_width=boolbv_width(pointer_type(void_type()));
+  offset_bits=pointer_width-object_bits;
+  bits=pointer_width;
 }
 
 bool bv_pointerst::convert_address_of_rec(
@@ -220,7 +221,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
     throw "convert_pointer_type got non-pointer type";
 
   // make sure the config hasn't been changed
-  assert(bits==config.ansi_c.pointer_width);
+  PRECONDITION(bits==boolbv_width(expr.type()));
 
   if(expr.id()==ID_symbol)
   {
diff --git a/src/util/pointer_offset_size.cpp b/src/util/pointer_offset_size.cpp
index e5e3dea6796..614aa4fa320 100644
--- a/src/util/pointer_offset_size.cpp
+++ b/src/util/pointer_offset_size.cpp
@@ -11,15 +11,13 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "pointer_offset_size.h"
 
-#include <cassert>
-
 #include "c_types.h"
 #include "expr.h"
+#include "invariant.h"
 #include "arith_tools.h"
 #include "std_types.h"
 #include "std_expr.h"
 #include "expr_util.h"
-#include "config.h"
 #include "simplify_expr.h"
 #include "namespace.h"
 #include "symbol.h"
@@ -103,6 +101,7 @@ mp_integer member_offset_bits(
   return offset;
 }
 
+/// Compute the size of a type in bytes, rounding up to full bytes
 mp_integer pointer_offset_size(
   const typet &type,
   const namespacet &ns)
@@ -110,7 +109,7 @@ mp_integer pointer_offset_size(
   mp_integer bits=pointer_offset_bits(type, ns);
   if(bits==-1)
     return -1;
-  return bits/8+(((bits%8)==0)?0:1);
+  return (bits+7)/8;
 }
 
 mp_integer pointer_offset_bits(
@@ -234,7 +233,7 @@ mp_integer pointer_offset_bits(
     if(type.get_bool(ID_C_ptr32))
       return 32;
 
-    return config.ansi_c.pointer_width;
+    return to_bitvector_type(type).get_width();
   }
   else if(type.id()==ID_symbol)
   {
@@ -495,7 +494,7 @@ exprt size_of_expr(
     if(type.get_bool(ID_C_ptr32))
       return from_integer(4, size_type());
 
-    std::size_t width=config.ansi_c.pointer_width;
+    std::size_t width=to_bitvector_type(type).get_width();
     std::size_t bytes=width/8;
     if(bytes*8!=width)
       bytes++;
@@ -531,12 +530,13 @@ mp_integer compute_pointer_offset(
   }
   else if(expr.id()==ID_index)
   {
-    assert(expr.operands().size()==2);
+    const index_exprt &index_expr=to_index_expr(expr);
+    const typet &array_type=ns.follow(index_expr.array().type());
+    DATA_INVARIANT(
+      array_type.id()==ID_array,
+      "index into array expected, found "+array_type.id_string());
 
-    const typet &array_type=ns.follow(expr.op0().type());
-    assert(array_type.id()==ID_array);
-
-    mp_integer o=compute_pointer_offset(expr.op0(), ns);
+    mp_integer o=compute_pointer_offset(index_expr.array(), ns);
 
     if(o!=-1)
     {
@@ -545,7 +545,7 @@ mp_integer compute_pointer_offset(
 
       mp_integer i;
 
-      if(sub_size>0 && !to_integer(expr.op1(), i))
+      if(sub_size>0 && !to_integer(index_expr.index(), i))
         return o+i*sub_size;
     }
 
@@ -553,13 +553,11 @@ mp_integer compute_pointer_offset(
   }
   else if(expr.id()==ID_member)
   {
-    assert(expr.operands().size()==1);
-    const typet &type=ns.follow(expr.op0().type());
-
-    assert(type.id()==ID_struct ||
-           type.id()==ID_union);
+    const member_exprt &member_expr=to_member_expr(expr);
+    const exprt &op=member_expr.struct_op();
+    const struct_union_typet &type=to_struct_union_type(ns.follow(op.type()));
 
-    mp_integer o=compute_pointer_offset(expr.op0(), ns);
+    mp_integer o=compute_pointer_offset(op, ns);
 
     if(o!=-1)
     {
@@ -567,7 +565,7 @@ mp_integer compute_pointer_offset(
         return o;
 
       return o+member_offset(
-        to_struct_type(type), expr.get(ID_component_name), ns);
+        to_struct_type(type), member_expr.get_component_name(), ns);
     }
   }
   else if(expr.id()==ID_string_constant)
@@ -594,8 +592,10 @@ exprt build_sizeof_expr(
      (type_size==0 && val>0))
     return nil_exprt();
 
-  assert(address_bits(val+1)<=config.ansi_c.pointer_width);
   const typet t(size_type());
+  DATA_INVARIANT(
+    address_bits(val+1)<=pointer_offset_bits(t, ns),
+    "sizeof value does not fit size_type");
 
   mp_integer remainder=0;
   if(type_size!=0)
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
index d601ef06e3f..1e8136eda64 100644
--- a/src/util/simplify_expr.cpp
+++ b/src/util/simplify_expr.cpp
@@ -204,7 +204,8 @@ bool simplify_exprt::simplify_typecast(exprt &expr)
      expr.op0().id()==ID_typecast &&
      expr.op0().operands().size()==1 &&
      (op_type.id()==ID_signedbv || op_type.id()==ID_unsignedbv) &&
-     to_bitvector_type(op_type).get_width()>=config.ansi_c.pointer_width)
+     to_bitvector_type(op_type).get_width()>=
+     to_bitvector_type(expr_type).get_width())
   {
     exprt tmp=expr.op0().op0();
     expr.op0().swap(tmp);