diff --git a/include/cobra/core/DecompositionEngine.h b/include/cobra/core/DecompositionEngine.h
index 20dd2e1..7dce6bb 100644
--- a/include/cobra/core/DecompositionEngine.h
+++ b/include/cobra/core/DecompositionEngine.h
@@ -40,6 +40,9 @@ namespace cobra {
         std::unique_ptr< Expr > expr;
         ExtractorKind kind;
         uint8_t degree_used = 0;
+        // kProductAST only: true when the whole input is a single product term
+        // (SplitAddTree found no additive split), i.e. the core equals the input.
+        bool single_product = false;
     };
 
     struct DecompositionResult
diff --git a/include/cobra/core/ExprCost.h b/include/cobra/core/ExprCost.h
index d0433fc..8cbc9b9 100644
--- a/include/cobra/core/ExprCost.h
+++ b/include/cobra/core/ExprCost.h
@@ -22,4 +22,16 @@ namespace cobra {
 
     bool IsBetter(const ExprCost &candidate, const ExprCost &baseline);
 
+    // Returns true when `candidate` is a pathological size blow-up relative to
+    // `baseline`. A blow-up must clear two bars at once: it more than doubles
+    // the baseline's weighted size AND is large in absolute terms. The ratio
+    // catches change-of-basis expansions proportional to a large input (e.g.
+    // sum(xi) - xor(xi) recovers an exponential AND-basis form); the absolute
+    // floor spares the small ~2x expansions of legitimate canonicalization
+    // (NOT-over-arith lowering ~(b*b) -> -(b*b)-1 roughly doubles a tiny
+    // expression). This is deliberately keyed on weighted_size alone: it is a
+    // size-explosion guard, distinct from IsBetter's full lexicographic
+    // "is this an improvement" comparison.
+    bool IsCostBlowup(const ExprCost &candidate, const ExprCost &baseline);
+
 } // namespace cobra
