diff --git a/HANDOFF-arith.md b/HANDOFF-arith.md
index 9583c1f..78521bf 100644
--- a/HANDOFF-arith.md
+++ b/HANDOFF-arith.md
@@ -59,6 +59,47 @@ IEEE `x / 0.0` is `inf`, which is defined and wanted — `rand-f32` in the prelu
 2. `lib/x86.ml`'s `prim` `Div`/`Rem`/`Cast` arms last, rebased onto the dev-loop tip, kept mechanical — this is item 3
    of `HANDOFF-x86-rt.md`'s "What remains".
 
-## Status
+## What landed
 
-Stub. Nothing below the line has landed yet; this section is updated as it does.
+**`lib/prelude.ml`** — `(defstruct ArithError [op i32  lhs i64  rhs i64])`, immediately after `BoundsError`, with the
+codes and the per-code meaning of `lhs`/`rhs` written on it.
+
+**`runtime/flan_rt.c`** — `flan_arith_error`, built out of the same three pieces `flan_bounds_error` is: fill a
+`flan_arith_cond` on this frame, `flan_signal`, try `flan_break_hook`, and fall through to a sentence and `rt_die()` if
+neither answered. `flan_arith_fail` is the sentence, and there is one per code rather than one shared "overflow",
+because the reader who reaches `(/ min -1)` has probably never had to think about that case.
+
+**`lib/emit.ml`** — `check_div` and `check_cast`, next to `check_at` and `check_slice` and built on the same
+`signal_block`, so an answered failure leaves through the innermost pad and runs the defers. `check_div` is called from
+`prim`'s `Div`/`Rem` arm and `check_cast` from `cast`'s `Float -> Int` arm.
+
+Three things in those two functions are worth knowing:
+
+- **Integer division only.** IEEE `x / 0.0` is an infinity and is a defined answer somebody may want — the prelude's
+  own `rand-f32` divides by a float constant — so guarding a float division would be refusing a result the language
+  already promises.
+- **One branch, not two.** The zero test and the `INT_MIN / -1` test are `or`-ed into a single compare-and-branch, and
+  *which* of them fired is decided by a `select` that is dead on the fall-through path. The guard is also dropped
+  outright when the divisor is a literal that cannot trigger it, which is nearly every division anyone writes.
+- **The cast test is exact and catches NaN.** Both bounds are powers of two and therefore exact in a double, an `f32`
+  source is `fpext`-ed first so there is one set of bounds rather than two, and the comparisons are *ordered*, which is
+  what makes a NaN fail both halves instead of passing both.
+
+**`test/programs/arith.flan`** — the unhandled half, one case per argument in `bounds.flan`'s shape. Case 0 is the one
+that must not die and is four shapes rather than one: a dynamic divisor, a literal one the guard drops, unsigned
+division, and a float division by zero.
+
+**`test/programs/arith-condition.flan`** — the answered half, in `bounds-condition.flan`'s shape: a `handler-bind`
+clause that reads the condition and takes a frame loop's `continue`. Five codes, four frames finishing, eight
+abandoned, and twelve defers run.
+
+**`test/test_acceptance.ml`** — both programs at `-O0` and `-O2`, the answered one also as a dev build, and the
+`--checks`-off case asserted on the IR rather than by running an unchecked program, because an unchecked divide by zero
+has no defined behaviour to assert on — it is the SIGFPE this change exists to replace.
+
+## The tests the brief asked for, and the one substitution
+
+Unhandled-with-a-location, a `handler-bind` that inspects the condition, and `--checks` off are all there. The
+`use-value` restart case is **not**, because no `use-value` restart is established — see above. What stands in its
+place is the same thing that stands in for it in `bounds-condition.flan`: a handler that transfers out through a
+restart the program already had.
diff --git a/lib/emit.ml b/lib/emit.ml
index 9b47bb5..01b8904 100644
--- a/lib/emit.ml
+++ b/lib/emit.ml
@@ -769,6 +769,166 @@ let signal_block f (loc : Loc.t) ~guard ok emit_call =
   term f "unreachable";
   label f good
 
