diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/MemsafetyPass.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/MemsafetyPass.kt
index 923dd78c56..f05bdbedd3 100644
--- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/MemsafetyPass.kt
+++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/MemsafetyPass.kt
@@ -208,7 +208,11 @@ class MemsafetyPass(val parseContext: ParseContext) : ProcedurePass {
         ?: XcfaGlobalVar(Var("__ptr", sizeVar.type.indexType), pointerType.nullValue)
           .also { builder.parent.addVar(it) }
           .wrappedVar
-    val remained = Gt(ArrayReadExpr.create<Type, Type>(sizeVar.ref, anyBase.ref), fitsall.nullValue)
+    val remained = // 3k+0: malloc
+      Gt(
+        ArrayReadExpr.create<Type, Type>(sizeVar.ref, Mul(anyBase.ref, pointerType.getValue("3"))),
+        fitsall.nullValue,
+      )
 
     for (incomingEdge in LinkedHashSet(finalLoc.incomingEdges)) {
       builder.removeEdge(incomingEdge)
diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ReferenceElimination.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ReferenceElimination.kt
index 8ce6c2f606..5fc074d697 100644
--- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ReferenceElimination.kt
+++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ReferenceElimination.kt
@@ -69,7 +69,15 @@ class ReferenceElimination(val parseContext: ParseContext) : ProcedurePass {
             builder.parent.addVar(XcfaGlobalVar(varDecl, lit))
             parseContext.metadata.create(varDecl.ref, "cType", ptrType)
             val assign = AssignStmtLabel(varDecl, lit)
-            Pair(varDecl, SequenceLabel(listOf(assign)))
+            val labels =
+              if (MemsafetyPass.NEED_CHECK) {
+                val assign2 = builder.parent.allocateUnit(parseContext, varDecl.ref)
+
+                listOf(assign, assign2)
+              } else {
+                listOf(assign)
+              }
+            Pair(varDecl, SequenceLabel(labels))
           }
       }
     checkState(globalReferredVars is Map<*, *>, "ReferenceElimination needs info on references")