diff --git a/tests/atomic.8.8.ref b/tests/atomic.8.8.ref
index a3f9185273b897d0d0eebbbde3e4ec0a5bd52004..ced301792b065656ceca683b8866fd3c0d9fa595 100644
--- a/tests/atomic.8.8.ref
+++ b/tests/atomic.8.8.ref
@@ -6,6 +6,7 @@
   Q : iProp Σ
   l : loc
   v : val
+  IPM_INTERNAL : IPM_STATE 3
   ============================
   "Hl" : l ↦ v
   --------------------------------------∗
@@ -36,6 +37,7 @@
   heapG0 : heapG Σ
   P : val → iProp Σ
   Φ : language.val heap_lang → iProp Σ
+  IPM_INTERNAL : IPM_STATE 2
   ============================
   _ : AACC << ∀ x : val, P x
               ABORT AU << ∀ x : val, P x >> @ ⊤, ∅
@@ -68,6 +70,7 @@
   heapG0 : heapG Σ
   l : loc
   Φ : language.val heap_lang → iProp Σ
+  IPM_INTERNAL : IPM_STATE 2
   ============================
   _ : AACC << ∀ x : val, l ↦ x
               ABORT AU << ∀ x : val, l ↦ x >> @ ⊤, ∅ << l ↦ x, COMM Φ #() >> >> 
@@ -99,6 +102,7 @@
   heapG0 : heapG Σ
   l : loc
   Φ : language.val heap_lang → iProp Σ
+  IPM_INTERNAL : IPM_STATE 2
   ============================
   _ : AACC << l ↦ #()
               ABORT AU << l ↦ #() >> @ ⊤, ∅
@@ -131,6 +135,7 @@
   heapG0 : heapG Σ
   l : loc
   Φ : language.val heap_lang → iProp Σ
+  IPM_INTERNAL : IPM_STATE 2
   ============================
   _ : AACC << l ↦ #()
               ABORT AU << l ↦ #() >> @ ⊤, ∅ << l ↦ #(), COMM Φ #() >> >> 
@@ -196,6 +201,7 @@
   heapG0 : heapG Σ
   l : loc
   Φ : language.val heap_lang → iProp Σ
+  IPM_INTERNAL : IPM_STATE 1
   ============================
   _ : AU << ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >> @ ⊤, ∅
          << ∃ yyyy : val, l ↦ yyyy
diff --git a/tests/list_reverse.ref b/tests/list_reverse.ref
index 2c8d900777a7f2ae8771cc1234c9f6b5a14ac975..430c8ed8f19f5c75a20d54c07de9e77a0fad0949 100644
--- a/tests/list_reverse.ref
+++ b/tests/list_reverse.ref
@@ -5,6 +5,7 @@
   hd, acc : val
   xs, ys : list val
   Φ : val → iPropI Σ
+  IPM_INTERNAL : IPM_STATE 2
   ============================
   "Hxs" : is_list hd xs
   "Hys" : is_list acc ys
@@ -16,6 +17,7 @@
   
   Σ : gFunctors
   heapG0 : heapG Σ
+  IPM_INTERNAL : IPM_STATE 2
   acc : val
   ys : list val
   Φ : val → iPropI Σ