From 032a9e817d8d8d4dbbdf13c44702f0359ff4b62b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Fri, 28 Mar 2025 18:05:20 -0700
Subject: [PATCH] fix: bug in `grind` model-based theory combination (#7714)

This PR fixes an assertion violation in the `grind` model-based theory
combination module.
---
 src/Lean/Meta/Tactic/Grind/Arith/Cutsat/MBTC.lean  | 4 ++--
 src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Model.lean | 6 +++---
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/MBTC.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/MBTC.lean
index 415b91dbc0..c05cf1f3c6 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/MBTC.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/MBTC.lean
@@ -12,7 +12,7 @@ import Lean.Meta.Tactic.Grind.Arith.Cutsat.Model
 namespace Lean.Meta.Grind.Arith.Cutsat
 
 private def getAssignmentExt? (e : Expr) : GoalM (Option Rat) := do
-  let val? ← getAssignment? (← get) (← getENode e)
+  let val? ← getAssignment? (← get) e
   if val?.isSome then
     return val?
   let type ← inferType e
@@ -20,7 +20,7 @@ private def getAssignmentExt? (e : Expr) : GoalM (Option Rat) := do
     for parent in (← getParents e) do
       let_expr NatCast.natCast _ inst _ := parent | pure ()
       let_expr instNatCastInt := inst | pure ()
-      return (← getAssignment? (← get) (← getENode parent))
+      return (← getAssignment? (← get) parent)
   return none
 
 private def hasTheoryVar (e : Expr) : GoalM Bool := do
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Model.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Model.lean
index 7821d5ad0f..36a75d5293 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Model.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Model.lean
@@ -69,8 +69,8 @@ private def assignEqc (goal : Goal) (e : Expr) (v : Rat) (a : Std.HashMap Expr R
     a := a.insert e v
   return a
 
-def getAssignment? (goal : Goal) (node : ENode) : MetaM (Option Rat) := do
-  assert! isSameExpr node.self node.root
+def getAssignment? (goal : Goal) (e : Expr) : MetaM (Option Rat) := do
+  let node ← goal.getENode (← goal.getRoot e)
   if let some v := getCutsatAssignment? goal node then
     return some v
   else if let some v ← getIntValue? node.self then
@@ -97,7 +97,7 @@ def mkModel (goal : Goal) : MetaM (Array (Expr × Rat)) := do
   for node in nodes do
     if isSameExpr node.root node.self then
     if (← isIntNatENode node) then
-      if let some v ← getAssignment? goal node then
+      if let some v ← getAssignment? goal node.self then
         if v.den == 1 then used := used.insert v.num
         model := assignEqc goal node.self v model
   -- Assign cast terms