[wp] Lookup only ignores primitive terms

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

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 =

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.