diff --git a/tests/list_reverse.8.10.ref b/tests/list_reverse.8.10.ref
new file mode 100644
index 0000000000000000000000000000000000000000..9440658dbf4e4d8b3cefd1c3f2577fc1afb222fd
--- /dev/null
+++ b/tests/list_reverse.8.10.ref
@@ -0,0 +1,33 @@
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  hd, acc : val
+  xs, ys : list val
+  Φ : val → iPropI Σ
+  ============================
+  "Hxs" : is_list hd xs
+  "Hys" : is_list acc ys
+  "HΦ" : ∀ w : val, is_list w (reverse xs ++ ys) -∗ Φ w
+  --------------------------------------∗
+  WP rev hd acc [{ v, Φ v }]
+  
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  acc : val
+  ys : list val
+  Φ : val → iPropI Σ
+  ============================
+  "Hys" : is_list acc ys
+  "HΦ" : ∀ w : val, is_list w ys -∗ Φ w
+  --------------------------------------∗
+  WP match: InjLV #() with
+       InjL <> => acc
+     | InjR "l" =>
+       let: "tmp1" := Fst ! "l" in
+       let: "tmp2" := Snd ! "l" in
+       "l" <- ("tmp1", acc);; rev "tmp2" (InjLV #())
+     end [{ v, Φ v }]
+