)]}'
{
  "commit": "4f3d4497185c1aa6417323f889588e43329f2efa",
  "tree": "b141d7b5a3b59b42e0438e3af408562231bea5a8",
  "parents": [
    "70acba11f2ef6ea839cb2581136fa4df94b17fad"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Wed Oct 21 00:45:22 2026 +0000"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Wed Oct 21 00:45:22 2026 +0000"
  },
  "message": "fix: count conflict resolutions as steps in the `lia` model search\n\nThis PR makes `liaSteps` also bound the cases enumerated by Cooper and disequality splits in `lia`, so that a long enumeration stops at the threshold instead of producing a proof the kernel rejects.\n\nThe step counter only ticked when a variable was processed. The next case of a split can be refuted as soon as it is asserted, so an enumeration of thousands of cases never reached the check. Conflict resolutions now count as steps; the search is interrupted only below a decision, where `resetDecisionStack` discards the pending conflict together with the cases.\n\nCo-Authored-By: Claude Fable 5.1 \u003cnoreply@anthropic.com\u003e\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "b1ade8924525712b6b5aef1f9d013c86b0a4489b",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Search.lean",
      "new_id": "8f51be7ff5d79f246922a15e60e1325406de193b",
      "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": "d2b406b5e0dda79d47fe0d0d026eaa48cf0476e8",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_lia_steps_cases.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "7cdf826ec13a999b8f9565f5ba73e5204f91cdb0",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_lia_steps_cases.lean.out.expected"
    }
  ]
}