fix: reset decision stack in grind linarith (#9904)

This PR ensures the decision stack is reset after an assignment is found
in `grind linarith`.

Closes #9897

src/Lean/Meta/Tactic/Grind/Arith/Linear/Search.lean

@@ -214,7 +214,7 @@ def hasAssignment : LinearM Bool := do
 private def findCase (decVars : FVarIdSet) : SearchM Case := do
   repeat
     let numCases := (← get).cases.size
-    assert! numCases > 0
+    unless numCases > 0 do throwError "`grind linarith` internal cases, cases stack is empty"
     let case := (← get).cases[numCases-1]!
     modify fun s => { s with cases := s.cases.pop }
     if decVars.contains case.fvarId then
@@ -240,12 +240,21 @@ def resolveConflict (h : UnsatProof) : SearchM Unit := do
   trace[grind.debug.linarith.search.backtrack] "resolved diseq split: {← c'.denoteExpr}"
   c'.assert
 
+private def resetDecisionStack : SearchM Unit := do
+  if (← get).cases.isEmpty then
+    -- Nothing to reset
+    return ()
+  -- Backtrack changes but keep the assignment
+  let first := (← get).cases[0]!
+  modifyStruct fun s => { first.saved with assignment := s.assignment }
+
 /-- Search for an assignment/model for the linear constraints. -/
 private def searchAssignmentMain : SearchM Unit := do
   repeat
     trace[grind.debug.linarith.search] "main loop"
     checkSystem "linarith"
     if (← hasAssignment) then
+      trace[grind.debug.linarith.search] "found assignment"
       return ()
     if (← isInconsistent) then
       -- `grind` state is inconsistent
@@ -258,7 +267,7 @@ private def searchAssignmentMain : SearchM Unit := do
       processVar x
 
 private def searchAssignment : LinearM Unit := do
-  searchAssignmentMain |>.run' {}
+  (do searchAssignmentMain; resetDecisionStack) |>.run' {}
 
 /--
 Returns `true` if work/progress has been done.

tests/lean/run/grind_9897.lean

@@ -0,0 +1,21 @@
+def Set' (α : Type u) := α → Prop
+
+namespace Set'
+
+protected def Mem (s : Set' α) (a : α) : Prop :=
+  s a
+
+instance : Membership α (Set' α) :=
+  ⟨Set'.Mem⟩
+
+end Set'
+
+def Ioi' [LT α] (a : α) : Set' α := fun x => a < x
+
+@[grind =] theorem mem_Ioi [LT α] {x a : α} : x ∈ Ioi' a ↔ a < x := Iff.rfl
+
+theorem ProbabilityTheory.crash.extracted_1_3
+    [LE α] [LT α] [DecidableEq α]
+    [Lean.Grind.Ring α] [Lean.Grind.LinearOrder α] [Lean.Grind.OrderedRing α] (X : α → α)
+  (hnonneg : ∀ (i : α), 0 ≤ X i) (n : α) (hn : X n ∉ Ioi' 0) :
+  (if n = X n then 0 else 0) + X n = 0 := by grind