From e69e469a377be7f0a166c0def6622c1d925fc670 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 18 Apr 2022 11:56:46 -0700
Subject: [PATCH] chore: update test

---
 tests/playground/sleep_save.lean | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/tests/playground/sleep_save.lean b/tests/playground/sleep_save.lean
index d432f1db9f..fb2724d6de 100644
--- a/tests/playground/sleep_save.lean
+++ b/tests/playground/sleep_save.lean
@@ -29,4 +29,9 @@ example (h₁ : p ∨ q) (h₂ : p → x = 0) (h₃ : q → y = 0) : x * y = 0 :
     save
     have : y = 0 := h₃ h
     simp [*]
-  | inl h => stop done
+  | inl h => stop
+    expensive_tactic
+    save
+    have : x = 0 := h₂ h
+    simp [*]
+    done