diff --git a/crates/oxidd-core/src/lib.rs b/crates/oxidd-core/src/lib.rs
index 005f0de..f35f818 100644
--- a/crates/oxidd-core/src/lib.rs
+++ b/crates/oxidd-core/src/lib.rs
@@ -947,7 +947,25 @@ pub trait WorkerManager: Manager + Sync {
     /// Get the current number of threads
     fn current_num_threads(&self) -> usize;
 
-    /// Execute `op_a` and `op_b` in parallel
+    /// Get the recursion depth up to which operations are split
+    fn split_depth(&self) -> u32;
+
+    /// Set the recursion depth up to which operations are split
+    ///
+    /// `None` means that the implementation should automatically choose the
+    /// depth. `Some(0)` means that no operations are split.
+    fn set_split_depth(&self, depth: Option<u32>);
+
+    /// Execute `op` within the thread pool
+    ///
+    /// If this method is called from another thread pool, it may cooperatively
+    /// yield execution to that pool until `op` has finished.
+    fn install<R: Send>(&self, op: impl FnOnce() -> R + Send) -> R;
+
+    /// Execute `op_a` and `op_b` in parallel within the thread pool
+    ///
+    /// Note that the split depth has no influence on this method. Checking
+    /// whether to split an operation must be done externally.
     fn join<RA: Send, RB: Send>(
         &self,
         op_a: impl FnOnce() -> RA + Send,
diff --git a/crates/oxidd-manager-index/src/manager.rs b/crates/oxidd-manager-index/src/manager.rs
index d54ed80..5cc32c2 100644
--- a/crates/oxidd-manager-index/src/manager.rs
+++ b/crates/oxidd-manager-index/src/manager.rs
@@ -14,43 +14,30 @@
 //! | `RC`         | Diagram Rules Type Constructor    |
 //! | `OP`         | Operation                         |
 
-use std::cell::Cell;
-use std::cell::UnsafeCell;
+use std::cell::{Cell, UnsafeCell};
 use std::cmp::Ordering;
-use std::hash::Hash;
-use std::hash::Hasher;
+use std::hash::{Hash, Hasher};
 use std::iter::FusedIterator;
 use std::marker::PhantomData;
 use std::mem::ManuallyDrop;
+use std::sync::atomic::AtomicU32;
 use std::sync::atomic::Ordering::{Acquire, Relaxed};
 use std::sync::Arc;
 
 use bitvec::vec::BitVec;
 use crossbeam_utils::CachePadded;
 use linear_hashtbl::raw::RawTable;
-use oxidd_core::function::EdgeOfFunc;
-use oxidd_core::util::GCContainer;
-use parking_lot::Condvar;
-use parking_lot::Mutex;
-use parking_lot::MutexGuard;
-use parking_lot::RwLock;
+use parking_lot::{Condvar, Mutex, MutexGuard, RwLock};
 use rayon::ThreadPool;
 use rustc_hash::FxHasher;
 
-use oxidd_core::util::AbortOnDrop;
-use oxidd_core::util::AllocResult;
-use oxidd_core::util::Borrowed;
-use oxidd_core::util::DropWith;
-use oxidd_core::util::OutOfMemory;
-use oxidd_core::DiagramRules;
-use oxidd_core::InnerNode;
-use oxidd_core::LevelNo;
-use oxidd_core::Tag;
+use oxidd_core::function::EdgeOfFunc;
+use oxidd_core::util::{AbortOnDrop, AllocResult, Borrowed, DropWith, GCContainer, OutOfMemory};
+use oxidd_core::{DiagramRules, InnerNode, LevelNo, Tag};
 
 use crate::node::NodeBase;
 use crate::terminal_manager::TerminalManager;
-use crate::util::Invariant;
-use crate::util::TryLock;
+use crate::util::{Invariant, TryLock};
 
 // === Type Constructors =======================================================
 
@@ -285,6 +272,7 @@ where
     reorder_count: u64,
     gc_ongoing: TryLock,
     workers: ThreadPool,
+    split_depth: AtomicU32,
 }
 
 /// Type "constructor" for the manager from `InnerNodeCons` etc.
@@ -1088,6 +1076,15 @@ where
     }
 }
 
+fn auto_split_depth(workers: &rayon::ThreadPool) -> u32 {
+    let threads = workers.current_num_threads();
+    if threads > 1 {
+        (4096 * threads).ilog2()
+    } else {
+        0
+    }
+}
+
 impl<'id, N, ET, TM, R, MD, const TERMINALS: usize> oxidd_core::WorkerManager
     for Manager<'id, N, ET, TM, R, MD, TERMINALS>
 where
@@ -1102,6 +1099,24 @@ where
         self.workers.current_num_threads()
     }
 
+    #[inline(always)]
+    fn split_depth(&self) -> u32 {
+        self.split_depth.load(Relaxed)
+    }
+
+    fn set_split_depth(&self, depth: Option<u32>) {
+        let depth = match depth {
+            Some(d) => d,
+            None => auto_split_depth(&self.workers),
+        };
+        self.split_depth.store(depth, Relaxed);
+    }
+
+    #[inline]
+    fn install<RA: Send>(&self, op: impl FnOnce() -> RA + Send) -> RA {
+        self.workers.install(op)
+    }
+
     #[inline]
     fn join<RA: Send, RB: Send>(
         &self,
@@ -1112,10 +1127,10 @@ where
     }
 
     #[inline]
