diff --git a/src/arch/aarch64/fault.c b/src/arch/aarch64/fault.c
index efd5df43..1cca4dad 100644
--- a/src/arch/aarch64/fault.c
+++ b/src/arch/aarch64/fault.c
@@ -27,7 +27,11 @@ bool fault_advance_vcpu(size_t vcpu_id, seL4_UserContext *regs)
     // For now we just ignore it and continue
     // Assume 32-bit instruction
     regs->pc += 4;
-    int err = seL4_TCB_WriteRegisters(BASE_VM_TCB_CAP + vcpu_id, true, 0, SEL4_USER_CONTEXT_SIZE, regs);
+    /*
+     * Do not explicitly resume the TCB because we will eventually reply to the
+     * fault which will result in the TCB being restarted.
+     */
+    int err = seL4_TCB_WriteRegisters(BASE_VM_TCB_CAP + vcpu_id, false, 0, SEL4_USER_CONTEXT_SIZE, regs);
     assert(err == seL4_NoError);
 
     return (err == seL4_NoError);