diff --git a/src/ansi-c/type2name.cpp b/src/ansi-c/type2name.cpp
index edc5c51f87b..0a49ae57e77 100644
--- a/src/ansi-c/type2name.cpp
+++ b/src/ansi-c/type2name.cpp
@@ -134,9 +134,12 @@ static std::string type2name(
   else if(type.id()==ID_natural)
     result+='N';
   else if(type.id()==ID_pointer)
-    result+='*';
-  else if(type.id()==ID_reference)
-    result+='&';
+  {
+    if(type.get_bool(ID_C_reference))
+      result+='&';
+    else
+      result+='*';
+  }
   else if(type.id()==ID_code)
   {
     const code_typet &t=to_code_type(type);
diff --git a/src/jsil/jsil_typecheck.cpp b/src/jsil/jsil_typecheck.cpp
index c7a8dd97acc..a91eaf36f6f 100644
--- a/src/jsil/jsil_typecheck.cpp
+++ b/src/jsil/jsil_typecheck.cpp
@@ -179,7 +179,7 @@ void jsil_typecheckt::typecheck_expr_main(exprt &expr)
             expr.id()=="builtin_object" ||
             expr.id()=="user_object" ||
             expr.id()=="object" ||
-            expr.id()==ID_reference ||
+            expr.id()==ID_pointer ||
             expr.id()==ID_member ||
             expr.id()=="variable")
       expr.type()=jsil_kind();
diff --git a/src/jsil/parser.y b/src/jsil/parser.y
index 41aba1315ae..2823337d76f 100644
--- a/src/jsil/parser.y
+++ b/src/jsil/parser.y
@@ -614,7 +614,8 @@ jsil_type: TOK_T_NULL
          | ref_type
          | TOK_T_REFERENCE
          {
-           newstack($$).id(ID_reference);
+           newstack($$).id(ID_pointer);
+           newstack($$).set(ID_C_reference, true);
          }
          ;
 
diff --git a/src/solvers/cvc/cvc_conv.cpp b/src/solvers/cvc/cvc_conv.cpp
index 356a9af1fd4..c9f2ecb0211 100644
--- a/src/solvers/cvc/cvc_conv.cpp
+++ b/src/solvers/cvc/cvc_conv.cpp
@@ -1308,8 +1308,7 @@ void cvc_convt::convert_type(const typet &type)
 
     out << " #]";
   }
-  else if(type.id()==ID_pointer ||
-          type.id()==ID_reference)
+  else if(type.id()==ID_pointer)
   {
     out << cvc_pointer_type();
   }
diff --git a/src/solvers/flattening/boolbv_width.cpp b/src/solvers/flattening/boolbv_width.cpp
index a61be58ad7f..4c2bd1c86c2 100644
--- a/src/solvers/flattening/boolbv_width.cpp
+++ b/src/solvers/flattening/boolbv_width.cpp
@@ -193,8 +193,7 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
   {
     // no width
   }
-  else if(type_id==ID_pointer ||
-          type_id==ID_reference)
+  else if(type_id==ID_pointer)
   {
     entry.total_width=config.ansi_c.pointer_width;
   }
diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp
index d0c61e8ae86..85ec254a0e6 100644
--- a/src/solvers/flattening/bv_pointers.cpp
+++ b/src/solvers/flattening/bv_pointers.cpp
@@ -26,7 +26,7 @@ literalt bv_pointerst::convert_rest(const exprt &expr)
   if(expr.id()==ID_invalid_pointer)
   {
     if(operands.size()==1 &&
-       is_ptr(operands[0].type()))
+       operands[0].type().id()==ID_pointer)
     {
       const bvt &bv=convert_bv(operands[0]);
 
@@ -58,7 +58,7 @@ literalt bv_pointerst::convert_rest(const exprt &expr)
   else if(expr.id()==ID_dynamic_object)
   {
     if(operands.size()==1 &&
-       is_ptr(operands[0].type()))
+       operands[0].type().id()==ID_pointer)
     {
       // we postpone
       literalt l=prop.new_variable();
@@ -75,8 +75,8 @@ literalt bv_pointerst::convert_rest(const exprt &expr)
           expr.id()==ID_gt || expr.id()==ID_ge)
   {
     if(operands.size()==2 &&
-       is_ptr(operands[0].type()) &&
-       is_ptr(operands[1].type()))
+       operands[0].type().id()==ID_pointer &&
+       operands[1].type().id()==ID_pointer)
     {
       const bvt &bv0=convert_bv(operands[0]);
       const bvt &bv1=convert_bv(operands[1]);
@@ -216,7 +216,7 @@ bool bv_pointerst::convert_address_of_rec(
 
 bvt bv_pointerst::convert_pointer_type(const exprt &expr)
 {
-  if(!is_ptr(expr.type()))
+  if(expr.type().id()!=ID_pointer)
     throw "convert_pointer_type got non-pointer type";
 
   // make sure the config hasn't been changed
@@ -444,7 +444,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
 
 bvt bv_pointerst::convert_bitvector(const exprt &expr)
 {
-  if(is_ptr(expr.type()))
+  if(expr.type().id()==ID_pointer)
     return convert_pointer_type(expr);
 
   if(expr.id()==ID_minus &&
@@ -483,7 +483,7 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
   }
   else if(expr.id()==ID_pointer_offset &&
           expr.operands().size()==1 &&
-          is_ptr(expr.op0().type()))
+          expr.op0().type().id()==ID_pointer)
   {
     bvt op0=convert_bv(expr.op0());
 
@@ -500,7 +500,7 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
   }
   else if(expr.id()==ID_object_size &&
           expr.operands().size()==1 &&
-          is_ptr(expr.op0().type()))
+          expr.op0().type().id()==ID_pointer)
   {
     // we postpone until we know the objects
     std::size_t width=boolbv_width(expr.type());
@@ -521,7 +521,7 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
   }
   else if(expr.id()==ID_pointer_object &&
           expr.operands().size()==1 &&
-          is_ptr(expr.op0().type()))
+          expr.op0().type().id()==ID_pointer)
   {
     bvt op0=convert_bv(expr.op0());
 
@@ -562,7 +562,7 @@ exprt bv_pointerst::bv_get_rec(
   std::size_t offset,
   const typet &type) const
 {
-  if(!is_ptr(type))
+  if(type.id()!=ID_pointer)
     return SUB::bv_get_rec(bv, unknown, offset, type);
 
   std::string value_addr, value_offset, value;
@@ -605,7 +605,7 @@ exprt bv_pointerst::bv_get_rec(
 
   // we add the elaborated expression as operand
   result.copy_to_operands(
-    pointer_logic.pointer_expr(pointer, type));
+    pointer_logic.pointer_expr(pointer, to_pointer_type(type)));
 
   return result;
 }
diff --git a/src/solvers/flattening/bv_pointers.h b/src/solvers/flattening/bv_pointers.h
index 34a2a61af5a..cd0cc8166ef 100644
--- a/src/solvers/flattening/bv_pointers.h
+++ b/src/solvers/flattening/bv_pointers.h
@@ -64,11 +64,6 @@ class bv_pointerst:public boolbvt
   postponed_listt postponed_list;
 
   void do_postponed(const postponedt &postponed);
-
-  static bool is_ptr(const typet &type)
-  {
-    return type.id()==ID_pointer || type.id()==ID_reference;
-  }
 };
 
 #endif // CPROVER_SOLVERS_FLATTENING_BV_POINTERS_H
diff --git a/src/solvers/flattening/pointer_logic.cpp b/src/solvers/flattening/pointer_logic.cpp
index 1018dfca2b7..63a2c809b5d 100644
--- a/src/solvers/flattening/pointer_logic.cpp
+++ b/src/solvers/flattening/pointer_logic.cpp
@@ -65,7 +65,7 @@ std::size_t pointer_logict::add_object(const exprt &expr)
 
 exprt pointer_logict::pointer_expr(
   std::size_t object,
-  const typet &type) const
+  const pointer_typet &type) const
 {
   pointert pointer(object, 0);
   return pointer_expr(pointer, type);
@@ -73,7 +73,7 @@ exprt pointer_logict::pointer_expr(
 
 exprt pointer_logict::pointer_expr(
   const pointert &pointer,
-  const typet &type) const
+  const pointer_typet &type) const
 {
   if(pointer.object==null_object) // NULL?
   {
@@ -109,17 +109,7 @@ exprt pointer_logict::pointer_expr(
 
   exprt deep_object=object_rec(pointer.offset, type, object_expr);
 
-  exprt result;
-
-  if(type.id()==ID_pointer)
-    result=exprt(ID_address_of, type);
-  else if(type.id()==ID_reference)
-    result=exprt("reference_to", type);
-  else
-    assert(0);
-
-  result.copy_to_operands(deep_object);
-  return result;
+  return address_of_exprt(deep_object, type);
 }
 
 exprt pointer_logict::object_rec(
diff --git a/src/solvers/flattening/pointer_logic.h b/src/solvers/flattening/pointer_logic.h
index d094dbd8523..f1b791a7fd1 100644
--- a/src/solvers/flattening/pointer_logic.h
+++ b/src/solvers/flattening/pointer_logic.h
@@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/numbering.h>
 
 class namespacet;
+class pointer_typet;
 
 class pointer_logict
 {
@@ -42,12 +43,12 @@ class pointer_logict
   // converts an (object,offset) pair to an expression
   exprt pointer_expr(
     const pointert &pointer,
-    const typet &type) const;
+    const pointer_typet &type) const;
 
   // converts an (object,0) pair to an expression
   exprt pointer_expr(
     std::size_t object,
-    const typet &type) const;
+    const pointer_typet &type) const;
 
   ~pointer_logict();
   explicit pointer_logict(const namespacet &_ns);
diff --git a/src/solvers/smt1/smt1_conv.cpp b/src/solvers/smt1/smt1_conv.cpp
index 1a5553370f8..d1ab4e6fbfc 100644
--- a/src/solvers/smt1/smt1_conv.cpp
+++ b/src/solvers/smt1/smt1_conv.cpp
@@ -160,7 +160,8 @@ exprt smt1_convt::ce_value(
       binary2integer(
         value.substr(config.bv_encoding.object_bits, std::string::npos), true);
 
-    result.copy_to_operands(pointer_logic.pointer_expr(p, type));
+    result.copy_to_operands(
+      pointer_logic.pointer_expr(p, to_pointer_type(type)));
 
     return result;
   }
@@ -2946,13 +2947,12 @@ void smt1_convt::convert_type(const typet &type)
 
     out << "BitVec[" << width << "]";
   }
-  else if(type.id()==ID_pointer ||
-          type.id()==ID_reference)
+  else if(type.id()==ID_pointer)
   {
     std::size_t width=boolbv_width(type);
 
     if(width==0)
-      throw "failed to get width of pointer/reference";
+      throw "failed to get width of pointer";
 
     out << "BitVec[" << width << "]";
   }
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index 745f6e57826..23e06f37c48 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/src/solvers/smt2/smt2_conv.cpp
@@ -460,7 +460,7 @@ exprt smt2_convt::parse_rec(const irept &src, const typet &_type)
     pointer_logict::pointert ptr;
     ptr.object=integer2size_t(v/pow);
     ptr.offset=v%pow;
-    return pointer_logic.pointer_expr(ptr, type);
+    return pointer_logic.pointer_expr(ptr, to_pointer_type(type));
   }
   else if(type.id()==ID_struct)
   {
@@ -4167,8 +4167,7 @@ void smt2_convt::find_symbols(const exprt &expr)
   {
     const exprt &op = expr.op0();
 
-    if(op.type().id()==ID_pointer ||
-       op.type().id()==ID_reference)
+    if(op.type().id()==ID_pointer)
     {
       if(object_sizes.find(expr)==object_sizes.end())
       {
@@ -4344,8 +4343,7 @@ void smt2_convt::convert_type(const typet &type)
 
     out << "(_ BitVec " << width << ")";
   }
-  else if(type.id()==ID_pointer ||
-          type.id()==ID_reference)
+  else if(type.id()==ID_pointer)
   {
     out << "(_ BitVec "
         << boolbv_width(type) << ")";
diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def
index 1f97b519ac9..e5e998633c0 100644
--- a/src/util/irep_ids.def
+++ b/src/util/irep_ids.def
@@ -197,7 +197,6 @@ IREP_ID_ONE(forever)
 IREP_ID_ONE(repeat)
 IREP_ID_ONE(extractbit)
 IREP_ID_ONE(extractbits)
-IREP_ID_ONE(reference)
 IREP_ID_TWO(C_reference, #reference)
 IREP_ID_TWO(C_rvalue_reference, #rvalue_reference)
 IREP_ID_ONE(true)