diff --git a/tests/heap_lang2.ref b/tests/heap_lang2.ref
index 73cfb45d336fd9ea12cad338636bc4b649d44d26..b21642a0e1a96a6609de640e70a958c401508a6f 100644
--- a/tests/heap_lang2.ref
+++ b/tests/heap_lang2.ref
@@ -1,5 +1,12 @@
 1 subgoal
   
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  P, Q : iProp Σ
+  ============================
+  P ={⊤}=∗ Q
+1 subgoal
+  
   Σ : gFunctors
   heapG0 : heapG Σ
   fun1, fun2, fun3 : expr
@@ -10,3 +17,14 @@
      let: "val3" := fun3 "val2" in if: "val1" = "val2" then "val" else "val3"
   {{ _, True }}
   
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  fun1, fun2, fun3 : expr
+  ============================
+  {{{ True }}}
+    let: "val1" := fun1 #() in
+    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 }}}
diff --git a/tests/heap_lang2.v b/tests/heap_lang2.v
index 4ec6061ccf3f41787e5b1c017043c424d7d7d00f..334732089d05f98a877f5ded545789a5d930a002 100644
--- a/tests/heap_lang2.v
+++ b/tests/heap_lang2.v
@@ -8,6 +8,10 @@ Set Default Proof Using "Type".
 Section printing_tests.
   Context `{!heapG Σ}.
 
+  Lemma vs_print (P Q : iProp Σ) :
+    P ={⊤}=∗ Q.
+  Proof. Show. Abort.
+
   Lemma wp_print_long_expr (fun1 fun2 fun3 : expr) :
     True -∗ WP let: "val1" := fun1 #() in
        let: "val2" := fun2 "val1" in
@@ -17,4 +21,13 @@ Section printing_tests.
     iIntros "_". Show.
   Abort.
 
+  Lemma texan_triple_long_expr (fun1 fun2 fun3 : expr) :
+    {{{ True }}}
+       let: "val1" := fun1 #() in
+       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 }}}.
+  Proof. Show. Abort.
+
 End printing_tests.