diff --git a/SPEC_DAFNY.md b/SPEC_DAFNY.md
index fad4669..c280e7d 100644
--- a/SPEC_DAFNY.md
+++ b/SPEC_DAFNY.md
@@ -68,6 +68,8 @@ Non-pure functions become Dafny `method` declarations.
 
 On merge conflict, the original `foo.dfy` is restored and the merged result is saved as `foo.dfy.merged` for manual inspection. Conflicts and additions-only failures retain the old anchor. A verifier failure after a clean additions-only merge instead retains the new anchor, because the proof already contains that generation; the next retry must not merge it a second time.
 
+Merges use `--diff-algorithm=minimal`, matching the additions-only check so large proof additions do not cause spurious generated-line deletions in the diff. Git versions before 2.44 fall back to the default algorithm with a warning; upgrading avoids the resulting false conflicts. Git execution errors restore the proof and retain the old anchor, but do not create `.dfy.merged` or record a verification conflict.
+
 ---
 
 ## 4. Helper Preambles
diff --git a/tools/fixtures/regen-large-proof/LICENSE b/tools/fixtures/regen-large-proof/LICENSE
new file mode 100644
index 0000000..8038a1c
--- /dev/null
+++ b/tools/fixtures/regen-large-proof/LICENSE
@@ -0,0 +1,21 @@
+The MIT License (MIT)
+
+Copyright (c) 2015 David Khourshid
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.
diff --git a/tools/fixtures/regen-large-proof/README.md b/tools/fixtures/regen-large-proof/README.md
new file mode 100644
index 0000000..1fad6ae
--- /dev/null
+++ b/tools/fixtures/regen-large-proof/README.md
@@ -0,0 +1,14 @@
+# Large proof merge fixture
+
+Reduced from `packages/core/test/machine-model/formal/machineModel.dfy` and
+`.dfy.gen` in [robertpenner/xstate at e9042e7](https://github.com/robertpenner/xstate/tree/e9042e7/packages/core/test/machine-model/formal),
+using the proof-block layout described in [LemmaScript #280](https://github.com/midspiral/LemmaScript/issues/280).
+The upstream MIT license is included in `LICENSE`.
+
+`base.txt` has 32 generated lines; `proof.txt` preserves them with 513 inserted
+lines. Changing `below(candidate.node.path, kept.node.path)` to
+`below(kept.node.path, candidate.node.path)` conflicts with Git's default merge
+diff, but merges exactly with `--diff-algorithm=minimal` (Git 2.54.0).
+These are line-based merge inputs, not valid Dafny programs. Keep their blank
+lines, indentation, and LF line endings: repeated braces and the distance
+between matches are what exercise the diff heuristic.
diff --git a/tools/fixtures/regen-large-proof/base.txt b/tools/fixtures/regen-large-proof/base.txt
new file mode 100644
index 0000000..ca86f45
--- /dev/null
+++ b/tools/fixtures/regen-large-proof/base.txt
@@ -0,0 +1,32 @@
+  decreases |path|
+  var nodes := machine.nodes;
+  var selections := parallelSelections(machine, snapshot, event);
+    var selected := selections[0];
+    var result := selected.evaluation.result;
+          var updated := apply(snapshot.context, selected.evaluation);
+          var entered := runLifecycle(nodes, (if reenter then [selected.id] else []), updated.context, event, false);
+          ParallelStep(ParallelSnapshot(snapshot.active, entered.context), false, (updated.reused && entered.reused), (updated.effects + entered.effects))
+        else
+          var plan := parallelPlan(machine, snapshot.active, selected.id, i_target_val, reenter);
+          var exited := runLifecycle(nodes, plan.exits, snapshot.context, event, true);
+          var updated := apply(exited.context, selected.evaluation);
+          var entered := runLifecycle(nodes, plan.entries, updated.context, event, false);
+          ParallelStep(ParallelSnapshot(plan.active, entered.context), false, ((exited.reused && updated.reused) && entered.reused), ((exited.effects + updated.effects) + entered.effects))
+      case None =>
+        var updated := apply(snapshot.context, selected.evaluation);
+        var entered := runLifecycle(nodes, (if reenter then [selected.id] else []), updated.context, event, false);
+        ParallelStep(ParallelSnapshot(snapshot.active, entered.context), false, (updated.reused && entered.reused), (updated.effects + entered.effects))
+    }
+      }
+  }
+}
+  (overlaps(conflictExits(machine, active, candidate), conflictExits(machine, active, kept)) && !(below(candidate.node.path, kept.node.path)))
+  decreases |kept|
+  decreases |pending|
+    var first := pending[0];
+      var exits := conflictExits(machine, active, first);
+
+  decreases |selections|
+{
+    var entries := SeqFilter((id: string) => plansEnter(plans, id), machine.order);
+    var updated := applyAll(exited.context, kept);
diff --git a/tools/fixtures/regen-large-proof/proof.txt b/tools/fixtures/regen-large-proof/proof.txt
new file mode 100644
index 0000000..421f0ff
--- /dev/null
+++ b/tools/fixtures/regen-large-proof/proof.txt
@@ -0,0 +1,545 @@
+
+{
+      }
+    }
+  }
+}
+
+{
+}
+
+  decreases |path|
+{
+  }
+}
+
+{
+}
+
+{
+  }
+}
+
+}
+
+  decreases |path|
+  var nodes := machine.nodes;
+  var selections := parallelSelections(machine, snapshot, event);
+    var selected := selections[0];
+    var result := selected.evaluation.result;
+          var updated := apply(snapshot.context, selected.evaluation);
+          var entered := runLifecycle(nodes, (if reenter then [selected.id] else []), updated.context, event, false);
+          ParallelStep(ParallelSnapshot(snapshot.active, entered.context), false, (updated.reused && entered.reused), (updated.effects + entered.effects))
+        else
+          var plan := parallelPlan(machine, snapshot.active, selected.id, i_target_val, reenter);
+          var exited := runLifecycle(nodes, plan.exits, snapshot.context, event, true);
+          var updated := apply(exited.context, selected.evaluation);
+          var entered := runLifecycle(nodes, plan.entries, updated.context, event, false);
+          ParallelStep(ParallelSnapshot(plan.active, entered.context), false, ((exited.reused && updated.reused) && entered.reused), ((exited.effects + updated.effects) + entered.effects))
+      case None =>
+        var updated := apply(snapshot.context, selected.evaluation);
+        var entered := runLifecycle(nodes, (if reenter then [selected.id] else []), updated.context, event, false);
+        ParallelStep(ParallelSnapshot(snapshot.active, entered.context), false, (updated.reused && entered.reused), (updated.effects + entered.effects))
+    }
+{
+}
+
+{
+}
+
+{
+}
+
+{
+}
+
+{
+}
+
+{
+}
+
+{
+}
+
+{
+    }
+  }
+}
+
+{
+  }
+}
+
+{
+      }
+    }
+  }
+}
+
+  decreases |path|
+{
+  }
+}
+
+  decreases |path|
+{
+  }
+}
+
+  decreases |path|
+{
+  }
+}
+
+  decreases |path|
+{
+  }
+}
+
+{
+  }
+}
+
+{
+  }
+  }
+}
+
+{
+  }
+}
+
+{
+  }
+}
+
+{
+  }
+}
+
+  decreases |path|
+{
+  }
+}
+
+{
+  }
+}
+
+{
+  }
+}
+
+  decreases |path|
+{
+  }
+}
+
+{
+      }
+    }
+  }
+}
+
+{
+    }
+  }
+}
+
+{
+  }
+}
+
+{
+    }
+      }
+    }
+  }
+}
+
+{
+}
+
+{
+  var nodes := machine.nodes;
+}
+
+{
+  var nodes := machine.nodes;
+}
+
+{
+}
+
+{
+}
+
+{
+  var nodes := machine.nodes;
+}
+
+{
+}
+
+{
+}
+
+{
+}
+
+{
+}
+
+{
+}
+
+{
+}
+
+{
+}
+
+{
+}
+
+{
+  var nodes := machine.nodes;
+}
+
+{
+}
+
+{
+  var nodes := machine.nodes;
+    }
+  }
+  }
+  }
+}
+
+{
+  var nodes := machine.nodes;
+  }
+  }
+}
+
+{
+  var nodes := machine.nodes;
+    }
+  }
+}
+
+{
+}
+
+{
+  var nodes := machine.nodes;
+  }
+  }
+}
+
+{
+  var nodes := machine.nodes;
+    }
+  }
+  }
+}
+
+{
+  }
+}
+
+{
+  var nodes := machine.nodes;
+  }
+}
+
+{
+  var nodes := machine.nodes;
+}
+
+{
+    }
+  }
+}
+
+{
+  var nodes := machine.nodes;
+  }
+}
+
+{
+    }
+  }
+}
+
+{
+}
+
+{
+}
+
+{
+  var selections := parallelSelections(machine, snapshot, event);
+    var selected := selections[0];
+    var result := selected.evaluation.result;
+    }
+  }
+}
+
+{
+}
+
+{
+}
+
+{
+}
+
+{
+}
+
+{
+}
+
+{
+}
+
+{
+}
+
+{
+  }
+}
+
+{
+}
+
+{
+}
+
+      }
+  }
+}
+  (overlaps(conflictExits(machine, active, candidate), conflictExits(machine, active, kept)) && !(below(candidate.node.path, kept.node.path)))
+  decreases |kept|
+  decreases |pending|
+    var first := pending[0];
+      var exits := conflictExits(machine, active, first);
+
+  decreases |selections|
+{
+    var entries := SeqFilter((id: string) => plansEnter(plans, id), machine.order);
+    var updated := applyAll(exited.context, kept);
+
+{
+}
+
+  decreases |selections|
+{
+}
+
+{
+  }
+}
+
+  decreases |selections|
+{
+  }
+}
+
+  decreases |kept|
+{
+  }
+}
+
+  decreases |pending|
+{
+    var first := pending[0];
+      var exits := conflictExits(machine, active, first);
+    }
+  }
+}
+
+  decreases |pending|
+{
+    var first := pending[0];
+      var exits := conflictExits(machine, active, first);
+    }
+  }
+}
+
+{
+  }
+}
+
+  decreases |selections|
+{
+}
+
+  decreases |selections|
+{
+    }
+  }
+}
+
+  decreases |selections|
+{
+  }
+}
+
+  decreases |pending|
+{
+    var first := pending[0];
+      var exits := conflictExits(machine, active, first);
+    }
+  }
+}
+
+  decreases |selections|
+{
+      }
+    }
+  }
+}
+
+{
+}
+
+  decreases |selections|
+{
+  }
+}
+
+{
+}
+
+  decreases |pending|
+{
+}
+
+  decreases |pending|
+{
+    var first := pending[0];
+    }
+  }
+}
+
+{
+}
+
+{
+}
+
+{
+}
+
+{
+  }
+  }
+}
+
+{
+  }
+}
+
+{
+}
+
+{
+}
+
+  decreases |selections|
+{
+      }
+    }
+  }
+}
+
+{
+  }
+}
+
+{
+}
+
+{
+      }
+    }
+  }
+}
+
+{
+}
+
+{
+}
+
+{
+    }
+  }
+}
+
+{
+  }
+}
+
+{
+}
+
+{
+}
+
+{
+}
+
+{
+      }
+    }
+  }
+  }
+}
+
+{
+      }
+    }
+  }
+  }
+}
+
+{
+  }
+}
+
+{
+  }
+}
+
+{
+  }
+    }
+  }
+}
+
+{
+  var selections := parallelSelections(machine, snapshot, event);
+}
+
+{
+  }
+}
+
+{
+  var selections := parallelSelections(machine, snapshot, event);
+  }
+}
+
+    var entries := SeqFilter((id: string) => plansEnter(plans, id), machine.order);
+{
+}
+
+    var entries := SeqFilter((id: string) => plansEnter(plans, id), machine.order);
+    var updated := applyAll(exited.context, kept);
+{
+}
diff --git a/tools/src/dafny-commands.ts b/tools/src/dafny-commands.ts
index a56cc6b..445aa01 100644
--- a/tools/src/dafny-commands.ts
+++ b/tools/src/dafny-commands.ts
@@ -196,18 +196,51 @@ export function dafnyRegen(genPath: string, dfyPath: string, basePath: string, t
     if (!existsSync(basePath)) writeFileSync(basePath, anchor);
     const mergedPath = dfyPath + ".merged";
     console.log("Gen changed. Three-way merging...");
+    const merge = (flags: string[]) => execFileSync(
+      "git", ["merge-file", ...flags, "--", dfyPath, basePath, genPath],
+      // A stable locale lets us recognize an unsupported option without
+      // mistaking other usage errors for an older Git version.
+      { encoding: "utf-8", stdio: ["ignore", "pipe", "pipe"], env: { ...process.env, LC_ALL: "C" } },
+    );
     try {
-      execFileSync("git", ["merge-file", dfyPath, basePath, genPath], { stdio: "pipe" });
+      try {
+        // Match the additions-only check: the default diff can misalign
+        // unchanged generated lines after a large inserted proof block.
+        merge(["--diff-algorithm=minimal"]);
+      } catch (e: any) {
+        if (e?.status !== 129 || e?.signal != null || e?.code != null
+          || typeof e?.stderr !== "string"
+          || !/^error: unknown option [`']diff-algorithm(?:=minimal)?'/m.test(e.stderr)) throw e;
+        writeFileSync(dfyPath, savedDfy);
+        console.warn("WARNING: this Git does not support git merge-file --diff-algorithm; retrying with the default algorithm. " +
+          "Upgrade to Git 2.44 or later to avoid false conflicts after large proof additions.");
+        merge([]);
+      }
       console.log(`Merged: ${path.basename(dfyPath)}`);
     } catch (e: any) {
-      if (e.status > 0) {
-        copyFileSync(dfyPath, mergedPath);
+      // Git returns a conflict count capped at 127. Usage errors, fatal
+      // errors and interrupted/failed processes are not merge conflicts.
+      const conflict = Number.isInteger(e?.status) && e.status >= 1 && e.status <= 127
+        && e?.signal == null && e?.code == null;
+      try {
+        if (conflict) copyFileSync(dfyPath, mergedPath);
+      } finally {
         writeFileSync(dfyPath, savedDfy);
+      }
+      if (conflict) {
         console.error(`CONFLICT: ${path.basename(dfyPath)} — merge had conflicts, dfy restored. See ${path.basename(mergedPath)}`);
         log?.finish({ stage: "conflict", exit: 1, dfyPath });
-        process.exit(1);
+      } else {
+        const reason = e?.code === "ENOENT" ? " (git not found on PATH)"
+          : e?.code != null ? ` (${e.code})`
+          : e?.signal != null ? ` (signal ${e.signal})`
+          : typeof e?.status === "number" ? ` (git exited ${e.status})` : "";
+        const detail = typeof e?.stderr === "string" ? e.stderr.trim() : "";
+        console.error(`ERROR: could not run \`git merge-file\` for ${path.basename(dfyPath)}${reason}; dfy restored` +
+          `${detail ? `: ${detail}` : "."}`);
+        log?.discard();
       }
-      throw e;
+      process.exit(1);
     }
   }
 
diff --git a/tools/tests/dafny-regen.test.ts b/tools/tests/dafny-regen.test.ts
index 914b5e3..79fba89 100644
--- a/tools/tests/dafny-regen.test.ts
+++ b/tools/tests/dafny-regen.test.ts
@@ -1,17 +1,20 @@
 import { test } from "node:test";
 import assert from "node:assert/strict";
+import { spawnSync } from "node:child_process";
 import { chmodSync, existsSync, mkdirSync, mkdtempSync, readFileSync, rmSync, writeFileSync } from "node:fs";
 import { tmpdir } from "node:os";
 import { delimiter, join } from "node:path";
-import { dafnyRegen } from "../src/dafny-commands.ts";
+import { dafnyCheckDiff, dafnyRegen } from "../src/dafny-commands.ts";
+import { RunLog, readRecords } from "../src/run-log.ts";
 
 class ExitSignal extends Error {
   constructor(readonly code: number | undefined) { super(`process.exit(${code})`); }
 }
 const generation = (n: number): string => `method M() {\n  var value := ${n};\n}\n`;
 const addition = "\nlemma AddedProof() {}\n";
+type Fixture = { gen: string; proof: string; base: string; dir: string };
 
-function fixture(run: (f: { gen: string; proof: string; base: string; dir: string }) => void): void {
+function fixture(run: (f: Fixture) => void): void {
   const dir = mkdtempSync(join(tmpdir(), "lsc-regen-review-"));
   const bin = join(dir, "bin");
   const originalExit = process.exit;
@@ -38,6 +41,170 @@ function fails(run: () => void): void {
 }
 const posixOnly = { skip: process.platform === "win32" };
 
+// Intercept selected merge calls, forwarding everything else (including the
+// additions-only check) to real Git. Record calls to catch accidental retries.
+function installGit(f: Fixture, script: string): void {
+  const bin = join(f.dir, "bin");
+  const realPath = process.env.PATH!.split(delimiter).filter(p => p !== bin).join(delimiter);
+  const git = join(bin, "git");
+  writeFileSync(git, `#!${process.execPath}
+const { appendFileSync, writeFileSync } = require("node:fs");
+const { spawnSync } = require("node:child_process");
+const args = process.argv.slice(2);
+const proof = ${JSON.stringify(f.proof)};
+appendFileSync(${JSON.stringify(join(f.dir, "git-calls.jsonl"))}, JSON.stringify(args) + "\\n");
+${script}
+const result = spawnSync("git", args, {
+  stdio: "inherit", env: { ...process.env, PATH: ${JSON.stringify(realPath)} },
+});
+if (result.error) throw result.error;
+if (result.signal) process.kill(process.pid, result.signal);
+process.exit(result.status ?? 1);
+`);
+  chmodSync(git, 0o755);
+}
+
+function mergeCalls(f: Fixture): string[][] {
+  return readFileSync(join(f.dir, "git-calls.jsonl"), "utf8").trim().split("\n")
+    .map(line => JSON.parse(line) as string[]).filter(args => args[0] === "merge-file");
+}
+
+function runLog(f: Fixture): RunLog {
+  const sourcePath = join(f.dir, "x.ts");
+  writeFileSync(sourcePath, "");
+  return new RunLog({ logDir: f.dir, cmd: "regen", sourcePath, lscVersion: "test" });
+}
+
+const oldGit = `
+if (args[0] === "merge-file" && args.includes("--diff-algorithm=minimal")) {
+  console.error("error: unknown option 'diff-algorithm=minimal'");
+  process.exit(129);
+}
+`;
+
+test("a generated change after a large proof block preserves every other byte", posixOnly, t => fixture(f => {
+  const help = spawnSync("git", ["merge-file", "-h"], { encoding: "utf8", env: { ...process.env, LC_ALL: "C" } });
+  assert.ifError(help.error);
+  if (!(help.stdout + help.stderr).includes("--diff-algorithm")) {
+    t.skip("the large-proof fix requires Git 2.44 or later; older Git uses the tested fallback");
+    return;
+  }
+  const base = readFileSync(new URL("../fixtures/regen-large-proof/base.txt", import.meta.url), "utf8");
+  const proof = readFileSync(new URL("../fixtures/regen-large-proof/proof.txt", import.meta.url), "utf8");
+  const old = "below(candidate.node.path, kept.node.path)";
+  const next = "below(kept.node.path, candidate.node.path)";
+  assert.equal(base.split(old).length, 2);
+  assert.equal(proof.split(old).length, 2);
+  writeFileSync(f.gen, base);
+  writeFileSync(f.proof, proof);
+  assert.equal(dafnyCheckDiff(f.gen, f.proof), true);
+  dafnyRegen(f.gen, f.proof, f.base, base.replace(old, next), f.dir, undefined, undefined, true);
+  assert.equal(readFileSync(f.proof, "utf8"), proof.replace(old, next));
+  assert.equal(existsSync(f.base), false);
+  assert.equal(existsSync(f.proof + ".merged"), false);
+}));
+
+test("older Git retries once without the option and warns about false conflicts", posixOnly, t => fixture(f => {
+  installGit(f, oldGit);
+  const warnings: string[] = [];
+  t.mock.method(console, "warn", (message: string) => warnings.push(message));
+  dafnyRegen(f.gen, f.proof, f.base, generation(1), f.dir, undefined, undefined, true);
+  assert.equal(readFileSync(f.proof, "utf8"), generation(1) + addition);
+  assert.equal(existsSync(f.base), false);
+  assert.equal(existsSync(f.proof + ".merged"), false);
+  const calls = mergeCalls(f);
+  assert.equal(calls.length, 2);
+  assert.ok(calls[0].includes("--diff-algorithm=minimal"));
+  assert.ok(!calls[1].includes("--diff-algorithm=minimal"));
+  assert.equal(warnings.length, 1);
+  assert.match(warnings[0], /Git 2\.44.*false conflicts/);
+}));
+
+test("a genuine conflict on older Git still saves the merge and restores the proof", posixOnly, t => fixture(f => {
+  installGit(f, oldGit.replace("unknown option '", "unknown option `"));
+  t.mock.method(console, "warn", () => {});
+  const original = generation(99) + addition;
+  writeFileSync(f.proof, original);
+  const log = runLog(f);
+  fails(() => dafnyRegen(f.gen, f.proof, f.base, generation(1), f.dir, undefined, undefined, true, log));
+  assert.equal(readFileSync(f.proof, "utf8"), original);
+  assert.equal(readFileSync(f.base, "utf8"), generation(0));
+  assert.match(readFileSync(f.proof + ".merged", "utf8"), /<<<<<<</);
+  assert.equal(mergeCalls(f).length, 2);
+  assert.deepEqual(readRecords(f.dir).map(r => r.stage), ["conflict"]);
+}));
+
+for (const failure of [
+  { name: "fatal error", status: 128, detail: "fatal: cannot merge" },
+  { name: "unrelated usage error", status: 129, detail: "error: unknown option 'unrelated'" },
+  { name: "missing input", status: 255, detail: "error: Could not stat missing.dfy" },
+  { name: "signal", signal: "SIGTERM", detail: "merge interrupted" },
+  { name: "error after falling back", status: 255, detail: "error: Could not stat missing.dfy", legacy: true },
+]) {
+  test(`Git ${failure.name} restores recovery state without recording a conflict`, posixOnly, t => fixture(f => {
+    installGit(f, (failure.legacy ? oldGit : "") + `
+if (args[0] === "merge-file") {
+  writeFileSync(proof, "partial merge output\\n");
+  console.error(${JSON.stringify(failure.detail)});
+  ${failure.signal ? `process.kill(process.pid, ${JSON.stringify(failure.signal)});` : `process.exit(${failure.status});`}
+}
+`);
+    const errors: string[] = [];
+    const warnings: string[] = [];
+    t.mock.method(console, "error", (message: string) => errors.push(message));
+    t.mock.method(console, "warn", (message: string) => warnings.push(message));
+    // An existing recovery anchor must win over the last generated file.
+    writeFileSync(f.base, generation(0));
+    writeFileSync(f.gen, generation(9));
+    const priorMerge = "previous conflict for manual inspection\n";
+    if (failure.legacy) writeFileSync(f.proof + ".merged", priorMerge);
+    const log = runLog(f);
+    fails(() => dafnyRegen(f.gen, f.proof, f.base, generation(1), f.dir, undefined, undefined, true, log));
+    assert.equal(readFileSync(f.proof, "utf8"), generation(0) + addition);
+    assert.equal(readFileSync(f.base, "utf8"), generation(0));
+    assert.equal(readFileSync(f.gen, "utf8"), generation(1));
+    if (failure.legacy) assert.equal(readFileSync(f.proof + ".merged", "utf8"), priorMerge);
+    else assert.equal(existsSync(f.proof + ".merged"), false);
+    assert.equal(mergeCalls(f).length, failure.legacy ? 2 : 1);
+    assert.equal(warnings.length, failure.legacy ? 1 : 0);
+    assert.equal(errors.length, 1);
+    assert.match(errors[0], /^ERROR: could not run `git merge-file`/);
+    assert.ok(errors[0].includes(failure.detail));
+    assert.ok(errors[0].includes(failure.signal ?? `git exited ${failure.status}`));
+    assert.deepEqual(readRecords(f.dir), []);
+  }));
+}
+
+test("a missing Git executable is an error and leaves the proof and anchor intact", posixOnly, t => fixture(f => {
+  process.env.PATH = join(f.dir, "bin");
+  const errors: string[] = [];
+  t.mock.method(console, "error", (message: string) => errors.push(message));
+  const log = runLog(f);
+  fails(() => dafnyRegen(f.gen, f.proof, f.base, generation(1), f.dir, undefined, undefined, true, log));
+  assert.equal(readFileSync(f.proof, "utf8"), generation(0) + addition);
+  assert.equal(readFileSync(f.base, "utf8"), generation(0));
+  assert.equal(existsSync(f.proof + ".merged"), false);
+  assert.match(errors.join("\n"), /^ERROR:.*git not found on PATH/);
+  assert.deepEqual(readRecords(f.dir), []);
+}));
+
+test("Git's capped conflict count still saves the conflicted result", posixOnly, () => fixture(f => {
+  const conflicted = "<<<<<<< proof\nours\n=======\ntheirs\n>>>>>>> gen\n";
+  installGit(f, `
+if (args[0] === "merge-file") {
+  writeFileSync(proof, ${JSON.stringify(conflicted)});
+  process.exit(127);
+}
+`);
+  const log = runLog(f);
+  fails(() => dafnyRegen(f.gen, f.proof, f.base, generation(1), f.dir, undefined, undefined, true, log));
+  assert.equal(readFileSync(f.proof, "utf8"), generation(0) + addition);
+  assert.equal(readFileSync(f.base, "utf8"), generation(0));
+  assert.equal(readFileSync(f.proof + ".merged", "utf8"), conflicted);
+  assert.equal(mergeCalls(f).length, 1);
+  assert.deepEqual(readRecords(f.dir).map(r => r.stage), ["conflict"]);
+}));
+
 test("failed verification anchors the generation already merged into the proof", posixOnly, () => fixture(f => {
   fails(() => dafnyRegen(f.gen, f.proof, f.base, generation(1), f.dir));
   assert.equal(readFileSync(f.base, "utf8"), generation(1));