-    fn broadcast<RES: Send>(
+    fn broadcast<RA: Send>(
         &self,
-        op: impl Fn(oxidd_core::BroadcastContext) -> RES + Sync,
-    ) -> Vec<RES> {
+        op: impl Fn(oxidd_core::BroadcastContext) -> RA + Sync,
+    ) -> Vec<RA> {
         self.workers.broadcast(|ctx| {
             op(oxidd_core::BroadcastContext {
                 index: ctx.index() as u32,
@@ -2002,6 +2017,7 @@ pub fn new_manager<
         .thread_name(|i| format!("oxidd mi {i}")) // "mi" for "manager index"
         .build()
         .expect("could not build thread pool");
+    let split_depth = AtomicU32::new(auto_split_depth(&workers));
 
     let gc_lwm = inner_node_capacity / 100 * 90;
     let gc_hwm = inner_node_capacity / 100 * 95;
@@ -2027,6 +2043,7 @@ pub fn new_manager<
             reorder_count: 0,
             gc_ongoing: TryLock::new(),
             workers,
+            split_depth,
         }),
         terminal_manager: TMC::T::<'static>::with_capacity(terminal_node_capacity),
         gc_signal: (Mutex::new(GCSignal::RunGc), Condvar::new()),
diff --git a/crates/oxidd-manager-pointer/src/manager.rs b/crates/oxidd-manager-pointer/src/manager.rs
index 4ee71be..298f9da 100644
--- a/crates/oxidd-manager-pointer/src/manager.rs
+++ b/crates/oxidd-manager-pointer/src/manager.rs
@@ -16,49 +16,31 @@
 
 use std::cmp::Ordering;
 use std::collections::HashMap;
-use std::hash::BuildHasherDefault;
-use std::hash::Hash;
-use std::hash::Hasher;
+use std::hash::{BuildHasherDefault, Hash, Hasher};
 use std::iter::FusedIterator;
 use std::marker::PhantomData;
-use std::mem::align_of;
-use std::mem::ManuallyDrop;
-use std::mem::MaybeUninit;
-use std::ptr::addr_of;
-use std::ptr::addr_of_mut;
-use std::ptr::NonNull;
-
-use arcslab::ArcSlab;
-use arcslab::ArcSlabRef;
-use arcslab::AtomicRefCounted;
-use arcslab::ExtHandle;
-use arcslab::IntHandle;
+use std::mem::{align_of, ManuallyDrop, MaybeUninit};
+use std::ptr::{addr_of, addr_of_mut, NonNull};
+use std::sync::atomic::AtomicU32;
+use std::sync::atomic::Ordering::Relaxed;
+
+use arcslab::{ArcSlab, ArcSlabRef, AtomicRefCounted, ExtHandle, IntHandle};
 use bitvec::bitvec;
 use bitvec::vec::BitVec;
 use linear_hashtbl::raw::RawTable;
-use oxidd_core::util::GCContainer;
 use parking_lot::Mutex;
 use parking_lot::MutexGuard;
 use rustc_hash::FxHasher;
 
 use oxidd_core::function::EdgeOfFunc;
-use oxidd_core::util::AbortOnDrop;
-use oxidd_core::util::AllocResult;
-use oxidd_core::util::Borrowed;
-use oxidd_core::util::DropWith;
-use oxidd_core::DiagramRules;
-use oxidd_core::HasApplyCache;
-use oxidd_core::InnerNode;
-use oxidd_core::LevelNo;
-use oxidd_core::Node;
-use oxidd_core::Tag;
+use oxidd_core::util::{AbortOnDrop, AllocResult, Borrowed, DropWith, GCContainer};
+use oxidd_core::{DiagramRules, HasApplyCache, InnerNode, LevelNo, Node, Tag};
 
 use crate::node::NodeBase;
 use crate::terminal_manager::TerminalManager;
 use crate::util;
 use crate::util::rwlock::RwLock;
-use crate::util::Invariant;
-use crate::util::TryLock;
+use crate::util::{Invariant, TryLock};
 
 // === Type Constructors =======================================================
 
@@ -179,6 +161,7 @@ where
     gc_ongoing: TryLock,
     reorder_count: u64,
     workers: rayon::ThreadPool,
+    split_depth: AtomicU32,
     phantom: PhantomData<(TM, R)>,
 }
 
@@ -292,6 +275,7 @@ where
             .build()
             .expect("Failed to build thread pool");
 
+        let split_depth = AtomicU32::new(auto_split_depth(&workers));
         let data = RwLock::new(Manager {
             unique_table: Vec::new(),
             data: ManuallyDrop::new(data),
@@ -299,6 +283,7 @@ where
             gc_ongoing: TryLock::new(),
             reorder_count: 0,
             workers,
+            split_depth,
             phantom: PhantomData,
         });
         unsafe { std::ptr::write(addr_of_mut!((*slot).manager), data) };
@@ -777,6 +762,15 @@ where
     }
 }
 
+fn auto_split_depth(workers: &rayon::ThreadPool) -> u32 {
+    let threads = workers.current_num_threads();
+    if threads > 1 {
+        (4096 * threads).ilog2()
+    } else {
+        0
+    }
+}
+
 impl<'id, N, ET, TM, R, MD, const PAGE_SIZE: usize, const TAG_BITS: u32> oxidd_core::WorkerManager
     for Manager<'id, N, ET, TM, R, MD, PAGE_SIZE, TAG_BITS>
 where
@@ -786,10 +780,30 @@ where
     R: DiagramRules<Edge<'id, N, ET, TAG_BITS>, N, TM::TerminalNode>,
     MD: DropWith<Edge<'id, N, ET, TAG_BITS>> + GCContainer<Self> + Send + Sync,
 {
+    #[inline]
     fn current_num_threads(&self) -> usize {
         self.workers.current_num_threads()
     }
 
+    #[inline(always)]
+    fn split_depth(&self) -> u32 {
+        self.split_depth.load(Relaxed)
+    }
+
+    fn set_split_depth(&self, depth: Option<u32>) {
+        let depth = match depth {
+            Some(d) => d,
+            None => auto_split_depth(&self.workers),
+        };
+        self.split_depth.store(depth, Relaxed);
+    }
+
+    #[inline]
+    fn install<RA: Send>(&self, op: impl FnOnce() -> RA + Send) -> RA {
+        self.workers.install(op)
+    }
+
+    #[inline]
     fn join<RA: Send, RB: Send>(
         &self,
         op_a: impl FnOnce() -> RA + Send,
@@ -798,10 +812,10 @@ where
         self.workers.join(op_a, op_b)
     }
 
-    fn broadcast<RES: Send>(
+    fn broadcast<RA: Send>(
         &self,
-        op: impl Fn(oxidd_core::BroadcastContext) -> RES + Sync,
-    ) -> Vec<RES> {
+        op: impl Fn(oxidd_core::BroadcastContext) -> RA + Sync,
+    ) -> Vec<RA> {
         self.workers.broadcast(|ctx| {
             op(oxidd_core::BroadcastContext {
                 index: ctx.index() as u32,
diff --git a/crates/oxidd-rules-bdd/src/complement_edge/apply_rec.rs b/crates/oxidd-rules-bdd/src/complement_edge/apply_rec.rs
index 1789b71..d29e37e 100644
--- a/crates/oxidd-rules-bdd/src/complement_edge/apply_rec.rs
+++ b/crates/oxidd-rules-bdd/src/complement_edge/apply_rec.rs
@@ -1463,9 +1463,13 @@ pub mod mt {
                 Replacement = Borrowed<'a, EdgeOfFunc<'id, Self>>,
             >,
         ) -> AllocResult<EdgeOfFunc<'id, Self>> {
-            let rec = ParallelRecursor::new(manager);
             let subst = substitute_prepare(manager, substitution.pairs())?;
-            substitute(manager, rec, edge.borrowed(), &subst, substitution.id())
+            let edge = edge.borrowed();
+            let cache_id = substitution.id();
+            manager.install(move || {
+                let rec = ParallelRecursor::new(manager);
+                substitute(manager, rec, edge, &subst, cache_id)
+            })
         }
     }
 
@@ -1515,8 +1519,8 @@ pub mod mt {
             lhs: &EdgeOfFunc<'id, Self>,
             rhs: &EdgeOfFunc<'id, Self>,
         ) -> AllocResult<EdgeOfFunc<'id, Self>> {
-            let rec = ParallelRecursor::new(manager);
-            apply_and(manager, rec, lhs.borrowed(), rhs.borrowed())
+            let (lhs, rhs) = (lhs.borrowed(), rhs.borrowed());
+            manager.install(move || apply_and(manager, ParallelRecursor::new(manager), lhs, rhs))
         }
         #[inline]
         fn or_edge<'id>(
@@ -1524,7 +1528,10 @@ pub mod mt {
             lhs: &EdgeOfFunc<'id, Self>,
             rhs: &EdgeOfFunc<'id, Self>,
         ) -> AllocResult<EdgeOfFunc<'id, Self>> {
-            Ok(not_owned(Self::nor_edge(manager, lhs, rhs)?))
+            let (nl, nr) = (not(lhs), not(rhs));
+            Ok(not_owned(manager.install(move || {
+                apply_and(manager, ParallelRecursor::new(manager), nl, nr) // nor
+            })?))
         }
         #[inline]
         fn nand_edge<'id>(
@@ -1532,7 +1539,10 @@ pub mod mt {
             lhs: &EdgeOfFunc<'id, Self>,
             rhs: &EdgeOfFunc<'id, Self>,
         ) -> AllocResult<EdgeOfFunc<'id, Self>> {
-            Ok(not_owned(Self::and_edge(manager, lhs, rhs)?))
+            let (lhs, rhs) = (lhs.borrowed(), rhs.borrowed());
+            Ok(not_owned(manager.install(move || {
+                apply_and(manager, ParallelRecursor::new(manager), lhs, rhs)
+            })?))
         }
         #[inline]
         fn nor_edge<'id>(
@@ -1540,7 +1550,8 @@ pub mod mt {
             lhs: &EdgeOfFunc<'id, Self>,
             rhs: &EdgeOfFunc<'id, Self>,
         ) -> AllocResult<EdgeOfFunc<'id, Self>> {
-            apply_and(manager, ParallelRecursor::new(manager), not(lhs), not(rhs))
+            let (nl, nr) = (not(lhs), not(rhs));
+            manager.install(move || apply_and(manager, ParallelRecursor::new(manager), nl, nr))
         }
         #[inline]
         fn xor_edge<'id>(
@@ -1548,8 +1559,11 @@ pub mod mt {
             lhs: &EdgeOfFunc<'id, Self>,
             rhs: &EdgeOfFunc<'id, Self>,
         ) -> AllocResult<EdgeOfFunc<'id, Self>> {
-            let rec = ParallelRecursor::new(manager);
-            apply_bin::<_, _, { BCDDOp::Xor as u8 }>(manager, rec, lhs.borrowed(), rhs.borrowed())
+            let (lhs, rhs) = (lhs.borrowed(), rhs.borrowed());
+            manager.install(move || {
+                let rec = ParallelRecursor::new(manager);
+                apply_bin::<_, _, { BCDDOp::Xor as u8 }>(manager, rec, lhs, rhs)
+            })
         }
         #[inline]
         fn equiv_edge<'id>(
@@ -1557,7 +1571,11 @@ pub mod mt {
             lhs: &EdgeOfFunc<'id, Self>,
             rhs: &EdgeOfFunc<'id, Self>,
         ) -> AllocResult<EdgeOfFunc<'id, Self>> {
-            Ok(not_owned(Self::xor_edge(manager, lhs, rhs)?))
+            let (lhs, rhs) = (lhs.borrowed(), rhs.borrowed());
+            Ok(not_owned(manager.install(move || {
+                let rec = ParallelRecursor::new(manager);
+                apply_bin::<_, _, { BCDDOp::Xor as u8 }>(manager, rec, lhs, rhs)
+            })?))
         }
         #[inline]
         fn imp_edge<'id>(
