diff --git a/tests/heap_lang_printing.ref b/tests/heap_lang_printing.ref
index df425cad2f0aac41f7656d1a9cc95a1e99df61f5..b9f357b8ad41ef51565a202f9668dacf0d3f609d 100644
--- a/tests/heap_lang_printing.ref
+++ b/tests/heap_lang_printing.ref
@@ -23,27 +23,123 @@
   Σ : gFunctors
   heapGS0 : heapGS Σ
   fun1, fun2, fun3 : expr
-  Φ : language.val heap_lang → iPropI Σ
+  ============================
+  --------------------------------------∗
+  WP fun1 #()
+  {{ v, WP let: "val1" := v in
+           let: "val2" := fun2 "val1" in
+           let: "val3" := fun3 "val2" in
+           if: "val1" = "val2" then "val" else "val3" 
+        {{ _, True }} }}
+  
+1 goal
+  
+  Σ : gFunctors
+  heapGS0 : heapGS Σ
+  fun1, fun2, fun3 : expr
+  long_post : iPropI Σ
   ============================
   --------------------------------------∗
   WP let: "val1" := fun1 #() in
      let: "val2" := fun2 "val1" in
-     let: "v" := fun3 "v" in if: "v" = "v" then "v" else "v" 
-  {{ v, Φ v }}
+     let: "v" := fun3 "v" in if: "v" = "v" then "v" else "v"
+  {{ _, long_post
+        ∗ long_post
+          ∗ long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post }}
   
 1 goal
   
   Σ : gFunctors
   heapGS0 : heapGS Σ
   fun1, fun2, fun3 : expr
-  Φ : language.val heap_lang → iPropI Σ
-  E : coPset
+  long_post : iPropI Σ
   ============================
   --------------------------------------∗
-  WP let: "val1" := fun1 #() in
+  WP fun1 #()
+  {{ v, WP let: "val1" := v in
+           let: "val2" := fun2 "val1" in
+           let: "v" := fun3 "v" in if: "v" = "v" then "v" else "v"
+        {{ _, long_post
+              ∗ long_post
+                ∗ long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post }} }}
+  
+1 goal
+  
+  Σ : gFunctors
+  heapGS0 : heapGS Σ
+  l1 : loc
+  fun2, fun3 : expr
+  long_post : iPropI Σ
+  N : namespace
+  E_long : coPset
+  H : ↑N ⊆ E_long
+  ============================
+  "Hinv" : inv N True
+  --------------------------------------∗
+  WP let: "val1" := ! #l1 in
      let: "val2" := fun2 "val1" in
-     let: "v" := fun3 "v" in if: "v" = "v" then "v" else "v" 
-  @ E {{ v, Φ v }}
+     let: "v" := fun3 "v" in if: "v" = "v" then "v" else "v"
+  @ E_long {{ _, long_post
+                 ∗ long_post
+                   ∗ long_post
+                     ∗ long_post ∗ long_post ∗ long_post ∗ long_post }}
+  
+1 goal
+  
+  Σ : gFunctors
+  heapGS0 : heapGS Σ
+  l1 : loc
+  fun2, fun3 : expr
+  long_post : iPropI Σ
+  N : namespace
+  E_long : coPset
+  H : ↑N ⊆ E_long
+  ============================
+  "Hinv" : inv N True
+  --------------------------------------∗
+  WP ! #l1
+  @ E_long {{ v, WP let: "val1" := v in
+                    let: "val2" := fun2 "val1" in
+                    let: "v" := fun3 "v" in if: "v" = "v" then "v" else "v"
+                 @ E_long {{ _, long_post
+                                ∗ long_post
+                                  ∗ long_post
+                                    ∗ long_post
+                                      ∗ long_post ∗ long_post ∗ long_post }} }}
+  
+1 goal
+  
+  Σ : gFunctors
+  heapGS0 : heapGS Σ
+  l1 : loc
+  fun2, fun3 : expr
+  long_post : iPropI Σ
+  N : namespace
+  E_long : coPset
+  H : ↑N ⊆ E_long
+  ============================
+  --------------------------------------∗
+  WP ! #l1
+  @ E_long ∖ ↑N {{ v, |={E_long ∖ ↑N}=> ▷ True
+                                        ∗ WP let: "val1" := 
+                                             v in
+                                             let: "val2" := 
+                                             fun2 "val1" in
+                                             let: "v" := 
+                                             fun3 "v" in
+                                             if: "v" = "v" then "v" else "v"
+                                          @ E_long {{ _, 
+                                                 long_post
+                                                 ∗ 
+                                                 long_post
+                                                 ∗ 
+                                                 long_post
+                                                 ∗ 
+                                                 long_post
+                                                 ∗ 
+                                                 long_post
+                                                 ∗ 
+                                                 long_post ∗ long_post }} }}
   
 1 goal
   
