diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index 9bddbbb8b7cec241a216317ee3abdc29f7b59201..38671e22036e0fa707fc9333650fc62e95c4ae5d 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -30,6 +30,33 @@
      let: "val3" := fun3 "val2" in if: "val1" = "val2" then "val" else "val3"
   {{ _, True }}
   
+1 subgoal
+  
+  Σ : gFunctors
+  H : heapG Σ
+  fun1, fun2, fun3 : expr
+  Φ : language.val heap_lang → iProp Σ
+  ============================
+  --------------------------------------∗
+  WP let: "val1" := fun1 #() in
+     let: "val2" := fun2 "val1" in
+     let: "v" := fun3 "v" in if: "v" = "v" then "v" else "v" 
+  {{ v, Φ v }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  H : heapG Σ
+  fun1, fun2, fun3 : expr
+  Φ : language.val heap_lang → iProp Σ
+  E : coPset
+  ============================
+  --------------------------------------∗
+  WP let: "val1" := fun1 #() in
+     let: "val2" := fun2 "val1" in
+     let: "v" := fun3 "v" in if: "v" = "v" then "v" else "v" 
+  @ E {{ v, Φ v }}
+  
 1 subgoal
   
   Σ : gFunctors