@@ -1565,9 +1583,11 @@ pub mod mt {
             lhs: &EdgeOfFunc<'id, Self>,
             rhs: &EdgeOfFunc<'id, Self>,
         ) -> AllocResult<EdgeOfFunc<'id, Self>> {
-            let rec = ParallelRecursor::new(manager);
-            let tmp = apply_and(manager, rec, lhs.borrowed(), not(rhs))?;
-            Ok(not_owned(tmp))
+            // a → b ≡ ¬a ∨ b ≡ ¬(a ∧ ¬b)
+            let (lhs, nr) = (lhs.borrowed(), not(rhs));
+            Ok(not_owned(manager.install(move || {
+                apply_and(manager, ParallelRecursor::new(manager), lhs, nr)
+            })?))
         }
         #[inline]
         fn imp_strict_edge<'id>(
@@ -1575,24 +1595,19 @@ pub mod mt {
             lhs: &EdgeOfFunc<'id, Self>,
             rhs: &EdgeOfFunc<'id, Self>,
         ) -> AllocResult<EdgeOfFunc<'id, Self>> {
-            let rec = ParallelRecursor::new(manager);
-            apply_and(manager, rec, not(lhs), rhs.borrowed())
+            let (nl, rhs) = (not(lhs), rhs.borrowed());
+            manager.install(move || apply_and(manager, ParallelRecursor::new(manager), nl, rhs))
         }
 
         #[inline]
         fn ite_edge<'id>(
             manager: &Self::Manager<'id>,
-            if_edge: &EdgeOfFunc<'id, Self>,
-            then_edge: &EdgeOfFunc<'id, Self>,
-            else_edge: &EdgeOfFunc<'id, Self>,
+            f: &EdgeOfFunc<'id, Self>,
+            g: &EdgeOfFunc<'id, Self>,
+            h: &EdgeOfFunc<'id, Self>,
         ) -> AllocResult<EdgeOfFunc<'id, Self>> {
-            apply_ite(
-                manager,
-                ParallelRecursor::new(manager),
-                if_edge.borrowed(),
-                then_edge.borrowed(),
-                else_edge.borrowed(),
-            )
+            let (f, g, h) = (f.borrowed(), g.borrowed(), h.borrowed());
+            manager.install(move || apply_ite(manager, ParallelRecursor::new(manager), f, g, h))
         }
 
         #[inline]
@@ -1642,8 +1657,8 @@ pub mod mt {
             root: &EdgeOfFunc<'id, Self>,
             vars: &EdgeOfFunc<'id, Self>,
         ) -> AllocResult<EdgeOfFunc<'id, Self>> {
-            let rec = ParallelRecursor::new(manager);
-            restrict(manager, rec, root.borrowed(), vars.borrowed())
+            let (root, vars) = (root.borrowed(), vars.borrowed());
+            manager.install(move || restrict(manager, ParallelRecursor::new(manager), root, vars))
         }
 
         #[inline]
@@ -1652,8 +1667,11 @@ pub mod mt {
             root: &EdgeOfFunc<'id, Self>,
             vars: &EdgeOfFunc<'id, Self>,
         ) -> AllocResult<EdgeOfFunc<'id, Self>> {
-            let rec = ParallelRecursor::new(manager);
-            quant::<_, _, { BCDDOp::Forall as u8 }>(manager, rec, root.borrowed(), vars.borrowed())
+            let (root, vars) = (root.borrowed(), vars.borrowed());
+            manager.install(move || {
+                let rec = ParallelRecursor::new(manager);
+                quant::<_, _, { BCDDOp::Forall as u8 }>(manager, rec, root, vars)
+            })
         }
         #[inline]
         fn exist_edge<'id>(
@@ -1661,8 +1679,11 @@ pub mod mt {
             root: &EdgeOfFunc<'id, Self>,
             vars: &EdgeOfFunc<'id, Self>,
         ) -> AllocResult<EdgeOfFunc<'id, Self>> {
