diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md
index 7adc8dd0f..b6170942f 100644
--- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md
+++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md
@@ -269,7 +269,11 @@ A `Deref` projection in the projections list changes the target of the write ope
STACK
=> STACK[(FRAME -Int 1) <-
- #updateStackLocal({STACK[FRAME -Int 1]}:>StackFrame, I, #buildUpdate(NEW, CONTEXTS))
+ #updateStackLocal(
+ {STACK[FRAME -Int 1]}:>StackFrame,
+ I,
+ #adjustRef(#buildUpdate(NEW, CONTEXTS), 0 -Int FRAME)
+ )
]
requires 0
STACK
=> STACK[(FRAME -Int 1) <-
- #updateStackLocal({STACK[FRAME -Int 1]}:>StackFrame, I, #buildUpdate(Moved, CONTEXTS)) // TODO retain Ty and Mutability from _ORIGINAL
+ #updateStackLocal(
+ {STACK[FRAME -Int 1]}:>StackFrame,
+ I,
+ #adjustRef(#buildUpdate(Moved, CONTEXTS), 0 -Int FRAME)
+ ) // TODO retain Ty and Mutability from _ORIGINAL
]
requires 0 (dst: &mut &'a i32, src: &&'a i32) {
+ *dst = *src;
+}
+
+fn main() {
+ let x = 1;
+ let mut dst = &x;
+ let src = dst;
+
+ assign(&mut dst, &src);
+
+ assert_eq!(*dst, 1);
+}