diff --git a/src/main/scala/viper/gobra/ast/internal/PrettyPrinter.scala b/src/main/scala/viper/gobra/ast/internal/PrettyPrinter.scala
index 4b7950e42..d58b0892d 100644
--- a/src/main/scala/viper/gobra/ast/internal/PrettyPrinter.scala
+++ b/src/main/scala/viper/gobra/ast/internal/PrettyPrinter.scala
@@ -569,7 +569,7 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
     case PermTExpr() => "perm"
     case PointerTExpr(elem) => "*" <> showExpr(elem)
     case StructTExpr(fs) => "struct" <> braces(showList(fs)(f => f._1 <> ":" <+> showExpr(f._2)))
-    case ArrayTExpr(len, elem) => brackets(showExpr(len)) <> showExpr(elem)
+    case ArrayTExpr(len, elem) => brackets(len.toString()) <> showExpr(elem)
     case SliceTExpr(elem) => brackets(emptyDoc) <> showExpr(elem)
     case MapTExpr(key, elem) => "map" <> brackets(showExpr(key) <> comma <+> showExpr(elem))
     case SequenceTExpr(elem) => "seq" <> brackets(showExpr(elem))
@@ -583,6 +583,7 @@ class DefaultPrettyPrinter extends PrettyPrinter with kiama.output.PrettyPrinter
     case DfltVal(typ) => "dflt" <> brackets(showType(typ))
     case Tuple(args) => parens(showExprList(args))
     case Deref(exp, _) => "*" <> showExpr(exp)
+    case UncheckedRef(ref, _) => "&" <> showAddressable(ref)
     case Ref(ref, _) => "&" <> showAddressable(ref)
     case FieldRef(recv, field) => showExpr(recv) <> "."  <> field.name
     case StructUpdate(base, field, newVal) => showExpr(base) <> brackets(showField(field) <+> ":=" <+> showExpr(newVal))
diff --git a/src/main/scala/viper/gobra/ast/internal/Program.scala b/src/main/scala/viper/gobra/ast/internal/Program.scala
index 688bd6ec8..c8ebca72e 100644
--- a/src/main/scala/viper/gobra/ast/internal/Program.scala
+++ b/src/main/scala/viper/gobra/ast/internal/Program.scala
@@ -645,7 +645,7 @@ case class Float32TExpr()(val info: Source.Parser.Info) extends TypeExpr
 case class Float64TExpr()(val info: Source.Parser.Info) extends TypeExpr
 case class IntTExpr(kind: IntegerKind)(val info: Source.Parser.Info) extends TypeExpr
 case class StructTExpr(fields: Vector[(String, Expr, Boolean)])(val info: Source.Parser.Info) extends TypeExpr
-case class ArrayTExpr(length: Expr, elems: Expr)(val info: Source.Parser.Info) extends TypeExpr
+case class ArrayTExpr(length: BigInt, elems: Expr)(val info: Source.Parser.Info) extends TypeExpr
 case class SliceTExpr(elems: Expr)(val info: Source.Parser.Info) extends TypeExpr
 case class MapTExpr(keys: Expr, elems: Expr)(val info: Source.Parser.Info) extends TypeExpr
 case class PermTExpr()(val info: Source.Parser.Info) extends TypeExpr
@@ -945,7 +945,18 @@ case class Deref(exp: Expr, underlyingTypeExpr: Type)(val info: Source.Parser.In
   override val typ: Type = underlyingTypeExpr.asInstanceOf[PointerT].t
 }
 
