diff --git a/Cargo.lock b/Cargo.lock
index 3def0dd2..e9078752 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -659,18 +659,18 @@ checksum = "d6790f58c7ff633d8771f42965289203411a5e5c68388703c06e14f24770b41e"
 
 [[package]]
 name = "ordeal"
-version = "0.16.1"
+version = "0.18.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "67b320966e15c0447e8bb02b86031f0f32b451a4940f1af24e9c0b5b2434e09b"
+checksum = "3d56ca8355f266f889a33ac6f413fc016d647fb2cec38e94ed80f03d9dc56c4b"
 dependencies = [
  "ordeal-lrat",
 ]
 
 [[package]]
 name = "ordeal-lrat"
-version = "0.16.1"
+version = "0.18.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d1dd8471cb03a6290624af9b033e071479a63bbdb7820d23c2a673f16e9984df"
+checksum = "514834f970104c492975d07788f7afcc9cd16f27b4aa9c6122a03d52bbab3328"
 
 [[package]]
 name = "page_size"
diff --git a/crates/synth-verify/Cargo.toml b/crates/synth-verify/Cargo.toml
index 7ad772fd..ae91bb59 100644
--- a/crates/synth-verify/Cargo.toml
+++ b/crates/synth-verify/Cargo.toml
@@ -30,13 +30,19 @@ synth-opt = { path = "../synth-opt", version = "0.57.0" }
 synth-synthesis = { path = "../synth-synthesis", version = "0.57.0", optional = true }
 
 # Default SMT engine: pure-Rust, certificate-checked QF_BV solver (#553).
-# 0.9 adds the `ordeal::trap` module (trap-preservation VCs, VCR-VER-002 / #166);
-# 0.9.1 adds the float→int trunc trap classifier (`trap_trunc`, ordeal#59/TR-020).
-# PINNED at 0.9.1: the 0.12.0 bump (#825) has a bvsrem/bvsdiv solver-performance
-# regression that HANGS div/rem trap-preservation VCs (4-6h CI timeouts, #849).
-# Re-adopt only once the perf regression is fixed upstream AND native i64 rem
-# (#844/#848) re-lands behind a per-query timeout. Do NOT let dependabot bump this.
-ordeal = "=0.16.1"
+# EXACT-PINNED deliberately: for a 0.x solver a MINOR bump is a breaking bump,
+# and this dependency IS the verification engine — a solver regression is a
+# verification outage (0.12 hung div/rem trap VCs for 4-6h, #849; 0.16 landed
+# with no CI run at all, #864). Every bump goes through a dedicated lane:
+# build ALL CI feature sets (incl. `z3-solver`), run the solver-heavy suites
+# against a wall clock, and read the upstream CHANGELOG — never auto-merge.
+# 0.15 adds `check_with_deadline` (#848); 0.16.1 fixes the bvurem hang
+# (ordeal#101); 0.17 seals the term enums (`#[non_exhaustive]`, ordeal#104 —
+# consumers keep loud catch-alls in term.rs/solver.rs; variant additions are
+# CHANGELOG-called-out) and adds opt-in `cadical`/`cert-bundle` features
+# (unused here); 0.18 is benches/BMC corpus + internal solver split, with the
+# core certified solve path unchanged (verified by this repo's #997 lane).
+ordeal = "=0.18.0"
 
 # Z3: optional differential oracle (feature `z3-solver`) — no longer default.
 # Default features only (NO `static-link-z3`/`bundled`): z3-sys links the
diff --git a/crates/synth-verify/src/solver.rs b/crates/synth-verify/src/solver.rs
index d1ee9c4f..26091a61 100644
--- a/crates/synth-verify/src/solver.rs
+++ b/crates/synth-verify/src/solver.rs
@@ -290,6 +290,15 @@ mod z3_backend {
             BvTerm::Ite { cond, then_, else_ } => {
                 bool_to_z3(cond).ite(&bv_to_z3(then_), &bv_to_z3(else_))
             }
+            // ordeal ≥0.17 seals the term enums (`#[non_exhaustive]`,
+            // ordeal#104). A differential oracle must never guess a
+            // translation — an unknown variant means an ordeal bump added an
+            // op nobody taught this backend; refuse loudly (see the term.rs
+            // catch-alls, which fire first on any such term).
+            other => panic!(
+                "synth-verify z3 oracle: unmodeled ordeal BvTerm variant {other:?} — \
+                 extend bv_to_z3 before trusting any differential verdict"
+            ),
         }
     }
 
