From d5ca0c7032fe18e5bbdb19600075e01677bca659 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Fri, 24 Oct 2025 21:16:32 -0700
Subject: [PATCH] fix: bug in `cutsat` model construction (#10951)

This PR fixes a bug in the `cutsat` incremental model construction. The
model was not being reset when new (unsatisfied) equalities were
asserted.
---
 .../Tactic/Grind/Arith/Cutsat/EqCnstr.lean     |  2 ++
 .../Meta/Tactic/Grind/Arith/Cutsat/Util.lean   |  8 ++++++++
 tests/lean/run/grind_finish_trace.lean         | 18 ++++++++++++++++++
 3 files changed, 28 insertions(+)

diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean
index 76e665eeab..d730cc5c5b 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean
@@ -359,6 +359,8 @@ def EqCnstr.assertImpl (c : EqCnstr) : GoalM Unit := do
   trace[grind.debug.cutsat.subst] ">> {← getVar x}, {← c.pp}"
   trace[grind.cutsat.assert.store] "{← c.pp}"
   trace[grind.debug.cutsat.elimEq] "{← getVar x}, {← c.pp}"
+  if (← c.satisfied) == .false then
+    resetAssignmentFrom x
   modify' fun s => { s with
     elimEqs := s.elimEqs.set x (some c)
     elimStack := x :: s.elimStack
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Util.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Util.lean
index ab8eb48774..b4643609a1 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Util.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Util.lean
@@ -218,6 +218,14 @@ def DiseqCnstr.satisfied (c : DiseqCnstr) : GoalM LBool := do
   let some v ← c.p.eval? | return .undef
   return v != 0 |>.toLBool
 
+/--
+Returns `.true` if `c` is satisfied by the current partial model,
+`.undef` if `c` contains unassigned variables, and `.false` otherwise.
+-/
+def EqCnstr.satisfied (c : EqCnstr) : GoalM LBool := do
+  let some v ← c.p.eval? | return .undef
+  return v == 0 |>.toLBool
+
 /--
 Given a polynomial `p`, returns `some (x, k, c)` if `p` contains the monomial `k*x`,
 and `x` has been eliminated using the equality `c`.
diff --git a/tests/lean/run/grind_finish_trace.lean b/tests/lean/run/grind_finish_trace.lean
index f0d3424ffe..f0ebcdd30f 100644
--- a/tests/lean/run/grind_finish_trace.lean
+++ b/tests/lean/run/grind_finish_trace.lean
@@ -162,3 +162,21 @@ example (f : Int → Int → Int) (x y : Int)
   grind =>
     -- We can use `have` to golf proofs using `mbtc` and `cases`
     have : x = 1
+
+example (f : Int → Int) (x y : Int)
+    : 0 ≤ x → x ≤ 2 → f 0 = y → f 1 = y → f 2 = y → f x = y := by
+  grind
+
+example (f : Int → Int) (x y : Int)
+    : 0 ≤ x → x ≤ 2 → f 0 = y → f 1 = y → f 2 = y → f x = y := by
+  grind =>
+    mbtc
+    cases #23ad <;> mbtc <;> cases #beb4 <;> mbtc <;> cases #beed
+
+example (f : Int → Int) (x y : Int)
+    : 0 ≤ x → x ≤ 2 → f 0 = y → f 1 = y → f 2 = y → f x = y := by
+  grind =>
+    -- Again, we can use `have` to golf the proof with `mbtc`
+    have : x ≠ 0
+    have : x ≠ 1
+    have : x ≠ 2