@@ -56,3 +152,30 @@
     let: "val2" := fun2 "val1" in
     let: "val3" := fun3 "val2" in if: "val1" = "val2" then "val" else "val3"
   {{{ (x y : val) (z : Z), RET (x, y, #z); True }}}
+1 goal
+  
+  Σ : gFunctors
+  heapGS0 : heapGS Σ
+  fun1, fun2, fun3 : expr
+  E_mask_is_long_too : coPset
+  ============================
+  {{{ True }}}
+    let: "val1" := fun1 #() in
+    let: "val2" := fun2 "val1" in
+    let: "val3" := fun3 "val2" in if: "val1" = "val2" then "val" else "val3"
+  @ E_mask_is_long_too {{{ (x y : val) (z : Z), RET 
+  (x, y, #z); True }}}
+1 goal
+  
+  Σ : gFunctors
+  heapGS0 : heapGS Σ
+  fun1, fun2, fun3 : expr
+  long_post : iPropI Σ
+  E_mask_is_long_too : coPset
+  ============================
+  {{{ True }}}
+    let: "val1" := fun1 #() in
+    let: "val2" := fun2 "val1" in
+    let: "val3" := fun3 "val2" in if: "val1" = "val2" then "val" else "val3"
+  @ E_mask_is_long_too {{{ (x y : val) (z : Z), RET 
+  (x, y, #z); long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post }}}
diff --git a/tests/heap_lang_printing.v b/tests/heap_lang_printing.v
index 31e92bd610f33697be896eb618178bd55f51f4c4..c580e42b7c987debe04d963a2811eef3fb3d8645 100644
--- a/tests/heap_lang_printing.v
+++ b/tests/heap_lang_printing.v
@@ -27,24 +27,32 @@ Section printing_tests.
        if: "val1" = "val2" then "val" else "val3"  {{ _, True }}.
   Proof.
     iIntros "_". Show.
+    wp_bind (fun1 #()). Show.
   Abort.
 
-  Lemma wp_print_long_expr (fun1 fun2 fun3 : expr) Φ :
+  Lemma wp_print_long_expr (fun1 fun2 fun3 : expr) long_post :
     True -∗ WP let: "val1" := fun1 #() in
        let: "val2" := fun2 "val1" in
        let: "v" := fun3 "v" in
-       if: "v" = "v" then "v" else "v"  {{ Φ }}.
+       if: "v" = "v" then "v" else "v"
+    {{ _, long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post }}.
   Proof.
     iIntros "_". Show.
+    wp_bind (fun1 #()). Show.
   Abort.
 
-  Lemma wp_print_long_expr (fun1 fun2 fun3 : expr) Φ E :
-    True -∗ WP let: "val1" := fun1 #() in
+  Lemma wp_print_long_expr (l1 : loc) (fun2 fun3 : expr) long_post N E_long :
+    ↑N ⊆ E_long →
+    inv N True -∗ WP let: "val1" := ! #l1 in
        let: "val2" := fun2 "val1" in
        let: "v" := fun3 "v" in
-       if: "v" = "v" then "v" else "v" @ E {{ Φ }}.
+       if: "v" = "v" then "v" else "v"
+    @ E_long
+    {{ _, long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post }}.
   Proof.
-    iIntros "_". Show.
+    iIntros (?) "Hinv". Show.
+    wp_bind (! #l1)%E. Show.
+    iInv "Hinv" as "_". Show.
   Abort.
 
   Lemma texan_triple_long_expr (fun1 fun2 fun3 : expr) :
@@ -56,4 +64,24 @@ Section printing_tests.
     {{{ (x y : val) (z : Z), RET (x, y, #z); True }}}.
   Proof. Show. Abort.
 
+  Lemma texan_triple_long_expr_mask (fun1 fun2 fun3 : expr) E_mask_is_long_too :
+    {{{ True }}}
+       let: "val1" := fun1 #() in
+       let: "val2" := fun2 "val1" in
+       let: "val3" := fun3 "val2" in
+       if: "val1" = "val2" then "val" else "val3"
+    @ E_mask_is_long_too
+    {{{ (x y : val) (z : Z), RET (x, y, #z); True }}}.
+  Proof. Show. Abort.
+
+  Lemma texan_triple_long_expr_mask_post (fun1 fun2 fun3 : expr) long_post E_mask_is_long_too :
+    {{{ True }}}
+       let: "val1" := fun1 #() in
+       let: "val2" := fun2 "val1" in
+       let: "val3" := fun3 "val2" in
+       if: "val1" = "val2" then "val" else "val3"
+    @ E_mask_is_long_too
+    {{{ (x y : val) (z : Z), RET (x, y, #z); long_post ∗ long_post ∗ long_post ∗ long_post ∗ long_post }}}.
+  Proof. Show. Abort.
+
 End printing_tests.