@@ -308,6 +317,11 @@ mod z3_backend {
             BoolTerm::Not(a) => bool_to_z3(a).not(),
             BoolTerm::And(a, b) => z3::ast::Bool::and(&[&bool_to_z3(a), &bool_to_z3(b)]),
             BoolTerm::Or(a, b) => z3::ast::Bool::or(&[&bool_to_z3(a), &bool_to_z3(b)]),
+            // Sealed enum (ordeal#104) — see the `bv_to_z3` catch-all.
+            other => panic!(
+                "synth-verify z3 oracle: unmodeled ordeal BoolTerm variant {other:?} — \
+                 extend bool_to_z3 before trusting any differential verdict"
+            ),
         }
     }
 
diff --git a/crates/synth-verify/src/term.rs b/crates/synth-verify/src/term.rs
index 08a80531..8e79a13a 100644
--- a/crates/synth-verify/src/term.rs
+++ b/crates/synth-verify/src/term.rs
@@ -82,6 +82,20 @@ fn bv_rank(t: &BvTerm) -> u8 {
         BvTerm::ZeroExt { .. } => 16,
         BvTerm::SignExt { .. } => 17,
         BvTerm::Ite { .. } => 18,
+        // ordeal ≥0.17 seals the term enums (`#[non_exhaustive]`, ordeal#104):
+        // a variant is only ever added together with a proven blasting rule
+        // and a CHANGELOG callout. synth-verify builds no terms outside the
+        // fragment above, so reaching this arm means an ordeal bump added an
+        // op nobody taught this crate. Refuse LOUDLY (ordeal's documented
+        // consumer policy: conservative error, "never a guess") — a guessed
+        // rank would silently corrupt canonicalization. When this fires,
+        // extend ALL sibling matches together: `bool_rank`, `ord_bv`,
+        // `ord_bool`, `canonicalize_bv`, `canonicalize_bool`, `fmt_bv`,
+        // `fmt_bool`, and the z3 oracle translation in `solver.rs`.
+        other => panic!(
+            "synth-verify: unmodeled ordeal BvTerm variant {other:?} — \
+             extend term.rs + solver.rs before trusting any verdict"
+        ),
     }
 }
 
@@ -100,6 +114,11 @@ fn bool_rank(t: &BoolTerm) -> u8 {
         BoolTerm::Not(..) => 10,
         BoolTerm::And(..) => 11,
         BoolTerm::Or(..) => 12,
+        // Sealed enum (ordeal#104) — see the `bv_rank` catch-all.
+        other => panic!(
+            "synth-verify: unmodeled ordeal BoolTerm variant {other:?} — \
+             extend term.rs + solver.rs before trusting any verdict"
+        ),
     }
 }
 
@@ -284,6 +303,14 @@ fn canonicalize_bv(t: &BvTerm) -> BvTerm {
             then_: Box::new(canonicalize_bv(then_)),
             else_: Box::new(canonicalize_bv(else_)),
         },
+        // Sealed enum (ordeal#104) — see the `bv_rank` catch-all. Cloning an
+        // unknown node instead would silently skip canonicalizing its
+        // children: exactly the commuted-`Mul` CDCL cliff this function
+        // exists to prevent (the 0.12-era hang class, #849).
+        other => panic!(
+            "synth-verify: unmodeled ordeal BvTerm variant {other:?} — \
+             extend term.rs + solver.rs before trusting any verdict"
+        ),
     }
 }
 
@@ -340,6 +367,11 @@ fn canonicalize_bool(t: &BoolTerm) -> BoolTerm {
             Box::new(canonicalize_bool(a)),
             Box::new(canonicalize_bool(b)),
         ),
+        // Sealed enum (ordeal#104) — see the `canonicalize_bv` catch-all.
+        other => panic!(
+            "synth-verify: unmodeled ordeal BoolTerm variant {other:?} — \
+             extend term.rs + solver.rs before trusting any verdict"
+        ),
     }
 }
 
@@ -887,6 +919,11 @@ fn fmt_bv(t: &BvTerm, f: &mut fmt::Formatter<'_>) -> fmt::Result {
             fmt_bv(else_, f)?;
             write!(f, ")")
         }
+        // Sealed enum (ordeal#104). Display feeds diagnostics, so it must
+        // not panic mid-report — emit an unmistakable marker instead (any
+        // such term already panics loudly in `bv_rank`/`canonicalize_bv`
+        // before verification consumes it).
+        _ => write!(f, "<unmodeled-ordeal-bv-term>"),
     }
 }
 
@@ -936,6 +973,8 @@ fn fmt_bool(t: &BoolTerm, f: &mut fmt::Formatter<'_>) -> fmt::Result {
             fmt_bool(b, f)?;
             write!(f, ")")
         }
+        // Sealed enum (ordeal#104) — see the `fmt_bv` catch-all.
+        _ => write!(f, "<unmodeled-ordeal-bool-term>"),
     }
 }