+(* ── Arithmetic with no answer ─────────────────────────────────────────
+
+   Three situations that had no defined behaviour until now, and they share a
+   helper for the same reason the two bounds checks share one: they are one
+   condition, ArithError, and a handler should write one clause and not five.
+
+   The shape is [signal_block]'s and not [fail_block]'s, so an answered
+   failure leaves through the innermost pad and runs the defers on its way
+   out, exactly as an answered bad index does.
+
+   The thing worth knowing about the divide guard is that it is a branch
+   *before* the instruction rather than anything after it. A SIGFPE cannot be
+   caught and resumed, so there is no version of this that tests afterwards;
+   the branch is the price of the operation having a defined behaviour at all,
+   not the price of that behaviour being a condition. Which is also why the
+   overflow test rides along for nearly nothing: the zero test has already
+   put a compare and a branch on the path, and (/ min -1) is two more compares
+   folded into the same one. *)
+
+(* The codes flan_arith_fail switches on, and the ones the prelude's
+   ArithError documents. They are named here rather than written as bare
+   numbers at the call sites, because a bare number at a call site is exactly
+   the kind of agreement that drifts. *)
+let arith_div_zero = 0
+let arith_rem_zero = 1
+let arith_div_overflow = 2
+let arith_rem_overflow = 3
+let arith_cast_range = 4
+
+(* ArithError's fields are i64 and an operand may be narrower, so every
+   operand is widened on the way into the condition — signed or not according
+   to its own type, so that (-1 : i8) reads back as -1 and (255 : u8) reads
+   back as 255. A u64 above 2^63 still reinterprets as negative, which the
+   prelude says out loud and which a fourth field is not worth fixing. *)
+let widen f (k : Types.ikind) v =
+  if Types.bits k = 64 then v
+  else begin
+    let t = fresh f in
+    ins f "%s = %s %s %s to i64" t
+      (if Types.signed k then "sext" else "zext") (ll (Types.Int k)) v;
+    t
+  end
+
+(* The most negative value of a signed kind, as the decimal LLVM wants. *)
+let int_min k = Int64.neg (Int64.shift_left 1L (Types.bits k - 1))
+
+(* A divide or a remainder. [is_rem] only picks which pair of codes is used;
+   the tests are identical, because `srem` overflows on exactly the operands
+   `sdiv` does — the intermediate quotient is the thing that does not fit.
+
+   Both tests are elided when the divisor is a literal that cannot trigger
+   them, which matters more than it looks: (/ x 2) is the common case, and
+   without this every one of them would carry a branch forever. *)
+let check_div f ~guard loc ~is_rem (k : Types.ikind) ~lit a b =
+  if f.md.checks then begin
+    let ty = ll (Types.Int k) in
+    let need_zero = match lit with Some n -> Int64.equal n 0L | None -> true in
+    let need_ovf =
+      Types.signed k
+      && (match lit with Some n -> Int64.equal n (-1L) | None -> true)
+    in
+    if need_zero || need_ovf then begin
+      (* [false] rather than an emitted instruction when a test is elided: an
+         LLVM operand may be a constant, and the [or] and the [select] below
+         then fold to nothing without a special case for either shape. *)
+      let bad_zero =
+        if need_zero then begin
+          let t = fresh f in
+          ins f "%s = icmp eq %s %s, 0" t ty b;
+          t
+        end
+        else "false"
+      in
+      let bad =
+        if need_ovf then begin
+          let lo = fresh f in
+          ins f "%s = icmp eq %s %s, %Ld" lo ty a (int_min k);
+          let neg1 = fresh f in
+          ins f "%s = icmp eq %s %s, -1" neg1 ty b;
+          let ovf = fresh f in
+          ins f "%s = and i1 %s, %s" ovf lo neg1;
+          let t = fresh f in
+          ins f "%s = or i1 %s, %s" t bad_zero ovf;
+          t
+        end
+        else bad_zero
+      in
+      let ok = fresh f in
+      ins f "%s = xor i1 %s, true" ok bad;
+      (* Which of the two it was is decided with a [select] rather than with a
+         second branch, so the hot path keeps the single compare-and-branch the
+         zero test already cost. The select is dead on the fall-through and any
+         optimiser sinks it into the cold block; at -O0 it is one instruction
+         nobody is going to notice next to a division. *)
+      let code = fresh f in
+      ins f "%s = select i1 %s, i32 %d, i32 %d" code bad_zero
+        (if is_rem then arith_rem_zero else arith_div_zero)
+        (if is_rem then arith_rem_overflow else arith_div_overflow);
+      let aw = widen f k a and bw = widen f k b in
+      signal_block f loc ~guard ok (fun id n ->
+        ins f
+          "call void @flan_arith_error(ptr %s, i64 %d, i32 %s, i64 %s, i64 %s, \
+           ptr %s)"
+          id n code aw bw xfer_param)
+    end
+  end
+
+(* A float to integer cast whose value does not fit. The two bounds are exact
+   in a double for every integer kind up to 64 bits — both are powers of two —
+   so the test is exact rather than approximate, and it is written as
+   [lo <= v < hi] with an *open* top because the top bound is 2^(n-1) or 2^n
+   itself, which is the first value that does not fit rather than the last one
+   that does.
+
+   Ordered comparisons, which is what makes NaN fail both of them. That is
+   wanted: a NaN cast to an integer is as undefined as a value out of range
+   and would otherwise walk straight through the guard.
+
+   An f32 source is extended to a double first. The extension is exact and
+   costs an instruction, and it buys writing one set of bounds instead of two
+   and never having to ask whether 2^63 is representable in the narrower
+   type. *)
+let check_cast f ~guard loc (src : Types.fkind) (k : Types.ikind) v =
+  if f.md.checks then begin
+    let v =
+      match src with
+      | Types.F64 -> v
+      | Types.F32 ->
+        let t = fresh f in
+        ins f "%s = fpext float %s to double" t v;
+        t
+    in
+    let n = Types.bits k in
+    let signed = Types.signed k in
+    (* The first value below the range and the first value above it, and then
+       the range the condition reports, which is the last value *in* it. *)
+    let lo_f = if signed then ldexp (-1.0) (n - 1) else 0.0 in
+    let hi_f = if signed then ldexp 1.0 (n - 1) else ldexp 1.0 n in
+    let lo_i = if signed then int_min k else 0L in
+    let hi_i =
+      if signed then Int64.sub (Int64.shift_left 1L (n - 1)) 1L
+      else if n = 64 then -1L
+      else Int64.sub (Int64.shift_left 1L n) 1L
+    in
+    (* LLVM takes a double constant as the hex of its bits, which is the only
+       spelling that cannot lose anything on the way through. *)
+    let dbl x = Printf.sprintf "0x%016Lx" (Int64.bits_of_float x) in
+    let a = fresh f in
+    ins f "%s = fcmp oge double %s, %s" a v (dbl lo_f);
+    let b = fresh f in
+    ins f "%s = fcmp olt double %s, %s" b v (dbl hi_f);
+    let ok = fresh f in
+    ins f "%s = and i1 %s, %s" ok a b;
+    signal_block f loc ~guard ok (fun id nn ->
+      ins f
+        "call void @flan_arith_error(ptr %s, i64 %d, i32 %d, i64 %Ld, i64 %Ld, \
+         ptr %s)"
+        id nn arith_cast_range lo_i hi_i xfer_param)
+  end
+
 (* [at] is strict: the last valid index is len - 1. *)
 let check_at f ~guard loc idx len =
   if f.md.checks then begin
