diff --git a/kmir/src/kmir/kdist/mir-semantics/intrinsics.md b/kmir/src/kmir/kdist/mir-semantics/intrinsics.md
index f95c90d6a..4fbd84645 100644
--- a/kmir/src/kmir/kdist/mir-semantics/intrinsics.md
+++ b/kmir/src/kmir/kdist/mir-semantics/intrinsics.md
@@ -53,6 +53,29 @@ before it's used. They have no effect on program semantics, and are implemented
   rule <k> #execIntrinsic(IntrinsicFunction(symbol("prefetch_write_instruction")), _ARG1:Operand _ARG2:Operand .Operands, _DEST) => .K ... </k>
 ```
 
+#### Assert Inhabited (`std::intrinsics::assert_inhabited`)
+
+The `assert_inhabited` instrinsic asserts that a type is "inhabited" (able to be instantiated). Types such as
+`Never` (`!`) cannot be instantiated and are uninhabited types. The target / codegen decides how to handle this
+intrinsic, it is not required to panic if the type is not inhabited, it could also perform a NO OP. We have witnessed
+in the case that there is an uninhabited type that the following basic block is `noBasicBlockIdx`, and so we
+error with `#AssertInhabitedFailure` if we see that following the intrinsic. Otherwise, we perform a NO OP.
+
+```k
+  syntax MIRError ::= "AssertInhabitedFailure"
+  rule <k> #execIntrinsic(IntrinsicFunction(symbol("assert_inhabited")), .Operands, _DEST)
+            ~> #continueAt(noBasicBlockIdx)
+        => AssertInhabitedFailure
+       ...
+      </k>
+
+  rule <k> #execIntrinsic(IntrinsicFunction(symbol("assert_inhabited")), .Operands, _DEST)
+        => .K
+       ...
+      </k>
+      [owise]
+```
+
 #### Raw Eq (`std::intrinsics::raw_eq`)
 
 The `raw_eq` intrinsic performs byte-by-byte equality comparison of the memory contents pointed to by two references.
diff --git a/kmir/src/tests/integration/data/prove-rs/assert-inhabited-fail.rs b/kmir/src/tests/integration/data/prove-rs/assert-inhabited-fail.rs
new file mode 100644
index 000000000..d459c9f60
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/assert-inhabited-fail.rs
@@ -0,0 +1,9 @@
+#![feature(core_intrinsics)]
+#![feature(never_type)]
+use std::intrinsics::assert_inhabited;
+
+fn main() {
+    std::hint::black_box(
+        assert_inhabited::<!>() // Up to compiler/CodegenBackend to panic or NOOP
+    );
+}
diff --git a/kmir/src/tests/integration/data/prove-rs/intrinsics.rs b/kmir/src/tests/integration/data/prove-rs/intrinsics.rs
index fb8a2d0c1..e3a6da659 100644
--- a/kmir/src/tests/integration/data/prove-rs/intrinsics.rs
+++ b/kmir/src/tests/integration/data/prove-rs/intrinsics.rs
@@ -1,5 +1,5 @@
 #![feature(core_intrinsics)]