-            let rec = ParallelRecursor::new(manager);
-            quant::<_, _, { BCDDOp::Exist as u8 }>(manager, rec, root.borrowed(), vars.borrowed())
+            let (root, vars) = (root.borrowed(), vars.borrowed());
+            manager.install(move || {
+                let rec = ParallelRecursor::new(manager);
+                quant::<_, _, { BCDDOp::Exist as u8 }>(manager, rec, root, vars)
+            })
         }
         #[inline]
         fn unique_edge<'id>(
@@ -1670,8 +1691,11 @@ pub mod mt {
             root: &EdgeOfFunc<'id, Self>,
             vars: &EdgeOfFunc<'id, Self>,
         ) -> AllocResult<EdgeOfFunc<'id, Self>> {
-            let rec = ParallelRecursor::new(manager);
-            quant::<_, _, { BCDDOp::Unique as u8 }>(manager, rec, root.borrowed(), vars.borrowed())
+            let (root, vars) = (root.borrowed(), vars.borrowed());
+            manager.install(move || {
+                let rec = ParallelRecursor::new(manager);
+                quant::<_, _, { BCDDOp::Unique as u8 }>(manager, rec, root, vars)
+            })
         }
 
         #[inline]
@@ -1682,14 +1706,17 @@ pub mod mt {
             rhs: &EdgeOfFunc<'id, Self>,
             vars: &EdgeOfFunc<'id, Self>,
         ) -> AllocResult<EdgeOfFunc<'id, Self>> {
-            apply_quant_dispatch::<_, _, { BCDDOp::Forall as u8 }, { BCDDOp::Exist as u8 }>(
-                manager,
-                ParallelRecursor::new(manager),
-                op,
-                lhs.borrowed(),
-                rhs.borrowed(),
-                vars.borrowed(),
-            )
+            let (lhs, rhs, vars) = (lhs.borrowed(), rhs.borrowed(), vars.borrowed());
+            manager.install(move || {
+                apply_quant_dispatch::<_, _, { BCDDOp::Forall as u8 }, { BCDDOp::Exist as u8 }>(
+                    manager,
+                    ParallelRecursor::new(manager),
+                    op,
+                    lhs,
+                    rhs,
+                    vars,
+                )
+            })
         }
         #[inline]
         fn apply_exist_edge<'id>(
@@ -1699,14 +1726,17 @@ pub mod mt {
             rhs: &EdgeOfFunc<'id, Self>,
             vars: &EdgeOfFunc<'id, Self>,
         ) -> AllocResult<EdgeOfFunc<'id, Self>> {
-            apply_quant_dispatch::<_, _, { BCDDOp::Exist as u8 }, { BCDDOp::Forall as u8 }>(
-                manager,
-                ParallelRecursor::new(manager),
-                op,
-                lhs.borrowed(),
-                rhs.borrowed(),
-                vars.borrowed(),
-            )
+            let (lhs, rhs, vars) = (lhs.borrowed(), rhs.borrowed(), vars.borrowed());
+            manager.install(move || {
+                apply_quant_dispatch::<_, _, { BCDDOp::Exist as u8 }, { BCDDOp::Forall as u8 }>(
+                    manager,
+                    ParallelRecursor::new(manager),
+                    op,
+                    lhs,
+                    rhs,
+                    vars,
+                )
+            })
         }
         #[inline]
         fn apply_unique_edge<'id>(
@@ -1716,9 +1746,11 @@ pub mod mt {
             rhs: &EdgeOfFunc<'id, Self>,
             vars: &EdgeOfFunc<'id, Self>,
         ) -> AllocResult<EdgeOfFunc<'id, Self>> {
-            let rec = ParallelRecursor::new(manager);
             let (lhs, rhs, vars) = (lhs.borrowed(), rhs.borrowed(), vars.borrowed());
-            apply_quant_unique_dispatch(manager, rec, op, lhs, rhs, vars)
+            manager.install(move || {
+                let rec = ParallelRecursor::new(manager);
+                apply_quant_unique_dispatch(manager, rec, op, lhs, rhs, vars)
+            })
         }
     }
 
diff --git a/crates/oxidd-rules-bdd/src/recursor.rs b/crates/oxidd-rules-bdd/src/recursor.rs
index 5748131..1af73ee 100644
--- a/crates/oxidd-rules-bdd/src/recursor.rs
+++ b/crates/oxidd-rules-bdd/src/recursor.rs
@@ -142,9 +142,9 @@ pub mod mt {
 
     impl ParallelRecursor {
         pub fn new<M: WorkerManager>(manager: &M) -> Self {
-            let n = manager.current_num_threads();
-            let remaining_depth = if n > 1 { (4096 * n).ilog2() } else { 0 };
-            Self { remaining_depth }
+            Self {
+                remaining_depth: manager.split_depth(),
+            }
         }
     }
 
diff --git a/crates/oxidd-rules-bdd/src/simple/apply_rec.rs b/crates/oxidd-rules-bdd/src/simple/apply_rec.rs
index 0dc27eb..fbe7e3a 100644
--- a/crates/oxidd-rules-bdd/src/simple/apply_rec.rs
+++ b/crates/oxidd-rules-bdd/src/simple/apply_rec.rs
@@ -1200,8 +1200,12 @@ pub mod mt {
             >,
         ) -> AllocResult<EdgeOfFunc<'id, Self>> {
             let subst = substitute_prepare(manager, substitution.pairs())?;
-            let rec = ParallelRecursor::new(manager);
-            substitute(manager, rec, edge.borrowed(), &subst, substitution.id())
+            let cache_id = substitution.id();
+            let edge = edge.borrowed();
+            manager.install(move || {
+                let rec = ParallelRecursor::new(manager);
+                substitute(manager, rec, edge.borrowed(), &subst, cache_id)
+            })
         }
     }
 
@@ -1234,8 +1238,8 @@ pub mod mt {
             manager: &Self::Manager<'id>,
             edge: &EdgeOfFunc<'id, Self>,
         ) -> AllocResult<EdgeOfFunc<'id, Self>> {
-            let rec = ParallelRecursor::new(manager);
-            apply_not(manager, rec, edge.borrowed())
+            let edge = edge.borrowed();
+            manager.install(move || apply_not(manager, ParallelRecursor::new(manager), edge))
         }
 
         #[inline]
@@ -1244,8 +1248,11 @@ pub mod mt {
             lhs: &EdgeOfFunc<'id, Self>,
             rhs: &EdgeOfFunc<'id, Self>,
         ) -> AllocResult<EdgeOfFunc<'id, Self>> {
-            let rec = ParallelRecursor::new(manager);
-            apply_bin::<_, _, { BDDOp::And as u8 }>(manager, rec, lhs.borrowed(), rhs.borrowed())
+            let (lhs, rhs) = (lhs.borrowed(), rhs.borrowed());
+            manager.install(move || {
+                let rec = ParallelRecursor::new(manager);
+                apply_bin::<_, _, { BDDOp::And as u8 }>(manager, rec, lhs, rhs)
+            })
         }
         #[inline]
         fn or_edge<'id>(
@@ -1253,8 +1260,11 @@ pub mod mt {
             lhs: &EdgeOfFunc<'id, Self>,
             rhs: &EdgeOfFunc<'id, Self>,
         ) -> AllocResult<EdgeOfFunc<'id, Self>> {
