diff --git a/Cargo.toml b/Cargo.toml
index 70255a0..e6217ec 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -9,11 +9,11 @@ exclude = ["python", "bench"]
 [workspace.dependencies]
 tracing = "0.1"
 tracing-subscriber = "0.3"
-biodivine-lib-bdd = "0.5.23"
-itertools = "0.14.0"
+biodivine-lib-bdd = "0.6"
+itertools = "0.14"
 indexmap = "2.7"
 bimap = "0.6"
-rand = "0.8.5"
+rand = { version = "0.10", features = ["thread_rng"] }
 thiserror = "2.0"
-crossbeam-channel = "0.5.14"
-tabled = { version = "0.16", features = ["ansi"] }
+crossbeam-channel = "0.5"
+tabled = { version = "0.20", features = ["ansi"] }
diff --git a/crates/automata-core/src/alphabet.rs b/crates/automata-core/src/alphabet.rs
index ad9dc19..b2adea7 100644
--- a/crates/automata-core/src/alphabet.rs
+++ b/crates/automata-core/src/alphabet.rs
@@ -182,7 +182,7 @@ impl<S: Symbol> Iterator for FreeMonoid<S> {
         }
 
         if carry {
-            self.current = std::iter::repeat(0).take(self.current.len() + 1).collect();
+            self.current = std::iter::repeat_n(0, self.current.len() + 1).collect();
         }
 
         Some(out)
diff --git a/crates/automata-core/src/alphabet/propositional.rs b/crates/automata-core/src/alphabet/propositional.rs
index a06afd2..d7e3d8d 100644
--- a/crates/automata-core/src/alphabet/propositional.rs
+++ b/crates/automata-core/src/alphabet/propositional.rs
@@ -111,7 +111,7 @@ impl<RawTy: RawSymbolRepr> PropSymbol<RawTy> {
         BddValuation::new(self.as_bools())
     }
     pub fn from_bdd_valuation(val: BddValuation) -> Self {
-        Self::from_bools(val.vector())
+        Self::from_bools(val.into_vector())
     }
 }
 
diff --git a/crates/automata-core/src/word/finite.rs b/crates/automata-core/src/word/finite.rs
index a3ff173..9a295ce 100644
--- a/crates/automata-core/src/word/finite.rs
+++ b/crates/automata-core/src/word/finite.rs
@@ -2,7 +2,7 @@ use std::collections::VecDeque;
 
 use itertools::Itertools;
 
-use crate::{alphabet::Symbol, show::Show};
+use crate::{alphabet::Symbol, show::Show, word::skip::Rotated};
 
 use super::{Concat, PeriodicOmegaWord, Repeat, Word, omega::OmegaIteration};
 
@@ -78,6 +78,13 @@ pub trait FiniteWord: Word {
         Repeat::new(self, times)
     }
 
+    fn rotate(self, steps: usize) -> Rotated<Self>
+    where
+        Self: Sized,
+    {
+        Rotated(self, steps)
+    }
+
     /// Builds the [`PeriodicOmegaWord`] word that is the omega power of this word, i.e. if
     /// `self` is the word `u`, then the result is the word `u^ω` = `u u u u ...`.
     /// Panics if `self` is empty as the operation is not defined in that case.
