diff --git a/repos/ports/src/virtualbox/spec/muen/sup.cc b/repos/ports/src/virtualbox/spec/muen/sup.cc
index ad090537c..08cab05b7 100644
--- a/repos/ports/src/virtualbox/spec/muen/sup.cc
+++ b/repos/ports/src/virtualbox/spec/muen/sup.cc
@@ -219,10 +219,6 @@ inline bool set_cr(struct Subject_state *cur_state, unsigned cr, uint64_t value)
 			cur_state->Regs.Cr2 = value;
 			res = true;
 			break;
-		case 3:
-			cur_state->Cr3 = value;
-			res = true;
-			break;
 		case 4:
 			cur_state->Shadow_cr4 = value;
 			cur_state->Cr4  = value | 1 << 13;
@@ -433,7 +429,6 @@ int SUPR3CallVMMR0Fast(PVMR0 pVMR0, unsigned uOperation, VMCPUID idCpu)
 
 		set_cr(cur_state, 0, pCtx->cr0);
 		set_cr(cur_state, 2, pCtx->cr2);
-		set_cr(cur_state, 3, pCtx->cr3);
 		set_cr(cur_state, 4, pCtx->cr4);
 
 		GENODE_WRITE_SELREG(cs);
diff --git a/repos/ports/src/virtualbox/spec/muen/vcpu.h b/repos/ports/src/virtualbox/spec/muen/vcpu.h
index c4e59dc4e..ff6d1262b 100644
--- a/repos/ports/src/virtualbox/spec/muen/vcpu.h
+++ b/repos/ports/src/virtualbox/spec/muen/vcpu.h
@@ -49,7 +49,6 @@ struct Subject_state
 	struct Cpu_registers Regs;
 	Genode::uint32_t Exit_reason;
 	Genode::uint32_t Intr_state;
-	Genode::uint32_t Interrupt_info;
 	Genode::uint32_t Sysenter_cs;
 	Genode::uint64_t Exit_qualification;
 	Genode::uint64_t Guest_phys_addr;
@@ -75,6 +74,6 @@ struct Subject_state
 	Segment ldtr;
 	Segment gdtr;
 	Segment idtr;
-} __attribute__((packed));
+};
 
 #endif /* _VIRTUALBOX__SPEC__MUEN__VCPU_H_ */