)]}'
{
  "commit": "388a64a9c6711be8abf892e7396cd48fdeb65ac8",
  "tree": "bea093b61d5c59783cd0c551981170a17fa3e2e1",
  "parents": [
    "05a10f7c34dc782ce2925fc0bf4aac751e19a180"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Wed Aug 12 20:35:31 2026 +0000"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Wed Aug 12 20:35:31 2026 +0000"
  },
  "message": "test: increase split budget in `grind_bitvec2` bench\n\nThe `replicate_append_self` goal needs the exponent identity `w + w * n \u003d w * (n + 1)` to relate `2 ^ _` terms in the `toNat` images of the appends. `grind` finds it only via a model-based theory combination case split, and the homomorphism encoding eagerly translates every `BitVec` term (including `cast` variants), producing enough competing exponent-pair split candidates that the default budget of 9 is no longer sufficient; the goal needs 11.\n\nCo-Authored-By: Claude Fable 5 \u003cnoreply@anthropic.com\u003e\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "5e572e8556ee61fc0dcd04075eb8b2ba9ba91b26",
      "old_mode": 33188,
      "old_path": "tests/elab_bench/grind_bitvec2.lean",
      "new_id": "dcd61ea5852b448f463cb55e6303796164908eef",
      "new_mode": 33188,
      "new_path": "tests/elab_bench/grind_bitvec2.lean"
    }
  ]
}