)]}'
{
  "commit": "47df859469f50a9b0e7e5ff143c3ea438b86f0d1",
  "tree": "9e062f7b5ae9bbf16318f8cf3d773dd9725287b3",
  "parents": [
    "c0521efb94e75b1faa1b711b841986e3a645e73e"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Wed Oct 21 01:38:23 2026 +0000"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Wed Oct 21 01:38:30 2026 +0000"
  },
  "message": "fix: prefer decision-free explanations of conflicts in the `lia` model search\n\nThis PR fixes a regression from #15827 where `lia` enumerated all cases of a Cooper split although the untightened bounds refuted every case at once.\n\nA bound tightened with a divisibility constraint of the current case yields a conflict that depends on the case. The search now keeps, per side, the best bound with all tightenings and the best bound tightened only with constraints that do not depend on decisions. The former selects values; the latter explains conflicts whenever it conflicts as well, so that the goal is closed instead of moving to the next case.\n\nCo-Authored-By: Claude Fable 5.1 \u003cnoreply@anthropic.com\u003e\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "f697f78c9d208e339667885378f785195a88e994",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Search.lean",
      "new_id": "02ea4beab944e6fe96184ce5d46d876c56b3be36",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Search.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "0f5d3380ab38846cd6b170799dad0cf3513de3a4",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_lia_decfree_conflicts.lean"
    }
  ]
}