-use std::intrinsics;
+use std::intrinsics::{self, assert_inhabited};
 
 fn main() {
     intrinsics::cold_path();
@@ -7,6 +7,10 @@ fn main() {
     intrinsics::likely(b);
     intrinsics::unlikely(b);
     prefetch();
+    assert_inhabited::<i32>(); // Up to compiler/CodegenBackend to panic or NOOP
+    std::hint::black_box(
+        assert_inhabited::<()>() // Trying to stop being optimised away
+    );
 }
 
 fn prefetch() {
diff --git a/kmir/src/tests/integration/data/prove-rs/iterator-simple-fail.rs b/kmir/src/tests/integration/data/prove-rs/iterator-simple-fail.rs
new file mode 100644
index 000000000..ee9b6bce3
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/iterator-simple-fail.rs
@@ -0,0 +1,7 @@
+fn main() {
+    let arr = [1];
+
+    for elem in arr {
+        assert!(elem != 0);
+    }
+}
\ No newline at end of file
diff --git a/kmir/src/tests/integration/data/prove-rs/show/assert-inhabited-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/assert-inhabited-fail.main.expected
new file mode 100644
index 000000000..f0468d340
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/show/assert-inhabited-fail.main.expected
@@ -0,0 +1,15 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: 0
+│
+│  (8 steps)
+└─ 3 (stuck, leaf)
+    #ProgramError ( AssertInhabitedFailure ) ~> .K
+    function: main
+
+
+┌─ 2 (root, leaf, target, terminal)
+│   #EndProgram ~> .K
+
+
diff --git a/kmir/src/tests/integration/data/prove-rs/show/iterator-simple-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/iterator-simple-fail.main.expected
new file mode 100644
index 000000000..bd2f040cd
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/show/iterator-simple-fail.main.expected
@@ -0,0 +1,15 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: 0
+│
+│  (487 steps)
+└─ 3 (stuck, leaf)
+    #traverseProjection ( toLocal ( 24 ) , thunk ( #cast ( PtrLocal ( 1 , place ( ..
+    span: 219
+
+
+┌─ 2 (root, leaf, target, terminal)
+│   #EndProgram ~> .K
+
+
diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-0.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-0.expected
index 0c9a838cd..623683966 100644
--- a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-0.expected
+++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-0.expected
@@ -1,6 +1,6 @@
 <kmir>
   <k>
-    #execIntrinsic ( IntrinsicFunction ( symbol ( "assert_inhabited" ) ) , .Operands , place (... local: local ( 23 ) , projection: .ProjectionElems ) ) ~> #continueAt ( someBasicBlockIdx ( basicBlockIdx ( 8 ) ) ) ~> .K
+    #traverseProjection ( toLocal ( 24 ) , thunk ( #cast ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , castKindPtrToPtr , ty ( 53 ) , ty ( 54 ) ) ) , projectionElemDeref  .ProjectionElems , .Contexts ) ~> #readProjection ( false ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindStorageDead ( local ( 24 ) ) , span: span ( 299 ) )  statement (... kind: statementKindStorageDead ( local ( 17 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 16 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 25 ) ) , span: span ( 300 ) )  statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueAggregate ( aggregateKindAdt ( adtDef ( 15 ) , variantIdx ( 1 ) , genericArgKindType ( ty ( 23 ) )  .GenericArgs , noUserTypeAnnotationIndex , noFieldIdx ) , operandMove ( place (... local: local ( 15 ) , projection: .ProjectionElems ) )  .Operands ) ) , span: span ( 301 ) )  statement (... kind: statementKindStorageDead ( local ( 15 ) ) , span: span ( 295 ) )  .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindGoto (... target: basicBlockIdx ( 5 ) ) , span: span ( 295 ) ) ) ~> .K
   </k>
   <retVal>
     noReturn
@@ -57,7 +57,7 @@
       ListItem ( typedValue ( Moved , ty ( 4 ) , mutabilityMut ) )
       ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , ty ( 53 ) , mutabilityNot ) )
       ListItem ( newLocal ( ty ( 2 ) , mutabilityNot ) )
-      ListItem ( newLocal ( ty ( 54 ) , mutabilityMut ) )
+      ListItem ( typedValue ( thunk ( #cast ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , castKindPtrToPtr , ty ( 53 ) , ty ( 54 ) ) ) , ty ( 54 ) , mutabilityMut ) )
       ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 57 ) , mutabilityMut ) )
       ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 57 ) , mutabilityMut ) )
     </locals>
diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-1.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-1.expected
index 735b1530d..91d3745e9 100644
--- a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-1.expected
+++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-1.expected
@@ -1,6 +1,6 @@
 <kmir>
   <k>
-    #execIntrinsic ( IntrinsicFunction ( symbol ( "assert_inhabited" ) ) , .Operands , place (... local: local ( 23 ) , projection: .ProjectionElems ) ) ~> #continueAt ( someBasicBlockIdx ( basicBlockIdx ( 8 ) ) ) ~> .K
+    #traverseProjection ( toLocal ( 24 ) , thunk ( #cast ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , castKindPtrToPtr , ty ( 53 ) , ty ( 54 ) ) ) , projectionElemDeref  .ProjectionElems , .Contexts ) ~> #readProjection ( false ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindStorageDead ( local ( 24 ) ) , span: span ( 299 ) )  statement (... kind: statementKindStorageDead ( local ( 17 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 16 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 25 ) ) , span: span ( 300 ) )  statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueAggregate ( aggregateKindAdt ( adtDef ( 15 ) , variantIdx ( 1 ) , genericArgKindType ( ty ( 23 ) )  .GenericArgs , noUserTypeAnnotationIndex , noFieldIdx ) , operandMove ( place (... local: local ( 15 ) , projection: .ProjectionElems ) )  .Operands ) ) , span: span ( 301 ) )  statement (... kind: statementKindStorageDead ( local ( 15 ) ) , span: span ( 295 ) )  .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindGoto (... target: basicBlockIdx ( 5 ) ) , span: span ( 295 ) ) ) ~> .K
   </k>
   <retVal>
     noReturn
