)]}'
{
  "commit": "f45b9cac383dd03c6de58eaa4695f6fcbf1bb1d7",
  "tree": "8985434c73fa85b22fcb32aefcb630e2bd16d01c",
  "parents": [
    "8f6540f9e114b6b71c7277ab56401358397e4716"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Wed Oct 21 02:33:06 2026 +0000"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Wed Oct 21 02:33:12 2026 +0000"
  },
  "message": "feat: dynamic variable reordering before large Cooper splits in `lia`\n\nThis PR makes `lia` reorder its variables instead of enumerating a Cooper case split with many cases, which fixes goals such as a three-limb counter increment that previously needed a `2^32`-way split.\n\nA split on `x` has as many cases as the coefficient of `x` in the conflicting bounds. The search now abandons such a split, orders `x` first so that it becomes a parameter of those bounds, and restarts; the conflict then surfaces at a variable with a smaller coefficient. Two new options control it: `liaReorderCases` (default 16), the case count above which a reordering is requested, and `liaReorders` (default 8), the maximum number of reorderings per goal, with `0` disabling the mechanism.\n\nCo-Authored-By: Claude Fable 5.1 \u003cnoreply@anthropic.com\u003e\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "b4274d4b4dbb8557bdaaea3fead68679ee7b9446",
      "old_mode": 33188,
      "old_path": "src/Init/Grind/Config.lean",
      "new_id": "d291a5470c24202106e4c63296f8ad9d7c6117dd",
      "new_mode": 33188,
      "new_path": "src/Init/Grind/Config.lean"
    },
    {
      "type": "modify",
      "old_id": "99bebf6738a914e82dbef01d43028797b28934aa",
      "old_mode": 33188,
      "old_path": "src/Init/Grind/Tactics.lean",
      "new_id": "02ced42651e2d5be5a7f64d643ea4315776c3f94",
      "new_mode": 33188,
      "new_path": "src/Init/Grind/Tactics.lean"
    },
    {
      "type": "modify",
      "old_id": "e66ac0ea05915741a99407d43ebc91e59653d2b3",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Grind/Arith/Cutsat/ReorderVars.lean",
      "new_id": "c2daf8473f96423711135d39aea628a7517970b7",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Grind/Arith/Cutsat/ReorderVars.lean"
    },
    {
      "type": "modify",
      "old_id": "02ea4beab944e6fe96184ce5d46d876c56b3be36",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Search.lean",
      "new_id": "014642c8cb2314ed1ce75717b026ef8c01108e64",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Search.lean"
    },
    {
      "type": "modify",
      "old_id": "e156a266b2c9b7661e605e7f04bf8a7b4e6a39e9",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Grind/Arith/Cutsat/SearchM.lean",
      "new_id": "d060f114e16d8a5be4563ff1723b620af5083aef",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Grind/Arith/Cutsat/SearchM.lean"
    },
    {
      "type": "modify",
      "old_id": "1e053c8e54134d23a7bf65b7ed81d65f8a26ff22",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean",
      "new_id": "51eee5ab1730d116545369c2d1b402648dde028d",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "6af354e4b837ff71c90aaded004ebfe367f8d12a",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_lia_reorder_request.lean"
    }
  ]
}