diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md
index 9fd89c6a9..ed9194065 100644
--- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md
+++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md
@@ -1456,6 +1456,45 @@ What can be supported without additional layout consideration is trivial casts b
       requires lookupTy(TY_SOURCE) ==K lookupTy(TY_TARGET)
 ```
 
+Transmuting a pointer to an integer discards provenance and reinterprets the pointer’s offset as a value of the target integer type.
+
+```k
+  syntax Int ::= #ptrOffsetBytes ( Int , MaybeTy ) [function, total]
+  rule #ptrOffsetBytes(PTR_OFFSET, _TY:Ty) => 0
+    requires PTR_OFFSET ==Int 0
+  rule #ptrOffsetBytes(PTR_OFFSET, TY:Ty)
+    => PTR_OFFSET *Int #elemSize(#lookupMaybeTy(elemTy(lookupTy(TY))))
+    requires PTR_OFFSET =/=Int 0
+     andBool #isArrayType(lookupTy(TY))
+  rule #ptrOffsetBytes(_, _) => -1 [owise] // should not happen
+
+  syntax Bool ::= #isArrayType ( TypeInfo ) [function, total]
+  rule #isArrayType(typeInfoArrayType(_, _)) => true
+  rule #isArrayType(_) => false [owise]
+```
+
+```k
+  rule <k> #cast(
+              PtrLocal(_, _, _, metadata(_, PTR_OFFSET, _)),
+              castKindTransmute,
+              TY_SOURCE,
+              TY_TARGET
+            )
+          =>
+            #intAsType(
+              #ptrOffsetBytes(
+                PTR_OFFSET,
+                pointeeTy(#lookupMaybeTy(TY_SOURCE))
+              ),
+              #bitWidth(#numTypeOf(lookupTy(TY_TARGET))),
+              #numTypeOf(lookupTy(TY_TARGET))
+            )
+          ...
+        </k>
+      requires #isIntType(lookupTy(TY_TARGET))
+       andBool 0 <=Int #ptrOffsetBytes(PTR_OFFSET,pointeeTy(#lookupMaybeTy(TY_SOURCE)))
+```
+
 Other `Transmute` casts that can be resolved are round-trip casts from type A to type B and then directly back from B to A.
 The first cast is reified as a `thunk`, the second one resolves it and eliminates the `thunk`:
 
diff --git a/kmir/src/tests/integration/data/prove-rs/show/interior-mut3-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/interior-mut3-fail.main.expected
index 5d1bd2ecc..80793fa28 100644
--- a/kmir/src/tests/integration/data/prove-rs/show/interior-mut3-fail.main.expected
+++ b/kmir/src/tests/integration/data/prove-rs/show/interior-mut3-fail.main.expected
@@ -3,57 +3,11 @@
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │   span: 0
 │
-│  (151 steps)
-├─ 3
-│   #expect ( thunk ( #applyBinOp ( binOpEq , thunk ( #applyBinOp ( binOpBitAnd , th
-│   function: main
-┃
-┃ (1 step)
-┣━━┓
-┃  │
-┃  ├─ 4
-┃  │   AssertError ( assertMessageMisalignedPointerDereference ( ... required: operandC
-┃  │   function: main
-┃  │
-┃  │  (1 step)
-┃  └─ 6 (stuck, leaf)
-┃      #ProgramError ( AssertError ( assertMessageMisalignedPointerDereference ( ... re
-┃      function: main
-┃
-┗━━┓
-   │
-   ├─ 5
-   │   #execBlockIdx ( basicBlockIdx ( 8 ) ) ~> .K
-   │   function: main
-   │
-   │  (111 steps)
-   ├─ 7
-   │   #expect ( thunk ( #applyBinOp ( binOpEq , thunk ( #applyBinOp ( binOpBitAnd , th
-   │   function: main
-   ┃
-   ┃ (1 step)
-   ┣━━┓
-   ┃  │
-   ┃  ├─ 8
-   ┃  │   AssertError ( assertMessageMisalignedPointerDereference ( ... required: operandC
-   ┃  │   function: main
-   ┃  │
-   ┃  │  (1 step)
-   ┃  └─ 10 (stuck, leaf)
-   ┃      #ProgramError ( AssertError ( assertMessageMisalignedPointerDereference ( ... re
-   ┃      function: main
-   ┃
-   ┗━━┓
-      │
-      ├─ 9
-      │   #execBlockIdx ( basicBlockIdx ( 7 ) ) ~> .K
-      │   function: main
-      │
-      │  (17 steps)
-      └─ 11 (stuck, leaf)
-          #setLocalValue ( place ( ... local: local ( 1 ) , projection: .ProjectionElems )
-          function: main
-          span: 79
+│  (281 steps)
+└─ 3 (stuck, leaf)
+    #setLocalValue ( place ( ... local: local ( 1 ) , projection: .ProjectionElems )
+    function: main
+    span: 79
 
 
 ┌─ 2 (root, leaf, target, terminal)