diff --git a/repos/base-hw/src/core/spec/x86_64/virtualization/kernel/svm.cc b/repos/base-hw/src/core/spec/x86_64/virtualization/kernel/svm.cc
index 1d9bbcc88c..9246d870d2 100644
--- a/repos/base-hw/src/core/spec/x86_64/virtualization/kernel/svm.cc
+++ b/repos/base-hw/src/core/spec/x86_64/virtualization/kernel/svm.cc
@@ -67,8 +67,7 @@ Vmcb_buf &Vmcb::host_vmcb(size_t cpu_id)
 	return *host_vmcb[cpu_id];
 }
 
-void Vmcb::initialize(Kernel::Cpu &cpu, addr_t page_table_phys_addr,
-                      Core::Cpu::Context &)
+void Vmcb::initialize(Kernel::Cpu &cpu, addr_t page_table_phys_addr)
 {
 	using Cpu = Hw::X86_64_cpu;
 
diff --git a/repos/base-hw/src/core/spec/x86_64/virtualization/kernel/vm.cc b/repos/base-hw/src/core/spec/x86_64/virtualization/kernel/vm.cc
index 702dc05698..5a6cc3bbc7 100644
--- a/repos/base-hw/src/core/spec/x86_64/virtualization/kernel/vm.cc
+++ b/repos/base-hw/src/core/spec/x86_64/virtualization/kernel/vm.cc
@@ -266,5 +266,5 @@ void Board::Vcpu_context::write_vcpu_state(Vcpu_state &state)
 
 void Board::Vcpu_context::initialize(Kernel::Cpu &cpu, addr_t table_phys_addr)
 {
-	virt.initialize(cpu, table_phys_addr, *regs);
+	virt.initialize(cpu, table_phys_addr);
 }
diff --git a/repos/base-hw/src/core/spec/x86_64/virtualization/kernel/vmx.cc b/repos/base-hw/src/core/spec/x86_64/virtualization/kernel/vmx.cc
index 0380c107c3..6ee5bd3150 100644
--- a/repos/base-hw/src/core/spec/x86_64/virtualization/kernel/vmx.cc
+++ b/repos/base-hw/src/core/spec/x86_64/virtualization/kernel/vmx.cc
@@ -53,6 +53,21 @@ extern int       __idt;
 
 Vmcs * current_vmcs[Hw::Pc_board::NR_OF_CPUS]  = { nullptr };
 
+/*
+ * We need to push the artifical TRAP_VMEXIT value
+ * to trapno after returning from vmlauch and before
+ * jumping to _kernel_entry
+ */
+void kernel_entry_push_trap()
+{
+	asm volatile(
+	      "pushq %[trap_val];" /* make the stack point to trapno, the right place */
+	      "jmp _kernel_entry;"
+	      :
+	      : [trap_val] "i"(Board::TRAP_VMEXIT)
+	      : "memory");
+}
+
 Vmcs_buf::Vmcs_buf(Genode::uint32_t system_rev)
 {
 	Genode::memset((void *) this, 0, sizeof(Vmcs_buf));
@@ -233,8 +248,7 @@ void Vmcs::setup_vmx_info()
 	cr4_mask   = ~cr4_fixed1 | cr4_fixed0;
 }
 
-void Vmcs::initialize(Kernel::Cpu &cpu, Genode::addr_t page_table_phys,
-                      Core::Cpu::Context &regs)
+void Vmcs::initialize(Kernel::Cpu &cpu, Genode::addr_t page_table_phys)
 {
 	using Cpu = Hw::X86_64_cpu;
 
@@ -346,14 +360,14 @@ void Vmcs::initialize(Kernel::Cpu &cpu, Genode::addr_t page_table_phys,
 
 	write(E_HOST_IA32_SYSENTER_ESP, reinterpret_cast<Genode::addr_t>(&(cpu.tss.rsp[0])));
 	write(E_HOST_IA32_SYSENTER_CS, 0x8);
-	write(E_HOST_IA32_SYSENTER_EIP, reinterpret_cast<Genode::uint64_t>(&_kernel_entry));
+	write(E_HOST_IA32_SYSENTER_EIP, reinterpret_cast<Genode::uint64_t>(&kernel_entry_push_trap));
 
 	/*
 	 * Set the RSP to trapno, so that _kernel_entry will save the registers
 	 * into the right fields.
 	 */
-	write(E_HOST_RSP, reinterpret_cast<Genode::uint64_t>(&(regs.trapno)));
-	write(E_HOST_RIP, reinterpret_cast<Genode::uint64_t>(&_kernel_entry));
+	write(E_HOST_RSP, cpu.stack_start() - 568);
+	write(E_HOST_RIP, reinterpret_cast<Genode::uint64_t>(&kernel_entry_push_trap));
 }
 
 
diff --git a/repos/base-hw/src/core/spec/x86_64/virtualization/svm.h b/repos/base-hw/src/core/spec/x86_64/virtualization/svm.h
index b654f3a275..1b97c5f232 100644
--- a/repos/base-hw/src/core/spec/x86_64/virtualization/svm.h
+++ b/repos/base-hw/src/core/spec/x86_64/virtualization/svm.h
@@ -332,8 +332,7 @@ struct Board::Vmcb
 	void enforce_intercepts(uint32_t desired_primary   = 0U,
 	                        uint32_t desired_secondary = 0U);
 	void initialize(Kernel::Cpu   &cpu,
-	                addr_t page_table_phys_addr,
-	                Core::Cpu::Context &) override;
+	                addr_t page_table_phys_addr) override;
 	void write_vcpu_state(Vcpu_state &state) override;
 	void read_vcpu_state(Vcpu_state &state) override;
 	void switch_world(Core::Cpu::Context &regs, addr_t) override;
diff --git a/repos/base-hw/src/core/spec/x86_64/virtualization/virt_interface.h b/repos/base-hw/src/core/spec/x86_64/virtualization/virt_interface.h
index 1c0a1e6502..37d2ad9689 100644
--- a/repos/base-hw/src/core/spec/x86_64/virtualization/virt_interface.h
+++ b/repos/base-hw/src/core/spec/x86_64/virtualization/virt_interface.h
@@ -38,8 +38,8 @@ struct Virt_interface
 	Genode::Vcpu_data &vcpu_data;
 
 	virtual void initialize(Kernel::Cpu        &cpu,
-	                        addr_t              page_table_phys_addr,
-				Core::Cpu::Context &regs)   = 0;
+	                        addr_t              page_table_phys_addr)
+				                            = 0;
 	virtual void write_vcpu_state(Vcpu_state &state)    = 0;
 	virtual void read_vcpu_state(Vcpu_state &state)     = 0;
 	virtual void switch_world(Core::Cpu::Context &regs, addr_t) = 0;
diff --git a/repos/base-hw/src/core/spec/x86_64/virtualization/vmx.h b/repos/base-hw/src/core/spec/x86_64/virtualization/vmx.h
index ed98fc788c..a6386e5578 100644
--- a/repos/base-hw/src/core/spec/x86_64/virtualization/vmx.h
+++ b/repos/base-hw/src/core/spec/x86_64/virtualization/vmx.h
@@ -382,8 +382,7 @@ Board::Vmcs
 		return ((ar >> 4) & 0x1F00) | (ar & 0xFF);
 	}
 
-	void initialize(Kernel::Cpu &cpu, addr_t page_table_phys,
-	                Core::Cpu::Context &regs) override;
+	void initialize(Kernel::Cpu &cpu, addr_t page_table_phys) override;
 	void write_vcpu_state(Genode::Vcpu_state &state) override;
 	void read_vcpu_state(Genode::Vcpu_state &state) override;
 	void switch_world(Core::Cpu::Context &regs, addr_t) override;