diff --git a/crates/automata-core/src/word/omega.rs b/crates/automata-core/src/word/omega.rs
index 70ac189..17d04ab 100644
--- a/crates/automata-core/src/word/omega.rs
+++ b/crates/automata-core/src/word/omega.rs
@@ -155,7 +155,7 @@ fn deduplicate_inplace<S: Eq>(input: &mut Vec<S>) {
     for i in 1..=(input.len() / 2) {
         // for a word w of length n, if th first n-i symbols of w are equal to the
         // last n-i symbols of w, then w is periodic with period i
-        if input.len() % i == 0 && input[..input.len() - i] == input[i..] {
+        if input.len().is_multiple_of(i) && input[..input.len() - i] == input[i..] {
             input.truncate(i);
             return;
         }
diff --git a/crates/automata-core/src/word/skip.rs b/crates/automata-core/src/word/skip.rs
index b9e3853..0a1dfa6 100644
--- a/crates/automata-core/src/word/skip.rs
+++ b/crates/automata-core/src/word/skip.rs
@@ -56,6 +56,7 @@ impl<W: FiniteWord> Word for Rotated<W> {
     }
 }
 
+#[derive(Clone, PartialEq, Debug, Hash, Eq)]
 pub struct RotatedIter<'a, W> {
     rotated: &'a Rotated<W>,
     start: usize,
diff --git a/crates/automata-learning/src/active/lstar.rs b/crates/automata-learning/src/active/lstar.rs
index b7f4c94..26e4588 100644
--- a/crates/automata-learning/src/active/lstar.rs
+++ b/crates/automata-learning/src/active/lstar.rs
@@ -351,16 +351,16 @@ mod tests {
     use automata::TransitionSystem;
     use automata::automaton::{MealyMachine, MooreMachine};
     use automata::core::alphabet::CharAlphabet;
-    use rand::Rng;
+    use rand::{Rng, RngExt};
     use tracing::trace;
 
     #[test]
     fn lstar_random_mealy() {
-        let mut rng = rand::thread_rng();
+        let mut rng = rand::rng();
         for i in 0..200 {
-            let symbols = rng.gen_range(1..5);
-            let max_color = rng.gen_range(1..10);
-            let size = rng.gen_range(1..25);
+            let symbols = rng.random_range(1..5);
+            let max_color = rng.random_range(1..10);
+            let size = rng.random_range(1..25);
 
             let pre_gen = std::time::Instant::now();
             let ts = automata::random::generate_random_mealy(symbols, max_color, size);
@@ -387,11 +387,11 @@ mod tests {
     }
     #[test]
     fn lstar_random_moore() {
-        let mut rng = rand::thread_rng();
+        let mut rng = rand::rng();
         for i in 0..200 {
-            let symbols = rng.gen_range(1..5);
-            let max_color = rng.gen_range(1..10);
-            let size = rng.gen_range(1..25);
+            let symbols = rng.random_range(1..5);
+            let max_color = rng.random_range(1..10);
+            let size = rng.random_range(1..25);
 
             let pre_gen = std::time::Instant::now();
             let ts = automata::random::generate_random_moore(symbols, max_color, size);
diff --git a/crates/automata-learning/src/passive/dpainf.rs b/crates/automata-learning/src/passive/dpainf.rs
index 7a38cb9..71ff0e6 100644
--- a/crates/automata-learning/src/passive/dpainf.rs
+++ b/crates/automata-learning/src/passive/dpainf.rs
@@ -316,6 +316,7 @@ pub enum DpaInfError<A: Alphabet> {
 }
 
 /// Runs the omega-sprout algorithm on a given conflict relation.
+#[allow(clippy::result_large_err)]
 pub fn dpainf<A, C>(
     conflicts: C,
     additional_constraints: Vec<Box<dyn ConsistencyCheck<A>>>,
diff --git a/crates/automata-learning/src/passive/sample/omega.rs b/crates/automata-learning/src/passive/sample/omega.rs
index 7b50ee7..8fc2a01 100644
--- a/crates/automata-learning/src/passive/sample/omega.rs
+++ b/crates/automata-learning/src/passive/sample/omega.rs
@@ -188,6 +188,7 @@ impl<A: Alphabet> OmegaSample<A> {
     }
 
     /// Computes the [`RightCongruence`] underlying the sample.
+    #[allow(clippy::result_large_err)]
     pub fn infer_prefix_congruence(&self) -> Result<RightCongruence<A>, DpaInfError<A>> {
         dpainf(prefix_consistency_conflicts(self), vec![], true, None)
     }
diff --git a/crates/automata/src/automaton/omega/buchi.rs b/crates/automata/src/automaton/omega/buchi.rs
index c2a1bf9..a4f1406 100644
--- a/crates/automata/src/automaton/omega/buchi.rs
+++ b/crates/automata/src/automaton/omega/buchi.rs
@@ -70,13 +70,13 @@ where
                 // let InfinityColors(colors) = self
                 //     .induced(&full_word, self.initial())
                 //     .expect("word is valid");
-                if let Some(infset) = self.visited_edge_colors_from(good_scc.first(), &full_word) {
-                    if infset.iter().any(|b| *b) {
-                        let spoke = self
-                            .word_from_to(self.initial, good_scc.first())
-                            .expect("We know this is reachable!");
-                        return Some(ReducedOmegaWord::ultimately_periodic(spoke, full_word));
-                    }
+                if let Some(infset) = self.visited_edge_colors_from(good_scc.first(), &full_word)
+                    && infset.iter().any(|b| *b)
+                {
+                    let spoke = self
+                        .word_from_to(self.initial, good_scc.first())
+                        .expect("We know this is reachable!");
+                    return Some(ReducedOmegaWord::ultimately_periodic(spoke, full_word));
                 }
                 // if colors.contains(&true) {
                 //     let base = self
diff --git a/crates/automata/src/automaton/omega/parity.rs b/crates/automata/src/automaton/omega/parity.rs
index ec5e7d2..1f2a99d 100644
--- a/crates/automata/src/automaton/omega/parity.rs
+++ b/crates/automata/src/automaton/omega/parity.rs
@@ -51,7 +51,7 @@ where
     type Output = bool;
     type Observer = run::EdgeColorLimit<T>;
     fn evaluate(&self, observed: <Self::Observer as run::Observer<T>>::Current) -> Self::Output {
-        observed % 2 == 0
+        observed.is_multiple_of(2)
     }
 }
 
diff --git a/crates/automata/src/dot.rs b/crates/automata/src/dot.rs
index 9ae2d15..28ab694 100644
--- a/crates/automata/src/dot.rs
+++ b/crates/automata/src/dot.rs
@@ -216,18 +216,16 @@ pub trait Dottable: TransitionSystem {
             .arg(tempfile_name)
             .spawn()?;
         if !child.wait()?.success() {
-            Err(std::io::Error::new(
-                std::io::ErrorKind::Other,
-                child
-                    .stdout
-                    .map_or("Error in dot...".to_string(), |mut err| {
-                        let mut buf = String::new();
-                        if let Err(e) = err.read_to_string(&mut buf) {
-                            buf = format!("Could not read from stdout: {e}");
-                        }
-                        buf
-                    }),
-            ))
+            Err(std::io::Error::other(child.stdout.map_or(
+                "Error in dot...".to_string(),
+                |mut err| {
+                    let mut buf = String::new();
+                    if let Err(e) = err.read_to_string(&mut buf) {
+                        buf = format!("Could not read from stdout: {e}");
+                    }
+                    buf
+                },
+            )))
         } else {
             Ok(())
         }
diff --git a/crates/automata/src/minimization/partition_refinement.rs b/crates/automata/src/minimization/partition_refinement.rs
index 08c0331..21fc953 100644
--- a/crates/automata/src/minimization/partition_refinement.rs
+++ b/crates/automata/src/minimization/partition_refinement.rs
@@ -33,13 +33,13 @@ where
         for sym in mm.symbols() {
             let mut splitter = math::Map::default();
             for q in mm.state_indices() {
-                if let Some(t) = mm.edge(q, sym) {
-                    if set.contains(&t.target()) {
-                        splitter
-                            .entry(t.color())
-                            .or_insert(BTreeSet::default())
-                            .insert(q);
-                    }
+                if let Some(t) = mm.edge(q, sym)
+                    && set.contains(&t.target())
+                {
+                    splitter
+                        .entry(t.color())
+                        .or_insert(BTreeSet::default())
+                        .insert(q);
                 }
             }
 
diff --git a/crates/automata/src/random/mod.rs b/crates/automata/src/random/mod.rs
index 30e8f3b..68179ad 100644
--- a/crates/automata/src/random/mod.rs
+++ b/crates/automata/src/random/mod.rs
@@ -7,7 +7,8 @@ use automata_core::alphabet::{Alphabet, CharAlphabet};
 use automata_core::word::ReducedOmegaWord;
 use automata_core::{Int, Void, math, upw};
 use math::sample_continuous_bernoulli;
-use rand::{Rng, rngs::ThreadRng, thread_rng};
+use rand::RngExt;
+use rand::{Rng, rng, rngs::ThreadRng};
 use std::cmp::min;
 use tracing::{debug, info};
 
@@ -25,7 +26,7 @@ pub fn generate_random_ts(symbols: usize, probability: f64) -> (DTS, StateIndex<
 
     let mut current = dts.add_state(Void);
     let mut symbol_position = 0;
-    let mut rng = thread_rng();
+    let mut rng = rng();
 
     'outer: loop {
         if current >= (dts.size() as DefaultIdType) {
@@ -44,7 +45,7 @@ pub fn generate_random_ts(symbols: usize, probability: f64) -> (DTS, StateIndex<
         symbol_position += 1;
 
         for target in 0..=current {
-            let value: f64 = rng.gen_range(0.0..=1.0);
+            let value: f64 = rng.random_range(0.0..=1.0);
             if value < probability {
                 dts.add_edge((current, symbol, target));
                 continue 'outer;
@@ -62,7 +63,7 @@ pub fn generate_random_ts(symbols: usize, probability: f64) -> (DTS, StateIndex<
 /// Works as [`generate_random_ts`], but returns a [`DFA`] instead by randomly coloring the states.
 pub fn generate_random_dfa(symbols: usize, probability: f64) -> DFA {
     let (ts, initial) = generate_random_ts(symbols, probability);
-    ts.map_state_colors(|_| thread_rng().gen_bool(probability))
+    ts.map_state_colors(|_| rng().random_bool(probability))
         .with_initial(initial)
         .into_dfa()
 }
@@ -72,7 +73,7 @@ pub fn generate_random_dfa(symbols: usize, probability: f64) -> DFA {
 pub fn generate_random_mealy(symbols: usize, max_color: usize, size: usize) -> MealyMachine {
     let (ts, initial) = generate_random_ts_sized(symbols, size);
     let mut mm = ts
-        .map_edge_colors(|_| thread_rng().gen_range(0..=max_color) as Int)
+        .map_edge_colors(|_| rng().random_range(0..=max_color) as Int)
         .with_initial(initial)
         .into_mealy()
         .minimize()
@@ -86,7 +87,7 @@ pub fn generate_random_mealy(symbols: usize, max_color: usize, size: usize) -> M
 pub fn generate_random_moore(symbols: usize, max_color: usize, size: usize) -> MooreMachine {
     let (ts, initial) = generate_random_ts_sized(symbols, size);
     let mut mm = ts
-        .map_state_colors(|_| thread_rng().gen_range(0..=max_color) as Int)
+        .map_state_colors(|_| rng().random_range(0..=max_color) as Int)
         .with_initial(initial)
         .into_moore()
         .minimize()
@@ -111,10 +112,10 @@ pub fn generate_random_ts_sized(symbols: usize, size: usize) -> (DTS, StateIndex
         dts.add_state(Void);
     }
     // add edges
-    let mut rng = thread_rng();
+    let mut rng = rng();
     for q in dts.state_indices_vec() {
         for sym in alphabet.universe() {
-            let target = rng.gen_range(0..(dts.size() as DefaultIdType));
+            let target = rng.random_range(0..(dts.size() as DefaultIdType));
             dts.add_edge((q, sym, target));
         }
     }
@@ -165,11 +166,11 @@ pub fn draw_priority(num_prios: u8, lambda: f64) -> u8 {
 pub fn generate_random_word(alphabet: &CharAlphabet, min_len: usize, max_len: usize) -> String {
     let charset: Vec<char> = alphabet.universe().collect();
 
-    let mut rng = thread_rng();
-    let length = rng.gen_range(min_len..=max_len);
+    let mut rng = rng();
+    let length = rng.random_range(min_len..=max_len);
     let random_word: String = (0..length)
         .map(|_| {
-            let idx = rng.gen_range(0..charset.len());
+            let idx = rng.random_range(0..charset.len());
             charset[idx] as char
         })
         .collect();
diff --git a/crates/automata/src/ts/impls/linked.rs b/crates/automata/src/ts/impls/linked.rs
index 77b8d47..2dfb946 100644
--- a/crates/automata/src/ts/impls/linked.rs
+++ b/crates/automata/src/ts/impls/linked.rs
@@ -504,11 +504,9 @@ impl<A: Alphabet, Q: Color, C: Color, const DET: bool> Sproutable
         let (q, a, c, p) = t.into_edge_tuple();
 
         let mut out = None;
-        if DET {
-            if let Some(pos) = self.out_edge_position(q.into_usize(), &a) {
-                trace!("found previously existing edge {pos} in deterministic automaton");
-                out = Some(self.swap_remove_edge(pos).unwrap());
-            }
+        if DET && let Some(pos) = self.out_edge_position(q.into_usize(), &a) {
+            trace!("found previously existing edge {pos} in deterministic automaton");
+            out = Some(self.swap_remove_edge(pos).unwrap());
         }
 
         let mut edge = LinkedListTransitionSystemEdge::new(q, a, c, p);
diff --git a/crates/hoars/src/body.rs b/crates/hoars/src/body.rs
index 7048dec..30a65cb 100644
--- a/crates/hoars/src/body.rs
+++ b/crates/hoars/src/body.rs
@@ -8,6 +8,7 @@ use crate::{
 };
 
 #[derive(Debug, Clone, PartialEq, Eq, Hash)]
+#[allow(unused)]
 pub struct Alphabet(pub Vec<AtomicProposition>);
 
 #[derive(Clone, Debug)]
diff --git a/crates/hoars/src/format.rs b/crates/hoars/src/format.rs
index ef14534..d921614 100644
--- a/crates/hoars/src/format.rs
+++ b/crates/hoars/src/format.rs
@@ -55,7 +55,7 @@ impl AcceptanceSignature {
     /// Tries to get the singleton element of the acceptance signature, if it exists.
     /// Returns `None` if the acceptance signature is not a singleton.
     pub fn get_singleton(&self) -> Option<Option<Id>> {
-        if self.len() == 0 {
+        if self.is_empty() {
             Some(None)
         } else if self.len() == 1 {
             Some(Some(self[0]))
diff --git a/crates/hoars/src/lib.rs b/crates/hoars/src/lib.rs
index ca11598..ea85f13 100644
--- a/crates/hoars/src/lib.rs
+++ b/crates/hoars/src/lib.rs
@@ -155,14 +155,14 @@ impl HoaRepresentation {
             }
             states.push(state.id());
         }
-        if let Some(num_states) = self.num_states() {
-            if states.len() != num_states {
-                errors.push(format!(
-                    "The number of states is set to {} but there are {} states!",
-                    num_states,
-                    states.len()
-                ));
-            }
+        if let Some(num_states) = self.num_states()
+            && states.len() != num_states
+        {
+            errors.push(format!(
+                "The number of states is set to {} but there are {} states!",
+                num_states,
+                states.len()
+            ));
         }
         if errors.is_empty() {
             Ok(())
@@ -422,10 +422,10 @@ pub fn first_automaton_split_position(input: &str) -> Option<usize> {
 
     'outer: loop {
         if let Some(end) = input.find("--END--") {
-            if let Some(abort) = input.find("--ABORT--") {
-                if abort < end {
-                    continue 'outer;
-                }
+            if let Some(abort) = input.find("--ABORT--")
+                && abort < end
+            {
+                continue 'outer;
             }
             return Some(end + ENDLEN);
         } else {