-case class Ref(ref: Addressable, typ: PointerT)(val info: Source.Parser.Info) extends Expr with Location
+/** Only used internally to separate the type encodings. Should not be created by the desugarer. */
+case class UncheckedRef(ref: Addressable, typ: PointerT)(val info: Source.Parser.Info) extends Expr {
+  def checked: Ref = Ref(ref, typ)(info)
+}
+
+object UncheckedRef {
+  def apply(exp: Expr)(info: Source.Parser.Info): UncheckedRef = Ref(exp)(info).unchecked
+}
+
+case class Ref(ref: Addressable, typ: PointerT)(val info: Source.Parser.Info) extends Expr {
+  def unchecked: UncheckedRef = UncheckedRef(ref, typ)(info)
+}
 
 object Ref {
   def apply(ref: Expr)(info: Source.Parser.Info): Ref = {
diff --git a/src/main/scala/viper/gobra/ast/internal/theory/Comparability.scala b/src/main/scala/viper/gobra/ast/internal/theory/Comparability.scala
index 0ea896aa5..8db217a22 100644
--- a/src/main/scala/viper/gobra/ast/internal/theory/Comparability.scala
+++ b/src/main/scala/viper/gobra/ast/internal/theory/Comparability.scala
@@ -42,7 +42,7 @@ object Comparability {
 
     case _: TypeHead.StructHD => Kind.Recursive
     case _: TypeHead.FunctionHD => Kind.NonComparable
-    case TypeHead.ArrayHD => Kind.Recursive
+    case _: TypeHead.ArrayHD => Kind.Recursive
     case TypeHead.SliceHD => Kind.NonComparable
     case TypeHead.MapHD => Kind.NonComparable
     case _: TypeHead.InterfaceHD => Kind.Dynamic
diff --git a/src/main/scala/viper/gobra/ast/internal/theory/TypeHead.scala b/src/main/scala/viper/gobra/ast/internal/theory/TypeHead.scala
index 27bae7961..f0089f3ec 100644
--- a/src/main/scala/viper/gobra/ast/internal/theory/TypeHead.scala
+++ b/src/main/scala/viper/gobra/ast/internal/theory/TypeHead.scala
@@ -27,7 +27,7 @@ object TypeHead {
   case class FunctionHD(arity: Int) extends TypeHead
   /** 'fields' stores for each field the name and whether the field is ghost. */
   case class StructHD(fields: Vector[(String, Boolean)]) extends TypeHead
-  case object ArrayHD extends TypeHead
+  case class ArrayHD(size: BigInt) extends TypeHead
   case object SliceHD extends TypeHead
   case object MapHD extends TypeHead
   case class InterfaceHD(name: String) extends TypeHead
@@ -74,7 +74,7 @@ object TypeHead {
     case VoidT => UnitHD
     case _: PermissionT => PermHD
     case SortT => SortHD
-    case _: ArrayT => ArrayHD
+    case t: ArrayT => ArrayHD(t.length)
     case _: SliceT => SliceHD
     case _: MapT => MapHD
     case _: SequenceT => SeqHD
@@ -151,7 +151,7 @@ object TypeHead {
     case _: PointerTExpr => PointerHD
     case t: DefinedTExpr => DefinedHD(t.name)
     case t: StructTExpr => StructHD(t.fields.map(t => (t._1, t._3)))
-    case _: ArrayTExpr => ArrayHD
+    case t: ArrayTExpr => ArrayHD(t.length)
     case _: SliceTExpr => SliceHD
     case _: MapTExpr => MapHD
     case _: PermTExpr => PermHD
@@ -174,7 +174,7 @@ object TypeHead {
     case _: DefinedHD => 0
     case t: FunctionHD => t.arity
     case t: StructHD => t.fields.size
-    case ArrayHD => 1
+    case _: ArrayHD => 1
     case SliceHD => 1
     case MapHD => 2
     case _: InterfaceHD => 0
@@ -195,5 +195,13 @@ object TypeHead {
     case t: PredHD => t.arity
   }
 
-
+  def isZeroSize(t: Type)(ctx: LookupTable): Boolean = isZeroSize(typeTree(t))(ctx)
+  def isZeroSize(t: RoseTree[TypeHead])(ctx: LookupTable): Boolean = {
+    t match {
+      case RoseTree(_: StructHD, children) => children.forall(isZeroSize(_)(ctx))
+      case RoseTree(hd: ArrayHD, children) => hd.size == 0 || children.forall(isZeroSize(_)(ctx))
+      case RoseTree(hd: DefinedHD, _) => isZeroSize(ctx.lookup(DefinedT(hd.name, Addressability.Exclusive)))(ctx)
+      case _ => false
+    }
+  }
 }
diff --git a/src/main/scala/viper/gobra/ast/internal/transform/CGEdgesTerminationTransform.scala b/src/main/scala/viper/gobra/ast/internal/transform/CGEdgesTerminationTransform.scala
index af4eb1036..74173eed2 100644
--- a/src/main/scala/viper/gobra/ast/internal/transform/CGEdgesTerminationTransform.scala
+++ b/src/main/scala/viper/gobra/ast/internal/transform/CGEdgesTerminationTransform.scala
@@ -229,7 +229,7 @@ object CGEdgesTerminationTransform extends InternalTransform {
       case in.IntT(_, kind) => in.IntTExpr(kind)(src)
       case in.StringT(_) => in.StringTExpr()(src)
       case in.PermissionT(_) => in.PermTExpr()(src)
-      case in.ArrayT(length, elems, _) => in.ArrayTExpr(in.IntLit(length)(src), typeAsExpr(elems)(src))(src)
+      case in.ArrayT(length, elems, _) => in.ArrayTExpr(length, typeAsExpr(elems)(src))(src)
       case in.SliceT(elems, _) => in.SliceTExpr(typeAsExpr(elems)(src))(src)
       case in.MapT(keys, values, _) => in.MapTExpr(typeAsExpr(keys)(src), typeAsExpr(values)(src))(src)
       case in.SequenceT(t, _) => in.SequenceTExpr(typeAsExpr(t)(src))(src)
diff --git a/src/main/scala/viper/gobra/frontend/Desugar.scala b/src/main/scala/viper/gobra/frontend/Desugar.scala
index 5f8dd2cfc..08ed5d4c7 100644
--- a/src/main/scala/viper/gobra/frontend/Desugar.scala
+++ b/src/main/scala/viper/gobra/frontend/Desugar.scala
@@ -2965,9 +2965,8 @@ object Desugar extends LazyLogging {
 
         case PArrayType(len, elem) =>
           for {
-            inLen <- exprD(ctx, info)(len)
             inElem <- go(elem)
-          } yield in.ArrayTExpr(inLen, inElem)(src)
+          } yield in.ArrayTExpr(info.evalInt(len), inElem)(src)
 
         case PSliceType(elem) =>
           for {
diff --git a/src/main/scala/viper/gobra/frontend/info/TypeInfo.scala b/src/main/scala/viper/gobra/frontend/info/TypeInfo.scala
index 09c479f9f..1a8e358bc 100644
--- a/src/main/scala/viper/gobra/frontend/info/TypeInfo.scala
+++ b/src/main/scala/viper/gobra/frontend/info/TypeInfo.scala
@@ -42,4 +42,9 @@ trait TypeInfo extends ExternalTypeInfo {
   def freeDeclared(n: PNode): Vector[PIdnNode]
 
   def capturedLocalVariables(decl: PClosureDecl): Vector[PIdnNode]
+
+  def evalBool(exp: PExpression): Boolean
+  def evalInt(exp: PExpression): BigInt
+  def evalString(exp: PExpression): String
+  def evalPerm(exp: PExpression): (BigInt, BigInt)
 }
diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/property/ConstantEvaluation.scala b/src/main/scala/viper/gobra/frontend/info/implementation/property/ConstantEvaluation.scala
index e045a787c..5f59a1962 100644
--- a/src/main/scala/viper/gobra/frontend/info/implementation/property/ConstantEvaluation.scala
+++ b/src/main/scala/viper/gobra/frontend/info/implementation/property/ConstantEvaluation.scala
@@ -15,6 +15,23 @@ import viper.gobra.util.Violation.violation
 
 trait ConstantEvaluation { this: TypeInfoImpl =>
 
+  def evalBool(exp: PExpression): Boolean = {
+    boolConstantEval(exp).getOrElse(violation(s"expected constant bool expression, but got $exp"))
+  }
+
+  def evalInt(exp: PExpression): BigInt = {
+    intConstantEval(exp).getOrElse(violation(s"expected constant int expression, but got $exp"))
+  }
+
+  def evalString(exp: PExpression): String = {
+    stringConstantEval(exp).getOrElse(violation(s"expected constant string expression, but got $exp"))
+  }
+
+  def evalPerm(exp: PExpression): (BigInt, BigInt) = {
+    permConstantEval(exp).getOrElse(violation(s"expected constant permission expression, but got $exp"))
+  }
+
+
   lazy val boolConstantEval: PExpression => Option[Boolean] =
     attr[PExpression, Option[Boolean]] {
       case PBoolLit(lit) => Some(lit)
diff --git a/src/main/scala/viper/gobra/reporting/DefaultErrorBackTranslator.scala b/src/main/scala/viper/gobra/reporting/DefaultErrorBackTranslator.scala
index ae4ccc88b..7a6bf64fd 100644
--- a/src/main/scala/viper/gobra/reporting/DefaultErrorBackTranslator.scala
+++ b/src/main/scala/viper/gobra/reporting/DefaultErrorBackTranslator.scala
@@ -91,7 +91,7 @@ object DefaultErrorBackTranslator {
 
     val transformVerificationErrorReason: VerificationErrorReason => VerificationErrorReason = {
       case AssertionFalseError(info / OverflowCheckAnnotation) => OverflowErrorReason(info)
-      case AssertionFalseError(info / ReceiverNotNilCheckAnnotation) => InterfaceReceiverIsNilReason(info)
+      case AssertionFalseError(info / ReceiverNotNilCheckAnnotation) => ReceiverIsNilReason(info)
       case x => x
     }
 
diff --git a/src/main/scala/viper/gobra/reporting/VerifierError.scala b/src/main/scala/viper/gobra/reporting/VerifierError.scala
index b7e986dc6..624f878c8 100644
--- a/src/main/scala/viper/gobra/reporting/VerifierError.scala
+++ b/src/main/scala/viper/gobra/reporting/VerifierError.scala
@@ -448,9 +448,9 @@ case class OverflowErrorReason(node: Source.Verifier.Info) extends VerificationE
   override def message: String = s"Expression ${node.origin.tag.trim} might cause integer overflow."
 }
 
-case class InterfaceReceiverIsNilReason(node: Source.Verifier.Info) extends VerificationErrorReason {
+case class ReceiverIsNilReason(node: Source.Verifier.Info) extends VerificationErrorReason {
   override def id: String = "receiver_is_nil_error"
-  override def message: String = s"The receiver might be nil"
+  override def message: String = s"The receiver ${node.origin.tag.trim} might be nil"
 }
 
 case class DynamicValueNotASubtypeReason(node: Source.Verifier.Info) extends VerificationErrorReason {
diff --git a/src/main/scala/viper/gobra/translator/context/Context.scala b/src/main/scala/viper/gobra/translator/context/Context.scala
index 224a5c613..6323c6d29 100644
--- a/src/main/scala/viper/gobra/translator/context/Context.scala
+++ b/src/main/scala/viper/gobra/translator/context/Context.scala
@@ -99,6 +99,8 @@ trait Context {
 
   def reference(x: in.Location): CodeWriter[vpr.Exp] = typeEncoding.reference(this)(x)
 
+  def safeReference(x: in.Location): CodeWriter[vpr.Exp] = typeEncoding.safeReference(this)(x)
+
   def value(x: in.Expr): CodeWriter[vpr.Exp] = typeEncoding.value(this)(x)
 
   def footprint(x: in.Location, perm: in.Expr): CodeWriter[vpr.Exp] = typeEncoding.addressFootprint(this)(x, perm)
@@ -138,7 +140,6 @@ trait Context {
   }
 
   // mapping
-
   def addVars(vars: vpr.LocalVarDecl*): Context
 
   // fresh variable counter
@@ -146,7 +147,7 @@ trait Context {
   def freshNames: Iterator[String] = internalFreshNames
 
   /** internal fresh name iterator that additionally provides a getter function for its counter value */
-  protected def internalFreshNames: FreshNameIterator
+  protected def internalFreshNames: Context.FreshNameIterator
 
   /** copy constructor */
   def :=(
@@ -165,7 +166,28 @@ trait Context {
           unknownValueN: UnknownValues = unknownValue,
           typeEncodingN: TypeEncoding = typeEncoding,
           defaultEncodingN: DefaultEncoding = defaultEncoding,
-          initialFreshCounterValueN: Int = internalFreshNames.getValue
+          initialFreshCounterValueN: Option[Int] = None,
+        ): Context = {
+    update(fieldN, arrayN, seqToSetN, seqToMultisetN, seqMultiplicityN, optionN, optionToSeqN, sliceN, fixpointN, tupleN, equalityN, conditionN, unknownValueN, typeEncodingN, defaultEncodingN, initialFreshCounterValueN)
+  }
+
+  protected def update(
+          fieldN: Fields,
+          arrayN: Arrays,
+          seqToSetN: SeqToSet,
+          seqToMultisetN: SeqToMultiset,
+          seqMultiplicityN: SeqMultiplicity,
+          optionN: Options,
+          optionToSeqN: OptionToSeq,
+          sliceN: Slices,
+          fixpointN: Fixpoint,
+          tupleN: Tuples,
+          equalityN: Equality,
+          conditionN: Conditions,
+          unknownValueN: UnknownValues,
+          typeEncodingN: TypeEncoding,
+          defaultEncodingN: DefaultEncoding,
+          initialFreshCounterValueN: Option[Int],
         ): Context
 
 
@@ -189,8 +211,10 @@ trait Context {
     col.finalize(typeEncoding)
   }
 
+}
+
+object Context {
   trait FreshNameIterator extends Iterator[String] {
     def getValue: Int
   }
-
-}
+}
\ No newline at end of file
diff --git a/src/main/scala/viper/gobra/translator/context/ContextImpl.scala b/src/main/scala/viper/gobra/translator/context/ContextImpl.scala
index 1bfa6abc0..5cb3157b3 100644
--- a/src/main/scala/viper/gobra/translator/context/ContextImpl.scala
+++ b/src/main/scala/viper/gobra/translator/context/ContextImpl.scala
@@ -22,25 +22,25 @@ import viper.gobra.translator.library.tuples.Tuples
 import viper.gobra.translator.library.unknowns.UnknownValues
 import viper.silver.ast.LocalVarDecl
 
-case class ContextImpl(
-                        field: Fields,
-                        array: Arrays,
-                        seqToSet: SeqToSet,
-                        seqToMultiset: SeqToMultiset,
-                        seqMultiplicity: SeqMultiplicity,
-                        option: Options,
-                        optionToSeq: OptionToSeq,
-                        slice: Slices,
-                        fixpoint: Fixpoint,
-                        tuple: Tuples,
-                        equality: Equality,
-                        condition: Conditions,
-                        unknownValue: UnknownValues,
-                        typeEncoding: TypeEncoding,
-                        defaultEncoding: DefaultEncoding,
-                        table: LookupTable,
-                        initialFreshCounterValue: Int = 0
-                      ) extends Context {
+class ContextImpl(
+                   override val field: Fields,
+                   override val array: Arrays,
+                   override val seqToSet: SeqToSet,
+                   override val seqToMultiset: SeqToMultiset,
+                   override val seqMultiplicity: SeqMultiplicity,
+                   override val option: Options,
+                   override val optionToSeq: OptionToSeq,
+                   override val slice: Slices,
+                   override val fixpoint: Fixpoint,
+                   override val tuple: Tuples,
+                   override val equality: Equality,
+                   override val condition: Conditions,
+                   override val unknownValue: UnknownValues,
+                   override val typeEncoding: TypeEncoding,
+                   override val defaultEncoding: DefaultEncoding,
+                   override val table: LookupTable,
+                   override val internalFreshNames: Context.FreshNameIterator = ContextImpl.FreshNameIteratorImpl(0),
+                 ) extends Context {
 
   def this(conf: TranslatorConfig, table: LookupTable) = {
     this(
@@ -64,24 +64,24 @@ case class ContextImpl(
   }
 
   /** copy constructor */
-  override def :=(
-                   fieldN: Fields = field,
-                   arrayN: Arrays = array,
-                   seqToSetN: SeqToSet = seqToSet,
-                   seqToMultisetN: SeqToMultiset = seqToMultiset,
-                   seqMultiplicityN: SeqMultiplicity = seqMultiplicity,
-                   optionN: Options = option,
-                   optionToSeqN: OptionToSeq = optionToSeq,
-                   sliceN: Slices = slice,
-                   fixpointN: Fixpoint = fixpoint,
-                   tupleN: Tuples = tuple,
-                   equalityN: Equality = equality,
-                   conditionN: Conditions = condition,
-                   unknownValueN: UnknownValues = unknownValue,
-                   typeEncodingN: TypeEncoding = typeEncoding,
-                   defaultEncodingN: DefaultEncoding = defaultEncoding,
-                   initialFreshCounterValueN: Int = internalFreshNames.getValue
-                 ): Context = copy(
+  override def update(
+                   fieldN: Fields,
+                   arrayN: Arrays,
+                   seqToSetN: SeqToSet,
+                   seqToMultisetN: SeqToMultiset,
+                   seqMultiplicityN: SeqMultiplicity,
+                   optionN: Options,
+                   optionToSeqN: OptionToSeq,
+                   sliceN: Slices,
+                   fixpointN: Fixpoint,
+                   tupleN: Tuples,
+                   equalityN: Equality,
+                   conditionN: Conditions,
+                   unknownValueN: UnknownValues,
+                   typeEncodingN: TypeEncoding,
+                   defaultEncodingN: DefaultEncoding,
+                   initialFreshCounterValueN: Option[Int],
+                 ): Context = new ContextImpl(
     fieldN,
     arrayN,
     seqToSetN,
@@ -97,14 +97,19 @@ case class ContextImpl(
     unknownValueN,
     typeEncodingN,
     defaultEncodingN,
-    initialFreshCounterValue = initialFreshCounterValueN
+    table,
+    initialFreshCounterValueN match {
+      case None => internalFreshNames
+      case Some(n) => ContextImpl.FreshNameIteratorImpl(n)
+    },
   )
 
   override def addVars(vars: LocalVarDecl*): Context = this
 
-  override val internalFreshNames: FreshNameIteratorImpl = FreshNameIteratorImpl(initialFreshCounterValue)
+}
 
-  case class FreshNameIteratorImpl(private val initialValue: Int) extends FreshNameIterator {
+object ContextImpl {
+  case class FreshNameIteratorImpl(private val initialValue: Int) extends Context.FreshNameIterator {
     private var currentValue: Int = initialValue
 
     override def hasNext: Boolean = true
@@ -117,5 +122,4 @@ case class ContextImpl(
 
     override def getValue: Int = currentValue
   }
-
 }
diff --git a/src/main/scala/viper/gobra/translator/encodings/PointerEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/PointerEncoding.scala
index 9b94bafae..a2a9d5be8 100644
--- a/src/main/scala/viper/gobra/translator/encodings/PointerEncoding.scala
+++ b/src/main/scala/viper/gobra/translator/encodings/PointerEncoding.scala
@@ -72,7 +72,6 @@ class PointerEncoding extends LeafTypeEncoding {
     * Ref[*e] -> [e]
     */
   override def reference(ctx: Context): in.Location ==> CodeWriter[vpr.Exp] = default(super.reference(ctx)){
-    case (loc: in.Deref) :: _ / Shared =>
-      ctx.expression(loc.exp)
+    case (loc: in.Deref) :: _ / Shared => ctx.expression(loc.exp)
   }
 }
diff --git a/src/main/scala/viper/gobra/translator/encodings/arrays/ArrayEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/arrays/ArrayEncoding.scala
index 5eb0a288e..feaf8f5d8 100644
--- a/src/main/scala/viper/gobra/translator/encodings/arrays/ArrayEncoding.scala
+++ b/src/main/scala/viper/gobra/translator/encodings/arrays/ArrayEncoding.scala
@@ -109,14 +109,8 @@ class ArrayEncoding extends TypeEncoding with SharedArrayEmbedding {
     *
     * [lhs: [n]T == rhs: [n]T] -> let x = lhs, y = rhs in Forall idx :: {trigger} 0 <= idx < n ==> [ x[idx] == y[idx] ]
     *     where trigger = array_get(x, idx, n), array_get(y, idx, n)
-    *
-    * // According to the Go spec, pointers to distinct zero-sized data may or may not be equal. Thus:
-    * [x: *[0]T° == x: *[0]T] -> true
-    * [lhs: *[0]T° == rhs: *[0]T] -> [rhs] == [nil] ? [lhs] == [rhs] : unknown()
-    *
-    * [lhs: *[n]T° == rhs: *[n]T] -> [lhs] == [rhs]
     */
-  override def equal(ctx: Context): (in.Expr, in.Expr, in.Node) ==> CodeWriter[vpr.Exp] = {
+  override def equal(ctx: Context): (in.Expr, in.Expr, in.Node) ==> CodeWriter[vpr.Exp] = default(super.equal(ctx)){
     case (lhs :: ctx.Array(len, _), rhs :: ctx.Array(len2, _), src) if len == len2 =>
       for {
         (x, xTrigger) <- copyArray(lhs)(ctx)
@@ -126,27 +120,6 @@ class ArrayEncoding extends TypeEncoding with SharedArrayEmbedding {
         body = (idx: in.BoundVar) => ctx.equal(in.IndexedExp(x, idx, typLhs)(src.info), in.IndexedExp(y, idx, typRhs)(src.info))(src)
         res <- boundedQuant(len, idx => xTrigger(idx) ++ yTrigger(idx), body)(src)(ctx)
       } yield res
-
-    case (lhs :: ctx.*(ctx.Array(len, _)) / Exclusive, rhs :: ctx.*(ctx.Array(len2, _)), src) if len == len2 =>
-      if (len == 0) {
-        val (pos, info, errT) = src.vprMeta
-        if (lhs == rhs) unit(vpr.TrueLit()(pos, info ,errT))
-        else {
-          for {
-            vLhs <- ctx.expression(lhs)
-            vRhs <- ctx.expression(rhs)
-            vNil <- ctx.expression(in.NilLit(rhs.typ)(src.info))
-            eq1 = vpr.EqCmp(vRhs, vNil)(pos, info, errT)
-            eq2 = vpr.EqCmp(vLhs, vRhs)(pos, info, errT)
-            vUnk = ctx.unknownValue.unkownValue(vpr.Bool)(pos, info ,errT)
-          } yield vpr.CondExp(eq1, eq2, vUnk)(pos, info, errT)
-        }
-      } else {
-        for {
-          vLhs <- ctx.expression(lhs)
-          vRhs <- ctx.expression(rhs)
-        } yield withSrc(vpr.EqCmp(vLhs, vRhs), src)
-      }
   }
 
   /**
@@ -168,7 +141,7 @@ class ArrayEncoding extends TypeEncoding with SharedArrayEmbedding {
     * R[ mset(e: [n]T) ] -> seqToMultiset(ex_array_toSeq([e]))
     * R[ x in (e: [n]T) ] -> [x] in ex_array_toSeq([e])
     * R[ x # (e: [n]T) ] -> [x] # ex_array_toSeq([e])
-    * R[ loc: ([n]T)@ ] -> arrayConversion(L[loc])
+    * R[ loc: ([n]T)@ ] -> arrayConversion(Ref[loc]) // assert [&loc != nil] if [n]T has size zero
     */
   override def expression(ctx: Context): in.Expr ==> CodeWriter[vpr.Exp] = default(super.expression(ctx)){
     case (loc@ in.IndexedExp(base :: ctx.Array(len, t), idx, _)) :: _ / Exclusive =>
@@ -198,7 +171,7 @@ class ArrayEncoding extends TypeEncoding with SharedArrayEmbedding {
     case n@ in.Length(e :: ctx.Array(len, t) / m) =>
       m match {
         case Exclusive => ctx.expression(e).map(ex.length(_, cptParam(len, t)(ctx))(n)(ctx))
-        case Shared => ctx.reference(e.asInstanceOf[in.Location]).map(sh.length(_, cptParam(len, t)(ctx))(n)(ctx))
+        case Shared => ctx.safeReference(e.asInstanceOf[in.Location]).map(sh.length(_, cptParam(len, t)(ctx))(n)(ctx))
       }
 
     case n@ in.SequenceConversion(e :: ctx.Array(len, t) / Exclusive) =>
@@ -226,7 +199,7 @@ class ArrayEncoding extends TypeEncoding with SharedArrayEmbedding {
         vE <- ctx.expression(e)
       } yield ctx.seqMultiplicity.create(vX, ex.toSeq(vE, cptParam(len, t)(ctx))(n)(ctx))(pos, info, errT)
 
-    case (loc: in.Location) :: ctx.Array(len, t) / Shared =>
+    case (loc: in.Location) :: ctx.NoZeroSize(ctx.Array(len, t)) / Shared =>
       val (pos, info, errT) = loc.vprMeta
       for {
         arg <- ctx.reference(loc)
@@ -258,12 +231,15 @@ class ArrayEncoding extends TypeEncoding with SharedArrayEmbedding {
     * i.e. all permissions involved in converting the shared location to an exclusive r-value.
     * An encoding for type T should be defined at all shared locations of type T.
     *
+    * The default implements:
+    * Footprint[loc: T@ if sizeOf(T) == 0] -> [&loc != nil: *T°]
+    *
     * Footprint[loc: [n]T] -> forall idx :: {trigger} 0 <= idx < n ==> Footprint[ loc[idx] ]
     *   where trigger = sh_array_get(Ref[loc], idx, n)
     *
     * We do not use let because (at the moment) Viper does not accept quantified permissions with let expressions.
     */
-  override def addressFootprint(ctx: Context): (in.Location, in.Expr) ==> CodeWriter[vpr.Exp] = {
+  override def addressFootprint(ctx: Context): (in.Location, in.Expr) ==> CodeWriter[vpr.Exp] = super.addressFootprint(ctx).orElse {
     case (loc :: ctx.Array(len, t) / Shared, perm) =>
       val (pos, info, errT) = loc.vprMeta
       val typ = underlyingType(loc.typ)(ctx)
@@ -309,13 +285,16 @@ class ArrayEncoding extends TypeEncoding with SharedArrayEmbedding {
     * */
   private val conversionFunc: FunctionGenerator[ComponentParameter] = new FunctionGenerator[ComponentParameter]{
     def genFunction(t: ComponentParameter)(ctx: Context): vpr.Function = {
+      val info = Source.Parser.Internal
+
       val argType = t.arrayT(Shared)
       // variable name does not matter because it is the only argument
-      val x = in.LocalVar("x", argType)(Source.Parser.Internal)
+      val x = in.LocalVar("x", argType)(info)
+
       val resultType = argType.withAddressability(Exclusive)
       val vResultType = typ(ctx)(resultType)
       // variable name does not matter because it is turned into a vpr.Result
-      val resultVar = in.LocalVar("res", resultType)(Source.Parser.Internal)
+      val resultVar = in.LocalVar("res", resultType)(info)
       val post = pure(equal(ctx)(x, resultVar, x))(ctx).res
         // replace resultVar with vpr.Result
         .transform{ case v: vpr.LocalVar if v.name == resultVar.id => vpr.Result(vResultType)() }
@@ -325,7 +304,7 @@ class ArrayEncoding extends TypeEncoding with SharedArrayEmbedding {
         formalArgs = Vector(variable(ctx)(x)),
         typ = vResultType,
         pres = Vector(
-          pure(addressFootprint(ctx)(x, in.WildcardPerm(Source.Parser.Internal)))(ctx).res,
+          pure(addressFootprint(ctx)(x, in.WildcardPerm(info)))(ctx).res,
           synthesized(termination.DecreasesWildcard(None))("This function is assumed to terminate")
         ),
         posts = Vector(post),
diff --git a/src/main/scala/viper/gobra/translator/encodings/closures/MethodObjectEncoder.scala b/src/main/scala/viper/gobra/translator/encodings/closures/MethodObjectEncoder.scala
index a4a0e7d9b..41a13c19c 100644
--- a/src/main/scala/viper/gobra/translator/encodings/closures/MethodObjectEncoder.scala
+++ b/src/main/scala/viper/gobra/translator/encodings/closures/MethodObjectEncoder.scala
@@ -7,8 +7,9 @@
 package viper.gobra.translator.encodings.closures
 
 import viper.gobra.ast.{internal => in}
+import viper.gobra.reporting.BackTranslator.RichErrorMessage
 import viper.gobra.reporting.BackTranslator.{ErrorTransformer, RichErrorMessage}
-import viper.gobra.reporting.{InterfaceReceiverIsNilReason, MethodObjectGetterPreconditionError, Source}
+import viper.gobra.reporting.{ReceiverIsNilReason, MethodObjectGetterPreconditionError, Source}
 import viper.gobra.translator.Names
 import viper.gobra.translator.context.Context
 import viper.gobra.translator.encodings.interfaces.{InterfaceComponent, InterfaceComponentImpl, InterfaceUtils, PolymorphValueComponent, PolymorphValueComponentImpl, TypeComponent, TypeComponentImpl}
@@ -105,6 +106,6 @@ class MethodObjectEncoder(domain: ClosureDomainEncoder) {
     case e@vprerr.PreconditionInAppFalse(_, _, _) if e causedBy call=>
       val info = m.vprMeta._2.asInstanceOf[Source.Verifier.Info]
       val recvInfo = m.recv.vprMeta._2.asInstanceOf[Source.Verifier.Info]
-      MethodObjectGetterPreconditionError(info).dueTo(InterfaceReceiverIsNilReason(recvInfo))
+      MethodObjectGetterPreconditionError(info).dueTo(ReceiverIsNilReason(recvInfo))
   }
 }
\ No newline at end of file
diff --git a/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncoding.scala
index 377b54000..9cd3eea47 100644
--- a/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncoding.scala
+++ b/src/main/scala/viper/gobra/translator/encodings/combinators/TypeEncoding.scala
@@ -10,7 +10,8 @@ import org.bitbucket.inkytonik.kiama.==>
 import viper.gobra.ast.{internal => in}
 import viper.gobra.ast.internal.theory.Comparability
 import viper.gobra.reporting.BackTranslator.{ErrorTransformer, RichErrorMessage}
-import viper.gobra.reporting.{AssignmentError, DefaultErrorBackTranslator, LoopInvariantNotWellFormedError, MethodContractNotWellFormedError, NoPermissionToRangeExpressionError, Source}
+//  import viper.gobra.reporting.{AssignmentError, DefaultErrorBackTranslator, DerefError, LoopInvariantNotWellFormedError, MethodContractNotWellFormedError, NoPermissionToRangeExpressionError, Source}
+import viper.gobra.reporting.{AssignmentError, DefaultErrorBackTranslator, LoadError, LoopInvariantNotWellFormedError, MethodContractNotWellFormedError, NoPermissionToRangeExpressionError, Source}
 import viper.gobra.theory.Addressability.{Exclusive, Shared}
 import viper.gobra.translator.library.Generator
 import viper.gobra.translator.context.Context
@@ -18,10 +19,11 @@ import viper.gobra.translator.util.ViperWriter.{CodeWriter, MemberWriter}
 import viper.silver.verifier.{errors => vprerr}
 import viper.silver.{ast => vpr}
 
-import scala.annotation.unused
+import scala.annotation.{tailrec, unused}
 
 trait TypeEncoding extends Generator {
 
+  import viper.gobra.translator.encodings.combinators.TypeEncoding._
   import viper.gobra.translator.util.TypePatterns._
   import viper.gobra.translator.util.ViperWriter.CodeLevel._
   import viper.gobra.translator.util.ViperWriter.{MemberLevel => ml}
@@ -121,7 +123,7 @@ trait TypeEncoding extends Generator {
       for {
         footprint <- addressFootprint(ctx)(loc, in.FullPerm(loc.info))
         eq1 <- ctx.equal(loc, in.DfltVal(t.withAddressability(Exclusive))(loc.info))(loc)
-        eq2 <- ctx.equal(in.Ref(loc)(loc.info), in.NilLit(in.PointerT(t, Exclusive))(loc.info))(loc)
+        eq2 <- ctx.equal(in.UncheckedRef(loc)(loc.info), in.NilLit(in.PointerT(t, Exclusive))(loc.info))(loc)
       } yield vpr.Inhale(vpr.And(footprint, vpr.And(eq1, vpr.Not(eq2)(pos, info, errT))(pos, info, errT))(pos, info, errT))(pos, info, errT)
   }
 
@@ -217,7 +219,9 @@ trait TypeEncoding extends Generator {
     * (1) exclusive operations on T, which includes literals and default values
     * (2) shared expression of type T
     * The default implements exclusive local variables and constants with [[variable]] and [[Fixpoint::get]], respectively.
-    * Furthermore, the default implements global exclusive variables and conversions as [T(e: T)] -> [e].
+    * Furthermore, the default implements
+    * [T(e: T)] -> [e]
+    * [loc: T@ if sizeOf(T) == 0] -> assert [&loc != nil: *T°]; [dflt(T°)]
     */
   def expression(ctx: Context): in.Expr ==> CodeWriter[vpr.Exp] = {
     case v: in.GlobalConst if typ(ctx) isDefinedAt v.typ => unit(ctx.fixpoint.get(v)(ctx))
@@ -231,6 +235,11 @@ trait TypeEncoding extends Generator {
       )(pos, info, typ, errT)
       unit(vprExpr)
     case in.Conversion(t2, expr :: t) if typ(ctx).isDefinedAt(t) && typ(ctx).isDefinedAt(t2) => ctx.expression(expr)
+    case (loc: in.Location) :: (t@ctx.ZeroSize()) / Shared if typ(ctx).isDefinedAt(t) =>
+      for {
+        dflt <- ctx.expression(in.DfltVal(t.withAddressability(Exclusive))(loc.info))
+        checked <- checkNotNil(loc, dflt)(ctx)
+      } yield checked
   }
 
   /**
@@ -308,6 +317,22 @@ trait TypeEncoding extends Generator {
       unit(vprExpr)
   }
 
+  /**
+    * Checks whether an L-value is safe, i.e. does not cause a runtime panic due to dereferencing nil.
+    * Instead of checking that a dereference is safe immediately, the encoding checks that usages of l-values are safe.
+    * Usages of L-values are: (1) taking a reference, (2) taking a slice, (3) converting to R-value
+    *
+    * SafeRef[loc: T@] => assert [&loc != nil: *T°]; Ref[loc]
+    */
+  final def safeReference(ctx: Context): in.Location ==> CodeWriter[vpr.Exp] = {
+    val r = reference(ctx); { case loc@r(w) =>
+      for {
+        vprLoc <- w
+        checked <- checkNotNil(loc, vprLoc)(ctx)
+      } yield checked
+    }
+  }
+
   /**
     * Encodes an expression such that substitution is possible.
     * For an expression `e` and a context `K`, the encoding of K[e] is semantically equal to K[x] with x := Value[e].
@@ -328,8 +353,13 @@ trait TypeEncoding extends Generator {
     * Encodes the permissions for all addresses of a shared type,
     * i.e. all permissions involved in converting the shared location to an exclusive r-value.
     * An encoding for type T should be defined at all shared locations of type T.
+    *
+    * The default implements:
+    * Footprint[loc: T@ if sizeOf(T) == 0] -> [&loc != nil: *T°]
     */
-  def addressFootprint(@unused ctx: Context): (in.Location, in.Expr) ==> CodeWriter[vpr.Exp] = PartialFunction.empty
+  def addressFootprint(ctx: Context): (in.Location, in.Expr) ==> CodeWriter[vpr.Exp] = {
+    case (loc :: (t@ctx.ZeroSize()) / Shared, _) if typ(ctx).isDefinedAt(t) => checkNotNil(loc)(ctx)
+  }
 
   /**
     * Encodes whether a value is comparable or not.
@@ -430,7 +460,6 @@ trait TypeEncoding extends Generator {
     }
   }
 
-
   /**
     * Alternative version of `orElse` to simplify delegations to super implementations.
     *
@@ -451,3 +480,52 @@ trait TypeEncoding extends Generator {
     node(pos, info, errT)(ctx)
   }
 }
+
+object TypeEncoding {
+
+  import viper.gobra.translator.util.ViperWriter.{CodeLevel => cl}
+
+  /**
+    * Checks whether an L-value is safe, i.e. does not cause a runtime panic due to dereferencing nil.
+    *
+    * assert [&loc != nil: *T°]; res
+    *
+    */
+  final def checkNotNil(loc: in.Location, res: vpr.Exp)(ctx: Context): CodeWriter[vpr.Exp] = {
+    if (cannotBeNil(loc)) cl.unit(res)
+    else {
+      for {
+        cond <- checkNotNil(loc)(ctx)
+        checked <- cl.assertWithDefaultReason(cond, res, LoadError)(ctx)
+      } yield checked
+    }
+  }
+
+  /**
+    * Checks whether an L-value is safe, i.e. does not cause a runtime panic due to dereferencing nil.
+    *
+    * [&loc != nil: *T°]
+    *
+    */
+  final def checkNotNil(loc: in.Location)(ctx: Context): CodeWriter[vpr.Exp] = {
+
+    val annotatedInfo = loc.info.asInstanceOf[Source.Parser.Single].createAnnotatedInfo(Source.ReceiverNotNilCheckAnnotation)
+    val (pos, info, errT) = loc.vprMeta
+
+    if (cannotBeNil(loc)) cl.unit(vpr.TrueLit()(pos, info, errT))
+    else {
+      ctx.expression(in.UneqCmp(
+        in.UncheckedRef(loc)(annotatedInfo),
+        in.NilLit(in.PointerT(loc.typ, Exclusive))(annotatedInfo)
+      )(annotatedInfo))
+    }
+  }
+
+  @tailrec
+  private def cannotBeNil(l: in.Expr): Boolean = l match {
+    case _: in.Var => true
+    case l: in.FieldRef => cannotBeNil(l.recv)
+    case l: in.IndexedExp => cannotBeNil(l.base)
+    case _ => false
+  }
+}
diff --git a/src/main/scala/viper/gobra/translator/encodings/interfaces/TypeComponentImpl.scala b/src/main/scala/viper/gobra/translator/encodings/interfaces/TypeComponentImpl.scala
index 10fd1d691..195a46fbc 100644
--- a/src/main/scala/viper/gobra/translator/encodings/interfaces/TypeComponentImpl.scala
+++ b/src/main/scala/viper/gobra/translator/encodings/interfaces/TypeComponentImpl.scala
@@ -33,7 +33,7 @@ class TypeComponentImpl extends TypeComponent {
     case Float64HD => "float64"
     case StringHD => "string"
     case PointerHD => "pointer"
-    case ArrayHD => "array"
+    case ArrayHD(n) => s"array$n"
     case SliceHD => "slice"
     case MapHD => "map"
     case ChannelHD => "channel"
@@ -336,15 +336,7 @@ class TypeComponentImpl extends TypeComponent {
 
   /** Translates Gobra types into Viper type expressions. */
   override def typeToExpr(typ: in.Type)(pos: vpr.Position = vpr.NoPosition, info: vpr.Info = vpr.NoInfo, errT: vpr.ErrorTrafo = vpr.NoTrafos)(ctx: Context): vpr.Exp = {
-    def go(typ: in.Type): vpr.Exp = typeToExpr(typ)(pos, info, errT)(ctx)
-
-    typ match {
-      case t: in.ArrayT =>
-        typeApp(typeHead(t), Vector(vpr.IntLit(t.length)(pos, info, errT), go(t.elems)))(pos, info, errT)(ctx)
-
-      case t =>
-        typeApp(typeHead(t), children(t) map go)(pos, info, errT)(ctx)
-    }
+    typeApp(typeHead(typ), children(typ) map (typeToExpr(_)(pos, info, errT)(ctx)))(pos, info, errT)(ctx)
   }
 
   /** Generates precise equality axioms for 'typ'. */
@@ -352,11 +344,7 @@ class TypeComponentImpl extends TypeComponent {
 
     typeTree(typ).toVector foreach { hd => arity(hd) match {
       case 0 => // already precise
-      case 1 if hd == ArrayHD =>
-        genPreciseEqualityAxioms(hd, Vector(vpr.Int, domainType))(ctx)
-
-      case n =>
-        genPreciseEqualityAxioms(hd, (0 until n).toVector map (_ => domainType))(ctx)
+      case n => genPreciseEqualityAxioms(hd, (0 until n).toVector map (_ => domainType))(ctx)
     }}
   }
 
diff --git a/src/main/scala/viper/gobra/translator/encodings/programs/ProgramsImpl.scala b/src/main/scala/viper/gobra/translator/encodings/programs/ProgramsImpl.scala
index b47a3aa74..4d7ab1581 100644
--- a/src/main/scala/viper/gobra/translator/encodings/programs/ProgramsImpl.scala
+++ b/src/main/scala/viper/gobra/translator/encodings/programs/ProgramsImpl.scala
@@ -25,7 +25,7 @@ class ProgramsImpl extends Programs {
 
     def goM(member: in.Member): MemberWriter[(Vector[vpr.Member], Context)] = {
       /** we use a separate context for each member in order to reset the fresh counter */
-      val ctx = mainCtx := (initialFreshCounterValueN = 0)
+      val ctx = mainCtx := (initialFreshCounterValueN = Some(0))
       ctx.member(member).map(m => (m, ctx))
     }
 
diff --git a/src/main/scala/viper/gobra/translator/encodings/slices/SliceEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/slices/SliceEncoding.scala
index 5590c54f7..69cdc8db8 100644
--- a/src/main/scala/viper/gobra/translator/encodings/slices/SliceEncoding.scala
+++ b/src/main/scala/viper/gobra/translator/encodings/slices/SliceEncoding.scala
@@ -70,8 +70,8 @@ class SliceEncoding(arrayEmb : SharedArrayEmbedding) extends LeafTypeEncoding {
     * R[ nil: []T° ] -> nilSlice()
     * R[ len(e: []T) ] -> slen([e])
     * R[ cap(e: []T) ] -> scap([e])
-    * R[ (e: [n]T@)[e1:e2] ] -> sliceFromArray([e], [e1], [e2])
-    * R[ (e: [n]T@)[e1:e2:e3] ] -> fullSliceFromArray([e], [e1], [e2], [e3])
+    * R[ (e: [n]T@)[e1:e2] ] -> sliceFromArray(SafeRef[e], [e1], [e2])
+    * R[ (e: [n]T@)[e1:e2:e3] ] -> fullSliceFromArray(SafeRef[e], [e1], [e2], [e3])
     * R[ (e: []T@)[e1:e2] ] -> sliceFromSlice([e], [e1], [e2])
     * R[ (e: []T@)[e1:e2:e3] ] -> fullSliceFromSlice([e], [e1], [e2], [e3])
     *
@@ -97,7 +97,7 @@ class SliceEncoding(arrayEmb : SharedArrayEmbedding) extends LeafTypeEncoding {
       } yield withSrc(ctx.slice.cap(expT), exp)
 
       case exp @ in.Slice((base : in.Location) :: ctx.Array(_, _) / Shared, low, high, max, _) => for {
-        baseT <- ctx.reference(base)
+        baseT <- ctx.safeReference(base)
         baseType = base.typ.asInstanceOf[in.ArrayT]
         unboxedBaseT = arrayEmb.unbox(baseT, baseType)(base)(ctx)
         lowT <- goE(low)
diff --git a/src/main/scala/viper/gobra/translator/encodings/structs/SharedStructComponent.scala b/src/main/scala/viper/gobra/translator/encodings/structs/SharedStructComponent.scala
index 7d7e9a7ea..229bfa2d1 100644
--- a/src/main/scala/viper/gobra/translator/encodings/structs/SharedStructComponent.scala
+++ b/src/main/scala/viper/gobra/translator/encodings/structs/SharedStructComponent.scala
@@ -31,7 +31,7 @@ trait SharedStructComponent extends Generator {
     * All permissions involved in the conversion should be returned by [[addressFootprint]].
     *
     * The default implementation is:
-    * Convert[loc: Struct{F}@] -> create_ex_struct( R[loc.f] | f in F )
+    * Convert[loc: Struct{F}@] -> create_ex_struct( [loc.f] | f in F )
     */
   def convertToExclusive(loc: in.Location)(ctx: Context, ex: ExclusiveStructComponent): CodeWriter[vpr.Exp] = {
     loc match {
@@ -54,7 +54,6 @@ trait SharedStructComponent extends Generator {
     * i.e. all permissions involved in converting the shared location to an exclusive value ([[convertToExclusive]]).
     * An encoding for type T should be defined at all shared locations of type T.
     *
-    * The default implementation is:
     * Footprint[loc: Struct{F}@] -> AND f in F: Footprint[loc.f]
     */
   def addressFootprint(loc: in.Location, perm: in.Expr)(ctx: Context): CodeWriter[vpr.Exp] = {
diff --git a/src/main/scala/viper/gobra/translator/encodings/structs/StructEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/structs/StructEncoding.scala
index f3f4e78e2..8209a9c08 100644
--- a/src/main/scala/viper/gobra/translator/encodings/structs/StructEncoding.scala
+++ b/src/main/scala/viper/gobra/translator/encodings/structs/StructEncoding.scala
@@ -99,13 +99,13 @@ class StructEncoding extends TypeEncoding {
     * [loc: T@ = rhs] -> exhale Footprint[loc]; inhale Footprint[loc] && [loc == rhs]
     *
     * [e.f: Struct{F}° = rhs] -> [ e = e[f := rhs] ]
-    * [lhs: Struct{F}@ = rhs] -> FOREACH f in F: [lhs.f = rhs.f]
+    * [lhs: Struct{F}@ = rhs if size != 0] -> FOREACH f in F: [lhs.f = rhs.f]
     */
   override def assignment(ctx: Context): (in.Assignee, in.Expr, in.Node) ==> CodeWriter[vpr.Stmt] = default(super.assignment(ctx)){
     case (in.Assignee((fa: in.FieldRef) :: _ / Exclusive), rhs, src) =>
       ctx.assignment(in.Assignee(fa.recv), in.StructUpdate(fa.recv, fa.field, rhs)(src.info))(src)
 
-    case (in.Assignee(lhs :: ctx.Struct(lhsFs) / Shared), rhs :: ctx.Struct(rhsFs), src) =>
+    case (in.Assignee(lhs :: ctx.NoZeroSize(ctx.Struct(lhsFs)) / Shared), rhs :: ctx.Struct(rhsFs), src) =>
       for {
         x <- bind(lhs)(ctx)
         y <- bind(rhs)(ctx)
@@ -125,22 +125,15 @@ class StructEncoding extends TypeEncoding {
     * [lhs: T == rhs: T] -> [lhs] == [rhs]
     * [lhs: *T° == rhs: *T] -> [lhs] == [rhs]
     *
-    * [(lhs: Struct{F}) == rhs: Struct{_}] -> AND f in F: [lhs.f == rhs.f] (NOTE: f ranges over actual & ghost fields since `equal` corresponds to ghost comparison)
-    * // According to the Go spec, pointers to distinct zero-sized data may or may not be equal. Thus:
-    * [(x: *Struct{}°) == x: *Struct{}] -> true
-    * [(lhs: *Struct{}°) == rhs: *Struct{}] -> unknown()
-    * [(lhs: *Struct{F}°) == rhs: *Struct{_}] -> [lhs] == [rhs]
+    * [(lhs: Struct{F}) == rhs: Struct{_}] -> AND f in F: [lhs.f == rhs.f]
     */
-  override def equal(ctx: Context): (in.Expr, in.Expr, in.Node) ==> CodeWriter[vpr.Exp] = structEqual(ctx, useGoEquality = false) orElse {
-    case (lhs :: ctx.*(ctx.Struct(lhsFs)) / Exclusive, rhs :: ctx.*(ctx.Struct(_)), src) =>
-      if (lhsFs.isEmpty) {
-        unit(withSrc(if (lhs == rhs) vpr.TrueLit() else ctx.unknownValue.unkownValue(vpr.Bool), src))
-      } else {
-        for {
-          vLhs <- ctx.expression(lhs)
-          vRhs <- ctx.expression(rhs)
-        } yield withSrc(vpr.EqCmp(vLhs, vRhs), src)
-      }
+  override def equal(ctx: Context): (in.Expr, in.Expr, in.Node) ==> CodeWriter[vpr.Exp] = default(super.equal(ctx)){
+    case (lhs :: ctx.Struct(lhsFs), rhs :: ctx.Struct(rhsFs), src) =>
+      val lhsFAccs = fieldAccesses(lhs, lhsFs)
+      val rhsFAccs = fieldAccesses(rhs, rhsFs)
+      val equalFields = sequence((lhsFAccs zip rhsFAccs).map{ case (lhsFA, rhsFA) => ctx.equal(lhsFA, rhsFA)(src) })
+      val (pos, info, errT) = src.vprMeta
+      equalFields.map(VU.bigAnd(_)(pos, info, errT))
   }
 
   /**
@@ -188,7 +181,7 @@ class StructEncoding extends TypeEncoding {
     * R[ (base: Struct{F})[f = e] ] -> ex_struct_upd([base], f, [e], F)
     * R[ dflt(Struct{F}) ] -> create_ex_struct( [T] | (f: T) in F )
     * R[ structLit(E) ] -> create_ex_struct( [e] | e in E )
-    * R[ loc: Struct{F}@ ] -> convert_to_exclusive( Ref[loc] )
+    * R[ loc: Struct{F}@ ] -> convert_to_exclusive( Ref[loc] ) // assert [&loc != nil] if Struct{F} has size zero
     */
   override def expression(ctx: Context): in.Expr ==> CodeWriter[vpr.Exp] = default(super.expression(ctx)){
     case (loc@ in.FieldRef(recv :: ctx.Struct(fs), field)) :: _ / Exclusive =>
@@ -216,7 +209,7 @@ class StructEncoding extends TypeEncoding {
       val fieldExprs = lit.args.map(arg => ctx.expression(arg))
       sequence(fieldExprs).map(ex.create(_, cptParam(fs)(ctx))(lit)(ctx))
 
-    case (loc: in.Location) :: ctx.Struct(_) / Shared =>
+    case (loc: in.Location) :: ctx.NoZeroSize(ctx.Struct(_)) / Shared =>
       sh.convertToExclusive(loc)(ctx, ex)
   }
 
@@ -240,8 +233,13 @@ class StructEncoding extends TypeEncoding {
     * Encodes the permissions for all addresses of a shared type,
     * i.e. all permissions involved in converting the shared location to an exclusive r-value.
     * An encoding for type T should be defined at all shared locations of type T.
+    *
+    * The default implements:
+    * Footprint[loc: T@ if sizeOf(T) == 0] -> [&loc != nil: *T°]
+    *
+    * Footprint[loc: Struct{F}@] -> AND f in F: Footprint[loc.f]
     */
-  override def addressFootprint(ctx: Context): (in.Location, in.Expr) ==> CodeWriter[vpr.Exp] = {
+  override def addressFootprint(ctx: Context): (in.Location, in.Expr) ==> CodeWriter[vpr.Exp] = super.addressFootprint(ctx).orElse {
     case (loc :: ctx.Struct(_) / Shared, perm) => sh.addressFootprint(loc, perm)(ctx)
   }
 
@@ -292,7 +290,7 @@ class StructEncoding extends TypeEncoding {
       val src = in.DfltVal(resType)(Source.Parser.Internal)
       // variable name does not matter because it is turned into a vpr.Result
       val resDummy = in.LocalVar("res", resType)(src.info)
-      val resFAccs = fs.map(f => in.Ref(in.FieldRef(resDummy, f)(src.info))(src.info))
+      val resFAccs = fs.map(f => in.UncheckedRef(in.FieldRef(resDummy, f)(src.info))(src.info))
       val fieldEq = resFAccs map (f => ctx.equal(f, in.DfltVal(f.typ)(src.info))(src))
       // termination measure
       val pre = synthesized(termination.DecreasesWildcard(None))("This function is assumed to terminate")
diff --git a/src/main/scala/viper/gobra/translator/encodings/typeless/MemoryEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/typeless/MemoryEncoding.scala
index b5149518a..4a4b1a558 100644
--- a/src/main/scala/viper/gobra/translator/encodings/typeless/MemoryEncoding.scala
+++ b/src/main/scala/viper/gobra/translator/encodings/typeless/MemoryEncoding.scala
@@ -16,7 +16,8 @@ import viper.silver.{ast => vpr}
 class MemoryEncoding extends Encoding {
 
   override def expression(ctx: Context): in.Expr ==> CodeWriter[vpr.Exp] = {
-    case r: in.Ref => ctx.reference(r.ref.op)
+    case r: in.UncheckedRef => ctx.reference(r.ref.op)
+    case r: in.Ref => ctx.safeReference(r.ref.op)
     case x@ in.EqCmp(l, r) => ctx.goEqual(l, r)(x)
     case x@ in.UneqCmp(l, r) => ctx.goEqual(l, r)(x).map(v => withSrc(vpr.Not(v), x))
     case x@ in.GhostEqCmp(l, r) => ctx.equal(l, r)(x)
diff --git a/src/main/scala/viper/gobra/translator/util/TypePatterns.scala b/src/main/scala/viper/gobra/translator/util/TypePatterns.scala
index dec73f083..71bc6446c 100644
--- a/src/main/scala/viper/gobra/translator/util/TypePatterns.scala
+++ b/src/main/scala/viper/gobra/translator/util/TypePatterns.scala
@@ -6,6 +6,7 @@
 
 package viper.gobra.translator.util
 
+import viper.gobra.ast.internal.theory.TypeHead.isZeroSize
 import viper.gobra.ast.{internal => in}
 import viper.gobra.theory.Addressability
 import viper.gobra.theory.Addressability.{Exclusive, Shared}
@@ -238,6 +239,18 @@ object TypePatterns {
         case _ => None
       }
     }
+
+    object ZeroSize {
+      def unapply(arg: in.Type): Boolean =
+        isZeroSize(underlyingType(arg)(ctx))(ctx.table)
+    }
+
+    object NoZeroSize {
+      def unapply(arg: in.Type): Option[in.Type] = underlyingType(arg)(ctx) match {
+        case ctx.ZeroSize() => None
+        case t => Some(t)
+      }
+    }
   }
 
 
diff --git a/src/main/scala/viper/gobra/translator/util/ViperWriter.scala b/src/main/scala/viper/gobra/translator/util/ViperWriter.scala
index c5387b74b..50496afcd 100644
--- a/src/main/scala/viper/gobra/translator/util/ViperWriter.scala
+++ b/src/main/scala/viper/gobra/translator/util/ViperWriter.scala
@@ -418,6 +418,13 @@ object ViperWriter {
       } yield call
     }
 
+    /* Can be used in expressions. */
+    def assertWithDefaultReason(cond: vpr.Exp, exp: vpr.Exp, error: Source.Verifier.Info => VerificationError)(ctx: Context): Writer[vpr.Exp] = {
+      // In the future, this might do something more sophisticated
+      val (res, errT) = ctx.condition.assert(cond, exp, (info, reason) => error(info) dueTo DefaultErrorBackTranslator.defaultTranslate(reason))
+      errorT(errT).map(_ => res)
+    }
+
     /* Emits Viper statements. */
     def assert(cond: vpr.Exp, reasonT: (Source.Verifier.Info, ErrorReason) => VerificationError): Writer[Unit] = {
       val res = vpr.Assert(cond)(cond.pos, cond.info, cond.errT)
diff --git a/src/test/resources/regressions/features/closures/closures-recursion2-mutual.gobra b/src/test/resources/regressions/features/closures/closures-recursion2-mutual.gobra
index 6e4ce0e07..c186bdb57 100644
--- a/src/test/resources/regressions/features/closures/closures-recursion2-mutual.gobra
+++ b/src/test/resources/regressions/features/closures/closures-recursion2-mutual.gobra
@@ -1,3 +1,5 @@
+//:: IgnoreFile(/gobra/issue/532/)
+
 // Any copyright is dedicated to the Public Domain.
 // http://creativecommons.org/publicdomain/zero/1.0/
 
diff --git a/src/test/resources/regressions/features/termination/termination-fail-02.gobra b/src/test/resources/regressions/features/termination/termination-fail-02.gobra
index ed5df003e..16ea1db32 100644
--- a/src/test/resources/regressions/features/termination/termination-fail-02.gobra
+++ b/src/test/resources/regressions/features/termination/termination-fail-02.gobra
@@ -6,8 +6,7 @@
 package termination
 
 type Func interface {
-    //:: ExpectedOutput(pure_function_termination_error)
-    //:: ExpectedOutput(postcondition_error:assertion_error)
+	//:: ExpectedOutput(pure_function_termination_error)
 	pure
 	decreases n
 	requires a != nil
diff --git a/src/test/resources/regressions/issues/000491-2.gobra b/src/test/resources/regressions/issues/000491-2.gobra
new file mode 100644
index 000000000..34828beda
--- /dev/null
+++ b/src/test/resources/regressions/issues/000491-2.gobra
@@ -0,0 +1,16 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package main
+
+type Pair struct {
+	x int
+	y int
+}
+
+func f(p *Pair) (r *int) {
+	//:: ExpectedOutput(load_error:receiver_is_nil_error)
+	r = &p.x
+	return
+}
+
diff --git a/src/test/resources/regressions/issues/000491.gobra b/src/test/resources/regressions/issues/000491.gobra
new file mode 100644
index 000000000..7b3300c38
--- /dev/null
+++ b/src/test/resources/regressions/issues/000491.gobra
@@ -0,0 +1,73 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package main
+
+type A struct {
+	x int
+}
+
+func test1() {
+	var x *A
+	//:: ExpectedOutput(load_error:receiver_is_nil_error)
+	var y *A = &(*x)
+}
+
+func test2() {
+	var x *[3]int
+	//:: ExpectedOutput(load_error:receiver_is_nil_error)
+	var y []int = (*x)[:]
+}
+
+requires x != nil
+func test3(x *struct{}) {
+	v := *x
+
+	//:: ExpectedOutput(assert_error:assertion_error)
+	assert false
+}
+
+requires x != nil
+func test4(x *[0]int) {
+	v := *x
+
+	//:: ExpectedOutput(assert_error:assertion_error)
+	assert false
+}
+
+func test5(x *struct{}) {
+	//:: ExpectedOutput(load_error:receiver_is_nil_error)
+	v := *x
+}
+
+func test6(x *[0]int) {
+	//:: ExpectedOutput(load_error:receiver_is_nil_error)
+	v := *x
+}
+
+func test7(x, y *struct{}) {
+	//:: ExpectedOutput(assert_error:assertion_error)
+	assert x == y
+}
+
+func test8(x, y *[0]int) {
+	//:: ExpectedOutput(assert_error:assertion_error)
+	assert x == y
+}
+
+func test9(x *struct{}) {
+	//:: ExpectedOutput(assignment_error:receiver_is_nil_error)
+	*x = struct{}{}
+}
+
+func test10(x *[0]int) {
+	//:: ExpectedOutput(assignment_error:receiver_is_nil_error)
+	*x = [0]int{}
+}
+
+func test11() {
+	var x *[10]int
+
+	//:: ExpectedOutput(load_error:receiver_is_nil_error)
+	assert len(*x) == 10
+}
\ No newline at end of file