diff --git a/include/cobra/core/ExprUtils.h b/include/cobra/core/ExprUtils.h
index 9d3c5fc..cd0ab41 100644
--- a/include/cobra/core/ExprUtils.h
+++ b/include/cobra/core/ExprUtils.h
@@ -18,6 +18,10 @@ namespace cobra {
     /// Rewrite every kVariable node's var_index through index_map.
     void RemapVarIndices(Expr &expr, const std::vector< uint32_t > &index_map);
 
+    /// Deep structural equality: same kind, constant, var_index, and children
+    /// (in order). Unlike std::hash<Expr> this never reports false positives.
+    bool ExprStructurallyEqual(const Expr &lhs, const Expr &rhs);
+
     /// Map a subset of variable names to their indices in the full variable list.
     std::vector< uint32_t > BuildVarSupport(
         const std::vector< std::string > &all_vars,
@@ -27,8 +31,8 @@ namespace cobra {
     /// Check if an Expr subtree contains only constants (no variables).
     bool IsConstantSubtree(const Expr &expr);
 
-    /// Returns true if any node in the AST is kShr.
-    bool ContainsShr(const Expr &expr);
+    /// Returns true if any node in the AST has the given kind.
+    bool ContainsType(const Expr &expr, Expr::Kind kind);
 
     /// Append the var_index of every kVariable node (pre-order). Duplicates
     /// are preserved; callers that want a deduplicated support set must
@@ -46,13 +50,9 @@ namespace cobra {
     /// Chains: constant folding → negation refolding → ExtractCommonFactor
     /// → constant folding.
     ///
-    /// Semantics-preserving under the assumption that std::hash<Expr>
-    /// does not collide on the input AST. ExtractCommonFactor uses
-    /// hash-based factor equality, so a hash collision could in
-    /// principle produce a non-equivalent rewrite. The hash-collision
-    /// tradeoff is accepted at the project level (see audit
-    /// 2026-05-04 lifting-passes-29 / -65). Callers requiring strict
-    /// semantics-preservation must re-verify the result.
+    /// Semantics-preserving: ExtractCommonFactor matches common factors by
+    /// exact structural equality (ExprStructurallyEqual), so the distributive
+    /// rewrite never fires on a non-equal factor.
     std::unique_ptr< Expr > CleanupFinalExpr(std::unique_ptr< Expr > expr, uint32_t bitwidth);
 
     /// Check if an Expr subtree depends on any variable.
diff --git a/include/cobra/core/MathUtils.h b/include/cobra/core/MathUtils.h
index c6c1ea6..51b5d75 100644
--- a/include/cobra/core/MathUtils.h
+++ b/include/cobra/core/MathUtils.h
@@ -37,15 +37,17 @@ namespace cobra {
     }
 
     // Modular inverse of an odd number x modulo 2^bits.
-    // Hensel lifting: x*x = 1 mod 8 for all odd x, so 3 bits are
-    // correct initially. Each iteration doubles the number of
-    // correct bits.
+    // Newton/Hensel lifting: the seed ((3 * x) ^ 2) -- i.e. (3*x) XOR 2, not a
+    // square -- satisfies x * seed = 1 mod 32 for all odd x, so 5 bits are
+    // correct initially. Each iteration doubles the correct bits
+    // (5 -> 10 -> 20 -> 40 -> 80), so 64-bit inverses need 4 iterations. (The
+    // bare seed x is correct to only 3 bits and would need a 5th iteration.)
     inline uint64_t ModInverseOdd(uint64_t x, uint32_t bits) {
         assert(bits >= 1);
         assert(x & 1);
         const uint64_t kModMask = Bitmask(bits);
-        uint64_t inv            = x & kModMask;
-        for (uint32_t b = 3; b < bits; b *= 2) { inv = (inv * (2 - (x * inv))) & kModMask; }
+        uint64_t inv            = ((3 * x) ^ 2) & kModMask;
+        for (uint32_t b = 5; b < bits; b *= 2) { inv = (inv * (2 - (x * inv))) & kModMask; }
         return inv & kModMask;
     }
 
diff --git a/include/cobra/core/PatternMatcher.h b/include/cobra/core/PatternMatcher.h
index 849f326..c97bd1f 100644
--- a/include/cobra/core/PatternMatcher.h
+++ b/include/cobra/core/PatternMatcher.h
@@ -20,4 +20,10 @@ namespace cobra {
     std::unique_ptr< Expr >
     SimplifyPatternSubtrees(std::unique_ptr< Expr > expr, uint32_t bitwidth);
 
+    // Recursively cancel XOR operands that appear an even number of times
+    // (T ^ T == 0), flattening nested XOR chains. This is an exact algebraic
+    // identity (no full-width approximation), so the result is provably
+    // equivalent to the input at every bit width.
+    std::unique_ptr< Expr > SimplifyXorChains(std::unique_ptr< Expr > expr, uint32_t bitwidth);
+
 } // namespace cobra
diff --git a/lib/core/CoeffInterpolator.cpp b/lib/core/CoeffInterpolator.cpp
index 8256a4b..4663c12 100644
--- a/lib/core/CoeffInterpolator.cpp
+++ b/lib/core/CoeffInterpolator.cpp
@@ -28,12 +28,16 @@ namespace cobra {
         // "without this variable" entry from the "with" entry to isolate its
         // contribution. Equivalent to evaluating directly in the (1, x, y, x&y)
         // basis rather than computing a change-of-basis matrix.
+        //
+        // Canonical block butterfly: each var pairs index i (bit clear) with
+        // i + half (bit set), so we touch exactly len/2 elements per var with
+        // no per-element bit test and contiguous access within each half-block.
         for (uint32_t var = 0; var < num_vars; ++var) {
-            const uint32_t stride = 1U << var;
-            for (size_t i = 0; i < len; ++i) {
-                if ((i & stride) != 0u) {
-                    const size_t i0 = i & ~static_cast< size_t >(stride);
-                    sig[i]          = (sig[i] - sig[i0]) & mask;
+            const size_t half  = size_t{ 1 } << var;
+            const size_t block = half << 1;
+            for (size_t base = 0; base < len; base += block) {
+                for (size_t i = base; i < base + half; ++i) {
+                    sig[i + half] = (sig[i + half] - sig[i]) & mask;
                 }
             }
         }
diff --git a/lib/core/CoefficientSplitter.cpp b/lib/core/CoefficientSplitter.cpp
index 1907f65..b04822f 100644
--- a/lib/core/CoefficientSplitter.cpp
+++ b/lib/core/CoefficientSplitter.cpp
@@ -1,5 +1,6 @@
 #include "cobra/core/CoefficientSplitter.h"
 #include "cobra/core/BitWidth.h"
+#include "cobra/core/MathUtils.h"
 #include "cobra/core/Trace.h"
 #include <bit>
 #include <cassert>
@@ -12,20 +13,8 @@ namespace cobra {
 
     uint64_t ModInverseOddHalf(uint64_t x, uint32_t w) {
         assert(w >= 2);
-        assert(x & 1);
-
-        // Target: x^{-1} mod 2^{w-1}.
-        // Hensel lifting: inv = x is correct mod 2^3 (since x^2 = 1 mod 8
-        // for all odd x). Each iteration doubles correct bits.
-        const uint32_t kTargetBits = w - 1;
-        const uint64_t kModMask = (kTargetBits >= 64) ? UINT64_MAX : (1ULL << kTargetBits) - 1;
-
-        uint64_t inv = x & kModMask;
-        // ceil(log2(kTargetBits)) iterations, starting from 3 correct bits
-        for (uint32_t bits = 3; bits < kTargetBits; bits *= 2) {
-            inv = (inv * (2 - (x * inv))) & kModMask;
-        }
-        return inv & kModMask;
+        // x^{-1} mod 2^{w-1} is exactly the general odd inverse at width w-1.
+        return ModInverseOdd(x, w - 1);
     }
 
     namespace {
diff --git a/lib/core/DecompositionEngine.cpp b/lib/core/DecompositionEngine.cpp
index a24c87b..7b309c9 100644
--- a/lib/core/DecompositionEngine.cpp
+++ b/lib/core/DecompositionEngine.cpp
@@ -157,8 +157,9 @@ namespace cobra {
         }
 
         CoreCandidate core;
-        core.expr = std::move(core_expr);
-        core.kind = ExtractorKind::kProductAST;
+        core.expr           = std::move(core_expr);
+        core.kind           = ExtractorKind::kProductAST;
+        core.single_product = (products.size() == 1);
         return SolverResult< CoreCandidate >::Success(std::move(core));
     }
 
diff --git a/lib/core/DecompositionPasses.cpp b/lib/core/DecompositionPasses.cpp
index 662203a..f98dd29 100644
--- a/lib/core/DecompositionPasses.cpp
+++ b/lib/core/DecompositionPasses.cpp
@@ -166,6 +166,30 @@ namespace cobra {
                 FullWidthCheckEval(*active_eval, num_vars, *core_payload.expr, ctx.bitwidth);
 
             if (direct_check.passed) {
+                // A degenerate product core -- the whole input as a single
+                // product term (single_product) -- "passes" the direct check
+                // only because it IS the input. Emitting it short-circuits the
+                // worklist as a no-op winner before the decomposition/signature
+                // passes can recover a simpler form. When such a core also has a
+                // (full-width-confirmed) spurious variable, a real reduction is
+                // reachable, so decline the short-circuit and let later passes
+                // run. Genuine sum-of-product cores (single_product == false)
+                // and cores with no spurious variable are unaffected. The
+                // cheap boolean elimination gates the 128-probe full-width
+                // confirmation: full-width spurious vars are always a subset
+                // of the boolean ones, so an empty boolean result is final.
+                if (expected_kind == ExtractorKind::kProductAST && core_payload.single_product
+                    && !EliminateAuxVars(decomp_sig, active_vars).spurious_vars.empty()
+                    && !EliminateAuxVars(decomp_sig, active_vars, *active_eval, ctx.bitwidth)
+                            .spurious_vars.empty())
+                {
+                    return Ok(
+                        PassResult{
+                            .decision    = PassDecision::kNotApplicable,
+                            .disposition = ItemDisposition::kRetainCurrent,
+                        }
+                    );
+                }
                 auto cost_info = ComputeCost(*core_payload.expr);
                 WorkItem cand_item;
                 cand_item.payload = CandidatePayload{
diff --git a/lib/core/ExprCost.cpp b/lib/core/ExprCost.cpp
index 83531f3..b6107f0 100644
--- a/lib/core/ExprCost.cpp
+++ b/lib/core/ExprCost.cpp
@@ -92,4 +92,14 @@ namespace cobra {
             );
     }
 
+    bool IsCostBlowup(const ExprCost &candidate, const ExprCost &baseline) {
+        // Output must exceed this multiple of the input to count as a blow-up.
+        constexpr uint32_t kBlowupRatio    = 2;
+        // ...and exceed this absolute weighted size, sparing the small ~2x
+        // expansions of legitimate canonicalization on tiny inputs.
+        constexpr uint32_t kBlowupAbsFloor = 32;
+        return candidate.weighted_size > kBlowupRatio * baseline.weighted_size
+            && candidate.weighted_size > kBlowupAbsFloor;
+    }
+
 } // namespace cobra
diff --git a/lib/core/ExprUtils.cpp b/lib/core/ExprUtils.cpp
index 03c179b..a831782 100644
--- a/lib/core/ExprUtils.cpp
+++ b/lib/core/ExprUtils.cpp
@@ -32,6 +32,18 @@ namespace cobra {
         for (auto &child : expr.children) { RemapVarIndices(*child, index_map); }
     }
 
+    bool ExprStructurallyEqual(const Expr &lhs, const Expr &rhs) {
+        if (lhs.kind != rhs.kind || lhs.constant_val != rhs.constant_val
+            || lhs.var_index != rhs.var_index || lhs.children.size() != rhs.children.size())
+        {
+            return false;
+        }
+        for (size_t i = 0; i < lhs.children.size(); ++i) {
+            if (!ExprStructurallyEqual(*lhs.children[i], *rhs.children[i])) { return false; }
+        }
+        return true;
+    }
+
     std::unique_ptr< Expr > BuildAndProduct(uint64_t mask) {
         std::unique_ptr< Expr > result;
         while (mask != 0) {
@@ -60,10 +72,10 @@ namespace cobra {
         });
     }
 
-    bool ContainsShr(const Expr &expr) {
-        if (expr.kind == Expr::Kind::kShr) { return true; }
-        return std::ranges::any_of(expr.children, [](const auto &child) {
-            return ContainsShr(*child);
+    bool ContainsType(const Expr &expr, Expr::Kind kind) {
+        if (expr.kind == kind) { return true; }
+        return std::ranges::any_of(expr.children, [kind](const auto &child) {
+            return ContainsType(*child, kind);
         });
     }
 
@@ -133,15 +145,17 @@ namespace cobra {
 
     namespace {
 
-        // Flatten a left-folded Add chain into a list of terms.
-        void FlattenAdd(
-            std::unique_ptr< Expr > node, std::vector< std::unique_ptr< Expr > > &terms
+        // Flatten a left-folded binary associative chain of `kind` (kAdd or
+        // kMul) into its operand list, moving each leaf out of the tree.
+        void FlattenAssoc(
+            std::unique_ptr< Expr > node, Expr::Kind kind,
+            std::vector< std::unique_ptr< Expr > > &out
         ) {
-            if (node->kind == Expr::Kind::kAdd) {
-                FlattenAdd(std::move(node->children[0]), terms);
-                FlattenAdd(std::move(node->children[1]), terms);
+            if (node->kind == kind) {
+                FlattenAssoc(std::move(node->children[0]), kind, out);
+                FlattenAssoc(std::move(node->children[1]), kind, out);
             } else {
-                terms.push_back(std::move(node));
+                out.push_back(std::move(node));
             }
         }
 
@@ -161,7 +175,7 @@ namespace cobra {
             if (expr->kind != Expr::Kind::kAdd) { return expr; }
 
             std::vector< std::unique_ptr< Expr > > terms;
-            FlattenAdd(std::move(expr), terms);
+            FlattenAssoc(std::move(expr), Expr::Kind::kAdd, terms);
 
             uint64_t const_sum = 0;
             std::vector< std::unique_ptr< Expr > > non_const;
@@ -214,18 +228,6 @@ namespace cobra {
             return expr;
         }
 
-        // Flatten binary Mul chain into factor list.
-        void FlattenMul(
-            std::unique_ptr< Expr > node, std::vector< std::unique_ptr< Expr > > &factors
-        ) {
-            if (node->kind == Expr::Kind::kMul) {
-                FlattenMul(std::move(node->children[0]), factors);
-                FlattenMul(std::move(node->children[1]), factors);
-            } else {
-                factors.push_back(std::move(node));
-            }
-        }
-
         // Rebuild a left-folded Mul chain from a factor list.
         std::unique_ptr< Expr > RebuildMul(std::vector< std::unique_ptr< Expr > > &factors) {
             auto result = std::move(factors[0]);
@@ -248,7 +250,7 @@ namespace cobra {
 
             // Flatten the Add chain.
             std::vector< std::unique_ptr< Expr > > terms;
-            FlattenAdd(std::move(expr), terms);
+            FlattenAssoc(std::move(expr), Expr::Kind::kAdd, terms);
 
             if (terms.size() < 2) {
                 if (terms.size() == 1) { return std::move(terms[0]); }
@@ -266,7 +268,7 @@ namespace cobra {
             for (auto &t : terms) {
                 TermFactors tf;
                 if (t->kind == Expr::Kind::kMul) {
-                    FlattenMul(std::move(t), tf.factors);
+                    FlattenAssoc(std::move(t), Expr::Kind::kMul, tf.factors);
                 } else {
                     tf.factors.push_back(std::move(t));
                 }
@@ -280,9 +282,8 @@ namespace cobra {
                 if (candidate->kind == Expr::Kind::kConstant) { continue; }
                 if (candidate->kind == Expr::Kind::kVariable) { continue; }
 
-                auto candidate_hash = std::hash< Expr >{}(*candidate);
-
-                // Check all other terms for this factor.
+                // Check all other terms for this factor, matching on exact
+                // structural equality (never a false positive, unlike a hash).
                 bool universal = true;
                 std::vector< size_t > match_indices;
                 match_indices.push_back(fi);
@@ -291,11 +292,7 @@ namespace cobra {
                     for (size_t fj = 0; fj < all_factors[ti].factors.size(); ++fj) {
                         auto &f = all_factors[ti].factors[fj];
                         if (f->kind == Expr::Kind::kConstant) { continue; }
-                        if (std::hash< Expr >{}(*f) == candidate_hash
-                            && f->kind == candidate->kind)
-                        {
-                            // Deep equality check via CloneExpr comparison.
-                            // Use the hash as strong filter — collisions are rare.
+                        if (ExprStructurallyEqual(*f, *candidate)) {
                             found = true;
                             match_indices.push_back(fj);
                             break;
diff --git a/lib/core/MultivarPolyRecovery.cpp b/lib/core/MultivarPolyRecovery.cpp
index ef11b20..7aded93 100644
--- a/lib/core/MultivarPolyRecovery.cpp
+++ b/lib/core/MultivarPolyRecovery.cpp
@@ -27,6 +27,118 @@ namespace cobra {
         };
     } // namespace multivar_poly
 
+    namespace {
+
+        // Convert an evaluated {0..max_degree}^k grid (mixed-radix base
+        // max_degree+1, little-endian over support_vars) into factorial-basis
+        // coefficients via tensor-product forward differences. The grid is
+        // consumed in place. Validation is the caller's responsibility.
+        SolverResult< NormalizedPoly > RecoverFromGrid(
+            std::vector< uint64_t > table, const std::vector< uint32_t > &support_vars,
+            uint32_t total_num_vars, uint32_t bitwidth, uint8_t max_degree
+        ) {
+            const auto kK           = static_cast< uint32_t >(support_vars.size());
+            const uint64_t kMask    = Bitmask(bitwidth);
+            const auto kBase        = static_cast< size_t >(max_degree) + 1;
+            const size_t table_size = table.size();
+
+            // Tensor-product forward differences: max_degree passes per dimension
+            for (uint32_t dim = 0; dim < kK; ++dim) {
+                size_t stride = 1;
+                for (uint32_t i = 0; i < dim; ++i) { stride *= kBase; }
+
+                for (uint32_t pass = 1; pass <= max_degree; ++pass) {
+                    for (size_t idx = table_size; idx-- > 0;) {
+                        const auto kCoord = static_cast< uint32_t >((idx / stride) % kBase);
+                        if (kCoord < pass) { continue; }
+                        table[idx] = (table[idx] - table[idx - stride]) & kMask;
+                    }
+                }
+            }
+
+            // Convert forward differences to factorial-basis coefficients
+            auto nv = static_cast< uint8_t >(total_num_vars);
+            NormalizedPoly result;
+            result.num_vars = nv;
+            result.bitwidth = bitwidth;
+
+            std::array< uint8_t, kMaxPolyVars > exps{};
+
+            // Per-degree odd-part factorials at full 64-bit width, built once.
+            // OddPartFactorial(e, bw) == odd_fact[e] & Bitmask(bw), so the
+            // per-monomial product below uses the table directly under the
+            // existing kPrecMask instead of recomputing the odd-part product.
+            std::vector< uint64_t > odd_fact(static_cast< size_t >(max_degree) + 1, 1);
+            for (uint32_t e = 2; e <= max_degree; ++e) {
+                uint32_t odd = e;
+                while ((odd & 1) == 0) { odd >>= 1; }
+                odd_fact[e] = odd_fact[e - 1] * odd;
+            }
+
+            for (size_t idx = 0; idx < table_size; ++idx) {
+                const uint64_t kAlpha = table[idx];
+                if (kAlpha == 0) { continue; }
+
+                // Decode mixed-radix to per-variable exponents
+                exps.fill(0);
+                size_t tmp = idx;
+                uint32_t q = 0;
+                for (uint32_t i = 0; i < kK; ++i) {
+                    const auto kE          = static_cast< uint8_t >(tmp % kBase);
+                    exps[support_vars[i]]  = kE;
+                    q                     += TwosInFactorial(kE);
+                    tmp                   /= kBase;
+                }
+
+                // Null-space term: 2^q >= bitwidth means coefficient vanishes
+                if (q >= bitwidth) { continue; }
+
+                // Divisibility gate: alpha must be divisible by 2^q
+                if (q > 0) {
+                    const uint64_t kLowBits = kAlpha & ((1ULL << q) - 1);
+                    if (kLowBits != 0) {
+                        ReasonDetail reason{
+                            .top = { .code = { ReasonCategory::kNoSolution,
+                                               ReasonDomain::kMultivarPoly,
+                                               multivar_poly::kDivisibilityFail },
+                                    .message =
+                                         "falling-factorial coefficient fails divisibility "
+                                         "gate" }
+                        };
+                        return SolverResult< NormalizedPoly >::Blocked(std::move(reason));
+                    }
+                }
+
+                const uint32_t kPrecBits = bitwidth - q;
+
+                // Product of odd parts mod 2^kPrecBits, via the precomputed
+                // table (masking by kPrecMask is equivalent to computing the
+                // odd-part product at width kPrecBits).
+                uint64_t odd_product = 1;
+                const uint64_t kPrecMask =
+                    (kPrecBits >= 64) ? UINT64_MAX : ((1ULL << kPrecBits) - 1);
+                for (uint32_t i = 0; i < kK; ++i) {
+                    uint8_t e = exps[support_vars[i]];
+                    if (e >= 2) { odd_product = (odd_product * odd_fact[e]) & kPrecMask; }
+                }
+
+                // h = (alpha >> q) * ModInverseOdd(odd_product) mod 2^kPrecBits
+                uint64_t h = (kAlpha >> q) & kPrecMask;
+                if (odd_product != 1) {
+                    h = (h * ModInverseOdd(odd_product, kPrecBits)) & kPrecMask;
+                }
+
+                if (h == 0) { continue; }
+
+                auto key           = MonomialKey::FromExponents(exps.data(), nv);
+                result.coeffs[key] = h;
+            }
+
+            return SolverResult< NormalizedPoly >::Success(std::move(result));
+        }
+
+    } // namespace
+
     SolverResult< NormalizedPoly > RecoverMultivarPoly(
         const Evaluator &eval, const std::vector< uint32_t > &support_vars,
         uint32_t total_num_vars, uint32_t bitwidth, uint8_t max_degree
@@ -97,87 +209,9 @@ namespace cobra {
         }
         for (uint32_t i = 0; i < kK; ++i) { point[support_vars[i]] = 0; }
 
-        // Tensor-product forward differences: max_degree passes per dimension
-        for (uint32_t dim = 0; dim < kK; ++dim) {
-            size_t stride = 1;
-            for (uint32_t i = 0; i < dim; ++i) { stride *= kBase; }
-
-            for (uint32_t pass = 1; pass <= max_degree; ++pass) {
-                for (size_t idx = table_size; idx-- > 0;) {
-                    const auto kCoord = static_cast< uint32_t >((idx / stride) % kBase);
-                    if (kCoord < pass) { continue; }
-                    table[idx] = (table[idx] - table[idx - stride]) & kMask;
-                }
-            }
-        }
-
-        // Convert forward differences to factorial-basis coefficients
-        auto nv = static_cast< uint8_t >(total_num_vars);
-        NormalizedPoly result;
-        result.num_vars = nv;
-        result.bitwidth = bitwidth;
-
-        std::array< uint8_t, kMaxPolyVars > exps{};
-
-        for (size_t idx = 0; idx < table_size; ++idx) {
-            const uint64_t kAlpha = table[idx];
-            if (kAlpha == 0) { continue; }
-
-            // Decode mixed-radix to per-variable exponents
-            exps.fill(0);
-            size_t tmp = idx;
-            uint32_t q = 0;
-            for (uint32_t i = 0; i < kK; ++i) {
-                const auto kE          = static_cast< uint8_t >(tmp % kBase);
-                exps[support_vars[i]]  = kE;
-                q                     += TwosInFactorial(kE);
-                tmp                   /= kBase;
-            }
-
-            // Null-space term: 2^q >= bitwidth means coefficient vanishes
-            if (q >= bitwidth) { continue; }
-
-            // Divisibility gate: alpha must be divisible by 2^q
-            if (q > 0) {
-                const uint64_t kLowBits = kAlpha & ((1ULL << q) - 1);
-                if (kLowBits != 0) {
-                    ReasonDetail reason{
-                        .top = { .code    = { ReasonCategory::kNoSolution,
-                                              ReasonDomain::kMultivarPoly,
-                                              multivar_poly::kDivisibilityFail },
-                                .message = "falling-factorial coefficient fails divisibility "
-                                            "gate" }
-                    };
-                    return SolverResult< NormalizedPoly >::Blocked(std::move(reason));
-                }
-            }
-
-            const uint32_t kPrecBits = bitwidth - q;
-
-            // Compute product of odd parts mod 2^kPrecBits
-            uint64_t odd_product = 1;
-            const uint64_t kPrecMask =
-                (kPrecBits >= 64) ? UINT64_MAX : ((1ULL << kPrecBits) - 1);
-            for (uint32_t i = 0; i < kK; ++i) {
-                uint8_t e = exps[support_vars[i]];
-                if (e >= 2) {
-                    odd_product = (odd_product * OddPartFactorial(e, kPrecBits)) & kPrecMask;
-                }
-            }
-
-            // h = (alpha >> q) * ModInverseOdd(odd_product) mod 2^kPrecBits
-            uint64_t h = (kAlpha >> q) & kPrecMask;
-            if (odd_product != 1) {
-                h = (h * ModInverseOdd(odd_product, kPrecBits)) & kPrecMask;
-            }
-
-            if (h == 0) { continue; }
-
-            auto key           = MonomialKey::FromExponents(exps.data(), nv);
-            result.coeffs[key] = h;
-        }
-
-        return SolverResult< NormalizedPoly >::Success(std::move(result));
+        return RecoverFromGrid(
+            std::move(table), support_vars, total_num_vars, bitwidth, max_degree
+        );
     }
 
     SolverResult< PolyRecoveryResult > RecoverAndVerifyPoly(
@@ -194,20 +228,92 @@ namespace cobra {
             return SolverResult< PolyRecoveryResult >::Inapplicable(std::move(reason));
         }
 
-        // Each degree is recovered independently (no incremental reuse).
-        for (uint8_t d = min_degree; d <= max_degree_cap; ++d) {
-            auto poly = RecoverMultivarPoly(eval, support_vars, total_num_vars, bitwidth, d);
-            if (!poly.Succeeded()) { continue; }
+        // Validate the degree-independent preconditions once. RecoverMultivarPoly
+        // re-checks these per call; when they fail the old loop swallowed the
+        // Inapplicable into kNoVerifiedDegree, so mirror that by skipping the
+        // grid work and falling through to the exhaustion result.
+        bool inputs_ok = !support_vars.empty() && total_num_vars <= kMaxPolyVars
+            && bitwidth >= 2 && bitwidth <= 64;
+        if (inputs_ok) {
+            for (auto idx : support_vars) {
+                if (idx >= total_num_vars) {
+                    inputs_ok = false;
+                    break;
+                }
+            }
+        }
+
+        if (inputs_ok) {
+            const auto kK        = static_cast< uint32_t >(support_vars.size());
+            const uint64_t kMask = Bitmask(bitwidth);
+
+            // Incrementally-grown {0..d}^k evaluation grid (mixed-radix base
+            // d+1). Each distinct support point is evaluated once across all
+            // degrees: a higher degree extends the grid by its new shell rather
+            // than re-evaluating from scratch (evaluator calls dominate the
+            // per-degree cost). Reuse is exact because the evaluator is pure.
+            std::vector< uint64_t > grid;
+            uint32_t grid_base = 0; // 0 = empty; otherwise current degree + 1
+            std::vector< uint64_t > point(total_num_vars, 0);
+
+            auto eval_at = [&](size_t idx, uint32_t base) -> uint64_t {
+                size_t tmp = idx;
+                for (uint32_t i = 0; i < kK; ++i) {
+                    point[support_vars[i]]  = tmp % base;
+                    tmp                    /= base;
+                }
+                const uint64_t v = eval(point) & kMask;
+                for (uint32_t i = 0; i < kK; ++i) { point[support_vars[i]] = 0; }
+                return v;
+            };
+
+            for (uint8_t d = min_degree; d <= max_degree_cap; ++d) {
+                if (d < 1) { continue; } // RecoverMultivarPoly rejects max_degree < 1
+
+                const uint32_t kBase = static_cast< uint32_t >(d) + 1;
+                size_t table_size    = 1;
+                for (uint32_t i = 0; i < kK; ++i) { table_size *= kBase; }
 
-            auto expr = BuildPolyExpr(poly.TakePayload());
-            if (!expr.has_value()) { continue; }
+                // Extend the grid to base kBase, evaluating only the new points.
+                if (grid_base == 0) {
+                    grid.assign(table_size, 0);
+                    for (size_t idx = 0; idx < table_size; ++idx) {
+                        grid[idx] = eval_at(idx, kBase);
+                    }
+                } else {
+                    std::vector< uint64_t > grown(table_size, 0);
+                    for (size_t idx = 0; idx < table_size; ++idx) {
+                        size_t tmp     = idx;
+                        size_t old_idx = 0;
+                        size_t place   = 1;
+                        bool is_old    = true;
+                        for (uint32_t i = 0; i < kK; ++i) {
+                            const size_t kCoord  = tmp % kBase;
+                            tmp                 /= kBase;
+                            if (kCoord >= grid_base) { is_old = false; }
+                            old_idx += kCoord * place;
+                            place   *= grid_base;
+                        }
+                        grown[idx] = is_old ? grid[old_idx] : eval_at(idx, kBase);
+                    }
+                    grid = std::move(grown);
+                }
+                grid_base = kBase;
+
+                // RecoverFromGrid consumes its grid in place, so pass a copy.
+                auto poly = RecoverFromGrid(grid, support_vars, total_num_vars, bitwidth, d);
+                if (!poly.Succeeded()) { continue; }
 
-            auto check = FullWidthCheckEval(eval, total_num_vars, *expr.value(), bitwidth);
-            if (!check.passed) { continue; }
+                auto expr = BuildPolyExpr(poly.TakePayload());
+                if (!expr.has_value()) { continue; }
 
-            return SolverResult< PolyRecoveryResult >::Success(
-                PolyRecoveryResult{ std::move(expr.value()), d }
-            );
+                auto check = FullWidthCheckEval(eval, total_num_vars, *expr.value(), bitwidth);
+                if (!check.passed) { continue; }
+
+                return SolverResult< PolyRecoveryResult >::Success(
+                    PolyRecoveryResult{ std::move(expr.value()), d }
+                );
+            }
         }
         ReasonDetail reason{
             .top = { .code    = { ReasonCategory::kSearchExhausted, ReasonDomain::kMultivarPoly,
diff --git a/lib/core/Orchestrator.cpp b/lib/core/Orchestrator.cpp
index 73b746e..37ccae3 100644
--- a/lib/core/Orchestrator.cpp
+++ b/lib/core/Orchestrator.cpp
@@ -840,12 +840,12 @@ namespace cobra {
 
         SimplifyOutcome ToSimplifyOutcome(
             OrchestratorResult result, const Expr *original_expr,
-            const OrchestratorTelemetry &telemetry, uint32_t bitwidth
+            const OrchestratorTelemetry &telemetry, uint32_t bitwidth,
+            const std::optional< ExprCost > &input_cost
         ) {
             SimplifyOutcome outcome;
 
             if (result.outcome.Succeeded()) {
-                outcome.kind      = SimplifyOutcome::Kind::kSimplified;
                 outcome.real_vars = result.outcome.RealVars();
                 // Read PassOutcome.Verification() instead of the parallel
                 // ItemMetadata.verification field. The two were initialized
@@ -858,6 +858,28 @@ namespace cobra {
                     result.outcome.Verification() == VerificationState::kVerified;
                 outcome.expr       = CleanupFinalExpr(result.outcome.TakeExpr(), bitwidth);
                 outcome.sig_vector = std::move(result.metadata.sig_vector);
+                outcome.kind       = SimplifyOutcome::Kind::kSimplified;
+
+                // Don't return a result that blows up relative to the input. A
+                // CoB-linear function (e.g. sum(xi) - xor(xi)) recovers an
+                // exponential AND-basis expansion that is correct but far larger
+                // than the already-minimal input; keep the input in that case.
+                // See IsCostBlowup for the ratio/floor rationale.
+                if (original_expr != nullptr && input_cost.has_value()) {
+                    const auto out_cost = ComputeCost(*outcome.expr).cost;
+                    if (IsCostBlowup(out_cost, *input_cost)) {
+                        outcome.kind = SimplifyOutcome::Kind::kUnchangedUnsupported;
+                        outcome.expr = CloneExpr(*original_expr);
+                        outcome.real_vars.clear();
+                        outcome.verified = false;
+                        // Stamp a structured reason so the unsupported result
+                        // still satisfies the has_structured_reason invariant
+                        // (set on result.metadata so the copy below propagates).
+                        result.metadata.reason_code =
+                            ReasonCode{ ReasonCategory::kCostRejected,
+                                        ReasonDomain::kOrchestrator, 0 };
+                    }
+                }
             } else {
                 outcome.kind = SimplifyOutcome::Kind::kUnchangedUnsupported;
                 outcome.expr = original_expr != nullptr ? CloneExpr(*original_expr) : nullptr;
@@ -947,7 +969,7 @@ namespace cobra {
         // recurse only a handful of times before reaching 1 bit.
         if (input_expr != nullptr) {
             auto mask = DetectRootLowBitMask(*input_expr, opts.bitwidth);
-            if (mask.has_value() && !ContainsShr(*mask->inner)) {
+            if (mask.has_value() && !ContainsType(*mask->inner, Expr::Kind::kShr)) {
                 auto inner      = CloneExpr(*mask->inner);
                 uint32_t eff_bw = mask->effective_width;
                 auto inner_sig  = EvaluateBooleanSignature(
@@ -1004,13 +1026,21 @@ namespace cobra {
         Worklist worklist;
         OrchestratorTelemetry telemetry;
 
+        // Cost of the raw input, computed once and reused by every return path
+        // (the blow-up gate in ToSimplifyOutcome and the XOR exhaustion
+        // fallback). Absent when there is no input AST (sig-only path).
+        const std::optional< ExprCost > input_cost = input_expr
+            ? std::optional< ExprCost >(ComputeCost(*input_expr).cost)
+            : std::nullopt;
+
         // Seeding
         if (input_expr == nullptr) {
             auto seed_result = SeedNoAst(sig, vars, context, worklist);
             if (!seed_result.has_value()) { return std::unexpected(seed_result.error()); }
             if (seed_result.value().has_value()) {
                 return Ok(ToSimplifyOutcome(
-                    std::move(*seed_result.value()), input_expr, telemetry, context.bitwidth
+                    std::move(*seed_result.value()), input_expr, telemetry, context.bitwidth,
+                    input_cost
                 ));
             }
         } else {
@@ -1018,7 +1048,8 @@ namespace cobra {
             if (!seed_result.has_value()) { return std::unexpected(seed_result.error()); }
             if (seed_result.value().has_value()) {
                 return Ok(ToSimplifyOutcome(
-                    std::move(*seed_result.value()), input_expr, telemetry, context.bitwidth
+                    std::move(*seed_result.value()), input_expr, telemetry, context.bitwidth,
+                    input_cost
                 ));
             }
         }
@@ -1135,7 +1166,7 @@ namespace cobra {
                             .metadata     = std::move(item.metadata),
                             .run_metadata = context.run_metadata,
                         },
-                        input_expr, telemetry, context.bitwidth
+                        input_expr, telemetry, context.bitwidth, input_cost
                     ));
                 }
             }
@@ -1356,13 +1387,55 @@ namespace cobra {
         }
 
         telemetry.queue_high_water = static_cast< uint32_t >(worklist.HighWaterMark());
+
+        // Exhaustion fallback: cancel structurally-repeated XOR operands in the
+        // raw input (T ^ T == 0, an EXACT identity at every bit width). When the
+        // survivors have a degenerate {0,1} signature, no signature/decomposition
+        // pass re-emits them, so the worklist exhausts even though the input
+        // collapses. Because this is exact (not a full-width approximation) the
+        // result is provably equivalent and sound to return directly. Fire only
+        // when it actually cancelled something and the result is strictly
+        // cheaper; the full-width check is defense in depth, not the proof.
+        if (input_expr != nullptr && context.evaluator
+            && ContainsType(*input_expr, Expr::Kind::kXor))
+        {
+            auto xor_peel = SimplifyXorChains(CloneExpr(*input_expr), context.bitwidth);
+            if (!ExprStructurallyEqual(*xor_peel, *input_expr)
+                && IsBetter(ComputeCost(*xor_peel).cost, *input_cost))
+            {
+                const auto num_vars = static_cast< uint32_t >(vars.size());
+                auto check          = FullWidthCheckEval(
+                    *context.evaluator, num_vars, *xor_peel, context.bitwidth
+                );
+                if (check.passed) {
+                    // This is a genuine (exact) simplification, not the
+                    // exhaustion failure final_meta was built to describe. Drop
+                    // the stale failure lineage so the kSimplified result does
+                    // not report a search-exhausted reason or cause chain.
+                    final_meta.reason_code.reset();
+                    final_meta.cause_chain.clear();
+                    final_meta.candidate_failed_verification = false;
+                    return Ok(ToSimplifyOutcome(
+                        OrchestratorResult{
+                            .outcome = PassOutcome::Success(
+                                std::move(xor_peel), vars, VerificationState::kVerified
+                            ),
+                            .metadata     = std::move(final_meta),
+                            .run_metadata = context.run_metadata,
+                        },
+                        input_expr, telemetry, context.bitwidth, input_cost
+                    ));
+                }
+            }
+        }
+
         return Ok(ToSimplifyOutcome(
             OrchestratorResult{
                 .outcome      = PassOutcome::Blocked(std::move(exhaustion_reason)),
                 .metadata     = std::move(final_meta),
                 .run_metadata = context.run_metadata,
             },
-            input_expr, telemetry, context.bitwidth
+            input_expr, telemetry, context.bitwidth, input_cost
         ));
     }
 
diff --git a/lib/core/OrchestratorPasses.cpp b/lib/core/OrchestratorPasses.cpp
index 80a2a67..7521519 100644
--- a/lib/core/OrchestratorPasses.cpp
+++ b/lib/core/OrchestratorPasses.cpp
@@ -282,20 +282,6 @@ namespace cobra {
             size_t r = 0;
         };
 
-        bool ExprStructurallyEqual(const Expr &lhs, const Expr &rhs) {
-            if (lhs.kind != rhs.kind || lhs.constant_val != rhs.constant_val
-                || lhs.var_index != rhs.var_index || lhs.children.size() != rhs.children.size())
-            {
-                return false;
-            }
-            for (size_t i = 0; i < lhs.children.size(); ++i) {
-                if (!ExprStructurallyEqual(*lhs.children[i], *rhs.children[i])) {
-                    return false;
-                }
-            }
-            return true;
-        }
-
         std::unique_ptr< Expr >
         ReconstructMaskedProductFactor(const Expr &inclusive_term, const Expr &exclusive_term) {
             if (inclusive_term.kind != Expr::Kind::kAnd
diff --git a/lib/core/PatternMatcher.cpp b/lib/core/PatternMatcher.cpp
index f5ecdad..716d708 100644
--- a/lib/core/PatternMatcher.cpp
+++ b/lib/core/PatternMatcher.cpp
@@ -1266,6 +1266,266 @@ namespace cobra {
             return result;
         }
 
+        // ---- Inclusion-exclusion disjunction recovery ----------------------
+        //
+        // Reverses the MBA obfuscation A + B - (A & B) -> A | B for arbitrary
+        // operands (including arithmetic ones such as 10*y+5), where A and B may
+        // be spread across several terms of a flattened additive sum. Operands
+        // are read verbatim from the AND node's children; the rewrite is the
+        // exact inclusion-exclusion identity and is verified with FullWidthCheck.
+
+        struct AdditiveTerm
+        {
+            uint64_t coeff;
+            const Expr *atom; // non-owning; points into the source tree
+        };
+
+        // Flatten `e` (scaled by `coeff`) into signed additive terms plus an
+        // accumulated constant. Constant multipliers fold into the coefficient.
+        void FlattenAdditive(
+            const Expr &e, uint64_t coeff, uint32_t bitwidth,
+            std::vector< AdditiveTerm > &terms, uint64_t &constant
+        ) {
+            switch (e.kind) {
+                case Expr::Kind::kAdd:
+                    for (const auto &child : e.children) {
+                        FlattenAdditive(*child, coeff, bitwidth, terms, constant);
+                    }
+                    return;
+                case Expr::Kind::kNeg:
+                    FlattenAdditive(
+                        *e.children[0], ModNeg(coeff, bitwidth), bitwidth, terms, constant
+                    );
+                    return;
+                case Expr::Kind::kConstant:
+                    constant =
+                        ModAdd(constant, ModMul(coeff, e.constant_val, bitwidth), bitwidth);
+                    return;
+                case Expr::Kind::kMul:
+                    if (e.children.size() == 2 && e.children[0]->kind == Expr::Kind::kConstant)
+                    {
+                        FlattenAdditive(
+                            *e.children[1],
+                            ModMul(coeff, e.children[0]->constant_val, bitwidth), bitwidth,
+                            terms, constant
+                        );
+                        return;
+                    }
+                    if (e.children.size() == 2 && e.children[1]->kind == Expr::Kind::kConstant)
+                    {
+                        FlattenAdditive(
+                            *e.children[0],
+                            ModMul(coeff, e.children[1]->constant_val, bitwidth), bitwidth,
+                            terms, constant
+                        );
+                        return;
+                    }
+                    terms.push_back({ coeff, &e });
+                    return;
+                default:
+                    terms.push_back({ coeff, &e });
+                    return;
+            }
+        }
+
+        // Mark pool terms matching each of `need` (exact coeff + structural
+        // atom) as consumed. Returns false (leaving `consumed` unchanged) when
+        // any needed term is absent.
+        bool ConsumeTerms(
+            const std::vector< AdditiveTerm > &pool, const std::vector< AdditiveTerm > &need,
+            std::vector< bool > &consumed
+        ) {
+            auto trial = consumed;
+            for (const auto &nt : need) {
+                bool found = false;
+                for (size_t i = 0; i < pool.size(); ++i) {
+                    if (trial[i]) { continue; }
+                    if (pool[i].coeff == nt.coeff
+                        && ExprStructurallyEqual(*pool[i].atom, *nt.atom))
+                    {
+                        trial[i] = true;
+                        found    = true;
+                        break;
+                    }
+                }
+                if (!found) { return false; }
+            }
+            consumed = std::move(trial);
+            return true;
+        }
+
+        std::unique_ptr< Expr > RebuildAdditive(
+            const std::vector< AdditiveTerm > &pool, const std::vector< bool > &consumed,
+            uint64_t constant, std::unique_ptr< Expr > extra, uint32_t bitwidth
+        ) {
+            std::unique_ptr< Expr > result;
+            if (constant != 0) { result = Expr::Constant(constant); }
+            for (size_t i = 0; i < pool.size(); ++i) {
+                if (consumed[i]) { continue; }
+                auto term = ApplyCoefficient(CloneExpr(*pool[i].atom), pool[i].coeff, bitwidth);
+                result =
+                    result ? Expr::Add(std::move(result), std::move(term)) : std::move(term);
+            }
+            if (extra) {
+                result =
+                    result ? Expr::Add(std::move(result), std::move(extra)) : std::move(extra);
+            }
+            return result ? std::move(result) : Expr::Constant(0);
+        }
+
+        // Confirm `candidate` matches `original` at random full-width inputs.
+        // candidate reuses original's variable indices, so an identity var_map
+        // over [0, max_index] is sufficient (no densification needed).
+        bool VerifyRecovery(const Expr &original, const Expr &candidate, uint32_t bitwidth) {
+            std::vector< uint32_t > support;
+            CollectSupport(original, support);
+            uint32_t num_vars = 0;
+            for (uint32_t v : support) { num_vars = std::max(num_vars, v + 1); }
+            return FullWidthCheck(original, num_vars, candidate, {}, bitwidth).passed;
+        }
+
+        // Attempt to collapse the inclusion-exclusion pattern anchored at the
+        // AND term `terms[and_idx]`. Returns the rewritten expression on success.
+        std::optional< std::unique_ptr< Expr > > TryRecoverDisjunctionAt(
+            const std::vector< AdditiveTerm > &terms, uint64_t constant, size_t and_idx,
+            const Expr &expr, uint32_t bitwidth
+        ) {
+            const Expr *and_atom = terms[and_idx].atom;
+            if (and_atom->kind != Expr::Kind::kAnd || and_atom->children.size() != 2) {
+                return std::nullopt;
+            }
+            const uint64_t c = ModNeg(terms[and_idx].coeff, bitwidth);
+            if (c == 0) { return std::nullopt; }
+
+            std::vector< AdditiveTerm > a_terms;
+            std::vector< AdditiveTerm > b_terms;
+            uint64_t a_const = 0;
+            uint64_t b_const = 0;
+            FlattenAdditive(*and_atom->children[0], c, bitwidth, a_terms, a_const);
+            FlattenAdditive(*and_atom->children[1], c, bitwidth, b_terms, b_const);
+
+            std::vector< bool > consumed(terms.size(), false);
+            consumed[and_idx] = true;
+            if (!ConsumeTerms(terms, a_terms, consumed)) { return std::nullopt; }
+            if (!ConsumeTerms(terms, b_terms, consumed)) { return std::nullopt; }
+
+            const uint64_t new_constant =
+                ModSub(ModSub(constant, a_const, bitwidth), b_const, bitwidth);
+            auto or_term = ApplyCoefficient(
+                Expr::BitwiseOr(
+                    CloneExpr(*and_atom->children[0]), CloneExpr(*and_atom->children[1])
+                ),
+                c, bitwidth
+            );
+            auto candidate =
+                RebuildAdditive(terms, consumed, new_constant, std::move(or_term), bitwidth);
+
+            if (!IsBetter(ComputeCost(*candidate).cost, ComputeCost(expr).cost)) {
+                return std::nullopt;
+            }
+            if (!VerifyRecovery(expr, *candidate, bitwidth)) { return std::nullopt; }
+            return candidate;
+        }
+
+        // Cheap precondition for TryRecoverInclusionExclusion: does the additive
+        // chain rooted at `e` contain a top-level 2-child AND term? Mirrors
+        // FlattenAdditive's descent (through kAdd / kNeg / constant-scaled kMul)
+        // but allocates nothing, so additive nodes with no AND term skip the
+        // FlattenAdditive + per-term scan entirely.
+        bool AdditiveHasBinaryAnd(const Expr &e) {
+            switch (e.kind) {
+                case Expr::Kind::kAdd:
+                    for (const auto &child : e.children) {
+                        if (AdditiveHasBinaryAnd(*child)) { return true; }
+                    }
+                    return false;
+                case Expr::Kind::kNeg:
+                    return AdditiveHasBinaryAnd(*e.children[0]);
+                case Expr::Kind::kMul:
+                    if (e.children.size() == 2 && e.children[0]->kind == Expr::Kind::kConstant)
+                    {
+                        return AdditiveHasBinaryAnd(*e.children[1]);
+                    }
+                    if (e.children.size() == 2 && e.children[1]->kind == Expr::Kind::kConstant)
+                    {
+                        return AdditiveHasBinaryAnd(*e.children[0]);
+                    }
+                    return false;
+                case Expr::Kind::kAnd:
+                    return e.children.size() == 2;
+                default:
+                    return false;
+            }
+        }
+
+        std::optional< std::unique_ptr< Expr > >
+        TryRecoverInclusionExclusion(const Expr &expr, uint32_t bitwidth) {
+            if (expr.kind != Expr::Kind::kAdd && expr.kind != Expr::Kind::kNeg) {
+                return std::nullopt;
+            }
+            if (!AdditiveHasBinaryAnd(expr)) { return std::nullopt; }
+            std::vector< AdditiveTerm > terms;
+            uint64_t constant = 0;
+            FlattenAdditive(expr, 1, bitwidth, terms, constant);
+
+            for (size_t i = 0; i < terms.size(); ++i) {
+                auto recovered = TryRecoverDisjunctionAt(terms, constant, i, expr, bitwidth);
+                if (recovered.has_value()) { return recovered; }
+            }
+            return std::nullopt;
+        }
+
+        void FlattenXor(const Expr &e, std::vector< const Expr * > &out) {
+            if (e.kind == Expr::Kind::kXor) {
+                for (const auto &child : e.children) { FlattenXor(*child, out); }
+                return;
+            }
+            out.push_back(&e);
+        }
+
+        // Cancel XOR operands appearing an even number of times (T ^ T == 0).
+        // Flattens the XOR chain and keeps each distinct operand that occurs an
+        // odd number of times. Universally sound; a FullWidthCheck backstops the
+        // structural equality. Unlike the signature path, this fires even when
+        // the surviving operand has a degenerate {0,1} signature.
+        std::optional< std::unique_ptr< Expr > >
+        TryXorSelfCancel(const Expr &expr, uint32_t bitwidth) {
+            if (expr.kind != Expr::Kind::kXor) { return std::nullopt; }
+
+            std::vector< const Expr * > operands;
+            FlattenXor(expr, operands);
+
+            std::vector< bool > consumed(operands.size(), false);
+            std::vector< const Expr * > survivors;
+            for (size_t i = 0; i < operands.size(); ++i) {
+                if (consumed[i]) { continue; }
+                size_t count = 1;
+                consumed[i]  = true;
+                for (size_t j = i + 1; j < operands.size(); ++j) {
+                    if (!consumed[j] && ExprStructurallyEqual(*operands[i], *operands[j])) {
+                        consumed[j] = true;
+                        ++count;
+                    }
+                }
+                if (count % 2 == 1) { survivors.push_back(operands[i]); }
+            }
+
+            if (survivors.size() == operands.size()) { return std::nullopt; }
+
+            std::unique_ptr< Expr > result;
+            if (survivors.empty()) {
+                result = Expr::Constant(0);
+            } else {
+                result = CloneExpr(*survivors[0]);
+                for (size_t i = 1; i < survivors.size(); ++i) {
+                    result = Expr::BitwiseXor(std::move(result), CloneExpr(*survivors[i]));
+                }
+            }
+
+            if (!VerifyRecovery(expr, *result, bitwidth)) { return std::nullopt; }
+            return result;
+        }
+
     } // namespace
 
     std::optional< std::unique_ptr< Expr > >
@@ -1314,8 +1574,30 @@ namespace cobra {
         }
 
         auto rewritten = TrySimplifyPatternSubtree(*expr, bitwidth);
-        if (!rewritten.has_value()) { return expr; }
-        return SimplifyPatternSubtrees(std::move(*rewritten), bitwidth);
+        if (rewritten.has_value()) {
+            return SimplifyPatternSubtrees(std::move(*rewritten), bitwidth);
+        }
+
+        auto recovered = TryRecoverInclusionExclusion(*expr, bitwidth);
+        if (recovered.has_value()) {
+            return SimplifyPatternSubtrees(std::move(*recovered), bitwidth);
+        }
+        return expr;
+    }
+
+    std::unique_ptr< Expr > SimplifyXorChains(std::unique_ptr< Expr > expr, uint32_t bitwidth) {
+        // Cancel repeated operands across the full XOR chain rooted here first
+        // (top-down): flattening the whole chain before reducing children avoids
+        // a nested pair collapsing to 0 and stranding an odd third copy.
+        auto cancelled = TryXorSelfCancel(*expr, bitwidth);
+        if (cancelled.has_value()) {
+            return SimplifyXorChains(std::move(*cancelled), bitwidth);
+        }
+        // No cancellation here: recurse into children to handle nested chains.
+        for (auto &child : expr->children) {
+            child = SimplifyXorChains(std::move(child), bitwidth);
+        }
+        return expr;
     }
 
 } // namespace cobra
diff --git a/lib/core/SemilinearNormalizer.cpp b/lib/core/SemilinearNormalizer.cpp
index e324529..9cd6937 100644
--- a/lib/core/SemilinearNormalizer.cpp
+++ b/lib/core/SemilinearNormalizer.cpp
@@ -203,7 +203,7 @@ namespace cobra {
             // identical Boolean truth tables but differ on full-width inputs
             // because variables evaluate to {0,1} while constants keep their
             // full value.
-            const bool kPure = !HasConstant(expr) && !ContainsShr(expr);
+            const bool kPure = !HasConstant(expr) && !ContainsType(expr, Expr::Kind::kShr);
             if (kPure && !kKey.truth_table.empty()) {
                 auto it = ctx.atom_map.find(kKey);
                 if (it != ctx.atom_map.end()) { return it->second; }
diff --git a/lib/core/SignatureEval.cpp b/lib/core/SignatureEval.cpp
index 253704c..f9d3c88 100644
--- a/lib/core/SignatureEval.cpp
+++ b/lib/core/SignatureEval.cpp
@@ -17,38 +17,62 @@ namespace cobra {
 
     namespace {
 
-        // Bottom-up evaluation: walk the expression tree once,
-        // computing all 2^n outputs per node instead of calling
-        // eval_expr 2^n times. Complexity: O(tree_size * 2^n)
-        // element-wise ops in a single tree walk, vs O(tree_size)
-        // recursive calls * 2^n invocations in the naive approach.
-        // The key win is eliminating function call/dispatch overhead.
+        // Reusable per-node buffers for EvalSigRecursive. Each node produces a
+        // length-2^n result; binary nodes free their right child's buffer back
+        // here so leaf acquisitions recycle it. This bounds live buffers (and
+        // thus allocations) to ~tree depth instead of one per leaf.
+        struct SigBufferPool
+        {
+            size_t len = 0;
+            std::vector< std::vector< uint64_t > > free;
+
+            std::vector< uint64_t > Acquire() {
+                if (!free.empty()) {
+                    std::vector< uint64_t > buf = std::move(free.back());
+                    free.pop_back();
+                    buf.resize(len); // no-op: every pooled buffer is already len
+                    return buf;
+                }
+                return std::vector< uint64_t >(len);
+            }
+
+            void Release(std::vector< uint64_t > &&buf) { free.push_back(std::move(buf)); }
+        };
+
+        // Bottom-up evaluation: walk the expression tree once, computing all
+        // 2^n outputs per node instead of calling eval_expr 2^n times.
+        // Complexity: O(tree_size * 2^n) element-wise ops in a single tree
+        // walk. Per-node result buffers are recycled through `pool` so the
+        // 2^n vectors are not malloc'd once per leaf.
         std::vector< uint64_t >
-        EvalSigRecursive(const Expr &expr, size_t len, uint32_t bitwidth) {
+        EvalSigRecursive(const Expr &expr, SigBufferPool &pool, uint32_t bitwidth) {
             const uint64_t kMask = Bitmask(bitwidth);
+            const size_t len     = pool.len;
 
             switch (expr.kind) {
                 case Expr::Kind::kConstant: {
-                    return std::vector< uint64_t >(len, expr.constant_val & kMask);
+                    auto r = pool.Acquire();
+                    std::fill(r.begin(), r.end(), expr.constant_val & kMask);
+                    return r;
                 }
                 case Expr::Kind::kVariable: {
-                    std::vector< uint64_t > r(len);
+                    auto r              = pool.Acquire();
                     const uint32_t kIdx = expr.var_index;
                     for (size_t i = 0; i < len; ++i) { r[i] = (i >> kIdx) & 1; }
                     return r;
                 }
                 case Expr::Kind::kNot: {
-                    auto child = EvalSigRecursive(*expr.children[0], len, bitwidth);
+                    auto child = EvalSigRecursive(*expr.children[0], pool, bitwidth);
                     for (size_t i = 0; i < len; ++i) { child[i] = (~child[i]) & kMask; }
                     return child;
                 }
                 case Expr::Kind::kNeg: {
-                    auto child = EvalSigRecursive(*expr.children[0], len, bitwidth);
+                    auto child = EvalSigRecursive(*expr.children[0], pool, bitwidth);
                     for (size_t i = 0; i < len; ++i) { child[i] = (-child[i]) & kMask; }
                     return child;
                 }
                 case Expr::Kind::kShr: {
-                    auto child        = EvalSigRecursive(*expr.children[0], len, bitwidth);
+                    auto child        = EvalSigRecursive(*expr.children[0], pool, bitwidth);
                     const uint64_t kK = expr.constant_val;
                     if (kK >= 64) {
                         std::fill(child.begin(), child.end(), 0);
@@ -60,33 +84,38 @@ namespace cobra {
                     return child;
                 }
                 case Expr::Kind::kAdd: {
-                    auto left  = EvalSigRecursive(*expr.children[0], len, bitwidth);
-                    auto right = EvalSigRecursive(*expr.children[1], len, bitwidth);
+                    auto left  = EvalSigRecursive(*expr.children[0], pool, bitwidth);
+                    auto right = EvalSigRecursive(*expr.children[1], pool, bitwidth);
                     for (size_t i = 0; i < len; ++i) { left[i] = (left[i] + right[i]) & kMask; }
+                    pool.Release(std::move(right));
                     return left;
                 }
                 case Expr::Kind::kMul: {
-                    auto left  = EvalSigRecursive(*expr.children[0], len, bitwidth);
-                    auto right = EvalSigRecursive(*expr.children[1], len, bitwidth);
+                    auto left  = EvalSigRecursive(*expr.children[0], pool, bitwidth);
+                    auto right = EvalSigRecursive(*expr.children[1], pool, bitwidth);
                     for (size_t i = 0; i < len; ++i) { left[i] = (left[i] * right[i]) & kMask; }
+                    pool.Release(std::move(right));
                     return left;
                 }
                 case Expr::Kind::kAnd: {
-                    auto left  = EvalSigRecursive(*expr.children[0], len, bitwidth);
-                    auto right = EvalSigRecursive(*expr.children[1], len, bitwidth);
+                    auto left  = EvalSigRecursive(*expr.children[0], pool, bitwidth);
+                    auto right = EvalSigRecursive(*expr.children[1], pool, bitwidth);
                     for (size_t i = 0; i < len; ++i) { left[i] = left[i] & right[i]; }
+                    pool.Release(std::move(right));
                     return left;
                 }
                 case Expr::Kind::kOr: {
-                    auto left  = EvalSigRecursive(*expr.children[0], len, bitwidth);
-                    auto right = EvalSigRecursive(*expr.children[1], len, bitwidth);
+                    auto left  = EvalSigRecursive(*expr.children[0], pool, bitwidth);
+                    auto right = EvalSigRecursive(*expr.children[1], pool, bitwidth);
                     for (size_t i = 0; i < len; ++i) { left[i] = (left[i] | right[i]) & kMask; }
+                    pool.Release(std::move(right));
                     return left;
                 }
                 case Expr::Kind::kXor: {
-                    auto left  = EvalSigRecursive(*expr.children[0], len, bitwidth);
-                    auto right = EvalSigRecursive(*expr.children[1], len, bitwidth);
+                    auto left  = EvalSigRecursive(*expr.children[0], pool, bitwidth);
+                    auto right = EvalSigRecursive(*expr.children[1], pool, bitwidth);
                     for (size_t i = 0; i < len; ++i) { left[i] = (left[i] ^ right[i]) & kMask; }
+                    pool.Release(std::move(right));
                     return left;
                 }
             }
@@ -116,7 +145,8 @@ namespace cobra {
         auto t0 = std::chrono::high_resolution_clock::now();
 #endif
         const size_t kLen = size_t{ 1 } << num_vars;
-        auto result       = EvalSigRecursive(expr, kLen, bitwidth);
+        SigBufferPool pool{ .len = kLen, .free = {} };
+        auto result = EvalSigRecursive(expr, pool, bitwidth);
 #ifdef COBRA_SIG_STATS
         auto t1   = std::chrono::high_resolution_clock::now();
         double us = std::chrono::duration< double, std::micro >(t1 - t0).count();
diff --git a/lib/core/StructureRecovery.cpp b/lib/core/StructureRecovery.cpp
index 52a9200..05cfdf4 100644
--- a/lib/core/StructureRecovery.cpp
+++ b/lib/core/StructureRecovery.cpp
@@ -360,7 +360,9 @@ namespace cobra {
             // Only flatten single-variable atoms without shifts.
             // Shifts mix bits across positions, breaking the per-bit
             // decomposition f(x) = f(0) + (x & pass) - (x & invert).
-            if (info.key.support.size() != 1 || ContainsShr(*info.original_subtree)) {
+            if (info.key.support.size() != 1
+                || ContainsType(*info.original_subtree, Expr::Kind::kShr))
+            {
                 new_terms.push_back(term);
                 continue;
             }
diff --git a/lib/core/TemplateDecomposer.cpp b/lib/core/TemplateDecomposer.cpp
index f33117d..dd8772d 100644
--- a/lib/core/TemplateDecomposer.cpp
+++ b/lib/core/TemplateDecomposer.cpp
@@ -19,6 +19,7 @@
 #include <optional>
 #include <random>
 #include <span>
+#include <unordered_set>
 #include <utility>
 #include <vector>
 
@@ -1038,6 +1039,33 @@ namespace cobra {
         }
         COBRA_PLOT("TemplatePoolSize", static_cast< int64_t >(pool.size()));
 
+        // Seed data-derived constants so masking results like x & M (whose set
+        // bit is invisible to the {0,1} signature) become synthesizable. The
+        // OR-fold of observed outputs recovers the mask; a few distinct output
+        // values cover split masks. Soundness is unchanged: every candidate is
+        // FullWidthCheckEval-gated, so extra constants only widen the search.
+        {
+            uint64_t or_fold = 0;
+            for (size_t i = 0; i < kNProbes; ++i) { or_fold |= target[i]; }
+            // Skip values already seeded: Push dedups the pool by probe-vals, so
+            // re-seeding the same constant only wastes a Probe() call.
+            std::unordered_set< uint64_t > seeded_vals;
+            auto seed_const = [&](uint64_t c) {
+                if (c == 0 || !seeded_vals.insert(c).second) { return; }
+                auto e = Expr::Constant(c);
+                auto v = Probe(*e, pts, opts.bitwidth);
+                Push(pool, vmap, std::move(e), v);
+            };
+            seed_const(or_fold);
+            uint32_t seeded = 0;
+            for (size_t i = 0; i < kNProbes && seeded < 7; ++i) {
+                if (target[i] != 0) {
+                    seed_const(target[i]);
+                    ++seeded;
+                }
+            }
+        }
+
         // Direct atom match.
         {
             const auto *slot = vmap.find(target);
diff --git a/lib/core/WeightedPolyFit.cpp b/lib/core/WeightedPolyFit.cpp
index 3541f36..13c708c 100644
--- a/lib/core/WeightedPolyFit.cpp
+++ b/lib/core/WeightedPolyFit.cpp
@@ -166,6 +166,20 @@ namespace cobra {
             std::vector< uint64_t > full_point(total_num_vars, 0);
             std::vector< uint64_t > local_point(kK, 0);
 
+            // Precompute falling factorials over the grid. The matrix build
+            // below would otherwise recompute FallingFactorial(coord, exp) once
+            // per (row, col, dim) for only kGridBase x (kPerVarCap+1) distinct
+            // (coord, exp) pairs.
+            std::vector< std::vector< uint64_t > > falling(
+                kGridBase, std::vector< uint64_t >(static_cast< size_t >(kPerVarCap) + 1, 0)
+            );
+            for (size_t coord = 0; coord < kGridBase; ++coord) {
+                for (uint32_t e = 0; e <= kPerVarCap; ++e) {
+                    falling[coord][e] =
+                        FallingFactorial(coord, static_cast< uint8_t >(e), kMask);
+                }
+            }
+
             for (size_t row = 0; row < num_rows; ++row) {
                 size_t tmp = row;
                 for (uint32_t i = 0; i < kK; ++i) {
@@ -178,9 +192,7 @@ namespace cobra {
                 for (size_t col = 0; col < kNumCols; ++col) {
                     uint64_t phi = 1;
                     for (uint32_t i = 0; i < kK; ++i) {
-                        phi =
-                            (phi * FallingFactorial(local_point[i], basis_exps[col][i], kMask))
-                            & kMask;
+                        phi = (phi * falling[local_point[i]][basis_exps[col][i]]) & kMask;
                     }
                     mat[row][col] = (kWVal * phi) & kMask;
                 }
diff --git a/test/bench/bench_mask_audit.cpp b/test/bench/bench_mask_audit.cpp
index 0e6c6e1..327bd36 100644
--- a/test/bench/bench_mask_audit.cpp
+++ b/test/bench/bench_mask_audit.cpp
@@ -101,7 +101,7 @@ namespace {
             MaskAuditResult r;
             r.line       = lineno;
             r.node_count = CountNodes(expr);
-            r.has_shr    = ContainsShr(expr);
+            r.has_shr    = ContainsType(expr, Expr::Kind::kShr);
 
             // Root mask
             auto root_mask    = DetectRootLowBitMask(expr, 64);
diff --git a/test/core/test_coeff_interpolator.cpp b/test/core/test_coeff_interpolator.cpp
index e1fa802..7bb82bb 100644
--- a/test/core/test_coeff_interpolator.cpp
+++ b/test/core/test_coeff_interpolator.cpp
@@ -221,6 +221,45 @@ TEST(CoeffInterpolatorTest, AllZeroSig) {
     // Interaction terms are zero — affine result
 }
 
+// Property: the butterfly equals the naive subset Mobius transform,
+//   coeff[i] = sum_{j subset of i} (-1)^(popcount(i)-popcount(j)) * sig[j],
+// across random signatures, variable counts, and bitwidths.
+TEST(CoeffInterpolatorTest, MatchesNaiveMobius) {
+    uint64_t state = 0xC0B7A1234ULL;
+    auto next      = [&state]() {
+        state      += 0x9E3779B97F4A7C15ULL;
+        uint64_t z  = state;
+        z           = (z ^ (z >> 30)) * 0xBF58476D1CE4E5B9ULL;
+        z           = (z ^ (z >> 27)) * 0x94D049BB133111EBULL;
+        return z ^ (z >> 31);
+    };
+    for (uint32_t num_vars : { 0u, 1u, 2u, 3u, 4u, 5u, 6u }) {
+        for (uint32_t bitwidth : { 1u, 8u, 16u, 32u, 64u }) {
+            const uint64_t mask = Bitmask(bitwidth);
+            const size_t len    = size_t{ 1 } << num_vars;
+            std::vector< uint64_t > sig(len);
+            for (auto &s : sig) { s = next() & mask; }
+
+            std::vector< uint64_t > expected(len, 0);
+            for (size_t i = 0; i < len; ++i) {
+                // Enumerate submasks j of i; sign by parity of |i| - |j|.
+                for (size_t j = i;; j = (j - 1) & i) {
+                    uint64_t term = sig[j] & mask;
+                    if (((std::popcount(i) - std::popcount(j)) & 1) != 0) {
+                        term = (0 - term) & mask;
+                    }
+                    expected[i] = (expected[i] + term) & mask;
+                    if (j == 0) { break; }
+                }
+            }
+
+            auto got = InterpolateCoefficients(sig, num_vars, bitwidth);
+            EXPECT_EQ(got, expected)
+                << "num_vars=" << num_vars << " bitwidth=" << bitwidth;
+        }
+    }
+}
+
 // Large constant with wrapping at 8-bit
 TEST(CoeffInterpolatorTest, Bitwidth8LargeCoeffs) {
     // 200*x + 100*y at 8-bit: sig = [0, 200, 100, 44]
diff --git a/test/core/test_dynamic_mask.cpp b/test/core/test_dynamic_mask.cpp
index e20c5f3..bb75ade 100644
--- a/test/core/test_dynamic_mask.cpp
+++ b/test/core/test_dynamic_mask.cpp
@@ -64,20 +64,20 @@ TEST(DynamicMaskTest, DetectRootLowBitMask_NotAndNode) {
     EXPECT_FALSE(mask.has_value());
 }
 
-TEST(DynamicMaskTest, ContainsShr_False) {
+TEST(DynamicMaskTest, ContainsTypeShrFalse) {
     auto expr = Expr::Add(
         Expr::BitwiseAnd(Expr::Variable(0), Expr::Variable(1)),
         Expr::BitwiseNot(Expr::Variable(0))
     );
-    EXPECT_FALSE(ContainsShr(*expr));
+    EXPECT_FALSE(ContainsType(*expr, Expr::Kind::kShr));
 }
 
-TEST(DynamicMaskTest, ContainsShr_True) {
+TEST(DynamicMaskTest, ContainsTypeShrTrue) {
     auto expr = Expr::Add(Expr::LogicalShr(Expr::Variable(0), 3), Expr::Variable(1));
-    EXPECT_TRUE(ContainsShr(*expr));
+    EXPECT_TRUE(ContainsType(*expr, Expr::Kind::kShr));
 }
 
-TEST(DynamicMaskTest, ContainsShr_Deep) {
+TEST(DynamicMaskTest, ContainsTypeShrDeep) {
     auto expr = Expr::BitwiseAnd(
         Expr::Add(
             Expr::Variable(0),
@@ -85,5 +85,31 @@ TEST(DynamicMaskTest, ContainsShr_Deep) {
         ),
         Expr::Constant(0xFF)
     );
-    EXPECT_TRUE(ContainsShr(*expr));
+    EXPECT_TRUE(ContainsType(*expr, Expr::Kind::kShr));
+}
+
+TEST(DynamicMaskTest, ContainsTypeXorFalse) {
+    auto expr = Expr::Add(
+        Expr::BitwiseAnd(Expr::Variable(0), Expr::Variable(1)),
+        Expr::BitwiseOr(Expr::Variable(0), Expr::Constant(3))
+    );
+    EXPECT_FALSE(ContainsType(*expr, Expr::Kind::kXor));
+}
+
+TEST(DynamicMaskTest, ContainsTypeXorTrue) {
+    auto expr = Expr::BitwiseXor(Expr::Variable(0), Expr::Variable(1));
+    EXPECT_TRUE(ContainsType(*expr, Expr::Kind::kXor));
+}
+
+TEST(DynamicMaskTest, ContainsTypeXorDeep) {
+    auto expr = Expr::BitwiseAnd(
+        Expr::Add(
+            Expr::Variable(0),
+            Expr::BitwiseOr(
+                Expr::Variable(1), Expr::BitwiseXor(Expr::Variable(0), Expr::Variable(2))
+            )
+        ),
+        Expr::Constant(0xFF)
+    );
+    EXPECT_TRUE(ContainsType(*expr, Expr::Kind::kXor));
 }
diff --git a/test/core/test_expr_cost.cpp b/test/core/test_expr_cost.cpp
index 47227bb..3dccecb 100644
--- a/test/core/test_expr_cost.cpp
+++ b/test/core/test_expr_cost.cpp
@@ -100,3 +100,41 @@ TEST(ExprCostTest, IsBetterEqual) {
     ExprCost a{ 5, 1, 3 };
     EXPECT_FALSE(IsBetter(a, a));
 }
+
+TEST(ExprCostTest, IsCostBlowupExponentialExpansion) {
+    // 100 weighted vs 10: > 2x AND > 32 absolute -> blow-up.
+    ExprCost candidate{ 100, 0, 5 };
+    ExprCost baseline{ 10, 0, 3 };
+    EXPECT_TRUE(IsCostBlowup(candidate, baseline));
+}
+
+TEST(ExprCostTest, IsCostBlowupSparedByRatio) {
+    // 30 vs 20: not more than 2x (would need > 40), so not a blow-up
+    // even though it exceeds the absolute floor.
+    ExprCost candidate{ 30, 0, 4 };
+    ExprCost baseline{ 20, 0, 4 };
+    EXPECT_FALSE(IsCostBlowup(candidate, baseline));
+}
+
+TEST(ExprCostTest, IsCostBlowupSparedBySmallAbsoluteFloor) {
+    // 15 vs 7: more than 2x, but below the absolute floor (32). This is
+    // the legitimate NOT-over-arith canonicalization that must be kept.
+    ExprCost candidate{ 15, 0, 4 };
+    ExprCost baseline{ 7, 0, 3 };
+    EXPECT_FALSE(IsCostBlowup(candidate, baseline));
+}
+
+TEST(ExprCostTest, IsCostBlowupBoundary) {
+    // Exactly at both thresholds is NOT a blow-up (strict greater-than);
+    // one past both is.
+    EXPECT_FALSE(IsCostBlowup(ExprCost{ 32, 0, 1 }, ExprCost{ 16, 0, 1 }));
+    EXPECT_TRUE(IsCostBlowup(ExprCost{ 33, 0, 1 }, ExprCost{ 16, 0, 1 }));
+}
+
+TEST(ExprCostTest, IsCostBlowupKeysOnSizeNotMulOrDepth) {
+    // The gate axis is weighted_size only: a candidate that is smaller in
+    // size is never a blow-up regardless of mul-count or depth.
+    ExprCost candidate{ 10, 50, 50 };
+    ExprCost baseline{ 100, 0, 1 };
+    EXPECT_FALSE(IsCostBlowup(candidate, baseline));
+}
diff --git a/test/core/test_math_utils.cpp b/test/core/test_math_utils.cpp
index 0c5a6ec..715c130 100644
--- a/test/core/test_math_utils.cpp
+++ b/test/core/test_math_utils.cpp
@@ -98,3 +98,29 @@ TEST(ModInverseOddTest, SingleBit) {
     EXPECT_EQ(ModInverseOdd(1, 1), 1u);
     EXPECT_EQ(ModInverseOdd(3, 1), 1u); // 3 & 1 == 1
 }
+
+// Exhaustive: every odd residue is its own inverse's partner mod 2^bits, and
+// the result is reduced to [0, 2^bits). Covers the (3x)^2 seed at small widths
+// where the doubling loop runs 0-2 times.
+TEST(ModInverseOddTest, ExhaustiveSmallWidths) {
+    for (uint32_t bits : { 1u, 2u, 3u, 4u, 5u, 6u, 7u, 8u, 12u, 16u }) {
+        uint64_t mask = Bitmask(bits);
+        for (uint64_t x = 1; x <= mask; x += 2) {
+            uint64_t inv = ModInverseOdd(x, bits);
+            EXPECT_EQ((x * inv) & mask, 1u) << "bits=" << bits << " x=" << x;
+            EXPECT_EQ(inv & mask, inv) << "bits=" << bits << " x=" << x;
+        }
+    }
+}
+
+TEST(ModInverseOddTest, Random64Bit) {
+    uint64_t state = 0x123456789abcdef0ULL;
+    for (int i = 0; i < 100000; ++i) {
+        state      += 0x9E3779B97F4A7C15ULL;
+        uint64_t z  = state;
+        z           = (z ^ (z >> 30)) * 0xBF58476D1CE4E5B9ULL;
+        z           = (z ^ (z >> 27)) * 0x94D049BB133111EBULL;
+        uint64_t x  = (z ^ (z >> 31)) | 1ULL;
+        EXPECT_EQ(x * ModInverseOdd(x, 64), 1u) << "x=" << x;
+    }
+}
diff --git a/test/core/test_pattern_matcher.cpp b/test/core/test_pattern_matcher.cpp
index 7dd7cd4..9f8a785 100644
--- a/test/core/test_pattern_matcher.cpp
+++ b/test/core/test_pattern_matcher.cpp
@@ -741,3 +741,108 @@ TEST(PatternMatcherTest, FiveVarSampledCorrectness) {
         verify(rng);
     }
 }
+
+namespace {
+    bool ContainsKind(const Expr &e, Expr::Kind k) {
+        if (e.kind == k) { return true; }
+        for (const auto &c : e.children) {
+            if (ContainsKind(*c, k)) { return true; }
+        }
+        return false;
+    }
+} // namespace
+
+// Inclusion-exclusion OR recovery (GAMBA recon): A + B - (A & B) -> A | B,
+// where B is arithmetic (10*y+5) and operands are spread across a flattened
+// additive sum. Target: 10*y + 5 + x + (x^4) - ((x^4) & (10*y+5)) == x + ((x^4) | (10*y+5)).
+TEST(PatternMatcherTest, RecoverDisjunctionArithmeticOperand) {
+    auto x = []() { return Expr::Variable(0); };
+    auto y = []() { return Expr::Variable(1); };
+    auto a = [&]() { return Expr::BitwiseXor(x(), Expr::Constant(4)); };
+    auto b = [&]() { return Expr::Add(Expr::Mul(Expr::Constant(10), y()), Expr::Constant(5)); };
+    auto input = Expr::Add(
+        Expr::Add(Expr::Add(b(), x()), a()), Expr::Negate(Expr::BitwiseAnd(a(), b()))
+    );
+
+    auto original = CloneExpr(*input);
+    auto result   = SimplifyPatternSubtrees(std::move(input), 64);
+
+    EXPECT_TRUE(ContainsKind(*result, Expr::Kind::kOr));
+    EXPECT_TRUE(FullWidthCheck(*original, 2, *result, {}, 64).passed);
+    EXPECT_TRUE(IsBetter(ComputeCost(*result).cost, ComputeCost(*original).cost));
+}
+
+// Simpler 2-var instance of the same gap: (x^4) + y - ((x^4) & y) -> (x^4) | y.
+TEST(PatternMatcherTest, RecoverDisjunctionTwoVar) {
+    auto x     = []() { return Expr::Variable(0); };
+    auto y     = []() { return Expr::Variable(1); };
+    auto a     = [&]() { return Expr::BitwiseXor(x(), Expr::Constant(4)); };
+    auto input = Expr::Add(Expr::Add(a(), y()), Expr::Negate(Expr::BitwiseAnd(a(), y())));
+
+    auto original = CloneExpr(*input);
+    auto result   = SimplifyPatternSubtrees(std::move(input), 64);
+
+    EXPECT_TRUE(ContainsKind(*result, Expr::Kind::kOr));
+    EXPECT_TRUE(FullWidthCheck(*original, 2, *result, {}, 64).passed);
+}
+
+// Regression guard: XOR lowering A + B - 2*(A & B) must stay A ^ B and must
+// NOT be misrecovered as A | B (coefficient on the AND term is 2, not 1).
+TEST(PatternMatcherTest, RecoverDisjunctionDoesNotMisfireOnXor) {
+    auto x     = []() { return Expr::Variable(0); };
+    auto y     = []() { return Expr::Variable(1); };
+    auto input = Expr::Add(
+        Expr::Add(x(), y()),
+        Expr::Negate(Expr::Mul(Expr::Constant(2), Expr::BitwiseAnd(x(), y())))
+    );
+
+    auto original = CloneExpr(*input);
+    auto result   = SimplifyPatternSubtrees(std::move(input), 64);
+
+    EXPECT_FALSE(ContainsKind(*result, Expr::Kind::kOr));
+    EXPECT_TRUE(FullWidthCheck(*original, 2, *result, {}, 64).passed);
+}
+
+// Structural XOR self-cancellation: (A ^ B) ^ B -> A, even when A has a
+// degenerate {0,1} signature (so the signature path can't recover it).
+// A = ((x+y)&z)|3 (constant 3 on {0,1}); B = (x*z | y&85) + w (appears twice).
+TEST(PatternMatcherTest, XorSelfCancelComplexOperand) {
+    auto a = []() {
+        return Expr::BitwiseOr(
+            Expr::BitwiseAnd(
+                Expr::Add(Expr::Variable(0), Expr::Variable(1)), Expr::Variable(2)
+            ),
+            Expr::Constant(3)
+        );
+    };
+    auto b = []() {
+        return Expr::Add(
+            Expr::BitwiseOr(
+                Expr::Mul(Expr::Variable(0), Expr::Variable(2)),
+                Expr::BitwiseAnd(Expr::Variable(1), Expr::Constant(85))
+            ),
+            Expr::Variable(3)
+        );
+    };
+    auto input = Expr::BitwiseXor(Expr::BitwiseXor(a(), b()), b());
+
+    auto original = CloneExpr(*input);
+    auto result   = SimplifyXorChains(std::move(input), 64);
+
+    // B ^ B cancels; no XOR should remain, and the result equals A.
+    EXPECT_FALSE(ContainsKind(*result, Expr::Kind::kXor));
+    EXPECT_TRUE(FullWidthCheck(*original, 4, *result, {}, 64).passed);
+    EXPECT_TRUE(IsBetter(ComputeCost(*result).cost, ComputeCost(*original).cost));
+}
+
+// Odd multiplicity: T ^ T ^ T -> T (a single copy survives).
+TEST(PatternMatcherTest, XorSelfCancelOddMultiplicity) {
+    auto t        = []() { return Expr::BitwiseAnd(Expr::Variable(0), Expr::Variable(1)); };
+    auto input    = Expr::BitwiseXor(Expr::BitwiseXor(t(), t()), t());
+    auto original = CloneExpr(*input);
+    auto result   = SimplifyXorChains(std::move(input), 64);
+
+    EXPECT_FALSE(ContainsKind(*result, Expr::Kind::kXor));
+    EXPECT_EQ(result->kind, Expr::Kind::kAnd);
+    EXPECT_TRUE(FullWidthCheck(*original, 2, *result, {}, 64).passed);
+}
diff --git a/test/core/test_simplifier.cpp b/test/core/test_simplifier.cpp
index 4736e4e..50ad1e5 100644
--- a/test/core/test_simplifier.cpp
+++ b/test/core/test_simplifier.cpp
@@ -1122,7 +1122,7 @@ TEST(SimplifierTest, RepairProductShadow_CompoundChildSkipped) {
 // --- Dynamic masking fallback tests ---
 
 TEST(SimplifierTest, DynamicMask_ShrRejectsOptimization) {
-    // 0xFF & (x >> 1): ContainsShr rejects dynamic masking,
+    // 0xFF & (x >> 1): the shift check rejects dynamic masking,
     // falls through to normal pipeline.
     auto inner  = Expr::LogicalShr(Expr::Variable(0), 1);
     auto masked = Expr::BitwiseAnd(Expr::Constant(0xFF), std::move(inner));
@@ -1893,7 +1893,7 @@ TEST(SimplifierTest, RejectsExcessiveInputVarCount) {
     // any allocation.
     std::vector< std::string > vars;
     for (int i = 0; i < 25; ++i) { vars.push_back("x" + std::to_string(i)); }
-    std::vector< uint64_t > sig(2, 0);  // size doesn't matter; rejected first
+    std::vector< uint64_t > sig(2, 0); // size doesn't matter; rejected first
     Options opts{ .bitwidth = 64, .max_vars = 16, .spot_check = false };
 
     auto result = Simplify(sig, vars, nullptr, opts);
@@ -1955,3 +1955,191 @@ TEST(SimplifierTest, AcceptsInputVarCountAtCeiling) {
     ASSERT_TRUE(result.has_value());
     EXPECT_EQ(Render(*result.value().expr, result.value().real_vars), "7");
 }
+
+namespace {
+    // s(v) = 1 - 2*(v & 1), a +-1 value (s^2 == 1). GAMBA parity sign-flip.
+    std::unique_ptr< Expr > SignFlip(uint32_t var_index) {
+        return Expr::Add(
+            Expr::Constant(1),
+            Expr::Mul(
+                Expr::BitwiseAnd(Expr::Variable(var_index), Expr::Constant(1)),
+                Expr::Constant(static_cast< uint64_t >(-2))
+            )
+        );
+    }
+
+    bool RendersToSum(const SimplifyOutcome &out, const char *a, const char *b) {
+        auto text = Render(*out.expr, out.real_vars);
+        return text == std::string(a) + " + " + b || text == std::string(b) + " + " + a;
+    }
+} // namespace
+
+// GAMBA recon: parity sign-square E*s*s -> E for multi-variable E. The
+// degenerate single-product core (the whole input) used to short-circuit the
+// worklist before the recovery passes ran, leaving the input unchanged.
+TEST(SimplifierTest, SignSquareCollapseMultiVar) {
+    // (x1 + x2) * s(x3) * s(x3)  ==  x1 + x2
+    auto ast = Expr::Mul(
+        Expr::Mul(Expr::Add(Expr::Variable(0), Expr::Variable(1)), SignFlip(2)), SignFlip(2)
+    );
+    std::vector< std::string > vars = { "x1", "x2", "x3" };
+
+    auto sig = EvaluateBooleanSignature(*ast, 3, 64);
+    Options opts{ .bitwidth = 64, .max_vars = 16, .spot_check = true };
+    opts.evaluator = Evaluator::FromExpr(*ast, 64);
+
+    auto result = Simplify(sig, vars, ast.get(), opts);
+    ASSERT_TRUE(result.has_value());
+    EXPECT_EQ(result->kind, SimplifyOutcome::Kind::kSimplified);
+    EXPECT_TRUE(RendersToSum(result.value(), "x1", "x2"));
+    auto check = FullWidthCheckEval(Evaluator::FromExpr(*ast, 64), 3, *result->expr, 64);
+    EXPECT_TRUE(check.passed);
+}
+
+// Full Arnau target: XOR self-cancel of duplicate complex operands plus the
+// sign-square collapse must together reduce to x1 + x2.
+TEST(SimplifierTest, SignSquareWithXorSelfCancel) {
+    // ((((x1+x2)*s3) ^ ((x5+3)*s4) ^ ((x5+3)*s4)) * s3)  ==  x1 + x2
+    auto term_a = Expr::Mul(Expr::Add(Expr::Variable(0), Expr::Variable(1)), SignFlip(2));
+    auto term_b = [&]() {
+        return Expr::Mul(Expr::Add(Expr::Variable(4), Expr::Constant(3)), SignFlip(3));
+    };
+    auto inner = Expr::BitwiseXor(Expr::BitwiseXor(std::move(term_a), term_b()), term_b());
+    auto ast   = Expr::Mul(std::move(inner), SignFlip(2));
+    std::vector< std::string > vars = { "x1", "x2", "x3", "x4", "x5" };
+
+    auto sig = EvaluateBooleanSignature(*ast, 5, 64);
+    Options opts{ .bitwidth = 64, .max_vars = 16, .spot_check = true };
+    opts.evaluator = Evaluator::FromExpr(*ast, 64);
+
+    auto result = Simplify(sig, vars, ast.get(), opts);
+    ASSERT_TRUE(result.has_value());
+    EXPECT_EQ(result->kind, SimplifyOutcome::Kind::kSimplified);
+    EXPECT_TRUE(RendersToSum(result.value(), "x1", "x2"));
+    auto check = FullWidthCheckEval(Evaluator::FromExpr(*ast, 64), 5, *result->expr, 64);
+    EXPECT_TRUE(check.passed);
+}
+
+namespace {
+    bool RendersToAndConst(const SimplifyOutcome &out, const char *v, uint64_t c) {
+        auto text = Render(*out.expr, out.real_vars);
+        auto cs   = std::to_string(c);
+        return text == std::string(v) + " & " + cs || text == cs + " & " + std::string(v);
+    }
+
+    // ((x & m) + (y & ymask)) & outmask
+    std::unique_ptr< Expr > MaskedAdd(uint64_t m, uint64_t ymask, uint64_t outmask) {
+        return Expr::BitwiseAnd(
+            Expr::Add(
+                Expr::BitwiseAnd(Expr::Variable(0), Expr::Constant(m)),
+                Expr::BitwiseAnd(Expr::Variable(1), Expr::Constant(ymask))
+            ),
+            Expr::Constant(outmask)
+        );
+    }
+
+    SimplifyOutcome RunAst(const Expr &ast, std::vector< std::string > vars) {
+        auto nv  = static_cast< uint32_t >(vars.size());
+        auto sig = EvaluateBooleanSignature(ast, nv, 64);
+        Options opts{ .bitwidth = 64, .max_vars = 16, .spot_check = true };
+        opts.evaluator = Evaluator::FromExpr(ast, 64);
+        auto result    = Simplify(sig, vars, &ast, opts);
+        return std::move(result.value());
+    }
+} // namespace
+
+// GAMBA recon: carry-free masked addition. ((x & 128) + (y & 127)) & 128 == x & 128
+// because y&127 < 128 is disjoint from bit 7, so the add can't carry into it. The
+// {0,1} signature is all-zero (bit 7 invisible); recovered once TemplateDecomposer
+// can synthesize the mask constant 128.
+TEST(SimplifierTest, MaskedCarryFreeAddBit7) {
+    auto ast = MaskedAdd(128, 127, 128);
+    auto out = RunAst(*ast, { "x", "y" });
+    EXPECT_EQ(out.kind, SimplifyOutcome::Kind::kSimplified);
+    EXPECT_TRUE(RendersToAndConst(out, "x", 128));
+    EXPECT_TRUE(FullWidthCheckEval(Evaluator::FromExpr(*ast, 64), 2, *out.expr, 64).passed);
+}
+
+// Whole family across the former bit>=3 threshold: ((x&2^k)+(y&(2^k-1)))&2^k -> x&2^k.
+TEST(SimplifierTest, MaskedCarryFreeAddFamily) {
+    for (uint32_t bit : { 3u, 4u, 5u, 6u, 7u, 8u }) {
+        const uint64_t m = uint64_t{ 1 } << bit;
+        auto ast         = MaskedAdd(m, m - 1, m);
+        auto out         = RunAst(*ast, { "x", "y" });
+        EXPECT_EQ(out.kind, SimplifyOutcome::Kind::kSimplified) << "bit " << bit;
+        EXPECT_TRUE(RendersToAndConst(out, "x", m)) << "bit " << bit;
+        EXPECT_TRUE(FullWidthCheckEval(Evaluator::FromExpr(*ast, 64), 2, *out.expr, 64).passed)
+            << "bit " << bit;
+    }
+}
+
+// End-to-end XOR self-cancel: (A ^ B) ^ B -> A through the full Simplify pipeline,
+// where A = ((x+y)&z)|3 (degenerate {0,1} signature) and B = (x*z | y&85) + w.
+TEST(SimplifierTest, XorSelfCancelEndToEnd) {
+    auto a = []() {
+        return Expr::BitwiseOr(
+            Expr::BitwiseAnd(
+                Expr::Add(Expr::Variable(0), Expr::Variable(1)), Expr::Variable(2)
+            ),
+            Expr::Constant(3)
+        );
+    };
+    auto b = []() {
+        return Expr::Add(
+            Expr::BitwiseOr(
+                Expr::Mul(Expr::Variable(0), Expr::Variable(2)),
+                Expr::BitwiseAnd(Expr::Variable(1), Expr::Constant(85))
+            ),
+            Expr::Variable(3)
+        );
+    };
+    auto ast = Expr::BitwiseXor(Expr::BitwiseXor(a(), b()), b());
+    auto out = RunAst(*ast, { "x", "y", "z", "w" });
+    EXPECT_EQ(out.kind, SimplifyOutcome::Kind::kSimplified);
+    // B ^ B cancels -> no XOR remains in the rendered result.
+    EXPECT_EQ(Render(*out.expr, out.real_vars).find('^'), std::string::npos);
+    EXPECT_TRUE(FullWidthCheckEval(Evaluator::FromExpr(*ast, 64), 4, *out.expr, 64).passed);
+    // The exact-XOR-cancel success must not carry the exhaustion failure
+    // lineage that the fallback path was built atop.
+    EXPECT_FALSE(out.diag.reason_code.has_value());
+    EXPECT_TRUE(out.diag.cause_chain.empty());
+}
+
+// Soundness: a genuine carry ((x & 255) + (y & 255)) & 255 must NOT collapse to
+// x & 255 (it is (x + y) & 255). Whatever is returned must stay full-width-correct.
+TEST(SimplifierTest, MaskedAddWithCarryNotFalselyCollapsed) {
+    auto ast = MaskedAdd(255, 255, 255);
+    auto out = RunAst(*ast, { "x", "y" });
+    EXPECT_TRUE(FullWidthCheckEval(Evaluator::FromExpr(*ast, 64), 2, *out.expr, 64).passed);
+    EXPECT_FALSE(RendersToAndConst(out, "x", 255));
+}
+
+// A change-of-basis blow-up must be rejected. sum(xi) - xor(xi) is CoB-linear,
+// so change-of-basis recovers an exponential AND-basis expansion; the input is
+// already minimal, so the cost gate keeps the input and reports kCostRejected.
+TEST(SimplifierTest, RejectsExponentialBlowup) {
+    auto sum = Expr::Variable(0);
+    auto xr  = Expr::Variable(0);
+    for (uint32_t i = 1; i < 8; ++i) {
+        sum = Expr::Add(std::move(sum), Expr::Variable(i));
+        xr  = Expr::BitwiseXor(std::move(xr), Expr::Variable(i));
+    }
+    auto ast = Expr::Add(std::move(sum), Expr::Negate(std::move(xr)));
+    std::vector< std::string > vars;
+    for (uint32_t i = 0; i < 8; ++i) { vars.push_back("x" + std::to_string(i)); }
+
+    auto input_cost = ComputeCost(*ast).cost;
+    auto sig        = EvaluateBooleanSignature(*ast, 8, 64);
+    Options opts{ .bitwidth = 64, .max_vars = 16, .spot_check = true };
+    opts.evaluator = Evaluator::FromExpr(*ast, 64);
+    auto result    = Simplify(sig, vars, ast.get(), opts);
+    ASSERT_TRUE(result.has_value());
+    // The blow-up is rejected: the input is kept unchanged...
+    EXPECT_EQ(result->kind, SimplifyOutcome::Kind::kUnchangedUnsupported);
+    EXPECT_TRUE(ExprStructurallyEqual(*result->expr, *ast));
+    // ...and the result must not be strictly more expensive than the input.
+    EXPECT_FALSE(IsBetter(input_cost, ComputeCost(*result->expr).cost));
+    // ...with a kCostRejected structured reason.
+    ASSERT_TRUE(result->diag.reason_code.has_value());
+    EXPECT_EQ(result->diag.reason_code->category, ReasonCategory::kCostRejected);
+}
diff --git a/test/verify/test_dataset_benchmarks.cpp b/test/verify/test_dataset_benchmarks.cpp
index 660d279..3fda5e5 100644
--- a/test/verify/test_dataset_benchmarks.cpp
+++ b/test/verify/test_dataset_benchmarks.cpp
@@ -358,15 +358,18 @@ TEST(GAMBADataset, QSynthEA) {
     EXPECT_EQ(stats.total, 503);
     EXPECT_EQ(stats.skipped_parse, 3);
     EXPECT_EQ(stats.parsed, 500);
-    EXPECT_EQ(stats.simplified, 466);
-    EXPECT_EQ(stats.unsupported, 34);
+    // +2 vs prior baseline: two cases with structurally-repeated XOR operands
+    // (one previously verify-failed, one search-exhausted) now collapse via the
+    // exact XOR self-cancellation exhaustion fallback (T^T==0).
+    EXPECT_EQ(stats.simplified, 468);
+    EXPECT_EQ(stats.unsupported, 32);
     EXPECT_EQ(stats.failed_simplify, 0);
 
     // Every unsupported result carries a structured reason code.
     EXPECT_EQ(stats.has_structured_reason, stats.unsupported);
-    EXPECT_EQ(stats.by_category[ReasonCategory::kVerifyFailed], 7);
+    EXPECT_EQ(stats.by_category[ReasonCategory::kVerifyFailed], 6);
     EXPECT_EQ(stats.by_category[ReasonCategory::kGuardFailed], 6);
-    EXPECT_EQ(stats.by_category[ReasonCategory::kSearchExhausted], 21);
+    EXPECT_EQ(stats.by_category[ReasonCategory::kSearchExhausted], 20);
 
     // Decomposition cause frames propagated into cause_chain.
     // MixedRewrite unsupported outcomes should carry delegated