diff --git a/tests/lean/1062.lean b/tests/lean/1062.lean
new file mode 100644
index 0000000000..6b397ac9ee
--- /dev/null
+++ b/tests/lean/1062.lean
@@ -0,0 +1,11 @@
+example : if x = 0 then y + x = y else x ≠ 0 := by
+  simp (config := { contextual := true })
+
+example : if x = 0 then y + x = y else x ≠ 0 := by
+  split
+  simp_all
+  simp_all
+
+example : if x = 0 then y + x = y else x ≠ 0 := by
+  simp (config := { contextual := true })
+  split -- Error: no goals to be solved
diff --git a/tests/lean/1062.lean.expected.out b/tests/lean/1062.lean.expected.out
new file mode 100644
index 0000000000..1ebc0b0b70
--- /dev/null
+++ b/tests/lean/1062.lean.expected.out
@@ -0,0 +1 @@
+1062.lean:11:2-11:7: error: no goals to be solved