diff --git a/src/col/vct/col/ast/Node.scala b/src/col/vct/col/ast/Node.scala
index a944e6fa9..273dc1f97 100644
--- a/src/col/vct/col/ast/Node.scala
+++ b/src/col/vct/col/ast/Node.scala
@@ -157,10 +157,10 @@ final case class TPointer[G](element: Type[G], unique: Option[BigInt])(
 final case class TNonNullPointer[G](element: Type[G], unique: Option[BigInt])(
   implicit val o: Origin = DiagnosticOrigin
 ) extends PointerType[G] with TNonNullPointerImpl[G]
-final case class TConstPointer[G](pureElement: Type[G])(
+final case class TConstPointer[G](element: Type[G])(
   implicit val o: Origin = DiagnosticOrigin
 ) extends PointerType[G] with TConstPointerImpl[G]
-final case class TNonNullConstPointer[G](pureElement: Type[G])(
+final case class TNonNullConstPointer[G](element: Type[G])(
   implicit val o: Origin = DiagnosticOrigin
 ) extends PointerType[G] with TNonNullConstPointerImpl[G]
 
@@ -692,7 +692,7 @@ final case class ModelDo[G](
 @family
 sealed trait GlobalDeclaration[G]
     extends Declaration[G] with GlobalDeclarationImpl[G]
-final class HeapVariable[G](val t: Type[G])(implicit val o: Origin)
+final class HeapVariable[G](val t: Type[G], val init: Option[Expr[G]])(implicit val o: Origin)
     extends GlobalDeclaration[G] with HeapVariableImpl[G]
 final class SimplificationRule[G](val axiom: Expr[G])(implicit val o: Origin)
     extends GlobalDeclaration[G] with SimplificationRuleImpl[G]
@@ -1484,6 +1484,8 @@ final case class PointerAdd[G](pointer: Expr[G], offset: Expr[G])(
     extends Expr[G] with PointerAddImpl[G]
 final case class AddrOf[G](e: Expr[G])(implicit val o: Origin)
     extends Expr[G] with AddrOfImpl[G]
+final case class AddrOfConstCast[G](e: Expr[G])(implicit val o: Origin)
+  extends Expr[G] with AddrOfConstCastImpl[G]
 final case class FunctionOf[G](
     binding: Ref[G, Variable[G]],
     vars: Seq[Ref[G, Variable[G]]],
diff --git a/src/col/vct/col/ast/declaration/global/HeapVariableImpl.scala b/src/col/vct/col/ast/declaration/global/HeapVariableImpl.scala
index a61021641..fc6af45ba 100644
--- a/src/col/vct/col/ast/declaration/global/HeapVariableImpl.scala
+++ b/src/col/vct/col/ast/declaration/global/HeapVariableImpl.scala
@@ -6,11 +6,14 @@ import vct.col.ast.ops.HeapVariableOps
 
 trait HeapVariableImpl[G] extends HeapVariableOps[G] {
   this: HeapVariable[G] =>
-  override def layout(implicit ctx: Ctx): Doc =
-    ctx.syntax match {
+  override def layout(implicit ctx: Ctx): Doc = {
+    val decl: Doc = ctx.syntax match {
       case Ctx.C | Ctx.Cuda | Ctx.OpenCL | Ctx.CPP =>
         val (spec, decl) = t.layoutSplitDeclarator
-        spec <+> decl <> ctx.name(this) <> ";"
-      case _ => t.show <+> ctx.name(this) <> ";"
+        spec <+> decl <> ctx.name(this)
+      case _ => t.show <+> ctx.name(this)
+
     }
+    decl <> init.map(i => Text(" = ") <> i).getOrElse(Text("")) <> ";"
+  }
 }
diff --git a/src/col/vct/col/ast/expr/heap/read/AddrOfConstCastImpl.scala b/src/col/vct/col/ast/expr/heap/read/AddrOfConstCastImpl.scala
new file mode 100644
index 000000000..1a28afd8f
--- /dev/null
+++ b/src/col/vct/col/ast/expr/heap/read/AddrOfConstCastImpl.scala
@@ -0,0 +1,11 @@
+package vct.col.ast.expr.heap.read
+
+import vct.col.ast.{AddrOfConstCast, TConst}
+import vct.col.ast.ops.AddrOfConstCastOps
+import vct.col.print._
+
+trait AddrOfConstCastImpl[G] extends AddrOfConstCastOps[G] { this: AddrOfConstCast[G] =>
+  override lazy val t = TConst(e.t)
+
+  override def layout(implicit ctx: Ctx): Doc = Text("constCast(") <> e <> ")"
+}
diff --git a/src/col/vct/col/ast/expr/heap/read/AddrOfImpl.scala b/src/col/vct/col/ast/expr/heap/read/AddrOfImpl.scala
index 3281d5692..5f01ddbd0 100644
--- a/src/col/vct/col/ast/expr/heap/read/AddrOfImpl.scala
+++ b/src/col/vct/col/ast/expr/heap/read/AddrOfImpl.scala
@@ -1,6 +1,6 @@
 package vct.col.ast.expr.heap.read
 
-import vct.col.ast.{AddrOf, TPointer, Type, DerefPointer, AmbiguousSubscript}
+import vct.col.ast.{AddrOf, AddrOfConstCast, TPointer, TConstPointer, Type, DerefPointer, AmbiguousSubscript}
 import vct.col.print._
 import vct.col.ast.ops.AddrOfOps
 
@@ -10,6 +10,7 @@ trait AddrOfImpl[G] extends AddrOfOps[G] {
     e match {
       case DerefPointer(p) => p.t
       case AmbiguousSubscript(p, i) => p.t
+      case AddrOfConstCast(e) => TConstPointer(e.t)
       case _ => TPointer(e.t, None)
     }
   }
diff --git a/src/col/vct/col/ast/type/TConstPointerImpl.scala b/src/col/vct/col/ast/type/TConstPointerImpl.scala
index 5d4573127..5f75e1336 100644
--- a/src/col/vct/col/ast/type/TConstPointerImpl.scala
+++ b/src/col/vct/col/ast/type/TConstPointerImpl.scala
@@ -5,12 +5,11 @@ import vct.col.ast.ops.TConstPointerOps
 import vct.col.print._
 
 trait TConstPointerImpl[G] extends TConstPointerOps[G] { this: TConstPointer[G] =>
-  val element: Type[G] = TConst[G](pureElement)
   val unique: Option[BigInt] = None
 
   val isConst = true
   val isNonNull = false
 
   override def layout(implicit ctx: Ctx): Doc =
-    Text("const_pointer") <> open <> pureElement <> close
+    Text("const_pointer") <> open <> element <> close
 }
diff --git a/src/col/vct/col/ast/type/TNonNullConstPointerImpl.scala b/src/col/vct/col/ast/type/TNonNullConstPointerImpl.scala
index bbf9e9117..9faf3d5f2 100644
--- a/src/col/vct/col/ast/type/TNonNullConstPointerImpl.scala
+++ b/src/col/vct/col/ast/type/TNonNullConstPointerImpl.scala
@@ -5,12 +5,11 @@ import vct.col.ast.ops.TNonNullConstPointerOps
 import vct.col.print._
 
 trait TNonNullConstPointerImpl[G] extends TNonNullConstPointerOps[G] { this: TNonNullConstPointer[G] =>
-  val element: Type[G] = TConst[G](pureElement)
   val unique: Option[BigInt] = None
 
   val isConst = true
   val isNonNull = true
 
   override def layout(implicit ctx: Ctx): Doc =
-    Text("constNonNullPointer") <> open <> pureElement <> close
+    Text("constNonNullPointer") <> open <> element <> close
 }
diff --git a/src/col/vct/col/typerules/CoercingRewriter.scala b/src/col/vct/col/typerules/CoercingRewriter.scala
index 7f3d42443..da60421cd 100644
--- a/src/col/vct/col/typerules/CoercingRewriter.scala
+++ b/src/col/vct/col/typerules/CoercingRewriter.scala
@@ -780,6 +780,7 @@ abstract class CoercingRewriter[Pre <: Generation]()
         ActionApply(action, coerceArgs(args, action.decl))
       case ActionPerm(loc, perm) => ActionPerm(loc, rat(perm))
       case AddrOf(e) => AddrOf(e)
+      case AddrOfConstCast(e) => AddrOfConstCast(e)
       case ADTFunctionInvocation(typeArgs, ref, args) =>
         typeArgs match {
           case Some((adt, typeArgs)) =>
@@ -2415,7 +2416,8 @@ abstract class CoercingRewriter[Pre <: Generation]()
         new CTranslationUnit(unit.declarations)
       case unit: CPPTranslationUnit[Pre] =>
         new CPPTranslationUnit(unit.declarations)
-      case variable: HeapVariable[Pre] => new HeapVariable(variable.t)
+      case variable: HeapVariable[Pre] =>
+        new HeapVariable(variable.t, variable.init.map(i => coerce(i, variable.t)))
       case rule: SimplificationRule[Pre] =>
         new SimplificationRule[Pre](bool(rule.axiom))
       case dataType: AxiomaticDataType[Pre] => dataType
diff --git a/src/rewrite/vct/rewrite/TypeQualifierCoercion.scala b/src/rewrite/vct/rewrite/TypeQualifierCoercion.scala
index 4ed4b7a04..a14f8ed6c 100644
--- a/src/rewrite/vct/rewrite/TypeQualifierCoercion.scala
+++ b/src/rewrite/vct/rewrite/TypeQualifierCoercion.scala
@@ -1,12 +1,14 @@
 package vct.rewrite
 
-import vct.col.ast.{Expr, Type, _}
-import vct.col.origin.Origin
+import vct.col.ast._
+import vct.col.origin.{AbstractApplicable, AssignLocalOk, Origin, PanicBlame, TrueSatisfiable}
 import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder}
 import vct.col.typerules.CoercingRewriter
+import vct.col.util.AstBuildHelpers._
 import vct.result.VerificationError.UserError
 import hre.util.ScopedStack
-import vct.col.ref.{LazyRef, Ref}
+import vct.col.ref.LazyRef
+import vct.col.util.SuccessionMap
 
 import scala.collection.mutable
 
@@ -47,15 +49,18 @@ case object TypeQualifierCoercion extends RewriterBuilder {
   def getUniqueMap[G](t: TClassUnique[G]): Map[InstanceField[G], BigInt] = {
     t.uniqueMap.map {case (ref, unique) => (ref.decl, unique)}.toMap
   }
-
-
 }
 
+/* This rewrite step removes type qualifiers TUnique, TConst and TClassUnique.
+ * Some of them were okay to coerce, thus we the node `UniquePointerCoercion` which the pass
+ * MakeUniqueMethodCopies removes again to make the coercion correct by adding method/function copies
+ */
 case class TypeQualifierCoercion[Pre <: Generation]()
   extends CoercingRewriter[Pre] {
 
   val uniqueClasses: mutable.Map[(Class[Pre], Map[InstanceField[Pre], BigInt]), Class[Post]] = mutable.Map()
   val uniqueField: mutable.Map[(InstanceField[Pre], Map[InstanceField[Pre], BigInt]), InstanceField[Post]] = mutable.Map()
+  private val constGlobalHeapsSucc: SuccessionMap[HeapVariable[Pre], Function[Post]] = SuccessionMap()
 
   def createUniqueClassCopy(original: Class[Pre], pointerInstanceFields: Map[InstanceField[Pre], BigInt]): Class[Post] = {
       globalDeclarations.declare({
@@ -89,6 +94,26 @@ case class TypeQualifierCoercion[Pre <: Generation]()
       })
   }
 
+  override def coerce(decl: Declaration[Pre]): Declaration[Pre] = decl match {
+    // Turn of coercions for a sec, otherwise we cannot use our constGlobalHeapsSucc successfully
+    case h: HeapVariable[Pre] if isConstElement(h.t) => h
+    case other => super.coerce(other)
+  }
+
+  override def postCoerce(d: Declaration[Pre]): Unit = d match {
+    case h: HeapVariable[Pre] if isConstElement(h.t) =>
+      val f = globalDeclarations.declare({
+        function(
+          blame = AbstractApplicable,
+          contractBlame = TrueSatisfiable,
+          returnType = dispatch(h.t),
+          body = h.init.map(dispatch)
+        )(h.o)
+      })
+      constGlobalHeapsSucc(h) = f
+    case other => allScopes.anySucceed(other, other.rewriteDefault())
+  }
+
   override def applyCoercion(e: => Expr[Post], coercion: Coercion[Pre])(
     implicit o: Origin
   ): Expr[Post] = {
@@ -162,7 +187,25 @@ case class TypeQualifierCoercion[Pre <: Generation]()
             d.rewrite(ref = uniqueField(ref.decl, map).ref)
           case _ => d.rewriteDefault()
         }
-
+      case DerefHeapVariable(ref) if isConstElement(ref.decl.t) =>
+        functionInvocation(TrueSatisfiable, constGlobalHeapsSucc.ref(ref.decl))
+      case a@AddrOf(deref@DerefHeapVariable(ref)) if isConstElement(ref.decl.t) =>
+        implicit val o: Origin = a.o
+        val t = dispatch(ref.decl.t)
+        val v = new Variable[Post](TNonNullConstPointer(t))
+        val l = Local[Post](v.ref)
+        val newP = NewNonNullConstPointerArray(dispatch(ref.decl.t), const(1))(PanicBlame("Size >0"))(a.o)
+        ScopedExpr(Seq(v),
+          With[Post](Block(Seq(
+            Assign(l, newP)(AssignLocalOk),
+            Assume(DerefPointer(l)(PanicBlame("Not null & Size>0")) === dispatch(deref))
+          )),
+          l
+          )
+        )
+      case a@AddrOf(e) if isConstElement(e.t) =>
+        if(e.collectFirst {case Deref(_, _) => ()}.isDefined) throw DisallowedQualifiedType(e)
+        AddrOf(AddrOfConstCast(postCoerce(e)))
       case other => other.rewriteDefault()
     }
   }
diff --git a/src/rewrite/vct/rewrite/VariableToPointer.scala b/src/rewrite/vct/rewrite/VariableToPointer.scala
index 68f89acd8..524d8978f 100644
--- a/src/rewrite/vct/rewrite/VariableToPointer.scala
+++ b/src/rewrite/vct/rewrite/VariableToPointer.scala
@@ -15,7 +15,7 @@ case object VariableToPointer extends RewriterBuilder {
   override def key: String = "variableToPointer"
 
   override def desc: String =
-    "Translate every local and field to a pointer such that it can have its address taken"
+    "Translate locals and globals to a pointer when their addresses are taken"
 
   case class UnsupportedAddrOf(loc: Expr[_]) extends UserError {
     override def code: String = "unsupportedAddrOf"
@@ -41,27 +41,48 @@ case class VariableToPointer[Pre <: Generation]() extends Rewriter[Pre] {
 
   import VariableToPointer._
 
-  val addressedSet: mutable.Set[Node[Pre]] = new mutable.HashSet[Node[Pre]]()
+  trait PointerSort
+  case class Normal() extends PointerSort
+  case class Const() extends PointerSort
+
+  val addressedSet: mutable.Map[Node[Pre], PointerSort] = new mutable.HashMap[Node[Pre], PointerSort]()
   val heapVariableMap: SuccessionMap[HeapVariable[Pre], HeapVariable[Post]] =
     SuccessionMap()
   val variableMap: SuccessionMap[Variable[Pre], Variable[Post]] =
     SuccessionMap()
-  val fieldMap: SuccessionMap[InstanceField[Pre], InstanceField[Post]] =
-    SuccessionMap()
   val noTransform: ScopedStack[scala.collection.Set[Variable[Pre]]] =
     ScopedStack()
 
+  def getPointerSort(isConst: Boolean): PointerSort = if(!isConst) Normal() else Const()
+
+  def makePointer(innerType: Type[Post], pt: PointerSort): PointerType[Post] = pt match {
+    case Normal() => TNonNullPointer[Post](innerType, None)
+    case Const() => TNonNullConstPointer[Post](innerType)
+  }
+
+  def isConstPointer(pt: PointerSort) = pt match {
+    case Const() => true
+    case _ => false
+  }
+
+  def makeNewPointerArray(t: Type[Post])(implicit o: Origin): NewPointer[Post] = t match {
+    case TNonNullPointer(innerType, None) =>
+      NewNonNullPointerArray[Post](innerType, const(1), None)(PanicBlame("Size is > 0"))
+    case TNonNullConstPointer(innerType) =>
+      NewNonNullConstPointerArray[Post](innerType, const(1))(PanicBlame("Size is > 0"))
+  }
+
+
+  // TODO: Replace the asByReferenceClass checks with something that more clearly communicates that we want to exclude all reference types
+  def getAddresses(e: Node[Pre], isConst: Boolean = false): Option[(Node[Pre], PointerSort)] = e match {
+    case Local(Ref(v)) if v.t.asByReferenceClass.isEmpty => Some(v, getPointerSort(isConst))
+    case DerefHeapVariable(Ref(v)) if v.t.asByReferenceClass.isEmpty => Some(v, getPointerSort(isConst))
+    case AddrOfConstCast(e) => getAddresses(e, isConst=true)
+    case _ => None
+  }
+
   override def dispatch(program: Program[Pre]): Program[Rewritten[Pre]] = {
-    // TODO: Replace the asByReferenceClass checks with something that more clearly communicates that we want to exclude all reference types
-    addressedSet.addAll(program.collect {
-      case AddrOf(Local(Ref(v))) if v.t.asByReferenceClass.isEmpty => v
-      case AddrOf(DerefHeapVariable(Ref(v)))
-          if v.t.asByReferenceClass.isEmpty =>
-        v
-      case AddrOf(Deref(o, Ref(f)))
-          if f.t.asByReferenceClass.isEmpty && o.t.asByValueClass.isEmpty =>
-        f
-    })
+    addressedSet.addAll(program.flatCollect {case AddrOf(e) =>getAddresses (e)})
     super.dispatch(program)
   }
 
@@ -74,7 +95,7 @@ case class VariableToPointer[Pre <: Generation]() extends Rewriter[Pre] {
       }
       case proc: Procedure[Pre] => {
         val skipVars = mutable.Set[Variable[Pre]]()
-        val extraVars = mutable.ArrayBuffer[(Variable[Post], Variable[Post])]()
+        val extraVars = mutable.ArrayBuffer[(Variable[Post], Variable[Post], PointerSort)]()
         // Relies on args being evaluated before body
         allScopes.anySucceed(
           proc,
@@ -85,9 +106,9 @@ case class VariableToPointer[Pre <: Generation]() extends Rewriter[Pre] {
                   val newV = variables.succeed(v, v.rewriteDefault())
                   if (addressedSet.contains(v)) {
                     variableMap(v) =
-                      new Variable(TNonNullPointer(dispatch(v.t), None))(v.o)
+                      new Variable[Post](makePointer(dispatch(v.t), addressedSet(v)))(v.o)
                     skipVars += v
-                    extraVars += ((newV, variableMap(v)))
+                    extraVars += ((newV, variableMap(v), addressedSet(v)))
                   }
                 }
               }._1,
@@ -99,18 +120,25 @@ case class VariableToPointer[Pre <: Generation]() extends Rewriter[Pre] {
                   variables.scope {
                     val locals =
                       variables.collect {
-                        extraVars.map { case (_, pointer) =>
+                        extraVars.map { case (_, pointer, _) =>
                           variables.declare(pointer)
                         }
                       }._1
                     val block =
-                      Block(extraVars.map { case (normal, pointer) =>
-                        Assign(
-                          DerefPointer(pointer.get(normal.o))(PanicBlame(
+                      Block(extraVars.map {
+                        case (normal, pointer, Normal()) =>
+                          Assign(
+                            DerefPointer(pointer.get(normal.o))(PanicBlame(
+                              "Non-null pointer should always be initialized successfully"
+                            ))(normal.o),
+                            normal.get(normal.o),
+                          )(AssignLocalOk)(proc.o)
+                        case (normal, pointer, Const()) =>
+                          implicit val o: Origin = normal.o
+                          // Const pointers are sequences, so we need to assume their values
+                          Assume(DerefPointer(pointer.get)(PanicBlame(
                             "Non-null pointer should always be initialized successfully"
-                          ))(normal.o),
-                          normal.get(normal.o),
-                        )(AssignLocalOk)(proc.o)
+                          )) === normal.get)
                       }.toSeq :+ dispatch(proc.body.get))(proc.o)
                     Some(Scope(locals, block)(proc.o))
                   }
@@ -125,24 +153,27 @@ case class VariableToPointer[Pre <: Generation]() extends Rewriter[Pre] {
       }
       case v: HeapVariable[Pre] if addressedSet.contains(v) =>
         heapVariableMap(v) = globalDeclarations
-          .succeed(v, new HeapVariable(TNonNullPointer(dispatch(v.t), None))(v.o))
+          .succeed(v, new HeapVariable(makePointer(dispatch(v.t), addressedSet(v)), None)(v.o))
       case v: Variable[Pre] if addressedSet.contains(v) =>
         variableMap(v) = variables
-          .succeed(v, new Variable(TNonNullPointer(dispatch(v.t), None))(v.o))
-      case f: InstanceField[Pre] if addressedSet.contains(f) =>
-        fieldMap(f) = classDeclarations.succeed(
-          f,
-          new InstanceField(
-            TNonNullPointer(dispatch(f.t), None),
-            f.flags.map { it => dispatch(it) },
-          )(f.o),
-        )
+          .succeed(v, new Variable(makePointer(dispatch(v.t), addressedSet(v)))(v.o))
       case other => allScopes.anySucceed(other, other.rewriteDefault())
     }
 
+  def assignToConst(target: Expr[Pre]): Boolean = target match {
+    case Local(v) if addressedSet.contains(v.decl) && isConstPointer(addressedSet(v.decl))=> true
+    case HeapLocal(v) if addressedSet.contains(v.decl) && isConstPointer(addressedSet(v.decl))=> true
+    case _ => false
+  }
+
   override def dispatch(stat: Statement[Pre]): Statement[Post] = {
     implicit val o: Origin = stat.o
     stat match {
+      case assign @ Assign(target, value) if assignToConst(target) =>
+        // We cannot assign towards a const pointer, since it is modelled as sequence. So we have to assume its value
+        Assume[Post](
+          dispatch(target) === dispatch(value)
+        )
       case s: Scope[Pre] =>
         s.rewrite(
           locals = variables.dispatch(s.locals),
@@ -151,56 +182,36 @@ case class VariableToPointer[Pre <: Generation]() extends Rewriter[Pre] {
               implicit val o: Origin = local.o
               Assign(
                 Local[Post](variableMap.ref(local)),
-                NewNonNullPointerArray(
-                  variableMap(local).t.asPointer.get.element,
-                  const(1),
-                  None
-                )(PanicBlame("Size is > 0")),
+                makeNewPointerArray(variableMap(local).t)
               )(PanicBlame("Initialisation should always succeed"))
             } ++ Seq(dispatch(s.body))),
         )
-      case i @ Instantiate(cls, out)
-          if cls.decl.isInstanceOf[ByValueClass[Pre]] =>
-        Block(Seq(i.rewriteDefault()) ++ cls.decl.declarations.flatMap {
-          case f: InstanceField[Pre] =>
-            if (f.t.asClass.isDefined) {
-              Seq(
-                Assign(
-                  Deref[Post](dispatch(out), fieldMap.ref(f))(PanicBlame(
-                    "Initialisation should always succeed"
-                  )),
-                  NewNonNullPointerArray(
-                    fieldMap(f).t.asPointer.get.element,
-                    const(1),
-                    None
-                  )(PanicBlame("Size is > 0")),
-                )(PanicBlame("Initialisation should always succeed")),
-                Assign(
-                  PointerSubscript(
-                    Deref[Post](dispatch(out), fieldMap.ref(f))(PanicBlame(
-                      "Initialisation should always succeed"
-                    )),
-                    const[Post](0),
-                  )(PanicBlame("Size is > 0")),
-                  dispatch(NewObject[Pre](f.t.asClass.get.cls)),
-                )(PanicBlame("Initialisation should always succeed")),
-              )
-            } else if (addressedSet.contains(f)) {
-              Seq(
-                Assign(
-                  Deref[Post](dispatch(out), fieldMap.ref(f))(PanicBlame(
-                    "Initialisation should always succeed"
-                  )),
-                  NewNonNullPointerArray(
-                    fieldMap(f).t.asPointer.get.element,
-                    const(1),
-                    None
-                  )(PanicBlame("Size is > 0")),
-                )(PanicBlame("Initialisation should always succeed"))
-              )
-            } else { Seq() }
-          case _ => Seq()
-        })
+        // TODO: Can we remove this? It doesn't seem we ever fill fieldMap anyway
+//      case i @ Instantiate(cls, out)
+//          if cls.decl.isInstanceOf[ByValueClass[Pre]] =>
+//        Block(Seq(i.rewriteDefault()) ++ cls.decl.declarations.flatMap {
+//          case f: InstanceField[Pre] =>
+//            if (f.t.asClass.isDefined) {
+//              Seq(
+//                Assign(
+//                  Deref[Post](dispatch(out), fieldMap.ref(f))(PanicBlame(
+//                    "Initialisation should always succeed"
+//                  )),
+//                  makeNewPointerArray(fieldMap(f).t),
+//                )(PanicBlame("Initialisation should always succeed")),
+//                Assign(
+//                  PointerSubscript(
+//                    Deref[Post](dispatch(out), fieldMap.ref(f))(PanicBlame(
+//                      "Initialisation should always succeed"
+//                    )),
+//                    const[Post](0),
+//                  )(PanicBlame("Size is > 0")),
+//                  dispatch(NewObject[Pre](f.t.asClass.get.cls)),
+//                )(PanicBlame("Initialisation should always succeed")),
+//              )
+//            } else { Seq() }
+//          case _ => Seq()
+//        })
       case other => other.rewriteDefault()
     }
   }
@@ -217,10 +228,6 @@ case class VariableToPointer[Pre <: Generation]() extends Rewriter[Pre] {
         DerefPointer(Local[Post](variableMap.ref(v)))(PanicBlame(
           "Should always be accessible"
         ))
-      case deref @ Deref(obj, Ref(f)) if addressedSet.contains(f) =>
-        DerefPointer(Deref[Post](dispatch(obj), fieldMap.ref(f))(deref.blame))(
-          PanicBlame("Should always be accessible")
-        )
       case newObject @ NewObject(Ref(cls: ByValueClass[Pre])) =>
         val obj = new Variable[Post](TByValueClass(succ(cls), Seq()))
         ScopedExpr(
@@ -239,19 +246,6 @@ case class VariableToPointer[Pre <: Generation]() extends Rewriter[Pre] {
                           dispatch(NewObject[Pre](f.t.asClass.get.cls)),
                         )(PanicBlame("Initialisation should always succeed"))
                       )
-                    } else if (addressedSet.contains(f)) {
-                      Seq(
-                        Assign(
-                          Deref[Post](obj.get, fieldMap.ref(f))(PanicBlame(
-                            "Initialisation should always succeed"
-                          )),
-                          NewNonNullPointerArray(
-                            fieldMap(f).t.asPointer.get.element,
-                            const(1),
-                            None
-                          )(PanicBlame("Size is > 0")),
-                        )(PanicBlame("Initialisation should always succeed"))
-                      )
                     } else { Seq() }
                   case _ => Seq()
                 }
@@ -281,6 +275,7 @@ case class VariableToPointer[Pre <: Generation]() extends Rewriter[Pre] {
             ))(PanicBlame("cannot be null"))
           ),
         )
+      case a@AddrOf(AddrOfConstCast(e)) => a.rewrite(e=dispatch(e))
       case other => other.rewriteDefault()
     }
   }
@@ -294,13 +289,6 @@ case class VariableToPointer[Pre <: Generation]() extends Rewriter[Pre] {
             "Should always be accessible"
           ))
         )(PanicBlame("Should always be accessible"))
-      case FieldLocation(obj, Ref(f)) if addressedSet.contains(f) =>
-        PointerLocation(Deref[Post](dispatch(obj), fieldMap.ref(f))(PanicBlame(
-          "Should always be accessible"
-        )))(PanicBlame("Should always be accessible"))
-      case PointerLocation(AddrOf(Deref(obj, Ref(f))))
-          if addressedSet.contains(f) =>
-        FieldLocation[Post](dispatch(obj), fieldMap.ref(f))
       case PointerLocation(AddrOf(DerefHeapVariable(Ref(v))))
           if addressedSet.contains(v) =>
         HeapVariableLocation[Post](heapVariableMap.ref(v))
diff --git a/src/rewrite/vct/rewrite/lang/LangCPPToCol.scala b/src/rewrite/vct/rewrite/lang/LangCPPToCol.scala
index 3460278bd..4ddd2e2ca 100644
--- a/src/rewrite/vct/rewrite/lang/LangCPPToCol.scala
+++ b/src/rewrite/vct/rewrite/lang/LangCPPToCol.scala
@@ -978,7 +978,7 @@ case class LangCPPToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
             declared = true
           case None =>
             cppGlobalNameSuccessor(RefCPPGlobalDeclaration(decl, idx)) = rw
-              .globalDeclarations.declare(new HeapVariable(t)(namedO))
+              .globalDeclarations.declare(new HeapVariable(t, init.init.map(rw.dispatch))(namedO))
         }
       }
     }
diff --git a/src/rewrite/vct/rewrite/lang/LangCToCol.scala b/src/rewrite/vct/rewrite/lang/LangCToCol.scala
index dedd606a2..4918ae42c 100644
--- a/src/rewrite/vct/rewrite/lang/LangCToCol.scala
+++ b/src/rewrite/vct/rewrite/lang/LangCToCol.scala
@@ -1210,7 +1210,7 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
             else { t }
           cGlobalNameSuccessor(RefCGlobalDeclaration(decl, idx)) = rw
             .globalDeclarations
-            .declare(new HeapVariable(newT)(init.o.sourceName(info.name)))
+            .declare(new HeapVariable(newT, init.init.map(rw.dispatch))(init.o.sourceName(info.name)))
       }
     }
   }
