diff --git a/dev/compile_time.exs b/dev/compile_time.exs
new file mode 100644
index 00000000..686e62d4
--- /dev/null
+++ b/dev/compile_time.exs
@@ -0,0 +1,107 @@
+# Compiler time: compare rounds of DEFK_COMPILE_TIME logs from two
+# checkouts. One round is one dump of every kernel, its log one line per
+# module, "<Module> <microseconds> <reductions>" of a compile measured in a
+# fresh process (Defk.__before_compile__):
+#
+#   DEFK_COMPILE_TIME=tmp/base1.log DEFK_DUMP_C=tmp/c_base mix dump_c   # in the base checkout
+#   DEFK_COMPILE_TIME=tmp/new1.log  DEFK_DUMP_C=tmp/c_new  mix dump_c   # in the new one
+#   ... base2, new2, ..., interleaved so drift hits both sides ...
+#   elixir dev/compile_time.exs tmp/base*.log -- tmp/new*.log
+#   elixir dev/compile_time.exs --reductions tmp/base*.log -- tmp/new*.log
+#
+# Microseconds drift with the machine (a laptop's clock on battery moved a
+# whole round by about 25% between runs); reductions, the work the BEAM
+# counts, repeat to about 0.1% and are the figure to compare when the
+# change is the compiler's own work. Only the modules every log has are
+# compared, so kernels added between the two checkouts do not count as a
+# cost, but a kernel edited between them does: check that the examples and
+# test modules are unchanged. A module name compiled twice in one round
+# (two files) is summed. Each side's figure is the median of its rounds,
+# with and without SatEx.Kernels (examples/cdcl_sat.exs, thousands of kept
+# checks: it dominates any prover cost). With no `--`, the logs are one
+# side and only its medians are printed.
+
+{column, args} =
+  case System.argv() do
+    ["--reductions" | rest] -> {2, rest}
+    rest -> {1, rest}
+  end
+
+{base_paths, new_paths} =
+  case Enum.split_while(args, &(&1 != "--")) do
+    {base, ["--" | new]} -> {base, new}
+    {base, []} -> {base, []}
+  end
+
+if base_paths == [] do
+  IO.puts(
+    :stderr,
+    "usage: elixir dev/compile_time.exs [--reductions] <base logs> [-- <new logs>]"
+  )
+
+  System.halt(2)
+end
+
+read = fn path ->
+  for line <- File.read!(path) |> String.split("\n", trim: true),
+      [mod | figures] = String.split(line),
+      n = String.to_integer(Enum.at(figures, column - 1)),
+      reduce: %{},
+      do: (acc -> Map.update(acc, mod, n, &(&1 + n)))
+end
+
+{base, new} = {Enum.map(base_paths, read), Enum.map(new_paths, read)}
+
+common =
+  (base ++ new)
+  |> Enum.map(&MapSet.new(Map.keys(&1)))
+  |> Enum.reduce(&MapSet.intersection/2)
+
+median = fn xs ->
+  sorted = Enum.sort(xs)
+  n = length(sorted)
+  mid = div(n, 2)
+
+  if rem(n, 2) == 1,
+    do: Enum.at(sorted, mid),
+    else: div(Enum.at(sorted, mid - 1) + Enum.at(sorted, mid), 2)
+end
+
+total = fn round, mods -> mods |> Enum.map(&Map.fetch!(round, &1)) |> Enum.sum() end
+without_sat = MapSet.delete(common, "SatEx.Kernels")
+
+side = fn rs ->
+  {median.(Enum.map(rs, &total.(&1, common))), median.(Enum.map(rs, &total.(&1, without_sat)))}
+end
+
+show =
+  if column == 1,
+    do: fn us -> :erlang.float_to_binary(us / 1000, decimals: 1) <> " ms" end,
+    else: fn r -> :erlang.float_to_binary(r / 1.0e6, decimals: 2) <> "M reductions" end
+
+pct = fn a, b -> :erlang.float_to_binary(100 * (b - a) / a, decimals: 1) <> "%" end
+
+IO.puts(
+  "#{MapSet.size(common)} modules in every log; rounds: #{length(base)} base, #{length(new)} new"
+)
+
+{b_all, b_wo} = side.(base)
+IO.puts("base: #{show.(b_all)} (without SatEx.Kernels #{show.(b_wo)})")
+
+if new != [] do
+  {n_all, n_wo} = side.(new)
+  IO.puts("new:  #{show.(n_all)} (without SatEx.Kernels #{show.(n_wo)})")
+  IO.puts("change: #{pct.(b_all, n_all)} (without SatEx.Kernels #{pct.(b_wo, n_wo)})")
+
+  deltas =
+    for m <- common do
+      {m, median.(Enum.map(new, & &1[m])) - median.(Enum.map(base, & &1[m]))}
+    end
+
+  IO.puts("largest changes by module (median):")
+
+  deltas
+  |> Enum.sort_by(&(-abs(elem(&1, 1))))
+  |> Enum.take(5)
+  |> Enum.each(fn {m, d} -> IO.puts("  #{m} #{if d >= 0, do: "+", else: ""}#{show.(d)}") end)
+end
diff --git a/docs/adr/0007-symbolic-bounds.md b/docs/adr/0007-symbolic-bounds.md
index 7f860095..d64b7e45 100644
--- a/docs/adr/0007-symbolic-bounds.md
+++ b/docs/adr/0007-symbolic-bounds.md
@@ -80,7 +80,14 @@ Replace the fact model with one representation:
   (products, `defk-pvt`) +1.7% (+0.9% without `SatEx.Kernels`) after
   cutting a second fact lookup per step and the ranking of one-term forms;
   the chain is at about +14%, under the ceiling, with about 1% left