@@ -57,7 +57,7 @@
       ListItem ( typedValue ( Moved , ty ( 4 ) , mutabilityMut ) )
       ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , ty ( 53 ) , mutabilityNot ) )
       ListItem ( newLocal ( ty ( 2 ) , mutabilityNot ) )
-      ListItem ( newLocal ( ty ( 54 ) , mutabilityMut ) )
+      ListItem ( typedValue ( thunk ( #cast ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , castKindPtrToPtr , ty ( 53 ) , ty ( 54 ) ) ) , ty ( 54 ) , mutabilityMut ) )
       ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 57 ) , mutabilityMut ) )
       ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 57 ) , mutabilityMut ) )
     </locals>
diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-2.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-2.expected
index 536fff676..f02732169 100644
--- a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-2.expected
+++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-2.expected
@@ -1,6 +1,6 @@
 <kmir>
   <k>
-    #execIntrinsic ( IntrinsicFunction ( symbol ( "assert_inhabited" ) ) , .Operands , place (... local: local ( 23 ) , projection: .ProjectionElems ) ) ~> #continueAt ( someBasicBlockIdx ( basicBlockIdx ( 8 ) ) ) ~> .K
+    #traverseProjection ( toLocal ( 24 ) , thunk ( #cast ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , castKindPtrToPtr , ty ( 53 ) , ty ( 54 ) ) ) , projectionElemDeref  .ProjectionElems , .Contexts ) ~> #readProjection ( false ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindStorageDead ( local ( 24 ) ) , span: span ( 299 ) )  statement (... kind: statementKindStorageDead ( local ( 17 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 16 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 25 ) ) , span: span ( 300 ) )  statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueAggregate ( aggregateKindAdt ( adtDef ( 15 ) , variantIdx ( 1 ) , genericArgKindType ( ty ( 23 ) )  .GenericArgs , noUserTypeAnnotationIndex , noFieldIdx ) , operandMove ( place (... local: local ( 15 ) , projection: .ProjectionElems ) )  .Operands ) ) , span: span ( 301 ) )  statement (... kind: statementKindStorageDead ( local ( 15 ) ) , span: span ( 295 ) )  .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindGoto (... target: basicBlockIdx ( 5 ) ) , span: span ( 295 ) ) ) ~> .K
   </k>
   <retVal>
     noReturn
@@ -57,7 +57,7 @@
       ListItem ( typedValue ( Moved , ty ( 4 ) , mutabilityMut ) )
       ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , ty ( 53 ) , mutabilityNot ) )
       ListItem ( newLocal ( ty ( 2 ) , mutabilityNot ) )
-      ListItem ( newLocal ( ty ( 54 ) , mutabilityMut ) )
+      ListItem ( typedValue ( thunk ( #cast ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , castKindPtrToPtr , ty ( 53 ) , ty ( 54 ) ) ) , ty ( 54 ) , mutabilityMut ) )
       ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 57 ) , mutabilityMut ) )
       ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 57 ) , mutabilityMut ) )
     </locals>
diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-3.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-3.expected
index 114bd6bea..7df1ab662 100644
--- a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-3.expected
+++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-3.expected
@@ -1,6 +1,6 @@
 <kmir>
   <k>
-    #execIntrinsic ( IntrinsicFunction ( symbol ( "assert_inhabited" ) ) , .Operands , place (... local: local ( 23 ) , projection: .ProjectionElems ) ) ~> #continueAt ( someBasicBlockIdx ( basicBlockIdx ( 8 ) ) ) ~> .K
+    #traverseProjection ( toLocal ( 24 ) , thunk ( #cast ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , castKindPtrToPtr , ty ( 53 ) , ty ( 54 ) ) ) , projectionElemDeref  .ProjectionElems , .Contexts ) ~> #readProjection ( false ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindStorageDead ( local ( 24 ) ) , span: span ( 299 ) )  statement (... kind: statementKindStorageDead ( local ( 17 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 16 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 25 ) ) , span: span ( 300 ) )  statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueAggregate ( aggregateKindAdt ( adtDef ( 15 ) , variantIdx ( 1 ) , genericArgKindType ( ty ( 23 ) )  .GenericArgs , noUserTypeAnnotationIndex , noFieldIdx ) , operandMove ( place (... local: local ( 15 ) , projection: .ProjectionElems ) )  .Operands ) ) , span: span ( 301 ) )  statement (... kind: statementKindStorageDead ( local ( 15 ) ) , span: span ( 295 ) )  .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindGoto (... target: basicBlockIdx ( 5 ) ) , span: span ( 295 ) ) ) ~> .K
   </k>
   <retVal>
     noReturn
