diff --git a/src/plugins/wp/Conditions.ml b/src/plugins/wp/Conditions.ml
index d6e531f56be84457ef273df9c4db17a9d8391ccd..1ff6550e70594e0042b4520ed530a9c3a98ef8cd 100644
--- a/src/plugins/wp/Conditions.ml
+++ b/src/plugins/wp/Conditions.ml
@@ -1595,9 +1595,11 @@ struct
     let visited = ref Tset.empty in
     let rec term_is_init_in_states states t =
       let raise_if_is_init t s =
-        match Mstate.lookup s t with
-        | Mlval(_, KInit) | Mchunk(_, KInit) -> raise Found
-        | _ -> ()
+        if Lang.F.is_primitive t then ()
+        else
+          match Mstate.lookup s t with
+          | Mlval(_, KInit) | Mchunk(_, KInit) -> raise Found
+          | _ -> ()
       in
       if Tset.mem t !visited then ()
       else begin
diff --git a/src/plugins/wp/MemVar.ml b/src/plugins/wp/MemVar.ml
index a718b83125210523236163b716cb4c9db4c8ea81..6706a5a6f194fc3767189e66f288eb3ea5eb8222 100644
--- a/src/plugins/wp/MemVar.ml
+++ b/src/plugins/wp/MemVar.ml
@@ -453,11 +453,7 @@ struct
     | Iinit _ -> Sigs.Mlval (ilval c, KInit)
 
   let lookup s e =
-    try
-      (* If the term is closed, any variable simplified to [e] can match. Thus,
-         we could return a variable that equals to [e] but is not really [e]. *)
-      if Lang.F.is_closed e then Sigs.Mterm
-      else imval (Tmap.find e s.svar)
+    try imval (Tmap.find e s.svar)
     with Not_found -> M.lookup s.smem e
 
   let apply f s =
diff --git a/src/plugins/wp/tests/wp_tip/oracle/chunk_printing.res.oracle b/src/plugins/wp/tests/wp_tip/oracle/chunk_printing.res.oracle
index 091d995adcda4b3e5bcbbd9b4fd615c9932cf7d4..598ec02c22b31480783d0e71c8ee206b3c3ca225 100644
--- a/src/plugins/wp/tests/wp_tip/oracle/chunk_printing.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle/chunk_printing.res.oracle
@@ -17,10 +17,10 @@ Assume {
   Stmt { L1:  }
   Stmt { x.a = `v;  }
   (* Call 'get_int' *)
-  Have: ((x@L1.F1_V_a) = `v) \/ (« null->a »@L1 = `v).
+  Have: ((x@L1.F1_V_a) = `v) \/ (« y->a »@L1 = `v).
   Stmt { x.b = `v_1;  }
   (* Call 'get_uint' *)
-  Have: ((x@L1.F1_V_b) = `v_1) \/ (« null->b »@L1 = `v_1).
+  Have: ((x@L1.F1_V_b) = `v_1) \/ (« y->b »@L1 = `v_1).
 }
 Prove: `x_2 = `x_1.