From 22bc264a8294c2c6eaaca143910efc2268ecdc04 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 2 Oct 2021 10:45:53 -0400
Subject: [PATCH] add a test

---
 tests/heap_lang.v | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index a83b6662d..1c4d73212 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -368,6 +368,11 @@ Section mapsto_tests.
     iIntros (Φ) "Hl HΦ". Show. wp_load. by iApply "HΦ".
   Qed.
 
+  (* Make sure that we can split a mapsto containing an evar. *)
+  Lemma mapsto_evar_iSplit l v :
+    l ↦{#1 / 2} v -∗  ∃ q, l ↦{#1 / 2 + q} v.
+  Proof. iIntros "H". iExists _. iSplitL; first by iAssumption. Abort.
+
 End mapsto_tests.
 
 Section inv_mapsto_tests.
-- 
GitLab