@@ -1226,7 +1226,7 @@ case class LangCToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
         Assume[Post](
         AmbiguousSubscript(array.get, c_const(index))(PanicBlame(
           "The explicit initialization of an array in C should never exceed the bounds of the array"
-        )) === rw.dispatch(value),
+        )) === rw.dispatch(value)
         )
     })
   }
diff --git a/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala b/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala
index b4338bcdd..005359c2d 100644
--- a/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala
+++ b/src/rewrite/vct/rewrite/lang/LangLLVMToCol.scala
@@ -681,7 +681,8 @@ case class LangLLVMToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
                   Seq(),
                 )(struct.o),
                 None
-              )(struct.o)
+              )(struct.o),
+              decl.value.map(rw.dispatch)
             )(decl.o)
           ),
         )
@@ -691,7 +692,8 @@ case class LangLLVMToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
           decl,
           rw.globalDeclarations.declare(
             new HeapVariable[Post](
-              new TPointer[Post](rw.dispatch(array.elementType), None)(array.o)
+              new TPointer[Post](rw.dispatch(array.elementType), None)(array.o),
+              None
             )(decl.o)
           ),
         )
@@ -701,7 +703,8 @@ case class LangLLVMToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
           decl,
           rw.globalDeclarations.declare(
             new HeapVariable[Post](
-              new TPointer[Post](rw.dispatch(vector.elementType), None)(vector.o)
+              new TPointer[Post](rw.dispatch(vector.elementType), None)(vector.o),
+              None
             )(decl.o)
           ),
         )