@@ -57,7 +57,7 @@
       ListItem ( typedValue ( Moved , ty ( 4 ) , mutabilityMut ) )
       ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , ty ( 53 ) , mutabilityNot ) )
       ListItem ( newLocal ( ty ( 2 ) , mutabilityNot ) )
-      ListItem ( newLocal ( ty ( 54 ) , mutabilityMut ) )
+      ListItem ( typedValue ( thunk ( #cast ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , castKindPtrToPtr , ty ( 53 ) , ty ( 54 ) ) ) , ty ( 54 ) , mutabilityMut ) )
       ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 57 ) , mutabilityMut ) )
       ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 57 ) , mutabilityMut ) )
     </locals>
diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-4.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-4.expected
index ddd746bad..40170c732 100644
--- a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-4.expected
+++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-4.expected
@@ -1,6 +1,6 @@
 <kmir>
   <k>
-    #execIntrinsic ( IntrinsicFunction ( symbol ( "assert_inhabited" ) ) , .Operands , place (... local: local ( 23 ) , projection: .ProjectionElems ) ) ~> #continueAt ( someBasicBlockIdx ( basicBlockIdx ( 8 ) ) ) ~> .K
+    #traverseProjection ( toLocal ( 24 ) , thunk ( #cast ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , castKindPtrToPtr , ty ( 53 ) , ty ( 54 ) ) ) , projectionElemDeref  .ProjectionElems , .Contexts ) ~> #readProjection ( false ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindStorageDead ( local ( 24 ) ) , span: span ( 299 ) )  statement (... kind: statementKindStorageDead ( local ( 17 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 16 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 25 ) ) , span: span ( 300 ) )  statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueAggregate ( aggregateKindAdt ( adtDef ( 15 ) , variantIdx ( 1 ) , genericArgKindType ( ty ( 23 ) )  .GenericArgs , noUserTypeAnnotationIndex , noFieldIdx ) , operandMove ( place (... local: local ( 15 ) , projection: .ProjectionElems ) )  .Operands ) ) , span: span ( 301 ) )  statement (... kind: statementKindStorageDead ( local ( 15 ) ) , span: span ( 295 ) )  .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindGoto (... target: basicBlockIdx ( 5 ) ) , span: span ( 295 ) ) ) ~> .K
   </k>
   <retVal>
     noReturn
@@ -57,7 +57,7 @@
       ListItem ( typedValue ( Moved , ty ( 4 ) , mutabilityMut ) )
       ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , ty ( 53 ) , mutabilityNot ) )
       ListItem ( newLocal ( ty ( 2 ) , mutabilityNot ) )
-      ListItem ( newLocal ( ty ( 54 ) , mutabilityMut ) )
+      ListItem ( typedValue ( thunk ( #cast ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , castKindPtrToPtr , ty ( 53 ) , ty ( 54 ) ) ) , ty ( 54 ) , mutabilityMut ) )
       ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 57 ) , mutabilityMut ) )
       ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 57 ) , mutabilityMut ) )
     </locals>
diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-5.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-5.expected
index d54772d2c..1c554b71a 100644
--- a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-5.expected
+++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-5.expected
@@ -1,6 +1,6 @@
 <kmir>
   <k>
