diff --git a/tests/atomic.8.9.ref b/tests/atomic.8.7.ref
similarity index 96%
rename from tests/atomic.8.9.ref
rename to tests/atomic.8.7.ref
index c51ade4ecb45eae71cc5255da2e926e868412fbc..af5aa0bbc9bfb2f551a55650446276679623defe 100644
--- a/tests/atomic.8.9.ref
+++ b/tests/atomic.8.7.ref
@@ -348,8 +348,8 @@
   ============================
   --------------------------------------∗
   ∀ Φ : language.val heap_lang → iProp Σ,
-    AU << ∀ x : val, P x >> @ ⊤, ∅ << ∃ y : val, P y, COMM Φ #() >>
-    -∗ WP ! #0 {{ v, Φ v }}
+  AU << ∀ x : val, P x >> @ ⊤, ∅ << ∃ y : val, P y, COMM Φ #() >>
+  -∗ WP ! #0 {{ v, Φ v }}
   
 1 subgoal
   
@@ -359,11 +359,11 @@
   Φ : language.val heap_lang → iProp Σ
   ============================
   "AU" : ∃ x : val,
-           P x
-           ∗ (P x
-              ={∅,⊤}=∗ AU << ∀ x0 : val, P x0 >> @ ⊤, ∅
-                          << ∃ y : val, P y, COMM Φ #() >>)
-             ∧ (∀ x0 : val, P x0 ={∅,⊤}=∗ Φ #())
+         P x
+         ∗ (P x
+            ={∅,⊤}=∗ AU << ∀ x0 : val, P x0 >> @ ⊤, ∅
+                        << ∃ y : val, P y, COMM Φ #() >>)
+           ∧ (∀ x0 : val, P x0 ={∅,⊤}=∗ Φ #())
   --------------------------------------∗
   WP ! #0 @ ∅ {{ v, |={∅,⊤}=> Φ v }}
   
diff --git a/tests/atomic.8.8.ref b/tests/atomic.8.8.ref
new file mode 100644
index 0000000000000000000000000000000000000000..238708315a1656731ecc3a853489338db7c99e9d
--- /dev/null
+++ b/tests/atomic.8.8.ref
@@ -0,0 +1,371 @@
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  P : val → iProp Σ
+  ============================
+  <<< ∀ x : val, P x >>> code @ ⊤ <<< ∃ y : val, P y, RET #() >>>
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  P : val → iProp Σ
+  Q : iPropI Σ
+  Φ : language.val heap_lang → iProp Σ
+  ============================
+  _ : Q
+  "AU" : AU << ∀ x : val, P x >> @ ⊤, ∅ << ∃ y : val, P y, COMM Q -∗ Φ #() >>
+  --------------------------------------∗
+  WP code {{ v, Φ v }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  P : val → iProp Σ
+  Q : iPropI Σ
+  Φ : language.val heap_lang → iProp Σ
+  ============================
+  _ : Q
+  _ : AACC << ∀ x : val, P x
+              ABORT AU << ∀ x : val, P x >> @ ⊤, ∅
+                       << ∃ y : val, P y, COMM Q -∗ Φ #() >> >> @ ⊤, ∅
+           << ∃ y : val, P y, COMM Q -∗ Φ #() >>
+  --------------------------------------∗
+  WP code {{ v, Φ v }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  ============================
+  <<< ∀ x : val, l ↦ x >>> code @ ⊤ <<< l ↦ x, RET #() >>>
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  Q : iPropI Σ
+  Φ : language.val heap_lang → iProp Σ
+  ============================
+  _ : Q
+  "AU" : AU << ∀ x : val, l ↦ x >> @ ⊤, ∅ << l ↦ x, COMM Q -∗ Φ #() >>
+  --------------------------------------∗
+  WP code {{ v, Φ v }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  Q : iPropI Σ
+  Φ : language.val heap_lang → iProp Σ
+  ============================
+  _ : Q
+  _ : AACC << ∀ x : val, l ↦ x
+              ABORT AU << ∀ x : val, l ↦ x >> @ ⊤, ∅
+                       << l ↦ x, COMM Q -∗ Φ #() >> >> @ ⊤, ∅
+           << l ↦ x, COMM Q -∗ Φ #() >>
+  --------------------------------------∗
+  WP code {{ v, Φ v }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  ============================
+  <<< l ↦ #() >>> code @ ⊤ <<< ∃ y : val, l ↦ y, RET #() >>>
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  Q : iPropI Σ
+  Φ : language.val heap_lang → iProp Σ
+  ============================
+  _ : Q
+  "AU" : AU << l ↦ #() >> @ ⊤, ∅ << ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >>
+  --------------------------------------∗
+  WP code {{ v, Φ v }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  Q : iPropI Σ
+  Φ : language.val heap_lang → iProp Σ
+  ============================
+  _ : Q
+  _ : AACC << l ↦ #()
+              ABORT AU << l ↦ #() >> @ ⊤, ∅
+                       << ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >> >> @ ⊤, ∅
+           << ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >>
+  --------------------------------------∗
+  WP code {{ v, Φ v }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  ============================
+  <<< l ↦ #() >>> code @ ⊤ <<< l ↦ #(), RET #() >>>
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  Q : iPropI Σ
+  Φ : language.val heap_lang → iProp Σ
+  ============================
+  _ : Q
+  "AU" : AU << l ↦ #() >> @ ⊤, ∅ << l ↦ #(), COMM Q -∗ Φ #() >>
+  --------------------------------------∗
+  WP code {{ v, Φ v }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  Q : iPropI Σ
+  Φ : language.val heap_lang → iProp Σ
+  ============================
+  _ : Q
+  _ : AACC << l ↦ #()
+              ABORT AU << l ↦ #() >> @ ⊤, ∅ << l ↦ #(), COMM Q -∗ Φ #() >> >> 
+           @ ⊤, ∅ << l ↦ #(), COMM Q -∗ Φ #() >>
+  --------------------------------------∗
+  WP code {{ v, Φ v }}
+  
+"Now come the long pre/post tests"
+     : string
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  ============================
+  <<< ∀ x : val, l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< ∃ y : val, l ↦ y, RET #() >>>
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  Q : iPropI Σ
+  Φ : language.val heap_lang → iProp Σ
+  ============================
+  _ : Q
+  "AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x >> @ ⊤, ∅
+            << ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >>
+  --------------------------------------∗
+  WP code {{ v, Φ v }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  ============================
+  <<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
+    code @ ⊤
+  <<< ∃ y : val, l ↦ y, RET #() >>>
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  Q : iPropI Σ
+  Φ : language.val heap_lang → iProp Σ
+  ============================
+  _ : Q
+  "AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>
+            @ ⊤, ∅ << ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >>
+  --------------------------------------∗
+  WP code {{ v, Φ v }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  ============================
+  <<< ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
+    code @ ⊤
+  <<< ∃ yyyy : val, l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
+      RET #() >>>
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  Q : iPropI Σ
+  Φ : language.val heap_lang → iProp Σ
+  ============================
+  _ : Q
+  _ : AU << ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >> @ ⊤, ∅
+         << ∃ yyyy : val, l ↦ yyyy
+                          ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
+            COMM Q -∗ Φ #() >>
+  --------------------------------------∗
+  WP code {{ v, Φ v }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  ============================
+  <<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
+    code @ ⊤
+  <<< l ↦ x, RET #() >>>
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  Q : iPropI Σ
+  Φ : language.val heap_lang → iProp Σ
+  ============================
+  _ : Q
+  "AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> @ ⊤, ∅
+            << l ↦ x, COMM Q -∗ Φ #() >>
+  --------------------------------------∗
+  WP code {{ v, Φ v }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  x : val
+  ============================
+  <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
+    code @ ⊤
+  <<< ∃ y : val, l ↦ y, RET #() >>>
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  x : val
+  Q : iPropI Σ
+  Φ : language.val heap_lang → iProp Σ
+  ============================
+  _ : Q
+  "AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> @ ⊤, ∅
+            << ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >>
+  --------------------------------------∗
+  WP code {{ v, Φ v }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  x : val
+  ============================
+  <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
+    code @ ⊤
+  <<< l ↦ #(), RET #() >>>
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  x : val
+  Q : iPropI Σ
+  Φ : language.val heap_lang → iProp Σ
+  ============================
+  _ : Q
+  "AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> @ ⊤, ∅
+            << l ↦ #(), COMM Q -∗ Φ #() >>
+  --------------------------------------∗
+  WP code {{ v, Φ v }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  xx, yyyy : val
+  ============================
+  <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
+    code @ ⊤
+  <<< l ↦ yyyy, RET #() >>>
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  xx, yyyy : val
+  Q : iPropI Σ
+  Φ : language.val heap_lang → iProp Σ
+  ============================
+  _ : Q
+  "AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>
+            @ ⊤, ∅ << l ↦ yyyy, COMM Q -∗ Φ #() >>
+  --------------------------------------∗
+  WP code {{ v, Φ v }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  xx, yyyy : val
+  ============================
+  <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
+    code @ ⊤
+  <<< l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
+      RET #() >>>
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  xx, yyyy : val
+  Q : iPropI Σ
+  Φ : language.val heap_lang → iProp Σ
+  ============================
+  _ : Q
+  "AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >> @ ⊤, ∅
+            << l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
+               COMM Q -∗ Φ #() >>
+  --------------------------------------∗
+  WP code {{ v, Φ v }}
+  
+"Prettification"
+     : string
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  P : val → iProp Σ
+  ============================
+  --------------------------------------∗
+  ∀ Φ : language.val heap_lang → iProp Σ, AU << ∀ 
+                                             x : val, 
+                                             P x >> @ ⊤, ∅
+                                             << ∃ y : val, P y, COMM Φ #() >>
+                                          -∗ WP ! #0 {{ v, Φ v }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  P : val → iProp Σ
+  Φ : language.val heap_lang → iProp Σ
+  ============================
+  "AU" : ∃ x : val, P x
+                    ∗ (P x
+                       ={∅,⊤}=∗ AU << ∀ x0 : val, 
+                                   P x0 >> @ ⊤, ∅
+                                   << ∃ y : val, P y, COMM Φ #() >>)
+                      ∧ (∀ x0 : val, P x0 ={∅,⊤}=∗ Φ #())
+  --------------------------------------∗
+  WP ! #0 @ ∅ {{ v, |={∅,⊤}=> Φ v }}
+  
diff --git a/tests/atomic.ref b/tests/atomic.ref
index 238708315a1656731ecc3a853489338db7c99e9d..c51ade4ecb45eae71cc5255da2e926e868412fbc 100644
--- a/tests/atomic.ref
+++ b/tests/atomic.ref
@@ -347,11 +347,9 @@
   P : val → iProp Σ
   ============================
   --------------------------------------∗
-  ∀ Φ : language.val heap_lang → iProp Σ, AU << ∀ 
-                                             x : val, 
-                                             P x >> @ ⊤, ∅
-                                             << ∃ y : val, P y, COMM Φ #() >>
-                                          -∗ WP ! #0 {{ v, Φ v }}
+  ∀ Φ : language.val heap_lang → iProp Σ,
+    AU << ∀ x : val, P x >> @ ⊤, ∅ << ∃ y : val, P y, COMM Φ #() >>
+    -∗ WP ! #0 {{ v, Φ v }}
   
 1 subgoal
   
@@ -360,12 +358,12 @@
   P : val → iProp Σ
   Φ : language.val heap_lang → iProp Σ
   ============================
-  "AU" : ∃ x : val, P x
-                    ∗ (P x
-                       ={∅,⊤}=∗ AU << ∀ x0 : val, 
-                                   P x0 >> @ ⊤, ∅
-                                   << ∃ y : val, P y, COMM Φ #() >>)
-                      ∧ (∀ x0 : val, P x0 ={∅,⊤}=∗ Φ #())
+  "AU" : ∃ x : val,
+           P x
+           ∗ (P x
+              ={∅,⊤}=∗ AU << ∀ x0 : val, P x0 >> @ ⊤, ∅
+                          << ∃ y : val, P y, COMM Φ #() >>)
+             ∧ (∀ x0 : val, P x0 ={∅,⊤}=∗ Φ #())
   --------------------------------------∗
   WP ! #0 @ ∅ {{ v, |={∅,⊤}=> Φ v }}