diff --git a/src/col/vct/col/ast/Node.scala b/src/col/vct/col/ast/Node.scala
index 637dc32d4..ccd8065e6 100644
--- a/src/col/vct/col/ast/Node.scala
+++ b/src/col/vct/col/ast/Node.scala
@@ -1409,6 +1409,10 @@ final case class DerefPointer[G](pointer: Expr[G])(
     val blame: Blame[PointerDerefError]
 )(implicit val o: Origin)
     extends Expr[G] with DerefPointerImpl[G]
+final case class DerefPointerTyped[G](pointer: Expr[G], elementType: Type[G])(
+    val blame: Blame[PointerDerefError]
+)(implicit val o: Origin)
+    extends Expr[G] with DerefPointerTypedImpl[G]
 final case class RawDerefPointer[G](pointer: Expr[G])(
     val blame: Blame[PointerDerefError]
 )(implicit val o: Origin)
@@ -1766,6 +1770,11 @@ final case class PointerLocation[G](pointer: Expr[G])(
     val blame: Blame[PointerLocationError]
 )(implicit val o: Origin)
     extends Location[G] with PointerLocationImpl[G]
+final case class TypedPointerLocation[G](
+    pointer: Expr[G],
+    pointerType: Type[G],
+)(val blame: Blame[PointerLocationError])(implicit val o: Origin)
+    extends Location[G] with TypedPointerLocationImpl[G]
 final case class ByValueClassLocation[G](expr: Expr[G])(
     val blame: Blame[PointerLocationError]
 )(implicit val o: Origin)
diff --git a/src/col/vct/col/ast/expr/heap/read/DerefPointerTypedImpl.scala b/src/col/vct/col/ast/expr/heap/read/DerefPointerTypedImpl.scala
new file mode 100644
index 000000000..52f90dd39
--- /dev/null
+++ b/src/col/vct/col/ast/expr/heap/read/DerefPointerTypedImpl.scala
@@ -0,0 +1,13 @@
+package vct.col.ast.expr.heap.read
+
+import vct.col.ast.ops.DerefPointerTypedOps
+import vct.col.ast.{DerefPointerTyped, Type}
+import vct.col.print._
+
+trait DerefPointerTypedImpl[G] extends DerefPointerTypedOps[G] {
+  this: DerefPointerTyped[G] =>
+  override def t: Type[G] = elementType
+
+  override def precedence: Int = Precedence.PREFIX
+  override def layout(implicit ctx: Ctx): Doc = Text("*") <> assoc(pointer)
+}
diff --git a/src/col/vct/col/ast/family/location/TypedPointerLocationImpl.scala b/src/col/vct/col/ast/family/location/TypedPointerLocationImpl.scala
new file mode 100644
index 000000000..51a885156
--- /dev/null
+++ b/src/col/vct/col/ast/family/location/TypedPointerLocationImpl.scala
@@ -0,0 +1,11 @@
+package vct.col.ast.family.location
+
+import vct.col.ast.TypedPointerLocation
+import vct.col.ast.ops.TypedPointerLocationOps
+import vct.col.print.{Ctx, Doc, Text}
+
+trait TypedPointerLocationImpl[G] extends TypedPointerLocationOps[G] {
+  this: TypedPointerLocation[G] =>
+  override def layout(implicit ctx: Ctx): Doc =
+    Text("(") <> pointerType <> ")" <> pointer
+}
diff --git a/src/col/vct/col/typerules/CoercingRewriter.scala b/src/col/vct/col/typerules/CoercingRewriter.scala
index 3920a1159..d21421e38 100644
--- a/src/col/vct/col/typerules/CoercingRewriter.scala
+++ b/src/col/vct/col/typerules/CoercingRewriter.scala
@@ -1261,6 +1261,8 @@ abstract class CoercingRewriter[Pre <: Generation]()
       case deref @ Deref(obj, ref) => Deref(cls(obj), ref)(deref.blame)
       case deref @ DerefHeapVariable(ref) => DerefHeapVariable(ref)(deref.blame)
       case deref @ DerefPointer(p) => DerefPointer(pointer(p)._1)(deref.blame)