-    #execIntrinsic ( IntrinsicFunction ( symbol ( "assert_inhabited" ) ) , .Operands , place (... local: local ( 23 ) , projection: .ProjectionElems ) ) ~> #continueAt ( someBasicBlockIdx ( basicBlockIdx ( 8 ) ) ) ~> .K
+    #traverseProjection ( toLocal ( 24 ) , thunk ( #cast ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , castKindPtrToPtr , ty ( 53 ) , ty ( 54 ) ) ) , projectionElemDeref  .ProjectionElems , .Contexts ) ~> #readProjection ( false ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindStorageDead ( local ( 24 ) ) , span: span ( 299 ) )  statement (... kind: statementKindStorageDead ( local ( 17 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 16 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 25 ) ) , span: span ( 300 ) )  statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueAggregate ( aggregateKindAdt ( adtDef ( 15 ) , variantIdx ( 1 ) , genericArgKindType ( ty ( 23 ) )  .GenericArgs , noUserTypeAnnotationIndex , noFieldIdx ) , operandMove ( place (... local: local ( 15 ) , projection: .ProjectionElems ) )  .Operands ) ) , span: span ( 301 ) )  statement (... kind: statementKindStorageDead ( local ( 15 ) ) , span: span ( 295 ) )  .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindGoto (... target: basicBlockIdx ( 5 ) ) , span: span ( 295 ) ) ) ~> .K
   </k>
   <retVal>
     noReturn
@@ -57,7 +57,7 @@
       ListItem ( typedValue ( Moved , ty ( 4 ) , mutabilityMut ) )
       ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , ty ( 53 ) , mutabilityNot ) )
       ListItem ( newLocal ( ty ( 2 ) , mutabilityNot ) )
-      ListItem ( newLocal ( ty ( 54 ) , mutabilityMut ) )
+      ListItem ( typedValue ( thunk ( #cast ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , castKindPtrToPtr , ty ( 53 ) , ty ( 54 ) ) ) , ty ( 54 ) , mutabilityMut ) )
       ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 57 ) , mutabilityMut ) )
       ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 57 ) , mutabilityMut ) )
     </locals>
diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-6.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-6.expected
index aee43e719..732928c90 100644
--- a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-6.expected
+++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-6.expected
@@ -1,6 +1,6 @@
 <kmir>
   <k>
-    #execIntrinsic ( IntrinsicFunction ( symbol ( "assert_inhabited" ) ) , .Operands , place (... local: local ( 23 ) , projection: .ProjectionElems ) ) ~> #continueAt ( someBasicBlockIdx ( basicBlockIdx ( 8 ) ) ) ~> .K
+    #traverseProjection ( toLocal ( 24 ) , thunk ( #cast ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , castKindPtrToPtr , ty ( 53 ) , ty ( 54 ) ) ) , projectionElemDeref  .ProjectionElems , .Contexts ) ~> #readProjection ( false ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindStorageDead ( local ( 24 ) ) , span: span ( 299 ) )  statement (... kind: statementKindStorageDead ( local ( 17 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 16 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 25 ) ) , span: span ( 300 ) )  statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueAggregate ( aggregateKindAdt ( adtDef ( 15 ) , variantIdx ( 1 ) , genericArgKindType ( ty ( 23 ) )  .GenericArgs , noUserTypeAnnotationIndex , noFieldIdx ) , operandMove ( place (... local: local ( 15 ) , projection: .ProjectionElems ) )  .Operands ) ) , span: span ( 301 ) )  statement (... kind: statementKindStorageDead ( local ( 15 ) ) , span: span ( 295 ) )  .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindGoto (... target: basicBlockIdx ( 5 ) ) , span: span ( 295 ) ) ) ~> .K
   </k>
   <retVal>
     noReturn
@@ -57,7 +57,7 @@
       ListItem ( typedValue ( Moved , ty ( 4 ) , mutabilityMut ) )
       ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , ty ( 53 ) , mutabilityNot ) )
       ListItem ( newLocal ( ty ( 2 ) , mutabilityNot ) )
-      ListItem ( newLocal ( ty ( 54 ) , mutabilityMut ) )
+      ListItem ( typedValue ( thunk ( #cast ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , castKindPtrToPtr , ty ( 53 ) , ty ( 54 ) ) ) , ty ( 54 ) , mutabilityMut ) )
       ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 57 ) , mutabilityMut ) )
       ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 57 ) , mutabilityMut ) )
     </locals>
diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-8.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-8.expected
index 6c279456d..174ed9019 100644
--- a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-8.expected
+++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-8.expected
@@ -1,6 +1,6 @@
 <kmir>
   <k>
