diff --git a/arch/arm64/kvm/hyp/include/nvhe/trap_handler.h b/arch/arm64/kvm/hyp/include/nvhe/trap_handler.h
index 1e6d995..bd1cc9e 100644
--- a/arch/arm64/kvm/hyp/include/nvhe/trap_handler.h
+++ b/arch/arm64/kvm/hyp/include/nvhe/trap_handler.h
@@ -13,6 +13,6 @@
 
 #define cpu_reg(ctxt, r)	(ctxt)->regs.regs[r]
 #define DECLARE_REG(type, name, ctxt, reg)	\
-				type name = (type)cpu_reg(ctxt, (reg))
+				type name; //= (type)cpu_reg(ctxt, (reg))
 
 #endif /* __ARM64_KVM_NVHE_TRAP_HANDLER_H__ */
diff --git a/arch/arm64/kvm/hyp/nvhe/hyp-main.c b/arch/arm64/kvm/hyp/nvhe/hyp-main.c
index 1086ff2..504a857 100644
--- a/arch/arm64/kvm/hyp/nvhe/hyp-main.c
+++ b/arch/arm64/kvm/hyp/nvhe/hyp-main.c
@@ -896,7 +896,7 @@ static void handle___vgic_v3_restore_vmcr_aprs(struct kvm_cpu_context *host_ctxt
 	__vgic_v3_restore_vmcr_aprs(shadow_cpu_if);
 }
 
-static void handle___pkvm_init(struct kvm_cpu_context *host_ctxt)
+static void handle___pkvm_init(int host_ctxt)
 {
 	DECLARE_REG(phys_addr_t, phys, host_ctxt, 1);
 	DECLARE_REG(unsigned long, size, host_ctxt, 2);
@@ -910,7 +910,7 @@ static void handle___pkvm_init(struct kvm_cpu_context *host_ctxt)
 	 * will tail-call in __pkvm_init_finalise() which will have to deal
 	 * with the host context directly.
 	 */
-	cpu_reg(host_ctxt, 1) = __pkvm_init(phys, size, nr_cpus, per_cpu_base,
+	__pkvm_init(phys, size, nr_cpus, per_cpu_base,
 					    hyp_va_bits, iommu_driver);
 }
 
diff --git a/cbmc.sh b/cbmc.sh
new file mode 100755
index 0000000..be29f7a
--- /dev/null
+++ b/cbmc.sh
@@ -0,0 +1,25 @@
+#!/bin/bash
+
+CBMC=cbmc
+TARGET_FILE=arch/arm64/kvm/hyp/nvhe/kvm_nvhe.gb
+
+CHECKS="--bounds-check \
+  --pointer-check \
+  --div-by-zero-check \
+  --signed-overflow-check \
+  --unsigned-overflow-check \
+  --pointer-overflow-check \
+  --conversion-check \
+  --undefined-shift-check \
+  --float-overflow-check \
+  --nan-check \
+  --enum-range-check"
+
+$CBMC \
+  $CHECKS \
+  --nondet-static \
+  --trace \
+  --trace-show-code \
+  --trace-show-function-calls \
+  $@ \
+  $TARGET_FILE