+      case deref @ DerefPointerTyped(p, t) =>
+        DerefPointerTyped(pointer(p)._1, t)(deref.blame)
       case deref @ RawDerefPointer(p) =>
         RawDerefPointer(pointer(p)._1)(deref.blame)
       case Drop(xs, count) => Drop(seq(xs)._1, int(count))
@@ -2713,6 +2715,8 @@ abstract class CoercingRewriter[Pre <: Generation]()
         ArrayLocation(array(arrayObj)._1, int(subscript))(a.blame)
       case p @ PointerLocation(pointerExp) =>
         PointerLocation(pointer(pointerExp)._1)(p.blame)
+      case p @ TypedPointerLocation(pointerExp, pointerType) =>
+        TypedPointerLocation(pointer(pointerExp)._1, pointerType)(p.blame)
       case ByValueClassLocation(expr) => node
       case PredicateLocation(inv) => PredicateLocation(inv)
       case al @ AmbiguousLocation(expr) => AmbiguousLocation(expr)(al.blame)
diff --git a/src/rewrite/vct/rewrite/ClassToRef.scala b/src/rewrite/vct/rewrite/ClassToRef.scala
index c7f48ef2b..2aa56ae63 100644
--- a/src/rewrite/vct/rewrite/ClassToRef.scala
+++ b/src/rewrite/vct/rewrite/ClassToRef.scala
@@ -5,6 +5,7 @@ import vct.col.origin._
 import vct.result.VerificationError
 import vct.col.util.AstBuildHelpers._
 import hre.util.ScopedStack
+import vct.col.print.Ctx
 import vct.col.rewrite.error.{ExcludedByPassOrder, ExtraNode}
 import vct.col.ref.Ref
 import vct.col.resolve.ctx.Referrable
