def Lean.Meta.Grind.Arith.Offset.mkModel (goal : Goal) : MetaM (Array (Expr × Nat))

Construct a model that satisfies all offset constraints