chore: add test case where grind causes a PANIC

tests/lean/grind/panic.lean

@@ -0,0 +1,35 @@
+-- grind fails, but also produces a panic.
+
+@[grind] inductive star (R : α → α → Prop) : α → α → Prop where
+  | star_refl : ∀ x : α, star R x x
+  | star_step : ∀ x y z, R x y → star R y z → star R x z
+
+set_option grind.debug true
+set_option grind.warning false
+
+inductive com: Type where
+  | SKIP
+  | ASSIGN
+
+inductive cexec : com → Prop where
+
+@[grind] inductive red : com × Nat → com × Nat → Prop where
+  | red_assign: ∀ s, red (.ASSIGN, s) (.SKIP, 0)
+
+/--
+The following theorem causes assertion violation in grind.
+We obtain the following:
+_private.Lean.Meta.Tactic.Grind.Inv.0.Lean.Meta.Grind.checkEqc Lean.Meta.Tactic.Grind.Inv:29:10: assertion violation: isSameExpr e ( __do_lift._@.Lean.Meta.Tactic.Grind.Inv._hyg.31.0 )
+-/
+theorem issue3 (s s' : Nat) (c : com) :
+  star red (c, s) (.SKIP, s') → cexec c := by
+    intro h
+    generalize heq1 : (c, s) = h1
+    generalize heq2 : (com.SKIP, s') = h2
+    rw [heq1, heq2] at h
+    induction h
+    case star_refl =>
+      sorry
+    case star_step r _ a_ih =>
+      -- this is where the assertion violation happens
+      grind