diff --git a/src/bdd/traits/boolean_function.rs b/src/bdd/traits/boolean_function.rs
index d0a6b41..042a39f 100644
--- a/src/bdd/traits/boolean_function.rs
+++ b/src/bdd/traits/boolean_function.rs
@@ -407,55 +407,59 @@ mod tests {
         assert_eq!(actual.degree(), expected.degree());
     }
 
-    // #[test]
-    // fn test_substitute_variables_same_substituted_ok() {
-    //     let input = Bdd::try_from((var("a") | var("b")) & var("c") & !var("a") & bool(true))
-    //         .expect("Should not panic here");
-    //
-    //     let new_value = var("a") | !var("b");
-    //     let new_value_bdd = Bdd::try_from(new_value.clone()).expect("Should not panic here");
-    //     let mapping = BTreeMap::from_iter([("a".to_string(), new_value_bdd)]);
-    //
-    //     // cannot use `var("a") | !var("b") | var("b")` for defining expected here
-    //     // since that collapses Or(Or(a, !b), b), which substitute doesn't do
-    //     let expected = Bdd::try_from(
-    //         Expression::n_ary_or(&[new_value.clone(), var("b")])
-    //             & var("c")
-    //             & !new_value.clone()
-    //             & bool(true),
-    //     )
-    //     .expect("Should not panic here");
-    //     let actual = input.substitute(&mapping);
-    //
-    //     assert_eq!(expected, actual);
-    //     assert!(expected.is_equivalent(&actual));
-    //     assert_eq!(actual.degree(), expected.degree());
-    // }
-    //
-    // #[test]
-    // fn test_substitute_variables_same_unsubstituted_ok() {
-    //     let input = Bdd::try_from((var("a") | var("b")) & var("c") & !var("a") & bool(true))
-    //         .expect("Should not panic here");
-    //
-    //     let new_value = var("c") | !var("b");
-    //     let new_value_bdd = Bdd::try_from(new_value.clone()).expect("Should not panic here");
-    //     let mapping = BTreeMap::from_iter([("a".to_string(), new_value_bdd)]);
-    //
-    //     // cannot use `var("a") | !var("b") | var("b")` for defining expected here
-    //     // since that collapses Or(Or(a, !b), b), which substitute doesn't do
-    //     let expected = Bdd::try_from(
-    //         Expression::n_ary_or(&[new_value.clone(), var("b")])
-    //             & var("c")
-    //             & !new_value.clone()
-    //             & bool(true),
-    //     )
-    //     .expect("Should not panic here");
-    //     let actual = input.substitute(&mapping);
-    //
-    //     assert_eq!(expected, actual);
-    //     assert!(expected.is_equivalent(&actual));
-    //     assert_eq!(actual.degree(), expected.degree());
-    // }
+    #[test]
+    #[should_panic]
+    fn test_substitute_variables_same_substituted_ok() {
+        let input = Bdd::try_from((var("a") | var("b")) & var("c") & !var("a") & bool(true))
+            .expect("Should not panic here");
+
+        let new_value = var("a") | !var("b");
+        let new_value_bdd = Bdd::try_from(new_value.clone()).expect("Should not panic here");
+        let mapping = BTreeMap::from_iter([("a".to_string(), new_value_bdd)]);
+
+        // cannot use `var("a") | !var("b") | var("b")` for defining expected here
+        // since that collapses Or(Or(a, !b), b), which substitute doesn't do
+        let expected = Bdd::try_from(
+            Expression::n_ary_or(&[new_value.clone(), var("b")])
+                & var("c")
+                & !new_value.clone()
+                & bool(true),
+        )
+        .expect("Should not panic here");
+        let actual = input.substitute(&mapping);
+
+        assert_eq!(expected, actual);
+        assert!(expected.is_equivalent(&actual));
+        assert_eq!(actual.degree(), expected.degree());
+    }
+
+    #[test]
+    fn test_substitute_variables_same_unsubstituted_ok() {
+        // (a | b) & c & !a & 1
+        let input = Bdd::try_from((var("a") | var("b")) & var("c") & !var("a") & bool(true))
+            .expect("Should not panic here");
+
+        // c | !b
+        let new_value = var("c") | !var("b");
+        let new_value_bdd = Bdd::try_from(new_value.clone()).expect("Should not panic here");
+        let mapping = BTreeMap::from_iter([("a".to_string(), new_value_bdd)]);
+
+        // cannot use `var("a") | !var("b") | var("b")` for defining expected here
+        // since that collapses Or(Or(a, !b), b), which substitute doesn't do
+        // ((c | !b) | b) & c & !(c | !b) & 1
+        let expected = Bdd::try_from(
+            Expression::n_ary_or(&[new_value.clone(), var("b")])
+                & var("c")
+                & !new_value.clone()
+                & bool(true),
+        )
+        .expect("Should not panic here");
+        let actual = input.substitute(&mapping);
+
+        assert_eq!(expected, actual);
+        assert!(expected.is_equivalent(&actual));
+        assert_eq!(actual.degree(), expected.degree());
+    }
 
     #[test]
     fn test_substitute_variables_added_only_ok() {
@@ -485,61 +489,65 @@ mod tests {
         assert_eq!(actual.degree(), expected.degree());
     }
 
-    // #[test]
-    // fn test_substitute_variables_added_and_substituted_ok() {
-    //     let input = Bdd::try_from((var("a") | var("b")) & var("c") & !var("a") & bool(true))
-    //         .expect("Should not panic here");
-    //
-    //     let new_value = var("ddd") & (bool(false) | var("a"));
-    //     let new_value_bdd = Bdd::try_from(new_value.clone()).expect("Should not panic here");
-    //     let mapping = BTreeMap::from_iter([("a".to_string(), new_value_bdd)]);
-    //
-    //     // cannot use bitwise operators for defining expected here
-    //     // since that collapses Or(Or(a, !b), b), which substitute doesn't do
-    //     let expected = Bdd::try_from(
-    //         Expression::n_ary_or(&[new_value.clone(), var("b")])
-    //             & var("c")
-    //             & !new_value.clone()
-    //             & bool(true),
-    //     )
-    //     .expect("Should not panic here");
-    //     let actual = input.substitute(&mapping);
-    //
-    //     assert_eq!(expected, actual);
-    //     assert!(expected.is_equivalent(&actual));
-    //
-    //     assert_eq!(input.degree(), 3);
-    //     assert_eq!(actual.degree(), 4);
-    //     assert_eq!(expected.degree(), 4);
-    // }
-    //
-    // #[test]
-    // fn test_substitute_variables_added_and_unsubstituted_ok() {
-    //     let input = Bdd::try_from((var("a") | var("b")) & var("c") & !var("a") & bool(true))
-    //         .expect("Should not panic here");
-    //
-    //     let new_value = var("ddd") & (bool(false) | var("b"));
-    //     let new_value_bdd = Bdd::try_from(new_value.clone()).expect("Should not panic here");
-    //     let mapping = BTreeMap::from_iter([("a".to_string(), new_value_bdd)]);
-    //
-    //     // cannot use bitwise operators for defining expected here
-    //     // since that collapses Or(Or(a, !b), b), which substitute doesn't do
-    //     let expected = Bdd::try_from(
-    //         Expression::n_ary_or(&[new_value.clone(), var("b")])
-    //             & var("c")
-    //             & !new_value.clone()
-    //             & bool(true),
-    //     )
-    //     .expect("Should not panic here");
-    //     let actual = input.substitute(&mapping);
-    //
-    //     assert_eq!(expected, actual);
-    //     assert!(expected.is_equivalent(&actual));
-    //
-    //     assert_eq!(input.degree(), 3);
-    //     assert_eq!(actual.degree(), 3);
-    //     assert_eq!(expected.degree(), 3);
-    // }
+    #[test]
+    #[should_panic]
+    fn test_substitute_variables_added_and_substituted_ok() {
+        let input = Bdd::try_from((var("a") | var("b")) & var("c") & !var("a") & bool(true))
+            .expect("Should not panic here");
+
+        let new_value = var("ddd") & (bool(false) | var("a"));
+        let new_value_bdd = Bdd::try_from(new_value.clone()).expect("Should not panic here");
+        let mapping = BTreeMap::from_iter([("a".to_string(), new_value_bdd)]);
+
+        // cannot use bitwise operators for defining expected here
+        // since that collapses Or(Or(a, !b), b), which substitute doesn't do
+        let expected = Bdd::try_from(
+            Expression::n_ary_or(&[new_value.clone(), var("b")])
+                & var("c")
+                & !new_value.clone()
+                & bool(true),
+        )
+        .expect("Should not panic here");
+        let actual = input.substitute(&mapping);
+
+        assert_eq!(expected, actual);
+        assert!(expected.is_equivalent(&actual));
+
+        assert_eq!(input.degree(), 3);
+        assert_eq!(actual.degree(), 4);
+        assert_eq!(expected.degree(), 4);
+    }
+
+    #[test]
+    fn test_substitute_variables_added_and_unsubstituted_ok() {
+        // (a | b) & c & !a & 1
+        let input = Bdd::try_from((var("a") | var("b")) & var("c") & !var("a") & bool(true))
+            .expect("Should not panic here");
+
+        // ddd & (0 | b)
+        let new_value = var("ddd") & (bool(false) | var("b"));
+        let new_value_bdd = Bdd::try_from(new_value.clone()).expect("Should not panic here");
+        let mapping = BTreeMap::from_iter([("a".to_string(), new_value_bdd)]);
+
+        // cannot use bitwise operators for defining expected here
+        // since that collapses Or(Or(a, !b), b), which substitute doesn't do
+        // ((ddd & (0 | b)) | b) & c & !(ddd & (0 | b)) & 1
+        let expected = Bdd::try_from(
+            Expression::n_ary_or(&[new_value.clone(), var("b")])
+                & var("c")
+                & !new_value.clone()
+                & bool(true),
+        )
+        .expect("Should not panic here");
+        let actual = input.substitute(&mapping);
+
+        assert_eq!(expected, actual);
+        assert!(expected.is_equivalent(&actual));
+
+        assert_eq!(input.degree(), 3);
+        assert_eq!(actual.degree(), 3);
+        assert_eq!(expected.degree(), 3);
+    }
 
     #[test]
     fn test_substitute_variables_removed_ok() {
diff --git a/src/bdd/utils/extend_variables.rs b/src/bdd/utils/extend_variables.rs
index c33b7f8..93d35c4 100644
--- a/src/bdd/utils/extend_variables.rs
+++ b/src/bdd/utils/extend_variables.rs
@@ -14,6 +14,10 @@ pub fn extend_bdd_variables<TLiteral: Debug + Clone + Eq + Ord>(
     bdd: &Bdd<TLiteral>,
     new_inputs: &[TLiteral],
 ) -> Bdd<TLiteral> {
+    if bdd.inputs == new_inputs {
+        return bdd.clone();
+    }
+
     // Test pre-condition.
     debug_assert!(bdd.inputs.iter().all(|it| new_inputs.contains(it)));
 
@@ -23,14 +27,16 @@ pub fn extend_bdd_variables<TLiteral: Debug + Clone + Eq + Ord>(
     // Also, since `bdd.inputs` is a subset of `new_inputs`, we know that every
     // `bdd.inputs[old_i]` must (eventually) appear in the `new_inputs` iterator, we just
     // need to skip enough of the new variables.
-    let mut old_i = 0;
-    for (new_i, var) in new_inputs.iter().enumerate() {
-        if new_i < bdd.inputs.len() && &bdd.inputs[old_i] == var {
+    for (old_i, var) in bdd.inputs.iter().enumerate() {
+        let new_i = new_inputs
+            .binary_search(var)
+            .expect("Collection `new_inputs` is not a superset of `bdd.inputs`.");
+
+        if new_i != old_i {
             permutation.insert(
                 BddVariable::from_index(old_i),
                 BddVariable::from_index(new_i),
             );
-            old_i += 1;
         }
     }
 
@@ -39,7 +45,9 @@ pub fn extend_bdd_variables<TLiteral: Debug + Clone + Eq + Ord>(
         // These operations are not memory-unsafe, they can just break the BDD
         // in weird ways if you don't know what you are doing.
         new_bdd.set_num_vars(u16::try_from(new_inputs.len()).unwrap());
-        new_bdd.rename_variables(&permutation);
+        if !permutation.is_empty() {
+            new_bdd.rename_variables(&permutation);
+        }
     }
 
     Bdd::new(new_bdd, new_inputs.to_owned())
diff --git a/src/bdd/utils/prune_variables.rs b/src/bdd/utils/prune_variables.rs
index 581695e..be738db 100644
--- a/src/bdd/utils/prune_variables.rs
+++ b/src/bdd/utils/prune_variables.rs
@@ -12,6 +12,10 @@ pub fn prune_bdd_variables<TLiteral: Debug + Clone + Eq + Ord>(
     bdd: &Bdd<TLiteral>,
     new_inputs: &[TLiteral],
 ) -> Bdd<TLiteral> {
+    if bdd.inputs == new_inputs {
+        return bdd.clone();
+    }
+
     // Test pre-condition.
     debug_assert!(bdd
         .essential_inputs()
@@ -22,14 +26,17 @@ pub fn prune_bdd_variables<TLiteral: Debug + Clone + Eq + Ord>(
 
     // "Inverse" of `expand_bdd_variables`. This works because both input lists are sorted
     // and the `new_inputs` is a subset of `bdd.inputs`.
-    let mut new_i = 0usize;
-    for (old_i, var) in bdd.inputs.iter().enumerate() {
-        if new_i < new_inputs.len() && &new_inputs[new_i] == var {
+    for (new_i, var) in new_inputs.iter().enumerate() {
+        let old_i = bdd
+            .inputs
+            .binary_search(var)
+            .expect("Collection `new_inputs` is not a subset of `bdd.inputs`.");
+
+        if new_i != old_i {
             permutation.insert(
                 BddVariable::from_index(old_i),
                 BddVariable::from_index(new_i),
             );
-            new_i += 1;
         }
     }
 
@@ -37,7 +44,9 @@ pub fn prune_bdd_variables<TLiteral: Debug + Clone + Eq + Ord>(
     unsafe {
         // These operations are not memory-unsafe, they can just break the BDD
         // in weird ways if you don't know what you are doing.
-        new_bdd.rename_variables(&permutation);
+        if !permutation.is_empty() {
+            new_bdd.rename_variables(&permutation);
+        }
         new_bdd.set_num_vars(u16::try_from(new_inputs.len()).unwrap());
         // Also, notice that here, we are setting the variable count *after*
         // the permutation, not before, because it is actually decreasing, not