-            let rec = ParallelRecursor::new(manager);
-            apply_bin::<_, _, { BDDOp::Or as u8 }>(manager, rec, lhs.borrowed(), rhs.borrowed())
+            let (lhs, rhs) = (lhs.borrowed(), rhs.borrowed());
+            manager.install(move || {
+                let rec = ParallelRecursor::new(manager);
+                apply_bin::<_, _, { BDDOp::Or as u8 }>(manager, rec, lhs, rhs)
+            })
         }
         #[inline]
         fn nand_edge<'id>(
@@ -1262,8 +1272,11 @@ pub mod mt {
             lhs: &EdgeOfFunc<'id, Self>,
             rhs: &EdgeOfFunc<'id, Self>,
         ) -> AllocResult<EdgeOfFunc<'id, Self>> {
-            let rec = ParallelRecursor::new(manager);
-            apply_bin::<_, _, { BDDOp::Nand as u8 }>(manager, rec, lhs.borrowed(), rhs.borrowed())
+            let (lhs, rhs) = (lhs.borrowed(), rhs.borrowed());
+            manager.install(move || {
+                let rec = ParallelRecursor::new(manager);
+                apply_bin::<_, _, { BDDOp::Nand as u8 }>(manager, rec, lhs, rhs)
+            })
         }
         #[inline]
         fn nor_edge<'id>(
@@ -1271,8 +1284,11 @@ pub mod mt {
             lhs: &EdgeOfFunc<'id, Self>,
             rhs: &EdgeOfFunc<'id, Self>,
         ) -> AllocResult<EdgeOfFunc<'id, Self>> {
-            let rec = ParallelRecursor::new(manager);
-            apply_bin::<_, _, { BDDOp::Nor as u8 }>(manager, rec, lhs.borrowed(), rhs.borrowed())
+            let (lhs, rhs) = (lhs.borrowed(), rhs.borrowed());
+            manager.install(move || {
+                let rec = ParallelRecursor::new(manager);
+                apply_bin::<_, _, { BDDOp::Nor as u8 }>(manager, rec, lhs, rhs)
+            })
         }
         #[inline]
         fn xor_edge<'id>(
@@ -1280,8 +1296,11 @@ pub mod mt {
             lhs: &EdgeOfFunc<'id, Self>,
             rhs: &EdgeOfFunc<'id, Self>,
         ) -> AllocResult<EdgeOfFunc<'id, Self>> {
-            let rec = ParallelRecursor::new(manager);
-            apply_bin::<_, _, { BDDOp::Xor as u8 }>(manager, rec, lhs.borrowed(), rhs.borrowed())
+            let (lhs, rhs) = (lhs.borrowed(), rhs.borrowed());
+            manager.install(move || {
+                let rec = ParallelRecursor::new(manager);
+                apply_bin::<_, _, { BDDOp::Xor as u8 }>(manager, rec, lhs, rhs)
+            })
         }
         #[inline]
         fn equiv_edge<'id>(
@@ -1289,8 +1308,11 @@ pub mod mt {
             lhs: &EdgeOfFunc<'id, Self>,
             rhs: &EdgeOfFunc<'id, Self>,
         ) -> AllocResult<EdgeOfFunc<'id, Self>> {
-            let rec = ParallelRecursor::new(manager);
-            apply_bin::<_, _, { BDDOp::Equiv as u8 }>(manager, rec, lhs.borrowed(), rhs.borrowed())
+            let (lhs, rhs) = (lhs.borrowed(), rhs.borrowed());
+            manager.install(move || {
+                let rec = ParallelRecursor::new(manager);
+                apply_bin::<_, _, { BDDOp::Equiv as u8 }>(manager, rec, lhs, rhs)
+            })
         }
         #[inline]
         fn imp_edge<'id>(
@@ -1298,8 +1320,11 @@ pub mod mt {
             lhs: &EdgeOfFunc<'id, Self>,
             rhs: &EdgeOfFunc<'id, Self>,
         ) -> AllocResult<EdgeOfFunc<'id, Self>> {
-            let rec = ParallelRecursor::new(manager);
-            apply_bin::<_, _, { BDDOp::Imp as u8 }>(manager, rec, lhs.borrowed(), rhs.borrowed())
+            let (lhs, rhs) = (lhs.borrowed(), rhs.borrowed());
+            manager.install(move || {
+                let rec = ParallelRecursor::new(manager);
+                apply_bin::<_, _, { BDDOp::Imp as u8 }>(manager, rec, lhs, rhs)
+            })
         }
         #[inline]
         fn imp_strict_edge<'id>(
@@ -1307,28 +1332,22 @@ pub mod mt {
             lhs: &EdgeOfFunc<'id, Self>,
             rhs: &EdgeOfFunc<'id, Self>,
         ) -> AllocResult<EdgeOfFunc<'id, Self>> {
-            apply_bin::<_, _, { BDDOp::ImpStrict as u8 }>(
-                manager,
-                ParallelRecursor::new(manager),
-                lhs.borrowed(),
-                rhs.borrowed(),
-            )
+            let (lhs, rhs) = (lhs.borrowed(), rhs.borrowed());
+            manager.install(move || {
+                let rec = ParallelRecursor::new(manager);
+                apply_bin::<_, _, { BDDOp::ImpStrict as u8 }>(manager, rec, lhs, rhs)
+            })
         }
 
         #[inline]
         fn ite_edge<'id>(
             manager: &Self::Manager<'id>,
-            if_edge: &EdgeOfFunc<'id, Self>,
-            then_edge: &EdgeOfFunc<'id, Self>,
-            else_edge: &EdgeOfFunc<'id, Self>,
+            f: &EdgeOfFunc<'id, Self>,
+            g: &EdgeOfFunc<'id, Self>,
+            h: &EdgeOfFunc<'id, Self>,
         ) -> AllocResult<EdgeOfFunc<'id, Self>> {
-            apply_ite(
-                manager,
-                ParallelRecursor::new(manager),
-                if_edge.borrowed(),
-                then_edge.borrowed(),
-                else_edge.borrowed(),
-            )
+            let (f, g, h) = (f.borrowed(), g.borrowed(), h.borrowed());
+            manager.install(move || apply_ite(manager, ParallelRecursor::new(manager), f, g, h))
         }
 
         #[inline]
@@ -1377,8 +1396,8 @@ pub mod mt {
             root: &EdgeOfFunc<'id, Self>,
             vars: &EdgeOfFunc<'id, Self>,
         ) -> AllocResult<EdgeOfFunc<'id, Self>> {
-            let rec = ParallelRecursor::new(manager);
-            restrict(manager, rec, root.borrowed(), vars.borrowed())
+            let (root, vars) = (root.borrowed(), vars.borrowed());
+            manager.install(move || restrict(manager, ParallelRecursor::new(manager), root, vars))
         }
 
         #[inline]
@@ -1387,8 +1406,11 @@ pub mod mt {
             root: &EdgeOfFunc<'id, Self>,
             vars: &EdgeOfFunc<'id, Self>,
         ) -> AllocResult<EdgeOfFunc<'id, Self>> {
