diff --git a/hypervisor/arch/x86/page.c b/hypervisor/arch/x86/page.c
index 907800a7c..4f170656c 100644
--- a/hypervisor/arch/x86/page.c
+++ b/hypervisor/arch/x86/page.c
@@ -12,7 +12,6 @@
 #include <vtd.h>
 #include <security.h>
 #include <vm.h>
-#include <vm_configurations.h>
 
 static struct page ppt_pml4_pages[PML4_PAGE_NUM(CONFIG_PLATFORM_RAM_SIZE + PLATFORM_LO_MMIO_SIZE)];
 static struct page ppt_pdpt_pages[PDPT_PAGE_NUM(CONFIG_PLATFORM_RAM_SIZE + PLATFORM_LO_MMIO_SIZE)];
@@ -104,7 +103,7 @@ static union pgtable_pages_info ept_pages_info[CONFIG_MAX_VM_NUM];
 static const uint64_t vm_address_space_size[MAX_LOAD_ORDER] = {
 	PRE_VM_EPT_ADDRESS_SPACE(CONFIG_UOS_RAM_SIZE), /* for Pre-Launched VM */
 	EPT_ADDRESS_SPACE(CONFIG_SOS_RAM_SIZE), /* for SOS VM */
-	EPT_ADDRESS_SPACE(CONFIG_SOS_RAM_SIZE), /* for Post-Launched VM */
+	EPT_ADDRESS_SPACE(CONFIG_UOS_RAM_SIZE), /* for Post-Launched VM */
 };
 
 /*
diff --git a/hypervisor/include/arch/x86/vm_config.h b/hypervisor/include/arch/x86/vm_config.h
index 49f2dbb43..49bac1ffa 100644
--- a/hypervisor/include/arch/x86/vm_config.h
+++ b/hypervisor/include/arch/x86/vm_config.h
@@ -36,6 +36,9 @@
  * PRE_LAUNCHED_VM is launched by ACRN hypervisor, with LAPIC_PT;
  * SOS_VM is launched by ACRN hypervisor, without LAPIC_PT;
  * POST_LAUNCHED_VM is launched by ACRN devicemodel, with/without LAPIC_PT depends on usecases.
+ *
+ * Assumption: vm_configs array is completely initialized w.r.t. load_order member of
+ * 		acrn_vm_config for all the VMs.
  */
 enum acrn_vm_load_order {
 	PRE_LAUNCHED_VM = 0,