@@ -1718,6 +1878,20 @@ and prim f (e : Tast.expr) (p : Tast.prim) (args : Tast.expr list) =
       | Types.Int k, _ -> if Types.signed k then "srem" else "urem"
       | t, _ -> failwith ("arithmetic on " ^ Types.to_string t)
     in
+    (* A divide or a remainder by zero, and the one division that overflows,
+       signal ArithError. Integers only: IEEE says x / 0.0 is an infinity and
+       that is a defined answer somebody may want — the prelude's own
+       [rand-f32] divides by a float constant — so guarding a float division
+       would be refusing a result the language already promises.
+
+       A literal divisor is handed through so that the guard can be dropped
+       when it cannot fire, which is nearly every division anyone writes. *)
+    (match x.Tast.ty, p with
+     | Types.Int k, (Tast.Div | Tast.Rem) ->
+       let lit = match y.Tast.e with Tast.Int (n, _) -> Some n | _ -> None in
+       check_div f ~guard:(fun () -> guard f) e.Tast.loc
+         ~is_rem:(p = Tast.Rem) k ~lit a b
+     | _ -> ());
     let t = fresh f in
     (* No nsw/nuw: arithmetic wraps (plan.org, Types). *)
     ins f "%s = %s %s %s, %s" t op (ll x.Tast.ty) a b;
@@ -1967,7 +2141,7 @@ and prim f (e : Tast.expr) (p : Tast.prim) (args : Tast.expr list) =
   | Tast.SizeOf t, [] -> Printf.sprintf "%d" (fst (lay f.md t))
   | Tast.AlignOf t, [] -> Printf.sprintf "%d" (snd (lay f.md t))
   | Tast.AddrOf, [ x ] -> addr f x
-  | Tast.Cast target, [ x ] -> cast f x target
+  | Tast.Cast target, [ x ] -> cast f ~guard:(fun () -> guard f) x target
   | _ -> failwith "malformed primitive"
 
 (* A slice argument crosses to C as ptr+len, never as a struct by value. *)
@@ -1999,7 +2173,7 @@ and shim_in_out f name (x : Tast.expr) =
   ins f "call void %s(ptr %s, i64 %s, ptr %s)" name p n tmp;
   load f tmp (Types.Slice (Types.Int Types.U8))
 