-            let rec = ParallelRecursor::new(manager);
-            quant::<_, _, { BDDOp::And as u8 }>(manager, rec, root.borrowed(), vars.borrowed())
+            let (root, vars) = (root.borrowed(), vars.borrowed());
+            manager.install(move || {
+                let rec = ParallelRecursor::new(manager);
+                quant::<_, _, { BDDOp::And as u8 }>(manager, rec, root, vars)
+            })
         }
         #[inline]
         fn exist_edge<'id>(
@@ -1396,8 +1418,11 @@ pub mod mt {
             root: &EdgeOfFunc<'id, Self>,
             vars: &EdgeOfFunc<'id, Self>,
         ) -> AllocResult<EdgeOfFunc<'id, Self>> {
-            let rec = ParallelRecursor::new(manager);
-            quant::<_, _, { BDDOp::Or as u8 }>(manager, rec, root.borrowed(), vars.borrowed())
+            let (root, vars) = (root.borrowed(), vars.borrowed());
+            manager.install(move || {
+                let rec = ParallelRecursor::new(manager);
+                quant::<_, _, { BDDOp::Or as u8 }>(manager, rec, root, vars)
+            })
         }
         #[inline]
         fn unique_edge<'id>(
@@ -1405,8 +1430,11 @@ pub mod mt {
             root: &EdgeOfFunc<'id, Self>,
             vars: &EdgeOfFunc<'id, Self>,
         ) -> AllocResult<EdgeOfFunc<'id, Self>> {
-            let rec = ParallelRecursor::new(manager);
-            quant::<_, _, { BDDOp::Xor as u8 }>(manager, rec, root.borrowed(), vars.borrowed())
+            let (root, vars) = (root.borrowed(), vars.borrowed());
+            manager.install(move || {
+                let rec = ParallelRecursor::new(manager);
+                quant::<_, _, { BDDOp::Xor as u8 }>(manager, rec, root, vars)
+            })
         }
 
         #[inline]
@@ -1417,9 +1445,11 @@ pub mod mt {
             rhs: &EdgeOfFunc<'id, Self>,
             vars: &EdgeOfFunc<'id, Self>,
         ) -> AllocResult<EdgeOfFunc<'id, Self>> {
-            let rec = ParallelRecursor::new(manager);
             let (lhs, rhs, vars) = (lhs.borrowed(), rhs.borrowed(), vars.borrowed());
-            apply_quant_dispatch::<_, _, { BDDOp::And as u8 }>(manager, rec, op, lhs, rhs, vars)
+            manager.install(move || {
+                let rec = ParallelRecursor::new(manager);
+                apply_quant_dispatch::<_, _, { BDDOp::And as u8 }>(manager, rec, op, lhs, rhs, vars)
+            })
         }
         #[inline]
         fn apply_exist_edge<'id>(
@@ -1429,9 +1459,11 @@ pub mod mt {
             rhs: &EdgeOfFunc<'id, Self>,
             vars: &EdgeOfFunc<'id, Self>,
         ) -> AllocResult<EdgeOfFunc<'id, Self>> {
-            let rec = ParallelRecursor::new(manager);
             let (lhs, rhs, vars) = (lhs.borrowed(), rhs.borrowed(), vars.borrowed());
-            apply_quant_dispatch::<_, _, { BDDOp::Or as u8 }>(manager, rec, op, lhs, rhs, vars)
+            manager.install(move || {
+                let rec = ParallelRecursor::new(manager);
+                apply_quant_dispatch::<_, _, { BDDOp::Or as u8 }>(manager, rec, op, lhs, rhs, vars)
+            })
         }
         #[inline]
         fn apply_unique_edge<'id>(
@@ -1441,9 +1473,11 @@ pub mod mt {
             rhs: &EdgeOfFunc<'id, Self>,
             vars: &EdgeOfFunc<'id, Self>,
         ) -> AllocResult<EdgeOfFunc<'id, Self>> {
-            let rec = ParallelRecursor::new(manager);
             let (lhs, rhs, vars) = (lhs.borrowed(), rhs.borrowed(), vars.borrowed());
-            apply_quant_dispatch::<_, _, { BDDOp::Xor as u8 }>(manager, rec, op, lhs, rhs, vars)
+            manager.install(move || {
+                let rec = ParallelRecursor::new(manager);
+                apply_quant_dispatch::<_, _, { BDDOp::Xor as u8 }>(manager, rec, op, lhs, rhs, vars)
+            })
         }
     }
 
diff --git a/crates/oxidd-rules-zbdd/src/apply_rec.rs b/crates/oxidd-rules-zbdd/src/apply_rec.rs
index 95d6a69..cf2ff55 100644
--- a/crates/oxidd-rules-zbdd/src/apply_rec.rs
+++ b/crates/oxidd-rules-zbdd/src/apply_rec.rs
@@ -299,6 +299,15 @@ where
     Ok(h)
 }
 
+fn apply_not<M, R: Recursor<M>>(manager: &M, rec: R, f: Borrowed<M::Edge>) -> AllocResult<M::Edge>
+where
+    M: Manager<Terminal = ZBDDTerminal> + HasApplyCache<M, ZBDDOp> + HasZBDDCache<M::Edge>,
+    M::InnerNode: HasLevel,
+{
+    let taut = manager.zbdd_cache().tautology(0);
+    apply_diff(manager, rec, taut.borrowed(), f)
+}
+
 /// Recursively apply the symmetric difference operator to `f` and `g`
 fn apply_symm_diff<M, R: Recursor<M>>(
     manager: &M,
@@ -661,9 +670,7 @@ where
         manager: &Self::Manager<'id>,
         edge: &EdgeOfFunc<'id, Self>,
     ) -> AllocResult<EdgeOfFunc<'id, Self>> {
-        let rec = SequentialRecursor;
-        let taut = manager.zbdd_cache().tautology(0);
-        apply_diff(manager, rec, taut.borrowed(), edge.borrowed())
+        apply_not(manager, SequentialRecursor, edge.borrowed())
     }
 
     #[inline]
@@ -955,9 +962,12 @@ pub mod mt {
             set: &EdgeOfFunc<'id, Self>,
             var: &EdgeOfFunc<'id, Self>,
         ) -> AllocResult<EdgeOfFunc<'id, Self>> {
-            let rec = ParallelRecursor::new(manager);
-            let var_level = singleton_level(manager, var);
-            subset::<_, _, 0>(manager, rec, set.borrowed(), var.borrowed(), var_level)
+            let (set, var) = (set.borrowed(), var.borrowed());
+            manager.install(move || {
+                let rec = ParallelRecursor::new(manager);
+                let var_level = singleton_level(manager, &var);
+                subset::<_, _, 0>(manager, rec, set, var, var_level)
+            })
         }
 
         #[inline]
@@ -966,9 +976,12 @@ pub mod mt {
             set: &EdgeOfFunc<'id, Self>,
             var: &EdgeOfFunc<'id, Self>,
         ) -> AllocResult<EdgeOfFunc<'id, Self>> {
-            let rec = ParallelRecursor::new(manager);
-            let var_level = singleton_level(manager, var);
-            subset::<_, _, 1>(manager, rec, set.borrowed(), var.borrowed(), var_level)
+            let (set, var) = (set.borrowed(), var.borrowed());
+            manager.install(move || {
+                let rec = ParallelRecursor::new(manager);
+                let var_level = singleton_level(manager, &var);
+                subset::<_, _, 1>(manager, rec, set, var, var_level)
+            })
         }
 
         #[inline]
