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

@@ -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

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