diff --git a/src/pointer-analysis/dereference.cpp b/src/pointer-analysis/dereference.cpp
index aaf33ca18de..4aad728ecd3 100644
--- a/src/pointer-analysis/dereference.cpp
+++ b/src/pointer-analysis/dereference.cpp
@@ -264,9 +264,9 @@ exprt dereferencet::dereference_typecast(
     return dereference_rec(op, offset, type); // just pass down
   else if(op_type.id()==ID_signedbv || op_type.id()==ID_unsignedbv)
   {
-    // We got an integer-typed address A. We turn this back (!)
-    // into *(type *)(A+offset), and then let some other layer
-    // worry about it.
+    // We got an integer-typed address A. We turn this
+    // into integer_dereference(A+offset),
+    // and then let some other layer worry about it.
 
     exprt integer=op;
 
@@ -274,10 +274,7 @@ exprt dereferencet::dereference_typecast(
       integer=
         plus_exprt(offset, typecast_exprt(op, offset.type()));
 
-    exprt new_typecast=
-      typecast_exprt(integer, pointer_type(type));
-
-    return dereference_exprt(new_typecast, type);
+    return unary_exprt(ID_integer_dereference, integer, type);
   }
   else
     throw "dereferencet: unexpected cast";
diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def
index fca18c8693b..30e7b73a1a1 100644
--- a/src/util/irep_ids.def
+++ b/src/util/irep_ids.def
@@ -823,6 +823,7 @@ IREP_ID_ONE(array_replace)
 IREP_ID_ONE(switch_case_number)
 IREP_ID_ONE(java_array_access)
 IREP_ID_ONE(java_member_access)
+IREP_ID_ONE(integer_dereference)
 
 #undef IREP_ID_ONE
 #undef IREP_ID_TWO