diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp
index c0cd29a3877..b22896bd7f7 100644
--- a/src/ansi-c/ansi_c_entry_point.cpp
+++ b/src/ansi-c/ansi_c_entry_point.cpp
@@ -327,16 +327,13 @@ bool ansi_c_entry_point(
         zero_string.type().set(ID_size, "infinity");
         exprt index(ID_index, char_type());
         index.copy_to_operands(zero_string, from_integer(0, uint_type()));
-        exprt address_of("address_of", pointer_typet());
-        address_of.type().subtype()=char_type();
-        address_of.copy_to_operands(index);
+        exprt address_of=address_of_exprt(index, pointer_type(char_type()));
 
         if(argv_symbol.type.subtype()!=address_of.type())
           address_of.make_typecast(argv_symbol.type.subtype());
 
         // assign argv[*] to the address of a string-object
-        exprt array_of("array_of", argv_symbol.type);
-        array_of.copy_to_operands(address_of);
+        array_of_exprt array_of(address_of, argv_symbol.type);
 
         init_code.copy_to_operands(
           code_assignt(argv_symbol.symbol_expr(), array_of));
@@ -400,17 +397,18 @@ bool ansi_c_entry_point(
 
         {
           const exprt &arg1=parameters[1];
+          const pointer_typet &pointer_type=
+            to_pointer_type(arg1.type());
 
-          exprt index_expr(ID_index, arg1.type().subtype());
-          index_expr.copy_to_operands(
+          index_exprt index_expr(
             argv_symbol.symbol_expr(),
-            from_integer(0, index_type()));
+            from_integer(0, index_type()),
+            pointer_type.subtype());
 
           // disable bounds check on that one
           index_expr.set("bounds_check", false);
 
-          op1=exprt(ID_address_of, arg1.type());
-          op1.move_to_operands(index_expr);
+          op1=address_of_exprt(index_expr, pointer_type);
         }
 
         // do we need envp?
@@ -420,13 +418,15 @@ bool ansi_c_entry_point(
           exprt &op2=operands[2];
 
           const exprt &arg2=parameters[2];
+          const pointer_typet &pointer_type=
+            to_pointer_type(arg2.type());
 
-          exprt index_expr(ID_index, arg2.type().subtype());
-          index_expr.copy_to_operands(
-            envp_symbol.symbol_expr(), from_integer(0, index_type()));
+          index_exprt index_expr(
+            envp_symbol.symbol_expr(),
+            from_integer(0, index_type()),
+            pointer_type.subtype());
 
-          op2=exprt(ID_address_of, arg2.type());
-          op2.move_to_operands(index_expr);
+          op2=address_of_exprt(index_expr, pointer_type);
         }
       }
     }
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index 677a0c78152..fee4e8685d1 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -834,11 +834,10 @@ void c_typecheck_baset::typecheck_expr_symbol(exprt &expr)
 
     if(expr.type().id()==ID_code) // function designator
     { // special case: this is sugar for &f
-      exprt tmp(ID_address_of, pointer_type(expr.type()));
+      address_of_exprt tmp(expr, pointer_type(expr.type()));
       tmp.set("#implicit", true);
       tmp.add_source_location()=expr.source_location();
-      tmp.move_to_operands(expr);
-      expr.swap(tmp);
+      expr=tmp;
     }
   }
 }
@@ -1778,11 +1777,10 @@ void c_typecheck_baset::typecheck_expr_function_identifier(exprt &expr)
 {
   if(expr.type().id()==ID_code)
   {
-    exprt tmp(ID_address_of, pointer_type(expr.type()));
+    address_of_exprt tmp(expr, pointer_type(expr.type()));
     tmp.set(ID_C_implicit, true);
     tmp.add_source_location()=expr.source_location();
-    tmp.move_to_operands(expr);
-    expr.swap(tmp);
+    expr=tmp;
   }
 }
 
diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp
index 62e651f9135..5195e653364 100644
--- a/src/ansi-c/c_typecheck_type.cpp
+++ b/src/ansi-c/c_typecheck_type.cpp
@@ -1498,9 +1498,7 @@ void c_typecheck_baset::adjust_function_parameter(typet &type) const
   {
     // see ISO/IEC 9899:1999 page 199 clause 8,
     // may be hidden in typedef
-    pointer_typet tmp;
-    tmp.subtype()=type;
-    type.swap(tmp);
+    type=pointer_type(type);
   }
   else if(type.id()==ID_KnR)
   {
diff --git a/src/cpp/cpp_constructor.cpp b/src/cpp/cpp_constructor.cpp
index e584d25fc45..9be6e8c3f01 100644
--- a/src/cpp/cpp_constructor.cpp
+++ b/src/cpp/cpp_constructor.cpp
@@ -289,10 +289,7 @@ codet cpp_typecheckt::cpp_constructor(
     assert(tmp_this.id()==ID_address_of
            && tmp_this.op0().id()=="new_object");
 
-    exprt address_of(ID_address_of, typet(ID_pointer));
-    address_of.type().subtype()=object_tc.type();
-    address_of.copy_to_operands(object_tc);
-    tmp_this.swap(address_of);
+    tmp_this=address_of_exprt(object_tc);
 
     if(block.operands().empty())
       return to_code(initializer);
diff --git a/src/cpp/cpp_convert_type.cpp b/src/cpp/cpp_convert_type.cpp
index cd552871b96..b98845964e0 100644
--- a/src/cpp/cpp_convert_type.cpp
+++ b/src/cpp/cpp_convert_type.cpp
@@ -251,8 +251,8 @@ void cpp_convert_typet::read_function_type(const typet &type)
         // see if it's an array type
         if(final_type.id()==ID_array)
         {
-          final_type.id(ID_pointer);
-          final_type.remove(ID_size);
+          // turn into pointer type
+          final_type=pointer_type(final_type.subtype());
         }
 
         code_typet::parametert new_parameter(final_type);
diff --git a/src/cpp/cpp_destructor.cpp b/src/cpp/cpp_destructor.cpp
index 6f4157c15f0..6a35398475c 100644
--- a/src/cpp/cpp_destructor.cpp
+++ b/src/cpp/cpp_destructor.cpp
@@ -142,10 +142,7 @@ codet cpp_typecheckt::cpp_destructor(
     assert(tmp_this.id()==ID_address_of
            && tmp_this.op0().id()=="new_object");
 
-    exprt address_of(ID_address_of, typet(ID_pointer));
-    address_of.type().subtype()=object.type();
-    address_of.copy_to_operands(object);
-    tmp_this.swap(address_of);
+    tmp_this=address_of_exprt(object, pointer_type(object.type()));
 
     new_code.swap(initializer);
   }
diff --git a/src/cpp/cpp_typecheck_compound_type.cpp b/src/cpp/cpp_typecheck_compound_type.cpp
index 12fbfa67849..36d2a2e70b6 100644
--- a/src/cpp/cpp_typecheck_compound_type.cpp
+++ b/src/cpp/cpp_typecheck_compound_type.cpp
@@ -16,6 +16,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #include <util/arith_tools.h>
 #include <util/simplify_expr.h>
 #include <util/std_types.h>
+#include <util/c_types.h>
 
 #include <ansi-c/c_qualifiers.h>
 
@@ -545,7 +546,7 @@ void cpp_typecheckt::typecheck_compound_declarator(
 
         // add a virtual-table pointer
         struct_typet::componentt compo;
-        compo.type()=pointer_typet(symbol_typet(vt_name));
+        compo.type()=pointer_type(symbol_typet(vt_name));
         compo.set_name(id2string(symbol.name) +"::@vtable_pointer");
         compo.set(ID_base_name, "@vtable_pointer");
         compo.set(
@@ -567,7 +568,7 @@ void cpp_typecheckt::typecheck_compound_declarator(
 
       // add an entry to the virtual table
       struct_typet::componentt vt_entry;
-      vt_entry.type()=pointer_typet(component.type());
+      vt_entry.type()=pointer_type(component.type());
       vt_entry.set_name(id2string(vtit->first)+"::"+virtual_name);
       vt_entry.set(ID_base_name, virtual_name);
       vt_entry.set(ID_pretty_name, virtual_name);
@@ -1353,7 +1354,7 @@ void cpp_typecheckt::add_this_to_method_type(
   if(has_volatile(method_qualifier))
     subtype.set(ID_C_volatile, true);
 
-  parameter.type()=pointer_typet(subtype);
+  parameter.type()=pointer_type(subtype);
 }
 
 void cpp_typecheckt::add_anonymous_members_to_scope(
diff --git a/src/cpp/cpp_typecheck_conversions.cpp b/src/cpp/cpp_typecheck_conversions.cpp
index 4b76a2ebd40..f2c5d04f36f 100644
--- a/src/cpp/cpp_typecheck_conversions.cpp
+++ b/src/cpp/cpp_typecheck_conversions.cpp
@@ -73,15 +73,13 @@ bool cpp_typecheckt::standard_conversion_array_to_pointer(
 {
   assert(expr.type().id()==ID_array);
 
-  exprt index(ID_index, expr.type().subtype());
-  index.copy_to_operands(expr, from_integer(0, index_type()));
-  index.set(ID_C_lvalue, true);
+  index_exprt index(
+    expr,
+    from_integer(0, index_type()));
 
-  pointer_typet pointer;
-  pointer.subtype()=expr.type().subtype();
+  index.set(ID_C_lvalue, true);
 
-  new_expr=exprt(ID_address_of, pointer);
-  new_expr.move_to_operands(index);
+  new_expr=address_of_exprt(index);
 
   return true;
 }
@@ -96,17 +94,10 @@ bool cpp_typecheckt::standard_conversion_array_to_pointer(
 bool cpp_typecheckt::standard_conversion_function_to_pointer(
   const exprt &expr, exprt &new_expr) const
 {
-  const code_typet &func_type=to_code_type(expr.type());
-
   if(!expr.get_bool(ID_C_lvalue))
     return false;
 
-  pointer_typet pointer;
-  pointer.subtype()=func_type;
-
-  new_expr=exprt(ID_address_of);
-  new_expr.copy_to_operands(expr);
-  new_expr.type()=pointer;
+  new_expr=address_of_exprt(expr);
 
   return true;
 }
@@ -887,16 +878,13 @@ bool cpp_typecheckt::user_defined_conversion_sequence(
 
         if(subtype_typecast(from_struct, to_struct))
         {
-          exprt address(ID_address_of, pointer_typet());
-          address.copy_to_operands(expr);
-          address.type().subtype()=expr.type();
+          exprt address=address_of_exprt(expr);
 
           // simplify address
           if(expr.id()==ID_dereference)
             address=expr.op0();
 
-          pointer_typet ptr_sub;
-          ptr_sub.subtype()=type;
+          pointer_typet ptr_sub=pointer_type(type);
           c_qualifierst qual_from;
           qual_from.read(expr.type());
           qual_from.write(ptr_sub.subtype());
@@ -1019,62 +1007,60 @@ bool cpp_typecheckt::user_defined_conversion_sequence(
           }
           else if(from_struct.is_not_nil() && arg1_struct.is_not_nil())
           {
-              // try derived-to-base conversion
-              exprt expr_pfrom(ID_address_of, pointer_typet());
-              expr_pfrom.type().subtype()=expr.type();
-              expr_pfrom.copy_to_operands(expr);
-
-              pointer_typet pto;
-              pto.subtype()=arg1_type;
-
-              exprt expr_ptmp;
-              tmp_rank=0;
-              if(standard_conversion_sequence(
-                  expr_pfrom, pto, expr_ptmp, tmp_rank))
+            // try derived-to-base conversion
+            address_of_exprt expr_pfrom(expr, pointer_type(expr.type()));
+            pointer_typet pto=pointer_type(arg1_type);
+
+            exprt expr_ptmp;
+            tmp_rank=0;
+            if(standard_conversion_sequence(
+                expr_pfrom, pto, expr_ptmp, tmp_rank))
+            {
+              // check if it's ambiguous
+              if(found)
+                return false;
+              found=true;
+
+              rank+=tmp_rank;
+
+              // create temporary object
+              exprt expr_deref=
+                exprt(ID_dereference, expr_ptmp.type().subtype());
+              expr_deref.set(ID_C_lvalue, true);
+              expr_deref.copy_to_operands(expr_ptmp);
+              expr_deref.add_source_location()=expr.source_location();
+
+              exprt new_object("new_object", type);
+              new_object.set(ID_C_lvalue, true);
+              new_object.type().set(ID_C_constant, false);
+
+              exprt func_symb=cpp_symbol_expr(lookup(component.get(ID_name)));
+              func_symb.type()=comp_type;
               {
-                // check if it's ambiguous
-                if(found)
-                  return false;
-                found=true;
-
-                rank+=tmp_rank;
-
-                // create temporary object
-                exprt expr_deref=
-                  exprt(ID_dereference, expr_ptmp.type().subtype());
-                expr_deref.set(ID_C_lvalue, true);
-                expr_deref.copy_to_operands(expr_ptmp);
-                expr_deref.add_source_location()=expr.source_location();
-
-                exprt new_object("new_object", type);
-                new_object.set(ID_C_lvalue, true);
-                new_object.type().set(ID_C_constant, false);
-
-                exprt func_symb=cpp_symbol_expr(lookup(component.get(ID_name)));
-                func_symb.type()=comp_type;
-                {
-                  exprt tmp("already_typechecked");
-                  tmp.copy_to_operands(func_symb);
-                  func_symb.swap(func_symb);
-                }
-
-                side_effect_expr_function_callt ctor_expr;
-                ctor_expr.add_source_location()=expr.source_location();
-                ctor_expr.function().swap(func_symb);
-                ctor_expr.arguments().push_back(expr_deref);
-                typecheck_side_effect_function_call(ctor_expr);
-
-                new_expr.swap(ctor_expr);
-
-                assert(new_expr.get(ID_statement)==ID_temporary_object);
-
-                if(to.get_bool(ID_C_constant))
-                  new_expr.type().set(ID_C_constant, true);
+                exprt tmp("already_typechecked");
+                tmp.copy_to_operands(func_symb);
+                func_symb.swap(func_symb);
               }
+
+              side_effect_expr_function_callt ctor_expr;
+              ctor_expr.add_source_location()=expr.source_location();
+              ctor_expr.function().swap(func_symb);
+              ctor_expr.arguments().push_back(expr_deref);
+              typecheck_side_effect_function_call(ctor_expr);
+
+              new_expr.swap(ctor_expr);
+
+              INVARIANT(
+                new_expr.get(ID_statement)==ID_temporary_object,
+                "statement ID");
+
+              if(to.get_bool(ID_C_constant))
+                new_expr.type().set(ID_C_constant, true);
             }
           }
-          if(found)
-            return true;
+        }
+        if(found)
+          return true;
       }
   }
 
@@ -1297,9 +1283,8 @@ bool cpp_typecheckt::reference_binding(
         address_of_exprt tmp;
         tmp.add_source_location()=expr.source_location();
         tmp.object()=expr;
-        tmp.type()=pointer_typet();
+        tmp.type()=pointer_type(tmp.op0().type());
         tmp.type().set(ID_C_reference, true);
-        tmp.type().subtype()=tmp.op0().type();
         new_expr.swap(tmp);
       }
 
@@ -1427,10 +1412,9 @@ bool cpp_typecheckt::reference_binding(
   if(user_defined_conversion_sequence(arg_expr, type.subtype(), new_expr, rank))
   {
     address_of_exprt tmp;
-    tmp.type()=pointer_typet();
+    tmp.type()=pointer_type(new_expr.type());
     tmp.object()=new_expr;
     tmp.type().set(ID_C_reference, true);
-    tmp.type().subtype()= new_expr.type();
     tmp.add_source_location()=new_expr.source_location();
     new_expr.swap(tmp);
     return true;
@@ -1449,12 +1433,11 @@ bool cpp_typecheckt::reference_binding(
       new_expr.swap(tmp);
     }
 
-    exprt tmp(ID_address_of, pointer_typet());
-    tmp.copy_to_operands(new_expr);
+    address_of_exprt tmp(new_expr, pointer_type(new_expr.type()));
     tmp.type().set(ID_C_reference, true);
-    tmp.type().subtype()= new_expr.type();
     tmp.add_source_location()=new_expr.source_location();
-    new_expr.swap(tmp);
+
+    new_expr=tmp;
     return true;
   }
 
@@ -1715,10 +1698,9 @@ bool cpp_typecheckt::const_typecast(
     if(new_expr.type()!=type.subtype())
       return false;
 
-    exprt address_of(ID_address_of, type);
-    address_of.copy_to_operands(expr);
+    exprt address_of=address_of_exprt(expr, to_pointer_type(type));
     add_implicit_dereference(address_of);
-    new_expr.swap(address_of);
+    new_expr=address_of;
     return true;
   }
   else if(type.id()==ID_pointer)
@@ -1880,9 +1862,7 @@ bool cpp_typecheckt::reinterpret_typecast(
 
   if(is_reference(type) && e.get_bool(ID_C_lvalue))
   {
-    exprt tmp(ID_address_of, pointer_typet());
-    tmp.type().subtype()=e.type();
-    tmp.copy_to_operands(e);
+    exprt tmp=address_of_exprt(e);
     tmp.make_typecast(type);
     new_expr.swap(tmp);
     return true;
@@ -1946,10 +1926,8 @@ bool cpp_typecheckt::static_typecast(
           return true;
         }
 
-        exprt address_of(ID_address_of, pointer_typet());
-        address_of.type().subtype()=e.type();
-        address_of.copy_to_operands(e);
-        make_ptr_typecast(address_of , type);
+        exprt address_of=address_of_exprt(e);
+        make_ptr_typecast(address_of, type);
         new_expr.swap(address_of);
         return true;
       }
diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp
index e54f69589ff..87f15a16a3b 100644
--- a/src/cpp/cpp_typecheck_expr.cpp
+++ b/src/cpp/cpp_typecheck_expr.cpp
@@ -722,9 +722,7 @@ void cpp_typecheckt::typecheck_expr_address_of(exprt &expr)
     // we take the address of the method.
     assert(expr.op0().id()==ID_member);
     exprt symb=cpp_symbol_expr(lookup(expr.op0().get(ID_component_name)));
-    exprt address(ID_address_of, typet(ID_pointer));
-    address.copy_to_operands(symb);
-    address.type().subtype()=symb.type();
+    address_of_exprt address(symb, pointer_type(symb.type()));
     address.set(ID_C_implicit, true);
     expr.op0().swap(address);
   }
@@ -757,7 +755,7 @@ void cpp_typecheckt::typecheck_expr_address_of(exprt &expr)
   const bool is_ref=is_reference(expr.type());
   c_typecheck_baset::typecheck_expr_address_of(expr);
   if(is_ref)
-    expr.type()=reference_typet(expr.type().subtype());
+    expr.type()=reference_type(expr.type().subtype());
 }
 
 void cpp_typecheckt::typecheck_expr_throw(exprt &expr)
@@ -810,8 +808,8 @@ void cpp_typecheckt::typecheck_expr_new(exprt &expr)
     expr.set(ID_size, to_array_type(expr.type()).size());
 
     // new actually returns a pointer, not an array
-    pointer_typet ptr_type;
-    ptr_type.subtype()=expr.type().subtype();
+    pointer_typet ptr_type=
+      pointer_type(expr.type().subtype());
     expr.type().swap(ptr_type);
   }
   else
@@ -821,8 +819,7 @@ void cpp_typecheckt::typecheck_expr_new(exprt &expr)
 
     expr.set(ID_statement, ID_cpp_new);
 
-    pointer_typet ptr_type;
-    ptr_type.subtype().swap(expr.type());
+    pointer_typet ptr_type=pointer_type(expr.type());
     expr.type().swap(ptr_type);
   }
 
@@ -2255,11 +2252,9 @@ void cpp_typecheckt::typecheck_side_effect_function_call(
       if(operand.type().id()!=ID_pointer &&
          operand.type()==argument.type().subtype())
       {
-        exprt tmp(ID_address_of, typet(ID_pointer));
-        tmp.type().subtype()=operand.type();
+        address_of_exprt tmp(operand, pointer_type(operand.type()));
         tmp.add_source_location()=operand.source_location();
-        tmp.move_to_operands(operand);
-        operand.swap(tmp);
+        operand=tmp;
       }
     }
   }
@@ -2671,10 +2666,7 @@ void cpp_typecheckt::convert_pmop(exprt &expr)
     else
     {
       assert(expr.op0().get_bool(ID_C_lvalue));
-      exprt address_of(ID_address_of, typet(ID_pointer));
-      address_of.copy_to_operands(expr.op0());
-      address_of.type().subtype()=address_of.op0().type();
-      expr.op0().swap(address_of);
+      expr.op0()=address_of_exprt(expr.op0());
     }
   }
 
diff --git a/src/cpp/cpp_typecheck_type.cpp b/src/cpp/cpp_typecheck_type.cpp
index cf392b2957c..41fcd49b68c 100644
--- a/src/cpp/cpp_typecheck_type.cpp
+++ b/src/cpp/cpp_typecheck_type.cpp
@@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 
 #include <util/source_location.h>
 #include <util/simplify_expr.h>
+#include <util/c_types.h>
 
 #include <ansi-c/c_qualifiers.h>
 
@@ -107,8 +108,7 @@ void cpp_typecheckt::typecheck_type(typet &type)
           // Add 'this' to the parameters
           exprt a0(ID_parameter);
           a0.set(ID_C_base_name, ID_this);
-          a0.type().id(ID_pointer);
-          a0.type().subtype() = class_object;
+          a0.type()=pointer_type(class_object);
           parameters.insert(parameters.begin(), a0);
         }
       }
diff --git a/src/cpp/cpp_typecheck_virtual_table.cpp b/src/cpp/cpp_typecheck_virtual_table.cpp
index b36e42d1320..f882db1f1af 100644
--- a/src/cpp/cpp_typecheck_virtual_table.cpp
+++ b/src/cpp/cpp_typecheck_virtual_table.cpp
@@ -11,7 +11,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 
 #include "cpp_typecheck.h"
 
-#include <util/std_types.h>
+#include <util/c_types.h>
 #include <util/std_expr.h>
 
 void cpp_typecheckt::do_virtual_table(const symbolt &symbol)
@@ -32,21 +32,20 @@ void cpp_typecheckt::do_virtual_table(const symbolt &symbol)
     const code_typet &code_type=to_code_type(compo.type());
     assert(code_type.parameters().size() > 0);
 
-    const pointer_typet &pointer_type =
-      static_cast<const pointer_typet&>(code_type.parameters()[0].type());
+    const pointer_typet &parameter_pointer_type=
+      to_pointer_type(code_type.parameters()[0].type());
 
-    irep_idt class_id=pointer_type.subtype().get("identifier");
+    irep_idt class_id=parameter_pointer_type.subtype().get("identifier");
 
     std::map<irep_idt, exprt> &value_map =
       vt_value_maps[class_id];
 
-
     exprt e=symbol_exprt(compo.get_name(), code_type);
 
     if(compo.get_bool("is_pure_virtual"))
     {
-      pointer_typet pointer_type(code_type);
-      e=null_pointer_exprt(pointer_type);
+      pointer_typet code_pointer_type=pointer_type(code_type);
+      e=null_pointer_exprt(code_pointer_type);
       value_map[compo.get("virtual_name")]=e;
     }
     else
diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp
index a2cd41a8dd2..87e9ad099d7 100644
--- a/src/cpp/parse.cpp
+++ b/src/cpp/parse.cpp
@@ -6476,7 +6476,7 @@ bool Parser::rPrimaryExpr(exprt &exp)
 
   case TOK_NULLPTR:
     lex.get_token(tk);
-    exp=constant_exprt(ID_NULL, pointer_typet(typet(ID_nullptr)));
+    exp=constant_exprt(ID_NULL, typet(ID_pointer, typet(ID_nullptr)));
     set_location(exp, tk);
     #ifdef DEBUG
     std::cout << std::string(__indent, ' ') << "Parser::rPrimaryExpr 6\n";
diff --git a/src/goto-instrument/function.cpp b/src/goto-instrument/function.cpp
index 9af29573ad0..6c62a07f4f7 100644
--- a/src/goto-instrument/function.cpp
+++ b/src/goto-instrument/function.cpp
@@ -32,7 +32,7 @@ code_function_callt function_to_call(
   if(s_it==symbol_table.symbols.end())
   {
     // not there
-    pointer_typet p(char_type());
+    typet p=pointer_type(char_type());
     p.subtype().set(ID_C_constant, true);
 
     code_typet function_type;
diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp
index 968b49026c7..1a96eb4ee34 100644
--- a/src/goto-instrument/goto_program2code.cpp
+++ b/src/goto-instrument/goto_program2code.cpp
@@ -384,7 +384,7 @@ goto_programt::const_targett goto_program2codet::convert_assign_varargs(
       static_cast<typet const&>(r.find(ID_C_va_arg_type));
 
     dereference_exprt deref(
-      null_pointer_exprt(pointer_typet(va_arg_type)),
+      null_pointer_exprt(pointer_type(va_arg_type)),
       va_arg_type);
 
     type_of.arguments().push_back(deref);
@@ -1378,7 +1378,7 @@ goto_programt::const_targett goto_program2codet::convert_start_thread(
     // we don't bother setting the type
     f.lhs()=cf.lhs();
     f.function()=symbol_exprt("pthread_create", code_typet());
-    exprt n=null_pointer_exprt(pointer_typet(empty_typet()));
+    exprt n=null_pointer_exprt(pointer_type(empty_typet()));
     f.arguments().push_back(n);
     f.arguments().push_back(n);
     f.arguments().push_back(cf.function());
diff --git a/src/goto-instrument/thread_instrumentation.cpp b/src/goto-instrument/thread_instrumentation.cpp
index 3cfb0b57759..a2943424a33 100644
--- a/src/goto-instrument/thread_instrumentation.cpp
+++ b/src/goto-instrument/thread_instrumentation.cpp
@@ -43,7 +43,7 @@ void thread_exit_instrumentation(goto_programt &goto_program)
   binary_exprt get_may("get_may");
 
   // NULL is any
-  get_may.op0()=null_pointer_exprt(to_pointer_type(pointer_type(empty_typet())));
+  get_may.op0()=null_pointer_exprt(pointer_type(empty_typet()));
   get_may.op1()=address_of_exprt(mutex_locked_string);
 
   end->make_assertion(not_exprt(get_may));
diff --git a/src/goto-instrument/wmm/shared_buffers.cpp b/src/goto-instrument/wmm/shared_buffers.cpp
index 5e70bc9c6a5..f68b29b2fec 100644
--- a/src/goto-instrument/wmm/shared_buffers.cpp
+++ b/src/goto-instrument/wmm/shared_buffers.cpp
@@ -6,13 +6,12 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
-
 #include "shared_buffers.h"
-
 #include "fence.h"
-
 #include "../rw_set.h"
 
+#include <util/c_types.h>
+
 /// returns a unique id (for fresh variables)
 std::string shared_bufferst::unique(void)
 {
@@ -54,7 +53,7 @@ const shared_bufferst::varst &shared_bufferst::operator()(
       object,
       symbol.base_name,
       "$read_delayed_var",
-      pointer_typet(symbol.type));
+      pointer_type(symbol.type));
 
   for(unsigned cnt=0; cnt<nb_threads; cnt++)
   {
@@ -121,7 +120,7 @@ void shared_bufferst::add_initialization(goto_programt &goto_program)
     assignment(goto_program, t, source_location, vars.second.read_delayed,
       false_exprt());
     assignment(goto_program, t, source_location, vars.second.read_delayed_var,
-      null_pointer_exprt(pointer_typet(vars.second.type)));
+      null_pointer_exprt(pointer_type(vars.second.type)));
 
     for(const auto &id : vars.second.r_buff0_thds)
       assignment(goto_program, t, source_location, id, false_exprt());
@@ -1173,7 +1172,7 @@ void shared_bufferst::cfg_visitort::weak_memory(
                     r_it->second.object, vars.type);
                   symbol_exprt new_read_expr=symbol_exprt(
                     vars.read_delayed_var,
-                  pointer_typet(vars.type));
+                    pointer_type(vars.type));
                   symbol_exprt read_delayed_expr=symbol_exprt(
                     vars.read_delayed, bool_typet());
 
diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp
index e7b128ff282..530e5e31574 100644
--- a/src/goto-programs/builtin_functions.cpp
+++ b/src/goto-programs/builtin_functions.cpp
@@ -602,7 +602,7 @@ void goto_convertt::do_java_new(
   // we produce a malloc side-effect, which stays
   side_effect_exprt malloc_expr(ID_malloc);
   malloc_expr.copy_to_operands(object_size);
-  malloc_expr.type()=pointer_typet(object_type);
+  malloc_expr.type()=rhs.type();
 
   goto_programt::targett t_n=dest.add_instruction(ASSIGN);
   t_n->code=code_assignt(lhs, malloc_expr);
@@ -658,7 +658,7 @@ void goto_convertt::do_java_new_array(
   // we produce a malloc side-effect, which stays
   side_effect_exprt malloc_expr(ID_malloc);
   malloc_expr.copy_to_operands(object_size);
-  malloc_expr.type()=pointer_typet(object_type);
+  malloc_expr.type()=rhs.type();
 
   goto_programt::targett t_n=dest.add_instruction(ASSIGN);
   t_n->code=code_assignt(lhs, malloc_expr);
@@ -1384,8 +1384,7 @@ void goto_convertt::do_function_call_symbol(
 
     if(lhs.is_not_nil())
     {
-      typet t=pointer_typet();
-      t.subtype()=lhs.type();
+      typet t=pointer_type(lhs.type());
       dereference_exprt rhs(lhs.type());
       rhs.op0()=typecast_exprt(list_arg, t);
       rhs.add_source_location()=function.source_location();
diff --git a/src/goto-programs/class_identifier.cpp b/src/goto-programs/class_identifier.cpp
index bbdc94c8533..3e92586e759 100644
--- a/src/goto-programs/class_identifier.cpp
+++ b/src/goto-programs/class_identifier.cpp
@@ -12,6 +12,7 @@ Author: Chris Smowton, chris.smowton@diffblue.com
 #include "class_identifier.h"
 
 #include <util/std_expr.h>
+#include <util/c_types.h>
 #include <util/namespace.h>
 
 /// \par parameters: Struct expression
@@ -66,7 +67,7 @@ exprt get_class_identifier_field(
          "Non-pointer this-arg in remove-virtuals?");
   const auto &points_to=this_expr.type().subtype();
   if(points_to==empty_typet())
-    this_expr=typecast_exprt(this_expr, pointer_typet(suggested_type));
+    this_expr=typecast_exprt(this_expr, pointer_type(suggested_type));
   exprt deref=dereference_exprt(this_expr, this_expr.type().subtype());
   return build_class_identifier(deref, ns);
 }
diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp
index 3218d3f7f81..5f308b3f9ff 100644
--- a/src/goto-programs/goto_convert.cpp
+++ b/src/goto-programs/goto_convert.cpp
@@ -712,9 +712,7 @@ void goto_convertt::convert_decl(
   if(destructor.is_not_nil())
   {
     // add "this"
-    exprt this_expr(ID_address_of, pointer_typet());
-    this_expr.type().subtype()=symbol.type;
-    this_expr.copy_to_operands(symbol_expr);
+    address_of_exprt this_expr(symbol_expr, pointer_type(symbol.type));
     destructor.arguments().push_back(this_expr);
 
     targets.destructor_stack.push_back(destructor);
diff --git a/src/goto-programs/goto_convert_new_switch_case.cpp b/src/goto-programs/goto_convert_new_switch_case.cpp
index 290c3a241e2..cf8c6579d63 100644
--- a/src/goto-programs/goto_convert_new_switch_case.cpp
+++ b/src/goto-programs/goto_convert_new_switch_case.cpp
@@ -555,9 +555,7 @@ void goto_convertt::convert_decl(
   if(destructor.is_not_nil())
   {
     // add "this"
-    exprt this_expr(ID_address_of, pointer_typet());
-    this_expr.type().subtype()=symbol.type;
-    this_expr.copy_to_operands(symbol_expr);
+    address_of_exprt this_expr(symbol_expr, pointer_type(symbol.type));
     destructor.arguments().push_back(this_expr);
 
     targets.destructor_stack.push_back(destructor);
diff --git a/src/goto-programs/remove_asm.cpp b/src/goto-programs/remove_asm.cpp
index bd3517ce0a3..29958434d48 100644
--- a/src/goto-programs/remove_asm.cpp
+++ b/src/goto-programs/remove_asm.cpp
@@ -16,6 +16,7 @@ Date:   December 2014
 
 #include <sstream>
 
+#include <util/c_types.h>
 #include <util/std_expr.h>
 
 #include <ansi-c/string_constant.h>
@@ -61,7 +62,8 @@ void remove_asmt::gcc_asm_function_call(
   code_function_callt function_call;
   function_call.lhs().make_nil();
 
-  const pointer_typet void_pointer=pointer_typet(void_typet());
+  const typet void_pointer=
+    pointer_type(void_typet());
 
   // outputs
   forall_operands(it, code.op1())
diff --git a/src/goto-programs/remove_exceptions.cpp b/src/goto-programs/remove_exceptions.cpp
index 4b24980f5be..09fe45f2dec 100644
--- a/src/goto-programs/remove_exceptions.cpp
+++ b/src/goto-programs/remove_exceptions.cpp
@@ -20,6 +20,7 @@ Date:   December 2016
 #include <stack>
 #include <algorithm>
 
+#include <util/c_types.h>
 #include <util/std_expr.h>
 #include <util/symbol_table.h>
 
@@ -108,12 +109,12 @@ void remove_exceptionst::add_exceptional_returns(
     new_symbol.base_name=id2string(function_symbol.base_name)+EXC_SUFFIX;
     new_symbol.name=id2string(function_symbol.name)+EXC_SUFFIX;
     new_symbol.mode=function_symbol.mode;
-    new_symbol.type=typet(ID_pointer, empty_typet());
+    new_symbol.type=pointer_type(empty_typet());
     symbol_table.add(new_symbol);
 
     // initialize the exceptional return with NULL
     symbol_exprt lhs_expr_null=new_symbol.symbol_expr();
-    null_pointer_exprt rhs_expr_null((pointer_typet(empty_typet())));
+    null_pointer_exprt rhs_expr_null(pointer_type(empty_typet()));
     goto_programt::targett t_null=
       goto_program.insert_before(goto_program.instructions.begin());
     t_null->make_assignment();
@@ -146,7 +147,7 @@ void remove_exceptionst::instrument_exception_handler(
       symbol_table.lookup(id2string(function_id)+EXC_SUFFIX);
     // next we reset the exceptional return to NULL
     symbol_exprt lhs_expr_null=function_symbol.symbol_expr();
-    null_pointer_exprt rhs_expr_null((pointer_typet(empty_typet())));
+    null_pointer_exprt rhs_expr_null(pointer_type(empty_typet()));
 
     // add the assignment
     goto_programt::targett t_null=goto_program.insert_after(instr_it);
@@ -326,7 +327,7 @@ void remove_exceptionst::instrument_function_call(
     // add a null check (so that instanceof can be applied)
     equal_exprt eq_null(
       callee_exc,
-      null_pointer_exprt(pointer_typet(empty_typet())));
+      null_pointer_exprt(pointer_type(empty_typet())));
     goto_programt::targett t_null=goto_program.insert_after(instr_it);
     t_null->make_goto(next_it);
     t_null->source_location=instr_it->source_location;
diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp
index 142fc8a957c..bec1ce5ea47 100644
--- a/src/goto-programs/remove_function_pointers.cpp
+++ b/src/goto-programs/remove_function_pointers.cpp
@@ -375,10 +375,7 @@ void remove_function_pointerst::remove_function_pointer(
     t3->make_goto(t_final, true_exprt());
 
     // goto to call
-    address_of_exprt address_of;
-    address_of.object()=fun;
-    address_of.type()=pointer_typet();
-    address_of.type().subtype()=fun.type();
+    address_of_exprt address_of(fun, pointer_type(fun.type()));
 
     if(address_of.type()!=pointer.type())
       address_of.make_typecast(pointer.type());
diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp
index c512e2b3212..5ae06fceeb0 100644
--- a/src/goto-programs/remove_virtual_functions.cpp
+++ b/src/goto-programs/remove_virtual_functions.cpp
@@ -10,13 +10,13 @@ Author: Daniel Kroening, kroening@kroening.com
 /// Remove Virtual Function (Method) Calls
 
 #include "remove_virtual_functions.h"
+#include "class_hierarchy.h"
+#include "class_identifier.h"
 
+#include <util/c_types.h>
 #include <util/prefix.h>
 #include <util/type_eq.h>
 
-#include "class_hierarchy.h"
-#include "class_identifier.h"
-
 class remove_virtual_functionst
 {
 public:
@@ -147,7 +147,8 @@ void remove_virtual_functionst::remove_virtual_function(
         t1->make_function_call(code);
         auto &newcall=to_code_function_call(t1->code);
         newcall.function()=fun.symbol_expr;
-        pointer_typet need_type(symbol_typet(fun.symbol_expr.get(ID_C_class)));
+        typet need_type=
+          pointer_type(symbol_typet(fun.symbol_expr.get(ID_C_class)));
         if(!type_eq(newcall.arguments()[0].type(), need_type, ns))
           newcall.arguments()[0].make_typecast(need_type);
       }
diff --git a/src/goto-programs/string_abstraction.cpp b/src/goto-programs/string_abstraction.cpp
index da6119d2429..299d27cceef 100644
--- a/src/goto-programs/string_abstraction.cpp
+++ b/src/goto-programs/string_abstraction.cpp
@@ -207,7 +207,7 @@ void string_abstractiont::add_argument(
     const irep_idt &identifier)
 {
   typet final_type=is_ptr_argument(type)?
-    type:pointer_typet(type);
+                   type:pointer_type(type);
 
   str_args.push_back(code_typet::parametert(final_type));
   str_args.back().add_source_location()=fct_symbol.location;
@@ -689,7 +689,7 @@ const typet &string_abstractiont::build_abstraction_type_rec(const typet &type,
     // char* or void* or char[]
     if(is_char_type(eff_type.subtype()) ||
         eff_type.subtype().id()==ID_empty)
-      map_entry.first->second=pointer_typet(string_struct);
+      map_entry.first->second=pointer_type(string_struct);
     else
     {
       const typet &subt=build_abstraction_type_rec(eff_type.subtype(), known);
@@ -699,8 +699,7 @@ const typet &string_abstractiont::build_abstraction_type_rec(const typet &type,
           map_entry.first->second=
             array_typet(subt, to_array_type(eff_type).size());
         else
-          map_entry.first->second=
-            pointer_typet(subt);
+          map_entry.first->second=pointer_type(subt);
       }
     }
   }
diff --git a/src/goto-programs/string_instrumentation.cpp b/src/goto-programs/string_instrumentation.cpp
index 41bf92a529b..f4ce4129eed 100644
--- a/src/goto-programs/string_instrumentation.cpp
+++ b/src/goto-programs/string_instrumentation.cpp
@@ -825,14 +825,12 @@ void string_instrumentationt::do_strerror(
   }
 
   // return a pointer to some magic buffer
-  exprt index=exprt(ID_index, char_type());
-  index.copy_to_operands(
+  index_exprt index(
     symbol_buf.symbol_expr(),
-    from_integer(0, index_type()));
+    from_integer(0, index_type()),
+    char_type());
 
-  exprt ptr=exprt(ID_address_of, pointer_typet());
-  ptr.type().subtype()=char_type();
-  ptr.copy_to_operands(index);
+  address_of_exprt ptr(index);
 
   // make that zero-terminated
   {
diff --git a/src/goto-symex/auto_objects.cpp b/src/goto-symex/auto_objects.cpp
index f2a90b1550b..2338b102593 100644
--- a/src/goto-symex/auto_objects.cpp
+++ b/src/goto-symex/auto_objects.cpp
@@ -66,8 +66,9 @@ void goto_symext::initialize_auto_object(
     {
       // could be NULL nondeterministically
 
-      address_of_exprt address_of_expr=
-        address_of_exprt(make_auto_object(type.subtype()));
+      address_of_exprt address_of_expr(
+        make_auto_object(type.subtype()),
+        pointer_type);
 
       if_exprt rhs(
         side_effect_expr_nondett(bool_typet()),
diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp
index d3d26b540f2..d6e9fd416d8 100644
--- a/src/goto-symex/symex_builtin_functions.cpp
+++ b/src/goto-symex/symex_builtin_functions.cpp
@@ -169,7 +169,7 @@ void goto_symext::symex_malloc(
 
   if(object_type.id()==ID_array)
   {
-    rhs.type()=pointer_typet(value_symbol.type.subtype());
+    rhs.type()=pointer_type(value_symbol.type.subtype());
     index_exprt index_expr(value_symbol.type.subtype());
     index_expr.array()=value_symbol.symbol_expr();
     index_expr.index()=from_integer(0, index_type());
@@ -178,7 +178,7 @@ void goto_symext::symex_malloc(
   else
   {
     rhs.op0()=value_symbol.symbol_expr();
-    rhs.type()=pointer_typet(value_symbol.type);
+    rhs.type()=pointer_type(value_symbol.type);
   }
 
   if(rhs.type()!=lhs.type())
@@ -404,7 +404,7 @@ void goto_symext::symex_cpp_new(
 
   // make symbol expression
 
-  exprt rhs(ID_address_of, pointer_typet());
+  exprt rhs(ID_address_of, code.type());
   rhs.type().subtype()=code.type().subtype();
 
   if(do_array)
diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp
index 61dcecbf3a4..f066ee1065f 100644
--- a/src/goto-symex/symex_dereference.cpp
+++ b/src/goto-symex/symex_dereference.cpp
@@ -122,7 +122,7 @@ exprt goto_symext::address_arithmetic(
     }
 
     // do (expr.type() *)(((char *)op)+offset)
-    result=typecast_exprt(result, pointer_typet(char_type()));
+    result=typecast_exprt(result, pointer_type(char_type()));
 
     // there could be further dereferencing in the offset
     exprt offset=be.offset();
@@ -132,14 +132,14 @@ exprt goto_symext::address_arithmetic(
 
     // treat &array as &array[0]
     const typet &expr_type=ns.follow(expr.type());
-    pointer_typet dest_type;
+    typet dest_type_subtype;
 
     if(expr_type.id()==ID_array && !keep_array)
-      dest_type.subtype()=expr_type.subtype();
+      dest_type_subtype=expr_type.subtype();
     else
-      dest_type.subtype()=expr_type;
+      dest_type_subtype=expr_type;
 
-    result=typecast_exprt(result, dest_type);
+    result=typecast_exprt(result, pointer_type(dest_type_subtype));
   }
   else if(expr.id()==ID_index ||
           expr.id()==ID_member)
@@ -222,7 +222,7 @@ exprt goto_symext::address_arithmetic(
 
   const typet &expr_type=ns.follow(expr.type());
   assert((expr_type.id()==ID_array && !keep_array) ||
-         base_type_eq(pointer_typet(expr_type), result.type(), ns));
+         base_type_eq(pointer_type(expr_type), result.type(), ns));
 
   return result;
 }
@@ -281,7 +281,7 @@ void goto_symext::dereference_rec(
     index_exprt index_expr=to_index_expr(expr);
 
     address_of_exprt address_of_expr(index_expr.array());
-    address_of_expr.type()=pointer_typet(expr.type());
+    address_of_expr.type()=pointer_type(expr.type());
 
     dereference_exprt tmp;
     tmp.pointer()=plus_exprt(address_of_expr, index_expr.index());
@@ -318,7 +318,7 @@ void goto_symext::dereference_rec(
        to_address_of_expr(tc_op).object().type().id()==ID_array &&
        base_type_eq(
          expr.type(),
-         pointer_typet(to_address_of_expr(tc_op).object().type().subtype()),
+         pointer_type(to_address_of_expr(tc_op).object().type().subtype()),
          ns))
     {
       expr=
diff --git a/src/java_bytecode/java_bytecode_convert_class.cpp b/src/java_bytecode/java_bytecode_convert_class.cpp
index b6f28694f16..ab4c3d50ce9 100644
--- a/src/java_bytecode/java_bytecode_convert_class.cpp
+++ b/src/java_bytecode/java_bytecode_convert_class.cpp
@@ -20,6 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "java_bytecode_convert_method.h"
 #include "java_bytecode_language.h"
 
+#include <util/c_types.h>
 #include <util/namespace.h>
 #include <util/std_expr.h>
 
@@ -294,7 +295,7 @@ void java_bytecode_convert_classt::add_array_types()
     struct_type.components().push_back(comp1);
 
     struct_typet::componentt
-      comp2("data", pointer_typet(java_type_from_char(l)));
+      comp2("data", pointer_type(java_type_from_char(l)));
     struct_type.components().push_back(comp2);
 
     symbolt symbol;
@@ -366,7 +367,7 @@ void java_bytecode_convert_classt::add_string_type()
   // Use a pointer-to-unbounded-array instead of a pointer-to-char.
   // Saves some casting in the string refinement algorithm but may
   // be unnecessary.
-  string_type.components()[2].type()=pointer_typet(
+  string_type.components()[2].type()=pointer_type(
     array_typet(java_char_type(), infinity_exprt(java_int_type())));
   string_type.add_base(symbol_typet("java::java.lang.Object"));
 
@@ -392,9 +393,9 @@ void java_bytecode_convert_classt::add_string_type()
   string_equals_type.return_type()=java_boolean_type();
   code_typet::parametert thisparam;
   thisparam.set_this();
-  thisparam.type()=pointer_typet(symbol_typet(string_symbol.name));
+  thisparam.type()=java_reference_type(symbol_typet(string_symbol.name));
   code_typet::parametert otherparam;
-  otherparam.type()=pointer_typet(symbol_typet("java::java.lang.Object"));
+  otherparam.type()=java_reference_type(symbol_typet("java::java.lang.Object"));
   string_equals_type.parameters().push_back(thisparam);
   string_equals_type.parameters().push_back(otherparam);
   string_equals_symbol.type=std::move(string_equals_type);
diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp
index 9adf82a0218..8a02f4f8855 100644
--- a/src/java_bytecode/java_bytecode_convert_method.cpp
+++ b/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -9,29 +9,29 @@ Author: Daniel Kroening, kroening@kroening.com
 /// \file
 /// JAVA Bytecode Language Conversion
 
-#include "java_bytecode_convert_method.h"
-
 #ifdef DEBUG
 #include <iostream>
 #endif
 
-#include <util/namespace.h>
-#include <util/std_expr.h>
-#include <util/string2int.h>
-#include <util/prefix.h>
+#include "java_bytecode_convert_method.h"
+#include "java_bytecode_convert_method_class.h"
+#include "bytecode_info.h"
+#include "java_types.h"
+
 #include <util/arith_tools.h>
+#include <util/c_types.h>
 #include <util/ieee_float.h>
+#include <util/namespace.h>
+#include <util/prefix.h>
 #include <util/simplify_expr.h>
+#include <util/std_expr.h>
+#include <util/string2int.h>
 
 #include <linking/zero_initializer.h>
 
 #include <goto-programs/cfg.h>
 #include <analyses/cfg_dominators.h>
 
-#include "java_bytecode_convert_method_class.h"
-#include "bytecode_info.h"
-#include "java_types.h"
-
 #include <limits>
 #include <algorithm>
 #include <functional>
@@ -242,7 +242,8 @@ void java_bytecode_convert_method_lazy(
     code_typet &code_type=to_code_type(member_type);
     code_typet::parameterst &parameters=code_type.parameters();
     code_typet::parametert this_p;
-    const reference_typet object_ref_type(symbol_typet(class_symbol.name));
+    const reference_typet object_ref_type=
+      java_reference_type(symbol_typet(class_symbol.name));
     this_p.type()=object_ref_type;
     this_p.set_this();
     parameters.insert(parameters.begin(), this_p);
@@ -437,7 +438,7 @@ static member_exprt to_member(const exprt &pointer, const exprt &fieldref)
   symbol_typet class_type(fieldref.get(ID_class));
 
   exprt pointer2=
-    typecast_exprt(pointer, pointer_typet(class_type));
+    typecast_exprt(pointer, java_reference_type(class_type));
 
   const dereference_exprt obj_deref(pointer2, class_type);
 
@@ -1016,7 +1017,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
       assert(op.size()==1 && results.size()==1);
       code_blockt block;
       // TODO throw NullPointerException instead
-      const typecast_exprt lhs(op[0], pointer_typet(empty_typet()));
+      const typecast_exprt lhs(op[0], java_reference_type(empty_typet()));
       const exprt rhs(null_pointer_exprt(to_pointer_type(lhs.type())));
       const exprt not_equal_null(
         binary_relation_exprt(lhs, ID_notequal, rhs));
@@ -1103,7 +1104,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
             else
               code_type.set(ID_java_super_method_call, true);
           }
-          pointer_typet object_ref_type(thistype);
+          reference_typet object_ref_type=java_reference_type(thistype);
           code_typet::parametert this_p(object_ref_type);
           this_p.set_this();
           this_p.set_base_name("this");
@@ -1227,7 +1228,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
       const member_exprt data_ptr(
         deref,
         "data",
-        pointer_typet(java_type_from_char(type_char)));
+        pointer_type(java_type_from_char(type_char)));
 
       plus_exprt data_plus_offset(data_ptr, op[1], data_ptr.type());
       typet element_type=data_ptr.type().subtype();
@@ -1292,7 +1293,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
       const member_exprt data_ptr(
         deref,
         "data",
-        pointer_typet(java_type_from_char(type_char)));
+        pointer_type(java_type_from_char(type_char)));
 
       plus_exprt data_plus_offset(data_ptr, op[1], data_ptr.type());
       typet element_type=data_ptr.type().subtype();
@@ -1327,7 +1328,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
         // these need to be references to java.lang.String
         results[0]=arg0;
         symbol_typet string_type("java::java.lang.String");
-        results[0].type()=pointer_typet(string_type);
+        results[0].type()=java_reference_type(string_type);
       }
       else if(arg0.id()==ID_type)
       {
@@ -1500,7 +1501,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
       irep_idt number=to_constant_expr(arg0).get_value();
       assert(op.size()==1 && results.empty());
       code_ifthenelset code_branch;
-      const typecast_exprt lhs(op[0], pointer_typet(empty_typet()));
+      const typecast_exprt lhs(op[0], java_reference_type(empty_typet()));
       const exprt rhs(null_pointer_exprt(to_pointer_type(lhs.type())));
       code_branch.cond()=binary_relation_exprt(lhs, ID_notequal, rhs);
       code_branch.then_case()=code_gotot(label(number));
@@ -1514,7 +1515,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
       assert(op.size()==1 && results.empty());
       irep_idt number=to_constant_expr(arg0).get_value();
       code_ifthenelset code_branch;
-      const typecast_exprt lhs(op[0], pointer_typet(empty_typet()));
+      const typecast_exprt lhs(op[0], java_reference_type(empty_typet()));
       const exprt rhs(null_pointer_exprt(to_pointer_type(lhs.type())));
       code_branch.cond()=binary_relation_exprt(lhs, ID_equal, rhs);
       code_branch.then_case()=code_gotot(label(number));
@@ -1820,7 +1821,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
     {
       // use temporary since the stack symbol might get duplicated
       assert(op.empty() && results.size()==1);
-      const pointer_typet ref_type(arg0.type());
+      const reference_typet ref_type=java_reference_type(arg0.type());
       exprt java_new_expr=side_effect_exprt(ID_java_new, ref_type);
 
       if(!i_it->source_location.get_line().empty())
@@ -1865,7 +1866,8 @@ codet java_bytecode_convert_methodt::convert_instructions(
       else
         element_type='a';
 
-      const pointer_typet ref_type=java_array_type(element_type);
+      const reference_typet ref_type=
+        java_array_type(element_type);
 
       side_effect_exprt java_new_array(ID_java_new_array, ref_type);
       java_new_array.copy_to_operands(op[0]);
@@ -1905,7 +1907,8 @@ codet java_bytecode_convert_methodt::convert_instructions(
       op=pop(dimension);
       assert(results.size()==1);
 
-      const pointer_typet ref_type(arg0.type());
+      const reference_typet ref_type=
+        java_reference_type(arg0.type());
 
       side_effect_exprt java_new_array(ID_java_new_array, ref_type);
       java_new_array.operands()=op;
@@ -2020,7 +2023,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
       code_typet type;
       type.return_type()=void_typet();
       type.parameters().resize(1);
-      type.parameters()[0].type()=reference_typet(void_typet());
+      type.parameters()[0].type()=java_reference_type(void_typet());
       code_function_callt call;
       call.function()=symbol_exprt("java::monitorenter", type);
       call.lhs().make_nil();
@@ -2034,7 +2037,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
       code_typet type;
       type.return_type()=void_typet();
       type.parameters().resize(1);
-      type.parameters()[0].type()=reference_typet(void_typet());
+      type.parameters()[0].type()=java_reference_type(void_typet());
       code_function_callt call;
       call.function()=symbol_exprt("java::monitorexit", type);
       call.lhs().make_nil();
diff --git a/src/java_bytecode/java_bytecode_internal_additions.cpp b/src/java_bytecode/java_bytecode_internal_additions.cpp
index 9a0211239df..bc7715ecd9b 100644
--- a/src/java_bytecode/java_bytecode_internal_additions.cpp
+++ b/src/java_bytecode/java_bytecode_internal_additions.cpp
@@ -10,7 +10,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/std_types.h>
 #include <util/cprover_prefix.h>
-
 #include <util/c_types.h>
 
 void java_internal_additions(symbol_tablet &dest)
@@ -35,7 +34,7 @@ void java_internal_additions(symbol_tablet &dest)
     symbolt symbol;
     symbol.base_name="__CPROVER_malloc_object";
     symbol.name=CPROVER_PREFIX "malloc_object";
-    symbol.type=pointer_typet(empty_typet());
+    symbol.type=pointer_type(empty_typet());
     symbol.mode=ID_C;
     symbol.is_lvalue=true;
     symbol.is_state_var=true;
diff --git a/src/java_bytecode/java_bytecode_vtable.cpp b/src/java_bytecode/java_bytecode_vtable.cpp
index a352fbd74cd..68da4c6b494 100644
--- a/src/java_bytecode/java_bytecode_vtable.cpp
+++ b/src/java_bytecode/java_bytecode_vtable.cpp
@@ -118,7 +118,7 @@ class java_bytecode_vtable_factoryt
     struct_typet::componentt entry_component;
     entry_component.set_name(ifc_name);
     entry_component.set_base_name(ifc_method->get_base_name());
-    entry_component.type()=pointer_typet(implementation.type());
+    entry_component.type()=pointer_type(implementation.type());
     vtable_type.components().push_back(entry_component);
 
     const irep_idt &impl_name(implementation.get_name());
@@ -288,7 +288,7 @@ static void add_vtable_pointer_member(
 {
   struct_typet::componentt comp;
 
-  comp.type()=pointer_typet(symbol_typet(vt_name));
+  comp.type()=pointer_type(symbol_typet(vt_name));
   comp.set_name(ID_vtable_pointer);
   comp.set_base_name(ID_vtable_pointer);
   comp.set_pretty_name(ID_vtable_pointer);
@@ -391,7 +391,7 @@ static exprt get_ref(
   if(ID_symbol==type_id)
     return get_ref(address_of_exprt(this_obj), target_type);
   assert(ID_pointer==type_id);
-  const typecast_exprt cast(this_obj, pointer_typet(target_type));
+  const typecast_exprt cast(this_obj, pointer_type(target_type));
   return dereference_exprt(cast, target_type);
 }
 
@@ -436,13 +436,13 @@ exprt make_vtable_function(
   }
 
   const symbol_typet vtable_type(vtnamest::get_type(class_id));
-  const pointer_typet vt_ptr_type(vtable_type);
+  const pointer_typet vt_ptr_type=pointer_type(vtable_type);
   const symbol_typet target_type(class_id);
   const exprt this_ref(get_ref(this_obj, target_type));
   const typet ref_type(this_ref.type());
   const member_exprt vtable_member(this_ref, ID_vtable_pointer, vt_ptr_type);
   const dereference_exprt vtable(vtable_member, vtable_type); // TODO: cast?
-  const pointer_typet func_ptr_type(func.type());
+  const pointer_typet func_ptr_type=pointer_type(func.type());
   const member_exprt func_ptr(vtable, func_name, func_ptr_type);
   const dereference_exprt virtual_func(func_ptr, func.type());
   return virtual_func;
diff --git a/src/java_bytecode/java_entry_point.cpp b/src/java_bytecode/java_entry_point.cpp
index 1cb0a10d701..72414955785 100644
--- a/src/java_bytecode/java_entry_point.cpp
+++ b/src/java_bytecode/java_entry_point.cpp
@@ -556,7 +556,7 @@ bool java_entry_point(
   exc_symbol.is_static_lifetime=false;
   exc_symbol.name=id2string(symbol.name)+EXC_SUFFIX;
   exc_symbol.base_name=id2string(symbol.name)+EXC_SUFFIX;
-  exc_symbol.type=typet(ID_pointer, empty_typet());
+  exc_symbol.type=java_reference_type(empty_typet());
   symbol_table.add(exc_symbol);
 
   exprt::operandst main_arguments=
diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp
index 15d8eac7bc4..a903483aa4c 100644
--- a/src/java_bytecode/java_object_factory.cpp
+++ b/src/java_bytecode/java_object_factory.cpp
@@ -13,7 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/arith_tools.h>
 #include <util/fresh_symbol.h>
-#include <util/std_types.h>
+#include <util/c_types.h>
 #include <util/std_code.h>
 #include <util/std_expr.h>
 #include <util/namespace.h>
@@ -167,7 +167,7 @@ exprt java_object_factoryt::allocate_object(
       // malloc expression
       exprt malloc_expr=side_effect_exprt(ID_malloc);
       malloc_expr.copy_to_operands(object_size);
-      typet result_type=pointer_typet(allocate_type);
+      typet result_type=pointer_type(allocate_type);
       malloc_expr.type()=result_type;
       // Create a symbol for the malloc expression so we can initialize
       // without having to do it potentially through a double-deref, which
@@ -175,7 +175,7 @@ exprt java_object_factoryt::allocate_object(
       symbolt &malloc_sym=new_tmp_symbol(
         symbol_table,
         loc,
-        pointer_typet(allocate_type),
+        pointer_type(allocate_type),
         "malloc_site");
       symbols_created.push_back(&malloc_sym);
       code_assignt assign=code_assignt(malloc_sym.symbol_expr(), malloc_expr);
@@ -532,9 +532,9 @@ void java_object_factoryt::gen_nondet_array_init(
   exprt length_expr=member_exprt(deref_expr, "length", comps[1].type());
   exprt init_array_expr=member_exprt(deref_expr, "data", comps[2].type());
 
-  if(init_array_expr.type()!=pointer_typet(element_type))
+  if(init_array_expr.type()!=pointer_type(element_type))
     init_array_expr=
-      typecast_exprt(init_array_expr, pointer_typet(element_type));
+      typecast_exprt(init_array_expr, pointer_type(element_type));
 
   // Interpose a new symbol, as the goto-symex stage can't handle array indexing
   // via a cast.
diff --git a/src/jsil/jsil_internal_additions.cpp b/src/jsil/jsil_internal_additions.cpp
index 446910062d7..af963454e25 100644
--- a/src/jsil/jsil_internal_additions.cpp
+++ b/src/jsil/jsil_internal_additions.cpp
@@ -43,7 +43,7 @@ void jsil_internal_additions(symbol_tablet &dest)
     symbolt symbol;
     symbol.base_name="__CPROVER_malloc_object";
     symbol.name=CPROVER_PREFIX "malloc_object";
-    symbol.type=pointer_typet(empty_typet());
+    symbol.type=pointer_type(empty_typet());
     symbol.mode=ID_C;
     symbol.is_lvalue=true;
     symbol.is_state_var=true;
diff --git a/src/path-symex/path_symex.cpp b/src/path-symex/path_symex.cpp
index c5004e51d55..f64071ec617 100644
--- a/src/path-symex/path_symex.cpp
+++ b/src/path-symex/path_symex.cpp
@@ -249,7 +249,7 @@ void path_symext::symex_malloc(
 
   if(object_type.id()==ID_array)
   {
-    rhs.type()=pointer_typet(value_symbol.type.subtype());
+    rhs.type()=pointer_type(value_symbol.type.subtype());
     index_exprt index_expr(value_symbol.type.subtype());
     index_expr.array()=value_symbol.symbol_expr();
     index_expr.index()=from_integer(0, index_type());
@@ -258,7 +258,7 @@ void path_symext::symex_malloc(
   else
   {
     rhs.op0()=value_symbol.symbol_expr();
-    rhs.type()=pointer_typet(value_symbol.type);
+    rhs.type()=pointer_type(value_symbol.type);
   }
 
   if(rhs.type()!=lhs.type())
diff --git a/src/pointer-analysis/dereference.cpp b/src/pointer-analysis/dereference.cpp
index 5063278d4c9..aaf33ca18de 100644
--- a/src/pointer-analysis/dereference.cpp
+++ b/src/pointer-analysis/dereference.cpp
@@ -275,7 +275,7 @@ exprt dereferencet::dereference_typecast(
         plus_exprt(offset, typecast_exprt(op, offset.type()));
 
     exprt new_typecast=
-      typecast_exprt(integer, pointer_typet(type));
+      typecast_exprt(integer, pointer_type(type));
 
     return dereference_exprt(new_typecast, type);
   }
diff --git a/src/solvers/smt1/smt1_conv.cpp b/src/solvers/smt1/smt1_conv.cpp
index 65f55640400..ee85dfc63a0 100644
--- a/src/solvers/smt1/smt1_conv.cpp
+++ b/src/solvers/smt1/smt1_conv.cpp
@@ -21,6 +21,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/base_type.h>
 #include <util/ieee_float.h>
 #include <util/byte_operators.h>
+#include <util/c_types.h>
 
 #include <ansi-c/string_constant.h>
 
@@ -286,12 +287,14 @@ void smt1_convt::convert_address_of_rec(
       exprt new_index_expr=expr;
       new_index_expr.op1()=from_integer(0, index.type());
 
-      exprt address_of_expr(ID_address_of, pointer_typet());
-      address_of_expr.type().subtype()=array.type().subtype();
-      address_of_expr.copy_to_operands(new_index_expr);
+      address_of_exprt address_of_expr(
+        new_index_expr,
+        pointer_type(array.type().subtype()));
 
-      exprt plus_expr(ID_plus, address_of_expr.type());
-      plus_expr.copy_to_operands(address_of_expr, index);
+      plus_exprt plus_expr(
+        address_of_expr,
+        index,
+        address_of_expr.type());
 
       convert_expr(plus_expr, true);
     }
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index d6198ebea5f..ccf6087379f 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/src/solvers/smt2/smt2_conv.cpp
@@ -14,15 +14,16 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <cassert>
 
 #include <util/arith_tools.h>
+#include <util/base_type.h>
+#include <util/c_types.h>
 #include <util/expr_util.h>
-#include <util/std_types.h>
-#include <util/std_expr.h>
 #include <util/fixedbv.h>
-#include <util/pointer_offset_size.h>
 #include <util/ieee_float.h>
-#include <util/base_type.h>
-#include <util/string2int.h>
 #include <util/invariant.h>
+#include <util/pointer_offset_size.h>
+#include <util/std_types.h>
+#include <util/std_expr.h>
+#include <util/string2int.h>
 
 #include <ansi-c/string_constant.h>
 
@@ -512,12 +513,14 @@ void smt2_convt::convert_address_of_rec(
       exprt new_index_expr=expr;
       new_index_expr.op1()=from_integer(0, index.type());
 
-      exprt address_of_expr(ID_address_of, pointer_typet());
-      address_of_expr.type().subtype()=array.type().subtype();
-      address_of_expr.copy_to_operands(new_index_expr);
+      address_of_exprt address_of_expr(
+        new_index_expr,
+        pointer_type(array.type().subtype()));
 
-      exprt plus_expr(ID_plus, address_of_expr.type());
-      plus_expr.copy_to_operands(address_of_expr, index);
+      plus_exprt plus_expr(
+        address_of_expr,
+        index,
+        address_of_expr.type());
 
       convert_expr(plus_expr);
     }
diff --git a/src/util/std_expr.cpp b/src/util/std_expr.cpp
index 6fc3de230d2..cef9446e2e1 100644
--- a/src/util/std_expr.cpp
+++ b/src/util/std_expr.cpp
@@ -13,10 +13,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "arith_tools.h"
 #include "byte_operators.h"
 #include "c_types.h"
-#include "config.h"
 #include "namespace.h"
 #include "pointer_offset_size.h"
-
 #include "std_types.h"
 
 bool constant_exprt::value_is_zero_string() const
@@ -171,3 +169,20 @@ extractbits_exprt::extractbits_exprt(
   upper()=constant_exprt::integer_constant(_upper);
   lower()=constant_exprt::integer_constant(_lower);
 }
+
+/*******************************************************************\
+
+Function: address_of_exprt::address_of_exprt
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+address_of_exprt::address_of_exprt(const exprt &_op):
+  unary_exprt(ID_address_of, _op, pointer_type(_op.type()))
+{
+}
diff --git a/src/util/std_expr.h b/src/util/std_expr.h
index e2ed2ad433d..c4837be001a 100644
--- a/src/util/std_expr.h
+++ b/src/util/std_expr.h
@@ -2590,19 +2590,19 @@ inline extractbits_exprt &to_extractbits_expr(exprt &expr)
 
 /*! \brief Operator to return the address of an object
 */
-class address_of_exprt:public exprt
+class address_of_exprt:public unary_exprt
 {
 public:
-  explicit address_of_exprt(const exprt &op):
-    exprt(ID_address_of, pointer_typet(op.type()))
+  explicit address_of_exprt(const exprt &op);
+
+  address_of_exprt(const exprt &op, const pointer_typet &_type):
+    unary_exprt(ID_address_of, op, _type)
   {
-    copy_to_operands(op);
   }
 
   address_of_exprt():
-    exprt(ID_address_of, pointer_typet())
+    unary_exprt(ID_address_of, pointer_typet())
   {
-    operands().resize(1);
   }
 
   exprt &object()