diff --git a/reactos/ntoskrnl/mm/ARM3/miarm.h b/reactos/ntoskrnl/mm/ARM3/miarm.h
index 78bbcce6f14..6b4035be0ff 100644
--- a/reactos/ntoskrnl/mm/ARM3/miarm.h
+++ b/reactos/ntoskrnl/mm/ARM3/miarm.h
@@ -565,6 +565,50 @@ MiIsMemoryTypeInvisible(TYPE_OF_MEMORY MemoryType)
             (MemoryType == LoaderBBTMemory));
 }
 
+#ifdef _M_AMD64
+BOOLEAN
+FORCEINLINE
+MiIsUserPxe(PVOID Address)
+{
+    return ((ULONG_PTR)Address >> 7) == 0x1FFFFEDF6FB7DA0ULL;
+}
+
+BOOLEAN
+FORCEINLINE
+MiIsUserPpe(PVOID Address)
+{
+    return ((ULONG_PTR)Address >> 16) == 0xFFFFF6FB7DA0ULL;
+}
+
+BOOLEAN
+FORCEINLINE
+MiIsUserPde(PVOID Address)
+{
+    return ((ULONG_PTR)Address >> 25) == 0x7FFFFB7DA0ULL;
+}
+
+BOOLEAN
+FORCEINLINE
+MiIsUserPte(PVOID Address)
+{
+    return ((ULONG_PTR)Address >> 34) == 0x3FFFFDA0ULL;
+}
+#else
+BOOLEAN
+FORCEINLINE
+MiIsUserPde(PVOID Address)
+{
+    return ((Address >= (PVOID)MiAddressToPde(NULL)) &&
+            (Address <= (PVOID)MiHighestUserPde));
+}
+
+BOOLEAN
+FORCEINLINE
+MiIsUserPte(PVOID Address)
+{
+    return (Address <= (PVOID)MiHighestUserPte);
+}
+#endif
 
 //
 // Figures out the hardware bits for a PTE
@@ -583,9 +627,15 @@ MiDetermineUserGlobalPteMask(IN PVOID PointerPte)
     MI_MAKE_ACCESSED_PAGE(&TempPte);
 
     /* Is this for user-mode? */
-    if ((PointerPte <= (PVOID)MiHighestUserPte) ||
-        ((PointerPte >= (PVOID)MiAddressToPde(NULL)) &&
-         (PointerPte <= (PVOID)MiHighestUserPde)))
+    if (
+#if (_MI_PAGING_LEVELS == 4)
+        MiIsUserPxe(PointerPte) ||
+#endif
+#if (_MI_PAGING_LEVELS >= 3)
+        MiIsUserPpe(PointerPte) ||
+#endif
+        MiIsUserPde(PointerPte) ||
+        MiIsUserPte(PointerPte))
     {
         /* Set the owner bit */
         MI_MAKE_OWNER_PAGE(&TempPte);
diff --git a/reactos/ntoskrnl/mm/ARM3/pagfault.c b/reactos/ntoskrnl/mm/ARM3/pagfault.c
index 0b59938eb0b..fda089794fe 100644
--- a/reactos/ntoskrnl/mm/ARM3/pagfault.c
+++ b/reactos/ntoskrnl/mm/ARM3/pagfault.c
@@ -335,22 +335,10 @@ MiResolveDemandZeroFault(IN PVOID Address,
     if (NeedZero) MiZeroPfn(PageFrameNumber);
 
     /* Build the PTE */
-    if (PointerPte <= MiHighestUserPte)
-    {
-        /* For user mode */
-        MI_MAKE_HARDWARE_PTE_USER(&TempPte,
-                                  PointerPte,
-                                  Protection,
-                                  PageFrameNumber);
-    }
-    else
-    {
-        /* For kernel mode */
-        MI_MAKE_HARDWARE_PTE(&TempPte,
-                             PointerPte,
-                             Protection,
-                             PageFrameNumber);
-    }
+    MI_MAKE_HARDWARE_PTE(&TempPte,
+                         PointerPte,
+                         Protection,
+                         PageFrameNumber);
 
     /* Set it dirty if it's a writable page */
     if (MI_IS_PAGE_WRITEABLE(&TempPte)) MI_MAKE_DIRTY_PAGE(&TempPte);
@@ -625,6 +613,7 @@ MiDispatchFault(IN BOOLEAN StoreInstruction,
     /* Check if the PTE is completely empty */
     if (TempPte.u.Long == 0)
     {
+        /* The address is not from any pageable area! */
         KeBugCheckEx(PAGE_FAULT_IN_NONPAGED_AREA,
                      (ULONG_PTR)Address,
                      StoreInstruction,