diff --git a/src/assertions.cpp b/src/assertions.cpp
index b2258691a..8caf3b0a1 100644
--- a/src/assertions.cpp
+++ b/src/assertions.cpp
@@ -229,7 +229,13 @@ class AssertExtractor {
 
     vector<Assert> operator()(const Bin& ins) const {
         switch (ins.op) {
-        case Bin::Op::MOV: return {};
+        case Bin::Op::MOV:
+            if (const auto src = std::get_if<Reg>(&ins.v)) {
+                if (!ins.is64) {
+                    return {Assert{TypeConstraint{*src, TypeGroup::number}}};
+                }
+            }
+            return {};
         case Bin::Op::MOVSX8:
         case Bin::Op::MOVSX16:
         case Bin::Op::MOVSX32:
diff --git a/test-data/assign.yaml b/test-data/assign.yaml
index 22a765b0f..cfbf98917 100644
--- a/test-data/assign.yaml
+++ b/test-data/assign.yaml
@@ -186,6 +186,9 @@ post:
   - r2.uvalue=[0, 4294967295]
   - r10.type=stack
   - r10.stack_offset=512
+
+messages:
+  - "0: Invalid type (r10.type == number)"
 ---
 test-case: assign register shared value
 
@@ -220,6 +223,9 @@ post:
   - r2.svalue=[0, 4294967295]
   - r2.uvalue=[0, 4294967295]
   - r2.svalue=r2.uvalue
+
+messages:
+  - "0: Invalid type (r1.type == number)"
 ---
 test-case: assign register combination value
 
@@ -323,6 +329,9 @@ post:
   - packet_size=r2.packet_offset
   - r2.type=packet
   - r2.svalue=[4098, 2147418112]
+
+messages:
+  - "0: Invalid type (r2.type == number)"
 ---
 test-case: assign register context value
 
@@ -360,6 +369,9 @@ post:
   - r2.svalue=[1, 2147418112]
   - r2.uvalue=[1, 2147418112]
   - r2.svalue=r2.uvalue
+
+messages:
+  - "0: Invalid type (r1.type == number)"
 ---
 test-case: assign register map value
 
@@ -391,6 +403,9 @@ post:
   - r2.svalue=[0, 4294967295]
   - r2.uvalue=[0, 4294967295]
   - r2.svalue=r2.uvalue
+
+messages:
+  - "0: Invalid type (r1.type == number)"
 ---
 test-case: assign register map programs value
 
@@ -422,3 +437,6 @@ post:
   - r2.svalue=[0, 4294967295]
   - r2.uvalue=[0, 4294967295]
   - r2.svalue=r2.uvalue
+
+messages:
+  - "0: Invalid type (r1.type == number)"
diff --git a/test-data/pointer.yaml b/test-data/pointer.yaml
index 7d3dc969c..ade7147df 100644
--- a/test-data/pointer.yaml
+++ b/test-data/pointer.yaml
@@ -1,6 +1,6 @@
-# Copyright (c) Prevail Verifier contributors.
-# SPDX-License-Identifier: MIT
----
+# # Copyright (c) Prevail Verifier contributors.
+# # SPDX-License-Identifier: MIT
+# ---
 test-case: 32-bit pointer truncation - addition
 
 pre:
@@ -355,3 +355,70 @@ messages:
   - "1: Invalid type (r1.type == number)"
   - "2: Lower bound must be at least 0 (valid_access(r1.offset, width=4) for read)"
   - "2: Upper bound must be at most 64 (valid_access(r1.offset, width=4) for read)"
+
+---
+test-case: 64-bit return context pointer
+
+pre:
+  - r0.uvalue=[0, 4294967295]
+  - r0.svalue=r0.uvalue
+  - r0.type=number
+  - "r1.ctx_offset=0"
+  - "r1.svalue=[0, 4294967295]"
+  - "r1.svalue=r1.uvalue"
+  - "r1.type=ctx"
+  - "r1.uvalue=[0, 4294967295]"
+
+code:
+  <start>: |
+    r0 = r1
+    exit
+
+post:
+  - r0.ctx_offset=0
+  - r0.svalue=[0, 4294967295]
+  - r0.svalue=r0.uvalue
+  - r0.svalue=r1.svalue
+  - r0.svalue=r1.uvalue
+  - r0.type=ctx
+  - r0.uvalue=[0, 4294967295]
+  - r0.uvalue=r1.svalue
+  - r0.uvalue=r1.uvalue
+  - r1.ctx_offset=0
+  - r1.svalue=[0, 4294967295]
+  - r1.svalue=r1.uvalue
+  - r1.type=ctx
+  - r1.uvalue=[0, 4294967295]
+
+messages:
+  - "1: Invalid type (r0.type == number)"
+
+---
+test-case: 32-bit return context pointer
+
+pre:
+  - r0.uvalue=0
+  - r0.svalue=r0.uvalue
+  - r0.type=number
+  - "r1.ctx_offset=0"
+  - "r1.svalue=1234567890"
+  - "r1.svalue=r1.uvalue"
+  - "r1.type=ctx"
+  - "r1.uvalue=1234567890"
+
+code:
+  <start>: |
+    w0 = w1
+
+post:
+  - r1.ctx_offset=0
+  - r1.svalue=1234567890
+  - r1.svalue=r1.uvalue
+  - r1.type=ctx
+  - r1.uvalue=1234567890
+  - r0.svalue=1234567890
+  - r0.type=number
+  - r0.uvalue=1234567890
+
+messages:
+  - "0: Invalid type (r1.type == number)"