diff --git a/test/main/vct/test/integration/examples/QualifierSpec.scala b/test/main/vct/test/integration/examples/QualifierSpec.scala
index 9e1471fd4..d3e39b478 100644
--- a/test/main/vct/test/integration/examples/QualifierSpec.scala
+++ b/test/main/vct/test/integration/examples/QualifierSpec.scala
@@ -13,6 +13,7 @@ class ConstQualifierSpec extends VercorsSpec {
   vercors should error withCode "disallowedConstAssignment" in "Assign to param pointer of const" c """void f(const int *x){x[0] = 1;}"""
 
   vercors should verify using silicon in "Assign const array to const pointer" c """void f(const int* y){const int x[2] = {0, 2}; y = x;}"""
+
   vercors should error withCode "resolutionError:type" in "Assign const array to non-const pointer" c """void f(int* y){const int x[2] = {0, 2}; x = y;}"""
 
   vercors should error withCode "disallowedConstAssignment" in "Assign const pointer" c """void f(int* const y){int* const x; y = x;}"""
@@ -70,6 +71,68 @@ int f(struct vec v){
 void f(const int* x){
   int y = x[0];
 }
+"""
+
+  vercors should verify using silicon in "Return head of const pointer" c
+    """
+//@ context a!= NULL ** \pointer_length(a)==1;
+int foo(const int *a) {
+    return *a;
+}
+"""
+
+  vercors should verify using silicon in "Take address of const int" c
+    """
+int f() {
+    const int a = 0;
+    const int *b = &a;
+    return *b;
+}
+"""
+
+  vercors should error withCode "disallowedQualifiedType" in "Cannot take address for unique pointer" c
+    """
+int f() {
+    /*@unique<1>@*/ int a = 0;
+    /*@unique<1>@*/ int *b = &a;
+    return *b;
+}
+"""
+
+  vercors should verify using silicon in "Take address of const int param" c
+    """
+int f(const int a) {
+    const int *b = &a;
+    return *b;
+}
+"""
+
+
+  /* TODO: This is possible if we want it. But it would be best to do this in one go together
+   *  with making unique types work for pointer fields && it takes quite some work.
+   */
+  vercors should error withCode "disallowedQualifiedType" in  "Take address of const int field" c
+    """
+struct vec {
+  const int a;
+};
+
+//@ context Perm(v, 1\2);
+int f(struct vec v) {
+  const int *b = &v.a;
+  return *b;
+}
+"""
+
+  vercors should verify using silicon in "Take address of const global int" c
+    """
+const int a = 5;
+
+//@ ensures \result == 5;
+int foo() {
+   const int * b = &a;
+   return *b;
+}
 """
 }
 
@@ -941,4 +1004,12 @@ void f(/*@unique<1>@*/ int* x){
   int* y = &(x[0]);
 }
 """
+}
+
+class WIP extends VercorsSpec {
+
+}
+
+class WIP2 extends VercorsSpec {
+
 }
\ No newline at end of file