diff --git a/sys/arm64/vmm/vmm_hyp.c b/sys/arm64/vmm/vmm_hyp.c
--- a/sys/arm64/vmm/vmm_hyp.c
+++ b/sys/arm64/vmm/vmm_hyp.c
@@ -262,6 +262,9 @@
 	uint64_t dfr0;
 
 	/* Restore the special registers */
+	WRITE_SPECIALREG(hcr_el2, hypctx->hcr_el2);
+	isb();
+
 	WRITE_SPECIALREG(elr_el1, hypctx->elr_el1);
 	WRITE_SPECIALREG(sp_el0, hypctx->sp_el0);
 	WRITE_SPECIALREG(tpidr_el0, hypctx->tpidr_el0);
@@ -290,7 +293,6 @@
 	WRITE_SPECIALREG(spsr_el1, hypctx->spsr_el1);
 
 	WRITE_SPECIALREG(cptr_el2, hypctx->cptr_el2);
-	WRITE_SPECIALREG(hcr_el2, hypctx->hcr_el2);
 	WRITE_SPECIALREG(vpidr_el2, hypctx->vpidr_el2);
 	WRITE_SPECIALREG(vmpidr_el2, hypctx->vmpidr_el2);