-  (`docs/performance.md` 6.37).
+  (`docs/performance.md` 6.37). Measured again (2026-10-20) with a warm
+  compile in a fresh process (6.38; the method before included waiting
+  and heap noise): the chain cost +13.4% of the time but +20.8% of the
+  work (reductions), and the refactors after it another +13.5% / +7.3%.
+  The compiler is at about +29% of its time before step 1, past the
+  ceiling; the next step cuts first. The copy analysis's one pass per arm
+  (`defk-o08.3`, 6.39) took 9% off: +17.6% of the work before step 1, still
+  past the ceiling.
 - **Raising guards become the way to state facts about arguments** in a
   kernel, which the language docs would describe.
 - **Out of scope:** degree 3 and nested products, facts across loop
diff --git a/docs/agents/runs.md b/docs/agents/runs.md
index 968d2f11..d964836b 100644
--- a/docs/agents/runs.md
+++ b/docs/agents/runs.md
@@ -61,9 +61,23 @@ cores it uses.
 
 ## Compiler time
 
-The compiler-time rounds (a temporary `:timer.tc` around
-`Defk.Compiler.compile` in `Defk.__before_compile__`, interleaved `mix
-dump_c` rounds on both sides) measure defk's compile, not `cc`, so they run
-without `cc` too. Name the files when the change touches only some kernels,
-and report `SatEx.Kernels` (`examples/cdcl_sat.exs`) on its own: it
-dominates the prover's cost.
+The compiler-time rounds measure defk's compile, not `cc`, so they run
+without `cc` too. With `DEFK_COMPILE_TIME=<file>` set, every module compiles
+once more in a fresh process and logs that compile's microseconds and
+reductions (`Defk.__before_compile__`, `timed_compile/2`). Run interleaved
+rounds on both sides and compare them:
+
+    DEFK_COMPILE_TIME=tmp/base1.log DEFK_DUMP_C=tmp/c_base mix dump_c   # base checkout
+    DEFK_COMPILE_TIME=tmp/new1.log  DEFK_DUMP_C=tmp/c_new  mix dump_c   # branch
+    ... base2, new2 ...
+    elixir dev/compile_time.exs --reductions tmp/base*.log -- tmp/new*.log
+    elixir dev/compile_time.exs tmp/base*.log -- tmp/new*.log
+
+Two rounds a side are enough for reductions, which repeat to about 0.1%;
+microseconds drift with the machine (about 25% between runs on a laptop
+on battery), so report them with the conditions. A full round takes about
+a minute and a half. Name the files when the change touches only some
+kernels, and report `SatEx.Kernels` (`examples/cdcl_sat.exs`) on its own:
+it dominates the prover's cost. Do not time a module's first compile: under
+`mix compile` it waits for the compiler's own modules (`docs/performance.md`
+6.38).
diff --git a/docs/performance.md b/docs/performance.md
index 6447d776..f9e449d1 100644
--- a/docs/performance.md
+++ b/docs/performance.md
@@ -2514,6 +2514,69 @@ else: 0))`; it now says `if first < 0 and n > 0, do: raise(ArgumentError,
   the whole suite under AddressSanitizer.
 - **Status:** measured, provisional.
 
+### 6.38 Compiler time: measure a second compile in a fresh process; the chain and the refactors cost ~29% together
+
+- **The method before** (6.32-6.37) timed `Defk.Compiler.compile` once per
+  module under `mix dump_c`. That run is `compile --force`, so `lib` and
+  `test/support` compile in parallel, and the first kernel module
+  (`Examples.Kernels`) waited about 1 s for the compiler's own modules: of
+  a 2.5 s round, about 1.0 s was that wait (the module needs 13 ms warm).
+  A second compile in the same process was no better: `SatEx.Kernels`
+  then took either ~240 or ~510 ms on the same code (what the first
+  compile left on the heap), and a whole round moved by ~25% between two
+  runs on the laptop.
+- **The method now:** `DEFK_COMPILE_TIME=<file>` makes every module compile
+  once for its result and once more in a fresh process, which is measured:
+  microseconds and the process's reductions. `dev/compile_time.exs`
+  compares interleaved rounds of two checkouts on the modules both have.
+  Five compiles of `SatEx.Kernels`: 355-369 ms, 50.64-50.68 M reductions
+  (±2% and ±0.05%). Reductions are the figure to compare for a change to
+  the compiler's own work; time is the one a user feels.
+- **Numbers** (99 modules both checkouts have, two rounds each,
+  interleaved, medians): before step 1 (`23e27970`) 105.8 M reductions /
+  801 ms; after step 4 (`a371dcab`) 127.8 M / 909 ms; main (`b90ed0ff`)
+  137.1 M / 1,032 ms. The symbolic-bounds chain: +20.8% reductions, +13.4%
+  time (without `SatEx.Kernels` +6.8%, +3.9%). The readability refactors
+  after it (`x3a`, `rt2`): +7.3% reductions, +13.5% time (+6.7%, +3.3%).
+  Together +29.5% reductions, +28.8% time (+14.0%, +7.3%). `SatEx.Kernels`
+  alone went from ~150 to ~340 ms.
+- **What it means:** the chain's own +14% (6.37) holds for time but not for
+  work, and the compiler is about twice as far past its state before step
+  1 as the +15% ceiling of ADR-0007 allows, half of it from refactors no
+  budget covered. Where the time is (one warm round, 2026-10-20): the copy
+  analysis's per-statement walks ~16% (`Copies.nested/3` 9.7%), the
+  prover ~3.5%, the report's hint search 2.4%, the strip classifier 2.4%;
+  the rest is spread over the lowering.
+- **Conditions:** M-series Mac on battery, no quiet check; `cc` not run
+  (`DEFK_NO_CC=1`; the baseline with the `DEFK_NO_CC` change applied, a
+  tooling change). A few examples and test kernels changed between the
+  checkouts (`hash_chain.exs` gained a raising guard), so the 99 modules are
+  not all identical; `SatEx.Kernels` (`cdcl_sat.exs`) is.
+- **Source:** `defk-o08.2`; `dev/compile_time.exs`; the harness in
+  `Defk.__before_compile__` (`timed_compile/2`).
+- **Status:** measured, provisional.
+
+### 6.39 The copy analysis asked each arm's reads in one pass: -9% of the compiler's work
+
+- **Numbers:** `Copies.nested/3` asked, for every block nested in a
+  statement, `arm?/2`, `taken/2` and `reads_outside/2`: five walks of the
+  whole statement, one of them quadratic (`taken/2` called `holds_arm?/2`,
+  a walk of the arms, on every node). `arm_reads/2` does it in three
+  linear walks, rebuilding only the path to the arm. Over the 108 modules
+  of `mix dump_c`, two rounds each, interleaved with main plus the harness:
+  138.6 -> 125.8 M reductions (-9.2%; without `SatEx.Kernels` -5.0%),
+  1,101 -> 996 ms (-9.6%; -2.9%); `SatEx.Kernels` -8.4 M reductions,
+  -86 ms. Against the compiler before step 1 (6.38's baseline, by
+  reductions, which repeat between runs): +17.6% (+8.4% without
+  `SatEx.Kernels`), from +29.5%.
+- **Same C:** `mix dump_c` byte-identical for all 108 modules. The old
+  functions stay as the spec: a property test compares `arm_reads/2` with
+  them on every subterm of generated statements (if, cond, case, matches,
+  blocks, few names so that a node appears twice).
+- **Conditions:** M-series Mac on battery, no quiet check; `cc` not run.
+- **Source:** `defk-o08.3`; `test/copies_test.exs`.
+- **Status:** measured, provisional.
+
 ---
 
 ## 7. When a hand-written or wrapper NIF is still the answer
@@ -2820,4 +2883,5 @@ example or close a workload ticket, add its entries and its line here.
   `defk-l2g`, `defk-yzw`, `defk-dtw.2`, `defk-dtw.20`, `defk-dtw.21`,
   `defk-sve`, `defk-sve.1` ([`state-copy-cost.md`](https://github.com/DanielLuning/defk/blob/main/docs/research/state-copy-cost.md)), `defk-ulk`, `defk-ulk.1` ([`simd.md`](https://github.com/DanielLuning/defk/blob/main/docs/research/simd.md)), `defk-33b`,
   `defk-ulk.4`, `defk-52v.15` ([`cdcl_sat.exs`](https://github.com/DanielLuning/defk/blob/main/examples/cdcl_sat.exs)), `defk-tif`, `defk-gqk`, `defk-6ag`,
-  `defk-7dm` ([`bench/port_roundtrip.exs`](https://github.com/DanielLuning/defk/blob/main/bench/port_roundtrip.exs)), `defk-1ub`.
+  `defk-7dm` ([`bench/port_roundtrip.exs`](https://github.com/DanielLuning/defk/blob/main/bench/port_roundtrip.exs)), `defk-1ub`,
+  `defk-o08.2`, `defk-o08.3`.
diff --git a/lib/defk.ex b/lib/defk.ex
index ca69d1ec..e32f349d 100644
--- a/lib/defk.ex
+++ b/lib/defk.ex
@@ -439,12 +439,14 @@ defmodule Defk do
     adaptive? = Module.get_attribute(env.module, :defk_adaptive_slice)
 
     {c_src, all_sigs, report} =
-      Defk.Compiler.compile(env.module, kernels, env.file,
-        nif_name: nif_name,
-        fault_hooks: fault_hooks?,
-        adaptive_slice: adaptive?,
-        max_owned_bytes: max_owned_bytes!(env.module)
-      )
+      timed_compile(env.module, fn ->
+        Defk.Compiler.compile(env.module, kernels, env.file,
+          nif_name: nif_name,
+          fault_hooks: fault_hooks?,
+          adaptive_slice: adaptive?,
+          max_owned_bytes: max_owned_bytes!(env.module)
+        )
+      end)
 
     # a yielding kernel's NIF takes the run-queue hint: it is
     # renamed, and the kernel's function passes the hint
@@ -520,6 +522,48 @@ defmodule Defk do
     File.write!(Path.join(dir, "#{inspect(module)}.c"), c_src)
   end
 
+  # DEFK_COMPILE_TIME=<file>: every module compiled while it is set appends
+  # "<Module> <microseconds> <reductions>" to <file>, of a second compile
+  # run in a fresh process (dev/compile_time.exs). The first compile, whose
+  # result the module uses, is not measured: under `mix compile` it may wait
+  # for the compiler's own modules, compiled in parallel with the kernels,
+  # and that wait is not compiler work. A fresh process starts with a small
+  # heap, so the time does not depend on what the first compile left. Like
+  # DEFK_DUMP_C, a side channel: the module is unchanged.
+  defp timed_compile(module, compile) do
+    case System.get_env("DEFK_COMPILE_TIME") do
+      nil ->
+        compile.()
+
+      log ->
+        result = compile.()
+        {us, reductions} = measured(compile)
+        File.write!(log, "#{inspect(module)} #{us} #{reductions}\n", [:append])
+        result
+    end
+  end
+
+  defp measured(compile) do
+    parent = self()
+
+    {pid, mref} =
+      spawn_monitor(fn ->
+        {:reductions, r0} = Process.info(self(), :reductions)
+        {us, _} = :timer.tc(compile)
+        {:reductions, r1} = Process.info(self(), :reductions)
+        send(parent, {self(), us, r1 - r0})
+      end)
+
+    receive do
+      {^pid, us, reductions} ->
+        Process.demonitor(mref, [:flush])
+        {us, reductions}
+
+      {:DOWN, ^mref, :process, ^pid, reason} ->
+        raise "DEFK_COMPILE_TIME: the measured compile failed: #{inspect(reason)}"
+    end
+  end
+
   # `use Defk, max_owned_bytes: n`: a positive integer of bytes that fits in
   # a uint64 (DEFK_MAX_OWNED), or nil (the runtime's default)
   defp max_owned_bytes!(module) do
diff --git a/lib/defk/copies.ex b/lib/defk/copies.ex
index 8339489d..8f157f06 100644
--- a/lib/defk/copies.ex
+++ b/lib/defk/copies.ex
@@ -303,13 +303,133 @@ defmodule Defk.Copies do
   # body, run again) keeps what is live for nested blocks.
   def nested(%Scope{} = s, ast, vars) do
     out =
-      if arm?(s.stmt, ast),
-        do: MapSet.union(s.live, pairs(vars, reads_outside(taken(s.stmt, ast), ast))),
-        else: s.nest
+      case arm_reads(s.stmt, ast) do
+        nil -> s.nest
+        names -> MapSet.union(s.live, pairs(vars, names))
+      end
 
     %{s | out: out, depth: s.depth + 1}
   end
 
+  # What nested/3 asks of statement `stmt`, in three linear walks: nil when
+  # `node` is not an arm of it (arm?/2), else the names
+  # reads_outside(taken(stmt, node), node) gives, the spec (copies_test
+  # compares the two). taken/2 changes only the if, cond and case nodes on
+  # the path to `node`, so cut/2 rebuilds that path with `node` cut out and
+  # the rest shared, and what is read is what is left.
+  def arm_reads(nil, _node), do: nil
+
+  def arm_reads(stmt, node) do
+    {_, found} =
+      Macro.prewalk(stmt, {0, false}, fn x, {n, arm} ->
+        {x, {if(x == node, do: n + 1, else: n), arm or node in arms(x)}}
+      end)
+
+    if found == {1, true}, do: stmt |> cut(node) |> elem(0) |> reads()
+  end
+
+  # {`x` with `node` (in it once) replaced by nil and each if, cond and case
+  # holding it in an arm cut as other_arms_out/2 cuts it, whether `node` was
+  # in `x`}; it walks what Macro.prewalk/3 walks
+  defp cut(x, node) do
+    if x == node, do: {nil, true}, else: cut_in(x, node)
+  end
+
+  # each part is walked once: an if, cond or case not holding `node` in an
+  # arm is rebuilt from the parts already cut
+  defp cut_in({:if, m, [c, kw]} = x, node) when is_list(kw) do
+    {c2, in_c} = cut(c, node)
+    parts = Enum.map(kw, &{&1, cut(&1, node)})
+
+    cond do
+      Enum.any?(parts, fn {e, {_, f}} -> f and match?({k, _} when k in [:do, :else], e) end) ->
+        arms = for {{k, _}, {{_, b}, f}} <- parts, do: {k, if(f, do: b)}
+        {{:if, m, [nil, arms]}, true}
+
+      in_c or Enum.any?(parts, fn {_, {_, f}} -> f end) ->
+        {{:if, m, [c2, Enum.map(parts, fn {_, {e, _}} -> e end)]}, true}
+
+      true ->
+        {x, false}
+    end
+  end
+
+  defp cut_in({:cond, m, [[do: clauses]]} = x, node) when is_list(clauses) do
+    case cut_clauses(clauses, node) do
+      {:arm, out} -> {{:cond, m, [[do: out]]}, true}
+      {:in, clauses2} -> {{:cond, m, [[do: clauses2]]}, true}
+      :no -> {x, false}
+    end
+  end
+
+  defp cut_in({:case, m, [subject, [do: clauses]]} = x, node) when is_list(clauses) do
+    {subject2, in_s} = cut(subject, node)
+
+    case cut_clauses(clauses, node) do
+      {:arm, out} -> {{:case, m, [nil, [do: out]]}, true}
+      {:in, clauses2} -> {{:case, m, [subject2, [do: clauses2]]}, true}
+      :no when in_s -> {{:case, m, [subject2, [do: clauses]]}, true}
+      :no -> {x, false}
+    end
+  end
+
+  defp cut_in(x, node), do: cut_args(x, node)
+
+  # {:arm, the clauses as clauses_out/2 gives them} when `node` is in a
+  # clause body, {:in, the clauses cut} when it is elsewhere in them, :no
+  defp cut_clauses(clauses, node) do
+    parts =
+      Enum.map(clauses, fn
+        {:->, cm, [head, body]} -> {:clause, cm, cut(head, node), cut(body, node)}
+        e -> {:other, cut(e, node)}
+      end)
+
+    cond do
+      Enum.any?(parts, &match?({:clause, _, _, {_, true}}, &1)) ->
+        {:arm, for({:clause, cm, _, {b, f}} <- parts, do: {:->, cm, [[nil], if(f, do: b)]})}
+
+      Enum.any?(
+        parts,
+        &(match?({:clause, _, {_, true}, _}, &1) or match?({:other, {_, true}}, &1))
+      ) ->
+        {:in,
+         Enum.map(parts, fn
+           {:clause, cm, {h, _}, {b, _}} -> {:->, cm, [h, b]}
+           {:other, {e, _}} -> e
+         end)}
+
+      true ->
+        :no
+    end
+  end
+
+  # Macro.prewalk/3's descent: a call's form (unless an atom) and its
+  # arguments, both halves of a pair, every element of a list
+  defp cut_args({form, m, args} = x, node) do
+    {form2, f1} = if is_atom(form), do: {form, false}, else: cut(form, node)
+    {args2, f2} = if is_list(args), do: cut_list(args, node), else: {args, false}
+    if f1 or f2, do: {{form2, m, args2}, true}, else: {x, false}
+  end
+
+  defp cut_args({a, b} = x, node) do
+    {a2, f1} = cut(a, node)
+    {b2, f2} = cut(b, node)
+    if f1 or f2, do: {{a2, b2}, true}, else: {x, false}
+  end
+
+  defp cut_args(l, node) when is_list(l), do: cut_list(l, node)
+  defp cut_args(x, _node), do: {x, false}
+
+  defp cut_list(l, node) do
+    {l2, found} =
+      Enum.map_reduce(l, false, fn e, f ->
+        {e2, f2} = cut(e, node)
+        {e2, f or f2}
+      end)
+
+    if found, do: {l2, true}, else: {l, false}
+  end
+
   # Leaving a nested plain block, which binds into the scope around it as in
   # Elixir: `vars` the bindings at the block's end, now bound in the outer
   # block and so at its depth.
diff --git a/test/copies_test.exs b/test/copies_test.exs
index 6b9b52be..1a32eb51 100644
--- a/test/copies_test.exs
+++ b/test/copies_test.exs
@@ -6,6 +6,7 @@
 # runtime contract holds.
 defmodule Defk.CopiesTest do
   use ExUnit.Case, async: true
+  use ExUnitProperties
 
   alias Defk.Copies
 
@@ -348,4 +349,62 @@ defmodule Defk.CopiesTest do
       refute {vars.a.id, vars.a.buf} in Copies.live(callee)
     end
   end
+
+  describe "arm_reads/2, nested/3's one pass" do
+    # the spec: arm?/2, then reads_outside(taken(stmt, node), node)
+    defp spec(stmt, node),
+      do: if(Copies.arm?(stmt, node), do: Copies.reads_outside(Copies.taken(stmt, node), node))
+
+    # statements of variables, calls, matches, blocks and nested if, cond
+    # and case; few names, so equal subterms (a node twice) are common
+    defp stmt_gen do
+      leaf = StreamData.member_of([:a, :b, :c, :d] |> Enum.map(&{&1, [], nil}))
+
+      StreamData.tree(leaf, fn inner ->
+        StreamData.one_of([
+          StreamData.map(StreamData.list_of(inner, max_length: 2), &{:f, [], &1}),
+          StreamData.map({leaf, inner}, fn {v, e} -> {:=, [], [v, e]} end),
+          StreamData.map(
+            StreamData.list_of(inner, min_length: 1, max_length: 3),
+            &{:__block__, [], &1}
+          ),
+          StreamData.map({inner, inner, inner}, fn {c, t, e} ->
+            {:if, [], [c, [do: t, else: e]]}
+          end),
+          StreamData.map({inner, inner}, fn {c, t} -> {:if, [], [c, [do: t]]} end),
+          StreamData.map({inner, inner, inner}, fn {c, t, e} ->
+            {:cond, [], [[do: [{:->, [], [[c], t]}, {:->, [], [[true], e]}]]]}
+          end),
+          StreamData.map({inner, leaf, inner, inner}, fn {s, p, t, e} ->
+            {:case, [], [s, [do: [{:->, [], [[p], t]}, {:->, [], [[{:_, [], nil}], e]}]]]}
+          end)
+        ])
+      end)
+    end
+
+    defp subterms(ast) do
+      {_, acc} = Macro.prewalk(ast, [], &{&1, [&1 | &2]})
+      acc
+    end
+
+    property "gives what the spec gives, for every subterm of a statement" do
+      check all(stmt <- stmt_gen(), max_runs: 300) do
+        for node <- subterms(stmt) do
+          assert Copies.arm_reads(stmt, node) == spec(stmt, node),
+                 "stmt #{Macro.to_string(stmt)}, node #{inspect(node)}"
+        end
+      end
+    end
+
+    test "an arm read beside a branch in an expression, and an arm twice" do
+      node = quote do: helper(a)
+      stmt = quote do: f(if(keep, do: unquote(node), else: g(b)), peek(c))
+      # keep chose the arm, g(b) runs instead of it: only c is read beside it
+      assert Copies.arm_reads(stmt, node) == MapSet.new([:c])
+      assert Copies.arm_reads(stmt, node) == spec(stmt, node)
+
+      twice = quote do: if(keep, do: unquote(node), else: unquote(node))
+      assert Copies.arm_reads(twice, node) == nil
+    end
+  end
 end