diff --git a/src/plugins/wp/share/why3/frama_c_wp/memaddr.mlw b/src/plugins/wp/share/why3/frama_c_wp/memaddr.mlw
index 4d86f2a53f0970b6e563d3d3350a1e388596fc53..bbce544b27c9f648061f32038f22daf6adcfb97d 100644
--- a/src/plugins/wp/share/why3/frama_c_wp/memaddr.mlw
+++ b/src/plugins/wp/share/why3/frama_c_wp/memaddr.mlw
@@ -144,7 +144,7 @@ theory MemAddr
      statically allocated uses static_malloc which is abstract. *)
   lemma valid_pointers_are_statically_allocated:
     forall a: addr, m: malloc, n: int.
-      valid_rd m a n -> statically_allocated (a.base)
+      n > 0 -> valid_rd m a n -> statically_allocated (a.base)
 
   function int_of_addr addr: int
   function addr_of_int int: addr