From ea355392b5ccf9f4fb014d7347e209f0436f21a0 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 14 Jun 2018 13:21:32 +0200
Subject: [PATCH] forgot to update reference output

---
 tests/heap_lang.ref | 27 +++++++++++++++++++++++++++
 1 file changed, 27 insertions(+)

diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index 9bddbbb8b..38671e220 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
-- 
GitLab