diff --git a/model_checking/src/lib.rs b/model_checking/src/lib.rs
index 78d53813..e7b70af4 100644
--- a/model_checking/src/lib.rs
+++ b/model_checking/src/lib.rs
@@ -158,10 +158,7 @@ pub fn fences() {
 #[cfg_attr(kani, kani::proof)]
 #[cfg_attr(test, test)]
 pub fn read_csr() {
-    let (mut ctx, mctx, mut sail_ctx) = symbolic::new_symbolic_contexts();
-
-    // Infinite number of pmps for the formal verification
-    ctx.nb_pmp = usize::MAX;
+    let (ctx, mctx, mut sail_ctx) = symbolic::new_symbolic_contexts();
 
     let csr_register = generate_csr_register();
 
diff --git a/src/virt/csr.rs b/src/virt/csr.rs
index 2e2bbdd3..d6278854 100644
--- a/src/virt/csr.rs
+++ b/src/virt/csr.rs
@@ -91,7 +91,7 @@ impl RegisterContextGetter<Csr> for VirtContext {
                     log::warn!("Invalid pmpcfg {}", pmp_cfg_idx);
                     return 0;
                 }
-                if pmp_cfg_idx >= self.nb_pmp / 8 {
+                if pmp_cfg_idx >= 2 * self.nb_pmp / 8 {
                     // This PMP is not emulated
                     return 0;
                 }