-    #execIntrinsic ( IntrinsicFunction ( symbol ( "assert_inhabited" ) ) , .Operands , place (... local: local ( 23 ) , projection: .ProjectionElems ) ) ~> #continueAt ( someBasicBlockIdx ( basicBlockIdx ( 8 ) ) ) ~> .K
+    #traverseProjection ( toLocal ( 24 ) , thunk ( #cast ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , castKindPtrToPtr , ty ( 53 ) , ty ( 54 ) ) ) , projectionElemDeref  .ProjectionElems , .Contexts ) ~> #readProjection ( false ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindStorageDead ( local ( 24 ) ) , span: span ( 299 ) )  statement (... kind: statementKindStorageDead ( local ( 17 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 16 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 25 ) ) , span: span ( 300 ) )  statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueAggregate ( aggregateKindAdt ( adtDef ( 15 ) , variantIdx ( 1 ) , genericArgKindType ( ty ( 23 ) )  .GenericArgs , noUserTypeAnnotationIndex , noFieldIdx ) , operandMove ( place (... local: local ( 15 ) , projection: .ProjectionElems ) )  .Operands ) ) , span: span ( 301 ) )  statement (... kind: statementKindStorageDead ( local ( 15 ) ) , span: span ( 295 ) )  .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindGoto (... target: basicBlockIdx ( 5 ) ) , span: span ( 295 ) ) ) ~> .K
   </k>
   <retVal>
     noReturn
@@ -57,7 +57,7 @@
       ListItem ( typedValue ( Moved , ty ( 4 ) , mutabilityMut ) )
       ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , ty ( 53 ) , mutabilityNot ) )
       ListItem ( newLocal ( ty ( 2 ) , mutabilityNot ) )
-      ListItem ( newLocal ( ty ( 54 ) , mutabilityMut ) )
+      ListItem ( typedValue ( thunk ( #cast ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , castKindPtrToPtr , ty ( 53 ) , ty ( 54 ) ) ) , ty ( 54 ) , mutabilityMut ) )
       ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 57 ) , mutabilityMut ) )
       ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 57 ) , mutabilityMut ) )
     </locals>
diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-9.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-9.expected
index 3925b10fe..c9e4b185e 100644
--- a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-9.expected
+++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-9.expected
@@ -1,6 +1,6 @@
 <kmir>
   <k>
-    #execIntrinsic ( IntrinsicFunction ( symbol ( "assert_inhabited" ) ) , .Operands , place (... local: local ( 23 ) , projection: .ProjectionElems ) ) ~> #continueAt ( someBasicBlockIdx ( basicBlockIdx ( 8 ) ) ) ~> .K
+    #traverseProjection ( toLocal ( 24 ) , thunk ( #cast ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , castKindPtrToPtr , ty ( 53 ) , ty ( 54 ) ) ) , projectionElemDeref  .ProjectionElems , .Contexts ) ~> #readProjection ( false ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindStorageDead ( local ( 24 ) ) , span: span ( 299 ) )  statement (... kind: statementKindStorageDead ( local ( 17 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 16 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 25 ) ) , span: span ( 300 ) )  statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueAggregate ( aggregateKindAdt ( adtDef ( 15 ) , variantIdx ( 1 ) , genericArgKindType ( ty ( 23 ) )  .GenericArgs , noUserTypeAnnotationIndex , noFieldIdx ) , operandMove ( place (... local: local ( 15 ) , projection: .ProjectionElems ) )  .Operands ) ) , span: span ( 301 ) )  statement (... kind: statementKindStorageDead ( local ( 15 ) ) , span: span ( 295 ) )  .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindGoto (... target: basicBlockIdx ( 5 ) ) , span: span ( 295 ) ) ) ~> .K
   </k>
   <retVal>
     noReturn
@@ -57,7 +57,7 @@
       ListItem ( typedValue ( Moved , ty ( 4 ) , mutabilityMut ) )
       ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , ty ( 53 ) , mutabilityNot ) )
       ListItem ( newLocal ( ty ( 2 ) , mutabilityNot ) )
-      ListItem ( newLocal ( ty ( 54 ) , mutabilityMut ) )
+      ListItem ( typedValue ( thunk ( #cast ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , castKindPtrToPtr , ty ( 53 ) , ty ( 54 ) ) ) , ty ( 54 ) , mutabilityMut ) )
       ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 57 ) , mutabilityMut ) )
       ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 57 ) , mutabilityMut ) )
     </locals>
diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py
index 1c791b2a7..d5462b555 100644
--- a/kmir/src/tests/integration/test_integration.py
+++ b/kmir/src/tests/integration/test_integration.py
@@ -54,6 +54,8 @@
     'raw-ptr-cast-fail',
     'transmute-u8-to-enum-fail',
     'transmute-u8-to-enum-changed-discriminant-signed-fail',
+    'assert-inhabited-fail',
+    'iterator-simple-fail',
 ]