-and cast f (x : Tast.expr) target =
+and cast f ~guard (x : Tast.expr) target =
   let v = value f x in
   (* An enum is an i32 at run time and its own type only in the checker, so a
      cast involving one is a cast on that i32. Nothing in the surface language
@@ -2017,6 +2191,7 @@ and cast f (x : Tast.expr) target =
     | t -> t
   in
   let src = concrete x.Tast.ty and target = concrete target in
+  let src_loc = x.Tast.loc in
   if Types.equal src target then v
   else
     let op =
@@ -2026,7 +2201,14 @@ and cast f (x : Tast.expr) target =
         else if Types.bits b = Types.bits a then "bitcast"
         else if Types.signed a then "sext" else "zext"
       | Types.Int a, Types.Float _ -> if Types.signed a then "sitofp" else "uitofp"
-      | Types.Float _, Types.Int b -> if Types.signed b then "fptosi" else "fptoui"
+      (* The one cast that can have no answer. LLVM calls an out-of-range
+         fptosi undefined and will fold it to anything; x86 produces a fixed
+         "integer indefinite". Neither is a result, so the value is tested
+         against the destination's range first and signals ArithError when it
+         misses. See [check_cast], which is also where NaN is dealt with. *)
+      | Types.Float a, Types.Int b ->
+        check_cast f ~guard src_loc a b v;
+        if Types.signed b then "fptosi" else "fptoui"
       | Types.Float a, Types.Float b ->
         if Types.bits_f b > Types.bits_f a then "fpext" else "fptrunc"
       (* Nothing in the surface language writes this: [check.ml] has no cast
@@ -2435,6 +2617,10 @@ declare void @flan_transfer_fail(ptr, i64) noreturn cold
 declare void @flan_bounds_error(ptr, i64, i64, i64, ptr) cold
 declare void @flan_slice_error(ptr, i64, i64, i64, i64, ptr) cold
 declare void @flan_slice_promise_error(ptr, i64, i64, ptr) cold
+; The same shape and the same reason: it signals ArithError and returns when
+; something answered it. The i32 is the op code and the two i64s are the
+; operands, or the destination's range for a cast.
+declare void @flan_arith_error(ptr, i64, i32, i64, i64, ptr) cold
 declare ptr @flan_context_allocator()
 declare ptr @flan_context_temp()
 declare ptr @flan_heap_allocator()
diff --git a/lib/prelude.ml b/lib/prelude.ml
index b2212b6..5dfe459 100644
--- a/lib/prelude.ml
+++ b/lib/prelude.ml
@@ -82,6 +82,64 @@ let source = {flan|
 ;; the default side of the rule.
 (defstruct BoundsError [low i64 high i64 length i64])
 
+;; What an arithmetic operation with no answer signals. Three situations, and
+;; until now none of them had a defined behaviour: a divide or remainder by
+;; zero, which was a raw SIGFPE with no message and no location; the one
+;; division that overflows, (/ most-negative -1), whose true quotient is one
+;; past the top of the type and which `idiv` also makes a SIGFPE; and a float
+;; to integer cast whose value does not fit, where x86 produces a fixed
+;; "integer indefinite" and LLVM calls the whole thing undefined and may fold
+;; it to anything.
+;;
+;; They signal, for the reason spelled out over BoundsError and for one more
+;; that is specific to these: a SIGFPE cannot be caught and resumed, so the
+;; only way to get a message naming the file and the line is to test *before*
+;; the instruction. Once that branch is being paid for, making it a condition
+;; rather than a die costs nothing further, and a program that genuinely does
+;; not care installs a handler once at startup and never thinks about it again.
+;;
+;; Same shape as the two above, and for the same reasons: fixed numeric
+;; fields, no rendered message, nothing that allocates. It is signalled from
+;; the runtime — flan_arith_error in runtime/flan_rt.c — so **these three
+;; fields are a C struct that has to agree with this one field for field**,
+;; the same hand-kept agreement flan_bounds_cond keeps with BoundsError.
+;;
+;; `op` is a small integer and not a keyword, exactly as FileError's `op` is,
+;; because the field is filled in from C and a keyword is not a thing that
+;; exists there. The codes:
+;;
+;;   0  (/ a 0)      1  (% a 0)
+;;   2  (/ min -1)   3  (% min -1)
+;;   4  a float to integer cast whose value does not fit
+;;
+;; `lhs` and `rhs` are the two operands for codes 0 through 3 and the
+;; destination type's representable range for code 4 — the violated condition
+;; written as a range, which is what flan_slice_promise_error already does
+;; with BoundsError's fields. Two meanings over two fields rather than two
+;; condition types, so that a handler writes one clause and not five. The
+;; value that did not fit is not carried, because it is a float and these
+;; fields are not; what the handler needs in order to say something useful is
+;; the range it missed.
+;;
+;; The fields are the low 64 bits of whatever they hold. A u64 operand above
+;; 2^63 therefore reads back negative, which is the same reinterpretation
+;; every i64 field in every condition here makes and is not worth a fourth
+;; field to fix.
+;;
+;; **No restart is established at the failing operation**, which is
+;; BoundsError's decision and not StorageExhausted's. The sketch this started
+;; from asked for `use-value`, and the implementation is what ruled it out: a
+;; restart frame is allocated by the restart-case that offers it, on its own
+;; stack, and a transfer carries that frame's address (runtime/flan_rt.c, the
+;; restart stack). The runtime cannot hold one on a program's behalf, so
+;; `use-value` here would mean an alloca and a restart frame emitted at every
+;; division in every checked build — the identical cost refused for indexing
+;; a few lines above, buying a silently different answer. What answers a
+;; division by zero is the restart the program already established, a frame
+;; loop's `continue`, which is reachable from a handler without anything being
+;; pushed here.
+(defstruct ArithError [op i32  lhs i64  rhs i64])
+
 ;; A breakpoint. (pause) stops the program where it stands and hands it to the
 ;; break loop, with the whole stack under it readable — C-c C-b lists the
 ;; frames, TAB opens one, and taking `continue` resumes at the call.
diff --git a/runtime/flan_rt.c b/runtime/flan_rt.c
index 8406e70..9a3fcf0 100644
--- a/runtime/flan_rt.c
+++ b/runtime/flan_rt.c
@@ -585,6 +585,112 @@ void flan_slice_promise_error(const uint8_t *loc, int64_t loclen, int64_t n,
   flan_slice_promise_fail(loc, loclen, n);
 }
 
+/* ── Arithmetic with no answer is a condition ──────────────────
+ *
+ * Three situations, and until now none of them had a defined behaviour.
+ * A divide or remainder by zero was a raw SIGFPE: the process died with no
+ * message, no location, and nothing to handle. (/ INT64_MIN -1) is the one
+ * division that overflows — its true quotient is one past the top of the
+ * type -- and `idiv` makes that a SIGFPE too, where LLVM calls it undefined.
+ * And a float to integer cast whose value does not fit produces x86's fixed
+ * "integer indefinite" under one backend and whatever the optimiser feels
+ * like under the other.
+ *
+ * They now signal ArithError, and the argument is the one made for
+ * BoundsError above with one addition that is specific to these: a SIGFPE
+ * cannot be caught and resumed, so the only way to get a message naming the
+ * file and the line at all is a test *before* the instruction. The emitted
+ * branch is therefore not the price of making this a condition — it is the
+ * price of it having any defined behaviour at all — and once it is being
+ * paid, signalling rather than dying costs nothing further.
+ *
+ * **No restart is established here**, which is BoundsError's decision rather
+ * than StorageExhausted's, and here it is forced rather than chosen. A
+ * restart frame is allocated by the restart-case that offers it, on its own
+ * stack, and a transfer carries that frame's address — see the restart stack
+ * at the top of this file. Nothing in C can push one on a program's behalf,
+ * so a `use-value` at the failing division would have to be an alloca and a
+ * push/pop emitted at every division in every checked build. That is the same
+ * cost refused for indexing, buying a silently different answer, and division
+ * is the weaker case of the two: an `at` at least has an element to hand
+ * back. What answers this is the restart the program already established.
+ *
+ * The condition is three fields on this frame and must agree field for field
+ * with the prelude's (defstruct ArithError [op i32 lhs i64 rhs i64]) — the
+ * same hand-kept agreement flan_bounds_cond has with BoundsError. `op` is one
+ * of the codes below; `lhs` and `rhs` are the two operands for a division and
+ * the destination type's representable range for a cast, which is the
+ * violated condition written as a range, exactly as flan_slice_promise_error
+ * writes one into BoundsError's fields. */
+
+enum {
+  FLAN_ARITH_DIV_ZERO = 0,
+  FLAN_ARITH_REM_ZERO = 1,
+  FLAN_ARITH_DIV_OVERFLOW = 2,
+  FLAN_ARITH_REM_OVERFLOW = 3,
+  FLAN_ARITH_CAST_RANGE = 4
+};
+
+typedef struct { int32_t op; int64_t lhs, rhs; } flan_arith_cond;
+
+static const uint8_t flan_arith_name[] = "ArithError";
+#define FLAN_ARITH_NAMELEN 10
+
+/* The sentence each code gets when nothing answered. It is separate from the
+ * struct because the condition deliberately carries no rendered message:
+ * formatting is the unhandled path's job, and this is the unhandled path. */
+static void flan_arith_fail(const uint8_t *loc, int64_t loclen, int32_t op,
+                            int64_t lhs, int64_t rhs) {
+  fflush(stdout);
+  switch (op) {
+  case FLAN_ARITH_DIV_ZERO:
+    fprintf(stderr, "%.*s: divide by zero: (/ %lld 0)\n", (int)loclen,
+            (const char *)loc, (long long)lhs);
+    break;
+  case FLAN_ARITH_REM_ZERO:
+    fprintf(stderr, "%.*s: remainder by zero: (%% %lld 0)\n", (int)loclen,
+            (const char *)loc, (long long)lhs);
+    break;
+  /* Worth its own sentence rather than sharing the word "overflow", because
+   * the reader who hits it has probably never had to think about this case:
+   * it is the single pair of operands in the whole type for which a division
+   * overflows, and it overshoots by exactly one. */
+  case FLAN_ARITH_DIV_OVERFLOW:
+  case FLAN_ARITH_REM_OVERFLOW:
+    fprintf(stderr,
+            "%.*s: (%s %lld %lld) overflows: the quotient is one past the "
+            "largest value the type holds, and this is the only pair of "
+            "operands for which that is true\n",
+            (int)loclen, (const char *)loc,
+            op == FLAN_ARITH_DIV_OVERFLOW ? "/" : "%", (long long)lhs,
+            (long long)rhs);
+    break;
+  default:
+    fprintf(stderr,
+            "%.*s: this value does not fit the integer type it is cast to, "
+            "which holds [%lld %lld]\n",
+            (int)loclen, (const char *)loc, (long long)lhs, (long long)rhs);
+    break;
+  }
+  rt_die();
+}
+
+void flan_arith_error(const uint8_t *loc, int64_t loclen, int32_t op,
+                      int64_t lhs, int64_t rhs, void *xfer) {
+  flan_arith_cond c;
+  uint32_t id = flan_name_id(flan_arith_name, FLAN_ARITH_NAMELEN);
+  c.op = op;
+  c.lhs = lhs;
+  c.rhs = rhs;
+  flan_signal(id, &c, xfer);
+  if (*(void **)xfer != NULL) return;
+  if (flan_break_hook != NULL) {
+    flan_break_hook(flan_arith_name, FLAN_ARITH_NAMELEN, &c, xfer);
+    if (*(void **)xfer != NULL) return;
+  }
+  flan_arith_fail(loc, loclen, op, lhs, rhs);
+}
+
 /* ── Allocators, spec-memory.md ────────────────────────────────────────
  *
  * One type-erased procedure plus an opaque data pointer, which is Odin's
diff --git a/test/programs/arith-condition.flan b/test/programs/arith-condition.flan
new file mode 100644
index 0000000..9f501a0
--- /dev/null
+++ b/test/programs/arith-condition.flan
@@ -0,0 +1,199 @@
+;;;; Arithmetic with no answer is a condition, not a SIGFPE.
+;;;;
+;;;; Three situations had no defined behaviour in this language until now, and
+;;;; the two backends disagreed on all three. A divide or remainder by zero was
+;;;; a raw SIGFPE: the process died with no message, no location, and nothing
+;;;; to handle — which is the worst failure in the whole system, because it
+;;;; tells the programmer less than a segfault does. (/ min -1) is the one
+;;;; division whose true quotient is one past the top of the type, and `idiv`
+;;;; makes that a SIGFPE too where LLVM calls it undefined. And a float to
+;;;; integer cast whose value does not fit produces x86's fixed "integer
+;;;; indefinite" under one backend and whatever the optimiser feels like under
+;;;; the other.
+;;;;
+;;;; All three now signal ArithError with `error`, the same way a bad index
+;;;; signals BoundsError. This program is the "something answered" half; the
+;;;; unhandled half is arith.flan, which dies with a sentence naming the file,
+;;;; the line and the operands.
+;;;;
+;;;; The decision worth reading this file for is the same one BoundsError
+;;;; made, and here it was forced rather than chosen. **No restart is
+;;;; established at the failing operation.** A restart frame is allocated by
+;;;; the restart-case that offers it, on its own stack, and a transfer carries
+;;;; that frame's address — so nothing in the runtime can push one on a
+;;;; program's behalf, and a `use-value` at the failing division would mean an
+;;;; alloca and a restart frame emitted at every division in every checked
+;;;; build. That is the cost already refused for indexing, buying a silently
+;;;; different answer, and division is the weaker case of the two: an `at` at
+;;;; least has an element to hand back. What answers a division by zero here is
+;;;; the restart the program already had — a frame loop's `continue`, which is
+;;;; sand.flan's shape and is what a game wants: abandon this frame, keep the
+;;;; window open.
+;;;;
+;;;; Four things are asserted:
+;;;;
+;;;;   1. The frame is abandoned and the program carries on, over every one of
+;;;;      the five codes.
+;;;;   2. Defers run. An answered arithmetic failure leaves through the same
+;;;;      unwind path a `return` uses, so the defers run innermost first; a
+;;;;      SIGFPE ran none, and could not have.
+;;;;   3. The condition carries the numbers: `op` says which of the five, and
+;;;;      `lhs`/`rhs` are the two operands for a division and the destination
+;;;;      type's representable range for a cast.
+;;;;   4. Division that is fine stays fine, including the two shapes the guard
+;;;;      is allowed to elide — a literal divisor that is neither 0 nor -1, and
+;;;;      unsigned division, which has no overflow case at all.
+
+(defvar frames  i64)
+(defvar skipped i64)
+(defvar cleaned i64)
+(defvar op      i32)
+(defvar lhs     i64)
+(defvar rhs     i64)
+
+;;; Globals rather than locals because a handler cannot see the locals of the
+;;; function that established it — check.ml refuses a capture by name and says
+;;; to use a global.
+(defvar zero  i64)
+(defvar neg1  i64 -1)
+(defvar big   i64 9223372036854775807)
+(defvar huge  f64 1e300)
+(defvar small f64 -1e300)
+(defvar uz    u32)
+
+(defn show [name string  n i64] ()
+  (print name) (print " ") (print n) (println ""))
+
+;;; Two frames deep with a defer on the way, so the transfer has something to
+;;; cross and something to run on its way out.
+(defn divide [a i64  b i64] i64
+  (defer (set cleaned (+ cleaned 1)))
+  (/ a b))
+
+(defn remainder [a i64  b i64] i64
+  (defer (set cleaned (+ cleaned 1)))
+  (% a b))
+
+(defn narrow [x f64] i64
+  (defer (set cleaned (+ cleaned 1)))
+  (i64 x))
+
+(defn narrow-8 [x f64] i8
+  (defer (set cleaned (+ cleaned 1)))
+  (i8 x))
+
+;;; The frame loop's shape: one restart-case around the work, offering
+;;; `continue`, which abandons this frame and nothing else.
+(defn div-frame [a i64  b i64] ()
+  (restart-case
+    (do (show "div" (divide a b))
+        (set frames (+ frames 1)))
+    (continue [] (set skipped (+ skipped 1)))))
+
+(defn rem-frame [a i64  b i64] ()
+  (restart-case
+    (do (show "rem" (remainder a b))
+        (set frames (+ frames 1)))
+    (continue [] (set skipped (+ skipped 1)))))
+
+(defn cast-frame [x f64] ()
+  (restart-case
+    (do (show "cast" (narrow x))
+        (set frames (+ frames 1)))
+    (continue [] (set skipped (+ skipped 1)))))
+
+(defn cast8-frame [x f64] ()
+  (restart-case
+    (do (show "cast8" (i64 (narrow-8 x)))
+        (set frames (+ frames 1)))
+    (continue [] (set skipped (+ skipped 1)))))
+
+(defn main [] i32
+  ;; The most negative i64, which no literal in this language can spell: the
+  ;; reader parses the digits and then negates, and the positive half of the
+  ;; pair does not fit.
+  (let [min (- (- (i64 0) big) 1)]
+
+    (handler-bind
+      [(ArithError [c]
+         ;; The numbers rather than a message, for the reason StorageExhausted
+         ;; has none: formatting allocates, and a condition has to be buildable
+         ;; on a frame where allocation may be the thing that failed.
+         (set op  (.op c))
+         (set lhs (.lhs c))
+         (set rhs (.rhs c))
+         ;; Abandon the frame. The transfer crosses `divide` — running its
+         ;; defer — and lands in the clause of the restart-case two frames out.
+         (invoke-restart 'continue))]
+
+      ;; Fine, so the handler never runs and the defer runs on the ordinary
+      ;; return path.
+      (div-frame 10 3)
+
+      ;; Code 0: a divide by zero. `lhs` and `rhs` are the operands as written.
+      (div-frame 10 zero)
+      (show "op" (i64 op))
+      (show "lhs" lhs)
+      (show "rhs" rhs)
+
+      ;; Code 1: the same for a remainder, which is a different instruction and
+      ;; its own arm in both backends.
+      (rem-frame 7 zero)
+      (show "op" (i64 op))
+
+      ;; Code 2: the one division that overflows. Nothing about the divisor is
+      ;; wrong and nothing about the dividend is wrong; it is the pair.
+      (div-frame min neg1)
+      (show "op" (i64 op))
+      (show "lhs" lhs)
+      (show "rhs" rhs)
+
+      ;; Code 3: and its remainder, which overflows on exactly the same pair —
+      ;; the intermediate quotient is the thing that does not fit, and `srem`
+      ;; computes one too.
+      (rem-frame min neg1)
+      (show "op" (i64 op))
+
+      ;; In range, so no signal: the truncation toward zero is the ordinary
+      ;; result and the guard is not in the way of it.
+      (cast-frame 3.9)
+      (cast-frame -3.9)
+
+      ;; Code 4, both ends. `lhs` and `rhs` are the destination's range rather
+      ;; than the value, because the value is a float and these fields are not;
+      ;; what a handler needs in order to say anything useful is the range it
+      ;; missed.
+      (cast-frame huge)
+      (show "op" (i64 op))
+      (show "lhs" lhs)
+      (show "rhs" rhs)
+      (cast-frame small)
+      (show "op" (i64 op))
+
+      ;; A narrower destination reports its own range, which is the whole point
+      ;; of carrying one: 300 is a perfectly ordinary number and is out of
+      ;; range only for this type.
+      (cast8-frame 12.0)
+      (cast8-frame 300.0)
+      (show "lhs" lhs)
+      (show "rhs" rhs)
+
+      ;; NaN fails both halves of the range test, which is deliberate: a NaN
+      ;; cast to an integer is exactly as undefined as a value out of range,
+      ;; and an unordered comparison would have waved it through.
+      (cast-frame (/ (f64 0.0) (f64 0.0)))
+      (show "op" (i64 op))
+
+      ;; And the shapes the guard is allowed to drop, which have to keep
+      ;; working. A literal divisor that is neither 0 nor -1 needs no test at
+      ;; all; unsigned division needs the zero test and has no overflow case,
+      ;; because there is no most-negative value to overflow from.
+      (show "lit" (/ (+ big 0) 2))
+      (show "u" (i64 (/ (u32 100) (+ uz 7))))))
+
+  ;; Four frames finished, eight were abandoned, and all twelve ran their
+  ;; defer — the claim a SIGFPE could not make.
+  (show "frames" frames)
+  (show "skipped" skipped)
+  (show "cleaned" cleaned)
+  0)
diff --git a/test/programs/arith.flan b/test/programs/arith.flan
new file mode 100644
index 0000000..55b19e4
--- /dev/null
+++ b/test/programs/arith.flan
@@ -0,0 +1,60 @@
+;;;; Arithmetic with no answer, unhandled. One program, one case per argument,
+;;;; the same shape bounds.flan has and for the same reason: a death is
+;;;; observable only as an exit status and a sentence on stderr, so each case
+;;;; needs its own run.
+;;;;
+;;;; What is asserted is the *reason* — the location, and which operation
+;;;; against which operands. Before this change none of these cases had a
+;;;; reason to assert on: the first four were a raw SIGFPE, which prints
+;;;; nothing at all, and the last was undefined and would have printed whatever
+;;;; the optimiser decided the answer was.
+;;;;
+;;;; Everything comes through a global rather than a literal, which keeps the
+;;;; operands dynamic. A literal divisor is exactly the case the guard is
+;;;; allowed to elide, and folding these away would leave the test asserting on
+;;;; a program that does not contain the check.
+
+(defvar zero i64)
+(defvar neg1 i64 -1)
+(defvar big  i64 9223372036854775807)
+(defvar ten  i64 10)
+(defvar uz   u32)
+(defvar huge f64 1e300)
+
+(defn main [args [string]] i32
+  (let [n (i32 (bytes->i64 (bytes (at args 1))))
+        ;; The most negative i64. No literal spells it — the reader parses the
+        ;; digits and then negates, and the positive half does not fit — so it
+        ;; is built, which also keeps it out of the constant folder's reach.
+        min (- (- (i64 0) big) 1)]
+    (cond
+      ;; None of these may die. Division that is fine has to stay fine, and
+      ;; these are the four shapes the guard has an opinion about: an ordinary
+      ;; dynamic divisor, a literal one the guard drops entirely, unsigned
+      ;; division, which has no overflow case because it has no most-negative
+      ;; value, and a float division by zero, which is an infinity and is a
+      ;; defined answer this language is not in the business of refusing.
+      (= n 0) (do (print (/ ten (+ zero 3))) (print " ")
+                  (print (/ ten 2)) (print " ")
+                  (print (/ (u32 100) (+ uz 7))) (print " ")
+                  (print (/ (f64 1.0) (f64 0.0)))
+                  (println ""))
+
+      (= n 1) (print (/ ten zero))            ; divide by zero
+      (= n 2) (print (% ten zero))            ; remainder by zero
+      ;; The one division that overflows. Nothing is wrong with either
+      ;; operand on its own; it is the pair, and it is the only pair.
+      (= n 3) (print (/ min neg1))
+      ;; `srem` overflows on exactly the operands `sdiv` does, because the
+      ;; quotient is what does not fit and a remainder computes one too.
+      (= n 4) (print (% min neg1))
+      ;; A float too large for the destination, and the same value against a
+      ;; narrower destination, which reports its own range.
+      (= n 5) (print (i64 huge))
+      (= n 6) (print (i8 (/ huge 1e290)))
+      ;; NaN, which fails the range test at both ends rather than passing it at
+      ;; neither: the comparisons are ordered, deliberately.
+      (= n 7) (print (i64 (/ (f64 0.0) (f64 0.0))))
+
+      :else (println "?"))
+    0))
diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml
index a6a4c31..01fbe25 100644
--- a/test/test_acceptance.ml
+++ b/test/test_acceptance.ml
@@ -1275,6 +1275,120 @@ let () =
     outputs ~dev:true "a bad index is a condition, dev"
       "programs/bounds-condition.flan" bounds_cond_out;
 
+    (* ── Arithmetic with no answer ─────────────────────────────────────
+       The same pair of programs and the same pair of shapes, for the three
+       situations that had no defined behaviour at all until now: a divide or
+       remainder by zero, which was a raw SIGFPE — no message, no location,
+       nothing to handle — the one division that overflows, and a float to
+       integer cast whose value does not fit, which LLVM called undefined and
+       would fold to anything.
+
+       arith.flan is the unhandled half. It is asserted the way bounds.flan is,
+       on the reason rather than on a result: the location, and which operation
+       against which operands. The first case is the one that must *not* die,
+       and it is four shapes rather than one — an ordinary dynamic divisor, a
+       literal one the guard is allowed to drop, unsigned division, which has
+       no overflow case because it has no most-negative value, and a float
+       division by zero, which is an infinity and is a defined answer this
+       language has no business refusing. *)
+    let arith ?opt () =
+      let exe = compile ?opt "programs/arith.flan" in
+      let traps name arg reason =
+        let code, text = run exe (Some arg) in
+        if code <> 134
+           || not (contains text "programs/arith.flan:")
+           || not (contains text reason)
+        then begin
+          incr failures;
+          Printf.printf
+            "FAIL  %s\n        got: %S (exit %d)\n     wanted: %S (exit 134)\n"
+            name text code reason
+        end
+      in
+      let code, text = run exe (Some "0") in
+      if text <> "3 5 14 inf\n" || code <> 0 then begin
+        incr failures;
+        Printf.printf "FAIL  arithmetic that is fine\n        got: %S (exit %d)\n"
+          text code
+      end;
+      traps "divide by zero" "1" "divide by zero: (/ 10 0)";
+      traps "remainder by zero" "2" "remainder by zero: (% 10 0)";
+      (* The only pair of operands in the whole type for which a division
+         overflows, and the reason this cannot be left to the hardware: `idiv`
+         raises SIGFPE here and LLVM calls it undefined, so the two backends
+         disagreed about a case that is one comparison away from being
+         answerable. *)
+      traps "the division that overflows" "3"
+        "(/ -9223372036854775808 -1) overflows";
+      (* `srem` overflows on exactly the operands `sdiv` does: the quotient is
+         what does not fit, and a remainder computes one on the way. *)
+      traps "the remainder that overflows" "4"
+        "(% -9223372036854775808 -1) overflows";
+      (* The range is the destination's, and it is in the message because it is
+         the only thing that explains the failure — the value is a float and
+         the number that matters about it is which end it fell off. *)
+      traps "a float too large for an i64" "5"
+        "which holds [-9223372036854775808 9223372036854775807]";
+      traps "a float too large for an i8" "6" "which holds [-128 127]";
+      (* NaN fails both halves of the range test rather than passing both,
+         which is what the comparisons being *ordered* buys. An unordered pair
+         would have waved it through into an fptosi that is as undefined for a
+         NaN as it is for 1e300. *)
+      traps "NaN cast to an integer" "7"
+        "does not fit the integer type it is cast to";
+      (try Sys.remove exe with Sys_error _ -> ())
+    in
+    arith ();
+    arith ~opt:"-O0" ();
+
+    (* The release build drops the guards. Asserted on the IR and not by
+       running an unchecked program, for the reason the bounds case gives: an
+       unchecked divide by zero has no defined behaviour to assert on — it is
+       the SIGFPE this whole change exists to replace. *)
+    let ap =
+      Reader.read_file "programs/arith.flan" |> Parse.program |> Check.program
+    in
+    if not (contains (Emit.program ap) "call void @flan_arith_error(") then begin
+      incr failures;
+      print_endline "FAIL  checks on: no arithmetic guard emitted"
+    end;
+    if contains (Emit.program ~checks:false ap) "call void @flan_arith_error("
+    then begin
+      incr failures;
+      print_endline "FAIL  --no-bounds-checks: an arithmetic guard survived"
+    end;
+
+    (* And the answered half. Five codes, five routes, one condition type, and
+       the same three claims bounds-condition.flan makes. (1) The frame is
+       abandoned and the program carries on: four frames finish and eight are
+       abandoned. (2) `cleaned` is 12, every defer on every one of those paths
+       — an answered arithmetic failure leaves through the unwind path a
+       `return` uses, where a SIGFPE ran nothing and could not have. (3) The
+       condition carries the numbers: `op` is which of the five, and
+       `lhs`/`rhs` are the operands for a division and the destination's range
+       for a cast, which is two meanings over two fields rather than five
+       condition types and is BoundsError's precedent exactly.
+
+       The last two rows are the elisions, which are here because a dropped
+       guard is indistinguishable from a broken one unless the result is
+       asserted: a literal divisor, and unsigned division, which gets the zero
+       test and no overflow test at all. *)
+    let arith_cond_out =
+      "div 3\nop 0\nlhs 10\nrhs 0\nop 1\n\
+       op 2\nlhs -9223372036854775808\nrhs -1\nop 3\n\
+       cast 3\ncast -3\n\
+       op 4\nlhs -9223372036854775808\nrhs 9223372036854775807\nop 4\n\
+       cast8 12\nlhs -128\nrhs 127\nop 4\n\
+       lit 4611686018427387903\nu 14\n\
+       frames 4\nskipped 8\ncleaned 12\n"
+    in
+    outputs "arithmetic with no answer is a condition"
+      "programs/arith-condition.flan" arith_cond_out;
+    outputs ~opt:"-O0" "arithmetic with no answer is a condition, -O0"
+      "programs/arith-condition.flan" arith_cond_out;
+    outputs ~dev:true "arithmetic with no answer is a condition, dev"
+      "programs/arith-condition.flan" arith_cond_out;
+
     (* And the half that finishes that thought. bounds-condition.flan's last
        line is `10 99 12 13` — an abandoned frame's leftovers — and a restart
        undoes none of it, because a restart is not a transaction