@@ -977,9 +990,12 @@ pub mod mt {
             set: &EdgeOfFunc<'id, Self>,
             var: &EdgeOfFunc<'id, Self>,
         ) -> AllocResult<EdgeOfFunc<'id, Self>> {
-            let rec = ParallelRecursor::new(manager);
-            let var_level = singleton_level(manager, var);
-            subset::<_, _, -1>(manager, rec, set.borrowed(), var.borrowed(), var_level)
+            let (set, var) = (set.borrowed(), var.borrowed());
+            manager.install(move || {
+                let rec = ParallelRecursor::new(manager);
+                let var_level = singleton_level(manager, &var);
+                subset::<_, _, -1>(manager, rec, set, var, var_level)
+            })
         }
 
         #[inline]
@@ -988,8 +1004,8 @@ pub mod mt {
             lhs: &EdgeOfFunc<'id, Self>,
             rhs: &EdgeOfFunc<'id, Self>,
         ) -> AllocResult<EdgeOfFunc<'id, Self>> {
-            let rec = ParallelRecursor::new(manager);
-            apply_union(manager, rec, lhs.borrowed(), rhs.borrowed())
+            let (lhs, rhs) = (lhs.borrowed(), rhs.borrowed());
+            manager.install(move || apply_union(manager, ParallelRecursor::new(manager), lhs, rhs))
         }
 
         #[inline]
@@ -998,8 +1014,8 @@ pub mod mt {
             lhs: &EdgeOfFunc<'id, Self>,
             rhs: &EdgeOfFunc<'id, Self>,
         ) -> AllocResult<EdgeOfFunc<'id, Self>> {
-            let rec = ParallelRecursor::new(manager);
-            apply_intsec(manager, rec, lhs.borrowed(), rhs.borrowed())
+            let (lhs, rhs) = (lhs.borrowed(), rhs.borrowed());
+            manager.install(move || apply_intsec(manager, ParallelRecursor::new(manager), lhs, rhs))
         }
 
         #[inline]
@@ -1008,8 +1024,8 @@ pub mod mt {
             lhs: &EdgeOfFunc<'id, Self>,
             rhs: &EdgeOfFunc<'id, Self>,
         ) -> AllocResult<EdgeOfFunc<'id, Self>> {
-            let rec = ParallelRecursor::new(manager);
-            apply_diff(manager, rec, lhs.borrowed(), rhs.borrowed())
+            let (lhs, rhs) = (lhs.borrowed(), rhs.borrowed());
+            manager.install(move || apply_diff(manager, ParallelRecursor::new(manager), lhs, rhs))
         }
     }
 
@@ -1062,9 +1078,12 @@ pub mod mt {
             manager: &Self::Manager<'id>,
             edge: &EdgeOfFunc<'id, Self>,
         ) -> AllocResult<EdgeOfFunc<'id, Self>> {
-            let rec = ParallelRecursor::new(manager);
-            let taut = manager.zbdd_cache().tautology(0);
-            apply_diff(manager, rec, taut.borrowed(), edge.borrowed())
+            let edge = edge.borrowed();
+            manager.install(move || {
+                let rec = ParallelRecursor::new(manager);
+                let taut = manager.zbdd_cache().tautology(0);
+                apply_diff(manager, rec, taut.borrowed(), edge)
+            })
         }
 
         #[inline]
@@ -1073,8 +1092,8 @@ pub mod mt {
             lhs: &EdgeOfFunc<'id, Self>,
             rhs: &EdgeOfFunc<'id, Self>,
         ) -> AllocResult<EdgeOfFunc<'id, Self>> {
-            let rec = ParallelRecursor::new(manager);
-            apply_intsec(manager, rec, lhs.borrowed(), rhs.borrowed())
+            let (lhs, rhs) = (lhs.borrowed(), rhs.borrowed());
+            manager.install(move || apply_intsec(manager, ParallelRecursor::new(manager), lhs, rhs))
         }
         #[inline]
         fn or_edge<'id>(
@@ -1082,8 +1101,8 @@ pub mod mt {
             lhs: &EdgeOfFunc<'id, Self>,
             rhs: &EdgeOfFunc<'id, Self>,
         ) -> AllocResult<EdgeOfFunc<'id, Self>> {
-            let rec = ParallelRecursor::new(manager);
-            apply_union(manager, rec, lhs.borrowed(), rhs.borrowed())
+            let (lhs, rhs) = (lhs.borrowed(), rhs.borrowed());
+            manager.install(move || apply_union(manager, ParallelRecursor::new(manager), lhs, rhs))
         }
         #[inline]
         fn nand_edge<'id>(
@@ -1091,8 +1110,12 @@ pub mod mt {
             lhs: &EdgeOfFunc<'id, Self>,
             rhs: &EdgeOfFunc<'id, Self>,
         ) -> AllocResult<EdgeOfFunc<'id, Self>> {
-            let and = Self::and_edge(manager, lhs, rhs)?;
-            Self::not_edge(manager, &*EdgeDropGuard::new(manager, and))
+            let (lhs, rhs) = (lhs.borrowed(), rhs.borrowed());
+            manager.install(move || {
+                let rec = ParallelRecursor::new(manager);
+                let and = EdgeDropGuard::new(manager, apply_intsec(manager, rec, lhs, rhs)?);
+                apply_not(manager, rec, and.borrowed())
+            })
         }
         #[inline]
         fn nor_edge<'id>(
@@ -1100,8 +1123,12 @@ pub mod mt {
             lhs: &EdgeOfFunc<'id, Self>,
             rhs: &EdgeOfFunc<'id, Self>,
         ) -> AllocResult<EdgeOfFunc<'id, Self>> {
-            let or = Self::or_edge(manager, lhs, rhs)?;
-            Self::not_edge(manager, &*EdgeDropGuard::new(manager, or))
+            let (lhs, rhs) = (lhs.borrowed(), rhs.borrowed());
+            manager.install(move || {
+                let rec = ParallelRecursor::new(manager);
+                let or = EdgeDropGuard::new(manager, apply_union(manager, rec, lhs, rhs)?);
+                apply_not(manager, rec, or.borrowed())
+            })
         }
         #[inline]
         fn xor_edge<'id>(
@@ -1109,8 +1136,9 @@ pub mod mt {
             lhs: &EdgeOfFunc<'id, Self>,
             rhs: &EdgeOfFunc<'id, Self>,
         ) -> AllocResult<EdgeOfFunc<'id, Self>> {
-            let rec = ParallelRecursor::new(manager);
-            apply_symm_diff(manager, rec, lhs.borrowed(), rhs.borrowed())
+            let (lhs, rhs) = (lhs.borrowed(), rhs.borrowed());
+            manager
+                .install(move || apply_symm_diff(manager, ParallelRecursor::new(manager), lhs, rhs))
         }
         #[inline]
         fn equiv_edge<'id>(
@@ -1118,8 +1146,12 @@ pub mod mt {
             lhs: &EdgeOfFunc<'id, Self>,
             rhs: &EdgeOfFunc<'id, Self>,
         ) -> AllocResult<EdgeOfFunc<'id, Self>> {