@@ -55,6 +56,8 @@ case class ClassToRef[Pre <: Generation]() extends Rewriter[Pre] {
   private def This: Origin =
     Origin(Seq(PreferredName(Seq("this")), LabelContext("classToRef")))
 
+  private var namingContext: Ctx = null
+
   val byRefFieldSucc: SuccessionMap[Field[Pre], SilverField[Post]] =
     SuccessionMap()
   val byValFieldSucc: SuccessionMap[Field[Pre], ADTFunction[Post]] =
@@ -85,8 +88,11 @@ case class ClassToRef[Pre <: Generation]() extends Rewriter[Pre] {
   val valueAsFunctions: mutable.Map[Type[Pre], ADTFunction[Post]] = mutable
     .Map()
 
-  val castHelpers: SuccessionMap[Type[Pre], Procedure[Post]] = SuccessionMap()
-  val requiredCastHelpers: ScopedStack[mutable.Set[Type[Pre]]] = ScopedStack()
+  val castHelpers: SuccessionMap[(Type[Post], Type[Pre]), Procedure[Post]] =
+    SuccessionMap()
+  val requiredCastHelpers
+      : ScopedStack[mutable.Set[(Expr[Post], Type[Pre], Type[Pre])]] =
+    ScopedStack()
 
   def typeNumber(cls: Class[Pre]): Int =
     typeNumberStore.getOrElseUpdate(cls, typeNumberStore.size + 1)
@@ -194,9 +200,10 @@ case class ClassToRef[Pre <: Generation]() extends Rewriter[Pre] {
       axiomType,
       body = { a =>
         InlinePattern(adtFunctionInvocation[Post](
-          valueAsFunctions
-            .getOrElseUpdate(oldT, makeValueAsFunction(oldT.toString, newT))
-            .ref,
+          valueAsFunctions.getOrElseUpdate(
+            oldT,
+            makeValueAsFunction(oldT.toStringWithContext(namingContext), newT),
+          ).ref,
           typeArgs = Some((valueAdt.ref(()), Seq(axiomType))),
           args = Seq(a),
         )) === Cast(
@@ -207,7 +214,8 @@ case class ClassToRef[Pre <: Generation]() extends Rewriter[Pre] {
     ))
   }
 
-  override def dispatch(program: Program[Pre]): Program[Rewritten[Pre]] =
+  override def dispatch(program: Program[Pre]): Program[Rewritten[Pre]] = {
+    namingContext = Ctx().namesIn(program)
     program.rewrite(declarations =
       globalDeclarations.collect {
         program.declarations.foreach(dispatch)
@@ -220,6 +228,7 @@ case class ClassToRef[Pre <: Generation]() extends Rewriter[Pre] {
         }
       }._1
     )
+  }
 
   override def dispatch(decl: Declaration[Pre]): Unit =
     decl match {
@@ -396,7 +405,10 @@ case class ClassToRef[Pre <: Generation]() extends Rewriter[Pre] {
                         InlinePattern(adtFunctionInvocation[Post](
                           valueAsFunctions.getOrElseUpdate(
                             field.t,
-                            makeValueAsFunction(field.t.toString, newT),
+                            makeValueAsFunction(
+                              field.t.toStringWithContext(namingContext),
+                              newT,
+                            ),
                           ).ref,
                           typeArgs = Some((valueAdt.ref(()), Seq(axiomType))),
                           args = Seq(a),
@@ -577,15 +589,15 @@ case class ClassToRef[Pre <: Generation]() extends Rewriter[Pre] {
 
   private def addCastConstraints(
       expr: Expr[Pre],
-      totalHelpers: mutable.Set[Type[Pre]],
+      totalHelpers: mutable.Set[(Expr[Post], Type[Pre], Type[Pre])],
   ): Expr[Post] = {
-    val helpers: mutable.Set[Type[Pre]] = mutable.Set()
+    val helpers: mutable.Set[(Expr[Post], Type[Pre], Type[Pre])] = mutable.Set()
     var result: Seq[Expr[Post]] = Nil
     for (clause <- expr.unfoldStar) {
       val newClause = requiredCastHelpers.having(helpers) { dispatch(clause) }
       if (helpers.nonEmpty) {
-        result ++= helpers.map { t =>
-          unwrapCastConstraints(dispatch(t), t)(CastHelperOrigin)
+        result ++= helpers.map { case (e, t, _) =>
+          unwrapCastConstraints(dispatch(t), t, e)(CastHelperOrigin)
         }.toSeq
         totalHelpers.addAll(helpers)
         helpers.clear()
@@ -597,7 +609,7 @@ case class ClassToRef[Pre <: Generation]() extends Rewriter[Pre] {
 
   // For loops add cast helpers before and as an invariant (since otherwise the contract might not be well-formed)
   override def dispatch(node: LoopContract[Pre]): LoopContract[Post] = {
-    val helpers: mutable.Set[Type[Pre]] = mutable.Set()
+    val helpers: mutable.Set[(Expr[Post], Type[Pre], Type[Pre])] = mutable.Set()
     node match {
       case inv @ LoopInvariant(invariant, decreases) => {
         val result =
@@ -631,7 +643,7 @@ case class ClassToRef[Pre <: Generation]() extends Rewriter[Pre] {
   }
 
   override def dispatch(stat: Statement[Pre]): Statement[Post] = {
-    val helpers: mutable.Set[Type[Pre]] = mutable.Set()
+    val helpers: mutable.Set[(Expr[Post], Type[Pre], Type[Pre])] = mutable.Set()
     val result =
       requiredCastHelpers.having(helpers) {
         stat match {
@@ -685,15 +697,36 @@ case class ClassToRef[Pre <: Generation]() extends Rewriter[Pre] {
       }
 
     if (helpers.nonEmpty) {
-      Block(helpers.map { t =>
-        InvokeProcedure[Post](
-          castHelpers.getOrElseUpdate(t, makeCastHelper(t)).ref,
-          Nil,
-          Nil,
-          Nil,
-          Nil,
-          Nil,
-        )(TrueSatisfiable)(CastHelperOrigin)
+      // TODO: Branch/match here!
+      Block(helpers.map { case (ptr, t, oldPtrT) =>
+        ptr.t match {
+          case pt: TPointer[Post] =>
+            Branch(Seq((
+              Neq(ptr, Null()(stat.o))(stat.o),
+              InvokeProcedure[Post](
+                castHelpers
+                  .getOrElseUpdate((ptr.t, t), makeCastHelper(t, oldPtrT)).ref,
+                Seq(Cast(ptr, TypeValue(TNonNullPointer(pt.element))(stat.o))(
+                  stat.o
+                )),
+                Nil,
+                Nil,
+                Nil,
+                Nil,
+              )(TrueSatisfiable)(CastHelperOrigin),
+            )))(stat.o)
+          case _: TNonNullPointer[Post] =>
+            InvokeProcedure[Post](
+              castHelpers
+                .getOrElseUpdate((ptr.t, t), makeCastHelper(t, oldPtrT)).ref,
+              Seq(ptr),
+              Nil,
+              Nil,
+              Nil,
+              Nil,
+            )(TrueSatisfiable)(CastHelperOrigin)
+          case _ => ???
+        }
       }.toSeq :+ result)(stat.o)
     } else { result }
   }
@@ -708,81 +741,96 @@ case class ClassToRef[Pre <: Generation]() extends Rewriter[Pre] {
       case other => other.rewriteDefault()
     }
 
-  private def unwrapCastConstraints(outerType: Type[Post], t: Type[Pre])(
-      implicit o: Origin
-  ): Expr[Post] = {
+  private def unwrapCastConstraints(
+      outerType: Type[Post],
+      t: Type[Pre],
+      ptr: Expr[Post],
+  )(implicit o: Origin): Expr[Post] = {
     val newT = dispatch(t)
-    val constraint =
-      forall[Post](
-        TNonNullPointer(outerType),
-        body = { p =>
-          PolarityDependent(
-            Greater(
-              CurPerm(PointerLocation(p)(PanicBlame(
-                "Referring to a non-null pointer should not cause any verification failures"
-              ))),
-              NoPerm(),
-            ) ==>
-              (InlinePattern(Cast(p, TypeValue(TNonNullPointer(newT)))) ===
-                adtFunctionInvocation(
-                  valueAsFunctions
-                    .getOrElseUpdate(t, makeValueAsFunction(t.toString, newT))
-                    .ref,
-                  typeArgs = Some((valueAdt.ref(()), Seq(outerType))),
-                  args = Seq(DerefPointer(p)(PanicBlame(
-                    "Pointer deref is safe since the permission is framed"
-                  ))),
-                )),
-            tt,
-          )
-        },
-      ) &* forall[Post](
-        TNonNullPointer(outerType),
-        body = { p =>
-          PolarityDependent(
-            Greater(
-              CurPerm(PointerLocation(p)(PanicBlame(
+    var constraint: Expr[Post] = PolarityDependent(
+      Greater(
+        CurPerm(
+          TypedPointerLocation(ptr, TNonNullPointer(outerType))(PanicBlame(
+            "Referring to a non-null pointer should not cause any verification failures"
+          ))
+        ),
+        NoPerm(),
+      ) ==>
+        (InlinePattern(Cast(ptr, TypeValue(TNonNullPointer(newT)))) ===
+          adtFunctionInvocation(
+            valueAsFunctions.getOrElseUpdate(
+              t,
+              makeValueAsFunction(t.toStringWithContext(namingContext), newT),
+            ).ref,
+            typeArgs = Some((valueAdt.ref(()), Seq(outerType))),
+            args = Seq(DerefPointerTyped(ptr, outerType)(PanicBlame(
+              "Pointer deref is safe since the permission is framed"
+            ))),
+          )),
+      tt,
+    )
+
+    if (newT != outerType) {
+      constraint =
+        constraint &* PolarityDependent(
+          Greater(
+            CurPerm(
+              TypedPointerLocation(ptr, TNonNullPointer(outerType))(PanicBlame(
                 "Referring to a non-null pointer should not cause any verification failures"
-              ))),
-              NoPerm(),
-            ) ==>
-              (InlinePattern(Cast(
-                Cast(p, TypeValue(TNonNullPointer(newT))),
-                TypeValue(TNonNullPointer(outerType)),
-              )) === p),
-            tt,
-          )
-        },
-      )
+              ))
+            ),
+            NoPerm(),
+          ) ==>
+            (InlinePattern(Cast(
+              Cast(ptr, TypeValue(TNonNullPointer(newT))),
+              TypeValue(TNonNullPointer(outerType)),
+            )) === ptr),
+          tt,
+        )
+    }
 
     if (t.isInstanceOf[TByValueClass[Pre]]) {
       constraint &*
         t.asInstanceOf[TByValueClass[Pre]].cls.decl.decls.collectFirst {
           case field: InstanceField[Pre] =>
-            unwrapCastConstraints(outerType, field.t)
+            unwrapCastConstraints(outerType, field.t, ptr)
         }.getOrElse(tt)
     } else { constraint }
   }
 
-  private def makeCastHelper(t: Type[Pre]): Procedure[Post] = {
-    implicit val o: Origin = CastHelperOrigin
-      .where(name = "constraints_" + t.toString)
+  private def makeCastHelper(
+      t: Type[Pre],
+      inType: Type[Pre],
+  ): Procedure[Post] = {
+    implicit val o: Origin = CastHelperOrigin.where(name =
+      "constraints_" + t.toStringWithContext(namingContext) + "_from_" +
+        inType.toStringWithContext(namingContext)
+    )
+    val ptr =
+      new Variable[Post](TNonNullPointer(dispatch(inType)))(
+        o.where(name = "ptr")
+      )
     globalDeclarations.declare(procedure(
       AbstractApplicable,
       TrueSatisfiable,
-      ensures = UnitAccountedPredicate(unwrapCastConstraints(dispatch(t), t)),
+      args = Seq(ptr),
+      ensures = UnitAccountedPredicate(
+        unwrapCastConstraints(dispatch(t), t, ptr.get)
+      ),
     ))
   }
 
   private def addCastHelpers(
       t: Type[Pre],
-      helpers: mutable.Set[Type[Pre]],
+      helpers: mutable.Set[(Expr[Post], Type[Pre], Type[Pre])],
+      ptr: Expr[Post],
+      oldPtrT: Type[Pre],
   ): Unit = {
     t match {
       case cls: TByValueClass[Pre] => {
-        helpers.add(t)
+        helpers.add((ptr, t, oldPtrT))
         cls.cls.decl.decls.collectFirst { case field: InstanceField[Pre] =>
-          addCastHelpers(field.t, helpers)
+          addCastHelpers(field.t, helpers, ptr, oldPtrT)
         }
       }
       case _ =>
@@ -902,13 +950,16 @@ case class ClassToRef[Pre <: Generation]() extends Rewriter[Pre] {
           Nil,
           Nil,
         )(PanicBlame("instanceOf requires nothing"))(e.o)
+      // Is this a pointer cast between two different types:
       case Cast(value, typeValue) if value.t.asPointer.isDefined => {
+        val newValue = dispatch(value)
         // Keep pointer casts and add extra annotations
         if (requiredCastHelpers.nonEmpty) {
-          addCastHelpers(value.t.asPointer.get.element, requiredCastHelpers.top)
+          val element = value.t.asPointer.get.element
+          addCastHelpers(element, requiredCastHelpers.top, newValue, element)
         }
 
-        e.rewriteDefault()
+        Cast(newValue, dispatch(typeValue))(e.o)
       }
       case Cast(value, typeValue) =>
         dispatch(
diff --git a/src/rewrite/vct/rewrite/adt/ImportPointer.scala b/src/rewrite/vct/rewrite/adt/ImportPointer.scala
index 72b843209..7e07549ce 100644
--- a/src/rewrite/vct/rewrite/adt/ImportPointer.scala
+++ b/src/rewrite/vct/rewrite/adt/ImportPointer.scala
@@ -4,6 +4,7 @@ import vct.col.ast._
 import ImportADT.typeText
 import hre.util.ScopedStack
 import vct.col.origin._
+import vct.col.print.Ctx
 import vct.col.ref.Ref
 import vct.col.rewrite.Generation
 import vct.col.util.AstBuildHelpers.{functionInvocation, _}
@@ -20,7 +21,7 @@ case object ImportPointer extends ImportADTBuilder("pointer") {
   )
 
   private val AsTypeOrigin: Origin = Origin(
-    Seq(LabelContext("classToRef, asType function"))
+    Seq(LabelContext("adtPointer, asType function"))
   )
 
   case class PointerNullOptNone(inner: Blame[PointerNull], expr: Expr[_])
@@ -93,6 +94,8 @@ case class ImportPointer[Pre <: Generation](importer: ImportADTImporter)
   val asTypeFunctions: mutable.Map[Type[Pre], Function[Post]] = mutable.Map()
   private val inAxiom: ScopedStack[Unit] = ScopedStack()
 
+  private var namingContext: Ctx = null
+
   private def makeAsTypeFunction(typeName: String): Function[Post] = {
     val value =
       new Variable[Post](TAxiomatic(pointerAdt.ref, Nil))(
@@ -160,6 +163,12 @@ case class ImportPointer[Pre <: Generation](importer: ImportADTImporter)
 
   private def getPointerField(ptr: Expr[Pre]): Ref[Post, SilverField[Post]] = {
     val tElement = dispatch(ptr.t.asPointer.get.element)
+    getPointerField(tElement)
+  }
+
+  private def getPointerField(
+      tElement: Type[Post]
+  ): Ref[Post, SilverField[Post]] = {
     pointerField.getOrElseUpdate(
       tElement, {
         globalDeclarations
@@ -179,6 +188,11 @@ case class ImportPointer[Pre <: Generation](importer: ImportADTImporter)
     }
   }
 
+  override def postCoerce(program: Program[Pre]): Program[Post] = {
+    namingContext = Ctx().namesIn(program)
+    super.postCoerce(program)
+  }
+
   override def applyCoercion(e: => Expr[Post], coercion: Coercion[Pre])(
       implicit o: Origin
   ): Expr[Post] =
@@ -225,7 +239,19 @@ case class ImportPointer[Pre <: Generation](importer: ImportADTImporter)
             )(PanicBlame("ptr_deref requires nothing."))(pointer.o),
           field = getPointerField(pointer),
         )
-      case other => rewriteDefault(other)
+      case loc @ TypedPointerLocation(pointer, pointerType) =>
+        SilverFieldLocation(
+          obj =
+            FunctionInvocation[Post](
+              ref = pointerDeref.ref,
+              args = Seq(unwrapOption(pointer, loc.blame)),
+              typeArgs = Nil,
+              Nil,
+              Nil,
+            )(PanicBlame("ptr_deref requires nothing."))(pointer.o),
+          field = getPointerField(dispatch(pointerType.asPointer.get.element)),
+        )
+      case other => other.rewriteDefault()
     }
   }
 
@@ -284,35 +310,37 @@ case class ImportPointer[Pre <: Generation](importer: ImportADTImporter)
           Nil,
           Nil,
         )(PanicBlame("ptr_deref requires nothing."))
-      case deref @ DerefPointer(pointer) =>
-        FunctionInvocation[Post](
-          ref = pointerDeref.ref,
-          args = Seq(
-            if (
-              inAxiom.isEmpty &&
-              !deref.o.find[LabelContext]
-                .exists(_.label == "classToRef cast helpers")
-            ) {
-              FunctionInvocation[Post](
-                ref = pointerAdd.ref,
-                // Always index with zero, otherwise quantifiers with pointers do not get triggered
-                args = Seq(unwrapOption(pointer, deref.blame), const(0)),
-                typeArgs = Nil,
-                Nil,
-                Nil,
-              )(NoContext(
-                DerefPointerBoundsPreconditionFailed(deref.blame, pointer)
-              ))
-            } else { unwrapOption(pointer, deref.blame) }
-          ),
-          typeArgs = Nil,
-          Nil,
-          Nil,
-        )(PanicBlame("ptr_deref requires nothing."))
+      case deref @ DerefPointer(pointer) => derefWithAdd(pointer, deref.blame)
       case other => dispatch(other)
     }
   }
 
+  private def derefWithAdd(ptr: Expr[Pre], blame: Blame[PointerDerefError])(
+      implicit o: Origin
+  ): Expr[Post] = {
+    FunctionInvocation[Post](
+      ref = pointerDeref.ref,
+      args = Seq(
+        if (
+          inAxiom.isEmpty &&
+          !o.find[LabelContext].exists(_.label == "classToRef cast helpers")
+        ) {
+          FunctionInvocation[Post](
+            ref = pointerAdd.ref,
+            // Always index with zero, otherwise quantifiers with pointers do not get triggered
+            args = Seq(unwrapOption(ptr, blame), const(0)),
+            typeArgs = Nil,
+            Nil,
+            Nil,
+          )(NoContext(DerefPointerBoundsPreconditionFailed(blame, ptr)))
+        } else { unwrapOption(ptr, blame) }
+      ),
+      typeArgs = Nil,
+      Nil,
+      Nil,
+    )(PanicBlame("ptr_deref requires nothing."))
+  }
+
   override def postCoerce(e: Expr[Pre]): Expr[Post] = {
     implicit val o: Origin = e.o
     e match {
@@ -363,58 +391,16 @@ case class ImportPointer[Pre <: Generation](importer: ImportADTImporter)
         }
       case deref @ DerefPointer(pointer) =>
         SilverDeref(
-          obj =
-            FunctionInvocation[Post](
-              ref = pointerDeref.ref,
-              args = Seq(
-                if (
-                  inAxiom.isEmpty &&
-                  !deref.o.find[LabelContext]
-                    .exists(_.label == "classToRef cast helpers")
-                ) {
-                  FunctionInvocation[Post](
-                    ref = pointerAdd.ref,
-                    // Always index with zero, otherwise quantifiers with pointers do not get triggered
-                    args = Seq(unwrapOption(pointer, deref.blame), const(0)),
-                    typeArgs = Nil,
-                    Nil,
-                    Nil,
-                  )(NoContext(
-                    DerefPointerBoundsPreconditionFailed(deref.blame, pointer)
-                  ))
-                } else { unwrapOption(pointer, deref.blame) }
-              ),
-              typeArgs = Nil,
-              Nil,
-              Nil,
-            )(PanicBlame("ptr_deref requires nothing.")),
+          obj = derefWithAdd(pointer, deref.blame),
           field = getPointerField(pointer),
         )(PointerFieldInsufficientPermission(deref.blame, deref))
+      case deref @ DerefPointerTyped(pointer, elementType) =>
+        SilverDeref(
+          obj = derefWithAdd(pointer, deref.blame),
+          field = getPointerField(dispatch(elementType)),
+        )(PointerFieldInsufficientPermission(deref.blame, deref))
       case deref @ RawDerefPointer(pointer) =>
-        FunctionInvocation[Post](
-          ref = pointerDeref.ref,
-          args = Seq(
-            if (
-              inAxiom.isEmpty &&
-              !deref.o.find[LabelContext]
-                .exists(_.label == "classToRef cast helpers")
-            ) {
-              FunctionInvocation[Post](
-                ref = pointerAdd.ref,
-                // Always index with zero, otherwise quantifiers with pointers do not get triggered
-                args = Seq(unwrapOption(pointer, deref.blame), const(0)),
-                typeArgs = Nil,
-                Nil,
-                Nil,
-              )(NoContext(
-                DerefPointerBoundsPreconditionFailed(deref.blame, pointer)
-              ))
-            } else { unwrapOption(pointer, deref.blame) }
-          ),
-          typeArgs = Nil,
-          Nil,
-          Nil,
-        )(PanicBlame("ptr_deref requires nothing."))
+        derefWithAdd(pointer, deref.blame)
       case len @ PointerBlockLength(pointer) =>
         ADTFunctionInvocation[Post](
           typeArgs = Some((blockAdt.ref, Nil)),
@@ -476,10 +462,13 @@ case class ImportPointer[Pre <: Generation](importer: ImportADTImporter)
       preExpr: Expr[Pre],
       postExpr: Expr[Post],
   )(implicit o: Origin): Expr[Post] = {
+    if (preExpr.t.asPointer.get.element == innerType) { return postExpr }
     functionInvocation[Post](
       PanicBlame("as_type requires nothing"),
-      asTypeFunctions
-        .getOrElseUpdate(innerType, makeAsTypeFunction(innerType.toString)).ref,
+      asTypeFunctions.getOrElseUpdate(
+        innerType,
+        makeAsTypeFunction(innerType.toStringWithContext(namingContext)),
+      ).ref,
       Seq(preExpr match {
         case PointerAdd(_, _) => postExpr
         // Don't add ptrAdd in an ADT axiom since we cannot use functions with preconditions there