diff --git a/src/plugins/wp/MemVar.ml b/src/plugins/wp/MemVar.ml
index 854010dbff5acdee3f50abd66f1041bb38950127..a693fa73f0bdf2b988654090ec45f2e7e849750f 100644
--- a/src/plugins/wp/MemVar.ml
+++ b/src/plugins/wp/MemVar.ml
@@ -1067,7 +1067,7 @@ struct
         end
     | Rrange(l,elt, Some a, Some b) ->
         begin match l with
-          | Ref x -> noref ~op:"initialized sub-range of" x
+          | Ref _ -> p_true
           | Loc l -> M.initialized sigma.mem (Rrange(l,elt,Some a, Some b))
           | Val(m,x,p) ->
               try