-            let xor = Self::xor_edge(manager, lhs, rhs)?;
-            Self::not_edge(manager, &*EdgeDropGuard::new(manager, xor))
+            let (lhs, rhs) = (lhs.borrowed(), rhs.borrowed());
+            manager.install(move || {
+                let rec = ParallelRecursor::new(manager);
+                let xor = EdgeDropGuard::new(manager, apply_symm_diff(manager, rec, lhs, rhs)?);
+                apply_not(manager, rec, xor.borrowed())
+            })
         }
         #[inline]
         fn imp_edge<'id>(
@@ -1127,7 +1159,12 @@ pub mod mt {
             lhs: &EdgeOfFunc<'id, Self>,
             rhs: &EdgeOfFunc<'id, Self>,
         ) -> AllocResult<EdgeOfFunc<'id, Self>> {
-            Self::ite_edge(manager, lhs, rhs, manager.zbdd_cache().tautology(0))
+            let (lhs, rhs) = (lhs.borrowed(), rhs.borrowed());
+            manager.install(move || {
+                let rec = ParallelRecursor::new(manager);
+                let taut = manager.zbdd_cache().tautology(0);
+                apply_ite(manager, rec, lhs, rhs, taut.borrowed())
+            })
         }
         #[inline]
         fn imp_strict_edge<'id>(
@@ -1135,8 +1172,8 @@ pub mod mt {
             lhs: &EdgeOfFunc<'id, Self>,
             rhs: &EdgeOfFunc<'id, Self>,
         ) -> AllocResult<EdgeOfFunc<'id, Self>> {
-            let rec = ParallelRecursor::new(manager);
-            apply_diff(manager, rec, rhs.borrowed(), lhs.borrowed())
+            let (lhs, rhs) = (lhs.borrowed(), rhs.borrowed());
+            manager.install(move || apply_diff(manager, ParallelRecursor::new(manager), rhs, lhs))
         }
 
         #[inline]
@@ -1146,8 +1183,8 @@ pub mod mt {
             g: &EdgeOfFunc<'id, Self>,
             h: &EdgeOfFunc<'id, Self>,
         ) -> AllocResult<EdgeOfFunc<'id, Self>> {
-            let rec = ParallelRecursor::new(manager);
-            apply_ite(manager, rec, f.borrowed(), g.borrowed(), h.borrowed())
+            let (f, g, h) = (f.borrowed(), g.borrowed(), h.borrowed());
+            manager.install(move || apply_ite(manager, ParallelRecursor::new(manager), f, g, h))
         }
 
         #[inline]
diff --git a/crates/oxidd-rules-zbdd/src/recursor.rs b/crates/oxidd-rules-zbdd/src/recursor.rs
index bc1ae16..73021bb 100644
--- a/crates/oxidd-rules-zbdd/src/recursor.rs
+++ b/crates/oxidd-rules-zbdd/src/recursor.rs
@@ -143,9 +143,9 @@ pub mod mt {
 
     impl ParallelRecursor {
         pub fn new<M: WorkerManager>(manager: &M) -> Self {
-            let n = manager.current_num_threads();
-            let remaining_depth = if n > 1 { (4096 * n).ilog2() } else { 0 };
-            Self { remaining_depth }
+            Self {
+                remaining_depth: manager.split_depth(),
+            }
         }
     }
 
diff --git a/crates/oxidd-test-utils/src/edge.rs b/crates/oxidd-test-utils/src/edge.rs
index 3c48223..898022c 100644
--- a/crates/oxidd-test-utils/src/edge.rs
+++ b/crates/oxidd-test-utils/src/edge.rs
@@ -207,6 +207,16 @@ impl WorkerManager for DummyManager {
         rayon::current_num_threads()
     }
 
+    fn split_depth(&self) -> u32 {
+        42
+    }
+
+    fn set_split_depth(&self, _depth: Option<u32>) {}
+
+    fn install<R: Send>(&self, op: impl FnOnce() -> R + Send) -> R {
+        op()
+    }
+
     fn join<RA: Send, RB: Send>(
         &self,
         op_a: impl FnOnce() -> RA + Send,
diff --git a/crates/oxidd/src/lib.rs b/crates/oxidd/src/lib.rs
index 9e9efc6..3380503 100644
--- a/crates/oxidd/src/lib.rs
+++ b/crates/oxidd/src/lib.rs
@@ -17,7 +17,7 @@ pub use oxidd_core::function::{
     NumberBase, PseudoBooleanFunction, TVLFunction,
 };
 pub use oxidd_core::util::{Subst, Substitution};
-pub use oxidd_core::{Edge, InnerNode, LevelNo, Manager, ManagerRef, NodeID};
+pub use oxidd_core::{Edge, InnerNode, LevelNo, Manager, ManagerRef, NodeID, WorkerManager};
 
 pub mod util;
 
diff --git a/crates/oxidd/tests/boolean_function.rs b/crates/oxidd/tests/boolean_function.rs
index 6a18a1b..26cd545 100644
--- a/crates/oxidd/tests/boolean_function.rs
+++ b/crates/oxidd/tests/boolean_function.rs
@@ -15,7 +15,7 @@ use oxidd::zbdd::ZBDDFunction;
 use oxidd::zbdd::ZBDDManagerRef;
 use oxidd::{
     BooleanFunction, BooleanFunctionQuant, BooleanOperator, BooleanVecSet, Function, FunctionSubst,
-    ManagerRef,
+    ManagerRef, WorkerManager,
 };
 
 use boolean_prop::Prop;
@@ -857,6 +857,7 @@ fn bdd_all_boolean_functions_2vars_t1() {
 #[cfg_attr(miri, ignore)]
 fn bdd_all_boolean_functions_2vars_t2() {
     let mref = oxidd::bdd::new_manager(65536, 1024, 2);
+    mref.with_manager_shared(|manager| manager.set_split_depth(Some(u32::MAX)));
     let vars = bdd_vars::<BDDFunction>(&mref, 2);
     let test = TestAllBooleanFunctions::init(&mref, &vars, &vars);
     test.basic();
@@ -879,6 +880,7 @@ fn bcdd_all_boolean_functions_2vars_t1() {
 #[cfg_attr(miri, ignore)]
 fn bcdd_all_boolean_functions_2vars_t2() {
     let mref = oxidd::bcdd::new_manager(65536, 1024, 2);
+    mref.with_manager_shared(|manager| manager.set_split_depth(Some(u32::MAX)));
     let vars = bdd_vars::<BCDDFunction>(&mref, 2);
     let test = TestAllBooleanFunctions::init(&mref, &vars, &vars);
     test.basic();
@@ -899,6 +901,7 @@ fn zbdd_all_boolean_functions_2vars_t1() {
 #[cfg_attr(miri, ignore)]
 fn zbdd_all_boolean_functions_2vars_t2() {
     let mref = oxidd::zbdd::new_manager(65536, 1024, 2);
+    mref.with_manager_shared(|manager| manager.set_split_depth(Some(u32::MAX)));
     let (singletons, vars) = zbdd_singletons_vars(&mref, 2);
     let test = TestAllBooleanFunctions::init(&mref, &vars, &singletons);
     test.basic();